diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/term.ml | 113 | ||||
| -rw-r--r-- | lib/term.mli | 61 |
2 files changed, 174 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 ")@]" diff --git a/lib/term.mli b/lib/term.mli new file mode 100644 index 0000000..cf79d89 --- /dev/null +++ b/lib/term.mli @@ -0,0 +1,61 @@ +(** Canonical terms: the values of Sol. + + Every literal denotes a member of a domain, and every composite + value is a labeled tuple (a record). A [t] is canonical by + construction: no reducible rational, no integer disguised as a + rational, no duplicate attribute. Structural equality is + therefore value equality, which content addressing relies on. + + The constructors are exposed [private]: pattern match freely, + build only through the smart constructors below. *) + +type t = private + | Integer of Z.t + | Rational of Q.t + (** Irreducible and with denominator strictly greater than + one. An integer-valued rational normalizes to {!Integer}, + its minimal shape, so integer membership inclusion holds + literally. *) + | String of string + | Nil (** The empty sequence, written [#()]. *) + | Record of t Label.Map.t + (** A nonempty labeled tuple. Attribute order is canonical + (by {!Label.compare}), never source order. *) + +val integer : Z.t -> t + +val string : string -> t + +val nil : t +(** The empty sequence, [#()]. The distinguished base every + {!sequence} chain ends in. *) + +val rational : num:Z.t -> den:Z.t -> (t, [ `Zero_denominator ]) result +(** Normalizes on entry: reduces by the gcd, moves the sign to the + numerator, and collapses to {!Integer} when the reduced + denominator is one. [rational ~num:4 ~den:2] is [Integer 2]. *) + +val record : (Label.t * t) list -> (t, [ `Empty_record | `Duplicate_label of Label.t ]) result +(** Builds a labeled tuple. Rejects duplicates rather than choosing + one, and rejects emptiness ({!Nil} is the only empty term). *) + +val sequence : t list -> t +(** The published elaboration of [#(a b c)]: a right fold of + [{head: _ tail: _}] records ending in {!Nil}. *) + +val cons : head:t -> tail:t -> t +(** One sequence cell, [{head: _ tail: _}]. [sequence] iterates + this; exposed for building improper or streamed chains. *) + +val equal : t -> t -> bool +(** Value equality. Sound as plain structural comparison precisely + because every [t] is canonical. *) + +val compare : t -> t -> int +(** A total order compatible with {!equal}. Exists to key maps and + to make serialization deterministic; it is not a semantic order + on domains. *) + +val pp : Format.formatter -> t -> unit +(** Prints Sol notation: [123], [1/4], ["s"], [#()], [{a: 1 b: 2}]. + A record chain shaped like a sequence prints as [#(1 2 3)]. *) |