module Wcclausenv

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

5 files changed, 261 insertions, 49 deletions

diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 8836631fef..297b26bb8e 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -2,15 +2,14 @@
 (* $Id$ *)
 
 open Pp
-open Initial
+open Util
 open Names
 open Generic
 open Term
 open Reduction
-open Termenv
 open Evd
+open Environ
 open Proof_trees
-open Trad
 open Stock
 open Clenv
 
@@ -25,14 +24,17 @@ type module_mark = Stock.module_mark
 type marked_term = constr Stock.stocked
 
 let rec whd_replmeta = function
-  | DOP0(XTRA("ISEVAR",[])) -> DOP0(Meta (newMETA()))
+  | DOP0(XTRA("ISEVAR")) -> DOP0(Meta (new_meta()))
   | DOP2(Cast,c,_) -> whd_replmeta c
   | c -> c
 
 let raw_sopattern_of_compattern sign com =
+  failwith "raw_sopattern_of_compattern: TODO"
+  (***
   let c = Astterm.raw_constr_of_compattern empty_evd (gLOB sign) com in
   strong whd_replmeta c
-    
+  ***)
+
 let parse_pattern s =
   let com =
     try 
@@ -40,7 +42,7 @@ let parse_pattern s =
     with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
       error "Malformed pattern" 
   in
-  raw_sopattern_of_compattern (initial_sign()) com
+  raw_sopattern_of_compattern (Global.context()) com
     
 let (pattern_stock : constr Stock.stock) =
   Stock.make_stock {name="PATTERN";proc=parse_pattern}
@@ -72,15 +74,15 @@ let get_pat = Stock.retrieve pattern_stock
  *)
 
 let dest_soapp_operator = function
