aboutsummaryrefslogtreecommitdiffstats
path: root/lib/term.ml
diff options
context:
space:
mode:
authorMarcos Magueta <maguetamarcos@gmail.com>2026-07-12 17:55:27 -0300
committerMarcos Magueta <maguetamarcos@gmail.com>2026-07-12 17:56:11 -0300
commitb4a2485afbf74e99e2147086fbca0568b7e2b7b8 (patch)
treef2f0f653c7de2d5a1b1565d0ec48c46dec580a5a /lib/term.ml
parentb7ab0a9d1f0275db32a526faf7cffe9d520b15c8 (diff)
downloadSOL-b4a2485afbf74e99e2147086fbca0568b7e2b7b8.tar.gz
SOL-b4a2485afbf74e99e2147086fbca0568b7e2b7b8.zip
relation references as a term kind, written #Name
Diffstat (limited to 'lib/term.ml')
-rw-r--r--lib/term.ml15
1 files changed, 15 insertions, 0 deletions
diff --git a/lib/term.ml b/lib/term.ml
index a0dc760..fcef6f9 100644
--- a/lib/term.ml
+++ b/lib/term.ml
@@ -2,6 +2,7 @@ type t =
| Integer of Z.t
| Rational of Q.t
| String of string
+ | Reference of string
| Nil
| Record of t Label.Map.t
@@ -9,6 +10,16 @@ let integer z = Integer z
let string s = String s
let nil = Nil
+let reference name =
+ let is_letter c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') in
+ let is_body c = is_letter c || (c >= '0' && c <= '9') || c = '_' in
+ if
+ String.length name > 0
+ && is_letter name.[0]
+ && String.for_all is_body name
+ then Ok (Reference name)
+ else Error (`Invalid_reference name)
+
let rational ~num ~den =
if Z.equal den Z.zero then Error `Zero_denominator
else
@@ -52,6 +63,7 @@ let rec compare a b =
| Integer x, Integer y -> Z.compare x y
| Rational x, Rational y -> Q.compare x y
| String x, String y -> String.compare x y
+ | Reference x, Reference y -> String.compare x y
| Nil, Nil -> 0
| Record x, Record y -> Label.Map.compare compare x y
| Integer _, _ -> -1
@@ -60,6 +72,8 @@ let rec compare a b =
| _, Rational _ -> 1
| String _, _ -> -1
| _, String _ -> 1
+ | Reference _, _ -> -1
+ | _, Reference _ -> 1
| Nil, _ -> -1
| _, Nil -> 1
@@ -81,6 +95,7 @@ let rec pp fmt t =
| Integer z -> Z.pp_print fmt z
| Rational q -> Q.pp_print fmt q
| String s -> Format.fprintf fmt "%S" s
+ | Reference name -> Format.fprintf fmt "#%s" name
| Nil -> Format.pp_print_string fmt "#()"
| Record map -> (
match as_cell t with