Syntax.hs 4.58 KB
Newer Older
Sven Keidel's avatar
Sven Keidel committed
1
{-# LANGUAGE TupleSections #-}
2 3
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
Sven Keidel's avatar
Sven Keidel committed
4
{-# LANGUAGE FlexibleContexts #-}
Sven Keidel's avatar
Sven Keidel committed
5
{-# LANGUAGE MultiParamTypeClasses #-}
Sven Keidel's avatar
Sven Keidel committed
6
module Syntax where
Jente Hidskes's avatar
Jente Hidskes committed
7

8 9 10 11 12 13
import           Data.Text(Text,unpack)
import           Data.Hashable
import           Data.Label
import           Data.String
import           Data.Lens (Prism')
import qualified Data.Lens as L
Sven Keidel's avatar
Sven Keidel committed
14 15 16 17
import           Data.HashMap.Lazy(HashMap)
import qualified Data.HashMap.Lazy as M
import           Data.HashSet(HashSet)
import qualified Data.HashSet as H
Jente Hidskes's avatar
Jente Hidskes committed
18

19 20
import Control.Monad.State

Sven Keidel's avatar
Sven Keidel committed
21 22 23 24
-- | Expressions of PCF. Each expression has a label, with which the
-- expression can be uniquely identified.
data Expr
  = Var Text Label
Sven Keidel's avatar
Sven Keidel committed
25 26
  | Lam [Text] Expr Label
  | App Expr [Expr] Label
Sven Keidel's avatar
Sven Keidel committed
27
  | Zero Label
Sven Keidel's avatar
Sven Keidel committed
28
  | Mult Expr Expr Label
Sven Keidel's avatar
Sven Keidel committed
29 30 31
  | Succ Expr Label
  | Pred Expr Label
  | IfZero Expr Expr Expr Label
Sven Keidel's avatar
Sven Keidel committed
32
  | Let [(Text,Expr)] Expr Label
33
  | Apply Expr Label
Sven Keidel's avatar
Sven Keidel committed
34 35 36 37
  deriving (Eq)

-- Smart constructors that build labeled PCF expressions.

38 39 40
var :: Text -> State Label Expr
var x = Var x <$> fresh

Sven Keidel's avatar
Sven Keidel committed
41 42
lam :: [Text] -> State Label Expr -> State Label Expr
lam xs e = Lam xs <$> e <*> fresh
43

Sven Keidel's avatar
Sven Keidel committed
44 45
app :: State Label Expr -> [State Label Expr] -> State Label Expr
app e1 e2 = App <$> e1 <*> sequence e2 <*> fresh
46 47 48 49 50 51 52 53 54 55

zero :: State Label Expr
zero = Zero <$> fresh

succ :: State Label Expr -> State Label Expr
succ e = Succ <$> e <*> fresh

pred :: State Label Expr -> State Label Expr
pred e = Pred <$> e <*> fresh

Sven Keidel's avatar
Sven Keidel committed
56 57 58
mult :: State Label Expr -> State Label Expr -> State Label Expr
mult e1 e2 = Mult <$> e1 <*> e2 <*> fresh

59 60 61
ifZero :: State Label Expr -> State Label Expr -> State Label Expr -> State Label Expr
ifZero e1 e2 e3 = IfZero <$> e1 <*> e2 <*> e3 <*> fresh

Sven Keidel's avatar
Sven Keidel committed
62 63
let_ :: [(Text, State Label Expr)] -> State Label Expr -> State Label Expr
let_ bnds body = Let <$> sequence [ (v,) <$> e | (v,e) <- bnds ] <*> body <*> fresh
64

65

Sven Keidel's avatar
Sven Keidel committed
66 67
instance Show Expr where
  showsPrec d e0 = case e0 of
68 69 70 71
    Var x _ -> showString (unpack x)
    Zero _ -> showString "zero"
    Succ e _ -> showParen (d > app_prec) $ showString "succ " . showsPrec (app_prec + 1) e
    Pred e _ -> showParen (d > app_prec) $ showString "pred " . showsPrec (app_prec + 1) e
Sven Keidel's avatar
Sven Keidel committed
72
    Let bnds e _ -> showParen (d > app_prec) $ showString "let " . shows bnds . showString " in " . showsPrec (app_prec + 1) e
73
    Apply e _ -> showParen (d > app_prec) $ showsPrec (app_prec + 1) e
74
    IfZero e1 e2 e3 _ -> showParen (d > app_prec)
Sven Keidel's avatar
Sven Keidel committed
75 76 77 78 79 80
      $ showString "ifZero "
      . showsPrec (app_prec + 1) e1
      . showString " "
      . showsPrec (app_prec + 1) e2
      . showString " "
      . showsPrec (app_prec + 1) e3
81
    App e1 e2 _ -> showParen (d > app_prec)
Sven Keidel's avatar
Sven Keidel committed
82 83 84
      $ showsPrec (app_prec + 1) e1
      . showString " "
      . showsPrec (app_prec + 1) e2
Sven Keidel's avatar
Sven Keidel committed
85 86 87 88
    Mult e1 e2 _ -> showParen (d > mult_prec)
      $ showsPrec (mult_prec + 1) e1
      . showString " * "
      . showsPrec (mult_prec + 1) e2
89
    Lam x e2 _ -> showParen (d > lam_prec)
Sven Keidel's avatar
Sven Keidel committed
90
      $ showString "λ"
Sven Keidel's avatar
Sven Keidel committed
91
      . showString (unwords (map unpack x))
Sven Keidel's avatar
Sven Keidel committed
92 93 94 95 96
      . showString ". "
      . shows e2
    where
      app_prec = 10
      lam_prec = 9
Sven Keidel's avatar
Sven Keidel committed
97
      mult_prec = 8
Sven Keidel's avatar
Sven Keidel committed
98

Sven Keidel's avatar
Sven Keidel committed
99
instance HasLabel Expr where
100 101 102 103 104 105 106
  label e = case e of
    Var _ l -> l
    Lam _ _ l -> l
    App _ _ l -> l
    Zero l -> l
    Succ _ l -> l
    Pred _ l -> l
Sven Keidel's avatar
Sven Keidel committed
107
    Mult _ _ l -> l
108
    IfZero _ _ _ l -> l
Sven Keidel's avatar
Sven Keidel committed
109
    Let _ _ l -> l
110
    Apply _ l -> l
Jente Hidskes's avatar
Jente Hidskes committed
111

112 113
instance IsString (State Label Expr) where
  fromString = var . fromString
114 115

instance Hashable Expr where
Sven Keidel's avatar
Sven Keidel committed
116
  hashWithSalt s e = s `hashWithSalt` label e
117

118 119 120 121
apply :: Prism' (store,(env,Expr)) (store,((Expr,Label),env))
apply = L.prism' (\(store,((e',l),env)) -> (store,(env,Apply e' l)))
                 (\(store,(env,e)) -> case e of
                      Apply e' l -> Just (store,((e',l),env))
122
                      _ -> Nothing)
