diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt index 2fc2c65..6e368ec 100644 --- a/aoc2023/Day1.newt +++ b/aoc2023/Day1.newt @@ -43,8 +43,6 @@ part1 text digits = let nums = map combine $ map digits lines in foldl _+_ 0 nums -#check digits1 ∘ unpack : String -> List Int - runFile : String -> IO Unit runFile fn = do text <- readFile fn diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt index b8584d1..efe7491 100644 --- a/src/Lib/Compile.newt +++ b/src/Lib/Compile.newt @@ -6,6 +6,7 @@ module Lib.Compile import Prelude import Lib.Common import Lib.Types +import Lib.Eval import Lib.Prettier import Lib.CompileExp import Lib.TopContext @@ -330,8 +331,10 @@ getEntries acc name = do pure acc Just (MkEntry _ name type def@(Fn exp) _) => case lookupMap' name acc of Just _ => pure acc - Nothing => - let acc = updateMap name def acc in + Nothing => do + top <- getTop + exp <- zonk top 0 Nil exp + let acc = updateMap name (Fn exp) acc foldlM getEntries acc $ getNames exp Nil Just (MkEntry _ name type def@(PrimFn _ _ used) _) => let acc = updateMap name def acc in diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 90f1d80..8a6675b 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -140,9 +140,18 @@ processPrimFn ns fc nm used ty src = do -- I'm trying to get ++ and + inlined as javascript + complexity : Tm → Int complexity (Ref _ _) = 1 +complexity (Meta _ _) = 1 -- what's a good score for this, it's not inlined yet. complexity (Lam _ _ _ _ sc) = 1 + complexity sc -complexity (App _ t u) = complexity t + complexity u +-- Ignore metas - they may be erased and likely are much smaller when substituted +complexity (App _ t u) = go t (complexity u) + where + go : Tm → Int → Int + go (App _ t u) acc = go t (acc + complexity u) + go (Meta _ _) acc = 1 + go t acc = acc + complexity t complexity (Bnd _ _) = 1 +complexity (UU _) = 0 +complexity (Lit _ _) = 0 -- These turn into a projection complexity (Case _ sc (CaseCons _ _ t :: Nil)) = 1 + complexity sc + complexity t complexity _ = 100 @@ -167,21 +176,19 @@ processDef ns fc nm clauses = do tm <- buildTree (mkCtx fc) (MkProb clauses' vty) solveAutos - -- TODO - make nf that expands all metas and drop zonk - -- Idris2 doesn't expand metas for performance - a lot of these are dropped during erasure. - -- Day1.newt is a test case -- This inlines metas and functions flagged Inline. - tm' <- zonk top 0 Nil tm - 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') - -- putStrLn "complexity \{show (QN ns nm)} \{show $ complexity tm'}" - -- putStrLn $ show tm' + -- moved to Compile.newt because it was interfering with type checking (Zoo4eg.newt) via over-reduction + -- tm' <- zonk top 0 Nil tm + + debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm} : \{render 90 $ pprint Nil ty}" + updateDef (QN ns nm) fc ty (Fn tm) + -- putStrLn "complexity \{show (QN ns nm)} \{show $ complexity tm}" + -- putStrLn $ show tm -- TODO we need some protection against inlining a function calling itself. - -- 14 gets us to 6.21s, higher than 11 breaks Zoo4eg.newt with a unification error (probably need to inline at the end instead) - -- But we need better heuristics, maybe fuel and deciding while inlining. + -- We need better heuristics, maybe fuel and deciding while inlining. -- bind is explicit here because the complexity has a 100 in it. - if complexity tm' < 11 || show (QN ns nm) == "Prelude.Prelude.Monad Prelude.IO,bind" + let name = show $ QN ns nm + if complexity tm < 15 || name == "Prelude.Prelude.Monad Prelude.IO,bind" || name == "Prelude._>>=_" then setFlag (QN ns nm) fc Inline else pure MkUnit