More notation (up to where the open bugs allow me to put it without adding

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 9707149d568cd52bb87de6846f782bebce038322..fe9ea94d66b3ba1dafab5310c035217dcb5f164a 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -59,8 +59,9 @@ let tactic_of_ast = function
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width) -> 
-      AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
+  | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *)
+      AutoTactic.auto_tac ?depth ?width ?paramodulation
+        ~dbd:(MatitaDb.instance ()) ()
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -178,7 +179,7 @@ let disambiguate_tactic status = function
       let status, cic = disambiguate_term status term in
       status, GrafiteAst.Absurd (loc, cic)
   | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
-  | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width)
+  | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *)
   | GrafiteAst.Change (loc, pattern, with_what) -> 
       let status, with_what = disambiguate_term status with_what in
       let status, pattern = disambiguate_pattern status pattern in
@@ -501,21 +502,19 @@ let disambiguate_command status = function
       let status,obj = disambiguate_obj status obj in
        status, GrafiteAst.Obj (loc,obj)
 
-let try_open_in ~f paths path =
+let make_absolute paths path =
   let rec aux = function
-  | [] -> f path
+  | [] -> ignore (Unix.stat path); path
   | p :: tl ->
+     let path = p ^ "/" ^ path in
       try
-        f (p ^ "/" ^ path)
-      with Sys_error _ -> aux tl
+        ignore (Unix.stat path); path
+      with Unix.Unix_error _ -> aux tl
   in
   try
     aux paths
-  with Sys_error _ as exc ->
-    MatitaLog.error ("Unable to read " ^ path);
-    MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
-    MatitaLog.error ("current working directory is " ^ Unix.getcwd ());
-    raise exc
+  with Unix.Unix_error _ as exc ->
+    command_error ("File " ^ path ^ " not found")
 ;;
        
 let eval_command opts status cmd =
@@ -530,15 +529,15 @@ let eval_command opts status cmd =
      {status with moo_content_rev =
         (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | GrafiteAst.Include (loc, path) ->
-     let path = MatitaMisc.obj_file_of_script path in
-     (try
-       let ic = try_open_in ~f:open_in opts.include_paths path in
-       let stream = Stream.of_channel ic in
-       let status = ref status in
-       !eval_from_stream_ref status stream (fun _ _ -> ());
-       close_in ic;
-       !status
-     with Sys_error _ -> raise (UnableToInclude 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 (UnableToInclude moopath) in
+     let stream = Stream.of_channel ic in
+     let status = ref status in
+      !eval_from_stream_ref status stream (fun _ _ -> ());
+      close_in ic;
+      !status
   | GrafiteAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
@@ -550,7 +549,7 @@ let eval_command opts status cmd =
         else
           value
       in
-      if not (MatitacleanLib.is_empty value) then
+      if not (MatitaMisc.is_empty value) then
         begin
           MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
           if opts.clean_baseuri then