-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
- *)
- index_term_and_unfolded_term acc [] term (tyof term))
- cache terms
-;;
-let cache_add_context context 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 ty = CicSubstitution.lift i t in
- let elem = Cic.Rel i in
- index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
- (* index acc key elem, i+1, tail ctx *)
- | Some (_,Cic.Def (_,Some t)) ->
- let ty = CicSubstitution.lift i t in
- let elem = Cic.Rel i in
- index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
- | Some (_,Cic.Def (t,None)) ->
- let ctx = tail ctx in
- let ty =
- CicSubstitution.lift i
- (fst (CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph))
- in
- let elem = Cic.Rel i in
- index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
- | _ -> acc,i+1,tail ctx)
- (cache,1,context) context
- in
- rc
-;;