From 2064c2fa76b0f3d569658ba0abace8fd90ddf58f Mon Sep 17 00:00:00 2001 From: admin Date: Sat, 26 Oct 2024 20:19:51 -0400 Subject: [PATCH] Improve handling of name scopes --- help.txt | 13 + src/v.c | 1226 +++++++++++++++++++++++++++++++----------------------- 2 files changed, 723 insertions(+), 516 deletions(-) create mode 100644 help.txt diff --git a/help.txt b/help.txt new file mode 100644 index 0000000..44691b1 --- /dev/null +++ b/help.txt @@ -0,0 +1,13 @@ +Slots +... zero or more of something (variable declarations or hypotheses) +█ empty input +█? optional input + +Global Commands +ESC q quit Vouivre +ESC splash go to splash screen +ESC h go to (this) help screen + +Workspace Commands +TAB move to next slot +RET add an item when on a '...' slot diff --git a/src/v.c b/src/v.c index 17aa16c..9d39ae2 100644 --- a/src/v.c +++ b/src/v.c @@ -36,81 +36,98 @@ #define HYPOTHESES_SPACING 4 #define EMPTY_SLOT "█" +/* The editor is always in either one of these modes. */ enum ui_major_mode { - uimam_splash, - uimam_workspace, - uimam_help, + ui_major_mode_splash, + ui_major_mode_workspace, + ui_major_mode_help, }; -enum ui_minor_mode +/* The editor's input mode. */ +enum ui_input_mode { - uimim_esc, - uimim_backslash, - uimim_default, + ui_input_mode_command, + ui_input_mode_special_characters, + ui_input_mode_default, }; +/* The type of slots in a rule. */ enum slot_type { - st_rule_dots, - st_ctx_l, - st_ctx_v, - st_ctx_t, - st_ctx_dots, - st_ctx_r, - st_thesis, - st_generic_thesis, - st_type_thesis, - st_element_thesis_element, - st_element_thesis_type, - st_type_equal_thesis_type_1, - st_type_equal_thesis_type_2, - st_element_equal_thesis_element_1, - st_element_equal_thesis_element_2, - st_element_equal_thesis_type, - st_rule_name, + 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 { - ctp_before = -1, - ctp_on = 0, - ctp_after = +1, + caret_before_point = -1, + caret_on_point = 0, + caret_after_point = +1, }; +/* Kinds of judgment thesis. */ enum thesis_kind { - tk_generic, - tk_type, - tk_element, - tk_type_equal, - tk_element_equal, - tk_unknown, + thesis_kind_generic, + thesis_kind_type, + thesis_kind_element, + thesis_kind_type_equal, + thesis_kind_element_equal, + thesis_kind_unknown, }; +enum vet_kind + { + vetk_variable, + vetk_element, + vetk_type, + }; + +/* A name's scope. */ enum scope { - s_contextual, - s_local, - s_global, + scope_contextual, + scope_local, + scope_global, }; enum name_kind { - nk_variable, - nk_element, - nk_type, 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; @@ -121,12 +138,23 @@ struct name 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; @@ -144,18 +172,11 @@ struct rule struct judgment *conclusion; }; -/* - * As we draw a rule we move the point (pt - an address) from one variable to - * another down the rabbit hole of the data structure. When that address equals - * the address of the caret, i.e. where we are currently editing, we set the - * flag `is_pt_geq_caret', allowing us to know whether or not to draw dots and - * conditional slots. - */ struct state { bool running; enum ui_major_mode major_mode; - enum ui_minor_mode minor_mode; + enum ui_input_mode minor_mode; struct rule *rule; struct judgment *judgment; struct name *dependency; @@ -163,10 +184,10 @@ struct state WINDOW *support_w; WINDOW *echo_w; GHashTable *rules; /* str -> rule */ - GHashTable *decls; /* str -> name */ + GHashTable *globals; /* str -> name */ + GHashTable *temporaries; /* str -> name */ GHashTable *gctxs; /* str -> name */ GHashTable *gtheses; /* str -> name */ - GHashTable *vets; /* str -> name */ GSList *support; /* rules */ int caret; enum slot_type st; @@ -179,7 +200,11 @@ struct state GSList *stack; /* reference stack */ }; -const char *escaped_strings[] = { +/* + * Special characters that can be entered while in the special character mode by + * typing the corresponding key. + */ +const char *special_characters[] = { "→", "to", "α", "alpha", "β", "beta", @@ -283,9 +308,14 @@ const char *escaped_strings[] = { "𝟡", "99", }; -GHashTable *escaped_table; +/* + * Map of sub-keys to the list of possible corresponding special characters. + * Example: "D" -> "Δ", "𝔻" + */ +GHashTable *special_character_map; -gpointer copy_user_data(gconstpointer src, gpointer data) +gpointer +copy_user_data(gconstpointer src, gpointer data) { return data; } @@ -297,16 +327,16 @@ conclusion_p(struct rule *rule, struct judgment *judgment) } void -clear_contextuals(GHashTable *vets) +clear_contextuals(GHashTable *temporaries) { GHashTableIter iter; gpointer key, value; struct name *name; - g_hash_table_iter_init(&iter, vets); + g_hash_table_iter_init(&iter, temporaries); while (g_hash_table_iter_next(&iter, &key, &value)) { name = value; - if (name->scope == s_contextual) + if (name->scope == scope_contextual) g_hash_table_iter_remove (&iter); } } @@ -316,229 +346,31 @@ clear_locals(struct state *state) { g_hash_table_steal_all(state->gctxs); g_hash_table_steal_all(state->gtheses); - g_hash_table_steal_all(state->vets); + g_hash_table_steal_all(state->temporaries); } -void -next_slot(struct state *state) +GSList * +reference_list_type_names(GSList *list, struct reference *ref) { - switch (state->st) { - case st_rule_dots: - state->st = st_ctx_l; - state->caret += 1; - break; - case st_ctx_l: - state->st = st_ctx_dots; - state->caret += 1; - break; - case st_ctx_v: - state->st = st_ctx_t; - state->caret += 1; - break; - case st_ctx_t: - state->st = st_ctx_dots; - state->caret += 1; - break; - case st_ctx_dots: - state->st = st_ctx_r; - state->caret += 1; - break; - case st_ctx_r: - state->st = st_thesis; - state->caret += 1; - break; - case st_thesis: - switch (state->judgment->kind) - { - case tk_generic: - state->st = st_generic_thesis; - break; - case tk_type: - state->st = st_type_thesis; - break; - case tk_element: - state->st = st_element_thesis_element; - break; - case tk_type_equal: - state->st = st_type_equal_thesis_type_1; - break; - case tk_element_equal: - state->st = st_element_equal_thesis_element_1; - break; - default: - break; - } - break; - case st_generic_thesis: - if (conclusion_p(state->rule, state->judgment)) - state->st = st_rule_name; - else - state->st = st_rule_dots; - state->caret += 1; - clear_contextuals(state->vets); - break; - case st_type_thesis: - if (conclusion_p(state->rule, state->judgment)) - state->st = st_rule_name; - else - state->st = st_rule_dots; - state->caret += 1; - clear_contextuals(state->vets); - break; - case st_element_thesis_element: - if (state->judgment->a->is_origin) { - state->st = st_element_thesis_type; - state->caret += 1; - } - else { - if (conclusion_p(state->rule, state->judgment)) - state->st = st_rule_name; - else - state->st = st_rule_dots; - state->caret += 2; - } - break; - case st_element_thesis_type: - if (conclusion_p(state->rule, state->judgment)) - state->st = st_rule_name; - else - state->st = st_rule_dots; - state->caret += 1; - clear_contextuals(state->vets); - break; - case st_type_equal_thesis_type_1: - state->st = st_type_equal_thesis_type_2; - state->caret += 1; - break; - case st_type_equal_thesis_type_2: - if (conclusion_p(state->rule, state->judgment)) - state->st = st_rule_name; - else - state->st = st_rule_dots; - state->caret += 1; - clear_contextuals(state->vets); - break; - case st_element_equal_thesis_element_1: - state->st = st_element_equal_thesis_element_2; - state->caret += 1; - break; - case st_element_equal_thesis_element_2: - if (state->judgment->a->is_origin) { - state->st = st_element_equal_thesis_type; - state->caret += 1; - } - else { - if (conclusion_p(state->rule, state->judgment)) - state->st = st_rule_name; - else - state->st = st_rule_dots; - state->caret += 2; - } - break; - case st_element_equal_thesis_type: - if (conclusion_p(state->rule, state->judgment)) - state->st = st_rule_name; - else - state->st = st_rule_dots; - state->caret += 1; - clear_contextuals(state->vets); - break; - case st_rule_name: - state->st = st_rule_dots; - state->caret = 0; - break; - default: - } -} + GSList *l; -enum slot_type -prev_thesis_kind_switch(enum thesis_kind tk) -{ - switch (tk) - { - case tk_generic: - return st_generic_thesis; - break; - case tk_type: - return st_type_thesis; - break; - case tk_element: - return st_element_thesis_type; - break; - case tk_type_equal: - return st_type_equal_thesis_type_2; - break; - case tk_element_equal: - return st_element_equal_thesis_type; - break; - default: - return -1; - break; - } + list = g_slist_prepend(list, ref->origin); + l = ref->replacements; + while (l) { + list = reference_list_type_names(list, l->data); + l = l->next; + } + return list; } -enum slot_type -prev_slot(struct state *state) +GSList * +wrap_list_type_names(GSList *list, struct wrap *wrap) { - switch (state->st) { - case st_rule_dots: - if (state->rule->hypotheses) - return prev_thesis_kind_switch(((struct judgment *)g_slist_last(state->rule->hypotheses)->data)->kind); - break; - case st_ctx_l: - return st_rule_dots; - break; - case st_ctx_v: - return st_ctx_dots; - break; - case st_ctx_t: - return st_ctx_v; - break; - case st_ctx_dots: - if (state->judgment->vdecls) - return st_ctx_t; - else - return st_ctx_l; - break; - case st_ctx_r: - return st_ctx_dots; - break; - case st_thesis: - return st_ctx_r; - break; - case st_generic_thesis: - return st_thesis; - break; - case st_type_thesis: - return st_thesis; - break; - case st_element_thesis_element: - return st_thesis; - break; - case st_element_thesis_type: - return st_element_thesis_element; - break; - case st_type_equal_thesis_type_1: - return st_thesis; - break; - case st_type_equal_thesis_type_2: - return st_type_equal_thesis_type_1; - break; - case st_element_equal_thesis_element_1: - return st_thesis; - break; - case st_element_equal_thesis_element_2: - return st_element_equal_thesis_element_1; - break; - case st_element_equal_thesis_type: - return st_element_equal_thesis_element_2; - break; - case st_rule_name: - return prev_thesis_kind_switch(state->judgment->kind); - break; - default: - return -1; - } + if (wrap->is_origin) + list = g_slist_prepend(list, wrap->ptr); + else + list = reference_list_type_names(list, wrap->ptr); + return list; } struct wrap * @@ -585,7 +417,7 @@ create_judgment() struct judgment *j; j = malloc(sizeof(struct judgment)); - j->kind = tk_unknown; + j->kind = thesis_kind_unknown; j->generic_l = NULL; j->generic_r = NULL; j->a = NULL; @@ -687,6 +519,14 @@ get_wrap_type(struct wrap *wrap) 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 *); @@ -710,10 +550,378 @@ copy_wrap(struct wrap *wrap) return create_wrap(FALSE, copy_reference(wrap->ptr)); } -int -greekstrlen(const char *str) +/* 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 *type_names) +{ + GSList *deps, *types, *l, *prev; + GHashTableIter iter; + gpointer key, value; + struct name *name; + + deps = NULL; + 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); + } + + /* 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 +next_slot(struct state *state) +{ + GSList *l; + struct name *name; + + 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; + g_hash_table_insert(state->temporaries, name->str, name); + if (name->type->is_origin) { + name = name->type->ptr; + g_hash_table_insert(state->temporaries, name->str, name); + } + 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) { + name = state->judgment->a->ptr; + if (name->scope != scope_global) + g_hash_table_insert(state->temporaries, name->str, name); + } + 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; + if (state->judgment->a->is_origin) + name = state->judgment->a->ptr; + else + name = ((struct reference *)state->judgment->a->ptr)->origin; + if (state->judgment->a->is_origin) { + l = wrap_list_type_names(NULL, name->type); + name->dependencies = list_dependencies(name, state->temporaries, l); + g_slist_free(g_steal_pointer(&l)); + if (name->scope != scope_global) + g_hash_table_insert(state->temporaries, name->str, name); + } + if (name->type->is_origin) { + name = name->type->ptr; + g_hash_table_insert(state->temporaries, name->str, name); + } + 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) { + name = state->judgment->a->ptr; + g_hash_table_insert(state->temporaries, name->str, name); + } + 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) { + name = state->judgment->b->ptr; + g_hash_table_insert(state->temporaries, name->str, name); + } + 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->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 the dependencies and + temporaries here if needed. */ + *get_wrap_type_addr(state->judgment->b) = + copy_wrap(get_wrap_type(state->judgment->a)); + if (state->judgment->a->is_origin) { + name = state->judgment->a->ptr; + l = wrap_list_type_names(NULL, name->type); + name->dependencies = list_dependencies(name, state->temporaries, l); + g_slist_free(g_steal_pointer(&l)); + g_hash_table_insert(state->temporaries, name->str, name); + } + if (state->judgment->b->is_origin) { + name = state->judgment->b->ptr; + l = wrap_list_type_names(NULL, name->type); + name->dependencies = list_dependencies(name, state->temporaries, l); + g_slist_free(g_steal_pointer(&l)); + g_hash_table_insert(state->temporaries, name->str, name); + } + } + 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; + *get_wrap_type_addr(state->judgment->b) = + copy_wrap(get_wrap_type(state->judgment->a)); + if (state->judgment->a->is_origin) { + name = state->judgment->a->ptr; + l = wrap_list_type_names(NULL, name->type); + name->dependencies = list_dependencies(name, state->temporaries, l); + g_slist_free(g_steal_pointer(&l)); + g_hash_table_insert(state->temporaries, name->str, name); + } + if (state->judgment->b->is_origin) { + name = state->judgment->b->ptr; + l = wrap_list_type_names(NULL, name->type); + name->dependencies = list_dependencies(name, state->temporaries, l); + g_slist_free(g_steal_pointer(&l)); + g_hash_table_insert(state->temporaries, name->str, name); + } + if (state->judgment->a->is_origin) + name = state->judgment->a->ptr; + else + name = ((struct reference *)state->judgment->a->ptr)->origin; + if (name->type->is_origin) { + name = name->type->ptr; + g_hash_table_insert(state->temporaries, name->str, name); + } + + 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) { - return mbstowcs(NULL, str, 0); + 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 @@ -732,7 +940,7 @@ draw_slot(WINDOW *w, int *y, int *x, bool virtual, bool optional, int pair, cons wattroff(w, COLOR_PAIR(pair)); } if (str && *str != '\0') - *x += greekstrlen(str); + *x += mbstowcs(NULL, str, 0); else { if (optional) *x += 2; @@ -744,8 +952,8 @@ draw_slot(WINDOW *w, int *y, int *x, bool virtual, bool optional, int pair, cons void set_ctp_and_pair(enum caret_to_point *ctp, int *pair, int caret, int point) { - *ctp = caret < point ? ctp_before : (caret > point ? ctp_after : ctp_on); - *pair = *ctp == ctp_on ? PAIR_HL : PAIR_NORMAL; + *ctp = caret < point ? caret_before_point : (caret > point ? caret_after_point : caret_on_point); + *pair = *ctp == caret_on_point ? PAIR_HL : PAIR_NORMAL; } void @@ -758,9 +966,9 @@ draw_ref(WINDOW *w, int *y, int *x, bool virtual, if (!ref) { set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) + if (ctp == caret_on_point) draw_slot(w, y, x, virtual, FALSE, pair, inputstr); - else if (ctp == ctp_before) + else if (ctp == caret_before_point) draw_slot(w, y, x, virtual, FALSE, pair, NULL); } else { @@ -790,9 +998,9 @@ draw_wrap(WINDOW *w, int *y, int *x, bool virtual, bool optional, if (!wrap) { set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (ctp == ctp_on) + if (ctp == caret_on_point) draw_slot(w, y, x, virtual, FALSE, pair, inputstr); - else if (ctp == ctp_before) + else if (ctp == caret_before_point) draw_slot(w, y, x, virtual, optional, pair, NULL); else return FALSE; @@ -835,7 +1043,7 @@ draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, var = l->data; if (!(l == judgment->vdecls && !is_prev_displayed)) draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", "); - if (ctp == ctp_on) + 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); @@ -847,7 +1055,7 @@ draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, /* ctx_dots */ set_ctp_and_pair(&ctp, &pair, caret, (*point)++); - if (workspace_mode && (ctp == ctp_before || ctp == ctp_on)) { + 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, "..."); @@ -857,7 +1065,7 @@ draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, /* Δ */ if (workspace_mode || judgment->generic_r) { set_ctp_and_pair(&ctp, &pair, caret, *point); - if (is_prev_displayed && (judgment->generic_r || ctp <= ctp_on)) + 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); } @@ -866,32 +1074,32 @@ draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, /* thesis */ switch (judgment->kind) { - case tk_generic: + case thesis_kind_generic: draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a); break; - case tk_type: + 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 tk_element: + 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 tk_type_equal: + 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 tk_element_equal: + 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 tk_unknown: + case thesis_kind_unknown: set_ctp_and_pair(&ctp, &pair, caret, (*point)++); draw_slot(w, y, x, v, FALSE, pair, NULL); break; @@ -932,13 +1140,13 @@ draw_rule(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, l = l->next; } set_ctp_and_pair(&ctp, &pair, caret, point++); - if (workspace_mode && (ctp <= ctp_on)) + 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 == ctp_on ? inputstr : rule->name); + 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 @@ -972,7 +1180,7 @@ draw_rule(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode, l = l->next; } set_ctp_and_pair(&ctp, &pair, caret, point++); - if (workspace_mode && (ctp <= ctp_on)) + if (workspace_mode && (ctp <= caret_on_point)) draw_slot(w, y, x, virtual, FALSE, pair, "..."); *y += 1; *x = col; wmove(w, *y, *x); @@ -984,7 +1192,7 @@ draw_rule(WINDOW *w, int *y, int *x, bool virtual, bool 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 == ctp_on ? inputstr : rule->name); + 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; } @@ -1066,6 +1274,9 @@ echo_status(WINDOW *w, int status) case 6: str = "error: inconsistant kinds"; /* TODO: list the two kinds conflicting */ break; + case 7: + str = "error: incompatible replacement"; + break; default: str = "error: TBD"; } @@ -1091,6 +1302,7 @@ render(struct state *state, char kkey) "=e: judgmentally equal elements"; GHashTableIter iter; GSList *l; + GList *l1; gpointer key, value; struct rule *rule; @@ -1098,6 +1310,13 @@ render(struct state *state, char kkey) clear(); /* draw debug info */ + i = 0; + l1 = g_hash_table_get_keys(state->temporaries); + 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); @@ -1137,14 +1356,14 @@ render(struct state *state, char kkey) } else { switch (state->major_mode) { - case uimam_workspace: - if (state->st == st_thesis) { + 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); } - else if (state->minor_mode == uimim_backslash) { + else if (state->minor_mode == ui_input_mode_special_characters) { mvwprintw(state->echo_w, 0, 0, "\\"); wprintw(state->echo_w, state->backslash_input->str); } @@ -1171,31 +1390,31 @@ handle_input(struct state *state, char key) struct name *name; if (key == '\\') { - state->minor_mode = uimim_backslash; + state->minor_mode = ui_input_mode_special_characters; state->status = 0; state->backslash_input = g_string_erase(state->backslash_input, 0, -1); } else if (key > 32 && key < 127) { - if (state->minor_mode == uimim_default) + if (state->minor_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(escaped_table, state->backslash_input->str); + l = g_hash_table_lookup(special_character_map, state->backslash_input->str); if (!l) { - state->minor_mode = uimim_default; + state->minor_mode = ui_input_mode_default; } else if (!l->next) { - state->minor_mode = uimim_default; + state->minor_mode = ui_input_mode_default; state->input = g_string_append(state->input, l->data); } } else - state->minor_mode = uimim_default; + state->minor_mode = ui_input_mode_default; } } - if ((name = g_hash_table_lookup(state->decls, state->input->str))) { + if ((name = g_hash_table_lookup(state->globals, state->input->str))) { if (state->support) state->support->data = name->src; else @@ -1206,12 +1425,12 @@ handle_input(struct state *state, char key) void handle_slot_backspace(struct state *state) { - /* if ((state->st == st_generic_thesis) || */ - /* (state->st == st_type_thesis) || */ - /* (state->st == st_element_thesis_element) || */ - /* (state->st == st_type_equal_thesis_type_1) || */ - /* (state->st == st_element_equal_thesis_element_1)) */ - /* state->judgment->kind = tk_unknown; */ + /* if ((state->st == slot_type_generic_thesis) || */ + /* (state->st == slot_type_type_thesis) || */ + /* (state->st == slot_type_element_thesis_element) || */ + /* (state->st == slot_type_type_equal_thesis_type_1) || */ + /* (state->st == slot_type_element_equal_thesis_element_1)) */ + /* state->judgment->kind = thesis_kind_unknown; */ /* state->st = prev_slot(state); */ } @@ -1227,12 +1446,12 @@ handle_input_backspace(struct state *state) void handle_backspace(struct state *state) { - if (state->minor_mode == uimim_default) + if (state->minor_mode == ui_input_mode_default) handle_input_backspace(state); else { if (*state->backslash_input->str == '\0') - state->minor_mode = uimim_default; + state->minor_mode = ui_input_mode_default; else state->backslash_input = g_string_erase(state->backslash_input, 0, -1); } @@ -1242,22 +1461,22 @@ void handle_esc(struct state *state, wint_t key) { if (key == KEY_ESC) { - if (state->minor_mode = uimim_esc) - state->minor_mode = uimim_default; + 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 = uimim_esc; + state->minor_mode = ui_input_mode_command; } } - else if (state->minor_mode == uimim_esc) { + else if (state->minor_mode == ui_input_mode_command) { if (key == KEY_RETURN) { - state->minor_mode = uimim_default; + 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 = uimam_splash; + state->major_mode = ui_major_mode_splash; else if (strcmp(state->esc_input->str, "h") == 0) - state->major_mode = uimam_help; + 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); @@ -1266,33 +1485,21 @@ handle_esc(struct state *state, wint_t key) } GSList * -list_dependencies(GHashTable *vets, enum name_kind nk, enum scope s, void *addr) +filter_out_of_scope(GSList *dependencies, GHashTable *temporaries) { - GSList *l; - GHashTableIter iter; - gpointer key, value; - struct name *name; + GSList *l, *oos; + struct name *dep, *name; - l = NULL; - g_hash_table_iter_init(&iter, vets); - while (g_hash_table_iter_next(&iter, &key, &value)) { - name = value; - if (nk == nk_generic_context_left || nk == nk_generic_context_right) { - if (name->scope == s_contextual) - l = g_slist_prepend(l, name); - } - else { - /* The name is a dependency if it goes out of scope sooner than its - target. This is always the case when the target is global. This is - also the case when the target is local and the name contextual. A - variable is not a dependency of its declaration type */ - if (s == s_global || (s == s_local && - name->scope == s_contextual && - &name->type != addr)) - l = g_slist_prepend(l, 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 l; + return oos; } int @@ -1301,6 +1508,7 @@ validate_generic_context(struct state *state, bool is_left) enum name_kind nk; struct name *name; struct wrap *wrap; + GSList *deps; if (*state->input->str == '\0') return 0; @@ -1309,9 +1517,10 @@ validate_generic_context(struct state *state, bool is_left) 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(name->dependencies, + g_slist_copy_deep(deps, copy_user_data, NULL))); if (is_left) @@ -1323,11 +1532,11 @@ validate_generic_context(struct state *state, bool is_left) } else if (conclusion_p(state->rule, state->judgment)) return 3; - name = create_name(s_local, + name = create_name(scope_local, nk, NULL, state->rule, - list_dependencies(state->vets, nk, s_local, NULL), + list_dependencies(NULL, state->temporaries, NULL), strdup(state->input->str)); wrap = create_wrap(TRUE, name); if (is_left) @@ -1345,14 +1554,16 @@ validate_generic_thesis(struct state *state) enum name_kind nk; struct name *name; struct wrap *wrap; + GSList *deps; if (*state->input->str == '\0') return 1; name = g_hash_table_lookup(state->gtheses, state->input->str); if (name) { + deps = filter_out_of_scope(name->dependencies, state->temporaries); wrap = create_wrap(FALSE, create_reference(name, - g_slist_copy_deep(name->dependencies, + g_slist_copy_deep(deps, copy_user_data, NULL))); state->judgment->a = wrap; @@ -1361,12 +1572,11 @@ validate_generic_thesis(struct state *state) } else if (conclusion_p(state->rule, state->judgment)) return 3; - name = create_name(s_local, + name = create_name(scope_local, nk_generic_thesis, NULL, state->rule, - list_dependencies(state->vets, nk_generic_thesis, - s_local, NULL), + list_dependencies(NULL, state->temporaries, NULL), strdup(state->input->str)); wrap = create_wrap(TRUE, name); state->judgment->a = wrap; @@ -1376,65 +1586,57 @@ validate_generic_thesis(struct state *state) } int -validate_vet_input(void *addr, struct state *state, enum name_kind nk) +validate_vet_input(void *addr, struct state *state, + enum thesis_kind tk, enum vet_kind vetk) { - bool is_c; - enum thesis_kind tk; + bool no_deps, c_p; + GSList *l, *deps; + enum scope scope; struct name *name; - GSList *l; - tk = state->judgment->kind; - is_c = conclusion_p(state->rule, state->judgment); if (*state->input->str == '\0') return 1; - if ((name = g_hash_table_lookup(state->decls, state->input->str))) { - if (nk == nk_variable || tk == tk_type || - (tk == tk_element && nk == nk_element)) - return 5; - if (name->kind != nk) - return 6; - state->input = g_string_erase(state->input, 0, -1); - l = g_slist_copy_deep(name->dependencies, copy_user_data, NULL); - *(struct wrap **)addr = create_wrap(FALSE, create_reference(name, l)); - return 0; - } - if ((name = g_hash_table_lookup(state->vets, state->input->str))) { - if (nk == nk_variable) + name = g_hash_table_lookup(state->globals, state->input->str); + if (!name) + name = g_hash_table_lookup(state->temporaries, state->input->str); + if (name) { + if (vetk == vetk_variable) return 5; - if (name->kind != nk) - return 6; state->input = g_string_erase(state->input, 0, -1); - l = g_slist_copy_deep(name->dependencies, copy_user_data, NULL); + 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)); - return 0; - } - if (nk == nk_variable) { - name = create_name(s_contextual, nk_element, NULL, state->rule, - NULL, - strdup(state->input->str)); - g_hash_table_insert(state->vets, name->str, name); - state->input = g_string_erase(state->input, 0, -1); - *(struct name **)addr = name; - return 0; - } - if (is_c) { - if (tk == tk_type_equal || - tk == tk_element_equal || - (tk == tk_unknown && nk == nk_type) || /* variable type */ - (tk == tk_element && nk == nk_type)) /* element type */ - return 3; - name = create_name(s_global, nk, NULL, state->rule, - list_dependencies(state->vets, nk, s_global, addr), - strdup(state->input->str)); } else { - name = create_name(s_local, nk, NULL, state->rule, - list_dependencies(state->vets, nk, s_local, addr), + c_p = conclusion_p(state->rule, state->judgment); + if (c_p && + (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 */ + return 3; + if (vetk == vetk_variable || + (tk == thesis_kind_element && vetk == vetk_element) || + (tk == thesis_kind_element_equal && vetk == vetk_element)) + no_deps = TRUE; + 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))) + scope = scope_global; + else + scope = scope_local; + name = create_name(scope, nk_vet, NULL, state->rule, + no_deps ? NULL : + list_dependencies(NULL, state->temporaries, NULL), strdup(state->input->str)); - g_hash_table_insert(state->vets, name->str, name); + state->input = g_string_erase(state->input, 0, -1); + if (vetk == vetk_variable) + *(struct name **)addr = name; + else + *(struct wrap **)addr = create_wrap(TRUE, name); } - state->input = g_string_erase(state->input, 0, -1); - *(struct wrap **)addr = create_wrap(TRUE, name); return 0; } @@ -1443,28 +1645,43 @@ validate_replacement(struct state *state) { bool is_c; guint idx; - GSList *reps, *l; - struct name *dep, *name; + GSList *reps, *l, *deps; + struct name *dep, *name, *addr, *dtname; struct reference *ref; if (*state->input->str == '\0') return 1; - name = g_hash_table_lookup(state->decls, state->input->str); + name = g_hash_table_lookup(state->globals, state->input->str); if (!name) - name = g_hash_table_lookup(state->vets, state->input->str); + 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); - if (name->kind != dep->kind) - return 6; - /* TODO: check that the types of (the input) `name' and of `dep' are - compatible - */ + /* 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 */ + } + } + /* set the state for the next slot */ l = g_slist_nth(ref->replacements, idx); - reps = g_slist_copy_deep(name->dependencies, copy_user_data, NULL); + 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); @@ -1498,10 +1715,16 @@ validate_rule_name(struct state *state) g_hash_table_insert(state->rules, state->rule->name, rule); c = rule->conclusion; switch (c->kind) { - case tk_type: + case thesis_kind_type: if (c->a->is_origin) { name = c->a->ptr; - g_hash_table_insert(state->decls, name->str, name); + g_hash_table_insert(state->globals, name->str, name); + } + break; + case thesis_kind_element: + if (c->a->is_origin) { + name = c->a->ptr; + g_hash_table_insert(state->globals, name->str, name); } break; default: @@ -1537,12 +1760,13 @@ main() int i, j, q; struct state state; struct judgment *j_p; - GSList *l; + struct name *name; + GSList *l, *type_names; GHashTableIter iter; gpointer hkey, hvalue; wint_t key; struct wrap **addr; - void *naddr; + struct name ** naddr; setlocale(LC_ALL, ""); initscr(); @@ -1561,8 +1785,8 @@ main() bkgd(COLOR_PAIR(PAIR_NORMAL)); q = (LINES - 3) / 2; state.running = TRUE; - state.major_mode = uimam_splash; - state.minor_mode = uimim_default; + state.major_mode = ui_major_mode_splash; + state.minor_mode = ui_input_mode_default; state.rule = create_rule(); state.judgment = state.rule->conclusion; state.dependency = NULL; @@ -1571,13 +1795,13 @@ main() 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.decls = g_hash_table_new(g_str_hash, g_str_equal); + state.globals = g_hash_table_new(g_str_hash, g_str_equal); state.gctxs = g_hash_table_new(g_str_hash, g_str_equal); state.gtheses = g_hash_table_new(g_str_hash, g_str_equal); - state.vets = 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 = st_rule_dots; + 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); @@ -1590,32 +1814,32 @@ main() This is not what we want for the value list. Thus, we will free the values manually before destroying the table. */ - escaped_table = g_hash_table_new_full(g_str_hash, g_str_equal, free, NULL); - for (i = 0 ; i < sizeof(escaped_strings) / sizeof(char *) / 2 ; i++) { - k = escaped_strings[2 * i + 1]; - v = escaped_strings[2 * i + 0]; + 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]; for (j = 1 ; j <= strlen(k) ; j++) { str = strndup(k, j); - l = g_hash_table_lookup(escaped_table, str); + l = g_hash_table_lookup(special_character_map, str); l = g_slist_prepend(l, (void *)v); - g_hash_table_insert(escaped_table, str, l); + g_hash_table_insert(special_character_map, str, l); } } render_splash(); get_wch(&key); - state.major_mode = uimam_workspace; + state.major_mode = ui_major_mode_workspace; render(&state, key); while(state.running) { get_wch(&key); switch(state.major_mode) { - case uimam_splash: + case ui_major_mode_splash: render_splash(); /* no break (intentional) */ - case uimam_help: + case ui_major_mode_help: render_help(); /* no break (intentional) */ - case uimam_workspace: + case ui_major_mode_workspace: if (key == KEY_ESC) state.running = FALSE; else if (state.replacing) { @@ -1636,7 +1860,7 @@ main() } else { switch (state.st) { - case st_rule_dots: + case slot_type_rule_dots: if (key == KEY_TAB) { next_slot(&state); state.judgment = state.rule->conclusion; @@ -1644,7 +1868,7 @@ main() else if (key == KEY_RETURN) { state.judgment = create_judgment(); state.rule->hypotheses = g_slist_append(state.rule->hypotheses, state.judgment); - state.st = st_ctx_l; + state.st = slot_type_ctx_l; } else if (key == KEY_BACKSPACE) { if (state.rule->hypotheses) { @@ -1654,7 +1878,7 @@ main() } } break; - case st_ctx_l: + case slot_type_ctx_l: if (key == KEY_TAB) { if (!(state.err = validate_generic_context(&state, TRUE))) { addr = &state.judgment->generic_l; @@ -1669,10 +1893,11 @@ main() else handle_input(&state, key); break; - case st_ctx_v: + case slot_type_ctx_v: if (key == KEY_TAB) { - naddr = &g_slist_last(state.judgment->vdecls)->data; - if (!(state.err = validate_vet_input(naddr, &state, nk_variable))) + 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) @@ -1680,11 +1905,12 @@ main() else handle_input(&state, key); break; - case st_ctx_t: + case slot_type_ctx_t: if (key == KEY_TAB) { - naddr = &g_slist_last(state.judgment->vdecls)->data; - addr = &((*((struct name **)naddr))->type); - if (!(state.err = validate_vet_input(addr, &state, nk_type))) + 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) @@ -1692,15 +1918,15 @@ main() else handle_input(&state, key); break; - case st_ctx_dots: + 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 = st_ctx_v; + state.st = slot_type_ctx_v; } break; - case st_ctx_r: + case slot_type_ctx_r: if (key == KEY_TAB) { if (!(state.err = validate_generic_context(&state, FALSE))) { addr = &state.judgment->generic_r; @@ -1717,20 +1943,20 @@ main() else handle_input(&state, key); break; - case st_thesis: + case slot_type_thesis: j_p = state.judgment; if (state.status == 0) { switch (key) { case 'g': - j_p->kind = tk_generic; + j_p->kind = thesis_kind_generic; next_slot(&state); break; case 't': - j_p->kind = tk_type; + j_p->kind = thesis_kind_type; next_slot(&state); break; case 'e': - j_p->kind = tk_element; + j_p->kind = thesis_kind_element; next_slot(&state); break; case '=': @@ -1742,11 +1968,11 @@ main() else if (state.status == 1) { switch (key) { case 't': - j_p->kind = tk_type_equal; + j_p->kind = thesis_kind_type_equal; next_slot(&state); break; case 'e': - j_p->kind = tk_element_equal; + j_p->kind = thesis_kind_element_equal; next_slot(&state); break; default: @@ -1754,7 +1980,7 @@ main() } } break; - case st_generic_thesis: + case slot_type_generic_thesis: if (key == KEY_TAB) { addr = &state.judgment->a; if (!(state.err = validate_generic_thesis(&state))) { @@ -1769,10 +1995,12 @@ main() else handle_input(&state, key); break; - case st_type_thesis: + case slot_type_type_thesis: if (key == KEY_TAB) { addr = &state.judgment->a; - if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + if (!(state.err = validate_vet_input(addr, &state, + thesis_kind_type, + vetk_type))) { if (requires_replacements(*addr)) handle_replacements(&state, *addr); else @@ -1784,10 +2012,12 @@ main() else handle_input(&state, key); break; - case st_element_thesis_element: + case slot_type_element_thesis_element: if (key == KEY_TAB) { addr = &state.judgment->a; - if (!(state.err = validate_vet_input(addr, &state, nk_element))) + if (!(state.err = validate_vet_input(addr, &state, + thesis_kind_element, + vetk_element))) next_slot(&state); } else if (key == KEY_BACKSPACE) @@ -1795,22 +2025,16 @@ main() else handle_input(&state, key); break; - case st_element_thesis_type: + 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, nk_type))) { + 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); - /* if ((*addr)->is_origin == FALSE && */ - /* ((struct reference *)((*addr)->ptr))->replacements) { */ - /* state.replacing = TRUE; */ - /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ - /* state.caret += 1; */ - /* } */ - /* else */ - /* next_slot(&state); */ } } else if (key == KEY_BACKSPACE) @@ -1818,22 +2042,16 @@ main() else handle_input(&state, key); break; - case st_type_equal_thesis_type_1: + case slot_type_type_equal_thesis_type_1: if (key == KEY_TAB) { addr = &state.judgment->a; - if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + 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); - /* if ((*addr)->is_origin == FALSE && */ - /* ((struct reference *)((*addr)->ptr))->replacements) { */ - /* state.replacing = TRUE; */ - /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ - /* state.caret += 1; */ - /* } */ - /* else */ - /* next_slot(&state); */ } } else if (key == KEY_BACKSPACE) @@ -1841,22 +2059,16 @@ main() else handle_input(&state, key); break; - case st_type_equal_thesis_type_2: + case slot_type_type_equal_thesis_type_2: if (key == KEY_TAB) { addr = &state.judgment->b; - if (!(state.err = validate_vet_input(addr, &state, nk_type))) { + 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); - /* if ((*addr)->is_origin == FALSE && */ - /* ((struct reference *)((*addr)->ptr))->replacements) { */ - /* state.replacing = TRUE; */ - /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ - /* state.caret += 1; */ - /* } */ - /* else */ - /* next_slot(&state); */ } } else if (key == KEY_BACKSPACE) @@ -1864,22 +2076,16 @@ main() else handle_input(&state, key); break; - case st_element_equal_thesis_element_1: + case slot_type_element_equal_thesis_element_1: if (key == KEY_TAB) { addr = &state.judgment->a; - if (!(state.err = validate_vet_input(addr, &state, nk_element))) { + 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); - /* if ((*addr)->is_origin == FALSE && */ - /* ((struct reference *)((*addr)->ptr))->replacements) { */ - /* state.replacing = TRUE; */ - /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ - /* state.caret += 1; */ - /* } */ - /* else */ - /* next_slot(&state); */ } } else if (key == KEY_BACKSPACE) @@ -1887,22 +2093,16 @@ main() else handle_input(&state, key); break; - case st_element_equal_thesis_element_2: + case slot_type_element_equal_thesis_element_2: if (key == KEY_TAB) { addr = &state.judgment->b; - if (!(state.err = validate_vet_input(addr, &state, nk_element))) { + 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); - /* if ((*addr)->is_origin == FALSE && */ - /* ((struct reference *)((*addr)->ptr))->replacements) { */ - /* state.replacing = TRUE; */ - /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ - /* state.caret += 1; */ - /* } */ - /* else */ - /* next_slot(&state); */ } } else if (key == KEY_BACKSPACE) @@ -1910,19 +2110,13 @@ main() else handle_input(&state, key); break; - case st_element_equal_thesis_type: + 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, nk_type))) { + if (!(state.err = validate_vet_input(addr, &state, + thesis_kind_element_equal, + vetk_type))) { *get_wrap_type_addr(state.judgment->b) = copy_wrap(*addr); - - /* if ((*addr)->is_origin == FALSE && */ - /* ((struct reference *)((*addr)->ptr))->replacements) { */ - /* state.replacing = TRUE; */ - /* state.stack = g_slist_prepend(state.stack, (*addr)->ptr); */ - /* state.caret += 1; */ - /* } */ - /* else */ next_slot(&state); } } @@ -1931,7 +2125,7 @@ main() else handle_input(&state, key); break; - case st_rule_name: + case slot_type_rule_name: if (key == KEY_TAB) { if (!(state.err = validate_rule_name(&state))) { /* reset the workspace to initial state */ @@ -1955,16 +2149,16 @@ main() delwin(state.support_w); delwin(state.echo_w); endwin(); - g_hash_table_iter_init(&iter, escaped_table); + g_hash_table_iter_init(&iter, special_character_map); while (g_hash_table_iter_next(&iter, &hkey, &hvalue)) g_slist_free(hvalue); - g_hash_table_destroy(escaped_table); + g_hash_table_destroy(special_character_map); free_rule(state.rule); g_hash_table_destroy(state.rules); - g_hash_table_destroy(state.decls); + g_hash_table_destroy(state.globals); g_hash_table_destroy(state.gctxs); g_hash_table_destroy(state.gtheses); - g_hash_table_destroy(state.vets); + g_hash_table_destroy(state.temporaries); g_slist_free(state.support); g_string_free(state.input, TRUE); g_string_free(state.backslash_input, TRUE); -- 2.39.5