WIP generate scott adts

This commit is contained in:
imaqtkatt 2023-11-08 11:08:07 -03:00
parent baa1a861c9
commit b617dc0dbd
6 changed files with 117 additions and 3 deletions

25
Cargo.lock generated
View File

@ -162,7 +162,7 @@ version = "1.0.0-alpha.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cc3172a80699de358070dd99f80ea8badc6cdf8ac2417cb5a96e6d81bf5fe06d"
dependencies = [
"hashbrown",
"hashbrown 0.13.2",
"stacker",
]
@ -243,6 +243,12 @@ version = "1.9.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07"
[[package]]
name = "equivalent"
version = "1.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
[[package]]
name = "errno"
version = "0.3.5"
@ -274,6 +280,12 @@ dependencies = [
"ahash",
]
[[package]]
name = "hashbrown"
version = "0.14.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
[[package]]
name = "heck"
version = "0.4.1"
@ -302,6 +314,7 @@ dependencies = [
"clap",
"derive_more",
"hvm-core",
"indexmap",
"itertools 0.11.0",
"logos",
"miette",
@ -312,6 +325,16 @@ dependencies = [
"walkdir",
]
[[package]]
name = "indexmap"
version = "2.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d530e1a18b1cb4c484e6e34556a0d948706958449fca0cab753d649f2bce3d1f"
dependencies = [
"equivalent",
"hashbrown 0.14.2",
]
[[package]]
name = "is-terminal"
version = "0.4.9"

View File

@ -25,6 +25,7 @@ chumsky = "= 1.0.0-alpha.4"
clap = { version = "4.4.1", features = ["derive"], optional = true }
derive_more = "0.99.17"
hvm-core = { git = "https://github.com/HigherOrderCO/hvm-core.git" }
indexmap = "2.1.0"
itertools = "0.11.0"
logos = "0.13.0"
miette = { version = "5.10.0", features = ["fancy"] }

View File

@ -267,6 +267,8 @@ impl Book {
mod test {
use std::collections::{BTreeMap, HashMap};
use indexmap::IndexMap;
use crate::term::{
check::exhaustiveness::{useful, wildcard, Ctx, Problem},
parser::parse_definition_book,
@ -280,7 +282,7 @@ mod test {
fn bool_ctx() -> HashMap<Name, Adt> {
HashMap::from([(Name::new("Bool"), Adt {
ctrs: BTreeMap::from([(Name::new("T"), 0), (Name::new("F"), 0)]),
ctrs: IndexMap::from([(Name::new("T"), 0), (Name::new("F"), 0)]),
})])
}

View File

@ -1,11 +1,13 @@
use bimap::{BiHashMap, Overwritten};
use derive_more::{Display, From, Into};
use hvmc::run::Val;
use indexmap::IndexMap;
use itertools::Itertools;
use shrinkwraprs::Shrinkwrap;
use std::{
collections::{BTreeMap, HashMap},
fmt,
hash::Hash,
};
pub mod check;
@ -150,7 +152,8 @@ pub enum Op {
/// A user defined datatype
#[derive(Debug, Clone, Default)]
pub struct Adt {
pub ctrs: BTreeMap<Name, usize>,
// pub ctrs: BTreeMap<Name, usize>,
pub ctrs: IndexMap<Name, usize>,
}
#[derive(Debug, PartialEq, Eq, Clone, Shrinkwrap, Hash, PartialOrd, Ord, From, Into, Display)]

View File

@ -4,5 +4,6 @@ pub mod detach_supercombinators;
pub mod flatten;
pub mod linearize;
pub mod resolve_refs;
pub mod scott_generation;
pub mod simplify_ref_to_ref;
pub mod unique_names;

View File

@ -0,0 +1,84 @@
use crate::term::{Book, Definition, Name, Rule, Term};
impl Book {
pub fn generate_scott_adts(&mut self) {
for adt in self.adts.values() {
let curr_ctrs = adt.ctrs.clone();
let mut ctr_args = Vec::new();
let mut ctrs = Vec::new();
for (ctr_name, arity) in &curr_ctrs {
for ctr in curr_ctrs.keys() {
ctrs.push(ctr.clone());
if ctr == ctr_name {
make_args(arity, &mut ctr_args);
}
}
let lam = make_lam(&ctr_args, &mut ctrs, ctr_name);
ctr_args.clear();
ctrs.clear();
let def_id = self.def_names.insert(ctr_name.clone());
let rule = Rule { def_id, pats: vec![], body: lam };
let rules = vec![rule];
let def = Definition { def_id, rules };
self.defs.insert(def_id, def);
}
}
}
}
fn make_args(args_count: &usize, ctr_args: &mut Vec<Name>) {
for n in 0 .. *args_count {
let nam = Name(format!("a{n}"));
ctr_args.push(nam);
}
}
fn make_lam(ctr_args: &Vec<Name>, ctrs: &mut Vec<Name>, ctr_name: &Name) -> Term {
let args_to_apply = ctr_args.clone();
ctrs.reverse();
let mut lam_args = ctrs.clone();
let mut lam_args_ctrs = ctr_args.clone();
lam_args_ctrs.reverse();
lam_args.extend(lam_args_ctrs);
let app = Term::Var { nam: ctr_name.clone() };
let app = args_to_apply
.into_iter()
.fold(app, |acc, nam| Term::App { fun: Box::new(acc), arg: Box::new(Term::Var { nam }) });
let lam = app;
lam_args.into_iter().fold(lam, |acc, arg| Term::Lam { nam: Some(arg), bod: Box::new(acc) })
}
#[cfg(test)]
mod test {
use crate::term::parser::parse_definition_book;
#[test]
// what should we test here?
fn adt_generation() {
let code = r"
data List = (Cons x xs) | Nil
data Bool = True | False
data Tree = (Node val lft rgt) | Leaf
";
let book = parse_definition_book(code);
match book {
Ok(mut book) => {
book.generate_scott_adts();
println!("{}", book);
}
Err(_) => todo!(),
}
}
}