~jojo/Carth

a75c1ebc2c72f53e4fccbd4e068aaf43727a0853 — JoJo 1 year, 10 months ago 26203a9
Allow pattern matching on uninhabited types, which returns Absurd

The following is now legal:

```
(type Bottom)

(define: bottom-elimination
    (forall (a) (Fun Bottom a))
  (fun-match))
```
M src/AnnotAst.hs => src/AnnotAst.hs +1 -0
@@ 88,6 88,7 @@ data Expr' m
    | Ctor VariantIx Span TConst [Type]
    | Box (Expr m)
    | Deref (Expr m)
    | Absurd Type
    deriving (Show)

type Expr m = WithPos (Expr' m)

M src/Check.hs => src/Check.hs +8 -7
@@ 183,6 183,7 @@ checkTypeVarsBound ds = runReaderT (boundInDefs ds) Set.empty
            forM_ ts (boundInType pos)
        An.Box x -> boundInExpr x
        An.Deref x -> boundInExpr x
        An.Absurd t -> boundInType pos t
    boundInType :: SrcPos -> An.Type -> Bound
    boundInType pos = \case
        TVar tv -> do


@@ 218,14 219,14 @@ checkPatternMatches tdefs = checkMsDefs
        An.Let lds b -> liftA2 An.Let (checkMsDefs lds) (checkMsExpr b)
        An.Match m cs tp tb -> do
            m' <- checkMsExpr m
            dt <- toDecisionTree' pos tp cs
            pure (An.Match m' dt tp tb)
        An.FunMatch cs tp tb -> fmap
            (\dt -> An.FunMatch dt tp tb)
            (toDecisionTree' pos tp cs)
            toDecisionTree' pos tp cs tb (An.Match m')
        An.FunMatch cs tp tb -> toDecisionTree' pos tp cs tb An.FunMatch
        An.Ctor v s tc ts -> pure (An.Ctor v s tc ts)
        An.Box x -> fmap An.Box (checkMsExpr x)
        An.Deref x -> fmap An.Deref (checkMsExpr x)
    toDecisionTree' pos tp (An.Cases cs) = do
        An.Absurd t -> pure (An.Absurd t)
    toDecisionTree' pos tp (An.Cases cs) tb f = do
        cs' <- mapM (secondM checkMsExpr) cs
        toDecisionTree tdefs pos tp cs'
        case runExceptT (toDecisionTree tdefs pos tp cs') of
            Nothing -> pure (An.Absurd tb)
            Just e -> fmap (\dt -> f dt tp tb) (liftEither e)

M src/Codegen.hs => src/Codegen.hs +1 -0
@@ 276,6 276,7 @@ genExpr expr = do
        Ction c -> genCtion c
        Box e -> genBox =<< genExpr e
        Deref e -> genDeref e
        Absurd t -> fmap (VLocal . undef) (genType t)

genConst :: MonoAst.Const -> Gen Val
genConst = \case

M src/Desugar.hs => src/Desugar.hs +3 -0
@@ 1,5 1,7 @@
{-# LANGUAGE LambdaCase #-}

-- TODO: Let's get rid of this module. It wasn't a good idea after all.

module Desugar (desugar) where

import Data.Bifunctor


@@ 41,6 43,7 @@ desugarExpr (WithPos _ e) = case e of
            params
    An.Box e -> Box (desugarExpr e)
    An.Deref e -> Deref (desugarExpr e)
    An.Absurd t -> Absurd t

desugarDecTree :: An.DecisionTree -> DecisionTree
desugarDecTree = \case

M src/DesugaredAst.hs => src/DesugaredAst.hs +1 -0
@@ 56,6 56,7 @@ data Expr
    | Ction VariantIx Span TConst [Expr]
    | Box Expr
    | Deref Expr
    | Absurd Type
    deriving (Show)

type Defs = Map String (Scheme, Expr)

M src/Match.hs => src/Match.hs +8 -7
@@ 52,7 52,7 @@ type RedundantCases = [SrcPos]
data Env = Env { _tdefs :: MTypeDefs, _tpat :: Type, _exprPos :: SrcPos }
makeLenses ''Env

type Match = ReaderT Env (StateT RedundantCases (Except TypeErr))
type Match = ReaderT Env (StateT RedundantCases (ExceptT TypeErr Maybe))


instance Eq Con where


@@ 67,7 67,7 @@ toDecisionTree
    -> SrcPos
    -> Type
    -> [(Pat, Expr)]
    -> Except TypeErr DecisionTree
    -> ExceptT TypeErr Maybe DecisionTree
toDecisionTree tds ePos tp cases =
    let
        rules = map (\(WithPos pos p, e) -> (p, (pos, Map.empty, e))) cases


@@ 93,17 93,18 @@ disjunct descr = \case

missingPat :: Type -> Descr -> Match String
missingPat t descr = case t of
    TVar _ -> pure "_"
    TPrim _ -> pure "_"
    TVar _ -> underscore
    TPrim _ -> underscore
    TConst (tx, _) -> do
        vs <- views tdefs (fromJust . Map.lookup tx)
        missingPat' vs descr
    TFun _ _ -> pure "_"
    TBox _ -> pure "_"
    TFun _ _ -> underscore
    TBox _ -> underscore
    where underscore = pure ("_ (" ++ pretty t ++ ")")

missingPat' :: [String] -> Descr -> Match String
missingPat' vs = \case
    Neg cs -> pure $ head $ Map.elems
    Neg cs -> lift $ lift $ lift $ listToMaybe $ Map.elems
        (Map.withoutKeys (allVariants vs) (Set.map variant cs))
    Pos con dargs ->
        let

M src/Mono.hs => src/Mono.hs +2 -1
@@ 1,6 1,6 @@
{-# LANGUAGE TemplateHaskell, LambdaCase, TupleSections
           , TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses
           , FlexibleContexts#-}
           , FlexibleContexts #-}

-- | Monomorphization
module Mono (monomorphize) where


@@ 69,6 69,7 @@ mono = \case
    An.Ction v span' inst as -> monoCtion v span' inst as
    An.Box x -> fmap Box (mono x)
    An.Deref x -> fmap Deref (mono x)
    An.Absurd t -> fmap Absurd (monotype t)

monoFun :: (String, An.Type) -> (An.Expr, An.Type) -> Mono Expr
monoFun (p, tp) (b, bt) = do

M src/MonoAst.hs => src/MonoAst.hs +2 -0
@@ 75,6 75,7 @@ data Expr
    | Ction Ction
    | Box Expr
    | Deref Expr
    | Absurd Type
    deriving (Show)

type Defs = Map TypedVar ([Type], Expr)


@@ 101,6 102,7 @@ fvExpr = \case
    Ction (_, _, _, as) -> Set.unions (map fvExpr as)
    Box e -> fvExpr e
    Deref e -> fvExpr e
    Absurd _ -> Set.empty

fvDecisionTree :: DecisionTree -> Set TypedVar
fvDecisionTree = \case

M src/Subst.hs => src/Subst.hs +1 -0
@@ 37,6 37,7 @@ substExpr s (WithPos p e) = WithPos p $ case e of
        Ctor i span' (tx, map (subst s) tts) (map (subst s) ps)
    Box e -> Box (substExpr s e)
    Deref e -> Deref (substExpr s e)
    Absurd t -> Absurd (subst s t)

substCases :: Subst -> Cases -> Cases
substCases s (Cases cs) = Cases (map (bimap (substPat s) (substExpr s)) cs)