]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguatePp.ml
Yet another implementation of the single aliases / multi aliases idea.
[helm.git] / helm / ocaml / cic_disambiguation / disambiguatePp.ml
index d0b6447c5a5a66db35d8df5248f9538925a23020..b7c1012a8dc68474e2515f567320f82a4c7bbe8d 100644 (file)
@@ -28,6 +28,7 @@ open DisambiguateTypes
 let parse_environment str =
  let stream = Stream.of_string str in
  let environment = ref Environment.empty in
+ let multiple_environment = ref Environment.empty in
   try
     while true do
      let alias =
@@ -49,25 +50,23 @@ let parse_environment str =
           Num instance,
           DisambiguateChoices.lookup_num_by_dsc desc
      in
-      environment := Environment.cons key value !environment;
+      environment := Environment.add key value !environment;
+      multiple_environment := Environment.cons key value !multiple_environment;
     done;
     assert false
   with End_of_file ->
-   !environment
+   !environment, !multiple_environment
 
 let aliases_of_environment env =
   Environment.fold
-    (fun domain_item codomain_items acc ->
-      List.fold_left
-        (fun strings (dsc, _) ->
-          let s =
-            match domain_item with
-            | Id id -> GrafiteAst.Ident_alias (id, dsc)
-            | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc)
-            | Num i -> GrafiteAst.Number_alias (i, dsc)
-          in
-          s :: strings)
-        acc codomain_items)
+    (fun domain_item (dsc,_) acc ->
+      let s =
+        match domain_item with
+        | Id id -> GrafiteAst.Ident_alias (id, dsc)
+        | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc)
+        | Num i -> GrafiteAst.Number_alias (i, dsc)
+      in
+       s :: acc)
     env []
 
 let commands_of_environment env =