X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=055059dd71c2ad3807a343569ce4444703ad5391;hb=0d2bfb98d8343b4e6cefdb506a813b7cb5749630;hp=e87795900c77bef72aee0ac6ffda9371695f8ac0;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index e87795900..055059dd7 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -28,9 +28,6 @@
 exception Drop
 (* mo file name, ma file name *)
 exception IncludedFileNotCompiled of string * string 
-exception Macro of
- GrafiteAst.loc *
-  (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a
@@ -45,73 +42,6 @@ let concat_nuris uris nuris =
    | _ -> assert false
 ;;
 
-type eval_ast =
- {ea_go:
-  'term 'lazy_term 'reduction 'obj 'ident.
-
-  disambiguate_command:
-   (GrafiteTypes.status ->
-    (('term,'obj) GrafiteAst.command) disambiguator_input ->
-    GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
-  disambiguate_macro:
-   (GrafiteTypes.status ->
-    (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
-    Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
-
-  ?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 -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
-    GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> 
-  options -> GrafiteTypes.status -> 
-    (('term,'obj) 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 -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
-    GrafiteTypes.status * (Cic.term,Cic.obj) 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 ->
-    (('term,'obj) GrafiteAst.command) disambiguator_input ->
-    GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
-  disambiguate_macro:
-   (GrafiteTypes.status ->
-    (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
-    Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
-
-  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 coercion_moo_statement_of (uri,arity, saturations,_) =
-  GrafiteAst.Coercion
-   (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
-
 let basic_eval_unification_hint (t,n) status =
  NCicUnifHint.add_user_provided_hint status t n
 ;;
@@ -289,32 +219,6 @@ let eval_add_constraint status u1 u2 =
   status,`New []
 ;;
 
-let add_coercions_of_lemmas lemmas status =
-  let moo_content = 
-    HExtlib.filter_map 
-      (fun uri ->
-        match CoercDb.is_a_coercion (Cic.Const (uri,[])) with
-        | None -> None
-        | Some (_,tgt,_,sat,_) ->
-            let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
-            Some (coercion_moo_statement_of (uri,arity,sat,0)))
-      lemmas
-  in
-  let status = GrafiteTypes.add_moo_content moo_content status in 
-   status#set_coercions (CoercDb.dump ()), 
-  lemmas
-
-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
@@ -663,50 +567,41 @@ 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.Default (loc, what, uris) as cmd ->
-     LibraryObjects.set_default what uris;
-     GrafiteTypes.add_moo_content [cmd] status,`New []
-  | 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 []
   | GrafiteAst.Set (loc, name, value) -> status, `New []
-(*       GrafiteTypes.set_option status name value,[] *)
-  | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
  in
   status,uris
 
-} and eval_executable = {ee_go = fun ~disambiguate_command
-~disambiguate_macro 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
@@ -721,15 +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.Macro (loc, macro) ->
-     raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
   | 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,
@@ -740,29 +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)
-         ~disambiguate_macro:(fun _ _ -> assert false)
+       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
-~disambiguate_macro ?(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
-      ~disambiguate_macro 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