Allow proofs to start with dependent goals.

I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.

6 files changed, 66 insertions, 1 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 35166def0..9e6045661 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -233,6 +233,14 @@ let start sigma goals =
     shelf = [] ;
     given_up = [] } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
+let dependent_start sigma goals =
+  let pr = {
+    proofview = Proofview.dependent_init sigma goals ;
+    focus_stack = [] ;
+    shelf = [] ;
+    given_up = [] } in
+  let number_of_goals = List.length (Proofview.initial_goals pr.proofview) in
+  _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
 exception UnfinishedProof
 exception HasShelvedGoals
diff --git a/proofs/proof.mli b/proofs/proof.mli
index b9c3aa1b0..c535fa914 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -54,6 +54,8 @@ val proof : proof ->
 (*** General proof functions ***)
 
 val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
+val dependent_start : Evd.evar_map -> Proofview.telescope -> proof
+
 val initial_goals : proof -> (Term.constr * Term.types) list
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 12a528504..b7a32a980 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -248,6 +248,18 @@ let start_proof id str goals ?(compute_guard=[]) hook =
     mode = find_proof_mode "No" } in
   push initial_state pstates
 
+let start_dependent_proof id str goals ?(compute_guard=[]) hook =
+  let initial_state = {
+    pid = id;
+    proof = Proof.dependent_start Evd.empty goals;
+    endline_tactic = None;
+    section_vars = None;
+    strength = str;
+    compute_guard = compute_guard;
+    hook = Ephemeron.create hook;
+    mode = find_proof_mode "No" } in
+  push initial_state pstates
+
 let get_used_variables () = (cur_pstate ()).section_vars
 
 let set_used_variables l =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index b710b4ffe..e88c2f394 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -52,12 +52,20 @@ val give_me_the_proof : unit -> Proof.proof
     proof end (e.g. to declare the built constructions as a coercion
     or a setoid morphism). *)
 type lemma_possible_guards = int list list
-val start_proof : Names.Id.t -> 
+val start_proof : Names.Id.t ->
                           Decl_kinds.goal_kind ->
                           (Environ.env * Term.types) list  ->
                           ?compute_guard:lemma_possible_guards -> 
                           unit Tacexpr.declaration_hook -> 
                           unit
+(** Like [start_proof] except that there may be dependencies between
+    initial goals. *)
+val start_dependent_proof : Names.Id.t ->
+                          Decl_kinds.goal_kind ->
+                          Proofview.telescope  ->
+                          ?compute_guard:lemma_possible_guards ->
+                          unit Tacexpr.declaration_hook ->
+                          unit
 
 type closed_proof =
   Names.Id.t *
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 26a2985c6..1dff6203b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -53,6 +53,32 @@ let init sigma =
     (* Marks all the goal unresolvable for typeclasses. *)
     { v with solution = Typeclasses.mark_unresolvables v.solution }
 
+type telescope =
+  | TNil
+  | TCons of Environ.env*Term.types*(Term.constr -> telescope)
+
+let dependent_init =
+  let rec aux sigma = function
+  | TNil -> { initial = [] ;
+	     solution = sigma ;
+             comb = [];
+	   }
+  | TCons (env,typ,t) -> let ( sigma , econstr ) =
+			  Evarutil.new_evar sigma env typ
+			in
+                        let { initial = ret ; solution = sol ; comb = comb } =
+                          aux sigma (t econstr)
+                        in
+			let (e,_) = Term.destEvar econstr in
+			let gl = Goal.build e in
+			{ initial = (econstr,typ)::ret;
+			   solution = sol ;
+                           comb = gl::comb; }
+  in
+  fun sigma t -> let v = aux sigma t in
+    (* Marks all the goal unresolvable for typeclasses. *)
+    { v with solution = Typeclasses.mark_unresolvables v.solution }
+
 let initial_goals { initial } = initial
 
 (* Returns whether this proofview is finished or not. That is,
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b9251fffb..2f215ba94 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -38,6 +38,15 @@ val proofview : proofview -> Goal.goal list * Evd.evar_map
    conclusion types, creating that many initial goals. *)
 val init : Evd.evar_map -> (Environ.env * Term.types) list -> proofview
 
+type telescope =
+  | TNil
+  | TCons of Environ.env*Term.types*(Term.constr -> telescope)
+
+(* Like [init], but goals are allowed to be depedenent on one
+   another. Dependencies between goals is represented with the type
+   [telescope] instead of [list]. *)
+val dependent_init  : Evd.evar_map -> telescope -> proofview
+
 (* Returns whether this proofview is finished or not. That is,
    if it has empty subgoals in the comb. There could still be unsolved
    subgoaled, but they would then be out of the view, focused out. *)