(* 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/ *) (* $Id$ *) (* type domain_item = | Id of (string * string option) (* literal, opt. uri *) | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *) | Num of (string option * string) option (* opt. uri, interpretation *) *) type domain_item = | Id of string (* literal *) | Symbol of string (* literal *) | Num exception Invalid_choice of (Stdpp.location * string) Lazy.t module OrderedDomain = struct type t = domain_item (* let compare a b = match a,b with | Id (x,None), Id (y,_) | Id (x,_), Id (y,None) when x = y -> 0 | Symbol (x,None), Symbol (y,_) | Symbol (x,_), Symbol (y,None) when x = y -> 0 | _ -> Pervasives.compare a b *) let compare = Pervasives.compare end (* module Domain = Set.Make (OrderedDomain) *) module Environment = struct module Environment' = Map.Make (OrderedDomain) include Environment' let find k env = try find k env with Not_found -> (* match k with | Symbol (sym,_) -> find (Symbol (sym,None)) env | Num _ -> find (Num None) env | Id (id,_) -> find (Id (id,None)) env *) raise Not_found let cons desc_of_alias k v env = let default_dom_item x = x in let env' = try let current = Environment'.find k env in let dsc = desc_of_alias v in add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env with Not_found -> add k [v] env in (* we also add default aliases *) let k' = default_dom_item k in try let current = find k' env' in let dsc = desc_of_alias v in add k' (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env' with Not_found -> add k' [v] env' end module InterprOD = struct type t = Stdpp.location let compare = Pervasives.compare end module InterprEnv = Map.Make (InterprOD) type 'term codomain_item = string * (* description *) [`Num_interp of string -> 'term |`Sym_interp of 'term list -> 'term] type interactive_user_uri_choice_type = selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> NReference.reference list -> NReference.reference list type interactive_interpretation_choice_type = string -> int -> (Stdpp.location list * string * string) list list -> int list type interactive_ast_choice_type = string list -> int type input_or_locate_uri_type = title:string -> ?id:string -> unit -> NReference.reference option (* let string_of_domain_item item = let f_opt f x default = match x with | None -> default | Some y -> f y in match item with | Id (s,huri) -> Printf.sprintf "ID(%s,%s)" s (f_opt (fun x -> x) huri "_") | Symbol (s,None) -> Printf.sprintf "SYMBOL(%s)" s | Symbol (s,Some (_,dsc)) -> Printf.sprintf "SYMBOL(%s,%s)" s dsc | Num _ -> "NUM" ;; *) let string_of_domain_item item = let f_opt f x default = match x with | None -> default | Some y -> f y in match item with | Id s -> Printf.sprintf "ID(%s)" s | Symbol s -> Printf.sprintf "SYMBOL(%s)" s | Num -> "NUM" ;;