From 66f3787cb716f427f3c548767f63670683d362dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stefan=20H=C3=B6ck?= Date: Tue, 18 May 2021 13:37:51 +0200 Subject: [PATCH] [ cleanup ] Annotate JS backend sources (#1425) --- libs/base/Data/List.idr | 39 +++ src/Compiler/ES/ES.idr | 1 + src/Compiler/ES/Imperative.idr | 413 ++++++++++++++++++++---------- src/Compiler/ES/ImperativeAst.idr | 324 +++++++++++++++++------ src/Compiler/ES/Javascript.idr | 25 +- src/Compiler/ES/Node.idr | 30 ++- src/Compiler/ES/RemoveUnused.idr | 48 +++- src/Compiler/ES/TailRec.idr | 373 ++++++++++++++++++--------- src/Libraries/Data/List/Extra.idr | 29 +++ src/Libraries/Data/SortedSet.idr | 4 + 10 files changed, 907 insertions(+), 379 deletions(-) diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index fd71927a4..15687f80b 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -621,6 +621,45 @@ transpose (heads :: tails) = spreadHeads heads (transpose tails) where spreadHeads (head :: heads) [] = [head] :: spreadHeads heads [] spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails +------------------------------------------------------------------------ +-- Grouping + +||| `groupBy` operates like `group`, but uses the provided equality +||| predicate instead of `==`. +public export +groupBy : (a -> a -> Bool) -> List a -> List (List1 a) +groupBy _ [] = [] +groupBy eq (h :: t) = let (ys,zs) = go h t + in ys :: zs + + where go : a -> List a -> (List1 a, List (List1 a)) + go v [] = (singleton v,[]) + go v (x :: xs) = let (ys,zs) = go x xs + in if eq v x + then (cons v ys, zs) + else (singleton v, ys :: zs) + +||| The `group` function takes a list of values and returns a list of +||| lists such that flattening the resulting list is equal to the +||| argument. Moreover, each list in the resulting list +||| contains only equal elements. +public export +group : Eq a => List a -> List (List1 a) +group = groupBy (==) + +||| `groupWith` operates like `group`, but uses the provided projection when +||| comparing for equality +public export +groupWith : Eq b => (a -> b) -> List a -> List (List1 a) +groupWith f = groupBy (\x,y => f x == f y) + +||| `groupAllWith` operates like `groupWith`, but sorts the list +||| first so that each equivalence class has, at most, one list in the +||| output +public export +groupAllWith : Ord b => (a -> b) -> List a -> List (List1 a) +groupAllWith f = groupWith f . sortBy (comparing f) + -------------------------------------------------------------------------------- -- Properties -------------------------------------------------------------------------------- diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index c8c775e08..8522453f4 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -94,6 +94,7 @@ jsIdent : String -> String jsIdent s = concatMap okchar (unpack s) where okchar : Char -> String + okchar '_' = "_" okchar c = if isAlphaNum c then cast c else "$" ++ the (String) (asHex (cast {to=Int} c)) diff --git a/src/Compiler/ES/Imperative.idr b/src/Compiler/ES/Imperative.idr index f94e91088..e502686a6 100644 --- a/src/Compiler/ES/Imperative.idr +++ b/src/Compiler/ES/Imperative.idr @@ -1,3 +1,8 @@ +||| This module is responsible for compiling an +||| Idris2 `ClosedTerm` to a pair of `ImperativeStatement`s, +||| one of which corresponds to a sequence of toplevel +||| definitions, the other being the program's main entry +||| point. module Compiler.ES.Imperative import public Compiler.ES.ImperativeAst @@ -54,134 +59,247 @@ record ImpSt where genName : {auto c : Ref Imps ImpSt} -> Core Name genName = - do - s <- get Imps - let i = nextName s - put Imps (record { nextName = i + 1 } s) - pure $ MN "imp_gen" i + do s <- get Imps + let i = nextName s + put Imps (record { nextName = i + 1 } s) + pure $ MN "imp_gen" i + +-- Processing an Idris2 expression results in +-- an `ImperativeStatement` (since this is a monoid, +-- this might actually be many statements) of utility +-- functions and intermediary vars and results, and +-- a final imperative expression, calculating a result +-- from the related statement(s). These +-- are then converted to JS code. +-- +-- The boolean flag indicates, whether the two parts +-- should be returned as a pair for further +-- processing, or should be converted +-- to a single statement (in which case, the final +-- expression is converted to a `return` statement). +ImperativeResult : (toReturn : Bool) -> Type +ImperativeResult True = ImperativeStatement +ImperativeResult False = (ImperativeStatement, ImperativeExp) + +-- when invoking `impExp`, in some cases we always +-- generate a pair (statements plus related final +-- expression). In such a case, this function converts +-- the statement to the correct result type as indicated +-- by `toReturn`. +pairToReturn : (toReturn : Bool) + -> (ImperativeStatement, ImperativeExp) + -> (ImperativeResult toReturn) +pairToReturn False (s, e) = (s, e) +pairToReturn True (s, e) = s <+> ReturnStatement e + +-- when invoking `impExp`, in some cases we +-- generate just an expression. +-- In such a case, this function converts +-- the expression to the correct result type as indicated +-- by `toReturn`. +expToReturn : (toReturn : Bool) + -> ImperativeExp + -> (ImperativeResult toReturn) +expToReturn False e = (DoNothing, e) +expToReturn True e = ReturnStatement e + +impTag : Name -> Maybe Int -> Either Int String +impTag n Nothing = Right $ show n +impTag n (Just i) = Left i mutual - - pairToReturn : (toReturn : Bool) -> (ImperativeStatement, ImperativeExp) -> - Core (ifThenElse toReturn ImperativeStatement (ImperativeStatement, ImperativeExp)) - pairToReturn False (s, e) = pure (s, e) - pairToReturn True (s, e) = pure $ s <+> ReturnStatement e - - expToReturn : (toReturn : Bool) -> ImperativeExp -> - Core (ifThenElse toReturn ImperativeStatement (ImperativeStatement, ImperativeExp)) - expToReturn False e = pure $ (DoNothing, e) - expToReturn True e = pure $ ReturnStatement e - - impVectExp : {auto c : Ref Imps ImpSt} -> Vect n NamedCExp -> Core (ImperativeStatement, Vect n ImperativeExp) + -- converts primOps arguments to a set of + -- statements plus a corresponding vect of expressions + impVectExp : {auto c : Ref Imps ImpSt} + -> Vect n NamedCExp + -> Core (ImperativeStatement, Vect n ImperativeExp) impVectExp args = - do - a <- traverseVect (impExp False) args - pure (concat (map fst a), map snd a) + do a <- traverseVect (impExp False) args + pure (concatMap fst a, map snd a) - impListExp : {auto c : Ref Imps ImpSt} -> List NamedCExp -> Core (ImperativeStatement, List ImperativeExp) + -- converts function arguments to a set of + -- statements plus a corresponding list of expressions + impListExp : {auto c : Ref Imps ImpSt} + -> List NamedCExp + -> Core (ImperativeStatement, List ImperativeExp) impListExp args = - do - a <- traverse (impExp False) args - pure (concat (map fst a), map snd a) + do a <- traverse (impExp False) args + pure (concatMap fst a, map snd a) - impExp : {auto c : Ref Imps ImpSt} -> (toReturn : Bool) -> NamedCExp -> - Core (ifThenElse toReturn ImperativeStatement (ImperativeStatement, ImperativeExp)) - impExp toReturn (NmLocal fc n) = expToReturn toReturn $ IEVar n - impExp toReturn (NmRef fc n) = expToReturn toReturn $ IEVar n - impExp toReturn (NmLam fc n e) = expToReturn toReturn $ IELambda [n] !(impExp True e) + impExp : {auto c : Ref Imps ImpSt} + -> (toReturn : Bool) + -> NamedCExp + -> Core (ImperativeResult toReturn) + -- convert local names to vars + impExp toReturn (NmLocal fc n) = + pure . expToReturn toReturn $ IEVar n + + impExp toReturn (NmRef fc n) = + pure . expToReturn toReturn $ IEVar n + + -- TODO: right now, nested lambda expressions are curried + -- (or are they?). + -- It might be more efficient (and more readable!) to uncurry + -- these, at least in the most simple cases. + impExp toReturn (NmLam fc n e) = + pure . expToReturn toReturn $ IELambda [n] !(impExp True e) + + -- Function application: Statements for the + -- implementation of the function and the arguments are + -- generated separately and concatenated. impExp toReturn (NmApp fc x args) = - do - (s1, f) <- impExp False x - (s2, a) <- impListExp args - pairToReturn toReturn (s1 <+> s2, IEApp f a) - impExp toReturn (NmPrimVal fc c) = expToReturn toReturn $ IEConstant c - impExp toReturn (NmOp fc op args) = - do - (s, a) <- impVectExp args - pairToReturn toReturn (s, IEPrimFn op a) - impExp False (NmConCase fc sc alts def) = - do - (s1, exp) <- impExp False sc - res <- genName - swalts <- traverse (impConAltFalse res exp) alts - swdef <- case def of - Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc - Just x => - do - (sd, r) <- impExp False x - pure $ sd <+> MutateStatement res r - let switch = SwitchStatement (IEConstructorHead exp) swalts (Just swdef) - pure (s1 <+> LetDecl res Nothing <+> switch, IEVar res) - impExp True (NmConCase fc sc alts def) = - do - (s1, exp) <- impExp False sc - swalts <- traverse (impConAltTrue exp) alts - swdef <- case def of - Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc - Just x => impExp True x - let switch = SwitchStatement (IEConstructorHead exp) swalts (Just swdef) - pure (s1 <+> switch) - impExp False (NmConstCase fc sc alts def) = - do - (s1, exp) <- impExp False sc - res <- genName - swalts <- traverse (impConstAltFalse res) alts - swdef <- case def of - Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc - Just x => - do - (sd, r) <- impExp False x - pure $ sd <+> MutateStatement res r - let switch = SwitchStatement exp swalts (Just swdef) - pure (s1 <+> LetDecl res Nothing <+> switch, IEVar res) - impExp True (NmConstCase fc sc alts def) = - do - (s1, exp) <- impExp False sc - swalts <- traverse impConstAltTrue alts - swdef <- case def of - Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc - Just x => impExp True x - let switch = SwitchStatement exp swalts (Just swdef) - pure $ s1 <+> switch - impExp toReturn (NmExtPrim fc p args) = - do - (s, a) <- impListExp args - pairToReturn toReturn (s, IEPrimFnExt p a) - impExp toReturn (NmCon fc x _ tag args) = - do - (s, a) <- impListExp args - pairToReturn toReturn (s, IEConstructor (impTag x tag) a) - impExp toReturn (NmDelay fc _ t) = - do - (s, x) <- impExp False t - pairToReturn toReturn (s, IEDelay x) - impExp toReturn (NmForce fc _ t) = - do - (s, x) <- impExp False t - pairToReturn toReturn (s, IEForce x) - impExp toReturn (NmLet fc x val sc) = - do - (s1, v) <- impExp False val - (s2, sc_) <- impExp False sc - if isNameUsed x sc - then do - x_ <- genName - let reps = [(x, IEVar x_)] - let s2_ = replaceNamesExpS reps s2 - let sc__ = replaceNamesExp reps sc_ - let decl = ConstDecl x_ v - pairToReturn toReturn (s1 <+> decl <+> s2_, sc__) - else do - let decl = EvalExpStatement v - pairToReturn toReturn (s1 <+> decl <+> s2, sc_) - impExp toReturn (NmErased fc) = - expToReturn toReturn $ IENull - impExp toReturn (NmCrash fc msg) = - pairToReturn toReturn (ErrorStatement msg, IENull) + do (s1, f) <- impExp False x + (s2, a) <- impListExp args + pure $ pairToReturn toReturn (s1 <+> s2, IEApp f a) - impTag : Name -> Maybe Int -> Either Int String - impTag n Nothing = Right $ show n - impTag n (Just i) = Left i + -- primitive values + impExp toReturn (NmPrimVal fc c) = + pure . expToReturn toReturn $ IEConstant c + + -- primitive operations + impExp toReturn (NmOp fc op args) = + do (s, a) <- impVectExp args + pure $ pairToReturn toReturn (s, IEPrimFn op a) + + -- a pattern match on a constructor + -- is converted to a switch statement in JS. + -- + -- TODO: We should treat record constructors + -- separately, to avoid the unnecessary + -- switch + -- + -- ``` + -- s1 + -- let res; + -- switch(exp.h) { + -- alternatives + -- default (if any) + -- } + -- res; + -- ``` + impExp False (NmConCase fc sc alts def) = + do (s1, exp) <- impExp False sc + res <- genName + swalts <- traverse (impConAltFalse res exp) alts + swdef <- case def of + Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc + Just x => + do (sd, r) <- impExp False x + pure $ sd <+> MutateStatement res r + let switch = SwitchStatement (IEConstructorHead exp) swalts (Just swdef) + pure (s1 <+> LetDecl res Nothing <+> switch, IEVar res) + + -- like `impExp False NmConCase`, but we return directly without + -- a local let binding + impExp True (NmConCase fc sc alts def) = + do (s1, exp) <- impExp False sc + swalts <- traverse (impConAltTrue exp) alts + swdef <- case def of + Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc + Just x => impExp True x + let switch = SwitchStatement (IEConstructorHead exp) swalts (Just swdef) + pure (s1 <+> switch) + + -- a case statement (pattern match on a constant) + -- is converted to a switch statement in JS. + -- the distinction between `impExp False` and + -- `impExp True` is the same as for constructor matches + impExp False (NmConstCase fc sc alts def) = + do (s1, exp) <- impExp False sc + res <- genName + swalts <- traverse (impConstAltFalse res) alts + swdef <- case def of + Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc + Just x => + do + (sd, r) <- impExp False x + pure $ sd <+> MutateStatement res r + let switch = SwitchStatement exp swalts (Just swdef) + pure (s1 <+> LetDecl res Nothing <+> switch, IEVar res) + + impExp True (NmConstCase fc sc alts def) = + do (s1, exp) <- impExp False sc + swalts <- traverse impConstAltTrue alts + swdef <- case def of + Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc + Just x => impExp True x + let switch = SwitchStatement exp swalts (Just swdef) + pure $ s1 <+> switch + + -- coversion of primitive external functions like + -- `prim__newIORef` + impExp toReturn (NmExtPrim fc p args) = + do (s, a) <- impListExp args + pure $ pairToReturn toReturn (s, IEPrimFnExt p a) + + -- A saturated constructor + -- TODO: Use ConInfo + impExp toReturn (NmCon fc x _ tag args) = + do (s, a) <- impListExp args + pure $ pairToReturn toReturn + (s, IEConstructor (impTag x tag) a) + + -- a delayed computation + impExp toReturn (NmDelay fc _ t) = + do (s, x) <- impExp False t + pure $ pairToReturn toReturn (s, IEDelay x) + + -- a forced computation + impExp toReturn (NmForce fc _ t) = + do (s, x) <- impExp False t + pure $ pairToReturn toReturn (s, IEForce x) + + -- a let statement of the form + -- ```idris + -- let name = expr1 + -- in expr2 + -- + -- ``` + -- is converted to + -- + -- ```javascript + -- expr1_statements; + -- const name_ = expr1_expr; + -- expr2_statements; + -- expr2_expr; + -- ``` + -- where `name_` is a newly generated name, which + -- is replaced in `expr2`. + -- + -- if `name` is not used in `expr2`, this is + -- simplified to + -- + -- ```javascript + -- expr1_statements; + -- expr1_expr; -- evaluation of expr1! + -- expr2_statements; + -- expr2_expr; + -- ``` + -- TODO: Is it necessary to generate a new name + -- here, or is this already handled by Idris itself? + impExp toReturn (NmLet fc x val sc) = + do (s1, v) <- impExp False val + (s2, sc_) <- impExp False sc + if isNameUsed x sc + then do + x_ <- genName + let reps = [(x, IEVar x_)] + let s2_ = replaceNamesExpS reps s2 + let sc__ = replaceNamesExp reps sc_ + let decl = ConstDecl x_ v + pure $ pairToReturn toReturn (s1 <+> decl <+> s2_, sc__) + else do + let decl = EvalExpStatement v + pure $ pairToReturn toReturn (s1 <+> decl <+> s2, sc_) + + -- an erased argument is converted to `undefined` + impExp toReturn (NmErased fc) = + pure . expToReturn toReturn $ IENull + + -- an error is converted to a `throw new Error` + -- statement. It's result is `undefined` (`IENull`). + impExp toReturn (NmCrash fc msg) = + pure $ pairToReturn toReturn (ErrorStatement msg, IENull) -- a single alternative in a case statement. -- In JS, this will be a single alternative of @@ -232,7 +350,11 @@ mutual do s <- impExp True exp pure (IEConstant c, s) -getImp : {auto c : Ref Imps ImpSt} -> (Name, FC, NamedDef) -> Core ImperativeStatement +-- generate an `ImperativeStatement` from the +-- given named definition +getImp : {auto c : Ref Imps ImpSt} + -> (Name, FC, NamedDef) + -> Core ImperativeStatement getImp (n, fc, MkNmFun args exp) = pure $ FunDecl fc n args !(impExp True exp) getImp (n, fc, MkNmError exp) = @@ -242,16 +364,43 @@ getImp (n, fc, MkNmForeign cs args ret) = getImp (n, fc, MkNmCon _ _ _) = pure DoNothing +||| Compiles a `ClosedTerm` to a pair of statements, +||| the first corresponding to a list of toplevel definitions +||| the other being the program's main entry point. +||| +||| Toplevel definitions defined in the given `ClosedTerm` +||| are only included if they are (transitively) being +||| invoked by the main function. +||| +||| In addition, toplevel definitions are tail call optimized +||| (see module `Compiler.ES.TailRec`). export -compileToImperative : Ref Ctxt Defs -> ClosedTerm -> Core (ImperativeStatement, ImperativeStatement) +compileToImperative : Ref Ctxt Defs + -> ClosedTerm + -> Core (ImperativeStatement, ImperativeStatement) compileToImperative c tm = - do - cdata <- getCompileData False Cases tm - let ndefs = namedDefs cdata - let ctm = forget (mainExpr cdata) - ref <- newRef Imps (MkImpSt 0) - lst_defs <- traverse getImp (defsUsedByNamedCExp ctm ndefs) - let defs = concat lst_defs - defs_optim <- tailRecOptim defs - (s, main) <- impExp False ctm - pure $ (defs_optim, s <+> EvalExpStatement main) + do -- generate the named definitions and main expression + -- from the `ClosedTerm` + cdata <- getCompileData False Cases tm + + -- list of named definitions + let ndefs = namedDefs cdata + + -- main expression + let ctm = forget (mainExpr cdata) + + ref <- newRef Imps (MkImpSt 0) + + -- list of toplevel definitions (only those necessary + -- to implement the main expression) + lst_defs <- traverse getImp (defsUsedByNamedCExp ctm ndefs) + + let defs = concat lst_defs + + -- tail rec optimited definitions + defs_optim <- tailRecOptim defs + + -- main expression and statements necessary to + -- implement main's body + (s, main) <- impExp False ctm + pure $ (defs_optim, s <+> EvalExpStatement main) diff --git a/src/Compiler/ES/ImperativeAst.idr b/src/Compiler/ES/ImperativeAst.idr index 38c855f36..86b1fa9ab 100644 --- a/src/Compiler/ES/ImperativeAst.idr +++ b/src/Compiler/ES/ImperativeAst.idr @@ -1,3 +1,8 @@ +||| ASTs representing imperative ES (= ECMAScript) +||| expressions and statements. +||| These are converted to ES code in module `Compiler.ES.ES`. +||| They are generated from `Term []`s in +||| module `Compiler.ES.Imperative`. module Compiler.ES.ImperativeAst import Compiler.CompileExpr @@ -6,35 +11,196 @@ import public Data.Vect import public Data.List mutual + ||| A tree representing an ES expression. + ||| + ||| This is converted to ES code in function + ||| `Compiler.ES.ES.impExp2es`. public export - data ImperativeExp = IEVar Name - | IELambda (List Name) ImperativeStatement - | IEApp ImperativeExp (List ImperativeExp) - | IEConstant Constant - | IEPrimFn (PrimFn arity) (Vect arity ImperativeExp) - | IEPrimFnExt Name (List ImperativeExp) - | IEConstructorHead ImperativeExp - | IEConstructorTag (Either Int String) - | IEConstructorArg Int ImperativeExp -- constructor arg index starts at 1 - | IEConstructor (Either Int String) (List ImperativeExp) - | IEDelay ImperativeExp - | IEForce ImperativeExp - | IENull + data ImperativeExp : Type where + ||| A variable of the given name + IEVar : (name : Name) -> ImperativeExp + ||| A lambda expression : `(args) => { body }` + IELambda : (args : List Name) + -> (body : ImperativeStatement) + -> ImperativeExp + + ||| Function application : `lhs(args)` + IEApp : (lhs : ImperativeExp) + -> (args : List ImperativeExp) + -> ImperativeExp + + ||| A (primitive) constant + IEConstant : (value : Constant) -> ImperativeExp + + ||| A primitive function. This will be converted to + ||| ES code in `Compiler.ES.ES.jsOp`. + IEPrimFn : (function : PrimFn arity) + -> (args : Vect arity ImperativeExp) + -> ImperativeExp + + ||| A primitive external function. Example `prim__newIORef` + IEPrimFnExt : (function : Name) + -> (args : List ImperativeExp) + -> ImperativeExp + + ||| Calls `object.h` on the JS object built by `object` + ||| This is used to extract the constructor, which + ||| this specific object represents. + IEConstructorHead : (object : ImperativeExp) -> ImperativeExp + + ||| Tag representing either a data constructor (in that case + ||| an integer is used as its index) or a type constructor + ||| (these come up when pattern matching on types). + IEConstructorTag : (tag : Either Int String) -> ImperativeExp + + ||| Argument of a data constructor applied to the given JS object. + ||| The arg index starts at 1. + ||| + ||| Example: `object.a3` + IEConstructorArg : (index : Int) + -> (object : ImperativeExp) + -> ImperativeExp + + ||| Creates a JS object using the given constructor + ||| tag and arguments. The corresponding values are + ||| extracted using `IEConstructorTag` and `IEConstructorArg`. + IEConstructor : (tag : Either Int String) + -> (args : List ImperativeExp) + -> ImperativeExp + + ||| A delayed calculation coming either from a `Lazy` + ||| or infinite (`Inf`) value. + ||| + ||| In the JS backends, these are wrapped zero-argument lambdas: + ||| `(() => expr)`. + IEDelay : (expr : ImperativeExp) -> ImperativeExp + + ||| Forces the evaluation of a delayed (`Lazy` or `Inf`) + ||| value. + ||| + ||| In the JS backends, these just invoke the corresponding + ||| zero-argument lambdas: + ||| `expr()`. + IEForce : (expr : ImperativeExp) -> ImperativeExp + + ||| This is converted to `undefined`. + ||| + ||| TODO: This should be renamed to `IEUndefined` in + ||| order not to be confused with the JS constant + ||| `null`. + IENull : ImperativeExp + + ||| A tree of ES statements. + ||| + ||| This is converted to ES code in `Compiler.ES.imperative2es`. public export - data ImperativeStatement = DoNothing - | SeqStatement ImperativeStatement ImperativeStatement - | FunDecl FC Name (List Name) ImperativeStatement - | ForeignDecl FC Name (List String) (List CFType) CFType - | ReturnStatement ImperativeExp - | SwitchStatement ImperativeExp (List (ImperativeExp, ImperativeStatement)) (Maybe ImperativeStatement) - | LetDecl Name (Maybe ImperativeExp) - | ConstDecl Name ImperativeExp - | MutateStatement Name ImperativeExp - | ErrorStatement String - | EvalExpStatement ImperativeExp - | CommentStatement String - | ForEverLoop ImperativeStatement + data ImperativeStatement : Type where + ||| This is converted to the empty string. + DoNothing : ImperativeStatement + + ||| A sequence of statements. These will be processed + ||| individually and separated by a line break. + SeqStatement : (fstStmt : ImperativeStatement) + -> (sndStmt : ImperativeStatement) + -> ImperativeStatement + + ||| A function declaration. This will be converted + ||| to a declaration of the following form: + ||| + ||| ``` + ||| function funName(args){ -- fc + ||| body + ||| } + ||| ``` + FunDecl : (fc : FC) + -> (funName : Name) + -> (args : List Name) + -> (body : ImperativeStatement) + -> ImperativeStatement + + ||| An FFI declaration + ||| + ||| @ ffiImpls : List of implementation strings. + ||| `Compiler.ES.ES.foreignDecl` + ||| will try to lookup a valid codegen prefix like "node" + ||| or "javascript" in each of these and return the + ||| remainder as the actual ES code in case of a success. + ||| + ||| The argtypes and returnType will be ignored when generating + ||| ES code. + ForeignDecl : (fc : FC) + -> (funName : Name) + -> (ffiImpls : List String) + -> (argTypes : List CFType) + -> (returnType : CFType) + -> ImperativeStatement + + ||| A `return` statement. Example: `return body;` + ReturnStatement : (body : ImperativeExp) -> ImperativeStatement + + ||| A `switch` statement of the form + ||| + ||| ``` + ||| switch(expr) { + ||| case altExp1 : { + ||| altImpl1 + ||| break; + ||| } + ||| case altExp2 : { + ||| altImpl2 + ||| break; + ||| } + ||| default: + ||| deflt + ||| } + ||| ``` + SwitchStatement : (expr : ImperativeExp) + -> (alts : List (ImperativeExp, ImperativeStatement)) + -> (deflt : Maybe ImperativeStatement) + -> ImperativeStatement + + ||| A `let` statement with an optional value + ||| This is converted to `let name;` if `value` + ||| is `Nothing` and to `let name = expr;` if + ||| `value` is `Just expr`. + LetDecl : (name : Name) + -> (value : Maybe ImperativeExp) + -> ImperativeStatement + + ||| A `const` declaration. + ||| This is converted to `const name = expr;`. + ConstDecl : (name : Name) + -> (expr : ImperativeExp) + -> ImperativeStatement + + ||| Assigns the given expression to the variable + ||| of the given name: `name = expr;`. + MutateStatement : (name : Name) + -> (expr : ImperativeExp) + -> ImperativeStatement + + ||| Throws an error with the given message: + ||| `throw new Error(msg);`. + ErrorStatement : (msg : String) -> ImperativeStatement + + ||| Evaluates the given expression (by ending the corresponding + ||| ES code with a semicolon): + ||| `expr;`. + EvalExpStatement : (expr : ImperativeExp) -> ImperativeStatement + + ||| Adds the given String as a comment + ||| `/*comment*/`. + CommentStatement : (comment : String) -> ImperativeStatement + + ||| Runs the given statement 'forever': + ||| + ||| ``` + ||| while(true){ + ||| body + ||| } + ||| ``` + ForEverLoop : (body : ImperativeStatement) -> ImperativeStatement public export Semigroup ImperativeStatement where @@ -80,63 +246,42 @@ mutual show (ForEverLoop x) = "(ForEverLoop " ++ show x ++ ")" mutual + ||| Iteratively replaces expressions using + ||| the given function. This is mainly used for + ||| replacing variables according to their name as + ||| in `replaceNamesExp`. public export - replaceExp : (ImperativeExp -> Maybe ImperativeExp) -> ImperativeExp -> ImperativeExp - replaceExp rep x@(IEVar n) = + replaceExp : (ImperativeExp -> Maybe ImperativeExp) + -> ImperativeExp + -> ImperativeExp + replaceExp rep x = case rep x of - Just z => z - Nothing => x - replaceExp rep x@(IELambda args body) = - case rep x of - Just z => z - Nothing => IELambda args $ replaceExpS rep body - replaceExp rep x@(IEApp f args) = - case rep x of - Just z => z - Nothing => IEApp (replaceExp rep f) (replaceExp rep <$> args) - replaceExp rep x@(IEConstant c) = - case rep x of - Just z => z - Nothing => x - replaceExp rep x@(IEPrimFn f args) = - case rep x of - Just z => z - Nothing => IEPrimFn f (replaceExp rep <$> args) - replaceExp rep x@(IEPrimFnExt f args) = - case rep x of - Just z => z - Nothing => IEPrimFnExt f (replaceExp rep <$> args) - replaceExp rep x@(IEConstructorHead e) = - case rep x of - Just z => z - Nothing => IEConstructorHead $ replaceExp rep e - replaceExp rep x@(IEConstructorTag i) = - case rep x of - Just z => z - Nothing => x - replaceExp rep x@(IEConstructorArg i e) = - case rep x of - Just z => z - Nothing => IEConstructorArg i (replaceExp rep e) - replaceExp rep x@(IEConstructor t args) = - case rep x of - Just z => z - Nothing => IEConstructor t (replaceExp rep <$> args) - replaceExp rep x@(IEDelay e) = - case rep x of - Just z => z - Nothing => IEDelay $ replaceExp rep e - replaceExp rep x@(IEForce e) = - case rep x of - Just z => z - Nothing => IEForce $ replaceExp rep e - replaceExp rep x@IENull = - case rep x of - Just z => z - Nothing => x + Just z => z + Nothing => + case x of + IEVar _ => x + IELambda args body => IELambda args $ replaceExpS rep body + IEApp f args => IEApp (replaceExp rep f) + (replaceExp rep <$> args) + IEConstant _ => x + IEPrimFn f args => IEPrimFn f (replaceExp rep <$> args) + IEPrimFnExt f args => IEPrimFnExt f (replaceExp rep <$> args) + IEConstructorHead e => IEConstructorHead $ replaceExp rep e + IEConstructorTag _ => x + IEConstructorArg i e => IEConstructorArg i (replaceExp rep e) + IEConstructor t args => IEConstructor t (replaceExp rep <$> args) + IEDelay e => IEDelay $ replaceExp rep e + IEForce e => IEForce $ replaceExp rep e + IENull => x + ||| Iteratively replaces expressions using + ||| the given function. This is mainly used for + ||| replacing variables according to their name as + ||| in `replaceNamesExpS`. public export - replaceExpS : (ImperativeExp -> Maybe ImperativeExp) -> ImperativeStatement -> ImperativeStatement + replaceExpS : (ImperativeExp -> Maybe ImperativeExp) + -> ImperativeStatement + -> ImperativeStatement replaceExpS rep DoNothing = DoNothing replaceExpS rep (SeqStatement x y) = @@ -168,17 +313,26 @@ mutual ForEverLoop $ replaceExpS rep x -rep : List (Name, ImperativeExp) -> ImperativeExp -> Maybe ImperativeExp -rep reps (IEVar n) = - lookup n reps -rep _ _ = Nothing +rep : List (Name, ImperativeExp) + -> ImperativeExp + -> Maybe ImperativeExp +rep reps (IEVar n) = lookup n reps +rep _ _ = Nothing +||| Replaces all occurences of the names in the +||| assoc list with the corresponding expression. public export -replaceNamesExpS : List (Name, ImperativeExp) -> ImperativeStatement -> ImperativeStatement +replaceNamesExpS : List (Name, ImperativeExp) + -> ImperativeStatement + -> ImperativeStatement replaceNamesExpS reps x = replaceExpS (rep reps) x +||| Replaces all occurences of the names in the +||| assoc list with the corresponding expression. public export -replaceNamesExp : List (Name, ImperativeExp) -> ImperativeExp -> ImperativeExp +replaceNamesExp : List (Name, ImperativeExp) + -> ImperativeExp + -> ImperativeExp replaceNamesExp reps x = replaceExp (rep reps) x diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index 229042219..af77821f4 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -1,3 +1,4 @@ +||| The `Javascript` code generator. module Compiler.ES.Javascript import Compiler.ES.ES @@ -16,11 +17,10 @@ import Data.Maybe import Data.Strings import Libraries.Data.String.Extra - ||| Compile a TT expression to Javascript compileToJS : Ref Ctxt Defs -> ClosedTerm -> Core String -compileToJS c tm = do +compileToJS c tm = compileToES c tm ["browser", "javascript"] htmlHeader : String @@ -47,15 +47,18 @@ addHeaderAndFooter outfile es = _ => es ||| Javascript implementation of the `compileExpr` interface. -compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) -compileExpr c tmpDir outputDir tm outfile - = do es <- compileToJS c tm - let res = addHeaderAndFooter outfile es - let out = outputDir outfile - Right () <- coreLift (writeFile out res) - | Left err => throw (FileErr out err) - pure (Just out) +compileExpr : Ref Ctxt Defs + -> (tmpDir : String) + -> (outputDir : String) + -> ClosedTerm + -> (outfile : String) + -> Core (Maybe String) +compileExpr c tmpDir outputDir tm outfile = + do es <- compileToJS c tm + let res = addHeaderAndFooter outfile es + let out = outputDir outfile + Core.writeFile out res + pure (Just out) ||| Node implementation of the `executeExpr` interface. executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core () diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index 2c6846259..ea36ad950 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -1,3 +1,4 @@ +||| The `Node` generator. module Compiler.ES.Node import Idris.Env @@ -24,28 +25,29 @@ findNode = do pure $ fromMaybe "/usr/bin/env node" path ||| Compile a TT expression to Node -compileToNode : Ref Ctxt Defs -> - ClosedTerm -> Core String +compileToNode : Ref Ctxt Defs -> ClosedTerm -> Core String compileToNode c tm = do compileToES c tm ["node", "javascript"] ||| Node implementation of the `compileExpr` interface. -compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) -compileExpr c tmpDir outputDir tm outfile - = do es <- compileToNode c tm - let out = outputDir outfile - Right () <- coreLift (writeFile out es) - | Left err => throw (FileErr out err) - pure (Just out) +compileExpr : Ref Ctxt Defs + -> (tmpDir : String) + -> (outputDir : String) + -> ClosedTerm + -> (outfile : String) + -> Core (Maybe String) +compileExpr c tmpDir outputDir tm outfile = + do es <- compileToNode c tm + let out = outputDir outfile + Core.writeFile out es + pure (Just out) ||| Node implementation of the `executeExpr` interface. executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core () -executeExpr c tmpDir tm -= do let outn = tmpDir "_tmp_node" ++ ".js" +executeExpr c tmpDir tm = + do let outn = tmpDir "_tmp_node" ++ ".js" js <- compileToNode c tm - Right () <- coreLift $ writeFile outn js - | Left err => throw (FileErr outn err) + Core.writeFile outn js node <- coreLift findNode quoted_node <- pure $ "\"" ++ node ++ "\"" -- Windows often have a space in the path. coreLift_ $ system (quoted_node ++ " " ++ outn) diff --git a/src/Compiler/ES/RemoveUnused.idr b/src/Compiler/ES/RemoveUnused.idr index f01cad681..126005528 100644 --- a/src/Compiler/ES/RemoveUnused.idr +++ b/src/Compiler/ES/RemoveUnused.idr @@ -1,3 +1,8 @@ +||| Functions in this module are responsible to +||| find those toplevel definitions that should +||| be included in the generated JS code since +||| they are (transitively) being invoked by the +||| main function. module Compiler.ES.RemoveUnused import Libraries.Data.SortedSet @@ -16,13 +21,17 @@ mutual usedNames (NmLocal fc n) = empty usedNames (NmRef fc n) = insert n empty usedNames (NmLam fc n e) = usedNames e - usedNames (NmApp fc x args) = usedNames x `union` concat (usedNames <$> args) + usedNames (NmApp fc x args) = usedNames x `union` concatMap usedNames args usedNames (NmPrimVal fc c) = empty - usedNames (NmOp fc op args) = concat $ usedNames <$> args - usedNames (NmConCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConAlt <$> alts)) `union` maybe empty usedNames def - usedNames (NmConstCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConstAlt <$> alts)) `union` maybe empty usedNames def - usedNames (NmExtPrim fc p args) = concat $ usedNames <$> args - usedNames (NmCon fc x _ t args) = concat $ usedNames <$> args + usedNames (NmOp fc op args) = concatMap usedNames args + usedNames (NmConCase fc sc alts def) = + (usedNames sc `union` concatMap usedNamesConAlt alts) `union` + maybe empty usedNames def + usedNames (NmConstCase fc sc alts def) = + (usedNames sc `union` concatMap usedNamesConstAlt alts) + `union` maybe empty usedNames def + usedNames (NmExtPrim fc p args) = concatMap usedNames args + usedNames (NmCon fc x _ t args) = concatMap usedNames args usedNames (NmDelay fc _ t) = usedNames t usedNames (NmForce fc _ t) = usedNames t usedNames (NmLet fc x val sc) = usedNames val `union` usedNames sc @@ -41,11 +50,16 @@ usedNamesDef (MkNmError exp) = usedNames exp usedNamesDef (MkNmForeign cs args ret) = empty usedNamesDef (MkNmCon _ _ _) = empty -defsToUsedMap : List (Name, FC, NamedDef) -> SortedMap Name (SortedSet Name) +defsToUsedMap : List (Name, FC, NamedDef) + -> SortedMap Name (SortedSet Name) defsToUsedMap defs = fromList $ (\(n,_,d)=> (n, usedNamesDef d)) <$> defs -calcUsed : SortedSet Name -> SortedMap Name (SortedSet Name) -> List Name -> SortedSet Name +-- TODO: Should we use `SortedSet Name` instead of `List Name` here? +calcUsed : SortedSet Name + -> SortedMap Name (SortedSet Name) + -> List Name + -> SortedSet Name calcUsed done d [] = done calcUsed done d xs = let used_in_xs = foldl f empty $ (\z => lookup z d) <$> xs @@ -56,11 +70,23 @@ calcUsed done d xs = f x Nothing = x f x (Just y) = union x y -calcUsedDefs : List Name -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef) +calcUsedDefs : List Name + -> List (Name, FC, NamedDef) + -> List (Name, FC, NamedDef) calcUsedDefs names defs = let usedNames = calcUsed empty (defsToUsedMap defs) names in List.filter (\(n, fc, d) => contains n usedNames) defs +||| Filters a list of toplevel definitions, keeping only those +||| that are (transitively) used by the given expression. +||| +||| @ exp : Expression invoking some of the toplevel +||| definitions. Typically, this is the expression implementing +||| a program's `main` function. +||| @ defs : List of toplevel definitions. export -defsUsedByNamedCExp : NamedCExp -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef) -defsUsedByNamedCExp exp defs = calcUsedDefs (SortedSet.toList $ usedNames exp) defs +defsUsedByNamedCExp : (exp : NamedCExp) + -> (defs : List (Name, FC, NamedDef)) + -> List (Name, FC, NamedDef) +defsUsedByNamedCExp exp defs = + calcUsedDefs (SortedSet.toList $ usedNames exp) defs diff --git a/src/Compiler/ES/TailRec.idr b/src/Compiler/ES/TailRec.idr index 533520976..facdabe29 100644 --- a/src/Compiler/ES/TailRec.idr +++ b/src/Compiler/ES/TailRec.idr @@ -1,8 +1,90 @@ +||| Tail-call optimization. +||| +||| Here is a lengthy explanation how this works at the +||| moment. Assume the following call graph of functions f1,f2,f3,f4 all +||| calling each other in tail call position: +||| +||| ``` +||| ------------ f2 ---- f4 (result) +||| / / \ +||| f1 ---- f1 / -- f1 +||| \ / +||| -- f3 -- +||| ``` +||| +||| Function `tailCallGraph` creates a directed graph of all toplevel +||| function calls (incoming and outgoing) in tail-call position: +||| +||| ```idris +||| MkCallGraph $ fromList [(f1,[f1,f2,f3]),(f2,[f1,f4]),(f3,[f2])] +||| $ fromList [(f1,[f1,f2]),(f2,[f1,f3]),(f3,[f1]),(f4,[f2])] +||| ``` +||| +||| Mutually tail-recursive functions form a strongly connected +||| component in such a call graph: There is a (directed) path from every function +||| to every other function. Kosaraju's algorithm is used to identify +||| these strongly connected components by mapping every function +||| of a strongly connected component to the same representative (called `root`) +||| of its component. In the above case, this would result in a sorted +||| map of the following structure: +||| +||| +||| ```idris +||| fromList [(f1,f1),(f1,f2),(f1,f3),(f4,f4)] +||| ```idris +||| +||| As can be seen, f1,f2, and f3 all point to the same root (f1), while +||| f4 points to a different root. +||| +||| Such a tail-recursive call graph is now converted to an imperative +||| loop as follows: Let `obj0={h:0, a1:...}` be a Javascript object consisting +||| of a tag `h` and an argument `a1`. `h` indicates, whether `obj0.a1` +||| contains the result of the computation (`h = 1`) or describes +||| a continuation indicating the next function to invoke +||| together with the necessary arguments. A single `step` +||| function will take such an object and use `a1` in a switch +||| statement to decide , which function +||| implementation to invoke (f1,f2,f3). +||| The result will be a new object, again indicating in tag `h`, whether +||| we arrived at a result, or we need to continue looping. +||| +||| Here is a cleaned-up and simplified version of the Javascript code +||| generated: +||| +||| ```javascript +||| function imp_gen_tailoptim_0(imp_gen_tailoptim_fusion_args_0){//EmptyFC +||| function imp_gen_tailoptim_step_0(obj0){ +||| switch(obj0.a1.h){ +||| case 0: ... //implementation of a single step of f1 +||| //taking its arguments from the fields of `obj0.a1`. +||| case 1: ... //implementation of a single step of f2 +||| case 2: ... //implementation of a single step of f3 +||| } +||| } +||| +||| // initial object containing the arguments for the first +||| // function call +||| obj0 = ({h:0, a1: imp_gen_tailoptim_fusion_args_0}); +||| +||| // infinite loop running until `obj0.h != 0`. +||| while(true){ +||| switch(obj0.h){ +||| case 0: { +||| obj0 = imp_gen_tailoptim_step_0(obj0); +||| break; } +||| default: +||| return obj0.a1; +||| } +||| } +||| } +||| ``` module Compiler.ES.TailRec import Data.Maybe import Data.List +import Data.List1 import Data.Strings +import Libraries.Data.List.Extra as L import Libraries.Data.SortedSet import Libraries.Data.SortedMap import Core.Name @@ -19,26 +101,21 @@ record TailSt where genName : {auto c : Ref TailRecS TailSt} -> Core Name genName = - do - s <- get TailRecS - let i = nextName s - put TailRecS (record { nextName = i + 1 } s) - pure $ MN "imp_gen_tailoptim" i + do s <- get TailRecS + let i = nextName s + put TailRecS (record { nextName = i + 1 } s) + pure $ MN "imp_gen_tailoptim" i +-- returns the set of tail calls made from a given +-- imperative statement. allTailCalls : ImperativeStatement -> SortedSet Name -allTailCalls (SeqStatement x y) = - allTailCalls y -allTailCalls (ReturnStatement x) = - case x of - IEApp (IEVar n) _ => insert n empty - _ => empty +allTailCalls (SeqStatement x y) = allTailCalls y +allTailCalls (ReturnStatement $ IEApp (IEVar n) _) = singleton n allTailCalls (SwitchStatement e alts d) = - maybe empty allTailCalls d `union` concat (map allTailCalls (map snd alts)) -allTailCalls (ForEverLoop x) = - allTailCalls x + concatMap allTailCalls d `union` concatMap (allTailCalls . snd) alts +allTailCalls (ForEverLoop x) = allTailCalls x allTailCalls o = empty - argsName : Name argsName = MN "imp_gen_tailoptim_Args" 0 @@ -49,9 +126,7 @@ fusionArgsName : Name fusionArgsName = MN "imp_gen_tailoptim_fusion_args" 0 createNewArgs : List ImperativeExp -> ImperativeExp -createNewArgs values = - IEConstructor (Left 0) values - +createNewArgs = IEConstructor (Left 0) createArgInit : List Name -> ImperativeStatement createArgInit names = @@ -67,26 +142,50 @@ replaceTailCall n (ReturnStatement x) = else defRet _ => defRet replaceTailCall n (SwitchStatement e alts d) = - SwitchStatement e (map (\(x,y) => (x, replaceTailCall n y)) alts) (map (replaceTailCall n) d) + SwitchStatement e (map (mapSnd $ replaceTailCall n) alts) + (map (replaceTailCall n) d) replaceTailCall n (ForEverLoop x) = ForEverLoop $ replaceTailCall n x replaceTailCall n o = o -makeTailOptimToBody : Name -> List Name -> ImperativeStatement -> ImperativeStatement +-- generates the tailcall-optimized function body +makeTailOptimToBody : Name + -> List Name + -> ImperativeStatement + -> ImperativeStatement makeTailOptimToBody n argNames body = - let lastArg = (length argNames) + 1 - newArgExp = map (\x => IEConstructorArg (cast x) (IEVar argsName)) [1..lastArg] + let newArgExp = map (\x => IEConstructorArg (cast x) (IEVar argsName)) [1..length argNames] bodyArgsReplaced = replaceNamesExpS (zip argNames newArgExp) body stepBody = replaceTailCall n bodyArgsReplaced + + -- single step function. This takes a single argument + -- and returns a new object indicating whether to continue looping + -- or to return a result. stepFn = FunDecl EmptyFC stepFnName [argsName] stepBody + + -- calls the step function and mutates the loop object with the result loopRec = MutateStatement argsName (IEApp (IEVar stepFnName) [IEVar argsName]) + + -- returns field `a1` from the loop object. loopReturn = ReturnStatement (IEConstructorArg 1 $ IEVar argsName) - loop = ForEverLoop $ SwitchStatement (IEConstructorHead $ IEVar argsName) [(IEConstructorTag $ Left 0, loopRec)] (Just loopReturn) + + -- switch on the constructor head and either continue looping or + -- return the result + loop = ForEverLoop + $ SwitchStatement (IEConstructorHead $ IEVar argsName) + [(IEConstructorTag $ Left 0, loopRec)] + (Just loopReturn) in stepFn <+> createArgInit argNames <+> loop +||| A directed graph mapping function names +||| to the set of names they directly call and +||| to the set of names from which they are directly called record CallGraph where - constructor MkCallGraph - calls, callers : SortedMap Name (SortedSet Name) + constructor MkCallGraph + ||| Map function names to function names they call + calls : SortedMap Name (SortedSet Name) + ||| Map function names to function names, from which they are called + callers : SortedMap Name (SortedSet Name) showCallGraph : CallGraph -> String showCallGraph x = @@ -98,83 +197,95 @@ showCallGraph x = (SortedMap.toList x.callers) in calls ++ "\n----\n" ++ callers - +-- when creating the tail call graph, we only process +-- function declarations and we are only interested +-- in calls being made at tail position tailCallGraph : ImperativeStatement -> CallGraph tailCallGraph (SeqStatement x y) = - let xg = tailCallGraph x - yg = tailCallGraph y - in MkCallGraph + let xg = tailCallGraph x + yg = tailCallGraph y + in MkCallGraph (mergeWith union xg.calls yg.calls) (mergeWith union xg.callers yg.callers) + tailCallGraph (FunDecl fc n args body) = - let calls = allTailCalls body - in MkCallGraph (insert n calls empty) (SortedMap.fromList $ map (\x => (x, SortedSet.insert n empty)) (SortedSet.toList calls)) + let calls = allTailCalls body + in MkCallGraph (singleton n calls) (toSortedMap calls $> singleton n) + tailCallGraph _ = MkCallGraph empty empty -kosarajuL : SortedSet Name -> List Name -> CallGraph -> (SortedSet Name, List Name) -kosarajuL visited [] graph = - (visited, []) +-- lookup up the list of values associated with +-- a given key (`Nil` if the key is not present in the list) +lookupList : k -> SortedMap k (SortedSet b) -> List b +lookupList v = maybe [] SortedSet.toList . lookup v + +-- look up the nodes transitively called from +-- the given list of callers. already visited nodes +-- (as indicated by `visited`) are ignored +-- +-- For the resulting list, the following post-condition holds: +-- if x is callable from y, then y will appear before x in the list. +kosarajuL : (visited : SortedSet Name) + -> (callers : List Name) + -> (graph : CallGraph) + -> (SortedSet Name, List Name) +kosarajuL visited [] graph = (visited, []) kosarajuL visited (x::xs) graph = - if contains x visited then kosarajuL visited xs graph - else let outNeighbours = maybe [] SortedSet.toList $ lookup x (graph.calls) - (visited_, l_) = kosarajuL (insert x visited) (toList outNeighbours) graph - (visited__, l__) = kosarajuL visited_ xs graph - in (visited__, l__ ++ (x :: l_)) + if contains x visited + then kosarajuL visited xs graph + else let outNeighbours = lookupList x (graph.calls) + (visited2, l2) = kosarajuL (insert x visited) outNeighbours graph + (visited3, l3) = kosarajuL visited2 xs graph + in (visited3, l3 ++ (x :: l2)) +kosarajuAssign : CallGraph + -> (root : Name) + -> SortedMap Name Name + -> (u : Name) + -> SortedMap Name Name +kosarajuAssign graph root s u = + case lookup u s of + Just _ => s + Nothing => + let inNeighbours = lookupList u (graph.callers) + in foldl (kosarajuAssign graph root) (insert u root s) inNeighbours - -kosarajuAssign : CallGraph -> Name -> Name -> SortedMap Name Name -> SortedMap Name Name -kosarajuAssign graph u root s = - case lookup u s of - Just _ => s - Nothing => let inNeighbours = maybe [] SortedSet.toList $ lookup u (graph.callers) - in foldl (\acc, elem => kosarajuAssign graph elem root acc) (insert u root s) inNeighbours - -kosaraju: CallGraph -> SortedMap Name Name +-- associates every caller in a call graph with +-- an arbitrary root node of its strongly connected +-- component. +-- +-- This allows us to find the strongly connected components +-- of a tail-call graph, by grouping nodes by their +-- assigned root node. +-- +-- See https://en.wikipedia.org/wiki/Kosaraju%27s_algorithm +kosaraju : CallGraph -> SortedMap Name Name kosaraju graph = let l = snd $ kosarajuL empty (keys $ graph.calls) graph - in foldl (\acc, elem => kosarajuAssign graph elem elem acc) empty l - -groupBy : (a -> a -> Bool) -> List a -> List (List a) -groupBy _ [] = [] -groupBy p' (x'::xs') = - let (ys',zs') = go p' x' xs' - in (x' :: ys') :: zs' - where - go : (a -> a -> Bool) -> a -> List a -> (List a, List (List a)) - go p z (x::xs) = - let (ys,zs) = go p x xs - in case p z x of - True => (x :: ys, zs) - False => ([], (x :: ys) :: zs) - go _ _ [] = ([], []) + in foldl (\acc, elem => kosarajuAssign graph elem acc elem) empty l recursiveTailCallGroups : CallGraph -> List (List Name) recursiveTailCallGroups graph = - let roots = kosaraju graph - groups = map (map fst) $ - groupBy (\x,y => Builtin.snd x == Builtin.snd y) $ - sortBy (\x,y=> compare (snd x) (snd y)) $ - toList roots - in [x | x<-groups, hasTailCalls x] - where - hasTailCalls : List Name -> Bool - hasTailCalls [] = - False - hasTailCalls [x] = - case lookup x (graph.calls) of - Nothing => - False - Just s => - case SortedSet.toList s of - [n] => n == x - _ => False - hasTailCalls _ = - True + let roots = kosaraju graph + groups = map (map fst) . L.groupAllWith snd $ toList roots + in [forget x | x<-groups, hasTailCalls x] + -- in case of larger groups (more than one element) + -- the group contains tailcalls by construction. In case + -- of a single function, we need to check that at least one + -- outgoing tailcall goes back to the function itself. + where hasTailCalls : List1 Name -> Bool + hasTailCalls (x ::: Nil) = x `elem` lookupList x (graph.calls) + hasTailCalls _ = True -extractFunctions : SortedSet Name -> ImperativeStatement -> - (ImperativeStatement, SortedMap Name (FC, List Name, ImperativeStatement)) +-- extracts the functions belonging to the given tailcall +-- group from the given imperative statement, thereby removing +-- them from the given statement. +extractFunctions : (tailCallGroup : SortedSet Name) + -> ImperativeStatement + -> ( ImperativeStatement + , SortedMap Name (FC, List Name, ImperativeStatement) + ) extractFunctions toExtract (SeqStatement x y) = let (xs, xf) = extractFunctions toExtract x (ys, yf) = extractFunctions toExtract y @@ -185,17 +296,23 @@ extractFunctions toExtract f@(FunDecl fc n args body) = extractFunctions toExtract x = (x, empty) -getDef : SortedMap Name (FC, List Name, ImperativeStatement) -> Name -> Core (FC, List Name, ImperativeStatement) +-- lookup a function definition, throwing a compile-time error +-- if none is found +getDef : SortedMap Name (FC, List Name, ImperativeStatement) + -> Name + -> Core (FC, List Name, ImperativeStatement) getDef defs n = case lookup n defs of Nothing => throw $ (InternalError $ "Can't find function definition in tailRecOptim") Just x => pure x - -makeFusionBranch : Name -> List (Name, Nat) -> (Nat, FC, List Name, ImperativeStatement) -> - (ImperativeExp, ImperativeStatement) +makeFusionBranch : Name + -> List (Name, Nat) + -> (Nat, FC, List Name, ImperativeStatement) + -> (ImperativeExp, ImperativeStatement) makeFusionBranch fusionName functionsIdx (i, _, args, body) = - let newArgExp = map (\i => IEConstructorArg (cast i) (IEVar fusionArgsName)) [1..(length args)] + let newArgExp = map (\i => IEConstructorArg (cast i) (IEVar fusionArgsName)) + [1..length args] bodyRepArgs = replaceNamesExpS (zip args newArgExp) body in (IEConstructorTag $ Left $ cast i, replaceExpS rep bodyRepArgs) where @@ -204,49 +321,53 @@ makeFusionBranch fusionName functionsIdx (i, _, args, body) = case lookup n functionsIdx of Nothing => Nothing Just i => Just $ IEApp - (IEVar fusionName) - [IEConstructor (Left $ cast i) arg_vals] + (IEVar fusionName) + [IEConstructor (Left $ cast i) arg_vals] rep _ = Nothing -changeBodyToUseFusion : Name -> (Nat, Name, FC, List Name, ImperativeStatement) -> ImperativeStatement +changeBodyToUseFusion : Name + -> (Nat, Name, FC, List Name, ImperativeStatement) + -> ImperativeStatement changeBodyToUseFusion fusionName (i, n, (fc, args, _)) = - FunDecl fc n args (ReturnStatement $ IEApp (IEVar fusionName) [IEConstructor (Left $ cast i) (map IEVar args)]) + FunDecl fc n args (ReturnStatement $ IEApp (IEVar fusionName) + [IEConstructor (Left $ cast i) (map IEVar args)]) -tailRecOptimGroup : {auto c : Ref TailRecS TailSt} -> - SortedMap Name (FC, List Name, ImperativeStatement) -> - List Name -> Core ImperativeStatement +tailRecOptimGroup : {auto c : Ref TailRecS TailSt} + -> SortedMap Name (FC, List Name, ImperativeStatement) + -> List Name -> Core ImperativeStatement tailRecOptimGroup defs [] = pure neutral tailRecOptimGroup defs [n] = - do - (fc, args , body) <- getDef defs n - pure $ FunDecl fc n args (makeTailOptimToBody n args body) + do (fc, args , body) <- getDef defs n + pure $ FunDecl fc n args (makeTailOptimToBody n args body) + tailRecOptimGroup defs names = - do - fusionName <- genName - d <- traverse (getDef defs) names - let ids = [0..(length names `minus` 1)] - let alts = map (makeFusionBranch fusionName (zip names ids)) (zip ids d) - let fusionBody = SwitchStatement - (IEConstructorHead $ IEVar fusionArgsName) - alts - Nothing - let fusionArgs = [fusionArgsName] - let fusion = FunDecl EmptyFC fusionName fusionArgs (makeTailOptimToBody fusionName fusionArgs fusionBody) - let newFunctions = Prelude.concat $ map - (changeBodyToUseFusion fusionName) - (ids `zip` (names `zip` d)) - pure $ fusion <+> newFunctions - - + do fusionName <- genName + d <- traverse (getDef defs) names + let ids = [0..(length names `minus` 1)] + let alts = map (makeFusionBranch fusionName (zip names ids)) (zip ids d) + let fusionBody = SwitchStatement + (IEConstructorHead $ IEVar fusionArgsName) + alts + Nothing + let fusionArgs = [fusionArgsName] + let fusion = FunDecl EmptyFC + fusionName + fusionArgs + (makeTailOptimToBody fusionName fusionArgs fusionBody) + let newFunctions = Prelude.concat $ map + (changeBodyToUseFusion fusionName) + (ids `zip` (names `zip` d)) + pure $ fusion <+> newFunctions +||| (Mutual) Tail recursion optimizations: Converts all groups of +||| mutually tail recursive functions to an imperative loop. export -tailRecOptim : ImperativeStatement -> Core ImperativeStatement +tailRecOptim : ImperativeStatement -> Core ImperativeStatement tailRecOptim x = - do - ref <- newRef TailRecS (MkTailSt 0) - let graph = tailCallGraph x - let groups = recursiveTailCallGroups graph - let functionsToOptimize = foldl SortedSet.union empty $ map SortedSet.fromList groups - let (unchanged, defs) = extractFunctions functionsToOptimize x - optimized <- traverse (tailRecOptimGroup defs) groups - pure $ unchanged <+> (concat optimized) + do ref <- newRef TailRecS (MkTailSt 0) + let graph = tailCallGraph x + let groups = recursiveTailCallGroups graph + let functionsToOptimize = foldl SortedSet.union empty $ map SortedSet.fromList groups + let (unchanged, defs) = extractFunctions functionsToOptimize x + optimized <- traverse (tailRecOptimGroup defs) groups + pure $ unchanged <+> (concat optimized) diff --git a/src/Libraries/Data/List/Extra.idr b/src/Libraries/Data/List/Extra.idr index 36cc1376f..9ca165cc6 100644 --- a/src/Libraries/Data/List/Extra.idr +++ b/src/Libraries/Data/List/Extra.idr @@ -81,3 +81,32 @@ dedup xs = xs export sortedNub : Ord a => List a -> List a sortedNub = dedup . sort + +||| TODO: use the version in `Data.List1` in base after the next release. +export +groupBy : (a -> a -> Bool) -> List a -> List (List1 a) +groupBy _ [] = [] +groupBy eq (h :: t) = let (ys,zs) = go h t + in ys :: zs + + where go : a -> List a -> (List1 a, List (List1 a)) + go v [] = (singleton v,[]) + go v (x :: xs) = let (ys,zs) = go x xs + in if eq v x + then (cons v ys, zs) + else (singleton v, ys :: zs) + +||| TODO: use the version in `Data.List1` in base after the next release. +export +group : Eq a => List a -> List (List1 a) +group = Libraries.Data.List.Extra.groupBy (==) + +||| TODO: use the version in `Data.List1` in base after the next release. +export +groupWith : Eq b => (a -> b) -> List a -> List (List1 a) +groupWith f = Libraries.Data.List.Extra.groupBy (\x,y => f x == f y) + +||| TODO: use the version in `Data.List1` in base after the next release. +export +groupAllWith : Ord b => (a -> b) -> List a -> List (List1 a) +groupAllWith f = Libraries.Data.List.Extra.groupWith f . sortBy (comparing f) diff --git a/src/Libraries/Data/SortedSet.idr b/src/Libraries/Data/SortedSet.idr index b3cc14053..6a0bf8cfd 100644 --- a/src/Libraries/Data/SortedSet.idr +++ b/src/Libraries/Data/SortedSet.idr @@ -71,3 +71,7 @@ keySet = SetWrapper . map (const ()) export singleton : Ord k => k -> SortedSet k singleton k = insert k empty + +export +toSortedMap : SortedSet k -> SortedMap k () +toSortedMap (SetWrapper m) = m