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 HLog.debug debug; assert false
48 let __Implicit = "__Implicit__"
49 let __Closed_Implicit = "__Closed_Implicit__"
51 let cic_mk_choice = function
52 | LexiconAst.Symbol_alias (name, _, dsc) ->
53 if name = __Implicit then
54 dsc, `Sym_interp (fun _ -> Cic.Implicit None)
55 else if name = __Closed_Implicit then
56 dsc, `Sym_interp (fun _ -> Cic.Implicit (Some `Closed))
58 DisambiguateChoices.cic_lookup_symbol_by_dsc name dsc
59 | LexiconAst.Number_alias (_, dsc) ->
60 DisambiguateChoices.lookup_num_by_dsc dsc
61 | LexiconAst.Ident_alias (name, uri) ->
63 (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri))
66 let ncic_mk_choice = function
67 | LexiconAst.Symbol_alias (name, _, dsc) ->
68 if name = __Implicit then
69 dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
70 else if name = __Closed_Implicit then
71 dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
73 DisambiguateChoices.lookup_symbol_by_dsc
74 ~mk_implicit:(function
75 | true -> NCic.Implicit `Closed
76 | false -> NCic.Implicit `Term)
78 (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
79 ~term_of_uri:(fun uri ->
80 fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
82 | LexiconAst.Number_alias (_, dsc) ->
83 let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
86 fst (OCic2NCic.convert_term
87 (UriManager.uri_of_string "cic:/xxx/x.con")
88 (match f with `Num_interp f -> f num | _ -> assert false)))
89 | LexiconAst.Ident_alias (name, uri) ->
91 (fun l->assert(l = []);
93 let nref = NReference.reference_of_string uri in
96 NReference.IllFormedReference _ ->
97 let uri = UriManager.uri_of_string uri in
98 fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
105 LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
107 LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
110 let lookup_in_library
111 interactive_user_uri_choice input_or_locate_uri item
113 let mk_ident_alias id u =
114 LexiconAst.Ident_alias (id,UriManager.string_of_uri u)
116 let mk_num_alias instance =
118 (fun dsc,_ -> LexiconAst.Number_alias (instance,dsc))
119 (DisambiguateChoices.lookup_num_choices())
121 let mk_symbol_alias symb ino (dsc, _,_) =
122 LexiconAst.Symbol_alias (symb,ino,dsc)
124 let dbd = LibraryDb.instance () in
125 let choices_of_id id =
126 let uris = Whelp.locate ~dbd id in
131 ~title:("URI matching \"" ^ id ^ "\" unknown.")
138 interactive_user_uri_choice ~selection_mode:`MULTIPLE
139 ?ok:(Some "Try selected.")
140 ?enable_button_for_non_vars:(Some true)
141 ~title:"Ambiguous input."
142 ~msg: ("Ambiguous input \"" ^ id ^
143 "\". Please, choose one or more interpretations:")
148 | DisambiguateTypes.Id id ->
149 let uris = choices_of_id id in
150 List.map (mk_ident_alias id) uris
151 | DisambiguateTypes.Symbol (symb, ino) ->
153 List.map (mk_symbol_alias symb ino)
154 (TermAcicContent.lookup_interpretations symb)
156 TermAcicContent.Interpretation_not_found -> [])
157 | DisambiguateTypes.Num instance -> mk_num_alias instance
160 let nlookup_in_library
161 interactive_user_uri_choice input_or_locate_uri item
164 | DisambiguateTypes.Id id ->
166 let references = NCicLibrary.resolve id in
168 (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
170 lookup_in_library interactive_user_uri_choice input_or_locate_uri item
172 NCicLibrary.ObjectNotFound _ ->
173 lookup_in_library interactive_user_uri_choice input_or_locate_uri item)
174 | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item
177 (** @param term not meaningful when context is given *)
178 let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
180 let lexicon_status = !lexicon_status_ref in
181 let (diff, metasenv, subst, cic, _) =
183 (CicDisambiguate.disambiguate_term
184 ~aliases:lexicon_status.LexiconEngine.aliases
185 ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
187 ~mk_choice:cic_mk_choice
189 ~description_of_alias:LexiconAst.description_of_alias
190 ~context ~metasenv ~subst:[] (text,prefix_len,term))
192 let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
193 lexicon_status_ref := lexicon_status;
194 metasenv,(*subst,*) cic
197 let disambiguate_nterm expty lexicon_status context metasenv subst thing
199 let diff, metasenv, subst, cic =
201 (NCicDisambiguate.disambiguate_term
202 ~coercion_db:(NCicCoercion.db ())
203 ~aliases:lexicon_status.LexiconEngine.aliases
205 ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
206 ~lookup_in_library:nlookup_in_library
207 ~mk_choice:ncic_mk_choice
209 ~description_of_alias:LexiconAst.description_of_alias
210 ~context ~metasenv ~subst thing)
212 let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
213 metasenv, subst, lexicon_status, cic
217 (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
218 * rationale: lazy_term will be invoked in different context to obtain a term,
219 * each invocation will disambiguate the term and can add aliases. Once all
220 * disambiguations have been performed, the first returned function can be
221 * used to obtain the resulting aliases *)
222 let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
223 (fun context metasenv ugraph ->
224 let lexicon_status = !lexicon_status_ref in
225 let (diff, metasenv, _, cic, ugraph) =
227 (CicDisambiguate.disambiguate_term
229 ~mk_choice:cic_mk_choice
231 ~description_of_alias:LexiconAst.description_of_alias
232 ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
233 ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
234 ~context ~metasenv ~subst:[]
235 (text,prefix_len,term) ~expty) in
236 let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
237 lexicon_status_ref := lexicon_status;
238 cic, metasenv, ugraph)
241 let disambiguate_pattern
242 text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path)
244 let interp path =CicDisambiguate.interpretate_path [] path in
245 let goal_path = HExtlib.map_option interp goal_path in
246 let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
252 disambiguate_lazy_term None text prefix_len lexicon_status_ref wanted
256 (wanted, hyp_paths, goal_path)
260 CicNotationPt.term Disambiguate.disambiguator_input option *
261 (string * NCic.term) list * NCic.term option
263 let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
264 let interp path = NCicDisambiguate.disambiguate_path path in
265 let goal_path = HExtlib.map_option interp goal_path in
266 let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
268 match wanted with None -> None | Some x -> Some (text,prefix_len,x)
270 (wanted, hyp_paths, goal_path)
273 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
274 | `Unfold (Some t) ->
276 disambiguate_lazy_term None text prefix_len lexicon_status_ref t in
281 | `Whd as kind -> kind
284 let disambiguate_auto_params
285 disambiguate_term metasenv context (terms, params)
287 let metasenv, terms =
289 (fun t (metasenv, terms) ->
290 let metasenv,t = disambiguate_term context metasenv t in
291 metasenv,t::terms) terms (metasenv, [])
293 metasenv, (terms, params)
296 let disambiguate_just disambiguate_term context metasenv =
299 let metasenv,t = disambiguate_term context metasenv t in
302 let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
305 metasenv, `Auto params
308 let rec disambiguate_tactic
309 lexicon_status_ref context metasenv goal (text,prefix_len,tactic)
311 let disambiguate_term_hint =
313 List.find (fun (x,_,_) -> Some x = goal) metasenv
315 disambiguate_term (Some expty) text prefix_len lexicon_status_ref in
316 let disambiguate_term =
317 disambiguate_term None text prefix_len lexicon_status_ref in
318 let disambiguate_pattern =
319 disambiguate_pattern text prefix_len lexicon_status_ref in
320 let disambiguate_reduction_kind =
321 disambiguate_reduction_kind text prefix_len lexicon_status_ref in
322 let disambiguate_lazy_term =
323 disambiguate_lazy_term None text prefix_len lexicon_status_ref in
324 let disambiguate_tactic metasenv tac =
325 disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tac)
327 let disambiguate_auto_params m p =
328 disambiguate_auto_params disambiguate_term m context p
331 (* Higher order tactics *)
332 | GrafiteAst.Progress (loc,tac) ->
333 let metasenv,tac = disambiguate_tactic metasenv tac in
334 metasenv,GrafiteAst.Progress (loc,tac)
335 | GrafiteAst.Solve (loc,tacl) ->
338 (fun tac (metasenv,tacl) ->
339 let metasenv,tac = disambiguate_tactic metasenv tac in
343 metasenv,GrafiteAst.Solve (loc,tacl)
344 | GrafiteAst.Try (loc,tac) ->
345 let metasenv,tac = disambiguate_tactic metasenv tac in
346 metasenv,GrafiteAst.Try (loc,tac)
347 | GrafiteAst.First (loc,tacl) ->
350 (fun tac (metasenv,tacl) ->
351 let metasenv,tac = disambiguate_tactic metasenv tac in
355 metasenv,GrafiteAst.First (loc,tacl)
356 | GrafiteAst.Seq (loc,tacl) ->
359 (fun tac (metasenv,tacl) ->
360 let metasenv,tac = disambiguate_tactic metasenv tac in
364 metasenv,GrafiteAst.Seq (loc,tacl)
365 | GrafiteAst.Repeat (loc,tac) ->
366 let metasenv,tac = disambiguate_tactic metasenv tac in
367 metasenv,GrafiteAst.Repeat (loc,tac)
368 | GrafiteAst.Do (loc,n,tac) ->
369 let metasenv,tac = disambiguate_tactic metasenv tac in
370 metasenv,GrafiteAst.Do (loc,n,tac)
371 | GrafiteAst.Then (loc,tac,tacl) ->
372 let metasenv,tac = disambiguate_tactic metasenv tac in
375 (fun tac (metasenv,tacl) ->
376 let metasenv,tac = disambiguate_tactic metasenv tac in
380 metasenv,GrafiteAst.Then (loc,tac,tacl)
381 (* First order tactics *)
382 | GrafiteAst.Absurd (loc, term) ->
383 let metasenv,cic = disambiguate_term context metasenv term in
384 metasenv,GrafiteAst.Absurd (loc, cic)
385 | GrafiteAst.Apply (loc, term) ->
386 let metasenv,cic = disambiguate_term context metasenv term in
387 metasenv,GrafiteAst.Apply (loc, cic)
388 | GrafiteAst.ApplyRule (loc, term) ->
389 let metasenv,cic = disambiguate_term_hint context metasenv term in
390 metasenv,GrafiteAst.ApplyRule (loc, cic)
391 | GrafiteAst.ApplyP (loc, term) ->
392 let metasenv,cic = disambiguate_term context metasenv term in
393 metasenv,GrafiteAst.ApplyP (loc, cic)
394 | GrafiteAst.ApplyS (loc, term, params) ->
395 let metasenv, params = disambiguate_auto_params metasenv params in
396 let metasenv,cic = disambiguate_term context metasenv term in
397 metasenv,GrafiteAst.ApplyS (loc, cic, params)
398 | GrafiteAst.Assumption loc ->
399 metasenv,GrafiteAst.Assumption loc
400 | GrafiteAst.AutoBatch (loc,params) ->
401 let metasenv, params = disambiguate_auto_params metasenv params in
402 metasenv,GrafiteAst.AutoBatch (loc,params)
403 | GrafiteAst.Cases (loc, what, pattern, idents) ->
404 let metasenv,what = disambiguate_term context metasenv what in
405 let pattern = disambiguate_pattern pattern in
406 metasenv,GrafiteAst.Cases (loc, what, pattern, idents)
407 | GrafiteAst.Change (loc, pattern, with_what) ->
408 let with_what = disambiguate_lazy_term with_what in
409 let pattern = disambiguate_pattern pattern in
410 metasenv,GrafiteAst.Change (loc, pattern, with_what)
411 | GrafiteAst.Clear (loc,id) ->
412 metasenv,GrafiteAst.Clear (loc,id)
413 | GrafiteAst.ClearBody (loc,id) ->
414 metasenv,GrafiteAst.ClearBody (loc,id)
415 | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
416 let metasenv,t1 = disambiguate_term context metasenv t1 in
419 | None -> metasenv, None
421 let m, t2 = disambiguate_term context metasenv t2 in
424 metasenv, GrafiteAst.Compose (loc, t1, t2, times, spec)
425 | GrafiteAst.Constructor (loc,n) ->
426 metasenv,GrafiteAst.Constructor (loc,n)
427 | GrafiteAst.Contradiction loc ->
428 metasenv,GrafiteAst.Contradiction loc
429 | GrafiteAst.Cut (loc, ident, term) ->
430 let metasenv,cic = disambiguate_term context metasenv term in
431 metasenv,GrafiteAst.Cut (loc, ident, cic)
432 | GrafiteAst.Decompose (loc, names) ->
433 metasenv,GrafiteAst.Decompose (loc, names)
434 | GrafiteAst.Demodulate (loc, params) ->
435 let metasenv, params = disambiguate_auto_params metasenv params in
436 metasenv,GrafiteAst.Demodulate (loc, params)
437 | GrafiteAst.Destruct (loc, Some terms) ->
438 let map term (metasenv, terms) =
439 let metasenv, term = disambiguate_term context metasenv term in
440 metasenv, term :: terms
442 let metasenv, terms = List.fold_right map terms (metasenv, []) in
443 metasenv, GrafiteAst.Destruct(loc, Some terms)
444 | GrafiteAst.Destruct (loc, None) ->
445 metasenv,GrafiteAst.Destruct(loc,None)
446 | GrafiteAst.Exact (loc, term) ->
447 let metasenv,cic = disambiguate_term context metasenv term in
448 metasenv,GrafiteAst.Exact (loc, cic)
449 | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
450 let metasenv,what = disambiguate_term context metasenv what in
451 let metasenv,using = disambiguate_term context metasenv using in
452 let pattern = disambiguate_pattern pattern in
453 metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
454 | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
455 let metasenv,what = disambiguate_term context metasenv what in
456 let pattern = disambiguate_pattern pattern in
457 metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
458 | GrafiteAst.ElimType (loc, what, Some using, specs) ->
459 let metasenv,what = disambiguate_term context metasenv what in
460 let metasenv,using = disambiguate_term context metasenv using in
461 metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
462 | GrafiteAst.ElimType (loc, what, None, specs) ->
463 let metasenv,what = disambiguate_term context metasenv what in
464 metasenv,GrafiteAst.ElimType (loc, what, None, specs)
465 | GrafiteAst.Exists loc ->
466 metasenv,GrafiteAst.Exists loc
467 | GrafiteAst.Fail loc ->
468 metasenv,GrafiteAst.Fail loc
469 | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
470 let pattern = disambiguate_pattern pattern in
471 let term = disambiguate_lazy_term term in
472 let red_kind = disambiguate_reduction_kind red_kind in
473 metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
474 | GrafiteAst.FwdSimpl (loc, hyp, names) ->
475 metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)
476 | GrafiteAst.Fourier loc ->
477 metasenv,GrafiteAst.Fourier loc
478 | GrafiteAst.Generalize (loc,pattern,ident) ->
479 let pattern = disambiguate_pattern pattern in
480 metasenv,GrafiteAst.Generalize (loc,pattern,ident)
481 | GrafiteAst.IdTac loc ->
482 metasenv,GrafiteAst.IdTac loc
483 | GrafiteAst.Intros (loc, specs) ->
484 metasenv,GrafiteAst.Intros (loc, specs)
485 | GrafiteAst.Inversion (loc, term) ->
486 let metasenv,term = disambiguate_term context metasenv term in
487 metasenv,GrafiteAst.Inversion (loc, term)
488 | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
489 let f term (metasenv, to_what) =
490 let metasenv, term = disambiguate_term context metasenv term in
491 metasenv, term :: to_what
493 let metasenv, to_what = List.fold_right f to_what (metasenv, []) in
494 let metasenv, what = disambiguate_term context metasenv what in
495 metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
496 | GrafiteAst.Left loc ->
497 metasenv,GrafiteAst.Left loc
498 | GrafiteAst.LetIn (loc, term, name) ->
499 let metasenv,term = disambiguate_term context metasenv term in
500 metasenv,GrafiteAst.LetIn (loc,term,name)
501 | GrafiteAst.Reduce (loc, red_kind, pattern) ->
502 let pattern = disambiguate_pattern pattern in
503 let red_kind = disambiguate_reduction_kind red_kind in
504 metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
505 | GrafiteAst.Reflexivity loc ->
506 metasenv,GrafiteAst.Reflexivity loc
507 | GrafiteAst.Replace (loc, pattern, with_what) ->
508 let pattern = disambiguate_pattern pattern in
509 let with_what = disambiguate_lazy_term with_what in
510 metasenv,GrafiteAst.Replace (loc, pattern, with_what)
511 | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
512 let metasenv,term = disambiguate_term context metasenv t in
513 let pattern = disambiguate_pattern pattern in
514 metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
515 | GrafiteAst.Right loc ->
516 metasenv,GrafiteAst.Right loc
517 | GrafiteAst.Ring loc ->
518 metasenv,GrafiteAst.Ring loc
519 | GrafiteAst.Split loc ->
520 metasenv,GrafiteAst.Split loc
521 | GrafiteAst.Symmetry loc ->
522 metasenv,GrafiteAst.Symmetry loc
523 | GrafiteAst.Transitivity (loc, term) ->
524 let metasenv,cic = disambiguate_term context metasenv term in
525 metasenv,GrafiteAst.Transitivity (loc, cic)
527 | GrafiteAst.Assume (loc, id, term) ->
528 let metasenv,cic = disambiguate_term context metasenv term in
529 metasenv,GrafiteAst.Assume (loc, id, cic)
530 | GrafiteAst.Suppose (loc, term, id, term') ->
531 let metasenv,cic = disambiguate_term context metasenv term in
534 None -> metasenv,None
536 let metasenv,t = disambiguate_term context metasenv t in
538 metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
539 | GrafiteAst.Bydone (loc,just) ->
541 disambiguate_just disambiguate_term context metasenv just
543 metasenv,GrafiteAst.Bydone (loc, just)
544 | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
545 let metasenv,cic = disambiguate_term context metasenv term in
548 None -> metasenv,None
550 let metasenv,t = disambiguate_term context metasenv t in
552 metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
553 | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') ->
555 disambiguate_just disambiguate_term context metasenv just in
556 let metasenv,cic' = disambiguate_term context metasenv term' in
559 None -> metasenv,None
561 let metasenv,t = disambiguate_term context metasenv t in
563 metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'')
564 | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
565 let metasenv,cic = disambiguate_term context metasenv term in
566 let metasenv,cic' = disambiguate_term context metasenv term' in
567 metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
568 | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
569 let metasenv,cic = disambiguate_term context metasenv term in
570 let metasenv,cic' = disambiguate_term context metasenv term' in
571 metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
572 | GrafiteAst.Byinduction (loc, term, id) ->
573 let metasenv,cic = disambiguate_term context metasenv term in
574 metasenv,GrafiteAst.Byinduction(loc, cic, id)
575 | GrafiteAst.Thesisbecomes (loc, term) ->
576 let metasenv,cic = disambiguate_term context metasenv term in
577 metasenv,GrafiteAst.Thesisbecomes (loc, cic)
578 | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) ->
580 disambiguate_just disambiguate_term context metasenv just in
581 let metasenv,cic' = disambiguate_term context metasenv term1 in
582 let cic''= disambiguate_lazy_term term2 in
583 metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'')
584 | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) ->
586 disambiguate_just disambiguate_term context metasenv just in
587 let metasenv,cic'= disambiguate_term context metasenv term1 in
588 let metasenv,cic''= disambiguate_term context metasenv term2 in
589 metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'')
590 | GrafiteAst.Case (loc, id, params) ->
591 let metasenv,params' =
593 (fun (id,term) (metasenv,params) ->
594 let metasenv,cic = disambiguate_term context metasenv term in
595 metasenv,(id,cic)::params
596 ) params (metasenv,[])
598 metasenv,GrafiteAst.Case(loc, id, params')
599 | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
602 None -> metasenv,None
604 let metasenv,t = disambiguate_term context metasenv t in
605 metasenv,Some (start,t) in
606 let metasenv,cic'= disambiguate_term context metasenv term2 in
610 let metasenv,term = disambiguate_term context metasenv term in
611 metasenv, `SolveWith term
613 let metasenv, params = disambiguate_auto_params metasenv params in
614 metasenv,`Auto params
616 let metasenv,t = disambiguate_term context metasenv t in
618 | `Proof as t -> metasenv,t in
619 metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
621 let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
624 match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
628 | CicNotationPt.Inductive (_,(name,_,_,_)::_)
629 | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
630 | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
631 | CicNotationPt.Inductive _ -> assert false
633 UriManager.uri_of_string (baseuri ^ "/" ^ name)
636 (NCicLibrary.clear_cache ();
637 NCicEnvironment.invalidate ();
641 | Some (Cic.CurrentProof (_,metasenv, _, ty,_,_)) ->
643 CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph
646 | Some (Cic.Constant (_,_, ty,_,_)) ->
648 CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph
651 | _ -> CicUniv.empty_ugraph
655 prerr_endline "PRIMA COERCIONS";
656 let _,l = CicUniv.do_rank graph in
658 prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
659 (CicUniv.get_rank k))) l;
664 (fun graph (_,_,l) ->
666 (fun graph (uri,_,_) ->
667 let _,g = CicTypeChecker.typecheck uri in
668 CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
670 graph (CoercDb.to_list ())
672 ignore(CicUniv.do_rank graph);
676 prerr_endline "DOPO COERCIONS";
677 let _,l = CicUniv.do_rank graph in
679 prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
680 (CicUniv.get_rank k))) l;
684 prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
685 let time = Unix.gettimeofday () in
688 NCicDisambiguate.disambiguate_obj
689 ~lookup_in_library:nlookup_in_library
690 ~description_of_alias:LexiconAst.description_of_alias
691 ~mk_choice:ncic_mk_choice
693 ~uri:(OCic2NCic.nuri_of_ouri uri)
694 ~coercion_db:(NCicCoercion.db ())
695 ~aliases:lexicon_status.LexiconEngine.aliases
696 ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
697 (text,prefix_len,obj)
700 let time = Unix.gettimeofday () -. time in
701 (* NCicTypeChecker.typecheck_obj obj; *)
702 prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
705 let u,i,m,_,o = obj in
709 prerr_endline (NCicPp.ppobj obj)
711 prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! "))
713 | MultiPassDisambiguator.DisambiguationError (_,s) ->
714 prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE ("
715 ^UriManager.string_of_uri uri^
718 (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
719 (* | exn -> prerr_endline (Printexc.to_string exn) *)
726 (* let time = Unix.gettimeofday () in *)
729 let (diff, metasenv, _, cic, _) =
731 (CicDisambiguate.disambiguate_obj
733 ~mk_choice:cic_mk_choice
735 ~description_of_alias:LexiconAst.description_of_alias
736 ~aliases:lexicon_status.LexiconEngine.aliases
737 ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
739 (text,prefix_len,obj)) in
743 let time = Unix.gettimeofday () -. time in
744 prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
745 UriManager.string_of_uri uri ^"): " ^ string_of_float time);
747 (* try_new (Some cic); *)
750 let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
751 lexicon_status, metasenv, cic
754 | Sys.Break as exn -> raise exn
760 let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
763 match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
767 | CicNotationPt.Inductive (_,(name,_,_,_)::_)
768 | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
769 | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
770 | CicNotationPt.Inductive _ -> assert false
772 UriManager.uri_of_string (baseuri ^ "/" ^ name)
774 let diff, _, _, cic =
776 (NCicDisambiguate.disambiguate_obj
777 ~lookup_in_library:nlookup_in_library
778 ~description_of_alias:LexiconAst.description_of_alias
779 ~mk_choice:ncic_mk_choice
781 ~uri:(OCic2NCic.nuri_of_ouri uri)
782 ~coercion_db:(NCicCoercion.db ())
783 ~aliases:lexicon_status.LexiconEngine.aliases
784 ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
785 (text,prefix_len,obj)) in
786 let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
790 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
792 | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj)
793 | GrafiteAst.Index(loc,key,uri) ->
794 let lexicon_status_ref = ref lexicon_status in
795 let disambiguate_term =
796 disambiguate_term None text prefix_len lexicon_status_ref [] in
797 let disambiguate_term_option metasenv =
799 None -> metasenv,None
801 let metasenv,t = disambiguate_term metasenv t in
804 let metasenv,key = disambiguate_term_option metasenv key in
805 !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
806 | GrafiteAst.Select (loc,uri) ->
807 lexicon_status, metasenv, GrafiteAst.Select(loc,uri)
808 | GrafiteAst.Pump(loc,i) ->
809 lexicon_status, metasenv, GrafiteAst.Pump(loc,i)
810 | GrafiteAst.PreferCoercion (loc,t) ->
811 let lexicon_status_ref = ref lexicon_status in
812 let disambiguate_term =
813 disambiguate_term None text prefix_len lexicon_status_ref [] in
814 let metasenv,t = disambiguate_term metasenv t in
815 !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t)
816 | GrafiteAst.Coercion (loc,t,b,a,s) ->
817 let lexicon_status_ref = ref lexicon_status in
818 let disambiguate_term =
819 disambiguate_term None text prefix_len lexicon_status_ref [] in
820 let metasenv,t = disambiguate_term metasenv t in
821 !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
822 | GrafiteAst.Inverter (loc,n,indty,params) ->
823 let lexicon_status_ref = ref lexicon_status in
824 let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in
825 let metasenv,indty = disambiguate_term metasenv indty in
826 !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
827 | GrafiteAst.UnificationHint (loc, t, n) ->
828 let lexicon_status_ref = ref lexicon_status in
829 let disambiguate_term =
830 disambiguate_term None text prefix_len lexicon_status_ref [] in
831 let metasenv,t = disambiguate_term metasenv t in
832 !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t,n)
833 | GrafiteAst.Default _
835 | GrafiteAst.Include _
839 | GrafiteAst.NUnivConstraint _
840 | GrafiteAst.Set _ as cmd ->
841 lexicon_status,metasenv,cmd
842 | GrafiteAst.Obj (loc,obj) ->
843 let lexicon_status,metasenv,obj =
844 disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
845 lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
846 | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
847 let lexicon_status_ref = ref lexicon_status in
848 let disambiguate_term =
849 disambiguate_term None text prefix_len lexicon_status_ref [] in
850 let disambiguate_term_option metasenv =
852 None -> metasenv,None
854 let metasenv,t = disambiguate_term metasenv t in
857 let metasenv,a = disambiguate_term metasenv a in
858 let metasenv,aeq = disambiguate_term metasenv aeq in
859 let metasenv,refl = disambiguate_term_option metasenv refl in
860 let metasenv,sym = disambiguate_term_option metasenv sym in
861 let metasenv,trans = disambiguate_term_option metasenv trans in
862 !lexicon_status_ref, metasenv,
863 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
865 let disambiguate_macro
866 lexicon_status_ref metasenv context (text,prefix_len, macro)
868 let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in
869 let disambiguate_reduction_kind =
870 disambiguate_reduction_kind text prefix_len lexicon_status_ref in
872 | GrafiteAst.WMatch (loc,term) ->
873 let metasenv,term = disambiguate_term context metasenv term in
874 metasenv,GrafiteAst.WMatch (loc,term)
875 | GrafiteAst.WInstance (loc,term) ->
876 let metasenv,term = disambiguate_term context metasenv term in
877 metasenv,GrafiteAst.WInstance (loc,term)
878 | GrafiteAst.WElim (loc,term) ->
879 let metasenv,term = disambiguate_term context metasenv term in
880 metasenv,GrafiteAst.WElim (loc,term)
881 | GrafiteAst.WHint (loc,term) ->
882 let metasenv,term = disambiguate_term context metasenv term in
883 metasenv,GrafiteAst.WHint (loc,term)
884 | GrafiteAst.Check (loc,term) ->
885 let metasenv,term = disambiguate_term context metasenv term in
886 metasenv,GrafiteAst.Check (loc,term)
887 | GrafiteAst.Eval (loc,kind,term) ->
888 let metasenv, term = disambiguate_term context metasenv term in
889 let kind = disambiguate_reduction_kind kind in
890 metasenv,GrafiteAst.Eval (loc,kind,term)
891 | GrafiteAst.AutoInteractive (loc, params) ->
892 let metasenv, params =
893 disambiguate_auto_params disambiguate_term metasenv context params in
894 metasenv, GrafiteAst.AutoInteractive (loc, params)
896 | GrafiteAst.WLocate _
897 | GrafiteAst.Inline _ as macro ->