| // Code generated by running "go generate". DO NOT EDIT. |
| |
| // Copyright 2017 The Wuffs Authors. |
| // |
| // Licensed under the Apache License, Version 2.0 (the "License"); |
| // you may not use this file except in compliance with the License. |
| // You may obtain a copy of the License at |
| // |
| // https://www.apache.org/licenses/LICENSE-2.0 |
| // |
| // Unless required by applicable law or agreed to in writing, software |
| // distributed under the License is distributed on an "AS IS" BASIS, |
| // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| // See the License for the specific language governing permissions and |
| // limitations under the License. |
| |
| package check |
| |
| import ( |
| a "github.com/google/wuffs/lang/ast" |
| t "github.com/google/wuffs/lang/token" |
| ) |
| |
| var reasons = [...]struct { |
| s string |
| r reason |
| }{ |
| |
| {`"a < b: b > a"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| // b > a |
| if err := proveReasonRequirement(q, t.IDXBinaryGreaterThan, xb, xa); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| return nil |
| }}, |
| |
| {`"a < b: a < c; c < b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| // a < c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xa, xc); err != nil { |
| return err |
| } |
| // c < b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a < b: a < c; c == b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| // a < c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xa, xc); err != nil { |
| return err |
| } |
| // c == b |
| if err := proveReasonRequirement(q, t.IDXBinaryEqEq, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a < b: a == c; c < b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| // a == c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryEqEq, xa, xc); err != nil { |
| return err |
| } |
| // c < b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a < b: a < c; c <= b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| // a < c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xa, xc); err != nil { |
| return err |
| } |
| // c <= b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a < b: a <= c; c < b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| // a <= c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xa, xc); err != nil { |
| return err |
| } |
| // c < b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a > b: b < a"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryGreaterThan { |
| return errFailed |
| } |
| // b < a |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xb, xa); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| return nil |
| }}, |
| |
| {`"a <= b: a == b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessEq { |
| return errFailed |
| } |
| // a == b |
| if err := proveReasonRequirement(q, t.IDXBinaryEqEq, xa, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| return nil |
| }}, |
| |
| {`"a <= b: b >= a"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessEq { |
| return errFailed |
| } |
| // b >= a |
| if err := proveReasonRequirement(q, t.IDXBinaryGreaterEq, xb, xa); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| return nil |
| }}, |
| |
| {`"a <= b: a <= c; c <= b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessEq { |
| return errFailed |
| } |
| // a <= c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xa, xc); err != nil { |
| return err |
| } |
| // c <= b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a <= b: a <= c; c == b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessEq { |
| return errFailed |
| } |
| // a <= c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xa, xc); err != nil { |
| return err |
| } |
| // c == b |
| if err := proveReasonRequirement(q, t.IDXBinaryEqEq, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a <= b: a == c; c <= b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessEq { |
| return errFailed |
| } |
| // a == c |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| if err := proveReasonRequirement(q, t.IDXBinaryEqEq, xa, xc); err != nil { |
| return err |
| } |
| // c <= b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xc, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a >= b: a == b"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryGreaterEq { |
| return errFailed |
| } |
| // a == b |
| if err := proveReasonRequirement(q, t.IDXBinaryEqEq, xa, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| return nil |
| }}, |
| |
| {`"a >= b: b <= a"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryGreaterEq { |
| return errFailed |
| } |
| // b <= a |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xb, xa); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| return nil |
| }}, |
| |
| {`"a >= b: a >= (b + c); 0 <= c"`, func(q *checker, n *a.Assert) error { |
| op, xa, xb := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryGreaterEq { |
| return errFailed |
| } |
| // a >= (b + c) |
| xc := argValue(q.tm, n.Args(), "c") |
| if xc == nil { |
| return errFailed |
| } |
| t0 := a.NewExpr(0, t.IDXBinaryPlus, 0, xb.AsNode(), nil, xc.AsNode(), nil) |
| if err := proveReasonRequirement(q, t.IDXBinaryGreaterEq, xa, t0); err != nil { |
| return err |
| } |
| // 0 <= c |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, zeroExpr, xc); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a < (b + c): a < c; 0 <= b"`, func(q *checker, n *a.Assert) error { |
| op, xa, t0 := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| op, xb, xc := parseBinaryOp(t0) |
| if op != t.IDXBinaryPlus { |
| return errFailed |
| } |
| // a < c |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xa, xc); err != nil { |
| return err |
| } |
| // 0 <= b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, zeroExpr, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"a < (b + c): a < (b0 + c0); b0 <= b; c0 <= c"`, func(q *checker, n *a.Assert) error { |
| op, xa, t0 := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| op, xb, xc := parseBinaryOp(t0) |
| if op != t.IDXBinaryPlus { |
| return errFailed |
| } |
| // a < (b0 + c0) |
| xb0 := argValue(q.tm, n.Args(), "b0") |
| if xb0 == nil { |
| return errFailed |
| } |
| xc0 := argValue(q.tm, n.Args(), "c0") |
| if xc0 == nil { |
| return errFailed |
| } |
| t1 := a.NewExpr(0, t.IDXBinaryPlus, 0, xb0.AsNode(), nil, xc0.AsNode(), nil) |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xa, t1); err != nil { |
| return err |
| } |
| // b0 <= b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xb0, xb); err != nil { |
| return err |
| } |
| // c0 <= c |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xc0, xc); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xb0 |
| _ = xc |
| _ = xc0 |
| return nil |
| }}, |
| |
| {`"a <= (a + b): 0 <= b"`, func(q *checker, n *a.Assert) error { |
| op, xa, t0 := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessEq { |
| return errFailed |
| } |
| op, xa, xb := parseBinaryOp(t0) |
| if op != t.IDXBinaryPlus { |
| return errFailed |
| } |
| // 0 <= b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, zeroExpr, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| return nil |
| }}, |
| |
| {`"(a + b) <= c: a <= (c - b)"`, func(q *checker, n *a.Assert) error { |
| op, t0, xc := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessEq { |
| return errFailed |
| } |
| op, xa, xb := parseBinaryOp(t0) |
| if op != t.IDXBinaryPlus { |
| return errFailed |
| } |
| // a <= (c - b) |
| t1 := a.NewExpr(0, t.IDXBinaryMinus, 0, xc.AsNode(), nil, xb.AsNode(), nil) |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xa, t1); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| |
| {`"(a - b) < c: a < c; 0 <= b"`, func(q *checker, n *a.Assert) error { |
| op, t0, xc := parseBinaryOp(n.Condition()) |
| if op != t.IDXBinaryLessThan { |
| return errFailed |
| } |
| op, xa, xb := parseBinaryOp(t0) |
| if op != t.IDXBinaryMinus { |
| return errFailed |
| } |
| // a < c |
| if err := proveReasonRequirement(q, t.IDXBinaryLessThan, xa, xc); err != nil { |
| return err |
| } |
| // 0 <= b |
| if err := proveReasonRequirement(q, t.IDXBinaryLessEq, zeroExpr, xb); err != nil { |
| return err |
| } |
| _ = xa |
| _ = xb |
| _ = xc |
| return nil |
| }}, |
| } |