Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unit testing l2afm #1107

Merged
merged 4 commits into from
Jan 15, 2025
Merged

Unit testing l2afm #1107

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0a18cfb
is-t query
andrew-johnson-4 Jan 15, 2025
ca05d19
OK
andrew-johnson-4 Jan 15, 2025
f40de4f
t
andrew-johnson-4 Jan 15, 2025
fa2155f
start unit testing
andrew-johnson-4 Jan 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46,092 changes: 23,046 additions & 23,046 deletions BOOTSTRAP/cli.c
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)"
Expand Down
12 changes: 6 additions & 6 deletions PLUGINS/BACKEND/C/cc-args.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) (
Expand Down Expand Up @@ -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) (
Expand All @@ -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) )) )))
Expand All @@ -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) )) )))
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/compile-c-typedef.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
))
Expand All @@ -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)
))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-c.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/compile-destructure-args.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) )))
Expand Down
14 changes: 7 additions & 7 deletions PLUGINS/BACKEND/C/compile-expr-direct.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) )))
Expand All @@ -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
Expand Down Expand Up @@ -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 (
Expand All @@ -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 )) )) )) (
Expand Down Expand Up @@ -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) )))
) ())

Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/compile-global.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
)))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-maybe-push-stack.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )))
Expand Down
6 changes: 3 additions & 3 deletions PLUGINS/BACKEND/C/compile-stack-call.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) ())
Expand All @@ -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 )))
))

Expand Down
8 changes: 4 additions & 4 deletions PLUGINS/BACKEND/C/initialize-c-struct.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
))
))
Expand Down Expand Up @@ -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)
))
))
Expand Down
12 changes: 6 additions & 6 deletions SRC/apply.lsts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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) {
Expand All @@ -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) {
Expand All @@ -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));
};
};
Expand Down
4 changes: 2 additions & 2 deletions SRC/destructure-lhs.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )) (
Expand All @@ -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 () )
( _ (
Expand Down
6 changes: 3 additions & 3 deletions SRC/fragment-context::lookups.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>) )))
Expand All @@ -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>) )))
Expand Down
2 changes: 1 addition & 1 deletion SRC/global-is-seen.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
) (
Expand Down
3 changes: 0 additions & 3 deletions SRC/index-types.lm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down
Loading
Loading