shithub: lpa

ref: 2b23d05d57743af57385cd42c0fd2d223b11d8c8
dir: /constraint.c/

#include <u.h>
#include <libc.h>
#include <thread.h>

#include "dat.h"
#include "fns.h"

/* monadic constraints */

/* dyadic constraints */
static void constraint_equal(Ast *, Array *, Array *);


Array *
allocvar(char *name)
{
	static int id = 0;

	if(name == nil)
		name = "⎕var";

	ConstraintVar *v = alloc(DataConstraintVar);
	v->name = name;
	v->id = id++;

	Array *a = allocarray(TypeVar, 0, 1);
	setvar(a, 0, v);
	return a;
}

static Ast *
varast(Array *a)
{
	if(a == nil)
		return nil;

	if(gettype(a) == TypeVar && getrank(a) == 0){
		ConstraintVar *v = getvar(a, 0);
		if(v->ast)
			return v->ast;
	}
	Ast *c = alloc(DataAst);
	c->tag = AstConst;
	c->val = a;

	return c;
}

Array *
delayedexpr(int prim, Array *x, Array *y)
{
	Array *a = allocvar(nil);
	ConstraintVar *v = getvar(a, 0);

	Ast *func = alloc(DataAst);
	func->tag = AstPrim;
	func->prim = prim;

	Ast *e = alloc(DataAst);
	v->ast = e;
	e->func = func;
	e->tag = x ? AstDyadic : AstMonadic;
	e->left = varast(x);
	e->right = varast(y);

	return a;
}

void
graphadd(ConstraintGraph *g, Constraint *c)
{
	for(uvlong i = 0; i < g->ccount; i++){
		if(g->cs[i] == c)
			return; /* The constraint is already there. TODO: make a better test */
	}

	if(g->ccount == nelem(g->cs))
		error(EInternal, "not enough space in the constraint graph");
	g->cs[g->ccount] = c;
	g->ccount++;

	for(uvlong i = 0; i < nelem(c->vars); i++){
		ConstraintVar *v = c->vars[i];
		if(v == nil)
			continue;
		int new = 1;
		for(uvlong j = 0; j < g->vcount && new; j++){
			if(g->vs[j] == v)
				new = 0;
		}
		if(!new)
			continue;
		g->vs[g->vcount] = v;
		g->vcount++;
		for(uvlong j = 0; j < v->count; j++)
			graphadd(g, v->constraints[j]);
	}
}

Array *
solve(ConstraintVar *v)
{
	Array *res;

	if(v->ast)
		error(EDomain, "Cannot solve expression. Use ⎕assert first.");

	/* Consider the available constraints on the variable, and find a solutions (just one).
	 * If that isn't possible, fail with some appropriate error.
	 *
	 * There are of course multiple strategies to perform this search, and perhaps it would
	 * make sense if ⎕solve let the user specify one as the left argument.
	 */

	/* Build a graph containing all the variables and constraints involved.
	 * The number of max vars and constraints are fixed for now.
	 */
	ConstraintGraph *g = alloc(DataConstraintGraph);

	for(uvlong i = 0; i < v->count; i++)
		graphadd(g, v->constraints[i]);
	if(g->ccount == 0){
		/* it can have any value */
		res = allocarray(TypeNumber, 0, 1);
		setint(res, 0, 0);
	}else
		error(EInternal, "⎕solve not implemented (%ulld vars and %ulld constraints)", g->vcount, g->ccount);
	return res;
}

void
constrain(ConstraintVar *v)
{
	if(!v->ast)
		error(EDomain, "Expected a constraint expression, not a variable.");

	/* Analyse the AST and add the appropriate constraints to the variables involved.
	 * Also simplify with the constraints already there, and give an error if
	 * the simplifications show that no solutions are possible.
	 */
	int prim, dyadic;
	Array *left = nil;
	Array *right = nil;

	if(!(v->ast->tag == AstMonadic || v->ast->tag == AstDyadic))
		goto fail;
	if(v->ast->func->tag != AstPrim)
		goto fail;
	prim = v->ast->func->prim;
	dyadic = 0;
	switch(v->ast->tag){
	case AstDyadic:
		dyadic = 1;
		if(v->ast->left->tag != AstConst)
			goto fail;
		left = v->ast->left->val;
		/* fall through */
	case AstMonadic:
		if(v->ast->right->tag != AstConst)
			goto fail;
		right = v->ast->right->val;
	}

	switch(prim){
	case PMatch:
		if(dyadic)
			constraint_equal(v->ast, left, right);
		else
			goto fail;
		break;
	default:
		goto fail;
	}
	return;

fail:
	error(EInternal, "don't know how to assert the given constraint");
}

static void
applyconstraint(Constraint *c)
{
	/* Find the variables involved */
	Array *args[2];
	args[0] = c->left;
	args[1] = c->right;
	int nvars = 0;

	for(int i = 0; i < nelem(args); i++){
		Array *a = args[i];
		if(gettype(a) != TypeVar || getrank(a) != 0)
			continue;
		ConstraintVar *v = getvar(a, 0);
		c->vars[nvars] = v;
		nvars++;

		v->count++;
		v->constraints = allocextra(v, sizeof(c) * v->count);
		v->constraints[v->count-1] = c;
	}

	/* Should simplify here as well */
}

/* monadic constraints */

/* dyadic constraints */

static void
constraint_equal(Ast *a, Array *x, Array *y)
{
	Constraint *c = alloc(DataConstraint);
	c->tag = CEqual;
	c->ast = a;
	c->left = x;
	c->right = y;
	applyconstraint(c);
}