# HG changeset patch # User blanchet # Date 1381305198 -7200 # Node ID 957115f3dae4927880945de475c1adac86d95c9c # Parent 819cd1046922171514ccfbf03223c909548fbd9d use plain types instead of dedicated type pattern diff -r 819cd1046922 -r 957115f3dae4 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Oct 09 09:51:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Oct 09 09:53:18 2013 +0200 @@ -43,23 +43,23 @@ (* An abstraction of Isabelle types and first-order terms *) datatype pattern = PVar | PApp of string * pattern list -datatype patternT = PVarT | PAppT of string * patternT list -datatype ptype = PType of int * patternT list +datatype ptype = PType of int * typ list fun string_of_pattern PVar = "_" | string_of_pattern (PApp (s, ps)) = if null ps then s else s ^ string_of_patterns ps and string_of_patterns ps = "(" ^ commas (map string_of_pattern ps) ^ ")" -fun string_of_patternT PVarT = "_" - | string_of_patternT (PAppT (s, ps)) = +fun string_of_patternT (TVar _) = "_" + | string_of_patternT (Type (s, ps)) = if null ps then s else s ^ string_of_patternsT ps + | string_of_patternT (TFree (s, _)) = s and string_of_patternsT ps = "(" ^ commas (map string_of_patternT ps) ^ ")" fun string_of_ptype (PType (_, ps)) = string_of_patternsT ps (*Is the second type an instance of the first one?*) fun match_pattern (PVar, _) = true - | match_pattern (PApp _, PVar) = false + | match_pattern (_, PVar) = false | match_pattern (PApp (s, ps), PApp (t, qs)) = s = t andalso match_patterns (ps, qs) and match_patterns (_, []) = true @@ -68,10 +68,11 @@ match_pattern (p, q) andalso match_patterns (ps, qs) (*Is the second type an instance of the first one?*) -fun match_patternT (PVarT, _) = true - | match_patternT (PAppT _, PVarT) = false - | match_patternT (PAppT (s, ps), PAppT (t, qs)) = +fun match_patternT (TVar _, _) = true + | match_patternT (Type (s, ps), Type (t, qs)) = s = t andalso match_patternsT (ps, qs) + | match_patternT (TFree (s, _), TFree (t, _)) = s = t + | match_patternT (_, _) = false and match_patternsT (_, []) = true | match_patternsT ([], _) = false | match_patternsT (p :: ps, q :: qs) = @@ -85,14 +86,9 @@ fun pconst_hyper_mem f const_tab (s, ps) = exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s)) -fun patternT_of_type (Type (s, Ts)) = PAppT (s, map patternT_of_type Ts) - | patternT_of_type (TFree (s, _)) = PAppT (s, []) - | patternT_of_type (TVar _) = PVarT - (* Pairs a constant with the list of its type instantiations. *) fun ptype thy const x = - (if const then map patternT_of_type (these (try (Sign.const_typargs thy) x)) - else []) + (if const then these (try (Sign.const_typargs thy) x) else []) fun rich_ptype thy const (s, T) = PType (order_of_type T, ptype thy const (s, T)) fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T)) @@ -100,9 +96,19 @@ fun string_of_hyper_pconst (s, ps) = s ^ "{" ^ commas (map string_of_ptype ps) ^ "}" -(* Add a pconstant to the table, but a [] entry means a standard - connective, which we ignore.*) -fun add_pconst_to_table (s, p) = Symtab.map_default (s, [p]) (insert (op =) p) +fun patternT_eq (TVar _, TVar _) = true + | patternT_eq (Type (s, Ts), Type (t, Us)) = s = t andalso patternsT_eq (Ts, Us) + | patternT_eq (TFree (s, _), TFree (t, _)) = (s = t) + | patternT_eq _ = false +and patternsT_eq ([], []) = true + | patternsT_eq ([], _) = false + | patternsT_eq (_, []) = false + | patternsT_eq (T :: Ts, U :: Us) = patternT_eq (T, U) andalso patternsT_eq (Ts, Us) +fun ptype_eq (PType (m, Ts), PType (n, Us)) = m = n andalso patternsT_eq (Ts, Us) + + (* Add a pconstant to the table, but a [] entry means a standard connective, + which we ignore. *) +fun add_pconst_to_table (s, p) = Symtab.map_default (s, [p]) (insert ptype_eq p) (* Set constants tend to pull in too many irrelevant facts. We limit the damage by treating them more or less as if they were built-in but add their @@ -195,11 +201,16 @@ fun patternT_ord p = case p of - (PVarT, PVarT) => EQUAL - | (PVarT, PAppT _) => LESS - | (PAppT _, PVarT) => GREATER - | (PAppT q1, PAppT q2) => + (TVar _, TVar _) => EQUAL + | (TVar _, Type _) => LESS + | (TVar _, TFree _) => LESS + | (Type _, TVar _) => GREATER + | (TFree _, TVar _) => GREATER + | (Type q1, Type q2) => prod_ord fast_string_ord (dict_ord patternT_ord) (q1, q2) + | (Type _, TFree _) => LESS + | (TFree _, Type _) => GREATER + | (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t) fun ptype_ord (PType p, PType q) = prod_ord (dict_ord patternT_ord) int_ord (swap p, swap q) @@ -376,6 +387,8 @@ facts are included. *) val special_fact_index = 45 (* FUDGE *) +fun eq_prod eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2) + val really_hopeless_get_kicked_out_iter = 5 (* FUDGE *) fun relevance_filter ctxt thres0 decay max_facts is_built_in_const @@ -437,7 +450,8 @@ trace_msg ctxt (fn () => "New or updated constants: " ^ commas (rel_const_tab' |> Symtab.dest - |> subtract (op =) (rel_const_tab |> Symtab.dest) + |> subtract (eq_prod (op =) (eq_list ptype_eq)) + (rel_const_tab |> Symtab.dest) |> map string_of_hyper_pconst)); map (fst o fst) accepts @ (if remaining_max = 0 then