Merge pull request #257

abbreviations for tactic in terms

.github/workflows/main.yml

@@ -18,7 +18,8 @@ jobs:
         coq_version:
           - '8.13'
         ocaml_version:
-          - 'minimal'
+          - '4.07-flambda'
+          - '4.11-flambda'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1

Changelog.md

@@ -1,5 +1,32 @@
 # Changelog
 
+## [1.11.0] - 30-06-2021
+
+Requires Elpi 1.13.6 and Coq 8.13.
+
+### HOAS
+- New node `proj` of type `projection -> int -> primitive-value` holding the
+  projection name (a Coq detail) and the number of the field it projects (0
+  based), eg: `primitive (proj _ N)` stands for the projection for the Nth
+  constructor field counting parameters.
+- Change `cs-instance` carries a `gref`
+
+### API
+- New `coq.notation.add-abbreviation-for-tactic` to add a parsing rule
+  for a tactic-in-term, along the lines of
+    `Notation foo := ltac:(elpi mytactic arguments)`
+  but passing `mytactic` the correct `elpi.loc` of invocation.
+- New `@pplevel!` attribute to control outermost parentheses in `coq.term->pp`
+  and similar
+- New `coq.hints.add-mode` like the `Hint Mode` vernacular
+- New `coq.hints.modes`
+- New `coq.TC.declare-class`
+- Deprecate `coq.env.const-opaque?` -> `coq.env.opaque?`
+- Deprecate `coq.env.const-primitive?` -> `coq.env.primitive?`
+- Deprecate `coq.CS.canonical-projections` -> `coq.env.projections`
+- New `coq.env.primitive-projections`
+- Change `coq.warning` emits the same warning only once
+
 ## [1.10.3] - 18-06-2021
 
 Requires Elpi 1.13.6 and Coq 8.13.

README.md

@@ -214,8 +214,11 @@ where:
   is how you invoke a tactic.
 
 - `Elpi Export <qname>` makes it possible to invoke command `<qname>` without
-  the `Elpi` prefix. Exporting tactics is not supported, but one can define
-  a `Tactic Notation` to give the tactic a better syntax and a shorter name.
+  the `Elpi` prefix or invoke tactic `<qname>` in the middle of a term just
+  writing `<qname> args` instead of `ltac:(elpi <qname> args)`. Note that in
+  the case of tactics, all arguments are considered to be terms.
+  Moreover, remember that one can use `Tactic Notation` to give the tactic a
+  better syntax and a shorter name when used in the middle of a proof script.
 
 where `<argument>` can be:
 

_CoqProject

@@ -1,4 +1,4 @@
--arg -w -arg +elpi.add-const-for-axiom-or-sectionvar
+-arg -w -arg +elpi.deprecated
 
 -R theories elpi
 -Q examples elpi.examples
@@ -32,9 +32,11 @@ src/coq_elpi_glob_quotation.ml
 src/coq_elpi_glob_quotation.mli
 src/coq_elpi_arg_HOAS.ml
 src/coq_elpi_arg_HOAS.mli
+src/coq_elpi_arg_syntax.mlg
 src/coq_elpi_builtins_HOAS.ml
 src/coq_elpi_builtins.ml
 src/coq_elpi_builtins.mli
 src/coq_elpi_config.ml
 
 src/elpi_plugin.mlpack
+

_CoqProject.test

@@ -1,3 +1,5 @@
+-arg -w -arg +elpi.deprecated
+
 -Q theories elpi
 -Q examples elpi.examples
 -Q tests    elpi.tests

apps/derive/tests/test_lens.v

@@ -21,7 +21,7 @@ Check @_pf4 : forall A, Lens (pr_record A) (pr_record A) A A.
 Goal forall A x, x = @_pf3 A.
 intros; unfold _pf3.
 match goal with
-| |- x = {| over := fun f r => {| pf3 := f (pf3 A r); pf4 := pf4 A r |} ;
+| |- x = {| over := fun f r => {| pf3 := f (_ r); pf4 := _ r |} ;
             view := _ |}
     => idtac "ok"
 | |- _ => fail "not primitive"

coq-builtin.elpi

@@ -42,6 +42,7 @@ pred attributes o:list attribute.
 %   solve <goal> <new goals>
 % Where [str "foo", int 3, trm (app[f,x])] is part of <goal>.
 % The encoding of goals is described below.
+% msolve is for tactics that operate on multiple goals (called via all: ).
 pred solve i:goal, o:list sealed-goal.
 pred msolve i:list sealed-goal, o:list sealed-goal.
 
@@ -85,9 +86,6 @@ type app   list term -> term.                   % app [hd|args]
 type match term -> term -> list term -> term.   % match t p [branch])
 type fix   name -> int -> term -> (term -> term) -> term. % fix name rno ty bo
 
