diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 89d7abbef..d33740b6f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -16,7 +16,7 @@ jobs: strategy: matrix: coq_version: - - '8.12' + - '8.13' ocaml_version: - 'minimal' steps: @@ -26,26 +26,9 @@ jobs: opam_file: './coq-elpi.opam' coq_version: ${{ matrix.coq_version }} ocaml_version: ${{ matrix.ocaml_version }} - custom_script: | - startGroup Print opam config - opam config list; opam repo list; opam list - endGroup - startGroup Build dependencies - opam pin add -n -y -k path $PACKAGE $WORKDIR - opam update -y - opam install -y -j 4 $PACKAGE --deps-only - endGroup - startGroup List installed packages + after_script: | + startGroup "Test HB" + opam pin add coq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git --ignore-constraints-on=coq-elpi -y -j 4 opam list - endGroup - startGroup Build - opam install -y -v -j 4 $PACKAGE - opam list - endGroup - startGroup Test Hierarchy Builder - opam pin add coq-hierarchy-builder 'https://github.com/math-comp/hierarchy-builder.git' --ignore-constraints-on=coq-elpi -y -j 4 opam remove coq-hierarchy-builder -y - endGroup - startGroup Uninstallation test - opam remove $PACKAGE -y - endGroup + endGroup \ No newline at end of file diff --git a/Changelog.md b/Changelog.md index 984a89b0d..c09a4979f 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,14 @@ # Changelog +## [1.8.1] - 11-12-2020 + +Requires Elpi 1.12 and Coq 8.13. +### HOAS +- Illformed terms like `global (const X)` (which have no + representation in Coq) are now reported with a proper error message. + Whe passed to `coq.term->string`, instead of a fatal error, we pick for + the illformed sub term the `unknown_gref` special constant. + ## [1.8.0] - 29-11-2020 Requires Elpi 1.12 and Coq 8.12. diff --git a/coq-elpi.opam b/coq-elpi.opam index c1aec25b0..d3c800655 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -12,7 +12,7 @@ build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ] install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ] depends: [ "elpi" {>= "1.12.0" & < "1.13.0~"} - "coq" {>= "8.12" & < "8.13~" } + "coq" {>= "8.13" & < "8.14~" } ] tags: [ "logpath:elpi" ] synopsis: "Elpi extension language for Coq" diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index ef2e87895..853c8cfa0 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -78,6 +78,7 @@ type options = { local : bool option; deprecation : Deprecation.t option; primitive : bool option; + failsafe : bool; (* don't fail, e.g. we are trying to print a term *) } let default_options = { @@ -85,6 +86,7 @@ let default_options = { local = None; deprecation = None; primitive = None; + failsafe = false; } type 'a coq_context = { @@ -268,7 +270,7 @@ let abbreviation = } module GROrd = struct - include Names.GlobRef.Ordered + include Names.GlobRef.CanOrd let show x = Pp.string_of_ppcmds (Printer.pr_global x) let pp fmt x = Format.fprintf fmt "%s" (show x) end @@ -282,10 +284,17 @@ let in_elpi_gr ~depth s r = assert (gl = []); E.mkApp globalc t [] -let in_coq_gref ~depth s t = - let s, t, gls = gref.API.Conversion.readback ~depth s t in - assert(gls = []); - s, t +let in_coq_gref ~depth ~origin ~failsafe s t = + try + let s, t, gls = gref.API.Conversion.readback ~depth s t in + assert(gls = []); + s, t + with API.Conversion.TypeErr _ -> + if failsafe then + s, Coqlib.lib_ref "elpi.unknown_gref" + else + err Pp.(str "The term " ++ str(pp2string (P.term depth) origin) ++ + str " cannot be represented in Coq since its gref part is illformed") let mpin, ismp, mpout, modpath = let { CD.cin; isc; cout }, x = CD.declare { @@ -429,8 +438,8 @@ let show_coq_engine = Format.asprintf "%a" pp_coq_engine let from_env env = from_env_sigma env (Evd.from_env env) let from_env_keep_univ_of_sigma env sigma0 = - let sigma = Evd.update_sigma_env sigma0 env in - let sigma = Evd.from_ctx (UState.demote_global_univs env (Evd.evar_universe_context sigma)) in + let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in + let sigma = Evd.from_ctx (UState.demote_global_univs env uctx) in from_env_sigma env sigma let init () = from_env (Global.env ()) @@ -617,6 +626,7 @@ let get_options ~depth hyps state = local = locality @@ get_string_option "coq:locality"; deprecation = deprecation @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:deprecation"; primitive = get_bool_option "coq:primitive"; + failsafe = false; } let mk_coq_context ~options state = @@ -792,7 +802,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t = check_univ_inst (EC.EInstance.kind sigma i); state, in_elpi_gr ~depth state (G.ConstructRef construct) | C.Case((*{ C.ci_ind; C.ci_npar; C.ci_cstr_ndecls; C.ci_cstr_nargs }*)_, - rt,t,bs) -> + rt,_,t,bs) -> let state, t = aux ~depth env state t in let state, rt = aux ~depth env state rt in let state, bs = CArray.fold_left_map (aux ~depth env) state bs in @@ -811,6 +821,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t = | 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.Array _ -> nYI "HOAS for persistent arrays" in if debug () then Feedback.msg_debug Pp.(str"term2lp: depth=" ++ int depth ++ @@ -1096,7 +1107,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals state, EC.mkSort u, gsl (* constants *) | E.App(c,d,[]) when globalc == c -> - let state, gr = in_coq_gref ~depth state d in + let state, gr = in_coq_gref ~depth ~origin:t ~failsafe:coq_ctx.options.failsafe state d in begin match gr with | G.VarRef x -> state, EC.mkVar x, [] | G.ConstRef x -> state, EC.mkConst x, [] @@ -1183,7 +1194,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals match ind with | Some ind -> Inductiveops.make_case_info (get_global_env state) ind Sorts.Relevant C.RegularStyle | None -> default_case_info () in - state, EC.mkCase (ci,rt,t,Array.of_list bt), gl1 @ gl2 @ gl3 + state, EC.mkCase (ci,rt,C.NoInvert,t,Array.of_list bt), gl1 @ gl2 @ gl3 (* fix *) | E.App(c,name,[rno;ty;bo]) when fixc == c -> @@ -2062,7 +2073,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t = mind_entry_inds = [oe]; mind_entry_universes = Monomorphic_entry (Evd.universe_context_set sigma); - mind_entry_cumulative = false; + mind_entry_variance = None; mind_entry_private = None; }, i_impls, kimpls, List.(concat (rev gls_rev)) in diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index bf96fdb10..ac303cb0e 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -20,6 +20,7 @@ type options = { local : bool option; deprecation : Deprecation.t option; primitive : bool option; + failsafe : bool; (* readback is resilient to illformed terms *) } type 'a coq_context = { diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 89e9299f5..e859cece5 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -85,7 +85,7 @@ let add_universe_constraint state c = | Univ.UniverseInconsistency p -> Feedback.msg_debug (Univ.explain_universe_inconsistency - UnivNames.pr_with_global_universes p); + UnivNames.(pr_with_global_universes empty_binders) p); raise Pred.No_clause | Evd.UniversesDiffer | UState.UniversesDiffer -> Feedback.msg_debug Pp.(str"UniversesDiffer"); @@ -176,6 +176,14 @@ let term = { readback = lp2constr; embed = constr2lp; } +let failsafe_term = { + CConv.ty = Conv.TyName "term"; + pp_doc = (fun fmt () -> Format.fprintf fmt "A Coq term containing evars"); + pp = (fun fmt t -> Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_econstr_env (Global.env()) Evd.empty t))); + readback = (fun ~depth coq_ctx csts s t -> lp2constr ~depth { coq_ctx with options = { coq_ctx.options with failsafe = true }} csts s t); + embed = constr2lp; +} + let proof_context : (full coq_context, API.Data.constraints) CConv.ctx_readback = fun ~depth hyps constraints state -> let state, proof_context, _, gls = get_current_env_sigma ~depth hyps constraints state in @@ -204,7 +212,10 @@ let closed_ground_term = { let term_skeleton = { CConv.ty = Conv.TyName "term"; pp_doc = (fun fmt () -> Format.fprintf fmt "A Coq term containing holes"); - pp = (fun fmt t -> Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_glob_constr_env (Global.env()) t))); + pp = (fun fmt t -> + let env = Global.env() in + let sigma = Evd.from_env env in + Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_glob_constr_env env sigma t))); readback = lp2skeleton; embed = (fun ~depth _ _ _ _ -> assert false); } @@ -310,13 +321,19 @@ let cs_pattern = doc = "Pattern for canonical values"; pp = (fun fmt -> function | Const_cs x -> Format.fprintf fmt "Const_cs %s" "" + | Proj_cs x -> Format.fprintf fmt "Proj_cs %s" "" | Prod_cs -> Format.fprintf fmt "Prod_cs" | Sort_cs _ -> Format.fprintf fmt "Sort_cs" | Default_cs -> Format.fprintf fmt "Default_cs"); constructors = [ K("cs-gref","",A(gref,N), - B (fun x -> Const_cs x), - M (fun ~ok ~ko -> function Const_cs x -> ok x | _ -> ko ())); + B (function + | GlobRef.ConstructRef _ | GlobRef.IndRef _ | GlobRef.VarRef _ as x -> Const_cs x + | GlobRef.ConstRef cst as x -> + match Recordops.find_primitive_projection cst with + | None -> Const_cs x + | Some p -> Proj_cs p), + M (fun ~ok ~ko -> function Const_cs x -> ok x | Proj_cs p -> ok (GlobRef.ConstRef (Projection.Repr.constant p)) | _ -> ko ())); K("cs-prod","",N, B Prod_cs, M (fun ~ok ~ko -> function Prod_cs -> ok | _ -> ko ())); @@ -518,8 +535,8 @@ let attribute_value = let open API.AlgebraicData in let open Attributes in let o pp = (fun fmt a -> Format.fprintf fmt "TODO"); constructors = [ K("leaf","",A(B.string,N), - B (fun s -> if s = "" then VernacFlagEmpty else VernacFlagLeaf s), - M (fun ~ok ~ko -> function VernacFlagEmpty -> ok "" | VernacFlagLeaf x -> ok x | _ -> ko ())); + B (fun s -> if s = "" then VernacFlagEmpty else VernacFlagLeaf (FlagString s)), + M (fun ~ok ~ko -> function VernacFlagEmpty -> ok "" | VernacFlagLeaf (FlagString x | FlagIdent x) -> ok x | _ -> ko ())); K("node","",C((fun self -> !> (B.list (attribute (!< self)))),N), B (fun l -> VernacFlagList l), M (fun ~ok ~ko -> function VernacFlagList l -> ok l | _ -> ko ()) @@ -592,11 +609,6 @@ let gr2path state gr = | Names.GlobRef.IndRef _ | Names.GlobRef.ConstructRef _ -> nYI "mutual inductive (make-derived...)" -(* See https://github.com/coq/coq/pull/12759 , the system asserts no evars - and the allow_evars flag is gone! *) -let hack_prune_all_evars sigma = - Evd.from_ctx (Evd.evar_universe_context sigma) - let coq_builtins = let open API.BuiltIn in let open Pred in @@ -993,7 +1005,7 @@ Supported attributes: ComAssumption.declare_variable false ~kind (EConstr.to_constr sigma ty) impargs Glob_term.Explicit variable; GlobRef.VarRef(Id.of_string id), Univ.Instance.empty end else - ComAssumption.declare_axiom false ~local:Declare.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty) + ComAssumption.declare_axiom false ~local:Locality.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty) (uentry, ubinders) impargs Declaremods.NoInline variable in @@ -1012,13 +1024,11 @@ Supported attributes: let udecl = UState.default_univ_decl in let kind = Decls.(IsDefinition Definition) in let scope = if local - then Declare.Discharge - else Declare.Global Declare.ImportDefaultBehavior in - let gr = DeclareDef.declare_definition - ~name:(Id.of_string id) ~scope ~kind ~impargs:[] - ~poly:false ~udecl ~opaque:(opaque = Given true) ~types ~body - (hack_prune_all_evars sigma) - in + then Locality.Discharge + else Locality.(Global ImportDefaultBehavior) in + let cinfo = Declare.CInfo.make ~name:(Id.of_string id) ~typ:types ~impargs:[] () in + let info = Declare.Info.make ~scope ~kind ~poly:false ~udecl () in + let gr = Declare.declare_definition ~cinfo ~info ~opaque:(opaque = Given true) ~body sigma in state, !: (global_constant_of_globref gr), []))), DocAbove); @@ -1041,7 +1051,7 @@ Supported attributes: | Some (primitive,field_specs) -> (* record: projection... *) let names, flags = List.(split (map (fun { name; is_coercion; is_canonical } -> name, - { Record.pf_subclass = is_coercion ; pf_canonical = is_canonical }) + { Record.Internal.pf_subclass = is_coercion ; pf_canonical = is_canonical }) field_specs)) in let is_implicit = List.map (fun _ -> []) names in let cstr = (ind,1) in @@ -1049,7 +1059,7 @@ Supported attributes: let k_ty = List.(hd (hd me.mind_entry_inds).mind_entry_lc) in let fields_as_relctx = Term.prod_assum k_ty in let kinds, sp_projs = - Record.declare_projections ind ~kind:Decls.Definition + Record.Internal.declare_projections ind ~kind:Decls.Definition (Evd.univ_entry ~poly:false sigma) (Names.Id.of_string "record") flags is_implicit fields_as_relctx @@ -1062,7 +1072,7 @@ Supported attributes: s_EXPECTEDPARAM = npars; } in - Record.declare_structure_entry struc; + Record.Internal.declare_structure_entry struc; end; state, !: ind, []))), DocAbove); @@ -1426,8 +1436,8 @@ Supported attributes: (fun gref imps ~depth {options} _ -> on_global_state "coq.arguments.set-implicit" (fun state -> let local = options.local <> Some false in let imps = imps |> List.(map (map (function - | Unspec -> Glob_term.Explicit - | Given x -> x))) in + | Unspec -> Anonymous, Glob_term.Explicit + | Given x -> Anonymous, x))) in Impargs.set_implicits local gref imps; state, (), []))), DocAbove); @@ -2022,7 +2032,7 @@ coq.id->name S N :- coq.string->name S N. DocAbove); MLCode(Pred("coq.term->string", - CIn(term,"T", + CIn(failsafe_term,"T", Out(B.string, "S", Full(proof_context, "prints a term T to a string S using Coq's pretty printer"))), (fun t _ ~depth proof_context constraints state -> diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index d1f37f02a..c349b5ee9 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -90,7 +90,7 @@ let type_gen = ref 0 let rec gterm2lp ~depth state x = if debug () then Feedback.msg_debug Pp.(str"gterm2lp: depth=" ++ int depth ++ - str " term=" ++Printer.pr_glob_constr_env (get_global_env state) x); + str " term=" ++Printer.pr_glob_constr_env (get_global_env state) (get_sigma state) x); match (DAst.get x) (*.CAst.v*) with | GRef(GlobRef.ConstRef p,_ul) when Recordops.is_primitive_projection p -> let p = Option.get @@ Recordops.find_primitive_projection p in @@ -109,8 +109,8 @@ let rec gterm2lp ~depth state x = let state, s = API.RawQuery.mk_Arg state ~name:(Printf.sprintf "type_%d" !type_gen) ~args:[] in state, in_elpi_flex_sort s | GSort(UNamed [name,0]) -> - let env = get_global_env state in - state, in_elpi_sort (Sorts.sort_of_univ @@ Univ.Universe.make @@ Pretyping.interp_known_glob_level (Evd.from_env env) name) + let env = get_global_env state in + state, in_elpi_sort (Sorts.sort_of_univ @@ Univ.Universe.make @@ Pretyping.known_glob_level (Evd.from_env env) name) | GSort(_) -> nYI "(glob)HOAS for Type@{i j}" | GProd(name,_,s,t) -> @@ -302,6 +302,7 @@ let rec gterm2lp ~depth state x = | GRec _ -> nYI "(glob)HOAS mutual/non-struct fix" | GInt i -> in_elpi_uint63 ~depth state i | GFloat f -> in_elpi_float64 ~depth state f + | GArray _ -> nYI "(glob)HOAS persistent arrays" ;; let coq_quotation ~depth state _loc src = diff --git a/src/coq_elpi_goal_HOAS.ml b/src/coq_elpi_goal_HOAS.ml index 1fda4a176..fcaec6418 100644 --- a/src/coq_elpi_goal_HOAS.ml +++ b/src/coq_elpi_goal_HOAS.ml @@ -68,7 +68,7 @@ let rec list_map_acc f acc = function let acc, xs = list_map_acc f acc xs in acc, x :: xs -let contract_params env name params t = +let contract_params env sigma name params t = let open Glob_term in let loc = Option.map Coq_elpi_utils.of_coq_loc t.CAst.loc in let rec contract params args = @@ -85,7 +85,7 @@ let contract_params env name params t = | GHole _ -> contract ps rest | _ -> Coq_elpi_utils.err ?loc Pp.(str "Inductive type "++ Names.Id.print name ++ str" is not applied to parameter " ++ Names.Id.print pname ++ - str" but rather " ++ Printer.pr_glob_constr_env env arg) + str" but rather " ++ Printer.pr_glob_constr_env env sigma arg) end in let rec aux x = @@ -102,7 +102,7 @@ let contract_params env name params t = let ginductive2lp ~depth state { finiteness; name; arity; params; nuparams; constructors } = let open Coq_elpi_glob_quotation in let space, indt_name = name in - let contract state x = contract_params (get_global_env state) indt_name params x in + let contract state x = contract_params (get_global_env state) (get_sigma state) indt_name params x in let do_constructor ~depth state (name, ty) = let state, ty = do_params nuparams (do_arity (contract state ty)) ~depth state in state, in_elpi_indtdecl_constructor (Name.Name name) ty diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 8c5ebbc1a..b4ff6ea50 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -62,7 +62,7 @@ let _pp_qualified_name fmt l = Format.fprintf fmt "%s" (String.concat "." l) type expr_record_decl = { name : qualified_name; parameters : Constrexpr.local_binder_expr list; - sort : Glob_term.glob_sort option; + sort : Constrexpr.sort_expr option; constructor : Names.Id.t option; fields : (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) list } @@ -143,7 +143,7 @@ let intern_global_constr_ty { Ltac_plugin.Tacintern.genv = env } ?(intern_env=Co Constrintern.intern_gen Pretyping.IsType env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t let intern_global_context { Ltac_plugin.Tacintern.genv = env } ?(intern_env=Constrintern.empty_internalization_env) ctx = - Constrintern.intern_context env intern_env ctx + Constrintern.intern_context env ~bound_univs:UnivNames.empty_binders intern_env ctx let subst_global_constr s t = Detyping.subst_glob_constr (Global.env()) s t let subst_global_decl s (n,bk,ot,t) = @@ -164,11 +164,11 @@ let intern_record_decl glob_sign { name; sort; parameters; constructor; fields } let arity = intern_global_constr_ty glob_sign_params @@ CAst.make sort in let _, fields = List.fold_left (fun (gs,acc) -> function - | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,x), { Vernacexpr.rf_subclass = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } -> + | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,bl,x), { Vernacexpr.rf_subclass = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } -> if nots <> [] then Coq_elpi_utils.nYI "notation in record fields"; if pr <> None then Coq_elpi_utils.nYI "priority in record fields"; - if inst = Some false then Coq_elpi_utils.nYI "instance :>> flag in record fields"; - let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = inst <> None; name } in + let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = inst <> Vernacexpr.NoInstance; name } in + let x = if bl = [] then x else Constrexpr_ops.mkCProdN bl x in push_name gs fn.CAst.v, (intern_global_constr_ty gs x, atts) :: acc | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr") (glob_sign_params,[]) fields in diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index f093b8b87..cb63d1a0c 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -37,7 +37,7 @@ val print : qualified_name -> string list -> unit type expr_record_decl = { name : qualified_name; parameters : Constrexpr.local_binder_expr list; - sort : Glob_term.glob_sort option; + sort : Constrexpr.sort_expr option; constructor : Names.Id.t option; fields : (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) list } diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 66dfe1e35..e3f53ba3e 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -158,7 +158,10 @@ let pr_glob_constr_and_expr = function let env = Global.env () in let sigma = Evd.from_env env in Ppconstr.pr_constr_expr env sigma c - | (c, None) -> Printer.pr_glob_constr_env (Global.env ()) c + | (c, None) -> + let env = Global.env () in + let sigma = Evd.from_env env in + Printer.pr_glob_constr_env env sigma c let pp_elpi_arg _ _ _ = EV.pr_arg (fun (_,x) -> pr_glob_constr_and_expr x) (fun (_,r) -> Coq_elpi_goal_HOAS.pr_glob_record_decl r) (fun (_,r) -> Coq_elpi_goal_HOAS.pr_glob_indt_decl r) (fun (_,r) -> Coq_elpi_goal_HOAS.pr_glob_constant_decl r) (fun (_,x) -> Coq_elpi_goal_HOAS.pr_glob_context_decl x) let pp_glob_elpi_arg _ _ _ = EV.pr_arg pr_glob_constr_and_expr Coq_elpi_goal_HOAS.pr_glob_record_decl Coq_elpi_goal_HOAS.pr_glob_indt_decl Coq_elpi_goal_HOAS.pr_glob_constant_decl Coq_elpi_goal_HOAS.pr_glob_context_decl diff --git a/tests/test_API.v b/tests/test_API.v index a32896441..1ba170461 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -140,6 +140,26 @@ Elpi Query lp:{{ }}. +Elpi Tactic test. +Elpi Accumulate lp:{{ +solve _ _ _ :- + coq.term->string X S, + X = global (indc Y), + coq.say S. +}}. +Goal True. +Fail elpi test. +Abort. + +Elpi Tactic test2. +Elpi Accumulate lp:{{ +solve _ _ _ :- + coq.term->string (global (indc Y)) S, + coq.say S. +}}. +Goal True. +elpi test2. +Abort. End elab. (****** say *************************************) diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index 48029ee21..b34d07d2c 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -86,7 +86,7 @@ Elpi declarations Record foo A (B : A) : Type := { a of A & A : A; z (a : A) :> B = B -> A; -#[canonical(false)] +#[canonical=no] x (w := 3) : forall x, a x x = x; }. @@ -223,4 +223,4 @@ Elpi primitive (2000000003333002 + 1). From Coq Require Import Floats. Open Scope float_scope. -Elpi primitive (2.4e13 + 1). \ No newline at end of file +Elpi primitive (2.4e13 + 1). diff --git a/theories/elpi.v b/theories/elpi.v index 5c650130f..aa5178d69 100644 --- a/theories/elpi.v +++ b/theories/elpi.v @@ -19,6 +19,14 @@ Register hole as elpi.hole. Inductive unknown_inductive : Prop := unknown_constructor. Register unknown_inductive as elpi.unknown_inductive. +(* Special global constant used to signal a datum of type gref which + has no corresponding Coq global reference. This typically signals + an error: a term like (global (const X)) has no meaning in Coq, X must + be an actual name. +*) +Inductive unknown_gref : Prop := . +Register unknown_gref as elpi.unknown_gref. + (* Common constants available inside Coq's syntax {{ ... lib: ... }} *) Register Coq.Init.Logic.eq as elpi.eq. Register Coq.Init.Logic.eq_refl as elpi.erefl.