linearization for HOAS trees. It should word but we need a type checker in order to test it properly

1 files changed, 180 insertions, 18 deletions

diff --git a/src/runtime/c/pgf/linearizer.c b/src/runtime/c/pgf/linearizer.c
index 8bb685724..796dc24c1 100644
--- a/src/runtime/c/pgf/linearizer.c
+++ b/src/runtime/c/pgf/linearizer.c
@@ -90,51 +90,85 @@ typedef struct {
 	PgfCCat* ccat;
 	PgfCncFun* fun;
 	int fid;
-	GuLength n_args;
+
+	size_t n_vars;
+	PgfPrintContext* context;
+
+	size_t n_args;
 	PgfCncTree args[];
 } PgfCncTreeApp;
 
 typedef struct {
+	size_t n_vars;
+	PgfPrintContext* context;
+
 	GuLength n_args;
 	PgfCncTree args[];
 } PgfCncTreeChunks;
 
 typedef struct {
+	size_t n_vars;
+	PgfPrintContext* context;
+
 	int fid;
 	PgfLiteral lit;
 } PgfCncTreeLit;
 
 #ifdef PGF_LINEARIZER_DEBUG
 void
+pgf_print_cnc_tree_vars(size_t n_vars, PgfPrintContext* context,
+                        GuOut* out, GuExn* err)
+{
+	if (n_vars > 0) {
+		gu_putc('\\', out, err);
+		for (;;) {
+			gu_string_write(context->name, out, err);
+			n_vars--;
+
+			if (n_vars > 0)
+				gu_putc(',', out, err);
+			else
+				break;
+		}
+		gu_puts(" -> ", out, err);
+	}
+}
+
+void
 pgf_print_cnc_tree(PgfCncTree ctree, GuOut* out, GuExn* err)
 {
 	GuVariantInfo ti = gu_variant_open(ctree);
 	switch (ti.tag) {
 	case PGF_CNC_TREE_APP: {
 		PgfCncTreeApp* capp = ti.data;
-		if (capp->n_args > 0) gu_putc('(', out, err);
+		if (capp->n_vars+capp->n_args > 0) gu_putc('(', out, err);
+		pgf_print_cnc_tree_vars(capp->n_vars, capp->context, out, err);
 		gu_printf(out, err, "F%d", capp->fun->funid);
 		for (size_t i = 0; i < capp->n_args; i++) {
 			gu_putc(' ', out, err);
 			pgf_print_cnc_tree(capp->args[i], out, err);
 		}
-		if (capp->n_args > 0) gu_putc(')', out, err);
+		if (capp->n_vars+capp->n_args > 0) gu_putc(')', out, err);
 		break;
 	}
 	case PGF_CNC_TREE_CHUNKS: {
 		PgfCncTreeChunks* chunks = ti.data;
-		if (chunks->n_args > 0) gu_putc('(', out, err);
+		if (chunks->n_vars+chunks->n_args > 0) gu_putc('(', out, err);
+		pgf_print_cnc_tree_vars(chunks->n_vars, chunks->context, out, err);
 		gu_putc('?', out, err);
 		for (size_t i = 0; i < chunks->n_args; i++) {
 			gu_putc(' ', out, err);
 			pgf_print_cnc_tree(chunks->args[i], out, err);
 		}
-		if (chunks->n_args > 0) gu_putc(')', out, err);
+		if (chunks->n_vars+chunks->n_args > 0) gu_putc(')', out, err);
 		break;
 	}
 	case PGF_CNC_TREE_LIT: {
 		PgfCncTreeLit* clit = ti.data;
+		if (clit->n_vars > 0) gu_putc('(', out, err);
+		pgf_print_cnc_tree_vars(clit->n_vars, clit->context, out, err);
 		pgf_print_literal(clit->lit, out, err);
+		if (clit->n_vars > 0) gu_putc(')', out, err);
 		break;
 	}
 	case GU_VARIANT_NULL:
@@ -147,10 +181,16 @@ pgf_print_cnc_tree(PgfCncTree ctree, GuOut* out, GuExn* err)
 #endif
 
 static PgfCncTree
-pgf_lzn_resolve(PgfLzn* lzn, PgfExpr expr, PgfCCat* ccat, GuPool* pool);
+pgf_lzn_resolve(PgfLzn* lzn, 
+                PgfPrintContext* context, PgfExpr expr,
+                PgfCCat* ccat,
+                GuPool* pool);
 
 static PgfCncTree
-pgf_lzn_resolve_app(PgfLzn* lzn, PgfCCat* ccat, GuBuf* buf, GuBuf* args, GuPool* pool)
+pgf_lzn_resolve_app(PgfLzn* lzn,
+                    size_t n_vars, PgfPrintContext* context,
+                    PgfCCat* ccat, GuBuf* buf, GuBuf* args,
+                    GuPool* pool)
 {
 	GuChoiceMark mark = gu_choice_mark(lzn->ch);
 	int save_fid = lzn->fid;
@@ -162,6 +202,9 @@ pgf_lzn_resolve_app(PgfLzn* lzn, PgfCCat* ccat, GuBuf* buf, GuBuf* args, GuPool*
 		gu_new_flex_variant(PGF_CNC_TREE_APP,
 							PgfCncTreeApp,
 							args, n_args, &ret, pool);
+	capp->ccat    = ccat;
+	capp->n_vars  = n_vars;
+	capp->context = context;
 
 redo:;
 	int index = gu_choice_next(lzn->ch, gu_buf_length(buf));
@@ -173,7 +216,6 @@ redo:;
 		gu_buf_get(buf, PgfProductionApply*, index);
 	gu_assert(n_args == gu_seq_length(papply->args));
 
-	capp->ccat= ccat;
 	capp->fun = papply->fun;
 	capp->fid = 0;
 	capp->n_args = n_args;
@@ -203,7 +245,7 @@ redo:;
 		}
 
 		capp->args[i] =
-			pgf_lzn_resolve(lzn, earg, ccat, pool);
+			pgf_lzn_resolve(lzn, context, earg, ccat, pool);
 		if (gu_variant_is_null(capp->args[i])) {
 			lzn->fid = save_fid;
 			gu_choice_reset(lzn->ch, mark);
@@ -219,7 +261,9 @@ redo:;
 }
 
 static PgfCncTree
-pgf_lzn_resolve_def(PgfLzn* lzn, PgfCCat* ccat, GuString s, GuPool* pool)
+pgf_lzn_resolve_def(PgfLzn* lzn,
+                    size_t n_vars, PgfPrintContext* context,
+                    PgfCCat* ccat, GuString s, GuPool* pool)
 {
 	PgfCncTree lit = gu_null_variant;
 	PgfCncTree ret = gu_null_variant;
@@ -228,6 +272,8 @@ pgf_lzn_resolve_def(PgfLzn* lzn, PgfCCat* ccat, GuString s, GuPool* pool)
 		gu_new_variant(PGF_CNC_TREE_LIT,
 					   PgfCncTreeLit,
 					   &lit, pool);
+	clit->n_vars  = 0;
+	clit->context = context;
 	clit->fid = lzn->fid++;
 	PgfLiteralStr* lit_str =
 		gu_new_flex_variant(PGF_LITERAL_STR,
@@ -251,7 +297,9 @@ pgf_lzn_resolve_def(PgfLzn* lzn, PgfCCat* ccat, GuString s, GuPool* pool)
 	capp->ccat = ccat;
 	capp->fun = gu_seq_get(ccat->lindefs, PgfCncFun*, index);
 	capp->fid = lzn->fid++;
-	capp->n_args = 1;
+	capp->n_vars  = n_vars;
+	capp->context = context;
+	capp->n_args  = 1;
 	capp->args[0] = lit;
 
 	return ret;
@@ -298,6 +346,8 @@ pgf_lzr_wrap_linref(PgfCncTree ctree, GuPool* pool)
 		new_capp->ccat    = NULL;
 		new_capp->fun     = gu_seq_get(capp->ccat->linrefs, PgfCncFun*, 0);
 		new_capp->fid     = -1;
+		new_capp->n_vars  = 0;
+		new_capp->context = NULL;
 		new_capp->n_args  = 1;
 		new_capp->args[0] = ctree;
 
@@ -310,15 +360,32 @@ pgf_lzr_wrap_linref(PgfCncTree ctree, GuPool* pool)
 }
 
 static PgfCncTree
-pgf_lzn_resolve(PgfLzn* lzn, PgfExpr expr, PgfCCat* ccat, GuPool* pool)
+pgf_lzn_resolve(PgfLzn* lzn, 
+                PgfPrintContext* context, PgfExpr expr,
+                PgfCCat* ccat, 
+                GuPool* pool)
 {
 	PgfCncTree ret = gu_null_variant;
 	GuPool* tmp_pool = gu_new_pool();
+	size_t n_vars = 0;
 	GuBuf* args = gu_new_buf(PgfExpr, tmp_pool);
 
 	for (;;) {
 		GuVariantInfo i = gu_variant_open(expr);
 		switch (i.tag) {
+		case PGF_EXPR_ABS: {
+			PgfExprAbs* eabs = i.data;
+
+			PgfPrintContext* new_context = gu_new(PgfPrintContext, pool);
+			new_context->name = eabs->id;
+			new_context->next = context;
+			context = new_context;
+			
+			n_vars++;
+			
+			expr = eabs->body;
+			break;
+		}
 		case PGF_EXPR_APP: {
 			PgfExprApp* eapp = i.data;
 			gu_buf_push(args, PgfExpr, eapp->arg);
@@ -331,6 +398,8 @@ pgf_lzn_resolve(PgfLzn* lzn, PgfExpr expr, PgfCCat* ccat, GuPool* pool)
 				gu_new_variant(PGF_CNC_TREE_LIT,
 				               PgfCncTreeLit,
 				               &ret, pool);
+			clit->n_vars  = n_vars;
+			clit->context = context;
 			clit->fid = lzn->fid++;
 			clit->lit = elit->lit;
 			goto done;
@@ -343,11 +412,13 @@ pgf_lzn_resolve(PgfLzn* lzn, PgfExpr expr, PgfCCat* ccat, GuPool* pool)
 				gu_new_flex_variant(PGF_CNC_TREE_CHUNKS,
 				                    PgfCncTreeChunks,
 				                    args, n_args, &chunks_tree, pool);
+			chunks->n_vars  = n_vars;
+			chunks->context = context;
 			chunks->n_args = n_args;
 
 			for (size_t i = 0; i < n_args; i++) {
 				PgfExpr earg = gu_buf_get(args, PgfExpr, n_args-i-1);
-				chunks->args[i] = pgf_lzn_resolve(lzn, earg, NULL, pool);
+				chunks->args[i] = pgf_lzn_resolve(lzn, context, earg, NULL, pool);
 				if (gu_variant_is_null(chunks->args[i])) {
 					ret = gu_null_variant;
 					goto done;
@@ -376,6 +447,8 @@ pgf_lzn_resolve(PgfLzn* lzn, PgfExpr expr, PgfCCat* ccat, GuPool* pool)
 			capp->ccat = ccat;
 			capp->fun = gu_seq_get(ccat->lindefs, PgfCncFun*, index);
 			capp->fid = lzn->fid++;
+			capp->n_vars = 0;
+			capp->context = context;
 			capp->n_args = 1;
 			capp->args[0] = chunks_tree;
 
@@ -402,12 +475,14 @@ pgf_lzn_resolve(PgfLzn* lzn, PgfExpr expr, PgfCCat* ccat, GuPool* pool)
 				GuString s = gu_string_buf_freeze(sbuf, tmp_pool);
 
 				if (ccat != NULL) {
-					ret = pgf_lzn_resolve_def(lzn, ccat, s, pool);
+					ret = pgf_lzn_resolve_def(lzn, n_vars, context, ccat, s, pool);
 				} else {
 					PgfCncTreeLit* clit = 
 						gu_new_variant(PGF_CNC_TREE_LIT,
 									   PgfCncTreeLit,
 									   &ret, pool);
+					clit->n_vars = 0;
+					clit->context = context;
 					clit->fid = lzn->fid++;
 					PgfLiteralStr* lit = 
 						gu_new_flex_variant(PGF_LITERAL_STR,
@@ -435,7 +510,7 @@ redo:;
 				gu_map_iter(overl_table, &clo.fn, NULL);
 				assert(clo.ccat != NULL && clo.buf != NULL);
 
-				ret = pgf_lzn_resolve_app(lzn, clo.ccat, clo.buf, args, pool);
+				ret = pgf_lzn_resolve_app(lzn, n_vars, context, clo.ccat, clo.buf, args, pool);
 				if (gu_variant_is_null(ret)) {
 					gu_choice_reset(lzn->ch, mark);
 					if (gu_choice_advance(lzn->ch))
@@ -448,8 +523,43 @@ redo:;
 					goto done;
 				}
 
-				ret = pgf_lzn_resolve_app(lzn, ccat, buf, args, pool);
+				ret = pgf_lzn_resolve_app(lzn, n_vars, context, ccat, buf, args, pool);
+			}
+			goto done;
+		}
+		case PGF_EXPR_VAR: {
+			PgfExprVar* evar = i.data;
+			
+			int index = evar->var;
+			PgfPrintContext* ctxt = context;
+			while (index > 0) {
+				assert (ctxt != NULL);
+				ctxt = ctxt->next;
+				index--;
+			}
+
+			if (ccat != NULL && ccat->lindefs == NULL) {
+				goto done;
+			}
+
+			if (ccat != NULL) {
+				ret = pgf_lzn_resolve_def(lzn, n_vars, context, ccat, ctxt->name, pool);
+			} else {
+				PgfCncTreeLit* clit = 
+					gu_new_variant(PGF_CNC_TREE_LIT,
+								   PgfCncTreeLit,
+								   &ret, pool);
+				clit->n_vars  = 0;
+				clit->context = context;
+				clit->fid = lzn->fid++;
+				PgfLiteralStr* lit = 
+					gu_new_flex_variant(PGF_LITERAL_STR,
+								        PgfLiteralStr,
+								        val, strlen(ctxt->name)+1,
+								        &clit->lit, pool);
+				strcpy(lit->val, ctxt->name);
 			}
+
 			goto done;
 		}
 		case PGF_EXPR_TYPED: {
@@ -486,7 +596,7 @@ pgf_cnc_tree_enum_next(GuEnum* self, void* to, GuPool* pool)
 	lzn->fid = 0;
 
 	GuChoiceMark mark = gu_choice_mark(lzn->ch);
-	*toc = pgf_lzn_resolve(lzn, lzn->expr, NULL, pool);
+	*toc = pgf_lzn_resolve(lzn, NULL, lzn->expr, NULL, pool);
 	gu_choice_reset(lzn->ch, mark);
 
 #ifdef PGF_LINEARIZER_DEBUG
@@ -520,6 +630,48 @@ pgf_lzr_concretize(PgfConcr* concr, PgfExpr expr, GuPool* pool)
 }
 
 void
+pgf_lzr_linearize_var(PgfConcr* concr, PgfCncTree ctree, size_t var_idx, PgfLinFuncs** fnsp)
+{
+	GuVariantInfo cti = gu_variant_open(ctree);
+
+	size_t n_vars = 0;
+	PgfPrintContext* context = NULL;
+	
+	switch (cti.tag) {
+	case PGF_CNC_TREE_APP: {
+		PgfCncTreeApp* fapp = cti.data;
+		n_vars  = fapp->n_vars;
+		context = fapp->context;
+		break;
+	}
+	case PGF_CNC_TREE_CHUNKS: {
+		PgfCncTreeChunks* fchunks = cti.data;
+		n_vars  = fchunks->n_vars;
+		context = fchunks->context;
+		break;
+	}
+	case PGF_CNC_TREE_LIT: {
+		PgfCncTreeLit* flit = cti.data;
+		n_vars  = flit->n_vars;
+		context = flit->context;
+		break;
+	}
+	default:
+		gu_impossible();
+	}
+
+	n_vars -= var_idx+1;
+	while (n_vars > 0) {
+		context = context->next;
+		n_vars--;
+	}
+
+	if ((*fnsp)->symbol_token) {
+		(*fnsp)->symbol_token(fnsp, context->name);
+	}
+}
+
+void
 pgf_lzr_linearize_symbols(PgfConcr* concr, PgfCncTreeApp* fapp,
                           PgfSymbols* syms, uint16_t sym_idx,
                           PgfLinFuncs** fnsp)
@@ -530,7 +682,6 @@ pgf_lzr_linearize_symbols(PgfConcr* concr, PgfCncTreeApp* fapp,
 		GuVariantInfo sym_i = gu_variant_open(sym);
 		switch (sym_i.tag) {
 		case PGF_SYMBOL_CAT:
-		case PGF_SYMBOL_VAR:
 		case PGF_SYMBOL_LIT: {
 			if (fapp == NULL)
 				return;
@@ -542,6 +693,17 @@ pgf_lzr_linearize_symbols(PgfConcr* concr, PgfCncTreeApp* fapp,
 			pgf_lzr_linearize(concr, argf, sidx->r, fnsp);
 			break;
 		}
+		case PGF_SYMBOL_VAR: {
+			if (fapp == NULL)
+				return;
+
+			PgfSymbolIdx* sidx = sym_i.data;
+			gu_assert((unsigned) sidx->d < fapp->n_args);
+
+			PgfCncTree argf = fapp->args[sidx->d];
+			pgf_lzr_linearize_var(concr, argf, sidx->r, fnsp);
+			break;
+		}
 		case PGF_SYMBOL_KS: {
 			PgfSymbolKS* ks = sym_i.data;
 			if ((*fnsp)->symbol_token) {