X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=af8b086bfb58a256999d28a49fbe34cc72990f44;hb=4b6193be548c96964beee706b75a06e269eed88d;hp=b0df46ba33c29789eb4514506759af16d78d2fea;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b0df46ba3..af8b086bf 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -571,7 +571,37 @@ let eval_tactical status tac =
   status
 
 let add_obj = GrafiteSync.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj
-      
+
+let eval_ng_punct (_text, _prefix_len, punct) =
+  match punct with
+  | GrafiteAst.Dot _ -> NTactics.dot_tac 
+  | GrafiteAst.Semicolon _ -> fun x -> x
+  | GrafiteAst.Branch _ -> NTactics.branch_tac 
+  | GrafiteAst.Shift _ -> NTactics.shift_tac 
+  | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
+  | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac 
+  | GrafiteAst.Merge _ -> NTactics.merge_tac 
+;;
+
+let eval_ng_tac (text, prefix_len, tac) =
+  match tac with
+  | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
+  | GrafiteAst.NCases (_loc, what, where) ->
+      NTactics.cases_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
+  | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
+  | GrafiteAst.NChange (_loc, pat, ww) -> 
+      NTactics.change_tac 
+       ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NElim (_loc, what, where) ->
+      NTactics.elim_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
+  | GrafiteAst.NId _ -> (fun x -> x)
+  | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+;;
+
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 (text,prefix_len,cmd) ->
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
@@ -672,20 +702,26 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        | _ -> assert false
      in
      let suri = "cic:/ng_matita/" ^ name ^ ".def" in
+     let nlexicon_status =
+       match status.GrafiteTypes.ng_status with
+       | GrafiteTypes.ProofMode _ -> assert false
+       | GrafiteTypes.CommandMode ls -> ls
+     in
      let nmenv, nsubst, nlexicon_status, nty = 
        GrafiteDisambiguate.disambiguate_nterm None
-       LexiconEngine.initial_status [] [] [] (text,prefix_len,ty)
+       nlexicon_status [] [] [] (text,prefix_len,ty)
      in
      let nmenv, nsubst, nlexicon_status, nbo = 
        GrafiteDisambiguate.disambiguate_nterm (Some nty)
-       LexiconEngine.initial_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
+       nlexicon_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
      in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
      prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
      { status with
-        GrafiteTypes.ng_status = Some { NTactics.gstatus = ninitial_stack; 
+        GrafiteTypes.ng_status = 
+           GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; 
           istatus = { 
-            NTactics.pstatus = 
+            NTacStatus.pstatus = 
              NUri.uri_of_string suri, 0, nmenv, nsubst, 
               (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
             lstatus = nlexicon_status} }   
@@ -782,22 +818,14 @@ 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)),[]
-  | GrafiteAst.NTactic (_(*loc*), Some (GrafiteAst.NApply (_loc, t)), punct) ->
+  | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
       (match  status.GrafiteTypes.ng_status with
-      | None -> assert false
-      | Some status ->
-          let nts = NTactics.apply_tac (text,prefix_len,t) status in
-          prerr_endline "esco da apply";
-          NTactics.pp_tac_status nts;
-    (*
-     let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
-     let status = eval_tactical status (tactic_of_ast' tac) in
-      eval_tactical status
-       (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
-     *) assert false)
-  | GrafiteAst.NTactic (_, None, _punct) -> assert false (*
-      eval_tactical status
-       (punctuation_tactical_of_ast (text,prefix_len,punct)),[] *)
+      | GrafiteTypes.CommandMode _ -> assert false
+      | GrafiteTypes.ProofMode nstatus ->
+         let nstatus = eval_ng_tac (text,prefix_len,tac) 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 }, [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status