let debug = ref false
let debug_print ?(depth=0) s =
if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
-let print ?(depth=0) s =
+(* let print= debug_print *)
+ let print ?(depth=0) s =
prerr_endline (String.make depth '\t'^Lazy.force s)
+
let debug_do f = if !debug then f () else ()
open Continuationals.Stack
NTactics.distribute_tac (auto_paramod ~params) status
;;
+(*************** subsumption ****************)
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+(* exceptions *)
+
+let get_sgoalty status g =
+ let _,_,metasenv,subst,_ = status#obj in
+ try
+ let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
+ let ctx = NCicUntrusted.apply_subst_context
+ ~fix_projections:true subst ctx
+ in
+ NTacStatus.mk_cic_term ctx ty
+ with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
+;;
+
+let deps status g =
+ let gty = get_sgoalty status g in
+ metas_of_term status gty
+;;
+
+let menv_closure status gl =
+ let rec closure acc = function
+ | [] -> acc
+ | x::l when IntSet.mem x acc -> closure acc l
+ | x::l -> closure (IntSet.add x acc) (deps status x @ l)
+ in closure IntSet.empty gl
+;;
+
+let close_wrt_context =
+ List.fold_left
+ (fun ty ctx_entry ->
+ match ctx_entry with
+ | name, NCic.Decl t -> NCic.Prod(name,t,ty)
+ | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
+;;
+
+let args_for_context ?(k=1) ctx =
+ let _,args =
+ List.fold_left
+ (fun (n,l) ctx_entry ->
+ match ctx_entry with
+ | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
+ | name, NCic.Def(bo, _) -> n+1,l)
+ (k,[]) ctx in
+ args
+
+let constant_for_meta ctx ty i =
+ let name = "cic:/foo"^(string_of_int i)^".con" in
+ let uri = NUri.uri_of_string name in
+ let ty = close_wrt_context ty ctx in
+ (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
+ let attr = (`Generated,`Definition,`Local) in
+ let obj = NCic.Constant([],name,None,ty,attr) in
+ (* Constant of relevance * string * term option * term * c_attr *)
+ (uri,0,[],[],obj)
+
+(* not used *)
+let refresh metasenv =
+ List.fold_left
+ (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
+ let ikind = NCicUntrusted.kind_of_meta iattr in
+ let metasenv,j,instance,ty =
+ NCicMetaSubst.mk_meta ~attrs:iattr
+ metasenv ctx ~with_type:ty ikind in
+ let s_entry = i,(iattr, ctx, instance, ty) in
+ let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
+ metasenv,s_entry::subst)
+ (metasenv,[]) metasenv
+
+(* close metasenv returns a ground instance of all the metas in the
+metasenv, insantiatied with axioms, and the list of these axioms *)
+let close_metasenv metasenv subst =
+ (*
+ let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
+ *)
+ let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
+ List.fold_left
+ (fun (subst,objs) (i,(iattr,ctx,ty)) ->
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
+ let ctx =
+ NCicUntrusted.apply_subst_context ~fix_projections:true
+ subst ctx in
+ let (uri,_,_,_,obj) as okind =
+ constant_for_meta ctx ty i in
+ try
+ NCicEnvironment.check_and_add_obj okind;
+ let iref = NReference.reference_of_spec uri NReference.Decl in
+ let iterm =
+ let args = args_for_context ctx in
+ if args = [] then NCic.Const iref
+ else NCic.Appl(NCic.Const iref::args)
+ in
+ (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
+ let s_entry = i, ([], ctx, iterm, ty)
+ in s_entry::subst,okind::objs
+ with _ -> assert false)
+ (subst,[]) metasenv
+;;
+
+let ground_instances status gl =
+ let _,_,metasenv,subst,_ = status#obj in
+ let subset = menv_closure status gl in
+ let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
+(*
+ let submenv = metasenv in
+*)
+ let subst, objs = close_metasenv submenv subst in
+ try
+ List.iter
+ (fun i ->
+ let (_, ctx, t, _) = List.assoc i subst in
+ debug_print (lazy (NCicPp.ppterm ctx [] [] t));
+ List.iter
+ (fun (uri,_,_,_,_) as obj ->
+ NCicEnvironment.invalidate_item (`Obj (uri, obj)))
+ objs;
+ ())
+ gl
+ with
+ Not_found -> assert false
+ (* (ctx,t) *)
+;;
+
+let replace_meta i args target =
+ let rec aux k = function
+ (* TODO: local context *)
+ | NCic.Meta (j,lc) when i = j ->
+ (match args with
+ | [] -> NCic.Rel 1
+ | _ -> let args =
+ List.map (NCicSubstitution.subst_meta lc) args in
+ NCic.Appl(NCic.Rel k::args))
+ | NCic.Meta (j,lc) as m ->
+ (match lc with
+ _,NCic.Irl _ -> m
+ | n,NCic.Ctx l ->
+ NCic.Meta
+ (i,(0,NCic.Ctx
+ (List.map (fun t ->
+ aux k (NCicSubstitution.lift n t)) l))))
+ | t -> NCicUtils.map (fun _ k -> k+1) k aux t
+ in
+ aux 1 target
+;;
+
+let close_wrt_metasenv subst =
+ List.fold_left
+ (fun ty (i,(iattr,ctx,mty)) ->
+ let mty = NCicUntrusted.apply_subst subst ctx mty in
+ let ctx =
+ NCicUntrusted.apply_subst_context ~fix_projections:true
+ subst ctx in
+ let cty = close_wrt_context mty ctx in
+ let name = "foo"^(string_of_int i) in
+ let ty = NCicSubstitution.lift 1 ty in
+ let args = args_for_context ~k:1 ctx in
+ (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
+ let ty = replace_meta i args ty
+ in
+ NCic.Prod(name,cty,ty))
+;;
+
+let close status g =
+ let _,_,metasenv,subst,_ = status#obj in
+ let subset = menv_closure status [g] in
+ let subset = IntSet.remove g subset in
+ let elems = IntSet.elements subset in
+ let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
+ debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty)));
+ debug_print (lazy (String.concat ", " (List.map string_of_int elems)));
+ let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
+ let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in
+(*
+ let submenv = metasenv in
+*)
+ let ty = close_wrt_metasenv subst ty submenv in
+ debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
+ ctx,ty
+;;
+
+
+
(* =================================== auto =========================== *)
(****************** AUTO ********************
pp_idx status idx)
;;
-
let search_in_th gty th =
let c = ctx_of gty in
let rec aux acc = function
type fail = goal * cic_term
type candidate = int * Ast.term (* unique candidate number, candidate *)
-module IntSet = Set.Make(struct type t = int let compare = compare end)
-(* exceptions *)
-
exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
atoms of the input goals *)
exception Proved of #NTacStatus.tac_status
-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 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 only _ _ _ = true;;
+let only _ _ _ = true;;
let candidate_no = ref 0;;
List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
;;
-let try_candidate flags depth status t g =
+let try_candidate flags depth status t =
try
debug_print ~depth (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 ~depth
with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
;;
-let get_candidates status cache_th signature gty =
+let get_candidates status cache 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
+ let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe raw_gty
in
let cands =
List.filter (only signature context)
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)
+ (search_in_th gty cache)
@
List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
;;
-let applicative_case depth signature status flags g gty cache =
+let applicative_case depth signature status flags gty cache =
+ let tcache,_ = cache in
app_counter:= !app_counter+1;
- let candidates = get_candidates status cache signature gty in
+ let candidates = get_candidates status tcache signature gty in
debug_print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
let elems =
List.fold_left
(fun elems cand ->
- match try_candidate flags depth status cand g with
+ match try_candidate flags depth status cand with
| None -> elems
| Some x -> x::elems)
[] candidates
elems
;;
+exception Found
+;;
+
+(* gty is supposed to be meta-closed *)
+let is_subsumed depth status gty (_,cache) =
+ if cache=[] then false else (
+ debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
+ let n,h,metasenv,subst,obj = status#obj in
+ let ctx = ctx_of gty in
+ let _ , target = term_of_cic_term status gty ctx in
+ let target = NCicSubstitution.lift 1 target in
+ (* candidates must only be searched w.r.t the given context *)
+ let candidates =
+ try
+ let idx = List.assq ctx cache in
+ Ncic_termSet.elements
+ (InvRelDiscriminationTree.retrieve_generalizations idx gty)
+ with Not_found -> []
+ in
+ debug_print ~depth
+ (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
+ try
+ List.iter
+ (fun t ->
+ let _ , source = term_of_cic_term status t ctx in
+ let implication =
+ NCic.Prod("foo",source,target) in
+ let metasenv,j,_,_ =
+ NCicMetaSubst.mk_meta
+ metasenv ctx ~with_type:implication `IsType in
+ let status = status#set_obj (n,h,metasenv,subst,obj) in
+ let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
+ try
+ let status = NTactics.intro_tac "foo" status in
+ let status =
+ NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
+ in
+ if (head_goals status#stack = []) then raise Found
+ else ()
+ with
+ | Error _ -> ())
+ candidates;false
+ with Found -> debug_print ~depth (lazy "success");true)
+;;
+
+
let equational_and_applicative_case
signature flags status g depth gty cache
=
in
let more_elems =
applicative_case depth
- signature status flags g gty cache
+ signature status flags gty cache
in
elems@more_elems
else
gty m context signature universe cache flags
| None -> *)
applicative_case depth
- signature status flags g gty cache
+ signature status flags gty cache
in
elems
in
in
i,sort) gl) elems
in
- let elems = sort_new_elems elems in
+ (* let elems = sort_new_elems elems in *)
elems, cache
;;
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 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, keys = keys_of_term status t in
- let cache = List.fold_left (add_to_th t) cache keys in
- debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
- incr candidate_no;
- (* XXX compute the sort *)
- [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]],
- cache
+let intro ~depth status (tcache,fcache) name =
+ let status = NTactics.intro_tac name 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 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, keys = keys_of_term status t in
+ let tcache = List.fold_left (add_to_th t) tcache keys in
+ debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
+ (* unprovability is not stable w.r.t introduction *)
+ status, (tcache,[])
+;;
+
+let rec intros ~depth status cache =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals = 1);
+ let open_goal = List.hd open_goals in
+ let gty = get_goalty status open_goal in
+ let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in
+ match raw_gty with
+ | NCic.Prod (name,_,_) ->
+ let status,cache =
+ intro ~depth status cache (guess_name name (ctx_of gty))
+ in intros ~depth status cache
+ | _ -> status, cache, open_goal
+;;
+
+let reduce ~depth status g =
+ let n,h,metasenv,subst,o = status#obj in
+ let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
+ let ty' = NCicReduction.whd ~subst ctx ty in
+ if ty = ty' then []
+ else
+ (debug_print ~depth
+ (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
+ let metasenv =
+ (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
+ in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ incr candidate_no;
+ [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]])
+;;
+
+let do_something signature flags status g depth gty cache =
+ let l = reduce ~depth status g in
+ let l1,cache =
+ (equational_and_applicative_case
+ signature flags status g depth gty cache)
+ in
+ sort_new_elems (l@l1), cache
;;
let pp_goal = function
l)
;;
-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 deps status g =
- let gty = get_goalty status g in
- metas_of_term status gty
-;;
-
module M =
struct
type t = int
let compare = Pervasives.compare
end
;;
+
module MS = HTopoSort.Make(M)
;;
and
-(* The pair solved,init_status is used for chaching purposes.
- solved is the list of goals in init_status already proved.
- Initially, init_status=status and k is set to [] *)
(* let rec auto_main flags signature cache status k depth = *)
auto_main flags signature cache depth status: unit =
match goals with
| [] -> raise (Proved status)
| g::tlg ->
- if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
- else
- let status =
+ if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ else
+ let status =
if tlg=[] then status
else NTactics.branch_tac status in
+ let status, cache, g = intros ~depth status cache in
let gty = get_goalty status g in
+ let ctx,ty = close status g in
+ let closegty = mk_cic_term ctx ty in
let status, gty = apply_subst status (ctx_of gty) gty in
- debug_print ~depth (lazy("Depth = " ^ (string_of_int depth)));
- print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
- (* let closed = metas_of_term status gty = [] in *)
+ debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
+ if is_subsumed depth status closegty cache then
+ (debug_print (lazy "SUBSUMED");
+ raise (Gaveup IntSet.add g IntSet.empty))
+ else
let alternatives, cache =
do_something signature flags status g depth gty cache in
+ let loop_cache =
+ let tcache,fcache = cache in
+ tcache,add_to_th closegty fcache closegty in
let unsat =
List.fold_left
(* the underscore information does not need to be returned
by do_something *)
(fun unsat ((_,t),_,_,status,_) ->
- let depth' =
- if t=(Ast.Implicit `JustOne) then depth else depth+1 in
- print (~depth:depth')
- (lazy ("Case: " ^ CicNotationPp.pp_term t));
- try auto_clusters flags signature cache
+ let depth',looping_cache =
+ if t=(Ast.Implicit `JustOne) then depth,cache
+ else depth+1, loop_cache in
+ debug_print (~depth:depth')
+ (lazy ("Case: " ^ CicNotationPp.pp_term t));
+ try auto_clusters flags signature loop_cache
depth' status; unsat
with
| Proved status ->
else
let status = NTactics.merge_tac status
in
- (try auto_clusters flags signature cache
- depth status; unsat
+ ( (* old cache, here *)
+ try auto_clusters flags signature cache
+ depth status; assert false
with Gaveup f ->
- let debug_print = print in
debug_print ~depth
(lazy ("Unsat1 at depth " ^ (string_of_int depth)
^ ": " ^
(* TODO: cache failures *)
IntSet.union f unsat)
| Gaveup f ->
- let debug_print = print in
debug_print (~depth:depth')
(lazy ("Unsat2 at depth " ^ (string_of_int depth')
^ ": " ^
let initial_time = Unix.gettimeofday() in
app_counter:= 0;
let rec up_to x y =
- if x > y then raise (Error (lazy "auto gave up", None))
+ if x > y then
+ (print(lazy
+ ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+ print(lazy
+ ("Applicative nodes:"^string_of_int !app_counter));
+ raise (Error (lazy "auto gave up", None)))
else
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;status
+ try auto_clusters flags signature (cache,[]) 0 status;status
with
| Gaveup _ -> up_to (x+1) y
| Proved s ->
- HLog.debug ("proved at depth " ^ string_of_int x);
+ print (lazy ("proved at depth " ^ string_of_int x));
let stack =
match s#stack with
| (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
s#set_stack stack
in
let s = up_to depth depth in
- debug_print(lazy
+ print(lazy
("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- debug_print(lazy
+ print(lazy
("Applicative nodes:"^string_of_int !app_counter));
s
;;
projects / helm.git / blobdiff