1{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE FlexibleContexts #-}
3{-# LANGUAGE FlexibleInstances #-}
4{-# LANGUAGE GADTs #-}
5{-# LANGUAGE GeneralizedNewtypeDeriving #-}
6{-# LANGUAGE LambdaCase #-}
7{-# LANGUAGE MultiParamTypeClasses #-}
8{-# LANGUAGE ScopedTypeVariables #-}
9{-# LANGUAGE UnicodeSyntax #-}
10{-# LANGUAGE ViewPatterns #-}
11{-# LANGUAGE Arrows          #-}
12
13module Tutorial where
14
15-- import Abt.Class
16-- import Abt.Types
17-- import Abt.Concrete.LocallyNameless
18
19import Control.Applicative
20import Control.Monad.Trans.State.Strict
21import Control.Monad.Trans.Maybe
22import Control.Monad.Trans.Except
23-- import Data.Vinyl
24import Prelude hiding (pi)
25
26-- | We'll start off with a monad in which to manipulate ABTs; we'll need some
27-- state for fresh variable generation.
28--
29newtype M α
30  = M
31  { _M ∷ State Int α
32  } deriving (Functor, Applicative, Monad)
33
34-- | We'll run an ABT computation by starting the variable counter at @0@.
35--
36runM ∷ M α → α
37runM (M m) = evalState m 0
38
39-- | Check out the source to see fresh variable generation.
40--
41instance MonadVar Var M where
42  fresh = M $ do
43    n ← get
44    let n' = n + 1
45    put n'
46    return $ Var Nothing n'
47
48  named a = do
49    v ← fresh
50    return $ v { _varName = Just a }
51
52-- | Next, we'll define the operators for a tiny lambda calculus as a datatype
53-- indexed by arities.
54--
55data Lang ns where
56  LAM ∷ Lang '[S Z]
57  APP ∷ Lang '[Z, Z]
58  PI ∷ Lang '[Z, S Z]
59  UNIT ∷ Lang '[]
60  AX ∷ Lang '[]
61
62instance Show1 Lang where
63  show1 = \case
64    LAM → "lam"
65    APP → "ap"
66    PI → "pi"
67    UNIT → "unit"
68    AX → "<>"
69
70instance HEq1 Lang where
71  heq1 LAM LAM = Just Refl
72  heq1 APP APP = Just Refl
73  heq1 PI PI = Just Refl
74  heq1 UNIT UNIT = Just Refl
75  heq1 AX AX = Just Refl
76  heq1 _ _ = Nothing
77
78lam ∷ Tm Lang (S Z) → Tm0 Lang
79lam e = LAM $$ e :& RNil
80
81app ∷ Tm0 Lang → Tm0 Lang → Tm0 Lang
82app m n = APP $$ m :& n :& RNil
83
84ax ∷ Tm0 Lang
85ax = AX $$ RNil
86
87unit ∷ Tm0 Lang
88unit = UNIT $$ RNil
89
90pi ∷ Tm0 Lang → Tm Lang (S Z) → Tm0 Lang
91pi α xβ = PI $$ α :& xβ :& RNil
92
93-- | A monad transformer for small step operational semantics.
94--
95newtype StepT m α
96  = StepT
97  { runStepT ∷ MaybeT m α
98  } deriving (Monad, Functor, Applicative, Alternative)
99
100-- | To indicate that a term is in normal form.
101--
102stepsExhausted
103  ∷ Applicative m
104  ⇒ StepT m α
105stepsExhausted = StepT . MaybeT $ pure Nothing
106
107instance MonadVar Var m ⇒ MonadVar Var (StepT m) where
108  fresh = StepT . MaybeT $ Just <$> fresh
109  named str = StepT . MaybeT $ Just <$> named str
110
111-- | A single evaluation step.
112--
113step
114  ∷ Tm0 Lang
115  → StepT M (Tm0 Lang)
116step tm =
117  out tm >>= \case
118    APP :$ m :& n :& RNil →
119      out m >>= \case
120        LAM :$ xe :& RNil → xe // n
121        _ → app <$> step m <*> pure n <|> app <$> pure m <*> step n
122    PI :$ α :& xβ :& RNil → pi <$> step α <*> pure xβ
123    _ → stepsExhausted
124
125-- | The reflexive-transitive closure of a small-step operational semantics.
126--
127star
128  ∷ Monad m
129  ⇒ (α → StepT m α)
130  → (α → m α)
131star f a =
132  runMaybeT (runStepT $ f a) >>=
133    return a `maybe` star f
134
135-- | Evaluate a term to normal form
136--
137eval ∷ Tm0 Lang → Tm0 Lang
138eval = runM . star step
139
140newtype JudgeT m α
141  = JudgeT
142  { runJudgeT ∷ ExceptT String m α
143  } deriving (Monad, Functor, Applicative, Alternative)
144
145instance MonadVar Var m ⇒ MonadVar Var (JudgeT m) where
146  fresh = JudgeT . ExceptT $ Right <$> fresh
147  named str = JudgeT . ExceptT $ Right <$> named str
148
149type Ctx = [(Var, Tm0 Lang)]
150
151raise ∷ Monad m ⇒ String → JudgeT m α
152raise = JudgeT . ExceptT . return . Left
153
154checkTy
155  ∷ Ctx
156  → Tm0 Lang
157  → Tm0 Lang
158  → JudgeT M ()
159checkTy g tm ty = do
160  let ntm = eval tm
161      nty = eval ty
162  (,) <$> out ntm <*> out nty >>= \case
163    (LAM :$ xe :& RNil, PI :$ α :& yβ :& RNil) → do
164      z ← fresh
165      ez ← xe // var z
166      βz ← yβ // var z
167      checkTy ((z,α):g) ez βz
168    (AX :$ RNil, UNIT :$ RNil) → return ()
169    _ → do
170      ty' ← inferTy g tm
171      if ty' === nty
172        then return ()
173        else raise "Type error"
174
175inferTy
176  ∷ Ctx
177  → Tm0 Lang
178  → JudgeT M (Tm0 Lang)
179inferTy g tm = do
180  out (eval tm) >>= \case
181    V v | Just (eval → ty) ← lookup v g → return ty
182        | otherwise → raise "Ill-scoped variable"
183    APP :$ m :& n :& RNil → do
184      inferTy g m >>= out >>= \case
185        PI :$ α :& xβ :& RNil → do
186          checkTy g n α
187          eval <$> xβ // n
188        _ → raise "Expected pi type for lambda abstraction"
189    _ → raise "Only infer neutral terms"
190
191-- | @λx.x@
192--
193identityTm ∷ M (Tm0 Lang)
194identityTm = do
195  x ← fresh
196  return $ lam (x \\ var x)
197
198-- | @(λx.x)(λx.x)@
199--
200appTm ∷ M (Tm0 Lang)
201appTm = do
202  tm ← identityTm
203  return $ app tm tm
204
205-- | A demonstration of evaluating (and pretty-printing). Output:
206--
207-- @
208-- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@4.\@4]
209-- @
210--
211main ∷ IO ()
212main = do
213  -- Try out the type checker
214  either fail print . runM . runExceptT . runJudgeT $ do
215    x ← fresh
216    checkTy [] (lam (x \\ var x)) (pi unit (x \\ unit))
217
218  print . runM $ do
219    mm ← appTm
220    mmStr ← toString mm
221    mmStr' ← toString $ eval mm
222    return $ mmStr ++ " ~>* " ++ mmStr'
223
224doMap ∷ FilePath → IOSArrow XmlTree TiledMap
225doMap mapPath = proc m → do
226    mapWidth       ← getAttrR "width"      ⤙ m
227    returnA -< baz
228
229-- ^ An opaque ESD handle for recording data from the soundcard via ESD.
230data Recorder fr ch (r ∷ ★ → ★)
231    = Recorder {
232        reRate   ∷ !Int
233      , reHandle ∷ !Handle
234      , reCloseH ∷ !(FinalizerHandle r)
235      }
236
237-- from ghc-prim
238
239-- | A backward-compatible (pre-GHC 8.0) synonym for 'Type'
240-- type * = TYPE 'PtrRepLifted
241
242-- | A unicode backward-compatible (pre-GHC 8.0) synonym for 'Type'
243-- type ★ = TYPE 'PtrRepLifted
244