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=7f5327b56e81a5f1c1244f4cbfb6eff0f7bf6609;hpb=4573f1fecaf83f4706f39702555d5319d132477b;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 7f5327b56..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
@@ -665,6 +695,38 @@ 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 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
+       nlexicon_status [] [] [] (text,prefix_len,ty)
+     in
+     let nmenv, nsubst, nlexicon_status, nbo = 
+       GrafiteDisambiguate.disambiguate_nterm (Some nty)
+       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 = 
+           GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; 
+          istatus = { 
+            NTacStatus.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 +778,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 +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*), tac, punct) ->
+      (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 = 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