open Printf
-let debug = false
+let debug = true
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
open Continuationals.Stack
]
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 * NTacStatus.cic_term
+type candidate = int * NCic.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 * NTacStatus.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
+ (#NTacStatus.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 * Cache.t
-type auto_result =
+type 'a auto_result =
| Gaveup
- | Proved of menv * subst * auto_status (* the alternative proofs *)
+ | Proved of (#NTacStatus.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 " ^
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
+ ));
+ let ast_for_t =
+ match t with
+ | NCic.Rel i -> assert false
+ | NCic.Const ref -> CicNotationPt.NRef ref
+ | _ -> assert false
+ in
+ let status = NTactics.focus_tac [g] status in
+ let status = NTactics.apply_tac ("",0,ast_for_t) status in
+ let open_goals = Continuationals.Stack.head_goals status#stack in
+ incr candidate_no;
+ Some ((!candidate_no,t),status,open_goals)
+ with NTacStatus.Error (msg,exn) -> debug_print msg; None
+;;
+
+
+let get_candidates status context gty =
+ let universe = status#auto_cache in
+ let _, gty = NTacStatus.term_of_cic_term status gty (NTacStatus.ctx_of gty) in
+ let cands =
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
+ in
+ (* XXX we have to trie for the context *)
+ let cands = NDiscriminationTree.TermSet.elements cands in
+ List.iter (fun x ->
+ debug_print (lazy (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)))
+ cands;
+ cands
+;;
+
+let applicative_case signature status flags g gty cache context =
+ let candidates = get_candidates status context gty in
+ let candidates = List.filter (only signature context) candidates 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 context
+=
+ let elems =
+ if false (*is_equational_case gty flags*) then
+ let elems =
+ equational_case
+ signature status flags g gty cache context
+ in
+ let more_elems =
+ applicative_case
+ signature status flags g gty cache context
+ 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 context
+ 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
+;;
+let calculate_goal_ty (goalno,_,_) status =
+ try Some (NTacStatus.get_goalty status goalno)
+ with NTacStatus.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 auto_main context 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
(* 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 context 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 ->
+ debug_print (lazy ("EXAMINE: "^ NTacStatus.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));
+ NTacStatus.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
+ signature flags s gno depth gty cache context
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
+ List.iter
+ (fun t ->
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
+ (NDiscriminationTree.TermSet.elements t));
+ let cache = Cache.empty in
+ let goals = Continuationals.Stack.head_goals status#stack in
+ let depth = 3 in (* XXX fix sort *)
+ let goals = List.map (fun i -> D(i,depth,P)) goals in
+ let elems = [status,0,[],goals,[]] in
+ let context = [] (* XXX big problem *) in
+ let signature = () in
+ let flags = {
+ maxwidth = 3;
+ maxsize = 10;
+ timeout = Unix.gettimeofday() +. 3000.;
+ do_types = false;
+ } in
+ match auto_main context flags signature elems cache with
+ | Gaveup -> raise (NTacStatus.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 / commitdiff