Skip to content

Commit

Permalink
Update the parser to deal more robustly with type applications.
Browse files Browse the repository at this point in the history
We now reject situations where the user writes a type application
on a term that is not an identifier, and we correctly unwind
and reapply tuple and field selectors.

Fixes #962
Fixes #1045
Fixes #1050
  • Loading branch information
robdockins committed Feb 10, 2021
1 parent 19630f8 commit a4681b3
Show file tree
Hide file tree
Showing 8 changed files with 102 additions and 29 deletions.
9 changes: 5 additions & 4 deletions src/Cryptol/Parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ module Cryptol.Parser

import Control.Applicative as A
import Data.Maybe(fromMaybe)
import Data.List.NonEmpty ( NonEmpty(..), cons )
import Data.Text(Text)
import qualified Data.Text as T
import Control.Monad(liftM2,msum)
Expand Down Expand Up @@ -470,17 +471,17 @@ longRHS :: { Expr PName }

-- Prefix application expression, ends with an atom.
simpleApp :: { Expr PName }
: aexprs { mkEApp $1 }
: aexprs {% mkEApp $1 }

-- Prefix application expression, may end with a long expression
longApp :: { Expr PName }
: simpleApp longExpr { at ($1,$2) (EApp $1 $2) }
| longExpr { $1 }
| simpleApp { $1 }

aexprs :: { [Expr PName] }
: aexpr { [$1] }
| aexprs aexpr { $2 : $1 }
aexprs :: { NonEmpty (Expr PName) }
: aexpr { $1 :| [] }
| aexprs aexpr { cons $2 $1 }


-- Expression atom (needs no parens)
Expand Down
70 changes: 52 additions & 18 deletions src/Cryptol/Parser/ParserUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ module Cryptol.Parser.ParserUtils where

import Data.Maybe(fromMaybe)
import Data.Bits(testBit,setBit)
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Control.Monad(liftM,ap,unless,guard)
import qualified Control.Monad.Fail as Fail
import Data.Text(Text)
Expand Down Expand Up @@ -281,11 +283,14 @@ mkRecord rng f xs =


-- | Input expression are reversed
mkEApp :: [Expr PName] -> Expr PName
mkEApp es@(eLast : _) = at (eFirst,eLast) $ foldl EApp f xs
mkEApp :: NonEmpty (Expr PName) -> ParseM (Expr PName)

mkEApp es@(eLast :| _) =
do f :| xs <- cvtTypeParams eFirst rest
pure (at (eFirst,eLast) $ foldl EApp f xs)

where
eFirst : rest = reverse es
f : xs = cvtTypeParams eFirst rest
eFirst :| rest = NE.reverse es

