mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
[ new ] Add chez-sep
codegen (#1359)
Co-authored-by: Johann Rudloff <johann@sinyax.net>
This commit is contained in:
parent
1db440d3cf
commit
4de7b2133a
@ -35,6 +35,15 @@ Compiler changes:
|
||||
than `Number.MAX_SAFE_INTEGER`. `Bits32` goes via `BigInt` for
|
||||
multiplication for the same reason as well as for all bitops, since `Number`
|
||||
uses signed 32 bit integers for those.
|
||||
* New code generator: `chez-sep`. This code generator produces many Chez Scheme
|
||||
files and compiles them separately instead of producing one huge Scheme
|
||||
program. This significantly reduces the amount of memory needed to build
|
||||
large programs. Since this backend will skip calling the Chez compiler on
|
||||
modules that haven't changed, it also leads to shorter compilation times in
|
||||
large codebases where only some files have changed -- for example when
|
||||
developing Idris2 code generators. The codegen has a large parallelisation
|
||||
potential but at the moment, it is significantly slower for a full rebuild of
|
||||
a large code base (the code generation stage takes about 3x longer).
|
||||
|
||||
Library changes:
|
||||
|
||||
|
5
Makefile
5
Makefile
@ -116,10 +116,12 @@ test: testenv
|
||||
support:
|
||||
@${MAKE} -C support/c
|
||||
@${MAKE} -C support/refc
|
||||
@${MAKE} -C support/chez
|
||||
|
||||
support-clean:
|
||||
@${MAKE} -C support/c clean
|
||||
@${MAKE} -C support/refc clean
|
||||
@${MAKE} -C support/chez clean
|
||||
|
||||
clean-libs:
|
||||
${MAKE} -C libs/prelude clean
|
||||
@ -151,18 +153,17 @@ endif
|
||||
install ${TARGETDIR}/${NAME}_app/* ${PREFIX}/bin/${NAME}_app
|
||||
|
||||
install-support:
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/chez
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/docs
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/racket
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/gambit
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/js
|
||||
install support/chez/* ${PREFIX}/${NAME_VERSION}/support/chez
|
||||
install support/docs/* ${PREFIX}/${NAME_VERSION}/support/docs
|
||||
install support/racket/* ${PREFIX}/${NAME_VERSION}/support/racket
|
||||
install support/gambit/* ${PREFIX}/${NAME_VERSION}/support/gambit
|
||||
install support/js/* ${PREFIX}/${NAME_VERSION}/support/js
|
||||
@${MAKE} -C support/c install
|
||||
@${MAKE} -C support/refc install
|
||||
@${MAKE} -C support/chez install
|
||||
|
||||
install-libs:
|
||||
${MAKE} -C libs/prelude install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
|
@ -13,6 +13,7 @@ modules =
|
||||
Compiler.CompileExpr,
|
||||
Compiler.Inline,
|
||||
Compiler.LambdaLift,
|
||||
Compiler.Separate,
|
||||
Compiler.VMCode,
|
||||
|
||||
Compiler.ES.ES,
|
||||
@ -27,6 +28,7 @@ modules =
|
||||
Compiler.RefC.RefC,
|
||||
|
||||
Compiler.Scheme.Chez,
|
||||
Compiler.Scheme.ChezSep,
|
||||
Compiler.Scheme.Racket,
|
||||
Compiler.Scheme.Gambit,
|
||||
Compiler.Scheme.Common,
|
||||
|
@ -30,6 +30,7 @@ import System.Info
|
||||
|
||||
%default covering
|
||||
|
||||
export
|
||||
findChez : IO String
|
||||
findChez
|
||||
= do Nothing <- idrisGetEnv "CHEZ"
|
||||
@ -43,6 +44,7 @@ findChez
|
||||
-- of the library paths managed by Idris
|
||||
-- If it can't be found, we'll assume it's a system library and that chez
|
||||
-- will thus be able to find it.
|
||||
export
|
||||
findLibs : {auto c : Ref Ctxt Defs} ->
|
||||
List String -> Core (List (String, String))
|
||||
findLibs ds
|
||||
@ -55,7 +57,7 @@ findLibs ds
|
||||
then Just (trim (substr 3 (length d) d))
|
||||
else Nothing
|
||||
|
||||
|
||||
export
|
||||
escapeString : String -> String
|
||||
escapeString s = pack $ foldr escape [] $ unpack s
|
||||
where
|
||||
@ -97,6 +99,7 @@ showChezString [] = id
|
||||
showChezString ('"'::cs) = ("\\\"" ++) . showChezString cs
|
||||
showChezString (c ::cs) = (showChezChar c) . showChezString cs
|
||||
|
||||
export
|
||||
chezString : String -> String
|
||||
chezString cs = strCons '"' (showChezString (unpack cs) "\"")
|
||||
|
||||
@ -129,6 +132,7 @@ mutual
|
||||
getFArgs (NmCon fc _ _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
|
||||
getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg))
|
||||
|
||||
export
|
||||
chezExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String
|
||||
chezExtPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
|
||||
NmPrimVal _ (Str fld), _]
|
||||
@ -162,9 +166,11 @@ mutual
|
||||
= schExtCommon chezExtPrim chezString i prim args
|
||||
|
||||
-- Reference label for keeping track of loaded external libraries
|
||||
export
|
||||
data Loaded : Type where
|
||||
|
||||
-- Label for noting which struct types are declared
|
||||
export
|
||||
data Structs : Type where
|
||||
|
||||
cftySpec : FC -> CFType -> Core String
|
||||
@ -328,14 +334,16 @@ schFgnDef appdir fc n (MkNmForeign cs args ret)
|
||||
body ++ "))\n")
|
||||
schFgnDef _ _ _ _ = pure ("", "")
|
||||
|
||||
export
|
||||
getFgnCall : {auto c : Ref Ctxt Defs} ->
|
||||
{auto l : Ref Loaded (List String)} ->
|
||||
{auto s : Ref Structs (List String)} ->
|
||||
String -> (Name, FC, NamedDef) -> Core (String, String)
|
||||
getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d
|
||||
|
||||
startChez : String -> String -> String
|
||||
startChez appdir target = unlines
|
||||
export
|
||||
startChezPreamble : String
|
||||
startChezPreamble = unlines
|
||||
[ "#!/bin/sh"
|
||||
, ""
|
||||
, "set -e # exit on any error"
|
||||
@ -356,7 +364,12 @@ startChez appdir target = unlines
|
||||
, "fi "
|
||||
, ""
|
||||
, "DIR=$(dirname \"$($REALPATH \"$0\")\")"
|
||||
, "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ "\":$LD_LIBRARY_PATH"
|
||||
, "" -- so that the preamble ends with a newline
|
||||
]
|
||||
|
||||
startChez : String -> String -> String
|
||||
startChez appdir target = startChezPreamble ++ unlines
|
||||
[ "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ "\":$LD_LIBRARY_PATH"
|
||||
, "\"$DIR/" ++ target ++ "\" \"$@\""
|
||||
]
|
||||
|
||||
|
310
src/Compiler/Scheme/ChezSep.idr
Normal file
310
src/Compiler/Scheme/ChezSep.idr
Normal file
@ -0,0 +1,310 @@
|
||||
module Compiler.Scheme.ChezSep
|
||||
|
||||
import Compiler.Common
|
||||
import Compiler.CompileExpr
|
||||
import Compiler.Inline
|
||||
import Compiler.Scheme.Common
|
||||
import Compiler.Scheme.Chez
|
||||
import Compiler.Separate
|
||||
|
||||
import Core.Core
|
||||
import Core.Hash
|
||||
import Core.Context
|
||||
import Core.Context.Log
|
||||
import Core.Directory
|
||||
import Core.Name
|
||||
import Core.Options
|
||||
import Core.TT
|
||||
import Libraries.Utils.Hex
|
||||
import Libraries.Utils.Path
|
||||
|
||||
import Data.List
|
||||
import Data.List1
|
||||
import Data.Maybe
|
||||
import Libraries.Data.NameMap
|
||||
import Data.Strings
|
||||
import Data.Vect
|
||||
|
||||
import Idris.Env
|
||||
|
||||
import System
|
||||
import System.Directory
|
||||
import System.File
|
||||
import System.Info
|
||||
|
||||
%default covering
|
||||
|
||||
schHeader : List String -> List String -> String
|
||||
schHeader libs compilationUnits = unlines
|
||||
[ "(import (chezscheme) (support) "
|
||||
++ unwords ["(" ++ cu ++ ")" | cu <- compilationUnits]
|
||||
++ ")"
|
||||
, "(case (machine-type)"
|
||||
, " [(i3le ti3le a6le ta6le) (load-shared-object \"libc.so.6\")]"
|
||||
, " [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]"
|
||||
, " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")"
|
||||
, " (load-shared-object \"ws2_32.dll\")]"
|
||||
, " [else (load-shared-object \"libc.so\")]"
|
||||
, unlines [" (load-shared-object \"" ++ escapeString lib ++ "\")" | lib <- libs]
|
||||
, ")"
|
||||
]
|
||||
|
||||
schFooter : String
|
||||
schFooter = "(collect 4)\n(blodwen-run-finalisers)\n"
|
||||
|
||||
startChez : String -> String -> String -> String
|
||||
startChez chez appDirSh targetSh = Chez.startChezPreamble ++ unlines
|
||||
[ "export LD_LIBRARY_PATH=\"$DIR/" ++ appDirSh ++ "\":$LD_LIBRARY_PATH"
|
||||
, "\"" ++ chez ++ "\" -q "
|
||||
++ "--libdirs \"$DIR/" ++ appDirSh ++ "\" "
|
||||
++ "--program \"$DIR/" ++ targetSh ++ "\" "
|
||||
++ "\"$@\""
|
||||
]
|
||||
|
||||
startChezCmd : String -> String -> String -> String
|
||||
startChezCmd chez appDirSh targetSh = unlines
|
||||
[ "@echo off"
|
||||
, "set APPDIR=%~dp0"
|
||||
, "set PATH=%APPDIR%\\" ++ appDirSh ++ ";%PATH%"
|
||||
, "\"" ++ chez ++ "\" -q "
|
||||
++ "--libdirs \"%APPDIR%/" ++ appDirSh ++ "\" "
|
||||
++ "--program \"%APPDIR%/" ++ targetSh ++ "\" "
|
||||
++ "%*"
|
||||
]
|
||||
|
||||
startChezWinSh : String -> String -> String -> String
|
||||
startChezWinSh chez appDirSh targetSh = unlines
|
||||
[ "#!/bin/sh"
|
||||
, ""
|
||||
, "set -e # exit on any error"
|
||||
, ""
|
||||
, "DIR=$(dirname \"$(realpath \"$0\")\")"
|
||||
, "CHEZ=$(cygpath \"" ++ chez ++"\")"
|
||||
, "export PATH=\"$DIR/" ++ appDirSh ++ "\":$PATH"
|
||||
, "\"$CHEZ\" --program \"$DIR/" ++ targetSh ++ "\" \"$@\""
|
||||
, "\"$CHEZ\" -q "
|
||||
++ "--libdirs \"$DIR/" ++ appDirSh ++ "\" "
|
||||
++ "--program \"$DIR/" ++ targetSh ++ "\" "
|
||||
++ "\"$@\""
|
||||
]
|
||||
|
||||
-- TODO: parallelise this
|
||||
compileChezLibraries : (chez : String) -> (libDir : String) -> (ssFiles : List String) -> Core ()
|
||||
compileChezLibraries chez libDir ssFiles = coreLift_ $ system $ unwords
|
||||
[ "echo"
|
||||
, unwords
|
||||
[ "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-library " ++ chezString ssFile ++ "))'"
|
||||
++ " '(delete-file " ++ chezString ssFile ++ ")'"
|
||||
-- we must delete the SS file to prevent it from interfering with the SO files
|
||||
-- we keep the .hash file, though, so we still keep track of what to rebuild
|
||||
| ssFile <- ssFiles
|
||||
]
|
||||
, "|", chez, "-q", "--libdirs", libDir
|
||||
]
|
||||
|
||||
compileChezLibrary : (chez : String) -> (libDir : String) -> (ssFile : String) -> Core ()
|
||||
compileChezLibrary chez libDir ssFile = coreLift_ $ system $ unwords
|
||||
[ "echo"
|
||||
, "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-library " ++ chezString ssFile ++ "))'"
|
||||
, "'(delete-file " ++ chezString ssFile ++ ")'"
|
||||
, "|", chez, "-q", "--libdirs", libDir
|
||||
]
|
||||
|
||||
compileChezProgram : (chez : String) -> (libDir : String) -> (ssFile : String) -> Core ()
|
||||
compileChezProgram chez libDir ssFile = coreLift_ $ system $ unwords
|
||||
[ "echo"
|
||||
, "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-program " ++ chezString ssFile ++ "))'"
|
||||
, "'(delete-file " ++ chezString ssFile ++ ")'"
|
||||
, "|", chez, "-q", "--libdirs", libDir
|
||||
]
|
||||
|
||||
chezNS : Namespace -> String
|
||||
chezNS ns = case showNSWithSep "-" ns of
|
||||
"" => "unqualified"
|
||||
nss => nss
|
||||
|
||||
-- arbitrarily name the compilation unit
|
||||
-- after the alphabetically first namespace contained within
|
||||
chezLibraryName : CompilationUnit def -> String
|
||||
chezLibraryName cu = chezNS (min1 cu.namespaces)
|
||||
where
|
||||
-- the stdlib of the previous stable version
|
||||
-- has some strange version of List1.foldl1
|
||||
-- so we reimplement it here for compatibility
|
||||
min1 : List1 Namespace -> Namespace
|
||||
min1 (ns ::: nss) = foldl min ns nss
|
||||
|
||||
-- TODO: use a proper exec function without shell injection
|
||||
touch : String -> Core ()
|
||||
touch s = coreLift_ $ system ("touch \"" ++ s ++ "\"")
|
||||
|
||||
record ChezLib where
|
||||
constructor MkChezLib
|
||||
name : String
|
||||
isOutdated : Bool -- needs recompiling
|
||||
|
||||
||| Compile a TT expression to a bunch of Chez Scheme files
|
||||
compileToSS : Ref Ctxt Defs -> String -> String -> ClosedTerm -> Core (Bool, List ChezLib)
|
||||
compileToSS c chez appdir tm = do
|
||||
-- process native libraries
|
||||
ds <- getDirectives Chez
|
||||
libs <- findLibs ds
|
||||
traverse_ copyLib libs
|
||||
|
||||
-- get the material for compilation
|
||||
cdata <- getCompileData False Cases tm
|
||||
let ctm = forget (mainExpr cdata)
|
||||
let ndefs = namedDefs cdata
|
||||
let cui = getCompilationUnits ndefs
|
||||
|
||||
-- copy the support library
|
||||
support <- readDataFile "chez/support-sep.ss"
|
||||
let supportHash = show $ hash support
|
||||
supportChanged <-
|
||||
coreLift (File.readFile (appdir </> "support.hash")) >>= \case
|
||||
Left err => pure True
|
||||
Right fileHash => pure (fileHash /= supportHash)
|
||||
when supportChanged $ do
|
||||
Core.writeFile (appdir </> "support.ss") support
|
||||
Core.writeFile (appdir </> "support.hash") supportHash
|
||||
|
||||
-- TODO: add extraRuntime
|
||||
-- the problem with this is that it's unclear what to put in the (export) clause of the library
|
||||
-- extraRuntime <- getExtraRuntime ds
|
||||
|
||||
-- for each compilation unit, generate code
|
||||
chezLibs <- for cui.compilationUnits $ \cu => do
|
||||
let chezLib = chezLibraryName cu
|
||||
|
||||
-- check if the hash has changed
|
||||
-- TODO: also check that the .so file exists
|
||||
let cuHash = show (hash cu)
|
||||
hashChanged <-
|
||||
coreLift (File.readFile (appdir </> chezLib <.> "hash")) >>= \case
|
||||
Left err => pure True
|
||||
Right fileHash => pure (fileHash /= cuHash)
|
||||
|
||||
-- generate code only when necessary
|
||||
when hashChanged $ do
|
||||
defs <- get Ctxt
|
||||
l <- newRef {t = List String} Loaded ["libc", "libc 6"]
|
||||
s <- newRef {t = List String} Structs []
|
||||
|
||||
-- create imports + exports + header + footer
|
||||
let imports = unwords
|
||||
[ "(" ++
|
||||
maybe
|
||||
"unqualified"
|
||||
chezLibraryName
|
||||
(SortedMap.lookup cuid cui.byId)
|
||||
++ ")"
|
||||
| cuid <- SortedSet.toList cu.dependencies
|
||||
]
|
||||
let exports = unwords $ concat
|
||||
-- constructors don't generate Scheme definitions
|
||||
[ case d of
|
||||
MkNmCon _ _ _ => []
|
||||
_ => [schName dn]
|
||||
| (dn, fc, d) <- cu.definitions
|
||||
]
|
||||
let header =
|
||||
"(library (" ++ chezLib ++ ")\n"
|
||||
++ " (export " ++ exports ++ ")\n"
|
||||
++ " (import (chezscheme) (support) " ++ imports ++ ")\n\n"
|
||||
let footer = ")"
|
||||
|
||||
fgndefs <- traverse (Chez.getFgnCall appdir) cu.definitions
|
||||
compdefs <- traverse (getScheme Chez.chezExtPrim Chez.chezString) cu.definitions
|
||||
|
||||
-- write the files
|
||||
log "compiler.scheme.chez" 3 $ "Generating code for " ++ chezLib
|
||||
Core.writeFile (appdir </> chezLib <.> "ss") $ fastAppend $
|
||||
[header]
|
||||
++ map snd fgndefs -- definitions using foreign libs
|
||||
++ compdefs
|
||||
++ map fst fgndefs -- foreign library load statements
|
||||
++ [footer]
|
||||
|
||||
Core.writeFile (appdir </> chezLib <.> "hash") cuHash
|
||||
|
||||
pure (MkChezLib chezLib hashChanged)
|
||||
|
||||
-- main module
|
||||
main <- schExp Chez.chezExtPrim Chez.chezString 0 ctm
|
||||
Core.writeFile (appdir </> "mainprog.ss") $ unlines $
|
||||
[ schHeader (map snd libs) [lib.name | lib <- chezLibs]
|
||||
, "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))"
|
||||
, main
|
||||
, schFooter
|
||||
]
|
||||
|
||||
pure (supportChanged, chezLibs)
|
||||
|
||||
makeSh : String -> String -> String -> String -> Core ()
|
||||
makeSh chez outShRel appDirSh targetSh =
|
||||
Core.writeFile outShRel (startChez chez appDirSh targetSh)
|
||||
|
||||
||| Make Windows start scripts, one for bash environments and one batch file
|
||||
makeShWindows : String -> String -> String -> String -> Core ()
|
||||
makeShWindows chez outShRel appDirSh targetSh = do
|
||||
let cmdFile = outShRel ++ ".cmd"
|
||||
Core.writeFile cmdFile (startChezCmd chez appDirSh targetSh)
|
||||
Core.writeFile outShRel (startChezWinSh chez appDirSh targetSh)
|
||||
|
||||
||| Chez Scheme implementation of the `compileExpr` interface.
|
||||
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
|
||||
ClosedTerm -> (outfile : String) -> Core (Maybe String)
|
||||
compileExpr makeitso c tmpDir outputDir tm outfile = do
|
||||
-- set up paths
|
||||
Just cwd <- coreLift currentDir
|
||||
| Nothing => throw (InternalError "Can't get current directory")
|
||||
let appDirSh = outfile ++ "_app" -- relative to the launcher shell script
|
||||
let appDirRel = outputDir </> appDirSh -- relative to CWD
|
||||
let appDirAbs = cwd </> appDirRel
|
||||
coreLift_ $ mkdirAll appDirRel
|
||||
|
||||
-- generate the code
|
||||
chez <- coreLift $ findChez
|
||||
(supportChanged, chezLibs) <- compileToSS c chez appDirRel tm
|
||||
|
||||
-- compile the code
|
||||
logTime "++ Make SO" $ when makeitso $ do
|
||||
-- compile the support code
|
||||
when supportChanged $ do
|
||||
log "compiler.scheme.chez" 3 $ "Compiling support"
|
||||
compileChezLibrary chez appDirRel (appDirRel </> "support.ss")
|
||||
|
||||
-- compile every compilation unit
|
||||
compileChezLibraries chez appDirRel
|
||||
[appDirRel </> lib.name <.> "ss" | lib <- chezLibs, lib.isOutdated]
|
||||
|
||||
-- touch them in the right order to make the timestamps right
|
||||
-- even for the libraries that were not recompiled
|
||||
for_ chezLibs $ \lib => do
|
||||
log "compiler.scheme.chez" 3 $ "Touching " ++ lib.name
|
||||
touch (appDirRel </> lib.name <.> "so")
|
||||
|
||||
-- compile the main program
|
||||
compileChezProgram chez appDirRel (appDirRel </> "mainprog.ss")
|
||||
|
||||
-- generate the launch script
|
||||
let outShRel = outputDir </> outfile
|
||||
let launchTargetSh = appDirSh </> "mainprog" <.> (if makeitso then "so" else "ss")
|
||||
if isWindows
|
||||
then makeShWindows chez outShRel appDirSh launchTargetSh
|
||||
else makeSh chez outShRel appDirSh launchTargetSh
|
||||
coreLift_ $ chmodRaw outShRel 0o755
|
||||
pure (Just outShRel)
|
||||
|
||||
||| Chez Scheme implementation of the `executeExpr` interface.
|
||||
||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it.
|
||||
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
|
||||
executeExpr c tmpDir tm
|
||||
= do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
|
||||
| Nothing => throw (InternalError "compileExpr returned Nothing")
|
||||
coreLift_ $ system sh
|
||||
|
||||
||| Codegen wrapper for Chez scheme implementation.
|
||||
export
|
||||
codegenChezSep : Codegen
|
||||
codegenChezSep = MkCG (compileExpr True) executeExpr
|
345
src/Compiler/Separate.idr
Normal file
345
src/Compiler/Separate.idr
Normal file
@ -0,0 +1,345 @@
|
||||
module Compiler.Separate
|
||||
|
||||
import public Core.FC
|
||||
import public Core.Name
|
||||
import public Core.Name.Namespace
|
||||
import public Core.CompileExpr
|
||||
import public Compiler.VMCode
|
||||
import public Libraries.Data.SortedMap
|
||||
import public Libraries.Data.SortedSet
|
||||
import public Libraries.Data.StringMap
|
||||
|
||||
import Core.Hash
|
||||
import Core.TT
|
||||
import Data.List
|
||||
import Data.List1
|
||||
import Data.Vect
|
||||
import Data.Maybe
|
||||
|
||||
-- Compilation unit IDs are intended to be opaque,
|
||||
-- just to be able to express dependencies via keys in a map and such.
|
||||
export
|
||||
record CompilationUnitId where
|
||||
constructor CUID
|
||||
int : Int
|
||||
|
||||
export
|
||||
Eq CompilationUnitId where
|
||||
CUID x == CUID y = x == y
|
||||
|
||||
export
|
||||
Ord CompilationUnitId where
|
||||
compare (CUID x) (CUID y) = compare x y
|
||||
|
||||
export
|
||||
Hashable CompilationUnitId where
|
||||
hashWithSalt h (CUID int) = hashWithSalt h int
|
||||
|
||||
||| A compilation unit is a set of namespaces.
|
||||
|||
|
||||
||| The record is parameterised by the type of the definition,
|
||||
||| which makes it reusable for various IRs provided by getCompileData.
|
||||
public export
|
||||
record CompilationUnit def where
|
||||
constructor MkCompilationUnit
|
||||
|
||||
||| Unique identifier of a compilation unit within a CompilationUnitInfo record.
|
||||
id : CompilationUnitId
|
||||
|
||||
||| Namespaces contained within the compilation unit.
|
||||
namespaces : List1 Namespace
|
||||
|
||||
||| Other units that this unit depends on.
|
||||
dependencies : SortedSet CompilationUnitId
|
||||
|
||||
||| The definitions belonging into this compilation unit.
|
||||
definitions : List (Name, def)
|
||||
|
||||
export
|
||||
Hashable def => Hashable (CompilationUnit def) where
|
||||
hashWithSalt h cu =
|
||||
h `hashWithSalt` SortedSet.toList cu.dependencies
|
||||
`hashWithSalt` cu.definitions
|
||||
|
||||
private
|
||||
getNS : Name -> Namespace
|
||||
getNS (NS ns _) = ns
|
||||
getNS _ = emptyNS
|
||||
|
||||
||| Group definitions by namespace.
|
||||
private
|
||||
splitByNS : List (Name, def) -> List (Namespace, List (Name, def))
|
||||
splitByNS = SortedMap.toList . foldl addOne SortedMap.empty
|
||||
where
|
||||
addOne
|
||||
: SortedMap Namespace (List (Name, def))
|
||||
-> (Name, def)
|
||||
-> SortedMap Namespace (List (Name, def))
|
||||
addOne nss ndef@(n, _) =
|
||||
SortedMap.mergeWith
|
||||
(++)
|
||||
(SortedMap.singleton (getNS n) [ndef])
|
||||
nss
|
||||
|
||||
-- Mechanically transcribed from
|
||||
-- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode
|
||||
namespace Tarjan
|
||||
private
|
||||
record TarjanVertex where
|
||||
constructor TV
|
||||
index : Int
|
||||
lowlink : Int
|
||||
inStack : Bool
|
||||
|
||||
private
|
||||
record TarjanState cuid where
|
||||
constructor TS
|
||||
vertices : SortedMap cuid TarjanVertex
|
||||
stack : List cuid
|
||||
nextIndex : Int
|
||||
components : List (List1 cuid)
|
||||
impossibleHappened : Bool -- we should get at least some indication of broken assumptions
|
||||
|
||||
||| Find strongly connected components in the given graph.
|
||||
|||
|
||||
||| Input: map from vertex X to all vertices Y such that there is edge X->Y
|
||||
||| Output: list of strongly connected components, ordered by output degree descending
|
||||
export
|
||||
tarjan : Ord cuid => SortedMap cuid (SortedSet cuid) -> List (List1 cuid)
|
||||
tarjan {cuid} deps = loop initialState (SortedMap.keys deps)
|
||||
where
|
||||
initialState : TarjanState cuid
|
||||
initialState =
|
||||
TS
|
||||
SortedMap.empty
|
||||
[]
|
||||
0
|
||||
[]
|
||||
False
|
||||
|
||||
strongConnect : TarjanState cuid -> cuid -> TarjanState cuid
|
||||
strongConnect ts v =
|
||||
let ts'' = case SortedMap.lookup v deps of
|
||||
Nothing => ts' -- no edges
|
||||
Just edgeSet => loop ts' (SortedSet.toList edgeSet)
|
||||
in case SortedMap.lookup v ts''.vertices of
|
||||
Nothing => record { impossibleHappened = True } ts''
|
||||
Just vtv =>
|
||||
if vtv.index == vtv.lowlink
|
||||
then createComponent ts'' v []
|
||||
else ts''
|
||||
where
|
||||
createComponent : TarjanState cuid -> cuid -> List cuid -> TarjanState cuid
|
||||
createComponent ts v acc =
|
||||
case ts.stack of
|
||||
[] => record { impossibleHappened = True } ts
|
||||
w :: ws =>
|
||||
let ts' : TarjanState cuid = record {
|
||||
vertices $= SortedMap.adjust w record{ inStack = False },
|
||||
stack = ws
|
||||
} ts
|
||||
in if w == v
|
||||
then record { components $= ((v ::: acc) ::) } ts' -- that's it
|
||||
else createComponent ts' v (w :: acc)
|
||||
|
||||
loop : TarjanState cuid -> List cuid -> TarjanState cuid
|
||||
loop ts [] = ts
|
||||
loop ts (w :: ws) =
|
||||
loop (
|
||||
case SortedMap.lookup w ts.vertices of
|
||||
Nothing => let ts' = strongConnect ts w in
|
||||
case SortedMap.lookup w ts'.vertices of
|
||||
Nothing => record { impossibleHappened = True } ts'
|
||||
Just wtv => record { vertices $= SortedMap.adjust v record{ lowlink $= min wtv.lowlink } } ts'
|
||||
|
||||
Just wtv => case wtv.inStack of
|
||||
False => ts -- nothing to do
|
||||
True => record { vertices $= SortedMap.adjust v record{ lowlink $= min wtv.index } } ts
|
||||
) ws
|
||||
|
||||
ts' : TarjanState cuid
|
||||
ts' = record {
|
||||
vertices $= SortedMap.insert v (TV ts.nextIndex ts.nextIndex True),
|
||||
stack $= (v ::),
|
||||
nextIndex $= (1+)
|
||||
} ts
|
||||
|
||||
loop : TarjanState cuid -> List cuid -> List (List1 cuid)
|
||||
loop ts [] =
|
||||
if ts.impossibleHappened
|
||||
then []
|
||||
else ts.components
|
||||
loop ts (v :: vs) =
|
||||
case SortedMap.lookup v ts.vertices of
|
||||
Just _ => loop ts vs -- done, skip
|
||||
Nothing => loop (strongConnect ts v) vs
|
||||
|
||||
public export
|
||||
interface HasNamespaces a where
|
||||
||| Return the set of namespaces mentioned within
|
||||
nsRefs : a -> SortedSet Namespace
|
||||
|
||||
-- For now, we have instances only for NamedDef and VMDef.
|
||||
-- For other IR representations, we'll have to add more instances.
|
||||
-- This is not hard, just a bit of tedious mechanical work.
|
||||
mutual
|
||||
export
|
||||
HasNamespaces NamedCExp where
|
||||
nsRefs (NmLocal fc n) = SortedSet.empty
|
||||
nsRefs (NmRef fc n) = SortedSet.singleton $ getNS n
|
||||
nsRefs (NmLam fc n rhs) = nsRefs rhs
|
||||
nsRefs (NmLet fc n val rhs) = nsRefs val <+> nsRefs rhs
|
||||
nsRefs (NmApp fc f args) = nsRefs f <+> concatMap nsRefs args
|
||||
nsRefs (NmCon fc cn ci tag args) = concatMap nsRefs args
|
||||
nsRefs (NmForce fc reason rhs) = nsRefs rhs
|
||||
nsRefs (NmDelay fc reason rhs) = nsRefs rhs
|
||||
nsRefs (NmErased fc) = SortedSet.empty
|
||||
nsRefs (NmPrimVal ft x) = SortedSet.empty
|
||||
nsRefs (NmOp fc op args) = concatMap nsRefs args
|
||||
nsRefs (NmExtPrim fc n args) = concatMap nsRefs args
|
||||
nsRefs (NmConCase fc scrut alts mbDflt) =
|
||||
nsRefs scrut <+> concatMap nsRefs alts <+> concatMap nsRefs mbDflt
|
||||
nsRefs (NmConstCase fc scrut alts mbDflt) =
|
||||
nsRefs scrut <+> concatMap nsRefs alts <+> concatMap nsRefs mbDflt
|
||||
nsRefs (NmCrash fc msg) = SortedSet.empty
|
||||
|
||||
export
|
||||
HasNamespaces NamedConAlt where
|
||||
nsRefs (MkNConAlt n ci tag args rhs) = nsRefs rhs
|
||||
|
||||
export
|
||||
HasNamespaces NamedConstAlt where
|
||||
nsRefs (MkNConstAlt c rhs) = nsRefs rhs
|
||||
|
||||
export
|
||||
HasNamespaces NamedDef where
|
||||
nsRefs (MkNmFun argNs rhs) = nsRefs rhs
|
||||
nsRefs (MkNmCon tag arity nt) = SortedSet.empty
|
||||
nsRefs (MkNmForeign ccs fargs rty) = SortedSet.empty
|
||||
nsRefs (MkNmError rhs) = nsRefs rhs
|
||||
|
||||
export
|
||||
HasNamespaces VMInst where
|
||||
nsRefs (DECLARE x) = empty
|
||||
nsRefs START = empty
|
||||
nsRefs (ASSIGN x y) = empty
|
||||
nsRefs (MKCON x tag args) = either (const empty) (singleton . getNS) tag
|
||||
nsRefs (MKCLOSURE x n missing args) = singleton $ getNS n
|
||||
nsRefs (MKCONSTANT x y) = empty
|
||||
nsRefs (APPLY x f a) = empty
|
||||
nsRefs (CALL x tailpos n args) = singleton $ getNS n
|
||||
nsRefs (OP x y xs) = empty
|
||||
nsRefs (EXTPRIM x n xs) = singleton $ getNS n
|
||||
nsRefs (CASE x alts def) =
|
||||
maybe empty (concatMap nsRefs) def <+>
|
||||
concatMap ((concatMap nsRefs) . snd) alts <+>
|
||||
concatMap ((either (const empty) (singleton . getNS)) . fst) alts
|
||||
nsRefs (CONSTCASE x alts def) =
|
||||
maybe empty (concatMap nsRefs) def <+>
|
||||
concatMap ((concatMap nsRefs) . snd) alts
|
||||
nsRefs (PROJECT x value pos) = empty
|
||||
nsRefs (NULL x) = empty
|
||||
nsRefs (ERROR x) = empty
|
||||
|
||||
export
|
||||
HasNamespaces VMDef where
|
||||
nsRefs (MkVMFun args is) = concatMap nsRefs is
|
||||
nsRefs (MkVMError is) = concatMap nsRefs is
|
||||
|
||||
|
||||
-- a slight hack for convenient use with CompileData.namedDefs
|
||||
export
|
||||
HasNamespaces a => HasNamespaces (FC, a) where
|
||||
nsRefs (_, x) = nsRefs x
|
||||
|
||||
-- another slight hack for convenient use with CompileData.namedDefs
|
||||
export
|
||||
Hashable def => Hashable (FC, def) where
|
||||
-- ignore FC in hash, like everywhere else
|
||||
hashWithSalt h (fc, x) = hashWithSalt h x
|
||||
|
||||
||| Output of the codegen separation algorithm.
|
||||
||| Should contain everything you need in a separately compiling codegen.
|
||||
public export
|
||||
record CompilationUnitInfo def where
|
||||
constructor MkCompilationUnitInfo
|
||||
|
||||
||| Compilation units computed from the given definitions,
|
||||
||| ordered topologically, starting from units depending on no other unit.
|
||||
compilationUnits : List (CompilationUnit def)
|
||||
|
||||
||| Mapping from ID to CompilationUnit.
|
||||
byId : SortedMap CompilationUnitId (CompilationUnit def)
|
||||
|
||||
||| Maps each namespace to the compilation unit that contains it.
|
||||
namespaceMap : SortedMap Namespace CompilationUnitId
|
||||
|
||||
||| Group the given definitions into compilation units for separate code generation.
|
||||
export
|
||||
getCompilationUnits : HasNamespaces def => List (Name, def) -> CompilationUnitInfo def
|
||||
getCompilationUnits {def} defs =
|
||||
let
|
||||
-- Definitions grouped by namespace.
|
||||
defsByNS : SortedMap Namespace (List (Name, def))
|
||||
= SortedMap.fromList $ splitByNS defs
|
||||
|
||||
-- Mapping from a namespace to all namespaces mentioned within.
|
||||
-- Represents graph edges pointing in that direction.
|
||||
nsDeps : SortedMap Namespace (SortedSet Namespace)
|
||||
= foldl (SortedMap.mergeWith SortedSet.union) SortedMap.empty
|
||||
[ SortedMap.singleton (getNS n) (SortedSet.delete (getNS n) (nsRefs d))
|
||||
| (n, d) <- defs
|
||||
]
|
||||
|
||||
-- Strongly connected components of the NS dep graph,
|
||||
-- ordered by output degree ascending.
|
||||
--
|
||||
-- Each SCC will become a compilation unit.
|
||||
components : List (List1 Namespace)
|
||||
= List.reverse $ tarjan nsDeps -- tarjan generates reverse toposort
|
||||
|
||||
-- Maps a namespace to the compilation unit that contains it.
|
||||
nsMap : SortedMap Namespace CompilationUnitId
|
||||
= SortedMap.fromList [(ns, cuid) | (cuid, nss) <- withCUID components, ns <- List1.forget nss]
|
||||
|
||||
-- List of all compilation units, ordered by number of dependencies, ascending.
|
||||
units : List (CompilationUnit def)
|
||||
= [mkUnit nsDeps nsMap defsByNS cuid nss | (cuid, nss) <- withCUID components]
|
||||
|
||||
in MkCompilationUnitInfo
|
||||
{ compilationUnits = units
|
||||
, byId = SortedMap.fromList [(unit.id, unit) | unit <- units]
|
||||
, namespaceMap = nsMap
|
||||
}
|
||||
|
||||
where
|
||||
withCUID : List a -> List (CompilationUnitId, a)
|
||||
withCUID xs = [(CUID $ cast i, x) | (i, x) <- zip [0..length xs] xs]
|
||||
|
||||
||| Wrap all information in a compilation unit record.
|
||||
mkUnit :
|
||||
SortedMap Namespace (SortedSet Namespace)
|
||||
-> SortedMap Namespace CompilationUnitId
|
||||
-> SortedMap Namespace (List (Name, def))
|
||||
-> CompilationUnitId -> List1 Namespace -> CompilationUnit def
|
||||
mkUnit nsDeps nsMap defsByNS cuid nss =
|
||||
MkCompilationUnit
|
||||
{ id = cuid
|
||||
, namespaces = nss
|
||||
, dependencies = SortedSet.delete cuid dependencies
|
||||
, definitions = definitions
|
||||
}
|
||||
where
|
||||
dependencies : SortedSet CompilationUnitId
|
||||
dependencies = SortedSet.fromList $ do
|
||||
ns <- List1.forget nss -- NS contained within
|
||||
depsNS <- SortedSet.toList $ -- NS we depend on
|
||||
fromMaybe SortedSet.empty $
|
||||
SortedMap.lookup ns nsDeps
|
||||
|
||||
case SortedMap.lookup depsNS nsMap of
|
||||
Nothing => []
|
||||
Just depCUID => [depCUID]
|
||||
|
||||
definitions : List (Name, def)
|
||||
definitions = concat [fromMaybe [] $ SortedMap.lookup ns defsByNS | ns <- nss]
|
@ -31,7 +31,7 @@ import Data.Buffer
|
||||
-- TTC files can only be compatible if the version number is the same
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 50
|
||||
ttcVersion = 51
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
|
@ -619,6 +619,10 @@ traverse_ f [] = pure ()
|
||||
traverse_ f (x :: xs)
|
||||
= Core.do ignore (f x)
|
||||
traverse_ f xs
|
||||
%inline
|
||||
export
|
||||
for_ : List a -> (a -> Core ()) -> Core ()
|
||||
for_ = flip traverse_
|
||||
|
||||
%inline
|
||||
export
|
||||
@ -751,3 +755,18 @@ condC : List (Core Bool, Core a) -> Core a -> Core a
|
||||
condC [] def = def
|
||||
condC ((x, y) :: xs) def
|
||||
= if !x then y else condC xs def
|
||||
|
||||
export
|
||||
writeFile : (fname : String) -> (content : String) -> Core ()
|
||||
writeFile fname content =
|
||||
coreLift (File.writeFile fname content) >>= \case
|
||||
Right () => pure ()
|
||||
Left err => throw $ FileErr fname err
|
||||
|
||||
export
|
||||
readFile : (fname : String) -> Core String
|
||||
readFile fname =
|
||||
coreLift (File.readFile fname) >>= \case
|
||||
Right content => pure content
|
||||
Left err => throw $ FileErr fname err
|
||||
|
||||
|
@ -2,12 +2,14 @@ module Core.Hash
|
||||
|
||||
import Core.CaseTree
|
||||
import Core.TT
|
||||
import Core.CompileExpr
|
||||
|
||||
import Data.List
|
||||
import Data.List1
|
||||
import Libraries.Data.List.Lazy
|
||||
import Data.Strings
|
||||
import Libraries.Data.String.Iterator
|
||||
import Data.Vect
|
||||
|
||||
%default covering
|
||||
|
||||
@ -42,6 +44,11 @@ export
|
||||
Hashable Char where
|
||||
hash = cast
|
||||
|
||||
export
|
||||
Hashable a => Hashable (Vect n a) where
|
||||
hashWithSalt h [] = abs h
|
||||
hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
|
||||
|
||||
export
|
||||
Hashable a => Hashable (List a) where
|
||||
hashWithSalt h [] = abs h
|
||||
@ -56,10 +63,18 @@ Hashable a => Hashable (Maybe a) where
|
||||
hashWithSalt h Nothing = abs h
|
||||
hashWithSalt h (Just x) = hashWithSalt h x
|
||||
|
||||
export
|
||||
Hashable a => Hashable b => Hashable (a, b) where
|
||||
hashWithSalt h (x, y) = h `hashWithSalt` x `hashWithSalt` y
|
||||
|
||||
export
|
||||
Hashable String where
|
||||
hashWithSalt h = String.Iterator.foldl hashWithSalt h
|
||||
|
||||
export
|
||||
Hashable Double where
|
||||
hash = hash . show
|
||||
|
||||
export
|
||||
Hashable Namespace where
|
||||
hashWithSalt h ns = hashWithSalt h (unsafeUnfoldNamespace ns)
|
||||
@ -174,3 +189,256 @@ mutual
|
||||
= h `hashWithSalt` 3 `hashWithSalt` (show x) `hashWithSalt` y
|
||||
hashWithSalt h (DefaultCase x)
|
||||
= h `hashWithSalt` 4 `hashWithSalt` x
|
||||
|
||||
export
|
||||
Hashable CFType where
|
||||
hashWithSalt h = \case
|
||||
CFUnit =>
|
||||
h `hashWithSalt` 0
|
||||
CFInt =>
|
||||
h `hashWithSalt` 1
|
||||
CFUnsigned8 =>
|
||||
h `hashWithSalt` 2
|
||||
CFUnsigned16 =>
|
||||
h `hashWithSalt` 3
|
||||
CFUnsigned32 =>
|
||||
h `hashWithSalt` 4
|
||||
CFUnsigned64 =>
|
||||
h `hashWithSalt` 5
|
||||
CFString =>
|
||||
h `hashWithSalt` 6
|
||||
CFDouble =>
|
||||
h `hashWithSalt` 7
|
||||
CFChar =>
|
||||
h `hashWithSalt` 8
|
||||
CFPtr =>
|
||||
h `hashWithSalt` 9
|
||||
CFGCPtr =>
|
||||
h `hashWithSalt` 10
|
||||
CFBuffer =>
|
||||
h `hashWithSalt` 11
|
||||
CFWorld =>
|
||||
h `hashWithSalt` 12
|
||||
CFFun a b =>
|
||||
h `hashWithSalt` 13 `hashWithSalt` a `hashWithSalt` b
|
||||
CFIORes a =>
|
||||
h `hashWithSalt` 14 `hashWithSalt` a
|
||||
CFStruct n fs =>
|
||||
h `hashWithSalt` 15 `hashWithSalt` n `hashWithSalt` fs
|
||||
CFUser n xs =>
|
||||
h `hashWithSalt` 16 `hashWithSalt` n `hashWithSalt` xs
|
||||
|
||||
export
|
||||
Hashable Constant where
|
||||
hashWithSalt h = \case
|
||||
I i =>
|
||||
h `hashWithSalt` 0 `hashWithSalt` i
|
||||
BI x =>
|
||||
h `hashWithSalt` 1 `hashWithSalt` x
|
||||
B8 x =>
|
||||
h `hashWithSalt` 2 `hashWithSalt` x
|
||||
B16 x =>
|
||||
h `hashWithSalt` 3 `hashWithSalt` x
|
||||
B32 x =>
|
||||
h `hashWithSalt` 4 `hashWithSalt` x
|
||||
B64 x =>
|
||||
h `hashWithSalt` 5 `hashWithSalt` x
|
||||
Str x =>
|
||||
h `hashWithSalt` 6 `hashWithSalt` x
|
||||
Ch x =>
|
||||
h `hashWithSalt` 7 `hashWithSalt` x
|
||||
Db x =>
|
||||
h `hashWithSalt` 8 `hashWithSalt` x
|
||||
|
||||
WorldVal =>
|
||||
h `hashWithSalt` 9
|
||||
|
||||
IntType =>
|
||||
h `hashWithSalt` 10
|
||||
IntegerType =>
|
||||
h `hashWithSalt` 11
|
||||
Bits8Type =>
|
||||
h `hashWithSalt` 12
|
||||
Bits16Type =>
|
||||
h `hashWithSalt` 13
|
||||
Bits32Type =>
|
||||
h `hashWithSalt` 14
|
||||
Bits64Type =>
|
||||
h `hashWithSalt` 15
|
||||
StringType =>
|
||||
h `hashWithSalt` 16
|
||||
CharType =>
|
||||
h `hashWithSalt` 17
|
||||
DoubleType =>
|
||||
h `hashWithSalt` 18
|
||||
WorldType =>
|
||||
h `hashWithSalt` 19
|
||||
|
||||
I8 x => h `hashWithSalt` 20 `hashWithSalt` x
|
||||
I16 x => h `hashWithSalt` 21 `hashWithSalt` x
|
||||
I32 x => h `hashWithSalt` 22 `hashWithSalt` x
|
||||
I64 x => h `hashWithSalt` 23 `hashWithSalt` x
|
||||
|
||||
Int8Type => h `hashWithSalt` 24
|
||||
Int16Type => h `hashWithSalt` 25
|
||||
Int32Type => h `hashWithSalt` 26
|
||||
Int64Type => h `hashWithSalt` 27
|
||||
|
||||
export
|
||||
Hashable LazyReason where
|
||||
hashWithSalt h = \case
|
||||
LInf => h `hashWithSalt` 0
|
||||
LLazy => h `hashWithSalt` 1
|
||||
LUnknown => h `hashWithSalt` 2
|
||||
|
||||
export
|
||||
Hashable (PrimFn arity) where
|
||||
hashWithSalt h = \case
|
||||
Add ty =>
|
||||
h `hashWithSalt` 0 `hashWithSalt` ty
|
||||
Sub ty =>
|
||||
h `hashWithSalt` 1 `hashWithSalt` ty
|
||||
Mul ty =>
|
||||
h `hashWithSalt` 2 `hashWithSalt` ty
|
||||
Div ty =>
|
||||
h `hashWithSalt` 3 `hashWithSalt` ty
|
||||
Mod ty =>
|
||||
h `hashWithSalt` 4 `hashWithSalt` ty
|
||||
Neg ty =>
|
||||
h `hashWithSalt` 5 `hashWithSalt` ty
|
||||
ShiftL ty =>
|
||||
h `hashWithSalt` 6 `hashWithSalt` ty
|
||||
ShiftR ty =>
|
||||
h `hashWithSalt` 7 `hashWithSalt` ty
|
||||
|
||||
BAnd ty =>
|
||||
h `hashWithSalt` 8 `hashWithSalt` ty
|
||||
BOr ty =>
|
||||
h `hashWithSalt` 9 `hashWithSalt` ty
|
||||
BXOr ty =>
|
||||
h `hashWithSalt` 10 `hashWithSalt` ty
|
||||
|
||||
LT ty =>
|
||||
h `hashWithSalt` 11 `hashWithSalt` ty
|
||||
LTE ty =>
|
||||
h `hashWithSalt` 12 `hashWithSalt` ty
|
||||
EQ ty =>
|
||||
h `hashWithSalt` 13 `hashWithSalt` ty
|
||||
GTE ty =>
|
||||
h `hashWithSalt` 14 `hashWithSalt` ty
|
||||
GT ty =>
|
||||
h `hashWithSalt` 15 `hashWithSalt` ty
|
||||
|
||||
StrLength =>
|
||||
h `hashWithSalt` 16
|
||||
StrHead =>
|
||||
h `hashWithSalt` 17
|
||||
StrTail =>
|
||||
h `hashWithSalt` 18
|
||||
StrIndex =>
|
||||
h `hashWithSalt` 19
|
||||
StrCons =>
|
||||
h `hashWithSalt` 20
|
||||
StrAppend =>
|
||||
h `hashWithSalt` 21
|
||||
StrReverse =>
|
||||
h `hashWithSalt` 22
|
||||
StrSubstr =>
|
||||
h `hashWithSalt` 23
|
||||
|
||||
DoubleExp =>
|
||||
h `hashWithSalt` 24
|
||||
DoubleLog =>
|
||||
h `hashWithSalt` 25
|
||||
DoubleSin =>
|
||||
h `hashWithSalt` 26
|
||||
DoubleCos =>
|
||||
h `hashWithSalt` 27
|
||||
DoubleTan =>
|
||||
h `hashWithSalt` 28
|
||||
DoubleASin =>
|
||||
h `hashWithSalt` 29
|
||||
DoubleACos =>
|
||||
h `hashWithSalt` 30
|
||||
DoubleATan =>
|
||||
h `hashWithSalt` 31
|
||||
DoubleSqrt =>
|
||||
h `hashWithSalt` 32
|
||||
DoubleFloor =>
|
||||
h `hashWithSalt` 33
|
||||
DoubleCeiling =>
|
||||
h `hashWithSalt` 34
|
||||
|
||||
Cast f t =>
|
||||
h `hashWithSalt` 35 `hashWithSalt` f `hashWithSalt` t
|
||||
BelieveMe =>
|
||||
h `hashWithSalt` 36
|
||||
Crash =>
|
||||
h `hashWithSalt` 37
|
||||
|
||||
export
|
||||
Hashable ConInfo where
|
||||
hashWithSalt h = \case
|
||||
DATACON => h `hashWithSalt` 0
|
||||
TYCON => h `hashWithSalt` 1
|
||||
NIL => h `hashWithSalt` 2
|
||||
CONS => h `hashWithSalt` 3
|
||||
ENUM => h `hashWithSalt` 4
|
||||
|
||||
|
||||
mutual
|
||||
export
|
||||
Hashable NamedCExp where
|
||||
hashWithSalt h = \case
|
||||
NmLocal fc n =>
|
||||
h `hashWithSalt` 0 `hashWithSalt` n
|
||||
NmRef fc n =>
|
||||
h `hashWithSalt` 1 `hashWithSalt` n
|
||||
NmLam fc x rhs =>
|
||||
h `hashWithSalt` 2 `hashWithSalt` x `hashWithSalt` rhs
|
||||
NmLet fc x val rhs =>
|
||||
h `hashWithSalt` 3 `hashWithSalt` x `hashWithSalt` val `hashWithSalt` rhs
|
||||
NmApp fc f xs =>
|
||||
h `hashWithSalt` 4 `hashWithSalt` f `hashWithSalt` xs
|
||||
NmCon fc cn ci t args =>
|
||||
h `hashWithSalt` 5 `hashWithSalt` cn `hashWithSalt` ci `hashWithSalt` t `hashWithSalt` args
|
||||
NmOp fc fn args =>
|
||||
h `hashWithSalt` 6 `hashWithSalt` fn `hashWithSalt` args
|
||||
NmExtPrim fc p args =>
|
||||
h `hashWithSalt` 7 `hashWithSalt` p `hashWithSalt` args
|
||||
NmForce fc r x =>
|
||||
h `hashWithSalt` 8 `hashWithSalt` r `hashWithSalt` x
|
||||
NmDelay fc r x =>
|
||||
h `hashWithSalt` 9 `hashWithSalt` r `hashWithSalt` x
|
||||
NmConCase fc sc alts df =>
|
||||
h `hashWithSalt` 10 `hashWithSalt` sc `hashWithSalt` alts `hashWithSalt` df
|
||||
NmConstCase fc sc alts df =>
|
||||
h `hashWithSalt` 11 `hashWithSalt` sc `hashWithSalt` alts `hashWithSalt` df
|
||||
NmPrimVal fc c =>
|
||||
h `hashWithSalt` 12 `hashWithSalt` c
|
||||
NmErased fc =>
|
||||
h `hashWithSalt` 13
|
||||
NmCrash fc msg =>
|
||||
h `hashWithSalt` 14 `hashWithSalt` msg
|
||||
|
||||
export
|
||||
Hashable NamedConAlt where
|
||||
hashWithSalt h (MkNConAlt n ci tag args rhs) =
|
||||
h `hashWithSalt` n `hashWithSalt` ci `hashWithSalt` tag `hashWithSalt` args `hashWithSalt` rhs
|
||||
|
||||
export
|
||||
Hashable NamedConstAlt where
|
||||
hashWithSalt h (MkNConstAlt c rhs) =
|
||||
h `hashWithSalt` c `hashWithSalt` rhs
|
||||
|
||||
export
|
||||
Hashable NamedDef where
|
||||
hashWithSalt h = \case
|
||||
MkNmFun args ce =>
|
||||
h `hashWithSalt` 0 `hashWithSalt` args `hashWithSalt` ce
|
||||
MkNmCon tag arity nt =>
|
||||
h `hashWithSalt` 1 `hashWithSalt` tag `hashWithSalt` arity `hashWithSalt` nt
|
||||
MkNmForeign ccs fargs cft =>
|
||||
h `hashWithSalt` 2 `hashWithSalt` ccs `hashWithSalt` fargs `hashWithSalt` cft
|
||||
MkNmError e =>
|
||||
h `hashWithSalt` 3 `hashWithSalt` e
|
||||
|
@ -53,6 +53,7 @@ toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) =
|
||||
|
||||
public export
|
||||
data CG = Chez
|
||||
| ChezSep
|
||||
| Racket
|
||||
| Gambit
|
||||
| Node
|
||||
@ -63,6 +64,7 @@ data CG = Chez
|
||||
export
|
||||
Eq CG where
|
||||
Chez == Chez = True
|
||||
ChezSep == ChezSep = True
|
||||
Racket == Racket = True
|
||||
Gambit == Gambit = True
|
||||
Node == Node = True
|
||||
@ -74,6 +76,7 @@ Eq CG where
|
||||
export
|
||||
Show CG where
|
||||
show Chez = "chez"
|
||||
show ChezSep = "chez-sep"
|
||||
show Racket = "racket"
|
||||
show Gambit = "gambit"
|
||||
show Node = "node"
|
||||
@ -180,6 +183,7 @@ export
|
||||
availableCGs : Options -> List (String, CG)
|
||||
availableCGs o
|
||||
= [("chez", Chez),
|
||||
("chez-sep", ChezSep),
|
||||
("racket", Racket),
|
||||
("node", Node),
|
||||
("javascript", Javascript),
|
||||
|
@ -788,6 +788,7 @@ TTC CDef where
|
||||
export
|
||||
TTC CG where
|
||||
toBuf b Chez = tag 0
|
||||
toBuf b ChezSep = tag 1
|
||||
toBuf b Racket = tag 2
|
||||
toBuf b Gambit = tag 3
|
||||
toBuf b (Other s) = do tag 4; toBuf b s
|
||||
@ -798,6 +799,7 @@ TTC CG where
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
0 => pure Chez
|
||||
1 => pure ChezSep
|
||||
2 => pure Racket
|
||||
3 => pure Gambit
|
||||
4 => do s <- fromBuf b
|
||||
|
@ -1,6 +1,7 @@
|
||||
module Idris.REPL
|
||||
|
||||
import Compiler.Scheme.Chez
|
||||
import Compiler.Scheme.ChezSep
|
||||
import Compiler.Scheme.Racket
|
||||
import Compiler.Scheme.Gambit
|
||||
import Compiler.ES.Node
|
||||
@ -211,6 +212,7 @@ findCG
|
||||
= do defs <- get Ctxt
|
||||
case codegen (session (options defs)) of
|
||||
Chez => pure codegenChez
|
||||
ChezSep => pure codegenChezSep
|
||||
Racket => pure codegenRacket
|
||||
Gambit => pure codegenGambit
|
||||
Node => pure codegenNode
|
||||
|
@ -314,6 +314,13 @@ export
|
||||
mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v
|
||||
mergeLeft = mergeWith const
|
||||
|
||||
export
|
||||
adjust : k -> (v -> v) -> SortedMap k v -> SortedMap k v
|
||||
adjust k f m =
|
||||
case lookup k m of
|
||||
Nothing => m
|
||||
Just v => insert k (f v) m
|
||||
|
||||
export
|
||||
(Show k, Show v) => Show (SortedMap k v) where
|
||||
show m = "fromList " ++ (show $ toList m)
|
||||
|
1
support/chez/.gitignore
vendored
Normal file
1
support/chez/.gitignore
vendored
Normal file
@ -0,0 +1 @@
|
||||
support-sep.ss
|
30
support/chez/Makefile
Normal file
30
support/chez/Makefile
Normal file
@ -0,0 +1,30 @@
|
||||
include ../../config.mk
|
||||
|
||||
all: build
|
||||
|
||||
clean:
|
||||
-$(RM) support-sep.ss
|
||||
|
||||
.PHONY: install build
|
||||
|
||||
build: support-sep.ss
|
||||
|
||||
install: build
|
||||
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
|
||||
install *.ss ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
|
||||
|
||||
support-sep.ss: support.ss
|
||||
# start library header
|
||||
echo "(library (support) (export" > $@
|
||||
|
||||
# print the list of exports
|
||||
cat support.ss \
|
||||
| sed -n 's|(define (\?\([^ )]*\).*|\1|p' \
|
||||
>> $@
|
||||
echo ") (import (chezscheme))" >> $@
|
||||
|
||||
# copy the code
|
||||
cat $< >> $@
|
||||
|
||||
# close the bracket
|
||||
echo ") ; end of (library)" >> $@
|
@ -1,5 +1,5 @@
|
||||
Error: The given specifier was not accepted by any backend. Available backends:
|
||||
chez, racket, node, javascript, refc, gambit
|
||||
chez, chez-sep, racket, node, javascript, refc, gambit
|
||||
Some backends have additional specifier rules, refer to their documentation.
|
||||
|
||||
Specifiers.idr:29:1--30:35
|
||||
@ -7,7 +7,7 @@ Specifiers.idr:29:1--30:35
|
||||
30 | plusRacketFail : Int -> Int -> Int
|
||||
|
||||
Error: The given specifier was not accepted by any backend. Available backends:
|
||||
chez, racket, node, javascript, refc, gambit
|
||||
chez, chez-sep, racket, node, javascript, refc, gambit
|
||||
Some backends have additional specifier rules, refer to their documentation.
|
||||
|
||||
Specifiers.idr:29:1--30:35
|
||||
@ -16,13 +16,13 @@ Specifiers.idr:29:1--30:35
|
||||
|
||||
Main> Loaded file Specifiers.idr
|
||||
Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
|
||||
chez, racket, node, javascript, refc, gambit
|
||||
chez, chez-sep, racket, node, javascript, refc, gambit
|
||||
Some backends have additional specifier rules, refer to their documentation.
|
||||
|
||||
Specifiers.idr:29:1--30:35
|
||||
|
||||
Specifiers> [exec] Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
|
||||
chez, racket, node, javascript, refc, gambit
|
||||
chez, chez-sep, racket, node, javascript, refc, gambit
|
||||
Some backends have additional specifier rules, refer to their documentation.
|
||||
|
||||
Specifiers.idr:29:1--30:35
|
||||
|
Loading…
Reference in New Issue
Block a user