X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=055059dd71c2ad3807a343569ce4444703ad5391;hb=308d9394c3f8c0919427fcc7e00842e105840b4e;hp=b4a20c20259347bca72f16a95505fe989967664a;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b4a20c202..055059dd7 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -42,59 +42,6 @@ let concat_nuris uris nuris =
    | _ -> assert false
 ;;
 
-type eval_ast =
- {ea_go:
-  'term 'lazy_term 'reduction 'obj 'ident.
-
-  disambiguate_command:
-   (GrafiteTypes.status ->
-    (GrafiteAst.command) disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) ->
-
-  ?do_heavy_checks:bool ->
-  GrafiteTypes.status ->
-  (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
-  disambiguator_input ->
-  GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_command =
- {ec_go: 'term 'obj.
-  disambiguate_command:
-   (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) -> 
-  options -> GrafiteTypes.status -> 
-    GrafiteAst.command disambiguator_input ->
-   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_comment =
- {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
-  disambiguate_command:
-   (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) -> 
-  options -> GrafiteTypes.status -> 
-    (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
-   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_executable =
- {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
-
-  disambiguate_command:
-   (GrafiteTypes.status ->
-    GrafiteAst.command disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) ->
-
-  options ->
-  GrafiteTypes.status ->
-  (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input ->
-  GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_from_moo =
- { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-      
 let basic_eval_unification_hint (t,n) status =
  NCicUnifHint.add_user_provided_hint status t n
 ;;
@@ -272,17 +219,6 @@ let eval_add_constraint status u1 u2 =
   status,`New []
 ;;
 
-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 ~force:false
-  | 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 tac =
  let rec aux f (text, prefix_len, tac) =
   match tac with
@@ -631,36 +567,33 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
       eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
-let rec eval_command = {ec_go = fun ~disambiguate_command opts status
-(text,prefix_len,cmd) ->
+let eval_comment ~disambiguate_command opts status (text,prefix_len,c) =
+ status, `New []
+
+let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
  let status,uris =
   match cmd with
-  | GrafiteAst.Drop loc -> raise Drop
-  | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
-     (* Old Include command is not recursive; new one is *)
+  | GrafiteAst.Include (loc, baseuri) ->
      let status =
-      if new_or_old = `OldAndNew then
-       let moopath_rw, moopath_r = 
-        LibraryMisc.obj_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true,
-        LibraryMisc.obj_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:false in
-       let moopath = 
-        if Sys.file_exists moopath_r then moopath_r else
-          if Sys.file_exists moopath_rw then moopath_rw else
-            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
-       in
-        eval_from_moo.efm_go status moopath
-      else
-       status
+      let moopath_rw, moopath_r = 
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true,
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:false in
+      let moopath = 
+       if Sys.file_exists moopath_r then moopath_r else
+         if Sys.file_exists moopath_rw then moopath_rw else
+           raise (IncludedFileNotCompiled (moopath_rw,baseuri))
+      in
+       eval_from_moo status moopath
      in
       let status =
        NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
         status in
       let status =
        GrafiteTypes.add_moo_content
-        [GrafiteAst.Include (loc,mode,`New,baseuri)] status
+        [GrafiteAst.Include (loc,baseuri)] status
       in
        status,`New []
   | GrafiteAst.Print (_,_) -> status,`New []
@@ -668,8 +601,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
  in
   status,uris
 
-} and eval_executable = {ee_go = fun ~disambiguate_command
- opts status (text,prefix_len,ex) ->
+and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
   match ex with
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
       if status#ng_mode <> `ProofMode then
@@ -684,13 +616,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        in
         status,`New []
   | GrafiteAst.Command (_, cmd) ->
-      eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
+      eval_command ~disambiguate_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_from_moo = {efm_go = fun status fname ->
+and eval_from_moo status fname =
   let ast_of_cmd cmd =
     ("",0,GrafiteAst.Executable (HExtlib.dummy_floc,
       GrafiteAst.Command (HExtlib.dummy_floc,
@@ -701,28 +633,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
     (fun status ast -> 
       let ast = ast_of_cmd ast in
       let status,lemmas =
-       eval_ast.ea_go
-         ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
+       eval_ast ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
          status ast
       in
        assert (lemmas=`New []);
        status)
     status moo
-} and eval_ast = {ea_go = fun ~disambiguate_command
-?(do_heavy_checks=false) status
+
+and eval_ast ~disambiguate_command ?(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.ee_go ~disambiguate_command
-      opts status (text,prefix_len,ex)
+     eval_executable ~disambiguate_command opts status (text,prefix_len,ex)
   | GrafiteAst.Comment (_,c) -> 
-      eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) 
-} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> 
-    status, `New []
-}
+      eval_comment ~disambiguate_command opts status (text,prefix_len,c) 
 ;;
-
-
-let eval_ast = eval_ast.ea_go