GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 01:13:34 +03:00
Code Issues Projects Releases Wiki Activity

Remove [x..] and [x,y..] syntax from Cryptol.

Browse Source
This commit is contained in:
Brian Huffman 2019-02-27 16:36:53 -08:00
parent c387dbe5fd
commit 61a17adb02
6 changed files with 16 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -790,7 +790,7 @@ instance Rename Expr where
EList es -> EList <$> traverse rename es
EFromTo s n e'-> EFromTo <$> rename s
<*> traverse rename n
<*> traverse rename e'
<*> rename e'
EInfFrom a b -> EInfFrom<$> rename a <*> traverse rename b
EComp e' bs -> do arms' <- traverse renameArm bs
let (envs,bs') = unzip arms'

6
src/Cryptol/Parser.y
View File

@ -537,10 +537,8 @@ list_expr :: { Expr PName }
is being parsed. For this reason, we use `expr` temporarily and
then convert it to the corresponding type in the AST. -}
| expr '..' {% eFromTo $2 $1 Nothing Nothing }
| expr '..' expr {% eFromTo $2 $1 Nothing (Just $3) }
| expr ',' expr '..' {% eFromTo $4 $1 (Just $3) Nothing }
| expr ',' expr '..' expr {% eFromTo $4 $1 (Just $3) (Just $5) }
| expr '..' expr {% eFromTo $2 $1 Nothing $3 }
| expr ',' expr '..' expr {% eFromTo $4 $1 (Just $3) $5 }
| expr '...' { EInfFrom $1 Nothing }
| expr ',' expr '...' { EInfFrom $1 (Just $3) }

5
src/Cryptol/Parser/AST.hs
View File

@ -267,7 +267,7 @@ 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)) (Maybe (Type n)) -- ^ @[1, 5 .. 117 ] @
| EFromTo (Type n) (Maybe (Type n)) (Type n) -- ^ @[1, 5 .. 117 ] @
| EInfFrom (Expr n) (Maybe (Expr n))-- ^ @ [1, 3 ...] @
| EComp (Expr n) [[Match n]] -- ^ @ [ 1 | x <- xs ] @
| EApp (Expr n) (Expr n) -- ^ @ f x @
@ -688,9 +688,8 @@ 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 ".." <+> end)
EFromTo e1 e2 e3 -> brackets (pp e1 <.> step <+> text ".." <+> pp e3)
where step = maybe empty (\e -> comma <+> pp e) e2
end = maybe empty pp e3
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))

2
src/Cryptol/Parser/Names.hs
View File

@ -236,7 +236,7 @@ tnamesE expr =
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) (maybe Set.empty tnamesT c))
(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)

5
src/Cryptol/Parser/ParserUtils.hs
View File

@ -284,10 +284,11 @@ 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
eFromTo :: Range -> Expr PName -> Maybe (Expr PName) -> Maybe (Expr PName) -> ParseM (Expr PName)
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
<*> mapM (exprToNumT r) e3
<*> exprToNumT r e3
exprToNumT :: Range -> Expr PName -> ParseM (Type PName)
exprToNumT r expr =
case translateExprToNumT expr of

34
src/Cryptol/TypeCheck/Infer.hs
View File

@ -31,7 +31,7 @@ import Cryptol.TypeCheck.AST hiding (tSub,tMul,tExp)
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Solve
import Cryptol.TypeCheck.SimpType(tSub,tMul,tExp,tAdd)
import Cryptol.TypeCheck.SimpType(tMul)
import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
checkPropSyn,checkNewtype,
checkParameterType,
@ -279,37 +279,13 @@ checkE expr tGoal =
es' <- mapM (`checkE` a) es
return (EList es' a)
P.EFromTo t1 Nothing Nothing ->
do rng <- curRange
fromThenPrim <- mkPrim' "fromThen"
let src = TypeParamInstNamed fromThenPrim (packIdent "bits")
bit <- newType src KNum
fstT <- checkTypeOfKind t1 KNum
let nextT = tAdd fstT (tNum (1::Int))
lenT = tSub (tExp (tNum (2::Int)) bit) fstT
appTys (P.EVar fromThenPrim)
[ Located rng (Just (packIdent x), y)
| (x,y) <- [ ("first", fstT)
, ("next", nextT)
, ("len", lenT)
, ("bits", bit) ]
] tGoal
P.EFromTo t1 mbt2 mbt3 ->
P.EFromTo t1 mbt2 t3 ->
do l <- curRange
let (c,fs) =
case (mbt2, mbt3) of
(Nothing, Nothing) -> tcPanic "checkE"
[ "EFromTo _ Nothing Nothing" ]
(Just t2, Nothing) ->
("fromThen", [ ("next", t2) ])
(Nothing, Just t3) ->
case mbt2 of
Nothing ->
("fromTo", [ ("last", t3) ])
(Just t2, Just t3) ->
Just t2 ->
("fromThenTo", [ ("next",t2), ("last",t3) ])
prim <- mkPrim c