X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=323777d18846e895eabfcaaeff3ae7e3e6c2ecfa;hb=4c4228417fc38e71bce647174d175561db2afb01;hp=827c1dc46f06a67146cf6d3b1a053971776231bf;hpb=0232b651c37511743ce9e99d517a41adac3a7064;p=helm.git diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 827c1dc46..323777d18 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -11,70 +11,67 @@ 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_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 -(* =================================== 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) -;; +module RHT = struct + type t = NReference.reference + let equal = (==) + let compare = Pervasives.compare + let hash = Hashtbl.hash +end;; -let auto_paramod_tac ~params status = - NTactics.distribute_tac (auto_paramod ~params) status -;; +module RefHash = Hashtbl.Make(RHT);; -let fast_eq_check ~params status goal = - let gty = get_goalty status goal in - 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 status = status#set_obj (n,h,metasenv,subst,o) in - instantiate status goal (mk_cic_term (ctx_of gty) pt) -;; +type info = { + nominations : int ref; + uses: int ref; +} -let fast_eq_check_tac ~params = - NTactics.distribute_tac (fast_eq_check ~params) -;; +let statistics: info RefHash.t = RefHash.create 503 -(*************** subsumption ****************) +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 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.NRef a) ^ ": rel = " ^ + (string_of_float (relevance v)) ^ + "; uses = " ^ (string_of_int !(v.uses)) in + lazy (String.concat "\n" (List.map vstring l)) + +(* ======================= 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 @@ -101,10 +98,267 @@ let menv_closure status gl = in closure IntSet.empty gl ;; +(* we call a "fact" an object whose hypothesis occur in the goal + or in types of goal-variables *) +let branch status ty = + let status, ty, metas = saturate ~delta:0 status ty in + 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 *) + 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 *) + 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(_,_,_,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 + +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 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_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 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 + 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 + 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))); + 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\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 ^ + "\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 NCicParamod.fast_eq_check 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 NCicParamod.paramod 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 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 + 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) ;; @@ -113,9 +367,9 @@ let args_for_context ?(k=1) ctx = let _,args = List.fold_left (fun (n,l) ctx_entry -> - match ctx_entry with - | name, NCic.Decl t -> n+1,NCic.Rel(n)::l - | name, NCic.Def(bo, _) -> n+1,l) + 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 @@ -135,11 +389,11 @@ let refresh metasenv = (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 @@ -151,24 +405,24 @@ let close_metasenv metasenv subst = 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 ;; @@ -183,13 +437,13 @@ let ground_instances status gl = 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 @@ -200,11 +454,11 @@ let replace_meta i args target = let rec aux k = function (* TODO: local context *) | NCic.Meta (j,lc) when i = j -> - (match args with - | [] -> NCic.Rel 1 - | _ -> let args = - List.map (NCicSubstitution.subst_meta lc) args in - NCic.Appl(NCic.Rel k::args)) + (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 @@ -223,8 +477,8 @@ let close_wrt_metasenv subst = (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 @@ -254,884 +508,174 @@ let close status g = ctx,ty ;; +(****************** smart application ********************) - -(* =================================== 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 +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 ty (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 - 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 -;; + aux metasenv ty [] -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 +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 _,_,metasenv,subst,_ = status#obj in + let ty = NCicTypeChecker.typeof subst metasenv ctx t 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 + match t with + | NCic.Appl l -> NCic.Appl(l@args) + | _ -> NCic.Appl(t::args) 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) + 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 + let ref = NReference.reference_of_spec uri (NReference.Def(2)) in + NCic.Const ref 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 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 mk_fake_proof metasenv subst (goalno,_,_) goalty context = - None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] -;; +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 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) = +let smart_apply_auto t eq_cache = + NTactics.distribute_tac (smart_apply t eq_cache) - 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) -;; +(****************** types **************) -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 -;; +type th_cache = (NCic.context * InvRelDiscriminationTree.t) list -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 +(* 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 - 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 + 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 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 all_keys_of_type status t = + let _,_,metasenv,subst,_ = status#obj in + let context = ctx_of 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 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 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 = (* -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")) -;; + 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] *) - -(****************** types **************) -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 - let _, ty, _ = saturate ~delta:max_int status orig_ty in - let keys = [ty] in + [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 - | 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 @@ -1140,6 +684,16 @@ let keys_of_term status t = 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 -> @@ -1153,8 +707,8 @@ let mk_th_cache status gl = 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 @@ -1181,6 +735,19 @@ let add_to_th t c ty = 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 -> @@ -1202,7 +769,7 @@ let pp_th status = 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 @@ -1217,12 +784,42 @@ let search_in_th gty th = 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; timeout : float; } +type cache = + {facts : th_cache; (* positive results *) + under_inspection : cic_term list * th_cache; (* to prune looping *) + 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 @@ -1230,7 +827,7 @@ type candidate = int * Ast.term (* unique candidate number, candidate *) 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 * Ast.term list (* let close_failures _ c = c;; *) (* let prunable _ _ _ = false;; *) @@ -1238,71 +835,325 @@ exception Proved of #NTacStatus.tac_status (* let put_in_subst s _ _ _ = s;; *) (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *) (* let cache_add_underinspection c _ _ = c;; *) -let equational_case _ _ _ _ _ _ = [];; -let only _ _ _ = true;; + +let init_cache ?(facts=[]) ?(under_inspection=[],[]) + ?(unit_eq=NCicParamod.empty_state) + ?(trace=[]) + _ = + {facts = facts; + under_inspection = under_inspection; + unit_eq = unit_eq; + trace = trace} + +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 + 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)); + + 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 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 flags depth status t = +let try_candidate ?(smart=0) flags depth status eq_cache ctx 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 - (debug_print ~depth (lazy "pruned immediately"); None) - else - (incr candidate_no; - Some ((!candidate_no,t),status,open_goals)) + 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 _ as exc -> + 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 *) + (* 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 get_candidates status cache signature gty = +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 cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables - universe raw_gty + 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 cands = - List.filter (only signature context) - (NDiscriminationTree.TermSet.elements cands) + 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 -> Ast.NRef r | _ -> assert false in + List.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 + 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 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 +*) + 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 = + 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 = sort_candidates status context candidates in + let smart_candidates = + if smart then + match raw_gty with + | 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 *) + 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 + (* together more_cands more_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) - @ - List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands -;; + 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 = - let tcache,_ = cache in app_counter:= !app_counter+1; - let candidates = get_candidates status tcache signature gty in + let _,_,metasenv,subst,_ = status#obj in + let context = ctx_of gty in + let tcache = cache.facts in + let is_prod, is_eq = + let status, t = term_of_cic_term status gty context in + 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)); + let candidates, smart_candidates = + get_candidates ~smart:(not is_eq) depth + flags 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 with - | None -> elems - | Some x -> x::elems) + if (only_one && (elems <> [])) then elems + else + 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 context 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_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 context cand with + | None -> elems + | Some x -> x::elems) + [] smart_candidates + in + elems@more_elems ;; exception Found ;; (* 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 @@ -1314,134 +1165,89 @@ let is_subsumed depth status gty (_,cache) = try let idx = List.assq ctx cache in Ncic_termSet.elements - (InvRelDiscriminationTree.retrieve_generalizations idx gty) + (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 () + (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 + | Error _ -> ()) + candidates;false 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 reduce ~depth status g = +let rec intros ~depth status cache = + match is_prod status with + | Some _ -> + let trace = cache.trace in + 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 () ~trace + | _ -> status, cache +;; + +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 @@ -1450,17 +1256,37 @@ let reduce ~depth status g = (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.Implicit `JustOne),0,0,status,[g,P]]) + [(!candidate_no,Ast.Ident("__whd",None)),status]) ;; let do_something signature flags status g depth gty cache = - let l = reduce ~depth status g in - let l1,cache = - (equational_and_applicative_case - signature flags status g depth gty cache) + (* whd *) + 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 + (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 + let l2 = + if ((l1 <> []) && flags.last) then [] else + applicative_case depth signature status flags gty cache + 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 @ (List.rev l2) @ l, cache ;; let pp_goal = function @@ -1472,8 +1298,8 @@ let pp_goals status l = 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) ;; @@ -1493,20 +1319,20 @@ let sort_tac status = | [] -> 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 ;; @@ -1517,11 +1343,11 @@ let clean_up_tac status = | [] -> 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 ;; @@ -1532,132 +1358,255 @@ let focus_tac focus status = | [] -> 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 + (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s in status#set_stack gstatus ;; -let rec auto_clusters +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 + (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 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"); + 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 raise (Proved status) - else if depth = flags.maxdepth then raise (Gaveup IntSet.empty) - else if List.length goals < 2 then - auto_main flags signature cache depth status + if goals = [] then + if depth = 0 then raise (Proved (status, cache.trace)) + else + 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 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 + 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 - (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,trace,b = + List.fold_left + (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))); + 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,trace) -> + let status = NTactics.merge_tac status in + let lnew = List.length status#stack in + assert (lold = lnew); + (status,trace,true) + | Gaveup _ when top -> (status,trace,b) + ) + (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,trace)) else raise (Gaveup IntSet.empty) and - -(* let rec auto_main flags signature cache status k depth = *) - + +(* BRAND NEW VERSION *) 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 - | [] -> raise (Proved status) - | g::tlg -> - if depth = flags.maxdepth then raise (Gaveup IntSet.empty) + | [] 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 + | [] -> 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 + | orig::_ -> + 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 ~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 + 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 + (debug_print ~depth (lazy "SUBSUMED"); + raise (Gaveup IntSet.add g IntSet.empty)) else - let status = - if tlg=[] then status - else NTactics.branch_tac status in - let status, cache, g = intros ~depth status cache in - let gty = get_goalty status g in - let ctx,ty = close status g in - let closegty = mk_cic_term ctx ty in - let status, gty = apply_subst status (ctx_of gty) gty in - debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); - if is_subsumed depth status closegty cache then - (debug_print (lazy "SUBSUMED"); - raise (Gaveup IntSet.add g IntSet.empty)) - else - let alternatives, cache = + 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 flags status g depth gty cache in - let loop_cache = - let tcache,fcache = cache in - tcache,add_to_th closegty fcache closegty in - let unsat = - List.fold_left - (* the underscore information does not need to be returned - by do_something *) - (fun unsat ((_,t),_,_,status,_) -> - let depth',looping_cache = - if t=(Ast.Implicit `JustOne) then depth,cache - else depth+1, loop_cache in - debug_print (~depth:depth') - (lazy ("Case: " ^ CicNotationPp.pp_term t)); - try auto_clusters flags signature loop_cache - depth' status; unsat - with - | Proved status -> - debug_print (~depth:depth') (lazy "proved"); - if tlg=[] then raise (Proved status) - else - 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) - ^ ": " ^ - (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) + 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 + let cache = add_to_trace ~depth cache t in + try + auto_clusters flags signature cache depth status + with Gaveup _ -> + debug_print ~depth (lazy "Failed"); + ()) + alternatives; + raise (debug_print(lazy "no more candidates"); 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 = +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) 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( @@ -1667,13 +1616,25 @@ let auto_tac ~params:(_univ,flags) status = (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 (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; + candidates = candidates; maxwidth = width; maxsize = size; maxdepth = depth; @@ -1686,29 +1647,37 @@ let auto_tac ~params:(_univ,flags) status = if x > y then (print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - print(lazy + 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 -> - print (lazy ("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,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 + 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 - print(lazy + debug_print (print_stat statistics); + debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - print(lazy + debug_print(lazy ("Applicative nodes:"^string_of_int !app_counter)); s ;;