ok implemented most of the typing rules
This commit is contained in:
parent
809c25c8bc
commit
f91029c107
34 changed files with 314 additions and 2645 deletions
47
Cargo.lock
generated
47
Cargo.lock
generated
|
|
@ -22,6 +22,7 @@ dependencies = [
|
|||
"im",
|
||||
"lazy_static",
|
||||
"parking_lot",
|
||||
"trace",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
|
|
@ -104,6 +105,24 @@ dependencies = [
|
|||
"windows-targets",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "1.0.69"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "134c189feb4956b20f6f547d2cf727d4c0fe06722b20a0eec87ed445a97f92da"
|
||||
dependencies = [
|
||||
"unicode-ident",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "quote"
|
||||
version = "1.0.33"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5267fca4496028628a95160fc423a33e8b2e6af8a5302579e322e4b520293cae"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_core"
|
||||
version = "0.6.4"
|
||||
|
|
@ -150,12 +169,40 @@ version = "1.11.1"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "942b4a808e05215192e39f4ab80813e599068285906cc91aa64f923db842bd5a"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "1.0.109"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"unicode-ident",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "trace"
|
||||
version = "0.1.7"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9ad0c048e114d19d1140662762bfdb10682f3bc806d8be18af846600214dd9af"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "typenum"
|
||||
version = "1.17.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
|
||||
|
||||
[[package]]
|
||||
name = "unicode-ident"
|
||||
version = "1.0.12"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.9.4"
|
||||
|
|
|
|||
|
|
@ -1,17 +0,0 @@
|
|||
open Jest
|
||||
open Belt
|
||||
open Data
|
||||
open Bidir
|
||||
|
||||
open Expect
|
||||
open! Expect.Operators
|
||||
|
||||
let mapFirst = a => a->Result.map(((x, _)) => x)
|
||||
|
||||
test("id", () => {
|
||||
let id: term = Lam("x", Var("x"))
|
||||
let ctx = list{}
|
||||
let typ = synthesize(ctx, id)->mapFirst
|
||||
Js.Console.error2("output: ", typ)
|
||||
expect(typ) === Ok(TPolytype("ex0", TArrow(TVar("ex0"), TVar("ex0"))))
|
||||
})
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
module.exports = {
|
||||
presets: [
|
||||
[
|
||||
"@babel/preset-env",
|
||||
{ targets: { node: "current", esmodules: false }, modules: "cjs" },
|
||||
],
|
||||
],
|
||||
plugins: [],
|
||||
};
|
||||
|
|
@ -1,3 +1,30 @@
|
|||
#import "@preview/prooftrees:0.1.0": *
|
||||
#let synth = text(red, sym.arrow.double.r)
|
||||
#let tyck = text(blue, sym.arrow.double.l)
|
||||
|
||||
= Ideas
|
||||
|
||||
- Compared to Hindley-Milner type systems, this bidirectional system still serves a lot of similar purposes:
|
||||
- Rather than collecting and unifying variables, we have input and output contexts
|
||||
- Rather than having special unification rules for polymorphic variables, we use existential variables in the context and solve them using subtyping
|
||||
|
||||
= Expressions
|
||||
|
||||
- $ id : forall a. a arrow.r a $
|
||||
- $ id &: forall a. a arrow.r a \
|
||||
id &= lambda x . x $
|
||||
|
||||
The typing rules should be:
|
||||
|
||||
- Apply $arrow.r"I"synth$
|
||||
|
||||
#tree(
|
||||
axi[$Gamma, hat(alpha), hat(beta), x : hat(alpha) tack.r e tyck hat(beta) tack.l Delta, x : hat(alpha), Theta $],
|
||||
uni[$Gamma tack.r lambda x.e synth hat(alpha) arrow.r hat(beta) tack.l Delta$]
|
||||
)
|
||||
|
||||
Get $Gamma, hat(alpha), hat(beta), x : hat(alpha) tack.r x tyck hat(beta) tack.l Delta , x : hat(alpha), Theta$
|
||||
|
||||
= Open Questions
|
||||
|
||||
- Why is subtyping critical to this type system? What would happen without it?
|
||||
- $Gamma_0 [hat(beta) = hat(alpha)]$ is listed as a type of instantiation but isn't one of the types of contexts defined. How are they allowed to do this?
|
||||
|
|
@ -10,3 +10,4 @@ anyhow = "1.0.75"
|
|||
im = "15.1.0"
|
||||
lazy_static = "1.4.0"
|
||||
parking_lot = "0.12.1"
|
||||
trace = "0.1.7"
|
||||
|
|
|
|||
|
|
@ -1,26 +1,38 @@
|
|||
use anyhow::{bail, Result};
|
||||
|
||||
use crate::DEPTH;
|
||||
|
||||
use crate::data::FreeVar;
|
||||
use crate::{
|
||||
data::{ctx_lookup_type, Context, ContextEntry, Term, Type},
|
||||
data::{Context, ContextEntry, Term, Type},
|
||||
gensym::gensym_prefix,
|
||||
};
|
||||
|
||||
// Figure 8. Applying a context, as a substitution, to a type
|
||||
|
||||
pub fn app_ctx(ctx: &Context, ty: &Type) -> Type {
|
||||
#[trace]
|
||||
pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
|
||||
match ty {
|
||||
Type::Existential(_) => todo!(),
|
||||
Type::Existential(a) => match ctx.lookup_existential(a) {
|
||||
Some(Some(m)) => Ok(m.into_poly()),
|
||||
Some(None) => Ok(Type::Existential(a.clone())),
|
||||
None => bail!("existential variable {a} doesn't exist in context"),
|
||||
},
|
||||
|
||||
Type::Polytype(_, _) => todo!(),
|
||||
Type::Arrow(a, b) => Type::Arrow(Box::new(app_ctx(ctx, a)), Box::new(app_ctx(ctx, b))),
|
||||
_ => ty.clone(),
|
||||
Type::Arrow(a, b) => Ok(Type::Arrow(
|
||||
Box::new(app_ctx(ctx, a)?),
|
||||
Box::new(app_ctx(ctx, b)?),
|
||||
)),
|
||||
_ => todo!("shiiet"),
|
||||
}
|
||||
}
|
||||
|
||||
// Figure 9. Algorithmic subtyping
|
||||
|
||||
/// Under input context Γ , type A is a subtype of B, with output context ∆
|
||||
#[trace]
|
||||
pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
|
||||
println!("subtype(ctx = {ctx:?}, a = {a:?}, b = {b:?})");
|
||||
match (a, b) {
|
||||
// <:Unit rule
|
||||
(Type::Unit, Type::Unit) => Ok(ctx.clone()),
|
||||
|
|
@ -28,19 +40,32 @@ pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
|
|||
// <:Var rule
|
||||
(Type::Var(x), Type::Var(y)) if x == y => {
|
||||
// Ensure that the name exists in the context
|
||||
if !ctx.iter().any(|entry| match entry {
|
||||
ContextEntry::ExistentialVar(z) if x == z => true,
|
||||
_ => false,
|
||||
}) {
|
||||
if ctx.lookup_type(x).is_none() {
|
||||
bail!("name {x} not in context");
|
||||
}
|
||||
|
||||
Ok(ctx.clone())
|
||||
}
|
||||
|
||||
// <:Exvar rule
|
||||
(Type::Existential(x), Type::Existential(y)) if x == y => {
|
||||
// Ensure that the name exists in the context
|
||||
if ctx.lookup_existential(x).is_none() {
|
||||
bail!("name {x} not in context");
|
||||
}
|
||||
|
||||
Ok(ctx.clone())
|
||||
}
|
||||
|
||||
(Type::Existential(a), ty_a)
|
||||
if !b.free_vars().contains(&FreeVar::Existential(a.to_string()))
|
||||
&& ctx.lookup_existential(a).is_some() =>
|
||||
{
|
||||
let ctx_delta = instantiate_left(ctx, a, ty_a)?;
|
||||
Ok(ctx_delta)
|
||||
}
|
||||
(Type::Existential(_), Type::Unit) => todo!(),
|
||||
(Type::Existential(_), Type::Var(_)) => todo!(),
|
||||
(Type::Existential(_), Type::Existential(_)) => todo!(),
|
||||
(Type::Existential(_), Type::Polytype(_, _)) => todo!(),
|
||||
(Type::Existential(_), Type::Arrow(_, _)) => todo!(),
|
||||
(Type::Polytype(_, _), Type::Unit) => todo!(),
|
||||
|
|
@ -54,16 +79,33 @@ pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
|
|||
(Type::Arrow(_, _), Type::Polytype(_, _)) => todo!(),
|
||||
(Type::Arrow(_, _), Type::Arrow(_, _)) => todo!(),
|
||||
|
||||
_ => bail!("subtyping relation failed"),
|
||||
_ => bail!("subtyping relation failed between {a:?} and {b:?} (ctx = {ctx:?})"),
|
||||
}
|
||||
}
|
||||
|
||||
// Figure 10. Instantiation
|
||||
|
||||
#[trace]
|
||||
pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result<Context> {
|
||||
match ty_a {
|
||||
// InstLReach rule
|
||||
Type::Existential(b) if ctx.has_existential(a) && ctx.has_existential(b) => {
|
||||
// TODO: WTF?
|
||||
todo!()
|
||||
}
|
||||
Type::Existential(b) => todo!(),
|
||||
|
||||
Type::Unit => todo!(),
|
||||
Type::Var(_) => todo!(),
|
||||
Type::Polytype(_, _) => todo!(),
|
||||
Type::Arrow(_, _) => todo!(),
|
||||
}
|
||||
}
|
||||
|
||||
// Figure 11. Algorithmic typing
|
||||
|
||||
#[trace]
|
||||
pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
|
||||
println!("typecheck(ctx = {ctx:?}, term = {term:?}, ty = {ty:?})");
|
||||
match (term, ty) {
|
||||
// 1I rule
|
||||
(Term::Unit, Type::Unit) => Ok(ctx.clone()),
|
||||
|
|
@ -80,20 +122,20 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
|
|||
// Sub rule
|
||||
(term, ty) => {
|
||||
let (ty_a, ctx_theta) = synthesize(ctx, term)?;
|
||||
let a = app_ctx(&ctx_theta, &ty_a);
|
||||
let b = app_ctx(&ctx_theta, ty);
|
||||
let a = app_ctx(&ctx_theta, &ty_a)?;
|
||||
let b = app_ctx(&ctx_theta, ty)?;
|
||||
let ctx_delta = subtype(&ctx_theta, &a, &b)?;
|
||||
Ok(ctx_delta)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[trace]
|
||||
pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
|
||||
println!("synthesize(ctx = {ctx:?}, term = {term:?}");
|
||||
match term {
|
||||
// Var rule
|
||||
Term::Var(name) => {
|
||||
let ty = match ctx_lookup_type(ctx, name) {
|
||||
let ty = match ctx.lookup_type(name) {
|
||||
Some(v) => v,
|
||||
None => bail!("could not find name {name}"),
|
||||
};
|
||||
|
|
@ -104,31 +146,61 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
|
|||
Term::Unit => Ok((Type::Unit, ctx.clone())),
|
||||
|
||||
// Anno rule
|
||||
Term::Annot(_, _) => todo!(),
|
||||
Term::Annot(e, ty_a) => {
|
||||
// Make sure the type is well formed
|
||||
// TODO: Have an actual "well-formed" check
|
||||
|
||||
let ctx_delta = typecheck(ctx, &e, ty_a)?;
|
||||
Ok((ty_a.clone(), ctx_delta))
|
||||
}
|
||||
|
||||
// →I⇒ rule
|
||||
// > Rule →I⇒ corresponds to Decl→I⇒, one of the guessing rules, so we
|
||||
// > create new existential variables ^α (for the function domain) and ^β (for
|
||||
// > the codomain) and check the function body against ^β. As in ∀App, we do
|
||||
// > not place a marker before ^α, because ^α and ^β appear in the output type
|
||||
// > (λx. e ⇒ ^α → ^β).
|
||||
Term::Lam(x, e) => {
|
||||
let mut aug_ctx = ctx.clone();
|
||||
let ex_a = gensym_prefix("ex");
|
||||
let ex_b = gensym_prefix("ex");
|
||||
aug_ctx.push_back(ContextEntry::TypeVar(ex_a.clone()));
|
||||
aug_ctx.push_back(ContextEntry::TypeVar(ex_b.clone()));
|
||||
aug_ctx.push_back(ContextEntry::TermAnnot(x.clone(), Type::Var(ex_a.clone())));
|
||||
let ex_a_s = gensym_prefix("ex");
|
||||
let ex_b_s = gensym_prefix("ex");
|
||||
let ex_a = Type::Existential(ex_a_s.clone());
|
||||
let ex_b = Type::Existential(ex_b_s.clone());
|
||||
let aug_ctx = ctx.add(vec![
|
||||
ContextEntry::ExistentialVar(ex_a_s.clone()),
|
||||
ContextEntry::ExistentialVar(ex_b_s.clone()),
|
||||
ContextEntry::TermAnnot(x.clone(), ex_a.clone()),
|
||||
]);
|
||||
|
||||
let res = typecheck(&aug_ctx, &e, &Type::Var(ex_b.clone()));
|
||||
Ok((
|
||||
Type::Arrow(
|
||||
Box::new(Type::Existential(ex_a)),
|
||||
Box::new(Type::Existential(ex_b)),
|
||||
),
|
||||
ctx.clone(),
|
||||
))
|
||||
let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
|
||||
println!("the wtf ctx is {wtf_ctx:?}");
|
||||
Ok((Type::Arrow(Box::new(ex_a), Box::new(ex_b)), ctx.clone()))
|
||||
}
|
||||
|
||||
// →E rule
|
||||
Term::App(e1, e2) => {
|
||||
let (tyA, out_ctx) = synthesize(ctx, e1)?;
|
||||
todo!()
|
||||
let (ty_a, ctx_theta) = synthesize(ctx, e1)?;
|
||||
let app_a = app_ctx(&ctx_theta, &ty_a)?;
|
||||
let (ty_c, ctx_delta) = app_synthesize(&ctx_theta, &app_a, &e2)?;
|
||||
Ok((ty_c, ctx_delta))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[trace]
|
||||
pub fn app_synthesize(ctx: &Context, fun_ty: &Type, term: &Term) -> Result<(Type, Context)> {
|
||||
match (fun_ty, term) {
|
||||
// →App rule
|
||||
(Type::Arrow(ty_a, ty_c), e) => {
|
||||
typecheck(ctx, e, ty_a)?;
|
||||
Ok((*ty_c.clone(), ctx.clone()))
|
||||
}
|
||||
|
||||
// ∀App rule
|
||||
(Type::Polytype(_, _), _) => todo!(),
|
||||
|
||||
// âApp rule
|
||||
(Type::Existential(_), _) => todo!(),
|
||||
|
||||
_ => bail!("trying to appSynthesize with a non-function type"),
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,6 @@
|
|||
use im::Vector;
|
||||
use std::hash::Hash;
|
||||
|
||||
use im::{HashSet, Vector};
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum Term {
|
||||
|
|
@ -18,6 +20,57 @@ pub enum Type {
|
|||
Arrow(Box<Type>, Box<Type>),
|
||||
}
|
||||
|
||||
impl Type {
|
||||
pub fn into_mono(&self) -> Option<Monotype> {
|
||||
match self {
|
||||
Type::Unit => Some(Monotype::Unit),
|
||||
Type::Var(x) => Some(Monotype::Var(x.clone())),
|
||||
Type::Existential(x) => Some(Monotype::Existential(x.clone())),
|
||||
Type::Polytype(_, _) => None,
|
||||
Type::Arrow(a, b) => Some(Monotype::Arrow(
|
||||
Box::new(a.into_mono()?),
|
||||
Box::new(b.into_mono()?),
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn is_mono(&self) -> bool {
|
||||
self.into_mono().is_some()
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||
pub enum FreeVar {
|
||||
Var(String),
|
||||
Existential(String),
|
||||
}
|
||||
|
||||
impl Type {
|
||||
pub fn free_vars(&self) -> HashSet<FreeVar> {
|
||||
fn free_vars_with_context(ctx: &Context, ty: &Type) -> HashSet<FreeVar> {
|
||||
match ty {
|
||||
Type::Unit => HashSet::default(),
|
||||
Type::Var(x) if ctx.lookup_type(x).is_some() => HashSet::default(),
|
||||
Type::Var(x) => [FreeVar::Var(x.to_owned())].into_iter().collect(),
|
||||
Type::Existential(x) if ctx.lookup_existential(x).is_some() => HashSet::default(),
|
||||
Type::Existential(x) => [FreeVar::Existential(x.to_owned())].into_iter().collect(),
|
||||
Type::Polytype(x, ty_a) => {
|
||||
let new_ctx = ctx.add(vec![ContextEntry::ExistentialVar(x.to_owned())]);
|
||||
free_vars_with_context(&new_ctx, &ty_a)
|
||||
}
|
||||
Type::Arrow(ty_a, ty_b) => {
|
||||
let a_vars = free_vars_with_context(&ctx, &ty_a);
|
||||
let b_vars = free_vars_with_context(&ctx, &ty_b);
|
||||
a_vars.union(b_vars)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
free_vars_with_context(&Context::default(), self)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum Monotype {
|
||||
Unit,
|
||||
|
|
@ -26,7 +79,16 @@ pub enum Monotype {
|
|||
Arrow(Box<Monotype>, Box<Monotype>),
|
||||
}
|
||||
|
||||
pub type Context = Vector<ContextEntry>;
|
||||
impl Monotype {
|
||||
pub fn into_poly(&self) -> Type {
|
||||
match self {
|
||||
Monotype::Unit => Type::Unit,
|
||||
Monotype::Var(x) => Type::Var(x.clone()),
|
||||
Monotype::Existential(x) => Type::Existential(x.clone()),
|
||||
Monotype::Arrow(a, b) => Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly())),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum ContextEntry {
|
||||
|
|
@ -45,9 +107,45 @@ pub enum CompleteContextEntry {
|
|||
Marker(String),
|
||||
}
|
||||
|
||||
pub fn ctx_lookup_type(ctx: &Context, name: impl AsRef<str>) -> Option<Type> {
|
||||
ctx.iter().find_map(|entry| match entry {
|
||||
#[derive(Debug, Clone, Default)]
|
||||
pub struct Context(Vector<ContextEntry>);
|
||||
|
||||
impl Context {
|
||||
pub fn add(&self, entries: Vec<ContextEntry>) -> Context {
|
||||
let mut new_ctx = self.clone();
|
||||
for entry in entries {
|
||||
new_ctx.0.push_back(entry);
|
||||
}
|
||||
new_ctx
|
||||
}
|
||||
|
||||
/// Looks up a polytype by name
|
||||
pub fn lookup_type(&self, name: impl AsRef<str>) -> Option<Type> {
|
||||
self.0.iter().find_map(|entry| match entry {
|
||||
ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some(t.clone()),
|
||||
_ => None,
|
||||
})
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn has_type(&self, name: impl AsRef<str>) -> bool {
|
||||
self.lookup_type(name).is_some()
|
||||
}
|
||||
|
||||
/// Looks up an existential variable by name
|
||||
/// - Returns Some(Some(t)) if solved
|
||||
/// - Returns Some(None) if exists but unsolved
|
||||
/// - Returns None if not found
|
||||
pub fn lookup_existential(&self, name: impl AsRef<str>) -> Option<Option<Monotype>> {
|
||||
self.0.iter().find_map(|entry| match entry {
|
||||
ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some(None),
|
||||
ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some(Some(t.clone())),
|
||||
_ => None,
|
||||
})
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn has_existential(&self, name: impl AsRef<str>) -> bool {
|
||||
self.lookup_existential(name).is_some()
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,3 +1,8 @@
|
|||
#[macro_use]
|
||||
extern crate trace;
|
||||
|
||||
trace::init_depth_var!();
|
||||
|
||||
mod bidir;
|
||||
mod data;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,13 +1,29 @@
|
|||
use anyhow::{bail, Result};
|
||||
use im::Vector;
|
||||
|
||||
use crate::{bidir::synthesize, data::Term};
|
||||
use crate::{
|
||||
bidir::synthesize,
|
||||
data::{Context, Term},
|
||||
};
|
||||
|
||||
macro_rules! id_term {
|
||||
() => {
|
||||
Term::Lam("x".to_owned(), Box::new(Term::Var("x".to_owned())))
|
||||
};
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_id() -> Result<()> {
|
||||
let id = Term::Lam("x".to_owned(), Box::new(Term::Var("x".to_owned())));
|
||||
let ctx = Vector::new();
|
||||
let (ty, out_ctx) = synthesize(&ctx, &id)?;
|
||||
// bail!("Output: {ty:?} in context {out_ctx:?}");
|
||||
let id = id_term!();
|
||||
let ctx = Context::default();
|
||||
bail!("Result: {:?}", synthesize(&ctx, &id));
|
||||
Ok(())
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_id_of_unit() -> Result<()> {
|
||||
let id = id_term!();
|
||||
let id_of_unit = Term::App(Box::new(id), Box::new(Term::Unit));
|
||||
let ctx = Context::default();
|
||||
bail!("Result: {:?}", synthesize(&ctx, &id_of_unit));
|
||||
Ok(())
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,17 +0,0 @@
|
|||
{
|
||||
"name": "your-project-name",
|
||||
"bsc-flags": [],
|
||||
"sources": [
|
||||
{ "dir": "src", "subdirs": true },
|
||||
{ "dir": "__tests__", "subdirs": true, "type": "dev" }
|
||||
],
|
||||
"package-specs": [
|
||||
{
|
||||
"module": "commonjs",
|
||||
"in-source": true
|
||||
}
|
||||
],
|
||||
"suffix": ".bs.js",
|
||||
"bs-dependencies": [],
|
||||
"bs-dev-dependencies": ["@glennsl/bs-jest"]
|
||||
}
|
||||
BIN
bun.lockb
BIN
bun.lockb
Binary file not shown.
|
|
@ -1,10 +0,0 @@
|
|||
{
|
||||
"verbose": true,
|
||||
"moduleFileExtensions": ["js", "mjs"],
|
||||
"extensionsToTreatAsEsm": [".bs.mjs"],
|
||||
"testMatch": ["**/__tests__/**/*_test.mjs", "**/__tests__/**/*_test.bs.js"],
|
||||
"transform": {
|
||||
"^.+.m?js$": "babel-jest"
|
||||
},
|
||||
"transformIgnorePatterns": ["node_modules/(?!(rescript)/)"]
|
||||
}
|
||||
14
package.json
14
package.json
|
|
@ -1,14 +0,0 @@
|
|||
{
|
||||
"scripts": {
|
||||
"res:build": "rescript",
|
||||
"res:dev": "rescript build -w",
|
||||
"test": "retest lib/**/*.mjs"
|
||||
},
|
||||
"devDependencies": {
|
||||
"@glennsl/bs-jest": "^0.7.0",
|
||||
"jest": "^29.7.0",
|
||||
"rescript": "^10.1.4",
|
||||
"rescript-js": "^1.0.0-beta.2",
|
||||
"rescript-test": "^5.0.0"
|
||||
}
|
||||
}
|
||||
30
pmltt-lang/.gitignore
vendored
30
pmltt-lang/.gitignore
vendored
|
|
@ -1,30 +0,0 @@
|
|||
# Logs
|
||||
logs
|
||||
*.log
|
||||
npm-debug.log*
|
||||
yarn-debug.log*
|
||||
yarn-error.log*
|
||||
pnpm-debug.log*
|
||||
lerna-debug.log*
|
||||
|
||||
node_modules
|
||||
dist
|
||||
dist-ssr
|
||||
*.local
|
||||
|
||||
# Editor directories and files
|
||||
.vscode/*
|
||||
!.vscode/extensions.json
|
||||
.idea
|
||||
.DS_Store
|
||||
*.suo
|
||||
*.ntvs*
|
||||
*.njsproj
|
||||
*.sln
|
||||
*.sw?
|
||||
|
||||
# ReScript
|
||||
/lib/
|
||||
.bsb.lock
|
||||
.merlin
|
||||
*.bs.mjs
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
# ReScript / Vite Starter Template
|
||||
|
||||
This is a Vite-based template with following setup:
|
||||
|
||||
- [ReScript](https://rescript-lang.org) 10.1 with @rescript/react and JSX 4 automatic mode
|
||||
- ES6 modules (ReScript code compiled to `.bs.mjs` files)
|
||||
- Vite 4 with React Plugin (Fast Refresh)
|
||||
- Tailwind 3
|
||||
|
||||
## Development
|
||||
|
||||
Run ReScript in dev mode:
|
||||
|
||||
```sh
|
||||
npm run res:dev
|
||||
```
|
||||
|
||||
In another tab, run the Vite dev server:
|
||||
|
||||
```sh
|
||||
npm run dev
|
||||
```
|
||||
|
||||
## Tips
|
||||
|
||||
### Fast Refresh & ReScript
|
||||
|
||||
Make sure to create interface files (`.resi`) for each `*.res` file.
|
||||
|
||||
Fast Refresh requires you to **only export React components**, and it's easy to unintenionally export other values that will disable Fast Refresh (you will see a message in the browser console whenever this happens).
|
||||
|
||||
### Why are the generated `.bs.mjs` files tracked in git?
|
||||
|
||||
In ReScript, it's a good habit to keep track of the actual JS output the compiler emits. It allows quick sanity checking if we made any changes that actually have an impact on the resulting JS code (especially when doing major compiler upgrades, it's a good way to verify if production code will behave the same way as before the upgrade).
|
||||
|
||||
This will also make it easier for your Non-ReScript coworkers to read and understand the changes in Github PRs, and call you out when you are writing inefficient code.
|
||||
|
||||
If you want to opt-out, feel free to remove all compiled `.mjs` files within the `src` directory and add `src/**/*.mjs` in your `.gitignore`.
|
||||
|
|
@ -1,27 +0,0 @@
|
|||
{
|
||||
"name": "pmltt-lang",
|
||||
"sources": [
|
||||
{
|
||||
"dir": "src",
|
||||
"subdirs": true
|
||||
}
|
||||
],
|
||||
"package-specs": [
|
||||
{
|
||||
"module": "es6",
|
||||
"in-source": true
|
||||
}
|
||||
],
|
||||
"suffix": ".bs.mjs",
|
||||
"bs-dependencies": [
|
||||
"@rescript/react",
|
||||
"@rescript/core"
|
||||
],
|
||||
"jsx": {
|
||||
"version": 4,
|
||||
"mode": "automatic"
|
||||
},
|
||||
"bsc-flags": [
|
||||
"-open RescriptCore"
|
||||
]
|
||||
}
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
<!DOCTYPE html>
|
||||
<html lang="en">
|
||||
|
||||
<head>
|
||||
<meta charset="UTF-8" />
|
||||
<link rel="icon" type="image/svg+xml" href="/vite.svg" />
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
|
||||
<title>ReScript + Vite + React</title>
|
||||
</head>
|
||||
|
||||
<body>
|
||||
<div id="root"></div>
|
||||
<script type="module" src="/src/Main.bs.mjs"></script>
|
||||
</body>
|
||||
|
||||
</html>
|
||||
2226
pmltt-lang/package-lock.json
generated
2226
pmltt-lang/package-lock.json
generated
File diff suppressed because it is too large
Load diff
|
|
@ -1,28 +0,0 @@
|
|||
{
|
||||
"name": "pmltt-lang",
|
||||
"private": true,
|
||||
"version": "0.0.0",
|
||||
"type": "module",
|
||||
"scripts": {
|
||||
"res:build": "rescript",
|
||||
"res:clean": "rescript clean",
|
||||
"res:dev": "rescript build -w",
|
||||
"dev": "vite",
|
||||
"build": "vite build",
|
||||
"preview": "vite preview"
|
||||
},
|
||||
"dependencies": {
|
||||
"@rescript/core": "^0.5.0",
|
||||
"@rescript/react": "^0.11.0",
|
||||
"react": "^18.2.0",
|
||||
"react-dom": "^18.2.0",
|
||||
"rescript": "10.1"
|
||||
},
|
||||
"devDependencies": {
|
||||
"@vitejs/plugin-react": "4.0.0",
|
||||
"autoprefixer": "^10.4.15",
|
||||
"postcss": "^8.4.28",
|
||||
"tailwindcss": "^3.3.3",
|
||||
"vite": "^4.4.9"
|
||||
}
|
||||
}
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
module.exports = {
|
||||
plugins: {
|
||||
tailwindcss: {},
|
||||
autoprefixer: {},
|
||||
},
|
||||
};
|
||||
|
|
@ -1 +0,0 @@
|
|||
<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" aria-hidden="true" role="img" class="iconify iconify--logos" width="31.88" height="32" preserveAspectRatio="xMidYMid meet" viewBox="0 0 256 257"><defs><linearGradient id="IconifyId1813088fe1fbc01fb466" x1="-.828%" x2="57.636%" y1="7.652%" y2="78.411%"><stop offset="0%" stop-color="#41D1FF"></stop><stop offset="100%" stop-color="#BD34FE"></stop></linearGradient><linearGradient id="IconifyId1813088fe1fbc01fb467" x1="43.376%" x2="50.316%" y1="2.242%" y2="89.03%"><stop offset="0%" stop-color="#FFEA83"></stop><stop offset="8.333%" stop-color="#FFDD35"></stop><stop offset="100%" stop-color="#FFA800"></stop></linearGradient></defs><path fill="url(#IconifyId1813088fe1fbc01fb466)" d="M255.153 37.938L134.897 252.976c-2.483 4.44-8.862 4.466-11.382.048L.875 37.958c-2.746-4.814 1.371-10.646 6.827-9.67l120.385 21.517a6.537 6.537 0 0 0 2.322-.004l117.867-21.483c5.438-.991 9.574 4.796 6.877 9.62Z"></path><path fill="url(#IconifyId1813088fe1fbc01fb467)" d="M185.432.063L96.44 17.501a3.268 3.268 0 0 0-2.634 3.014l-5.474 92.456a3.268 3.268 0 0 0 3.997 3.378l24.777-5.718c2.318-.535 4.413 1.507 3.936 3.838l-7.361 36.047c-.495 2.426 1.782 4.5 4.151 3.78l15.304-4.649c2.372-.72 4.652 1.36 4.15 3.788l-11.698 56.621c-.732 3.542 3.979 5.473 5.943 2.437l1.313-2.028l72.516-144.72c1.215-2.423-.88-5.186-3.54-4.672l-25.505 4.922c-2.396.462-4.435-1.77-3.759-4.114l16.646-57.705c.677-2.35-1.37-4.583-3.769-4.113Z"></path></svg>
|
||||
|
Before Width: | Height: | Size: 1.5 KiB |
|
|
@ -1,22 +0,0 @@
|
|||
open React
|
||||
open ReactEvent.Form
|
||||
|
||||
@react.component
|
||||
let make = () => {
|
||||
let (inputExpr, setInputExpr) = useState(() => "")
|
||||
|
||||
let (interp, setInterp) = useState(() => OneTruth.make())
|
||||
|
||||
<div className="p-6">
|
||||
<h1 className="text-3xl font-semibold"> {"What is this about?"->React.string} </h1>
|
||||
<div>
|
||||
<input
|
||||
className="bg-gray-50 border border-gray-300 text-gray-900 text-sm rounded-lg focus:ring-blue-500 focus:border-blue-500 block w-full p-2.5 dark:bg-gray-700 dark:border-gray-600 dark:placeholder-gray-400 dark:text-white dark:focus:ring-blue-500 dark:focus:border-blue-500"
|
||||
type_="text"
|
||||
value={inputExpr}
|
||||
onChange={event => setInputExpr(currentTarget(event)["value"])}
|
||||
/>
|
||||
<pre> {interp->JSON.stringifyAnyWithIndent(2)->Option.getWithDefault("")->string} </pre>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
|
@ -1,2 +0,0 @@
|
|||
@react.component
|
||||
let make: unit => Jsx.element
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
// Styling from https://tailwind-elements.com/docs/standard/components/buttons/
|
||||
let make = props =>
|
||||
<button
|
||||
{...
|
||||
props}
|
||||
className="inline-block px-6 py-2.5 bg-blue-600 text-white font-medium text-xs leading-tight uppercase rounded shadow-md hover:bg-blue-700 hover:shadow-lg focus:bg-blue-700 focus:shadow-lg focus:outline-none focus:ring-0 active:bg-blue-800 active:shadow-lg transition duration-150 ease-in-out"
|
||||
/>
|
||||
|
|
@ -1 +0,0 @@
|
|||
let make: JsxDOM.domProps => Jsx.element
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
%%raw("import './index.css'")
|
||||
|
||||
switch ReactDOM.querySelector("#root") {
|
||||
| Some(domElement) =>
|
||||
ReactDOM.Client.createRoot(domElement)->ReactDOM.Client.Root.render(
|
||||
<React.StrictMode>
|
||||
<App />
|
||||
</React.StrictMode>,
|
||||
)
|
||||
| None => ()
|
||||
}
|
||||
|
|
@ -1 +0,0 @@
|
|||
<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" aria-hidden="true" role="img" class="iconify iconify--logos" width="35.93" height="32" preserveAspectRatio="xMidYMid meet" viewBox="0 0 256 228"><path fill="#00D8FF" d="M210.483 73.824a171.49 171.49 0 0 0-8.24-2.597c.465-1.9.893-3.777 1.273-5.621c6.238-30.281 2.16-54.676-11.769-62.708c-13.355-7.7-35.196.329-57.254 19.526a171.23 171.23 0 0 0-6.375 5.848a155.866 155.866 0 0 0-4.241-3.917C100.759 3.829 77.587-4.822 63.673 3.233C50.33 10.957 46.379 33.89 51.995 62.588a170.974 170.974 0 0 0 1.892 8.48c-3.28.932-6.445 1.924-9.474 2.98C17.309 83.498 0 98.307 0 113.668c0 15.865 18.582 31.778 46.812 41.427a145.52 145.52 0 0 0 6.921 2.165a167.467 167.467 0 0 0-2.01 9.138c-5.354 28.2-1.173 50.591 12.134 58.266c13.744 7.926 36.812-.22 59.273-19.855a145.567 145.567 0 0 0 5.342-4.923a168.064 168.064 0 0 0 6.92 6.314c21.758 18.722 43.246 26.282 56.54 18.586c13.731-7.949 18.194-32.003 12.4-61.268a145.016 145.016 0 0 0-1.535-6.842c1.62-.48 3.21-.974 4.76-1.488c29.348-9.723 48.443-25.443 48.443-41.52c0-15.417-17.868-30.326-45.517-39.844Zm-6.365 70.984c-1.4.463-2.836.91-4.3 1.345c-3.24-10.257-7.612-21.163-12.963-32.432c5.106-11 9.31-21.767 12.459-31.957c2.619.758 5.16 1.557 7.61 2.4c23.69 8.156 38.14 20.213 38.14 29.504c0 9.896-15.606 22.743-40.946 31.14Zm-10.514 20.834c2.562 12.94 2.927 24.64 1.23 33.787c-1.524 8.219-4.59 13.698-8.382 15.893c-8.067 4.67-25.32-1.4-43.927-17.412a156.726 156.726 0 0 1-6.437-5.87c7.214-7.889 14.423-17.06 21.459-27.246c12.376-1.098 24.068-2.894 34.671-5.345a134.17 134.17 0 0 1 1.386 6.193ZM87.276 214.515c-7.882 2.783-14.16 2.863-17.955.675c-8.075-4.657-11.432-22.636-6.853-46.752a156.923 156.923 0 0 1 1.869-8.499c10.486 2.32 22.093 3.988 34.498 4.994c7.084 9.967 14.501 19.128 21.976 27.15a134.668 134.668 0 0 1-4.877 4.492c-9.933 8.682-19.886 14.842-28.658 17.94ZM50.35 144.747c-12.483-4.267-22.792-9.812-29.858-15.863c-6.35-5.437-9.555-10.836-9.555-15.216c0-9.322 13.897-21.212 37.076-29.293c2.813-.98 5.757-1.905 8.812-2.773c3.204 10.42 7.406 21.315 12.477 32.332c-5.137 11.18-9.399 22.249-12.634 32.792a134.718 134.718 0 0 1-6.318-1.979Zm12.378-84.26c-4.811-24.587-1.616-43.134 6.425-47.789c8.564-4.958 27.502 2.111 47.463 19.835a144.318 144.318 0 0 1 3.841 3.545c-7.438 7.987-14.787 17.08-21.808 26.988c-12.04 1.116-23.565 2.908-34.161 5.309a160.342 160.342 0 0 1-1.76-7.887Zm110.427 27.268a347.8 347.8 0 0 0-7.785-12.803c8.168 1.033 15.994 2.404 23.343 4.08c-2.206 7.072-4.956 14.465-8.193 22.045a381.151 381.151 0 0 0-7.365-13.322Zm-45.032-43.861c5.044 5.465 10.096 11.566 15.065 18.186a322.04 322.04 0 0 0-30.257-.006c4.974-6.559 10.069-12.652 15.192-18.18ZM82.802 87.83a323.167 323.167 0 0 0-7.227 13.238c-3.184-7.553-5.909-14.98-8.134-22.152c7.304-1.634 15.093-2.97 23.209-3.984a321.524 321.524 0 0 0-7.848 12.897Zm8.081 65.352c-8.385-.936-16.291-2.203-23.593-3.793c2.26-7.3 5.045-14.885 8.298-22.6a321.187 321.187 0 0 0 7.257 13.246c2.594 4.48 5.28 8.868 8.038 13.147Zm37.542 31.03c-5.184-5.592-10.354-11.779-15.403-18.433c4.902.192 9.899.29 14.978.29c5.218 0 10.376-.117 15.453-.343c-4.985 6.774-10.018 12.97-15.028 18.486Zm52.198-57.817c3.422 7.8 6.306 15.345 8.596 22.52c-7.422 1.694-15.436 3.058-23.88 4.071a382.417 382.417 0 0 0 7.859-13.026a347.403 347.403 0 0 0 7.425-13.565Zm-16.898 8.101a358.557 358.557 0 0 1-12.281 19.815a329.4 329.4 0 0 1-23.444.823c-7.967 0-15.716-.248-23.178-.732a310.202 310.202 0 0 1-12.513-19.846h.001a307.41 307.41 0 0 1-10.923-20.627a310.278 310.278 0 0 1 10.89-20.637l-.001.001a307.318 307.318 0 0 1 12.413-19.761c7.613-.576 15.42-.876 23.31-.876H128c7.926 0 15.743.303 23.354.883a329.357 329.357 0 0 1 12.335 19.695a358.489 358.489 0 0 1 11.036 20.54a329.472 329.472 0 0 1-11 20.722Zm22.56-122.124c8.572 4.944 11.906 24.881 6.52 51.026c-.344 1.668-.73 3.367-1.15 5.09c-10.622-2.452-22.155-4.275-34.23-5.408c-7.034-10.017-14.323-19.124-21.64-27.008a160.789 160.789 0 0 1 5.888-5.4c18.9-16.447 36.564-22.941 44.612-18.3ZM128 90.808c12.625 0 22.86 10.235 22.86 22.86s-10.235 22.86-22.86 22.86s-22.86-10.235-22.86-22.86s10.235-22.86 22.86-22.86Z"></path></svg>
|
||||
|
Before Width: | Height: | Size: 4 KiB |
|
|
@ -1,3 +0,0 @@
|
|||
@tailwind base;
|
||||
@tailwind components;
|
||||
@tailwind utilities;
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
type rec arity =
|
||||
| Zero
|
||||
| Combined(array<arity>)
|
||||
| Arrow(arity, arity)
|
||||
|
||||
type rec expr =
|
||||
| Var(string)
|
||||
| Abs(string, expr)
|
||||
| App(expr, expr)
|
||||
|
||||
type judgment =
|
||||
// Base judgments
|
||||
| IsSet(expr)
|
||||
| AreEqualSets(expr, expr)
|
||||
| InSet(expr, expr)
|
||||
| AreEqualElementsInSet(expr, expr, expr)
|
||||
|
||||
// Proposition stuff
|
||||
| IsProp(expr)
|
||||
| IsTrue(expr)
|
||||
|
|
@ -1,50 +0,0 @@
|
|||
open Core
|
||||
|
||||
type context = {judgments: array<judgment>}
|
||||
|
||||
type t = {
|
||||
context: context,
|
||||
knownNames: Map.t<string, expr>,
|
||||
knownSets: Set.t<string>,
|
||||
}
|
||||
|
||||
// Something that appears in the top or bottom of a derivation
|
||||
type hypotheticalJudgment = {
|
||||
assumptions?: context,
|
||||
judgment: judgment,
|
||||
}
|
||||
|
||||
type rule = {
|
||||
premises: array<hypotheticalJudgment>,
|
||||
conclusions: array<hypotheticalJudgment>,
|
||||
}
|
||||
|
||||
let makeWithRules = (initialRules: array<rule>) => {
|
||||
let knownSets = ref(Set.make())
|
||||
let knownNames = ref(Map.make())
|
||||
let context = {judgments: []}
|
||||
|
||||
// Evaluate some shit
|
||||
initialRules->Array.forEach(rule => {
|
||||
Js.log2("helloge", rule)
|
||||
()
|
||||
})
|
||||
|
||||
{
|
||||
context,
|
||||
knownSets: knownSets.contents,
|
||||
knownNames: knownNames.contents,
|
||||
}
|
||||
}
|
||||
|
||||
// Evaluate an expression without changing the interpreter state
|
||||
let eval = (state: t, expr: expr) => {
|
||||
let stop = ref(false)
|
||||
while !stop.contents {
|
||||
stop := true
|
||||
state.context.judgments->Array.forEach(rule => ())
|
||||
}
|
||||
|
||||
//
|
||||
state
|
||||
}
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
open Interp
|
||||
|
||||
let make = () =>
|
||||
makeWithRules([
|
||||
{
|
||||
premises: [{judgment: InSet(Var("a"), Var("A"))}],
|
||||
conclusions: [{judgment: IsTrue(Var("A"))}],
|
||||
},
|
||||
// Bool
|
||||
{
|
||||
premises: [],
|
||||
conclusions: [{judgment: IsSet(Var("Bool"))}],
|
||||
},
|
||||
{
|
||||
premises: [],
|
||||
conclusions: [{judgment: InSet(Var("true"), Var("Bool"))}],
|
||||
},
|
||||
{
|
||||
premises: [],
|
||||
conclusions: [{judgment: InSet(Var("false"), Var("Bool"))}],
|
||||
},
|
||||
])
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
/** @type {import('tailwindcss').Config} */
|
||||
module.exports = {
|
||||
content: ["./index.html", "./src/**/*.bs.mjs"],
|
||||
theme: {
|
||||
extend: {},
|
||||
},
|
||||
plugins: [],
|
||||
};
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
import { defineConfig } from 'vite'
|
||||
import react from '@vitejs/plugin-react'
|
||||
|
||||
// https://vitejs.dev/config/
|
||||
export default defineConfig({
|
||||
plugins: [
|
||||
react({
|
||||
include: ['**/*.bs.mjs'],
|
||||
}),
|
||||
],
|
||||
});
|
||||
Loading…
Reference in a new issue