open Printf
-let debug = false
+let debug = true
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
open Continuationals.Stack
match
NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
with
- | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+ | [] -> raise (Error (lazy "no proof found",None))
| (pt, metasenv, subst)::_ ->
let status = status#set_obj (n,h,metasenv,subst,o) in
- instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+ instantiate status goal (mk_cic_term (ctx_of gty) pt)
;;
let auto_paramod_tac ~params status =
;;
*)
-module CacheElem : Set.OrderedType =
- struct
- type t =
- | Failed_in of int * NCic.term (* depth, goal type *)
- | Succeded of Cic.term * Cic.term (* proof, proof type *)
- | UnderInspection of Cic.term (* avoid looping *)
- let compare = Pervasives.compare
- end
+type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
-module CacheSet = Set.Make(CacheElem)
-module Cache =
- Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CacheSet)
+let mk_th_cache status gl =
+ List.fold_left
+ (fun (status, acc) g ->
+ let gty = get_goalty status g in
+ let ctx = ctx_of gty in
+ if List.mem_assq ctx acc then status, acc else
+ let idx = InvRelDiscriminationTree.empty in
+ let status,_,idx =
+ List.fold_left (fun (status, i, idx) _ ->
+ let t = mk_cic_term ctx (NCic.Rel i) in
+ let status, ty = typeof status ctx t in
+ let _, ty, _ = saturate status ty in
+ let idx = InvRelDiscriminationTree.index idx ty t in
+ status, i+1, idx)
+ (status, 1, idx) ctx
+ in
+ status, (ctx, idx) :: acc)
+ (status,[]) gl
+;;
+
+let add_to_th t ty c =
+ let key_c = ctx_of t in
+ if not (List.mem_assq key_c c) then
+ (key_c ,InvRelDiscriminationTree.index
+ InvRelDiscriminationTree.empty ty t ) :: c
+ else
+ let rec replace = function
+ | [] -> []
+ | (x, idx) :: tl when x == key_c ->
+ (x, InvRelDiscriminationTree.index idx ty t) :: tl
+ | x :: tl -> x :: replace tl
+ in
+ replace c
+;;
+
+let search_in_th gty th =
+ let c = ctx_of gty in
+ let rec aux acc = function
+ | [] -> Ncic_termSet.elements acc
+ | (_::tl) as k ->
+ try
+ let idx = List.assq k th in
+ let acc = Ncic_termSet.union acc
+ (InvRelDiscriminationTree.retrieve_unifiables idx gty)
+ in
+ aux acc tl
+ with Not_found -> aux acc tl
+ in
+ aux Ncic_termSet.empty c
+;;
+
+let pp_th status =
+ List.iter
+ (fun ctx, idx ->
+ prerr_endline "-----------------------------------------------";
+ prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx);
+ prerr_endline "||====> ";
+ InvRelDiscriminationTree.iter idx
+ (fun k set ->
+ prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k);
+ Ncic_termSet.iter
+ (fun t -> prerr_endline ("\t"^ppterm status t)) set))
+;;
type cache_examination_result =
[ `Failed_in of int
]
type sort = T | P
-type goal = int * int * sort
-type fail = goal * NCic.term
-type candidate = NCic.term
-type menv = NCic.metasenv
-type subst = NCic.substitution
+type goal = int * int * sort (* goal, depth, sort *)
+type fail = goal * cic_term
+type candidate = int * Ast.term (* unique candidate number, candidate *)
type op =
(* goal has to be proved *)
| D of goal
(* goal has to be cached as a success obtained using candidate as the first
* step *)
- | S of goal * Cache.input * candidate (* int was minsize *)
-type elem =
+ | S of goal * cic_term * candidate (* int was minsize *)
+type 'a elem =
(* menv, subst, size, operations done (only S), operations to do,
* failures to cache if any op fails *)
- menv * subst * int * op list * op list * fail list
+ (#tac_status as 'a) * int * op list * op list * fail list
-type auto_status =
+type 'a auto_status =
(* list of computations that may lead to the solution: all op list will
* end with the same (S(g,_)) *)
- elem list * Cache.t
+ 'a elem list * th_cache
-type auto_result =
+type 'a auto_result =
| Gaveup
- | Proved of menv * subst * auto_status (* the alternative proofs *)
+ | Proved of (#tac_status as 'a) * 'a auto_status (* alt. proofs *)
type flags = {
do_types : bool; (* solve goals in Type *)
timeout : float;
}
-let close_failures = assert false;;
-let equational_and_applicative_case = assert false;;
-let prunable = assert false;;
-let cache_examine = assert false;;
-let put_in_subst = assert false;;
-let calculate_goal_ty = assert false;;
-let add_to_cache_and_del_from_orlist_if_green_cut = assert false;;
-let cache_add_underinspection = assert false;;
+let close_failures _ c = c;;
+let prunable _ _ _ = false;;
+let cache_examine cache gty = `Notfound;;
+let put_in_subst s _ _ _ = s;;
+let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;;
+let cache_add_underinspection c _ _ = c;;
+let equational_case _ _ _ _ _ _ = [];;
+let sort_new_elems l = l;;
+let only _ _ _ = true;;
+
+let candidate_no = ref 0;;
+
+let try_candidate status t g =
+ try
+ debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
+ let status = NTactics.focus_tac [g] status in
+ let status = NTactics.apply_tac ("",0,t) status in
+ let open_goals = head_goals status#stack in
+ debug_print
+ (lazy (" success: "^String.concat " "(List.map string_of_int open_goals)));
+ incr candidate_no;
+ Some ((!candidate_no,t),status,open_goals)
+ with Error (msg,exn) -> debug_print (lazy " failed"); None
+;;
+
+let rec mk_irl n = function
+ | [] -> []
+ | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
+;;
+let get_candidates status cache_th signature gty =
+ let universe = status#auto_cache in
+ let context = ctx_of gty 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)
+ in
+ List.map (fun t ->
+ let _status, t = term_of_cic_term status t context in Ast.NCic t)
+ (search_in_th gty cache_th)
+ @
+ List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
+;;
+
+let applicative_case signature status flags g gty cache =
+ let candidates = get_candidates status cache signature gty in
+ debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
+ let elems =
+ List.fold_left
+ (fun elems cand ->
+ match try_candidate status cand g with
+ | None -> elems
+ | Some x -> x::elems)
+ [] candidates
+ in
+ elems
+;;
+
+let equational_and_applicative_case
+ signature flags status g depth gty cache
+=
+ let elems =
+ if false (*is_equational_case gty flags*) then
+ let elems =
+ equational_case
+ signature status flags g gty cache
+ in
+ let more_elems =
+ applicative_case
+ signature status flags g gty cache
+ in
+ elems@more_elems
+ else
+ let elems =
+ (*match LibraryObjects.eq_URI () with
+ | Some _ ->
+ smart_applicative_case dbd tables depth s fake_proof goalno
+ gty m context signature universe cache flags
+ | None -> *)
+ applicative_case
+ signature status flags g gty cache
+ in
+ elems
+ in
+ let elems =
+ (* XXX calculate the sort *)
+ List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems
+ in
+ let elems = sort_new_elems elems in
+ elems, cache
+;;
+
+let calculate_goal_ty (goalno,_,_) status =
+ try Some (get_goalty status goalno)
+ with Error _ -> None
+;;
let d_goals l =
let rec aux acc = function
| (D g)::tl -> aux (acc@[g]) tl
aux fl
;;
-let auto_main status context flags signature elems cache =
- let rec aux (elems, cache : auto_status) =
+let rec guess_name name ctx =
+ if name = "_" then guess_name "auto" ctx else
+ if not (List.mem_assoc name ctx) then name else
+ guess_name (name^"'") ctx
+;;
+
+let intro_case status gno gty depth cache name =
+ let status = NTactics.focus_tac [gno] status in
+ let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals = 1);
+ let open_goal = List.hd open_goals in
+ let status, cache =
+ let ngty = get_goalty status open_goal in
+ let ctx = ctx_of ngty in
+ let t = mk_cic_term ctx (NCic.Rel 1) in
+ let status, ty = typeof status ctx t in
+ let _status, ty, _args = saturate status ty in
+ status, add_to_th t ty cache
+ in
+ debug_print (lazy (" intro: "^ string_of_int open_goal));
+(* pp_th status cache; *)
+ incr candidate_no;
+ (* XXX calculate the sort *)
+ [(!candidate_no,Ast.Implicit `JustOne),status,[open_goal,depth,P]],
+ cache
+;;
+
+let do_something signature flags s gno depth gty cache =
+ let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in
+ match raw_gty with
+ | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name
+ | _ ->
+ equational_and_applicative_case signature flags s gno depth gty cache
+;;
+
+let auto_main flags signature elems cache =
+ let rec aux (elems, cache : 'a auto_status) =
(* processa le hint dell'utente *)
(* let cache, elems = filter_prune_hint cache elems in *)
match elems with
aux tables flags cache elems)
*)
| [] ->
- (* complete failure *)
debug_print (lazy "gave up");
Gaveup
- | (m, s, _, _, [],_)::orlist ->
- (* complete success *)
+ | (s, _, _, [],_)::orlist ->
debug_print (lazy "success");
- Proved (m, s, (orlist, cache))
- | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
+ Proved (s, (orlist, cache))
+ | (s, size, don, (D (_,_,T))::todo, fl)::orlist
when not flags.do_types ->
- (* skip since not Prop, don't even check if closed by side-effect *)
debug_print (lazy "skip goal in Type");
- aux ((m, s, size, don, todo, fl)::orlist, cache)
- | (m, s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
- (* partial success, cache g and go on *)
+ aux ((s, size, don, todo, fl)::orlist, cache)
+ | (s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
let cache, orlist, fl, sibling_pruned =
add_to_cache_and_del_from_orlist_if_green_cut
- g s m cache key todo orlist fl context size
+ g s cache key todo orlist fl size
in
let fl = remove_s_from_fl g fl in
let don = if sibling_pruned then don else op::don in
- aux ((m, s, size, don, todo, fl)::orlist, cache)
- | (m, s, size, don, todo, fl)::orlist
+ let s = NTactics.unfocus_tac s in
+ aux ((s, size, don, todo, fl)::orlist, cache)
+ | (s, size, don, todo, fl)::orlist
when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
debug_print (lazy ("FAIL: WIDTH"));
aux (orlist, cache)
- | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
+ | (s, size, don, todo, fl)::orlist when size > flags.maxsize ->
debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^
" > " ^ string_of_int flags.maxsize ));
aux (orlist, cache)
| _ when Unix.gettimeofday () > flags.timeout ->
debug_print (lazy ("FAIL: TIMEOUT"));
Gaveup
- | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
+ | (s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist ->
debug_print (lazy "attack goal");
- match calculate_goal_ty g s m with
+ match calculate_goal_ty g s with
| None ->
debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
- aux ((m,s,size,don,todo, fl)::orlist, cache)
- | Some (canonical_ctx, gty) ->
- debug_print (lazy ("EXAMINE: "^
- NCicPp.ppterm ~metasenv:m ~subst:s ~context gty));
+ aux ((s,size,don,todo, fl)::orlist, cache)
+ | Some gty ->
+ let s, gty = apply_subst s (ctx_of gty) gty in
+ debug_print (lazy ("EXAMINE: "^ ppterm s gty));
match cache_examine cache gty with
| `Failed_in d when d >= depth ->
debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
aux (orlist,cache)
| `Succeded t ->
debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
- let s, m = put_in_subst s m g canonical_ctx t gty in
- aux ((m, s, size, don,todo, fl)::orlist, cache)
+ let s = put_in_subst s g t gty in
+ aux ((s, size, don,todo, fl)::orlist, cache)
| `Notfound
| `Failed_in _ when depth > 0 ->
( (* more depth or is the first time we see the goal *)
- if prunable m s gty todo then
+ if prunable s gty todo then
(debug_print (lazy( "FAIL: LOOP: one father is equal"));
let cache = close_failures fl cache in
aux (orlist,cache))
let cache = cache_add_underinspection cache gty depth in
debug_print (lazy ("INSPECTING: " ^
string_of_int gno ^ "("^ string_of_int size ^ "): "^
- NCicPp.ppterm ~metasenv:m ~subst:s ~context gty));
+ ppterm s gty));
(* elems are possible computations for proving gty *)
- let elems =
- equational_and_applicative_case
- signature status flags m s g gty cache context
+ let elems, cache =
+ do_something signature flags s gno depth gty cache
in
if elems = [] then
(* this goal has failed *)
let inj_gl gl = List.map (fun g -> D g) gl in
let rec map = function
| [] -> assert false
- | (cand,m,s,gl)::[] ->
+ | (cand,s,gl)::[] ->
let todo =
inj_gl gl @ (S(g,gty,cand))::todo
in
(* we are the last in OR, we fail on g and
* also on all failures implied by g *)
- (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
+ (s, size + size_gl gl, don, todo, (g,gty)::fl)
:: orlist
- | (cand,m,s,gl)::tl ->
+ | (cand,s,gl)::tl ->
let todo =
inj_gl gl @ (S(g,gty,cand))::todo
in
- (m,s, size + size_gl gl, don, todo, []) :: map tl
+ (s, size + size_gl gl, don, todo, []) :: map tl
in
map elems
in
let cache = close_failures fl cache in
aux (orlist, cache)
in
- (aux (elems, cache) : auto_result)
+ (aux (elems, cache) : 'a auto_result)
;;
-let auto_tac ~params status =
- prerr_endline "I teoremi noti sono";
- NDiscriminationTree.DiscriminationTree.iter status#auto_cache
- (fun _ t ->
- List.iter (fun t ->
- prerr_endline
- (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
- (NDiscriminationTree.TermSet.elements t));
- status
+let int name l def =
+ try int_of_string (List.assoc name l)
+ with Failure _ | Not_found -> def
+;;
+
+let auto_tac ~params:(_univ,flags) status =
+ let goals = head_goals status#stack in
+ let status, cache = mk_th_cache status goals in
+ let depth = int "depth" flags 3 in
+ (* XXX fix sort *)
+ let goals = List.map (fun i -> D(i,depth,P)) goals in
+ let elems = [status,0,[],goals,[]] in
+ let signature = () in
+ let flags = {
+ maxwidth = 3 + List.length goals;
+ maxsize = 10;
+ timeout = Unix.gettimeofday() +. 3000.;
+ do_types = false;
+ } in
+ match auto_main flags signature elems cache with
+ | Gaveup -> raise (Error (lazy "auto gave up", None))
+ | Proved (s, (_orlist, _cache)) ->
+ let stack =
+ match s#stack with
+ | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
+ | _ -> assert false
+ in
+ s#set_stack stack
;;
projects / helm.git / blobdiff