{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# OPTIONS_GHC -Wno-missing-methods #-}

module Nix.Lint where

import           Control.Monad
import           Control.Monad.Catch
import           Control.Monad.Fix
import           Control.Monad.Reader           ( MonadReader )
import           Control.Monad.Ref
import           Control.Monad.ST
import           Control.Monad.Trans.Reader
import           Data.HashMap.Lazy              ( HashMap )
import qualified Data.HashMap.Lazy             as M
import           Data.List
import qualified Data.List.NonEmpty            as NE
import           Data.Text                      ( Text )
import qualified Data.Text                     as Text
import           Nix.Atoms
import           Nix.Context
import           Nix.Convert
import           Nix.Eval                       ( MonadEval(..) )
import qualified Nix.Eval                      as Eval
import           Nix.Expr
import           Nix.Frames
import           Nix.Fresh
import           Nix.String
import           Nix.Options
import           Nix.Scope
import           Nix.Thunk
import           Nix.Thunk.Basic
import           Nix.Utils
import           Nix.Var
import           Nix.Value.Monad

data TAtom
  = TInt
  | TFloat
  | TBool
  | TNull
  deriving (Int -> TAtom -> ShowS
[TAtom] -> ShowS
TAtom -> String
(Int -> TAtom -> ShowS)
-> (TAtom -> String) -> ([TAtom] -> ShowS) -> Show TAtom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TAtom] -> ShowS
$cshowList :: [TAtom] -> ShowS
show :: TAtom -> String
$cshow :: TAtom -> String
showsPrec :: Int -> TAtom -> ShowS
$cshowsPrec :: Int -> TAtom -> ShowS
Show, TAtom -> TAtom -> Bool
(TAtom -> TAtom -> Bool) -> (TAtom -> TAtom -> Bool) -> Eq TAtom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TAtom -> TAtom -> Bool
$c/= :: TAtom -> TAtom -> Bool
== :: TAtom -> TAtom -> Bool
$c== :: TAtom -> TAtom -> Bool
Eq, Eq TAtom
Eq TAtom =>
(TAtom -> TAtom -> Ordering)
-> (TAtom -> TAtom -> Bool)
-> (TAtom -> TAtom -> Bool)
-> (TAtom -> TAtom -> Bool)
-> (TAtom -> TAtom -> Bool)
-> (TAtom -> TAtom -> TAtom)
-> (TAtom -> TAtom -> TAtom)
-> Ord TAtom
TAtom -> TAtom -> Bool
TAtom -> TAtom -> Ordering
TAtom -> TAtom -> TAtom
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TAtom -> TAtom -> TAtom
$cmin :: TAtom -> TAtom -> TAtom
max :: TAtom -> TAtom -> TAtom
$cmax :: TAtom -> TAtom -> TAtom
>= :: TAtom -> TAtom -> Bool
$c>= :: TAtom -> TAtom -> Bool
> :: TAtom -> TAtom -> Bool
$c> :: TAtom -> TAtom -> Bool
<= :: TAtom -> TAtom -> Bool
$c<= :: TAtom -> TAtom -> Bool
< :: TAtom -> TAtom -> Bool
$c< :: TAtom -> TAtom -> Bool
compare :: TAtom -> TAtom -> Ordering
$ccompare :: TAtom -> TAtom -> Ordering
$cp1Ord :: Eq TAtom
Ord)

data NTypeF (m :: * -> *) r
    = TConstant [TAtom]
    | TStr
    | TList r
    | TSet (Maybe (HashMap Text r))
    | TClosure (Params ())
    | TPath
    | TBuiltin String (Symbolic m -> m r)
    deriving a -> NTypeF m b -> NTypeF m a
(a -> b) -> NTypeF m a -> NTypeF m b
(forall a b. (a -> b) -> NTypeF m a -> NTypeF m b)
-> (forall a b. a -> NTypeF m b -> NTypeF m a)
-> Functor (NTypeF m)
forall a b. a -> NTypeF m b -> NTypeF m a
forall a b. (a -> b) -> NTypeF m a -> NTypeF m b
forall (m :: * -> *) a b.
Functor m =>
a -> NTypeF m b -> NTypeF m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NTypeF m a -> NTypeF m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> NTypeF m b -> NTypeF m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> NTypeF m b -> NTypeF m a
fmap :: (a -> b) -> NTypeF m a -> NTypeF m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NTypeF m a -> NTypeF m b
Functor

compareTypes :: NTypeF m r -> NTypeF m r -> Ordering
compareTypes :: NTypeF m r -> NTypeF m r -> Ordering
compareTypes (TConstant _)  (TConstant _)  = Ordering
EQ
compareTypes (TConstant _)  _              = Ordering
LT
compareTypes _              (TConstant _)  = Ordering
GT
compareTypes TStr           TStr           = Ordering
EQ
compareTypes TStr           _              = Ordering
LT
compareTypes _              TStr           = Ordering
GT
compareTypes (TList _)      (TList _)      = Ordering
EQ
compareTypes (TList _)      _              = Ordering
LT
compareTypes _              (TList _)      = Ordering
GT
compareTypes (TSet _)       (TSet  _)      = Ordering
EQ
compareTypes (TSet _)       _              = Ordering
LT
compareTypes _              (TSet _)       = Ordering
GT
compareTypes TClosure{}     TClosure{}     = Ordering
EQ
compareTypes TClosure{}     _              = Ordering
LT
compareTypes _              TClosure{}     = Ordering
GT
compareTypes TPath          TPath          = Ordering
EQ
compareTypes TPath          _              = Ordering
LT
compareTypes _              TPath          = Ordering
GT
compareTypes (TBuiltin _ _) (TBuiltin _ _) = Ordering
EQ

