Fix broken test, clean up repo a bit

lazear · Jul 26, 2020 · 38fe0f8 · 38fe0f8
1 parent 439fb96
commit 38fe0f8
Show file tree

Hide file tree

Showing 82 changed files with 7 additions and 43 deletions.
diff --git a/arith/Cargo.toml → 01_arith/Cargo.toml b/arith/Cargo.toml → 01_arith/Cargo.toml
diff --git a/arith/src/lexer.rs → 01_arith/src/lexer.rs b/arith/src/lexer.rs → 01_arith/src/lexer.rs
diff --git a/arith/src/main.rs → 01_arith/src/main.rs b/arith/src/main.rs → 01_arith/src/main.rs
diff --git a/arith/src/parser.rs → 01_arith/src/parser.rs b/arith/src/parser.rs → 01_arith/src/parser.rs
diff --git a/lambda/Cargo.toml → 02_lambda/Cargo.toml b/lambda/Cargo.toml → 02_lambda/Cargo.toml
diff --git a/lambda/src/context.rs → 02_lambda/src/context.rs b/lambda/src/context.rs → 02_lambda/src/context.rs
diff --git a/lambda/src/lexer.rs → 02_lambda/src/lexer.rs b/lambda/src/lexer.rs → 02_lambda/src/lexer.rs
diff --git a/lambda/src/main.rs → 02_lambda/src/main.rs b/lambda/src/main.rs → 02_lambda/src/main.rs
diff --git a/lambda/src/parser.rs → 02_lambda/src/parser.rs b/lambda/src/parser.rs → 02_lambda/src/parser.rs
diff --git a/typedarith/Cargo.toml → 03_typedarith/Cargo.toml b/typedarith/Cargo.toml → 03_typedarith/Cargo.toml
diff --git a/typedarith/src/ast.rs → 03_typedarith/src/ast.rs b/typedarith/src/ast.rs → 03_typedarith/src/ast.rs
diff --git a/typedarith/src/lexer.rs → 03_typedarith/src/lexer.rs b/typedarith/src/lexer.rs → 03_typedarith/src/lexer.rs
diff --git a/typedarith/src/main.rs → 03_typedarith/src/main.rs b/typedarith/src/main.rs → 03_typedarith/src/main.rs
diff --git a/typedarith/src/parser.rs → 03_typedarith/src/parser.rs b/typedarith/src/parser.rs → 03_typedarith/src/parser.rs
diff --git a/stlc/.gitignore → 04_stlc/.gitignore b/stlc/.gitignore → 04_stlc/.gitignore
diff --git a/stlc/Cargo.toml → 04_stlc/Cargo.toml b/stlc/Cargo.toml → 04_stlc/Cargo.toml
diff --git a/stlc/src/eval.rs → 04_stlc/src/eval.rs b/stlc/src/eval.rs → 04_stlc/src/eval.rs
diff --git a/stlc/src/lexer.rs → 04_stlc/src/lexer.rs b/stlc/src/lexer.rs → 04_stlc/src/lexer.rs
diff --git a/stlc/src/main.rs → 04_stlc/src/main.rs b/stlc/src/main.rs → 04_stlc/src/main.rs
diff --git a/stlc/src/parser.rs → 04_stlc/src/parser.rs b/stlc/src/parser.rs → 04_stlc/src/parser.rs
diff --git a/stlc/src/term.rs → 04_stlc/src/term.rs b/stlc/src/term.rs → 04_stlc/src/term.rs
diff --git a/stlc/src/typing.rs → 04_stlc/src/typing.rs b/stlc/src/typing.rs → 04_stlc/src/typing.rs
diff --git a/stlc/src/visitor.rs → 04_stlc/src/visitor.rs b/stlc/src/visitor.rs → 04_stlc/src/visitor.rs
diff --git a/recon/Cargo.toml → 05_recon/Cargo.toml b/recon/Cargo.toml → 05_recon/Cargo.toml
diff --git a/recon/src/disjoint.rs → 05_recon/src/disjoint.rs b/recon/src/disjoint.rs → 05_recon/src/disjoint.rs
@@ -294,31 +294,3 @@ impl<T: std::fmt::Debug> std::fmt::Debug for DisjointSet<T> {
         writeln!(f, "}}")
     }
 }
