Skip to content

Commit

Permalink
Merge pull request #1367 from GaloisInc/prefix-fixities
Browse files Browse the repository at this point in the history
Add fixities for prefix operators
  • Loading branch information
qsctr authored Jun 25, 2022
2 parents cfb1631 + 9b0a22a commit c6a795c
Show file tree
Hide file tree
Showing 12 changed files with 129 additions and 63 deletions.
20 changes: 17 additions & 3 deletions src/Cryptol/ModuleSystem/Renamer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -728,9 +728,6 @@ instance Rename Expr where
rename expr = case expr of
EVar n -> EVar <$> renameVar NameUse 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
Expand Down Expand Up @@ -786,6 +783,7 @@ instance Rename Expr where
x' <- rename x
z' <- rename z
mkEInfix x' op z'
EPrefix op e -> EPrefix op <$> rename e


checkLabels :: [UpdField PName] -> RenameM ()
Expand Down Expand Up @@ -830,6 +828,22 @@ mkEInfix e@(EInfix x o1 f1 y) op@(o2,f2) z =
FCError -> do record (FixityError o1 f1 o2 f2)
return (EInfix e o2 f2 z)

mkEInfix e@(EPrefix o1 x) op@(o2, f2) y =
case compareFixity (prefixFixity o1) f2 of
FCRight -> do
let warning = PrefixAssocChanged o1 x o2 f2 y
RenameM $ sets_ (\rw -> rw {rwWarnings = warning : rwWarnings rw})
r <- mkEInfix x op y
return (EPrefix o1 r)

-- Even if the fixities conflict, we make the prefix operator take
-- precedence.
_ -> return (EInfix e o2 f2 y)

-- Note that for prefix operator on RHS of infix operator we make the prefix
-- operator always have precedence, so we allow a * -b instead of requiring
-- a * (-b).

