continued work on pattern matching v2

Session.vim

@@ -0,0 +1,219 @@
+let SessionLoad = 1
+let s:so_save = &g:so | let s:siso_save = &g:siso | setg so=0 siso=0 | setl so=-1 siso=-1
+let v:this_session=expand("<sfile>:p")
+silent only
+silent tabonly
+cd ~/Documents/bachelor_thesis/language
+if expand('%') == '' && !&modified && line('$') <= 1 && getline(1) == ''
+  let s:wipebuf = bufnr('%')
+endif
+let s:shortmess_save = &shortmess
+if &shortmess =~ 'A'
+  set shortmess=aoOA
+else
+  set shortmess=aoO
+endif
+badd +1 ~/Documents/bachelor_thesis/language
+badd +298 src/TypeChecker/TypeChecker.hs
+badd +7 test_program
+badd +46 src/TypeChecker/TypeCheckerIr.hs
+badd +6 Grammar.cf
+badd +1 src/Grammar/Abs.hs
+argglobal
+%argdel
+$argadd ~/Documents/bachelor_thesis/language
+set stal=2
+tabnew +setlocal\ bufhidden=wipe
+tabnew +setlocal\ bufhidden=wipe
+tabnew +setlocal\ bufhidden=wipe
+tabrewind
+edit src/TypeChecker/TypeChecker.hs
+let s:save_splitbelow = &splitbelow
+let s:save_splitright = &splitright
+set splitbelow splitright
+wincmd _ | wincmd |
+vsplit
+1wincmd h
+wincmd w
+let &splitbelow = s:save_splitbelow
+let &splitright = s:save_splitright
+wincmd t
+let s:save_winminheight = &winminheight
+let s:save_winminwidth = &winminwidth
+set winminheight=0
+set winheight=1
+set winminwidth=0
+set winwidth=1
+exe 'vert 1resize ' . ((&columns * 99 + 86) / 173)
+exe 'vert 2resize ' . ((&columns * 73 + 86) / 173)
+argglobal
+setlocal fdm=manual
+setlocal fde=0
+setlocal fmr={{{,}}}
+setlocal fdi=#
+setlocal fdl=0
+setlocal fml=1
+setlocal fdn=20
+setlocal fen
+silent! normal! zE
+let &fdl = &fdl
+let s:l = 298 - ((18 * winheight(0) + 21) / 42)
+if s:l < 1 | let s:l = 1 | endif
+keepjumps exe s:l
+normal! zt
+keepjumps 298
+normal! 029|
+lcd ~/Documents/bachelor_thesis/language
+wincmd w
+argglobal
+if bufexists(fnamemodify("~/Documents/bachelor_thesis/language/Grammar.cf", ":p")) | buffer ~/Documents/bachelor_thesis/language/Grammar.cf | else | edit ~/Documents/bachelor_thesis/language/Grammar.cf | endif
+if &buftype ==# 'terminal'
+  silent file ~/Documents/bachelor_thesis/language/Grammar.cf
+endif
+balt ~/Documents/bachelor_thesis/language/src/TypeChecker/TypeChecker.hs
+setlocal fdm=manual
+setlocal fde=0
+setlocal fmr={{{,}}}
+setlocal fdi=#
+setlocal fdl=0
+setlocal fml=1
+setlocal fdn=20
+setlocal fen
+silent! normal! zE
+let &fdl = &fdl
+let s:l = 7 - ((6 * winheight(0) + 21) / 42)
+if s:l < 1 | let s:l = 1 | endif
+keepjumps exe s:l
+normal! zt
+keepjumps 7
+normal! 0
+lcd ~/Documents/bachelor_thesis/language
+wincmd w
+exe 'vert 1resize ' . ((&columns * 99 + 86) / 173)
+exe 'vert 2resize ' . ((&columns * 73 + 86) / 173)
+tabnext
+edit ~/Documents/bachelor_thesis/language/src/TypeChecker/TypeCheckerIr.hs
+let s:save_splitbelow = &splitbelow
+let s:save_splitright = &splitright
+set splitbelow splitright
+wincmd _ | wincmd |
+vsplit
+1wincmd h
+wincmd w
+let &splitbelow = s:save_splitbelow
+let &splitright = s:save_splitright
+wincmd t
+let s:save_winminheight = &winminheight
+let s:save_winminwidth = &winminwidth
+set winminheight=0
+set winheight=1
+set winminwidth=0
+set winwidth=1
+exe 'vert 1resize ' . ((&columns * 86 + 86) / 173)
+exe 'vert 2resize ' . ((&columns * 86 + 86) / 173)
+argglobal
+balt ~/Documents/bachelor_thesis/language/test_program
+setlocal fdm=manual
+setlocal fde=0
+setlocal fmr={{{,}}}
+setlocal fdi=#
+setlocal fdl=0
+setlocal fml=1
+setlocal fdn=20
+setlocal fen
+silent! normal! zE
+let &fdl = &fdl
+let s:l = 1 - ((0 * winheight(0) + 21) / 42)
+if s:l < 1 | let s:l = 1 | endif
+keepjumps exe s:l
+normal! zt
+keepjumps 1
+normal! 0
+lcd ~/Documents/bachelor_thesis/language
+wincmd w
+argglobal
+if bufexists(fnamemodify("~/Documents/bachelor_thesis/language/src/Grammar/Abs.hs", ":p")) | buffer ~/Documents/bachelor_thesis/language/src/Grammar/Abs.hs | else | edit ~/Documents/bachelor_thesis/language/src/Grammar/Abs.hs | endif
+if &buftype ==# 'terminal'
+  silent file ~/Documents/bachelor_thesis/language/src/Grammar/Abs.hs
+endif
+balt ~/Documents/bachelor_thesis/language/src/TypeChecker/TypeCheckerIr.hs
+setlocal fdm=manual
+setlocal fde=0
+setlocal fmr={{{,}}}
+setlocal fdi=#
+setlocal fdl=0
+setlocal fml=1
+setlocal fdn=20
+setlocal fen
+silent! normal! zE
+let &fdl = &fdl
+let s:l = 1 - ((0 * winheight(0) + 21) / 42)
+if s:l < 1 | let s:l = 1 | endif
+keepjumps exe s:l
+normal! zt
+keepjumps 1
+normal! 0
+lcd ~/Documents/bachelor_thesis/language
+wincmd w
+exe 'vert 1resize ' . ((&columns * 86 + 86) / 173)
+exe 'vert 2resize ' . ((&columns * 86 + 86) / 173)
+tabnext
+edit ~/Documents/bachelor_thesis/language/Grammar.cf
+argglobal
+balt ~/Documents/bachelor_thesis/language/src/Grammar/Abs.hs
+setlocal fdm=manual
+setlocal fde=0
+setlocal fmr={{{,}}}
+setlocal fdi=#
+setlocal fdl=0
+setlocal fml=1
+setlocal fdn=20
+setlocal fen
+silent! normal! zE
+let &fdl = &fdl
+let s:l = 40 - ((12 * winheight(0) + 21) / 42)
+if s:l < 1 | let s:l = 1 | endif
+keepjumps exe s:l
+normal! zt
+keepjumps 40
+normal! 0
+lcd ~/Documents/bachelor_thesis/language
+tabnext
+edit ~/Documents/bachelor_thesis/language/test_program
+argglobal
+balt ~/Documents/bachelor_thesis/language/src/TypeChecker/TypeChecker.hs
+setlocal fdm=manual
+setlocal fde=0
+setlocal fmr={{{,}}}
+setlocal fdi=#
+setlocal fdl=0
+setlocal fml=1
+setlocal fdn=20
+setlocal fen
+silent! normal! zE
+let &fdl = &fdl
+let s:l = 7 - ((6 * winheight(0) + 21) / 42)
+if s:l < 1 | let s:l = 1 | endif
+keepjumps exe s:l
+normal! zt
+keepjumps 7
+normal! 010|
+lcd ~/Documents/bachelor_thesis/language
+tabnext 1
+set stal=1
+if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal'
+  silent exe 'bwipe ' . s:wipebuf
+endif
+unlet! s:wipebuf
+set winheight=1 winwidth=20
+let &shortmess = s:shortmess_save
+let s:sx = expand("<sfile>:p:r")."x.vim"
+if filereadable(s:sx)
+  exe "source " . fnameescape(s:sx)
+endif
+let &g:so = s:so_save | let &g:siso = s:siso_save
+set hlsearch
+nohlsearch
+doautoall SessionLoadPost
+unlet SessionLoad
+" vim: set ft=vim :

