summaryrefslogtreecommitdiff
path: root/tests/examples/pre-ghc86/UnicodeSyntax.hs
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examples/pre-ghc86/UnicodeSyntax.hs')
-rw-r--r--tests/examples/pre-ghc86/UnicodeSyntax.hs243
1 files changed, 243 insertions, 0 deletions
diff --git a/tests/examples/pre-ghc86/UnicodeSyntax.hs b/tests/examples/pre-ghc86/UnicodeSyntax.hs
new file mode 100644
index 0000000..9e4cc50
--- /dev/null
+++ b/tests/examples/pre-ghc86/UnicodeSyntax.hs
@@ -0,0 +1,243 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE Arrows #-}
+
+module Tutorial where
+
+-- import Abt.Class
+-- import Abt.Types
+-- import Abt.Concrete.LocallyNameless
+
+import Control.Applicative
+import Control.Monad.Trans.State.Strict
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Except
+-- import Data.Vinyl
+import Prelude hiding (pi)
+
+-- | We'll start off with a monad in which to manipulate ABTs; we'll need some
+-- state for fresh variable generation.
+--
+newtype M α
+ = M
+ { _M ∷ State Int α
+ } deriving (Functor, Applicative, Monad)
+
+-- | We'll run an ABT computation by starting the variable counter at @0@.
+--
+runM ∷ M α → α
+runM (M m) = evalState m 0
+
+-- | Check out the source to see fresh variable generation.
+--
+instance MonadVar Var M where
+ fresh = M $ do
+ n ← get
+ let n' = n + 1
+ put n'
+ return $ Var Nothing n'
+
+ named a = do
+ v ← fresh
+ return $ v { _varName = Just a }
+
+-- | Next, we'll define the operators for a tiny lambda calculus as a datatype
+-- indexed by arities.
+--
+data Lang ns where
+ LAM ∷ Lang '[S Z]
+ APP ∷ Lang '[Z, Z]
+ PI ∷ Lang '[Z, S Z]
+ UNIT ∷ Lang '[]
+ AX ∷ Lang '[]
+
+instance Show1 Lang where
+ show1 = \case
+ LAM → "lam"
+ APP → "ap"
+ PI → "pi"
+ UNIT → "unit"
+ AX → "<>"
+
+instance HEq1 Lang where
+ heq1 LAM LAM = Just Refl
+ heq1 APP APP = Just Refl
+ heq1 PI PI = Just Refl
+ heq1 UNIT UNIT = Just Refl
+ heq1 AX AX = Just Refl
+ heq1 _ _ = Nothing
+
+lam ∷ Tm Lang (S Z) → Tm0 Lang
+lam e = LAM $$ e :& RNil
+
+app ∷ Tm0 Lang → Tm0 Lang → Tm0 Lang
+app m n = APP $$ m :& n :& RNil
+
+ax ∷ Tm0 Lang
+ax = AX $$ RNil
+
+unit ∷ Tm0 Lang
+unit = UNIT $$ RNil
+
+pi ∷ Tm0 Lang → Tm Lang (S Z) → Tm0 Lang
+pi α xβ = PI $$ α :& xβ :& RNil
+
+-- | A monad transformer for small step operational semantics.
+--
+newtype StepT m α
+ = StepT
+ { runStepT ∷ MaybeT m α
+ } deriving (Monad, Functor, Applicative, Alternative)
+
+-- | To indicate that a term is in normal form.
+--
+stepsExhausted
+ ∷ Applicative m
+ ⇒ StepT m α
+stepsExhausted = StepT . MaybeT $ pure Nothing
+
+instance MonadVar Var m ⇒ MonadVar Var (StepT m) where
+ fresh = StepT . MaybeT $ Just <$> fresh
+ named str = StepT . MaybeT $ Just <$> named str
+
+-- | A single evaluation step.
+--
+step
+ ∷ Tm0 Lang
+ → StepT M (Tm0 Lang)
+step tm =
+ out tm >>= \case
+ APP :$ m :& n :& RNil →
+ out m >>= \case
+ LAM :$ xe :& RNil → xe // n
+ _ → app <$> step m <*> pure n <|> app <$> pure m <*> step n
+ PI :$ α :& xβ :& RNil → pi <$> step α <*> pure xβ
+ _ → stepsExhausted
+
+-- | The reflexive-transitive closure of a small-step operational semantics.
+--
+star
+ ∷ Monad m
+ ⇒ (α → StepT m α)
+ → (α → m α)
+star f a =
+ runMaybeT (runStepT $ f a) >>=
+ return a `maybe` star f
+
+-- | Evaluate a term to normal form
+--
+eval ∷ Tm0 Lang → Tm0 Lang
+eval = runM . star step
+
+newtype JudgeT m α
+ = JudgeT
+ { runJudgeT ∷ ExceptT String m α
+ } deriving (Monad, Functor, Applicative, Alternative)
+
+instance MonadVar Var m ⇒ MonadVar Var (JudgeT m) where
+ fresh = JudgeT . ExceptT $ Right <$> fresh
+ named str = JudgeT . ExceptT $ Right <$> named str
+
+type Ctx = [(Var, Tm0 Lang)]
+
+raise ∷ Monad m ⇒ String → JudgeT m α
+raise = JudgeT . ExceptT . return . Left
+
+checkTy
+ ∷ Ctx
+ → Tm0 Lang
+ → Tm0 Lang
+ → JudgeT M ()
+checkTy g tm ty = do
+ let ntm = eval tm
+ nty = eval ty
+ (,) <$> out ntm <*> out nty >>= \case
+ (LAM :$ xe :& RNil, PI :$ α :& yβ :& RNil) → do
+ z ← fresh
+ ez ← xe // var z
+ βz ← yβ // var z
+ checkTy ((z,α):g) ez βz
+ (AX :$ RNil, UNIT :$ RNil) → return ()
+ _ → do
+ ty' ← inferTy g tm
+ if ty' === nty
+ then return ()
+ else raise "Type error"
+
+inferTy
+ ∷ Ctx
+ → Tm0 Lang
+ → JudgeT M (Tm0 Lang)
+inferTy g tm = do
+ out (eval tm) >>= \case
+ V v | Just (eval → ty) ← lookup v g → return ty
+ | otherwise → raise "Ill-scoped variable"
+ APP :$ m :& n :& RNil → do
+ inferTy g m >>= out >>= \case
+ PI :$ α :& xβ :& RNil → do
+ checkTy g n α
+ eval <$> xβ // n
+ _ → raise "Expected pi type for lambda abstraction"
+ _ → raise "Only infer neutral terms"
+
+-- | @λx.x@
+--
+identityTm ∷ M (Tm0 Lang)
+identityTm = do
+ x ← fresh
+ return $ lam (x \\ var x)
+
+-- | @(λx.x)(λx.x)@
+--
+appTm ∷ M (Tm0 Lang)
+appTm = do
+ tm ← identityTm
+ return $ app tm tm
+
+-- | A demonstration of evaluating (and pretty-printing). Output:
+--
+-- @
+-- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@4.\@4]
+-- @
+--
+main ∷ IO ()
+main = do
+ -- Try out the type checker
+ either fail print . runM . runExceptT . runJudgeT $ do
+ x ← fresh
+ checkTy [] (lam (x \\ var x)) (pi unit (x \\ unit))
+
+ print . runM $ do
+ mm ← appTm
+ mmStr ← toString mm
+ mmStr' ← toString $ eval mm
+ return $ mmStr ++ " ~>* " ++ mmStr'
+
+doMap ∷ FilePath → IOSArrow XmlTree TiledMap
+doMap mapPath = proc m → do
+ mapWidth ← getAttrR "width" ⤙ m
+ returnA -< baz
+
+-- ^ An opaque ESD handle for recording data from the soundcard via ESD.
+data Recorder fr ch (r ∷ ★ → ★)
+ = Recorder {
+ reRate ∷ !Int
+ , reHandle ∷ !Handle
+ , reCloseH ∷ !(FinalizerHandle r)
+ }
+
+-- from ghc-prim
+
+-- | A backward-compatible (pre-GHC 8.0) synonym for 'Type'
+type * = TYPE 'PtrRepLifted
+
+-- | A unicode backward-compatible (pre-GHC 8.0) synonym for 'Type'
+type ★ = TYPE 'PtrRepLifted