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/
29 aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
30 multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
31 new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
34 let initial_status = {
35 aliases = DisambiguateTypes.Environment.empty;
36 multi_aliases = DisambiguateTypes.Environment.empty;
42 inherit Interpretations.g_status
43 method disambiguate_db: db
46 class virtual status =
48 inherit Interpretations.status
49 val disambiguate_db = initial_status
50 method disambiguate_db = disambiguate_db
51 method set_disambiguate_db v = {< disambiguate_db = v >}
52 method set_disambiguate_status
53 : 'status. #g_status as 'status -> 'self
54 = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
57 let eval_with_new_aliases status f =
59 status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
61 let new_aliases = status#disambiguate_db.new_aliases in
65 let dump_aliases out msg status =
66 out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
67 DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
68 status#disambiguate_db.aliases
70 let set_proof_aliases status ~implicit_aliases mode new_aliases =
71 prerr_endline "set_proof_aliases";
72 if mode = GrafiteAst.WithoutPreferences then
75 (prerr_endline "set_proof_aliases 2";
77 List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
78 status#disambiguate_db.aliases new_aliases in
80 List.fold_left (fun acc (d,c) ->
81 DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
83 status#disambiguate_db.multi_aliases new_aliases
86 {multi_aliases = multi_aliases ;
89 (if implicit_aliases then new_aliases else []) @
90 status#disambiguate_db.new_aliases}
92 status#set_disambiguate_db new_status)
94 exception BaseUriNotSetYet
96 let singleton msg = function
100 Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
103 prerr_endline debug; assert false
105 let __Implicit = "__Implicit__"
106 let __Closed_Implicit = "__Closed_Implicit__"
108 let ncic_mk_choice status = function
109 | GrafiteAst.Symbol_alias (name,_, dsc) ->
110 if name = __Implicit then
111 dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
112 else if name = __Closed_Implicit then
113 dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
115 DisambiguateChoices.lookup_symbol_by_dsc status
116 ~mk_implicit:(function
117 | true -> NCic.Implicit `Closed
118 | false -> NCic.Implicit `Term)
120 (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
121 ~term_of_nref:(fun nref -> NCic.Const nref)
123 | GrafiteAst.Number_alias (_,dsc) ->
124 let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
126 (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
127 | GrafiteAst.Ident_alias (name, uri) ->
129 (fun l->assert(l = []);
130 let nref = NReference.reference_of_string uri in
138 GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
140 GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
143 let nlookup_in_library
144 interactive_user_uri_choice input_or_locate_uri item
147 | DisambiguateTypes.Id (id,_) ->
149 let references = NCicLibrary.resolve id in
152 GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
155 NCicEnvironment.ObjectNotFound _ -> [])
159 (* XXX TO BE REMOVED: no need to fix instances any more *)
160 (*let fix_instance item l =
162 DisambiguateTypes.Symbol (_,n) ->
165 GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
168 | DisambiguateTypes.Num n ->
171 GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
174 | DisambiguateTypes.Id _ -> l
176 let fix_instance _ l = l;;
179 let disambiguate_nterm status expty context metasenv subst thing
181 let newast, diff, metasenv, subst, cic =
183 (NCicDisambiguate.disambiguate_term
185 ~aliases:status#disambiguate_db.aliases
187 ~universe:(status#disambiguate_db.multi_aliases)
188 ~lookup_in_library:nlookup_in_library
189 ~mk_choice:(ncic_mk_choice status)
190 ~mk_implicit ~fix_instance
191 ~description_of_alias:GrafiteAst.description_of_alias
192 ~context ~metasenv ~subst thing)
195 set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
198 newast, metasenv, subst, status, cic
203 NotationPt.term Disambiguate.disambiguator_input option *
204 (string * NCic.term) list * NCic.term option
206 let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
207 let interp path = NCicDisambiguate.disambiguate_path status path in
208 let goal_path = HExtlib.map_option interp goal_path in
209 let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
210 let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
211 (wanted, hyp_paths, goal_path)
214 let disambiguate_reduction_kind text prefix_len = function
215 | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
219 | `Whd as kind -> kind
222 let disambiguate_auto_params
223 disambiguate_term metasenv context (oterms, params)
226 | None -> metasenv, (None, params)
228 let metasenv, terms =
230 (fun t (metasenv, terms) ->
231 let metasenv,t = disambiguate_term context metasenv t in
232 metasenv,t::terms) terms (metasenv, [])
234 metasenv, (Some terms, params)
237 let disambiguate_just disambiguate_term context metasenv =
240 let metasenv,t = disambiguate_term context metasenv t in
243 let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
246 metasenv, `Auto params
249 let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
252 match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
256 | NotationPt.Inductive (_,(name,_,_,_)::_)
257 | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
258 | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
259 | NotationPt.Inductive _ -> assert false
261 NUri.uri_of_string (baseuri ^ "/" ^ name)
263 let diff, _, _, cic =
265 (NCicDisambiguate.disambiguate_obj
267 ~lookup_in_library:nlookup_in_library
268 ~description_of_alias:GrafiteAst.description_of_alias
269 ~mk_choice:(ncic_mk_choice status)
270 ~mk_implicit ~fix_instance ~uri
271 ~aliases:status#disambiguate_db.aliases
272 ~universe:(status#disambiguate_db.multi_aliases)
273 (text,prefix_len,obj)) in
275 set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
281 let disambiguate_cic_appl_pattern status args =
282 let rec disambiguate =
284 NotationPt.ApplPattern l ->
285 NotationPt.ApplPattern (List.map disambiguate l)
286 | NotationPt.VarPattern id
289 (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
291 let item = DisambiguateTypes.Id (id,None) in
295 DisambiguateTypes.Environment.find item
296 status#disambiguate_db.aliases
298 GrafiteAst.Ident_alias (_,uri) ->
299 NotationPt.NRefPattern (NReference.reference_of_string uri)
303 ("LexiconEngine.eval_command: domain item not found: " ^
304 (DisambiguateTypes.string_of_domain_item item));
305 dump_aliases prerr_endline "" status;
308 ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
315 let aliases_for_objs status refs =
319 let references = NCicLibrary.aliases_of nref in
322 let name = NCicPp.r2s status true u in
323 DisambiguateTypes.Id (name, Some (NReference.string_of_reference u)),
324 GrafiteAst.Ident_alias (name,NReference.string_of_reference u)