equal
deleted
inserted
replaced
18 datatype locality = |
18 datatype locality = |
19 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | |
19 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | |
20 Chained |
20 Chained |
21 |
21 |
22 datatype order = First_Order | Higher_Order |
22 datatype order = First_Order | Higher_Order |
23 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic |
23 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
24 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
24 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
25 datatype type_level = |
25 datatype type_level = |
26 All_Types | |
26 All_Types | |
27 Noninf_Nonmono_Types of soundness | |
27 Noninf_Nonmono_Types of soundness | |
28 Fin_Nonmono_Types | |
28 Fin_Nonmono_Types | |
520 datatype locality = |
520 datatype locality = |
521 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | |
521 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | |
522 Chained |
522 Chained |
523 |
523 |
524 datatype order = First_Order | Higher_Order |
524 datatype order = First_Order | Higher_Order |
525 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic |
525 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic |
526 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
526 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound |
527 datatype type_level = |
527 datatype type_level = |
528 All_Types | |
528 All_Types | |
529 Noninf_Nonmono_Types of soundness | |
529 Noninf_Nonmono_Types of soundness | |
530 Fin_Nonmono_Types | |
530 Fin_Nonmono_Types | |
542 |
542 |
543 fun type_enc_from_string soundness s = |
543 fun type_enc_from_string soundness s = |
544 (case try (unprefix "poly_") s of |
544 (case try (unprefix "poly_") s of |
545 SOME s => (SOME Polymorphic, s) |
545 SOME s => (SOME Polymorphic, s) |
546 | NONE => |
546 | NONE => |
547 case try (unprefix "mono_") s of |
547 case try (unprefix "raw_mono_") s of |
548 SOME s => (SOME Monomorphic, s) |
548 SOME s => (SOME Raw_Monomorphic, s) |
549 | NONE => |
549 | NONE => |
550 case try (unprefix "mangled_") s of |
550 case try (unprefix "mono_") s of |
551 SOME s => (SOME Mangled_Monomorphic, s) |
551 SOME s => (SOME Mangled_Monomorphic, s) |
552 | NONE => (NONE, s)) |
552 | NONE => (NONE, s)) |
553 ||> (fn s => |
553 ||> (fn s => |
554 (* "_query" and "_bang" are for the ASCII-challenged Metis and |
554 (* "_query" and "_bang" are for the ASCII-challenged Metis and |
555 Mirabelle. *) |
555 Mirabelle. *) |