X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.mli;h=e8cdbad0e18cff1f9efe869fe2b8482b11aaed7b;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=3fcc4cc3ee7f864180f20c79398ec0bb4b8b9512;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 3fcc4cc3e..e8cdbad0e 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -23,18 +23,40 @@ * http://helm.cs.unibo.it/ *) -(*val eval_ast:*) +exception Drop +exception UnableToInclude of string +exception IncludedFileNotCompiled of string -val eval_string: MatitaTypes.status -> string -> MatitaTypes.status +(* heavy checks slow down the compilation process but give you some interesting + * infos like if the theorem is a duplicate *) +val eval_string: + ?do_heavy_checks:bool -> + ?include_paths:string list -> + ?clean_baseuri:bool -> + MatitaTypes.status ref -> string -> unit -val eval_from_stream: MatitaTypes.status -> char Stream.t -> MatitaTypes.status +val eval_from_stream: + ?do_heavy_checks:bool -> + ?include_paths:string list -> + ?clean_baseuri:bool -> + MatitaTypes.status ref -> Ulexing.lexbuf -> + (MatitaTypes.status -> GrafiteParser.statement -> unit) -> + unit -val eval_ast: - MatitaTypes.status -> (CicAst.term, string) TacticAst.statement -> - MatitaTypes.status +val eval_from_stream_greedy: + ?do_heavy_checks:bool -> + ?include_paths:string list -> + ?clean_baseuri:bool -> + MatitaTypes.status ref-> Ulexing.lexbuf -> + (MatitaTypes.status -> GrafiteParser.statement -> unit) -> + unit -val eval: - MatitaTypes.status -> (Cic.term, string) TacticAst.statement -> +val eval_ast: + ?do_heavy_checks:bool -> + ?include_paths:string list -> + ?clean_baseuri:bool -> + MatitaTypes.status -> + GrafiteParser.statement -> MatitaTypes.status val initial_status: MatitaTypes.status lazy_t