big change in parsing, trying to make all functional

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

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 3a9e87eea0a785e3d9c50f33f558cea2625d2842..00160ac81b0ad885d47fe7477ce5f94f3a3f93c5 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -46,10 +46,8 @@ let inject_unification_hint =
  =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
-  NCicLibrary.Serializer.register#run "unification_hints"
-   object(_ : 'a NCicLibrary.register_type)
-     method run = basic_eval_unification_hint
-   end
+  GrafiteTypes.Serializer.register#run "unification_hints"
+   basic_eval_unification_hint
 ;;
 
 let eval_unification_hint status t n = 
@@ -83,10 +81,7 @@ let record_index_obj =
         (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) 
       l)
  in
-  NCicLibrary.Serializer.register#run "index_obj"
-   object(_ : 'a NCicLibrary.register_type)
-     method run = aux
-   end
+  GrafiteTypes.Serializer.register#run "index_obj" aux
 ;;
 
 let compute_keys status uri height kind = 
@@ -167,10 +162,7 @@ let record_index_eq =
    ~refresh_uri_in_term 
    = index_eq (NCicLibrary.refresh_uri uri) 
  in
-  NCicLibrary.Serializer.register#run "index_eq"
-   object(_ : 'a NCicLibrary.register_type)
-     method run = basic_index_eq
-   end
+  GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
 ;;
 
 let index_eq_for_auto status uri =
@@ -199,10 +191,7 @@ let inject_constraint =
   let u2 = refresh_uri_in_universe u2 in 
   basic_eval_add_constraint (u1,u2)
  in
-  NCicLibrary.Serializer.register#run "constraints"
-   object(_:'a NCicLibrary.register_type)
-     method run = basic_eval_add_constraint 
-   end
+  GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
 ;;
 
 let eval_add_constraint status u1 u2 = 
@@ -560,22 +549,34 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
       eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
-let eval_comment ~disambiguate_command opts status (text,prefix_len,c) =
- status, []
+let eval_comment opts status (text,prefix_len,c) = status, []
 
-let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
- let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
+let rec eval_command opts status (text,prefix_len,cmd) =
  let status,uris =
   match cmd with
-  | GrafiteAst.Include (loc, baseuri) ->
-       NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        status, []
+  | GrafiteAst.Include (loc, fname, mode, _) ->
+                  let include_paths = assert false in
+                  let never_include = assert false in
+                  let mode = assert false in
+                  let baseuri = assert false in
+      let status =
+       let _root, buri, fullpath, _rrelpath = 
+          Librarian.baseuri_of_script ~include_paths fname in
+        if never_include then raise (GrafiteParser.NoInclusionPerformed fullpath) 
+        else
+           LexiconEngine.eval_command status (LexiconAst.Include (loc,buri,mode,fullpath)) 
+      in
+     let status,obj =
+       GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
+        status in
+     let status = status#set_dump (obj::status#dump) in
+       status,[]
   | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Set (loc, name, value) -> status, []
  in
   status,uris
 
-and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
+and eval_executable opts status (text,prefix_len,ex) =
   match ex with
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
       if status#ng_mode <> `ProofMode then
@@ -590,19 +591,17 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
        in
         status,[]
   | GrafiteAst.Command (_, cmd) ->
-      eval_command ~disambiguate_command opts status (text,prefix_len,cmd)
+      eval_command opts status (text,prefix_len,cmd)
   | GrafiteAst.NCommand (_, cmd) ->
       eval_ncommand opts status (text,prefix_len,cmd)
   | GrafiteAst.NMacro (loc, macro) ->
      raise (NMacro (loc,macro))
 
-and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status
-(text,prefix_len,st)
-=
+and eval_ast ?(do_heavy_checks=false) status (text,prefix_len,st) =
   let opts = { do_heavy_checks = do_heavy_checks ; } in
   match st with
   | GrafiteAst.Executable (_,ex) ->
-     eval_executable ~disambiguate_command opts status (text,prefix_len,ex)
+     eval_executable opts status (text,prefix_len,ex)
   | GrafiteAst.Comment (_,c) -> 
-      eval_comment ~disambiguate_command opts status (text,prefix_len,c) 
+      eval_comment opts status (text,prefix_len,c) 
 ;;