From 8875508dc4b6a52f62dd8769b1c6ed941aa0d8f0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 15 Jun 2009 09:41:44 +0000 Subject: [PATCH] part of last commit --- .../grafite_engine/grafiteEngine.ml | 38 +++++++++---------- 1 file changed, 18 insertions(+), 20 deletions(-) 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) -> -- 2.39.2