Merge branch 'master' into tracer

Author: gares

.github/workflows/main.yml

@@ -124,7 +124,7 @@ jobs:
         if: runner.os == 'Windows'
         run: |
           opam exec -- ls -l tests/sources/*.elpi
-          opam exec -- make tests PWD=${{ env.workspace }} RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe' TIME=--time=D:/cygwin/bin/time.exe
+          opam exec -- make tests PWD=${{ env.workspace }} RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe' TIME=--time=C:/cygwin/bin/time.exe
 
 # Artifacts 2 ################################################################
 

.github/workflows/users.yml

@@ -30,10 +30,10 @@ jobs:
           env:
             OPAMWITHTEST: false
 
-        - run: opam pin --ignore-constraints-on elpi add rocq-elpi https://github.com/LPCIC/coq-elpi.git#fix-elpi-3.0
-        - run: opam pin --ignore-constraints-on elpi add coq-elpi https://github.com/LPCIC/coq-elpi.git#fix-elpi-3.0
+        - run: opam pin --ignore-constraints-on elpi add rocq-elpi https://github.com/LPCIC/coq-elpi.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-elpi https://github.com/LPCIC/coq-elpi.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-stdlib https://github.com/rocq-prover/stdlib.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/gares/hierarchy-builder.git#elpi-3.0
+        - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-boot https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-order https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master

CHANGES.md

@@ -1,5 +1,71 @@
+# v3.4.2 (October 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Runtime:
+  - Fix bug concerning CHR rules firing on non-fully-dereffed terms
+
+# v3.4.1 (September 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Compiler:
+  - Fix extend_signature, was not updating the symbol table
+
+# v3.4.0 (September 2025)
+
+- Parser:
+  - New `->`-based syntax for `pred`, analogous to the new `func` one. E.g.
+    ```
+    func append list A, list A -> list A.
+    pred appendR -> list A, list A, list A.
+    ```
+
+- Compiler:
+  - Fix `=!=>` that was adding a head cut, rather than a tail cut, in some
+    cases
+  - Fix compilation bug concerning `Loc.t` being erroneously compared
+
+# v3.3.1 (September 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Tests:
+  - compare json files semantically
+
+# v3.3.0 (September 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Tooling:
+  - port to ppxlib 0.36.0
+
+# v3.2.0 (September 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Language:
+  - Remove: the `fprop` sort, use `(func)` instead
+
+# v3.1.0 (August 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Language:
+  - Change: constraints must be functions. Hence `declare_constraint` only
+    suspends functional predicated and CHR rules can only generate
+    determinitic goals.
+  - New: the `func` syntax now supports variadic functions as in
+    ```prolog
+    func f int, int -> int.. .
+    f N D Q   :- Q is N div D.
+    f N D Q R :- f N D Q, R is N mod D.
+    ```
+
 # v3.0.1 (July 2025)
 
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
 - Language:
   - Improve error message for non deterministic atom
   - Fix overlap check for `uvar F L as X`

ELPI.md

@@ -55,6 +55,8 @@ is very welcome. Questions or feature requests are welcome as well.
 - [Accumulate with paths](#accumulate-with-paths) accepts `accumulate "path".`
   so that one can use `.` in a file/path name.
 
+- [Variadic functions](#variadic-functions)
+
 - [Tracing facility](#tracing-facility) to debug your programs.
 
 - [Macros](#macros) are expanded at compilation time
@@ -662,10 +664,10 @@ goal> pi x\ sigma Y\ even x => (declare_constraint (even Y) [Y], Y = x).
 Success:
 ```
 
-The `declare_constraint` built in is typically used in conjunction with `mode`
-as follows:
+The `declare_constraint` built requires functions, and is typically
+used as follows:
 ```prolog
-mode (even i).
+func even int -> .
 even (uvar as X) :- !, declare_constraint (even X) [X].
 even 0.
 even X :- X > 1, Y is X - 2, even Y.
@@ -751,8 +753,8 @@ It is used only in debug output.
 
 #### Example
 ```prolog
-mode (odd i).
-mode (even i).
+func odd int -> .
+func even int -> .
 
 even (uvar as X) :- !, declare_constraint (even X) [X].
 odd  (uvar as X) :- !, declare_constraint (odd X)  [X].
@@ -801,7 +803,7 @@ we can compute GCDs of 2 sets of numbers: 99, 66 and 22 named X;
 14 and 77 called Y.
 
 ```prolog
-mode (gcd i i).
+func gcd int ,int -> .
 
 gcd A (uvar as Group) :- declare_constraint (gcd A Group) Group.
 
@@ -825,7 +827,7 @@ Constraints are resumed as regular delayed goals are.
 #### Example of higher order rules
 
 ```prolog
-mode (term i o).
+func term tm -> ty.
 term (app HD ARG) TGT :- term HD (arrow SRC TGT), term ARG SRC.
 term (lam F) (arrow SRC TGT) :- pi x\ term x SRC => term (F x) TGT.
 term (uvar as X) T :- declare_constraint (term X T) [X].
@@ -1033,6 +1035,21 @@ Here `main` calls `std.list.map`, `std.string.concat` and finally
 Elpi accepts `accumulate "path".` (i.e. a string rather than an indent)
 so that one can use `.` in a file or path name.
 
+## Variadic functions
+
+Functions, both external and written in Elpi, can be variadic.
+
+```prolog
+func f int, int -> int.. .
+f N D Q   :- Q is N div D.
+f N D Q R :- f N D Q, R is N mod D.
+```
+
+Here `f` takes 3 or 4 argument: when 4 are passed it also returns the
+reminder of the division. Only the last output can be variadic.
+
+This feature is mainly used for external functions.
+
 ## Tracing facility
 
 Elpi comes with a tracing facility.  The feature was designed to debug

dune-project

@@ -1,3 +1,3 @@
-(lang dune 2.8)
+(lang dune 2.9)
 (name elpi)
 (using menhir 2.0)

elpi.opam

@@ -10,20 +10,22 @@ bug-reports: "https://github.com/LPCIC/elpi/issues"
 build: [
   ["dune" "subst"] {dev}
   ["dune" "build" "-p" name "-j" jobs]
-  [make "tests" "DUNE_OPTS=-p %{name}%" "SKIP=performance_HO" "SKIP+=performance_FO" "SKIP+=elpi_api_performance"] {with-test & os != "macos" & os-distribution != "alpine" & os-distribution != "freebsd"}
+  [make "tests" "DUNE_OPTS=-p %{name}%" "SKIP=performance_HO" "SKIP+=performance_FO" "SKIP+=elpi_api_performance"] {with-test & os != "macos" & os-distribution != "alpine" & os-distribution != "freebsd"  & arch != "arm32" & arch != "x86_32"}
 ]
 x-maintenance-intent: ["(latest)"]
 depends: [
   "ocaml" {>= "4.13.0" }
   "stdlib-shims"
-  "ppxlib" {>= "0.12.0" & < "0.36.0"}
+  "ppxlib" {>= "0.12.0"}
+  "ppx_optcomp"
   "menhir" {>= "20211230" }
   "re" {>= "1.7.2"}
   "ppx_deriving" {>= "4.3"}
   "ANSITerminal" {with-test}
-  "cmdliner" {with-test}
+  "cmdliner"  {with-test & < "2.0"}
   "fileutils" {with-test}
-  "dune" {>= "2.8.0"}
+  "yojson" {with-test}
+  "dune" {>= "2.9.0"}
   "conf-time" {with-test}
   "atdgen" {>= "2.10.0"}
   "atdts" {>= "2.10.0"}

src/API.ml

@@ -518,7 +518,7 @@ end
 
 module Elpi = struct
 
-  type t = ED.uvar_body
+  type t = ED.uvar
 
   let pp = Compiler.pp_uvar_body
   let show m = Format.asprintf "%a" pp m
@@ -535,7 +535,7 @@ module Elpi = struct
 
   let alloc_Elpi name state =
     let module R = (val !r) in
-    state, (ED.oref ED.dummy)
+    state, (ED.oref ~depth:0 ED.dummy)
 
   let make ?name state =
     match name with
@@ -577,11 +577,11 @@ module RawData = struct
     let module R = (val !r) in let open R in
     match deref_head ~depth t with
     | ED.Term.Arg _ | ED.Term.AppArg _ -> assert false
-    | ED.Term.AppUVar(ub,0,args) -> UnifVar (ub,args)
-    | ED.Term.AppUVar(ub,lvl,args) -> look ~depth (R.expand_appuv ub ~depth ~lvl ~args)
-    | ED.Term.UVar(ub,lvl,ano) -> look ~depth (R.expand_uv ub ~depth ~lvl ~ano)
+    | ED.Term.AppUVar(ub,args) when ub.vardepth == 0 -> UnifVar (ub,args)
+    | ED.Term.AppUVar(ub,args) -> look ~depth (R.expand_appuv ub ~depth ~args)
+    | ED.Term.UVar(ub,ano) -> look ~depth (R.expand_uv ub ~depth ~ano)
     | ED.Term.Discard ->
-        let ub = ED.oref ED.dummy in
+        let ub = ED.oref ~depth:0 ED.dummy in
         UnifVar (ub,R.mkinterval 0 depth 0)
     | ED.Term.Lam _ as t ->
         begin match R.eta_contract_flex ~depth t with
@@ -591,7 +591,7 @@ module RawData = struct
     | x -> Obj.magic x (* HACK: view is a "subtype" of Term.term *)
 
   let kool = function
-    | UnifVar(ub,args) -> ED.Term.AppUVar(ub,0,args)
+    | UnifVar(ub,args) -> ED.Term.AppUVar(ub,args)
     | x -> Obj.magic x
   [@@ inline]
 
@@ -680,7 +680,8 @@ module RawData = struct
   let no_constraints = []
 
   let mkUnifVar ub ~args state =
-    ED.Term.mkAppUVar ub 0 args
+    if args = [] then ED.Term.mkUVar ub 0
+    else ED.Term.mkAppUVar ub args
 
   type Conversion.extra_goal +=
   | RawGoal = ED.Conversion.RawGoal
@@ -905,7 +906,7 @@ module BuiltInPredicate = struct
 
   let beta ~depth t args =
     let module R = (val !r) in let open R in
-    deref_appuv ~from:depth ~to_:depth ?avoid:None args t
+    deref_apparg ~from:depth ~to_:depth ?avoid:None t args
 
   module HOAdaptors = struct
 
@@ -915,7 +916,7 @@ module BuiltInPredicate = struct
     type ('a,'b,'c) pred3 = Data.term * 'a Conversion.t * 'b Conversion.t * 'c Conversion.t
     type ('a,'b) pred3a = Data.term * 'a Conversion.t * 'b Conversion.t
 
-    let pred1_ty x = Conversion.TyApp("->",x.Conversion.ty,[Conversion.TyName"prop"])
+    let pred1_ty x = Conversion.TyApp("->",x.Conversion.ty,[Conversion.TyName"(func)"])
     let pred1 x = { Conversion.ty = pred1_ty x; readback = (fun ~depth state e -> state,(e,x),[]); embed = (fun ~depth state (x,_) -> state,x,[]); pp = (fun fmt (x,_) -> Format.fprintf fmt "<pred1>"); pp_doc = (fun fmt () -> ()) }
     let pred2_ty x y = Conversion.(TyApp("->",x.Conversion.ty,[TyApp("->",y.Conversion.ty,[Conversion.TyName"prop"])]))
     let pred2 x y = { Conversion.ty = pred2_ty x y; readback = (fun ~depth state e -> state,(e,x,y),[]); embed = (fun ~depth state (x,_,_) -> state,x,[]); pp = (fun fmt (x,_,_) -> Format.fprintf fmt "<pred2>"); pp_doc = (fun fmt () -> ()) }

src/API.mli

@@ -1170,8 +1170,8 @@ module RawData : sig
     | UnifVar of FlexibleData.Elpi.t * term list
 
   (** Terms must be inspected after dereferencing their head.
-      If the resulting term is UVar then its uvar_body is such that
-      get_assignment uvar_body = None *)
+      If the resulting term is UVar then its uvar is such that
+      get_assignment uvar = None *)
   val look : depth:int -> term -> view
 
   (* to reuse a term that was looked at *)