mirror of
https://github.com/GaloisInc/cryptol.git
synced 2025-01-07 08:19:12 +03:00
Parsing of nested field updates
This commit is contained in:
parent
d0c2285b74
commit
9ca6ac7a82
@ -511,7 +511,7 @@ rec_expr :: { Expr PName }
|
||||
|
||||
field_expr :: { UpdField PName }
|
||||
: selector field_how expr { UpdField $2 [$1] $3 }
|
||||
| sels field_how expr { UpdField $2 (reverse $1) $3 }
|
||||
| sels field_how expr { UpdField $2 $1 $3 }
|
||||
| sels apats field_how expr { UpdField $3 $1 (EFun $2 $4) } -- ???
|
||||
|
||||
field_how :: { UpdHow }
|
||||
@ -519,7 +519,7 @@ field_how :: { UpdHow }
|
||||
| '->' { UpdFun }
|
||||
|
||||
sels :: { [ Located Selector ] }
|
||||
: sel_expr { undefined }
|
||||
: sel_expr {% selExprToSels $1 }
|
||||
|
||||
field_exprs :: { [UpdField PName] }
|
||||
: field_expr { [$1] }
|
||||
|
@ -584,5 +584,23 @@ ufToNamed (UpdField h ls e) =
|
||||
_ -> errorMessage (srcRange (head ls))
|
||||
"Invalid record field. Perhaps you meant to update a record?"
|
||||
|
||||
selExprToSels :: Expr PName -> ParseM [Located Selector]
|
||||
selExprToSels e0 = reverse <$> go noLoc e0
|
||||
where
|
||||
noLoc = panic "selExprToSels" ["Missing location?"]
|
||||
go loc expr =
|
||||
case expr of
|
||||
ELocated e1 r -> go r e1
|
||||
ESel e2 s ->
|
||||
do ls <- go loc e2
|
||||
let rng = loc { from = to (srcRange (head ls)) }
|
||||
pure (Located { thing = s, srcRange = rng } : ls)
|
||||
EVar (UnQual l) ->
|
||||
pure [ Located { thing = RecordSel l Nothing, srcRange = loc } ]
|
||||
ELit (ECNum n _) ->
|
||||
pure [ Located { thing = TupleSel (fromInteger n) Nothing
|
||||
, srcRange = loc } ]
|
||||
_ -> errorMessage loc "Invalid label in record update."
|
||||
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user