diff options
| -rw-r--r-- | plugins/Derive/derive.ml | 100 | ||||
| -rw-r--r-- | plugins/Derive/derive.mli | 9 | ||||
| -rw-r--r-- | plugins/Derive/g_derive.ml4 | 4 |
3 files changed, 65 insertions, 48 deletions
diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml index 1601a7ce2..bf4b78b04 100644 --- a/plugins/Derive/derive.ml +++ b/plugins/Derive/derive.ml @@ -6,57 +6,72 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let interp_init_def_and_relation env sigma init_def r = - let init_def, _ = Constrintern.interp_constr sigma env init_def in - let init_type = Typing.type_of env sigma init_def in +let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body) + : Entries.const_entry_body = + Future.chain ~pure:true x begin fun ((b,ctx),fx) -> + (f b , ctx) , fx + end - let r_type = - let open Term in - mkProd (Names.Anonymous,init_type, mkProd (Names.Anonymous,init_type,mkProp)) - in - let r, ctx = Constrintern.interp_casted_constr sigma env r r_type in - init_def , init_type , r, ctx - - -(** [start_deriving f init r lemma] starts a proof of [r init - ?x]. When the proof ends, [f] is defined as the value of [?x] and - [lemma] as the proof. *) -let start_deriving f init_def r lemma = +(** [start_deriving f suchthat lemma] starts a proof of [suchthat] + (which can contain references to [f]) in the context extended by + [f:=?x]. When the proof ends, [f] is defined as the value of [?x] + and [lemma] as the proof. *) +let start_deriving f suchthat lemma = let env = Global.env () in let sigma = Evd.from_env env in let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in - let ( init_def , init_type , r , ctx ) = - interp_init_def_and_relation env sigma init_def r - in + (* create a sort variable for the type of [f] *) + (* spiwack: I don't know what the rigidity flag does, picked the one + that looked the most general. *) + let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in + let f_type_type = Term.mkSort f_type_sort in let goals = let open Proofview in - TCons ( env , (init_type ) , (fun ef -> - TCons ( env , ( Term.mkApp ( r , [| init_def ; ef |] )) , (fun _ -> TNil)))) - in - let terminator com = - let open Proof_global in - match com with - | Admitted -> Errors.error"Admitted isn't supported in Derive." - | Proved (_,Some _,_) -> - Errors.error"Cannot save a proof of Derive with an explicit name." - | Proved (opaque, None, obj) -> - let (f_def,lemma_def) = - match Proof_global.(obj.entries) with - | [f_def;lemma_def] -> - f_def , lemma_def - | _ -> assert false - in - (* The opacity of [f_def] is adjusted to be [false]. *) - let f_def = let open Entries in { f_def with + TCons ( env , sigma , f_type_type , (fun sigma f_type -> + TCons ( env , sigma , f_type , (fun sigma ef -> + let env' = Environ.push_named (f , (Some ef) , f_type) env in + let evdref = ref sigma in + let suchthat = Constrintern.interp_type_evars evdref env' suchthat in + TCons ( env' , !evdref , suchthat , (fun sigma _ -> + TNil sigma)))))) + in + let terminator com = + let open Proof_global in + match com with + | Admitted -> Errors.error"Admitted isn't supported in Derive." + | Proved (_,Some _,_) -> + Errors.error"Cannot save a proof of Derive with an explicit name." + | Proved (opaque, None, obj) -> + let (f_def,lemma_def) = + match Proof_global.(obj.entries) with + | [_;f_def;lemma_def] -> + f_def , lemma_def + | _ -> assert false + in + (* The opacity of [f_def] is adjusted to be [false]. *) + let f_def = let open Entries in { f_def with const_entry_opaque = false ; } in let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in - let lemma_typ = Term.(mkApp ( r , [| init_def ; mkConst f_kn |] )) in + let f_kn_term = Term.mkConst f_kn in + let lemma_pretype = + match Entries.(lemma_def.const_entry_type) with + | Some t -> t + | None -> assert false (* Proof_global always sets type here. *) + in + (* substitutes the variable [f] by the constant [f] it was standing for. *) + let lemma_type = Vars.replace_vars [f,f_kn_term] lemma_pretype in (* The type of [lemma_def] is adjusted to refer to [f_kn], the opacity is adjusted by the proof ending command. *) + let lemma_body = + map_const_entry_body begin fun c -> + Vars.replace_vars [f,f_kn_term] c + end Entries.(lemma_def.const_entry_body) + in let lemma_def = let open Entries in { lemma_def with - const_entry_type = Some lemma_typ ; + const_entry_body = lemma_body ; + const_entry_type = Some lemma_type ; const_entry_opaque = opaque ; } in let lemma_def = @@ -65,11 +80,12 @@ let start_deriving f init_def r lemma = in ignore (Declare.declare_constant lemma lemma_def) in - let () = Proof_global.start_dependent_proof - lemma kind ctx goals terminator - in + let () = Proof_global.start_dependent_proof lemma kind goals terminator in let _ = Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 1 shelve) p + Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end in () + + + diff --git a/plugins/Derive/derive.mli b/plugins/Derive/derive.mli index 33f982bb6..5157c4a27 100644 --- a/plugins/Derive/derive.mli +++ b/plugins/Derive/derive.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** [start_deriving f init r lemma] starts a proof of [r init - ?x]. When the proof ends, [f] is defined as the value of [?x] and - [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Names.Id.t -> unit +(** [start_deriving f suchthat lemma] starts a proof of [suchthat] + (which can contain references to [f]) in the context extended by + [f:=?x]. When the proof ends, [f] is defined as the value of [?x] + and [lemma] as the proof. *) +val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> unit diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4 index 9137c3d28..0721c675f 100644 --- a/plugins/Derive/g_derive.ml4 +++ b/plugins/Derive/g_derive.ml4 @@ -11,6 +11,6 @@ let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command -| [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] -> - [ Derive.start_deriving f init r lemma ] +| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> + [ Derive.start_deriving f suchthat lemma ] END |