Experimental support for automatic destruction of recursive calls and

clearing of recursive protototypes in Program obligations. Relies on
marking said prototypes with a particular constant and preprocessing
obligation goals with an appropriate tactic.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12071 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 31 insertions, 9 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 00a69bba7..d65b520b6 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -92,7 +92,6 @@ let subst_vars acc n t =
 (** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
     to a product : forall H1 : t1, ..., forall Hn : tn, concl.
     Changes evars and hypothesis references to variable references.
-    A little optimization: don't include unnecessary let-ins and their dependencies.
 *) 
 let etype_of_evar evs hyps concl =
   let rec aux acc n = function
@@ -104,11 +103,9 @@ let etype_of_evar evs hyps concl =
 	let trans' = Idset.union trans trans' in
 	  (match copt with
 	      Some c -> 
-(* 		if noccurn 1 rest then lift (-1) rest, s', trans' *)
-(* 		else *)
-		  let c', s'', trans'' = subst_evar_constr evs n c in
-		  let c' = subst_vars acc 0 c' in
-		    mkNamedProd_or_LetIn (id, Some c', t'') rest, 
+		let c', s'', trans'' = subst_evar_constr evs n c in
+		let c' = subst_vars acc 0 c' in
+		  mkNamedProd_or_LetIn (id, Some c', t'') rest, 
 		Intset.union s'' s', 
 		Idset.union trans'' trans'
 	    | None -> 
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index bf402c24c..0bfafa492 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -396,7 +396,10 @@ let interp_recursive fixkind l boxed =
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let rec_sign = 
-    List.fold_left2 (fun env id t -> (id,None,t) :: env)
+    List.fold_left2 (fun env' id t ->
+      let sort = Retyping.get_type_of env !evdref t in
+      let fixprot = mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|]) in
+	(id,None,fixprot) :: env')
       [] fixnames fixtypes
   in
   let env_rec = push_named_context rec_sign env in
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 3a6a351ba..6f73bc942 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -42,6 +42,16 @@ val interp_binder :     Evd.evar_defs ref ->
     Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
 
 
+val telescope :
+  (Names.name * 'a option * Term.types) list ->
+  Term.types * (Names.name * Term.types option * Term.types) list *
+    Term.constr
+
+val build_wellfounded : 
+           Names.identifier * 'a * Topconstr.local_binder list *
+           Topconstr.constr_expr * Topconstr.constr_expr ->
+           Topconstr.constr_expr ->
+           Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
 
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 01fe4ef6f..5003b60a7 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -1,4 +1,4 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
+(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -221,7 +221,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let nbfix = Array.length lar in
 	let names = Array.map (fun id -> Name id) names in
 	  (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-	let newenv = push_rec_types (names,ftys,[||]) env in
+	let newenv = 
+	  let marked_ftys = 
+	    Array.map (fun ty -> let sort = Retyping.get_type_of env !isevars ty in
+				   mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |]))
+	      ftys
+	  in
+	    push_rec_types (names,marked_ftys,[||]) env 
+	in
 	let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in
 	let vdefj =
 	  array_map2_i 
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 8e38999fd..645e3e23e 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -17,6 +17,7 @@ let fix_sub_module = "Wf"
 let utils_module = "Utils"
 let fixsub_module = subtac_dir @ [fix_sub_module]
 let utils_module = subtac_dir @ [utils_module]
+let tactics_module = subtac_dir @ ["Tactics"]
 let init_constant dir s = gen_constant contrib_name dir s
 let init_reference dir s = gen_reference contrib_name dir s
 
@@ -48,6 +49,8 @@ let build_sig () =
 
 let sig_ = lazy (build_sig ())
 
+let fix_proto = lazy (init_constant tactics_module "fix_proto")
+
 let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
 let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
 let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect")
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index d60893283..dff1df8f9 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -34,6 +34,8 @@ val proj2_sig_ref : reference
 val build_sig : unit -> coq_sigma_data
 val sig_ : coq_sigma_data lazy_t
 
+val fix_proto : constr lazy_t
+
 val eq_ind : constr lazy_t
 val eq_rec : constr lazy_t
 val eq_rect : constr lazy_t