;;
(* =============================== paramod =========================== *)
-let solve fast status eq_cache goal =
+let solve f status eq_cache goal =
+(*
let f =
if fast then NCicParamod.fast_eq_check
else NCicParamod.paramod in
+*)
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 fast_eq_check eq_cache status goal =
- match solve true status eq_cache goal with
+ match solve NCicParamod.fast_eq_check status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
;;
let paramod eq_cache status goal =
- match solve false status eq_cache goal with
+ match solve NCicParamod.paramod status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
NTactics.distribute_tac (paramod unit_eq) s
;;
+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 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 _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in
let ty,metasenv,args =
match gty with
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
+ noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+ noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
let eq_coerc =
let uri =
NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
let _,_,metasenv,subst,_ = status#obj in
let _,ctx,jty = List.assoc j metasenv in
let jty = NCicUntrusted.apply_subst subst ctx jty in
- debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
+ print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
fast_eq_check unit_eq status j
with
| Error _ as e -> debug_print (lazy "error"); raise e
if depth = 0 then raise (Proved status)
else
let status = NTactics.merge_tac status 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
else if List.length goals < 2 then
auto_main flags signature cache depth status
else
let cache =
let l,tree = cache.under_inspection in
match l with
- | [] -> assert false
+ | [] -> 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
if depth > 0 && move_to_side depth status
then
let status = NTactics.merge_tac status 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
auto_clusters flags signature cache (depth-1) status
else
let ng = List.length goals in