17 |
17 |
18 datatype locality = |
18 datatype locality = |
19 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained |
19 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained |
20 |
20 |
21 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
21 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
22 datatype soundness = Sound_Modulo_Infinity | Sound |
22 datatype strictness = Strict | Non_Strict |
23 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars |
23 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars |
24 datatype type_level = |
24 datatype type_level = |
25 All_Types | |
25 All_Types | |
26 Noninf_Nonmono_Types of soundness * granularity | |
26 Noninf_Nonmono_Types of strictness * granularity | |
27 Fin_Nonmono_Types of granularity | |
27 Fin_Nonmono_Types of granularity | |
28 Const_Arg_Types | |
28 Const_Arg_Types | |
29 No_Types |
29 No_Types |
30 type type_enc |
30 type type_enc |
31 |
31 |
86 val is_type_enc_higher_order : type_enc -> bool |
86 val is_type_enc_higher_order : type_enc -> bool |
87 val polymorphism_of_type_enc : type_enc -> polymorphism |
87 val polymorphism_of_type_enc : type_enc -> polymorphism |
88 val level_of_type_enc : type_enc -> type_level |
88 val level_of_type_enc : type_enc -> type_level |
89 val is_type_enc_quasi_sound : type_enc -> bool |
89 val is_type_enc_quasi_sound : type_enc -> bool |
90 val is_type_enc_fairly_sound : type_enc -> bool |
90 val is_type_enc_fairly_sound : type_enc -> bool |
91 val type_enc_from_string : soundness -> string -> type_enc |
91 val type_enc_from_string : strictness -> string -> type_enc |
92 val adjust_type_enc : atp_format -> type_enc -> type_enc |
92 val adjust_type_enc : atp_format -> type_enc -> type_enc |
93 val mk_aconns : |
93 val mk_aconns : |
94 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula |
94 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula |
95 val unmangled_const : string -> string * (string, 'b) ho_term list |
95 val unmangled_const : string -> string * (string, 'b) ho_term list |
96 val unmangled_const_name : string -> string |
96 val unmangled_const_name : string -> string |
544 datatype locality = |
544 datatype locality = |
545 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained |
545 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained |
546 |
546 |
547 datatype order = First_Order | Higher_Order |
547 datatype order = First_Order | Higher_Order |
548 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
548 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
549 datatype soundness = Sound_Modulo_Infinity | Sound |
549 datatype strictness = Strict | Non_Strict |
550 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars |
550 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars |
551 datatype type_level = |
551 datatype type_level = |
552 All_Types | |
552 All_Types | |
553 Noninf_Nonmono_Types of soundness * granularity | |
553 Noninf_Nonmono_Types of strictness * granularity | |
554 Fin_Nonmono_Types of granularity | |
554 Fin_Nonmono_Types of granularity | |
555 Const_Arg_Types | |
555 Const_Arg_Types | |
556 No_Types |
556 No_Types |
557 |
557 |
558 datatype type_enc = |
558 datatype type_enc = |
606 case try_unsuffixes ats s of |
606 case try_unsuffixes ats s of |
607 SOME s => (constr Ghost_Type_Arg_Vars, s) |
607 SOME s => (constr Ghost_Type_Arg_Vars, s) |
608 | NONE => (constr All_Vars, s)) |
608 | NONE => (constr All_Vars, s)) |
609 | NONE => fallback s |
609 | NONE => fallback s |
610 |
610 |
611 fun type_enc_from_string soundness s = |
611 fun type_enc_from_string strictness s = |
612 (case try (unprefix "poly_") s of |
612 (case try (unprefix "poly_") s of |
613 SOME s => (SOME Polymorphic, s) |
613 SOME s => (SOME Polymorphic, s) |
614 | NONE => |
614 | NONE => |
615 case try (unprefix "raw_mono_") s of |
615 case try (unprefix "raw_mono_") s of |
616 SOME s => (SOME Raw_Monomorphic, s) |
616 SOME s => (SOME Raw_Monomorphic, s) |
618 case try (unprefix "mono_") s of |
618 case try (unprefix "mono_") s of |
619 SOME s => (SOME Mangled_Monomorphic, s) |
619 SOME s => (SOME Mangled_Monomorphic, s) |
620 | NONE => (NONE, s)) |
620 | NONE => (NONE, s)) |
621 ||> (pair All_Types |
621 ||> (pair All_Types |
622 |> try_nonmono Fin_Nonmono_Types bangs |
622 |> try_nonmono Fin_Nonmono_Types bangs |
623 |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries) |
623 |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries) |
624 |> (fn (poly, (level, core)) => |
624 |> (fn (poly, (level, core)) => |
625 case (core, (poly, level)) of |
625 case (core, (poly, level)) of |
626 ("simple", (SOME poly, _)) => |
626 ("simple", (SOME poly, _)) => |
627 (case (poly, level) of |
627 (case (poly, level) of |
628 (Polymorphic, All_Types) => |
628 (Polymorphic, All_Types) => |
1279 (* These types witness that the type classes they belong to allow infinite |
1279 (* These types witness that the type classes they belong to allow infinite |
1280 models and hence that any types with these type classes is monotonic. *) |
1280 models and hence that any types with these type classes is monotonic. *) |
1281 val known_infinite_types = |
1281 val known_infinite_types = |
1282 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}] |
1282 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}] |
1283 |
1283 |
1284 fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T = |
1284 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T = |
1285 soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T |
1285 strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T |
1286 |
1286 |
1287 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are |
1287 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are |
1288 dangerous because their "exhaust" properties can easily lead to unsound ATP |
1288 dangerous because their "exhaust" properties can easily lead to unsound ATP |
1289 proofs. On the other hand, all HOL infinite types can be given the same |
1289 proofs. On the other hand, all HOL infinite types can be given the same |
1290 models in first-order logic (via Löwenheim-Skolem). *) |
1290 models in first-order logic (via Löwenheim-Skolem). *) |
1291 |
1291 |
1292 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true |
1292 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true |
1293 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, |
1293 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, |
1294 maybe_nonmono_Ts, ...} |
1294 maybe_nonmono_Ts, ...} |
1295 (Noninf_Nonmono_Types (soundness, grain)) T = |
1295 (Noninf_Nonmono_Types (strictness, grain)) T = |
1296 grain = Ghost_Type_Arg_Vars orelse |
1296 grain = Ghost_Type_Arg_Vars orelse |
1297 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso |
1297 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso |
1298 not (exists (type_instance ctxt T) surely_infinite_Ts orelse |
1298 not (exists (type_instance ctxt T) surely_infinite_Ts orelse |
1299 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso |
1299 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso |
1300 is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts |
1300 is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts |
1301 T))) |
1301 T))) |
1302 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts, |
1302 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts, |
1303 maybe_nonmono_Ts, ...} |
1303 maybe_nonmono_Ts, ...} |
1304 (Fin_Nonmono_Types grain) T = |
1304 (Fin_Nonmono_Types grain) T = |
1305 grain = Ghost_Type_Arg_Vars orelse |
1305 grain = Ghost_Type_Arg_Vars orelse |
2044 {maybe_finite_Ts = [@{typ bool}], |
2044 {maybe_finite_Ts = [@{typ bool}], |
2045 surely_finite_Ts = [@{typ bool}], |
2045 surely_finite_Ts = [@{typ bool}], |
2046 maybe_infinite_Ts = known_infinite_types, |
2046 maybe_infinite_Ts = known_infinite_types, |
2047 surely_infinite_Ts = |
2047 surely_infinite_Ts = |
2048 case level of |
2048 case level of |
2049 Noninf_Nonmono_Types (Sound, _) => [] |
2049 Noninf_Nonmono_Types (Strict, _) => [] |
2050 | _ => known_infinite_types, |
2050 | _ => known_infinite_types, |
2051 maybe_nonmono_Ts = [@{typ bool}]} |
2051 maybe_nonmono_Ts = [@{typ bool}]} |
2052 |
2052 |
2053 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it |
2053 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it |
2054 out with monotonicity" paper presented at CADE 2011. *) |
2054 out with monotonicity" paper presented at CADE 2011. *) |
2057 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) |
2057 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) |
2058 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts, |
2058 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts, |
2059 surely_infinite_Ts, maybe_nonmono_Ts}) = |
2059 surely_infinite_Ts, maybe_nonmono_Ts}) = |
2060 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then |
2060 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then |
2061 case level of |
2061 case level of |
2062 Noninf_Nonmono_Types (soundness, _) => |
2062 Noninf_Nonmono_Types (strictness, _) => |
2063 if exists (type_instance ctxt T) surely_infinite_Ts orelse |
2063 if exists (type_instance ctxt T) surely_infinite_Ts orelse |
2064 member (type_equiv ctxt) maybe_finite_Ts T then |
2064 member (type_equiv ctxt) maybe_finite_Ts T then |
2065 mono |
2065 mono |
2066 else if is_type_kind_of_surely_infinite ctxt soundness |
2066 else if is_type_kind_of_surely_infinite ctxt strictness |
2067 surely_infinite_Ts T then |
2067 surely_infinite_Ts T then |
2068 {maybe_finite_Ts = maybe_finite_Ts, |
2068 {maybe_finite_Ts = maybe_finite_Ts, |
2069 surely_finite_Ts = surely_finite_Ts, |
2069 surely_finite_Ts = surely_finite_Ts, |
2070 maybe_infinite_Ts = maybe_infinite_Ts, |
2070 maybe_infinite_Ts = maybe_infinite_Ts, |
2071 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T, |
2071 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T, |