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 None in
- let metasenv, subst =
- NCicUnification.unify status metasenv subst ctx gty pty
-(* the previous code is much less expensive than directly refining
- pt with expected type pty
- in
- NCicRefiner.typeof
- (status#set_coerc_db NCicCoercion.empty_db)
- metasenv subst ctx pt (Some gty) *)
- in
- print (lazy (Printf.sprintf "Refined in %fs"
+ try
+ print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ let stamp = Unix.gettimeofday () in
+ let metasenv, subst, pt, pty =
+ NCicRefiner.typeof
+ (status#set_coerc_db NCicCoercion.empty_db)
+ metasenv subst ctx pt None in
+ print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
+ let metasenv, subst =
+ NCicUnification.unify status metasenv subst ctx gty pty
+ (* the previous code is much less expensive than directly refining
+ pt with expected type pty
+ in
+ prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
+ 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)
+ 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
+ Some (status#set_obj (n,h,metasenv,subst,o))
+ with _ -> prerr_endline "WARNING: refining in fast_eq_check failed"; None
in
- List.map build_status
+ HExtlib.filter_map build_status
(NCicParamod.fast_eq_check status metasenv subst ctx
eq_cache (NCic.Rel ~-1,gty))
;;
let search_in_th gty th =
let c = ctx_of gty in
let rec aux acc = function
- | [] -> Ncic_termSet.elements acc
+ | [] -> (* Ncic_termSet.elements *) acc
| (_::tl) as k ->
try
let idx = List.assq k th in
let sort_new_elems l =
List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
-let try_candidate flags depth status eq_cache t =
+let try_candidate ?(smart=0) flags depth status eq_cache t =
try
- debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
+ print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
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 ||
+ if smart= 0 then NTactics.apply_tac ("",0,t) 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
+ let og_no = openg_no status in
+ if og_no > flags.maxwidth ||
(depth = flags.maxdepth && og_no <> 0) then
- (debug_print ~depth (lazy "pruned immediately"); None)
+ (debug_print ~depth (lazy "pruned immediately"); None)
else
(incr candidate_no;
Some ((!candidate_no,t),status))
with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
;;
-let get_candidates status cache signature gty =
+let get_candidates ?(smart=true) status cache signature gty =
let universe = status#auto_cache in
let context = ctx_of gty in
+ let t_ast t =
+ let _status, t = term_of_cic_term status t context
+ in Ast.NCic t in
+ 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 cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe raw_gty
- in
- let cands =
- List.filter (only signature context)
- (NDiscriminationTree.TermSet.elements cands)
+ universe raw_gty in
+ let local_cands = search_in_th gty cache in
+ 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 smart_candidates =
+ if smart then
+ match raw_gty with
+ | NCic.Appl (hd::tl) ->
+ let weak_gty =
+ NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
+ (List.length tl)) in
+ let more_cands =
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe weak_gty in
+ let smart_cands =
+ NDiscriminationTree.TermSet.diff more_cands cands in
+ let cic_weak_gty = mk_cic_term context weak_gty 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
+ | _ -> []
+ else []
in
- List.map (fun t ->
- let _status, t = term_of_cic_term status t context in Ast.NCic t)
- (search_in_th gty cache)
- @
- List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
+ candidates, smart_candidates
;;
let applicative_case depth signature status flags gty (cache:cache) =
+ app_counter:= !app_counter+1;
let tcache = cache.facts in
- app_counter:= !app_counter+1;
- let candidates = get_candidates status tcache signature gty in
- debug_print ~depth
+ let candidates, smart_candidates =
+ get_candidates status tcache signature gty in
+ print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
+ print ~depth
+ (lazy ("smart candidates: " ^
+ string_of_int (List.length smart_candidates)));
let elems =
List.fold_left
(fun elems cand ->
- match try_candidate flags depth status cache.unit_eq cand with
+ match try_candidate (~smart:2)
+ flags depth status cache.unit_eq cand with
| None -> elems
| Some x -> x::elems)
[] candidates
in
- elems
+ let more_elems =
+ List.fold_left
+ (fun elems cand ->
+ match try_candidate (~smart:1)
+ flags depth status cache.unit_eq cand with
+ | None -> elems
+ | Some x -> x::elems)
+ [] smart_candidates
+ in
+ elems@more_elems
;;
exception Found
status#set_stack gstatus
;;
-let rec auto_clusters
+let rec auto_clusters ?(top=false)
flags signature cache depth status : unit =
debug_print ~depth (lazy "entering auto clusters");
(* ignore(Unix.select [] [] [] 0.01); *)
debug_print ~depth (lazy ("goals = " ^
String.concat "," (List.map string_of_int goals)));
let classes = HExtlib.clusters (deps status) goals in
+ let classes = if top then List.rev classes else classes in
debug_print ~depth
(lazy
(String.concat "\n"
(fun l ->
("cluster:" ^ String.concat "," (List.map string_of_int l)))
classes)));
- let status =
+ let status,b =
List.fold_left
- (fun status gl ->
+ (fun (status,b) gl ->
let status = focus_tac gl status in
try
debug_print ~depth (lazy ("focusing on" ^
String.concat "," (List.map string_of_int gl)));
- auto_main flags signature cache depth status; status
- with Proved(status) -> NTactics.merge_tac status)
- status classes
- in raise (Proved status)
+ auto_main flags signature cache depth status; assert false
+ with
+ | Proved(status) -> (NTactics.merge_tac status,true)
+ | Gaveup _ when top -> (NTactics.merge_tac status,b)
+ )
+ (status,false) classes
+ in if b then raise (Proved status) else raise (Gaveup IntSet.empty)
and
let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
let flags = { flags with maxdepth = x }
in
- try auto_clusters flags signature cache 0 status;assert false
+ try auto_clusters (~top:true) flags signature cache 0 status;assert false
with
| Gaveup _ -> up_to (x+1) y
| Proved s ->
projects / helm.git / commitdiff