idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 01:09:03 +03:00
Code Issues Projects Releases Wiki Activity

[ cleanup ] Annotate JS backend sources (#1425)

Browse Source
This commit is contained in:
Stefan Höck 2021-05-18 13:37:51 +02:00 committed by GitHub
parent 2f66f3e006
commit 66f3787cb7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 907 additions and 379 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
libs/base/Data/List.idr
View File

@ -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
--------------------------------------------------------------------------------

1
src/Compiler/ES/ES.idr
View File

@ -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))

287
src/Compiler/ES/Imperative.idr
View File

@ -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,76 +59,153 @@ record ImpSt where
genName : {auto c : Ref Imps ImpSt} -> Core Name
genName =
do
s <- get Imps
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
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
pure $ pairToReturn toReturn (s1 <+> s2, IEApp f a)
-- 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
pairToReturn toReturn (s, IEPrimFn op a)
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
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
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
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
do (s1, exp) <- impExp False sc
res <- genName
swalts <- traverse (impConstAltFalse res) alts
swdef <- case def of
@ -134,34 +216,69 @@ mutual
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
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
pairToReturn toReturn (s, IEPrimFnExt p a)
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
pairToReturn toReturn (s, IEConstructor (impTag x tag) a)
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
pairToReturn toReturn (s, IEDelay x)
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
pairToReturn toReturn (s, IEForce x)
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
do (s1, v) <- impExp False val
(s2, sc_) <- impExp False sc
if isNameUsed x sc
then do
@ -170,18 +287,19 @@ mutual
let s2_ = replaceNamesExpS reps s2
let sc__ = replaceNamesExp reps sc_
let decl = ConstDecl x_ v
pairToReturn toReturn (s1 <+> decl <+> s2_, sc__)
pure $ 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)
pure $ pairToReturn toReturn (s1 <+> decl <+> s2, sc_)
impTag : Name -> Maybe Int -> Either Int String
impTag n Nothing = Right $ show n
impTag n (Just i) = Left i
-- 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
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)

320
src/Compiler/ES/ImperativeAst.idr
View File

@ -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
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 : 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

19
src/Compiler/ES/Javascript.idr
View File

@ -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,14 +47,17 @@ 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
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)
Core.writeFile out res
pure (Just out)
||| Node implementation of the `executeExpr` interface.

26
src/Compiler/ES/Node.idr
View File

@ -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
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)
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)

48
src/Compiler/ES/RemoveUnused.idr
View File

@ -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

305
src/Compiler/ES/TailRec.idr
View File

@ -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
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)
||| 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,7 +197,9 @@ 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
@ -106,75 +207,85 @@ tailCallGraph (SeqStatement x 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))
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 -> Name -> Name -> SortedMap Name Name -> SortedMap Name Name
kosarajuAssign graph u root s =
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 = maybe [] SortedSet.toList $ lookup u (graph.callers)
in foldl (\acc, elem => kosarajuAssign graph elem root acc) (insert u root s) inNeighbours
Nothing =>
let inNeighbours = lookupList u (graph.callers)
in foldl (kosarajuAssign graph root) (insert u root s) inNeighbours
-- 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
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
@ -208,21 +325,23 @@ makeFusionBranch fusionName functionsIdx (i, _, args, body) =
[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
do (fc, args , body) <- getDef defs n
pure $ FunDecl fc n args (makeTailOptimToBody n args body)
tailRecOptimGroup defs names =
do
fusionName <- genName
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)
@ -231,19 +350,21 @@ tailRecOptimGroup defs names =
alts
Nothing
let fusionArgs = [fusionArgsName]
let fusion = FunDecl EmptyFC fusionName fusionArgs (makeTailOptimToBody fusionName fusionArgs fusionBody)
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 x =
do
ref <- newRef TailRecS (MkTailSt 0)
do ref <- newRef TailRecS (MkTailSt 0)
let graph = tailCallGraph x
let groups = recursiveTailCallGroups graph
let functionsToOptimize = foldl SortedSet.union empty $ map SortedSet.fromList groups

29
src/Libraries/Data/List/Extra.idr
View File

@ -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)

4
src/Libraries/Data/SortedSet.idr
View File

@ -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