Intégration progressive

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

2 files changed, 56 insertions, 67 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index a8b6787ed0..53eaa4ad15 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -11,6 +11,7 @@ open Sign
 open Environ
 open Printer
 open Reduction
+open Retyping
 open Tacmach
 open Proof_trees
 open Clenv
@@ -21,6 +22,7 @@ open Tactics
 open Elim
 open Equality
 open Typing
+open Pattern
 
 (* [make_inv_predicate (ity,args) C]
   
@@ -70,14 +72,15 @@ let named_push_lambda_and_liftl env n hyps t l =
 
 let dest_match_eq gls eqn =
   try 
-    dest_match gls eqn eq_pattern
-  with _ -> 
+    pf_matches gls (eq_pattern ()) eqn
+  with PatternMatchingFailure -> 
     (try 
-       dest_match gls eqn eqT_pattern
-     with _ -> 
+       pf_matches gls (eqT_pattern ()) eqn
+     with PatternMatchingFailure -> 
        (try 
-	  dest_match gls eqn idT_pattern
-        with _ -> errorlabstrm "dest_match_eq" 
+	  pf_matches gls (idT_pattern ()) eqn
+        with PatternMatchingFailure ->
+	  errorlabstrm "dest_match_eq" 
 	    [< 'sTR "no primitive equality here" >]))
     
 let type_of_predicate_argument gls ity globargs =
@@ -114,16 +117,13 @@ let make_inv_predicate (ity,args) c dflt_concl dep_option gls =
                 (nf_betadeltaiota env sigma (mind_arity ity)) globargs in 
   let len = List.length largs_init in
   let hyps = [] in
-  let largs = (List.map insert_lifted largs_init) in
+  let largs = List.map insert_lifted largs_init in
   let (hyps,larg_var_list,concl,dephyp) =                   
     if not dep_option (* (dependent (VAR id) concl) *) then 
       (* We push de arity and leave concl unchanged *)
       let hyps_ar,_,largs_ar = named_push_and_liftl env len hyps arity largs in
       let larg_var_list =
-        list_map_i 
-          (fun i ai ->
-             insert_lifted
-               (DOP2(implicit,extract_lifted ai,Rel(len-i+1)))) 1 largs
+        list_map_i (fun i ai -> (extract_lifted ai,len-i+1)) 1 largs
       in 
       (hyps_ar,larg_var_list,concl,0)
     else 
@@ -147,10 +147,7 @@ let make_inv_predicate (ity,args) c dflt_concl dep_option gls =
                                   (nb_prod arity +1)))) 
 	in
         let larg_var_list =
-          list_map_i
-            (fun i ai->
-               insert_lifted
-                 (DOP2(implicit,extract_lifted ai,Rel(len-i+2)))) 1 largs 
+          list_map_i (fun i ai-> (extract_lifted ai,len-i+2)) 1 largs 
         in 
 	(hyps,larg_var_list,c3,1)
   in
@@ -159,19 +156,15 @@ let make_inv_predicate (ity,args) c dflt_concl dep_option gls =
   (* Now, we can recurse down this list, for each ai,(Rel k) whether to
      push <Ai>(Rel k)=ai (when   Ai is closed).
    In any case, we carry along the rest of larg_var_list *)
-  let rec build_concl (hyps,l) =
-    match l with
+  let rec build_concl hyps n = function
       | [] ->
-          let neqns = ((List.length hyps-dephyp)-len) in
+          let neqns = (List.length hyps) - dephyp - len in
+	  let (hyps1,hyps2) = list_chop neqns hyps in
           let hyps,concl,_ = prod_and_popl neqns hyps concl [] in
-          let _,concl,_ = lam_and_popl (List.length hyps) hyps concl [] in 
-	  (concl,neqns)
-      | t::restlist ->
-          let (ai,k) = 
-	    match extract_lifted t with 
-	      | DOP2(_,ai,Rel k) -> (ai,k) 
-	      | _ -> assert false 
-	  in
+	  (lam_it (prod_it concl hyps1) hyps2,neqns)
+      | (ai,k)::restlist ->
+	  let ai = lift n ai in
+	  let k = k+n in
           let tk = (Typeops.relative (change_sign env (sign,hyps)) k).uj_val in
           let (lhs,eqnty,rhs) =
             if closed0 tk then 
@@ -180,15 +173,15 @@ let make_inv_predicate (ity,args) c dflt_concl dep_option gls =
 	      make_iterated_tuple Evd.empty
 		(change_sign env (sign,hyps))
 		(ai,type_of env Evd.empty ai)
-		(Rel k,tk) 
+		(Rel k,tk)
 	  in
-          let type_type_rhs = type_of env sigma (type_of env sigma rhs) in
-          let sort = pf_type_of gls (pf_concl gls) in 
+          let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in
+          let sort = destSort (pf_type_of gls (pf_concl gls)) in 
           let eq_term = find_eq_pattern type_type_rhs sort in
           let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in 
-	  build_concl (push_and_lift (Anonymous,eqn) hyps restlist) 
+	  build_concl ((Anonymous,eqn)::hyps) (n+1) restlist
   in
-  let (predicate,neqns) = build_concl (hyps,larg_var_list) in
+  let (predicate,neqns) = build_concl hyps 0 larg_var_list in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
   (predicate,neqns)
@@ -253,7 +246,7 @@ let rec dependent_hyps id idlist sign =
     | [] -> []
     | (id1::l) -> 
 	let id1ty = snd (lookup_var id1 sign) in  
-	if occur_var id id1ty.body then id1::dep_rec l else dep_rec l
+	if occur_var id (body_of_type id1ty) then id1::dep_rec l else dep_rec l
   in 
   dep_rec idlist 
 
@@ -279,7 +272,7 @@ let split_dep_and_nodep idl gl =
 
 let dest_eq gls t =
   match dest_match_eq gls t with
-    | [x;y;z] -> (x,y,z)
+    | [(1,x);(2,y);(3,z)] -> (x,y,z)
     | _ -> error "dest_eq: should be an equality"
 
 (* invariant: ProjectAndApplyNoThining simplifies the clause (an equality) .
@@ -513,7 +506,7 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
 	 | [ic; Identifier id; Command com] ->
              fun gls -> 
 	       inv false (com_of_id ic)
-		 (Some (pf_constr_of_com gls com)) true id gls
+		 (Some (pf_interp_constr gls com)) true id gls
 	 | _ -> anomaly "DInvWith called with bad args")
   in
   ((fun id com -> gentac [hinv_kind; Identifier id; Command com]),
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 240a8e172a..8c250bd3de 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -24,7 +24,7 @@ open Inv
 (* Fonctions temporaires pour relier la forme castée et la forme jugement *)
 let tsign_of_csign (idl,tl) = (idl,List.map outcast_type tl)
 
-let csign_of_tsign (idl,tl) = (idl,List.map incast_type tl)
+let csign_of_tsign = map_sign_typ incast_type
 (* FIN TMP *)
 
 let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
@@ -84,7 +84,7 @@ let thin_hyps_to_term (hyps,t) =
 
 let get_local_sign sign =
   let lid = ids_of_sign sign in
-  let globsign = initial_sign() in
+  let globsign = Global.var_context() in
   let add_local id res_sign = 
     if not (mem_sign globsign id) then 
       add_sign (lookup_sign id sign) res_sign
@@ -100,7 +100,7 @@ let get_local_sign sign =
  * it returns both the pair (id,(sign_prefix id sign)) *)
 
 let max_prefix_sign lid sign =
-  let rec max_rec (resid,prefix)  = function
+  let rec max_rec (resid,prefix) = function
     | [] -> (resid,prefix)
     | (id::l) -> 
 	let pre = sign_prefix id sign in  
@@ -109,8 +109,9 @@ let max_prefix_sign lid sign =
         else 
 	  max_rec (resid,prefix) l
   in
-  let (id::l) = lid in 
-  max_rec (id, sign_prefix id sign) l
+  match lid with 
+    | [] -> nil_sign
+    | id::l -> snd (max_rec (id, sign_prefix id sign) l)
 
 let rel_of_env env = 
   let rec rel_rec = function 
@@ -126,12 +127,7 @@ let build_app op env = applist (op, List.rev (rel_of_env env))
 let prod_and_pop_named = function
   | ([], body, l, acc_ids) -> error "lam_and_pop"
   | (((na,t)::tlenv), body, l, acc_ids) -> 
-      let (Name id)=
-	if na=Anonymous then 
-	  Name(next_ident_away (id_of_string "a") acc_ids)
-        else 
-	  na
-      in 
+      let id = next_name_away_with_default "a" na acc_ids in
       (tlenv,DOP2(Prod,t,DLAM((Name id),body)),
        List.map (function 
 		   | (0,x) -> (0,lift (-1) x)
@@ -163,13 +159,15 @@ let prod_and_popl_named  n env t l =
    where P: P:(x_bar:T_bar)(H:(I t_bar)->[sort]     
 *)
 
+(* Adaption rapide : à relire *)
 let compute_first_inversion_scheme sign i sort dep_option =
-  let (ity,largs) = find_mrectype empty_evd i in
-  let ar = mind_arity ity in 
+  let globenv = Global.env () in
+  let (ity,largs) = find_mrectype globenv Evd.empty i in
+  let ar = Global.mind_arity ity in 
   (* let ar = nf_betadeltaiota empty_evd (mind_arity ity) in *)
   let fv = global_vars i in
   let thin_sign = thin_hyps_to_term (sign,i) in
-  if not(same_members fv (ids_of_sign thin_sign)) then
+  if not(list_subset fv (ids_of_sign thin_sign)) then
     errorlabstrm "lemma_inversion"
       [< 'sTR"Cannot compute lemma inversion when there are" ; 'sPC ;
 	 'sTR"free variables in the types of an inductive" ; 'sPC ;
@@ -179,13 +177,13 @@ let compute_first_inversion_scheme sign i sort dep_option =
     let (pty,goal) =
       let (env,_,_) = push_and_liftl (nb_prod ar) []  ar [] in
       let h = next_ident_away (id_of_string "P") (ids_of_sign sign) in
-      let (env1,_)= push_and_lift (Name h, (build_app ity env)) env [] in
+      let (env1,_)= push_and_lift (Name h, (build_app (mkMutInd ity) env)) env [] in
       let (_,pty,_) = prod_and_popl_named (List.length env1) env1 sort [] in 
       let pHead= applist(VAR p, largs@[Rel 1]) 
-      in  (pty, Environ.prod_name(Name h,i,pHead))
+      in  (pty, Environ.prod_name globenv (Name h,i,pHead))
     in 
     (prepend_sign thin_sign 
-       (add_sign (p,nf_betadeltaiota empty_evd pty) nil_sign),
+       (add_sign (p,nf_betadeltaiota globenv Evd.empty pty) nil_sign),
        goal)
   else  
     let local_sign = get_local_sign thin_sign in 
@@ -196,11 +194,9 @@ let compute_first_inversion_scheme sign i sort dep_option =
       (it_sign (fun b id ty -> mkNamedProd id ty b) 
 	 sort local_sign, mkArrow i pHead) 
     in 
-    let npty = nf_betadeltaiota empty_evd pty in
+    let npty = nf_betadeltaiota globenv Evd.empty pty in
     let lid = global_vars npty in 
-    let maxprefix = 
-      if lid=[] then nil_sign else snd (max_prefix_sign lid thin_sign)
-    in 
+    let maxprefix = max_prefix_sign lid thin_sign in
     (prepend_sign local_sign (add_sign (p,npty)  maxprefix), goal)
 
 (* [inversion_scheme sign I]
@@ -211,15 +207,15 @@ let compute_first_inversion_scheme sign i sort dep_option =
    build a dependent lemma or a non-dependent one *)
 
 let inversion_scheme sign i sort dep_option inv_op =
-  let (i,sign) = add_prods_sign empty_evd (i,sign) in
+  let (i,sign) = add_prods_sign Evd.empty (i,sign) in
   let sign = csign_of_tsign sign in
   let (invSign,invGoal) =
     compute_first_inversion_scheme sign i sort dep_option in
-  let invSign = castify_sign empty_evd invSign in
-  if (not((subset (global_vars invGoal) (ids_of_sign invSign)))) then
+  let invSign = castify_sign Evd.empty invSign in
+  if (not((list_subset (global_vars invGoal) (ids_of_sign invSign)))) then
     errorlabstrm "lemma_inversion"
       [< 'sTR"Computed inversion goal was not closed in initial signature" >];
-  let invGoalj = fexecute empty_evd invSign invGoal in
+  let invGoalj = get_type_of Evd.empty invSign invGoal in
   let pfs =
     mk_pftreestate
       (mkGOAL (mt_ctxt Spset.empty) invSign (j_val_cast invGoalj)) in
@@ -315,8 +311,8 @@ let _ =
 	  VARG_COMMAND sort] ->
        fun () ->
 	 add_inversion_lemma_exn na 
-	   (constr_of_com empty_evd (initial_sign()) com)
-	   (constr_of_com empty_evd (initial_sign()) sort)
+	   (constr_of_com Evd.empty (initial_sign()) com)
+	   (constr_of_com Evd.empty (initial_sign()) sort)
 	   false (inversion_clear false))
 
 let _ = 
@@ -337,8 +333,8 @@ let _ =
 	  VARG_COMMAND sort] ->
        fun () ->
 	 add_inversion_lemma_exn na 
-	   (constr_of_com empty_evd (initial_sign()) com)
-	   (constr_of_com empty_evd (initial_sign()) sort)
+	   (constr_of_com Evd.empty (initial_sign()) com)
+	   (constr_of_com Evd.empty (initial_sign()) sort)
 	   false (inv false (Some false) None false))
 
 let _ = 
@@ -349,8 +345,8 @@ let _ =
 	  VARG_COMMAND sort] ->
        fun () ->
 	 add_inversion_lemma_exn na 
-	   (constr_of_com empty_evd (initial_sign()) com)
-	   (constr_of_com empty_evd (initial_sign()) sort)
+	   (constr_of_com Evd.empty (initial_sign()) com)
+	   (constr_of_com Evd.empty (initial_sign()) sort)
 	   true (inversion_clear true))
 
 let _ = 
@@ -361,8 +357,8 @@ let _ =
 	  VARG_COMMAND sort] ->
        fun () ->
 	 add_inversion_lemma_exn na
-	   (constr_of_com empty_evd (initial_sign()) com)
-	   (constr_of_com empty_evd (initial_sign()) sort)
+	   (constr_of_com Evd.empty (initial_sign()) com)
+	   (constr_of_com Evd.empty (initial_sign()) sort)
 	   true (inversion_clear true))
 
 (* ================================= *)