content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE Arrows #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DerivingVia #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PartialTypeSignatures #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# OPTIONS_GHC
    -fsimpl-tick-factor=500
    -fno-warn-orphans
    -fno-warn-partial-type-signatures
  #-}
  
  -- | k-CFA analysis for PCF where numbers are approximated by intervals.
  module TypedAnalysis where
  
  import           Prelude hiding (not,Bounded,fail,(.),exp,read)
  
  import           Control.Category
  import           Control.Arrow hiding ((<+>))
  import qualified Control.Arrow.Fix as Fix
  import           Control.Arrow.Fail as Fail
  import           Control.Arrow.Environment as Env
  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
  import           Control.Arrow.Store
  import qualified Control.Arrow.Store as Store
  import qualified Control.Arrow.Utils as ArrowUtils
  import           Control.Arrow.Fix.Context
  import           Control.Arrow.Transformer.Value
  import           Control.Arrow.Transformer.Abstract.Fix.Metrics as Metric
  import           Control.Arrow.Transformer.Abstract.Fix.ControlFlow
  import qualified Control.Arrow.Transformer.Abstract.FiniteEnvStore as M
  
  import           Control.DeepSeq
  
  import           Data.Hashed.Lazy
  import           Data.Hashable(Hashable(..))
  import           Data.Label
  import           Data.Order
  import           Data.Text (Text)
  import           Data.Utils
  import           Data.HashMap.Lazy (HashMap)
  import qualified Data.HashMap.Lazy as Map
  import qualified Data.Boolean as B
  import           Data.HashSet(HashSet)
  import qualified Data.HashSet as Set
  import           Data.Identifiable
  import           Prettyprinter
  import           Data.Profunctor
  import qualified Data.Lens as L
  
  import qualified Data.Abstract.MonotoneStore as S
  import qualified Data.Abstract.MonotoneErrors as E
  import qualified Data.Abstract.Boolean as B
  import           Data.Abstract.Terminating(Terminating)
  import           Data.Abstract.Closure (Closure)
  import           Data.Abstract.DiscretePowerset (Pow(Pow))
  import           Data.Abstract.CallString(CallString)
  import qualified Data.Abstract.Widening as W
  import           Data.Abstract.Stable
  
  import           GHC.Exts(IsString(..),toList)
  import           GHC.Generics(Generic)
  
  import           Text.Printf
  
  import           Syntax (LExpr,Expr(Apply,App),Literal(..) ,Op1(..),Op2(..),OpVar(..))
  import           GenericInterpreter as Generic
  
  type Cls = Closure Expr (HashSet Env)
  type Env = M.Env Text Addr
  type Store = S.Store Addr Val
  type Errors = E.Errors Text
  type Ctx = CallString Label
  -- -- Input and output type of the fixpoint.
  
  data Addr
    = VarA (Text,Label,Ctx)
    | LabelA (Label,Ctx)
    deriving stock (Eq,Generic)
    deriving anyclass (NFData)
    deriving PreOrd via Discrete Addr
  
  type Symbol = Text
  
  data Val
    = Top
    | NumVal Number
    | StringVal
    | CharVal
    | QuoteVal (Pow Symbol)
    | BoolVal B.Bool
    | ClosureVal Cls
    | ListVal List
    | VoidVal
    | Bottom
    deriving stock (Eq, Generic)
    deriving anyclass (NFData)
  
  data List
    = Nil
    | Cons (Pow Addr) (Pow Addr)
    | ConsNil (Pow Addr) (Pow Addr)
    deriving stock (Eq, Generic)
    deriving anyclass (NFData)
  
  data Number
    = IntVal
    | FloatVal
    | NumTop
    deriving stock (Eq, Generic)
    deriving anyclass (NFData)
  
  instance (ArrowCallSite Label c) => ArrowAlloc Addr (ValueT Val c) where
    alloc = proc (var,lab) -> do
      ctx <- Ctx.getCallSite -< ()
      returnA -< VarA (var,lab,ctx)
    {-# INLINE alloc #-}
    {-# SCC alloc #-}
  
  allocLabel :: (ArrowCallSite Label c) => c Label Addr
  allocLabel = proc l -> do
    ctx <- Ctx.getCallSite -< ()
    returnA -< LabelA (l,ctx)
  {-# INLINE allocLabel #-}
  {-# SCC allocLabel #-}
  
  instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowClosure Expr Cls c)
      => ArrowClosure Expr Val (ValueT Val c) where
    type Join y Val (ValueT Val c) = (Cls.Join y Cls c, Fail.Join y c)
    closure = ValueT $ proc e -> do
      cls <- Cls.closure -< e
      returnA -< ClosureVal cls
    apply (ValueT f) = ValueT $ proc (v,x) ->
      case v of
        ClosureVal cls -> Cls.apply f -< (cls,x)
        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."
        _ -> failString -< printf "Expected a closure, but got %s" (show v)
    {-# INLINE closure #-}
    {-# INLINE apply #-}
    {-# SCC closure #-}
    {-# SCC apply #-}
  
  instance (ArrowChoice c, ArrowComplete Val c, ArrowCallSite Label c, ArrowFail e c, ArrowStore Addr Val c, ArrowEnv Text Addr c,
            Store.Join Val c, Env.Join Addr c,Store.Join Addr c,Fail.Join Val c,IsString e)
      => IsVal Val (ValueT Val c) where
    type Join y (ValueT Val c) = (ArrowComplete y (ValueT Val c),Fail.Join y c)
    lit = proc x -> case x of
      Int _ -> returnA -< NumVal IntVal
      Float _ -> returnA -< NumVal FloatVal
      Rational _ -> returnA -< Bottom
      Bool True  -> returnA -< BoolVal B.True
      Bool False  -> returnA -< BoolVal B.False
      Char _ -> returnA -< StringVal
      String _ -> returnA -< StringVal
      Quote (Symbol sym) -> returnA -< QuoteVal $ singleton sym
      _ -> returnA -< Bottom
    {-# INLINE lit #-}
    {-# SCC lit #-}
  
    if_ = if__
    {-# INLINE if_ #-}
    {-# SCC if_ #-}
  
    nil_ = proc _ -> returnA -< ListVal Nil
    {-# INLINE nil_ #-}
    {-# SCC nil_ #-}
  
    cons_ = proc ((v1,l1),(v2,l2)) -> do
      a1 <- allocLabel -< l1
      a2 <- allocLabel -< l2
      write -< (a1,v1)
      write -< (a2,v2)
      returnA -< ListVal (Cons (singleton a1) (singleton a2))
    {-# INLINE cons_ #-}
    {-# SCC cons_ #-}
  
    void = proc _ -> returnA -< VoidVal
  
    op1_ = proc (op, x) -> case op of
      IsNumber -> returnA -< case x of
        NumVal _ -> BoolVal B.True
        Top -> BoolVal B.Top
        _ -> BoolVal B.False
      IsInteger -> returnA -< case x of
        NumVal IntVal -> BoolVal B.True
        Top -> BoolVal B.Top
        _ -> BoolVal B.False
      IsFloat -> returnA -< case x of
        NumVal FloatVal -> BoolVal B.True
        Top -> BoolVal B.Top
        _ -> BoolVal B.False
      IsRational -> returnA -< case x of
        NumVal IntVal -> BoolVal B.True
        NumVal FloatVal -> BoolVal B.True
        Top -> BoolVal B.Top
        _ -> BoolVal B.False
      IsBoolean -> returnA -< case x of
        BoolVal _ -> BoolVal B.True
        Top -> BoolVal B.Top
        _ -> BoolVal B.False
      IsCons -> returnA -< case x of
        ListVal (Cons _ _) -> BoolVal B.True
        ListVal (ConsNil _ _) -> BoolVal B.Top
        Top -> BoolVal B.Top
        _ -> BoolVal B.False
      IsNull -> returnA -< case x of
        ListVal Nil -> BoolVal B.True
        ListVal (ConsNil _ _) -> BoolVal B.Top
        Top -> BoolVal B.Top
        _ -> BoolVal B.False
      IsZero -> numToBool -< (op,x)
      IsPositive -> numToBool -< (op,x)
      IsNegative -> numToBool -< (op,x)
      IsOdd -> numToBool -< (op,x)
      IsEven -> numToBool -< (op,x)
      Abs -> numToNum -< (op,x)
      Floor -> numToNum' -< (op,x)
      Ceiling -> numToNum' -< (op,x)
      Log -> numToFloat -< (op,x)
      Not -> boolToBool B.not -< (op,x)
      Car -> car' -< x
      Cdr -> cdr' -< x
      Caar -> car' <<< car' -< x
      Cadr -> car' <<< cdr' -< x
      Cddr -> cdr' <<< cdr' -< x
      Caddr -> car' <<< cdr' <<< cdr' -< x
      Cadddr -> car' <<< cdr' <<< cdr' <<< cdr' -< x
      -- Error -> failString -< printf "error: %s" (show x)
      Random -> intToInt -< (op, x)
      NumberToString -> numToString -< (op, x)
      StringToSymbol -> stringToSym -< (op, x)
      SymbolToString -> symToString -< (op, x)
    {-# INLINABLE op1_ #-}
    {-# SCC op1_ #-}
  
    op2_ = proc (op, x, y) -> case op of
      Eqv -> returnA -< BoolVal $ eq x y
      Quotient -> intIntToInt -< (op,x,y)
      Remainder -> intIntToInt -< (op,x,y)
      Modulo -> intIntToInt -< (op,x,y)
      StringRef -> stringIntToChar -< (op,x,y)
    {-# INLINEABLE op2_ #-}
    {-# SCC op2_ #-}
  
    opvar_ = proc (op, xs) -> case op of
      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)
      Max -> numNTo -< (op,1,xs,foldl1 numLub xs)
      Min -> numNTo -< (op,1,xs,foldl1 numLub xs)
      Add -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
      Mul -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
      Sub -> numNTo -< (op,1,xs,foldl1 numLub xs)
      Div -> do
        numNTo -< (op,1,xs,foldl1 numLubDivision xs)
      Gcd -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
      Lcm -> numNTo -< (op,0,xs,foldl numLub (NumVal IntVal) xs)
      StringAppend -> stringNToString -< xs
    {-# INLINEABLE opvar_ #-}
    {-# SCC opvar_ #-}
  
  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__ #-}
  
  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 IntVal -> returnA -< NumVal IntVal
    NumVal FloatVal -> returnA -< NumVal FloatVal
    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 #-}
  
  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' #-}
  
  intToInt :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (Op1,Val) Val
  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)
  {-# INLINEABLE intToInt #-}
  {-# SCC intToInt #-}
  
  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
  numToBool = proc (op,v) -> case v of
    NumVal _ -> returnA -< BoolVal B.Top
    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)
  {-# INLINEABLE numToBool #-}
  {-# SCC numToBool #-}
  
  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
  intIntToInt = proc (op,v1,v2) -> case (v1,v2) of
    (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))
    _ -> 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])
  {-# INLINEABLE intIntToInt #-}
  {-# SCC intIntToInt #-}
  
  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 #-}
  
  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
  car' = proc v -> case v of
    ListVal l -> car -< l
    Top -> (returnA -< Top) <⊔> (err -< v)
    _ -> err -< v
    where
      err = proc v -> failString -< printf "Excpeted list as argument for car, but got %s" (show v)
  {-# INLINEABLE car' #-}
  {-# SCC car' #-}
  
  car :: (IsString e, Fail.Join Val c, Store.Join Val c, ArrowChoice c, ArrowFail e c, ArrowStore Addr Val c) => c List Val
  car = proc v -> case v of
    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
  {-# INLINEABLE car #-}
  {-# SCC car #-}
  
  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
  cdr' = proc v -> case v of
    ListVal l -> cdr -< l
    Top -> (returnA -< Top) <⊔> (err -< v)
    _ -> err -< v
    where
      err = proc v -> failString -< printf "Excpeted list as argument for cdr, but got %s" (show v)
  {-# INLINEABLE cdr' #-}
  {-# SCC cdr' #-}
  
  cdr :: (IsString e, ArrowChoice c, ArrowFail e c, ArrowStore Addr Val c, Fail.Join Val c, Store.Join Val c) => c List Val
  cdr = proc v -> case v of
    Cons _ y -> do
      vals <- ArrowUtils.map read' -< toList y
      returnA -< lub vals
    Nil -> failString -< "cannot cdr an empty list"
    ConsNil x y -> cdr -< Cons x y
  {-# INLINEABLE cdr #-}
  {-# SCC cdr #-}
  
  eq :: Val -> Val -> B.Bool
  eq v1 v2 = case (v1, v2) of
    (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
    (NumVal IntVal,NumVal IntVal) -> B.Top
    (NumVal FloatVal,NumVal FloatVal) -> B.Top
    (NumVal NumTop,NumVal _) -> B.Top
    (NumVal _,NumVal NumTop) -> B.Top
    (StringVal,StringVal) -> B.Top
    (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
      _ -> B.Top
    (_,_) -> B.False
  {-# SCC eq #-}
  
  numNTo :: (IsString e, Fail.Join Val c, ArrowFail e c, ArrowChoice c, ArrowComplete Val c) => c (OpVar,Int,[Val],Val) Val
  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)
  {-# INLINEABLE numNTo #-}
  {-# SCC numNTo #-}
  
  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)
  
  numLub :: Val -> Val -> Val
  numLub x y = case (x,y) of
    (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
  {-# SCC numLub #-}
  
  -- | 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
  -- @
  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
    (Top,_) -> Top
    (_,Top) -> Top
    (_,_) -> Bottom
  {-# SCC numLubDivision #-}
  
  isNum :: Val -> B.Bool
  isNum v = case v of
    NumVal _ -> B.True
    Top -> B.Top
    _ -> B.False
  {-# SCC isNum #-}
  
  instance (ArrowChoice c, IsString e, Fail.Join Val c, ArrowFail e c, ArrowComplete Val c)
      => ArrowComplete Val (ValueT Val c) where
    ValueT f <⊔> ValueT g = ValueT $ proc x -> (f -< x) <⊔> (g -< x)
    {-# INLINEABLE (<⊔>) #-}
  
  instance Hashable Addr
  instance Show Addr where show = show . pretty
  instance Pretty Addr where
    pretty (VarA (var,l,ctx)) = pretty var <> pretty l <> viaShow ctx
    pretty (LabelA (l,ctx)) = pretty (labelVal l) <> viaShow ctx
  
  instance Hashable Val
  instance Show Val where show = show . pretty
  instance Pretty Val where
    pretty (NumVal nv) = pretty nv
    pretty (BoolVal b) = pretty b
    pretty (ClosureVal cls) = pretty cls
    pretty StringVal = "string"
    pretty CharVal = "char"
    pretty (QuoteVal syms) = pretty ["'" <> sym | sym <- toList syms]
    pretty (ListVal l) = pretty l
    pretty VoidVal = "#<void>"
    pretty Top = "Top"
    pretty Bottom = "Bottom"
  instance Hashable List
  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"
  instance Hashable Number
  instance Show Number where show = show . pretty
  instance Pretty Number where
    pretty IntVal = "Int"
    pretty FloatVal = "Float"
    pretty NumTop = "NumTop"
  
  instance IsClosure Val (HashSet Env) where
    mapEnvironment f v = case v of
      ClosureVal c -> ClosureVal (mapEnvironment f c)
      _ -> v
    traverseEnvironment f v = case v of
      ClosureVal c -> ClosureVal <$> traverseEnvironment f c
      _ -> pure v
    {-# SCC mapEnvironment #-}
    {-# SCC traverseEnvironment #-}
  
  storeErrWidening :: W.Widening (Store,Errors)
  storeErrWidening (s1,e1) (s2,e2) =
    -- Because the store grows monotonically, we can assume that s1 ⊑ s2. For
    -- stabilization it remains to check that s2 ⊑ s1.
    (if (s2,e2) ⊑ (s1,e1) then Stable else Unstable, (s2,e2))
  
  instance PreOrd Val where
    Bottom ⊑ _ = True
    _ ⊑ Top = True
    NumVal nv1 ⊑ NumVal nv2 = nv1 ⊑ nv2
    StringVal ⊑ StringVal = True
    CharVal ⊑ CharVal = True
    QuoteVal sym1 ⊑ QuoteVal sym2 = sym1 ⊑ sym2
    BoolVal b1 ⊑ BoolVal b2 = b1 ⊑ b2
    ClosureVal c1 ⊑ ClosureVal c2 = c1 ⊑ c2
    ListVal l1 ⊑ ListVal l2 = l1 ⊑ l2
    VoidVal ⊑ VoidVal = True
    _ ⊑ _ = False
    {-# SCC (⊑) #-}
  
  instance Complete Val where
    Bottom ⊔ x = x
    x ⊔ Bottom = x
    NumVal nv1 ⊔ NumVal nv2 = NumVal (nv1 ⊔ nv2)
    StringVal ⊔ StringVal = StringVal
    CharVal ⊔ CharVal = CharVal
    QuoteVal sym1 ⊔ QuoteVal sym2 = QuoteVal (sym1 ⊔ sym2)
    BoolVal b1 ⊔ BoolVal b2 = BoolVal (b1 ⊔ b2)
    ClosureVal c1 ⊔ ClosureVal c2 = ClosureVal (c1 ⊔ c2)
    ListVal l1 ⊔ ListVal l2 = ListVal (l1 ⊔ l2)
    VoidVal ⊔ VoidVal = VoidVal
    _ ⊔ _ = Top
    {-# SCC (⊔) #-}
  
  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
  
  instance PreOrd Number where
    IntVal ⊑ IntVal = True
    FloatVal ⊑ FloatVal = True
    _ ⊑ NumTop = True
    _ ⊑ _ = False
  
  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
  
  instance Complete Number where
    IntVal ⊔ IntVal = IntVal
    FloatVal ⊔ FloatVal = FloatVal
    _ ⊔ _ = NumTop
  
  instance (Identifiable s, IsString s) => IsString (HashSet s) where
    fromString = singleton . fromString
  
  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]
  
  type In = ((Store,Errors),(Env,[Expr]))
  type Out = ((Store,Errors), Terminating Val)
  type In' = (Store,(Env,(Errors,[Expr])))
  type Out' = (Store,(Errors,Terminating Val))
  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)))
  
  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 #-}
  
  isFunctionBody :: In -> Bool
  isFunctionBody (_,(_,e)) = case e of
    Apply _ _:_ -> True
    _ -> False
  {-# INLINE isFunctionBody #-}
  
  isApplication :: In -> Bool 
  isApplication (_,(_,e)) = case e of 
    App _ _ _:_ -> True 
    _ -> False
  {-# INLINE isApplication #-}
  
  
  -- Pretty Printing of inputs and outputs
  
  printIn :: In -> Doc ann
  printIn ((store,_),(env,expr)) =
    vsep
    [ "EXPR:  " <> showFirst expr
    , "ENV:   " <> align (pretty (unhashed env))
    , "STORE: " <> align (pretty store)
    ]
  
  printOut :: Out -> Doc ann
  printOut ((store,errs),val) =
    vsep
    [ "RET:   " <> pretty val
    , "STORE: " <> align (pretty store)
    , "ERRORS:" <> align (pretty errs)
    ]
  
  printInExpr :: In -> Doc ann
  printInExpr (_,(_,expr)) = "EXPR:" <+> showFirst expr
  
  printOutVal :: Out -> Doc ann
  printOutVal (_,val) = "RET:" <+> pretty val
  
  showFirst :: Pretty x => [x] -> Doc ann
  showFirst (x:_) = pretty x
  showFirst [] = "[]"
  