{#abstractrefinements} ========================
7: module AbstractRefinements where 8: 9: import Prelude 10: import Language.Haskell.Liquid.Prelude 11: {-@ LIQUID "--no-termination" @-} 12: 13: o, no :: Int 14: maxInt :: Int -> Int -> Int
64: {-@ type Odd = {v:Int | (v mod 2) = 1} @-} 65: {-@ type Even = {v:Int | (v mod 2) = 0} @-}
77: maxInt :: Int -> Int -> Int 78: maxInt x y = if y <= x then x else yExample: `maxInt` ----------------- Has *many incomparable* refinement types
89: maxInt :: Nat -> Nat -> Nat 90: maxInt :: Even -> Even -> Even 91: maxInt :: Odd -> Odd -> Odd
133: max :: α -> α -> α 134: max x y = if y <= x then x else y
142: {-@ o :: Odd @-} 143: {VV : (Int) | ((VV mod 2) == 1)}o = forall <p :: (GHC.Types.Int)-> Bool>. {x3 : (Int)<p> | true} -> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (3 : int))}3 {x2 : (Int) | (x2 == (7 : int))}7 -- α := Odd 144: 145: {-@ e :: Even @-} 146: {VV : (Int) | ((VV mod 2) == 0)}e = forall <p :: (GHC.Types.Int)-> Bool>. {x3 : (Int)<p> | true} -> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (2 : int))}2 {x2 : (Int) | (x2 == (8 : int))}8 -- α := Even
155: max :: α -> α -> α 156: max x y = if y <= x then x else y
167: max :: (Ord α) => α -> α -> α
173: {-@ o :: Odd @-} 174: o = max 3 7 -- α := OddPolymorphic `(+)` in Haskell ---------------------------- ... but this is *unsound*!
182: max :: (Ord α) => α -> α -> α 183: (+) :: (Num α) => α -> α -> α
193: {-@ no :: Odd @-} 194: {VV : (Int) | ((VV mod 2) == 1)}no = {x2 : (Int) | (x2 == (3 : int))}3 x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ {x2 : (Int) | (x2 == (7 : int))}7 -- α := Odd !
213: {-@ maxInt :: forall <p :: Int -> Prop>. 214: Int<p> -> Int<p> -> Int<p> @-} 215: 216: forall <p :: (GHC.Types.Int)-> Bool>. {VV : (Int)<p> | true} -> {VV : (Int)<p> | true} -> {VV : (Int)<p> | true}maxInt {VV : (Int) | ((papp1 p VV))}x {VV : (Int) | ((papp1 p VV))}y = if {x3 : (Int) | ((papp1 p x3)) && (x3 == x)}x x1:{x6 : (Int) | ((papp1 p x6))} -> x2:{x6 : (Int) | ((papp1 p x6))} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}<= {x3 : (Int) | ((papp1 p x3)) && (x3 == y)}y then {x3 : (Int) | ((papp1 p x3)) && (x3 == y)}y else {x3 : (Int) | ((papp1 p x3)) && (x3 == x)}x
232: {-@ maxInt :: forall <p :: Int -> Prop>. 233: Int<p> -> Int<p> -> Int<p> @-} 234: 235: maxInt x y = if x <= y then y else x
` is `{v:Int | (p v)}`
250: {-@ maxInt :: forall <p :: Int -> Prop>. 251: Int<p> -> Int<p> -> Int<p> @-} 252: 253: maxInt x y = if x <= y then y else x
272: {-@ o' :: Odd @-} 273: {VV : (Int) | ((VV mod 2) == 1)}o' = forall <p :: (GHC.Types.Int)-> Bool>. {x3 : (Int)<p> | true} -> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (3 : int))}3 {x2 : (Int) | (x2 == (7 : int))}7 -- p := \v -> Odd v 274: 275: {-@ e' :: Even @-} 276: {VV : (Int) | ((VV mod 2) == 0)}e' = forall <p :: (GHC.Types.Int)-> Bool>. {x3 : (Int)<p> | true} -> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (2 : int))}2 {x2 : (Int) | (x2 == (8 : int))}8 -- p := \v -> Even v
289: {-@ type RGB = {v:_ | (0 <= v && v < 256)} @-} 290: 291: {-@ rgb :: RGB @-} 292: {v : (Int) | (v < 256) && (0 <= v)}rgb = forall <p :: (GHC.Types.Int)-> Bool>. {x3 : (Int)<p> | true} -> {x2 : (Int)<p> | true} -> {x1 : (Int)<p> | true}maxInt {x2 : (Int) | (x2 == (56 : int))}56 {x2 : (Int) | (x2 == (8 : int))}8Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4.