matitamake stuff:

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 53772ccf29a9d604a7b02afb8baa7d468e329472..94efb904f4a9da6685225c612673edb9c4a0f30f 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -7,6 +7,8 @@ exception Drop;;
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
+type options = { do_heavy_checks: bool ; include_paths: string list }
+
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
   * using FreshNamesGenerator module *)
@@ -443,7 +445,23 @@ let disambiguate_command status = function
       let status,obj = disambiguate_obj status obj in
        status, TacticAst.Obj (loc,obj)
 
-let eval_command do_heavy_checks status cmd =
+let try_open_in paths path =
+  let rec aux = function
+  | [] -> open_in path
+  | p :: tl ->
+      try
+        open_in (p ^ "/" ^ path)
+      with Sys_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);
+    raise exc
+;;
+       
+let eval_command opts status cmd =
  let status,cmd = disambiguate_command status cmd in
   match cmd with
   | TacticAst.Default (loc, what, uris) as cmd ->
@@ -452,7 +470,7 @@ let eval_command do_heavy_checks status cmd =
         (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | TacticAst.Include (loc, path) ->
      let path = MatitaMisc.obj_file_of_script path in
-     let stream = Stream.of_channel (open_in path) in
+     let stream = Stream.of_channel (try_open_in opts.include_paths path) in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());
       !status
@@ -525,7 +543,7 @@ let eval_command do_heavy_checks status cmd =
          let name = UriManager.name_of_uri uri in
          if not(CicPp.check name ty) then
            MatitaLog.warn ("Bad name: " ^ name);
-         if do_heavy_checks then
+         if opts.do_heavy_checks then
            begin
              let dbd = MatitaDb.instance () in
              let similar = MetadataQuery.match_term ~dbd ty in
@@ -575,45 +593,50 @@ let eval_command do_heavy_checks status cmd =
            | Cic.CurrentProof _
            | Cic.Variable _ -> assert false
 
-let eval_executable do_heavy_checks status ex =
+let eval_executable opts status ex =
   match ex with
   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
-  | TacticAst.Command (_, cmd) -> eval_command do_heavy_checks status cmd
+  | TacticAst.Command (_, cmd) -> eval_command opts status cmd
   | TacticAst.Macro (_, mac) -> 
       command_error (sprintf "The macro %s can't be in a script" 
         (TacticAstPp.pp_macro_ast mac))
 
 let eval_comment status c = status
             
-let eval_ast ?(do_heavy_checks=false) status st =
+
+let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st =
+  let opts = 
+    {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
+  in
   match st with
-  | TacticAst.Executable (_,ex) -> eval_executable do_heavy_checks status ex
+  | TacticAst.Executable (_,ex) -> eval_executable opts status ex
   | TacticAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_stream ?do_heavy_checks status str cb =
+let eval_from_stream ?do_heavy_checks ?include_paths status str cb =
   let stl = CicTextualParser2.parse_statements str in
   List.iter
    (fun ast -> 
-     cb !status ast;status := eval_ast ?do_heavy_checks !status ast) 
+     cb !status ast;
+     status := eval_ast ?do_heavy_checks ?include_paths !status ast) 
    stl
 ;;
 
 (* to avoid a long list of recursive functions *)
 eval_from_stream_ref := eval_from_stream;;
   
-let eval_from_stream_greedy ?do_heavy_checks status str cb =
+let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb =
   while true do
     print_string "matita> ";
     flush stdout;
     let ast = CicTextualParser2.parse_statement str in
     cb !status ast;
-    status := eval_ast ?do_heavy_checks !status ast 
+    status := eval_ast ?do_heavy_checks ?include_paths !status ast 
   done
 ;;
 
-let eval_string ?do_heavy_checks status str =
+let eval_string ?do_heavy_checks ?include_paths status str =
   eval_from_stream 
-    ?do_heavy_checks status (Stream.of_string str) (fun _ _ -> ())
+    ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
 
 let default_options () =
 (*
@@ -626,7 +649,7 @@ let default_options () =
 *)
   let options =
     StringMap.add "basedir"
-      (String (Helm_registry.get "matita.basedir" ))
+      (String (Helm_registry.get "matita.basedir"))
       no_options
   in
   options