Function makeQuantifier

parser/macro.go:558–595

(kind quantifierKind, eh ExprHelper, target ast.Expr, args []ast.Expr)

}

func makeQuantifier(kind quantifierKind, eh ExprHelper, target ast.Expr, args []ast.Expr) (ast.Expr, *common.Error) {
	v, found := extractIdent(args[0])
	if !found {
		return nil, eh.NewError(args[0].ID(), "argument must be a simple name")
	}
	accu := eh.AccuIdentName()
	if v == accu || v == AccumulatorName {
		return nil, eh.NewError(args[0].ID(), "iteration variable overwrites accumulator variable")
	}

	var init ast.Expr
	var condition ast.Expr
	var step ast.Expr
	var result ast.Expr
	switch kind {
	case quantifierAll:
		init = eh.NewLiteral(types.True)
		condition = eh.NewCall(operators.NotStrictlyFalse, eh.NewAccuIdent())
		step = eh.NewCall(operators.LogicalAnd, eh.NewAccuIdent(), args[1])
		result = eh.NewAccuIdent()
	case quantifierExists:
		init = eh.NewLiteral(types.False)
		condition = eh.NewCall(
			operators.NotStrictlyFalse,
			eh.NewCall(operators.LogicalNot, eh.NewAccuIdent()))
		step = eh.NewCall(operators.LogicalOr, eh.NewAccuIdent(), args[1])
		result = eh.NewAccuIdent()
	case quantifierExistsOne:
		init = eh.NewLiteral(types.Int(0))
		condition = eh.NewLiteral(types.True)
		step = eh.NewCall(operators.Conditional, args[1],
			eh.NewCall(operators.Add, eh.NewAccuIdent(), eh.NewLiteral(types.Int(1))), eh.NewAccuIdent())
		result = eh.NewCall(operators.Equals, eh.NewAccuIdent(), eh.NewLiteral(types.Int(1)))
	default:
		return nil, eh.NewError(args[0].ID(), fmt.Sprintf("unrecognized quantifier '%v'", kind))
	}
	return eh.NewComprehension(target, v, accu, init, condition, step, result), nil
}

func extractIdent(e ast.Expr) (string, bool) {
	switch e.Kind() {