src/TypeChecker/TypeChecker.hs

@@ -8,13 +8,16 @@ import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
 import Data.Foldable (traverse_)
+import Data.Function (on)
 import Data.Functor.Identity (runIdentity)
 import Data.List (foldl')
+import Data.List.Extra (allSame)
 import Data.Map (Map)
 import Data.Map qualified as M
 import Data.Maybe (fromMaybe)
 import Data.Set (Set)
 import Data.Set qualified as S
+import Data.Tree (flatten)
 import Debug.Trace (trace)
 import Grammar.Abs
 import Grammar.Print (printTree)
@@ -204,9 +207,9 @@ algoW = \case
     -- \| ------------------
     -- \|   Γ ⊢ i : Int, ∅
 
-    ELit (LInt n) ->
+    ELit lit ->
-        return (nullSubst, TMono "Int", T.ELit (TMono "Int") (LInt n))
+        let lt = litType lit
-    ELit a -> error $ "NOT IMPLEMENTED YET: ELit " ++ show a
+         in return (nullSubst, lt, T.ELit lt lit)
     -- \| x : σ ∈ Γ   τ = inst(σ)
     -- \| ----------------------
     -- \|     Γ ⊢ x : τ, ∅
@@ -289,16 +292,14 @@ algoW = \case
             (s2, t2, e1') <- algoW e1
             let composition = s2 `compose` s1
             return (composition, t2, apply composition $ T.ELet (T.Bind (name, t2) e0') e1')
+
+    -- TODO: give caseExpr a concrete type before proceeding
+    -- probably by returning substitutions in the functions used in this body
     ECase caseExpr injs -> do
-        (_, t0, e0') <- algoW caseExpr
+        (sub, _, e') <- algoW caseExpr
-        (injs', ts) <- mapAndUnzipM (checkInj t0) injs
+        trace ("SUB: " ++ show sub) return ()
-        case ts of
+        t <- checkCase caseExpr injs
-            [] -> throwError "Case expression missing any matches"
+        return (sub, t, T.ECase t e' (map (\(Inj i _) -> T.Inj (i, t) e') injs))
-            ts -> do
-                unified <- zipWithM unify ts (tail ts)
-                let composition = foldl' compose mempty unified
-                let typ = apply composition (head ts)
-                return (composition, typ, apply composition $ T.ECase typ e0' injs')
 
 -- | Unify two types producing a new substitution
 unify :: Type -> Type -> Infer Subst
@@ -312,7 +313,6 @@ unify t0 t1 = do
         (a, TPol b) -> occurs b a
         (TMono a, TMono b) ->
             if a == b then return M.empty else throwError "Types do not unify"
-        -- \| TODO: Figure out a cleaner way to express the same thing
         (TConstr (Constr name t), TConstr (Constr name' t')) ->
             if name == name' && length t == length t'
                 then do
@@ -464,52 +464,45 @@ insertConstr i t =
 
 -------- PATTERN MATCHING ---------
 
--- "case expr of", the type of 'expr' is caseType
+unifyAll :: [Type] -> Infer [Subst]
-checkInj :: Type -> Inj -> Infer (T.Inj, Type)
+unifyAll [] = return []
-checkInj caseType (Inj it expr) = do
+unifyAll [_] = return []
-    (args, t') <- initType caseType it
+unifyAll (x : y : xs) = do
-    subst <- unify caseType t'
+    uni <- unify x y
-    applySt subst $ do
+    all <- unifyAll (y : xs)
-        (_, t, e') <- local (\st -> st{vars = args `M.union` vars st}) (algoW expr)
+    return $ uni : all
-        return (T.Inj (it, t') e', t)
 
-initType :: Type -> Init -> Infer (Map Ident Poly, Type)
+checkCase :: Exp -> [Inj] -> Infer Type
-initType expected = \case
+checkCase e injs = do
-    InitLit lit -> error "Pattern match on literals not implemented yet"
+    expT <- fst <$> inferExp e
-    InitConstr c args -> do
+    (injTs, returns) <- mapAndUnzipM checkInj injs
-        st <- gets constructors
+    unifyAll (expT : injTs)
-        case M.lookup c st of
+    subst <- foldl1 compose <$> zipWithM unify returns (tail returns)
-            Nothing ->
+    let substed = map (apply subst) returns
-                throwError $
+    unless (allSame substed || null substed) (throwError "Different return types of case, or no cases")
-                    unwords
+    return $ head substed
-                        [ "Constructor:"
+
-                        , printTree c
+{- | fst = type of init
-                        , "does not exist"
+| snd = type of expr
-                        ]
+-}
-            Just t -> do
+checkInj :: Inj -> Infer (Type, Type)
-                let flat = flattenType t
+checkInj (Inj it expr) = do
-                let returnType = last flat
+    initT <- inferInit it
-                case ( length (init flat) == length args
+    (exprT, _) <- inferExp expr
-                     , returnType `isMoreSpecificOrEq` expected
+    return (initT, exprT)
-                     ) of
+
-                    (True, True) ->
+inferInit :: Init -> Infer Type
-                        return
+inferInit = \case
-                            ( M.fromList $ zip args (map (Forall []) flat)
+    InitLit lit -> return $ litType lit
-                            , expected
+    InitConstr fn vars -> do
-                            )
+        gets (M.lookup fn . constructors) >>= \case
-                    (False, _) ->
+            Nothing -> throwError $ "Constructor: " ++ printTree fn ++ " does not exist"
-                        throwError $
+            Just a -> do
-                            "Can't partially match on the constructor: "
+                let ft = init $ flattenType a
-                                ++ printTree c
+                case compare (length vars) (length ft) of
-                    (_, False) ->
+                    EQ -> return . last $ flattenType a
-                        throwError $
+                    _ -> throwError "Partial pattern match not allowed"
-                            unwords
+    InitCatch -> fresh
-                                [ "Inferred type"
-                                , printTree returnType
-                                , "does not match expected type:"
-                                , printTree expected
-                                ]
-    InitCatch -> return (mempty, expected)
 
 flattenType :: Type -> [Type]
 flattenType (TArr a b) = flattenType a ++ flattenType b

test_program

@@ -1,2 +1,9 @@
-id : 'a -> 'a ;
+data Bool () where {
-id = \x. x ;
+    True : Bool ()
+    False : Bool ()
+};
+
+main : Bool () -> _Int ;
+main x = case x of {
+    1 => 0
+}