~jojo/Carth

b1a31147fdef08e7538812603bbfbd31605326dc — JoJo 1 year, 6 months ago 1637b22
Allow patterns in parameter of fun

Refutable patterns will raise an error in the type checker.

Added bonus is that `fun` is now equivalent to a sugared, special case
of `fun-match`, and is desugared as such in Infer.
4 files changed, 30 insertions(+), 37 deletions(-)

M examples/std.carth
M src/Ast.hs
M src/Infer.hs
M src/Parse.hs
M examples/std.carth => examples/std.carth +4 -6
@@ 1,7 1,5 @@
(define fst
  (fun-match (case (Pair a _) a)))
(define snd
  (fun-match (case (Pair _ b) b)))
(define (fst (Pair a _)) a)
(define (snd (Pair _ b)) b)

(define: (undefined x)
    (forall (a) (Fun Unit a))


@@ 82,8 80,8 @@
(type (Iter a)
  (Iter (Lazy (Maybe (Pair a (Iter a))))))

(define next
  (fun-match (case (Iter it) (lively it))))
(define (next (Iter it)) (lively it))
(define (next! (Iter it)) (unwrap! (lively it)))

(define (range a b)
  (Iter (Lazy (if (> a b)

M src/Ast.hs => src/Ast.hs +13 -11
@@ 102,7 102,7 @@ data Expr'
    | Var (Id 'Small)
    | App Expr Expr
    | If Expr Expr Expr
    | Fun (Id 'Small) Expr
    | Fun Pat Expr
    | Let (NonEmpty Def) Expr
    | TypeAscr Expr Type
    | Match Expr (NonEmpty (Pat, Expr))


@@ 184,7 184,7 @@ fvExpr = unpos >>> \case
    Var x -> Set.singleton x
    App f a -> fvApp f a
    If p c a -> fvIf p c a
    Fun p b -> fvFun p b
    Fun p b -> fvFun' p b
    Let bs e ->
        fvLet (Set.fromList (fromList1 (map1 fst bs)), map1 (snd . snd) bs) e
    TypeAscr e _ -> freeVars e


@@ 194,6 194,9 @@ fvExpr = unpos >>> \case
    Box e -> fvExpr e
    Deref e -> fvExpr e

fvFun' :: Pat -> Expr -> Set (Id 'Small)
fvFun' p e = Set.difference (freeVars e) (bvPat p)

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



@@ 258,15 261,14 @@ prettyExpr' d = \case
        , indent (d + 4) ++ pretty' (d + 4) cons ++ "\n"
        , indent (d + 2) ++ pretty' (d + 2) alt ++ ")"
        ]
    Fun param body ->
        concat
            [ "(fun "
            , idstr param
            , "\n"
            , indent (d + 2)
            , pretty' (d + 2) body
            , ")"
            ]
    Fun param body -> concat
        [ "(fun ("
        , prettyPat param
        , ")\n"
        , indent (d + 2)
        , pretty' (d + 2) body
        , ")"
        ]
    Let binds body -> concat
        [ "(let ["
        , intercalate1 ("\n" ++ indent (d + 6)) (map1 (prettyDef (d + 6)) binds)

M src/Infer.hs => src/Infer.hs +10 -14
@@ 3,8 3,7 @@
module Infer (inferTopDefs) where

import Prelude hiding (span)
import Control.Lens
    ((<<+=), assign, makeLenses, over, use, view, views, locally, mapped)
import Control.Lens ((<<+=), assign, makeLenses, over, use, view, views, mapped)
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State.Strict


@@ 175,10 174,7 @@ infer (WithPos pos e) = fmap (second (WithPos pos)) $ case e of
        unify (Expected (TPrim TBool)) (Found (getPos p) tp)
        unify (Expected tc) (Found (getPos a) ta)
        pure (tc, If p' c' a')
    Ast.Fun p b -> do
        tp <- fresh
        (tb, b') <- withLocal (idstr p, Forall Set.empty tp) (infer b)
        pure (TFun tp tb, Fun (idstr p, tp) (b', tb))
    Ast.Fun p b -> inferFunMatch pos (pure (p, b))
    Ast.Let defs b -> do
        annotDefs <- inferDefs (fromList1 defs)
        let defsScms = fmap (\(scm, _) -> scm) annotDefs


@@ 193,11 189,7 @@ infer (WithPos pos e) = fmap (second (WithPos pos)) $ case e of
        (tbody, cases') <- inferCases (Expected tmatchee) cases
        dt <- toDecisionTree' pos tmatchee cases'
        pure (tbody, Match matchee' dt tbody)
    Ast.FunMatch cases -> do
        tpat <- fresh
        (tbody, cases') <- inferCases (Expected tpat) cases
        dt <- toDecisionTree' pos tpat cases'
        pure (TFun tpat tbody, FunMatch dt tpat tbody)
    Ast.FunMatch cases -> inferFunMatch pos cases
    Ast.Ctor c -> inferExprConstructor c
    Ast.Box x -> fmap (\(tx, x') -> (TBox tx, Box x')) (infer x)
    Ast.Deref x -> do


@@ 218,6 210,13 @@ toDecisionTree' pos tpat cases = do
    mTypeDefs <- views envTypeDefs (fmap (map fst . snd))
    lift (lift (toDecisionTree mTypeDefs pos tpat' cases'))

inferFunMatch :: SrcPos -> NonEmpty (Ast.Pat, Ast.Expr) -> Infer (Type, Expr')
inferFunMatch pos cases = do
    tpat <- fresh
    (tbody, cases') <- inferCases (Expected tpat) cases
    dt <- toDecisionTree' pos tpat cases'
    pure (TFun tpat tbody, FunMatch dt tpat tbody)

-- | All the patterns must be of the same types, and all the bodies must be of
--   the same type.
inferCases


@@ 330,9 329,6 @@ withLocals = withLocals' . Map.fromList
withLocals' :: Map String Scheme -> Infer a -> Infer a
withLocals' = augment envDefs

withLocal :: (String, Scheme) -> Infer a -> Infer a
withLocal b = locally envDefs (uncurry Map.insert b)

unify :: ExpectedType -> FoundType -> Infer ()
unify (Expected t1) (Found pos t2) = do
    s1 <- use substs

M src/Parse.hs => src/Parse.hs +3 -6
@@ 158,7 158,7 @@ def' schemeParser topPos = varDef <|> funDef
        body <- expr
        pure (name, (scm, body))
    funDef = do
        (name, params) <- parens (liftM2 (,) small' (some small'))
        (name, params) <- parens (liftM2 (,) small' (some pat))
        scm <- schemeParser
        body <- expr
        let f = foldr (WithPos topPos .* Fun) body params


@@ 250,12 250,9 @@ if' = do
fun :: Parser Expr'
fun = do
    reserved "fun"
    params <- choice
        [parens (some (withPos small')), fmap (\x -> [x]) (withPos small')]
    params <- choice [parens (some pat), fmap (pure . PVar) small']
    body <- expr
    pure $ unpos
        (foldr (\(WithPos pos p) b -> WithPos pos (Fun p b)) body params)

    pure $ unpos (foldr (\p b -> WithPos (getPos p) (Fun p b)) body params)

let' :: Parser Expr'
let' = do