From: admin <admin@vouivredigital.com>
Date: Mon, 4 Nov 2024 04:05:12 +0000 (-0500)
Subject: Draw rules in order entered
X-Git-Url: https://git.vouivredigital.com/?a=commitdiff_plain;h=26be31e3ad0823e7f6aed9d9ea9f76ba5673fc11;p=vouivre.git

Draw rules in order entered
---

diff --git a/help.txt b/help.txt
index 44691b1..d8d4001 100644
--- a/help.txt
+++ b/help.txt
@@ -1,13 +1,41 @@
-Slots
-...    zero or more of something (variable declarations or hypotheses)
-█      empty input
-█?     optional input
-
 Global Commands
+
 ESC q        quit Vouivre
 ESC splash   go to splash screen
 ESC h        go to (this) help screen
 
-Workspace Commands
+Slots
+
+...          zero or more hypotheses or variable declarations
+█            empty input
+█?           optional input
+
+Workspace Keys
+
 TAB          move to next slot
 RET          add an item when on a '...' slot
+\            enter a special character
+
+Special Characters
+
+\to       →    \Xi       Ξ    \BB       𝔹    \VV       𝕍    \pp       𝕡
+\alpha    α    \xi       ξ    \CC       ℂ    \WW       𝕎    \qq       𝕢
+\beta     β    \Omicron  Ο    \DD       𝔻    \XX       𝕏    \rr       𝕣
+\Gamma    Γ    \omicron  ο    \EE       𝔼    \YY       𝕐    \ss       𝕤
+\gamma    γ    \Pi       Π    \FF       𝔽    \ZZ       ℤ    \tt       𝕥
+\Delta    Δ    \pi       π    \GG       𝔾    \aa       𝕒    \uu       𝕦
+\delta    δ    \Rho      Ρ    \HH       ℍ    \bb       𝕓    \vv       𝕧
+\epsilon  ε    \rho      ρ    \II       𝕀    \cc       𝕔    \ww       𝕨
+\Zeta     Ζ    \Sigma    Σ    \JJ       𝕁    \dd       𝕕    \xx       𝕩
+\zeta     ζ    \sigma    σ    \KK       𝕂    \ee       𝕖    \yy       𝕪
+\eta      η    \upsilon  υ    \LL       𝕃    \ff       𝕗    \zz       𝕫
+\Theta    Θ    \Phi      Φ    \MM       𝕄    \gg       𝕘    \00       𝟘
+\theta    θ    \phi      φ    \NN       ℕ    \hh       𝕙    \11       𝟙
+\Iota     Ι    \Chi      Χ    \OO       𝕆    \ii       𝕚    \22       𝟚
+\iota     ι    \chi      χ    \PP       ℙ    \jj       𝕛    \33       𝟛
+\kappa    κ    \Psi      Ψ    \QQ       ℚ    \kk       𝕜    \44       𝟜
+\Lambda   Λ    \psi      ψ    \RR       ℝ    \ll       𝕝    \55       𝟝
+\lambda   λ    \Omega    Ω    \SS       𝕊    \mm       𝕞    \66       𝟞
+\mu       μ    \omega    ω    \TT       𝕋    \nn       𝕟    \77       𝟟
+\nu       ν    \AA       𝔸    \UU       𝕌    \oo       𝕠    \88       𝟠
+							    \99       𝟡
diff --git a/src/ui.c b/src/ui.c
index 8f14e68..171a312 100644
--- a/src/ui.c
+++ b/src/ui.c
@@ -792,8 +792,13 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset,
     n += 1;
     l = l->next;
   }
-  if (workspace_mode && (offset >= caret_offset))
+  if (workspace_mode && (offset >= caret_offset)) {
     is_dot = TRUE;
+    draw_slot(w, y, x, &offset, caret_offset, TRUE,
+	      "...", FALSE);
+  }
+  else
+    offset += 1;
   draw_judgment(w, y, &c, &offset, caret_offset, TRUE, inputstr,
 		rule->conclusion, workspace_mode);
   draw_slot(w, y, &r, &offset, caret_offset, TRUE,
@@ -847,5 +852,6 @@ draw_rule(WINDOW *w, int *y, int *x, int caret_offset,
     draw_slot(w, y, x, &offset, caret_offset, virtual,
 	      offset == caret_offset ? inputstr : rule->name, FALSE);
   }
-  *y = row + (stack_p ? n + (is_dot ? 1 : 0) + 2 : 3); *x = col + (lw + c) / 2;
+  *y = (stack_p ? n + (is_dot ? 1 : 0) + 2 : 3);
+  *x = lw + r + 1;
 }
