diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index ade57fe75..b08e6f1bc 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -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) @@ -470,7 +471,7 @@ 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 } @@ -478,9 +479,9 @@ longApp :: { Expr PName } | 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) diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 0e873ce7e..3b770fb13 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -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) @@ -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, @@ -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 @@ -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 } @@ -754,4 +789,3 @@ mkSelector tok = Selector (RecordSelectorTok t) -> RecordSel (mkIdent t) Nothing _ -> panic "mkSelector" [ "Unexpected selector token", show tok ] - diff --git a/src/Cryptol/Parser/Position.hs b/src/Cryptol/Parser/Position.hs index 96fc4ff46..e5912b931 100644 --- a/src/Cryptol/Parser/Position.hs +++ b/src/Cryptol/Parser/Position.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 8089bbd75..2853d229b 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -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 @@ -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 @@ -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 @@ -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 -> diff --git a/tests/issues/issue962.icry b/tests/issues/issue962.icry index 5d6f104da..f09988387 100644 --- a/tests/issues/issue962.icry +++ b/tests/issues/issue962.icry @@ -1,4 +1,9 @@ `{1} +(((True`{}, zero`{Integer})`{}).1)`{} +number`{3}`{}`{}`{}`{}`{Integer} :l issue962a.cry +:t i +:t j + :l issue962b.cry diff --git a/tests/issues/issue962.icry.stdout b/tests/issues/issue962.icry.stdout index e69de29bb..b8676f3e7 100644 --- a/tests/issues/issue962.icry.stdout +++ b/tests/issues/issue962.icry.stdout @@ -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. diff --git a/tests/issues/issue962a.cry b/tests/issues/issue962a.cry index 3d2a51bd9..3083451f3 100644 --- a/tests/issues/issue962a.cry +++ b/tests/issues/issue962a.cry @@ -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 diff --git a/tests/issues/issue962b.cry b/tests/issues/issue962b.cry index 4d7f7b265..20b9d7623 100644 --- a/tests/issues/issue962b.cry +++ b/tests/issues/issue962b.cry @@ -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}