]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite2/disambiguatePp.ml
1. Several files in grafite that should be in grafite_parser moved there.
[helm.git] / helm / ocaml / grafite2 / disambiguatePp.ml
index c3a48e409e885a767b4b6441d942ebff86baeab5..733179589a574e88a89fd283e7eeb57a63d7f1e3 100644 (file)
 
 open DisambiguateTypes
 
-let parse_environment str =
- let stream = Ulexing.from_utf8_string str in
- let environment = ref Environment.empty in
- let multiple_environment = ref Environment.empty in
-  try
-    while true do
-     let alias =
-      match GrafiteParser.parse_statement stream with
-         GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias)))
-           -> alias
-       | _ -> assert false in
-     let key,value =
-      (*CSC: Warning: this code should be factorized with the corresponding
-             code in MatitaEngine *)
-      match alias with
-         GrafiteAst.Ident_alias (id,uri) ->
-          Id id,
-          (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
-       | GrafiteAst.Symbol_alias (symb,instance,desc) ->
-          Symbol (symb,instance),
-          DisambiguateChoices.lookup_symbol_by_dsc symb desc
-       | GrafiteAst.Number_alias (instance,desc) ->
-          Num instance,
-          DisambiguateChoices.lookup_num_by_dsc desc
-     in
-      environment := Environment.add key value !environment;
-      multiple_environment := Environment.cons key value !multiple_environment;
-    done;
-    assert false
-  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)