class parserr () =
object
- method parseTerm (stream: char Stream.t) =
- CicTextualParser2.parse_term stream
-
- (* TODO Zack: implements methods below *)
- method parseTactic (_: char Stream.t) : DisambiguateTypes.tactic =
- MatitaTypes.not_implemented "parserr.parseTactic"
- method parseTactical (_: char Stream.t) : DisambiguateTypes.tactical =
- MatitaTypes.not_implemented "parserr.parseTactical"
- method parseCommand (_: char Stream.t) : DisambiguateTypes.command =
- MatitaTypes.not_implemented "parserr.parseCommand"
- method parseScript (_: char Stream.t) : DisambiguateTypes.script =
- MatitaTypes.not_implemented "parserr.parseScript"
+ method parseTerm = CicTextualParser2.parse_term
+ method parseTactical = CicTextualParser2.parse_tactical
end
class disambiguator
- ~parserr ~mqiconn ~(chooseUris: MatitaTypes.choose_uris_callback)
+ ~parserr ~dbh ~(chooseUris: MatitaTypes.choose_uris_callback)
~(chooseInterp: MatitaTypes.choose_interp_callback) ()
=
let disambiguate_term =
method parserr = parserr
method setParserr p = parserr <- p
- 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 ~dbh context metasenv termAst ~aliases:env with
+ | [ (env, metasenv, term) as x ] ->
+ if save_state then self#setEnv env;
+ x
+ | _ -> assert false
- method disambiguateTerm ~context ~metasenv ?env stream =
- self#disambiguateTermAst ~context ~metasenv ?env
+ method disambiguateTerm ?context ?metasenv ?env stream =
+ self#disambiguateTermAst ?context ?metasenv ?env
(parserr#parseTerm stream)
end