TypedAnalysis.hs 24.6 KB
Newer Older
1
2
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Arrows #-}
Sven Keidel's avatar
Sven Keidel committed
3
{-# LANGUAGE DeriveAnyClass #-}
4
{-# LANGUAGE DeriveGeneric #-}
Sven Keidel's avatar
Sven Keidel committed
5
{-# LANGUAGE DerivingVia #-}
6
7
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
8
{-# LANGUAGE ImplicitParams #-}
9
10
11
12
13
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
Sven Keidel's avatar
Sven Keidel committed
14
{-# LANGUAGE TypeApplications #-}
15
16
17
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
Sven Keidel's avatar
Sven Keidel committed
18
19
20
21
22
{-# OPTIONS_GHC
  -fsimpl-tick-factor=500
  -fno-warn-orphans
  -fno-warn-partial-type-signatures
#-}
23

24
25
26
-- | k-CFA analysis for PCF where numbers are approximated by intervals.
module TypedAnalysis where

27
import           Prelude hiding (not,Bounded,fail,(.),exp,read)
28
29

import           Control.Category
Sven Keidel's avatar
Sven Keidel committed
30
import           Control.Arrow hiding ((<+>))
31
import qualified Control.Arrow.Fix as Fix
32
import           Control.Arrow.Fail as Fail
33
import           Control.Arrow.Environment as Env
34
35
36
37
import qualified Control.Arrow.Fix.Context as Ctx
import           Control.Arrow.Closure (ArrowClosure,IsClosure(..))
import qualified Control.Arrow.Closure as Cls
import           Control.Arrow.Order
38
39
import           Control.Arrow.Store
import qualified Control.Arrow.Store as Store
40
41
import qualified Control.Arrow.Utils as ArrowUtils
import           Control.Arrow.Fix.Context
42
import           Control.Arrow.Transformer.Value
43
import           Control.Arrow.Transformer.Abstract.Fix.Metrics as Metric
Sven Keidel's avatar
Sven Keidel committed
44
import           Control.Arrow.Transformer.Abstract.Fix.ControlFlow
45
import qualified Control.Arrow.Transformer.Abstract.FiniteEnvStore as M
46

Sven Keidel's avatar
Sven Keidel committed
47
import           Control.DeepSeq
48

49
50
import           Data.Hashed.Lazy
import           Data.Hashable(Hashable(..))
51
52
import           Data.Label
import           Data.Order
53
import           Data.Text (Text)
54
55
56
import           Data.Utils
import           Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as Map
57
import qualified Data.Boolean as B
58
import           Data.HashSet(HashSet)
Sven Keidel's avatar
Sven Keidel committed
59
import qualified Data.HashSet as Set
60
import           Data.Identifiable
Sven Keidel's avatar
Sven Keidel committed
61
import           Data.Text.Prettyprint.Doc
62
63
import           Data.Profunctor
import qualified Data.Lens as L
64

65
import qualified Data.Abstract.MonotoneStore as S
66
import qualified Data.Abstract.MonotoneErrors as E
67
68
69
import qualified Data.Abstract.Boolean as B
import           Data.Abstract.Terminating(Terminating)
import           Data.Abstract.Closure (Closure)
Sven Keidel's avatar
Sven Keidel committed
70
import           Data.Abstract.DiscretePowerset (Pow(Pow))
71
import           Data.Abstract.CallString(CallString)
72
73
import qualified Data.Abstract.Widening as W
import           Data.Abstract.Stable
74

Sven Keidel's avatar
Sven Keidel committed
75
import           GHC.Exts(IsString(..),toList)
76
77
import           GHC.Generics(Generic)

Sven Keidel's avatar
Sven Keidel committed
78
79
import           Text.Printf

80
import           Syntax (LExpr,Expr(Apply,App),Literal(..) ,Op1(..),Op2(..),OpVar(..))
81
import           GenericInterpreter as Generic
82

83
type Cls = Closure Expr (HashSet Env)
84
85
type Env = M.Env Text Addr
type Store = S.Store Addr Val
86
type Errors = E.Errors Text
87
type Ctx = CallString Label
Tobias Leon Hombücher's avatar
Tobias Leon Hombücher committed
88
-- -- Input and output type of the fixpoint.
89

Sven Keidel's avatar
Sven Keidel committed
90
data Addr
91
  = VarA (Text,Label,Ctx)
92
  | LabelA (Label,Ctx)
Sven Keidel's avatar
Sven Keidel committed
93
94
  deriving stock (Eq,Generic)
  deriving anyclass (NFData)
95
  deriving PreOrd via Discrete Addr
Sven Keidel's avatar
Sven Keidel committed
96

97
98
type Symbol = Text

Sven Keidel's avatar
Sven Keidel committed
99
100
data Val
  = Top
101
  | NumVal Number
102
  | StringVal
103
  | CharVal
104
  | QuoteVal (Pow Symbol)
Sven Keidel's avatar
Sven Keidel committed
105
106
107
  | BoolVal B.Bool
  | ClosureVal Cls
  | ListVal List
108
  | VoidVal
109
  | Bottom
Sven Keidel's avatar
Sven Keidel committed
110
111
  deriving stock (Eq, Generic)
  deriving anyclass (NFData)
Sven Keidel's avatar
Sven Keidel committed
112
113
114
115
116

data List
  = Nil
  | Cons (Pow Addr) (Pow Addr)
  | ConsNil (Pow Addr) (Pow Addr)
Sven Keidel's avatar
Sven Keidel committed
117
118
  deriving stock (Eq, Generic)
  deriving anyclass (NFData)
119

120
121
122
data Number
  = IntVal
  | FloatVal
123
124
125
126
  | NumTop
  deriving stock (Eq, Generic)
  deriving anyclass (NFData)

127
instance (ArrowCallSite Label c) => ArrowAlloc Addr (ValueT Val c) where
128
  alloc = proc (var,lab) -> do
129
    ctx <- Ctx.getCallSite -< ()
130
    returnA -< VarA (var,lab,ctx)
Sven Keidel's avatar
Sven Keidel committed
131
  {-# INLINE alloc #-}
132
  {-# SCC alloc #-}
133

134
allocLabel :: (ArrowCallSite Label c) => c Label Addr
135
allocLabel = proc l -> do
136
  ctx <- Ctx.getCallSite -< ()
137
  returnA -< LabelA (l,ctx)
Sven Keidel's avatar
Sven Keidel committed
138
{-# INLINE allocLabel #-}
139
{-# SCC allocLabel #-}
Tobias Leon Hombücher's avatar
Tobias Leon Hombücher committed
140

141
142
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowClosure Expr Cls c)
    => ArrowClosure Expr Val (ValueT Val c) where
143
  type Join y Val (ValueT Val c) = (Cls.Join y Cls c, Fail.Join y c)
Sven Keidel's avatar
Sven Keidel committed
144
  closure = ValueT $ proc e -> do
145
    cls <- Cls.closure -< e
Sven Keidel's avatar
Sven Keidel committed
146
    returnA -< ClosureVal cls
147
  apply (ValueT f) = ValueT $ proc (v,x) ->
Sven Keidel's avatar
Sven Keidel committed
148
149
    case v of
      ClosureVal cls -> Cls.apply f -< (cls,x)
150
      Top -> returnA -< error "Tried to apply a function, but the closure was Top. Continuing at this point would mean that the analysis result is unsound."
Sven Keidel's avatar
Sven Keidel committed
151
      _ -> failString -< printf "Expected a closure, but got %s" (show v)
Sven Keidel's avatar
Sven Keidel committed
152
153
  {-# INLINE closure #-}
  {-# INLINE apply #-}
154
155
  {-# SCC closure #-}
  {-# SCC apply #-}
Sven Keidel's avatar
Sven Keidel committed
156

157
instance (ArrowChoice c, ArrowComplete Val c, ArrowCallSite Label c, ArrowFail e c, ArrowStore Addr Val c, ArrowEnv Text Addr c,
158
          Store.Join Val c, Env.Join Addr c,Store.Join Addr c,Fail.Join Val c,IsString e)
159
    => IsVal Val (ValueT Val c) where
160
  type Join y (ValueT Val c) = (ArrowComplete y (ValueT Val c),Fail.Join y c)
161
  lit = proc x -> case x of
162
    Int _ -> returnA -< NumVal IntVal
163
    Float _ -> returnA -< NumVal FloatVal
164
    Rational _ -> returnA -< Bottom
Sven Keidel's avatar
Sven Keidel committed
165
166
167
168
    Bool True  -> returnA -< BoolVal B.True
    Bool False  -> returnA -< BoolVal B.False
    Char _ -> returnA -< StringVal
    String _ -> returnA -< StringVal
169
    Quote (Symbol sym) -> returnA -< QuoteVal $ singleton sym
Sven Keidel's avatar
Sven Keidel committed
170
    _ -> returnA -< Bottom
Sven Keidel's avatar
Sven Keidel committed
171
  {-# INLINE lit #-}
172
  {-# SCC lit #-}
Sven Keidel's avatar
Sven Keidel committed
173

174
175
  if_ = if__
  {-# INLINE if_ #-}
176
  {-# SCC if_ #-}
Sven Keidel's avatar
Sven Keidel committed
177

178
  nil_ = proc _ -> returnA -< ListVal Nil
179
  {-# INLINE nil_ #-}
180
  {-# SCC nil_ #-}
Sven Keidel's avatar
Sven Keidel committed
181

182
  cons_ = proc ((v1,l1),(v2,l2)) -> do
183
184
185
186
187
    a1 <- allocLabel -< l1
    a2 <- allocLabel -< l2
    write -< (a1,v1)
    write -< (a2,v2)
    returnA -< ListVal (Cons (singleton a1) (singleton a2))
Sven Keidel's avatar
Sven Keidel committed
188
  {-# INLINE cons_ #-}
189
  {-# SCC cons_ #-}
Sven Keidel's avatar
Sven Keidel committed
190

191
192
  void = proc _ -> returnA -< VoidVal

193
  op1_ = proc (op, x) -> case op of
194
    IsNumber -> returnA -< case x of
195
      NumVal _ -> BoolVal B.True
Sven Keidel's avatar
Sven Keidel committed
196
197
      Top -> BoolVal B.Top
      _ -> BoolVal B.False
198
    IsInteger -> returnA -< case x of
199
      NumVal IntVal -> BoolVal B.True
Sven Keidel's avatar
Sven Keidel committed
200
201
      Top -> BoolVal B.Top
      _ -> BoolVal B.False
202
    IsFloat -> returnA -< case x of
203
      NumVal FloatVal -> BoolVal B.True
Sven Keidel's avatar
Sven Keidel committed
204
205
      Top -> BoolVal B.Top
      _ -> BoolVal B.False
206
207
208
    IsRational -> returnA -< case x of
      NumVal IntVal -> BoolVal B.True
      NumVal FloatVal -> BoolVal B.True
Sven Keidel's avatar
Sven Keidel committed
209
210
      Top -> BoolVal B.Top
      _ -> BoolVal B.False
211
    IsBoolean -> returnA -< case x of
212
      BoolVal _ -> BoolVal B.True
Sven Keidel's avatar
Sven Keidel committed
213
214
      Top -> BoolVal B.Top
      _ -> BoolVal B.False
215
    IsCons -> returnA -< case x of
216
217
218
219
      ListVal (Cons _ _) -> BoolVal B.True
      ListVal (ConsNil _ _) -> BoolVal B.Top
      Top -> BoolVal B.Top
      _ -> BoolVal B.False
220
    IsNull -> returnA -< case x of
221
222
223
224
      ListVal Nil -> BoolVal B.True
      ListVal (ConsNil _ _) -> BoolVal B.Top
      Top -> BoolVal B.Top
      _ -> BoolVal B.False
225
226
227
228
229
    IsZero -> numToBool -< (op,x)
    IsPositive -> numToBool -< (op,x)
    IsNegative -> numToBool -< (op,x)
    IsOdd -> numToBool -< (op,x)
    IsEven -> numToBool -< (op,x)
Sven Keidel's avatar
Sven Keidel committed
230
    Abs -> numToNum -< (op,x)
231
232
    Floor -> numToNum' -< (op,x)
    Ceiling -> numToNum' -< (op,x)
233
234
    Log -> numToFloat -< (op,x)
    Not -> boolToBool B.not -< (op,x)
Sven Keidel's avatar
Sven Keidel committed
235
236
237
    Car -> car' -< x
    Cdr -> cdr' -< x
    Caar -> car' <<< car' -< x
238
    Cadr -> car' <<< cdr' -< x
Sven Keidel's avatar
Sven Keidel committed
239
    Cddr -> cdr' <<< cdr' -< x
240
241
    Caddr -> car' <<< cdr' <<< cdr' -< x
    Cadddr -> car' <<< cdr' <<< cdr' <<< cdr' -< x
242
    -- Error -> failString -< printf "error: %s" (show x)
243
244
245
246
    Random -> intToInt -< (op, x)
    NumberToString -> numToString -< (op, x)
    StringToSymbol -> stringToSym -< (op, x)
    SymbolToString -> symToString -< (op, x)
247
  {-# INLINABLE op1_ #-}
248
  {-# SCC op1_ #-}
Sven Keidel's avatar
Sven Keidel committed
249

250
  op2_ = proc (op, x, y) -> case op of
Sven Keidel's avatar
Sven Keidel committed
251
252
253
254
    Eqv -> returnA -< BoolVal $ eq x y
    Quotient -> intIntToInt -< (op,x,y)
    Remainder -> intIntToInt -< (op,x,y)
    Modulo -> intIntToInt -< (op,x,y)
255
    StringRef -> stringIntToChar -< (op,x,y)
256
  {-# INLINEABLE op2_ #-}
257
  {-# SCC op2_ #-}
Sven Keidel's avatar
Sven Keidel committed
258

259
  opvar_ = proc (op, xs) -> case op of
260
261
262
263
264
    Equal -> numNTo -< (op,1,xs,BoolVal $ if length xs == 1 then B.True else B.Top)
    Smaller -> numNTo -< (op,1,xs,BoolVal $ if length xs == 1 then B.True else B.Top)
    Greater -> numNTo -< (op,1,xs,BoolVal $ if length xs == 1 then B.True else B.Top)
    SmallerEqual -> numNTo -< (op,1,xs,BoolVal $ if length xs == 1 then B.True else B.Top)
    GreaterEqual -> numNTo -< (op,1,xs,BoolVal $ if length xs == 1 then B.True else B.Top)
Sven Keidel's avatar
Sven Keidel committed
265
266
    Max -> numNTo -< (op,1,xs,foldl1 numLub xs)
    Min -> numNTo -< (op,1,xs,foldl1 numLub xs)
267
268
    Add -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
    Mul -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
Sven Keidel's avatar
Sven Keidel committed
269
    Sub -> numNTo -< (op,1,xs,foldl1 numLub xs)
Sven Keidel's avatar
Sven Keidel committed
270
    Div -> do
271
      numNTo -< (op,1,xs,foldl1 numLubDivision xs)
272
273
    Gcd -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
    Lcm -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
Sven Keidel's avatar
Sven Keidel committed
274
    StringAppend -> stringNToString -< xs
275
  {-# INLINEABLE opvar_ #-}
276
  {-# SCC opvar_ #-}
Sven Keidel's avatar
Sven Keidel committed
277

278
279
280
281
282
283
284
285
if__ :: (ArrowChoice c, ArrowComplete z c) => c x z -> c y z -> c (Val,(x,y)) z
if__ f g = proc (v,(x,y)) -> case v of
    BoolVal B.False -> g -< y
    BoolVal B.Top -> (f -< x) <> (g -< y)
    Top -> (f -< x) <> (g -< y)
    _ -> f -< x
{-# INLINEABLE if__ #-}

286
numToNum :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
Sven Keidel's avatar
Sven Keidel committed
287
numToNum = proc (op,v) -> case v of
288
289
  NumVal IntVal -> returnA -< NumVal IntVal
  NumVal FloatVal -> returnA -< NumVal FloatVal
290
291
292
  Top -> (returnA -< Top) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
293
    err = proc (op,v) -> failString -< printf "expected a number as argument for %s, but got %s" (show op) (show v)
294
{-# INLINEABLE numToNum #-}
295
{-# SCC numToNum #-}
296

297
298
299
300
301
302
303
304
305
numToNum' :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
numToNum' = proc (op,v) -> case v of
  NumVal _ -> returnA -< NumVal IntVal
  Top -> (returnA -< Top) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected a number as argument for %s, but got %s" (show op) (show v)
{-# INLINEABLE numToNum' #-}
{-# SCC numToNum' #-}
306

307
intToInt :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
308
309
310
311
312
313
intToInt = proc (op,v) -> case v of
  NumVal IntVal -> returnA -< NumVal IntVal
  Top -> (returnA -< Top) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected an integer as argument for %s, but got %s" (show op) (show v)
314
{-# INLINEABLE intToInt #-}
315
{-# SCC intToInt #-}
Sven Keidel's avatar
Sven Keidel committed
316

317
318
319
320
321
322
323
324
325
326
327
numToFloat :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
numToFloat = proc (op,v) -> case v of
  NumVal _ -> returnA -< NumVal FloatVal
  Top -> (returnA -< NumVal FloatVal) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected a number as argument for %s, but got %s" (show op) (show v)
{-# INLINEABLE numToFloat #-}
{-# SCC numToFloat #-}

numToBool :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
Sven Keidel's avatar
Sven Keidel committed
328
numToBool = proc (op,v) -> case v of
Sven Keidel's avatar
Sven Keidel committed
329
  NumVal _ -> returnA -< BoolVal B.Top
330
331
332
333
  Top -> (returnA -< BoolVal B.Top) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected a number as argument for %s, but got %s" (show op) (show v)
334
{-# INLINEABLE numToBool #-}
335
{-# SCC numToBool #-}
Sven Keidel's avatar
Sven Keidel committed
336

337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
boolToBool :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => (B.Bool -> B.Bool) -> c (Op1,Val) Val
boolToBool f = proc (op,v) -> case v of
  BoolVal b -> returnA -< BoolVal (f b)
  Top -> (returnA -< BoolVal B.Top) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected a bool as argument for %s, but got %s" (show op) (show v)
{-# INLINEABLE boolToBool #-}
{-# SCC boolToBool #-}

numToString :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
numToString = proc (op,v) -> case v of
  NumVal _ -> returnA -< StringVal
  Top -> (returnA -< StringVal) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected a number as argument for %s, but got %s" (show op) (show v)
{-# INLINEABLE numToString #-}
{-# SCC numToString #-}

stringToSym :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
stringToSym = proc (op,v) -> case v of
  StringVal -> returnA -< QuoteVal top
  Top -> (returnA -< QuoteVal top) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected a string as argument for %s, but got %s" (show op) (show v)
{-# INLINEABLE stringToSym #-}
{-# SCC stringToSym #-}

symToString :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
symToString = proc (op,v) -> case v of
  QuoteVal _ -> returnA -< StringVal
  Top -> (returnA -< StringVal) <> (err -< (op,v))
  _ -> err -< (op,v)
  where
    err = proc (op,v) -> failString -< printf "expected a quote as argument for %s, but got %s" (show op) (show v)
{-# INLINEABLE symToString #-}
{-# SCC symToString #-}

intIntToInt :: (IsString e, Fail.Join Val c, ArrowChoice c, ArrowFail e c, ArrowComplete Val c) => c (Op2,Val,Val) Val
Sven Keidel's avatar
Sven Keidel committed
378
intIntToInt = proc (op,v1,v2) -> case (v1,v2) of
379
380
381
382
  (NumVal IntVal,NumVal IntVal) -> returnA -< NumVal IntVal
  (Top,Top) -> (returnA -< NumVal IntVal) <> (err -< (op,v1,v2))
  (Top,NumVal IntVal) -> (returnA -< NumVal IntVal) <> (err -< (op,v1,v2))
  (NumVal IntVal,Top) -> (returnA -< NumVal IntVal) <> (err -< (op,v1,v2))
383
384
385
  _ -> err -< (op,v1,v2)
  where
    err = proc (op,v1,v2) -> failString -< printf "expected a two ints as arguments for %s, but got %s" (show op) (show [v1,v2])
386
{-# INLINEABLE intIntToInt #-}
387
{-# SCC intIntToInt #-}
Sven Keidel's avatar
Sven Keidel committed
388

389
390
391
392
393
394
395
396
397
398
399
400
stringIntToChar :: (IsString e, Fail.Join Val c, ArrowChoice c, ArrowFail e c, ArrowComplete Val c) => c (Op2,Val,Val) Val
stringIntToChar = proc (op,v1,v2) -> case (v1,v2) of
  (StringVal, NumVal IntVal) -> returnA -< CharVal
  (Top,Top) -> (returnA -< CharVal) <> (err -< (op,v1,v2))
  (Top,NumVal IntVal) -> (returnA -< CharVal) <> (err -< (op,v1,v2))
  (StringVal,Top) -> (returnA -< CharVal) <> (err -< (op,v1,v2))
  _ -> err -< (op,v1,v2)
  where
    err = proc (op,v1,v2) -> failString -< printf "expected a two string and an int as arguments for %s, but got %s" (show op) (show [v1,v2])
{-# INLINEABLE stringIntToChar #-}
{-# SCC stringIntToChar #-}

401
car' :: (IsString e, Fail.Join Val c, Store.Join Val c, ArrowChoice c, ArrowFail e c, ArrowStore Addr Val c, ArrowComplete Val c) => c Val Val
Sven Keidel's avatar
Sven Keidel committed
402
403
car' = proc v -> case v of
  ListVal l -> car -< l
404
405
406
407
  Top -> (returnA -< Top) <> (err -< v)
  _ -> err -< v
  where
    err = proc v -> failString -< printf "Excpeted list as argument for car, but got %s" (show v)
408
{-# INLINEABLE car' #-}
409
{-# SCC car' #-}
Sven Keidel's avatar
Sven Keidel committed
410

411
car :: (IsString e, Fail.Join Val c, Store.Join Val c, ArrowChoice c, ArrowFail e c, ArrowStore Addr Val c) => c List Val
412
car = proc v -> case v of
Sven Keidel's avatar
Sven Keidel committed
413
414
415
416
417
  Cons x _ -> do
    vals <- ArrowUtils.map read' -< toList x
    returnA -< lub vals
  Nil -> failString -< "cannot car an empty list"
  ConsNil x y -> car -< Cons x y
418
{-# INLINEABLE car #-}
419
{-# SCC car #-}
Sven Keidel's avatar
Sven Keidel committed
420

421
cdr' :: (IsString e, Fail.Join Val c, Store.Join Val c, ArrowChoice c, ArrowFail e c, ArrowStore Addr Val c, ArrowComplete Val c) => c Val Val
Sven Keidel's avatar
Sven Keidel committed
422
423
cdr' = proc v -> case v of
  ListVal l -> cdr -< l
424
425
426
427
  Top -> (returnA -< Top) <> (err -< v)
  _ -> err -< v
  where
    err = proc v -> failString -< printf "Excpeted list as argument for cdr, but got %s" (show v)
428
{-# INLINEABLE cdr' #-}
429
{-# SCC cdr' #-}
Sven Keidel's avatar
Sven Keidel committed
430

431
cdr :: (IsString e, ArrowChoice c, ArrowFail e c, ArrowStore Addr Val c, Fail.Join Val c, Store.Join Val c) => c List Val
432
cdr = proc v -> case v of
Sven Keidel's avatar
Sven Keidel committed
433
434
435
  Cons _ y -> do
    vals <- ArrowUtils.map read' -< toList y
    returnA -< lub vals
436
  Nil -> failString -< "cannot cdr an empty list"
Tobias Leon Hombücher's avatar
Tobias Leon Hombücher committed
437
  ConsNil x y -> cdr -< Cons x y
438
{-# INLINEABLE cdr #-}
439
{-# SCC cdr #-}
Sven Keidel's avatar
Sven Keidel committed
440
441

eq :: Val -> Val -> B.Bool
442
eq v1 v2 = case (v1, v2) of
Sven Keidel's avatar
Sven Keidel committed
443
444
445
446
447
448
449
450
451
  (Top,_) -> B.Top
  (_,Top) -> B.Top
  (BoolVal b1,BoolVal b2) -> case (b1,b2) of
    (B.Top,_) -> B.Top
    (_,B.Top) -> B.Top
    (B.True,B.True) -> B.True
    (B.False,B.False) -> B.True
    (B.True,B.False) -> B.False
    (B.False,B.True) -> B.False
452
453
454
455
  (NumVal IntVal,NumVal IntVal) -> B.Top
  (NumVal FloatVal,NumVal FloatVal) -> B.Top
  (NumVal NumTop,NumVal _) -> B.Top
  (NumVal _,NumVal NumTop) -> B.Top
Sven Keidel's avatar
Sven Keidel committed
456
  (StringVal,StringVal) -> B.Top
Sven Keidel's avatar
Sven Keidel committed
457
458
  (QuoteVal sym1,QuoteVal sym2) -> case (sym1, sym2) of
    (Pow xs, Pow ys) | Set.size xs == 1 && Set.size ys == 1 -> if xs == ys then B.True else B.False
459
    _ -> B.Top
Sven Keidel's avatar
Sven Keidel committed
460
  (_,_) -> B.False
461
{-# SCC eq #-}
Sven Keidel's avatar
Sven Keidel committed
462

463
numNTo :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (OpVar,Int,[Val],Val) Val
Sven Keidel's avatar
Sven Keidel committed
464
465
466
467
468
469
470
471
472
numNTo = proc (op,minArity,xs,ret) ->
  if minArity <= length xs
  then case lub (map isNum xs) of
    B.True -> returnA -< ret
    B.False -> err -< (op,xs)
    B.Top -> (returnA -< ret) <> (err -< (op,xs))
  else failString -< printf "the operator %s requires at least %d arguments, but got %d" (show op) minArity
  where
    err = proc (op,xs) -> failString -< printf "expected a numbers as argument for %s, but got %s" (show op) (show xs)
473
{-# INLINEABLE numNTo #-}
474
{-# SCC numNTo #-}
Sven Keidel's avatar
Sven Keidel committed
475

Sven Keidel's avatar
Sven Keidel committed
476
477
478
479
480
481
stringNToString :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c [Val] Val
stringNToString = proc xs -> case xs of
  (StringVal:ys) -> stringNToString -< ys
  [] -> returnA -< StringVal
  (x:_) -> failString -< printf "Expected a String, but got %s" (show x)

Sven Keidel's avatar
Sven Keidel committed
482
483
numLub :: Val -> Val -> Val
numLub x y = case (x,y) of
484
485
486
487
488
489
490
491
492
493
  (NumVal FloatVal,NumVal FloatVal) -> NumVal FloatVal
  (NumVal IntVal,NumVal IntVal) -> NumVal IntVal
  (NumVal IntVal,NumVal _) -> NumVal NumTop
  (NumVal _,NumVal IntVal) -> NumVal NumTop
  (NumVal FloatVal,NumVal _) -> NumVal NumTop
  (NumVal _,NumVal FloatVal) -> NumVal NumTop
  (NumVal NumTop,NumVal NumTop) -> NumVal NumTop
  (Top,_) -> Top
  (_,Top) -> Top
  (_,_) -> Bottom
494
{-# SCC numLub #-}
495

496
497
498
499
500
501
-- | Handles the case that the result of a division may be a whole number or a
-- floating point number:
-- @
--   (integer? (/ 2 2)) -> #t
--   (integer? (/ 2 3)) -> #f
-- @
502
503
504
505
506
507
508
numLubDivision :: Val -> Val -> Val
numLubDivision x y = case (x,y) of
  (NumVal FloatVal,NumVal _) -> NumVal FloatVal
  (NumVal _,NumVal FloatVal) -> NumVal FloatVal
  (NumVal IntVal,NumVal IntVal) -> NumVal NumTop
  (NumVal NumTop,NumVal _) -> NumVal NumTop
  (NumVal _,NumVal NumTop) -> NumVal NumTop
Sven Keidel's avatar
Sven Keidel committed
509
510
511
  (Top,_) -> Top
  (_,Top) -> Top
  (_,_) -> Bottom
512
{-# SCC numLubDivision #-}
Sven Keidel's avatar
Sven Keidel committed
513

Sven Keidel's avatar
Sven Keidel committed
514
isNum :: Val -> B.Bool
Sven Keidel's avatar
Sven Keidel committed
515
isNum v = case v of
516
  NumVal _ -> B.True
Sven Keidel's avatar
Sven Keidel committed
517
518
  Top -> B.Top
  _ -> B.False
519
{-# SCC isNum #-}
Sven Keidel's avatar
Sven Keidel committed
520

521
instance (ArrowChoice c, IsString e, Fail.Join Val c, ArrowFail e c, ArrowComplete Val c)
522
    => ArrowComplete Val (ValueT Val c) where
523
  ValueT f <> ValueT g = ValueT $ proc x -> (f -< x) <> (g -< x)
524
  {-# INLINEABLE (<⊔>) #-}
525

Sven Keidel's avatar
Sven Keidel committed
526
instance Hashable Addr
Sven Keidel's avatar
Sven Keidel committed
527
528
instance Show Addr where show = show . pretty
instance Pretty Addr where
529
  pretty (VarA (var,l,ctx)) = pretty var <> pretty l <> viaShow ctx
Sven Keidel's avatar
Sven Keidel committed
530
  pretty (LabelA (l,ctx)) = pretty (labelVal l) <> viaShow ctx
531

Sven Keidel's avatar
Sven Keidel committed
532
instance Hashable Val
Sven Keidel's avatar
Sven Keidel committed
533
534
instance Show Val where show = show . pretty
instance Pretty Val where
535
536
537
  pretty (NumVal nv) = pretty nv
  pretty (BoolVal b) = pretty b
  pretty (ClosureVal cls) = pretty cls
538
539
  pretty StringVal = "string"
  pretty CharVal = "char"
540
  pretty (QuoteVal syms) = pretty ["'" <> sym | sym <- toList syms]
Sven Keidel's avatar
Sven Keidel committed
541
  pretty (ListVal l) = pretty l
542
  pretty VoidVal = "#<void>"
Sven Keidel's avatar
Sven Keidel committed
543
544
  pretty Top = "Top"
  pretty Bottom = "Bottom"
Sven Keidel's avatar
Sven Keidel committed
545
instance Hashable List
Sven Keidel's avatar
Sven Keidel committed
546
547
548
549
instance Pretty List where
  pretty Nil = "Nil"
  pretty (Cons a1 a2) = "Cons" <> parens (pretty a1 <> "," <> pretty a2)
  pretty (ConsNil a1 a2) = "Cons" <> parens (pretty a1 <> "," <> pretty a2) <> " ⊔ Nil"
550
instance Hashable Number
551
552
553
554
555
instance Show Number where show = show . pretty
instance Pretty Number where
  pretty IntVal = "Int"
  pretty FloatVal = "Float"
  pretty NumTop = "NumTop"
Sven Keidel's avatar
Sven Keidel committed
556

557
instance IsClosure Val (HashSet Env) where
Sven Keidel's avatar
Sven Keidel committed
558
559
  mapEnvironment f v = case v of
    ClosureVal c -> ClosureVal (mapEnvironment f c)
560
    _ -> v
Sven Keidel's avatar
Sven Keidel committed
561
562
  traverseEnvironment f v = case v of
    ClosureVal c -> ClosureVal <$> traverseEnvironment f c
563
    _ -> pure v
564
565
  {-# SCC mapEnvironment #-}
  {-# SCC traverseEnvironment #-}
Sven Keidel's avatar
Sven Keidel committed
566

567
568
storeErrWidening :: W.Widening (Store,Errors)
storeErrWidening (s1,e1) (s2,e2) =
569
570
  -- Because the store grows monotonically, we can assume that s1 ⊑ s2. For
  -- stabilization it remains to check that s2 ⊑ s1.
571
  (if (s2,e2)  (s1,e1) then Stable else Unstable, (s2,e2))
572

Sven Keidel's avatar
Sven Keidel committed
573
574
575
instance PreOrd Val where
  Bottom  _ = True
  _  Top = True
576
  NumVal nv1  NumVal nv2 = nv1  nv2
Sven Keidel's avatar
Sven Keidel committed
577
  StringVal  StringVal = True
578
  CharVal  CharVal = True
579
  QuoteVal sym1  QuoteVal sym2 = sym1  sym2
Sven Keidel's avatar
Sven Keidel committed
580
581
582
  BoolVal b1  BoolVal b2 = b1  b2
  ClosureVal c1  ClosureVal c2 = c1  c2
  ListVal l1  ListVal l2 = l1  l2
583
  VoidVal  VoidVal = True
Sven Keidel's avatar
Sven Keidel committed
584
  _  _ = False
585
  {-# SCC (⊑) #-}
Sven Keidel's avatar
Sven Keidel committed
586
587
588
589

instance Complete Val where
  Bottom  x = x
  x  Bottom = x
590
  NumVal nv1  NumVal nv2 = NumVal (nv1  nv2)
Sven Keidel's avatar
Sven Keidel committed
591
  StringVal  StringVal = StringVal
592
  CharVal  CharVal = CharVal
593
  QuoteVal sym1  QuoteVal sym2 = QuoteVal (sym1  sym2)
594
595
  BoolVal b1  BoolVal b2 = BoolVal (b1  b2)
  ClosureVal c1  ClosureVal c2 = ClosureVal (c1  c2)
Sven Keidel's avatar
Sven Keidel committed
596
  ListVal l1  ListVal l2 = ListVal (l1  l2)
597
  VoidVal  VoidVal = VoidVal
Sven Keidel's avatar
Sven Keidel committed
598
  _  _ = Top
599
  {-# SCC (⊔) #-}
Sven Keidel's avatar
Sven Keidel committed
600
601
602
603
604
605
606
607
608
609

instance PreOrd List where
  Nil  Nil = True
  Cons x1 x2  Cons y1 y2 = x1  y1 && x2  y2
  ConsNil x1 x2  ConsNil y1 y2 = x1  y1 && x2  y2

  Nil  ConsNil _ _ = True
  Cons x1 x2  ConsNil y1 y2 = x1  y1 && x2  y2
  _  _ = False

610
611
612
613
614
615
instance PreOrd Number where
  IntVal  IntVal = True
  FloatVal  FloatVal = True
  _  NumTop = True
  _  _ = False

Sven Keidel's avatar
Sven Keidel committed
616
617
618
619
620
621
622
623
624
625
626
627
instance Complete List where
  Nil  Nil = Nil
  Cons x1 x2  Cons y1 y2 = Cons (x1  y1) (x2  y2)
  ConsNil x1 x2  ConsNil y1 y2 = ConsNil (x1  y1) (x2  y2)

  Cons x1 x2  Nil = ConsNil x1 x2
  Nil  Cons x1 x2 = ConsNil x1 x2
  ConsNil x1 x2  Cons y1 y2 = ConsNil (x1  y1) (x2  y2)
  Cons x1 x2  ConsNil y1 y2 = ConsNil (x1  y1) (x2  y2)
  Nil  ConsNil y1 y2 = ConsNil y1 y2
  ConsNil y1 y2  Nil = ConsNil y1 y2

628
629
630
instance Complete Number where
  IntVal  IntVal = IntVal
  FloatVal  FloatVal = FloatVal
631
  _  _ = NumTop
632

633
634
instance (Identifiable s, IsString s) => IsString (HashSet s) where
  fromString = singleton . fromString
635

Sven Keidel's avatar
Sven Keidel committed
636
637
638
639
640
641
instance (Identifiable s, Pretty s) => Pretty (HashSet s) where
  pretty m = braces $ hsep (punctuate "," (pretty <$> toList m))

instance (Pretty k, Pretty v) => Pretty (HashMap k v) where
  pretty m = list [ pretty k <+> " -> " <> pretty v | (k,v) <- Map.toList m]

642
643
644
645
type In = ((Store,Errors),(Env,[Expr]))
type Out = ((Store,Errors), Terminating Val)
type In' = (Store,(Env,(Errors,[Expr])))
type Out' = (Store,(Errors,Terminating Val))
646
647
type Eval = (?sensitivity :: Int) => [(Text,Addr)] -> [LExpr] -> (CFG Expr, (Metric.Monotone In, Out'))
type Eval' = (?sensitivity :: Int) => [LExpr] -> (CFG Expr, (Metric.Monotone In, (Errors,Terminating Val)))
648
649
650
651
652
653
654

transform :: Profunctor c => Fix.FixpointAlgorithm (c In Out) -> Fix.FixpointAlgorithm (c In' Out')
transform = Fix.transform (L.iso (\(store,(env,(errs,exprs))) -> ((store,errs),(env,exprs)))
                                 (\((store,errs),(env,exprs)) -> (store,(env,(errs,exprs)))))
                          (L.iso (\(store,(errs,val)) -> ((store,errs),val))
                                 (\((store,errs),val) -> (store,(errs,val))))
{-# INLINE transform #-}
655

656
657
658
659
660
661
isFunctionBody :: In -> Bool
isFunctionBody (_,(_,e)) = case e of
  Apply _ _:_ -> True
  _ -> False
{-# INLINE isFunctionBody #-}

662
663
664
665
666
667
668
isApplication :: In -> Bool 
isApplication (_,(_,e)) = case e of 
  App _ _ _:_ -> True 
  _ -> False
{-# INLINE isApplication #-}


669
670
671
-- Pretty Printing of inputs and outputs

printIn :: In -> Doc ann
672
printIn ((store,_),(env,expr)) =
673
  vsep
674
  [ "EXPR:  " <> showFirst expr
675
  , "ENV:   " <> align (pretty (unhashed env))
676
  , "STORE: " <> align (pretty store)
677
678
  ]

679
printOut :: Out -> Doc ann
680
printOut ((store,errs),val) =
681
  vsep
682
  [ "RET:   " <> pretty val
683
  , "STORE: " <> align (pretty store)
684
  , "ERRORS:" <> align (pretty errs)
685
  ]
686
687
688
689
690

printInExpr :: In -> Doc ann
printInExpr (_,(_,expr)) = "EXPR:" <+> showFirst expr

printOutVal :: Out -> Doc ann
691
printOutVal (_,val) = "RET:" <+> pretty val
692
693
694
695

showFirst :: Pretty x => [x] -> Doc ann
showFirst (x:_) = pretty x
showFirst [] = "[]"