data NSymbolicF r
    = NAny
    | NMany [r]
    deriving (Int -> NSymbolicF r -> ShowS
[NSymbolicF r] -> ShowS
NSymbolicF r -> String
(Int -> NSymbolicF r -> ShowS)
-> (NSymbolicF r -> String)
-> ([NSymbolicF r] -> ShowS)
-> Show (NSymbolicF r)
forall r. Show r => Int -> NSymbolicF r -> ShowS
forall r. Show r => [NSymbolicF r] -> ShowS
forall r. Show r => NSymbolicF r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NSymbolicF r] -> ShowS
$cshowList :: forall r. Show r => [NSymbolicF r] -> ShowS
show :: NSymbolicF r -> String
$cshow :: forall r. Show r => NSymbolicF r -> String
showsPrec :: Int -> NSymbolicF r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> NSymbolicF r -> ShowS
Show, NSymbolicF r -> NSymbolicF r -> Bool
(NSymbolicF r -> NSymbolicF r -> Bool)
-> (NSymbolicF r -> NSymbolicF r -> Bool) -> Eq (NSymbolicF r)
forall r. Eq r => NSymbolicF r -> NSymbolicF r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NSymbolicF r -> NSymbolicF r -> Bool
$c/= :: forall r. Eq r => NSymbolicF r -> NSymbolicF r -> Bool
== :: NSymbolicF r -> NSymbolicF r -> Bool
$c== :: forall r. Eq r => NSymbolicF r -> NSymbolicF r -> Bool
Eq, Eq (NSymbolicF r)
Eq (NSymbolicF r) =>
(NSymbolicF r -> NSymbolicF r -> Ordering)
-> (NSymbolicF r -> NSymbolicF r -> Bool)
-> (NSymbolicF r -> NSymbolicF r -> Bool)
-> (NSymbolicF r -> NSymbolicF r -> Bool)
-> (NSymbolicF r -> NSymbolicF r -> Bool)
-> (NSymbolicF r -> NSymbolicF r -> NSymbolicF r)
-> (NSymbolicF r -> NSymbolicF r -> NSymbolicF r)
-> Ord (NSymbolicF r)
NSymbolicF r -> NSymbolicF r -> Bool
NSymbolicF r -> NSymbolicF r -> Ordering
NSymbolicF r -> NSymbolicF r -> NSymbolicF r
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall r. Ord r => Eq (NSymbolicF r)
forall r. Ord r => NSymbolicF r -> NSymbolicF r -> Bool
forall r. Ord r => NSymbolicF r -> NSymbolicF r -> Ordering
forall r. Ord r => NSymbolicF r -> NSymbolicF r -> NSymbolicF r
min :: NSymbolicF r -> NSymbolicF r -> NSymbolicF r
$cmin :: forall r. Ord r => NSymbolicF r -> NSymbolicF r -> NSymbolicF r
max :: NSymbolicF r -> NSymbolicF r -> NSymbolicF r
$cmax :: forall r. Ord r => NSymbolicF r -> NSymbolicF r -> NSymbolicF r
>= :: NSymbolicF r -> NSymbolicF r -> Bool
$c>= :: forall r. Ord r => NSymbolicF r -> NSymbolicF r -> Bool
> :: NSymbolicF r -> NSymbolicF r -> Bool
$c> :: forall r. Ord r => NSymbolicF r -> NSymbolicF r -> Bool
<= :: NSymbolicF r -> NSymbolicF r -> Bool
$c<= :: forall r. Ord r => NSymbolicF r -> NSymbolicF r -> Bool
< :: NSymbolicF r -> NSymbolicF r -> Bool
$c< :: forall r. Ord r => NSymbolicF r -> NSymbolicF r -> Bool
compare :: NSymbolicF r -> NSymbolicF r -> Ordering
$ccompare :: forall r. Ord r => NSymbolicF r -> NSymbolicF r -> Ordering
$cp1Ord :: forall r. Ord r => Eq (NSymbolicF r)
Ord, a -> NSymbolicF b -> NSymbolicF a
(a -> b) -> NSymbolicF a -> NSymbolicF b
(forall a b. (a -> b) -> NSymbolicF a -> NSymbolicF b)
-> (forall a b. a -> NSymbolicF b -> NSymbolicF a)
-> Functor NSymbolicF
forall a b. a -> NSymbolicF b -> NSymbolicF a
forall a b. (a -> b) -> NSymbolicF a -> NSymbolicF b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> NSymbolicF b -> NSymbolicF a
$c<$ :: forall a b. a -> NSymbolicF b -> NSymbolicF a
fmap :: (a -> b) -> NSymbolicF a -> NSymbolicF b
$cfmap :: forall a b. (a -> b) -> NSymbolicF a -> NSymbolicF b
Functor, NSymbolicF a -> Bool
(a -> m) -> NSymbolicF a -> m
(a -> b -> b) -> b -> NSymbolicF a -> b
(forall m. Monoid m => NSymbolicF m -> m)
-> (forall m a. Monoid m => (a -> m) -> NSymbolicF a -> m)
-> (forall m a. Monoid m => (a -> m) -> NSymbolicF a -> m)
-> (forall a b. (a -> b -> b) -> b -> NSymbolicF a -> b)
-> (forall a b. (a -> b -> b) -> b -> NSymbolicF a -> b)
-> (forall b a. (b -> a -> b) -> b -> NSymbolicF a -> b)
-> (forall b a. (b -> a -> b) -> b -> NSymbolicF a -> b)
-> (forall a. (a -> a -> a) -> NSymbolicF a -> a)
-> (forall a. (a -> a -> a) -> NSymbolicF a -> a)
-> (forall a. NSymbolicF a -> [a])
-> (forall a. NSymbolicF a -> Bool)
-> (forall a. NSymbolicF a -> Int)
-> (forall a. Eq a => a -> NSymbolicF a -> Bool)
-> (forall a. Ord a => NSymbolicF a -> a)
-> (forall a. Ord a => NSymbolicF a -> a)
-> (forall a. Num a => NSymbolicF a -> a)
-> (forall a. Num a => NSymbolicF a -> a)
-> Foldable NSymbolicF
forall a. Eq a => a -> NSymbolicF a -> Bool
forall a. Num a => NSymbolicF a -> a
forall a. Ord a => NSymbolicF a -> a
forall m. Monoid m => NSymbolicF m -> m
forall a. NSymbolicF a -> Bool
forall a. NSymbolicF a -> Int
forall a. NSymbolicF a -> [a]
forall a. (a -> a -> a) -> NSymbolicF a -> a
forall m a. Monoid m => (a -> m) -> NSymbolicF a -> m
forall b a. (b -> a -> b) -> b -> NSymbolicF a -> b
forall a b. (a -> b -> b) -> b -> NSymbolicF a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: NSymbolicF a -> a
$cproduct :: forall a. Num a => NSymbolicF a -> a
sum :: NSymbolicF a -> a
$csum :: forall a. Num a => NSymbolicF a -> a
minimum :: NSymbolicF a -> a
$cminimum :: forall a. Ord a => NSymbolicF a -> a
maximum :: NSymbolicF a -> a
$cmaximum :: forall a. Ord a => NSymbolicF a -> a
elem :: a -> NSymbolicF a -> Bool
$celem :: forall a. Eq a => a -> NSymbolicF a -> Bool
length :: NSymbolicF a -> Int
$clength :: forall a. NSymbolicF a -> Int
null :: NSymbolicF a -> Bool
$cnull :: forall a. NSymbolicF a -> Bool
toList :: NSymbolicF a -> [a]
$ctoList :: forall a. NSymbolicF a -> [a]
foldl1 :: (a -> a -> a) -> NSymbolicF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> NSymbolicF a -> a
foldr1 :: (a -> a -> a) -> NSymbolicF a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> NSymbolicF a -> a
foldl' :: (b -> a -> b) -> b -> NSymbolicF a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> NSymbolicF a -> b
foldl :: (b -> a -> b) -> b -> NSymbolicF a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> NSymbolicF a -> b
foldr' :: (a -> b -> b) -> b -> NSymbolicF a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> NSymbolicF a -> b
foldr :: (a -> b -> b) -> b -> NSymbolicF a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> NSymbolicF a -> b
foldMap' :: (a -> m) -> NSymbolicF a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> NSymbolicF a -> m
foldMap :: (a -> m) -> NSymbolicF a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> NSymbolicF a -> m
fold :: NSymbolicF m -> m
$cfold :: forall m. Monoid m => NSymbolicF m -> m
Foldable, Functor NSymbolicF
Foldable NSymbolicF
(Functor NSymbolicF, Foldable NSymbolicF) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> NSymbolicF a -> f (NSymbolicF b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    NSymbolicF (f a) -> f (NSymbolicF a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NSymbolicF a -> m (NSymbolicF b))
-> (forall (m :: * -> *) a.
    Monad m =>
    NSymbolicF (m a) -> m (NSymbolicF a))
-> Traversable NSymbolicF
(a -> f b) -> NSymbolicF a -> f (NSymbolicF b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
NSymbolicF (m a) -> m (NSymbolicF a)
forall (f :: * -> *) a.
Applicative f =>
NSymbolicF (f a) -> f (NSymbolicF a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NSymbolicF a -> m (NSymbolicF b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NSymbolicF a -> f (NSymbolicF b)
sequence :: NSymbolicF (m a) -> m (NSymbolicF a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
NSymbolicF (m a) -> m (NSymbolicF a)
mapM :: (a -> m b) -> NSymbolicF a -> m (NSymbolicF b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NSymbolicF a -> m (NSymbolicF b)
sequenceA :: NSymbolicF (f a) -> f (NSymbolicF a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
NSymbolicF (f a) -> f (NSymbolicF a)
traverse :: (a -> f b) -> NSymbolicF a -> f (NSymbolicF b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NSymbolicF a -> f (NSymbolicF b)
$cp2Traversable :: Foldable NSymbolicF
$cp1Traversable :: Functor NSymbolicF
Traversable)

type SThunk (m :: * -> *) = NThunkF m (Symbolic m)

type SValue (m :: * -> *) = Var m (NSymbolicF (NTypeF m (Symbolic m)))

data Symbolic m = SV { Symbolic m -> SValue m
getSV :: SValue m } | ST { Symbolic m -> SThunk m
getST :: SThunk m }

instance Show (Symbolic m) where
  show :: Symbolic m -> String
show _ = "<symbolic>"

everyPossible :: MonadVar m => m (Symbolic m)
everyPossible :: m (Symbolic m)
everyPossible = NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
packSymbolic NSymbolicF (NTypeF m (Symbolic m))
forall r. NSymbolicF r
NAny

mkSymbolic :: MonadVar m => [NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic :: [NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic xs :: [NTypeF m (Symbolic m)]
xs = NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
packSymbolic ([NTypeF m (Symbolic m)] -> NSymbolicF (NTypeF m (Symbolic m))
forall r. [r] -> NSymbolicF r
NMany [NTypeF m (Symbolic m)]
xs)

packSymbolic
  :: MonadVar m => NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
packSymbolic :: NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
packSymbolic = (Ref m (NSymbolicF (NTypeF m (Symbolic m))) -> Symbolic m)
-> m (Ref m (NSymbolicF (NTypeF m (Symbolic m)))) -> m (Symbolic m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ref m (NSymbolicF (NTypeF m (Symbolic m))) -> Symbolic m
forall (m :: * -> *). SValue m -> Symbolic m
SV (m (Ref m (NSymbolicF (NTypeF m (Symbolic m)))) -> m (Symbolic m))
-> (NSymbolicF (NTypeF m (Symbolic m))
    -> m (Ref m (NSymbolicF (NTypeF m (Symbolic m)))))
-> NSymbolicF (NTypeF m (Symbolic m))
-> m (Symbolic m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NSymbolicF (NTypeF m (Symbolic m))
-> m (Ref m (NSymbolicF (NTypeF m (Symbolic m))))
forall (m :: * -> *) a. MonadRef m => a -> m (Ref m a)
newVar

unpackSymbolic
  :: (MonadVar m, MonadThunkId m, MonadCatch m)
  => Symbolic m
  -> m (NSymbolicF (NTypeF m (Symbolic m)))
unpackSymbolic :: Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
unpackSymbolic = (Symbolic m
 -> (Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
 -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> (Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> Symbolic m
-> m (NSymbolicF (NTypeF m (Symbolic m)))
forall a b c. (a -> b -> c) -> b -> a -> c
flip Symbolic m
-> (Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> m (NSymbolicF (NTypeF m (Symbolic m)))
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand ((Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
 -> Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> (Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> Symbolic m
-> m (NSymbolicF (NTypeF m (Symbolic m)))
forall a b. (a -> b) -> a -> b
$ Ref m (NSymbolicF (NTypeF m (Symbolic m)))
-> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *) a. MonadRef m => Ref m a -> m a
readVar (Ref m (NSymbolicF (NTypeF m (Symbolic m)))
 -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> (Symbolic m -> Ref m (NSymbolicF (NTypeF m (Symbolic m))))
-> Symbolic m
-> m (NSymbolicF (NTypeF m (Symbolic m)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbolic m -> Ref m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *). Symbolic m -> SValue m
getSV

type MonadLint e m
  = ( Scoped (Symbolic m) m
  , Framed e m
  , MonadVar m
  , MonadCatch m
  , MonadThunkId m
  )

symerr :: forall e m a . MonadLint e m => String -> m a
symerr :: String -> m a
symerr = forall v (m :: * -> *) s a.
(MonadEval v m, Exception s) =>
s -> m a
forall (m :: * -> *) s a.
(MonadEval (Symbolic m) m, Exception s) =>
s -> m a
evalError @(Symbolic m) (ErrorCall -> m a) -> (String -> ErrorCall) -> String -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ErrorCall
ErrorCall

renderSymbolic :: MonadLint e m => Symbolic m -> m String
renderSymbolic :: Symbolic m -> m String
renderSymbolic = Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *).
(MonadVar m, MonadThunkId m, MonadCatch m) =>
Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
unpackSymbolic (Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> (NSymbolicF (NTypeF m (Symbolic m)) -> m String)
-> Symbolic m
-> m String
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
  NAny     -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "<any>"
  NMany xs :: [NTypeF m (Symbolic m)]
xs -> ([String] -> String) -> m [String] -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", ") (m [String] -> m String) -> m [String] -> m String
forall a b. (a -> b) -> a -> b
$ [NTypeF m (Symbolic m)]
-> (NTypeF m (Symbolic m) -> m String) -> m [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NTypeF m (Symbolic m)]
xs ((NTypeF m (Symbolic m) -> m String) -> m [String])
-> (NTypeF m (Symbolic m) -> m String) -> m [String]
forall a b. (a -> b) -> a -> b
$ \case
    TConstant ys :: [TAtom]
ys -> ([String] -> String) -> m [String] -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", ") (m [String] -> m String) -> m [String] -> m String
forall a b. (a -> b) -> a -> b
$ [TAtom] -> (TAtom -> m String) -> m [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TAtom]
ys ((TAtom -> m String) -> m [String])
-> (TAtom -> m String) -> m [String]
forall a b. (a -> b) -> a -> b
$ \case
      TInt   -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "int"
      TFloat -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "float"
      TBool  -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "bool"
      TNull  -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "null"
    TStr    -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "string"
    TList r :: Symbolic m
r -> do
      String
x <- Symbolic m -> (Symbolic m -> m String) -> m String
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Symbolic m
r Symbolic m -> m String
forall e (m :: * -> *). MonadLint e m => Symbolic m -> m String
renderSymbolic
      String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ "[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ "]"
    TSet Nothing  -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "<any set>"
    TSet (Just s :: HashMap Text (Symbolic m)
s) -> do
      HashMap Text String
x <- (Symbolic m -> m String)
-> HashMap Text (Symbolic m) -> m (HashMap Text String)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Symbolic m -> (Symbolic m -> m String) -> m String
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
`demand` Symbolic m -> m String
forall e (m :: * -> *). MonadLint e m => Symbolic m -> m String
renderSymbolic) HashMap Text (Symbolic m)
s
      String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ "{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ HashMap Text String -> String
forall a. Show a => a -> String
show HashMap Text String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ "}"
    f :: NTypeF m (Symbolic m)
f@(TClosure p :: Params ()
p) -> do
      (args :: HashMap Text (Symbolic m)
args, sym :: Symbolic m
sym) <- do
        Symbolic m
f' <- [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [NTypeF m (Symbolic m)
f]
        NExprF ()
-> Symbolic m
-> m (Symbolic m)
-> m (HashMap Text (Symbolic m), Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF ()
-> Symbolic m
-> m (Symbolic m)
-> m (HashMap Text (Symbolic m), Symbolic m)
lintApp (Params () -> () -> NExprF ()
forall r. Params r -> r -> NExprF r
NAbs (Params () -> Params ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Params ()
p) ()) Symbolic m
f' m (Symbolic m)
forall (m :: * -> *). MonadVar m => m (Symbolic m)
everyPossible
      HashMap Text String
args' <- (Symbolic m -> m String)
-> HashMap Text (Symbolic m) -> m (HashMap Text String)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Symbolic m -> m String
forall e (m :: * -> *). MonadLint e m => Symbolic m -> m String
renderSymbolic HashMap Text (Symbolic m)
args
      String
sym'  <- Symbolic m -> m String
forall e (m :: * -> *). MonadLint e m => Symbolic m -> m String
renderSymbolic Symbolic m
sym
      String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ HashMap Text String -> String
forall a. Show a => a -> String
show HashMap Text String
args' String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sym' String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
    TPath          -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "path"
    TBuiltin _n :: String
_n _f :: Symbolic m -> m (Symbolic m)
_f -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "<builtin function>"

-- This function is order and uniqueness preserving (of types).
merge
  :: forall e m
   . MonadLint e m
  => NExprF ()
  -> [NTypeF m (Symbolic m)]
  -> [NTypeF m (Symbolic m)]
  -> m [NTypeF m (Symbolic m)]
merge :: NExprF ()
-> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)]
-> m [NTypeF m (Symbolic m)]
merge context :: NExprF ()
context = [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go
 where
  go
    :: [NTypeF m (Symbolic m)]
    -> [NTypeF m (Symbolic m)]
    -> m [NTypeF m (Symbolic m)]
  go :: [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go []       _        = [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  go _        []       = [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  go (x :: NTypeF m (Symbolic m)
x : xs :: [NTypeF m (Symbolic m)]
xs) (y :: NTypeF m (Symbolic m)
y : ys :: [NTypeF m (Symbolic m)]
ys) = case (NTypeF m (Symbolic m)
x, NTypeF m (Symbolic m)
y) of
    (TStr , TStr ) -> (NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TStr NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
:) ([NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
    (TPath, TPath) -> (NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TPath NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
:) ([NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
    (TConstant ls :: [TAtom]
ls, TConstant rs :: [TAtom]
rs) ->
      ([TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant ([TAtom]
ls [TAtom] -> [TAtom] -> [TAtom]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [TAtom]
rs) NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
:) ([NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
    (TList l :: Symbolic m
l, TList r :: Symbolic m
r) -> Symbolic m
-> (Symbolic m -> m [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)]
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Symbolic m
l ((Symbolic m -> m [NTypeF m (Symbolic m)])
 -> m [NTypeF m (Symbolic m)])
-> (Symbolic m -> m [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)]
forall a b. (a -> b) -> a -> b
$ \l' :: Symbolic m
l' -> Symbolic m
-> (Symbolic m -> m [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)]
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Symbolic m
r ((Symbolic m -> m [NTypeF m (Symbolic m)])
 -> m [NTypeF m (Symbolic m)])
-> (Symbolic m -> m [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)]
forall a b. (a -> b) -> a -> b
$ \r' :: Symbolic m
r' -> do
      Symbolic m
m <- m (Symbolic m) -> m (Symbolic m)
forall v (m :: * -> *). MonadValue v m => m v -> m v
defer (m (Symbolic m) -> m (Symbolic m))
-> m (Symbolic m) -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify NExprF ()
context Symbolic m
l' Symbolic m
r'
      (Symbolic m -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. r -> NTypeF m r
TList Symbolic m
m NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
:) ([NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
    (TSet x :: Maybe (HashMap Text (Symbolic m))
x       , TSet Nothing ) -> (Maybe (HashMap Text (Symbolic m)) -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. Maybe (HashMap Text r) -> NTypeF m r
TSet Maybe (HashMap Text (Symbolic m))
x NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
:) ([NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
    (TSet Nothing , TSet x :: Maybe (HashMap Text (Symbolic m))
x       ) -> (Maybe (HashMap Text (Symbolic m)) -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. Maybe (HashMap Text r) -> NTypeF m r
TSet Maybe (HashMap Text (Symbolic m))
x NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
:) ([NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
    (TSet (Just l :: HashMap Text (Symbolic m)
l), TSet (Just r :: HashMap Text (Symbolic m)
r)) -> do
      HashMap Text (Symbolic m)
m <- HashMap Text (m (Symbolic m)) -> m (HashMap Text (Symbolic m))
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (HashMap Text (m (Symbolic m)) -> m (HashMap Text (Symbolic m)))
-> HashMap Text (m (Symbolic m)) -> m (HashMap Text (Symbolic m))
forall a b. (a -> b) -> a -> b
$ (m (Symbolic m) -> m (Symbolic m) -> m (Symbolic m))
-> HashMap Text (m (Symbolic m))
-> HashMap Text (m (Symbolic m))
-> HashMap Text (m (Symbolic m))
forall k v1 v2 v3.
(Eq k, Hashable k) =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
M.intersectionWith
        (\i :: m (Symbolic m)
i j :: m (Symbolic m)
j -> m (Symbolic m)
i m (Symbolic m) -> (Symbolic m -> m (Symbolic m)) -> m (Symbolic m)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \i' :: Symbolic m
i' ->
          m (Symbolic m)
j
            m (Symbolic m) -> (Symbolic m -> m (Symbolic m)) -> m (Symbolic m)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \j' :: Symbolic m
j' -> Symbolic m -> (Symbolic m -> m (Symbolic m)) -> m (Symbolic m)
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Symbolic m
i'
                  ((Symbolic m -> m (Symbolic m)) -> m (Symbolic m))
-> (Symbolic m -> m (Symbolic m)) -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ \i'' :: Symbolic m
i'' -> Symbolic m -> (Symbolic m -> m (Symbolic m)) -> m (Symbolic m)
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Symbolic m
j' ((Symbolic m -> m (Symbolic m)) -> m (Symbolic m))
-> (Symbolic m -> m (Symbolic m)) -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ \j'' :: Symbolic m
j'' -> m (Symbolic m) -> m (Symbolic m)
forall v (m :: * -> *). MonadValue v m => m v -> m v
defer (m (Symbolic m) -> m (Symbolic m))
-> m (Symbolic m) -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify NExprF ()
context Symbolic m
i'' Symbolic m
j''
        )
        (Symbolic m -> m (Symbolic m)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbolic m -> m (Symbolic m))
-> HashMap Text (Symbolic m) -> HashMap Text (m (Symbolic m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Text (Symbolic m)
l)
        (Symbolic m -> m (Symbolic m)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbolic m -> m (Symbolic m))
-> HashMap Text (Symbolic m) -> HashMap Text (m (Symbolic m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Text (Symbolic m)
r)
      if HashMap Text (Symbolic m) -> Bool
forall k v. HashMap k v -> Bool
M.null HashMap Text (Symbolic m)
m then [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys else (Maybe (HashMap Text (Symbolic m)) -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. Maybe (HashMap Text r) -> NTypeF m r
TSet (HashMap Text (Symbolic m) -> Maybe (HashMap Text (Symbolic m))
forall a. a -> Maybe a
Just HashMap Text (Symbolic m)
m) NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
:) ([NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)])
-> m [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
    (TClosure{}, TClosure{}) ->
      ErrorCall -> m [NTypeF m (Symbolic m)]
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m [NTypeF m (Symbolic m)])
-> ErrorCall -> m [NTypeF m (Symbolic m)]
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "Cannot unify functions"
    (TBuiltin _ _, TBuiltin _ _) ->
      ErrorCall -> m [NTypeF m (Symbolic m)]
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m [NTypeF m (Symbolic m)])
-> ErrorCall -> m [NTypeF m (Symbolic m)]
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "Cannot unify builtin functions"
    _ | NTypeF m (Symbolic m) -> NTypeF m (Symbolic m) -> Ordering
forall (m :: * -> *) r. NTypeF m r -> NTypeF m r -> Ordering
compareTypes NTypeF m (Symbolic m)
x NTypeF m (Symbolic m)
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT -> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go [NTypeF m (Symbolic m)]
xs (NTypeF m (Symbolic m)
y NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
: [NTypeF m (Symbolic m)]
ys)
      | NTypeF m (Symbolic m) -> NTypeF m (Symbolic m) -> Ordering
forall (m :: * -> *) r. NTypeF m r -> NTypeF m r -> Ordering
compareTypes NTypeF m (Symbolic m)
x NTypeF m (Symbolic m)
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT -> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)] -> m [NTypeF m (Symbolic m)]
go (NTypeF m (Symbolic m)
x NTypeF m (Symbolic m)
-> [NTypeF m (Symbolic m)] -> [NTypeF m (Symbolic m)]
forall a. a -> [a] -> [a]
: [NTypeF m (Symbolic m)]
xs) [NTypeF m (Symbolic m)]
ys
      | Bool
otherwise              -> String -> m [NTypeF m (Symbolic m)]
forall a. HasCallStack => String -> a
error "impossible"

{-
    mergeFunctions pl nl fl pr fr xs ys = do
        m <- sequenceA $ M.intersectionWith
            (\i j -> i >>= \i' -> j >>= \j' -> case (i', j') of
                    (Nothing, Nothing) -> return $ Just Nothing
                    (_, Nothing) -> return Nothing
                    (Nothing, _) -> return Nothing
                    (Just i'', Just j'') ->
                        Just . Just <$> unify context i'' j'')
            (return <$> pl) (return <$> pr)
        let Just m' = sequenceA $ M.filter isJust m
        if M.null m'
            then go xs ys
            else do
                g <- unify context fl fr
                (TClosure (ParamSet m' False nl) g :)
                    <$> go xs ys
-}

-- | unify raises an error if the result is would be 'NMany []'.
unify
  :: forall e m
   . MonadLint e m
  => NExprF ()
  -> Symbolic m
  -> Symbolic m
  -> m (Symbolic m)
unify :: NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify context :: NExprF ()
context (SV x :: SValue m
x) (SV y :: SValue m
y) = do
  NSymbolicF (NTypeF m (Symbolic m))
x' <- SValue m -> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *) a. MonadRef m => Ref m a -> m a
readVar SValue m
x
  NSymbolicF (NTypeF m (Symbolic m))
y' <- SValue m -> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *) a. MonadRef m => Ref m a -> m a
readVar SValue m
y
  case (NSymbolicF (NTypeF m (Symbolic m))
x', NSymbolicF (NTypeF m (Symbolic m))
y') of
    (NAny, _) -> do
      SValue m -> NSymbolicF (NTypeF m (Symbolic m)) -> m ()
forall (m :: * -> *) a. MonadRef m => Ref m a -> a -> m ()
writeVar SValue m
x NSymbolicF (NTypeF m (Symbolic m))
y'
      Symbolic m -> m (Symbolic m)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbolic m -> m (Symbolic m)) -> Symbolic m -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ SValue m -> Symbolic m
forall (m :: * -> *). SValue m -> Symbolic m
SV SValue m
y
    (_, NAny) -> do
      SValue m -> NSymbolicF (NTypeF m (Symbolic m)) -> m ()
forall (m :: * -> *) a. MonadRef m => Ref m a -> a -> m ()
writeVar SValue m
y NSymbolicF (NTypeF m (Symbolic m))
x'
      Symbolic m -> m (Symbolic m)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbolic m -> m (Symbolic m)) -> Symbolic m -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ SValue m -> Symbolic m
forall (m :: * -> *). SValue m -> Symbolic m
SV SValue m
x
    (NMany xs :: [NTypeF m (Symbolic m)]
xs, NMany ys :: [NTypeF m (Symbolic m)]
ys) -> do
      [NTypeF m (Symbolic m)]
m <- NExprF ()
-> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)]
-> m [NTypeF m (Symbolic m)]
forall e (m :: * -> *).
MonadLint e m =>
NExprF ()
-> [NTypeF m (Symbolic m)]
-> [NTypeF m (Symbolic m)]
-> m [NTypeF m (Symbolic m)]
merge NExprF ()
context [NTypeF m (Symbolic m)]
xs [NTypeF m (Symbolic m)]
ys
      if [NTypeF m (Symbolic m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NTypeF m (Symbolic m)]
m
        then do
              -- x' <- renderSymbolic (Symbolic x)
              -- y' <- renderSymbolic (Symbolic y)
          ErrorCall -> m (Symbolic m)
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m (Symbolic m)) -> ErrorCall -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "Cannot unify "
                  -- ++ show x' ++ " with " ++ show y'
                  --  ++ " in context: " ++ show context
        else do
          SValue m -> NSymbolicF (NTypeF m (Symbolic m)) -> m ()
forall (m :: * -> *) a. MonadRef m => Ref m a -> a -> m ()
writeVar SValue m
x ([NTypeF m (Symbolic m)] -> NSymbolicF (NTypeF m (Symbolic m))
forall r. [r] -> NSymbolicF r
NMany [NTypeF m (Symbolic m)]
m)
          SValue m -> NSymbolicF (NTypeF m (Symbolic m)) -> m ()
forall (m :: * -> *) a. MonadRef m => Ref m a -> a -> m ()
writeVar SValue m
y ([NTypeF m (Symbolic m)] -> NSymbolicF (NTypeF m (Symbolic m))
forall r. [r] -> NSymbolicF r
NMany [NTypeF m (Symbolic m)]
m)
          NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
NSymbolicF (NTypeF m (Symbolic m)) -> m (Symbolic m)
packSymbolic ([NTypeF m (Symbolic m)] -> NSymbolicF (NTypeF m (Symbolic m))
forall r. [r] -> NSymbolicF r
NMany [NTypeF m (Symbolic m)]
m)
unify _ _ _ = String -> m (Symbolic m)
forall a. HasCallStack => String -> a
error "The unexpected hath transpired!"

-- These aren't worth defining yet, because once we move to Hindley-Milner,
-- we're not going to be managing Symbolic values this way anymore.

instance ToValue Bool m (Symbolic m) where

instance ToValue [Symbolic m] m (Symbolic m) where

instance FromValue NixString m (Symbolic m) where

instance FromValue (AttrSet (Symbolic m), AttrSet SourcePos) m (Symbolic m) where

instance ToValue (AttrSet (Symbolic m), AttrSet SourcePos) m (Symbolic m) where

instance (MonadThunkId m, MonadAtomicRef m, MonadCatch m)
  => MonadValue (Symbolic m) m where
  defer :: m (Symbolic m) -> m (Symbolic m)
defer = (SThunk m -> Symbolic m) -> m (SThunk m) -> m (Symbolic m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SThunk m -> Symbolic m
forall (m :: * -> *). SThunk m -> Symbolic m
ST (m (SThunk m) -> m (Symbolic m))
-> (m (Symbolic m) -> m (SThunk m))
-> m (Symbolic m)
-> m (Symbolic m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Symbolic m) -> m (SThunk m)
forall t (m :: * -> *) a. MonadThunk t m a => m a -> m t
thunk
  demand :: Symbolic m -> (Symbolic m -> m r) -> m r
demand (ST v :: SThunk m
v) f :: Symbolic m -> m r
f = SThunk m -> (Symbolic m -> m r) -> m r
forall t (m :: * -> *) a r.
MonadThunk t m a =>
t -> (a -> m r) -> m r
force SThunk m
v ((Symbolic m -> (Symbolic m -> m r) -> m r)
-> (Symbolic m -> m r) -> Symbolic m -> m r
forall a b c. (a -> b -> c) -> b -> a -> c
flip Symbolic m -> (Symbolic m -> m r) -> m r
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Symbolic m -> m r
f)
  demand (SV v :: SValue m
v) f :: Symbolic m -> m r
f = Symbolic m -> m r
f (SValue m -> Symbolic m
forall (m :: * -> *). SValue m -> Symbolic m
SV SValue m
v)

instance MonadLint e m => MonadEval (Symbolic m) m where
  freeVariable :: Text -> m (Symbolic m)
freeVariable var :: Text
var = String -> m (Symbolic m)
forall e (m :: * -> *) a. MonadLint e m => String -> m a
symerr (String -> m (Symbolic m)) -> String -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ "Undefined variable '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
var String -> ShowS
forall a. [a] -> [a] -> [a]
++ "'"

  attrMissing :: NonEmpty Text -> Maybe (Symbolic m) -> m (Symbolic m)
attrMissing ks :: NonEmpty Text
ks Nothing =
    forall v (m :: * -> *) s a.
(MonadEval v m, Exception s) =>
s -> m a
forall (m :: * -> *) s a.
(MonadEval (Symbolic m) m, Exception s) =>
s -> m a
evalError @(Symbolic m)
      (ErrorCall -> m (Symbolic m)) -> ErrorCall -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$  String -> ErrorCall
ErrorCall
      (String -> ErrorCall) -> String -> ErrorCall
forall a b. (a -> b) -> a -> b
$  "Inheriting unknown attribute: "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "." ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
Text.unpack (NonEmpty Text -> [Text]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Text
ks))

  attrMissing ks :: NonEmpty Text
ks (Just s :: Symbolic m
s) =
    forall v (m :: * -> *) s a.
(MonadEval v m, Exception s) =>
s -> m a
forall (m :: * -> *) s a.
(MonadEval (Symbolic m) m, Exception s) =>
s -> m a
evalError @(Symbolic m)
      (ErrorCall -> m (Symbolic m)) -> ErrorCall -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$  String -> ErrorCall
ErrorCall
      (String -> ErrorCall) -> String -> ErrorCall
forall a b. (a -> b) -> a -> b
$  "Could not look up attribute "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "." ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
Text.unpack (NonEmpty Text -> [Text]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Text
ks))
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ " in "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbolic m -> String
forall a. Show a => a -> String
show Symbolic m
s

  evalCurPos :: m (Symbolic m)
evalCurPos = do
    Symbolic m
f <- [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TPath]
    Symbolic m
l <- [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt]]
    Symbolic m
c <- [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt]]
    [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [Maybe (HashMap Text (Symbolic m)) -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. Maybe (HashMap Text r) -> NTypeF m r
TSet (HashMap Text (Symbolic m) -> Maybe (HashMap Text (Symbolic m))
forall a. a -> Maybe a
Just ([(Text, Symbolic m)] -> HashMap Text (Symbolic m)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (Symbolic m -> Symbolic m -> Symbolic m -> [(Text, Symbolic m)]
forall b. b -> b -> b -> [(Text, b)]
go Symbolic m
f Symbolic m
l Symbolic m
c)))]
   where
    go :: b -> b -> b -> [(Text, b)]
go f :: b
f l :: b
l c :: b
c =
      [(String -> Text
Text.pack "file", b
f), (String -> Text
Text.pack "line", b
l), (String -> Text
Text.pack "col", b
c)]

  evalConstant :: NAtom -> m (Symbolic m)
evalConstant c :: NAtom
c = [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [NAtom -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. NAtom -> NTypeF m r
go NAtom
c]
   where
    go :: NAtom -> NTypeF m r
go = \case
      NURI   _ -> NTypeF m r
forall (m :: * -> *) r. NTypeF m r
TStr
      NInt   _ -> [TAtom] -> NTypeF m r
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt]
      NFloat _ -> [TAtom] -> NTypeF m r
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TFloat]
      NBool  _ -> [TAtom] -> NTypeF m r
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TBool]
      NNull    -> [TAtom] -> NTypeF m r
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TNull]

  evalString :: NString (m (Symbolic m)) -> m (Symbolic m)
evalString      = m (Symbolic m) -> NString (m (Symbolic m)) -> m (Symbolic m)
forall a b. a -> b -> a
const (m (Symbolic m) -> NString (m (Symbolic m)) -> m (Symbolic m))
-> m (Symbolic m) -> NString (m (Symbolic m)) -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TStr]
  evalLiteralPath :: String -> m (Symbolic m)
evalLiteralPath = m (Symbolic m) -> String -> m (Symbolic m)
forall a b. a -> b -> a
const (m (Symbolic m) -> String -> m (Symbolic m))
-> m (Symbolic m) -> String -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TPath]
  evalEnvPath :: String -> m (Symbolic m)
evalEnvPath     = m (Symbolic m) -> String -> m (Symbolic m)
forall a b. a -> b -> a
const (m (Symbolic m) -> String -> m (Symbolic m))
-> m (Symbolic m) -> String -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TPath]

  evalUnary :: NUnaryOp -> Symbolic m -> m (Symbolic m)
evalUnary op :: NUnaryOp
op arg :: Symbolic m
arg =
    NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify (NExprF (Symbolic m) -> NExprF ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (NUnaryOp -> Symbolic m -> NExprF (Symbolic m)
forall r. NUnaryOp -> r -> NExprF r
NUnary NUnaryOp
op Symbolic m
arg)) Symbolic m
arg (Symbolic m -> m (Symbolic m)) -> m (Symbolic m) -> m (Symbolic m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt, TAtom
TBool]]

  evalBinary :: NBinaryOp -> Symbolic m -> m (Symbolic m) -> m (Symbolic m)
evalBinary = NBinaryOp -> Symbolic m -> m (Symbolic m) -> m (Symbolic m)
forall e (m :: * -> *).
(MonadLint e m, MonadEval (Symbolic m) m) =>
NBinaryOp -> Symbolic m -> m (Symbolic m) -> m (Symbolic m)
lintBinaryOp

  -- The scope is deliberately wrapped in a thunk here, since it is evaluated
  -- each time a name is looked up within the weak scope, and we want to be
  -- sure the action it evaluates is to force a thunk, so its value is only
  -- computed once.
  evalWith :: m (Symbolic m) -> m (Symbolic m) -> m (Symbolic m)
evalWith scope :: m (Symbolic m)
scope body :: m (Symbolic m)
body = do
    Symbolic m
s <- m (Symbolic m) -> m (Symbolic m)
forall v (m :: * -> *). MonadValue v m => m v -> m v
defer m (Symbolic m)
scope
    m (HashMap Text (Symbolic m)) -> m (Symbolic m) -> m (Symbolic m)
forall (m :: * -> *) a r.
(Functor m, Scoped a m) =>
m (AttrSet a) -> m r -> m r
pushWeakScope (m (HashMap Text (Symbolic m)) -> m (Symbolic m) -> m (Symbolic m))
-> m (Symbolic m)
-> m (HashMap Text (Symbolic m))
-> m (Symbolic m)
forall (f :: * -> *) a b. Functor f => f (a -> b) -> a -> f b
?? m (Symbolic m)
body (m (HashMap Text (Symbolic m)) -> m (Symbolic m))
-> m (HashMap Text (Symbolic m)) -> m (Symbolic m)
forall a b. (a -> b) -> a -> b
$ Symbolic m
-> (Symbolic m -> m (HashMap Text (Symbolic m)))
-> m (HashMap Text (Symbolic m))
forall v (m :: * -> *) r. MonadValue v m => v -> (v -> m r) -> m r
demand Symbolic m
s ((Symbolic m -> m (HashMap Text (Symbolic m)))
 -> m (HashMap Text (Symbolic m)))
-> (Symbolic m -> m (HashMap Text (Symbolic m)))
-> m (HashMap Text (Symbolic m))
forall a b. (a -> b) -> a -> b
$ Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *).
(MonadVar m, MonadThunkId m, MonadCatch m) =>
Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
unpackSymbolic (Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> (NSymbolicF (NTypeF m (Symbolic m))
    -> m (HashMap Text (Symbolic m)))
-> Symbolic m
-> m (HashMap Text (Symbolic m))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
      NMany [TSet (Just s' :: HashMap Text (Symbolic m)
s')] -> HashMap Text (Symbolic m) -> m (HashMap Text (Symbolic m))
forall (m :: * -> *) a. Monad m => a -> m a
return HashMap Text (Symbolic m)
s'
      NMany [TSet Nothing] -> String -> m (HashMap Text (Symbolic m))
forall a. HasCallStack => String -> a
error "NYI: with unknown"
      _ -> ErrorCall -> m (HashMap Text (Symbolic m))
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m (HashMap Text (Symbolic m)))
-> ErrorCall -> m (HashMap Text (Symbolic m))
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "scope must be a set in with statement"

  evalIf :: Symbolic m -> m (Symbolic m) -> m (Symbolic m) -> m (Symbolic m)
evalIf cond :: Symbolic m
cond t :: m (Symbolic m)
t f :: m (Symbolic m)
f = do
    Symbolic m
t' <- m (Symbolic m)
t
    Symbolic m
f' <- m (Symbolic m)
f
    let e :: NExprF (Symbolic m)
e = Symbolic m -> Symbolic m -> Symbolic m -> NExprF (Symbolic m)
forall r. r -> r -> r -> NExprF r
NIf Symbolic m
cond Symbolic m
t' Symbolic m
f'
    Symbolic m
_ <- NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify (NExprF (Symbolic m) -> NExprF ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void NExprF (Symbolic m)
e) Symbolic m
cond (Symbolic m -> m (Symbolic m)) -> m (Symbolic m) -> m (Symbolic m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TBool]]
    NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify (NExprF (Symbolic m) -> NExprF ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void NExprF (Symbolic m)
e) Symbolic m
t' Symbolic m
f'

  evalAssert :: Symbolic m -> m (Symbolic m) -> m (Symbolic m)
evalAssert cond :: Symbolic m
cond body :: m (Symbolic m)
body = do
    Symbolic m
body' <- m (Symbolic m)
body
    let e :: NExprF (Symbolic m)
e = Symbolic m -> Symbolic m -> NExprF (Symbolic m)
forall r. r -> r -> NExprF r
NAssert Symbolic m
cond Symbolic m
body'
    Symbolic m
_ <- NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify (NExprF (Symbolic m) -> NExprF ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void NExprF (Symbolic m)
e) Symbolic m
cond (Symbolic m -> m (Symbolic m)) -> m (Symbolic m) -> m (Symbolic m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TBool]]
    Symbolic m -> m (Symbolic m)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Symbolic m
body'

  evalApp :: Symbolic m -> m (Symbolic m) -> m (Symbolic m)
evalApp = (((HashMap Text (Symbolic m), Symbolic m) -> Symbolic m)
-> m (HashMap Text (Symbolic m), Symbolic m) -> m (Symbolic m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HashMap Text (Symbolic m), Symbolic m) -> Symbolic m
forall a b. (a, b) -> b
snd (m (HashMap Text (Symbolic m), Symbolic m) -> m (Symbolic m))
-> (m (Symbolic m) -> m (HashMap Text (Symbolic m), Symbolic m))
-> m (Symbolic m)
-> m (Symbolic m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((m (Symbolic m) -> m (HashMap Text (Symbolic m), Symbolic m))
 -> m (Symbolic m) -> m (Symbolic m))
-> (Symbolic m
    -> m (Symbolic m) -> m (HashMap Text (Symbolic m), Symbolic m))
-> Symbolic m
-> m (Symbolic m)
-> m (Symbolic m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NExprF ()
-> Symbolic m
-> m (Symbolic m)
-> m (HashMap Text (Symbolic m), Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF ()
-> Symbolic m
-> m (Symbolic m)
-> m (HashMap Text (Symbolic m), Symbolic m)
lintApp (NBinaryOp -> () -> () -> NExprF ()
forall r. NBinaryOp -> r -> r -> NExprF r
NBinary NBinaryOp
NApp () ())
  evalAbs :: Params (m (Symbolic m))
-> (forall a.
    m (Symbolic m)
    -> (AttrSet (m (Symbolic m))
        -> m (Symbolic m) -> m (a, Symbolic m))
    -> m (a, Symbolic m))
-> m (Symbolic m)
evalAbs params :: Params (m (Symbolic m))
params _ = [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [Params () -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. Params () -> NTypeF m r
TClosure (Params (m (Symbolic m)) -> Params ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Params (m (Symbolic m))
params)]

  evalError :: s -> m a
evalError = s -> m a
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError

lintBinaryOp
  :: forall e m
   . (MonadLint e m, MonadEval (Symbolic m) m)
  => NBinaryOp
  -> Symbolic m
  -> m (Symbolic m)
  -> m (Symbolic m)
lintBinaryOp :: NBinaryOp -> Symbolic m -> m (Symbolic m) -> m (Symbolic m)
lintBinaryOp op :: NBinaryOp
op lsym :: Symbolic m
lsym rarg :: m (Symbolic m)
rarg = do
  Symbolic m
rsym <- m (Symbolic m)
rarg
  Symbolic m
y    <- m (Symbolic m) -> m (Symbolic m)
forall v (m :: * -> *). MonadValue v m => m v -> m v
defer m (Symbolic m)
forall (m :: * -> *). MonadVar m => m (Symbolic m)
everyPossible
  case NBinaryOp
op of
    NApp    -> String -> m (Symbolic m)
forall e (m :: * -> *) a. MonadLint e m => String -> m a
symerr "lintBinaryOp:NApp: should never get here"
    NEq     -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt, TAtom
TBool, TAtom
TNull], NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TStr, Symbolic m -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. r -> NTypeF m r
TList Symbolic m
y]
    NNEq    -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt, TAtom
TBool, TAtom
TNull], NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TStr, Symbolic m -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. r -> NTypeF m r
TList Symbolic m
y]

    NLt     -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt, TAtom
TBool, TAtom
TNull]]
    NLte    -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt, TAtom
TBool, TAtom
TNull]]
    NGt     -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt, TAtom
TBool, TAtom
TNull]]
    NGte    -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt, TAtom
TBool, TAtom
TNull]]

    NAnd    -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TBool]]
    NOr     -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TBool]]
    NImpl   -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TBool]]

    -- jww (2018-04-01): NYI: Allow Path + Str
    NPlus   -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt], NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TStr, NTypeF m (Symbolic m)
forall (m :: * -> *) r. NTypeF m r
TPath]
    NMinus  -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt]]
    NMult   -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt]]
    NDiv    -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [[TAtom] -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. [TAtom] -> NTypeF m r
TConstant [TAtom
TInt]]

    NUpdate -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [Maybe (HashMap Text (Symbolic m)) -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. Maybe (HashMap Text r) -> NTypeF m r
TSet Maybe (HashMap Text (Symbolic m))
forall a. Maybe a
Nothing]

    NConcat -> Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check Symbolic m
