/
Base_LHAssumptions.hs
55 lines (41 loc) · 1.85 KB
/
Base_LHAssumptions.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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}
module GHC.Base_LHAssumptions where
import GHC.CString_LHAssumptions()
import GHC.Exts_LHAssumptions()
import GHC.Types_LHAssumptions()
import GHC.Base
import Data.Tuple_LHAssumptions()
{-@
assume GHC.Base.. :: forall <p :: b -> c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.
{xcmp::a, wcmp::b<q xcmp> |- c<p wcmp> <: c<r xcmp>}
(ycmp:b -> c<p ycmp>)
-> (zcmp:a -> b<q zcmp>)
-> xcmp:a -> c<r xcmp>
measure autolen :: forall a. a -> GHC.Types.Int
// Useless as compiled into GHC primitive, which is ignored
assume GHC.Base.assert :: {v:Bool | v } -> a -> a
instance measure len :: forall a. [a] -> GHC.Types.Int
len [] = 0
len (y:ys) = 1 + len ys
invariant {v: [a] | len v >= 0 }
assume GHC.Base.map :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}
assume GHC.Base.++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}
assume (GHC.Base.$) :: (a -> b) -> a -> b
assume GHC.Base.id :: x:a -> {v:a | v = x}
qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs > 0))
qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs = 0))
qualif ListZ(v: [a]) : (len v = 0)
qualif ListZ(v: [a]) : (len v >= 0)
qualif ListZ(v: [a]) : (len v > 0)
qualif CmpLen(v:[a], xs:[b]) : (len v = len xs )
qualif CmpLen(v:[a], xs:[b]) : (len v >= len xs )
qualif CmpLen(v:[a], xs:[b]) : (len v > len xs )
qualif CmpLen(v:[a], xs:[b]) : (len v <= len xs )
qualif CmpLen(v:[a], xs:[b]) : (len v < len xs )
qualif EqLen(v:int, xs: [a]) : (v = len xs )
qualif LenEq(v:[a], x: int) : (x = len v )
qualif LenDiff(v:[a], x:int) : (len v = x + 1)
qualif LenDiff(v:[a], x:int) : (len v = x - 1)
qualif LenAcc(v:int, xs:[a], n: int): (v = len xs + n)
@-}