X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=41ea1e5e44386f35ec74959a6784bdfb0a095deb;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=d24c244a75f4f24e26530dd5319229affd2fa0be;hpb=2b80cfd9b2f739a28ea9938c4b1fbb7629839d32;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index d24c244a7..41ea1e5e4 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -30,6 +30,8 @@ let debug = false;; let debug_print s = if debug then prerr_endline (Lazy.force s);; +type auto_params = Cic.term list * (string * string) list + let elems = ref [] ;; (* closing a term w.r.t. its metavariables @@ -66,11 +68,11 @@ let naif_closure ?(prefix_name="xxx_") t metasenv context = let lambda_close ?prefix_name t menv ctx = let t = naif_closure ?prefix_name t menv ctx in List.fold_left - (fun t -> function - | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *) - | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t) - | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t)) - t ctx + (fun (t,i) -> function + | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *) + | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1 + | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1) + (t,List.length menv) ctx ;; (* functions for retrieving theorems *) @@ -98,16 +100,9 @@ let find_context_theorems context metasenv = match ctxentry with | Some (_,Cic.Decl t) -> (Cic.Rel i, CicSubstitution.lift i t)::res,i+1 - | Some (_,Cic.Def (_,Some t)) -> + | Some (_,Cic.Def (_,t)) -> (Cic.Rel i, CicSubstitution.lift i t)::res,i+1 - | Some (_,Cic.Def (_,None)) -> - let t = Cic.Rel i in - let ty,_ = - CicTypeChecker.type_of_aux' - metasenv context t CicUniv.empty_ugraph - in - (t,ty)::res,i+1 - | _ -> res,i+1) + | None -> res,i+1) ([],1) context in l @@ -147,7 +142,9 @@ let is_unit_equation context metasenv oldnewmeta term = args in if propositional_args = [] then - let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in + let newmetas = + List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv + in Some (args,metasenv,newmetas,head,newmeta) else None ;; @@ -163,19 +160,21 @@ let get_candidates universe cache t = candidates ;; -let only signature context t = +let only signature context metasenv t = try - let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + in let consts = MetadataConstraints.constants_of ty in let b = MetadataConstraints.UriManagerSet.subset consts signature in if b then b else - try - let ty' = unfold context ty in - let consts' = MetadataConstraints.constants_of ty' in - MetadataConstraints.UriManagerSet.subset consts' signature - with _-> false - with _ -> false + let ty' = unfold context ty in + let consts' = MetadataConstraints.constants_of ty' in + MetadataConstraints.UriManagerSet.subset consts' signature + with + | CicTypeChecker.TypeCheckerFailure _ -> assert false + | ProofEngineTypes.Fail _ -> false (* unfold may fail *) ;; let not_default_eq_term t = @@ -184,7 +183,7 @@ let not_default_eq_term t = not (LibraryObjects.in_eq_URIs uri) with Invalid_argument _ -> true -let retrieve_equations signature universe cache context= +let retrieve_equations dont_filter signature universe cache context metasenv = match LibraryObjects.eq_URI() with | None -> [] | Some eq_uri -> @@ -192,11 +191,10 @@ let retrieve_equations signature universe cache context= let fake= Cic.Meta(-1,[]) in let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in let candidates = get_candidates universe cache fake_eq in - (* defaults eq uris are built-in in auto *) - let candidates = List.filter not_default_eq_term candidates in - let candidates = List.filter (only signature context) candidates in - List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates; - candidates + if dont_filter then candidates + else + let candidates = List.filter not_default_eq_term candidates in + List.filter (only signature context metasenv) candidates let build_equality bag head args proof newmetas maxmeta = match head with @@ -218,6 +216,14 @@ let build_equality bag head args proof newmetas maxmeta = let partition_unit_equalities context metasenv newmeta bag equations = List.fold_left (fun (units,other,maxmeta)(t,ty) -> + if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then + let _ = + HLog.warn + ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context + ^ " since it is not meta closed") + in + units,(t,ty)::other,maxmeta + else match is_unit_equation context metasenv maxmeta ty with | Some (args,metasenv,newmetas,head,newmeta') -> let maxmeta,equality = @@ -232,50 +238,58 @@ let empty_tables = Saturation.make_passive [], Equality.mk_equality_bag) -let init_cache_and_tables dbd use_library paramod universe (proof, goal) = +let init_cache_and_tables + ?dbd use_library paramod use_context dont_filter universe (proof, goal) += (* the local cache in initially empty *) let cache = AutoCache.cache_empty in let _, metasenv, _subst,_, _, _ = proof in let signature = MetadataQuery.signature_of metasenv goal in let newmeta = CicMkImplicit.new_meta metasenv [] in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let ct = find_context_theorems context metasenv in + let ct = if use_context then find_context_theorems context metasenv else [] in debug_print (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct)))); let lt = - if use_library then - find_library_theorems dbd metasenv goal - else [] in + match use_library, dbd with + | true, Some dbd -> find_library_theorems dbd metasenv goal + | _ -> [] + in debug_print (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt)))); let cache = cache_add_list cache context (ct@lt) in let equations = - retrieve_equations signature universe cache context in + retrieve_equations dont_filter signature universe cache context metasenv + in debug_print (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations)))); let eqs_and_types = HExtlib.filter_map (fun t -> let ty,_ = - CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in - (* retrieve_equations could also return flexible terms *) - if is_an_equality ty then Some(t,ty) - else - try - let ty' = unfold context ty in - if is_an_equality ty' then Some(t,ty') else None - with _ -> None) (* catturare l'eccezione giusta di unfold *) - equations in + CicTypeChecker.type_of_aux' + metasenv context t CicUniv.empty_ugraph + in + (* retrieve_equations could also return flexible terms *) + if is_an_equality ty then Some(t,ty) + else + try + let ty' = unfold context ty in + if is_an_equality ty' then Some(t,ty') else None + with ProofEngineTypes.Fail _ -> None) + equations + in let bag = Equality.mk_equality_bag () in let units, other_equalities, newmeta = - partition_unit_equalities context metasenv newmeta bag eqs_and_types in - (* let env = (metasenv, context, CicUniv.empty_ugraph) in - let equalities = - let eq_uri = - match LibraryObjects.eq_URI() with - | None ->assert false - | Some eq_uri -> eq_uri in - Saturation.simplify_equalities bag eq_uri env units in *) + partition_unit_equalities context metasenv newmeta bag eqs_and_types + in + (* SIMPLIFICATION STEP + let equalities = + let env = (metasenv, context, CicUniv.empty_ugraph) in + let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in + Saturation.simplify_equalities bag eq_uri env units + in + *) let passive = Saturation.make_passive units in let no = List.length units in let active = Saturation.make_active [] in @@ -380,7 +394,9 @@ let close_more tables maxmeta context status auto universe cache = let proof, goalno = status in let _, metasenv,_subst,_,_, _ = proof in let signature = MetadataQuery.signature_of metasenv goalno in - let equations = retrieve_equations signature universe cache context in + let equations = + retrieve_equations false signature universe cache context metasenv + in let eqs_and_types = HExtlib.filter_map (fun t -> @@ -466,6 +482,80 @@ let find_context_equalities indexes, equalities, maxm, cache ;; +(********** PARAMETERS PASSING ***************) + +let bool params name default = + try + let s = List.assoc name params in + if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true + else if s = "0" || s = "false" || s = "no" || s= "off" then false + else + let msg = "Unrecognized value for parameter "^name^"\n" in + let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in + raise (ProofEngineTypes.Fail (lazy msg)) + with Not_found -> default +;; + +let string params name default = + try List.assoc name params with + | Not_found -> default +;; + +let int params name default = + try int_of_string (List.assoc name params) with + | Not_found -> default + | Failure _ -> + raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) +;; + +let flags_of_params params ?(for_applyS=false) () = + let int = int params in + let bool = bool params in + let close_more = bool "close_more" false in + let use_paramod = bool "use_paramod" true in + let use_only_paramod = + if for_applyS then true else bool "paramodulation" false in + let use_library = bool "library" + ((AutoTypes.default_flags()).AutoTypes.use_library) in + let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in + let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in + let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in + let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in + let do_type = bool "type" false in + let timeout = int "timeout" 0 in + { AutoTypes.maxdepth = + if use_only_paramod then 2 else depth; + AutoTypes.maxwidth = width; + AutoTypes.maxsize = size; + AutoTypes.timeout = + if timeout = 0 then + if for_applyS then Unix.gettimeofday () +. 30.0 + else + infinity + else + Unix.gettimeofday() +. (float_of_int timeout); + AutoTypes.use_library = use_library; + AutoTypes.use_paramod = use_paramod; + AutoTypes.use_only_paramod = use_only_paramod; + AutoTypes.close_more = close_more; + AutoTypes.dont_cache_failures = false; + AutoTypes.maxgoalsizefactor = gsize; + AutoTypes.do_types = do_type; + } + +let universe_of_params metasenv context universe tl = + if tl = [] then universe else + let tys = + List.map + (fun term -> + fst (CicTypeChecker.type_of_aux' metasenv context term + CicUniv.oblivion_ugraph)) + tl + in + Universe.index_list Universe.empty context (List.combine tl tys) +;; + + (***************** applyS *******************) let new_metasenv_and_unify_and_t @@ -509,7 +599,7 @@ let new_metasenv_and_unify_and_t in match let (active, passive,bag), cache, maxmeta = - init_cache_and_tables dbd flags.use_library true universe + init_cache_and_tables ~dbd flags.use_library true true false universe (proof'''',newmeta) in Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive @@ -528,12 +618,16 @@ let rec count_prods context ty = Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) = +let apply_smart + ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal) += let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let flags = flags_of_params params ~for_applyS:true () in + let universe = universe_of_params metasenv context universe univ in let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -831,9 +925,13 @@ 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 @@ -967,7 +1065,6 @@ let add_to_cache_and_del_from_orlist_if_green_cut | None -> assert false | Some (canonical_ctx , gty) -> let goalno,depth,sort = g in - assert (sort = P); let irl = mk_irl canonical_ctx in let goal = Cic.Meta(goalno, irl) in let proof = CicMetaSubst.apply_subst s goal in @@ -1081,7 +1178,7 @@ let equational_case assert (maxmeta >= maxm); let res' = List.map - (fun subst',(_,metasenv,_subst,proof,_, _),open_goals -> + (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) -> assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = @@ -1119,8 +1216,8 @@ let try_candidate ;; let sort_new_elems = - List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) -(* List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2) *) + List.sort (fun (_,_,_,l1) (_,_,_,l2) -> + List.length (prop_only l1) - List.length (prop_only l2)) ;; let applicative_case @@ -1224,7 +1321,7 @@ let prunable menv subst ty todo = | (D (_,_,T))::tl -> aux tl | _ -> false and no_progress variant = function - | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true + | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true | D ((n,_,P) as g)::tl -> (match calculate_goal_ty g subst menv with | None -> no_progress variant tl @@ -1240,7 +1337,18 @@ let prunable menv subst ty todo = 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 l = + let prune = !prune_hint in + prune_hint := []; (* possible race... *) + if prune = [] then l + else List.filter (condition_for_prune_hint prune) l +;; let auto_main tables maxm context flags universe cache elems = auto_context := context; let rec aux tables maxm flags cache (elems : status) = @@ -1249,8 +1357,9 @@ let auto_main tables maxm context flags universe cache elems = auto_status := elems; check_pause (); *) + let elems = filter_prune_hint elems in match elems with - | (m, s, size, don, todo, fl)::orlist as status when !hint <> None -> + | (m, s, size, don, todo, fl)::orlist when !hint <> None -> (match !hint with | Some i when condition_for_hint i todo -> aux tables maxm flags cache orlist @@ -1263,7 +1372,8 @@ let auto_main tables maxm context flags universe cache elems = | (m, s, _, _, [],_)::orlist -> (* complete success *) Proved (m, s, orlist, tables, cache, maxm) - | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist -> + | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist + when not flags.AutoTypes.do_types -> (* skip since not Prop, don't even check if closed by side-effect *) aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist) | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist -> @@ -1293,7 +1403,7 @@ let auto_main tables maxm context flags universe cache elems = (* timeout *) debug_print (lazy ("FAIL: TIMEOUT")); Gaveup (tables, cache, maxm) - | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status -> + | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status -> (* attack g *) match calculate_goal_ty g s m with | None -> @@ -1308,7 +1418,7 @@ let auto_main tables maxm context flags universe cache elems = (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize)); aux tables maxm flags cache orlist) else if prunable_for_size flags s m todo then - (prerr_endline ("POTO at depth: "^(string_of_int depth)); + (debug_print (lazy ("POTO at depth: "^(string_of_int depth))); aux tables maxm flags cache orlist) else (* still to be proved *) @@ -1445,70 +1555,12 @@ let auto flags metasenv tables universe cache context metasenv gl = None,cache ;; -let bool params name default = - try - let s = List.assoc name params in - if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true - else if s = "0" || s = "false" || s = "no" || s= "off" then false - else - let msg = "Unrecognized value for parameter "^name^"\n" in - let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in - raise (ProofEngineTypes.Fail (lazy msg)) - with Not_found -> default -;; - -let string params name default = - try List.assoc name params with - | Not_found -> default -;; - -let int params name default = - try int_of_string (List.assoc name params) with - | Not_found -> default - | Failure _ -> - raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) -;; - -let flags_of_params params ?(for_applyS=false) () = - let int = int params in - let bool = bool params in - let close_more = bool "close_more" false in - let use_paramod = bool "use_paramod" true in - let use_only_paramod = - if for_applyS then true else bool "paramodulation" false in - let use_library = bool "library" - ((AutoTypes.default_flags()).AutoTypes.use_library) in - let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in - let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in - let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in - let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in - let timeout = int "timeout" 0 in - { AutoTypes.maxdepth = - if use_only_paramod then 2 else depth; - AutoTypes.maxwidth = width; - AutoTypes.maxsize = size; - AutoTypes.timeout = - if timeout = 0 then - if for_applyS then Unix.gettimeofday () +. 30.0 - else - infinity - else - Unix.gettimeofday() +. (float_of_int timeout); - AutoTypes.use_library = use_library; - AutoTypes.use_paramod = use_paramod; - AutoTypes.use_only_paramod = use_only_paramod; - AutoTypes.close_more = close_more; - AutoTypes.dont_cache_failures = false; - AutoTypes.maxgoalsizefactor = gsize; - } - let applyS_tac ~dbd ~term ~params ~universe = ProofEngineTypes.mk_tactic (fun status -> try let proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] ~universe - (flags_of_params params ~for_applyS:true ()) status + apply_smart ~dbd ~term ~subst:[] ~params ~universe status in proof, gl with @@ -1516,185 +1568,45 @@ let applyS_tac ~dbd ~term ~params ~universe = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) -(* SUPERPOSITION *) - -(* Syntax: - * auto superposition target = NAME - * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only] - * - * - if table is omitted no superposition will be performed - * - if demod_table is omitted no demodulation will be prformed - * - subterms_only is passed to Indexing.superposition_right - * - * lists are coded using _ (example: H_H1_H2) - *) - -let eq_and_ty_of_goal = function - | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> - uri,t - | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) -;; - -let rec find_in_ctx i name = function - | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) - | Some (Cic.Name name', _)::tl when name = name' -> i - | _::tl -> find_in_ctx (i+1) name tl -;; - -let rec position_of i x = function - | [] -> assert false - | j::tl when j <> x -> position_of (i+1) x tl - | _ -> i -;; - - -let superposition_tac ~target ~table ~subterms_only ~demod_table status = - Saturation.reset_refs(); - let proof,goalno = status in - let curi,metasenv,_subst,pbo,pty, attrs = proof in - let metano,context,ty = CicUtil.lookup_meta goalno metasenv in - let eq_uri,tty = eq_and_ty_of_goal ty in - let env = (metasenv, context, CicUniv.empty_ugraph) in - let names = Utils.names_of_context context in - let bag = Equality.mk_equality_bag () in - let eq_index, equalities, maxm,cache = - find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty - in - let eq_what = - let what = find_in_ctx 1 target context in - List.nth equalities (position_of 0 what eq_index) - in - let eq_other = - if table <> "" then - let other = - let others = Str.split (Str.regexp "_") table in - List.map (fun other -> find_in_ctx 1 other context) others - in - List.map - (fun other -> List.nth equalities (position_of 0 other eq_index)) - other - else - [] - in - let index = List.fold_left Indexing.index Indexing.empty eq_other in - let maxm, eql = - if table = "" then maxm,[eq_what] else - Indexing.superposition_right bag - ~subterms_only eq_uri maxm env index eq_what +let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) = + let _,metasenv,_subst,_,_, _ = proof in + let _,context,goalty = CicUtil.lookup_meta goal metasenv in + let universe = universe_of_params metasenv context universe univ in + let flags = flags_of_params params () in + let use_library = flags.use_library in + let tables,cache,newmeta = + init_cache_and_tables ~dbd use_library flags.use_only_paramod true + false universe (proof, goal) in + let tables,cache,newmeta = + if flags.close_more then + close_more + tables newmeta context (proof, goal) + auto_all_solutions universe cache + else tables,cache,newmeta in + let initial_time = Unix.gettimeofday() in + let (_,oldmetasenv,_subst,_,_, _) = proof in + hint := None; + let elem = + metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] in - debug_print (lazy ("Superposition right:")); - debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env)); - debug_print (lazy ("\n table: ")); - List.iter - (fun e -> - debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other; - debug_print (lazy ("\n result: ")); - List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql; - debug_print (lazy ("\n result (cut&paste): ")); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - debug_print (lazy (CicPp.pp t names))) - eql; - debug_print (lazy ("\n result proofs: ")); - List.iter (fun e -> - debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in - let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in - Subst.ppsubst s ^ "\n" ^ - CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql; - if demod_table <> "" then - begin - let eql = - if eql = [] then [eq_what] else eql - in - let demod = - let demod = Str.split (Str.regexp "_") demod_table in - List.map (fun other -> find_in_ctx 1 other context) demod - in - let eq_demod = - List.map - (fun demod -> List.nth equalities (position_of 0 demod eq_index)) - demod - in - let table = List.fold_left Indexing.index Indexing.empty eq_demod in - let maxm,eql = - List.fold_left - (fun (maxm,acc) e -> - let maxm,eq = - Indexing.demodulation_equality bag eq_uri maxm env table e - in - maxm,eq::acc) - (maxm,[]) eql - in - let eql = List.rev eql in - debug_print (lazy ("\n result [demod]: ")); - List.iter - (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql; - debug_print (lazy ("\n result [demod] (cut&paste): ")); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - debug_print (lazy (CicPp.pp t names))) - eql; - end; - proof,[goalno] -;; - -let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) = - (* argument parsing *) - let string = string params in - let bool = bool params in - (* hacks to debug paramod *) - let superposition = bool "superposition" false in - let target = string "target" "" in - let table = string "table" "" in - let subterms_only = bool "subterms_only" false in - let demod_table = string "demod_table" "" in - match superposition with - | true -> - (* this is the ugly hack to debug paramod *) - superposition_tac - ~target ~table ~subterms_only ~demod_table (proof,goal) - | false -> - (* this is the real auto *) - let _,metasenv,_subst,_,_, _ = proof in - let _,context,goalty = CicUtil.lookup_meta goal metasenv in - let flags = flags_of_params params () in - (* just for testing *) - let use_library = flags.use_library in - let tables,cache,newmeta = - init_cache_and_tables dbd use_library flags.use_only_paramod - universe (proof, goal) in - let tables,cache,newmeta = - if flags.close_more then - close_more - tables newmeta context (proof, goal) - auto_all_solutions universe cache - else tables,cache,newmeta in - let initial_time = Unix.gettimeofday() in - let (_,oldmetasenv,_subst,_,_, _) = proof in - hint := None; - let elem = - metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] - in - match auto_main tables newmeta context flags universe cache [elem] with - | Proved (metasenv,subst,_, tables,cache,_) -> - prerr_endline - ("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,maxm) -> - debug_print - (lazy ("TIME:"^ - string_of_float(Unix.gettimeofday()-.initial_time))); - raise (ProofEngineTypes.Fail (lazy "Auto gave up")) + match auto_main tables newmeta context flags universe cache [elem] with + | Proved (metasenv,subst,_, tables,cache,_) -> + (*prerr_endline + ("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,maxm) -> + debug_print + (lazy ("TIME:"^ + string_of_float(Unix.gettimeofday()-.initial_time))); + raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; let auto_tac ~dbd ~params ~universe = @@ -1706,15 +1618,60 @@ let eq_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; +(* performs steps of rewrite with the universe, obtaining if possible + * a trivial goal *) +let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= + let _,metasenv,_subst,_,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let steps = int_of_string (string params "steps" "1") in + let universe = universe_of_params metasenv context universe univ in + let eq_uri = eq_of_goal ty in + let (active,passive,bag), cache, maxm = + (* we take the whole universe (no signature filtering) *) + init_cache_and_tables false true false true universe (proof,goal) + in + let initgoal = [], metasenv, ty in + let table = + let equalities = (Saturation.list_of_passive passive) in + (* we demodulate using both actives passives *) + List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities + in + let env = metasenv,context,CicUniv.empty_ugraph in + match Indexing.solve_demodulating bag env table initgoal steps with + | Some (proof, metasenv, newty) -> + let refl = + match newty with + | Cic.Appl[Cic.MutInd _;eq_ty;left;_] -> + Equality.Exact (Equality.refl_proof eq_uri eq_ty left) + | _ -> assert false + in + let proofterm,_ = + Equality.build_goal_proof + bag eq_uri proof refl newty [] context metasenv + in + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) status + | None -> + raise + (ProofEngineTypes.Fail (lazy + ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) +;; +let solve_rewrite_tac ~params ~universe () = + ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params) +;; + (* DEMODULATE *) -let demodulate_tac ~dbd ~universe (proof,goal)= +let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let universe = universe_of_params metasenv context universe univ in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let initgoal = [], [], ty in + let initgoal = [], metasenv, ty in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = - init_cache_and_tables dbd false true universe (proof,goal) in + init_cache_and_tables + ~dbd false true true false universe (proof,goal) + in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let table = @@ -1749,9 +1706,10 @@ let demodulate_tac ~dbd ~universe (proof,goal)= ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) ;; -let demodulate_tac ~dbd ~universe = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);; +let demodulate_tac ~dbd ~params ~universe = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);; let pp_proofterm = Equality.pp_proofterm;; let revision = "$Revision$";; +let size_and_depth context metasenv t = 100, 100