-  | DOPN(XTRA("$SOAPP",[]),v) ->
+  | DOPN(XTRA("$SOAPP"),v) ->
       (match Array.to_list v with
 	 | (DOP0(Meta n))::l ->
              let l' = 
 	       List.map (function (Rel i) -> i | _ -> error "somatch") l in
-             Some (n, Listset.uniquize l')
+             Some (n, list_uniquize l')
 	 | _ -> error "somatch")
-  | (DOP2(XTRA("$SOAPP",[]),DOP0(Meta n),Rel p)) ->
-      Some (n,Listset.uniquize [p])
+  | (DOP2(XTRA("$SOAPP"),DOP0(Meta n),Rel p)) ->
+      Some (n,list_uniquize [p])
   | _ -> None
 
 let constrain ((n:int),(m:constr)) sigma =
@@ -93,7 +95,7 @@ let build_dlam toabstract stk (m:constr) =
   let rec buildrec m p_0 p_1 = match p_0,p_1 with 
     | (_, []) -> m
     | (n, (na::tl)) -> 
-	if Listset.mem n toabstract then
+	if List.mem n toabstract then
           buildrec (DLAM(na,m)) (n+1) tl
         else 
 	  buildrec (pop m) (n+1) tl
@@ -102,8 +104,8 @@ let build_dlam toabstract stk (m:constr) =
 
 let memb_metavars m n =
   match (m,n) with
-    | (None, _)       -> true
-    | ((Some mvs), n) -> Listset.mem n mvs
+    | (None, _)     -> true
+    | (Some mvs, n) -> List.mem n mvs
 	  
 let somatch metavars = 
   let rec sorec stk sigma p t =
@@ -111,9 +113,9 @@ let somatch metavars =
     and cT = whd_castapp t in
     match dest_soapp_operator cP with
       | Some (n,ok_args) ->
-          if (not((memb_metavars metavars n))) then error "somatch";
-	  let frels = free_rels cT in
-	  if Listset.subset frels ok_args then 
+          if not (memb_metavars metavars n) then error "somatch";
+	  let frels = Intset.elements (free_rels cT) in
+	  if list_subset frels ok_args then 
 	    constrain (n,build_dlam ok_args stk cT) sigma
 	  else 
 	    error "somatch"
@@ -121,14 +123,15 @@ let somatch metavars =
       | None ->
 	  match (cP,cT) with
        	    | (DOP0(Meta n),m) ->
-		if (not((memb_metavars metavars n))) then
+		if not (memb_metavars metavars n) then
 		  match m with
 		    | DOP0(Meta m_0) -> 
 			if n=m_0 then sigma else error "somatch"
 		    | _ -> error "somatch"
 		else
 		  let depth = List.length stk in
-        	  if Listset.for_all (fun i -> i > depth) (free_rels m) then
+		  let frels = Intset.elements (free_rels m) in
+        	  if List.for_all (fun i -> i > depth) frels then
 		    constrain (n,lift (-depth) m) sigma
         	  else 
 		    error "somatch"
@@ -153,7 +156,7 @@ let somatch metavars =
 	       
   	    | (DOPN(op1,cl1), DOPN(op2,cl2)) ->
 		if op1 = op2 & Array.length cl1 = Array.length cl2 then
-		  it_vect2 (sorec stk) sigma cl1 cl2
+		  array_fold_left2 (sorec stk) sigma cl1 cl2
 		else 
 		  error "somatch"
 
@@ -168,7 +171,7 @@ let somatch metavars =
 		  
   	    | (DLAMV(_,cl1), DLAMV(na,cl2)) ->
 		if Array.length cl1 = Array.length cl2 then
-		  it_vect2 (sorec (na::stk)) sigma cl1 cl2
+		  array_fold_left2 (sorec (na::stk)) sigma cl1 cl2
 		else 
 		  error "somatch"
 		    
@@ -178,19 +181,20 @@ let somatch metavars =
 
 let somatches n pat =
   let m = get_pat pat in 
-  try somatch None m n; true with UserError _ -> false
+  try let _ = somatch None m n in true with UserError _ -> false
 
 let dest_somatch n pat =
-  let m    = get_pat pat in
-  let mvs  = collect_metas m in
-  let mvb  = somatch (Some (Listset.uniquize mvs)) m n in
+  let m = get_pat pat in
+  let mvs = collect_metas m in
+  let mvb = somatch (Some (list_uniquize mvs)) m n in
   List.map (fun b -> List.assoc b mvb) mvs
 
 let soinstance pat arglist =
-  let m =   get_pat pat in
+  let m = get_pat pat in
   let mvs = collect_metas m in
   let mvb = List.combine mvs arglist in 
-  Sosub.soexecute (Reduction.strong (Reduction.whd_meta mvb) m)
+  Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) 
+		     empty_env Evd.empty m)
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -200,9 +204,7 @@ let soinstance pat arglist =
    since they do not depend on the name of the type. Hence, they 
    also work on ad-hoc disjunctions introduced by the user.
   
-  -- Eduardo (6/8/97).
-
- *)
+  -- Eduardo (6/8/97). *)
 
 let mmk = make_module_marker ["Prelude"]
 
@@ -216,9 +218,9 @@ let match_with_non_recursive_type t =
   match kind_of_term t with 
     | IsAppL _ -> 
         let (hdapp,args) = decomp_app t in
