Skip to content

Commit

Permalink
Merge pull request #628 from GaloisInc/issue625
Browse files Browse the repository at this point in the history 
Issue625
  • Loading branch information
brianhuffman authored Jun 28, 2019
2 parents 1e11ff6 + 8b0e236 commit c5dec74
Show file tree
Hide file tree
Showing 5 changed files with 132 additions and 110 deletions.
87 changes: 44 additions & 43 deletions src/Cryptol/ModuleSystem/Renamer.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -736,49 +736,50 @@ 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 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'
-- 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 ()
Expand Down
56 changes: 29 additions & 27 deletions src/Cryptol/Parser/AST.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 @
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -946,31 +948,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 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)
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)
Expand Down
60 changes: 31 additions & 29 deletions src/Cryptol/Parser/Names.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down Expand Up @@ -210,34 +210,36 @@ 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 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)
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
Expand Down
29 changes: 21 additions & 8 deletions src/Cryptol/Parser/ParserUtils.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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."
]


Expand Down
10 changes: 7 additions & 3 deletions src/Cryptol/TypeCheck/Infer.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit c5dec74

Please sign in to comment.