+
+module EnvironmentP3 =
+ struct
+ type t = domain_and_interpretation
+
+ let empty = ""
+
+ let to_string (dom,resolve_id) =
+ let string_of_cic_textual_parser_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+ let uri' =
+ match uri with
+ CTP.ConUri uri -> UriManager.string_of_uri uri
+ | CTP.VarUri uri -> UriManager.string_of_uri uri
+ | CTP.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
+ | CTP.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
+ string_of_int consno
+ in
+ (* 4 = String.length "cic:" *)
+ String.sub uri' 4 (String.length uri' - 4)
+ in
+ String.concat "\n"
+ (List.map
+ (function v ->
+ let uri =
+ match resolve_id v with
+ None -> assert false
+ | Some (CicTextualParser0.Uri uri) -> uri
+ | Some (CicTextualParser0.Term _)
+ | Some CicTextualParser0.Implicit -> assert false
+ in
+ "alias " ^
+ (match v with
+ CicTextualParser0.Id id -> id
+ | CicTextualParser0.Symbol (descr,_) ->
+ (* CSC: To be implemented *)
+ assert false
+ )^ " " ^ (string_of_cic_textual_parser_uri uri)
+ ) dom)
+
+ 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 = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
+ let uri =
+ MQueryMisc.cic_textual_parser_uri_of_string
+ ("cic:" ^ (Str.matched_group 5 inputtext))
+ in
+ let dom,resolve_id = aux (n' + 1) in
+ if List.mem id dom then
+ dom,resolve_id
+ else
+ id::dom,
+ (function id' ->
+ if id = id' then
+ Some (CicTextualParser0.Uri uri)
+ else resolve_id id')
+ with
+ Not_found -> ([],function _ -> None)
+ in
+ aux 0
+ end