From 599d0635e90c11b565353bb5a8063938f7fbd24c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stefan=20H=C3=B6ck?= Date: Sat, 10 Jul 2021 10:15:21 +0000 Subject: [PATCH] [ refactor ] JS backend overhaul (#1609) --- idris2api.ipkg | 8 +- libs/base/Data/Buffer.idr | 42 +- libs/base/System.idr | 6 +- libs/base/System/File.idr | 8 +- libs/prelude/PrimIO.idr | 2 +- src/Compiler/ES/Ast.idr | 195 +++++++ src/Compiler/ES/Codegen.idr | 725 +++++++++++++++++++++++++ src/Compiler/ES/Doc.idr | 106 ++++ src/Compiler/ES/ES.idr | 577 -------------------- src/Compiler/ES/Imperative.idr | 423 --------------- src/Compiler/ES/ImperativeAst.idr | 340 ------------ src/Compiler/ES/Javascript.idr | 6 +- src/Compiler/ES/Node.idr | 6 +- src/Compiler/ES/State.idr | 237 ++++++++ src/Compiler/ES/TailRec.idr | 508 +++++++++-------- src/Compiler/ES/ToAst.idr | 238 ++++++++ support/js/support.js | 186 +++++++ support/js/support_system_directory.js | 8 +- support/js/support_system_file.js | 22 +- tests/node/casts/Casts.idr | 30 +- tests/node/integers/TestIntegers.idr | 6 +- tests/node/integers/expected | 28 +- tests/node/newints/IntOps.idr | 2 +- tests/node/node015/expected | 2 +- tests/node/node024/BitOps.idr | 13 +- tests/node/node024/expected | 18 +- 26 files changed, 2069 insertions(+), 1673 deletions(-) create mode 100644 src/Compiler/ES/Ast.idr create mode 100644 src/Compiler/ES/Codegen.idr create mode 100644 src/Compiler/ES/Doc.idr delete mode 100644 src/Compiler/ES/ES.idr delete mode 100644 src/Compiler/ES/Imperative.idr delete mode 100644 src/Compiler/ES/ImperativeAst.idr create mode 100644 src/Compiler/ES/State.idr create mode 100644 src/Compiler/ES/ToAst.idr create mode 100644 support/js/support.js diff --git a/idris2api.ipkg b/idris2api.ipkg index bf6087d1d..c5513ada1 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -17,12 +17,14 @@ modules = Compiler.Separate, Compiler.VMCode, - Compiler.ES.ES, - Compiler.ES.Imperative, - Compiler.ES.ImperativeAst, + Compiler.ES.Ast, + Compiler.ES.Codegen, + Compiler.ES.Doc, Compiler.ES.Javascript, Compiler.ES.Node, + Compiler.ES.State, Compiler.ES.TailRec, + Compiler.ES.ToAst, Compiler.Interpreter.VMCode, diff --git a/libs/base/Data/Buffer.idr b/libs/base/Data/Buffer.idr index 60076cd43..bf6a401f1 100644 --- a/libs/base/Data/Buffer.idr +++ b/libs/base/Data/Buffer.idr @@ -19,7 +19,7 @@ data Buffer : Type where [external] %foreign "scheme:blodwen-buffer-size" "RefC:getBufferSize" - "node:lambda:b => BigInt(b.length)" + "node:lambda:b => b.length" prim__bufferSize : Buffer -> Int export %inline @@ -28,7 +28,7 @@ rawSize buf = pure (prim__bufferSize buf) %foreign "scheme:blodwen-new-buffer" "RefC:newBuffer" - "node:lambda:s=>Buffer.alloc(Number(s))" + "node:lambda:s=>Buffer.alloc(s)" prim__newBuffer : Int -> PrimIO Buffer export @@ -44,12 +44,12 @@ newBuffer size %foreign "scheme:blodwen-buffer-setbyte" "RefC:setBufferByte" - "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))" + "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)" prim__setByte : Buffer -> Int -> Int -> PrimIO () %foreign "scheme:blodwen-buffer-setbyte" "RefC:setBufferByte" - "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))" + "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)" prim__setBits8 : Buffer -> Int -> Bits8 -> PrimIO () -- Assumes val is in the range 0-255 @@ -65,12 +65,12 @@ setBits8 buf loc val %foreign "scheme:blodwen-buffer-getbyte" "RefC:getBufferByte" - "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))" + "node:lambda:(buf,offset)=>buf.readUInt8(offset)" prim__getByte : Buffer -> Int -> PrimIO Int %foreign "scheme:blodwen-buffer-getbyte" "RefC:getBufferByte" - "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))" + "node:lambda:(buf,offset)=>buf.readUInt8(offset)" prim__getBits8 : Buffer -> Int -> PrimIO Bits8 export %inline @@ -84,7 +84,7 @@ getBits8 buf loc = primIO (prim__getBits8 buf loc) %foreign "scheme:blodwen-buffer-setbits16" - "node:lambda:(buf,offset,value)=>buf.writeUInt16LE(Number(value), Number(offset))" + "node:lambda:(buf,offset,value)=>buf.writeUInt16LE(value, offset)" prim__setBits16 : Buffer -> Int -> Bits16 -> PrimIO () export %inline @@ -93,7 +93,7 @@ setBits16 buf loc val = primIO (prim__setBits16 buf loc val) %foreign "scheme:blodwen-buffer-getbits16" - "node:lambda:(buf,offset)=>BigInt(buf.readUInt16LE(Number(offset)))" + "node:lambda:(buf,offset)=>buf.readUInt16LE(offset)" prim__getBits16 : Buffer -> Int -> PrimIO Bits16 export %inline @@ -102,7 +102,7 @@ getBits16 buf loc = primIO (prim__getBits16 buf loc) %foreign "scheme:blodwen-buffer-setbits32" - "node:lambda:(buf,offset,value)=>buf.writeUInt32LE(Number(value), Number(offset))" + "node:lambda:(buf,offset,value)=>buf.writeUInt32LE(value, offset)" prim__setBits32 : Buffer -> Int -> Bits32 -> PrimIO () export %inline @@ -111,7 +111,7 @@ setBits32 buf loc val = primIO (prim__setBits32 buf loc val) %foreign "scheme:blodwen-buffer-getbits32" - "node:lambda:(buf,offset)=>BigInt(buf.readUInt32LE(Number(offset)))" + "node:lambda:(buf,offset)=>buf.readUInt32LE(offset)" prim__getBits32 : Buffer -> Int -> PrimIO Bits32 export %inline @@ -136,7 +136,7 @@ getBits64 buf loc = primIO (prim__getBits64 buf loc) %foreign "scheme:blodwen-buffer-setint32" - "node:lambda:(buf,offset,value)=>buf.writeInt32LE(Number(value), Number(offset))" + "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)" prim__setInt32 : Buffer -> Int -> Int -> PrimIO () export %inline @@ -145,7 +145,7 @@ setInt32 buf loc val = primIO (prim__setInt32 buf loc val) %foreign "scheme:blodwen-buffer-getint32" - "node:lambda:(buf,offset)=>BigInt(buf.readInt32LE(Number(offset)))" + "node:lambda:(buf,offset)=>buf.readInt32LE(offset)" prim__getInt32 : Buffer -> Int -> PrimIO Int export %inline @@ -155,7 +155,7 @@ getInt32 buf loc %foreign "scheme:blodwen-buffer-setint" "RefC:setBufferInt" - "node:lambda:(buf,offset,value)=>buf.writeInt64(Number(value), Number(offset))" + "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)" prim__setInt : Buffer -> Int -> Int -> PrimIO () export %inline @@ -165,7 +165,7 @@ setInt buf loc val %foreign "scheme:blodwen-buffer-getint" "RefC:getBufferInt" - "node:lambda:(buf,offset)=>BigInt(buf.readInt64(Number(offset)))" + "node:lambda:(buf,offset)=>buf.readInt32LE(offset)" prim__getInt : Buffer -> Int -> PrimIO Int export %inline @@ -175,7 +175,7 @@ getInt buf loc %foreign "scheme:blodwen-buffer-setdouble" "RefC:setBufferDouble" - "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, Number(offset))" + "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, offset)" prim__setDouble : Buffer -> Int -> Double -> PrimIO () export %inline @@ -185,7 +185,7 @@ setDouble buf loc val %foreign "scheme:blodwen-buffer-getdouble" "RefC:getBufferDouble" - "node:lambda:(buf,offset)=>buf.readDoubleLE(Number(offset))" + "node:lambda:(buf,offset)=>buf.readDoubleLE(offset)" prim__getDouble : Buffer -> Int -> PrimIO Double export %inline @@ -200,7 +200,7 @@ stringByteLength : String -> Int %foreign "scheme:blodwen-buffer-setstring" "RefC:setBufferString" - "node:lambda:(buf,offset,value)=>buf.write(value, Number(offset),buf.length - Number(offset), 'utf-8')" + "node:lambda:(buf,offset,value)=>buf.write(value, offset,buf.length - offset, 'utf-8')" prim__setString : Buffer -> Int -> String -> PrimIO () export %inline @@ -210,7 +210,7 @@ setString buf loc val %foreign "scheme:blodwen-buffer-getstring" "RefC:getBufferString" - "node:lambda:(buf,offset,len)=>buf.slice(Number(offset), Number(offset+len)).toString('utf-8')" + "node:lambda:(buf,offset,len)=>buf.slice(offset, offset+len).toString('utf-8')" prim__getString : Buffer -> Int -> Int -> PrimIO String export %inline @@ -235,7 +235,7 @@ bufferData buf %foreign "scheme:blodwen-buffer-copydata" "RefC:copyBuffer" - "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,Number(o2), Number(o1), Number(o1+length))" + "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,o2,o1,o1+length)" prim__copyData : Buffer -> Int -> Int -> Buffer -> Int -> PrimIO () export @@ -246,12 +246,12 @@ copyData src start len dest loc %foreign "C:idris2_readBufferData, libidris2_support, idris_file.h" "RefC:readBufferData" - "node:lambda:(f,b,l,m) => BigInt(require('fs').readSync(f.fd,b,Number(l), Number(m)))" + "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)" prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int %foreign "C:idris2_writeBufferData, libidris2_support, idris_file.h" "RefC:writeBufferData" - "node:lambda:(f,b,l,m) => BigInt(require('fs').writeSync(f.fd,b,Number(l), Number(m)))" + "node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)" prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int export diff --git a/libs/base/System.idr b/libs/base/System.idr index beaf31324..02c209adf 100644 --- a/libs/base/System.idr +++ b/libs/base/System.idr @@ -34,13 +34,13 @@ usleep sec = primIO (prim__usleep sec) -- Get the number of arguments %foreign "scheme:blodwen-arg-count" support "idris2_getArgCount" - "node:lambda:() => BigInt(process.argv.length)" + "node:lambda:() => process.argv.length" prim__getArgCount : PrimIO Int -- Get argument number `n` %foreign "scheme:blodwen-arg" support "idris2_getArg" - "node:lambda:n => process.argv[(Number(n))]" + "node:lambda:n => process.argv[n]" prim__getArg : Int -> PrimIO String export @@ -124,7 +124,7 @@ getPID : HasIO io => io Int getPID = primIO prim__getPID %foreign libc "exit" - "node:lambda:c => process.exit(Number(c))" + "node:lambda:c => process.exit(c)" prim__exit : Int -> PrimIO () ||| Programs can either terminate successfully, or end in a caught diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index 9f50f3990..f6c228c7b 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -27,7 +27,7 @@ prim__open : String -> String -> PrimIO FilePtr prim__close : FilePtr -> PrimIO () %foreign support "idris2_fileError" - "node:lambda:x=>(x===1n?BigInt(1):BigInt(0))" + "node:lambda:x=>(x===1?1:0)" prim__error : FilePtr -> PrimIO Int %foreign support "idris2_fileErrno" @@ -52,7 +52,7 @@ prim__readChar : FilePtr -> PrimIO Int prim__writeLine : FilePtr -> String -> PrimIO Int %foreign support "idris2_eof" - "node:lambda:x=>(x.eof?1n:0n)" + "node:lambda:x=>(x.eof?1:0)" prim__eof : FilePtr -> PrimIO Int %foreign "C:fflush,libc 6" @@ -66,7 +66,7 @@ prim__pclose : FilePtr -> PrimIO () prim__removeFile : String -> PrimIO Int %foreign support "idris2_fileSize" - "node:lambda:fp=>require('fs').fstatSync(fp.fd, {bigint: true}).size" + "node:lambda:fp=>require('fs').fstatSync(fp.fd).size" prim__fileSize : FilePtr -> PrimIO Int %foreign support "idris2_fileSize" @@ -76,7 +76,7 @@ prim__fPoll : FilePtr -> PrimIO Int prim__fileAccessTime : FilePtr -> PrimIO Int %foreign support "idris2_fileModifiedTime" - "node:lambda:fp=>require('fs').fstatSync(fp.fd, {bigint: true}).mtimeMs / 1000n" + "node:lambda:fp=>require('fs').fstatSync(fp.fd).mtimeMs / 1000" prim__fileModifiedTime : FilePtr -> PrimIO Int %foreign support "idris2_fileStatusTime" diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr index 4ca07ee15..4dd2bbbff 100644 --- a/libs/prelude/PrimIO.idr +++ b/libs/prelude/PrimIO.idr @@ -73,7 +73,7 @@ toPrim : (1 act : IO a) -> PrimIO a toPrim (MkIO fn) = fn %foreign "C:idris2_isNull, libidris2_support, idris_support.h" - "javascript:lambda:x=>x===undefined||x===null?1n:0n" + "javascript:lambda:x=>x===undefined||x===null?1:0" export prim__nullAnyPtr : AnyPtr -> Int diff --git a/src/Compiler/ES/Ast.idr b/src/Compiler/ES/Ast.idr new file mode 100644 index 000000000..9413263b2 --- /dev/null +++ b/src/Compiler/ES/Ast.idr @@ -0,0 +1,195 @@ +module Compiler.ES.Ast + +import Core.CompileExpr +import Core.Context +import Compiler.Common +import Data.List1 +import Data.Nat +import Data.Vect + +%default total + +||| A variable in a toplevel function definition +||| +||| When generating the syntax tree of imperative +||| statements and expressions, we decide - based on +||| codegen directives - which Idris names to keep +||| and which names to convert to short, mangled +||| versions. +public export +data Var = + ||| An unaltered name - usually a toplevel function + ||| or a function argument with an explicitly given + ||| name + VName Name | + + ||| Index of a local variables + VLoc Int | + + ||| Index of a mangled toplevel function + VRef Int + +||| A minimal expression. +public export +data Minimal = + ||| A variable + MVar Var | + + ||| A projection targeting the field of a data type. + ||| We include these here since it allows us to + ||| conveniently carry around a `SortedMap Name Minimal` + ||| for name resolution during the generation of the + ||| imperative syntax tree. + MProjection Nat Minimal + +-------------------------------------------------------------------------------- +-- Expressions +-------------------------------------------------------------------------------- + +||| The effect of a statement or a block of statements. +||| `Returns` means the +||| result of the final expression will be returned as +||| the current function's result, while `ErrorWithout v` +||| is a reminder, that the block of code will eventually +||| assign a value to `v` and will fail to do so if +||| `v` hasn't previously been declared. +||| +||| This is used as a typelevel index to prevent us from +||| making some common stupid errors like declaring a variable +||| twice, or having several `return` statements in the same +||| block of code. +public export +data Effect = Returns | ErrorWithout Var + +mutual + ||| An expression in a function definition. + public export + data Exp : Type where + ||| A variable or projection. Minimal expressions + ||| will always be inlined unless explicitly bound + ||| in an Idris2 `let` expression. + EMinimal : Minimal -> Exp + + ||| Lambda expression + ||| + ||| An empty argument list represents a delayed computation + ELam : List Var -> Stmt (Just Returns) -> Exp + + ||| Function application. + ||| + ||| In case of a zero-argument list, we might also be + ||| dealing with forcing a delayed computation. + EApp : Exp -> List Exp -> Exp + + ||| Saturated construtor application. + ||| + ||| The tag either represents the name of a type constructor + ||| (when we are pattern matching on types) or the index + ||| of a data constructor. + ECon : (tag : Either Int Name) -> ConInfo -> List Exp -> Exp + + ||| Primitive operation + EOp : {0 arity : Nat} -> PrimFn arity -> Vect arity Exp -> Exp + + ||| Externally defined primitive operation. + EExtPrim : Name -> List Exp -> Exp + + ||| A constant primitive. + EPrimVal : Constant -> Exp + + ||| An erased value. + EErased : Exp + + ||| An imperative statement in a function definition. + ||| + ||| This is indexed over the `Effect` the statement, + ||| will have. + ||| An `effect` of `Nothing` means that the result of + ||| the statement is `undefined`: The declaration of + ||| a constant or assignment of a previously declared + ||| variable. When we sequence statements in a block + ||| of code, all but the last one of them must have + ||| effect `Nothing`. This makes sure we properly declare variables + ||| exactly once before eventually assigning them. + ||| It makes also sure a block of code does not contain + ||| several `return` statements (until they are the + ||| results of the branches of a `switch` statement). + public export + data Stmt : (effect : Maybe Effect) -> Type where + ||| Returns the result of the given expression. + Return : Exp -> Stmt (Just Returns) + + ||| Introduces a new constant by assigning the result + ||| of a single expression to the given variable. + Const : (v : Var) -> Exp -> Stmt Nothing + + ||| Assigns the result of an expression to the given variable. + ||| This will result in an error, if the variable has not + ||| yet been declared. + Assign : (v : Var) -> Exp -> Stmt (Just $ ErrorWithout v) + + ||| Declares (but does not yet assign) a new mutable + ||| variable. This is the only way to "saturate" + ||| a `Stmt (Just $ ErrorWithout v)`. + Declare : (v : Var) -> Stmt (Just $ ErrorWithout v) -> Stmt Nothing + + ||| Switch statement from a pattern match on + ||| data or type constructors. The result of each branch + ||| will have the given `Effect`. + ||| + ||| The scrutinee has already been lifted to + ||| the outer scope to make sure it is only + ||| evaluated once. + ConSwitch : (e : Effect) + -> (scrutinee : Minimal) + -> (alts : List $ EConAlt e) + -> (def : Maybe $ Stmt $ Just e) + -> Stmt (Just e) + + ||| Switch statement from a pattern on + ||| a constant. The result of each branch + ||| will have the given `Effect`. + ConstSwitch : (e : Effect) + -> (scrutinee : Exp) + -> (alts : List $ EConstAlt e) + -> (def : Maybe $ Stmt $ Just e) + -> Stmt (Just e) + + ||| A runtime exception. + Error : {0 any : _} -> String -> Stmt (Just any) + + ||| A code block consisting of one or more + ||| imperative statements. + Block : List1 (Stmt Nothing) -> Stmt e -> Stmt e + + ||| Single branch in a pattern match on a data or + ||| type constructor. + public export + record EConAlt (e : Effect) where + constructor MkEConAlt + tag : Either Int Name + conInfo : ConInfo + body : Stmt (Just e) + + ||| Single branch in a pattern match on a constant + public export + record EConstAlt (e : Effect) where + constructor MkEConstAlt + constant : Constant + body : Stmt (Just e) + +export +toMinimal : Exp -> Maybe Minimal +toMinimal (EMinimal v) = Just v +toMinimal _ = Nothing + +export +prepend : List (Stmt Nothing) -> Stmt (Just e) -> Stmt (Just e) +prepend [] s = s +prepend (h :: t) s = Block (h ::: t) s + +export total +declare : {v : _} -> Stmt (Just $ ErrorWithout v) -> Stmt Nothing +declare (Assign v y) = Const v y +declare (Block ss s) = Block ss $ declare s +declare s = Declare v s diff --git a/src/Compiler/ES/Codegen.idr b/src/Compiler/ES/Codegen.idr new file mode 100644 index 000000000..f9ab9a78c --- /dev/null +++ b/src/Compiler/ES/Codegen.idr @@ -0,0 +1,725 @@ +module Compiler.ES.Codegen + +import Compiler.Common +import Core.CompileExpr +import Core.Context +import Core.Directory +import Core.Options +import Data.List1 +import Data.String +import Compiler.ES.Ast +import Compiler.ES.Doc +import Compiler.ES.ToAst +import Compiler.ES.TailRec +import Compiler.ES.State +import Libraries.Data.SortedMap +import Libraries.Utils.Hex +import Libraries.Data.String.Extra + +import Data.Vect + +-------------------------------------------------------------------------------- +-- Utilities +-------------------------------------------------------------------------------- + +-- Split at the given character and remove it. +breakDrop1 : Char -> String -> (String, String) +breakDrop1 c = mapSnd (drop 1) . break (== c) + +-- Display a quoted list of strings. +stringList : List String -> String +stringList = fastConcat . intersperse "," . map show + +-------------------------------------------------------------------------------- +-- JS Strings +-------------------------------------------------------------------------------- + +-- Convert an Idris2 string to a Javascript String +-- by escaping most non-alphanumeric characters. +jsString : String -> String +jsString s = "'" ++ (concatMap okchar (unpack s)) ++ "'" + where + okchar : Char -> String + okchar c = if (c >= ' ') && (c /= '\\') + && (c /= '"') && (c /= '\'') && (c <= '~') + then cast c + else case c of + '\0' => "\\0" + '\'' => "\\'" + '"' => "\\\"" + '\r' => "\\r" + '\n' => "\\n" + other => "\\u{" ++ asHex (cast {to=Int} c) ++ "}" + +||| Alias for Text . jsString +jsStringDoc : String -> Doc +jsStringDoc = Text . jsString + +-- A name from the preamble (file `support.js`). +-- the given string is just prefixed with an underscore. +esName : String -> String +esName x = "_" ++ x + +-- convert a string to a Javascript identifier +-- by escaping non-alphanumeric characters (except underscores). +jsIdent : String -> String +jsIdent s = concatMap okchar (unpack s) + where + okchar : Char -> String + okchar '_' = "_" + okchar c = if isAlphaNum c + then cast c + else "x" ++ the (String) (asHex (cast {to=Int} c)) + +keywordSafe : String -> String +keywordSafe "var" = "var$" +keywordSafe "switch" = "switch$" +keywordSafe "return" = "return$" +keywordSafe "const" = "const$" +keywordSafe "function" = "function$" +keywordSafe s = s + +-------------------------------------------------------------------------------- +-- JS Name +-------------------------------------------------------------------------------- + +jsName : Name -> String +jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n +jsName (UN n) = keywordSafe $ jsIdent n +jsName (MN n i) = jsIdent n ++ "_" ++ show i +jsName (PV n d) = "pat__" ++ jsName n +jsName (DN _ n) = jsName n +jsName (RF n) = "rf__" ++ jsIdent n +jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n +jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y +jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y +jsName (Resolved i) = "fn__" ++ show i + +jsNameDoc : Name -> Doc +jsNameDoc = Text . jsName + +mainExpr : Name +mainExpr = MN "__mainExpression" 0 + +-------------------------------------------------------------------------------- +-- Pretty Printing +-------------------------------------------------------------------------------- + +var : Var -> Doc +var (VName x) = jsNameDoc x +var (VLoc x) = Text $ "$" ++ asHex x +var (VRef x) = Text $ "$R" ++ asHex x + +minimal : Minimal -> Doc +minimal (MVar v) = var v +minimal (MProjection n v) = minimal v <+> ".a" <+> shown n + +tag2es : Either Int Name -> Doc +tag2es (Left x) = shown x +tag2es (Right x) = jsStringDoc $ show x + +constant : Doc -> Doc -> Doc +constant n d = "const" <++> n <+> softEq <+> d <+> ";" + +applyList : (lparen : Doc) -> (rparen : Doc) -> (sep : Doc) -> List Doc -> Doc +applyList l r sep ds = l <+> (concat $ intersperse sep ds) <+> r + +conTags : List Doc -> List Doc +conTags as = zipWith (\i,a => hcat ["a",shown i,softColon,a]) [1..length as] as + +applyObj : (args : List Doc) -> Doc +applyObj = applyList "{" "}" softComma + +-- fully applied constructors are converted to JS objects with fields +-- labeled `a1`, `a2`, and so on for the given list of arguments. +-- a header field (label: `h`) is added holding either the index of +-- the data constructor used or a string representing the type constructor +-- in question. +-- +-- Exceptions based on the given `ConInfo`: +-- `NIL` and `NOTHING`-like data constructors are represented as `{h: 0}`, +-- while `CONS`, `JUST`, and `RECORD` come without the header field. +applyCon : ConInfo -> (tag : Either Int Name) -> (args : List Doc) -> Doc +applyCon NIL _ [] = "{h" <+> softColon <+> "0}" +applyCon NOTHING _ [] = "{h" <+> softColon <+> "0}" +applyCon CONS _ as = applyObj (conTags as) +applyCon JUST _ as = applyObj (conTags as) +applyCon RECORD _ as = applyObj (conTags as) +applyCon _ t as = applyObj (("h" <+> softColon <+> tag2es t)::conTags as) + +-- applys the given list of arguments to the given function. +app : (fun : Doc) -> (args : List Doc) -> Doc +app fun args = fun <+> applyList "(" ")" softComma args + +-- invoke a function whose name is given as a `String` instead +-- of a `Doc`. +callFun : String -> List Doc -> Doc +callFun = app . Text + +-- like `callFun` but with just a single argument +callFun1 : String -> Doc -> Doc +callFun1 fun = callFun fun . pure + +-- throws an error in JS land with the given error message. +jsCrashExp : (msg : Doc) -> Doc +jsCrashExp = callFun1 (esName "crashExp") + +-- creates a toplevel function definition of the form +-- ```javascript +-- function name(args) { +-- body +-- } +function : (name : Doc) -> (args : List Doc) -> (body : Doc) -> Doc +function n args body = + "function" <++> app n args <+> SoftSpace <+> block body + +-------------------------------------------------------------------------------- +-- Primitives +-------------------------------------------------------------------------------- + +toBigInt : Doc -> Doc +toBigInt = callFun1 "BigInt" + +fromBigInt : Doc -> Doc +fromBigInt = callFun1 "Number" + +-- we need to use `BigInt` in JS if an integral type's +-- bit size is greater than 32. +useBigInt' : Int -> Bool +useBigInt' = (> 32) + +-- same as `useBigInt'` but based on `IntKind` +useBigInt : IntKind -> Bool +useBigInt (Signed $ P x) = useBigInt' x +useBigInt (Signed Unlimited) = True +useBigInt (Unsigned x) = useBigInt' x + +-- call _bigIntOfString from the preamble, which +-- converts a string to a `BigInt` +jsBigIntOfString : Doc -> Doc +jsBigIntOfString = callFun1 (esName "bigIntOfString") + +-- call _parseFloat from the preamble, which +-- converts a string to a `Number` +jsNumberOfString : Doc -> Doc +jsNumberOfString = callFun1 "parseFloat" + +-- convert an string to an integral type based +-- on its `IntKind`. +jsIntOfString : IntKind -> Doc -> Doc +jsIntOfString k = if useBigInt k then jsBigIntOfString else jsNumberOfString + +-- introduce a binary infix operation +binOp : (symbol : String) -> (lhs : Doc) -> (rhs : Doc) -> Doc +binOp sym lhs rhs = hcat ["(", lhs, Text sym, rhs, ")"] + +-- converts a `Number` to an integer +-- based on the given precision (`IntKind`). +toInt : IntKind -> Doc -> Doc +toInt k = if useBigInt k then toBigInt else id + +-- converts an integer to a `Number` +-- based on the given precision (`IntKind`). +fromInt : IntKind -> Doc -> Doc +fromInt k = if useBigInt k then fromBigInt else id + +-- converts a character (in JS, a string of length 1) +-- to an integer. +jsIntOfChar : IntKind -> Doc -> Doc +jsIntOfChar k s = toInt k $ s <+> ".codePointAt(0)" + +-- converts a floating point number to an integer. +jsIntOfDouble : IntKind -> Doc -> Doc +jsIntOfDouble k = toInt k . callFun1 "Math.trunc" + +jsAnyToString : Doc -> Doc +jsAnyToString s = "(''+" <+> s <+> ")" + +-- converts an integer (`Number` or `BigInt`) to a character +-- by calling `_truncToChar` from the preamble. +jsCharOfInt : IntKind -> Doc -> Doc +jsCharOfInt k = callFun1 (esName "truncToChar") . fromInt k + +-- Invokes a function from the preamble to check if an bounded +-- signed integer is within bounds, and - if that's not the case - +-- truncate it accordingly. +-- `isBigInt` reflects whether `int` is a `BigInt` or a `Number`. +-- +-- Note: We can't determine `isBigInt` from the given number of bits, since +-- when casting from BigInt (for instance, a `Bits64`) to Number +-- we need to truncate the BigInt +-- first, otherwise we might lose precision. +truncateSigned : (isBigInt : Bool) -> (bits : Int) -> (int : Doc) -> Doc +truncateSigned isBigInt bits = + let add = if isBigInt then "BigInt" else "Int" + in callFun1 (esName "trunc" ++ add ++ show bits) + +-- like `truncateSigned` but for unsigned integers +truncateUnsigned : (isBigInt : Bool) -> (bits : Int) -> (int : Doc) -> Doc +truncateUnsigned isBigInt bits = + let add = if isBigInt then "BigInt" else "Int" + in callFun1 (esName "truncU" ++ add ++ show bits) + +-- invokes an arithmetic operation for a bounded integral value. +-- this is used to implement `boundedIntOp` and `boundedUIntOp` +-- where the suffix is set to "s" or "u", respectively. +boundedOp : (suffix : String) + -> (bits : Int) + -> (op : String) + -> (lhs : Doc) + -> (rhs : Doc) + -> Doc +boundedOp s bits o x y = callFun (fastConcat ["_", o, show bits, s]) [x,y] + +-- alias for `boundedOp "s"` +boundedIntOp : Int -> String -> Doc -> Doc -> Doc +boundedIntOp = boundedOp "s" + +-- alias for `boundedOp "u"` +boundedUIntOp : Int -> String -> Doc -> Doc -> Doc +boundedUIntOp = boundedOp "u" + +-- generates code for a boolean binop, like `>=`. +boolOp : (op : String) -> (lhs : Doc) -> (rhs : Doc) -> Doc +boolOp o lhs rhs = "(" <+> binOp o lhs rhs <+> "?1:0)" + +-- convert an Idris constant to its JS representation +jsConstant : Constant -> String +jsConstant (I i) = show i +jsConstant (I8 i) = show i +jsConstant (I16 i) = show i +jsConstant (I32 i) = show i +jsConstant (I64 i) = show i ++ "n" +jsConstant (BI i) = show i ++ "n" +jsConstant (Str s) = jsString s +jsConstant (Ch c) = jsString $ singleton c +jsConstant (Db f) = show f +jsConstant WorldVal = esName "idrisworld" +jsConstant (B8 i) = show i +jsConstant (B16 i) = show i +jsConstant (B32 i) = show i +jsConstant (B64 i) = show i ++ "n" +jsConstant IntType = "#t" +jsConstant Int8Type = "#t" +jsConstant Int16Type = "#t" +jsConstant Int32Type = "#t" +jsConstant Int64Type = "#t" +jsConstant IntegerType = "#t" +jsConstant Bits8Type = "#t" +jsConstant Bits16Type = "#t" +jsConstant Bits32Type = "#t" +jsConstant Bits64Type = "#t" +jsConstant StringType = "#t" +jsConstant CharType = "#t" +jsConstant DoubleType = "#t" +jsConstant WorldType = "#t" + +-- Creates the definition of a binary arithmetic operation. +-- Rounding / truncation behavior is determined from the +-- `IntKind`. +arithOp : Maybe IntKind + -> (sym : String) -- operator symbol (in case we can use the symbolic version) + -> (op : String) -- operation name (for operations on bounded integrals) + -> (lhs : Doc) + -> (rhs : Doc) + -> Doc +arithOp (Just $ Signed $ P n) _ op = boundedIntOp n op +arithOp (Just $ Unsigned n) _ op = boundedUIntOp n op +arithOp _ sym _ = binOp sym + +-- use 32bit signed integer for `Int`. +jsIntKind : Constant -> Maybe IntKind +jsIntKind IntType = Just . Signed $ P 32 +jsIntKind x = intKind x + +-- implementation of all kinds of cast from and / or to integral +-- values. +castInt : Constant -> Constant -> Doc -> Core Doc +castInt from to x = + case ((from, jsIntKind from), (to, jsIntKind to)) of + ((CharType,_), (_,Just k)) => truncInt (useBigInt k) k $ jsIntOfChar k x + ((StringType,_),(_,Just k)) => truncInt (useBigInt k) k (jsIntOfString k x) + ((DoubleType,_),(_,Just k)) => truncInt (useBigInt k) k $ jsIntOfDouble k x + ((_,Just k),(CharType,_)) => pure $ jsCharOfInt k x + ((_,Just k),(StringType,_)) => pure $ jsAnyToString x + ((_,Just k),(DoubleType,_)) => pure $ fromInt k x + ((_,Just k1),(_,Just k2)) => intImpl k1 k2 + _ => errorConcat $ ["invalid cast: + ",show from," + ' -> ' + ",show to] + where + truncInt : (isBigInt : Bool) -> IntKind -> Doc -> Core Doc + truncInt b (Signed Unlimited) = pure + truncInt b (Signed $ P n) = pure . truncateSigned b n + truncInt b (Unsigned n) = pure . truncateUnsigned b n + + shrink : IntKind -> IntKind -> Doc -> Doc + shrink k1 k2 = case (useBigInt k1, useBigInt k2) of + (True, False) => fromBigInt + _ => id + + expand : IntKind -> IntKind -> Doc -> Doc + expand k1 k2 = case (useBigInt k1, useBigInt k2) of + (False,True) => toBigInt + _ => id + + -- when going from BigInt to Number, we must make + -- sure to first truncate the BigInt, otherwise we + -- might get rounding issues + intImpl : IntKind -> IntKind -> Core Doc + intImpl k1 k2 = + let expanded = expand k1 k2 x + shrunk = shrink k1 k2 <$> truncInt (useBigInt k1) k2 x + in case (k1,k2) of + (_, Signed Unlimited) => pure $ expanded + (Signed m, Signed n) => + if n >= m then pure expanded else shrunk + + (Signed _, Unsigned n) => + case (useBigInt k1, useBigInt k2) of + (False,True) => truncInt True k2 (toBigInt x) + _ => shrunk + + (Unsigned m, Unsigned n) => + if n >= m then pure expanded else shrunk + + -- Only if the precision of the target is greater + -- than the one of the source, there is no need to cast. + (Unsigned m, Signed n) => + if n > P m then pure expanded else shrunk + +-- implementations of primitive functions. +jsOp : {0 arity : Nat} -> + PrimFn arity -> Vect arity Doc -> Core Doc +jsOp (Add ty) [x, y] = pure $ arithOp (jsIntKind ty) "+" "add" x y +jsOp (Sub ty) [x, y] = pure $ arithOp (jsIntKind ty) "-" "sub" x y +jsOp (Mul ty) [x, y] = pure $ arithOp (jsIntKind ty) "*" "mul" x y +jsOp (Div ty) [x, y] = pure $ arithOp (jsIntKind ty) "/" "div" x y +jsOp (Mod ty) [x, y] = pure $ binOp "%" x y +jsOp (Neg ty) [x] = pure $ "(-(" <+> x <+> "))" +jsOp (ShiftL Int32Type) [x, y] = pure $ binOp "<<" x y +jsOp (ShiftL IntType) [x, y] = pure $ binOp "<<" x y +jsOp (ShiftL ty) [x, y] = pure $ arithOp (jsIntKind ty) "<<" "shl" x y +jsOp (ShiftR Int32Type) [x, y] = pure $ binOp ">>" x y +jsOp (ShiftR IntType) [x, y] = pure $ binOp ">>" x y +jsOp (ShiftR ty) [x, y] = pure $ arithOp (jsIntKind ty) ">>" "shr" x y +jsOp (BAnd Bits32Type) [x, y] = pure $ boundedUIntOp 32 "and" x y +jsOp (BOr Bits32Type) [x, y] = pure $ boundedUIntOp 32 "or" x y +jsOp (BXOr Bits32Type) [x, y] = pure $ boundedUIntOp 32 "xor" x y +jsOp (BAnd ty) [x, y] = pure $ binOp "&" x y +jsOp (BOr ty) [x, y] = pure $ binOp "|" x y +jsOp (BXOr ty) [x, y] = pure $ binOp "^" x y +jsOp (LT ty) [x, y] = pure $ boolOp "<" x y +jsOp (LTE ty) [x, y] = pure $ boolOp "<=" x y +jsOp (EQ ty) [x, y] = pure $ boolOp "===" x y +jsOp (GTE ty) [x, y] = pure $ boolOp ">=" x y +jsOp (GT ty) [x, y] = pure $ boolOp ">" x y +jsOp StrLength [x] = pure $ x <+> ".length" +jsOp StrHead [x] = pure $ "(" <+> x <+> ".charAt(0))" +jsOp StrTail [x] = pure $ "(" <+> x <+> ".slice(1))" +jsOp StrIndex [x, y] = pure $ "(" <+> x <+> ".charAt(" <+> y <+> "))" +jsOp StrCons [x, y] = pure $ binOp "+" x y +jsOp StrAppend [x, y] = pure $ binOp "+" x y +jsOp StrReverse [x] = pure $ callFun1 (esName "strReverse") x +jsOp StrSubstr [offset, len, str] = + pure $ callFun (esName "substr") [offset,len,str] +jsOp DoubleExp [x] = pure $ callFun1 "Math.exp" x +jsOp DoubleLog [x] = pure $ callFun1 "Math.log" x +jsOp DoubleSin [x] = pure $ callFun1 "Math.sin" x +jsOp DoubleCos [x] = pure $ callFun1 "Math.cos" x +jsOp DoubleTan [x] = pure $ callFun1 "Math.tan" x +jsOp DoubleASin [x] = pure $ callFun1 "Math.asin" x +jsOp DoubleACos [x] = pure $ callFun1 "Math.acos" x +jsOp DoubleATan [x] = pure $ callFun1 "Math.atan" x +jsOp DoubleSqrt [x] = pure $ callFun1 "Math.sqrt" x +jsOp DoubleFloor [x] = pure $ callFun1 "Math.floor" x +jsOp DoubleCeiling [x] = pure $ callFun1 "Math.ceil" x + +jsOp (Cast StringType DoubleType) [x] = pure $ jsNumberOfString x +jsOp (Cast ty StringType) [x] = pure $ jsAnyToString x +jsOp (Cast ty ty2) [x] = castInt ty ty2 x +jsOp BelieveMe [_,_,x] = pure x +jsOp (Crash) [_, msg] = pure $ jsCrashExp msg + +-------------------------------------------------------------------------------- +-- FFI +-------------------------------------------------------------------------------- + +-- from an FFI declaration, reads the backend to use. +-- Example: `readCCPart "node:lambda: x => x"` yields +-- `("node","lambda: x => x")`. +readCCPart : String -> (String, String) +readCCPart = breakDrop1 ':' + +-- search a an FFI implementation for one of the supported +-- backends. +searchForeign : List String -> List String -> Either (List String) String +searchForeign knownBackends decls = + let pairs = map readCCPart decls + backends = Left $ map fst pairs + in maybe backends (Right. snd) $ find ((`elem` knownBackends) . fst) pairs + +-- given a function name and FFI implementation string, +-- generate a toplevel function definition. +makeForeign : {auto d : Ref Ctxt Defs} + -> {auto c : Ref ESs ESSt} + -> (name : Name) + -> (ffDecl : String) + -> Core Doc +makeForeign n x = do + nd <- var <$> getOrRegisterRef n + let (ty, def) = readCCPart x + case ty of + "lambda" => pure . constant nd . paren $ Text def + "support" => do + let (name, lib) = breakDrop1 ',' def + lib_code <- readDataFile ("js/" ++ lib ++ ".js") + addToPreamble lib lib_code + pure . constant nd . Text $ lib ++ "_" ++ name + "stringIterator" => + case def of + "new" => pure $ constant nd "__prim_stringIteratorNew" + "next" => pure $ constant nd "__prim_stringIteratorNext" + "toString" => pure $ constant nd "__prim_stringIteratorToString" + _ => errorConcat + [ "Invalid string iterator function: ", def, ". " + , "Supported functions are: " + , stringList ["new","next","toString"], "." + ] + + _ => errorConcat + [ "Invalid foreign type : ", ty, ". " + , "Supported types are: " + , stringList ["lambda", "support", "stringIterator"] + ] + +-- given a function name and list of FFI declarations, tries +-- to extract a declaration for one of the supported backends. +foreignDecl : {auto d : Ref Ctxt Defs} + -> {auto c : Ref ESs ESSt} + -> Name + -> List String + -> Core Doc +foreignDecl n ccs = do + tys <- ccTypes <$> get ESs + case searchForeign tys ccs of + Right x => makeForeign n x + Left backends => + errorConcat + [ "No supported backend found in the definition of ", show n, ". " + , "Supported backends: ", stringList tys, ". " + , "Backends in definition: ", stringList backends, "." + ] + +-- implementations for external primitive functions. +jsPrim : {auto c : Ref ESs ESSt} -> Name -> List Doc -> Core Doc +jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ hcat ["({value:", v, "})"] +jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ hcat ["(", r, ".value)"] +jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ hcat ["(", r, ".value=", v, ")"] +jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ hcat ["(Array(", s, ").fill(", v, "))"] +jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ hcat ["(", x, "[", p, "])"] +jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ hcat ["(", x, "[", p, "]=", v, ")"] +jsPrim (NS _ (UN "prim__os")) [] = pure $ Text $ esName "sysos" +jsPrim (NS _ (UN "void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" +jsPrim (NS _ (UN "prim__void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" +jsPrim (NS _ (UN "prim__codegen")) [] = do + (cg :: _) <- ccTypes <$> get ESs + | _ => pure "\"javascript\"" + pure . Text $ jsString cg +jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x) + +-------------------------------------------------------------------------------- +-- Codegen +-------------------------------------------------------------------------------- + +-- checks, whether we accept the given `Exp` as a function argument, or +-- whether it needs to be lifted to the surrounding scope and assigned +-- to a new variable. +isArg : CGMode -> Exp -> Bool +isArg Pretty (ELam _ $ Block _ _) = False +isArg Pretty (ELam _ $ ConSwitch _ _ _ _) = False +isArg Pretty (ELam _ $ ConstSwitch _ _ _ _) = False +isArg Pretty (ELam _ $ Error _) = False +isArg _ _ = True + +-- like `isArg` but for function expressions, which we are about +-- to apply +isFun : Exp -> Bool +isFun (ELam _ _) = False +isFun _ = True + +-- creates a JS switch statment from the given scrutinee and +-- case blocks (the first entry in a pair is the value belonging +-- to a `case` statement, the second is the body +-- +-- Example: switch "foo.a1" [("0","return 2;")] (Just "return 0;") +-- generates the following code: +-- ```javascript +-- switch(foo.a1) { +-- case 0: return 2; +-- default: return 0; +-- } +-- ``` +switch : (scrutinee : Doc) + -> (alts : List (Doc,Doc)) + -> (def : Maybe Doc) + -> Doc +switch sc alts def = + let stmt = "switch" <+> paren sc <+> SoftSpace + defcase = concatMap (pure . anyCase "default") def + in stmt <+> block (vcat $ map alt alts ++ defcase) + + where anyCase : Doc -> Doc -> Doc + anyCase s d = + let b = if isMultiline d then block d else d + in s <+> softColon <+> b + + alt : (Doc,Doc) -> Doc + alt (e,d) = anyCase ("case" <++> e) d + +-- creates an argument list for a (possibly multi-argument) +-- anonymous function. An empty argument list is treated +-- as a delayed computation (prefixed by `() =>`). +lambdaArgs : List Var -> Doc +lambdaArgs [] = "()" <+> lambdaArrow +lambdaArgs xs = hcat $ (<+> lambdaArrow) . var <$> xs + +mutual + -- converts an `Exp` to JS code + exp : {auto c : Ref ESs ESSt} -> Exp -> Core Doc + exp (EMinimal x) = pure $ minimal x + exp (ELam xs (Return $ y@(ECon _ _ _))) = + map (\e => lambdaArgs xs <+> paren e) (exp y) + exp (ELam xs (Return $ y)) = (lambdaArgs xs <+> ) <$> exp y + exp (ELam xs y) = (lambdaArgs xs <+>) . block <$> stmt y + exp (EApp x xs) = do + o <- exp x + args <- traverse exp xs + pure $ app o args + + exp (ECon tag ci xs) = applyCon ci tag <$> traverse exp xs + + exp (EOp x xs) = traverseVect exp xs >>= jsOp x + exp (EExtPrim x xs) = traverse exp xs >>= jsPrim x + exp (EPrimVal x) = pure . Text $ jsConstant x + exp EErased = pure "undefined" + + -- converts a `Stmt e` to JS code. + stmt : {e : _} -> {auto c : Ref ESs ESSt} -> Stmt e -> Core Doc + stmt (Return y) = (\e => "return" <++> e <+> ";") <$> exp y + stmt (Const v x) = constant (var v) <$> exp x + stmt (Declare v s) = + (\d => vcat ["let" <++> var v <+> ";",d]) <$> stmt s + stmt (Assign v x) = + (\d => vcat [hcat [var v,softEq,d,";"], "break;"]) <$> exp x + + stmt (ConSwitch r sc alts def) = do + as <- traverse alt alts + d <- traverseOpt stmt def + pure $ switch (minimal sc <+> ".h") as d + where alt : EConAlt r -> Core (Doc,Doc) + alt (MkEConAlt _ RECORD b) = ("undefined",) <$> stmt b + alt (MkEConAlt _ NIL b) = ("0",) <$> stmt b + alt (MkEConAlt _ CONS b) = ("undefined",) <$> stmt b + alt (MkEConAlt _ NOTHING b) = ("0",) <$> stmt b + alt (MkEConAlt _ JUST b) = ("undefined",) <$> stmt b + alt (MkEConAlt t _ b) = (tag2es t,) <$> stmt b + + stmt (ConstSwitch r sc alts def) = do + as <- traverse alt alts + d <- traverseOpt stmt def + ex <- exp sc + pure $ switch ex as d + where alt : EConstAlt r -> Core (Doc,Doc) + alt (MkEConstAlt c b) = do d <- stmt b + pure (Text $ jsConstant c, d) + + stmt (Error x) = pure $ jsCrashExp (jsStringDoc x) <+> ";" + stmt (Block ss s) = do + docs <- traverse stmt $ forget ss + doc <- stmt s + pure $ vcat (docs ++ [doc]) + +-- pretty print a piece of code based on the given +-- codegen mode. +printDoc : CGMode -> Doc -> String +printDoc Pretty y = pretty (y <+> LineBreak) +printDoc Compact y = compact y +printDoc Minimal y = compact y + +-- generate code for the given toplevel function. +def : {auto c : Ref ESs ESSt} -> Function -> Core String +def (MkFunction n as body) = do + reset + ref <- getOrRegisterRef n + args <- traverse registerLocal as + mde <- mode <$> get ESs + b <- stmt Returns body >>= stmt + pure $ printDoc mde $ function (var ref) (map var args) b + +-- generate code for the given foreign function definition +foreign : {auto c : Ref ESs ESSt} + -> {auto d : Ref Ctxt Defs} + -> (Name,FC,NamedDef) + -> Core (List String) +foreign (n, _, MkNmForeign path _ _) = pure . pretty <$> foreignDecl n path +foreign _ = pure [] + +-- name of the toplevel tail call loop from the +-- preamble. +tailRec : Name +tailRec = UN "__tailRec" + +||| Compiles the given `ClosedTerm` for the list of supported +||| backends to JS code. +export +compileToES : Ref Ctxt Defs -> (cg : CG) -> ClosedTerm -> List String -> Core String +compileToES c cg tm ccTypes = do + cdata <- getCompileData False Cases tm + + -- read a derive the codegen mode to use from + -- user defined directives for the + directives <- getDirectives cg + let mode = if "minimal" `elem` directives then Minimal + else if "compact" `elem` directives then Compact + else Pretty + + -- initialize the state used in the code generator + s <- newRef ESs $ init mode (isArg mode) isFun ccTypes + + -- register the toplevel `__tailRec` function to make sure + -- it is not mangled in `Minimal` mode + addRef tailRec (VName tailRec) + + -- the list of all toplevel definitions (including the main + -- function) + let allDefs = (mainExpr, EmptyFC, MkNmFun [] $ forget cdata.mainExpr) + :: cdata.namedDefs + + -- tail-call optimized set of toplevel functions + defs = TailRec.functions tailRec allDefs + + -- pretty printed toplevel function definitions + defDecls <- traverse def defs + + -- pretty printed toplevel FFI definitions + foreigns <- concat <$> traverse foreign allDefs + + -- lookup the (possibly mangled) name of the main function + mainName <- compact . var <$> getOrRegisterRef mainExpr + + -- main function and list of all declarations + let main = "try{" + ++ mainName + ++ "()}catch(e){if(e instanceof IdrisError){console.log('ERROR: ' + e.message)}else{throw e} }" + + allDecls = fastUnlines $ foreigns ++ defDecls + + st <- get ESs + + -- main preamble containing primops implementations + static_preamble <- readDataFile ("js/support.js") + + -- complete preamble, including content from additional + -- support files (if any) + let pre = showSep "\n" $ static_preamble :: (values $ preamble st) + + pure $ fastUnlines [pre,allDecls,main] diff --git a/src/Compiler/ES/Doc.idr b/src/Compiler/ES/Doc.idr new file mode 100644 index 000000000..2b2c0080c --- /dev/null +++ b/src/Compiler/ES/Doc.idr @@ -0,0 +1,106 @@ +module Compiler.ES.Doc + +import Data.List + +infixl 8 <++>, + +public export +data Doc + = Nil + | LineBreak + | SoftSpace -- this will be ignored in compact printing + | Text String + | Nest Nat Doc + | Seq Doc Doc + +export +Semigroup Doc where + Nil <+> y = y + x <+> Nil = x + x <+> y = Seq x y + +export +Monoid Doc where + neutral = Nil + +public export %inline +shown : Show a => a -> Doc +shown a = Text (show a) + +export +FromString Doc where + fromString = Text + +export +isMultiline : Doc -> Bool +isMultiline [] = False +isMultiline LineBreak = True +isMultiline SoftSpace = False +isMultiline (Text x) = False +isMultiline (Nest k x) = isMultiline x +isMultiline (Seq x y) = isMultiline x || isMultiline y + +export +(<++>) : Doc -> Doc -> Doc +a <++> b = a <+> " " <+> b + +export +vcat : List Doc -> Doc +vcat = concat . intersperse LineBreak + +export +hcat : List Doc -> Doc +hcat = concat + +export +hsep : List Doc -> Doc +hsep = concat . intersperse " " + +export +block : Doc -> Doc +block b = concat ["{", Nest 1 (LineBreak <+> b), LineBreak, "}"] + +export +paren : Doc -> Doc +paren d = "(" <+> d <+> ")" + +export +lambdaArrow : Doc +lambdaArrow = SoftSpace <+> "=>" <+> SoftSpace + +export +softComma : Doc +softComma = "," <+> SoftSpace + +export +softColon : Doc +softColon = ":" <+> SoftSpace + +export +softEq : Doc +softEq = SoftSpace <+> "=" <+> SoftSpace + +export +compact : Doc -> String +compact = fastConcat . go + where go : Doc -> List String + go Nil = [] + go LineBreak = [] + go SoftSpace = [] + go (Text x) = [x] + go (Nest _ y) = go y + go (Seq x y) = go x ++ go y + +export +pretty : Doc -> String +pretty = fastConcat . go "" + where nSpaces : Nat -> String + nSpaces n = fastPack $ replicate n ' ' + + go : (spaces : String) -> Doc -> List String + go _ Nil = [] + go s LineBreak = ["\n",s] + go _ SoftSpace = [" "] + go _ (Text x) = [x] + go s (Nest x y) = go (s ++ nSpaces x) y + go s (Seq x y) = go s x ++ go s y diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr deleted file mode 100644 index 309c0b900..000000000 --- a/src/Compiler/ES/ES.idr +++ /dev/null @@ -1,577 +0,0 @@ -module Compiler.ES.ES - -import Compiler.Common -import Compiler.ES.Imperative -import Libraries.Utils.Hex -import Data.List1 -import Data.String -import Libraries.Data.SortedMap -import Libraries.Data.String.Extra - -import Core.Directory - -%default covering - -%hide Data.String.lines -%hide Data.String.lines' -%hide Data.String.unlines -%hide Data.String.unlines' - -data ESs : Type where - -record ESSt where - constructor MkESSt - preamble : SortedMap String String - ccTypes : List String - -jsString : String -> String -jsString s = "'" ++ (concatMap okchar (unpack s)) ++ "'" - where - okchar : Char -> String - okchar c = if (c >= ' ') && (c /= '\\') - && (c /= '"') && (c /= '\'') && (c <= '~') - then cast c - else case c of - '\0' => "\\0" - '\'' => "\\'" - '"' => "\\\"" - '\r' => "\\r" - '\n' => "\\n" - other => "\\u{" ++ asHex (cast {to=Int} c) ++ "}" - -esName : String -> String -esName x = "__esPrim_" ++ x - - -addToPreamble : {auto c : Ref ESs ESSt} -> - String -> String -> String -> Core String -addToPreamble name newName def = - do - s <- get ESs - case lookup name (preamble s) of - Nothing => - do - put ESs (record { preamble = insert name def (preamble s) } s) - pure newName - Just x => - if x /= def - then throw $ InternalError $ "two incompatible definitions for " - ++ name ++ "<|" ++ x ++"|> <|"++ def ++ "|>" - else pure newName - -addConstToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String -addConstToPreamble name def = - do - let newName = esName name - let v = "const " ++ newName ++ " = (" ++ def ++ ");" - addToPreamble name newName v - -addSupportToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String -addSupportToPreamble name code = - addToPreamble name name code - -addStringIteratorToPreamble : {auto c : Ref ESs ESSt} -> Core String -addStringIteratorToPreamble = - do - let defs = unlines $ - [ "function __prim_stringIteratorNew(str) {" - , " return 0;" - , "}" - , "function __prim_stringIteratorToString(_, str, it, f) {" - , " return f(str.slice(it));" - , "}" - , "function __prim_stringIteratorNext(str, it) {" - , " if (it >= str.length)" - , " return {h: 0};" - , " else" - , " return {h: 1, a1: str.charAt(it), a2: it + 1};" - , "}" - ] - let name = "stringIterator" - let newName = esName name - addToPreamble name newName defs - - -jsIdent : String -> String -jsIdent s = concatMap okchar (unpack s) - where - okchar : Char -> String - okchar '_' = "_" - okchar c = if isAlphaNum c - then cast c - else "$" ++ (asHex (cast {to=Int} c)) - -keywordSafe : String -> String -keywordSafe "var" = "var_" -keywordSafe s = s - -jsName : Name -> String -jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n -jsName (UN n) = keywordSafe $ jsIdent n -jsName (MN n i) = jsIdent n ++ "_" ++ show i -jsName (PV n d) = "pat__" ++ jsName n -jsName (DN _ n) = jsName n -jsName (RF n) = "rf__" ++ jsIdent n -jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n -jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y -jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y -jsName (Resolved i) = "fn__" ++ show i - -jsCrashExp : {auto c : Ref ESs ESSt} -> String -> Core String -jsCrashExp message = - do - n <- addConstToPreamble "crashExp" "x=>{throw new IdrisError(x)}" - pure $ n ++ "("++ message ++ ")" - -toBigInt : String -> String -toBigInt e = "BigInt(" ++ e ++ ")" - -fromBigInt : String -> String -fromBigInt e = "Number(" ++ e ++ ")" - -useBigInt' : Int -> Bool -useBigInt' = (> 32) - -useBigInt : IntKind -> Bool -useBigInt (Signed $ P x) = useBigInt' x -useBigInt (Signed Unlimited) = True -useBigInt (Unsigned x) = useBigInt' x - -jsBigIntOfString : {auto c : Ref ESs ESSt} -> String -> Core String -jsBigIntOfString x = - do - n <- addConstToPreamble "bigIntOfString" "s=>{const idx = s.indexOf('.'); return idx === -1 ? BigInt(s) : BigInt(s.slice(0, idx));}" - pure $ n ++ "(" ++ x ++ ")" - -jsNumberOfString : {auto c : Ref ESs ESSt} -> String -> Core String -jsNumberOfString x = pure $ "parseFloat(" ++ x ++ ")" - -jsIntOfString : {auto c : Ref ESs ESSt} -> IntKind -> String -> Core String -jsIntOfString k = if useBigInt k then jsBigIntOfString else jsNumberOfString - -nSpaces : Nat -> String -nSpaces n = pack $ List.replicate n ' ' - -binOp : String -> String -> String -> String -binOp o lhs rhs = "(" ++ lhs ++ " " ++ o ++ " " ++ rhs ++ ")" - -adjInt : Int -> String -> String -adjInt bits = if useBigInt' bits then toBigInt else id - -toInt : IntKind -> String -> String -toInt k = if useBigInt k then toBigInt else id - -fromInt : IntKind -> String -> String -fromInt k = if useBigInt k then fromBigInt else id - -jsIntOfChar : IntKind -> String -> String -jsIntOfChar k s = toInt k $ s ++ ".codePointAt(0)" - -jsIntOfDouble : IntKind -> String -> String -jsIntOfDouble k s = toInt k $ "Math.trunc(" ++ s ++ ")" - -jsAnyToString : String -> String -jsAnyToString s = "(''+" ++ s ++ ")" - --- Valid unicode code poing range is [0,1114111], therefore, --- we calculate the remainder modulo 1114112 (= 17 * 2^16). -jsCharOfInt : {auto c : Ref ESs ESSt} -> IntKind -> String -> Core String -jsCharOfInt k e = - do fn <- addConstToPreamble - ("truncToChar") - ("x=>(x >= 0 && x <= 55295) || (x >= 57344 && x <= 1114111) ? x : 0") - pure $ "String.fromCodePoint(" ++ fn ++ "(" ++ fromInt k e ++ "))" - -makeIntBound : {auto c : Ref ESs ESSt} -> - (isBigInt : Bool) -> Int -> Core String -makeIntBound isBigInt bits = - let f = if isBigInt then toBigInt else id - name = if isBigInt then "bigint_bound_" else "int_bound_" - in addConstToPreamble (name ++ show bits) (f "2" ++ " ** "++ f (show bits)) - -boundedInt : {auto c : Ref ESs ESSt} - -> (isBigInt : Bool) - -> Int - -> String - -> Core String -boundedInt useBigInt bits e = - let bs = show bits - f = if useBigInt then toBigInt else id - name = if useBigInt then "truncToBigInt" else "truncToInt" - in do max <- makeIntBound useBigInt bits - half <- makeIntBound useBigInt (bits - 1) - fn <- addConstToPreamble - (name ++ show bits) - ( concat {t = List} - [ "x=>{ const v = x<",f "0","?x%",max,"+",max,":x%",max,";" - , "return v>=",half,"?","v-",max,":v}" - ]) - pure $ fn ++ "(" ++ e ++ ")" - -boundedUInt : {auto c : Ref ESs ESSt} -> - (isBigInt : Bool) -> Int -> String -> Core String -boundedUInt isBigInt bits e = - let name = if isBigInt then "truncToUBigInt" else "truncToUInt" - in do n <- makeIntBound isBigInt bits - fn <- addConstToPreamble - (name ++ show bits) - ("x=>{const m = x%" ++ n ++ ";return m>=0?m:m+" ++ n ++ "}") - pure $ fn ++ "(" ++ e ++ ")" - -boundedIntOp : {auto c : Ref ESs ESSt} -> - Int -> String -> String -> String -> Core String -boundedIntOp bits o lhs rhs = - boundedInt (useBigInt' bits) bits (binOp o lhs rhs) - -boundedUIntOp : {auto c : Ref ESs ESSt} -> - Int -> String -> String -> String -> Core String -boundedUIntOp bits o lhs rhs = - boundedUInt (useBigInt' bits) bits (binOp o lhs rhs) - -boolOp : String -> String -> String -> String -boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? BigInt(1) : BigInt(0))" - -jsConstant : {auto c : Ref ESs ESSt} -> Constant -> Core String -jsConstant (I i) = pure $ show i ++ "n" -jsConstant (I8 i) = pure $ show i -jsConstant (I16 i) = pure $ show i -jsConstant (I32 i) = pure $ show i -jsConstant (I64 i) = pure $ show i ++ "n" -jsConstant (BI i) = pure $ show i ++ "n" -jsConstant (Str s) = pure $ jsString s -jsConstant (Ch c) = pure $ jsString $ Data.String.singleton c -jsConstant (Db f) = pure $ show f -jsConstant WorldVal = addConstToPreamble "idrisworld" "Symbol('idrisworld')"; -jsConstant (B8 i) = pure $ show i -jsConstant (B16 i) = pure $ show i -jsConstant (B32 i) = pure $ show i -jsConstant (B64 i) = pure $ show i ++ "n" -jsConstant ty = throw (InternalError $ "Unsuported constant " ++ show ty) - --- For multiplication of 32bit integers (signed or unsigned), --- we go via BigInt and back, otherwise the calculation is --- susceptible to rounding error, since we might exceed `MAX_SAFE_INTEGER`. -mult : {auto c : Ref ESs ESSt} - -> Maybe IntKind - -> (x : String) - -> (y : String) - -> Core String -mult (Just $ Signed $ P 32) x y = - fromBigInt <$> boundedInt True 32 (binOp "*" (toBigInt x) (toBigInt y)) - -mult (Just $ Unsigned 32) x y = - fromBigInt <$> boundedUInt True 32 (binOp "*" (toBigInt x) (toBigInt y)) - -mult (Just $ Signed $ P n) x y = boundedIntOp n "*" x y -mult (Just $ Unsigned n) x y = boundedUIntOp n "*" x y -mult _ x y = pure $ binOp "*" x y - -div : {auto c : Ref ESs ESSt} - -> Maybe IntKind - -> (x : String) - -> (y : String) - -> Core String -div (Just $ Signed $ Unlimited) x y = pure $ binOp "/" x y -div (Just $ k@(Signed $ P n)) x y = - if useBigInt k then boundedIntOp n "/" x y - else boundedInt False n (jsIntOfDouble k (x ++ " / " ++ y)) -div (Just $ k@(Unsigned n)) x y = - if useBigInt k then pure $ binOp "/" x y - else pure $ jsIntOfDouble k (x ++ " / " ++ y) -div Nothing x y = pure $ binOp "/" x y - --- Creates the definition of a binary arithmetic operation. --- Rounding / truncation behavior is determined from the --- `IntKind`. -arithOp : {auto c : Ref ESs ESSt} - -> Maybe IntKind - -> (op : String) - -> (x : String) - -> (y : String) - -> Core String -arithOp (Just $ Signed $ P n) op x y = boundedIntOp n op x y -arithOp (Just $ Unsigned n) op x y = boundedUIntOp n op x y -arithOp _ op x y = pure $ binOp op x y - --- Same as `arithOp` but for bitwise operations that might --- go out of the valid range. --- Note: Bitwise operations on `Number` work correctly for --- 32bit *signed* integers. For `Bits32` we therefore go via `BigInt` --- in order not having to deal with all kinds of negativity nastiness. -bitOp : {auto c : Ref ESs ESSt} - -> Maybe IntKind - -> (op : String) - -> (x : String) - -> (y : String) - -> Core String -bitOp (Just $ Signed $ P n) op x y = boundedIntOp n op x y -bitOp (Just $ Unsigned 32) op x y = - fromBigInt <$> boundedUInt True 32 (binOp op (toBigInt x) (toBigInt y)) -bitOp (Just $ Unsigned n) op x y = boundedUIntOp n op x y -bitOp _ op x y = pure $ binOp op x y - -constPrimitives : {auto c : Ref ESs ESSt} -> ConstantPrimitives -constPrimitives = MkConstantPrimitives { - charToInt = \k => truncInt (useBigInt k) k . jsIntOfChar k - , intToChar = jsCharOfInt - , stringToInt = \k,s => jsIntOfString k s >>= truncInt (useBigInt k) k - , intToString = \_ => pure . jsAnyToString - , doubleToInt = \k => truncInt (useBigInt k) k . jsIntOfDouble k - , intToDouble = \k => pure . fromInt k - , intToInt = intImpl - } - where truncInt : (isBigInt : Bool) -> IntKind -> String -> Core String - truncInt b (Signed Unlimited) = pure - truncInt b (Signed $ P n) = boundedInt b n - truncInt b (Unsigned n) = boundedUInt b n - - shrink : IntKind -> IntKind -> String -> String - shrink k1 k2 = case (useBigInt k1, useBigInt k2) of - (True, False) => fromBigInt - _ => id - - expand : IntKind -> IntKind -> String -> String - expand k1 k2 = case (useBigInt k1, useBigInt k2) of - (False,True) => toBigInt - _ => id - - -- when going from BigInt to Number, we must make - -- sure to first truncate the BigInt, otherwise we - -- might get rounding issues - intImpl : IntKind -> IntKind -> String -> Core String - intImpl k1 k2 s = - let expanded = expand k1 k2 s - shrunk = shrink k1 k2 <$> truncInt (useBigInt k1) k2 s - in case (k1,k2) of - (_, Signed Unlimited) => pure $ expanded - (Signed m, Signed n) => - if n >= m then pure expanded else shrunk - - (Signed _, Unsigned n) => - case (useBigInt k1, useBigInt k2) of - (False,True) => truncInt True k2 (toBigInt s) - _ => shrunk - - (Unsigned m, Unsigned n) => - if n >= m then pure expanded else shrunk - - -- Only if the precision of the target is greater - -- than the one of the source, there is no need to cast. - (Unsigned m, Signed n) => - if n > P m then pure expanded else shrunk - -jsOp : {0 arity : Nat} -> {auto c : Ref ESs ESSt} -> - PrimFn arity -> Vect arity String -> Core String -jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y -jsOp (Sub ty) [x, y] = arithOp (intKind ty) "-" x y -jsOp (Mul ty) [x, y] = mult (intKind ty) x y -jsOp (Div ty) [x, y] = div (intKind ty) x y -jsOp (Mod ty) [x, y] = arithOp (intKind ty) "%" x y -jsOp (Neg ty) [x] = pure $ "(-(" ++ x ++ "))" -jsOp (ShiftL Int32Type) [x, y] = pure $ binOp "<<" x y -jsOp (ShiftL ty) [x, y] = bitOp (intKind ty) "<<" x y -jsOp (ShiftR Int32Type) [x, y] = pure $ binOp ">>" x y -jsOp (ShiftR ty) [x, y] = bitOp (intKind ty) ">>" x y -jsOp (BAnd Bits32Type) [x, y] = pure . fromBigInt $ binOp "&" (toBigInt x) (toBigInt y) -jsOp (BOr Bits32Type) [x, y] = pure . fromBigInt $ binOp "|" (toBigInt x) (toBigInt y) -jsOp (BXOr Bits32Type) [x, y] = pure . fromBigInt $ binOp "^" (toBigInt x) (toBigInt y) -jsOp (BAnd ty) [x, y] = pure $ binOp "&" x y -jsOp (BOr ty) [x, y] = pure $ binOp "|" x y -jsOp (BXOr ty) [x, y] = pure $ binOp "^" x y -jsOp (LT ty) [x, y] = pure $ boolOp "<" x y -jsOp (LTE ty) [x, y] = pure $ boolOp "<=" x y -jsOp (EQ ty) [x, y] = pure $ boolOp "===" x y -jsOp (GTE ty) [x, y] = pure $ boolOp ">=" x y -jsOp (GT ty) [x, y] = pure $ boolOp ">" x y -jsOp StrLength [x] = pure $ toBigInt $ x ++ ".length" -jsOp StrHead [x] = pure $ "(" ++ x ++ ".charAt(0))" -jsOp StrTail [x] = pure $ "(" ++ x ++ ".slice(1))" -jsOp StrIndex [x, y] = pure $ "(" ++ x ++ ".charAt(" ++ fromBigInt y ++ "))" -jsOp StrCons [x, y] = pure $ binOp "+" x y -jsOp StrAppend [x, y] = pure $ binOp "+" x y -jsOp StrReverse [x] = - do - n <- addConstToPreamble "strReverse" "x => x.split('').reverse().join('')" - pure $ n ++ "(" ++ x ++ ")" -jsOp StrSubstr [offset, length, str] = - pure $ str ++ ".slice(" ++ fromBigInt offset ++ ", " ++ fromBigInt offset ++ " + " ++ fromBigInt length ++ ")" -jsOp DoubleExp [x] = pure $ "Math.exp(" ++ x ++ ")" -jsOp DoubleLog [x] = pure $ "Math.log(" ++ x ++ ")" -jsOp DoubleSin [x] = pure $ "Math.sin(" ++ x ++ ")" -jsOp DoubleCos [x] = pure $ "Math.cos(" ++ x ++ ")" -jsOp DoubleTan [x] = pure $ "Math.tan(" ++ x ++ ")" -jsOp DoubleASin [x] = pure $ "Math.asin(" ++ x ++ ")" -jsOp DoubleACos [x] = pure $ "Math.acos(" ++ x ++ ")" -jsOp DoubleATan [x] = pure $ "Math.atan(" ++ x ++ ")" -jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")" -jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")" -jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")" - -jsOp (Cast StringType DoubleType) [x] = jsNumberOfString x -jsOp (Cast ty StringType) [x] = pure $ jsAnyToString x -jsOp (Cast ty ty2) [x] = castInt constPrimitives ty ty2 x -jsOp BelieveMe [_,_,x] = pure x -jsOp (Crash) [_, msg] = jsCrashExp msg - - -readCCPart : String -> (String, String) -readCCPart x = - let (cc, def) = break (== ':') x - in (cc, drop 1 def) - - -searchForeign : List String -> List String -> Maybe String -searchForeign prefixes [] = Nothing -searchForeign prefixes (x::xs) = - let (cc, def) = readCCPart x - in if cc `elem` prefixes then Just def - else searchForeign prefixes xs - - -makeForeign : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Name -> String -> Core String -makeForeign n x = - do - let (ty, def) = readCCPart x - case ty of - "lambda" => pure $ "const " ++ jsName n ++ " = (" ++ def ++ ")\n" - "support" => - do - let (name, lib_) = break (== ',') def - let lib = drop 1 lib_ - lib_code <- readDataFile ("js/" ++ lib ++ ".js") - ignore $ addSupportToPreamble lib lib_code - pure $ "const " ++ jsName n ++ " = " ++ lib ++ "_" ++ name ++ "\n" - "stringIterator" => - do - ignore addStringIteratorToPreamble - case def of - "new" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNew;\n" - "next" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNext;\n" - "toString" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorToString;\n" - _ => throw (InternalError $ "invalid string iterator function: " ++ def ++ ", supported functions are \"new\", \"next\", \"toString\"") - - - _ => throw (InternalError $ "invalid foreign type : " ++ ty ++ ", supported types are \"lambda\", \"support\"") - -foreignDecl : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Name -> List String -> Core String -foreignDecl n ccs = - do - s <- get ESs - case searchForeign (ccTypes s) ccs of - Just x => makeForeign n x - Nothing => throw (InternalError $ "No node or javascript definition found for " ++ show n ++ " in " ++ show ccs) - -jsPrim : {auto c : Ref ESs ESSt} -> Name -> List String -> Core String -jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ "({value: "++ v ++"})" -jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ "(" ++ r ++ ".value)" -jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ "(" ++ r ++ ".value=" ++ v ++ ")" -jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ "(Array(Number(" ++ s ++ ")).fill(" ++ v ++ "))" -jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ "(" ++ x ++ "[" ++ p ++ "])" -jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ "(" ++ x ++ "[" ++ p ++ "] = " ++ v ++ ")" -jsPrim (NS _ (UN "prim__os")) [] = - do - let oscalc = "(o => o === 'linux'?'unix':o==='win32'?'windows':o)" - sysos <- addConstToPreamble "sysos" (oscalc ++ "(require('os').platform())") - pure sysos -jsPrim (NS _ (UN "void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'" -- DEPRECATED. TODO: remove when bootstrap has been updated -jsPrim (NS _ (UN "prim__void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'" -jsPrim (NS _ (UN "prim__codegen")) [] = do - (cg :: _) <- ccTypes <$> get ESs - | _ => pure "\"javascript\"" - pure $ jsString cg -jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x) - -tag2es : Either Int String -> String -tag2es (Left x) = show x -tag2es (Right x) = jsString x - -mutual - impExp2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> ImperativeExp -> Core String - impExp2es (IEVar n) = - pure $ jsName n - impExp2es (IELambda args body) = - pure $ "(" ++ showSep ", " (map jsName args) ++ ") => {" ++ !(imperative2es 0 body) ++ "}" - impExp2es (IEApp f args) = - pure $ !(impExp2es f) ++ "(" ++ showSep ", " !(traverse impExp2es args) ++ ")" - impExp2es (IEConstant c) = - jsConstant c - impExp2es (IEPrimFn f args) = - jsOp f !(traverseVect impExp2es args) - impExp2es (IEPrimFnExt n args) = - jsPrim n !(traverse impExp2es args) - impExp2es (IEConstructorHead e) = - pure $ !(impExp2es e) ++ ".h" - impExp2es (IEConstructorTag x) = - pure $ tag2es x - impExp2es (IEConstructorArg i e) = - pure $ !(impExp2es e) ++ ".a" ++ show i - impExp2es (IEConstructor h args) = - let argPairs = zipWith (\i,a => "a" ++ show i ++ ": " ++ a ) [1..length args] !(traverse impExp2es args) - in pure $ "({" ++ showSep ", " (("h:" ++ tag2es h)::argPairs) ++ "})" - impExp2es (IEDelay e) = - pure $ "(()=>" ++ !(impExp2es e) ++ ")" - impExp2es (IEForce e) = - pure $ !(impExp2es e) ++ "()" - impExp2es IENull = - pure "undefined" - - imperative2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Nat -> ImperativeStatement -> Core String - imperative2es indent DoNothing = - pure "" - imperative2es indent (SeqStatement x y) = - pure $ !(imperative2es indent x) ++ "\n" ++ !(imperative2es indent y) - imperative2es indent (FunDecl fc n args body) = - pure $ nSpaces indent ++ "function " ++ jsName n ++ "(" ++ showSep ", " (map jsName args) ++ "){//"++ show fc ++"\n" ++ - !(imperative2es (indent+1) body) ++ "\n" ++ nSpaces indent ++ "}\n" - imperative2es indent (ForeignDecl fc n path args ret) = - pure $ !(foreignDecl n path) ++ "\n" - imperative2es indent (ReturnStatement x) = - pure $ nSpaces indent ++ "return " ++ !(impExp2es x) ++ ";" - imperative2es indent (SwitchStatement e alts def) = - do - def <- case def of - Nothing => pure "" - Just x => pure $ nSpaces (indent+1) ++ "default:\n" ++ !(imperative2es (indent+2) x) - let sw = nSpaces indent ++ "switch(" ++ !(impExp2es e) ++ "){\n" - let alts = concat !(traverse (alt2es (indent+1)) alts) - pure $ sw ++ alts ++ def ++ "\n" ++ nSpaces indent ++ "}" - imperative2es indent (LetDecl x v) = - case v of - Nothing => pure $ nSpaces indent ++ "let " ++ jsName x ++ ";" - Just v_ => pure $ nSpaces indent ++ "let " ++ jsName x ++ " = " ++ !(impExp2es v_) ++ ";" - imperative2es indent (ConstDecl x v) = - pure $ nSpaces indent ++ "const " ++ jsName x ++ " = " ++ !(impExp2es v) ++ ";" - imperative2es indent (MutateStatement x v) = - pure $ nSpaces indent ++ jsName x ++ " = " ++ !(impExp2es v) ++ ";" - imperative2es indent (ErrorStatement msg) = - pure $ nSpaces indent ++ "throw new Error("++ jsString msg ++");" - imperative2es indent (EvalExpStatement e) = - pure $ nSpaces indent ++ !(impExp2es e) ++ ";" - imperative2es indent (CommentStatement x) = - pure $ "\n/*" ++ x ++ "*/\n" - imperative2es indent (ForEverLoop x) = - pure $ nSpaces indent ++ "while(true){\n" ++ !(imperative2es (indent+1) x) ++ "\n" ++ nSpaces indent ++ "}" - - alt2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Nat -> (ImperativeExp, ImperativeStatement) -> Core String - alt2es indent (e, b) = pure $ nSpaces indent ++ "case " ++ !(impExp2es e) ++ ": {\n" ++ - !(imperative2es (indent+1) b) ++ "\n" ++ nSpaces (indent+1) ++ "break; }\n" - -static_preamble : List String -static_preamble = - [ "class IdrisError extends Error { }" - , "function __prim_js2idris_array(x){if(x.length ===0){return {h:0}}else{return {h:1,a1:x[0],a2: __prim_js2idris_array(x.slice(1))}}}" - , "function __prim_idris2js_array(x){const result = Array();while (x.h != 0) {result.push(x.a1); x = x.a2;}return result;}" - ] - -export -compileToES : Ref Ctxt Defs -> ClosedTerm -> List String -> Core String -compileToES c tm ccTypes = - do - (impDefs, impMain) <- compileToImperative c tm - s <- newRef ESs (MkESSt empty ccTypes) - defs <- imperative2es 0 impDefs - main_ <- imperative2es 0 impMain - let main = "try{" ++ main_ ++ "}catch(e){if(e instanceof IdrisError){console.log('ERROR: ' + e.message)}else{throw e} }" - st <- get ESs - let pre = showSep "\n" $ static_preamble ++ (SortedMap.values $ preamble st) - pure $ pre ++ "\n\n" ++ defs ++ main diff --git a/src/Compiler/ES/Imperative.idr b/src/Compiler/ES/Imperative.idr deleted file mode 100644 index 28844e895..000000000 --- a/src/Compiler/ES/Imperative.idr +++ /dev/null @@ -1,423 +0,0 @@ -||| 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 - -import Data.List - -import Compiler.Common -import Compiler.CompileExpr - -import public Core.Context - -import Compiler.ES.TailRec - -%default covering - -mutual - isNameUsed : Name -> NamedCExp -> Bool - isNameUsed name (NmLocal fc n) = n == name - isNameUsed name (NmRef fc n) = n == name - isNameUsed name (NmLam fc n e) = isNameUsed name e - isNameUsed name (NmApp fc x args) - = isNameUsed name x || any (isNameUsed name) args - isNameUsed name (NmPrimVal fc c) = False - isNameUsed name (NmOp fc op args) = any (isNameUsed name) args - isNameUsed name (NmConCase fc sc alts def) - = isNameUsed name sc - || any (isNameUsedConAlt name) alts - || maybe False (isNameUsed name) def - isNameUsed name (NmConstCase fc sc alts def) - = isNameUsed name sc - || any (isNameUsedConstAlt name) alts - || maybe False (isNameUsed name) def - isNameUsed name (NmExtPrim fc p args) = any (isNameUsed name) args - isNameUsed name (NmCon fc x _ t args) = any (isNameUsed name) args - isNameUsed name (NmDelay fc _ t) = isNameUsed name t - isNameUsed name (NmForce fc _ t) = isNameUsed name t - isNameUsed name (NmLet fc x val sc) = - if x == name then isNameUsed name val - else isNameUsed name val || isNameUsed name sc - isNameUsed name (NmErased fc) = False - isNameUsed name (NmCrash fc msg) = False - - isNameUsedConAlt : Name -> NamedConAlt -> Bool - isNameUsedConAlt name (MkNConAlt n _ t args exp) = isNameUsed name exp - - isNameUsedConstAlt : Name -> NamedConstAlt -> Bool - isNameUsedConstAlt name (MkNConstAlt c exp) = isNameUsed name exp - -data Imps : Type where - -record ImpSt where - constructor MkImpSt - nextName : Int - -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 - --- 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 - --- memoize an intermediary result in a `let` binding. --- doesn't do anything if `exp` is a variable, constant --- or undefined. -memoExp : {auto c : Ref Imps ImpSt} - -> (exp : ImperativeExp) - -> Core (ImperativeStatement, ImperativeExp) -memoExp e@(IEVar _) = pure (neutral, e) -memoExp e@(IEConstant _) = pure (neutral, e) -memoExp IENull = pure (neutral, IENull) -memoExp e = map (\n =>(LetDecl n $ Just e, IEVar n)) genName - -mutual - -- 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 (concatMap fst a, map snd a) - - -- 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 (concatMap fst a, map snd a) - - 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 - 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 - 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 - (s2, exp2) <- memoExp exp - res <- genName - swalts <- traverse (impConAltFalse res exp2) 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 exp2) swalts (Just swdef) - pure (s1 <+> s2 <+> 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 - (s2, exp2) <- memoExp exp - swalts <- traverse (impConAltTrue exp2) alts - swdef <- case def of - Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc - Just x => impExp True x - let switch = SwitchStatement (IEConstructorHead exp2) swalts (Just swdef) - pure (s1 <+> s2 <+> 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 - -- a switch statement. - -- TODO: Use ConInfo - -- - -- @ res : name of the local var (from a `let` statement) - -- to which the result should be assigned (if any) - -- @ target : The value against which to match - -- @ con : The constructor to use - impConAltFalse : {auto c : Ref Imps ImpSt} - -> (res : Name) - -> (target : ImperativeExp) - -> (con : NamedConAlt) - -> Core (ImperativeExp, ImperativeStatement) - impConAltFalse res target (MkNConAlt n _ tag args exp) = - do (s, r) <- impExp False exp - (tgts,tgte) <- memoExp target - let nargs = length args - let reps = zipWith (\i, n => (n, IEConstructorArg (cast i) tgte)) - [1..nargs] - args - pure ( IEConstructorTag (impTag n tag) - , tgts <+> (replaceNamesExpS reps $ s <+> MutateStatement res r) - ) - - impConAltTrue : {auto c : Ref Imps ImpSt} - -> (target : ImperativeExp) - -> (con : NamedConAlt) - -> Core (ImperativeExp, ImperativeStatement) - impConAltTrue target (MkNConAlt n _ tag args exp) = - do s <- impExp True exp - (tgts,tgte) <- memoExp target - let nargs = length args - let reps = zipWith (\i, n => (n, IEConstructorArg (cast i) tgte)) - [1..nargs] - args - pure ( IEConstructorTag (impTag n tag), tgts <+> replaceNamesExpS reps s) - - impConstAltFalse : {auto c : Ref Imps ImpSt} - -> Name - -> NamedConstAlt - -> Core (ImperativeExp, ImperativeStatement) - impConstAltFalse res (MkNConstAlt c exp) = - do (s, r) <- impExp False exp - pure (IEConstant c, s <+> MutateStatement res r) - - impConstAltTrue : {auto c : Ref Imps ImpSt} - -> NamedConstAlt - -> Core (ImperativeExp, ImperativeStatement) - impConstAltTrue (MkNConstAlt c exp) = - do s <- impExp True exp - pure (IEConstant c, s) - --- 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) = - throw $ (InternalError $ show exp) -getImp (n, fc, MkNmForeign cs args ret) = - pure $ ForeignDecl fc n 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 c tm = - 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 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 deleted file mode 100644 index c74465147..000000000 --- a/src/Compiler/ES/ImperativeAst.idr +++ /dev/null @@ -1,340 +0,0 @@ -||| 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 -import public Core.TT -import public Data.Vect -import public Data.List - -%default covering - -mutual - ||| A tree representing an ES expression. - ||| - ||| This is converted to ES code in function - ||| `Compiler.ES.ES.impExp2es`. - public export - 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 : 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 - DoNothing <+> y = y - x <+> DoNothing = x - x <+> y = SeqStatement x y - -public export -Monoid ImperativeStatement where - neutral = DoNothing - -mutual - export - Show ImperativeExp where - show (IEVar n) = "(IEVar " ++ show n ++ ")" - show (IELambda args b) = "(IELambda " ++ show args ++ " " ++ show b ++ ")" - show (IEApp f args) = "(IEApp " ++ show f ++ " " ++ show args ++ ")" - show (IEConstant c) = "(IEConstant " ++ show c ++ ")" - show (IEPrimFn f args) = "(IEPrimFn " ++ show f ++ " " ++ show args ++ ")" - show (IEPrimFnExt f args) = "(IEPrimFnExt " ++ show f ++ " " ++ show args ++ ")" - show (IEConstructorHead c) = "(IEConstructorHead " ++ show c ++ ")" - show (IEConstructorTag t) = "(IEConstructorTag " ++ show t ++ ")" - show (IEConstructorArg i c) = "(IEConstructorArg " ++ show i ++ " " ++ show c ++ ")" - show (IEConstructor i args) = "(IEConstructor " ++ show i ++ " " ++ show args ++ ")" - show (IEDelay x) = "(IEDelay " ++ show x ++ ")" - show (IEForce x) = "(IEForce " ++ show x ++ ")" - show IENull = "IENull" - - export - Show ImperativeStatement where - show DoNothing = "DoNothing" - show (SeqStatement x y) = show x ++ ";" ++ show y - show (FunDecl fc n args b) = "\n\n" ++ "(FunDecl (" ++ show fc ++ ") " ++ show n ++ " " ++ show args ++ " " ++ show b ++ ")" - show (ForeignDecl fc n path args ret) = "(ForeignDecl " ++ show n ++ " " ++ show path ++")" - show (ReturnStatement x) = "(ReturnStatement " ++ show x ++ ")" - show (SwitchStatement e alts d) = "(SwitchStatement " ++ show e ++ " " ++ show alts ++ " " ++ show d ++ ")" - show (LetDecl n v) = "(LetDecl " ++ show n ++ " " ++ show v ++ ")" - show (ConstDecl n v) = "(ConstDecl " ++ show n ++ " " ++ show v ++ ")" - show (MutateStatement n v) = "(MutateStatement " ++ show n ++ " " ++ show v ++ ")" - show (ErrorStatement s) = "(ErrorStatement " ++ s ++ ")" - show (EvalExpStatement x) = "(EvalExpStatement " ++ show x ++ ")" - show (CommentStatement x) = "(CommentStatement " ++ show x ++ ")" - 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 = - case rep x of - 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 rep DoNothing = - DoNothing - replaceExpS rep (SeqStatement x y) = - SeqStatement (replaceExpS rep x) (replaceExpS rep y) - replaceExpS rep (FunDecl fc n args body) = - FunDecl fc n args $ replaceExpS rep body - replaceExpS reps decl@(ForeignDecl fc n path args ret) = - decl - replaceExpS rep (ReturnStatement e) = - ReturnStatement $ replaceExp rep e - replaceExpS rep (SwitchStatement s alts def) = - let s_ = replaceExp rep s - alts_ = (\(e,b) => (replaceExp rep e, replaceExpS rep b)) <$> alts - def_ = replaceExpS rep <$> def - in SwitchStatement s_ alts_ def_ - replaceExpS rep (LetDecl n v) = - LetDecl n $ replaceExp rep <$> v - replaceExpS rep (ConstDecl n v) = - ConstDecl n $ replaceExp rep v - replaceExpS rep (MutateStatement n v) = - MutateStatement n $ replaceExp rep v - replaceExpS rep (ErrorStatement s) = - ErrorStatement s - replaceExpS rep (EvalExpStatement x) = - EvalExpStatement $ replaceExp rep x - replaceExpS rep (CommentStatement x) = - CommentStatement x - replaceExpS rep (ForEverLoop x) = - ForEverLoop $ replaceExpS rep x - - -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 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 reps x = - replaceExp (rep reps) x diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index 2e366a3e0..ac70fed96 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -1,13 +1,14 @@ ||| The `Javascript` code generator. module Compiler.ES.Javascript -import Compiler.ES.ES +import Compiler.ES.Codegen import Compiler.Common import Compiler.CompileExpr import Core.Context import Core.TT +import Core.Options import Libraries.Utils.Path import System @@ -22,8 +23,7 @@ import Libraries.Data.String.Extra ||| Compile a TT expression to Javascript compileToJS : Ref Ctxt Defs -> ClosedTerm -> Core String -compileToJS c tm = - compileToES c tm ["browser", "javascript"] +compileToJS c tm = compileToES c Javascript tm ["browser", "javascript"] htmlHeader : String htmlHeader = concat $ the (List String) $ diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index bf9664fee..223143e12 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -3,12 +3,13 @@ module Compiler.ES.Node import Idris.Env -import Compiler.ES.ES +import Compiler.ES.Codegen import Compiler.Common import Compiler.CompileExpr import Core.Context +import Core.Options import Core.TT import Libraries.Utils.Path @@ -28,8 +29,7 @@ findNode = do ||| Compile a TT expression to Node compileToNode : Ref Ctxt Defs -> ClosedTerm -> Core String -compileToNode c tm = do - compileToES c tm ["node", "javascript"] +compileToNode c tm = compileToES c Node tm ["node", "javascript"] ||| Node implementation of the `compileExpr` interface. compileExpr : Ref Ctxt Defs diff --git a/src/Compiler/ES/State.idr b/src/Compiler/ES/State.idr new file mode 100644 index 000000000..c41f9e260 --- /dev/null +++ b/src/Compiler/ES/State.idr @@ -0,0 +1,237 @@ +||| State used during JS code generation and when +||| converting `NamedCExp` to imperative statements. +module Compiler.ES.State + +import Core.Context +import Compiler.ES.Ast +import Libraries.Data.SortedMap + +%default total + +-------------------------------------------------------------------------------- +-- Utilities +-------------------------------------------------------------------------------- + +||| Convenient alias for `throw . InternalError` +export +error : String -> Core a +error = throw . InternalError + +||| Convenient alias for `error . fastConcat`. +export +errorConcat : List String -> Core a +errorConcat = error . fastConcat + +-------------------------------------------------------------------------------- +-- CG Mode +-------------------------------------------------------------------------------- + +||| Specifies the readability of the generated code. +||| +||| In `Pretty` mode (the default), the codegen will +||| lift multiline lambdas from argument lists to the +||| surrounding scope and keep user generated names. +||| In addition, blocks of code are laid out with indentation +||| and linebreaks for better readability. +||| +||| In `Compact` mode, all local variables are replace with +||| short machine generated ones, and every toplevel +||| function is printed on a single line without +||| line-breaks or indentation. +||| +||| Finally, `Minimal` mode is like `Compact`, but toplevel +||| function names will be mangled and replaced with +||| machine generated indices. +public export +data CGMode = Pretty | Compact | Minimal + +||| We only keep user defined local names and only so +||| in `Pretty` mode. +export +keepLocalName : Name -> CGMode -> Bool +keepLocalName (UN n) Pretty = True +keepLocalName _ _ = False + +||| We mangle toplevel function names only in `Minimal` mode. +export +keepRefName : Name -> CGMode -> Bool +keepRefName _ Minimal = False +keepRefName _ _ = True + +-------------------------------------------------------------------------------- +-- State +-------------------------------------------------------------------------------- + +public export +data ESs : Type where + +||| Settings and state used during JS code generation. +public export +record ESSt where + constructor MkESSt + ||| Whether to always use minimal names + mode : CGMode + + ||| Returns `True`, if the given expression can be used as an + ||| argument in a function call. (If this returns `False`, the + ||| given expression will be lifted to the surrounding scope + ||| and bound to a new local variable). + isArg : Exp -> Bool + + ||| Returns `True`, if the given expression can be used directly + ||| in a function application. (If this returns `False`, the + ||| given expression will be lifted to the surrounding scope + ||| and bound to a variable). + isFun : Exp -> Bool + + ||| Current local variable index + loc : Int + + ||| Current global variable index + ref : Int + + ||| Mapping from local names to minimal expressions + locals : SortedMap Name Minimal + + ||| Mapping from toplevel function names to variables + refs : SortedMap Name Var + + ||| Mappings from name to definitions to be added + ||| to the preamble. + preamble : SortedMap String String + + ||| Accepted codegen types in foreign function definitions. + ||| For JS, this is either `["node","javascript"]` or + ||| `["browser","javascript"]`. + ccTypes : List String + +-------------------------------------------------------------------------------- +-- Local Variables +-------------------------------------------------------------------------------- + +||| Map a local name to the given minimal expression +export +addLocal : { auto c : Ref ESs ESSt } -> Name -> Minimal -> Core () +addLocal n v = update ESs $ record { locals $= insert n v } + +||| Get and bump the local var index +export +nextLocal : { auto c : Ref ESs ESSt } -> Core Var +nextLocal = do + st <- get ESs + put ESs $ record { loc $= (+1) } st + pure $ VLoc st.loc + +||| Register a `Name` as a local variable. The name is kept +||| unchanged if `keepLocalName` returns `True` with the +||| current name and state, otherwise it is converted to +||| a new local variable. +export +registerLocal : {auto c : Ref ESs ESSt} -> (name : Name) -> Core Var +registerLocal n = do + st <- get ESs + if keepLocalName n st.mode + then let v = VName n in addLocal n (MVar v) >> pure v + else do v <- nextLocal + addLocal n (MVar v) + pure v + +||| Look up a name and call `registerLocal` in case it has +||| not been added to the map of local names. +export +getOrRegisterLocal : {auto c : Ref ESs ESSt} -> Name -> Core Minimal +getOrRegisterLocal n = do + Nothing <- lookup n . locals <$> get ESs + | Just v => pure v + MVar <$> registerLocal n + +||| Maps the given list of names (from a pattern match +||| on a data constructor) to the corresponding +||| projections on the given scrutinee. +export +projections : {auto c : Ref ESs ESSt} + -> (scrutinee : Minimal) + -> List Name + -> Core () +projections sc xs = + let ps = zip [1..length xs] xs + in traverse_ (\(i,n) => addLocal n $ MProjection i sc) ps + +-------------------------------------------------------------------------------- +-- Toplevel Names +-------------------------------------------------------------------------------- + +||| Map a toplevel function name to the given `Var` +export +addRef : { auto c : Ref ESs ESSt } -> Name -> Var -> Core () +addRef n v = update ESs $ record { refs $= insert n v } + +||| Get and bump the local ref index +export +nextRef : { auto c : Ref ESs ESSt } -> Core Var +nextRef = do + st <- get ESs + put ESs $ record { ref $= (+1) } st + pure $ VRef st.ref + +registerRef : {auto c : Ref ESs ESSt} -> (name : Name) -> Core Var +registerRef n = do + st <- get ESs + if keepRefName n st.mode + then let v = VName n in addRef n v >> pure v + else do v <- nextRef + addRef n v + pure v + +||| Look up a name and call `registerRef` in case it has +||| not been added to the map of toplevel function names. +||| The name will be replace with an index if the current +||| `GCMode` is set to `Minimal`. +export +getOrRegisterRef : {auto c : Ref ESs ESSt} -> Name -> Core Var +getOrRegisterRef n = do + Nothing <- lookup n . refs <$> get ESs + | Just v => pure v + registerRef n + +-------------------------------------------------------------------------------- +-- Preamble and Foreign Definitions +-------------------------------------------------------------------------------- + +||| Add a new set of definitions under the given name to +||| the preamble. Fails with an error if a different set +||| of definitions have already been added under the same name. +export +addToPreamble : {auto c : Ref ESs ESSt} + -> (name : String) + -> (def : String) -> Core () +addToPreamble name def = do + s <- get ESs + case lookup name (preamble s) of + Nothing => put ESs $ record { preamble $= insert name def } s + Just x => + unless (x == def) $ do + errorConcat + [ "two incompatible definitions for ", name + , "<|",x ,"|> <|" , def, "|>" + ] + +-------------------------------------------------------------------------------- +-- Initialize State +-------------------------------------------------------------------------------- + +||| Initial state of the code generator +export +init : (mode : CGMode) + -> (isArg : Exp -> Bool) + -> (isFun : Exp -> Bool) + -> (types : List String) + -> ESSt +init mode isArg isFun ccs = + MkESSt mode isArg isFun 0 0 empty empty empty ccs + +||| Reset the local state before defining a new toplevel +||| function. +export +reset : {auto c : Ref ESs ESSt} -> Core () +reset = update ESs $ record { loc = 0, locals = empty } diff --git a/src/Compiler/ES/TailRec.idr b/src/Compiler/ES/TailRec.idr index e204a4402..6e3b581c5 100644 --- a/src/Compiler/ES/TailRec.idr +++ b/src/Compiler/ES/TailRec.idr @@ -12,8 +12,8 @@ ||| -- f3 -- ||| ``` ||| -||| Function `tailCallGraph` creates a directed graph of all toplevel -||| function calls (incoming and outgoing) in tail-call position: +||| First, a directed graph of all toplevel function calls +||| (incoming and outgoing) in tail-call position is created: ||| ||| ```idris ||| MkCallGraph $ fromList [(f1,[f1,f2,f3]),(f2,[f1,f4]),(f3,[f2])] @@ -22,62 +22,98 @@ ||| ||| 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: +||| to every other function. Tarjan's algorithm is used to identify +||| these strongly connected components and grouping them in +||| a `List` of `List1`s. ||| +||| A tail-recursive group of functions is now converted to an imperative +||| loop as follows: Let `obj={h:_, a1:_, a2:_, ...}` +||| be a Javascript object consisting +||| of a tag `h` and arguments `a1`,`a2`,... . `h` indicates, whether `obj.a1` +||| contains the result of the computation (`h = 0`) or describes +||| a continuation indicating the next function to be invoked, in which +||| case fields `a1`,`a2`,... are the function's arguments. +||| together with the necessary arguments. The group of mutually +||| recursive functions is now converted to a single switch statement +||| where each branch corresponds to one of the function. +||| Each function will be changed in such a way that instead of +||| (recursively) calling another function in its group it will return +||| a new object `{h:_, a1:_, ...}` with `h` indicating the next +||| function to call (the next branch to choose in the `switch` +||| statement and `a1`,`a2`,... being the next function's set of +||| arguments. The function and initial argument object will then +||| be passed to toplevel function `__tailRec`, which loops +||| until the object signals that we have arrived at a result. ||| -||| ```idris -||| fromList [(f1,f1),(f1,f2),(f1,f3),(f4,f4)] -||| ```idris +||| Here is an example of two mutually tail-recursive functions +||| together with the generated tail-call optimized code. ||| -||| 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: +||| Original version: ||| ||| ```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 +||| function isEven(arg){ +||| switch (arg) { +||| case 0 : return 1; +||| default : return isOdd(arg - 1); ||| } -||| } +||| } ||| -||| // 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; +||| function isOdd(arg){ +||| switch (arg) { +||| case 0 : return 0; +||| default : return isEven(arg - 1); ||| } -||| } ||| } ||| ``` +||| +||| The above gets converted to code similar to +||| the following. +||| +||| ```javascript +||| function tcOpt(arg) { +||| switch(arg.h) { +||| // former function isEven +||| case 1: { +||| switch (arg.a1) { +||| case 0 : return {h: 0, a1: 1}; +||| default : return {h: 2, a1: arg.a1 - 1}; +||| } +||| } +||| // former function isOdd +||| case 2: { +||| switch (a1) { +||| case 0 : return {h: 0, a1: 0}; +||| default : return {h: 1, a1: arg.a1 - 1}; +||| } +||| } +||| } +||| +||| function isEven(arg){ +||| return __tailRec(tcOpt,{h: 1, a1: arg}) +||| } +||| +||| function isOdd(arg){ +||| return __tailRec(tcOpt,{h: 2, a1: arg}) +||| } +||| ``` +||| +||| Finally, `__tailRec` is implemented as follows: +||| +||| ```javascript +||| function __tailRec(f,ini) { +||| let obj = ini; +||| while(true){ +||| switch(obj.h){ +||| case 0: return obj.a1; +||| default: obj = f(obj); +||| } +||| } +||| } +||| ``` +||| +||| While the above example is in Javascript, this module operates +||| on `NamedCExp` exclusively, so it might be used with any backend +||| where the things described above can be expressed. module Compiler.ES.TailRec import Data.Maybe @@ -87,218 +123,230 @@ import Data.String import Libraries.Data.Graph import Libraries.Data.SortedSet import Libraries.Data.List.Extra as L -import Libraries.Data.SortedSet -import Libraries.Data.SortedMap +import Libraries.Data.SortedMap as M import Core.Name +import Core.CompileExpr import Core.Context -import Compiler.ES.ImperativeAst -import Debug.Trace +-------------------------------------------------------------------------------- +-- Utilities +-------------------------------------------------------------------------------- -%default covering +-- indices of a list starting at 1 +indices : List a -> List Int +indices as = [1 .. cast (length as)] -data TailRecS : Type where +zipWithIndices : List a -> List (Int,a) +zipWithIndices as = zip (indices as) as -record TailSt where - constructor MkTailSt - nextName : Int +-------------------------------------------------------------------------------- +-- Tailcall Graph +-------------------------------------------------------------------------------- -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 +||| A (toplevel) function in a group of mutually tail recursive functions. +public export +record TcFunction where + constructor MkTcFunction + ||| Function's name + name : Name --- returns the set of tail calls made from a given --- imperative statement. -allTailCalls : ImperativeStatement -> SortedSet Name -allTailCalls (SeqStatement x y) = allTailCalls y -allTailCalls (ReturnStatement $ IEApp (IEVar n) _) = singleton n -allTailCalls (SwitchStatement e alts d) = - concatMap allTailCalls d `union` concatMap (allTailCalls . snd) alts -allTailCalls (ForEverLoop x) = allTailCalls x -allTailCalls o = empty + ||| Function's index in its tail call group + ||| This is used to decide on which branch to choose in + ||| the next iteration + index : Int -argsName : Name -argsName = MN "imp_gen_tailoptim_Args" 0 + ||| Argument list + args : List Name -stepFnName : Name -stepFnName = MN "imp_gen_tailoptim_step" 0 + ||| Function's definition + exp : NamedCExp -fusionArgsName : Name -fusionArgsName = MN "imp_gen_tailoptim_fusion_args" 0 +||| A group of mutually tail recursive toplevel functions. +public export +record TcGroup where + constructor MkTcGroup + ||| Index of the group. This is used to generate a uniquely + ||| named tail call optimized toplevel function. + index : Int -createNewArgs : List ImperativeExp -> ImperativeExp -createNewArgs = IEConstructor (Left 0) + ||| Set of mutually recursive functions. + functions : SortedMap Name TcFunction -createArgInit : List Name -> ImperativeStatement -createArgInit names = - LetDecl argsName (Just $ IEConstructor (Left 0) (map IEVar names)) +-- tail calls made from an expression +tailCalls : NamedCExp -> SortedSet Name +tailCalls (NmLet _ _ _ z) = tailCalls z +tailCalls (NmApp _ (NmRef _ x) _) = singleton x +tailCalls (NmConCase fc sc xs x) = + concatMap (\(MkNConAlt _ _ _ _ x) => tailCalls x) xs <+> + concatMap tailCalls x +tailCalls (NmConstCase fc sc xs x) = + concatMap (\(MkNConstAlt _ x) => tailCalls x) xs <+> + concatMap tailCalls x +tailCalls _ = empty -replaceTailCall : Name -> ImperativeStatement -> ImperativeStatement -replaceTailCall n (SeqStatement x y) = SeqStatement x (replaceTailCall n y) -replaceTailCall n (ReturnStatement x) = - let defRet = ReturnStatement $ IEConstructor (Left 1) [x] - in case x of - IEApp (IEVar cn) arg_vals => - if n == cn then ReturnStatement $ createNewArgs arg_vals - else defRet - _ => defRet -replaceTailCall n (SwitchStatement e alts d) = - SwitchStatement e (map (mapSnd $ replaceTailCall n) alts) - (map (replaceTailCall n) d) -replaceTailCall n (ForEverLoop x) = - ForEverLoop $ replaceTailCall n x -replaceTailCall n o = o +-- Checks if a `List1` of functions actually has any tail recursive +-- function calls and needs to be optimized. +-- In case of a larger group (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. +-- We use the given mapping from `Name` to set of names +-- called in tail position to verify this. +hasTailCalls : SortedMap Name (SortedSet Name) -> List1 Name -> Bool +hasTailCalls g (x ::: Nil) = maybe False (contains x) $ lookup x g +hasTailCalls _ _ = True --- generates the tailcall-optimized function body -makeTailOptimToBody : Name - -> List Name - -> ImperativeStatement - -> ImperativeStatement -makeTailOptimToBody n argNames body = - let newArgExp = map (\x => IEConstructorArg (cast x) (IEVar argsName)) [1..length argNames] - bodyArgsReplaced = replaceNamesExpS (zip argNames newArgExp) body - stepBody = replaceTailCall n bodyArgsReplaced +-- Given a strongly connected group of functions, plus +-- a unique index, convert them to a list of +-- consisting of the function names plus the `TcGroup`, +-- to which they belong. +toGroup : SortedMap Name (Name,List Name,NamedCExp) + -> (Int,List1 Name) + -> List (Name,TcGroup) +toGroup funMap (groupIndex,functions) = + let ns = zipWithIndices $ forget functions + group = MkTcGroup groupIndex . fromList $ mapMaybe fun ns + in (,group) <$> forget functions + where fun : (Int,Name) -> Maybe (Name,TcFunction) + fun (fx, n) = do + (_,args,exp) <- lookup n funMap + pure (n,MkTcFunction n fx args exp) - -- 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 +-- Returns the connected components of the tail call graph +-- of a set of toplevel function definitions. +-- Every function name that is part of a tail-call group +-- (a set of mutually tail-recursive functions) +-- points to its corresponding group. +tailCallGroups : List (Name,List Name,NamedCExp) + -> SortedMap Name TcGroup +tailCallGroups funs = + let funMap = M.fromList $ map (\t => (fst t,t)) funs + graph = map (\(_,_,x) => tailCalls x) funMap + groups = filter (hasTailCalls graph) $ tarjan graph + in fromList $ concatMap (toGroup funMap) (zipWithIndices groups) - -- calls the step function and mutates the loop object with the result - loopRec = MutateStatement argsName (IEApp (IEVar stepFnName) [IEVar argsName]) +-------------------------------------------------------------------------------- +-- Converting tail call groups to expressions +-------------------------------------------------------------------------------- - -- returns field `a1` from the loop object. - loopReturn = ReturnStatement (IEConstructorArg 1 $ IEVar argsName) +public export +record Function where + constructor MkFunction + name : Name + args : List Name + body : NamedCExp - -- 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 +tcFunction : Int -> Name +tcFunction = MN "$tcOpt" --- 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 -> SortedMap Name (SortedSet Name) -tailCallGraph (SeqStatement x y) = - mergeWith union (tailCallGraph x) (tailCallGraph y) +tcArgName : Name +tcArgName = MN "$a" 0 -tailCallGraph (FunDecl fc n args body) = - singleton n $ allTailCalls body +tcContinueName : (groupIndex : Int) -> (functionIndex : Int) -> Name +tcContinueName gi fi = MN ("TcContinue" ++ show gi) fi -tailCallGraph _ = empty +tcDoneName : (groupIndex : Int) -> Name +tcDoneName gi = MN "TcDone" gi --- 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 +-- Converts a single function in a mutually tail-recursive +-- group of functions to a single branch in a pattern match. +-- Recursive function calls will be replaced with an +-- applied data constructor whose tag indicates the +-- branch in the pattern match to use next, and whose values +-- will be used as the arguments for the next function. +conAlt : TcGroup -> TcFunction -> NamedConAlt +conAlt (MkTcGroup tcIx funs) (MkTcFunction n ix args exp) = + let name = tcContinueName tcIx ix + in MkNConAlt name DATACON (Just ix) args (toTc exp) -recursiveTailCallGroups : SortedMap Name (SortedSet Name) -> List (List Name) -recursiveTailCallGroups graph = - [forget x | x <-tarjan graph, hasTailCalls x] + where mutual + -- this is returned in case we arrived at a result + -- (an expression not corresponding to a recursive + -- call in tail position). + tcDone : NamedCExp -> NamedCExp + tcDone x = NmCon EmptyFC (tcDoneName tcIx) DATACON (Just 0) [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 - hasTailCalls _ = True + -- this is returned in case we arrived at a resursive call + -- in tail position. The index indicates the next "function" + -- to call, the list of expressions are the function's + -- arguments. + tcContinue : (index : Int) -> List NamedCExp -> NamedCExp + tcContinue ix = NmCon EmptyFC (tcContinueName tcIx ix) DATACON (Just ix) --- 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 - in (xs <+> ys, mergeLeft xf yf) -extractFunctions toExtract f@(FunDecl fc n args body) = - if contains n toExtract then (neutral, insert n (fc, args, body) empty) - else (f, empty) -extractFunctions toExtract x = - (x, empty) + -- recursively converts an expression. Only the `NmApp` case is + -- interesting, the rest is pretty much boiler plate. + toTc : NamedCExp -> NamedCExp + toTc (NmLet fc x y z) = NmLet fc x y $ toTc z + toTc x@(NmApp _ (NmRef _ n) xs) = + case lookup n funs of + Just v => tcContinue v.index xs + Nothing => tcDone x + toTc (NmConCase fc sc a d) = NmConCase fc sc (map con a) (map toTc d) + toTc (NmConstCase fc sc a d) = NmConstCase fc sc (map const a) (map toTc d) + toTc x@(NmCrash _ _) = x + toTc x = tcDone x --- 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 + con : NamedConAlt -> NamedConAlt + con (MkNConAlt x y tag xs z) = MkNConAlt x y tag xs (toTc z) -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] - bodyRepArgs = replaceNamesExpS (zip args newArgExp) body - in (IEConstructorTag $ Left $ cast i, replaceExpS rep bodyRepArgs) - where - rep : ImperativeExp -> Maybe ImperativeExp - rep (IEApp (IEVar n) arg_vals) = - case lookup n functionsIdx of - Nothing => Nothing - Just i => Just $ IEApp - (IEVar fusionName) - [IEConstructor (Left $ cast i) arg_vals] - rep _ = Nothing + const : NamedConstAlt -> NamedConstAlt + const (MkNConstAlt x y) = MkNConstAlt x (toTc y) -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)]) +-- Converts a group of mutually tail recursive functions +-- to a list of toplevel function declarations. `tailRecLoopName` +-- is the name of the toplevel function that does the +-- infinite looping (function `__tailRec` in the example at +-- the top of this module). +convertTcGroup : (tailRecLoopName : Name) -> TcGroup -> List Function +convertTcGroup loop g@(MkTcGroup gindex fs) = + let functions = sortBy (comparing index) $ values fs + branches = map (conAlt g) functions + switch = NmConCase EmptyFC (local tcArgName) branches Nothing + in MkFunction tcFun [tcArgName] switch :: map toFun functions -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) + where tcFun : Name + tcFun = tcFunction gindex -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 + local : Name -> NamedCExp + local = NmLocal EmptyFC -||| (Mutual) Tail recursion optimizations: Converts all groups of -||| mutually tail recursive functions to an imperative loop. + toFun : TcFunction -> Function + toFun (MkTcFunction n ix args x) = + let exps = map local args + tcArg = NmCon EmptyFC (tcContinueName gindex ix) + DATACON (Just ix) exps + tcFun = NmRef EmptyFC tcFun + body = NmApp EmptyFC (NmRef EmptyFC loop) [tcFun,tcArg] + in MkFunction n args body + +-- Tail recursion optimizations: Converts all groups of +-- mutually tail recursive functions to an imperative loop. +tailRecOptim : SortedMap Name TcGroup + -> (tcLoopName : Name) + -> List (Name,List Name,NamedCExp) + -> List Function +tailRecOptim groups loop ts = + let regular = mapMaybe toFun ts + tailOpt = concatMap (convertTcGroup loop) $ values groups + in tailOpt ++ regular + + where toFun : (Name,List Name,NamedCExp) -> Maybe Function + toFun (n,args,exp) = case lookup n groups of + Just _ => Nothing + Nothing => Just $ MkFunction n args exp + +||| Converts a list of toplevel definitions (potentially +||| several groups of mutually tail-recursive functions) +||| to a new set of tail-call optimized function definitions. +||| `MkNmFun`s are converted. Other constructors of `NamedDef` +||| are ignored and silently dropped. export -tailRecOptim : ImperativeStatement -> Core ImperativeStatement -tailRecOptim x = - do ref <- newRef TailRecS (MkTailSt 0) - let groups = recursiveTailCallGroups (tailCallGraph x) - 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) +functions : (tcLoopName : Name) + -> List (Name,FC,NamedDef) + -> List Function +functions loop dfs = + let ts = mapMaybe def dfs + in tailRecOptim (tailCallGroups ts) loop ts + where def : (Name,FC,NamedDef) -> Maybe (Name,List Name,NamedCExp) + def (n,_,MkNmFun args x) = Just (n,args,x) + def _ = Nothing diff --git a/src/Compiler/ES/ToAst.idr b/src/Compiler/ES/ToAst.idr new file mode 100644 index 000000000..7d9d6d42d --- /dev/null +++ b/src/Compiler/ES/ToAst.idr @@ -0,0 +1,238 @@ +||| Functionality to convert an Idris `NamedCExp` +||| to a sequence of imperative statements. +module Compiler.ES.ToAst + +import Data.DPair +import Data.Nat +import Data.List1 +import Data.Vect +import Compiler.Common +import Core.CompileExpr +import Core.Context +import Compiler.ES.Ast +import Compiler.ES.State +import Libraries.Data.SortedMap + +-------------------------------------------------------------------------------- +-- Converting NamedCExp +-------------------------------------------------------------------------------- + +-- used to convert data and type constructor tags +tag : Name -> Maybe Int -> Either Int Name +tag n = maybe (Right n) Left + +-- creates a single assignment statement. +assign : (e : Effect) -> Exp -> Stmt (Just e) +assign Returns = Return +assign (ErrorWithout v) = Assign v + +mutual + getInteger : NamedCExp -> Maybe Integer + getInteger (NmPrimVal _ $ BI x) = Just x + getInteger x = integerArith x + + -- this is a local hack to fix #1320 for the JS backend + -- the moste basic sequences of arithmetic `Integer` expressions + -- are evaluated to prevent us from introducing slow + -- cascades of (1n + ...) coming from small `Nat` literals. + integerArith : NamedCExp -> Maybe Integer + integerArith (NmOp _ (Add IntegerType) [x,y]) = + [| getInteger x + getInteger y |] + integerArith (NmOp _ (Mul IntegerType) [x,y]) = + [| getInteger x * getInteger y |] + integerArith _ = Nothing + +mutual + -- Converts a `NamedCExp` by calling `stmt` with a + -- newly generated local variable. + -- If the result is a single assignment statement + -- and the given filter function returns a `Just a`, + -- only result `a` is returned. + -- If the result is more complex or the filter returns + -- `Nothing`, the resulting block + -- will be kept and a pointer to the new variable + -- will be returned which can then be used for instance + -- as a function's argument. + lift : { auto c : Ref ESs ESSt } + -> NamedCExp + -> (filter : Exp -> Maybe a) + -> (fromVar : Var -> a) + -> Core (List (Stmt Nothing), a) + lift n filter fromVar = do + l <- nextLocal + b <- stmt (ErrorWithout l) n + let pair = ([declare b], fromVar l) + case b of + -- elaborator needed some help here + Assign _ e => pure $ maybe pair (the (List _) [],) (filter e) + _ => pure pair + + -- Convert and lift (if necessary, see comment for `lift`) + -- a function argument. The filter function used to + -- decide whether to keep or lift a function argument + -- comes from the passed `ESSt` state and can therefore + -- vary across backends. + liftArg : { auto c : Ref ESs ESSt } + -> NamedCExp + -> Core (List (Stmt Nothing), Exp) + liftArg x = do + f <- isArg <$> get ESs + lift x (\e => guard (f e) $> e) (EMinimal . MVar) + + -- Convert and lift (if necessary, see comment for `lift`) + -- a function expression. + liftFun : { auto c : Ref ESs ESSt } + -> NamedCExp + -> Core (List (Stmt Nothing), Exp) + liftFun x = do + f <- isFun <$> get ESs + lift x (\e => guard (f e) $> e) (EMinimal . MVar) + + -- Convert and lift (if necessary, see comment for `liftArg`) + -- a `Vect` of function arguments. + liftArgsVect : { auto c : Ref ESs ESSt } + -> Vect n NamedCExp + -> Core (List (Stmt Nothing), Vect n Exp) + liftArgsVect xs = do + ps <- traverseVect liftArg xs + pure (concatMap fst ps, map snd ps) + + -- Convert and lift (if necessary, see comment for `liftArg`) + -- a `List` of function arguments. + liftArgs : { auto c : Ref ESs ESSt } + -> List NamedCExp + -> Core (List (Stmt Nothing), List Exp) + liftArgs xs = do + ps <- traverse liftArg xs + pure (concatMap fst ps, map snd ps) + + -- Convert and lift an expression. If the result is + -- not a `Minimal` expression, an additional assignment statement is + -- generated. This is used to lift the scrutinees of + -- constructor case expressions to make sure they are + -- only evluated once (see also PR #1494). + liftMinimal : { auto c : Ref ESs ESSt } + -> NamedCExp + -> Core (List (Stmt Nothing), Minimal) + liftMinimal n = lift n toMinimal MVar + + -- creates a (possibly multiargument) lambda. + lambda : {auto c : Ref ESs ESSt} -> Name -> NamedCExp -> Core Exp + lambda n x = go [n] x + where go : List Name -> NamedCExp -> Core Exp + go ns (NmLam _ n x) = go (n :: ns) x + go ns x = do + vs <- traverse registerLocal (reverse ns) + ELam vs <$> stmt Returns x + + -- convert a `NamedCExp` to a sequence of statements. + export + stmt : {auto c : Ref ESs ESSt} + -> (e : Effect) + -> NamedCExp + -> Core (Stmt $ Just e) + -- a local name gets registered or resolved + stmt e (NmLocal _ n) = assign e . EMinimal <$> getOrRegisterLocal n + + -- a function name gets registered or resolved + stmt e (NmRef _ n) = assign e . EMinimal . MVar <$> getOrRegisterRef n + + stmt e (NmLam _ n x) = assign e <$> lambda n x + + -- in case of a let expression, we just generate two + -- blocks of statements and concatenate them. + -- We always introduce a new local variable for `n`, + -- since a variable called `n` might be used in both blocks. + stmt e (NmLet _ n y z) = do + v <- nextLocal + b1 <- stmt (ErrorWithout v) y + addLocal n (MVar v) + b2 <- stmt e z + pure $ prepend [declare b1] b2 + + -- when applying a function, we potentially need to + -- lift both, the function expression itself and the argument + -- list, to the surrounding scope. + stmt e (NmApp _ x xs) = do + (mbx, vx) <- liftFun x + (mbxs, args) <- liftArgs xs + pure . prepend (mbx ++ mbxs) $ assign e (EApp vx args) + + stmt e (NmCon _ n ci tg xs) = do + (mbxs, args) <- liftArgs xs + pure . prepend mbxs $ assign e (ECon (tag n tg) ci args) + + stmt e o@(NmOp _ x xs) = + case integerArith o of + Just n => pure . assign e $ EPrimVal (BI n) + Nothing => do + (mbxs, args) <- liftArgsVect xs + pure . prepend mbxs $ assign e (EOp x args) + + stmt e (NmExtPrim _ n xs) = do + (mbxs, args) <- liftArgs xs + pure . prepend mbxs $ assign e (EExtPrim n args) + + stmt e (NmForce _ _ x) = do + (mbx, vx) <- liftFun x + pure . prepend mbx $ assign e (EApp vx []) + + stmt e (NmDelay _ _ x) = assign e . ELam [] <$> stmt Returns x + + -- No need for a `switch` if we only have a single branch. + -- It's still necessary to lift the scrutinee, however, + -- since its fields might be accessed several times in + -- the implementation of `x`. + stmt e (NmConCase _ sc [x] Nothing) = do + (mbx, vx) <- liftMinimal sc + b <- body <$> conAlt e vx x + pure $ prepend mbx b + + -- No need for a `switch` statement if we only have + -- a `default` branch. + stmt e (NmConCase _ _ [] (Just x)) = stmt e x + + -- Create a `switch` statement from a pattern match + -- on constructors. The scrutinee is lifted to the + -- surrounding scope and memoized if necessary. + stmt e (NmConCase _ sc xs x) = do + (mbx, vx) <- liftMinimal sc + alts <- traverse (conAlt e vx) xs + def <- traverseOpt (stmt e) x + pure . prepend mbx $ ConSwitch e vx alts def + + -- Pattern matches on constants behave very similar + -- to the ones on constructors. + stmt e (NmConstCase _ _ [x] Nothing) = body <$> constAlt e x + stmt e (NmConstCase _ _ [] (Just x)) = stmt e x + stmt e (NmConstCase _ sc xs x) = do + (mbx, ex) <- liftArg sc + alts <- traverse (constAlt e) xs + def <- traverseOpt (stmt e) x + pure . prepend mbx $ ConstSwitch e ex alts def + + stmt e (NmPrimVal _ x) = pure . assign e $ EPrimVal x + + stmt e (NmErased _) = pure . assign e $ EErased + + stmt _ (NmCrash _ x) = pure $ Error x + + -- a single branch in a pattern match on constructors + conAlt : { auto c : Ref ESs ESSt } + -> (e : Effect) + -> (scrutinee : Minimal) + -> NamedConAlt + -> Core (EConAlt e) + conAlt e sc (MkNConAlt n ci tg args x) = do + -- We map the list of args to the corresponding + -- data projections (field accessors). They'll + -- be then properly inlined when converting `x`. + projections sc args + MkEConAlt (tag n tg) ci <$> stmt e x + + -- a single branch in a pattern match on a constant + constAlt : { auto c : Ref ESs ESSt } + -> (e : Effect) + -> NamedConstAlt + -> Core (EConstAlt e) + constAlt e (MkNConstAlt c x) = MkEConstAlt c <$> stmt e x diff --git a/support/js/support.js b/support/js/support.js new file mode 100644 index 000000000..dc18d4fe3 --- /dev/null +++ b/support/js/support.js @@ -0,0 +1,186 @@ +class IdrisError extends Error { } + +function __prim_js2idris_array(x){ + if(x.length === 0){ + return {h:0} + } else { + return {a1:x[0],a2: __prim_js2idris_array(x.slice(1))} + } +} + +function __prim_idris2js_array(x){ + const result = Array(); + while (x.h === undefined) { + result.push(x.a1); x = x.a2; + } + return result; +} + +function __prim_stringIteratorNew(str) { + return 0 +} + +function __prim_stringIteratorToString(_, str, it, f) { + return f(str.slice(it)) +} + +function __prim_stringIteratorNext(str, it) { + if (it >= str.length) + return {h: 0}; + else + return {a1: str.charAt(it), a2: it + 1}; +} + +function __tailRec(f,ini) { + let obj = ini; + while(true){ + switch(obj.h){ + case 0: return obj.a1; + default: obj = f(obj); + } + } +} + +const _idrisworld = Symbol('idrisworld') + +const _crashExp = x=>{throw new IdrisError(x)} + +const _sysos = + ((o => o === 'linux'?'unix':o==='win32'?'windows':o)(require('os').platform())); + +const _bigIntOfString = s=>{ + const idx = s.indexOf('.') + return idx === -1 ? BigInt(s) : BigInt(s.slice(0, idx)) +} + +const _truncToChar = x=> String.fromCodePoint( + (x >= 0 && x <= 55295) || (x >= 57344 && x <= 1114111) ? x : 0 +) + +// Int8 +const _truncInt8 = x => { + const res = x & 0xff; + return res >= 0x80 ? res - 0x100 : res; +} + +const _truncBigInt8 = x => { + const res = Number(x & 0xffn); + return res >= 0x80 ? res - 0x100 : res; +} + +const _add8s = (a,b) => _truncInt8(a + b) +const _sub8s = (a,b) => _truncInt8(a - b) +const _mul8s = (a,b) => _truncInt8(a * b) +const _div8s = (a,b) => _truncInt8(Math.trunc(a / b)) +const _shl8s = (a,b) => _truncInt8(a << b) +const _shr8s = (a,b) => _truncInt8(a >> b) + +// Int16 +const _truncInt16 = x => { + const res = x & 0xffff; + return res >= 0x8000 ? res - 0x10000 : res; +} + +const _truncBigInt16 = x => { + const res = Number(x & 0xffffn); + return res >= 0x8000 ? res - 0x10000 : res; +} + +const _add16s = (a,b) => _truncInt16(a + b) +const _sub16s = (a,b) => _truncInt16(a - b) +const _mul16s = (a,b) => _truncInt16(a * b) +const _div16s = (a,b) => _truncInt16(Math.trunc(a / b)) +const _shl16s = (a,b) => _truncInt16(a << b) +const _shr16s = (a,b) => _truncInt16(a >> b) + +//Int32 +const _truncInt32 = x => x & 0xffffffff + +const _truncBigInt32 = x => { + const res = Number(x & 0xffffffffn); + return res >= 0x80000000 ? res - 0x100000000 : res; +} + +const _add32s = (a,b) => _truncInt32(a + b) +const _sub32s = (a,b) => _truncInt32(a - b) +const _div32s = (a,b) => _truncInt32(Math.trunc(a / b)) + +const _mul32s = (a,b) => { + const res = a * b; + if (res <= Number.MIN_SAFE_INTEGER || res >= Number.MAX_SAFE_INTEGER) { + return _truncInt32((a & 0xffff) * b + (b & 0xffff) * (a & 0xffff0000)) + } else { + return _truncInt32(res) + } +} + +//Int64 +const _truncBigInt64 = x => { + const res = x & 0xffffffffffffffffn; + return res >= 0x8000000000000000n ? res - 0x10000000000000000n : res; +} + +const _add64s = (a,b) => _truncBigInt64(a + b) +const _sub64s = (a,b) => _truncBigInt64(a - b) +const _mul64s = (a,b) => _truncBigInt64(a * b) +const _div64s = (a,b) => _truncBigInt64(a / b) +const _shl64s = (a,b) => _truncBigInt64(a << b) +const _shr64s = (a,b) => _truncBigInt64(a >> b) + +//Bits8 +const _truncUInt8 = x => x & 0xff + +const _truncUBigInt8 = x => Number(x & 0xffn) + +const _add8u = (a,b) => (a + b) & 0xff +const _sub8u = (a,b) => (a - b) & 0xff +const _mul8u = (a,b) => (a * b) & 0xff +const _div8u = (a,b) => Math.trunc(a / b) +const _shl8u = (a,b) => (a << b) & 0xff +const _shr8u = (a,b) => (a >> b) & 0xff + +//Bits16 +const _truncUInt16 = x => x & 0xffff + +const _truncUBigInt16 = x => Number(x & 0xffffn) + +const _add16u = (a,b) => (a + b) & 0xffff +const _sub16u = (a,b) => (a - b) & 0xffff +const _mul16u = (a,b) => (a * b) & 0xffff +const _div16u = (a,b) => Math.trunc(a / b) +const _shl16u = (a,b) => (a << b) & 0xffff +const _shr16u = (a,b) => (a >> b) & 0xffff + +//Bits32 +const _truncUBigInt32 = x => Number(x & 0xffffffffn) + +const _truncUInt32 = x => { + const res = x & -1; + return res < 0 ? res + 0x100000000 : res; +} + +const _add32u = (a,b) => _truncUInt32(a + b) +const _sub32u = (a,b) => _truncUInt32(a - b) +const _mul32u = (a,b) => _truncUInt32(_mul32s(a,b)) +const _div32u = (a,b) => Math.trunc(a / b) + +const _shl32u = (a,b) => _truncUInt32(a << b) +const _shr32u = (a,b) => _truncUInt32(a <= 0x7fffffff ? a >> b : (b == 0 ? a : (a >> b) ^ ((-0x80000000) >> (b-1)))) +const _and32u = (a,b) => _truncUInt32(a & b) +const _or32u = (a,b) => _truncUInt32(a | b) +const _xor32u = (a,b) => _truncUInt32(a ^ b) + +//Bits64 +const _truncUBigInt64 = x => x & 0xffffffffffffffffn + +const _add64u = (a,b) => (a + b) & 0xffffffffffffffffn +const _mul64u = (a,b) => (a * b) & 0xffffffffffffffffn +const _div64u = (a,b) => a / b +const _shl64u = (a,b) => (a << b) & 0xffffffffffffffffn +const _shr64u = (a,b) => (a >> b) & 0xffffffffffffffffn +const _sub64u = (a,b) => (a - b) & 0xffffffffffffffffn + +//String +const _strReverse = x => x.split('').reverse().join('') + +const _substr = (o,l,x) => x.slice(o, o + l) diff --git a/support/js/support_system_directory.js b/support/js/support_system_directory.js index 3f1b94ee9..0668f6c70 100644 --- a/support/js/support_system_directory.js +++ b/support/js/support_system_directory.js @@ -3,19 +3,19 @@ const support_system_directory_fs = require("fs"); function support_system_directory_changeDir(d){ try{ process.chdir(d); - return 0n + return 0 }catch(e){ process.__lasterr = e; - return 1n + return 1 } } function support_system_directory_createDir(d){ try{ support_system_directory_fs.mkdirSync(d) - return 0n + return 0 }catch(e){ process.__lasterr = e; - return 1n + return 1 } } diff --git a/support/js/support_system_file.js b/support/js/support_system_file.js index 4f058e67b..8c076f26e 100644 --- a/support/js/support_system_file.js +++ b/support/js/support_system_file.js @@ -2,18 +2,18 @@ const support_system_file_fs = require('fs') function support_system_file_fileErrno(){ - const n = process.__lasterr.errno || 0 + const n = process.__lasterr===undefined?0:process.__lasterr.errno || 0 if (process.platform == 'win32') { // TODO: Add the error codes for the other errors switch(n) { - case -4058: return 2n - case -4075: return 4n - default: return -BigInt(n) + case -4058: return 2 + case -4075: return 4 + default: return -n } } else { switch(n){ - case -17: return 4n - default: return -BigInt(n) + case -17: return 4 + default: return -n } } } @@ -29,13 +29,13 @@ function support_system_file_seekLine (file_ptr) { if (bytesRead === 0) { file_ptr.eof = true file_ptr.buffer = Buffer.alloc(0) - return 0n + return 0 } file_ptr.buffer = Buffer.concat([file_ptr.buffer, readBuf.slice(0, bytesRead)]) lineEnd = file_ptr.buffer.indexOf(LF) } file_ptr.buffer = file_ptr.buffer.slice(lineEnd + 1) - return 0n + return 0 } function support_system_file_readLine (file_ptr) { @@ -74,10 +74,10 @@ function support_system_file_openFile (n, m) { function support_system_file_chmod (filename, mode) { try { - support_system_file_fs.chmodSync(filename, Number(mode)) - return 0n + support_system_file_fs.chmodSync(filename, mode) + return 0 } catch (e) { process.__lasterr = e - return 1n + return 1 } } diff --git a/tests/node/casts/Casts.idr b/tests/node/casts/Casts.idr index ebbba9f6d..88823a493 100644 --- a/tests/node/casts/Casts.idr +++ b/tests/node/casts/Casts.idr @@ -156,7 +156,7 @@ results = testCasts Int8 Int16 [(-129,127),(-128,-128),(0,0),(127,127),(128,- ++ testCasts Int64 Int8 [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)] ++ testCasts Int64 Int16 [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)] ++ testCasts Int64 Int32 [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)] - ++ testCasts Int64 Int [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] + ++ testCasts Int64 Int [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)] ++ testCasts Int64 Double [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] ++ testCasts Int64 String [(-9223372036854775809,"9223372036854775807"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"-9223372036854775808")] ++ testCasts Int64 Integer [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] @@ -165,17 +165,17 @@ results = testCasts Int8 Int16 [(-129,127),(-128,-128),(0,0),(127,127),(128,- ++ testCasts Int64 Bits32 [(-9223372036854775809,4294967295),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)] ++ testCasts Int64 Bits64 [(-9223372036854775809,9223372036854775807),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] - ++ testCasts Int Int8 [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)] - ++ testCasts Int Int16 [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)] - ++ testCasts Int Int32 [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)] - ++ testCasts Int Int64 [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] - ++ testCasts Int Double [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] - ++ testCasts Int String [(-9223372036854775809,"9223372036854775807"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"-9223372036854775808")] - ++ testCasts Int Integer [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] - ++ testCasts Int Bits8 [(-9223372036854775809,255),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)] - ++ testCasts Int Bits16 [(-9223372036854775809,65535),(0,0),(9223372036854775807,0xffff),(9223372036854775808,0)] - ++ testCasts Int Bits32 [(-9223372036854775809,4294967295),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)] - ++ testCasts Int Bits64 [(-9223372036854775809,9223372036854775807),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)] + ++ testCasts Int Int8 [(-2147483649,2147483647),(-2147483648,0),(0,0),(2147483647,-1),(2147483648,0)] + ++ testCasts Int Int16 [(-2147483649,2147483647),(-2147483648,0),(0,0),(2147483647,-1),(2147483648,0)] + ++ testCasts Int Int64 [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] + ++ testCasts Int Int32 [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] + ++ testCasts Int Double [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] + ++ testCasts Int String [(-2147483649,"2147483647"),(-2147483648,"-2147483648"),(0,"0"),(2147483647,"2147483647"),(2147483648,"-2147483648")] + ++ testCasts Int Integer [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] + ++ testCasts Int Bits8 [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] + ++ testCasts Int Bits16 [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] + ++ testCasts Int Bits32 [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] + ++ testCasts Int Bits64 [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)] ++ testCasts Integer Int8 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,-1),(170141183460469231731687303715884105728,0)] ++ testCasts Integer Int16 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,-1),(170141183460469231731687303715884105728,0)] @@ -216,7 +216,7 @@ results = testCasts Int8 Int16 [(-129,127),(-128,-128),(0,0),(127,127),(128,- ++ testCasts Bits32 Int16 [(0,0),(0xffffffff,-1),(0x100000000,0)] ++ testCasts Bits32 Int32 [(0,0),(0xffffffff,-1),(0x100000000,0)] ++ testCasts Bits32 Int64 [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)] - ++ testCasts Bits32 Int [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)] + ++ testCasts Bits32 Int [(0,0),(0xffffffff,-1),(0x100000000,0)] ++ testCasts Bits32 Double [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)] ++ testCasts Bits32 String [(0,"0"),(0xffffffff,"4294967295"),(0x100000000,"0")] ++ testCasts Bits32 Integer [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)] @@ -240,7 +240,7 @@ results = testCasts Int8 Int16 [(-129,127),(-128,-128),(0,0),(127,127),(128,- ++ testCasts String Int16 [("-32769",32767),("-32768",-32768),("0",0),("32767",32767), ("32768",-32768)] ++ testCasts String Int32 [("-2147483649",2147483647),("-2147483648",-2147483648),("0",0),("2147483647",2147483647), ("2147483648",-2147483648)] ++ testCasts String Int64 [("-9223372036854775809",9223372036854775807),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",-9223372036854775808)] - ++ testCasts String Int [("-9223372036854775809",9223372036854775807),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",-9223372036854775808)] + ++ testCasts String Int [("-2147483649",2147483647),("-2147483648",-2147483648),("0",0),("2147483647",2147483647), ("2147483648",-2147483648)] ++ testCasts String Integer [("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("0",0),("170141183460469231731687303715884105728",170141183460469231731687303715884105728)] ++ testCasts String Bits8 [("0",0),("255",255), ("256",0)] ++ testCasts String Bits16 [("0",0),("65535",65535), ("65536",0)] @@ -251,7 +251,7 @@ results = testCasts Int8 Int16 [(-129,127),(-128,-128),(0,0),(127,127),(128,- ++ testCasts Double Int16 [(-32769.0, 32767),(-32768.0,-32768),(-12.001,-12),(12.001,12),(32767.0,32767),(32768.0,-32768)] ++ testCasts Double Int32 [(-2147483649.0,2147483647),(-2147483648.0,-2147483648),(-12.001,-12),(12.001,12),(2147483647.0,2147483647),(2147483648.0,-2147483648)] ++ testCasts Double Int64 [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,-9223372036854775808)] - ++ testCasts Double Int [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,-9223372036854775808)] + ++ testCasts Double Int [(-2147483649.0,2147483647),(-2147483648.0,-2147483648),(-12.001,-12),(12.001,12),(2147483647.0,2147483647),(2147483648.0,-2147483648)] ++ testCasts Double Bits8 [(0.0,0),(255.0,255), (256.0,0)] ++ testCasts Double Bits16 [(0.0,0),(65535.0,65535), (65536.0,0)] ++ testCasts Double Bits32 [(0.0,0),(4294967295.0,4294967295), (4294967296.0,0)] diff --git a/tests/node/integers/TestIntegers.idr b/tests/node/integers/TestIntegers.idr index a85e2315e..6f2867a1b 100644 --- a/tests/node/integers/TestIntegers.idr +++ b/tests/node/integers/TestIntegers.idr @@ -75,9 +75,9 @@ main = do the Int64 $ -9223372036854775808, -- Int64 min the Int64 1000000000000000000, the Int64 9223372036854775807, -- Int64 max - the Int $ -9223372036854775808, -- Int min - the Int 1000000000000000000, - the Int 9223372036854775807, -- Int max + the Int $ -2147483648, -- Int min + the Int 500000000, + the Int 2147483647, -- Int max the Integer $ -9223372036854775809, -- Int min - 1 the Integer 0, the Integer 9223372036854775808 -- Int max + 1 diff --git a/tests/node/integers/expected b/tests/node/integers/expected index 8788ffa6d..c4e737402 100644 --- a/tests/node/integers/expected +++ b/tests/node/integers/expected @@ -1,32 +1,32 @@ Cast to String: -[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775809, 0, 9223372036854775808] +[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -2147483648, 500000000, 2147483647, -9223372036854775809, 0, 9223372036854775808] Cast to Bits8: [0, 50, 255, 0, 16, 255, 0, 0, 255, 0, 0, 255, 128, 50, 127, 0, 16, 255, 0, 0, 255, 0, 0, 255, 0, 0, 255, 255, 0, 0] Cast to Bits16: -[0, 50, 255, 0, 10000, 65535, 0, 51712, 65535, 0, 0, 65535, 65408, 50, 127, 32768, 10000, 32767, 0, 25856, 65535, 0, 0, 65535, 0, 0, 65535, 65535, 0, 0] +[0, 50, 255, 0, 10000, 65535, 0, 51712, 65535, 0, 0, 65535, 65408, 50, 127, 32768, 10000, 32767, 0, 25856, 65535, 0, 0, 65535, 0, 25856, 65535, 65535, 0, 0] Cast to Bits32: -[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 1156841472, 4294967295, 4294967168, 50, 127, 4294934528, 10000, 32767, 2147483648, 500000000, 2147483647, 0, 2808348672, 4294967295, 0, 2808348672, 4294967295, 4294967295, 0, 0] +[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 1156841472, 4294967295, 4294967168, 50, 127, 4294934528, 10000, 32767, 2147483648, 500000000, 2147483647, 0, 2808348672, 4294967295, 2147483648, 500000000, 2147483647, 4294967295, 0, 0] Cast to Bits64: -[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, 18446744073709551488, 50, 127, 18446744073709518848, 10000, 32767, 18446744071562067968, 500000000, 2147483647, 9223372036854775808, 1000000000000000000, 9223372036854775807, 9223372036854775808, 1000000000000000000, 9223372036854775807, 9223372036854775807, 0, 9223372036854775808] +[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, 18446744073709551488, 50, 127, 18446744073709518848, 10000, 32767, 18446744071562067968, 500000000, 2147483647, 9223372036854775808, 1000000000000000000, 9223372036854775807, 18446744071562067968, 500000000, 2147483647, 9223372036854775807, 0, 9223372036854775808] Cast to Int: -[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, -1, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, 9223372036854775807, 0, -9223372036854775808] +[0, 50, 255, 0, 10000, 65535, 0, 1000000000, -1, 0, 1156841472, -1, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, 0, -1486618624, -1, -2147483648, 500000000, 2147483647, -1, 0, 0] Cast to Integer: -[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775809, 0, 9223372036854775808] +[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -2147483648, 500000000, 2147483647, -9223372036854775809, 0, 9223372036854775808] Add: -[1, 51, 0, 1, 10001, 0, 1, 1000000001, 0, 1, 5000000000000000001, 0, -127, 51, -128, -32767, 10001, -32768, -2147483647, 500000001, -2147483648, -9223372036854775807, 1000000000000000001, -9223372036854775808, -9223372036854775807, 1000000000000000001, -9223372036854775808, -9223372036854775808, 1, 9223372036854775809] +[1, 51, 0, 1, 10001, 0, 1, 1000000001, 0, 1, 5000000000000000001, 0, -127, 51, -128, -32767, 10001, -32768, -2147483647, 500000001, -2147483648, -9223372036854775807, 1000000000000000001, -9223372036854775808, -2147483647, 500000001, -2147483648, -9223372036854775808, 1, 9223372036854775809] Subtract: -[255, 49, 254, 65535, 9999, 65534, 4294967295, 999999999, 4294967294, 18446744073709551615, 4999999999999999999, 18446744073709551614, 127, 49, 126, 32767, 9999, 32766, 2147483647, 499999999, 2147483646, 9223372036854775807, 999999999999999999, 9223372036854775806, 9223372036854775807, 999999999999999999, 9223372036854775806, -9223372036854775810, -1, 9223372036854775807] +[255, 49, 254, 65535, 9999, 65534, 4294967295, 999999999, 4294967294, 18446744073709551615, 4999999999999999999, 18446744073709551614, 127, 49, 126, 32767, 9999, 32766, 2147483647, 499999999, 2147483646, 9223372036854775807, 999999999999999999, 9223372036854775806, 2147483647, 499999999, 2147483646, -9223372036854775810, -1, 9223372036854775807] Negate: -[0, 206, 1, 0, 55536, 1, 0, 3294967296, 1, 0, 13446744073709551616, 1, -128, -50, -127, -32768, -10000, -32767, -2147483648, -500000000, -2147483647, -9223372036854775808, -1000000000000000000, -9223372036854775807, -9223372036854775808, -1000000000000000000, -9223372036854775807, 9223372036854775809, 0, -9223372036854775808] +[0, 206, 1, 0, 55536, 1, 0, 3294967296, 1, 0, 13446744073709551616, 1, -128, -50, -127, -32768, -10000, -32767, -2147483648, -500000000, -2147483647, -9223372036854775808, -1000000000000000000, -9223372036854775807, -2147483648, -500000000, -2147483647, 9223372036854775809, 0, -9223372036854775808] Multiply: -[0, 100, 254, 0, 20000, 65534, 0, 2000000000, 4294967294, 0, 10000000000000000000, 18446744073709551614, 0, 100, -2, 0, 20000, -2, 0, 1000000000, -2, 0, 2000000000000000000, -2, 0, 2000000000000000000, -2, -18446744073709551618, 0, 18446744073709551616] +[0, 100, 254, 0, 20000, 65534, 0, 2000000000, 4294967294, 0, 10000000000000000000, 18446744073709551614, 0, 100, -2, 0, 20000, -2, 0, 1000000000, -2, 0, 2000000000000000000, -2, 0, 1000000000, -2, -18446744073709551618, 0, 18446744073709551616] Shift: -[0, 100, 254, 0, 20000, 65534, 0, 2000000000, 4294967294, 0, 10000000000000000000, 18446744073709551614, 0, 100, -2, 0, 20000, -2, 0, 1000000000, -2, 0, 2000000000000000000, -2, 0, 2000000000000000000, -2, -18446744073709551618, 0, 18446744073709551616] -[0, 25, 127, 0, 5000, 32767, 0, 500000000, 2147483647, 0, 2500000000000000000, 9223372036854775807, -64, 25, 63, -16384, 5000, 16383, -1073741824, 250000000, 1073741823, -4611686018427387904, 500000000000000000, 4611686018427387903, -4611686018427387904, 500000000000000000, 4611686018427387903, -4611686018427387905, 0, 4611686018427387904] +[0, 100, 254, 0, 20000, 65534, 0, 2000000000, 4294967294, 0, 10000000000000000000, 18446744073709551614, 0, 100, -2, 0, 20000, -2, 0, 1000000000, -2, 0, 2000000000000000000, -2, 0, 1000000000, -2, -18446744073709551618, 0, 18446744073709551616] +[0, 25, 127, 0, 5000, 32767, 0, 500000000, 2147483647, 0, 2500000000000000000, 9223372036854775807, -64, 25, 63, -16384, 5000, 16383, -1073741824, 250000000, 1073741823, -4611686018427387904, 500000000000000000, 4611686018427387903, -1073741824, 250000000, 1073741823, -4611686018427387905, 0, 4611686018427387904] Bit Ops: [0, 34, 170, 0, 0, 170, 0, 0, 170, 0, 0, 170, -128, 34, 42, 0, 0, 170, 0, 0, 170, 0, 0, 170, 0, 0, 170, 170, 0, 0] -[170, 186, 255, 170, 10170, 65535, 170, 1000000170, 4294967295, 170, 5000000000000000170, 18446744073709551615, -86, -70, -1, -32598, 10170, 32767, -2147483478, 500000170, 2147483647, -9223372036854775638, 1000000000000000170, 9223372036854775807, -9223372036854775638, 1000000000000000170, 9223372036854775807, -9223372036854775809, 170, 9223372036854775978] -[170, 152, 85, 170, 10170, 65365, 170, 1000000170, 4294967125, 170, 5000000000000000170, 18446744073709551445, 42, -104, -43, -32598, 10170, 32597, -2147483478, 500000170, 2147483477, -9223372036854775638, 1000000000000000170, 9223372036854775637, -9223372036854775638, 1000000000000000170, 9223372036854775637, -9223372036854775979, 170, 9223372036854775978] +[170, 186, 255, 170, 10170, 65535, 170, 1000000170, 4294967295, 170, 5000000000000000170, 18446744073709551615, -86, -70, -1, -32598, 10170, 32767, -2147483478, 500000170, 2147483647, -9223372036854775638, 1000000000000000170, 9223372036854775807, -2147483478, 500000170, 2147483647, -9223372036854775809, 170, 9223372036854775978] +[170, 152, 85, 170, 10170, 65365, 170, 1000000170, 4294967125, 170, 5000000000000000170, 18446744073709551445, 42, -104, -43, -32598, 10170, 32597, -2147483478, 500000170, 2147483477, -9223372036854775638, 1000000000000000170, 9223372036854775637, -2147483478, 500000170, 2147483477, -9223372036854775979, 170, 9223372036854775978] Comparisons: [False, False, False, False, False, False, False, False, False, False, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False] [True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, True, False] diff --git a/tests/node/newints/IntOps.idr b/tests/node/newints/IntOps.idr index 702f93ef7..78bbdc166 100644 --- a/tests/node/newints/IntOps.idr +++ b/tests/node/newints/IntOps.idr @@ -83,7 +83,7 @@ int64 : IntType Int64 int64 = intType True "Int64" 64 int : IntType Int -int = intType True "Int" 64 +int = intType True "Int" 32 record Op a where constructor MkOp diff --git a/tests/node/node015/expected b/tests/node/node015/expected index 71b75bbab..49162bd51 100644 --- a/tests/node/node015/expected +++ b/tests/node/node015/expected @@ -1,4 +1,4 @@ 1/1: Building Numbers (Numbers.idr) Main> [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339] -[8650625671965379659, -3787822715642646718, 8650625671965378905, 22945956689563340, 102] +[912198731, 301395778, 912197977, 2419624, 106] Main> Bye for now! diff --git a/tests/node/node024/BitOps.idr b/tests/node/node024/BitOps.idr index 34eeca98f..5de46998b 100644 --- a/tests/node/node024/BitOps.idr +++ b/tests/node/node024/BitOps.idr @@ -24,12 +24,11 @@ b32max = 0xffffffff b64max : Bits64 b64max = 18446744073709551615 --- the only way to create -2^63 intmin : Int -intmin = shl1 63 +intmin = -0x8000000 intmax : Int -intmax = 0x7fffffffffffffff +intmax = 0x7fffffff powsOf2 : Num a => Nat -> List a powsOf2 n = take n (iterate (*2) 1) @@ -54,10 +53,10 @@ shiftRInteger : List Integer shiftRInteger = map (`prim__shr_Integer` 1) (powsOf2 128) shiftRInt : List Int -shiftRInt = map (`prim__shr_Int` 1) (powsOf2 63 ++ [intmax]) +shiftRInt = map (`prim__shr_Int` 1) (powsOf2 31 ++ [intmax]) shiftRNegativeInt : List Int -shiftRNegativeInt = map (`prim__shr_Int` 1) (map negate (powsOf2 63) ++ [intmin]) +shiftRNegativeInt = map (`prim__shr_Int` 1) (map negate (powsOf2 31) ++ [intmin]) -------------------------------------------------------------------------------- -- shiftL @@ -79,10 +78,10 @@ shiftLInteger : List Integer shiftLInteger = map (`prim__shl_Integer` 1) (0 :: powsOf2 127) shiftLInt : List Int -shiftLInt = map (`prim__shl_Int` 1) (0 :: powsOf2 62) +shiftLInt = map (`prim__shl_Int` 1) (0 :: powsOf2 31) shiftLNegativeInt : List Int -shiftLNegativeInt = map (`prim__shl_Int` 1) (map negate (powsOf2 62)) +shiftLNegativeInt = map (`prim__shl_Int` 1) (map negate (powsOf2 31)) -------------------------------------------------------------------------------- diff --git a/tests/node/node024/expected b/tests/node/node024/expected index ea5c96346..cc59ca1e9 100644 --- a/tests/node/node024/expected +++ b/tests/node/node024/expected @@ -1,21 +1,21 @@ 1/1: Building BitOps (BitOps.idr) -Main> -9223372036854775808 +Main> -134217728 [0, 1, 2, 4, 8, 16, 32, 64, 127] [0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32767] [0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483647] [0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648, 4294967296, 8589934592, 17179869184, 34359738368, 68719476736, 137438953472, 274877906944, 549755813888, 1099511627776, 2199023255552, 4398046511104, 8796093022208, 17592186044416, 35184372088832, 70368744177664, 140737488355328, 281474976710656, 562949953421312, 1125899906842624, 2251799813685248, 4503599627370496, 9007199254740992, 18014398509481984, 36028797018963968, 72057594037927936, 144115188075855872, 288230376151711744, 576460752303423488, 1152921504606846976, 2305843009213693952, 4611686018427387904, 9223372036854775807] [0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648, 4294967296, 8589934592, 17179869184, 34359738368, 68719476736, 137438953472, 274877906944, 549755813888, 1099511627776, 2199023255552, 4398046511104, 8796093022208, 17592186044416, 35184372088832, 70368744177664, 140737488355328, 281474976710656, 562949953421312, 1125899906842624, 2251799813685248, 4503599627370496, 9007199254740992, 18014398509481984, 36028797018963968, 72057594037927936, 144115188075855872, 288230376151711744, 576460752303423488, 1152921504606846976, 2305843009213693952, 4611686018427387904, 9223372036854775808, 18446744073709551616, 36893488147419103232, 73786976294838206464, 147573952589676412928, 295147905179352825856, 590295810358705651712, 1180591620717411303424, 2361183241434822606848, 4722366482869645213696, 9444732965739290427392, 18889465931478580854784, 37778931862957161709568, 75557863725914323419136, 151115727451828646838272, 302231454903657293676544, 604462909807314587353088, 1208925819614629174706176, 2417851639229258349412352, 4835703278458516698824704, 9671406556917033397649408, 19342813113834066795298816, 38685626227668133590597632, 77371252455336267181195264, 154742504910672534362390528, 309485009821345068724781056, 618970019642690137449562112, 1237940039285380274899124224, 2475880078570760549798248448, 4951760157141521099596496896, 9903520314283042199192993792, 19807040628566084398385987584, 39614081257132168796771975168, 79228162514264337593543950336, 158456325028528675187087900672, 316912650057057350374175801344, 633825300114114700748351602688, 1267650600228229401496703205376, 2535301200456458802993406410752, 5070602400912917605986812821504, 10141204801825835211973625643008, 20282409603651670423947251286016, 40564819207303340847894502572032, 81129638414606681695789005144064, 162259276829213363391578010288128, 324518553658426726783156020576256, 649037107316853453566312041152512, 1298074214633706907132624082305024, 2596148429267413814265248164610048, 5192296858534827628530496329220096, 10384593717069655257060992658440192, 20769187434139310514121985316880384, 41538374868278621028243970633760768, 83076749736557242056487941267521536, 166153499473114484112975882535043072, 332306998946228968225951765070086144, 664613997892457936451903530140172288, 1329227995784915872903807060280344576, 2658455991569831745807614120560689152, 5316911983139663491615228241121378304, 10633823966279326983230456482242756608, 21267647932558653966460912964485513216, 42535295865117307932921825928971026432, 85070591730234615865843651857942052864] -[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648, 4294967296, 8589934592, 17179869184, 34359738368, 68719476736, 137438953472, 274877906944, 549755813888, 1099511627776, 2199023255552, 4398046511104, 8796093022208, 17592186044416, 35184372088832, 70368744177664, 140737488355328, 281474976710656, 562949953421312, 1125899906842624, 2251799813685248, 4503599627370496, 9007199254740992, 18014398509481984, 36028797018963968, 72057594037927936, 144115188075855872, 288230376151711744, 576460752303423488, 1152921504606846976, 2305843009213693952, 4611686018427387903] -[-1, -1, -2, -4, -8, -16, -32, -64, -128, -256, -512, -1024, -2048, -4096, -8192, -16384, -32768, -65536, -131072, -262144, -524288, -1048576, -2097152, -4194304, -8388608, -16777216, -33554432, -67108864, -134217728, -268435456, -536870912, -1073741824, -2147483648, -4294967296, -8589934592, -17179869184, -34359738368, -68719476736, -137438953472, -274877906944, -549755813888, -1099511627776, -2199023255552, -4398046511104, -8796093022208, -17592186044416, -35184372088832, -70368744177664, -140737488355328, -281474976710656, -562949953421312, -1125899906842624, -2251799813685248, -4503599627370496, -9007199254740992, -18014398509481984, -36028797018963968, -72057594037927936, -144115188075855872, -288230376151711744, -576460752303423488, -1152921504606846976, -2305843009213693952, -4611686018427387904] +[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741823] +[-1, -1, -2, -4, -8, -16, -32, -64, -128, -256, -512, -1024, -2048, -4096, -8192, -16384, -32768, -65536, -131072, -262144, -524288, -1048576, -2097152, -4194304, -8388608, -16777216, -33554432, -67108864, -134217728, -268435456, -536870912, -67108864] [0, 2, 4, 8, 16, 32, 64, 128] [0, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768] [0, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648] [0, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648, 4294967296, 8589934592, 17179869184, 34359738368, 68719476736, 137438953472, 274877906944, 549755813888, 1099511627776, 2199023255552, 4398046511104, 8796093022208, 17592186044416, 35184372088832, 70368744177664, 140737488355328, 281474976710656, 562949953421312, 1125899906842624, 2251799813685248, 4503599627370496, 9007199254740992, 18014398509481984, 36028797018963968, 72057594037927936, 144115188075855872, 288230376151711744, 576460752303423488, 1152921504606846976, 2305843009213693952, 4611686018427387904, 9223372036854775808] [0, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648, 4294967296, 8589934592, 17179869184, 34359738368, 68719476736, 137438953472, 274877906944, 549755813888, 1099511627776, 2199023255552, 4398046511104, 8796093022208, 17592186044416, 35184372088832, 70368744177664, 140737488355328, 281474976710656, 562949953421312, 1125899906842624, 2251799813685248, 4503599627370496, 9007199254740992, 18014398509481984, 36028797018963968, 72057594037927936, 144115188075855872, 288230376151711744, 576460752303423488, 1152921504606846976, 2305843009213693952, 4611686018427387904, 9223372036854775808, 18446744073709551616, 36893488147419103232, 73786976294838206464, 147573952589676412928, 295147905179352825856, 590295810358705651712, 1180591620717411303424, 2361183241434822606848, 4722366482869645213696, 9444732965739290427392, 18889465931478580854784, 37778931862957161709568, 75557863725914323419136, 151115727451828646838272, 302231454903657293676544, 604462909807314587353088, 1208925819614629174706176, 2417851639229258349412352, 4835703278458516698824704, 9671406556917033397649408, 19342813113834066795298816, 38685626227668133590597632, 77371252455336267181195264, 154742504910672534362390528, 309485009821345068724781056, 618970019642690137449562112, 1237940039285380274899124224, 2475880078570760549798248448, 4951760157141521099596496896, 9903520314283042199192993792, 19807040628566084398385987584, 39614081257132168796771975168, 79228162514264337593543950336, 158456325028528675187087900672, 316912650057057350374175801344, 633825300114114700748351602688, 1267650600228229401496703205376, 2535301200456458802993406410752, 5070602400912917605986812821504, 10141204801825835211973625643008, 20282409603651670423947251286016, 40564819207303340847894502572032, 81129638414606681695789005144064, 162259276829213363391578010288128, 324518553658426726783156020576256, 649037107316853453566312041152512, 1298074214633706907132624082305024, 2596148429267413814265248164610048, 5192296858534827628530496329220096, 10384593717069655257060992658440192, 20769187434139310514121985316880384, 41538374868278621028243970633760768, 83076749736557242056487941267521536, 166153499473114484112975882535043072, 332306998946228968225951765070086144, 664613997892457936451903530140172288, 1329227995784915872903807060280344576, 2658455991569831745807614120560689152, 5316911983139663491615228241121378304, 10633823966279326983230456482242756608, 21267647932558653966460912964485513216, 42535295865117307932921825928971026432, 85070591730234615865843651857942052864, 170141183460469231731687303715884105728] -[0, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648, 4294967296, 8589934592, 17179869184, 34359738368, 68719476736, 137438953472, 274877906944, 549755813888, 1099511627776, 2199023255552, 4398046511104, 8796093022208, 17592186044416, 35184372088832, 70368744177664, 140737488355328, 281474976710656, 562949953421312, 1125899906842624, 2251799813685248, 4503599627370496, 9007199254740992, 18014398509481984, 36028797018963968, 72057594037927936, 144115188075855872, 288230376151711744, 576460752303423488, 1152921504606846976, 2305843009213693952, 4611686018427387904] -[-2, -4, -8, -16, -32, -64, -128, -256, -512, -1024, -2048, -4096, -8192, -16384, -32768, -65536, -131072, -262144, -524288, -1048576, -2097152, -4194304, -8388608, -16777216, -33554432, -67108864, -134217728, -268435456, -536870912, -1073741824, -2147483648, -4294967296, -8589934592, -17179869184, -34359738368, -68719476736, -137438953472, -274877906944, -549755813888, -1099511627776, -2199023255552, -4398046511104, -8796093022208, -17592186044416, -35184372088832, -70368744177664, -140737488355328, -281474976710656, -562949953421312, -1125899906842624, -2251799813685248, -4503599627370496, -9007199254740992, -18014398509481984, -36028797018963968, -72057594037927936, -144115188075855872, -288230376151711744, -576460752303423488, -1152921504606846976, -2305843009213693952, -4611686018427387904] +[0, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, -2147483648] +[-2, -4, -8, -16, -32, -64, -128, -256, -512, -1024, -2048, -4096, -8192, -16384, -32768, -65536, -131072, -262144, -524288, -1048576, -2097152, -4194304, -8388608, -16777216, -33554432, -67108864, -134217728, -268435456, -536870912, -1073741824, -2147483648] [11, 0, 1, 2, 0, 11] [11, 0, 1, 2, 0, 11] @@ -23,14 +23,14 @@ Main> -9223372036854775808 [11, 0, 1, 2, 0, 11] [11, 0, 1, 2, 0, 11] [11, 0, 1, 2, 0, 11] -[9223372036854775797, 0, 1, 0, 4, 1, -9223372036854775808, -11, -12, -12, -11] +[2147483637, 0, 1, 0, 4, 1, -134217728, -11, -12, -12, -11] [255, 11, 11, 11, 15, 11] [65535, 11, 11, 11, 15, 11] [4294967295, 11, 11, 11, 15, 11] [18446744073709551615, 11, 11, 11, 15, 11] [340282366920938463463374607431768211455, 11, 11, 11, 15, 11] -[9223372036854775807, 11, 11, 11, 15, 11] +[2147483647, 11, 11, 11, 15, 11] [-1, -11, -11, -9, -11, -1, -11, -1, -1, -3, -11] [244, 11, 10, 9, 15, 0] @@ -38,6 +38,6 @@ Main> -9223372036854775808 [4294967284, 11, 10, 9, 15, 0] [18446744073709551604, 11, 10, 9, 15, 0] [340282366920938463463374607431768211444, 11, 10, 9, 15, 0] -[9223372036854775796, 11, 10, 9, 15, 0] -[-9223372036854775798, -11, -12, -9, -15, -2, 9223372036854775797, 10, 11, 9, 0] +[2147483636, 11, 10, 9, 15, 0] +[-2147483638, -11, -12, -9, -15, -2, 134217717, 10, 11, 9, 0] Main> Bye for now!