From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 23 Sep 2005 09:29:23 +0000 (+0000)
Subject: Environment replaced by lists of domain and codomain items.
X-Git-Tag: LAST_BEFORE_NEW~50
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=adfeba63282f11f92705b61cb961a61e107fb5bb;p=helm.git

Environment replaced by lists of domain and codomain items.
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index 4bf917bb8..1f25e1f95 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -57,22 +57,28 @@ let parse_environment str =
   with End_of_file ->
    !environment, !multiple_environment
 
+let alias_of_domain_and_codomain_items domain_item (dsc,_) =
+ 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)
+
 let aliases_of_environment env =
   Environment.fold
-    (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 []
+    (fun domain_item codomain_item acc ->
+      alias_of_domain_and_codomain_items domain_item codomain_item::acc
+    ) env []
+
+let aliases_of_domain_and_codomain_items_list l =
+  List.fold_left
+    (fun acc (domain_item,codomain_item) ->
+      alias_of_domain_and_codomain_items domain_item codomain_item::acc
+    ) [] l
 
-let commands_of_environment env =
+let commands_of_domain_and_codomain_items_list l =
   List.map
     (fun alias -> GrafiteAst.Alias (dummy_floc, alias))
-    (aliases_of_environment env)
+    (aliases_of_domain_and_codomain_items_list l)
 
 let pp_environment env =
   let aliases = aliases_of_environment env in
@@ -80,4 +86,3 @@ let pp_environment env =
     List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases
   in
   String.concat "\n" (List.sort compare strings)
-
diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.mli b/helm/ocaml/cic_disambiguation/disambiguatePp.mli
index e5a656d22..9c3b50661 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.mli
@@ -27,8 +27,8 @@ val parse_environment:
   string ->
    DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
 
-val commands_of_environment:
-  DisambiguateTypes.environment ->
-    (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list
+val commands_of_domain_and_codomain_items_list:
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
+  (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list
 
 val pp_environment: DisambiguateTypes.environment -> string