Merge pull request #231 from LPCIC/more-red

adapt to elpi 1.13.1

Changelog.md

@@ -1,6 +1,8 @@
 # Changelog
 
-## UNRELEASED
+## [1.9.6] - 13-04-2021
+
+Requires Elpi 1.13.1 and Coq 8.13.
 
 ### API
 - New `coq.reduction.lazy.norm`

coq-builtin.elpi

@@ -1080,7 +1080,7 @@ external pred coq.gref.set.mem i:gref, i:coq.gref.set.
 % [coq.gref.set.add Elem A B] B is A union {Elem}
 external pred coq.gref.set.add i:gref, i:coq.gref.set, o:coq.gref.set.
 
-% [coq.gref.set.remove Elem A B] B is A  {Elem}
+% [coq.gref.set.remove Elem A B] B is A \ {Elem}
 external pred coq.gref.set.remove i:gref, i:coq.gref.set, o:coq.gref.set.
 
 % [coq.gref.set.union A B X] X is A union B

coq-elpi.opam

@@ -13,7 +13,7 @@ build: [ [ make "build"   "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAML
        ]
 install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
-  "elpi" {>= "1.13.0" & < "1.14.0~"}
+  "elpi" {>= "1.13.1" & < "1.14.0~"}
   "coq" {>= "8.13" & < "8.14~" }
   ]
 tags: [ "logpath:elpi" ]

elpi-builtin.elpi

@@ -119,6 +119,14 @@ type iabs int -> int.
 
 type rabs float -> float.
 
+type max int -> int -> int.
+
+type max float -> float -> float.
+
+type min int -> int -> int.
+
+type min float -> float -> float.
+
 type sqrt float -> float.
 
 type sin float -> float.
@@ -254,29 +262,44 @@ external type dprint variadic any prop.
 % [print ...] prints terms
 external type print variadic any prop.
 
-% [counter Name Value] reads the Value of a trace point Name
-external pred counter i:string, o:int.
+% Deprecated, use trace.counter
+pred counter i:string, o:int.
+counter C N :- trace.counter C N.
+
+% [quote_syntax FileName QueryText QuotedProgram QuotedQuery] quotes the
+% program from FileName and the QueryText. See elpi-quoted_syntax.elpi for
+% the syntax tree
+external pred quote_syntax i:string, i:string, o:list A, o:A.
 
-% [rex_match Rex Subject] checks if Subject matches Rex. Matching is based
+typeabbrev loc (ctype "Loc.t").
+
+
+% == Regular Expressions =====================================
+
+% [rex.match Rex Subject] checks if Subject matches Rex. Matching is based
 % on OCaml's Str library
-external pred rex_match i:string, i:string.
+external pred rex.match i:string, i:string.
 
-% [rex_replace Rex Replacement Subject Out] Out is obtained by replacing all
+% [rex.replace Rex Replacement Subject Out] Out is obtained by replacing all
 % occurrences of Rex with Replacement in Subject. See also OCaml's
 % Str.global_replace
-external pred rex_replace i:string, i:string, i:string, o:string.
+external pred rex.replace i:string, i:string, i:string, o:string.
 
-% [rex_split Rex Subject Out] Out is obtained by splitting Subject at all
+% [rex.split Rex Subject Out] Out is obtained by splitting Subject at all
 % occurrences of Rex. See also OCaml's Str.split
-external pred rex_split i:string, i:string, o:list string.
+external pred rex.split i:string, i:string, o:list string.
 
-% [quote_syntax FileName QueryText QuotedProgram QuotedQuery] quotes the
-% program from FileName and the QueryText. See elpi-quoted_syntax.elpi for
-% the syntax tree
-external pred quote_syntax i:string, i:string, o:list A, o:A.
+% Deprecated, use rex.match
+pred rex_match i:string, i:string.
+rex_match Rx S :- rex.match Rx S.
 
-typeabbrev loc (ctype "Loc.t").
+% Deprecated, use rex.replace
+pred rex_replace i:string, i:string, i:string, o:string.
+rex_replace Rx R S O :- rex.replace Rx R S O.
 
+% Deprecated, use rex.split
+pred rex_split i:string, i:string, o:list string.
+rex_split Rx S L :- rex.split Rx S L.
 
 % == Elpi nonlogical builtins =====================================
 
@@ -422,15 +445,15 @@ assert-ok! _ Msg :- fatal-error-w-data Msg "no diagnostic returned".
 
 % [spy P] traces the call to P, printing all success and the final failure
 pred spy i:prop.
-spy P :- counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
+spy P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
          debug-print "----<<---- enter: " P,
          P,
          debug-print "---->>---- exit: " P.
 spy P :- debug-print "---->>---- fail: " P, fail.
 
 % [spy! P] traces the first call to P without leaving a choice point
 pred spy! i:prop.
-spy! P :- counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
+spy! P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
          debug-print "----<<---- enter: " P,
          P,
          debug-print "---->>---- exit: " P, !.
