let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc goal metasenv in
let gty = NCicUntrusted.apply_subst subst ctx gty in
let build_status (pt, _, metasenv, subst) =
try
let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc goal metasenv in
let gty = NCicUntrusted.apply_subst subst ctx gty in
let build_status (pt, _, metasenv, subst) =
try
let stamp = Unix.gettimeofday () in
let metasenv, subst, pt, pty =
(* NCicRefiner.typeof status
let stamp = Unix.gettimeofday () in
let metasenv, subst, pt, pty =
(* NCicRefiner.typeof status
+let demod eq_cache status goal =
+ match solve NCicParamod.demod status eq_cache goal with
+ | [] -> raise (Error (lazy "no progress",None))
+ | s::_ -> s
+;;
+
+let demod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (demod unit_eq) s
+;;
+
(*
let fast_eq_check_tac_all ~params eq_cache status =
let g,_,_ = current_goal status in
(*
let fast_eq_check_tac_all ~params eq_cache status =
let g,_,_ = current_goal status in
(* let ggty = mk_cic_term context gty in *)
let status, t = disambiguate status ctx t None in
let status,t = term_of_cic_term status t ctx in
(* let ggty = mk_cic_term context gty in *)
let status, t = disambiguate status ctx t None in
let status,t = term_of_cic_term status t ctx in
NCicMetaSubst.saturate metasenv subst ctx ty 0 in
let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
let status = status#set_obj (n,h,metasenv,subst,o) in
NCicMetaSubst.saturate metasenv subst ctx ty 0 in
let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
let status = status#set_obj (n,h,metasenv,subst,o) in
- let pterm = if args=[] then t else NCic.Appl(t::args) in
- debug_print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
- debug_print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
+ let pterm = if args=[] then t else
+ match t with
+ | NCic.Appl l -> NCic.Appl(l@args)
+ | _ -> NCic.Appl(t::args)
+ in
+ print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+ print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
let _,_,metasenv,subst,_ = status#obj in
let _,ctx,jty = List.assoc j metasenv in
let jty = NCicUntrusted.apply_subst subst ctx jty in
let _,_,metasenv,subst,_ = status#obj in
let _,ctx,jty = List.assoc j metasenv in
let jty = NCicUntrusted.apply_subst subst ctx jty in
- auto_clusters flags signature (cache:cache) (depth-1) status
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache *)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
+ auto_clusters flags signature cache (depth-1) status
| a::tl -> let tree = rm_from_th a tree a in
{cache with under_inspection = tl,tree}
in
| a::tl -> let tree = rm_from_th a tree a in
{cache with under_inspection = tl,tree}
in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache*)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in