a new reasoner in the C runtime. It supports tabling which makes it decideable for propositional logic. dependent types and high-order types are not supported yet. The generation is still in decreasing probability order

5 files changed, 247 insertions, 143 deletions

diff --git a/src/runtime/c/pgf/data.c b/src/runtime/c/pgf/data.c
index d5607031b..d7a44e31c 100644
--- a/src/runtime/c/pgf/data.c
+++ b/src/runtime/c/pgf/data.c
@@ -181,11 +181,6 @@ GU_DEFINE_TYPE(
 	GU_MEMBER(PgfFunDecl, defns, PgfEquationsM),
 	GU_MEMBER(PgfFunDecl, ep, PgfExprProb));
 
-GU_DEFINE_TYPE(
-	PgfCatFun, struct,
-	GU_MEMBER(PgfCatFun, prob, double),
-	GU_MEMBER(PgfCatFun, fun, PgfCId));
-
 static prob_t inf_prob = INFINITY;
 
 GU_DEFINE_TYPE(prob_t, GuFloating, _);
@@ -196,9 +191,7 @@ GU_DEFINE_TYPE(PgfMetaChildMap, GuMap,
 
 GU_DEFINE_TYPE(
 	PgfCat, struct, 
-	GU_MEMBER(PgfCat, context, PgfHypos),
-	GU_MEMBER(PgfCat, n_functions, GuLength),
-	GU_FLEX_MEMBER(PgfCat, functions, PgfCatFun));
+	GU_MEMBER(PgfCat, context, PgfHypos));
 
 
 GU_DEFINE_TYPE(
diff --git a/src/runtime/c/pgf/data.h b/src/runtime/c/pgf/data.h
index ea87e17c1..f2cbc31cc 100644
--- a/src/runtime/c/pgf/data.h
+++ b/src/runtime/c/pgf/data.h
@@ -131,11 +131,6 @@ struct PgfFunDecl {
 
 extern GU_DECLARE_TYPE(PgfFunDecl, struct);
 
-struct PgfCatFun {
-	double prob;
-	PgfCId fun;
-};
-
 typedef GuMap PgfMetaChildMap;
 extern GU_DECLARE_TYPE(PgfMetaChildMap, GuMap);
 
@@ -147,8 +142,7 @@ struct PgfCat {
 	prob_t meta_token_prob;
 	PgfMetaChildMap* meta_child_probs;
 
-	GuLength n_functions;
-	PgfCatFun functions[]; // XXX: resolve to PgfFunDecl*?
+	GuBuf* functions; // -->PgfFunDecl
 };
 
 
diff --git a/src/runtime/c/pgf/pgf.c b/src/runtime/c/pgf/pgf.c
index 46592fa21..ccee4bf24 100644
--- a/src/runtime/c/pgf/pgf.c
+++ b/src/runtime/c/pgf/pgf.c
@@ -155,10 +155,23 @@ pgf_iter_functions_by_cat(PgfPGF* pgf, PgfCId catname,
 		return;
 	}
 	
-	for (size_t i = 0; i < abscat->n_functions; i++) {
-		fn->fn(fn, &abscat->functions[i].fun, NULL, err);
-		if (!gu_ok(err))
-			return;
+	size_t n_functions = gu_buf_length(abscat->functions);
+	for (size_t i = 0; i < n_functions; i++) {
+		PgfFunDecl* fun =
+			gu_buf_get(abscat->functions, PgfFunDecl*, i);
+		
+		GuVariantInfo i = gu_variant_open(fun->ep.expr);
+		switch (i.tag) {
+		case PGF_EXPR_FUN: {
+			PgfExprFun* efun = i.data;
+			fn->fn(fn, &efun->fun, NULL, err);
+			if (!gu_ok(err))
+				return;
+			break;
+		}
+		default:
+			gu_impossible();
+		}
 	}
 }
 
diff --git a/src/runtime/c/pgf/reader.c b/src/runtime/c/pgf/reader.c
index 30e613217..1f82f8471 100644
--- a/src/runtime/c/pgf/reader.c
+++ b/src/runtime/c/pgf/reader.c
@@ -644,28 +644,42 @@ typedef struct {
 } PgfIndexFn;
 
 static void
-pgf_init_meta_probs(GuMapItor* fn, const void* key, void* value, GuExn* err)
+pgf_read_to_PgfAbstr(GuType* type, PgfReader* rdr, void* to)
 {
-	(void) (err);
-	
-	PgfCId name = *((PgfCId*) key);
-    PgfCat* cat = *((PgfCat**) value);
+	rdr->curr_abstr = to;
+	pgf_read_to_struct(type, rdr, to);
+}
+
+static void*
+pgf_read_new_PgfCat(GuType* type, PgfReader* rdr, GuPool* pool,
+		       size_t* size_out)
+{
+	(void) (type && size_out);
+	PgfCat* cat = gu_new(PgfCat, pool);
 
-    cat->name = name;
+	cat->name = *((PgfCId*) rdr->curr_key);	
 
-    cat->meta_prob = INFINITY;
+	pgf_read_to(rdr, gu_type(PgfHypos), &cat->context);
+
+	cat->meta_prob = INFINITY;
 	cat->meta_token_prob = INFINITY;
     cat->meta_child_probs = NULL;
-}
 
-static void
-pgf_read_to_PgfAbstr(GuType* type, PgfReader* rdr, void* to)
-{
-	rdr->curr_abstr = to;
-	pgf_read_to_struct(type, rdr, to);
+    cat->functions = gu_new_buf(PgfFunDecl*, rdr->opool);
 
-	PgfIndexFn clo = { { pgf_init_meta_probs }, rdr };
-	gu_map_iter(rdr->curr_abstr->cats, &clo.fn, NULL);
+	size_t n_functions = pgf_read_len(rdr);
+	for (size_t i = 0; i < n_functions; i++) {
+		double prob;
+		PgfCId name;
+		pgf_read_to_double(gu_type(double), rdr, &prob);
+		pgf_read_to_GuString(gu_type(PgfCId), rdr, &name);
+		
+		PgfFunDecl* absfun =
+			gu_map_get(rdr->curr_abstr->funs, &name, PgfFunDecl*);
+		gu_buf_push(cat->functions, PgfFunDecl*, absfun);
+	}
+	
+	return cat;
 }
 
 static GU_DEFINE_TYPE(PgfLinDefs, GuIntMap, gu_ptr_type(PgfFunIds),
@@ -880,7 +894,8 @@ pgf_read_new_table = GU_TYPETABLE(
 	PGF_READ_NEW(PgfFunDecl),
 	PGF_READ_NEW(PgfCCat),
 	PGF_READ_NEW(PgfCncCat),
-	PGF_READ_NEW(PgfConcr)
+	PGF_READ_NEW(PgfConcr),
+	PGF_READ_NEW(PgfCat)
 	);
 
 PgfReader*
diff --git a/src/runtime/c/pgf/reasoner.c b/src/runtime/c/pgf/reasoner.c
index 28714a948..07bd3735a 100644
--- a/src/runtime/c/pgf/reasoner.c
+++ b/src/runtime/c/pgf/reasoner.c
@@ -8,23 +8,43 @@
 
 typedef struct PgfExprState PgfExprState;
 
+typedef struct {
+	GuBuf* conts;
+	GuBuf* exprs;
+	prob_t outside_prob;
+} PgfAnswers;
+
 struct PgfExprState {
-	PgfExprState* cont;
-	PgfExpr expr;
+	PgfAnswers* answers;
+	PgfExprProb ep;
 	PgfHypos hypos;
 	size_t arg_idx;
 };
 
+typedef enum {
+	PGF_EXPR_QSTATE_PREDICT,
+	PGF_EXPR_QSTATE_COMBINE1,
+	PGF_EXPR_QSTATE_COMBINE2
+} PGF_EXPR_QSTATE_KIND;
+
 typedef struct {
-	PgfExprState *st;
-	prob_t cont_prob;
-	size_t fun_idx;
-	PgfCat* abscat;
+	prob_t prob;
+	PGF_EXPR_QSTATE_KIND kind;
+	void*  single;
+	size_t choice_idx;
+	GuBuf* choices;
 } PgfExprQState;
 
+static GU_DEFINE_TYPE(PgfAnswers, abstract);
+
+typedef GuStringMap PgfAbswersMap;
+static GU_DEFINE_TYPE(PgfAbswersMap, GuStringMap, gu_ptr_type(PgfAnswers),
+                      &gu_null_struct);
+
 typedef struct {
 	GuPool* tmp_pool;
 	PgfAbstr* abstract;
+	PgfAbswersMap* table;
 	GuBuf* pqueue;
 	PgfExprEnum en;
 } PgfReasoner;
@@ -32,15 +52,12 @@ typedef struct {
 static int
 cmp_expr_qstate(GuOrder* self, const void* a, const void* b)
 {
-	PgfExprQState *q1 = (PgfExprQState *) a;
-	PgfExprQState *q2 = (PgfExprQState *) b;
-
-	prob_t prob1 = q1->cont_prob-log(q1->abscat->functions[q1->fun_idx].prob);
-	prob_t prob2 = q2->cont_prob-log(q2->abscat->functions[q2->fun_idx].prob);
+	PgfExprQState *q1 = *((PgfExprQState **) a);
+	PgfExprQState *q2 = *((PgfExprQState **) b);
 	
-	if (prob1 < prob2)
+	if (q1->prob < q2->prob)
 		return -1;
-	else if (prob1 > prob2)
+	else if (q1->prob > q2->prob)
 		return 1;
 	else
 		return 0;
@@ -56,38 +73,37 @@ pgf_print_expr_state(PgfExprState* st,
 {
 	gu_buf_push(stack, int, (gu_seq_length(st->hypos) - st->arg_idx - 1));
 
-	if (st->cont != NULL)
-		pgf_print_expr_state(st->cont, wtr, err, stack);
+	PgfExprState* cont = gu_buf_get(st->answers->conts, PgfExprState*, 0);
+	if (cont != NULL)
+		pgf_print_expr_state(cont, wtr, err, stack);
 
 	gu_puts(" (", wtr, err);
-	pgf_print_expr(st->expr, 0, wtr, err);
+	pgf_print_expr(st->ep.expr, 0, wtr, err);
 }
 
 static void
-pgf_print_expr_qstate(PgfExprQState* q, PgfAbstr* abstract,
+pgf_print_expr_state0(PgfExprState* st, PgfAbstr* abstract,
                       GuWriter* wtr, GuExn* err, GuPool* tmp_pool)
-{
-	PgfCId fun = q->abscat->functions[q->fun_idx].fun;
-	PgfFunDecl* absfun =
-		gu_map_get(abstract->funs, &fun, PgfFunDecl*);
-	
-	prob_t prob = q->cont_prob+absfun->ep.prob;
+{	
+	prob_t prob = st->answers->outside_prob+st->ep.prob;
 	gu_printf(wtr, err, "[%f]", prob);
-	
-	size_t n_args = gu_seq_length(absfun->type->hypos);
+
+	size_t n_args = gu_seq_length(st->hypos);
 
 	GuBuf* stack = gu_new_buf(int, tmp_pool);
 	if (n_args > 0)
-		gu_buf_push(stack, int, n_args);
+		gu_buf_push(stack, int, gu_seq_length(st->hypos) - st->arg_idx);
 
-	if (q->st != NULL)
-		pgf_print_expr_state(q->st, wtr, err, stack);
+	PgfExprState* cont =
+		gu_buf_get(st->answers->conts, PgfExprState*, 0);
+	if (cont != NULL)
+		pgf_print_expr_state(cont, wtr, err, stack);
 
 	if (n_args > 0)
 		gu_puts(" (", wtr, err);
 	else
 		gu_puts(" ", wtr, err);
-	pgf_print_expr(absfun->ep.expr, 0, wtr, err);
+	pgf_print_expr(st->ep.expr, 0, wtr, err);
 
 	size_t n_counts = gu_buf_length(stack);
 	for (size_t i = 0; i < n_counts; i++) {
@@ -101,107 +117,183 @@ pgf_print_expr_qstate(PgfExprQState* q, PgfAbstr* abstract,
 }
 #endif
 
-static bool
-pgf_reasoner_cat_init(PgfReasoner* rs, 
-                      PgfExprState* cont, prob_t cont_prob, PgfCId cat,
-                      GuPool* pool)
+static PgfExprState*
+pgf_reasoner_combine(PgfReasoner* rs,
+                     PgfExprState* st, PgfExprProb* ep,
+                     GuPool* pool)
 {
-	// Checking for loops in the chart
-	if (cont != NULL) {
-		PgfExprState* st = cont->cont;
-		while (st != NULL) {
-			PgfHypo* hypo = gu_seq_index(st->hypos, PgfHypo, st->arg_idx);
-			if (gu_string_eq(hypo->type->cid, cat))
-				return false;
-
-			st = st->cont;
-		}
-	}
+	PgfExprState* nst = 
+		gu_new(PgfExprState, rs->tmp_pool);
+	nst->answers = st->answers;
+	nst->ep.expr =
+		gu_new_variant_i(pool, PGF_EXPR_APP,
+				PgfExprApp,
+				.fun = st->ep.expr,
+				.arg = ep->expr);
+	nst->ep.prob = st->ep.prob+ep->prob;
+	nst->hypos = st->hypos;
+	nst->arg_idx = st->arg_idx+1;
+	return nst;
+}
 
-	PgfCat* abscat = gu_map_get(rs->abstract->cats, &cat, PgfCat*);
-	if (abscat == NULL) {
-		return false;
+static void
+pgf_reasoner_predict(PgfReasoner* rs, PgfExprState* cont,
+                     prob_t outside_prob, PgfCId cat,
+                     GuPool* pool)
+{
+	PgfAnswers* answers = gu_map_get(rs->table, &cat, PgfAnswers*);
+	if (answers == NULL) {
+		answers = gu_new(PgfAnswers, rs->tmp_pool);
+		answers->conts = gu_new_buf(PgfExprState*, rs->tmp_pool);
+		answers->exprs = gu_new_buf(PgfExprProb*, rs->tmp_pool);
+		answers->outside_prob = outside_prob;
+
+		gu_map_put(rs->table, &cat, PgfAnswers*, answers);
 	}
 
-	if (abscat->n_functions > 0) {
-		PgfExprQState q = {cont, cont_prob, 0, abscat};
-		gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
+	gu_buf_push(answers->conts, PgfExprState*, cont);
+
+	if (gu_buf_length(answers->conts) == 1) {
+		PgfCat* abscat = gu_map_get(rs->abstract->cats, &cat, PgfCat*);
+		if (abscat == NULL) {
+			return;
+		}
+
+		if (gu_buf_length(abscat->functions) > 0) {
+			PgfExprQState *q = gu_new(PgfExprQState, rs->tmp_pool);
+			q->kind = PGF_EXPR_QSTATE_PREDICT;
+			q->single = answers;
+			q->choice_idx = 0;
+			q->choices = abscat->functions;
+
+			q->prob = answers->outside_prob + gu_buf_get(q->choices, PgfFunDecl*, 0)->ep.prob;
+			gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
+		}
+	} else {
+		if (gu_buf_length(answers->exprs) > 0) {
+			PgfExprQState *q = gu_new(PgfExprQState, rs->tmp_pool);
+			q->prob = cont->ep.prob + gu_buf_get(answers->exprs, PgfExprProb*, 0)->prob;
+			q->kind = PGF_EXPR_QSTATE_COMBINE1;
+			q->single = cont;
+			q->choice_idx = 0;
+			q->choices = answers->exprs;
+
+			gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
+		}
 	}
-	return true;
 }
 
 static PgfExprProb*
 pgf_reasoner_next(PgfReasoner* rs, GuPool* pool)
 {
-	if (rs->pqueue == NULL)
+	if (rs->tmp_pool == NULL)
 		return NULL;
 
 	while (gu_buf_length(rs->pqueue) > 0) {
-		PgfExprQState q;
+		PgfExprQState* q;
 		gu_buf_heap_pop(rs->pqueue, &pgf_expr_qstate_order, &q);
 
+		PgfExprState* st = NULL;
+		switch (q->kind) {
+		case PGF_EXPR_QSTATE_PREDICT: {
+			PgfFunDecl* absfun =
+				gu_buf_get(q->choices, PgfFunDecl*, q->choice_idx);
+
+			st = gu_new(PgfExprState, pool);
+			st->answers = q->single;
+			st->ep      = absfun->ep;
+			st->hypos   = absfun->type->hypos;
+			st->arg_idx = 0;
+
+			q->choice_idx++;
+			if (q->choice_idx < gu_buf_length(q->choices)) {
+				q->prob = st->answers->outside_prob + gu_buf_get(q->choices, PgfFunDecl*, q->choice_idx)->ep.prob;
+				gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
+			}
+			break;
+		}
+		case PGF_EXPR_QSTATE_COMBINE1: {
+			PgfExprState* cont = q->single;
+			PgfExprProb* ep =
+				gu_buf_get(q->choices, PgfExprProb*, q->choice_idx);
+			st = pgf_reasoner_combine(rs, cont, ep, pool);
+			
+			q->choice_idx++;
+			if (q->choice_idx < gu_buf_length(q->choices)) {
+				q->prob = cont->ep.prob + gu_buf_get(q->choices, PgfExprProb*, q->choice_idx)->prob;
+				gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
+			}
+			break;
+		}
+		case PGF_EXPR_QSTATE_COMBINE2: {
+			PgfExprState* cont =
+				gu_buf_get(q->choices, PgfExprState*, q->choice_idx);
+			PgfExprProb* ep = q->single;
+			st = pgf_reasoner_combine(rs, cont, ep, pool);
+			
+			q->choice_idx++;
+			if (q->choice_idx < gu_buf_length(q->choices)) {
+				q->prob = ep->prob + gu_buf_get(q->choices, PgfExprState*, q->choice_idx)->ep.prob;
+				gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
+			}
+			break;
+		}
+		default:
+			gu_impossible();
+		}
+		
+
 #ifdef PGF_REASONER_DEBUG
 		{
 			GuPool* tmp_pool = gu_new_pool();
 			GuOut* out = gu_file_out(stderr, tmp_pool);
 			GuWriter* wtr = gu_new_utf8_writer(out, tmp_pool);
 			GuExn* err = gu_exn(NULL, type, tmp_pool);
-			pgf_print_expr_qstate(&q, rs->abstract, wtr, err, tmp_pool);
+			pgf_print_expr_state0(st, rs->abstract, wtr, err, tmp_pool);
 			gu_pool_free(tmp_pool);
 		}
 #endif
 
-		PgfCId fun = q.abscat->functions[q.fun_idx++].fun;
-		PgfFunDecl* absfun =
-			gu_map_get(rs->abstract->funs, &fun, PgfFunDecl*);
+		if (st->arg_idx < gu_seq_length(st->hypos)) {
+			PgfHypo *hypo = gu_seq_index(st->hypos, PgfHypo, st->arg_idx);
+			prob_t outside_prob = 
+				st->ep.prob+st->answers->outside_prob;
+			pgf_reasoner_predict(rs, st, outside_prob,
+								 hypo->type->cid, pool);
+		} else {
+			gu_buf_push(st->answers->exprs, PgfExprProb*, &st->ep);
+
+			PgfExprProb* target = NULL;
+				
+			GuBuf* conts = st->answers->conts;
+			size_t choice_idx = 0;
+			PgfExprState* cont =
+				gu_buf_get(conts, PgfExprState*, 0);
+			if (cont == NULL) {
+				target = &st->ep;
+				cont   = gu_buf_get(conts, PgfExprState*, 1);
+				choice_idx++;
+			}
 
-		if (q.fun_idx < q.abscat->n_functions) {
-			gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
-		}
+			if (choice_idx < gu_buf_length(conts)) {
+				PgfExprQState *q = gu_new(PgfExprQState, rs->tmp_pool);
+				q->prob = st->ep.prob + cont->ep.prob;
+				q->kind = PGF_EXPR_QSTATE_COMBINE2;
+				q->single = &st->ep;
+				q->choice_idx = choice_idx;
+				q->choices = conts;
 
-		if (absfun == NULL)
-			continue;
-
-		PgfExprState *st = gu_new(PgfExprState, rs->tmp_pool);
-		st->cont = q.st;
-		st->expr =
-			gu_new_variant_i(pool, PGF_EXPR_FUN,
-							 PgfExprFun,
-							 .fun = fun);
-		st->hypos = absfun->type->hypos;
-		st->arg_idx = 0;
-
-		for (;;) {
-			prob_t prob = q.cont_prob+absfun->ep.prob;
-
-			if (st->arg_idx < gu_seq_length(st->hypos)) {
-				PgfHypo *hypo = gu_seq_index(st->hypos, PgfHypo, st->arg_idx);
-				pgf_reasoner_cat_init(rs, st, prob,
-									  hypo->type->cid, pool);
-				break;
-			} else {
-				PgfExprState* cont = st->cont;
-				if (cont == NULL) {
-					PgfExprProb* ep = gu_new(PgfExprProb, pool);
-					ep->expr = st->expr;
-					ep->prob = prob;
-					return ep;
-				}
-
-				st->cont = cont->cont;
-				st->expr =
-					gu_new_variant_i(pool, PGF_EXPR_APP,
-							PgfExprApp,
-							.fun = cont->expr, .arg = st->expr);
-				st->hypos = cont->hypos;
-				st->arg_idx = cont->arg_idx+1;
+				gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
 			}
+
+			if (target != NULL)
+				return target;
 		}
 	}
 
 	gu_pool_free(rs->tmp_pool);
 	rs->tmp_pool = NULL;
-	rs->pqueue = NULL;
+	rs->pqueue   = NULL;
 	return NULL;
 }
 
@@ -215,17 +307,14 @@ pgf_reasoner_enum_next(GuEnum* self, void* to, GuPool* pool)
 PgfExprEnum*
 pgf_generate(PgfPGF* pgf, PgfCId cat, GuPool* pool)
 {
-	GuPool* tmp_pool = gu_new_pool();
-	GuBuf* pqueue = gu_new_buf(PgfExprQState, tmp_pool);
-
-	PgfReasoner* rs =
-           gu_new_i(pool, PgfReasoner,
-			 .tmp_pool = tmp_pool,
-             .abstract = &pgf->abstract,
-			 .pqueue = pqueue,
-			 .en.next = pgf_reasoner_enum_next);
-
-	pgf_reasoner_cat_init(rs, NULL, 0, cat, pool);
+	PgfReasoner* rs = gu_new(PgfReasoner, pool);
+	rs->tmp_pool = gu_new_pool(),
+    rs->abstract = &pgf->abstract,
+	rs->table = gu_map_type_new(PgfAbswersMap, rs->tmp_pool),
+	rs->pqueue  = gu_new_buf(PgfExprQState*, rs->tmp_pool);
+	rs->en.next = pgf_reasoner_enum_next;
+
+	pgf_reasoner_predict(rs, NULL, 0, cat, pool);
 
 	return &rs->en;
 }