X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=c2d933b0a091750b5205587faddbf872984f7216;hb=d3d4ea54cb895a1adc6cb327df42e1394b3f2bea;hp=1e326df1086c25f7ce6f92640aff9d87b413dcc8;hpb=cee1c02ad6a113b711b9d93176296cf16b9ec351;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 1e326df10..c2d933b0a 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -26,7 +26,9 @@ open AutoTypes;; open AutoCache;; -let debug_print s = prerr_endline (Lazy.force s);; +let debug = false;; +let debug_print s = + if debug then prerr_endline (Lazy.force s);; (* functions for retrieving theorems *) @@ -82,7 +84,7 @@ let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;; let is_unit_equation context metasenv oldnewmeta term = let head, metasenv, args, newmeta = - ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 + TermUtil.saturate_term oldnewmeta metasenv context term 0 in let propositional_args = HExtlib.filter_map @@ -108,7 +110,7 @@ let is_unit_equation context metasenv oldnewmeta term = ;; let get_candidates universe cache t = - let candidates = + let candidates= (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t) in let debug_msg = @@ -118,14 +120,27 @@ let get_candidates universe cache t = candidates ;; -let only singature context t = +let only signature context t = try let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in let consts = MetadataConstraints.constants_of ty in - MetadataConstraints.UriManagerSet.subset consts singature + 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 not_default_eq_term t = + try + let uri = CicUtil.uri_of_term t in + not (LibraryObjects.in_eq_URIs uri) + with Invalid_argument _ -> true + let retrieve_equations signature universe cache context= match LibraryObjects.eq_URI() with | None -> [] @@ -134,7 +149,11 @@ 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 - List.filter (only signature context) candidates + (* 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 -> prerr_endline (CicPp.ppterm t)) candidates; + candidates let build_equality bag head args proof newmetas maxmeta = match head with @@ -170,24 +189,25 @@ let empty_tables = Saturation.make_passive [], Equality.mk_equality_bag) -let init_cache_and_tables dbd use_library universe (proof, goal) = +let init_cache_and_tables dbd use_library paramod universe (proof, goal) = (* the local cache in initially empty *) let cache = AutoCache.cache_empty in - let _, metasenv, _, _ = proof in + let _, metasenv, _, _, _ = 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 + prerr_endline + ("ho trovato nel contesto " ^ (string_of_int (List.length ct))); let lt = if use_library then - find_library_theorems dbd metasenv goal + find_library_theorems dbd metasenv goal else [] in - (* all equations are added to the cache *) prerr_endline ("ho trovato nella libreria " ^ (string_of_int (List.length lt))); - (* let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in *) let cache = cache_add_list cache context (ct@lt) in - let equations = retrieve_equations signature universe cache context in + let equations = + retrieve_equations signature universe cache context in prerr_endline ("ho trovato equazioni n. " ^ (string_of_int (List.length equations))); let eqs_and_types = @@ -217,13 +237,16 @@ let init_cache_and_tables dbd use_library universe (proof, goal) = let no = List.length units in let active = Saturation.make_active [] in let active,passive,newmeta = - Saturation.pump_actives context bag newmeta active passive (no+1) infinity + if paramod then active,passive,newmeta + else + Saturation.pump_actives + context bag newmeta active passive (no+1) infinity in (active,passive,bag),cache,newmeta let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = let head, metasenv, args, newmeta = - ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 + TermUtil.saturate_term oldnewmeta metasenv context term 0 in let propositional_args = HExtlib.filter_map @@ -312,7 +335,7 @@ let build_equalities auto context metasenv tables universe cache newmeta equatio let close_more tables maxmeta context status auto universe cache = let (active,passive,bag) = tables in let proof, goalno = status in - let _, metasenv,_,_ = proof in + let _, metasenv,_,_, _ = proof in let signature = MetadataQuery.signature_of metasenv goalno in let equations = retrieve_equations signature universe cache context in let eqs_and_types = @@ -345,7 +368,7 @@ let find_context_equalities let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let _,metasenv,_,_ = proof in + let _,metasenv,_,_, _ = proof in let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in (* if use_auto is true, we try to close the hypothesis of equational statements using auto; a naif, and probably wrong approach *) @@ -407,13 +430,13 @@ let new_metasenv_and_unify_and_t context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = - ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in + TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in let proof',oldmetasenv = - let (puri,metasenv,pbo,pty) = proof in - (puri,newmetasenv,pbo,pty),metasenv + let (puri,metasenv,pbo,pty, attrs) = proof in + (puri,newmetasenv,pbo,pty, attrs),metasenv in let goal_for_paramod = match LibraryObjects.eq_URI () with @@ -423,13 +446,13 @@ let new_metasenv_and_unify_and_t in let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in - let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in + let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let proof''',goals = ProofEngineTypes.apply_tactic (EqualityTactics.rewrite_tac ~direction:`RightToLeft ~pattern:(ProofEngineTypes.conclusion_pattern None) - (Cic.Meta(newmeta,irl))) + (Cic.Meta(newmeta,irl)) []) (proof'',goal) in let goal = match goals with [g] -> g | _ -> assert false in @@ -438,7 +461,7 @@ let new_metasenv_and_unify_and_t in match let (active, passive,bag), cache, maxmeta = - init_cache_and_tables dbd flags.use_library universe (proof'''',newmeta) + init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta) in Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive max_int max_int flags.timeout @@ -448,7 +471,7 @@ let new_metasenv_and_unify_and_t | Some (_,proof''''',_), active,passive,_ -> subst,proof''''', ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive + ~newmetasenv:(let _,m,_,_, _ = proof''''' in m), active, passive ;; let rec count_prods context ty = @@ -460,7 +483,7 @@ let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let (_,metasenv,_,_) = proof in + let (_,metasenv,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = @@ -521,26 +544,35 @@ let is_in_prop context subst metasenv ty = let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u) ;; + let assert_proof_is_valid proof metasenv context goalty = - let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in - let b,_ = CicReduction.are_convertible context ty goalty u in - if not b then + if debug then begin - let names = - List.map (function None -> None | Some (x,_) -> Some x) context - in - prerr_endline ("PROOF:" ^ CicPp.pp proof names); - prerr_endline ("PROOFTY:" ^ CicPp.pp ty names); - prerr_endline ("GOAL:" ^ CicPp.pp goalty names); - prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv); - end; - assert b + let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in + let b,_ = CicReduction.are_convertible context ty goalty u in + if not b then + begin + let names = + List.map (function None -> None | Some (x,_) -> Some x) context + in + prerr_endline ("PROOF:" ^ CicPp.pp proof names); + prerr_endline ("PROOFTY:" ^ CicPp.pp ty names); + prerr_endline ("GOAL:" ^ CicPp.pp goalty names); + prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv); + end; + assert b + end + else () ;; + let assert_subst_are_disjoint subst subst' = - assert(List.for_all - (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') - subst) + if debug then + assert(List.for_all + (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') + subst) + else () ;; + let sort_new_elems = List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) ;; @@ -621,7 +653,7 @@ let equational_case with | None, active, passive, maxmeta -> [], (active,passive,bag), cache, maxmeta, flags - | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta -> + | Some(subst',(_,metasenv,proof,_, _),open_goals),active,passive,maxmeta -> assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = order_new_goals metasenv subst open_goals ppterm in @@ -636,7 +668,7 @@ let equational_case assert (maxmeta >= maxm); let res' = List.map - (fun subst',(_,metasenv,proof,_),open_goals -> + (fun subst',(_,metasenv,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 @@ -670,16 +702,14 @@ let try_candidate = let ppterm = ppterm context in try - let subst', ((_,metasenv,_,_), open_goals), maxmeta = + let subst', ((_,metasenv,_,_, _), open_goals), maxmeta = PrimitiveTactics.apply_with_subst ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) in debug_print (lazy (" OK: " ^ ppterm cand)); let metasenv = CicRefine.pack_coercion_metasenv metasenv in - assert (maxmeta >= maxm); - (*FIXME:sicuro che posso @?*) - assert_subst_are_disjoint subst subst'; - let subst = subst@subst' in + (* assert_subst_are_disjoint subst subst'; *) + let 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 Some (metasenv,subst,open_goals), tables , maxmeta @@ -715,7 +745,8 @@ let is_a_green_cut goalty = CicUtil.is_meta_closed goalty ;; -let prop = function (_,_,P) -> true | _ -> false;; +let prop = function (_,depth,P) -> depth < 9 | _ -> false;; + let calculate_timeout flags = if flags.timeout = 0. then (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity}) @@ -760,16 +791,17 @@ let rec auto_main tables maxm context flags elems universe cache = try let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in debug_print - (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty)); + (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^ + "with depth"^string_of_int depth)); debug_print (lazy (AutoCache.cache_print context cache)); - if sort = T && tl <> [] then (* FIXME!!!! *) + if sort = T (* && tl <> []*) then (debug_print (lazy (" FAILURE(not in prop)")); - aux flags tables maxm cache tl (* FAILURE (not in prop) *)) + aux flags tables maxm cache ((metasenv,subst,gl)::tl)) else match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with | Fail s, tables, cache, maxm' -> - assert(maxm' >= maxm);let maxm = maxm' in + let maxm = maxm' in debug_print (lazy (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty)); @@ -780,7 +812,7 @@ let rec auto_main tables maxm context flags elems universe cache = in aux flags tables maxm cache tl | Success (metasenv,subst,others), tables, cache, maxm' -> - assert(maxm' >= maxm);let maxm = maxm' in + let maxm = maxm' in (* others are alternatives in OR *) try let goal = Cic.Meta(goalno,irl) in @@ -788,12 +820,12 @@ let rec auto_main tables maxm context flags elems universe cache = debug_print (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof)); if is_a_green_cut goalty then - (assert_proof_is_valid proof metasenv context goalty; + (* assert_proof_is_valid proof metasenv context goalty; *) let cache = cache_add_success sort cache goalty proof in - aux flags tables maxm cache ((metasenv,subst,gl)::tl)) + aux flags tables maxm cache ((metasenv,subst,gl)::tl) else (let goalty = CicMetaSubst.apply_subst subst goalty in - assert_proof_is_valid proof metasenv context goalty; + (* assert_proof_is_valid proof metasenv context goalty; *) let cache = if is_a_green_cut goalty then cache_add_success sort cache goalty proof @@ -815,6 +847,7 @@ let rec auto_main tables maxm context flags elems universe cache = aux flags tables maxm cache ((metasenv,subst,gl)::tl) and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc = + (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *) let goalty = CicMetaSubst.apply_subst subst goalty in (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *) (* FAILURE (euristic cut) *) @@ -823,24 +856,24 @@ let rec auto_main tables maxm context flags elems universe cache = Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth), tables,cache,maxm(*FAILURE(depth)*) | Succeded t -> - assert(List.for_all (fun (i,_) -> i <> goalno) subst); let entry = goalno, (cc, t,goalty) in assert_subst_are_disjoint subst [entry]; let subst = entry :: subst in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in debug_print (lazy (" CACHE HIT!")); Success (metasenv, subst, []), tables, cache, maxm - | UnderInspection -> Fail "looping",tables,cache, maxm + | UnderInspection -> + (* assert (not (is_a_green_cut goalty)); *) + Fail "looping",tables,cache, maxm | Notfound | Failed_in _ when depth > 0 -> (* we have more depth now *) let cache = cache_add_underinspection cache goalty depth in - let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in + let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *) let elems, tables, cache, maxm, flags = if is_equational_case goalty flags then let elems,tables,cache,maxm1, flags = equational_case tables maxm cache depth fake_proof goalno goalty subst context flags in - assert(maxm1 >= maxm); let maxm = maxm1 in let more_elems, tables, cache, maxm1 = if flags.use_only_paramod then @@ -849,7 +882,6 @@ let rec auto_main tables maxm context flags elems universe cache = applicative_case tables maxm depth subst fake_proof goalno goalty metasenv context universe cache in - assert(maxm1 >= maxm); let maxm = maxm1 in elems@more_elems, tables, cache, maxm, flags else @@ -859,7 +891,7 @@ let rec auto_main tables maxm context flags elems universe cache = elems, tables, cache, maxm, flags in aux flags tables maxm cache elems - | _ -> Fail "??",tables,cache,maxm + | _ -> Fail "depth = 0",tables,cache,maxm in aux flags tables maxm cache elems @@ -912,7 +944,9 @@ let auto flags metasenv tables universe cache context metasenv gl = | Success (metasenv,subst,_), tables,cache,_ -> prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); Some (subst,metasenv), cache - | Fail s,tables,cache,maxm -> None,cache + | Fail s,tables,cache,maxm -> + prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); + None,cache ;; let bool params name default = @@ -1017,7 +1051,7 @@ let rec position_of i x = function let superposition_tac ~target ~table ~subterms_only ~demod_table status = Saturation.reset_refs(); let proof,goalno = status in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,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 @@ -1121,20 +1155,21 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) = ~target ~table ~subterms_only ~demod_table (proof,goal) | false -> (* this is the real auto *) - let _,metasenv,_,_ = proof in + let _,metasenv,_,_, _ = proof in let _,context,_ = 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 universe (proof, goal) in + 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,_,_) = proof in + let (_,oldmetasenv,_,_, _) = proof in let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in match auto_main tables newmeta context flags [elem] universe cache with | Success (metasenv,subst,_), tables,cache,_ -> @@ -1149,6 +1184,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) = in proof,opened | Fail s,tables,cache,maxm -> + prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; @@ -1162,14 +1198,14 @@ let eq_of_goal = function ;; (* DEMODULATE *) -let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = - let curi,metasenv,pbo,pty = proof in +let demodulate_tac ~dbd ~universe (proof,goal)= + let curi,metasenv,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let initgoal = [], [], ty in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = - init_cache_and_tables dbd true Universe.empty (proof,goal) in + init_cache_and_tables dbd false true universe (proof,goal) in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let table = @@ -1190,7 +1226,7 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = in let extended_metasenv = (maxm,context,newty)::metasenv in let extended_status = - (curi,extended_metasenv,pbo,pty),goal in + (curi,extended_metasenv,pbo,pty, attrs),goal in let (status,newgoals) = ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac ~term:proofterm) @@ -1204,7 +1240,8 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) ;; -let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);; +let demodulate_tac ~dbd ~universe = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;