X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=b065040523bc2d46d3fa2b4f3db89d91a9611ca9;hb=57b996a466e62a8696c46d1d58883c4fade7c59e;hp=4bb40797527a38bb03cbec392cb0e82df5675aae;hpb=78044035b4419e569df0d7f6a7f96fa32d21a19d;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 4bb407975..b06504052 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -162,7 +162,7 @@ let singleton = function
 
 let disambiguate_term status_ref term =
   let status = !status_ref in
-  let (aliases, metasenv, cic, _) =
+  let (diff, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
         ~aliases:status.aliases ~universe:(Some status.multi_aliases)
@@ -170,7 +170,7 @@ let disambiguate_term status_ref term =
         ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
   in
   let status = MatitaTypes.set_metasenv metasenv status in
-  let status = MatitaSync.set_proof_aliases status aliases in
+  let status = MatitaSync.set_proof_aliases status diff in
   status_ref := status;
   cic
   
@@ -182,14 +182,14 @@ let disambiguate_term status_ref term =
 let disambiguate_lazy_term status_ref term =
   (fun context metasenv ugraph ->
     let status = !status_ref in
-    let (aliases, metasenv, cic, ugraph) =
+    let (diff, metasenv, cic, ugraph) =
       singleton
         (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
           ~initial_ugraph:ugraph ~aliases:status.aliases
           ~universe:(Some status.multi_aliases) ~context ~metasenv term)
     in
     let status = MatitaTypes.set_metasenv metasenv status in
-    let status = MatitaSync.set_proof_aliases status aliases in
+    let status = MatitaSync.set_proof_aliases status diff in
     status_ref := status;
     cic, metasenv, ugraph)
 
@@ -580,7 +580,7 @@ let eval_coercion status coercion =
     (* also adds them to the Db *)
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
   let status =
-   List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
+   List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
     status new_coercions in
   let statement_of name =
     GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 
@@ -597,14 +597,19 @@ let eval_coercion status coercion =
   { status with proof_status = No_proof }
 
 let generate_elimination_principles uri status =
- let elim sort status =
-   try
-    let uri,obj = CicElim.elim_of ~sort uri 0 in
-     MatitaSync.add_obj uri obj status
-   with CicElim.Can_t_eliminate -> status
- in
- List.fold_left (fun status sort -> elim sort status) status
-  [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
+  let status' = ref status in
+  let elim sort =
+    try
+      let uri,obj = CicElim.elim_of ~sort uri 0 in
+      status' := MatitaSync.add_obj uri obj !status'
+    with CicElim.Can_t_eliminate -> ()
+  in
+  try
+    List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+    !status'
+  with exn ->
+    MatitaSync.time_travel ~present:!status' ~past:status;
+    raise exn
 
 let generate_projections uri fields status =
  let projections = CicRecord.projections_of uri fields in
@@ -629,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 =
@@ -639,7 +644,7 @@ let disambiguate_obj status obj =
        Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
     | GrafiteAst.Inductive _ -> assert false
     | GrafiteAst.Theorem _ -> None in
-  let (aliases, metasenv, cic, _) =
+  let (diff, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
         ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
@@ -652,7 +657,7 @@ let disambiguate_obj status obj =
     | Intermediate _ -> assert false
   in
   let status = { status with proof_status = proof_status } in
-  let status = MatitaSync.set_proof_aliases status aliases in
+  let status = MatitaSync.set_proof_aliases status diff in
   status, cic
   
 let disambiguate_command status = function
@@ -704,14 +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 = Stream.of_channel ic in
      let status = ref status in
-      !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
@@ -751,40 +753,32 @@ 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 aliases =
+     let diff =
       (*CSC: Warning: this code should be factorized with the corresponding
              code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
-         DisambiguateTypes.Environment.add
-          (DisambiguateTypes.Id id) 
-          (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
-          status.aliases 
+         [DisambiguateTypes.Id id,
+          (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))]
       | GrafiteAst.Symbol_alias (symb, instance, desc) ->
-         DisambiguateTypes.Environment.add
-          (DisambiguateTypes.Symbol (symb,instance))
-          (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
-          status.aliases
+         [DisambiguateTypes.Symbol (symb,instance),
+          DisambiguateChoices.lookup_symbol_by_dsc symb desc]
       | GrafiteAst.Number_alias (instance,desc) ->
-         DisambiguateTypes.Environment.add
-          (DisambiguateTypes.Num instance)
-          (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
+         [DisambiguateTypes.Num instance,
+          DisambiguateChoices.lookup_num_by_dsc desc]
      in
-      MatitaSync.set_proof_aliases status aliases
+      MatitaSync.set_proof_aliases status diff
   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
   | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
       let status' = add_moo_content [stm] status in
-      let aliases' =
-        DisambiguateTypes.Environment.add
-          (DisambiguateTypes.Symbol (symbol, 0))
-          (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
-          status.aliases
+      let diff =
+       [DisambiguateTypes.Symbol (symbol, 0),
+         DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
       in
-      MatitaSync.set_proof_aliases status' aliases'
+      MatitaSync.set_proof_aliases status' diff
   | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
@@ -843,22 +837,29 @@ let eval_command opts status cmd =
           command_error (
             "metasenv not empty while giving a definition with body: " ^
             CicMetaSubst.ppmetasenv [] metasenv);
-         let status = MatitaSync.add_obj uri obj status in
-          match obj with
-             Cic.Constant _ -> status
+         let status' = ref status in
+         (try
+           status' := MatitaSync.add_obj uri obj !status';
+           (match obj with
+           | Cic.Constant _ -> ()
            | Cic.InductiveDefinition (_,_,_,attrs) ->
-              let status = generate_elimination_principles uri status in
-              let rec get_record_attrs =
-               function
-                  [] -> None
-                | (`Class (`Record fields))::_ -> Some fields
-                | _::tl -> get_record_attrs tl
-              in
+               status' := generate_elimination_principles uri !status';
+               let rec get_record_attrs =
+                 function
+                 | [] -> None
+                 | (`Class (`Record fields))::_ -> Some fields
+                 | _::tl -> get_record_attrs tl
+               in
                (match get_record_attrs attrs with
-                   None -> status (* not a record *)
-                 | Some fields -> generate_projections uri fields status)
+               | None -> () (* not a record *)
+               | Some fields ->
+                   status' := generate_projections uri fields !status')
            | Cic.CurrentProof _
-           | Cic.Variable _ -> assert false
+           | Cic.Variable _ -> assert false);
+           !status'
+         with exn ->
+           MatitaSync.time_travel ~present:!status' ~past:status;
+           raise exn)
 
 let eval_executable opts status ex =
   match ex with
@@ -883,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 
 =
@@ -890,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 
@@ -911,7 +929,8 @@ let eval_from_stream_greedy
 
 let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
   eval_from_stream 
-    ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->())
+    ?do_heavy_checks ?include_paths ?clean_baseuri status
+      (Ulexing.from_utf8_string str) (fun _ _ ->())
 
 let default_options () =
 (*