(* Copyright (C) 2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) exception NoWellTypedInterpretation module Environment = struct type t = Disambiguate_types.environment let empty = Disambiguate_types.Environment.empty let to_string env = prerr_endline "TODO: implement and move away" ; Disambiguate_types.Environment.fold (fun i v s -> match i with | Disambiguate_types.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 = Disambiguate_types.Id (Str.matched_group 2 inputtext) in let uri = "cic:" ^ (Str.matched_group 5 inputtext) in let resolve_id = aux (n' + 1) in if Disambiguate_types.Environment.mem id resolve_id then resolve_id else let term = Disambiguate.term_of_uri uri in (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term)) resolve_id) with Not_found -> Disambiguate_types.Environment.empty in aux 0 end ;; module Make (C : Disambiguate_types.Callbacks) = struct let disambiguate_term mqi_handle context metasenv term_as_string environment = let module Disambiguate' = Disambiguate.Make (C) in let term = Parser.parse_term (Stream.of_string term_as_string) in Disambiguate'.disambiguate_term mqi_handle context metasenv term environment end ;;