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 π‘
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;
}
}
}
+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);
}
}
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;
+}
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,
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);
void free_judgment(struct judgment *judgment);
+void free_node(struct node *node);
+
void free_rule(struct rule *rule);
GSList *list_reference_names(GSList *list,
struct reference *copy_reference(struct reference *reference);
+struct judgment *get_tree_conclusion(GNode *tree);
+
#endif
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)
{
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;
}
int c, m, n, r, lw, s, ow, row, col;
int offset;
int point, pair, spaces;
- GSList *l;
+ GNode *gn;
c = 0;
m = 0;
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;
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);
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,
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);
ui_major_mode_help,
ui_major_mode_splash,
ui_major_mode_workspace,
+ ui_major_mode_derivation,
};
/* The editor's input mode. */
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,
{
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;
/* 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);
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();
}
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 {
}
}
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) {
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;
}
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);
}
}
+void
+handle_derivation_input(struct state *state, wint_t key)
+{
+ if (!handle_esc(state, key)) {
+ }
+}
+
int
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);
case ui_major_mode_workspace:
handle_workspace_input(&state, key);
break;
+ case ui_major_mode_derivation:
+ handle_derivation_input(&state, key);
+ break;
default:
}
case ui_major_mode_workspace:
render(&state, key);
break;
+ case ui_major_mode_derivation:
+ render_derivation(&state);
+ break;
default:
}
}
projects / vouivre.git / commitdiff