lsym Symbolic m
rsym [Symbolic m -> NTypeF m (Symbolic m)
forall (m :: * -> *) r. r -> NTypeF m r
TList Symbolic m
y]
 where
  check :: Symbolic m
-> Symbolic m -> [NTypeF m (Symbolic m)] -> m (Symbolic m)
check lsym :: Symbolic m
lsym rsym :: Symbolic m
rsym xs :: [NTypeF m (Symbolic m)]
xs = do
    let e :: NExprF (Symbolic m)
e = NBinaryOp -> Symbolic m -> Symbolic m -> NExprF (Symbolic m)
forall r. NBinaryOp -> r -> r -> NExprF r
NBinary NBinaryOp
op Symbolic m
lsym Symbolic m
rsym
    Symbolic m
m <- [NTypeF m (Symbolic m)] -> m (Symbolic m)
forall (m :: * -> *).
MonadVar m =>
[NTypeF m (Symbolic m)] -> m (Symbolic m)
mkSymbolic [NTypeF m (Symbolic m)]
xs
    Symbolic m
_ <- NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify (NExprF (Symbolic m) -> NExprF ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void NExprF (Symbolic m)
e) Symbolic m
lsym Symbolic m
m
    Symbolic m
_ <- NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify (NExprF (Symbolic m) -> NExprF ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void NExprF (Symbolic m)
e) Symbolic m
rsym Symbolic m
m
    NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify (NExprF (Symbolic m) -> NExprF ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void NExprF (Symbolic m)
e) Symbolic m
lsym Symbolic m
rsym

