open Printf
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= debug_print *)
- let print ?(depth=0) s =
+let print ?(depth=0) s =
prerr_endline (String.make depth '\t'^Lazy.force s)
+let debug_print ?(depth=0) s =
+ if !debug then print ~depth s else ()
let debug_do f = if !debug then f () else ()
module Ast = CicNotationPt
let app_counter = ref 0
-(* =================================== paramod =========================== *)
-let auto_paramod ~params:(l,_) status goal =
- let gty = get_goalty status goal in
- let n,h,metasenv,subst,o = status#obj in
- let status,t = term_of_cic_term status gty (ctx_of gty) in
- let status, l =
- List.fold_left
- (fun (status, l) t ->
- let status, t = disambiguate status (ctx_of gty) t None in
- let status, ty = typeof status (ctx_of t) t in
- let status, t = term_of_cic_term status t (ctx_of gty) in
- let status, ty = term_of_cic_term status ty (ctx_of ty) in
- (status, (t,ty) :: l))
- (status,[]) l
- in
- match
- NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
- with
- | [] -> raise (Error (lazy "no proof found",None))
- | (pt, metasenv, subst)::_ ->
- let status = status#set_obj (n,h,metasenv,subst,o) in
- instantiate status goal (mk_cic_term (ctx_of gty) pt)
-;;
-
-let auto_paramod_tac ~params status =
- NTactics.distribute_tac (auto_paramod ~params) status
-;;
-
-(*************** subsumption ****************)
+(* ======================= utility functions ========================= *)
module IntSet = Set.Make(struct type t = int let compare = compare end)
-(* exceptions *)
let get_sgoalty status g =
let _,_,metasenv,subst,_ = status#obj in
in closure IntSet.empty gl
;;
+(* we call a "fact" an object whose hypothesis occur in the goal
+ or in types of goal-variables *)
+let is_a_fact status ty =
+ let status, ty, metas = saturate ~delta:0 status ty in
+ debug_print (lazy ("saturated ty :" ^ (ppterm status ty)));
+ let g_metas = metas_of_term status ty in
+ let clos = menv_closure status g_metas in
+ (* let _,_,metasenv,_,_ = status#obj in *)
+ let menv =
+ List.fold_left
+ (fun acc m ->
+ let _, m = term_of_cic_term status m (ctx_of m) in
+ match m with
+ | NCic.Meta(i,_) -> IntSet.add i acc
+ | _ -> assert false)
+ IntSet.empty metas
+ in IntSet.subset menv clos;;
+
+let is_a_fact_obj s uri =
+ let obj = NCicEnvironment.get_checked_obj uri in
+ match obj with
+ | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
+ is_a_fact s (mk_cic_term [] ty)
+(* aggiungere i costruttori *)
+ | _ -> false
+
+let is_a_fact_ast status subst metasenv ctx cand =
+ debug_print ~depth:0
+ (lazy ("------- checking " ^ CicNotationPp.pp_term cand));
+ let status, t = disambiguate status ctx ("",0,cand) None in
+ let status,t = term_of_cic_term status t ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ is_a_fact status (mk_cic_term ctx ty)
+
+let current_goal status =
+ 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 ctx = ctx_of gty in
+ open_goal, ctx, gty
+
+
+(* =============================== paramod =========================== *)
+let solve fast status eq_cache goal =
+ let f =
+ if fast then NCicParamod.fast_eq_check
+ else NCicParamod.paramod in
+ let n,h,metasenv,subst,o = status#obj in
+ let gname, ctx, gty = List.assoc goal metasenv in
+ let gty = NCicUntrusted.apply_subst subst ctx gty in
+ let build_status (pt, _, metasenv, subst) =
+ try
+ debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ let stamp = Unix.gettimeofday () in
+ let metasenv, subst, pt, pty =
+ NCicRefiner.typeof status
+ (* (status#set_coerc_db NCicCoercion.empty_db) *)
+ metasenv subst ctx pt None in
+ debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
+ let metasenv, subst =
+ NCicUnification.unify status metasenv subst ctx gty pty
+ (* the previous code is much less expensive than directly refining
+ pt with expected type pty
+ in
+ prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
+ NCicRefiner.typeof
+ (status#set_coerc_db NCicCoercion.empty_db)
+ metasenv subst ctx pt (Some gty) *)
+ in
+ debug_print (lazy (Printf.sprintf "Refined in %fs"
+ (Unix.gettimeofday() -. stamp)));
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
+ let subst = (goal,(gname,ctx,pt,pty)) :: subst in
+ Some (status#set_obj (n,h,metasenv,subst,o))
+ with
+ NCicRefiner.RefineFailure msg
+ | NCicRefiner.Uncertain msg ->
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ snd (Lazy.force msg))); None
+ | NCicRefiner.AssertFailure msg ->
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ Lazy.force msg)); None
+ | _ -> None
+ in
+ HExtlib.filter_map build_status
+ (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
+;;
+
+let fast_eq_check eq_cache status goal =
+ match solve true status eq_cache goal with
+ | [] -> raise (Error (lazy "no proof found",None))
+ | s::_ -> s
+;;
+
+let dist_fast_eq_check eq_cache s =
+ NTactics.distribute_tac (fast_eq_check eq_cache) s
+;;
+
+let auto_eq_check eq_cache status =
+ try
+ let s = dist_fast_eq_check eq_cache status in
+ [s]
+ with
+ | Error _ -> []
+;;
+
+(* warning: ctx is supposed to be already instantiated w.r.t subst *)
+let index_local_equations eq_cache status =
+ debug_print (lazy "indexing equations");
+ let open_goals = head_goals status#stack in
+ let open_goal = List.hd open_goals in
+ let ngty = get_goalty status open_goal in
+ let ctx = ctx_of ngty in
+ let c = ref 0 in
+ List.fold_left
+ (fun eq_cache _ ->
+ c:= !c+1;
+ let t = NCic.Rel !c in
+ try
+ let ty = NCicTypeChecker.typeof [] [] ctx t in
+ if is_a_fact status (mk_cic_term ctx ty) then
+ (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+ NCicParamod.forward_infer_step eq_cache t ty)
+ else
+ (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
+ eq_cache)
+ with
+ | NCicTypeChecker.TypeCheckerFailure _
+ | NCicTypeChecker.AssertFailure _ -> eq_cache)
+ eq_cache ctx
+;;
+
+let fast_eq_check_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ dist_fast_eq_check unit_eq s
+;;
+
+let paramod eq_cache status goal =
+ match solve false status eq_cache goal with
+ | [] -> raise (Error (lazy "no proof found",None))
+ | s::_ -> s
+;;
+
+let paramod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (paramod unit_eq) s
+;;
+
+(*
+let fast_eq_check_tac_all ~params eq_cache status =
+ let g,_,_ = current_goal status in
+ let allstates = fast_eq_check_all status eq_cache g in
+ let pseudo_low_tac s _ _ = s in
+ let pseudo_low_tactics =
+ List.map pseudo_low_tac allstates
+ in
+ List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
+;;
+*)
+
+(*
+let demod status eq_cache goal =
+ let n,h,metasenv,subst,o = status#obj in
+ let gname, ctx, gty = List.assoc goal metasenv in
+ let gty = NCicUntrusted.apply_subst subst ctx gty in
+
+let demod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ dist_fast_eq_check unit_eq s
+*)
+
+(*************** subsumption ****************)
+
let close_wrt_context =
List.fold_left
(fun ty ctx_entry ->
- match ctx_entry with
+ match ctx_entry with
| name, NCic.Decl t -> NCic.Prod(name,t,ty)
| name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
;;
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)
+ 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
(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
+ 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,s_entry::subst)
(metasenv,[]) metasenv
(* close metasenv returns a ground instance of all the metas in the
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 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
+ 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)
+ let s_entry = i, ([], ctx, iterm, ty)
+ in s_entry::subst,okind::objs
+ with _ -> assert false)
(subst,[]) metasenv
;;
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;
- ())
+ 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
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))
+ (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
(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
+ 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 elems = IntSet.elements subset in
let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
let ty = NCicUntrusted.apply_subst subst ctx ty in
- print (lazy ("Elements for " ^ (NCicPp.ppterm ctx [] metasenv ty)));
- print (lazy (String.concat ", " (List.map string_of_int elems)));
+ 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
- print (lazy (NCicPp.ppterm ctx [] [] ty));
- ty
+ debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
+ ctx,ty
;;
with
| None, tables ->
(* if normal application fails we try to be smart *)
- (match try_smart_candidate dbd goalty
+ (match try_smart_candidate dbd goalty
tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
+ with
+ | None, tables -> tables, elems
| Some x, tables -> tables, x::elems)
| Some x, tables -> tables, x::elems)
(tables,[]) candidates
| (S _)::tl -> aux b tl
| (D (_,_,T))::tl -> aux b tl
| (D g)::tl ->
- (match calculate_goal_ty g s m with
+ (match calculate_goal_ty g s m with
| None -> aux b tl
- | Some (canonical_ctx, gty) ->
+ | Some (canonical_ctx, gty) ->
let gsize, _ =
Utils.weight_of_term
- ~consider_metas:false ~count_metas_occurrences:true gty in
- let newb = b || gsize > flags.maxgoalsizefactor in
- aux newb tl)
+ ~consider_metas:false ~count_metas_occurrences:true gty in
+ let newb = b || gsize > flags.maxgoalsizefactor in
+ aux newb tl)
| [] -> b
in
aux false todo
let prunable menv subst ty todo =
let rec aux = function
| (S(_,k,_,_))::tl ->
- (match Equality.meta_convertibility_subst k ty menv with
- | None -> aux tl
- | Some variant ->
- no_progress variant tl (* || aux tl*))
+ (match Equality.meta_convertibility_subst k ty menv with
+ | None -> aux tl
+ | Some variant ->
+ no_progress variant tl (* || aux tl*))
| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
| [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
| D ((n,_,P) as g)::tl ->
- (match calculate_goal_ty g subst menv with
+ (match calculate_goal_ty g subst menv with
| None -> no_progress variant tl
| Some (_, gty) ->
- (match calculate_goal_ty g variant menv with
- | None -> assert false
- | Some (_, gty') ->
- if gty = gty' then no_progress variant tl
+ (match calculate_goal_ty g variant menv with
+ | None -> assert false
+ | Some (_, gty') ->
+ if gty = gty' then no_progress variant tl
(*
(prerr_endline (string_of_int n);
prerr_endline (CicPp.ppterm gty);
prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
prerr_endline "---------- menv";
prerr_endline (CicMetaSubst.ppmetasenv [] menv);
- no_progress variant tl) *)
- else false))
+ no_progress variant tl) *)
+ else false))
| _::tl -> no_progress variant tl
in
aux todo
let signature =
List.fold_left
(fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataQuery.signature_of metasenv g)
)
MetadataConstraints.UriManagerSet.empty gl
in
let signature =
List.fold_left
(fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataQuery.signature_of metasenv g)
)
MetadataConstraints.UriManagerSet.empty gl
in
List.fold_left
(fun set t ->
let ty, _ =
- CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.oblivion_ugraph
- in
- MetadataConstraints.UriManagerSet.union set
- (MetadataConstraints.constants_of ty)
+ CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.oblivion_ugraph
+ in
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataConstraints.constants_of ty)
)
signature univ
in
;;
*)
+(****************** smart application ********************)
+
+
+let smart_apply t unit_eq status g =
+ let n,h,metasenv,subst,o = status#obj in
+ let gname, ctx, gty = List.assoc g metasenv in
+ (* let ggty = mk_cic_term context gty in *)
+ let status, t = disambiguate status ctx t None in
+ let status,t = term_of_cic_term status t ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in
+ let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ let pterm = if args=[] then t else NCic.Appl(t::args) in
+ let eq_coerc =
+ let uri =
+ NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
+ NCic.Const ref
+ in
+ let smart =
+ NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
+ let smart = mk_cic_term ctx smart in
+ try
+ let status = instantiate status g smart in
+ let _,_,metasenv,subst,_ = status#obj in
+ let _,ctx,jty = List.assoc j metasenv in
+ let jty = NCicUntrusted.apply_subst subst ctx jty in
+ debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
+ fast_eq_check unit_eq status j
+ with
+ | Error _ as e -> debug_print (lazy "error"); raise e
+
+let smart_apply_tac t s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (smart_apply t unit_eq) s
+
+let smart_apply_auto t eq_cache =
+ NTactics.distribute_tac (smart_apply t eq_cache)
+
+
(****************** types **************)
+
+
type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
let keys_of_term status t =
let keys =
let _, ty = term_of_cic_term status ty (ctx_of ty) in
match ty with
- | NCic.Const (NReference.Ref (_,NReference.Def h))
- | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
+ | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
+ | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
when h > 0 ->
let _,ty,_= saturate status ~delta:(h-1) orig_ty in
ty::keys
List.fold_left
(fun (status, i, idx) _ ->
let t = mk_cic_term ctx (NCic.Rel i) in
- debug_print(lazy("indexing: "^ppterm status t));
let status, keys = keys_of_term status t in
+ debug_print(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
let idx =
List.fold_left (fun idx k ->
InvRelDiscriminationTree.index idx k t) idx keys
replace c
;;
+let rm_from_th t c ty =
+ let key_c = ctx_of t in
+ if not (List.mem_assq key_c c) then assert false
+ else
+ let rec replace = function
+ | [] -> []
+ | (x, idx) :: tl when x == key_c ->
+ (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
+ | x :: tl -> x :: replace tl
+ in
+ replace c
+;;
+
let pp_idx status idx =
InvRelDiscriminationTree.iter idx
(fun k set ->
pp_idx status idx)
;;
-
let search_in_th gty th =
let c = ctx_of gty in
let rec aux acc = function
- | [] -> Ncic_termSet.elements acc
+ | [] -> (* Ncic_termSet.elements *) acc
| (_::tl) as k ->
try
let idx = List.assq k th in
type flags = {
do_types : bool; (* solve goals in Type *)
+ last : bool; (* last goal: take first solution only *)
maxwidth : int;
maxsize : int;
maxdepth : int;
timeout : float;
}
+type cache =
+ {facts : th_cache; (* positive results *)
+ under_inspection : cic_term list * th_cache; (* to prune looping *)
+ unit_eq : NCicParamod.state
+ }
+
type sort = T | P
type goal = int * sort (* goal, depth, sort *)
type fail = goal * cic_term
exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
atoms of the input goals *)
-exception Proved of #NTacStatus.tac_status
+exception Proved of NTacStatus.tac_status
+
+let height_of_ref (NReference.Ref (uri, x)) =
+ match x with
+ | NReference.Decl
+ | NReference.Ind _
+ | NReference.Con _
+ | NReference.CoFix _ ->
+ let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
+ height
+ | NReference.Def h -> h
+ | NReference.Fix (_,_,h) -> h
+;;
+
+let fast_height_of_term t =
+ let h = ref 0 in
+ let rec aux =
+ function
+ NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
+ | NCic.Meta _ -> ()
+ | NCic.Rel _
+ | NCic.Sort _ -> ()
+ | NCic.Implicit _ -> assert false
+ | NCic.Const nref as t ->
+(*
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
+ ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
+*)
+ h := max !h (height_of_ref nref)
+ | NCic.Prod (_,t1,t2)
+ | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | NCic.Appl l -> List.iter aux l
+ | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ in
+ aux t; !h
+;;
+
+let height_of_goals status =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals > 0);
+ let h = ref 1 in
+ List.iter
+ (fun open_goal ->
+ let ty = get_goalty status open_goal in
+ let context = ctx_of ty in
+ let _, ty = term_of_cic_term status ty (ctx_of ty) in
+ h := max !h (fast_height_of_term ty);
+ List.iter
+ (function
+ | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty)
+ | _, NCic.Def (bo,ty) ->
+ h := max !h (fast_height_of_term ty);
+ h := max !h (fast_height_of_term bo);
+ )
+ context)
+ open_goals;
+ prerr_endline ("altezza sequente: " ^ string_of_int !h);
+ !h
+;;
+
+(* 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 init_cache ?(facts=[]) ?(under_inspection=[],[])
+ ?(unit_eq=NCicParamod.empty_state) _ =
+ {facts = facts;
+ under_inspection = under_inspection;
+ unit_eq = unit_eq
+ }
+
+let only signature _context candidate =
+ (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
+ let candidate_ty =
+ NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
+ in
+ let height = fast_height_of_term candidate_ty in
+ let rc = signature >= height in
+ if rc = false then
+ debug_print (lazy ("Filtro: " ^ NCicPp.ppterm ~context:[] ~subst:[]
+ ~metasenv:[] candidate ^ ": " ^ string_of_int height))
+ else
+ debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
+ ~metasenv:[] candidate ^ ": " ^ string_of_int height));
-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;;
+ rc
+;;
let candidate_no = ref 0;;
-let sort_new_elems l =
- List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
-;;
+let openg_no status = List.length (head_goals status#stack)
-let try_candidate flags depth status t g =
+let sort_new_elems l =
+ List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
+
+let try_candidate ?(smart=0) flags depth status eq_cache 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
- (lazy ("success: "^String.concat " "(List.map string_of_int open_goals)));
- if List.length open_goals > flags.maxwidth ||
- (depth = flags.maxdepth && open_goals <> []) then
- (debug_print ~depth (lazy "pruned immediately"); None)
+ debug_print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
+ let status =
+ if smart= 0 then NTactics.apply_tac ("",0,t) status
+ else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
+ else (* smart = 2: both *)
+ try NTactics.apply_tac ("",0,t) status
+ with Error _ ->
+ smart_apply_auto ("",0,t) eq_cache status in
+ let og_no = openg_no status in
+ if (* og_no > flags.maxwidth || *)
+ ((depth + 1) = flags.maxdepth && og_no <> 0) then
+ (debug_print ~depth (lazy "pruned immediately"); None)
else
(incr candidate_no;
- Some ((!candidate_no,t),status,open_goals))
+ Some ((!candidate_no,t),status))
with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
;;
-let get_candidates status cache_th signature gty =
+let get_candidates ?(smart=true) status cache signature gty =
let universe = status#auto_cache in
let context = ctx_of gty in
+ let t_ast t =
+ let _status, t = term_of_cic_term status t context
+ in Ast.NCic t in
+ let c_ast = function
+ | NCic.Const r -> Ast.NRef r | _ -> assert false 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)
+ let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe raw_gty in
+ let local_cands = search_in_th gty cache in
+ debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
+ debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
+ let together global local =
+ List.map c_ast
+ (List.filter (only signature context)
+ (NDiscriminationTree.TermSet.elements global)) @
+ List.map t_ast (Ncic_termSet.elements local) in
+ let candidates = together cands local_cands in
+ let smart_candidates =
+ if smart then
+ match raw_gty with
+ | NCic.Appl (hd::tl) ->
+ let weak_gty =
+ NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
+ (List.length tl)) in
+ let more_cands =
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe weak_gty in
+ let smart_cands =
+ NDiscriminationTree.TermSet.diff more_cands cands in
+ let cic_weak_gty = mk_cic_term context weak_gty in
+ let more_local_cands = search_in_th cic_weak_gty cache in
+ let smart_local_cands =
+ Ncic_termSet.diff more_local_cands local_cands in
+ together smart_cands smart_local_cands
+ | _ -> []
+ else []
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
+ candidates, smart_candidates
;;
-let applicative_case depth signature status flags g gty cache =
+let applicative_case depth signature status flags gty (cache:cache) =
app_counter:= !app_counter+1;
- let candidates = get_candidates status cache signature gty in
+ let _,_,metasenv,subst,_ = status#obj in
+ let context = ctx_of gty in
+ let tcache = cache.facts in
+ let is_eq =
+ let status, t = term_of_cic_term status gty context in
+ NCicParamod.is_equation metasenv subst context t
+ in
+ debug_print(lazy (string_of_bool is_eq));
+ let candidates, smart_candidates =
+ get_candidates ~smart:(not is_eq) status tcache signature gty in
debug_print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
- let elems =
+ debug_print ~depth
+ (lazy ("smart candidates: " ^
+ string_of_int (List.length smart_candidates)));
+(*
+ let sm = 0 in
+ let smart_candidates = [] in *)
+ let sm = if is_eq then 0 else 2 in
+ let maxd = ((depth + 1) = flags.maxdepth) in
+ let only_one = flags.last && maxd in
+ debug_print (lazy ("only_one: " ^ (string_of_bool only_one)));
+ debug_print (lazy ("maxd: " ^ (string_of_bool maxd)));
+ let elems =
List.fold_left
(fun elems cand ->
- match try_candidate flags depth status cand g with
- | None -> elems
- | Some x -> x::elems)
+ if (only_one && (elems <> [])) then elems
+ else
+ if (maxd && not(is_a_fact_ast status subst metasenv context cand))
+ then (debug_print (lazy "pruned: not a fact"); elems)
+ else
+ match try_candidate (~smart:sm)
+ flags depth status cache.unit_eq cand with
+ | None -> elems
+ | Some x -> x::elems)
[] candidates
in
- elems
+ let more_elems =
+ if only_one && elems <> [] then elems
+ else
+ List.fold_left
+ (fun elems cand ->
+ if (only_one && (elems <> [])) then elems
+ else
+ if (maxd && not(is_a_fact_ast status subst metasenv context cand))
+ then (debug_print (lazy "pruned: not a fact"); elems)
+ else
+ match try_candidate (~smart:1)
+ flags depth status cache.unit_eq cand with
+ | None -> elems
+ | Some x -> x::elems)
+ [] smart_candidates
+ in
+ elems@more_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 depth
- 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 depth
- signature status flags g gty cache
- in
- elems
- in
- let elems =
- List.map (fun c,s,gl ->
- c,1,1,s,List.map (fun i ->
- let sort =
- let gty = get_goalty s i in
- let _, sort = typeof s (ctx_of gty) gty in
- match term_of_cic_term s sort (ctx_of sort) with
- | _, NCic.Sort NCic.Prop -> P
- | _ -> T
- in
- i,sort) gl) elems
- in
- let elems = sort_new_elems elems in
- elems, cache
+exception Found
+;;
+
+(* gty is supposed to be meta-closed *)
+let is_subsumed depth status gty cache =
+ if cache=[] then false else (
+ 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 rec guess_name name ctx =
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 is_prod status =
+ let _, ctx, gty = current_goal status in
+ let _, raw_gty = term_of_cic_term status gty ctx in
+ match raw_gty with
+ | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
+ | _ -> None
+
+let intro ~depth status facts name =
+ let status = NTactics.intro_tac name status in
+ let _, ctx, ngty = current_goal status in
+ let t = mk_cic_term ctx (NCic.Rel 1) in
+ let status, keys = keys_of_term status t in
+ let facts = List.fold_left (add_to_th t) facts keys in
+ debug_print ~depth (lazy ("intro: "^ name));
+ (* unprovability is not stable w.r.t introduction *)
+ status, facts
+;;
+
+let rec intros_facts ~depth status facts =
+ match is_prod status with
+ | Some(name) ->
+ let status,facts =
+ intro ~depth status facts name
+ in intros_facts ~depth status facts
+ | _ -> status, facts
+;;
+
+let rec intros ~depth status (cache:cache) =
+ match is_prod status with
+ | Some _ ->
+ let status,facts =
+ intros_facts ~depth status cache.facts
+ in
+ (* we reindex the equation from scratch *)
+ let unit_eq =
+ index_local_equations status#eq_cache status in
+ status, init_cache ~facts ~unit_eq ()
+ | _ -> status, cache
+;;
+
+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
+ (* we merge to gain a depth level; the previous goal level should
+ be empty *)
+ let status = NTactics.merge_tac status in
+ incr candidate_no;
+ [(!candidate_no,Ast.Ident("__whd",None)),status])
+;;
+
+let do_something signature flags status g depth gty cache =
+ (* whd *)
+ let l = reduce ~depth status g in
+ (* backward aplications *)
+ let l1 =
+ List.map
+ (fun s ->
+ incr candidate_no;
+ ((!candidate_no,Ast.Ident("__paramod",None)),s))
+ (auto_eq_check cache.unit_eq status)
+ in
+ let l2 =
+ (* if (l1 <> []) then [] else *)
+ applicative_case depth signature status flags gty cache
+ (* fast paramodulation *)
+ in
+ (* states in l1 have have an empty set of subgoals: no point to sort them *)
+ debug_print ~depth
+ (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
+ l1 @ (sort_new_elems (l@l2)), cache
;;
let pp_goal = function
String.concat ", "
(List.map
(fun i ->
- let gty = get_goalty status i in
- NTacStatus.ppterm status gty)
+ let gty = get_goalty status i in
+ NTacStatus.ppterm status gty)
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
-;;
-
module M =
struct
type t = int
| [] -> assert false
| (goals, t, k, tag) :: s ->
let g = head_goals status#stack in
- let sortedg =
- (List.rev (MS.topological_sort g (deps status))) in
+ let sortedg =
+ (List.rev (MS.topological_sort g (deps status))) in
debug_print (lazy ("old g = " ^
String.concat "," (List.map string_of_int g)));
debug_print (lazy ("sorted goals = " ^
- String.concat "," (List.map string_of_int sortedg)));
- let is_it i = function
- | (_,Continuationals.Stack.Open j )
+ String.concat "," (List.map string_of_int sortedg)));
+ let is_it i = function
+ | (_,Continuationals.Stack.Open j )
| (_,Continuationals.Stack.Closed j ) -> i = j
- in
- let sorted_goals =
- List.map (fun i -> List.find (is_it i) goals) sortedg
- in
- (sorted_goals, t, k, tag) :: s
+ in
+ let sorted_goals =
+ List.map (fun i -> List.find (is_it i) goals) sortedg
+ in
+ (sorted_goals, t, k, tag) :: s
in
status#set_stack gstatus
;;
| [] -> assert false
| (g, t, k, tag) :: s ->
let is_open = function
- | (_,Continuationals.Stack.Open _) -> true
+ | (_,Continuationals.Stack.Open _) -> true
| (_,Continuationals.Stack.Closed _) -> false
- in
- let g' = List.filter is_open g in
- (g', t, k, tag) :: s
+ in
+ let g' = List.filter is_open g in
+ (g', t, k, tag) :: s
in
status#set_stack gstatus
;;
| [] -> assert false
| (g, t, k, tag) :: s ->
let in_focus = function
- | (_,Continuationals.Stack.Open i)
+ | (_,Continuationals.Stack.Open i)
| (_,Continuationals.Stack.Closed i) -> List.mem i focus
- in
+ in
let focus,others = List.partition in_focus g
- in
+ in
+ (* we need to mark it as a BranchTag, otherwise cannot merge later *)
+ (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
+ in
+ status#set_stack gstatus
+;;
+
+let deep_focus_tac level focus status =
+ let in_focus = function
+ | (_,Continuationals.Stack.Open i)
+ | (_,Continuationals.Stack.Closed i) -> List.mem i focus
+ in
+ let rec slice level gs =
+ if level = 0 then [],[],gs else
+ match gs with
+ | [] -> assert false
+ | (g, t, k, tag) :: s ->
+ let f,o,gs = slice (level-1) s in
+ let f1,o1 = List.partition in_focus g
+ in
(* we need to mark it as a BranchTag, otherwise cannot merge later *)
- (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
+ (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
+ in
+ let gstatus =
+ let f,o,s = slice level status#stack in f@o@s
in
status#set_stack gstatus
;;
-let rec auto_clusters
+let open_goals level status =
+ let rec aux level gs =
+ if level = 0 then []
+ else match gs with
+ | [] -> assert false
+ | _ :: s -> head_goals gs @ aux (level-1) s
+ in
+ aux level status#stack
+;;
+
+let rec auto_clusters ?(top=false)
flags signature cache depth status : unit =
- debug_print ~depth (lazy "entering auto clusters");
+ debug_print ~depth (lazy ("entering auto clusters at depth " ^
+ (string_of_int depth)));
(* ignore(Unix.select [] [] [] 0.01); *)
let status = clean_up_tac status in
let goals = head_goals status#stack in
- if goals = [] then raise (Proved status)
- else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ if goals = [] then
+ if depth = 0 then raise (Proved status)
+ else
+ let status = NTactics.merge_tac status in
+ auto_clusters flags signature (cache:cache) (depth-1) status
else if List.length goals < 2 then
auto_main flags signature cache depth status
else
+ let all_goals = open_goals (depth+1) status in
debug_print ~depth (lazy ("goals = " ^
- String.concat "," (List.map string_of_int goals)));
- let classes = HExtlib.clusters (deps status) goals in
+ String.concat "," (List.map string_of_int all_goals)));
+ let classes = HExtlib.clusters (deps status) all_goals in
+ let classes = if top then List.rev classes else classes in
debug_print ~depth
- (lazy
- (String.concat "\n"
- (List.map
- (fun l ->
- ("cluster:" ^ String.concat "," (List.map string_of_int l)))
- classes)));
- let status =
- List.fold_left
- (fun status gl ->
- let status = focus_tac gl status in
- try
+ (lazy
+ (String.concat "\n"
+ (List.map
+ (fun l ->
+ ("cluster:" ^ String.concat "," (List.map string_of_int l)))
+ classes)));
+ let status,b =
+ List.fold_left
+ (fun (status,b) gl ->
+ let lold = List.length status#stack in
+ debug_print ~depth (lazy ("stack length = " ^
+ (string_of_int lold)));
+ let fstatus = deep_focus_tac (depth+1) gl status in
+ try
debug_print ~depth (lazy ("focusing on" ^
- String.concat "," (List.map string_of_int gl)));
- auto_main flags signature cache depth status; status
- with Proved(status) -> NTactics.merge_tac status)
- status classes
- in raise (Proved status)
+ String.concat "," (List.map string_of_int gl)));
+ auto_main flags signature cache depth fstatus; assert false
+ with
+ | Proved(status) ->
+ let status = NTactics.merge_tac status in
+ let lnew = List.length status#stack in
+ assert (lold = lnew);
+ (status,true)
+ | Gaveup _ when top -> (status,b)
+ )
+ (status,false) classes
+ in
+ let rec final_merge n s =
+ if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
+ in let status = final_merge depth status
+ in if b then raise (Proved status) else raise (Gaveup IntSet.empty)
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 =
+
+(* BRAND NEW VERSION *)
+auto_main flags signature (cache:cache) depth status: unit =
debug_print ~depth (lazy "entering auto main");
+ debug_print ~depth (lazy ("stack length = " ^
+ (string_of_int (List.length status#stack))));
(* ignore(Unix.select [] [] [] 0.01); *)
let status = sort_tac (clean_up_tac status) in
let goals = head_goals status#stack in
match goals with
- | [] -> raise (Proved status)
- | g::tlg ->
- if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
- else
- let status =
- if tlg=[] then status
- else NTactics.branch_tac status in
- let gty = get_goalty status g in
- let status, gty = apply_subst status (ctx_of gty) gty in
- debug_print ~depth (lazy("Depth = " ^ (string_of_int depth)));
- debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
- close status g;
- (* let closed = metas_of_term status gty = [] in *)
- let alternatives, cache =
- do_something signature flags status g depth gty cache 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
- debug_print (~depth:depth')
- (lazy ("Case: " ^ CicNotationPp.pp_term t));
- try auto_clusters flags signature cache
- depth' status; unsat
- with
- | Proved status ->
- debug_print (~depth:depth') (lazy "proved");
- if tlg=[] then raise (Proved status)
- else
- let status = NTactics.merge_tac status
- in
- (try auto_clusters flags signature cache
- depth status; unsat
- with Gaveup f ->
- debug_print ~depth
- (lazy ("Unsat1 at depth " ^ (string_of_int depth)
- ^ ": " ^
- (pp_goals status (IntSet.elements f))));
- (* TODO: cache failures *)
- IntSet.union f unsat)
- | Gaveup f ->
- debug_print (~depth:depth')
- (lazy ("Unsat2 at depth " ^ (string_of_int depth')
- ^ ": " ^
- (pp_goals status (IntSet.elements f))));
- (* TODO: cache local failures *)
- unsat)
- IntSet.empty alternatives
- in
- raise (Gaveup IntSet.add g unsat)
-;;
-
+ | [] when depth = 0 -> raise (Proved status)
+ | [] ->
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> assert false
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
+ auto_clusters flags signature (cache:cache) (depth-1) status
+ | orig::_ ->
+ let ng = List.length goals in
+ if ng > flags.maxwidth then
+ (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
+ else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ else
+ let status = NTactics.branch_tac ~force:true status in
+ let status, cache = intros ~depth status cache in
+ let g,gctx, gty = current_goal status in
+ let ctx,ty = close status g in
+ let closegty = mk_cic_term ctx ty in
+ let status, gty = apply_subst status gctx gty in
+ debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
+ if is_subsumed depth status closegty (snd cache.under_inspection) then
+ (print ~depth (lazy "SUBSUMED");
+ raise (Gaveup IntSet.add g IntSet.empty))
+ else
+ let do_flags =
+ {flags with last = flags.last && ng=1} in
+ let alternatives, cache =
+ do_something signature do_flags status g depth gty cache in
+ let loop_cache =
+ let l,tree = cache.under_inspection in
+ let l,tree = closegty::l, add_to_th closegty tree closegty in
+ {cache with under_inspection = l,tree} in
+ List.iter
+ (fun ((_,t),status) ->
+ debug_print ~depth
+ (lazy("(re)considering goal " ^
+ (string_of_int g) ^" : "^ppterm status gty));
+ debug_print (~depth:depth)
+ (lazy ("Case: " ^ CicNotationPp.pp_term t));
+ let depth,cache =
+ if t=Ast.Ident("__whd",None) then depth, cache
+ else depth+1,loop_cache in
+ try
+ auto_clusters flags signature (cache:cache) depth status
+ with Gaveup _ ->
+ debug_print ~depth (lazy "Failed");())
+ alternatives;
+ raise (Gaveup IntSet.empty)
+;;
+
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 oldstatus = status in
+ let status = (status:> NTacStatus.tac_status) in
let goals = head_goals status#stack in
- let status, cache = mk_th_cache status goals in
-(* pp_th status cache; *)
+ let status, facts = mk_th_cache status goals in
+ let unit_eq = index_local_equations status#eq_cache status in
+ let cache = init_cache ~facts ~unit_eq () in
+(* pp_th status facts; *)
(*
NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
debug_print (lazy(
*)
let depth = int "depth" flags 3 in
let size = int "size" flags 10 in
- let width = int "width" flags (3+List.length goals) in
+ let width = int "width" flags 4 (* (3+List.length goals)*) in
(* XXX fix sort *)
- let goals = List.map (fun i -> (i,P)) goals in
- let signature = () in
+(* let goals = List.map (fun i -> (i,P)) goals in *)
+ let signature = height_of_goals status in
let flags = {
+ last = true;
maxwidth = width;
maxsize = size;
maxdepth = 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)));
+ debug_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
- with
- | Gaveup _ -> up_to (x+1) y
- | Proved s ->
- HLog.debug ("proved at depth " ^ string_of_int x);
+ try auto_clusters (~top:true) flags signature cache 0 status;assert false
+(*
+ try auto_main flags signature cache 0 status;assert false
+*)
+ with
+ | Gaveup _ -> up_to (x+1) y
+ | Proved s ->
+ debug_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
- | _ -> assert false
+ match s#stack with
+ | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
+ | _ -> assert false
in
- s#set_stack stack
+ let s = s#set_stack stack in
+ oldstatus#set_status s
in
let s = up_to depth depth in
debug_print(lazy
projects / helm.git / blobdiff