mkEInfix (ELocated e' _) op z =
mkEInfix e' op z

Expand Down
33 changes: 21 additions & 12 deletions src/Cryptol/ModuleSystem/Renamer/Error.hs
Original file line number Diff line number Diff line change
Expand Up @@ -161,27 +161,29 @@ instance PP DepName where
data RenamerWarning
= SymbolShadowed PName Name [Name]
| UnusedName Name
| PrefixAssocChanged PrefixOp (Expr Name) (Located Name) Fixity (Expr Name)
deriving (Show, Generic, NFData)

instance Eq RenamerWarning where
x == y = compare x y == EQ

-- used to determine in what order ot show things
-- used to determine in what order to show things
instance Ord RenamerWarning where
compare w1 w2 =
case w1 of
SymbolShadowed x y _ ->
case w2 of
SymbolShadowed x' y' _ -> compare (byStart y,x) (byStart y',x')
_ -> LT
UnusedName x ->
case w2 of
UnusedName y -> compare (byStart x) (byStart y)
_ -> GT
case (w1, w2) of
(SymbolShadowed x y _, SymbolShadowed x' y' _) ->
compare (byStart y, x) (byStart y', x')
(UnusedName x, UnusedName x') ->
compare (byStart x) (byStart x')
(PrefixAssocChanged _ _ op _ _, PrefixAssocChanged _ _ op' _ _) ->
compare (from $ srcRange op) (from $ srcRange op')
_ -> compare (priority w1) (priority w2)

where
byStart = from . nameLoc

priority SymbolShadowed {} = 0 :: Int
priority UnusedName {} = 1
priority PrefixAssocChanged {} = 2

instance PP RenamerWarning where
ppPrec _ (SymbolShadowed k x os) =
Expand All @@ -201,5 +203,12 @@ instance PP RenamerWarning where
hang (text "[warning] at" <+> pp (nameLoc x))
4 (text "Unused name:" <+> pp x)

ppPrec _ (PrefixAssocChanged prefixOp x infixOp infixFixity y) =
hang (text "[warning] at" <+> pp (srcRange infixOp))
4 $ fsep [ backticks (pp old)
, "is now parsed as"
, backticks (pp new) ]


where
old = EInfix (EPrefix prefixOp x) infixOp infixFixity y
new = EPrefix prefixOp (EInfix x infixOp infixFixity y)
8 changes: 4 additions & 4 deletions src/Cryptol/Parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -516,13 +516,13 @@ ifBranch :: { (Expr PName, Expr PName) }
: expr 'then' expr { ($1, $3) }

simpleRHS :: { Expr PName }
: '-' simpleApp { at ($1,$2) (ENeg $2) }
| '~' simpleApp { at ($1,$2) (EComplement $2) }
: '-' simpleApp { at ($1,$2) (EPrefix PrefixNeg $2) }
| '~' simpleApp { at ($1,$2) (EPrefix PrefixComplement $2) }
| simpleApp { $1 }

longRHS :: { Expr PName }
: '-' longApp { at ($1,$2) (ENeg $2) }
| '~' longApp { at ($1,$2) (EComplement $2) }
: '-' longApp { at ($1,$2) (EPrefix PrefixNeg $2) }
| '~' longApp { at ($1,$2) (EPrefix PrefixComplement $2) }
| longApp { $1 }


Expand Down
28 changes: 22 additions & 6 deletions src/Cryptol/Parser/AST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,8 @@ module Cryptol.Parser.AST
, UpdHow(..)
, FunDesc(..)
, emptyFunDesc
, PrefixOp(..)
, prefixFixity

-- * Positions
, Located(..)
Expand Down Expand Up @@ -341,8 +343,6 @@ data Literal = ECNum Integer NumInfo -- ^ @0x10@ (HexLit 2)

data Expr n = EVar n -- ^ @ x @
| ELit Literal -- ^ @ 0x10 @
| ENeg (Expr n) -- ^ @ -1 @
| EComplement (Expr n) -- ^ @ ~1 @
| EGenerate (Expr n) -- ^ @ generate f @
| ETuple [Expr n] -- ^ @ (1,2,3) @
| ERecord (Rec (Expr n)) -- ^ @ { x = 1, y = 2 } @
Expand Down Expand Up @@ -373,8 +373,20 @@ data Expr n = EVar n -- ^ @ x @
| ESplit (Expr n) -- ^ @ splitAt x @ (Introduced by NoPat)
| EParens (Expr n) -- ^ @ (e) @ (Removed by Fixity)
| EInfix (Expr n) (Located n) Fixity (Expr n)-- ^ @ a + b @ (Removed by Fixity)
| EPrefix PrefixOp (Expr n) -- ^ @ -1, ~1 @
deriving (Eq, Show, Generic, NFData, Functor)

-- | Prefix operator.
data PrefixOp = PrefixNeg -- ^ @ - @
| PrefixComplement -- ^ @ ~ @
deriving (Eq, Show, Generic, NFData)

prefixFixity :: PrefixOp -> Fixity
prefixFixity op = Fixity { fAssoc = LeftAssoc, .. }
where fLevel = case op of
PrefixNeg -> 80
PrefixComplement -> 100

-- | Description of functions. Only trivial information is provided here
-- by the parser. The NoPat pass fills this in as required.
data FunDesc n =
Expand Down Expand Up @@ -816,8 +828,6 @@ instance (Show name, PPName name) => PP (Expr name) where
EVar x -> ppPrefixName x
ELit x -> pp x

ENeg x -> wrap n 3 (text "-" <.> ppPrec 4 x)
EComplement x -> wrap n 3 (text "~" <.> ppPrec 4 x)
EGenerate x -> wrap n 3 (text "generate" <+> ppPrec 4 x)

ETuple es -> parens (commaSep (map pp es))
Expand Down Expand Up @@ -877,12 +887,19 @@ instance (Show name, PPName name) => PP (Expr name) where

EParens e -> parens (pp e)

-- NOTE: these don't produce correctly parenthesized expressions without
-- explicit EParens nodes when necessary, since we don't check the actual
-- fixities of the operators.
EInfix e1 op _ e2 -> wrap n 0 (pp e1 <+> ppInfixName (thing op) <+> pp e2)

EPrefix op e -> wrap n 3 (text (prefixText op) <.> ppPrec 4 e)
where
isInfix (EApp (EApp (EVar ieOp) ieLeft) ieRight) = do
ieFixity <- ppNameFixity ieOp
return Infix { .. }
isInfix _ = Nothing
prefixText PrefixNeg = "-"
prefixText PrefixComplement = "~"

instance (Show name, PPName name) => PP (UpdField name) where
ppPrec _ (UpdField h xs e) = ppNestedSels (map thing xs) <+> pp h <+> pp e
Expand Down Expand Up @@ -1082,8 +1099,6 @@ instance NoPos (Expr name) where
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 (fmap noPos x)
Expand All @@ -1110,6 +1125,7 @@ instance NoPos (Expr name) where
ESplit x -> ESplit (noPos x)
EParens e -> EParens (noPos e)
EInfix x y f z -> EInfix (noPos x) y f (noPos z)
EPrefix op x -> EPrefix op (noPos x)

instance NoPos (UpdField name) where
noPos (UpdField h xs e) = UpdField h xs (noPos e)
Expand Down
6 changes: 2 additions & 4 deletions src/Cryptol/Parser/Names.hs
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,6 @@ namesE expr =
case expr of
EVar x -> Set.singleton x
ELit _ -> Set.empty
ENeg e -> namesE e
EComplement e -> namesE e
EGenerate e -> namesE e
ETuple es -> Set.unions (map namesE es)
ERecord fs -> Set.unions (map (namesE . snd) (recordElements fs))
Expand Down Expand Up @@ -102,6 +100,7 @@ namesE expr =
ESplit e -> namesE e
EParens e -> namesE e
EInfix a o _ b-> Set.insert (thing o) (Set.union (namesE a) (namesE b))
EPrefix _ e -> namesE e

namesUF :: Ord name => UpdField name -> Set name
namesUF (UpdField _ _ e) = namesE e
Expand Down Expand Up @@ -192,8 +191,6 @@ 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 . snd) (recordElements fs))
Expand Down Expand Up @@ -224,6 +221,7 @@ tnamesE expr =
ESplit e -> tnamesE e
EParens e -> tnamesE e
EInfix a _ _ b -> Set.union (tnamesE a) (tnamesE b)
EPrefix _ e -> tnamesE e

tnamesUF :: Ord name => UpdField name -> Set name
tnamesUF (UpdField _ _ e) = tnamesE e
Expand Down
3 changes: 1 addition & 2 deletions src/Cryptol/Parser/NoPat.hs
Original file line number Diff line number Diff line change
Expand Up @@ -150,8 +150,6 @@ noPatE expr =
case expr of
EVar {} -> return expr
ELit {} -> return expr
ENeg e -> ENeg <$> noPatE e
EComplement e -> EComplement <$> noPatE e
EGenerate e -> EGenerate <$> noPatE e
ETuple es -> ETuple <$> mapM noPatE es
ERecord es -> ERecord <$> traverse (traverse noPatE) es
Expand All @@ -176,6 +174,7 @@ noPatE expr =
ESplit e -> ESplit <$> noPatE e
EParens e -> EParens <$> noPatE e
EInfix x y f z-> EInfix <$> noPatE x <*> pure y <*> pure f <*> noPatE z
EPrefix op e -> EPrefix op <$> noPatE e


noPatUF :: UpdField PName -> NoPatM (UpdField PName)
Expand Down
24 changes: 16 additions & 8 deletions src/Cryptol/REPL/Command.hs
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,8 @@ import Cryptol.REPL.Browse
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
import qualified Cryptol.ModuleSystem.Renamer as M
(RenamerWarning(SymbolShadowed, PrefixAssocChanged))
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.ModuleSystem.Env as M

Expand Down Expand Up @@ -1493,8 +1494,9 @@ liftModuleCmd cmd =

moduleCmdResult :: M.ModuleRes a -> REPL a
moduleCmdResult (res,ws0) = do
warnDefaulting <- getKnownUser "warnDefaulting"
warnShadowing <- getKnownUser "warnShadowing"
warnDefaulting <- getKnownUser "warnDefaulting"
warnShadowing <- getKnownUser "warnShadowing"
warnPrefixAssoc <- getKnownUser "warnPrefixAssoc"
-- XXX: let's generalize this pattern
let isDefaultWarn (T.DefaultingTo _ _) = True
isDefaultWarn _ = False
Expand All @@ -1509,14 +1511,20 @@ moduleCmdResult (res,ws0) = do
isShadowWarn (M.SymbolShadowed {}) = True
isShadowWarn _ = False

filterShadowing w | warnShadowing = Just w
filterShadowing (M.RenamerWarnings xs) =
case filter (not . isShadowWarn) xs of
isPrefixAssocWarn (M.PrefixAssocChanged {}) = True
isPrefixAssocWarn _ = False

filterRenamer True _ w = Just w
filterRenamer _ check (M.RenamerWarnings xs) =
case filter (not . check) xs of
[] -> Nothing
ys -> Just (M.RenamerWarnings ys)
filterShadowing w = Just w
filterRenamer _ _ w = Just w

let ws = mapMaybe filterDefaults . mapMaybe filterShadowing $ ws0
let ws = mapMaybe filterDefaults
. mapMaybe (filterRenamer warnShadowing isShadowWarn)
. mapMaybe (filterRenamer warnPrefixAssoc isPrefixAssocWarn)
$ ws0
names <- M.mctxNameDisp <$> getFocusedEnv
mapM_ (rPrint . runDoc names . pp) ws
case res of
Expand Down
2 changes: 2 additions & 0 deletions src/Cryptol/REPL/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -898,6 +898,8 @@ userOptions = mkOptionMap
"Choose whether to display warnings when defaulting."
, simpleOpt "warnShadowing" ["warn-shadowing"] (EnvBool True) noCheck
"Choose whether to display warnings when shadowing symbols."
, simpleOpt "warnPrefixAssoc" ["warn-prefix-assoc"] (EnvBool True) noCheck
"Choose whether to display warnings when expression association has changed due to new prefix operator fixities."
, simpleOpt "warnUninterp" ["warn-uninterp"] (EnvBool True) noCheck
"Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
, simpleOpt "smtFile" ["smt-file"] (EnvString "-") noCheck
Expand Down
17 changes: 7 additions & 10 deletions src/Cryptol/TypeCheck/Infer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -157,8 +157,6 @@ appTys expr ts tGoal =
cs <- getCallStacks
if cs then pure (ELocated r e') else pure e'

P.ENeg {} -> mono
P.EComplement {} -> mono
P.EGenerate {} -> mono

P.ETuple {} -> mono
Expand All @@ -178,6 +176,7 @@ appTys expr ts tGoal =
P.ETypeVal {} -> mono
P.EFun {} -> mono
P.ESplit {} -> mono
P.EPrefix {} -> mono

P.EParens e -> appTys e ts tGoal
P.EInfix a op _ b -> appTys (P.EVar (thing op) `P.EApp` a `P.EApp` b) ts tGoal
Expand Down Expand Up @@ -221,14 +220,6 @@ checkE expr tGoal =
checkHasType t tGoal
return e'

P.ENeg e ->
do prim <- mkPrim "negate"
checkE (P.EApp prim e) tGoal

P.EComplement e ->
do prim <- mkPrim "complement"
checkE (P.EApp prim e) tGoal

P.EGenerate e ->
do prim <- mkPrim "generate"
checkE (P.EApp prim e) tGoal
Expand Down Expand Up @@ -454,6 +445,12 @@ checkE expr tGoal =

P.EInfix a op _ b -> checkE (P.EVar (thing op) `P.EApp` a `P.EApp` b) tGoal

P.EPrefix op e ->
do prim <- mkPrim case op of
P.PrefixNeg -> "negate"
P.PrefixComplement -> "complement"
checkE (P.EApp prim e) tGoal

P.EParens e -> checkE e tGoal


Expand Down
15 changes: 15 additions & 0 deletions tests/issues/issue1322.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// ^^ has higher precedence than -
-2^^8 : Integer

// - allowed in second operand
3 + -2 : Integer

// >> has lower precedence than -
-1 >> 2 : [3]

// ~ is still highest precedence
~2^^2 : [3]

// disable new behavior warning
:set warnPrefixAssoc=off
-2^^8 : Integer
8 changes: 8 additions & 0 deletions tests/issues/issue1322.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
Loading module Cryptol
[warning] at issue1322.icry:2:3--2:5
`-2 ^^ 8` is now parsed as `-(2 ^^ 8)`
-256
1
0x1
0x1
-256
Loading

0 comments on commit c6a795c

Please sign in to comment.