* http://cs.unibo.it/helm/.
*)
-type universe
-val empty_universe:universe
-val get_candidates: universe -> Cic.term -> Cic.term list
-val universe_of_goals:
- HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
- universe -> universe
-val universe_of_context: Cic.context -> Cic.metasenv -> universe -> universe
-val add_to_universe: Cic.term -> Cic.term -> universe -> universe
-
-type cache
-type cache_key = Cic.term
-type cache_elem =
- | Failed_in of int
- | Succeded of Cic.term
- | UnderInspection
- | Notfound
-val cache_examine: cache -> cache_key -> cache_elem
-val cache_add_failure: cache -> cache_key -> int -> cache
-val cache_add_success: cache -> cache_key -> Cic.term -> cache
-val cache_add_underinspection: cache -> cache_key -> int -> cache
-val cache_empty: cache
-val cache_print: Cic.context -> cache -> string
-val cache_size: cache -> int
-val cache_clean: cache -> cache
-
type flags = {
maxwidth: int;
+ maxsize: int;
maxdepth: int;
+ maxgoalsizefactor : int;
timeout: float;
+ use_library: bool;
use_paramod: bool;
use_only_paramod : bool;
+ close_more : bool;
+ dont_cache_failures: bool
}
val default_flags : unit -> flags
(* (metasenv, subst, (metano,depth)list *)
type sort = P | T;;
type and_elem =
- Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list
+ (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list
type auto_result =
| Fail of string
- | Success of Cic.metasenv * Cic.substitution * and_elem list
+ | Success of (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * and_elem list