+let pump cache steps =
+ let active, passive, bag = cache.tables in
+ let active, passive, bag =
+ Saturation.pump_actives
+ [] bag active passive steps infinity
+ in
+ let tables = active, passive, bag in
+ { cache with tables = tables }
+;;
+
+let add_term_to_active cache metasenv subst context t ty_opt =
+ let actives, passives, bag = cache.tables in
+ let bag, metasenv, head, t, args, mes, ugraph =
+ match ty_opt with
+ | Some ty ->
+ bag, metasenv, ty, t, [], (CicUtil.metas_of_term (Cic.Appl [t;ty])),
+ CicUniv.oblivion_ugraph
+ | None ->
+ let ty, ugraph =
+ CicTypeChecker.type_of_aux'
+ ~subst metasenv context t CicUniv.oblivion_ugraph
+ in
+ let bag, head, metasenv, args =
+ Equality.saturate_term bag metasenv subst context ty
+ in
+ let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
+ let t = if args = [] then t else Cic.Appl (t:: args) in
+ bag, metasenv, head, t, args, mes, ugraph
+ in
+ if List.exists
+ (function
+ | Cic.Meta(i,_) ->
+ (try
+ let _,mc, mt = CicUtil.lookup_meta i metasenv in
+ let sort, u =
+ CicTypeChecker.type_of_aux' metasenv mc mt ugraph
+ in
+ fst (CicReduction.are_convertible mc sort (Cic.Sort Cic.Prop) u)
+ with
+ | CicUtil.Meta_not_found _ -> false)
+ | _ -> assert false)
+ args
+ then
+ cache
+ else
+ let env = metasenv, context, CicUniv.oblivion_ugraph in
+ let newmetas =
+ List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv
+ in
+ let tables =
+ Saturation.add_to_active bag actives passives env head t newmetas
+ in
+ { cache with tables = tables }
+;;
+
+let pp_cache cache =
+ prerr_endline "Automation cache";
+ prerr_endline "----------------------------------------------";
+ prerr_endline "universe:";
+ Universe.iter cache.univ (fun _ ts ->
+ prerr_endline (" "^
+ String.concat "\n " (List.map CicPp.ppterm ts)));
+ prerr_endline "tables/actives:";
+ let active, passive, _ = cache.tables in
+ List.iter
+ (fun e -> prerr_endline (" " ^ Equality.string_of_equality e))
+ (Saturation.list_of_active active);
+ prerr_endline "tables/passives:";
+ List.iter
+ (fun e -> prerr_endline (" " ^ Equality.string_of_equality e))
+ (Saturation.list_of_passive passive);
+ prerr_endline "----------------------------------------------";
+;;