From 797e307a9d4a02e1dd100cf7548426accd82f0cb Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 10:51:57 -0600 Subject: [PATCH 01/16] lookup a fragment and apply the arguments --- PRODUCTION/fragment.lm | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/PRODUCTION/fragment.lm b/PRODUCTION/fragment.lm index 357f23e09..52dd6a883 100644 --- a/PRODUCTION/fragment.lm +++ b/PRODUCTION/fragment.lm @@ -76,3 +76,7 @@ fragment-apply-context := λctx fragment-rhs e . (match fragment-rhs ( )) ( u (fail (UnknownSubstituteFragment fragment-rhs))) )); + +fragment-apply := λctx function-name function-type function-args . ( + fail (TODO FragmentApply function-name function-type) +); From bc1fd37140a5ba87f59bd5f261d6ad67a6447206 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 13:51:30 -0600 Subject: [PATCH 02/16] going to start gradually typing everything --- Makefile | 2 +- PRODUCTION/fragment.lm | 8 +++++--- PRODUCTION/utility.lm | 4 ++++ tests/unit/utility.lm | 2 ++ 4 files changed, 12 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 4ced4fd67..d8554860b 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ -unit-tests: +unit-tests: prod cargo test unit_test_suite -- --nocapture nostd: prod diff --git a/PRODUCTION/fragment.lm b/PRODUCTION/fragment.lm index 52dd6a883..4754d989b 100644 --- a/PRODUCTION/fragment.lm +++ b/PRODUCTION/fragment.lm @@ -77,6 +77,8 @@ fragment-apply-context := λctx fragment-rhs e . (match fragment-rhs ( ( u (fail (UnknownSubstituteFragment fragment-rhs))) )); -fragment-apply := λctx function-name function-type function-args . ( - fail (TODO FragmentApply function-name function-type) -); +# ( [(String,StrictExpr)], String, Type, [StrictExpr] ) -> StrictExpr +fragment-apply := λctx function-name function-type function-args . (tail( + (assert-typeof( ctx List<[String,StrictExpr]> )) + (fail (TODO FragmentApply function-name function-type)) +)); diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 43d539f5d..2b072448c 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -260,3 +260,7 @@ assert-eq := λ msg l r . ( (print-s \t)(fail msg) )) )); + +assert-typeof := λ term tt . ( + (fail (TODO Typeof tt)) +); diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index 5fa5d0ae7..f3f7ac601 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -2,3 +2,5 @@ import PRODUCTION/utility.lm; (assert-eq( LiteralEquality True True )); + +(assert-typeof( 'a String )); From e6ed0c91e70297e460c1c18fe4d01527a377771a Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 13:56:25 -0600 Subject: [PATCH 03/16] build unit tests correctly and test typeof --- tests/b_unit.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/b_unit.rs b/tests/b_unit.rs index cc489fe99..c92579fc6 100644 --- a/tests/b_unit.rs +++ b/tests/b_unit.rs @@ -48,6 +48,7 @@ fn compile_compiler() { .stderr(std::process::Stdio::piped()) .arg("-o") .arg("production.s") + .arg("PRODUCTION/cli.lm") .spawn() .expect("failed to execute process") .wait_with_output() @@ -87,13 +88,13 @@ fn compile_compiler() { } fn run_unit(unit: &str) { + println!("Run unit test {}", unit); let exit = Command::new("./production") .stdout(std::process::Stdio::piped()) .stderr(std::process::Stdio::piped()) .arg("-o") .arg("unit.s") .arg(unit) - .arg("PRODUCTION/utility.lm") .spawn() .expect("failed to execute process") .wait_with_output() From 43ec9e9e790d447bd93936a3094417a71cfbcf2c Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 14:02:22 -0600 Subject: [PATCH 04/16] begin typecheck --- PRODUCTION/utility.lm | 27 ++++++++++++++++++++++----- tests/unit/utility.lm | 14 ++++++++++++-- 2 files changed, 34 insertions(+), 7 deletions(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 2b072448c..8771bd752 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -252,15 +252,32 @@ is-builtin := λf . (match f ( -assert-eq := λ msg l r . ( - (if (deep-eq( l r)) () ( - (print-s AssertNotEqual)(print-s \n) +assert-eq := λ l r . ( + (if (deep-eq( l r )) () ( + (print-s FailedAssertEqual)(print-s \n) (print-s \t)(print-s l)(print-s \n) (print-s \t)(print-s r)(print-s \n) - (print-s \t)(fail msg) + (exit 1) )) )); assert-typeof := λ term tt . ( - (fail (TODO Typeof tt)) + (if (is-typeof( term tt )) () ( + (print-s FailedAssertTypeof)(print-s \n) + (print-s \t)(print-s tt)(print-s \n) + (print-s \t)(print-s term)(print-s \n) + (exit 1) + )) +); + +assert-not-typeof := λ term tt . ( + (if (is-typeof( term tt )) ( + (print-s FailedAssertNotTypeof)(print-s \n) + (print-s \t)(print-s tt)(print-s \n) + (print-s \t)(print-s term)(print-s \n) + (exit 1) + ) ()) +); + +is-typeof := λ term tt . ( ); diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index f3f7ac601..e6a18e498 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -1,6 +1,16 @@ import PRODUCTION/utility.lm; -(assert-eq( LiteralEquality True True )); +(assert-eq( True True )); -(assert-typeof( 'a String )); +(assert-typeof( () Nil )); +(assert-not-typeof( 1 Nil )); +(assert-not-typeof( (1 2) Nil )); + +(assert-typeof( 1 Atom )); +(assert-not-typeof( () Atom )); +(assert-not-typeof( (1 2) Atom )); + +(assert-typeof( (1 2) Cons )); +(assert-not-typeof( 1 Cons )); +(assert-not-typeof( () Cons )); From 5725920cb2c2a8b3a7413289fd6e90dc6b9360f4 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 14:04:59 -0600 Subject: [PATCH 05/16] gradual typechecking is started --- PRODUCTION/utility.lm | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 8771bd752..29f287eb2 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -279,5 +279,10 @@ assert-not-typeof := λ term tt . ( ) ()) ); -is-typeof := λ term tt . ( -); +is-typeof := λ term tt . (match tt ( + () + ( Nil (not term) ) + ( Atom (is-atom term) ) + ( Cons (is-cons term) ) + (_ (fail (UnknownTypeofType tt))) +)); From a47c4dceccbf055d7c578123835d153a11c55c6d Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 14:10:14 -0600 Subject: [PATCH 06/16] struct gradual typing works --- PRODUCTION/fragment.lm | 2 +- PRODUCTION/utility.lm | 4 +++- tests/unit/utility.lm | 5 +++++ 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/PRODUCTION/fragment.lm b/PRODUCTION/fragment.lm index 4754d989b..3b50d65ca 100644 --- a/PRODUCTION/fragment.lm +++ b/PRODUCTION/fragment.lm @@ -79,6 +79,6 @@ fragment-apply-context := λctx fragment-rhs e . (match fragment-rhs ( # ( [(String,StrictExpr)], String, Type, [StrictExpr] ) -> StrictExpr fragment-apply := λctx function-name function-type function-args . (tail( - (assert-typeof( ctx List<[String,StrictExpr]> )) + (assert-typeof( ctx List<[Atom,StrictExpr]> )) (fail (TODO FragmentApply function-name function-type)) )); diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 29f287eb2..8f7463588 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -284,5 +284,7 @@ is-typeof := λ term tt . (match tt ( ( Nil (not term) ) ( Atom (is-atom term) ) ( Cons (is-cons term) ) - (_ (fail (UnknownTypeofType tt))) + ( (l r) (fail (UnknownTypeofType tt))) + ( () (fail (UnknownTypeofType tt))) + ( label (eq( (head term) label )) ) )); diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index e6a18e498..f46d95bb8 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -14,3 +14,8 @@ import PRODUCTION/utility.lm; (assert-typeof( (1 2) Cons )); (assert-not-typeof( 1 Cons )); (assert-not-typeof( () Cons )); + +(assert-typeof( (StrictExpr ()) StrictExpr )); +(assert-not-typeof( (StrictExpr ()) Expr )); +(assert-not-typeof( (StrictExpr ()) Nil )); +(assert-not-typeof( (StrictExpr ()) Atom )); From bf4e70db7c6d55422e1c7082f38a9f77be97f575 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 14:17:21 -0600 Subject: [PATCH 07/16] gradual typing some more --- PRODUCTION/utility.lm | 15 +++++++++++++-- tests/unit/utility.lm | 6 ++++++ 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 8f7463588..5e05cb35d 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -262,7 +262,7 @@ assert-eq := λ l r . ( )); assert-typeof := λ term tt . ( - (if (is-typeof( term tt )) () ( + (if (is-typeof( term (parse-typeof tt) )) () ( (print-s FailedAssertTypeof)(print-s \n) (print-s \t)(print-s tt)(print-s \n) (print-s \t)(print-s term)(print-s \n) @@ -271,7 +271,7 @@ assert-typeof := λ term tt . ( ); assert-not-typeof := λ term tt . ( - (if (is-typeof( term tt )) ( + (if (is-typeof( term (parse-typeof tt) )) ( (print-s FailedAssertNotTypeof)(print-s \n) (print-s \t)(print-s tt)(print-s \n) (print-s \t)(print-s term)(print-s \n) @@ -279,11 +279,22 @@ assert-not-typeof := λ term tt . ( ) ()) ); +parse-typeof := λ tt . tt; + is-typeof := λ term tt . (match tt ( () ( Nil (not term) ) ( Atom (is-atom term) ) ( Cons (is-cons term) ) + ( (List te) ( + (if (is-cons term) ( + (if (is-typeof( (tail term) te )) ( + (is-typeof( (head term) te )) + ) ()) + ) ( + (not term) + )) + )) ( (l r) (fail (UnknownTypeofType tt))) ( () (fail (UnknownTypeofType tt))) ( label (eq( (head term) label )) ) diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index f46d95bb8..5755168d9 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -19,3 +19,9 @@ import PRODUCTION/utility.lm; (assert-not-typeof( (StrictExpr ()) Expr )); (assert-not-typeof( (StrictExpr ()) Nil )); (assert-not-typeof( (StrictExpr ()) Atom )); + +(assert-typeof( () (List Atom) )); +(assert-typeof( () List )); +(assert-typeof( ((() 1) 2) List )); +(assert-not-typeof( ((() 1) 2) List )); +(assert-not-typeof( ((() 1) 2) List )); From 74e75a3774ea09b5680090459661b745f5a74182 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:09:15 -0600 Subject: [PATCH 08/16] type parser works better --- PRODUCTION/utility.lm | 47 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 40 insertions(+), 7 deletions(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 5e05cb35d..bdfef1e22 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -261,25 +261,58 @@ assert-eq := λ l r . ( )) )); -assert-typeof := λ term tt . ( - (if (is-typeof( term (parse-typeof tt) )) () ( +assert-typeof := λ term tt . (tail( + (set tt (parse-typeof tt)) + (if (is-typeof( term tt )) () ( (print-s FailedAssertTypeof)(print-s \n) (print-s \t)(print-s tt)(print-s \n) (print-s \t)(print-s term)(print-s \n) (exit 1) )) -); +)); -assert-not-typeof := λ term tt . ( - (if (is-typeof( term (parse-typeof tt) )) ( +assert-not-typeof := λ term tt . (tail( + (set tt (parse-typeof tt)) + (if (is-typeof( term tt )) ( (print-s FailedAssertNotTypeof)(print-s \n) (print-s \t)(print-s tt)(print-s \n) (print-s \t)(print-s term)(print-s \n) (exit 1) ) ()) -); +)); -parse-typeof := λ tt . tt; +parse-parameter-typeof := λ tt . (tail( + (assert-eq( '< (head-string tt) )) + (set tt (tail-string tt)) + (local inner) + (while tt ( + (match (head-string tt) ( + () + ('> ( (assert-eq( () (tail-string tt) )) )) + (c (set inner (inner (clone-rope c)) )) + )) + (set tt (tail-string tt)) + )) + (parse-typeof (clone-rope inner)) +)); + +parse-typeof := λ tt . (tail( + (local buff) + (local base) + (while tt ( + (match (head-string tt) ( + () + ('[ (fail (TODO Array Typeof tt))) + ('< ( + (set base ( (clone-rope buff) (parse-parameter-typeof tt) )) + (set tt ()) + )) + (c (set buff (buff (clone-rope c)) )) + )) + (set tt (tail-string tt)) + )) + (if base base (clone-rope buff)) +)); is-typeof := λ term tt . (match tt ( () From 771797d2fd85bfa62e5c138e8bd3f76c8b2fdc0e Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:11:44 -0600 Subject: [PATCH 09/16] gradually gradually typing --- PRODUCTION/utility.lm | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index bdfef1e22..c548d0868 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -299,6 +299,10 @@ parse-parameter-typeof := λ tt . (tail( parse-typeof := λ tt . (tail( (local buff) (local base) + (if (is-cons tt) ( + (set base tt) + (set tt ()) + ) ()) (while tt ( (match (head-string tt) ( () @@ -322,7 +326,7 @@ is-typeof := λ term tt . (match tt ( ( (List te) ( (if (is-cons term) ( (if (is-typeof( (tail term) te )) ( - (is-typeof( (head term) te )) + (is-typeof( (head term) tt )) ) ()) ) ( (not term) From e8595ab2077b9309a3def920be88c633e976b804 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:13:31 -0600 Subject: [PATCH 10/16] todo parse cons --- tests/unit/utility.lm | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index 5755168d9..bd802ce18 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -25,3 +25,8 @@ import PRODUCTION/utility.lm; (assert-typeof( ((() 1) 2) List )); (assert-not-typeof( ((() 1) 2) List )); (assert-not-typeof( ((() 1) 2) List )); + +(assert-typeof( () List<[Atom,Nil]> )); +(assert-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Nil]> )); +(assert-typeof( ((() (1 ()) ) (2 ()) ) List<[Nil,Nil]> )); +(assert-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Atom]> )); From 2094ef1e68b13cf88bb8252d1919f230576209e0 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:25:15 -0600 Subject: [PATCH 11/16] parse slightly more complex type --- PRODUCTION/utility.lm | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index c548d0868..2bafc92bb 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -296,6 +296,36 @@ parse-parameter-typeof := λ tt . (tail( (parse-typeof (clone-rope inner)) )); +parse-tuple-typeof := λ tt . (tail( + (assert-eq( '[ (head-string tt) )) + (set tt (tail-string tt)) + (local inner) + (local base) + (while tt ( + (match (head-string tt) ( + () + ('] ( (assert-eq( () (tail-string tt) )) )) + (', (tail( + (set inner (parse-typeof (clone-rope inner) )) + (if base ( + (set base ('[] ( base inner ))) + ) ( + (set base inner) + )) + (set inner ()) + ))) + (c (set inner (inner (clone-rope c)) )) + )) + (set tt (tail-string tt)) + )) + (if base ( + (set base ('[] ( base (parse-typeof (clone-rope inner )) ))) + ) ( + (set base (parse-typeof (clone-rope inner))) + )) + base +)); + parse-typeof := λ tt . (tail( (local buff) (local base) @@ -306,7 +336,10 @@ parse-typeof := λ tt . (tail( (while tt ( (match (head-string tt) ( () - ('[ (fail (TODO Array Typeof tt))) + ('[ ( + (set base ( (clone-rope buff) (parse-tuple-typeof tt) )) + (set tt ()) + )) ('< ( (set base ( (clone-rope buff) (parse-parameter-typeof tt) )) (set tt ()) From 68c0452c6250245b04665401cd348d861b0eccf6 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:33:55 -0600 Subject: [PATCH 12/16] structural typing works --- PRODUCTION/utility.lm | 9 ++++++++- tests/unit/utility.lm | 4 ++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 2bafc92bb..76c9a7804 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -337,7 +337,7 @@ parse-typeof := λ tt . (tail( (match (head-string tt) ( () ('[ ( - (set base ( (clone-rope buff) (parse-tuple-typeof tt) )) + (set base (parse-tuple-typeof tt)) (set tt ()) )) ('< ( @@ -365,6 +365,13 @@ is-typeof := λ term tt . (match tt ( (not term) )) )) + ( ('[] ( lt rt )) ( + (if (is-cons term) ( + (if (is-typeof( (head term) lt )) ( + (is-typeof( (tail term) rt )) + ) ()) + ) ()) + )) ( (l r) (fail (UnknownTypeofType tt))) ( () (fail (UnknownTypeofType tt))) ( label (eq( (head term) label )) ) diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index bd802ce18..30c7c6203 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -28,5 +28,5 @@ import PRODUCTION/utility.lm; (assert-typeof( () List<[Atom,Nil]> )); (assert-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Nil]> )); -(assert-typeof( ((() (1 ()) ) (2 ()) ) List<[Nil,Nil]> )); -(assert-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Atom]> )); +(assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Nil,Nil]> )); +(assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Atom]> )); From b842dfdb5ce79f19f0530e484cee3a50313e2508 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:36:21 -0600 Subject: [PATCH 13/16] try recursive descent parsing --- tests/unit/utility.lm | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index 30c7c6203..edf7b3e6f 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -30,3 +30,8 @@ import PRODUCTION/utility.lm; (assert-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Nil]> )); (assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Nil,Nil]> )); (assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Atom]> )); + +(assert-typeof( () List> )); +(assert-typeof( ( () (() '1) ) List> )); +(assert-not-typeof( ( () (() '1) ) List> )); +(assert-not-typeof( ( () (() '1) ) List )); From f24a0520459ba9efcb9b85d62a0381883988cf00 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:40:12 -0600 Subject: [PATCH 14/16] parse typeof working --- PRODUCTION/utility.lm | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index 76c9a7804..e56b27b74 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -285,10 +285,21 @@ parse-parameter-typeof := λ tt . (tail( (assert-eq( '< (head-string tt) )) (set tt (tail-string tt)) (local inner) + (local depth) (while tt ( (match (head-string tt) ( () - ('> ( (assert-eq( () (tail-string tt) )) )) + ('< (tail( + (set inner (inner '[)) + (set depth (inc depth)) + ))) + ('> ( + (if depth ( + (set depth (dec depth)) + ) ( + (assert-eq( () (tail-string tt) )) + )) + )) (c (set inner (inner (clone-rope c)) )) )) (set tt (tail-string tt)) @@ -301,10 +312,21 @@ parse-tuple-typeof := λ tt . (tail( (set tt (tail-string tt)) (local inner) (local base) + (local depth) (while tt ( (match (head-string tt) ( () - ('] ( (assert-eq( () (tail-string tt) )) )) + ('[ (tail( + (set inner (inner '[)) + (set depth (inc depth)) + ))) + ('] ( + (if depth ( + (set depth (dec depth)) + ) ( + (assert-eq( () (tail-string tt) )) + )) + )) (', (tail( (set inner (parse-typeof (clone-rope inner) )) (if base ( From 54650920e5a2a3098be6f6ea0d3c83b2a8e6e404 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:45:22 -0600 Subject: [PATCH 15/16] test --- tests/unit/utility.lm | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index edf7b3e6f..a757d01ff 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -3,6 +3,13 @@ import PRODUCTION/utility.lm; (assert-eq( True True )); +(assert-eq( (parse-typeof Nil) Nil )); +(assert-eq( (parse-typeof Atom) Atom )); +(assert-eq( (parse-typeof List) (List Atom) )); +(assert-eq( (parse-typeof List>) (List (List Atom)) )); +(assert-eq( (parse-typeof [Atom,Nil]) ('[] (Atom Nil)) )); +(assert-eq( (parse-typeof [Atom,Nil,Cons]) ('[]( ('[]( Atom Nil )) Cons )) )); + (assert-typeof( () Nil )); (assert-not-typeof( 1 Nil )); (assert-not-typeof( (1 2) Nil )); @@ -31,7 +38,7 @@ import PRODUCTION/utility.lm; (assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Nil,Nil]> )); (assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Atom]> )); -(assert-typeof( () List> )); -(assert-typeof( ( () (() '1) ) List> )); -(assert-not-typeof( ( () (() '1) ) List> )); -(assert-not-typeof( ( () (() '1) ) List )); +#(assert-typeof( () List> )); +#(assert-typeof( ( () (() '1) ) List> )); +#(assert-not-typeof( ( () (() '1) ) List> )); +#(assert-not-typeof( ( () (() '1) ) List )); From 185d40cf1d081d709d217638293b3a1ebd1128d0 Mon Sep 17 00:00:00 2001 From: Andrew Johnson Date: Sat, 16 Mar 2024 15:53:06 -0600 Subject: [PATCH 16/16] everything that I can think to test with dynamic typechecks works --- Cargo.toml | 2 +- PRODUCTION/utility.lm | 16 ++++++++++------ tests/unit/utility.lm | 15 ++++++++++----- 3 files changed, 21 insertions(+), 12 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index bdec8cb1a..625c2ae32 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "lambda_mountain" -version = "1.11.23" +version = "1.11.24" authors = ["Andrew "] license = "MIT" description = "Lambda Mountain" diff --git a/PRODUCTION/utility.lm b/PRODUCTION/utility.lm index e56b27b74..dd0d7a8b7 100644 --- a/PRODUCTION/utility.lm +++ b/PRODUCTION/utility.lm @@ -290,7 +290,7 @@ parse-parameter-typeof := λ tt . (tail( (match (head-string tt) ( () ('< (tail( - (set inner (inner '[)) + (set inner (inner '<)) (set depth (inc depth)) ))) ('> ( @@ -328,13 +328,17 @@ parse-tuple-typeof := λ tt . (tail( )) )) (', (tail( - (set inner (parse-typeof (clone-rope inner) )) - (if base ( - (set base ('[] ( base inner ))) + (if depth ( + (set inner (inner ',)) ) ( - (set base inner) + (set inner (parse-typeof (clone-rope inner) )) + (if base ( + (set base ('[] ( base inner ))) + ) ( + (set base inner) + )) + (set inner ()) )) - (set inner ()) ))) (c (set inner (inner (clone-rope c)) )) )) diff --git a/tests/unit/utility.lm b/tests/unit/utility.lm index a757d01ff..3cf18af0a 100644 --- a/tests/unit/utility.lm +++ b/tests/unit/utility.lm @@ -8,7 +8,9 @@ import PRODUCTION/utility.lm; (assert-eq( (parse-typeof List) (List Atom) )); (assert-eq( (parse-typeof List>) (List (List Atom)) )); (assert-eq( (parse-typeof [Atom,Nil]) ('[] (Atom Nil)) )); -(assert-eq( (parse-typeof [Atom,Nil,Cons]) ('[]( ('[]( Atom Nil )) Cons )) )); +(assert-eq( (parse-typeof [Atom,Nil,Cons]) ([] (([] (Atom Nil)) Cons)) )); + +(assert-eq( (parse-typeof [Atom,List<[Cons,Nil]>]) ([] (Atom (List ([] (Cons Nil))))) )); (assert-typeof( () Nil )); (assert-not-typeof( 1 Nil )); @@ -38,7 +40,10 @@ import PRODUCTION/utility.lm; (assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Nil,Nil]> )); (assert-not-typeof( ((() (1 ()) ) (2 ()) ) List<[Atom,Atom]> )); -#(assert-typeof( () List> )); -#(assert-typeof( ( () (() '1) ) List> )); -#(assert-not-typeof( ( () (() '1) ) List> )); -#(assert-not-typeof( ( () (() '1) ) List )); +(assert-typeof( () List> )); +(assert-typeof( ( () (() '1) ) List> )); +(assert-not-typeof( ( () (() '1) ) List> )); +(assert-not-typeof( ( () (() '1) ) List )); + +(assert-typeof( ( (1 2) () ) [Atom,Atom,Nil] )); +(assert-not-typeof( ( (1 2) () ) [Atom,Nil,Nil] ));