Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix issue #1042 MetaCoq Run does not support evars. #1068

Merged
merged 1 commit into from
Mar 15, 2024
Merged

Fix issue #1042 MetaCoq Run does not support evars. #1068

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 10 additions & 9 deletions template-coq/src/g_template_coq.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,14 +51,14 @@ let to_ltac_val c = Tacinterp.Value.of_constr c
let run_template_program ~pm env evm ~poly pgm =
Run_template_monad.run_template_program_rec ~poly (fun ~st _ _ _ -> st) ~st:pm env (evm, pgm)

let fresh_env () =
let fresh_env () =
let env = Global.env () in
let sigma = Evd.from_env env in
env, sigma

let to_constr_evars sigma c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c
}

(** ********* Commands ********* *)

VERNAC COMMAND EXTEND TemplateCoq_Test_Quote CLASSIFIED AS QUERY STATE program
Expand All @@ -76,7 +76,7 @@ VERNAC COMMAND EXTEND TemplateCoq_Quote_Definition CLASSIFIED AS SIDEFF STATE pr
{ let (env, evm) = fresh_env () in
let (evm, def) = Constrintern.interp_open_constr env evm def in
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmQuoteDefinition) in
let pgm = Constr.mkApp (EConstr.to_constr evm pgm, [|Constr_quoter.quote_ident name; Constr.mkRel 0;
let pgm = Constr.mkApp (EConstr.to_constr evm pgm, [|Constr_quoter.quote_ident name; Constr.mkRel 0;
to_constr_evars evm def|]) in
run_template_program env evm ~poly pgm }
END
Expand All @@ -98,7 +98,7 @@ VERNAC COMMAND EXTEND TemplateCoq_Quote_Recursively_Definition CLASSIFIED AS SID
{ let (env, evm) = fresh_env () in
let (evm, def) = Constrintern.interp_open_constr env evm def in
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmQuoteRecDefinition) in
let pgm = Constr.mkApp (EConstr.to_constr evm pgm, [|Constr_quoter.quote_ident name; Constr.mkRel 0;
let pgm = Constr.mkApp (EConstr.to_constr evm pgm, [|Constr_quoter.quote_ident name; Constr.mkRel 0;
to_constr_evars evm def|]) in
run_template_program env evm ~poly pgm }
END
Expand All @@ -108,7 +108,7 @@ VERNAC COMMAND EXTEND TemplateCoq_Test_Unquote CLASSIFIED AS QUERY STATE program
{ let (env, evm) = fresh_env () in
let (evm, def) = Constrintern.interp_open_constr env evm def in
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmTestUnquote) in
let pgm = Constr.mkApp (EConstr.to_constr evm pgm,
let pgm = Constr.mkApp (EConstr.to_constr evm pgm,
[|to_constr_evars evm def|]) in
run_template_program env evm ~poly pgm }
END
Expand All @@ -119,7 +119,7 @@ VERNAC COMMAND EXTEND TemplateCoq_Make_Definition CLASSIFIED AS SIDEFF STATE pro
let (evm, def) = Constrintern.interp_open_constr env evm def in
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmMkDefinition) in
let pgm = Constr.mkApp (EConstr.to_constr evm pgm,
[|Constr_quoter.quote_ident name;
[|Constr_quoter.quote_ident name;
to_constr_evars evm def|]) in
run_template_program env evm ~poly pgm }
END
Expand All @@ -129,16 +129,17 @@ VERNAC COMMAND EXTEND TemplateCoq_Make_Inductive CLASSIFIED AS SIDEFF STATE prog
{ let (env, evm) = fresh_env () in
let (evm, def) = Constrintern.interp_open_constr env evm def in
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmMkInductive) in
let pgm = Constr.mkApp (EConstr.to_constr evm pgm,
let pgm = Constr.mkApp (EConstr.to_constr evm pgm,
[|Constr_quoter.quote_bool false; to_constr_evars evm def|]) in
run_template_program env evm ~poly pgm }
END

VERNAC COMMAND EXTEND TemplateCoq_Run_Template_Program CLASSIFIED AS SIDEFF STATE program
| #[ poly = polymorphic ] [ "MetaCoq" "Run" constr(def) ] ->
{ let (env, evm) = fresh_env () in
let (evm, def) = Constrintern.interp_open_constr env evm def in
let pgm = to_constr_evars evm def in
let (pgm, ctx) = Constrintern.interp_constr env evm def in
let evm = Evd.from_ctx ctx in
let pgm = EConstr.to_constr ~abort_on_undefined_evars:true evm pgm in
run_template_program env evm ~poly pgm }
END

Expand Down
20 changes: 10 additions & 10 deletions template-coq/src/run_template_monad.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,12 +70,12 @@ let rec unquote_pos trm : int =
let (h,args) = app_full trm [] in
match args with
[x] ->
if constr_equall h cposI then
if constr_equall h cposI then
(2 * unquote_pos x + 1)
else if constr_equall h cposO then
(2 * unquote_pos x)
else not_supported_verb trm "unquote_pos"
| [] ->
| [] ->
if constr_equall h cposzero then 1
else not_supported_verb trm "unquote_pos"
| _ -> bad_term_verb trm "unquote_pos"
Expand All @@ -87,7 +87,7 @@ let unquote_Z trm : int =
if constr_equall h cZpos then unquote_pos x
else if constr_equall h cZneg then - unquote_pos x
else not_supported_verb trm "unquote_pos"
| [] ->
| [] ->
if constr_equall h cZ0 then 0
else not_supported_verb trm "unquote_pos"
| _ -> bad_term_verb trm "unquote_pos"
Expand All @@ -96,12 +96,12 @@ let unquote_constraint_type trm (* of type constraint_type *) : constraint_type
let (h,args) = app_full trm [] in
match args with
[x] ->
if constr_equall h tunivLe then
if constr_equall h tunivLe then
let n = unquote_Z x in
if n = 0 then Univ.Le
else Univ.Lt
else not_supported_verb trm "unquote_constraint_type"
| [] ->
| [] ->
if constr_equall h tunivEq then Univ.Eq
else not_supported_verb trm "unquote_constraint_type"
| _ -> bad_term_verb trm "unquote_constraint_type"
Expand Down Expand Up @@ -176,7 +176,7 @@ let denote_variance trm (* of type Variance *) : Variance.t =
else if constr_equall trm cInvariant then Variance.Invariant
else not_supported_verb trm "denote_variance"


let denote_variance evm trm (* of type Variance.t list *) : _ * Variance.t array =
let variances = List.map denote_variance (unquote_list trm) in
evm, Array.of_list variances
Expand Down Expand Up @@ -243,9 +243,9 @@ let unquote_one_inductive_entry env evm trm (* of type one_inductive_entry *) :
let map_option f o =
match o with
| Some x -> Some (f x)
| None -> None
| None -> None

let denote_decl env evm d =
let denote_decl env evm d =
let (h, args) = app_full d [] in
if constr_equall h tmkdecl then
match args with
Expand All @@ -262,7 +262,7 @@ let denote_decl env evm d =

let denote_context env evm ctx =
fold_env_evm_right denote_decl env evm (unquote_list ctx)

let unquote_mutual_inductive_entry env evm trm (* of type mutual_inductive_entry *) : _ * _ * Entries.mutual_inductive_entry =
let (h,args) = app_full trm [] in
if constr_equall h tBuild_mutual_inductive_entry then
Expand Down Expand Up @@ -301,7 +301,7 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool
let evm' = Evd.from_env env in
let evm', ctx, mind = unquote_mutual_inductive_entry env evm' mind in
let () = DeclareUctx.declare_universe_context ~poly:false ctx in
let evm, mind =
let evm, mind =
if infer_univs then
let ctx, mind = Tm_util.RetypeMindEntry.infer_mentry_univs env evm' mind in
debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.pr_universe_context_set (Level.pr) ctx));
Expand Down
28 changes: 28 additions & 0 deletions test-suite/issue1042.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
From MetaCoq.Utils Require Import utils.
From MetaCoq.Template Require Import All.
Import MCMonadNotation.


(*Exemple with a typing error*)
Definition ident_term (a : term) : term := a.

Definition quote_inductive {X}(inductive:X): TemplateMonad _ :=
quote <- tmQuote inductive;;
tmReturn quote.

Inductive tm : Set := .

Definition d1 : TemplateMonad unit.
(* Set Debug "backtrace". *)
Fail MetaCoq Run(
quote <- quote_inductive tm;;
constructor <- ident_term quote;;
tmPrint constructor)
.
Fail run_template_program (quote <- quote_inductive tm;;
constructor <- ident_term quote;;
tmPrint constructor) ltac:(fun x => idtac).
Fail refine (
quote <- quote_inductive tm;;
constructor <- ident_term quote;;
tmPrint constructor).
Loading