* 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
-(* (proof,ty) list *)
type cache_key = Cic.term
type cache_elem =
| Failed_in of int
| Succeded of Cic.term
| UnderInspection
| Notfound
-type cache = (universe * ((cache_key * cache_elem) list));;
+type cache = (Universe.universe * ((cache_key * cache_elem) list));;
-let cache_empty = (TI.empty,[]);;
-let get_candidates (univ,_) ty =
- S.elements (TI.retrieve_unifiables univ ty)
+let debug = false;;
+let prerr_endline s =
+ if debug then prerr_endline s else ()
;;
-let rec unfold context = function
- | Cic.Prod(name,s,t) ->
- let t' = unfold ((Some (name,Cic.Decl s))::context) t in
- Cic.Prod(name,s,t')
- | t -> ProofEngineReduction.unfold context t
-
+let cache_empty = (Universe.empty,[]);;
-let rec collapse_head_metas = function
- | Cic.Appl(a::l) ->
- let a' = collapse_head_metas a in
- (match a' with
- | Cic.Meta(n,m) -> Cic.Meta(n,m)
- | t ->
- let l' = List.map collapse_head_metas l in
- Cic.Appl(t::l'))
- | t -> t
-;;
-
-let rec head t =
- let rec aux = function
- | Cic.Prod(_,_,t) ->
- CicSubstitution.subst (Cic.Meta (-1,[])) (aux t)
- | t -> t
- in collapse_head_metas (aux t)
+let get_candidates (univ,_) ty =
+(* if Universe.key ty = ty then *)
+ Universe.get_candidates univ ty
+(*
+ else
+ (prerr_endline ("skip: " ^ CicPp.ppterm (Universe.key ty)); [])
+ *)
;;
-let index (univ,oldcache) key term =
- prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
- (TI.index univ key term,oldcache)
+let index (univ,cache) key term =
+ Universe.index univ key term,cache
;;
-let index_term_and_unfolded_term cache context t ty =
- let key = head ty in
- let cache = index cache key t in
- try
- let key = head (unfold context ty) in
- index cache key t
- with ProofEngineTypes.Fail _ -> cache
+let index_term_and_unfolded_term (univ,cache) context t ty =
+ Universe.index_local_term univ context t ty, cache
;;
-let cache_add_list cache context terms_and_types =
- List.fold_left
- (fun acc (term,ty) ->
- index_term_and_unfolded_term acc context term ty)
- cache terms_and_types
+let cache_add_list (univ,cache) context terms_and_types =
+ let univ =
+ List.fold_left
+ (fun univ (t,ty) ->
+ prerr_endline ("indexing: " ^ CicPp.ppterm ty);
+ Universe.index_local_term univ context t ty)
+ univ terms_and_types
+ in
+ univ, cache
let cache_examine (_,oldcache) cache_key =
- try List.assoc cache_key oldcache with Not_found -> Notfound
+ prerr_endline ("examine : " ^ CicPp.ppterm cache_key);
+ try snd (List.find (fun (x,_) -> CicUtil.alpha_equivalence x cache_key)
+ oldcache) with Not_found ->
+ prerr_endline "notfound";
+ Notfound
;;
let cache_replace (univ,oldcache) key v =
let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
univ,oldcache
;;
let cache_add_failure cache cache_key depth =
+ prerr_endline
+ ("CACHE: ADD FAIL " ^ CicPp.ppterm cache_key ^
+ " depth: " ^ string_of_int 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 ->
+ | Succeded t -> cache
+ (*
prerr_endline (CicPp.ppterm t);
- assert false (* if succed it can't fail *)
+ assert false (* if succed it can't fail *) *)
;;
let cache_add_success ((univ,_) as cache) cache_key proof =
- TI.index univ cache_key proof,snd
- (match cache_examine cache cache_key with
+ let u_key = Universe.key cache_key in
+ if u_key <> cache_key then
+ Universe.index univ u_key proof, snd cache
+ else
+ univ,
+ snd
+ (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))
+(*
+ (if Universe.key cache_key = cache_key then
+ Universe.index univ cache_key proof
+ else
+ univ),snd
+ (prerr_endline ("CACHE: ADD SUCCESS" ^ CicPp.ppterm cache_key);
+ 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 ((univ,oldcache) as cache) cache_key depth =
+ prerr_endline ("CACHE: ADD INSPECTING" ^ CicPp.ppterm cache_key);
match cache_examine cache cache_key with
| Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
| Notfound -> univ,(cache_key,UnderInspection)::oldcache
String.concat "\n"
(HExtlib.filter_map
(function
- | (k,Succeded _) -> Some (CicPp.pp k names)
+ | (k,Succeded _) -> Some ("CACHE SUCCESS: " ^ CicPp.pp k names)
| _ -> None)
oldcache)
;;
let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
+ prerr_endline ("CACHE: REMOVE INSPECTING" ^ CicPp.ppterm cache_key);
match cache_examine cache cache_key with
| Notfound
+ | Failed_in _ (* -> assert false *)
| UnderInspection -> cache_remove cache cache_key
- | Failed_in _ -> assert false
- | Succeded _ -> assert false (* it must be a new goal *)
+ | Succeded _ -> cache (*
+ prerr_endline (CicPp.ppterm cache_key);
+ assert false (* it must be a new goal *) *)
;;
let cache_size (_,oldcache) =
List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
let cache_clean (univ,oldcache) =
univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
;;
+let cache_reset_underinspection (u,c) =
+ u,List.filter (function (_,UnderInspection) -> false | _ -> true) c
+;;
projects / helm.git / blobdiff