exposed additional primitives

src/builtin.ml

@@ -105,6 +105,18 @@ let bool = AlgebraicData.declare {
   ]
 }|> ContextualConversion.(!<)
 
+let char : char Conversion.t =  {
+  ty = TyName "char";
+  pp_doc = (fun fmt () -> Format.fprintf fmt "Char values: single character strings");
+  pp = (fun fmt b -> Format.fprintf fmt "%c" b);
+  embed = (fun ~depth (st: State.t) (c: char) -> BuiltInData.string.embed ~depth st (String.make 1 c));
+  readback = (fun ~depth st term  ->
+      let st,name,goals = BuiltInData.string.readback ~depth st term in
+      st,name.[0],goals
+    );
+}
+
+
 let pair a b = let open AlgebraicData in declare {
   ty = TyApp ("pair",a.Conversion.ty,[b.Conversion.ty]);
   doc = "Pair: the constructor is pr, since ',' is for conjunction";
@@ -116,6 +128,28 @@ let pair a b = let open AlgebraicData in declare {
   ]
 } |> ContextualConversion.(!<)
 
+let triple a b c = let open AlgebraicData in declare {
+  ty = TyApp ("triple",a.Conversion.ty,[b.Conversion.ty;c.Conversion.ty]);
+  doc = "Triple: the constructor is trpl, since ',' is for conjunction";
+  pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_triple a.Conversion.pp b.Conversion.pp c.Conversion.pp) o);
+  constructors = [
+    K("trpl","",A(a,A(b,A(c,N))),
+      B (fun a b c -> (a,b, c)),
+      M (fun ~ok ~ko:_ -> function (a,b,c) -> ok a b c));
+  ]
+} |> ContextualConversion.(!<)
+
+let quadruple a b c d = let open AlgebraicData in declare {
+  ty = TyApp ("quadruple",a.Conversion.ty,[b.Conversion.ty;c.Conversion.ty;d.Conversion.ty]);
+  doc = "Quadruple: the constructor is quadrpl, since ',' is for conjunction";
+  pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_quadruple a.Conversion.pp b.Conversion.pp c.Conversion.pp d.Conversion.pp) o);
+  constructors = [
+    K("quadrpl","",A(a,A(b,A(c,A(d,N)))),
+      B (fun a b c d -> (a,b,c,d)),
+      M (fun ~ok ~ko:_ -> function (a,b,c,d) -> ok a b c d));
+  ]
+} |> ContextualConversion.(!<)
+
 let option a = let open AlgebraicData in declare {
   ty = TyApp("option",a.Conversion.ty,[]);
   doc = "The option type (aka Maybe)";

src/builtin.mli

@@ -56,8 +56,11 @@ val std_builtins : API.Setup.builtins
 
 (* Type descriptors for built-in predicates *)
 val pair : 'a API.Conversion.t -> 'b API.Conversion.t -> ('a * 'b) API.Conversion.t
+val triple : 'a API.Conversion.t -> 'b API.Conversion.t -> 'c API.Conversion.t -> ('a * 'b * 'c) API.Conversion.t
+val quadruple : 'a API.Conversion.t -> 'b API.Conversion.t -> 'c API.Conversion.t -> 'd API.Conversion.t -> ('a * 'b * 'c * 'd) API.Conversion.t
 val option : 'a API.Conversion.t -> 'a option API.Conversion.t
 val bool : bool API.Conversion.t
+val char : char API.Conversion.t
 
 (* A standard way to make a predicate always succeed but still give errors *)
 type diagnostic = private OK | ERROR of string API.BuiltInPredicate.ioarg

src/utils/util.ml

@@ -340,11 +340,77 @@ module Pair = struct
   let show poly_a poly_b x =
     Format.asprintf "@[%a@]" (pp poly_a poly_b) x
 end
