Skip to content

Commit 10918bf

Browse files
committed
feed the typechecker with concrete syntax tree
1 parent 0038efe commit 10918bf

File tree

7 files changed

+188
-86
lines changed

7 files changed

+188
-86
lines changed

src/PPrint.hs

-4
Original file line numberDiff line numberDiff line change
@@ -35,10 +35,6 @@ instance Pretty Chan where
3535
pretty (NR StdOut) = "stdout"
3636
pretty (NR StdIn) = "stdin"
3737

38-
instance Pretty PureName where
39-
pretty (PH x) = pretty x
40-
pretty (PG i) = "x" <> pretty i
41-
4238
instance Pretty a => Pretty (Polarised a) where
4339
pretty (Pos x) = pretty x
4440
pretty (Neg x) = "~" <> pretty x

src/Syntax/Abstract.hs

+18-20
Original file line numberDiff line numberDiff line change
@@ -26,15 +26,16 @@ data Chan = ND Name -- user defined
2626
| NR ResName -- reserved name
2727
deriving (Ord, Eq, Show)
2828

29-
data PureName = PH Text -- "pure" names, without polarization
30-
| PG Int
31-
deriving (Eq, Show, Ord)
32-
33-
3429
instance HasDual (Polarised a) where
3530
dual (Pos a) = Neg a
3631
dual (Neg a) = Pos a
3732

33+
instance HasDual Chan where
34+
dual (ND n) = ND (dual n)
35+
dual (NG n) = NG (dual n)
36+
dual (NR StdIn) = NR StdOut
37+
dual (NR StdOut) = NR StdIn
38+
3839
isPositive :: Polarised a -> Bool
3940
isPositive (Pos _) = True
4041
isPositive (Neg _) = False
@@ -44,13 +45,9 @@ depolarise (Pos x) = x
4445
depolarise (Neg x) = x
4546
-- depolar (Neu x) = x
4647

47-
depolarCh :: Chan -> PureName
48-
depolarCh (ND c) = PH (depolarise c)
49-
depolarCh (NG c) = PG (depolarise c)
50-
depolarCh (NR _) = error "bug: shouldn't call depolar without checking"
51-
52-
depolarCH :: Chan -> Text
53-
depolarCH = depolarise . unND
48+
depolariseChan :: Chan -> Text
49+
depolariseChan (ND c) = depolarise c
50+
depolariseChan _ = error "bug: shouldn't call depolar without checking"
5451

5552
unND :: Chan -> Name
5653
unND (ND n) = n
@@ -70,7 +67,7 @@ data Proc = End
7067
| Send Chan Expr Proc
7168
| Recv Chan [Clause]
7269
| Par Proc Proc
73-
| Nu Text (Maybe Type) Proc
70+
| Nu Chan (Maybe Type) Proc
7471
| Repl Proc
7572
| Call ProcName
7673
deriving (Eq, Show)
@@ -153,18 +150,18 @@ End `par` p = p
153150
p `par` End = p
154151
p `par` q = Par p q
155152

156-
type Subst = Map PureName Val
153+
type Subst = Map Text Val
157154

158155
substChan :: Subst -> Chan -> Chan
159156
substChan _ (NR r) = NR r
160-
substChan th c = case Map.lookup (depolarCh c) th of
157+
substChan th c = case Map.lookup (depolariseChan c) th of
161158
Just (VC y) -> y
162159
Just _ -> error "not a channel"
163160
Nothing -> c
164161

