-Debugging multiple induction, a bug appeared when having function

 arguments to a principle (like in map_ind).

 -Added nbranches and npredicates to elim_scheme, and made the elimc
 field optional.


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

1 files changed, 83 insertions, 66 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bf354a608..0f061fd76 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1367,9 +1367,76 @@ let cook_sign hyp0_opt indvars_init env =
     (statuslists, (if hyp0_opt=None then None else lhyp0) , !indhyps, !decldeps)
 
 
+(*
+   The general form of an induction principle is the following:
+   
+   forall prm1 prm2 ... prmp,                          (induction parameters)
+   forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates)
+   branch1, branch2, ... , branchr,                    (branches of the principle)
+   forall (x1:Ti_1) (x2:Ti_2) ... (xni:Ti_ni),         (induction arguments)
+   (HI: I prm1..prmp x1...xni)                         (optional main induction arg)
+   -> (Qi x1...xni HI        (f prm1...prmp x1...xni)).(conclusion)
+                   ^^        ^^^^^^^^^^^^^^^^^^^^^^^^
+               optional        optional argument added if
+               even if HI    principle generated by functional 
+             present above   induction, only if HI does not exist
+             [indarg]                  [farg]
+
+  HI is not present when the induction principle does not come directly from an
+  inductive type (like when it is generated by functional induction for
+  example). HI is present otherwise BUT may not appear in the conclusion
+  (dependent principle). HI and (f...) cannot be both present.
+
+  Principles taken from functional induction have the final (f...).*)
+
+(* [rel_contexts] and [rel_declaration] actually contain triples, and
+   lists are actually in reverse order to fit [compose_prod]. *)
+type elim_scheme = { 
+  elimc: (Term.constr * constr Rawterm.bindings) option;
+  elimt: types;
+  indref: global_reference option;
+  params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  nparams: int;            (* number of parameters *)
+  predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  npredicates: int;        (* Number of predicates *)
+  branches: rel_context;   (* branchr,...,branch1 *)
+  nbranches: int;          (* Number of branches *) 
+  args: rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
+  nargs: int;              (* number of arguments *)
+  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) 
+				     if HI is in premisses, None otherwise *)
+  concl: types;            (* Qi x1...xni HI (f...), HI and (f...) 
+			      are optional and mutually exclusive *)
+  indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
+}
+
+let empty_scheme = 
+  { 
+    elimc = None;
+    elimt = mkProp;
+    indref = None;
+    params = [];
+    nparams = 0;
+    predicates = [];
+    npredicates = 0;
+    branches = [];
+    nbranches = 0;
+    args = [];
+    nargs = 0;
+    indarg = None;
+    concl = mkProp;
+    indarg_in_concl = false;
+    farg_in_concl = false;
+  }
+
+
 (* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the
    hypothesis on which the induction is made *)
-let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
+let induction_tac varname typ scheme (*(elimc,lbindelimc),elimt*) gl =
+  let elimc,lbindelimc = 
+    match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in
+  let elimt = scheme.elimt in
   let c = mkVar varname in
   let indclause  = make_clenv_binding gl (c,typ) NoBindings  in
   let elimclause =
@@ -1520,64 +1587,6 @@ let decompose_paramspred_branch_args elimt =
 let exchange_hd_app subst_hd t =
   let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args)
 
-(*
-   The general form of an induction principle is the following:
-   
-   forall prm1 prm2 ... prmp,                          (induction parameters)
-   forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates)
-   branch1, branch2, ... , branchr,                    (branches of the principle)
-   forall (x1:Ti_1) (x2:Ti_2) ... (xni:Ti_ni),         (induction arguments)
-   (HI: I prm1..prmp x1...xni)                         (optional main induction arg)
-   -> (Qi x1...xni HI        (f prm1...prmp x1...xni)).(conclusion)
-                   ^^        ^^^^^^^^^^^^^^^^^^^^^^^^
-               optional        optional argument added if
-               even if HI    principle generated by functional 
-             present above   induction, only if HI does not exist
-             [indarg]                  [farg]
-
-  HI is not present when the induction principle does not come directly from an
-  inductive type (like when it is generated by functional induction for
-  example). HI is present otherwise BUT may not appear in the conclusion
-  (dependent principle). HI and (f...) cannot be both present.
-
-  Principles taken from functional induction have the final (f...).*)
-
-(* [rel_contexts] and [rel_declaration] actually contain triples, and
-   lists are actually in reverse order to fit [compose_prod]. *)
-type elim_scheme = { 
-  elimc: Term.constr * constr Rawterm.bindings;
-  elimt: types;
-  indref: global_reference option;
-  params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
-  nparams: int;            (* number of parameters *)
-  predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
-  branches: rel_context;    (* branchr,...,branch1 *)
-  args: rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
-  nargs: int;              (* number of arguments *)
-  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) 
-				     if HI is in premisses, None otherwise *)
-  concl: types;            (* Qi x1...xni HI (f...), HI and (f...) 
-			      are optional and mutually exclusive *)
-  indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
-  farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
-}
-
-let empty_scheme = 
-  { 
-    elimc = mkProp,NoBindings;
-    elimt = mkProp;
-    indref = None;
-    params = [];
-    nparams = 0;
-    predicates = [];
-    branches = [];
-    args = [];
-    nargs = 0;
-    indarg = None;
-    concl = mkProp;
-    indarg_in_concl = false;
-    farg_in_concl = false;
-  }
 
 exception NoLastArg
 exception NoLastArgCcl
