* http://cs.unibo.it/helm/.
*)
-
-module Codomain = struct
- type t = Cic.term
- let compare = Pervasives.compare
-end
-module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
-type universe = TI.t
-
-let empty_universe = TI.empty
-let get_candidates universe ty =
- S.elements (TI.retrieve_unifiables universe ty)
-;;
-let rec head = function
- | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
- | t -> t
-;;
-let index acc key term =
- match key with
- | Cic.Meta _ -> acc
- | _ ->
- prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
- TI.index acc key term
-;;
-let universe_of_goals dbd proof gl universe =
- let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
- let terms = List.map CicUtil.term_of_uri univ in
- let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in
- List.fold_left
- (fun acc term ->
- let key = head (tyof term) in
- index acc key term)
- universe terms
-;;
-let universe_of_context ctx metasenv universe =
- let tail = function [] -> [] | h::tl -> tl in
- let rc,_,_ =
- List.fold_left
- (fun (acc,i,ctx) ctxentry ->
- match ctxentry with
- | Some (_,Cic.Decl t) ->
- let key = CicSubstitution.lift i (head t) in
- let elem = Cic.Rel i in
- index acc key elem, i+1, tail ctx
- | Some (_,Cic.Def (_,Some t)) ->
- let key = CicSubstitution.lift i (head t) in
- let elem = Cic.Rel i in
- index acc key elem, i+1, tail ctx
- | Some (_,Cic.Def (t,None)) ->
- let ctx = tail ctx in
- let key,_ =
- CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
- in
- let elem = Cic.Rel i in
- let key = CicSubstitution.lift i (head key) in
- index acc key elem, i+1, ctx
- | _ -> universe,i+1,tail ctx)
- (universe,1,ctx) ctx
- in
- rc
-;;
-
-(* (proof,ty) list *)
-type cache_key = Cic.term
-type cache_elem =
- | Failed_in of int
- | Succeded of Cic.term
- | UnderInspection
- | Notfound
-type cache = (cache_key * cache_elem) list
-let cache_examine cache cache_key =
- try List.assoc cache_key cache with Not_found -> Notfound
-;;
-let cache_replace cache key v =
- let cache = List.filter (fun (i,_) -> i <> key) cache in
- (key,v)::cache
-;;
-let cache_add_failure cache cache_key depth =
- match cache_examine cache cache_key with
- | Failed_in i when i > depth -> cache
- | Notfound
- | Failed_in _
- | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
- | Succeded t ->
- prerr_endline (CicPp.ppterm t);
- assert false (* if succed it can't fail *)
-;;
-let cache_add_success cache cache_key proof =
- match cache_examine cache cache_key with
- | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
- | UnderInspection -> cache_replace cache cache_key (Succeded proof)
- | Succeded t -> (* we may decide to keep the smallest proof *) cache
- | Notfound -> cache_replace cache cache_key (Succeded proof)
-;;
-let cache_add_underinspection cache cache_key depth =
- match cache_examine cache cache_key with
- | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
- | Notfound -> (cache_key,UnderInspection)::cache
- | Failed_in _
- | UnderInspection
- | Succeded _ -> assert false (* it must be a new goal *)
-;;
-let cache_empty = []
-
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;
+ do_types: bool;
}
-let default_flags = {
- maxwidth = 3;
- maxdepth = 5;
- timeout = 0.;
+let default_flags _ =
+ {maxwidth=3;
+ maxdepth=3;
+ maxsize = 6;
+ maxgoalsizefactor = max_int;
+ timeout=Unix.gettimeofday() +.3.0;
+ use_library=false;
+ use_paramod=true;
+ use_only_paramod=false;
+ close_more=false;
+ dont_cache_failures=false;
+ do_types=false;
}
+;;
(* (metasenv, subst, (metano,depth)list *)
type sort = P | T;;
-type and_elem = Cic.metasenv * Cic.substitution * (int * int * sort) list
+type and_elem = (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * (int * 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