From e03446dbc843e7a5a9a9963914c0b752ecb40f28 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 27 Jun 2019 14:25:08 -0700 Subject: [PATCH 1/2] Adjust whitespace. --- src/Cryptol/ModuleSystem/Renamer.hs | 86 ++++++++++++++--------------- src/Cryptol/Parser/AST.hs | 50 ++++++++--------- src/Cryptol/Parser/Names.hs | 57 +++++++++---------- 3 files changed, 97 insertions(+), 96 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 6bc692a13..532432d31 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -736,49 +736,49 @@ instance Rename UpdField where instance Rename Expr where rename expr = case expr of - EVar n -> EVar <$> renameVar n - ELit l -> return (ELit l) - ENeg e -> ENeg <$> rename e - EComplement e -> EComplement - <$> rename e - EGenerate e -> EGenerate - <$> rename e - ETuple es -> ETuple <$> traverse rename es - ERecord fs -> ERecord <$> traverse (rnNamed rename) fs - ESel e' s -> ESel <$> rename e' <*> pure s - EUpd mb fs -> do checkLabels fs - EUpd <$> traverse rename mb <*> traverse rename fs - EList es -> EList <$> traverse rename es - EFromTo s n e'-> EFromTo <$> rename s - <*> traverse rename n - <*> rename e' - EInfFrom a b -> EInfFrom<$> rename a <*> traverse rename b - EComp e' bs -> do arms' <- traverse renameArm bs - let (envs,bs') = unzip arms' - -- NOTE: renameArm will generate shadowing warnings; we only - -- need to check for repeated names across multiple arms - shadowNames' CheckOverlap envs (EComp <$> rename e' <*> pure bs') - EApp f x -> EApp <$> rename f <*> rename x - EAppT f ti -> EAppT <$> rename f <*> traverse rename ti - EIf b t f -> EIf <$> rename b <*> rename t <*> rename f - EWhere e' ds -> do ns <- getNS - shadowNames (map (InModule ns) ds) $ - EWhere <$> rename e' <*> traverse rename ds - ETyped e' ty -> ETyped <$> rename e' <*> rename ty - ETypeVal ty -> ETypeVal<$> rename ty - EFun ps e' -> do (env,ps') <- renamePats ps - -- NOTE: renamePats will generate warnings, so we don't - -- need to duplicate them here - shadowNames' CheckNone env (EFun ps' <$> rename e') - ELocated e' r -> withLoc r - $ ELocated <$> rename e' <*> pure r - - ESplit e -> ESplit <$> rename e - EParens p -> EParens <$> rename p - EInfix x y _ z-> do op <- renameOp y - x' <- rename x - z' <- rename z - mkEInfix x' op z' + EVar n -> EVar <$> renameVar n + ELit l -> return (ELit l) + ENeg e -> ENeg <$> rename e + EComplement e -> EComplement + <$> rename e + EGenerate e -> EGenerate + <$> rename e + ETuple es -> ETuple <$> traverse rename es + ERecord fs -> ERecord <$> traverse (rnNamed rename) fs + ESel e' s -> ESel <$> rename e' <*> pure s + EUpd mb fs -> do checkLabels fs + EUpd <$> traverse rename mb <*> traverse rename fs + EList es -> EList <$> traverse rename es + EFromTo s n e -> EFromTo <$> rename s + <*> traverse rename n + <*> rename e + EInfFrom a b -> EInfFrom<$> rename a <*> traverse rename b + EComp e' bs -> do arms' <- traverse renameArm bs + let (envs,bs') = unzip arms' + -- NOTE: renameArm will generate shadowing warnings; we only + -- need to check for repeated names across multiple arms + shadowNames' CheckOverlap envs (EComp <$> rename e' <*> pure bs') + EApp f x -> EApp <$> rename f <*> rename x + EAppT f ti -> EAppT <$> rename f <*> traverse rename ti + EIf b t f -> EIf <$> rename b <*> rename t <*> rename f + EWhere e' ds -> do ns <- getNS + shadowNames (map (InModule ns) ds) $ + EWhere <$> rename e' <*> traverse rename ds + ETyped e' ty -> ETyped <$> rename e' <*> rename ty + ETypeVal ty -> ETypeVal<$> rename ty + EFun ps e' -> do (env,ps') <- renamePats ps + -- NOTE: renamePats will generate warnings, so we don't + -- need to duplicate them here + shadowNames' CheckNone env (EFun ps' <$> rename e') + ELocated e' r -> withLoc r + $ ELocated <$> rename e' <*> pure r + + ESplit e -> ESplit <$> rename e + EParens p -> EParens <$> rename p + EInfix x y _ z -> do op <- renameOp y + x' <- rename x + z' <- rename z + mkEInfix x' op z' checkLabels :: [UpdField PName] -> RenameM () diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 365f4a693..4a252e4c1 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -946,31 +946,31 @@ instance NoPos (PropSyn name) where instance NoPos (Expr name) where noPos expr = case expr of - EVar x -> EVar x - ELit x -> ELit x - ENeg x -> ENeg (noPos x) - EComplement x -> EComplement (noPos x) - EGenerate x -> EGenerate (noPos x) - ETuple x -> ETuple (noPos x) - ERecord x -> ERecord (noPos x) - ESel x y -> ESel (noPos x) y - EUpd x y -> EUpd (noPos x) (noPos y) - EList x -> EList (noPos x) - EFromTo x y z -> EFromTo (noPos x) (noPos y) (noPos z) - EInfFrom x y -> EInfFrom (noPos x) (noPos y) - EComp x y -> EComp (noPos x) (noPos y) - EApp x y -> EApp (noPos x) (noPos y) - EAppT x y -> EAppT (noPos x) (noPos y) - EIf x y z -> EIf (noPos x) (noPos y) (noPos z) - EWhere x y -> EWhere (noPos x) (noPos y) - ETyped x y -> ETyped (noPos x) (noPos y) - ETypeVal x -> ETypeVal (noPos x) - EFun x y -> EFun (noPos x) (noPos y) - ELocated x _ -> noPos x - - ESplit x -> ESplit (noPos x) - EParens e -> EParens (noPos e) - EInfix x y f z-> EInfix (noPos x) y f (noPos z) + EVar x -> EVar x + ELit x -> ELit x + ENeg x -> ENeg (noPos x) + EComplement x -> EComplement (noPos x) + EGenerate x -> EGenerate (noPos x) + ETuple x -> ETuple (noPos x) + ERecord x -> ERecord (noPos x) + ESel x y -> ESel (noPos x) y + EUpd x y -> EUpd (noPos x) (noPos y) + EList x -> EList (noPos x) + EFromTo x y z -> EFromTo (noPos x) (noPos y) (noPos z) + EInfFrom x y -> EInfFrom (noPos x) (noPos y) + EComp x y -> EComp (noPos x) (noPos y) + EApp x y -> EApp (noPos x) (noPos y) + EAppT x y -> EAppT (noPos x) (noPos y) + EIf x y z -> EIf (noPos x) (noPos y) (noPos z) + EWhere x y -> EWhere (noPos x) (noPos y) + ETyped x y -> ETyped (noPos x) (noPos y) + ETypeVal x -> ETypeVal (noPos x) + EFun x y -> EFun (noPos x) (noPos y) + ELocated x _ -> noPos x + + ESplit x -> ESplit (noPos x) + EParens e -> EParens (noPos e) + EInfix x y f z -> EInfix (noPos x) y f (noPos z) instance NoPos (UpdField name) where noPos (UpdField h xs e) = UpdField h xs (noPos e) diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index b5feaa1c3..62ca0e680 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -210,34 +210,35 @@ tnamesDef (DExpr e) = tnamesE e tnamesE :: Ord name => Expr name -> Set name tnamesE expr = case expr of - EVar _ -> Set.empty - ELit _ -> Set.empty - ENeg e -> tnamesE e - EComplement e -> tnamesE e - EGenerate e -> tnamesE e - ETuple es -> Set.unions (map tnamesE es) - ERecord fs -> Set.unions (map (tnamesE . value) fs) - ESel e _ -> tnamesE e - EUpd mb fs -> let e = maybe Set.empty tnamesE mb - in Set.unions (e : map tnamesUF fs) - EList es -> Set.unions (map tnamesE es) - EFromTo a b c -> Set.union (tnamesT a) - (Set.union (maybe Set.empty tnamesT b) (tnamesT c)) - EInfFrom e e' -> Set.union (tnamesE e) (maybe Set.empty tnamesE e') - EComp e mss -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss))) - EApp e1 e2 -> Set.union (tnamesE e1) (tnamesE e2) - EAppT e fs -> Set.union (tnamesE e) (Set.unions (map tnamesTI fs)) - EIf e1 e2 e3 -> Set.union (tnamesE e1) (Set.union (tnamesE e2) (tnamesE e3)) - EWhere e ds -> let (bs,xs) = tnamesDs ds - in Set.union (boundNames bs (tnamesE e)) xs - ETyped e t -> Set.union (tnamesE e) (tnamesT t) - ETypeVal t -> tnamesT t - EFun ps e -> Set.union (Set.unions (map tnamesP ps)) (tnamesE e) - ELocated e _ -> tnamesE e - - ESplit e -> tnamesE e - EParens e -> tnamesE e - EInfix a _ _ b-> Set.union (tnamesE a) (tnamesE b) + EVar _ -> Set.empty + ELit _ -> Set.empty + ENeg e -> tnamesE e + EComplement e -> tnamesE e + EGenerate e -> tnamesE e + ETuple es -> Set.unions (map tnamesE es) + ERecord fs -> Set.unions (map (tnamesE . value) fs) + ESel e _ -> tnamesE e + EUpd mb fs -> let e = maybe Set.empty tnamesE mb + in Set.unions (e : map tnamesUF fs) + EList es -> Set.unions (map tnamesE es) + EFromTo a b c -> tnamesT a + `Set.union` maybe Set.empty tnamesT b + `Set.union` tnamesT c + EInfFrom e e' -> Set.union (tnamesE e) (maybe Set.empty tnamesE e') + EComp e mss -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss))) + EApp e1 e2 -> Set.union (tnamesE e1) (tnamesE e2) + EAppT e fs -> Set.union (tnamesE e) (Set.unions (map tnamesTI fs)) + EIf e1 e2 e3 -> Set.union (tnamesE e1) (Set.union (tnamesE e2) (tnamesE e3)) + EWhere e ds -> let (bs,xs) = tnamesDs ds + in Set.union (boundNames bs (tnamesE e)) xs + ETyped e t -> Set.union (tnamesE e) (tnamesT t) + ETypeVal t -> tnamesT t + EFun ps e -> Set.union (Set.unions (map tnamesP ps)) (tnamesE e) + ELocated e _ -> tnamesE e + + ESplit e -> tnamesE e + EParens e -> tnamesE e + EInfix a _ _ b -> Set.union (tnamesE a) (tnamesE b) tnamesUF :: Ord name => UpdField name -> Set name tnamesUF (UpdField _ _ e) = tnamesE e From 8b0e236eec79a47093c96e9eabdf6d2b92a9f67d Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 27 Jun 2019 14:31:06 -0700 Subject: [PATCH 2/2] Support element type ascriptions on list enumerations: `[a,b..c:t]`. Cf. issue #625. --- src/Cryptol/ModuleSystem/Renamer.hs | 3 ++- src/Cryptol/Parser/AST.hs | 8 +++++--- src/Cryptol/Parser/Names.hs | 5 +++-- src/Cryptol/Parser/ParserUtils.hs | 29 +++++++++++++++++++++-------- src/Cryptol/TypeCheck/Infer.hs | 10 +++++++--- 5 files changed, 38 insertions(+), 17 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 532432d31..566c502ba 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -749,9 +749,10 @@ instance Rename Expr where EUpd mb fs -> do checkLabels fs EUpd <$> traverse rename mb <*> traverse rename fs EList es -> EList <$> traverse rename es - EFromTo s n e -> EFromTo <$> rename s + EFromTo s n e t -> EFromTo <$> rename s <*> traverse rename n <*> rename e + <*> traverse rename t EInfFrom a b -> EInfFrom<$> rename a <*> traverse rename b EComp e' bs -> do arms' <- traverse renameArm bs let (envs,bs') = unzip arms' diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 4a252e4c1..a49823996 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -294,7 +294,8 @@ data Expr n = EVar n -- ^ @ x @ | ESel (Expr n) Selector -- ^ @ e.l @ | EUpd (Maybe (Expr n)) [ UpdField n ] -- ^ @ { r | x = e } @ | EList [Expr n] -- ^ @ [1,2,3] @ - | EFromTo (Type n) (Maybe (Type n)) (Type n) -- ^ @[1, 5 .. 117 ] @ + | EFromTo (Type n) (Maybe (Type n)) (Type n) (Maybe (Type n)) + -- ^ @ [1, 5 .. 117 : t] @ | EInfFrom (Expr n) (Maybe (Expr n))-- ^ @ [1, 3 ...] @ | EComp (Expr n) [[Match n]] -- ^ @ [ 1 | x <- xs ] @ | EApp (Expr n) (Expr n) -- ^ @ f x @ @@ -704,8 +705,9 @@ instance (Show name, PPName name) => PP (Expr name) where ETuple es -> parens (commaSep (map pp es)) ERecord fs -> braces (commaSep (map (ppNamed "=") fs)) EList es -> brackets (commaSep (map pp es)) - EFromTo e1 e2 e3 -> brackets (pp e1 <.> step <+> text ".." <+> pp e3) + EFromTo e1 e2 e3 t1 -> brackets (pp e1 <.> step <+> text ".." <+> end) where step = maybe empty (\e -> comma <+> pp e) e2 + end = maybe (pp e3) (\t -> pp e3 <+> colon <+> pp t) t1 EInfFrom e1 e2 -> brackets (pp e1 <.> step <+> text "...") where step = maybe empty (\e -> comma <+> pp e) e2 EComp e mss -> brackets (pp e <+> vcat (map arm mss)) @@ -956,7 +958,7 @@ instance NoPos (Expr name) where ESel x y -> ESel (noPos x) y EUpd x y -> EUpd (noPos x) (noPos y) EList x -> EList (noPos x) - EFromTo x y z -> EFromTo (noPos x) (noPos y) (noPos z) + EFromTo x y z t -> EFromTo (noPos x) (noPos y) (noPos z) (noPos t) EInfFrom x y -> EInfFrom (noPos x) (noPos y) EComp x y -> EComp (noPos x) (noPos y) EApp x y -> EApp (noPos x) (noPos y) diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index 62ca0e680..08ab65b04 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -82,7 +82,7 @@ namesE expr = EUpd mb fs -> let e = maybe Set.empty namesE mb in Set.unions (e : map namesUF fs) EList es -> Set.unions (map namesE es) - EFromTo _ _ _ -> Set.empty + EFromTo{} -> Set.empty EInfFrom e e' -> Set.union (namesE e) (maybe Set.empty namesE e') EComp e arms -> let (dss,uss) = unzip (map namesArm arms) in Set.union (boundNames (concat dss) (namesE e)) @@ -221,9 +221,10 @@ tnamesE expr = EUpd mb fs -> let e = maybe Set.empty tnamesE mb in Set.unions (e : map tnamesUF fs) EList es -> Set.unions (map tnamesE es) - EFromTo a b c -> tnamesT a + EFromTo a b c t -> tnamesT a `Set.union` maybe Set.empty tnamesT b `Set.union` tnamesT c + `Set.union` maybe Set.empty tnamesT t EInfFrom e e' -> Set.union (tnamesE e) (maybe Set.empty tnamesE e') EComp e mss -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss))) EApp e1 e2 -> Set.union (tnamesE e1) (tnamesE e2) diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index c055ab12d..cbbe28a13 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -285,10 +285,27 @@ unOp f x = at (f,x) $ EApp f x binOp :: Expr PName -> Located PName -> Expr PName -> Expr PName binOp x f y = at (x,y) $ EInfix x f defaultFixity y +-- An element type ascription is allowed to appear on one of the arguments. eFromTo :: Range -> Expr PName -> Maybe (Expr PName) -> Expr PName -> ParseM (Expr PName) -eFromTo r e1 e2 e3 = EFromTo <$> exprToNumT r e1 - <*> mapM (exprToNumT r) e2 - <*> exprToNumT r e3 +eFromTo r e1 e2 e3 = + case (asETyped e1, asETyped =<< e2, asETyped e3) of + (Just (e1', t), Nothing, Nothing) -> eFromToType r e1' e2 e3 (Just t) + (Nothing, Just (e2', t), Nothing) -> eFromToType r e1 (Just e2') e3 (Just t) + (Nothing, Nothing, Just (e3', t)) -> eFromToType r e1 e2 e3' (Just t) + (Nothing, Nothing, Nothing) -> eFromToType r e1 e2 e3 Nothing + _ -> errorMessage r "A sequence enumeration may have at most one element type annotation." + where + asETyped (ELocated e _) = asETyped e + asETyped (ETyped e t) = Just (e, t) + asETyped _ = Nothing + +eFromToType :: + Range -> Expr PName -> Maybe (Expr PName) -> Expr PName -> Maybe (Type PName) -> ParseM (Expr PName) +eFromToType r e1 e2 e3 t = + EFromTo <$> exprToNumT r e1 + <*> mapM (exprToNumT r) e2 + <*> exprToNumT r e3 + <*> pure t exprToNumT :: Range -> Expr PName -> ParseM (Type PName) exprToNumT r expr = @@ -298,11 +315,7 @@ exprToNumT r expr = where bad = errorMessage (fromMaybe r (getLoc expr)) $ unlines [ "The boundaries of .. sequences should be valid numeric types." - , "The expression `" ++ show (pp expr) ++ "` is not." - , "" - , "If you were trying to specify the width of the elements," - , "you may add a type annotation outside the sequence. For example:" - , " [ 1 .. 10 ] : [_][16]" + , "The expression `" ++ show expr ++ "` is not." ] diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index ffd6c731d..6febe3c44 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -279,14 +279,18 @@ checkE expr tGoal = es' <- mapM (`checkE` a) es return (EList es' a) - P.EFromTo t1 mbt2 t3 -> + P.EFromTo t1 mbt2 t3 mety -> do l <- curRange + let fs0 = + case mety of + Just ety -> [("a", ety)] + Nothing -> [] let (c,fs) = case mbt2 of Nothing -> - ("fromTo", [ ("last", t3) ]) + ("fromTo", ("last", t3) : fs0) Just t2 -> - ("fromThenTo", [ ("next",t2), ("last",t3) ]) + ("fromThenTo", ("next",t2) : ("last",t3) : fs0) prim <- mkPrim c let e' = P.EAppT prim