Skip to content

Commit

Permalink
Merge pull request #849 from andrew-johnson-4/prune-optimize-6
Browse files Browse the repository at this point in the history
Prune optimize 6
  • Loading branch information
andrew-johnson-4 authored Oct 20, 2024
2 parents 0d65f6c + c58353c commit 4442ea2
Show file tree
Hide file tree
Showing 20 changed files with 26,475 additions and 27,279 deletions.
53,549 changes: 26,346 additions & 27,203 deletions BOOTSTRAP/cli.s

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.17.19"
version = "1.17.20"
authors = ["Andrew <andrew@subarctic.org>"]
license = "MIT"
description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"
Expand Down
3 changes: 3 additions & 0 deletions LIB/default-u64.lm
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@

import LIB/unop-macro.lm;
import LIB/binop-macro.lm;

meta
Expand All @@ -9,6 +10,8 @@ meta
;
fragment type U64; size U64 8; atom suffix U64 _u64;

(declare-unop( not '\tandq\s$1,%RAX\n\txor\s$1,%RAX\n_l U64 U64+Reg64 8_l 8_l Reg64 ));

(declare-binop( && '\tandq\s%R14,%RAX\n_l U64 U64+Reg64 8_l 8_l Reg64 ));
(declare-binop( || '\torq\s%R14,%RAX\n_l U64 U64+Reg64 8_l 8_l Reg64 ));
(declare-binop( + '\taddq\s%R14,%RAX\n_l U64 U64+Reg64 8_l 8_l Reg64 ));
Expand Down
3 changes: 3 additions & 0 deletions LIB/default-u8.lm
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@

import LIB/unop-macro.lm;
import LIB/binop-macro.lm;

meta
Expand All @@ -9,6 +10,8 @@ meta
;
fragment type U8; size U8 1; atom suffix U8 _u8;

(declare-unop( not '\tandq\s$1,%RAX\n\txor\s$1,%RAX\n_l U8 U8+Reg64 1_l 8_l Reg64 ));

(declare-binop( && '\tandb\s%R14B,%AL\n_l U8 U8+Reg8 1_l 1_l Reg8 ));
(declare-binop( || '\torb\s%R14B,%AL\n_l U8 U8+Reg8 1_l 1_l Reg8 ));
(declare-binop( + '\taddb\s%R14B,%AL\n_l U8 U8+Reg8 1_l 1_l Reg8 ));
Expand Down
42 changes: 42 additions & 0 deletions LIB/unop-macro.lm
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@

macro ('declare-unop (op-alias op-code op-type op-rtype op-size return-size reg-type)) (
op-alias := λ: Blob(: l op-type+Constant). (: (
(:program(
'\tmov\s$_s (:expression l) ',\s%_l (rax-of-size op-size) '\n_s
op-code
))
(:frame( (:frame l) ))
(:unframe( (:unframe l) ))
(:expression(rax-of-size return-size))
) op-rtype);
op-alias := λ: Blob(: l op-type+LocalVariable). (: (
(:program(
'\tmov\s_s (:expression l) '\[%RBP\],\s%_l (rax-of-size op-size) '\n_s
op-code
))
(:frame( (:frame l) ))
(:unframe( (:unframe l) ))
(:expression(rax-of-size return-size))
) op-rtype);
op-alias := λ: Blob(: l op-type+GlobalVariable). (: (
(:program(
'\tmov\s$_s (:expression l) ',\s%RAX\n_s
'\tmov\s0\[%RAX\],\s%_l (rax-of-size op-size) '\n_s
op-code
))
(:frame( (:frame l) ))
(:unframe( (:unframe l) ))
(:expression(rax-of-size return-size))
) op-rtype);
op-alias := λ: Blob(: l op-type+reg-type). (: (
(:program(
(:program l)
'\tmov\s%_s (:expression l) ',\s%_l (rax-of-size op-size) '\n_s
op-code
))
(:frame( (:frame l) ))
(:unframe( (:unframe l) ))
(:expression(rax-of-size return-size))
) op-rtype);
);

27 changes: 14 additions & 13 deletions SRC/compile-expr-direct.lm
Original file line number Diff line number Diff line change
Expand Up @@ -78,20 +78,21 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
))
( (App( (Var( 'open_s _ )) t )) (
(let tt (typeof t))
(match (slot( tt 'Array_s )) (
()
( (TGround( 'Array_s (LCons( _ (LCons( TAny LEOF )) )) )) (
(set e (compile-expr( ctx t stack-offset Used )))
) )
( (TGround( 'Array_s (LCons( TAny (LCons( inner-tt LEOF )) )) )) (
(set e (compile-stack-calls( ctx 'push-deref_s TAny (t1 'Nil_s) t stack-offset Used )))
(set e (fragment::set-type( e (and( (denormalize inner-tt) (t1 'StackVariable_s) )) )))
(let new-offset (-( stack-offset (as (sizeof-aligned inner-tt) I64) )))
(set e (fragment::set-offset( e new-offset )))
))
( _ (
(set e (compile-expr( ctx t stack-offset Used )))
(if (is-array tt) (
(match (slot( tt 'Array_s )) (
()
( (TGround( 'Array_s (LCons( _ (LCons( TAny LEOF )) )) )) (
(set e (compile-expr( ctx t stack-offset Used )))
) )
( (TGround( 'Array_s (LCons( TAny (LCons( inner-tt LEOF )) )) )) (
(set e (compile-stack-calls( ctx 'push-deref_s TAny (t1 'Nil_s) t stack-offset Used )))
(set e (fragment::set-type( e (and( (denormalize inner-tt) (t1 'StackVariable_s) )) )))
(let new-offset (-( stack-offset (as (sizeof-aligned inner-tt) I64) )))
(set e (fragment::set-offset( e new-offset )))
))
))
) (
(set e (compile-expr( ctx t stack-offset Used )))
))
))
( (App( (Var( 'sizeof_s _ )) (AType tt) )) (
Expand Down
34 changes: 0 additions & 34 deletions SRC/compile-fragment-args.lm

This file was deleted.

2 changes: 1 addition & 1 deletion SRC/compile-global.lm
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ compile-global := λ(: ctx FContext)(: k String)(: term AST). (: (
(let kt (typeof term))
(match term (
()
( (Abs( lhs rhs tlt )) (if (||( (is-open kt) (non-zero(slot( tlt 'Blob_s ))) )) () (
( (Abs( lhs rhs tlt )) (if (||( (is-open kt) (is-blob tlt) )) () (

(let args-type (domain kt))
(let args-size (sizeof-aligned args-type))
Expand Down
20 changes: 8 additions & 12 deletions SRC/compile-maybe-push-stack.lm
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,14 @@
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))
(match (slot( ft 'StackVariable_s )) (
()
( (TGround( '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 )))
(set fragment (fragment::set-type( fragment (and( (t1 'StackVariable_s) ft )) )))
(set fragment (fragment::set-context( fragment ctx )))
(let f-sz (as (sizeof-aligned ft) I64))
(set fragment (fragment::set-offset( fragment (-( offset f-sz )) )))
))
(if (is-stack-variable ft) () (
(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 )))
(set fragment (fragment::set-type( fragment (and( (t1 'StackVariable_s) ft )) )))
(set fragment (fragment::set-context( fragment ctx )))
(let f-sz (as (sizeof-aligned ft) I64))
(set fragment (fragment::set-offset( fragment (-( offset f-sz )) )))
))
fragment
) Fragment);
4 changes: 2 additions & 2 deletions SRC/compile-push-rvalue.lm
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ compile-push-rvalue := λ(: ctx FContext)(: rval AST)(: offset I64)(: count U64)
(let e1 (compile-push-rvalue( ctx le offset count )))
(if (!=( count 0_u64 )) (
(let re-tt (typeof re))
(if (non-zero(slot( re-tt 'Rc_s ))) (
(if (is-rc re-tt) (
(let inc-rc (Var( 'inc_s (token::new 'inc_s) )))
(set re-tt (guess-representation(without-representation re-tt)))
(ascript( inc-rc (t3( 'Arrow_s (typeof re) re-tt )) ))
Expand All @@ -39,7 +39,7 @@ compile-push-rvalue := λ(: ctx FContext)(: rval AST)(: offset I64)(: count U64)
) (
(if (!=( count 0_u64 )) (
(let rval-tt (typeof rval))
(if (non-zero(slot( rval-tt 'Rc_s ))) (
(if (is-rc rval-tt) (
(let inc-rc (Var( 'inc_s (token::new 'inc_s) )))
(set rval-tt (guess-representation(without-representation rval-tt)))
(ascript( inc-rc (t3( 'Arrow_s (typeof rval) rval-tt )) ))
Expand Down
2 changes: 1 addition & 1 deletion SRC/compile-stack-call.lm
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ compile-stack-call := λ(: ctx FContext)(: f Fragment)(: function-name String)(:
(let function-type (.type f))
(let r (fragment::new()))

(if (non-zero(slot( function-type 'Blob_s ))) (
(if (is-blob function-type) (
(set r (cc-blob( ctx function-name args offset )))
(set r (fragment::set-context( r ctx )))
) (
Expand Down
2 changes: 1 addition & 1 deletion SRC/global-is-seen.lm
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
global-symbol-registry := (: BTreeEqEOF BTreeEq<Tuple<String,Type>,U64>);

mark-global-as-seen := λ(: name String)(: tt Type)(: tlt Type). (: (
(if (&&( (global-is-seen( name tt )) (not(non-zero(slot( tlt 'Hook_s )))) )) (
(if (&&( (global-is-seen( name tt )) (not(is-hook tlt)) )) (
(print 'Duplicate\sGlobal\sSymbol\s_s)(print name)(print '\s:\s_s)(print tt)(print '\n_s)
(exit 1_u64)
) (
Expand Down
3 changes: 3 additions & 0 deletions SRC/index-ast.lm
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,14 @@ import SRC/align.lm;
import SRC/is-nil.lm;
import SRC/is-seq.lm;
import SRC/is-arrow.lm;
import SRC/is-array.lm;
import SRC/is-hook.lm;
import SRC/is-blob.lm;
import SRC/is-stack-variable.lm;
import SRC/is-cons.lm;
import SRC/is-impure-ctx.lm;
import SRC/is-string.lm;
import SRC/is-rc.lm;
import SRC/is-onto-stack.lm;
import SRC/is-impure-offset.lm;
import SRC/is-branchconditional.lm;
Expand Down
1 change: 0 additions & 1 deletion SRC/index-codegen.lm
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ import SRC/compile-declare-cstring.lm;
import SRC/compile-destructure-args.lm;
import SRC/compile-expr-direct.lm;
import SRC/compile-expr.lm;
import SRC/compile-fragment-args.lm;
import SRC/compile-global.lm;
import SRC/compile-maybe-push-stack.lm;
import SRC/compile-push-rvalue.lm;
Expand Down
12 changes: 5 additions & 7 deletions SRC/infer-expr.lm
Original file line number Diff line number Diff line change
Expand Up @@ -101,13 +101,11 @@ infer-expr := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type)(:
(if (non-zero inner-repr) (
(set tt (and( tt inner-repr )))
) ())
(if (non-zero(slot( tt 'AsOnly_s ))) () (
(let inner-class (with-only-class inner-tt))
(if (non-zero inner-class) (
(set tt (and( tt inner-class )))
) ())
(set tt (with-fields( tt )))
))
(let inner-class (with-only-class inner-tt))
(if (non-zero inner-class) (
(set tt (and( tt inner-class )))
) ())
(set tt (with-fields( tt )))
(ascript-normal( term tt ))
) ())
))
Expand Down
11 changes: 11 additions & 0 deletions SRC/is-array.lm
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@

is-array := λ(: tt Type). (: (
(let r 0_u64)
(match tt (
()
( (TAnd( t1 t2 )) (set r (||( (is-array t1) (is-array t2) ))) )
( (TGround( 'Array_s _ )) (set r 1_u64) )
( _ () )
))
r
) U64);
11 changes: 11 additions & 0 deletions SRC/is-rc.lm
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@

is-rc := λ(: tt Type). (: (
(let r 0_u64)
(match tt (
()
( (TAnd( t1 t2 )) (set r (||( (is-rc t1) (is-rc t2) ))) )
( (TGround( 'Rc_s _ )) (set r 1_u64) )
( _ () )
))
r
) U64);
11 changes: 11 additions & 0 deletions SRC/is-stack-variable.lm
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@

is-stack-variable := λ(: tt Type). (: (
(let r 0_u64)
(match tt (
()
( (TAnd( t1 t2 )) (set r (||( (is-stack-variable t1) (is-stack-variable t2) ))) )
( (TGround( 'StackVariable_s _ )) (set r 1_u64) )
( _ () )
))
r
) U64);
11 changes: 10 additions & 1 deletion SRC/is-vararg.lm
Original file line number Diff line number Diff line change
@@ -1,2 +1,11 @@

is-vararg := λ(: tt Type). (: (non-zero(slot( tt '..._s ))) U64)
is-vararg := λ(: tt Type). (: (
(let r 0_u64)
(match tt (
()
( (TAnd( t1 t2 )) (set r (||( (is-vararg t1) (is-vararg t2) ))) )
( (TGround( '..._s _ )) (set r 1_u64) )
( _ () )
))
r
) U64);
4 changes: 2 additions & 2 deletions SRC/try-specialize.lm
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ try-specialize := λ(: function-name String)(: ft Type)(: unify-ctx TContext)(:
( (TCtxBind( rst k kt t )) (
(if (==( function-name k )) (
(let special-type result-type)
(if (non-zero(slot( kt 'Blob_s ))) () (
(if (is-blob kt) () (
(set special-type (normalize special-type))
))
(set kt (slot( kt 'Arrow_s )))
(if (is-special( function-name special-type )) () (
(set kt (slot( kt 'Arrow_s )))
(if (==( ft kt )) (
(match t (
()
Expand Down

0 comments on commit 4442ea2

Please sign in to comment.