#include <glib.h>
#include <signal.h>
-#define PAIR_BW 1
-#define PAIR_WB 2
+#define PAIR_NORMAL 1
+#define PAIR_INVERSE 2
#define PAIR_HL 3
#define PAIR_SUCCESS 4
#define PAIR_ERROR 5
#define HYPOTHESES_SPACING 4
#define EMPTY_SLOT "█"
-enum ui_state
+enum ui_major_mode
{
- uis_splash,
- uis_workspace,
+ uimam_splash,
+ uimam_workspace,
+ uimam_help,
+ };
+
+enum ui_minor_mode
+ {
+ uimim_esc,
+ uimim_backslash,
+ uimim_default,
};
enum slot_type
st_ctx_dots,
st_ctx_r,
st_thesis,
- st_a,
- st_b,
- st_c,
+ 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,
};
nk_variable,
nk_element,
nk_type,
- nk_generic_context,
+ nk_generic_context_left,
+ nk_generic_context_right,
nk_generic_thesis,
};
struct reference
{
struct name *origin;
- GSList *replacements; /* wraps */
-};
-
-struct vdecl
-{
- struct name *elem;
- struct wrap *type;
+ GSList *replacements; /* references */
};
struct judgment
struct wrap *generic_r;
struct wrap *a;
struct wrap *b;
- GSList *vdecls;
+ GSList *vdecls; /* names */
};
struct rule
struct judgment *conclusion;
};
-struct drawing_params
-{
- bool virtual;
- bool hide;
- WINDOW *w;
- int y;
- int x;
- int row;
- int col;
- int c;
- int m;
- int n;
- int r;
- int s;
- int stacked;
- int lw;
- int jw;
-};
-
/*
* 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
struct state
{
bool running;
- enum ui_state mode;
+ enum ui_major_mode major_mode;
+ enum ui_minor_mode minor_mode;
struct rule *rule;
struct judgment *judgment;
struct name *dependency;
int caret;
enum slot_type st;
GString *input;
- GString *escaped_input;
+ GString *backslash_input;
+ GString *esc_input;
int status;
- bool escape;
int err;
+ bool replacing;
+ GSList *stack; /* reference stack */
};
const char *escaped_strings[] = {
GHashTable *escaped_table;
+gpointer copy_user_data(gconstpointer src, gpointer data)
+{
+ return data;
+}
+
+bool
+conclusion_p(struct rule *rule, struct judgment *judgment)
+{
+ return judgment == rule->conclusion ? TRUE : FALSE;
+}
+
+void
+clear_contextuals(GHashTable *vets)
+{
+ GHashTableIter iter;
+ gpointer key, value;
+ struct name *name;
+
+ g_hash_table_iter_init(&iter, vets);
+ while (g_hash_table_iter_next(&iter, &key, &value)) {
+ name = value;
+ if (name->scope == s_contextual)
+ g_hash_table_iter_remove (&iter);
+ }
+}
+
+void
+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);
+}
+
+void
+next_slot(struct state *state)
+{
+ 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:
+ }
+}
+
+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;
+ }
+}
+
+enum slot_type
+prev_slot(struct state *state)
+{
+ 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;
+ }
+}
+
struct wrap *
create_wrap(bool is_origin, void *ptr)
{
return name;
}
+struct reference *
+create_reference(struct name *origin, GSList *replacements)
+{
+ struct reference *ref;
+
+ ref = malloc(sizeof(struct reference));
+ ref->origin = origin;
+ ref->replacements = replacements;
+ return ref;
+}
+
struct judgment *
create_judgment()
{
return j;
}
-
struct rule *
create_rule()
{
}
void free_wrap(struct wrap *);
+void free_reference(struct reference *);
void
free_name(struct name *name)
free_reference(struct reference *ref)
{
if (ref) {
- free_name(ref->origin);
- g_slist_free_full(ref->replacements, (GDestroyNotify)free_wrap);
+ g_slist_free_full(ref->replacements, (GDestroyNotify)free_reference);
free(ref);
}
}
-
void
free_wrap(struct wrap *wrap)
{
}
}
-void
-free_vdecl(struct vdecl *decl)
-{
- if (decl) {
- free_name(decl->elem);
- free_wrap(decl->type);
- free(decl);
- }
-}
-
-
void
free_judgment(struct judgment *judgment)
{
free_wrap(judgment->generic_r);
free_wrap(judgment->a);
free_wrap(judgment->b);
- g_slist_free_full(judgment->vdecls, (GDestroyNotify)free_vdecl);
+ g_slist_free_full(judgment->vdecls, (GDestroyNotify)free_name);
free(judgment);
}
}
}
}
+struct wrap **
+get_wrap_type_addr(struct wrap *wrap)
+{
+ if (wrap) {
+ if (wrap->is_origin)
+ return &(((struct name *)wrap->ptr)->type);
+ return &(((struct reference *)wrap->ptr)->origin->type);
+ }
+ return NULL;
+}
+
+struct wrap *
+get_wrap_type(struct wrap *wrap)
+{
+ struct wrap **addr;
+
+ addr = get_wrap_type_addr(wrap);
+ if (addr)
+ return *addr;
+ return NULL;
+}
+
+struct wrap *copy_wrap(struct wrap *);
+struct reference *copy_reference(struct reference *);
+
+struct reference *
+copy_reference(struct reference *reference)
+{
+ if (!reference)
+ return NULL;
+ return create_reference(reference->origin,
+ g_slist_copy_deep(reference->replacements,
+ (GCopyFunc)copy_reference, NULL));
+}
+
+struct wrap *
+copy_wrap(struct wrap *wrap)
+{
+ if (!wrap)
+ return NULL;
+ if (wrap->is_origin)
+ return create_wrap(FALSE, create_reference(wrap->ptr, NULL));
+ return create_wrap(FALSE, copy_reference(wrap->ptr));
+}
+
int
greekstrlen(const char *str)
{
}
void
-draw_wrap(WINDOW *w, int *y, int *x, bool virtual, bool optional,
- int pair, struct wrap *wrap)
+set_ctp_and_pair(enum caret_to_point *ctp, int *pair, int caret, int point)
{
- struct reference *r;
+ *ctp = caret < point ? ctp_before : (caret > point ? ctp_after : ctp_on);
+ *pair = *ctp == ctp_on ? PAIR_HL : PAIR_NORMAL;
+}
+
+void
+draw_ref(WINDOW *w, int *y, int *x, bool virtual,
+ int caret, int *point, char *inputstr, struct reference *ref)
+{
+ int pair;
+ enum caret_to_point ctp;
GSList *l;
- if (!wrap)
- draw_slot(w, y, x, virtual, optional, pair, NULL);
+ if (!ref) {
+ set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
+ if (ctp == ctp_on)
+ draw_slot(w, y, x, virtual, FALSE, pair, inputstr);
+ else if (ctp == ctp_before)
+ draw_slot(w, y, x, virtual, FALSE, pair, NULL);
+ }
else {
- if (wrap->is_origin) {
- draw_slot(w, y, x, virtual, optional, pair,
- ((struct name *)wrap->ptr)->str);
- }
- else {
- r = wrap->ptr;
- draw_slot(w, y, x, virtual, optional, pair, r->origin->str);
- l = r->replacements;
- if (l) {
- draw_slot(w, y, x, virtual, FALSE, PAIR_BW, "[");
- while (l) {
- draw_wrap(w, y, x, virtual, FALSE, pair, l->data);
- l = l->next;
- if (l)
- draw_slot(w, y, x, virtual, FALSE, PAIR_BW, ", ");
- }
- draw_slot(w, y, x, virtual, FALSE, PAIR_BW, "]");
+ set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
+ draw_slot(w, y, x, virtual, FALSE, pair, ref->origin->str);
+ l = ref->replacements;
+ if (l) {
+ draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, "[");
+ while (l) {
+ draw_ref(w, y, x, virtual, caret, point, inputstr, l->data);
+ l = l->next;
+ if (l)
+ draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, ", ");
}
+ draw_slot(w, y, x, virtual, FALSE, PAIR_NORMAL, "]");
}
}
}
-struct wrap *
-get_wrap_type(struct wrap *wrap)
+bool /* is displayed ? */
+draw_wrap(WINDOW *w, int *y, int *x, bool virtual, bool optional,
+ int caret, int *point, char *inputstr, struct wrap *wrap)
{
- if (wrap) {
- if (wrap->is_origin)
- return ((struct name *)wrap->ptr)->type;
+ int pair;
+ enum caret_to_point ctp;
+ GSList *l;
+
+ if (!wrap) {
+ set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
+ if (ctp == ctp_on)
+ draw_slot(w, y, x, virtual, FALSE, pair, inputstr);
+ else if (ctp == ctp_before)
+ draw_slot(w, y, x, virtual, optional, pair, NULL);
else
- return ((struct reference *)wrap->ptr)->origin->type;
+ return FALSE;
}
- else
- return NULL;
-}
-
-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_BW;
+ else {
+ if (wrap->is_origin) {
+ set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
+ draw_slot(w, y, x, virtual, optional, pair,
+ ((struct name *)wrap->ptr)->str);
+ }
+ else
+ draw_ref(w, y, x, virtual, caret, point, inputstr, wrap->ptr);
+ }
+ return TRUE;
}
void
draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode,
int caret, int *point, char *inputstr, struct judgment *judgment)
{
- bool v, prev_not_displayed;
+ bool v, is_prev_displayed;
int pair;
GSList *l;
- struct vdecl *decl;
+ struct name *var;
enum caret_to_point ctp;
v = virtual;
/* Γ */
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- prev_not_displayed = FALSE;
- if (judgment->generic_l)
- draw_wrap(w, y, x, v, TRUE, pair, judgment->generic_l);
- else if (workspace_mode) {
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else if (ctp == ctp_before)
- draw_slot(w, y, x, v, TRUE, pair, NULL);
- else
- prev_not_displayed = TRUE;
+ is_prev_displayed = FALSE;
+ if (workspace_mode || judgment->generic_l) {
+ is_prev_displayed = draw_wrap(w, y, x, v, TRUE,
+ caret, point, inputstr, judgment->generic_l);
}
- else
- prev_not_displayed = TRUE;
/* vdecls */
l = judgment->vdecls;
while (l) {
set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- decl = l->data;
- if (!(l == judgment->vdecls && prev_not_displayed))
- draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
+ var = l->data;
+ if (!(l == judgment->vdecls && !is_prev_displayed))
+ draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", ");
if (ctp == ctp_on)
draw_slot(w, y, x, v, FALSE, pair, inputstr);
else
- draw_slot(w, y, x, v, FALSE, pair, decl->elem->str);
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " : ");
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, decl->type);
- prev_not_displayed = FALSE;
+ draw_slot(w, y, x, v, FALSE, pair, var->str);
+ draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " : ");
+ draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, var ? var->type : NULL);
+ is_prev_displayed = TRUE;
l = l->next;
}
/* ctx_dots */
set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
if (workspace_mode && (ctp == ctp_before || ctp == ctp_on)) {
- if (!prev_not_displayed)
- draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
+ if (is_prev_displayed)
+ draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", ");
draw_slot(w, y, x, v, FALSE, pair, "...");
- prev_not_displayed = FALSE;
+ is_prev_displayed = TRUE;
}
/* Δ */
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (judgment->generic_r) {
- if (!prev_not_displayed)
- draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
- draw_wrap(w, y, x, v, TRUE, pair, judgment->generic_r);
- }
- else if (workspace_mode) {
- if (ctp == ctp_on) {
- if (!prev_not_displayed)
- draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- }
- else if (ctp == ctp_before) {
- if (!prev_not_displayed)
- draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
- draw_slot(w, y, x, v, TRUE, pair, NULL);
- }
+ if (workspace_mode || judgment->generic_r) {
+ set_ctp_and_pair(&ctp, &pair, caret, *point);
+ if (is_prev_displayed && (judgment->generic_r || ctp <= ctp_on))
+ draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, ", ");
+ draw_wrap(w, y, x, v, TRUE, caret, point, inputstr, judgment->generic_r);
}
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " ⊢ ");
+ draw_slot(w, y, x, v, FALSE, PAIR_NORMAL, " ⊢ ");
/* thesis */
switch (judgment->kind) {
case tk_generic:
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, judgment->a);
+ draw_wrap(w, y, x, v, FALSE, caret, point, inputstr, judgment->a);
break;
case tk_type:
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, judgment->a);
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " 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:
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, judgment->a);
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " : ");
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, get_wrap_type(judgment->a));
+ 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:
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, judgment->a);
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " ≐ ");
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, judgment->b);
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " type");
+ 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:
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, judgment->a);
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " ≐ ");
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, judgment->b);
- draw_slot(w, y, x, v, FALSE, PAIR_BW, " : ");
- set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
- if (ctp == ctp_on)
- draw_slot(w, y, x, v, FALSE, pair, inputstr);
- else
- draw_wrap(w, y, x, v, FALSE, pair, get_wrap_type(judgment->a));
+ 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:
set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
void
render_splash()
{
+ int i, n;
+ static const char *strs[] = {
+ "VOUIVRE",
+ "",
+ "version 0.2.0",
+ "by Vouivre Digital Corporation",
+ "",
+ "type ESC q RET to quit",
+ "type ESC splash RET to return to this screen",
+ "type ESC h RET to get help",
+ "type any other key to continue",
+ };
+
+ n = sizeof(strs) / sizeof(char *);
clear();
- mvprintw(0, 0, "VOUIVRE version 0.2.0");
- mvprintw(1, 0, "press any key to continue");
+ for (i = 0 ; i < 5 ; i++) {
+ mvprintw((LINES - n) / 2 + i,
+ (COLS - strlen(strs[i])) / 2,
+ strs[i]);
+ }
+ for (i = 5 ; i < n ; i++) {
+ mvprintw((LINES - n) / 2 + i,
+ (COLS - strlen(strs[6])) / 2,
+ strs[i]);
+ }
+ refresh();
+}
+
+void
+render_help()
+{
+ int c;
+ FILE *fd;
+
+ clear();
+ fd = fopen("help.txt", "r");
+ move(0, 0);
+ while ((c = fgetc(fd)) != EOF)
+ addch(c);
+ fclose(fd);
refresh();
}
str = "error: left and right generic contexts must differ";
break;
case 5:
- str = "error: type already defined";
+ str = "error: name already defined";
break;
case 6:
str = "error: inconsistant kinds"; /* TODO: list the two kinds conflicting */
}
void
-render(struct state *state)
+echo_esc(struct state *state)
+{
+ mvwprintw(state->echo_w, 0, 0, "ESC");
+ mvwprintw(state->echo_w, 0, 4, state->esc_input->str);
+}
+
+void
+render(struct state *state, char kkey)
{
int y, x, q, i;
static const char *str1 = "g: generic t: type e: element "
clear();
/* draw debug info */
- mvwprintw(stdscr, LINES - 3, 0, "mode: %d st: %d caret: %d",
- state->mode, state->st, state->caret);
+ 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);
/* draw workspace rule */
y = 0; x = 0;
state->err = 0;
}
else {
- switch (state->mode) {
- case uis_workspace:
+ switch (state->major_mode) {
+ case uimam_workspace:
if (state->st == st_thesis) {
if (state->status == 0)
mvwprintw(state->echo_w, 0, 0, str1);
else
mvwprintw(state->echo_w, 0, 0, str2);
}
- else if (state->escape) {
+ else if (state->minor_mode == uimim_backslash) {
mvwprintw(state->echo_w, 0, 0, "\\");
- wprintw(state->echo_w, state->escaped_input->str);
+ wprintw(state->echo_w, state->backslash_input->str);
}
break;
default:
}
/* draw window names */
- attron(COLOR_PAIR(PAIR_WB));
+ attron(COLOR_PAIR(PAIR_INVERSE));
move(q, 0);
printw("workspace%*s", COLS - 9, "");
- move(2 * q + 1, 0);
+ move(LINES - 2, 0);
printw("support%*s", COLS - 7, "");
- attroff(COLOR_PAIR(PAIR_WB));
+ attroff(COLOR_PAIR(PAIR_INVERSE));
refresh();
}
struct name *name;
if (key == '\\') {
- state->escape = TRUE;
+ state->minor_mode = uimim_backslash;
state->status = 0;
- g_string_erase(state->escaped_input, 0, -1);
+ state->backslash_input = g_string_erase(state->backslash_input, 0, -1);
}
else if (key > 32 && key < 127) {
- if (!state->escape)
+ if (state->minor_mode == uimim_default)
state->input = g_string_append_c(state->input, key);
else {
if ((key > 64 && key < 91) || (key > 96 && key < 123))
{
- state->escaped_input = g_string_append_c(state->escaped_input, key);
- l = g_hash_table_lookup(escaped_table, state->escaped_input->str);
+ state->backslash_input = g_string_append_c(state->backslash_input, key);
+ l = g_hash_table_lookup(escaped_table, state->backslash_input->str);
if (!l) {
- state->escape = FALSE;
+ state->minor_mode = uimim_default;
}
else if (!l->next) {
- state->escape = FALSE;
+ state->minor_mode = uimim_default;
state->input = g_string_append(state->input, l->data);
}
}
else
- state->escape = FALSE;
+ state->minor_mode = uimim_default;
}
}
if ((name = g_hash_table_lookup(state->decls, state->input->str))) {
- if (state->support)
- state->support->data = name->src;
- else
- state->support = g_slist_prepend(state->support, name->src);
- }
+ if (state->support)
+ state->support->data = name->src;
+ else
+ state->support = g_slist_prepend(state->support, name->src);
+ }
}
void
handle_slot_backspace(struct state *state)
{
- switch (state->st) {
- case st_a:
- state->st = st_thesis;
- state->judgment->kind = tk_unknown;
- break;
- case st_b:
- break;
- default:
- }
+ /* 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; */
+ /* state->st = prev_slot(state); */
}
void
if (*state->input->str == '\0')
handle_slot_backspace(state);
else
- g_string_erase(state->input, 0, -1);
+ state->input = g_string_erase(state->input, 0, -1);
}
void
handle_backspace(struct state *state)
{
- if (!state->escape)
+ if (state->minor_mode == uimim_default)
handle_input_backspace(state);
else
{
- if (*state->escaped_input->str == '\0')
- state->escape = FALSE;
+ if (*state->backslash_input->str == '\0')
+ state->minor_mode = uimim_default;
else
- g_string_erase(state->escaped_input, 0, -1);
+ state->backslash_input = g_string_erase(state->backslash_input, 0, -1);
}
}
-bool
-conclusion_p(struct rule *rule, struct judgment *judgment)
-{
- return judgment == rule->conclusion ? TRUE : FALSE;
-}
-
-int
-validate_generic_context(struct state *state, bool is_left)
+void
+handle_esc(struct state *state, wint_t key)
{
- struct name *name;
-
- if (*state->input->str == '\0')
- return 0;
- if (conclusion_p(state->rule, state->judgment)) {
- if (!(name = g_hash_table_lookup(state->gctxs, state->input->str)))
- return 3;
- if (is_left) {
- state->judgment->generic_l = create_wrap(FALSE, name);
- }
+ if (key == KEY_ESC) {
+ if (state->minor_mode = uimim_esc)
+ state->minor_mode = uimim_default;
else {
- if (state->judgment->generic_l &&
- name == state->judgment->generic_l->ptr)
- return 4;
- state->judgment->generic_r = create_wrap(FALSE, name);
+ state->esc_input = g_string_erase(state->esc_input, 0, -1);
+ state->minor_mode = uimim_esc;
+ }
+ }
+ else if (state->minor_mode == uimim_esc) {
+ if (key == KEY_RETURN) {
+ state->minor_mode = uimim_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;
+ else if (strcmp(state->esc_input->str, "h") == 0)
+ state->major_mode = uimam_help;
+ }
+ else if ((key > 64 && key < 91) || (key > 96 && key < 123)) {
+ state->esc_input = g_string_append_c(state->esc_input, key);
}
- g_string_erase(state->input, 0, -1);
- return 0;
}
- else
- return -1;
}
GSList *
-list_dependencies(GHashTable *vets)
+list_dependencies(GHashTable *vets, enum name_kind nk, enum scope s, void *addr)
{
GSList *l;
GHashTableIter iter;
gpointer key, value;
+ struct name *name;
l = NULL;
g_hash_table_iter_init(&iter, vets);
- while (g_hash_table_iter_next(&iter, &key, &value))
- l = g_slist_prepend(l, value); /* value = a name */
+ 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);
+ }
+ }
return l;
}
int
-validate_type_thesis(struct state *state)
+validate_generic_context(struct state *state, bool is_left)
{
+ enum name_kind nk;
struct name *name;
+ struct wrap *wrap;
+ if (*state->input->str == '\0')
+ return 0;
+ name = g_hash_table_lookup(state->gctxs, state->input->str);
+ nk = is_left ? nk_generic_context_left : nk_generic_context_right;
+ if (name) {
+ if (nk != name->kind)
+ return 4;
+ wrap = create_wrap(FALSE,
+ create_reference(name,
+ g_slist_copy_deep(name->dependencies,
+ copy_user_data,
+ NULL)));
+ if (is_left)
+ state->judgment->generic_l = wrap;
+ else
+ state->judgment->generic_r = wrap;
+ state->input = g_string_erase(state->input, 0, -1);
+ return 0;
+ }
+ else if (conclusion_p(state->rule, state->judgment))
+ return 3;
+ name = create_name(s_local,
+ nk,
+ NULL,
+ state->rule,
+ list_dependencies(state->vets, nk, s_local, NULL),
+ strdup(state->input->str));
+ wrap = create_wrap(TRUE, name);
+ if (is_left)
+ state->judgment->generic_l = wrap;
+ else
+ state->judgment->generic_r = wrap;
+ g_hash_table_insert(state->gctxs, name->str, name);
+ state->input = g_string_erase(state->input, 0, -1);
+ return 0;
+}
+
+int
+/* validate_vet_input(struct wrap **wrap, struct state *state, enum name_kind nk) */
+validate_vet_input(void *addr, struct state *state, enum name_kind nk)
+{
+ bool is_c;
+ enum thesis_kind tk;
+ 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 (conclusion_p(state->rule, state->judgment)) {
- if ((name = g_hash_table_lookup(state->decls, state->input->str)))
+ 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 = g_hash_table_lookup(state->vets, state->input->str))) {
- if (name->kind != nk_type)
- return 6;
+ 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)
+ 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 (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),
+ strdup(state->input->str));
+ g_hash_table_insert(state->vets, name->str, name);
+ }
+ state->input = g_string_erase(state->input, 0, -1);
+ *(struct wrap **)addr = create_wrap(TRUE, name);
+ return 0;
+}
- /* the name exists, is a type, and is local */
- state->judgment->a = create_wrap(FALSE, name);
- return -1; /* TODO: check dependencies */
- }
+int
+validate_replacement(struct state *state)
+{
+ bool is_c;
+ guint idx;
+ GSList *reps, *l;
+ struct name *dep, *name;
+ struct reference *ref;
+
+ if (*state->input->str == '\0')
+ return 1;
+ name = g_hash_table_lookup(state->decls, state->input->str);
+ if (!name)
+ name = g_hash_table_lookup(state->vets, 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;
+ l = g_slist_nth(ref->replacements, idx);
+ reps = g_slist_copy_deep(name->dependencies, copy_user_data, NULL);
+ l->data = create_reference(name, reps);
+
+ if (reps)
+ state->stack = g_slist_prepend(state->stack, l->data);
else {
- name = create_name(s_global, nk_type, NULL, state->rule,
- list_dependencies(state->vets),
- strdup(state->input->str));
- state->judgment->a = create_wrap(TRUE, name);
- g_string_erase(state->input, 0, -1);
- return 0;
+ l = l->next;
+ while (state->stack && !l) {
+ state->stack = state->stack->next;
+ if (state->stack)
+ l = g_slist_find(((struct reference *)state->stack->data)->replacements, NULL);
+ }
}
+ state->input = g_string_erase(state->input, 0, -1);
+ return 0;
}
- return -1;
+ return 3;
}
int
break;
default:
}
- g_string_erase(state->input, 0, -1);
+ state->input = g_string_erase(state->input, 0, -1);
state->rule = create_rule();
state->judgment = state->rule->conclusion;
+ clear_locals(state);
return 0;
}
+bool
+requires_replacements(struct wrap *addr)
+{
+ return addr && addr->is_origin == FALSE &&
+ ((struct reference *)addr->ptr)->replacements;
+}
+
+void
+handle_replacements(struct state *state, struct wrap *addr)
+{
+ state->replacing = TRUE;
+ state->stack = g_slist_prepend(state->stack, addr->ptr);
+ state->caret += 1;
+}
+
int
main()
{
+ bool c_p;
const char *k, *v;
char *str;
int i, j, q;
GHashTableIter iter;
gpointer hkey, hvalue;
wint_t key;
+ struct wrap **addr;
+ void *naddr;
setlocale(LC_ALL, "");
initscr();
ESCDELAY = 0;
intrflush(stdscr, FALSE);
keypad(stdscr, TRUE);
- init_pair(PAIR_BW, COLOR_BLACK, COLOR_WHITE);
- init_pair(PAIR_WB, COLOR_WHITE, COLOR_BLACK);
- init_pair(PAIR_HL, COLOR_CYAN, COLOR_WHITE);
- init_pair(PAIR_SUCCESS, COLOR_GREEN, COLOR_WHITE);
- init_pair(PAIR_ERROR, COLOR_RED, COLOR_WHITE);
- bkgd(COLOR_PAIR(PAIR_BW));
+ init_pair(PAIR_NORMAL, COLOR_WHITE, COLOR_BLACK);
+ init_pair(PAIR_INVERSE, COLOR_BLACK, COLOR_WHITE);
+ init_pair(PAIR_HL, COLOR_CYAN, COLOR_BLACK);
+ init_pair(PAIR_SUCCESS, COLOR_GREEN, COLOR_BLACK);
+ init_pair(PAIR_ERROR, COLOR_RED, COLOR_BLACK);
+ bkgd(COLOR_PAIR(PAIR_NORMAL));
q = (LINES - 3) / 2;
state.running = TRUE;
- state.mode = uis_splash;
+ state.major_mode = uimam_splash;
+ state.minor_mode = uimim_default;
state.rule = create_rule();
state.judgment = state.rule->conclusion;
state.dependency = NULL;
state.caret = 0;
state.st = st_rule_dots;
state.input = g_string_new(NULL);
- state.escaped_input = g_string_new(NULL);
- state.escape = FALSE;
+ state.backslash_input = g_string_new(NULL);
+ state.esc_input = g_string_new(NULL);
state.err = 0;
+ state.replacing = FALSE;
+ state.stack = NULL;
/* populate escaped strings table */
/* NOTE: `g_hash_table_insert' deletes keys and values if they already exist.
}
}
- if (state.mode == uis_splash) {
- render_splash();
- getch();
- state.mode = uis_workspace;
- render(&state);
- }
+ render_splash();
+ get_wch(&key);
+ state.major_mode = uimam_workspace;
+ render(&state, key);
while(state.running) {
get_wch(&key);
- if (key == KEY_ESC) {
- state.running = FALSE;
- break;
- }
- switch(state.mode) {
- case uis_workspace:
- switch (state.st) {
- case st_rule_dots:
+ switch(state.major_mode) {
+ case uimam_splash:
+ render_splash();
+ /* no break (intentional) */
+ case uimam_help:
+ render_help();
+ /* no break (intentional) */
+ case uimam_workspace:
+ if (key == KEY_ESC)
+ state.running = FALSE;
+ else if (state.replacing) {
if (key == KEY_TAB) {
- state.caret += 1;
- state.st = st_ctx_l;
- 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;
- }
- break;
- case st_rule_name:
- if (key == KEY_TAB) {
- if (!(state.err = validate_rule_name(&state))) {
- /* reset the workspace to initial state */
- state.caret = 0;
- state.st = st_rule_dots;
- g_slist_free(g_steal_pointer(&state.support));
+ if (!(state.err = validate_replacement(&state))) {
+ if (state.stack)
+ state.caret += 1;
+ else { /* we are done replacing */
+ state.replacing = FALSE;
+ next_slot(&state);
+ }
}
}
else if (key == KEY_BACKSPACE)
handle_backspace(&state);
else
handle_input(&state, key);
- break;
- case st_ctx_l:
- if (key == KEY_TAB) {
- if (!(state.err = validate_generic_context(&state, TRUE))) {
- state.caret += 1;
- state.st = st_ctx_dots;
+ }
+ else {
+ switch (state.st) {
+ case st_rule_dots:
+ if (key == KEY_TAB) {
+ next_slot(&state);
+ state.judgment = state.rule->conclusion;
}
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case st_ctx_v:
- break;
- case st_ctx_t:
- break;
- case st_ctx_dots:
- if (key == KEY_TAB) {
- state.caret += 1;
- state.st = st_ctx_r;
- }
- else if (key == KEY_RETURN) {
- }
- break;
- case st_ctx_r:
- if (key == KEY_TAB) {
- if (!(state.err = validate_generic_context(&state, FALSE))) {
- state.caret += 1;
- state.st = st_thesis;
- state.status = 0;
+ 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;
}
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case st_thesis:
- j_p = state.judgment;
- if (state.status == 0) {
- switch (key) {
- case 'g':
- state.st = st_a;
- j_p->kind = tk_generic;
- break;
- case 't':
- state.st = st_a;
- j_p->kind = tk_type;
- break;
- case 'e':
- state.st = st_a;
- j_p->kind = tk_element;
- break;
- case '=':
- state.status = 1;
- break;
- default:
+ else if (key == KEY_BACKSPACE) {
+ if (state.rule->hypotheses) {
+ state.caret -= 1;
+ state.st = prev_slot(&state);
+ state.judgment = g_slist_last(state.rule->hypotheses)->data;
+ }
}
- }
- else if (state.status == 1) {
- switch (key) {
- case 't':
- state.st = st_a;
- j_p->kind = tk_type_equal;
- break;
- case 'e':
- state.st = st_a;
- j_p->kind = tk_element_equal;
- break;
- default:
- state.status = 0;
+ break;
+ case st_ctx_l:
+ if (key == KEY_TAB) {
+ if (!(state.err = validate_generic_context(&state, TRUE))) {
+ addr = &state.judgment->generic_l;
+ if (requires_replacements(*addr))
+ handle_replacements(&state, *addr);
+ else
+ next_slot(&state);
+ }
}
- }
- break;
- case st_a:
- if (key == KEY_TAB) {
- switch (state.judgment->kind) {
- case tk_type:
- if (!(state.err = validate_type_thesis(&state))) {
- state.caret += 1;
- if (conclusion_p(state.rule, state.judgment))
- state.st = st_rule_name;
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_ctx_v:
+ if (key == KEY_TAB) {
+ naddr = &g_slist_last(state.judgment->vdecls)->data;
+ if (!(state.err = validate_vet_input(naddr, &state, nk_variable)))
+ next_slot(&state);
+ }
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_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)))
+ next_slot(&state);
+ }
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_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;
+ }
+ break;
+ case st_ctx_r:
+ if (key == KEY_TAB) {
+ if (!(state.err = validate_generic_context(&state, FALSE))) {
+ addr = &state.judgment->generic_r;
+ if (requires_replacements(*addr))
+ handle_replacements(&state, *addr);
+ else {
+ next_slot(&state);
+ state.status = 0;
+ }
+ }
+ }
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_thesis:
+ j_p = state.judgment;
+ if (state.status == 0) {
+ switch (key) {
+ case 'g':
+ j_p->kind = tk_generic;
+ next_slot(&state);
+ break;
+ case 't':
+ j_p->kind = tk_type;
+ next_slot(&state);
+ break;
+ case 'e':
+ j_p->kind = tk_element;
+ next_slot(&state);
+ break;
+ case '=':
+ state.status = 1;
+ break;
+ default:
+ }
+ }
+ else if (state.status == 1) {
+ switch (key) {
+ case 't':
+ j_p->kind = tk_type_equal;
+ next_slot(&state);
+ break;
+ case 'e':
+ j_p->kind = tk_element_equal;
+ next_slot(&state);
+ break;
+ default:
+ state.status = 0;
+ }
+ }
+ break;
+ case st_generic_thesis:
+ state.err = -1;
+ break;
+ case st_type_thesis:
+ if (key == KEY_TAB) {
+ addr = &state.judgment->a;
+ if (!(state.err = validate_vet_input(addr, &state, nk_type))) {
+ if (requires_replacements(*addr))
+ handle_replacements(&state, *addr);
else
- state.st = st_rule_dots;
+ next_slot(&state);
}
- break;
- default:
- state.err = -1;
}
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case st_b:
- if (key == KEY_TAB) {
- state.caret += 1;
- if (j_p->kind == tk_element_equal) {
- state.st = st_c;
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_element_thesis_element:
+ if (key == KEY_TAB) {
+ addr = &state.judgment->a;
+ if (!(state.err = validate_vet_input(addr, &state, nk_element)))
+ next_slot(&state);
}
- else {
- state.st = st_rule_name;
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_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 (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)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_type_equal_thesis_type_1:
+ if (key == KEY_TAB) {
+ addr = &state.judgment->a;
+ if (!(state.err = validate_vet_input(addr, &state, nk_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)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_type_equal_thesis_type_2:
+ if (key == KEY_TAB) {
+ addr = &state.judgment->b;
+ if (!(state.err = validate_vet_input(addr, &state, nk_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)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_element_equal_thesis_element_1:
+ if (key == KEY_TAB) {
+ addr = &state.judgment->a;
+ if (!(state.err = validate_vet_input(addr, &state, nk_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)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_element_equal_thesis_element_2:
+ if (key == KEY_TAB) {
+ addr = &state.judgment->b;
+ if (!(state.err = validate_vet_input(addr, &state, nk_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)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_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))) {
+ *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 if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
+ case st_rule_name:
+ if (key == KEY_TAB) {
+ if (!(state.err = validate_rule_name(&state))) {
+ /* reset the workspace to initial state */
+ next_slot(&state);
+ g_slist_free(g_steal_pointer(&state.support));
+ }
+ }
+ else if (key == KEY_BACKSPACE)
+ handle_backspace(&state);
+ else
+ handle_input(&state, key);
+ break;
}
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- case st_c:
- if (key == KEY_TAB) {
- state.caret += 1;
- state.st = st_rule_name;
- }
- else if (key == KEY_BACKSPACE)
- handle_backspace(&state);
- else
- handle_input(&state, key);
- break;
- default:
}
+ render(&state, key);
break;
default:
}
- render(&state);
}
delwin(state.workspace_w);
delwin(state.support_w);
g_hash_table_destroy(state.vets);
g_slist_free(state.support);
g_string_free(state.input, TRUE);
- g_string_free(state.escaped_input, TRUE);
+ g_string_free(state.backslash_input, TRUE);
+ g_string_free(state.esc_input, TRUE);
return 0;
}
projects / vouivre.git / commitdiff