;;
(** @param term not meaningful when context is given *)
-let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
+let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
term =
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, subst, cic, _) =
singleton "first"
(CicDisambiguate.disambiguate_term
~aliases:lexicon_status.LexiconEngine.aliases
- ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~lookup_in_library
~mk_choice:cic_mk_choice
~mk_implicit
metasenv,(*subst,*) cic
;;
+let disambiguate_nterm expty lexicon_status context metasenv subst thing
+=
+ let diff, metasenv, subst, cic =
+ singleton "first"
+ (NCicDisambiguate.disambiguate_term
+ ~coercion_db:(NCicCoercion.db ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~expty
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~lookup_in_library
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~context ~metasenv ~subst thing)
+ in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ metasenv, subst, lexicon_status, cic
+;;
+
+
(** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
* rationale: lazy_term will be invoked in different context to obtain a 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 goal text prefix_len lexicon_status_ref term =
+let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
(fun context metasenv ugraph ->
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, _, cic, ugraph) =
~description_of_alias:LexiconAst.description_of_alias
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~context ~metasenv ~subst:[] ?goal
- (text,prefix_len,term)) in
+ ~context ~metasenv ~subst:[]
+ (text,prefix_len,term) ~expty) in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status_ref := lexicon_status;
cic, metasenv, ugraph)
(wanted, hyp_paths, goal_path)
;;
+type pattern =
+ CicNotationPt.term Disambiguate.disambiguator_input option *
+ (string * NCic.term) list * NCic.term option
+
+let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+ let interp path = NCicDisambiguate.disambiguate_path path in
+ let goal_path = HExtlib.map_option interp goal_path in
+ let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+ let wanted =
+ match wanted with None -> None | Some x -> Some (text,prefix_len,x)
+ in
+ (wanted, hyp_paths, goal_path)
+;;
+
let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
| `Unfold (Some t) ->
let t =
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 _,_,expty =
+ List.find (fun (x,_,_) -> Some x = goal) metasenv
+ in
+ disambiguate_term (Some expty) text prefix_len lexicon_status_ref in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref in
let disambiguate_pattern =
in
UriManager.uri_of_string (baseuri ^ "/" ^ name)
in
- let try_new cic =
+ let _try_new cic =
(NCicLibrary.clear_cache ();
NCicEnvironment.invalidate ();
OCic2NCic.clear ();
let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
match cmd with
+ | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj)
| GrafiteAst.Index(loc,key,uri) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =