- object (self)
- val mutable _env = DisambiguateTypes.Environment.empty
- method env = _env
- method setEnv e = _env <- e
-
- method chooseUris = !_chooseUris
- method setChooseUris f = _chooseUris := f
-
- method chooseInterp = !_chooseInterp
- method setChooseInterp f = _chooseInterp := f
-
- val parserr = parserr_instance ()
- method parserr = parserr
-
- val dbd = MatitaMisc.dbd_instance ()
-
- method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst =
- let (save_state, env) =
- match env with
- | Some env -> (false, env)
- | None -> (true, _env)
- in
- match disambiguate_term ~initial_ugraph:CicUniv.empty_ugraph
- ~dbd context metasenv termAst ~aliases:env with
- | [ (env, metasenv, term,ugraph) as x ] ->
- if save_state then self#setEnv env;
- x
- | _ -> assert false
-
- method disambiguateTermAsts ?(metasenv = []) ?env asts =
- let ast = CicAst.pack asts in
- let (env, metasenv, term, ugraph) =
- self#disambiguateTermAst ~context:[] ~metasenv ?env ast
- in
- (env, metasenv, CicUtil.unpack term, ugraph)
-
- method disambiguateTerm ?context ?metasenv ?env stream =
- self#disambiguateTermAst ?context ?metasenv ?env
- (parserr#parseTerm stream)
- end
+ let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
+ CoercDb.use_coercions := use_coercions;
+ f ~fresh_instances ~aliases ~universe thing
+ in
+ let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+ if use_mono_aliases && not instances then
+ drop_aliases res
+ else if user_asked then
+ drop_aliases res (* one shot aliases *)
+ else
+ drop_aliases_and_clear_diff res
+ in
+ let rec aux =
+ function
+ | [ pass ] -> set_aliases pass (try_pass pass)
+ | hd :: tl ->
+ (try
+ set_aliases hd (try_pass hd)
+ with Disambiguate.NoWellTypedInterpretation -> aux tl)
+ | [] -> assert false
+ in
+ let saved_use_coercions = !CoercDb.use_coercions in
+ try
+ let res = aux passes in
+ CoercDb.use_coercions := saved_use_coercions;
+ res
+ with exn ->
+ CoercDb.use_coercions := saved_use_coercions;
+ raise exn
+
+type disambiguator_thing =
+ { do_it :
+ 'a 'b.
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ f:(?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b * bool) ->
+ drop_aliases:('b * bool -> 'b * bool) ->
+ drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
+ }