open Printf
-let debug = ref false
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 ()
+let noprint ?(depth=0) _ = ()
+let debug_print = noprint
open Continuationals.Stack
open NTacStatus
module Ast = CicNotationPt
+
+(* ======================= statistics ========================= *)
+
let app_counter = ref 0
+module RHT = struct
+ type t = NReference.reference
+ let equal = (==)
+ let compare = Pervasives.compare
+ let hash = Hashtbl.hash
+end;;
+
+module RefHash = Hashtbl.Make(RHT);;
+
+type info = {
+ nominations : int ref;
+ uses: int ref;
+}
+
+let statistics: info RefHash.t = RefHash.create 503
+
+let incr_nominations tbl item =
+ try
+ let v = RefHash.find tbl item in incr v.nominations
+ with Not_found ->
+ RefHash.add tbl item {nominations = ref 1; uses = ref 0}
+
+let incr_uses tbl item =
+ try
+ let v = RefHash.find tbl item in incr v.uses
+ with Not_found -> assert false
+
+let toref f tbl t =
+ match t with
+ | Ast.NRef n ->
+ f tbl n
+ | Ast.NCic _ (* local candidate *)
+ | _ -> ()
+
+let is_relevant tbl item =
+ try
+ let v = RefHash.find tbl item in
+ if !(v.nominations) < 60 then true (* not enough info *)
+ else if !(v.uses) = 0 then false
+ else true
+ with Not_found -> true
+
+let print_stat tbl =
+ let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
+ let relevance v = float !(v.uses) /. float !(v.nominations) in
+ let vcompare (_,v1) (_,v2) =
+ Pervasives.compare (relevance v1) (relevance v2) in
+ let l = List.sort vcompare l in
+ let vstring (a,v)=
+ CicNotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
+ (string_of_float (relevance v)) ^
+ "; uses = " ^ (string_of_int !(v.uses)) ^
+ "; nom = " ^ (string_of_int !(v.nominations)) in
+ lazy ("\n\nSTATISTICS:\n" ^
+ String.concat "\n" (List.map vstring l))
+
(* ======================= utility functions ========================= *)
module IntSet = Set.Make(struct type t = int let compare = compare end)
(* 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 branch status ty =
let status, ty, metas = saturate ~delta:0 status ty in
- debug_print (lazy ("saturated ty :" ^ (ppterm status ty)));
+ noprint (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 *)
| NCic.Meta(i,_) -> IntSet.add i acc
| _ -> assert false)
IntSet.empty metas
- in IntSet.subset menv clos;;
+ in
+ (* IntSet.subset menv clos *)
+ IntSet.cardinal(IntSet.diff menv clos)
+
+let is_a_fact status ty = branch status ty = 0
let is_a_fact_obj s uri =
let obj = NCicEnvironment.get_checked_obj uri in
match obj with
- | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
+ | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
is_a_fact s (mk_cic_term [] ty)
(* aggiungere i costruttori *)
| _ -> false
let ctx = ctx_of gty in
open_goal, ctx, gty
+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
+;;
+
+(*************************** height functions ********************************)
+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 ->
+(*
+ 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_goal g status =
+ let ty = get_goalty status g in
+ let context = ctx_of ty in
+ let _, ty = term_of_cic_term status ty (ctx_of ty) in
+ let h = ref (fast_height_of_term ty) in
+ 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;
+ !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 ->
+ h := max !h (height_of_goal open_goal status))
+ open_goals;
+ debug_print (lazy ("altezza sequente: " ^ string_of_int !h));
+ !h
+;;
(* =============================== paramod =========================== *)
-let solve fast status eq_cache goal =
+let solve f 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
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) *)
+ (* 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) *)
+ 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 *)
+ 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)));
with
NCicRefiner.RefineFailure msg
| NCicRefiner.Uncertain msg ->
- debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
- snd (Lazy.force msg))); None
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
+ snd (Lazy.force msg) ^
+ "\n in the environment\n" ^
+ NCicPp.ppmetasenv subst metasenv)); None
| NCicRefiner.AssertFailure msg ->
debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
- Lazy.force msg)); None
+ Lazy.force msg ^
+ "\n in the environment\n" ^
+ NCicPp.ppmetasenv subst metasenv)); 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
+let fast_eq_check eq_cache status (goal:int) =
+ match solve NCicParamod.fast_eq_check status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
let s = dist_fast_eq_check eq_cache status in
[s]
with
- | Error _ -> []
+ | Error _ -> debug_print (lazy ("no paramod proof found"));[]
;;
-(* 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 ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
let c = ref 0 in
List.fold_left
(fun eq_cache _ ->
;;
let paramod eq_cache status goal =
- match solve false status eq_cache goal with
+ match solve NCicParamod.paramod status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
NTactics.distribute_tac (paramod unit_eq) s
;;
+let demod eq_cache status goal =
+ match solve NCicParamod.demod status eq_cache goal with
+ | [] -> raise (Error (lazy "no progress",None))
+ | s::_ -> s
+;;
+
+let demod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (demod unit_eq) s
+;;
+
(*
let fast_eq_check_tac_all ~params eq_cache status =
let g,_,_ = current_goal status in
ctx,ty
;;
-
-
-(* =================================== auto =========================== *)
-(****************** AUTO ********************
-
-let calculate_timeout flags =
- if flags.timeout = 0. then
- (debug_print (lazy "AUTO WITH NO TIMEOUT");
- {flags with timeout = infinity})
- else
- flags
-;;
-let is_equational_case goalty flags =
- let ensure_equational t =
- if is_an_equational_goal t then true
- else false
- in
- (flags.use_paramod && is_an_equational_goal goalty) ||
- (flags.use_only_paramod && ensure_equational goalty)
-;;
-
-type menv = Cic.metasenv
-type subst = Cic.substitution
-type goal = ProofEngineTypes.goal * int * AutoTypes.sort
-let candidate_no = ref 0;;
-type candidate = int * Cic.term Lazy.t
-type cache = AutoCache.cache
-
-type fail =
- (* the goal (mainly for depth) and key of the goal *)
- goal * AutoCache.cache_key
-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 * AutoCache.cache_key * candidate * int
-type elem =
- (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
- menv * subst * int * op list * op list * fail list
-type status =
- (* list of computations that may lead to the solution: all op list will
- * end with the same (S(g,_)) *)
- elem list
-type auto_result =
- (* menv, subst, alternatives, tables, cache *)
- | Proved of menv * subst * elem list * AutomationCache.tables * cache
- | Gaveup of AutomationCache.tables * cache
-
-
-(* the status exported to the external observer *)
-type auto_status =
- (* context, (goal,candidate) list, and_list, history *)
- Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
- (int * Cic.term * int) list * Cic.term Lazy.t list
-
-let d_prefix l =
- let rec aux acc = function
- | (D g)::tl -> aux (acc@[g]) tl
- | _ -> acc
- in
- aux [] l
-;;
-
-let calculate_goal_ty (goalno,_,_) s m =
- try
- let _,cc,goalty = CicUtil.lookup_meta goalno m in
- (* XXX applicare la subst al contesto? *)
- Some (cc, CicMetaSubst.apply_subst s goalty)
- with CicUtil.Meta_not_found i when i = goalno -> None
-;;
-
-let calculate_closed_goal_ty (goalno,_,_) s =
- try
- let cc,_,goalty = List.assoc goalno s in
- (* XXX applicare la subst al contesto? *)
- Some (cc, CicMetaSubst.apply_subst s goalty)
- with Not_found ->
- None
-;;
-
-let pp_status ctx status =
- if debug then
- let names = Utils.names_of_context ctx in
- let pp x =
- let x =
- ProofEngineReduction.replace
- ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
- ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
- in
- CicPp.pp x names
- in
- let string_of_do m s (gi,_,_ as g) d =
- match calculate_goal_ty g s m with
- | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
- | None -> Printf.sprintf "D(%d, _, %d)" gi d
- in
- let string_of_s m su k (ci,ct) gi =
- Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
- in
- let string_of_ol m su l =
- String.concat " | "
- (List.map
- (function
- | D (g,d,s) -> string_of_do m su (g,d,s) d
- | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
- l)
- in
- let string_of_fl m s fl =
- String.concat " | "
- (List.map (fun ((i,_,_),ty) ->
- Printf.sprintf "(%d, %s)" i (pp ty)) fl)
- in
- let rec aux = function
- | [] -> ()
- | (m,s,_,_,ol,fl)::tl ->
- Printf.eprintf "< [%s] ;;; [%s]>\n"
- (string_of_ol m s ol) (string_of_fl m s fl);
- aux tl
- in
- Printf.eprintf "-------------------------- status -------------------\n";
- aux status;
- Printf.eprintf "-----------------------------------------------------\n";
-;;
-
-let auto_status = ref [] ;;
-let auto_context = ref [];;
-let in_pause = ref false;;
-let pause b = in_pause := b;;
-let cond = Condition.create ();;
-let mutex = Mutex.create ();;
-let hint = ref None;;
-let prune_hint = ref [];;
-
-let step _ = Condition.signal cond;;
-let give_hint n = hint := Some n;;
-let give_prune_hint hint =
- prune_hint := hint :: !prune_hint
-;;
-
-let check_pause _ =
- if !in_pause then
- begin
- Mutex.lock mutex;
- Condition.wait cond mutex;
- Mutex.unlock mutex
- end
-;;
-
-let get_auto_status _ =
- let status = !auto_status in
- let and_list,elems,last =
- match status with
- | [] -> [],[],[]
- | (m,s,_,don,gl,fail)::tl ->
- let and_list =
- HExtlib.filter_map
- (fun (id,d,_ as g) ->
- match calculate_goal_ty g s m with
- | Some (_,x) -> Some (id,x,d) | None -> None)
- (d_goals gl)
- in
- let rows =
- (* these are the S goalsin the or list *)
- let orlist =
- List.map
- (fun (m,s,_,don,gl,fail) ->
- HExtlib.filter_map
- (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
- (List.rev don @ gl))
- status
- in
- (* this function eats id from a list l::[id,x] returning x, l *)
- let eat_tail_if_eq id l =
- let rec aux (s, l) = function
- | [] -> s, l
- | ((id1,_,_),k1,c)::tl when id = id1 ->
- (match s with
- | None -> aux (Some c,l) tl
- | Some _ -> assert false)
- | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
- in
- let c, l = aux (None, []) l in
- c, List.rev l
- in
- let eat_in_parallel id l =
- let rec aux (b,eaten, new_l as acc) l =
- match l with
- | [] -> acc
- | l::tl ->
- match eat_tail_if_eq id l with
- | None, l -> aux (b@[false], eaten, new_l@[l]) tl
- | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
- in
- aux ([],[],[]) l
- in
- let rec eat_all rows l =
- match l with
- | [] -> rows
- | elem::or_list ->
- match List.rev elem with
- | ((to_eat,depth,_),k,_)::next_lunch ->
- let b, eaten, l = eat_in_parallel to_eat l in
- let eaten = HExtlib.list_uniq eaten in
- let eaten = List.rev eaten in
- let b = true (* List.hd (List.rev b) *) in
- let rows = rows @ [to_eat,k,b,depth,eaten] in
- eat_all rows l
- | [] -> eat_all rows or_list
- in
- eat_all [] (List.rev orlist)
- in
- let history =
- HExtlib.filter_map
- (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
- gl
- in
-(* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
- and_list, rows, history
- in
- !auto_context, elems, and_list, last
-;;
-
-(* Works if there is no dependency over proofs *)
-let is_a_green_cut goalty =
- CicUtil.is_meta_closed goalty
-;;
-let rec first_s = function
- | (D _)::tl -> first_s tl
- | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
- | [] -> None
-;;
-let list_union l1 l2 =
- (* TODO ottimizzare compare *)
- HExtlib.list_uniq (List.sort compare (l1 @ l1))
-;;
-let rec eq_todo l1 l2 =
- match l1,l2 with
- | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
- | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
- when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
- if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
- | [],[] -> true
- | _ -> false
-;;
-let eat_head todo id fl orlist =
- let rec aux acc = function
- | [] -> [], acc
- | (m, s, _, _, todo1, fl1)::tl as orlist ->
- let rec aux1 todo1 =
- match first_s todo1 with
- | None -> orlist, acc
- | Some (((gno,_,_),_,_,_), todo11) ->
- (* TODO confronto tra todo da ottimizzare *)
- if gno = id && eq_todo todo11 todo then
- aux (list_union fl1 acc) tl
- else
- aux1 todo11
- in
- aux1 todo1
- in
- aux fl orlist
-;;
-let close_proof p ty menv context =
- let metas =
- List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
- in
- let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
- naif_closure p menv context
-;;
-(* XXX capire bene quando aggiungere alla cache *)
-let add_to_cache_and_del_from_orlist_if_green_cut
- g s m cache key todo orlist fl ctx size minsize
-=
- let cache = cache_remove_underinspection cache key in
- (* prima per fare la irl usavamo il contesto vero e proprio e non quello
- * canonico! XXX *)
- match calculate_closed_goal_ty g s with
- | None -> assert false
- | Some (canonical_ctx , gty) ->
- let goalno,depth,sort = g in
- let irl = mk_irl canonical_ctx in
- let goal = Cic.Meta(goalno, irl) in
- let proof = CicMetaSubst.apply_subst s goal in
- let green_proof, closed_proof =
- let b = is_a_green_cut proof in
- if not b then
- b, (* close_proof proof gty m ctx *) proof
- else
- b, proof
- in
- debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
- if is_a_green_cut key then
- (* if the initia goal was closed, we cut alternatives *)
- let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
- let orlist, fl = eat_head todo goalno fl orlist in
- let cache =
- if size < minsize then
- (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
- else
- (* if the proof is closed we cache it *)
- if green_proof then cache_add_success cache key proof
- else (* cache_add_success cache key closed_proof *)
- (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
- in
- cache, orlist, fl, true
- else
- let cache =
- debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
- if size < minsize then
- (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
- (* if the substituted goal and the proof are closed we cache it *)
- if is_a_green_cut gty then
- if green_proof then cache_add_success cache gty proof
- else (* cache_add_success cache gty closed_proof *)
- (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
- else (*
- try
- let ty, _ =
- CicTypeChecker.type_of_aux' ~subst:s
- m ctx closed_proof CicUniv.oblivion_ugraph
- in
- if is_a_green_cut ty then
- cache_add_success cache ty closed_proof
- else cache
- with
- | CicTypeChecker.TypeCheckerFailure _ ->*)
- (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
- in
- cache, orlist, fl, false
-;;
-let close_failures (fl : fail list) (cache : cache) =
- List.fold_left
- (fun cache ((gno,depth,_),gty) ->
- if CicUtil.is_meta_closed gty then
- ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
- cache_add_failure cache gty depth)
- else
- cache)
- cache fl
-;;
-let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
- let entry = goalno, (canonical_ctx, t,ty) in
- assert_subst_are_disjoint subst [entry];
- let subst = entry :: subst in
-
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-
- subst, metasenv
-;;
-
-let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
- None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
-;;
-
-let equational_case
- tables cache depth fake_proof goalno goalty subst context
- flags
-=
- let active,passive,bag = tables in
- let ppterm = ppterm context in
- let status = (fake_proof,goalno) in
- if flags.use_only_paramod then
- begin
- debug_print (lazy ("PARAMODULATION SU: " ^
- string_of_int goalno ^ " " ^ ppterm goalty ));
- let goal_steps, saturation_steps, timeout =
- max_int,max_int,flags.timeout
- in
- match
- Saturation.given_clause bag status active passive
- goal_steps saturation_steps timeout
- with
- | None, active, passive, bag ->
- [], (active,passive,bag), cache, flags
- | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
- passive,bag ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- [(!candidate_no,proof),metasenv,subst,open_goals],
- (active,passive,bag), cache, flags
- end
- else
- begin
- debug_print (lazy ("NARROWING DEL GOAL: " ^
- string_of_int goalno ^ " " ^ ppterm goalty ));
- let goal_steps, saturation_steps, timeout =
- 1,0,flags.timeout
- in
- match
- Saturation.solve_narrowing bag status active passive goal_steps
- with
- | None, active, passive, bag ->
- [], (active,passive,bag), cache, flags
- | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
- passive,bag ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- [(!candidate_no,proof),metasenv,subst,open_goals],
- (active,passive,bag), cache, flags
- end
-(*
- begin
- let params = ([],["use_context","false"]) in
- let automation_cache = {
- AutomationCache.tables = tables ;
- AutomationCache.univ = Universe.empty; }
- in
- try
- let ((_,metasenv,subst,_,_,_),open_goals) =
-
- solve_rewrite ~params ~automation_cache
- (fake_proof, goalno)
- in
- let proof = lazy (Cic.Meta (-1,[])) in
- [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
- with ProofEngineTypes.Fail _ -> [], tables, cache, flags
-(*
- let res = Saturation.all_subsumed bag status active passive in
- let res' =
- List.map
- (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- (!candidate_no,proof),metasenv,subst,open_goals)
- res
- in
- res', (active,passive,bag), cache, flags
-*)
- end
-*)
-;;
-
-let sort_new_elems =
- List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
- let p1 = List.length (prop_only l1) in
- let p2 = List.length (prop_only l2) in
- if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
-;;
-
-
-let try_candidate dbd
- goalty tables subst fake_proof goalno depth context cand
-=
- let ppterm = ppterm context in
- try
- let actives, passives, bag = tables in
- let (_,metasenv,subst,_,_,_), open_goals =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:cand)
- (fake_proof,goalno)
- in
- let tables = actives, passives,
- Equality.push_maxmeta bag
- (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
- in
- debug_print (lazy (" OK: " ^ ppterm cand));
- let metasenv = CicRefine.pack_coercion_metasenv metasenv in
- let open_goals = order_new_goals metasenv subst open_goals ppterm in
- let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
- incr candidate_no;
- Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
- with
- | ProofEngineTypes.Fail s -> None,tables
- | CicUnification.Uncertain s -> None,tables
-;;
-
-let applicative_case dbd
- tables depth subst fake_proof goalno goalty metasenv context
- signature universe cache flags
-=
- (* let goalty_aux =
- match goalty with
- | Cic.Appl (hd::tl) ->
- Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
- | _ -> goalty
- in *)
- let goalty_aux = goalty in
- let candidates =
- get_candidates flags.skip_trie_filtering universe cache goalty_aux
- in
- (* if the goal is an equality we skip the congruence theorems
- let candidates =
- if is_equational_case goalty flags
- then List.filter not_default_eq_term candidates
- else candidates
- in *)
- let candidates = List.filter (only signature context metasenv) candidates
- in
- let tables, elems =
- List.fold_left
- (fun (tables,elems) cand ->
- match
- try_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
- | Some x, tables -> tables, x::elems)
- (tables,[]) candidates
- in
- let elems = sort_new_elems elems in
- elems, tables, cache
-;;
-
-let try_smart_candidate dbd
- goalty tables subst fake_proof goalno depth context cand
-=
- let ppterm = ppterm context in
- try
- let params = ([],[]) in
- let automation_cache = {
- AutomationCache.tables = tables ;
- AutomationCache.univ = Universe.empty; }
- in
- debug_print (lazy ("candidato per " ^ string_of_int goalno
- ^ ": " ^ CicPp.ppterm cand));
-(*
- let (_,metasenv,subst,_,_,_) = fake_proof in
- prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
- prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
-*)
- let ((_,metasenv,subst,_,_,_),open_goals) =
- apply_smart ~dbd ~term:cand ~params ~automation_cache
- (fake_proof, goalno)
- in
- let metasenv = CicRefine.pack_coercion_metasenv metasenv in
- let open_goals = order_new_goals metasenv subst open_goals ppterm in
- let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
- incr candidate_no;
- Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
- with
- | ProofEngineTypes.Fail s -> None,tables
- | CicUnification.Uncertain s -> None,tables
-;;
-
-let smart_applicative_case dbd
- tables depth subst fake_proof goalno goalty metasenv context signature
- universe cache flags
-=
- let goalty_aux =
- match goalty with
- | Cic.Appl (hd::tl) ->
- Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
- | _ -> goalty
- in
- let smart_candidates =
- get_candidates flags.skip_trie_filtering universe cache goalty_aux
- in
- let candidates =
- get_candidates flags.skip_trie_filtering universe cache goalty
- in
- let smart_candidates =
- List.filter
- (fun x -> not(List.mem x candidates)) smart_candidates
- in
- let debug_msg =
- (lazy ("smart_candidates" ^ " = " ^
- (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
- debug_print debug_msg;
- let candidates = List.filter (only signature context metasenv) candidates in
- let smart_candidates =
- List.filter (only signature context metasenv) smart_candidates
- in
-(*
- let penalty cand depth =
- if only signature context metasenv cand then depth else ((prerr_endline (
- "penalizzo " ^ CicPp.ppterm cand));depth -1)
- in
-*)
- let tables, elems =
- List.fold_left
- (fun (tables,elems) cand ->
- match
- try_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables ->
- (* if normal application fails we try to be smart *)
- (match try_smart_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
- | Some x, tables -> tables, x::elems)
- | Some x, tables -> tables, x::elems)
- (tables,[]) candidates
- in
- let tables, smart_elems =
- List.fold_left
- (fun (tables,elems) cand ->
- match
- try_smart_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
- | Some x, tables -> tables, x::elems)
- (tables,[]) smart_candidates
- in
- let elems = sort_new_elems (elems @ smart_elems) in
- elems, tables, cache
-;;
-
-let equational_and_applicative_case dbd
- signature universe flags m s g gty tables cache context
-=
- let goalno, depth, sort = g in
- let fake_proof = mk_fake_proof m s g gty context in
- if is_equational_case gty flags then
- let elems,tables,cache, flags =
- equational_case tables cache
- depth fake_proof goalno gty s context flags
- in
- let more_elems, tables, cache =
- if flags.use_only_paramod then
- [],tables, cache
- else
- applicative_case dbd
- tables depth s fake_proof goalno
- gty m context signature universe cache flags
- in
- elems@more_elems, tables, cache, flags
- else
- let elems, tables, cache =
- 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 dbd tables depth s fake_proof goalno
- gty m context signature universe cache flags
- in
- elems, tables, cache, flags
-;;
-let rec condition_for_hint i = function
- | [] -> false
- | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
- | _::tl -> condition_for_hint i tl
-;;
-let prunable_for_size flags s m todo =
- let rec aux b = function
- | (S _)::tl -> aux b tl
- | (D (_,_,T))::tl -> aux b tl
- | (D g)::tl ->
- (match calculate_goal_ty g s m with
- | None -> aux b tl
- | 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)
- | [] -> b
- in
- aux false todo
-
-(*
-let prunable ty todo =
- let rec aux b = function
- | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
- | (D (_,_,T))::tl -> aux b tl
- | D _::_ -> false
- | [] -> 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*))
- | (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
- | 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
-(*
-(prerr_endline (string_of_int n);
- prerr_endline (CicPp.ppterm gty);
- prerr_endline (CicPp.ppterm gty');
- prerr_endline "---------- subst";
- prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
- prerr_endline "---------- variant";
- prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
- prerr_endline "---------- menv";
- prerr_endline (CicMetaSubst.ppmetasenv [] menv);
- no_progress variant tl) *)
- else false))
- | _::tl -> no_progress variant tl
- in
- aux todo
-
-;;
-let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
- let s =
- HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
- in
- List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
-;;
-let filter_prune_hint c l =
- let prune = !prune_hint in
- prune_hint := []; (* possible race... *)
- if prune = [] then c,l
- else
- cache_reset_underinspection c,
- List.filter (condition_for_prune_hint prune) l
-;;
-
-
-
-let
- auto_all_solutions dbd tables universe cache context metasenv gl flags
-=
- let signature =
- List.fold_left
- (fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
- )
- MetadataConstraints.UriManagerSet.empty gl
- in
- let goals = order_new_goals metasenv [] gl CicPp.ppterm in
- let goals =
- List.map
- (fun (x,s) -> D (x,flags.maxdepth,s)) goals
- in
- let elems = [metasenv,[],1,[],goals,[]] in
- let rec aux tables solutions cache elems flags =
- match auto_main dbd tables context flags signature universe cache elems with
- | Gaveup (tables,cache) ->
- solutions,cache, tables
- | Proved (metasenv,subst,others,tables,cache) ->
- if Unix.gettimeofday () > flags.timeout then
- ((subst,metasenv)::solutions), cache, tables
- else
- aux tables ((subst,metasenv)::solutions) cache others flags
- in
- let rc = aux tables [] cache elems flags in
- match rc with
- | [],cache,tables -> [],cache,tables
- | solutions, cache,tables ->
- let solutions =
- HExtlib.filter_map
- (fun (subst,newmetasenv) ->
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
- in
- if opened = [] then Some subst else None)
- solutions
- in
- solutions,cache,tables
-;;
-
-(******************* AUTO ***************)
-
-
-let auto dbd flags metasenv tables universe cache context metasenv gl =
- let initial_time = Unix.gettimeofday() in
- let signature =
- List.fold_left
- (fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
- )
- MetadataConstraints.UriManagerSet.empty gl
- in
- let goals = order_new_goals metasenv [] gl CicPp.ppterm in
- let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
- let elems = [metasenv,[],1,[],goals,[]] in
- match auto_main dbd tables context flags signature universe cache elems with
- | Proved (metasenv,subst,_, tables,cache) ->
- debug_print(lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- Some (subst,metasenv), cache
- | Gaveup (tables,cache) ->
- debug_print(lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- None,cache
-;;
-
-let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
- let flags = flags_of_params params () in
- let use_library = flags.use_library in
- let universe, tables, cache =
- init_cache_and_tables
- ~dbd ~use_library ~use_context:(not flags.skip_context)
- automation_cache univ (proof, goal)
- in
- let _,metasenv,subst,_,_, _ = proof in
- let _,context,goalty = CicUtil.lookup_meta goal metasenv in
- let signature = MetadataQuery.signature_of metasenv goal in
- let signature =
- 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)
- )
- signature univ
- in
- let tables,cache =
- if flags.close_more then
- close_more
- tables context (proof, goal)
- (auto_all_solutions dbd) signature universe cache
- else tables,cache in
- let initial_time = Unix.gettimeofday() in
- let (_,oldmetasenv,_,_,_, _) = proof in
- hint := None;
- let elem =
- metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
- in
- match auto_main dbd tables context flags signature universe cache [elem] with
- | Proved (metasenv,subst,_, tables,cache) ->
- debug_print (lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- let proof,metasenv =
- ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goal subst metasenv
- in
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:metasenv
- in
- proof,opened
- | Gaveup (tables,cache) ->
- debug_print
- (lazy ("TIME:"^
- string_of_float(Unix.gettimeofday()-.initial_time)));
- raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
-;;
-*)
-
(****************** smart application ********************)
+let saturate_to_ref metasenv subst ctx nref ty =
+ let height = height_of_ref nref in
+ let rec aux metasenv ty args =
+ let ty,metasenv,moreargs =
+ NCicMetaSubst.saturate ~delta:height metasenv subst ctx ty 0 in
+ match ty with
+ | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
+ when nre<>nref ->
+ let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
+ aux metasenv bo (args@moreargs)
+ | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
+ when nre<>nref ->
+ let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
+ aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
+ | _ -> ty,metasenv,(args@moreargs)
+ in
+ aux metasenv ty []
let smart_apply t unit_eq status g =
let n,h,metasenv,subst,o = status#obj 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 _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in
- let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in
+ let ty,metasenv,args =
+ match gty with
+ | NCic.Const(nref)
+ | NCic.Appl(NCic.Const(nref)::_) ->
+ saturate_to_ref metasenv subst ctx nref ty
+ | _ ->
+ 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 pterm = if args=[] then t else
+ match t with
+ | NCic.Appl l -> NCic.Appl(l@args)
+ | _ -> NCic.Appl(t::args)
+ in
+ noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+ noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
let eq_coerc =
let uri =
NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
fast_eq_check unit_eq status j
with
+ | NCicEnvironment.ObjectNotFound s as e ->
+ raise (Error (lazy "eq_coerc non yet defined",Some e))
| Error _ as e -> debug_print (lazy "error"); raise e
let smart_apply_tac t s =
type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
-let keys_of_term status t =
- let status, orig_ty = typeof status (ctx_of t) t in
+(* cartesian: term set list -> term list set *)
+let rec cartesian =
+ function
+ [] -> NDiscriminationTree.TermListSet.empty
+ | [l] ->
+ NDiscriminationTree.TermSet.fold
+ (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
+ | he::tl ->
+ let rest = cartesian tl in
+ NDiscriminationTree.TermSet.fold
+ (fun x acc ->
+ NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
+ ) he NDiscriminationTree.TermListSet.empty
+;;
+
+(* all_keys_of_cic_type: term -> term set *)
+let all_keys_of_cic_type metasenv subst context ty =
+ let saturate ty =
+ (* Here we are dropping the metasenv, but this should not raise any
+ exception (hopefully...) *)
+ let ty,_,hyps =
+ NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0
+ in
+ ty,List.length hyps
+ in
+ let rec aux ty =
+ match ty with
+ NCic.Appl (he::tl) ->
+ let tl' =
+ List.map (fun ty ->
+ let wty = NCicReduction.whd ~delta:0 ~subst context ty in
+ if ty = wty then
+ NDiscriminationTree.TermSet.add ty (aux ty)
+ else
+ NDiscriminationTree.TermSet.union
+ (NDiscriminationTree.TermSet.add ty (aux ty))
+ (NDiscriminationTree.TermSet.add wty (aux wty))
+ ) tl
+ in
+ NDiscriminationTree.TermListSet.fold
+ (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
+ (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
+ NDiscriminationTree.TermSet.empty
+ | _ -> NDiscriminationTree.TermSet.empty
+ in
+ let ty,ity = saturate ty in
+ let wty,iwty = saturate (NCicReduction.whd ~delta:0 ~subst context ty) in
+ if ty = wty then
+ [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
+ else
+ [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
+ iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
+;;
+
+let all_keys_of_type status t =
+ let _,_,metasenv,subst,_ = status#obj in
+ let context = ctx_of t in
+ let status, t = apply_subst status context t in
+ let keys =
+ all_keys_of_cic_type metasenv subst context
+ (snd (term_of_cic_term status t context))
+ in
+ status,
+ List.map
+ (fun (intros,keys) ->
+ intros,
+ NDiscriminationTree.TermSet.fold
+ (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
+ keys Ncic_termSet.empty
+ ) keys
+;;
+
+
+let keys_of_type status orig_ty =
+ (* Here we are dropping the metasenv (in the status), but this should not
+ raise any exception (hopefully...) *)
let _, ty, _ = saturate ~delta:max_int status orig_ty in
- let keys = [ty] in
+ let _, ty = apply_subst status (ctx_of ty) ty in
+ let keys =
+(*
+ let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
+ if orig_ty' <> orig_ty then
+ let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
+ [ty;ty']
+ else
+ [ty]
+*)
+ [ty] in
+(*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
let keys =
let _, ty = term_of_cic_term status ty (ctx_of ty) in
match ty with
status, keys
;;
+let all_keys_of_term status t =
+ let status, orig_ty = typeof status (ctx_of t) t in
+ all_keys_of_type status orig_ty
+;;
+
+let keys_of_term status t =
+ let status, orig_ty = typeof status (ctx_of t) t in
+ keys_of_type status orig_ty
+;;
+
let mk_th_cache status gl =
List.fold_left
(fun (status, acc) g ->
| [] -> (* Ncic_termSet.elements *) acc
| (_::tl) as k ->
try
- let idx = List.assq k th in
+ let idx = List.assoc(*q*) k th in
let acc = Ncic_termSet.union acc
(InvRelDiscriminationTree.retrieve_unifiables idx gty)
in
type flags = {
do_types : bool; (* solve goals in Type *)
last : bool; (* last goal: take first solution only *)
+ candidates: Ast.term list option;
maxwidth : int;
maxsize : int;
maxdepth : int;
type cache =
{facts : th_cache; (* positive results *)
under_inspection : cic_term list * th_cache; (* to prune looping *)
- unit_eq : NCicParamod.state
+ unit_eq : NCicParamod.state;
+ trace: Ast.term list
}
+let add_to_trace ~depth cache t =
+ match t with
+ | Ast.NRef _ ->
+ debug_print ~depth (lazy ("Adding to trace: " ^ CicNotationPp.pp_term t));
+ {cache with trace = t::cache.trace}
+ | Ast.NCic _ (* local candidate *)
+ | _ -> (*not an application *) cache
+
+let pptrace tr =
+ (lazy ("Proof Trace: " ^ (String.concat ";"
+ (List.map CicNotationPp.pp_term tr))))
+(* not used
+let remove_from_trace cache t =
+ match t with
+ | Ast.NRef _ ->
+ (match cache.trace with
+ | _::tl -> {cache with trace = tl}
+ | _ -> assert false)
+ | Ast.NCic _ (* local candidate *)
+ | _ -> (*not an application *) cache *)
+
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
-
-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;
- debug_print ("altezza sequente: " ^ string_of_int !h);
- !h
-;;
+exception Proved of NTacStatus.tac_status * Ast.term list
(* let close_failures _ c = c;; *)
(* let prunable _ _ _ = false;; *)
(* let cache_add_underinspection c _ _ = c;; *)
let init_cache ?(facts=[]) ?(under_inspection=[],[])
- ?(unit_eq=NCicParamod.empty_state) _ =
+ ?(unit_eq=NCicParamod.empty_state)
+ ?(trace=[])
+ _ =
{facts = facts;
under_inspection = under_inspection;
- unit_eq = unit_eq
- }
+ unit_eq = unit_eq;
+ trace = trace}
-let only signature _context candidate =
+let only signature _context candidate = true
+(*
(* TASSI: nel trie ci mettiamo solo il body, non il ty *)
let candidate_ty =
NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
~metasenv:[] candidate ^ ": " ^ string_of_int height));
- rc
+ rc *)
;;
let candidate_no = ref 0;;
let openg_no status = List.length (head_goals status#stack)
+let sort_candidates status ctx candidates =
+ let _,_,metasenv,subst,_ = status#obj in
+ let branch cand =
+ let status,ct = disambiguate status ctx ("",0,cand) None in
+ let status,t = term_of_cic_term status ct ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let res = branch status (mk_cic_term ctx ty) in
+ debug_print (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
+ ^ (string_of_int res)));
+ res
+ in
+ let candidates = List.map (fun t -> branch t,t) candidates in
+ let candidates =
+ List.sort (fun (a,_) (b,_) -> a - b) candidates in
+ let candidates = List.map snd candidates in
+ debug_print (lazy ("candidates =\n" ^ (String.concat "\n"
+ (List.map CicNotationPp.pp_term candidates))));
+ candidates
+
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 =
+let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
try
- debug_print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
+ 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
+ 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))
+ else *)
+ (* useless
+ let status, cict = disambiguate status ctx ("",0,t) None in
+ let status,ct = term_of_cic_term status cict ctx in
+ let _,_,metasenv,subst,_ = status#obj in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx ct in
+ let res = branch status (mk_cic_term ctx ty) in
+ if smart=1 && og_no > res then
+ (print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
+ ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
+ print ~depth (lazy "strange application"); None)
+ else *)
+ (incr candidate_no;
+ Some ((!candidate_no,t),status))
with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
;;
+let sort_of subst metasenv ctx t =
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let metasenv',ty = NCicUnification.fix_sorts metasenv subst ty in
+ assert (metasenv = metasenv');
+ NCicTypeChecker.typeof subst metasenv ctx ty
+;;
+
+let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
+;;
+
+let perforate_small subst metasenv context t =
+ let rec aux = function
+ | NCic.Appl (hd::tl) ->
+ let map t =
+ let s = sort_of subst metasenv context t in
+ match s with
+ | NCic.Sort(NCic.Type [`Type,u])
+ when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
+ | _ -> aux t
+ in
+ NCic.Appl (hd::List.map map tl)
+ | t -> t
+ in
+ aux t
+;;
+
+let get_cands retrieve_for diff empty gty weak_gty =
+ let cands = retrieve_for gty in
+ match weak_gty with
+ | None -> cands, empty
+ | Some weak_gty ->
+ let more_cands = retrieve_for weak_gty in
+ cands, diff more_cands cands
+;;
+
+let get_candidates ?(smart=true) depth flags status cache signature gty =
+ let maxd = ((depth + 1) = flags.maxdepth) in
+ let universe = status#auto_cache in
+ let _,_,metasenv,subst,_ = status#obj in
+ let context = ctx_of gty in
+ let _, raw_gty = term_of_cic_term status gty context in
+ let raw_weak_gty, weak_gty =
+ if smart then
+ match raw_gty with
+ | NCic.Appl _
+ | NCic.Const _
+ | NCic.Rel _ ->
+ let weak = perforate_small subst metasenv context raw_gty in
+ Some weak, Some (mk_cic_term context weak)
+ | _ -> None,None
+ else None,None
+ in
+ let global_cands, smart_global_cands =
+ match flags.candidates with
+ | Some l when (not maxd) -> l,[]
+ | Some _
+ | None ->
+ let mapf s =
+ let to_ast = function
+ | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r)
+ | NCic.Const _ -> None
+ | _ -> assert false in
+ HExtlib.filter_map
+ to_ast (NDiscriminationTree.TermSet.elements s) in
+ let g,l =
+ get_cands
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe)
+ NDiscriminationTree.TermSet.diff
+ NDiscriminationTree.TermSet.empty
+ raw_gty raw_weak_gty in
+ mapf g, mapf l in
+ let local_cands,smart_local_cands =
+ let mapf s =
+ let to_ast t =
+ let _status, t = term_of_cic_term status t context
+ in Ast.NCic t in
+ List.map to_ast (Ncic_termSet.elements s) in
+ let g,l =
+ get_cands
+ (fun ty -> search_in_th ty cache)
+ Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
+ mapf g, mapf l in
+ sort_candidates status context (global_cands@local_cands),
+ sort_candidates status context (smart_global_cands@smart_local_cands)
+;;
+
+(* old version
let get_candidates ?(smart=true) status cache signature gty =
let universe = status#auto_cache in
+ let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let t_ast t =
let _status, t = term_of_cic_term status t context
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 keys = all_keys_of_cic_term metasenv subst context raw_gty in
+ (* we only keep those keys that do not require any intros for now *)
+ let no_intros_keys = snd (List.hd keys) in
+ let cands =
+ NDiscriminationTree.TermSet.fold
+ (fun ty acc ->
+ NDiscriminationTree.TermSet.union acc
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe ty)
+ ) no_intros_keys NDiscriminationTree.TermSet.empty in
+(* old code:
let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe raw_gty in
+ universe raw_gty in
+*)
+ let local_cands =
+ NDiscriminationTree.TermSet.fold
+ (fun ty acc ->
+ Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache)
+ ) no_intros_keys Ncic_termSet.empty in
+(* old code:
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 =
+ 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 candidates = together cands local_cands in
+ let candidates = sort_candidates status context candidates in
let smart_candidates =
if smart then
match raw_gty with
- | NCic.Appl (hd::tl) ->
- let weak_gty =
+ | NCic.Appl _
+ | NCic.Const _
+ | NCic.Rel _ ->
+ let weak_gty = perforate_small subst metasenv context raw_gty in
+ (*
NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
- (List.length tl)) in
+ (List.length tl)) in *)
let more_cands =
- NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe weak_gty in
+ 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 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
+ together smart_cands smart_local_cands
+ (* together more_cands more_local_cands *)
| _ -> []
else []
in
- candidates, smart_candidates
-;;
+ let smart_candidates = sort_candidates status context smart_candidates in
+ (* if smart then smart_candidates, []
+ else candidates, [] *)
+ candidates, smart_candidates
+;;
+
+let get_candidates ?(smart=true) flags status cache signature gty =
+ match flags.candidates with
+ | None -> get_candidates ~smart status cache signature gty
+ | Some l -> l,[]
+;; *)
-let applicative_case depth signature status flags gty (cache:cache) =
+let applicative_case depth signature status flags gty cache =
app_counter:= !app_counter+1;
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let tcache = cache.facts in
- let is_eq =
+ let is_prod, is_eq =
let status, t = term_of_cic_term status gty context in
- NCicParamod.is_equation metasenv subst context t
+ let t = NCicReduction.whd subst context t in
+ match t with
+ | NCic.Prod _ -> true, false
+ | _ -> false, NCicParamod.is_equation metasenv subst context t
in
- debug_print(lazy (string_of_bool is_eq));
+ debug_print~depth (lazy (string_of_bool is_eq));
+ (* old
+ let candidates, smart_candidates =
+ get_candidates ~smart:(not is_eq) depth
+ flags status tcache signature gty in
+ (* if the goal is an equation we avoid to apply unit equalities,
+ since superposition should take care of them; refl is an
+ exception since it prompts for convertibility *)
+ let candidates =
+ let test x = not (is_a_fact_ast status subst metasenv context x) in
+ if is_eq then
+ Ast.Ident("refl",None) ::List.filter test candidates
+ else candidates in *)
+ (* new *)
let candidates, smart_candidates =
- get_candidates ~smart:(not is_eq) status tcache signature gty in
+ get_candidates ~smart:true depth
+ flags status tcache signature gty in
+ (* if the goal is an equation we avoid to apply unit equalities,
+ since superposition should take care of them; refl is an
+ exception since it prompts for convertibility *)
+ let candidates,smart_candidates =
+ let test x = not (is_a_fact_ast status subst metasenv context x) in
+ if is_eq then
+ Ast.Ident("refl",None) ::List.filter test candidates,
+ List.filter test smart_candidates
+ else candidates,smart_candidates in
debug_print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
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
(fun elems cand ->
if (only_one && (elems <> [])) then elems
else
- if (maxd && not(is_a_fact_ast status subst metasenv context cand))
+ if (maxd && not(is_prod) &
+ 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
+ flags depth status cache.unit_eq context cand with
| None -> elems
| Some x -> x::elems)
[] candidates
(fun elems cand ->
if (only_one && (elems <> [])) then elems
else
- if (maxd && not(is_a_fact_ast status subst metasenv context cand))
+ if (maxd && not(is_prod) &&
+ 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
+ flags depth status cache.unit_eq context cand with
| None -> elems
| Some x -> x::elems)
[] smart_candidates
let is_prod status =
let _, ctx, gty = current_goal status in
+ let status, gty = apply_subst status ctx gty 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
+ | NCic.Prod (name,src,_) ->
+ let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
+ (match snd (term_of_cic_term status src ctx) with
+ | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
+ | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
+ let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys r in
+ (match itys with
+ (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
+ | [_,_,_,[_]]
+ | [_,_,_,[]] -> `Inductive (guess_name name ctx)
+ | _ -> `Some (guess_name name ctx))
+ | _ -> `Some (guess_name name ctx))
+ | _ -> `None
let intro ~depth status facts name =
let status = NTactics.intro_tac name status in
;;
let rec intros_facts ~depth status facts =
+ if List.length (head_goals status#stack) <> 1 then status, facts else
match is_prod status with
- | Some(name) ->
+ | `Inductive name
+ | `Some(name) ->
let status,facts =
intro ~depth status facts name
- in intros_facts ~depth status facts
+ in intros_facts ~depth status facts
+(* | `Inductive name ->
+ let status = NTactics.case1_tac name status in
+ intros_facts ~depth status facts *)
| _ -> status, facts
;;
-let rec intros ~depth status (cache:cache) =
+let intros ~depth status cache =
match is_prod status with
- | Some _ ->
+ | `Inductive _
+ | `Some _ ->
+ let trace = cache.trace in
let status,facts =
intros_facts ~depth status cache.facts
in
+ if head_goals status#stack = [] then
+ let status = NTactics.merge_tac status in
+ [(0,Ast.Ident("__intros",None)),status], cache
+ else
(* 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 unit_eq = index_local_equations status#eq_cache status in
+ let status = NTactics.merge_tac status in
+ [(0,Ast.Ident("__intros",None)),status],
+ init_cache ~facts ~unit_eq () ~trace
+ | _ -> [],cache
;;
-let reduce ~depth status g =
+let reduce ~whd ~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
+ let ty' =
+ (if whd then NCicReduction.whd else NCicTacReduction.normalize) ~subst ctx ty
+ in
if ty = ty' then []
else
(debug_print ~depth
;;
let do_something signature flags status g depth gty cache =
+ let l0, cache = intros ~depth status cache in
+ if l0 <> [] then l0, cache
+ else
(* whd *)
- let l = reduce ~depth status g in
+ let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in
+ (* if l <> [] then l,cache else *)
(* backward aplications *)
let l1 =
List.map
(auto_eq_check cache.unit_eq status)
in
let l2 =
- (* if (l1 <> []) then [] else *)
+ if ((l1 <> []) && flags.last) then [] else
applicative_case depth signature status flags gty cache
- (* fast paramodulation *)
in
+ (* statistics *)
+ List.iter
+ (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
(* 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
+ (* l1 @ (sort_new_elems (l @ l2)), cache *)
+ l1 @ (List.rev l2) @ l, cache
;;
let pp_goal = function
| (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 *)
- (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
+ in
+ (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
in
let gstatus =
let f,o,s = slice level status#stack in f@o@s
status#set_stack gstatus
;;
-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 stack_goals level gs =
+ if level = 0 then []
+ else match gs with
+ | [] -> assert false
+ | (g,_,_,_)::s ->
+ let is_open = function
+ | (_,Continuationals.Stack.Open i) -> Some i
+ | (_,Continuationals.Stack.Closed _) -> None
+ in
+ HExtlib.filter_map is_open g @ stack_goals (level-1) s
;;
+let open_goals level status = stack_goals level status#stack
+;;
+
+let move_to_side level status =
+match status#stack with
+ | [] -> assert false
+ | (g,_,_,_)::tl ->
+ let is_open = function
+ | (_,Continuationals.Stack.Open i) -> Some i
+ | (_,Continuationals.Stack.Closed _) -> None
+ in
+ let others = menv_closure status (stack_goals (level-1) tl) in
+ List.for_all (fun i -> IntSet.mem i others)
+ (HExtlib.filter_map is_open g)
+
let rec auto_clusters ?(top=false)
flags signature cache depth status : unit =
debug_print ~depth (lazy ("entering auto clusters at depth " ^
(string_of_int depth)));
+ debug_print ~depth (pptrace cache.trace);
(* ignore(Unix.select [] [] [] 0.01); *)
let status = clean_up_tac status in
let goals = head_goals status#stack in
if goals = [] then
- if depth = 0 then raise (Proved status)
+ if depth = 0 then raise (Proved (status, cache.trace))
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
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache *)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
+ auto_clusters flags signature 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 all_goals)));
let classes = HExtlib.clusters (deps status) all_goals in
+ List.iter
+ (fun gl ->
+ if List.length gl > flags.maxwidth then
+ (debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
+ raise (Gaveup IntSet.empty))
+ else ()) classes;
+ if List.length classes = 1 then
+ let flags =
+ {flags with last = (List.length all_goals = 1)} in
+ (* no need to cluster *)
+ auto_main flags signature cache depth status
+ else
let classes = if top then List.rev classes else classes in
debug_print ~depth
(lazy
(fun l ->
("cluster:" ^ String.concat "," (List.map string_of_int l)))
classes)));
- let status,b =
+ let status,trace,b =
List.fold_left
- (fun (status,b) gl ->
+ (fun (status,trace,b) gl ->
+ let cache = {cache with trace = trace} in
+ let flags =
+ {flags with last = (List.length gl = 1)} in
let lold = List.length status#stack in
debug_print ~depth (lazy ("stack length = " ^
(string_of_int lold)));
String.concat "," (List.map string_of_int gl)));
auto_main flags signature cache depth fstatus; assert false
with
- | Proved(status) ->
+ | Proved(status,trace) ->
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,trace,true)
+ | Gaveup _ when top -> (status,trace,b)
)
- (status,false) classes
+ (status,cache.trace,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)
+ in if b then raise (Proved(status,trace)) else raise (Gaveup IntSet.empty)
and
(* BRAND NEW VERSION *)
-auto_main flags signature (cache:cache) depth status: unit =
+auto_main flags signature cache depth status: unit =
debug_print ~depth (lazy "entering auto main");
+ debug_print ~depth (pptrace cache.trace);
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
- | [] when depth = 0 -> raise (Proved status)
+ | [] when depth = 0 -> raise (Proved (status,cache.trace))
| [] ->
let status = NTactics.merge_tac status in
let cache =
let l,tree = cache.under_inspection in
match l with
- | [] -> assert false
+ | [] -> cache (* possible because of intros that cleans the cache *)
| 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
+ auto_clusters flags signature cache (depth-1) status
| orig::_ ->
- let ng = List.length goals in
+ if depth > 0 && move_to_side depth status
+ then
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache*)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
+ auto_clusters flags signature cache (depth-1) status
+ else
+ let ng = List.length goals in
+ (* moved inside auto_clusters *)
if ng > flags.maxwidth then
- (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
- else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
- else
+ (print ~depth (lazy "FAIL LOCAL 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
if is_subsumed depth status closegty (snd cache.under_inspection) then
(debug_print ~depth (lazy "SUBSUMED");
raise (Gaveup IntSet.add g IntSet.empty))
- else
- let do_flags =
- {flags with last = flags.last && ng=1} in
+ else
+ let new_sig = height_of_goal g status in
+ if new_sig < signature then
+ (debug_print (lazy ("news = " ^ (string_of_int new_sig)));
+ debug_print (lazy ("olds = " ^ (string_of_int signature))));
let alternatives, cache =
- do_something signature do_flags status g depth gty cache in
+ do_something signature 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
List.iter
(fun ((_,t),status) ->
debug_print ~depth
- (lazy("(re)considering goal " ^
+ (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
+ if t=Ast.Ident("__whd",None) ||
+ t=Ast.Ident("__intros",None)
+ then depth, cache
else depth+1,loop_cache in
+ let cache = add_to_trace ~depth cache t in
try
- auto_clusters flags signature (cache:cache) depth status
+ auto_clusters flags signature cache depth status
with Gaveup _ ->
- debug_print ~depth (lazy "Failed");())
+ debug_print ~depth (lazy "Failed");
+ ())
alternatives;
- raise (Gaveup IntSet.empty)
+ raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty)
;;
let int name l def =
with Failure _ | Not_found -> def
;;
-let auto_tac ~params:(_univ,flags) status =
+module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
+
+let cleanup_trace s trace =
+ (* removing duplicates *)
+ let trace_set =
+ List.fold_left
+ (fun acc t -> AstSet.add t acc)
+ AstSet.empty trace in
+ let trace = AstSet.elements trace_set
+ (* filtering facts *)
+ in List.filter
+ (fun t ->
+ match t with
+ | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
+ | _ -> false) trace
+;;
+
+let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let oldstatus = status in
let status = (status:> NTacStatus.tac_status) in
let goals = head_goals status#stack in
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
+ let cache = init_cache ~facts ~unit_eq () in
(* pp_th status facts; *)
(*
NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
(NDiscriminationTree.TermSet.elements t))
)));
*)
+ let candidates =
+ match univ with
+ | None -> None
+ | Some l ->
+ let to_Ast t =
+ let status, res = disambiguate status [] t None in
+ let _,res = term_of_cic_term status res (ctx_of res)
+ in Ast.NCic res
+ in Some (List.map to_Ast l)
+ in
let depth = int "depth" flags 3 in
let size = int "size" flags 10 in
let width = int "width" flags 4 (* (3+List.length goals)*) in
let signature = height_of_goals status in
let flags = {
last = true;
+ candidates = candidates;
maxwidth = width;
maxsize = size;
maxdepth = depth;
*)
with
| Gaveup _ -> up_to (x+1) y
- | Proved s ->
+ | Proved (s,trace) ->
debug_print (lazy ("proved at depth " ^ string_of_int x));
+ List.iter (toref incr_uses statistics) trace;
+ let trace = cleanup_trace s trace in
+ let _ = debug_print (pptrace trace) in
let stack =
match s#stack with
| (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
| _ -> assert false
in
let s = s#set_stack stack in
+ trace_ref := trace;
oldstatus#set_status s
in
let s = up_to depth depth in
+ debug_print (print_stat statistics);
debug_print(lazy
("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
debug_print(lazy
projects / helm.git / blobdiff