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
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
+ 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 " ^
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
| 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 _ = print (lazy "merged") in
+ let status = NTactics.merge_tac status 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 =
projects / helm.git / commitdiff