-kind primitive-value type.
-type uint63 uint63 -> primitive-value.
-type float64 float64 -> primitive-value.
 type primitive primitive-value -> term.
 
 
@@ -323,6 +321,22 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % Ltac1 code on that term (e.g. to call vm_compute, see also the example
 % on the reflexive tactic).
 
+% ----- Multi goals tactics. ----
+% Coq provides goal selectors, such as all:, to pass to a tactic more than one
+% goal. In order to write such a tactic, Coq-Elpi provides another entry point
+% called msolve. To be precise, if there are two goals under focus, say <g1> and
+% <g2>, then all: elpi tac <t> runs the following query
+%
+%   msolve [<g1>,<g2>] NewGoals ;                         % note the disjunction
+%   coq.ltac.all (coq.ltac.open solve) [<g1>,<g2>] NewGoals
+%
+% So, if msolve has no clause, Coq-Elpi will use solve on all the goals
+% independently. If msolve has a cluse, then it can manipulate the entire list
+% of sealed goals. Note that the argument <t> is in both <g1> and <g2> but
+% it is interpreted in both contexts independently. If both goals have a proof
+% variable named "x" then passing (@eq_refl _ x) as <t> equips both goals with
+% a (raw) proof that "x = x", no matter what their type is.
+
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Declarations for Coq's API (environment read/write access, etc).
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -341,6 +355,7 @@ macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
 macro @ppall! :- get-option "coq:pp" "all". % printing all
 macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
+macro @pplevel! N :- get-option "coq:pplevel" N. % printing precedence (for parentheses)
 
 macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute
 
@@ -569,8 +584,8 @@ external pred coq.env.record? i:inductive, o:bool.
 % [coq.env.recursive? Ind] checks if Ind is recursive
 external pred coq.env.recursive? i:inductive.
 
-% [coq.env.const-opaque? GR] checks if GR is an opaque constant
-external pred coq.env.const-opaque? i:constant.
+% [coq.env.opaque? GR] checks if GR is an opaque constant
+external pred coq.env.opaque? i:constant.
 
 % [coq.env.const GR Bo Ty] reads the type Ty and the body Bo of constant GR.
 % Opaque constants have Bo = none.
@@ -580,9 +595,9 @@ external pred coq.env.const i:constant, o:option term, o:term.
 % opaque. If such body is none, then the constant is a true axiom
 external pred coq.env.const-body i:constant, o:option term.
 
-% [coq.env.const-primitive? GR] tests if GR is a primitive constant (like
-% uin63 addition)
-external pred coq.env.const-primitive? i:constant.
+% [coq.env.primitive? GR] tests if GR is a primitive constant (like uin63
+% addition)
+external pred coq.env.primitive? i:constant.
 
 % [coq.locate-module ModName ModPath] locates a module.  It's a fatal error
 % if ModName cannot be located. *E*
@@ -607,6 +622,20 @@ external pred coq.env.section o:list constant.
 % [coq.env.current-path Path] lists the current module path
 external pred coq.env.current-path o:list string.
 
+% Deprecated, use coq.env.opaque?
+  pred coq.env.const-opaque? i:constant.
+  coq.env.const-opaque? C :-
+    coq.warning "elpi.deprecated" "elpi.const-opaque" "use coq.env.opaque? in place of coq.env.const-opaque?",
+    coq.env.opaque? C.
+
+
+% Deprecated, use coq.env.primitive?
+  pred coq.env.const-primitive? i:constant.
+  coq.env.const-primitive? C :-
+    coq.warning "elpi.deprecated" "elpi.const-primitive" "use coq.env.primitive? in place of coq.env.const-primitive?",
+    coq.env.primitive? C.
+
+
 % -- Environment: write -----------------------------------------------
 
 % Note: universe constraints are taken from ELPI's constraints store. Use
@@ -697,6 +726,15 @@ external pred coq.env.begin-section i:id.
 % [coq.env.end-section] end the current section *E*
 external pred coq.env.end-section .
 