diff --git a/src/v.c b/src/v.c
index 3b74d2c..7872457 100644
--- a/src/v.c
+++ b/src/v.c
@@ -43,14 +43,15 @@ struct state
   enum ui_input_mode input_mode;
   struct rule *rule;
   struct point *slot;
-  WINDOW *workspace_w;
-  WINDOW *support_w;
-  WINDOW *echo_w;
+  WINDOW *workspace;
+  WINDOW *status_bar;
+  WINDOW *echo_area;
   GHashTable *rules;		/* str -> rule */
   GHashTable *globals;		/* str -> name */
   GHashTable *temporaries;	/* str -> name */
   GHashTable *gctxs;		/* str -> name */
   GHashTable *gtheses;		/* str -> name */
+  GSList *ordered_rules;	/* rule names */
   GSList *support;		/* rules */
   GString *input;
   GString *special;
@@ -188,6 +189,13 @@ insert_name(GHashTable *temporaries, struct name *name)
     g_hash_table_insert(temporaries, name->str, name);
 }
 
+void
+insert_rule(struct state *state, struct rule *rule)
+{
+  g_hash_table_insert(state->rules, rule->name, rule);
+  state->ordered_rules = g_slist_prepend(state->ordered_rules, rule->name);
+}
+
 /*
  * Remove entries with contextual scope.  This is the end of the line for
  * variables.
@@ -255,7 +263,7 @@ render_splash(struct state *state)
 	     strs[i]);
   }
   if (state->input_mode == ui_input_mode_command)
-    echo_esc(state->echo_w, state->command->str);
+    echo_esc(state->echo_area, state->command->str);
   refresh();
 }
 
@@ -272,7 +280,7 @@ render_help(struct state *state)
     addch(c);
   fclose(fd);
   if (state->input_mode == ui_input_mode_command)
-    echo_esc(state->echo_w, state->command->str);
+    echo_esc(state->echo_area, state->command->str);
   refresh();
 }
 
@@ -318,118 +326,154 @@ echo_status(WINDOW *w, int status)
   wattroff(w, COLOR_PAIR(pair));
 }
 
+int
+status_bar_str(char *buf, size_t len,
+	       enum ui_major_mode major_mode, enum ui_input_mode input_mode,
+	       struct point *p, char *input, char key, GHashTable *temporaries)
+{
+  int n = 0;
+  GSList *l;
+  GList *head, *l1;
+
+  n += snprintf(buf, len, " %d:%d    (%d,%d,%d,%d,[",
+		major_mode, input_mode,
+		p->is_conclusion,
+		p->st,
+		p->judgment_idx,
+		p->vdecl_idx);
+  l = p->stack;
+  if (!l)
+    n += snprintf(buf + n, len - n, "NULL])");
+  while (l) {
+    n += snprintf(buf + n, len - n, "%d", GPOINTER_TO_INT(l->data));
+    if (l->next)
+      n += snprintf(buf + n, len - n, ",");
+    else
+      n += snprintf(buf + n, len - n, "])");
+    l = l->next;
+  }
+  n += snprintf(buf + n, len - n, "    \"%s\"", input);
+  if (key > 31 && key < 127)
+    n += snprintf(buf + n, len - n, "    '%c'", key);
+  else if (key == '\t')
+    n += snprintf(buf + n, len - n, "    'TAB'");
+  else if (key == '\n')
+    n += snprintf(buf + n, len - n, "    'RET'");
+  else if (key == 27)
+    n += snprintf(buf + n, len - n, "    'ESC'");
+  else
+    n += snprintf(buf + n, len - n, "    UNKNOWN_KEY");
+  head = g_hash_table_get_keys(temporaries);
+  if (head)
+    n += snprintf(buf + n, len - n, "    ");
+  l1 = head;
+  while (l1) {
+    n += snprintf(buf + n, len - n, "%s", l1->data);
+    if (l1->next)
+      n += snprintf(buf + n, len - n, " ");
+    l1 = l1->next;
+  }
+  n += snprintf(buf + n, len - n, " ");
+  g_list_free(head);
+  return n;
+}
+
 void
 render(struct state *state, char kkey)
 {
-  int y, x, q, i, caret_offset;
+  int caret_offset;
+  int y, x, h, w, h1, w1, yoff, xoff, maxw, maxn, n;
   static const char *str1 = "g: generic  t: type  e: element  "
     "=t: judgmentally equal types  =e: judgmentally equal elements";
   static const char *str2 = "=t: judgmentally equal types  "
     "=e: judgmentally equal elements";
-  GHashTableIter iter;
-  /* GSList *l, *deps; */
-  GList *head, *l1;
+  char buf[COLS];
   GSList *l;
-  gpointer key, value;
   struct rule *rule;
   struct point *p;
 
-  q = (LINES - 3) / 2;
   clear();
 
