+++ /dev/null
-;;;; test-driver.scm - Guile test driver for Automake testsuite harness
-
-(define script-version "2019-01-15.13") ;UTC
-
-;;; Copyright © 2015, 2016 Mathieu Lirzin <mthl@gnu.org>
-;;; Copyright © 2019 Alex Sassmannshausen <alex@pompo.co>
-;;;
-;;; This program is free software; you can redistribute it and/or modify it
-;;; under the terms of the GNU General Public License as published by
-;;; the Free Software Foundation; either version 3 of the License, or (at
-;;; your option) any later version.
-;;;
-;;; This program is distributed in the hope that it will be useful, but
-;;; WITHOUT ANY WARRANTY; without even the implied warranty of
-;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-;;; GNU General Public License for more details.
-;;;
-;;; You should have received a copy of the GNU General Public License
-;;; along with this program. If not, see <http://www.gnu.org/licenses/>.
-
-;;;; Commentary:
-;;;
-;;; This script provides a Guile test driver using the SRFI-64 Scheme API for
-;;; test suites. SRFI-64 is distributed with Guile since version 2.0.9.
-;;;
-;;; This script is a lightly modified version of the orignal written by
-;;; Matthieu Lirzin. The changes make it suitable for use as part of the
-;;; guile-hall infrastructure.
-;;;
-;;;; Code:
-
-(use-modules (ice-9 getopt-long)
- (ice-9 pretty-print)
- (srfi srfi-26)
- (srfi srfi-64))
-
-(define (show-help)
- (display "Usage:
- test-driver --test-name=NAME --log-file=PATH --trs-file=PATH
- [--expect-failure={yes|no}] [--color-tests={yes|no}]
- [--enable-hard-errors={yes|no}] [--brief={yes|no}}] [--]
- TEST-SCRIPT [TEST-SCRIPT-ARGUMENTS]
-The '--test-name', '--log-file' and '--trs-file' options are mandatory.
-"))
-
-(define %options
- '((test-name (value #t))
- (log-file (value #t))
- (trs-file (value #t))
- (color-tests (value #t))
- (expect-failure (value #t)) ;XXX: not implemented yet
- (enable-hard-errors (value #t)) ;not implemented in SRFI-64
- (brief (value #t))
- (help (single-char #\h) (value #f))
- (version (single-char #\V) (value #f))))
-
-(define (option->boolean options key)
- "Return #t if the value associated with KEY in OPTIONS is 'yes'."
- (and=> (option-ref options key #f) (cut string=? <> "yes")))
-
-(define* (test-display field value #:optional (port (current-output-port))
- #:key pretty?)
- "Display 'FIELD: VALUE\n' on PORT."
- (if pretty?
- (begin
- (format port "~A:~%" field)
- (pretty-print value port #:per-line-prefix "+ "))
- (format port "~A: ~S~%" field value)))
-
-(define* (result->string symbol #:key colorize?)
- "Return SYMBOL as an upper case string. Use colors when COLORIZE is #t."
- (let ((result (string-upcase (symbol->string symbol))))
- (if colorize?
- (string-append (case symbol
- ((pass) "\e[0;32m") ;green
- ((xfail) "\e[1;32m") ;light green
- ((skip) "\e[1;34m") ;blue
- ((fail xpass) "\e[0;31m") ;red
- ((error) "\e[0;35m")) ;magenta
- result
- "\e[m") ;no color
- result)))
-
-(define* (test-runner-gnu test-name #:key color? brief? out-port trs-port)
- "Return an custom SRFI-64 test runner. TEST-NAME is a string specifying the
-file name of the current the test. COLOR? specifies whether to use colors,
-and BRIEF?, well, you know. OUT-PORT and TRS-PORT must be output ports. The
-current output port is supposed to be redirected to a '.log' file."
-
- (define (test-on-test-begin-gnu runner)
- ;; Procedure called at the start of an individual test case, before the
- ;; test expression (and expected value) are evaluated.
- (let ((result (cute assq-ref (test-result-alist runner) <>)))
- (format #t "test-name: ~A~%" (result 'test-name))
- (format #t "location: ~A~%"
- (string-append (result 'source-file) ":"
- (number->string (result 'source-line))))
- (test-display "source" (result 'source-form) #:pretty? #t)))
-
- (define (test-on-test-end-gnu runner)
- ;; Procedure called at the end of an individual test case, when the result
- ;; of the test is available.
- (let* ((results (test-result-alist runner))
- (result? (cut assq <> results))
- (result (cut assq-ref results <>)))
- (unless brief?
- ;; Display the result of each test case on the console.
- (format out-port "~A: ~A - ~A~%"
- (result->string (test-result-kind runner) #:colorize? color?)
- test-name (test-runner-test-name runner)))
- (when (result? 'expected-value)
- (test-display "expected-value" (result 'expected-value)))
- (when (result? 'expected-error)
- (test-display "expected-error" (result 'expected-error) #:pretty? #t))
- (when (result? 'actual-value)
- (test-display "actual-value" (result 'actual-value)))
- (when (result? 'actual-error)
- (test-display "actual-error" (result 'actual-error) #:pretty? #t))
- (format #t "result: ~a~%" (result->string (result 'result-kind)))
- (newline)
- (format trs-port ":test-result: ~A ~A~%"
- (result->string (test-result-kind runner))
- (test-runner-test-name runner))))
-
- (define (test-on-group-end-gnu runner)
- ;; Procedure called by a 'test-end', including at the end of a test-group.
- (let ((fail (or (positive? (test-runner-fail-count runner))
- (positive? (test-runner-xpass-count runner))))
- (skip (or (positive? (test-runner-skip-count runner))
- (positive? (test-runner-xfail-count runner)))))
- ;; XXX: The global results need some refinements for XPASS.
- (format trs-port ":global-test-result: ~A~%"
- (if fail "FAIL" (if skip "SKIP" "PASS")))
- (format trs-port ":recheck: ~A~%"
- (if fail "yes" "no"))
- (format trs-port ":copy-in-global-log: ~A~%"
- (if (or fail skip) "yes" "no"))
- (when brief?
- ;; Display the global test group result on the console.
- (format out-port "~A: ~A~%"
- (result->string (if fail 'fail (if skip 'skip 'pass))
- #:colorize? color?)
- test-name))
- #f))
-
- (let ((runner (test-runner-null)))
- (test-runner-on-test-begin! runner test-on-test-begin-gnu)
- (test-runner-on-test-end! runner test-on-test-end-gnu)
- (test-runner-on-group-end! runner test-on-group-end-gnu)
- (test-runner-on-bad-end-name! runner test-on-bad-end-name-simple)
- runner))
-
-;;;
-;;; Entry point.
-;;;
-
-(define (main . args)
- (let* ((opts (getopt-long (command-line) %options))
- (option (cut option-ref opts <> <>)))
- (cond
- ((option 'help #f) (show-help))
- ((option 'version #f) (format #t "test-driver.scm ~A" script-version))
- (else
- (let ((log (open-file (option 'log-file "") "w0"))
- (trs (open-file (option 'trs-file "") "wl"))
- (out (duplicate-port (current-output-port) "wl")))
- (redirect-port log (current-output-port))
- (redirect-port log (current-warning-port))
- (redirect-port log (current-error-port))
- (test-with-runner
- (test-runner-gnu (option 'test-name #f)
- #:color? (option->boolean opts 'color-tests)
- #:brief? (option->boolean opts 'brief)
- #:out-port out #:trs-port trs)
- (load-from-path (option 'test-name #f)))
- (close-port log)
- (close-port trs)
- (close-port out))))
- (exit 0)))
--- /dev/null
+#include <curses.h>
+#include <locale.h>
+#include <glib.h>
+#include <signal.h>
+
+#define PAIR_BW 1
+#define PAIR_WB 2
+#define PAIR_HL 3
+#define PAIR_SUCCESS 4
+#define PAIR_ERROR 5
+
+#define KEY_ESC 27
+#define KEY_RETURN '\n'
+#define KEY_TAB '\t'
+
+#define NB_COLUMNS 80
+#define HYPOTHESES_SPACING 4
+#define EMPTY_SLOT "█"
+
+enum ui_state
+ {
+ uis_splash,
+ uis_workspace,
+ };
+
+enum slot_type
+ {
+ st_rule_dots,
+ st_ctx_l,
+ st_ctx_v,
+ st_ctx_t,
+ st_ctx_dots,
+ st_ctx_r,
+ st_thesis,
+ st_a,
+ st_b,
+ st_c,
+ st_rule_name,
+ };
+
+enum caret_to_point
+ {
+ ctp_before = -1,
+ ctp_on = 0,
+ ctp_after = +1,
+ };
+
+enum thesis_kind
+ {
+ tk_generic,
+ tk_type,
+ tk_element,
+ tk_type_equal,
+ tk_element_equal,
+ tk_unknown,
+ };
+
+enum scope
+ {
+ s_contextual,
+ s_local,
+ s_global,
+ };
+
+enum name_kind
+ {
+ nk_variable,
+ nk_element,
+ nk_type,
+ nk_generic_context,
+ nk_generic_thesis,
+ };
+
+struct wrap
+{
+ bool is_origin;
+ void *ptr; /* name or reference */
+};
+
+struct name
+{
+ enum scope scope;
+ enum name_kind kind;
+ struct wrap *type;
+ struct rule *src;
+ GSList *dependencies; /* names */
+ char *str;
+};
+
+struct reference
+{
+ struct name *origin;
+ GSList *replacements; /* wraps */
+};
+
+struct vdecl
+{
+ struct name *elem;
+ struct wrap *type;
+};
+
+struct judgment
+{
+ enum thesis_kind kind;
+ struct wrap *generic_l;
+ struct wrap *generic_r;
+ struct wrap *a;
+ struct wrap *b;
+ GSList *vdecls;
+};
+
+struct rule
+{
+ char *name;
+ GSList *hypotheses; /* judgments */
+ 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
+ * the address of the caret, i.e. where we are currently editing, we set the
+ * flag `is_pt_geq_caret', allowing us to know whether or not to draw dots and
+ * conditional slots.
+ */
+struct state
+{
+ bool running;
+ enum ui_state mode;
+ struct rule *rule;
+ struct judgment *judgment;
+ struct name *dependency;
+ WINDOW *workspace_w;
+ WINDOW *support_w;
+ WINDOW *echo_w;
+ GHashTable *rules; /* str -> rule */
+ GHashTable *decls; /* str -> name */
+ GHashTable *gctxs; /* str -> name */
+ GHashTable *gtheses; /* str -> name */
+ GHashTable *vets; /* str -> name */
+ GSList *support; /* rules */
+ int caret;
+ enum slot_type st;
+ GString *input;
+ GString *escaped_input;
+ int status;
+ bool escape;
+ int err;
+};
+
+const char *escaped_strings[] = {
+ "α", "alpha",
+ "β", "beta",
+ "Γ", "Gamma",
+ "γ", "gamma",
+ "Δ", "Delta",
+ "δ", "delta",
+ "ε", "epsilon",
+ "Ζ", "Zeta",
+ "ζ", "zeta",
+ "η", "eta",
+ "Θ", "Theta",
+ "θ", "theta",
+ "Ι", "Iota",
+ "ι", "iota",
+ "κ", "kappa",
+ "Λ", "Lambda",
+ "λ", "lambda",
+ "μ", "mu",
+ "ν", "nu",
+ "Ξ", "Xi",
+ "ξ", "xi",
+ "Ο", "Omicron",
+ "ο", "omicron",
+ "Π", "Pi",
+ "π", "pi",
+ "Ρ", "Rho",
+ "ρ", "rho",
+ "Σ", "Sigma",
+ "σ", "sigma",
+ "υ", "upsilon",
+ "Φ", "Phi",
+ "φ", "phi",
+ "Χ", "Chi",
+ "χ", "chi",
+ "Ψ", "Psi",
+ "ψ", "psi",
+ "Ω", "Omega",
+ "ω", "omega",
+ "𝔸", "AA",
+ "𝔹", "BB",
+ "ℂ", "CC",
+ "𝔻", "DD",
+ "𝔼", "EE",
+ "𝔽", "FF",
+ "𝔾", "GG",
+ "ℍ", "HH",
+ "𝕀", "II",
+ "𝕁", "JJ",
+ "𝕂", "KK",
+ "𝕃", "LL",
+ "𝕄", "MM",
+ "ℕ", "NN",
+ "𝕆", "OO",
+ "ℙ", "PP",
+ "ℚ", "QQ",
+ "ℝ", "RR",
+ "𝕊", "SS",
+ "𝕋", "TT",
+ "𝕌", "UU",
+ "𝕍", "VV",
+ "𝕎", "WW",
+ "𝕏", "XX",
+ "𝕐", "YY",
+ "ℤ", "ZZ",
+ "𝕒", "aa",
+ "𝕓", "bb",
+ "𝕔", "cc",
+ "𝕕", "dd",
+ "𝕖", "ee",
+ "𝕗", "ff",
+ "𝕘", "gg",
+ "𝕙", "hh",
+ "𝕚", "ii",
+ "𝕛", "jj",
+ "𝕜", "kk",
+ "𝕝", "ll",
+ "𝕞", "mm",
+ "𝕟", "nn",
+ "𝕠", "oo",
+ "𝕡", "pp",
+ "𝕢", "qq",
+ "𝕣", "rr",
+ "𝕤", "ss",
+ "𝕥", "tt",
+ "𝕦", "uu",
+ "𝕧", "vv",
+ "𝕨", "ww",
+ "𝕩", "xx",
+ "𝕪", "yy",
+ "𝕫", "zz",
+ "𝟘", "00",
+ "𝟙", "11",
+ "𝟚", "22",
+ "𝟛", "33",
+ "𝟜", "44",
+ "𝟝", "55",
+ "𝟞", "66",
+ "𝟟", "77",
+ "𝟠", "88",
+ "𝟡", "99",
+};
+
+GHashTable *escaped_table;
+
+struct wrap *
+create_wrap(bool is_origin, void *ptr)
+{
+ struct wrap *w;
+
+ w = malloc(sizeof(struct wrap));
+ w->is_origin = is_origin;
+ w->ptr = ptr;
+ return w;
+}
+
+struct name *
+create_name(enum scope scope, enum name_kind kind, struct wrap *type,
+ struct rule *src, GSList *dependencies, char *str)
+{
+ struct name *name;
+
+ name = malloc(sizeof(struct name));
+ name->scope = scope;
+ name->kind = kind;
+ name->type = type;
+ name->src = src;
+ name->dependencies = dependencies;
+ name->str = str;
+ return name;
+}
+
+struct rule *
+create_rule()
+{
+ struct rule *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;
+ return rule;
+}
+
+void free_wrap(struct wrap *);
+
+void
+free_name(struct name *name)
+{
+ if (name) {
+ free_wrap(name->type);
+ g_slist_free(name->dependencies);
+ free(name->str);
+ free(name);
+ }
+}
+
+void
+free_reference(struct reference *ref)
+{
+ if (ref) {
+ free_name(ref->origin);
+ g_slist_free_full(ref->replacements, (GDestroyNotify)free_wrap);
+ free(ref);
+ }
+}
+
+
+void
+free_wrap(struct wrap *wrap)
+{
+ if (wrap) {
+ if (wrap->is_origin)
+ free_name(wrap->ptr);
+ else
+ free_reference(wrap->ptr);
+ free(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)
+{
+ if (judgment) {
+ free_wrap(judgment->generic_l);
+ free_wrap(judgment->generic_r);
+ free_wrap(judgment->a);
+ free_wrap(judgment->b);
+ g_slist_free_full(judgment->vdecls, (GDestroyNotify)free_vdecl);
+ free(judgment);
+ }
+}
+
+void
+free_rule(struct rule *rule)
+{
+ if (rule) {
+ free(rule->name);
+ g_slist_free_full(rule->hypotheses, (GDestroyNotify)free_judgment);
+ free_judgment(rule->conclusion);
+ free(rule);
+ }
+}
+
+int
+greekstrlen(const char *str)
+{
+ return mbstowcs(NULL, str, 0);
+}
+
+void
+draw_slot(WINDOW *w, int *y, int *x, bool virtual, bool optional, int pair, const char *str)
+{
+ if (!virtual) {
+ wattron(w, COLOR_PAIR(pair));
+ wmove(w, *y, *x);
+ if (str && *str != '\0')
+ wprintw(w, str);
+ else {
+ wprintw(w, EMPTY_SLOT);
+ if (optional)
+ wprintw(w, "?");
+ }
+ wattroff(w, COLOR_PAIR(pair));
+ }
+ if (str && *str != '\0')
+ *x += greekstrlen(str);
+ else {
+ if (optional)
+ *x += 2;
+ else
+ *x += 1;
+ }
+}
+
+void
+draw_wrap(WINDOW *w, int *y, int *x, bool virtual, bool optional,
+ int pair, struct wrap *wrap)
+{
+ struct reference *r;
+ GSList *l;
+
+ if (!wrap)
+ draw_slot(w, y, x, virtual, optional, 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, "]");
+ }
+ }
+ }
+}
+
+struct wrap *
+get_wrap_type(struct wrap *wrap)
+{
+ if (wrap) {
+ if (wrap->is_origin)
+ return ((struct name *)wrap->ptr)->type;
+ else
+ return ((struct reference *)wrap->ptr)->origin->type;
+ }
+ 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;
+}
+
+void
+draw_judgment(WINDOW *w, int *y, int *x, bool virtual, bool workplace_mode,
+ int caret, int *point, char *inputstr, struct judgment *judgment)
+{
+ bool v, prev_not_displayed;
+ int pair;
+ GSList *l;
+ struct vdecl *decl;
+ enum caret_to_point ctp;
+
+ v = virtual;
+
+ /* Γ */
+ set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
+ if (judgment->generic_l)
+ draw_wrap(w, y, x, v, TRUE, pair, judgment->generic_l);
+ else if (workplace_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;
+ }
+ 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, ", ");
+ 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;
+ l = l->next;
+ }
+
+ /* ctx_dots */
+ set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
+ if (workplace_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, "...");
+ prev_not_displayed = FALSE;
+ }
+
+ /* Δ */
+ 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 (workplace_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);
+ }
+ }
+
+ draw_slot(w, y, x, v, FALSE, PAIR_BW, " ⊢ ");
+
+ /* 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);
+ 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");
+ 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));
+ 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");
+ 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));
+ break;
+ case tk_unknown:
+ set_ctp_and_pair(&ctp, &pair, caret, (*point)++);
+ draw_slot(w, y, x, v, FALSE, pair, NULL);
+ break;
+ default:
+ }
+}
+
+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;
+ enum caret_to_point ctp;
+
+ point = 0;
+ *y = 0; c = 0; r = 0;
+ 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 (!virtual) {
+ *y = row + 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;
+ draw_judgment(w, y, x, virtual, workspace_mode,
+ caret, &point, inputstr, rule->conclusion);
+ 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;
+}
+
+void
+render_splash()
+{
+ clear();
+ mvprintw(0, 0, "VOUIVRE version 0.2.0");
+ mvprintw(1, 0, "press any key to continue");
+ refresh();
+}
+
+void
+echo_status(WINDOW *w, int status)
+{
+ int pair;
+ char *str;
+
+ if (status)
+ pair = PAIR_ERROR;
+ else
+ pair = PAIR_SUCCESS;
+ switch (status) {
+ case 0:
+ str = "valid";
+ case 1:
+ str = "error: empty slot";
+ break;
+ case 2:
+ str = "error: rule name already exists";
+ break;
+ case 3:
+ str = "error: unknown name";
+ break;
+ case 4:
+ str = "error: left and right generic contexts must differ";
+ break;
+ case 5:
+ str = "error: type already defined";
+ break;
+ case 6:
+ str = "error: inconsistant kinds"; /* TODO: list the two kinds conflicting */
+ break;
+ default:
+ str = "error: TBD";
+ }
+ wattron(w, COLOR_PAIR(pair));
+ mvwprintw(w, 0, 0, str);
+ wattroff(w, COLOR_PAIR(pair));
+}
+
+void
+render(struct state *state)
+{
+ int y, x, q, i;
+ 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;
+ gpointer key, value;
+ struct rule *rule;
+
+ q = (LINES - 3) / 2;
+ clear();
+
+ /* draw debug info */
+ mvwprintw(stdscr, LINES - 3, 0, "mode: %d st: %d caret: %d",
+ state->mode, state->st, state->caret);
+
+ /* draw workspace rule */
+ y = 0; x = 0;
+ draw_rule(state->workspace_w, &y, &x, FALSE, TRUE,
+ state->caret, state->input->str, state->rule);
+
+ /* draw existing rules */
+ i = 0;
+ g_hash_table_iter_init(&iter, state->rules);
+ while (g_hash_table_iter_next(&iter, &key, &value))
+ {
+ rule = value;
+ y = i; x = COLS / 2;
+ draw_rule(state->support_w, &y, &x, FALSE, FALSE, -1, NULL, rule);
+ i = y + 2;
+ }
+
+ /* 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 echo area */
+ if (state->err) {
+ echo_status(state->echo_w, state->err);
+ state->err = 0;
+ }
+ else {
+ switch (state->mode) {
+ case uis_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) {
+ mvwprintw(state->echo_w, 0, 0, "\\");
+ wprintw(state->echo_w, state->escaped_input->str);
+ }
+ break;
+ default:
+ }
+ }
+
+ /* draw window names */
+ attron(COLOR_PAIR(PAIR_WB));
+ move(q, 0);
+ printw("workspace%*s", COLS - 9, "");
+ move(2 * q + 1, 0);
+ printw("support%*s", COLS - 7, "");
+ attroff(COLOR_PAIR(PAIR_WB));
+
+ refresh();
+}
+
+void
+handle_input(struct state *state, char key)
+{
+ GSList *l;
+ struct name *name;
+
+ if (key == '\\') {
+ state->escape = TRUE;
+ state->status = 0;
+ g_string_erase(state->escaped_input, 0, -1);
+ }
+ else if (key > 32 && key < 127) {
+ if (!state->escape)
+ 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);
+ if (!l) {
+ state->escape = FALSE;
+ }
+ else if (!l->next) {
+ state->escape = FALSE;
+ state->input = g_string_append(state->input, l->data);
+ }
+ }
+ else
+ state->escape = FALSE;
+ }
+ }
+ 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);
+ }
+}
+
+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)
+{
+ 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);
+ }
+ else {
+ if (state->judgment->generic_l &&
+ name == state->judgment->generic_l->ptr)
+ return 4;
+ state->judgment->generic_r = create_wrap(FALSE, name);
+ }
+ g_string_erase(state->input, 0, -1);
+ return 0;
+ }
+ else
+ return -1;
+}
+
+GSList *
+list_dependencies(GHashTable *vets)
+{
+ GSList *l;
+ GHashTableIter iter;
+ gpointer key, value;
+
+ 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 */
+ return l;
+}
+
+int
+validate_type_thesis(struct state *state)
+{
+ struct name *name;
+
+ 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)))
+ return 5;
+ if ((name = g_hash_table_lookup(state->vets, state->input->str))) {
+ if (name->kind != nk_type)
+ return 6;
+
+ /* the name exists, is a type, and is local */
+ state->judgment->a = create_wrap(FALSE, name);
+ return -1; /* TODO: check dependencies */
+ }
+ 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;
+ }
+ }
+ return -1;
+}
+
+int
+validate_rule_name(struct state *state)
+{
+ struct rule *rule;
+ struct judgment *c;
+ struct name *name;
+
+ rule = state->rule;
+ if (*state->input->str == '\0')
+ return 1;
+ 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);
+ c = rule->conclusion;
+ switch (c->kind) {
+ case tk_type:
+ if (c->a->is_origin) {
+ name = c->a->ptr;
+ g_hash_table_insert(state->decls, name->str, name);
+ }
+ break;
+ default:
+ }
+ g_string_erase(state->input, 0, -1);
+ state->rule = create_rule();
+ state->judgment = state->rule->conclusion;
+ return 0;
+}
+
+int
+main()
+{
+ const char *k, *v;
+ char key, *str;
+ int i, j, q;
+ struct state state;
+ struct judgment *j_p;
+ GSList *l;
+ GHashTableIter iter;
+ gpointer hkey, hvalue;
+
+ setlocale(LC_ALL, "");
+ initscr();
+ start_color();
+ curs_set(0);
+ cbreak();
+ noecho();
+ 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));
+ q = (LINES - 3) / 2;
+ state.running = TRUE;
+ state.mode = uis_splash;
+ state.rule = create_rule();
+ state.judgment = state.rule->conclusion;
+ state.dependency = NULL;
+ state.workspace_w = subwin(stdscr, q, COLS, 0, 0);
+ state.support_w = subwin(stdscr, q, COLS, q + 1, 0);
+ state.echo_w = subwin(stdscr, 1, COLS, LINES - 1, 0);
+ state.rules = g_hash_table_new_full(g_str_hash, g_str_equal,
+ free, (GDestroyNotify)free_rule);
+ state.decls = 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.vets = g_hash_table_new(g_str_hash, g_str_equal);
+ state.support = NULL;
+ state.caret = 0;
+ state.st = st_ctx_l;
+ state.input = g_string_new(NULL);
+ state.escaped_input = g_string_new(NULL);
+ state.escape = FALSE;
+ state.err = 0;
+
+ /* populate escaped strings table */
+ /* NOTE: `g_hash_table_insert' deletes keys and values if they already exist.
+ This is not what we want for the value list. Thus, we will free the
+ values manually before destroying the table.
+ */
+ escaped_table = g_hash_table_new_full(g_str_hash, g_str_equal, free, NULL);
+ for (i = 0 ; i < sizeof(escaped_strings) / sizeof(char *) / 2 ; i++) {
+ k = escaped_strings[2 * i + 1];
+ v = escaped_strings[2 * i + 0];
+ for (j = 1 ; j <= strlen(k) ; j++) {
+ str = strndup(k, j);
+ l = g_hash_table_lookup(escaped_table, str);
+ l = g_slist_prepend(l, (void *)v);
+ g_hash_table_insert(escaped_table, str, l);
+ }
+ }
+
+ if (state.mode == uis_splash) {
+ render_splash();
+ getch();
+ state.mode = uis_workspace;
+ render(&state);
+ }
+ while(state.running) {
+ key = getch();
+ if (key == KEY_ESC) {
+ state.running = FALSE;
+ break;
+ }
+ switch(state.mode) {
+ case uis_workspace:
+ switch (state.st) {
+ case st_rule_dots:
+ 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;
+ g_slist_free(g_steal_pointer(&state.support));
+ }
+ }
+ 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
+ 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
+ handle_input(&state, key);
+ break;
+ case st_thesis:
+ j_p = state.rule->conclusion;
+ 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 (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_a:
+ if (key == KEY_TAB) {
+ switch (state.judgment->kind) {
+ case tk_type:
+ if (!(state.err = validate_type_thesis(&state))) {
+ state.caret += 1;
+ state.st = st_rule_name;
+ }
+ break;
+ default:
+ state.err = -1;
+ }
+ }
+ 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 {
+ state.st = st_rule_name;
+ }
+ }
+ else
+ handle_input(&state, key);
+ break;
+ case st_c:
+ if (key == KEY_TAB) {
+ state.caret += 1;
+ state.st = st_rule_name;
+ }
+ else
+ handle_input(&state, key);
+ break;
+ default:
+ }
+ break;
+ default:
+ }
+ render(&state);
+ }
+ delwin(state.workspace_w);
+ delwin(state.support_w);
+ delwin(state.echo_w);
+ endwin();
+ g_hash_table_iter_init(&iter, escaped_table);
+ while (g_hash_table_iter_next(&iter, &hkey, &hvalue))
+ g_slist_free(hvalue);
+ g_hash_table_destroy(escaped_table);
+ free_rule(state.rule);
+ g_hash_table_destroy(state.rules);
+ g_hash_table_destroy(state.decls);
+ g_hash_table_destroy(state.gctxs);
+ g_hash_table_destroy(state.gtheses);
+ g_hash_table_destroy(state.vets);
+ g_slist_free(state.support);
+ g_string_free(state.input, TRUE);
+ g_string_free(state.escaped_input, TRUE);
+ return 0;
+}
projects / vouivre.git / commitdiff