Skip to content

Commit

Permalink
Merge pull request #1122 from andrew-johnson-4/port-more-lm-to-lsts
Browse files Browse the repository at this point in the history
Port more lm to lsts
  • Loading branch information
andrew-johnson-4 authored Jan 18, 2025
2 parents ba90cd7 + b5ebbab commit f6818f4
Show file tree
Hide file tree
Showing 63 changed files with 22,425 additions and 22,465 deletions.
44,582 changes: 22,278 additions & 22,304 deletions BOOTSTRAP/cli.c

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "lambda_mountain"
version = "1.20.25"
version = "1.20.26"
authors = ["Andrew <[email protected]>"]
license = "MIT"
description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/BLOB/compile-blob.lm
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ plugins-backend-blob-compile := λ. (: (
(match rhs (
()
( (Abs( _ _ _ )) (
(let fragment (fragment::new()))
(let fragment (mk-fragment()))
(set fragment (.set( fragment 'fragment-type_s (SAtom 'Function_s) )))
(set.term( fragment rhs ))
(set.type( fragment (typeof rhs) ))
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/blob-render.lm
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ blob-render-simple := λ(: ctx FContext)(: context-key String)(: term AST)(: off
(while (non-zero rngs) (match rngs (
()
( (SCons( a rst )) (
(let f (fragment::expression a))
(let f (mk-expression a))
(let inner-ctx (fragment-context::bind( ctx lhs (t1 'L_s) f )))
(let cs (blob-render-simple( inner-ctx context-key iter offset )))
(let s (.1 cs))
Expand Down Expand Up @@ -161,7 +161,7 @@ blob-render-simple := λ(: ctx FContext)(: context-key String)(: term AST)(: off
))
))
( (App( (Abs( (Var( lhs _ )) ASTNil tlt )) rhs )) (
(let f (fragment::new()))
(let f (mk-fragment()))
(let cs (blob-render-simple( ctx context-key rhs offset )))
(let s (.1 cs))
(set f (.set( f context-key s )))
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/cc-blob.lm
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ cc-blob := λ(: caller-ctx FContext)(: function-name String)(: args AST)(: offse
# callee context starts as global-ctx
# caller context is provided but not propagated
(let f (fragment-context::lookup( caller-ctx function-name (typeof args) args )))
(let r (fragment::new()))
(let r (mk-fragment()))
(match (.term f) (
()
( (Abs( lhs rhs tlt )) (
Expand All @@ -21,7 +21,7 @@ cc-blob := λ(: caller-ctx FContext)(: function-name String)(: args AST)(: offse

cc-blob := λ(: callee-ctx FContext)(: function-name String)(: args-tt Type)(: offset I64)(: blame AST). (: (
(let f (fragment-context::lookup( callee-ctx function-name args-tt blame )))
(let r (fragment::new()))
(let r (mk-fragment()))
(match (.term f) (
()
( (Abs( lhs rhs tlt )) (
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/compile-c.lm
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ plugins-backend-c-compile := λ . (: (
( (Seq( rst (Glb( k_t rhs )) )) (
(if (==( k 'main_s )) (set assemble-argv-referenced True_u8) ())
(let kt (typeof rhs))
(let fragment (fragment::new()))
(let fragment (mk-fragment()))
(if (.is-open kt) () (
(if (.is-t( kt 'Blob_s )) (
(set.term( fragment rhs ))
Expand All @@ -26,7 +26,7 @@ plugins-backend-c-compile := λ . (: (
global-ctx k kt fragment
)))
) (
(let repr-tt (and( clean-tt (t1 'GlobalVariable_s) )))
(let repr-tt (+( clean-tt (t1 'GlobalVariable_s) )))
(set.type( fragment (without-constructor repr-tt) ))
(set global-ctx (fragment-context::bind(
global-ctx k (without-constructor repr-tt) fragment
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-constructor.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

compile-constructor := λ(: ctx FContext)(: tag-name String)(: return-type Type)(: args-type Type)(: args AST)(: offset I64). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(let bare-ordinal (with-only-class return-type))
(let case-number (index-of-tag tag-name))
(set r (initialize-c-struct( ctx args case-number 1_u64 )))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-declare-cstring.lm
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ compile-declare-cstring := λ(: val String). (: (
) Fragment);

compile-declare-cstring-c := λ(: val String). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(set r (.set( r 'expression_s (
(+(
(SAtom '"_s)
Expand Down
40 changes: 20 additions & 20 deletions PLUGINS/BACKEND/C/compile-expr-direct.lm
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
compile-smart-string-index := (: (HashtableEq( 0_u64 0_u64 (as 0_u64 Tuple<String,String>[]) )) HashtableEq<String,String>);

compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used IsUsed). (: (
(let e (fragment::new()))
(let e (mk-fragment()))
(set.context( e (close ctx) ))
(match term (
()
Expand Down Expand Up @@ -64,12 +64,12 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
(+( (SAtom ',\s"_s) (escape-c-string val) )) ))
(SAtom '",\sREG_EXTENDED\]\:if\[return_code\]{fprintf\[stderr,"Could\snot\scompile\sregex."\]\:exit\[1\]\:}}\:\n_s) ))
)))
(set e (fragment::expression rgx-id))
(set e (mk-expression rgx-id))
) ())
) (
(let isa-fragment False_u8)
(if (==( isa-fragment True_u8 )) (
(set e (fragment::expression val))
(set e (mk-expression val))
) (
(if (non-zero(class-of-tag val)) (
(let tag-index (index-of-tag val))
Expand All @@ -91,16 +91,16 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
) (
(match val (
()
( 'True_s (set e (fragment::expression '\[1\]_s)) )
( 'False_s (set e (fragment::expression '\[0\]_s)) )
( '\\t_s (set e (fragment::expression '\[9\]_s)) )
( '\\n_s (set e (fragment::expression '\[10\]_s)) )
( '\\s_s (set e (fragment::expression '\[32\]_s)) )
( '\\o_s (set e (fragment::expression '\[35\]_s)) )
( '\\`_s (set e (fragment::expression '\[39\]_s)) )
( '\\[_s (set e (fragment::expression '\[40\]_s)) )
( '\\]_s (set e (fragment::expression '\[41\]_s)) )
( '\\:_s (set e (fragment::expression '\[59\]_s)) )
( 'True_s (set e (mk-expression '\[1\]_s)) )
( 'False_s (set e (mk-expression '\[0\]_s)) )
( '\\t_s (set e (mk-expression '\[9\]_s)) )
( '\\n_s (set e (mk-expression '\[10\]_s)) )
( '\\s_s (set e (mk-expression '\[32\]_s)) )
( '\\o_s (set e (mk-expression '\[35\]_s)) )
( '\\`_s (set e (mk-expression '\[39\]_s)) )
( '\\[_s (set e (mk-expression '\[40\]_s)) )
( '\\]_s (set e (mk-expression '\[41\]_s)) )
( '\\:_s (set e (mk-expression '\[59\]_s)) )
( _ (
(if (.is-t( ltype 'L_s )) (
(set e (.set( e 'expression_s (SAtom val) )))
Expand Down Expand Up @@ -144,7 +144,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
))
))
( (App( (Var( 'sizeof_s _ )) (AType tt) )) (
(set e (fragment::expression(
(set e (mk-expression(
(+( (SAtom '\[sizeof\[_s)
(+( (mangle-c-type tt) (SAtom '\]\]_s) ))
))
Expand Down Expand Up @@ -181,16 +181,16 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
( (App( (App( (App( (Var( 'if_s _ )) cond )) t )) f )) (
(let rsp-offset (+( stack-offset -8_i64 )))
(let ec (cc-blob( ctx 'into-branch-conditional_s cond rsp-offset )))
(let et (compile-expr( (open(.context ec)) t (.offset ec) Tail )))
(let end-offset (.offset et))
(let et (compile-expr( (open(.context ec)) t 0_i64 Tail )))
(let end-offset 0_i64)
(set.type( et (typeof t) ))
(let ef (compile-expr( (open(.context ec)) f (.offset ec) Tail )))
(let ef (compile-expr( (open(.context ec)) f 0_i64 Tail )))
(set.type( ef (typeof f) ))
(if (.is-t( (typeof f) 'Never_s )) (
(set ef (never-as-expr-type( ef (typeof t) )))
) ())

(let ictx (fragment::new()))
(let ictx (mk-fragment()))
(set.type( ictx (t1( 'ImplicitContext_s )) ))

(set ctx (fragment-context::bind( ctx 'ictx_s (t1 'ImplicitContext_s) ictx )))
Expand Down Expand Up @@ -313,12 +313,12 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
) (
(if (is( used Unused )) (scope(
(let e1 (compile-expr( ctx f stack-offset Unused )))
(let e2 (compile-expr( (open(.context e1)) a (.offset e1) Unused )))
(let e2 (compile-expr( (open(.context e1)) a 0_i64 Unused )))
(set e (fragment::chain( e1 e2 )))
(set.type( e (typeof term) ))
)) (scope(
(let e1 (compile-expr( ctx f stack-offset Unused )))
(let e2 (compile-expr( (open(.context e1)) a (.offset e1) Used )))
(let e2 (compile-expr( (open(.context e1)) a 0_i64 Used )))
(set e (fragment::chain( e1 e2 )))
(set.type( e (typeof term) ))
)))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-expr.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

compile-expr := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used IsUsed). (: (
(let e (fragment::new()))
(let e (mk-fragment()))
(match used (
()
( Return (
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-global.lm
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ compile-global-c := λ(: ctx FContext)(: k String)(: term AST). (: (
( (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))
(set ctx (compile-destructure-args( args-type ctx lhs 0_i64 (.is-t( tlt 'Blob_s )) )))
(let e (fragment::new()))
(let e (mk-fragment()))
(let function-name 'main_s)
(if (==( k 'main_s )) (
(set e (compile-expr( ctx rhs 0_i64 Unused )))
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/compile-push-rvalue.lm
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,15 @@ compile-push-rvalue := λ(: ctx FContext)(: rval AST)(: offset I64). (: (
) Fragment);

compile-push-rvalue := λ(: ctx FContext)(: rval AST)(: offset I64)(: count U64)(: left-assoc U64). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(match (slot( (typeof rval) 'Cons_s )) (
()
( (TGround( 'Cons_s (LCons( p2 (LCons( p1 LEOF )) )) )) (
(match rval (
()
( (App( le re )) (
(let e1 (compile-push-rvalue( ctx le offset count left-assoc )))
(let e2 (compile-expr( ctx re (.offset e1) Used )))
(let e2 (compile-expr( ctx re 0_i64 Used )))
(set r (fragment::chain( e1 e2 )))
(if left-assoc (
(set r (.set( r 'expression_s (
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-stack-call-push-args.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

compile-stack-call-push-args := λ(: ctx FContext)(: args AST)(: stack-offset I64). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(match args (
()
( ASTNil (
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/C/compile-stack-call.lm
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
compile-stack-call := λ(: ctx FContext)(: f Fragment)(: function-name String)(: return-type Type)(: args AST)(: offset I64)(: used IsUsed). (: (
(let original-ctx ctx)
(let function-type (.type f))
(let r (fragment::new()))
(let r (mk-fragment()))

(if (.is-t( function-type 'Blob_s )) (
(set r (cc-blob( ctx function-name args offset )))
Expand All @@ -17,7 +17,7 @@ compile-stack-call := λ(: ctx FContext)(: f Fragment)(: function-name String)(:
(set.type( push-args (t1( 'FunctionArguments_s )) ))
(let call SNil)

(let ictx (fragment::new()))
(let ictx (mk-fragment()))

(let function-id function-name)
(if (.is-t( function-type 'FFI_s )) () (
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/compile-stack-calls.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

compile-stack-calls := λ(: ctx FContext)(: function-name String)(: function-type Type)(: return-type Type)(: args AST)(: offset I64)(: used IsUsed). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(let fs (fragment-context::lookups( ctx function-name function-type (typeof args) args )))
(for-each (f in fs) (
(let r-tt (.type r))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/fragment::label.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

fragment::label := λ(: id String). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(set r (.set( r 'expression_s (SAtom id) )))
(set r (.set( r 'fragment-type_s (SAtom 'Label_s) )))
(set.type( r (t1 'Label_s) ))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/fragment::local-variable.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

fragment::local-variable := λ(: offset I64)(: tt Type). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(set r (.set( r 'expression_s (SAtom(uuid())) )))
(set r (.set( r 'fragment-type_s (SAtom 'LocalVariable_s) )))
(set.type( r tt ))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/C/initialize-c-struct.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

initialize-c-struct := λ(: ctx FContext)(: rval AST)(: case-number U64)(: field-index U64). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(match (slot( (typeof rval) 'Cons_s )) (
()
( (TGround( 'Cons_s (LCons( par2 (LCons( par1 LEOF )) )) )) (
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/GNU-X86/blob-render.lm
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ blob-render-simple := λ(: ctx FContext)(: context-key String)(: term AST)(: off
(while (non-zero rngs) (match rngs (
()
( (SCons( a rst )) (
(let f (fragment::expression a))
(let f (mk-expression a))
(let inner-ctx (fragment-context::bind( ctx lhs (t1 'L_s) f )))
(let cs (blob-render-simple( inner-ctx context-key iter offset )))
(let s (.1 cs))
Expand Down Expand Up @@ -161,7 +161,7 @@ blob-render-simple := λ(: ctx FContext)(: context-key String)(: term AST)(: off
))
))
( (App( (Abs( (Var( lhs _ )) ASTNil tlt )) rhs )) (
(let f (fragment::new()))
(let f (mk-fragment()))
(let cs (blob-render-simple( ctx context-key rhs offset )))
(let s (.1 cs))
(set f (.set( f context-key s )))
Expand Down
4 changes: 2 additions & 2 deletions PLUGINS/BACKEND/GNU-X86/cc-blob.lm
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ cc-blob := λ(: caller-ctx FContext)(: function-name String)(: args AST)(: offse
# callee context starts as global-ctx
# caller context is provided but not propagated
(let f (fragment-context::lookup( caller-ctx function-name (typeof args) args )))
(let r (fragment::new()))
(let r (mk-fragment()))
(match (.term f) (
()
( (Abs( lhs rhs tlt )) (
Expand All @@ -26,7 +26,7 @@ cc-blob := λ(: caller-ctx FContext)(: function-name String)(: args AST)(: offse

cc-blob := λ(: callee-ctx FContext)(: function-name String)(: args-tt Type)(: offset I64)(: blame AST). (: (
(let f (fragment-context::lookup( callee-ctx function-name args-tt blame )))
(let r (fragment::new()))
(let r (mk-fragment()))
(match (.term f) (
()
( (Abs( lhs rhs tlt )) (
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/GNU-X86/compile-blob.lm
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ compile-blob := λ. (: (
(match rhs (
()
( (Abs( _ _ _ )) (
(let fragment (fragment::new()))
(let fragment (mk-fragment()))
(set fragment (.set( fragment 'fragment-type_s (SAtom 'Function_s) )))
(set fragment (.set-term( fragment rhs )))
(set fragment (.set-type( fragment (typeof rhs) )))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/GNU-X86/compile-c.lm
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ compile-c := λ . (: (
( (Seq( rst (Glb( k_t rhs )) )) (
(if (==( k 'main_s )) (set assemble-argv-referenced True_u8) ())
(let kt (typeof rhs))
(let fragment (fragment::new()))
(let fragment (mk-fragment()))
(if (is-open kt) () (
(if (is-blob kt) (
(set fragment (.set-term( fragment rhs )))
Expand Down
2 changes: 1 addition & 1 deletion PLUGINS/BACKEND/GNU-X86/compile-constructor.lm
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

compile-constructor := λ(: ctx FContext)(: tag-name String)(: return-type Type)(: args-type Type)(: args AST)(: offset I64). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(if (is( config-assemble-mode AssembleC )) (
(let bare-ordinal (with-only-class return-type))
(let c-type-name (.lookup( index-c-type-ordinal (normalize bare-ordinal) 'UnknownCTypename_s )))
Expand Down
8 changes: 4 additions & 4 deletions PLUGINS/BACKEND/GNU-X86/compile-declare-cstring.lm
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

cstring-cache := (: SSEOF StringStringList);
compile-declare-cstring := λ(: val String). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(match config-assemble-mode (
()
( AssembleC (set r (compile-declare-cstring-c( val ))))
Expand All @@ -12,13 +12,13 @@ compile-declare-cstring := λ(: val String). (: (
) Fragment);

compile-declare-cstring-blob := λ(: val String). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(print 'TODO\sdeclare\scstring\sblob\n_s)(exit 1_u64)
r
) Fragment);

compile-declare-cstring-c := λ(: val String). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(set r (.set( r 'expression_s (
(+(
(SAtom '"_s)
Expand Down Expand Up @@ -67,7 +67,7 @@ escape-c-string := λ(: s String). (: (
) S);

compile-declare-cstring-gnu := λ(: val String). (: (
(let r (fragment::new()))
(let r (mk-fragment()))
(if (is( config-assemble-mode AssembleBlob )) (
(set r (.set( r 'expression_s (SAtom val) )))
) (
Expand Down
Loading

0 comments on commit f6818f4

Please sign in to comment.