From: Stefano Zacchiroli Date: Fri, 23 Jan 2004 16:38:17 +0000 (+0000) Subject: implemented interface for gTopLevel X-Git-Tag: V_0_2_3~160 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=308d03101d84a4d62465bb3ff7c0cd9ca866c659;p=helm.git implemented interface for gTopLevel --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 5f797ab5d..94690373a 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -25,9 +25,6 @@ open Disambiguate_types - (* TODO move to CicSomething *) -val term_of_uri: string -> Cic.term - (** {2 Choice registration interface} *) (** to be raised when a choice is invalid due to some given parameter (e.g. diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.ml b/helm/ocaml/cic_disambiguation/disambiguate_types.ml index 545099da1..522a08dc0 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate_types.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate_types.ml @@ -45,3 +45,47 @@ let string_of_domain dom = dom; Buffer.contents buf +module EnvironmentP3 = + struct + type t = environment + let empty = "" + + let to_string env = + Environment.fold + (fun i v s -> + match i with + | Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v) + | _ -> "") + env "" + + let of_string inputtext = + let regexpr = + let alfa = "[a-zA-Z_-]" in + let digit = "[0-9]" in + let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in + let blanks = "\( \|\t\|\n\)+" in + let nonblanks = "[^ \t\n]+" in + let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) + Str.regexp + ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") + in + let rec aux n = + try + let n' = Str.search_forward regexpr inputtext n in + let id = Id (Str.matched_group 2 inputtext) in + let uri = "cic:" ^ (Str.matched_group 5 inputtext) in + let resolve_id = aux (n' + 1) in + if Environment.mem id resolve_id then + resolve_id + else + let term = + HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) + in + (Environment.add id (uri, (fun _ _ _ -> term)) + resolve_id) + with + Not_found -> Environment.empty + in + aux 0 + end + diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.mli b/helm/ocaml/cic_disambiguation/disambiguate_types.mli index 525a7e33f..a8dda6c39 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate_types.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate_types.mli @@ -54,3 +54,13 @@ module type Callbacks = val string_of_domain_item: domain_item -> string val string_of_domain: Domain.t -> string +(**/**) + +module EnvironmentP3: + sig + type t = environment + val empty : string + val to_string : t -> string + val of_string : string -> t + end +