Skip to content

Commit

Permalink
Type checking wasn't checking disjointness
Browse files Browse the repository at this point in the history 
The type checker wasn't checking for disjointness when splitting the
context.  Thus, wasn't properly checking linearity.

This is now fixed:

ILL> :type \p:!A (x) !B.let p : !A (x) !B be x (x) y in discard x in x
TypeErrorDuplicatedFreeVar
ILL> :type \p:!A (x) !B.let p : !A (x) !B be x (x) y in discard x in y
(!A (x) !B) -o !B
ILL>
  • Loading branch information
Harley Eades committed Apr 9, 2017
1 parent 1eb9533 commit acb3066
Show file tree
Hide file tree
Showing 7 changed files with 85 additions and 34 deletions.
8 changes: 5 additions & 3 deletions Source/ALL/Languages/ILL/Parser/Parser.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,17 @@ import qualified Languages.ILL.Parser.Tokenizer as Tok
constParser p c = p >> return c

binOp assoc op f = Text.Parsec.Expr.Infix (do{ op;return f}) assoc
prefixOp op f = Text.Parsec.Expr.Prefix (do{ op;return f})

reservedWords = ["Top", "let", "in", "be", "triv", "discard",
"of", "copy", "derelicit", "as", "promote", "for"]

typeParser = buildExpressionParser typeTable typeParser'
where
typeTable = [[binOp AssocNone tensorParser (\d r -> Tensor d r)],
typeTable = [[prefixOp bangParser (\r -> Bang r)],
[binOp AssocNone tensorParser (\d r -> Tensor d r)],
[binOp AssocRight impParser (\d r -> Imp d r)]]
typeParser' = try (Tok.parens typeParser) <|> topParser <|> bangParser <|> tyvarParser
typeParser' = try (Tok.parens typeParser) <|> topParser <|> tyvarParser

tyvarParser = do
x <- Tok.var
Expand All @@ -37,7 +39,7 @@ tyvarParser = do
impParser = constParser Tok.linImp Imp
tensorParser = constParser Tok.tensor Tensor
topParser = constParser Tok.top Top
bangParser = (Tok.symbol '!') >> typeParser >>= (\ty -> return $ Bang ty)
bangParser = constParser (Tok.symbol '!') Bang

patternParser = try (Tok.parens patternParser) <|> try ptrivParser <|> ptensorParser <|> pvarParser

Expand Down
3 changes: 0 additions & 3 deletions Source/ALL/Languages/ILL/Pretty.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,14 @@ import Languages.ILL.Intermediate
parenType :: (Type -> String) -> Type -> String
parenType f t@(Imp _ _) = "(" ++ f t ++ ")"
parenType f t@(Tensor _ _) = "(" ++ f t ++ ")"
parenType f t@(Bang _) = "(" ++ f t ++ ")"
parenType f t = f t

parenITType :: (Type -> String) -> Type -> String
parenITType f t@(Tensor _ _) = "(" ++ f t ++ ")"
parenITType f t@(Bang _) = "(" ++ f t ++ ")"
parenITType f t = f t

parenTType :: (Type -> String) -> Type -> String
parenTType f t@(Imp _ _) = "(" ++ f t ++ ")"
parenTType f t@(Bang _) = "(" ++ f t ++ ")"
parenTType f t = f t

parenBType :: (Type -> String) -> Type -> String
Expand Down
2 changes: 1 addition & 1 deletion Source/ALL/Languages/ILL/Repl.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ repl = do
where
loop :: InputT REPLStateIO ()
loop = do
minput <- getInputLine "ALL> "
minput <- getInputLine "ILL> "
case minput of
Nothing -> return ()
Just [] -> loop
Expand Down
90 changes: 64 additions & 26 deletions Source/ALL/Languages/ILL/TypeCheck.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,12 +39,23 @@ get = stateT (λ x → right (x , x))
put : ∀{S} → S → StateT S (Either Exception) Unit
put s = stateT (λ x → Right (triv , s))

CTXEl : Set
CTXEl = Prod String Type

CTX : Set
CTX = List (Prod String Type)
CTX = List CTXEl

CTXV-eq : CTXEl → CTXEl → 𝔹
CTXV-eq (x , ty) (y , ty') = x str-eq y

TC : Set → Set
TC = StateT CTX (Either Exception)

_isDisjointWith_ : CTX → CTX → TC Unit
ctx₁ isDisjointWith ctx₂ with disjoint CTXV-eq ctx₁ ctx₂
... | tt = returnSTE triv
... | ff = throw TypeErrorDuplicatedFreeVar

getTypeCTX : String → CTX → maybe Type
getTypeCTX x ctx = lookup _str-eq_ x ctx

Expand Down Expand Up @@ -128,18 +139,22 @@ typeCheck' (Let t₁ ty PTriv t₂) =
get >>=STE
(λ ctx → lift (subctxFV ctx t₁) >>=STE
(λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
λ ctx₂ → ((put ctx₁) >>STE typeCheck' t₁) >>=STE
(λ ty₁ → isTop ty₁ >>STE (put ctx₂ >>STE typeCheck' t₂))))
λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
((put ctx₁) >>STE typeCheck' t₁) >>=STE
(λ ty₁ → isTop ty₁ >>STE
(put ctx₂ >>STE typeCheck' t₂))))
typeCheck' (Let t₁ ty (PTensor x y) t₂) =
get >>=STE
(λ ctx → lift (subctxFV ctx t₁) >>=STE
(λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → ((put ctx₁) >>STE typeCheck' t₁) >>=STE
(λ ty₁ → (isTensor ty₁) >>=STE
(λ tys → let A = fst tys
B = snd tys
t₂' = open-t 0 y RLPV (FVar y) (open-t 0 x LLPV (FVar x) t₂)
in put ((x , A) :: (y , B) :: ctx₂) >>STE typeCheck' t₂')))))
(λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
((put ctx₁) >>STE
typeCheck' t₁) >>=STE
(λ ty₁ → (isTensor ty₁) >>=STE
(λ tys → let A = fst tys
B = snd tys
t₂' = open-t 0 y RLPV (FVar y) (open-t 0 x LLPV (FVar x) t₂)
in put ((x , A) :: (y , B) :: ctx₂) >>STE typeCheck' t₂')))))
typeCheck' (Lam x ty t) =
get >>=STE
(λ ctx → (put ((x , ty) :: ctx)) >>STE
Expand All @@ -148,23 +163,43 @@ typeCheck' (Lam x ty t) =
typeCheck' (App t₁ t₂) =
get >>=STE
(λ ctx → lift (subctxFV ctx t₁) >>=STE
(λ ctx₁ → (put ctx₁) >>STE (typeCheck' t₁) >>=STE
(λ ty₁ → isImp ty₁ >>=STE
(λ tys → lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → (put ctx₂) >>STE (typeCheck' t₂) >>=STE
(λ ty₂ → ((fst tys) tyEq ty₂) >>STE returnSTE (snd tys)))))))
(λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
(put ctx₁) >>STE (typeCheck' t₁) >>=STE
(λ ty₁ → isImp ty₁ >>=STE
(λ tys → (put ctx₂) >>STE (typeCheck' t₂) >>=STE
(λ ty₂ → ((fst tys) tyEq ty₂) >>STE returnSTE (snd tys)))))))
typeCheck' (Tensor t₁ t₂) =
get >>=STE
(λ ctx → lift (subctxFV ctx t₁) >>=STE
(λ ctx₁ → (put ctx₁) >>STE typeCheck' t₁) >>=STE
(λ ty₁ → lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → (put ctx₂) >>STE typeCheck' t₂) >>=STE
(λ ty₂ → returnSTE (Tensor ty₁ ty₂))))
(λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
(put ctx₁) >>STE typeCheck' t₁ >>=STE
(λ ty₁ → (put ctx₂) >>STE typeCheck' t₂ >>=STE
(λ ty₂ → returnSTE (Tensor ty₁ ty₂))))))
typeCheck' (Promote ms t) =
put [] >>STE checkVectorOpenTerm ms t
put [] >>STE getSubctxs ms
>>=STE areDisjointCtxs
>>STE checkVectorOpenTerm ms t
>>=STE typeCheck'
>>=STE (λ ty → returnSTE (Bang ty))
where
getSubctxs : List (Triple Term String Type) → TC (List CTX)
getSubctxs ((triple t _ _) :: rest) =
get >>=STE
(λ ctx → (lift (subctxFV ctx t)) >>=STE
(λ ctx' → (getSubctxs rest) >>=STE
(λ r → returnSTE (ctx' :: r))))
getSubctxs l = returnSTE []

areDisjointCtxs : List CTX → TC Unit
areDisjointCtxs [] = returnSTE triv
areDisjointCtxs (ctx₁ :: rest) = aux ctx₁ rest >>STE areDisjointCtxs rest
where
aux : CTX → List CTX → TC Unit
aux ctx₁ (ctx₂ :: rest) = (ctx₁ isDisjointWith ctx₂) >>STE aux ctx₁ rest
aux _ [] = returnSTE triv

checkVectorTerm : Term → TC Type
checkVectorTerm t =
get >>=STE
Expand All @@ -184,16 +219,19 @@ typeCheck' (Promote ms t) =
typeCheck' (Discard t₁ t₂) = get >>=STE
(λ ctx → lift (subctxFV ctx t₁) >>=STE
(λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → (put ctx₁) >>STE typeCheck' t₁
>>=STE isBang
>>STE (put ctx₂)
>>STE typeCheck' t₂)))
(λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
(put ctx₁) >>STE typeCheck' t₁
>>=STE isBang
>>STE (put ctx₂)
>>STE typeCheck' t₂)))
typeCheck' (Copy t₁ (x , y) t₂) =
get >>=STE
(λ ctx → lift (subctxFV ctx t₁) >>=STE
(λ ctx₁ → (put ctx₁) >>STE typeCheck' t₁ >>=STE
(λ ty₁ → isBang ty₁ >>STE lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → (put ((x , ty₁) :: (y , ty₁) :: ctx₂) >>STE typeCheck' t₂')))))
(λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
(λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
(put ctx₁) >>STE typeCheck' t₁ >>=STE
(λ ty₁ → isBang ty₁ >>STE
(put ((x , ty₁) :: (y , ty₁) :: ctx₂) >>STE typeCheck' t₂')))))
where
t₂' = open-t 0 y RCPV (FVar y) (open-t 0 x LCPV (FVar x) t₂)
typeCheck' (Derelict t) = typeCheck' t >>=STE isBang
Expand Down
4 changes: 3 additions & 1 deletion Source/ALL/Utils/Exception.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ data Exception : Set where
TypeErrorTypesNotEqual : Exception
TypeErrorAppNotImp : Exception
NonLinearCtx : Exception
TypeErrorDuplicatedFreeVar : Exception
{-# COMPILED_DATA Exception Utils.Exception.Exception Utils.Exception.IllformedLetPattern
Utils.Exception.IllformedPromote
Utils.Exception.VarNotInCtx
Expand All @@ -53,4 +54,5 @@ data Exception : Set where
Utils.Exception.TypeErrorPromoteNotBang
Utils.Exception.TypeErrorTypesNotEqual
Utils.Exception.TypeErrorAppNotImp
Utils.Exception.NonLinearCtx #-}
Utils.Exception.NonLinearCtx
Utils.Exception.TypeErrorDuplicatedFreeVar #-}
1 change: 1 addition & 0 deletions Source/ALL/Utils/Exception.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,4 +12,5 @@ data Exception = IllformedLetPattern
| TypeErrorTypesNotEqual
| TypeErrorAppNotImp
| NonLinearCtx
| TypeErrorDuplicatedFreeVar
deriving Show
11 changes: 11 additions & 0 deletions Source/ALL/Utils/HaskellFunctions.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,19 @@ foldr : {A : Set}{B : Set} → (A → B → B) → B → List A → B
foldr f b [] = b
foldr f b (a :: as) = f a (foldr f b as)

foldl : {A : Set}{B : Set} → (B → A → B) → B → List A → B
foldl f b [] = b
foldl f b (x :: xs) = foldl f (f b x) xs

lookup : ∀{A B} → (A → A → 𝔹) → A → List (Prod A B) → maybe B
lookup _eq_ x [] = nothing
lookup _eq_ x ((y , b) :: l) with x eq y
... | tt = just b
... | ff = lookup _eq_ x l

disjoint : {A : Set} → (A → A → 𝔹) → List A → List A → 𝔹
disjoint _eq_ (x :: l₁) (y :: l₂) with x eq y
... | tt = ff
... | ff = disjoint _eq_ l₁ l₂
disjoint _ [] _ = tt
disjoint _ _ [] = tt

0 comments on commit acb3066

Please sign in to comment.