Merge pull request #634 from rlepigre/br/prim-string

Adapt to rocq-prover/rocq#18973.

Author: gares

coq-builtin.elpi

@@ -1080,6 +1080,9 @@ typeabbrev uint63 (ctype "uint63").
 typeabbrev float64 (ctype "float64").
 
 
+typeabbrev pstring (ctype "pstring").
+
+
 typeabbrev projection (ctype "projection").
 
 
@@ -1088,6 +1091,7 @@ kind primitive-value type.
 type uint63 uint63 -> primitive-value. % unsigned integers over 63 bits
 type float64 float64 ->
              primitive-value. % double precision foalting points
+type pstring pstring -> primitive-value. % primitive string
 type proj projection -> int -> primitive-value. % primitive projection
 
 % [coq.uint63->int U I] Transforms a primitive unsigned integer U into an
@@ -1106,6 +1110,15 @@ external pred coq.float64->float i:float64, o:float.
 % on 64 bits. Currently, it should not fail.
 external pred coq.float->float64 i:float, o:float64.
 
+% [coq.pstring->string PS S] Transforms a Coq primitive string to an elpi
+% string. It does not fail.
+external pred coq.pstring->string i:pstring, o:string.
+
+% [coq.string->pstring S PS] Transforms an elpi string into a Coq primitive
+% string. It fails if the lenght of S is greater than the maximal primitive
+% string length.
+external pred coq.string->pstring i:string, o:pstring.
+
 
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for extra logical objects

elpi/elpi_elaborator.elpi

@@ -310,6 +310,7 @@ of (pglobal GR I as X) T X :-
 
 of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:elpi.uint63 }} T.
 of (primitive (float64 _) as X) T X :- unify-leq {{ lib:elpi.float64 }} T.
+of (primitive (pstring _) as X) T X :- unify-leq {{ lib:elpi.pstring }} T.
 
 of (uvar as X) T Y :- !, evar X T Y.
 

src/coq_elpi_HOAS.ml

@@ -728,6 +728,7 @@ let primitivec   = E.Constants.declare_global_symbol "primitive"
 type primitive_value =
   | Uint63 of Uint63.t
   | Float64 of Float64.t
+  | Pstring of Pstring.t
   | Projection of Projection.t
 
 let primitive_value : primitive_value API.Conversion.t =
@@ -738,6 +739,7 @@ let primitive_value : primitive_value API.Conversion.t =
   pp = (fun fmt -> function
     | Uint63 i -> Format.fprintf fmt "Type"
     | Float64 f -> Format.fprintf fmt "Set"
+    | Pstring s -> Format.fprintf fmt "Set"
     | Projection p -> Format.fprintf fmt "");
   constructors = [
     K("uint63","unsigned integers over 63 bits",A(B.uint63,N),
@@ -746,6 +748,9 @@ let primitive_value : primitive_value API.Conversion.t =
     K("float64","double precision foalting points",A(B.float64,N),
       B (fun x -> Float64 x),
       M (fun ~ok ~ko -> function Float64 x -> ok x | _ -> ko ()));
+    K("pstring","primitive string",A(B.pstring,N),
+      B (fun x -> Pstring x),
+      M (fun ~ok ~ko -> function Pstring x -> ok x | _ -> ko ()));
     K("proj","primitive projection",A(B.projection,A(API.BuiltInData.int,N)),
       B (fun p n -> Projection p),
       M (fun ~ok ~ko -> function Projection p -> ok p Names.Projection.(arg p + npars p) | _ -> ko ()));
@@ -1382,6 +1387,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
     | C.CoFix _ -> nYI "HOAS for cofix"
     | C.Int i -> in_elpi_primitive ~depth state (Uint63 i)
     | C.Float f -> in_elpi_primitive ~depth state (Float64 f)
+    | C.String s -> in_elpi_primitive ~depth state (Pstring s)
     | C.Array _ -> nYI "HOAS for persistent arrays"
   in
   debug Pp.(fun () ->
@@ -1975,6 +1981,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
       begin match v with
       | Uint63 i -> state, EC.mkInt i, gls
       | Float64 f -> state, EC.mkFloat f, gls
+      | Pstring s -> state, EC.mkString s, gls
       | Projection p -> state, EC.UnsafeMonomorphic.mkConst (Names.Projection.constant p), gls
       end
 

src/coq_elpi_HOAS.mli

@@ -180,6 +180,7 @@ val collect_term_variables : depth:int -> term -> Names.Id.t list
 type primitive_value =
   | Uint63 of Uint63.t
   | Float64 of Float64.t
+  | Pstring of Pstring.t
   | Projection of Projection.t
 val primitive_value : primitive_value Conversion.t
 val in_elpi_primitive : depth:int -> state -> primitive_value -> state * term

src/coq_elpi_builtins.ml

@@ -2513,6 +2513,7 @@ declared as cumulative.|};
 
   MLData Coq_elpi_utils.uint63;
   MLData Coq_elpi_utils.float64;
+  MLData Coq_elpi_utils.pstring;
   MLData Coq_elpi_utils.projection;
   MLData primitive_value;
 
@@ -2553,6 +2554,23 @@ declared as cumulative.|};
        !: (Float64.of_float f))),
   DocAbove);
 
