canonical term algebra: labels, records, rationals, sequences

1 files changed, 113 insertions, 0 deletions

diff --git a/lib/term.ml b/lib/term.ml
new file mode 100644
index 0000000..a0dc760
--- /dev/null
+++ b/lib/term.ml
@@ -0,0 +1,113 @@
+type t =
+  | Integer of Z.t
+  | Rational of Q.t
+  | String of string
+  | Nil
+  | Record of t Label.Map.t
+
+let integer z = Integer z
+let string s = String s
+let nil = Nil
+
+let rational ~num ~den =
+  if Z.equal den Z.zero then Error `Zero_denominator
+  else
+    (* Q.make reduces by the gcd and moves the sign to the
+       numerator; collapsing den = 1 to Integer is the minimal-shape
+       rule that makes integer inclusion literal. *)
+    let q = Q.make num den in
+    if Z.equal (Q.den q) Z.one then Ok (Integer (Q.num q))
+    else Ok (Rational q)
+
+let record bindings =
+  match bindings with
+  | [] -> Error `Empty_record
+  | _ ->
+      let step acc (label, term) =
+        match acc with
+        | Error _ as e -> e
+        | Ok map ->
+            if Label.Map.mem label map then Error (`Duplicate_label label)
+            else Ok (Label.Map.add label term map)
+      in
+      Result.map
+        (fun map -> Record map)
+        (List.fold_left step (Ok Label.Map.empty) bindings)
+
+(* The head/tail labels of sequence cells. Direct construction:
+   both spellings are well formed by inspection. *)
+let head_label =
+  match Label.of_string "head" with Ok l -> l | Error _ -> assert false
+
+let tail_label =
+  match Label.of_string "tail" with Ok l -> l | Error _ -> assert false
+
+let cons ~head ~tail =
+  Record Label.Map.(empty |> add head_label head |> add tail_label tail)
+
+let sequence items = List.fold_right (fun x acc -> cons ~head:x ~tail:acc) items Nil
+
+let rec compare a b =
+  match (a, b) with
+  | Integer x, Integer y -> Z.compare x y
+  | Rational x, Rational y -> Q.compare x y
+  | String x, String y -> String.compare x y
+  | Nil, Nil -> 0
+  | Record x, Record y -> Label.Map.compare compare x y
+  | Integer _, _ -> -1
+  | _, Integer _ -> 1
+  | Rational _, _ -> -1
+  | _, Rational _ -> 1
+  | String _, _ -> -1
+  | _, String _ -> 1
+  | Nil, _ -> -1
+  | _, Nil -> 1
+
+let equal a b = compare a b = 0
+
+(* A record prints as #( ... ) exactly when it is a cell of the
+   sequence elaboration: the two labels head and tail, nothing else. *)
+let as_cell = function
+  | Record map when Label.Map.cardinal map = 2 -> (
+      match
+        (Label.Map.find_opt head_label map, Label.Map.find_opt tail_label map)
+      with
+      | Some head, Some tail -> Some (head, tail)
+      | _ -> None)
+  | _ -> None
+
+let rec pp fmt t =
+  match t with
+  | Integer z -> Z.pp_print fmt z
+  | Rational q -> Q.pp_print fmt q
+  | String s -> Format.fprintf fmt "%S" s
+  | Nil -> Format.pp_print_string fmt "#()"
+  | Record map -> (
+      match as_cell t with
+      | Some (head, tail) -> pp_sequence fmt head tail
+      | None ->
+          Format.fprintf fmt "@[<hv 1>{";
+          let first = ref true in
+          Label.Map.iter
+            (fun label term ->
+              if not !first then Format.fprintf fmt "@ ";
+              first := false;
+              Format.fprintf fmt "%a %a" Label.pp label pp term)
+            map;
+          Format.fprintf fmt "}@]")
+
+and pp_sequence fmt head tail =
+  Format.fprintf fmt "@[<hv 2>#(%a" pp head;
+  let rec spine = function
+    | Nil -> ()
+    | t -> (
+        match as_cell t with
+        | Some (h, rest) ->
+            Format.fprintf fmt "@ %a" pp h;
+            spine rest
+        | None ->
+            (* An improper chain: honest about the dangling tail. *)
+            Format.fprintf fmt "@ | %a" pp t)
+  in
+  spine tail;
+  Format.fprintf fmt ")@]"