#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;
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 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;
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;
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",
"𝟡", "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;
}
}
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);
}
}
{
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 *
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;
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 *);
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
wattroff(w, COLOR_PAIR(pair));
}
if (str && *str != '\0')
- *x += greekstrlen(str);
+ *x += mbstowcs(NULL, str, 0);
else {
if (optional)
*x += 2;
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
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 {
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;
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);
/* 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, "...");
/* Δ */
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);
}
/* 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;
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
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);
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;
}
case 6:
str = "error: inconsistant kinds"; /* TODO: list the two kinds conflicting */
break;
+ case 7:
+ str = "error: incompatible replacement";
+ break;
default:
str = "error: TBD";
}
"=e: judgmentally equal elements";
GHashTableIter iter;
GSList *l;
+ GList *l1;
gpointer key, value;
struct rule *rule;
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);
}
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);
}
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
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); */
}
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);
}
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);
}
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
enum name_kind nk;
struct name *name;
struct wrap *wrap;
+ GSList *deps;
if (*state->input->str == '\0')
return 0;
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)
}
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)
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;
}
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;
}
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;
}
{
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);
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:
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();
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;
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);
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) {
}
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;
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) {
}
}
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;
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)
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)
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;
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 '=':
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:
}
}
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))) {
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
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)
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)
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)
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)
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)
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)
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);
}
}
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 */
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);
projects / vouivre.git / commitdiff