open Printf
-let debug = ref true
+let debug = ref false
let debug_print ?(depth=0) s =
if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
-(* let print= debug_print *)
- let print ?(depth=0) s =
+(* let print = debug_print *)
+let print ?(depth=0) s =
prerr_endline (String.make depth '\t'^Lazy.force s)
let debug_do f = if !debug then f () else ()
in closure IntSet.empty gl
;;
-(* we call a "fact" an object whose hypothesis occurs in the goal
+(* we call a "fact" an object whose hypothesis occur in the goal
or in types of goal-variables *)
let is_a_fact status ty =
let status, ty, _ = saturate ~delta:max_int status ty in
open_goal, ctx, gty
-
(* =============================== paramod =========================== *)
let auto_paramod ~params:(l,_) status goal =
let gty = get_goalty status goal in
NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
with
| [] -> raise (Error (lazy "no proof found",None))
- | (pt, metasenv, subst)::_ ->
+ | (pt, _, metasenv, subst)::_ ->
let status = status#set_obj (n,h,metasenv,subst,o) in
instantiate status goal (mk_cic_term (ctx_of gty) pt)
;;
;;
let fast_eq_check_all status eq_cache goal =
- let gty = get_goalty status goal in
- let ctx = ctx_of gty in
let n,h,metasenv,subst,o = status#obj in
- let status,t = term_of_cic_term status gty ctx in
- let build_status (pt, metasenv, subst) =
- let status = status#set_obj (n,h,metasenv,subst,o) in
- let gty = get_goalty status goal in
- instantiate status goal (mk_cic_term ctx pt)
+ let gname, ctx, gty = List.assoc goal metasenv in
+ let gty = NCicUntrusted.apply_subst subst ctx gty in
+ let build_status (pt, _, metasenv, subst) =
+ (* let stamp = Unix.gettimeofday () in *)
+ let metasenv, subst, pt, pty =
+ NCicRefiner.typeof
+ (status#set_coerc_db NCicCoercion.empty_db)
+ metasenv subst ctx pt (Some gty)
+ in
+(* print (lazy (Printf.sprintf "Refined in %fs"
+ (Unix.gettimeofday() -. stamp))); *)
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
+ let subst = (goal,(gname,ctx,pt,pty)) :: subst in
+ status#set_obj (n,h,metasenv,subst,o)
in
List.map build_status
(NCicParamod.fast_eq_check status metasenv subst ctx
- eq_cache (NCic.Rel ~-1,t))
+ eq_cache (NCic.Rel ~-1,gty))
;;
let fast_eq_check eq_cache status goal =
| s::_ -> s
;;
-let fast_eq_check_tac ~params s =
- NTactics.distribute_tac (fast_eq_check s#eq_cache) s
+let dist_fast_eq_check eq_cache s =
+ NTactics.distribute_tac (fast_eq_check eq_cache) s
;;
let auto_eq_check eq_cache status =
try
- let s =
- NTactics.distribute_tac (fast_eq_check eq_cache) status in
+ let s = dist_fast_eq_check eq_cache status in
[s]
with
| Error _ -> []
;;
+(* warning: ctx is supposed to be already instantiated w.r.t subst *)
+let index_local_equations eq_cache status =
+ let open_goals = head_goals status#stack in
+ let open_goal = List.hd open_goals in
+ let ngty = get_goalty status open_goal in
+ let ctx = ctx_of ngty in
+ let c = ref 0 in
+ List.fold_left
+ (fun eq_cache _ ->
+ c:= !c+1;
+ let t = NCic.Rel !c in
+ try
+ let ty = NCicTypeChecker.typeof [] [] ctx t in
+ debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+ NCicParamod.forward_infer_step eq_cache t ty
+ with
+ | NCicTypeChecker.TypeCheckerFailure _
+ | NCicTypeChecker.AssertFailure _ -> eq_cache)
+ eq_cache ctx
+;;
+
+let fast_eq_check_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ dist_fast_eq_check unit_eq s
+;;
+
(*
let fast_eq_check_tac_all ~params eq_cache status =
let g,_,_ = current_goal status in
;;
*)
+(****************** smart application ********************)
+
+
+let smart_apply t unit_eq status g =
+ let n,h,metasenv,subst,o = status#obj in
+ let gname, ctx, gty = List.assoc g metasenv 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 ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let ty,metasenv,args = 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
+ let eq_coerc =
+ let uri =
+ NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
+ NCic.Const ref
+ in
+ let smart =
+ NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
+ let smart = mk_cic_term ctx smart in
+ try
+ let status = instantiate status g smart 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)));
+ fast_eq_check unit_eq status j
+ with
+ | Error _ as e -> debug_print (lazy "error"); raise e
+
+let smart_apply_tac t s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (smart_apply t unit_eq) s
+
+let smart_apply_auto t eq_cache =
+ NTactics.distribute_tac (smart_apply t eq_cache)
+
+
(****************** types **************)
exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
atoms of the input goals *)
-exception Proved of #NTacStatus.tac_status
+exception Proved of NTacStatus.tac_status
(* let close_failures _ c = c;; *)
(* let prunable _ _ _ = false;; *)
let sort_new_elems l =
List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
-let try_candidate flags depth status t =
+let try_candidate flags depth status eq_cache t =
try
debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
- let status = NTactics.apply_tac ("",0,t) status in
+ let status =
+ smart_apply_auto ("",0,t) eq_cache status in
+ (* let status = NTactics.apply_tac ("",0,t) status in *)
let og_no = openg_no status in
if og_no > flags.maxwidth ||
(depth = flags.maxdepth && og_no <> 0) then
let elems =
List.fold_left
(fun elems cand ->
- match try_candidate flags depth status cand with
+ match try_candidate flags depth status cache.unit_eq cand with
| None -> elems
| Some x -> x::elems)
[] candidates
with Found -> debug_print ~depth (lazy "success");true)
;;
-(* warning: ctx is supposed to be already instantiated w.r.t subst *)
-let index_local_equations eq_cache status =
- let open_goals = head_goals status#stack in
- assert (List.length open_goals = 1);
- let open_goal = List.hd open_goals in
- let ngty = get_goalty status open_goal in
- let ctx = ctx_of ngty in
- let c = ref 0 in
- List.fold_left
- (fun eq_cache _ ->
- c:= !c+1;
- let t = NCic.Rel !c in
- try
- let ty = NCicTypeChecker.typeof [] [] ctx t in
- prerr_endline ("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty));
- NCicParamod.forward_infer_step eq_cache t ty
- with
- | NCicTypeChecker.TypeCheckerFailure _
- | NCicTypeChecker.AssertFailure _ -> eq_cache)
- eq_cache ctx
-;;
-
let rec guess_name name ctx =
if name = "_" then guess_name "auto" ctx else
if not (List.mem_assoc name ctx) then name else
let rec intros ~depth status (cache:cache) =
match is_prod status with
| Some _ ->
- prerr_endline "is prod";
let status,facts =
intros_facts ~depth status cache.facts
in
incr candidate_no;
((!candidate_no,Ast.Ident("__paramod",None)),s))
(auto_eq_check cache.unit_eq status)
- (* states in l2 have have an set of subgoals: no point to sort them *)
in
+ (* states in l2 have have an set of subgoals: no point to sort them *)
l2 @ (sort_new_elems (l@l1)), cache
;;
and
-(* let rec auto_main flags signature cache status k depth = *)
+(* the goals returned upon failure are an unsatisfiable subset
+ of the initial head goals in the stack *)
auto_main flags signature (cache:cache) depth status: unit =
debug_print ~depth (lazy "entering auto main");
let goals = head_goals status#stack in
match goals with
| [] -> raise (Proved status)
- | _ ->
+ | orig::_ ->
let branch = List.length(goals)>1 in
if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
else
unsat)
IntSet.empty alternatives
in
- raise (Gaveup IntSet.add g unsat)
+ raise (Gaveup IntSet.add orig unsat)
;;
let int name l def =
;;
let auto_tac ~params:(_univ,flags) status =
+ let oldstatus = status in
+ let status = (status:> NTacStatus.tac_status) in
let goals = head_goals status#stack in
let status, facts = mk_th_cache status goals in
let unit_eq = index_local_equations status#eq_cache status in
| (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
| _ -> assert false
in
- s#set_stack stack
+ let s = s#set_stack stack in
+ oldstatus#set_status s
in
let s = up_to depth depth in
print(lazy
projects / helm.git / blobdiff