infixl 1 `lintApp`
lintApp
  :: forall e m
   . MonadLint e m
  => NExprF ()
  -> Symbolic m
  -> m (Symbolic m)
  -> m (HashMap VarName (Symbolic m), Symbolic m)
lintApp :: NExprF ()
-> Symbolic m
-> m (Symbolic m)
-> m (HashMap Text (Symbolic m), Symbolic m)
lintApp context :: NExprF ()
context fun :: Symbolic m
fun arg :: m (Symbolic m)
arg = Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *).
(MonadVar m, MonadThunkId m, MonadCatch m) =>
Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
unpackSymbolic Symbolic m
fun m (NSymbolicF (NTypeF m (Symbolic m)))
-> (NSymbolicF (NTypeF m (Symbolic m))
    -> m (HashMap Text (Symbolic m), Symbolic m))
-> m (HashMap Text (Symbolic m), Symbolic m)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  NAny ->
    ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m))
-> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "Cannot apply something not known to be a function"
  NMany xs :: [NTypeF m (Symbolic m)]
xs -> do
    (args :: [HashMap Text (Symbolic m)]
args, ys :: [Symbolic m]
ys) <- ([(HashMap Text (Symbolic m), Symbolic m)]
 -> ([HashMap Text (Symbolic m)], [Symbolic m]))
