Adapt to Elpi 2.0

Author: gares

Changelog.md

@@ -1,5 +1,11 @@
 # Development version
 
+### Vernacular
+- `Elpi Accumulate Db Header <db>` to accumulate just the `Db` declaration
+  but no code added after that
+- `Elpi Typecheck` is deprecated and is a no-op since `Elpi Accumulate`
+  performs type checking incrementally
+
 ### Build system
 - Support dune workspace build with `elpi`
 

Makefile

@@ -2,10 +2,12 @@ dune = dune $(1) $(DUNE_$(1)_FLAGS)
 
 all:
 	$(call dune,build)
+	$(call dune,build) builtin-doc
 .PHONY: all
 
 build-core:
 	$(call dune,build) theories
+	$(call dune,build) builtin-doc
 .PHONY: build-core
 
 build-apps:
@@ -14,6 +16,7 @@ build-apps:
 
 build:
 	$(call dune,build) -p coq-elpi @install
+	$(call dune,build) builtin-doc
 .PHONY: build
 
 test-core:

README.md

@@ -183,13 +183,23 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a
   command/tactic with a custom preamble `<code>`.
 - `From some.load.path Extra Dependency <filename> as <fname>`.
-- `Elpi Accumulate [<dbname>|<qname>] [<code>|File <fname>|Db <dbname>]`
+- `Elpi Accumulate [<dbname>|<qname>] [<code>|File <fname>|Db [Header] <dbname>]`
   adds code to the current program (or `<dbname>` or `<qname>` if specified).
   The code can be verbatim, from a file or a Db.
   File names `<fname>` must have been previously declared with the above command.
   It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command
   a no op if the Coq version is matched (or not) by the given regular expression.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
+  Accumulating `Db Header <dbname>`, instead of `Db <dbname>`, accumulates
+  only the first chunk of code associated with Db, typically the type
+  declaration of the predicates that live in the Db. When defining a command
+  or tactic it can be useful to first accumulate the Db header, then some
+  code (possibly calling the predicate living in the Db), and finally
+  accumulating the (full) Db.
+  Note that when a command is executed it may need to be (partially)
+  recompiled, e.g. if the Db was updated. In this case all the code accumulated
+  after the Db (but not after its header) may need to be recompiled. Hence
+  we recommend to accumulate Dbs last.
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)

apps/NES/tests/test_NES_lib.v

@@ -23,7 +23,7 @@ Elpi Command Make.
     nes.end-path,
   ].
 }}.
-Elpi Typecheck.
+
 Elpi Export Make.
 
 Make Cats.And.Dogs.

apps/NES/theories/NES.v

@@ -31,7 +31,7 @@ main _ :-
   coq.say "NES: registered namespaces" NS.
 
 }}.
-Elpi Typecheck.
+
 Elpi Export NES.Status.
 
 Elpi Command NES.Begin.
@@ -45,7 +45,7 @@ Elpi Command NES.Begin.
 
 }}.
 #[interp] Elpi Accumulate lp:{{ main _ :- nes.begin-path. }}.
-Elpi Typecheck.
+
 Elpi Export NES.Begin.
 
 Elpi Command NES.End.
@@ -59,7 +59,7 @@ Elpi Command NES.End.
 
 }}.
 #[interp] Elpi Accumulate lp:{{ main _ :- nes.end-path. }}.
-Elpi Typecheck.
+
 Elpi Export NES.End.
 
 
@@ -74,7 +74,7 @@ Elpi Command NES.Open.
 
 }}.
 #[interp] Elpi Accumulate lp:{{ main _ :- nes.open-path. }}.
-Elpi Typecheck.
+
 Elpi Export NES.Open.
 
 (* List the contents a namespace *)
@@ -93,7 +93,7 @@ Elpi Command NES.List.
   main _ :- coq.error "usage: NES.List <DotSeparatedPath>".
 
 }}.
-Elpi Typecheck.
+
 Elpi Export NES.List.
 
 (* NES.List with types *)
@@ -118,5 +118,5 @@ Elpi Accumulate lp:{{
   main _ :- coq.error "usage: NES.Print <DotSeparatedPath>".
 
 }}.