@@ -753,7 +776,7 @@ external pred std.string.set.mem i:string, i:std.string.set.
 external pred std.string.set.add i:string, i:std.string.set, 
                                  o:std.string.set.
 
-% [std.string.set.remove Elem A B] B is A  {Elem}
+% [std.string.set.remove Elem A B] B is A \ {Elem}
 external pred std.string.set.remove i:string, i:std.string.set, 
                                     o:std.string.set.
 
@@ -792,7 +815,7 @@ external pred std.int.set.mem i:int, i:std.int.set.
 % [std.int.set.add Elem A B] B is A union {Elem}
 external pred std.int.set.add i:int, i:std.int.set, o:std.int.set.
 
-% [std.int.set.remove Elem A B] B is A  {Elem}
+% [std.int.set.remove Elem A B] B is A \ {Elem}
 external pred std.int.set.remove i:int, i:std.int.set, o:std.int.set.
 
 % [std.int.set.union A B X] X is A union B
@@ -830,7 +853,7 @@ external pred std.loc.set.mem i:loc, i:std.loc.set.
 % [std.loc.set.add Elem A B] B is A union {Elem}
 external pred std.loc.set.add i:loc, i:std.loc.set, o:std.loc.set.
 
-% [std.loc.set.remove Elem A B] B is A  {Elem}
+% [std.loc.set.remove Elem A B] B is A \ {Elem}
 external pred std.loc.set.remove i:loc, i:std.loc.set, o:std.loc.set.
 
 % [std.loc.set.union A B X] X is A union B
@@ -1136,6 +1159,50 @@ external pred system i:string, o:int.
 % [term_to_string T S] prints T to S
 external pred term_to_string i:any, o:string.
 
+% == Elpi runtime builtins =====================================
+
+% [trace.counter Name Value] reads the Value of a trace point Name
+external pred trace.counter i:string, o:int.
+
+% [gc.get MinorHeapSize MajorHeapIncrement SpaceOverhead Verbose MaxOverhead
+% StackLimit AllocationPolicy WindowSize] Reads the current settings of the
+% garbage collector. See also OCaml's Gc.control type documentation.
+external pred gc.get o:int, o:int, o:int, o:int, o:int, o:int, o:int, 
+                     o:int.
+
+% [gc.set MinorHeapSize MajorHeapIncrement SpaceOverhead Verbose MaxOverhead
+% StackLimit AllocationPolicy WindowSize] Writes the current settings of the
+% garbage collector. Any parameter left unspecificed (eg _) is not changed.
+% See also OCaml's Gc.control type documentation.
+external pred gc.set i:int, i:int, i:int, i:int, i:int, i:int, i:int, 
+                     i:int.
+
+% [gc.minor] See OCaml's Gc.minor documentation.
+external pred gc.minor .
+
+% [gc.major] See OCaml's Gc.major documentation.
+external pred gc.major .
+
+% [gc.full] See OCaml's Gc.full_major documentation.
+external pred gc.full .
+
+% [gc.compact] See OCaml's Gc.compact documentation.
+external pred gc.compact .
+
+% [gc.stat MinorWords PromotedWords MajorWords MinorCollections
+% MajorCollections HeapWords HeapChunks LiveWords LiveBlocks FreeWords
+% FreeBlocks LargestFree Fragments Compactions TopHeapWords StackSize] See
+% OCaml's Gc.stat documentation.
+external pred gc.stat o:float, o:float, o:float, o:int, o:int, o:int, 
+                      o:int, o:int, o:int, o:int, o:int, o:int, o:int, 
+                      o:int, o:int, o:int.
+
+% [gc.quick-stat MinorWords PromotedWords MajorWords MinorCollections
+% MajorCollections HeapWords HeapChunks Compactions TopHeapWords StackSize]
+% See OCaml's Gc.quick_stat documentation.
+external pred gc.quick-stat o:float, o:float, o:float, o:int, o:int, 
+                            o:int, o:int, o:int, o:int, o:int.
+
 
 
 

src/coq_elpi_HOAS.ml

@@ -638,7 +638,7 @@ let get_options ~depth hyps state =
   let get_pair_option fst snd name =
     try
       let t, depth = API.Data.StrMap.find name map in
-      let _, b, _ = Elpi.Builtin.(pair (unspec fst) (unspec snd)).API.Conversion.readback ~depth state t in
+      let _, b, _ = (Elpi.Builtin.pair (unspec fst) (unspec snd)).API.Conversion.readback ~depth state t in
       Some b
     with Not_found -> None in
   let empty2none = function Some "" -> None | x -> x in

src/coq_elpi_vernacular.ml

@@ -410,7 +410,7 @@ let elpi_builtins =
     Elpi.Builtin.(core_builtins @
     elpi_builtins @ elpi_nonlogical_builtins @
     elpi_stdlib @ elpi_map @ elpi_set @
-    io_builtins)
+    io_builtins @ ocaml_runtime)
 
 let coq_builtins =
   API.BuiltIn.declare