-
-#[cfg(test)]
-mod tests {
-    use super::*;
-
-    #[test]
-    fn it_works() {
-        let mut set = DisjointSet::new();
-
-        let a = set.singleton(10);
-        let b = set.singleton(12);
-        let c = set.singleton(14);
-        let d = set.singleton(29);
-        let e = set.singleton(1);
-
-        set.union(|a, b| a, a, d);
-        set.union(|a, b| a, d, c);
-        set.union(|a, b| a, a, e);
-
-        assert_eq!(set.find(a), &29);
-        assert_eq!(set.find(e), &29);
-        assert_eq!(set.find(c), &29);
-        assert_eq!(set.find(d), &29);
-        assert!(set.find(a) != set.find(b));
-
-        assert_eq!(set.components.get(), 2);
-    }
-}
diff --git a/recon/src/main.rs → 05_recon/src/main.rs b/recon/src/main.rs → 05_recon/src/main.rs
diff --git a/recon/src/mutation/mod.rs → 05_recon/src/mutation/mod.rs b/recon/src/mutation/mod.rs → 05_recon/src/mutation/mod.rs
diff --git a/recon/src/mutation/write_once.rs → 05_recon/src/mutation/write_once.rs b/recon/src/mutation/write_once.rs → 05_recon/src/mutation/write_once.rs
diff --git a/recon/src/naive.rs → 05_recon/src/naive.rs b/recon/src/naive.rs → 05_recon/src/naive.rs
diff --git a/recon/src/parser.rs → 05_recon/src/parser.rs b/recon/src/parser.rs → 05_recon/src/parser.rs
diff --git a/recon/src/types.rs → 05_recon/src/types.rs b/recon/src/types.rs → 05_recon/src/types.rs
diff --git a/system_f/Cargo.toml → 06_system_f/Cargo.toml b/system_f/Cargo.toml → 06_system_f/Cargo.toml
diff --git a/system_f/README.md → 06_system_f/README.md b/system_f/README.md → 06_system_f/README.md
diff --git a/system_f/src/diagnostics.rs → 06_system_f/src/diagnostics.rs b/system_f/src/diagnostics.rs → 06_system_f/src/diagnostics.rs
diff --git a/system_f/src/eval.rs → 06_system_f/src/eval.rs b/system_f/src/eval.rs → 06_system_f/src/eval.rs
diff --git a/system_f/src/macros.rs → 06_system_f/src/macros.rs b/system_f/src/macros.rs → 06_system_f/src/macros.rs
diff --git a/system_f/src/main.rs → 06_system_f/src/main.rs b/system_f/src/main.rs → 06_system_f/src/main.rs
diff --git a/system_f/src/patterns/mod.rs → 06_system_f/src/patterns/mod.rs b/system_f/src/patterns/mod.rs → 06_system_f/src/patterns/mod.rs
diff --git a/system_f/src/syntax/lexer.rs → 06_system_f/src/syntax/lexer.rs b/system_f/src/syntax/lexer.rs → 06_system_f/src/syntax/lexer.rs
diff --git a/system_f/src/syntax/mod.rs → 06_system_f/src/syntax/mod.rs b/system_f/src/syntax/mod.rs → 06_system_f/src/syntax/mod.rs
diff --git a/system_f/src/syntax/parser.rs → 06_system_f/src/syntax/parser.rs b/system_f/src/syntax/parser.rs → 06_system_f/src/syntax/parser.rs
diff --git a/system_f/src/terms/mod.rs → 06_system_f/src/terms/mod.rs b/system_f/src/terms/mod.rs → 06_system_f/src/terms/mod.rs
diff --git a/system_f/src/terms/visit.rs → 06_system_f/src/terms/visit.rs b/system_f/src/terms/visit.rs → 06_system_f/src/terms/visit.rs
diff --git a/system_f/src/types/mod.rs → 06_system_f/src/types/mod.rs b/system_f/src/types/mod.rs → 06_system_f/src/types/mod.rs
diff --git a/system_f/src/types/patterns.rs → 06_system_f/src/types/patterns.rs b/system_f/src/types/patterns.rs → 06_system_f/src/types/patterns.rs
diff --git a/system_f/src/types/visit.rs → 06_system_f/src/types/visit.rs b/system_f/src/types/visit.rs → 06_system_f/src/types/visit.rs
diff --git a/system_f/src/visit.rs → 06_system_f/src/visit.rs b/system_f/src/visit.rs → 06_system_f/src/visit.rs
diff --git a/system_f/test.sf → 06_system_f/test.sf b/system_f/test.sf → 06_system_f/test.sf
diff --git a/system_fw/Cargo.toml → 07_system_fw/Cargo.toml b/system_fw/Cargo.toml → 07_system_fw/Cargo.toml
diff --git a/system_fw/README.md → 07_system_fw/README.md b/system_fw/README.md → 07_system_fw/README.md
diff --git a/system_fw/src/diagnostics.rs → 07_system_fw/src/diagnostics.rs b/system_fw/src/diagnostics.rs → 07_system_fw/src/diagnostics.rs
diff --git a/system_fw/src/elaborate.rs → 07_system_fw/src/elaborate.rs b/system_fw/src/elaborate.rs → 07_system_fw/src/elaborate.rs
diff --git a/system_fw/src/functor.rs → 07_system_fw/src/functor.rs b/system_fw/src/functor.rs → 07_system_fw/src/functor.rs
diff --git a/system_fw/src/hir/bidir.rs → 07_system_fw/src/hir/bidir.rs b/system_fw/src/hir/bidir.rs → 07_system_fw/src/hir/bidir.rs
diff --git a/system_fw/src/hir/mod.rs → 07_system_fw/src/hir/mod.rs b/system_fw/src/hir/mod.rs → 07_system_fw/src/hir/mod.rs
diff --git a/system_fw/src/macros.rs → 07_system_fw/src/macros.rs b/system_fw/src/macros.rs → 07_system_fw/src/macros.rs
diff --git a/system_fw/src/main.rs → 07_system_fw/src/main.rs b/system_fw/src/main.rs → 07_system_fw/src/main.rs
diff --git a/system_fw/src/stack.rs → 07_system_fw/src/stack.rs b/system_fw/src/stack.rs → 07_system_fw/src/stack.rs
diff --git a/system_fw/src/syntax/ast.rs → 07_system_fw/src/syntax/ast.rs b/system_fw/src/syntax/ast.rs → 07_system_fw/src/syntax/ast.rs
diff --git a/system_fw/src/syntax/lexer.rs → 07_system_fw/src/syntax/lexer.rs b/system_fw/src/syntax/lexer.rs → 07_system_fw/src/syntax/lexer.rs
diff --git a/system_fw/src/syntax/mod.rs → 07_system_fw/src/syntax/mod.rs b/system_fw/src/syntax/mod.rs → 07_system_fw/src/syntax/mod.rs
diff --git a/system_fw/src/syntax/parser/README.md → 07_system_fw/src/syntax/parser/README.md b/system_fw/src/syntax/parser/README.md → 07_system_fw/src/syntax/parser/README.md
diff --git a/system_fw/src/syntax/parser/decls.rs → 07_system_fw/src/syntax/parser/decls.rs b/system_fw/src/syntax/parser/decls.rs → 07_system_fw/src/syntax/parser/decls.rs
diff --git a/system_fw/src/syntax/parser/exprs.rs → 07_system_fw/src/syntax/parser/exprs.rs b/system_fw/src/syntax/parser/exprs.rs → 07_system_fw/src/syntax/parser/exprs.rs
diff --git a/system_fw/src/syntax/parser/infix.rs → 07_system_fw/src/syntax/parser/infix.rs b/system_fw/src/syntax/parser/infix.rs → 07_system_fw/src/syntax/parser/infix.rs
diff --git a/system_fw/src/syntax/parser/mod.rs → 07_system_fw/src/syntax/parser/mod.rs b/system_fw/src/syntax/parser/mod.rs → 07_system_fw/src/syntax/parser/mod.rs
diff --git a/system_fw/src/syntax/parser/patterns.rs → 07_system_fw/src/syntax/parser/patterns.rs b/system_fw/src/syntax/parser/patterns.rs → 07_system_fw/src/syntax/parser/patterns.rs
diff --git a/system_fw/src/syntax/parser/types.rs → 07_system_fw/src/syntax/parser/types.rs b/system_fw/src/syntax/parser/types.rs → 07_system_fw/src/syntax/parser/types.rs
diff --git a/system_fw/src/syntax/tokens.rs → 07_system_fw/src/syntax/tokens.rs b/system_fw/src/syntax/tokens.rs → 07_system_fw/src/syntax/tokens.rs
diff --git a/system_fw/src/syntax/visit/mod.rs → 07_system_fw/src/syntax/visit/mod.rs b/system_fw/src/syntax/visit/mod.rs → 07_system_fw/src/syntax/visit/mod.rs
diff --git a/system_fw/src/syntax/visit/types.rs → 07_system_fw/src/syntax/visit/types.rs b/system_fw/src/syntax/visit/types.rs → 07_system_fw/src/syntax/visit/types.rs
diff --git a/system_fw/src/terms.rs → 07_system_fw/src/terms.rs b/system_fw/src/terms.rs → 07_system_fw/src/terms.rs
diff --git a/system_fw/src/typecheck.rs → 07_system_fw/src/typecheck.rs b/system_fw/src/typecheck.rs → 07_system_fw/src/typecheck.rs
diff --git a/system_fw/src/types.rs → 07_system_fw/src/types.rs b/system_fw/src/types.rs → 07_system_fw/src/types.rs
diff --git a/system_fw/test.fw → 07_system_fw/test.fw b/system_fw/test.fw → 07_system_fw/test.fw
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,2 +1,2 @@
 [workspace]
