~jojo/Carth

41b6f9f79f0e9e6ed1b939da73db7c5e4e25e3ae — JoJo 1 year, 11 months ago 5807eef
Add phantom param to Id to encode upper/lower case

Will be useful when instancing Arbitrary, to have separate instances
for each case.
5 files changed, 69 insertions(+), 52 deletions(-)

M package.yaml
M src/Ast.hs
M src/Check.hs
M src/Parse.hs
M src/TypeErr.hs
M package.yaml => package.yaml +2 -0
@@ 55,6 55,7 @@ library:
  - -Wno-orphans
  - -Wno-missed-specialisations
  - -Wno-all-missed-specialisations
  - -Wno-unticked-promoted-constructors

executables:
  carth:


@@ 77,6 78,7 @@ executables:
    - -Wno-orphans
    - -Wno-missed-specialisations
    - -Wno-all-missed-specialisations
    - -Wno-unticked-promoted-constructors
    dependencies:
    - carth


M src/Ast.hs => src/Ast.hs +33 -24
@@ 1,5 1,6 @@
{-# LANGUAGE LambdaCase, TypeSynonymInstances, FlexibleInstances
           , MultiParamTypeClasses, TemplateHaskell #-}
           , MultiParamTypeClasses, TemplateHaskell, KindSignatures
           , DataKinds #-}

module Ast
    ( TVar(..)


@@ 9,7 10,8 @@ module Ast
    , Scheme(..)
    , scmParams
    , scmBody
    , Id
    , IdCase(..)
    , Id(..)
    , idstr
    , Const(..)
    , Pat(..)


@@ 34,11 36,13 @@ import SrcPos
import FreeVars
import NonEmpty

data IdCase = Big | Small

type Id = WithPos String
newtype Id (case' :: IdCase) = Id (WithPos String)
    deriving (Show, Eq, Ord)

data TVar
    = TVExplicit Id
    = TVExplicit (Id Small)
    | TVImplicit Int
    deriving (Show, Eq, Ord)



@@ 67,8 71,8 @@ data Scheme = Forall
makeLenses ''Scheme

data Pat
    = PConstruction SrcPos Id [Pat]
    | PVar Id
    = PConstruction SrcPos (Id Big) [Pat]
    | PVar (Id Small)
    deriving Show

data Const


@@ 82,25 86,25 @@ data Const

data Expr'
    = Lit Const
    | Var Id
    | Var (Id Small)
    | App Expr Expr
    | If Expr Expr Expr
    | Fun Id Expr
    | Fun (Id Small) Expr
    | Let (NonEmpty Def) Expr
    | TypeAscr Expr Type
    | Match Expr (NonEmpty (Pat, Expr))
    | FunMatch (NonEmpty (Pat, Expr))
    | Ctor Id
    | Ctor (Id Big)
    deriving (Show, Eq)

type Expr = WithPos Expr'

type Def = (Id, (Maybe (WithPos Scheme), Expr))
type Def = (Id Small, (Maybe (WithPos Scheme), Expr))

newtype ConstructorDefs = ConstructorDefs [(Id, [Type])]
newtype ConstructorDefs = ConstructorDefs [(Id Big, [Type])]
    deriving (Show, Eq)

data TypeDef = TypeDef Id [Id] ConstructorDefs
data TypeDef = TypeDef (Id Big) [Id Small] ConstructorDefs
    deriving (Show, Eq)

data Program = Program [Def] [TypeDef]


@@ 113,12 117,15 @@ instance Eq Pat where
        (PVar x, PVar x') -> x == x'
        _ -> False

instance FreeVars Def Id where
instance FreeVars Def (Id Small) where
    freeVars (name, (_, body)) = Set.delete name (freeVars body)

instance FreeVars Expr Id where
instance FreeVars Expr (Id Small) where
    freeVars = fvExpr

instance HasPos (Id a) where
    getPos (Id x) = getPos x

instance HasPos Pat where
    getPos = \case
        PConstruction p _ _ -> p


@@ 144,9 151,11 @@ instance Pretty TPrim where
    pretty' _ = prettyTPrim
instance Pretty TVar where
    pretty' _ = prettyTVar
instance Pretty (Id a) where
    pretty' _ = idstr


fvExpr :: Expr -> Set Id
fvExpr :: Expr -> Set (Id Small)
fvExpr = unpos >>> \case
    Lit _ -> Set.empty
    Var x -> Set.singleton x


@@ 160,13 169,13 @@ fvExpr = unpos >>> \case
    FunMatch cs -> fvCases (fromList1 cs)
    Ctor _ -> Set.empty

fvMatch :: Expr -> [(Pat, Expr)] -> Set Id
fvMatch :: Expr -> [(Pat, Expr)] -> Set (Id Small)
fvMatch e cs = Set.union (freeVars e) (fvCases cs)

fvCases :: [(Pat, Expr)] -> Set Id
fvCases :: [(Pat, Expr)] -> Set (Id Small)
fvCases = Set.unions . map (\(p, e) -> Set.difference (freeVars e) (bvPat p))

bvPat :: Pat -> Set Id
bvPat :: Pat -> Set (Id Small)
bvPat = \case
    PConstruction _ _ ps -> Set.unions (map bvPat ps)
    PVar x -> Set.singleton x


@@ 191,9 200,8 @@ prettyTypeDef d (TypeDef name params constrs) = concat
    [ "(type "
    , if null params
        then pretty name
        else "(" ++ pretty name ++ spcPretty params ++ ")"
    , indent (d + 2) ++ pretty' (d + 2) constrs
    , ")"
        else "(" ++ pretty name ++ " " ++ spcPretty params ++ ")"
    , "\n" ++ indent (d + 2) ++ pretty' (d + 2) constrs ++ ")"
    ]

prettyConstructorDefs :: Int -> ConstructorDefs -> String


@@ 264,7 272,8 @@ prettyExpr' d = \case

prettyPat :: Pat -> String
prettyPat = \case
    PConstruction _ c ps -> concat ["(", idstr c, " ", spcPretty ps, ")"]
    PConstruction _ (Id (WithPos _ c)) ps ->
        if null ps then c else concat ["(", c, " ", spcPretty ps, ")"]
    PVar v -> idstr v

prettyConst :: Const -> String


@@ 315,5 324,5 @@ prettyTVar = \case
spcPretty :: Pretty a => [a] -> String
spcPretty = unwords . map pretty

idstr :: Id -> String
idstr = unpos
idstr :: Id a -> String
idstr (Id (WithPos _ x)) = x

M src/Check.hs => src/Check.hs +20 -14
@@ 1,5 1,6 @@
{-# LANGUAGE LambdaCase, OverloadedStrings, TemplateHaskell, TupleSections
  , TypeSynonymInstances, FlexibleInstances, RankNTypes, FlexibleContexts #-}
  , TypeSynonymInstances, FlexibleInstances, RankNTypes, FlexibleContexts
  , DataKinds #-}

module Check (typecheck) where



@@ 24,7 25,7 @@ import FreeVars
import Subst
import NonEmpty
import qualified Ast
import Ast (Id, idstr, scmBody)
import Ast (Id(..), IdCase(..), idstr, scmBody)
import TypeErr
import AnnotAst
import Match


@@ 104,7 105,7 @@ inferProgram (Ast.Program defs tdefs) = do
    (_, (WithPos mainPos _)) <- maybe
        (throwError MainNotDefined)
        pure
        (lookup "main" (map (first unpos) defs))
        (lookup "main" (map (first idstr) defs))
    (tdefs', ctors) <- checkTypeDefs tdefs
    Defs defs' <-
        augment envTypeDefs tdefs' $ augment envCtors ctors $ inferDefs defs


@@ 136,9 137,12 @@ checkTypeDef
    :: Ast.TypeDef
    -> Infer
           ( (String, ([TVar], [(String, [Type])]))
           , Map String (Id, (VariantIx, (String, [TVar]), [Type], Span))
           , Map
                 String
                 (Id Big, (VariantIx, (String, [TVar]), [Type], Span))
           )
checkTypeDef (Ast.TypeDef (WithPos _ x) ps (Ast.ConstructorDefs cs)) = do
checkTypeDef (Ast.TypeDef x' ps (Ast.ConstructorDefs cs)) = do
    let x = idstr x'
    let ps' = map TVExplicit ps
    let cs' = map (first idstr) cs
    let cSpan = length cs


@@ 284,7 288,7 @@ inferCase (p, b) = do
    let ppos = getPos p
    pure (Found ppos tp, Found (getPos b) tb, (ppos, p', b'))

inferPat :: Ast.Pat -> Infer (Type, Pat, Map Id Scheme)
inferPat :: Ast.Pat -> Infer (Type, Pat, Map (Id Small) Scheme)
inferPat = \case
    Ast.PConstruction pos c ps -> inferPatConstruction pos c ps
    Ast.PVar x -> do


@@ 294,7 298,7 @@ inferPat = \case
        pure (tv', PVar x', Map.singleton x (Forall Set.empty tv'))

inferPatConstruction
    :: SrcPos -> Id -> [Ast.Pat] -> Infer (Type, Pat, Map Id Scheme)
    :: SrcPos -> Id Big -> [Ast.Pat] -> Infer (Type, Pat, Map (Id Small) Scheme)
inferPatConstruction pos c cArgs = do
    (variantIx, tdefLhs, cParams, cSpan) <- lookupEnvConstructor c
    let arity = length cParams


@@ 309,13 313,14 @@ inferPatConstruction pos c cArgs = do
    let con = Con { variant = variantIx, span = cSpan, argTs = cArgTs }
    pure (t, PCon con cArgs', cArgsVars')

nonconflictingPatVarDefs :: [Map Id Scheme] -> Infer (Map Id Scheme)
nonconflictingPatVarDefs
    :: [Map (Id Small) Scheme] -> Infer (Map (Id Small) Scheme)
nonconflictingPatVarDefs = flip foldM Map.empty $ \acc ks ->
    case listToMaybe (Map.keys (Map.intersection acc ks)) of
        Just (WithPos pos v) -> throwError (ConflictingPatVarDefs pos v)
        Just (Id (WithPos pos v)) -> throwError (ConflictingPatVarDefs pos v)
        Nothing -> pure (Map.union acc ks)

inferExprConstructor :: Id -> Infer (Type, Expr)
inferExprConstructor :: Id Big -> Infer (Type, Expr)
inferExprConstructor c = do
    (variantIx, tdefLhs, cParams, _) <- lookupEnvConstructor c
    (tdefInst, cParams') <- instantiateConstructorOfTypeDef tdefLhs cParams


@@ 334,8 339,9 @@ instantiateConstructorOfTypeDef (tName, tParams) cParams = do
    let cParams' = map (subst (Map.fromList (zip tParams tVars))) cParams
    pure ((tName, tVars), cParams')

lookupEnvConstructor :: Id -> Infer (VariantIx, (String, [TVar]), [Type], Span)
lookupEnvConstructor (WithPos pos cx) =
lookupEnvConstructor
    :: Id Big -> Infer (VariantIx, (String, [TVar]), [Type], Span)
lookupEnvConstructor (Id (WithPos pos cx)) =
    views envCtors (Map.lookup cx)
        >>= maybe (throwError (UndefCtor pos cx)) pure



@@ 348,8 354,8 @@ litType = \case
    Str _ -> TPrim TStr
    Bool _ -> TPrim TBool

lookupEnv :: Id -> Infer Type
lookupEnv (WithPos pos x) = views envDefs (Map.lookup x) >>= \case
lookupEnv :: Id Small -> Infer Type
lookupEnv (Id (WithPos pos x)) = views envDefs (Map.lookup x) >>= \case
    Just scm -> instantiate scm
    Nothing -> throwError (UndefVar pos x)


M src/Parse.hs => src/Parse.hs +8 -8
@@ 1,4 1,4 @@
{-# LANGUAGE FlexibleContexts, LambdaCase, TupleSections #-}
{-# LANGUAGE FlexibleContexts, LambdaCase, TupleSections, DataKinds #-}

-- Note: Some parsers are greedy wrt consuming spaces and comments succeding the
--       item, while others are lazy. You'll have to look at the impl to be


@@ 94,7 94,7 @@ defTyped = (reserved "define:" *>) . def' (fmap Just scheme)
def'
    :: Parser (Maybe (WithPos Scheme))
    -> SrcPos
    -> Parser (Id, (Maybe (WithPos Scheme), Expr))
    -> Parser (Id Small, (Maybe (WithPos Scheme), Expr))
def' schemeParser topPos = varDef <|> funDef
  where
    varDef = do


@@ 280,11 280,11 @@ ns_parens p = choice
        [("(", ")"), ("[", "]")]
    )

big' :: Parser Id
big' :: Parser (Id Big)
big' = andSkipSpaceAfter ns_big'

ns_big' :: Parser Id
ns_big' = withPos ns_big
ns_big' :: Parser (Id Big)
ns_big' = fmap Id (withPos ns_big)

big :: Parser String
big = andSkipSpaceAfter ns_big


@@ 297,11 297,11 @@ ns_big = try $ do
        then pure s
        else fail "Big identifier must start with an uppercase letter or colon."

small' :: Parser Id
small' :: Parser (Id Small)
small' = andSkipSpaceAfter ns_small'

ns_small' :: Parser Id
ns_small' = withPos $ try $ do
ns_small' :: Parser (Id Small)
ns_small' = fmap Id $ withPos $ try $ do
    s <- identifier
    let c = head s
    if (isUpper c || [c] == ":")

M src/TypeErr.hs => src/TypeErr.hs +6 -6
@@ 1,4 1,4 @@
{-# LANGUAGE LambdaCase, FlexibleContexts #-}
{-# LANGUAGE LambdaCase, FlexibleContexts, DataKinds #-}

module TypeErr (TypeErr(..), prettyErr) where



@@ 15,14 15,14 @@ import Control.Applicative
data TypeErr
    = MainNotDefined
    | InvalidUserTypeSig SrcPos Scheme Scheme
    | CtorArityMismatch SrcPos Id Int Int
    | CtorArityMismatch SrcPos (Id Big) Int Int
    | ConflictingPatVarDefs SrcPos String
    | UndefCtor SrcPos String
    | UndefVar SrcPos String
    | InfType SrcPos Type Type TVar Type
    | UnificationFailed SrcPos Type Type Type Type
    | ConflictingTypeDef Id
    | ConflictingCtorDef Id
    | ConflictingTypeDef (Id Big)
    | ConflictingCtorDef (Id Big)
    | RedundantCase SrcPos
    | InexhaustivePats SrcPos String
    deriving Show


@@ 60,9 60,9 @@ prettyErr = \case
            $ ("Couldn't match type " ++ pretty t'2 ++ " with " ++ pretty t'1)
            ++ (".\nExpected type: " ++ pretty t1)
            ++ (".\nFound type: " ++ pretty t2 ++ ".")
    ConflictingTypeDef (WithPos p x) ->
    ConflictingTypeDef (Id (WithPos p x)) ->
        posd p big $ "Conflicting definitions for type `" ++ x ++ "`."
    ConflictingCtorDef (WithPos p x) ->
    ConflictingCtorDef (Id (WithPos p x)) ->
        posd p big $ "Conflicting definitions for constructor `" ++ x ++ "`."
    RedundantCase p -> posd p pat $ "Redundant case in pattern match."
    InexhaustivePats p patStr ->