- object (self)
- val mutable parserr: parserr = parserr
- method parserr = parserr
- method setParserr p = parserr <- p
-
- val mutable _env = DisambiguateTypes.Environment.empty
- method env = _env
- method setEnv e = _env <- e
-
- 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 disambiguateTerm ?context ?metasenv ?env stream =
- self#disambiguateTermAst ?context ?metasenv ?env
- (parserr#parseTerm stream)
- end
+ let try_pass (fresh_instances, aliases, use_coercions) =
+ CoercDb.use_coercions := use_coercions;
+ f ~fresh_instances ~aliases thing
+ in
+ let set_aliases (instances,(use_multi_aliases,_),_) (_, user_asked as res) =
+ if not use_multi_aliases && not instances then
+ res
+ else if user_asked then
+ res (* one shot aliases *)
+ else
+ set_aliases aliases 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
+
+let set_aliases aliases (choices, user_asked) =
+ (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices),
+ user_asked
+
+let disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph ~aliases term =
+ let f =
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+ in
+ disambiguate_thing ~aliases ~f ~set_aliases term
+
+let disambiguate_obj ~dbd ~aliases ~uri obj =
+ let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+ disambiguate_thing ~aliases ~f ~set_aliases obj