-  /* draw debug info */
-  i = 0;
-  head = g_hash_table_get_keys(state->temporaries);
-  l1 = head;
-  while (l1) {
-    mvwprintw(stdscr, LINES - 4, i, "%s", l1->data);
-    i += strlen(l1->data) + 1;
-    l1 = l1->next;
-  }
-  g_list_free(head);
-  mvwprintw(stdscr, LINES - 3, 0,
-	    "major_mode: %d  input_mode: %d  is_conclusion: %d  "
-	    "st: %d  j_idx: %d  v_idx: %d  ",
-	    state->major_mode, state->input_mode,
-	    state->slot->is_conclusion,
-	    state->slot->st,
-	    state->slot->judgment_idx,
-	    state->slot->vdecl_idx);
-  wprintw(stdscr, "stack: ");
-  l = state->slot->stack;
-  if (!l)
-    wprintw(stdscr, "NULL  ");
-  while (l) {
-    wprintw(stdscr, "%d ", GPOINTER_TO_INT(l->data));
-    l = l->next;
-  }
-  wprintw(stdscr, " inputstr: %s  key: %d",
-	  state->input->str,
-	  kkey);
-
   /* draw workspace rule */
-  y = 0; x = 0;
   p = create_point(FALSE,
 		   state->rule->hypotheses ? slot_type_ctx_l :
 		   slot_type_rule_dots, 0, 0, NULL);
   caret_offset = point_distance(state->rule, p,	state->slot);
   free_point(p);
