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/
28 exception BaseUriNotSetYet
31 (CicNotationPt.term, CicNotationPt.term,
32 CicNotationPt.term GrafiteAst.reduction, string)
36 (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
39 let singleton msg = function
43 Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
46 prerr_endline debug; assert false
48 let __Implicit = "__Implicit__"
49 let __Closed_Implicit = "__Closed_Implicit__"
51 let ncic_mk_choice = function
52 | LexiconAst.Symbol_alias (name, _, dsc) ->
53 if name = __Implicit then
54 dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
55 else if name = __Closed_Implicit then
56 dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
58 DisambiguateChoices.lookup_symbol_by_dsc
59 ~mk_implicit:(function
60 | true -> NCic.Implicit `Closed
61 | false -> NCic.Implicit `Term)
63 (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
64 ~term_of_uri:(fun _ -> assert false)
65 ~term_of_nref:(fun nref -> NCic.Const nref)
67 | LexiconAst.Number_alias (_, dsc) ->
68 let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
70 (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
71 | LexiconAst.Ident_alias (name, uri) ->
73 (fun l->assert(l = []);
75 let nref = NReference.reference_of_string uri in
78 NReference.IllFormedReference _ ->
79 let uri = UriManager.uri_of_string uri in
80 fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
87 LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
89 LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
92 let nlookup_in_library
93 interactive_user_uri_choice input_or_locate_uri item
96 | DisambiguateTypes.Id id ->
98 let references = NCicLibrary.resolve id in
100 (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
103 NCicEnvironment.ObjectNotFound _ -> [])
107 let fix_instance item l =
109 DisambiguateTypes.Symbol (_,n) ->
112 LexiconAst.Symbol_alias (s,_,d) -> LexiconAst.Symbol_alias (s,n,d)
115 | DisambiguateTypes.Num n ->
118 LexiconAst.Number_alias (_,d) -> LexiconAst.Number_alias (n,d)
121 | DisambiguateTypes.Id _ -> l
125 let disambiguate_nterm expty estatus context metasenv subst thing
127 let diff, metasenv, subst, cic =
129 (NCicDisambiguate.disambiguate_term
131 ~aliases:estatus#lstatus.LexiconEngine.aliases
133 ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
134 ~lookup_in_library:nlookup_in_library
135 ~mk_choice:ncic_mk_choice
136 ~mk_implicit ~fix_instance
137 ~description_of_alias:LexiconAst.description_of_alias
138 ~context ~metasenv ~subst thing)
140 let estatus = LexiconEngine.set_proof_aliases estatus diff in
141 metasenv, subst, estatus, cic
146 CicNotationPt.term Disambiguate.disambiguator_input option *
147 (string * NCic.term) list * NCic.term option
149 let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
150 let interp path = NCicDisambiguate.disambiguate_path path in
151 let goal_path = HExtlib.map_option interp goal_path in
152 let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
154 match wanted with None -> None | Some x -> Some (text,prefix_len,x)
156 (wanted, hyp_paths, goal_path)
159 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
160 | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
164 | `Whd as kind -> kind
167 let disambiguate_auto_params
168 disambiguate_term metasenv context (oterms, params)
171 | None -> metasenv, (None, params)
173 let metasenv, terms =
175 (fun t (metasenv, terms) ->
176 let metasenv,t = disambiguate_term context metasenv t in
177 metasenv,t::terms) terms (metasenv, [])
179 metasenv, (Some terms, params)
182 let disambiguate_just disambiguate_term context metasenv =
185 let metasenv,t = disambiguate_term context metasenv t in
188 let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
191 metasenv, `Auto params
194 let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
197 match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
201 | CicNotationPt.Inductive (_,(name,_,_,_)::_)
202 | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
203 | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
204 | CicNotationPt.Inductive _ -> assert false
206 UriManager.uri_of_string (baseuri ^ "/" ^ name)
208 let diff, _, _, cic =
210 (NCicDisambiguate.disambiguate_obj
211 ~lookup_in_library:nlookup_in_library
212 ~description_of_alias:LexiconAst.description_of_alias
213 ~mk_choice:ncic_mk_choice
214 ~mk_implicit ~fix_instance
215 ~uri:(OCic2NCic.nuri_of_ouri uri)
217 ~aliases:estatus#lstatus.LexiconEngine.aliases
218 ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
219 (text,prefix_len,obj)) in
220 let estatus = LexiconEngine.set_proof_aliases estatus diff in
223 let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
225 | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
226 | GrafiteAst.Select (loc,uri) ->
227 estatus, metasenv, GrafiteAst.Select(loc,uri)
228 | GrafiteAst.Pump(loc,i) ->
229 estatus, metasenv, GrafiteAst.Pump(loc,i)
230 | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false
231 | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false
232 | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false
233 | GrafiteAst.Default _
235 | GrafiteAst.Include _
238 | GrafiteAst.Set _ as cmd ->
240 | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
241 | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false