X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=0ff4ddbe5358b82e7c27782c4e5974b6693d6e2e;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=7a9c20f0f85ce0b6106db7819162bf470c9d9793;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 7a9c20f0f..0ff4ddbe5 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -11,77 +11,51 @@ open Printf -let print ?(depth=0) s = +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 = prerr_endline (String.make depth '\t'^Lazy.force s) -let noprint ?(depth=0) _ = () -let debug_print = noprint + +let debug_do f = if !debug then f () else () 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 +(* =================================== paramod =========================== *) +let auto_paramod ~params:(l,_) status goal = + let gty = get_goalty status goal in + let n,h,metasenv,subst,o = status#obj in + let status,t = term_of_cic_term status gty (ctx_of gty) in + let status, l = + List.fold_left + (fun (status, l) t -> + let status, t = disambiguate status (ctx_of gty) t None in + let status, ty = typeof status (ctx_of t) t in + let status, t = term_of_cic_term status t (ctx_of gty) in + let status, ty = term_of_cic_term status ty (ctx_of ty) in + (status, (t,ty) :: l)) + (status,[]) l + in + match + NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l + with + | [] -> raise (Error (lazy "no proof found",None)) + | (pt, metasenv, subst)::_ -> + let status = status#set_obj (n,h,metasenv,subst,o) in + instantiate status goal (mk_cic_term (ctx_of gty) pt) +;; -let toref f tbl t = - match t with - | Ast.NRef n -> - f tbl n - | Ast.NCic _ (* local candidate *) - | _ -> () +let auto_paramod_tac ~params status = + NTactics.distribute_tac (auto_paramod ~params) status +;; -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 ========================= *) +(*************** subsumption ****************) module IntSet = Set.Make(struct type t = int let compare = compare end) +(* exceptions *) let get_sgoalty status g = let _,_,metasenv,subst,_ = status#obj in @@ -108,266 +82,10 @@ 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 -> -(* - 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:int) = - 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 _ -> debug_print (lazy ("no paramod proof found"));[] -;; - -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 = apply_subst_context ~fix_projections:true status (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) ;; @@ -376,9 +94,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 @@ -398,11 +116,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 @@ -414,24 +132,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 ;; @@ -446,13 +164,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 @@ -463,11 +181,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 @@ -486,8 +204,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 @@ -517,178 +235,884 @@ let close status g = ctx,ty ;; -(****************** 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) + +(* =================================== 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 - aux metasenv ty [] + (flags.use_paramod && is_an_equational_goal goalty) || + (flags.use_only_paramod && ensure_equational goalty) +;; -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) +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 - 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 + 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 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 - | 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 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 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 check_pause _ = + if !in_pause then + begin + Mutex.lock mutex; + Condition.wait cond mutex; + Mutex.unlock mutex + end +;; -let smart_apply_auto t eq_cache = - NTactics.distribute_tac (smart_apply t eq_cache) +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 -(****************** types **************) + subst, metasenv +;; +let mk_fake_proof metasenv subst (goalno,_,_) goalty context = + None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] +;; -type th_cache = (NCic.context * InvRelDiscriminationTree.t) list +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) = -(* 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 + 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 - 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) ] + (* 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 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 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 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 _, 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] +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 +;; *) - [ty] in -(*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *) + +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")) +;; +*) + +(****************** 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 let keys = let _, ty = term_of_cic_term status ty (ctx_of ty) in match ty with - | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h)))) - | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_) + | NCic.Const (NReference.Ref (_,NReference.Def h)) + | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) when h > 0 -> let _,ty,_= saturate status ~delta:(h-1) orig_ty in ty::keys @@ -697,16 +1121,6 @@ let keys_of_type status orig_ty = 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 -> @@ -720,8 +1134,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 @@ -748,19 +1162,6 @@ 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 -> @@ -782,10 +1183,10 @@ 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.assoc(*q*) k th in + let idx = List.assq k th in let acc = Ncic_termSet.union acc (InvRelDiscriminationTree.retrieve_unifiables idx gty) in @@ -797,42 +1198,12 @@ 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 @@ -840,7 +1211,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 * Ast.term list +exception Proved of #NTacStatus.tac_status (* let close_failures _ c = c;; *) (* let prunable _ _ _ = false;; *) @@ -848,350 +1219,71 @@ exception Proved of NTacStatus.tac_status * Ast.term list (* let put_in_subst s _ _ _ = s;; *) (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *) (* let cache_add_underinspection c _ _ = c;; *) - -let init_cache ?(facts=[]) ?(under_inspection=[],[]) - ?(unit_eq=NCicParamod.empty_state) - ?(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 equational_case _ _ _ _ _ _ = [];; +let only _ _ _ = true;; 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 sort_new_elems l = + List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l +;; -let try_candidate ?(smart=0) flags depth status eq_cache ctx t = +let try_candidate flags depth status t = try - debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); - let status = - if smart= 0 then NTactics.apply_tac ("",0,t) status - else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status - else (* smart = 2: both *) - try NTactics.apply_tac ("",0,t) status - with Error _ -> - smart_apply_auto ("",0,t) eq_cache status - in -(* - let og_no = openg_no status in - if (* og_no > flags.maxwidth || *) - ((depth + 1) = flags.maxdepth && og_no <> 0) then - (debug_print ~depth (lazy "pruned immediately"); None) - else *) - (* 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)) + 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)) 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 get_candidates status cache signature gty = 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 - 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 [] + universe raw_gty + in + let cands = + List.filter (only signature context) + (NDiscriminationTree.TermSet.elements cands) in - 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,[] -;; *) + 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 applicative_case depth signature status flags gty cache = + let tcache,_ = cache in app_counter:= !app_counter+1; - 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~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: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 + let candidates = get_candidates status tcache signature gty 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 - 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 = + let elems = 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:sm) - flags depth status cache.unit_eq context cand with - | None -> elems - | Some x -> x::elems) + match try_candidate flags depth status cand with + | None -> elems + | Some x -> x::elems) [] candidates in - 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 + 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 @@ -1203,112 +1295,118 @@ 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 +;; + 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 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,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 intro ~depth status (tcache,fcache) name = let status = NTactics.intro_tac name status in - let _, ctx, ngty = current_goal status in + let open_goals = head_goals status#stack in + assert (List.length open_goals = 1); + let open_goal = List.hd open_goals in + let ngty = get_goalty status open_goal in + let ctx = ctx_of ngty in let t = mk_cic_term ctx (NCic.Rel 1) in let status, keys = keys_of_term status t in - let facts = List.fold_left (add_to_th t) facts keys in - debug_print ~depth (lazy ("intro: "^ name)); + let tcache = List.fold_left (add_to_th t) tcache keys in + debug_print ~depth (lazy ("intro: "^ string_of_int open_goal)); (* unprovability is not stable w.r.t introduction *) - status, facts -;; - -let rec intros_facts ~depth status facts = - if List.length (head_goals status#stack) <> 1 then status, facts else - match is_prod status with - | `Inductive name - | `Some(name) -> - let status,facts = - intro ~depth status facts name - in intros_facts ~depth status facts -(* | `Inductive name -> - let status = NTactics.case1_tac name status in - intros_facts ~depth status facts *) - | _ -> status, facts -;; - -let intros ~depth status cache = - match is_prod status with - | `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 - let status = NTactics.merge_tac status in - [(0,Ast.Ident("__intros",None)),status], - init_cache ~facts ~unit_eq () ~trace - | _ -> [],cache -;; - -let reduce ~whd ~depth status g = + status, (tcache,[]) +;; + +let rec intros ~depth status cache = + let open_goals = head_goals status#stack in + assert (List.length open_goals = 1); + let open_goal = List.hd open_goals in + let gty = get_goalty status open_goal in + let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in + match raw_gty with + | NCic.Prod (name,_,_) -> + let status,cache = + intro ~depth status cache (guess_name name (ctx_of gty)) + in intros ~depth status cache + | _ -> status, cache, open_goal +;; + +let reduce ~depth status g = let n,h,metasenv,subst,o = status#obj in let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in let ty = NCicUntrusted.apply_subst subst ctx ty in - let ty' = - (if whd then NCicReduction.whd else NCicTacReduction.normalize) ~subst ctx ty - in + let ty' = NCicReduction.whd ~subst ctx ty in if ty = ty' then [] else (debug_print ~depth @@ -1317,40 +1415,17 @@ let reduce ~whd ~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.Ident("__whd",None)),status]) + [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]]) ;; 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 ~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 - let l2 = - if ((l1 <> []) && flags.last) then [] else - applicative_case depth signature status flags gty cache + let l = reduce ~depth status g in + let l1,cache = + (equational_and_applicative_case + signature flags status g depth 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 + sort_new_elems (l@l1), cache ;; let pp_goal = function @@ -1362,8 +1437,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) ;; @@ -1383,20 +1458,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 ;; @@ -1407,11 +1482,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 ;; @@ -1422,256 +1497,132 @@ 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 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) +let rec auto_clusters 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); + debug_print ~depth (lazy "entering auto clusters"); (* 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, 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 + 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 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 + String.concat "," (List.map string_of_int goals))); + let classes = HExtlib.clusters (deps status) goals in debug_print ~depth - (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 + (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 debug_print ~depth (lazy ("focusing on" ^ - 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) + 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) and - -(* BRAND NEW VERSION *) + +(* let rec auto_main flags signature cache status k depth = *) + 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,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 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)) + | [] -> raise (Proved status) + | g::tlg -> + if depth = flags.maxdepth then raise (Gaveup IntSet.empty) 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 = + 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 = 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 - {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) || - 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 depth status - with Gaveup _ -> - debug_print ~depth (lazy "Failed"); - ()) - alternatives; - raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty) + 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 int name l def = try int_of_string (List.assoc name l) with Failure _ | Not_found -> def ;; -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 auto_tac ~params:(_univ,flags) status = 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 -(* pp_th status facts; *) + let status, cache = mk_th_cache status goals in +(* pp_th status cache; *) (* NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> debug_print (lazy( @@ -1681,25 +1632,13 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) 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 4 (* (3+List.length goals)*) in + let width = int "width" flags (3+List.length goals) in (* XXX fix sort *) -(* let goals = List.map (fun i -> (i,P)) goals in *) - let signature = height_of_goals status in + let goals = List.map (fun i -> (i,P)) goals in + let signature = () in let flags = { - last = true; - candidates = candidates; maxwidth = width; maxsize = size; maxdepth = depth; @@ -1712,38 +1651,29 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = if x > y then (print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - debug_print(lazy + 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 (~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 + 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)); 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 - let s = s#set_stack stack in - trace_ref := trace; - oldstatus#set_status s + s#set_stack stack in let s = up_to depth depth in - debug_print (print_stat statistics); - debug_print(lazy + print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - debug_print(lazy + print(lazy ("Applicative nodes:"^string_of_int !app_counter)); s ;;