Skip to content

GitLab

Commit 11c2509a authored by Valentin Blot's avatar Valentin Blot
Browse files

Javascript version

parent c083a425
Expand all Hide whitespace changes
Inline Side-by-side
Javascript/f.html 0 → 100755
View file @ 11c2509a
<!DOCTYPE html>
<html>
<head>
<meta charset=UTF-8>
<title>title</title>
<style>
@font-face
{
font-family: LMMath;
src: local(LatinModernMath-Regular), url(latinmodern-math.otf);
}
</style>
<script src=peg-0.9.0.min.js></script>
<script>
"use strict";
let Type = class
{
constructor(kind, arg1, arg2)
{
this.kind = kind;
if(kind === "var")
this.value = arg1;
if(kind === "abs")
this.term = arg1;
if(kind === "app")
{
this.term1 = arg1;
this.term2 = arg2;
}
}
lift(index = 0)
{
if(this.kind === "var")
if(this.value < index)
return new Type("var", this.value);
else
return new Type("var", this.value + 1);
if(this.kind === "abs")
return new Type("abs", this.term.lift(index + 1));
if(this.kind === "app")
return new Type("app", this.term1.lift(index), this.term2.lift(index));
}
subst(type, index = 0)
{
if(this.kind === "var")
if(this.value < index)
return new Type("var", this.value);
else if(this.value === index)
return type;
else
return new Type("var", this.value - 1);
if(this.kind === "abs")
return new Type("abs", this.term.subst(type.lift(), index + 1));
if(this.kind === "app")
return new Type("app", this.term1.subst(type, index), this.term2.subst(type, index));
}
}
let Term = class
{
constructor(kind, arg1, arg2)
{
this.kind = kind;
if(kind === "var")
this.value = arg1;
if(kind === "abs")
{
this.type = arg1;
this.term = arg2;
}
if(kind === "app")
{
this.term1 = arg1;
this.term2 = arg2;
}
if(kind === "tabs")
this.term = arg1;
if(kind === "tapp")
{
this.term1 = arg1;
this.term2 = arg2;
}
if(this.kind === "meta_var")
this.value = arg1;
if(this.kind === "meta_app")
{
this.term = arg1;
this.stack = arg2;
}
if(this.kind === "meta_subst")
{
this.term = arg1;
this.stack = arg2;
}
}
get_type(context = [])
{
if(this.kind === "var")
return context[this.value];
if(this.kind === "abs")
{
context.unshift(this.type);
let ret = this.term.get_type(context);
context.shift();
return new Type("app", this.type, ret);
}
if(this.kind === "app")
return this.term1.get_type(context).term2;
if(this.kind === "tabs")
{
context.map(t => t.lift());
let ret = this.term.get_type(context);
context.map(t => t.subst(new Type("var", 0)));
return new Type("abs", ret);
}
if(this.kind === "tapp")
return this.term1.get_type(context).term.subst(this.term2);
}
strip()
{
if(this.kind === "var")
return new Term("var", this.value);
if(this.kind === "abs")
return new Term("abs", this.type, this.term.strip());
if(this.kind === "app")
return new Term("app", this.term1.strip(), this.term2.strip());
if(this.kind === "tabs")
return this.term.strip();
if(this.kind === "tapp")
return this.term1.strip();
if(this.kind === "meta_var")
return new Term("meta_var", this.value);
if(this.kind === "meta_app")
return new Term("meta_app", this.term.strip(), this.stack);
if(this.kind === "meta_subst")
return new Term("meta_subst", this.term.strip(), this.stack instanceof Array ? this.stack.map(t => t.strip()) : this.stack);
}
lift(index = 0)
{
if(this.kind === "var")
if(this.value < index)
return new Term("var", this.value);
else
return new Term("var", this.value + 1);
if(this.kind === "abs")
return new Term("abs", this.type, this.term.lift(index + 1));
if(this.kind === "app")
return new Term("app", this.term1.lift(index), this.term2.lift(index));
}
subst(stack, index = 0)
{
if(this.kind === "var")
if(this.value < index)
return new Term("var", this.value);
else if(this.value < index + stack.length)
return stack[this.value - index];
else
return new Term("var", this.value - stack.length);
if(this.kind === "abs")
return new Term("abs", this.type, this.term.subst(stack.map(t => t.lift(), index + 1)));
if(this.kind === "app")
return new Term("app", this.term1.subst(stack, index), this.term2.subst(stack, index));
}
meta_lift(index = 0)
{
if(this.kind === "var")
return new Term("var", this.value);
if(this.kind === "abs")
return new Term("abs", this.type, this.term.meta_lift(index))
if(this.kind === "app")
return new Term("app", this.term1.meta_lift(index), this.term2.meta_lift(index));
if(this.kind === "meta_var")
if(this.value < index)
return new Term("meta_var", this.value);
else
return new Term("meta_var", this.value + 1);
if(this.kind === "meta_app")
return new Term("meta_app", this.term.meta_lift(index), this.stack.meta_lift(index))
if(this.kind === "meta_subst")
return new Term("meta_subst", this.term.meta_lift(index), this.stack instanceof Array ? this.stack.map(t => t.meta_lift(index)) : this.stack.meta_lift(index))
}
meta_subst(term, index = 0)
{
if(this.kind === "var")
return new Term("var", this.value);
if(this.kind === "abs")
return new Term("abs", this.type, this.term.meta_subst(term, index))
if(this.kind === "app")
return new Term("app", this.term1.meta_subst(term, index), this.term2.meta_subst(term, index));
if(this.kind === "meta_var")
if(this.value < index)
return new Term("meta_var", this.value);
else if(this.value === index)
return term;
else
return new Term("meta_var", this.value - 1);
if(this.kind === "meta_app")
return new Term("meta_app", this.term.meta_subst(term, index), this.stack.meta_subst(term, index))
if(this.kind === "meta_subst")
return new Term("meta_subst", this.term.meta_subst(term, index), this.stack instanceof Array ? this.stack.map(t => t.meta_subst(term, index)) : this.stack.meta_subst(term, index))
}
normalize()
{
if(this.kind === "var")
return new Term("var", this.value);
if(this.kind === "abs")
return new Term("abs", this.type, this.term.normalize())
if(this.kind === "app")
return new Term("app", this.term1.normalize(), this.term2.normalize());
if(this.kind === "meta_var")
throw "Error: trying to normalize an open term";
if(this.kind === "meta_app")
return this.stack.reduce((t, u) => new Term("app", t, u.normalize()), this.term.normalize());
if(this.kind === "meta_subst")
return this.term.normalize().subst(this.stack.map(t => t.normalize()));
}
static equal(term1, term2)
{
if(term1.kind !== term2.kind)
return false;
if(term1.kind === "var")
return term1.value === term2.value;
if(term1.kind === "abs")
return Term.equal(term1.term, term2.term);
if(term1.kind === "app")
return Term.equal(term1.term1, term2.term1) && Term.equal(term1.term2, term2.term2);
}
}
let Formula = class
{
constructor(kind, arg1, arg2)
{
this.kind = kind;
if(kind === "atom")
{
this.term = arg1;
this.set = arg2;
}
if(kind === "forall")
this.form = arg1;
if(kind === "forall2")
this.form = arg1;
if(kind === "impl")
{
this.form1 = arg1;
this.form2 = arg2;
}
if(kind === "conj")
this.forms = arg1;
if(kind === "other") {}
}
subst(term, index = 0)
{
if(this.kind === "atom")
return new Formula("atom", this.term.meta_subst(term, index), this.set);
if(this.kind === "forall")
return new Formula("forall", this.form.subst(term.meta_lift(), index + 1));
if(this.kind === "forall2")
return new Formula("forall2", this.form.subst(term, index));
if(this.kind === "impl")
return new Formula("impl", this.form1.subst(term, index), this.form2.subst(term, index));
if(this.kind === "conj")
return new Formula("conj", this.forms.map(f => f.subst(term, index)));
if(this.kind === "other")
return new Formula("other");
}
lift(index = 0)
{
if(this.kind === "atom")
return new Formula("atom", this.term.meta_lift(index), this.set);
if(this.kind === "forall")
return new Formula("forall", this.form.lift(index + 1));
if(this.kind === "forall2")
return new Formula("forall2", this.form.lift(index));
if(this.kind === "impl")
return new Formula("impl", this.form1.lift(index), this.form2.lift(index));
if(this.kind === "conj")
return new Formula("conj", this.forms.map(f => f.lift(index)));
if(this.kind === "other")
return new Formula("other");
}
lift2(index = 0)
{
if(this.kind === "atom")
if(this.set < index)
return new Formula("atom", this.term, this.set);
else
return new Formula("atom", this.term, this.set + 1);
if(this.kind === "forall")
return new Formula("forall", this.form.lift2(index));
if(this.kind === "forall2")
return new Formula("forall2", this.form.lift2(index + 1));
if(this.kind === "impl")
return new Formula("impl", this.form1.lift2(index), this.form2.lift2(index));
if(this.kind === "conj")
return new Formula("conj", this.forms.map(f => f.lift2(index)));
if(this.kind === "other")
return new Formula("other");
}
subst2(form, index = 0)
{
if(this.kind === "atom")
if(this.set < index)
return new Formula("atom", this.term, this.set);
else if(this.set === index)
return form.subst(this.term);
else
return new Formula("atom", this.term, this.set - 1);
if(this.kind === "forall")
return new Formula("forall", this.form.subst2(form, index));
if(this.kind === "forall2")
return new Formula("forall2", this.form.subst2(form.lift2(), index + 1));
if(this.kind === "impl")
return new Formula("impl", this.form1.subst2(form, index), this.form2.subst2(form, index));
if(this.kind === "conj")
return new Formula("conj", this.forms.map(formi => formi.subst2(form, index)));
if(this.kind === "other")
return new Formula("other");
}
}
let norm = new Formula("impl", new Formula("forall", new Formula("impl", new Formula("other"), new Formula("other"))), new Formula("other"));
let redcand = new Formula("conj", [
new Formula("forall", new Formula("atom", new Term("meta_app", new Term("var", 0), new Term("meta_var", 0)), 0)),
new Formula("forall", new Formula("impl", new Formula("atom", new Term("meta_var", 0), 0), norm)),
new Formula("forall", new Formula("forall", new Formula("forall", new Formula("impl", new Formula("atom", new Term("meta_app", new Term("meta_subst", new Term("meta_var", 2), [new Term("meta_var", 1)]), new Term("meta_var", 0)), 0), new Formula("atom", new Term("meta_app", new Term("app", new Term("abs", new Type("var", 0), new Term("meta_var", 2)), new Term("meta_var", 1)), new Term("meta_var", 0)), 0)))))]);
let rc = function(type)
{
if(type.kind === "var")
return new Formula("atom", new Term("meta_var", 0), type.value);
if(type.kind === "abs")
return new Formula("forall2", new Formula("impl", redcand, rc(type.term)));
if(type.kind === "app")
return new Formula("forall", new Formula("impl", rc(type.term1), rc(type.term2).subst(new Term("app", new Term("meta_var", 1), new Term("meta_var", 0)))));
}
let repl = function(real, form, index = 0)
{
if(form.kind === "atom")
if(form.set === index)
return real(form.term.normalize());
else
return [y => y, y => y];
if(form.kind === "forall")
{
let res = term => repl(real, form.form.subst(term), index);
return [y => term => res(term)[0](y(term)), y => term => res(term)[1](y(term))];
}
if(form.kind === "forall2")
return repl(real, form.form, index + 1);
if(form.kind === "impl")
{
let res1 = repl(real, form.form1, index);
let res2 = repl(real, form.form2, index);
return [y => z => res2[0](y(res1[1](z))), y => z => res2[1](y(res1[0](z)))];
}
if(form.kind === "conj")
{
let res = form.forms.map(formi => repl(real, formi, index));
return [y => res.map((resi, i) => resi[0](y[i])), y => res.map((resi, i) => resi[1](y[i]))];
}
if(form.kind === "other")
return [y => y, y => y];
}
let brec = f => g => s => g(x => s(x) === null ? f(y => brec(f)(g)(z => Term.equal(z, x) ? y : s(z))) : s(x));
let dne = function(form)
{
if(form.kind === "atom")
return x => x(y => y);
if(form.kind === "forall")
return x => y => dne(form.form)(z => x(u => z(u(y))));
if(form.kind === "forall2")
return dne(form.form);
if(form.kind === "impl")
return x => y => dne(form.form2)(z => x(u => z(u(y))));
if(form.kind === "conj")
return x => form.forms.map((formi, i) => dne(formi)(y => x(z => y(z[i]))));
if(form.kind === "other")
return x => x(y => y);
}
let exf = function(form)
{
return x => dne(form)(y => x);
}
let comp = function(form)
{
return y => brec(x => exf(new Formula("conj", [new Formula("impl", new Formula("atom", new Term("var", 0), 0), form), new Formula("impl", form, new Formula("atom", new Term("var", 0), 0))]))(x([exf(form), u => x([z => u, z => 0])])))(y)(x => null)
}
let elim = function(form1, form2)
{
return x => dne(form1.subst2(form2))(y => comp(form2)(z => y(repl(z, form1)[0](x))));
}
let normrc = [p => x => x(0)(null), t => x => x, t => u => p => x => y => x(i => y(i + 1))];
let isrc = function(type, context = [])
{
if(type.kind === "var")
return context[type.value];
if(type.kind === "abs")
return [
p => x => isrc(type.term, [x, ...context])[0](p),
t => x => elim(new Formula("impl", redcand, new Formula("forall", new Formula("impl", rc(type.term), norm))), norm)(x => isrc(type.term, [x, ...context])[1])(normrc)(t)(elim(new Formula("impl", redcand, rc(type.term).subst(t)), norm)(x)(normrc)),
t => u => p => y => x => isrc(type.term, [x, ...context])[2](t)(u)(p)(y(x))];
if(type.kind === "app")
return [
p => t => x => isrc(type.term2, context)[0]([...p, t]),
t => x => isrc(type.term2, context)[1](new Term("app", t, new Term("var", 0)))(x(new Term("var", 0))(isrc(type.term1, context)[0]([]))),
t => u => p => x => v => y => isrc(type.term2, context)[2](t)(u)([...p, v])(x(v)(y))];
}
let adeq = function(term, context = [], tcontext = [])
{
if(term.kind === "var")
return context[term.value][1];
if(term.kind === "abs")
return t => y => isrc(term.term.get_type([term.type, ...context.map(p => p[2])]), tcontext)[2](term.term.strip().normalize().subst(context.map(p => p[0].normalize().lift()), 1))(t)([])(adeq(term.term, [[t, y, term.type], ...context], tcontext));
if(term.kind === "app")
return adeq(term.term1, context, tcontext)(term.term2.strip().normalize().subst(context.map(p => p[0])))(adeq(term.term2, context, tcontext));
if(term.kind === "tabs")
return x => adeq(term.term, context.map(p => [p[0], p[1].lift(), p[2]]), [x, ...tcontext]);
if(term.kind === "tapp")
return elim(new Formula("impl", redcand, rc(term.term1.get_type(context.map(p => p[2])).term).subst(new Term("meta_subst", term.term1.strip(), context.map(p => p[0])))), rc(term.term2))(adeq(term.term1, context, tcontext))(isrc(term.term2, tcontext));
}
let term;
let node_clear = function(node)
{
while(node.hasChildNodes())
node.removeChild(node.firstChild);
}
let parse = function()
{
node_clear(document.getElementById("parse_alert"));
try
{
term = PEG.buildParser(`
{
let context = [];
let tcontext = [];
}
term =
abs
/
app:app {return app.reduce((ret, val) => val instanceof Term ? new Term("app", ret, val) : new Term("tapp", ret, val))}
abs =
[λ\\\\] var_id:var_id ":" type:type "." term:term
{
context.shift();
return new Term("abs", type, term);
}
/
[λ\\\\] tvar_id:tvar_id "." term:term
{
tcontext.shift();
return new Term("tabs", term);
}
var_id =
id:[a-z]
{
context.unshift(id);
return id;
}
tvar_id =
id:[A-Z]
{
tcontext.unshift(id);
return id;
}
app =
arg:arg app:app {app.unshift(arg); return app}
/
last_arg:last_arg {return [last_arg]}
/
targ:targ app:app {app.unshift(targ); return app}
/
last_targ:last_targ {return [last_targ]}
arg =
id:[a-z] {return new Term('var', context.findIndex(val => val === id))}
/
"(" term:term ")" {return term}
last_arg =
arg
/
abs
targ =
id:[A-Z] {return new Type('var', tcontext.findIndex(val => val === id))}
/
"(" type:type ")" {return type}
last_targ =
targ
/
tabs
type =
tabs
/
tapp:tapp {return tapp.reduce((ret, val) => new Type("app", ret, val))}
tabs =
[∀\\\^] tvar_list:tvar_list "." type:type
{
let ret = type;
for(let id of tvar_list)
{
tcontext.shift();
ret = new Type("abs", ret);
}
return ret;
}
tvar_list =
tvar_ids:[A-Z]+
{
for(let id of tvar_ids)
tcontext.unshift(id);
return tvar_ids;
}
tapp =
targ:targ tapp:tapp {tapp.unshift(targ); return tapp}
/
last_targ:last_targ {return [last_targ]}
`).parse(document.getElementById("type_txt").value);
document.getElementById("parse_alert").appendChild(document.createTextNode(isrc(term.get_type())[1](term.strip())(adeq(term))(x => y => x)));
}
catch(e)
{
if(e.constructor.id === "peg$SyntaxError")
{
document.getElementById("parse_alert").appendChild(document.createTextNode(e.id + " at characters [" + e.location.start.column + "-" + e.location.end.column + "]: " + e.message));
return;
}
throw e;
}
}
</script>
</head>
<body>
<div>
<input type=text id=type_txt size=100 onkeypress=if(event.which===13){parse()} />
<input type=button value=Parse onclick=parse() />
<span id=parse_alert style=color:red ></span>
</div>
<div style=font-style:italic>(you can use "\" instead of "λ" and "^" instead of "∀")</div>
<br/>
<div>
<span style=vertical-align:top>Examples:</span>
<div style=display:inline-block>
<div>λX.λY.λZ.λx:XYZ.λy:XY.λz:X.xz(yz)</div>
<div>λX.λY.λZ.λx:XYZ.λy:XY.λz:X.(λu:Z.xzu)(yz)</div>
<div>λX.λf:XX.λx:X.f(fx)</div>
<div>λX.(λY.λf:YY.λx:Y.f(fx))(XX)((λY.λf:YY.λx:Y.f(fx))X)</div>
<div>λX.λx:X.x</div>
<div>λx:(∀X.XX).x(∀X.XX)x</div>
<div>(λx:(∀X.XX).x(∀X.XX)x)λX.λx:X.x</div>
<div>λx:(∀X.XX).x(∀X.XX)x(∀X.XX)x</div>
<div>(λx:(∀X.XX).x(∀X.XX)x(∀X.XX)x)λX.λx:X.x</div>
</div>
</div>
</body>
</html>
Javascript/peg-0.9.0.min.js 0 → 100755
View file @ 11c2509a
This diff is collapsed.
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