@@ -1598,7 +1607,7 @@ exception NoLastArgCcl
      predicates are cited in the conclusion.
 
    - finish to fill in the elim_scheme: indarg/farg/args and finally indref. *)
-let compute_elim_sig elimc elimt =
+let compute_elim_sig ?elimc elimt =
   let params_preds,branches,args_indargs,conclusion = 
     decompose_paramspred_branch_args elimt in
   
@@ -1611,7 +1620,8 @@ let compute_elim_sig elimc elimt =
   let res = ref { empty_scheme with
     (* This fields are ok: *)
     elimc = elimc; elimt = elimt; concl = conclusion;
-    predicates = preds; branches = branches; 
+    predicates = preds; npredicates = List.length preds; 
+    branches = branches; nbranches = List.length branches; 
     farg_in_concl = (try isApp (last_arg ccl) with _ -> false);
     params = params; nparams = nparams; 
     (* all other fields are unsure at this point. Including these:*)
@@ -1665,7 +1675,7 @@ let compute_elim_sig elimc elimt =
    the non standard case, naming of generated hypos is slightly
    different. *)
 let compute_elim_signature elimc elimt names_info =
-  let scheme = compute_elim_sig elimc elimt in
+  let scheme = compute_elim_sig ~elimc:elimc elimt in
   let f,l = decompose_app scheme.concl in
   (* Vérifier que les arguments de Qi sont bien les xi. *)
   match scheme.indarg with
@@ -1803,17 +1813,24 @@ let recolle_clenv scheme lid elimclause gl =
   List.fold_right
     (fun e acc ->
       let x,y,i = e in
-      let indclause  = make_clenv_binding gl (x,y) NoBindings in
+      (* from_n (Some 0) means that x should be taken "as is" without
+         trying to unify (which would lead to trying to apply it to
+         evars if y is a product). *)
+      let indclause  = mk_clenv_from_n gl (Some 0) (x,y) in
       let elimclause' = clenv_fchain i acc indclause in
       elimclause')
     (List.rev clauses)
     elimclause
 
+
 (* Unification of the goal and the principle applied to meta variables:
    (elimc ?i ?j ?k...?l). This solves partly meta variables (and may
     produce new ones). Then refine with the resulting term with holes.
 *)
-let induction_tac_felim indvars (elimc,lbindelimc) elimt scheme gl = 
+let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl = 
+  let elimt = scheme.elimt in
+  let elimc,lbindelimc = 
+    match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimclause =
     make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
@@ -1876,7 +1893,7 @@ let induction_from_context_l isrec elim_info lid names gl =
 	  (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all
 	     possible holes using arguments given by the user (but the
 	     functional one). *)
-	  induction_tac_felim realindvars scheme.elimc scheme.elimt scheme;
+	  induction_tac_felim realindvars scheme;
           tclTRY (thin (List.rev (indhyps)));
 	])
 	(array_map2 
@@ -1921,7 +1938,7 @@ let induction_from_context isrec elim_info hyp0 names gl =
       thin dephyps;
       (if isrec then tclTHENFIRSTn else tclTHENLASTn)
        	(tclTHENLIST
-	  [ induction_tac hyp0 typ0 (scheme.elimc,scheme.elimt);
+	  [ induction_tac hyp0 typ0 scheme (*scheme.elimc,scheme.elimt*);
 	    thin [hyp0];
             tclTRY (thin indhyps) ])
        	(array_map2