From d265b4b4fac92685c29f89887c1083a494bae6e5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 27 Nov 2006 12:31:26 +0000 Subject: [PATCH] Only modified for taking unfold into account. Assertion made only in case of debug. --- components/tactics/auto.ml | 100 ++++++++++++++++++++++++------------- 1 file changed, 64 insertions(+), 36 deletions(-) diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 1e326df10..92d66ef72 100644 --- a/components/tactics/auto.ml +++ b/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 () else prerr_endline (Lazy.force s);; (* functions for retrieving theorems *) @@ -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,7 +189,7 @@ 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 @@ -178,16 +197,17 @@ let init_cache_and_tables dbd use_library universe (proof, goal) = 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,7 +237,10 @@ 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 @@ -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 @@ -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) ;; @@ -676,8 +708,6 @@ let try_candidate 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 let open_goals = order_new_goals metasenv subst open_goals ppterm in @@ -769,7 +799,7 @@ let rec auto_main tables maxm context flags elems universe cache = 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 +810,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 @@ -823,7 +853,6 @@ 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 @@ -840,7 +869,6 @@ let rec auto_main tables maxm context flags elems universe cache = 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 +877,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 @@ -1127,7 +1154,8 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) = (* 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 @@ -1169,7 +1197,7 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 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 true true Universe.empty (proof,goal) in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let table = -- 2.39.2