123
{-# INLINE apply #-}
Sven Keidel's avatar
Sven Keidel committed
124 125 126 127 128 129 130

freeVars :: Expr -> HashMap Expr (HashSet Text)
freeVars e0 = execState (go e0) M.empty
  where
    go :: Expr -> State (HashMap Expr (HashSet Text)) (HashSet Text)
    go e = case e of
      Var x _ -> return (H.singleton x)
Sven Keidel's avatar
Sven Keidel committed
131 132
      Lam xs e1 _ -> save $ flip (foldr H.delete) xs <$> go e1
      App e1 e2 _ -> H.union <$> go e1 <*> (H.unions <$> mapM go e2)
Sven Keidel's avatar
Sven Keidel committed
133 134 135
      Zero _ -> return H.empty
      Succ e1 _ -> go e1
      Pred e1 _ -> go e1
Sven Keidel's avatar
Sven Keidel committed
136
      Mult e1 e2 _ -> H.union <$> go e1 <*> go e2
Sven Keidel's avatar
Sven Keidel committed
137 138 139 140 141
      IfZero e1 e2 e3 _ -> do
          m1 <- go e1
          m2 <- go e2
          m3 <- go e3
          return (m1 <> m2 <> m3)
Sven Keidel's avatar
Sven Keidel committed
142 143 144
      Let bnds e1 _ -> do
        vars <- go e1
        return (vars `H.difference` H.fromList [ v | (v,_) <- bnds])
Sven Keidel's avatar
Sven Keidel committed
145 146 147 148 149 150
      Apply e1 _ -> go e1
      where
        save m = do
          fv <- m
          modify (M.insert e fv)
          return fv