Draw hypotheses

diff --git a/src/v.c b/src/v.c
index 98e41304386836367e42f1cc2cc3bfc617ea35bf..99b49c0fc2a515598c90d6bb77c990daf5e97609 100644 (file)
--- a/src/v.c
+++ b/src/v.c
@@ -301,6 +301,22 @@ create_name(enum scope scope, enum name_kind kind, struct wrap *type,
   return name;
 }
 
+struct judgment *
+create_judgment()
+{
+  struct judgment *j;
+
+  j = malloc(sizeof(struct judgment));
+  j->kind = tk_unknown;
+  j->generic_l = NULL;
+  j->generic_r = NULL;
+  j->a = NULL;
+  j->b = NULL;
+  j->vdecls = NULL;
+  return j;
+}
+
+
 struct rule *
 create_rule()
 {
@@ -309,13 +325,7 @@ create_rule()
   rule = malloc(sizeof(struct rule));
   rule->name = NULL;
   rule->hypotheses = NULL;
-  rule->conclusion = malloc(sizeof(struct judgment));
-  rule->conclusion->kind = tk_unknown;
-  rule->conclusion->generic_l = NULL;
-  rule->conclusion->generic_r = NULL;
-  rule->conclusion->a = NULL;
-  rule->conclusion->b = NULL;
-  rule->conclusion->vdecls = NULL;
+  rule->conclusion = create_judgment();
   return rule;
 }
 
@@ -474,7 +484,7 @@ set_ctp_and_pair(enum caret_to_point *ctp, int *pair, int caret, int point)
 }
 
 void
-draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workplace_mode,
+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;
@@ -490,7 +500,7 @@ draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workplace_mode,
   prev_not_displayed = FALSE;
   if (judgment->generic_l)
     draw_wrap(w, y, x, v, TRUE, pair, judgment->generic_l);