-members = ["arith", "bidir", "dependent", "lambda", "typedarith", "stlc", "system_f", "system_fw", "recon", "util"]
+members = ["01_arith", "02_lambda",  "03_typedarith", "04_stlc", "05_recon",  "06_system_f", "07_system_fw", "x1_bidir", "x2_dependent", "util"]
diff --git a/README.md b/README.md
@@ -4,29 +4,21 @@
 
 Several Rust implementations of exercises from Benjamin Pierce's "Types and Programming Languages" are organized into different folders, as described below:
 
-- `lambda` is an implementation of the untyped lambda calculus as presented in chapter 5, 6, and 7.
-
 - `arith` is an implementation of the untyped lambda calculus extended with simple numeric operations
 
+- `lambda` is an implementation of the untyped lambda calculus as presented in chapter 5, 6, and 7.
+
 - `typedarith` is the `arith` project extended with simple types: `Nat` and `Bool`
 
 - `stlc` is an implementation of the simply typed lambda calculus, as discussed in chapters 9 and 10 of TAPL. This simply typed calculus has the types, `Unit`, `Nat`, `Bool`, `T -> T` (arrow), and `Record` types.
 
-- `system_f` contains a parser, typechecker, and evaluator for the simply typed lambda calculus with parametric polymorphism (System F). 
+- `recon` contains several implementations of Hindley-Milner based type reconstruction from the untyped lambda calculus to System F, with let-polymorphism. Both Algorithm W (the more common) and Algorithm J (the more efficient) are presented. For Alg. W, both a naive equality constraint solver, and a faster union-find (with path compression) solver are provided. Algorithm J makes use shared mutable references to promote type sharing instead.
 
