From: Stefano Zacchiroli 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 +