Implement generic theses

diff --git a/src/v.c b/src/v.c
index c76e25200a0215e6ab4894f598e0fdea6871d458..17aa16c3e0f1715dd9772c8fc9faaf45d94ea26c 100644 (file)
--- a/src/v.c
+++ b/src/v.c
@@ -1340,7 +1340,42 @@ validate_generic_context(struct state *state, bool is_left)
 }
 
 int
-/* validate_vet_input(struct wrap **wrap, struct state *state, enum name_kind nk) */
+validate_generic_thesis(struct state *state)
+{
+  enum name_kind nk;
+  struct name *name;
+  struct wrap *wrap;
+
+  if (*state->input->str == '\0')
+    return 1;
+  name = g_hash_table_lookup(state->gtheses, state->input->str);
+  if (name) {
+    wrap = create_wrap(FALSE,
+                      create_reference(name,
+                                       g_slist_copy_deep(name->dependencies,
+                                                         copy_user_data,
+                                                         NULL)));
+    state->judgment->a = 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_generic_thesis,
+                    NULL,
+                    state->rule,
+                    list_dependencies(state->vets, nk_generic_thesis,
+                                      s_local, NULL),
+                    strdup(state->input->str));
+  wrap = create_wrap(TRUE, name);
+  state->judgment->a = wrap;
+  g_hash_table_insert(state->gtheses, name->str, name);
+  state->input = g_string_erase(state->input, 0, -1);
+  return 0;
+}
+
+int
 validate_vet_input(void *addr, struct state *state, enum name_kind nk)
 {
   bool is_c;
@@ -1423,10 +1458,14 @@ validate_replacement(struct state *state)
     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
+    */
+
+
     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 {
@@ -1716,7 +1755,19 @@ main()
          }
          break;
        case st_generic_thesis:
-         state.err = -1;
+         if (key == KEY_TAB) {
+           addr = &state.judgment->a;
+           if (!(state.err = validate_generic_thesis(&state))) {
+             if (requires_replacements(*addr))
+               handle_replacements(&state, *addr);
+             else
+               next_slot(&state);
+           }
+         }
+         else if (key == KEY_BACKSPACE)
+           handle_backspace(&state);
+         else
+           handle_input(&state, key);
          break;
        case st_type_thesis:
          if (key == KEY_TAB) {