Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Formatter Pass #12

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Formatter Pass #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c07a2d1
Formatter Pass
MikaelMayer Sep 8, 2022
17526bb
Apply the newest formatter
MikaelMayer Sep 12, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
332 changes: 166 additions & 166 deletions src/AST/Predicates.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 {}
}
Loading