From 9cd2cdb511fa0456a0f55cca08f6739617bb05b1 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Mon, 20 Mar 2023 17:40:09 +0100 Subject: [PATCH] continued work on pattern matching v2 --- Session.vim | 219 +++++++++++++++++++++++++++++++++ src/TypeChecker/TypeChecker.hs | 109 ++++++++-------- test_program | 11 +- 3 files changed, 279 insertions(+), 60 deletions(-) create mode 100644 Session.vim diff --git a/Session.vim b/Session.vim new file mode 100644 index 0000000..1db0ec6 --- /dev/null +++ b/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(":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(":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 : diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs index 779867b..ec7b005 100644 --- a/src/TypeChecker/TypeChecker.hs +++ b/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) -> - return (nullSubst, TMono "Int", T.ELit (TMono "Int") (LInt n)) - ELit a -> error $ "NOT IMPLEMENTED YET: ELit " ++ show a + ELit lit -> + let lt = litType lit + 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 - (injs', ts) <- mapAndUnzipM (checkInj t0) injs - case ts of - [] -> throwError "Case expression missing any matches" - 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') + (sub, _, e') <- algoW caseExpr + trace ("SUB: " ++ show sub) return () + t <- checkCase caseExpr injs + return (sub, t, T.ECase t e' (map (\(Inj i _) -> T.Inj (i, t) e') 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 -checkInj :: Type -> Inj -> Infer (T.Inj, Type) -checkInj caseType (Inj it expr) = do - (args, t') <- initType caseType it - subst <- unify caseType t' - applySt subst $ do - (_, t, e') <- local (\st -> st{vars = args `M.union` vars st}) (algoW expr) - return (T.Inj (it, t') e', t) +unifyAll :: [Type] -> Infer [Subst] +unifyAll [] = return [] +unifyAll [_] = return [] +unifyAll (x : y : xs) = do + uni <- unify x y + all <- unifyAll (y : xs) + return $ uni : all -initType :: Type -> Init -> Infer (Map Ident Poly, Type) -initType expected = \case - InitLit lit -> error "Pattern match on literals not implemented yet" - InitConstr c args -> do - st <- gets constructors - case M.lookup c st of - Nothing -> - throwError $ - unwords - [ "Constructor:" - , printTree c - , "does not exist" - ] - Just t -> do - let flat = flattenType t - let returnType = last flat - case ( length (init flat) == length args - , returnType `isMoreSpecificOrEq` expected - ) of - (True, True) -> - return - ( M.fromList $ zip args (map (Forall []) flat) - , expected - ) - (False, _) -> - throwError $ - "Can't partially match on the constructor: " - ++ printTree c - (_, False) -> - throwError $ - unwords - [ "Inferred type" - , printTree returnType - , "does not match expected type:" - , printTree expected - ] - InitCatch -> return (mempty, expected) +checkCase :: Exp -> [Inj] -> Infer Type +checkCase e injs = do + expT <- fst <$> inferExp e + (injTs, returns) <- mapAndUnzipM checkInj injs + unifyAll (expT : injTs) + subst <- foldl1 compose <$> zipWithM unify returns (tail returns) + let substed = map (apply subst) returns + unless (allSame substed || null substed) (throwError "Different return types of case, or no cases") + return $ head substed + +{- | fst = type of init +| snd = type of expr +-} +checkInj :: Inj -> Infer (Type, Type) +checkInj (Inj it expr) = do + initT <- inferInit it + (exprT, _) <- inferExp expr + return (initT, exprT) + +inferInit :: Init -> Infer Type +inferInit = \case + InitLit lit -> return $ litType lit + InitConstr fn vars -> do + gets (M.lookup fn . constructors) >>= \case + Nothing -> throwError $ "Constructor: " ++ printTree fn ++ " does not exist" + Just a -> do + let ft = init $ flattenType a + case compare (length vars) (length ft) of + EQ -> return . last $ flattenType a + _ -> throwError "Partial pattern match not allowed" + InitCatch -> fresh flattenType :: Type -> [Type] flattenType (TArr a b) = flattenType a ++ flattenType b diff --git a/test_program b/test_program index 2470637..a8accca 100644 --- a/test_program +++ b/test_program @@ -1,2 +1,9 @@ -id : 'a -> 'a ; -id = \x. x ; +data Bool () where { + True : Bool () + False : Bool () +}; + +main : Bool () -> _Int ; +main x = case x of { + 1 => 0 +}