glambda (empty) → 1.0
raw patch · 26 files changed
+2274/−0 lines, 26 filesdep +ansi-wl-pprintdep +basedep +containerssetup-changed
Dependencies added: ansi-wl-pprint, base, containers, directory, errors, glambda, haskeline, mtl, parsec, tasty, tasty-hunit, template-haskell
Files
- CHANGES.md +7/−0
- LICENSE +27/−0
- README.md +186/−0
- Setup.hs +2/−0
- glambda.cabal +87/−0
- main/Main.hs +6/−0
- src/Language/Glambda/Check.hs +141/−0
- src/Language/Glambda/Eval.hs +86/−0
- src/Language/Glambda/Exp.hs +122/−0
- src/Language/Glambda/Globals.hs +57/−0
- src/Language/Glambda/Lex.hs +134/−0
- src/Language/Glambda/Monad.hs +108/−0
- src/Language/Glambda/Parse.hs +178/−0
- src/Language/Glambda/Pretty.hs +127/−0
- src/Language/Glambda/Repl.hs +225/−0
- src/Language/Glambda/Shift.hs +77/−0
- src/Language/Glambda/Statement.hs +27/−0
- src/Language/Glambda/Token.hs +199/−0
- src/Language/Glambda/Type.hs +119/−0
- src/Language/Glambda/Unchecked.hs +50/−0
- src/Language/Glambda/Util.hs +82/−0
- tests/Tests/Check.hs +69/−0
- tests/Tests/Lex.hs +43/−0
- tests/Tests/Main.hs +15/−0
- tests/Tests/Parse.hs +45/−0
- tests/Tests/Util.hs +55/−0
+ CHANGES.md view
@@ -0,0 +1,7 @@+Release notes for glambda+=========================++1.0+---++Initial release.
+ LICENSE view
@@ -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.
+ README.md view
@@ -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 <boolean expression> then <exp> else <exp>`.++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 `<name> = <expression>`.+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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ glambda.cabal view
@@ -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 <eir@cis.upenn.edu>+maintainer: Richard Eisenberg <eir@cis.upenn.edu>+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
+ main/Main.hs view
@@ -0,0 +1,6 @@+module Main where++import qualified Language.Glambda.Repl as Repl ( main )++main :: IO ()+main = Repl.main
+ src/Language/Glambda/Check.hs view
@@ -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
+ src/Language/Glambda/Eval.hs view
@@ -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)
+ src/Language/Glambda/Exp.hs view
@@ -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"
+ src/Language/Glambda/Globals.hs view
@@ -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)
+ src/Language/Glambda/Lex.hs view
@@ -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 '_')))
+ src/Language/Glambda/Monad.hs view
@@ -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
+ src/Language/Glambda/Parse.hs view
@@ -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
+ src/Language/Glambda/Pretty.hs view
@@ -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
+ src/Language/Glambda/Repl.hs view
@@ -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))
+ src/Language/Glambda/Shift.hs view
@@ -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)
+ src/Language/Glambda/Statement.hs view
@@ -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
+ src/Language/Glambda/Token.hs view
@@ -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)
+ src/Language/Glambda/Type.hs view
@@ -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"
+ src/Language/Glambda/Unchecked.hs view
@@ -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"
+ src/Language/Glambda/Util.hs view
@@ -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
+ tests/Tests/Check.hs view
@@ -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
+ tests/Tests/Lex.hs view
@@ -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
+ tests/Tests/Main.hs view
@@ -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
+ tests/Tests/Parse.hs view
@@ -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 ]
+ tests/Tests/Util.hs view
@@ -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