-
-module type CicDisambiguator =
-sig
- val disambiguate_term :
- ?fresh_instances:bool ->
- context:Cic.context ->
- metasenv:Cic.metasenv ->
- subst:Cic.substitution ->
- ?goal:int ->
- ?initial_ugraph:CicUniv.universe_graph ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.term*
- CicUniv.universe_graph) list *
- bool
-
- val disambiguate_obj :
- ?fresh_instances:bool ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- uri:UriManager.uri option -> (* required only for inductive types *)
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.obj *
- CicUniv.universe_graph) list *
- bool
-end
-
-module Make (C: DisambiguateTypes.Callbacks) =
- struct
- module Disambiguator = Disambiguate.Make(C)
-
- let mk_implicit =
- function true -> Cic.Implicit (Some `Closed)
- | _ -> Cic.Implicit None
- ;;
-
- let disambiguate_term ?(fresh_instances=false) ~context ~metasenv
- ~subst ?goal
- ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
- ~lookup_in_library
- (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 -> k
- | Some i ->
- (fun metasenv t ->
- let _,c,ty = CicUtil.lookup_meta i metasenv in
- assert(c=context);
- Cic.Cast(t,ty)),
- function
- | Disambiguate.Ok (t,m,s,ug) ->
- (match t with
- | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug)
- | _ -> assert false)
- | k -> k
- in
- let localization_tbl = Cic.CicHash.create 503 in
- Disambiguator.disambiguate_thing ~context ~metasenv ~subst
- ~initial_ugraph ~aliases ~mk_implicit
- ~universe ~lookup_in_library
- ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~domain_of_thing:Disambiguate.domain_of_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) ~aliases ~universe ~uri ~lookup_in_library
- (text,prefix_len,obj)
- =
- let obj =
- if fresh_instances then CicNotationUtil.freshen_obj obj else obj
- in
- let hint =
- (fun _ x -> x),
- fun k -> k
- in
- let localization_tbl = Cic.CicHash.create 503 in
- Disambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
- ~aliases ~universe ~uri ~mk_implicit
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
- ~domain_of_thing:Disambiguate.domain_of_obj
- ~lookup_in_library
- ~initial_ugraph:CicUniv.empty_ugraph
- ~interpretate_thing:interpretate_obj
- ~refine_thing:refine_obj
- ~localization_tbl
- ~hint
- (text,prefix_len,obj)
-end
+let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
+ ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
+=
+ let mk_localization_tbl x = Cic.CicHash.create x in
+ MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
+ ~aliases ~universe ~uri ~string_context_of_context
+ ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+ ~domain_of_thing:Disambiguate.domain_of_obj
+ ~lookup_in_library ~mk_implicit ~description_of_alias
+ ~initial_ugraph:CicUniv.empty_ugraph
+ ~interpretate_thing:(interpretate_obj ~mk_choice)
+ ~refine_thing:refine_obj
+ ~mk_localization_tbl
+ ~expty:None
+ ~passes:(MultiPassDisambiguator.passes ())
+ ~freshen_thing:CicNotationUtil.freshen_obj
+ (text,prefix_len,obj)