mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-14 22:02:07 +03:00
[ cleanup ] Add idents to some underindented stuff
This commit is contained in:
parent
c1fe44be01
commit
26b94f09f7
@ -27,22 +27,22 @@ compileToJS c tm = compileToES c Javascript tm ["browser", "javascript"]
|
||||
|
||||
htmlHeader : String
|
||||
htmlHeader = """
|
||||
<html>
|
||||
<head>
|
||||
<meta charset='utf-8'>
|
||||
</head>
|
||||
<body>
|
||||
<script type='text/javascript'>
|
||||
<html>
|
||||
<head>
|
||||
<meta charset='utf-8'>
|
||||
</head>
|
||||
<body>
|
||||
<script type='text/javascript'>
|
||||
|
||||
"""
|
||||
"""
|
||||
|
||||
htmlFooter : String
|
||||
htmlFooter = """
|
||||
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
"""
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
"""
|
||||
|
||||
addHeaderAndFooter : String -> String -> String
|
||||
addHeaderAndFooter outfile es =
|
||||
|
@ -110,11 +110,11 @@ schHeader chez libs whole
|
||||
schFooter : Bool -> Bool -> String
|
||||
schFooter prof whole = """
|
||||
|
||||
(collect 4)
|
||||
(blodwen-run-finalisers)
|
||||
\{ (if prof then "(profile-dump-html)" else "") }
|
||||
\{ (if whole then ")" else "") }
|
||||
"""
|
||||
(collect 4)
|
||||
(blodwen-run-finalisers)
|
||||
\{ (if prof then "(profile-dump-html)" else "") }
|
||||
\{ (if whole then ")" else "") }
|
||||
"""
|
||||
|
||||
showChezChar : Char -> String -> String
|
||||
showChezChar '\\' = ("\\\\" ++)
|
||||
@ -392,55 +392,55 @@ getFgnCall version (n, fc, d) = schFgnDef fc n d version
|
||||
export
|
||||
startChezPreamble : String
|
||||
startChezPreamble = #"""
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Chez") }
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Chez") }
|
||||
|
||||
set -e # exit on any error
|
||||
set -e # exit on any error
|
||||
|
||||
if [ "$(uname)" = Darwin ]; then
|
||||
DIR=$(zsh -c 'printf %s "$0:A:h"' "$0")
|
||||
else
|
||||
DIR=$(dirname "$(readlink -f -- "$0")")
|
||||
fi
|
||||
if [ "$(uname)" = Darwin ]; then
|
||||
DIR=$(zsh -c 'printf %s "$0:A:h"' "$0")
|
||||
else
|
||||
DIR=$(dirname "$(readlink -f -- "$0")")
|
||||
fi
|
||||
|
||||
"""#
|
||||
"""#
|
||||
|
||||
startChez : String -> String -> String
|
||||
startChez appdir target = startChezPreamble ++ #"""
|
||||
export LD_LIBRARY_PATH="$DIR/\#{ appdir }":$LD_LIBRARY_PATH
|
||||
export DYLD_LIBRARY_PATH="$DIR/\#{ appdir }":$DYLD_LIBRARY_PATH
|
||||
export IDRIS2_INC_SRC="$DIR/\#{ appdir }"
|
||||
export LD_LIBRARY_PATH="$DIR/\#{ appdir }":$LD_LIBRARY_PATH
|
||||
export DYLD_LIBRARY_PATH="$DIR/\#{ appdir }":$DYLD_LIBRARY_PATH
|
||||
export IDRIS2_INC_SRC="$DIR/\#{ appdir }"
|
||||
|
||||
"$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
"$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
|
||||
startChezCmd : String -> String -> String -> String
|
||||
startChezCmd chez appdir target progType = #"""
|
||||
@echo off
|
||||
@echo off
|
||||
|
||||
rem \#{ (generatedString "Chez") }
|
||||
rem \#{ (generatedString "Chez") }
|
||||
|
||||
set APPDIR=%~dp0
|
||||
set PATH=%APPDIR%\#{ appdir };%PATH%
|
||||
set IDRIS2_INC_SRC=%APPDIR%\#{ appdir }
|
||||
set APPDIR=%~dp0
|
||||
set PATH=%APPDIR%\#{ appdir };%PATH%
|
||||
set IDRIS2_INC_SRC=%APPDIR%\#{ appdir }
|
||||
|
||||
"\#{ chez }" \#{ progType } "%APPDIR%\#{ target }" %*
|
||||
"""#
|
||||
"\#{ chez }" \#{ progType } "%APPDIR%\#{ target }" %*
|
||||
"""#
|
||||
|
||||
startChezWinSh : String -> String -> String -> String
|
||||
startChezWinSh chez appdir target progType = #"""
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Chez") }
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Chez") }
|
||||
|
||||
set -e # exit on any error
|
||||
set -e # exit on any error
|
||||
|
||||
DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")")
|
||||
PATH="$DIR/\#{ appdir }":$PATH
|
||||
DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")")
|
||||
PATH="$DIR/\#{ appdir }":$PATH
|
||||
|
||||
export IDRIS2_INC_SRC="$DIR/\#{ appdir }"
|
||||
export IDRIS2_INC_SRC="$DIR/\#{ appdir }"
|
||||
|
||||
"\#{ chez }" \#{ progType } "$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
"\#{ chez }" \#{ progType } "$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
|
||||
||| Compile a TT expression to Chez Scheme
|
||||
compileToSS : Ref Ctxt Defs ->
|
||||
|
@ -50,57 +50,57 @@ schHeader libs compilationUnits = """
|
||||
\{
|
||||
unlines [" (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs]
|
||||
})
|
||||
"""
|
||||
"""
|
||||
|
||||
schFooter : String
|
||||
schFooter = """
|
||||
|
||||
(collect 4)
|
||||
(blodwen-run-finalisers)
|
||||
"""
|
||||
(collect 4)
|
||||
(blodwen-run-finalisers)
|
||||
"""
|
||||
|
||||
startChez : String -> String -> String -> String
|
||||
startChez chez appDirSh targetSh = Chez.startChezPreamble ++ #"""
|
||||
export LD_LIBRARY_PATH="$DIR/\#{ appDirSh }":$LD_LIBRARY_PATH
|
||||
export DYLD_LIBRARY_PATH="$DIR/\#{ appDirSh }":$DYLD_LIBRARY_PATH
|
||||
export LD_LIBRARY_PATH="$DIR/\#{ appDirSh }":$LD_LIBRARY_PATH
|
||||
export DYLD_LIBRARY_PATH="$DIR/\#{ appDirSh }":$DYLD_LIBRARY_PATH
|
||||
|
||||
"\#{ chez }" -q \
|
||||
--libdirs "$DIR/\#{ appDirSh }" \
|
||||
--program "$DIR/\#{ targetSh }" \
|
||||
"$@"
|
||||
"""#
|
||||
"\#{ chez }" -q \
|
||||
--libdirs "$DIR/\#{ appDirSh }" \
|
||||
--program "$DIR/\#{ targetSh }" \
|
||||
"$@"
|
||||
"""#
|
||||
|
||||
startChezCmd : String -> String -> String -> String
|
||||
startChezCmd chez appDirSh targetSh = #"""
|
||||
@echo off
|
||||
@echo off
|
||||
|
||||
rem \#{ (generatedString "ChezSep") }
|
||||
rem \#{ (generatedString "ChezSep") }
|
||||
|
||||
set APPDIR=%~dp0
|
||||
set PATH=%APPDIR%\#{ appDirSh };%PATH%
|
||||
set APPDIR=%~dp0
|
||||
set PATH=%APPDIR%\#{ appDirSh };%PATH%
|
||||
|
||||
"\#{ chez }" -q \
|
||||
--libdirs "%APPDIR%\#{ appDirSh }" \
|
||||
--program "%APPDIR%\#{ targetSh }" \
|
||||
%*
|
||||
"""#
|
||||
"\#{ chez }" -q \
|
||||
--libdirs "%APPDIR%\#{ appDirSh }" \
|
||||
--program "%APPDIR%\#{ targetSh }" \
|
||||
%*
|
||||
"""#
|
||||
|
||||
startChezWinSh : String -> String -> String -> String
|
||||
startChezWinSh chez appDirSh targetSh = #"""
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "ChezSep") }
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "ChezSep") }
|
||||
|
||||
set -e # exit on any error
|
||||
set -e # exit on any error
|
||||
|
||||
DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")")
|
||||
PATH="$DIR/\#{ appDirSh }":$PATH
|
||||
DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")")
|
||||
PATH="$DIR/\#{ appDirSh }":$PATH
|
||||
|
||||
"\#{ chez }" --program "$DIR/\#{ targetSh }" "$@"
|
||||
"\#{ chez }" -q \
|
||||
--libdirs "$DIR/\#{ appDirSh }" \
|
||||
--program "$DIR/\#{ targetSh }" \
|
||||
"$@"
|
||||
"""#
|
||||
"\#{ chez }" --program "$DIR/\#{ targetSh }" "$@"
|
||||
"\#{ chez }" -q \
|
||||
--libdirs "$DIR/\#{ appDirSh }" \
|
||||
--program "$DIR/\#{ targetSh }" \
|
||||
"$@"
|
||||
"""#
|
||||
|
||||
-- TODO: parallelise this
|
||||
compileChezLibraries : (chez : String) -> (libDir : String) -> (ssFiles : List String) -> Core ()
|
||||
|
@ -50,15 +50,15 @@ findGSCBackend =
|
||||
|
||||
schHeader : String
|
||||
schHeader = """
|
||||
;; \{ (generatedString "Gambit") }
|
||||
(declare (block)
|
||||
(inlining-limit 450)
|
||||
(standard-bindings)
|
||||
(extended-bindings)
|
||||
(not safe)
|
||||
(optimize-dead-definitions))
|
||||
;; \{ (generatedString "Gambit") }
|
||||
(declare (block)
|
||||
(inlining-limit 450)
|
||||
(standard-bindings)
|
||||
(extended-bindings)
|
||||
(not safe)
|
||||
(optimize-dead-definitions))
|
||||
|
||||
"""
|
||||
"""
|
||||
|
||||
showGambitChar : Char -> String -> String
|
||||
showGambitChar '\\' = ("\\\\" ++)
|
||||
|
@ -43,28 +43,28 @@ findRacoExe =
|
||||
|
||||
schHeader : Bool -> String -> String
|
||||
schHeader prof libs = """
|
||||
#lang racket/base
|
||||
;; \{ (generatedString "Racket") }
|
||||
(require racket/async-channel) ; for asynchronous channels
|
||||
(require racket/future) ; for parallelism/concurrency
|
||||
(require racket/math) ; for math ops
|
||||
(require racket/system) ; for system
|
||||
(require rnrs/bytevectors-6) ; for buffers
|
||||
(require rnrs/io/ports-6) ; for files
|
||||
(require srfi/19) ; for file handling and data
|
||||
(require ffi/unsafe ffi/unsafe/define) ; for calling C
|
||||
\{ (if prof then "(require profile)" else "") }
|
||||
(require racket/flonum) ; for float-typed transcendental functions
|
||||
\{ libs }
|
||||
(let ()
|
||||
#lang racket/base
|
||||
;; \{ (generatedString "Racket") }
|
||||
(require racket/async-channel) ; for asynchronous channels
|
||||
(require racket/future) ; for parallelism/concurrency
|
||||
(require racket/math) ; for math ops
|
||||
(require racket/system) ; for system
|
||||
(require rnrs/bytevectors-6) ; for buffers
|
||||
(require rnrs/io/ports-6) ; for files
|
||||
(require srfi/19) ; for file handling and data
|
||||
(require ffi/unsafe ffi/unsafe/define) ; for calling C
|
||||
\{ (if prof then "(require profile)" else "") }
|
||||
(require racket/flonum) ; for float-typed transcendental functions
|
||||
\{ libs }
|
||||
(let ()
|
||||
|
||||
"""
|
||||
"""
|
||||
|
||||
schFooter : String
|
||||
schFooter = """
|
||||
)
|
||||
(collect-garbage)
|
||||
"""
|
||||
)
|
||||
(collect-garbage)
|
||||
"""
|
||||
|
||||
showRacketChar : Char -> String -> String
|
||||
showRacketChar '\\' = ("\\\\" ++)
|
||||
@ -336,47 +336,47 @@ getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d
|
||||
|
||||
startRacket : String -> String -> String -> String
|
||||
startRacket racket appdir target = #"""
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Racket") }
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Racket") }
|
||||
|
||||
set -e # exit on any error
|
||||
set -e # exit on any error
|
||||
|
||||
if [ "$(uname)" = Darwin ]; then
|
||||
DIR=$(zsh -c 'printf %s "$0:A:h"' "$0")
|
||||
else
|
||||
DIR=$(dirname "$(readlink -f -- "$0")")
|
||||
fi
|
||||
if [ "$(uname)" = Darwin ]; then
|
||||
DIR=$(zsh -c 'printf %s "$0:A:h"' "$0")
|
||||
else
|
||||
DIR=$(dirname "$(readlink -f -- "$0")")
|
||||
fi
|
||||
|
||||
export LD_LIBRARY_PATH="$DIR/\#{ appdir }":$LD_LIBRARY_PATH
|
||||
export DYLD_LIBRARY_PATH="$DIR/\#{ appdir }":$DYLD_LIBRARY_PATH
|
||||
export LD_LIBRARY_PATH="$DIR/\#{ appdir }":$LD_LIBRARY_PATH
|
||||
export DYLD_LIBRARY_PATH="$DIR/\#{ appdir }":$DYLD_LIBRARY_PATH
|
||||
|
||||
\#{ racket } "$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
\#{ racket } "$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
|
||||
startRacketCmd : String -> String -> String -> String
|
||||
startRacketCmd racket appdir target = #"""
|
||||
@echo off
|
||||
@echo off
|
||||
|
||||
rem \#{ (generatedString "Racket") }
|
||||
rem \#{ (generatedString "Racket") }
|
||||
|
||||
set APPDIR=%~dp0
|
||||
set PATH=%APPDIR%\#{ appdir };%PATH%
|
||||
set APPDIR=%~dp0
|
||||
set PATH=%APPDIR%\#{ appdir };%PATH%
|
||||
|
||||
\#{ racket } "%APPDIR%\#{ target }" %*
|
||||
"""#
|
||||
\#{ racket } "%APPDIR%\#{ target }" %*
|
||||
"""#
|
||||
|
||||
startRacketWinSh : String -> String -> String -> String
|
||||
startRacketWinSh racket appdir target = #"""
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Racket") }
|
||||
#!/bin/sh
|
||||
# \#{ (generatedString "Racket") }
|
||||
|
||||
set -e # exit on any error
|
||||
set -e # exit on any error
|
||||
|
||||
DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")")
|
||||
PATH="$DIR/\#{ appdir }":$PATH
|
||||
DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")")
|
||||
PATH="$DIR/\#{ appdir }":$PATH
|
||||
|
||||
\#{ racket } "$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
\#{ racket } "$DIR/\#{ target }" "$@"
|
||||
"""#
|
||||
|
||||
compileToRKT : Ref Ctxt Defs ->
|
||||
String -> ClosedTerm -> (outfile : String) -> Core ()
|
||||
|
@ -403,15 +403,15 @@ versionMsg = "Idris 2, version " ++ show version
|
||||
export
|
||||
usage : String
|
||||
usage = """
|
||||
\{ versionMsg }
|
||||
Usage: idris2 [options] [input file]
|
||||
\{ versionMsg }
|
||||
Usage: idris2 [options] [input file]
|
||||
|
||||
Available options:
|
||||
\{ optsUsage }
|
||||
Available options:
|
||||
\{ optsUsage }
|
||||
|
||||
Environment variables:
|
||||
\{ envsUsage }
|
||||
"""
|
||||
Environment variables:
|
||||
\{ envsUsage }
|
||||
"""
|
||||
|
||||
checkNat : Integer -> Maybe Nat
|
||||
checkNat n = toMaybe (n >= 0) (integerToNat n)
|
||||
|
@ -133,14 +133,14 @@ tryTTM (c :: cs) = tryTTM cs
|
||||
|
||||
banner : String
|
||||
banner = #"""
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version \#{ showVersion True version }
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version \#{ showVersion True version }
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
|
||||
Welcome to Idris 2. Enjoy yourself!
|
||||
"""#
|
||||
Welcome to Idris 2. Enjoy yourself!
|
||||
"""#
|
||||
|
||||
checkVerbose : List CLOpt -> Bool
|
||||
checkVerbose [] = False
|
||||
|
@ -780,22 +780,22 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts
|
||||
|
||||
errorMsg : String
|
||||
errorMsg = """
|
||||
Not all command line options can be used to override package options.
|
||||
Not all command line options can be used to override package options.
|
||||
|
||||
Overridable options are:
|
||||
--quiet
|
||||
--verbose
|
||||
--timing
|
||||
--log <log level>
|
||||
--dumpcases <file>
|
||||
--dumplifted <file>
|
||||
--dumpvmcode <file>
|
||||
--debug-elab-check
|
||||
--codegen <cg>
|
||||
--directive <directive>
|
||||
--build-dir <dir>
|
||||
--output-dir <dir>
|
||||
"""
|
||||
Overridable options are:
|
||||
--quiet
|
||||
--verbose
|
||||
--timing
|
||||
--log <log level>
|
||||
--dumpcases <file>
|
||||
--dumplifted <file>
|
||||
--dumpvmcode <file>
|
||||
--debug-elab-check
|
||||
--codegen <cg>
|
||||
--directive <directive>
|
||||
--build-dir <dir>
|
||||
--output-dir <dir>
|
||||
"""
|
||||
|
||||
export
|
||||
processPackageOpts : {auto c : Ref Ctxt Defs} ->
|
||||
|
@ -249,14 +249,14 @@ opts x _ = pure $ if (x `elem` optionFlags)
|
||||
-- bash autocompletion script using the given function name
|
||||
completionScript : (fun : String) -> String
|
||||
completionScript fun = let fun' = "_" ++ fun in #"""
|
||||
\#{ fun' }()
|
||||
{
|
||||
ED=$([ -z $2 ] && echo "--" || echo $2)
|
||||
COMPREPLY=($(idris2 --bash-completion $ED $3))
|
||||
}
|
||||
\#{ fun' }()
|
||||
{
|
||||
ED=$([ -z $2 ] && echo "--" || echo $2)
|
||||
COMPREPLY=($(idris2 --bash-completion $ED $3))
|
||||
}
|
||||
|
||||
complete -F \#{ fun' } -o default idris2
|
||||
"""#
|
||||
complete -F \#{ fun' } -o default idris2
|
||||
"""#
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Processing Options
|
||||
|
Loading…
Reference in New Issue
Block a user