{- Type applications are parsed as `ETypeVal (TTyApp fs)` expressions.
Here we associate them with their corresponding functions,
Expand All @@ -295,21 +300,51 @@ mkEApp es@(eLast : _) = at (eFirst,eLast) $ foldl EApp f xs
becomes
[ f, x ` { a = 2 }, y ]
-}
cvtTypeParams e [] = [e]
cvtTypeParams e [] = pure (e :| [])
cvtTypeParams e (p : ps) =
case toTypeParam p of
Just fs -> cvtTypeParams (EAppT e fs) ps
Nothing -> e : cvtTypeParams p ps

toTypeParam e =
case dropLoc e of
ETypeVal t -> case dropLoc t of
TTyApp fs -> Just (map mkTypeInst fs)
_ -> Nothing
case toTypeParam p Nothing of
Nothing -> NE.cons e <$> cvtTypeParams p ps

Just (fs,ss,rng) ->
if checkAppExpr e then
let e' = foldr (flip ESel) (EAppT e fs) ss
e'' = case rCombMaybe (getLoc e) rng of
Just r -> ELocated e' r
Nothing -> e'
in cvtTypeParams e'' ps
else
errorMessage (fromMaybe emptyRange (getLoc e))
[ "Explicit type applications can only be applied to named values."
, "Unexpected: " ++ show (pp e)
]

{- Check if the given expression is a legal target for explicit type application.
This is basically only variables, but we also allow the parenthesis and
the phantom "located" AST node.
-}
checkAppExpr e =
case e of
ELocated e' _ -> checkAppExpr e'
EParens e' -> checkAppExpr e'
EVar{} -> True
_ -> False

{- Look under a potential chain of selectors to see if we have a TTyApp.
If so, return the ty app information and the collected selectors
to reapply.
-}
toTypeParam e mr =
case e of
ELocated e' rng -> toTypeParam e' (rCombMaybe mr (Just rng))
ETypeVal t -> toTypeParam' t mr
ESel e' s -> ( \(fs,ss,r) -> (fs,s:ss,r) ) <$> toTypeParam e' mr
_ -> Nothing

mkEApp es = panic "[Parser] mkEApp" ["Unexpected:", show es]

toTypeParam' t mr =
case t of
TLocated t' rng -> toTypeParam' t' (rCombMaybe mr (Just rng))
TTyApp fs -> Just (map mkTypeInst fs, [], mr)
_ -> Nothing

unOp :: Expr PName -> Expr PName -> Expr PName
unOp f x = at (f,x) $ EApp f x
Expand Down Expand Up @@ -355,7 +390,7 @@ exprToNumT r expr =
-- | WARNING: This is a bit of a hack.
-- It is used to represent anonymous type applications.
anonTyApp :: Maybe Range -> [Type PName] -> Type PName
anonTyApp ~(Just r) ts = TTyApp (map toField ts)
anonTyApp ~(Just r) ts = TLocated (TTyApp (map toField ts)) r
where noName = Located { srcRange = r, thing = mkIdent (T.pack "") }
toField t = Named { name = noName, value = t }

Expand Down Expand Up @@ -754,4 +789,3 @@ mkSelector tok =
Selector (RecordSelectorTok t) -> RecordSel (mkIdent t) Nothing
_ -> panic "mkSelector"
[ "Unexpected selector token", show tok ]

5 changes: 5 additions & 0 deletions src/Cryptol/Parser/Position.hs
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,11 @@ rComb r1 r2 = Range { from = rFrom, to = rTo, source = source r1 }
where rFrom = min (from r1) (from r2)
rTo = max (to r1) (to r2)

rCombMaybe :: Maybe Range -> Maybe Range -> Maybe Range
rCombMaybe Nothing y = y
rCombMaybe x Nothing = x
rCombMaybe (Just x) (Just y) = Just (rComb x y)

rCombs :: [Range] -> Range
rCombs = foldl1 rComb

Expand Down
10 changes: 6 additions & 4 deletions src/Cryptol/TypeCheck/Error.hs
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
errorImportance :: Error -> Int
errorImportance err =
case err of
BareTypeApp{} -> 11 -- basically a parse error
BareTypeApp -> 11 -- basically a parse error
KindMismatch {} -> 10
TyVarWithParams {} -> 9
TypeMismatch {} -> 8
Expand Down Expand Up @@ -224,7 +224,7 @@ instance TVars Error where
RepeatedTypeParameter {} -> err
AmbiguousSize x t -> AmbiguousSize x !$ (apSubst su t)

BareTypeApp{} -> err
BareTypeApp -> err

UndefinedExistVar {} -> err
TypeShadowing {} -> err
Expand Down Expand Up @@ -256,7 +256,7 @@ instance FVS Error where
RepeatedTypeParameter {} -> Set.empty
AmbiguousSize _ t -> fvs t

BareTypeApp{} -> Set.empty
BareTypeApp -> Set.empty

UndefinedExistVar {} -> Set.empty
TypeShadowing {} -> Set.empty
Expand Down Expand Up @@ -411,7 +411,9 @@ instance PP (WithNames Error) where
Nothing -> empty
in addTVarsDescsAfter names err ("Ambiguous numeric type:" <+> pp (tvarDesc x) $$ sizeMsg)

BareTypeApp -> "Unexpected bare type application"
BareTypeApp ->
"Unexpected bare type application." $$
"Perhaps you meant `( ... ) instead."

UndefinedExistVar x -> "Undefined type" <+> quotes (pp x)
TypeShadowing this new that ->
Expand Down
5 changes: 5 additions & 0 deletions tests/issues/issue962.icry
Original file line number Diff line number Diff line change
@@ -1,4 +1,9 @@
`{1}
(((True`{}, zero`{Integer})`{}).1)`{}
number`{3}`{}`{}`{}`{}`{Integer}

:l issue962a.cry
:t i
:t j

:l issue962b.cry
23 changes: 23 additions & 0 deletions tests/issues/issue962.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
Loading module Cryptol

[error] at issue962.icry:1:2--1:5:
Unexpected bare type application.
Perhaps you meant `( ... ) instead.

Parse error at issue962.icry:2:3--2:28
Explicit type applications can only be applied to named values.
Unexpected: (True`{}, zero`{Integer})

Parse error at issue962.icry:3:1--3:11
Explicit type applications can only be applied to named values.
Unexpected: number`{3}
Loading module Cryptol
Loading module Main
i : {a} (fin a) => [a] -> [a]
j : {a} (fin a) => [a]{fld : Integer} -> [a]Integer
Loading module Cryptol
Loading module Main

[error] at issue962b.cry:32:16--32:25:
Unexpected bare type application.
Perhaps you meant `( ... ) instead.
7 changes: 5 additions & 2 deletions tests/issues/issue962a.cry
Original file line number Diff line number Diff line change
@@ -1,10 +1,13 @@
f : {a} (fin a) => [a] -> (Bit, [a])
f : {a, b} (fin a) => [a]b -> (Bit, [a]b)
f x = (True, x)

g : {a} (fin a) => [a] -> [a]
g : {a,b} (fin a) => [a]b -> [a]b
g x = (f`{a=a} x).1

h = f.1

i : {a} (fin a) => [a] -> [a]
i = f`{a=a}.1

j : {a} (fin a) => [a]{ fld : Integer } -> [a]Integer
j = f`{a=a,b={fld : Integer}}.1.fld
2 changes: 1 addition & 1 deletion tests/issues/issue962b.cry
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ build2row : [v1][v1]Fld -> [v1][o1]Fld -> [v1][o2]Fld ->
[o1][o1]Fld -> [o1][o2]Fld -> [width nn] -> [nn]Fld
build2row a11 a12 a13 a22 a23 i =
if i < `v1 then
a11 @ i # a12 @ i # a13
a11 @ i # a12 @ i # a13 @ i
else if i < `{v1 + o1} then
/* vzero`{n=v1} # a22 @ (i - `v1) # a23 @ (i - `v1) */
vzero`{n=v1} # vzero`{n=o1} # vzero`{n=o2}
Expand Down

0 comments on commit a4681b3

Please sign in to comment.