X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguatePp.ml;h=c3a48e409e885a767b4b6441d942ebff86baeab5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4bf917bb8a9a4e5a2f757884d7484dd2690936c3;hpb=33b362600b2756274258f06f26a08c918ec28062;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml index 4bf917bb8..c3a48e409 100644 --- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml @@ -57,22 +57,23 @@ 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 commands_of_environment env = - List.map - (fun alias -> GrafiteAst.Alias (dummy_floc, alias)) - (aliases_of_environment 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 pp_environment env = let aliases = aliases_of_environment env in @@ -80,4 +81,3 @@ let pp_environment env = List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases in String.concat "\n" (List.sort compare strings) -