]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/disambiguation/disambiguateTypes.ml
8db0c220d302e46bdd9b3a210880dff6a170ae90
[helm.git] / matitaB / components / disambiguation / disambiguateTypes.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 type domain_item =
29  | Id of (string * string option)              (* literal, opt. uri *)
30  | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
31  | Num of (string option * string) option             (* opt. uri, interpretation *)
32
33 (*
34 type domain_item =
35  | Id of string     (* literal *)
36  | Symbol of string (* literal *)
37  | Num 
38  *)
39
40 exception Invalid_choice of (Stdpp.location * string) Lazy.t
41
42 module OrderedDomain =
43   struct
44     type t = domain_item
45     let compare = Pervasives.compare
46   end
47
48 (* module Domain = Set.Make (OrderedDomain) *)
49 module Environment =
50 struct
51   module Environment' = Map.Make (OrderedDomain)
52
53   include Environment'
54
55   let find k env =
56     try find k env 
57     with Not_found -> 
58       match k with
59        | Symbol (sym,_) -> find (Symbol (sym,None)) env
60        | Num _ -> find (Num None) env
61        | Id (id,_) -> find (Id (id,None)) env 
62
63   let cons desc_of_alias k v env =
64     let default_dom_item = function
65     | Id (s,_) -> Id (s,None)
66     | Symbol (s,_) -> Symbol (s,None)
67     | Num _ -> Num None
68     in
69     (*
70     try
71       let current = find k env in
72       let dsc = desc_of_alias v in
73       let entry = v::(List.filter (fun x -> desc_of_alias x <> dsc) current) in
74       let id = match k with
75         | Id (id,_) -> id
76         | Symbol (sym,_) -> "SYMBOL:"^sym
77         | Num _ -> "NUM"
78       in
79       prerr_endline (Printf.sprintf "updated alias for %s with entry of length %d (was: %d)" id (List.length entry) (List.length current));
80       let res = add k entry env
81       in
82       let test = find k res in
83       prerr_endline (Printf.sprintf "so the current length of the entry is %d."
84         (List.length test));
85       res
86     with Not_found -> add k [v] env
87     *)
88     let env' =
89       try
90         let current = find k env in
91         let dsc = desc_of_alias v in
92         add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
93       with Not_found ->
94         add k [v] env
95     in
96     (* we also add default aliases *)
97     let k' = default_dom_item k in
98     try
99       let current = find k' env' in
100       let dsc = desc_of_alias v in
101       add k' (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env'
102     with Not_found ->
103       add k' [v] env'
104
105 end
106
107 type 'term codomain_item =
108   string *  (* description *)
109    [`Num_interp of string -> 'term
110    |`Sym_interp of 'term list -> 'term]
111
112 type interactive_user_uri_choice_type =
113   selection_mode:[`SINGLE | `MULTIPLE] ->
114   ?ok:string ->
115   ?enable_button_for_non_vars:bool ->
116   title:string -> msg:string -> id:string -> NReference.reference list ->
117    NReference.reference list
118
119 type interactive_interpretation_choice_type = string -> int ->
120   (Stdpp.location list * string * string) list list -> int list
121
122 type input_or_locate_uri_type = 
123   title:string -> ?id:string -> unit -> NReference.reference option
124
125 let string_of_domain_item item =
126   let f_opt f x default =
127     match x with
128     | None -> default
129     | Some y -> f y
130   in
131   match item with
132   | Id (s,huri) -> 
133      Printf.sprintf "ID(%s,%s)" s (f_opt (fun x -> x) huri "_")
134   | Symbol (s,_) -> Printf.sprintf "SYMBOL(%s)" s
135   | Num _ -> "NUM"
136 ;;
137