diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index dad8d2f31..0bbffe49f 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/Changelog.md b/Changelog.md index d171f4e9d..28d728054 100644 --- a/Changelog.md +++ b/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. diff --git a/README.md b/README.md index f90e56c3e..5da06828d 100644 --- a/README.md +++ b/README.md @@ -214,8 +214,11 @@ where: is how you invoke a tactic. - `Elpi Export ` makes it possible to invoke command `` 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 `` in the middle of a term just + writing ` args` instead of `ltac:(elpi 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 `` can be: diff --git a/_CoqProject b/_CoqProject index 6dff4c0e8..e92d66812 100644 --- a/_CoqProject +++ b/_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 + diff --git a/_CoqProject.test b/_CoqProject.test index 84c236c41..0ffafbc79 100644 --- a/_CoqProject.test +++ b/_CoqProject.test @@ -1,3 +1,5 @@ +-arg -w -arg +elpi.deprecated + -Q theories elpi -Q examples elpi.examples -Q tests elpi.tests diff --git a/apps/derive/tests/test_lens.v b/apps/derive/tests/test_lens.v index 7526dde4b..bf7da076c 100644 --- a/apps/derive/tests/test_lens.v +++ b/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" diff --git a/coq-builtin.elpi b/coq-builtin.elpi index b19a39b73..ee89c8673 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -42,6 +42,7 @@ pred attributes o:list attribute. % solve % Where [str "foo", int 3, trm (app[f,x])] is part of . % 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 and +% , then all: elpi tac runs the following query +% +% msolve [,] NewGoals ; % note the disjunction +% coq.ltac.all (coq.ltac.open solve) [,] 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 is in both and but +% it is interpreted in both contexts independently. If both goals have a proof +% variable named "x" then passing (@eq_refl _ x) as 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. diff --git a/coq-elpi.opam b/coq-elpi.opam index 61f929d40..e277b92b2 100644 --- a/coq-elpi.opam +++ b/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~" } ] diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 05c6ba854..02947f7ea 100644 --- a/elpi/coq-HOAS.elpi +++ b/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 diff --git a/elpi/elpi-reduction.elpi b/elpi/elpi-reduction.elpi index 099176a5a..7f5485741 100644 --- a/elpi/elpi-reduction.elpi +++ b/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 diff --git a/examples/example_import_projections.v b/examples/example_import_projections.v index 86a5f9273..5f44e339f 100644 --- a/examples/example_import_projections.v +++ b/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; }. diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index f0a465b8a..64e192b3b 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -145,7 +145,7 @@ expand-spine (info _ GR NGR _ _ _) X Y AccL AccR Premises Clause :- pred expand i:inductive, i:gref, i:gref, i:term, o:term, o:prop. expand R GR NGR X Y Clause :- std.assert! (coq.env.indt R tt 0 0 _ [K] [KTY]) "record is too complex for this example", - coq.CS.canonical-projections R Projs, + coq.env.projections R Projs, expand-spine (info R GR NGR Projs K KTY) X Y [] [] [] Clause. % This simply dispatches between global references ---------------------------- diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 71a847daf..bd5955bad 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -82,6 +82,7 @@ type options = { failsafe : bool; (* don't fail, e.g. we are trying to print a term *) ppwidth : int; pp : ppoption; + pplevel : Constrexpr.entry_relative_level; using : string option; } @@ -93,6 +94,7 @@ let default_options = { failsafe = false; ppwidth = 80; pp = Normal; + pplevel = Constrexpr.LevelSome; using = None; } @@ -381,16 +383,38 @@ let in_elpi_fix name rno ty bo = E.mkApp fixc (in_elpi_name name) [CD.of_int rno; ty; E.mkLam bo] let primitivec = E.Constants.declare_global_symbol "primitive" -let uint63c = E.Constants.declare_global_symbol "uint63" -let float64c = E.Constants.declare_global_symbol "float64" -let in_elpi_uint63 ~depth state i = - let state, i, _ = Coq_elpi_utils.uint63.API.Conversion.embed ~depth state i in - state, E.mkApp primitivec (E.mkApp uint63c i []) [] +type primitive_value = + | Uint63 of Uint63.t + | Float64 of Float64.t + | Projection of Projection.t -let in_elpi_float64 ~depth state f = - let state, f, _ = Coq_elpi_utils.float64.API.Conversion.embed ~depth state f in - state, E.mkApp primitivec (E.mkApp float64c f []) [] +let primitive_value : primitive_value API.Conversion.t = + let module B = Coq_elpi_utils in + let open API.AlgebraicData in declare { + ty = API.Conversion.TyName "primitive-value"; + doc = "Primitive values"; + pp = (fun fmt -> function + | Uint63 i -> Format.fprintf fmt "Type" + | Float64 f -> Format.fprintf fmt "Set" + | Projection p -> Format.fprintf fmt ""); + constructors = [ + K("uint63","unsigned integers over 63 bits",A(B.uint63,N), + B (fun x -> Uint63 x), + M (fun ~ok ~ko -> function Uint63 x -> ok x | _ -> ko ())); + 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("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 ())); + ] +} |> API.ContextualConversion.(!<) + +let in_elpi_primitive ~depth state i = + let state, i, _ = primitive_value.API.Conversion.embed ~depth state i in + state, E.mkApp primitivec i [] + (* ********************************* }}} ********************************** *) @@ -673,6 +697,7 @@ let get_options ~depth hyps state = else if s = Some "most" then Most else Normal in let ppwidth = function Some i -> i | None -> 80 in + let pplevel = function None -> Constrexpr.LevelSome | Some i -> Constrexpr.LevelLe i in let get_pair_option fst snd name = try let t, depth = API.Data.StrMap.find name map in @@ -698,6 +723,7 @@ let get_options ~depth hyps state = failsafe = false; ppwidth = ppwidth @@ get_int_option "coq:ppwidth"; pp = pp @@ get_string_option "coq:pp"; + pplevel = pplevel @@ get_int_option "coq:pplevel"; using = get_string_option "coq:using"; } @@ -887,12 +913,13 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t = let state, bo = aux ~depth:(depth+1) env state bo in state, in_elpi_fix name.Context.binder_name rarg typ bo | C.Proj(p,t) -> - let t = Retyping.expand_projection env sigma p t [] in - aux ~depth env state t + let state, t = aux ~depth env state t in + let state, p = in_elpi_primitive ~depth state (Projection p) in + state, in_elpi_app ~depth p [|t|] | C.Fix _ -> nYI "HOAS for mutual fix" | C.CoFix _ -> nYI "HOAS for cofix" - | C.Int i -> in_elpi_uint63 ~depth state i - | C.Float f -> in_elpi_float64 ~depth state f + | C.Int i -> in_elpi_primitive ~depth state (Uint63 i) + | C.Float f -> in_elpi_primitive ~depth state (Float64 f) | C.Array _ -> nYI "HOAS for persistent arrays" in if debug () then @@ -1225,13 +1252,26 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals err Pp.(str"wrong constant:" ++ str (E.Constants.show n)) (* app *) - | E.App(c,x,[]) when appc == c -> - (match U.lp_list_to_list ~depth x with - | x :: xs -> - let state, x, gl1 = aux ~depth state x in - let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in - state, EC.mkApp (x, Array.of_list xs), gl1 @ gl2 - | _ -> assert false) (* TODO *) + | E.App(c,x,[]) when appc == c -> begin + match U.lp_list_to_list ~depth x with + | x :: xs -> begin + match E.look ~depth x, xs with + | E.App(c,p,[]), i :: xs when primitivec == c -> + let state, p, gls = primitive_value.API.Conversion.readback ~depth state p in + begin match p with + | Projection p -> + let state, i, gl1 = aux ~depth state i in + let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in + state, EC.mkApp (EC.mkProj (p,i),Array.of_list xs), gls @ gl1 @ gl2 + | _ -> err Pp.(str"not a primitive projection:" ++ str (E.Constants.show c)) + end + | x, _ -> + let state, x, gl1 = aux ~depth state (E.kool x) in + let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in + state, EC.mkApp (x, Array.of_list xs), gl1 @ gl2 + end + | _ -> assert false (* TODO *) + end (* match *) | E.App(c,t,[rt;bs]) when matchc == c -> @@ -1285,16 +1325,13 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals | _ -> err Pp.(str"Not an int: " ++ str (P.Debug.show_term rno)) in state, EC.mkFix (([|rno|],0),([|name|],[|ty|],[|bo|])), gl1 @ gl2 - | E.App(c,v,[]) when primitivec == c -> begin - match E.look ~depth v with - | E.App(c,i,[]) when uint63c == c -> - let state, i, gls = Coq_elpi_utils.uint63.API.Conversion.readback ~depth state i in - state, EC.mkInt i, gls - | E.App(c,f,[]) when float64c == c -> - let state, f, gls = Coq_elpi_utils.float64.API.Conversion.readback ~depth state f in - state, EC.mkFloat f, gls - | _ -> err Pp.(str"Not a HOAS primitive value:" ++ str (P.Debug.show_term t)) - end + | E.App(c,v,[]) when primitivec == c -> + let state, v, gls = primitive_value.API.Conversion.readback ~depth state v in + begin match v with + | Uint63 i -> state, EC.mkInt i, gls + | Float64 f -> state, EC.mkFloat f, gls + | Projection p -> state, EC.mkConst (Names.Projection.constant p), gls + end (* evar *) | E.UnifVar (elpi_evk,args) as x -> @@ -1743,19 +1780,26 @@ let reachable sigma roots acc = prlist_with_sep spc Evar.print (Evar.Set.elements res)); res -let tclSOLUTION2EVD { API.Data.constraints; assignments; state; pp_ctx } = +let tclSOLUTION2EVD sigma0 { API.Data.constraints; assignments; state; pp_ctx } = let open Proofview.Unsafe in - let open Proofview.Notations in let open Tacticals.New in - tclGETGOALS >>= fun gls -> + let open Proofview.Notations in + tclGETGOALS >>= fun gls -> let gls = gls |> List.map Proofview.drop_state in let roots = List.fold_right Evar.Set.add gls Evar.Set.empty in let state, solved_goals, _, _gls = elpi_solution_to_coq_solution constraints state in - let all_goals = reachable (get_sigma state) roots Evar.Set.empty in + let sigma = get_sigma state in + let all_goals = reachable sigma roots Evar.Set.empty in let declared_goals, shelved_goals = get_declared_goals (Evar.Set.diff all_goals solved_goals) constraints state assignments pp_ctx in + if debug () then Feedback.msg_debug Pp.(str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals); + if debug () then Feedback.msg_debug Pp.(str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals); + let sigma = Evd.fold_undefined (fun k _ sigma -> + if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma + else Evd.remove sigma k + ) sigma sigma in tclTHENLIST [ - tclEVARS (S.get engine state).sigma; + tclEVARS sigma; tclSETGOALS @@ List.map Proofview.with_empty_state declared_goals; Proofview.shelve_goals shelved_goals ] diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index d4f20bbce..fc562b962 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -24,6 +24,7 @@ type options = { failsafe : bool; (* readback is resilient to illformed terms *) ppwidth : int; pp : ppoption; + pplevel : Constrexpr.entry_relative_level; using : string option; } @@ -121,8 +122,7 @@ val in_elpi_let : Name.t -> term -> term -> term -> term val in_elpi_appl : depth:int -> term -> term list -> term val in_elpi_match : term -> term -> term list -> term val in_elpi_fix : Name.t -> int -> term -> term -> term -val in_elpi_uint63 : depth:int -> state -> Uint63.t -> state * term -val in_elpi_float64 : depth:int -> state -> Float64.t -> state * term + val in_elpi_name : Name.t -> term @@ -145,6 +145,12 @@ val global_constant_of_globref : Names.GlobRef.t -> global_constant val abbreviation : Globnames.syndef_name Conversion.t val implicit_kind : Glob_term.binding_kind Conversion.t val collect_term_variables : depth:int -> term -> Names.Id.t list +type primitive_value = + | Uint63 of Uint63.t + | Float64 of Float64.t + | Projection of Projection.t +val primitive_value : primitive_value Conversion.t +val in_elpi_primitive : depth:int -> state -> primitive_value -> state * term module GRMap : Elpi.API.Utils.Map.S with type key = Names.GlobRef.t module GRSet : Elpi.API.Utils.Set.S with type elt = Names.GlobRef.t @@ -208,6 +214,6 @@ val goals2query : Evd.evar_map -> Goal.goal list -> Elpi.API.Ast.Loc.t -> main:'a tactic_main -> in_elpi_arg:(depth:int -> ?calldepth:int -> 'b coq_context -> hyp list -> Evd.evar_map -> State.t -> 'a -> State.t * term list * Conversion.extra_goals) -> depth:int -> State.t -> State.t * (Elpi.API.Ast.Loc.t * term) -val tclSOLUTION2EVD : 'a Elpi.API.Data.solution -> unit Proofview.tactic +val tclSOLUTION2EVD : Evd.evar_map -> 'a Elpi.API.Data.solution -> unit Proofview.tactic val show_engine : State.t -> string diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 9b3fea423..eb9698aeb 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -107,7 +107,7 @@ type ('a,'b,'c,'d,'e,'f,_) arg = | Context : 'e -> ('a,'b,'c,'d,'e,'f,cmd) arg type 'a raw_arg = (raw_term, raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_ltac_arg,'a) arg -type 'a glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,glob_ltac_arg,'a) arg +type ('a,'b) glob_arg = ('b, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr,'a) arg type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,cmd) arg type top_tac_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,tac) arg @@ -342,7 +342,14 @@ let subst_tac_arg mod_subst = function Term (Ltac_plugin.Tacsubst.subst_glob_constr_and_expr mod_subst t) | LTac(ty,t) -> LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t)) - +let subst_tac_arg_glob mod_subst = function + | Int _ as x -> x + | String _ as x -> x + | Term t -> + Term (Detyping.subst_glob_constr (Global.env()) mod_subst t) + | LTac(ty,t) -> + LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t)) + let interp_arg ist evd = function | Int _ as x -> evd.Evd.sigma, x | String _ as x -> evd.Evd.sigma, x diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli index bfe3aa660..b0335d1ea 100644 --- a/src/coq_elpi_arg_HOAS.mli +++ b/src/coq_elpi_arg_HOAS.mli @@ -82,19 +82,21 @@ type ('a,'b,'c,'d,'e,'f,_) arg = | Context : 'e -> ('a,'b,'c,'d,'e,'f,cmd) arg type 'a raw_arg = (raw_term, raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_term,'a) arg -type 'a glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr,'a) arg +type ('a,'b) glob_arg = ('b, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr,'a) arg type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,cmd) arg type top_tac_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,tac) arg val pp_raw_arg : Environ.env -> Evd.evar_map -> cmd raw_arg -> Pp.t -val pp_glob_arg : Environ.env -> Evd.evar_map -> cmd glob_arg -> Pp.t +val pp_glob_arg : Environ.env -> Evd.evar_map -> (cmd,glob_term) glob_arg -> Pp.t val pp_top_arg : Environ.env -> Evd.evar_map -> top_arg -> Pp.t -val glob_arg : Genintern.glob_sign -> cmd raw_arg -> cmd glob_arg -val interp_arg : Geninterp.interp_sign -> 'g Evd.sigma -> cmd glob_arg -> Evd.evar_map * top_arg -val subst_arg : Mod_subst.substitution -> cmd glob_arg -> cmd glob_arg +val glob_arg : Genintern.glob_sign -> cmd raw_arg -> (cmd,glob_term) glob_arg +val interp_arg : Geninterp.interp_sign -> 'g Evd.sigma -> (cmd,glob_term) glob_arg -> Evd.evar_map * top_arg +val subst_arg : Mod_subst.substitution -> (cmd,glob_term) glob_arg -> (cmd,glob_term) glob_arg -val wit_elpi_ftactic_arg : (tac raw_arg, tac glob_arg, top_tac_arg) Genarg.genarg_type +val subst_tac_arg_glob : Mod_subst.substitution -> (tac,Glob_term.glob_constr) glob_arg -> (tac,Glob_term.glob_constr) glob_arg + +val wit_elpi_ftactic_arg : (tac raw_arg, (tac,glob_term) glob_arg, top_tac_arg) Genarg.genarg_type (* for tactics *) val in_elpi_tac_arg : diff --git a/src/coq_elpi_arg_syntax.ml b/src/coq_elpi_arg_syntax.ml new file mode 100644 index 000000000..b887e2aaa --- /dev/null +++ b/src/coq_elpi_arg_syntax.ml @@ -0,0 +1,944 @@ +let __coq_plugin_name = "elpi_plugin" +let _ = Mltop.add_known_module __coq_plugin_name + +# 7 "src/coq_elpi_arg_syntax.mlg" + + +open Ltac_plugin + +open Pcoq.Constr +open Pcoq.Prim + +module EA = Coq_elpi_arg_HOAS +module U = Coq_elpi_utils + +(* Arguments ************************************************************* *) +let pr_elpi_string _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) + +let trim_loc loc = + let open Loc in + { loc with bp = loc.bp + 1; ep = loc.ep - 1 } + +let idents_of loc s = + let s = String.sub s 1 (String.length s - 2) in + let l = Str.(split (regexp "[\t \n]+") s) in + List.iter (fun x -> if not (CLexer.is_ident x) then raise Stream.Failure) l; + Coq_elpi_utils.of_coq_loc (trim_loc loc), l + +let rec strip_curly loc s = + if s.[0] = '\123' then strip_curly (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_round loc s = + if s.[0] = '(' then strip_round (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_square loc s = + if s.[0] = '[' then strip_square (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s + + + +let (wit_elpi_string, elpi_string) = Tacentries.argument_extend ~name:"elpi_string" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "xxxxxxxx")))) + (fun _ loc -> + +# 43 "src/coq_elpi_arg_syntax.mlg" + (Elpi.API.Ast.Loc.initial "dummy", "") + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 42 "src/coq_elpi_arg_syntax.mlg" + pr_elpi_string + ), (fun env sigma -> + +# 42 "src/coq_elpi_arg_syntax.mlg" + pr_elpi_string + ), (fun env sigma -> + +# 42 "src/coq_elpi_arg_syntax.mlg" + pr_elpi_string + )); + } +let _ = (wit_elpi_string, elpi_string) + +let _ = let () = + Pcoq.grammar_extend elpi_string + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PSTRING (None))))) + (fun s loc -> +# 53 "src/coq_elpi_arg_syntax.mlg" + + Coq_elpi_utils.of_coq_loc loc, s + + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PQUOTATION "lp:")))) + (fun s loc -> +# 47 "src/coq_elpi_arg_syntax.mlg" + + if s.[0] = '\123' then strip_curly loc s + else if s.[0] = '(' then strip_round loc s + else if s.[0] = '[' then strip_square loc s + else Coq_elpi_utils.of_coq_loc loc, s + + )])]} + in () + + +# 59 "src/coq_elpi_arg_syntax.mlg" + +let pr_fp _ _ _ (_,x) = U.pr_qualified_name x +let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () + +let the_qname = ref "" +let any_qname loc_fun strm = + let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> + let pos = Stream.count strm in + Stream.junk strm; + let _, ep = Loc.unloc (loc_fun pos) in + begin match Stream.peek strm with + | Some (Tok.IDENT id) -> + let bp, _ = Loc.unloc (loc_fun (pos+1)) in + if Int.equal ep bp then + (Stream.junk strm; the_qname := sym ^ id) + else + the_qname := sym + | _ -> the_qname := sym + end + | _ -> raise Stream.Failure +let any_qname = Pcoq.Entry.of_parser "any_qname" any_qname + + + +let (wit_qualified_name, qualified_name) = Tacentries.argument_extend ~name:"qualified_name" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + []); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 85 "src/coq_elpi_arg_syntax.mlg" + pr_fp + ), (fun env sigma -> + +# 85 "src/coq_elpi_arg_syntax.mlg" + pr_fp + ), (fun env sigma -> + +# 85 "src/coq_elpi_arg_syntax.mlg" + pr_fp + )); + } +let _ = (wit_qualified_name, qualified_name) + +let _ = let () = + Pcoq.grammar_extend qualified_name + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm any_qname))) + (fun _ loc -> +# 91 "src/coq_elpi_arg_syntax.mlg" + loc, Str.split_delim (Str.regexp_string ".") !the_qname + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("_"))))) + (fun _ loc -> +# 90 "src/coq_elpi_arg_syntax.mlg" + loc, [] + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PIDENT (None))))) + ((Pcoq.Symbol.list0 (Pcoq.Symbol.token (Tok.PFIELD (None)))))) + (fun s i loc -> +# 89 "src/coq_elpi_arg_syntax.mlg" + loc, i :: s + )])]} + in () + +let (wit_elpi_loc, elpi_loc) = Tacentries.argument_extend ~name:"elpi_loc" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.stop) + (fun loc -> +# 97 "src/coq_elpi_arg_syntax.mlg" + loc + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 96 "src/coq_elpi_arg_syntax.mlg" + pp_elpi_loc + ), (fun env sigma -> + +# 96 "src/coq_elpi_arg_syntax.mlg" + pp_elpi_loc + ), (fun env sigma -> + +# 96 "src/coq_elpi_arg_syntax.mlg" + pp_elpi_loc + )); + } +let _ = (wit_elpi_loc, elpi_loc) + + +# 100 "src/coq_elpi_arg_syntax.mlg" + + +let record_fields = Pcoq.Entry.create "elpi:record_fields" +let telescope = Pcoq.Entry.create "elpi:telescope" +let colon_sort = Pcoq.Entry.create "elpi:colon_sort" +let colon_constr = Pcoq.Entry.create "elpi:colon_constr" +let pipe_telescope = Pcoq.Entry.create "elpi:pipe_telescope" +let inductive_constructors = Pcoq.Entry.create "elpi:inductive_constructors" + +let any_attribute : Attributes.vernac_flags Attributes.attribute = + Attributes.make_attribute (fun x -> [],x) +let skip_attribute : (Str.regexp list option * Str.regexp list option) Attributes.attribute = + let open Attributes.Notations in + let o2l = function None -> [] | Some l -> l in + Attributes.attribute_of_list + ["skip", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[skip=\"rex\"]")] + ++ + Attributes.attribute_of_list + ["only", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[only=\"rex\"]")] + +let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" + +let opt2list = function None -> [] | Some l -> l + +let the_kwd = ref "" +let any_kwd _ strm = + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when sym <> "." -> Stream.junk strm; the_kwd := sym + | _ -> raise Stream.Failure +let any_kwd = Pcoq.Entry.of_parser "any_symbols_or_kwd" any_kwd + + +let pr_attributes _ _ _ atts = + Pp.(prlist_with_sep (fun () -> str ",") Attributes.pr_vernac_flag atts) + +let wit_elpi_ftactic_arg = EA.wit_elpi_ftactic_arg + + + +let _ = let constructor = Pcoq.Entry.make "constructor" + and constructor_type = Pcoq.Entry.make "constructor_type" + in + let () = + Pcoq.grammar_extend record_fields + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make (Pcoq.Rule.stop) + (fun loc -> +# 151 "src/coq_elpi_arg_syntax.mlg" + [] + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm G_vernac.record_field))) + (fun f loc -> +# 150 "src/coq_elpi_arg_syntax.mlg" + [f] + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm G_vernac.record_field))) + ((Pcoq.Symbol.token (Tok.PKEYWORD (";"))))) + ((Pcoq.Symbol.nterm record_fields))) + (fun fs _ f loc -> +# 149 "src/coq_elpi_arg_syntax.mlg" + f :: fs + )])]} + in let () = + Pcoq.grammar_extend inductive_constructors + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm identref))) + ((Pcoq.Symbol.nterm constructor_type))) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("|"))))) + ((Pcoq.Symbol.list1sep ((Pcoq.Symbol.nterm constructor)) ((Pcoq.Symbol.token (Tok.PKEYWORD ("|")))) false))) + (fun l _ c id loc -> +# 157 "src/coq_elpi_arg_syntax.mlg" + c id :: l + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("|"))))) + ((Pcoq.Symbol.list1sep ((Pcoq.Symbol.nterm constructor)) ((Pcoq.Symbol.token (Tok.PKEYWORD ("|")))) false))) + (fun l _ loc -> +# 156 "src/coq_elpi_arg_syntax.mlg" + l + )])]} + in let () = + Pcoq.grammar_extend constructor + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm identref))) + ((Pcoq.Symbol.nterm constructor_type))) + (fun c id loc -> +# 161 "src/coq_elpi_arg_syntax.mlg" + c id + )])]} + in let () = + Pcoq.grammar_extend constructor_type + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm binders))) + ((Pcoq.Symbol.rules [Pcoq.Rules.make + (Pcoq.Rule.stop) + (fun + loc -> + +# 167 "src/coq_elpi_arg_syntax.mlg" + fun l id -> id,Constrexpr_ops.mkProdCN ~loc l (CAst.make ~loc @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, None)) + ); + Pcoq.Rules.make + (Pcoq.Rule.next_norec + (Pcoq.Rule.next_norec + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD (":"))))) + ((Pcoq.Symbol.nterm lconstr))) + (fun c _ + loc -> + +# 166 "src/coq_elpi_arg_syntax.mlg" + fun l id -> id,Constrexpr_ops.mkProdCN ~loc l c + )]))) + (fun t l loc -> +# 168 "src/coq_elpi_arg_syntax.mlg" + t l + )])]} + in let () = + Pcoq.grammar_extend pipe_telescope + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("|"))))) + ((Pcoq.Symbol.nterm binders))) + (fun bl _ loc -> +# 173 "src/coq_elpi_arg_syntax.mlg" + bl + )])]} + in let () = + Pcoq.grammar_extend telescope + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm binders))) + (fun bl loc -> +# 176 "src/coq_elpi_arg_syntax.mlg" + bl + )])]} + in let () = + Pcoq.grammar_extend colon_sort + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD (":"))))) + ((Pcoq.Symbol.nterm sort))) + (fun s _ loc -> +# 179 "src/coq_elpi_arg_syntax.mlg" + s + )])]} + in let () = + Pcoq.grammar_extend colon_constr + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD (":"))))) + ((Pcoq.Symbol.nterm lconstr))) + (fun s _ loc -> +# 182 "src/coq_elpi_arg_syntax.mlg" + s + )])]} + in let () = + Pcoq.grammar_extend coq_kwd_or_symbol + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm any_kwd))) + (fun _ loc -> +# 185 "src/coq_elpi_arg_syntax.mlg" + !the_kwd + )])]} + in () + +let (wit_elpi_arg, elpi_arg) = Tacentries.argument_extend ~name:"elpi_arg" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm coq_kwd_or_symbol))) + (fun x loc -> +# 215 "src/coq_elpi_arg_syntax.mlg" + EA.String x + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm lconstr))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ loc -> +# 213 "src/coq_elpi_arg_syntax.mlg" + EA.Term t + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Context")))) + ((Pcoq.Symbol.nterm telescope))) + (fun ty _ loc -> +# 212 "src/coq_elpi_arg_syntax.mlg" + EA.Context ty + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Axiom")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.nterm colon_constr))) + (fun t typ name _ + loc -> +# 210 "src/coq_elpi_arg_syntax.mlg" + + EA.ConstantDecl { EA.name = snd name; typ = (typ,Some t); body = None } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Definition")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm lconstr))) + (fun b _ t typ name + _ loc -> +# 208 "src/coq_elpi_arg_syntax.mlg" + + EA.ConstantDecl { EA.name = snd name; typ = (typ,t); body = Some b } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Class")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_sort)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm ident)))) + ((Pcoq.Symbol.token (CLexer.terminal "{")))) + ((Pcoq.Symbol.nterm record_fields))) + ((Pcoq.Symbol.token (CLexer.terminal "}")))) + (fun _ fs _ k _ s ps + name _ loc -> + +# 206 "src/coq_elpi_arg_syntax.mlg" + + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Record")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_sort)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm ident)))) + ((Pcoq.Symbol.token (CLexer.terminal "{")))) + ((Pcoq.Symbol.nterm record_fields))) + ((Pcoq.Symbol.token (CLexer.terminal "}")))) + (fun _ fs _ k _ s ps + name _ loc -> + +# 204 "src/coq_elpi_arg_syntax.mlg" + + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Variant")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm pipe_telescope)))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm inductive_constructors))) + (fun cs _ s nups ps + name _ loc -> + +# 202 "src/coq_elpi_arg_syntax.mlg" + + EA.IndtDecl { EA.finiteness = Vernacexpr.Variant; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "CoInductive")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm pipe_telescope)))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm inductive_constructors))) + (fun cs _ s nups ps + name _ loc -> + +# 200 "src/coq_elpi_arg_syntax.mlg" + + EA.IndtDecl { EA.finiteness = Vernacexpr.CoInductive; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Inductive")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm pipe_telescope)))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm inductive_constructors))) + (fun cs _ s nups ps + name _ loc -> + +# 198 "src/coq_elpi_arg_syntax.mlg" + + EA.IndtDecl { EA.finiteness = Vernacexpr.Inductive_kw; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm string))) + (fun s loc -> +# 197 "src/coq_elpi_arg_syntax.mlg" + EA.String s + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm integer))) + (fun n loc -> +# 196 "src/coq_elpi_arg_syntax.mlg" + EA.Int n + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm qualified_name))) + (fun s loc -> +# 195 "src/coq_elpi_arg_syntax.mlg" + EA.String (String.concat "." (snd s)) + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun ((fun f ist v -> (ist, f ist v)) ( + +# 191 "src/coq_elpi_arg_syntax.mlg" + EA.glob_arg + )); + Tacentries.arg_subst = Tacentries.ArgSubstFun ( + +# 192 "src/coq_elpi_arg_syntax.mlg" + EA.subst_arg + ); + Tacentries.arg_interp = Tacentries.ArgInterpLegacy ( + +# 190 "src/coq_elpi_arg_syntax.mlg" + EA.interp_arg + ); + Tacentries.arg_printer = ((fun env sigma -> + +# 193 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> EA.pp_raw_arg env sigma + ), (fun env sigma -> + +# 194 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> EA.pp_glob_arg env sigma + ), (fun env sigma -> + +# 189 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> EA.pp_top_arg env sigma + )); + } +let _ = (wit_elpi_arg, elpi_arg) + +let (wit_elpi_tactic_arg, elpi_tactic_arg) = Tacentries.argument_extend ~name:"elpi_tactic_arg" + { + Tacentries.arg_parsing = + Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_term_list")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 229 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.List EA.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_term")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 228 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_int_list")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 227 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.List EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_int")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 226 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_string_list")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 225 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.List EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_string")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 224 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm lconstr))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ loc -> +# 223 "src/coq_elpi_arg_syntax.mlg" + EA.Term t + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm string))) + (fun s loc -> +# 222 "src/coq_elpi_arg_syntax.mlg" + EA.String s + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm integer))) + (fun n loc -> +# 221 "src/coq_elpi_arg_syntax.mlg" + EA.Int n + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm qualified_name))) + (fun s loc -> +# 220 "src/coq_elpi_arg_syntax.mlg" + EA.String (String.concat "." (snd s)) + ))]); + Tacentries.arg_tag = Some + (Geninterp.val_tag (Genarg.topwit wit_elpi_ftactic_arg)); + Tacentries.arg_intern = + Tacentries.ArgInternWit (wit_elpi_ftactic_arg); + Tacentries.arg_subst = Tacentries.ArgSubstWit (wit_elpi_ftactic_arg); + Tacentries.arg_interp = + Tacentries.ArgInterpWit (wit_elpi_ftactic_arg); + Tacentries.arg_printer = + ((fun env sigma -> +# 0 "" +fun _ _ _ _ -> Pp.str "missing printer" + ), (fun env sigma -> +# 0 "" +fun _ _ _ _ -> Pp.str "missing printer" + ), (fun env sigma -> +# 0 "" +fun _ _ _ _ -> Pp.str "missing printer" + )); + } +let _ = (wit_elpi_tactic_arg, elpi_tactic_arg) + +let (wit_attributes, attributes) = Tacentries.argument_extend ~name:"attributes" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + []); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 233 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + ), (fun env sigma -> + +# 233 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + ), (fun env sigma -> + +# 233 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + )); + } +let _ = (wit_attributes, attributes) + +let _ = let my_attribute_list = Pcoq.Entry.make "my_attribute_list" + and my_attribute = Pcoq.Entry.make "my_attribute" + and my_attr_value = Pcoq.Entry.make "my_attr_value" + in + let () = + Pcoq.grammar_extend my_attribute_list + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.list0sep ((Pcoq.Symbol.nterm my_attribute)) ((Pcoq.Symbol.token (Tok.PKEYWORD (",")))) false))) + (fun a loc -> +# 237 "src/coq_elpi_arg_syntax.mlg" + a + )])]} + in let () = + Pcoq.grammar_extend my_attribute + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PIDENT (Some + ("using")))))) + ((Pcoq.Symbol.nterm my_attr_value))) + (fun v _ loc -> +# 243 "src/coq_elpi_arg_syntax.mlg" + "using", v + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.nterm my_attr_value))) + (fun v k loc -> +# 241 "src/coq_elpi_arg_syntax.mlg" + Names.Id.to_string k, v + )])]} + in let () = + Pcoq.grammar_extend my_attr_value + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make (Pcoq.Rule.stop) + (fun loc -> +# 250 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagEmpty + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("("))))) + ((Pcoq.Symbol.nterm my_attribute_list))) + ((Pcoq.Symbol.token (Tok.PKEYWORD (")"))))) + (fun _ a _ loc -> +# 249 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagList a + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("="))))) + ((Pcoq.Symbol.token (Tok.PIDENT (None))))) + (fun v _ loc -> +# 248 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagLeaf (Attributes.FlagIdent v) + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("="))))) + ((Pcoq.Symbol.nterm string))) + (fun v _ loc -> +# 247 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagLeaf (Attributes.FlagString v) + )])]} + in let () = + Pcoq.grammar_extend attributes + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.list1sep ((Pcoq.Symbol.nterm my_attribute)) ((Pcoq.Symbol.token (Tok.PKEYWORD (",")))) false))) + (fun atts loc -> +# 254 "src/coq_elpi_arg_syntax.mlg" + atts + )])]} + in () + +let (wit_ltac_attributes, ltac_attributes) = Tacentries.argument_extend ~name:"ltac_attributes" + { + Tacentries.arg_parsing = + Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm ident))) + (fun v loc -> +# 268 "src/coq_elpi_arg_syntax.mlg" + (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = + Tacentries.ArgInternFun ((fun f ist v -> (ist, f ist v)) ( + +# 264 "src/coq_elpi_arg_syntax.mlg" + fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t + )); + Tacentries.arg_subst = Tacentries.ArgSubstFun ( + +# 265 "src/coq_elpi_arg_syntax.mlg" + Detyping.subst_glob_constr (Global.env()) + ); + Tacentries.arg_interp = + Tacentries.ArgInterpLegacy ( +# 259 "src/coq_elpi_arg_syntax.mlg" + fun ist evd x -> match DAst.get x with + | Glob_term.GVar id -> + evd.Evd.sigma, + Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) + | _ -> assert false + ); + Tacentries.arg_printer = + ((fun env sigma -> +# 266 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> Ppconstr.pr_constr_expr env sigma + ), (fun env sigma -> +# 267 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> Printer.pr_glob_constr_env env sigma + ), (fun env sigma -> +# 258 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + )); + } +let _ = (wit_ltac_attributes, ltac_attributes) + diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg new file mode 100644 index 000000000..eea9d7c52 --- /dev/null +++ b/src/coq_elpi_arg_syntax.mlg @@ -0,0 +1,270 @@ +(* coq-elpi: Coq terms as the object language of elpi *) +(* license: GNU Lesser General Public License Version 2.1 or later *) +(* ------------------------------------------------------------------------- *) + +DECLARE PLUGIN "elpi_plugin" + +{ + +open Ltac_plugin + +open Pcoq.Constr +open Pcoq.Prim + +module EA = Coq_elpi_arg_HOAS +module U = Coq_elpi_utils + +(* Arguments ************************************************************* *) +let pr_elpi_string _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) + +let trim_loc loc = + let open Loc in + { loc with bp = loc.bp + 1; ep = loc.ep - 1 } + +let idents_of loc s = + let s = String.sub s 1 (String.length s - 2) in + let l = Str.(split (regexp "[\t \n]+") s) in + List.iter (fun x -> if not (CLexer.is_ident x) then raise Stream.Failure) l; + Coq_elpi_utils.of_coq_loc (trim_loc loc), l + +let rec strip_curly loc s = + if s.[0] = '\123' then strip_curly (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_round loc s = + if s.[0] = '(' then strip_round (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_square loc s = + if s.[0] = '[' then strip_square (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s + +} + +ARGUMENT EXTEND elpi_string PRINTED BY { pr_elpi_string } +| [ "xxxxxxxx" ] -> { (Elpi.API.Ast.Loc.initial "dummy", "") } (* XXX To be removed when maxime's patches gets merged *) +END +GRAMMAR EXTEND Gram GLOBAL: elpi_string; +elpi_string : [ + [ s = QUOTATION "lp:" -> { + if s.[0] = '\123' then strip_curly loc s + else if s.[0] = '(' then strip_round loc s + else if s.[0] = '[' then strip_square loc s + else Coq_elpi_utils.of_coq_loc loc, s + } + | s = STRING -> { + Coq_elpi_utils.of_coq_loc loc, s + } + ]]; +END + +{ +let pr_fp _ _ _ (_,x) = U.pr_qualified_name x +let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () + +let the_qname = ref "" +let any_qname loc_fun strm = + let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> + let pos = Stream.count strm in + Stream.junk strm; + let _, ep = Loc.unloc (loc_fun pos) in + begin match Stream.peek strm with + | Some (Tok.IDENT id) -> + let bp, _ = Loc.unloc (loc_fun (pos+1)) in + if Int.equal ep bp then + (Stream.junk strm; the_qname := sym ^ id) + else + the_qname := sym + | _ -> the_qname := sym + end + | _ -> raise Stream.Failure +let any_qname = Pcoq.Entry.of_parser "any_qname" any_qname + +} + +ARGUMENT EXTEND qualified_name PRINTED BY { pr_fp } +END +GRAMMAR EXTEND Gram GLOBAL: qualified_name; +qualified_name : + [ [ i = IDENT; s = LIST0 FIELD -> { loc, i :: s } + | "_" -> { loc, [] } + | any_qname -> { loc, Str.split_delim (Str.regexp_string ".") !the_qname } ] + ]; +END + +ARGUMENT EXTEND elpi_loc +PRINTED BY { pp_elpi_loc } +| [ ] -> { loc } +END + +{ + +let record_fields = Pcoq.Entry.create "elpi:record_fields" +let telescope = Pcoq.Entry.create "elpi:telescope" +let colon_sort = Pcoq.Entry.create "elpi:colon_sort" +let colon_constr = Pcoq.Entry.create "elpi:colon_constr" +let pipe_telescope = Pcoq.Entry.create "elpi:pipe_telescope" +let inductive_constructors = Pcoq.Entry.create "elpi:inductive_constructors" + +let any_attribute : Attributes.vernac_flags Attributes.attribute = + Attributes.make_attribute (fun x -> [],x) +let skip_attribute : (Str.regexp list option * Str.regexp list option) Attributes.attribute = + let open Attributes.Notations in + let o2l = function None -> [] | Some l -> l in + Attributes.attribute_of_list + ["skip", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[skip=\"rex\"]")] + ++ + Attributes.attribute_of_list + ["only", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[only=\"rex\"]")] + +let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" + +let opt2list = function None -> [] | Some l -> l + +let the_kwd = ref "" +let any_kwd _ strm = + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when sym <> "." -> Stream.junk strm; the_kwd := sym + | _ -> raise Stream.Failure +let any_kwd = Pcoq.Entry.of_parser "any_symbols_or_kwd" any_kwd + + +let pr_attributes _ _ _ atts = + Pp.(prlist_with_sep (fun () -> str ",") Attributes.pr_vernac_flag atts) + +let wit_elpi_ftactic_arg = EA.wit_elpi_ftactic_arg + +} + +GRAMMAR EXTEND Gram + GLOBAL: record_fields inductive_constructors telescope colon_sort colon_constr coq_kwd_or_symbol pipe_telescope; + + record_fields: + [ [ f = G_vernac.record_field; ";"; fs = record_fields -> { f :: fs } + | f = G_vernac.record_field -> { [f] } + | -> { [] } + ] ] + ; + + inductive_constructors: + [ [ "|"; l = LIST1 constructor SEP "|" -> { l } + | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { c id :: l } + ] ] + ; + constructor: + [ [ id = identref; c = constructor_type -> { c id } ] ] + ; + + constructor_type: + [[ l = binders; + t = [ ":"; c = lconstr -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l c } + | -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l (CAst.make ~loc @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, None)) } ] + -> { t l } + ]] + ; + + pipe_telescope: + [ [ "|"; bl = binders -> { bl } ] ]; + + telescope: + [ [ bl = binders -> { bl } ] ]; + + colon_sort: + [ [ ":"; s = sort -> { s } ] ]; + + colon_constr: + [ [ ":"; s = lconstr -> { s } ] ]; + + coq_kwd_or_symbol: + [ [ any_kwd -> { !the_kwd }] ]; +END + +ARGUMENT EXTEND elpi_arg +PRINTED BY { fun _ _ _ -> EA.pp_top_arg env sigma } +INTERPRETED BY { EA.interp_arg } +GLOBALIZED BY { EA.glob_arg } +SUBSTITUTED BY { EA.subst_arg } +RAW_PRINTED BY { fun _ _ _ -> EA.pp_raw_arg env sigma } +GLOB_PRINTED BY { fun _ _ _ -> EA.pp_glob_arg env sigma } +| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } +| [ integer(n) ] -> { EA.Int n } +| [ string(s) ] -> { EA.String s } +| [ "Inductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { + EA.IndtDecl { EA.finiteness = Vernacexpr.Inductive_kw; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } +| [ "CoInductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { + EA.IndtDecl { EA.finiteness = Vernacexpr.CoInductive; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } +| [ "Variant" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { + EA.IndtDecl { EA.finiteness = Vernacexpr.Variant; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } +| [ "Record" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } +| [ "Class" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } +| [ "Definition" qualified_name(name) telescope(typ) colon_constr_opt(t) ":=" lconstr(b) ] -> { + EA.ConstantDecl { EA.name = snd name; typ = (typ,t); body = Some b } } +| [ "Axiom" qualified_name(name) telescope(typ) colon_constr(t) ] -> { + EA.ConstantDecl { EA.name = snd name; typ = (typ,Some t); body = None } } +| [ "Context" telescope(ty) ] -> { EA.Context ty } +| [ "(" lconstr(t) ")" ] -> { EA.Term t } + +| [ coq_kwd_or_symbol(x) ] -> { EA.String x } +END + +ARGUMENT EXTEND elpi_tactic_arg +TYPED AS elpi_ftactic_arg +| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } +| [ integer(n) ] -> { EA.Int n } +| [ string(s) ] -> { EA.String s } +| [ "(" lconstr(t) ")" ] -> { EA.Term t } +| [ "ltac_string" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_string_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_int" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_int_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_term" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) } +| [ "ltac_term_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +END + +ARGUMENT EXTEND attributes + PRINTED BY { pr_attributes } +END +GRAMMAR EXTEND Gram GLOBAL: attributes; + my_attribute_list: + [ [ a = LIST0 my_attribute SEP "," -> { a } ] + ] + ; + my_attribute: + [ [ k = ident ; v = my_attr_value -> { Names.Id.to_string k, v } + (* Required because "ident" is declared a keyword when loading Ltac. *) + | IDENT "using" ; v = my_attr_value -> { "using", v } ] + ] + ; + my_attr_value: + [ [ "=" ; v = string -> { Attributes.VernacFlagLeaf (Attributes.FlagString v) } + | "=" ; v = IDENT -> { Attributes.VernacFlagLeaf (Attributes.FlagIdent v) } + | "(" ; a = my_attribute_list ; ")" -> { Attributes.VernacFlagList a } + | -> { Attributes.VernacFlagEmpty } ] + ] + ; + + attributes : [[ atts = LIST1 my_attribute SEP "," -> { atts } ]]; +END + +ARGUMENT EXTEND ltac_attributes + PRINTED BY { pr_attributes } + INTERPRETED BY { fun ist evd x -> match DAst.get x with + | Glob_term.GVar id -> + evd.Evd.sigma, + Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) + | _ -> assert false } + GLOBALIZED BY { fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t } + SUBSTITUTED BY { Detyping.subst_glob_constr (Global.env()) } + RAW_PRINTED BY { fun _ _ _ -> Ppconstr.pr_constr_expr env sigma } + GLOB_PRINTED BY { fun _ _ _ -> Printer.pr_glob_constr_env env sigma } +| [ ident(v) ] -> { (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) } +END + diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index fa588a24a..d6f8670de 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -96,7 +96,7 @@ let pr_econstr_env options env sigma t = | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in if options.hoas_holes = Some Heuristic then aux () expr else expr in - Ppconstr.pr_constr_expr env sigma expr) + Ppconstr.pr_constr_expr_n env sigma options.pplevel expr) let tactic_mode = ref false let on_global_state api thunk = (); (fun state -> @@ -305,6 +305,14 @@ let goal : ( (Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context * Evar.t * Coq_elpi_a state, (ctx,k,args), gls1 @ gls2); } +let tactic_arg : (Coq_elpi_arg_HOAS.coq_arg, Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context, API.Data.constraints) CConv.t = { + CConv.ty = Conv.TyName "argument"; + pp_doc = (fun fmt () -> ()); + pp = (fun fmt _ -> Format.fprintf fmt "TODO"); + embed = (fun ~depth _ _ _ _ -> assert false); + readback = Coq_elpi_arg_HOAS.in_coq_arg; +} + let id = { B.string with API.Conversion.ty = Conv.TyName "id"; pp_doc = (fun fmt () -> @@ -439,7 +447,7 @@ let cs_instance = let open Conv in let open API.AlgebraicData in let open Record doc = "Canonical Structure instances: (cs-instance Proj ValPat Inst)"; pp = (fun fmt (_,{ o_DEF }) -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((Printer.pr_constr_env (Global.env()) Evd.empty o_DEF))); constructors = [ - K("cs-instance","",A(gref,A(cs_pattern,CA(closed_ground_term,N))), (* XXX should be a gref *) + K("cs-instance","",A(gref,A(cs_pattern,A(gref,N))), B (fun p v i -> assert false), M (fun ~ok ~ko ((proj_gr,patt), { o_DEF = solution; (* c *) @@ -448,7 +456,7 @@ let cs_instance = let open Conv in let open API.AlgebraicData in let open Record o_TABS = types; (* b1 .. bk *) o_TPARAMS = params; (* p1 .. pm *) o_NPARAMS = nparams; (* m *) - o_TCOMPS = cval_args }) -> ok proj_gr patt (EConstr.of_constr solution))) + o_TCOMPS = cval_args }) -> ok proj_gr patt (fst @@ Constr.destRef solution))) ] } @@ -818,7 +826,7 @@ let ppboxes = let open Conv in let open Pp in let open API.AlgebraicData in decl let warn_deprecated_add_axiom = CWarnings.create ~name:"elpi.add-const-for-axiom-or-sectionvar" - ~category:"deprecated" + ~category:"elpi.deprecated" Pp.(fun () -> strbrk ("elpi: Using coq.env.add-const for declaring axioms or " ^ "section variables is deprecated. Use coq.env.add-axiom or " ^ @@ -852,7 +860,110 @@ let add_axiom_or_variable api id sigma ty local = gr ;; +type tac_abbrev = { + abbrev_name : qualified_name; + tac_name : qualified_name; + tac_fixed_args : (Coq_elpi_arg_HOAS.tac, Glob_term.glob_constr) Coq_elpi_arg_HOAS.glob_arg list; +} + + +let rec gbpmp = fun f -> function + | [x] -> Pcoq.Rule.next Pcoq.Rule.stop (Pcoq.Symbol.token (Tok.PIDENT(Some x))), (fun a _ -> f a) + | x :: xs -> + let r, f = gbpmp f xs in + Pcoq.Rule.next r (Pcoq.Symbol.token (Tok.PFIELD (Some x))), (fun a _ -> f a) + | [] -> assert false + +let cache_abbrev_for_tac (_, { abbrev_name; tac_name = tacname; tac_fixed_args = more_args }) = + let action args loc = + let open Ltac_plugin in + let tac = + let open Tacexpr in + let elpi_tac = { + mltac_plugin = "elpi_plugin"; + mltac_tactic = "elpi_tac"; } in + let elpi_tac_entry = { + mltac_name = elpi_tac; + mltac_index = 0; } in + let more_args = more_args |> List.map (function + | Coq_elpi_arg_HOAS.Int _ as t -> t + | Coq_elpi_arg_HOAS.String _ as t -> t + | Coq_elpi_arg_HOAS.Term t -> + let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in + let rec aux () ({ CAst.v } as orig) = match v with + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in + Coq_elpi_arg_HOAS.Term (aux () expr) + | _ -> assert false) in + let tacname = loc, tacname in + let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in + let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Term arg) in + let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in + (TacML (CAst.make (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)]))) in + CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac)) in + let rule, action = gbpmp (Obj.magic action) (List.rev abbrev_name) in + Pcoq.grammar_extend Pcoq.Constr.term { + Pcoq.pos = Some (Gramlib.Gramext.Before "10"); + data = [ (None, None, [ Pcoq.Production.make + (Pcoq.Rule.next (Obj.magic rule) (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) + (Obj.magic action) + ])] + } + +let subst_abbrev_for_tac (subst, { abbrev_name; tac_name; tac_fixed_args }) = { + abbrev_name; + tac_name; + tac_fixed_args = List.map (Coq_elpi_arg_HOAS.subst_tac_arg_glob subst) tac_fixed_args +} + +let inAbbreviationForTactic : tac_abbrev -> Libobject.obj = + Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED-TAC-ABBREV" + ~cache:cache_abbrev_for_tac ~subst:(Some subst_abbrev_for_tac) +let cache_tac_abbrev (q,qualid) = cache_abbrev_for_tac (q,{ + abbrev_name = qualid; + tac_name = qualid; + tac_fixed_args = []; +}) + +let mode = let open API.AlgebraicData in let open Hints in declare { + ty = Conv.TyName "hint-mode"; + doc = "Hint Mode"; + pp = (fun fmt (x : hint_mode) -> Pp.pp_with fmt (pp_hint_mode x)); + constructors = [ + K ("mode-ground", "No Evar",N, + B ModeInput, + M (fun ~ok ~ko -> function ModeInput -> ok | _ -> ko ())); + K("mode-input","No Head Evar",N, + B ModeNoHeadEvar, + M (fun ~ok ~ko -> function ModeNoHeadEvar -> ok | _ -> ko ())); + K("mode-output","Anything",N, + B ModeOutput, + M (fun ~ok ~ko -> function ModeOutput -> ok | _ -> ko ())); + ] +} |> CConv.(!<) + +module WMsg = Set.Make(struct + type t = Loc.t option * string + let compare = Stdlib.compare +end) + +let coq_warning_cache : WMsg.t API.Data.StrMap.t ref = + ref API.Data.StrMap.empty +let coq_warning_cache category name loc txt = + let key = category ^ " " ^ name in + let msg = loc, txt in + try + let s = API.Data.StrMap.find key !coq_warning_cache in + if WMsg.mem msg s then false + else + let s = WMsg.add msg s in + coq_warning_cache := API.Data.StrMap.add key s !coq_warning_cache; + true + with + Not_found -> + coq_warning_cache := API.Data.StrMap.add key (WMsg.singleton msg) !coq_warning_cache; + true (*****************************************************************************) @@ -945,7 +1056,8 @@ line option|}))), Some (Coq_elpi_utils.to_coq_loc (API.RawOpaqueData.to_loc loc)), args | _ -> None, x :: args in - warning ?loc (pp2string (P.list ~boxed:true pp " ") args); + let txt = pp2string (P.list ~boxed:true pp " ") args in + if coq_warning_cache category name loc txt then warning ?loc txt; state, ())), DocAbove); @@ -981,7 +1093,8 @@ Note: [ctype \"bla\"] is an opaque data type and by convention it is written [@b MLData gref; MLData id; MLData modpath; - MLData modtypath; ] @ + MLData modtypath; + ] @ [ LPDoc "-- Environment: read ------------------------------------------------"; @@ -1124,7 +1237,7 @@ It's a fatal error if Name cannot be located.|})), )), DocAbove); - MLCode(Pred("coq.env.const-opaque?", + MLCode(Pred("coq.env.opaque?", In(constant, "GR", Read(global, "checks if GR is an opaque constant")), (fun c ~depth {env} _ state -> @@ -1139,7 +1252,7 @@ It's a fatal error if Name cannot be located.|})), | Context.Named.Declaration.LocalDef _ -> raise Pred.No_clause | Context.Named.Declaration.LocalAssum _ -> ())), DocAbove); - + MLCode(Pred("coq.env.const", In(constant, "GR", COut(!>> option closed_ground_term, "Bo", @@ -1183,7 +1296,7 @@ It's a fatal error if Name cannot be located.|})), end, [])), DocAbove); - MLCode(Pred("coq.env.const-primitive?", + MLCode(Pred("coq.env.primitive?", In(constant, "GR", Read (global,"tests if GR is a primitive constant (like uin63 addition)")), (fun c ~depth {env} _ state -> @@ -1252,6 +1365,20 @@ It's a fatal error if Name cannot be located.|})), (fun _ ~depth _ _ state -> !: (mp2path (Safe_typing.current_modpath (Global.safe_env ()))))), DocAbove); + LPCode {|% 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. + |}; + + LPCode {|% 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. + |}; + LPDoc "-- Environment: write -----------------------------------------------"; LPDoc ("Note: universe constraints are taken from ELPI's constraints "^ @@ -1514,6 +1641,28 @@ denote the same x as before.|}; state, (), []))), DocAbove); + MLCode(Pred("coq.env.projections", + In(inductive, "StructureName", + Out(list (option constant), "Projections", + Easy "given a record StructureName lists all projections")), + (fun i _ ~depth -> + !: (Recordops.lookup_projections i |> + CList.map (Option.map (fun x -> Constant x))))), + DocAbove); + + MLCode(Pred("coq.env.primitive-projections", + In(inductive, "StructureName", + Out(list (option (pair projection int)), "Projections", + Easy "given a record StructureName lists all primitive projections")), + (fun i _ ~depth -> + !: (Recordops.lookup_projections i |> + CList.map (fun o -> Option.bind o (fun x -> + Option.bind (Recordops.find_primitive_projection x) (fun c -> + let c = Names.Projection.make c false in + let np = Names.Projection.npars c in + let na = Names.Projection.arg c in + Some (c, np + na))))))), + DocAbove); LPDoc "-- Universes --------------------------------------------------------"; @@ -1598,6 +1747,8 @@ denote the same x as before.|}; MLData Coq_elpi_utils.uint63; MLData Coq_elpi_utils.float64; + MLData Coq_elpi_utils.projection; + MLData primitive_value; LPCode {| % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -1652,17 +1803,16 @@ Supported attributes: !: (try [(p,v),snd @@ Recordops.lookup_canonical_conversion env (p,v)] with Not_found -> []))), DocAbove); - MLCode(Pred("coq.CS.canonical-projections", - In(inductive, "StructureName", - Out(list (option constant), "Projections", - Easy "given a record StructureName lists all projections")), - (fun i _ ~depth -> - !: (Recordops.lookup_projections i |> - CList.map (Option.map (fun x -> Constant x))))), + MLCode(Pred("coq.TC.declare-class", + In(gref, "GR", + Full(global, {|Declare GR as a type class|})), + (fun gr ~depth { options } _ -> on_global_state "coq.TC.declare-class" (fun state -> + Record.declare_existing_class gr; + state, (), []))), DocAbove); MLData tc_instance; - + MLCode(Pred("coq.TC.declare-instance", In(gref, "GR", In(int, "Priority", @@ -1757,6 +1907,47 @@ NParams can always be omitted, since it is inferred. with Not_found -> !: [])), DocAbove); + LPCode {|% 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. +|}; + + LPDoc "-- Coq's Hint DB -------------------------------------"; + + MLData mode; + + MLCode(Pred("coq.hints.add-mode", + In(gref, "GR", + In(B.string, "DB", + In(B.list mode, "Mode", + Full(global, {|Adds a mode declaration to DB about GR. +Supported attributes: +- @local! (default: false)|})))), + (fun gr db mode ~depth:_ {options} _ -> on_global_state "coq.hints.add-mode" (fun state -> + let open Goptions in + let locality = if options.local = Some true then OptLocal else OptExport in + Hints.add_hints ~locality [db] (Hints.HintsModeEntry(gr,mode)); + state, (), [] + ))), + DocAbove); + + MLCode(Pred("coq.hints.modes", + In(gref, "GR", + In(B.string, "DB", + Out(B.list (B.list mode), "Modes", + Easy {|Gets all the mode declarations in DB about GR|}))), + (fun gr db _ ~depth:_ -> + try + let db = Hints.searchtable_map db in + let modes = Hints.Hint_db.modes db in + !: (List.map (fun a -> Array.to_list a) @@ GlobRef.Map.find gr modes) + with Not_found -> + !: [] + )), + DocAbove); + LPDoc "-- Coq's notational mechanisms -------------------------------------"; MLData implicit_kind; @@ -2009,6 +2200,34 @@ Supported attributes: )), DocAbove); + MLCode(Pred("coq.notation.add-abbreviation-for-tactic", + In(B.string,"Name", + In(B.string,"TacticName", + CIn(CConv.(!>>) B.list tactic_arg,"FixedArgs", + Full(proof_context, {|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.|})))), + (fun name tacname more_args ~depth { options} _ -> on_global_state "coq.notation.add-abbreviation-for-tactic" (fun state -> + let sigma = get_sigma state in + let env = get_global_env state in + let tac_fixed_args = more_args |> List.map (function + | Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Int n + | Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.String s + | Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Term (Coq_elpi_utils.detype env sigma t)) in + let abbrev_name = Coq_elpi_utils.string_split_on_char '.' name in + let tac_name = Coq_elpi_utils.string_split_on_char '.' tacname in + Lib.add_anonymous_leaf @@ inAbbreviationForTactic { abbrev_name; tac_name; tac_fixed_args}; + state, (), []))), + DocAbove); + MLData attribute_value; MLData attribute; @@ -2275,14 +2494,14 @@ hole. Similarly universe levels present in T are disregarded.|}))))), LPCode {|% 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. |}; LPCode {|% 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. |}; @@ -2513,6 +2732,7 @@ Supported attributes: - @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 _)|}))), (fun t _ ~depth proof_context constraints state -> let sigma = get_sigma state in @@ -2527,6 +2747,7 @@ Supported attributes: 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 _)|}))), (fun t _ ~depth proof_context constraints state -> let sigma = get_sigma state in diff --git a/src/coq_elpi_builtins.mli b/src/coq_elpi_builtins.mli index eee3bf21f..74b8d170e 100644 --- a/src/coq_elpi_builtins.mli +++ b/src/coq_elpi_builtins.mli @@ -3,13 +3,14 @@ (* ------------------------------------------------------------------------- *) open Elpi.API +open Coq_elpi_utils val coq_builtins : BuiltIn.declaration list (* Clauses to be added to elpi programs when the execution is over *) val clauses_for_later : - (string list * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component + (qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component val set_accumulate_to_db : ((string list -> Ast.program -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit)) -> unit type attribute_data = @@ -23,4 +24,6 @@ type attribute_value = val attribute : (string * attribute_value) Conversion.t (* In tactic mode some APIs are disabled *) -val tactic_mode : bool ref \ No newline at end of file +val tactic_mode : bool ref + +val cache_tac_abbrev : (Libobject.object_name * qualified_name) -> unit diff --git a/src/coq_elpi_builtins_HOAS.ml b/src/coq_elpi_builtins_HOAS.ml index 3ef4b5cb1..f898f025f 100644 --- a/src/coq_elpi_builtins_HOAS.ml +++ b/src/coq_elpi_builtins_HOAS.ml @@ -29,6 +29,7 @@ pred attributes o:list attribute. % solve % Where [str "foo", int 3, trm (app[f,x])] is part of . % 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. @@ -72,9 +73,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. @@ -310,6 +308,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 and +% , then all: elpi tac runs the following query +% +% msolve [,] NewGoals ; % note the disjunction +% coq.ltac.all (coq.ltac.open solve) [,] 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 is in both and but +% it is interpreted in both contexts independently. If both goals have a proof +% variable named "x" then passing (@eq_refl _ x) as 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). % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -328,6 +342,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 diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 65c155927..e604bd72b 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -169,7 +169,7 @@ let rec gterm2lp ~depth state x = Id.Map.bindings ctx.name2db |> List.filter (fun (n,_) -> not(is_restricted_name n)) |> List.map snd |> - List.sort Pervasives.compare |> + List.sort Stdlib.compare |> List.map E.mkBound in state, E.mkUnifVar uv ~args state @@ -185,12 +185,26 @@ let rec gterm2lp ~depth state x = | GEvar(_k,_subst) -> nYI "(glob)HOAS for GEvar" | GPatVar _ -> nYI "(glob)HOAS for GPatVar" -(* | GProj _ -> nYI "(glob)HOAS for GProj" *) - | GApp(hd,args) -> - let state, hd = gterm2lp ~depth state hd in - let state, args = CList.fold_left_map (gterm2lp ~depth) state args in - state, in_elpi_appl ~depth hd args + | GApp(hd,args) -> begin + match DAst.get hd with + | GRef(GlobRef.ConstRef p,_ul) when Recordops.is_primitive_projection p -> + let p = Option.get @@ Recordops.find_primitive_projection p in + let p = Projection.make p false in + let npars = Projection.npars p in + begin match CList.skipn npars args with + | _ :: _ as args -> + let state, args = CList.fold_left_map (gterm2lp ~depth) state args in + let state, p = in_elpi_primitive ~depth state (Projection p) in + state, in_elpi_appl ~depth p args + | [] -> CErrors.user_err ~hdr:"elpi quotation" + Pp.(str"Coq primitive projection " ++ Projection.print p ++ str " has not enough arguments"); + end + | _ -> + let state, hd = gterm2lp ~depth state hd in + let state, args = CList.fold_left_map (gterm2lp ~depth) state args in + state, in_elpi_appl ~depth hd args + end | GLetTuple(kargs,(as_name,oty),t,b) -> let state, t = gterm2lp ~depth state t in @@ -300,8 +314,8 @@ let rec gterm2lp ~depth state x = let state, bo = under_ctx (Name name) ty None gterm2lp ~depth state bo in state, in_elpi_fix (Name name) rno ty bo | GRec _ -> nYI "(glob)HOAS mutual/non-struct fix" - | GInt i -> in_elpi_uint63 ~depth state i - | GFloat f -> in_elpi_float64 ~depth state f + | GInt i -> in_elpi_primitive ~depth state (Uint63 i) + | GFloat f -> in_elpi_primitive ~depth state (Float64 f) | GArray _ -> nYI "(glob)HOAS persistent arrays" ;; diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index a33124787..1c621d0b4 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -170,6 +170,18 @@ let float64 : Float64.t Elpi.API.Conversion.t = constants = []; } + let projection : Names.Projection.t Elpi.API.Conversion.t = + let open Elpi.API.OpaqueData in + declare { + name = "projection"; + doc = ""; + pp = (fun fmt i -> Format.fprintf fmt "%s" (Names.Projection.to_string i)); + compare = Names.Projection.CanOrd.compare; + hash = Names.Projection.CanOrd.hash; + hconsed = false; + constants = []; + } + let fold_elpi_term f acc ~depth t = let module E = Elpi.API.RawData in match t with @@ -210,7 +222,7 @@ let detype_closed_glob env sigma closure = fix_detype gbody type qualified_name = string list -let compare_qualified_name = Pervasives.compare +let compare_qualified_name = Stdlib.compare let pr_qualified_name = Pp.prlist_with_sep (fun () -> Pp.str".") Pp.str let show_qualified_name = String.concat "." let pp_qualified_name fmt l = Format.fprintf fmt "%s" (String.concat "." l) diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index 403936ac3..e5a944150 100644 --- a/src/coq_elpi_utils.mli +++ b/src/coq_elpi_utils.mli @@ -32,6 +32,7 @@ val fold_elpi_term : val uint63 : Uint63.t Elpi.API.Conversion.t val float64 : Float64.t Elpi.API.Conversion.t +val projection : Names.Projection.t Elpi.API.Conversion.t type clause_scope = Local | Regular | Global | SuperGlobal val pp_scope : Format.formatter -> clause_scope -> unit diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index b87252d5e..4653393c9 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -147,7 +147,7 @@ and src_string = { sast : EC.compilation_unit } type nature = Command | Tactic | Program -let compare_src = Pervasives.compare +let compare_src = Stdlib.compare module SrcSet = Set.Make(struct type t = src let compare = compare_src end) @@ -190,7 +190,7 @@ let get_paths () = "." :: build_dir :: installed_dirs (* Setup called *) -let elpi = Pervasives.ref None +let elpi = Stdlib.ref None let elpi_builtins = API.BuiltIn.declare @@ -694,7 +694,7 @@ let run_tactic_common loc ?(static_check=false) program ~main ?(atts=[]) () = in let program = get_and_compile program in match run ~tactic_mode:true ~static_check program (`Fun query) with - | API.Execute.Success solution -> Coq_elpi_HOAS.tclSOLUTION2EVD solution + | API.Execute.Success solution -> Coq_elpi_HOAS.tclSOLUTION2EVD sigma solution | API.Execute.NoMoreSteps -> CErrors.user_err Pp.(str "elpi run out of steps") | API.Execute.Failure -> CErrors.user_err Pp.(str "elpi fails") | exception (Coq_elpi_utils.LtacFail (level, msg)) -> tclFAIL level msg @@ -744,33 +744,37 @@ let loc_merge l1 l2 = try Loc.merge l1 l2 with Failure _ -> l1 -open Coq_elpi_arg_HOAS - -let in_exported_program : (qualified_name * (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag * (cmd raw_arg, cmd glob_arg,top_arg) Genarg.ArgT.tag * (Attributes.vernac_flags,Attributes.vernac_flags,Attributes.vernac_flags) Genarg.ArgT.tag) -> Libobject.obj = +let in_exported_program : nature * qualified_name * string -> Libobject.obj = Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED" - ~cache:(fun (_,(p,tag_loc,tag_arg,tag_attributes)) -> - let p_str = String.concat "." p in - match get_nature p with + ~cache:(fun (q,(nature,p,p_str)) -> + match nature with | Command -> Vernacextend.vernac_extend ~command:("Elpi"^p_str) ~classifier:(fun _ -> Vernacextend.(VtSideff ([], VtNow))) ?entry:None [ Vernacextend.TyML (false, - Vernacextend.TyNonTerminal (Extend.TUentry tag_loc, + Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), Vernacextend.TyTerminal (p_str, - Vernacextend.TyNonTerminal (Extend.TUlist0 (Extend.TUentry tag_arg), - Vernacextend.TyNonTerminal (Extend.TUentry tag_loc, + Vernacextend.TyNonTerminal (Extend.TUlist0 (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_arg)), + Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), Vernacextend.TyNil)))), (fun loc0 args loc1 (* 8.14 ~loc*) ~atts -> Vernacextend.VtDefault (fun () -> run_program (loc_merge loc0 loc1) (*loc*) p ~atts args)), None)] - | (Tactic | Program) -> - CErrors.user_err Pp.(str "elpi: Only commands can be exported")) - ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))) - -let export_command p tag_loc tag_arg tag_attributes = - Lib.add_anonymous_leaf (in_exported_program (p,tag_loc,tag_arg,tag_attributes)) + | Tactic -> + Coq_elpi_builtins.cache_tac_abbrev (q,p) + | Program -> + CErrors.user_err Pp.(str "elpi: Only commands and tactics can be exported")) + ~subst:(Some (function + | _, (Command, _, _) ->CErrors.user_err Pp.(str"elpi: No functors yet") + | _, (Tactic,_,_ as x) -> x + | _, (Program,_,_) -> assert false)) + +let export_command p = + let p_str = String.concat "." p in + let nature = get_nature p in + Lib.add_anonymous_leaf (in_exported_program (nature,p,p_str)) let skip ~atts:(skip,only) f x = let m rex = Str.string_match rex Coq_config.version 0 in diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index 2d510fec6..fe70f9e35 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -41,10 +41,5 @@ val run_in_program : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> u val run_tactic : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Geninterp.interp_sign -> top_tac_arg list -> unit Proofview.tactic val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Geninterp.interp_sign -> unit Proofview.tactic -val export_command : - qualified_name -> - (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag -> - (cmd raw_arg,cmd glob_arg,top_arg) Genarg.ArgT.tag -> - (Attributes.vernac_flags,Attributes.vernac_flags,Attributes.vernac_flags) Genarg.ArgT.tag -> - unit +val export_command : qualified_name -> unit diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 33867a52a..519c00911 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -10,96 +10,16 @@ open Stdarg open Ltac_plugin open Pcoq.Constr -open Pcoq.Prim +open Coq_elpi_arg_syntax module EV = Coq_elpi_vernacular module EA = Coq_elpi_arg_HOAS module U = Coq_elpi_utils -(* Arguments ************************************************************* *) -let pr_elpi_string _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) - -let trim_loc loc = - let open Loc in - { loc with bp = loc.bp + 1; ep = loc.ep - 1 } - -let idents_of loc s = - let s = String.sub s 1 (String.length s - 2) in - let l = Str.(split (regexp "[\t \n]+") s) in - List.iter (fun x -> if not (CLexer.is_ident x) then raise Stream.Failure) l; - Coq_elpi_utils.of_coq_loc (trim_loc loc), l - -let rec strip_curly loc s = - if s.[0] = '\123' then strip_curly (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s -let rec strip_round loc s = - if s.[0] = '(' then strip_round (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s -let rec strip_square loc s = - if s.[0] = '[' then strip_square (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s - -} - -ARGUMENT EXTEND elpi_string PRINTED BY { pr_elpi_string } -| [ "xxxxxxxx" ] -> { (Elpi.API.Ast.Loc.initial "dummy", "") } (* XXX To be removed when maxime's patches gets merged *) -END -GRAMMAR EXTEND Gram GLOBAL: elpi_string; -elpi_string : [ - [ s = QUOTATION "lp:" -> { - if s.[0] = '\123' then strip_curly loc s - else if s.[0] = '(' then strip_round loc s - else if s.[0] = '[' then strip_square loc s - else Coq_elpi_utils.of_coq_loc loc, s - } - | s = STRING -> { - Coq_elpi_utils.of_coq_loc loc, s - } - ]]; -END - -{ -let pr_fp _ _ _ (_,x) = U.pr_qualified_name x -let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () - -let the_qname = ref "" -let any_qname loc_fun strm = - let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in - match Stream.peek strm with - | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> - let pos = Stream.count strm in - Stream.junk strm; - let _, ep = Loc.unloc (loc_fun pos) in - begin match Stream.peek strm with - | Some (Tok.IDENT id) -> - let bp, _ = Loc.unloc (loc_fun (pos+1)) in - if Int.equal ep bp then - (Stream.junk strm; the_qname := sym ^ id) - else - the_qname := sym - | _ -> the_qname := sym - end - | _ -> raise Stream.Failure -let any_qname = Pcoq.Entry.of_parser "any_qname" any_qname - } -ARGUMENT EXTEND qualified_name PRINTED BY { pr_fp } -END -GRAMMAR EXTEND Gram GLOBAL: qualified_name; -qualified_name : - [ [ i = IDENT; s = LIST0 FIELD -> { loc, i :: s } - | "_" -> { loc, [] } - | any_qname -> { loc, Str.split_delim (Str.regexp_string ".") !the_qname } ] - ]; -END - -ARGUMENT EXTEND elpi_loc -PRINTED BY { pp_elpi_loc } -| [ ] -> { loc } -END - (* Anti-quotation ******************************************************** *) + { let pr_elpi_code _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) } @@ -145,7 +65,7 @@ GRAMMAR EXTEND Gram else Genarg.in_gen (Genarg.rawwit wit_elpi_code) (Coq_elpi_utils.of_coq_loc loc,s) in CAst.make ~loc (Constrexpr.CHole (None, Namegen.IntroAnonymous, Some arg)) } ] - ] + ] ; END @@ -166,177 +86,6 @@ GRAMMAR EXTEND Gram END (* Syntax **************************************************************** *) -{ - -let record_fields = Pcoq.Entry.create "elpi:record_fields" -let telescope = Pcoq.Entry.create "elpi:telescope" -let colon_sort = Pcoq.Entry.create "elpi:colon_sort" -let colon_constr = Pcoq.Entry.create "elpi:colon_constr" -let pipe_telescope = Pcoq.Entry.create "elpi:pipe_telescope" -let inductive_constructors = Pcoq.Entry.create "elpi:inductive_constructors" - -let any_attribute : Attributes.vernac_flags Attributes.attribute = - Attributes.make_attribute (fun x -> [],x) -let skip_attribute : (Str.regexp list option * Str.regexp list option) Attributes.attribute = - let open Attributes.Notations in - let o2l = function None -> [] | Some l -> l in - Attributes.attribute_of_list - ["skip", - fun old -> function - | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old - | _ -> CErrors.user_err (Pp.str "Syntax error, use #[skip=\"rex\"]")] - ++ - Attributes.attribute_of_list - ["only", - fun old -> function - | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old - | _ -> CErrors.user_err (Pp.str "Syntax error, use #[only=\"rex\"]")] - -let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" - -let opt2list = function None -> [] | Some l -> l - -let the_kwd = ref "" -let any_kwd _ strm = - match Stream.peek strm with - | Some (Tok.KEYWORD sym) when sym <> "." -> Stream.junk strm; the_kwd := sym - | _ -> raise Stream.Failure -let any_kwd = Pcoq.Entry.of_parser "any_symbols_or_kwd" any_kwd - - -let pr_attributes _ _ _ atts = - Pp.(prlist_with_sep (fun () -> str ",") Attributes.pr_vernac_flag atts) - -let wit_elpi_ftactic_arg = EA.wit_elpi_ftactic_arg - -} - -GRAMMAR EXTEND Gram - GLOBAL: record_fields inductive_constructors telescope colon_sort colon_constr coq_kwd_or_symbol pipe_telescope; - - record_fields: - [ [ f = G_vernac.record_field; ";"; fs = record_fields -> { f :: fs } - | f = G_vernac.record_field -> { [f] } - | -> { [] } - ] ] - ; - - inductive_constructors: - [ [ "|"; l = LIST1 constructor SEP "|" -> { l } - | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { c id :: l } - ] ] - ; - constructor: - [ [ id = identref; c = constructor_type -> { c id } ] ] - ; - - constructor_type: - [[ l = binders; - t = [ ":"; c = lconstr -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l c } - | -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l (CAst.make ~loc @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, None)) } ] - -> { t l } - ]] - ; - - pipe_telescope: - [ [ "|"; bl = binders -> { bl } ] ]; - - telescope: - [ [ bl = binders -> { bl } ] ]; - - colon_sort: - [ [ ":"; s = sort -> { s } ] ]; - - colon_constr: - [ [ ":"; s = lconstr -> { s } ] ]; - - coq_kwd_or_symbol: - [ [ any_kwd -> { !the_kwd }] ]; -END - -ARGUMENT EXTEND elpi_arg -PRINTED BY { fun _ _ _ -> EA.pp_top_arg env sigma } -INTERPRETED BY { EA.interp_arg } -GLOBALIZED BY { EA.glob_arg } -SUBSTITUTED BY { EA.subst_arg } -RAW_PRINTED BY { fun _ _ _ -> EA.pp_raw_arg env sigma } -GLOB_PRINTED BY { fun _ _ _ -> EA.pp_glob_arg env sigma } -| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } -| [ integer(n) ] -> { EA.Int n } -| [ string(s) ] -> { EA.String s } -| [ "Inductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { - EA.IndtDecl { EA.finiteness = Vernacexpr.Inductive_kw; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } -| [ "CoInductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { - EA.IndtDecl { EA.finiteness = Vernacexpr.CoInductive; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } -| [ "Variant" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { - EA.IndtDecl { EA.finiteness = Vernacexpr.Variant; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } -| [ "Record" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { - EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } -| [ "Class" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { - EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } -| [ "Definition" qualified_name(name) telescope(typ) colon_constr_opt(t) ":=" lconstr(b) ] -> { - EA.ConstantDecl { EA.name = snd name; typ = (typ,t); body = Some b } } -| [ "Axiom" qualified_name(name) telescope(typ) colon_constr(t) ] -> { - EA.ConstantDecl { EA.name = snd name; typ = (typ,Some t); body = None } } -| [ "Context" telescope(ty) ] -> { EA.Context ty } -| [ "(" lconstr(t) ")" ] -> { EA.Term t } - -| [ coq_kwd_or_symbol(x) ] -> { EA.String x } -END - -ARGUMENT EXTEND elpi_tactic_arg -TYPED AS elpi_ftactic_arg -| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } -| [ integer(n) ] -> { EA.Int n } -| [ string(s) ] -> { EA.String s } -| [ "(" lconstr(t) ")" ] -> { EA.Term t } -| [ "ltac_string" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_string_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_int" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_int_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_term" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) } -| [ "ltac_term_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -END - -ARGUMENT EXTEND attributes - PRINTED BY { pr_attributes } -END -GRAMMAR EXTEND Gram GLOBAL: attributes; - my_attribute_list: - [ [ a = LIST0 my_attribute SEP "," -> { a } ] - ] - ; - my_attribute: - [ [ k = ident ; v = my_attr_value -> { Names.Id.to_string k, v } - (* Required because "ident" is declared a keyword when loading Ltac. *) - | IDENT "using" ; v = my_attr_value -> { "using", v } ] - ] - ; - my_attr_value: - [ [ "=" ; v = string -> { Attributes.VernacFlagLeaf (Attributes.FlagString v) } - | "=" ; v = IDENT -> { Attributes.VernacFlagLeaf (Attributes.FlagIdent v) } - | "(" ; a = my_attribute_list ; ")" -> { Attributes.VernacFlagList a } - | -> { Attributes.VernacFlagEmpty } ] - ] - ; - - attributes : [[ atts = LIST1 my_attribute SEP "," -> { atts } ]]; -END - -ARGUMENT EXTEND ltac_attributes - PRINTED BY { pr_attributes } - INTERPRETED BY { fun ist evd x -> match DAst.get x with - | Glob_term.GVar id -> - evd.Evd.sigma, - Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) - | _ -> assert false } - GLOBALIZED BY { fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t } - SUBSTITUTED BY { Detyping.subst_glob_constr (Global.env()) } - RAW_PRINTED BY { fun _ _ _ -> Ppconstr.pr_constr_expr env sigma } - GLOB_PRINTED BY { fun _ _ _ -> Printer.pr_glob_constr_env env sigma } -| [ ident(v) ] -> { (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) } -END - VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF | #[ atts = skip_attribute ] [ "Elpi" "Accumulate" "File" string_list(s) ] -> { EV.skip ~atts EV.accumulate_files s } @@ -384,12 +133,8 @@ VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([ { EV.run_in_program s } | [ "Elpi" "Query" qualified_name(p) elpi_string(s) ] -> { EV.run_in_program ~program:(snd p) s } -| [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } -> { - EV.export_command (snd p) - (Genarg.get_arg_tag wit_elpi_loc) - (Genarg.get_arg_tag wit_elpi_arg) - (Genarg.get_arg_tag wit_attributes) - } +| [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } -> + { EV.export_command (snd p) } | #[ atts = any_attribute ] [ "Elpi" qualified_name(p) elpi_arg_list(args) ] -> { EV.run_program (fst p) (snd p) ~atts args } diff --git a/src/elpi_plugin.mlpack b/src/elpi_plugin.mlpack index 604ec968f..02905c7e6 100644 --- a/src/elpi_plugin.mlpack +++ b/src/elpi_plugin.mlpack @@ -4,6 +4,7 @@ Coq_elpi_HOAS Coq_elpi_glob_quotation Coq_elpi_name_quotation Coq_elpi_arg_HOAS +Coq_elpi_arg_syntax Coq_elpi_builtins_HOAS Coq_elpi_builtins Coq_elpi_vernacular diff --git a/tests/test_API.v b/tests/test_API.v index 32f52330f..1667282f0 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -107,7 +107,7 @@ Elpi Accumulate lp:{{ main [indt-decl D] :- std.assert-ok! (coq.elaborate-indt-decl-skeleton D D1) "illtyped", coq.env.add-indt D1 _. - main [const-decl N (some BO) TYA] :- std.spy-do! [ + main [const-decl N (some BO) TYA] :- std.do! [ coq.arity->term TYA TY, std.assert-ok! (coq.elaborate-ty-skeleton TY _ TY1) "illtyped", std.assert-ok! (coq.elaborate-skeleton BO TY1 BO1) "illtyped", @@ -168,10 +168,21 @@ Elpi Query lp:{{ coq.say "hello world" }}. +Set Warnings "-elpi,-category". +Elpi Query lp:{{ + coq.warn "this is a generic warning". +}}. +Elpi Query lp:{{ + coq.warning "category" "name" "this is a warning with a name an category". +}}. +Set Warnings "+category". Elpi Query lp:{{ - coq.warn "this is a generic warning", coq.warning "category" "name" "this is a warning with a name an category". }}. +Fail Elpi Query lp:{{ + coq.warning "category" "name" "this is another warning with a name an category". +}}. +Set Warnings "elpi,category". (****** locate **********************************) @@ -248,7 +259,7 @@ Elpi Query lp:{{ coq.gref->id (const GR) S, Name is S ^ "_equal", coq.env.add-const Name BO TY @opaque! NGR, - coq.env.const-opaque? NGR, + coq.env.opaque? NGR, coq.env.const NGR none _, coq.say {coq.gref->id (const NGR)}, coq.env.const-body NGR (some BO), rex_match "add_equal" {coq.gref->id (const NGR)}. @@ -261,7 +272,7 @@ About add_equal. Elpi Query lp:{{ coq.locate "False" F, coq.env.add-axiom "myfalse" (global F) GR, - coq.env.const-opaque? GR, + coq.env.opaque? GR, coq.env.const GR none _, coq.env.const-body GR none, coq.say GR. @@ -299,7 +310,7 @@ Elpi Query lp:{{ field _ "prim_eq_proof" {{lp:f = lp:f :> bool}} _\ end-record)), @primitive! => coq.env.add-indt DECL GR, - coq.CS.canonical-projections GR [some _, some _]. + coq.env.projections GR [some _, some _]. }}. (* primitive records have eta *) @@ -316,12 +327,12 @@ Definition pc (r : prim_eq_class nat) := r.(prim_eq_f). Elpi Query lp:{{ coq.locate "pc" (const C), - coq.env.const C (some (fun _ _ r\ app[global _, _, r])) _ + coq.env.const C (some (fun _ _ r\ app[primitive _, r])) _ }}. Elpi Command primp. Elpi Accumulate lp:{{ - main [const-decl _ (some (fun _ _ r\ app[global _, _, r])) _]. + main [const-decl _ (some (fun _ _ r\ app[primitive _, r])) _]. }}. Elpi primp Definition pc (r : prim_eq_class nat) := r.(prim_eq_f). @@ -401,6 +412,7 @@ Elpi Query lp:{{ Elpi Query lp:{{ coq.locate-module "Datatypes" MP, coq.env.module MP L }}. Module X. + Unset Auto Template Polymorphism. Inductive i := . Definition d := i. Module Y. @@ -480,6 +492,7 @@ Print ITA. (* section *) Section SA. +Unset Auto Template Polymorphism. Variable a : nat. Inductive ind := K. Section SB. @@ -578,6 +591,14 @@ Elpi Query lp:{{coq.locate "RewriteRelation" GR, coq.TC.db-for GR L}}. Elpi Query lp:{{coq.locate "RewriteRelation" GR, coq.TC.class? GR}}. Elpi Query lp:{{coq.locate "True" GR, not(coq.TC.class? GR)}}. +Axiom C : Type -> Type. + +Elpi Query lp:{{ coq.TC.declare-class {{:gref C }} }}. + +Axiom c : C nat. + +Instance foox : C nat := c. + (****** CS **********************************) Structure eq := mk_eq { carrier : Type; eq_op : carrier -> carrier -> bool; _ : nat }. @@ -598,7 +619,7 @@ Elpi Query lp:{{ coq.CS.db L }}. Elpi Query lp:{{ coq.locate "eq" (indt I), - coq.CS.canonical-projections I [some P1, some P2, none], + coq.env.projections I [some P1, some P2, none], coq.locate "carrier" (const P1), coq.locate "eq_op" (const P2) }}. @@ -618,7 +639,7 @@ Elpi Query lp:{{ coq.locate "eq_op" P, coq.CS.db-for P _ [_,_] }}. Elpi Query lp:{{ coq.locate "W" W, coq.CS.db-for _ (cs-gref W) [_] }}. -Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "Z1" W, coq.CS.db-for P (cs-gref W) L, coq.say L, L = [cs-instance P (cs-gref W) {{myc1}}] }}. +Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "Z1" W, coq.CS.db-for P (cs-gref W) L, coq.say L, L = [cs-instance P (cs-gref W) {{:gref myc1}}] }}. Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "nat" W, coq.CS.db-for P (cs-gref W) [] }}. diff --git a/tests/test_API2.v b/tests/test_API2.v index 7dbba9db5..bab927678 100644 --- a/tests/test_API2.v +++ b/tests/test_API2.v @@ -50,3 +50,13 @@ Elpi Query lp:{{ coq.strategy.get X3 (level 123). }}. + +Axiom P : nat -> Prop. + +Elpi Command mode. +Elpi Query lp:{{ + coq.hints.add-mode {{:gref P }} "core" [mode-input], + coq.hints.add-mode {{:gref P }} "core" [mode-ground], + coq.hints.modes {{:gref P }} "core" M, + std.assert! (M = [[mode-ground],[mode-input]]) "wrong modes" +}}. diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index ad7b0d496..d2182b16f 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -24,7 +24,7 @@ Ltac foobar x := idtac x; eapply x. Elpi Tactic test2. Elpi Accumulate lp:{{ -solve (goal [decl T A B | _ ] _ _ _ _ as G) GS :- +solve (goal [decl T _ _ | _ ] _ _ _ _ as G) GS :- coq.ltac.call "foobar" [trm T] G GS, coq.say GS. @@ -88,7 +88,7 @@ Record foo A (B : A) : Type := { Elpi Query lp:{{ coq.locate "foo" (indt I), - coq.CS.canonical-projections I [some _, some _, some _]. + coq.env.projections I [some _, some _, some _]. }}. End record_attributes. @@ -103,7 +103,7 @@ Print foo1. Check foo1 _ _ _ _ : Type. Fail Check (foo1 _ _ _ _ _). Check a_k1 _ _ _ 3 _ : foo1 _ _ _ 3. - +Unset Auto Template Polymorphism. Inductive r (A : Type) (a : A) := R { f :> A -> A; g : A; p : a = g }. End inductive_nup. @@ -242,6 +242,35 @@ From Coq Require Import PrimFloat. Open Scope float_scope. Elpi primitive (2.4e13 + 1). +Module P. +Set Primitive Projections. + +Unset Auto Template Polymorphism. +Record foo (A : Type) := { p1 : nat; p2 : A }. +Definition x : foo bool := {| p1 := 3; p2 := false |}. + +Unset Primitive Projections. +End P. + +Elpi Command primitive_proj. +Elpi Accumulate lp:{{ + main [trm (global (indt I)), trm T, int N, trm V] :- + coq.env.projections I [_,_], + coq.env.primitive-projections I [some (pr _ 1), some (pr _ 2)], + T = app[primitive (proj P N),A], + coq.say P N A, + coq.say {coq.term->string T}, + coq.say {coq.term->string (primitive (proj P N))}, + {{:gref P.p1 }} = const C, + coq.env.const C BO _, + coq.say BO, + std.assert! (unwind {whd T []} V) "wrong value". +}}. +Elpi Typecheck. + +Elpi primitive_proj (P.foo) (P.p1 _ P.x) 1 (3%nat). +Elpi primitive_proj (P.foo) (P.p2 _ P.x) 2 (false). + (* glob of ifte *) Elpi Command ifte. diff --git a/tests/test_quotation.v b/tests/test_quotation.v index 83bb2defd..dfdd0efc3 100644 --- a/tests/test_quotation.v +++ b/tests/test_quotation.v @@ -56,6 +56,7 @@ X = {{ fun (r : nat) (p : forall y : nat, y = 0 :> nat) (q : bool) => lp:{{ {of Local Notation inlined_sub_rect := (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px). +Unset Auto Template Polymorphism. Record is_SUB (T : Type) (P : T -> bool) (sub_sort : Type) := SubType { val : sub_sort -> T; Sub : forall x, P x = true -> sub_sort; @@ -68,7 +69,7 @@ Structure ord u := Ord { oval : nat; prop : leq oval u = true }. Check fun u => SubType _ _ _ (oval u) _ inlined_sub_rect. -Elpi Query lp:{{ std.spy-do! [ +Elpi Query lp:{{ std.do! [ T = {{ fun u => SubType _ _ _ (oval u) _ inlined_sub_rect }}, std.assert-ok! (coq.elaborate-skeleton T _ T1) "does not typecheck", T1 = {{ fun u => SubType _ _ _ _ (lp:K u) _ }}, @@ -77,7 +78,7 @@ Elpi Query lp:{{ std.spy-do! [ }}. (* unfortunately the error message does not mention "unknown_inductive" *) -Fail Elpi Query lp:{{ std.spy-do! [ +Fail Elpi Query lp:{{ std.do! [ T = {{ fun u => SubType _ _ _ (oval u) _ inlined_sub_rect }}, std.assert-ok! (coq.typecheck T _) "does not typecheck", ] diff --git a/tests/test_tactic.v b/tests/test_tactic.v index 5b6f3ca7d..ba29cda69 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -281,20 +281,60 @@ Abort. (* ***************** *) -Elpi Tactic test_m. +Elpi Tactic test.m. Elpi Accumulate lp:{{ type type-arg open-tactic. - type-arg (goal _ _ _ _ [trm T] as G) GL :- + type-arg (goal _ _ _ _ [trm T|_] as G) GL :- refine T G GL. + type-arg (goal A B C D [X|R]) GL :- + coq.say "skip" X, + type-arg (goal A B C D R) GL. - msolve GL New :- + msolve GL New :- coq.say {attributes}, coq.ltac.all (coq.ltac.open type-arg) GL New. }}. Elpi Typecheck. Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). split; intro x. -all: elpi test_m (@eq_refl _ x). +all: elpi test.m (@eq_refl _ x). +Qed. + +Elpi Query lp:{{ + coq.notation.add-abbreviation-for-tactic "XX.xxx" "test.m" [int 1, str "33", trm {{bool}}] +}}. + +Print Grammar constr. + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (XX.xxx (@eq_refl _ x)). +Qed. + +Check forall xxx : nat, forall XX : bool, True. + +Elpi Export test.m. + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (test.m (@eq_refl _ x)). +Qed. + +Set Warnings "-non-reversible-notation". +Notation Foo pp := ltac:(elpi test.m (pp)). + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (Foo (@eq_refl _ x)). +Qed. + +Tactic Notation "Bar" open_constr(pp) := + elpi test.m (pp). +Notation Bar qq := ltac:(Bar (@eq_refl _ qq)). + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (Bar x). Qed.