-Elpi Typecheck.
+
 Elpi Export NES.Print.

apps/coercion/src/coq_elpi_coercion_hook.mlg

@@ -24,23 +24,25 @@ let build_expected_type env sigma expected =
 let return s g t = Some (s,g,t)
 
 let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
-  let loc = API.Ast.Loc.initial "(unknown)" in
   let atts = [] in
   let sigma, expected, retype = build_expected_type env sigma expected in
   let sigma, goal = Evarutil.new_evar env sigma expected in
   let goal_evar, _ = EConstr.destEvar sigma goal in
-  let query ~depth state =
-    let state, (loc, q), gls =
-      Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred])
-        ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
+  let query state =
+    let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in
+    let depth = 0 in
+    let state, q, gls =
+      Coq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[v; inferred]
+        ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth ~base:() state in
     let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in
     let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
-    state, (loc, qatts), gls
+    state, qatts, gls
   in
-  match Interp.get_and_compile program with
+  let loc = Loc.initial Loc.ToplevelInput in
+  match Interp.get_and_compile ~loc program with
   | None -> None
   | Some (cprogram, _) ->
-    match Interp.run ~static_check:false cprogram (`Fun query) with
+    match Interp.run ~loc cprogram (Fun (query)) with
     | API.Execute.Success solution ->
       let gls = Evar.Set.singleton goal_evar in
       let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in

apps/coercion/theories/coercion.v

@@ -15,11 +15,12 @@ pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
 }}.
 
 Elpi Tactic coercion.
+Elpi Accumulate Db Header coercion.db.
 Elpi Accumulate lp:{{
 
 solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol.
 
 }}.
 Elpi Accumulate Db coercion.db.
-Elpi Typecheck.
+
 Elpi CoercionFallbackTactic coercion.

apps/cs/src/coq_elpi_cs_hook.mlg

@@ -8,27 +8,29 @@ open Coq_elpi_arg_syntax
 open Coq_elpi_vernacular
 
 let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
-	  let loc = API.Ast.Loc.initial "(unknown)" in
 	  let atts = [] in
      let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list args2 Reductionops.Stack.empty) in
      let sigma, (goal_ty, _) = Evarutil.new_type_evar env sigma Evd.UnivRigid in
 	  let sigma, goal = Evarutil.new_evar env sigma goal_ty in
 	  let goal_evar, _ = EConstr.destEvar sigma goal in
     let nparams = Structures.Structure.projection_nparams proji in
-	  let query ~depth state =
-		 let state, (loc, q), gls =
+	  let query state =
+         let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in
+		 let state, q, gls =
       let lhs = match params1 with
         | Some params1 -> EConstr.mkApp (EConstr.mkConstU (proji, u), Array.of_list params1)
         | None -> EConstr.mkConstU (proji, u) in
-			Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [lhs; rhs])
-			  ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
-		 let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in
+			Coq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[lhs; rhs]
+			  ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth:0 ~base:() state in
+		 let state, qatts = atts2impl loc Summary.Stage.Interp ~depth:0 state atts q in
 		 let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
-		 state, (loc, qatts), gls
-	  in match Interp.get_and_compile program with
+		 state, qatts, gls
+	  in
+	  let loc = Loc.initial Loc.ToplevelInput in
+      match Interp.get_and_compile ~loc program with
 	  | None -> None
 	  | Some (cprogram, _) ->
-		 begin match Interp.run ~static_check:false cprogram (`Fun query) with
+		 begin match Interp.run ~loc cprogram (Fun query) with
 		 | API.Execute.Success solution ->
 			let gls = Evar.Set.singleton goal_evar in
 			let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in

apps/cs/theories/cs.v

@@ -24,5 +24,4 @@ solve (goal Ctx _ _Ty Sol [trm Proj, trm Rhs]) _ :-
   true.
 
 }}.
-Elpi Typecheck canonical_solution.
 Elpi CS canonical_solution.

apps/derive/README.md

@@ -525,7 +525,7 @@ Elpi Accumulate lp:{{
   pred usage.
   usage :- coq.error "Usage: derive.myder <object name>".
 }}. 
-Elpi Typecheck.
+
 ```
 
 This is enough to run the derivation via something like