-  else if (workplace_mode) {
+  else if (workspace_mode) {
     if (ctp == ctp_on)
       draw_slot(w, y, x, v, FALSE, pair, inputstr);
     else if (ctp == ctp_before)
@@ -524,7 +534,7 @@ draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workplace_mode,
 
   /* ctx_dots */
   set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
-  if (workplace_mode && (ctp == ctp_before || ctp == ctp_on)) {
+  if (workspace_mode && (ctp == ctp_before || ctp == ctp_on)) {
     if (!prev_not_displayed)
       draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
     draw_slot(w, y, x, v, FALSE, pair, "...");
@@ -538,7 +548,7 @@ draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workplace_mode,
       draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
     draw_wrap(w, y, x, v, TRUE, pair, judgment->generic_r);
   }
-  else if (workplace_mode) {
+  else if (workspace_mode) {
     if (ctp == ctp_on) {
       if (!prev_not_displayed)
        draw_slot(w, y, x, v, FALSE, PAIR_BW, ", ");
@@ -628,32 +638,90 @@ void
 draw_rule(WINDOW *w, int *y, int *x, bool virtual, bool workspace_mode,
          int caret, char *inputstr, struct rule *rule)
 {
-  int c, r, lw, row = *y, col = *x;
-  int point, pair;
+  bool stack_p, is_dot;
+  int c, m, n, r, lw, s, ow, row, col;
+  int point, pair, spaces;
   enum caret_to_point ctp;
+  GSList *l;
 
+  c = 0;
+  m = 0;
+  n = 0;
+  r = 0;
+  s = 0;
+  lw = 0;
+  ow = 0;
+  row = *y;
+  col = *x;
   point = 0;
-  *y = 0; c = 0; r = 0;
+  is_dot = FALSE;
+
+  l = rule->hypotheses;
+  while (l) {
+    *y = 0; *x = 0;
+    draw_judgment(w, y, x, TRUE, workspace_mode,
+                 caret, &point, inputstr, l->data);
+    s += *x;
+    m = m > *x ? m : *x;
+    n += 1;
+    l = l->next;
+  }
+  set_ctp_and_pair(&ctp, &pair, caret, point++);
+  if (workspace_mode && (ctp <= ctp_on))
+    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);
 
-  lw = c;
+  /* If the width of the line (calculated as the hypotheses + "..." + spacing
+     between them + space + rule name) is greater than the allowed number of
+     columns, then we must stack the hypotheses. */
+  ow = s + (is_dot ? 3 : 0) +
+    HYPOTHESES_SPACING * (n + is_dot ? n + is_dot + 1 : 0);
+
+  stack_p = (n > 1) && (ow + 1 + r >= NB_COLUMNS);
+  ow = stack_p ? m : ow;
+  lw = c > ow ? c : ow;
   if (!virtual) {
-    *y = row + 1; *x = col;
+    *y = row;
+    *x = col;
+    if (n == 0)
+      spaces = (lw - (is_dot ? 3 : 0)) / 2;
+    else
+      spaces = (lw - s - (is_dot ? 3 : 0)) / (n + (is_dot ? 2 : 1));
+    if (!stack_p)
+      *x += spaces;
+    point = 0;
+    l = rule->hypotheses;
+    while (l) {
+      draw_judgment(w, y, x, virtual, workspace_mode,
+                   caret, &point, inputstr, l->data);
+      if (!stack_p)
+       *x += spaces;
+      else {
+       *y += 1;
+       *x = col;
+      }
+      l = l->next;
+    }
+    set_ctp_and_pair(&ctp, &pair, caret, point++);
+    if (workspace_mode && (ctp <= ctp_on))
+      draw_slot(w, y, x, virtual, FALSE, pair, "...");
+    *y += 1; *x = col;
     wmove(w, *y, *x);
     for (*x = col ; *x < col + lw ; *x = *x + 1)
       wprintw(w, "=");
-    point = 0;
-    *y = row + 2; *x = col;
+    *y += 1; *x = col + (lw - c) / 2;
+    set_ctp_and_pair(&ctp, &pair, caret, point);
     draw_judgment(w, y, x, virtual, workspace_mode,
                  caret, &point, inputstr, rule->conclusion);
+    *y -= 1; *x = col + lw + 1;
     set_ctp_and_pair(&ctp, &pair, caret, point++);
-    *y = row + 1; *x = col + lw + 1;
     draw_slot(w, y, x, virtual, FALSE, pair, ctp == ctp_on ? inputstr : rule->name);
   }
-  *y = row + 2; *x = lw;
+  *y = row + (stack_p ? n + (is_dot ? 1 : 0) + 2 : 3); *x = col + (lw + c) / 2;
 }
 
 void
@@ -1013,7 +1081,7 @@ main()
   state.vets = g_hash_table_new(g_str_hash, g_str_equal);
   state.support = NULL;
   state.caret = 0;
-  state.st = st_ctx_l;
+  state.st = st_rule_dots;
   state.input = g_string_new(NULL);
   state.escaped_input = g_string_new(NULL);
   state.escape = FALSE;
@@ -1052,13 +1120,23 @@ main()
     case uis_workspace:
       switch (state.st) {
       case st_rule_dots:
+       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_ctx_l;
+           state.st = st_rule_dots;
            g_slist_free(g_steal_pointer(&state.support));
          }
        }
@@ -1105,7 +1183,7 @@ main()
          handle_input(&state, key);
        break;
       case st_thesis:
-       j_p = state.rule->conclusion;
+       j_p = state.judgment;
        if (state.status == 0) {
          switch (key) {
          case 'g':
@@ -1147,7 +1225,10 @@ main()
          case tk_type:
            if (!(state.err = validate_type_thesis(&state))) {
              state.caret += 1;
-             state.st = st_rule_name;
+             if (conclusion_p(state.rule, state.judgment))
+               state.st = st_rule_name;
+             else
+               state.st = st_rule_dots;
            }
            break;
          default: