Commit 8b679f55 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

separated dune from flask

parent 0d999b01
[uwsgi]
module = wsgi:app
master = true
processes = 5
socket = /home/samuel/alpha/alpha.sock
chmod-socket = 666
uid = samuel
gid = www-data
vacuum = true
die-on-term = true
logto = /home/samuel/alpha/alpha.log
# -*- coding: utf-8 -*-
from flask import Flask, abort, render_template
import os
import json
import yaml
import subprocess
from flask import request
app = Flask(__name__)
def call_check(closed_term):
term_parsed = closed_term.replace(".", " -> ").replace("λ", "\\")
try:
typable = subprocess.check_output('./check.exe "' + term_parsed + '"', shell=True, cwd="stlc-infer", timeout=20)
return typable.decode('utf-8').strip()
except Exception as e:
return "Cannot check."
def get_random_term():
try:
term = subprocess.check_output('python3 random.py', shell=True, cwd='bnf/', timeout=20)
return term.decode('utf-8').strip()
except Exception as e:
return '(/x./y.x) y'
@app.route('/', methods=['GET', 'POST'])
def index():
term = get_random_term()
cterm = term
sim = 'false'
tterm = '(/x^0./y^0.x) y'
max_depth = '16'
ctx = 'y^0'
term_type = 'untyped'
res = ''
if request.method == 'POST':
max_depth = request.form['max_depth']
sim = 'true' if 'simultaneous' in request.form else 'false'
term_type = request.form['term-type']
if term_type == 'typed':
ctx = request.form['ctx']
tterm = request.form['tterm']
cterm = ctx + ":" + tterm
else:
term = request.form['term']
cterm = term
try:
res = subprocess.check_output('./main.exe ' + max_depth + ' ' + sim + ' false "' + cterm + '"', shell=True, timeout=20)
dct = yaml.safe_load(res)
dct = {k: v for d in dct for k, v in d.items()}
vc = dct['vc']
closed_term = dct['closed_term']
typable = call_check(closed_term)
max_depth = dct['max_depth']
oc = dct['order_consistent']
safe = dct['is_safe']
nf = dct['normal form']
safenaming = dct['safe_naming']
linear = dct['is_linear']
dot = dct['dot']
dot = dot.replace('"', '\"').replace('\r', '').replace('\n', ' ')
dot = json.dumps(dot)
attrs = { 'Variable capture' : vc, 'Safe naming': safenaming, 'Typable': typable, 'Linear': linear }
if term_type == 'typed':
attr['Order consistent'] = oc
attr['Safe'] = safe
if typable == "Typable.":
attrs["Normal form"] = nf
return render_template('index.html', error=False, info='', sim=sim=='true', tt=term_type, ctx=ctx, dot=dot, tterm=tterm, term=term, max_depth=max_depth, attrs=attrs)
except Exception as e:
return render_template('index.html', error=True, info="Error", sim=sim=='true', tt=term_type, dot="", ctx=ctx, tterm=tterm, term=term, max_depth=max_depth, attrs={})
if __name__ == '__main__':
app.run(host='0.0.0.0', debug=True)
# bnfgen
Script that generates random terms according to `grammar.bnf`
## Dependencies
```
opam install bnfgen
```
## Execution
Run following command in the `bnf` directory.
```
bnfgen --separator "" grammar.bnf
```
# A trivial subset of English.
# Generates one or more sentences.
# Generate up to ten sentences
<start> ::= <TERM>{1,1} ;
# It's fine to declare symbols out of order
# (<line_break> is defined at the end of the file).
<TERM> ::= 40 <VAR> | 30 "(" <TERM> ") (" <TERM> ")" | 30 <LAM>;
<VAR_XYZ> ::=
"x"
| "y"
| "z"
;
<VAR_REST> ::=
"a"
| "b"
| "c"
| "d"
| "e"
| "f"
| "g"
| "h"
| "i"
;
<VAR> ::= 60 <VAR_XYZ> | 40 <VAR_REST> ;
<LAM> ::= 70 "/" <VAR_XYZ> "." <TERM> | 30 "/" <VAR_REST> "." <TERM>;
import os
import yaml
import subprocess
def gen():
term = subprocess.check_output('/home/samuel/.opam/default/bin/bnfgen --separator "" grammar.bnf', shell=True, timeout=20)
term = term.decode('utf-8').strip()
return term
while True:
t = gen()
if len(t) < 80 and len(t) > 7:
break
print(t)
# stlc-infer
A small interpreter for the simply typed lambda calculus, with type inference.
[https://github.com/jez/stlc-infer](https://github.com/jez/stlc-infer)
The `check` executable relies on the implementation of the type inference algorithm from the repository referenced above.
import subprocess
import argparse
import os
parser = argparse.ArgumentParser(description='Call stlc-infer')
parser.add_argument('term',
help='the term as string')
args = parser.parse_args()
term_parsed = args.term.replace(".", " -> ").replace("λ", "\\")
try:
res = subprocess.check_output('./check "' + term_parsed + '"', shell=True, timeout=20)
print(res.decode("utf-8").replace('\n', ''))
except Exception as e:
print("Cannot check")
<!DOCTYPE html>
<html>
<meta name="MSSmartTagsPreventParsing" content="true" />
<meta http-equiv="content-type" content="text/html; charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>Alpha Avoidance</title>
<style>
body {
font-family: Arial;
padding: 0;
margin: 0;
height: 100vh;
font-size: 1.2em;
}
.footer {
position: absolute;
bottom: 10px;
right: 0;
left: 0;
text-align: center;
}
.sidebar .footer {
font-size: 12px;
bottom: 16px;
}
input[type=text], input[type=number] {
width: 100%;
padding: 6px 10px;
margin: 8px 0;
box-sizing: border-box;
border: none;
background: #eee;
border-radius: 4px;
}
input[type=text] {
font-family: monospace;
font-size: 14px;
}
button, input[type=button], input[type=submit], input[type=reset] {
background-color: #7A88A4;
border: none;
color: white;
padding: 12px 24px;
text-decoration: none;
cursor: pointer;
display: block;
width: 100%;
margin-top: 1em;
border-radius: 3px;
}
svg {
width: 100%;
height: 100%;
}
.row {
width: 100%;
}
.sidebar {
width: 30%;
float: left;
height: 100vh;
position: relative;
background: #485f73;
color: #fff;
}
.sidebar-header {
padding: .8em;
text-align: center;
background: #2e4159;
}
.sidebar-content {
padding: .8em;
}
.sidebar-content ul {
margin-top: 2em;
}
.content {
width: 70%;
float: left;
height: 100vh;
position: relative;
}
#graph {
border: 1px solid #ddd;
height: 100vh;
}
#toptop {
display: none;
}
div.grammars {
border: 1px solid #ddd;
padding: 1em .5em;
margin: 1em 0;
}
ul.grammar {
padding: 0;
margin: 0;
list-style: none;
font-family: monospace;
font-size: 10px
}
#typed-grammar,
#type-grammar, #ctx-grammar, #typed-wrapper {
display: none;
}
.term-type {
display: block;
}
.term-type-option {
float: left;
width: 50%;
padding: 1em 0;
text-align: center;
}
@media (max-width: 992px) {
#totop {
position: fixed;
right: 12px;
bottom: 12px;
background: #2e4159;
border-radius: 100%;
width: 38px;
height: 38px;
font-size: 38px;
padding: 0;
text-align: center;
color: #fff;
display: none;
}
.sidebar {
width: 100%;
height: auto;
float: none;
display: block;
}
.content {
width: 100%;
float: none;
display: block;
}
.footer {
display: none;
}
}
</style>
<script src="//d3js.org/d3.v5.min.js"></script>
<script src="https://unpkg.com/@hpcc-js/wasm@0.3.11/dist/index.min.js"></script>
<script src="https://unpkg.com/d3-graphviz@3.0.5/build/d3-graphviz.js"></script>
</head>
<body>
<div class="row">
<div class="sidebar">
<div class="sidebar-header">
<h1>Alpha Avoidance</h1>
<p>Master Thesis Project</p>
</div>
<div class="sidebar-content">
<form action="/" method="POST">
<div class="term-type">
<div class="term-type-option">
<input type="radio" id="typed" name="term-type" value="typed" {{'checked' if tt == 'typed' else ''}} onclick="termType('typed');">
<label for="typed">Typed</label>
</div>
<div class="term-type-option">
<input type="radio" id="untyped" name="term-type" value="untyped" {{'checked' if tt == 'untyped' else ''}} onclick="termType('untyped');">
<label for="untyped">Untyped</label>
</div>
</div>
<div id="typed-wrapper">
Context:
<br><input type="text" name="ctx" value="{{ctx}}">
Typed Term:
<br><input type="text" name="tterm" value="{{tterm}}" required>
</div>
<div id="untyped-wrapper">
Untyped Term:
<br><input type="text" name="term" value="{{term}}" required>
</div>
<!-- Term:
<br><input type="text" name="term" value="{{tterm}}" required> -->
<div class="grammars">
<ul class="grammar" id="untyped-grammar">
<li>UT = (UT) | /x ... y.UT | UT ... UT | x</li>
</ul>
<ul class="grammar" id="type-grammar">
<li>TYPE = 0 | TYPE -> TYPE</li>
</ul>
<ul class="grammar" id="ctx-grammar">
<li>CTX = _ | x^TYPE ... y^TYPE</li>
</ul>
<ul class="grammar" id="typed-grammar">
<li>TT = (TT) | /x^TYPE ... y^TYPE.TT | TT ... TT | x</li>
</ul>
</div>
Max depth:<br><input type="number" name="max_depth" value="{{max_depth}}" min="1" max="1000" placeholder="Max depth">
<input type="checkbox" name="simultaneous" {{'checked' if sim else ''}}> Simultaneous substitution
<button type="submit">Generate picture</button>
{% if error %}
<span style="color:#f55">{{ info }}</span>
{% endif %}
</form>
<ul>
{% for key in attrs.keys() %}
<li><b>{{key}}:</b> {{attrs[key]}}</li>
{% endfor %}
</ul>
</div>
<div class="footer">
<span>Samuel Frontull<br>supervised by Dr. Vincent van Oostrom</span>
</div>
</div>
<div class="content">
<div id="graph" style="text-align: center;"></div>
<div class="footer">
<p>Term: {{term}}</p>
</div>
</div>
<script>
var s = String("{{dot}}").replaceAll('&#34;','"').replaceAll('λ','/').replaceAll('&lt;','<').replaceAll('&gt;','>');
s = s.substring(1, s.length - 1);
console.log(s);
d3.select("#graph").graphviz().renderDot(s);
</script>
<button onclick="topFunction()" id="totop" title="Go to top">^</button>
<script>
function termType(type) {
a = ["untyped-grammar", "untyped-wrapper"];
b = ["typed-grammar", "typed-wrapper", "ctx-grammar", "type-grammar"];
if (type == "untyped") {
a.forEach(function(e) {
document.getElementById(e).style.display = "block";
});
b.forEach(function(e) {
document.getElementById(e).style.display = "none";
});
} else {
b.forEach(function(e) {
document.getElementById(e).style.display = "block";
});
a.forEach(function(e) {
document.getElementById(e).style.display = "none";
});
}
}
termType("{{tt}}");
</script>
<script>
//Get the button:
mybutton = document.getElementById("totop");
// When the user scrolls down 20px from the top of the document, show the button
window.onscroll = function() {scrollFunction()};
function scrollFunction() {
if (document.body.scrollTop > 20 || document.documentElement.scrollTop > 20) {
mybutton.style.display = "block";
} else {
mybutton.style.display = "none";
}
}
// When the user clicks on the button, scroll to the top of the document
function topFunction() {
document.body.scrollTop = 0; // For Safari
document.documentElement.scrollTop = 0; // For Chrome, Firefox, IE and Opera
}
</script>
</body>
</html>
from app import app
if __name__ == "__main__":
app.run()
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