From da5317cc9de98070c333badacf94f782cf3a127a Mon Sep 17 00:00:00 2001
From: Akim Demaille <akim.demaille@gmail.com>
Date: Sat, 16 May 2020 10:41:06 +0200
Subject: [PATCH] cex: isolate missing API from gl_list

* src/counterexample.c (list_get_end): New.
Use it.
Reduce scopes.
---
 TODO                 | 13 +++++++++++++
 src/counterexample.c | 26 +++++++++++++++++---------
 2 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/TODO b/TODO
index 7cdd17d5..c4ae11c9 100644
--- a/TODO
+++ b/TODO
@@ -1,4 +1,17 @@
 * Bison 3.7
+** Cex
+Don't do this (counterexample.c):
+
+// This is the fastest way to get the tail node from the gl_list API.
+gl_list_node_t
+list_get_end (gl_list_t list)
+{
+  gl_list_node_t sentinel = gl_list_add_last (list, NULL);
+  gl_list_node_t res = gl_list_previous_node (list, sentinel);
+  gl_list_remove_node (list, sentinel);
+  return res;
+}
+
 ** Bistromathic
 - Hitting tab on a line with a syntax error is ugly
 
diff --git a/src/counterexample.c b/src/counterexample.c
index b6ec09bb..44222c48 100644
--- a/src/counterexample.c
+++ b/src/counterexample.c
@@ -58,6 +58,16 @@
 
 #define CUMULATIVE_TIME_LIMIT 120.0f
 
+// This is the fastest way to get the tail node from the gl_list API.
+gl_list_node_t
+list_get_end (gl_list_t list)
+{
+  gl_list_node_t sentinel = gl_list_add_last (list, NULL);
+  gl_list_node_t res = gl_list_previous_node (list, sentinel);
+  gl_list_remove_node (list, sentinel);
+  return res;
+}
+
 typedef struct
 {
   const derivation *d1;
@@ -266,19 +276,17 @@ complete_diverging_example (symbol_number conflict_sym,
       gl_list_add_last (result, derivation_dot ());
       lookahead_required = true;
     }
-  // This is the fastest way to get the tail node from the gl_list API
-  gl_list_node_t tmpd = gl_list_add_last (derivs, NULL);
-  gl_list_node_t tmps = gl_list_add_last (path, NULL);
-  gl_list_node_t deriv = gl_list_previous_node (derivs, tmpd);
-  gl_list_node_t state_node = gl_list_previous_node (path, tmps);
-  gl_list_remove_node (derivs, tmpd);
-  gl_list_remove_node (path, tmps);
-  // we go backwards through the path to create the derivation tree bottom-up.
+
+  gl_list_node_t deriv = list_get_end (derivs);
+
+  // We go backwards through the path to create the derivation tree bottom-up.
   // Effectively this loops through each production once, and generates a
   // derivation of the left hand side by appending all of the rhs symbols.
   // this becomes the derivation of the non-terminal after the dot in the
   // next production, and all of the other symbols of the rule are added as normal.
-  for (; state_node != NULL; state_node = gl_list_previous_node (path, state_node))
+  for (gl_list_node_t state_node = list_get_end (path);
+       state_node != NULL;
+       state_node = gl_list_previous_node (path, state_node))
     {
       state_item *si = (state_item *) gl_list_node_value (path, state_node);
       item_number *item = si->item;