HLog.debug debug; assert false
(** @param term not meaningful when context is given *)
-let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
+let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
+term =
let lexicon_status = !lexicon_status_ref in
- let (diff, metasenv, cic, _) =
+ let (diff, metasenv, subst, cic, _) =
singleton "first"
(GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~context ~metasenv (text,prefix_len,term))
+ ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~context ~metasenv ~subst:[] (text,prefix_len,term))
in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status_ref := lexicon_status;
- metasenv,cic
+ metasenv,(*subst,*) cic
;;
(** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
* each invocation will disambiguate the term and can add aliases. Once all
* disambiguations have been performed, the first returned function can be
* used to obtain the resulting aliases *)
-let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
+let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
(fun context metasenv ugraph ->
let lexicon_status = !lexicon_status_ref in
- let (diff, metasenv, cic, ugraph) =
+ let (diff, metasenv, _, cic, ugraph) =
singleton "second"
(GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~context ~metasenv
+ ~context ~metasenv ~subst:[] ?goal
(text,prefix_len,term)) in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status_ref := lexicon_status;
None -> None
| Some wanted ->
let wanted =
- disambiguate_lazy_term text prefix_len lexicon_status_ref wanted
+ disambiguate_lazy_term None text prefix_len lexicon_status_ref wanted
in
Some wanted
in
let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
| `Unfold (Some t) ->
- let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
+ let t =
+ disambiguate_lazy_term None text prefix_len lexicon_status_ref t in
`Unfold (Some t)
| `Normalize
| `Simpl
;;
let rec disambiguate_tactic
- lexicon_status_ref context metasenv (text,prefix_len,tactic)
+ lexicon_status_ref context metasenv goal (text,prefix_len,tactic)
=
+ let disambiguate_term_hint =
+ disambiguate_term goal text prefix_len lexicon_status_ref in
let disambiguate_term =
- disambiguate_term text prefix_len lexicon_status_ref in
+ disambiguate_term None text prefix_len lexicon_status_ref in
let disambiguate_pattern =
disambiguate_pattern text prefix_len lexicon_status_ref in
let disambiguate_reduction_kind =
disambiguate_reduction_kind text prefix_len lexicon_status_ref in
let disambiguate_lazy_term =
- disambiguate_lazy_term text prefix_len lexicon_status_ref in
+ disambiguate_lazy_term None text prefix_len lexicon_status_ref in
let disambiguate_tactic metasenv tac =
- disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tac)
+ disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tac)
in
let disambiguate_auto_params m p =
disambiguate_auto_params disambiguate_term m context p
| GrafiteAst.Apply (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.ApplyRule (loc, term) ->
+ let metasenv,cic = disambiguate_term_hint context metasenv term in
+ metasenv,GrafiteAst.ApplyRule (loc, cic)
| GrafiteAst.ApplyP (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.ApplyP (loc, cic)
| None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
- let (diff, metasenv, cic, _) =
+ let (diff, metasenv, _, cic, _) =
singleton "third"
(GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
~aliases:lexicon_status.LexiconEngine.aliases
| GrafiteAst.Index(loc,key,uri) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =
- disambiguate_term text prefix_len lexicon_status_ref [] in
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
let disambiguate_term_option metasenv =
function
None -> metasenv,None
| GrafiteAst.Coercion (loc,t,b,a,s) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =
- disambiguate_term text prefix_len lexicon_status_ref [] in
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
!lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
| GrafiteAst.Default _
| GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =
- disambiguate_term text prefix_len lexicon_status_ref [] in
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
let disambiguate_term_option metasenv =
function
None -> metasenv,None
let disambiguate_macro
lexicon_status_ref metasenv context (text,prefix_len, macro)
=
- let disambiguate_term = disambiguate_term text prefix_len lexicon_status_ref in
+ let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in
let disambiguate_reduction_kind =
disambiguate_reduction_kind text prefix_len lexicon_status_ref in
match macro with