+% [coq.env.projections StructureName Projections] given a record
+% StructureName lists all projections
+external pred coq.env.projections i:inductive, o:list (option constant).
+
+% [coq.env.primitive-projections StructureName Projections] given a record
+% StructureName lists all primitive projections
+external pred coq.env.primitive-projections i:inductive, 
+                                            o:list (option (pair projection int)).
+
 % -- Universes --------------------------------------------------------
 
 % Univ.Universe.t
@@ -743,6 +781,16 @@ typeabbrev uint63 (ctype "uint63").
 typeabbrev float64 (ctype "float64").
 
 
+typeabbrev projection (ctype "projection").
+
+
+% Primitive values
+kind primitive-value type.
+type uint63 uint63 -> primitive-value. % unsigned integers over 63 bits
+type float64 float64 ->
+             primitive-value. % double precision foalting points
+type proj projection -> int -> primitive-value. % primitive projection
+
 
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for extra logical objects
@@ -759,7 +807,7 @@ type cs-sort universe -> cs-pattern.
 
 % Canonical Structure instances: (cs-instance Proj ValPat Inst)
 kind cs-instance type.
-type cs-instance gref -> cs-pattern -> term -> cs-instance.
+type cs-instance gref -> cs-pattern -> gref -> cs-instance.
 
 % [coq.CS.declare-instance GR] Declares GR as a canonical structure
 % instance.
@@ -774,10 +822,8 @@ external pred coq.CS.db o:list cs-instance.
 % or canonical Value, or both
 external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance.
 
-% [coq.CS.canonical-projections StructureName Projections] given a record
-% StructureName lists all projections
-external pred coq.CS.canonical-projections i:inductive, 
-                                           o:list (option constant).
+% [coq.TC.declare-class GR] Declare GR as a type class
+external pred coq.TC.declare-class i:gref.
 
 % Type class instance with priority
 kind tc-instance type.
@@ -824,6 +870,31 @@ external pred coq.coercion.db o:list coercion.
 external pred coq.coercion.db-for i:class, i:class, 
                                   o:list (pair gref int).
 
+% Deprecated, use coq.env.projections
+pred coq.CS.canonical-projections i:inductive, o:list (option constant).
+coq.CS.canonical-projections I L :-
+  coq.warning "elpi.deprecated" "elpi.canonical-projections" "use coq.env.projections in place of coq.CS.canonical-projections",
+  coq.env.projections I L.
+
+
+% -- Coq's Hint DB -------------------------------------
+
+% Hint Mode
+kind hint-mode type.
+type mode-ground hint-mode. % No Evar
+type mode-input hint-mode. % No Head Evar
+type mode-output hint-mode. % Anything
+
+% [coq.hints.add-mode GR DB Mode] Adds a mode declaration to DB about
+% GR.
+% Supported attributes:
+% - @local! (default: false)
+external pred coq.hints.add-mode i:gref, i:string, i:list hint-mode.
+
+% [coq.hints.modes GR DB Modes] Gets all the mode declarations in DB about
+% GR
+external pred coq.hints.modes i:gref, i:string, o:list (list hint-mode).
+
 % -- Coq's notational mechanisms -------------------------------------
 
 % Implicit status of an argument
@@ -927,6 +998,22 @@ external pred coq.notation.abbreviation i:abbreviation, i:list term,
 external pred coq.notation.abbreviation-body i:abbreviation, o:int, 
                                              o:term.
 
+% [coq.notation.add-abbreviation-for-tactic Name TacticName FixedArgs]
+% Declares a parsing rule similar to
+%   Notation Name X1..Xn := ltac:(elpi TacticName FixedArgs (X1)..(Xn))
+% so that Name can be used in the middle of a term to invoke an
+% elpi tactic. While FixedArgs can contain str, int, and trm all
+% other arguments will necessarily be terms, and their number is
+% not fixed (the user can pass as many as he likes).
+% The tactic receives as the elpi.loc attribute the precise location
+% at which the term is written (unlike if a regular abbreviation was
+% declared by hand).
+% A call to coq.notation.add-abbreviation-for-tactic TacName TacName []
+% is equivalent to Elpi Export TacName.
+external pred coq.notation.add-abbreviation-for-tactic i:string, 
+                                                       i:string, 
+                                                       i:list argument.
+
 % Generic attribute value
 kind attribute-value type.
 type leaf-str string -> attribute-value.
@@ -1004,14 +1091,14 @@ external pred coq.reduction.native.available? .
 % Deprecated, use coq.reduction.cbv.norm
 pred coq.reduction.cbv.whd_all i:term, o:term.
 coq.reduction.cbv.whd_all T R :-
