From da5202b04a10337fdf03679dc469cb96f34f74be Mon Sep 17 00:00:00 2001 From: admin Date: Sun, 6 Oct 2024 16:37:32 -0400 Subject: [PATCH] Create a development environment for dependent type theories --- .gitignore | 24 +- Makefile.am | 107 +--- build-aux/test-driver.scm | 179 ------ configure.ac | 45 +- doc/version.texi | 4 - doc/vouivre.texi | 60 -- guix.scm | 0 hall.scm | 69 --- pre-inst-env.in | 13 - src/v.c | 1159 +++++++++++++++++++++++++++++++++++++ 10 files changed, 1187 insertions(+), 473 deletions(-) delete mode 100644 build-aux/test-driver.scm delete mode 100644 doc/version.texi delete mode 100644 doc/vouivre.texi delete mode 100644 guix.scm delete mode 100644 hall.scm delete mode 100644 pre-inst-env.in create mode 100644 src/v.c diff --git a/.gitignore b/.gitignore index 2506c62..abdb074 100644 --- a/.gitignore +++ b/.gitignore @@ -3,13 +3,13 @@ *.log *.pdf *.png -*.tar.xz *.tar.gz +*.tar.xz *.tmp *~ -.#* -\#*\# ,* +.#* +/.version /ABOUT-NLS /INSTALL /aclocal.m4 @@ -25,11 +25,11 @@ /build-aux/missing /build-aux/test-driver /build-aux/texinfo.tex +/compile /config.status /configure +/depcomp /doc/*.1 -/doc/.dirstamp -/doc/contributing.*.texi /doc/*.aux /doc/*.cp /doc/*.cps @@ -40,25 +40,33 @@ /doc/*.info-[0-9] /doc/*.ky /doc/*.pg -/doc/*.toc /doc/*.t2p +/doc/*.toc /doc/*.tp /doc/*.vr /doc/*.vrs +/doc/.dirstamp +/doc/contributing.*.texi +/doc/stamp-[0-9] /doc/stamp-vti /doc/version-*.texi +/install-sh /m4/* +/missing /pre-inst-env +/src/*.o +/src/.deps/ +/src/.dirstamp /test-env /test-tmp /tests/*.trs +/v GPATH GRTAGS GTAGS Makefile Makefile.in +\#*\# config.cache stamp-h[0-9] tmp -/.version -/doc/stamp-[0-9] diff --git a/Makefile.am b/Makefile.am index 3d3a8f6..8ac5d26 100644 --- a/Makefile.am +++ b/Makefile.am @@ -1,103 +1,4 @@ -bin_SCRIPTS = examples/example.scm \ - examples/base.scm - -# Handle substitution of fully-expanded Autoconf variables. -do_subst = $(SED) \ - -e 's,[@]GUILE[@],$(GUILE),g' \ - -e 's,[@]guilemoduledir[@],$(guilemoduledir),g' \ - -e 's,[@]guileobjectdir[@],$(guileobjectdir),g' \ - -e 's,[@]localedir[@],$(localedir),g' - -nodist_noinst_SCRIPTS = pre-inst-env - -GOBJECTS = $(SOURCES:%.scm=%.go) - -moddir=$(prefix)/share/guile/site/$(GUILE_EFFECTIVE_VERSION) -godir=$(libdir)/guile/$(GUILE_EFFECTIVE_VERSION)/site-ccache -ccachedir=$(libdir)/guile/$(GUILE_EFFECTIVE_VERSION)/site-ccache - -nobase_dist_mod_DATA = $(filter-out $(BUILT_SOURCES),$(SOURCES)) $(NOCOMP_SOURCES) -nobase_nodist_mod_DATA = $(BUILT_SOURCES) -nobase_go_DATA = $(GOBJECTS) - -# Make sure source files are installed first, so that the mtime of -# installed compiled files is greater than that of installed source -# files. See -# -# for details. -guile_install_go_files = install-nobase_goDATA -$(guile_install_go_files): install-nobase_dist_modDATA - -GUILE_WARNINGS = -Wunbound-variable -Warity-mismatch -Wformat -SUFFIXES = .scm .go -.scm.go: - $(AM_V_GEN)$(top_builddir)/pre-inst-env $(GUILE_TOOLS) compile $(GUILE_TARGET) $(GUILE_WARNINGS) -o "$@" "$<" - -SOURCES = vouivre.scm \ - language/vouivre/decompile-tree-il.scm \ - language/vouivre/spec.scm \ - language/vouivre/compile-tree-il.scm \ - vouivre/hconfig.scm \ - vouivre/curry.scm \ - vouivre/autodiff.scm \ - vouivre/misc.scm \ - vouivre/promises.scm \ - vouivre/mnist.scm - -TESTS = tests/curry.scm \ - tests/autodiff.scm - -TEST_EXTENSIONS = .scm -SCM_LOG_DRIVER = \ - $(top_builddir)/pre-inst-env \ - $(GUILE) --no-auto-compile -e main \ - $(top_srcdir)/build-aux/test-driver.scm - -# Tell 'build-aux/test-driver.scm' to display only source file names, -# not indivdual test names. -AM_SCM_LOG_DRIVER_FLAGS = --brief=yes - -AM_SCM_LOG_FLAGS = --no-auto-compile -L "$(top_srcdir)" - -AM_TESTS_ENVIRONMENT = abs_top_srcdir="$(abs_top_srcdir)" - -info_TEXINFOS = doc/version.texi \ - doc/vouivre.texi - -EXTRA_DIST = README.org \ - README \ - HACKING \ - COPYING \ - doc/vouivre.info \ - doc/version.info \ - doc/.dirstamp \ - doc/stamp-vti \ - NEWS \ - AUTHORS \ - ChangeLog \ - guix.scm \ - .gitignore \ - hall.scm \ - build-aux/texinfo.tex \ - build-aux/mdate-sh \ - build-aux/test-driver.scm \ - build-aux/missing \ - build-aux/install-sh \ - configure.ac \ - pre-inst-env.in \ - Makefile.am \ - build-aux/test-driver.scm \ - $(TESTS) - -ACLOCAL_AMFLAGS = -I m4 - -AM_DISTCHECK_DVI_TARGET = info # Disable DVI as part of distcheck - -clean-go: - -$(RM) $(GOBJECTS) -.PHONY: clean-go - -CLEANFILES = \ - $(BUILT_SOURCES) \ - $(GOBJECTS) \ - $(TESTS:tests/%.scm=%.log) +bin_PROGRAMS = v +v_SOURCES = src/v.c +v_CFLAGS = $(GLIB_CFLAGS) +v_LDADD = $(GLIB_LIBS) -lncursesw diff --git a/build-aux/test-driver.scm b/build-aux/test-driver.scm deleted file mode 100644 index 0c555ea..0000000 --- a/build-aux/test-driver.scm +++ /dev/null @@ -1,179 +0,0 @@ -;;;; test-driver.scm - Guile test driver for Automake testsuite harness - -(define script-version "2019-01-15.13") ;UTC - -;;; Copyright © 2015, 2016 Mathieu Lirzin -;;; Copyright © 2019 Alex Sassmannshausen -;;; -;;; 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 . - -;;;; 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) "") ;green - ((xfail) "") ;light green - ((skip) "") ;blue - ((fail xpass) "") ;red - ((error) "")) ;magenta - result - "") ;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))) diff --git a/configure.ac b/configure.ac index 6f61cc2..1c9d824 100644 --- a/configure.ac +++ b/configure.ac @@ -1,39 +1,10 @@ -dnl -*- Autoconf -*- - -AC_INIT(vouivre, 0.1.0) -AC_SUBST(HVERSION, "\"0.1.0\"") -AC_SUBST(AUTHOR, "\"Vouivre Digital Corporation\"") -AC_SUBST(COPYRIGHT, "'(2023)") -AC_SUBST(LICENSE, gpl3+) -AC_CONFIG_SRCDIR(vouivre.scm) -AC_CONFIG_AUX_DIR([build-aux]) -AM_INIT_AUTOMAKE([1.12 gnu silent-rules subdir-objects color-tests parallel-tests -Woverride -Wno-portability]) -AM_SILENT_RULES([yes]) - +AC_INIT([Vouivre], [0.2.0], [admin@vouivredigital.com]) +AM_INIT_AUTOMAKE([-Wall -Werror foreign subdir-objects]) +AC_PROG_CC +PKG_PROG_PKG_CONFIG +PKG_CHECK_MODULES([GLIB], [glib-2.0]) +AC_CHECK_LIB(ncursesw, initscr) +AC_SUBST(GLIB_CFLAGS) +AC_SUBST(GLIB_LIBS) AC_CONFIG_FILES([Makefile]) -AC_CONFIG_FILES([pre-inst-env], [chmod +x pre-inst-env]) - -dnl Search for 'guile' and 'guild'. This macro defines -dnl 'GUILE_EFFECTIVE_VERSION'. -GUILE_PKG([3.0 2.2 2.0]) -GUILE_PROGS -GUILE_SITE_DIR -if test "x$GUILD" = "x"; then - AC_MSG_ERROR(['guild' binary not found; please check your guile-2.x installation.]) -fi - -if test "$cross_compiling" != no; then - GUILE_TARGET="--target=$host_alias" - AC_SUBST([GUILE_TARGET]) -fi - -dnl Hall auto-generated guile-module dependencies - - -dnl Installation directories for .scm and .go files. -guilemoduledir="${datarootdir}/guile/site/$GUILE_EFFECTIVE_VERSION" -guileobjectdir="${libdir}/guile/$GUILE_EFFECTIVE_VERSION/site-ccache" -AC_SUBST([guilemoduledir]) -AC_SUBST([guileobjectdir]) - AC_OUTPUT diff --git a/doc/version.texi b/doc/version.texi deleted file mode 100644 index 049af9e..0000000 --- a/doc/version.texi +++ /dev/null @@ -1,4 +0,0 @@ -@set UPDATED 25 November 2023 -@set UPDATED-MONTH November 2023 -@set EDITION 0.2.0 -@set VERSION 0.2.0 diff --git a/doc/vouivre.texi b/doc/vouivre.texi deleted file mode 100644 index 099f512..0000000 --- a/doc/vouivre.texi +++ /dev/null @@ -1,60 +0,0 @@ -\input texinfo -@c -*-texinfo-*- - -@c %**start of header -@setfilename vouivre.info -@documentencoding UTF-8 -@settitle Vouivre Reference Manual -@c %**end of header - -@include version.texi - -@copying -Copyright @copyright{} 2023 Vouivre Digital Corporation - -Permission is granted to copy, distribute and/or modify this document -under the terms of the GNU Free Documentation License, Version 1.3 or -any later version published by the Free Software Foundation; with no -Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A -copy of the license is included in the section entitled ``GNU Free -Documentation License''. -@end copying - -@dircategory The Algorithmic Language Scheme -@direntry -* Vouivre: (vouivre). -@end direntry - -@titlepage -@title The Vouivre Manual -@author Vouivre Digital Corporation - -@page -@vskip 0pt plus 1filll -Edition @value{EDITION} @* -@value{UPDATED} @* - -@insertcopying -@end titlepage - -@contents - -@c ********************************************************************* -@node Top -@top Vouivre - -This document describes Vouivre version @value{VERSION}. - -@menu -* Introduction:: Why Vouivre? -@end menu - -@c ********************************************************************* -@node Introduction -@chapter Introduction - -INTRODUCTION HERE - -This documentation is a stub. - -@bye diff --git a/guix.scm b/guix.scm deleted file mode 100644 index e69de29..0000000 diff --git a/hall.scm b/hall.scm deleted file mode 100644 index e8d74cf..0000000 --- a/hall.scm +++ /dev/null @@ -1,69 +0,0 @@ -(hall-description - (name "vouivre") - (prefix "") - (version "0.2.0") - (author "Vouivre Digital Corporation") - (email "admin@vouivredigital.com") - (copyright (2023)) - (synopsis "") - (description "") - (home-page "https://vouivredigital.com") - (license gpl3+) - (dependencies `()) - (skip ()) - (features ((guix #f) (native-language-support #f) (licensing #f))) - (files (libraries - ((scheme-file "vouivre") - (directory - "language" - ((directory - "vouivre" - ((scheme-file "decompile-tree-il") - (scheme-file "spec") - (scheme-file "compile-tree-il"))))) - (directory - "vouivre" - ((scheme-file "hconfig") - (scheme-file "curry") - (scheme-file "autodiff") - (scheme-file "misc") - (scheme-file "promises") - (scheme-file "mnist"))))) - (tests ((directory - "tests" - ((scheme-file "curry") (scheme-file "autodiff"))))) - (programs ((directory "scripts" ()) - (directory "examples" ((scheme-file "example") - (scheme-file "base"))))) - (documentation - ((org-file "README") - (symlink "README" "README.org") - (text-file "HACKING") - (text-file "COPYING") - (text-file "COPYING.LESSER") - (directory - "doc" - ((info-file "vouivre") - (info-file "version") - (texi-file "version") - (text-file ".dirstamp") - (texi-file "vouivre") - (text-file "stamp-vti"))) - (text-file "LICENSE") - (text-file "NEWS") - (text-file "AUTHORS") - (text-file "ChangeLog"))) - (infrastructure - ((scheme-file "guix") - (text-file ".gitignore") - (scheme-file "hall") - (directory - "build-aux" - ((tex-file "texinfo") - (text-file "mdate-sh") - (scheme-file "test-driver") - (text-file "missing") - (text-file "install-sh"))) - (autoconf-file "configure") - (in-file "pre-inst-env") - (automake-file "Makefile"))))) diff --git a/pre-inst-env.in b/pre-inst-env.in deleted file mode 100644 index 31c499d..0000000 --- a/pre-inst-env.in +++ /dev/null @@ -1,13 +0,0 @@ -#!/bin/sh - -abs_top_srcdir="`cd "@abs_top_srcdir@" > /dev/null; pwd`" -abs_top_builddir="`cd "@abs_top_builddir@" > /dev/null; pwd`" - -GUILE_LOAD_COMPILED_PATH="$abs_top_builddir${GUILE_LOAD_COMPILED_PATH:+:}$GUILE_LOAD_COMPILED_PATH" -GUILE_LOAD_PATH="$abs_top_builddir:$abs_top_srcdir${GUILE_LOAD_PATH:+:}:$GUILE_LOAD_PATH" -export GUILE_LOAD_COMPILED_PATH GUILE_LOAD_PATH - -PATH="$abs_top_builddir/scripts:$PATH" -export PATH - -exec "$@" diff --git a/src/v.c b/src/v.c new file mode 100644 index 0000000..6bbb16a --- /dev/null +++ b/src/v.c @@ -0,0 +1,1159 @@ +#include +#include +#include +#include + +#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; +} -- 2.39.5