diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 --- /dev/null +++ b/CHANGES.md @@ -0,0 +1,7 @@ +Release notes for glambda +========================= + +1.0 +--- + +Initial release. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +Copyright (c) 2015, Richard Eisenberg +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, +this list of conditions and the following disclaimer in the documentation +and/or other materials provided with the distribution. + +3. Neither the name of the author nor the names of its contributors may be +used to endorse or promote products derived from this software without +specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,186 @@ +A Practical Introduction to Haskell GADTs +========================================= + +This repo and these notes are for a talk given at [LambdaConf][1] in +Boulder, CO, USA, on 22 May, 2015. + +See below for more information about `glambda` itself. + +Setup +----- + +**Do this first!** + +We will be working from my [glambda][2] project to learn about Generalized +Algebraic Datatypes (GADTs). The `glambda` package has a non-trivial set +of dependencies. While I'm introducing myself and GADTs, generally, it would +be wise to download and compile all of the dependencies onto your laptop. +Then, when we get to hands-on exercises, you'll be all ready to go. + +Here's what to do + + > git clone git://github.com/goldfirere/glambda.git + > cd glambda + > cabal sandbox init + > cabal install --only-dependencies --enable-tests -j<# of CPUs you have> + +This should make your computer spin for a little while. In the meantime, +enjoy the talk! (If you have trouble with `cabal sandbox`, possibly because +of an old `cabal`, try the sequence of commands above without that step.) + +Exercises 1 and 2 do *not* require those dependencies, so you can work on +them while compiling dependencies. + +Instructions for exercises: + - [Exercise 1](Exercise1.md) + - [Exercise 2](Exercise2.md) + - [Exercise 3](Exercise3.md) + +[1]: http://www.degoesconsulting.com/lambdaconf-2015/ +[2]: https://github.com/goldfirere/glambda + +More information about `glambda` appears below: + +The Glamorous Glambda Interpreter +================================= + +Glambda is a simply-typed lambda calculus interpreter. While it is intended +to be easy-to-use and help users learn about the lambda calculus, its real +strength is its implementation, which makes heavy use of GADTs, and is designed +to serve as a showcase of writing a real-world program with extra compile-time +guarantees. + +This manual focuses only on the user experience. The structure of the code +will be described in a series of GADT programming tutorials coming out +Real Soon Now. + +Example session +--------------- + +Saying `cabal install glambda` will produce an executable `glam`. `glam` is +the lambda-calculus interpreter. It is GHCi-like, accepting commands beginning +with a `:`. Here is an example session: + +~~~ + \\\\\\ + \\\\\\ + /-\ \\\\\\ + | | \\\\\\ + \-/| \\\\\\ + | //\\\\\\ + \-/ ////\\\\\\ + //////\\\\\\ + ////// \\\\\\ + ////// \\\\\\ +Welcome to the Glamorous Glambda interpreter, version 1.0. +λ> (\x:Int.x + 2) 5 +7 : Int +λ> revapp = \x:Int.\y:Int->Int.y x +revapp = λ#. λ#. #0 #1 : Int -> (Int -> Int) -> Int +λ> not = \b:Bool.if b then false else true +not = λ#. if #0 then false else true : Bool -> Bool +λ> revapp (3 < 4) not +Bad function application. + Function type: Int -> (Int -> Int) -> Int + Argument type: Bool +in the expression 'revapp (3 < 4)' +λ> not (3 < 4) +false : Bool +λ> :type revapp (10 % 3) +(λ#. λ#. #0 #1) (10 % 3) : (Int -> Int) -> Int +λ> :step revapp (10 % 3) (\x:Int.x * 2) +(λ#. λ#. #0 #1) (10 % 3) (λ#. #0 * 2) : Int +--> (λ#. #0 (10 % 3)) (λ#. #0 * 2) : Int +--> (λ#. #0 * 2) (10 % 3) : Int +--> 10 % 3 * 2 : Int +--> 1 * 2 : Int +--> 2 : Int +2 : Int +λ> :quit +Good-bye. +~~~ + +As you can see, glambda uses [de Bruijn indices][1] to track variable binding. +In the actual output (if your console supports it), the binders (`#`) and +usage sites (`#0`, `#1`) are colored so that humans can easily tell which +variable is used where. + +[1]: https://en.wikipedia.org/wiki/De_Bruijn_index + +You can also see above that the input to glambda must be fully annotated; +glambda does *not* do type inference. However, note that types on binders +do not appear in the output: once an input is type-checked, the type information +is erased. Yet, because of the use of GADTs in the implementation, we +can be sure that the reductions are type-safe. + +The Language +------------ + +The glambda language is an explicitly typed simply typed lambda calculus, +with integers (`Int`) and booleans (`Bool`). The following operators are +supported, with their usual meanings, associativity, and precedence: + + + - * / % < <= > >= == + +The only slightly unusual member of this list is `%`, which takes a modulus, +like in C-inspired languages. The division operator `/` does integer division, +naturally. + +Glambda supports a ternary conditional operator, demonstrated in the +snippet above, as `if then else `. + +Integer constants must be positive. Subtract from 0 to get a negative integer. + +Boolean constants are spelled `false` and `true`. + +Comments are exactly as in Haskell: `--` starts a line comment, and +`{- ... -}` is a block comment. Comments can be nested. + +Variable names are as in Haskell: names must start with a letter or +underscore (although case is immaterial) and then may have letters, numbers, +and underscores. + +The language is not whitespace-aware. + +Most of what we have seen are *expressions*. Glambda also supports *statements*. +A statement is either an expression or has the form ` = `. +This latter form assigns a global variable to the expression. These global +variables are expanded during type-checking: they are more like macros than +proper cells holding information. Statements can be separated by `;`. + +The Interface +------------- + +When you type an expression into the glambda interpreter, it is evaluated +fully, and the value is printed, along with its type. + +When you type a global variable assignment, that variable is assigned, and +its (unevaluated) contents are printed, along with its type. + +You can also run commands, as described below. Commands all start with a +leading `:`, and that `:` must be the first character on the input line. +Arguments to a command are given after the command itself. Commands can +be abbreviated by typing an unambiguous prefix to a command. For example, +`:t` can be used to get an expression's type, because no other command +begins with `t`. + +Commands +-------- + +`:quit` quits the glambda interpreter. + +`:lex` lexes the given text and pretty-prints the result. + +`:parse` parses the given text and pretty-prints the result. + +`:eval` type-checks and evaluates the given expression. This is +the default behavior at the command line. + +`:step` runs the given expression through the single-step semantics. +This shows you every step of the way from your expression down to +a value. This uses a *different* evaluation strategy than `:eval` does, +but the result should always be the same. + +`:type` gives you the type of an expression. + +`:all` runs both `:eval` and `:step` on an expression. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/glambda.cabal b/glambda.cabal new file mode 100644 --- /dev/null +++ b/glambda.cabal @@ -0,0 +1,87 @@ +name: glambda +version: 1.0 +cabal-version: >= 1.10 +synopsis: A simply typed lambda calculus interpreter, written with GADTs +homepage: https://github.com/goldfirere/glambda +category: Compilers/Interpreters +author: Richard Eisenberg +maintainer: Richard Eisenberg +bug-reports: https://github.com/goldfirere/glambda/issues +stability: unknown +extra-source-files: README.md, CHANGES.md +license: BSD3 +license-file: LICENSE +build-type: Simple +description: + This is an interpreter for the simply-typed lambda calculus. It is + written making heavy use of generalized algebraic datatypes (GADTs), and is + meant to serve as an example how how these GADTs can be useful. See + the GitHub repo for more information about the syntax for the language + and interpreter commands. + +source-repository this + type: git + location: https://github.com/goldfirere/glambda.git + tag: v1.0 + +library + build-depends: base == 4.* + , ansi-wl-pprint >= 0.6.7.1 + , errors >= 1.4.6 && < 2.0 + , mtl >= 2.1.3.1 + , containers >= 0.5 + , parsec >= 3.1 + , haskeline >= 0.7.1.1 + , directory >= 1.2.0.1 + + + exposed-modules: Language.Glambda.Repl + Language.Glambda.Check + Language.Glambda.Eval + Language.Glambda.Exp + Language.Glambda.Globals + Language.Glambda.Lex + Language.Glambda.Monad + Language.Glambda.Parse + Language.Glambda.Pretty + Language.Glambda.Shift + Language.Glambda.Statement + Language.Glambda.Token + Language.Glambda.Type + Language.Glambda.Unchecked + Language.Glambda.Util + + hs-source-dirs: src + ghc-options: -Wall -fno-warn-name-shadowing + default-language: Haskell2010 + +executable glam + build-depends: base == 4.* + , glambda + + hs-source-dirs: main + ghc-options: -Wall -fno-warn-name-shadowing + default-language: Haskell2010 + main-is: Main.hs + +test-suite tests + type: exitcode-stdio-1.0 + hs-source-dirs: tests + ghc-options: -Wall -fno-warn-name-shadowing -main-is Tests.Main + default-language: Haskell2010 + main-is: Tests/Main.hs + + other-modules: Tests.Check + Tests.Parse + Tests.Lex + Tests.Util + + build-depends: base == 4.* + , glambda + , template-haskell + , ansi-wl-pprint >= 0.6.7.1 + , errors >= 1.4.6 && < 2.0 + , mtl >= 2.1.3.1 + , parsec >= 3.1 + , tasty >= 0.8.1 + , tasty-hunit >= 0.9 diff --git a/main/Main.hs b/main/Main.hs new file mode 100644 --- /dev/null +++ b/main/Main.hs @@ -0,0 +1,6 @@ +module Main where + +import qualified Language.Glambda.Repl as Repl ( main ) + +main :: IO () +main = Repl.main diff --git a/src/Language/Glambda/Check.hs b/src/Language/Glambda/Check.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Check.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, FlexibleContexts, CPP #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} + +#ifdef __HADDOCK_VERSION__ +{-# OPTIONS_GHC -fno-warn-unused-imports #-} +#endif + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Unchecked +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- The glambda typechecker. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Check ( check ) where + +import Language.Glambda.Exp +import Language.Glambda.Shift +import Language.Glambda.Token +import Language.Glambda.Type +import Language.Glambda.Unchecked +import Language.Glambda.Util +import Language.Glambda.Globals +#ifdef __HADDOCK_VERSION__ +import Language.Glambda.Monad ( GlamE ) +#endif + +import Text.PrettyPrint.ANSI.Leijen + +import Control.Monad.Reader +import Control.Monad.Error + +-- | Abort with a type error in the given expression +typeError :: MonadError Doc m => UExp -> Doc -> m a +typeError e doc = throwError $ + doc $$ text "in the expression" <+> squotes (pretty e) + +------------------------------------------------ +-- The typechecker + +-- | Check the given expression, aborting on type errors. The resulting +-- type and checked expression is given to the provided continuation. +-- This is parameterized over the choice of monad in order to support +-- pure operation during testing. 'GlamE' is the canonical choice for the +-- monad. +check :: (MonadError Doc m, MonadReader Globals m) + => UExp -> (forall t. STy t -> Exp '[] t -> m r) + -> m r +check = go emptyContext + where + go :: (MonadError Doc m, MonadReader Globals m) + => SCtx ctx -> UExp -> (forall t. STy t -> Exp ctx t -> m r) + -> m r + + go ctx (UVar n) k + = check_var ctx n $ \ty elem -> + k ty (Var elem) + + go ctx (UGlobal n) k + = do globals <- ask + lookupGlobal globals n $ \ty exp -> + k ty (shift_into_ctx ctx exp) + + go ctx (ULam ty body) k + = refineTy ty $ \arg_ty -> + go (arg_ty `SCons` ctx) body $ \res_ty body' -> + k (arg_ty `SArr` res_ty) (Lam body') + + go ctx e@(UApp e1 e2) k + = go ctx e1 $ \ty1 e1' -> + go ctx e2 $ \ty2 e2' -> + case (ty1, ty2) of + (SArr arg_ty res_ty, arg_ty') + | Just Refl <- arg_ty `eqSTy` arg_ty' + -> k res_ty (App e1' e2') + _ -> typeError e $ + text "Bad function application." $$ + indent 2 (vcat [ text "Function type:" <+> pretty ty1 + , text "Argument type:" <+> pretty ty2 ]) + + go ctx e@(UArith e1 (UArithOp op) e2) k + = go ctx e1 $ \sty1 e1' -> + go ctx e2 $ \sty2 e2' -> + case (sty1, sty2) of + (SIntTy, SIntTy) + -> k sty (Arith e1' op e2') + _ -> typeError e $ + text "Bad arith operand(s)." $$ + indent 2 (vcat [ text " Left-hand type:" <+> pretty sty1 + , text "Right-hand type:" <+> pretty sty2 ]) + + go ctx e@(UCond e1 e2 e3) k + = go ctx e1 $ \sty1 e1' -> + go ctx e2 $ \sty2 e2' -> + go ctx e3 $ \sty3 e3' -> + case sty1 of + SBoolTy + | Just Refl <- sty2 `eqSTy` sty3 + -> k sty2 (Cond e1' e2' e3') + _ -> typeError e $ + text "Bad conditional." $$ + indent 2 (vcat [ text "Flag type:" <+> pretty sty1 + , squotes (text "true") <+> text "expression type:" + <+> pretty sty2 + , squotes (text "false") <+> text "expression type:" + <+> pretty sty3 ]) + + go ctx e@(UFix e1) k + = go ctx e1 $ \sty1 e1' -> + case sty1 of + arg `SArr` res + | Just Refl <- arg `eqSTy` res + -> k arg (Fix e1') + _ -> typeError e $ + text "Bad fix over expression with type:" <+> pretty sty1 + + go _ (UIntE n) k = k sty (IntE n) + go _ (UBoolE b) k = k sty (BoolE b) + +check_var :: MonadError Doc m + => SCtx ctx -> Int + -> (forall t. STy t -> Elem ctx t -> m r) + -> m r +check_var SNil _ _ = throwError (text "unbound variable") + -- shouldn't happen. caught by parser. + +-- | Type-check a de Bruijn index variable +check_var (SCons ty _) 0 k = k ty EZ +check_var (SCons _ ctx) n k = check_var ctx (n-1) $ \ty elem -> + k ty (ES elem) + +-- | Take a closed expression and shift its indices to make sense in +-- a non-empty context. +shift_into_ctx :: SCtx ctx -> Exp '[] ty -> Exp ctx ty +shift_into_ctx SNil exp = exp +shift_into_ctx (_ `SCons` ctx') exp = shift $ shift_into_ctx ctx' exp diff --git a/src/Language/Glambda/Eval.hs b/src/Language/Glambda/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Eval.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE RankNTypes, TypeOperators, ScopedTypeVariables, + DataKinds, TypeFamilies, PolyKinds, + GADTs #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Eval +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Glambda expression evaluators for checked expressions. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Eval ( eval, step ) where + +import Language.Glambda.Exp +import Language.Glambda.Token +import Language.Glambda.Shift + +-- | Given a lambda and an expression, beta-reduce. +apply :: Val (arg -> res) -> Exp '[] arg -> Exp '[] res +apply (LamVal body) arg = subst arg body + +-- | Apply an arithmetic operator to two values. +arith :: Val Int -> ArithOp ty -> Val Int -> Exp '[] ty +arith (IntVal n1) Plus (IntVal n2) = IntE (n1 + n2) +arith (IntVal n1) Minus (IntVal n2) = IntE (n1 - n2) +arith (IntVal n1) Times (IntVal n2) = IntE (n1 * n2) +arith (IntVal n1) Divide (IntVal n2) = IntE (n1 `div` n2) +arith (IntVal n1) Mod (IntVal n2) = IntE (n1 `mod` n2) +arith (IntVal n1) Less (IntVal n2) = BoolE (n1 < n2) +arith (IntVal n1) LessE (IntVal n2) = BoolE (n1 <= n2) +arith (IntVal n1) Greater (IntVal n2) = BoolE (n1 > n2) +arith (IntVal n1) GreaterE (IntVal n2) = BoolE (n1 >= n2) +arith (IntVal n1) Equals (IntVal n2) = BoolE (n1 == n2) + +-- | Conditionally choose between two expressions +cond :: Val Bool -> Exp '[] t -> Exp '[] t -> Exp '[] t +cond (BoolVal True) e _ = e +cond (BoolVal False) _ e = e + +-- | Unroll a `fix` one level +unfix :: Val (ty -> ty) -> Exp '[] ty +unfix (LamVal body) = subst (Fix (Lam body)) body + +-- | A well-typed variable in an empty context is impossible. +impossibleVar :: Elem '[] x -> a +impossibleVar _ = error "GHC's typechecker failed" + -- GHC 7.8+ supports EmptyCase for this, but the warnings for that + -- construct don't work yet. + +-- | Evaluate an expression, using big-step semantics. +eval :: Exp '[] t -> Val t +eval (Var v) = impossibleVar v +eval (Lam body) = LamVal body +eval (App e1 e2) = eval (apply (eval e1) e2) +eval (Arith e1 op e2) = eval (arith (eval e1) op (eval e2)) +eval (Cond e1 e2 e3) = eval (cond (eval e1) e2 e3) +eval (Fix e) = eval (unfix (eval e)) +eval (IntE n) = IntVal n +eval (BoolE b) = BoolVal b + +-- | Step an expression, either to another expression or to a value. +step :: Exp '[] t -> Either (Exp '[] t) (Val t) +step (Var v) = impossibleVar v +step (Lam body) = Right (LamVal body) +step (App e1 e2) = case step e1 of + Left e1' -> Left (App e1' e2) + Right (LamVal body) -> Left (subst e2 body) +step (Arith e1 op e2) = case step e1 of + Left e1' -> Left (Arith e1' op e2) + Right v1 -> case step e2 of + Left e2' -> Left (Arith (val v1) op e2') + Right v2 -> Left (arith v1 op v2) +step (Cond e1 e2 e3) = case step e1 of + Left e1' -> Left (Cond e1' e2 e3) + Right v1 -> Left (cond v1 e2 e3) +step (Fix e) = case step e of + Left e' -> Left (Fix e') + Right v -> Left (unfix v) +step (IntE n) = Right (IntVal n) +step (BoolE b) = Right (BoolVal b) diff --git a/src/Language/Glambda/Exp.hs b/src/Language/Glambda/Exp.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Exp.hs @@ -0,0 +1,122 @@ +{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies, + ScopedTypeVariables #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Exp +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- The Exp GADT. Glambda expressions encoded in an 'Exp' value are +-- *always* well-typed. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Exp ( + Exp(..), Elem(..), GlamVal(..), Val(..), prettyVal, eqExp + ) where + +import Language.Glambda.Pretty +import Language.Glambda.Token +import Language.Glambda.Util +import Language.Glambda.Type + +import Text.PrettyPrint.ANSI.Leijen + +-- | @Elem xs x@ is evidence that @x@ is in the list @xs@. +-- @EZ :: Elem xs x@ is evidence that @x@ is the first element of @xs@. +-- @ES ev :: Elem xs x@ is evidence that @x@ is one position later in +-- @xs@ than is indicated in @ev@ +data Elem :: [a] -> a -> * where + EZ :: Elem (x ': xs) x + ES :: Elem xs x -> Elem (y ': xs) x + +-- | Convert an 'Elem' to a proper de Bruijn index +elemToInt :: Elem ctx ty -> Int +elemToInt EZ = 0 +elemToInt (ES e) = 1 + elemToInt e + +-- | @Exp ctx ty@ is a well-typed expression of type @ty@ in context +-- @ctx@. Note that a context is a list of types, where a type's index +-- in the list indicates the de Bruijn index of the associated term-level +-- variable. +data Exp :: [*] -> * -> * where + Var :: Elem ctx ty -> Exp ctx ty + Lam :: Exp (arg ': ctx) res -> Exp ctx (arg -> res) + App :: Exp ctx (arg -> res) -> Exp ctx arg -> Exp ctx res + Arith :: Exp ctx Int -> ArithOp ty -> Exp ctx Int -> Exp ctx ty + Cond :: Exp ctx Bool -> Exp ctx ty -> Exp ctx ty -> Exp ctx ty + Fix :: Exp ctx (ty -> ty) -> Exp ctx ty + IntE :: Int -> Exp ctx Int + BoolE :: Bool -> Exp ctx Bool + +-- | Classifies types that can be values of glambda expressions +class GlamVal t where + -- | Well-typed closed values. Encoded as a data family with newtype + -- instances in order to avoid runtime checking of values + data Val t + + -- | Convert a glambda value back into a glambda expression + val :: Val t -> Exp '[] t + +instance GlamVal Int where + newtype Val Int = IntVal Int + val (IntVal n) = IntE n + +instance GlamVal Bool where + newtype Val Bool = BoolVal Bool + val (BoolVal b) = BoolE b + +instance GlamVal (a -> b) where + newtype Val (a -> b) = LamVal (Exp '[a] b) + val (LamVal body) = Lam body + +---------------------------------------------------- +-- | Equality on expressions, needed for testing +eqExp :: Exp ctx1 ty1 -> Exp ctx2 ty2 -> Bool +eqExp (Var e1) (Var e2) = elemToInt e1 == elemToInt e2 +eqExp (Lam body1) (Lam body2) = body1 `eqExp` body2 +eqExp (App e1a e1b) (App e2a e2b) = e1a `eqExp` e2a && e1b `eqExp` e2b +eqExp (Arith e1a op1 e1b) (Arith e2a op2 e2b) + = e1a `eqExp` e2a && op1 `eqArithOp` op2 && e1b `eqExp` e2b +eqExp (Cond e1a e1b e1c) (Cond e2a e2b e2c) + = e1a `eqExp` e2a && e1b `eqExp` e2b && e1c `eqExp` e2c +eqExp (IntE i1) (IntE i2) = i1 == i2 +eqExp (BoolE b1) (BoolE b2) = b1 == b2 +eqExp _ _ = False + +---------------------------------------------------- +-- Pretty-printing + +instance Pretty (Exp ctx ty) where + pretty = defaultPretty + +instance PrettyExp (Exp ctx ty) where + prettyExp = pretty_exp + +instance GlamVal ty => Pretty (Val ty) where + pretty = defaultPretty + +instance GlamVal ty => PrettyExp (Val ty) where + prettyExp coloring prec v = prettyExp coloring prec (val v) + +-- | Pretty-prints a 'Val'. This needs type information to know how to print. +-- Pattern matching gives GHC enough information to be able to find the +-- 'GlamVal' instance needed to construct the 'PrettyExp' instance. +prettyVal :: Val t -> STy t -> Doc +prettyVal val SIntTy = pretty val +prettyVal val SBoolTy = pretty val +prettyVal val (_ `SArr` _) = pretty val + +pretty_exp :: Coloring -> Prec -> Exp ctx ty -> Doc +pretty_exp c _ (Var n) = prettyVar c (elemToInt n) +pretty_exp c prec (Lam body) = prettyLam c prec Nothing body +pretty_exp c prec (App e1 e2) = prettyApp c prec e1 e2 +pretty_exp c prec (Arith e1 op e2) = prettyArith c prec e1 op e2 +pretty_exp c prec (Cond e1 e2 e3) = prettyIf c prec e1 e2 e3 +pretty_exp c prec (Fix e) = prettyFix c prec e +pretty_exp _ _ (IntE n) = int n +pretty_exp _ _ (BoolE True) = text "true" +pretty_exp _ _ (BoolE False) = text "false" diff --git a/src/Language/Glambda/Globals.hs b/src/Language/Glambda/Globals.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Globals.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE GADTs, DataKinds, RankNTypes, FlexibleContexts #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Globals +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Manages the global variables in Glambda +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Globals ( + Globals, emptyGlobals, extend, lookupGlobal ) where + +import Language.Glambda.Exp +import Language.Glambda.Type + +import Text.PrettyPrint.ANSI.Leijen + +import Control.Monad.Error + +import Data.Map as Map + +-- | An existential wrapper around 'Exp', storing the expression and +-- its type. +data EExp where + EExp :: STy ty -> Exp '[] ty -> EExp + +-- | The global variable environment maps variables to type-checked +-- expressions +newtype Globals = Globals (Map String EExp) + +-- | An empty global variable environment +emptyGlobals :: Globals +emptyGlobals = Globals Map.empty + +-- | Extend a 'Globals' with a new binding +extend :: String -> STy ty -> Exp '[] ty -> Globals -> Globals +extend var sty exp (Globals globals) + = Globals $ Map.insert var (EExp sty exp) globals + +-- | Lookup a global variable. Fails with 'throwError' if the variable +-- is not bound. +lookupGlobal :: MonadError Doc m + => Globals -> String + -> (forall ty. STy ty -> Exp '[] ty -> m r) + -> m r +lookupGlobal (Globals globals) var k + = case Map.lookup var globals of + Just (EExp sty exp) -> k sty exp + Nothing -> throwError $ + text "Global variable not in scope:" <+> + squotes (text var) diff --git a/src/Language/Glambda/Lex.hs b/src/Language/Glambda/Lex.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Lex.hs @@ -0,0 +1,134 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Lex +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Lexes a Glambda program string into a sequence of tokens +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Lex ( lexG, lex ) where + +import Prelude hiding ( lex ) + +import Language.Glambda.Token +import Language.Glambda.Monad +import Language.Glambda.Util + +import Text.Parsec.Prim ( Parsec, parse, getPosition, try ) +import Text.Parsec.Combinator +import Text.Parsec.Char +import Text.Parsec.Token as Parsec +import Text.Parsec.Language + +import Data.Maybe + +import Control.Applicative +import Control.Arrow as Arrow + +type Lexer = Parsec String () + +--------------------------------------------------- +-- Utility +string_ :: String -> Lexer () +string_ = ignore . string + +--------------------------------------------------- +-- | Lex some program text into a list of 'LToken's, aborting upon failure +lexG :: String -> GlamE [LToken] +lexG = eitherToGlamE . lex + +-- | Lex some program text into a list of 'LToken's +lex :: String -> Either String [LToken] +lex = Arrow.left show . parse lexer "" + +-- | Overall lexer +lexer :: Lexer [LToken] +lexer = (catMaybes <$> many lexer1_ws) <* eof + +-- | Lex either one token or some whitespace +lexer1_ws :: Lexer (Maybe LToken) +lexer1_ws + = (Nothing <$ whitespace) + <|> + (Just <$> lexer1) + +-- | Lex some whitespace +whitespace :: Lexer () +whitespace + = choice [ ignore $ some space + , block_comment + , line_comment ] + +-- | Lex a @{- ... -}@ comment (perhaps nested); consumes no input +-- if the target doesn't start with @{-@. +block_comment :: Lexer () +block_comment = do + try $ string_ "{-" + comment_body + +-- | Lex a block comment, without the opening "{-" +comment_body :: Lexer () +comment_body + = choice [ block_comment *> comment_body + , try $ string_ "-}" + , anyChar *> comment_body ] + +-- | Lex a line comment +line_comment :: Lexer () +line_comment = do + try $ string_ "--" + ignore $ manyTill anyChar (eof <|> ignore newline) + +-- | Lex one token +lexer1 :: Lexer LToken +lexer1 = do + pos <- getPosition + L pos <$> choice [ symbolic + , word_token + , Int . fromInteger <$> Parsec.natural haskell ] + +-- | Lex one non-alphanumeric token +symbolic :: Lexer Token +symbolic = choice [ LParen <$ char '(' + , RParen <$ char ')' + , Lambda <$ char '\\' + , Dot <$ char '.' + , Arrow <$ try (string "->") + , Colon <$ char ':' + , ArithOp <$> arith_op + , Assign <$ char '=' + , Semi <$ char ';' ] + +-- | Lex one arithmetic operator +arith_op :: Lexer UArithOp +arith_op = choice [ UArithOp Plus <$ char '+' + , UArithOp Minus <$ char '-' + , UArithOp Times <$ char '*' + , UArithOp Divide <$ char '/' + , UArithOp Mod <$ char '%' + , UArithOp LessE <$ try (string "<=") + , UArithOp Less <$ char '<' + , UArithOp GreaterE <$ try (string ">=") + , UArithOp Greater <$ char '>' + , UArithOp Equals <$ try (string "==")] + +-- | Lex one alphanumeric token +word_token :: Lexer Token +word_token = to_token <$> word + where + to_token "true" = Bool True + to_token "false" = Bool False + to_token "if" = If + to_token "then" = Then + to_token "else" = Else + to_token "fix" = FixT + to_token other = Name other + +-- | Lex one word +word :: Lexer String +word = ((:) <$> (letter <|> char '_') <*> + (many (alphaNum <|> char '_'))) diff --git a/src/Language/Glambda/Monad.hs b/src/Language/Glambda/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Monad.hs @@ -0,0 +1,108 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, + FlexibleContexts, CPP, MultiParamTypeClasses #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Monad +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- The Glam monad, allowing for pretty-printed output to the user, failing +-- with an error message, and tracking global variables. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Monad ( + -- * The 'Glam' monad + Glam, runGlam, prompt, quit, + + -- * The 'GlamE' monad + GlamE, runGlamE, issueError, eitherToGlamE, + + -- * General functions over both glamorous monads + GlamM(..), + ) where + +import Language.Glambda.Globals +import Language.Glambda.Util + +import System.Console.Haskeline + +import Text.PrettyPrint.ANSI.Leijen + +import Control.Error +import Control.Monad.Reader +import Control.Monad.Error +import Control.Monad.State +import System.IO + +#if __GLASGOW_HASKELL__ < 709 +import Control.Applicative +#endif + +-- | A monad giving Haskeline-like interaction, access to 'Globals', +-- and the ability to abort with 'mzero'. +newtype Glam a = Glam { unGlam :: MaybeT (StateT Globals (InputT IO)) a } + deriving (Monad, Functor, Applicative, MonadState Globals, MonadIO) + +-- | Like the 'Glam' monad, but also supporting error messages via 'Doc's +newtype GlamE a = GlamE { unGlamE :: EitherT Doc Glam a } + deriving (Monad, Functor, Applicative, MonadError Doc) + +instance MonadReader Globals GlamE where + ask = GlamE get + local f thing_inside = GlamE $ do + old_globals <- get + put (f old_globals) + result <- unGlamE thing_inside + put old_globals + return result + +-- | Class for the two glamorous monads +class GlamM m where + -- | Print a 'Doc' without a newline at the end + printDoc :: Doc -> m () + + -- | Print a 'Doc' with a newline + printLine :: Doc -> m () + +instance GlamM Glam where + printDoc = Glam . liftIO . displayIO stdout . toSimpleDoc + printLine = Glam . liftIO . displayIO stdout . toSimpleDoc . (<> hardline) + +instance GlamM GlamE where + printDoc = GlamE . lift . printDoc + printLine = GlamE . lift . printLine + +-- | Prompt the user for input, returning a string if one is entered. +-- Like 'getInputLine'. +prompt :: String -> Glam (Maybe String) +prompt = Glam . lift . lift . getInputLine + +-- | Abort the 'Glam' monad +quit :: Glam a +quit = do + printLine (text "Good-bye.") + Glam mzero + +-- | Abort the computation with an error +issueError :: Doc -> GlamE a +issueError = GlamE . throwError + +-- | Hoist an 'Either' into 'GlamE' +eitherToGlamE :: Either String a -> GlamE a +eitherToGlamE (Left err) = issueError (text err) +eitherToGlamE (Right x) = return x + +-- | Run a 'Glam' computation +runGlam :: Glam () -> InputT IO () +runGlam thing_inside + = ignore $ flip evalStateT emptyGlobals $ runMaybeT $ unGlam thing_inside + +-- | Run a 'GlamE' computation +runGlamE :: GlamE a -> Glam (Either Doc a) +runGlamE thing_inside + = runEitherT $ unGlamE thing_inside diff --git a/src/Language/Glambda/Parse.hs b/src/Language/Glambda/Parse.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Parse.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE LambdaCase #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Parse +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Parses tokens into the un-type-checked AST. "Parsing", in glambda, +-- also includes name resolution. This all might +-- conceivably be done in a later pass, but there doesn't seem to be +-- an incentive to do so. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Parse ( + parseStmtsG, parseStmts, + parseStmtG, parseExpG, + parseStmt, parseExp + ) where + +import Language.Glambda.Unchecked +import Language.Glambda.Statement +import Language.Glambda.Token +import Language.Glambda.Type +import Language.Glambda.Monad +import Language.Glambda.Util + +import Text.Parsec.Prim as Parsec hiding ( parse ) +import Text.Parsec.Pos +import Text.Parsec.Combinator + +import Text.PrettyPrint.ANSI.Leijen hiding ( (<$>) ) + +import Data.List as List + +import Control.Applicative +import Control.Arrow as Arrow ( left ) +import Control.Monad.Reader + +-- | Parse a sequence of semicolon-separated statements, aborting with +-- an error upon failure +parseStmtsG :: [LToken] -> GlamE [Statement] +parseStmtsG = eitherToGlamE . parseStmts + +-- | Parse a sequence of semicolon-separated statements +parseStmts :: [LToken] -> Either String [Statement] +parseStmts = parse stmts + +-- | Parse a 'Statement', aborting with an error upon failure +parseStmtG :: [LToken] -> GlamE Statement +parseStmtG = eitherToGlamE . parseStmt + +-- | Parse a 'Statement' +parseStmt :: [LToken] -> Either String Statement +parseStmt = parse stmt + +-- | Parse a 'UExp', aborting with an error upon failure +parseExpG :: [LToken] -> GlamE UExp +parseExpG = eitherToGlamE . parseExp + +-- | Parse a 'UExp' +parseExp :: [LToken] -> Either String UExp +parseExp = parse expr + +parse :: Parser a -> [LToken] -> Either String a +parse p tokens = Arrow.left show $ + runReader (runParserT (p <* eof) () "" tokens) [] + +---------------------- +-- Plumbing + +-- the "state" is a list of bound names. searching a bound name in the list +-- gives you the correct deBruijn index +type Parser = ParsecT [LToken] () (Reader [String]) + +-- | Bind a name over an expression +bind :: String -> Parser a -> Parser a +bind bound_var thing_inside + = local (bound_var :) thing_inside + +-- | Parse the given nullary token +tok :: Token -> Parser () +tok t = tokenPrim (render . pretty) next_pos (guard . (t ==) . unLoc) + +-- | Parse the given unary token +tok' :: (Token -> Maybe thing) -> Parser thing +tok' matcher = tokenPrim (render . pretty) next_pos (matcher . unLoc) + +-- | Parse one of a set of 'ArithOp's +arith_op :: [UArithOp] -> Parser UArithOp +arith_op ops = tokenPrim (render . pretty) next_pos + (\case L _ (ArithOp op) | op `elem` ops -> Just op + _ -> Nothing) + +next_pos :: SourcePos -- ^ position of the current token + -> LToken -- ^ current token + -> [LToken] -- ^ remaining tokens + -> SourcePos -- ^ location of the next token +next_pos pos _ [] = pos +next_pos _ _ (L pos _ : _) = pos + +-------------- +-- Real work + +stmts :: Parser [Statement] +stmts = stmt `sepEndBy` tok Semi + +stmt :: Parser Statement +stmt = choice [ try $ NewGlobal <$> tok' unName <* tok Assign <*> expr + , BareExp <$> expr ] + +expr :: Parser UExp +expr = choice [ lam + , cond + , int_exp `chainl1` bool_op ] + +int_exp :: Parser UExp +int_exp = term `chainl1` add_op + +term :: Parser UExp +term = apps `chainl1` mul_op + +apps :: Parser UExp +apps = choice [ UFix <$ tok FixT <*> expr + , List.foldl1 UApp <$> some factor ] + +factor :: Parser UExp +factor = choice [ between (tok LParen) (tok RParen) expr + , UIntE <$> tok' unInt + , UBoolE <$> tok' unBool + , var ] + +lam :: Parser UExp +lam = do + tok Lambda + bound_var <- tok' unName + tok Colon + typ <- ty + tok Dot + e <- bind bound_var $ expr + return (ULam typ e) + +cond :: Parser UExp +cond = UCond <$ tok If <*> expr <* tok Then <*> expr <* tok Else <*> expr + +var :: Parser UExp +var = do + n <- tok' unName + m_index <- asks (elemIndex n) + case m_index of + Nothing -> return (UGlobal n) + Just i -> return (UVar i) + +ty :: Parser Ty +ty = chainr1 arg_ty (Arr <$ tok Arrow) + +arg_ty :: Parser Ty +arg_ty = choice [ between (tok LParen) (tok RParen) ty + , tycon ] + +tycon :: Parser Ty +tycon = do + n <- tok' unName + case readTyCon n of + Nothing -> unexpected $ render $ + text "type" <+> squotes (text n) + Just ty -> return ty + +add_op, mul_op, bool_op :: Parser (UExp -> UExp -> UExp) +add_op = mk_op <$> arith_op [uPlus, uMinus] +mul_op = mk_op <$> arith_op [uTimes, uDivide, uMod] +bool_op = mk_op <$> arith_op [uLess, uLessE, uGreater, uGreaterE, uEquals] + +mk_op :: UArithOp -> UExp -> UExp -> UExp +mk_op op = \e1 e2 -> UArith e1 op e2 diff --git a/src/Language/Glambda/Pretty.hs b/src/Language/Glambda/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Pretty.hs @@ -0,0 +1,127 @@ +{-# LANGUAGE ViewPatterns, GADTs, FlexibleInstances, UndecidableInstances, + CPP #-} +#if __GLASGOW_HASKELL__ <= 708 +{-# LANGUAGE OverlappingInstances #-} +{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-} +#endif + +{-# OPTIONS_GHC -fno-warn-orphans #-} + + + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Pretty +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Pretty-printing expressions. This allows reduction of code duplication +-- between unchecked and checked expressions. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Pretty ( + PrettyExp(..), defaultPretty, + Coloring, defaultColoring, + prettyVar, prettyLam, prettyApp, prettyArith, prettyIf, prettyFix + ) where + +import Language.Glambda.Token +import Language.Glambda.Type +import Language.Glambda.Util + +import Text.PrettyPrint.ANSI.Leijen + +lamPrec, appPrec, appLeftPrec, appRightPrec, ifPrec :: Prec +lamPrec = 1 +appPrec = 9 +appLeftPrec = 8.9 +appRightPrec = 9 +ifPrec = 1 + +opPrec, opLeftPrec, opRightPrec :: ArithOp ty -> Prec +opPrec (precInfo -> (x, _, _)) = x +opLeftPrec (precInfo -> (_, x, _)) = x +opRightPrec (precInfo -> (_, _, x)) = x + +-- | Returns (overall, left, right) precedences for an 'ArithOp' +precInfo :: ArithOp ty -> (Prec, Prec, Prec) +precInfo Plus = (5, 4.9, 5) +precInfo Minus = (5, 4.9, 5) +precInfo Times = (6, 5.9, 6) +precInfo Divide = (6, 5.9, 6) +precInfo Mod = (6, 5.9, 6) +precInfo Less = (4, 4, 4) +precInfo LessE = (4, 4, 4) +precInfo Greater = (4, 4, 4) +precInfo GreaterE = (4, 4, 4) +precInfo Equals = (4, 4, 4) + +-- | A function that changes a 'Doc's color +type ApplyColor = Doc -> Doc + +-- | Information about coloring in de Bruijn indexes and binders +data Coloring = Coloring [ApplyColor] + [ApplyColor] -- ^ a stream of remaining colors to use, + -- and the colors used for bound variables + +-- | A 'Coloring' for an empty context +defaultColoring :: Coloring +defaultColoring = Coloring all_colors [] + where + all_colors = red : green : yellow : blue : + magenta : cyan : all_colors + +-- | A class for expressions that can be pretty-printed +class Pretty exp => PrettyExp exp where + prettyExp :: Coloring -> Prec -> exp -> Doc + +-- | Convenient implementation of 'pretty' +defaultPretty :: PrettyExp exp => exp -> Doc +defaultPretty = nest 2 . prettyExp defaultColoring topPrec + +-- | Print a variable +prettyVar :: Coloring -> Int -> Doc +prettyVar (Coloring _ bound) n = (nthDefault id n bound) (char '#' <> int n) + +-- | Print a lambda expression +prettyLam :: PrettyExp exp => Coloring -> Prec -> Maybe Ty -> exp -> Doc +prettyLam (Coloring (next : supply) existing) prec m_ty body + = maybeParens (prec >= lamPrec) $ + fillSep [ char 'λ' <> next (char '#') <> + maybe empty (\ty -> text ":" <> pretty ty) m_ty <> char '.' + , prettyExp (Coloring supply (next : existing)) topPrec body ] +prettyLam _ _ _ _ = error "Infinite supply of colors ran out" + +-- | Print an application +prettyApp :: (PrettyExp exp1, PrettyExp exp2) + => Coloring -> Prec -> exp1 -> exp2 -> Doc +prettyApp coloring prec e1 e2 + = maybeParens (prec >= appPrec) $ + fillSep [ prettyExp coloring appLeftPrec e1 + , prettyExp coloring appRightPrec e2 ] + +-- | Print an arithemtic expression +prettyArith :: (PrettyExp exp1, PrettyExp exp2) + => Coloring -> Prec -> exp1 -> ArithOp ty -> exp2 -> Doc +prettyArith coloring prec e1 op e2 + = maybeParens (prec >= opPrec op) $ + fillSep [ prettyExp coloring (opLeftPrec op) e1 <+> pretty op + , prettyExp coloring (opRightPrec op) e2 ] + +-- | Print a conditional +prettyIf :: (PrettyExp exp1, PrettyExp exp2, PrettyExp exp3) + => Coloring -> Prec -> exp1 -> exp2 -> exp3 -> Doc +prettyIf coloring prec e1 e2 e3 + = maybeParens (prec >= ifPrec) $ + fillSep [ text "if" <+> prettyExp coloring topPrec e1 + , text "then" <+> prettyExp coloring topPrec e2 + , text "else" <+> prettyExp coloring topPrec e3 ] + +-- | Print a @fix@ +prettyFix :: PrettyExp exp => Coloring -> Prec -> exp -> Doc +prettyFix coloring prec e + = maybeParens (prec >= appPrec) $ + text "fix" <+> prettyExp coloring topPrec e diff --git a/src/Language/Glambda/Repl.hs b/src/Language/Glambda/Repl.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Repl.hs @@ -0,0 +1,225 @@ +{-# LANGUAGE FlexibleInstances, + UndecidableInstances, CPP, ViewPatterns, + NondecreasingIndentation #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE OverlappingInstances #-} +{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-} +#endif + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Repl +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Implements a REPL for glambda. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Repl ( main ) where + +import Prelude hiding ( lex ) + +import Language.Glambda.Check +import Language.Glambda.Eval +import Language.Glambda.Lex +import Language.Glambda.Parse +import Language.Glambda.Unchecked +import Language.Glambda.Util +import Language.Glambda.Statement +import Language.Glambda.Globals +import Language.Glambda.Monad +import Language.Glambda.Exp +import Language.Glambda.Type + +import Text.PrettyPrint.ANSI.Leijen as Pretty hiding ( (<$>) ) + +import System.Console.Haskeline +import System.Directory + +import Control.Monad +import Control.Monad.Reader +import Control.Monad.State +import Data.Char +import Data.List as List + +#if __GLASGOW_HASKELL__ < 709 +import Control.Applicative +#endif + +-- | The glamorous Glambda interpreter +main :: IO () +main = runInputT defaultSettings $ + runGlam $ do + helloWorld + loop + +loop :: Glam () +loop = do + m_line <- prompt "λ> " + case stripWhitespace <$> m_line of + Nothing -> quit + Just (':' : cmd) -> runCommand cmd + Just str -> runStmts str + loop + +-- | Prints welcome message +helloWorld :: Glam () +helloWorld = do + printLine lambda + printLine $ text "Welcome to the Glamorous Glambda interpreter, version" <+> + text version <> char '.' + +-- | The welcome message +lambda :: Doc +lambda + = vcat $ List.map text + [ " \\\\\\\\\\\\ " + , " \\\\\\\\\\\\ " + , " /-\\ \\\\\\\\\\\\ " + , " | | \\\\\\\\\\\\ " + , " \\-/| \\\\\\\\\\\\ " + , " | //\\\\\\\\\\\\ " + , " \\-/ ////\\\\\\\\\\\\ " + , " //////\\\\\\\\\\\\ " + , " ////// \\\\\\\\\\\\ " + , " ////// \\\\\\\\\\\\ " + ] + +-- | The current version of glambda +version :: String +version = "1.0" + +------------------------------------------- +-- running statements + +runStmts :: String -> Glam () +runStmts str = reportErrors $ do + toks <- lexG str + stmts <- parseStmtsG toks + doStmts stmts + +-- | Run a sequence of statements, returning the new global variables +doStmts :: [Statement] -> GlamE Globals +doStmts [] = ask +doStmts (s:ss) = doStmt s $ doStmts ss + +-- | Run a 'Statement' and then run another action with the global +-- variables built in the 'Statement' +doStmt :: Statement -> GlamE a -> GlamE a +doStmt (BareExp uexp) thing_inside = check uexp $ \sty exp -> do + printLine $ printValWithType (eval exp) sty + thing_inside +doStmt (NewGlobal g uexp) thing_inside = check uexp $ \sty exp -> do + printLine $ text g <+> char '=' <+> printWithType exp sty + local (extend g sty exp) thing_inside + +------------------------------------------- +-- commands + +-- | Interpret a command (missing the initial ':'). +runCommand :: String -> Glam () +runCommand = dispatchCommand cmdTable + +type CommandTable = [(String, String -> Glam ())] + +dispatchCommand :: CommandTable -> String -> Glam () +dispatchCommand table line + = case List.filter ((cmd `List.isPrefixOf`) . fst) table of + [] -> do printLine $ text "Unknown command:" <+> squotes (text cmd) + [(_, action)] -> action arg + many -> do printLine $ text "Ambiguous command:" <+> squotes (text cmd) + printLine $ text "Possibilities:" $$ + indent 2 (vcat $ List.map (text . fst) many) + where (cmd, arg) = List.break isSpace line + +cmdTable :: CommandTable +cmdTable = [ ("quit", quitCmd) + , ("d-lex", lexCmd) + , ("d-parse", parseCmd) + , ("load", loadCmd) + , ("eval", evalCmd) + , ("step", stepCmd) + , ("type", typeCmd) + , ("all", allCmd) ] + +quitCmd :: String -> Glam () +quitCmd _ = quit + +class Reportable a where + report :: a -> Glam Globals + +instance Reportable Doc where + report x = printLine x >> get +instance Reportable () where + report _ = get +instance Reportable Globals where + report = return +instance {-# OVERLAPPABLE #-} Pretty a => Reportable a where + report other = printLine (pretty other) >> get + +reportErrors :: Reportable a => GlamE a -> Glam () +reportErrors thing_inside = do + result <- runGlamE thing_inside + new_globals <- case result of + Left err -> printLine err >> get + Right x -> report x + put new_globals + +parseLex :: String -> GlamE UExp +parseLex = parseExpG <=< lexG + +printWithType :: (Pretty exp, Pretty ty) => exp -> ty -> Doc +printWithType exp ty + = pretty exp <+> colon <+> pretty ty + +printValWithType :: Val ty -> STy ty -> Doc +printValWithType val sty + = prettyVal val sty <+> colon <+> pretty sty + +lexCmd, parseCmd, evalCmd, stepCmd, typeCmd, allCmd, loadCmd + :: String -> Glam () +lexCmd expr = reportErrors $ lexG expr +parseCmd = reportErrors . parseLex + +evalCmd expr = reportErrors $ do + uexp <- parseLex expr + check uexp $ \sty exp -> + return $ printValWithType (eval exp) sty + +stepCmd expr = reportErrors $ do + uexp <- parseLex expr + check uexp $ \sty exp -> do + printLine $ printWithType exp sty + let loop e = case step e of + Left e' -> do + printLine $ text "-->" <+> printWithType e' sty + loop e' + Right v -> return v + v <- loop exp + return $ printValWithType v sty + +typeCmd expr = reportErrors $ do + uexp <- parseLex expr + check uexp $ \sty exp -> return (printWithType exp sty) + +allCmd expr = do + printLine (text "Small step:") + _ <- stepCmd expr + + printLine Pretty.empty + printLine (text "Big step:") + evalCmd expr + +loadCmd (stripWhitespace -> file) = do + file_exists <- liftIO $ doesFileExist file + if not file_exists then file_not_found else do + contents <- liftIO $ readFile file + runStmts contents + where + file_not_found = do + printLine (text "File not found:" <+> squotes (text file)) + cwd <- liftIO getCurrentDirectory + printLine (parens (text "Current directory:" <+> text cwd)) diff --git a/src/Language/Glambda/Shift.hs b/src/Language/Glambda/Shift.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Shift.hs @@ -0,0 +1,77 @@ +{-# LANGUAGE ScopedTypeVariables, DataKinds, PolyKinds, TypeOperators, + TypeFamilies, GADTs #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Shift +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- de Bruijn shifting and substitution +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Shift ( shift, subst ) where + +import Language.Glambda.Exp + +-- | @Length xs@ tells you how long a list @xs@ is. +-- @LZ :: Length xs@ says that @xs@ is empty. +-- @LS len :: Length xs@ tells you that @xs@ has one more element +-- than @len@ says. +data Length :: [a] -> * where + LZ :: Length '[] + LS :: Length xs -> Length (x ': xs) + +type family (xs :: [a]) ++ (ys :: [a]) :: [a] +type instance '[] ++ ys = ys +type instance (x ': xs) ++ ys = x ': (xs ++ ys) +infixr 5 ++ + +-- | Convert an expression typed in one context to one typed in a larger +-- context. Operationally, this amounts to de Bruijn index shifting. +-- As a proposition, this is the weakening lemma. +shift :: forall ts2 t ty. Exp ts2 ty -> Exp (t ': ts2) ty +shift = go LZ + where + go :: forall ts1 ty. Length ts1 -> Exp (ts1 ++ ts2) ty -> Exp (ts1 ++ t ': ts2) ty + go l_ts1 (Var v) = Var (shift_elem l_ts1 v) + go l_ts1 (Lam body) = Lam (go (LS l_ts1) body) + go l_ts1 (App e1 e2) = App (go l_ts1 e1) (go l_ts1 e2) + go l_ts1 (Arith e1 op e2) = Arith (go l_ts1 e1) op (go l_ts1 e2) + go l_ts1 (Cond e1 e2 e3) = Cond (go l_ts1 e1) (go l_ts1 e2) (go l_ts1 e3) + go l_ts1 (Fix e) = Fix (go l_ts1 e) + go _ (IntE n) = IntE n + go _ (BoolE b) = BoolE b + + shift_elem :: Length ts1 -> Elem (ts1 ++ ts2) x + -> Elem (ts1 ++ t ': ts2) x + shift_elem LZ e = ES e + shift_elem (LS _) EZ = EZ + shift_elem (LS l) (ES e) = ES (shift_elem l e) + +-- | Substitute the first expression into the second. As a proposition, +-- this is the substitution lemma. +subst :: forall ts2 s t. + Exp ts2 s -> Exp (s ': ts2) t -> Exp ts2 t +subst e = go LZ + where + go :: forall ts1 t. Length ts1 -> Exp (ts1 ++ s ': ts2) t -> Exp (ts1 ++ ts2) t + go len (Var v) = subst_var len v + go len (Lam body) = Lam (go (LS len) body) + go len (App e1 e2) = App (go len e1) (go len e2) + go len (Arith e1 op e2) = Arith (go len e1) op (go len e2) + go len (Cond e1 e2 e3) = Cond (go len e1) (go len e2) (go len e3) + go len (Fix e) = Fix (go len e) + go _ (IntE n) = IntE n + go _ (BoolE b) = BoolE b + + subst_var :: forall ts1 t. + Length ts1 -> Elem (ts1 ++ s ': ts2) t + -> Exp (ts1 ++ ts2) t + subst_var LZ EZ = e + subst_var LZ (ES v) = Var v + subst_var (LS _) EZ = Var EZ + subst_var (LS len) (ES v) = shift (subst_var len v) diff --git a/src/Language/Glambda/Statement.hs b/src/Language/Glambda/Statement.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Statement.hs @@ -0,0 +1,27 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Statement +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Defines the Glambda Statement type, which can either be a bare +-- expression or a global variable assignment. +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Statement ( Statement(..) ) where + +import Language.Glambda.Unchecked + +import Text.PrettyPrint.ANSI.Leijen + +-- | A statement can either be a bare expression, which will be evaluated, +-- or an assignment to a global variable. +data Statement = BareExp UExp + | NewGlobal String UExp + +instance Pretty Statement where + pretty (BareExp exp) = pretty exp + pretty (NewGlobal v exp) = text v <+> char '=' <+> pretty exp diff --git a/src/Language/Glambda/Token.hs b/src/Language/Glambda/Token.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Token.hs @@ -0,0 +1,199 @@ +{-# LANGUAGE TupleSections, GADTs, StandaloneDeriving, DataKinds #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Token +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Defines a lexical token +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Token ( + + -- * Arithmetic operators + ArithOp(..), UArithOp(..), eqArithOp, + + -- ** Unchecked synonyms for arithmetic operators + uPlus, uMinus, uTimes, uDivide, uMod, uLess, uLessE, + uGreater, uGreaterE, uEquals, + + -- * Tokens + Token(..), LToken(..), unLoc, unArithOp, unInt, unBool, unName + ) where + +import Language.Glambda.Type +import Language.Glambda.Util + +import Text.PrettyPrint.ANSI.Leijen as Pretty +import Text.Parsec.Pos ( SourcePos ) + +import Data.List as List + +-- | An @ArithOp ty@ is an operator on numbers that produces a result +-- of type @ty@ +data ArithOp ty where + Plus, Minus, Times, Divide, Mod :: ArithOp Int + Less, LessE, Greater, GreaterE, Equals :: ArithOp Bool + +-- | 'UArithOp' ("unchecked 'ArithOp'") is an existential package for +-- an 'ArithOp' +data UArithOp where + UArithOp :: ITy ty => ArithOp ty -> UArithOp + +uPlus, uMinus, uTimes, uDivide, uMod, uLess, uLessE, uGreater, + uGreaterE, uEquals :: UArithOp +uPlus = UArithOp Plus +uMinus = UArithOp Minus +uTimes = UArithOp Times +uDivide = UArithOp Divide +uMod = UArithOp Mod +uLess = UArithOp Less +uLessE = UArithOp LessE +uGreater = UArithOp Greater +uGreaterE = UArithOp GreaterE +uEquals = UArithOp Equals + +-- | Compare two 'ArithOp's (potentially of different types) for equality +eqArithOp :: ArithOp ty1 -> ArithOp ty2 -> Bool +eqArithOp Plus Plus = True +eqArithOp Minus Minus = True +eqArithOp Times Times = True +eqArithOp Divide Divide = True +eqArithOp Mod Mod = True +eqArithOp Less Less = True +eqArithOp LessE LessE = True +eqArithOp Greater Greater = True +eqArithOp GreaterE GreaterE = True +eqArithOp Equals Equals = True +eqArithOp _ _ = False + +instance Eq (ArithOp ty) where + (==) = eqArithOp + +instance Eq UArithOp where + UArithOp op1 == UArithOp op2 = op1 `eqArithOp` op2 + +-- | A lexed token +data Token + = LParen + | RParen + | Lambda + | Dot + | Arrow + | Colon + | ArithOp UArithOp + | Int Int + | Bool Bool + | If + | Then + | Else + | FixT + | Assign + | Semi + | Name String + deriving Eq + +-- | Perhaps extract a 'UArithOp' +unArithOp :: Token -> Maybe UArithOp +unArithOp (ArithOp x) = Just x +unArithOp _ = Nothing + +-- | Perhaps extract an 'Int' +unInt :: Token -> Maybe Int +unInt (Int x) = Just x +unInt _ = Nothing + +-- | Perhaps extract an 'Bool' +unBool :: Token -> Maybe Bool +unBool (Bool x) = Just x +unBool _ = Nothing + +-- | Perhaps extract a 'String' +unName :: Token -> Maybe String +unName (Name x) = Just x +unName _ = Nothing + +-- | A lexed token with location information attached +data LToken = L SourcePos Token + +-- | Remove location information from an 'LToken' +unLoc :: LToken -> Token +unLoc (L _ t) = t + +instance Pretty (ArithOp ty) where + pretty Plus = char '+' + pretty Minus = char '-' + pretty Times = char '*' + pretty Divide = char '/' + pretty Mod = char '%' + pretty Less = char '<' + pretty LessE = text "<=" + pretty Greater = char '>' + pretty GreaterE = text ">=" + pretty Equals = text "==" + +instance Show (ArithOp ty) where + show = render . pretty + +instance Pretty UArithOp where + pretty (UArithOp op) = pretty op + +instance Show UArithOp where + show = render . pretty + +instance Pretty Token where + pretty = getDoc . printingInfo + prettyList = printTogether . List.map printingInfo + +instance Show Token where + show = render . pretty + +instance Pretty LToken where + pretty = pretty . unLoc + prettyList = prettyList . List.map unLoc + +instance Show LToken where + show = render . pretty + +type PrintingInfo = (Doc, Bool, Bool) + -- the bools say whether or not to include a space before or a space after + +alone :: Doc -> PrintingInfo +alone = (, True, True) + +getDoc :: PrintingInfo -> Doc +getDoc (doc, _, _) = doc + +printingInfo :: Token -> PrintingInfo +printingInfo LParen = (char '(', True, False) +printingInfo RParen = (char ')', False, True) +printingInfo Lambda = (char '\\', True, False) +printingInfo Dot = (char '.', False, True) +printingInfo Arrow = alone $ text "->" +printingInfo Colon = (char ':', False, False) +printingInfo (ArithOp a) = alone $ pretty a +printingInfo (Int i) = alone $ int i +printingInfo (Bool True) = alone $ text "true" +printingInfo (Bool False) = alone $ text "false" +printingInfo If = alone $ text "if" +printingInfo Then = alone $ text "then" +printingInfo Else = alone $ text "else" +printingInfo FixT = alone $ text "fix" +printingInfo Assign = alone $ text "=" +printingInfo Semi = (char ';', False, True) +printingInfo (Name t) = alone $ text t + +printTogether :: [PrintingInfo] -> Doc +printTogether [] = Pretty.empty +printTogether pis = getDoc $ List.foldl1 combine pis + where + combine (doc1, before_space, inner_space1) (doc2, inner_space2, after_space) + | inner_space1 && inner_space2 + = (doc1 <+> doc2, before_space, after_space) + + | otherwise + = (doc1 <> doc2, before_space, after_space) diff --git a/src/Language/Glambda/Type.hs b/src/Language/Glambda/Type.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Type.hs @@ -0,0 +1,119 @@ +{-# LANGUAGE DataKinds, TypeOperators, PolyKinds, + GADTs, RankNTypes, FlexibleInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Type +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Defines types +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Type ( + -- * Glambda types to be used in Haskell terms + Ty(..), readTyCon, + + -- * Glambda types to be used in Haskell types + STy(..), SCtx(..), ITy(..), + emptyContext, refineTy, unrefineTy, eqSTy, + ) where + +import Language.Glambda.Util + +import Text.PrettyPrint.ANSI.Leijen + +-- | Representation of a glambda type +data Ty + = Arr Ty Ty -- ^ A function type + | IntTy + | BoolTy + deriving Eq +infixr 1 `Arr` + +-- | Perhaps convert a string representation of a base type into a 'Ty' +readTyCon :: String -> Maybe Ty +readTyCon "Int" = Just IntTy +readTyCon "Bool" = Just BoolTy +readTyCon _ = Nothing + +-- | Singleton for a glambda type +data STy :: * -> * where + SArr :: STy arg -> STy res -> STy (arg -> res) + SIntTy :: STy Int + SBoolTy :: STy Bool +infixr 1 `SArr` + +-- | An implicit 'STy', wrapped up in a class constraint +class ITy ty where + sty :: STy ty + +instance (ITy arg, ITy res) => ITy (arg -> res) where + sty = sty `SArr` sty +instance ITy Int where + sty = SIntTy +instance ITy Bool where + sty = SBoolTy + +-- | Singleton for a typing context +data SCtx :: [*] -> * where + SNil :: SCtx '[] + SCons :: STy h -> SCtx t -> SCtx (h ': t) +infixr 5 `SCons` + +-- | The singleton for the empty context +emptyContext :: SCtx '[] +emptyContext = SNil + +-- | Convert a 'Ty' into an 'STy'. +refineTy :: Ty -> (forall ty. STy ty -> r) -> r +refineTy (ty1 `Arr` ty2) k + = refineTy ty1 $ \sty1 -> + refineTy ty2 $ \sty2 -> + k (sty1 `SArr` sty2) +refineTy IntTy k = k SIntTy +refineTy BoolTy k = k SBoolTy + +-- | Convert an 'STy' into a 'Ty' +unrefineTy :: STy ty -> Ty +unrefineTy (arg `SArr` res) = unrefineTy arg `Arr` unrefineTy res +unrefineTy SIntTy = IntTy +unrefineTy SBoolTy = BoolTy + +-- | Compare two 'STy's for equality. +eqSTy :: STy ty1 -> STy ty2 -> Maybe (ty1 :~: ty2) +eqSTy (s1 `SArr` t1) (s2 `SArr` t2) + | Just Refl <- s1 `eqSTy` s2 + , Just Refl <- t1 `eqSTy` t2 + = Just Refl +eqSTy SIntTy SIntTy = Just Refl +eqSTy SBoolTy SBoolTy = Just Refl +eqSTy _ _ = Nothing + +----------------------------------------- +-- Pretty-printing + +instance Pretty Ty where + pretty = pretty_ty topPrec + +instance Show Ty where + show = render . pretty + +instance Pretty (STy ty) where + pretty = pretty . unrefineTy + +arrowLeftPrec, arrowRightPrec, arrowPrec :: Prec +arrowLeftPrec = 5 +arrowRightPrec = 4.9 +arrowPrec = 5 + +pretty_ty :: Prec -> Ty -> Doc +pretty_ty prec (Arr arg res) = maybeParens (prec >= arrowPrec) $ + hsep [ pretty_ty arrowLeftPrec arg + , text "->" + , pretty_ty arrowRightPrec res ] +pretty_ty _ IntTy = text "Int" +pretty_ty _ BoolTy = text "Bool" diff --git a/src/Language/Glambda/Unchecked.hs b/src/Language/Glambda/Unchecked.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Unchecked.hs @@ -0,0 +1,50 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Unchecked +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Defines the AST for un-type-checked expressions +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Unchecked ( UExp(..) ) where + +import Language.Glambda.Pretty +import Language.Glambda.Type +import Language.Glambda.Token +import Language.Glambda.Util + +import Text.PrettyPrint.ANSI.Leijen + +-- | Unchecked expression +data UExp + = UVar Int -- ^ de Bruijn index for a variable + | UGlobal String + | ULam Ty UExp + | UApp UExp UExp + | UArith UExp UArithOp UExp + | UCond UExp UExp UExp + | UFix UExp + | UIntE Int + | UBoolE Bool + +instance Pretty UExp where + pretty = defaultPretty + +instance PrettyExp UExp where + prettyExp = pretty_exp + +pretty_exp :: Coloring -> Prec -> UExp -> Doc +pretty_exp c _ (UVar n) = prettyVar c n +pretty_exp _ _ (UGlobal n) = text n +pretty_exp c prec (ULam ty body) = prettyLam c prec (Just ty) body +pretty_exp c prec (UApp e1 e2) = prettyApp c prec e1 e2 +pretty_exp c prec (UArith e1 (UArithOp op) e2) = prettyArith c prec e1 op e2 +pretty_exp c prec (UCond e1 e2 e3) = prettyIf c prec e1 e2 e3 +pretty_exp c prec (UFix body) = prettyFix c prec body +pretty_exp _ _ (UIntE n) = int n +pretty_exp _ _ (UBoolE True) = text "true" +pretty_exp _ _ (UBoolE False) = text "false" diff --git a/src/Language/Glambda/Util.hs b/src/Language/Glambda/Util.hs new file mode 100644 --- /dev/null +++ b/src/Language/Glambda/Util.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE GADTs, PolyKinds, TypeOperators, CPP #-} +{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-warnings-deprecations #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Language.Glambda.Util +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Utility exports (and re-exports) for glambda. This module is meant to +-- be internal -- do not import it if you are not part of the glambda +-- package! +-- +---------------------------------------------------------------------------- + +module Language.Glambda.Util ( + render, toSimpleDoc, maybeParens, ($$), + Prec, topPrec, + stripWhitespace, nthDefault, + (:~:)(..), ignore + ) where + +import Text.Parsec +import Text.PrettyPrint.ANSI.Leijen as Pretty + +import Data.Char +import Data.List + +#if __GLASGOW_HASKELL__ < 709 +import Data.Functor +#endif + +#if __GLASGOW_HASKELL__ >= 707 +import Data.Type.Equality +#else +data a :~: b where + Refl :: a :~: a +#endif + +-- | Like 'Data.Functor.void' +ignore :: Functor f => f a -> f () +ignore = (() <$) + +instance Pretty ParseError where + pretty = text . show + +-- | More perspicuous synonym for operator precedence +type Prec = Rational + +-- | Precedence for top-level printing +topPrec :: Prec +topPrec = 0 + +-- | Convert a 'Doc' to a 'String' +render :: Doc -> String +render = flip displayS "" . toSimpleDoc + +-- | Convert a 'Doc' to a 'SimpleDoc' for further rendering +toSimpleDoc :: Doc -> SimpleDoc +toSimpleDoc = renderPretty 1.0 78 + +-- | Enclose a 'Doc' in parens if the flag is 'True' +maybeParens :: Bool -> Doc -> Doc +maybeParens True = parens +maybeParens False = id + +-- | Synonym for 'Pretty.<$>' +($$) :: Doc -> Doc -> Doc +($$) = (Pretty.<$>) + +-- | (Inefficiently) strips whitespace from a string +stripWhitespace :: String -> String +stripWhitespace = dropWhile isSpace . dropWhileEnd isSpace + +-- | Pluck out the nth item from a list, or use a default if the list +-- is too short +nthDefault :: a -> Int -> [a] -> a +nthDefault _ 0 (x:_) = x +nthDefault def n (_:xs) = nthDefault def (n-1) xs +nthDefault def _ [] = def diff --git a/tests/Tests/Check.hs b/tests/Tests/Check.hs new file mode 100644 --- /dev/null +++ b/tests/Tests/Check.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE GADTs #-} + +module Tests.Check where + +import Prelude hiding ( lex ) + +import Language.Glambda.Exp +import Language.Glambda.Parse +import Language.Glambda.Lex +import Language.Glambda.Check +import Language.Glambda.Type +import Language.Glambda.Eval +import Language.Glambda.Globals +import Language.Glambda.Util + +import Control.Error +import Control.Monad.Reader + +import Text.PrettyPrint.ANSI.Leijen + +import Data.List as List +import Control.Arrow as Arrow + +import Test.Tasty +import Test.Tasty.HUnit + +checkTestCases :: [(String, Maybe (String, Ty, String))] +checkTestCases = [ ("1", Just ("1", IntTy, "1")) + , ("1 + true", Nothing) + , ("(\\x:Int.x) 5", + Just ("(λ#. #0) 5", IntTy, "5")) + , ("(\\x:Int.\\y:Int->Int.y x) 4 (\\z:Int.z*2)", + Just ("(λ#. λ#. #0 #1) 4 (λ#. #0 * 2)", + IntTy, "8")) + , ("1 + 2 * 3 / 4 - 10 % 3", + Just ("1 + 2 * 3 / 4 - 10 % 3", IntTy, "1")) + , ("if true then 1 else false", Nothing) + , ("if 3 - 1 == 2 then \\x:Int.x else \\x:Int.3", + Just ("if 3 - 1 == 2 then λ#. #0 else λ#. 3", + IntTy `Arr` IntTy, "λ#. #0")) + , ("1 > 2", Just ("1 > 2", BoolTy, "false")) + , ("2 > 1", Just ("2 > 1", BoolTy, "true")) + , ("1 > 1", Just ("1 > 1", BoolTy, "false")) + , ("1 >= 1", Just ("1 >= 1", BoolTy, "true")) + , ("1 < 2", Just ("1 < 2", BoolTy, "true")) + , ("1 < 1", Just ("1 < 1", BoolTy, "false")) + , ("1 <= 1", Just ("1 <= 1", BoolTy, "true")) + , ("id_int (id_int 5)", Just ("(λ#. #0) ((λ#. #0) 5)", IntTy, "5")) + ] + +checkTests :: TestTree +checkTests = testGroup "Typechecker" $ + List.map (\(expr_str, m_result) -> + testCase ("`" ++ expr_str ++ "'") $ + (case flip runReader id_globals $ runEitherT $ do + uexp <- hoistEither $ Arrow.left text $ parseExp =<< lex expr_str + check uexp $ \sty exp -> return $ + case m_result of + Just result + -> (render (plain $ pretty exp), unrefineTy sty, + render (plain $ prettyVal (eval exp) sty)) + @?= result + _ -> assertFailure "unexpected type-check success" + of + Left _ -> assertBool "unexpected failure" (isNothing m_result) + Right b -> b)) checkTestCases + +id_globals :: Globals +id_globals = extend "id_int" (SIntTy `SArr` SIntTy) (Lam (Var EZ)) emptyGlobals diff --git a/tests/Tests/Lex.hs b/tests/Tests/Lex.hs new file mode 100644 --- /dev/null +++ b/tests/Tests/Lex.hs @@ -0,0 +1,43 @@ +module Tests.Lex where + +import Language.Glambda.Lex +import Language.Glambda.Token +import Tests.Util + +import Prelude hiding ( lex ) + +import Data.List as List +import Control.Arrow as Arrow ( right ) + +lexTestCases :: [(String, [Token])] +lexTestCases = [ ("", []) + , (" ", []) + , (" {- hi -} \n ", []) + , (" {----} ", []) + , (" {- foo {- bar -} blah -}", []) + , (" {- foo {-- bar -}-}", []) + , ("{- blah ---}", []) + , ("{- froggle -} -- blah", []) + , ("x", [Name "x"]) + , ("(()", [LParen, LParen, RParen]) + , ("++--++", [ArithOp uPlus, ArithOp uPlus]) + , ("->->", [Arrow, Arrow]) + , ("45+332-89/1*3%xyz", [ Int 45, ArithOp uPlus, Int 332 + , ArithOp uMinus, Int 89, ArithOp uDivide + , Int 1, ArithOp uTimes, Int 3 + , ArithOp uMod, Name "xyz" ]) + , ("===", [ArithOp uEquals, Assign]) + , ("if x then y else z", [If, Name "x", Then, Name "y", Else, Name "z"]) + , ("ifs trues falsee true-", [ Name "ifs", Name "trues", Name "falsee" + , Bool True, ArithOp uMinus ]) + , (":\\", [Colon, Lambda]) + , (">>==<===<", [ ArithOp uGreater, ArithOp uGreaterE, Assign + , ArithOp uLessE, ArithOp uEquals, ArithOp uLess ]) + ] + +lexTests :: TestTree +lexTests = testGroup "Lexer" $ + List.map (\(str, out) -> testCase ("`" ++ str ++ "'") $ + Arrow.right (List.map unLoc) + (lex str) @?= Right out) + lexTestCases diff --git a/tests/Tests/Main.hs b/tests/Tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Tests/Main.hs @@ -0,0 +1,15 @@ +-- Main testing module + +module Tests.Main where + +import Test.Tasty + +import Tests.Lex +import Tests.Parse +import Tests.Check + +allTests :: TestTree +allTests = testGroup "Top" [lexTests, parseTests, checkTests] + +main :: IO () +main = defaultMain allTests diff --git a/tests/Tests/Parse.hs b/tests/Tests/Parse.hs new file mode 100644 --- /dev/null +++ b/tests/Tests/Parse.hs @@ -0,0 +1,45 @@ +module Tests.Parse where + +import Language.Glambda.Lex +import Language.Glambda.Parse +import Language.Glambda.Util +import Tests.Util + +import Prelude hiding ( lex ) + +import Text.PrettyPrint.ANSI.Leijen + +import Data.List as List + +parseTestCases :: [(String, String)] +parseTestCases = [ ("\\x:Int.x", "λ#:Int. #0") + , ("\\x:Int.\\y:Int.x", "λ#:Int. λ#:Int. #1") + , ("\\x:Int.\\x:Int.x", "λ#:Int. λ#:Int. #0") + , ("1 + 2 + 3", "1 + 2 + 3") + , ("1 + 2 * 4 % 5", "1 + 2 * 4 % 5") + , ("if \\x:Int.x then 4 else (\\x:Int.x) (\\y:Int.y)", + "if λ#:Int. #0 then 4 else (λ#:Int. #0) (λ#:Int. #0)") + , ("true true true", "true true true") + , ("true false (\\x:Int.x)", "true false (λ#:Int. #0)") + , ("\\x:Int->Int.\\y:Int.x y", "λ#:Int -> Int. λ#:Int. #1 #0") + , ("if 3 - 1 == 2 then \\x:Int.x else \\x:Int.3", + "if 3 - 1 == 2 then λ#:Int. #0 else λ#:Int. 3") + , ("\\x:Int.y", "λ#:Int. y") + ] + +parserFailTestCases :: [String] +parserFailTestCases = [ " {- " + , "{-{- -}" ] + +parseTests :: TestTree +parseTests = testGroup "Parser" + [ testGroup "Success" $ + List.map (\(str, out) -> testCase ("`" ++ str ++ "'") $ + (render $ plain $ pretty (parseExp =<< lex str)) @?= + ("Right " ++ out)) + parseTestCases + , testGroup "Failure" $ + List.map (\str -> testCase ("`" ++ str ++ "'") $ + (case parseExp =<< lex str of Left _ -> True; _ -> False) @? + "parse erroneously successful") + parserFailTestCases ] diff --git a/tests/Tests/Util.hs b/tests/Tests/Util.hs new file mode 100644 --- /dev/null +++ b/tests/Tests/Util.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Tests.Util +-- Copyright : (C) 2015 Richard Eisenberg +-- License : BSD-style (see LICENSE) +-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) +-- Stability : experimental +-- +-- Utility definnitions for testing glambda +-- +---------------------------------------------------------------------------- + +module Tests.Util ( + module Test.Tasty, + testCase, + (@?=), (@=?), (@?) ) + where + +import Language.Glambda.Util + +import Test.Tasty +import Test.Tasty.HUnit ( testCase, (@?), Assertion ) + +import Text.PrettyPrint.ANSI.Leijen + +import Text.Parsec ( ParseError ) + +import Data.Function +import Language.Haskell.TH +import Control.Monad + +prettyError :: Pretty a => a -> a -> String +prettyError exp act = (render $ text "Expected" <+> squotes (pretty exp) <> semi <+> + text "got" <+> squotes (pretty act)) + +(@?=) :: (Eq a, Pretty a) => a -> a -> Assertion +act @?= exp = (act == exp) @? prettyError exp act + +(@=?) :: (Eq a, Pretty a) => a -> a -> Assertion +exp @=? act = (act == exp) @? prettyError exp act + +$( do decs <- reifyInstances ''Eq [ConT ''ParseError] + case decs of -- GHC 7.6 eagerly typechecks the instance, sometimes + -- reporting a duplicate. Urgh. So we can't quote it. + [] -> liftM (:[]) $ + instanceD (return []) (appT (conT ''Eq) (conT ''ParseError)) + [ valD (varP '(==)) (normalB [| (==) `on` show |]) [] ] + _ -> return [] ) + +instance (Pretty a, Pretty b) => Pretty (Either a b) where + pretty (Left x) = text "Left" <+> pretty x + pretty (Right x) = text "Right" <+> pretty x