-        (match (kind_of_term hdapp) with
+        (match kind_of_term hdapp with
            | IsMutInd _ -> 
-               if not (mind_is_recursive hdapp) then 
+               if not (Global.mind_is_recursive hdapp) then 
 		 Some (hdapp,args) 
 	       else 
 		 None 
@@ -234,10 +236,10 @@ let match_with_conjunction t =
   let (hdapp,args) = decomp_app t in 
   match kind_of_term hdapp with
     | IsMutInd _ -> 
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in  
+        let nconstr = Global.mind_nconstr hdapp in  
 	if (nconstr = 1) && 
-          (not (mind_is_recursive hdapp)) &&
-          (nb_prod (mind_arity hdapp))=(mind_nparams hdapp)
+          (not (Global.mind_is_recursive hdapp)) &&
+          (nb_prod (Global.mind_arity hdapp)) = (Global.mind_nparams hdapp)
         then 
 	  Some (hdapp,args)
         else 
@@ -254,10 +256,11 @@ let match_with_disjunction t =
   match kind_of_term hdapp with
     | IsMutInd _  -> 
         let constr_types = 
-	  mis_lc_without_abstractions (mind_specif_of_mind hdapp) in
-        let only_one_arg c = ((nb_prod c) - (mind_nparams hdapp)) = 1 in 
-	if (Vectops.for_all_vect only_one_arg constr_types) &&
-          (not (mind_is_recursive hdapp))
+	  Global.mind_lc_without_abstractions hdapp in
+        let only_one_arg c = 
+	  ((nb_prod c) - (Global.mind_nparams hdapp)) = 1 in 
+	if (array_for_all only_one_arg constr_types) &&
+          (not (Global.mind_is_recursive hdapp))
         then 
 	  Some (hdapp,args)
         else 
@@ -270,7 +273,7 @@ let match_with_empty_type t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
     | IsMutInd _ -> 
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in  
+        let nconstr = Global.mind_nconstr hdapp in  
 	if nconstr = 0 then Some hdapp else None
     | _ ->  None
 	  
@@ -281,10 +284,10 @@ let match_with_unit_type t =
   match (kind_of_term hdapp) with
     | IsMutInd _  -> 
         let constr_types = 
-	  mis_lc_without_abstractions (mind_specif_of_mind hdapp) in 
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in
-        let zero_args c = ((nb_prod c) - (mind_nparams hdapp)) = 0 in  
-	if nconstr = 1 && (Vectops.for_all_vect zero_args constr_types) then 
+	  Global.mind_lc_without_abstractions hdapp in 
+        let nconstr = Global.mind_nconstr hdapp in
+        let zero_args c = ((nb_prod c) - (Global.mind_nparams hdapp)) = 0 in  
+	if nconstr = 1 && (array_for_all zero_args constr_types) then 
 	  Some hdapp
         else 
 	  None
@@ -302,10 +305,10 @@ let match_with_equation  t =
   match (kind_of_term hdapp) with
     | IsMutInd _  -> 
         let constr_types = 
-	  mis_lc_without_abstractions (mind_specif_of_mind hdapp) in 
+	  Global.mind_lc_without_abstractions hdapp in 
         let refl_rel_term1 = put_pat mmk "(A:?)(x:A)(? A x x)" in
         let refl_rel_term2 = put_pat mmk "(x:?)(? x x)" in
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in
+        let nconstr = Global.mind_nconstr hdapp in
 	if nconstr = 1 &&
            (somatches constr_types.(0) refl_rel_term1 ||
             somatches constr_types.(0) refl_rel_term2) 
diff --git a/tactics/pattern.mli b/tactics/pattern.mli
index e39ecf9ec8..4cfb482564 100644
--- a/tactics/pattern.mli
+++ b/tactics/pattern.mli
@@ -46,9 +46,9 @@ val make_module_marker : string list -> module_mark
 val put_pat            : module_mark -> string -> marked_term
 val get_pat            : marked_term -> constr
 val pattern_stock      : constr Stock.stock
-(***
+(*i**
 val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
-***)
+**i*)
 
 (*s Second part : Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
@@ -70,7 +70,7 @@ val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
    contained in the arguments of the application, and in that case, we
    construct a [DLAM] with the names on the stack. *)
 
-val somatch      : Intset.t option -> constr -> constr -> constr Intmap.t
+val somatch      : int list option -> constr -> constr -> (int * constr) list
 val somatches    : constr -> marked_term -> bool
 val dest_somatch : constr -> marked_term -> constr list
 val soinstance   : marked_term -> constr list -> constr 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 56cd5a42f9..49c384df4a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -190,7 +190,7 @@ fois pour toutes : en particulier si Pattern.somatch produit une UserError
 Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
 si après Intros la conclusion matche le pattern.
 *)
-(***
+(***TODO
 let conclPattern concl pat tacast gl = 
   let constr_bindings = Pattern.somatch None pat concl in
   let ast_bindings = 
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
new file mode 100644
index 0000000000..44f17e8165
--- /dev/null
+++ b/tactics/wcclausenv.ml
@@ -0,0 +1,207 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Reduction
+open Environ
+open Logic
+open Tacmach
+open Evd
+open Proof_trees
+open Clenv
+
+(* If you have a precise idea of the intended use of the following code, please
+   write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
+   -- Eduardo (11/8/97) *)
+
+let pf_get_new_id id gls = 
+  next_ident_away id (ids_of_sign (pf_untyped_hyps gls))
+
+let pf_get_new_ids ids gls =
+  let avoid = ids_of_sign (pf_untyped_hyps gls) in
+  List.fold_right
+    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
+    ids []
+
+type arg_binder =
+  | Dep of identifier
+  | Nodep of int
+  | Abs of int
+
+type arg_bindings = (arg_binder * constr) list
+
+let clenv_constrain_with_bindings bl clause =
+  if bl = [] then 
+    clause 
+  else 
+    let all_mvs = collect_metas (clenv_template clause).rebus
+    and ind_mvs = clenv_independent clause
+		    (clenv_template clause,
+                     clenv_template_type clause) in
+    let nb_indep = List.length ind_mvs in
+    let rec matchrec clause = function
+      | []       -> clause
+      | (b,c)::t ->
+          let k = 
+            match b with
+              | Dep s ->
+		  if List.mem_assoc b t then 
+		    errorlabstrm "clenv_match_args" 
+                      [< 'sTR "The variable "; print_id s; 
+			 'sTR " occurs more than once in binding" >];
+		  clenv_lookup_name clause s
+              | Nodep n ->
+		  let index = if n > 0 then n-1 else nb_indep+n in
+                  if List.mem_assoc (Nodep (index+1)) t or 
+                    List.mem_assoc (Nodep (index-nb_indep)) t
+                  then errorlabstrm "clenv_match_args"
+                    [< 'sTR "The position "; 'iNT n ;
+		       'sTR " occurs more than once in binding" >];
+		  (try 
+		     List.nth ind_mvs index
+		   with Failure _ ->
+                     errorlabstrm "clenv_constrain_with_bindings"
+                       [< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
+                          'sTR" unnamed argument" >])
+              | Abs n -> 
+                  (try
+                     if n > 0 then 
+		       List.nth all_mvs (n-1)
+                     else if n < 0 then 
+		       List.nth (List.rev all_mvs) (-n-1)
+                     else error "clenv_constrain_with_bindings" 
+                   with Failure _ ->
+                     errorlabstrm "clenv_constrain_with_bindings"
+                       [< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
+                          'sTR" absolute argument" >])
+	  in
+	  let env = Global.unsafe_env () in
+	  let sigma = Evd.empty in
+	  let k_typ = nf_betaiota env sigma (clenv_instance_type clause k) in
+	  let c_typ = nf_betaiota env sigma (w_type_of clause.hook c) in 
+	  matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t
+    in 
+    matchrec clause bl
+
+(***TODO: SUPPRIMMER ??
+let add_prod_rel sigma (t,env) =
+  match t with
+    | DOP2(Prod,c1,(DLAM(na,b))) ->
+        (b,add_rel (na,Typing_ev.execute_type sigma env c1) env)
+    | _ -> failwith "add_prod_rel"
+
+let rec add_prods_rel sigma (t,env) =
+  try 
+    add_prods_rel sigma (add_prod_rel sigma (whd_betadeltaiota sigma t,env))
+  with Failure "add_prod_rel" -> 
+    (t,env)
+
+let add_prod_sign sigma (t,sign) =
+  match t with
+    | DOP2(Prod,c1,(DLAM(na,_) as b)) ->
+        let id = Environ.id_of_name_using_hdchar t na in  
+	(sAPP b (VAR id),
+         add_sign (id, fexecute_type sigma sign c1) sign)
+    | _ -> failwith "add_prod_sign"
+
+let rec add_prods_sign sigma (t,sign) =
+  try 
+    add_prods_sign sigma (add_prod_sign sigma (whd_betadeltaiota sigma t,sign))
+  with Failure "add_prod_sign" -> 
+    (t,sign)
+***)
+
+(* What follows is part of the contents of the former file tactics3.ml *)
+    
+let res_pf_THEN kONT clenv tac gls =
+  let clenv' = (clenv_unique_resolver false clenv gls) in 
+  (tclTHEN (clenv_refine kONT clenv') (tac clenv')) gls
+
+let res_pf_THEN_i kONT clenv tac i gls =
+  let clenv' = (clenv_unique_resolver false clenv gls) in 
+  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+
+let elim_res_pf_THEN_i kONT clenv tac i gls =  
+  let clenv' = (clenv_unique_resolver true clenv gls) in
+  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+
+let rec build_args acc ce p_0 p_1 =
+  match p_0,p_1 with 
+    | ((DOP2(Prod,a,(DLAM(na,_) as b))), (a_0::bargs)) ->
+        let (newa,ce') = (build_term ce (na,Some a) a_0) in 
+	build_args (newa::acc) ce' (sAPP b a_0) bargs
+    | (_, [])     -> (List.rev acc,ce)
+    | (_, (_::_)) -> failwith "mk_clenv_using"
+
+and build_term ce p_0 p_1 =
+  let env = Global.unsafe_env() in
+  match p_0,p_1 with 
+    | ((na,Some t), (DOP0(Meta mv))) -> 
+        build_term ce (na,Some t) mkExistential
+    | ((na,Some t), (DOP0(XTRA("ISEVAR")))) ->
+    	let mv = new_meta() in 
+	(DOP0(Meta mv),
+         clenv_pose (na,mv,t) ce)
+    | ((na,_), (DOP2(Cast,c,t))) -> build_term ce (na,Some t) c
+    | ((na,Some t), c) ->
+    	if (not((occur_meta c))) then 
+	  (c,ce)
+    	else 
+	  let (hd,args) = 
+	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in
+          let hdty = w_type_of ce.hook hd in
+          let (args,ce') =
+	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
+          let newc = applist(hd,args) in
+          let t' = clenv_type_of ce' newc in  
+	  if w_conv_x ce'.hook t t' then 
+	    (newc,ce') 
+	  else 
+	    failwith "mk_clenv_using"
+    | ((na,None), c) ->
+    	if (not((occur_meta c))) then 
+	  (c,ce)
+    	else 
+	  let (hd,args) = 
+	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in
+          let hdty = w_type_of ce.hook hd in
+          let (args,ce') = 
+	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
+          let newc = applist(hd,args) in
+	  (newc,ce')
+
+let mk_clenv_using wc c =
+  let ce = mk_clenv wc mkImplicit in
+  let (newc,ce') = 
+    try 
+      build_term ce (Anonymous,None) c
+    with Failure _ -> 
+      raise (RefinerError (NotWellTyped c))
+  in
+  clenv_change_head (newc,clenv_type_of ce' newc) ce'
+
+let applyUsing c gl =
+  let (wc,kONT) = startWalk gl in
+  let clause = mk_clenv_using wc c in 
+  res_pf kONT clause gl
+
+let clenv_apply_n_times n ce =
+  let templtyp = clenv_instance_template_type ce
+  and templval = (clenv_template ce).rebus in   
+  let rec apprec ce argacc (n,ty) =
+    let env = Global.unsafe_env () in
+    match (n, whd_betadeltaiota env (w_Underlying ce.hook) ty) with 
+      | (0, templtyp) ->
+	  clenv_change_head (applist(templval,List.rev argacc), templtyp) ce
+      | (n, (DOP2(Prod,dom,DLAM(na,rng)))) ->
+          let mv = new_meta() in
+          let newce = clenv_pose (na,mv,dom) ce in
+	  apprec newce (mkMeta mv::argacc) (n-1, subst1 (mkMeta mv) rng)
+      | (n, _) -> failwith "clenv_apply_n_times"
+  in 
+  apprec ce [] (n, templtyp)
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 88d14d3602..3cea47392d 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -24,6 +24,7 @@ type arg_bindings = (arg_binder * constr) list
 val clenv_constrain_with_bindings :
   arg_bindings -> walking_constraints clausenv -> walking_constraints clausenv
 
+(*i**
 val add_prod_rel : 'a evar_map -> constr * context -> constr * context
 
 val add_prods_rel : 'a evar_map -> constr * context -> constr * context
@@ -33,6 +34,7 @@ val add_prod_sign :
 
 val add_prods_sign : 
   'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+**i*)
 
 val res_pf_THEN         : (walking_constraints -> tactic) -> 
                            walking_constraints clausenv ->