-
Notifications
You must be signed in to change notification settings - Fork 0
/
LList2.hs
34 lines (26 loc) · 1 KB
/
LList2.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
-- | https://github.com/ucsd-progsys/liquidhaskell/issues/889
{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--no-termination" @-}
import Language.Haskell.Liquid.ProofCombinators
{-@ type LListN a N = {v:LList a | (sz v) == N} @-}
{-@ data LList [sz] a = Nil | Cons {hd :: a, tl :: LList a} @-}
data LList a = Nil | Cons a (LList a)
{-@ measure sz @-}
{-@ sz :: LList a -> Nat @-}
sz :: LList a -> Int
sz Nil = 0
sz (Cons x xs) = 1 + sz xs
{-@ measure inf :: Int @-}
{-@ invariant {v:Int | v < inf} @-}
-- | sz (Cons x xs) == inf => sz xs = inf
{-@ tailInfProof :: l:(LListN a inf) -> {sz (select_Cons_2 l) == inf} @-}
tailInfProof :: LList a -> Proof
tailInfProof l@(Cons x xs)
= sz l
==. 1 + sz xs
*** QED
{-@ takeFromInfList :: xs:(LListN a inf) -> n:Nat -> (LListN a n) @-}
takeFromInfList :: (LList a) -> Int -> (LList a)
takeFromInfList _ 0 = Nil
takeFromInfList l@(Cons x xs) n = Cons (byTheorem x (tailInfProof l)) (takeFromInfList xs (n - 1))