Newt - a dependent typed programming language

Looping TCO for singleton components

+93 -15
+55 -9
src/Lib/Compile.newt
··· 53 53 JReturn : JSExp -> JSStmt Return 54 54 JLet : (nm : String) -> JSStmt (Assign nm) -> JSStmt Plain -- need somebody to assign 55 55 JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm) 56 - -- TODO - switch to Int tags 57 56 JCase : ∀ a. JSExp -> List JAlt -> JSStmt a 58 57 JIfThen : ∀ a. JSExp -> JSStmt a -> JSStmt a -> JSStmt a 59 58 -- throw can't be used 60 59 JError : ∀ a. String -> JSStmt a 60 + -- FIXME We're routing around the index here 61 + -- Might be able to keep the index if 62 + -- we add `Loop : List String -> StKind` 63 + -- JLoopAssign peels one off 64 + -- JContinue is a Loop Nil 65 + -- And LoopReturn 66 + JWhile : ∀ a. JSStmt a → JSStmt a 67 + JLoopAssign : (nm : String) → JSExp → JSStmt Plain 68 + JContinue : ∀ a. JSStmt a 61 69 62 70 Cont : StKind → U 63 71 Cont e = JSExp -> JSStmt e ··· 109 117 env' = push env (Var nm') 110 118 in (nm', env') 111 119 120 + -- get list of arg names and an environment with either references or undefined 121 + -- depending on quantity 112 122 freshNames : List (Quant × String) -> JSEnv -> (List String × JSEnv) 113 123 freshNames nms env = go nms env Lin 114 124 where ··· 132 142 simpleJSExp (LitBool _) = True 133 143 simpleJSExp _ = False 134 144 145 + getEnv : Int → List JSExp → JSExp 146 + getEnv ix env = case getAt' ix env of 147 + Just e => e 148 + Nothing => fatalError "Bad bounds \{show ix}" 149 + 135 150 -- This is inspired by A-normalization, look into the continuation monad 136 151 -- There is an index on JSStmt, adopted from Stefan Hoeck's code. 137 152 -- ··· 139 154 -- is a continuation, which turns the final JSExpr into a JSStmt, and the function returns 140 155 -- a JSStmt, wrapping recursive calls in JSnoc if necessary. 141 156 termToJS : ∀ e. JSEnv -> CExp -> Cont e -> JSStmt e 142 - termToJS env (CBnd k) f = case getAt (cast k) env.jsenv of 143 - (Just e) => f e 144 - Nothing => fatalError "Bad bounds" 157 + termToJS env (CBnd k) f = f $ getEnv k env.jsenv 145 158 termToJS env CErased f = f JUndefined 146 159 termToJS env (CRaw str _) f = f (Raw str) 147 160 termToJS env (CLam nm t) f = ··· 155 168 termToJS env (CMeta k) f = f $ LitString "META \{show k}" 156 169 termToJS env (CLit lit) f = f (litToJS lit) 157 170 -- if it's a var, just use the original 158 - termToJS env (CLet nm (CBnd k) u) f = case getAt (cast k) env.jsenv of 159 - Just e => termToJS (push env e) u f 160 - Nothing => fatalError "bad bounds" 171 + termToJS env (CLet nm (CBnd k) u) f = termToJS (push env $ getEnv k env.jsenv) u f 161 172 -- For a let, we run with a continuation to JAssign to a pre-declared variable 162 173 -- if JAssign comes back out, we either push the JSExpr into the environment or JConst it, 163 174 -- depending on complexity. Otherwise, stick the declaration in front. ··· 169 180 then termToJS (push env exp) u f 170 181 else JSnoc (JConst nm' exp) (termToJS env' u f) 171 182 t' => JSnoc (JLet nm' t') (termToJS env' u f) 183 + termToJS env (CLetLoop args body) f = 184 + let off = length' args in 185 + -- Add lets for the args, we put this in a while and 186 + -- mutate the args, then continue for the self-call 187 + let (lets, env') = go (length' args - 1) args env Lin in 188 + JWhile $ foldr (\a b => JSnoc a b) (termToJS env' body f) lets 189 + where 190 + go : Int → List (Quant × String) -> JSEnv -> SnocList (JSStmt Plain) -> (List (JSStmt Plain) × JSEnv) 191 + go off Nil env acc = (acc <>> Nil, env) 192 + go off ((Many, n) :: ns) env acc = 193 + let (n', env') = freshName' n env 194 + in go off ns env' (acc :< JConst n' (getEnv off env.jsenv)) 195 + go off ((Zero, n) :: ns) env acc = 196 + let env' = push env JUndefined 197 + in go off ns env' acc 198 + 172 199 termToJS env (CLetRec nm CErased u) f = termToJS (push env JUndefined) u f 173 200 termToJS env (CLetRec nm t u) f = 174 201 -- this shouldn't happen if where is lifted ··· 184 211 go (t :: ts) (Many :: qs) ix k = termToJS env t $ \ t' => go ts qs (ix + 1) $ \ args => k $ ("h\{show ix}", t') :: args 185 212 go (t :: ts) (q :: qs) ix k = go ts qs (ix + 1) $ \ args => k args 186 213 go _ _ ix k = k Nil 214 + termToJS {e} env (CLoop args quants) f = runArgs (reverse env.jsenv) args quants 215 + where 216 + -- Here we drop the continuation. It _should_ be a JReturn wrapper, because of how we insert JLoop. 217 + -- But we're not statically checking that. 218 + runArgs : List JSExp → List CExp → List Quant → JSStmt e 219 + runArgs _ Nil Nil = JContinue 220 + runArgs _ Nil _ = fatalError "too few CExp" 221 + runArgs (Var x :: rest) (arg :: args) (Many :: qs) = 222 + termToJS env arg $ \ arg' => JSnoc (JLoopAssign x arg') $ runArgs rest args qs 223 + -- TODO check arg erased 224 + runArgs (JUndefined :: rest) (arg :: args) (q :: qs) = runArgs rest args qs 225 + runArgs (wat :: rest) (arg :: args) (q :: qs) = fatalError "bad env for quant \{show q}" 226 + runArgs a b c = fatalError "FALLBACK \{show $ length' a} \{show $ length' b} \{show $ length' c}" 187 227 termToJS env (CAppRef nm args quants) f = termToJS env (CRef nm) (\ t' => (argsToJS env t' args quants Lin f)) 188 228 where 189 229 etaExpand : JSEnv -> List Quant -> SnocList JSExp -> JSExp -> JSExp ··· 329 369 -- I might not need these split yet. 330 370 stmtToDoc (JLet nm body) = text "let" <+> jsIdent nm ++ text ";" </> stmtToDoc body 331 371 stmtToDoc (JAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text ";" 332 - stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";") 372 + stmtToDoc (JLoopAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text ";" 373 + stmtToDoc (JContinue) = text "continue" ++ text ";" 374 + stmtToDoc (JWhile stmt) = text "while (1)" <+> bracket "{" (stmtToDoc stmt) "}" 375 + -- In the loop case, this may be reassigned 376 + stmtToDoc (JConst nm x) = text "let" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";") 333 377 stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ text ";" 334 378 stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ text ");" 335 379 stmtToDoc (JIfThen sc t e) = ··· 431 475 getNames : (deep : Bool) → List (Bool × QName) → CExp → List (Bool × QName) 432 476 -- liftIO calls a lambda statically 433 477 getNames deep acc (CLam _ t) = getNames deep acc t 478 + getNames deep acc (CLetLoop _ t) = getNames deep acc t 434 479 -- top level 0-ary function, doesn't happen 435 480 getNames deep acc (CFun _ t) = if deep then getNames deep acc t else acc 436 - 481 + -- REVIEW - True or deep? 482 + getNames deep acc (CLoop args qs) = foldl (getNames True) acc args 437 483 getNames deep acc (CAppRef nm args qs) = 438 484 if length' args == length' qs 439 485 then case args of
+5
src/Lib/CompileExp.newt
··· 36 36 CLit : Literal -> CExp 37 37 CLet : Name -> CExp -> CExp -> CExp 38 38 CLetRec : Name -> CExp -> CExp -> CExp 39 + -- Might be able to use a bunch of flagged lets or something 40 + CLetLoop : List (Quant × Name) → CExp → CExp 41 + -- This is like a CAppRef, self-call 42 + -- If we know it's a tail call fn, we could handle all of this in codegen... 43 + CLoop : List CExp → List Quant → CExp 39 44 CErased : CExp 40 45 -- Data / type constructor 41 46 CConstr : Nat → Name → List CExp → List Quant → CExp
+30 -1
src/Lib/TCO.newt
··· 20 20 -- Find names of applications in tail position 21 21 tailNames : CExp → List QName 22 22 tailNames (CAppRef nm args n) = nm :: Nil 23 + -- these two shouldn't exist yet 24 + tailNames (CLoop _ _) = Nil 25 + tailNames (CLetLoop _ _) = Nil 23 26 tailNames (CCase _ alts) = join $ map altTailNames alts 24 27 where 25 28 altTailNames : CAlt → List QName ··· 40 43 tailNames (CRaw _ _) = Nil 41 44 tailNames (CPrimOp _ _ _) = Nil 42 45 43 - -- rewrite tail calls to return an object 46 + -- rewrite tail calls to return an object to a trampoline 47 + -- takes a list of the names in the group and the function body 44 48 rewriteTailCalls : List QName → CExp → CExp 45 49 rewriteTailCalls nms tm = case tm of 46 50 CAppRef nm args qs => ··· 63 67 rewriteAlt (CDefAlt t) = CDefAlt $ rewriteTailCalls nms t 64 68 rewriteAlt (CLitAlt lit t) = CLitAlt lit $ rewriteTailCalls nms t 65 69 70 + -- A looping version of TCO, specialized for single function calls 71 + -- takes a list of the name of the function and the function body 72 + rewriteLoop : QName → CExp → CExp 73 + rewriteLoop qn tm = case tm of 74 + (CAppRef nm args qs) => 75 + if length' args == length' qs && nm == qn 76 + then CLoop args qs 77 + else tm 78 + (CLetRec nm t u) => CLetRec nm t $ rewriteLoop qn u 79 + (CLet nm t u) => CLet nm t $ rewriteLoop qn u 80 + (CCase sc alts) => CCase sc $ map rewriteAlt alts 81 + tm => tm 82 + where 83 + rewriteAlt : CAlt → CAlt 84 + rewriteAlt (CConAlt ix nm info args t) = CConAlt ix nm info args $ rewriteLoop qn t 85 + rewriteAlt (CDefAlt t) = CDefAlt $ rewriteLoop qn t 86 + rewriteAlt (CLitAlt lit t) = CLitAlt lit $ rewriteLoop qn t 87 + 66 88 -- the name of our trampoline 67 89 bouncer : QName 68 90 bouncer = QN "" "bouncer" 69 91 70 92 doOptimize : List (QName × CExp) → M (List (QName × CExp)) 93 + doOptimize ((qn, exp) :: Nil) = do 94 + let (CFun args body) = exp | _ => error emptyFC "doOptimize \{show qn} not a CFun" 95 + let body = rewriteLoop qn body 96 + pure $ (qn, CFun args (CLetLoop args body)) :: Nil 97 + 71 98 doOptimize fns = do 72 99 splitFuns <- traverse splitFun fns 73 100 let nms = map fst fns ··· 112 139 113 140 processGroup : ExpMap → List QName → M ExpMap 114 141 processGroup expMap names = do 142 + -- Looks like only two are > 1 143 + debug $ \ _ => "compile.tco: group \{show $ length' names} \{show names}" 115 144 let pairs = mapMaybe (flip lookupMap expMap) names 116 145 updates <- doOptimize pairs 117 146 pure $ foldl doUpdate expMap updates
+3 -5
vim/syntax/newt.vim
··· 1 1 syn keyword newtInfix infix infixl infixr 2 - syn keyword newtKW data where let in case of 3 - syn keyword newtLet let in 2 + syn keyword newtKW data where let in case of derive module import 4 3 syn match newtIdentifier "[a-zA-Z][a-zA-Z]*" contained 5 - syn keyword newtStructure data import module where 6 4 syn region newtBlockComment start="/-" end="-/" contained 7 5 syn match newtLineComment "--.*$" contains=@Spell 8 6 ··· 11 9 highlight def link newtInfix PreProc 12 10 highlight def link newtBlockComment Comment 13 11 highlight def link newtLineComment Comment 14 - highlight def link newtLet Structure 15 - highlight def link newtStructure Structure 12 + highlight def link newtStructure Keyword 13 + highlight def link newtKW Keyword 16 14 17 15 let b:current_syntax = "newt"