--- /dev/null
+/* Copyright (C) 2024 Vouivre Digital Corporation
+ *
+ * This file is part of Vouivre.
+ *
+ * Vouivre is free software: you can redistribute it and/or
+ * modify it under the terms of the GNU General Public
+ * License as published by the Free Software Foundation, either
+ * version 3 of the License, or (at your option) any later version.
+ *
+ * Vouivre is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public
+ * License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "name.h"
+#include "ui.h"
+
+#include <glib.h>
+#include <locale.h>
+
+#define NCURSES_WIDECHAR 1
+#include <ncurses.h>
+
+gpointer
+copy_int_pointer(gconstpointer src, gpointer data)
+{
+ return GINT_TO_POINTER(GPOINTER_TO_INT(src));
+}
+
+struct point *
+create_point(bool is_conclusion, enum slot_type st,
+ int judgment_idx, int vdecl_idx,
+ GSList *stack)
+{
+ struct point *p;
+
+ p = malloc(sizeof(struct point));
+ p->is_conclusion = is_conclusion;
+ p->st = st;
+ p->judgment_idx = judgment_idx;
+ p->vdecl_idx = vdecl_idx;
+ p->stack = stack;
+ return p;
+}
+
+void
+free_point(struct point *p)
+{
+ g_slist_free(p->stack);
+ free(p);
+}
+
+struct point *
+copy_point(struct point *p)
+{
+ return create_point(p->is_conclusion,
+ p->st,
+ p->judgment_idx,
+ p->vdecl_idx,
+ g_slist_copy_deep(p->stack, copy_int_pointer, NULL));
+}
+
+/* /\* struct point *\/ */
+/* /\* prev_slot(struct rule *rule, struct point slot) *\/ */
+/* /\* { *\/ */
+/* /\* } *\/ */
+
+struct judgment *
+get_slot_judgment(struct rule *rule, struct point *slot)
+{
+ if (slot->is_conclusion)
+ return rule->conclusion;
+ else
+ return g_slist_nth_data(rule->hypotheses, slot->judgment_idx);
+}
+
+
+struct reference *
+get_replacement_(struct reference *ref, GSList *stack)
+{
+ if (!stack)
+ return ref;
+ return get_replacement_(g_slist_nth_data(ref->replacements,
+ GPOINTER_TO_INT(stack->data)),
+ stack->next);
+}
+
+struct reference *
+get_replacement(struct reference *ref, GSList *stack)
+{
+ GSList *l;
+
+ l = g_slist_reverse(g_slist_copy_deep(stack, copy_int_pointer, NULL));
+ ref = get_replacement_(ref, l);
+ g_slist_free(l);
+ return ref;
+}
+
+void *
+get_slot_data(struct rule *rule, struct point *slot, GSList *stack)
+{
+ struct judgment *judgment;
+ GSList *l;
+
+ judgment = get_slot_judgment(rule, slot);
+ switch (slot->st) {
+ case slot_type_ctx_l:
+ return judgment->generic_l;
+ break;
+ case slot_type_ctx_v:
+ l = g_slist_nth(judgment->vdecls, slot->vdecl_idx);
+ return l->data;
+ break;
+ case slot_type_ctx_t:
+ l = g_slist_nth(judgment->vdecls, slot->vdecl_idx);
+ return get_replacement(((struct name *)l->data)->type, stack);
+ break;
+ case slot_type_ctx_r:
+ return get_replacement(judgment->generic_r, stack);
+ break;
+ case slot_type_generic_thesis:
+ return get_replacement(judgment->a, stack);
+ break;
+ case slot_type_type_thesis:
+ return get_replacement(judgment->a, stack);
+ break;
+ case slot_type_element_thesis_element:
+ return get_replacement(judgment->a, stack);
+ break;
+ case slot_type_element_thesis_type:
+ return get_replacement(judgment->a->origin->type, stack);
+ break;
+ case slot_type_type_equal_thesis_type_1:
+ return get_replacement(judgment->a, stack);
+ break;
+ case slot_type_type_equal_thesis_type_2:
+ return get_replacement(judgment->b, stack);
+ break;
+ case slot_type_element_equal_thesis_element_1:
+ return get_replacement(judgment->a, stack);
+ break;
+ case slot_type_element_equal_thesis_element_2:
+ return get_replacement(judgment->b, stack);
+ break;
+ case slot_type_element_equal_thesis_type:
+ return get_replacement(judgment->a->origin->type, stack);
+ break;
+ default:
+ return NULL;
+ }
+}
+
+enum slot_type
+next_thesis_slot_type(enum thesis_kind tk)
+{
+ switch (tk) {
+ case thesis_kind_generic:
+ return slot_type_generic_thesis;
+ break;
+ case thesis_kind_type:
+ return slot_type_type_thesis;
+ break;
+ case thesis_kind_element:
+ return slot_type_element_thesis_element;
+ break;
+ case thesis_kind_type_equal:
+ return slot_type_type_equal_thesis_type_1;
+ break;
+ case thesis_kind_element_equal:
+ return slot_type_element_equal_thesis_element_1;
+ break;
+ case thesis_kind_unknown:
+ return slot_type_thesis;
+ break;
+ default:
+ }
+}
+
+void
+next_after_thesis_slot(struct point *slot, struct rule *rule)
+{
+ GSList *l;
+
+ 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) {
+ slot->st = slot_type_ctx_l;
+ slot->judgment_idx += 1;
+ }
+ else {
+ slot->st = slot_type_rule_dots;
+ slot->judgment_idx = 0;
+ }
+ }
+}
+
+void
+first_replacement(struct point *slot)
+{
+ slot->stack = g_slist_prepend(slot->stack, 0);
+}
+
+void
+next_slot(struct point *slot, struct rule *rule)
+{
+ bool skip;
+ int idx;
+ GSList *l;
+ struct judgment *judgment;
+ struct reference *ref, *rep;
+ struct point *pslot;
+
+ skip = FALSE;
+ judgment = get_slot_judgment(rule, slot);
+ next_replacement:
+ if (slot->stack) {
+ skip = TRUE;
+ ref = get_slot_data(rule, slot, slot->stack->next);
+ idx = GPOINTER_TO_INT(slot->stack->data);
+ rep = get_slot_data(rule, slot, slot->stack);
+
+ /* If the replacement has replacements we're going in. */
+ if (rep->replacements)
+ slot->stack = g_slist_prepend(slot->stack, 0);
+ else {
+ l = g_slist_nth(ref->replacements, idx);
+ /* Otherwise, if there is a neighbour at the same level we go there. */
+ if (l->next) {
+ slot->stack->data = GINT_TO_POINTER(idx + 1);
+ }
+ /* Otherwise, recurse with the parent, but one step to the right. Note
+ that it's possible that there is nothing right. This is handled by
+ the "nothing right" block above. */
+ else {
+ do {
+ ref = get_slot_data(rule, slot, slot->stack->next);
+ idx = GPOINTER_TO_INT(slot->stack->data);
+ l = slot->stack;
+ slot->stack = l->next;
+ g_slist_free_1(l);
+ if (slot->stack)
+ slot->stack->data =
+ GINT_TO_POINTER(GPOINTER_TO_INT(slot->stack->data) + 1);
+ } while (slot->stack && idx >= g_slist_length(ref->replacements));
+ if (!slot->stack)
+ goto next_replacement;
+ }
+ }
+ }
+ else {
+ switch (slot->st) {
+ case slot_type_rule_dots:
+ slot->st = slot_type_ctx_l;
+ slot->is_conclusion = TRUE;
+ break;
+ case slot_type_ctx_l:
+ if (!skip && judgment->generic_l && judgment->generic_l->replacements)
+ first_replacement(slot);
+ else if (!judgment->vdecls)
+ slot->st = slot_type_ctx_dots;
+ else
+ slot->st = slot_type_ctx_v;
+ break;
+ case slot_type_ctx_v:
+ slot->st = slot_type_ctx_t;
+ break;
+ case slot_type_ctx_t:
+ l = g_slist_nth(judgment->vdecls, slot->vdecl_idx);
+ if (!skip && l && l->data && ((struct name *)l->data)->type &&
+ ((struct name *)l->data)->type->replacements)
+ first_replacement(slot);
+ else if (l && l->next) {
+ slot->st = slot_type_ctx_v;
+ slot->vdecl_idx += 1;
+ }
+ else {
+ slot->st = slot_type_ctx_dots;
+ slot->vdecl_idx = 0;
+ }
+ break;
+ case slot_type_ctx_dots:
+ slot->st = slot_type_ctx_r;
+ break;
+ case slot_type_ctx_r:
+ if (!skip && judgment->generic_r && judgment->generic_r->replacements)
+ first_replacement(slot);
+ else
+ slot->st = next_thesis_slot_type(judgment->kind);
+ break;
+ case slot_type_thesis:
+ slot->st = next_thesis_slot_type(judgment->kind);
+ break;
+ case slot_type_generic_thesis:
+ if (!skip && judgment->a->replacements)
+ first_replacement(slot);
+ else
+ next_after_thesis_slot(slot, rule);
+ break;
+ case slot_type_type_thesis:
+ if (!skip && judgment->a->replacements)
+ first_replacement(slot);
+ else
+ next_after_thesis_slot(slot, rule);
+ break;
+ case slot_type_element_thesis_element:
+ if (!skip && judgment->a->replacements)
+ first_replacement(slot);
+ else
+ slot->st = slot_type_element_thesis_type;
+ break;
+ case slot_type_element_thesis_type:
+ if (!skip && judgment->a->origin->type->replacements)
+ first_replacement(slot);
+ else
+ next_after_thesis_slot(slot, rule);
+ break;
+ case slot_type_type_equal_thesis_type_1:
+ if (!skip && judgment->a->replacements)
+ first_replacement(slot);
+ else
+ slot->st = slot_type_type_equal_thesis_type_2;
+ break;
+ case slot_type_type_equal_thesis_type_2:
+ if (!skip && judgment->b->replacements)
+ first_replacement(slot);
+ else
+ next_after_thesis_slot(slot, rule);
+ break;
+ case slot_type_element_equal_thesis_element_1:
+ if (!skip && judgment->a->replacements)
+ first_replacement(slot);
+ else
+ slot->st = slot_type_element_equal_thesis_element_2;
+ break;
+ case slot_type_element_equal_thesis_element_2:
+ if (!skip && judgment->b->replacements)
+ first_replacement(slot);
+ else
+ slot->st = slot_type_element_equal_thesis_type;
+ break;
+ case slot_type_element_equal_thesis_type:
+ if (!skip && judgment->a->origin->type->replacements)
+ first_replacement(slot);
+ else
+ next_after_thesis_slot(slot, rule);
+ break;
+ case slot_type_rule_name:
+ break;
+ default:
+ }
+ }
+}
+
+bool
+stack_loc_before_p(GSList *l1, GSList *l2)
+{
+ if (!l2)
+ return FALSE;
+ else if (!l1)
+ return TRUE;
+ else if (GPOINTER_TO_INT(l1->data) > GPOINTER_TO_INT(l2->data))
+ return FALSE;
+ else if (GPOINTER_TO_INT(l1->data) < GPOINTER_TO_INT(l2->data))
+ return TRUE;
+ else
+ return stack_loc_before_p(l1->next, l2->next);
+}
+
+bool
+point_before_p(struct rule *rule, struct point *p1, struct point *p2)
+{
+ if (p1->st == slot_type_rule_name)
+ return FALSE; /* rule name can't be before anything */
+ else if (p2->st == slot_type_rule_name)
+ return TRUE;
+ else if (p1->is_conclusion && !p2->is_conclusion)
+ return FALSE;
+ else if (!p1->is_conclusion && p2->is_conclusion)
+ return TRUE;
+ else if (p1->st == slot_type_rule_dots) /* rule dots can't be before anything */
+ return FALSE;
+ else if (p2->st == slot_type_rule_dots)
+ return TRUE;
+ else if (p1->judgment_idx > p2->judgment_idx)
+ return FALSE;
+ else if (p1->judgment_idx < p2->judgment_idx)
+ return TRUE;
+ else if (p1->st == p2->st && p1->vdecl_idx == p2->vdecl_idx)
+ return stack_loc_before_p(p1->stack, p2->stack);
+ else if (p2->st == slot_type_ctx_l)
+ return FALSE;
+ else if (p1->st == slot_type_ctx_l)
+ return TRUE;
+ else if ((p1->st == slot_type_ctx_v || p1->st == slot_type_ctx_t) &&
+ (p2->st == slot_type_ctx_v || p2->st == slot_type_ctx_t)) {
+ if (p1->vdecl_idx > p2->vdecl_idx)
+ return FALSE;
+ if (p1->vdecl_idx < p2->vdecl_idx)
+ return TRUE;
+ return p1->st < p2->st;
+ }
+ else if (p2->st == slot_type_ctx_v || p2->st == slot_type_ctx_t)
+ return FALSE;
+ else if (p1->st == slot_type_ctx_v || p1->st == slot_type_ctx_t)
+ return TRUE;
+ return p1->st < p2->st;
+}
+
+/* negative if p2 is before p1 and positive otherwise. */
+int
+point_distance(struct rule *rule, struct point *p1, struct point *p2)
+{
+ bool before;
+ int count = 0;
+ struct point *p_a, *p_b;
+
+ before = point_before_p(rule, p1, p2);
+ if (before) {
+ p_a = copy_point(p1);
+ p_b = p2;
+ }
+ else {
+ p_a = copy_point(p2);
+ p_b = p1;
+ }
+ while(point_before_p(rule, p_a, p_b)) {
+ if (p_a->st != slot_type_thesis)
+ count += 1;
+ next_slot(p_a, rule);
+ }
+ free_point(p_a);
+ return before ? count : -count;
+}
+
+bool
+empty_slot_p(struct rule *rule, struct point *slot)
+{
+ struct judgment *judgment;
+ struct name *name;
+
+ switch (slot->st) {
+ case slot_type_rule_dots:
+ return TRUE;
+ break;
+ case slot_type_ctx_l:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->generic_l &&
+ get_replacement(judgment->generic_l, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_ctx_v:
+ judgment = get_slot_judgment(rule, slot);
+ if (g_slist_nth_data(judgment->vdecls, slot->vdecl_idx))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_ctx_t:
+ judgment = get_slot_judgment(rule, slot);
+ name = g_slist_nth_data(judgment->vdecls, slot->vdecl_idx);
+ if (name && name->type &&
+ get_replacement(name->type, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_ctx_dots:
+ return TRUE;
+ break;
+ case slot_type_ctx_r:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->generic_r &&
+ get_replacement(judgment->generic_r, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_thesis:
+ return TRUE;
+ break;
+ case slot_type_generic_thesis:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->a &&
+ get_replacement(judgment->a, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_type_thesis:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->a &&
+ get_replacement(judgment->a, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_element_thesis_element:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->a &&
+ get_replacement(judgment->a, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_element_thesis_type:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->a &&
+ get_replacement(judgment->a->origin->type, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_type_equal_thesis_type_1:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->a &&
+ get_replacement(judgment->a, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_type_equal_thesis_type_2:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->b &&
+ get_replacement(judgment->b, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_element_equal_thesis_element_1:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->a &&
+ get_replacement(judgment->a, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_element_equal_thesis_element_2:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->b &&
+ get_replacement(judgment->b, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_element_equal_thesis_type:
+ judgment = get_slot_judgment(rule, slot);
+ if (judgment->a &&
+ get_replacement(judgment->a->origin->type, slot->stack))
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_rule_name:
+ if (rule->name)
+ return FALSE;
+ return TRUE;
+ break;
+ case slot_type_unknown:
+ return TRUE;
+ default:
+ }
+}
+
+void
+next_empty_slot(struct point *slot, struct rule *rule)
+{
+ do {
+ next_slot(slot, rule);
+ } while (!empty_slot_p(rule, slot));
+}
+
+void
+draw_delimiter(WINDOW *w, int *y, int *x, bool virtual, const char *str)
+{
+ if (!virtual)
+ mvwprintw(w, *y, *x, str);
+ *x += mbstowcs(NULL, str, 0);
+}
+
+void
+draw_slot(WINDOW *w, int *y, int *x, int *offset, int caret_offset,
+ bool virtual, const char *str, bool optional)
+{
+ int pair;
+
+ pair = *offset == caret_offset ? PAIR_HL : PAIR_NORMAL;
+ if (!virtual) {
+ wattron(w, COLOR_PAIR(pair));
+ wmove(w, *y, *x);
+ if (str && *str != '\0')
+ wprintw(w, str);
+ else {
+ wprintw(w, EMPTY_SLOT);
+ if (optional)
+ wprintw(w, "?");
+ }
+ wattroff(w, COLOR_PAIR(pair));
+ }
+ if (str && *str != '\0')
+ *x += mbstowcs(NULL, str, 0);
+ else {
+ if (optional)
+ *x += 2;
+ else
+ *x += 1;
+ }
+ *offset += 1;
+}
+
+void
+draw_input_slot(WINDOW *w, int *y, int *x, int *offset, int caret_offset,
+ bool virtual, const char *str, bool optional)
+{
+ draw_slot(w, y, x, offset, caret_offset, virtual,
+ *offset == caret_offset ? str : NULL, optional);
+}
+
+bool /* is displayed ? */
+draw_ref(WINDOW *w, int *y, int *x, int *offset, int caret_offset,
+ bool virtual, const char *inputstr, const struct reference *ref,
+ bool optional)
+{
+ GSList *l;
+
+ if (!ref) {
+ if (!optional || *offset >= caret_offset)
+ draw_input_slot(w, y, x, offset, caret_offset, virtual, inputstr,
+ optional);
+ else {
+ *offset += 1;
+ return FALSE;
+ }
+ }
+ else {
+ draw_slot(w, y, x, offset, caret_offset, virtual, ref->origin->str,
+ FALSE);
+ l = ref->replacements;
+ if (l) {
+ draw_delimiter(w, y, x, virtual, "[");
+ while (l) {
+ /* dep = TBD; */
+ /* l1 = list_out_of_scope_dependencies(name, temporaries); */
+ /* while (l1) { */
+ /* set_ctp_and_pair(&ctp, &pair, caret, (*point)++); */
+ /* draw_slot(w, y, x, virtual, FALSE, pair, NULL); */
+ /* if (l1->next) */
+ /* draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, ", "); */
+ /* else */
+ /* draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, ". "); */
+ /* l1 = l1->next; */
+ /* } */
+
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr, l->data,
+ FALSE);
+ l = l->next;
+ if (l)
+ draw_delimiter(w, y, x, virtual, ", ");
+ }
+ draw_delimiter(w, y, x, virtual, "]");
+ }
+ }
+ return TRUE;
+}
+
+void
+draw_judgment(WINDOW *w, int *y, int *x, int *offset, int caret_offset,
+ bool virtual, char *inputstr, struct judgment *judgment,
+ bool workspace_mode)
+{
+ bool is_prev_displayed;
+ int pair;
+ GSList *l;
+ struct name *var;
+
+ /* Γ */
+ is_prev_displayed = FALSE;
+ if (workspace_mode || judgment->generic_l) {
+ is_prev_displayed = draw_ref(w, y, x, offset, caret_offset,
+ virtual, inputstr, judgment->generic_l,
+ TRUE);
+ }
+
+ /* vdecls */
+ l = judgment->vdecls;
+ while (l) {
+ var = l->data;
+ if (!(l == judgment->vdecls && !is_prev_displayed))
+ draw_delimiter(w, y, x, virtual, ", ");
+ if (*offset == caret_offset)
+ draw_slot(w, y, x, offset, caret_offset, virtual, inputstr, FALSE);
+ else
+ draw_slot(w, y, x, offset, caret_offset, virtual,
+ var ? var->str : NULL, FALSE);
+ draw_delimiter(w, y, x, virtual, " : ");
+ draw_ref(w, y, x, offset, caret_offset, virtual,
+ inputstr, var ? var->type : NULL, FALSE);
+ is_prev_displayed = TRUE;
+ l = l->next;
+ }
+
+ /* ctx_dots */
+ if (workspace_mode && (*offset >= caret_offset)) {
+ if (is_prev_displayed)
+ draw_delimiter(w, y, x, virtual, ", ");
+ draw_slot(w, y, x, offset, caret_offset, virtual, "...", FALSE);
+ is_prev_displayed = TRUE;
+ }
+ else
+ *offset += 1;
+
+ /* Δ */
+ if (workspace_mode || judgment->generic_r) {
+ if (is_prev_displayed && (judgment->generic_r || *offset >= caret_offset))
+ draw_delimiter(w, y, x, virtual, ", ");
+ draw_ref(w, y, x, offset, caret_offset,
+ virtual, inputstr, judgment->generic_r, TRUE);
+ }
+
+ draw_delimiter(w, y, x, virtual, " ⊢ ");
+
+ /* thesis */
+ switch (judgment->kind) {
+ case thesis_kind_generic:
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->a, FALSE);
+ break;
+ case thesis_kind_type:
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->a, FALSE);
+ draw_delimiter(w, y, x, virtual, " type");
+ break;
+ case thesis_kind_element:
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->a, FALSE);
+ draw_delimiter(w, y, x, virtual, " : ");
+ /* TODO: use autofill_type */
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->a ? judgment->a->origin->type : NULL, FALSE);
+ break;
+ case thesis_kind_type_equal:
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->a, FALSE);
+ draw_delimiter(w, y, x, virtual, " ≐ ");
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->b, FALSE);
+ draw_delimiter(w, y, x, virtual, " type");
+ break;
+ case thesis_kind_element_equal:
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->a, FALSE);
+ draw_delimiter(w, y, x, virtual, " ≐ ");
+ draw_ref(w, y, x, offset, caret_offset, virtual, inputstr,
+ judgment->b, FALSE);
+ draw_delimiter(w, y, x, virtual, " : ");
+ draw_ref(w, y, x, offset, caret_offset, virtual,
+ inputstr, judgment->a ? judgment->a->origin->type : NULL, FALSE);
+ break;
+ case thesis_kind_unknown:
+ draw_slot(w, y, x, offset, caret_offset, virtual, NULL, FALSE);
+ break;
+ default:
+ }
+}
+
+void
+draw_rule(WINDOW *w, int *y, int *x, int caret_offset,
+ bool virtual, char *inputstr, struct rule *rule, bool workspace_mode)
+{
+ bool stack_p, is_dot;
+ int c, m, n, r, lw, s, ow, row, col;
+ int offset;
+ int point, pair, spaces;
+ GSList *l;
+
+ c = 0;
+ m = 0;
+ n = 0;
+ r = 0;
+ s = 0;
+ lw = 0;
+ ow = 0;
+ row = *y;
+ col = *x;
+ point = 0;
+ is_dot = FALSE;
+ offset = 0;
+
+ l = rule->hypotheses;
+ while (l) {
+ *y = 0; *x = 0;
+ draw_judgment(w, y, x, &offset, caret_offset, TRUE, inputstr, l->data,
+ workspace_mode);
+ s += *x;
+ m = m > *x ? m : *x;
+ n += 1;
+ l = l->next;
+ }
+ if (workspace_mode && (offset >= caret_offset))
+ is_dot = TRUE;
+ draw_judgment(w, y, &c, &offset, caret_offset, TRUE, inputstr,
+ rule->conclusion, workspace_mode);
+ draw_slot(w, y, &r, &offset, caret_offset, TRUE,
+ offset == caret_offset ? inputstr : rule->name, FALSE);
+
+ /* If the width of the line (calculated as the hypotheses + "..." + spacing
+ between them + space + rule name) is greater than the allowed number of
+ columns, then we must stack the hypotheses. */
+ ow = s + (is_dot ? 3 : 0) +
+ HYPOTHESES_SPACING * (n + is_dot ? n + is_dot + 1 : 0);
+
+ stack_p = (n > 1) && (ow + 1 + r >= NB_COLUMNS);
+ ow = stack_p ? m : ow;
+ lw = c > ow ? c : ow;
+ if (!virtual) {
+ offset = 0;
+ *y = row;
+ *x = col;
+ if (n == 0)
+ spaces = (lw - (is_dot ? 3 : 0)) / 2;
+ else
+ spaces = (lw - s - (is_dot ? 3 : 0)) / (n + (is_dot ? 2 : 1));
+ 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);
+ if (!stack_p)
+ *x += spaces;
+ else {
+ *y += 1;
+ *x = col;
+ }
+ l = l->next;
+ }
+ if (workspace_mode && (offset >= caret_offset))
+ draw_slot(w, y, x, &offset, caret_offset, virtual,
+ "...", FALSE);
+ else
+ offset += 1;
+ *y += 1; *x = col;
+ wmove(w, *y, *x);
+ for (*x = col ; *x < col + lw ; *x = *x + 1)
+ wprintw(w, "=");
+ *y += 1; *x = col + (lw - c) / 2;
+ draw_judgment(w, y, x, &offset, caret_offset, virtual, inputstr,
+ rule->conclusion, workspace_mode);
+ *y -= 1; *x = col + lw + 1;
+ 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;
+}
* License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
*/
-#define NCURSES_WIDECHAR 1
-#include <ncurses.h>
-#include <locale.h>
+#include "name.h"
+#include "ui.h"
+
#include <glib.h>
-#include <signal.h>
+#include <locale.h>
-#define PAIR_NORMAL 1
-#define PAIR_INVERSE 2
-#define PAIR_HL 3
-#define PAIR_SUCCESS 4
-#define PAIR_ERROR 5
+#define NCURSES_WIDECHAR 1
+#include <ncurses.h>
#define KEY_ESC 27
#define KEY_RETURN '\n'
#define KEY_TAB '\t'
-#define NB_COLUMNS 80
-#define HYPOTHESES_SPACING 4
-#define EMPTY_SLOT "█"
-
-/* The editor is always in either one of these modes. */
-enum ui_major_mode
- {
- ui_major_mode_splash,
- ui_major_mode_workspace,
- ui_major_mode_help,
- };
-
-/* The editor's input mode. */
-enum ui_input_mode
- {
- ui_input_mode_command,
- ui_input_mode_special_characters,
- ui_input_mode_default,
- };
-
-/* The type of slots in a rule. */
-enum slot_type
- {
- slot_type_rule_dots,
- slot_type_ctx_l,
- slot_type_ctx_v,
- slot_type_ctx_t,
- slot_type_ctx_dots,
- slot_type_ctx_r,
- slot_type_thesis,
- slot_type_generic_thesis,
- slot_type_type_thesis,
- slot_type_element_thesis_element,
- slot_type_element_thesis_type,
- slot_type_type_equal_thesis_type_1,
- slot_type_type_equal_thesis_type_2,
- slot_type_element_equal_thesis_element_1,
- slot_type_element_equal_thesis_element_2,
- slot_type_element_equal_thesis_type,
- slot_type_rule_name,
- };
-
-/* The position of the caret relative to the drawing point. */
-enum caret_to_point
- {
- caret_before_point = -1,
- caret_on_point = 0,
- caret_after_point = +1,
- };
-
-/* Kinds of judgment thesis. */
-enum thesis_kind
- {
- thesis_kind_generic,
- thesis_kind_type,
- thesis_kind_element,
- thesis_kind_type_equal,
- thesis_kind_element_equal,
- thesis_kind_unknown,
- };
-
enum vet_kind
{
vetk_variable,
vetk_type,
};
-/* A name's scope. */
-enum scope
- {
- scope_contextual,
- scope_local,
- scope_global,
- };
-
-enum name_kind
- {
- nk_generic_context_left,
- nk_generic_context_right,
- nk_generic_thesis,
- nk_vet, /* variable/element/type */
- };
-
-/* A name string can be an original name or reference an existing one. */
-struct wrap
-{
- bool is_origin;
- void *ptr; /* name or reference */
-};
-
-/*
- * A dependent type theory name has a scope, a kind, a rule where it was first
- * declared, a string used to refer to it, and a list of other names it depends
- * on. VETs also have a type with NULL standing for the terminal type.
- */
-struct name
-{
- enum scope scope;
- enum name_kind kind;
- struct wrap *type;
- struct rule *src;
- GSList *dependencies; /* names */
- char *str;
-};
-
-/*
- * Reference an existing (original) name. When doing so, if some of the
- * original name's denpendencies went out of scope they need to be replaced by
- * compatible references to names that are in scope.
- */
-struct reference
-{
- struct name *origin;
- GSList *replacements; /* references */
-};
-
-/*
- * A judgment has a thesis kind, optional generic left and right contexts,
- * optional variable declarations, and one or two wrappers for the thesis based
- * on its kind. For theses involving elements and their type, the type is
- * available through `a' or `b'.
- */
-struct judgment
-{
- enum thesis_kind kind;
- struct wrap *generic_l;
- struct wrap *generic_r;
- struct wrap *a;
- struct wrap *b;
- GSList *vdecls; /* names */
-};
-
-struct rule
-{
- char *name;
- GSList *hypotheses; /* judgments */
- struct judgment *conclusion;
-};
-
struct state
{
bool running;
enum ui_major_mode major_mode;
- enum ui_input_mode minor_mode;
+ enum ui_input_mode input_mode;
struct rule *rule;
- struct judgment *judgment;
- struct name *dependency;
+ struct point *slot;
WINDOW *workspace_w;
WINDOW *support_w;
WINDOW *echo_w;
GHashTable *gctxs; /* str -> name */
GHashTable *gtheses; /* str -> name */
GSList *support; /* rules */
- int caret;
- enum slot_type st;
GString *input;
- GString *backslash_input;
- GString *esc_input;
+ GString *special;
+ GString *command;
int status;
int err;
- bool replacing;
- GSList *stack; /* reference stack */
};
/*
*/
GHashTable *special_character_map;
+struct name * small;
+
gpointer
copy_user_data(gconstpointer src, gpointer data)
{
return data;
}
-/* Return whether or not the judgment is the conclusion of the rule. */
-bool
-conclusion_p(struct rule *rule, struct judgment *judgment)
+void
+insert_name(GHashTable *temporaries, struct name *name)
{
- return judgment == rule->conclusion ? TRUE : FALSE;
+ if (name->scope != scope_global)
+ g_hash_table_insert(temporaries, name->str, name);
}
/*
g_hash_table_steal_all(state->temporaries);
}
-/*
- * List all names involved (origin or replacement) in the reference,
- * recursively.
- */
-GSList *
-list_reference_type_names(GSList *list, struct reference *ref)
-{
- GSList *l;
-
- list = g_slist_prepend(list, ref->origin);
- l = ref->replacements;
- while (l) {
- list = list_reference_type_names(list, l->data);
- l = l->next;
- }
- return list;
-}
-
-/*
- * List all names involved (origin or through a reference — see
- * `list_reference_type_name') in the wrap, recursively.
- */
-GSList *
-list_wrap_names(GSList *list, struct wrap *wrap)
-{
- if (!wrap)
- return NULL;
- if (wrap->is_origin)
- list = g_slist_prepend(list, wrap->ptr);
- else
- list = list_reference_type_names(list, wrap->ptr);
- return list;
-}
-
-struct wrap *
-create_wrap(bool is_origin, void *ptr)
-{
- struct wrap *w;
-
- w = malloc(sizeof(struct wrap));
- w->is_origin = is_origin;
- w->ptr = ptr;
- return w;
-}
-
-struct name *
-create_name(enum scope scope, enum name_kind kind, struct wrap *type,
- struct rule *src, GSList *dependencies, char *str)
-{
- struct name *name;
-
- name = malloc(sizeof(struct name));
- name->scope = scope;
- name->kind = kind;
- name->type = type;
- name->src = src;
- name->dependencies = dependencies;
- name->str = str;
- 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()
-{
- struct judgment *j;
-
- j = malloc(sizeof(struct judgment));
- j->kind = thesis_kind_unknown;
- j->generic_l = NULL;
- j->generic_r = NULL;
- j->a = NULL;
- j->b = NULL;
- j->vdecls = NULL;
- return j;
-}
-
-struct rule *
-create_rule()
-{
- struct rule *rule;
-
- rule = malloc(sizeof(struct rule));
- rule->name = NULL;
- rule->hypotheses = NULL;
- rule->conclusion = create_judgment();
- return rule;
-}
-
-void free_wrap(struct wrap *);
-void free_reference(struct reference *);
-
-void
-free_name(struct name *name)
-{
- if (name) {
- free_wrap(name->type);
- g_slist_free(name->dependencies);
- free(name->str);
- free(name);
- }
-}
-
-void
-free_reference(struct reference *ref)
-{
- if (ref) {
- g_slist_free_full(ref->replacements, (GDestroyNotify)free_reference);
- free(ref);
- }
-}
-
-void
-free_wrap(struct wrap *wrap)
-{
- if (wrap) {
- if (wrap->is_origin)
- free_name(wrap->ptr);
- else
- free_reference(wrap->ptr);
- free(wrap);
- }
-}
-
-void
-free_judgment(struct judgment *judgment)
-{
- if (judgment) {
- free_wrap(judgment->generic_l);
- free_wrap(judgment->generic_r);
- free_wrap(judgment->a);
- free_wrap(judgment->b);
- g_slist_free_full(judgment->vdecls, (GDestroyNotify)free_name);
- free(judgment);
- }
-}
-
-void
-free_rule(struct rule *rule)
-{
- if (rule) {
- free(rule->name);
- g_slist_free_full(rule->hypotheses, (GDestroyNotify)free_judgment);
- free_judgment(rule->conclusion);
- free(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 name *
-get_wrap_name(struct wrap *wrap)
-{
- if (wrap->is_origin)
- return wrap->ptr;
- return ((struct reference *)wrap->ptr)->origin;
-}
-
-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));
-}
-
-/* The dependencies of a name are established at the point where it first occurs
- and consists in all names in scope at that point that aren't types of other
- names. The dependencies that need to be replaced at any point after that are
- those that are out of scope at that point (the replacements for their types
- can be deduced from these). In practice, because global names never go out
- of scope once created, we only have to care about dependencies and
- replacements of temporary names (those with contextual or local scope). As
- with any good rule there are exceptions: a name cannot be a dependency of its
- type (e.g. given `a:A', `A' doesn't depend on `a'), and a type, or any
- replacements therein, cannot be a dependency of one of its elements (e.g. if
- we have the hypothesis `A type' and the conclusion `a:A' or say `a:→[_, →[A,
- _]]' then `a' can't depend on `A'). */
-/*
- * 1. variables don't have dependencies (don't list_dependencies to create them)
- * 2. an element's type might be in `temporaries' if it is local, to know it is
- * declared, but shouldn't be added to the dependency list (we take care of
- * this here)
- * 3. names appearing in an element's type (`type_names') shouldn't be in the
- * elements dependency list (we take care of this here)
- * 4. a type's elements shouldn't be in the type's dependencies (create the
- * type's dependencies first then the element's dependencies)
- */
-GSList *
-list_dependencies(struct name *ptr, GHashTable *temporaries)
-{
- GSList *deps, *types, *l, *prev, *type_names;
- GHashTableIter iter;
- gpointer key, value;
- struct name *name;
-
- deps = NULL;
- type_names = !ptr ? NULL : list_wrap_names(NULL, ptr->type);
- g_hash_table_iter_init(&iter, temporaries);
- while (g_hash_table_iter_next(&iter, &key, &value)) {
- name = value;
-
- /* remember types as to remove those that make it to the dependency list. */
- if (name->type && name->type->is_origin)
- types = g_slist_prepend(types, name->type->ptr);
-
- /* The dependency list of a name shouldn't contain itself and, if it's for
- an element, shouldn't contain anything referenced by its type. */
- if (name != ptr && !g_slist_find(type_names, name))
- deps = g_slist_prepend(deps, name);
- }
- g_slist_free(g_steal_pointer(&type_names));
-
- /* Remove names that are types of other names in the dependency list. */
- prev = NULL;
- l = deps;
- while (l) {
- if (!g_slist_find(types, l->data)) {
- prev = l;
- l = l->next;
- }
- else {
- if (prev) {
- prev->next = l->next;
- g_slist_free_1(l);
- l = prev->next;
- }
- else {
- deps = l->next;
- g_slist_free_1(l);
- l = deps;
- }
- }
- }
-
- return deps;
-}
-
-void
-insert_name(GHashTable *temporaries, struct name *name)
-{
- if (name->scope != scope_global)
- g_hash_table_insert(temporaries, name->str, name);
-}
-
-void
-next_slot(struct state *state)
-{
- GSList *l;
- struct name *name, *ptr;
- struct wrap *wrap;
-
- switch (state->st) {
- case slot_type_rule_dots:
- state->st = slot_type_ctx_l;
- state->caret += 1;
- break;
- case slot_type_ctx_l:
- state->st = slot_type_ctx_dots;
- state->caret += 1;
- break;
- case slot_type_ctx_v:
- state->st = slot_type_ctx_t;
- state->caret += 1;
- break;
- case slot_type_ctx_t:
- state->st = slot_type_ctx_dots;
- state->caret += 1;
- name = (struct name *)g_slist_last(state->judgment->vdecls)->data;
- insert_name(state->temporaries, name);
- if (name->type->is_origin)
- insert_name(state->temporaries, name->type->ptr);
- break;
- case slot_type_ctx_dots:
- state->st = slot_type_ctx_r;
- state->caret += 1;
- break;
- case slot_type_ctx_r:
- state->st = slot_type_thesis;
- state->caret += 1;
- break;
- case slot_type_thesis:
- switch (state->judgment->kind)
- {
- case thesis_kind_generic:
- state->st = slot_type_generic_thesis;
- break;
- case thesis_kind_type:
- state->st = slot_type_type_thesis;
- break;
- case thesis_kind_element:
- state->st = slot_type_element_thesis_element;
- break;
- case thesis_kind_type_equal:
- state->st = slot_type_type_equal_thesis_type_1;
- break;
- case thesis_kind_element_equal:
- state->st = slot_type_element_equal_thesis_element_1;
- break;
- default:
- break;
- }
- break;
- case slot_type_generic_thesis:
- if (conclusion_p(state->rule, state->judgment))
- state->st = slot_type_rule_name;
- else
- state->st = slot_type_rule_dots;
- state->caret += 1;
- clear_contextuals(state->temporaries);
- break;
- case slot_type_type_thesis:
- if (conclusion_p(state->rule, state->judgment))
- state->st = slot_type_rule_name;
- else
- state->st = slot_type_rule_dots;
- state->caret += 1;
- if (state->judgment->a->is_origin)
- insert_name(state->temporaries, state->judgment->a->ptr);
- clear_contextuals(state->temporaries);
- break;
- case slot_type_element_thesis_element:
- if (state->judgment->a->is_origin) {
- state->st = slot_type_element_thesis_type;
- state->caret += 1;
- }
- else {
- if (conclusion_p(state->rule, state->judgment))
- state->st = slot_type_rule_name;
- else
- state->st = slot_type_rule_dots;
- state->caret += 2;
- }
- break;
- case slot_type_element_thesis_type:
- if (conclusion_p(state->rule, state->judgment))
- state->st = slot_type_rule_name;
- else
- state->st = slot_type_rule_dots;
- state->caret += 1;
- name = get_wrap_name(state->judgment->a);
- if (state->judgment->a->is_origin) {
- name->dependencies = list_dependencies(name, state->temporaries);
- insert_name(state->temporaries, name);
- }
- if (name->type->is_origin)
- insert_name(state->temporaries, name->type->ptr);
- clear_contextuals(state->temporaries);
- break;
- case slot_type_type_equal_thesis_type_1:
- state->st = slot_type_type_equal_thesis_type_2;
- state->caret += 1;
- if (state->judgment->a->is_origin)
- insert_name(state->temporaries, state->judgment->a->ptr);
- break;
- case slot_type_type_equal_thesis_type_2:
- if (conclusion_p(state->rule, state->judgment))
- state->st = slot_type_rule_name;
- else
- state->st = slot_type_rule_dots;
- state->caret += 1;
- if (state->judgment->b->is_origin)
- insert_name(state->temporaries, state->judgment->b->ptr);
- clear_contextuals(state->temporaries);
- break;
- case slot_type_element_equal_thesis_element_1:
- state->st = slot_type_element_equal_thesis_element_2;
- state->caret += 1;
- break;
- case slot_type_element_equal_thesis_element_2:
- if (state->judgment->a->is_origin && state->judgment->b->is_origin) {
- state->st = slot_type_element_equal_thesis_type;
- state->caret += 1;
- }
- else {
- if (conclusion_p(state->rule, state->judgment))
- state->st = slot_type_rule_name;
- else
- state->st = slot_type_rule_dots;
- state->caret += 2;
-
- /* Since we skip the type slot we should add dependencies to originals,
- here. */
- ptr = NULL;
- if (state->judgment->a->is_origin) {
- name = state->judgment->a->ptr;
- name->type = copy_wrap(get_wrap_type(state->judgment->b));
- name->dependencies = list_dependencies(name, state->temporaries);
- ptr = name; /* Don't insert `a' before we listed `b's deps */
- }
- if (state->judgment->b->is_origin) {
- name = state->judgment->b->ptr;
- name->type = copy_wrap(get_wrap_type(state->judgment->a));
- name->dependencies = list_dependencies(name, state->temporaries);
- insert_name(state->temporaries, name);
- }
- if (ptr) insert_name(state->temporaries, ptr);
- }
- break;
- case slot_type_element_equal_thesis_type:
- if (conclusion_p(state->rule, state->judgment))
- state->st = slot_type_rule_name;
- else
- state->st = slot_type_rule_dots;
- state->caret += 1;
-
- ptr = NULL;
- if (state->judgment->a->is_origin) {
- name = state->judgment->a->ptr;
- name->type = copy_wrap(get_wrap_type(state->judgment->b));
- name->dependencies = list_dependencies(name, state->temporaries);
- ptr = name; /* Don't insert `a' before we listed `b's deps */
- }
- if (state->judgment->b->is_origin) {
- name = state->judgment->b->ptr;
- name->type = copy_wrap(get_wrap_type(state->judgment->a));
- name->dependencies = list_dependencies(name, state->temporaries);
- insert_name(state->temporaries, name);
- }
- if (ptr) insert_name(state->temporaries, ptr);
- wrap = get_wrap_type(state->judgment->a);
- if (wrap->is_origin)
- insert_name(state->temporaries, wrap->ptr);
- clear_contextuals(state->temporaries);
- break;
- case slot_type_rule_name:
- state->st = slot_type_rule_dots;
- state->caret = 0;
- break;
- default:
- }
-}
-
-enum slot_type
-prev_thesis_kind_switch(enum thesis_kind tk)
-{
- switch (tk)
- {
- case thesis_kind_generic:
- return slot_type_generic_thesis;
- break;
- case thesis_kind_type:
- return slot_type_type_thesis;
- break;
- case thesis_kind_element:
- return slot_type_element_thesis_type;
- break;
- case thesis_kind_type_equal:
- return slot_type_type_equal_thesis_type_2;
- break;
- case thesis_kind_element_equal:
- return slot_type_element_equal_thesis_type;
- break;
- default:
- return -1;
- break;
- }
-}
-
-enum slot_type
-prev_slot(struct state *state)
-{
- switch (state->st) {
- case slot_type_rule_dots:
- if (state->rule->hypotheses)
- return prev_thesis_kind_switch(((struct judgment *)g_slist_last(state->rule->hypotheses)->data)->kind);
- break;
- case slot_type_ctx_l:
- return slot_type_rule_dots;
- break;
- case slot_type_ctx_v:
- return slot_type_ctx_dots;
- break;
- case slot_type_ctx_t:
- return slot_type_ctx_v;
- break;
- case slot_type_ctx_dots:
- if (state->judgment->vdecls)
- return slot_type_ctx_t;
- else
- return slot_type_ctx_l;
- break;
- case slot_type_ctx_r:
- return slot_type_ctx_dots;
- break;
- case slot_type_thesis:
- return slot_type_ctx_r;
- break;
- case slot_type_generic_thesis:
- return slot_type_thesis;
- break;
- case slot_type_type_thesis:
- return slot_type_thesis;
- break;
- case slot_type_element_thesis_element:
- return slot_type_thesis;
- break;
- case slot_type_element_thesis_type:
- return slot_type_element_thesis_element;
- break;
- case slot_type_type_equal_thesis_type_1:
- return slot_type_thesis;
- break;
- case slot_type_type_equal_thesis_type_2:
- return slot_type_type_equal_thesis_type_1;
- break;
- case slot_type_element_equal_thesis_element_1:
- return slot_type_thesis;
- break;
- case slot_type_element_equal_thesis_element_2:
- return slot_type_element_equal_thesis_element_1;
- break;
- case slot_type_element_equal_thesis_type:
- return slot_type_element_equal_thesis_element_2;
- break;
- case slot_type_rule_name:
- return prev_thesis_kind_switch(state->judgment->kind);
- break;
- default:
- return -1;
- }
-}
-
void
-draw_slot(WINDOW *w, int *y, int *x, bool virtual, bool optional, int pair, const char *str)
+echo_esc(WINDOW *w, const char *str)
{
- if (!virtual) {
- wattron(w, COLOR_PAIR(pair));
- wmove(w, *y, *x);
- if (str && *str != '\0')
- wprintw(w, str);
- else {
- wprintw(w, EMPTY_SLOT);
- if (optional)
- wprintw(w, "?");
- }
- wattroff(w, COLOR_PAIR(pair));
- }
- if (str && *str != '\0')
- *x += mbstowcs(NULL, str, 0);
- else {
- if (optional)
- *x += 2;
- else
- *x += 1;
- }
+ mvwprintw(w, 0, 0, "ESC");
+ mvwprintw(w, 0, 4, str);
}
void
-set_ctp_and_pair(enum caret_to_point *ctp, int *pair, int caret, int point)
-{
- *ctp = caret < point ? caret_before_point : (caret > point ? caret_after_point : caret_on_point);
- *pair = *ctp == caret_on_point ? 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 (!ref) {
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == caret_on_point)
- draw_slot(w, y, x, virtual, FALSE, pair, inputstr);
- else if (ctp == caret_before_point)
- draw_slot(w, y, x, virtual, FALSE, pair, NULL);
- }
- else {
- 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) {
- /* dep = TBD; */
- /* l1 = list_out_of_scope_dependencies(name, temporaries); */
- /* while (l1) { */
- /* set_ctp_and_pair(&ctp, &pair, caret, (*point)++); */
- /* draw_slot(w, y, x, virtual, FALSE, pair, NULL); */
- /* if (l1->next) */
- /* draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, ", "); */
- /* else */
- /* draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, ". "); */
- /* l1 = l1->next; */
- /* } */
-
- 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, "]");
- }
- }
-}
-
-bool /* is displayed ? */
-draw_wrap(WINDOW *w, int *y, int *x, bool virtual, bool optional,
- int caret, int *point, char *inputstr, struct wrap *wrap)
-{
- int pair;
- enum caret_to_point ctp;
- GSList *l;
-
- if (!wrap) {
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == caret_on_point)
- draw_slot(w, y, x, virtual, FALSE, pair, inputstr);
- else if (ctp == caret_before_point)
- draw_slot(w, y, x, virtual, optional, pair, NULL);
- else
- return FALSE;
- }
- 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, is_prev_displayed;
- int pair;
- GSList *l;
- struct name *var;
- enum caret_to_point ctp;
-
- v = virtual;
-
- /* Γ */
- 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);
- }
-
- /* vdecls */
- l = judgment->vdecls;
- while (l) {
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- var = l->data;
- if (!(l == judgment->vdecls && !is_prev_displayed))
- draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", ");
- if (ctp == caret_on_point)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- 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 == caret_before_point || ctp == caret_on_point)) {
- if (is_prev_displayed)
- draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", ");
- draw_slot(w, y, x, v, FALSE, pair, "...");
- is_prev_displayed = TRUE;
- }
-
- /* Δ */
- if (workspace_mode || judgment->generic_r) {
- set_ctp_and_pair(&ctp, &pair, caret, *point);
- if (is_prev_displayed && (judgment->generic_r || ctp <= caret_on_point))
- 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_NORMAL, " ⊢ ");
-
- /* thesis */
- switch (judgment->kind) {
- case thesis_kind_generic:
- draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a);
- break;
- case thesis_kind_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 thesis_kind_element:
- 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 thesis_kind_type_equal:
- 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 thesis_kind_element_equal:
- 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 thesis_kind_unknown:
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- draw_slot(w, y, x, v, FALSE, pair, NULL);
- break;
- default:
- }
-}
-
-void
-draw_rule(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode,
- int caret, char *inputstr, struct rule *rule)
-{
- bool stack_p, is_dot;
- int c, m, n, r, lw, s, ow, row, col;
- int point, pair, spaces;
- enum caret_to_point ctp;
- GSList *l;
-
- c = 0;
- m = 0;
- n = 0;
- r = 0;
- s = 0;
- lw = 0;
- ow = 0;
- row = *y;
- col = *x;
- point = 0;
- is_dot = FALSE;
-
- l = rule->hypotheses;
- while (l) {
- *y = 0; *x = 0;
- draw_judgment(w, y, x, TRUE, workspace_mode,
- caret, &point, inputstr, l->data);
- s += *x;
- m = m > *x ? m : *x;
- n += 1;
- l = l->next;
- }
- set_ctp_and_pair(&ctp, &pair, caret, point++);
- if (workspace_mode && (ctp <= caret_on_point))
- is_dot = TRUE;
- set_ctp_and_pair(&ctp, &pair, caret, point);
- draw_judgment(w, y, &c, TRUE, workspace_mode,
- caret, &point, inputstr, rule->conclusion);
- set_ctp_and_pair(&ctp, &pair, caret, point++);
- draw_slot(w, y, &r, TRUE, FALSE, pair, ctp == caret_on_point ? inputstr : rule->name);
-
- /* If the width of the line (calculated as the hypotheses + "..." + spacing
- between them + space + rule name) is greater than the allowed number of
- columns, then we must stack the hypotheses. */
- ow = s + (is_dot ? 3 : 0) +
- HYPOTHESES_SPACING * (n + is_dot ? n + is_dot + 1 : 0);
-
- stack_p = (n > 1) && (ow + 1 + r >= NB_COLUMNS);
- ow = stack_p ? m : ow;
- lw = c > ow ? c : ow;
- if (!virtual) {
- *y = row;
- *x = col;
- if (n == 0)
- spaces = (lw - (is_dot ? 3 : 0)) / 2;
- else
- spaces = (lw - s - (is_dot ? 3 : 0)) / (n + (is_dot ? 2 : 1));
- if (!stack_p)
- *x += spaces;
- point = 0;
- l = rule->hypotheses;
- while (l) {
- draw_judgment(w, y, x, virtual, workspace_mode,
- caret, &point, inputstr, l->data);
- if (!stack_p)
- *x += spaces;
- else {
- *y += 1;
- *x = col;
- }
- l = l->next;
- }
- set_ctp_and_pair(&ctp, &pair, caret, point++);
- if (workspace_mode && (ctp <= caret_on_point))
- draw_slot(w, y, x, virtual, FALSE, pair, "...");
- *y += 1; *x = col;
- wmove(w, *y, *x);
- for (*x = col ; *x < col + lw ; *x = *x + 1)
- wprintw(w, "=");
- *y += 1; *x = col + (lw - c) / 2;
- set_ctp_and_pair(&ctp, &pair, caret, point);
- draw_judgment(w, y, x, virtual, workspace_mode,
- caret, &point, inputstr, rule->conclusion);
- *y -= 1; *x = col + lw + 1;
- set_ctp_and_pair(&ctp, &pair, caret, point++);
- draw_slot(w, y, x, virtual, FALSE, pair, ctp == caret_on_point ? inputstr : rule->name);
- }
- *y = row + (stack_p ? n + (is_dot ? 1 : 0) + 2 : 3); *x = col + (lw + c) / 2;
-}
-
-void
-render_splash()
+render_splash(struct state *state)
{
int i, n;
static const char *strs[] = {
(COLS - strlen(strs[6])) / 2,
strs[i]);
}
+ if (state->input_mode == ui_input_mode_command)
+ echo_esc(state->echo_w, state->command->str);
refresh();
}
void
-render_help()
+render_help(struct state *state)
{
int c;
FILE *fd;
while ((c = fgetc(fd)) != EOF)
addch(c);
fclose(fd);
+ if (state->input_mode == ui_input_mode_command)
+ echo_esc(state->echo_w, state->command->str);
refresh();
}
str = "error: name already defined";
break;
case 6:
- str = "error: inconsistant kinds"; /* TODO: list the two kinds conflicting */
+ str = "error: inconsistant kinds";
break;
case 7:
str = "error: incompatible replacement";
wattroff(w, COLOR_PAIR(pair));
}
-void
-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;
+ int y, x, q, i, caret_offset;
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;
GSList *l;
- GList *l1;
gpointer key, value;
struct rule *rule;
+ struct point *p;
q = (LINES - 3) / 2;
clear();
/* draw debug info */
i = 0;
- l1 = g_hash_table_get_keys(state->temporaries);
+ 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;
}
- 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);
+ 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;
- draw_rule(state->workspace_w, &y, &x, FALSE, TRUE,
- state->caret, state->input->str, state->rule);
+ 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,
+ FALSE, state->input->str, state->rule, TRUE);
/* draw existing rules */
i = 0;
while (g_hash_table_iter_next(&iter, &key, &value))
{
rule = value;
- y = i; x = COLS / 2;
- draw_rule(state->support_w, &y, &x, FALSE, FALSE, -1, NULL, rule);
- i = y + 2;
+ y = i; x = 0;
+ draw_rule(state->support_w, &y, &x, -1,
+ FALSE, NULL, rule, FALSE);
+ i = y + 1;
}
- /* 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 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, "█");
+
+ /* draw echo area */
+ if (state->input_mode == ui_input_mode_command)
+ echo_esc(state->echo_w, state->command->str);
+ else if (state->err) {
+ echo_status(state->echo_w, state->err);
+ state->err = 0;
+ }
+ else {
+ if (state->slot->st == slot_type_thesis) {
+ if (state->status == 0)
+ mvwprintw(state->echo_w, 0, 0, str1);
+ else
+ mvwprintw(state->echo_w, 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);
}
+ }
+
+ refresh();
+}
- /* draw echo area */
- if (state->err) {
- echo_status(state->echo_w, state->err);
- state->err = 0;
+bool
+handle_esc(struct state *state, wint_t key)
+{
+ if (key == KEY_ESC) {
+ if (state->input_mode == ui_input_mode_command)
+ state->input_mode = ui_input_mode_default;
+ else {
+ state->command = g_string_erase(state->command, 0, -1);
+ state->input_mode = ui_input_mode_command;
+ }
}
else {
- switch (state->major_mode) {
- case ui_major_mode_workspace:
- if (state->st == slot_type_thesis) {
- if (state->status == 0)
- mvwprintw(state->echo_w, 0, 0, str1);
- else
- mvwprintw(state->echo_w, 0, 0, str2);
+ if (state->input_mode == ui_input_mode_command) {
+ if (key == KEY_RETURN) {
+ if (strcmp(state->command->str, "q") == 0) {
+ state->running = FALSE;
+ state->command = g_string_erase(state->command, 0, -1);
+ state->input_mode = ui_input_mode_default;
+ }
+ else if (strcmp(state->command->str, "splash") == 0) {
+ state->major_mode = ui_major_mode_splash;
+ state->command = g_string_erase(state->command, 0, -1);
+ state->input_mode = ui_input_mode_default;
+ }
+ else if (strcmp(state->command->str, "h") == 0) {
+ state->major_mode = ui_major_mode_help;
+ state->command = g_string_erase(state->command, 0, -1);
+ state->input_mode = ui_input_mode_default;
+ }
+ else {
+ }
}
- else if (state->minor_mode == ui_input_mode_special_characters) {
- mvwprintw(state->echo_w, 0, 0, "\\");
- wprintw(state->echo_w, state->backslash_input->str);
+ else if ((key > 64 && key < 91) || (key > 96 && key < 123)) {
+ state->command = g_string_append_c(state->command, key);
}
- break;
- default:
}
+ else
+ return FALSE;
}
+ return TRUE;
+}
- /* draw window names */
- attron(COLOR_PAIR(PAIR_INVERSE));
- move(q, 0);
- printw("workspace%*s", COLS - 9, "");
- move(LINES - 2, 0);
- printw("support%*s", COLS - 7, "");
- attroff(COLOR_PAIR(PAIR_INVERSE));
+void
+handle_help_input(struct state *state, wint_t key)
+{
+ if (!handle_esc(state, key))
+ state->major_mode = ui_major_mode_workspace;
+}
- refresh();
+void
+handle_splash_input(struct state *state, wint_t key)
+{
+ if (!handle_esc(state, key))
+ state->major_mode = ui_major_mode_workspace;
}
void
-handle_input(struct state *state, char key)
+handle_input(struct state *state, wint_t key)
{
GSList *l;
struct name *name;
if (key == '\\') {
- state->minor_mode = ui_input_mode_special_characters;
+ state->input_mode = ui_input_mode_special_characters;
state->status = 0;
- state->backslash_input = g_string_erase(state->backslash_input, 0, -1);
+ state->special = g_string_erase(state->special, 0, -1);
}
else if (key > 32 && key < 127) {
- if (state->minor_mode == ui_input_mode_default)
+ if (state->input_mode == ui_input_mode_default)
state->input = g_string_append_c(state->input, key);
else {
if ((key > 64 && key < 91) || (key > 96 && key < 123))
{
- state->backslash_input = g_string_append_c(state->backslash_input, key);
- l = g_hash_table_lookup(special_character_map, state->backslash_input->str);
+ state->special = g_string_append_c(state->special, key);
+ l = g_hash_table_lookup(special_character_map, state->special->str);
if (!l) {
- state->minor_mode = ui_input_mode_default;
+ state->input_mode = ui_input_mode_default;
}
else if (!l->next) {
- state->minor_mode = ui_input_mode_default;
+ state->input_mode = ui_input_mode_default;
state->input = g_string_append(state->input, l->data);
}
}
else
- state->minor_mode = ui_input_mode_default;
+ state->input_mode = ui_input_mode_default;
}
}
if ((name = g_hash_table_lookup(state->globals, state->input->str))) {
/* state->st = prev_slot(state); */
}
-void
-handle_input_backspace(struct state *state)
-{
- if (*state->input->str == '\0')
- handle_slot_backspace(state);
- else
- state->input = g_string_erase(state->input, 0, -1);
-}
-
void
handle_backspace(struct state *state)
{
- if (state->minor_mode == ui_input_mode_default)
- handle_input_backspace(state);
+ if (state->input_mode == ui_input_mode_default) {
+ if (*state->input->str == '\0')
+ handle_slot_backspace(state);
+ else
+ state->input = g_string_erase(state->input, 0, -1);
+ }
else
{
- if (*state->backslash_input->str == '\0')
- state->minor_mode = ui_input_mode_default;
+ if (*state->special->str == '\0')
+ state->input_mode = ui_input_mode_default;
else
- state->backslash_input = g_string_erase(state->backslash_input, 0, -1);
- }
-}
-
-void
-handle_esc(struct state *state, wint_t key)
-{
- if (key == KEY_ESC) {
- if (state->minor_mode = ui_input_mode_command)
- state->minor_mode = ui_input_mode_default;
- else {
- state->esc_input = g_string_erase(state->esc_input, 0, -1);
- state->minor_mode = ui_input_mode_command;
+ state->special = g_string_erase(state->special, 0, -1);
}
- }
- else if (state->minor_mode == ui_input_mode_command) {
- if (key == KEY_RETURN) {
- state->minor_mode = ui_input_mode_default;
- if (strcmp(state->esc_input->str, "q") == 0)
- state->running = FALSE;
- else if (strcmp(state->esc_input->str, "splash") == 0)
- state->major_mode = ui_major_mode_splash;
- else if (strcmp(state->esc_input->str, "h") == 0)
- state->major_mode = ui_major_mode_help;
- }
- else if ((key > 64 && key < 91) || (key > 96 && key < 123)) {
- state->esc_input = g_string_append_c(state->esc_input, key);
- }
- }
-}
-
-GSList *
-filter_out_of_scope(GSList *dependencies, GHashTable *temporaries)
-{
- GSList *l, *oos;
- struct name *dep, *name;
-
- oos = NULL;
- l = dependencies;
- while (l) {
- dep = l->data;
- name = g_hash_table_lookup(temporaries, dep->str);
- if (!name || name != dep)
- oos = g_slist_prepend(oos, dep);
- l = l->next;
- }
- return oos;
}
int
{
enum name_kind nk;
struct name *name;
- struct wrap *wrap;
+ struct reference *ref;
+ struct judgment *judgment;
GSList *deps;
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;
+ nk = is_left ?
+ name_kind_generic_context_left :
+ name_kind_generic_context_right;
+ judgment = get_slot_judgment(state->rule, state->slot);
if (name) {
if (nk != name->kind)
return 4;
- deps = filter_out_of_scope(name->dependencies, state->temporaries);
- wrap = create_wrap(FALSE,
- create_reference(name,
- g_slist_copy_deep(deps,
- copy_user_data,
- NULL)));
+ deps = list_out_of_scope_names(name->dependencies, state->temporaries);
+ ref = create_reference(name,
+ g_slist_copy_deep(deps,
+ copy_user_data,
+ NULL));
+ g_slist_free(g_steal_pointer(&deps));
if (is_left)
- state->judgment->generic_l = wrap;
+ judgment->generic_l = ref;
else
- state->judgment->generic_r = wrap;
+ judgment->generic_r = ref;
state->input = g_string_erase(state->input, 0, -1);
return 0;
}
- else if (conclusion_p(state->rule, state->judgment))
+ else if (state->slot->is_conclusion)
return 3;
name = create_name(scope_local,
nk,
state->rule,
list_dependencies(NULL, state->temporaries),
strdup(state->input->str));
- wrap = create_wrap(TRUE, name);
+ ref = create_reference(name, NULL);
if (is_left)
- state->judgment->generic_l = wrap;
+ judgment->generic_l = ref;
else
- state->judgment->generic_r = wrap;
+ judgment->generic_r = ref;
g_hash_table_insert(state->gctxs, name->str, name);
state->input = g_string_erase(state->input, 0, -1);
return 0;
{
enum name_kind nk;
struct name *name;
- struct wrap *wrap;
+ struct judgment *judgment;
GSList *deps;
if (*state->input->str == '\0')
return 1;
name = g_hash_table_lookup(state->gtheses, state->input->str);
+ judgment = get_slot_judgment(state->rule, state->slot);
if (name) {
- deps = filter_out_of_scope(name->dependencies, state->temporaries);
- wrap = create_wrap(FALSE,
- create_reference(name,
- g_slist_copy_deep(deps,
- copy_user_data,
- NULL)));
- state->judgment->a = wrap;
+ deps = list_out_of_scope_names(name->dependencies, state->temporaries);
+ judgment->a = create_reference(name,
+ g_slist_copy_deep(deps,
+ copy_user_data,
+ NULL));
+ g_slist_free(g_steal_pointer(&deps));
state->input = g_string_erase(state->input, 0, -1);
return 0;
}
- else if (conclusion_p(state->rule, state->judgment))
+ else if (state->slot->is_conclusion)
return 3;
name = create_name(scope_local,
- nk_generic_thesis,
+ name_kind_generic_thesis,
NULL,
state->rule,
list_dependencies(NULL, state->temporaries),
strdup(state->input->str));
- wrap = create_wrap(TRUE, name);
- state->judgment->a = wrap;
+ judgment->a = create_reference(name, NULL);;
g_hash_table_insert(state->gtheses, name->str, name);
state->input = g_string_erase(state->input, 0, -1);
return 0;
validate_vet_input(void *addr, struct state *state,
enum thesis_kind tk, enum vet_kind vetk)
{
- bool no_deps, c_p;
+ bool no_deps;
GSList *l, *deps;
enum scope scope;
struct name *name;
if (vetk == vetk_variable)
return 5;
state->input = g_string_erase(state->input, 0, -1);
- deps = filter_out_of_scope(name->dependencies, state->temporaries);
- l = g_slist_copy_deep(deps, copy_user_data, NULL);
- *(struct wrap **)addr = create_wrap(FALSE, create_reference(name, l));
+ deps = list_out_of_scope_names(name->dependencies, state->temporaries);
+ *(struct reference **)addr =
+ create_reference(name, g_slist_copy_deep(deps, copy_user_data, NULL));
+ g_slist_free(g_steal_pointer(&deps));
}
else {
- c_p = conclusion_p(state->rule, state->judgment);
- if (c_p &&
+ if (state->slot->is_conclusion &&
(tk == thesis_kind_type_equal || tk == thesis_kind_element_equal ||
(tk == thesis_kind_unknown && vetk == vetk_type) || /* variable type */
(tk == thesis_kind_element && vetk == vetk_type))) /* element type */
if (vetk == vetk_variable ||
(tk == thesis_kind_element && vetk == vetk_element) ||
(tk == thesis_kind_element_equal && vetk == vetk_element))
- no_deps = TRUE;
+ no_deps = TRUE; /* We will add the dependencies later */
else
no_deps = FALSE;
if (vetk == vetk_variable)
scope = scope_contextual;
- else if (c_p &&
- (tk == thesis_kind_type || (tk == thesis_kind_element && vetk == vetk_element)))
+ else if (state->slot->is_conclusion &&
+ (tk == thesis_kind_type ||
+ (tk == thesis_kind_element && vetk == vetk_element)))
scope = scope_global;
else
scope = scope_local;
- name = create_name(scope, nk_vet, NULL, state->rule,
+ name = create_name(scope, name_kind_vet,
+ vetk != vetk_type ? NULL : create_reference(small, NULL),
+ state->rule,
no_deps ? NULL :
list_dependencies(NULL, state->temporaries),
strdup(state->input->str));
if (vetk == vetk_variable)
*(struct name **)addr = name;
else
- *(struct wrap **)addr = create_wrap(TRUE, name);
+ *(struct reference **)addr = create_reference(name, NULL);
+
+ /* variables and elements will be added after creating their type */
+ if (vetk == vetk_type)
+ insert_name(state->temporaries, name);
}
return 0;
}
bool is_c;
guint idx;
GSList *reps, *l, *deps;
- struct name *dep, *name, *addr, *dtname;
+ struct name *dep, *rep, *addr, *dtname;
struct reference *ref;
if (*state->input->str == '\0')
return 1;
- name = g_hash_table_lookup(state->globals, state->input->str);
- if (!name)
- name = g_hash_table_lookup(state->temporaries, 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);
-
- /* check that the given `name' and the required `dep' are compatible */
- if ((!dep->type && name->type) || (dep->type && !name->type))
- return 7;
- if (dep->type && name->type) {
- /* check if the dep->type is in scope */
- dtname = get_wrap_name(dep->type);
- addr = g_hash_table_lookup(state->globals, dtname->str);
- if (!addr)
- addr = g_hash_table_lookup(state->temporaries, dtname->str);
- if (addr && addr == dtname) { /* it's in scope */
- /* when in scope the replacement's type must be the same */
- if (dtname != get_wrap_name(name->type))
- return 7;
- }
- else {
- /* anything goes */
- }
+ rep = g_hash_table_lookup(state->globals, state->input->str);
+ if (!rep)
+ rep = g_hash_table_lookup(state->temporaries, state->input->str);
+ if (!rep)
+ return 3;
+ ref = get_slot_data(state->rule, state->slot, state->slot->stack->next);
+ idx = GPOINTER_TO_INT(state->slot->stack->data);
+ dep = g_slist_nth_data(ref->origin->dependencies, idx);
+
+ /* check that the given `rep' and the required `dep' are compatible */
+ if ((!dep->type && rep->type) || (dep->type && !rep->type))
+ return 7;
+ if (dep->type && rep->type) {
+ /* check if the dep->type is in scope */
+ dtname = dep->type->origin;
+ addr = g_hash_table_lookup(state->globals, dtname->str);
+ if (!addr)
+ addr = g_hash_table_lookup(state->temporaries, dtname->str);
+ if (addr && addr == dtname) { /* it's in scope */
+ /* when in scope the replacement's type must be the same */
+ if (dtname != rep->type->origin)
+ return 7;
}
-
- /* set the state for the next slot */
- l = g_slist_nth(ref->replacements, idx);
- deps = filter_out_of_scope(name->dependencies, state->temporaries);
- reps = g_slist_copy_deep(deps, copy_user_data, NULL);
- l->data = create_reference(name, reps);
- if (reps)
- state->stack = g_slist_prepend(state->stack, l->data);
else {
- 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);
- }
+ /* anything goes */
}
- state->input = g_string_erase(state->input, 0, -1);
- return 0;
}
- return 3;
+
+ /* set the state for the next slot */
+ l = g_slist_nth(ref->replacements, idx);
+ deps = list_out_of_scope_names(rep->dependencies, state->temporaries);
+ reps = g_slist_copy_deep(deps, copy_user_data, NULL);
+ g_slist_free(g_steal_pointer(&deps));
+ l->data = create_reference(rep, reps);
+ state->input = g_string_erase(state->input, 0, -1);
+ return 0;
}
int
c = rule->conclusion;
switch (c->kind) {
case thesis_kind_type:
- if (c->a->is_origin) {
- name = c->a->ptr;
+ if (c->a->origin->scope == scope_global) {
+ name = c->a->origin;
g_hash_table_insert(state->globals, name->str, name);
}
break;
case thesis_kind_element:
- if (c->a->is_origin) {
- name = c->a->ptr;
+ if (c->a->origin->scope == scope_global) {
+ name = c->a->origin;
g_hash_table_insert(state->globals, name->str, name);
}
break;
}
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)
+handle_workspace_input(struct state *state, wint_t key)
{
- state->replacing = TRUE;
- state->stack = g_slist_prepend(state->stack, addr->ptr);
- state->caret += 1;
+ struct judgment *judgment;
+ struct name *name, *ptr;
+
+ if (!handle_esc(state, key)) {
+ if (key == KEY_RETURN) {
+ 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);
+ state->slot->st = slot_type_ctx_l;
+ state->slot->judgment_idx = g_slist_index(state->rule->hypotheses, judgment);
+ }
+ else if (state->slot->st == slot_type_ctx_dots) {
+ judgment = get_slot_judgment(state->rule, state->slot);
+ judgment->vdecls = g_slist_append(judgment->vdecls, NULL);
+ state->slot->st = slot_type_ctx_v;
+ state->slot->vdecl_idx = g_slist_length(judgment->vdecls) - 1;
+ }
+ }
+ else if (key == KEY_TAB) {
+ if (state->slot->stack) {
+ if (!(state->err = validate_replacement(state)))
+ next_empty_slot(state->slot, state->rule);
+ }
+ else {
+ switch (state->slot->st) {
+ case slot_type_rule_dots:
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case slot_type_ctx_l:
+ if (!(state->err = validate_generic_context(state, TRUE)))
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case slot_type_ctx_v:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err =
+ validate_vet_input(&g_slist_last(judgment->vdecls)->data,
+ state,
+ thesis_kind_unknown,
+ vetk_variable)))
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case slot_type_ctx_t:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ name = g_slist_last(judgment->vdecls)->data;
+ if (!(state->err =
+ validate_vet_input(&name->type,
+ state,
+ thesis_kind_unknown,
+ vetk_type))) {
+ insert_name(state->temporaries, name);
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_ctx_dots:
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case slot_type_ctx_r:
+ if (!(state->err = validate_generic_context(state, FALSE)))
+ next_empty_slot(state->slot, state->rule);
+ state->status = 0;
+ break;
+ case slot_type_thesis:
+ /* do nothing */
+ break;
+ case slot_type_generic_thesis:
+ if (!(state->err = validate_generic_thesis(state))) {
+ clear_contextuals(state->temporaries);
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_type_thesis:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->a, state,
+ thesis_kind_type,
+ vetk_type))) {
+ clear_contextuals(state->temporaries);
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_element_thesis_element:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->a, state,
+ thesis_kind_element,
+ vetk_element))) {
+ if (judgment->a->origin->type)
+ clear_contextuals(state->temporaries);
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_element_thesis_type:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->a->origin->type,
+ state,
+ thesis_kind_element,
+ vetk_type))) {
+ /* elements are created after their types */
+ name = judgment->a->origin;
+ name->dependencies = list_dependencies(name, state->temporaries);
+ insert_name(state->temporaries, name);
+ clear_contextuals(state->temporaries);
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_type_equal_thesis_type_1:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->a, state,
+ thesis_kind_type_equal,
+ vetk_type)))
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case slot_type_type_equal_thesis_type_2:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->b, state,
+ thesis_kind_type_equal,
+ vetk_type))) {
+
+ clear_contextuals(state->temporaries);
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_element_equal_thesis_element_1:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->a, state,
+ thesis_kind_element_equal,
+ vetk_element)))
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case slot_type_element_equal_thesis_element_2:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->b, state,
+ thesis_kind_element_equal,
+ vetk_element))) {
+ /* elements are created after their types */
+ /* we might already know the type of either one so we autofill */
+ if (judgment->a->origin->type) {
+ if (!judgment->b->origin->type) {
+ name = judgment->b->origin;
+ name->type = copy_reference(judgment->a->origin->type);
+ name->dependencies =
+ list_dependencies(name, state->temporaries);
+ insert_name(state->temporaries, name);
+ }
+ clear_contextuals(state->temporaries);
+ }
+ else if (judgment->a->origin->type) {
+ name = judgment->a->origin;
+ name->type = copy_reference(judgment->b->origin->type);
+ name->dependencies = list_dependencies(name, state->temporaries);
+ insert_name(state->temporaries, name);
+ clear_contextuals(state->temporaries);
+ }
+
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_element_equal_thesis_type:
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (!(state->err = validate_vet_input(&judgment->a->origin->type,
+ state,
+ thesis_kind_element_equal,
+ vetk_type))) {
+ ptr = NULL;
+ name = judgment->a->origin;
+ name->dependencies = list_dependencies(name, state->temporaries);
+ ptr = name; /* Don't insert `a' before we listed `b's deps */
+ name = judgment->b->origin;
+ name->type = copy_reference(judgment->a->origin->type);
+ name->dependencies = list_dependencies(name, state->temporaries);
+ insert_name(state->temporaries, name);
+ if (ptr) insert_name(state->temporaries, ptr);
+ clear_contextuals(state->temporaries);
+ next_empty_slot(state->slot, state->rule);
+ }
+ break;
+ case slot_type_rule_name:
+ if (!(state->err = validate_rule_name(state))) {
+ free_point(state->slot);
+ state->slot = create_point(FALSE, slot_type_rule_dots, 0, 0, NULL);
+ g_slist_free(g_steal_pointer(&state->support));
+ }
+ break;
+ case slot_type_unknown:
+ break;
+ default:
+ }
+ }
+ }
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(state);
+ else if (state->slot->st == slot_type_thesis) {
+ judgment = get_slot_judgment(state->rule, state->slot);
+ if (state->status == 0) {
+ switch (key) {
+ case 'g':
+ judgment->kind = thesis_kind_generic;
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case 't':
+ judgment->kind = thesis_kind_type;
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case 'e':
+ judgment->kind = thesis_kind_element;
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case '=':
+ state->status = 1;
+ break;
+ default:
+ }
+ }
+ else if (state->status == 1) {
+ switch (key) {
+ case 't':
+ judgment->kind = thesis_kind_type_equal;
+ next_empty_slot(state->slot, state->rule);
+ break;
+ case 'e':
+ judgment->kind = thesis_kind_element_equal;
+ next_empty_slot(state->slot, state->rule);
+ break;
+ default:
+ state->status = 0;
+ }
+ }
+ }
+ else if (state->slot->st == slot_type_ctx_l ||
+ state->slot->st == slot_type_ctx_v ||
+ state->slot->st == slot_type_ctx_t ||
+ state->slot->st == slot_type_ctx_r ||
+ state->slot->st == slot_type_generic_thesis ||
+ state->slot->st == slot_type_type_thesis ||
+ state->slot->st == slot_type_element_thesis_element ||
+ state->slot->st == slot_type_element_thesis_type ||
+ state->slot->st == slot_type_type_equal_thesis_type_1 ||
+ state->slot->st == slot_type_type_equal_thesis_type_2 ||
+ state->slot->st == slot_type_element_equal_thesis_element_1 ||
+ state->slot->st == slot_type_element_equal_thesis_element_2 ||
+ state->slot->st == slot_type_element_equal_thesis_type ||
+ state->slot->st == slot_type_rule_name)
+ handle_input(state, key);
+ }
}
int
main()
{
- bool c_p;
- const char *k, *v;
- char *str;
int i, j, q;
- struct state state;
- struct judgment *j_p;
- struct name *name;
- GSList *l, *type_names;
+ wint_t key;
+ GSList *l;
+ char *str;
+ const char *k, *v;
GHashTableIter iter;
gpointer hkey, hvalue;
- wint_t key;
- struct wrap **addr;
- struct name ** naddr;
+ struct state state;
setlocale(LC_ALL, "");
initscr();
q = (LINES - 3) / 2;
state.running = TRUE;
state.major_mode = ui_major_mode_splash;
- state.minor_mode = ui_input_mode_default;
+ state.input_mode = ui_input_mode_default;
state.rule = create_rule();
- state.judgment = state.rule->conclusion;
- state.dependency = NULL;
- state.workspace_w = subwin(stdscr, q, COLS, 0, 0);
- state.support_w = subwin(stdscr, q, COLS, q + 1, 0);
+ 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.rules = g_hash_table_new_full(g_str_hash, g_str_equal,
NULL, (GDestroyNotify)free_rule);
- state.globals = g_hash_table_new(g_str_hash, g_str_equal);
+ state.globals = g_hash_table_new_full(g_str_hash, g_str_equal,
+ NULL, (GDestroyNotify)free_name);
+ str = strdup("Small");
+ small = create_name(scope_global, name_kind_vet, NULL, NULL, NULL, str);
+ g_hash_table_insert(state.globals, str, small);
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.support = NULL;
- state.caret = 0;
- state.st = slot_type_rule_dots;
state.input = g_string_new(NULL);
- state.backslash_input = g_string_new(NULL);
- state.esc_input = g_string_new(NULL);
+ state.special = g_string_new(NULL);
+ state.command = g_string_new(NULL);
+ state.status = 0;
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.
This is not what we want for the value list. Thus, we will free the
values manually before destroying the table.
*/
- special_character_map = g_hash_table_new_full(g_str_hash, g_str_equal, free, NULL);
+ special_character_map =
+ g_hash_table_new_full(g_str_hash, g_str_equal, free, NULL);
for (i = 0 ; i < sizeof(special_characters) / sizeof(char *) / 2 ; i++) {
k = special_characters[2 * i + 1];
v = special_characters[2 * i + 0];
}
}
- render_splash();
- get_wch(&key);
- state.major_mode = ui_major_mode_workspace;
- render(&state, key);
- while(state.running) {
+ render_splash(&state); /* draw splash once before pausing for input */
+ while (state.running) {
+ /* pause for input */
get_wch(&key);
- switch(state.major_mode) {
+
+ /* handle key logic possibly changing the major mode */
+ switch (state.major_mode) {
+ case ui_major_mode_help:
+ handle_help_input(&state, key);
+ break;
case ui_major_mode_splash:
- render_splash();
- /* no break (intentional) */
+ handle_splash_input(&state, key);
+ break;
+ case ui_major_mode_workspace:
+ handle_workspace_input(&state, key);
+ break;
+ default:
+ }
+
+ /* draw the current major mode */
+ switch (state.major_mode) {
case ui_major_mode_help:
- render_help();
- /* no break (intentional) */
+ render_help(&state);
+ break;
+ case ui_major_mode_splash:
+ render_splash(&state);
+ break;
case ui_major_mode_workspace:
- if (key == KEY_ESC)
- state.running = FALSE;
- else if (state.replacing) {
- if (key == KEY_TAB) {
- 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);
- }
- else {
- switch (state.st) {
- case slot_type_rule_dots:
- if (key == KEY_TAB) {
- next_slot(&state);
- 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 = slot_type_ctx_l;
- }
- 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;
- }
- }
- break;
- case slot_type_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);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_ctx_v:
- if (key == KEY_TAB) {
- naddr = (struct name **)&g_slist_last(state.judgment->vdecls)->data;
- if (!(state.err = validate_vet_input(naddr, &state,
- thesis_kind_unknown, vetk_variable)))
- next_slot(&state);
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_ctx_t:
- if (key == KEY_TAB) {
- naddr = (struct name **)&g_slist_last(state.judgment->vdecls)->data;
- addr = &((*naddr)->type);
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_unknown, vetk_type)))
- next_slot(&state);
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_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 = slot_type_ctx_v;
- }
- break;
- case slot_type_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 slot_type_thesis:
- j_p = state.judgment;
- if (state.status == 0) {
- switch (key) {
- case 'g':
- j_p->kind = thesis_kind_generic;
- next_slot(&state);
- break;
- case 't':
- j_p->kind = thesis_kind_type;
- next_slot(&state);
- break;
- case 'e':
- j_p->kind = thesis_kind_element;
- next_slot(&state);
- break;
- case '=':
- state.status = 1;
- break;
- default:
- }
- }
- else if (state.status == 1) {
- switch (key) {
- case 't':
- j_p->kind = thesis_kind_type_equal;
- next_slot(&state);
- break;
- case 'e':
- j_p->kind = thesis_kind_element_equal;
- next_slot(&state);
- break;
- default:
- state.status = 0;
- }
- }
- break;
- case slot_type_generic_thesis:
- if (key == KEY_TAB) {
- addr = &state.judgment->a;
- if (!(state.err = validate_generic_thesis(&state))) {
- if (requires_replacements(*addr))
- handle_replacements(&state, *addr);
- else
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_type_thesis:
- if (key == KEY_TAB) {
- addr = &state.judgment->a;
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_type,
- vetk_type))) {
- if (requires_replacements(*addr))
- handle_replacements(&state, *addr);
- else
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_element_thesis_element:
- if (key == KEY_TAB) {
- addr = &state.judgment->a;
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_element,
- vetk_element)))
- next_slot(&state);
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_element_thesis_type:
- if (key == KEY_TAB) {
- addr = get_wrap_type_addr(state.judgment->a);
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_element,
- vetk_type))) {
- if (requires_replacements(*addr))
- handle_replacements(&state, *addr);
- else
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_type_equal_thesis_type_1:
- if (key == KEY_TAB) {
- addr = &state.judgment->a;
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_type_equal,
- vetk_type))) {
- if (requires_replacements(*addr))
- handle_replacements(&state, *addr);
- else
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_type_equal_thesis_type_2:
- if (key == KEY_TAB) {
- addr = &state.judgment->b;
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_type_equal,
- vetk_type))) {
- if (requires_replacements(*addr))
- handle_replacements(&state, *addr);
- else
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_element_equal_thesis_element_1:
- if (key == KEY_TAB) {
- addr = &state.judgment->a;
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_element_equal,
- vetk_element))) {
- if (requires_replacements(*addr))
- handle_replacements(&state, *addr);
- else
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_element_equal_thesis_element_2:
- if (key == KEY_TAB) {
- addr = &state.judgment->b;
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_element_equal,
- vetk_element))) {
- if (requires_replacements(*addr))
- handle_replacements(&state, *addr);
- else
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_element_equal_thesis_type:
- if (key == KEY_TAB) {
- addr = get_wrap_type_addr(state.judgment->a);
- if (!(state.err = validate_vet_input(addr, &state,
- thesis_kind_element_equal,
- vetk_type))) {
- *get_wrap_type_addr(state.judgment->b) = copy_wrap(*addr);
- next_slot(&state);
- }
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case slot_type_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;
- }
- }
render(&state, key);
break;
default:
g_slist_free(hvalue);
g_hash_table_destroy(special_character_map);
free_rule(state.rule);
+ free_point(state.slot);
g_hash_table_destroy(state.rules);
g_hash_table_destroy(state.globals);
g_hash_table_destroy(state.gctxs);
g_hash_table_destroy(state.temporaries);
g_slist_free(state.support);
g_string_free(state.input, TRUE);
- g_string_free(state.backslash_input, TRUE);
- g_string_free(state.esc_input, TRUE);
+ g_string_free(state.special, TRUE);
+ g_string_free(state.command, TRUE);
return 0;
}
projects / vouivre.git / commitdiff