From c07a2d148c97c1543e065e591a014b7870554bfa Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 8 Sep 2022 14:26:42 -0500 Subject: [PATCH 1/2] Formatter Pass This PR used the formatter being developed in #2399 to format all the dafny files --- src/AST/Predicates.dfy | 332 ++++----- src/AST/Syntax.dfy | 574 +++++++-------- src/AST/Translator.dfy | 182 ++--- src/Passes/EliminateNegatedBinops.dfy | 52 +- src/Passes/Pass.dfy | 8 +- src/Passes/SimplifyEmptyBlocks.dfy | 990 +++++++++++++------------- src/REPL/Repl.dfy | 466 ++++++------ src/Semantics/Equiv.dfy | 214 +++--- src/Semantics/Interp.dfy | 584 +++++++-------- src/Semantics/Printer.dfy | 24 +- src/Semantics/Pure.dfy | 70 +- src/Semantics/Values.dfy | 88 +-- src/Transforms/BottomUp.dfy | 70 +- src/Transforms/Generic.dfy | 2 +- src/Utils/Library.dfy | 630 ++++++++-------- src/Utils/StrTree.dfy | 18 +- 16 files changed, 2152 insertions(+), 2152 deletions(-) diff --git a/src/AST/Predicates.dfy b/src/AST/Predicates.dfy index 69cae7dd..713c77bc 100644 --- a/src/AST/Predicates.dfy +++ b/src/AST/Predicates.dfy @@ -1,213 +1,213 @@ include "Syntax.dfy" module Bootstrap.AST.Predicates { -module Shallow { - import opened Utils.Lib - import opened Syntax + module Shallow { + import opened Utils.Lib + import opened Syntax - function method All_Method(m: Method, P: Expr -> bool) : bool { - match m { - case Method(CompileName_, methodBody) => P(methodBody) + function method All_Method(m: Method, P: Expr -> bool) : bool { + match m { + case Method(CompileName_, methodBody) => P(methodBody) + } } - } - function method All_Program(p: Program, P: Expr -> bool) : bool { - match p { - case Program(mainMethod) => All_Method(mainMethod, P) + function method All_Program(p: Program, P: Expr -> bool) : bool { + match p { + case Program(mainMethod) => All_Method(mainMethod, P) + } } - } - function method All(p: Program, P: Expr -> bool) : bool { - All_Program(p, P) + function method All(p: Program, P: Expr -> bool) : bool { + All_Program(p, P) + } } -} -module DeepImpl { -abstract module Base { - import opened Utils.Lib - import opened Syntax - import Shallow + module DeepImpl { + abstract module Base { + import opened Utils.Lib + import opened Syntax + import Shallow - // - // Functions - // + // + // Functions + // - function method AllChildren_Expr(e: Expr, P: Expr -> bool) : bool - decreases e.Depth(), 0 + function method AllChildren_Expr(e: Expr, P: Expr -> bool) : bool + decreases e.Depth(), 0 - function method All_Expr(e: Expr, P: Expr -> bool) - : (b: bool) - decreases e.Depth(), 1 + function method All_Expr(e: Expr, P: Expr -> bool) + : (b: bool) + decreases e.Depth(), 1 - function method All_Method(m: Method, P: Expr -> bool) : bool { - Shallow.All_Method(m, e => All_Expr(e, P)) - } + function method All_Method(m: Method, P: Expr -> bool) : bool { + Shallow.All_Method(m, e => All_Expr(e, P)) + } - function method All_Program(p: Program, P: Expr -> bool) : bool { - Shallow.All_Program(p, e => All_Expr(e, P)) - } + function method All_Program(p: Program, P: Expr -> bool) : bool { + Shallow.All_Program(p, e => All_Expr(e, P)) + } - // - // Lemmas - // - - // This lemma allows callers to force one level of unfolding of All_Expr - lemma AllImpliesChildren(e: Expr, p: Expr -> bool) - requires All_Expr(e, p) - ensures AllChildren_Expr(e, p) - - lemma AllChildren_Expr_weaken(e: Exprs.T, P: Exprs.T -> bool, Q: Exprs.T -> bool) - requires AllChildren_Expr(e, P) - requires forall e' :: P(e') ==> Q(e') - decreases e, 0 - ensures AllChildren_Expr(e, Q) - - lemma All_Expr_weaken(e: Exprs.T, P: Exprs.T -> bool, Q: Exprs.T -> bool) - requires All_Expr(e, P) - requires forall e' :: P(e') ==> Q(e') - decreases e, 1 - ensures All_Expr(e, Q) - - lemma All_Expr_True(e: Expr, f: Expr -> bool) - requires forall e :: f(e) - ensures All_Expr(e, f) - decreases e, 1 - - lemma AllChildren_Expr_True(e: Expr, f: Expr -> bool) - requires forall e :: f(e) - ensures AllChildren_Expr(e, f) - decreases e, 0 - - lemma All_Expr_True_Forall(f: Expr -> bool) - requires forall e :: f(e) - ensures forall e :: All_Expr(e, f) -} + // + // Lemmas + // + + // This lemma allows callers to force one level of unfolding of All_Expr + lemma AllImpliesChildren(e: Expr, p: Expr -> bool) + requires All_Expr(e, p) + ensures AllChildren_Expr(e, p) + + lemma AllChildren_Expr_weaken(e: Exprs.T, P: Exprs.T -> bool, Q: Exprs.T -> bool) + requires AllChildren_Expr(e, P) + requires forall e' :: P(e') ==> Q(e') + decreases e, 0 + ensures AllChildren_Expr(e, Q) + + lemma All_Expr_weaken(e: Exprs.T, P: Exprs.T -> bool, Q: Exprs.T -> bool) + requires All_Expr(e, P) + requires forall e' :: P(e') ==> Q(e') + decreases e, 1 + ensures All_Expr(e, Q) + + lemma All_Expr_True(e: Expr, f: Expr -> bool) + requires forall e :: f(e) + ensures All_Expr(e, f) + decreases e, 1 + + lemma AllChildren_Expr_True(e: Expr, f: Expr -> bool) + requires forall e :: f(e) + ensures AllChildren_Expr(e, f) + decreases e, 0 + + lemma All_Expr_True_Forall(f: Expr -> bool) + requires forall e :: f(e) + ensures forall e :: All_Expr(e, f) + } - module Rec refines Base { // DISCUSS - function method All_Expr(e: Expr, P: Expr -> bool) : (b: bool) { - P(e) && - // BUG(https://github.com/dafny-lang/dafny/issues/2107) - // BUG(https://github.com/dafny-lang/dafny/issues/2109) - // Duplicated to avoid mutual recursion with AllChildren_Expr - match e { - case Var(_) => true - case Literal(lit) => true - case Abs(vars, body) => All_Expr(body, P) - case Apply(_, exprs) => - Seq.All(e requires e in exprs => All_Expr(e, P), exprs) - case Block(exprs) => - Seq.All((e requires e in exprs => All_Expr(e, P)), exprs) - case Bind(vars, vals, body) => - && Seq.All((e requires e in vals => All_Expr(e, P)), vals) - && All_Expr(body, P) - case If(cond, thn, els) => - All_Expr(cond, P) && All_Expr(thn, P) && All_Expr(els, P) + module Rec refines Base { // DISCUSS + function method All_Expr(e: Expr, P: Expr -> bool) : (b: bool) { + P(e) && + // BUG(https://github.com/dafny-lang/dafny/issues/2107) + // BUG(https://github.com/dafny-lang/dafny/issues/2109) + // Duplicated to avoid mutual recursion with AllChildren_Expr + match e { + case Var(_) => true + case Literal(lit) => true + case Abs(vars, body) => All_Expr(body, P) + case Apply(_, exprs) => + Seq.All(e requires e in exprs => All_Expr(e, P), exprs) + case Block(exprs) => + Seq.All((e requires e in exprs => All_Expr(e, P)), exprs) + case Bind(vars, vals, body) => + && Seq.All((e requires e in vals => All_Expr(e, P)), vals) + && All_Expr(body, P) + case If(cond, thn, els) => + All_Expr(cond, P) && All_Expr(thn, P) && All_Expr(els, P) + } } - } - function method AllChildren_Expr(e: Expr, P: Expr -> bool) : bool { - match e { - case Var(_) => true - case Literal(lit) => true - case Abs(vars, body) => All_Expr(body, P) - case Apply(_, exprs) => - Seq.All(e requires e in exprs => All_Expr(e, P), exprs) - case Block(exprs) => - Seq.All((e requires e in exprs => All_Expr(e, P)), exprs) - case Bind(vars, vals, body) => - && Seq.All((e requires e in vals => All_Expr(e, P)), vals) - && All_Expr(body, P) - case If(cond, thn, els) => - All_Expr(cond, P) && All_Expr(thn, P) && All_Expr(els, P) + function method AllChildren_Expr(e: Expr, P: Expr -> bool) : bool { + match e { + case Var(_) => true + case Literal(lit) => true + case Abs(vars, body) => All_Expr(body, P) + case Apply(_, exprs) => + Seq.All(e requires e in exprs => All_Expr(e, P), exprs) + case Block(exprs) => + Seq.All((e requires e in exprs => All_Expr(e, P)), exprs) + case Bind(vars, vals, body) => + && Seq.All((e requires e in vals => All_Expr(e, P)), vals) + && All_Expr(body, P) + case If(cond, thn, els) => + All_Expr(cond, P) && All_Expr(thn, P) && All_Expr(els, P) + } } - } - lemma AllImpliesChildren ... {} + lemma AllImpliesChildren ... {} - lemma All_Expr_weaken ... { - AllChildren_Expr_weaken(e, P, Q); - } + lemma All_Expr_weaken ... { + AllChildren_Expr_weaken(e, P, Q); + } - lemma AllChildren_Expr_weaken ... { // NEAT - forall e' | e' in e.Children() { All_Expr_weaken(e', P, Q); } - } + lemma AllChildren_Expr_weaken ... { // NEAT + forall e' | e' in e.Children() { All_Expr_weaken(e', P, Q); } + } - lemma All_Expr_True ... { - AllChildren_Expr_True(e, f); - } + lemma All_Expr_True ... { + AllChildren_Expr_True(e, f); + } - lemma AllChildren_Expr_True ... { - forall e' | e' in e.Children() { All_Expr_True(e', f); } - } + lemma AllChildren_Expr_True ... { + forall e' | e' in e.Children() { All_Expr_True(e', f); } + } - lemma All_Expr_True_Forall ... { - forall e ensures All_Expr(e, f) { - All_Expr_True(e, f); + lemma All_Expr_True_Forall ... { + forall e ensures All_Expr(e, f) { + All_Expr_True(e, f); + } } + } - } + module NonRec refines Base { + // BUG(https://github.com/dafny-lang/dafny/issues/2107) + // BUG(https://github.com/dafny-lang/dafny/issues/2109) + function method All_Expr(e: Expr, P: Expr -> bool) : (b: bool) { + P(e) && forall e' | e' in e.Children() :: All_Expr(e', P) + } -module NonRec refines Base { - // BUG(https://github.com/dafny-lang/dafny/issues/2107) - // BUG(https://github.com/dafny-lang/dafny/issues/2109) - function method All_Expr(e: Expr, P: Expr -> bool) : (b: bool) { - P(e) && forall e' | e' in e.Children() :: All_Expr(e', P) - } + function method AllChildren_Expr(e: Expr, P: Expr -> bool) : bool { + forall e' | e' in e.Children() :: All_Expr(e', P) + } - function method AllChildren_Expr(e: Expr, P: Expr -> bool) : bool { - forall e' | e' in e.Children() :: All_Expr(e', P) - } + lemma AllImpliesChildren ... {} - lemma AllImpliesChildren ... {} + lemma AllChildren_Expr_weaken ... { + forall e' | e' in e.Children() { All_Expr_weaken(e', P, Q); } + } - lemma AllChildren_Expr_weaken ... { - forall e' | e' in e.Children() { All_Expr_weaken(e', P, Q); } - } + lemma All_Expr_weaken ... { + AllChildren_Expr_weaken(e, P, Q); + } - lemma All_Expr_weaken ... { - AllChildren_Expr_weaken(e, P, Q); - } + lemma All_Expr_True ... { + AllChildren_Expr_True(e, f); + } - lemma All_Expr_True ... { - AllChildren_Expr_True(e, f); - } + lemma AllChildren_Expr_True ... { + forall e' | e' in e.Children() { All_Expr_True(e', f); } + } - lemma AllChildren_Expr_True ... { - forall e' | e' in e.Children() { All_Expr_True(e', f); } - } + lemma All_Expr_True_Forall ... { + forall e ensures All_Expr(e, f) { + All_Expr_True(e, f); + } + } - lemma All_Expr_True_Forall ... { - forall e ensures All_Expr(e, f) { - All_Expr_True(e, f); } - } - -} -module Equiv { - import Rec - import NonRec - import opened Syntax + module Equiv { + import Rec + import NonRec + import opened Syntax - lemma AllChildren_Expr(e: Expr, P: Expr -> bool) - decreases e.Depth(), 0 - ensures Rec.AllChildren_Expr(e, P) == NonRec.AllChildren_Expr(e, P) - { - forall e' | e' in e.Children() { All_Expr(e', P); } - } + lemma AllChildren_Expr(e: Expr, P: Expr -> bool) + decreases e.Depth(), 0 + ensures Rec.AllChildren_Expr(e, P) == NonRec.AllChildren_Expr(e, P) + { + forall e' | e' in e.Children() { All_Expr(e', P); } + } - lemma All_Expr(e: Expr, P: Expr -> bool) - decreases e.Depth(), 1 - ensures Rec.All_Expr(e, P) == NonRec.All_Expr(e, P) - { - AllChildren_Expr(e, P); + lemma All_Expr(e: Expr, P: Expr -> bool) + decreases e.Depth(), 1 + ensures Rec.All_Expr(e, P) == NonRec.All_Expr(e, P) + { + AllChildren_Expr(e, P); + } + } } -} -} // Both implementations of Deep should work, but NonRec can be somewhat // simpler to work with. If needed, use ``DeepImpl.Equiv.All_Expr`` to // switch between implementations. -module Deep refines DeepImpl.NonRec {} + module Deep refines DeepImpl.NonRec {} } diff --git a/src/AST/Syntax.dfy b/src/AST/Syntax.dfy index 4e5c025e..81a836cd 100644 --- a/src/AST/Syntax.dfy +++ b/src/AST/Syntax.dfy @@ -7,328 +7,328 @@ module Bootstrap.AST.Syntax { import Microsoft.Boogie import C = Interop.CSharpDafnyASTModel -module Types { - import C = Interop.CSharpDafnyASTModel - - type Path = seq - - datatype ClassType = ClassType(className: Path, typeArgs: seq) - - datatype CollectionKind = - | Seq - | Set - | Multiset - | Map(keyType: Type) - - datatype Type = - | Unit - | Bool - | Char - | Int - | Real - | BigOrdinal - | BitVector(width: nat) - | Collection(finite: bool, kind: CollectionKind, eltType: Type) - | Function(args: seq, ret: Type) // TODO - | Class(classType: ClassType) - { - // TODO: remove? - predicate method NoLeftFunction() + module Types { + import C = Interop.CSharpDafnyASTModel + + type Path = seq + + datatype ClassType = ClassType(className: Path, typeArgs: seq) + + datatype CollectionKind = + | Seq + | Set + | Multiset + | Map(keyType: Type) + + datatype Type = + | Unit + | Bool + | Char + | Int + | Real + | BigOrdinal + | BitVector(width: nat) + | Collection(finite: bool, kind: CollectionKind, eltType: Type) + | Function(args: seq, ret: Type) // TODO + | Class(classType: ClassType) { - match this { - case Unit => true - case Bool => true - case Char => true - case Int => true - case Real => true - case BigOrdinal => true - case BitVector(width: nat) => true - case Collection(finite: bool, kind: CollectionKind, eltType: Type) => - && eltType.NoLeftFunction() - && match kind { - case Seq => true - case Set => true - case Multiset => true - case Map(kt) => kt.NoLeftFunction() - } - case Function(args: seq, ret: Type) => false - case Class(classType: ClassType) => false + // TODO: remove? + predicate method NoLeftFunction() + { + match this { + case Unit => true + case Bool => true + case Char => true + case Int => true + case Real => true + case BigOrdinal => true + case BitVector(width: nat) => true + case Collection(finite: bool, kind: CollectionKind, eltType: Type) => + && eltType.NoLeftFunction() + && match kind { + case Seq => true + case Set => true + case Multiset => true + case Map(kt) => kt.NoLeftFunction() + } + case Function(args: seq, ret: Type) => false + case Class(classType: ClassType) => false + } } - } - // TODO: remove? - predicate method WellFormed() { - match this { - case Unit => true - case Bool => true - case Char => true - case Int => true - case Real => true - case BigOrdinal => true - case BitVector(width: nat) => true - case Collection(finite: bool, kind: CollectionKind, eltType: Type) => - && eltType.WellFormed() - // This condition is overly restrictive: we will do the general case later. - // For instance, maps can contain keys which don't have a decidable equality, - // and sequences can contain elements which also don't have a decidable equality - // (in which case we don't have a decidable equality over the sequences, but it - // is fine). - && eltType.NoLeftFunction() - && match kind { - case Seq => true - case Set => eltType.NoLeftFunction() - case Multiset => eltType.NoLeftFunction() - case Map(kt) => kt.WellFormed() && kt.NoLeftFunction() - } - case Function(args: seq, ret: Type) => - && (forall i | 0 <= i < |args| :: args[i].WellFormed()) - && ret.WellFormed() - case Class(classType: ClassType) => - && (forall i | 0 <= i < |classType.typeArgs| :: classType.typeArgs[i].WellFormed()) + // TODO: remove? + predicate method WellFormed() { + match this { + case Unit => true + case Bool => true + case Char => true + case Int => true + case Real => true + case BigOrdinal => true + case BitVector(width: nat) => true + case Collection(finite: bool, kind: CollectionKind, eltType: Type) => + && eltType.WellFormed() + // This condition is overly restrictive: we will do the general case later. + // For instance, maps can contain keys which don't have a decidable equality, + // and sequences can contain elements which also don't have a decidable equality + // (in which case we don't have a decidable equality over the sequences, but it + // is fine). + && eltType.NoLeftFunction() + && match kind { + case Seq => true + case Set => eltType.NoLeftFunction() + case Multiset => eltType.NoLeftFunction() + case Map(kt) => kt.WellFormed() && kt.NoLeftFunction() + } + case Function(args: seq, ret: Type) => + && (forall i | 0 <= i < |args| :: args[i].WellFormed()) + && ret.WellFormed() + case Class(classType: ClassType) => + && (forall i | 0 <= i < |classType.typeArgs| :: classType.typeArgs[i].WellFormed()) + } } } - } - type T(!new,00,==) = Type -} + type T(!new,00,==) = Type + } type Type = Types.T datatype Tokd = Tokd(tok: Boogie.IToken, val: T) -module BinaryOps { - datatype Logical = - Iff // And, Or, and Imp are in LazyOp - datatype Eq = - EqCommon | NeqCommon - datatype Numeric = - Lt | Le | Ge | Gt | Add | Sub | Mul | Div | Mod - datatype BV = - LeftShift | RightShift | BitwiseAnd | BitwiseOr | BitwiseXor - datatype Char = - LtChar | LeChar | GeChar | GtChar - datatype Sequences = - SeqEq | SeqNeq | Prefix | ProperPrefix | Concat | InSeq | NotInSeq | - SeqSelect | SeqTake | SeqDrop // Separate nodes in DafnyAST.cs - datatype Sets = - SetEq | SetNeq | Subset | Superset | ProperSubset | ProperSuperset | - Disjoint | InSet | NotInSet | Union | Intersection | SetDifference - datatype Multisets = - MultisetEq | MultisetNeq | MultiSubset | MultiSuperset | - ProperMultiSubset | ProperMultiSuperset | MultisetDisjoint | InMultiset | - NotInMultiset | MultisetUnion | MultisetIntersection | MultisetDifference | - MultisetSelect // Separate node in DafnyAST.cs - datatype Maps = - MapEq | MapNeq | InMap | NotInMap | MapMerge | MapSubtraction | - MapSelect // Separate node in DafnyAST.cs - datatype Datatypes = - RankLt | RankGt - datatype BinaryOp = - | Logical(oLogical: Logical) - | Eq(oEq: Eq) - | Numeric(oNumeric: Numeric) - | BV(oBV: BV) - | Char(oChar: Char) - | Sequences(oSequences: Sequences) - | Sets(oSets: Sets) - | Multisets(oMultisets: Multisets) - | Maps(oMaps: Maps) - | Datatypes(oDatatypes: Datatypes) - type T(!new,00,==) = BinaryOp -} + module BinaryOps { + datatype Logical = + Iff // And, Or, and Imp are in LazyOp + datatype Eq = + EqCommon | NeqCommon + datatype Numeric = + Lt | Le | Ge | Gt | Add | Sub | Mul | Div | Mod + datatype BV = + LeftShift | RightShift | BitwiseAnd | BitwiseOr | BitwiseXor + datatype Char = + LtChar | LeChar | GeChar | GtChar + datatype Sequences = + SeqEq | SeqNeq | Prefix | ProperPrefix | Concat | InSeq | NotInSeq | + SeqSelect | SeqTake | SeqDrop // Separate nodes in DafnyAST.cs + datatype Sets = + SetEq | SetNeq | Subset | Superset | ProperSubset | ProperSuperset | + Disjoint | InSet | NotInSet | Union | Intersection | SetDifference + datatype Multisets = + MultisetEq | MultisetNeq | MultiSubset | MultiSuperset | + ProperMultiSubset | ProperMultiSuperset | MultisetDisjoint | InMultiset | + NotInMultiset | MultisetUnion | MultisetIntersection | MultisetDifference | + MultisetSelect // Separate node in DafnyAST.cs + datatype Maps = + MapEq | MapNeq | InMap | NotInMap | MapMerge | MapSubtraction | + MapSelect // Separate node in DafnyAST.cs + datatype Datatypes = + RankLt | RankGt + datatype BinaryOp = + | Logical(oLogical: Logical) + | Eq(oEq: Eq) + | Numeric(oNumeric: Numeric) + | BV(oBV: BV) + | Char(oChar: Char) + | Sequences(oSequences: Sequences) + | Sets(oSets: Sets) + | Multisets(oMultisets: Multisets) + | Maps(oMaps: Maps) + | Datatypes(oDatatypes: Datatypes) + type T(!new,00,==) = BinaryOp + } type BinaryOp = BinaryOps.T -module TernaryOps { - import Types + module TernaryOps { + import Types - datatype Sequences = - SeqUpdate | SeqSubseq - datatype Multisets = - MultisetUpdate - datatype Maps = - MapUpdate + datatype Sequences = + SeqUpdate | SeqSubseq + datatype Multisets = + MultisetUpdate + datatype Maps = + MapUpdate - datatype TernaryOp = - | Sequences(oSequences: Sequences) - | Multisets(oMultisets: Multisets) - | Maps(oMaps: Maps) + datatype TernaryOp = + | Sequences(oSequences: Sequences) + | Multisets(oMultisets: Multisets) + | Maps(oMaps: Maps) - type T(!new,00,==) = TernaryOp -} + type T(!new,00,==) = TernaryOp + } type TernaryOp = TernaryOps.T -module UnaryOps { - datatype UnaryOp = - | BVNot - | BoolNot - | SeqLength - | SetCard - | MultisetCard - | MapCard - | MemberSelect(name: string) - // Ghost operators - // | Fresh - // | Allocated - // | Lit - type T(!new,00,==) = UnaryOp -} + module UnaryOps { + datatype UnaryOp = + | BVNot + | BoolNot + | SeqLength + | SetCard + | MultisetCard + | MapCard + | MemberSelect(name: string) + // Ghost operators + // | Fresh + // | Allocated + // | Lit + type T(!new,00,==) = UnaryOp + } type UnaryOp = UnaryOps.T -module Exprs { - import Utils.Lib.Math - import Utils.Lib.Seq - - import Types - import UnaryOps - import BinaryOps - import TernaryOps - import C = Interop.CSharpDafnyASTModel - - // FIXME should literals just be Values.T? - datatype Literal = - | LitUnit - | LitBool(b: bool) - | LitInt(i: int) - | LitReal(r: real) - | LitChar(c: char) - | LitString(s: string, verbatim: bool) // FIXME get rid of verbatim flag by unescaping - { - function method Depth() : nat { 1 } - } + module Exprs { + import Utils.Lib.Math + import Utils.Lib.Seq + + import Types + import UnaryOps + import BinaryOps + import TernaryOps + import C = Interop.CSharpDafnyASTModel + + // FIXME should literals just be Values.T? + datatype Literal = + | LitUnit + | LitBool(b: bool) + | LitInt(i: int) + | LitReal(r: real) + | LitChar(c: char) + | LitString(s: string, verbatim: bool) // FIXME get rid of verbatim flag by unescaping + { + function method Depth() : nat { 1 } + } - datatype BuiltinFunction = - | Display(ty: Types.Type) - | Print - - // DafnyAst.cs handles `f(1)` differently from `(var g := f; g)(1)`, but not us - datatype EagerOp = - | UnaryOp(uop: UnaryOps.T) - | BinaryOp(bop: BinaryOps.T) - | TernaryOp(top: TernaryOps.T) - | Builtin(builtin: BuiltinFunction) - | FunctionCall() // First argument is expression that resolves to function or method - | DataConstructor(name: Types.Path, typeArgs: seq) - - datatype LazyOp = - | And - | Or - | Imp - - datatype ApplyOp = - | Lazy(lOp: LazyOp) - | Eager(eOp: EagerOp) - -/// Notes on AST nodes -/// ================== -/// -/// - AST nodes have type ``Expr``. All subexpressions of a expression are -/// direct children of it; there are no subexpressions hidden within -/// ``ApplyOp``, for example). -/// -/// - ``ApplyOp`` is split into lazy and eager operations. This matter because -/// the language is not pure: if ``s`` is an empty sequence ``[]``, then the -/// expression ``false && s[0] == 1`` is a valid and reduces to ``false``, -/// whereas the expression ``0 * s[0] == 0`` is invalid and errors out with an -/// out-of-bounds access). -/// -/// - ``Block`` is semantically the same as ``Bind`` with no variables. -/// -/// - ``Bind`` is not the same as ``Apply`` on an ``Abs``, because variables are -/// captured by value, so mutations within an ``Abs`` are not propagated to the -/// caller's context. (In most cases, though, variables passed into an ``Abs`` -/// are not mutated at all, because dafny lambdas are pure). - - datatype Expr = - | Var(name: string) - | Literal(lit: Literal) - | Abs(vars: seq, body: Expr) - | Apply(aop: ApplyOp, args: seq) - | Block(stmts: seq) - | Bind(vars: seq, vals: seq, body: Expr) - | If(cond: Expr, thn: Expr, els: Expr) // DISCUSS: Lazy op node? - { - function method Depth() : nat { - 1 + match this { - case Var(_) => - 0 - case Literal(lit: Literal) => - 0 - case Abs(vars, body) => - body.Depth() - case Apply(_, args) => - Seq.MaxF(var f := (e: Expr) requires e in args => e.Depth(); f, args, 0) - case Block(stmts) => - Seq.MaxF(var f := (e: Expr) requires e in stmts => e.Depth(); f, stmts, 0) - case Bind(vars, vals, body) => - Math.Max( - Seq.MaxF(var f := (e: Expr) requires e in vals => e.Depth(); f, vals, 0), + datatype BuiltinFunction = + | Display(ty: Types.Type) + | Print + + // DafnyAst.cs handles `f(1)` differently from `(var g := f; g)(1)`, but not us + datatype EagerOp = + | UnaryOp(uop: UnaryOps.T) + | BinaryOp(bop: BinaryOps.T) + | TernaryOp(top: TernaryOps.T) + | Builtin(builtin: BuiltinFunction) + | FunctionCall() // First argument is expression that resolves to function or method + | DataConstructor(name: Types.Path, typeArgs: seq) + + datatype LazyOp = + | And + | Or + | Imp + + datatype ApplyOp = + | Lazy(lOp: LazyOp) + | Eager(eOp: EagerOp) + + /// Notes on AST nodes + /// ================== + /// + /// - AST nodes have type ``Expr``. All subexpressions of a expression are + /// direct children of it; there are no subexpressions hidden within + /// ``ApplyOp``, for example). + /// + /// - ``ApplyOp`` is split into lazy and eager operations. This matter because + /// the language is not pure: if ``s`` is an empty sequence ``[]``, then the + /// expression ``false && s[0] == 1`` is a valid and reduces to ``false``, + /// whereas the expression ``0 * s[0] == 0`` is invalid and errors out with an + /// out-of-bounds access). + /// + /// - ``Block`` is semantically the same as ``Bind`` with no variables. + /// + /// - ``Bind`` is not the same as ``Apply`` on an ``Abs``, because variables are + /// captured by value, so mutations within an ``Abs`` are not propagated to the + /// caller's context. (In most cases, though, variables passed into an ``Abs`` + /// are not mutated at all, because dafny lambdas are pure). + + datatype Expr = + | Var(name: string) + | Literal(lit: Literal) + | Abs(vars: seq, body: Expr) + | Apply(aop: ApplyOp, args: seq) + | Block(stmts: seq) + | Bind(vars: seq, vals: seq, body: Expr) + | If(cond: Expr, thn: Expr, els: Expr) // DISCUSS: Lazy op node? + { + function method Depth() : nat { + 1 + match this { + case Var(_) => + 0 + case Literal(lit: Literal) => + 0 + case Abs(vars, body) => body.Depth() - ) - case If(cond, thn, els) => - Math.Max(cond.Depth(), Math.Max(thn.Depth(), els.Depth())) + case Apply(_, args) => + Seq.MaxF(var f := (e: Expr) requires e in args => e.Depth(); f, args, 0) + case Block(stmts) => + Seq.MaxF(var f := (e: Expr) requires e in stmts => e.Depth(); f, stmts, 0) + case Bind(vars, vals, body) => + Math.Max( + Seq.MaxF(var f := (e: Expr) requires e in vals => e.Depth(); f, vals, 0), + body.Depth() + ) + case If(cond, thn, els) => + Math.Max(cond.Depth(), Math.Max(thn.Depth(), els.Depth())) + } } - } - function method Children() : (s: seq) - ensures forall e' | e' in s :: e'.Depth() < this.Depth() - { - match this { - case Var(_) => [] - case Literal(lit) => [] - case Abs(vars, body) => [body] - case Apply(aop, exprs) => exprs - case Block(exprs) => exprs - case Bind(vars, vals, body) => vals + [body] - case If(cond, thn, els) => [cond, thn, els] + function method Children() : (s: seq) + ensures forall e' | e' in s :: e'.Depth() < this.Depth() + { + match this { + case Var(_) => [] + case Literal(lit) => [] + case Abs(vars, body) => [body] + case Apply(aop, exprs) => exprs + case Block(exprs) => exprs + case Bind(vars, vals, body) => vals + [body] + case If(cond, thn, els) => [cond, thn, els] + } } } - } - function method WellFormed(e: Expr): bool { - match e { - case Apply(Lazy(_), es) => - |es| == 2 - case Apply(Eager(UnaryOp(_)), es) => - |es| == 1 - case Apply(Eager(BinaryOp(_)), es) => - |es| == 2 - case Apply(Eager(TernaryOp(top)), es) => - |es| == 3 - case Apply(Eager(FunctionCall()), es) => - |es| >= 1 // Needs a function to call - case Apply(Eager(Builtin(Display(ty))), es) => - ty.Collection? && ty.finite - case Bind(vars, vals, _) => - |vars| == |vals| - case _ => true + function method WellFormed(e: Expr): bool { + match e { + case Apply(Lazy(_), es) => + |es| == 2 + case Apply(Eager(UnaryOp(_)), es) => + |es| == 1 + case Apply(Eager(BinaryOp(_)), es) => + |es| == 2 + case Apply(Eager(TernaryOp(top)), es) => + |es| == 3 + case Apply(Eager(FunctionCall()), es) => + |es| >= 1 // Needs a function to call + case Apply(Eager(Builtin(Display(ty))), es) => + ty.Collection? && ty.finite + case Bind(vars, vals, _) => + |vars| == |vals| + case _ => true + } } - } - function method ConstructorsMatch(e: Expr, e': Expr): bool { - match e { - case Var(name) => - e'.Var? && name == e'.name - case Literal(l) => - e'.Literal? && l == e'.lit - case Abs(vars, body) => - e'.Abs? && vars == e'.vars - case Apply(aop, args) => - e'.Apply? && aop == e'.aop && |args| == |e'.args| - case Block(stmts) => - e'.Block? && |stmts| == |e'.stmts| - case If(cond, thn, els) => - e'.If? - case Bind(vars, vals, body) => - e'.Bind? && |vars| == |e'.vars| && |vals| == |e'.vals| + function method ConstructorsMatch(e: Expr, e': Expr): bool { + match e { + case Var(name) => + e'.Var? && name == e'.name + case Literal(l) => + e'.Literal? && l == e'.lit + case Abs(vars, body) => + e'.Abs? && vars == e'.vars + case Apply(aop, args) => + e'.Apply? && aop == e'.aop && |args| == |e'.args| + case Block(stmts) => + e'.Block? && |stmts| == |e'.stmts| + case If(cond, thn, els) => + e'.If? + case Bind(vars, vals, body) => + e'.Bind? && |vars| == |e'.vars| && |vals| == |e'.vals| + } } - } - type T(!new,00,==) = Expr -} + type T(!new,00,==) = Expr + } type Expr = Exprs.T diff --git a/src/AST/Translator.dfy b/src/AST/Translator.dfy index c01b50e4..623d4d5c 100644 --- a/src/AST/Translator.dfy +++ b/src/AST/Translator.dfy @@ -30,18 +30,18 @@ module Bootstrap.AST.Translator { { function method ToString() : string { match this - case Invalid(msg) => - "Invalid term: " + msg - case GhostExpr(expr) => - "Ghost expression: " + TypeConv.ObjectToString(expr) - case UnsupportedType(ty) => - "Unsupported type: " + TypeConv.ObjectToString(ty) - case UnsupportedExpr(expr) => - "Unsupported expression: " + TypeConv.ObjectToString(expr) - case UnsupportedStmt(stmt) => - "Unsupported statement: " + TypeConv.ObjectToString(stmt) - case UnsupportedMember(decl) => - "Unsupported declaration: " + TypeConv.ObjectToString(decl) + case Invalid(msg) => + "Invalid term: " + msg + case GhostExpr(expr) => + "Ghost expression: " + TypeConv.ObjectToString(expr) + case UnsupportedType(ty) => + "Unsupported type: " + TypeConv.ObjectToString(ty) + case UnsupportedExpr(expr) => + "Unsupported expression: " + TypeConv.ObjectToString(expr) + case UnsupportedStmt(stmt) => + "Unsupported statement: " + TypeConv.ObjectToString(stmt) + case UnsupportedMember(decl) => + "Unsupported declaration: " + TypeConv.ObjectToString(decl) } } @@ -70,8 +70,8 @@ module Bootstrap.AST.Translator { else if ty is C.BitvectorType then var bvTy := ty as C.BitvectorType; :- Need(bvTy.Width >= 0, Invalid("BV width must be >= 0")); - Success(DT.BitVector(bvTy.Width as int)) - // TODO: the following could be simplified + Success(DT.BitVector(bvTy.Width as int)) + // TODO: the following could be simplified else if ty is C.MapType then var ty := ty as C.MapType; assume TypeHeight(ty.Domain) < TypeHeight(ty); @@ -202,13 +202,13 @@ module Bootstrap.AST.Translator { reads * { :- Need(u is C.UnaryOpExpr, UnsupportedExpr(u)); - var u := u as C.UnaryOpExpr; - var op, e := u.ResolvedOp, u.E; - assume Decreases(e, u); - :- Need(op !in GhostUnaryOps, GhostExpr(u)); - :- Need(op in UnaryOpMap.Keys, UnsupportedExpr(u)); - var te :- TranslateExpression(e); - Success(DE.Apply(DE.Eager(DE.UnaryOp(UnaryOpMap[op])), [te])) + var u := u as C.UnaryOpExpr; + var op, e := u.ResolvedOp, u.E; + assume Decreases(e, u); + :- Need(op !in GhostUnaryOps, GhostExpr(u)); + :- Need(op in UnaryOpMap.Keys, UnsupportedExpr(u)); + var te :- TranslateExpression(e); + Success(DE.Apply(DE.Eager(DE.UnaryOp(UnaryOpMap[op])), [te])) } function method TranslateBinary(b: C.BinaryExpr) @@ -221,9 +221,9 @@ module Bootstrap.AST.Translator { assume Decreases(e0, b); assume Decreases(e1, b); :- Need(op in BinaryOpCodeMap, UnsupportedExpr(b)); - var t0 :- TranslateExpression(e0); - var t1 :- TranslateExpression(e1); - Success(DE.Apply(BinaryOpCodeMap[op], [t0, t1])) + var t0 :- TranslateExpression(e0); + var t1 :- TranslateExpression(e1); + Success(DE.Apply(BinaryOpCodeMap[op], [t0, t1])) } function method TranslateLiteral(l: C.LiteralExpr) @@ -240,7 +240,7 @@ module Bootstrap.AST.Translator { var str := TypeConv.AsString(l.Value); if l is C.CharLiteralExpr then :- Need(|str| == 1, Invalid("CharLiteralExpr must contain a single character.")); - Success(DE.Literal(DE.LitChar(str[0]))) + Success(DE.Literal(DE.LitChar(str[0]))) else if l is C.StringLiteralExpr then var sl := l as C.StringLiteralExpr; Success(DE.Literal(DE.LitString(str, sl.IsVerbatim))) @@ -259,7 +259,7 @@ module Bootstrap.AST.Translator { var fn :- TranslateExpression(ae.Function); var args := ListUtils.ToSeq(ae.Args); var args :- Seq.MapResult(args, e requires e in args reads * => - assume Decreases(e, ae); TranslateExpression(e)); + assume Decreases(e, ae); TranslateExpression(e)); Success(DE.Apply(DE.Eager(DE.FunctionCall()), [fn] + args)) } @@ -294,7 +294,7 @@ module Bootstrap.AST.Translator { var fn :- TranslateMemberSelect(fce.Receiver, fce.Function.FullName); var args := ListUtils.ToSeq(fce.Args); var args :- Seq.MapResult(args, e requires e in args reads * => - assume Decreases(e, fce); TranslateExpression(e)); + assume Decreases(e, fce); TranslateExpression(e)); Success(DE.Apply(DE.Eager(DE.FunctionCall()), [fn] + args)) } @@ -309,7 +309,7 @@ module Bootstrap.AST.Translator { // TODO: also include formals in the following, and filter out ghost arguments var args := ListUtils.ToSeq(dtv.Arguments); var args :- Seq.MapResult(args, e requires e in args reads * => - assume Decreases(e, dtv); TranslateExpression(e)); + assume Decreases(e, dtv); TranslateExpression(e)); Success(DE.Apply(DE.Eager(DE.DataConstructor([n], typeArgs)), args)) // TODO: proper path } @@ -320,10 +320,10 @@ module Bootstrap.AST.Translator { { var ty :- TranslateType(de.Type); :- Need(ty.Collection? && ty.finite, Invalid("`DisplayExpr` must be a finite collection.")); - var elems := ListUtils.ToSeq(de.Elements); - var elems :- Seq.MapResult(elems, e requires e in elems reads * => - assume Decreases(e, de); TranslateExpression(e)); - Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) + var elems := ListUtils.ToSeq(de.Elements); + var elems :- Seq.MapResult(elems, e requires e in elems reads * => + assume Decreases(e, de); TranslateExpression(e)); + Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) } function method TranslateExpressionPair(mde: C.MapDisplayExpr, ep: C.ExpressionPair) @@ -347,11 +347,11 @@ module Bootstrap.AST.Translator { { var ty :- TranslateType(mde.Type); :- Need(ty.Collection? && ty.kind.Map? && ty.finite, Invalid("`MapDisplayExpr` must be a map.")); - var elems := ListUtils.ToSeq(mde.Elements); - var elems :- Seq.MapResult(elems, (ep: C.ExpressionPair) requires ep in elems reads * => - assume Math.Max(ASTHeight(ep.A), ASTHeight(ep.B)) < ASTHeight(mde); - TranslateExpressionPair(mde, ep)); - Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) + var elems := ListUtils.ToSeq(mde.Elements); + var elems :- Seq.MapResult(elems, (ep: C.ExpressionPair) requires ep in elems reads * => + assume Math.Max(ASTHeight(ep.A), ASTHeight(ep.B)) < ASTHeight(mde); + TranslateExpressionPair(mde, ep)); + Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) } function method TranslateSeqSelectExpr(se: C.SeqSelectExpr): (e: TranslationResult) @@ -362,38 +362,38 @@ module Bootstrap.AST.Translator { var ty :- TranslateType(se.Seq.Type); :- Need(ty.Collection? && !ty.kind.Set?, Invalid("`SeqSelect` must be on a map, sequence, or multiset.")); - :- Need(se.SelectOne ==> se.E0 != null && se.E1 == null, - Invalid("Inconsistent values for `SelectOne` and E1 in SeqSelect.")); - :- Need(!se.SelectOne ==> ty.kind.Seq?, - Invalid("`SeqSelect` on a map or multiset must have a single index.")); - assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.E0), ASTHeight(se.E1))) < ASTHeight(se); - var recv :- TranslateExpression(se.Seq); - var eager := (op, args) => Success(DE.Apply(DE.Eager(op), args)); - match ty.kind { // FIXME AST gen should produce `Expression?` not `Expression` - case Seq() => - if se.SelectOne then - assert se.E1 == null; - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqSelect)), [recv, e0]) - else if se.E1 == null then - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqDrop)), [recv, e0]) - else if se.E0 == null then - var e1 :- TranslateExpression(se.E1); - eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqTake)), [recv, e1]) - else - var e0 :- TranslateExpression(se.E0); - var e1 :- TranslateExpression(se.E1); - eager(DE.TernaryOp(DE.TernaryOps.Sequences(DE.TernaryOps.SeqSubseq)), [recv, e0, e1]) - case Map(_) => - assert se.SelectOne && se.E1 == null; - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Maps(DE.BinaryOps.MapSelect)), [recv, e0]) - case Multiset() => - assert se.SelectOne && se.E1 == null; - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Multisets(DE.BinaryOps.MultisetSelect)), [recv, e0]) - } + :- Need(se.SelectOne ==> se.E0 != null && se.E1 == null, + Invalid("Inconsistent values for `SelectOne` and E1 in SeqSelect.")); + :- Need(!se.SelectOne ==> ty.kind.Seq?, + Invalid("`SeqSelect` on a map or multiset must have a single index.")); + assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.E0), ASTHeight(se.E1))) < ASTHeight(se); + var recv :- TranslateExpression(se.Seq); + var eager := (op, args) => Success(DE.Apply(DE.Eager(op), args)); + match ty.kind { // FIXME AST gen should produce `Expression?` not `Expression` + case Seq() => + if se.SelectOne then + assert se.E1 == null; + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqSelect)), [recv, e0]) + else if se.E1 == null then + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqDrop)), [recv, e0]) + else if se.E0 == null then + var e1 :- TranslateExpression(se.E1); + eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqTake)), [recv, e1]) + else + var e0 :- TranslateExpression(se.E0); + var e1 :- TranslateExpression(se.E1); + eager(DE.TernaryOp(DE.TernaryOps.Sequences(DE.TernaryOps.SeqSubseq)), [recv, e0, e1]) + case Map(_) => + assert se.SelectOne && se.E1 == null; + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Maps(DE.BinaryOps.MapSelect)), [recv, e0]) + case Multiset() => + assert se.SelectOne && se.E1 == null; + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Multisets(DE.BinaryOps.MultisetSelect)), [recv, e0]) + } } function method TranslateSeqUpdateExpr(se: C.SeqUpdateExpr) @@ -404,15 +404,15 @@ module Bootstrap.AST.Translator { var ty :- TranslateType(se.Type); :- Need(ty.Collection? && ty.kind != DT.Set(), Invalid("`SeqUpdate` must be a map, sequence, or multiset.")); - assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.Index), ASTHeight(se.Value))) < ASTHeight(se); - var tSeq :- TranslateExpression(se.Seq); - var tIndex :- TranslateExpression(se.Index); - var tValue :- TranslateExpression(se.Value); - var op := match ty.kind - case Seq() => DE.TernaryOps.Sequences(DE.TernaryOps.SeqUpdate) - case Map(_) => DE.TernaryOps.Maps(DE.TernaryOps.MapUpdate) - case Multiset() => DE.TernaryOps.Multisets(DE.TernaryOps.MultisetUpdate); - Success(DE.Apply(DE.Eager(DE.TernaryOp(op)), [tSeq, tIndex, tValue])) + assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.Index), ASTHeight(se.Value))) < ASTHeight(se); + var tSeq :- TranslateExpression(se.Seq); + var tIndex :- TranslateExpression(se.Index); + var tValue :- TranslateExpression(se.Value); + var op := match ty.kind + case Seq() => DE.TernaryOps.Sequences(DE.TernaryOps.SeqUpdate) + case Map(_) => DE.TernaryOps.Maps(DE.TernaryOps.MapUpdate) + case Multiset() => DE.TernaryOps.Multisets(DE.TernaryOps.MultisetUpdate); + Success(DE.Apply(DE.Eager(DE.TernaryOp(op)), [tSeq, tIndex, tValue])) } function method TranslateLambdaExpr(le: C.LambdaExpr) @@ -421,7 +421,7 @@ module Bootstrap.AST.Translator { decreases ASTHeight(le), 0 { var bvars := Seq.Map((bv: C.BoundVar) reads * => TypeConv.AsString(bv.Name), - ListUtils.ToSeq(le.BoundVars)); + ListUtils.ToSeq(le.BoundVars)); assume Decreases(le.Term, le); var body :- TranslateExpression(le.Term); Success(DE.Abs(bvars, body)) @@ -433,17 +433,17 @@ module Bootstrap.AST.Translator { decreases ASTHeight(le), 0 { :- Need(le.Exact, UnsupportedExpr(le)); - var lhss := ListUtils.ToSeq(le.LHSs); - var bvs :- Seq.MapResult(lhss, (pat: C.CasePattern) reads * => - :- Need(pat.Var != null, UnsupportedExpr(le)); - Success(TypeConv.AsString(pat.Var.Name))); - var rhss := ListUtils.ToSeq(le.RHSs); - var elems :- Seq.MapResult(rhss, e requires e in rhss reads * => - assume Decreases(e, le); TranslateExpression(e)); - :- Need(|bvs| == |elems|, UnsupportedExpr(le)); - assume Decreases(le.Body, le); - var body :- TranslateExpression(le.Body); - Success(DE.Bind(bvs, elems, body)) + var lhss := ListUtils.ToSeq(le.LHSs); + var bvs :- Seq.MapResult(lhss, (pat: C.CasePattern) reads * => + :- Need(pat.Var != null, UnsupportedExpr(le)); + Success(TypeConv.AsString(pat.Var.Name))); + var rhss := ListUtils.ToSeq(le.RHSs); + var elems :- Seq.MapResult(rhss, e requires e in rhss reads * => + assume Decreases(e, le); TranslateExpression(e)); + :- Need(|bvs| == |elems|, UnsupportedExpr(le)); + assume Decreases(le.Body, le); + var body :- TranslateExpression(le.Body); + Success(DE.Bind(bvs, elems, body)) } function method TranslateConcreteSyntaxExpression(ce: C.ConcreteSyntaxExpression) @@ -526,7 +526,7 @@ module Bootstrap.AST.Translator { { var stmts := ListUtils.ToSeq(b.Body); var stmts' :- Seq.MapResult(stmts, s' requires s' in stmts reads * => - assume Decreases(s', b); TranslateStatement(s')); + assume Decreases(s', b); TranslateStatement(s')); Success(DE.Block(stmts')) } diff --git a/src/Passes/EliminateNegatedBinops.dfy b/src/Passes/EliminateNegatedBinops.dfy index f58d06cb..4a0e0154 100644 --- a/src/Passes/EliminateNegatedBinops.dfy +++ b/src/Passes/EliminateNegatedBinops.dfy @@ -1,4 +1,4 @@ -include "../Interop/CSharpDafnyASTModel.dfy" + include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" @@ -41,16 +41,16 @@ module Bootstrap.Passes.EliminateNegatedBinops { // FlipNegatedBinop and the body of ``IsNegatedBinop``. { match op - case Eq(NeqCommon) => BinaryOps.Eq(BinaryOps.EqCommon) - case Sequences(SeqNeq) => BinaryOps.Sequences(BinaryOps.SeqEq) - case Sequences(NotInSeq) => BinaryOps.Sequences(BinaryOps.InSeq) - case Sets(SetNeq) => BinaryOps.Sets(BinaryOps.SetEq) - case Sets(NotInSet) => BinaryOps.Sets(BinaryOps.InSet) - case Multisets(MultisetNeq) => BinaryOps.Multisets(BinaryOps.MultisetEq) - case Multisets(NotInMultiset) => BinaryOps.Multisets(BinaryOps.InMultiset) - case Maps(MapNeq) => BinaryOps.Maps(BinaryOps.MapEq) - case Maps(NotInMap) => BinaryOps.Maps(BinaryOps.InMap) - case _ => op + case Eq(NeqCommon) => BinaryOps.Eq(BinaryOps.EqCommon) + case Sequences(SeqNeq) => BinaryOps.Sequences(BinaryOps.SeqEq) + case Sequences(NotInSeq) => BinaryOps.Sequences(BinaryOps.InSeq) + case Sets(SetNeq) => BinaryOps.Sets(BinaryOps.SetEq) + case Sets(NotInSet) => BinaryOps.Sets(BinaryOps.InSet) + case Multisets(MultisetNeq) => BinaryOps.Multisets(BinaryOps.MultisetEq) + case Multisets(NotInMultiset) => BinaryOps.Multisets(BinaryOps.InMultiset) + case Maps(MapNeq) => BinaryOps.Maps(BinaryOps.MapEq) + case Maps(NotInMap) => BinaryOps.Maps(BinaryOps.InMap) + case _ => op } // TODO(SMH): add a "_Single" prefix @@ -105,22 +105,22 @@ module Bootstrap.Passes.EliminateNegatedBinops { } lemma FlipNegatedBinop_Binop_Rel( - e: Interp.Expr, e': Interp.Expr, op: BinaryOp, v0: WV, v1: WV, v0': WV, v1': WV - ) + e: Interp.Expr, e': Interp.Expr, op: BinaryOp, v0: WV, v1: WV, v0': WV, v1': WV + ) requires IsNegatedBinop(op) requires EagerOpSupportsInterp(Exprs.BinaryOp(op)) requires EqValue(v0, v0') requires EqValue(v1, v1') ensures ( - match (InterpBinaryOp(e, op, v0, v1), InterpBinaryOp(e', FlipNegatedBinop(op), v0', v1')) - case (Success(b), Success(b')) => - && b.Bool? - && b'.Bool? - && b.b == ! b'.b - case (Failure(_), Failure(_)) => - true - case _ => - false) + match (InterpBinaryOp(e, op, v0, v1), InterpBinaryOp(e', FlipNegatedBinop(op), v0', v1')) + case (Success(b), Success(b')) => + && b.Bool? + && b'.Bool? + && b.b == ! b'.b + case (Failure(_), Failure(_)) => + true + case _ => + false) { reveal InterpBinaryOp(); EqValue_HasEqValue_Eq(v0, v0'); @@ -130,10 +130,10 @@ module Bootstrap.Passes.EliminateNegatedBinops { lemma FlipNegatedBinop_Single_Rel(op: BinaryOp, args: seq) requires IsNegatedBinop(op) ensures ( - var e := Exprs.Apply(Exprs.Eager(Exprs.BinaryOp(op)), args); - var e' := FlipNegatedBinop_Single(op, args); - Tr_Expr_Rel(e, e') - ) + var e := Exprs.Apply(Exprs.Eager(Exprs.BinaryOp(op)), args); + var e' := FlipNegatedBinop_Single(op, args); + Tr_Expr_Rel(e, e') + ) { reveal InterpExpr(); reveal InterpFunctionCall(); diff --git a/src/Passes/Pass.dfy b/src/Passes/Pass.dfy index 1a928834..6ca7f26f 100644 --- a/src/Passes/Pass.dfy +++ b/src/Passes/Pass.dfy @@ -14,10 +14,10 @@ module Bootstrap.Passes.Pass { // The postcondition of the transformation function method Apply(p: Program) : (p': Program) - // The transformation itself. - // - // For now, we enforce the use of ``EqInterp`` as the binary relation between - // the input and the output. + // The transformation itself. + // + // For now, we enforce the use of ``EqInterp`` as the binary relation between + // the input and the output. requires Tr_Pre(p) ensures Tr_Post(p) ensures EqInterp(p.mainMethod.methodBody, p'.mainMethod.methodBody) diff --git a/src/Passes/SimplifyEmptyBlocks.dfy b/src/Passes/SimplifyEmptyBlocks.dfy index 8c172399..f1df3db5 100644 --- a/src/Passes/SimplifyEmptyBlocks.dfy +++ b/src/Passes/SimplifyEmptyBlocks.dfy @@ -1,4 +1,4 @@ -include "../Interop/CSharpDafnyASTModel.dfy" + include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" @@ -59,7 +59,7 @@ module Bootstrap.Passes.SimplifyEmptyBlocks { // some blocks might lead to the simplification of some `if then else` branches which might in // turn lead to the simplification of other blocks, etc. // - // Rk.: pass 3. removes expressions that might fail. A pass like (3.) is correct because, following definition of ``EqInterp``, the original program (before simplification) is assumed to not fail. + // Rk.: pass 3. removes expressions that might fail. A pass like (3.) is correct because, following definition of ``EqInterp``, the original program (before simplification) is assumed to not fail. // // Rk.: one reason why we need these passes is that Dafny-in-Dafny unifies let // expressions and variable-declaration statements. For let expressions, this @@ -95,396 +95,396 @@ module Bootstrap.Passes.SimplifyEmptyBlocks { type Expr = Syntax.Expr -module FilterCommon { - import Utils.Lib - import Utils.Lib.Debug + module FilterCommon { + import Utils.Lib + import Utils.Lib.Debug - import opened AST.Syntax - import opened Semantics.Equiv - import opened Semantics.Interp + import opened AST.Syntax + import opened Semantics.Equiv + import opened Semantics.Interp - type Expr = Syntax.Expr + type Expr = Syntax.Expr - const EmptyBlock := Expr.Block([]) + const EmptyBlock := Expr.Block([]) - // TODO: move? - predicate method IsEmptyBlock(e: Expr) - { - e.Block? && e.stmts == [] - } + // TODO: move? + predicate method IsEmptyBlock(e: Expr) + { + e.Block? && e.stmts == [] + } - // TODO: move? - predicate method IsNotEmptyBlock(e: Expr) - { - !IsEmptyBlock(e) - } + // TODO: move? + predicate method IsNotEmptyBlock(e: Expr) + { + !IsEmptyBlock(e) + } - predicate Tr_Expr_Post(e: Expr) { - true - } + predicate Tr_Expr_Post(e: Expr) { + true + } - predicate Tr_Expr_Rel(e: Expr, e': Expr) { - EqInterp(e, e') + predicate Tr_Expr_Rel(e: Expr, e': Expr) { + EqInterp(e, e') + } } -} -module FilterEmptyBlocks { - // Tranformation 1 - - import Utils.Lib - import Utils.Lib.Debug - import opened Utils.Lib.Datatypes - import opened Transforms.BottomUp - - import opened AST.Syntax - import opened AST.Predicates - import opened Semantics.Interp - import opened Semantics.Values - import opened Semantics.Equiv - import opened Transforms.Generic - import opened Transforms.Proofs.BottomUp_ + module FilterEmptyBlocks { + // Tranformation 1 - import opened FilterCommon + import Utils.Lib + import Utils.Lib.Debug + import opened Utils.Lib.Datatypes + import opened Transforms.BottomUp - type Expr = Syntax.Expr + import opened AST.Syntax + import opened AST.Predicates + import opened Semantics.Interp + import opened Semantics.Values + import opened Semantics.Equiv + import opened Transforms.Generic + import opened Transforms.Proofs.BottomUp_ - function method FilterEmptyBlocks_Seq(es: seq): (es': seq) - ensures Seq_All(SupportsInterp, es) ==> Seq_All(SupportsInterp, es') - ensures |es| >= |es'| - { - Seq.Filter(es, IsNotEmptyBlock) - } + import opened FilterCommon - function method FilterEmptyBlocks_Single(e: Expr): Expr - { - if e.Block? then - Expr.Block(FilterEmptyBlocks_Seq(e.stmts)) - else - e - } + type Expr = Syntax.Expr - lemma FilterEmptyBlocks_Seq_Rel(es: seq, env: Environment, ctx: State, ctx': State) - requires Seq_All(SupportsInterp, es) - requires EqState(ctx, ctx') - ensures EqInterpResultValue(InterpBlock_Exprs(es, env, ctx), InterpBlock_Exprs(FilterEmptyBlocks_Seq(es), env, ctx')) - { - reveal InterpBlock_Exprs(); - reveal Seq.Filter(); + function method FilterEmptyBlocks_Seq(es: seq): (es': seq) + ensures Seq_All(SupportsInterp, es) ==> Seq_All(SupportsInterp, es') + ensures |es| >= |es'| + { + Seq.Filter(es, IsNotEmptyBlock) + } - var es' := FilterEmptyBlocks_Seq(es); + function method FilterEmptyBlocks_Single(e: Expr): Expr + { + if e.Block? then + Expr.Block(FilterEmptyBlocks_Seq(e.stmts)) + else + e + } - var res := InterpBlock_Exprs(es, env, ctx); - var res' := InterpBlock_Exprs(es', env, ctx'); + lemma FilterEmptyBlocks_Seq_Rel(es: seq, env: Environment, ctx: State, ctx': State) + requires Seq_All(SupportsInterp, es) + requires EqState(ctx, ctx') + ensures EqInterpResultValue(InterpBlock_Exprs(es, env, ctx), InterpBlock_Exprs(FilterEmptyBlocks_Seq(es), env, ctx')) + { + reveal InterpBlock_Exprs(); + reveal Seq.Filter(); - // TODO(SMH): there are too many subcases below: I'm pretty sure we can make the proofs in - // a smarter way. - if es == [] { - // Trivial - } - else if |es| == 1 { - assert es == [es[0]]; - reveal InterpExpr(); - reveal InterpBlock(); - if IsEmptyBlock(es[0]) { - assert es' == []; + var es' := FilterEmptyBlocks_Seq(es); - // Interp(es, ctx) == ((), ctx) - assert InterpBlock_Exprs([es[0]], env, ctx) == InterpExpr(es[0], env, ctx); - assert InterpExpr(es[0], env, ctx) == InterpBlock_Exprs(es[0].stmts, env, ctx); - assert InterpBlock_Exprs(es[0].stmts, env, ctx) == Success(Return(V.Unit, ctx)); + var res := InterpBlock_Exprs(es, env, ctx); + var res' := InterpBlock_Exprs(es', env, ctx'); - // Interp(es', ctx') == ((), ctx') - assert InterpBlock_Exprs(es', env, ctx') == Success(Return(V.Unit, ctx')); - } - else { - assert es' == es; - EqInterp_Refl(es[0]); - EqInterp_Inst(es[0], es[0], env, ctx, ctx'); + // TODO(SMH): there are too many subcases below: I'm pretty sure we can make the proofs in + // a smarter way. + if es == [] { + // Trivial } - } - else { - // Case disjunction: is the first expression in the sequence filtered or not? - if IsEmptyBlock(es[0]) { - // The first expression is filtered - var res0 := InterpExpr(es[0], env, ctx); - - // Evaluating the first expression leaves the context unchanged - assert res0 == Success(Return(V.Unit, ctx)) by { - reveal InterpExpr(); - reveal InterpBlock(); - // Doesn't work without this assertion - assert res0 == InterpBlock(es[0].stmts, env, ctx); - assert es[0].stmts == []; - // Doesn't work without this assertion - assert InterpBlock(es[0].stmts, env, ctx) == InterpBlock_Exprs([], env, ctx); - } + else if |es| == 1 { + assert es == [es[0]]; + reveal InterpExpr(); + reveal InterpBlock(); + if IsEmptyBlock(es[0]) { + assert es' == []; - // Doesn't work without this assertion - assert res0 == InterpExprWithType(es[0], Types.Unit, env, ctx); + // Interp(es, ctx) == ((), ctx) + assert InterpBlock_Exprs([es[0]], env, ctx) == InterpExpr(es[0], env, ctx); + assert InterpExpr(es[0], env, ctx) == InterpBlock_Exprs(es[0].stmts, env, ctx); + assert InterpBlock_Exprs(es[0].stmts, env, ctx) == Success(Return(V.Unit, ctx)); - assert es' == FilterEmptyBlocks_Seq(es[1..]); - FilterEmptyBlocks_Seq_Rel(es[1..], env, ctx, ctx'); + // Interp(es', ctx') == ((), ctx') + assert InterpBlock_Exprs(es', env, ctx') == Success(Return(V.Unit, ctx')); + } + else { + assert es' == es; + EqInterp_Refl(es[0]); + EqInterp_Inst(es[0], es[0], env, ctx, ctx'); + } } else { - // The first expression is not filtered + // Case disjunction: is the first expression in the sequence filtered or not? + if IsEmptyBlock(es[0]) { + // The first expression is filtered + var res0 := InterpExpr(es[0], env, ctx); - EqInterp_Refl(es[0]); - EqInterp_Inst(es[0], es'[0], env, ctx, ctx'); + // Evaluating the first expression leaves the context unchanged + assert res0 == Success(Return(V.Unit, ctx)) by { + reveal InterpExpr(); + reveal InterpBlock(); + // Doesn't work without this assertion + assert res0 == InterpBlock(es[0].stmts, env, ctx); + assert es[0].stmts == []; + // Doesn't work without this assertion + assert InterpBlock(es[0].stmts, env, ctx) == InterpBlock_Exprs([], env, ctx); + } - var tl := es[1..]; - var tl' := FilterEmptyBlocks_Seq(tl); + // Doesn't work without this assertion + assert res0 == InterpExprWithType(es[0], Types.Unit, env, ctx); - forall env, ctx, ctx' | EqState(ctx, ctx') - ensures EqInterpResultValue(InterpBlock_Exprs(tl, env, ctx), InterpBlock_Exprs(tl', env, ctx')) - { - FilterEmptyBlocks_Seq_Rel(tl, env, ctx, ctx'); + assert es' == FilterEmptyBlocks_Seq(es[1..]); + FilterEmptyBlocks_Seq_Rel(es[1..], env, ctx, ctx'); + } + else { + // The first expression is not filtered + + EqInterp_Refl(es[0]); + EqInterp_Inst(es[0], es'[0], env, ctx, ctx'); + + var tl := es[1..]; + var tl' := FilterEmptyBlocks_Seq(tl); + + forall env, ctx, ctx' | EqState(ctx, ctx') + ensures EqInterpResultValue(InterpBlock_Exprs(tl, env, ctx), InterpBlock_Exprs(tl', env, ctx')) + { + FilterEmptyBlocks_Seq_Rel(tl, env, ctx, ctx'); + } + InterpBlock_Exprs_Eq_Append(es[0], es[0], tl, tl', env, ctx, ctx'); } - InterpBlock_Exprs_Eq_Append(es[0], es[0], tl, tl', env, ctx, ctx'); } } - } - lemma FilterEmptyBlocks_Single_Rel(e: Expr) - ensures Tr_Expr_Rel(e, FilterEmptyBlocks_Single(e)) - { - if e.Block? && SupportsInterp(e) { - reveal SupportsInterp(); + lemma FilterEmptyBlocks_Single_Rel(e: Expr) + ensures Tr_Expr_Rel(e, FilterEmptyBlocks_Single(e)) + { + if e.Block? && SupportsInterp(e) { + reveal SupportsInterp(); - var e' := FilterEmptyBlocks_Single(e); - var es := e.stmts; + var e' := FilterEmptyBlocks_Single(e); + var es := e.stmts; - forall env, ctx, ctx' | EqState(ctx, ctx') - ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) - { + forall env, ctx, ctx' | EqState(ctx, ctx') + ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) + { FilterEmptyBlocks_Seq_Rel(es, env, ctx, ctx'); reveal InterpExpr(); reveal InterpBlock(); - } + } - assert SupportsInterp(e'); - assert EqInterp(e, e'); - } - else { - EqInterp_Refl(e); + assert SupportsInterp(e'); + assert EqInterp(e, e'); + } + else { + EqInterp_Refl(e); + } } } -} - -module InlineLastBlock { - // Tranformation 2 - - import Utils.Lib - import Utils.Lib.Debug - import opened Utils.Lib.Datatypes - import opened Transforms.BottomUp - import opened AST.Syntax - import opened AST.Predicates - import opened Semantics.Interp - import opened Semantics.Values - import opened Semantics.Equiv - import opened Transforms.Generic - import opened Transforms.Proofs.BottomUp_ - - import opened FilterCommon - - type Expr = Syntax.Expr + module InlineLastBlock { + // Tranformation 2 + + import Utils.Lib + import Utils.Lib.Debug + import opened Utils.Lib.Datatypes + import opened Transforms.BottomUp + + import opened AST.Syntax + import opened AST.Predicates + import opened Semantics.Interp + import opened Semantics.Values + import opened Semantics.Equiv + import opened Transforms.Generic + import opened Transforms.Proofs.BottomUp_ + + import opened FilterCommon + + type Expr = Syntax.Expr + + function method InlineLastBlock_Seq(es: seq): (es': seq) + ensures Seq_All(SupportsInterp, es) ==> Seq_All(SupportsInterp, es') + // If the last expression of a sequence of expressions is a block, inline its content. + // + // It seems easier to reason about this function if we define it in a recursive way, + // which is why we do so. + { + reveal SupportsInterp(); - function method InlineLastBlock_Seq(es: seq): (es': seq) - ensures Seq_All(SupportsInterp, es) ==> Seq_All(SupportsInterp, es') - // If the last expression of a sequence of expressions is a block, inline its content. - // - // It seems easier to reason about this function if we define it in a recursive way, - // which is why we do so. - { - reveal SupportsInterp(); - - // Empty sequence: nothing to do - if es == [] then - [] - // We reached the last statement: inline it if it is a block - else if |es| == 1 then - if es[0].Block? then - assert Seq_All(SupportsInterp, es) ==> SupportsInterp(es[0]); - assert SupportsInterp(es[0]) ==> Seq_All(SupportsInterp, es[0].stmts); - es[0].stmts + // Empty sequence: nothing to do + if es == [] then + [] + // We reached the last statement: inline it if it is a block + else if |es| == 1 then + if es[0].Block? then + assert Seq_All(SupportsInterp, es) ==> SupportsInterp(es[0]); + assert SupportsInterp(es[0]) ==> Seq_All(SupportsInterp, es[0].stmts); + es[0].stmts + else + [es[0]] + // We haven't reached the last element: recurse on the tail else - [es[0]] - // We haven't reached the last element: recurse on the tail - else - [es[0]] + InlineLastBlock_Seq(es[1..]) - } + [es[0]] + InlineLastBlock_Seq(es[1..]) + } - function method InlineLastBlock_Single(e: Expr): Expr - { - if e.Block? then Expr.Block(InlineLastBlock_Seq(e.stmts)) - else e - } + function method InlineLastBlock_Single(e: Expr): Expr + { + if e.Block? then Expr.Block(InlineLastBlock_Seq(e.stmts)) + else e + } - lemma InlineLastBlock_Seq_Rel(es: seq, env: Environment, ctx: State, ctx': State) - requires forall e | e in es :: SupportsInterp(e) - requires EqState(ctx, ctx') - ensures forall e | e in InlineLastBlock_Seq(es) :: SupportsInterp(e) - ensures EqInterpResultValue(InterpBlock_Exprs(es, env, ctx), InterpBlock_Exprs(InlineLastBlock_Seq(es), env, ctx')) - { - reveal InterpBlock_Exprs(); + lemma InlineLastBlock_Seq_Rel(es: seq, env: Environment, ctx: State, ctx': State) + requires forall e | e in es :: SupportsInterp(e) + requires EqState(ctx, ctx') + ensures forall e | e in InlineLastBlock_Seq(es) :: SupportsInterp(e) + ensures EqInterpResultValue(InterpBlock_Exprs(es, env, ctx), InterpBlock_Exprs(InlineLastBlock_Seq(es), env, ctx')) + { + reveal InterpBlock_Exprs(); - var es' := InlineLastBlock_Seq(es); + var es' := InlineLastBlock_Seq(es); - var res := InterpBlock_Exprs(es, env, ctx); - var res' := InterpBlock_Exprs(es', env, ctx'); + var res := InterpBlock_Exprs(es, env, ctx); + var res' := InterpBlock_Exprs(es', env, ctx'); - if es == [] { - // Trivial - } - else if |es| == 1 { - if es[0].Block? { - reveal InterpExpr(); - reveal InterpBlock(); + if es == [] { + // Trivial + } + else if |es| == 1 { + if es[0].Block? { + reveal InterpExpr(); + reveal InterpBlock(); - // Doesn't work without this assertion - is it because of the fuel? - assert res == InterpExpr(es[0], env, ctx); - assert InterpExpr(es[0], env, ctx) == InterpBlock(es[0].stmts, env, ctx); + // Doesn't work without this assertion - is it because of the fuel? + assert res == InterpExpr(es[0], env, ctx); + assert InterpExpr(es[0], env, ctx) == InterpBlock(es[0].stmts, env, ctx); - assert es' == es[0].stmts; - InterpBlock_Exprs_Refl(es[0].stmts, env, ctx, ctx'); + assert es' == es[0].stmts; + InterpBlock_Exprs_Refl(es[0].stmts, env, ctx, ctx'); + } + else { + assert es == es'; + InterpBlock_Exprs_Refl(es, env, ctx, ctx'); + } } else { - assert es == es'; - InterpBlock_Exprs_Refl(es, env, ctx, ctx'); - } - } - else { - // The first expression appears in both sequences - EqInterp_Refl(es[0]); - EqInterp_Inst(es[0], es'[0], env, ctx, ctx'); - - // Prove that the sequence concatenations are evaluated in a similar manner - var tl := es[1..]; - var tl' := InlineLastBlock_Seq(tl); - - forall env, ctx, ctx' | EqState(ctx, ctx') - ensures EqInterpResultValue(InterpBlock_Exprs(tl, env, ctx), InterpBlock_Exprs(tl', env, ctx')) - { - InlineLastBlock_Seq_Rel(tl, env, ctx, ctx'); + // The first expression appears in both sequences + EqInterp_Refl(es[0]); + EqInterp_Inst(es[0], es'[0], env, ctx, ctx'); + + // Prove that the sequence concatenations are evaluated in a similar manner + var tl := es[1..]; + var tl' := InlineLastBlock_Seq(tl); + + forall env, ctx, ctx' | EqState(ctx, ctx') + ensures EqInterpResultValue(InterpBlock_Exprs(tl, env, ctx), InterpBlock_Exprs(tl', env, ctx')) + { + InlineLastBlock_Seq_Rel(tl, env, ctx, ctx'); + } + InterpBlock_Exprs_Eq_Append(es[0], es[0], tl, tl', env, ctx, ctx'); } - InterpBlock_Exprs_Eq_Append(es[0], es[0], tl, tl', env, ctx, ctx'); } - } - // Rk.: modulo the names, this is exactly the same proof as for ``FilterEmptyBlocks_Single_Rel`` - lemma InlineLastBlock_Single_Rel(e: Expr) - ensures Tr_Expr_Rel(e, InlineLastBlock_Single(e)) - { - if e.Block? && SupportsInterp(e) { - reveal SupportsInterp(); + // Rk.: modulo the names, this is exactly the same proof as for ``FilterEmptyBlocks_Single_Rel`` + lemma InlineLastBlock_Single_Rel(e: Expr) + ensures Tr_Expr_Rel(e, InlineLastBlock_Single(e)) + { + if e.Block? && SupportsInterp(e) { + reveal SupportsInterp(); - var e' := InlineLastBlock_Single(e); - var es := e.stmts; + var e' := InlineLastBlock_Single(e); + var es := e.stmts; - forall env, ctx, ctx' | EqState(ctx, ctx') - ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) - { + forall env, ctx, ctx' | EqState(ctx, ctx') + ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) + { InlineLastBlock_Seq_Rel(es, env, ctx, ctx'); reveal InterpExpr(); reveal InterpBlock(); - } + } - assert SupportsInterp(e'); - assert EqInterp(e, e'); - } - else { - EqInterp_Refl(e); + assert SupportsInterp(e'); + assert EqInterp(e, e'); + } + else { + EqInterp_Refl(e); + } } } -} - -module SimplifyIfThenElse { - // Tranformation 3 - - import Utils.Lib - import Utils.Lib.Debug - import opened Utils.Lib.Datatypes - import opened Transforms.BottomUp - import opened AST.Syntax - import opened AST.Predicates - import opened Semantics.Interp - import opened Semantics.Values - import opened Semantics.Equiv - import opened Semantics.Pure - import opened Transforms.Generic - import opened Transforms.Proofs.BottomUp_ - - import opened FilterCommon + module SimplifyIfThenElse { + // Tranformation 3 + + import Utils.Lib + import Utils.Lib.Debug + import opened Utils.Lib.Datatypes + import opened Transforms.BottomUp + + import opened AST.Syntax + import opened AST.Predicates + import opened Semantics.Interp + import opened Semantics.Values + import opened Semantics.Equiv + import opened Semantics.Pure + import opened Transforms.Generic + import opened Transforms.Proofs.BottomUp_ + + import opened FilterCommon + + type Expr = Syntax.Expr + + function method SimplifyEmptyIfThenElse_Single(e: Expr): Expr + // Tranformation 3.1: `if b then {} else {} ---> {}` + // + // Eliminating `b` might lead to a program which fails less. We might want to be + // more precise in case we deal with potentially non-terminating programs, for instance + // by checking that `b` doesn't call any (potentially non-terminating) method. + { + // We might want to check that `e.cond` terminates + if e.If? && IsPure(e.cond) && IsEmptyBlock(e.thn) && IsEmptyBlock(e.els) then EmptyBlock + else e + } - type Expr = Syntax.Expr + lemma SimplifyEmptyIfThenElse_Single_Rel(e: Expr) + ensures Tr_Expr_Rel(e, SimplifyEmptyIfThenElse_Single(e)) + { + if e.If? && IsPure(e.cond) && IsEmptyBlock(e.thn) && IsEmptyBlock(e.els) && SupportsInterp(e) { + var e' := SimplifyEmptyIfThenElse_Single(e); + reveal SupportsInterp(); - function method SimplifyEmptyIfThenElse_Single(e: Expr): Expr - // Tranformation 3.1: `if b then {} else {} ---> {}` - // - // Eliminating `b` might lead to a program which fails less. We might want to be - // more precise in case we deal with potentially non-terminating programs, for instance - // by checking that `b` doesn't call any (potentially non-terminating) method. - { - // We might want to check that `e.cond` terminates - if e.If? && IsPure(e.cond) && IsEmptyBlock(e.thn) && IsEmptyBlock(e.els) then EmptyBlock - else e - } + forall env, ctx, ctx' | EqState(ctx, ctx') + ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) + { + var res := InterpExpr(e, env, ctx); + var res0 := InterpExprWithType(e.cond, Type.Bool, env, ctx); - lemma SimplifyEmptyIfThenElse_Single_Rel(e: Expr) - ensures Tr_Expr_Rel(e, SimplifyEmptyIfThenElse_Single(e)) - { - if e.If? && IsPure(e.cond) && IsEmptyBlock(e.thn) && IsEmptyBlock(e.els) && SupportsInterp(e) { - var e' := SimplifyEmptyIfThenElse_Single(e); - reveal SupportsInterp(); + if res0.Success? { + var Return(b, ctx0) := res0.value; - forall env, ctx, ctx' | EqState(ctx, ctx') - ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) - { - var res := InterpExpr(e, env, ctx); - var res0 := InterpExprWithType(e.cond, Type.Bool, env, ctx); + InterpExprWithType_IsPure_SameState(e.cond, Type.Bool, env, ctx); + assert ctx0 == ctx; - if res0.Success? { - var Return(b, ctx0) := res0.value; + assert res == InterpExpr(EmptyBlock, env, ctx0) by { + reveal InterpExpr(); + } - InterpExprWithType_IsPure_SameState(e.cond, Type.Bool, env, ctx); - assert ctx0 == ctx; - - assert res == InterpExpr(EmptyBlock, env, ctx0) by { - reveal InterpExpr(); + EqInterp_Refl(EmptyBlock); + EqInterp_Inst(EmptyBlock, EmptyBlock, env, ctx, ctx'); } - - EqInterp_Refl(EmptyBlock); - EqInterp_Inst(EmptyBlock, EmptyBlock, env, ctx, ctx'); - } - else { - assert res.Failure? by { - reveal InterpExpr(); + else { + assert res.Failure? by { + reveal InterpExpr(); + } } } - } - assert SupportsInterp(e'); - } - else { - EqInterp_Refl(e); + assert SupportsInterp(e'); + } + else { + EqInterp_Refl(e); + } } - } - // TODO: factorize with ``EliminateNegatedBinops``? - function method NegateExpr(e: Expr): (e':Expr) - ensures SupportsInterp(e) ==> SupportsInterp(e') - { - reveal SupportsInterp(); - Exprs.Apply(Exprs.Eager(Exprs.UnaryOp(UnaryOps.BoolNot)), [e]) - } + // TODO: factorize with ``EliminateNegatedBinops``? + function method NegateExpr(e: Expr): (e':Expr) + ensures SupportsInterp(e) ==> SupportsInterp(e') + { + reveal SupportsInterp(); + Exprs.Apply(Exprs.Eager(Exprs.UnaryOp(UnaryOps.BoolNot)), [e]) + } - // TODO: factorize with ``EliminateNegatedBinops``? - lemma InterpExpr_NegateExpr(e: Expr, env: Environment, ctx: State) - requires SupportsInterp(e) - ensures - match InterpExpr(e, env, ctx) + // TODO: factorize with ``EliminateNegatedBinops``? + lemma InterpExpr_NegateExpr(e: Expr, env: Environment, ctx: State) + requires SupportsInterp(e) + ensures + match InterpExpr(e, env, ctx) case Failure(_) => true case Success(Return(v, ctx1)) => match InterpExpr(NegateExpr(e), env, ctx) @@ -494,208 +494,208 @@ module SimplifyIfThenElse { && v'.Bool? && v.b == !v'.b && ctx1' == ctx1 - { - var res := InterpExpr(e, env, ctx); - var e' := NegateExpr(e); - var res' := InterpExpr(e', env, ctx); - - var args := [e]; - var args_res := InterpExprs(args, env, ctx); - InterpExprs1_Strong_Eq(e, env, ctx); - - reveal InterpExpr(); - - if args_res.Success? { - reveal InterpUnaryOp(); + { + var res := InterpExpr(e, env, ctx); + var e' := NegateExpr(e); + var res' := InterpExpr(e', env, ctx); + + var args := [e]; + var args_res := InterpExprs(args, env, ctx); + InterpExprs1_Strong_Eq(e, env, ctx); + + reveal InterpExpr(); + + if args_res.Success? { + reveal InterpUnaryOp(); + } + else {} } - else {} - } - function method NegateIfThenElse_Single(e: Expr): (e': Expr) - ensures SupportsInterp(e) ==> SupportsInterp(e') - // Auxiliary transformation: `if b then e0 else e1 ---> if !b then e1 else e0` - { - reveal SupportsInterp(); - if e.If? then Expr.If(NegateExpr(e.cond), e.els, e.thn) - else e - } - - - lemma NegateIfThenElse_Single_Rel(e: Expr) - ensures Tr_Expr_Rel(e, NegateIfThenElse_Single(e)) - { - if e.If? && SupportsInterp(e) { - var e' := NegateIfThenElse_Single(e); - + function method NegateIfThenElse_Single(e: Expr): (e': Expr) + ensures SupportsInterp(e) ==> SupportsInterp(e') + // Auxiliary transformation: `if b then e0 else e1 ---> if !b then e1 else e0` + { reveal SupportsInterp(); + if e.If? then Expr.If(NegateExpr(e.cond), e.els, e.thn) + else e + } - forall env, ctx, ctx' | EqState(ctx, ctx') - ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) - { - var res := InterpExpr(e, env, ctx); - var res' := InterpExpr(e', env, ctx); - - var res0 := InterpExprWithType(e.cond, Type.Bool, env, ctx); - var res0' := InterpExprWithType(e.cond, Type.Bool, env, ctx'); - EqInterp_Refl(e.cond); - EqInterp_Inst(e.cond, e.cond, env, ctx, ctx'); - - var res0'' := InterpExprWithType(e'.cond, Type.Bool, env, ctx'); - InterpExpr_NegateExpr(e.cond, env, ctx'); + lemma NegateIfThenElse_Single_Rel(e: Expr) + ensures Tr_Expr_Rel(e, NegateIfThenElse_Single(e)) + { + if e.If? && SupportsInterp(e) { + var e' := NegateIfThenElse_Single(e); - reveal InterpExpr(); - if res.Success? { - assert res0'.Success?; - assert res0''.Success?; + reveal SupportsInterp(); - var Return(b, ctx0) := res0.value; - var Return(b'', ctx0'') := res0''.value; + forall env, ctx, ctx' | EqState(ctx, ctx') + ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) + { + var res := InterpExpr(e, env, ctx); + var res' := InterpExpr(e', env, ctx); - assert b.Bool? && b''.Bool? && b.b == !b''.b; + var res0 := InterpExprWithType(e.cond, Type.Bool, env, ctx); + var res0' := InterpExprWithType(e.cond, Type.Bool, env, ctx'); - EqInterp_Refl(e.thn); - EqInterp_Inst(e.thn, e.thn, env, ctx0, ctx0''); - EqInterp_Refl(e.els); - EqInterp_Inst(e.els, e.els, env, ctx0, ctx0''); - } - else {} - } + EqInterp_Refl(e.cond); + EqInterp_Inst(e.cond, e.cond, env, ctx, ctx'); - assert SupportsInterp(e'); - } - else { - EqInterp_Refl(e); - } - } + var res0'' := InterpExprWithType(e'.cond, Type.Bool, env, ctx'); + InterpExpr_NegateExpr(e.cond, env, ctx'); - function method NegateIfThenElseIfEmptyThen_Single(e: Expr): (e': Expr) - ensures SupportsInterp(e) ==> SupportsInterp(e') - // Tranformation 3.2: `if b then {} else e ---> if !b then e else {}` - { - reveal SupportsInterp(); - if e.If? && IsEmptyBlock(e.thn) then NegateIfThenElse_Single(e) - else e - } + reveal InterpExpr(); + if res.Success? { + assert res0'.Success?; + assert res0''.Success?; - lemma NegateIfThenElseIfEmptyThen_Single_Rel(e: Expr) - ensures Tr_Expr_Rel(e, NegateIfThenElseIfEmptyThen_Single(e)) - { - if e.If? && IsEmptyBlock(e.thn) { - NegateIfThenElse_Single_Rel(e); - } - else { - EqInterp_Refl(e); - } - } + var Return(b, ctx0) := res0.value; + var Return(b'', ctx0'') := res0''.value; - function method Simplify_Single(e: Expr): (e': Expr) - ensures SupportsInterp(e) ==> SupportsInterp(e') - ensures Tr_Expr_Rel(e, e') - // The full transformation 3 - { - reveal SupportsInterp(); - var e1 := SimplifyEmptyIfThenElse_Single(e); - SimplifyEmptyIfThenElse_Single_Rel(e); - var e2 := NegateIfThenElseIfEmptyThen_Single(e1); - NegateIfThenElseIfEmptyThen_Single_Rel(e1); - EqInterp_Trans(e, e1, e2); - e2 - } -} + assert b.Bool? && b''.Bool? && b.b == !b''.b; -module Simplify { - /// The final transformation - - import Utils.Lib - import Utils.Lib.Debug - import opened Utils.Lib.Datatypes - import opened Transforms.BottomUp + EqInterp_Refl(e.thn); + EqInterp_Inst(e.thn, e.thn, env, ctx0, ctx0''); + EqInterp_Refl(e.els); + EqInterp_Inst(e.els, e.els, env, ctx0, ctx0''); + } + else {} + } - import opened AST.Syntax - import opened AST.Predicates - import opened Semantics.Interp - import opened Semantics.Values - import opened Semantics.Equiv - import opened Semantics.Pure - import opened Transforms.Generic - import opened Transforms.Proofs.BottomUp_ + assert SupportsInterp(e'); + } + else { + EqInterp_Refl(e); + } + } - import opened FilterCommon - import FilterEmptyBlocks - import InlineLastBlock - import SimplifyIfThenElse + function method NegateIfThenElseIfEmptyThen_Single(e: Expr): (e': Expr) + ensures SupportsInterp(e) ==> SupportsInterp(e') + // Tranformation 3.2: `if b then {} else e ---> if !b then e else {}` + { + reveal SupportsInterp(); + if e.If? && IsEmptyBlock(e.thn) then NegateIfThenElse_Single(e) + else e + } - type Expr = Syntax.Expr + lemma NegateIfThenElseIfEmptyThen_Single_Rel(e: Expr) + ensures Tr_Expr_Rel(e, NegateIfThenElseIfEmptyThen_Single(e)) + { + if e.If? && IsEmptyBlock(e.thn) { + NegateIfThenElse_Single_Rel(e); + } + else { + EqInterp_Refl(e); + } + } - function method Simplify_Single(e: Expr): (e': Expr) - ensures SupportsInterp(e) ==> SupportsInterp(e') - ensures EqInterp(e, e') - // This function puts all the transformation together - { - var e1 := FilterEmptyBlocks.FilterEmptyBlocks_Single(e); - FilterEmptyBlocks.FilterEmptyBlocks_Single_Rel(e); - assert EqInterp(e, e1); - var e2 := InlineLastBlock.InlineLastBlock_Single(e1); - InlineLastBlock.InlineLastBlock_Single_Rel(e1); - assert EqInterp(e1, e2); - var e3 := SimplifyIfThenElse.Simplify_Single(e2); - assert EqInterp(e2, e3); - - EqInterp_Trans(e, e1, e2); - EqInterp_Trans(e, e2, e3); - assert EqInterp(e, e3); - - e3 + function method Simplify_Single(e: Expr): (e': Expr) + ensures SupportsInterp(e) ==> SupportsInterp(e') + ensures Tr_Expr_Rel(e, e') + // The full transformation 3 + { + reveal SupportsInterp(); + var e1 := SimplifyEmptyIfThenElse_Single(e); + SimplifyEmptyIfThenElse_Single_Rel(e); + var e2 := NegateIfThenElseIfEmptyThen_Single(e1); + NegateIfThenElseIfEmptyThen_Single_Rel(e1); + EqInterp_Trans(e, e1, e2); + e2 + } } - predicate Tr_Pre(p: Program) { - true - } + module Simplify { + /// The final transformation + + import Utils.Lib + import Utils.Lib.Debug + import opened Utils.Lib.Datatypes + import opened Transforms.BottomUp + + import opened AST.Syntax + import opened AST.Predicates + import opened Semantics.Interp + import opened Semantics.Values + import opened Semantics.Equiv + import opened Semantics.Pure + import opened Transforms.Generic + import opened Transforms.Proofs.BottomUp_ + + import opened FilterCommon + import FilterEmptyBlocks + import InlineLastBlock + import SimplifyIfThenElse + + type Expr = Syntax.Expr + + function method Simplify_Single(e: Expr): (e': Expr) + ensures SupportsInterp(e) ==> SupportsInterp(e') + ensures EqInterp(e, e') + // This function puts all the transformation together + { + var e1 := FilterEmptyBlocks.FilterEmptyBlocks_Single(e); + FilterEmptyBlocks.FilterEmptyBlocks_Single_Rel(e); + assert EqInterp(e, e1); + var e2 := InlineLastBlock.InlineLastBlock_Single(e1); + InlineLastBlock.InlineLastBlock_Single_Rel(e1); + assert EqInterp(e1, e2); + var e3 := SimplifyIfThenElse.Simplify_Single(e2); + assert EqInterp(e2, e3); + + EqInterp_Trans(e, e1, e2); + EqInterp_Trans(e, e2, e3); + assert EqInterp(e, e3); + + e3 + } - predicate Tr_Expr_Post(e: Exprs.T) { - true - } + predicate Tr_Pre(p: Program) { + true + } - predicate Tr_Post(p: Program) - { - Deep.All_Program(p, Tr_Expr_Post) - } + predicate Tr_Expr_Post(e: Exprs.T) { + true + } - const Tr_Expr : BottomUpTransformer := - ( Deep.All_Expr_True_Forall(Tr_Expr_Post); - assert IsBottomUpTransformer(Simplify_Single, Tr_Expr_Post); - TR(Simplify_Single, - Tr_Expr_Post)) - - function method Apply_Method(m: Method) : (m': Method) - ensures Deep.All_Method(m', Tr_Expr_Post) - ensures Tr_Expr_Rel(m.methodBody, m'.methodBody) - // Apply the transformation to a method. - // - // We need it on a temporary basis, so that we can apply the transformation - // to all the methods in a program (we haven't defined modules, classes, - // etc. yet). When the `Program` definition is complete enough, we will - // remove this definition and exclusively use `Apply`. - { - Deep.All_Expr_True_Forall(Tr_Expr.f.requires); - assert Deep.All_Method(m, Tr_Expr.f.requires); - EqInterp_Lift(Tr_Expr.f); - Map_Method_PreservesRel(m, Tr_Expr, Tr_Expr_Rel); - Map_Method(m, Tr_Expr) - } + predicate Tr_Post(p: Program) + { + Deep.All_Program(p, Tr_Expr_Post) + } + + const Tr_Expr : BottomUpTransformer := + ( Deep.All_Expr_True_Forall(Tr_Expr_Post); + assert IsBottomUpTransformer(Simplify_Single, Tr_Expr_Post); + TR(Simplify_Single, + Tr_Expr_Post)) + + function method Apply_Method(m: Method) : (m': Method) + ensures Deep.All_Method(m', Tr_Expr_Post) + ensures Tr_Expr_Rel(m.methodBody, m'.methodBody) + // Apply the transformation to a method. + // + // We need it on a temporary basis, so that we can apply the transformation + // to all the methods in a program (we haven't defined modules, classes, + // etc. yet). When the `Program` definition is complete enough, we will + // remove this definition and exclusively use `Apply`. + { + Deep.All_Expr_True_Forall(Tr_Expr.f.requires); + assert Deep.All_Method(m, Tr_Expr.f.requires); + EqInterp_Lift(Tr_Expr.f); + Map_Method_PreservesRel(m, Tr_Expr, Tr_Expr_Rel); + Map_Method(m, Tr_Expr) + } - function method Apply(p: Program) : (p': Program) - requires Tr_Pre(p) - ensures Tr_Post(p') - ensures Tr_Expr_Rel(p.mainMethod.methodBody, p'.mainMethod.methodBody) - // Apply the transformation to a program. - { - Deep.All_Expr_True_Forall(Tr_Expr.f.requires); - assert Deep.All_Program(p, Tr_Expr.f.requires); - EqInterp_Lift(Tr_Expr.f); - Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel); - Map_Program(p, Tr_Expr) + function method Apply(p: Program) : (p': Program) + requires Tr_Pre(p) + ensures Tr_Post(p') + ensures Tr_Expr_Rel(p.mainMethod.methodBody, p'.mainMethod.methodBody) + // Apply the transformation to a program. + { + Deep.All_Expr_True_Forall(Tr_Expr.f.requires); + assert Deep.All_Program(p, Tr_Expr.f.requires); + EqInterp_Lift(Tr_Expr.f); + Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel); + Map_Program(p, Tr_Expr) + } } } -} diff --git a/src/REPL/Repl.dfy b/src/REPL/Repl.dfy index 577d6873..df82759f 100644 --- a/src/REPL/Repl.dfy +++ b/src/REPL/Repl.dfy @@ -1,4 +1,4 @@ -include "../Semantics/Interp.dfy" + include "../Semantics/Interp.dfy" include "../AST/Syntax.dfy" include "../AST/Translator.dfy" include "../Semantics/Printer.dfy" @@ -19,86 +19,86 @@ module Bootstrap.REPL { import opened Interop.CSharpDafnyInterop import C = Interop.CSharpDafnyASTModel -module {:extern "REPLInterop"} {:compile false} REPLInterop { - // BUG(TODO) - import System - import C = Interop.CSharpDafnyASTModel + module {:extern "REPLInterop"} {:compile false} REPLInterop { + // BUG(TODO) + import System + import C = Interop.CSharpDafnyASTModel - class {:compile false} {:extern} Utils { - constructor {:extern} () requires false + class {:compile false} {:extern} Utils { + constructor {:extern} () requires false - static method {:extern} Initialize() + static method {:extern} Initialize() - static method {:extern} ReadLine() - returns (e: System.String?) + static method {:extern} ReadLine() + returns (e: System.String?) - static method {:extern} RunWithCustomStack(f: A -> B, a0: A, size: System.int32) - returns (b: B) - ensures b == f(a0) - } + static method {:extern} RunWithCustomStack(f: A -> B, a0: A, size: System.int32) + returns (b: B) + ensures b == f(a0) + } - trait {:compile false} {:extern} ParseResult { - lemma Sealed() - ensures || this is FailedParse - || this is SuccessfulParse - } - class {:compile false} {:extern} FailedParse extends ParseResult { - lemma Sealed() {} - constructor {:extern} () requires false - var {:extern} Incomplete: bool; - var {:extern} Message: System.String; - } - class {:compile false} {:extern} SuccessfulParse extends ParseResult { - method {:extern} Resolve() returns (r: ResolutionResult) - lemma Sealed() {} - } + trait {:compile false} {:extern} ParseResult { + lemma Sealed() + ensures || this is FailedParse + || this is SuccessfulParse + } + class {:compile false} {:extern} FailedParse extends ParseResult { + lemma Sealed() {} + constructor {:extern} () requires false + var {:extern} Incomplete: bool; + var {:extern} Message: System.String; + } + class {:compile false} {:extern} SuccessfulParse extends ParseResult { + method {:extern} Resolve() returns (r: ResolutionResult) + lemma Sealed() {} + } - trait {:compile false} {:extern} ResolutionResult { - lemma Sealed() - ensures || this is ResolutionError - || this is TypecheckedProgram - } - class {:compile false} {:extern} ResolutionError extends ResolutionResult { - lemma Sealed() {} - constructor {:extern} () requires false - var {:extern} Message: System.String; - } - class {:compile false} {:extern} TypecheckedProgram extends ResolutionResult { - lemma Sealed() {} - constructor {:extern} () requires false - var {:extern} NewInputs: System.Collections.Generic.List; - } + trait {:compile false} {:extern} ResolutionResult { + lemma Sealed() + ensures || this is ResolutionError + || this is TypecheckedProgram + } + class {:compile false} {:extern} ResolutionError extends ResolutionResult { + lemma Sealed() {} + constructor {:extern} () requires false + var {:extern} Message: System.String; + } + class {:compile false} {:extern} TypecheckedProgram extends ResolutionResult { + lemma Sealed() {} + constructor {:extern} () requires false + var {:extern} NewInputs: System.Collections.Generic.List; + } - trait {:compile false} {:extern} UserInput { - lemma Sealed() - ensures || this is MemberDeclInput - var {:extern} FullName: System.String; - var {:extern} ShortName: System.String; - } - class {:compile false} {:extern} MemberDeclInput extends UserInput { - lemma Sealed() {} - constructor {:extern} () requires false - var {:extern} IsTopLevelExpr: bool; - var {:extern} Decl: C.MemberDecl; - } + trait {:compile false} {:extern} UserInput { + lemma Sealed() + ensures || this is MemberDeclInput + var {:extern} FullName: System.String; + var {:extern} ShortName: System.String; + } + class {:compile false} {:extern} MemberDeclInput extends UserInput { + lemma Sealed() {} + constructor {:extern} () requires false + var {:extern} IsTopLevelExpr: bool; + var {:extern} Decl: C.MemberDecl; + } - class {:compile false} {:extern} REPLState { - constructor {:extern} () - method {:extern} TryParse(input: System.String) returns (p: ParseResult) + class {:compile false} {:extern} REPLState { + constructor {:extern} () + method {:extern} TryParse(input: System.String) returns (p: ParseResult) + } } -} -datatype REPLError = - | EOF() - | StackOverflow() - | FailedParse(pmsg: string) - | ResolutionError(rmsg: string) - | TranslationError(te: Translator.TranslationError) - | InterpError(ie: Interp.InterpError) - | Unsupported(e: Syntax.Expr) -{ - function method ToString() : string { - match this + datatype REPLError = + | EOF() + | StackOverflow() + | FailedParse(pmsg: string) + | ResolutionError(rmsg: string) + | TranslationError(te: Translator.TranslationError) + | InterpError(ie: Interp.InterpError) + | Unsupported(e: Syntax.Expr) + { + function method ToString() : string { + match this case EOF() => "EOF" case StackOverflow() => @@ -113,159 +113,159 @@ datatype REPLError = "Execution error: " + ie.ToString() case Unsupported(ex) => "Unsupported expression" // FIXME change checker to return the unsupported subexpression + } } -} -type REPLResult<+A> = Result + type REPLResult<+A> = Result -datatype Named<+A> = Named(fullName: string, shortName: string, body: A) + datatype Named<+A> = Named(fullName: string, shortName: string, body: A) -class REPL { - var state: REPLInterop.REPLState; - var globals: Interp.Context; - var counter: int; + class REPL { + var state: REPLInterop.REPLState; + var globals: Interp.Context; + var counter: int; - constructor() { - state := new REPLInterop.REPLState(); - globals := map[]; - counter := 0; - } + constructor() { + state := new REPLInterop.REPLState(); + globals := map[]; + counter := 0; + } - static method ReadLine(prompt: string) - returns (o: Option) - decreases * - { - while true + static method ReadLine(prompt: string) + returns (o: Option) decreases * { - print prompt; - var line := REPLInterop.Utils.ReadLine(); - if line == null { - return None; - } else { - var line := TypeConv.AsString(line); - if line == "" { - continue; + while true + decreases * + { + print prompt; + var line := REPLInterop.Utils.ReadLine(); + if line == null { + return None; + } else { + var line := TypeConv.AsString(line); + if line == "" { + continue; + } + return Some(line); } - return Some(line); } } - } - method Read() returns (r: REPLResult) - modifies this`counter - decreases * - { - var prompt := "dfy[" + Lib.Str.of_int(counter) + "] "; - var input: string := ""; - counter := counter + 1; - while true - invariant |prompt| > 0 + method Read() returns (r: REPLResult) + modifies this`counter decreases * { - var ln := ReadLine(prompt); - var line :- ln.ToSuccessOr(EOF()); - - input := input + line + "\n"; - var parsed: REPLInterop.ParseResult := - state.TryParse(StringUtils.ToCString(input)); - - if parsed is REPLInterop.FailedParse { - var p := parsed as REPLInterop.FailedParse; // BUG(https://github.com/dafny-lang/dafny/issues/1731) - if p.Incomplete { - prompt := if prompt[0] == '.' then prompt - else seq(|prompt| - 1, _ => '.') + " "; - continue; + var prompt := "dfy[" + Lib.Str.of_int(counter) + "] "; + var input: string := ""; + counter := counter + 1; + while true + invariant |prompt| > 0 + decreases * + { + var ln := ReadLine(prompt); + var line :- ln.ToSuccessOr(EOF()); + + input := input + line + "\n"; + var parsed: REPLInterop.ParseResult := + state.TryParse(StringUtils.ToCString(input)); + + if parsed is REPLInterop.FailedParse { + var p := parsed as REPLInterop.FailedParse; // BUG(https://github.com/dafny-lang/dafny/issues/1731) + if p.Incomplete { + prompt := if prompt[0] == '.' then prompt + else seq(|prompt| - 1, _ => '.') + " "; + continue; + } + return Failure(FailedParse(TypeConv.AsString(p.Message))); + } else { + parsed.Sealed(); + return Success(parsed as REPLInterop.SuccessfulParse); } - return Failure(FailedParse(TypeConv.AsString(p.Message))); - } else { - parsed.Sealed(); - return Success(parsed as REPLInterop.SuccessfulParse); } } - } - function method AbsOfFunction(fn: C.Function) - : Result - reads * - { - var inParams := Lib.Seq.MapFilter(CSharpInterop.ListUtils.ToSeq(fn.Formals), (f: C.Formal) reads * => - if f.InParam then Some(TypeConv.AsString(f.Name)) else None); - var body :- Translator.TranslateExpression(fn.Body); - Success(Syntax.Exprs.Abs(inParams, body)) - } + function method AbsOfFunction(fn: C.Function) + : Result + reads * + { + var inParams := Lib.Seq.MapFilter(CSharpInterop.ListUtils.ToSeq(fn.Formals), (f: C.Formal) reads * => + if f.InParam then Some(TypeConv.AsString(f.Name)) else None); + var body :- Translator.TranslateExpression(fn.Body); + Success(Syntax.Exprs.Abs(inParams, body)) + } - function method TranslateBody(input: REPLInterop.UserInput) - : Result - reads * - { - if input is REPLInterop.MemberDeclInput then - var ei := input as REPLInterop.MemberDeclInput; - if ei.Decl is C.ConstantField then - var cf := ei.Decl as C.ConstantField; - Translator.TranslateExpression(cf.Rhs) - else if ei.Decl is C.Function then - AbsOfFunction(ei.Decl as C.Function) + function method TranslateBody(input: REPLInterop.UserInput) + : Result + reads * + { + if input is REPLInterop.MemberDeclInput then + var ei := input as REPLInterop.MemberDeclInput; + if ei.Decl is C.ConstantField then + var cf := ei.Decl as C.ConstantField; + Translator.TranslateExpression(cf.Rhs) + else if ei.Decl is C.Function then + AbsOfFunction(ei.Decl as C.Function) + else + Failure(Translator.UnsupportedMember(ei.Decl)) else - Failure(Translator.UnsupportedMember(ei.Decl)) - else - (input.Sealed(); - Lib.ControlFlow.Unreachable()) - } + (input.Sealed(); + Lib.ControlFlow.Unreachable()) + } - function method TranslateInput(input: REPLInterop.UserInput) - : REPLResult> - reads * - { - var fullName := TypeConv.AsString(input.FullName); - var shortName := TypeConv.AsString(input.ShortName); - var body :- TranslateBody(input).MapFailure(e => TranslationError(e)); - :- Need(Interp.SupportsInterp(body), Unsupported(body)); - Success(Named(fullName, shortName, body)) - } + function method TranslateInput(input: REPLInterop.UserInput) + : REPLResult> + reads * + { + var fullName := TypeConv.AsString(input.FullName); + var shortName := TypeConv.AsString(input.ShortName); + var body :- TranslateBody(input).MapFailure(e => TranslationError(e)); + :- Need(Interp.SupportsInterp(body), Unsupported(body)); + Success(Named(fullName, shortName, body)) + } - method ReadResolve() returns (r: REPLResult>>) - modifies this`counter - decreases * - { - var inputs :- Read(); + method ReadResolve() returns (r: REPLResult>>) + modifies this`counter + decreases * + { + var inputs :- Read(); - var tcRes: REPLInterop.ResolutionResult := inputs.Resolve(); - if tcRes is REPLInterop.ResolutionError { - var err := tcRes as REPLInterop.ResolutionError; - return Failure(ResolutionError(TypeConv.AsString(err.Message))); - } + var tcRes: REPLInterop.ResolutionResult := inputs.Resolve(); + if tcRes is REPLInterop.ResolutionError { + var err := tcRes as REPLInterop.ResolutionError; + return Failure(ResolutionError(TypeConv.AsString(err.Message))); + } - tcRes.Sealed(); - var newInputs := - var tp := tcRes as REPLInterop.TypecheckedProgram; - CSharpInterop.ListUtils.ToSeq(tp.NewInputs); - return Lib.Seq.MapResult(newInputs, TranslateInput); - } + tcRes.Sealed(); + var newInputs := + var tp := tcRes as REPLInterop.TypecheckedProgram; + CSharpInterop.ListUtils.ToSeq(tp.NewInputs); + return Lib.Seq.MapResult(newInputs, TranslateInput); + } - static const MAX_FUEL := 1024; - static const FRAME_SIZE := 1024 * 1024; + static const MAX_FUEL := 1024; + static const FRAME_SIZE := 1024 * 1024; - static method InterpExpr(e: Interp.Expr, env: Interp.Environment) - returns (r: REPLResult>) - requires env.fuel < MAX_FUEL - { - var stackSize := FRAME_SIZE * env.fuel; - var fn := (_: ()) => Interp.Eval(e, env, Interp.State.Empty).MapFailure(e => InterpError(e)); - r := REPLInterop.Utils.RunWithCustomStack(fn, (), stackSize as System.int32); - } + static method InterpExpr(e: Interp.Expr, env: Interp.Environment) + returns (r: REPLResult>) + requires env.fuel < MAX_FUEL + { + var stackSize := FRAME_SIZE * env.fuel; + var fn := (_: ()) => Interp.Eval(e, env, Interp.State.Empty).MapFailure(e => InterpError(e)); + r := REPLInterop.Utils.RunWithCustomStack(fn, (), stackSize as System.int32); + } - static method Eval(e: Interp.Expr, globals: Interp.Context) returns (r: REPLResult) - decreases * - { - var fuel: nat := 4; - while true - invariant fuel < MAX_FUEL + static method Eval(e: Interp.Expr, globals: Interp.Context) returns (r: REPLResult) decreases * { - var env := Interp.Environment(fuel := fuel, globals := globals); - var v := InterpExpr(e, env); - match v + var fuel: nat := 4; + while true + invariant fuel < MAX_FUEL + decreases * + { + var env := Interp.Environment(fuel := fuel, globals := globals); + var v := InterpExpr(e, env); + match v case Success(Return(val, _)) => return Success(val); case Failure(InterpError(OutOfFuel(_))) => @@ -277,49 +277,49 @@ class REPL { } case Failure(_) => return Failure(v.error); // Work around a translation bug + } } - } - method ReadEval() - returns (r: REPLResult>>) - modifies this`counter, this`globals - decreases * - { - var rds :- ReadResolve(); - - var idx := 0; - var outputs := []; - for idx := 0 to |rds| { - var Named(fullName, shortName, body) := rds[idx]; - var val :- Eval(body, globals); - globals := globals[fullName := val]; - outputs := outputs + [Named(fullName, shortName, val)]; - } + method ReadEval() + returns (r: REPLResult>>) + modifies this`counter, this`globals + decreases * + { + var rds :- ReadResolve(); + + var idx := 0; + var outputs := []; + for idx := 0 to |rds| { + var Named(fullName, shortName, body) := rds[idx]; + var val :- Eval(body, globals); + globals := globals[fullName := val]; + outputs := outputs + [Named(fullName, shortName, val)]; + } - return Success(outputs); + return Success(outputs); + } } -} -method Main() - decreases * -{ - REPLInterop.Utils.Initialize(); - var repl := new REPL(); - while true - decreases * { - var r := repl.ReadEval(); - match r { - case Failure(EOF()) => - return; - case Failure(err) => - print err.ToString(); - case Success(results) => - for idx := 0 to |results| { - var Named(_, shortName, val) := results[idx]; - print shortName, " := ", Semantics.Printer.ToString(val); - } + method Main() + decreases * + { + REPLInterop.Utils.Initialize(); + var repl := new REPL(); + while true + decreases * { + var r := repl.ReadEval(); + match r { + case Failure(EOF()) => + return; + case Failure(err) => + print err.ToString(); + case Success(results) => + for idx := 0 to |results| { + var Named(_, shortName, val) := results[idx]; + print shortName, " := ", Semantics.Printer.ToString(val); + } + } + print "\n"; } - print "\n"; } } -} diff --git a/src/Semantics/Equiv.dfy b/src/Semantics/Equiv.dfy index c2665a5f..f9f056f0 100644 --- a/src/Semantics/Equiv.dfy +++ b/src/Semantics/Equiv.dfy @@ -1,4 +1,4 @@ -include "../Interop/CSharpDafnyASTModel.dfy" + include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" @@ -45,8 +45,8 @@ module Bootstrap.Semantics.Equiv { // TODO: not sure it was worth making this opaque predicate {:opaque} GEqCtx( - eq_value: (WV,WV) -> bool, ctx: Context, ctx': Context - ) + eq_value: (WV,WV) -> bool, ctx: Context, ctx': Context + ) requires WellFormedContext(ctx) requires WellFormedContext(ctx') { @@ -55,7 +55,7 @@ module Bootstrap.Semantics.Equiv { } predicate GEqState( - eq_value: (WV,WV) -> bool, ctx: State, ctx': State) + eq_value: (WV,WV) -> bool, ctx: State, ctx': State) { GEqCtx(eq_value, ctx.locals, ctx'.locals) } @@ -66,7 +66,7 @@ module Bootstrap.Semantics.Equiv { } predicate GEqInterpResult( - eq_ctx: (State,State) -> bool, eq_value: (T,T) -> bool, res: InterpResult, res': InterpResult) + eq_ctx: (State,State) -> bool, eq_value: (T,T) -> bool, res: InterpResult, res': InterpResult) // Interpretation results are equivalent. // "G" stands for "generic". // @@ -213,31 +213,31 @@ module Bootstrap.Semantics.Equiv { var Closure(ctx', vars', body') := v'; && |vars| == |vars'| && ( - forall env: Environment, argvs: seq, argvs': seq | - && |argvs| == |argvs'| == |vars| // no partial applications are allowed in Dafny - // We need the argument types to be smaller than the closure types, to prove termination.\ - // In effect, the arguments types should be given by the closure's input types. - && (forall i | 0 <= i < |vars| :: ValueTypeHeight(argvs[i]) < ValueTypeHeight(v)) - && (forall i | 0 <= i < |vars| :: ValueTypeHeight(argvs'[i]) < ValueTypeHeight(v')) - && (forall i | 0 <= i < |vars| :: EqValue(argvs[i], argvs'[i])) :: - var res := InterpCallFunctionBody(v, env, argvs); - var res' := InterpCallFunctionBody(v', env, argvs'); - // We can't use naked functions in recursive setting: this forces us to write the expanded - // match rather than using an auxiliary function like `EqPureInterpResult`. - match (res, res') { - case (Success(ov), Success(ov')) => - // We need to assume those assertions to prove termination: the value returned by a closure - // has a type which is smaller than the closure type (its type is given by the closure return - // type) - assume ValueTypeHeight(ov) < ValueTypeHeight(v); - assume ValueTypeHeight(ov') < ValueTypeHeight(v'); - EqValue(ov, ov') - case (Failure(_), _) => - true - case _ => - false - } - ) + forall env: Environment, argvs: seq, argvs': seq | + && |argvs| == |argvs'| == |vars| // no partial applications are allowed in Dafny + // We need the argument types to be smaller than the closure types, to prove termination.\ + // In effect, the arguments types should be given by the closure's input types. + && (forall i | 0 <= i < |vars| :: ValueTypeHeight(argvs[i]) < ValueTypeHeight(v)) + && (forall i | 0 <= i < |vars| :: ValueTypeHeight(argvs'[i]) < ValueTypeHeight(v')) + && (forall i | 0 <= i < |vars| :: EqValue(argvs[i], argvs'[i])) :: + var res := InterpCallFunctionBody(v, env, argvs); + var res' := InterpCallFunctionBody(v', env, argvs'); + // We can't use naked functions in recursive setting: this forces us to write the expanded + // match rather than using an auxiliary function like `EqPureInterpResult`. + match (res, res') { + case (Success(ov), Success(ov')) => + // We need to assume those assertions to prove termination: the value returned by a closure + // has a type which is smaller than the closure type (its type is given by the closure return + // type) + assume ValueTypeHeight(ov) < ValueTypeHeight(v); + assume ValueTypeHeight(ov') < ValueTypeHeight(v'); + EqValue(ov, ov') + case (Failure(_), _) => + true + case _ => + false + } + ) } lemma EqValue_Closure_EqInterp_FunctionCall(f: WV, f': WV, argvs: seq, argvs': seq, env: Environment) @@ -267,7 +267,7 @@ module Bootstrap.Semantics.Equiv { } predicate EqInterpResult( - eq_value: (T,T) -> bool, res: InterpResult, res': InterpResult) + eq_value: (T,T) -> bool, res: InterpResult, res': InterpResult) { GEqInterpResult(Mk_EqState(EqValue), eq_value, res, res') } @@ -371,28 +371,28 @@ module Bootstrap.Semantics.Equiv { var res' := InterpCallFunctionBody(v, env, argvs'); EqPureInterpResultValue(res, res') { - var res := InterpCallFunctionBody(v, env, argvs); - var res' := InterpCallFunctionBody(v, env, argvs'); - - assert EqCtx(ctx, ctx) by { - // It would be difficult to call a lemma like ``EqState_Refl`` here, because - // of termination issues. However, we have that the values in the closure context - // are smaller than the closure value itself, which allows us to recursively call - // ``EqValue``. - forall x | x in ctx ensures EqValue(ctx[x], ctx[x]) { - EqValue_Refl(ctx[x]); - } - reveal GEqCtx(); + var res := InterpCallFunctionBody(v, env, argvs); + var res' := InterpCallFunctionBody(v, env, argvs'); + + assert EqCtx(ctx, ctx) by { + // It would be difficult to call a lemma like ``EqState_Refl`` here, because + // of termination issues. However, we have that the values in the closure context + // are smaller than the closure value itself, which allows us to recursively call + // ``EqValue``. + forall x | x in ctx ensures EqValue(ctx[x], ctx[x]) { + EqValue_Refl(ctx[x]); } + reveal GEqCtx(); + } - var ctx1 := BuildCallState(ctx, vars, argvs); - var ctx1' := BuildCallState(ctx, vars, argvs'); - BuildCallState_EqState(ctx, ctx, vars, argvs, argvs'); - assert EqState(ctx1, ctx1'); + var ctx1 := BuildCallState(ctx, vars, argvs); + var ctx1' := BuildCallState(ctx, vars, argvs'); + BuildCallState_EqState(ctx, ctx, vars, argvs, argvs'); + assert EqState(ctx1, ctx1'); - reveal InterpCallFunctionBody(); - EqInterp_Expr_EqState(body, env, ctx1, ctx1'); - assert EqPureInterpResultValue(res, res'); + reveal InterpCallFunctionBody(); + EqInterp_Expr_EqState(body, env, ctx1, ctx1'); + assert EqPureInterpResultValue(res, res'); } reveal EqValue_Closure(); } @@ -460,38 +460,38 @@ module Bootstrap.Semantics.Equiv { var res2 := InterpCallFunctionBody(v2, env, argvs2); EqPureInterpResultValue(res0, res2) { - var res0 := InterpCallFunctionBody(v0, env, argvs0); - var res2 := InterpCallFunctionBody(v2, env, argvs2); - - // Termination issue: we need to assume that the arguments' types have the - // proper height. In practice, if the program is properly type checked, we - // have: - // - `TypeOf(v0) == TypeOf(v1) == TypeOf(v2)` - // - `forall i, TypeOf(argvs0[i]) == TypeOf(argvs2[i])1 - // so the assumption is trivially true. - assume (forall i | 0 <= i < |vars0| :: ValueTypeHeight(argvs0[i]) < ValueTypeHeight(v1)); - - forall i | 0 <= i < |vars0| ensures EqValue(argvs0[i], argvs0[i]) { - EqValue_Refl(argvs0[i]); - } + var res0 := InterpCallFunctionBody(v0, env, argvs0); + var res2 := InterpCallFunctionBody(v2, env, argvs2); + + // Termination issue: we need to assume that the arguments' types have the + // proper height. In practice, if the program is properly type checked, we + // have: + // - `TypeOf(v0) == TypeOf(v1) == TypeOf(v2)` + // - `forall i, TypeOf(argvs0[i]) == TypeOf(argvs2[i])1 + // so the assumption is trivially true. + assume (forall i | 0 <= i < |vars0| :: ValueTypeHeight(argvs0[i]) < ValueTypeHeight(v1)); + + forall i | 0 <= i < |vars0| ensures EqValue(argvs0[i], argvs0[i]) { + EqValue_Refl(argvs0[i]); + } - var res1 := InterpCallFunctionBody(v1, env, argvs0); - if res0.Success? { - var ov0 := res0.value; - var ov1 := res1.value; - var ov2 := res2.value; + var res1 := InterpCallFunctionBody(v1, env, argvs0); + if res0.Success? { + var ov0 := res0.value; + var ov1 := res1.value; + var ov2 := res2.value; - // Termination - same as above: if the program is well-typed, this is - // trivially true. - assume ValueTypeHeight(ov0) < ValueTypeHeight(v0); + // Termination - same as above: if the program is well-typed, this is + // trivially true. + assume ValueTypeHeight(ov0) < ValueTypeHeight(v0); - EqValue_Trans(ov0, ov1, ov2); + EqValue_Trans(ov0, ov1, ov2); - assert EqPureInterpResultValue(res0, res2); - } - else { - // Trivial - } + assert EqPureInterpResultValue(res0, res2); + } + else { + // Trivial + } } } @@ -521,8 +521,8 @@ module Bootstrap.Semantics.Equiv { lemma EqValue_HasEqValue_Eq_Forall() ensures forall v:WV, v':WV | EqValue(v, v') :: - && (HasEqValue(v) == HasEqValue(v')) - && (HasEqValue(v) ==> v == v') + && (HasEqValue(v) == HasEqValue(v')) + && (HasEqValue(v) ==> v == v') // This is one of the important lemmas for the proofs of equivalence. // The reason is that the interpreter often checks that some values // have a decidable equality (for instance, before inserting a value in @@ -534,9 +534,9 @@ module Bootstrap.Semantics.Equiv { { forall v:WV, v':WV | EqValue(v, v') ensures - && (HasEqValue(v) == HasEqValue(v')) - && (HasEqValue(v) ==> v == v') { - EqValue_HasEqValue_Eq(v, v'); + && (HasEqValue(v) == HasEqValue(v')) + && (HasEqValue(v) ==> v == v') { + EqValue_HasEqValue_Eq(v, v'); } } @@ -687,11 +687,11 @@ module Bootstrap.Semantics.Equiv { // This is the important, generic equivalence relation over expressions. { SupportsInterp(e) ==> - (&& SupportsInterp(e') - && forall env, ctx, ctx' | eq.eq_state(ctx, ctx') :: - GEqInterpResult(eq.eq_state, eq.eq_value, - InterpExpr(e, env, ctx), - InterpExpr(e', env, ctx'))) + (&& SupportsInterp(e') + && forall env, ctx, ctx' | eq.eq_state(ctx, ctx') :: + GEqInterpResult(eq.eq_state, eq.eq_value, + InterpExpr(e, env, ctx), + InterpExpr(e', env, ctx'))) } function Mk_EqInterp(eq: Equivs): (Expr, Expr) -> bool { @@ -709,11 +709,11 @@ module Bootstrap.Semantics.Equiv { predicate EqInterpBlockExprs(es: seq, es': seq) { Seq_All(SupportsInterp, es) ==> - (&& Seq_All(SupportsInterp, es') - && forall env, ctx, ctx' | EqState(ctx, ctx') :: - EqInterpResultValue( - InterpBlock_Exprs(es, env, ctx), - InterpBlock_Exprs(es', env, ctx'))) + (&& Seq_All(SupportsInterp, es') + && forall env, ctx, ctx' | EqState(ctx, ctx') :: + EqInterpResultValue( + InterpBlock_Exprs(es, env, ctx), + InterpBlock_Exprs(es', env, ctx'))) } lemma EqInterp_Refl(e: Exprs.T) @@ -723,8 +723,8 @@ module Bootstrap.Semantics.Equiv { forall env, ctx, ctx' | EqState(ctx, ctx') ensures EqInterpResultValue( - InterpExpr(e, env, ctx), - InterpExpr(e, env, ctx')) + InterpExpr(e, env, ctx), + InterpExpr(e, env, ctx')) { EqInterp_Expr_EqState(e, env, ctx, ctx'); } @@ -825,7 +825,7 @@ module Bootstrap.Semantics.Equiv { reveal InterpBlock_Exprs(); if es == [] {} else { - // Evaluate the first expression + // Evaluate the first expression var res0 := InterpExprWithType(es[0], Types.Unit, env, ctx); var res0' := InterpExprWithType(es[0], Types.Unit, env, ctx'); EqInterp_Refl(es[0]); @@ -850,22 +850,22 @@ module Bootstrap.Semantics.Equiv { requires EqState(ctx, ctx') ensures SupportsInterp(e') ensures EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) - // We use this lemma because sometimes quantifiers are are not triggered. + // We use this lemma because sometimes quantifiers are are not triggered. {} lemma InterpExprs_GEqInterp_Inst( - eq: Equivs, es: seq, es': seq, env: Environment, ctx: State, ctx': State) + eq: Equivs, es: seq, es': seq, env: Environment, ctx: State, ctx': State) requires forall e | e in es :: SupportsInterp(e) requires All_Rel_Forall(Mk_EqInterp(eq), es, es') requires eq.eq_state(ctx, ctx') ensures forall e | e in es' :: SupportsInterp(e) ensures GEqInterpResultSeq(eq, InterpExprs(es, env, ctx), InterpExprs(es', env, ctx')) - // Auxiliary lemma: if two sequences contain equivalent expressions, evaluating those two - // sequences in equivalent contexts leads to equivalent results. - // This lemma is written generically over the equivalence relations over the states and - // values. We don't do this because it seems elegant: we do this as a desperate attempt - // to reduce the context size, while we are unable to use the `opaque` attribute on - // some definitions (``EqValue`` in particular). + // Auxiliary lemma: if two sequences contain equivalent expressions, evaluating those two + // sequences in equivalent contexts leads to equivalent results. + // This lemma is written generically over the equivalence relations over the states and + // values. We don't do this because it seems elegant: we do this as a desperate attempt + // to reduce the context size, while we are unable to use the `opaque` attribute on + // some definitions (``EqValue`` in particular). { reveal InterpExprs(); @@ -918,8 +918,8 @@ module Bootstrap.Semantics.Equiv { requires EqState(ctx, ctx') ensures forall e | e in es' :: SupportsInterp(e) ensures EqInterpResultSeqValue(InterpExprs(es, env, ctx), InterpExprs(es', env, ctx')) - // Auxiliary lemma: if two sequences contain equivalent expressions, evaluating those two - // sequences in equivalent contexts leads to equivalent results. + // Auxiliary lemma: if two sequences contain equivalent expressions, evaluating those two + // sequences in equivalent contexts leads to equivalent results. { InterpExprs_GEqInterp_Inst(EQ(EqValue, EqState), es, es', env, ctx, ctx'); } @@ -1011,7 +1011,7 @@ module Bootstrap.Semantics.Equiv { // (SMH) I don't understand why I need to use vcs_split_on_every_assert on this one. // For some strange reason it takes ~20s to verify with this, and timeouts without. lemma {:vcs_split_on_every_assert} - MapOfPairs_SeqZip_EqCtx(vars: seq, argvs: seq, argvs': seq) + MapOfPairs_SeqZip_EqCtx(vars: seq, argvs: seq, argvs': seq) requires |argvs| == |argvs'| == |vars| requires (forall i | 0 <= i < |vars| :: EqValue(argvs[i], argvs'[i])) ensures diff --git a/src/Semantics/Interp.dfy b/src/Semantics/Interp.dfy index f1c59bf6..a96c08e1 100644 --- a/src/Semantics/Interp.dfy +++ b/src/Semantics/Interp.dfy @@ -1,4 +1,4 @@ -include "../Utils/Library.dfy" + include "../Utils/Library.dfy" include "../AST/Syntax.dfy" include "../AST/Predicates.dfy" include "Values.dfy" @@ -49,17 +49,17 @@ module Bootstrap.Semantics.Interp { // TODO: rewrite as a shallow predicate applied through ``v.All``? predicate method WellFormedEqValue(v: V.T) - // This predicate gives the constrainst we need to be able to *define* our equivalence relation - // over values and actually *use* this relation to prove equivalence properties between expressions. - // - // The difficult point is linked to closures: when we apply transformations to the code, we often - // apply them in a deep manner to the expressions (i.e., to all the subexpressions of an expression). - // The problem is that it can have an effect on the closure values generated through the execution - // by modifying their bodies, leading to discrepancies in the execution of the code (imagine the case - // where we use closures as keys inside of maps). - // The good news is that when those cases happen, we actually try to use an equality over values - // which don't have a decidable equality: we solve the problem by forcing some subvalues to have - // a decidable equality. + // This predicate gives the constrainst we need to be able to *define* our equivalence relation + // over values and actually *use* this relation to prove equivalence properties between expressions. + // + // The difficult point is linked to closures: when we apply transformations to the code, we often + // apply them in a deep manner to the expressions (i.e., to all the subexpressions of an expression). + // The problem is that it can have an effect on the closure values generated through the execution + // by modifying their bodies, leading to discrepancies in the execution of the code (imagine the case + // where we use closures as keys inside of maps). + // The good news is that when those cases happen, we actually try to use an equality over values + // which don't have a decidable equality: we solve the problem by forcing some subvalues to have + // a decidable equality. { match v { case Unit => true @@ -89,11 +89,11 @@ module Bootstrap.Semantics.Interp { // TODO: rename to ValueHasEq predicate method HasEqValue(v: V.T) - // Return true if the value supports a decidale equality. - // - // Note that this is a bit subtle for collections: any empty collection supports a decidable - // equality, but non-empty collections support a decidable equality only if their elements - // support one. + // Return true if the value supports a decidale equality. + // + // Note that this is a bit subtle for collections: any empty collection supports a decidable + // equality, but non-empty collections support a decidable equality only if their elements + // support one. { match v { case Unit => true @@ -116,10 +116,10 @@ module Bootstrap.Semantics.Interp { } predicate method WellFormedValue1(v: V.T) - // The *shallow* well-formedness predicate for values manipulated by the interpreter. + // The *shallow* well-formedness predicate for values manipulated by the interpreter. { && v.Closure? ==> SupportsInterp(v.body) - && v.WellFormed1() + && v.WellFormed1() } predicate method WellFormedValue(v: V.T) { @@ -191,15 +191,15 @@ module Bootstrap.Semantics.Interp { { function method ToString() : string { match this // TODO include values in messages - case OutOfFuel(fn) => "Too many function evaluations" - case TypeError(e, value, expected) => "Type mismatch" - case Invalid(e) => "Invalid expression" - case OutOfIntBounds(x, low, high) => "Out-of-bounds value" - case OutOfSeqBounds(v, i) => "Index out of sequence bounds" - case OutOfMapDomain(v, i) => "Missing key in map" - case UnboundVariable(v) => "Unbound variable '" + v + "'" - case SignatureMismatch(vars, argvs) => "Wrong number of arguments in function call" - case DivisionByZero() => "Division by zero" + case OutOfFuel(fn) => "Too many function evaluations" + case TypeError(e, value, expected) => "Type mismatch" + case Invalid(e) => "Invalid expression" + case OutOfIntBounds(x, low, high) => "Out-of-bounds value" + case OutOfSeqBounds(v, i) => "Index out of sequence bounds" + case OutOfMapDomain(v, i) => "Missing key in map" + case UnboundVariable(v) => "Unbound variable '" + v + "'" + case SignatureMismatch(vars, argvs) => "Wrong number of arguments in function call" + case DivisionByZero() => "Division by zero" } } @@ -242,18 +242,18 @@ module Bootstrap.Semantics.Interp { case Apply(Eager(op), args: seq) => var Return(argvs, ctx) :- InterpExprs(args, env, ctx); LiftPureResult(ctx, match op { - case UnaryOp(op: UnaryOp) => - InterpUnaryOp(e, op, argvs[0]) - case BinaryOp(bop: BinaryOp) => - assert !bop.BV? && !bop.Datatypes?; - InterpBinaryOp(e, bop, argvs[0], argvs[1]) - case TernaryOp(top: TernaryOp) => - InterpTernaryOp(e, top, argvs[0], argvs[1], argvs[2]) - case Builtin(Display(ty)) => - InterpDisplay(e, ty.kind, argvs) - case FunctionCall() => - InterpFunctionCall(e, env, argvs[0], argvs[1..]) - }) + case UnaryOp(op: UnaryOp) => + InterpUnaryOp(e, op, argvs[0]) + case BinaryOp(bop: BinaryOp) => + assert !bop.BV? && !bop.Datatypes?; + InterpBinaryOp(e, bop, argvs[0], argvs[1]) + case TernaryOp(top: TernaryOp) => + InterpTernaryOp(e, top, argvs[0], argvs[1], argvs[2]) + case Builtin(Display(ty)) => + InterpDisplay(e, ty.kind, argvs) + case FunctionCall() => + InterpFunctionCall(e, env, argvs[0], argvs[1..]) + }) case Bind(vars, exprs: seq, body: Expr) => var Return(vals, ctx) :- InterpExprs(exprs, env, ctx); InterpBind(e, env, ctx, vars, vals, body) @@ -269,8 +269,8 @@ module Bootstrap.Semantics.Interp { : PureInterpResult { match TryGetVariable(ctx.locals, v, UnboundVariable(v)) - case Success(val) => Success(val) - case Failure(err) => TryGetVariable(env.globals, v, err) + case Success(val) => Success(val) + case Failure(err) => TryGetVariable(env.globals, v, err) } function method {:opaque} TryGetVariable(ctx: Context, k: string, err: InterpError) @@ -315,7 +315,7 @@ module Bootstrap.Semantics.Interp { reveal SupportsInterp(); var Return(val, ctx) :- InterpExpr(e, env, ctx); :- Need(val.HasType(ty), TypeError(e, val, ty)); - Success(Return(val, ctx)) + Success(Return(val, ctx)) } function method NeedType(e: Expr, val: Value, ty: Type) @@ -339,13 +339,13 @@ module Bootstrap.Semantics.Interp { // DISCUSS: No `:-` for outcomes? // DISCUSS: should match accept multiple discriminands? (with lazy evaluation?) match NeedType(es[0], vs[0], ty) - case Pass => - assert vs[0].HasType(ty); - match NeedTypes(es[1..], vs[1..], ty) { // TODO check that compiler does this efficiently - case Pass => assert forall v | v in vs[1..] :: v.HasType(ty); Pass - case fail => fail - } - case fail => fail + case Pass => + assert vs[0].HasType(ty); + match NeedTypes(es[1..], vs[1..], ty) { // TODO check that compiler does this efficiently + case Pass => assert forall v | v in vs[1..] :: v.HasType(ty); Pass + case fail => fail + } + case fail => fail } function method {:opaque} InterpExprs(es: seq, env: Environment, ctx: State) @@ -365,16 +365,16 @@ module Bootstrap.Semantics.Interp { ensures HasEqValue(v) { match a - case LitUnit => V.Unit - case LitBool(b: bool) => V.Bool(b) - case LitInt(i: int) => V.Int(i) - case LitReal(r: real) => V.Real(r) - case LitChar(c: char) => V.Char(c) - case LitString(s: string, verbatim: bool) => - var chars := seq(|s|, i requires 0 <= i < |s| => V.Char(s[i])); - assert forall c | c in chars :: WellFormedValue(c); - assert forall c | c in chars :: HasEqValue(c); - V.Seq(chars) + case LitUnit => V.Unit + case LitBool(b: bool) => V.Bool(b) + case LitInt(i: int) => V.Int(i) + case LitReal(r: real) => V.Real(r) + case LitChar(c: char) => V.Char(c) + case LitString(s: string, verbatim: bool) => + var chars := seq(|s|, i requires 0 <= i < |s| => V.Char(s[i])); + assert forall c | c in chars :: WellFormedValue(c); + assert forall c | c in chars :: HasEqValue(c); + V.Seq(chars) } function method {:opaque} InterpLazy(e: Expr, env: Environment, ctx: State) @@ -387,12 +387,12 @@ module Bootstrap.Semantics.Interp { var op, e0, e1 := e.aop.lOp, e.args[0], e.args[1]; var Return(v0, ctx0) :- InterpExprWithType(e0, Type.Bool, env, ctx); match (op, v0) - case (And, Bool(false)) => Success(Return(V.Bool(false), ctx0)) - case (Or, Bool(true)) => Success(Return(V.Bool(true), ctx0)) - case (Imp, Bool(false)) => Success(Return(V.Bool(true), ctx0)) - case (_, Bool(b)) => - assert op in {Exprs.And, Exprs.Or, Exprs.Imp}; - InterpExprWithType(e1, Type.Bool, env, ctx0) + case (And, Bool(false)) => Success(Return(V.Bool(false), ctx0)) + case (Or, Bool(true)) => Success(Return(V.Bool(true), ctx0)) + case (Imp, Bool(false)) => Success(Return(V.Bool(true), ctx0)) + case (_, Bool(b)) => + assert op in {Exprs.And, Exprs.Or, Exprs.Imp}; + InterpExprWithType(e1, Type.Bool, env, ctx0) } // Alternate implementation of ``InterpLazy``: less efficient but more closely @@ -408,12 +408,12 @@ module Bootstrap.Semantics.Interp { var Return(v0, ctx0) :- InterpExprWithType(e0, Type.Bool, env, ctx); var Return(v1, ctx1) :- InterpExprWithType(e1, Type.Bool, env, ctx0); match (op, v0, v1) - case (And, Bool(b0), Bool(b1)) => - Success(Return(V.Bool(b0 && b1), if b0 then ctx1 else ctx0)) - case (Or, Bool(b0), Bool(b1)) => - Success(Return(V.Bool(b0 || b1), if b0 then ctx0 else ctx1)) - case (Imp, Bool(b0), Bool(b1)) => - Success(Return(V.Bool(b0 ==> b1), if b0 then ctx1 else ctx0)) + case (And, Bool(b0), Bool(b1)) => + Success(Return(V.Bool(b0 && b1), if b0 then ctx1 else ctx0)) + case (Or, Bool(b0), Bool(b1)) => + Success(Return(V.Bool(b0 || b1), if b0 then ctx0 else ctx1)) + case (Imp, Bool(b0), Bool(b1)) => + Success(Return(V.Bool(b0 ==> b1), if b0 then ctx1 else ctx0)) } lemma InterpLazy_Complete(e: Expr, env: Environment, ctx: State) @@ -441,18 +441,18 @@ module Bootstrap.Semantics.Interp { requires !op.MemberSelect? { match op - case BVNot => :- Need(v0.BitVector?, Invalid(expr)); - Success(V.BitVector(v0.width, Math.IntPow(2, v0.width) - 1 - v0.value)) - case BoolNot => :- Need(v0.Bool?, Invalid(expr)); - Success(V.Bool(!v0.b)) - case SeqLength => :- Need(v0.Seq?, Invalid(expr)); - Success(V.Int(|v0.sq|)) - case SetCard => :- Need(v0.Set?, Invalid(expr)); - Success(V.Int(|v0.st|)) - case MultisetCard => :- Need(v0.Multiset?, Invalid(expr)); - Success(V.Int(|v0.ms|)) - case MapCard => :- Need(v0.Map?, Invalid(expr)); - Success(V.Int(|v0.m|)) + case BVNot => :- Need(v0.BitVector?, Invalid(expr)); + Success(V.BitVector(v0.width, Math.IntPow(2, v0.width) - 1 - v0.value)) + case BoolNot => :- Need(v0.Bool?, Invalid(expr)); + Success(V.Bool(!v0.b)) + case SeqLength => :- Need(v0.Seq?, Invalid(expr)); + Success(V.Int(|v0.sq|)) + case SetCard => :- Need(v0.Set?, Invalid(expr)); + Success(V.Int(|v0.st|)) + case MultisetCard => :- Need(v0.Multiset?, Invalid(expr)); + Success(V.Int(|v0.ms|)) + case MapCard => :- Need(v0.Map?, Invalid(expr)); + Success(V.Int(|v0.m|)) } function method {:opaque} InterpBinaryOp(expr: Expr, bop: Syntax.BinaryOp, v0: Value, v1: Value) @@ -460,22 +460,22 @@ module Bootstrap.Semantics.Interp { requires !bop.BV? && !bop.Datatypes? { match bop - case Numeric(op) => InterpBinaryNumeric(expr, op, v0, v1) - case Logical(op) => InterpBinaryLogical(expr, op, v0, v1) - case Eq(op) => // FIXME which types is this Eq applicable to (vs. the type-specific ones?) - :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); - match op { - case EqCommon() => Success(V.Bool(v0 == v1)) - case NeqCommon() => Success(V.Bool(v0 != v1)) - } - // case BV(op) => - case Char(op) => InterpBinaryChar(expr, op, v0, v1) - case Sets(op) => InterpBinarySets(expr, op, v0, v1) - case Multisets(op) => InterpBinaryMultisets(expr, op, v0, v1) - case Sequences(op) => InterpBinarySequences(expr, op, v0, v1) - case Maps(op) => InterpBinaryMaps(expr, op, v0, v1) - // case Datatypes(op) => + case Numeric(op) => InterpBinaryNumeric(expr, op, v0, v1) + case Logical(op) => InterpBinaryLogical(expr, op, v0, v1) + case Eq(op) => // FIXME which types is this Eq applicable to (vs. the type-specific ones?) + :- Need(HasEqValue(v0), Invalid(expr)); + :- Need(HasEqValue(v1), Invalid(expr)); + match op { + case EqCommon() => Success(V.Bool(v0 == v1)) + case NeqCommon() => Success(V.Bool(v0 != v1)) + } + // case BV(op) => + case Char(op) => InterpBinaryChar(expr, op, v0, v1) + case Sets(op) => InterpBinarySets(expr, op, v0, v1) + case Multisets(op) => InterpBinaryMultisets(expr, op, v0, v1) + case Sequences(op) => InterpBinarySequences(expr, op, v0, v1) + case Maps(op) => InterpBinaryMaps(expr, op, v0, v1) + // case Datatypes(op) => } function method InterpBinaryNumeric(expr: Expr, op: Exprs.BinaryOps.Numeric, v0: Value, v1: Value) @@ -512,7 +512,7 @@ module Bootstrap.Semantics.Interp { function method NeedIntBounds(x: int, low: int, high: int) : PureInterpResult { :- Need(low <= x < high, OutOfIntBounds(x, Some(low), Some(high))); - Success(x) + Success(x) } function method InterpBinaryNumericChar(expr: Expr, bop: Syntax.BinaryOps.Numeric, x1: char, x2: char) @@ -551,24 +551,24 @@ module Bootstrap.Semantics.Interp { : PureInterpResult { :- Need(v0.Bool? && v1.Bool?, Invalid(expr)); - match op - case Iff() => - Success(V.Bool(v0.b <==> v1.b)) + match op + case Iff() => + Success(V.Bool(v0.b <==> v1.b)) } function method InterpBinaryChar(expr: Expr, op: Syntax.BinaryOps.Char, v0: Value, v1: Value) : PureInterpResult { // FIXME eliminate distinction between GtChar and GT? :- Need(v0.Char? && v1.Char?, Invalid(expr)); - match op - case LtChar() => - Success(V.Bool(v0.c < v1.c)) - case LeChar() => - Success(V.Bool(v0.c <= v1.c)) - case GeChar() => - Success(V.Bool(v0.c >= v1.c)) - case GtChar() => - Success(V.Bool(v0.c > v1.c)) + match op + case LtChar() => + Success(V.Bool(v0.c < v1.c)) + case LeChar() => + Success(V.Bool(v0.c <= v1.c)) + case GeChar() => + Success(V.Bool(v0.c >= v1.c)) + case GtChar() => + Success(V.Bool(v0.c > v1.c)) } function method InterpBinarySets(expr: Expr, op: Exprs.BinaryOps.Sets, v0: Value, v1: Value) @@ -577,34 +577,34 @@ module Bootstrap.Semantics.Interp { // Rk.: we enforce through `WellFormedEqValue` that sets contain values with a decidable // equality. match op - case SetEq() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st == v1.st)) - case SetNeq() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st != v1.st)) - case Subset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st <= v1.st)) - case Superset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st >= v1.st)) - case ProperSubset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st < v1.st)) - case ProperSuperset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st > v1.st)) - case Disjoint() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st !! v1.st)) - case Union() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Set(v0.st + v1.st)) - case Intersection() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Set(v0.st * v1.st)) - case SetDifference() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Set(v0.st - v1.st)) - case InSet() => - :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Set?, Invalid(expr)); - Success(V.Bool(v0 in v1.st)) - case NotInSet() => - :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Set?, Invalid(expr)); - Success(V.Bool(v0 !in v1.st)) + case SetEq() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Bool(v0.st == v1.st)) + case SetNeq() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Bool(v0.st != v1.st)) + case Subset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Bool(v0.st <= v1.st)) + case Superset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Bool(v0.st >= v1.st)) + case ProperSubset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Bool(v0.st < v1.st)) + case ProperSuperset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Bool(v0.st > v1.st)) + case Disjoint() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Bool(v0.st !! v1.st)) + case Union() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Set(v0.st + v1.st)) + case Intersection() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Set(v0.st * v1.st)) + case SetDifference() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); + Success(V.Set(v0.st - v1.st)) + case InSet() => + :- Need(HasEqValue(v0), Invalid(expr)); + :- Need(v1.Set?, Invalid(expr)); + Success(V.Bool(v0 in v1.st)) + case NotInSet() => + :- Need(HasEqValue(v0), Invalid(expr)); + :- Need(v1.Set?, Invalid(expr)); + Success(V.Bool(v0 !in v1.st)) } function method InterpBinaryMultisets(expr: Expr, op: Exprs.BinaryOps.Multisets, v0: Value, v1: Value) @@ -613,38 +613,38 @@ module Bootstrap.Semantics.Interp { // Rk.: we enforce through `WellFormedEqValue` that multisets contain values with a decidable // equality. match op // DISCUSS - case MultisetEq() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms == v1.ms)) - case MultisetNeq() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms != v1.ms)) - case MultiSubset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms <= v1.ms)) - case MultiSuperset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms >= v1.ms)) - case ProperMultiSubset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms < v1.ms)) - case ProperMultiSuperset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms > v1.ms)) - case MultisetDisjoint() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms !! v1.ms)) - case MultisetUnion() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Multiset(v0.ms + v1.ms)) - case MultisetIntersection() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Multiset(v0.ms * v1.ms)) - case MultisetDifference() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Multiset(v0.ms - v1.ms)) - case InMultiset() => - :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0 in v1.ms)) - case NotInMultiset() => - :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0 !in v1.ms)) - case MultisetSelect() => - :- Need(HasEqValue(v1), Invalid(expr)); - :- Need(v0.Multiset?, Invalid(expr)); - Success(V.Int(v0.ms[v1])) + case MultisetEq() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0.ms == v1.ms)) + case MultisetNeq() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0.ms != v1.ms)) + case MultiSubset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0.ms <= v1.ms)) + case MultiSuperset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0.ms >= v1.ms)) + case ProperMultiSubset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0.ms < v1.ms)) + case ProperMultiSuperset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0.ms > v1.ms)) + case MultisetDisjoint() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0.ms !! v1.ms)) + case MultisetUnion() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Multiset(v0.ms + v1.ms)) + case MultisetIntersection() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Multiset(v0.ms * v1.ms)) + case MultisetDifference() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); + Success(V.Multiset(v0.ms - v1.ms)) + case InMultiset() => + :- Need(HasEqValue(v0), Invalid(expr)); + :- Need(v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0 in v1.ms)) + case NotInMultiset() => + :- Need(HasEqValue(v0), Invalid(expr)); + :- Need(v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0 !in v1.ms)) + case MultisetSelect() => + :- Need(HasEqValue(v1), Invalid(expr)); + :- Need(v0.Multiset?, Invalid(expr)); + Success(V.Int(v0.ms[v1])) } function method InterpBinarySequences(expr: Expr, op: Exprs.BinaryOps.Sequences, v0: Value, v1: Value) @@ -656,47 +656,47 @@ module Bootstrap.Semantics.Interp { // TODO: the dynamic checks for decidable equality may make the interpreter quite // slow. We might want to deduce this from a type check instead. match op - case SeqEq() => - :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq == v1.sq)) - case SeqNeq() => - :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq != v1.sq)) - case Prefix() => - :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq <= v1.sq)) - case ProperPrefix() => - :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq < v1.sq)) - case Concat() => :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - Success(V.Seq(v0.sq + v1.sq)) - case InSeq() => - :- Need(v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 in v1.sq)) - case NotInSeq() => - :- Need(v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 !in v1.sq)) - case SeqDrop() => - :- NeedValidEndpoint(expr, v0, v1); - Success(V.Seq(v0.sq[v1.i..])) - case SeqTake() => - :- NeedValidEndpoint(expr, v0, v1); - Success(V.Seq(v0.sq[..v1.i])) - case SeqSelect() => - :- NeedValidIndex(expr, v0, v1); - Success(v0.sq[v1.i]) + case SeqEq() => + :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq == v1.sq)) + case SeqNeq() => + :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq != v1.sq)) + case Prefix() => + :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq <= v1.sq)) + case ProperPrefix() => + :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq < v1.sq)) + case Concat() => :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); + Success(V.Seq(v0.sq + v1.sq)) + case InSeq() => + :- Need(v1.Seq?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 in v1.sq)) + case NotInSeq() => + :- Need(v1.Seq?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 !in v1.sq)) + case SeqDrop() => + :- NeedValidEndpoint(expr, v0, v1); + Success(V.Seq(v0.sq[v1.i..])) + case SeqTake() => + :- NeedValidEndpoint(expr, v0, v1); + Success(V.Seq(v0.sq[..v1.i])) + case SeqSelect() => + :- NeedValidIndex(expr, v0, v1); + Success(v0.sq[v1.i]) } function method InterpBinaryMaps(expr: Expr, op: Exprs.BinaryOps.Maps, v0: Value, v1: Value) @@ -705,117 +705,117 @@ module Bootstrap.Semantics.Interp { // Rk.: values in maps don't necessarily have a decidable equality. We thus perform // dynamic checks when we need one and fail if it is not the case. match op - case MapEq() => - :- Need(v0.Map? && v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.m == v1.m)) - case MapNeq() => - :- Need(v0.Map? && v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.m != v1.m)) - case MapMerge() => - :- Need(v0.Map? && v1.Map?, Invalid(expr)); - Success(V.Map(v0.m + v1.m)) - case MapSubtraction() => - :- Need(v0.Map? && v1.Set?, Invalid(expr)); - Success(V.Map(v0.m - v1.st)) - case InMap() => - :- Need(v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 in v1.m)) - case NotInMap() => - :- Need(v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 !in v1.m)) - case MapSelect() => - :- Need(v0.Map?, Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - :- Need(v1 in v0.m, OutOfMapDomain(v0, v1)); - Success(v0.m[v1]) + case MapEq() => + :- Need(v0.Map? && v1.Map?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.m == v1.m)) + case MapNeq() => + :- Need(v0.Map? && v1.Map?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.m != v1.m)) + case MapMerge() => + :- Need(v0.Map? && v1.Map?, Invalid(expr)); + Success(V.Map(v0.m + v1.m)) + case MapSubtraction() => + :- Need(v0.Map? && v1.Set?, Invalid(expr)); + Success(V.Map(v0.m - v1.st)) + case InMap() => + :- Need(v1.Map?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 in v1.m)) + case NotInMap() => + :- Need(v1.Map?, Invalid(expr)); + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 !in v1.m)) + case MapSelect() => + :- Need(v0.Map?, Invalid(expr)); + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + :- Need(v1 in v0.m, OutOfMapDomain(v0, v1)); + Success(v0.m[v1]) } function method {:opaque} InterpTernaryOp(expr: Expr, top: Syntax.TernaryOp, v0: Value, v1: Value, v2: Value) : PureInterpResult { match top - case Sequences(op) => - InterpTernarySequences(expr, op, v0, v1, v2) - case Multisets(op) => - InterpTernaryMultisets(expr, op, v0, v1, v2) - case Maps(op) => - InterpTernaryMaps(expr, op, v0, v1, v2) + case Sequences(op) => + InterpTernarySequences(expr, op, v0, v1, v2) + case Multisets(op) => + InterpTernaryMultisets(expr, op, v0, v1, v2) + case Maps(op) => + InterpTernaryMaps(expr, op, v0, v1, v2) } function method NeedValidIndex(expr: Expr, vs: Value, vidx: Value) : Outcome { // FIXME no monadic operator for combining outcomes? match Need(vidx.Int? && vs.Seq?, Invalid(expr)) - case Pass() => Need(0 <= vidx.i < |vs.sq|, OutOfSeqBounds(vs, vidx)) - case fail => fail + case Pass() => Need(0 <= vidx.i < |vs.sq|, OutOfSeqBounds(vs, vidx)) + case fail => fail } function method NeedValidEndpoint(expr: Expr, vs: Value, vidx: Value) : Outcome { match Need(vidx.Int? && vs.Seq?, Invalid(expr)) - case Pass() => Need(0 <= vidx.i <= |vs.sq|, OutOfSeqBounds(vs, vidx)) - case fail => fail + case Pass() => Need(0 <= vidx.i <= |vs.sq|, OutOfSeqBounds(vs, vidx)) + case fail => fail } function method InterpTernarySequences(expr: Expr, op: Syntax.TernaryOps.Sequences, v0: Value, v1: Value, v2: Value) : PureInterpResult { match op - case SeqUpdate() => - :- NeedValidIndex(expr, v0, v1); - Success(V.Seq(v0.sq[v1.i := v2])) - case SeqSubseq() => - :- NeedValidEndpoint(expr, v0, v2); - :- Need(v1.Int?, Invalid(expr)); - :- Need(0 <= v1.i <= v2.i, OutOfIntBounds(v1.i, Some(0), Some(v2.i))); - Success(V.Seq(v0.sq[v1.i..v2.i])) + case SeqUpdate() => + :- NeedValidIndex(expr, v0, v1); + Success(V.Seq(v0.sq[v1.i := v2])) + case SeqSubseq() => + :- NeedValidEndpoint(expr, v0, v2); + :- Need(v1.Int?, Invalid(expr)); + :- Need(0 <= v1.i <= v2.i, OutOfIntBounds(v1.i, Some(0), Some(v2.i))); + Success(V.Seq(v0.sq[v1.i..v2.i])) } function method InterpTernaryMultisets(expr: Expr, op: Syntax.TernaryOps.Multisets, v0: Value, v1: Value, v2: Value) : PureInterpResult { match op - case MultisetUpdate() => - :- Need(v0.Multiset?, Invalid(expr)); - :- Need(v2.Int? && v2.i >= 0, Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Multiset(v0.ms[v1 := v2.i])) + case MultisetUpdate() => + :- Need(v0.Multiset?, Invalid(expr)); + :- Need(v2.Int? && v2.i >= 0, Invalid(expr)); + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Multiset(v0.ms[v1 := v2.i])) } function method InterpTernaryMaps(expr: Expr, op: Syntax.TernaryOps.Maps, v0: Value, v1: Value, v2: Value) : PureInterpResult { match op - case MapUpdate() => - :- Need(v0.Map?, Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Map(v0.m[v1 := v2])) + case MapUpdate() => + :- Need(v0.Map?, Invalid(expr)); + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Map(v0.m[v1 := v2])) } function method {:opaque} InterpDisplay(e: Expr, kind: Types.CollectionKind, argvs: seq) : PureInterpResult { match kind - case Map(_) => - var m :- InterpMapDisplay(e, argvs); - Success(V.Map(m)) - case Multiset() => - :- Need(forall i | 0 <= i < |argvs| :: HasEqValue(argvs[i]), Invalid(e)); // The elements must have a decidable equality - var v := V.Multiset(multiset(argvs)); - assert WellFormedEqValue(v); // Doesn't work without this assert - Success(v) - case Seq() => - Success(V.Seq(argvs)) - case Set() => - :- Need(forall x | x in argvs :: HasEqValue(x), Invalid(e)); // The elements must have a decidable equality - Success(V.Set(set s | s in argvs)) + case Map(_) => + var m :- InterpMapDisplay(e, argvs); + Success(V.Map(m)) + case Multiset() => + :- Need(forall i | 0 <= i < |argvs| :: HasEqValue(argvs[i]), Invalid(e)); // The elements must have a decidable equality + var v := V.Multiset(multiset(argvs)); + assert WellFormedEqValue(v); // Doesn't work without this assert + Success(v) + case Seq() => + Success(V.Seq(argvs)) + case Set() => + :- Need(forall x | x in argvs :: HasEqValue(x), Invalid(e)); // The elements must have a decidable equality + Success(V.Set(set s | s in argvs)) } function method InterpMapDisplay(e: Expr, argvs: seq) @@ -829,8 +829,8 @@ module Bootstrap.Semantics.Interp { : PureInterpResult<(EqWV, Value)> { :- Need(argv.Seq? && |argv.sq| == 2, Invalid(e)); - :- Need(HasEqValue(argv.sq[0]), Invalid(e)); - Success((argv.sq[0], argv.sq[1])) + :- Need(HasEqValue(argv.sq[0]), Invalid(e)); + Success((argv.sq[0], argv.sq[1])) } function method AugmentContext(base: Context, vars: seq, vals: seq) @@ -852,13 +852,13 @@ module Bootstrap.Semantics.Interp { decreases env.fuel, e, 0 { :- Need(env.fuel > 0, OutOfFuel(fn)); - :- Need(fn.Closure?, Invalid(e)); - reveal SupportsInterp(); - Predicates.Deep.AllImpliesChildren(fn.body, SupportsInterp1); - :- Need(|fn.vars| == |argvs|, SignatureMismatch(fn.vars, argvs)); - var ctx := State(locals := AugmentContext(fn.ctx, fn.vars, argvs)); - var Return(val, ctx) :- InterpExpr(fn.body, env.(fuel := env.fuel - 1), ctx); - Success(val) + :- Need(fn.Closure?, Invalid(e)); + reveal SupportsInterp(); + Predicates.Deep.AllImpliesChildren(fn.body, SupportsInterp1); + :- Need(|fn.vars| == |argvs|, SignatureMismatch(fn.vars, argvs)); + var ctx := State(locals := AugmentContext(fn.ctx, fn.vars, argvs)); + var Return(val, ctx) :- InterpExpr(fn.body, env.(fuel := env.fuel - 1), ctx); + Success(val) } // TODO(SMH): update this to not enforce the intermediary blocks to evaluate to `Unit`, diff --git a/src/Semantics/Printer.dfy b/src/Semantics/Printer.dfy index c4e63542..68c9d9f0 100644 --- a/src/Semantics/Printer.dfy +++ b/src/Semantics/Printer.dfy @@ -9,17 +9,17 @@ module Bootstrap.Semantics.Printer { function method ToString(v: Values.T) : string { match v - case Unit => "()" - case Bool(b) => Str.of_bool(b) - case Char(c) => "'" + Str.of_char(c) + "'" - case Int(i) => Str.of_int(i) - case Real(r) => var (n, d) := Interop.TypeConv.AsIntegerRatio(r); Str.of_int(n) + "/" + Str.of_int(d) - case BigOrdinal(o) => "<*>" // FIXME - case BitVector(width, value) => "bv" + Str.of_int(width, 10) + "(0x" + Str.of_int(value, 16) + ")" - case Map(m) => "map[" + "<*>" + "]" // FIXME iterate over map - case Multiset(ms) => "multiset{" + "<*>" + "}]" // FIXME iterate over multiset (convert to map?) - case Seq(sq) => "[" + Lib.Str.Join(", ", Lib.Seq.Map(v requires v in sq => ToString(v), sq)) + "]" - case Set(st) => "set{" + "<*>" + "}" // FIXME iterate over set - case Closure(ctx, vars, body) => "(" + Lib.Str.Join(", ", vars) + ") => <*>" // FIXME print context + case Unit => "()" + case Bool(b) => Str.of_bool(b) + case Char(c) => "'" + Str.of_char(c) + "'" + case Int(i) => Str.of_int(i) + case Real(r) => var (n, d) := Interop.TypeConv.AsIntegerRatio(r); Str.of_int(n) + "/" + Str.of_int(d) + case BigOrdinal(o) => "<*>" // FIXME + case BitVector(width, value) => "bv" + Str.of_int(width, 10) + "(0x" + Str.of_int(value, 16) + ")" + case Map(m) => "map[" + "<*>" + "]" // FIXME iterate over map + case Multiset(ms) => "multiset{" + "<*>" + "}]" // FIXME iterate over multiset (convert to map?) + case Seq(sq) => "[" + Lib.Str.Join(", ", Lib.Seq.Map(v requires v in sq => ToString(v), sq)) + "]" + case Set(st) => "set{" + "<*>" + "}" // FIXME iterate over set + case Closure(ctx, vars, body) => "(" + Lib.Str.Join(", ", vars) + ") => <*>" // FIXME print context } } diff --git a/src/Semantics/Pure.dfy b/src/Semantics/Pure.dfy index ffea548a..e39fffe4 100644 --- a/src/Semantics/Pure.dfy +++ b/src/Semantics/Pure.dfy @@ -1,4 +1,4 @@ -include "../Interop/CSharpDafnyASTModel.dfy" + include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" @@ -25,26 +25,26 @@ module Bootstrap.Semantics.Pure { predicate method IsPure_Single(e: Syntax.Expr) { match e - case Var(_) => true - case Literal(_) => true - case Abs(_, _) => true - case Apply(aop, _) => - match aop { - case Lazy(lOp) => true - case Eager(eOp) => - match eOp { - case UnaryOp(_) => true - case BinaryOp(_) => true - case TernaryOp(_) => true - case Builtin(Display(_)) => true - case Builtin(Print) => false // For now, we actually don't model the fact that `Print` has side effects - case FunctionCall() => true // TODO(SMH): ok for now because we only have terminating, pure functions - case DataConstructor(_, _) => true - } - } - case Block(_) => true - case Bind(_, _, _) => true - case If(_, _, _) => true + case Var(_) => true + case Literal(_) => true + case Abs(_, _) => true + case Apply(aop, _) => + match aop { + case Lazy(lOp) => true + case Eager(eOp) => + match eOp { + case UnaryOp(_) => true + case BinaryOp(_) => true + case TernaryOp(_) => true + case Builtin(Display(_)) => true + case Builtin(Print) => false // For now, we actually don't model the fact that `Print` has side effects + case FunctionCall() => true // TODO(SMH): ok for now because we only have terminating, pure functions + case DataConstructor(_, _) => true + } + } + case Block(_) => true + case Bind(_, _, _) => true + case If(_, _, _) => true } predicate method {:opaque} IsPure(e: Syntax.Expr) { @@ -68,19 +68,19 @@ module Bootstrap.Semantics.Pure { reveal IsPure(); reveal InterpExpr(); match e - case Var(v) => - case Abs(vars, body) => {} - case Literal(lit) => {} - case Apply(Lazy(op), args) => - InterpExpr_Lazy_IsPure_SameState(e, env, ctx); - case Apply(Eager(op), args) => - InterpExpr_Eager_IsPure_SameState(e, env, ctx); - case Bind(vars, exprs, body) => - assume false; // TODO: prove - case Block(stmts) => - InterpExpr_Block_IsPure_SameState(e, env, ctx); - case If(cond, thn, els) => - InterpExpr_If_IsPure_SameState(e, env, ctx); + case Var(v) => + case Abs(vars, body) => {} + case Literal(lit) => {} + case Apply(Lazy(op), args) => + InterpExpr_Lazy_IsPure_SameState(e, env, ctx); + case Apply(Eager(op), args) => + InterpExpr_Eager_IsPure_SameState(e, env, ctx); + case Bind(vars, exprs, body) => + assume false; // TODO: prove + case Block(stmts) => + InterpExpr_Block_IsPure_SameState(e, env, ctx); + case If(cond, thn, els) => + InterpExpr_If_IsPure_SameState(e, env, ctx); } lemma InterpExprWithType_IsPure_SameState(e: PureExpr, ty: Type, env: Environment, ctx: State) @@ -103,7 +103,7 @@ module Bootstrap.Semantics.Pure { reveal InterpExpr(); reveal IsPure(); reveal InterpLazy(); - + var op, e0, e1 := e.aop.lOp, e.args[0], e.args[1]; var res0 := InterpExprWithType(e0, Type.Bool, env, ctx); if res0.Success? { diff --git a/src/Semantics/Values.dfy b/src/Semantics/Values.dfy index e53527f0..b7dc1c36 100644 --- a/src/Semantics/Values.dfy +++ b/src/Semantics/Values.dfy @@ -1,4 +1,4 @@ -include "../AST/Syntax.dfy" + include "../AST/Syntax.dfy" include "../Utils/Library.dfy" module Bootstrap.Semantics.Values { @@ -26,56 +26,56 @@ module Bootstrap.Semantics.Values { predicate method HasType(ty: Types.T) { this.WellFormed1() && match (this, ty) // FIXME tests on other side - case (Unit, Unit) => true - case (Bool(b), Bool()) => true - case (Char(c), Char()) => true - case (Int(i), Int()) => true - case (Real(r), Real()) => true - case (BigOrdinal(o), BigOrdinal()) => true - case (BitVector(width, value), BitVector(twidth)) => - width == twidth - case (Map(m), Collection(true, Map(kT), eT)) => - forall x | x in m :: x.HasType(kT) && m[x].HasType(eT) - case (Multiset(ms), Collection(true, Multiset, eT)) => - forall x | x in ms :: x.HasType(eT) - case (Seq(sq), Collection(true, Seq, eT)) => - forall x | x in sq :: x.HasType(eT) - case (Set(st), Collection(true, Set, eT)) => - forall x | x in st :: x.HasType(eT) - case (Closure(ctx, vars, body), Function(args, ret)) => - true // FIXME: Need a typing relation on terms, not just values + case (Unit, Unit) => true + case (Bool(b), Bool()) => true + case (Char(c), Char()) => true + case (Int(i), Int()) => true + case (Real(r), Real()) => true + case (BigOrdinal(o), BigOrdinal()) => true + case (BitVector(width, value), BitVector(twidth)) => + width == twidth + case (Map(m), Collection(true, Map(kT), eT)) => + forall x | x in m :: x.HasType(kT) && m[x].HasType(eT) + case (Multiset(ms), Collection(true, Multiset, eT)) => + forall x | x in ms :: x.HasType(eT) + case (Seq(sq), Collection(true, Seq, eT)) => + forall x | x in sq :: x.HasType(eT) + case (Set(st), Collection(true, Set, eT)) => + forall x | x in st :: x.HasType(eT) + case (Closure(ctx, vars, body), Function(args, ret)) => + true // FIXME: Need a typing relation on terms, not just values - // DISCUSS: Better way to write this? Need exhaustivity checking - case (Unit, _) => false - case (Bool(b), _) => false - case (Char(c), _) => false - case (Int(i), _) => false - case (Real(r), _) => false - case (BigOrdinal(o), _) => false - case (BitVector(width, value), _) => false - case (Map(m), _) => false - case (Multiset(ms), _) => false - case (Seq(sq), _) => false - case (Set(st), _) => false - case (Closure(ctx, vars, body), _) => false + // DISCUSS: Better way to write this? Need exhaustivity checking + case (Unit, _) => false + case (Bool(b), _) => false + case (Char(c), _) => false + case (Int(i), _) => false + case (Real(r), _) => false + case (BigOrdinal(o), _) => false + case (BitVector(width, value), _) => false + case (Map(m), _) => false + case (Multiset(ms), _) => false + case (Seq(sq), _) => false + case (Set(st), _) => false + case (Closure(ctx, vars, body), _) => false } function method Children() : (cs: set) ensures forall c | c in cs :: c < this { match this - case Unit => {} - case Bool(b) => {} - case Char(c) => {} - case Int(i) => {} - case Real(r) => {} - case BigOrdinal(o) => {} - case BitVector(width, value) => {} - case Map(m) => m.Values - case Multiset(ms) => set x | x in ms - case Seq(sq) => set x | x in sq - case Set(st) => st - case Closure(ctx, vars_, body_) => ctx.Values + case Unit => {} + case Bool(b) => {} + case Char(c) => {} + case Int(i) => {} + case Real(r) => {} + case BigOrdinal(o) => {} + case BitVector(width, value) => {} + case Map(m) => m.Values + case Multiset(ms) => set x | x in ms + case Seq(sq) => set x | x in sq + case Set(st) => st + case Closure(ctx, vars_, body_) => ctx.Values } // This duplicates a bit ``Types.WellFormed()``. diff --git a/src/Transforms/BottomUp.dfy b/src/Transforms/BottomUp.dfy index e52284bf..395273e7 100644 --- a/src/Transforms/BottomUp.dfy +++ b/src/Transforms/BottomUp.dfy @@ -1,4 +1,4 @@ -include "../Interop/CSharpDafnyASTModel.dfy" + include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" @@ -30,10 +30,10 @@ module Bootstrap.Transforms.BottomUp { // - `e'` satisfies the pre of `f` { forall e, e' :: - && Exprs.ConstructorsMatch(e, e') - && f.requires(e) - && Deep.AllChildren_Expr(e', post) - ==> f.requires(e') + && Exprs.ConstructorsMatch(e, e') + && f.requires(e) + && Deep.AllChildren_Expr(e', post) + ==> f.requires(e') } predicate TransformerMatchesPrePost(f: Expr --> Expr, post: Expr -> bool) @@ -47,7 +47,7 @@ module Bootstrap.Transforms.BottomUp { // - `f(e)` deeply satisfies the post of `f` { forall e: Expr | Deep.AllChildren_Expr(e, post) && f.requires(e) :: - Deep.All_Expr(f(e), post) + Deep.All_Expr(f(e), post) } // FIXME(CPC) move? @@ -63,10 +63,10 @@ module Bootstrap.Transforms.BottomUp { // can relate `e` and `f(e')` with `rel`. { forall e, e' :: - && Exprs.ConstructorsMatch(e, e') - && f.requires(e') - && All_Rel_Forall(rel, e.Children(), e'.Children()) - ==> rel(e, f(e')) + && Exprs.ConstructorsMatch(e, e') + && f.requires(e') + && All_Rel_Forall(rel, e.Children(), e'.Children()) + ==> rel(e, f(e')) } predicate IsBottomUpTransformer(f: Expr --> Expr, post: Expr -> bool) @@ -104,9 +104,9 @@ module Bootstrap.Transforms.BottomUp { // and can be lifted through the map function. { forall e, e' :: - && Exprs.ConstructorsMatch(e, e') - && All_Rel_Forall(rel, e.Children(), e'.Children()) - ==> rel(e, e') + && Exprs.ConstructorsMatch(e, e') + && All_Rel_Forall(rel, e.Children(), e'.Children()) + ==> rel(e, e') } // A bottom-up transformer, i.e.: a transformer we can recursively apply bottom-up to @@ -507,9 +507,9 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { requires EqCtx(cv.ctx, cv'.ctx) requires EqInterp(cv.body, cv'.body) ensures - var res := InterpCallFunctionBody(cv, env, argvs); - var res' := InterpCallFunctionBody(cv', env, argvs'); - EqPureInterpResultValue(res, res') + var res := InterpCallFunctionBody(cv, env, argvs); + var res' := InterpCallFunctionBody(cv', env, argvs'); + EqPureInterpResultValue(res, res') { var res := InterpCallFunctionBody(cv, env, argvs); var res' := InterpCallFunctionBody(cv', env, argvs'); @@ -644,8 +644,8 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { // TODO: e and e' should be the same actually lemma EqInterp_Expr_UnaryOp_CanBeMapLifted( - e: Interp.Expr, e': Interp.Expr, op: UnaryOp, v: WV, v': WV - ) + e: Interp.Expr, e': Interp.Expr, op: UnaryOp, v: WV, v': WV + ) requires !op.MemberSelect? requires EqValue(v, v') ensures EqPureInterpResultValue(InterpUnaryOp(e, op, v), InterpUnaryOp(e', op, v')) @@ -703,8 +703,8 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { // but it is a bit annoying to do... // TODO: e and e' should be the same actually lemma EqInterp_Expr_BinaryOp_CanBeMapLifted( - e: Interp.Expr, e': Interp.Expr, bop: BinaryOp, v0: WV, v1: WV, v0': WV, v1': WV - ) + e: Interp.Expr, e': Interp.Expr, bop: BinaryOp, v0: WV, v1: WV, v0': WV, v1': WV + ) requires !bop.BV? && !bop.Datatypes? requires EqValue(v0, v0') requires EqValue(v1, v1') @@ -876,8 +876,8 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { // TODO: e and e' should be the same actually lemma EqInterp_Expr_TernaryOp_CanBeMapLifted( - e: Interp.Expr, e': Interp.Expr, top: TernaryOp, v0: WV, v1: WV, v2: WV, v0': WV, v1': WV, v2': WV - ) + e: Interp.Expr, e': Interp.Expr, top: TernaryOp, v0: WV, v1: WV, v2: WV, v0': WV, v1': WV, v2': WV + ) requires EqValue(v0, v0') requires EqValue(v1, v1') requires EqValue(v2, v2') @@ -900,8 +900,8 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { } lemma EqInterp_Expr_Display_CanBeMapLifted( - e: Interp.Expr, e': Interp.Expr, kind: Types.CollectionKind, vs: seq, vs': seq - ) + e: Interp.Expr, e': Interp.Expr, kind: Types.CollectionKind, vs: seq, vs': seq + ) requires EqSeqValue(vs, vs') ensures EqPureInterpResultValue(InterpDisplay(e, kind, vs), InterpDisplay(e', kind, vs')) { @@ -950,8 +950,8 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { } lemma EqInterp_Expr_FunctionCall_CanBeMapLifted( - e: Interp.Expr, e': Interp.Expr, env: Environment, f: WV, f': WV, argvs: seq, argvs': seq - ) + e: Interp.Expr, e': Interp.Expr, env: Environment, f: WV, f': WV, argvs: seq, argvs': seq + ) requires EqValue(f, f') requires EqSeqValue(argvs, argvs') ensures EqPureInterpResultValue(InterpFunctionCall(e, env, f, argvs), @@ -1070,7 +1070,7 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { var res' := InterpBlock_Exprs(es', env, ctx'); if es == [] { - // Trivial + // Trivial } else if |es| == 1 { assert es == [es[0]]; @@ -1136,9 +1136,9 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { { forall e, e' ensures - (&& Exprs.ConstructorsMatch(e, e') - && All_Rel_Forall(EqInterp, e.Children(), e'.Children())) - ==> EqInterp(e, e') + (&& Exprs.ConstructorsMatch(e, e') + && All_Rel_Forall(EqInterp, e.Children(), e'.Children())) + ==> EqInterp(e, e') { if && Exprs.ConstructorsMatch(e, e') && All_Rel_Forall(EqInterp, e.Children(), e'.Children()) { @@ -1147,7 +1147,7 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { assert SupportsInterp(e'); forall env, ctx, ctx' | EqState(ctx, ctx') ensures - EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) { + EqInterpResultValue(InterpExpr(e, env, ctx), InterpExpr(e', env, ctx')) { reveal EqInterp_CanBeMapLifted_Pre(); reveal EqInterp_CanBeMapLifted_Post(); EqInterp_Expr_CanBeMapLifted(e, e', env, ctx, ctx'); @@ -1158,7 +1158,7 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { else {} } } - + // TODO(SMH): move? (or even remove?) lemma EqInterp_CanBeComposed(f: Expr --> Expr, g: Expr --> Expr) requires TransformerShallowPreservesRel(f, EqInterp) @@ -1180,8 +1180,8 @@ module Bootstrap.Transforms.Proofs.BottomUp_ { // It is enough to prove that `f` links its input and output with ``EqInterp`` // to be able to lift it through map. { - EqInterp_IsTransitive(); - EqInterp_CanBeMapLifted(); - TransformationAndRel_Lift(f, EqInterp); + EqInterp_IsTransitive(); + EqInterp_CanBeMapLifted(); + TransformationAndRel_Lift(f, EqInterp); } } diff --git a/src/Transforms/Generic.dfy b/src/Transforms/Generic.dfy index a9ea714f..1db81804 100644 --- a/src/Transforms/Generic.dfy +++ b/src/Transforms/Generic.dfy @@ -1,4 +1,4 @@ -include "../AST/Syntax.dfy" + include "../AST/Syntax.dfy" module Bootstrap.Transforms.Generic { import opened AST.Syntax diff --git a/src/Utils/Library.dfy b/src/Utils/Library.dfy index 454f658d..e79a7cd2 100644 --- a/src/Utils/Library.dfy +++ b/src/Utils/Library.dfy @@ -1,372 +1,372 @@ module Utils.Lib { -module ControlFlow { - function method Unreachable() : A - requires false - { - match () {} + module ControlFlow { + function method Unreachable() : A + requires false + { + match () {} + } } -} -module Debug { - class {:compile false} Debugger { - static method {:extern "System.Diagnostics.Debugger", "Break"} Break() {} - } + module Debug { + class {:compile false} Debugger { + static method {:extern "System.Diagnostics.Debugger", "Break"} Break() {} + } - function TODO(a : A) : A { - a - } by method { - Debugger.Break(); - return a; + function TODO(a : A) : A { + a + } by method { + Debugger.Break(); + return a; + } } -} -module Datatypes { - datatype Option<+T> = | Some(value: T) | None - { - function method UnwrapOr(default: T) : T { - if this.Some? then value else default - } + module Datatypes { + datatype Option<+T> = | Some(value: T) | None + { + function method UnwrapOr(default: T) : T { + if this.Some? then value else default + } - function method ToSuccessOr(f: E): Result { - match this + function method ToSuccessOr(f: E): Result { + match this case Some(v) => Success(v) case None() => Failure(f) + } } - } - datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) { - predicate method IsFailure() { - Failure? + datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) { + predicate method IsFailure() { + Failure? + } + + function method PropagateFailure(): Result + requires Failure? + { + Failure(this.error) + } + + function method Extract(): T + requires Success? + { + value + } + + // FIXME: Port + function method MapFailure(f: R --> R') : Result + requires this.Failure? ==> f.requires(this.error) + { + match this + case Success(value) => Success(value) + case Failure(error) => Failure(f(error)) + } + + function method Then(f: T --> Result) : Result + requires Success? ==> f.requires(value) + { + match this + case Success(value) => f(value) + case Failure(err) => Failure(err) + } } - function method PropagateFailure(): Result - requires Failure? + datatype Outcome = Pass | Fail(error: E) { - Failure(this.error) + predicate method IsFailure() { + Fail? + } + // Note: PropagateFailure returns a Result, not an Outcome. + function method PropagateFailure(): Result + requires Fail? + { + Failure(this.error) + } + // Note: no Extract method } - function method Extract(): T - requires Success? + // A helper function to ensure a requirement is true at runtime + // :- Need(5 == |mySet|, "The set MUST have 5 elements.") + // FIXME: Move to library (added opaque) + function method {:opaque} Need(condition: bool, error: E): (result: Outcome) + ensures condition <==> result.Pass? { - value + if condition then Pass else Fail(error) } + } - // FIXME: Port - function method MapFailure(f: R --> R') : Result - requires this.Failure? ==> f.requires(this.error) + module Seq { + // FIXME why not use a comprehension directly? + function method {:opaque} Map(f: T ~> Q, ts: seq) : (qs: seq) + reads f.reads + requires forall t | t in ts :: f.requires(t) + ensures |qs| == |ts| + ensures forall i | 0 <= i < |ts| :: qs[i] == f(ts[i]) + ensures forall q | q in qs :: exists t | t in ts :: q == f(t) { - match this - case Success(value) => Success(value) - case Failure(error) => Failure(f(error)) + if ts == [] then [] else [f(ts[0])] + Map(f, ts[1..]) } - function method Then(f: T --> Result) : Result - requires Success? ==> f.requires(value) + function method FoldL(f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq) : TAcc + reads f.reads + requires forall a, t | t in ts :: f.requires(a, t) { - match this - case Success(value) => f(value) - case Failure(err) => Failure(err) + if ts == [] then a0 else FoldL(f, f(a0, ts[0]), ts[1..]) } - } - datatype Outcome = Pass | Fail(error: E) - { - predicate method IsFailure() { - Fail? - } - // Note: PropagateFailure returns a Result, not an Outcome. - function method PropagateFailure(): Result - requires Fail? + lemma FoldL_induction'( + f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq, + prefix: seq, P: (TAcc, seq) -> bool + ) + requires forall a, t | t in ts :: f.requires(a, t) + requires P(a0, prefix) + requires forall a, t, ts' | t in ts && P(a, ts') :: P(f(a, t), ts' + [t]) + ensures P(FoldL(f, a0, ts), prefix + ts) { - Failure(this.error) + if ts == [] { + assert prefix + ts == prefix; + } else { + var t0, ts' := ts[0], ts[1..]; + var a0' := f(a0, t0); + var prefix' := prefix + [t0]; + FoldL_induction'(f, a0', ts[1..], prefix', P); + assert P(FoldL(f, a0', ts[1..]), prefix' + ts'); + assert prefix' + ts' == prefix + ts; + } } - // Note: no Extract method - } - - // A helper function to ensure a requirement is true at runtime - // :- Need(5 == |mySet|, "The set MUST have 5 elements.") - // FIXME: Move to library (added opaque) - function method {:opaque} Need(condition: bool, error: E): (result: Outcome) - ensures condition <==> result.Pass? - { - if condition then Pass else Fail(error) - } -} - -module Seq { - // FIXME why not use a comprehension directly? - function method {:opaque} Map(f: T ~> Q, ts: seq) : (qs: seq) - reads f.reads - requires forall t | t in ts :: f.requires(t) - ensures |qs| == |ts| - ensures forall i | 0 <= i < |ts| :: qs[i] == f(ts[i]) - ensures forall q | q in qs :: exists t | t in ts :: q == f(t) - { - if ts == [] then [] else [f(ts[0])] + Map(f, ts[1..]) - } - function method FoldL(f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq) : TAcc - reads f.reads - requires forall a, t | t in ts :: f.requires(a, t) - { - if ts == [] then a0 else FoldL(f, f(a0, ts[0]), ts[1..]) - } - - lemma FoldL_induction'( - f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq, - prefix: seq, P: (TAcc, seq) -> bool - ) - requires forall a, t | t in ts :: f.requires(a, t) - requires P(a0, prefix) - requires forall a, t, ts' | t in ts && P(a, ts') :: P(f(a, t), ts' + [t]) - ensures P(FoldL(f, a0, ts), prefix + ts) - { - if ts == [] { - assert prefix + ts == prefix; - } else { - var t0, ts' := ts[0], ts[1..]; - var a0' := f(a0, t0); - var prefix' := prefix + [t0]; - FoldL_induction'(f, a0', ts[1..], prefix', P); - assert P(FoldL(f, a0', ts[1..]), prefix' + ts'); - assert prefix' + ts' == prefix + ts; + lemma FoldL_induction( + f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq, + P: (TAcc, seq) -> bool + ) + requires forall a, t | t in ts :: f.requires(a, t) + requires P(a0, []) + requires forall a, t, ts' | t in ts && P(a, ts') :: P(f(a, t), ts' + [t]) + ensures P(FoldL(f, a0, ts), ts) + { + assert [] + ts == ts; + FoldL_induction'(f, a0, ts, [], P); } - } - lemma FoldL_induction( - f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq, - P: (TAcc, seq) -> bool - ) - requires forall a, t | t in ts :: f.requires(a, t) - requires P(a0, []) - requires forall a, t, ts' | t in ts && P(a, ts') :: P(f(a, t), ts' + [t]) - ensures P(FoldL(f, a0, ts), ts) - { - assert [] + ts == ts; - FoldL_induction'(f, a0, ts, [], P); - } + function method FoldR(f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq) : TAcc + reads f.reads + requires forall a, t | t in ts :: f.requires(a, t) + { + if ts == [] then a0 else f(FoldL(f, a0, ts[1..]), ts[0]) + } - function method FoldR(f: (TAcc, T) ~> TAcc, a0: TAcc, ts: seq) : TAcc - reads f.reads - requires forall a, t | t in ts :: f.requires(a, t) - { - if ts == [] then a0 else f(FoldL(f, a0, ts[1..]), ts[0]) - } + // TODO: Why not use forall directly? + function method {:opaque} All(P: T ~> bool, ts: seq) : (b: bool) + reads P.reads + requires forall t | t in ts :: P.requires(t) + ensures b == forall t | t in ts :: P(t) + ensures b == forall i | 0 <= i < |ts| :: P(ts[i]) + { + if ts == [] then true else P(ts[0]) && All(P, ts[1..]) + } - // TODO: Why not use forall directly? - function method {:opaque} All(P: T ~> bool, ts: seq) : (b: bool) - reads P.reads - requires forall t | t in ts :: P.requires(t) - ensures b == forall t | t in ts :: P(t) - ensures b == forall i | 0 <= i < |ts| :: P(ts[i]) - { - if ts == [] then true else P(ts[0]) && All(P, ts[1..]) - } + lemma All_weaken(P: T ~> bool, Q: T~> bool, ts: seq) + requires forall t | t in ts :: P.requires(t) + requires forall t | t in ts :: Q.requires(t) + requires forall t | t in ts :: P(t) ==> Q(t) + ensures All(P, ts) ==> All(Q, ts) + {} + + lemma All_weaken_auto(ts: seq) + ensures forall P: T ~> bool, Q: T ~> bool | + && (forall t: T | t in ts :: P.requires(t)) + && (forall t: T | t in ts :: Q.requires(t)) + && (forall t: T | t in ts :: P(t) ==> Q(t)) :: + All(P, ts) ==> All(Q, ts) + {} + + import Math + + function method {:opaque} Max(s: seq, default: int) : (m: int) + requires forall i | i in s :: default <= i + ensures if s == [] then m == default else m in s + ensures forall i | i in s :: i <= m + ensures default <= m + { + var P := (m, s) => + && (if s == [] then m == default else m in s) + && (forall i | i in s :: i <= m); + FoldL_induction(Math.Max, default, s, P); + FoldL(Math.Max, default, s) + } - lemma All_weaken(P: T ~> bool, Q: T~> bool, ts: seq) - requires forall t | t in ts :: P.requires(t) - requires forall t | t in ts :: Q.requires(t) - requires forall t | t in ts :: P(t) ==> Q(t) - ensures All(P, ts) ==> All(Q, ts) - {} - - lemma All_weaken_auto(ts: seq) - ensures forall P: T ~> bool, Q: T ~> bool | - && (forall t: T | t in ts :: P.requires(t)) - && (forall t: T | t in ts :: Q.requires(t)) - && (forall t: T | t in ts :: P(t) ==> Q(t)) :: - All(P, ts) ==> All(Q, ts) - {} - - import Math - - function method {:opaque} Max(s: seq, default: int) : (m: int) - requires forall i | i in s :: default <= i - ensures if s == [] then m == default else m in s - ensures forall i | i in s :: i <= m - ensures default <= m - { - var P := (m, s) => - && (if s == [] then m == default else m in s) - && (forall i | i in s :: i <= m); - FoldL_induction(Math.Max, default, s, P); - FoldL(Math.Max, default, s) - } + function method {:opaque} MaxF(f: T ~> int, ts: seq, default: int) : (m: int) + reads f.reads + requires forall t | t in ts :: f.requires(t) + requires forall t | t in ts :: default <= f(t) + ensures if ts == [] then m == default else exists t | t in ts :: f(t) == m + ensures forall t | t in ts :: f(t) <= m + ensures default <= m + { + var s := Map(f, ts); + var m := Max(s, default); + assert forall t | t in ts :: f(t) <= m by { + forall t | t in ts ensures f(t) <= m { assert f(t) in s; } + } + m + } - function method {:opaque} MaxF(f: T ~> int, ts: seq, default: int) : (m: int) - reads f.reads - requires forall t | t in ts :: f.requires(t) - requires forall t | t in ts :: default <= f(t) - ensures if ts == [] then m == default else exists t | t in ts :: f(t) == m - ensures forall t | t in ts :: f(t) <= m - ensures default <= m - { - var s := Map(f, ts); - var m := Max(s, default); - assert forall t | t in ts :: f(t) <= m by { - forall t | t in ts ensures f(t) <= m { assert f(t) in s; } + function method {:opaque} Zip(ts: seq, qs: seq) + : (tqs: seq<(T, Q)>) + requires |ts| == |qs| + ensures |ts| == |tqs| == |qs| + ensures forall i | 0 <= i < |tqs| :: tqs[i] == (ts[i], qs[i]) + ensures forall tq | tq in tqs :: tq.0 in ts && tq.1 in qs + { + if ts == [] then [] + else [(ts[0], qs[0])] + Zip(ts[1..], qs[1..]) } - m - } - function method {:opaque} Zip(ts: seq, qs: seq) - : (tqs: seq<(T, Q)>) - requires |ts| == |qs| - ensures |ts| == |tqs| == |qs| - ensures forall i | 0 <= i < |tqs| :: tqs[i] == (ts[i], qs[i]) - ensures forall tq | tq in tqs :: tq.0 in ts && tq.1 in qs - { - if ts == [] then [] - else [(ts[0], qs[0])] + Zip(ts[1..], qs[1..]) - } + // TODO: Merge. Removed unnecessary trigger and strengthened postcondition + function method {:opaque} Filter(s: seq, f: (T ~> bool)): (result: seq) + requires forall i | 0 <= i < |s| :: f.requires(s[i]) + ensures |result| <= |s| // DISCUSS: This allows duplication / unifiqation + ensures forall x | x in result :: f.requires(x) && x in s && f(x) + ensures forall x | x in s && f(x) :: x in result + reads f.reads + { + if |s| == 0 then [] + else (if f(s[0]) then [s[0]] else []) + Filter(s[1..], f) + } - // TODO: Merge. Removed unnecessary trigger and strengthened postcondition - function method {:opaque} Filter(s: seq, f: (T ~> bool)): (result: seq) - requires forall i | 0 <= i < |s| :: f.requires(s[i]) - ensures |result| <= |s| // DISCUSS: This allows duplication / unifiqation - ensures forall x | x in result :: f.requires(x) && x in s && f(x) - ensures forall x | x in s && f(x) :: x in result - reads f.reads - { - if |s| == 0 then [] - else (if f(s[0]) then [s[0]] else []) + Filter(s[1..], f) - } + import Datatypes - import Datatypes - - function method {:opaque} MapResult(ts: seq, f: T ~> Datatypes.Result) - : (qs: Datatypes.Result, E>) - reads f.reads - requires forall t | t in ts :: f.requires(t) - decreases ts - ensures qs.Success? ==> |qs.value| == |ts| - ensures qs.Success? ==> forall i | 0 <= i < |ts| :: f(ts[i]).Success? && qs.value[i] == f(ts[i]).value - ensures qs.Failure? ==> exists i | 0 <= i < |ts| :: f(ts[i]).Failure? && qs.error == f(ts[i]).error - { - if ts == [] then - Datatypes.Success([]) - else - var hd :- f(ts[0]); - var tl :- MapResult(ts[1..], f); - Datatypes.Success([hd] + tl) - } + function method {:opaque} MapResult(ts: seq, f: T ~> Datatypes.Result) + : (qs: Datatypes.Result, E>) + reads f.reads + requires forall t | t in ts :: f.requires(t) + decreases ts + ensures qs.Success? ==> |qs.value| == |ts| + ensures qs.Success? ==> forall i | 0 <= i < |ts| :: f(ts[i]).Success? && qs.value[i] == f(ts[i]).value + ensures qs.Failure? ==> exists i | 0 <= i < |ts| :: f(ts[i]).Failure? && qs.error == f(ts[i]).error + { + if ts == [] then + Datatypes.Success([]) + else + var hd :- f(ts[0]); + var tl :- MapResult(ts[1..], f); + Datatypes.Success([hd] + tl) + } - function method FoldLResult(f: (TAcc, T) ~> Datatypes.Result, a0: TAcc, ts: seq) - : (acc: Datatypes.Result) - reads f.reads - requires forall a, t | t in ts :: f.requires(a, t) - { - if ts == [] then Datatypes.Success(a0) - else - var a0 :- f(a0, ts[0]); - FoldLResult(f, a0, ts[1..]) - } + function method FoldLResult(f: (TAcc, T) ~> Datatypes.Result, a0: TAcc, ts: seq) + : (acc: Datatypes.Result) + reads f.reads + requires forall a, t | t in ts :: f.requires(a, t) + { + if ts == [] then Datatypes.Success(a0) + else + var a0 :- f(a0, ts[0]); + FoldLResult(f, a0, ts[1..]) + } - function method {:opaque} MapFilter(s: seq, f: (T ~> Datatypes.Option)): (result: seq) - requires forall i | 0 <= i < |s| :: f.requires(s[i]) - ensures |result| <= |s| - ensures forall y | y in result :: exists x | x in s :: f.requires(x) && f(x) == Datatypes.Some(y) - ensures forall x | x in s && f(x).Some? :: f(x).value in result - reads f.reads - { - if |s| == 0 then [] - else (match f(s[0]) + function method {:opaque} MapFilter(s: seq, f: (T ~> Datatypes.Option)): (result: seq) + requires forall i | 0 <= i < |s| :: f.requires(s[i]) + ensures |result| <= |s| + ensures forall y | y in result :: exists x | x in s :: f.requires(x) && f(x) == Datatypes.Some(y) + ensures forall x | x in s && f(x).Some? :: f(x).value in result + reads f.reads + { + if |s| == 0 then [] + else (match f(s[0]) case Some(y) => [y] case None => []) + MapFilter(s[1..], f) - } -} - -module Str { -module Private { - function method digits(n: int, base: int): (digits: seq) - requires base > 1 - requires n >= 0 - decreases n - ensures forall d | d in digits :: 0 <= d < base - { - if n == 0 then - [] - else - assert n > 0; - assert base > 1; - assert n < base * n; - assert n / base < n; - digits(n / base, base) + [n % base] + } } - function method string_of_digits(digits: seq, chars: seq) : string - requires forall d | d in digits :: 0 <= d < |chars| - { - if digits == [] then "" - else - assert digits[0] in digits; - assert forall d | d in digits[1..] :: d in digits; - [chars[digits[0]]] + string_of_digits(digits[1..], chars) - } -} + module Str { + module Private { + function method digits(n: int, base: int): (digits: seq) + requires base > 1 + requires n >= 0 + decreases n + ensures forall d | d in digits :: 0 <= d < base + { + if n == 0 then + [] + else + assert n > 0; + assert base > 1; + assert n < base * n; + assert n / base < n; + digits(n / base, base) + [n % base] + } + + function method string_of_digits(digits: seq, chars: seq) : string + requires forall d | d in digits :: 0 <= d < |chars| + { + if digits == [] then "" + else + assert digits[0] in digits; + assert forall d | d in digits[1..] :: d in digits; + [chars[digits[0]]] + string_of_digits(digits[1..], chars) + } + } - function method of_int_any(n: int, chars: seq) : string - requires |chars| > 1 - { - var base := |chars|; - if n == 0 then - "0" - else if n > 0 then - Private.string_of_digits(Private.digits(n, base), chars) - else - "-" + Private.string_of_digits(Private.digits(-n, base), chars) - } + function method of_int_any(n: int, chars: seq) : string + requires |chars| > 1 + { + var base := |chars|; + if n == 0 then + "0" + else if n > 0 then + Private.string_of_digits(Private.digits(n, base), chars) + else + "-" + Private.string_of_digits(Private.digits(-n, base), chars) + } - const HEX_DIGITS := [ - '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', - 'A', 'B', 'C', 'D', 'E', 'F'] + const HEX_DIGITS := [ + '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', + 'A', 'B', 'C', 'D', 'E', 'F'] - // FIXME rename - function method of_int(n: int, base: int := 10) : string - requires 2 <= base <= 16 - { - of_int_any(n, HEX_DIGITS[..base]) - } + // FIXME rename + function method of_int(n: int, base: int := 10) : string + requires 2 <= base <= 16 + { + of_int_any(n, HEX_DIGITS[..base]) + } - method Test() { // FIXME {:test}? - expect of_int(0, 10) == "0"; - expect of_int(3, 10) == "3"; - expect of_int(302, 10) == "302"; - expect of_int(-3, 10) == "-3"; - expect of_int(-302, 10) == "-302"; - } + method Test() { // FIXME {:test}? + expect of_int(0, 10) == "0"; + expect of_int(3, 10) == "3"; + expect of_int(302, 10) == "302"; + expect of_int(-3, 10) == "-3"; + expect of_int(-302, 10) == "-302"; + } - function method of_bool(b: bool) : string { - if b then "true" else "false" - } + function method of_bool(b: bool) : string { + if b then "true" else "false" + } - function method of_char(c: char) : string { - [c] - } + function method of_char(c: char) : string { + [c] + } - function method Join(sep: string, strs: seq) : string { - if |strs| == 0 then "" - else if |strs| == 1 then strs[0] - else strs[0] + sep + Join(sep, strs[1..]) - } + function method Join(sep: string, strs: seq) : string { + if |strs| == 0 then "" + else if |strs| == 1 then strs[0] + else strs[0] + sep + Join(sep, strs[1..]) + } - function method Concat(strs: seq) : string { - Join("", strs) + function method Concat(strs: seq) : string { + Join("", strs) + } } -} -module Math { - function method {:opaque} Max(x: int, y: int) : (m: int) - ensures x <= m - ensures y <= m - ensures x == m || y == m - { - if (x <= y) then y else x - } + module Math { + function method {:opaque} Max(x: int, y: int) : (m: int) + ensures x <= m + ensures y <= m + ensures x == m || y == m + { + if (x <= y) then y else x + } - function method {:opaque} IntPow(x: int, n: nat) : int { - if n == 0 then 1 - else x * IntPow(x, n - 1) + function method {:opaque} IntPow(x: int, n: nat) : int { + if n == 0 then 1 + else x * IntPow(x, n - 1) + } } } -} diff --git a/src/Utils/StrTree.dfy b/src/Utils/StrTree.dfy index 4608cb4d..0475adc3 100644 --- a/src/Utils/StrTree.dfy +++ b/src/Utils/StrTree.dfy @@ -11,11 +11,11 @@ module Utils.StrTree { { function method ToString() : string { match this - case Str(s) => s - case SepSeq(sep, asts) => - var strs := Lib.Seq.Map(s requires s in asts => s.ToString(), asts); - Lib.Str.Join(sep.UnwrapOr(""), strs) - case Unsupported => "<*>" + case Str(s) => s + case SepSeq(sep, asts) => + var strs := Lib.Seq.Map(s requires s in asts => s.ToString(), asts); + Lib.Str.Join(sep.UnwrapOr(""), strs) + case Unsupported => "<*>" } } @@ -40,8 +40,8 @@ module Utils.StrTree { } function method interleave( - outside: seq, inside: seq, start: int := 0 - ) : seq + outside: seq, inside: seq, start: int := 0 + ) : seq requires |outside| == |inside| + 1 requires 0 <= start < |outside| decreases |outside| - start @@ -67,14 +67,14 @@ module Utils.StrTree { lemma countFormat_Acc(formatString: string, start: int := 0, count: int := 0) decreases |formatString| - start ensures countFormat(formatString, start, count) - == countFormat(formatString, start) + count + == countFormat(formatString, start) + count {} lemma splitFormat_countFormat(formatString: string, start: int := 0, pos: int := start) requires 0 <= start <= pos <= |formatString| decreases |formatString| - pos ensures |splitFormat(formatString, start, pos)| - == 1 + countFormat(formatString, pos) + == 1 + countFormat(formatString, pos) { if pos >= |formatString| - 1 { } else if formatString[pos] == '{' && formatString[pos + 1] == '}' { From 17526bb6beb7c9809a78b05754c3704312a4b81f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 12 Sep 2022 11:49:33 -0500 Subject: [PATCH 2/2] Apply the newest formatter --- src/AST/Syntax.dfy | 32 ++-- src/AST/Translator.dfy | 148 ++++++++--------- src/Passes/EliminateNegatedBinops.dfy | 2 +- src/Passes/SimplifyEmptyBlocks.dfy | 2 +- src/REPL/Repl.dfy | 4 +- src/Semantics/Equiv.dfy | 2 +- src/Semantics/Interp.dfy | 230 +++++++++++++------------- src/Semantics/Pure.dfy | 2 +- src/Semantics/Values.dfy | 2 +- src/Transforms/BottomUp.dfy | 2 +- src/Transforms/Generic.dfy | 2 +- src/Utils/StrTree.dfy | 4 +- 12 files changed, 216 insertions(+), 216 deletions(-) diff --git a/src/AST/Syntax.dfy b/src/AST/Syntax.dfy index 81a836cd..98a54120 100644 --- a/src/AST/Syntax.dfy +++ b/src/AST/Syntax.dfy @@ -101,29 +101,29 @@ module Bootstrap.AST.Syntax { datatype Logical = Iff // And, Or, and Imp are in LazyOp datatype Eq = - EqCommon | NeqCommon + EqCommon | NeqCommon datatype Numeric = - Lt | Le | Ge | Gt | Add | Sub | Mul | Div | Mod + Lt | Le | Ge | Gt | Add | Sub | Mul | Div | Mod datatype BV = - LeftShift | RightShift | BitwiseAnd | BitwiseOr | BitwiseXor + LeftShift | RightShift | BitwiseAnd | BitwiseOr | BitwiseXor datatype Char = - LtChar | LeChar | GeChar | GtChar + LtChar | LeChar | GeChar | GtChar datatype Sequences = - SeqEq | SeqNeq | Prefix | ProperPrefix | Concat | InSeq | NotInSeq | - SeqSelect | SeqTake | SeqDrop // Separate nodes in DafnyAST.cs + SeqEq | SeqNeq | Prefix | ProperPrefix | Concat | InSeq | NotInSeq | + SeqSelect | SeqTake | SeqDrop // Separate nodes in DafnyAST.cs datatype Sets = - SetEq | SetNeq | Subset | Superset | ProperSubset | ProperSuperset | - Disjoint | InSet | NotInSet | Union | Intersection | SetDifference + SetEq | SetNeq | Subset | Superset | ProperSubset | ProperSuperset | + Disjoint | InSet | NotInSet | Union | Intersection | SetDifference datatype Multisets = - MultisetEq | MultisetNeq | MultiSubset | MultiSuperset | - ProperMultiSubset | ProperMultiSuperset | MultisetDisjoint | InMultiset | - NotInMultiset | MultisetUnion | MultisetIntersection | MultisetDifference | - MultisetSelect // Separate node in DafnyAST.cs + MultisetEq | MultisetNeq | MultiSubset | MultiSuperset | + ProperMultiSubset | ProperMultiSuperset | MultisetDisjoint | InMultiset | + NotInMultiset | MultisetUnion | MultisetIntersection | MultisetDifference | + MultisetSelect // Separate node in DafnyAST.cs datatype Maps = - MapEq | MapNeq | InMap | NotInMap | MapMerge | MapSubtraction | - MapSelect // Separate node in DafnyAST.cs + MapEq | MapNeq | InMap | NotInMap | MapMerge | MapSubtraction | + MapSelect // Separate node in DafnyAST.cs datatype Datatypes = - RankLt | RankGt + RankLt | RankGt datatype BinaryOp = | Logical(oLogical: Logical) | Eq(oEq: Eq) @@ -144,7 +144,7 @@ module Bootstrap.AST.Syntax { import Types datatype Sequences = - SeqUpdate | SeqSubseq + SeqUpdate | SeqSubseq datatype Multisets = MultisetUpdate datatype Maps = diff --git a/src/AST/Translator.dfy b/src/AST/Translator.dfy index 623d4d5c..0e64e059 100644 --- a/src/AST/Translator.dfy +++ b/src/AST/Translator.dfy @@ -70,8 +70,8 @@ module Bootstrap.AST.Translator { else if ty is C.BitvectorType then var bvTy := ty as C.BitvectorType; :- Need(bvTy.Width >= 0, Invalid("BV width must be >= 0")); - Success(DT.BitVector(bvTy.Width as int)) - // TODO: the following could be simplified + Success(DT.BitVector(bvTy.Width as int)) + // TODO: the following could be simplified else if ty is C.MapType then var ty := ty as C.MapType; assume TypeHeight(ty.Domain) < TypeHeight(ty); @@ -202,13 +202,13 @@ module Bootstrap.AST.Translator { reads * { :- Need(u is C.UnaryOpExpr, UnsupportedExpr(u)); - var u := u as C.UnaryOpExpr; - var op, e := u.ResolvedOp, u.E; - assume Decreases(e, u); - :- Need(op !in GhostUnaryOps, GhostExpr(u)); - :- Need(op in UnaryOpMap.Keys, UnsupportedExpr(u)); - var te :- TranslateExpression(e); - Success(DE.Apply(DE.Eager(DE.UnaryOp(UnaryOpMap[op])), [te])) + var u := u as C.UnaryOpExpr; + var op, e := u.ResolvedOp, u.E; + assume Decreases(e, u); + :- Need(op !in GhostUnaryOps, GhostExpr(u)); + :- Need(op in UnaryOpMap.Keys, UnsupportedExpr(u)); + var te :- TranslateExpression(e); + Success(DE.Apply(DE.Eager(DE.UnaryOp(UnaryOpMap[op])), [te])) } function method TranslateBinary(b: C.BinaryExpr) @@ -221,9 +221,9 @@ module Bootstrap.AST.Translator { assume Decreases(e0, b); assume Decreases(e1, b); :- Need(op in BinaryOpCodeMap, UnsupportedExpr(b)); - var t0 :- TranslateExpression(e0); - var t1 :- TranslateExpression(e1); - Success(DE.Apply(BinaryOpCodeMap[op], [t0, t1])) + var t0 :- TranslateExpression(e0); + var t1 :- TranslateExpression(e1); + Success(DE.Apply(BinaryOpCodeMap[op], [t0, t1])) } function method TranslateLiteral(l: C.LiteralExpr) @@ -240,7 +240,7 @@ module Bootstrap.AST.Translator { var str := TypeConv.AsString(l.Value); if l is C.CharLiteralExpr then :- Need(|str| == 1, Invalid("CharLiteralExpr must contain a single character.")); - Success(DE.Literal(DE.LitChar(str[0]))) + Success(DE.Literal(DE.LitChar(str[0]))) else if l is C.StringLiteralExpr then var sl := l as C.StringLiteralExpr; Success(DE.Literal(DE.LitString(str, sl.IsVerbatim))) @@ -320,10 +320,10 @@ module Bootstrap.AST.Translator { { var ty :- TranslateType(de.Type); :- Need(ty.Collection? && ty.finite, Invalid("`DisplayExpr` must be a finite collection.")); - var elems := ListUtils.ToSeq(de.Elements); - var elems :- Seq.MapResult(elems, e requires e in elems reads * => - assume Decreases(e, de); TranslateExpression(e)); - Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) + var elems := ListUtils.ToSeq(de.Elements); + var elems :- Seq.MapResult(elems, e requires e in elems reads * => + assume Decreases(e, de); TranslateExpression(e)); + Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) } function method TranslateExpressionPair(mde: C.MapDisplayExpr, ep: C.ExpressionPair) @@ -347,11 +347,11 @@ module Bootstrap.AST.Translator { { var ty :- TranslateType(mde.Type); :- Need(ty.Collection? && ty.kind.Map? && ty.finite, Invalid("`MapDisplayExpr` must be a map.")); - var elems := ListUtils.ToSeq(mde.Elements); - var elems :- Seq.MapResult(elems, (ep: C.ExpressionPair) requires ep in elems reads * => - assume Math.Max(ASTHeight(ep.A), ASTHeight(ep.B)) < ASTHeight(mde); - TranslateExpressionPair(mde, ep)); - Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) + var elems := ListUtils.ToSeq(mde.Elements); + var elems :- Seq.MapResult(elems, (ep: C.ExpressionPair) requires ep in elems reads * => + assume Math.Max(ASTHeight(ep.A), ASTHeight(ep.B)) < ASTHeight(mde); + TranslateExpressionPair(mde, ep)); + Success(DE.Apply(DE.Eager(DE.Builtin(DE.Display(ty))), elems)) } function method TranslateSeqSelectExpr(se: C.SeqSelectExpr): (e: TranslationResult) @@ -362,38 +362,38 @@ module Bootstrap.AST.Translator { var ty :- TranslateType(se.Seq.Type); :- Need(ty.Collection? && !ty.kind.Set?, Invalid("`SeqSelect` must be on a map, sequence, or multiset.")); - :- Need(se.SelectOne ==> se.E0 != null && se.E1 == null, - Invalid("Inconsistent values for `SelectOne` and E1 in SeqSelect.")); - :- Need(!se.SelectOne ==> ty.kind.Seq?, - Invalid("`SeqSelect` on a map or multiset must have a single index.")); - assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.E0), ASTHeight(se.E1))) < ASTHeight(se); - var recv :- TranslateExpression(se.Seq); - var eager := (op, args) => Success(DE.Apply(DE.Eager(op), args)); - match ty.kind { // FIXME AST gen should produce `Expression?` not `Expression` - case Seq() => - if se.SelectOne then - assert se.E1 == null; - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqSelect)), [recv, e0]) - else if se.E1 == null then - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqDrop)), [recv, e0]) - else if se.E0 == null then - var e1 :- TranslateExpression(se.E1); - eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqTake)), [recv, e1]) - else - var e0 :- TranslateExpression(se.E0); - var e1 :- TranslateExpression(se.E1); - eager(DE.TernaryOp(DE.TernaryOps.Sequences(DE.TernaryOps.SeqSubseq)), [recv, e0, e1]) - case Map(_) => - assert se.SelectOne && se.E1 == null; - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Maps(DE.BinaryOps.MapSelect)), [recv, e0]) - case Multiset() => - assert se.SelectOne && se.E1 == null; - var e0 :- TranslateExpression(se.E0); - eager(DE.BinaryOp(DE.BinaryOps.Multisets(DE.BinaryOps.MultisetSelect)), [recv, e0]) - } + :- Need(se.SelectOne ==> se.E0 != null && se.E1 == null, + Invalid("Inconsistent values for `SelectOne` and E1 in SeqSelect.")); + :- Need(!se.SelectOne ==> ty.kind.Seq?, + Invalid("`SeqSelect` on a map or multiset must have a single index.")); + assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.E0), ASTHeight(se.E1))) < ASTHeight(se); + var recv :- TranslateExpression(se.Seq); + var eager := (op, args) => Success(DE.Apply(DE.Eager(op), args)); + match ty.kind { // FIXME AST gen should produce `Expression?` not `Expression` + case Seq() => + if se.SelectOne then + assert se.E1 == null; + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqSelect)), [recv, e0]) + else if se.E1 == null then + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqDrop)), [recv, e0]) + else if se.E0 == null then + var e1 :- TranslateExpression(se.E1); + eager(DE.BinaryOp(DE.BinaryOps.Sequences(DE.BinaryOps.SeqTake)), [recv, e1]) + else + var e0 :- TranslateExpression(se.E0); + var e1 :- TranslateExpression(se.E1); + eager(DE.TernaryOp(DE.TernaryOps.Sequences(DE.TernaryOps.SeqSubseq)), [recv, e0, e1]) + case Map(_) => + assert se.SelectOne && se.E1 == null; + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Maps(DE.BinaryOps.MapSelect)), [recv, e0]) + case Multiset() => + assert se.SelectOne && se.E1 == null; + var e0 :- TranslateExpression(se.E0); + eager(DE.BinaryOp(DE.BinaryOps.Multisets(DE.BinaryOps.MultisetSelect)), [recv, e0]) + } } function method TranslateSeqUpdateExpr(se: C.SeqUpdateExpr) @@ -404,15 +404,15 @@ module Bootstrap.AST.Translator { var ty :- TranslateType(se.Type); :- Need(ty.Collection? && ty.kind != DT.Set(), Invalid("`SeqUpdate` must be a map, sequence, or multiset.")); - assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.Index), ASTHeight(se.Value))) < ASTHeight(se); - var tSeq :- TranslateExpression(se.Seq); - var tIndex :- TranslateExpression(se.Index); - var tValue :- TranslateExpression(se.Value); - var op := match ty.kind - case Seq() => DE.TernaryOps.Sequences(DE.TernaryOps.SeqUpdate) - case Map(_) => DE.TernaryOps.Maps(DE.TernaryOps.MapUpdate) - case Multiset() => DE.TernaryOps.Multisets(DE.TernaryOps.MultisetUpdate); - Success(DE.Apply(DE.Eager(DE.TernaryOp(op)), [tSeq, tIndex, tValue])) + assume Math.Max(ASTHeight(se.Seq), Math.Max(ASTHeight(se.Index), ASTHeight(se.Value))) < ASTHeight(se); + var tSeq :- TranslateExpression(se.Seq); + var tIndex :- TranslateExpression(se.Index); + var tValue :- TranslateExpression(se.Value); + var op := match ty.kind + case Seq() => DE.TernaryOps.Sequences(DE.TernaryOps.SeqUpdate) + case Map(_) => DE.TernaryOps.Maps(DE.TernaryOps.MapUpdate) + case Multiset() => DE.TernaryOps.Multisets(DE.TernaryOps.MultisetUpdate); + Success(DE.Apply(DE.Eager(DE.TernaryOp(op)), [tSeq, tIndex, tValue])) } function method TranslateLambdaExpr(le: C.LambdaExpr) @@ -433,17 +433,17 @@ module Bootstrap.AST.Translator { decreases ASTHeight(le), 0 { :- Need(le.Exact, UnsupportedExpr(le)); - var lhss := ListUtils.ToSeq(le.LHSs); - var bvs :- Seq.MapResult(lhss, (pat: C.CasePattern) reads * => - :- Need(pat.Var != null, UnsupportedExpr(le)); - Success(TypeConv.AsString(pat.Var.Name))); - var rhss := ListUtils.ToSeq(le.RHSs); - var elems :- Seq.MapResult(rhss, e requires e in rhss reads * => - assume Decreases(e, le); TranslateExpression(e)); - :- Need(|bvs| == |elems|, UnsupportedExpr(le)); - assume Decreases(le.Body, le); - var body :- TranslateExpression(le.Body); - Success(DE.Bind(bvs, elems, body)) + var lhss := ListUtils.ToSeq(le.LHSs); + var bvs :- Seq.MapResult(lhss, (pat: C.CasePattern) reads * => + :- Need(pat.Var != null, UnsupportedExpr(le)); + Success(TypeConv.AsString(pat.Var.Name))); + var rhss := ListUtils.ToSeq(le.RHSs); + var elems :- Seq.MapResult(rhss, e requires e in rhss reads * => + assume Decreases(e, le); TranslateExpression(e)); + :- Need(|bvs| == |elems|, UnsupportedExpr(le)); + assume Decreases(le.Body, le); + var body :- TranslateExpression(le.Body); + Success(DE.Bind(bvs, elems, body)) } function method TranslateConcreteSyntaxExpression(ce: C.ConcreteSyntaxExpression) diff --git a/src/Passes/EliminateNegatedBinops.dfy b/src/Passes/EliminateNegatedBinops.dfy index 4a0e0154..c04340cc 100644 --- a/src/Passes/EliminateNegatedBinops.dfy +++ b/src/Passes/EliminateNegatedBinops.dfy @@ -1,4 +1,4 @@ - include "../Interop/CSharpDafnyASTModel.dfy" +include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" diff --git a/src/Passes/SimplifyEmptyBlocks.dfy b/src/Passes/SimplifyEmptyBlocks.dfy index f1df3db5..2b64f31a 100644 --- a/src/Passes/SimplifyEmptyBlocks.dfy +++ b/src/Passes/SimplifyEmptyBlocks.dfy @@ -1,4 +1,4 @@ - include "../Interop/CSharpDafnyASTModel.dfy" +include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" diff --git a/src/REPL/Repl.dfy b/src/REPL/Repl.dfy index df82759f..52bcd981 100644 --- a/src/REPL/Repl.dfy +++ b/src/REPL/Repl.dfy @@ -1,4 +1,4 @@ - include "../Semantics/Interp.dfy" +include "../Semantics/Interp.dfy" include "../AST/Syntax.dfy" include "../AST/Translator.dfy" include "../Semantics/Printer.dfy" @@ -221,7 +221,7 @@ module Bootstrap.REPL { var shortName := TypeConv.AsString(input.ShortName); var body :- TranslateBody(input).MapFailure(e => TranslationError(e)); :- Need(Interp.SupportsInterp(body), Unsupported(body)); - Success(Named(fullName, shortName, body)) + Success(Named(fullName, shortName, body)) } method ReadResolve() returns (r: REPLResult>>) diff --git a/src/Semantics/Equiv.dfy b/src/Semantics/Equiv.dfy index f9f056f0..f82bd987 100644 --- a/src/Semantics/Equiv.dfy +++ b/src/Semantics/Equiv.dfy @@ -1,4 +1,4 @@ - include "../Interop/CSharpDafnyASTModel.dfy" +include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" diff --git a/src/Semantics/Interp.dfy b/src/Semantics/Interp.dfy index a96c08e1..361cc9c8 100644 --- a/src/Semantics/Interp.dfy +++ b/src/Semantics/Interp.dfy @@ -1,4 +1,4 @@ - include "../Utils/Library.dfy" +include "../Utils/Library.dfy" include "../AST/Syntax.dfy" include "../AST/Predicates.dfy" include "Values.dfy" @@ -315,7 +315,7 @@ module Bootstrap.Semantics.Interp { reveal SupportsInterp(); var Return(val, ctx) :- InterpExpr(e, env, ctx); :- Need(val.HasType(ty), TypeError(e, val, ty)); - Success(Return(val, ctx)) + Success(Return(val, ctx)) } function method NeedType(e: Expr, val: Value, ty: Type) @@ -442,17 +442,17 @@ module Bootstrap.Semantics.Interp { { match op case BVNot => :- Need(v0.BitVector?, Invalid(expr)); - Success(V.BitVector(v0.width, Math.IntPow(2, v0.width) - 1 - v0.value)) + Success(V.BitVector(v0.width, Math.IntPow(2, v0.width) - 1 - v0.value)) case BoolNot => :- Need(v0.Bool?, Invalid(expr)); - Success(V.Bool(!v0.b)) + Success(V.Bool(!v0.b)) case SeqLength => :- Need(v0.Seq?, Invalid(expr)); - Success(V.Int(|v0.sq|)) + Success(V.Int(|v0.sq|)) case SetCard => :- Need(v0.Set?, Invalid(expr)); - Success(V.Int(|v0.st|)) + Success(V.Int(|v0.st|)) case MultisetCard => :- Need(v0.Multiset?, Invalid(expr)); - Success(V.Int(|v0.ms|)) + Success(V.Int(|v0.ms|)) case MapCard => :- Need(v0.Map?, Invalid(expr)); - Success(V.Int(|v0.m|)) + Success(V.Int(|v0.m|)) } function method {:opaque} InterpBinaryOp(expr: Expr, bop: Syntax.BinaryOp, v0: Value, v1: Value) @@ -464,11 +464,11 @@ module Bootstrap.Semantics.Interp { case Logical(op) => InterpBinaryLogical(expr, op, v0, v1) case Eq(op) => // FIXME which types is this Eq applicable to (vs. the type-specific ones?) :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); - match op { - case EqCommon() => Success(V.Bool(v0 == v1)) - case NeqCommon() => Success(V.Bool(v0 != v1)) - } + :- Need(HasEqValue(v1), Invalid(expr)); + match op { + case EqCommon() => Success(V.Bool(v0 == v1)) + case NeqCommon() => Success(V.Bool(v0 != v1)) + } // case BV(op) => case Char(op) => InterpBinaryChar(expr, op, v0, v1) case Sets(op) => InterpBinarySets(expr, op, v0, v1) @@ -512,7 +512,7 @@ module Bootstrap.Semantics.Interp { function method NeedIntBounds(x: int, low: int, high: int) : PureInterpResult { :- Need(low <= x < high, OutOfIntBounds(x, Some(low), Some(high))); - Success(x) + Success(x) } function method InterpBinaryNumericChar(expr: Expr, bop: Syntax.BinaryOps.Numeric, x1: char, x2: char) @@ -551,24 +551,24 @@ module Bootstrap.Semantics.Interp { : PureInterpResult { :- Need(v0.Bool? && v1.Bool?, Invalid(expr)); - match op - case Iff() => - Success(V.Bool(v0.b <==> v1.b)) + match op + case Iff() => + Success(V.Bool(v0.b <==> v1.b)) } function method InterpBinaryChar(expr: Expr, op: Syntax.BinaryOps.Char, v0: Value, v1: Value) : PureInterpResult { // FIXME eliminate distinction between GtChar and GT? :- Need(v0.Char? && v1.Char?, Invalid(expr)); - match op - case LtChar() => - Success(V.Bool(v0.c < v1.c)) - case LeChar() => - Success(V.Bool(v0.c <= v1.c)) - case GeChar() => - Success(V.Bool(v0.c >= v1.c)) - case GtChar() => - Success(V.Bool(v0.c > v1.c)) + match op + case LtChar() => + Success(V.Bool(v0.c < v1.c)) + case LeChar() => + Success(V.Bool(v0.c <= v1.c)) + case GeChar() => + Success(V.Bool(v0.c >= v1.c)) + case GtChar() => + Success(V.Bool(v0.c > v1.c)) } function method InterpBinarySets(expr: Expr, op: Exprs.BinaryOps.Sets, v0: Value, v1: Value) @@ -578,33 +578,33 @@ module Bootstrap.Semantics.Interp { // equality. match op case SetEq() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st == v1.st)) + Success(V.Bool(v0.st == v1.st)) case SetNeq() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st != v1.st)) + Success(V.Bool(v0.st != v1.st)) case Subset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st <= v1.st)) + Success(V.Bool(v0.st <= v1.st)) case Superset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st >= v1.st)) + Success(V.Bool(v0.st >= v1.st)) case ProperSubset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st < v1.st)) + Success(V.Bool(v0.st < v1.st)) case ProperSuperset() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st > v1.st)) + Success(V.Bool(v0.st > v1.st)) case Disjoint() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Bool(v0.st !! v1.st)) + Success(V.Bool(v0.st !! v1.st)) case Union() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Set(v0.st + v1.st)) + Success(V.Set(v0.st + v1.st)) case Intersection() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Set(v0.st * v1.st)) + Success(V.Set(v0.st * v1.st)) case SetDifference() => :- Need(v0.Set? && v1.Set?, Invalid(expr)); - Success(V.Set(v0.st - v1.st)) + Success(V.Set(v0.st - v1.st)) case InSet() => :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Set?, Invalid(expr)); - Success(V.Bool(v0 in v1.st)) + :- Need(v1.Set?, Invalid(expr)); + Success(V.Bool(v0 in v1.st)) case NotInSet() => :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Set?, Invalid(expr)); - Success(V.Bool(v0 !in v1.st)) + :- Need(v1.Set?, Invalid(expr)); + Success(V.Bool(v0 !in v1.st)) } function method InterpBinaryMultisets(expr: Expr, op: Exprs.BinaryOps.Multisets, v0: Value, v1: Value) @@ -614,37 +614,37 @@ module Bootstrap.Semantics.Interp { // equality. match op // DISCUSS case MultisetEq() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms == v1.ms)) + Success(V.Bool(v0.ms == v1.ms)) case MultisetNeq() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms != v1.ms)) + Success(V.Bool(v0.ms != v1.ms)) case MultiSubset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms <= v1.ms)) + Success(V.Bool(v0.ms <= v1.ms)) case MultiSuperset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms >= v1.ms)) + Success(V.Bool(v0.ms >= v1.ms)) case ProperMultiSubset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms < v1.ms)) + Success(V.Bool(v0.ms < v1.ms)) case ProperMultiSuperset() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms > v1.ms)) + Success(V.Bool(v0.ms > v1.ms)) case MultisetDisjoint() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0.ms !! v1.ms)) + Success(V.Bool(v0.ms !! v1.ms)) case MultisetUnion() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Multiset(v0.ms + v1.ms)) + Success(V.Multiset(v0.ms + v1.ms)) case MultisetIntersection() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Multiset(v0.ms * v1.ms)) + Success(V.Multiset(v0.ms * v1.ms)) case MultisetDifference() => :- Need(v0.Multiset? && v1.Multiset?, Invalid(expr)); - Success(V.Multiset(v0.ms - v1.ms)) + Success(V.Multiset(v0.ms - v1.ms)) case InMultiset() => :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0 in v1.ms)) + :- Need(v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0 in v1.ms)) case NotInMultiset() => :- Need(HasEqValue(v0), Invalid(expr)); - :- Need(v1.Multiset?, Invalid(expr)); - Success(V.Bool(v0 !in v1.ms)) + :- Need(v1.Multiset?, Invalid(expr)); + Success(V.Bool(v0 !in v1.ms)) case MultisetSelect() => :- Need(HasEqValue(v1), Invalid(expr)); - :- Need(v0.Multiset?, Invalid(expr)); - Success(V.Int(v0.ms[v1])) + :- Need(v0.Multiset?, Invalid(expr)); + Success(V.Int(v0.ms[v1])) } function method InterpBinarySequences(expr: Expr, op: Exprs.BinaryOps.Sequences, v0: Value, v1: Value) @@ -658,45 +658,45 @@ module Bootstrap.Semantics.Interp { match op case SeqEq() => :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq == v1.sq)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq == v1.sq)) case SeqNeq() => :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq != v1.sq)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq != v1.sq)) case Prefix() => :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq <= v1.sq)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq <= v1.sq)) case ProperPrefix() => :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.sq < v1.sq)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.sq < v1.sq)) case Concat() => :- Need(v0.Seq? && v1.Seq?, Invalid(expr)); - Success(V.Seq(v0.sq + v1.sq)) + Success(V.Seq(v0.sq + v1.sq)) case InSeq() => :- Need(v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 in v1.sq)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 in v1.sq)) case NotInSeq() => :- Need(v1.Seq?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 !in v1.sq)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 !in v1.sq)) case SeqDrop() => :- NeedValidEndpoint(expr, v0, v1); - Success(V.Seq(v0.sq[v1.i..])) + Success(V.Seq(v0.sq[v1.i..])) case SeqTake() => :- NeedValidEndpoint(expr, v0, v1); - Success(V.Seq(v0.sq[..v1.i])) + Success(V.Seq(v0.sq[..v1.i])) case SeqSelect() => :- NeedValidIndex(expr, v0, v1); - Success(v0.sq[v1.i]) + Success(v0.sq[v1.i]) } function method InterpBinaryMaps(expr: Expr, op: Exprs.BinaryOps.Maps, v0: Value, v1: Value) @@ -707,33 +707,33 @@ module Bootstrap.Semantics.Interp { match op case MapEq() => :- Need(v0.Map? && v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.m == v1.m)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.m == v1.m)) case MapNeq() => :- Need(v0.Map? && v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0.m != v1.m)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0.m != v1.m)) case MapMerge() => :- Need(v0.Map? && v1.Map?, Invalid(expr)); - Success(V.Map(v0.m + v1.m)) + Success(V.Map(v0.m + v1.m)) case MapSubtraction() => :- Need(v0.Map? && v1.Set?, Invalid(expr)); - Success(V.Map(v0.m - v1.st)) + Success(V.Map(v0.m - v1.st)) case InMap() => :- Need(v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 in v1.m)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 in v1.m)) case NotInMap() => :- Need(v1.Map?, Invalid(expr)); - :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality - Success(V.Bool(v0 !in v1.m)) + :- Need(HasEqValue(v0), Invalid(expr)); // We need decidable equality + Success(V.Bool(v0 !in v1.m)) case MapSelect() => :- Need(v0.Map?, Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - :- Need(v1 in v0.m, OutOfMapDomain(v0, v1)); - Success(v0.m[v1]) + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + :- Need(v1 in v0.m, OutOfMapDomain(v0, v1)); + Success(v0.m[v1]) } function method {:opaque} InterpTernaryOp(expr: Expr, top: Syntax.TernaryOp, v0: Value, v1: Value, v2: Value) @@ -770,12 +770,12 @@ module Bootstrap.Semantics.Interp { match op case SeqUpdate() => :- NeedValidIndex(expr, v0, v1); - Success(V.Seq(v0.sq[v1.i := v2])) + Success(V.Seq(v0.sq[v1.i := v2])) case SeqSubseq() => :- NeedValidEndpoint(expr, v0, v2); - :- Need(v1.Int?, Invalid(expr)); - :- Need(0 <= v1.i <= v2.i, OutOfIntBounds(v1.i, Some(0), Some(v2.i))); - Success(V.Seq(v0.sq[v1.i..v2.i])) + :- Need(v1.Int?, Invalid(expr)); + :- Need(0 <= v1.i <= v2.i, OutOfIntBounds(v1.i, Some(0), Some(v2.i))); + Success(V.Seq(v0.sq[v1.i..v2.i])) } function method InterpTernaryMultisets(expr: Expr, op: Syntax.TernaryOps.Multisets, v0: Value, v1: Value, v2: Value) @@ -784,9 +784,9 @@ module Bootstrap.Semantics.Interp { match op case MultisetUpdate() => :- Need(v0.Multiset?, Invalid(expr)); - :- Need(v2.Int? && v2.i >= 0, Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Multiset(v0.ms[v1 := v2.i])) + :- Need(v2.Int? && v2.i >= 0, Invalid(expr)); + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Multiset(v0.ms[v1 := v2.i])) } function method InterpTernaryMaps(expr: Expr, op: Syntax.TernaryOps.Maps, v0: Value, v1: Value, v2: Value) @@ -795,8 +795,8 @@ module Bootstrap.Semantics.Interp { match op case MapUpdate() => :- Need(v0.Map?, Invalid(expr)); - :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality - Success(V.Map(v0.m[v1 := v2])) + :- Need(HasEqValue(v1), Invalid(expr)); // We need decidable equality + Success(V.Map(v0.m[v1 := v2])) } function method {:opaque} InterpDisplay(e: Expr, kind: Types.CollectionKind, argvs: seq) @@ -808,14 +808,14 @@ module Bootstrap.Semantics.Interp { Success(V.Map(m)) case Multiset() => :- Need(forall i | 0 <= i < |argvs| :: HasEqValue(argvs[i]), Invalid(e)); // The elements must have a decidable equality - var v := V.Multiset(multiset(argvs)); - assert WellFormedEqValue(v); // Doesn't work without this assert - Success(v) + var v := V.Multiset(multiset(argvs)); + assert WellFormedEqValue(v); // Doesn't work without this assert + Success(v) case Seq() => Success(V.Seq(argvs)) case Set() => :- Need(forall x | x in argvs :: HasEqValue(x), Invalid(e)); // The elements must have a decidable equality - Success(V.Set(set s | s in argvs)) + Success(V.Set(set s | s in argvs)) } function method InterpMapDisplay(e: Expr, argvs: seq) @@ -829,8 +829,8 @@ module Bootstrap.Semantics.Interp { : PureInterpResult<(EqWV, Value)> { :- Need(argv.Seq? && |argv.sq| == 2, Invalid(e)); - :- Need(HasEqValue(argv.sq[0]), Invalid(e)); - Success((argv.sq[0], argv.sq[1])) + :- Need(HasEqValue(argv.sq[0]), Invalid(e)); + Success((argv.sq[0], argv.sq[1])) } function method AugmentContext(base: Context, vars: seq, vals: seq) @@ -852,13 +852,13 @@ module Bootstrap.Semantics.Interp { decreases env.fuel, e, 0 { :- Need(env.fuel > 0, OutOfFuel(fn)); - :- Need(fn.Closure?, Invalid(e)); - reveal SupportsInterp(); - Predicates.Deep.AllImpliesChildren(fn.body, SupportsInterp1); - :- Need(|fn.vars| == |argvs|, SignatureMismatch(fn.vars, argvs)); - var ctx := State(locals := AugmentContext(fn.ctx, fn.vars, argvs)); - var Return(val, ctx) :- InterpExpr(fn.body, env.(fuel := env.fuel - 1), ctx); - Success(val) + :- Need(fn.Closure?, Invalid(e)); + reveal SupportsInterp(); + Predicates.Deep.AllImpliesChildren(fn.body, SupportsInterp1); + :- Need(|fn.vars| == |argvs|, SignatureMismatch(fn.vars, argvs)); + var ctx := State(locals := AugmentContext(fn.ctx, fn.vars, argvs)); + var Return(val, ctx) :- InterpExpr(fn.body, env.(fuel := env.fuel - 1), ctx); + Success(val) } // TODO(SMH): update this to not enforce the intermediary blocks to evaluate to `Unit`, diff --git a/src/Semantics/Pure.dfy b/src/Semantics/Pure.dfy index e39fffe4..d1c21972 100644 --- a/src/Semantics/Pure.dfy +++ b/src/Semantics/Pure.dfy @@ -1,4 +1,4 @@ - include "../Interop/CSharpDafnyASTModel.dfy" +include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" diff --git a/src/Semantics/Values.dfy b/src/Semantics/Values.dfy index b7dc1c36..de10286f 100644 --- a/src/Semantics/Values.dfy +++ b/src/Semantics/Values.dfy @@ -1,4 +1,4 @@ - include "../AST/Syntax.dfy" +include "../AST/Syntax.dfy" include "../Utils/Library.dfy" module Bootstrap.Semantics.Values { diff --git a/src/Transforms/BottomUp.dfy b/src/Transforms/BottomUp.dfy index 395273e7..762c7345 100644 --- a/src/Transforms/BottomUp.dfy +++ b/src/Transforms/BottomUp.dfy @@ -1,4 +1,4 @@ - include "../Interop/CSharpDafnyASTModel.dfy" +include "../Interop/CSharpDafnyASTModel.dfy" include "../Interop/CSharpInterop.dfy" include "../Interop/CSharpDafnyInterop.dfy" include "../Interop/CSharpDafnyASTInterop.dfy" diff --git a/src/Transforms/Generic.dfy b/src/Transforms/Generic.dfy index 1db81804..a9ea714f 100644 --- a/src/Transforms/Generic.dfy +++ b/src/Transforms/Generic.dfy @@ -1,4 +1,4 @@ - include "../AST/Syntax.dfy" +include "../AST/Syntax.dfy" module Bootstrap.Transforms.Generic { import opened AST.Syntax diff --git a/src/Utils/StrTree.dfy b/src/Utils/StrTree.dfy index 0475adc3..99244466 100644 --- a/src/Utils/StrTree.dfy +++ b/src/Utils/StrTree.dfy @@ -67,14 +67,14 @@ module Utils.StrTree { lemma countFormat_Acc(formatString: string, start: int := 0, count: int := 0) decreases |formatString| - start ensures countFormat(formatString, start, count) - == countFormat(formatString, start) + count + == countFormat(formatString, start) + count {} lemma splitFormat_countFormat(formatString: string, start: int := 0, pos: int := start) requires 0 <= start <= pos <= |formatString| decreases |formatString| - pos ensures |splitFormat(formatString, start, pos)| - == 1 + countFormat(formatString, pos) + == 1 + countFormat(formatString, pos) { if pos >= |formatString| - 1 { } else if formatString[pos] == '{' && formatString[pos + 1] == '}' {