module Blank where {-@ LIQUID "--no-termination" @-} data Vec a = V (Int -> a) {-@ data Vec a < dom :: Int -> Bool, rng :: Int -> a -> Bool > = V {a :: i:Int -> a } @-} {-@ empty :: forall

a -> Bool>. Vec <{v:Int|0=1}, p> a @-} empty = V \$ \_ -> error "empty vector!" {-@ set :: forall a Bool, r :: Int -> a -> Bool>. key: Int -> val: a -> vec: Vec<{v:Int| v /= key},r> a -> Vec a @-} set key val (V f) = V \$ \k -> if k == key then val else f k {- loop :: forall a

a -> Bool>. lo:Int -> hi:{Int | lo <= hi} -> base:a

-> f:(i:Int -> a

-> a

) -> a

@-} -- loop :: Int -> Int -> a -> (Int -> a -> a) -> a -- loop lo hi base f = go lo base -- where -- go i acc -- | i < hi = go (i+1) (f i acc) -- | otherwise = acc {-@ loop :: forall a

a -> Bool>. lo:Nat -> hi:{Nat | lo <= hi} -> base:Vec <{v:Nat | (v < lo)}, p> a -> f:(i:Nat -> Vec <{v:Nat | v < i}, p> a -> Vec <{v:Nat | v < i+1}, p> a) -> Vec <{v:Nat | v < hi}, p> a @-} loop :: Int -> Int -> Vec a -> (Int -> Vec a -> Vec a) -> Vec a loop lo hi base f = go lo base where go i acc | i < hi = go (i+1) (f i acc) | otherwise = acc {-@ predicate Seg V I J = (I <= V && V < J) @-} {-@ type IdVec N = Vec <{\v -> (Seg v 0 N)}, {\k v -> v=k}> Int @-} {-@ initUpto :: n:Nat -> (IdVec n) @-} initUpto n = loop 0 n empty (\i acc -> set i i acc) {-@ qualif Foo(v:Int): v < 0 @-}