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 = 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 ()
module Ast = CicNotationPt
let app_counter = ref 0
-(* =================================== paramod =========================== *)
+(* ======================= utility functions ========================= *)
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+
+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
+;;
+
+(* 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, _ = saturate ~delta:max_int status ty in
+ 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 (i,_) -> IntSet.add i acc)
+ IntSet.empty metasenv
+ in IntSet.equal clos menv;;
+
+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 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 auto_paramod ~params:(l,_) status goal =
let gty = get_goalty status goal in
let n,h,metasenv,subst,o = status#obj in
NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
with
| [] -> raise (Error (lazy "no proof found",None))
- | (pt, metasenv, subst)::_ ->
+ | (pt, _, metasenv, subst)::_ ->
let status = status#set_obj (n,h,metasenv,subst,o) in
instantiate status goal (mk_cic_term (ctx_of gty) pt)
;;
NTactics.distribute_tac (auto_paramod ~params) status
;;
-let fast_eq_check ~params status goal =
- let gty = get_goalty status goal in
+let fast_eq_check_all status eq_cache goal =
let n,h,metasenv,subst,o = status#obj in
- let eq_cache = status#eq_cache in
- let status,t = term_of_cic_term status gty (ctx_of gty) in
- match
- NCicParamod.fast_eq_check status metasenv subst (ctx_of gty)
- eq_cache (NCic.Rel ~-1,t)
- with
- | [] -> raise (Error (lazy "no proof found",None))
- | (pt, metasenv, subst)::_ ->
+ let gname, ctx, gty = List.assoc goal metasenv in
+ let gty = NCicUntrusted.apply_subst subst ctx gty in
+ let build_status (pt, _, metasenv, subst) =
+ (* let stamp = Unix.gettimeofday () in *)
+ let metasenv, subst, pt, pty =
+ NCicRefiner.typeof
+ (status#set_coerc_db NCicCoercion.empty_db)
+ metasenv subst ctx pt (Some gty)
+ in
+(* print (lazy (Printf.sprintf "Refined in %fs"
+ (Unix.gettimeofday() -. stamp))); *)
let status = status#set_obj (n,h,metasenv,subst,o) in
- instantiate status goal (mk_cic_term (ctx_of gty) pt)
+ let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
+ let subst = (goal,(gname,ctx,pt,pty)) :: subst in
+ status#set_obj (n,h,metasenv,subst,o)
+ in
+ List.map build_status
+ (NCicParamod.fast_eq_check status metasenv subst ctx
+ eq_cache (NCic.Rel ~-1,gty))
;;
-let fast_eq_check_tac ~params =
- NTactics.distribute_tac (fast_eq_check ~params)
+let fast_eq_check eq_cache status goal =
+ match fast_eq_check_all status eq_cache goal with
+ | [] -> raise (Error (lazy "no proof found",None))
+ | s::_ -> s
;;
-(*************** subsumption ****************)
-module IntSet = Set.Make(struct type t = int let compare = compare end)
-(* exceptions *)
+let dist_fast_eq_check eq_cache s =
+ NTactics.distribute_tac (fast_eq_check eq_cache) s
+;;
-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 auto_eq_check eq_cache status =
+ try
+ let s = dist_fast_eq_check eq_cache status in
+ [s]
+ with
+ | Error _ -> []
;;
-let deps status g =
- let gty = get_sgoalty status g in
- metas_of_term status gty
+(* warning: ctx is supposed to be already instantiated w.r.t subst *)
+let index_local_equations eq_cache status =
+ 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
+ debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+ NCicParamod.forward_infer_step eq_cache t ty
+ with
+ | NCicTypeChecker.TypeCheckerFailure _
+ | NCicTypeChecker.AssertFailure _ -> eq_cache)
+ eq_cache ctx
;;
-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 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 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
+;;
+*)
+
+(*************** subsumption ****************)
+
let close_wrt_context =
List.fold_left
(fun ty ctx_entry ->
;;
*)
+(****************** 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 =
timeout : float;
}
+type cache =
+ {facts : th_cache; (* positive results *)
+ under_inspection : 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 close_failures _ c = c;; *)
(* let prunable _ _ _ = false;; *)
(* 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 init_cache ?(facts=[]) ?(under_inspection=[])
+ ?(unit_eq=NCicParamod.empty_state) _ =
+ {facts = facts;
+ under_inspection = under_inspection;
+ unit_eq = unit_eq
+ }
+
let only _ _ _ = true;;
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 =
+let sort_new_elems l =
+ List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
+
+let try_candidate flags depth status eq_cache t =
try
debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
- 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
+ let status =
+ smart_apply_auto ("",0,t) eq_cache status in
+ (* let status = NTactics.apply_tac ("",0,t) status in *)
+ let og_no = openg_no status in
+ if og_no > flags.maxwidth ||
+ (depth = 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
;;
List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
;;
-let applicative_case depth signature status flags gty cache =
- let tcache,_ = cache in
+let applicative_case depth signature status flags gty (cache:cache) =
+ let tcache = cache.facts in
app_counter:= !app_counter+1;
let candidates = get_candidates status tcache signature gty in
debug_print ~depth
let elems =
List.fold_left
(fun elems cand ->
- match try_candidate flags depth status cand with
+ match try_candidate flags depth status cache.unit_eq cand with
| None -> elems
| Some x -> x::elems)
[] candidates
;;
(* gty is supposed to be meta-closed *)
-let is_subsumed depth status gty (_,cache) =
+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
with Found -> debug_print ~depth (lazy "success");true)
;;
-
-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 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 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
-;;
-
-(* warning: ctx is supposed to be already instantiated w.r.t subst *)
-let index_local_equations eq_cache ctx =
- let c = ref 0 in
- List.fold_left
- (fun cache _ ->
- c:= !c+1;
- let t = NCic.Rel 1 in
- try
- let ty = NCicTypeChecker.typeof [] [] ctx t in
- NCicParamod.forward_infer_step eq_cache t ty
- with
- | NCicTypeChecker.TypeCheckerFailure _
- | NCicTypeChecker.AssertFailure _ -> eq_cache)
- eq_cache ctx
-;;
-
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 ~depth status (tcache,fcache) name =
+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 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 _, 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 tcache = List.fold_left (add_to_th t) tcache keys in
- debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
+ 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, (tcache,[])
+ status, facts
;;
-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 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
+ (* under_inspection must be set to empty *)
+ status, init_cache ~facts ~unit_eq ()
+ | _ -> status, cache
;;
let reduce ~depth status g =
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]])
+ [(!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
- let l1,cache =
- (equational_and_applicative_case
- signature flags status g depth gty cache)
+ (* backward aplications *)
+ let l1 = applicative_case depth signature status flags gty cache in
+ (* fast paramodulation *)
+ let l2 =
+ List.map
+ (fun s ->
+ incr candidate_no;
+ ((!candidate_no,Ast.Ident("__paramod",None)),s))
+ (auto_eq_check cache.unit_eq status)
in
- sort_new_elems (l@l1), cache
+ (* states in l2 have have an set of subgoals: no point to sort them *)
+ l2 @ (sort_new_elems (l@l1)), cache
;;
let pp_goal = function
and
-(* let rec auto_main flags signature cache status k depth = *)
+(* the goals returned upon failure are an unsatisfiable subset
+ of the initial head goals in the stack *)
-auto_main flags signature cache depth status: unit =
+auto_main flags signature (cache:cache) depth status: unit =
debug_print ~depth (lazy "entering auto main");
(* 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 ->
+ | orig::_ ->
+ let branch = List.length(goals)>1 in
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
+ if branch then NTactics.branch_tac status
+ else 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 (ctx_of gty) gty 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 cache then
+ if is_subsumed depth status closegty cache.under_inspection 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 loop_cache =
+ let under_inspection =
+ add_to_th closegty cache.under_inspection closegty in
+ {cache with under_inspection = under_inspection} in
let unsat =
List.fold_left
(* the underscore information does not need to be returned
by do_something *)
- (fun unsat ((_,t),_,_,status,_) ->
+ (fun unsat ((_,t),status) ->
let depth',looping_cache =
- if t=(Ast.Implicit `JustOne) then depth,cache
+ if t=Ast.Ident("__whd",None) then depth,cache
else depth+1, loop_cache in
debug_print (~depth:depth')
(lazy ("Case: " ^ CicNotationPp.pp_term t));
with
| Proved status ->
debug_print (~depth:depth') (lazy "proved");
- if tlg=[] then raise (Proved status)
- else
+ if branch then
let status = NTactics.merge_tac status
- in
- ( (* old cache, here *)
- try auto_clusters flags signature cache
- depth status; assert false
- with Gaveup f ->
- debug_print ~depth
- (lazy ("Unsat1 at depth " ^ (string_of_int depth)
+ in
+ (* old cache, here *)
+ try auto_clusters flags signature cache
+ depth status; assert false
+ 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)
+ IntSet.union f unsat
+ else raise (Proved status)
| Gaveup f ->
debug_print (~depth:depth')
(lazy ("Unsat2 at depth " ^ (string_of_int depth')
unsat)
IntSet.empty alternatives
in
- raise (Gaveup IntSet.add g unsat)
+ raise (Gaveup IntSet.add orig unsat)
;;
let int name l 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 _ = 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;assert false
with
| Gaveup _ -> up_to (x+1) y
| Proved s ->
| (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
print(lazy
projects / helm.git / blobdiff