From d2169648aecdbfe52d7d8e471b2738cb6a3cd082 Mon Sep 17 00:00:00 2001 From: admin Date: Tue, 5 Nov 2024 15:08:11 -0500 Subject: [PATCH] Adapt rules to support general derivations --- help.txt | 42 +++++++++++----------- src/name.c | 44 +++++++++++++++++++---- src/name.h | 29 +++++++++++++-- src/ui.c | 39 ++++++++++---------- src/ui.h | 1 + src/v.c | 102 ++++++++++++++++++++++++++++++++++++++--------------- 6 files changed, 179 insertions(+), 78 deletions(-) diff --git a/help.txt b/help.txt index d8d4001..cb81e1e 100644 --- a/help.txt +++ b/help.txt @@ -18,24 +18,24 @@ RET add an item when on a '...' slot 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 𝟡 +\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/name.c b/src/name.c index 49a90ce..bf10743 100644 --- a/src/name.c +++ b/src/name.c @@ -63,16 +63,25 @@ create_judgment(enum thesis_kind kind, return j; } +struct node * +create_node(struct judgment *conclusion, struct rule *step) +{ + struct node *node; + + node = malloc(sizeof(struct node)); + node->conclusion = conclusion; + node->step = step; + return node; +} + struct rule * -create_rule() +create_rule(const char *name, GNode *tree) { struct rule *rule; rule = malloc(sizeof(struct rule)); rule->name = NULL; - rule->hypotheses = NULL; - rule->conclusion = create_judgment(thesis_kind_unknown, - NULL, NULL, NULL, NULL, NULL); + rule->tree = tree; return rule; } @@ -109,13 +118,28 @@ free_judgment(struct judgment *judgment) } } +void +free_node(struct node *node) +{ + free_judgment(node->conclusion); + free(node); +} + +gboolean +free_gnode_data(GNode *gnode, gpointer data) +{ + free_node(g_steal_pointer(&gnode->data)); + return FALSE; +} + void free_rule(struct rule *rule) { if (rule) { free(rule->name); - g_slist_free_full(rule->hypotheses, (GDestroyNotify)free_judgment); - free_judgment(rule->conclusion); + g_node_traverse(rule->tree, G_IN_ORDER, G_TRAVERSE_ALL, -1, + (GNodeTraverseFunc)free_gnode_data, NULL); + g_node_destroy(rule->tree); free(rule); } } @@ -219,3 +243,11 @@ copy_reference(struct reference *reference) g_slist_copy_deep(reference->replacements, (GCopyFunc)copy_reference, NULL)); } + +struct judgment * +get_tree_conclusion(GNode *tree) +{ + if (tree && tree->data) + return ((struct node *)tree->data)->conclusion; + return NULL; +} diff --git a/src/name.h b/src/name.h index 99187e9..18c6816 100644 --- a/src/name.h +++ b/src/name.h @@ -92,11 +92,27 @@ struct judgment GSList *vdecls; /* names */ }; +/* + * A node has a conclusion (judgment) that results from the application of a + * derivation step (a rule) to the leaves of its GNode. When the step is NULL + * it indicates that the conclusion was formulated as a rule of the theory + * instead of derived. + */ +struct node +{ + struct judgment *conclusion; + struct rule *step; +}; + +/* + * A rule, whether given (NULL root step) or derived, has a name and a tree. + * The tree gives the judgments involved, and, when the rule is derived, the + * corresponding derivation steps. + */ struct rule { char *name; - GSList *hypotheses; /* judgments */ - struct judgment *conclusion; + GNode *tree; /* nodes */ }; struct name *create_name(enum scope scope, @@ -116,7 +132,10 @@ struct judgment *create_judgment(enum thesis_kind kind, struct reference *b, GSList *vdecls); -struct rule *create_rule(); +struct node *create_node(struct judgment *conclusion, + struct rule *step); + +struct rule *create_rule(const char *name, GNode *tree); void free_name(struct name *name); @@ -124,6 +143,8 @@ void free_reference(struct reference *reference); void free_judgment(struct judgment *judgment); +void free_node(struct node *node); + void free_rule(struct rule *rule); GSList *list_reference_names(GSList *list, @@ -137,4 +158,6 @@ GSList *list_out_of_scope_names(GSList *dependencies, struct reference *copy_reference(struct reference *reference); +struct judgment *get_tree_conclusion(GNode *tree); + #endif diff --git a/src/ui.c b/src/ui.c index 171a312..5141f00 100644 --- a/src/ui.c +++ b/src/ui.c @@ -73,12 +73,12 @@ struct judgment * get_slot_judgment(struct rule *rule, struct point *slot) { if (slot->is_conclusion) - return rule->conclusion; + return get_tree_conclusion(rule->tree); else - return g_slist_nth_data(rule->hypotheses, slot->judgment_idx); + return get_tree_conclusion(g_node_nth_child(rule->tree, + slot->judgment_idx)); } - struct reference * get_replacement_(struct reference *ref, GSList *stack) { @@ -183,15 +183,15 @@ next_thesis_slot_type(enum thesis_kind tk) void next_after_thesis_slot(struct point *slot, struct rule *rule) { - GSList *l; + GNode *gn; if (slot->is_conclusion) { slot->is_conclusion = FALSE; slot->st = slot_type_rule_name; } else { - l = g_slist_nth(rule->hypotheses, slot->judgment_idx); - if (l && l->next) { + gn = g_node_nth_child(rule->tree, slot->judgment_idx); + if (gn && g_node_next_sibling(gn)) { slot->st = slot_type_ctx_l; slot->judgment_idx += 1; } @@ -767,7 +767,7 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset, int c, m, n, r, lw, s, ow, row, col; int offset; int point, pair, spaces; - GSList *l; + GNode *gn; c = 0; m = 0; @@ -782,15 +782,16 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset, is_dot = FALSE; offset = 0; - l = rule->hypotheses; - while (l) { + + gn = g_node_first_child(rule->tree); + while (gn) { *y = 0; *x = 0; - draw_judgment(w, y, x, &offset, caret_offset, TRUE, inputstr, l->data, - workspace_mode); + draw_judgment(w, y, x, &offset, caret_offset, TRUE, inputstr, + get_tree_conclusion(gn), workspace_mode); s += *x; m = m > *x ? m : *x; n += 1; - l = l->next; + gn = g_node_next_sibling(gn); } if (workspace_mode && (offset >= caret_offset)) { is_dot = TRUE; @@ -800,7 +801,7 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset, else offset += 1; draw_judgment(w, y, &c, &offset, caret_offset, TRUE, inputstr, - rule->conclusion, workspace_mode); + get_tree_conclusion(rule->tree), workspace_mode); draw_slot(w, y, &r, &offset, caret_offset, TRUE, offset == caret_offset ? inputstr : rule->name, FALSE); @@ -824,17 +825,17 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset, if (!stack_p) *x += spaces; point = 0; - l = rule->hypotheses; - while (l) { - draw_judgment(w, y, x, &offset, caret_offset, FALSE, inputstr, l->data, - workspace_mode); + gn = g_node_first_child(rule->tree); + while (gn) { + draw_judgment(w, y, x, &offset, caret_offset, FALSE, inputstr, + get_tree_conclusion(gn), workspace_mode); if (!stack_p) *x += spaces; else { *y += 1; *x = col; } - l = l->next; + gn = g_node_next_sibling(gn); } if (workspace_mode && (offset >= caret_offset)) draw_slot(w, y, x, &offset, caret_offset, virtual, @@ -847,7 +848,7 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset, wprintw(w, "="); *y += 1; *x = col + (lw - c) / 2; draw_judgment(w, y, x, &offset, caret_offset, virtual, inputstr, - rule->conclusion, workspace_mode); + get_tree_conclusion(rule->tree), workspace_mode); *y -= 1; *x = col + lw + 1; draw_slot(w, y, x, &offset, caret_offset, virtual, offset == caret_offset ? inputstr : rule->name, FALSE); diff --git a/src/ui.h b/src/ui.h index 88bc8d1..0df3eb9 100644 --- a/src/ui.h +++ b/src/ui.h @@ -38,6 +38,7 @@ enum ui_major_mode ui_major_mode_help, ui_major_mode_splash, ui_major_mode_workspace, + ui_major_mode_derivation, }; /* The editor's input mode. */ diff --git a/src/v.c b/src/v.c index 7872457..223887c 100644 --- a/src/v.c +++ b/src/v.c @@ -326,6 +326,34 @@ echo_status(WINDOW *w, int status) wattroff(w, COLOR_PAIR(pair)); } +void +draw_echo_area(struct state *state) +{ + 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"; + + if (state->input_mode == ui_input_mode_command) + echo_esc(state->echo_area, state->command->str); + else if (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_area, 0, 0, str1); + else + mvwprintw(state->echo_area, 0, 0, str2); + } + else if (state->input_mode == ui_input_mode_special_characters) { + mvwprintw(state->echo_area, 0, 0, "\\"); + wprintw(state->echo_area, state->special->str); + } + } +} + int status_bar_str(char *buf, size_t len, enum ui_major_mode major_mode, enum ui_input_mode input_mode, @@ -383,10 +411,6 @@ render(struct state *state, char kkey) { 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"; char buf[COLS]; GSList *l; struct rule *rule; @@ -396,7 +420,7 @@ render(struct state *state, char kkey) /* draw workspace rule */ p = create_point(FALSE, - state->rule->hypotheses ? slot_type_ctx_l : + state->rule->tree->children ? slot_type_ctx_l : slot_type_rule_dots, 0, 0, NULL); caret_offset = point_distance(state->rule, p, state->slot); free_point(p); @@ -458,24 +482,17 @@ render(struct state *state, char kkey) wattroff(state->status_bar, COLOR_PAIR(PAIR_INVERSE)); /* echo area */ - if (state->input_mode == ui_input_mode_command) - echo_esc(state->echo_area, state->command->str); - else if (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_area, 0, 0, str1); - else - mvwprintw(state->echo_area, 0, 0, str2); - } - else if (state->input_mode == ui_input_mode_special_characters) { - mvwprintw(state->echo_area, 0, 0, "\\"); - wprintw(state->echo_area, state->special->str); - } - } + draw_echo_area(state); + + refresh(); +} + +void +render_derivation(struct state *state) +{ + clear(); + + draw_echo_area(state); refresh(); } @@ -509,6 +526,11 @@ handle_esc(struct state *state, wint_t key) state->command = g_string_erase(state->command, 0, -1); state->input_mode = ui_input_mode_default; } + else if (strcmp(state->command->str, "d") == 0) { + state->major_mode = ui_major_mode_derivation; + state->command = g_string_erase(state->command, 0, -1); + state->input_mode = ui_input_mode_default; + } else { } } @@ -816,7 +838,7 @@ validate_rule_name(struct state *state) return 2; rule->name = strdup(state->input->str); insert_rule(state, rule); - c = rule->conclusion; + c = get_tree_conclusion(rule->tree); switch (c->kind) { case thesis_kind_type: if (c->a->origin->scope == scope_global) { @@ -833,7 +855,12 @@ validate_rule_name(struct state *state) default: } state->input = g_string_erase(state->input, 0, -1); - state->rule = create_rule(); + state->rule = + create_rule(NULL, + g_node_new(create_node(create_judgment(thesis_kind_unknown, + NULL, NULL, NULL, NULL, + NULL), + NULL))); clear_locals(state); return 0; } @@ -849,10 +876,9 @@ handle_workspace_input(struct state *state, wint_t key) if (state->slot->st == slot_type_rule_dots) { judgment = create_judgment(thesis_kind_unknown, NULL, NULL, NULL, NULL, NULL); - state->rule->hypotheses = g_slist_append(state->rule->hypotheses, - judgment); + g_node_append(state->rule->tree, g_node_new(create_node(judgment, NULL))); state->slot->st = slot_type_ctx_l; - state->slot->judgment_idx = g_slist_index(state->rule->hypotheses, judgment); + state->slot->judgment_idx = g_node_n_children(state->rule->tree) - 1; } else if (state->slot->st == slot_type_ctx_dots) { judgment = get_slot_judgment(state->rule, state->slot); @@ -1087,6 +1113,13 @@ handle_workspace_input(struct state *state, wint_t key) } } +void +handle_derivation_input(struct state *state, wint_t key) +{ + if (!handle_esc(state, key)) { + } +} + int main() { @@ -1121,7 +1154,12 @@ main() state.running = TRUE; state.major_mode = ui_major_mode_splash; state.input_mode = ui_input_mode_default; - state.rule = create_rule(); + state.rule = + create_rule(NULL, + g_node_new(create_node(create_judgment(thesis_kind_unknown, + NULL, NULL, NULL, NULL, + NULL), + NULL))); state.slot = create_point(FALSE, slot_type_rule_dots, 0, 0, NULL); state.workspace = subwin(stdscr , LINES - 2, COLS, 0 , 0); state.status_bar = subwin(stdscr, 1 , COLS, LINES - 2, 0); @@ -1178,6 +1216,9 @@ main() case ui_major_mode_workspace: handle_workspace_input(&state, key); break; + case ui_major_mode_derivation: + handle_derivation_input(&state, key); + break; default: } @@ -1192,6 +1233,9 @@ main() case ui_major_mode_workspace: render(&state, key); break; + case ui_major_mode_derivation: + render_derivation(&state); + break; default: } } -- 2.39.5