-> m [(HashMap Text (Symbolic m), Symbolic m)]
-> m ([HashMap Text (Symbolic m)], [Symbolic m])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(HashMap Text (Symbolic m), Symbolic m)]
-> ([HashMap Text (Symbolic m)], [Symbolic m])
forall a b. [(a, b)] -> ([a], [b])
unzip (m [(HashMap Text (Symbolic m), Symbolic m)]
 -> m ([HashMap Text (Symbolic m)], [Symbolic m]))
-> m [(HashMap Text (Symbolic m), Symbolic m)]
-> m ([HashMap Text (Symbolic m)], [Symbolic m])
forall a b. (a -> b) -> a -> b
$ [NTypeF m (Symbolic m)]
-> (NTypeF m (Symbolic m)
    -> m (HashMap Text (Symbolic m), Symbolic m))
-> m [(HashMap Text (Symbolic m), Symbolic m)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NTypeF m (Symbolic m)]
xs ((NTypeF m (Symbolic m)
  -> m (HashMap Text (Symbolic m), Symbolic m))
 -> m [(HashMap Text (Symbolic m), Symbolic m)])
-> (NTypeF m (Symbolic m)
    -> m (HashMap Text (Symbolic m), Symbolic m))
-> m [(HashMap Text (Symbolic m), Symbolic m)]
forall a b. (a -> b) -> a -> b
$ \case
      TClosure _params :: Params ()
