From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 13 Sep 2005 13:23:05 +0000 (+0000)
Subject: added "commands_of_environment"
X-Git-Tag: V_0_1_2_1~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a9513f3af74622f9bebc8c68b0b53e2e01c4200;p=helm.git

added "commands_of_environment"
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index 24f9ea37e..d0b6447c5 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -55,24 +55,30 @@ let parse_environment str =
   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 codomain_items acc ->
-        List.fold_left
-          (fun strings (dsc, _) ->
-            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 :: strings)
-          acc codomain_items)
-      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)
+
diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.mli b/helm/ocaml/cic_disambiguation/disambiguatePp.mli
index 68cecfaa8..9d2051134 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.mli
@@ -24,4 +24,10 @@
  *)
 
 val parse_environment: string -> DisambiguateTypes.environment
+
+val commands_of_environment:
+  DisambiguateTypes.environment ->
+    (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list
+
 val pp_environment: DisambiguateTypes.environment -> string
+