* http://helm.cs.unibo.it/
*)
+open MatitaTypes
+
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 ~dbd ~(chooseUris: MatitaTypes.choose_uris_callback)
~(chooseInterp: MatitaTypes.choose_interp_callback) ()
=
let disambiguate_term =
~nonvars_button:enable_button_for_non_vars uris
let interactive_interpretation_choice = chooseInterp
- let input_or_locate_uri ~(title:string) =
- (* TODO Zack: I try to avoid using this callback. I therefore assume
- * that the presence of an identifier that can't be resolved via
- * "locate" query is a syntax error *)
- MatitaTypes.not_implemented
- "MatitaDisambiguator: input_or_locate_uri callback"
+ let input_or_locate_uri ~(title:string) ?id =
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+ let msg = match id with Some id -> id | _ -> "" in
+ raise (Unbound_identifier msg)
end
in
let module Disambiguator = Disambiguate.Make (Callbacks) in
method env = _env
method setEnv e = _env <- e
- method disambiguateTermAst ?(context = []) ?(metasenv = []) ?(env = _env)
- termAst
- =
- match disambiguate_term mqiconn context metasenv termAst ~aliases:env with
- | [ x ] -> x
+ method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst =
+ let (save_state, env) =
+ match env with
+ | Some env -> (false, env)
+ | None -> (true, _env)
+ in
+ match disambiguate_term ~dbd 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 =