Portage d'AutoRewrite

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

6 files changed, 161 insertions, 92 deletions

diff --git a/tactics/AutoRewrite.v b/tactics/AutoRewrite.v
new file mode 100644
index 000000000..531f4ee91
--- /dev/null
+++ b/tactics/AutoRewrite.v
@@ -0,0 +1,25 @@
+Declare ML Module "autorewrite".
+
+Grammar vernac orient : ast :=
+| lr ["->"] -> ["LR"]
+| rl ["<-"] -> ["RL"]
+| ng [] -> ["LR"]
+
+with vernac : ast :=
+| hint_rew_b [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
+  identarg($b) "."] -> [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b) ]
+| hint_rew_t [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
+  identarg($b) "using" tacarg($t) "." ] ->
+  [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC $t)) ].
+
+Grammar tactic simple_tactic : ast :=
+| auto_rew_b [ "AutoRewrite" "[" ne_identarg_list($l) "]" ] ->
+  [ (AutoRewrite ($LIST $l)) ]
+| auto_rew_t [ "AutoRewrite" "[" ne_identarg_list($l) "]" "using"
+  tactic($t) ] -> [ (AutoRewrite (TACTIC $t) ($LIST $l)) ].
+
+Syntax tactic level 0:
+| auto_rew_b [<<(AutoRewrite $l)>>] ->
+  [ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" ]
+| auto_rew_t [<<(AutoRewrite $t $l)>>] ->
+  [ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" [1 0] "using" [1 0] $t ].
diff --git a/tactics/Equality.v b/tactics/Equality.v
index 971d1e72c..057e6f900 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -3,71 +3,6 @@
 
 Declare ML Module "equality".
 
-Grammar vernac orient_rule: ast :=
-   lr ["LR"] -> [ "LR" ]
-  |rl ["RL"] -> [ "RL" ]
-with rule_list: ast list :=
-   single_rlt [ constrarg($com) orient_rule($ort) ] ->
-     [ (VERNACARGLIST $com $ort) ]
-  |recursive_rlt [ constrarg($com) orient_rule($ort) rule_list($tail)] ->
-    [ (VERNACARGLIST $com $ort) ($LIST $tail) ]
-with base_list: ast list :=
-   single_blt [identarg($rbase) "[" rule_list($rlt) "]"] ->
-     [ (VERNACARGLIST $rbase ($LIST $rlt)) ]
-  |recursive_blt [identarg($rbase) "[" rule_list($rlt) "]"
-    base_list($blt)] ->
-    [ (VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt) ]
-with vernac: ast :=
-   addrule ["HintRewrite" base_list($blt) "."] ->
-     [ (HintRewrite ($LIST $blt)) ].
-
-Grammar tactic list_tactics: ast list :=
-   single_lt [tactic($tac)] -> [$tac]
-  |recursive_lt [tactic($tac) "|" list_tactics($tail)] ->
-    [ $tac ($LIST $tail) ]
-
-with step_largs: ast list :=
-   nil_step [] -> []
-  |solve_step ["with" "Solve"] -> [(REDEXP (SolveStep))]
-  |use_step ["with" "Use"] -> [(REDEXP (Use))]
-  |all_step ["with" "All"] -> [(REDEXP (All))]
-
-with rest_largs: ast list :=
-   nil_rest [] -> []
-  |solve_rest ["with" "Solve"] -> [(REDEXP (SolveRest))]
-  |cond_rest ["with" "Cond"] -> [(REDEXP (Cond))]
-
-with autorew_largs: ast list :=
-   step_arg ["Step" "=" "[" list_tactics($ltac) "]" step_largs($slargs)] ->
-    [(REDEXP (Step ($LIST $ltac))) ($LIST $slargs)]
-  |rest_arg ["Rest" "=" "[" list_tactics($ltac) "]" rest_largs($llargs)] ->
-    [(REDEXP (Rest ($LIST $ltac))) ($LIST $llargs)]
-  |depth_arg ["Depth" "=" numarg($dth)] ->
-    [(REDEXP (Depth $dth))]
-
-with list_args_autorew: ast list :=
-   nil_laa [] -> []
-  |recursive_laa [autorew_largs($largs) list_args_autorew($laa)] ->
-    [($LIST $largs) ($LIST $laa)]
-
-with hintbase_list: ast list :=
-  nil_hintbase [] -> []
-| base_by_name [identarg($id) hintbase_list($tail)] -> 
-       [ (REDEXP (ByName $id)) ($LIST $tail)]
-| explicit_base ["[" hintbase($b) "]" hintbase_list($tail)] -> 
-       [(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ]
-
-with hintbase: ast list := 
-  onehint_lr [ constrarg($c) "LR" ] -> [(REDEXP (LR $c))]
-| onehint_rl  [ constrarg($c) "RL" ] -> [(REDEXP (RL $c))]
-| conshint_lr [ constrarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)]
-| conshint_rl [ constrarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)]
-
-with simple_tactic: ast := 
- AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]"
-  list_args_autorew($laa)] ->
-  [(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))].
-
 Grammar tactic simple_tactic: ast :=
   replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
 
