7: module LiquidArray where 8: 9: import Language.Haskell.Liquid.Prelude (liquidAssume) 10: 11: {-@ LIQUID "--no-termination" @-}
We define a Vector of a
s implemented as a function from Int
to a
s
22: data Vec a = V (Int -> a)
We parameterize the definition with two abstract refinements:
33: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop> 34: = V {a :: i:Int<dom> -> a <rng i>} 35: @-}
dom
: describes the domain
rng
: describes each value with respect to its index
47: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop> 48: = V {a :: i:Int<dom> -> a <rng i>} 49: @-}
A vector of Int
defined on values less than 42
containing values equal to their index:
59: {-@ type IdVec = 60: Vec <{\v -> (v < 42)}, {\j v -> (v = j)}> Int 61: @-}
67: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop> 68: = V {a :: i:Int<dom> -> a <rng i>} 69: @-}
A vector defined on the range [0..n)
with its last element equal to 0
:
78: {-@ type ZeroTerm N = 79: Vec <{\v -> (0 <= v && v < N)}, {\j v -> (j = N - 1 => v = 0)}> Int 80: @-}
86: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop> 87: = V {a :: i:Int<dom> -> a <rng i>} 88: @-}
A vector defined on integers whose value at index j
is either 0
or the j
th fibonacci:
99: {-@ type FibV = 100: Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int 101: @-}
We give appropriate types to vector operations (empty, set, get...)
empty
returns a Vector whose domain is always false
123: {-@ empty :: forall <p :: Int -> a -> Prop>. Vec < {v:Int | 0=1}, p> a @-} 124: 125: empty :: Vec a 126: forall a <p :: (GHC.Types.Int)-> a-> Bool>. (LiquidArray.Vec <false, \_ VV -> p> a)empty = ({VV : (GHC.Types.Int) | false} -> {VV : a | false}) -> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false})V (({VV : (GHC.Types.Int) | false} -> {VV : a | false}) -> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false})) -> ({VV : (GHC.Types.Int) | false} -> {VV : a | false}) -> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false})$ {VV : (GHC.Types.Int) | false} -> {VV : a | false}\_ -> ([(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | ((len VV) >= 0) && ((sumLens VV) >= 0)}"Empty array!")
If i
satisfies the domain then if we get
the i
th element of an array, the result should satisfy the range at i
139: {-@ get :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>. 140: i: Int<d> 141: -> a: Vec<d, r> a 142: -> a<r i> @-} 143: 144: get :: Int -> Vec a -> a 145: forall a <r :: (GHC.Types.Int)-> a-> Bool, d :: (GHC.Types.Int)-> Bool>. i:{VV : (GHC.Types.Int)<d> | true} -> (LiquidArray.Vec <d, \_ VV -> r> a) -> {VV : a<r i> | true}get {VV : (GHC.Types.Int) | ((papp1 d VV))}i (V f) = i:{VV : (GHC.Types.Int) | ((papp1 d VV))} -> {VV : a | ((papp2 r VV i))}f {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == i)}i
If i
satisfies the domain then if we set
the i
th element of a Vector to a value that satisfies range at i
, then Vector's domain will be extended with i
159: {-@ set :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>. 160: i: Int<d> 161: -> x: a<r i> 162: -> a: Vec < {v:Int<d> | v != i}, r> a 163: -> Vec <d, r> a @-} 164: 165: set :: Int -> a -> Vec a -> Vec a 166: forall a <r :: (GHC.Types.Int)-> a-> Bool, d :: (GHC.Types.Int)-> Bool>. i:{VV : (GHC.Types.Int)<d> | true} -> {VV : a<r i> | true} -> (LiquidArray.Vec <d & (VV /= i), \_ VV -> r> a) -> (LiquidArray.Vec <d, \_ VV -> r> a)set {VV : (GHC.Types.Int) | ((papp1 d VV))}i {VV : a | ((papp2 r VV i))}v (V f) = (i:{VV : (GHC.Types.Int) | ((papp1 d VV))} -> {VV : a | ((papp2 r VV i))}) -> (LiquidArray.Vec <((papp1 d VV)), \x1 VV -> ((papp2 r VV x1))> a)V ((x5:{VV : (GHC.Types.Int) | ((papp1 d VV))} -> {VV : a | ((papp2 r VV x5))}) -> (LiquidArray.Vec <((papp1 d VV)), \x2 VV -> ((papp2 r VV x2))> a)) -> (x5:{VV : (GHC.Types.Int) | ((papp1 d VV))} -> {VV : a | ((papp2 r VV x5))}) -> (LiquidArray.Vec <((papp1 d VV)), \x2 VV -> ((papp2 r VV x2))> a)$ k:{VV : (GHC.Types.Int) | ((papp1 d VV))} -> {VV : a | ((papp2 r VV k))}\{VV : (GHC.Types.Int) | ((papp1 d VV))}k -> if {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == k)}k x1:{VV : (GHC.Types.Int) | ((papp1 d VV))} -> x2:{VV : (GHC.Types.Int) | ((papp1 d VV))} -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}== {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == i)}i then {VV : a | ((papp2 r VV i)) && (VV == v)}v else i:{VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV /= i)} -> {VV : a | ((papp2 r VV i))}f {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == k)}k
173: type FibV = 174: Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int
Where fib
is an uninterprented function
180: {-@ measure fib :: Int -> Int @-}
We used fib
to define the axiom_fib
187: {-@ predicate Fib I = 188: (fib i) = (if (i <= 1) then 1 else ((fib (i-1)) + (fib (i-2)))) 189: @-} 190: 191: {-@ assume axiom_fib :: i:Int -> {v: Bool | ((Prop v) <=> (Fib i))} @-} 192: 193: axiom_fib :: Int -> Bool 194: i:(GHC.Types.Int) -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib (GHC.Types.Int)i = forall a. aundefined
Now we can efficiently compute the i
th fibonacci number
203: {-@ fastFib :: x:Int -> {v:Int | v = fib(x)} @-} 204: fastFib :: Int -> Int 205: x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (fib x))}fastFib (GHC.Types.Int)n = ((LiquidArray.Vec <false, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))}) -> {VV : (GHC.Types.Int) | (VV == (fib n))}snd (((LiquidArray.Vec <false, \x2 VV -> ((VV /= 0) => (VV == (fib x2)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))}) -> {VV : (GHC.Types.Int) | (VV == (fib n))}) -> ((LiquidArray.Vec <false, \x2 VV -> ((VV /= 0) => (VV == (fib x2)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))}) -> {VV : (GHC.Types.Int) | (VV == (fib n))}$ (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) -> i:(GHC.Types.Int) -> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo (forall <rng :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, dom :: (GHC.Types.Int)-> Bool>. (i:{VV : (GHC.Types.Int)<dom> | true} -> {VV : (GHC.Types.Int)<rng i> | ((VV /= 0) => (VV == (fib n))) && (VV == 0)}) -> (LiquidArray.Vec <dom, rng> {VV : (GHC.Types.Int) | ((VV /= 0) => (VV == (fib n))) && (VV == 0)})V ((GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (0 : int))}\_ -> {VV : (GHC.Types.Int) | (VV == (0 : int))}0)) {VV : (GHC.Types.Int) | (VV == n)}n
212: {-@ fibMemo :: FibV -> i:Int -> (FibV, {v: Int | v = (fib i)}) @-} 213: 214: fibMemo :: Vec Int -> Int -> (Vec Int, Int) 215: (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) -> i:(GHC.Types.Int) -> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int))t (GHC.Types.Int)i 216: | {VV : (GHC.Types.Int) | (VV == i)}i x1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : (GHC.Types.Int) | (VV == (1 : int))}1 217: = forall a b <p2 :: a-> b-> Bool>. x1:a -> x2:{VV : b<p2 x1> | true} -> {VV : (a, b)<p2> | ((fst VV) == x1) && ((snd VV) == x2)}({VV : (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t, x1:(GHC.Types.Bool) -> {VV : (GHC.Types.Int) | (VV == 1) && (VV > 0) && (VV >= i)} -> {VV : (GHC.Types.Int) | ((Prop x1)) && (VV == 1) && (VV > 0) && (VV >= i)}liquidAssume (i:(GHC.Types.Int) -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib {VV : (GHC.Types.Int) | (VV == i)}i) ({VV : (GHC.Types.Int) | (VV == (1 : int))}1 :: Int)) 218: 219: | otherwise 220: = case forall <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>. i:{VV : (GHC.Types.Int)<d> | true} -> (LiquidArray.Vec <d, \_ VV -> r> (GHC.Types.Int)) -> {VV : (GHC.Types.Int)<r i> | true}get {VV : (GHC.Types.Int) | (VV == i)}i {VV : (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t of 221: 0 -> let ({VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t1)}t1, {VV : (GHC.Types.Int) | (VV == n1)}n1) = (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) -> i:(GHC.Types.Int) -> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo {VV : (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t ({VV : (GHC.Types.Int) | (VV == i)}ix1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1 : int))}1) 222: ({VV : (LiquidArray.Vec <(VV /= i), \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t2)}t2, {VV : (GHC.Types.Int) | (VV == n2)}n2) = (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) -> i:(GHC.Types.Int) -> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo {VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t1) && (VV == t1)}t1 ({VV : (GHC.Types.Int) | (VV == i)}ix1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (2 : int))}2) 223: (GHC.Types.Int)n = x1:(GHC.Types.Bool) -> (GHC.Types.Int) -> {VV : (GHC.Types.Int) | ((Prop x1))}liquidAssume (i:(GHC.Types.Int) -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib {VV : (GHC.Types.Int) | (VV == i)}i) ({VV : (GHC.Types.Int) | (VV == n1) && (VV == n1)}n1 x1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == n2) && (VV == n2)}n2) 224: in forall a b <p2 :: a-> b-> Bool>. x1:a -> x2:{VV : b<p2 x1> | true} -> {VV : (a, b)<p2> | ((fst VV) == x1) && ((snd VV) == x2)}(forall <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>. i:{VV : (GHC.Types.Int)<d> | true} -> {VV : (GHC.Types.Int)<r i> | true} -> (LiquidArray.Vec <d & (VV /= i), \_ VV -> r> (GHC.Types.Int)) -> (LiquidArray.Vec <d, \_ VV -> r> (GHC.Types.Int))set {VV : (GHC.Types.Int) | (VV == i)}i {VV : (GHC.Types.Int) | (VV == n)}n {VV : (LiquidArray.Vec <(VV /= i), \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t2) && (VV == t2)}t2, {VV : (GHC.Types.Int) | (VV == n)}n) 225: n -> {VV : ({VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t)}, {VV : (GHC.Types.Int) | (VV == (fib i)) && (VV /= 0)})<\_ VV -> (VV == (fib i)) && (VV /= 0)> | ((fst VV) == t)}({VV : (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t, {VV : (GHC.Types.Int) | ((VV /= 0) => (VV == (fib i)))}n)