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 inherit LexiconTypes.g_status
35 inherit LexiconTypes.status
36 method set_grafite_disambiguate_status
37 : 'status. #g_status as 'status -> 'self
38 = fun o -> (self#set_lexicon_engine_status o)
41 exception BaseUriNotSetYet
43 let singleton msg = function
47 Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
50 prerr_endline debug; assert false
52 let __Implicit = "__Implicit__"
53 let __Closed_Implicit = "__Closed_Implicit__"
55 let ncic_mk_choice status = function
56 | GrafiteAst.Symbol_alias (name, _, dsc) ->
57 if name = __Implicit then
58 dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
59 else if name = __Closed_Implicit then
60 dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
62 DisambiguateChoices.lookup_symbol_by_dsc status
63 ~mk_implicit:(function
64 | true -> NCic.Implicit `Closed
65 | false -> NCic.Implicit `Term)
67 (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
68 ~term_of_nref:(fun nref -> NCic.Const nref)
70 | GrafiteAst.Number_alias (_, dsc) ->
71 let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
73 (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
74 | GrafiteAst.Ident_alias (name, uri) ->
76 (fun l->assert(l = []);
77 let nref = NReference.reference_of_string uri in
85 GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
87 GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
90 let nlookup_in_library
91 interactive_user_uri_choice input_or_locate_uri item
94 | DisambiguateTypes.Id id ->
96 let references = NCicLibrary.resolve id in
98 (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
101 NCicEnvironment.ObjectNotFound _ -> [])
105 let fix_instance item l =
107 DisambiguateTypes.Symbol (_,n) ->
110 GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
113 | DisambiguateTypes.Num n ->
116 GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
119 | DisambiguateTypes.Id _ -> l
123 let disambiguate_nterm expty estatus context metasenv subst thing
125 let diff, metasenv, subst, cic =
127 (NCicDisambiguate.disambiguate_term
129 ~aliases:estatus#lstatus.LexiconTypes.aliases
131 ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
132 ~lookup_in_library:nlookup_in_library
133 ~mk_choice:(ncic_mk_choice estatus)
134 ~mk_implicit ~fix_instance
135 ~description_of_alias:GrafiteAst.description_of_alias
136 ~context ~metasenv ~subst thing)
139 LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
140 GrafiteAst.WithPreferences diff
142 metasenv, subst, estatus, cic
147 NotationPt.term Disambiguate.disambiguator_input option *
148 (string * NCic.term) list * NCic.term option
150 let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
151 let interp path = NCicDisambiguate.disambiguate_path path in
152 let goal_path = HExtlib.map_option interp goal_path in
153 let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
155 match wanted with None -> None | Some x -> Some (text,prefix_len,x)
157 (wanted, hyp_paths, goal_path)
160 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
161 | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
165 | `Whd as kind -> kind
168 let disambiguate_auto_params
169 disambiguate_term metasenv context (oterms, params)
172 | None -> metasenv, (None, params)
174 let metasenv, terms =
176 (fun t (metasenv, terms) ->
177 let metasenv,t = disambiguate_term context metasenv t in
178 metasenv,t::terms) terms (metasenv, [])
180 metasenv, (Some terms, params)
183 let disambiguate_just disambiguate_term context metasenv =
186 let metasenv,t = disambiguate_term context metasenv t in
189 let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
192 metasenv, `Auto params
195 let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
198 match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
202 | NotationPt.Inductive (_,(name,_,_,_)::_)
203 | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
204 | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
205 | NotationPt.Inductive _ -> assert false
207 NUri.uri_of_string (baseuri ^ "/" ^ name)
209 let diff, _, _, cic =
211 (NCicDisambiguate.disambiguate_obj
212 ~lookup_in_library:nlookup_in_library
213 ~description_of_alias:GrafiteAst.description_of_alias
214 ~mk_choice:(ncic_mk_choice estatus)
215 ~mk_implicit ~fix_instance
218 ~aliases:estatus#lstatus.LexiconTypes.aliases
219 ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
220 (text,prefix_len,obj)) in
222 LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
223 GrafiteAst.WithPreferences diff