@@ -153,26 +88,4 @@ Syntax tactic level 0:
 
 | cutrewriteRL [<<(SubstConcl_RL $eqn)>>] -> ["CutRewrite <- " $eqn:E]
 | cutrewriteRLin [<<(SubstHyp_RL $eqn $id)>>]
-      -> ["CutRewrite <- " $eqn:E [1 1]"in " $id]
-|nil_consbase [<<(CONSBASE)>>] -> []
-|single_consbase [<<(CONSBASE $tac)>>] -> [[1 0] $tac]
-|nil_ortactic [<<(ORTACTIC)>>] -> []
-|single_ortactic [<<(ORTACTIC $tac)>>] -> ["|" $tac]
-|AutoRewrite [<<(AutoRewrite $id)>>] -> ["AutoRewrite " $id]
-|AutoRewriteBaseList [<<(REDEXP (BaseList $ft ($LIST $tl)))>>] ->
-  ["[" $ft (CONSBASE ($LIST $tl)) "]"]
-|AutoRewriteStep [<<(REDEXP (Step $ft ($LIST $tl)))>>] ->
-  [[0 1] "Step=" "[" $ft (ORTACTIC ($LIST $tl)) "]"]
-|AutoRewriteRest [<<(REDEXP (Rest $ft ($LIST $tl)))>>] ->
-  [[0 1] "Rest=" "[" $ft (ORTACTIC ($LIST $tl)) "]"]
-|AutoRewriteSolveStep [<<(REDEXP (SolveStep))>>] -> ["with Solve"]
-|AutoRewriteSolveRest [<<(REDEXP (SolveRest))>>] -> ["with Solve"]
-|AutoRewriteUse [<<(REDEXP (Use))>>] -> ["with Use"]
-|AutoRewriteAll [<<(REDEXP (All))>>] -> ["with All"]
-|AutoRewriteCond [<<(REDEXP (Cond))>>] -> ["with Cond"]
-|AutoRewriteDepth [<<(REDEXP (Depth $dth))>>] -> [[0 1] "Depth=" $dth]
-|AutoRewriteByName [<<(REDEXP (ByName $id))>>] -> [ $id ]
-|AutoRewriteExplicit [<<(REDEXP (Explicit $l))>>] -> ["[" $l "]"]
-|AutoRewriteLR [<<(REDEXP (LR $c))>>] -> [ $c "LR" ]
-|AutoRewriteRL [<<(REDEXP (RL $c))>>] -> [ $c "RL" ]
-.
+      -> ["CutRewrite <- " $eqn:E [1 1]"in " $id].
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
new file mode 100644
index 000000000..921280f3c
--- /dev/null
+++ b/tactics/autorewrite.ml
@@ -0,0 +1,120 @@
+open Ast
+open Coqast
+open Equality
+open Hipattern
+open Names
+open Pp
+open Proof_type
+open Tacmach
+open Tacinterp
+open Tactics
+open Term
+open Util
+open Vernacinterp
+
+(* Summary and Object declaration *)
+let rewtab =
+  ref ((Hashtbl.create 53):(string,constr * bool * tactic) Hashtbl.t)
+
+let lookup id = Hashtbl.find id !rewtab
+
+let _ = 
+  let init () = rewtab := (Hashtbl.create 53) in
+  let freeze () = !rewtab in
+  let unfreeze fs = rewtab := fs in
+  Summary.declare_summary "autorewrite"
+    { Summary.freeze_function   = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function     = init;
+      Summary.survive_section   = false }
+
+(* Rewriting rules *)
+type rew_rule = constr * bool * tactic
+
+(* Applies all the rules of one base *)
+let one_base tac_main bas =
+  let lrul = Hashtbl.find_all !rewtab bas in
+  if lrul = [] then
+    errorlabstrm "AutoRewrite"
+      [<'sTR ("Rewriting base "^(bas)^" does not exist") >]
+  else
+    tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
+      tclTHEN tac
+      (if dir then tclREPEAT_MAIN (tclTHENST (rewriteLR csr) [tac_main] tc)
+       else tclREPEAT_MAIN (tclTHENST (rewriteRL csr) [tac_main] tc))) 
+      tclIDTAC lrul))
+
+(* The AutoRewrite tactic *)
+let autorewrite tac_main lbas =
+  tclREPEAT_MAIN (tclPROGRESS
+    (List.fold_left (fun tac bas -> 
+       tclTHEN tac (one_base tac_main bas)) tclIDTAC lbas))
+
+(* Functions necessary to the library object declaration *)
+let load_hintrewrite _ = ()
+let cache_hintrewrite (_,(rbase,lrl)) =
+  List.iter (fun c -> Hashtbl.add !rewtab rbase c) lrl
+let export_hintrewrite x = Some x
+
+(* Declaration of the Hint Rewrite library object *)
+let (in_hintrewrite,out_hintrewrite)=
+  Libobject.declare_object
+    ("HINT_REWRITE",
+     { Libobject.load_function = load_hintrewrite;
+       Libobject.open_function = cache_hintrewrite;
+       Libobject.cache_function = cache_hintrewrite;
+       Libobject.export_function = export_hintrewrite })
+
+(* To add rewriting rules to a base *)
+let add_rew_rules base lrul =
+  Lib.add_anonymous_leaf (in_hintrewrite (base,lrul))
+
+(* The vernac declaration of HintRewrite *)
+let _ = vinterp_add "HintRewrite"
+  (function
+    | [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id]
+      when ort = "LR" || ort = "RL" ->
+      (fun () ->
+       let (evc,env) = Command.get_current_context () in
+       let lcsr =
+         List.map (function
+	   | Node(loc,"CONSTR",l) ->
+             constr_of_Constr (interp_tacarg
+             (evc,env,[],[],None,Tactic_debug.DebugOff)
+             (Node(loc,"COMMAND",l)))
+           | _ -> bad_vernac_args "HintRewrite") lcom in
+       add_rew_rules (string_of_id id)
+         (List.map (fun csr -> (csr,ort = "LR",tclIDTAC)) lcsr))
+    | [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id;VARG_TACTIC t]
+      when ort = "LR" || ort = "RL" ->
+      (fun () ->
+       let (evc,env) = Command.get_current_context () in
+       let lcsr =
+         List.map (function
+	   | Node(loc,"CONSTR",l) ->
+             constr_of_Constr (interp_tacarg
+             (evc,env,[],[],None,Tactic_debug.DebugOff)
+             (Node(loc,"COMMAND",l)))
+           | _ -> bad_vernac_args "HintRewrite") lcom
+       and tac = Tacinterp.interp t in
+       add_rew_rules (string_of_id id)
+         (List.map (fun csr -> (csr,ort = "LR",tac)) lcsr))
+    | _  -> bad_vernac_args "HintRewrite")
+
+(* To get back the tactic arguments and call AutoRewrite *)
+let v_autorewrite = function
+  | (Tac (t,_))::l ->
+    let lbas =
+      List.map (function 
+	| Identifier id -> string_of_id id
+	| _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in
+    autorewrite t lbas
+  | l ->
+    let lbas = 
+      List.map (function 
+	| Identifier id -> string_of_id id
+	| _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in
+    autorewrite tclIDTAC lbas
+
+(* Declaration of AutoRewrite *)
+let _ = hide_tactic "AutoRewrite" v_autorewrite
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
new file mode 100644
index 000000000..bbbc2b047
--- /dev/null
+++ b/tactics/autorewrite.mli
@@ -0,0 +1,11 @@
+open Tacmach
+open Term
+
+(* Rewriting rules *)
+type rew_rule = constr * bool * tactic
+
+(* To add rewriting rules to a base *)
+val add_rew_rules : string -> rew_rule list -> unit
+
+(* The AutoRewrite tactic *)
+val autorewrite : tactic -> string list -> tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6ba9f0076..8a6291c2d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1572,12 +1572,12 @@ let freeze () = !rew_tab
 let unfreeze ft = rew_tab := ft
 
 (*Declaration of the summary*)
-let _ = 
+(*let _ = 
   Summary.declare_summary "autorewrite"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
-      Summary.survive_section = false }
+      Summary.survive_section = false }*)
 
 (*Adds a list of rules to the rule table*)
 let add_list_rules rbase lrl = 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9dd71b75d..0e26d170e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1698,8 +1698,8 @@ let tclABSTRACT name_op tac gls =
 let dyn_tclABSTRACT = 
   hide_tactic "ABSTRACT"
    (function 
-       | [Tac tac] ->
+       | [Tac (tac,_)] ->
 	   tclABSTRACT None tac
-       | [Identifier s; Tac tac] ->
+       | [Identifier s; Tac (tac,_)] ->
 	   tclABSTRACT (Some s) tac
        | _ -> invalid_arg "tclABSTRACT")