new tactics are almost ready

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 7f5327b56e81a5f1c1244f4cbfb6eff0f7bf6609..b0df46ba33c29789eb4514506759af16d78d2fea 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -665,6 +665,32 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      status, [] (*CSC: TO BE FIXED *)
   | GrafiteAst.Set (loc, name, value) -> status, []
 (*       GrafiteTypes.set_option status name value,[] *)
+  | GrafiteAst.NObj (loc,obj) ->
+     let ty, name = 
+       match obj with
+       | CicNotationPt.Theorem (_,name,ty,_) -> ty, name
+       | _ -> assert false
+     in
+     let suri = "cic:/ng_matita/" ^ name ^ ".def" in
+     let nmenv, nsubst, nlexicon_status, nty = 
+       GrafiteDisambiguate.disambiguate_nterm None
+       LexiconEngine.initial_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)
+     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; 
+          istatus = { 
+            NTactics.pstatus = 
+             NUri.uri_of_string suri, 0, nmenv, nsubst, 
+              (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
+            lstatus = nlexicon_status} }   
+     },
+      []
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -716,7 +742,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
          let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
          { status with GrafiteTypes.proof_status =
             GrafiteTypes.Incomplete_proof
-             { GrafiteTypes.proof = initial_proof; stack = initial_stack } },
+            { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
+         },
           []
      | _ ->
          if metasenv <> [] then
@@ -755,6 +782,22 @@ 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) ->
+      (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)),[] *)
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status