diff --git a/template-coq/src/g_template_coq.mlg b/template-coq/src/g_template_coq.mlg index 7639ed088..87d9acf3f 100644 --- a/template-coq/src/g_template_coq.mlg +++ b/template-coq/src/g_template_coq.mlg @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -129,7 +129,7 @@ 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 @@ -137,8 +137,9 @@ 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 diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml index 189cc834e..05d1629ef 100644 --- a/template-coq/src/run_template_monad.ml +++ b/template-coq/src/run_template_monad.ml @@ -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" @@ -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" @@ -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" @@ -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 @@ -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 @@ -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 @@ -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)); diff --git a/test-suite/issue1042.v b/test-suite/issue1042.v new file mode 100644 index 000000000..819c11f0b --- /dev/null +++ b/test-suite/issue1042.v @@ -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). \ No newline at end of file