- method disambiguateTermAst
- ~context ~metasenv ?(env = DisambiguateTypes.Environment.empty) termAst
- =
- disambiguate_term mqiconn context metasenv termAst ~aliases:env
+ 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 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)