165162
substVal :: Subst -> Val -> Val
166163
substVal _ (VC (NR r)) = VC (NR r)
167-
substVal th (VC c) = case Map.lookup (depolarCh c) th of
164+
substVal th (VC c) = case Map.lookup (depolariseChan c) th of
168165
Just v -> v
169166
Nothing -> VC c
170167
substVal th (VT vs) = VT (map (substVal th) vs)
@@ -201,7 +198,7 @@ substProc th (Recv c clauses) =
201198
(map (\(Clause ptrn p) -> Clause ptrn (substProc th' p)) clauses)
202199
where th' = foldr mask th (map (\(Clause ptrn _) -> ptrn) clauses)
203200
substProc th (Par p q) = Par (substProc th p) (substProc th q)
204-
substProc th (Nu y t p) = if Map.member (PH y) th
201+
substProc th (Nu y t p) = if Map.member (depolariseChan y) th
205202
then Nu y t p -- is this right?
206203
else Nu y t (substProc th p)
207204
substProc th (Repl p) = Repl (substProc th p) -- is this right?
@@ -249,7 +246,7 @@ evalExpr (EPrj i e) =
249246
-- substitution related stuffs
250247

251248
match :: Ptrn -> Val -> Maybe Subst
252-
match (PtrnVar x) v = Just $ Map.fromList [(PH x,v)]
249+
match (PtrnVar x) v = Just $ Map.fromList [(x, v)]
253250
match (PtrnLabel x) (VL y) | x == y = Just Map.empty
254251
match (PtrnTuple xs) (VT vs) | length xs == length vs =
255252
Map.unions <$> mapM (uncurry match) (zip xs vs)
@@ -267,7 +264,7 @@ matchClauses ((Clause pt e):_) v
267264
matchClauses (_:pps) v = matchClauses pps v
268265

269266
mask :: Ptrn -> Subst -> Subst
270-
mask (PtrnVar x) = Map.delete (PH x)
267+
mask (PtrnVar x) = Map.delete x
271268
mask (PtrnTuple []) = id
272269
mask (PtrnTuple (p:ps)) = mask (PtrnTuple ps) . mask p
273270
mask (PtrnLabel _) = id
@@ -310,7 +307,8 @@ freeProc (Send c e p) =
310307
freeProc (Recv c ps) =
311308
freeN c `Set.union` Set.unions (map freeClause ps)
312309
freeProc (Par p1 p2) = freeProc p1 `Set.union` freeProc p2
313-
freeProc (Nu x _ p) = freeProc p `Set.difference` Set.fromList [Pos x, Neg x]
310+
freeProc (Nu x _ p) = freeProc p `Set.difference` Set.fromList
311+
[Pos (depolariseChan x), Neg (depolariseChan x)]
314312
freeProc (Repl p) = freeProc p -- is that right?
315313
freeProc (Call _) = undefined -- what to do here?
316314

src/Syntax/Concrete.hs

+101-4
Original file line numberDiff line numberDiff line change
@@ -7,35 +7,66 @@ module Syntax.Concrete where
77

88
import qualified Syntax.Abstract as A
99
import qualified Type as A
10+
import Type (HasDual(..))
1011
import Data.Text (Text)
11-
import Data.Loc (Loc, Located(..))
12+
import Data.Loc (Loc(..), Located(..))
1213
import Prelude hiding (LT, EQ, GT)
14+
import Data.Function (on)
1315

1416
--------------------------------------------------------------------------------
1517
-- | Concrete Syntax Tree
1618

1719
data Label = Label Text Loc
1820
deriving (Show)
21+
22+
instance Eq Label where
23+
(==) = (==) `on` toAbstract
24+
instance Ord Label where
25+
compare = compare `on` toAbstract
26+
1927
data Chan = Pos Text Loc
2028
| Neg Text Loc
2129
| Res Text Loc
2230
deriving (Show)
2331

32+
instance Eq Chan where
33+
(==) = (==) `on` toAbstract
34+
instance Ord Chan where
35+
compare = compare `on` toAbstract
36+
instance HasDual Chan where
37+
dual (Pos x l) = Neg x l
38+
dual (Neg x l) = Pos x l
39+
dual (Res "stdout" l) = Res "stdin" l
40+
dual (Res "stdin" l) = Res "stdout" l
41+
dual (Res x l) = Res x l
42+
2443
data Program = Program [Definition] Loc
2544
deriving (Show)
2645
data ProcName = ProcName Text Loc
2746
deriving (Show)
47+
48+
instance Eq ProcName where
49+
(==) = (==) `on` toAbstract
50+
instance Ord ProcName where
51+
compare = compare `on` toAbstract
52+
2853
data TypeName = TypeName Text Loc
2954
deriving (Show)
3055

56+
instance Eq TypeName where
57+
(==) = (==) `on` toAbstract
58+
instance Ord TypeName where
59+
compare = compare `on` toAbstract
60+
61+
3162
data Definition = ProcDefn ProcName Proc Loc
3263
| ChanType Chan Type Loc
3364
| TypeDefn TypeName Type Loc
3465
deriving (Show)
3566

3667
data Proc = Send Chan Expr Proc Loc
3768
| Recv Chan [Clause] Loc
38-
| Nu ProcName (Maybe Type) Proc Loc
69+
| Nu Chan (Maybe Type) Proc Loc
3970
| Par Proc Proc Loc
4071
| Call ProcName Loc
4172
| Repl Proc Loc
@@ -75,7 +106,10 @@ data Expr = ExprTuple [Expr] Loc
75106

76107
data TypeVar = TypeVarIndex Int Loc
77108
| TypeVarText TypeName Loc
78-
deriving (Show)
109+
deriving (Show)
110+
111+
instance Eq TypeVar where
112+
(==) = (==) `on` toAbstract
79113

80114
data BaseType = BaseInt Loc
81115
| BaseBool Loc
@@ -91,9 +125,72 @@ data Type = TypeEnd Loc
91125
| TypeVar TypeVar Loc
92126
| TypeMu Type Loc
93127
deriving (Show)
94-
data TypeOfLabel = TypeOfLabel Label Type Loc
128+
129+
-- type substitution. it is assumed that s contains
130+
-- no bound variables.
131+
132+
substTypeOfLabel :: Int -> Type -> TypeOfLabel -> TypeOfLabel
133+
substTypeOfLabel i s (TypeOfLabel label t l) = TypeOfLabel label (substType i s t) l
134+
135+
substType :: Int -> Type -> Type -> Type
136+
substType _ _ (TypeEnd l) = TypeEnd l
137+
substType _ _ (TypeBase t l) = TypeBase t l
138+
substType i s (TypeTuple ts l) = TypeTuple (map (substType i s) ts) l
139+
substType i s (TypeSend t u l) = TypeSend (substType i s t) (substType i s u) l
140+
substType i s (TypeRecv t u l) = TypeRecv (substType i s t) (substType i s u) l
141+
substType i s (TypeChoi ts l) = TypeChoi (map (substTypeOfLabel i s) ts) l
142+
substType i s (TypeSele ts l) = TypeSele (map (substTypeOfLabel i s) ts) l
143+
substType i s (TypeUn t l) = TypeUn (substType i s t) l
144+
substType i s (TypeVar j l) | TypeVarIndex i l == j = s
145+
| otherwise = TypeVar j l
146+
substType i s (TypeMu t l) = TypeMu (substType (1+i) s t) l
147+
148+
unfoldType :: Type -> Type
149+
unfoldType (TypeMu t l) = substType 0 (TypeMu t l) t
150+
unfoldType t = t
151+
152+
stripUnrestricted :: Type -> (Type, Bool)
153+
stripUnrestricted (TypeEnd l) = (TypeEnd l, True)
154+
stripUnrestricted (TypeBase t l) = (TypeBase t l, True)
155+
stripUnrestricted (TypeUn t l) = (t, True) -- shouldn't be nested
156+
stripUnrestricted (TypeTuple ts l) = (TypeTuple (map fst tts) l, and (map snd tts))
157+
where tts = map stripUnrestricted ts
158+
stripUnrestricted (TypeMu t l) = let (t', p) = stripUnrestricted t in (TypeMu t' l, p)
159+
stripUnrestricted t = (t, False)
160+
161+
tInt :: Type
162+
tInt = TypeBase (BaseInt NoLoc) NoLoc
163+
164+
tBool :: Type
165+
tBool = TypeBase (BaseBool NoLoc) NoLoc
166+
167+
instance Eq Type where
168+
(==) = (==) `on` toAbstract
169+
170+
instance Ord Type where
171+
compare = compare `on` toAbstract
172+
173+
instance HasDual Type where
174+
dual (TypeEnd l) = TypeEnd l
175+
dual (TypeBase t l) = TypeBase t l
176+
dual (TypeTuple ts l) = TypeTuple (map dual ts) l
177+
dual (TypeSend c t l) = TypeRecv c (dual t) l
178+
dual (TypeRecv c t l) = TypeSend c (dual t) l
179+
dual (TypeSele ts l) = TypeChoi (map dual ts) l
180+
dual (TypeChoi ts l) = TypeSele (map dual ts) l
181+
dual (TypeUn t l) = TypeUn (dual t) l
182+
dual (TypeVar i l) = TypeVar i l
183+
dual (TypeMu t l) = TypeMu (dual t) l
184+
185+
data TypeOfLabel = TypeOfLabel Label Type Loc
95186
deriving (Show)
96187

188+
instance HasDual TypeOfLabel where
189+
dual (TypeOfLabel label t l) = TypeOfLabel label (dual t) l
190+
191+
typedLabelToPair :: TypeOfLabel -> (Label, Type)
192+
typedLabelToPair (TypeOfLabel l t _) = (l, t)
193+
97194
--------------------------------------------------------------------------------
98195
-- | Instance of Located
99196

src/Syntax/Parser/Parser.y

+5-4
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ import Data.Text (Text)
4949
';' { TokenSemi }
5050
'->' { TokenArrow }
5151
':' { TokenTypeOf }
52-
'Int' { TokenSortInt }
52+
'Int' { TokenSorTBase TInt }
5353
string { TokenString $$ }
5454
-- typing stuff
5555
'type' { TokenType }
@@ -63,7 +63,7 @@ import Data.Text (Text)
6363
typeName { TokenTypeName $$ }
6464

6565
-- boolean stuff
66-
'Bool' { TokenSortBool }
66+
'Bool' { TokenSorTBase TBool }
6767
'True' { TokenTrue }
6868
'False' { TokenFalse }
6969
'==' { TokenEQ }
@@ -113,8 +113,8 @@ Proc :: {Proc}
113113
| Chan '>>' '{' ChoiceClauses '}' {% locate $ Recv $1 (reverse $4) }
114114
| Chan '<<' SelectLabel '.' Proc {% locate $ Send $1 $3 $5 }
115115
| 'end' {% locate $ End }
116-
| '(' 'nu' ProcName ')' Proc {% locate $ Nu $3 Nothing $5 }
117-
| '(' 'nu' ProcName ':' Type ')' Proc {% locate $ Nu $3 (Just $5) $7 }
116+
| '(' 'nu' Chan ')' Proc {% locate $ Nu $3 Nothing $5 }
117+
| '(' 'nu' Chan ':' Type ')' Proc {% locate $ Nu $3 (Just $5) $7 }
118118
| '*' Proc {% locate $ Repl $2 }
119119
| ProcName {% locate $ Call $1 }
120120
| '(' ProcPar ')' { $2 }
@@ -148,6 +148,7 @@ ProcName :: {ProcName}
148148
TypeVar :: {TypeVar}
149149
: TypeName {% locate $ TypeVarText $1 }
150150

151+
151152
Chan :: {Chan}
152153
: namePos {% locate $ Pos $1 }
153154
| nameNeg {% locate $ Neg $1 }

src/Type.hs

+4-1
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,12 @@ data Type = TEnd -- end
2424
| TMu Type
2525
deriving (Eq, Show, Ord)
2626

27-
tInt = TBase TInt
27+
tBool :: Type
2828
tBool = TBase TBool
2929

30+
tInt :: Type
31+
tInt = TBase TInt
32+
3033
class HasDual a where
3134
dual :: a -> a
3235

0 commit comments

Comments
 (0)