relation references as a term kind, written #Name

2 files changed, 10 insertions, 2 deletions

diff --git a/lib/pattern.ml b/lib/pattern.ml
index 5186e04..9c69622 100644
--- a/lib/pattern.ml
+++ b/lib/pattern.ml
@@ -3,6 +3,7 @@ type t =
   | Integer of Z.t
   | Rational of Q.t
   | String of string
+  | Reference of string
   | Nil
   | Record of t Label.Map.t
 
@@ -11,11 +12,13 @@ let rec of_term (term : Term.t) =
   | Term.Integer z -> Integer z
   | Term.Rational q -> Rational q
   | Term.String s -> String s
+  | Term.Reference name -> Reference name
   | Term.Nil -> Nil
   | Term.Record map -> Record (Label.Map.map of_term map)
 
 let rec to_term = function
   | Var _ -> None
+  | Reference name -> Result.to_option (Term.reference name)
   | Integer z -> Some (Term.integer z)
   | Rational q ->
       (* Rebuilding through the smart constructor keeps canonicity a
@@ -40,7 +43,7 @@ let is_ground pattern = Option.is_some (to_term pattern)
 let vars pattern =
   let rec collect acc = function
     | Var v -> if List.mem v acc then acc else v :: acc
-    | Integer _ | Rational _ | String _ | Nil -> acc
+    | Integer _ | Rational _ | String _ | Reference _ | Nil -> acc
     | Record map -> Label.Map.fold (fun _ p acc -> collect acc p) map acc
   in
   List.rev (collect [] pattern)
@@ -60,6 +63,7 @@ let rec equal a b =
   | Integer x, Integer y -> Z.equal x y
   | Rational x, Rational y -> Q.equal x y
   | String x, String y -> String.equal x y
+  | Reference x, Reference y -> String.equal x y
   | Nil, Nil -> true
   | Record x, Record y -> Label.Map.equal equal x y
   | _ -> false
@@ -73,11 +77,12 @@ type checker_leaf =
   | L_int of Z.t
   | L_rat of Q.t
   | L_str of string
+  | L_ref of string
   | L_nil
 
 let checker_leaf_equal a b =
   match (a, b) with
-  | L_var x, L_var y | L_str x, L_str y -> String.equal x y
+  | L_var x, L_var y | L_str x, L_str y | L_ref x, L_ref y -> String.equal x y
   | L_int x, L_int y -> Z.equal x y
   | L_rat x, L_rat y -> Q.equal x y
   | L_nil, L_nil -> true
@@ -88,6 +93,7 @@ let rec to_checker = function
   | Integer z -> Decrease_extracted.Leaf (L_int z)
   | Rational q -> Decrease_extracted.Leaf (L_rat q)
   | String s -> Decrease_extracted.Leaf (L_str s)
+  | Reference name -> Decrease_extracted.Leaf (L_ref name)
   | Nil -> Decrease_extracted.Leaf L_nil
   | Record map ->
       Decrease_extracted.Node
@@ -105,6 +111,7 @@ let rec pp fmt = function
   | 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 ->
       Format.fprintf fmt "@[<hv 1>{";
diff --git a/lib/pattern.mli b/lib/pattern.mli
index f79dce0..f14a8e5 100644
--- a/lib/pattern.mli
+++ b/lib/pattern.mli
@@ -12,6 +12,7 @@ type t =
   | Integer of Z.t
   | Rational of Q.t
   | String of string
+  | Reference of string  (** a relation reference, [#Name] *)
   | Nil
   | Record of t Label.Map.t