mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 09:23:04 +03:00
Support indexing on the left-hand sides of declarations.
The declaration `xs @ i = e` is syntactic sugar for `xs = generate (\i -> e)`.
This commit is contained in:
Brian Huffman
parent
0a1cea2912
commit
69ebb77a56
@ -495,6 +495,9 @@ primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a
|
||||
/**
|
||||
* Produce a sequence using a generating function.
|
||||
* Satisfies 'generate f @ i == f i' for all 'i' between '0' and 'n-1'.
|
||||
*
|
||||
* Declarations of the form 'x @ i = e' are syntactic sugar for
|
||||
* 'x = generate (\i -> e)'.
|
||||
*/
|
||||
generate : {n, ix, a}
|
||||
(fin ix, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a
|
||||
|
||||
@ -788,6 +788,8 @@ instance Rename Expr where
|
||||
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
|
||||
|
||||
@ -48,7 +48,7 @@ import Paths_cryptol
|
||||
expressions, for example `[ 12 .. _ ]`.
|
||||
-}
|
||||
|
||||
%expect 1
|
||||
-- %expect 1
|
||||
|
||||
|
||||
%token
|
||||
@ -120,6 +120,7 @@ import Paths_cryptol
|
||||
'~' { Located $$ (Token (Op Complement) _)}
|
||||
|
||||
'#' { Located $$ (Token (Op Hash) _)}
|
||||
'@' { Located $$ (Token (Op At) _)}
|
||||
|
||||
OP { $$@(Located _ (Token (Op (Other [] _)) _))}
|
||||
QOP { $$@(Located _ (Token (Op Other{} ) _))}
|
||||
@ -288,17 +289,8 @@ decl :: { Decl PName }
|
||||
: vars_comma ':' schema { at (head $1,$3) $ DSignature (reverse $1) $3 }
|
||||
| ipat '=' expr { at ($1,$3) $ DPatBind $1 $3 }
|
||||
| '(' op ')' '=' expr { at ($1,$5) $ DPatBind (PVar $2) $5 }
|
||||
| var apats '=' expr { at ($1,$4) $
|
||||
DBind $ Bind { bName = $1
|
||||
, bParams = reverse $2
|
||||
, bDef = at $4 (Located emptyRange (DExpr $4))
|
||||
, bSignature = Nothing
|
||||
, bPragmas = []
|
||||
, bMono = False
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
} }
|
||||
| var apats_indices '=' expr
|
||||
{ at ($1,$4) $ mkIndexedDecl $1 $2 $4 }
|
||||
|
||||
| apat pat_op apat '=' expr
|
||||
{ at ($1,$5) $
|
||||
@ -329,17 +321,7 @@ decl :: { Decl PName }
|
||||
|
||||
let_decl :: { Decl PName }
|
||||
: 'let' ipat '=' expr { at ($2,$4) $ DPatBind $2 $4 }
|
||||
| 'let' name apats '=' expr { at ($2,$5) $
|
||||
DBind $ Bind { bName = $2
|
||||
, bParams = reverse $3
|
||||
, bDef = at $5 (Located emptyRange (DExpr $5))
|
||||
, bSignature = Nothing
|
||||
, bPragmas = []
|
||||
, bMono = False
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
} }
|
||||
| 'let' name apats_indices '=' expr { at ($2,$5) $ mkIndexedDecl $2 $3 $5 }
|
||||
|
||||
newtype :: { Newtype PName }
|
||||
: 'newtype' qname '=' newtype_body
|
||||
@ -363,6 +345,18 @@ apats :: { [Pattern PName] }
|
||||
: apat { [$1] }
|
||||
| apats apat { $2 : $1 }
|
||||
|
||||
indices :: { [Pattern PName] }
|
||||
: '@' indices1 { $2 }
|
||||
| {- empty -} { [] }
|
||||
|
||||
indices1 :: { [Pattern PName] }
|
||||
: apat { [$1] }
|
||||
| indices1 '@' apat { $3 : $1 }
|
||||
|
||||
apats_indices :: { ([Pattern PName], [Pattern PName]) }
|
||||
: apats indices { ($1, $2) }
|
||||
| '@' indices1 { ([], $2) }
|
||||
|
||||
decls :: { [Decl PName] }
|
||||
: decl ';' { [$1] }
|
||||
| decls decl ';' { $2 : $1 }
|
||||
@ -392,6 +386,7 @@ qop :: { LPName }
|
||||
op :: { LPName }
|
||||
: pat_op { $1 }
|
||||
| '#' { Located $1 $ mkUnqual $ mkInfix "#" }
|
||||
| '@' { Located $1 $ mkUnqual $ mkInfix "@" }
|
||||
|
||||
pat_op :: { LPName }
|
||||
: other_op { $1 }
|
||||
|
||||
@ -270,6 +270,7 @@ 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 [Named (Expr n)] -- ^ @ { x = 1, y = 2 } @
|
||||
| ESel (Expr n) Selector -- ^ @ e.l @
|
||||
@ -701,6 +702,7 @@ instance (Show name, PPName name) => PP (Expr name) where
|
||||
|
||||
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))
|
||||
ERecord fs -> braces (commaSep (map (ppNamed "=") fs))
|
||||
@ -966,6 +968,7 @@ instance NoPos (Expr name) where
|
||||
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
|
||||
|
||||
@ -164,6 +164,9 @@ $white+ { emit $ White Space }
|
||||
-- hash is used as a kind, and as a pattern
|
||||
"#" { emit (Op Hash ) }
|
||||
|
||||
-- at-sign is used in declaration bindings
|
||||
"@" { emit (Op At ) }
|
||||
|
||||
-- ~ is used for unary complement
|
||||
"~" { emit (Op Complement) }
|
||||
|
||||
|
||||
@ -399,7 +399,7 @@ data TokenKW = KW_else
|
||||
-- used for all other cases that lexed as an operator.
|
||||
data TokenOp = Plus | Minus | Mul | Div | Exp | Mod
|
||||
| Equal | LEQ | GEQ
|
||||
| Complement | Hash
|
||||
| Complement | Hash | At
|
||||
| Other [T.Text] T.Text
|
||||
deriving (Eq, Show, Generic, NFData)
|
||||
|
||||
|
||||
@ -81,6 +81,7 @@ namesE expr =
|
||||
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 . value) fs)
|
||||
ESel e _ -> namesE e
|
||||
@ -229,6 +230,7 @@ tnamesE expr =
|
||||
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
|
||||
|
||||
@ -148,6 +148,7 @@ noPatE 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 <$> mapM noPatF es
|
||||
ESel e s -> ESel <$> noPatE e <*> return s
|
||||
|
||||
@ -422,6 +422,28 @@ mkProperty f ps e = DBind Bind { bName = f
|
||||
, bDoc = Nothing
|
||||
}
|
||||
|
||||
-- NOTE: The lists of patterns are reversed!
|
||||
mkIndexedDecl ::
|
||||
LPName -> ([Pattern PName], [Pattern PName]) -> Expr PName -> Decl PName
|
||||
mkIndexedDecl f (ps, ixs) e =
|
||||
DBind Bind { bName = f
|
||||
, bParams = reverse ps
|
||||
, bDef = at e (Located emptyRange (DExpr rhs))
|
||||
, bSignature = Nothing
|
||||
, bPragmas = []
|
||||
, bMono = False
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
}
|
||||
where
|
||||
rhs :: Expr PName
|
||||
rhs = foldr mkGenerate e (reverse ixs)
|
||||
|
||||
mkGenerate :: Pattern PName -> Expr PName -> Expr PName
|
||||
mkGenerate pat body = EGenerate (EFun [pat] body)
|
||||
|
||||
|
||||
mkIf :: [(Expr PName, Expr PName)] -> Expr PName -> Expr PName
|
||||
mkIf ifThens theElse = foldr addIfThen theElse ifThens
|
||||
where
|
||||
|
||||
@ -164,6 +164,7 @@ appTys expr ts tGoal =
|
||||
|
||||
P.ENeg {} -> mono
|
||||
P.EComplement {} -> mono
|
||||
P.EGenerate {} -> mono
|
||||
|
||||
P.ETuple {} -> mono
|
||||
P.ERecord {} -> mono
|
||||
@ -230,6 +231,10 @@ checkE expr tGoal =
|
||||
do prim <- mkPrim "complement"
|
||||
checkE (P.EApp prim e) tGoal
|
||||
|
||||
P.EGenerate e ->
|
||||
do prim <- mkPrim "generate"
|
||||
checkE (P.EApp prim e) tGoal
|
||||
|
||||
P.ELit l@(P.ECNum _ P.DecLit) ->
|
||||
do e <- desugarLiteral False l
|
||||
-- NOTE: When 'l' is a decimal literal, 'desugarLiteral' does
|
||||
|
||||
Loading…
Reference in New Issue
Block a user