X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=4e48df8072d13a027ea5dac975936fa884d91d1f;hb=aeb7f0539398561dc84cadf38df14a051dd1ba75;hp=9a194b5ba19e00e3a382b02b0b77fc815eeb2e7d;hpb=2eeeed0dca0fd4fde2c0ec2b98db40d327e7e158;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 9a194b5ba..4e48df807 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -65,8 +65,8 @@ let tactic_of_ast ast =
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width,paramodulation) ->
-      AutoTactic.auto_tac ?depth ?width ?paramodulation
+  | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
+      AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
         ~dbd:(MatitaDb.instance ()) ()
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
@@ -227,8 +227,8 @@ let disambiguate_tactic status tactic =
         let cic = disambiguate_term status_ref term in
         GrafiteAst.Apply (loc, cic)
     | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
-    | GrafiteAst.Auto (loc,depth,width,paramodulation) ->
-        GrafiteAst.Auto (loc,depth,width,paramodulation)
+    | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
+        GrafiteAst.Auto (loc,depth,width,paramodulation,full)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term status_ref with_what in
         let pattern = disambiguate_pattern status_ref pattern in
@@ -634,7 +634,7 @@ let generate_projections uri fields status =
   ) status projections
 
 (* to avoid a long list of recursive functions *)
-let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
+let eval_from_moo_ref = ref (fun _ _ _ -> assert false);;
  
 let disambiguate_obj status obj =
   let uri =
@@ -696,8 +696,6 @@ let make_absolute paths path =
    with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
-let profiler_include = HExtlib.profile "include"
-
 let eval_command opts status cmd =
   let status,cmd = disambiguate_command status cmd in
   let cmd,notation_ids' = CicNotation.process_notation cmd in
@@ -711,15 +709,11 @@ let eval_command opts status cmd =
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
-     let ic =
-      try open_in moopath with Sys_error _ -> 
-        raise (IncludedFileNotCompiled moopath) in
-     let stream = Ulexing.from_utf8_channel ic in
      let status = ref status in
-      profiler_include.HExtlib.profile
-       (!eval_from_stream_ref status stream) (fun _ _ -> ());
-      close_in ic;
-      !status
+     if not (Sys.file_exists moopath) then
+       raise (IncludedFileNotCompiled moopath);
+     !eval_from_moo_ref status moopath (fun _ _ -> ());
+     !status
   | GrafiteAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
@@ -759,8 +753,7 @@ let eval_command opts status cmd =
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       MatitaSync.add_obj uri obj status
-  | GrafiteAst.Coercion (loc, coercion) -> 
-      eval_coercion status coercion
+  | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion
   | GrafiteAst.Alias (loc, spec) -> 
      let diff =
       (*CSC: Warning: this code should be factorized with the corresponding
@@ -891,6 +884,22 @@ let eval_ast
   | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
   | GrafiteAst.Comment (_,c) -> eval_comment status c
 
+let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname
+  cb
+=
+  let moo = MatitaMoo.load_moo fname in
+  List.iter 
+    (fun ast -> 
+      let ast =
+        GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
+          GrafiteAst.Command (DisambiguateTypes.dummy_floc,
+            (GrafiteAst.reash_cmd_uris ast)))
+      in
+      cb !status ast;
+      status :=
+        eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
+    moo
+
 let eval_from_stream 
   ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
 =
@@ -898,12 +907,13 @@ let eval_from_stream
     while true do
       let ast = GrafiteParser.parse_statement str in
       cb !status ast;
-      status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
+      status :=
+        eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
     done
   with End_of_file -> ()
 
 (* to avoid a long list of recursive functions *)
-let _ = eval_from_stream_ref := eval_from_stream
+let _ = eval_from_moo_ref := eval_from_moo
   
 let eval_from_stream_greedy 
   ?do_heavy_checks ?include_paths ?clean_baseuri status str cb