support for Extractable.tmDependencies.

MetaCoq · May 14, 2019 · 9979d60 · 9979d60
1 parent 8827e89
commit 9979d60
Show file tree

Hide file tree

Showing 8 changed files with 42 additions and 15 deletions.
diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml
@@ -82,10 +82,6 @@ struct
       with Not_found ->
         CErrors.user_err ~hdr:"unquote_level" (str ("Level "^s^" is not a declared level."))
 
-
-
-
-
   let unquote_level evm trm (* of type level *) : Evd.evar_map * Univ.Level.t =
     let (h,args) = app_full trm [] in
     if Constr.equal h lProp then

diff --git a/template-coq/src/constr_quoted.ml b/template-coq/src/constr_quoted.ml
@@ -210,6 +210,10 @@ struct
     else
       not_supported_verb trm "unquote_list"
 
+  let rec quote_list ty = function
+      [] -> Constr.mkApp (c_nil, [| ty |])
+    | l::ls -> Constr.mkApp (c_cons, [| ty ; l ; quote_list ty ls |])
+
   (* Unquote Coq nat to OCaml int *)
   let rec unquote_nat trm =
     let (h,args) = app_full trm [] in

diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
@@ -114,6 +114,11 @@ let tmLemma (nm : ident) ?poly:(poly=false)(ty : term) : kername tm =
         | _ -> failwith "Evd.fresh_global did not return a Const") in
     ignore (Obligations.add_definition nm ~term:c cty ctx ~kind ~hook obls)
 
+let tmInductive (mi : mutual_inductive_entry) : unit tm =
+  fun env evd success _fail ->
+    ignore (ComInductive.declare_mutual_inductive_with_eliminations mi Names.Id.Map.empty []) ;
+    success (Global.env ()) evd ()
+
 let tmFreshName (nm : ident) : ident tm =
   fun env evd success _fail ->
     let name' =
@@ -134,6 +139,9 @@ let tmAboutString (s : string) : global_reference option tm =
     let q = Libnames.make_qualid dp nm in
     tmAbout q env evd success fail
 
+let tmDependencies (gr : global_reference) ?bypass : global_reference list tm =
+  failwith "not implemented"
+
 let tmCurrentModPath : Names.ModPath.t tm =
   fun env evd success _fail ->
     let mp = Lib.current_mp () in success env evd mp
@@ -161,11 +169,6 @@ let tmQuoteConstant (kn : kername) (bypass : bool) : constant_entry tm =
     with
       Not_found -> fail Pp.(str "constant not found " ++ Names.KerName.print kn)
 
-let tmInductive (mi : mutual_inductive_entry) : unit tm =
-  fun env evd success _fail ->
-    ignore (ComInductive.declare_mutual_inductive_with_eliminations mi Names.Id.Map.empty []) ;
-    success (Global.env ()) evd ()
-
 let tmExistingInstance (kn : kername) : unit tm =
   fun env evd success _fail ->
     (* note(gmm): this seems wrong. *)

diff --git a/template-coq/src/plugin_core.mli b/template-coq/src/plugin_core.mli
@@ -40,18 +40,19 @@ val tmEval : reduction_strategy -> term -> term tm
 val tmDefinition : ident -> ?poly:bool -> term option -> term -> kername tm
 val tmAxiom : ident -> ?poly:bool -> term -> kername tm
 val tmLemma : ident -> ?poly:bool -> term -> kername tm
+val tmInductive : mutual_inductive_entry -> unit tm
 
 val tmFreshName : ident -> ident tm
 
 val tmAbout : qualid -> global_reference option tm
 val tmAboutString : string -> global_reference option tm
+val tmDependencies : global_reference -> ?bypass:bool -> global_reference list tm
+
 val tmCurrentModPath : Names.ModPath.t tm
 
 val tmQuoteInductive : kername -> (Names.MutInd.t * mutual_inductive_body) option tm
 val tmQuoteUniverses : UGraph.t tm
 val tmQuoteConstant : kername -> bool -> constant_entry tm
 
-val tmInductive : mutual_inductive_entry -> unit tm
-
 val tmExistingInstance : kername -> unit tm
 val tmInferInstance : term -> term option tm
diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
@@ -444,3 +444,14 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
     let evm,trm = denote_term evm (reduce_all env evm trm) in
     Plugin_core.run (Plugin_core.tmPrint trm) env evm
       (fun env evm _ -> k (env, evm, unit_tt))
+  | TmDependencies (trm, bypass) ->
+    let trm = Constr_denoter.CoqLiveDenoter.unquote_kn (reduce_all env evm trm) in
+    let bypass = Constr_quoted.ConstrQuoted.unquote_bool (reduce_all env evm bypass) in
+    Plugin_core.run Plugin_core.(tmBind (tmAbout trm) (function
+                                       None -> tmFail Pp.(str "Failed to resolve kernel name " ++ Libnames.pr_qualid trm)
+                                     | Some gr -> tmDependencies gr ~bypass)) env evm
+      (fun env evm result ->
+        let open Constr_quoted.ConstrQuoted in
+        let qresult = List.map quote_global_reference result in
+        let res = quote_list tglobal_reference qresult in
+        k (env, evm, res))
diff --git a/template-coq/src/template_monad.ml b/template-coq/src/template_monad.ml
@@ -108,7 +108,8 @@ let (ttmReturn,
      ttmQuoteConstant,
      ttmInductive,
      ttmInferInstance,
-     ttmExistingInstance) =
+     ttmExistingInstance,
+     ttmDependencies) =
   (r_template_monad_type_p "tmReturn",
    r_template_monad_type_p "tmBind",
 
@@ -133,7 +134,8 @@ let (ttmReturn,
    r_template_monad_type_p "tmInductive",
 
    r_template_monad_type_p "tmInferInstance",
-   r_template_monad_type_p "tmExistingInstance")
+   r_template_monad_type_p "tmExistingInstance",
+   r_template_monad_type_p "tmDependencies")
 
 type constr = Constr.t
 
@@ -179,6 +181,8 @@ type template_monad =
   | TmInferInstance of Constr.t * Constr.t (* only Prop *)
   | TmInferInstanceTerm of Constr.t        (* only Extractable *)
 
+  | TmDependencies of Constr.t * Constr.t
+
 (* todo: the recursive call is uneeded provided we call it on well formed terms *)
 let rec app_full trm acc =
   match Constr.kind trm with
@@ -370,4 +374,11 @@ let next_action env evd (pgm : constr) : template_monad * _ =
        (TmInferInstanceTerm typ, universes)
     | _ -> monad_failure "tmInferInstance" 2
 
+  else if Globnames.eq_gr glob_ref ttmDependencies then
+    match args with
+    | trm :: bypass :: [] ->
+      (TmDependencies (trm, bypass), universes)
+    | _ -> monad_failure "tmInferInstance" 2
+
+
   else CErrors.user_err (str "Invalid argument or not yet implemented. The argument must be a TemplateProgram: " ++ pr_constr coConstr)
diff --git a/template-coq/src/template_monad.mli b/template-coq/src/template_monad.mli
@@ -1,4 +1,3 @@
-
 val ptmTestQuote : Names.global_reference
 val ptmQuoteDefinition : Names.global_reference
 val ptmQuoteDefinitionRed : Names.global_reference
@@ -48,7 +47,7 @@ type template_monad =
   | TmExistingInstance of Constr.t
   | TmInferInstance of Constr.t * Constr.t (* only Prop *)
   | TmInferInstanceTerm of Constr.t        (* only Extractable *)
-
+  | TmDependencies of Constr.t * Constr.t
 
 val app_full
   : Constr.constr -> Constr.constr list -> Constr.constr * Constr.constr list

diff --git a/template-coq/theories/TemplateMonad/Extractable.v b/template-coq/theories/TemplateMonad/Extractable.v
@@ -52,6 +52,8 @@ Cumulative Inductive TM@{t} : Type@{t} -> Type :=
   : TM constant_entry
 
 | tmQuoteUniverses : TM uGraph.t
+| tmDependencies (gr : global_reference) (bypass : bool)
+  : TM (list global_reference)
 
 (* unquote before making the definition *)
 (* FIXME take an optional universe context as well *)