1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 | Id of (string * string option) (* literal, opt. uri *)
31 | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
32 | Num of (string option * string) option (* opt. uri, interpretation *)
36 | Id of string (* literal *)
37 | Symbol of string (* literal *)
40 exception Invalid_choice of (Stdpp.location * string) Lazy.t
42 module OrderedDomain =
48 | Id (x,None), Id (y,_)
49 | Id (x,_), Id (y,None) when x = y -> 0
50 | Symbol (x,None), Symbol (y,_)
51 | Symbol (x,_), Symbol (y,None) when x = y -> 0
52 | _ -> Pervasives.compare a b *)
53 let compare = Pervasives.compare
56 (* module Domain = Set.Make (OrderedDomain) *)
59 module Environment' = Map.Make (OrderedDomain)
68 | Symbol (sym,_) -> find (Symbol (sym,None)) env
69 | Num _ -> find (Num None) env
70 | Id (id,_) -> find (Id (id,None)) env
73 let cons desc_of_alias k v env =
74 let default_dom_item x = x in
77 let current = Environment'.find k env in
78 let dsc = desc_of_alias v in
79 add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
83 (* we also add default aliases *)
84 let k' = default_dom_item k in
86 let current = find k' env' in
87 let dsc = desc_of_alias v in
88 add k' (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env'
96 type t = Stdpp.location
97 let compare = Pervasives.compare
100 module InterprEnv = Map.Make (InterprOD)
102 type 'term codomain_item =
103 string * (* description *)
104 [`Num_interp of string -> 'term
105 |`Sym_interp of 'term list -> 'term]
107 type interactive_user_uri_choice_type =
108 selection_mode:[`SINGLE | `MULTIPLE] ->
110 ?enable_button_for_non_vars:bool ->
111 title:string -> msg:string -> id:string -> NReference.reference list ->
112 NReference.reference list
114 type interactive_interpretation_choice_type = string -> int ->
115 (Stdpp.location list * string * string) list list -> int list
117 type interactive_ast_choice_type = string list -> int
119 type input_or_locate_uri_type =
120 title:string -> ?id:string -> unit -> NReference.reference option
123 let string_of_domain_item item =
124 let f_opt f x default =
131 Printf.sprintf "ID(%s,%s)" s (f_opt (fun x -> x) huri "_")
132 | Symbol (s,None) -> Printf.sprintf "SYMBOL(%s)" s
133 | Symbol (s,Some (_,dsc)) -> Printf.sprintf "SYMBOL(%s,%s)" s dsc
137 let string_of_domain_item item =
138 let f_opt f x default =
145 Printf.sprintf "ID(%s)" s
146 | Symbol s -> Printf.sprintf "SYMBOL(%s)" s