Commit 1de67c5e authored by ioa's avatar ioa

Added "random" graphs web feature

parent cc0127e4
......@@ -21,7 +21,9 @@
"read"
"predicates"
"draw"))
(:file "website" :depends-on ("main"))
(:file "parse-web-input" :depends-on ("packages"))
(:file "website" :depends-on ("main"
"parse-web-input"))
(:file "example-form-groups" :depends-on ("main"))
(:file "test" :depends-on ("packages"
"graph"
......
......@@ -60,14 +60,13 @@
(assert (= 10 (length (remove-duplicates
(random-numbers
10 '(0 1 2 3 4 5 6 7 8 9 10 11) '())))))
(defun random-HR-numbers (n)
(append '(0 1)
(random-numbers n
(node-names *graph*)
(append *bad-forms*
'(0 1)))))
(defun random-graph (amount-of-nodes filename style &optional (ending "png"))
(graph
(append (random-numbers amount-of-nodes
(node-names *graph*)
(append *bad-forms*
'(0 1)))
'(1 0))
filename
style
ending))
(graph (random-HR-numbers amount-of-nodes) filename style ending))
......@@ -87,7 +87,6 @@
(:use :common-lisp
:jeffrey.graph
:jeffrey.read
:split-sequence
:external-program)
(:documentation "Creates the fancy labels that dot may use. I hope to make this obsolete at some point, and create the labels on the fly."))
......@@ -100,7 +99,7 @@
:jeffrey.draw)
(:export :name-transformer
:graph
:random-graph
:random-HR-numbers
:*local-directory*
:*names*
:*bad-forms*)
......@@ -111,9 +110,15 @@
To produce a diagram, open a Common Lisp REPL (I have tested it only with SBCL and Clozure CL so far. Please let me know if you test it with other implementations). Then type in `(ql:quickload \"jeffrey\")` and then type in `(in-package :jeffrey.main)`. Now, to draw the diagram between the forms with Howard-Rubin numbers (HR) a b c d ... use the command `(main \"a b c d ...\")`."))
(defpackage jeffrey.parse-web-input
(:use :cl :hunchentoot :split-sequence
:jeffrey.main)
(:export :process-input)
(:documentation "Parses the user input and accordingly transforms the input names to be used by `:jeffrey.website`."))
(defpackage jeffrey.website
(:use :cl :hunchentoot :html-template
:split-sequence
:jeffrey.parse-web-input
:jeffrey.main)
(:documentation "The currently unfinished website of choiceless grapher, following Adam Tornhill's \"Lisp for the Web\" www.adamtornhill.com/articles/lispweb.htm."))
(:documentation "Creates the websites using `html_template` and feeds them to a `hunchentoot` server."))
(in-package :jeffrey.website)
;; ## Website module
;;
;; Server and initial dispatch table
(defvar *server*)
......@@ -21,6 +23,8 @@
"/jeffrey.css" (local "www/jeffrey.css"))
(hunchentoot:create-prefix-dispatcher
"/diagram" 'diagram)
(hunchentoot:create-prefix-dispatcher
"/random-diagram" 'random-diagram)
(hunchentoot:create-prefix-dispatcher
"/examples" 'examples)
(hunchentoot:create-prefix-dispatcher
......@@ -33,7 +37,9 @@
:port port))))
;; strangely, the above does not work for localhost on my side...
;; but the below does transmit the website fine at http://127.0.0.1:8080/
;; but the below does transmit the website fine at
;; http://127.0.0.1:8080/
(defun start-website?? (&key (port "8080"))
(setq *server* (hunchentoot:start
(make-instance 'easy-acceptor
......@@ -42,103 +48,137 @@
(defun stop-website ()
(stop *server*))
;; HTML pages
(setq html-template:*default-template-pathname*
(concatenate 'string *local-directory* "www/"))
;; ## Index page
(defun generate-index-page ()
(with-output-to-string (stream)
(html-template:fill-and-print-template
#P"jeffrey.tmpl"
(list :title "Choiceless Grapher"
:index? T
:error? NIL
:bad-forms (format nil "~{~a~^, ~}" *bad-forms*))
:stream stream)))
;double checks:
(defun parse-input (input-string)
(when (every (lambda (x) (or (digit-char-p x)
(equal #\Space x)
(equal #\Tab x)))
input-string)
(sort (mapcar #'parse-integer
(split-sequence #\Space input-string
:remove-empty-subseqs T))
#'<)))
(defvar *temp-hack* 0
"Until I take care of concurrency, this ugly variable
will allow up to 100 large diagrams to be created in 'parallel'.")
(defun encode-names (input-names)
"This code is not a code, it's literal and too long."
(if (< (length input-names) 50)
(format nil "~{~a~^-~}" input-names)
(let ((temp-hack (write-to-string *temp-hack*)))
(prog1 (concatenate 'string
"large-diagram-" temp-hack)
(if (>= *temp-hack* 100)
(setq *temp-hack* 0)
(setq *temp-hack* (+ 1 *temp-hack*)))))))
(defun encoded-string (key input-string label-style add-top-bottom)
;=> '(names-list filename uri rel-path)
(let* ((input-names% (remove-duplicates
(if (and add-top-bottom
(equal key :these))
(append '(0 1)
#1=(parse-input input-string))
#1#)))
(input-names (name-transformer key input-names%))
(filename (concatenate 'string
label-style "-"
(encode-names input-names)))
(uri (concatenate 'string "/" filename ".png"))
(rel-path (concatenate 'string "diagrams" uri)))
(list input-names filename uri rel-path)))
(defmacro make-diagram-page (input-names uri)
;; ## Examples page
(defun examples ()
(with-output-to-string (stream)
(html-template:fill-and-print-template
#P"examples.tmpl" '()
:stream stream)))
;; ## Diagrams pages
;; ### Encoding filenames
;;
;; I represent a subset of '(0 1 ... 430) as a 431-long
;; sequence of 0s and 1s: position i will be 1 if the form with
;; HR. number i is in the subset. This sequence can be seen as an
;; integer in base 2. The encoding is this integer in base 36.
(defun names->bits (names)
(loop for i from 0 to 430
if (member i names)
sum (expt 2 i)))
(defun names->code (names)
(write-to-string (names->bits names) :base 36))
;; ### Getting the variables for the templates and the lock
(defun names->filename (names label-style)
(format nil "~a-~a" label-style (names->code names)))
(defun names->uri (names label-style)
(format nil "/~a.png" (names->filename names label-style)))
(defun names->rel-path (names label-style)
(format nil "diagrams~a" (names->uri names label-style)))
(defun names->temp (names label-style)
(format nil "diagrams/~a.temp"
(names->filename names label-style)))
(defun print-names (names &key kind)
(concatenate
'string
(case kind
("random"
(format nil
"the following (pseudo) randomly chosen forms: "))
("standard"
(format nil
"the forms with HR numbers: ")))
(format nil "~{~a~^, ~}" names)))
;; ## Graphing
;;
;; To take care of concurrency, I create a temp file when graphing,
;; whose existence `web-graph` has to check before attempting
;; to graph.
(defun create-temp (names label-style)
(with-open-file (out (local (names->temp names label-style))
:direction :output
:if-exists :error
:if-does-not-exist :create)
(declare (ignore out))))
(defun delete-temp (names label-style)
(delete-file (local (names->temp names label-style))))
(defun lock-graph (names label-style)
(create-temp names label-style)
(graph names (names->filename names label-style) label-style)
(delete-temp names label-style))
(defun file-exists-p (rel-path)
(probe-file (local rel-path)))
(defun web-graph (names label-style)
(unless (file-exists-p (names->rel-path names label-style))
(if #1=(file-exists-p (names->temp names label-style))
(loop while #1#
do (sleep 1))
(lock-graph names label-style))))
;; ### Filling the diagram templates and getting the pages online.
(defmacro get-graph (names label-style)
`(push
(hunchentoot:create-static-file-dispatcher-and-handler
(names->uri ,names ,label-style)
(local (names->rel-path ,names ,label-style)))
hunchentoot:*dispatch-table*))
(defmacro fill-template (names label-style bad-input &key kind)
`(with-output-to-string (stream)
(html-template:fill-and-print-template
#P"jeffrey.tmpl"
(list :title "Implication diagram"
:index? NIL
:print-names (format nil "~{~a~^, ~}"
,input-names)
:path-to-image ,uri)
:error? NIL
:print-names (print-names ,names :kind ,kind)
:bad-input ,bad-input
:path-to-image (names->uri ,names ,label-style))
:stream stream)))
(defun diagram ()
(let ((input-string (parameter "names"))
(label-style (parameter "label-style"))
(add-top-bottom (parameter "add-top-bottom"))
(key (cond ((parameter "these") :these)
((parameter "descendants") :descendants)
((parameter "ancestors") :ancestors)
(T (error "Unknown key used in `diagram`")))))
(destructuring-bind (input-names filename uri rel-path)
(encoded-string key input-string label-style add-top-bottom)
(progn
(unless (probe-file
(concatenate 'string
*local-directory*
rel-path))
(graph input-names filename label-style))
(push
(hunchentoot:create-static-file-dispatcher-and-handler
uri (local rel-path))
hunchentoot:*dispatch-table*)
(make-diagram-page input-names uri)))))
(defun examples ()
(with-output-to-string (stream)
(html-template:fill-and-print-template
#P"examples.tmpl" '()
:stream stream)))
(destructuring-bind (names bad-input label-style) (process-input)
(web-graph names label-style)
(get-graph names label-style)
(fill-template names label-style bad-input :kind "standard")))
(defun random-diagram ()
(let* ((n (parse-integer (parameter "n")))
(names (sort (random-HR-numbers n) #'<)))
(web-graph names "fancy")
(get-graph names "fancy")
(fill-template names "fancy" nil :kind "random")))
;;; debugging
......
<h2> The diagram of implications you requested, between the forms with HR numbers <!-- TMPL_VAR print-names -->: </h2>
<h2> The diagram of implications you requested, between <!-- TMPL_VAR print-names -->: </h2>
<img src="<!-- TMPL_VAR path-to-image -->" :alt "Your diagram">
<!-- TMPL_IF bad-input --> <!-- TMPL_INCLUDE 'bad-input.tmpl' -->
<!-- /TMPL_IF -->
<p> An arrow from A to B means that A implies B. <br/>
A boldfaced arrow from A to B moreover means that B does not imply A in ZF, so the arrow is provably not reversible in ZF. </p>
......
<h1> Choiceless Grapher </h1>
<h2> Diagram creator for consequences of the axiom of choice (AC). Enter space separated integers:</h2>
<h2> Diagram creator for consequences of the axiom of choice (AC). </h2>
<p>
Hover over forms and buttons for more details.<br/>
<strong>Enter space separated integers:</strong>
</p>
<div class="formBox">
<div class="formDiv">
<form action="/diagram" method="GET">
<input type="text" name="names" required autofocus
<input class="input" type="text" name="names" required autofocus
title="Input space separated HR numbers as integers" placeholder="Enter space separated HR numbers as integers"
pattern="(\d{0,3}[ ]+)*\d{0,3}[ ]*"
oninvalid="this.setCustomValidity('Only enter space separated integers that represent HR. form numbers.')" oninput="setCustomValidity('')" style="width:100%"><br/>
......@@ -14,21 +20,34 @@
Label style:
<input type="radio" title="Full statements in LaTeX" name="label-style" value="fancy" required checked/> fancy
<input type="radio" title="HR. form numbers" name="label-style" value="numbers"/> numbers
<br/>
<input type="submit" name="these" value="Graph these"/>
<input type="submit" name="these" value="Graph these"/>
<input type="checkbox" title="Top node is HR.1, the axiom of choice. Bottom node is HR.0, 0=0. Without a top or bottom node, these diagrams may be disconnected." name="add-top-bottom" checked="checked" value="T"/> Include top and bottom node
<input type="checkbox" title="Top node is HR.1, the axiom of choice. Bottom node is HR.0, 0=0. Without one of these, these diagrams may be disconnected." name="add-top-bottom" checked="checked" value="T"/> Include top and bottom node
<br/>
<input type="submit" name="descendants" value="Graph their descendants"/>
<input type="submit" name="ancestors" value="Graph their ancestors"/>
<br/>
Be prepared to wait more than a few minutes for diagrams with
over 30 forms, or with forms with many ancestors/descendants.
<br/>
Be prepared to wait a few minutes for diagrams with over 50 forms, or with forms with many ancestors/descendants. <br/>
</form>
</div>
<div class="formDiv">
<form action="/random-diagram" method="GET">
<strong>Get a (pseudo) random diagram</strong><br/>
of size:
<input type="text" name="n" title="Please enter a number up to 99. Top and bottom nodes will be included." required
pattern="([ ]*)\d{0,2}([ ]*)" oninvalid="Please enter a positive integer up to 99." oninput="setCustomValidity('')"
style="width: 23px"/>
<input type="submit" value="Get random graph"/>
</form>
</div>
</div>
<p> The Choiceless Grapher can produce any* size of graph of the implication and non-implication relationships between consequences of the axiom of choice, as found in the <strong>Consequences of the Axiom of Choice Project</strong> (link tba), by Prof. Paul Howard and Prof. Jean E. Rubin.</p>
<p> The Choiceless Grapher can produce any size of graph of the implication and non-implication relationships between consequences of the axiom of choice, as found in the <a href="http://consequences.emich.edu/"><strong>Consequences of the Axiom of Choice Project</strong></a>, by Prof. Paul Howard and Prof. Jean E. Rubin.</p>
<p> Accepted Howard-Rubin (HR) form numbers are between 0 and 430 (inclusive), except: <!-- TMPL_VAR bad-forms -->. All results visualised are results in Zermelo-Fraenkel set theory (ZF).</p>
......@@ -36,7 +55,3 @@ over 30 forms, or with forms with many ancestors/descendants.
<p> This project's <a href="https://github.com/ioannad/jeffrey">GitHub repository</a> contains more details.</p>
<p> (*: The website version can only handle about 70-80 form names for now. -- 12.Dec.2016)</p>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment