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 (* goal, depth, sort *)
-type fail = goal * NTacStatus.cic_term
-type candidate = int * NCic.term (* unique candidate number, candidate *)
+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 * NTacStatus.cic_term * candidate (* int was minsize *)
+ | 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 *)
- (#NTacStatus.tac_status as 'a) * int * op list * op list * fail list
+ (#tac_status as 'a) * int * op list * op list * fail list
type 'a auto_status =
(* list of computations that may lead to the solution: all op list will
* end with the same (S(g,_)) *)
- 'a elem list * Cache.t
+ 'a elem list * th_cache
type 'a auto_result =
| Gaveup
- | Proved of (#NTacStatus.tac_status as 'a) * 'a auto_status (* alt. proofs *)
+ | Proved of (#tac_status as 'a) * 'a auto_status (* alt. proofs *)
type flags = {
do_types : bool; (* solve goals in Type *)
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 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 equational_case _ _ _ _ _ _ = [];;
let sort_new_elems l = l;;
let only _ _ _ = true;;
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
+ debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
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
+ 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 NTacStatus.Error (msg,exn) -> debug_print msg; None
+ 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 context gty =
+let get_candidates status cache_th signature gty =
let universe = status#auto_cache in
- let _, gty = NTacStatus.term_of_cic_term status gty (NTacStatus.ctx_of gty) 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 =
- NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
+ List.filter (only signature context)
+ (NDiscriminationTree.TermSet.elements cands)
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
+ 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 context =
- let candidates = get_candidates status context gty in
- let candidates = List.filter (only signature context) candidates in
+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
;;
let equational_and_applicative_case
- signature flags status g depth gty cache context
+ 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 context
+ signature status flags g gty cache
in
let more_elems =
applicative_case
- signature status flags g gty cache context
+ signature status flags g gty cache
in
elems@more_elems
else
gty m context signature universe cache flags
| None -> *)
applicative_case
- signature status flags g gty cache context
+ signature status flags g gty cache
in
elems
in
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
+ elems, cache
;;
let calculate_goal_ty (goalno,_,_) status =
- try Some (NTacStatus.get_goalty status goalno)
- with NTacStatus.Error _ -> None
+ try Some (get_goalty status goalno)
+ with Error _ -> None
;;
let d_goals l =
let rec aux acc = function
aux fl
;;
-let auto_main context flags signature elems cache =
+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 *)
aux tables flags cache elems)
*)
| [] ->
- (* complete failure *)
debug_print (lazy "gave up");
Gaveup
| (s, _, _, [],_)::orlist ->
| (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 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
debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
aux ((s,size,don,todo, fl)::orlist, cache)
| Some gty ->
- debug_print (lazy ("EXAMINE: "^ NTacStatus.ppterm s 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));
let cache = cache_add_underinspection cache gty depth in
debug_print (lazy ("INSPECTING: " ^
string_of_int gno ^ "("^ string_of_int size ^ "): "^
- NTacStatus.ppterm s gty));
+ ppterm s gty));
(* elems are possible computations for proving gty *)
- let elems =
- equational_and_applicative_case
- signature flags s gno depth gty cache context
+ let elems, cache =
+ do_something signature flags s gno depth gty cache
in
if elems = [] then
(* this goal has failed *)
(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));
- let cache = Cache.empty in
- let goals = Continuationals.Stack.head_goals status#stack in
- let depth = 3 in (* XXX fix sort *)
+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 context = [] (* XXX big problem *) in
let signature = () in
let flags = {
- maxwidth = 3;
+ maxwidth = 3 + List.length goals;
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))
+ 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
projects / helm.git / blobdiff