Code mort de AutoRewrite

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

2 files changed, 0 insertions, 355 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 72aa724af..73626f07b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1195,324 +1195,6 @@ let substHypInConcl_RL_tac =
    SubstHypInHyp id H.
     id:a=b H:(P a) |- G
 *)
-(*
-(**********************************************************************)
-(*                    AutoRewrite                                     *)
-(**********************************************************************)
-
-(****Dealing with the rewriting rules****)
-
-(* A rewriting is typically an equational constr with an orientation (true=LR
-   and false=RL) *)
-type rewriting_rule = constr * bool
-
-(* The table of rewriting rules. The key is the name of the rule base.  
-   the value is a list of [rewriting_rule] *)
-let rew_tab = ref Gmapl.empty
-
-(*Functions necessary to the summary*)
-let init () = rew_tab := Gmapl.empty
-let freeze () = !rew_tab
-let unfreeze ft = rew_tab := ft
-
-(*Declaration of the summary*)
-(*let _ = 
-  Summary.declare_summary "autorewrite"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_section = false }*)
-
-(*Adds a list of rules to the rule table*)
-let add_list_rules rbase lrl = 
-  List.iter (fun r -> rew_tab := Gmapl.add rbase r !rew_tab) lrl
-
-(*Gives the list of rules for the base named rbase*)
-let rules_of_base rbase = List.rev (Gmapl.find rbase !rew_tab)
-
-(*Functions necessary to the library object declaration*)
-let cache_autorewrite_rule (_,(rbase,lrl)) = add_list_rules rbase lrl
-
-let subst_autorewrite_rule (_,subst,(rbase,list as node)) = 
-  let subst_first (cst,b as pair) = 
-    let cst' = Term.subst_mps subst cst in
-      if cst == cst' then pair else
-	(cst',b)
-  in
-  let list' = list_smartmap subst_first list in
-    if list' == list then node else
-      (rbase,list')
-      
-let classify_autorewrite_rule (_,x) = Libobject.Substitute x
-
-let export_autorewrite_rule x = Some x
-
-(*Declaration of the AUTOREWRITE_RULE library object*)
-let (in_autorewrite_rule,out_autorewrite_rule)=
-  Libobject.declare_object {(Libobject.default_object "AUTOREWRITE_RULE") with
-       Libobject.cache_function = cache_autorewrite_rule;
-       Libobject.open_function = (fun i o -> if i=1 then cache_autorewrite_rule o);
-       Libobject.subst_function = subst_autorewrite_rule;
-       Libobject.classify_function = classify_autorewrite_rule;
-       Libobject.export_function = export_autorewrite_rule }
-
-(****The tactic****)
-
-(*To build the validation function. Length=number of unproven goals, Valid=a
-  validation which solves*)
-type valid_elem =
-  | Length of int
-  | Valid of validation
-
-(* Ce truc devrait aller dans Std -- papageno *)
-(*Gives the sub_list characterized by the indexes i_s and i_e with respect to
-  lref*)
-let sub_list lref i_s i_e =
-  let rec sub_list_rec l i =
-    if i = i_e then
-      l @ [List.nth lref i]
-    else if (i>=i_s) & (i<i_e) then
-      sub_list_rec (l@[List.nth lref i]) (i+1)
-    else
-      anomalylabstrm "Equality.sub_list" (str "Out of range")
-  in
-  sub_list_rec [] i_s
-
-(*Cuts the list l2becut in lists which lengths are given by llth*)
-let cut_list l2becut lval =
-  let rec cut4_1goal cmr l1g = function
-    | [] -> (cmr,l1g)
-    | a::b ->
-	(match a with
-           | Length lth ->
-               if lth = 0 then
-		 cut4_1goal cmr l1g b
-               else
-		 cut4_1goal (cmr+lth) 
-		   (l1g@(sub_list l2becut cmr (cmr+lth-1))) b
-           | Valid p ->
-               cut4_1goal cmr (l1g@[p []]) b)	
-  and cut_list_rec cmr l2b=function
-    | [] -> l2b
-    | a::b ->
-	let (cmr,l1g)=cut4_1goal cmr [] a in
-        cut_list_rec cmr (l2b@[l1g]) b
-  in
-  cut_list_rec 0 [] lval
-
-(*Builds the validation function with lvalid and with respect to l*)
-let validation_gen lvalid l =
-  let (lval,larg_velem) = List.split lvalid in
-  let larg=cut_list l larg_velem in
-  List.fold_left2 (fun a p l -> p ([a]@l)) (List.hd lval (List.hd larg))
-    (List.tl lval) (List.tl larg)
-
-(*Adds the main argument for the last validation function*)
-let mod_hdlist l =
-  match (List.hd l) with
-    | (p,[Length 0]) -> l
-    | (p,larg) -> (p,[Length 1]@larg)::(List.tl l)
-
-(*For the Step options*)
-type option_step=
-  | Solve
-  | Use
-  | All
-
-(* the user can give a base either by a name of by its full definition
-  The definition is an Ast that will find its meaning only in the context
-  of a given goal *)
-type hint_base = 
-  | By_name of identifier
-  | Explicit of (Coqast.t * bool) list
-
-let explicit_hint_base gl = function 
-  | By_name id -> 
-      begin match rules_of_base id with
-	| [] -> errorlabstrm "autorewrite" (str ("Base "^(string_of_id id)^
-						   " does not exist"))
-	| lbs -> lbs
-      end 
-  | Explicit lbs -> 
-      List.map (fun (ast,b) -> (pf_interp_constr gl ast, b)) lbs 
-
-(*AutoRewrite cannot be expressed with a combination of tacticals (due to the
-  options). So, we make it in a primitive way*)
-let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
-  let lst = List.flatten (List.map (explicit_hint_base gls) lbases)
-  and unproven_goals = ref []
-  and fails = ref 0
-  and (sigr,g) = unpackage gls in
-  let put_rewrite lrw = List.map (fun (x,y) -> general_rewrite y x) lrw
-  and nbr_rules = List.length lst in
-  let lst_rew = put_rewrite lst in
-  let rec try2solve_main_goal mgl = function
-    | [] -> None
-    | a::b ->
-        try
-          let (gl_solve,p_solve)=apply_sig_tac sigr a mgl in
-          if gl_solve=[] then
-            Some (gl_solve,p_solve)
-          else
-            try2solve_main_goal mgl b
-        with e when catchable_exception e -> 
-	  try2solve_main_goal mgl b
-  and try_tacs4main_goal mgl = function
-    | [] -> None
-    | a::b ->
-        try
-          Some (apply_sig_tac sigr a mgl)
-        with e when catchable_exception e -> 
-	  try_tacs4main_goal mgl b
-  and try2solve1gen_goal gl = function
-    | [] -> ([gl],Length 1)
-    | a::b ->
-        try
-          let (gl_solve,p_solve)=apply_sig_tac sigr a gl in
-          if gl_solve=[] then
-            ([],Valid p_solve)
-          else
-            try2solve1gen_goal gl b
-        with e when catchable_exception e -> 
-	  try2solve1gen_goal gl b
-  and try2solve_gen_goals (lgls,valg) ltac = function
-    | [] -> (lgls,valg)
-    | a::b ->
-        let (g,elem)=try2solve1gen_goal a ltac in
-        try2solve_gen_goals (lgls@g,valg@[elem]) ltac b
-  and iterative_rew cmr fails (cglob,cmod,warn) unp_goals lvalid =
-    let cmd = ref cmod
-    and wrn = ref warn in
-    if !cmd=depth_step then begin
-      msg_warning (str ((string_of_int cglob)^" rewriting(s) carried out"));
-      cmd := 0;
-      wrn := true
-    end;
-    if fails = nbr_rules then
-      (unp_goals,lvalid,!wrn)
-    else if cmr = nbr_rules then
-      iterative_rew 0 0 (cglob,!cmd,!wrn) unp_goals lvalid
-    else 
-      try
-	let (gl,p) = 
-	  apply_sig_tac sigr (List.nth lst_rew cmr) (List.hd unp_goals) 
-	in
-	let (lgl_gen,lval_gen) =
-	  match ltacrest with
-            | None ->
-		if (List.length gl)=1 then
-		  ([],[])
-		else
-		  (List.tl gl,[Length ((List.length gl)-1)])
-            | Some ltac ->
-		try2solve_gen_goals ([],[]) ltac (List.tl gl)
-	in
-	if opt_rest & (not(lgl_gen=[])) then
-          iterative_rew (cmr+1) (fails+1) (cglob,!cmd,!wrn) unp_goals lvalid
-	else
-          (match ltacstp with
-             | None ->
-                 iterative_rew (cmr+1) fails
-                   (cglob+1,!cmd+1,!wrn) 
-		   ((List.hd gl)::(lgl_gen@(List.tl unp_goals)))
-                   ((p,lval_gen)::lvalid)
-             | Some ltac ->
-                 (match opt_step with
-                    | Solve ->
-			(match (try2solve_main_goal (List.hd gl) ltac) with
-                           | None ->
-                               iterative_rew (cmr+1) fails
-                                 (cglob+1,!cmd+1,!wrn) 
-				 ((List.hd gl)::(lgl_gen@(List.tl unp_goals)))
-                                 ((p,lval_gen)::lvalid)
-                           | Some (gl_solve,p_solve) ->
-                               (lgl_gen@(List.tl unp_goals),
-				(p_solve,[Length 0])::(p,lval_gen)
-				::lvalid,!wrn))
-                    | Use ->	
-			(match (try_tacs4main_goal (List.hd gl) ltac) with
-                           | None ->
-                               iterative_rew (cmr+1) fails
-                                 (cglob+1,!cmd+1,!wrn) 
-				 ((List.hd gl)::(lgl_gen@(List.tl unp_goals)))
-                                 ((p,lval_gen)::lvalid)
-                           | Some(gl_trans,p_trans) ->
-                               let lth=List.length gl_trans in
-                               if lth=0 then
-                                 (lgl_gen@(List.tl unp_goals),
-				  (p_trans,[Length 0])::(p,lval_gen)::lvalid,
-				  !wrn)
-                               else if lth=1 then
-                                 iterative_rew (cmr+1) fails
-                                   (cglob+1,!cmd+1,!wrn)
-                                   (gl_trans@(lgl_gen@(List.tl
-							 unp_goals)))
-                                   ((p_trans,[])::(p,lval_gen)::
-                                    lvalid)
-                               else
-                                 iterative_rew (cmr+1) fails
-                                   (cglob+1,!cmd+1,!wrn)
-                                   (gl_trans@(lgl_gen@(List.tl unp_goals))) 
-				   ((p_trans,
-				     [Length ((List.length gl_trans)-1)])::
-				    (p,lval_gen):: lvalid))
-                    | All ->
-			(match (try2solve_main_goal (List.hd gl) ltac) with
-                           | None ->
-                               (match (try_tacs4main_goal 
-					 (List.hd gl) ltac) with
-                                  | None ->
-                                      iterative_rew (cmr+1) fails
-					(cglob+1,!cmd+1,!wrn)
-					((List.hd
-                                            gl)::(lgl_gen@(List.tl
-							     unp_goals)))
-					((p,lval_gen)::lvalid)
-                                  | Some(gl_trans,p_trans) ->
-                                      let lth = List.length gl_trans in
-                                      if lth = 0 then
-                                        (lgl_gen@(List.tl unp_goals),
-					 (p_trans,[Length 0])::
-					 (p,lval_gen)::lvalid, !wrn)
-                                      else if lth = 1 then
-                                        iterative_rew (cmr+1) fails
-                                          (cglob+1,!cmd+1,!wrn)
-                                          (gl_trans@
-					   (lgl_gen@
-					    (List.tl unp_goals)))
-                                          ((p_trans,[])::
-					   (p,lval_gen)::lvalid)
-                                      else
-                                        iterative_rew (cmr+1) fails
-                                          (cglob+1,!cmd+1,!wrn)
-                                          (gl_trans@
-					   (lgl_gen@
-					    (List.tl unp_goals)))
-                                          ((p_trans,
-					    [Length 
-					       ((List.length gl_trans)-1)])::
-					   (p, lval_gen)::lvalid))
-                           | Some (gl_solve,p_solve) ->
-                               (lgl_gen@(List.tl unp_goals),
-				(p_solve,[Length 0])::
-				(p,lval_gen)::lvalid,!wrn))))
-      with e when catchable_exception e ->
-	iterative_rew (cmr+1) (fails+1) (cglob,!cmd,!wrn) unp_goals lvalid
-    in
-    let (gl,lvalid)=
-      let (gl_res,lvalid_res,warn)=iterative_rew 0 0 (0,0,false) [g] [] in
-      if warn then msgnl (mt ());
-      (gl_res,lvalid_res)
-    in
-    let validation_fun=
-      if lvalid = [] then
-        (fun l -> List.hd l)
-      else
-        let nlvalid=mod_hdlist lvalid in
-        (fun l -> validation_gen nlvalid l)
-    in
-    (repackage sigr gl,validation_fun)
-*)
 
 (* Substitutions tactics (JCF) *)
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 42b0d9b32..e92e251bd 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -88,43 +88,6 @@ val hypSubst_LR : identifier -> clause -> tactic
 val hypSubst_RL : identifier -> clause -> tactic
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
-(*
-(***************)
-(* AutoRewrite *)
-(***************)
-
-(****Dealing with the rewriting rules****)
-
-(*A rewriting is typically an equational constr with an orientation (true=LR
-  and false=RL)*)
-type rewriting_rule = constr * bool
-
-(*Adds a list of rules to the rule table*)
-val add_list_rules : identifier -> rewriting_rule list -> unit
-
-(****The tactic****)
-
-(*For the Step options*)
-type option_step =
-  | Solve
-  | Use
-  | All
-
-(* the user can give a base either by a name of by its full definition
-  The definition is an Ast that will find its meaning only in the context
-  of a given goal *)
-type hint_base = 
-  | By_name of identifier
-  | Explicit of (Coqast.t * bool) list
-
-val explicit_hint_base : goal sigma -> hint_base -> rewriting_rule list
-
-(*AutoRewrite cannot be expressed with a combination of tacticals (due to the
-  options). So, we make it in a primitive way*)
-val autorewrite :
-  hint_base list -> tactic list option -> option_step 
-    -> tactic list option -> bool -> int -> tactic
-*)
 
 (* Subst *)