Merge pull request #1107 from andrew-johnson-4/unit-testing-l2afm

Unit testing l2afm
andrew-johnson-4 · Jan 15, 2025 · a1c51d2 · a1c51d2
2 parents ebdbc55 + fa2155f
commit a1c51d2
Show file tree

Hide file tree

Showing 29 changed files with 23,148 additions and 23,141 deletions.
diff --git a/BOOTSTRAP/cli.c b/BOOTSTRAP/cli.c
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.20.17"
+version = "1.20.18"
 authors = ["Andrew <[email protected]>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

diff --git a/PLUGINS/BACKEND/C/cc-args.lm b/PLUGINS/BACKEND/C/cc-args.lm
@@ -5,11 +5,11 @@ cc-args := λ(: callee-ctx FContext)(: caller-ctx FContext)(: lhs AST)(: rhs AST
    (match lhs (
       ()
       ( (App( lhs-rst (App( (Lit( ':_s _ )) (App( (Var( k _ )) (AType kt) )) )) )) (
-         (if (is-t( (typeof rhs) 'Cons_s )) (scope(
+         (if (.is-t( (typeof rhs) 'Cons_s )) (scope(
             (match rhs (
                ()
                ( (App( le re )) (
-                  (if (is-t( kt '..._s )) (
+                  (if (.is-t( kt '..._s )) (
                      (set kt (get-vararg-inner kt))
                      (if (can-unify( kt (typeof re) )) (scope(
                         (if (is-open kt) (
@@ -40,7 +40,7 @@ cc-args := λ(: callee-ctx FContext)(: caller-ctx FContext)(: lhs AST)(: rhs AST
                ))
             ))
          )) (
-            (if (is-t( kt '..._s )) (
+            (if (.is-t( kt '..._s )) (
                (set kt (get-vararg-inner kt))
                (if (can-unify( kt (typeof rhs) )) (scope(
                   (if (is-open kt) (
@@ -65,11 +65,11 @@ cc-args := λ(: callee-ctx FContext)(: caller-ctx FContext)(: lhs AST)(: rhs AST
          ))
       ))
       ( (App( (Lit( ':_s _ )) (App( (Var( k _ )) (AType kt) )) )) (
-         (if (is-t( (typeof rhs) 'Cons_s )) (
+         (if (.is-t( (typeof rhs) 'Cons_s )) (
             (match rhs (
                ()
                ( (App( le re )) (
-                  (if (is-t( kt '..._s )) (scope(
+                  (if (.is-t( kt '..._s )) (scope(
                      (set kt (get-vararg-inner kt))
                      (if (is-open kt) (
                         (set callee-ctx (union( callee-ctx (unify( kt (typeof re) )) )))
@@ -87,7 +87,7 @@ cc-args := λ(: callee-ctx FContext)(: caller-ctx FContext)(: lhs AST)(: rhs AST
                ))
             ))
          ) (
-            (if (is-t( kt '..._s )) (scope(
+            (if (.is-t( kt '..._s )) (scope(
                (set kt (get-vararg-inner kt))
                (if (is-open kt) (
                   (set callee-ctx (union( callee-ctx (unify( kt (typeof rhs) )) )))

diff --git a/PLUGINS/BACKEND/C/compile-c-typedef.lm b/PLUGINS/BACKEND/C/compile-c-typedef.lm
@@ -101,7 +101,7 @@ compile-c-typedef-concrete := λ(: tctx TContext)(: base-type Type)(: body AST).
             (let fields (compile-c-fields-of-case( base-type case-definition case-number )))
             (set fields (substitute( tctx fields )))
             (set incomplete (||( incomplete (is-incomplete-typedef fields) )))
-            (if (is-t( fields 'Nil_s )) () (
+            (if (.is-t( fields 'Nil_s )) () (
                (set cases (+( cases (compile-c-casedef( tctx fields case-number )) )))
                (set has-case 1_u64)
             ))
@@ -112,7 +112,7 @@ compile-c-typedef-concrete := λ(: tctx TContext)(: base-type Type)(: body AST).
             (let fields (compile-c-fields-of-case( base-type case-definition case-number )))
             (set fields (substitute( tctx fields )))
             (set incomplete (||( incomplete (is-incomplete-typedef fields) )))
-            (if (is-t( fields 'Nil_s )) () (
+            (if (.is-t( fields 'Nil_s )) () (
                (set cases (+( cases (compile-c-casedef( tctx fields case-number )) )))
                (set has-case 1_u64)
             ))

diff --git a/PLUGINS/BACKEND/C/compile-c.lm b/PLUGINS/BACKEND/C/compile-c.lm
@@ -9,7 +9,7 @@ plugins-backend-c-compile := λ . (: (
          (let kt (typeof rhs))
          (let fragment (fragment::new()))
          (if (is-open kt) () (
-            (if (is-t( kt 'Blob_s )) (
+            (if (.is-t( kt 'Blob_s )) (
                (set.term( fragment rhs ))
                (set.type( fragment kt ))
                (set global-ctx (fragment-context::bind(

diff --git a/PLUGINS/BACKEND/C/compile-destructure-args.lm b/PLUGINS/BACKEND/C/compile-destructure-args.lm
@@ -3,8 +3,8 @@ compile-destructure-args := λ(: tt Type)(: ctx FContext)(: lhs AST)(: offset I6
    (match lhs (
       ()
       ( (App( rst (App( (Lit( ':_s _ )) (App( (Var( k _ )) (AType kt) )) )) )) (
-         (if (is-t( tt 'Cons_s )) (
-            (let rst-tt (p2 tt))
+         (if (.is-t( tt 'Cons_s )) (
+            (let rst-tt (.p2 tt))
             (set ctx (compile-destructure-args( rst-tt ctx rst offset is-fragment )))
             (let rst-sz (sizeof-aligned rst-tt))
             (let rst-offset (-( offset (as rst-sz I64) )))

diff --git a/PLUGINS/BACKEND/C/compile-expr-direct.lm b/PLUGINS/BACKEND/C/compile-expr-direct.lm
@@ -21,11 +21,11 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
       ))
       ( (Lit( val _ )) (
          (let ltype (typeof term))
-         (if (||( (||( (is-t( ltype 'String_s )) (is-t( ltype 'SmartString_s )) )) (is-t( ltype 'Regex_s )) )) (
-            (if (is-t( ltype 'String_s )) (
+         (if (||( (||( (.is-t( ltype 'String_s )) (.is-t( ltype 'SmartString_s )) )) (.is-t( ltype 'Regex_s )) )) (
+            (if (.is-t( ltype 'String_s )) (
                (set e (compile-declare-cstring( val )))
             ) ())
-            (if (is-t( ltype 'SmartString_s )) (
+            (if (.is-t( ltype 'SmartString_s )) (
                (let guid (.lookup( compile-smart-string-index val '_s )))
                (if (non-zero guid) (
                   (set e (fragment::set( e 'expression_s (SAtom guid) )))
@@ -52,7 +52,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
                   )))
                ))
             ) ())
-            (if (is-t( ltype 'Regex_s )) (
+            (if (.is-t( ltype 'Regex_s )) (
                (let rgx-id (uuid()))
                (set assemble-header-section (+(
                   assemble-header-section
@@ -102,7 +102,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
                      ( '\\]_s (set e (fragment::expression '\[41\]_s)) )
                      ( '\\:_s (set e (fragment::expression '\[59\]_s)) )
                      ( _ (
-                        (if (is-t( ltype 'L_s )) (
+                        (if (.is-t( ltype 'L_s )) (
                            (set e (fragment::set( e 'expression_s (SAtom val) )))
                         ) (
                            (set e (fragment::set( e 'expression_s (
@@ -126,7 +126,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
       ))
       ( (App( (Var( 'open_s _ )) t )) (
          (let tt (typeof t))
-         (if (is-t( tt 'Array_s )) (
+         (if (.is-t( tt 'Array_s )) (
             (match (slot( tt 'Array_s )) (
                ()
                ( (TGround( 'Array_s (LCons( _ (LCons( TAny LEOF )) )) )) (
@@ -190,7 +190,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
          (set.type( et (typeof t) ))
          (let ef (compile-expr( (open(.context ec)) f (.offset ec) Tail )))
          (set.type( ef (typeof f) ))
-         (if (is-t( (typeof f) 'Never_s )) (
+         (if (.is-t( (typeof f) 'Never_s )) (
             (set ef (never-as-expr-type( ef (typeof t) )))
          ) ())
 

diff --git a/PLUGINS/BACKEND/C/compile-global.lm b/PLUGINS/BACKEND/C/compile-global.lm
@@ -9,10 +9,10 @@ compile-global-c := λ(: ctx FContext)(: k String)(: term AST). (: (
    (let kt (typeof term))
    (match term (
       ()
-      ( (Abs( lhs rhs tlt )) (if (||( (is-open kt) (||( (is-t( tlt 'Blob_s )) (||( (is-t( tlt 'FFI_s )) (is-t( tlt 'Prop_s )) )) )) )) () (
+      ( (Abs( lhs rhs tlt )) (if (||( (is-open kt) (||( (.is-t( tlt 'Blob_s )) (||( (.is-t( tlt 'FFI_s )) (.is-t( tlt 'Prop_s )) )) )) )) () (
          (let args-type (domain kt))
          (let args-size (sizeof-aligned args-type))
-         (set ctx (compile-destructure-args( args-type ctx lhs 0_i64 (is-t( tlt 'Blob_s )) )))
+         (set ctx (compile-destructure-args( args-type ctx lhs 0_i64 (.is-t( tlt 'Blob_s )) )))
          (set ctx (FCtxBind( (close ctx) 'cdecl::args-size_s TAny
             (fragment::expression(to-string args-size))
          )))

diff --git a/PLUGINS/BACKEND/C/compile-maybe-push-stack.lm b/PLUGINS/BACKEND/C/compile-maybe-push-stack.lm
@@ -2,7 +2,7 @@
 compile-maybe-push-stack := λ(: ctx FContext)(: offset I64)(: fragment Fragment)(: expression-type Type)(: sloc AST). (: (
    (let ft (.type( fragment )))
    (if (non-zero ft) () (set ft expression-type))
-   (if (is-t( ft 'StackVariable_s )) () (
+   (if (.is-t( ft 'StackVariable_s )) () (
       (let callee-ctx ctx)
       (set callee-ctx (fragment-context::bind( callee-ctx 'src_s (denormalize ft) fragment )))
       (set fragment (cc-blob( callee-ctx 'push_s (denormalize ft) offset sloc )))

diff --git a/PLUGINS/BACKEND/C/compile-stack-call.lm b/PLUGINS/BACKEND/C/compile-stack-call.lm
@@ -4,11 +4,11 @@ compile-stack-call := λ(: ctx FContext)(: f Fragment)(: function-name String)(:
    (let function-type (.type f))
    (let r (fragment::new()))
 
-   (if (is-t( function-type 'Blob_s )) (
+   (if (.is-t( function-type 'Blob_s )) (
       (set r (cc-blob( ctx function-name args offset )))
       (set.context( r (close ctx) ))
    ) (
-      (if (is-t( function-type 'Prop_s )) (
+      (if (.is-t( function-type 'Prop_s )) (
          (set r (compile-expr( ctx args offset Used )))
       ) (
          (if (is( used Tail )) (set used Used) ())
@@ -21,7 +21,7 @@ compile-stack-call := λ(: ctx FContext)(: f Fragment)(: function-name String)(:
          (let ictx (fragment::new()))
 
          (let function-id function-name)
-         (if (is-t( function-type 'FFI_s )) () (
+         (if (.is-t( function-type 'FFI_s )) () (
             (set function-id (mangle-identifier( function-name function-type )))
          ))
 

diff --git a/PLUGINS/BACKEND/C/initialize-c-struct.lm b/PLUGINS/BACKEND/C/initialize-c-struct.lm
@@ -24,12 +24,12 @@ initialize-c-struct := λ(: ctx FContext)(: rval AST)(: case-number U64)(: field
                            (+(
                               (+(
                                  (SAtom ',sizeof\[_s)
-                                 (mangle-c-type(p2(slot( par1 'Array_s ))))
+                                 (mangle-c-type(.p2(slot( par1 'Array_s ))))
                               ))
                               (+(
                                  (SAtom '\]*_s)
                                  (+(
-                                    (SAtom(tag-of(p1(slot( par1 'Array_s )))))
+                                    (SAtom(tag-of(.p1(slot( par1 'Array_s )))))
                                     (SAtom '\]\:_s)
                                  ))
                               ))
@@ -70,12 +70,12 @@ initialize-c-struct := λ(: ctx FContext)(: rval AST)(: case-number U64)(: field
                      (+(
                         (+(
                            (SAtom ',sizeof\[_s)
-                           (mangle-c-type(p2(slot( par1 'Array_s ))))
+                           (mangle-c-type(.p2(slot( par1 'Array_s ))))
                         ))
                         (+(
                            (SAtom '\]*_s)
                            (+(
-                              (SAtom(tag-of(p1(slot( par1 'Array_s )))))
+                              (SAtom(tag-of(.p1(slot( par1 'Array_s )))))
                               (SAtom '\]\:_s)
                            ))
                         ))

diff --git a/SRC/apply.lsts b/SRC/apply.lsts
@@ -9,13 +9,13 @@ let apply-blame(function-name: CString, function-type: Type, parameters: Type, d
            "With Candidates:\n"
            "\{function-type.pretty}\n")
    };
-   if is-t(r.return-type, c"Error: Did Not Close Before Specialization") {
+   if r.return-type.is-t(c"Error: Did Not Close Before Specialization") {
       fail("Application\sDid\sNot\sClose\sBefore\sSpecialization:\n"
            "Function \{function-name}: \{function-type}\n"
            "Argument \{parameters}\n"
            "At \{location-of(blame)}\n");
    };
-   if is-t(r.return-type, c"Error: Function Application Yielded An Irreducible Plurality Of Matches") {
+   if r.return-type.is-t(c"Error: Function Application Yielded An Irreducible Plurality Of Matches") {
       fail("Function Application Yielded An Irreducible Plurality Of Matches\n"
            "\{function-name}\n"
            "With Arguments \{parameters}\n"
@@ -29,11 +29,11 @@ let apply-blame(function-name: CString, function-type: Type, parameters: Type, d
 let apply(function-name: CString, function-type: Type, parameters: Type, do-specialize: U64): ApplyResult = (
    let r = TAny {};
    let rs = apply-plural(function-name, function-type, parameters);
-   if not(is-t( function-type, c"Hook" )) {
+   if not(function-type.is-t( c"Hook" )) {
       rs = reduce-plural(rs);
    };
    let phi-types = [] :: List<Tuple<CString,Type>>;
-   if rs.length > 1 && not(is-t( function-type, c"Hook" )) {
+   if rs.length > 1 && not(function-type.is-t( c"Hook" )) {
       r = t1(c"Error: Function Application Yielded An Irreducible Plurality Of Matches");
       function-type = head(rs);
       for candidate in tail(rs) {
@@ -57,7 +57,7 @@ let apply(function-name: CString, function-type: Type, parameters: Type, do-spec
          } };
          let closed-type = substitute( ctx, sft );
          function-type = closed-type;
-         if not(is-t( r, c"Error: Did Not Close Before Specialization")) {
+         if not(r.is-t( c"Error: Did Not Close Before Specialization")) {
             r = substitute(ctx, frt);
          };
          if do-specialize && is-open(sft) {
@@ -67,7 +67,7 @@ let apply(function-name: CString, function-type: Type, parameters: Type, do-spec
             try-specialize(function-name, sft, ctx, closed-type);
          }
       };
-      if is-t(function-type, c"Prop") {
+      if function-type.is-t(c"Prop") {
          r = and(r, cons-root(parameters));
       };
    };

diff --git a/SRC/destructure-lhs.lm b/SRC/destructure-lhs.lm
@@ -15,7 +15,7 @@ destructure-lhs := λ(: ctx FContext)(: tt Type)(: lhs S)(: args FragmentList).
          ))
       ))
       ( (SCons( (SAtom 'App_s) (SCons( lhs-rst (SCons( (SAtom 'Var_s) (SAtom k) )) )) )) (
-         (let a-type (p1 tt))
+         (let a-type (.p1 tt))
          (match args (
             ()
             ( (FLSeq( fl-rst f )) (
@@ -26,7 +26,7 @@ destructure-lhs := λ(: ctx FContext)(: tt Type)(: lhs S)(: args FragmentList).
                (set args fl-rst)
             ))
          ))
-         (set ctx (destructure-lhs( ctx (p2 tt) lhs-rst args )))
+         (set ctx (destructure-lhs( ctx (.p2 tt) lhs-rst args )))
       ))
       ( SNil () )
       ( _ (

diff --git a/SRC/fragment-context::lookups.lm b/SRC/fragment-context::lookups.lm
@@ -22,15 +22,15 @@ fragment-context::lookups := λ(: ctx FContext)(: k String)(: ft Type)(: kt Type
                   (if (can-unify( domaint kt )) (
                      (if (non-zero found) (
                         (if (can-unify( found domaint )) (
-                           (if (!=( (is-t( rt 'Hook_s )) 0_u64 )) (
+                           (if (!=( (.is-t( rt 'Hook_s )) 0_u64 )) (
                               (set r (cons( rf r )))
                            ) (
                               (set r (cons( rf (: LEOF List<Fragment>) )))
                               (set found domaint)
                            ))
                         ) ())
                      ) (
-                        (if (!=( (is-t( rt 'Hook_s )) 0_u64 )) (
+                        (if (!=( (.is-t( rt 'Hook_s )) 0_u64 )) (
                            (set r (cons( rf r )))
                         ) (
                            (set r (cons( rf (: LEOF List<Fragment>) )))
@@ -40,7 +40,7 @@ fragment-context::lookups := λ(: ctx FContext)(: k String)(: ft Type)(: kt Type
                   ) ())
                   (set ctx rst)
                ) (
-                  (if (!=( (is-t( rt 'Hook_s )) 0_u64 )) (
+                  (if (!=( (.is-t( rt 'Hook_s )) 0_u64 )) (
                      (set r (cons( rf r )))
                   ) (
                      (set r (cons( rf (: LEOF List<Fragment>) )))

diff --git a/SRC/global-is-seen.lm b/SRC/global-is-seen.lm
@@ -2,7 +2,7 @@
 global-symbol-registry := (: (HashtableEq( 0_u64 0_u64 (as 0_u64 Tuple<Tuple<String,Type>,U64>[]) )) HashtableEq<Tuple<String,Type>,U64>);
 
 mark-global-as-seen := λ(: name String)(: tt Type)(: tlt Type). (: (
-   (if (&&( (&&( (global-is-seen( name tt )) (not(is-t( tlt 'Hook_s ))) )) (not(is-t( tlt 'FFI_s ))) )) (
+   (if (&&( (&&( (global-is-seen( name tt )) (not(.is-t( tlt 'Hook_s ))) )) (not(.is-t( tlt 'FFI_s ))) )) (
       (print 'Duplicate\sGlobal\sSymbol\s_s)(print name)(print '\s:\s_s)(print tt)(print '\n_s)
       (exit 1_u64)
    ) (

diff --git a/SRC/index-types.lm b/SRC/index-types.lm
@@ -5,7 +5,6 @@ import SRC/quick-prop.lsts;
 import SRC/cmp.lsts;
 
 import SRC/cons-root.lsts;
-import SRC/is-t.lm;
 import SRC/is-and.lsts;
 import SRC/index-concrete-type-instances.lm;
 import SRC/type-index.lm;
@@ -49,8 +48,6 @@ import SRC/typeof.lm;
 import SRC/to-s.lm;
 import SRC/domain.lm;
 import SRC/range.lm;
-import SRC/t.lm;
-import SRC/p.lm;
 import SRC/and.lm;
 import SRC/union.lm;
 import SRC/tag-of.lm;