-  coq.warning "elpi" "deprecated-reduction" "use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all",
+  coq.warning "elpi.deprecated" "elpi.cbv-whd-all" "use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all",
   coq.reduction.cbv.norm T R.
 
 
 % Deprecated, use coq.reduction.vm.norm
 pred coq.reduction.vm.whd_all i:term, i:term, o:term.
 coq.reduction.vm.whd_all T TY R :-
-  coq.warning "elpi" "deprecated-reduction" "use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all",
+  coq.warning "elpi.deprecated" "elpi.vm-whd-all" "use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all",
   coq.reduction.vm.norm T TY R.
 
 
@@ -1103,6 +1190,8 @@ external pred coq.modtypath->path i:modtypath, o:list string.
 % - @ppwidth! N (default 80, max line length)
 % - @ppall! (default: false, prints all details)
 % - @ppmost! (default: false, prints most details)
+% - @pplevel! (default: _, prints parentheses to reach that level, 200 =
+% off)
 % - @holes! (default: false, prints evars as _)
 external pred coq.term->string i:term, o:string.
 
@@ -1111,6 +1200,8 @@ external pred coq.term->string i:term, o:string.
 % Supported attributes:
 % - @ppall! (default: false, prints all details)
 % - @ppmost! (default: false, prints most details)
+% - @pplevel! (default: _, prints parentheses to reach that level, 200 =
+% off)
 % - @holes! (default: false, prints evars as _)
 external pred coq.term->pp i:term, o:coq.pp.
 

coq-elpi.opam

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

elpi/coq-HOAS.elpi

@@ -71,9 +71,6 @@ type app   list term -> term.                   % app [hd|args]
 type match term -> term -> list term -> term.   % match t p [branch])
 type fix   name -> int -> term -> (term -> term) -> term. % fix name rno ty bo
 
-kind primitive-value type.
-type uint63 uint63 -> primitive-value.
-type float64 float64 -> primitive-value.
 type primitive primitive-value -> term.
 
 
@@ -343,6 +340,7 @@ macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
 macro @ppall! :- get-option "coq:pp" "all". % printing all
 macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
+macro @pplevel! N :- get-option "coq:pplevel" N. % printing precedence (for parentheses)
 
 macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute
 

elpi/elpi-reduction.elpi

@@ -34,7 +34,9 @@ whd (fun N T F) [B|C] X XC :- !,
 whd (let N T B F) C X XC :- !,
   (pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B.
 whd (global (const GR)) C X XC :- unfold GR C D DC, !, whd D DC X XC.
-whd (global (const GR) as HD) C X XC :- coq.env.const-primitive? GR, !,
+whd (primitive (proj _ N)) [A|C] X XC :- whd-indc A _ KA, !,
+  whd {proj-red KA N C} X XC.
+whd (global (const GR) as HD) C X XC :- coq.env.primitive? GR, !,
   unwind HD C Orig,
   coq.reduction.lazy.whd_all Orig R,
   if (same_term Orig R) (X = HD, XC = C) (whd R [] X XC).
@@ -61,6 +63,9 @@ match-red GR KArgs BL C X XC :-
   drop Lno KArgs Args,
   nth Ki BL Bi,
   hd-beta {coq.mk-app Bi Args} C X XC.
+pred proj-red i:list term, i:int, i:stack, o:term, o:stack.
+proj-red Args FieldNo C V C :-
+  nth FieldNo Args V.
 
 % iota step
 pred fix-red

examples/example_import_projections.v

@@ -19,7 +19,7 @@ main-import-projections T Ty :-
   std.assert! (coq.env.record? I PrimProjs) "not a record",
   coq.env.indt I _ _ NParams _ _ _,
   std.assert! (std.length Args NParams) "the record is not fully appplied",
-  coq.CS.canonical-projections I Ps, % get the projections generated by Coq
+  coq.env.projections I Ps, % get the projections generated by Coq
   if (PrimProjs = tt)
      (std.forall Ps (declare-abbrev {std.append {coq.mk-n-holes NParams} [T]}))
      (std.forall Ps (declare-abbrev {std.append Args [T]})).
@@ -59,7 +59,8 @@ Check refl_equal _ : p1 = 3. (* check the value of p1 is 3 *)
 End test.
 
 Set Primitive Projections.
-Record r1 (A : Type) := {
+Unset Auto Template Polymorphism.
+Record r1 (A : Type) : Type := {
   f1 : A;
   f2 : nat;
 }.