;;
*)
-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 '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
| _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
;;
-let get_candidates status signature gty =
+let get_candidates status cache_th signature gty =
let universe = status#auto_cache in
let context = ctx_of gty in
- let _, gty = term_of_cic_term status gty context in
+ let _, raw_gty = term_of_cic_term status gty context in
let cands =
- NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty
in
let cands =
List.filter (only signature context)
(NDiscriminationTree.TermSet.elements cands)
in
- (* XXX we have to use the trie for the context *)
- HExtlib.filter_map (fun name,_ ->
- if name <> "_" then Some (Ast.Ident (name,None)) else None) context
+ 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 signature gty in
+ let candidates = get_candidates status cache signature gty in
debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
let elems =
List.fold_left
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 =
aux fl
;;
+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 *)
debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
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 ->
string_of_int gno ^ "("^ string_of_int size ^ "): "^
ppterm s gty));
(* elems are possible computations for proving gty *)
- let elems =
- equational_and_applicative_case
- signature flags s gno depth gty cache
+ 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 =
- let cache = Cache.empty in
+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 depth = 3 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
projects / helm.git / commitdiff
