let get_candidates (univ,_) ty =
S.elements (TI.retrieve_unifiables univ ty)
;;
-let rec head = function
- | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
+
+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 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 index ((univ,oldcache) as cache) key term =
- match key with
- | Cic.Meta _ -> cache
- | _ ->
- prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
- (TI.index univ key term,oldcache)
+
+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 cache_add_library dbd proof gl cache =
- 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)
- cache terms
+
+let index (univ,oldcache) key term =
+ prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
+ (TI.index univ key term,oldcache)
;;
-let cache_add_context ctx metasenv cache =
- 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
- | _ -> acc,i+1,tail ctx)
- (cache,1,ctx) ctx
- in
- rc
+
+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 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_examine (_,oldcache) cache_key =
try List.assoc cache_key oldcache with Not_found -> Notfound
;;