module Pattern, Wcclausenv (interface) et Tacticals

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

6 files changed, 1083 insertions, 1 deletions

diff --git a/tactics/pattern.ml b/tactics/pattern.ml
new file mode 100644
index 000000000..8836631fe
--- /dev/null
+++ b/tactics/pattern.ml
@@ -0,0 +1,334 @@
+
+(* $Id$ *)
+
+open Pp
+open Initial
+open Names
+open Generic
+open Term
+open Reduction
+open Termenv
+open Evd
+open Proof_trees
+open Trad
+open Stock
+open Clenv
+
+(* The pattern table for tactics. *)
+
+(* Description: see the interface. *)
+
+(* First part : introduction of term patterns *)
+
+type module_mark = Stock.module_mark
+
+type marked_term = constr Stock.stocked
+
+let rec whd_replmeta = function
+  | DOP0(XTRA("ISEVAR",[])) -> DOP0(Meta (newMETA()))
+  | DOP2(Cast,c,_) -> whd_replmeta c
+  | c -> c
+
+let raw_sopattern_of_compattern sign com =
+  let c = Astterm.raw_constr_of_compattern empty_evd (gLOB sign) com in
+  strong whd_replmeta c
+    
+let parse_pattern s =
+  let com =
+    try 
+      Pcoq.parse_string Pcoq.Command.command_eoi s 
+    with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
+      error "Malformed pattern" 
+  in
+  raw_sopattern_of_compattern (initial_sign()) com
+    
+let (pattern_stock : constr Stock.stock) =
+  Stock.make_stock {name="PATTERN";proc=parse_pattern}
+
+let make_module_marker = Stock.make_module_marker pattern_stock
+let put_pat = Stock.stock pattern_stock
+let get_pat = Stock.retrieve pattern_stock
+
+(* Second part : Given a term with second-order variables in it,
+   represented by Meta's, and possibly applied using XTRA[$SOAPP] to
+   terms, this function will perform second-order, binding-preserving,
+   matching, in the case where the pattern is a pattern in the sense
+   of Dale Miller.
+
+   ALGORITHM:
+
+   Given a pattern, we decompose it, flattening Cast's and apply's,
+   recursing on all operators, and pushing the name of the binder each
+   time we descend a binder.
+
+   When we reach a first-order variable, we ask that the corresponding
+   term's free-rels all be higher than the depth of the current stack.
+
+   When we reach a second-order application, we ask that the
+   intersection of the free-rels of the term and the current stack be
+   contained in the arguments of the application, and in that case, we
+   construct a DLAM with the names on the stack.
+
+ *)
+
+let dest_soapp_operator = function
+  | 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')
+	 | _ -> error "somatch")
+  | (DOP2(XTRA("$SOAPP",[]),DOP0(Meta n),Rel p)) ->
+      Some (n,Listset.uniquize [p])
+  | _ -> None
+
+let constrain ((n:int),(m:constr)) sigma =
+  if List.mem_assoc n sigma then
+    if eq_constr m (List.assoc n sigma) then sigma else error "somatch"
+  else 
+    (n,m)::sigma
+    
+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
+          buildrec (DLAM(na,m)) (n+1) tl
+        else 
+	  buildrec (pop m) (n+1) tl
+  in 
+  buildrec m 1 stk
+
+let memb_metavars m n =
+  match (m,n) with
+    | (None, _)       -> true
+    | ((Some mvs), n) -> Listset.mem n mvs
+	  
+let somatch metavars = 
+  let rec sorec stk sigma p t =
+    let cP = whd_castapp p 
+    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 
+	    constrain (n,build_dlam ok_args stk cT) sigma
+	  else 
+	    error "somatch"
+
+      | None ->
+	  match (cP,cT) with
+       	    | (DOP0(Meta n),m) ->
+		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
+		    constrain (n,lift (-depth) m) sigma
+        	  else 
+		    error "somatch"
+
+  	    | (VAR v1,VAR v2) ->
+		if v1 = v2 then sigma else error "somatch"
+		  
+  	    | (Rel n1,Rel n2) ->
+		if n1 = n2 then sigma else error "somatch"
+
+  	    | (DOP0 op1,DOP0 op2) ->
+		if op1 = op2 then sigma else error "somatch"
+
+  	    | (DOP1(op1,c1), DOP1(op2,c2)) ->
+		if op1 = op2 then sorec stk sigma c1 c2	else error "somatch"
+	       
+  	    | (DOP2(op1,c1,d1), DOP2(op2,c2,d2)) ->
+		if op1 = op2 then
+		  sorec stk (sorec stk sigma c1 c2) d1 d2
+		else 
+		  error "somatch"
+	       
+  	    | (DOPN(op1,cl1), DOPN(op2,cl2)) ->
+		if op1 = op2 & Array.length cl1 = Array.length cl2 then
+		  it_vect2 (sorec stk) sigma cl1 cl2
+		else 
+		  error "somatch"
+
+  	    | (DOPL(op1,cl1), DOPL(op2,cl2)) ->
+		if op1 = op2 & List.length cl1 = List.length cl2 then
+		  List.fold_left2 (sorec stk) sigma cl1 cl2
+		else 
+		  error "somatch"
+
+  	    | (DLAM(_,c1), DLAM(na,c2)) -> 
+		sorec (na::stk) sigma c1 c2
+		  
+  	    | (DLAMV(_,cl1), DLAMV(na,cl2)) ->
+		if Array.length cl1 = Array.length cl2 then
+		  it_vect2 (sorec (na::stk)) sigma cl1 cl2
+		else 
+		  error "somatch"
+		    
+  	    | _ -> error "somatch"
+    in 
+    sorec [] []
+
+let somatches n pat =
+  let m = get_pat pat in 
+  try somatch None m n; 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
+  List.map (fun b -> List.assoc b mvb) mvs
+
+let soinstance pat arglist =
+  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)
+
+(* I implemented the following functions which test whether a term t
+   is an inductive but non-recursive type, a general conjuction, a
+   general disjunction, or a type with no constructors.
+
+   They are more general than matching with or_term, and_term, etc, 
+   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).
+
+ *)
+
+let mmk = make_module_marker ["Prelude"]
+
+type 'a matching_function = constr -> 'a option
+
+type testing_function  = constr -> bool
+
+let op2bool = function Some _ -> true | None -> false
+
+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
+           | IsMutInd _ -> 
+               if not (mind_is_recursive hdapp) then 
+		 Some (hdapp,args) 
+	       else 
+		 None 
+           | _ -> None)
+    | _ -> None
+
+let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
+
+(* A general conjunction type is a non-recursive inductive type with
+   only one constructor. *)
+
+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  
+	if (nconstr = 1) && 
+          (not (mind_is_recursive hdapp)) &&
+          (nb_prod (mind_arity hdapp))=(mind_nparams hdapp)
+        then 
+	  Some (hdapp,args)
+        else 
+	  None
+    | _ -> None
+
+let is_conjunction t = op2bool (match_with_conjunction t)
+    
+(* A general disjunction type is a non-recursive inductive type all
+   whose constructors have a single argument. *)
+
+let match_with_disjunction t =
+  let (hdapp,args) = decomp_app t in 
+  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))
+        then 
+	  Some (hdapp,args)
+        else 
+	  None
+    | _ -> None
+
+let is_disjunction t = op2bool (match_with_disjunction t)
+
+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  
+	if nconstr = 0 then Some hdapp else None
+    | _ ->  None
+	  
+let is_empty_type t = op2bool (match_with_empty_type t)
+
+let match_with_unit_type t =
+  let (hdapp,args) = decomp_app t in
+  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 
+	  Some hdapp
+        else 
+	  None
+    | _ -> None
+
+let is_unit_type t = op2bool (match_with_unit_type t)
+
+
+(* Checks if a given term is an application of an
+   inductive binary relation R, so that R has only one constructor
+   stablishing its reflexivity.  *)
+
+let match_with_equation  t =
+  let (hdapp,args) = decomp_app t in
+  match (kind_of_term hdapp) with
+    | IsMutInd _  -> 
+        let constr_types = 
+	  mis_lc_without_abstractions (mind_specif_of_mind 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
+	if nconstr = 1 &&
+           (somatches constr_types.(0) refl_rel_term1 ||
+            somatches constr_types.(0) refl_rel_term2) 
+        then 
+	  Some (hdapp,args)
+        else 
+	  None
+    | _ -> None
+
+let is_equation t = op2bool (match_with_equation  t)
+
+let match_with_nottype t =
+  let notpat = put_pat mmk "(?1->?2)" in 
+  try 
+    (match dest_somatch t notpat with
+       | [arg;mind] when is_empty_type mind -> Some (mind,arg)
+       | [arg;mind] -> None
+       | _ -> anomaly "match_with_nottype")
+  with UserError ("somatches",_) -> 
+    None  
+
+let is_nottype t = op2bool (match_with_nottype t)
+		     
+let is_imp_term = function
+  | DOP2(Prod,_,DLAM(_,b)) -> not (dependent (Rel 1) b)
+  | _                      -> false
diff --git a/tactics/pattern.mli b/tactics/pattern.mli
new file mode 100644
index 000000000..e39ecf9ec
--- /dev/null
+++ b/tactics/pattern.mli
@@ -0,0 +1,111 @@
+
+(* $Id$ *)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Evd
+open Proof_trees
+(*i*)
+
+(* The pattern table for tactics. *)
+
+(* The idea is that we want to write tactic files which are only
+   "activated" when certain modules are loaded and imported.  Already,
+   the question of how to store the tactics is hard, and we will not
+   address that here.  However, the question arises of how to store
+   the patterns that we will want to use for term-destructuring, and
+   the solution proposed is that we will store patterns with a
+   "module-marker", telling us which modules have to be open in order
+   to use the pattern.  So we will write:
+   \begin{verbatim}
+   let mark = make_module_marker ["<module-name>";<module-name>;...];;
+   let p1 = put_pat mark "<parseable pattern goes here>";;
+   \end{verbatim}
+   And now, we can use [(get p1)]
+   to get the term which corresponds to this pattern, already parsed
+   and with the global names adjusted.
+
+   In other words, we will have the term which we would have had if we
+   had done an:
+   \begin{verbatim}
+        constr_of_com mt_ctxt (initial_sign()) "<text here>"
+   \end{verbatim}
+   except that it will be computed at module-opening time, rather than
+   at tactic-application time.  The ONLY difference will be that
+   no implicit syntax resolution will happen. *)
+
+(*s First part : introduction of term patterns *)
+
+type module_mark = Stock.module_mark
+type marked_term
+
+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
+(***
+val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
+***)
+
+(*s Second part : Given a term with second-order variables in it,
+   represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
+   terms, this function will perform second-order, binding-preserving,
+   matching, in the case where the pattern is a pattern in the sense
+   of Dale Miller.
+
+   ALGORITHM:
+
+   Given a pattern, we decompose it, flattening casts and apply's,
+   recursing on all operators, and pushing the name of the binder each
+   time we descend a binder.
+
+   When we reach a first-order variable, we ask that the corresponding
+   term's free-rels all be higher than the depth of the current stack.
+
+   When we reach a second-order application, we ask that the
+   intersection of the free-rels of the term and the current stack be
+   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 somatches    : constr -> marked_term -> bool
+val dest_somatch : constr -> marked_term -> constr list
+val soinstance   : marked_term -> constr list -> constr 
+
+val is_imp_term : constr -> bool
+
+(*s I implemented the following functions which test whether a term [t]
+   is an inductive but non-recursive type, a general conjuction, a
+   general disjunction, or a type with no constructors.
+
+   They are more general than matching with [or_term], [and_term], etc, 
+   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). *)
+
+type 'a matching_function = constr -> 'a option
+type testing_function = constr -> bool
+
+val match_with_non_recursive_type : (constr * constr list) matching_function
+val is_non_recursive_type         : testing_function 
+
+val match_with_disjunction : (constr * constr list) matching_function
+val is_disjunction         : testing_function 
+
+val match_with_conjunction : (constr * constr list) matching_function
+val is_conjunction         : testing_function 
+
+val match_with_empty_type  : constr matching_function
+val is_empty_type          : testing_function 
+
+val match_with_unit_type   : constr matching_function
+val is_unit_type           : testing_function 
+
+val match_with_equation    : (constr * constr list) matching_function
+val is_equation            : testing_function 
+
+val match_with_nottype     : (constr * constr) matching_function
+val is_nottype             : testing_function 
diff --git a/tactics/stock.mli b/tactics/stock.mli
index 5c3b44eb9..bbc919514 100644
--- a/tactics/stock.mli
+++ b/tactics/stock.mli
@@ -5,7 +5,7 @@
 open Names
 (*i*)
 
-(* The pattern table for tactics. *)
+(* Module markers. *)
 
 type 'a stock
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
new file mode 100644
index 000000000..1794755ff
--- /dev/null
+++ b/tactics/tacticals.ml
@@ -0,0 +1,447 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Inductive
+open Reduction
+open Environ
+open Declare
+open Tacmach
+open Proof_trees
+open Clenv
+open Pattern
+open Wcclausenv
+
+(******************************************)
+(*         Basic Tacticals                *)
+(******************************************)
+
+let tclIDTAC         = Tacmach.tclIDTAC
+let tclORELSE        = Tacmach.tclORELSE
+let tclTHEN          = Tacmach.tclTHEN
+let tclTHEN_i        = Tacmach.tclTHEN_i
+let tclTHENL         = Tacmach.tclTHENL
+let tclTHENS         = Tacmach.tclTHENS
+let tclREPEAT        = Tacmach.tclREPEAT
+let tclFIRST         = Tacmach.tclFIRST
+let tclSOLVE         = Tacmach.tclSOLVE
+let tclTRY           = Tacmach.tclTRY
+let tclINFO          = Tacmach.tclINFO
+let tclCOMPLETE      = Tacmach.tclCOMPLETE
+let tclAT_LEAST_ONCE = Tacmach.tclAT_LEAST_ONCE
+let tclFAIL          = Tacmach.tclFAIL
+let tclDO            = Tacmach.tclDO
+let tclPROGRESS      = Tacmach.tclPROGRESS
+let tclWEAK_PROGRESS = Tacmach.tclWEAK_PROGRESS
+
+(* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
+(* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
+let tclMAP tacfun l = 
+  List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
+
+let dyn_tclIDTAC = function [] -> tclIDTAC |  _ -> anomaly "tclIDTAC"
+
+let dyn_tclFAIL  = function [] -> tclFAIL |  _ -> anomaly "tclFAIL"
+
+let tclTHEN_i1 tac1 tac2 = tclTHEN_i tac1 tac2 1
+
+(* apply a tactic to the nth element of the signature  *)
+
+let tclNTH_HYP m (tac:constr->tactic) gl =
+  tac (try VAR(fst(nth_sign (pf_untyped_hyps gl) m)) 
+       with Failure _ -> error "No such assumption") gl
+
+(* apply a tactic to the last element of the signature  *)
+
+let tclLAST_HYP = tclNTH_HYP 1
+
+let tclTRY_sign (tac:constr->tactic) sign gl =
+  let rec arec = function
+    | []      -> tclFAIL
+    | [s]     -> tac (VAR(s)) (* added in order to get useful error messages *)
+    | (s::sl) -> tclORELSE (tac (VAR(s))) (arec sl) 
+  in 
+  arec (fst sign) gl
+
+let tclTRY_HYPS (tac:constr->tactic) gl = 
+  tclTRY_sign tac (pf_untyped_hyps gl) gl
+
+(* OR-branch *)
+let tryClauses tac = 
+  let rec firstrec = function
+    | []      -> tclFAIL
+    | [cls]   -> tac cls (* added in order to get a useful error message *)
+    | cls::tl -> (tclORELSE (tac cls) (firstrec tl))
+  in 
+  firstrec
+
+(***************************************)
+(*           Clause Tacticals          *)
+(***************************************)
+
+(* The following functions introduce several tactic combinators and
+   functions useful for working with clauses. A clause is either None
+   or (Some id), where id is an identifier. This type is useful for
+   defining tactics that may be used either to transform the
+   conclusion (None) or to transform a hypothesis id (Some id).  --
+   --Eduardo (8/8/97) 
+*)
+
+(* The type of clauses *)
+
+type clause = identifier option
+
+(* A clause corresponding to the |n|-th hypothesis or None *)
+
+let nth_clause n gl =
+  if n = 0 then 
+    None
+  else if n < 0 then 
+    let id = List.nth (ids_of_sign (pf_untyped_hyps gl)) (-n-1) in 
+    Some id
+  else 
+    let id = List.nth (ids_of_sign (pf_untyped_hyps gl)) (n-1) in 
+    Some id
+
+(* Gets the conclusion or the type of a given hypothesis *)
+
+let clause_type cls gl =
+  match cls with
+    | None    -> pf_concl gl
+    | Some id -> pf_get_hyp gl id
+
+(* Functions concerning matching of clausal environments *)
+
+let matches gls n pat =
+  let m = get_pat pat in
+  let (wc,_) = startWalk gls in 
+  try let _ = Clenv.unify_0 [] wc m n in true with UserError _ -> false
+
+let dest_match gls n pat =
+  let m       = get_pat pat in
+  let mvs     = collect_metas m in
+  let (wc,_)  = startWalk gls in
+  let (mvb,_) = Clenv.unify_0 [] wc m n in 
+  List.map (fun x -> List.assoc x mvb) mvs
+
+
+(* [OnCL clausefinder clausetac]
+ * executes the clausefinder to find the clauses, and then executes the
+ * clausetac on the list so obtained. *)
+
+let onCL cfind cltac gl = cltac (cfind gl) gl
+
+
+(* Create a clause list with all the hypotheses from the context *)
+
+let allHyps gl = (List.map in_some (ids_of_sign (pf_untyped_hyps gl)))
+
+
+(* Create a clause list with all the hypotheses from the context, occuring
+   after id *)
+
+let afterHyp id gl =
+  List.map in_some
+    (fst (list_splitby (fun hyp -> hyp = id) 
+	    (ids_of_sign (pf_untyped_hyps gl))))
+    
+
+(* Create a singleton clause list with the last hypothesis from then context *)
+
+let lastHyp gl = 
+  let (id,_) = hd_sign (pf_untyped_hyps gl) in [(Some id)]
+
+(* Create a clause list with the n last hypothesis from then context *)
+
+let nLastHyps n gl =
+  let ids =
+    try list_firstn n (ids_of_sign (pf_untyped_hyps gl))
+    with Failure "firstn" -> error "Not enough hypotheses in the goal"
+  in 
+  List.map in_some ids
+
+
+(* A clause list with the conclusion and all the hypotheses *)
+
+let allClauses gl = 
+  let ids = ids_of_sign(pf_untyped_hyps gl) in  
+  (None::(List.map in_some ids))
+
+let onClause t cls gl  = t cls gl
+let tryAllHyps     tac = onCL allHyps (tryClauses tac)
+let tryAllClauses  tac = onCL allClauses (tryClauses tac)
+let onAllClauses   tac = onCL allClauses (tclMAP tac)
+let onAllClausesLR tac = onCL (compose List.rev allClauses) (tclMAP tac)
+let onLastHyp      tac = onCL lastHyp (tclMAP tac)
+let onNLastHyps n  tac = onCL (nLastHyps n) (tclMAP tac)
+let onNthLastHyp n tac gls = tac (nth_clause n gls) gls
+
+(* Serait-ce possible de compiler d'abord la tactique puis de faire la
+   substitution sans passer par bdize dont l'objectif est de préparer un
+   terme pour l'affichage ? (HH) *)
+
+(* Si on enlève le dernier argument (gl) conclPattern est calculé une
+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.
+*)
+(***
+let conclPattern concl pat tacast gl = 
+  let constr_bindings = Pattern.somatch None pat concl in
+  let ast_bindings = 
+    List.map 
+      (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c))
+      constr_bindings in 
+  let tacast' = CoqAst.subst_meta ast_bindings tacast in
+    Tacinterp.interp tacast' gl
+***)
+
+let clauseTacThen tac continuation =
+  (fun cls -> (tclTHEN (tac cls) continuation))
+
+let if_tac pred tac1 tac2 gl =
+  if pred gl then tac1 gl else tac2 gl
+
+let ifOnClause pred tac1 tac2 cls gl =
+  if pred (cls,clause_type cls gl) then
+    tac1 cls gl
+  else 
+    tac2 cls gl
+
+(***************************************)
+(*         Elimination Tacticals       *)
+(***************************************)
+
+(* The following tacticals allow to apply a tactic to the
+   branches generated by the application of an elimination
+  tactic. 
+
+  Two auxiliary types --branch_args and branch_assumptions-- are
+  used to keep track of some information about the ``branches'' of 
+  the elimination. *)
+
+type branch_args = {
+  ity        : constr;      (* the type we were eliminating on *)
+  largs      : constr list; (* its arguments *)
+  branchnum  : int;         (* the branch number *)
+  pred       : constr;      (* the predicate we used *)
+  nassums    : int;         (* the number of assumptions to be introduced *)
+  branchsign : bool list}   (* the signature of the branch.
+                               true=recursive argument, false=constant *)
+
+type branch_assumptions = {
+  ba        : branch_args;     (* the branch args *)
+  assums    : identifier list; (* the list of assumptions introduced *)
+  cargs     : identifier list; (* the constructor arguments *)
+  constargs : identifier list; (* the CONSTANT constructor arguments *)
+  recargs   : identifier list; (* the RECURSIVE constructor arguments *)
+  indargs   : identifier list} (* the inductive arguments *)
+
+
+(* Hum ... the following function looks quite similar to the one 
+ * defined with the same name in Tactics.ml. 
+ *  --Eduardo (11/8/97) *)
+
+let reduce_to_ind gl t = 
+  let rec elimrec t l = 
+    match decomp_app(t) with
+      | (DOPN(MutInd (sp,_),_) as mind,_) -> 
+	  (mind,mind_path mind,t,prod_it t l)
+      | (DOPN(Const _,_),_) -> 
+	  elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t)) l
+      | (DOP2(Cast,c,_),[]) -> elimrec c l
+      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
+      | _ -> error "Not an inductive product"
+  in 
+  elimrec t []
+
+let case_sign ity i = 
+  let rec analrec acc = function 
+    | [] -> acc 
+    | (c::rest) -> analrec (false::acc) rest
+  in
+  let recarg = mis_recarg (lookup_mind_specif ity (Global.unsafe_env())) in 
+  analrec [] recarg.(i-1)
+
+let elim_sign ity i =
+  let (_,j,_) = destMutInd ity in
+  let rec analrec acc = function 
+    | (Param(_)::rest) -> analrec (false::acc) rest
+    | (Norec::rest)    -> analrec (false::acc) rest
+    | (Imbr(_)::rest)  -> analrec (false::acc) rest
+    | (Mrec k::rest)   -> analrec ((j=k)::acc) rest
+    | []               -> List.rev acc 
+  in 
+  let recarg = mis_recarg (lookup_mind_specif ity (Global.unsafe_env())) in
+  analrec [] recarg.(i-1)
+
+let sort_of_goal gl = 
+  match hnf_type_of gl (pf_concl gl) with 
+    | DOP0(Sort s) -> s
+    | _            -> anomaly "goal should be a type"
+
+
+(* Find the right elimination suffix corresponding to the sort of the goal *)
+(* c should be of type A1->.. An->B with B an inductive definition *)
+
+let suff gl cl = match hnf_type_of gl cl with
+  | DOP0(Sort(Type(_)))    -> "_rect"
+  | DOP0(Sort(Prop(Null))) -> "_ind"
+  | DOP0(Sort(Prop(Pos)))  -> "_rec"
+  | _                      -> anomaly "goal should be a type"
+
+(* Look up function for the default elimination constant *)
+
+let lookup_eliminator sign path suff =
+  let name = id_of_string ((string_of_id (basename path)) ^ suff) in
+  try 
+    Declare.global_reference (kind_of_path path) name
+  with UserError _ -> 
+    VAR(fst(lookup_glob name (gLOB sign)))
+
+let last_arg = function
+  | DOPN(AppL,cl) -> cl.(Array.length cl - 1)
+  | _ -> anomaly "last_arg"
+
+let general_elim_then_using 
+  elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl =
+  let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let name_elim =
+    (match elim with
+       | DOPN(Const sp,_) -> id_of_string(string_of_path sp)
+       | VAR id -> id
+       | _ -> id_of_string " ") 
+  in
+  (* applying elimination_scheme just a little modified *)
+  let (wc,kONT)  = startWalk gl in
+  let indclause  = mk_clenv_from wc (c,t) in
+  let indclause' = clenv_constrain_with_bindings indbindings indclause in
+  let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in
+  let indmv  = 
+    match last_arg (clenv_template elimclause).rebus with
+      | DOP0(Meta mv) -> mv
+      | _            -> error "elimination"
+  in
+  let pmv = 
+    match decomp_app (clenv_template_type elimclause).rebus with
+      | (DOP0(Meta(p)),oplist) -> p
+      | _ -> error ("The elimination combinator " ^
+                    (string_of_id name_elim) ^ " is not known") 
+  in
+  let elimclause' = clenv_fchain indmv elimclause indclause' in
+  let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in
+  let after_tac ce i gl =
+    let (hd,largs) = decomp_app (clenv_template_type ce).rebus in
+    let branchsign =  elim_sign_fun ity i in
+    let ba = { branchsign = branchsign;
+               nassums = 
+		 List.fold_left 
+                   (fun acc b -> if b then acc+2 else acc+1) 0 branchsign;
+               branchnum = i;
+               ity = ity;
+               largs = List.map (clenv_instance_term ce) largs;
+               pred = clenv_instance_term ce hd }
+    in 
+    tac ba gl 
+  in
+  let elimclause' =
+    match predicate with
+       | None   -> elimclause'
+       | Some p -> clenv_assign pmv p elimclause'
+  in 
+  elim_res_pf_THEN_i kONT elimclause' after_tac 1 gl
+
+
+let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
+  let (ity,path_name,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let elim = 
+    lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl))
+  in
+  general_elim_then_using
+    elim elim_sign tac predicate (indbindings,elimbindings) c gl
+
+
+let elimination_then tac        = elimination_then_using tac None 
+let simple_elimination_then tac = elimination_then tac ([],[])
+
+let case_then_using tac predicate (indbindings,elimbindings) c gl =
+  (* finding the case combinator *)
+  let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let sigma = project gl in 
+  let sort  = sort_of_goal gl  in
+  let elim  = Indrec.make_case_gen sigma ity sort in  
+  general_elim_then_using 
+    elim case_sign tac predicate (indbindings,elimbindings) c gl
+
+let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
+  (* finding the case combinator *)
+  let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let sigma = project gl in 
+  let sort  = sort_of_goal gl  in
+  let elim  = Indrec.make_case_nodep sigma ity sort in  
+  general_elim_then_using 
+    elim case_sign tac predicate (indbindings,elimbindings) c gl
+
+
+let make_elim_branch_assumptions ba gl =   
+  let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
+    match lb,lc with 
+      | ([], _) -> 
+          { ba = ba;
+            assums    = assums;
+            cargs     = cargs;
+            constargs = constargs;
+            recargs   = recargs;
+            indargs   = indargs}
+      | ((true::tl), (recarg::indarg::idtl)) ->
+	  makerec (recarg::indarg::assums,
+		   recarg::cargs,
+		   recarg::recargs,
+		   constargs,
+		   indarg::indargs) tl idtl
+      | ((false::tl), (constarg::idtl))      ->
+	  makerec (constarg::assums,
+		   constarg::cargs,
+		   constarg::constargs,
+		   recargs,
+		   indargs) tl idtl
+      | (_, _) -> error "make_elim_branch_assumptions"
+  in 
+  makerec ([],[],[],[],[]) ba.branchsign
+    (try firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl))
+     with Failure _ -> anomaly "make_elim_branch_assumptions")
+
+let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
+
+let make_case_branch_assumptions ba gl =
+  let rec makerec (assums,cargs,constargs,recargs) p_0 p_1 =
+    match p_0,p_1 with 
+      | ([], _) -> 
+          { ba = ba;
+            assums    = assums;
+            cargs     = cargs;
+            constargs = constargs;
+            recargs   = recargs;
+            indargs   = []}
+      | ((true::tl), (recarg::idtl)) ->
+	  makerec (recarg::assums,
+		   recarg::cargs,
+		   recarg::recargs,
+		   constargs) tl idtl
+      | ((false::tl), (constarg::idtl)) ->
+	  makerec (constarg::assums,
+		   constarg::cargs,
+		   recargs,
+		   constarg::constargs) tl idtl
+      | (_, _) -> error "make_case_branch_assumptions"
+  in 
+  makerec ([],[],[],[]) ba.branchsign
+    (try firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl))
+     with Failure _ -> anomaly "make_case_branch_assumptions")
+
+let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
new file mode 100644
index 000000000..1ebd64f43
--- /dev/null
+++ b/tactics/tacticals.mli
@@ -0,0 +1,131 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Tacmach
+open Proof_trees
+open Clenv
+open Reduction
+open Pattern
+open Wcclausenv
+(*i*)
+
+val tclIDTAC         : tactic
+val tclORELSE        : tactic -> tactic -> tactic
+val tclTHEN          : tactic -> tactic -> tactic
+val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
+val tclTHENL         : tactic -> tactic -> tactic
+val tclTHENS         : tactic -> tactic list -> tactic
+val tclREPEAT        : tactic -> tactic
+val tclFIRST         : tactic list -> tactic
+val tclTRY           : tactic -> tactic
+val tclINFO          : tactic -> tactic
+val tclCOMPLETE      : tactic -> tactic
+val tclAT_LEAST_ONCE : tactic -> tactic
+val tclFAIL          : tactic
+val tclDO            : int -> tactic -> tactic
+val tclPROGRESS      : tactic -> tactic
+val tclWEAK_PROGRESS : tactic -> tactic
+val tclNTH_HYP       : int -> (constr -> tactic) -> tactic
+val tclMAP           : ('a -> tactic) -> 'a list -> tactic
+val tclLAST_HYP      : (constr -> tactic) -> tactic
+val tclTRY_sign      : (constr -> tactic) -> constr signature -> tactic
+val tclTRY_HYPS      : (constr -> tactic) -> tactic
+
+val dyn_tclIDTAC     : tactic_arg list -> tactic
+val dyn_tclFAIL      : tactic_arg list -> tactic
+
+(* Clause tacticals *)
+
+type clause = identifier option
+
+val tclTHEN_i1     : tactic -> (int -> tactic) -> tactic
+val nth_clause  : int -> goal sigma -> clause
+val clause_type : clause -> goal sigma -> constr
+
+val matches      : goal sigma -> constr -> marked_term -> bool
+val dest_match   : goal sigma -> constr -> marked_term -> constr list
+
+val allHyps    : goal sigma -> clause list
+val afterHyp   : identifier -> goal sigma -> clause list
+val lastHyp    : goal sigma -> clause  list
+val nLastHyps  : int -> goal sigma -> clause list
+val allClauses : goal sigma -> clause list
+
+val onCL           : (goal sigma -> clause list) -> 
+                     (clause list -> tactic) -> tactic
+val tryAllHyps     : (clause -> tactic) -> tactic
+val tryAllClauses  : (clause -> tactic) -> tactic
+val onAllClauses   : (clause -> tactic) -> tactic
+val onClause       : (clause -> tactic) -> clause -> tactic
+val onAllClausesLR : (clause -> tactic) -> tactic
+val onLastHyp      : (clause -> tactic) -> tactic
+val onNthLastHyp   : int -> (clause -> tactic) -> tactic
+val onNLastHyps    : int -> (clause -> tactic) -> tactic
+val clauseTacThen  : (clause -> tactic) -> tactic -> clause -> tactic
+val if_tac         : (goal sigma -> bool) -> tactic -> (tactic) -> tactic
+val ifOnClause     : (clause * constr -> bool) -> 
+                      (clause -> tactic) -> 
+                      (clause -> tactic) -> 
+                       clause -> tactic
+
+(* Usage : [ConclPattern concl pat tacast]
+   if the term concl matches the pattern pat, (in sense of 
+   Pattern.somatches, then replace ?1 ?2 metavars in tacast by the
+   right values to build a tactic *)
+(***
+val conclPattern : constr -> constr -> CoqAst.t -> tactic
+***)
+
+(* Elimination tacticals *)
+
+type branch_args = { 
+  ity        : constr;      (* the type we were eliminating on *)
+  largs      : constr list; (* its arguments *)
+  branchnum  : int;         (* the branch number *)
+  pred       : constr;      (* the predicate we used *)
+  nassums    : int;         (* the number of assumptions to be introduced *)
+  branchsign : bool list }  (* the signature of the branch.
+                               true=recursive argument, false=constant *)
+
+type branch_assumptions = {
+  ba        : branch_args;     (* the branch args *)
+  assums    : identifier list; (* the list of assumptions introduced *)
+  cargs     : identifier list; (* the constructor arguments *)
+  constargs : identifier list; (* the CONSTANT constructor arguments *)
+  recargs   : identifier list; (* the RECURSIVE constructor arguments *)
+  indargs   : identifier list} (* the inductive arguments *)
+
+val sort_of_goal      : goal sigma -> sorts
+val suff              : goal sigma -> constr -> string
+val lookup_eliminator : context -> section_path -> string -> constr
+
+val general_elim_then_using :
+  constr ->  (constr -> int -> bool list) -> 
+    (branch_args -> tactic) -> constr option -> 
+      (arg_bindings * arg_bindings) -> constr -> tactic
+	  
+val elimination_then_using :
+  (branch_args -> tactic) -> constr option -> 
+    (arg_bindings * arg_bindings) -> constr -> tactic
+
+val elimination_then :
+  (branch_args -> tactic) -> 
+    (arg_bindings * arg_bindings) -> constr -> tactic
+
+val case_then_using :
+  (branch_args -> tactic) -> 
+    constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
+
+val case_nodep_then_using :
+  (branch_args -> tactic) -> 
+    constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
+
+val simple_elimination_then :
+  (branch_args -> tactic) -> constr -> tactic
+
+val elim_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic 
+val case_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic 
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
new file mode 100644
index 000000000..88d14d360
--- /dev/null
+++ b/tactics/wcclausenv.mli
@@ -0,0 +1,59 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Evd
+open Proof_trees
+open Tacmach
+open Clenv
+(*i*)
+
+val pf_get_new_id  : identifier      -> goal sigma -> identifier
+val pf_get_new_ids : identifier list -> goal sigma -> identifier list
+
+type arg_binder = 
+  | Dep of identifier 
+  | Nodep of int 
+  | Abs of int
+
+type arg_bindings = (arg_binder * constr) list
+
+val clenv_constrain_with_bindings :
+  arg_bindings -> walking_constraints clausenv -> walking_constraints clausenv
+
+val add_prod_rel : 'a evar_map -> constr * context -> constr * context
+
+val add_prods_rel : 'a evar_map -> constr * context -> constr * context
+
+val add_prod_sign : 
+  'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+
+val add_prods_sign : 
+  'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+
+val res_pf_THEN         : (walking_constraints -> tactic) -> 
+                           walking_constraints clausenv -> 
+                          (walking_constraints clausenv -> tactic) -> tactic
+
+val res_pf_THEN_i       : (walking_constraints -> tactic) -> 
+                           walking_constraints clausenv -> 
+                          (walking_constraints clausenv -> int -> tactic) -> 
+                           int -> tactic
+
+val elim_res_pf_THEN_i  : (walking_constraints -> tactic) -> 
+                           walking_constraints clausenv -> 
+                          (walking_constraints clausenv -> int -> tactic) -> 
+                            int -> tactic
+
+val mk_clenv_using      : walking_constraints -> constr -> 
+                                     walking_constraints clausenv
+
+val applyUsing          : constr -> tactic
+
+val clenv_apply_n_times : int -> walking_constraints clausenv -> 
+                          walking_constraints clausenv
+
+