- non_punctuational_tacticals ported to NG

[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 97af8a06f7e0ab0d54b8652e11231fc259d0689d..89f50c8fd39324eecfdec735cbbc67f6c5abef66 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -583,6 +583,13 @@ 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) 
@@ -758,12 +765,24 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
              else
               let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-               uri,height,[],[],NTacStatus.apply_subst_obj subst obj
+               (uri,height,[],[],
+                NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst)
+                 obj) in
+              NCicTypeChecker.typecheck_obj obj;
+              NCicLibrary.add_obj uri obj;
+              let objs = NCicElim.mk_elims obj in
+              let uris =
+               uri::
+                List.map
+                 (fun (uri,_,_,_,_) as obj ->
+                   NCicTypeChecker.typecheck_obj obj;
+                   NCicLibrary.add_obj uri obj;
+                   uri
+                 ) objs
               in
-               NCicLibrary.add_obj uri obj;
                {status with 
                  GrafiteTypes.ng_status = 
-                  GrafiteTypes.CommandMode lexicon_status },`New [uri]
+                  GrafiteTypes.CommandMode lexicon_status },`New uris
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;
@@ -779,25 +798,20 @@ prerr_endline "CSC: here we should fix the height!!!";
       GrafiteDisambiguate.disambiguate_nobj lexicon_status
        ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
      let uri,height,nmenv,nsubst,nobj = obj in
+     let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
+     let status =
+      { status with
+         GrafiteTypes.ng_status = 
+          GrafiteTypes.ProofMode
+           { NTacStatus.gstatus = ninitial_stack; 
+             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
+           }
+     in
      (match nmenv with
-        [] ->
-          (* CSC: cut&paste code from NQed *)
-          let obj =
-prerr_endline "CSC: here we should fix the height!!!";
-           uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj
-          in
-           NCicLibrary.add_obj uri obj;
-           {status with 
-             GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
-           `New [uri]
-      | _ ->
-        let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
-        { status with
-           GrafiteTypes.ng_status = 
-            GrafiteTypes.ProofMode
-             { NTacStatus.gstatus = ninitial_stack; 
-               istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-             },`New [])
+         [] ->
+          eval_command.ec_go ~disambiguate_command opts status
+           ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+       | _ -> status,`New [])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -903,6 +917,15 @@ prerr_endline "CSC: here we should fix the height!!!";
      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) ->