lang/check/data.go

// 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: 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: 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 + 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, 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, 0, xc.AsNode(), nil, xb.AsNode(), nil)
		if err := proveReasonRequirement(q, t.IDXBinaryLessEq, xa, t1); err != nil {
			return err
		}
		_ = xa
		_ = xb
		_ = xc
		return nil
	}},
}