From 26be31e3ad0823e7f6aed9d9ea9f76ba5673fc11 Mon Sep 17 00:00:00 2001 From: admin Date: Sun, 3 Nov 2024 23:05:12 -0500 Subject: [PATCH] Draw rules in order entered --- help.txt | 40 ++++++++-- src/ui.c | 10 ++- src/v.c | 225 +++++++++++++++++++++++++++++++++---------------------- 3 files changed, 179 insertions(+), 96 deletions(-) diff --git a/help.txt b/help.txt index 44691b1..d8d4001 100644 --- a/help.txt +++ b/help.txt @@ -1,13 +1,41 @@ -Slots -... zero or more of something (variable declarations or hypotheses) -█ empty input -█? optional input - Global Commands + ESC q quit Vouivre ESC splash go to splash screen ESC h go to (this) help screen -Workspace Commands +Slots + +... zero or more hypotheses or variable declarations +█ empty input +█? optional input + +Workspace Keys + TAB move to next slot RET add an item when on a '...' slot +\ enter a special character + +Special Characters + +\to → \Xi Ξ \BB 𝔹 \VV 𝕍 \pp 𝕡 +\alpha α \xi ξ \CC ℂ \WW 𝕎 \qq 𝕢 +\beta β \Omicron Ο \DD 𝔻 \XX 𝕏 \rr 𝕣 +\Gamma Γ \omicron ο \EE 𝔼 \YY 𝕐 \ss 𝕤 +\gamma γ \Pi Π \FF 𝔽 \ZZ ℤ \tt 𝕥 +\Delta Δ \pi π \GG 𝔾 \aa 𝕒 \uu 𝕦 +\delta δ \Rho Ρ \HH ℍ \bb 𝕓 \vv 𝕧 +\epsilon ε \rho ρ \II 𝕀 \cc 𝕔 \ww 𝕨 +\Zeta Ζ \Sigma Σ \JJ 𝕁 \dd 𝕕 \xx 𝕩 +\zeta ζ \sigma σ \KK 𝕂 \ee 𝕖 \yy 𝕪 +\eta η \upsilon υ \LL 𝕃 \ff 𝕗 \zz 𝕫 +\Theta Θ \Phi Φ \MM 𝕄 \gg 𝕘 \00 𝟘 +\theta θ \phi φ \NN ℕ \hh 𝕙 \11 𝟙 +\Iota Ι \Chi Χ \OO 𝕆 \ii 𝕚 \22 𝟚 +\iota ι \chi χ \PP ℙ \jj 𝕛 \33 𝟛 +\kappa κ \Psi Ψ \QQ ℚ \kk 𝕜 \44 𝟜 +\Lambda Λ \psi ψ \RR ℝ \ll 𝕝 \55 𝟝 +\lambda λ \Omega Ω \SS 𝕊 \mm 𝕞 \66 𝟞 +\mu μ \omega ω \TT 𝕋 \nn 𝕟 \77 𝟟 +\nu ν \AA 𝔸 \UU 𝕌 \oo 𝕠 \88 𝟠 + \99 𝟡 diff --git a/src/ui.c b/src/ui.c index 8f14e68..171a312 100644 --- a/src/ui.c +++ b/src/ui.c @@ -792,8 +792,13 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset, n += 1; l = l->next; } - if (workspace_mode && (offset >= caret_offset)) + if (workspace_mode && (offset >= caret_offset)) { is_dot = TRUE; + draw_slot(w, y, x, &offset, caret_offset, TRUE, + "...", FALSE); + } + else + offset += 1; draw_judgment(w, y, &c, &offset, caret_offset, TRUE, inputstr, rule->conclusion, workspace_mode); draw_slot(w, y, &r, &offset, caret_offset, TRUE, @@ -847,5 +852,6 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset, draw_slot(w, y, x, &offset, caret_offset, virtual, offset == caret_offset ? inputstr : rule->name, FALSE); } - *y = row + (stack_p ? n + (is_dot ? 1 : 0) + 2 : 3); *x = col + (lw + c) / 2; + *y = (stack_p ? n + (is_dot ? 1 : 0) + 2 : 3); + *x = lw + r + 1; } diff --git a/src/v.c b/src/v.c index 3b74d2c..7872457 100644 --- a/src/v.c +++ b/src/v.c @@ -43,14 +43,15 @@ struct state enum ui_input_mode input_mode; struct rule *rule; struct point *slot; - WINDOW *workspace_w; - WINDOW *support_w; - WINDOW *echo_w; + WINDOW *workspace; + WINDOW *status_bar; + WINDOW *echo_area; GHashTable *rules; /* str -> rule */ GHashTable *globals; /* str -> name */ GHashTable *temporaries; /* str -> name */ GHashTable *gctxs; /* str -> name */ GHashTable *gtheses; /* str -> name */ + GSList *ordered_rules; /* rule names */ GSList *support; /* rules */ GString *input; GString *special; @@ -188,6 +189,13 @@ insert_name(GHashTable *temporaries, struct name *name) g_hash_table_insert(temporaries, name->str, name); } +void +insert_rule(struct state *state, struct rule *rule) +{ + g_hash_table_insert(state->rules, rule->name, rule); + state->ordered_rules = g_slist_prepend(state->ordered_rules, rule->name); +} + /* * Remove entries with contextual scope. This is the end of the line for * variables. @@ -255,7 +263,7 @@ render_splash(struct state *state) strs[i]); } if (state->input_mode == ui_input_mode_command) - echo_esc(state->echo_w, state->command->str); + echo_esc(state->echo_area, state->command->str); refresh(); } @@ -272,7 +280,7 @@ render_help(struct state *state) addch(c); fclose(fd); if (state->input_mode == ui_input_mode_command) - echo_esc(state->echo_w, state->command->str); + echo_esc(state->echo_area, state->command->str); refresh(); } @@ -318,118 +326,154 @@ echo_status(WINDOW *w, int status) wattroff(w, COLOR_PAIR(pair)); } +int +status_bar_str(char *buf, size_t len, + enum ui_major_mode major_mode, enum ui_input_mode input_mode, + struct point *p, char *input, char key, GHashTable *temporaries) +{ + int n = 0; + GSList *l; + GList *head, *l1; + + n += snprintf(buf, len, " %d:%d (%d,%d,%d,%d,[", + major_mode, input_mode, + p->is_conclusion, + p->st, + p->judgment_idx, + p->vdecl_idx); + l = p->stack; + if (!l) + n += snprintf(buf + n, len - n, "NULL])"); + while (l) { + n += snprintf(buf + n, len - n, "%d", GPOINTER_TO_INT(l->data)); + if (l->next) + n += snprintf(buf + n, len - n, ","); + else + n += snprintf(buf + n, len - n, "])"); + l = l->next; + } + n += snprintf(buf + n, len - n, " \"%s\"", input); + if (key > 31 && key < 127) + n += snprintf(buf + n, len - n, " '%c'", key); + else if (key == '\t') + n += snprintf(buf + n, len - n, " 'TAB'"); + else if (key == '\n') + n += snprintf(buf + n, len - n, " 'RET'"); + else if (key == 27) + n += snprintf(buf + n, len - n, " 'ESC'"); + else + n += snprintf(buf + n, len - n, " UNKNOWN_KEY"); + head = g_hash_table_get_keys(temporaries); + if (head) + n += snprintf(buf + n, len - n, " "); + l1 = head; + while (l1) { + n += snprintf(buf + n, len - n, "%s", l1->data); + if (l1->next) + n += snprintf(buf + n, len - n, " "); + l1 = l1->next; + } + n += snprintf(buf + n, len - n, " "); + g_list_free(head); + return n; +} + void render(struct state *state, char kkey) { - int y, x, q, i, caret_offset; + int caret_offset; + int y, x, h, w, h1, w1, yoff, xoff, maxw, maxn, n; static const char *str1 = "g: generic t: type e: element " "=t: judgmentally equal types =e: judgmentally equal elements"; static const char *str2 = "=t: judgmentally equal types " "=e: judgmentally equal elements"; - GHashTableIter iter; - /* GSList *l, *deps; */ - GList *head, *l1; + char buf[COLS]; GSList *l; - gpointer key, value; struct rule *rule; struct point *p; - q = (LINES - 3) / 2; clear(); - /* draw debug info */ - i = 0; - head = g_hash_table_get_keys(state->temporaries); - l1 = head; - while (l1) { - mvwprintw(stdscr, LINES - 4, i, "%s", l1->data); - i += strlen(l1->data) + 1; - l1 = l1->next; - } - g_list_free(head); - mvwprintw(stdscr, LINES - 3, 0, - "major_mode: %d input_mode: %d is_conclusion: %d " - "st: %d j_idx: %d v_idx: %d ", - state->major_mode, state->input_mode, - state->slot->is_conclusion, - state->slot->st, - state->slot->judgment_idx, - state->slot->vdecl_idx); - wprintw(stdscr, "stack: "); - l = state->slot->stack; - if (!l) - wprintw(stdscr, "NULL "); - while (l) { - wprintw(stdscr, "%d ", GPOINTER_TO_INT(l->data)); - l = l->next; - } - wprintw(stdscr, " inputstr: %s key: %d", - state->input->str, - kkey); - /* draw workspace rule */ - y = 0; x = 0; p = create_point(FALSE, state->rule->hypotheses ? slot_type_ctx_l : slot_type_rule_dots, 0, 0, NULL); caret_offset = point_distance(state->rule, p, state->slot); free_point(p); - draw_rule(state->workspace_w, &y, &x, caret_offset, + h = 0; w = 0; + draw_rule(state->workspace, &h, &w, caret_offset, + TRUE, state->input->str, state->rule, TRUE); + y = (LINES - 2 - h) / 2; x = (COLS - w) / 2; + draw_rule(state->workspace, &y, &x, caret_offset, FALSE, state->input->str, state->rule, TRUE); /* draw existing rules */ - i = 0; - g_hash_table_iter_init(&iter, state->rules); - while (g_hash_table_iter_next(&iter, &key, &value)) + yoff = 0; + maxw = 0; maxn = 0; + l = state->ordered_rules; + while (l) + { + rule = g_hash_table_lookup(state->rules, l->data); + h1 = 0; w1 = 0; + draw_rule(state->workspace, &h1, &w1, -1, + TRUE, NULL, rule, FALSE); + if (yoff + h1 + 1 > LINES - 2) + break; + if (w1 > maxw) + maxw = w1; + if (maxn < (n = mbstowcs(NULL, rule->name, 0))) + maxn = n; + yoff += h1 + 1; + l = l->next; + } + yoff = 0; + l = state->ordered_rules; + while (l) { - rule = value; - y = i; x = 0; - draw_rule(state->support_w, &y, &x, -1, + rule = g_hash_table_lookup(state->rules, l->data); + h1 = 0; w1 = 0; + draw_rule(state->workspace, &h1, &w1, -1, + TRUE, NULL, rule, FALSE); + n = mbstowcs(NULL, rule->name, 0); + if (yoff + h1 + 1 > (LINES - 2 - h) / 2 && + yoff < (LINES - 2 + h) / 2 && + COLS - 1 - maxn - 1 - (w1 - n - 1) < (COLS + w) / 2) + yoff = (LINES - 2 + h) / 2 + 1; + if (yoff + h1 + 1 > LINES - 2) + break; + y = yoff; x = COLS - 1 - (maxn - n) - w1; + draw_rule(state->workspace, &y, &x, -1, FALSE, NULL, rule, FALSE); - i = y + 1; + yoff += h1 + 1; + l = l->next; } - /* /\* draw support rules *\/ */ - /* i = 0; */ - /* l = state->support; */ - /* while (l) */ - /* { */ - /* rule = l->data; */ - /* y = i; x = 0; */ - /* draw_rule(state->support_w, &y, &x, FALSE, FALSE, -1, NULL, rule); */ - /* i = y + 2; */ - /* l = l->next; */ - /* } */ - - /* draw window names and boundaries */ - attron(COLOR_PAIR(PAIR_INVERSE)); - move(q, 0); - printw("workspace%*s", COLS - NB_COLUMNS - 1 - 9, ""); - move(LINES - 2, 0); - printw("support%*s", COLS - NB_COLUMNS - 1 - 7, ""); - move(LINES - 2, COLS - NB_COLUMNS); - printw("rules%*s", NB_COLUMNS - 5, ""); - attroff(COLOR_PAIR(PAIR_INVERSE)); - for (i = 0 ; i < LINES - 1 ; i++) - mvprintw(i, COLS - NB_COLUMNS - 1, "█"); + /* status bar */ + n = status_bar_str(buf, sizeof(buf), + state->major_mode, state->input_mode, + state->slot, state->input->str, kkey, + state->temporaries); + wattron(state->status_bar, COLOR_PAIR(PAIR_INVERSE)); + mvwprintw(state->status_bar, 0, (COLS - n) / 2, buf); + wattroff(state->status_bar, COLOR_PAIR(PAIR_INVERSE)); - /* draw echo area */ + /* echo area */ if (state->input_mode == ui_input_mode_command) - echo_esc(state->echo_w, state->command->str); + echo_esc(state->echo_area, state->command->str); else if (state->err) { - echo_status(state->echo_w, state->err); + echo_status(state->echo_area, state->err); state->err = 0; } else { if (state->slot->st == slot_type_thesis) { if (state->status == 0) - mvwprintw(state->echo_w, 0, 0, str1); + mvwprintw(state->echo_area, 0, 0, str1); else - mvwprintw(state->echo_w, 0, 0, str2); + mvwprintw(state->echo_area, 0, 0, str2); } else if (state->input_mode == ui_input_mode_special_characters) { - mvwprintw(state->echo_w, 0, 0, "\\"); - wprintw(state->echo_w, state->special->str); + mvwprintw(state->echo_area, 0, 0, "\\"); + wprintw(state->echo_area, state->special->str); } } @@ -771,7 +815,7 @@ validate_rule_name(struct state *state) if (g_hash_table_lookup(state->rules, state->input->str)) return 2; rule->name = strdup(state->input->str); - g_hash_table_insert(state->rules, state->rule->name, rule); + insert_rule(state, rule); c = rule->conclusion; switch (c->kind) { case thesis_kind_type: @@ -1055,6 +1099,9 @@ main() gpointer hkey, hvalue; struct state state; + int n = 0; + char cmd[100]; + setlocale(LC_ALL, ""); initscr(); start_color(); @@ -1076,9 +1123,9 @@ main() state.input_mode = ui_input_mode_default; state.rule = create_rule(); state.slot = create_point(FALSE, slot_type_rule_dots, 0, 0, NULL); - state.workspace_w = subwin(stdscr, q, COLS - NB_COLUMNS - 1, 0, 0); - state.support_w = subwin(stdscr, LINES - 1, NB_COLUMNS, 0, COLS - NB_COLUMNS); - state.echo_w = subwin(stdscr, 1, COLS, LINES - 1, 0); + state.workspace = subwin(stdscr , LINES - 2, COLS, 0 , 0); + state.status_bar = subwin(stdscr, 1 , COLS, LINES - 2, 0); + state.echo_area = subwin(stdscr , 1 , COLS, LINES - 1, 0); state.rules = g_hash_table_new_full(g_str_hash, g_str_equal, NULL, (GDestroyNotify)free_rule); state.globals = g_hash_table_new_full(g_str_hash, g_str_equal, @@ -1086,9 +1133,10 @@ main() str = strdup("Small"); small = create_name(scope_global, name_kind_vet, NULL, NULL, NULL, str); g_hash_table_insert(state.globals, str, small); + state.temporaries = g_hash_table_new(g_str_hash, g_str_equal); state.gctxs = g_hash_table_new(g_str_hash, g_str_equal); state.gtheses = g_hash_table_new(g_str_hash, g_str_equal); - state.temporaries = g_hash_table_new(g_str_hash, g_str_equal); + state.ordered_rules = NULL; state.support = NULL; state.input = g_string_new(NULL); state.special = g_string_new(NULL); @@ -1147,9 +1195,9 @@ main() default: } } - delwin(state.workspace_w); - delwin(state.support_w); - delwin(state.echo_w); + delwin(state.workspace); + delwin(state.status_bar); + delwin(state.echo_area); endwin(); g_hash_table_iter_init(&iter, special_character_map); while (g_hash_table_iter_next(&iter, &hkey, &hvalue)) @@ -1162,6 +1210,7 @@ main() g_hash_table_destroy(state.gctxs); g_hash_table_destroy(state.gtheses); g_hash_table_destroy(state.temporaries); + g_slist_free(state.ordered_rules); g_slist_free(state.support); g_string_free(state.input, TRUE); g_string_free(state.special, TRUE); -- 2.39.5