open Printf
-let debug = ref false
let print ?(depth=0) s =
prerr_endline (String.make depth '\t'^Lazy.force s)
-let debug_print ?(depth=0) s =
- if !debug then print ~depth s else ()
-
-let debug_do f = if !debug then f () else ()
+let noprint ?(depth=0) _ = ()
+let debug_print = noprint
open Continuationals.Stack
open NTacStatus
(* 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 branch status ty =
let status, ty, metas = saturate ~delta:0 status ty in
- debug_print (lazy ("saturated ty :" ^ (ppterm status ty)));
+ noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
let g_metas = metas_of_term status ty in
let clos = menv_closure status g_metas in
(* let _,_,metasenv,_,_ = status#obj in *)
| NCic.Meta(i,_) -> IntSet.add i acc
| _ -> assert false)
IntSet.empty metas
- in IntSet.subset menv clos;;
+ in
+ (* IntSet.subset menv clos *)
+ IntSet.cardinal(IntSet.diff menv clos)
+
+let is_a_fact status ty = branch status ty = 0
let is_a_fact_obj s uri =
let obj = NCicEnvironment.get_checked_obj uri in
;;
(* =============================== 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 build_status (pt, _, metasenv, subst) =
try
- debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
let stamp = Unix.gettimeofday () in
let metasenv, subst, pt, pty =
(* NCicRefiner.typeof status
;;
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
+ print(lazy("prima"));
let ty,metasenv,args =
match gty with
| NCic.Const(nref)
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 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
unit_eq = unit_eq
}
-let only signature _context candidate =
+let only signature _context candidate = true
+(*
(* TASSI: nel trie ci mettiamo solo il body, non il ty *)
let candidate_ty =
NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
~metasenv:[] candidate ^ ": " ^ string_of_int height));
- rc
+ rc *)
;;
let candidate_no = ref 0;;
let openg_no status = List.length (head_goals status#stack)
+let sort_candidates status ctx candidates =
+ let _,_,metasenv,subst,_ = status#obj in
+ let branch cand =
+ let status,ct = disambiguate status ctx ("",0,cand) None in
+ let status,t = term_of_cic_term status ct ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let res = branch status (mk_cic_term ctx ty) in
+ debug_print (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
+ ^ (string_of_int res)));
+ res
+ in
+ let candidates = List.map (fun t -> branch t,t) candidates in
+ let candidates =
+ List.sort (fun (a,_) (b,_) -> a - b) candidates in
+ let candidates = List.map snd candidates in
+ debug_print (lazy ("candidates =\n" ^ (String.concat "\n"
+ (List.map CicNotationPp.pp_term candidates))));
+ candidates
+
let sort_new_elems l =
List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
-let try_candidate ?(smart=0) flags depth status eq_cache t =
+let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
try
debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
let status =
else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
else (* smart = 2: both *)
try NTactics.apply_tac ("",0,t) status
- with Error _ ->
- smart_apply_auto ("",0,t) eq_cache status in
+ with Error _ as exc ->
+ smart_apply_auto ("",0,t) eq_cache status
+ in
+(*
let og_no = openg_no status in
if (* og_no > flags.maxwidth || *)
((depth + 1) = flags.maxdepth && og_no <> 0) then
(debug_print ~depth (lazy "pruned immediately"); None)
- else
- (incr candidate_no;
- Some ((!candidate_no,t),status))
+ else *)
+ (* useless
+ let status, cict = disambiguate status ctx ("",0,t) None in
+ let status,ct = term_of_cic_term status cict ctx in
+ let _,_,metasenv,subst,_ = status#obj in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx ct in
+ let res = branch status (mk_cic_term ctx ty) in
+ if smart=1 && og_no > res then
+ (print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
+ ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
+ print ~depth (lazy "strange application"); None)
+ else *)
+ (incr candidate_no;
+ Some ((!candidate_no,t),status))
with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
;;
-let sort_of metasenv ctx t =
- let ty = NCicTypeChecker.typeof [] metasenv ctx t in
- NCicTypeChecker.typeof [] metasenv ctx ty
+let sort_of subst metasenv ctx t =
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let metasenv',ty = NCicUnification.fix_sorts metasenv subst ty in
+ assert (metasenv = metasenv');
+ NCicTypeChecker.typeof subst metasenv ctx ty
;;
let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
;;
-let perforate_small metasenv context t =
+let perforate_small subst metasenv context t =
let rec aux = function
| NCic.Appl (hd::tl) ->
let map t =
- let s = sort_of metasenv context t in
+ let s = sort_of subst metasenv context t in
match s with
| NCic.Sort(NCic.Type [`Type,u])
when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
let c_ast = function
| NCic.Const r -> Ast.NRef r | _ -> assert false in
let _, raw_gty = term_of_cic_term status gty context in
-(* let raw_gty = NCicUntrusted.apply_subst subst context raw_gty in *)
let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe raw_gty in
+ universe raw_gty in
let local_cands = search_in_th gty cache in
debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
- let together global local =
+ let together global local =
List.map c_ast
(List.filter (only signature context)
(NDiscriminationTree.TermSet.elements global)) @
List.map t_ast (Ncic_termSet.elements local) in
- let candidates = together cands local_cands in
+ let candidates = together cands local_cands in
+ let candidates = sort_candidates status context candidates in
let smart_candidates =
if smart then
match raw_gty with
- | NCic.Appl _ ->
- let weak_gty = perforate_small metasenv context raw_gty in
+ | NCic.Appl _
+ | NCic.Const _
+ | NCic.Rel _ ->
+ let weak_gty = perforate_small subst metasenv context raw_gty in
(*
NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
(List.length tl)) in *)
let more_local_cands = search_in_th cic_weak_gty cache in
let smart_local_cands =
Ncic_termSet.diff more_local_cands local_cands in
- together smart_cands smart_local_cands
+ together smart_cands smart_local_cands
+ (* together more_cands more_local_cands *)
| _ -> []
else []
in
- candidates, smart_candidates
+ let smart_candidates = sort_candidates status context smart_candidates in
+ (* if smart then smart_candidates, []
+ else candidates, [] *)
+ candidates, smart_candidates
;;
let applicative_case depth signature status flags gty (cache:cache) =
then (debug_print (lazy "pruned: not a fact"); elems)
else
match try_candidate (~smart:sm)
- flags depth status cache.unit_eq cand with
+ flags depth status cache.unit_eq context cand with
| None -> elems
| Some x -> x::elems)
[] candidates
then (debug_print (lazy "pruned: not a fact"); elems)
else
match try_candidate (~smart:1)
- flags depth status cache.unit_eq cand with
+ flags depth status cache.unit_eq context cand with
| None -> elems
| Some x -> x::elems)
[] smart_candidates
(* states in l1 have have an empty set of subgoals: no point to sort them *)
debug_print ~depth
(lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
- l1 @ (sort_new_elems (l @ l2)), cache
+ (* l1 @ (sort_new_elems (l @ l2)), cache *)
+ l1 @ (List.rev l2) @ l, cache
;;
let pp_goal = function
status#set_stack gstatus
;;
-let open_goals level status =
- let rec aux level gs =
- if level = 0 then []
- else match gs with
- | [] -> assert false
- | (g, _, _, _) :: s ->
- let is_open = function
- | (_,Continuationals.Stack.Open i) -> Some i
- | (_,Continuationals.Stack.Closed _) -> None
- in
- HExtlib.filter_map is_open g @ aux (level-1) s
- in
- aux level status#stack
+let rec stack_goals level gs =
+ if level = 0 then []
+ else match gs with
+ | [] -> assert false
+ | (g,_,_,_)::s ->
+ let is_open = function
+ | (_,Continuationals.Stack.Open i) -> Some i
+ | (_,Continuationals.Stack.Closed _) -> None
+ in
+ HExtlib.filter_map is_open g @ stack_goals (level-1) s
+;;
+
+let open_goals level status = stack_goals level status#stack
;;
+let move_to_side level status =
+match status#stack with
+ | [] -> assert false
+ | (g,_,_,_)::tl ->
+ let is_open = function
+ | (_,Continuationals.Stack.Open i) -> Some i
+ | (_,Continuationals.Stack.Closed _) -> None
+ in
+ let others = menv_closure status (stack_goals (level-1) tl) in
+ List.for_all (fun i -> IntSet.mem i others)
+ (HExtlib.filter_map is_open g)
+
let rec auto_clusters ?(top=false)
flags signature cache depth status : unit =
debug_print ~depth (lazy ("entering auto clusters at depth " ^
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
List.iter
(fun gl ->
if List.length gl > flags.maxwidth then
- (debug_print (lazy "FAIL GLOBAL WIDTH");
+ (debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
raise (Gaveup IntSet.empty))
else ()) classes;
if List.length classes = 1 then
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
- auto_clusters flags signature (cache:cache) (depth-1) status
+ auto_clusters flags signature cache (depth-1) status
| orig::_ ->
+ 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
(* moved inside auto_clusters *)
if ng > flags.maxwidth then
- (debug_print (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
- else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
+ else if depth = flags.maxdepth then
+ raise (Gaveup IntSet.empty)
else
let status = NTactics.branch_tac ~force:true status in
let status, cache = intros ~depth status cache in
with Gaveup _ ->
debug_print ~depth (lazy "Failed");())
alternatives;
- raise (Gaveup IntSet.empty)
+ raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty)
;;
let int name l def =