diff options
Diffstat (limited to 'Jennisys/DafnyPrinter.fs')
| -rw-r--r-- | Jennisys/DafnyPrinter.fs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs index 495daba9..43536ceb 100644 --- a/Jennisys/DafnyPrinter.fs +++ b/Jennisys/DafnyPrinter.fs @@ -24,6 +24,14 @@ let rec PrintExpr ctx expr = | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id
| UnaryExpr(op,UnaryExpr(op2, e2)) -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))
| UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)
+ | BinaryExpr(strength,"in",lhs,BinaryExpr(_,"..",lo,hi)) ->
+ let needParens = strength <= ctx
+ let openParen = if needParens then "(" else ""
+ let closeParen = if needParens then ")" else ""
+ let loStr = PrintExpr strength lo
+ let hiStr = PrintExpr strength hi
+ let lhsStr = PrintExpr strength lhs
+ sprintf "%s%s <= %s && %s <= %s%s" openParen loStr lhsStr lhsStr hiStr closeParen
| BinaryExpr(strength,op,e0,e1) ->
let op =
match op with
|