_params -> m (Symbolic m)
arg m (Symbolic m)
-> (Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m))))
-> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
forall (m :: * -> *).
(MonadVar m, MonadThunkId m, MonadCatch m) =>
Symbolic m -> m (NSymbolicF (NTypeF m (Symbolic m)))
unpackSymbolic m (NSymbolicF (NTypeF m (Symbolic m)))
-> (NSymbolicF (NTypeF m (Symbolic m))
    -> m (HashMap Text (Symbolic m), Symbolic m))
-> m (HashMap Text (Symbolic m), Symbolic m)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        NAny -> do
          String -> m (HashMap Text (Symbolic m), Symbolic m)
forall a. HasCallStack => String -> a
error "NYI"

        NMany [TSet (Just _)] -> do
          String -> m (HashMap Text (Symbolic m), Symbolic m)
forall a. HasCallStack => String -> a
error "NYI"

        NMany _ -> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m))
-> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "NYI: lintApp NMany not set"
      TBuiltin _ _f :: Symbolic m -> m (Symbolic m)
_f -> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m))
-> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "NYI: lintApp builtin"
      TSet _m :: Maybe (HashMap Text (Symbolic m))
_m       -> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m))
-> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "NYI: lintApp Set"
      _x :: NTypeF m (Symbolic m)
_x            -> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall s e (m :: * -> *) a.
(Framed e m, Exception s, MonadThrow m) =>
s -> m a
throwError (ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m))
-> ErrorCall -> m (HashMap Text (Symbolic m), Symbolic m)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
ErrorCall "Attempt to call non-function"

    Symbolic m
