mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Chez output fix from upstream
This commit is contained in:
Edwin Brady
parent
17b17be963
commit
0363b8350b
270
idris2.ipkg
270
idris2.ipkg
@ -1,147 +1,147 @@
|
||||
package idris2
|
||||
|
||||
modules =
|
||||
-- Algebra,
|
||||
Algebra.Preorder
|
||||
-- Algebra.Semiring,
|
||||
-- Algebra.ZeroOneOmega,
|
||||
Algebra,
|
||||
Algebra.Preorder,
|
||||
Algebra.Semiring,
|
||||
Algebra.ZeroOneOmega,
|
||||
|
||||
-- Compiler.ANF,
|
||||
-- Compiler.Common,
|
||||
-- Compiler.CompileExpr,
|
||||
-- Compiler.Inline,
|
||||
-- Compiler.LambdaLift,
|
||||
-- Compiler.Scheme.Chez,
|
||||
-- Compiler.Scheme.Racket,
|
||||
-- Compiler.Scheme.Gambit,
|
||||
-- Compiler.Scheme.Common,
|
||||
-- Compiler.VMCode,
|
||||
--
|
||||
-- Control.Delayed,
|
||||
--
|
||||
-- Core.AutoSearch,
|
||||
-- Core.Binary,
|
||||
-- Core.CaseBuilder,
|
||||
-- Core.CaseTree,
|
||||
-- Core.Context,
|
||||
-- Core.CompileExpr,
|
||||
-- Core.Core,
|
||||
-- Core.Coverage,
|
||||
-- Core.Directory,
|
||||
-- Core.Env,
|
||||
-- Core.FC,
|
||||
-- Core.GetType,
|
||||
-- Core.Hash,
|
||||
-- Core.LinearCheck,
|
||||
-- Core.Metadata,
|
||||
-- Core.Name,
|
||||
-- Core.Normalise,
|
||||
-- Core.Options,
|
||||
-- -- Core.Reflect,
|
||||
-- Core.Termination,
|
||||
-- Core.TT,
|
||||
-- Core.TTC,
|
||||
-- Core.Unify,
|
||||
-- Core.UnifyState,
|
||||
-- Core.Value,
|
||||
--
|
||||
-- Data.ANameMap,
|
||||
-- Data.Bool.Extra,
|
||||
-- Data.IntMap,
|
||||
-- Data.IOArray,
|
||||
-- Data.NameMap,
|
||||
-- Data.StringMap,
|
||||
-- Data.These,
|
||||
-- Data.StringTrie,
|
||||
--
|
||||
-- Idris.CommandLine,
|
||||
-- Idris.Desugar,
|
||||
-- Idris.Elab.Implementation,
|
||||
-- Idris.Elab.Interface,
|
||||
-- Idris.Error,
|
||||
-- Idris.IDEMode.CaseSplit,
|
||||
-- Idris.IDEMode.Commands,
|
||||
-- Idris.IDEMode.MakeClause,
|
||||
-- Idris.IDEMode.Parser,
|
||||
-- Idris.IDEMode.REPL,
|
||||
-- Idris.IDEMode.TokenLine,
|
||||
-- Idris.ModTree,
|
||||
-- Idris.Package,
|
||||
-- Idris.Parser,
|
||||
-- Idris.ProcessIdr,
|
||||
-- Idris.REPL,
|
||||
-- Idris.REPLCommon,
|
||||
-- Idris.REPLOpts,
|
||||
-- Idris.Resugar,
|
||||
-- Idris.SetOptions,
|
||||
Compiler.ANF,
|
||||
Compiler.Common,
|
||||
Compiler.CompileExpr,
|
||||
Compiler.Inline,
|
||||
Compiler.LambdaLift,
|
||||
Compiler.Scheme.Chez,
|
||||
Compiler.Scheme.Racket,
|
||||
Compiler.Scheme.Gambit,
|
||||
Compiler.Scheme.Common,
|
||||
Compiler.VMCode,
|
||||
|
||||
Control.Delayed,
|
||||
|
||||
Core.AutoSearch,
|
||||
Core.Binary,
|
||||
Core.CaseBuilder,
|
||||
Core.CaseTree,
|
||||
Core.Context,
|
||||
Core.CompileExpr,
|
||||
Core.Core,
|
||||
Core.Coverage,
|
||||
Core.Directory,
|
||||
Core.Env,
|
||||
Core.FC,
|
||||
Core.GetType,
|
||||
Core.Hash,
|
||||
Core.LinearCheck,
|
||||
Core.Metadata,
|
||||
Core.Name,
|
||||
Core.Normalise,
|
||||
Core.Options,
|
||||
-- Core.Reflect,
|
||||
Core.Termination,
|
||||
Core.TT,
|
||||
Core.TTC,
|
||||
Core.Unify,
|
||||
Core.UnifyState,
|
||||
Core.Value,
|
||||
|
||||
Data.ANameMap,
|
||||
Data.Bool.Extra,
|
||||
Data.IntMap,
|
||||
Data.NameMap,
|
||||
Data.StringMap,
|
||||
Data.These,
|
||||
Data.StringTrie,
|
||||
|
||||
Idris.CommandLine,
|
||||
Idris.Desugar,
|
||||
Idris.Elab.Implementation,
|
||||
Idris.Elab.Interface,
|
||||
Idris.Error,
|
||||
Idris.IDEMode.CaseSplit,
|
||||
Idris.IDEMode.Commands,
|
||||
Idris.IDEMode.MakeClause,
|
||||
Idris.IDEMode.Parser,
|
||||
Idris.IDEMode.REPL,
|
||||
Idris.IDEMode.TokenLine,
|
||||
Idris.ModTree,
|
||||
Idris.Package,
|
||||
Idris.Parser,
|
||||
Idris.ProcessIdr,
|
||||
Idris.REPL,
|
||||
Idris.REPLCommon,
|
||||
Idris.REPLOpts,
|
||||
Idris.Resugar,
|
||||
Idris.SetOptions,
|
||||
-- Idris.Socket,
|
||||
-- Idris.Socket.Data,
|
||||
-- Idris.Socket.Raw,
|
||||
-- Idris.Syntax,
|
||||
-- Idris.Version,
|
||||
--
|
||||
-- Parser.Lexer,
|
||||
-- Parser.Support,
|
||||
-- Parser.Unlit,
|
||||
--
|
||||
-- Text.Lexer,
|
||||
-- Text.Lexer.Core,
|
||||
-- Text.Literate,
|
||||
-- Text.Parser,
|
||||
-- Text.Parser.Core,
|
||||
-- Text.Quantity,
|
||||
-- Text.Token,
|
||||
--
|
||||
-- TTImp.BindImplicits,
|
||||
-- TTImp.Elab,
|
||||
-- TTImp.Elab.Ambiguity,
|
||||
-- TTImp.Elab.App,
|
||||
-- TTImp.Elab.As,
|
||||
-- TTImp.Elab.Binders,
|
||||
-- TTImp.Elab.Case,
|
||||
-- TTImp.Elab.Check,
|
||||
-- TTImp.Elab.Dot,
|
||||
-- TTImp.Elab.Hole,
|
||||
-- TTImp.Elab.ImplicitBind,
|
||||
-- TTImp.Elab.Lazy,
|
||||
-- TTImp.Elab.Local,
|
||||
-- TTImp.Elab.Prim,
|
||||
-- -- TTImp.Elab.Quote,
|
||||
-- TTImp.Elab.Record,
|
||||
-- TTImp.Elab.Rewrite,
|
||||
-- TTImp.Elab.Term,
|
||||
-- TTImp.Elab.Utils,
|
||||
-- TTImp.Impossible,
|
||||
-- TTImp.Interactive.CaseSplit,
|
||||
-- TTImp.Interactive.ExprSearch,
|
||||
-- TTImp.Interactive.GenerateDef,
|
||||
-- TTImp.Interactive.MakeLemma,
|
||||
-- TTImp.Parser,
|
||||
-- TTImp.PartialEval,
|
||||
-- TTImp.ProcessData,
|
||||
-- TTImp.ProcessDecls,
|
||||
-- TTImp.ProcessDef,
|
||||
-- TTImp.ProcessParams,
|
||||
-- TTImp.ProcessRecord,
|
||||
-- TTImp.ProcessTransform,
|
||||
-- TTImp.ProcessType,
|
||||
-- -- TTImp.Reflect,
|
||||
-- TTImp.TTImp,
|
||||
-- TTImp.Unelab,
|
||||
-- TTImp.Utils,
|
||||
-- TTImp.WithClause,
|
||||
--
|
||||
-- Utils.Binary,
|
||||
-- Utils.Hex,
|
||||
-- Utils.Octal,
|
||||
-- Utils.Shunting,
|
||||
-- Utils.String,
|
||||
--
|
||||
-- Yaffle.Main,
|
||||
-- Yaffle.REPL
|
||||
Idris.Syntax,
|
||||
Idris.Version,
|
||||
|
||||
Parser.Lexer,
|
||||
Parser.Support,
|
||||
Parser.Unlit,
|
||||
|
||||
Text.Lexer,
|
||||
Text.Lexer.Core,
|
||||
Text.Literate,
|
||||
Text.Parser,
|
||||
Text.Parser.Core,
|
||||
Text.Quantity,
|
||||
Text.Token,
|
||||
|
||||
TTImp.BindImplicits,
|
||||
TTImp.Elab,
|
||||
TTImp.Elab.Ambiguity,
|
||||
TTImp.Elab.App,
|
||||
TTImp.Elab.As,
|
||||
TTImp.Elab.Binders,
|
||||
TTImp.Elab.Case,
|
||||
TTImp.Elab.Check,
|
||||
TTImp.Elab.Dot,
|
||||
TTImp.Elab.Hole,
|
||||
TTImp.Elab.ImplicitBind,
|
||||
TTImp.Elab.Lazy,
|
||||
TTImp.Elab.Local,
|
||||
TTImp.Elab.Prim,
|
||||
-- TTImp.Elab.Quote,
|
||||
TTImp.Elab.Record,
|
||||
TTImp.Elab.Rewrite,
|
||||
TTImp.Elab.Term,
|
||||
TTImp.Elab.Utils,
|
||||
TTImp.Impossible,
|
||||
TTImp.Interactive.CaseSplit,
|
||||
TTImp.Interactive.ExprSearch,
|
||||
TTImp.Interactive.GenerateDef,
|
||||
TTImp.Interactive.MakeLemma,
|
||||
TTImp.Parser,
|
||||
TTImp.PartialEval,
|
||||
TTImp.ProcessData,
|
||||
TTImp.ProcessDecls,
|
||||
TTImp.ProcessDef,
|
||||
TTImp.ProcessParams,
|
||||
TTImp.ProcessRecord,
|
||||
TTImp.ProcessTransform,
|
||||
TTImp.ProcessType,
|
||||
-- TTImp.Reflect,
|
||||
TTImp.TTImp,
|
||||
TTImp.Unelab,
|
||||
TTImp.Utils,
|
||||
TTImp.WithClause,
|
||||
|
||||
Utils.Binary,
|
||||
Utils.Hex,
|
||||
Utils.Octal,
|
||||
Utils.Shunting,
|
||||
Utils.String,
|
||||
|
||||
Yaffle.Main,
|
||||
Yaffle.REPL
|
||||
|
||||
depends = contrib
|
||||
|
||||
sourcedir = "src"
|
||||
|
||||
-- main = Idris.Main
|
||||
main = Idris.Main
|
||||
executable = idris2sh
|
||||
|
||||
@ -307,12 +307,12 @@ getFgnCall : {auto c : Ref Ctxt Defs} ->
|
||||
String -> (Name, FC, NamedDef) -> Core (String, String)
|
||||
getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d
|
||||
|
||||
startChez : String -> String
|
||||
startChez target = unlines
|
||||
startChez : String -> String -> String
|
||||
startChez appdir target = unlines
|
||||
[ "#!/bin/sh"
|
||||
, ""
|
||||
, "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:$(dirname \"" ++ target ++ "\")\""
|
||||
, "\"" ++ target ++ "\" \"$@\""
|
||||
, "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname $0`/\"" ++ appdir ++ "\"\""
|
||||
, "`dirname $0`/\"" ++ target ++ "\" \"$@\""
|
||||
]
|
||||
|
||||
||| Compile a TT expression to Chez Scheme
|
||||
@ -359,9 +359,9 @@ compileToSO appDirRel outSsAbs
|
||||
coreLift $ system tmpFileAbs
|
||||
pure ()
|
||||
|
||||
makeSh : String -> String -> Core ()
|
||||
makeSh outShRel outAbs
|
||||
= do Right () <- coreLift $ writeFile outShRel (startChez outAbs)
|
||||
makeSh : String -> String -> String -> Core ()
|
||||
makeSh outShRel appdir outAbs
|
||||
= do Right () <- coreLift $ writeFile outShRel (startChez appdir outAbs)
|
||||
| Left err => throw (FileErr outShRel err)
|
||||
pure ()
|
||||
|
||||
@ -369,16 +369,21 @@ makeSh outShRel outAbs
|
||||
compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
|
||||
ClosedTerm -> (outfile : String) -> Core (Maybe String)
|
||||
compileExpr makeitso c execDir tm outfile
|
||||
= do let appDirRel = execDir ++ dirSep ++ outfile ++ "_app"
|
||||
coreLift $ mkdirs (splitDir appDirRel)
|
||||
= do let appDirRel = outfile ++ "_app" -- relative to build dir
|
||||
let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
|
||||
|
||||
coreLift $ mkdirs (splitDir appDirGen)
|
||||
Just cwd <- coreLift currentDir
|
||||
| Nothing => throw (InternalError "Can't get current directory")
|
||||
let outSsAbs = cwd ++ dirSep ++ appDirRel ++ dirSep ++ outfile ++ ".ss"
|
||||
let outSoAbs = cwd ++ dirSep ++ appDirRel ++ dirSep ++ outfile ++ ".so"
|
||||
compileToSS c appDirRel tm outSsAbs
|
||||
logTime "Make SO" $ when makeitso $ compileToSO appDirRel outSsAbs
|
||||
let outSsFile = appDirRel ++ dirSep ++ outfile ++ ".ss"
|
||||
let outSoFile = appDirRel ++ dirSep ++ outfile ++ ".so"
|
||||
let outSsAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSsFile
|
||||
let outSoAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSoFile
|
||||
|
||||
compileToSS c appDirGen tm outSsAbs
|
||||
logTime "Make SO" $ when makeitso $ compileToSO appDirGen outSsAbs
|
||||
let outShRel = execDir ++ dirSep ++ outfile
|
||||
makeSh outShRel (if makeitso then outSoAbs else outSsAbs)
|
||||
makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
|
||||
coreLift $ chmodRaw outShRel 0o755
|
||||
pure (Just outShRel)
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user