+
+module Triple = struct
+
+  let pp poly_a poly_b poly_c fmt x =
+    let (x0, x1, x2) = x in
+    Format.pp_open_box fmt 1;
+    Format.pp_print_string fmt "(";
+    Format.pp_open_box fmt 0;
+    poly_a fmt x0;
+    Format.pp_close_box fmt ();
+    Format.pp_print_string fmt ",";
+    Format.pp_print_space fmt ();
+    Format.pp_open_box fmt 0;
+    poly_b fmt x1;
+    Format.pp_close_box fmt ();
+    Format.pp_print_string fmt ",";
+    Format.pp_print_space fmt ();
+    Format.pp_open_box fmt 0;
+    poly_c fmt x2;
+    Format.pp_close_box fmt ();
+    Format.pp_print_string fmt ")";
+    Format.pp_close_box fmt ()
+
+  let show poly_a poly_b poly_c x =
+    Format.asprintf "@[%a@]" (pp poly_a poly_b poly_c) x
+end
+
+module Quadruple = struct
+
+  let pp poly_a poly_b poly_c poly_d fmt x =
+    let (x0, x1, x2, x3) = x in
+    Format.pp_open_box fmt 1;
+    Format.pp_print_string fmt "(";
+    Format.pp_open_box fmt 0;
+    poly_a fmt x0;
+    Format.pp_close_box fmt ();
+    Format.pp_print_string fmt ",";
+    Format.pp_print_space fmt ();
+    Format.pp_open_box fmt 0;
+    poly_b fmt x1;
+    Format.pp_close_box fmt ();
+    Format.pp_print_string fmt ",";
+    Format.pp_print_space fmt ();
+    Format.pp_open_box fmt 0;
+    poly_c fmt x2;
+    Format.pp_close_box fmt ();
+    Format.pp_print_string fmt ",";
+    Format.pp_print_space fmt ();
+    Format.pp_open_box fmt 0;
+    poly_d fmt x3;
+    Format.pp_close_box fmt ();
+    Format.pp_print_string fmt ")";
+    Format.pp_close_box fmt ()
+
+  let show poly_a poly_b poly_c poly_d x =
+    Format.asprintf "@[%a@]" (pp poly_a poly_b poly_c poly_d) x
+end
+
+
+
+
 let pp_option f fmt = function None -> () | Some x -> f fmt x
 let pp_int = Int.pp
 let pp_string = String.pp
 let pp_pair = Pair.pp
 let show_pair = Pair.show
+let pp_triple = Triple.pp
+let show_triple = Triple.show
+let pp_quadruple = Quadruple.pp
+let show_quadruple = Quadruple.show
+
 
 let remove_from_list x =
  let rec aux acc =

src/utils/util.mli

@@ -174,6 +174,32 @@ val show_pair :
   (Format.formatter -> 'b -> unit) ->
     ('a * 'b) -> string
 
+val pp_triple :
+  (Format.formatter -> 'a -> unit) ->
+  (Format.formatter -> 'b -> unit) ->
+  (Format.formatter -> 'c -> unit) ->
+    Format.formatter -> 'a * 'b * 'c -> unit
+val show_triple :
+  (Format.formatter -> 'a -> unit) ->
+  (Format.formatter -> 'b -> unit) ->
+  (Format.formatter -> 'c -> unit) ->
+    ('a * 'b * 'c) -> string
+
+val pp_quadruple :
+  (Format.formatter -> 'a -> unit) ->
+  (Format.formatter -> 'b -> unit) ->
+  (Format.formatter -> 'c -> unit) ->
+  (Format.formatter -> 'd -> unit) ->
+    Format.formatter -> 'a * 'b * 'c * 'd -> unit
+val show_quadruple :
+  (Format.formatter -> 'a -> unit) ->
+  (Format.formatter -> 'b -> unit) ->
+  (Format.formatter -> 'c -> unit) ->
+  (Format.formatter -> 'd -> unit) ->
+    ('a * 'b * 'c * 'd) -> string
+
+
+
 (* for open types *)
 type 'a spaghetti_printer
 val mk_spaghetti_printer : unit -> 'a spaghetti_printer
@@ -275,4 +301,4 @@ end
 (* file access *)
 val std_resolver :
   ?cwd:string -> paths:string list -> unit ->
-     (?cwd:string -> unit:string -> unit -> string)
+     (?cwd:string -> unit:string -> unit -> string)