module Disco.Typecheck.Util where
import Disco.Effects.Fresh
import Polysemy
import Polysemy.Error
import Polysemy.Output
import Polysemy.Reader
import Polysemy.Writer
import Unbound.Generics.LocallyNameless (Name, bind, string2Name)
import qualified Data.Map as M
import Data.Tuple (swap)
import Prelude hiding (lookup)
import Disco.AST.Surface
import Disco.Context
import Disco.Messages
import Disco.Names (ModuleName, QName)
import Disco.Typecheck.Constraints
import Disco.Typecheck.Solve
import Disco.Types
type TyCtx = Ctx Term PolyType
data LocTCError = LocTCError (Maybe (QName Term)) TCError
deriving (Int -> LocTCError -> ShowS
[LocTCError] -> ShowS
LocTCError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LocTCError] -> ShowS
$cshowList :: [LocTCError] -> ShowS
show :: LocTCError -> String
$cshow :: LocTCError -> String
showsPrec :: Int -> LocTCError -> ShowS
$cshowsPrec :: Int -> LocTCError -> ShowS
Show)
noLoc :: TCError -> LocTCError
noLoc :: TCError -> LocTCError
noLoc = Maybe (QName Term) -> TCError -> LocTCError
LocTCError forall a. Maybe a
Nothing
data TCError
=
Unbound (Name Term)
|
Ambiguous (Name Term) [ModuleName]
|
NoType (Name Term)
|
NotCon Con Term Type
|
EmptyCase
|
PatternType Con Pattern Type
|
DuplicateDecls (Name Term)
|
DuplicateDefns (Name Term)
|
DuplicateTyDefns String
|
CyclicTyDef String
|
NumPatterns
|
NonlinearPattern Pattern (Name Term)
|
NoSearch Type
|
Unsolvable SolveError
|
NotTyDef String
|
NoTWild
|
NotEnoughArgs Con
|
TooManyArgs Con
|
UnboundTyVar (Name Type)
|
NoPolyRec String [String] [Type]
|
NoError
deriving (Int -> TCError -> ShowS
[TCError] -> ShowS
TCError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCError] -> ShowS
$cshowList :: [TCError] -> ShowS
show :: TCError -> String
$cshow :: TCError -> String
showsPrec :: Int -> TCError -> ShowS
$cshowsPrec :: Int -> TCError -> ShowS
Show)
instance Semigroup TCError where
TCError
_ <> :: TCError -> TCError -> TCError
<> TCError
r = TCError
r
instance Monoid TCError where
mempty :: TCError
mempty = TCError
NoError
mappend :: TCError -> TCError -> TCError
mappend = forall a. Semigroup a => a -> a -> a
(<>)
constraint :: Member (Writer Constraint) r => Constraint -> Sem r ()
constraint :: forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint = forall o (r :: EffectRow). Member (Writer o) r => o -> Sem r ()
tell
constraints :: Member (Writer Constraint) r => [Constraint] -> Sem r ()
constraints :: forall (r :: EffectRow).
Member (Writer Constraint) r =>
[Constraint] -> Sem r ()
constraints = forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint] -> Constraint
cAnd
forAll :: Member (Writer Constraint) r => [Name Type] -> Sem r a -> Sem r a
forAll :: forall (r :: EffectRow) a.
Member (Writer Constraint) r =>
[Name Type] -> Sem r a -> Sem r a
forAll [Name Type]
nms = forall o (r :: EffectRow) a.
Member (Writer o) r =>
(o -> o) -> Sem r a -> Sem r a
censor (Bind [Name Type] Constraint -> Constraint
CAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Type]
nms)
cOr :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r ()
cOr :: forall (r :: EffectRow).
Members '[Writer Constraint] r =>
Sem r () -> Sem r () -> Sem r ()
cOr Sem r ()
m1 Sem r ()
m2 = do
(Constraint
c1, ()
_) <- forall o (r :: EffectRow) a.
Member (Writer o) r =>
(o -> o) -> Sem r a -> Sem r a
censor (forall a b. a -> b -> a
const Constraint
CTrue) (forall o (r :: EffectRow) a.
Member (Writer o) r =>
Sem r a -> Sem r (o, a)
listen Sem r ()
m1)
(Constraint
c2, ()
_) <- forall o (r :: EffectRow) a.
Member (Writer o) r =>
(o -> o) -> Sem r a -> Sem r a
censor (forall a b. a -> b -> a
const Constraint
CTrue) (forall o (r :: EffectRow) a.
Member (Writer o) r =>
Sem r a -> Sem r (o, a)
listen Sem r ()
m2)
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ [Constraint] -> Constraint
COr [Constraint
c1, Constraint
c2]
withConstraint :: Sem (Writer Constraint ': r) a -> Sem r (a, Constraint)
withConstraint :: forall (r :: EffectRow) a.
Sem (Writer Constraint : r) a -> Sem r (a, Constraint)
withConstraint = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> (b, a)
swap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o (r :: EffectRow) a.
Monoid o =>
Sem (Writer o : r) a -> Sem r (o, a)
runWriter
solve ::
Members '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Sem (Writer Constraint ': r) a ->
Sem r (a, S)
solve :: forall ann (r :: EffectRow) a.
Members
'[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve Sem (Writer Constraint : r) a
m = do
(a
a, Constraint
c) <- forall (r :: EffectRow) a.
Sem (Writer Constraint : r) a -> Sem r (a, Constraint)
withConstraint Sem (Writer Constraint : r) a
m
Either SolveError S
res <- forall (r :: EffectRow) a.
Sem (Fresh : Error SolveError : r) a -> Sem r (Either SolveError a)
runSolve forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: EffectRow) a.
Member (Reader i) r =>
Sem (Input i : r) a -> Sem r a
inputToReader forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann (r :: EffectRow).
Members
'[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx]
r =>
Constraint -> Sem r S
solveConstraint forall a b. (a -> b) -> a -> b
$ Constraint
c
case Either SolveError S
res of
Left SolveError
e -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (SolveError -> TCError
Unsolvable SolveError
e)
Right S
s -> forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, S
s)
lookupTyDefn ::
Members '[Reader TyDefCtx, Error TCError] r =>
String ->
[Type] ->
Sem r Type
lookupTyDefn :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
x [Type]
args = do
TyDefCtx
d <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyDefCtx
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
x TyDefCtx
d of
Maybe TyDefBody
Nothing -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (String -> TCError
NotTyDef String
x)
Just (TyDefBody [String]
_ [Type] -> Type
body) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Type] -> Type
body [Type]
args
withTyDefns :: Member (Reader TyDefCtx) r => TyDefCtx -> Sem r a -> Sem r a
withTyDefns :: forall (r :: EffectRow) a.
Member (Reader TyDefCtx) r =>
TyDefCtx -> Sem r a -> Sem r a
withTyDefns TyDefCtx
tyDefnCtx = forall i (r :: EffectRow) a.
Member (Reader i) r =>
(i -> i) -> Sem r a -> Sem r a
local (forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union TyDefCtx
tyDefnCtx)
freshTy :: Member Fresh r => Sem r Type
freshTy :: forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy = Name Type -> Type
TyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"a")
freshAtom :: Member Fresh r => Sem r Atom
freshAtom :: forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom = Var -> Atom
AVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name Type -> Var
U forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"c")