Merge pull request #828 from andrew-johnson-4/unpush-7

Unpush 7

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.17.12"
+version = "1.17.13"
 authors = ["Andrew <andrew@subarctic.org>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

LIB/default-instruction-set.lm

@@ -146,54 +146,13 @@ push-deref := λ: Blob(: src LocalVariable+Array<Sized<size>,?>). (: (
    ))
 ) Nil);
 
-fragment  push := λ(: src Sized<0>). (: () Nil);
-
-fragment  push := λ(: src GlobalVariable+Sized<size>). (: (
-   (.program (
-      (\t 'mov \s '$ (.expression src) , \s '%r15 \n)
-      (for word-offset in (range( 0 (/( (.expression size) 8 )) )) (
-         \t 'pushq \s (+( (+( (.expression size) '-8 )) (inv(*( (.expression word-offset) 8 ))) )) \[ '%r15 \] \n
-      ))
-      (if-eq (.expression size) 4 (
-         \t 'mov \s '0 \[ '%r15 \] , \s '%r15d \n
-         \t 'push \s '%r15 \n
-      ))
-      (if-eq (.expression size) 2 (
-         \t 'mov \s '0 \[ '%r15 \] , \s '%r15w \n
-         \t 'push \s '%r15 \n
-      ))
-      (if-eq (.expression size) 1 (
-         \t 'mov \s '0 \[ '%r15 \] , \s '%r15b \n
-         \t 'push \s '%r15 \n
-      ))
-   ))
-) Nil);
-fragment  push := λ(: src LocalVariable+Sized<size>). (: (
-   (.program (
-      (for word-offset in (range( 0 (/( (.expression size) 8 )) )) (
-         \t 'pushq \s (+(
-            (.expression src)
-            (+(
-               (+( (.expression size) '-8 ))
-               (inv(*( (.expression word-offset) 8 )))
-            ))
-         )) \[ '%rbp \] \n
-     ))
-      (if-eq (.expression size) 4 (
-         \t 'pushq \s (.expression src) \[ '%rbp \] \n
-      ))
-      (if-eq (.expression size) 2 (
-         \t 'pushq \s (.expression src) \[ '%rbp \] \n
-      ))
-      (if-eq (.expression size) 1 (
-         \t 'pushq \s (.expression src) \[ '%rbp \] \n
-      ))
-   ))
+push := λ: Blob(: src Sized<0>). (: (
+   (:frame (:frame src))
+   (:unframe (:unframe src))
+   (:program (:program src))
 ) Nil);
 
-dev-push := λ: Blob(: src Sized<0>). (: () Nil);
-
-dev-push := λ: Blob(: src GlobalVariable+Sized<size>). (: (
+push := λ: Blob(: src GlobalVariable+Sized<size>). (: (
    (:program (
       '\tmov\s$_l (:expression src) ',\s%r15\n_l
       (for-atom (word-offset in (range( 0_l (/( (: size L) 8_l )) ))) (
@@ -213,7 +172,7 @@ dev-push := λ: Blob(: src GlobalVariable+Sized<size>). (: (
       ) ())
    ))
 ) Nil);
-dev-push := λ: Blob(: src LocalVariable+Sized<size>). (: (
+push := λ: Blob(: src LocalVariable+Sized<size>). (: (
    (:program (
       (for-atom (word-offset in (range( 0_l (/( (: size L) 8_l )) ))) (
          '\tpushq\s_l (+(
@@ -421,20 +380,15 @@ mov := λ: Blob(: src Constant+Literal+Sized<8>)(: dst GlobalVariable+Sized<8>).
    ))
 ) Nil);
 
-fragment  push := λ(: src Constant+Literal+Sized<1>). (: (.program( \t 'pushq \s '$ (.expression src) \n )) Nil);
-fragment  push := λ(: src Constant+Literal+Sized<2>). (: (.program( \t 'pushq \s '$ (.expression src) \n )) Nil);
-fragment  push := λ(: src Constant+Literal+Sized<4>). (: (.program( \t 'pushq \s '$ (.expression src) \n )) Nil);
-fragment  push := λ(: src Constant+Literal+Sized<8>). (: (.program( \t 'pushq \s '$ (.expression src) \n )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<1>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<2>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<4>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<8>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
 
-dev-push := λ: Blob(: src Constant+Literal+Sized<1>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
-dev-push := λ: Blob(: src Constant+Literal+Sized<2>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
-dev-push := λ: Blob(: src Constant+Literal+Sized<4>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
-dev-push := λ: Blob(: src Constant+Literal+Sized<8>). (: (:program( '\tpushq\s$_l (:expression src) '\n_l )) Nil);
-
-dev-push := λ: Blob(: src Constant+Literal+Sized<1>+Reg8). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
-dev-push := λ: Blob(: src Constant+Literal+Sized<2>+Reg16). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
-dev-push := λ: Blob(: src Constant+Literal+Sized<4>+Reg32). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
-dev-push := λ: Blob(: src Constant+Literal+Sized<8>+Reg64). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<1>+Reg8). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<2>+Reg16). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<4>+Reg32). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
+push := λ: Blob(: src Constant+Literal+Sized<8>+Reg64). (: (:program( '\tpushq\s%_l (:expression src) '\n_l )) Nil);
 
 mov := λ: Blob(: src Reg8)(: dst LocalVariable+Sized<1>). (: (
    (:frame (:frame src))
@@ -520,45 +474,39 @@ mov := λ: Blob(: src Constant+Literal+Sized<2>)(: dst Constant+Reg16). (: (:pro
 mov := λ: Blob(: src Constant+Literal+Sized<4>)(: dst Constant+Reg32). (: (:program( '\tmov\s$_l (:expression src) ',\s%_l (:expression dst) '\n_l )) Nil);
 mov := λ: Blob(: src Constant+Literal+Sized<8>)(: dst Constant+Reg64). (: (:program( '\tmov\s$_l (:expression src) ',\s%_l (:expression dst) '\n_l )) Nil);
 
-fragment  push := λ(: dst Reg8). (: (.program( \t 'mov \s '% (.expression dst) , '%r15b \n \t 'push \s '%r15 \n )) Nil);
-fragment  push := λ(: dst Reg16). (: (.program( \t 'mov \s '% (.expression dst) , '%r15w \n \t 'push \s '%r15 \n )) Nil);
-fragment  push := λ(: dst Reg32). (: (.program( \t 'mov \s '% (.expression dst) , '%r15d \n \t 'push \s '%r15 \n )) Nil);
-fragment  push := λ(: dst Reg64). (: (.program( \t 'push \s '% (.expression dst) \n )) Nil);
-
-dev-push := λ: Blob(: src Reg8). (: (
+push := λ: Blob(: src Reg8). (: (
    (:frame (:frame src))
    (:unframe (:unframe src))
    (:program(
       (:program src)
-      '\tmov\s%_l (:expression src) ',%r15b\n_l
-      '\tpushq\s%r15\n_l
+      '\tmov\s%_l (:expression src) ',\s%AL\n_s
+      '\tpush\s%RAX\n_s
    ))
 ) Nil);
-dev-push := λ: Blob(: src Reg16). (: (
+push := λ: Blob(: src Reg16). (: (
    (:frame (:frame src))
    (:unframe (:unframe src))
    (:program(
       (:program src)
-      '\tmov\s%_l (:expression src) ',%r15w\n_l
-      '\tpushq\s%r15\n_l
+      '\tmov\s%_l (:expression src) ',\s%AX\n_l
+      '\tpush\s%RAX\n_l
    ))
 ) Nil);
-dev-push := λ: Blob(: src Reg32). (: (
+push := λ: Blob(: src Reg32). (: (
    (:frame (:frame src))
    (:unframe (:unframe src))
    (:program(
       (:program src)
-      '\tmov\s%_l (:expression src) ',%r15d\n_l
-      '\tpushq\s%r15\n_l
+      '\tmov\s%_l (:expression src) ',\s%EAX\n_l
+      '\tpush\s%RAX\n_l
    ))
 ) Nil);
-dev-push := λ: Blob(: src Reg64). (: (
+push := λ: Blob(: src Reg64). (: (
    (:frame (:frame src))
    (:unframe (:unframe src))
    (:program(
       (:program src)
-      '\tmov\s%_l (:expression src) ',%r15\n_l
-      '\tpushq\s%r15\n_l
+      '\tpush\s%_l (:expression src) '\n_l
    ))
 ) Nil);
 

LIB/default-templates.lm

@@ -1,7 +1,7 @@
 
 import LIB/default-templates-stackvariable.lm;
 
-dev-push := λ: Blob(: src Constructor<tag>+CaseNumber<case-number>+Sized<struct-size>+FieldsSized<fields-size>). (: (
+push := λ: Blob(: src Constructor<tag>+CaseNumber<case-number>+Sized<struct-size>+FieldsSized<fields-size>). (: (
    (:program(
       (for-atom (wsz in (range( 0_l (/( (-( (-( (: struct-size L) (: fields-size L) )) 8_l )) 8_l )) ))) (
          '\tpushq\s$0\n_l
@@ -38,16 +38,6 @@ mov := λ: Blob(: src Constructor<tag>+CaseNumber<case-number>+Sized<struct-size
    ))
 ) Nil);
 
-fragment  template::push := λ: DontChain(: src Constructor<tag>+Sized<struct-size>+FieldsSized<fields-size>). (: (
-   (.program(
-      (for wsz in (range( '0 (/( (-( (-( (.expression struct-size) (.expression fields-size) )) '8 )) '8 )) )) (
-         \t 'pushq \s '$0 \n
-      ))
-      (.program src)
-      \t 'pushq \s '$ 'case-number \n
-   ))
-) StackVariable);
-
 .0 := λ: Blob(: src Constant). (: (
    (:program(
       '\tmov\s$_s (:expression src) ',\s%RAX\n_s

Makefile

@@ -1,6 +1,7 @@
 
 dev: install-production
-	lm -o dev.s tests/regress/paradata.lm
+	./bootstrap -o safe.s tests/regress/list.lm
+	lm -o dev.s tests/regress/list.lm
 	as dev.s -o dev.o
 	ld dev.o -o dev
 	./dev

SRC/compile-blob.lm

@@ -19,7 +19,6 @@ compile-blob := λ. (: (
          (set preview-program rst)
       ))
       ( (Seq( rst (Typedef( lhs rhs )) )) (
-         (set global-ctx (compile-type( global-ctx lhs rhs )))
          (set preview-program rst)
       ))
       ( (Seq( rst (Glb( k_t rhs )) )) (

SRC/compile-constructor.lm

@@ -15,7 +15,7 @@ compile-constructor := λ(: ctx FContext)(: tag-name String)(: return-type Type)
 
    (let callee-ctx ctx)
    (set callee-ctx (fragment-context::bind( callee-ctx 'src_s constructor-parms e )))
-   (let r (cc-blob( callee-ctx 'dev-push_s constructor-parms offset args )))
+   (let r (cc-blob( callee-ctx 'push_s constructor-parms offset args )))
 
    (set r (fragment::set-context( r ctx )))
    (set r (fragment::set-type( r (denormalize return-type) )))

SRC/compile-expr-direct.lm

@@ -154,11 +154,8 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
             (set e (fragment::set-type( e (typeof term) )))
          ))
       ))
-      ( (App( (Abs( (Var( lhs _ )) ASTNil tlt )) rhs )) (
-         (let rtype (typeof rhs))
-         (set rtype (without-representation rtype))
-         (set rtype (and( rtype (t1 'LocalVariable_s) )))
-         (set rtype (with-size( rtype )))
+      ( (App( (Abs( (@( lhs-t (Var( lhs _ )) )) ASTNil tlt )) rhs )) (
+         (let rtype (typeof lhs-t))
          (let size (sizeof-aligned rtype))
          (set e (compile-push-rvalue( ctx rhs stack-offset )))
          (let bind-offset (-( stack-offset (as size I64) )))

SRC/compile-gnu.lm

@@ -1,31 +1,6 @@
 
 compile-gnu := λ. (: (
    (let preview-program ast-parsed-program)
-   (while (non-zero preview-program) (match preview-program (
-      ()
-      ( (Seq( rst (Frg( k_t rhs )) )) (
-         (let is-template False_u8)
-         (match k (
-            ()
-            ( 'template::push_s (set is-template True_u8) )
-            ( _ () )
-         ))
-         (if (==( is-template True_u8 )) (
-            (let fragment (fragment::new()))
-            (set fragment (fragment::set( fragment 'fragment-type_s (SAtom 'Fragment_s) )))
-            (set fragment (fragment::set( fragment 'fragment_s (to-s rhs) )))
-            (set fragment (fragment::set-type( fragment (typeof rhs) )))
-            (set global-ctx (fragment-context::bind(
-               global-ctx k (typeof rhs) fragment
-            )))
-         ) ())
-         (set preview-program rst)
-      ))
-      ( (Seq( rst _ )) (
-         (set preview-program rst)
-      ))
-   )))
-   (set preview-program ast-parsed-program)
    (while (non-zero preview-program) (match preview-program (
       ()
       ( (Seq( rst (Glb( k_t rhs )) )) (
@@ -52,11 +27,11 @@ compile-gnu := λ. (: (
                   ( _ (
                      (let clean-tt (without-representation kt))
                      (let repr-tt (and( clean-tt (t1 'GlobalVariable_s) )))
-                     (set fragment (fragment::set-type( fragment repr-tt )))
+                     (set fragment (fragment::set-type( fragment (without-constructor repr-tt) )))
                      (let mid (mangle-identifier( k clean-tt )))
                      (set fragment (fragment::set( fragment 'expression_s (SAtom mid) )))
                      (set global-ctx (fragment-context::bind(
-                        global-ctx k repr-tt fragment
+                        global-ctx k (without-constructor repr-tt) fragment
                      )))
                   ))
                ))
@@ -75,7 +50,6 @@ compile-gnu := λ. (: (
          (set preview-program rst)
       ))
       ( (Seq( rst (Typedef( lhs rhs )) )) (
-         (set global-ctx (compile-type( global-ctx lhs rhs )))
          (set preview-program rst)
       ))
       ( (Seq( rst _ )) (

SRC/compile-maybe-push-stack.lm

@@ -6,26 +6,13 @@ compile-maybe-push-stack := λ(: ctx FContext)(: offset I64)(: fragment Fragment
       ()
       ( (TGround( 'StackVariable_s _ )) () )
       ( _ (
-         (set fragment (fragment::set-type( fragment (denormalize ft) )))
-         (set fragment (fragment-apply(
-            ctx offset 'push_s
-            (FLSeq( (close FLEOF) fragment ))
-            (t3( 'Arrow_s ft
-               (and( (t1 'StackVariable_s) (t2( 'Sized_s (t1(to-string(sizeof-aligned ft))) )) ))
-            ))
-            sloc
-         )))
+         (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 )) )))
-
-         #(set ft (denormalize ft))
-         #(let callee-ctx ctx)
-         #(set callee-ctx (fragment-context::bind( callee-ctx 'src_s ft fragment )))
-         #(set fragment (cc-blob( callee-ctx 'dev-push_s 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