1. Several files in grafite that should be in grafite_parser moved there.

[helm.git] / helm / ocaml / grafite2 / grafiteEngine.ml

diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml
index 70fb767a87f419bedb3eeab075351b66f81de789..00470b9fc2b6bfb0ff39fdd0f32966b75eaf1f64 100644 (file)
--- a/helm/ocaml/grafite2/grafiteEngine.ml
+++ b/helm/ocaml/grafite2/grafiteEngine.ml
@@ -24,13 +24,11 @@
  *)
 
 exception Drop
-exception UnableToInclude of string
 exception IncludedFileNotCompiled of string (* file name *)
 exception MetadataNotFound of string        (* file name *)
 
 type options = { 
   do_heavy_checks: bool ; 
-  include_paths: string list ;
   clean_baseuri: bool
 }
 
@@ -319,6 +317,7 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos
 type eval_ast =
  {ea_go:
   'term 'lazy_term 'reduction 'obj 'ident.
+  baseuri_of_script:(string -> string) ->
   disambiguate_tactic:
    (GrafiteTypes.status ->
     ProofEngineTypes.goal ->
@@ -332,7 +331,6 @@ type eval_ast =
     GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
 
   ?do_heavy_checks:bool ->
-  ?include_paths:string list ->
   ?clean_baseuri:bool ->
   GrafiteTypes.status ->
   ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
@@ -341,6 +339,7 @@ type eval_ast =
 
 type 'a eval_command =
  {ec_go: 'term 'obj.
+  baseuri_of_script:(string -> string) ->
   disambiguate_command:
    (GrafiteTypes.status ->
     ('term,'obj) GrafiteAst.command ->
@@ -351,6 +350,7 @@ type 'a eval_command =
 
 type 'a eval_executable =
  {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
+  baseuri_of_script:(string -> string) ->
   disambiguate_tactic:
    (GrafiteTypes.status ->
     ProofEngineTypes.goal ->
@@ -446,23 +446,9 @@ let eval_tactical ~disambiguate_tactic status tac =
   in
   status
 
-let make_absolute paths path =
-   let rec aux = function
-   | [] -> ignore (Unix.stat path); path
-   | p :: tl ->
-      let path = p ^ "/" ^ path in
-       try
-         ignore (Unix.stat path); path
-       with Unix.Unix_error _ -> aux tl
-   in
-   try
-     aux paths
-   with Unix.Unix_error _ -> raise (UnableToInclude path)
-;;
-       
 let eval_comment status c = status
 
-let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
+let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opts status cmd ->
   let status,cmd = disambiguate_command status cmd in
   let cmd,notation_ids' = CicNotation.process_notation cmd in
   let status =
@@ -475,10 +461,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status
   | GrafiteAst.Include (loc, path) ->
-     let absolute_path = make_absolute opts.include_paths path in
-     let moopath = GrafiteMisc.obj_file_of_script ~basedir absolute_path in
-     let metadatapath =
-       GrafiteMisc.metadata_file_of_script ~basedir absolute_path in
+     let baseuri = baseuri_of_script path in
+     let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+     let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
      let status =
@@ -634,7 +619,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
          MatitaSync.add_obj uri obj
           {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
 
-} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex ->
+} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex ->
   match ex with
   | GrafiteAst.Tactical (_, tac, None) ->
      eval_tactical ~disambiguate_tactic status tac
@@ -642,7 +627,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
      let status = eval_tactical ~disambiguate_tactic status tac in
       eval_tactical ~disambiguate_tactic status punct
   | GrafiteAst.Command (_, cmd) ->
-      eval_command.ec_go ~disambiguate_command opts status cmd
+      eval_command.ec_go ~baseuri_of_script ~disambiguate_command
+       opts status cmd
   | GrafiteAst.Macro (_, mac) -> 
 (*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO
       raise (Command_error
@@ -662,21 +648,23 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
       let ast = ast_of_cmd ast in
       status :=
         eval_ast.ea_go
+         ~baseuri_of_script:(fun _ -> assert false)
          ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
          ~disambiguate_command:(fun status cmd -> status,cmd)
          !status ast)
     moo
-} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
-  ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st 
+} and eval_ast = {ea_go = fun ~baseuri_of_script ~disambiguate_tactic
+ ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status
+ st 
 ->
   let opts = {
     do_heavy_checks = do_heavy_checks ; 
-    include_paths = include_paths;
     clean_baseuri = clean_baseuri }
   in
   match st with
   | GrafiteAst.Executable (_,ex) ->
-     eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command opts status ex
+     eval_executable.ee_go ~baseuri_of_script ~disambiguate_tactic
+      ~disambiguate_command opts status ex
   | GrafiteAst.Comment (_,c) -> eval_comment status c
 }