Derive plugin: a more general interface.

Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.

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