y <- m (Symbolic m)
forall (m :: * -> *). MonadVar m => m (Symbolic m)
everyPossible
    ([HashMap Text (Symbolic m)] -> HashMap Text (Symbolic m)
forall a. [a] -> a
head [HashMap Text (Symbolic m)]
args, ) (Symbolic m -> (HashMap Text (Symbolic m), Symbolic m))
-> m (Symbolic m) -> m (HashMap Text (Symbolic m), Symbolic m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbolic m -> Symbolic m -> m (Symbolic m))
-> Symbolic m -> [Symbolic m] -> m (Symbolic m)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
forall e (m :: * -> *).
MonadLint e m =>
NExprF () -> Symbolic m -> Symbolic m -> m (Symbolic m)
unify NExprF ()
context) Symbolic m
y [Symbolic m]
ys

newtype Lint s a = Lint
  { Lint s a
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
runLint :: ReaderT (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a }
  deriving
    ( a -> Lint s b -> Lint s a
(a -> b) -> Lint s a -> Lint s b
(forall a b. (a -> b) -> Lint s a -> Lint s b)
-> (forall a b. a -> Lint s b -> Lint s a) -> Functor (Lint s)
forall a b. a -> Lint s b -> Lint s a
forall a b. (a -> b) -> Lint s a -> Lint s b
forall s a b. a -> Lint s b -> Lint s a
forall s a b. (a -> b) -> Lint s a -> Lint s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Lint s b -> Lint s a
$c<$ :: forall s a b. a -> Lint s b -> Lint s a
fmap :: (a -> b) -> Lint s a -> Lint s b
$cfmap :: forall s a b. (a -> b) -> Lint s a -> Lint s b
Functor
    , Functor (Lint s)
a -> Lint s a
Functor (Lint s) =>
(forall a. a -> Lint s a)
-> (forall a b. Lint s (a -> b) -> Lint s a -> Lint s b)
-> (forall a b c.
    (a -> b -> c) -> Lint s a -> Lint s b -> Lint s c)
-> (forall a b. Lint s a -> Lint s b -> Lint s b)
-> (forall a b. Lint s a -> Lint s b -> Lint s a)
-> Applicative (Lint s)
Lint s a -> Lint s b -> Lint s b
Lint s a -> Lint s b -> Lint s a
Lint s (a -> b) -> Lint s a -> Lint s b
(a -> b -> c) -> Lint s a -> Lint s b -> Lint s c
forall s. Functor (Lint s)
forall a. a -> Lint s a
forall s a. a -> Lint s a
forall a b. Lint s a -> Lint s b -> Lint s a
forall a b. Lint s a -> Lint s b -> Lint s b
forall a b. Lint s (a -> b) -> Lint s a -> Lint s b
forall s a b. Lint s a -> Lint s b -> Lint s a
forall s a b. Lint s a -> Lint s b -> Lint s b
forall s a b. Lint s (a -> b) -> Lint s a -> Lint s b
forall a b c. (a -> b -> c) -> Lint s a -> Lint s b -> Lint s c
forall s a b c. (a -> b -> c) -> Lint s a -> Lint s b -> Lint s c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Lint s a -> Lint s b -> Lint s a
$c<* :: forall s a b. Lint s a -> Lint s b -> Lint s a
*> :: Lint s a -> Lint s b -> Lint s b
$c*> :: forall s a b. Lint s a -> Lint s b -> Lint s b
liftA2 :: (a -> b -> c) -> Lint s a -> Lint s b -> Lint s c
$cliftA2 :: forall s a b c. (a -> b -> c) -> Lint s a -> Lint s b -> Lint s c
<*> :: Lint s (a -> b) -> Lint s a -> Lint s b
$c<*> :: forall s a b. Lint s (a -> b) -> Lint s a -> Lint s b
pure :: a -> Lint s a
$cpure :: forall s a. a -> Lint s a
$cp1Applicative :: forall s. Functor (Lint s)
Applicative
    , Applicative (Lint s)
a -> Lint s a
Applicative (Lint s) =>
(forall a b. Lint s a -> (a -> Lint s b) -> Lint s b)
-> (forall a b. Lint s a -> Lint s b -> Lint s b)
-> (forall a. a -> Lint s a)
-> Monad (Lint s)
Lint s a -> (a -> Lint s b) -> Lint s b
Lint s a -> Lint s b -> Lint s b
forall s. Applicative (Lint s)
forall a. a -> Lint s a
forall s a. a -> Lint s a
forall a b. Lint s a -> Lint s b -> Lint s b
forall a b. Lint s a -> (a -> Lint s b) -> Lint s b
forall s a b. Lint s a -> Lint s b -> Lint s b
forall s a b. Lint s a -> (a -> Lint s b) -> Lint s b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Lint s a
$creturn :: forall s a. a -> Lint s a
>> :: Lint s a -> Lint s b -> Lint s b
$c>> :: forall s a b. Lint s a -> Lint s b -> Lint s b
>>= :: Lint s a -> (a -> Lint s b) -> Lint s b
$c>>= :: forall s a b. Lint s a -> (a -> Lint s b) -> Lint s b
$cp1Monad :: forall s. Applicative (Lint s)
Monad
    , Monad (Lint s)
Monad (Lint s) =>
(forall a. (a -> Lint s a) -> Lint s a) -> MonadFix (Lint s)
(a -> Lint s a) -> Lint s a
forall s. Monad (Lint s)
forall a. (a -> Lint s a) -> Lint s a
forall s a. (a -> Lint s a) -> Lint s a
forall (m :: * -> *).
Monad m =>
(forall a. (a -> m a) -> m a) -> MonadFix m
mfix :: (a -> Lint s a) -> Lint s a
$cmfix :: forall s a. (a -> Lint s a) -> Lint s a
$cp1MonadFix :: forall s. Monad (Lint s)
MonadFix
    , MonadReader (Context (Lint s) (Symbolic (Lint s)))
    , Eq (ThunkId (Lint s))
Monad (Lint s)
Ord (ThunkId (Lint s))
Show (ThunkId (Lint s))
Typeable (ThunkId (Lint s))
Lint s (ThunkId (Lint s))
(Monad (Lint s), Eq (ThunkId (Lint s)), Ord (ThunkId (Lint s)),
 Show (ThunkId (Lint s)), Typeable (ThunkId (Lint s))) =>
Lint s (ThunkId (Lint s)) -> MonadThunkId (Lint s)
forall s. Eq (ThunkId (Lint s))
forall s. Monad (Lint s)
forall s. Ord (ThunkId (Lint s))
forall s. Show (ThunkId (Lint s))
forall s. Typeable (ThunkId (Lint s))
forall s. Lint s (ThunkId (Lint s))
forall (m :: * -> *).
(Monad m, Eq (ThunkId m), Ord (ThunkId m), Show (ThunkId m),
 Typeable (ThunkId m)) =>
m (ThunkId m) -> MonadThunkId m
freshId :: Lint s (ThunkId (Lint s))
$cfreshId :: forall s. Lint s (ThunkId (Lint s))
$cp5MonadThunkId :: forall s. Typeable (ThunkId (Lint s))
$cp4MonadThunkId :: forall s. Show (ThunkId (Lint s))
$cp3MonadThunkId :: forall s. Ord (ThunkId (Lint s))
$cp2MonadThunkId :: forall s. Eq (ThunkId (Lint s))
$cp1MonadThunkId :: forall s. Monad (Lint s)
MonadThunkId
    , Monad (Lint s)
a -> Lint s (Ref (Lint s) a)
Monad (Lint s) =>
(forall a. a -> Lint s (Ref (Lint s) a))
-> (forall a. Ref (Lint s) a -> Lint s a)
-> (forall a. Ref (Lint s) a -> a -> Lint s ())
-> (forall a. Ref (Lint s) a -> (a -> a) -> Lint s ())
-> (forall a. Ref (Lint s) a -> (a -> a) -> Lint s ())
-> MonadRef (Lint s)
Ref (Lint s) a -> Lint s a
Ref (Lint s) a -> a -> Lint s ()
Ref (Lint s) a -> (a -> a) -> Lint s ()
Ref (Lint s) a -> (a -> a) -> Lint s ()
forall s. Monad (Lint s)
forall a. a -> Lint s (Ref (Lint s) a)
forall a. Ref (Lint s) a -> Lint s a
forall a. Ref (Lint s) a -> a -> Lint s ()
forall a. Ref (Lint s) a -> (a -> a) -> Lint s ()
forall s a. a -> Lint s (Ref (Lint s) a)
forall s a. Ref (Lint s) a -> Lint s a
forall s a. Ref (Lint s) a -> a -> Lint s ()
forall s a. Ref (Lint s) a -> (a -> a) -> Lint s ()
forall (m :: * -> *).
Monad m =>
(forall a. a -> m (Ref m a))
-> (forall a. Ref m a -> m a)
-> (forall a. Ref m a -> a -> m ())
-> (forall a. Ref m a -> (a -> a) -> m ())
-> (forall a. Ref m a -> (a -> a) -> m ())
-> MonadRef m
modifyRef' :: Ref (Lint s) a -> (a -> a) -> Lint s ()
$cmodifyRef' :: forall s a. Ref (Lint s) a -> (a -> a) -> Lint s ()
modifyRef :: Ref (Lint s) a -> (a -> a) -> Lint s ()
$cmodifyRef :: forall s a. Ref (Lint s) a -> (a -> a) -> Lint s ()
writeRef :: Ref (Lint s) a -> a -> Lint s ()
$cwriteRef :: forall s a. Ref (Lint s) a -> a -> Lint s ()
readRef :: Ref (Lint s) a -> Lint s a
$creadRef :: forall s a. Ref (Lint s) a -> Lint s a
newRef :: a -> Lint s (Ref (Lint s) a)
$cnewRef :: forall s a. a -> Lint s (Ref (Lint s) a)
$cp1MonadRef :: forall s. Monad (Lint s)
MonadRef
    , MonadRef (Lint s)
Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
MonadRef (Lint s) =>
(forall a b. Ref (Lint s) a -> (a -> (a, b)) -> Lint s b)
-> (forall a b. Ref (Lint s) a -> (a -> (a, b)) -> Lint s b)
-> MonadAtomicRef (Lint s)
forall s. MonadRef (Lint s)
forall a b. Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
forall s a b. Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
forall (m :: * -> *).
MonadRef m =>
(forall a b. Ref m a -> (a -> (a, b)) -> m b)
-> (forall a b. Ref m a -> (a -> (a, b)) -> m b)
-> MonadAtomicRef m
atomicModifyRef' :: Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
$catomicModifyRef' :: forall s a b. Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
atomicModifyRef :: Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
$catomicModifyRef :: forall s a b. Ref (Lint s) a -> (a -> (a, b)) -> Lint s b
$cp1MonadAtomicRef :: forall s. MonadRef (Lint s)
MonadAtomicRef
    )

instance MonadThrow (Lint s) where
  throwM :: e -> Lint s a
throwM e :: e
e = ReaderT
  (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> Lint s a
forall s a.
ReaderT
  (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> Lint s a
Lint (ReaderT
   (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
 -> Lint s a)
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> Lint s a
forall a b. (a -> b) -> a -> b
$ (Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a)
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a)
 -> ReaderT
      (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a)
-> (Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a)
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
forall a b. (a -> b) -> a -> b
$ \_ -> e -> FreshIdT Int (ST s) a
forall a e. Exception e => e -> a
throw e
e

instance MonadCatch (Lint s) where
  catch :: Lint s a -> (e -> Lint s a) -> Lint s a
catch _m :: Lint s a
_m _h :: e -> Lint s a
_h = ReaderT
  (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> Lint s a
forall s a.
ReaderT
  (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> Lint s a
Lint (ReaderT
   (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
 -> Lint s a)
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> Lint s a
forall a b. (a -> b) -> a -> b
$ (Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a)
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a)
 -> ReaderT
      (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a)
-> (Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a)
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
forall a b. (a -> b) -> a -> b
$ \_ -> String -> FreshIdT Int (ST s) a
forall a. HasCallStack => String -> a
error "Cannot catch in 'Lint s'"

runLintM :: Options -> Lint s a -> ST s a
runLintM :: Options -> Lint s a -> ST s a
runLintM opts :: Options
opts action :: Lint s a
action = do
  STRef s Int
i <- Int -> ST s (Ref (ST s) Int)
forall (m :: * -> *) a. MonadRef m => a -> m (Ref m a)
newVar (1 :: Int)
  Ref (ST s) Int -> FreshIdT Int (ST s) a -> ST s a
forall (m :: * -> *) i a.
Functor m =>
Var m i -> FreshIdT i m a -> m a
runFreshIdT STRef s Int
Ref (ST s) Int
i (FreshIdT Int (ST s) a -> ST s a)
-> FreshIdT Int (ST s) a -> ST s a
forall a b. (a -> b) -> a -> b
$ (ReaderT
   (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
 -> Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a)
-> Context (Lint s) (Symbolic (Lint s))
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> FreshIdT Int (ST s) a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> Context (Lint s) (Symbolic (Lint s)) -> FreshIdT Int (ST s) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Options -> Context (Lint s) (Symbolic (Lint s))
forall (m :: * -> *) t. Options -> Context m t
newContext Options
opts) (ReaderT
   (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
 -> FreshIdT Int (ST s) a)
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
-> FreshIdT Int (ST s) a
forall a b. (a -> b) -> a -> b
$ Lint s a
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
forall s a.
Lint s a
-> ReaderT
     (Context (Lint s) (Symbolic (Lint s))) (FreshIdT Int (ST s)) a
runLint Lint s a
action

symbolicBaseEnv :: Monad m => m (Scopes m (Symbolic m))
symbolicBaseEnv :: m (Scopes m (Symbolic m))
symbolicBaseEnv = Scopes m (Symbolic m) -> m (Scopes m (Symbolic m))
forall (m :: * -> *) a. Monad m => a -> m a
return Scopes m (Symbolic m)
forall (m :: * -> *) a. Scopes m a
emptyScopes

lint :: Options -> NExprLoc -> ST s (Symbolic (Lint s))
lint :: Options -> NExprLoc -> ST s (Symbolic (Lint s))
lint opts :: Options
opts expr :: NExprLoc
expr =
  Options -> Lint s (Symbolic (Lint s)) -> ST s (Symbolic (Lint s))
forall s a. Options -> Lint s a -> ST s a
runLintM Options
opts
    (Lint s (Symbolic (Lint s)) -> ST s (Symbolic (Lint s)))
-> Lint s (Symbolic (Lint s)) -> ST s (Symbolic (Lint s))
forall a b. (a -> b) -> a -> b
$   Lint s (Scopes (Lint s) (Symbolic (Lint s)))
forall (m :: * -> *). Monad m => m (Scopes m (Symbolic m))
symbolicBaseEnv
    Lint s (Scopes (Lint s) (Symbolic (Lint s)))
-> (Scopes (Lint s) (Symbolic (Lint s))
    -> Lint s (Symbolic (Lint s)))
-> Lint s (Symbolic (Lint s))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Scopes (Lint s) (Symbolic (Lint s))
-> Lint s (Symbolic (Lint s)) -> Lint s (Symbolic (Lint s))
forall a (m :: * -> *) r. Scoped a m => Scopes m a -> m r -> m r
`pushScopes` (Compose (Ann SrcSpan) NExprF (Lint s (Symbolic (Lint s)))
 -> Lint s (Symbolic (Lint s)))
-> ((NExprLoc -> Lint s (Symbolic (Lint s)))
    -> NExprLoc -> Lint s (Symbolic (Lint s)))
-> NExprLoc
-> Lint s (Symbolic (Lint s))
forall (f :: * -> *) a.
Functor f =>
(f a -> a) -> ((Fix f -> a) -> Fix f -> a) -> Fix f -> a
adi (NExprF (Lint s (Symbolic (Lint s))) -> Lint s (Symbolic (Lint s))
forall v (m :: * -> *). MonadNixEval v m => NExprF (m v) -> m v
Eval.eval (NExprF (Lint s (Symbolic (Lint s))) -> Lint s (Symbolic (Lint s)))
-> (Compose (Ann SrcSpan) NExprF (Lint s (Symbolic (Lint s)))
    -> NExprF (Lint s (Symbolic (Lint s))))
-> Compose (Ann SrcSpan) NExprF (Lint s (Symbolic (Lint s)))
-> Lint s (Symbolic (Lint s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ann SrcSpan (NExprF (Lint s (Symbolic (Lint s))))
-> NExprF (Lint s (Symbolic (Lint s)))
forall ann a. Ann ann a -> a
annotated (Ann SrcSpan (NExprF (Lint s (Symbolic (Lint s))))
 -> NExprF (Lint s (Symbolic (Lint s))))
-> (Compose (Ann SrcSpan) NExprF (Lint s (Symbolic (Lint s)))
    -> Ann SrcSpan (NExprF (Lint s (Symbolic (Lint s)))))
-> Compose (Ann SrcSpan) NExprF (Lint s (Symbolic (Lint s)))
-> NExprF (Lint s (Symbolic (Lint s)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose (Ann SrcSpan) NExprF (Lint s (Symbolic (Lint s)))
-> Ann SrcSpan (NExprF (Lint s (Symbolic (Lint s))))
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
                          (NExprLoc -> Lint s (Symbolic (Lint s)))
-> NExprLoc -> Lint s (Symbolic (Lint s))
forall e (m :: * -> *) a.
(MonadReader e m, Has e SrcSpan) =>
Transform NExprLocF (m a)
Eval.addSourcePositions
                          NExprLoc
expr
        )

instance Scoped (Symbolic (Lint s)) (Lint s) where
  currentScopes :: Lint s (Scopes (Lint s) (Symbolic (Lint s)))
currentScopes = Lint s (Scopes (Lint s) (Symbolic (Lint s)))
forall (m :: * -> *) a e.
(MonadReader e m, Has e (Scopes m a)) =>
m (Scopes m a)
currentScopesReader
  clearScopes :: Lint s r -> Lint s r
clearScopes   = forall e r.
(MonadReader e (Lint s),
 Has e (Scopes (Lint s) (Symbolic (Lint s)))) =>
Lint s r -> Lint s r
forall (m :: * -> *) a e r.
(MonadReader e m, Has e (Scopes m a)) =>
m r -> m r
clearScopesReader @(Lint s) @(Symbolic (Lint s))
  pushScopes :: Scopes (Lint s) (Symbolic (Lint s)) -> Lint s r -> Lint s r
pushScopes    = Scopes (Lint s) (Symbolic (Lint s)) -> Lint s r -> Lint s r
forall e (m :: * -> *) a r.
(MonadReader e m, Has e (Scopes m a)) =>
Scopes m a -> m r -> m r
pushScopesReader
  lookupVar :: Text -> Lint s (Maybe (Symbolic (Lint s)))
lookupVar     = Text -> Lint s (Maybe (Symbolic (Lint s)))
forall (m :: * -> *) a e.
(MonadReader e m, Has e (Scopes m a)) =>
Text -> m (Maybe a)
lookupVarReader