Merge pull request #1068 from MetaCoq/fix-1042

Fix issue #1042 MetaCoq Run does not support evars.

Author: mattam82

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,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
 

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));

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).