From 4662d81b4624ec3bcdba82d22e1cee29122b1b39 Mon Sep 17 00:00:00 2001 From: Diana Tomilovskaia <84839431+frog-da@users.noreply.github.com> Date: Mon, 2 Sep 2024 22:33:25 +0300 Subject: [PATCH] implement lambda abstraction and application (#3) Co-authored-by: evermake --- grammar/hindley-milner.cf | 3 + src/HM/Eval.hs | 43 +- src/HM/Parser/Abs.hs | 4 +- src/HM/Parser/Doc.txt | 7 +- src/HM/Parser/Lex.hs | 777 ++++++++++++++++++++++-------------- src/HM/Parser/Lex.x | 14 +- src/HM/Parser/Par.hs | 610 ++++++++++++++++++---------- src/HM/Parser/Par.y | 33 +- src/HM/Parser/Print.hs | 3 + src/HM/Parser/Skel.hs | 3 + src/HM/Syntax.hs | 52 +-- src/HM/Typecheck.hs | 50 ++- test/files/ill-typed/7.lam | 1 + test/files/ill-typed/8.lam | 1 + test/files/ill-typed/9.lam | 1 + test/files/well-typed/7.lam | 1 + test/files/well-typed/8.lam | 1 + test/files/well-typed/9.lam | 1 + 18 files changed, 1005 insertions(+), 600 deletions(-) create mode 100644 test/files/ill-typed/7.lam create mode 100644 test/files/ill-typed/8.lam create mode 100644 test/files/ill-typed/9.lam create mode 100644 test/files/well-typed/7.lam create mode 100644 test/files/well-typed/8.lam create mode 100644 test/files/well-typed/9.lam diff --git a/grammar/hindley-milner.cf b/grammar/hindley-milner.cf index fbfe541..7ba4204 100644 --- a/grammar/hindley-milner.cf +++ b/grammar/hindley-milner.cf @@ -10,6 +10,8 @@ EIf. Exp1 ::= "if" Exp1 "then" Exp1 "else" Exp1 ; EIsZero. Exp2 ::= "iszero" "(" Exp ")" ; ETyped. Exp ::= Exp1 ":" Type ; ELet. Exp1 ::= "let" Pattern "=" Exp1 "in" ScopedExp ; +EAbs. Exp1 ::= "λ" Pattern ":" Type "." ScopedExp ; +EApp. Exp1 ::= Exp1 Exp2 ; ScopedExp. ScopedExp ::= Exp1 ; @@ -18,3 +20,4 @@ coercions Exp 3 ; TNat. Type ::= "Nat" ; TBool. Type ::= "Bool" ; +TArrow. Type ::= Type "->" Type ; diff --git a/src/HM/Eval.hs b/src/HM/Eval.hs index 3923e3f..61409de 100644 --- a/src/HM/Eval.hs +++ b/src/HM/Eval.hs @@ -1,10 +1,15 @@ {-# LANGUAGE LambdaCase #-} + module HM.Eval where -import Control.Monad.Foil (Distinct, Scope, addSubst, - identitySubst) -import Control.Monad.Free.Foil (AST (Var), substitute) -import HM.Syntax +import Control.Monad.Foil + ( Distinct, + Scope, + addSubst, + identitySubst, + ) +import Control.Monad.Free.Foil (AST (Var), substitute) +import HM.Syntax -- $setup -- >>> :set -XOverloadedStrings @@ -14,7 +19,7 @@ import HM.Syntax -- Right "true" -- >>> eval emptyScope "if (iszero (2 - (true + 1))) then true else 0" -- Left "Unsupported expression in addition" -eval :: Distinct n => Scope n -> Exp n -> Either String (Exp n) +eval :: (Distinct n) => Scope n -> Exp n -> Either String (Exp n) eval _scope (Var x) = Right (Var x) eval _scope ETrue = Right ETrue eval _scope EFalse = Right EFalse @@ -24,26 +29,36 @@ eval scope (EAdd l r) = do r' <- eval scope r case (l', r') of (ENat x, ENat y) -> Right (ENat (x + y)) - _ -> Left "Unsupported expression in addition" + _ -> Left "Unsupported expression in addition" eval scope (ESub l r) = do l' <- eval scope l r' <- eval scope r case (l', r') of (ENat x, ENat y) -> Right (ENat (x - y)) - _ -> Left "Unsupported expression in subtraction" + _ -> Left "Unsupported expression in subtraction" eval scope (EIf cond then_ else_) = do cond' <- eval scope cond case cond' of - ETrue -> eval scope then_ + ETrue -> eval scope then_ EFalse -> eval scope else_ - _ -> Left "Unsupported condition in if statement" -eval scope (EIsZero n) = eval scope n >>= \case - ENat n' - | n' == 0 -> Right ETrue - | otherwise -> Right EFalse - _ -> Left "Unsupported expression in iszero" + _ -> Left "Unsupported condition in if statement" +eval scope (EIsZero n) = + eval scope n >>= \case + ENat n' + | n' == 0 -> Right ETrue + | otherwise -> Right EFalse + _ -> Left "Unsupported expression in iszero" eval scope (ETyped e _) = eval scope e eval scope (ELet e1 x e2) = do e1' <- eval scope e1 let subst = addSubst identitySubst x e1' eval scope (substitute scope subst e2) +eval _scope (EAbs type_ x e) = Right (EAbs type_ x e) +eval scope (EApp e1 e2) = do + e1' <- eval scope e1 + e2' <- eval scope e2 + case e1' of + EAbs _ x e -> do + let subst = addSubst identitySubst x e2' + eval scope (substitute scope subst e) + _ -> Left "Unsupported expression in application" diff --git a/src/HM/Parser/Abs.hs b/src/HM/Parser/Abs.hs index 844d965..dcff1da 100644 --- a/src/HM/Parser/Abs.hs +++ b/src/HM/Parser/Abs.hs @@ -29,12 +29,14 @@ data Exp | EIsZero Exp | ETyped Exp Type | ELet Pattern Exp ScopedExp + | EAbs Pattern Type ScopedExp + | EApp Exp Exp deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) data ScopedExp = ScopedExp Exp deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) -data Type = TNat | TBool +data Type = TNat | TBool | TArrow Type Type deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) newtype Ident = Ident String diff --git a/src/HM/Parser/Doc.txt b/src/HM/Parser/Doc.txt index b0f2f3f..e14ac1a 100644 --- a/src/HM/Parser/Doc.txt +++ b/src/HM/Parser/Doc.txt @@ -27,11 +27,11 @@ The set of reserved words is the set of terminals appearing in the grammar. Thos The reserved words used in Parser are the following: | ``Bool`` | ``Nat`` | ``else`` | ``false`` | ``if`` | ``in`` | ``iszero`` | ``let`` - | ``then`` | ``true`` | | + | ``then`` | ``true`` | ``λ`` | The symbols used in Parser are the following: | + | - | ( | ) - | : | = | | + | : | = | . | -> ===Comments=== There are no single-line comments in the grammar.There are no multiple-line comments in the grammar. @@ -54,12 +54,15 @@ All other symbols are terminals. | | **|** | //Exp3// | //Exp1// | -> | ``if`` //Exp1// ``then`` //Exp1// ``else`` //Exp1// | | **|** | ``let`` //Pattern// ``=`` //Exp1// ``in`` //ScopedExp// + | | **|** | ``λ`` //Pattern// ``:`` //Type// ``.`` //ScopedExp// + | | **|** | //Exp1// //Exp2// | | **|** | //Exp2// | //Exp// | -> | //Exp1// ``:`` //Type// | | **|** | //Exp1// | //ScopedExp// | -> | //Exp1// | //Type// | -> | ``Nat`` | | **|** | ``Bool`` + | | **|** | //Type// ``->`` //Type// diff --git a/src/HM/Parser/Lex.hs b/src/HM/Parser/Lex.hs index e0a9405..27ac67c 100644 --- a/src/HM/Parser/Lex.hs +++ b/src/HM/Parser/Lex.hs @@ -22,23 +22,179 @@ import qualified Data.Array alex_tab_size :: Int alex_tab_size = 8 alex_base :: Data.Array.Array Int Int -alex_base = Data.Array.listArray (0 :: Int, 5) +alex_base = Data.Array.listArray (0 :: Int, 7) [ -8 + , 140 , -42 - , 91 + , -46 + , -13 + , 171 , 0 - , 7 - , 86 + , -170 ] alex_table :: Data.Array.Array Int Int -alex_table = Data.Array.listArray (0 :: Int, 346) +alex_table = Data.Array.listArray (0 :: Int, 426) [ 0 - , 4 - , 4 - , 4 - , 4 - , 4 + , 5 + , 5 + , 5 + , 5 + , 5 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 6 + , 6 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 5 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 6 + , 6 + , 0 + , 6 + , 0 + , 3 + , 6 + , 0 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 2 + , 6 + , 0 + , 0 + , 6 + , 0 + , 0 + , 0 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 0 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 , 1 , 1 , 1 @@ -49,30 +205,73 @@ alex_table = Data.Array.listArray (0 :: Int, 346) , 1 , 1 , 1 - , 4 - , 4 - , 4 - , 4 - , 4 , 0 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 5 + , 5 + , 5 + , 5 + , 5 , 0 , 0 , 4 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 7 , 0 , 0 , 0 , 0 + , 5 , 0 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 , 0 , 0 - , 3 - , 3 , 0 - , 3 , 0 - , 3 + , 1 , 0 - , 4 , 1 , 1 , 1 @@ -83,71 +282,33 @@ alex_table = Data.Array.listArray (0 :: Int, 346) , 1 , 1 , 1 - , 3 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 + , 1 , 0 , 0 - , 3 , 0 , 0 , 0 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 , 0 , 0 , 0 , 0 , 0 , 0 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 , 0 , 0 , 0 @@ -163,7 +324,6 @@ alex_table = Data.Array.listArray (0 :: Int, 346) , 0 , 0 , 0 - , 2 , 0 , 0 , 0 @@ -172,16 +332,6 @@ alex_table = Data.Array.listArray (0 :: Int, 346) , 0 , 0 , 0 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 , 0 , 0 , 0 @@ -189,128 +339,12 @@ alex_table = Data.Array.listArray (0 :: Int, 346) , 0 , 0 , 0 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 , 0 , 0 , 0 , 0 - , 2 - , 5 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 , 0 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 , 0 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 - , 2 , 0 , 0 , 0 @@ -319,7 +353,55 @@ alex_table = Data.Array.listArray (0 :: Int, 346) , 0 , 0 , 0 - , 5 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 4 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 + , 0 , 0 , 0 , 0 @@ -383,7 +465,7 @@ alex_table = Data.Array.listArray (0 :: Int, 346) ] alex_check :: Data.Array.Array Int Int -alex_check = Data.Array.listArray (0 :: Int, 346) +alex_check = Data.Array.listArray (0 :: Int, 426) [ -1 , 9 , 10 @@ -400,11 +482,11 @@ alex_check = Data.Array.listArray (0 :: Int, 346) , 55 , 56 , 57 - , 9 - , 10 - , 11 - , 12 - , 13 + , 62 + , 187 + , -1 + , -1 + , -1 , -1 , -1 , -1 @@ -422,8 +504,8 @@ alex_check = Data.Array.listArray (0 :: Int, 346) , 43 , -1 , 45 + , 46 , -1 - , 32 , 48 , 49 , 50 @@ -499,30 +581,79 @@ alex_check = Data.Array.listArray (0 :: Int, 346) , 120 , 121 , 122 + , 128 + , 129 + , 130 + , 131 + , 132 + , 133 + , 134 + , 135 + , 136 + , 137 + , 138 + , 139 + , 140 + , 141 + , 142 + , 143 + , 144 + , 145 + , 146 + , 147 + , 148 + , 149 + , 150 , -1 + , 152 + , 153 + , 154 + , 155 + , 156 + , 157 + , 158 + , 159 + , 160 + , 161 + , 162 + , 163 + , 164 + , 165 + , 166 + , 167 + , 168 + , 169 + , 170 + , 171 + , 172 + , 173 + , 174 + , 175 + , 176 + , 177 + , 178 + , 179 + , 180 + , 181 + , 182 , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 + , 184 + , 185 + , 186 + , 187 + , 188 + , 189 + , 190 + , 191 , 39 + , 9 + , 10 + , 11 + , 12 + , 13 , -1 , -1 - , -1 - , -1 - , -1 - , -1 - , -1 - , -1 + , 195 , 48 , 49 , 50 @@ -533,12 +664,12 @@ alex_check = Data.Array.listArray (0 :: Int, 346) , 55 , 56 , 57 + , 206 , -1 , -1 , -1 , -1 - , -1 - , -1 + , 32 , -1 , 65 , 66 @@ -571,7 +702,7 @@ alex_check = Data.Array.listArray (0 :: Int, 346) , -1 , -1 , 95 - , 195 + , -1 , 97 , 98 , 99 @@ -598,70 +729,70 @@ alex_check = Data.Array.listArray (0 :: Int, 346) , 120 , 121 , 122 - , 128 - , 129 - , 130 - , 131 - , 132 - , 133 - , 134 - , 135 - , 136 - , 137 - , 138 - , 139 - , 140 - , 141 - , 142 - , 143 - , 144 - , 145 - , 146 - , 147 - , 148 - , 149 - , 150 , -1 - , 152 - , 153 - , 154 - , 155 - , 156 - , 157 - , 158 - , 159 - , 160 - , 161 - , 162 - , 163 - , 164 - , 165 - , 166 - , 167 - , 168 - , 169 - , 170 - , 171 - , 172 - , 173 - , 174 - , 175 - , 176 - , 177 - , 178 - , 179 - , 180 - , 181 - , 182 , -1 - , 184 - , 185 - , 186 - , 187 - , 188 - , 189 - , 190 - , 191 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 , -1 , -1 , -1 @@ -731,30 +862,66 @@ alex_check = Data.Array.listArray (0 :: Int, 346) , -1 , -1 , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 + , -1 ] alex_deflt :: Data.Array.Array Int Int -alex_deflt = Data.Array.listArray (0 :: Int, 5) +alex_deflt = Data.Array.listArray (0 :: Int, 7) [ -1 , -1 , -1 , -1 , -1 , -1 + , -1 + , -1 ] -alex_accept = Data.Array.listArray (0 :: Int, 5) +alex_accept = Data.Array.listArray (0 :: Int, 7) [ AlexAccNone + , AlexAcc 3 , AlexAcc 2 , AlexAcc 1 - , AlexAcc 0 + , AlexAccNone , AlexAccSkip + , AlexAcc 0 , AlexAccNone ] -alex_actions = Data.Array.array (0 :: Int, 3) - [ (2,alex_action_3) - , (1,alex_action_2) +alex_actions = Data.Array.array (0 :: Int, 4) + [ (3,alex_action_2) + , (2,alex_action_3) + , (1,alex_action_1) , (0,alex_action_1) ] @@ -1095,13 +1262,13 @@ eitherResIdent tv s = treeFind resWords -- | The keywords and symbols of the language organized as binary search tree. resWords :: BTree resWords = - b "else" 9 - (b ":" 5 + b "Nat" 10 + (b "->" 5 (b "+" 3 (b ")" 2 (b "(" 1 N N) N) (b "-" 4 N N)) - (b "Bool" 7 (b "=" 6 N N) (b "Nat" 8 N N))) - (b "iszero" 13 - (b "if" 11 (b "false" 10 N N) (b "in" 12 N N)) - (b "then" 15 (b "let" 14 N N) (b "true" 16 N N))) + (b "=" 8 (b ":" 7 (b "." 6 N N) N) (b "Bool" 9 N N))) + (b "iszero" 15 + (b "if" 13 (b "false" 12 (b "else" 11 N N) N) (b "in" 14 N N)) + (b "true" 18 (b "then" 17 (b "let" 16 N N) N) (b "\955" 19 N N))) where b s n = B bs (TS bs n) where diff --git a/src/HM/Parser/Lex.x b/src/HM/Parser/Lex.x index 6d8c3be..885ea45 100644 --- a/src/HM/Parser/Lex.x +++ b/src/HM/Parser/Lex.x @@ -28,7 +28,7 @@ $u = [. \n] -- universal: any character -- Symbols and non-identifier-like reserved words -@rsyms = \+ | \- | \( | \) | \: | \= +@rsyms = \λ | \+ | \- | \( | \) | \: | \= | \. | \- \> :- @@ -148,13 +148,13 @@ eitherResIdent tv s = treeFind resWords -- | The keywords and symbols of the language organized as binary search tree. resWords :: BTree resWords = - b "else" 9 - (b ":" 5 + b "Nat" 10 + (b "->" 5 (b "+" 3 (b ")" 2 (b "(" 1 N N) N) (b "-" 4 N N)) - (b "Bool" 7 (b "=" 6 N N) (b "Nat" 8 N N))) - (b "iszero" 13 - (b "if" 11 (b "false" 10 N N) (b "in" 12 N N)) - (b "then" 15 (b "let" 14 N N) (b "true" 16 N N))) + (b "=" 8 (b ":" 7 (b "." 6 N N) N) (b "Bool" 9 N N))) + (b "iszero" 15 + (b "if" 13 (b "false" 12 (b "else" 11 N N) N) (b "in" 14 N N)) + (b "true" 18 (b "then" 17 (b "let" 16 N N) N) (b "\955" 19 N N))) where b s n = B bs (TS bs n) where diff --git a/src/HM/Parser/Par.hs b/src/HM/Parser/Par.hs index c574ef0..cc98246 100644 --- a/src/HM/Parser/Par.hs +++ b/src/HM/Parser/Par.hs @@ -102,7 +102,16 @@ action_0, action_49, action_50, action_51, - action_52 :: () => Prelude.Int -> ({-HappyReduction (Err) = -} + action_52, + action_53, + action_54, + action_55, + action_56, + action_57, + action_58, + action_59, + action_60, + action_61 :: () => Prelude.Int -> ({-HappyReduction (Err) = -} Prelude.Int -> (Token) -> HappyState (Token) (HappyStk HappyAbsSyn -> [(Token)] -> (Err) HappyAbsSyn) @@ -129,7 +138,10 @@ happyReduce_7, happyReduce_23, happyReduce_24, happyReduce_25, - happyReduce_26 :: () => ({-HappyReduction (Err) = -} + happyReduce_26, + happyReduce_27, + happyReduce_28, + happyReduce_29 :: () => ({-HappyReduction (Err) = -} Prelude.Int -> (Token) -> HappyState (Token) (HappyStk HappyAbsSyn -> [(Token)] -> (Err) HappyAbsSyn) @@ -138,88 +150,91 @@ happyReduce_7, -> [(Token)] -> (Err) HappyAbsSyn) happyExpList :: Happy_Data_Array.Array Prelude.Int Prelude.Int -happyExpList = Happy_Data_Array.listArray (0,134) ([0,0,4,128,449,4096,14624,0,27650,7,32832,237,2048,7600,0,192,0,0,32,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32768,1,0,0,0,0,0,4096,15200,0,0,0,32832,237,2048,0,0,0,1,0,0,0,0,0,8,0,0,0,0,0,0,3,0,0,0,0,0,0,0,0,2052,14,128,449,0,12,0,64,0,32832,237,0,512,0,2,0,0,0,1024,3800,0,1,0,24592,59,0,0,0,0,0,0,0,0,8,0,0,0,1024,0,128,475,4096,15200,0,0,0,0,0,0 +happyExpList = Happy_Data_Array.listArray (0,193) ([0,0,32,1024,26656,0,8196,105,1024,31584,0,24580,123,1024,31584,0,3072,0,0,8192,0,0,0,16384,0,0,0,0,0,0,0,0,0,0,0,0,0,0,12288,0,0,0,0,0,0,0,24580,123,0,0,0,24580,123,1024,0,0,0,32,0,0,0,0,32,0,0,0,8452,105,0,0,0,8196,105,12288,0,0,0,0,0,0,0,0,0,1024,26656,0,8196,104,12288,0,0,3072,0,0,1,0,512,0,1024,31584,0,8196,109,2048,0,0,3072,0,0,0,0,0,0,1024,31584,0,8,0,1024,31584,0,3072,0,16384,0,0,0,0,0,0,0,192,0,1024,27040,0,0,0,1024,26928,0,24580,123,1024,31584,0,24580,123,0,0,0,0,0,0,0,0 ]) {-# NOINLINE happyExpListPerState #-} happyExpListPerState st = token_strs_expected - where token_strs = ["error","%dummy","%start_pPattern","%start_pExp3","%start_pExp2","%start_pExp1","%start_pExp","%start_pScopedExp","%start_pType","Ident","Integer","Pattern","Exp3","Exp2","Exp1","Exp","ScopedExp","Type","'('","')'","'+'","'-'","':'","'='","'Bool'","'Nat'","'else'","'false'","'if'","'in'","'iszero'","'let'","'then'","'true'","L_Ident","L_integ","%eof"] - bit_start = st Prelude.* 37 - bit_end = (st Prelude.+ 1) Prelude.* 37 + where token_strs = ["error","%dummy","%start_pPattern","%start_pExp3","%start_pExp2","%start_pExp1","%start_pExp","%start_pScopedExp","%start_pType","Ident","Integer","Pattern","Exp3","Exp2","Exp1","Exp","ScopedExp","Type","'('","')'","'+'","'-'","'->'","'.'","':'","'='","'Bool'","'Nat'","'else'","'false'","'if'","'in'","'iszero'","'let'","'then'","'true'","'\955'","L_Ident","L_integ","%eof"] + bit_start = st Prelude.* 40 + bit_end = (st Prelude.+ 1) Prelude.* 40 read_bit = readArrayBit happyExpList bits = Prelude.map read_bit [bit_start..bit_end Prelude.- 1] - bits_indexed = Prelude.zip bits [0..36] + bits_indexed = Prelude.zip bits [0..39] token_strs_expected = Prelude.concatMap f bits_indexed f (Prelude.False, _) = [] f (Prelude.True, nr) = [token_strs Prelude.!! nr] -action_0 (35) = happyShift action_8 -action_0 (10) = happyGoto action_30 -action_0 (12) = happyGoto action_31 +action_0 (38) = happyShift action_8 +action_0 (10) = happyGoto action_31 +action_0 (12) = happyGoto action_32 action_0 _ = happyFail (happyExpListPerState 0) action_1 (19) = happyShift action_18 -action_1 (28) = happyShift action_19 -action_1 (34) = happyShift action_23 -action_1 (35) = happyShift action_8 -action_1 (36) = happyShift action_24 +action_1 (30) = happyShift action_19 +action_1 (36) = happyShift action_23 +action_1 (38) = happyShift action_8 +action_1 (39) = happyShift action_25 action_1 (10) = happyGoto action_12 action_1 (11) = happyGoto action_13 -action_1 (13) = happyGoto action_29 +action_1 (13) = happyGoto action_30 action_1 _ = happyFail (happyExpListPerState 1) action_2 (19) = happyShift action_18 -action_2 (28) = happyShift action_19 -action_2 (31) = happyShift action_21 -action_2 (34) = happyShift action_23 -action_2 (35) = happyShift action_8 -action_2 (36) = happyShift action_24 +action_2 (30) = happyShift action_19 +action_2 (33) = happyShift action_21 +action_2 (36) = happyShift action_23 +action_2 (38) = happyShift action_8 +action_2 (39) = happyShift action_25 action_2 (10) = happyGoto action_12 action_2 (11) = happyGoto action_13 action_2 (13) = happyGoto action_14 -action_2 (14) = happyGoto action_28 +action_2 (14) = happyGoto action_29 action_2 _ = happyFail (happyExpListPerState 2) action_3 (19) = happyShift action_18 -action_3 (28) = happyShift action_19 -action_3 (29) = happyShift action_20 -action_3 (31) = happyShift action_21 -action_3 (32) = happyShift action_22 -action_3 (34) = happyShift action_23 -action_3 (35) = happyShift action_8 -action_3 (36) = happyShift action_24 +action_3 (30) = happyShift action_19 +action_3 (31) = happyShift action_20 +action_3 (33) = happyShift action_21 +action_3 (34) = happyShift action_22 +action_3 (36) = happyShift action_23 +action_3 (37) = happyShift action_24 +action_3 (38) = happyShift action_8 +action_3 (39) = happyShift action_25 action_3 (10) = happyGoto action_12 action_3 (11) = happyGoto action_13 action_3 (13) = happyGoto action_14 action_3 (14) = happyGoto action_15 -action_3 (15) = happyGoto action_27 +action_3 (15) = happyGoto action_28 action_3 _ = happyFail (happyExpListPerState 3) action_4 (19) = happyShift action_18 -action_4 (28) = happyShift action_19 -action_4 (29) = happyShift action_20 -action_4 (31) = happyShift action_21 -action_4 (32) = happyShift action_22 -action_4 (34) = happyShift action_23 -action_4 (35) = happyShift action_8 -action_4 (36) = happyShift action_24 +action_4 (30) = happyShift action_19 +action_4 (31) = happyShift action_20 +action_4 (33) = happyShift action_21 +action_4 (34) = happyShift action_22 +action_4 (36) = happyShift action_23 +action_4 (37) = happyShift action_24 +action_4 (38) = happyShift action_8 +action_4 (39) = happyShift action_25 action_4 (10) = happyGoto action_12 action_4 (11) = happyGoto action_13 action_4 (13) = happyGoto action_14 action_4 (14) = happyGoto action_15 -action_4 (15) = happyGoto action_25 -action_4 (16) = happyGoto action_26 +action_4 (15) = happyGoto action_26 +action_4 (16) = happyGoto action_27 action_4 _ = happyFail (happyExpListPerState 4) action_5 (19) = happyShift action_18 -action_5 (28) = happyShift action_19 -action_5 (29) = happyShift action_20 -action_5 (31) = happyShift action_21 -action_5 (32) = happyShift action_22 -action_5 (34) = happyShift action_23 -action_5 (35) = happyShift action_8 -action_5 (36) = happyShift action_24 +action_5 (30) = happyShift action_19 +action_5 (31) = happyShift action_20 +action_5 (33) = happyShift action_21 +action_5 (34) = happyShift action_22 +action_5 (36) = happyShift action_23 +action_5 (37) = happyShift action_24 +action_5 (38) = happyShift action_8 +action_5 (39) = happyShift action_25 action_5 (10) = happyGoto action_12 action_5 (11) = happyGoto action_13 action_5 (13) = happyGoto action_14 @@ -228,22 +243,23 @@ action_5 (15) = happyGoto action_16 action_5 (17) = happyGoto action_17 action_5 _ = happyFail (happyExpListPerState 5) -action_6 (25) = happyShift action_10 -action_6 (26) = happyShift action_11 +action_6 (27) = happyShift action_10 +action_6 (28) = happyShift action_11 action_6 (18) = happyGoto action_9 action_6 _ = happyFail (happyExpListPerState 6) -action_7 (35) = happyShift action_8 +action_7 (38) = happyShift action_8 action_7 _ = happyFail (happyExpListPerState 7) action_8 _ = happyReduce_7 -action_9 (37) = happyAccept +action_9 (23) = happyShift action_42 +action_9 (40) = happyAccept action_9 _ = happyFail (happyExpListPerState 9) -action_10 _ = happyReduce_26 +action_10 _ = happyReduce_28 -action_11 _ = happyReduce_25 +action_11 _ = happyReduce_27 action_12 _ = happyReduce_10 @@ -251,215 +267,341 @@ action_13 _ = happyReduce_13 action_14 _ = happyReduce_18 -action_15 (21) = happyShift action_32 -action_15 (22) = happyShift action_33 -action_15 _ = happyReduce_21 - -action_16 _ = happyReduce_24 - -action_17 (37) = happyAccept +action_15 (21) = happyShift action_33 +action_15 (22) = happyShift action_34 +action_15 _ = happyReduce_23 + +action_16 (19) = happyShift action_18 +action_16 (30) = happyShift action_19 +action_16 (33) = happyShift action_21 +action_16 (36) = happyShift action_23 +action_16 (38) = happyShift action_8 +action_16 (39) = happyShift action_25 +action_16 (10) = happyGoto action_12 +action_16 (11) = happyGoto action_13 +action_16 (13) = happyGoto action_14 +action_16 (14) = happyGoto action_35 +action_16 _ = happyReduce_26 + +action_17 (40) = happyAccept action_17 _ = happyFail (happyExpListPerState 17) action_18 (19) = happyShift action_18 -action_18 (28) = happyShift action_19 -action_18 (29) = happyShift action_20 -action_18 (31) = happyShift action_21 -action_18 (32) = happyShift action_22 -action_18 (34) = happyShift action_23 -action_18 (35) = happyShift action_8 -action_18 (36) = happyShift action_24 +action_18 (30) = happyShift action_19 +action_18 (31) = happyShift action_20 +action_18 (33) = happyShift action_21 +action_18 (34) = happyShift action_22 +action_18 (36) = happyShift action_23 +action_18 (37) = happyShift action_24 +action_18 (38) = happyShift action_8 +action_18 (39) = happyShift action_25 action_18 (10) = happyGoto action_12 action_18 (11) = happyGoto action_13 action_18 (13) = happyGoto action_14 action_18 (14) = happyGoto action_15 -action_18 (15) = happyGoto action_25 -action_18 (16) = happyGoto action_38 +action_18 (15) = happyGoto action_26 +action_18 (16) = happyGoto action_41 action_18 _ = happyFail (happyExpListPerState 18) action_19 _ = happyReduce_12 action_20 (19) = happyShift action_18 -action_20 (28) = happyShift action_19 -action_20 (29) = happyShift action_20 -action_20 (31) = happyShift action_21 -action_20 (32) = happyShift action_22 -action_20 (34) = happyShift action_23 -action_20 (35) = happyShift action_8 -action_20 (36) = happyShift action_24 +action_20 (30) = happyShift action_19 +action_20 (31) = happyShift action_20 +action_20 (33) = happyShift action_21 +action_20 (34) = happyShift action_22 +action_20 (36) = happyShift action_23 +action_20 (37) = happyShift action_24 +action_20 (38) = happyShift action_8 +action_20 (39) = happyShift action_25 action_20 (10) = happyGoto action_12 action_20 (11) = happyGoto action_13 action_20 (13) = happyGoto action_14 action_20 (14) = happyGoto action_15 -action_20 (15) = happyGoto action_37 +action_20 (15) = happyGoto action_40 action_20 _ = happyFail (happyExpListPerState 20) -action_21 (19) = happyShift action_36 +action_21 (19) = happyShift action_39 action_21 _ = happyFail (happyExpListPerState 21) -action_22 (35) = happyShift action_8 -action_22 (10) = happyGoto action_30 -action_22 (12) = happyGoto action_35 +action_22 (38) = happyShift action_8 +action_22 (10) = happyGoto action_31 +action_22 (12) = happyGoto action_38 action_22 _ = happyFail (happyExpListPerState 22) action_23 _ = happyReduce_11 -action_24 _ = happyReduce_8 - -action_25 (23) = happyShift action_34 -action_25 _ = happyReduce_23 - -action_26 (37) = happyAccept -action_26 _ = happyFail (happyExpListPerState 26) - -action_27 (37) = happyAccept +action_24 (38) = happyShift action_8 +action_24 (10) = happyGoto action_31 +action_24 (12) = happyGoto action_37 +action_24 _ = happyFail (happyExpListPerState 24) + +action_25 _ = happyReduce_8 + +action_26 (19) = happyShift action_18 +action_26 (25) = happyShift action_36 +action_26 (30) = happyShift action_19 +action_26 (33) = happyShift action_21 +action_26 (36) = happyShift action_23 +action_26 (38) = happyShift action_8 +action_26 (39) = happyShift action_25 +action_26 (10) = happyGoto action_12 +action_26 (11) = happyGoto action_13 +action_26 (13) = happyGoto action_14 +action_26 (14) = happyGoto action_35 +action_26 _ = happyReduce_25 + +action_27 (40) = happyAccept action_27 _ = happyFail (happyExpListPerState 27) -action_28 (21) = happyShift action_32 -action_28 (22) = happyShift action_33 -action_28 (37) = happyAccept +action_28 (19) = happyShift action_18 +action_28 (30) = happyShift action_19 +action_28 (33) = happyShift action_21 +action_28 (36) = happyShift action_23 +action_28 (38) = happyShift action_8 +action_28 (39) = happyShift action_25 +action_28 (40) = happyAccept +action_28 (10) = happyGoto action_12 +action_28 (11) = happyGoto action_13 +action_28 (13) = happyGoto action_14 +action_28 (14) = happyGoto action_35 action_28 _ = happyFail (happyExpListPerState 28) -action_29 (37) = happyAccept +action_29 (21) = happyShift action_33 +action_29 (22) = happyShift action_34 +action_29 (40) = happyAccept action_29 _ = happyFail (happyExpListPerState 29) -action_30 _ = happyReduce_9 +action_30 (40) = happyAccept +action_30 _ = happyFail (happyExpListPerState 30) -action_31 (37) = happyAccept -action_31 _ = happyFail (happyExpListPerState 31) +action_31 _ = happyReduce_9 -action_32 (19) = happyShift action_18 -action_32 (28) = happyShift action_19 -action_32 (34) = happyShift action_23 -action_32 (35) = happyShift action_8 -action_32 (36) = happyShift action_24 -action_32 (10) = happyGoto action_12 -action_32 (11) = happyGoto action_13 -action_32 (13) = happyGoto action_45 +action_32 (40) = happyAccept action_32 _ = happyFail (happyExpListPerState 32) action_33 (19) = happyShift action_18 -action_33 (28) = happyShift action_19 -action_33 (34) = happyShift action_23 -action_33 (35) = happyShift action_8 -action_33 (36) = happyShift action_24 +action_33 (30) = happyShift action_19 +action_33 (36) = happyShift action_23 +action_33 (38) = happyShift action_8 +action_33 (39) = happyShift action_25 action_33 (10) = happyGoto action_12 action_33 (11) = happyGoto action_13 -action_33 (13) = happyGoto action_44 +action_33 (13) = happyGoto action_51 action_33 _ = happyFail (happyExpListPerState 33) -action_34 (25) = happyShift action_10 -action_34 (26) = happyShift action_11 -action_34 (18) = happyGoto action_43 +action_34 (19) = happyShift action_18 +action_34 (30) = happyShift action_19 +action_34 (36) = happyShift action_23 +action_34 (38) = happyShift action_8 +action_34 (39) = happyShift action_25 +action_34 (10) = happyGoto action_12 +action_34 (11) = happyGoto action_13 +action_34 (13) = happyGoto action_50 action_34 _ = happyFail (happyExpListPerState 34) -action_35 (24) = happyShift action_42 -action_35 _ = happyFail (happyExpListPerState 35) - -action_36 (19) = happyShift action_18 -action_36 (28) = happyShift action_19 -action_36 (29) = happyShift action_20 -action_36 (31) = happyShift action_21 -action_36 (32) = happyShift action_22 -action_36 (34) = happyShift action_23 -action_36 (35) = happyShift action_8 -action_36 (36) = happyShift action_24 -action_36 (10) = happyGoto action_12 -action_36 (11) = happyGoto action_13 -action_36 (13) = happyGoto action_14 -action_36 (14) = happyGoto action_15 -action_36 (15) = happyGoto action_25 -action_36 (16) = happyGoto action_41 +action_35 (21) = happyShift action_33 +action_35 (22) = happyShift action_34 +action_35 _ = happyReduce_22 + +action_36 (27) = happyShift action_10 +action_36 (28) = happyShift action_11 +action_36 (18) = happyGoto action_49 action_36 _ = happyFail (happyExpListPerState 36) -action_37 (33) = happyShift action_40 +action_37 (25) = happyShift action_48 action_37 _ = happyFail (happyExpListPerState 37) -action_38 (20) = happyShift action_39 +action_38 (26) = happyShift action_47 action_38 _ = happyFail (happyExpListPerState 38) -action_39 _ = happyReduce_14 +action_39 (19) = happyShift action_18 +action_39 (30) = happyShift action_19 +action_39 (31) = happyShift action_20 +action_39 (33) = happyShift action_21 +action_39 (34) = happyShift action_22 +action_39 (36) = happyShift action_23 +action_39 (37) = happyShift action_24 +action_39 (38) = happyShift action_8 +action_39 (39) = happyShift action_25 +action_39 (10) = happyGoto action_12 +action_39 (11) = happyGoto action_13 +action_39 (13) = happyGoto action_14 +action_39 (14) = happyGoto action_15 +action_39 (15) = happyGoto action_26 +action_39 (16) = happyGoto action_46 +action_39 _ = happyFail (happyExpListPerState 39) action_40 (19) = happyShift action_18 -action_40 (28) = happyShift action_19 -action_40 (29) = happyShift action_20 -action_40 (31) = happyShift action_21 -action_40 (32) = happyShift action_22 -action_40 (34) = happyShift action_23 -action_40 (35) = happyShift action_8 -action_40 (36) = happyShift action_24 +action_40 (30) = happyShift action_19 +action_40 (33) = happyShift action_21 +action_40 (35) = happyShift action_45 +action_40 (36) = happyShift action_23 +action_40 (38) = happyShift action_8 +action_40 (39) = happyShift action_25 action_40 (10) = happyGoto action_12 action_40 (11) = happyGoto action_13 action_40 (13) = happyGoto action_14 -action_40 (14) = happyGoto action_15 -action_40 (15) = happyGoto action_48 +action_40 (14) = happyGoto action_35 action_40 _ = happyFail (happyExpListPerState 40) -action_41 (20) = happyShift action_47 +action_41 (20) = happyShift action_44 action_41 _ = happyFail (happyExpListPerState 41) -action_42 (19) = happyShift action_18 -action_42 (28) = happyShift action_19 -action_42 (29) = happyShift action_20 -action_42 (31) = happyShift action_21 -action_42 (32) = happyShift action_22 -action_42 (34) = happyShift action_23 -action_42 (35) = happyShift action_8 -action_42 (36) = happyShift action_24 -action_42 (10) = happyGoto action_12 -action_42 (11) = happyGoto action_13 -action_42 (13) = happyGoto action_14 -action_42 (14) = happyGoto action_15 -action_42 (15) = happyGoto action_46 +action_42 (27) = happyShift action_10 +action_42 (28) = happyShift action_11 +action_42 (18) = happyGoto action_43 action_42 _ = happyFail (happyExpListPerState 42) -action_43 _ = happyReduce_22 - -action_44 _ = happyReduce_16 - -action_45 _ = happyReduce_15 - -action_46 (30) = happyShift action_50 +action_43 (23) = happyShift action_42 +action_43 _ = happyReduce_29 + +action_44 _ = happyReduce_14 + +action_45 (19) = happyShift action_18 +action_45 (30) = happyShift action_19 +action_45 (31) = happyShift action_20 +action_45 (33) = happyShift action_21 +action_45 (34) = happyShift action_22 +action_45 (36) = happyShift action_23 +action_45 (37) = happyShift action_24 +action_45 (38) = happyShift action_8 +action_45 (39) = happyShift action_25 +action_45 (10) = happyGoto action_12 +action_45 (11) = happyGoto action_13 +action_45 (13) = happyGoto action_14 +action_45 (14) = happyGoto action_15 +action_45 (15) = happyGoto action_55 +action_45 _ = happyFail (happyExpListPerState 45) + +action_46 (20) = happyShift action_54 action_46 _ = happyFail (happyExpListPerState 46) -action_47 _ = happyReduce_17 - -action_48 (27) = happyShift action_49 +action_47 (19) = happyShift action_18 +action_47 (30) = happyShift action_19 +action_47 (31) = happyShift action_20 +action_47 (33) = happyShift action_21 +action_47 (34) = happyShift action_22 +action_47 (36) = happyShift action_23 +action_47 (37) = happyShift action_24 +action_47 (38) = happyShift action_8 +action_47 (39) = happyShift action_25 +action_47 (10) = happyGoto action_12 +action_47 (11) = happyGoto action_13 +action_47 (13) = happyGoto action_14 +action_47 (14) = happyGoto action_15 +action_47 (15) = happyGoto action_53 +action_47 _ = happyFail (happyExpListPerState 47) + +action_48 (27) = happyShift action_10 +action_48 (28) = happyShift action_11 +action_48 (18) = happyGoto action_52 action_48 _ = happyFail (happyExpListPerState 48) -action_49 (19) = happyShift action_18 -action_49 (28) = happyShift action_19 -action_49 (29) = happyShift action_20 -action_49 (31) = happyShift action_21 -action_49 (32) = happyShift action_22 -action_49 (34) = happyShift action_23 -action_49 (35) = happyShift action_8 -action_49 (36) = happyShift action_24 -action_49 (10) = happyGoto action_12 -action_49 (11) = happyGoto action_13 -action_49 (13) = happyGoto action_14 -action_49 (14) = happyGoto action_15 -action_49 (15) = happyGoto action_52 -action_49 _ = happyFail (happyExpListPerState 49) - -action_50 (19) = happyShift action_18 -action_50 (28) = happyShift action_19 -action_50 (29) = happyShift action_20 -action_50 (31) = happyShift action_21 -action_50 (32) = happyShift action_22 -action_50 (34) = happyShift action_23 -action_50 (35) = happyShift action_8 -action_50 (36) = happyShift action_24 -action_50 (10) = happyGoto action_12 -action_50 (11) = happyGoto action_13 -action_50 (13) = happyGoto action_14 -action_50 (14) = happyGoto action_15 -action_50 (15) = happyGoto action_16 -action_50 (17) = happyGoto action_51 -action_50 _ = happyFail (happyExpListPerState 50) - -action_51 _ = happyReduce_20 - -action_52 _ = happyReduce_19 +action_49 (23) = happyShift action_42 +action_49 _ = happyReduce_24 + +action_50 _ = happyReduce_16 + +action_51 _ = happyReduce_15 + +action_52 (23) = happyShift action_42 +action_52 (24) = happyShift action_58 +action_52 _ = happyFail (happyExpListPerState 52) + +action_53 (19) = happyShift action_18 +action_53 (30) = happyShift action_19 +action_53 (32) = happyShift action_57 +action_53 (33) = happyShift action_21 +action_53 (36) = happyShift action_23 +action_53 (38) = happyShift action_8 +action_53 (39) = happyShift action_25 +action_53 (10) = happyGoto action_12 +action_53 (11) = happyGoto action_13 +action_53 (13) = happyGoto action_14 +action_53 (14) = happyGoto action_35 +action_53 _ = happyFail (happyExpListPerState 53) + +action_54 _ = happyReduce_17 + +action_55 (19) = happyShift action_18 +action_55 (29) = happyShift action_56 +action_55 (30) = happyShift action_19 +action_55 (33) = happyShift action_21 +action_55 (36) = happyShift action_23 +action_55 (38) = happyShift action_8 +action_55 (39) = happyShift action_25 +action_55 (10) = happyGoto action_12 +action_55 (11) = happyGoto action_13 +action_55 (13) = happyGoto action_14 +action_55 (14) = happyGoto action_35 +action_55 _ = happyFail (happyExpListPerState 55) + +action_56 (19) = happyShift action_18 +action_56 (30) = happyShift action_19 +action_56 (31) = happyShift action_20 +action_56 (33) = happyShift action_21 +action_56 (34) = happyShift action_22 +action_56 (36) = happyShift action_23 +action_56 (37) = happyShift action_24 +action_56 (38) = happyShift action_8 +action_56 (39) = happyShift action_25 +action_56 (10) = happyGoto action_12 +action_56 (11) = happyGoto action_13 +action_56 (13) = happyGoto action_14 +action_56 (14) = happyGoto action_15 +action_56 (15) = happyGoto action_61 +action_56 _ = happyFail (happyExpListPerState 56) + +action_57 (19) = happyShift action_18 +action_57 (30) = happyShift action_19 +action_57 (31) = happyShift action_20 +action_57 (33) = happyShift action_21 +action_57 (34) = happyShift action_22 +action_57 (36) = happyShift action_23 +action_57 (37) = happyShift action_24 +action_57 (38) = happyShift action_8 +action_57 (39) = happyShift action_25 +action_57 (10) = happyGoto action_12 +action_57 (11) = happyGoto action_13 +action_57 (13) = happyGoto action_14 +action_57 (14) = happyGoto action_15 +action_57 (15) = happyGoto action_16 +action_57 (17) = happyGoto action_60 +action_57 _ = happyFail (happyExpListPerState 57) + +action_58 (19) = happyShift action_18 +action_58 (30) = happyShift action_19 +action_58 (31) = happyShift action_20 +action_58 (33) = happyShift action_21 +action_58 (34) = happyShift action_22 +action_58 (36) = happyShift action_23 +action_58 (37) = happyShift action_24 +action_58 (38) = happyShift action_8 +action_58 (39) = happyShift action_25 +action_58 (10) = happyGoto action_12 +action_58 (11) = happyGoto action_13 +action_58 (13) = happyGoto action_14 +action_58 (14) = happyGoto action_15 +action_58 (15) = happyGoto action_16 +action_58 (17) = happyGoto action_59 +action_58 _ = happyFail (happyExpListPerState 58) + +action_59 _ = happyReduce_21 + +action_60 _ = happyReduce_20 + +action_61 (19) = happyShift action_18 +action_61 (30) = happyShift action_19 +action_61 (33) = happyShift action_21 +action_61 (36) = happyShift action_23 +action_61 (38) = happyShift action_8 +action_61 (39) = happyShift action_25 +action_61 (10) = happyGoto action_12 +action_61 (11) = happyGoto action_13 +action_61 (13) = happyGoto action_14 +action_61 (14) = happyGoto action_35 +action_61 _ = happyReduce_19 happyReduce_7 = happySpecReduce_1 10 happyReduction_7 happyReduction_7 (HappyTerminal (PT _ (TV happy_var_1))) @@ -576,50 +718,79 @@ happyReduction_20 ((HappyAbsSyn17 happy_var_6) `HappyStk` (HM.Parser.Abs.ELet happy_var_2 happy_var_4 happy_var_6 ) `HappyStk` happyRest -happyReduce_21 = happySpecReduce_1 15 happyReduction_21 -happyReduction_21 (HappyAbsSyn13 happy_var_1) +happyReduce_21 = happyReduce 6 15 happyReduction_21 +happyReduction_21 ((HappyAbsSyn17 happy_var_6) `HappyStk` + _ `HappyStk` + (HappyAbsSyn18 happy_var_4) `HappyStk` + _ `HappyStk` + (HappyAbsSyn12 happy_var_2) `HappyStk` + _ `HappyStk` + happyRest) + = HappyAbsSyn13 + (HM.Parser.Abs.EAbs happy_var_2 happy_var_4 happy_var_6 + ) `HappyStk` happyRest + +happyReduce_22 = happySpecReduce_2 15 happyReduction_22 +happyReduction_22 (HappyAbsSyn13 happy_var_2) + (HappyAbsSyn13 happy_var_1) + = HappyAbsSyn13 + (HM.Parser.Abs.EApp happy_var_1 happy_var_2 + ) +happyReduction_22 _ _ = notHappyAtAll + +happyReduce_23 = happySpecReduce_1 15 happyReduction_23 +happyReduction_23 (HappyAbsSyn13 happy_var_1) = HappyAbsSyn13 (happy_var_1 ) -happyReduction_21 _ = notHappyAtAll +happyReduction_23 _ = notHappyAtAll -happyReduce_22 = happySpecReduce_3 16 happyReduction_22 -happyReduction_22 (HappyAbsSyn18 happy_var_3) +happyReduce_24 = happySpecReduce_3 16 happyReduction_24 +happyReduction_24 (HappyAbsSyn18 happy_var_3) _ (HappyAbsSyn13 happy_var_1) = HappyAbsSyn13 (HM.Parser.Abs.ETyped happy_var_1 happy_var_3 ) -happyReduction_22 _ _ _ = notHappyAtAll +happyReduction_24 _ _ _ = notHappyAtAll -happyReduce_23 = happySpecReduce_1 16 happyReduction_23 -happyReduction_23 (HappyAbsSyn13 happy_var_1) +happyReduce_25 = happySpecReduce_1 16 happyReduction_25 +happyReduction_25 (HappyAbsSyn13 happy_var_1) = HappyAbsSyn13 (happy_var_1 ) -happyReduction_23 _ = notHappyAtAll +happyReduction_25 _ = notHappyAtAll -happyReduce_24 = happySpecReduce_1 17 happyReduction_24 -happyReduction_24 (HappyAbsSyn13 happy_var_1) +happyReduce_26 = happySpecReduce_1 17 happyReduction_26 +happyReduction_26 (HappyAbsSyn13 happy_var_1) = HappyAbsSyn17 (HM.Parser.Abs.ScopedExp happy_var_1 ) -happyReduction_24 _ = notHappyAtAll +happyReduction_26 _ = notHappyAtAll -happyReduce_25 = happySpecReduce_1 18 happyReduction_25 -happyReduction_25 _ +happyReduce_27 = happySpecReduce_1 18 happyReduction_27 +happyReduction_27 _ = HappyAbsSyn18 (HM.Parser.Abs.TNat ) -happyReduce_26 = happySpecReduce_1 18 happyReduction_26 -happyReduction_26 _ +happyReduce_28 = happySpecReduce_1 18 happyReduction_28 +happyReduction_28 _ = HappyAbsSyn18 (HM.Parser.Abs.TBool ) +happyReduce_29 = happySpecReduce_3 18 happyReduction_29 +happyReduction_29 (HappyAbsSyn18 happy_var_3) + _ + (HappyAbsSyn18 happy_var_1) + = HappyAbsSyn18 + (HM.Parser.Abs.TArrow happy_var_1 happy_var_3 + ) +happyReduction_29 _ _ _ = notHappyAtAll + happyNewToken action sts stk [] = - action 37 37 notHappyAtAll (HappyState action) sts stk [] + action 40 40 notHappyAtAll (HappyState action) sts stk [] happyNewToken action sts stk (tk:tks) = let cont i = action i i tk (HappyState action) sts stk tks in @@ -640,12 +811,15 @@ happyNewToken action sts stk (tk:tks) = PT _ (TS _ 14) -> cont 32; PT _ (TS _ 15) -> cont 33; PT _ (TS _ 16) -> cont 34; - PT _ (TV happy_dollar_dollar) -> cont 35; - PT _ (TI happy_dollar_dollar) -> cont 36; + PT _ (TS _ 17) -> cont 35; + PT _ (TS _ 18) -> cont 36; + PT _ (TS _ 19) -> cont 37; + PT _ (TV happy_dollar_dollar) -> cont 38; + PT _ (TI happy_dollar_dollar) -> cont 39; _ -> happyError' ((tk:tks), []) } -happyError_ explist 37 tk tks = happyError' (tks, explist) +happyError_ explist 40 tk tks = happyError' (tks, explist) happyError_ explist _ tk tks = happyError' ((tk:tks), explist) happyThen :: () => Err a -> (a -> Err b) -> Err b diff --git a/src/HM/Parser/Par.y b/src/HM/Parser/Par.y index aa45000..1db0f1d 100644 --- a/src/HM/Parser/Par.y +++ b/src/HM/Parser/Par.y @@ -39,18 +39,21 @@ import HM.Parser.Lex ')' { PT _ (TS _ 2) } '+' { PT _ (TS _ 3) } '-' { PT _ (TS _ 4) } - ':' { PT _ (TS _ 5) } - '=' { PT _ (TS _ 6) } - 'Bool' { PT _ (TS _ 7) } - 'Nat' { PT _ (TS _ 8) } - 'else' { PT _ (TS _ 9) } - 'false' { PT _ (TS _ 10) } - 'if' { PT _ (TS _ 11) } - 'in' { PT _ (TS _ 12) } - 'iszero' { PT _ (TS _ 13) } - 'let' { PT _ (TS _ 14) } - 'then' { PT _ (TS _ 15) } - 'true' { PT _ (TS _ 16) } + '->' { PT _ (TS _ 5) } + '.' { PT _ (TS _ 6) } + ':' { PT _ (TS _ 7) } + '=' { PT _ (TS _ 8) } + 'Bool' { PT _ (TS _ 9) } + 'Nat' { PT _ (TS _ 10) } + 'else' { PT _ (TS _ 11) } + 'false' { PT _ (TS _ 12) } + 'if' { PT _ (TS _ 13) } + 'in' { PT _ (TS _ 14) } + 'iszero' { PT _ (TS _ 15) } + 'let' { PT _ (TS _ 16) } + 'then' { PT _ (TS _ 17) } + 'true' { PT _ (TS _ 18) } + 'λ' { PT _ (TS _ 19) } L_Ident { PT _ (TV $$) } L_integ { PT _ (TI $$) } @@ -84,6 +87,8 @@ Exp1 :: { HM.Parser.Abs.Exp } Exp1 : 'if' Exp1 'then' Exp1 'else' Exp1 { HM.Parser.Abs.EIf $2 $4 $6 } | 'let' Pattern '=' Exp1 'in' ScopedExp { HM.Parser.Abs.ELet $2 $4 $6 } + | 'λ' Pattern ':' Type '.' ScopedExp { HM.Parser.Abs.EAbs $2 $4 $6 } + | Exp1 Exp2 { HM.Parser.Abs.EApp $1 $2 } | Exp2 { $1 } Exp :: { HM.Parser.Abs.Exp } @@ -94,7 +99,9 @@ ScopedExp : Exp1 { HM.Parser.Abs.ScopedExp $1 } Type :: { HM.Parser.Abs.Type } Type - : 'Nat' { HM.Parser.Abs.TNat } | 'Bool' { HM.Parser.Abs.TBool } + : 'Nat' { HM.Parser.Abs.TNat } + | 'Bool' { HM.Parser.Abs.TBool } + | Type '->' Type { HM.Parser.Abs.TArrow $1 $3 } { diff --git a/src/HM/Parser/Print.hs b/src/HM/Parser/Print.hs index 1d75666..f1d2846 100644 --- a/src/HM/Parser/Print.hs +++ b/src/HM/Parser/Print.hs @@ -155,6 +155,8 @@ instance Print HM.Parser.Abs.Exp where HM.Parser.Abs.EIsZero exp -> prPrec i 2 (concatD [doc (showString "iszero"), doc (showString "("), prt 0 exp, doc (showString ")")]) HM.Parser.Abs.ETyped exp type_ -> prPrec i 0 (concatD [prt 1 exp, doc (showString ":"), prt 0 type_]) HM.Parser.Abs.ELet pattern_ exp scopedexp -> prPrec i 1 (concatD [doc (showString "let"), prt 0 pattern_, doc (showString "="), prt 1 exp, doc (showString "in"), prt 0 scopedexp]) + HM.Parser.Abs.EAbs pattern_ type_ scopedexp -> prPrec i 1 (concatD [doc (showString "\955"), prt 0 pattern_, doc (showString ":"), prt 0 type_, doc (showString "."), prt 0 scopedexp]) + HM.Parser.Abs.EApp exp1 exp2 -> prPrec i 1 (concatD [prt 1 exp1, prt 2 exp2]) instance Print HM.Parser.Abs.ScopedExp where prt i = \case @@ -164,3 +166,4 @@ instance Print HM.Parser.Abs.Type where prt i = \case HM.Parser.Abs.TNat -> prPrec i 0 (concatD [doc (showString "Nat")]) HM.Parser.Abs.TBool -> prPrec i 0 (concatD [doc (showString "Bool")]) + HM.Parser.Abs.TArrow type_1 type_2 -> prPrec i 0 (concatD [prt 0 type_1, doc (showString "->"), prt 0 type_2]) diff --git a/src/HM/Parser/Skel.hs b/src/HM/Parser/Skel.hs index cede61a..a3cdae1 100644 --- a/src/HM/Parser/Skel.hs +++ b/src/HM/Parser/Skel.hs @@ -35,6 +35,8 @@ transExp x = case x of HM.Parser.Abs.EIsZero exp -> failure x HM.Parser.Abs.ETyped exp type_ -> failure x HM.Parser.Abs.ELet pattern_ exp scopedexp -> failure x + HM.Parser.Abs.EAbs pattern_ type_ scopedexp -> failure x + HM.Parser.Abs.EApp exp1 exp2 -> failure x transScopedExp :: HM.Parser.Abs.ScopedExp -> Result transScopedExp x = case x of @@ -44,3 +46,4 @@ transType :: HM.Parser.Abs.Type -> Result transType x = case x of HM.Parser.Abs.TNat -> failure x HM.Parser.Abs.TBool -> failure x + HM.Parser.Abs.TArrow type_1 type_2 -> failure x diff --git a/src/HM/Syntax.hs b/src/HM/Syntax.hs index 895550b..7c26dae 100644 --- a/src/HM/Syntax.hs +++ b/src/HM/Syntax.hs @@ -1,22 +1,23 @@ -{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TemplateHaskell #-} + module HM.Syntax where -import qualified Control.Monad.Foil as Foil -import Control.Monad.Free.Foil -import Control.Monad.Free.Foil.TH -import Data.Bifunctor.TH -import Data.Map (Map) -import qualified Data.Map as Map -import Data.String (IsString (..)) -import qualified HM.Parser.Abs as Raw -import qualified HM.Parser.Par as Raw -import qualified HM.Parser.Print as Raw +import qualified Control.Monad.Foil as Foil +import Control.Monad.Free.Foil +import Control.Monad.Free.Foil.TH +import Data.Bifunctor.TH +import Data.Map (Map) +import qualified Data.Map as Map +import Data.String (IsString (..)) +import qualified HM.Parser.Abs as Raw +import qualified HM.Parser.Par as Raw +import qualified HM.Parser.Print as Raw -- $setup -- >>> :set -XOverloadedStrings @@ -28,6 +29,7 @@ import qualified HM.Parser.Print as Raw -- * Generated code -- ** Signature + mkSignature ''Raw.Exp ''Raw.Ident ''Raw.ScopedExp ''Raw.Pattern deriveZipMatch ''ExpSig deriveBifunctor ''ExpSig @@ -35,6 +37,7 @@ deriveBifoldable ''ExpSig deriveBitraversable ''ExpSig -- ** Pattern synonyms + mkPatternSynonyms ''ExpSig {-# COMPLETE Var, ETrue, EFalse, ENat, EAdd, ESub, EIf, EIsZero, ETyped, ELet #-} @@ -52,7 +55,7 @@ type Exp n = AST ExpSig n -- | Convert 'Raw.Exp' into a scope-safe expression. -- This is a special case of 'convertToAST'. -toExp :: Foil.Distinct n => Foil.Scope n -> Map Raw.Ident (Foil.Name n) -> Raw.Exp -> AST ExpSig n +toExp :: (Foil.Distinct n) => Foil.Scope n -> Map Raw.Ident (Foil.Name n) -> Raw.Exp -> AST ExpSig n toExp = convertToAST convertToExpSig getPatternBinder getExpFromScopedExp -- | Convert 'Raw.Exp' into a closed scope-safe expression. @@ -67,12 +70,13 @@ toExpClosed = toExp Foil.emptyScope Map.empty -- -- This function does not recover location information for variables, patterns, or scoped terms. fromExp :: Exp n -> Raw.Exp -fromExp = convertFromAST - convertFromExpSig - Raw.EVar - Raw.PatternVar - Raw.ScopedExp - (\n -> Raw.Ident ("x" ++ show n)) +fromExp = + convertFromAST + convertFromExpSig + Raw.EVar + Raw.PatternVar + Raw.ScopedExp + (\n -> Raw.Ident ("x" ++ show n)) -- | Parse scope-safe terms via raw representation. -- @@ -80,9 +84,9 @@ fromExp = convertFromAST -- let x0 = 2 + 2 in let x1 = x0 - 1 in let x2 = 3 in x1 + x2 + x1 instance IsString (Exp Foil.VoidS) where fromString input = case Raw.pExp (Raw.myLexer input) of - Left err -> error ("could not parse expression: " <> input <> "\n " <> err) + Left err -> error ("could not parse expression: " <> input <> "\n " <> err) Right term -> toExpClosed term --- | Pretty-print scope-safe terms via raw representation. +-- | Pretty-print scope-safe terms via"λ" Ident ":" Type "." Exp1 raw representation. instance Show (Exp n) where show = Raw.printTree . fromExp diff --git a/src/HM/Typecheck.hs b/src/HM/Typecheck.hs index b9fd830..d414927 100644 --- a/src/HM/Typecheck.hs +++ b/src/HM/Typecheck.hs @@ -1,14 +1,19 @@ {-# LANGUAGE DataKinds #-} +{-# OPTIONS_GHC -Wno-overlapping-patterns #-} module HM.Typecheck where -import Control.Monad.Foil (NameMap, addNameBinder, emptyNameMap, - lookupName) -import qualified Control.Monad.Foil as Foil +import Control.Monad.Foil + ( NameMap, + addNameBinder, + emptyNameMap, + lookupName, + ) +import qualified Control.Monad.Foil as Foil import qualified Control.Monad.Free.Foil as FreeFoil -import HM.Parser.Abs (Type (..)) -import qualified HM.Parser.Print as Raw -import HM.Syntax +import HM.Parser.Abs (Type (..)) +import qualified HM.Parser.Print as Raw +import HM.Syntax -- $setup -- >>> :set -XOverloadedStrings @@ -43,14 +48,10 @@ typecheck scope e expectedType = do ] inferType :: NameMap n Type -> Exp n -> Either String Type +inferType scope (FreeFoil.Var n) = Right (lookupName n scope) -- Γ, x : T ⊢ x : T inferType _scope ETrue = return TBool inferType _scope EFalse = return TBool inferType _scope (ENat _) = return TNat -inferType scope (EIf eCond eThen eElse) = do - _ <- typecheck scope eCond TBool - typeOfThen <- inferType scope eThen - _ <- typecheck scope eElse typeOfThen - return typeOfThen inferType scope (EAdd l r) = do _ <- typecheck scope l TNat _ <- typecheck scope r TNat @@ -59,13 +60,30 @@ inferType scope (ESub l r) = do _ <- typecheck scope l TNat _ <- typecheck scope r TNat return TNat +inferType scope (EIf eCond eThen eElse) = do + _ <- typecheck scope eCond TBool + typeOfThen <- inferType scope eThen + _ <- typecheck scope eElse typeOfThen + return typeOfThen inferType scope (EIsZero e) = do _ <- typecheck scope e TNat return TBool -inferType scope (ELet e1 x e2) = do -- Γ ⊢ let x = e1 in e2 : ? - type1 <- inferType scope e1 -- Γ ⊢ e1 : type1 - let newScope = addNameBinder x type1 scope -- Γ' = Γ, x : type1 - inferType newScope e2 -- Γ' ⊢ e2 : ? inferType scope (ETyped expr type_) = do typecheck scope expr type_ -inferType scope (FreeFoil.Var n) = Right (lookupName n scope) -- Γ, x : T ⊢ x : T +inferType scope (ELet e1 x e2) = do + -- Γ ⊢ let x = e1 in e2 : ? + type1 <- inferType scope e1 -- Γ ⊢ e1 : type1 + let newScope = addNameBinder x type1 scope -- Γ' = Γ, x : type1 + inferType newScope e2 -- Γ' ⊢ e2 : ? +inferType scope (EAbs type_ x e) = do + -- Γ ⊢ λx : type_. e : ? + let newScope = addNameBinder x type_ scope -- Γ' = Γ, x : type_ + TArrow type_ <$> inferType newScope e +inferType scope (EApp e1 e2) = do + -- (Γ ⊢ e1) (Γ ⊢ e2) : ? + type1 <- inferType scope e1 -- Γ ⊢ e1 : type1 + case type1 of + TArrow type_ types -> do + _ <- typecheck scope e2 type_ + return types + _ -> Left ("expected type\n TArrow\nbut got type\n " <> show type1) diff --git a/test/files/ill-typed/7.lam b/test/files/ill-typed/7.lam new file mode 100644 index 0000000..f446180 --- /dev/null +++ b/test/files/ill-typed/7.lam @@ -0,0 +1 @@ +λx:Nat. let y = x + 1 in y : Nat -> Bool \ No newline at end of file diff --git a/test/files/ill-typed/8.lam b/test/files/ill-typed/8.lam new file mode 100644 index 0000000..c279aee --- /dev/null +++ b/test/files/ill-typed/8.lam @@ -0,0 +1 @@ +let f = λx:Nat. x + 1 in f true \ No newline at end of file diff --git a/test/files/ill-typed/9.lam b/test/files/ill-typed/9.lam new file mode 100644 index 0000000..3388fe3 --- /dev/null +++ b/test/files/ill-typed/9.lam @@ -0,0 +1 @@ +let f = if iszero (5) then (λx:Nat. x) else (λx:Bool. x + 1) in f 5 \ No newline at end of file diff --git a/test/files/well-typed/7.lam b/test/files/well-typed/7.lam new file mode 100644 index 0000000..34d456e --- /dev/null +++ b/test/files/well-typed/7.lam @@ -0,0 +1 @@ +(λx:Nat. if iszero (x) then 0 else x + 1) 5 \ No newline at end of file diff --git a/test/files/well-typed/8.lam b/test/files/well-typed/8.lam new file mode 100644 index 0000000..4bbb9f9 --- /dev/null +++ b/test/files/well-typed/8.lam @@ -0,0 +1 @@ +let f = λx:Nat. x + 1 in f 5 \ No newline at end of file diff --git a/test/files/well-typed/9.lam b/test/files/well-typed/9.lam new file mode 100644 index 0000000..7d03101 --- /dev/null +++ b/test/files/well-typed/9.lam @@ -0,0 +1 @@ +let f = if iszero (5) then (λx:Nat. x) else (λx:Nat. x + 1) in f 5 \ No newline at end of file