-The implementation of System F is the most complete so far, and I've tried to write a parser, typechecker and diagnostic system that can given meaningful messages, such as:
+- `system_f` contains a parser, typechecker, and evaluator for the simply typed lambda calculus with parametric polymorphism (System F). The implementation of System F is the most complete so far, and I've tried to write a parser, typechecker and diagnostic system that can given meaningful messages
 
-```
-type Var = { A | B Nat | C Nat }
-let func = (\x: Var. case x of | A => 0 | B y => succ x | C y => pred x) in func C 2 of Var
-                                                 ^~~~^ --- abstraction requires type Nat
-                                                      ^^ --- but it is applied to type "A: Unit | B: Nat | C: Nat"
-```
+- `system_fw` contains a parser for a high-level, Standard ML like source language that is desugared into an HIR, and then System F-omega. This extends `system_f` with type operators and higher-kinded types. This is where most of the ongoing work is located, as I'd like to make this the basis of a toy (but powerful, and useable) programming language. Ideally we will have some form of bidirectional type inference. Work on this has accidentally turned into a full fledged [SML compiler](https://github.com/SomewhatML/sml-compiler), so it's likely that I will roll back the work on the system_fw project to just type checking
 
-- `system_fw` contains a parser for a high-level, Standard ML like source language that is desugared into an HIR, and then System F-omega. This extends `system_f` with type operators and higher-kinded types. This is where most of the ongoing work is located, as I'd like to make this the basis of a toy (but powerful, and useable) programming language. Ideally we will have some form of bidirectional type inference
+- `bidir` is is an implementation of the bidirectional typechecker from 'Complete and Easy Bidirectional Typechecking', extended with booleans, product, and sum types. I make no claims on the correctness of the implementation for the extended features not present in the paper.
 
 - `dependent` is WIP, implementing a simple, dependently typed lambda calculus as discussed in ATAPL.
 
-- `bidir` is is an implementation of the bidirectional typechecker from 'Complete and Easy Bidirectional Typechecking', extended with booleans, product, and sum types. I make no claims on the correctness of the implementation for the extended features not present in the paper.
-
-- `recon` contains several implementations of Hindley-Milner based type reconstruction from the untyped lambda calculus to System F, with let-polymorphism. Both Algorithm W (the more common) and Algorithm J (the more efficient) are presented. For Alg. W, both a naive equality constraint solver, and a faster union-find (with path compression) solver are provided. Algorithm J makes use shared mutable references to promote type sharing instead.
diff --git a/bidir/Cargo.toml → x1_bidir/Cargo.toml b/bidir/Cargo.toml → x1_bidir/Cargo.toml
diff --git a/bidir/src/helpers.rs → x1_bidir/src/helpers.rs b/bidir/src/helpers.rs → x1_bidir/src/helpers.rs
diff --git a/bidir/src/main.rs → x1_bidir/src/main.rs b/bidir/src/main.rs → x1_bidir/src/main.rs
diff --git a/dependent/Cargo.toml → x2_dependent/Cargo.toml b/dependent/Cargo.toml → x2_dependent/Cargo.toml
diff --git a/dependent/src/main.rs → x2_dependent/src/main.rs b/dependent/src/main.rs → x2_dependent/src/main.rs