From c1fe44be01c3a10641451483d64bfbc98d8ac860 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Fri, 25 Jun 2021 18:23:47 +0600 Subject: [PATCH 1/9] [refactor] Use multiline strings for better readability --- src/Compiler/ES/Javascript.idr | 28 +++---- src/Compiler/RefC/RefC.idr | 42 +++++----- src/Compiler/Scheme/Chez.idr | 131 ++++++++++++++++++-------------- src/Compiler/Scheme/ChezSep.idr | 99 +++++++++++++----------- src/Compiler/Scheme/Gambit.idr | 18 +++-- src/Compiler/Scheme/Racket.idr | 107 ++++++++++++++------------ src/Core/Metadata.idr | 25 +++--- src/Core/Options.idr | 23 +++--- src/Idris/CommandLine.idr | 17 +++-- src/Idris/Driver.idr | 16 ++-- src/Idris/Package.idr | 33 ++++---- src/Idris/SetOptions.idr | 19 +++-- 12 files changed, 300 insertions(+), 258 deletions(-) diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index ac70fed96..ca82ab931 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -26,21 +26,23 @@ compileToJS : Ref Ctxt Defs -> compileToJS c tm = compileToES c Javascript tm ["browser", "javascript"] htmlHeader : String -htmlHeader = concat $ the (List String) $ - [ "\n" - , " \n" - , " \n" - , " \n" - , " \n" - , " \n" - , " \n" - , "" - ] +htmlFooter = """ + + + + +""" addHeaderAndFooter : String -> String -> String addHeaderAndFooter outfile es = diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 5b12cc11a..9bb6d80ff 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -452,9 +452,6 @@ const2Integer c i = _ => i - - - -- we return for each of the ANF a set of statements and two possible return statements -- The first one for non-tail statements, the second one for tail statements -- this way, we can deal with tail calls and tail recursion. @@ -545,7 +542,6 @@ mutual constBlockSwitch alts retValVar (i+1) - constDefaultBlock : {auto a : Ref ArgCounter Nat} -> {auto t : Ref TemporaryVariableTracker (List (List String))} -> {auto oft : Ref OutfileText Output} @@ -566,7 +562,6 @@ mutual emit EmptyFC " }" - makeNonIntSwitchStatementConst : {auto a : Ref ArgCounter Nat} -> {auto t : Ref TemporaryVariableTracker (List (List String))} @@ -729,9 +724,6 @@ mutual pure $ MkRS "NULL" "NULL" - - - addCommaToList : List String -> List String addCommaToList [] = [] addCommaToList (x :: xs) = (" " ++ x) :: map (", " ++) xs @@ -989,29 +981,35 @@ header : {auto c : Ref Ctxt Defs} -> {auto h : Ref HeaderFiles (SortedSet String)} -> Core () header = do - let initLines = [ "#include " - , "/* " ++ (generatedString "RefC") ++" */"] + let initLines = """ + #include + /* \{ (generatedString "RefC") } */ + + """ let headerFiles = Libraries.Data.SortedSet.toList !(get HeaderFiles) let headerLines = map (\h => "#include <" ++ h ++ ">\n") headerFiles fns <- get FunctionDefinitions - update OutfileText (appendL (initLines ++ headerLines ++ ["\n// function definitions"] ++ fns)) + update OutfileText (appendL ([initLines] ++ headerLines ++ ["\n// function definitions"] ++ fns)) footer : {auto il : Ref IndentLevel Nat} -> {auto f : Ref OutfileText Output} -> {auto h : Ref HeaderFiles (SortedSet String)} -> Core () footer = do - emit EmptyFC "" - emit EmptyFC " // main function" - emit EmptyFC "int main(int argc, char *argv[])" - emit EmptyFC "{" - if contains "idris_support.h" !(get HeaderFiles) - then emit EmptyFC " idris2_setArgs(argc, argv);" - else pure () - emit EmptyFC " Value *mainExprVal = __mainExpression_0();" - emit EmptyFC " trampoline(mainExprVal);" - emit EmptyFC " return 0; // bye bye" - emit EmptyFC "}" + emit EmptyFC """ + + // main function + int main(int argc, char *argv[]) + { + \{ + (if contains "idris_support.h" !(get HeaderFiles) + then "idris2_setArgs(argc, argv);" else "") + } + Value *mainExprVal = __mainExpression_0(); + trampoline(mainExprVal); + return 0; // bye bye + } + """ export executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core () diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 4ea9922d5..3522b1d31 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -87,28 +87,34 @@ schHeader : String -> List String -> Bool -> String schHeader chez libs whole = (if os /= "windows" then "#!" ++ chez ++ (if whole then " --program\n\n" else " --script\n\n") - else "") ++ - "; " ++ (generatedString "Chez") ++ "\n" ++ - "(import (chezscheme))\n" ++ - "(case (machine-type)\n" ++ - " [(i3fb ti3fb a6fb ta6fb) #f]\n" ++ - " [(i3le ti3le a6le ta6le tarm64le) (load-shared-object \"libc.so.6\")]\n" ++ - " [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object \"libc.dylib\")]\n" ++ - " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++ - " [else (load-shared-object \"libc.so\")])\n\n" ++ - showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) ++ "\n\n" ++ - if whole - then "(let ()\n" - else "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") (source-directories)))\n" + else "") ++ """ + ;; \{ (generatedString "Chez") } + (import (chezscheme)) + (case (machine-type) + [(i3fb ti3fb a6fb ta6fb) #f] + [(i3le ti3le a6le ta6le tarm64le) (load-shared-object "libc.so.6")] + [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object "libc.dylib")] + [(i3nt ti3nt a6nt ta6nt) (load-shared-object "msvcrt.dll")] + [else (load-shared-object "libc.so")]) + + \{ showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) } + + \{ + (if whole + then "(let ()" + else "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") (source-directories)))") + } + + """ schFooter : Bool -> Bool -> String -schFooter prof whole - = "(collect 4)\n(blodwen-run-finalisers)\n" ++ - (if prof - then "(profile-dump-html)" - else "") ++ - (if whole - then ")\n" else "\n") +schFooter prof whole = """ + + (collect 4) + (blodwen-run-finalisers) + \{ (if prof then "(profile-dump-html)" else "") } + \{ (if whole then ")" else "") } +""" showChezChar : Char -> String -> String showChezChar '\\' = ("\\\\" ++) @@ -385,49 +391,56 @@ getFgnCall version (n, fc, d) = schFgnDef fc n d version export startChezPreamble : String -startChezPreamble = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Chez") - , "" - , "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" - , "" -- so that the preamble ends with a newline - ] +startChezPreamble = #""" +#!/bin/sh +# \#{ (generatedString "Chez") } + +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 + +"""# startChez : String -> String -> String -startChez appdir target = startChezPreamble ++ unlines - [ "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 ++ "\" \"$@\"" - ] +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 }" -startChezCmd : String -> String -> String -> String -> String -startChezCmd chez appdir target progType = unlines - [ "@echo off" - , "set APPDIR=%~dp0" - , "set PATH=%APPDIR%" ++ appdir ++ ";%PATH%" - , "set IDRIS2_INC_SRC=%APPDIR%" ++ appdir - , "\"" ++ chez ++ "\" " ++ progType ++ " \"%APPDIR%" ++ target ++ "\" %*" - ] +"$DIR/\#{ target }" "$@" +"""# -startChezWinSh : String -> String -> String -> String -> String -startChezWinSh chez appdir target progType = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Chez") - , "" - , "set -e # exit on any error" - , "" - , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")" - , "PATH=\"$DIR/" ++ appdir ++ ":$PATH\"" - , "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\"" - , "\"" ++ chez ++ "\" " ++ progType ++ " \"$DIR/" ++ target ++ "\" \"$@\"" - ] +startChezCmd : String -> String -> String -> String +startChezCmd chez appdir target progType = #""" +@echo off + +rem \#{ (generatedString "Chez") } + +set APPDIR=%~dp0 +set PATH=%APPDIR%\#{ appdir };%PATH% +set IDRIS2_INC_SRC=%APPDIR%\#{ appdir } + +"\#{ chez }" \#{ progType } "%APPDIR%\#{ target }" %* +"""# + +startChezWinSh : String -> String -> String -> String +startChezWinSh chez appdir target progType = #""" +#!/bin/sh +# \#{ (generatedString "Chez") } + +set -e # exit on any error + +DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") +PATH="$DIR/\#{ appdir }":$PATH + +export IDRIS2_INC_SRC="$DIR/\#{ appdir }" + +"\#{ chez }" \#{ progType } "$DIR/\#{ target }" "$@" +"""# ||| Compile a TT expression to Chez Scheme compileToSS : Ref Ctxt Defs -> diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index a78a120e1..f7e5b1cbc 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -39,59 +39,68 @@ import Libraries.Utils.String %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 tarm64le) (load-shared-object \"libc.so.6\")]" - , " [(i3osx ti3osx a6osx ta6osx tarm64osx) (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 \"" ++ escapeStringChez lib ++ "\")" | lib <- libs] - , ")" - ] +schHeader libs compilationUnits = """ + (import (chezscheme) (support) + \{ unwords ["(" ++ cu ++ ")" | cu <- compilationUnits] }) + (case (machine-type) + [(i3le ti3le a6le ta6le tarm64le) (load-shared-object "libc.so.6")] + [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object "libc.dylib")] + [(i3nt ti3nt a6nt ta6nt) (load-shared-object "msvcrt.dll")] + [else (load-shared-object "libc.so")] + \{ + unlines [" (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs] + }) +""" schFooter : String -schFooter = "(collect 4)\n(blodwen-run-finalisers)\n" +schFooter = """ + +(collect 4) +(blodwen-run-finalisers) +""" startChez : String -> String -> String -> String -startChez chez appDirSh targetSh = Chez.startChezPreamble ++ unlines - [ "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 ++ "\" " - ++ "\"$@\"" - ] +startChez chez appDirSh targetSh = Chez.startChezPreamble ++ #""" +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 }" \ + "$@" +"""# 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 ++ "\" " - ++ "%*" - ] +startChezCmd chez appDirSh targetSh = #""" +@echo off + +rem \#{ (generatedString "ChezSep") } + +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" - , "# " ++ (generatedString "Chez") - , "" - , "set -e # exit on any error" - , "" - , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")" - , "PATH=\"$DIR/" ++ appDirSh ++ ":$PATH\"" - , "\"" ++ chez ++ "\" --program \"$DIR/" ++ targetSh ++ "\" \"$@\"" - , "\"" ++ chez ++ "\" -q " - ++ "--libdirs \"$DIR/" ++ appDirSh ++ "\" " - ++ "--program \"$DIR/" ++ targetSh ++ "\" " - ++ "\"$@\"" - ] +startChezWinSh chez appDirSh targetSh = #""" +#!/bin/sh +# \#{ (generatedString "ChezSep") } + +set -e # exit on any error + +DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") +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 () diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 691112a57..453aa665c 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -49,14 +49,16 @@ findGSCBackend = Just e => " -cc " ++ e schHeader : String -schHeader = - "; " ++ (generatedString "Gambit") ++ "\n" ++ - "(declare (block)\n" ++ - "(inlining-limit 450)\n" ++ - "(standard-bindings)\n" ++ - "(extended-bindings)\n" ++ - "(not safe)\n" ++ - "(optimize-dead-definitions))\n" +schHeader = """ +;; \{ (generatedString "Gambit") } +(declare (block) + (inlining-limit 450) + (standard-bindings) + (extended-bindings) + (not safe) + (optimize-dead-definitions)) + +""" showGambitChar : Char -> String -> String showGambitChar '\\' = ("\\\\" ++) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index fdb49288b..dbb49bbdd 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -42,24 +42,29 @@ findRacoExe = pure $ (fromMaybe "/usr/bin/env raco" env) ++ " exe" schHeader : Bool -> String -> String -schHeader prof libs - = "#lang racket/base\n" ++ - "; " ++ (generatedString "Racket") ++ "\n" ++ - "(require racket/async-channel)\n" ++ -- for asynchronous channels - "(require racket/future)\n" ++ -- for parallelism/concurrency - "(require racket/math)\n" ++ -- for math ops - "(require racket/system)\n" ++ -- for system - "(require rnrs/bytevectors-6)\n" ++ -- for buffers - "(require rnrs/io/ports-6)\n" ++ -- for files - "(require srfi/19)\n" ++ -- for file handling and data - "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C - (if prof then "(require profile)\n" else "") ++ - "(require racket/flonum)\n" ++ -- for float-typed transcendental functions - libs ++ - "(let ()\n" +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 () + +""" schFooter : String -schFooter = ") (collect-garbage)" +schFooter = """ +) +(collect-garbage) +""" showRacketChar : Char -> String -> String showRacketChar '\\' = ("\\\\" ++) @@ -330,42 +335,48 @@ getFgnCall : {auto f : Ref Done (List String) } -> getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d startRacket : String -> String -> String -> String -startRacket racket appdir target = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Racket") - , "" - , "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" - , "" - , "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$LD_LIBRARY_PATH\"" - , "export DYLD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$DYLD_LIBRARY_PATH\"" - , racket ++ "\"$DIR/" ++ target ++ "\" \"$@\"" - ] +startRacket racket appdir target = #""" +#!/bin/sh +# \#{ (generatedString "Racket") } + +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 + +export LD_LIBRARY_PATH="$DIR/\#{ appdir }":$LD_LIBRARY_PATH +export DYLD_LIBRARY_PATH="$DIR/\#{ appdir }":$DYLD_LIBRARY_PATH + +\#{ racket } "$DIR/\#{ target }" "$@" +"""# startRacketCmd : String -> String -> String -> String -startRacketCmd racket appdir target = unlines - [ "@echo off" - , "set APPDIR=%~dp0" - , "set PATH=%APPDIR%" ++ appdir ++ ";%PATH%" - , racket ++ "\"%APPDIR%" ++ target ++ "\" %*" - ] +startRacketCmd racket appdir target = #""" +@echo off + +rem \#{ (generatedString "Racket") } + +set APPDIR=%~dp0 +set PATH=%APPDIR%\#{ appdir };%PATH% + +\#{ racket } "%APPDIR%\#{ target }" %* +"""# startRacketWinSh : String -> String -> String -> String -startRacketWinSh racket appdir target = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Racket") - , "" - , "set -e # exit on any error" - , "" - , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")" - , "PATH=\"$DIR/" ++ appdir ++ ":$PATH\"" - , racket ++ "\"$DIR/" ++ target ++ "\" \"$@\"" - ] +startRacketWinSh racket appdir target = #""" +#!/bin/sh +# \#{ (generatedString "Racket") } + +set -e # exit on any error + +DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") +PATH="$DIR/\#{ appdir }":$PATH + +\#{ racket } "$DIR/\#{ target }" "$@" +"""# compileToRKT : Ref Ctxt Defs -> String -> ClosedTerm -> (outfile : String) -> Core () diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 63e7073d7..882e3799e 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -141,18 +141,19 @@ record Metadata where covering Show Metadata where show (MkMetadata apps names tydecls currentLHS holeLHS nameLocMap - fname semanticHighlighting semanticAliases semanticDefaults) - = "Metadata:\n" ++ - " lhsApps: " ++ show apps ++ "\n" ++ - " names: " ++ show names ++ "\n" ++ - " type declarations: " ++ show tydecls ++ "\n" ++ - " current LHS: " ++ show currentLHS ++ "\n" ++ - " holes: " ++ show holeLHS ++ "\n" ++ - " nameLocMap: " ++ show nameLocMap ++ "\n" ++ - " sourceIdent: " ++ show fname ++ - " semanticHighlighting: " ++ show semanticHighlighting ++ - " semanticAliases: " ++ show semanticAliases ++ - " semanticDefaults: " ++ show semanticDefaults + fname semanticHighlighting semanticAliases semanticDefaults) = """ + Metadata: + lhsApps: \{ show apps } + names: \{ show names } + type declarations: \{ show tydecls } + current LHS: \{ show currentLHS } + holes: \{ show holeLHS } + nameLocMap: \{ show nameLocMap } + sourceIdent: \{ show fname } + semanticHighlighting: \{ show semanticHighlighting } + semanticAliases: \{ show semanticAliases } + semanticDefaults: \{ show semanticDefaults } + """ export initMetadata : OriginDesc -> Metadata diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 44a24beb9..d7e2e2be2 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -40,17 +40,18 @@ outputDirWithDefault d = fromMaybe (build_dir d "exec") (output_dir d) public export toString : Dirs -> String -toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = - unlines [ "+ Working Directory :: " ++ show wdir - , "+ Source Directory :: " ++ show sdir - , "+ Build Directory :: " ++ show bdir - , "+ Local Depend Directory :: " ++ show ldir - , "+ Output Directory :: " ++ show (outputDirWithDefault d) - , "+ Installation Prefix :: " ++ show dfix - , "+ Extra Directories :: " ++ show edirs - , "+ Package Directories :: " ++ show pdirs - , "+ CG Library Directories :: " ++ show ldirs - , "+ Data Directories :: " ++ show ddirs] +toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """ + Working Directory: \{ show wdir } + Source Directory: \{ show sdir } + Build Directory: \{ show bdir } + Local Depend Directory: \{ show ldir } + Output Directory: \{ show (outputDirWithDefault d) } + Installation Prefix: \{ show dfix } + Extra Directories: \{ show edirs } + Package Directories: \{ show pdirs } + CG Library Directories: \{ show ldirs } + Data Directories: \{ show ddirs } + """ public export data CG = Chez diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 20f98719b..5dec38af4 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -402,13 +402,16 @@ versionMsg = "Idris 2, version " ++ show version export usage : String -usage = versionMsg ++ "\n" ++ - "Usage: idris2 [options] [input file]\n\n" ++ - "Available options:\n" ++ - optsUsage ++ - "\n" ++ - "Environment variables:\n" ++ - envsUsage +usage = """ +\{ versionMsg } +Usage: idris2 [options] [input file] + +Available options: +\{ optsUsage } + +Environment variables: +\{ envsUsage } +""" checkNat : Integer -> Maybe Nat checkNat n = toMaybe (n >= 0) (integerToNat n) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 7b525ca7f..f3723f4ae 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -132,13 +132,15 @@ tryTTM (c :: cs) = tryTTM cs banner : String -banner = " ____ __ _ ___ \n" ++ - " / _/___/ /____(_)____ |__ \\ \n" ++ - " / // __ / ___/ / ___/ __/ / Version " ++ showVersion True version ++ "\n" ++ - " _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org \n" ++ - " /___/\\__,_/_/ /_/____/ /____/ Type :? for help \n" ++ - "\n" ++ - "Welcome to Idris 2. Enjoy yourself!" +banner = #""" + ____ __ _ ___ + / _/___/ /____(_)____ |__ \ + / // __ / ___/ / ___/ __/ / Version \#{ showVersion True version } + _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org + /___/\__,_/_/ /_/____/ /____/ Type :? for help + +Welcome to Idris 2. Enjoy yourself! +"""# checkVerbose : List CLOpt -> Bool checkVerbose [] = False diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index a4bc752d6..6d2c08e5f 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -779,22 +779,23 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts pOptUpdate opt | PErr = record {hasError = True} errorMsg : String -errorMsg = unlines - [ "Not all command line options can be used to override package options.\n" - , "Overridable options are:" - , " --quiet" - , " --verbose" - , " --timing" - , " --log " - , " --dumpcases " - , " --dumplifted " - , " --dumpvmcode " - , " --debug-elab-check" - , " --codegen " - , " --directive " - , " --build-dir " - , " --output-dir " - ] +errorMsg = """ +Not all command line options can be used to override package options. + +Overridable options are: + --quiet + --verbose + --timing + --log + --dumpcases + --dumplifted + --dumpvmcode + --debug-elab-check + --codegen + --directive + --build-dir + --output-dir +""" export processPackageOpts : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 4a78301d5..14b25087e 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -248,16 +248,15 @@ 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 unlines [ fun' ++ "()" - , "{" - , " ED=$([ -z $2 ] && echo \"--\" || echo $2)" - , " COMPREPLY=($(idris2 --bash-completion $ED $3))" - , "}" - , "" - , "complete -F " ++ fun' ++ " -o default idris2" - ] +completionScript fun = let fun' = "_" ++ fun in #""" +\#{ fun' }() +{ + ED=$([ -z $2 ] && echo "--" || echo $2) + COMPREPLY=($(idris2 --bash-completion $ED $3)) +} + +complete -F \#{ fun' } -o default idris2 +"""# -------------------------------------------------------------------------------- -- Processing Options From 26b94f09f7193ab4f43884abad7e54d5581e3e45 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Mon, 28 Jun 2021 12:07:06 +0300 Subject: [PATCH 2/9] [ cleanup ] Add idents to some underindented stuff --- src/Compiler/ES/Javascript.idr | 22 ++++----- src/Compiler/Scheme/Chez.idr | 68 +++++++++++++------------- src/Compiler/Scheme/ChezSep.idr | 62 ++++++++++++------------ src/Compiler/Scheme/Gambit.idr | 16 +++--- src/Compiler/Scheme/Racket.idr | 86 ++++++++++++++++----------------- src/Idris/CommandLine.idr | 14 +++--- src/Idris/Driver.idr | 14 +++--- src/Idris/Package.idr | 30 ++++++------ src/Idris/SetOptions.idr | 14 +++--- 9 files changed, 163 insertions(+), 163 deletions(-) diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index ca82ab931..ea325ce02 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -27,22 +27,22 @@ compileToJS c tm = compileToES c Javascript tm ["browser", "javascript"] htmlHeader : String htmlHeader = """ - - - - - - - - -""" + + + + """ addHeaderAndFooter : String -> String -> String addHeaderAndFooter outfile es = diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 3522b1d31..dcd15a5ac 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -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 -> diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index f7e5b1cbc..91b10db58 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -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 () diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 453aa665c..57ef7142b 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -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 '\\' = ("\\\\" ++) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index dbb49bbdd..5b822d256 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -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 () diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 5dec38af4..0b3a3d239 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -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) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index f3723f4ae..14b26b425 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -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 diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 6d2c08e5f..d22d9e42a 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -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 - --dumpcases - --dumplifted - --dumpvmcode - --debug-elab-check - --codegen - --directive - --build-dir - --output-dir -""" + Overridable options are: + --quiet + --verbose + --timing + --log + --dumpcases + --dumplifted + --dumpvmcode + --debug-elab-check + --codegen + --directive + --build-dir + --output-dir + """ export processPackageOpts : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 14b25087e..89a831a51 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -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 From 1e6f9dad718ed6ba067ed3db19a7bf5f3283ca3c Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Fri, 22 Oct 2021 15:59:15 +0600 Subject: [PATCH 3/9] [cleanup] Cleanup after rebasing --- src/Compiler/RefC/RefC.idr | 6 ++-- src/Compiler/Scheme/Chez.idr | 59 ++++++++++++++++----------------- src/Compiler/Scheme/ChezSep.idr | 49 ++++++++++++++------------- src/Compiler/Scheme/Racket.idr | 34 +++++++++---------- src/Core/Options.idr | 10 +++--- src/Idris/SetOptions.idr | 8 ++--- 6 files changed, 82 insertions(+), 84 deletions(-) diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 9bb6d80ff..5aed5727e 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -1001,9 +1001,9 @@ footer = do // main function int main(int argc, char *argv[]) { - \{ - (if contains "idris_support.h" !(get HeaderFiles) - then "idris2_setArgs(argc, argv);" else "") + \{ ifThenElse (contains "idris_support.h" !(get HeaderFiles)) + "idris2_setArgs(argc, argv);" + "" } Value *mainExprVal = __mainExpression_0(); trampoline(mainExprVal); diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index dcd15a5ac..5c975dc00 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -99,11 +99,10 @@ schHeader chez libs whole \{ showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) } - \{ - (if whole - then "(let ()" - else "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") (source-directories)))") - } + \{ ifThenElse whole + "(let ()" + "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") (source-directories)))" + } """ @@ -112,8 +111,8 @@ schFooter prof whole = """ (collect 4) (blodwen-run-finalisers) - \{ (if prof then "(profile-dump-html)" else "") } - \{ (if whole then ")" else "") } + \{ ifThenElse prof "(profile-dump-html)" "" } + \{ ifThenElse whole ")" "" } """ showChezChar : Char -> String -> String @@ -391,9 +390,9 @@ getFgnCall version (n, fc, d) = schFgnDef fc n d version export startChezPreamble : String -startChezPreamble = #""" +startChezPreamble = """ #!/bin/sh - # \#{ (generatedString "Chez") } + # \{ (generatedString "Chez") } set -e # exit on any error @@ -403,44 +402,44 @@ startChezPreamble = #""" 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 }" +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 }" - "$DIR/\#{ target }" "$@" - """# + "$DIR/\{ target }" "$@" + """ -startChezCmd : String -> String -> String -> String -startChezCmd chez appdir target progType = #""" +startChezCmd : String -> String -> String -> String -> String +startChezCmd chez appdir target progType = """ @echo off - rem \#{ (generatedString "Chez") } + rem \{ (generatedString "Chez") } set APPDIR=%~dp0 - set PATH=%APPDIR%\#{ appdir };%PATH% - set IDRIS2_INC_SRC=%APPDIR%\#{ appdir } + 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 = #""" +startChezWinSh : String -> String -> String -> String -> String +startChezWinSh chez appdir target progType = """ #!/bin/sh - # \#{ (generatedString "Chez") } + # \{ (generatedString "Chez") } set -e # exit on any error DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") - PATH="$DIR/\#{ appdir }":$PATH + 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 -> diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index 91b10db58..02c57284d 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -47,9 +47,8 @@ schHeader libs compilationUnits = """ [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object "libc.dylib")] [(i3nt ti3nt a6nt ta6nt) (load-shared-object "msvcrt.dll")] [else (load-shared-object "libc.so")] - \{ - unlines [" (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs] - }) + \{ unlines [" (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs] }) + """ schFooter : String @@ -60,47 +59,47 @@ schFooter = """ """ 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 +startChez chez appDirSh targetSh = Chez.startChezPreamble ++ """ + 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 = #""" +startChezCmd chez appDirSh targetSh = """ @echo off - rem \#{ (generatedString "ChezSep") } + rem \{ (generatedString "ChezSep") } set APPDIR=%~dp0 - set PATH=%APPDIR%\#{ appDirSh };%PATH% + 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 = #""" +startChezWinSh chez appDirSh targetSh = """ #!/bin/sh - # \#{ (generatedString "ChezSep") } + # \{ (generatedString "ChezSep") } set -e # exit on any error DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") - PATH="$DIR/\#{ appDirSh }":$PATH + 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 () diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 5b822d256..4ebef3595 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -53,7 +53,7 @@ schHeader prof libs = """ (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 "") } + \{ ifThenElse prof "(require profile)" "" } (require racket/flonum) ; for float-typed transcendental functions \{ libs } (let () @@ -335,9 +335,9 @@ getFgnCall : {auto f : Ref Done (List String) } -> getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d startRacket : String -> String -> String -> String -startRacket racket appdir target = #""" +startRacket racket appdir target = """ #!/bin/sh - # \#{ (generatedString "Racket") } + # \{ (generatedString "Racket") } set -e # exit on any error @@ -347,36 +347,36 @@ startRacket racket appdir target = #""" 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 = #""" +startRacketCmd racket appdir target = """ @echo off - rem \#{ (generatedString "Racket") } + rem \{ (generatedString "Racket") } set APPDIR=%~dp0 - set PATH=%APPDIR%\#{ appdir };%PATH% + set PATH=%APPDIR%\{ appdir };%PATH% - \#{ racket } "%APPDIR%\#{ target }" %* - """# + \{ racket } "%APPDIR%\{ target }" %* + """ startRacketWinSh : String -> String -> String -> String -startRacketWinSh racket appdir target = #""" +startRacketWinSh racket appdir target = """ #!/bin/sh - # \#{ (generatedString "Racket") } + # \{ (generatedString "Racket") } set -e # exit on any error DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") - PATH="$DIR/\#{ appdir }":$PATH + PATH="$DIR/\{ appdir }":$PATH - \#{ racket } "$DIR/\#{ target }" "$@" - """# + \{ racket } "$DIR/\{ target }" "$@" + """ compileToRKT : Ref Ctxt Defs -> String -> ClosedTerm -> (outfile : String) -> Core () diff --git a/src/Core/Options.idr b/src/Core/Options.idr index d7e2e2be2..fa0d5167f 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -41,12 +41,12 @@ outputDirWithDefault d = fromMaybe (build_dir d "exec") (output_dir d) public export toString : Dirs -> String toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """ - Working Directory: \{ show wdir } + Working Directory: \{ wdir } Source Directory: \{ show sdir } - Build Directory: \{ show bdir } - Local Depend Directory: \{ show ldir } - Output Directory: \{ show (outputDirWithDefault d) } - Installation Prefix: \{ show dfix } + Build Directory: \{ bdir } + Local Depend Directory: \{ ldir } + Output Directory: \{ (outputDirWithDefault d) } + Installation Prefix: \{ dfix } Extra Directories: \{ show edirs } Package Directories: \{ show pdirs } CG Library Directories: \{ show ldirs } diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 89a831a51..6e99ea526 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -248,15 +248,15 @@ 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' }() +completionScript fun = let fun' = "_" ++ fun in """ + \{ 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 From 15d5c784479c87712a8532c0f815c6409ca2d114 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Mon, 25 Oct 2021 13:38:09 +0600 Subject: [PATCH 4/9] [ cleanup ] A few more cleanups --- src/Compiler/RefC/RefC.idr | 2 +- src/Compiler/Scheme/Chez.idr | 8 ++++---- src/Compiler/Scheme/ChezSep.idr | 4 ++-- src/Compiler/Scheme/Gambit.idr | 2 +- src/Compiler/Scheme/Racket.idr | 8 ++++---- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 5aed5727e..bac4730e9 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -983,7 +983,7 @@ header : {auto c : Ref Ctxt Defs} header = do let initLines = """ #include - /* \{ (generatedString "RefC") } */ + /* \{ generatedString "RefC" } */ """ let headerFiles = Libraries.Data.SortedSet.toList !(get HeaderFiles) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 5c975dc00..9c5493c9c 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -88,7 +88,7 @@ schHeader chez libs whole = (if os /= "windows" then "#!" ++ chez ++ (if whole then " --program\n\n" else " --script\n\n") else "") ++ """ - ;; \{ (generatedString "Chez") } + ;; \{ generatedString "Chez" } (import (chezscheme)) (case (machine-type) [(i3fb ti3fb a6fb ta6fb) #f] @@ -392,7 +392,7 @@ export startChezPreamble : String startChezPreamble = """ #!/bin/sh - # \{ (generatedString "Chez") } + # \{ generatedString "Chez" } set -e # exit on any error @@ -417,7 +417,7 @@ startChezCmd : String -> String -> String -> String -> String startChezCmd chez appdir target progType = """ @echo off - rem \{ (generatedString "Chez") } + rem \{ generatedString "Chez" } set APPDIR=%~dp0 set PATH=%APPDIR%\{ appdir };%PATH% @@ -429,7 +429,7 @@ startChezCmd chez appdir target progType = """ startChezWinSh : String -> String -> String -> String -> String startChezWinSh chez appdir target progType = """ #!/bin/sh - # \{ (generatedString "Chez") } + # \{ generatedString "Chez" } set -e # exit on any error diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index 02c57284d..e5c67b419 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -73,7 +73,7 @@ startChezCmd : String -> String -> String -> String startChezCmd chez appDirSh targetSh = """ @echo off - rem \{ (generatedString "ChezSep") } + rem \{ generatedString "ChezSep" } set APPDIR=%~dp0 set PATH=%APPDIR%\{ appDirSh };%PATH% @@ -87,7 +87,7 @@ startChezCmd chez appDirSh targetSh = """ startChezWinSh : String -> String -> String -> String startChezWinSh chez appDirSh targetSh = """ #!/bin/sh - # \{ (generatedString "ChezSep") } + # \{ generatedString "ChezSep" } set -e # exit on any error diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 57ef7142b..acc8a20d7 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -50,7 +50,7 @@ findGSCBackend = schHeader : String schHeader = """ - ;; \{ (generatedString "Gambit") } + ;; \{ generatedString "Gambit" } (declare (block) (inlining-limit 450) (standard-bindings) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 4ebef3595..c644ca075 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -44,7 +44,7 @@ findRacoExe = schHeader : Bool -> String -> String schHeader prof libs = """ #lang racket/base - ;; \{ (generatedString "Racket") } + ;; \{ generatedString "Racket" } (require racket/async-channel) ; for asynchronous channels (require racket/future) ; for parallelism/concurrency (require racket/math) ; for math ops @@ -337,7 +337,7 @@ getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d startRacket : String -> String -> String -> String startRacket racket appdir target = """ #!/bin/sh - # \{ (generatedString "Racket") } + # \{ generatedString "Racket" } set -e # exit on any error @@ -357,7 +357,7 @@ startRacketCmd : String -> String -> String -> String startRacketCmd racket appdir target = """ @echo off - rem \{ (generatedString "Racket") } + rem \{ generatedString "Racket" } set APPDIR=%~dp0 set PATH=%APPDIR%\{ appdir };%PATH% @@ -368,7 +368,7 @@ startRacketCmd racket appdir target = """ startRacketWinSh : String -> String -> String -> String startRacketWinSh racket appdir target = """ #!/bin/sh - # \{ (generatedString "Racket") } + # \{ generatedString "Racket" } set -e # exit on any error From 47326767ace3ebb399e145eb4bfbf0ec61ee0c21 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Mon, 25 Oct 2021 13:52:26 +0600 Subject: [PATCH 5/9] [ cleanup ] A few more cleanups --- src/Core/Options.idr | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Core/Options.idr b/src/Core/Options.idr index fa0d5167f..f8b96c326 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -41,16 +41,16 @@ outputDirWithDefault d = fromMaybe (build_dir d "exec") (output_dir d) public export toString : Dirs -> String toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """ - Working Directory: \{ wdir } - Source Directory: \{ show sdir } - Build Directory: \{ bdir } - Local Depend Directory: \{ ldir } - Output Directory: \{ (outputDirWithDefault d) } - Installation Prefix: \{ dfix } - Extra Directories: \{ show edirs } - Package Directories: \{ show pdirs } - CG Library Directories: \{ show ldirs } - Data Directories: \{ show ddirs } + + Working Directory :: \{ wdir } + + Source Directory :: \{ show sdir } + + Build Directory :: \{ bdir } + + Local Depend Directory :: \{ ldir } + + Output Directory :: \{ outputDirWithDefault d } + + Installation Prefix :: \{ dfix } + + Extra Directories :: \{ show edirs } + + Package Directories :: \{ show pdirs } + + CG Library Directories :: \{ show ldirs } + + Data Directories :: \{ show ddirs } """ public export From 25b62b4e23d5c997490a53668f02234ba7514de4 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Tue, 2 Nov 2021 12:30:01 +0600 Subject: [PATCH 6/9] Revert the problematic code block to `unlines` Noted in issue #2087 --- src/Idris/Package.idr | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index d22d9e42a..1411f58b3 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -779,6 +779,23 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts pOptUpdate opt | PErr = record {hasError = True} errorMsg : String +errorMsg = unlines + [ "Not all command line options can be used to override package options.\n" + , "Overridable options are:" + , " --quiet" + , " --verbose" + , " --timing" + , " --log " + , " --dumpcases " + , " --dumplifted " + , " --dumpvmcode " + , " --debug-elab-check" + , " --codegen " + , " --directive " + , " --build-dir " + , " --output-dir " + ] +{- errorMsg = """ Not all command line options can be used to override package options. @@ -796,6 +813,7 @@ errorMsg = """ --build-dir --output-dir """ +-} export processPackageOpts : {auto c : Ref Ctxt Defs} -> From 1e19189debd803d9406877ea8417720d9e3fd535 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Thu, 4 Nov 2021 12:52:28 +0600 Subject: [PATCH 7/9] Apply suggestions from code review --- src/Compiler/Scheme/Chez.idr | 6 +++--- src/Compiler/Scheme/ChezSep.idr | 6 +++--- src/Compiler/Scheme/Racket.idr | 6 +++--- src/Core/Options.idr | 10 +++++----- src/Idris/CommandLine.idr | 1 - 5 files changed, 14 insertions(+), 15 deletions(-) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 9c5493c9c..f974f0566 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -406,8 +406,8 @@ startChezPreamble = """ 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 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 }" "$@" @@ -434,7 +434,7 @@ startChezWinSh chez appdir target progType = """ set -e # exit on any error DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") - PATH="$DIR/\{ appdir }":$PATH + PATH="$DIR/\{ appdir }:$PATH" export IDRIS2_INC_SRC="$DIR/\{ appdir }" diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index e5c67b419..455b2ac87 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -60,8 +60,8 @@ schFooter = """ 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 }" \ @@ -92,7 +92,7 @@ startChezWinSh chez appDirSh targetSh = """ set -e # exit on any error DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") - PATH="$DIR/\{ appDirSh }":$PATH + PATH="$DIR/\{ appDirSh }:$PATH" "\{ chez }" --program "$DIR/\{ targetSh }" "$@" "\{ chez }" -q \ diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index c644ca075..3f6fe798c 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -347,8 +347,8 @@ startRacket racket appdir target = """ 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 }" "$@" """ @@ -373,7 +373,7 @@ startRacketWinSh racket appdir target = """ set -e # exit on any error DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") - PATH="$DIR/\{ appdir }":$PATH + PATH="$DIR/\{ appdir }:$PATH" \{ racket } "$DIR/\{ target }" "$@" """ diff --git a/src/Core/Options.idr b/src/Core/Options.idr index f8b96c326..046015879 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -41,12 +41,12 @@ outputDirWithDefault d = fromMaybe (build_dir d "exec") (output_dir d) public export toString : Dirs -> String toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """ - + Working Directory :: \{ wdir } + + Working Directory :: \{ show wdir } + Source Directory :: \{ show sdir } - + Build Directory :: \{ bdir } - + Local Depend Directory :: \{ ldir } - + Output Directory :: \{ outputDirWithDefault d } - + Installation Prefix :: \{ dfix } + + Build Directory :: \{ show bdir } + + Local Depend Directory :: \{ show ldir } + + Output Directory :: \{ show $ outputDirWithDefault d } + + Installation Prefix :: \{ show dfix } + Extra Directories :: \{ show edirs } + Package Directories :: \{ show pdirs } + CG Library Directories :: \{ show ldirs } diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 0b3a3d239..5edb0ae7a 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -408,7 +408,6 @@ usage = """ Available options: \{ optsUsage } - Environment variables: \{ envsUsage } """ From a73e8a3e33065f416d5f020cc22b3a3efbe9916a Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Sat, 6 Nov 2021 18:48:21 +0600 Subject: [PATCH 8/9] Apply suggestions from code review --- src/Compiler/RefC/RefC.idr | 7 +++++++ src/Idris/Package.idr | 19 ------------------- 2 files changed, 7 insertions(+), 19 deletions(-) diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index bac4730e9..5ce55156f 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -452,6 +452,8 @@ const2Integer c i = _ => i + + -- we return for each of the ANF a set of statements and two possible return statements -- The first one for non-tail statements, the second one for tail statements -- this way, we can deal with tail calls and tail recursion. @@ -542,6 +544,7 @@ mutual constBlockSwitch alts retValVar (i+1) + constDefaultBlock : {auto a : Ref ArgCounter Nat} -> {auto t : Ref TemporaryVariableTracker (List (List String))} -> {auto oft : Ref OutfileText Output} @@ -562,6 +565,7 @@ mutual emit EmptyFC " }" + makeNonIntSwitchStatementConst : {auto a : Ref ArgCounter Nat} -> {auto t : Ref TemporaryVariableTracker (List (List String))} @@ -724,6 +728,9 @@ mutual pure $ MkRS "NULL" "NULL" + + + addCommaToList : List String -> List String addCommaToList [] = [] addCommaToList (x :: xs) = (" " ++ x) :: map (", " ++) xs diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 1411f58b3..a4bc752d6 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -795,25 +795,6 @@ errorMsg = unlines , " --build-dir " , " --output-dir " ] -{- -errorMsg = """ - Not all command line options can be used to override package options. - - Overridable options are: - --quiet - --verbose - --timing - --log - --dumpcases - --dumplifted - --dumpvmcode - --debug-elab-check - --codegen - --directive - --build-dir - --output-dir - """ --} export processPackageOpts : {auto c : Ref Ctxt Defs} -> From cadbee9fc6b6cccd1fa4b12a73a2a76a884c64c5 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Sat, 6 Nov 2021 18:49:41 +0600 Subject: [PATCH 9/9] Apply suggestions from code review --- src/Compiler/RefC/RefC.idr | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 5ce55156f..f73ea3e9b 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -454,6 +454,7 @@ const2Integer c i = + -- we return for each of the ANF a set of statements and two possible return statements -- The first one for non-tail statements, the second one for tail statements -- this way, we can deal with tail calls and tail recursion.