+let mk_th_cache status gl =
+ List.fold_left
+ (fun (status, acc) g ->
+ let gty = get_goalty status g in
+ let ctx = ctx_of gty in
+ if List.mem_assq ctx acc then status, acc else
+ let idx = InvRelDiscriminationTree.empty in
+ let status,_,idx =
+ List.fold_left (fun (status, i, idx) _ ->
+ let t = mk_cic_term ctx (NCic.Rel i) in
+ let status, ty = typeof status ctx t in
+ let _, ty, _ = saturate status ty in
+ let idx = InvRelDiscriminationTree.index idx ty t in
+ status, i+1, idx)
+ (status, 1, idx) ctx
+ in
+ status, (ctx, idx) :: acc)
+ (status,[]) gl
+;;
+
+let add_to_th t ty c =
+ let key_c = ctx_of t in
+ if not (List.mem_assq key_c c) then
+ (key_c ,InvRelDiscriminationTree.index
+ InvRelDiscriminationTree.empty ty t ) :: c
+ else
+ let rec replace = function
+ | [] -> []
+ | (x, idx) :: tl when x == key_c ->
+ (x, InvRelDiscriminationTree.index idx ty t) :: tl
+ | x :: tl -> x :: replace tl
+ in
+ replace c
+;;
+
+let search_in_th gty th =
+ let c = ctx_of gty in
+ let rec aux acc = function
+ | [] -> Ncic_termSet.elements acc
+ | (_::tl) as k ->
+ try
+ let idx = List.assq k th in
+ let acc = Ncic_termSet.union acc
+ (InvRelDiscriminationTree.retrieve_unifiables idx gty)
+ in
+ aux acc tl
+ with Not_found -> aux acc tl
+ in
+ aux Ncic_termSet.empty c
+;;
+
+let pp_th status =
+ List.iter
+ (fun ctx, idx ->
+ prerr_endline "-----------------------------------------------";
+ prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx);
+ prerr_endline "||====> ";
+ InvRelDiscriminationTree.iter idx
+ (fun k set ->
+ prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k);
+ Ncic_termSet.iter
+ (fun t -> prerr_endline ("\t"^ppterm status t)) set))
+;;