context:'context ->
metasenv:'metasenv ->
initial_ugraph:'ugraph ->
+ hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
+ (('refined_thing,'metasenv) test_result -> 'ugraph ->
+ ('refined_thing,'metasenv) test_result * 'ugraph) ->
aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
universe:DisambiguateTypes.codomain_item list
DisambiguateTypes.Environment.t option ->
((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
list * 'metasenv * 'refined_thing * 'ugraph)
list * bool
+
val disambiguate_term :
?fresh_instances:bool ->
dbd:HSql.dbd ->
context:Cic.context ->
- metasenv:Cic.metasenv ->
+ metasenv:Cic.metasenv -> ?goal:int ->
?initial_ugraph:CicUniv.universe_graph ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing ~dbd ~context ~metasenv
- ~initial_ugraph ~aliases ~universe
+ ~initial_ugraph ~hint
+ ~aliases ~universe
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~localization_tbl
(thing_txt,thing_txt_prefix_len,thing)
interpretate_thing ~context ~env:filled_env
~uri ~is_path:false thing ~localization_tbl
in
+ let cic_thing = (fst hint) metasenv cic_thing in
let foo () =
let k,ugraph1 =
refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
in
+ let k, ugraph1 = (snd hint) k ugraph1 in
(k , ugraph1 )
in refine_profiler.HExtlib.profile foo ()
with
CicEnvironment.CircularDependency s ->
failwith "Disambiguate: circular dependency"
- let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
+ let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
+ ?goal
?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
(text,prefix_len,term)
=
let term =
if fresh_instances then CicNotationUtil.freshen_term term else term
in
+ let hint = match goal with
+ | None -> (fun _ x -> x), fun k u -> k, u
+ | Some i ->
+ (fun metasenv t ->
+ let _,c,ty = CicUtil.lookup_meta i metasenv in
+ assert(c=context);
+ Cic.Cast(t,ty)),
+ function
+ | Ok (t,m) -> fun ug ->
+ (match t with
+ | Cic.Cast(t,_) -> Ok (t,m), ug
+ | _ -> assert false)
+ | k -> fun ug -> k, ug
+ in
let localization_tbl = Cic.CicHash.create 503 in
disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
~refine_thing:refine_term (text,prefix_len,term)
~localization_tbl
+ ~hint
let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
(text,prefix_len,obj)
let obj =
if fresh_instances then CicNotationUtil.freshen_obj obj else obj
in
+ let hint =
+ (fun _ x -> x),
+ fun k u -> k, u
+ in
let localization_tbl = Cic.CicHash.create 503 in
- disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
+ disambiguate_thing ~dbd ~context:[] ~metasenv:[]
+ ~aliases ~universe ~uri
~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
~initial_ugraph:CicUniv.empty_ugraph
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
~localization_tbl
+ ~hint
(text,prefix_len,obj)
end