- Grammar for all obj commands ported to NG (let recs and inductives still need

[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 26e3aab2d05d4066def1e1e64fcbe267746226d1..ebba1988dab1a22ab3f9069d9321b807dcd0d526 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -753,7 +753,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
              else
               let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-prerr_endline (NUri.string_of_uri uri);
                uri,height,[],[],NTacStatus.apply_subst_obj subst obj
               in
                NCicLibrary.add_obj uri obj;
@@ -767,38 +766,32 @@ prerr_endline (NUri.string_of_uri uri);
   | 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
-     (* CSC: ".con"??? it is like that for now *)
-     let suri = "cic:/ng_matita/" ^ name ^ ".con" in
-     let nlexicon_status =
+     let lexicon_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} }   
-     },
-      []
+       | GrafiteTypes.CommandMode ls -> ls in
+     let lexicon_status,obj =
+      GrafiteDisambiguate.disambiguate_nobj lexicon_status
+       ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
+     let uri,height,nmenv,nsubst,nobj = obj 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 },[]
+      | _ ->
+        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}}
+             },[])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with