From 829c9b9494ad073ecc5bf3dcef8355ba3fcf8d9a Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 19 Jun 2019 10:30:28 -0700 Subject: [PATCH] Support lhs indexing on record field constructors and updaters. For example, we can now write foo = { f : [8] -> [4][4][8] } foo = { f i @ j @ k = i + j + k } --- src/Cryptol/Parser.y | 8 ++++++-- src/Cryptol/Parser/ParserUtils.hs | 8 ++++---- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index d830d364..2e540bc6 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -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 } diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index bbcb850e..9bc2a022 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -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