]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguatePp.ml
added "commands_of_environment"
[helm.git] / helm / ocaml / cic_disambiguation / disambiguatePp.ml
index d6a33cfaedf76a1daa38daa1e1279a8d9f024d21..d0b6447c5a5a66db35d8df5248f9538925a23020 100644 (file)
@@ -49,27 +49,36 @@ let parse_environment str =
           Num instance,
           DisambiguateChoices.lookup_num_by_dsc desc
      in
-      environment := Environment.add key value !environment;
+      environment := Environment.cons key value !environment;
     done;
     assert false
   with End_of_file ->
    !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)
+    env []
+
+let commands_of_environment env =
+  List.map
+    (fun alias -> GrafiteAst.Alias (dummy_floc, alias))
+    (aliases_of_environment env)
+
 let pp_environment env =
-  let aliases =
-    Environment.fold
-      (fun domain_item (dsc, _) acc ->
-        let s =
-          match domain_item with
-          | Id id ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "."
-          | Symbol (symb, i) ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc))
-              ^ "."
-          | Num i ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "."
-        in
-        s :: acc)
-      env []
+  let aliases = aliases_of_environment env in
+  let strings =
+    List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases
   in
-  String.concat "\n" (List.sort compare aliases)
+  String.concat "\n" (List.sort compare strings)
+