Merge pull request #848 from andrew-johnson-4/prune-optimize-4

Prune optimize 4

Cargo.toml

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

Makefile

@@ -10,6 +10,10 @@ profile: install-production
 	as profile.s -o profile.o
 	ld profile.o -o profile
 	./profile SRC/index-index.lm | sort -n
+	lm --profile-invocations SRC/index-index.lm -o profile.s
+	as profile.s -o profile.o
+	ld profile.o -o profile
+	./profile --typecheck SRC/index-index.lm | sort -n
 
 build-docs:
 	lm --blob -o docs/index.html docs/index.html.lm

SRC/alias.lm

@@ -14,8 +14,10 @@ find-alias := λ(: from String)(: pars Type). (: (
               (Tuple( alt-from alt-to ))
               (TGround( 'Arrow_s (LCons( _ (LCons( alt-domain LEOF )) )) ))
            )) (
-            (if (&&( (==( from alt-from )) (can-unify( alt-domain pars )) )) (
-               (set to alt-to)
+            (if (==( from alt-from )) (
+               (if (can-unify( alt-domain pars )) (
+                  (set to alt-to)
+               ) ())
             ) ())
          ))
       ))

SRC/apply-or-cons-and-specialize.lm

@@ -1,12 +1,15 @@
 
 apply-or-cons-and-specialize := λ(: function-name String)(: ft Type)(: pt Type)(: blame AST). (: (
-   (let r TAny)
+   (let r (Tuple( TAny TAny )))
    (if (is-arrow ft) (
       (set r (apply( function-name ft pt 1_u64 blame )))
    ) (
       (if (&&( (non-zero ft) (non-zero pt) )) (
-         (set r (t3( 'Cons_s ft pt )))
+         (set r (Tuple(
+             ft
+             (t3( 'Cons_s ft pt ))
+         )))
       ) ())
    ))
    r
-) Type);
+) Tuple<Type,Type>);

SRC/apply.lm

@@ -1,11 +1,10 @@
 apply := λ(: function-name String)(: ft Type)(: pt Type)(: blame AST). (: (
-   (let tt (apply( function-name ft pt 0_u64 blame )))
-   tt
-) Type);
+   (apply( function-name ft pt 0_u64 blame ))
+) Tuple<Type,Type>);
 
 apply := λ(: function-name String)(: ft Type)(: pt Type)(: do-specialize U64)(: blame AST). (: (
    (apply( function-name ft pt do-specialize blame 1_u64 ))
-) Type);
+) Tuple<Type,Type>);
 
 apply := λ(: function-name String)(: ft Type)(: pt Type)(: do-specialize U64)(: blame AST)(: hard U64). (: (
    (let r TAny)
@@ -46,6 +45,7 @@ apply := λ(: function-name String)(: ft Type)(: pt Type)(: do-specialize U64)(:
             (let ctx (unify( fpt pt )))
             (set ctx (normalize ctx))
             (let closed-type (substitute( ctx sft )))
+            (set ft closed-type)
             (set r (guess-representation(substitute( ctx frt ))))
             (if (&&( do-specialize (is-open sft) )) (
                (if (is-open closed-type) (
@@ -64,8 +64,8 @@ apply := λ(: function-name String)(: ft Type)(: pt Type)(: do-specialize U64)(:
          ))
       ))
    ))
-   r
-) Type);
+   (Tuple( ft r ))
+) Tuple<Type,Type>);
 
 apply := λ(: ctx Context)(: term AST). (: (
    (let return term)

SRC/can-unify.lm

@@ -32,7 +32,7 @@ can-unify := λ(: fpt Type)(: pt Type). (: (
       ))
       ( (Tuple( lt (TAnd( rt1 rt2 )) )) (
          (if (can-unify( lt rt1 )) (set r 1_u64) ())
-         (if (can-unify( lt rt2 )) (set r 1_u64) ())
+         (if r () (set r (can-unify( lt rt2 ))))
       ))
 
       # Varargs
@@ -90,9 +90,7 @@ can-unify := λ(: fpt Type)(: pt Type). (: (
       ))
       ( (Tuple( (TGround( ltn lps )) (TGround( rtn rps )) )) (
          (if (==( ltn rtn )) (
-            (if (can-unify( lps rps )) (
-               (set r 1_u64)
-            ) ())
+            (set r (can-unify( lps rps )))
          ) ())
       ))
       ( _ () )

SRC/compile-expr-direct.lm

@@ -84,7 +84,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
                (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 (t1 'Nil_s) t stack-offset Used )))
+               (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 )))
@@ -169,7 +169,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
                (let tc (fragment-context::lookup-soft( ctx 'del_s (typeof lhs-var) term )))
                (let t (.type tc))
                (if (non-zero t) (
-                  (let del-call (compile-stack-calls( ctx 'del_s rtype lhs-var stack-offset used )))
+                  (let del-call (compile-stack-calls( ctx 'del_s TAny rtype lhs-var stack-offset used )))
                   (set unframe-del (fragment::get( del-call 'program_s )))
                ) ())
             ))
@@ -196,10 +196,10 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
             (match f (
                ()
                ( (Var( fname _ )) (
-                  (set e (compile-stack-calls( ctx fname (typeof term) a stack-offset used )))
+                  (set e (compile-stack-calls( ctx fname (typeof f) (typeof term) a stack-offset used )))
                ))
                ( (App( (Lit( ':_s _ )) (App( (Var( fname _ )) (AType ft) )) )) (
-                  (set e (compile-stack-calls( ctx fname (typeof term) a stack-offset used )))
+                  (set e (compile-stack-calls( ctx fname (typeof f) (typeof term) a stack-offset used )))
                ))
                ( (Lit( fname _ )) (
                   (set e (compile-constructor( ctx fname (typeof term) (typeof a) a stack-offset )))

SRC/compile-expr.lm

@@ -4,7 +4,7 @@ compile-expr := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used IsUsed
    (match used (
       ()
       ( Return (
-         (set e (compile-stack-call( ctx 'cdecl::return_s (typeof term) term stack-offset used )))
+         (set e (compile-stack-calls( ctx 'cdecl::return_s TAny (typeof term) term stack-offset used )))
       ))
       ( _ (
          (set e (compile-expr-direct( ctx term stack-offset used )))

SRC/compile-global.lm

@@ -89,7 +89,7 @@ compile-global := λ(: ctx FContext)(: k String)(: term AST). (: (
          (ascript-normal( kterm kt ))
          (let init-app (App( (close term) (close kterm) )))
          (ascript-normal( init-app (t3( 'Cons_s kt (and( (without-representation kt) (t1 'GlobalVariable_s) )) )) ))
-         (let init (compile-stack-calls( ctx 'mov_s (t1 'Nil_s) init-app -8_i64 Used )))
+         (let init (compile-stack-calls( ctx 'mov_s TAny (t1 'Nil_s) init-app -8_i64 Used )))
 
          (set assemble-init-section (SCons(
             (close assemble-init-section)

SRC/compile-gnu.lm

@@ -16,24 +16,20 @@ compile-gnu := λ. (: (
                )))
             ) (
                (set fragment (fragment::set( fragment 'fragment-type_s (SAtom 'Global_s) )))
-               (match (slot( kt '->_s )) (
-                  ()
-                  ( (TGround( '->_s _ )) (
-                     (set fragment (fragment::set-type( fragment kt )))
-                     (set global-ctx (fragment-context::bind(
-                        global-ctx k kt fragment
-                     )))
-                  ))
-                  ( _ (
-                     (let clean-tt (without-representation kt))
-                     (let repr-tt (and( clean-tt (t1 'GlobalVariable_s) )))
-                     (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 (without-constructor repr-tt) fragment
-                     )))
-                  ))
+               (if (is-arrow kt) (
+                  (set fragment (fragment::set-type( fragment kt )))
+                  (set global-ctx (fragment-context::bind(
+                     global-ctx k kt fragment
+                  )))
+               ) (
+                  (let clean-tt (without-representation kt))
+                  (let repr-tt (and( clean-tt (t1 'GlobalVariable_s) )))
+                  (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 (without-constructor repr-tt) fragment
+                  )))
                ))
             ))
          ))

SRC/compile-stack-call.lm

@@ -44,7 +44,3 @@ compile-stack-call := λ(: ctx FContext)(: f Fragment)(: function-name String)(:
    r
 ) Fragment);
 
-compile-stack-call := λ(: ctx FContext)(: function-name String)(: return-type Type)(: args AST)(: offset I64)(: used IsUsed). (: (
-   (let f (fragment-context::lookup( ctx function-name (typeof args) args )))
-   (compile-stack-call( ctx f function-name return-type args offset used ))
-) Fragment);

SRC/compile-stack-calls.lm

@@ -1,9 +1,9 @@
 
-compile-stack-calls := λ(: ctx FContext)(: function-name String)(: return-type Type)(: args AST)(: offset I64)(: used IsUsed). (: (
+compile-stack-calls := λ(: ctx FContext)(: function-name String)(: function-type Type)(: return-type Type)(: args AST)(: offset I64)(: used IsUsed). (: (
    (let r (fragment::new()))
    (set r (fragment::set-context( r ctx )))
    (set r (fragment::set-offset( r offset )))
-   (let fs (fragment-context::lookups( ctx function-name (typeof args) args )))
+   (let fs (fragment-context::lookups( ctx function-name function-type (typeof args) args )))
    (for-each (f in fs) (
       (set r (fragment::chain(
          r

SRC/fragment-context::lookup.lm

@@ -12,27 +12,25 @@ fragment-context::lookup := λ(: ctx FContext)(: k String)(: kt Type)(: sloc AST
       ()
       ( (FCtxBind( rst rk rt rf )) (
          (if (==( k rk )) (
-            (match (slot( rt 'Arrow_s )) (
-               ()
-               ( (TGround( 'Arrow_s (LCons( ranget (LCons( domaint LEOF )) )) )) (
-                  (if (can-unify( domaint kt )) (
-                     (if (non-zero found) (
-                        (if (can-unify( found domaint )) (
-                           (set r rf)
-                           (set found domaint)
-                        ) ())
-                     ) (
+            (if (is-arrow rt) (
+               (let domaint (domain rt))
+               (let ranget (range rt))
+               (if (can-unify( domaint kt )) (
+                  (if (non-zero found) (
+                     (if (can-unify( found domaint )) (
                         (set r rf)
                         (set found domaint)
-                     ))
-                  ) ())
-                  (set ctx rst)
-               ))
-               ( _ (
-                  (set r rf)
-                  (set found (t1 'LocalVariable_s))
-                  (set ctx FCtxEOF)
-               ))
+                     ) ())
+                  ) (
+                     (set r rf)
+                     (set found domaint)
+                  ))
+               ) ())
+               (set ctx rst)
+            ) (
+               (set r rf)
+               (set found (t1 'LocalVariable_s))
+               (set ctx FCtxEOF)
             ))
          ) (
             (set ctx rst)

SRC/fragment-context::lookups.lm

@@ -1,19 +1,23 @@
 
-fragment-context::lookups := λ(: ctx FContext)(: k String)(: kt Type)(: sloc AST). (: (
-   (fragment-context::lookups( ctx k kt sloc True_u8 ))
+fragment-context::lookups := λ(: ctx FContext)(: k String)(: ft Type)(: kt Type)(: sloc AST). (: (
+   (fragment-context::lookups( ctx k ft kt sloc True_u8 ))
 ) List<Fragment>);
 
-fragment-context::lookups := λ(: ctx FContext)(: k String)(: kt Type)(: sloc AST)(: hard U8). (: (
+fragment-context::lookups := λ(: ctx FContext)(: k String)(: ft Type)(: kt Type)(: sloc AST)(: hard U8). (: (
    (set k (find-alias( k kt )))
    (let r (: LEOF List<Fragment>))
    (let found TAny)
    (while (non-zero ctx) (match ctx (
       ()
       ( (FCtxBind( rst rk rt rf )) (
          (if (==( k rk )) (
-            (match (slot( rt 'Arrow_s )) (
-               ()
-               ( (TGround( 'Arrow_s (LCons( ranget (LCons( domaint LEOF )) )) )) (
+            (if (is( ft rt )) (
+               (set r (cons( rf (: LEOF List<Fragment>) )))
+               (set ctx FCtxEOF)
+            ) (
+               (if (is-arrow rt) (
+                  (let domaint (domain rt))
+                  (let ranget (range rt))
                   (if (can-unify( domaint kt )) (
                      (if (non-zero found) (
                         (if (can-unify( found domaint )) (
@@ -34,8 +38,7 @@ fragment-context::lookups := λ(: ctx FContext)(: k String)(: kt Type)(: sloc AS
                      ))
                   ) ())
                   (set ctx rst)
-               ))
-               ( _ (
+               ) (
                   (if (!=( (is-hook rt) 0_u64 )) (
                      (set r (cons( rf r )))
                   ) (

SRC/infer-expr.lm

@@ -167,16 +167,38 @@ infer-expr := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type)(:
          (let l-used Unused)
          (if (is( used Call )) (set l-used Call) ())
          (let r-used Used)
-         (if (is( used Unused )) (set r-used Unused) ())
-         (set tctx (infer-expr( tctx l Unscoped TAny l-used )))
-         (if (is-arrow(typeof l)) (set r-used Call) ())
-         (set tctx (infer-expr( tctx r Unscoped TAny r-used )))
-         (let rt (apply-or-cons-and-specialize(
-            (var-name-if-var l)
-            (typeof l)
-            (typeof r)
-            term
-         )))
+         (let rt TAny)
+         (match l (
+            ()
+            ( (Var( l-fname _ )) (
+               (if (is( used Unused )) (set r-used Unused) ())
+               (set tctx (infer-expr( tctx l Unscoped TAny l-used )))
+               (if (is-arrow(typeof l)) (set r-used Call) ())
+               (set tctx (infer-expr( tctx r Unscoped TAny r-used )))
+               (let ftrt (apply-or-cons-and-specialize(
+                  (var-name-if-var l)
+                  (typeof l)
+                  (typeof r)
+                  term
+               )))
+               (let function-type (.2 ftrt))
+               (ascript-normal( l function-type ))
+               (set rt (.1 ftrt))
+            ))
+            ( _ (
+               (if (is( used Unused )) (set r-used Unused) ())
+               (set tctx (infer-expr( tctx l Unscoped TAny l-used )))
+               (if (is-arrow(typeof l)) (set r-used Call) ())
+               (set tctx (infer-expr( tctx r Unscoped TAny r-used )))
+               (let ftrt (apply-or-cons-and-specialize(
+                  (var-name-if-var l)
+                  (typeof l)
+                  (typeof r)
+                  term
+               )))
+               (set rt (.1 ftrt))
+            ))
+         ))
          (if (is( l-used Unused )) (
             (set rt (implicit-tail rt))
          ) ())