From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 15 Jun 2009 09:41:44 +0000 (+0000)
Subject: part of last commit
X-Git-Tag: make_still_working~3872
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8875508dc4b6a52f62dd8769b1c6ed941aa0d8f0;p=helm.git

part of last commit
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 1c918ac50..6d7632f75 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -583,13 +583,6 @@ let eval_ng_punct (_text, _prefix_len, punct) =
   | GrafiteAst.Merge _ -> NTactics.merge_tac 
 ;;
 
-let eval_ng_non_punct (_text, _prefix_len, punct) =
-  match punct with
-  | GrafiteAst.Focus (_,l) -> NTactics.focus_tac l
-  | GrafiteAst.Unfocus _ -> NTactics.unfocus_tac
-  | GrafiteAst.Skip _ -> NTactics.skip_tac
-;;
-
 let eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
@@ -607,6 +600,7 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NAuto (_loc, (l,a)) ->
       NTactics.auto_tac
 	~params:(List.map (fun x -> "",0,x) l,a)
+  | GrafiteAst.NBranch _ -> NTactics.branch_tac 
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
         ~what:(text,prefix_len,what)
@@ -615,10 +609,12 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
         ~what:(text,prefix_len,what)
         ~where:(text,prefix_len,where)
+  | GrafiteAst.NFocus (_,l) -> NTactics.focus_tac l
   | GrafiteAst.NGeneralize (_loc, where) -> 
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
@@ -626,11 +622,18 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 
         ~what:(text,prefix_len,what) name
+  | GrafiteAst.NMerge _ -> NTactics.merge_tac 
+  | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
   | GrafiteAst.NReduce (_loc, reduction, where) ->
       NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
      NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
       ~where:(text,prefix_len,where)
+  | GrafiteAst.NSemicolon _ -> fun x -> x
+  | GrafiteAst.NShift _ -> NTactics.shift_tac 
+  | GrafiteAst.NSkip _ -> NTactics.skip_tac
+  | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
+  | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
 ;;
       
 let subst_metasenv_and_fix_names s =
@@ -918,13 +921,17 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Tactic (_, None, punct) ->
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
-  | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
+  | GrafiteAst.NTactic (_(*loc*), tacl) ->
       (match status.GrafiteTypes.ng_status with
       | GrafiteTypes.CommandMode _ -> assert false
       | GrafiteTypes.ProofMode nstatus ->
-         let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
-         let nstatus = subst_metasenv_and_fix_names nstatus in
-         let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
+         let nstatus =
+          List.fold_left 
+            (fun nstatus tac ->
+              let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
+              subst_metasenv_and_fix_names nstatus)
+            nstatus tacl
+         in
          NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
          `New [])
@@ -935,15 +942,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      in
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
-  | GrafiteAst.NNonPunctuationTactical (_, non_punct, punct) ->
-     (match status.GrafiteTypes.ng_status with
-     | GrafiteTypes.CommandMode _ -> assert false
-     | GrafiteTypes.ProofMode nstatus ->
-        let nstatus = eval_ng_non_punct (text,prefix_len,non_punct) nstatus in
-        let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
-        NTacStatus.pp_tac_status nstatus;
-        { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
-        `New [])
   | GrafiteAst.Command (_, cmd) ->
       eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
   | GrafiteAst.Macro (loc, macro) ->