-  draw_rule(state->workspace_w, &y, &x, caret_offset,
+  h = 0; w = 0;
+  draw_rule(state->workspace, &h, &w, caret_offset,
+	    TRUE, state->input->str, state->rule, TRUE);
+  y = (LINES - 2 - h) / 2; x = (COLS - w) / 2;
+  draw_rule(state->workspace, &y, &x, caret_offset,
 	    FALSE, state->input->str, state->rule, TRUE);
 
   /* draw existing rules */
-  i = 0;
-  g_hash_table_iter_init(&iter, state->rules);
-  while (g_hash_table_iter_next(&iter, &key, &value))
+  yoff = 0;
+  maxw = 0; maxn = 0;
+  l = state->ordered_rules;
+  while (l)
+    {
+      rule = g_hash_table_lookup(state->rules, l->data);
+      h1 = 0; w1 = 0;
+      draw_rule(state->workspace, &h1, &w1, -1,
+		TRUE, NULL, rule, FALSE);
+      if (yoff + h1 + 1 > LINES - 2)
+	break;
+      if (w1 > maxw)
+	maxw = w1;
+      if (maxn < (n = mbstowcs(NULL, rule->name, 0)))
+	maxn = n;
+      yoff += h1 + 1;
+      l = l->next;
+    }
+  yoff = 0;
+  l = state->ordered_rules;
+  while (l)
     {
-      rule = value;
-      y = i; x = 0;
-      draw_rule(state->support_w, &y, &x, -1,
+      rule = g_hash_table_lookup(state->rules, l->data);
+      h1 = 0; w1 = 0;
+      draw_rule(state->workspace, &h1, &w1, -1,
+		TRUE, NULL, rule, FALSE);
+      n = mbstowcs(NULL, rule->name, 0);
+      if (yoff + h1 + 1 > (LINES - 2 - h) / 2 &&
+	  yoff < (LINES - 2 + h) / 2 &&
+	  COLS - 1 - maxn - 1 - (w1 - n - 1) < (COLS + w) / 2)
+	yoff = (LINES - 2 + h) / 2 + 1;
+      if (yoff + h1 + 1 > LINES - 2)
+	break;
+      y = yoff; x = COLS - 1 - (maxn - n) - w1;
+      draw_rule(state->workspace, &y, &x, -1,
 		FALSE, NULL, rule, FALSE);
-      i = y + 1;
+      yoff += h1 + 1;
+      l = l->next;
     }
 
-  /* /\* draw support rules *\/ */
-  /* i = 0; */
-  /* l = state->support; */
-  /* while (l) */
-  /*   { */
-  /*     rule = l->data; */
-  /*     y = i; x = 0; */
-  /*     draw_rule(state->support_w, &y, &x, FALSE, FALSE, -1, NULL, rule); */
-  /*     i = y + 2; */
-  /*     l = l->next; */
-  /*   } */
-
-  /* draw window names and boundaries */
-  attron(COLOR_PAIR(PAIR_INVERSE));
-  move(q, 0);
-  printw("workspace%*s", COLS - NB_COLUMNS - 1 - 9, "");
-  move(LINES - 2, 0);
-  printw("support%*s", COLS - NB_COLUMNS - 1 - 7, "");
-  move(LINES - 2, COLS - NB_COLUMNS);
-  printw("rules%*s", NB_COLUMNS - 5, "");
-  attroff(COLOR_PAIR(PAIR_INVERSE));
-  for (i = 0 ; i < LINES - 1 ; i++)
-    mvprintw(i, COLS - NB_COLUMNS - 1, "█");
+  /* status bar */
+  n = status_bar_str(buf, sizeof(buf),
+			  state->major_mode, state->input_mode,
+			  state->slot, state->input->str, kkey,
+			  state->temporaries);
+  wattron(state->status_bar, COLOR_PAIR(PAIR_INVERSE));
+  mvwprintw(state->status_bar, 0, (COLS - n) / 2, buf);
+  wattroff(state->status_bar, COLOR_PAIR(PAIR_INVERSE));
 
-  /* draw echo area */
+  /* echo area */
   if (state->input_mode == ui_input_mode_command)
-    echo_esc(state->echo_w, state->command->str);
+    echo_esc(state->echo_area, state->command->str);
   else if (state->err) {
-    echo_status(state->echo_w, state->err);
+    echo_status(state->echo_area, state->err);
     state->err = 0;
   }
   else {
     if (state->slot->st == slot_type_thesis) {
       if (state->status == 0)
-	mvwprintw(state->echo_w, 0, 0, str1);
+	mvwprintw(state->echo_area, 0, 0, str1);
       else
-	mvwprintw(state->echo_w, 0, 0, str2);
+	mvwprintw(state->echo_area, 0, 0, str2);
     }
     else if (state->input_mode == ui_input_mode_special_characters) {
-      mvwprintw(state->echo_w, 0, 0, "\\");
-      wprintw(state->echo_w, state->special->str);
+      mvwprintw(state->echo_area, 0, 0, "\\");
+      wprintw(state->echo_area, state->special->str);
     }
   }
 
@@ -771,7 +815,7 @@ validate_rule_name(struct state *state)
   if (g_hash_table_lookup(state->rules, state->input->str))
     return 2;
   rule->name = strdup(state->input->str);
-  g_hash_table_insert(state->rules, state->rule->name, rule);
+  insert_rule(state, rule);
   c = rule->conclusion;
   switch (c->kind) {
   case thesis_kind_type:
@@ -1055,6 +1099,9 @@ main()
   gpointer hkey, hvalue;
   struct state state;
 
+  int n = 0;
+  char cmd[100];
+
   setlocale(LC_ALL, "");
   initscr();
   start_color();
@@ -1076,9 +1123,9 @@ main()
   state.input_mode = ui_input_mode_default;
   state.rule = create_rule();
   state.slot = create_point(FALSE, slot_type_rule_dots, 0, 0, NULL);
-  state.workspace_w = subwin(stdscr, q, COLS - NB_COLUMNS - 1, 0, 0);
-  state.support_w = subwin(stdscr, LINES - 1, NB_COLUMNS, 0, COLS - NB_COLUMNS);
-  state.echo_w = subwin(stdscr, 1, COLS, LINES - 1, 0);
+  state.workspace = subwin(stdscr , LINES - 2, COLS, 0        , 0);
+  state.status_bar = subwin(stdscr, 1        , COLS, LINES - 2, 0);
+  state.echo_area = subwin(stdscr , 1        , COLS, LINES - 1, 0);
   state.rules = g_hash_table_new_full(g_str_hash, g_str_equal,
 				      NULL, (GDestroyNotify)free_rule);
   state.globals = g_hash_table_new_full(g_str_hash, g_str_equal,
@@ -1086,9 +1133,10 @@ main()
   str = strdup("Small");
   small = create_name(scope_global, name_kind_vet, NULL, NULL, NULL, str);
   g_hash_table_insert(state.globals, str, small);
+  state.temporaries = 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.temporaries = g_hash_table_new(g_str_hash, g_str_equal);
+  state.ordered_rules = NULL;
   state.support = NULL;
   state.input = g_string_new(NULL);
   state.special = g_string_new(NULL);
@@ -1147,9 +1195,9 @@ main()
     default:
     }
   }
-  delwin(state.workspace_w);
-  delwin(state.support_w);
-  delwin(state.echo_w);
+  delwin(state.workspace);
+  delwin(state.status_bar);
+  delwin(state.echo_area);
   endwin();
   g_hash_table_iter_init(&iter, special_character_map);
   while (g_hash_table_iter_next(&iter, &hkey, &hvalue))
@@ -1162,6 +1210,7 @@ main()
   g_hash_table_destroy(state.gctxs);
   g_hash_table_destroy(state.gtheses);
   g_hash_table_destroy(state.temporaries);
+  g_slist_free(state.ordered_rules);
   g_slist_free(state.support);
   g_string_free(state.input, TRUE);
   g_string_free(state.special, TRUE);