The disambiguation now returns the aliases diff. It used to return the

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3658b0c20ab93d2990a9a73717faaf35c87bf463..365f947c001a5c163efa811d046797c36d12197a 100644 (file)
--- 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)
 
@@ -639,7 +639,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 +652,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
@@ -709,7 +709,7 @@ let eval_command opts status cmd =
      let ic =
       try open_in moopath with Sys_error _ -> 
         raise (IncludedFileNotCompiled moopath) in
-     let stream = Stream.of_channel ic in
+     let stream = Ulexing.from_utf8_channel ic in
      let status = ref status in
       profiler_include.CicUtil.profile
        (!eval_from_stream_ref status stream) (fun _ _ -> ());
@@ -757,37 +757,30 @@ let eval_command opts status cmd =
   | 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 =
@@ -914,7 +907,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 () =
 (*