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

2026-04-29 06:22:51 -06:00 · 2013-01-07 12:50:32 +00:00
parent cade578d04
commit 2c169406fc
5 changed files with 250 additions and 146 deletions
--- 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;
+	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;
+}

-			st = st->cont;
+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);
+	}
+
+	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);
 		}
 	}
-
-	PgfCat* abscat = gu_map_get(rs->abstract->cats, &cat, PgfCat*);
-	if (abscat == NULL) {
-		return false;
-	}
-
-	if (abscat->n_functions > 0) {
-		PgfExprQState q = {cont, cont_prob, 0, abscat};
-		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);

-		if (q.fun_idx < q.abscat->n_functions) {
-			gu_buf_heap_push(rs->pqueue, &pgf_expr_qstate_order, &q);
-		}
-
-		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;
+			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 (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;
+
+				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(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;

-	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);
+	pgf_reasoner_predict(rs, NULL, 0, cat, pool);

 	return &rs->en;
 }