From: admin Date: Sun, 3 Nov 2024 17:33:50 +0000 (-0500) Subject: Refactor wraps and points X-Git-Url: https://git.vouivredigital.com/?a=commitdiff_plain;h=ea50a0cb74e8607b81bd6ee43409cdb09704a0e9;p=vouivre.git Refactor wraps and points - All wraps become references. - Points are no longer based on the memory layout. --- diff --git a/Makefile.am b/Makefile.am index 8ac5d26..229f193 100644 --- a/Makefile.am +++ b/Makefile.am @@ -1,4 +1,4 @@ bin_PROGRAMS = v -v_SOURCES = src/v.c +v_SOURCES = src/name.c src/ui.c src/v.c v_CFLAGS = $(GLIB_CFLAGS) v_LDADD = $(GLIB_LIBS) -lncursesw diff --git a/src/name.c b/src/name.c new file mode 100644 index 0000000..49a90ce --- /dev/null +++ b/src/name.c @@ -0,0 +1,221 @@ +/* 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 . + */ + +#include "name.h" +#include + +struct name * +create_name(enum scope scope, enum name_kind kind, struct reference *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(enum thesis_kind kind, + struct reference *generic_l, struct reference *generic_r, + struct reference *a, struct reference *b, GSList *vdecls) +{ + struct judgment *j; + + j = malloc(sizeof(struct judgment)); + j->kind = kind; + j->generic_l = generic_l; + j->generic_r = generic_r; + j->a = a; + j->b = b; + j->vdecls = vdecls; + return j; +} + +struct rule * +create_rule() +{ + 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); + return rule; +} + +void +free_name(struct name *name) +{ + if (name) { + free_reference(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_judgment(struct judgment *judgment) +{ + if (judgment) { + free_reference(judgment->generic_l); + free_reference(judgment->generic_r); + free_reference(judgment->a); + free_reference(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); + } +} + +/* + * List all names involved (origin or replacement) in the reference, + * recursively. + */ +GSList * +list_reference_names(GSList *list, struct reference *ref) +{ + GSList *l; + + if (!ref) + return list; + list = g_slist_prepend(list, ref->origin); + l = ref->replacements; + while (l) { + list = list_reference_names(list, l->data); + l = l->next; + } + return list; +} + +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; + types = NULL; + type_names = !ptr ? NULL : list_reference_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) + types = g_slist_prepend(types, name->type->origin); + + /* 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; + } + } + } + g_slist_free(types); + + return deps; +} + +GSList * +list_out_of_scope_names(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; +} + +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)); +} diff --git a/src/name.h b/src/name.h new file mode 100644 index 0000000..99187e9 --- /dev/null +++ b/src/name.h @@ -0,0 +1,140 @@ +/* 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 . + */ + +#ifndef DEF_NAME_H +#define DEF_NAME_H + +#include +#include + +/* 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, + }; + +/* A name's scope. */ +enum scope + { + scope_contextual, + scope_local, + scope_global, + }; + +enum name_kind + { + name_kind_generic_context_left, + name_kind_generic_context_right, + name_kind_generic_thesis, + name_kind_vet, /* variable/element/type */ + }; + +/* + * 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, except for the prebuilt terminal type which has + * none (NULL). + */ +struct name +{ + enum scope scope; + enum name_kind kind; + struct reference *type; + struct rule *src; + GSList *dependencies; /* names */ + char *str; +}; + +/* + * Reference an existing (original) name. When doing so, if some of the + * original name's dependencies 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 left and right generic contexts, + * optional variable declarations, and one or two references 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 reference *generic_l; + struct reference *generic_r; + struct reference *a; + struct reference *b; + GSList *vdecls; /* names */ +}; + +struct rule +{ + char *name; + GSList *hypotheses; /* judgments */ + struct judgment *conclusion; +}; + +struct name *create_name(enum scope scope, + enum name_kind kind, + struct reference *type, + struct rule *src, + GSList *dependencies, + char *str); + +struct reference *create_reference(struct name *origin, + GSList *replacements); + +struct judgment *create_judgment(enum thesis_kind kind, + struct reference *generic_l, + struct reference *generic_r, + struct reference *a, + struct reference *b, + GSList *vdecls); + +struct rule *create_rule(); + +void free_name(struct name *name); + +void free_reference(struct reference *reference); + +void free_judgment(struct judgment *judgment); + +void free_rule(struct rule *rule); + +GSList *list_reference_names(GSList *list, + struct reference *ref); + +GSList *list_dependencies(struct name *ptr, + GHashTable *temporaries); + +GSList *list_out_of_scope_names(GSList *dependencies, + GHashTable *temporaries); + +struct reference *copy_reference(struct reference *reference); + +#endif diff --git a/src/ui.c b/src/ui.c new file mode 100644 index 0000000..8f14e68 --- /dev/null +++ b/src/ui.c @@ -0,0 +1,851 @@ +/* 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 . + */ + +#include "name.h" +#include "ui.h" + +#include +#include + +#define NCURSES_WIDECHAR 1 +#include + +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; +} diff --git a/src/ui.h b/src/ui.h new file mode 100644 index 0000000..88bc8d1 --- /dev/null +++ b/src/ui.h @@ -0,0 +1,161 @@ +/* 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 . + */ + +#ifndef DEF_UI_H +#define DEF_UI_H + +#define NCURSES_WIDECHAR 1 +#include + +#define PAIR_NORMAL 1 +#define PAIR_INVERSE 2 +#define PAIR_HL 3 +#define PAIR_SUCCESS 4 +#define PAIR_ERROR 5 + +#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_help, + ui_major_mode_splash, + ui_major_mode_workspace, + }; + +/* 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 = 0, + slot_type_ctx_l = 1, + slot_type_ctx_v = 2, + slot_type_ctx_t = 3, + slot_type_ctx_dots = 4, + slot_type_ctx_r = 5, + slot_type_thesis = 6, + slot_type_generic_thesis = 7, + slot_type_type_thesis = 8, + slot_type_element_thesis_element = 9, + slot_type_element_thesis_type = 10, + slot_type_type_equal_thesis_type_1 = 11, + slot_type_type_equal_thesis_type_2 = 12, + slot_type_element_equal_thesis_element_1 = 13, + slot_type_element_equal_thesis_element_2 = 14, + slot_type_element_equal_thesis_type = 15, + slot_type_rule_name = 16, + slot_type_unknown = 17, + }; + +/* The location information of a slot in a rule is given by a point. */ +struct point { + bool is_conclusion; + int judgment_idx; + int vdecl_idx; + enum slot_type st; + GSList *stack; /* reference stack */ +}; + +struct point *create_point(bool is_conclusion, + enum slot_type st, + int judgment_idx, + int vdecl_idx, + GSList *stack); + +void free_point(struct point *p); + +struct judgment *get_slot_judgment(struct rule *rule, + struct point *slot); + +void *get_slot_data(struct rule *rule, + struct point *slot, + GSList *stack); + +void next_slot(struct point *slot, + struct rule *rule); + +void next_empty_slot(struct point *slot, + struct rule *rule); + +int point_distance(struct rule *rule, + struct point *p1, + struct point *p2); + +void draw_delimiter(WINDOW *w, + int *y, + int *x, + bool virtual, + const char *str); + +void draw_slot(WINDOW *w, + int *y, + int *x, + int *offset, + int caret_offset, + bool virtual, + const char *str, + bool optional); + +void draw_input_slot(WINDOW *w, + int *y, + int *x, + int *offset, + int caret_offset, + bool virtual, + const char *str, + bool optional); + +bool draw_ref(WINDOW *w, + int *y, + int *x, + int *offset, + int caret_offset, + bool virtual, + const char *inputstr, + const struct reference *ref, + bool optional); + +void draw_judgment(WINDOW *w, + int *y, + int *x, + int *offset, + int caret_offset, + bool virtual, + char *inputstr, + struct judgment *judgment, + bool workspace_mode); + +void draw_rule(WINDOW *w, + int *y, + int *x, + int caret_offset, + bool virtual, + char *inputstr, + struct rule *rule, + bool workspace_mode); + +#endif diff --git a/src/v.c b/src/v.c index a50f6f2..3b74d2c 100644 --- a/src/v.c +++ b/src/v.c @@ -16,83 +16,19 @@ * License along with Vouivre. If not, see . */ -#define NCURSES_WIDECHAR 1 -#include -#include +#include "name.h" +#include "ui.h" + #include -#include +#include -#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 #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, @@ -100,86 +36,13 @@ enum vet_kind 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; @@ -189,15 +52,11 @@ struct state 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 */ }; /* @@ -314,17 +173,19 @@ const char *special_characters[] = { */ 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); } /* @@ -358,861 +219,15 @@ clear_locals(struct state *state) 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[] = { @@ -1239,11 +254,13 @@ render_splash() (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; @@ -1254,6 +271,8 @@ render_help() 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(); } @@ -1286,7 +305,7 @@ echo_status(WINDOW *w, int status) 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"; @@ -1299,46 +318,64 @@ echo_status(WINDOW *w, int status) 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; @@ -1346,86 +383,144 @@ render(struct state *state, char kkey) 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))) { @@ -1448,72 +543,22 @@ handle_slot_backspace(struct state *state) /* 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 @@ -1521,30 +566,34 @@ validate_generic_context(struct state *state, bool is_left) { 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, @@ -1552,11 +601,11 @@ validate_generic_context(struct state *state, bool is_left) 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; @@ -1567,33 +616,32 @@ validate_generic_thesis(struct state *state) { 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; @@ -1603,7 +651,7 @@ int 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; @@ -1617,13 +665,13 @@ validate_vet_input(void *addr, struct state *state, 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 */ @@ -1631,17 +679,20 @@ validate_vet_input(void *addr, struct state *state, 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)); @@ -1649,7 +700,11 @@ validate_vet_input(void *addr, struct state *state, 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; } @@ -1660,57 +715,47 @@ validate_replacement(struct state *state) 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 @@ -1730,14 +775,14 @@ validate_rule_name(struct state *state) 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; @@ -1745,42 +790,270 @@ validate_rule_name(struct state *state) } 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(); @@ -1800,35 +1073,36 @@ main() 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]; @@ -1840,320 +1114,34 @@ main() } } - 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: @@ -2168,6 +1156,7 @@ main() 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); @@ -2175,7 +1164,7 @@ main() 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; }