From 49c90cce6d47844f83413a98d72044b5b56b0163 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 20 Sep 2025 17:21:19 -0700
Subject: [PATCH] inline "simple" functions and inline after app in inline

---
 src/Lib/Eval.newt        |  4 ++--
 src/Lib/ProcessDecl.newt | 12 +++++++++++-
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt
index b4a03e9..d862796 100644
--- a/src/Lib/Eval.newt
+++ b/src/Lib/Eval.newt
@@ -286,7 +286,6 @@ tweakFC fc (LetRec fc1 nm ty t u) = LetRec fc nm ty t u
 tweakFC fc (Lit fc1 lit) = Lit fc lit
 tweakFC fc (Erased fc1) = Erased fc
 
--- TODO replace this with a variant on nf
 zonkApp : TopContext -> Int -> Env -> Tm -> List Tm -> M Tm
 zonkApp top l env (App fc t u) sp = do
   u' <- zonk top l env u
@@ -309,7 +308,8 @@ zonkApp top l env t sp = do
   vtm <- eval env tm
   catchError (do
     foo <- vappSpine vtm (Lin <>< sp')
-    quote l foo)
+    t' <- quote l foo
+    zonk top l env t')
     (\_ => pure $ appSpine t' sp)
   where
     inlineDef : Tm → Maybe Tm
diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt
index c6447be..9664078 100644
--- a/src/Lib/ProcessDecl.newt
+++ b/src/Lib/ProcessDecl.newt
@@ -137,6 +137,13 @@ processPrimFn ns fc nm used ty src = do
   let arity = piArity ty'
   setDef (QN ns nm) fc ty' (PrimFn src arity used') Nil
 
+-- I'm trying to get ++ and + inlined as javascript +
+complexity : Tm → Int
+complexity (Ref _ _) = 1
+complexity (Lam _ _ _ _ sc) = 1 + complexity sc
+complexity (App _ t u) = complexity t + complexity u
+complexity (Bnd _ _) = 1
+complexity _ = 100
 
 processDef : List String → FC → String → List (Raw × Raw) → M Unit
 processDef ns fc nm clauses = do
@@ -166,6 +173,9 @@ processDef ns fc nm clauses = do
   debug $ \ _ => "NF\n\{render 80 $ pprint Nil tm'}"
   debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm'} : \{render 90 $ pprint Nil ty}"
   updateDef (QN ns nm) fc ty (Fn tm')
+  if complexity tm' < 10
+    then setFlag (QN ns nm) fc Inline
+    else pure MkUnit
 
 processCheck : List String → FC → Raw → Raw → M Unit
 processCheck ns fc tm ty = do
@@ -213,8 +223,8 @@ processClass ns classFC nm tele decls = do
       log 1 $ \ _ => "\{name} : \{render 90 $ pretty funType}"
       log 1 $ \ _ => "\{render 90 $ pretty decl}"
       processDecl ns $ TypeSig fc (name :: Nil) funType
-      processDecl ns decl
       setFlag (QN ns name) fc Inline
+      processDecl ns decl
   where
     makeLHS : Raw → Telescope → Raw
     makeLHS acc ((BI fc' nm icit quant,  _) :: tele) = RApp fc' (makeLHS acc tele) (RVar fc' nm) Implicit