From e65edab12d96f0c78e7a5a32e674c7f932d05695 Mon Sep 17 00:00:00 2001 From: admin Date: Fri, 18 Oct 2024 20:32:07 -0400 Subject: [PATCH] =?utf8?q?Improve=20rule=20creation=20=E2=80=94=20especial?= =?utf8?q?ly=20replacements?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- src/v.c | 1473 +++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 1042 insertions(+), 431 deletions(-) diff --git a/src/v.c b/src/v.c index bb12bb3..c76e252 100644 --- a/src/v.c +++ b/src/v.c @@ -22,8 +22,8 @@ #include #include -#define PAIR_BW 1 -#define PAIR_WB 2 +#define PAIR_NORMAL 1 +#define PAIR_INVERSE 2 #define PAIR_HL 3 #define PAIR_SUCCESS 4 #define PAIR_ERROR 5 @@ -36,10 +36,18 @@ #define HYPOTHESES_SPACING 4 #define EMPTY_SLOT "█" -enum ui_state +enum ui_major_mode { - uis_splash, - uis_workspace, + uimam_splash, + uimam_workspace, + uimam_help, + }; + +enum ui_minor_mode + { + uimim_esc, + uimim_backslash, + uimim_default, }; enum slot_type @@ -51,9 +59,15 @@ enum slot_type st_ctx_dots, st_ctx_r, st_thesis, - st_a, - st_b, - st_c, + st_generic_thesis, + st_type_thesis, + st_element_thesis_element, + st_element_thesis_type, + st_type_equal_thesis_type_1, + st_type_equal_thesis_type_2, + st_element_equal_thesis_element_1, + st_element_equal_thesis_element_2, + st_element_equal_thesis_type, st_rule_name, }; @@ -86,7 +100,8 @@ enum name_kind nk_variable, nk_element, nk_type, - nk_generic_context, + nk_generic_context_left, + nk_generic_context_right, nk_generic_thesis, }; @@ -109,13 +124,7 @@ struct name struct reference { struct name *origin; - GSList *replacements; /* wraps */ -}; - -struct vdecl -{ - struct name *elem; - struct wrap *type; + GSList *replacements; /* references */ }; struct judgment @@ -125,7 +134,7 @@ struct judgment struct wrap *generic_r; struct wrap *a; struct wrap *b; - GSList *vdecls; + GSList *vdecls; /* names */ }; struct rule @@ -135,25 +144,6 @@ struct rule struct judgment *conclusion; }; -struct drawing_params -{ - bool virtual; - bool hide; - WINDOW *w; - int y; - int x; - int row; - int col; - int c; - int m; - int n; - int r; - int s; - int stacked; - int lw; - int jw; -}; - /* * As we draw a rule we move the point (pt - an address) from one variable to * another down the rabbit hole of the data structure. When that address equals @@ -164,7 +154,8 @@ struct drawing_params struct state { bool running; - enum ui_state mode; + enum ui_major_mode major_mode; + enum ui_minor_mode minor_mode; struct rule *rule; struct judgment *judgment; struct name *dependency; @@ -180,10 +171,12 @@ struct state int caret; enum slot_type st; GString *input; - GString *escaped_input; + GString *backslash_input; + GString *esc_input; int status; - bool escape; int err; + bool replacing; + GSList *stack; /* reference stack */ }; const char *escaped_strings[] = { @@ -292,6 +285,262 @@ const char *escaped_strings[] = { GHashTable *escaped_table; +gpointer copy_user_data(gconstpointer src, gpointer data) +{ + return data; +} + +bool +conclusion_p(struct rule *rule, struct judgment *judgment) +{ + return judgment == rule->conclusion ? TRUE : FALSE; +} + +void +clear_contextuals(GHashTable *vets) +{ + GHashTableIter iter; + gpointer key, value; + struct name *name; + + g_hash_table_iter_init(&iter, vets); + while (g_hash_table_iter_next(&iter, &key, &value)) { + name = value; + if (name->scope == s_contextual) + g_hash_table_iter_remove (&iter); + } +} + +void +clear_locals(struct state *state) +{ + g_hash_table_steal_all(state->gctxs); + g_hash_table_steal_all(state->gtheses); + g_hash_table_steal_all(state->vets); +} + +void +next_slot(struct state *state) +{ + switch (state->st) { + case st_rule_dots: + state->st = st_ctx_l; + state->caret += 1; + break; + case st_ctx_l: + state->st = st_ctx_dots; + state->caret += 1; + break; + case st_ctx_v: + state->st = st_ctx_t; + state->caret += 1; + break; + case st_ctx_t: + state->st = st_ctx_dots; + state->caret += 1; + break; + case st_ctx_dots: + state->st = st_ctx_r; + state->caret += 1; + break; + case st_ctx_r: + state->st = st_thesis; + state->caret += 1; + break; + case st_thesis: + switch (state->judgment->kind) + { + case tk_generic: + state->st = st_generic_thesis; + break; + case tk_type: + state->st = st_type_thesis; + break; + case tk_element: + state->st = st_element_thesis_element; + break; + case tk_type_equal: + state->st = st_type_equal_thesis_type_1; + break; + case tk_element_equal: + state->st = st_element_equal_thesis_element_1; + break; + default: + break; + } + break; + case st_generic_thesis: + if (conclusion_p(state->rule, state->judgment)) + state->st = st_rule_name; + else + state->st = st_rule_dots; + state->caret += 1; + clear_contextuals(state->vets); + break; + case st_type_thesis: + if (conclusion_p(state->rule, state->judgment)) + state->st = st_rule_name; + else + state->st = st_rule_dots; + state->caret += 1; + clear_contextuals(state->vets); + break; + case st_element_thesis_element: + if (state->judgment->a->is_origin) { + state->st = st_element_thesis_type; + state->caret += 1; + } + else { + if (conclusion_p(state->rule, state->judgment)) + state->st = st_rule_name; + else + state->st = st_rule_dots; + state->caret += 2; + } + break; + case st_element_thesis_type: + if (conclusion_p(state->rule, state->judgment)) + state->st = st_rule_name; + else + state->st = st_rule_dots; + state->caret += 1; + clear_contextuals(state->vets); + break; + case st_type_equal_thesis_type_1: + state->st = st_type_equal_thesis_type_2; + state->caret += 1; + break; + case st_type_equal_thesis_type_2: + if (conclusion_p(state->rule, state->judgment)) + state->st = st_rule_name; + else + state->st = st_rule_dots; + state->caret += 1; + clear_contextuals(state->vets); + break; + case st_element_equal_thesis_element_1: + state->st = st_element_equal_thesis_element_2; + state->caret += 1; + break; + case st_element_equal_thesis_element_2: + if (state->judgment->a->is_origin) { + state->st = st_element_equal_thesis_type; + state->caret += 1; + } + else { + if (conclusion_p(state->rule, state->judgment)) + state->st = st_rule_name; + else + state->st = st_rule_dots; + state->caret += 2; + } + break; + case st_element_equal_thesis_type: + if (conclusion_p(state->rule, state->judgment)) + state->st = st_rule_name; + else + state->st = st_rule_dots; + state->caret += 1; + clear_contextuals(state->vets); + break; + case st_rule_name: + state->st = st_rule_dots; + state->caret = 0; + break; + default: + } +} + +enum slot_type +prev_thesis_kind_switch(enum thesis_kind tk) +{ + switch (tk) + { + case tk_generic: + return st_generic_thesis; + break; + case tk_type: + return st_type_thesis; + break; + case tk_element: + return st_element_thesis_type; + break; + case tk_type_equal: + return st_type_equal_thesis_type_2; + break; + case tk_element_equal: + return st_element_equal_thesis_type; + break; + default: + return -1; + break; + } +} + +enum slot_type +prev_slot(struct state *state) +{ + switch (state->st) { + case st_rule_dots: + if (state->rule->hypotheses) + return prev_thesis_kind_switch(((struct judgment *)g_slist_last(state->rule->hypotheses)->data)->kind); + break; + case st_ctx_l: + return st_rule_dots; + break; + case st_ctx_v: + return st_ctx_dots; + break; + case st_ctx_t: + return st_ctx_v; + break; + case st_ctx_dots: + if (state->judgment->vdecls) + return st_ctx_t; + else + return st_ctx_l; + break; + case st_ctx_r: + return st_ctx_dots; + break; + case st_thesis: + return st_ctx_r; + break; + case st_generic_thesis: + return st_thesis; + break; + case st_type_thesis: + return st_thesis; + break; + case st_element_thesis_element: + return st_thesis; + break; + case st_element_thesis_type: + return st_element_thesis_element; + break; + case st_type_equal_thesis_type_1: + return st_thesis; + break; + case st_type_equal_thesis_type_2: + return st_type_equal_thesis_type_1; + break; + case st_element_equal_thesis_element_1: + return st_thesis; + break; + case st_element_equal_thesis_element_2: + return st_element_equal_thesis_element_1; + break; + case st_element_equal_thesis_type: + return st_element_equal_thesis_element_2; + break; + case st_rule_name: + return prev_thesis_kind_switch(state->judgment->kind); + break; + default: + return -1; + } +} + struct wrap * create_wrap(bool is_origin, void *ptr) { @@ -319,6 +568,17 @@ create_name(enum scope scope, enum name_kind kind, struct wrap *type, return name; } +struct reference * +create_reference(struct name *origin, GSList *replacements) +{ + struct reference *ref; + + ref = malloc(sizeof(struct reference)); + ref->origin = origin; + ref->replacements = replacements; + return ref; +} + struct judgment * create_judgment() { @@ -334,7 +594,6 @@ create_judgment() return j; } - struct rule * create_rule() { @@ -348,6 +607,7 @@ create_rule() } void free_wrap(struct wrap *); +void free_reference(struct reference *); void free_name(struct name *name) @@ -364,13 +624,11 @@ void free_reference(struct reference *ref) { if (ref) { - free_name(ref->origin); - g_slist_free_full(ref->replacements, (GDestroyNotify)free_wrap); + g_slist_free_full(ref->replacements, (GDestroyNotify)free_reference); free(ref); } } - void free_wrap(struct wrap *wrap) { @@ -383,17 +641,6 @@ free_wrap(struct wrap *wrap) } } -void -free_vdecl(struct vdecl *decl) -{ - if (decl) { - free_name(decl->elem); - free_wrap(decl->type); - free(decl); - } -} - - void free_judgment(struct judgment *judgment) { @@ -402,7 +649,7 @@ free_judgment(struct judgment *judgment) free_wrap(judgment->generic_r); free_wrap(judgment->a); free_wrap(judgment->b); - g_slist_free_full(judgment->vdecls, (GDestroyNotify)free_vdecl); + g_slist_free_full(judgment->vdecls, (GDestroyNotify)free_name); free(judgment); } } @@ -418,6 +665,51 @@ free_rule(struct rule *rule) } } +struct wrap ** +get_wrap_type_addr(struct wrap *wrap) +{ + if (wrap) { + if (wrap->is_origin) + return &(((struct name *)wrap->ptr)->type); + return &(((struct reference *)wrap->ptr)->origin->type); + } + return NULL; +} + +struct wrap * +get_wrap_type(struct wrap *wrap) +{ + struct wrap **addr; + + addr = get_wrap_type_addr(wrap); + if (addr) + return *addr; + return NULL; +} + +struct wrap *copy_wrap(struct wrap *); +struct reference *copy_reference(struct reference *); + +struct reference * +copy_reference(struct reference *reference) +{ + if (!reference) + return NULL; + return create_reference(reference->origin, + g_slist_copy_deep(reference->replacements, + (GCopyFunc)copy_reference, NULL)); +} + +struct wrap * +copy_wrap(struct wrap *wrap) +{ + if (!wrap) + return NULL; + if (wrap->is_origin) + return create_wrap(FALSE, create_reference(wrap->ptr, NULL)); + return create_wrap(FALSE, copy_reference(wrap->ptr)); +} + int greekstrlen(const char *str) { @@ -450,199 +742,154 @@ draw_slot(WINDOW *w, int *y, int *x, bool virtual, bool optional, int pair, cons } void -draw_wrap(WINDOW *w, int *y, int *x, bool virtual, bool optional, - int pair, struct wrap *wrap) +set_ctp_and_pair(enum caret_to_point *ctp, int *pair, int caret, int point) { - struct reference *r; + *ctp = caret < point ? ctp_before : (caret > point ? ctp_after : ctp_on); + *pair = *ctp == ctp_on ? PAIR_HL : PAIR_NORMAL; +} + +void +draw_ref(WINDOW *w, int *y, int *x, bool virtual, + int caret, int *point, char *inputstr, struct reference *ref) +{ + int pair; + enum caret_to_point ctp; GSList *l; - if (!wrap) - draw_slot(w, y, x, virtual, optional, pair, NULL); + if (!ref) { + set_ctp_and_pair(&ctp, &pair, caret, (*point)++); + if (ctp == ctp_on) + draw_slot(w, y, x, virtual, FALSE, pair, inputstr); + else if (ctp == ctp_before) + draw_slot(w, y, x, virtual, FALSE, pair, NULL); + } else { - if (wrap->is_origin) { - draw_slot(w, y, x, virtual, optional, pair, - ((struct name *)wrap->ptr)->str); - } - else { - r = wrap->ptr; - draw_slot(w, y, x, virtual, optional, pair, r->origin->str); - l = r->replacements; - if (l) { - draw_slot(w, y, x, virtual, FALSE, PAIR_BW, "["); - while (l) { - draw_wrap(w, y, x, virtual, FALSE, pair, l->data); - l = l->next; - if (l) - draw_slot(w, y, x, virtual, FALSE, PAIR_BW, ", "); - } - draw_slot(w, y, x, virtual, FALSE, PAIR_BW, "]"); + set_ctp_and_pair(&ctp, &pair, caret, (*point)++); + draw_slot(w, y, x, virtual, FALSE, pair, ref->origin->str); + l = ref->replacements; + if (l) { + draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, "["); + while (l) { + draw_ref(w, y, x, virtual, caret, point, inputstr, l->data); + l = l->next; + if (l) + draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, ", "); } + draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, "]"); } } } -struct wrap * -get_wrap_type(struct wrap *wrap) +bool /* is displayed ? */ +draw_wrap(WINDOW *w, int *y, int *x, bool virtual, bool optional, + int caret, int *point, char *inputstr, struct wrap *wrap) { - if (wrap) { - if (wrap->is_origin) - return ((struct name *)wrap->ptr)->type; + int pair; + enum caret_to_point ctp; + GSList *l; + + if (!wrap) { + set_ctp_and_pair(&ctp, &pair, caret, (*point)++); + if (ctp == ctp_on) + draw_slot(w, y, x, virtual, FALSE, pair, inputstr); + else if (ctp == ctp_before) + draw_slot(w, y, x, virtual, optional, pair, NULL); else - return ((struct reference *)wrap->ptr)->origin->type; + return FALSE; } - else - return NULL; -} - -void -set_ctp_and_pair(enum caret_to_point *ctp, int *pair, int caret, int point) -{ - *ctp = caret < point ? ctp_before : (caret > point ? ctp_after : ctp_on); - *pair = *ctp == ctp_on ? PAIR_HL : PAIR_BW; + else { + if (wrap->is_origin) { + set_ctp_and_pair(&ctp, &pair, caret, (*point)++); + draw_slot(w, y, x, virtual, optional, pair, + ((struct name *)wrap->ptr)->str); + } + else + draw_ref(w, y, x, virtual, caret, point, inputstr, wrap->ptr); + } + return TRUE; } void draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, int caret, int *point, char *inputstr, struct judgment *judgment) { - bool v, prev_not_displayed; + bool v, is_prev_displayed; int pair; GSList *l; - struct vdecl *decl; + struct name *var; enum caret_to_point ctp; v = virtual; /* Γ */ - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - prev_not_displayed = FALSE; - if (judgment->generic_l) - draw_wrap(w, y, x, v, TRUE, pair, judgment->generic_l); - else if (workspace_mode) { - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else if (ctp == ctp_before) - draw_slot(w, y, x, v, TRUE, pair, NULL); - else - prev_not_displayed = TRUE; + is_prev_displayed = FALSE; + if (workspace_mode || judgment->generic_l) { + is_prev_displayed = draw_wrap(w, y, x, v, TRUE, + caret, point, inputstr, judgment->generic_l); } - else - prev_not_displayed = TRUE; /* vdecls */ l = judgment->vdecls; while (l) { set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - decl = l->data; - if (!(l == judgment->vdecls && prev_not_displayed)) - draw_slot(w, y, x, v, FALSE, PAIR_BW, ", "); + var = l->data; + if (!(l == judgment->vdecls && !is_prev_displayed)) + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", "); if (ctp == ctp_on) draw_slot(w, y, x, v, FALSE, pair, inputstr); else - draw_slot(w, y, x, v, FALSE, pair, decl->elem->str); - draw_slot(w, y, x, v, FALSE, PAIR_BW, " : "); - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, decl->type); - prev_not_displayed = FALSE; + draw_slot(w, y, x, v, FALSE, pair, var->str); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " : "); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, var ? var->type : NULL); + is_prev_displayed = TRUE; l = l->next; } /* ctx_dots */ set_ctp_and_pair(&ctp, &pair, caret, (*point)++); if (workspace_mode && (ctp == ctp_before || ctp == ctp_on)) { - if (!prev_not_displayed) - draw_slot(w, y, x, v, FALSE, PAIR_BW, ", "); + if (is_prev_displayed) + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", "); draw_slot(w, y, x, v, FALSE, pair, "..."); - prev_not_displayed = FALSE; + is_prev_displayed = TRUE; } /* Δ */ - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (judgment->generic_r) { - if (!prev_not_displayed) - draw_slot(w, y, x, v, FALSE, PAIR_BW, ", "); - draw_wrap(w, y, x, v, TRUE, pair, judgment->generic_r); - } - else if (workspace_mode) { - if (ctp == ctp_on) { - if (!prev_not_displayed) - draw_slot(w, y, x, v, FALSE, PAIR_BW, ", "); - draw_slot(w, y, x, v, FALSE, pair, inputstr); - } - else if (ctp == ctp_before) { - if (!prev_not_displayed) - draw_slot(w, y, x, v, FALSE, PAIR_BW, ", "); - draw_slot(w, y, x, v, TRUE, pair, NULL); - } + if (workspace_mode || judgment->generic_r) { + set_ctp_and_pair(&ctp, &pair, caret, *point); + if (is_prev_displayed && (judgment->generic_r || ctp <= ctp_on)) + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", "); + draw_wrap(w, y, x, v, TRUE, caret, point, inputstr, judgment->generic_r); } - draw_slot(w, y, x, v, FALSE, PAIR_BW, " ⊢ "); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " ⊢ "); /* thesis */ switch (judgment->kind) { case tk_generic: - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, judgment->a); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a); break; case tk_type: - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, judgment->a); - draw_slot(w, y, x, v, FALSE, PAIR_BW, " type"); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " type"); break; case tk_element: - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, judgment->a); - draw_slot(w, y, x, v, FALSE, PAIR_BW, " : "); - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, get_wrap_type(judgment->a)); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " : "); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, get_wrap_type(judgment->a)); break; case tk_type_equal: - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, judgment->a); - draw_slot(w, y, x, v, FALSE, PAIR_BW, " ≐ "); - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, judgment->b); - draw_slot(w, y, x, v, FALSE, PAIR_BW, " type"); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " ≐ "); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->b); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " type"); break; case tk_element_equal: - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, judgment->a); - draw_slot(w, y, x, v, FALSE, PAIR_BW, " ≐ "); - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, judgment->b); - draw_slot(w, y, x, v, FALSE, PAIR_BW, " : "); - set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) - draw_slot(w, y, x, v, FALSE, pair, inputstr); - else - draw_wrap(w, y, x, v, FALSE, pair, get_wrap_type(judgment->a)); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " ≐ "); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->b); + draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " : "); + draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, get_wrap_type(judgment->a)); break; case tk_unknown: set_ctp_and_pair(&ctp, &pair, caret, (*point)++); @@ -745,9 +992,46 @@ draw_rule(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, void render_splash() { + int i, n; + static const char *strs[] = { + "VOUIVRE", + "", + "version 0.2.0", + "by Vouivre Digital Corporation", + "", + "type ESC q RET to quit", + "type ESC splash RET to return to this screen", + "type ESC h RET to get help", + "type any other key to continue", + }; + + n = sizeof(strs) / sizeof(char *); clear(); - mvprintw(0, 0, "VOUIVRE version 0.2.0"); - mvprintw(1, 0, "press any key to continue"); + for (i = 0 ; i < 5 ; i++) { + mvprintw((LINES - n) / 2 + i, + (COLS - strlen(strs[i])) / 2, + strs[i]); + } + for (i = 5 ; i < n ; i++) { + mvprintw((LINES - n) / 2 + i, + (COLS - strlen(strs[6])) / 2, + strs[i]); + } + refresh(); +} + +void +render_help() +{ + int c; + FILE *fd; + + clear(); + fd = fopen("help.txt", "r"); + move(0, 0); + while ((c = fgetc(fd)) != EOF) + addch(c); + fclose(fd); refresh(); } @@ -777,7 +1061,7 @@ echo_status(WINDOW *w, int status) str = "error: left and right generic contexts must differ"; break; case 5: - str = "error: type already defined"; + str = "error: name already defined"; break; case 6: str = "error: inconsistant kinds"; /* TODO: list the two kinds conflicting */ @@ -791,7 +1075,14 @@ echo_status(WINDOW *w, int status) } void -render(struct state *state) +echo_esc(struct state *state) +{ + mvwprintw(state->echo_w, 0, 0, "ESC"); + mvwprintw(state->echo_w, 0, 4, state->esc_input->str); +} + +void +render(struct state *state, char kkey) { int y, x, q, i; static const char *str1 = "g: generic t: type e: element " @@ -807,8 +1098,9 @@ render(struct state *state) clear(); /* draw debug info */ - mvwprintw(stdscr, LINES - 3, 0, "mode: %d st: %d caret: %d", - state->mode, state->st, state->caret); + mvwprintw(stdscr, LINES - 3, 0, "major_mode: %d minor_mode: %d st: %d caret: %d inputstr: %s replacing: %d key: %d", + state->major_mode, state->minor_mode, state->st, state->caret, + state->input->str, state->replacing, kkey); /* draw workspace rule */ y = 0; x = 0; @@ -844,17 +1136,17 @@ render(struct state *state) state->err = 0; } else { - switch (state->mode) { - case uis_workspace: + switch (state->major_mode) { + case uimam_workspace: if (state->st == st_thesis) { if (state->status == 0) mvwprintw(state->echo_w, 0, 0, str1); else mvwprintw(state->echo_w, 0, 0, str2); } - else if (state->escape) { + else if (state->minor_mode == uimim_backslash) { mvwprintw(state->echo_w, 0, 0, "\\"); - wprintw(state->echo_w, state->escaped_input->str); + wprintw(state->echo_w, state->backslash_input->str); } break; default: @@ -862,12 +1154,12 @@ render(struct state *state) } /* draw window names */ - attron(COLOR_PAIR(PAIR_WB)); + attron(COLOR_PAIR(PAIR_INVERSE)); move(q, 0); printw("workspace%*s", COLS - 9, ""); - move(2 * q + 1, 0); + move(LINES - 2, 0); printw("support%*s", COLS - 7, ""); - attroff(COLOR_PAIR(PAIR_WB)); + attroff(COLOR_PAIR(PAIR_INVERSE)); refresh(); } @@ -879,50 +1171,48 @@ handle_input(struct state *state, char key) struct name *name; if (key == '\\') { - state->escape = TRUE; + state->minor_mode = uimim_backslash; state->status = 0; - g_string_erase(state->escaped_input, 0, -1); + state->backslash_input = g_string_erase(state->backslash_input, 0, -1); } else if (key > 32 && key < 127) { - if (!state->escape) + if (state->minor_mode == uimim_default) state->input = g_string_append_c(state->input, key); else { if ((key > 64 && key < 91) || (key > 96 && key < 123)) { - state->escaped_input = g_string_append_c(state->escaped_input, key); - l = g_hash_table_lookup(escaped_table, state->escaped_input->str); + state->backslash_input = g_string_append_c(state->backslash_input, key); + l = g_hash_table_lookup(escaped_table, state->backslash_input->str); if (!l) { - state->escape = FALSE; + state->minor_mode = uimim_default; } else if (!l->next) { - state->escape = FALSE; + state->minor_mode = uimim_default; state->input = g_string_append(state->input, l->data); } } else - state->escape = FALSE; + state->minor_mode = uimim_default; } } if ((name = g_hash_table_lookup(state->decls, state->input->str))) { - if (state->support) - state->support->data = name->src; - else - state->support = g_slist_prepend(state->support, name->src); - } + if (state->support) + state->support->data = name->src; + else + state->support = g_slist_prepend(state->support, name->src); + } } void handle_slot_backspace(struct state *state) { - switch (state->st) { - case st_a: - state->st = st_thesis; - state->judgment->kind = tk_unknown; - break; - case st_b: - break; - default: - } + /* if ((state->st == st_generic_thesis) || */ + /* (state->st == st_type_thesis) || */ + /* (state->st == st_element_thesis_element) || */ + /* (state->st == st_type_equal_thesis_type_1) || */ + /* (state->st == st_element_equal_thesis_element_1)) */ + /* state->judgment->kind = tk_unknown; */ + /* state->st = prev_slot(state); */ } void @@ -931,97 +1221,226 @@ handle_input_backspace(struct state *state) if (*state->input->str == '\0') handle_slot_backspace(state); else - g_string_erase(state->input, 0, -1); + state->input = g_string_erase(state->input, 0, -1); } void handle_backspace(struct state *state) { - if (!state->escape) + if (state->minor_mode == uimim_default) handle_input_backspace(state); else { - if (*state->escaped_input->str == '\0') - state->escape = FALSE; + if (*state->backslash_input->str == '\0') + state->minor_mode = uimim_default; else - g_string_erase(state->escaped_input, 0, -1); + state->backslash_input = g_string_erase(state->backslash_input, 0, -1); } } -bool -conclusion_p(struct rule *rule, struct judgment *judgment) -{ - return judgment == rule->conclusion ? TRUE : FALSE; -} - -int -validate_generic_context(struct state *state, bool is_left) +void +handle_esc(struct state *state, wint_t key) { - struct name *name; - - if (*state->input->str == '\0') - return 0; - if (conclusion_p(state->rule, state->judgment)) { - if (!(name = g_hash_table_lookup(state->gctxs, state->input->str))) - return 3; - if (is_left) { - state->judgment->generic_l = create_wrap(FALSE, name); - } + if (key == KEY_ESC) { + if (state->minor_mode = uimim_esc) + state->minor_mode = uimim_default; else { - if (state->judgment->generic_l && - name == state->judgment->generic_l->ptr) - return 4; - state->judgment->generic_r = create_wrap(FALSE, name); + state->esc_input = g_string_erase(state->esc_input, 0, -1); + state->minor_mode = uimim_esc; + } + } + else if (state->minor_mode == uimim_esc) { + if (key == KEY_RETURN) { + state->minor_mode = uimim_default; + if (strcmp(state->esc_input->str, "q") == 0) + state->running = FALSE; + else if (strcmp(state->esc_input->str, "splash") == 0) + state->major_mode = uimam_splash; + else if (strcmp(state->esc_input->str, "h") == 0) + state->major_mode = uimam_help; + } + else if ((key > 64 && key < 91) || (key > 96 && key < 123)) { + state->esc_input = g_string_append_c(state->esc_input, key); } - g_string_erase(state->input, 0, -1); - return 0; } - else - return -1; } GSList * -list_dependencies(GHashTable *vets) +list_dependencies(GHashTable *vets, enum name_kind nk, enum scope s, void *addr) { GSList *l; GHashTableIter iter; gpointer key, value; + struct name *name; l = NULL; g_hash_table_iter_init(&iter, vets); - while (g_hash_table_iter_next(&iter, &key, &value)) - l = g_slist_prepend(l, value); /* value = a name */ + while (g_hash_table_iter_next(&iter, &key, &value)) { + name = value; + if (nk == nk_generic_context_left || nk == nk_generic_context_right) { + if (name->scope == s_contextual) + l = g_slist_prepend(l, name); + } + else { + /* The name is a dependency if it goes out of scope sooner than its + target. This is always the case when the target is global. This is + also the case when the target is local and the name contextual. A + variable is not a dependency of its declaration type */ + if (s == s_global || (s == s_local && + name->scope == s_contextual && + &name->type != addr)) + l = g_slist_prepend(l, name); + } + } return l; } int -validate_type_thesis(struct state *state) +validate_generic_context(struct state *state, bool is_left) { + enum name_kind nk; struct name *name; + struct wrap *wrap; + if (*state->input->str == '\0') + return 0; + name = g_hash_table_lookup(state->gctxs, state->input->str); + nk = is_left ? nk_generic_context_left : nk_generic_context_right; + if (name) { + if (nk != name->kind) + return 4; + wrap = create_wrap(FALSE, + create_reference(name, + g_slist_copy_deep(name->dependencies, + copy_user_data, + NULL))); + if (is_left) + state->judgment->generic_l = wrap; + else + state->judgment->generic_r = wrap; + state->input = g_string_erase(state->input, 0, -1); + return 0; + } + else if (conclusion_p(state->rule, state->judgment)) + return 3; + name = create_name(s_local, + nk, + NULL, + state->rule, + list_dependencies(state->vets, nk, s_local, NULL), + strdup(state->input->str)); + wrap = create_wrap(TRUE, name); + if (is_left) + state->judgment->generic_l = wrap; + else + state->judgment->generic_r = wrap; + g_hash_table_insert(state->gctxs, name->str, name); + state->input = g_string_erase(state->input, 0, -1); + return 0; +} + +int +/* validate_vet_input(struct wrap **wrap, struct state *state, enum name_kind nk) */ +validate_vet_input(void *addr, struct state *state, enum name_kind nk) +{ + bool is_c; + enum thesis_kind tk; + struct name *name; + GSList *l; + + tk = state->judgment->kind; + is_c = conclusion_p(state->rule, state->judgment); if (*state->input->str == '\0') return 1; - if (conclusion_p(state->rule, state->judgment)) { - if ((name = g_hash_table_lookup(state->decls, state->input->str))) + if ((name = g_hash_table_lookup(state->decls, state->input->str))) { + if (nk == nk_variable || tk == tk_type || + (tk == tk_element && nk == nk_element)) return 5; - if ((name = g_hash_table_lookup(state->vets, state->input->str))) { - if (name->kind != nk_type) - return 6; + if (name->kind != nk) + return 6; + state->input = g_string_erase(state->input, 0, -1); + l = g_slist_copy_deep(name->dependencies, copy_user_data, NULL); + *(struct wrap **)addr = create_wrap(FALSE, create_reference(name, l)); + return 0; + } + if ((name = g_hash_table_lookup(state->vets, state->input->str))) { + if (nk == nk_variable) + return 5; + if (name->kind != nk) + return 6; + state->input = g_string_erase(state->input, 0, -1); + l = g_slist_copy_deep(name->dependencies, copy_user_data, NULL); + *(struct wrap **)addr = create_wrap(FALSE, create_reference(name, l)); + return 0; + } + if (nk == nk_variable) { + name = create_name(s_contextual, nk_element, NULL, state->rule, + NULL, + strdup(state->input->str)); + g_hash_table_insert(state->vets, name->str, name); + state->input = g_string_erase(state->input, 0, -1); + *(struct name **)addr = name; + return 0; + } + if (is_c) { + if (tk == tk_type_equal || + tk == tk_element_equal || + (tk == tk_unknown && nk == nk_type) || /* variable type */ + (tk == tk_element && nk == nk_type)) /* element type */ + return 3; + name = create_name(s_global, nk, NULL, state->rule, + list_dependencies(state->vets, nk, s_global, addr), + strdup(state->input->str)); + } + else { + name = create_name(s_local, nk, NULL, state->rule, + list_dependencies(state->vets, nk, s_local, addr), + strdup(state->input->str)); + g_hash_table_insert(state->vets, name->str, name); + } + state->input = g_string_erase(state->input, 0, -1); + *(struct wrap **)addr = create_wrap(TRUE, name); + return 0; +} - /* the name exists, is a type, and is local */ - state->judgment->a = create_wrap(FALSE, name); - return -1; /* TODO: check dependencies */ - } +int +validate_replacement(struct state *state) +{ + bool is_c; + guint idx; + GSList *reps, *l; + struct name *dep, *name; + struct reference *ref; + + if (*state->input->str == '\0') + return 1; + name = g_hash_table_lookup(state->decls, state->input->str); + if (!name) + name = g_hash_table_lookup(state->vets, state->input->str); + if (name) { + ref = state->stack->data; + idx = g_slist_index(ref->replacements, NULL); + dep = g_slist_nth_data(ref->origin->dependencies, idx); + if (name->kind != dep->kind) + return 6; + l = g_slist_nth(ref->replacements, idx); + reps = g_slist_copy_deep(name->dependencies, copy_user_data, NULL); + l->data = create_reference(name, reps); + + if (reps) + state->stack = g_slist_prepend(state->stack, l->data); else { - name = create_name(s_global, nk_type, NULL, state->rule, - list_dependencies(state->vets), - strdup(state->input->str)); - state->judgment->a = create_wrap(TRUE, name); - g_string_erase(state->input, 0, -1); - return 0; + l = l->next; + while (state->stack && !l) { + state->stack = state->stack->next; + if (state->stack) + l = g_slist_find(((struct reference *)state->stack->data)->replacements, NULL); + } } + state->input = g_string_erase(state->input, 0, -1); + return 0; } - return -1; + return 3; } int @@ -1048,15 +1467,32 @@ validate_rule_name(struct state *state) break; default: } - g_string_erase(state->input, 0, -1); + state->input = g_string_erase(state->input, 0, -1); state->rule = create_rule(); state->judgment = state->rule->conclusion; + clear_locals(state); return 0; } +bool +requires_replacements(struct wrap *addr) +{ + return addr && addr->is_origin == FALSE && + ((struct reference *)addr->ptr)->replacements; +} + +void +handle_replacements(struct state *state, struct wrap *addr) +{ + state->replacing = TRUE; + state->stack = g_slist_prepend(state->stack, addr->ptr); + state->caret += 1; +} + int main() { + bool c_p; const char *k, *v; char *str; int i, j, q; @@ -1066,6 +1502,8 @@ main() GHashTableIter iter; gpointer hkey, hvalue; wint_t key; + struct wrap **addr; + void *naddr; setlocale(LC_ALL, ""); initscr(); @@ -1076,15 +1514,16 @@ main() ESCDELAY = 0; intrflush(stdscr, FALSE); keypad(stdscr, TRUE); - init_pair(PAIR_BW, COLOR_BLACK, COLOR_WHITE); - init_pair(PAIR_WB, COLOR_WHITE, COLOR_BLACK); - init_pair(PAIR_HL, COLOR_CYAN, COLOR_WHITE); - init_pair(PAIR_SUCCESS, COLOR_GREEN, COLOR_WHITE); - init_pair(PAIR_ERROR, COLOR_RED, COLOR_WHITE); - bkgd(COLOR_PAIR(PAIR_BW)); + init_pair(PAIR_NORMAL, COLOR_WHITE, COLOR_BLACK); + init_pair(PAIR_INVERSE, COLOR_BLACK, COLOR_WHITE); + init_pair(PAIR_HL, COLOR_CYAN, COLOR_BLACK); + init_pair(PAIR_SUCCESS, COLOR_GREEN, COLOR_BLACK); + init_pair(PAIR_ERROR, COLOR_RED, COLOR_BLACK); + bkgd(COLOR_PAIR(PAIR_NORMAL)); q = (LINES - 3) / 2; state.running = TRUE; - state.mode = uis_splash; + state.major_mode = uimam_splash; + state.minor_mode = uimim_default; state.rule = create_rule(); state.judgment = state.rule->conclusion; state.dependency = NULL; @@ -1101,9 +1540,11 @@ main() state.caret = 0; state.st = st_rule_dots; state.input = g_string_new(NULL); - state.escaped_input = g_string_new(NULL); - state.escape = FALSE; + state.backslash_input = g_string_new(NULL); + state.esc_input = g_string_new(NULL); state.err = 0; + state.replacing = FALSE; + state.stack = NULL; /* populate escaped strings table */ /* NOTE: `g_hash_table_insert' deletes keys and values if they already exist. @@ -1122,173 +1563,342 @@ main() } } - if (state.mode == uis_splash) { - render_splash(); - getch(); - state.mode = uis_workspace; - render(&state); - } + render_splash(); + get_wch(&key); + state.major_mode = uimam_workspace; + render(&state, key); while(state.running) { get_wch(&key); - if (key == KEY_ESC) { - state.running = FALSE; - break; - } - switch(state.mode) { - case uis_workspace: - switch (state.st) { - case st_rule_dots: + switch(state.major_mode) { + case uimam_splash: + render_splash(); + /* no break (intentional) */ + case uimam_help: + render_help(); + /* no break (intentional) */ + case uimam_workspace: + if (key == KEY_ESC) + state.running = FALSE; + else if (state.replacing) { if (key == KEY_TAB) { - state.caret += 1; - state.st = st_ctx_l; - state.judgment = state.rule->conclusion; - } - else if (key == KEY_RETURN) { - state.judgment = create_judgment(); - state.rule->hypotheses = g_slist_append(state.rule->hypotheses, state.judgment); - state.st = st_ctx_l; - } - break; - case st_rule_name: - if (key == KEY_TAB) { - if (!(state.err = validate_rule_name(&state))) { - /* reset the workspace to initial state */ - state.caret = 0; - state.st = st_rule_dots; - g_slist_free(g_steal_pointer(&state.support)); + if (!(state.err = validate_replacement(&state))) { + if (state.stack) + state.caret += 1; + else { /* we are done replacing */ + state.replacing = FALSE; + next_slot(&state); + } } } else if (key == KEY_BACKSPACE) handle_backspace(&state); else handle_input(&state, key); - break; - case st_ctx_l: - if (key == KEY_TAB) { - if (!(state.err = validate_generic_context(&state, TRUE))) { - state.caret += 1; - state.st = st_ctx_dots; + } + else { + switch (state.st) { + case st_rule_dots: + if (key == KEY_TAB) { + next_slot(&state); + state.judgment = state.rule->conclusion; } - } - else if (key == KEY_BACKSPACE) - handle_backspace(&state); - else - handle_input(&state, key); - break; - case st_ctx_v: - break; - case st_ctx_t: - break; - case st_ctx_dots: - if (key == KEY_TAB) { - state.caret += 1; - state.st = st_ctx_r; - } - else if (key == KEY_RETURN) { - } - break; - case st_ctx_r: - if (key == KEY_TAB) { - if (!(state.err = validate_generic_context(&state, FALSE))) { - state.caret += 1; - state.st = st_thesis; - state.status = 0; + else if (key == KEY_RETURN) { + state.judgment = create_judgment(); + state.rule->hypotheses = g_slist_append(state.rule->hypotheses, state.judgment); + state.st = st_ctx_l; } - } - else if (key == KEY_BACKSPACE) - handle_backspace(&state); - else - handle_input(&state, key); - break; - case st_thesis: - j_p = state.judgment; - if (state.status == 0) { - switch (key) { - case 'g': - state.st = st_a; - j_p->kind = tk_generic; - break; - case 't': - state.st = st_a; - j_p->kind = tk_type; - break; - case 'e': - state.st = st_a; - j_p->kind = tk_element; - break; - case '=': - state.status = 1; - break; - default: + else if (key == KEY_BACKSPACE) { + if (state.rule->hypotheses) { + state.caret -= 1; + state.st = prev_slot(&state); + state.judgment = g_slist_last(state.rule->hypotheses)->data; + } } - } - else if (state.status == 1) { - switch (key) { - case 't': - state.st = st_a; - j_p->kind = tk_type_equal; - break; - case 'e': - state.st = st_a; - j_p->kind = tk_element_equal; - break; - default: - state.status = 0; + break; + case st_ctx_l: + if (key == KEY_TAB) { + if (!(state.err = validate_generic_context(&state, TRUE))) { + addr = &state.judgment->generic_l; + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); + else + next_slot(&state); + } } - } - break; - case st_a: - if (key == KEY_TAB) { - switch (state.judgment->kind) { - case tk_type: - if (!(state.err = validate_type_thesis(&state))) { - state.caret += 1; - if (conclusion_p(state.rule, state.judgment)) - state.st = st_rule_name; + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_ctx_v: + if (key == KEY_TAB) { + naddr = &g_slist_last(state.judgment->vdecls)->data; + if (!(state.err = validate_vet_input(naddr, &state, nk_variable))) + next_slot(&state); + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_ctx_t: + if (key == KEY_TAB) { + naddr = &g_slist_last(state.judgment->vdecls)->data; + addr = &((*((struct name **)naddr))->type); + if (!(state.err = validate_vet_input(addr, &state, nk_type))) + next_slot(&state); + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_ctx_dots: + if (key == KEY_TAB) + next_slot(&state); + else if (key == KEY_RETURN) { + state.judgment->vdecls = g_slist_append(state.judgment->vdecls, NULL); + state.st = st_ctx_v; + } + break; + case st_ctx_r: + if (key == KEY_TAB) { + if (!(state.err = validate_generic_context(&state, FALSE))) { + addr = &state.judgment->generic_r; + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); + else { + next_slot(&state); + state.status = 0; + } + } + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_thesis: + j_p = state.judgment; + if (state.status == 0) { + switch (key) { + case 'g': + j_p->kind = tk_generic; + next_slot(&state); + break; + case 't': + j_p->kind = tk_type; + next_slot(&state); + break; + case 'e': + j_p->kind = tk_element; + next_slot(&state); + break; + case '=': + state.status = 1; + break; + default: + } + } + else if (state.status == 1) { + switch (key) { + case 't': + j_p->kind = tk_type_equal; + next_slot(&state); + break; + case 'e': + j_p->kind = tk_element_equal; + next_slot(&state); + break; + default: + state.status = 0; + } + } + break; + case st_generic_thesis: + state.err = -1; + break; + case st_type_thesis: + if (key == KEY_TAB) { + addr = &state.judgment->a; + if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); else - state.st = st_rule_dots; + next_slot(&state); } - break; - default: - state.err = -1; } - } - else if (key == KEY_BACKSPACE) - handle_backspace(&state); - else - handle_input(&state, key); - break; - case st_b: - if (key == KEY_TAB) { - state.caret += 1; - if (j_p->kind == tk_element_equal) { - state.st = st_c; + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_element_thesis_element: + if (key == KEY_TAB) { + addr = &state.judgment->a; + if (!(state.err = validate_vet_input(addr, &state, nk_element))) + next_slot(&state); } - else { - state.st = st_rule_name; + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_element_thesis_type: + if (key == KEY_TAB) { + addr = get_wrap_type_addr(state.judgment->a); + if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); + else + next_slot(&state); + /* if ((*addr)->is_origin == FALSE && */ + /* ((struct reference *)((*addr)->ptr))->replacements) { */ + /* state.replacing = TRUE; */ + /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ + /* state.caret += 1; */ + /* } */ + /* else */ + /* next_slot(&state); */ + } } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_type_equal_thesis_type_1: + if (key == KEY_TAB) { + addr = &state.judgment->a; + if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); + else + next_slot(&state); + /* if ((*addr)->is_origin == FALSE && */ + /* ((struct reference *)((*addr)->ptr))->replacements) { */ + /* state.replacing = TRUE; */ + /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ + /* state.caret += 1; */ + /* } */ + /* else */ + /* next_slot(&state); */ + } + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_type_equal_thesis_type_2: + if (key == KEY_TAB) { + addr = &state.judgment->b; + if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); + else + next_slot(&state); + /* if ((*addr)->is_origin == FALSE && */ + /* ((struct reference *)((*addr)->ptr))->replacements) { */ + /* state.replacing = TRUE; */ + /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ + /* state.caret += 1; */ + /* } */ + /* else */ + /* next_slot(&state); */ + } + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_element_equal_thesis_element_1: + if (key == KEY_TAB) { + addr = &state.judgment->a; + if (!(state.err = validate_vet_input(addr, &state, nk_element))) { + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); + else + next_slot(&state); + /* if ((*addr)->is_origin == FALSE && */ + /* ((struct reference *)((*addr)->ptr))->replacements) { */ + /* state.replacing = TRUE; */ + /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ + /* state.caret += 1; */ + /* } */ + /* else */ + /* next_slot(&state); */ + } + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_element_equal_thesis_element_2: + if (key == KEY_TAB) { + addr = &state.judgment->b; + if (!(state.err = validate_vet_input(addr, &state, nk_element))) { + if (requires_replacements(*addr)) + handle_replacements(&state, *addr); + else + next_slot(&state); + /* if ((*addr)->is_origin == FALSE && */ + /* ((struct reference *)((*addr)->ptr))->replacements) { */ + /* state.replacing = TRUE; */ + /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ + /* state.caret += 1; */ + /* } */ + /* else */ + /* next_slot(&state); */ + } + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_element_equal_thesis_type: + if (key == KEY_TAB) { + addr = get_wrap_type_addr(state.judgment->a); + if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + *get_wrap_type_addr(state.judgment->b) = copy_wrap(*addr); + + /* if ((*addr)->is_origin == FALSE && */ + /* ((struct reference *)((*addr)->ptr))->replacements) { */ + /* state.replacing = TRUE; */ + /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ + /* state.caret += 1; */ + /* } */ + /* else */ + next_slot(&state); + } + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; + case st_rule_name: + if (key == KEY_TAB) { + if (!(state.err = validate_rule_name(&state))) { + /* reset the workspace to initial state */ + next_slot(&state); + g_slist_free(g_steal_pointer(&state.support)); + } + } + else if (key == KEY_BACKSPACE) + handle_backspace(&state); + else + handle_input(&state, key); + break; } - else if (key == KEY_BACKSPACE) - handle_backspace(&state); - else - handle_input(&state, key); - break; - case st_c: - if (key == KEY_TAB) { - state.caret += 1; - state.st = st_rule_name; - } - else if (key == KEY_BACKSPACE) - handle_backspace(&state); - else - handle_input(&state, key); - break; - default: } + render(&state, key); break; default: } - render(&state); } delwin(state.workspace_w); delwin(state.support_w); @@ -1306,6 +1916,7 @@ main() g_hash_table_destroy(state.vets); g_slist_free(state.support); g_string_free(state.input, TRUE); - g_string_free(state.escaped_input, TRUE); + g_string_free(state.backslash_input, TRUE); + g_string_free(state.esc_input, TRUE); return 0; } -- 2.39.5