+  MLCode(Pred("coq.pstring->string",
+    In(Coq_elpi_utils.pstring,"PS",
+    Out(B.string,"S",
+    Easy "Transforms a Coq primitive string to an elpi string. It does not fail.")),
+    (fun s _ ~depth:_ -> !: (Pstring.to_string s))),
+  DocAbove);
+
+  MLCode(Pred("coq.string->pstring",
+    In(B.string,"S",
+    Out(Coq_elpi_utils.pstring,"PS",
+    Easy "Transforms an elpi string into a Coq primitive string. It fails if the lenght of S is greater than the maximal primitive string length.")),
+    (fun s _ ~depth:_ ->
+       match Pstring.of_string s with
+       | Some s -> !: s
+       | None -> raise No_clause)),
+  DocAbove);
+
   LPCode {|
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for extra logical objects

src/coq_elpi_glob_quotation.ml

@@ -379,6 +379,7 @@ let rec gterm2lp ~depth state x =
   | GRec _ -> nYI "(glob)HOAS mutual/non-struct fix"
   | GInt i -> in_elpi_primitive ~depth state (Uint63 i)
   | GFloat f -> in_elpi_primitive ~depth state (Float64 f)
+  | GString s -> in_elpi_primitive ~depth state (Pstring s)
   | GArray _ -> nYI "(glob)HOAS persistent arrays"
 ;;
 

src/coq_elpi_utils.ml

@@ -190,6 +190,18 @@ let float64 : Float64.t Elpi.API.Conversion.t =
     constants = [];
   }
 
+let pstring : Pstring.t Elpi.API.Conversion.t =
+  let open Elpi.API.OpaqueData in
+  declare {
+    name = "pstring";
+    doc = "";
+    pp = (fun fmt s -> Format.fprintf fmt "%S" (Pstring.to_string s));
+    compare = Pstring.compare;
+    hash = Pstring.hash;
+    hconsed = false;
+    constants = [];
+  }
+
 let debug = CDebug.create ~name:"elpi" ()
 
   let projection : Names.Projection.t Elpi.API.Conversion.t =

src/coq_elpi_utils.mli

@@ -44,6 +44,7 @@ val fold_elpi_term :
 
 val uint63 : Uint63.t Elpi.API.Conversion.t
 val float64 : Float64.t Elpi.API.Conversion.t
+val pstring : Pstring.t Elpi.API.Conversion.t
 val projection : Names.Projection.t Elpi.API.Conversion.t
 
 val debug : CDebug.t

theories/elpi.v

@@ -46,7 +46,8 @@ Register Coq.Bool.Bool.reflect  as elpi.reflect.
 Register Coq.Bool.Bool.ReflectF as elpi.ReflectF.
 Register Coq.Bool.Bool.ReflectT as elpi.ReflectT.
 
-From Coq Require PrimFloat PrimInt63.
+From Coq Require PrimFloat PrimInt63 PrimString.
 
 Register Coq.Floats.PrimFloat.float as elpi.float64.
 Register Coq.Numbers.Cyclic.Int63.PrimInt63.int as elpi.uint63.
+Register Coq.Strings.PrimString.string as elpi.pstring.