Documentation of Program and its tactics, fix enormous interaction bug due to bad cache handling.

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

8 files changed, 59 insertions, 13 deletions

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 3734db855c..f047b729dd 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -1,6 +1,8 @@
 Require Import Wf.
 Require Import Coq.subtac.Utils.
 
+(** Reformulation of the Wellfounded module using subsets where possible. *)
+
 Section Well_founded.
   Variable A : Type.
   Variable R : A -> A -> Prop.
diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v
index 3429bf8ad0..f2b216d960 100644
--- a/contrib/subtac/Heq.v
+++ b/contrib/subtac/Heq.v
@@ -1,24 +1,34 @@
 Require Export JMeq.
 
+(** Notation for heterogenous equality. *)
+
 Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
 
+(** Do something on an heterogeneous equality appearing in the context. *)
+
 Ltac on_JMeq tac := 
   match goal with
     | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
   end.
 
+(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
+
 Ltac simpl_one_JMeq :=
   on_JMeq 
   ltac:(fun H => let H' := fresh "H" in 
     assert (H' := JMeq_eq H) ; clear H ; rename H' into H).
 
+(** Repeat it for every possible hypothesis. *)
+
+Ltac simpl_JMeq := repeat simpl_one_JMeq.
+
+(** Just simplify an h.eq. without clearing it. *)
+
 Ltac simpl_one_dep_JMeq :=
   on_JMeq
   ltac:(fun H => let H' := fresh "H" in 
     assert (H' := JMeq_eq H)).
 
-Ltac simpl_JMeq := repeat simpl_one_JMeq.
-
 
 
 
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index 7e66369f6b..a00234dde8 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -1,9 +1,7 @@
 Ltac induction_with_subterm c H :=
   let x := fresh "x" in
   let y := fresh "y" in
-  (set(x := c) ; assert(y:x = c) by reflexivity ;
-  rewrite <- y in H ; 
-  induction H ; subst).
+  (remember c as x ; rewrite <- y in H ; induction H ; subst).
 
 Ltac induction_on_subterm c :=
   let x := fresh "x" in
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 1d19dbd194..76f49dd3bc 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -2,21 +2,31 @@ Require Export Coq.subtac.SubtacTactics.
 
 Set Implicit Arguments.
 
+(** Wrap a proposition inside a subset. *)
+
 Notation " {{ x }} " := (tt : { y : unit | x }).
 
+(** A simpler notation for subsets defined on a cartesian product. *)
+
 Notation "{ ( x , y )  :  A  |  P }" := 
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident) : type_scope.
 
+(** Generates an obligation to prove False. *)
+
 Notation " ! " := (False_rect _ _).
 
+(** Abbreviation for first projection and hiding of proofs of subset objects. *)
+
 Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
 Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
 
-(** Coerces objects before comparing them *)
+(** Coerces objects to their support before comparing them. *)
+
 Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
 
-(** Quantifying over subsets *)
+(** Quantifying over subsets. *)
+
 Notation "'fun' { x : A | P } => Q" :=
   (fun x:{x:A|P} => Q)
   (at level 200, x ident, right associativity).
@@ -26,14 +36,18 @@ Notation "'forall' { x : A | P } , Q" :=
   (at level 200, x ident, right associativity).
 
 Require Import Coq.Bool.Sumbool.
+
 (** Construct a dependent disjunction from a boolean. *)
+
 Notation "'dec'" := (sumbool_of_bool) (at level 0). 
 
 (** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
+
 Notation in_right := (@right _ _ _).
 Notation in_left := (@left _ _ _).
 
 (** Default simplification tactic. *)
+
 Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
   try (solve [ red ; intros ; discriminate ]) ; auto with *.  
 
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index dd4535c33e..2a84fdd003 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -113,6 +113,9 @@ let rec chop_product n t =
 let eterm_obligations name nclen isevars evm fs t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
+  trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
+  trace (str "Term given to eterm" ++ spc () ++
+	    Termops.print_constr_env (Global.env ()) t);
   let evl = List.rev (to_list evm) in
   let evn = 
     let i = ref (-1) in
@@ -153,8 +156,6 @@ let eterm_obligations name nclen isevars evm fs t tycon =
     List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts
   in
     (try
-       trace (str "Term given to eterm" ++ spc () ++
-		Termops.print_constr_env (Global.env ()) t);
        trace (str "Term constructed in eterm" ++ spc () ++
 		Termops.print_constr_env (Global.env ()) t');
        ignore(iter
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index b5deafc5f8..4b33f9d86f 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -2071,7 +2071,16 @@ let liftn_rel_context n k sign =
   in
     liftrec (k + rel_context_length sign) sign
 
-
+let nf_evars_env evar_defs (env : env) : env = 
+  let nf t = nf_isevar evar_defs t in
+  let env0 : env = reset_context env in 
+  let f e (na, b, t) e' : env =
+    Environ.push_named (na, option_map nf b, nf t) e'
+  in
+  let env' = Environ.fold_named_context f ~init:env0 env in
+    Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e')
+     ~init:env' env
+      
 let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env eqns in
@@ -2079,6 +2088,11 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
   let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+(*   isevars := nf_evar_defs !isevars; *)
+(*   let env = nf_evars_env !isevars (env : env) in *)
+(*      trace (str "Evars : " ++ my_print_evardefs !isevars); *)
+(*     trace (str "Env : " ++ my_print_env env); *)
+    
   let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
   let tomatchs_len = List.length tomatchs_lets in
   let tycon = lift_tycon tomatchs_len tycon in
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index eaa177bce2..dded538b59 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -319,6 +319,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
     (* 	 evars; *)
     (*      with _ -> ());     *)
     Subtac_obligations.add_definition recname evars_def fullctyp evars
+
+let nf_evar_context isevars ctx = 
+  List.map (fun (n, b, t) -> 
+    (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
     
 let build_mutrec l boxed = 
   let sigma = Evd.empty and env = Global.env () in 
@@ -384,10 +388,13 @@ let build_mutrec l boxed =
       let (isevars, info, def) = defrec.(i) in
 	(*       let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *)
       let def = evar_nf isevars def in
+      let x, y, typ = arrec.(i) in
+      let typ = evar_nf isevars typ in
+      arrec.(i) <- (x, y, typ);
+      let rec_sign = nf_evar_context !isevars rec_sign in
       let isevars = Evd.undefined_evars !isevars in
 	(*       let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *)
       let evm = Evd.evars_of isevars in
-      let _, _, typ = arrec.(i) in
       let id = namerec.(i) in
 	(* Generalize by the recursive prototypes  *)
       let def = 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 9e41759504..1bd85b92bd 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -109,13 +109,13 @@ let _ =
 let progmap_union = ProgMap.fold ProgMap.add
 
 let cache (_, (infos, tac)) =
-  from_prg := progmap_union infos !from_prg;
+  from_prg := infos;
   default_tactic_expr := tac
 
 let (input,output) = 
   declare_object
     { (default_object "Program state") with
-      cache_function = cache ; 
+      cache_function = cache;
       load_function = (fun _ -> cache);
       open_function = (fun _ -> cache);
       classify_function = (fun _ -> Dispose);