GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-15 02:01:39 +03:00
Code Issues Projects Releases Wiki Activity

Support lhs indexing on record field constructors and updaters.

Browse Source 
For example, we can now write

    foo = { f : [8] -> [4][4][8] }
    foo = { f i @ j @ k = i + j + k }
This commit is contained in:
Brian Huffman 2019-06-19 10:30:28 -07:00
parent d94a37adea
commit 829c9b9494
2 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Cryptol/Parser.y
View File

@ -538,8 +538,12 @@ rec_expr :: { Expr PName }
field_expr :: { UpdField PName }
: selector field_how expr { UpdField $2 [$1] $3 }
| sels field_how expr { UpdField $2 $1 $3 }
| sels apats field_how expr { UpdField $3 $1 (EFun (reverse $2) $4) }
| selector apats field_how expr { UpdField $3 [$1] (EFun (reverse $2) $4) }
| sels apats_indices field_how expr
{ UpdField $3 $1 (EFun (reverse (fst $2))
(mkGenerate (reverse (snd $2)) $4)) }
| selector apats_indices field_how expr
{ UpdField $3 [$1] (EFun (reverse (fst $2))
(mkGenerate (reverse (snd $2)) $4)) }
field_how :: { UpdHow }
: '=' { UpdSet }

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

@ -438,11 +438,11 @@ mkIndexedDecl f (ps, ixs) e =
}
where
rhs :: Expr PName
rhs = foldr mkGenerate e (reverse ixs)
mkGenerate :: Pattern PName -> Expr PName -> Expr PName
mkGenerate pat body = EGenerate (EFun [pat] body)
rhs = mkGenerate (reverse ixs) e
mkGenerate :: [Pattern PName] -> Expr PName -> Expr PName
mkGenerate pats body =
foldr (\pat e -> EGenerate (EFun [pat] e)) body pats
mkIf :: [(Expr PName, Expr PName)] -> Expr PName -> Expr PName
mkIf ifThens theElse = foldr addIfThen theElse ifThens