mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
Support for incremental compilation with Chez
This adds a new flag '--inc <backend>' which, if set, compiles all modules incrementally, and for executables, links the incrementally compiled modules rather than building the whole program. Also, adds an environment variable IDRIS2_INC_CGS for providing a comma separated list of backends to use for incremental builds. Also, adds '--whole-program', which overrides incremental builds for an executable. Incremental builds are much faster if there's nothing to recompile, but for the Chez backend, generate code which runs at about half the speed. Currently only works for Chez - other backends ignore the flag. Also, incremental building of an executable will only work if *all* required modules have been built incrementally for the backend in use.
This commit is contained in:
parent
939bc8d8ff
commit
94088bea80
10
Makefile
10
Makefile
@ -68,19 +68,19 @@ src/IdrisPaths.idr: FORCE
|
||||
FORCE:
|
||||
|
||||
prelude:
|
||||
${MAKE} -C libs/prelude IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
${MAKE} -C libs/prelude IDRIS2=${TARGET} IDRIS2_INC_CGS=chez IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
|
||||
base: prelude
|
||||
${MAKE} -C libs/base IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
${MAKE} -C libs/base IDRIS2=${TARGET} IDRIS2_INC_CGS=chez IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
|
||||
network: prelude
|
||||
${MAKE} -C libs/network IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
${MAKE} -C libs/network IDRIS2=${TARGET} IDRIS2_INC_CGS=chez IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
|
||||
contrib: base
|
||||
${MAKE} -C libs/contrib IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
${MAKE} -C libs/contrib IDRIS2=${TARGET} IDRIS2_INC_CGS=chez IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
|
||||
test-lib: contrib
|
||||
${MAKE} -C libs/test IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
${MAKE} -C libs/test IDRIS2=${TARGET} IDRIS2_INC_CGS=chez IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
|
||||
libs : prelude base contrib network test-lib
|
||||
|
||||
|
@ -8,5 +8,12 @@ sourcedir = "src"
|
||||
-- (Currently supported by Racket and Chez back ends, others ignore it)
|
||||
-- opts = "--profile"
|
||||
|
||||
-- Set if you want incremental builds. This is good for development, since
|
||||
-- small changes compile faster, but bad for deployment since the resulting
|
||||
-- executable runs at around half the speed.
|
||||
-- (Alternatively: set the environment variable IDRIS2_INC_CGS=chez)
|
||||
-- For this to work, you need to do the initial incremental build from clean.
|
||||
-- opts = "--inc chez"
|
||||
|
||||
main = Idris.Main
|
||||
executable = idris2
|
||||
|
@ -39,6 +39,17 @@ record Codegen where
|
||||
ClosedTerm -> (outfile : String) -> Core (Maybe String)
|
||||
||| Execute an Idris 2 expression directly.
|
||||
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
|
||||
||| Incrementally compile definitions in the current module (toIR defs)
|
||||
||| if supported
|
||||
||| Takes a source file name, returns the name of the generated object
|
||||
||| file, if successful, plus any other backend specific data in a list
|
||||
||| of strings. The generated object file should be placed in the same
|
||||
||| directory as the associated TTC.
|
||||
incCompileFile : Maybe (Ref Ctxt Defs ->
|
||||
(sourcefile : String) ->
|
||||
Core (Maybe (String, List String)))
|
||||
||| If incremental compilation is supported, get the output file extension
|
||||
incExt : Maybe String
|
||||
|
||||
-- Say which phase of compilation is the last one to use - it saves time if
|
||||
-- you only ask for what you need.
|
||||
@ -107,6 +118,14 @@ execute {c} cg tm
|
||||
executeExpr cg c tmpDir tm
|
||||
pure ()
|
||||
|
||||
export
|
||||
incCompile : {auto c : Ref Ctxt Defs} ->
|
||||
Codegen -> String -> Core (Maybe (String, List String))
|
||||
incCompile {c} cg src
|
||||
= do let Just inc = incCompileFile cg
|
||||
| Nothing => pure Nothing
|
||||
inc c src
|
||||
|
||||
-- If an entry isn't already decoded, get the minimal entry we need for
|
||||
-- compilation, and record the Binary so that we can put it back when we're
|
||||
-- done (so that we don't obliterate the definition)
|
||||
@ -250,6 +269,15 @@ dumpVMCode fn lns
|
||||
dumpDef : (Name, VMDef) -> String
|
||||
dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"
|
||||
|
||||
export
|
||||
nonErased : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core Bool
|
||||
nonErased n
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => pure True
|
||||
pure (multiplicity gdef /= erased)
|
||||
|
||||
-- Find all the names which need compiling, from a given expression, and compile
|
||||
-- them to CExp form (and update that in the Defs).
|
||||
-- Return the names, the type tags, and a compiled version of the expression
|
||||
@ -324,13 +352,40 @@ getCompileData doLazyAnnots phase tm_in
|
||||
pure (MkCompileData compiledtm
|
||||
(mapMaybe id namedefs)
|
||||
lifted anf vmcode)
|
||||
where
|
||||
nonErased : Name -> Core Bool
|
||||
nonErased n
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => pure True
|
||||
pure (multiplicity gdef /= erased)
|
||||
|
||||
export
|
||||
compileTerm : {auto c : Ref Ctxt Defs} ->
|
||||
ClosedTerm -> Core (CExp [])
|
||||
compileTerm tm_in
|
||||
= do tm <- toFullNames tm_in
|
||||
fixArityExp !(compileExp tm)
|
||||
|
||||
export
|
||||
getIncCompileData : {auto c : Ref Ctxt Defs} -> (doLazyAnnots : Bool) ->
|
||||
UsePhase -> Core CompileData
|
||||
getIncCompileData doLazyAnnots phase
|
||||
= do defs <- get Ctxt
|
||||
-- Compile all the names in 'toIR', since those are the ones defined
|
||||
-- in the current source file
|
||||
let ns = keys (toIR defs)
|
||||
cns <- traverse toFullNames ns
|
||||
rcns <- filterM nonErased cns
|
||||
traverse_ mkForgetDef rcns
|
||||
|
||||
namedefs <- traverse getNamedDef rcns
|
||||
lifted_in <- if phase >= Lifted
|
||||
then logTime "++ Lambda lift" $ traverse (lambdaLift doLazyAnnots) rcns
|
||||
else pure []
|
||||
let lifted = concat lifted_in
|
||||
anf <- if phase >= ANF
|
||||
then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
|
||||
else pure []
|
||||
vmcode <- if phase >= VMCode
|
||||
then logTime "++ Get VM Code" $ pure (allDefs anf)
|
||||
else pure []
|
||||
pure (MkCompileData (CErased emptyFC)
|
||||
(mapMaybe id namedefs)
|
||||
lifted anf vmcode)
|
||||
|
||||
-- Some things missing from Prelude.File
|
||||
|
||||
|
@ -6,6 +6,7 @@ import Core.Context
|
||||
import Core.Env
|
||||
import Core.Name
|
||||
import Core.Normalise
|
||||
import Core.Options
|
||||
import Core.TT
|
||||
import Core.Value
|
||||
|
||||
@ -683,17 +684,53 @@ getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)
|
||||
getCFTypes args t
|
||||
= pure (reverse args, !(nfToCFType (getLoc t) False t))
|
||||
|
||||
lamRHSenv : Int -> FC -> (ns : List Name) -> SubstCEnv ns []
|
||||
lamRHSenv i fc [] = []
|
||||
lamRHSenv i fc (n :: ns)
|
||||
= CRef fc (MN "x" i) :: lamRHSenv (i + 1) fc ns
|
||||
|
||||
mkBounds : (xs : _) -> Bounds xs
|
||||
mkBounds [] = None
|
||||
mkBounds (x :: xs) = Add x x (mkBounds xs)
|
||||
|
||||
getNewArgs : {done : _} ->
|
||||
SubstCEnv done args -> List Name
|
||||
getNewArgs [] = []
|
||||
getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs
|
||||
getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
|
||||
|
||||
-- If a name is declared in one module and defined in another,
|
||||
-- we have to assume arity 0 for incremental compilation because
|
||||
-- we have no idea how it's defined, and when we made calls to the
|
||||
-- function, they had arity 0.
|
||||
lamRHS : (ns : List Name) -> CExp ns -> CExp []
|
||||
lamRHS ns tm
|
||||
= let env = lamRHSenv 0 (getFC tm) ns
|
||||
tmExp = substs env (rewrite appendNilRightNeutral ns in tm)
|
||||
newArgs = reverse $ getNewArgs env
|
||||
bounds = mkBounds newArgs
|
||||
expLocs = mkLocals zero {vars = []} bounds tmExp in
|
||||
lamBind (getFC tm) _ expLocs
|
||||
where
|
||||
lamBind : FC -> (ns : List Name) -> CExp ns -> CExp []
|
||||
lamBind fc [] tm = tm
|
||||
lamBind fc (n :: ns) tm = lamBind fc ns (CLam fc n tm)
|
||||
|
||||
toCDef : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> ClosedTerm -> List Nat -> Def ->
|
||||
Core CDef
|
||||
toCDef n ty _ None
|
||||
= pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
|
||||
toCDef n ty erased (PMDef _ args _ tree _)
|
||||
toCDef n ty erased (PMDef pi args _ tree _)
|
||||
= do let (args' ** p) = mkSub 0 args erased
|
||||
comptree <- toCExpTree n tree
|
||||
if isNil erased
|
||||
then pure $ MkFun args comptree
|
||||
else pure $ MkFun args' (shrinkCExp p comptree)
|
||||
pure $ toLam (externalDecl pi) $ if isNil erased
|
||||
then MkFun args comptree
|
||||
else MkFun args' (shrinkCExp p comptree)
|
||||
where
|
||||
toLam : Bool -> CDef -> CDef
|
||||
toLam True (MkFun args rhs) = MkFun [] (lamRHS args rhs)
|
||||
toLam _ d = d
|
||||
toCDef n ty _ (ExternDef arity)
|
||||
= let (ns ** args) = mkArgList 0 arity in
|
||||
pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
|
||||
@ -759,9 +796,22 @@ compileDef n
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
|
||||
ce <- toCDef n (type gdef) (eraseArgs gdef)
|
||||
!(toFullNames (definition gdef))
|
||||
setCompiled n ce
|
||||
-- If we're incremental, and the name has no definition yet, it
|
||||
-- might end up defined in another module, so leave it, but warn
|
||||
if noDefYet (definition gdef) (incrementalCGs !getSession)
|
||||
-- This won't be accurate if we have names declared in one module
|
||||
-- and defined elsewhere. It's tricky to do the complete check that
|
||||
-- we do for whole program compilation, though, since that involves
|
||||
-- traversing everything from the main expression.
|
||||
-- For now, consider it an incentive not to have cycles :).
|
||||
then recordWarning (GenericWarn ("Compiling hole " ++ show n))
|
||||
else do ce <- toCDef n (type gdef) (eraseArgs gdef)
|
||||
!(toFullNames (definition gdef))
|
||||
setCompiled n ce
|
||||
where
|
||||
noDefYet : Def -> List CG -> Bool
|
||||
noDefYet None (_ :: _) = True
|
||||
noDefYet _ _ = False
|
||||
|
||||
export
|
||||
mkForgetDef : {auto c : Ref Ctxt Defs} ->
|
||||
|
@ -70,4 +70,4 @@ executeExpr c tmpDir tm =
|
||||
||| Codegen wrapper for Javascript implementation.
|
||||
export
|
||||
codegenJavascript : Codegen
|
||||
codegenJavascript = MkCG compileExpr executeExpr
|
||||
codegenJavascript = MkCG compileExpr executeExpr Nothing Nothing
|
||||
|
@ -58,4 +58,4 @@ executeExpr c tmpDir tm =
|
||||
||| Codegen wrapper for Node implementation.
|
||||
export
|
||||
codegenNode : Codegen
|
||||
codegenNode = MkCG compileExpr executeExpr
|
||||
codegenNode = MkCG compileExpr executeExpr Nothing Nothing
|
||||
|
@ -7,6 +7,7 @@ import Core.CompileExpr
|
||||
import Core.Context
|
||||
import Core.Context.Log
|
||||
import Core.FC
|
||||
import Core.Options
|
||||
import Core.TT
|
||||
|
||||
import Libraries.Data.LengthMatch
|
||||
@ -315,9 +316,9 @@ fixArityTm (CRef fc n) args
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => pure (unload args (CRef fc n))
|
||||
let Just def = compexpr gdef
|
||||
| Nothing => pure (unload args (CRef fc n))
|
||||
let arity = getArity def
|
||||
let arity = case compexpr gdef of
|
||||
Just def => getArity def
|
||||
_ => 0
|
||||
pure $ expandToArity arity (CApp fc (CRef fc n) []) args
|
||||
fixArityTm (CLam fc x sc) args
|
||||
= pure $ expandToArity Z (CLam fc x !(fixArityTm sc [])) args
|
||||
@ -501,9 +502,16 @@ mergeLamDef : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
mergeLamDef n
|
||||
= do defs <- get Ctxt
|
||||
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
|
||||
let Just cexpr = compexpr def | Nothing => pure ()
|
||||
setCompiled n !(mergeLam cexpr)
|
||||
Just def <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => pure ()
|
||||
let PMDef pi _ _ _ _ = definition def
|
||||
| _ => pure ()
|
||||
if not (isNil (incrementalCGs !getSession)) &&
|
||||
externalDecl pi -- better keep it at arity 0
|
||||
then pure ()
|
||||
else do let Just cexpr = compexpr def
|
||||
| Nothing => pure ()
|
||||
setCompiled n !(mergeLam cexpr)
|
||||
|
||||
export
|
||||
compileAndInlineAll : {auto c : Ref Ctxt Defs} ->
|
||||
|
@ -1046,4 +1046,4 @@ compileExpr _ _ _ _ _ _ = pure Nothing
|
||||
|
||||
export
|
||||
codegenRefC : Codegen
|
||||
codegenRefC = MkCG (compileExpr ANF) executeExpr
|
||||
codegenRefC = MkCG (compileExpr ANF) executeExpr Nothing Nothing
|
||||
|
@ -82,8 +82,8 @@ findLibs ds
|
||||
then Just (trim (substr 3 (length d) d))
|
||||
else Nothing
|
||||
|
||||
schHeader : String -> List String -> String
|
||||
schHeader chez libs
|
||||
schHeader : String -> List String -> Bool -> String
|
||||
schHeader chez libs whole
|
||||
= (if os /= "windows" then "#!" ++ chez ++ " --script\n\n" else "") ++
|
||||
"; @generated\n" ++
|
||||
"(import (chezscheme))\n" ++
|
||||
@ -95,14 +95,18 @@ schHeader chez libs
|
||||
" (load-shared-object \"ws2_32.dll\")]\n" ++
|
||||
" [else (load-shared-object \"libc.so\")])\n\n" ++
|
||||
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) ++ "\n\n" ++
|
||||
"(let ()\n"
|
||||
if whole
|
||||
then "(let ()\n"
|
||||
else "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") '()))\n"
|
||||
|
||||
schFooter : Bool -> String
|
||||
schFooter prof
|
||||
schFooter : Bool -> Bool -> String
|
||||
schFooter prof whole
|
||||
= "(collect 4)\n(blodwen-run-finalisers)\n" ++
|
||||
if prof
|
||||
then "(profile-dump-html))\n"
|
||||
else ")\n"
|
||||
(if prof
|
||||
then "(profile-dump-html)"
|
||||
else "") ++
|
||||
(if whole
|
||||
then ")\n" else "\n")
|
||||
|
||||
showChezChar : Char -> String -> String
|
||||
showChezChar '\\' = ("\\\\" ++)
|
||||
@ -156,7 +160,7 @@ mutual
|
||||
= do structsc <- schExp chezExtPrim chezString 0 struct
|
||||
pure $ "(ftype-ref " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ ")"
|
||||
chezExtPrim i GetField [_,_,_,_,_,_]
|
||||
= pure "(error \"bad getField\")"
|
||||
= pure "(blodwen-error-quit \"bad getField\")"
|
||||
chezExtPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
|
||||
NmPrimVal _ (Str fld), _, val, world]
|
||||
= do structsc <- schExp chezExtPrim chezString 0 struct
|
||||
@ -165,7 +169,7 @@ mutual
|
||||
"(ftype-set! " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++
|
||||
" " ++ valsc ++ ")"
|
||||
chezExtPrim i SetField [_,_,_,_,_,_,_,_]
|
||||
= pure "(error \"bad setField\")"
|
||||
= pure "(blodwen-error-quit \"bad setField\")"
|
||||
chezExtPrim i SysCodegen []
|
||||
= pure $ "\"chez\""
|
||||
chezExtPrim i OnCollect [_, p, c, world]
|
||||
@ -213,34 +217,55 @@ cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
|
||||
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
|
||||
" to foreign function"))
|
||||
|
||||
export
|
||||
loadLib : {auto c : Ref Ctxt Defs} ->
|
||||
String -> String -> Core String
|
||||
loadLib appdir clib
|
||||
= do (fname, fullname) <- locate clib
|
||||
copyLib (appdir </> fname, fullname)
|
||||
pure $ "(load-shared-object \""
|
||||
++ escapeStringChez fname
|
||||
++ "\")\n"
|
||||
|
||||
loadSO : {auto c : Ref Ctxt Defs} ->
|
||||
String -> String -> Core String
|
||||
loadSO appdir "" = pure ""
|
||||
loadSO appdir mod
|
||||
= do d <- getDirs
|
||||
let fs = map (\p => p </> mod)
|
||||
((build_dir d </> "ttc") :: extra_dirs d)
|
||||
Just fname <- firstAvailable fs
|
||||
| Nothing => throw (InternalError ("Missing .so:" ++ mod))
|
||||
-- Easier to put them all in the same directory, so we don't need
|
||||
-- to traverse a directory tree when installing the executable. So,
|
||||
-- separate with '-' rather than directory separators.
|
||||
let modfname = fastConcat (intersperse "-" (splitPath mod))
|
||||
copyLib (appdir </> modfname, fname)
|
||||
pure $ "(load \"" ++ escapeStringChez modfname ++ "\")\n"
|
||||
|
||||
cCall : {auto c : Ref Ctxt Defs}
|
||||
-> {auto l : Ref Loaded (List String)}
|
||||
-> String
|
||||
-> FC
|
||||
-> (cfn : String)
|
||||
-> (clib : String)
|
||||
-> List (Name, CFType)
|
||||
-> CFType
|
||||
-> (collectSafe : Bool)
|
||||
-> Core (String, String)
|
||||
cCall appdir fc cfn clib args (CFIORes CFGCPtr) _
|
||||
-> Core (Maybe String, String)
|
||||
cCall fc cfn clib args (CFIORes CFGCPtr) _
|
||||
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
|
||||
cCall appdir fc cfn clib args CFGCPtr _
|
||||
cCall fc cfn clib args CFGCPtr _
|
||||
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
|
||||
cCall appdir fc cfn clib args (CFIORes CFBuffer) _
|
||||
cCall fc cfn clib args (CFIORes CFBuffer) _
|
||||
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
|
||||
cCall appdir fc cfn clib args CFBuffer _
|
||||
cCall fc cfn clib args CFBuffer _
|
||||
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
|
||||
cCall appdir fc cfn clib args ret collectSafe
|
||||
cCall fc cfn clib args ret collectSafe
|
||||
= do loaded <- get Loaded
|
||||
lib <- if clib `elem` loaded
|
||||
then pure ""
|
||||
else do (fname, fullname) <- locate clib
|
||||
copyLib (appdir </> fname, fullname)
|
||||
put Loaded (clib :: loaded)
|
||||
pure $ "(load-shared-object \""
|
||||
++ escapeStringChez fname
|
||||
++ "\")\n"
|
||||
then pure Nothing
|
||||
else do put Loaded (clib :: loaded)
|
||||
pure (Just clib)
|
||||
argTypes <- traverse (cftySpec fc . snd) args
|
||||
retType <- cftySpec fc ret
|
||||
let callConv = if collectSafe then " __collect_safe" else ""
|
||||
@ -305,22 +330,22 @@ schemeCall fc sfn argns ret
|
||||
-- function call.
|
||||
useCC : {auto c : Ref Ctxt Defs} ->
|
||||
{auto l : Ref Loaded (List String)} ->
|
||||
String -> FC -> List String -> List (Name, CFType) -> CFType ->
|
||||
Maybe Version -> Core (String, String)
|
||||
useCC appdir fc ccs args ret version
|
||||
FC -> List String -> List (Name, CFType) -> CFType ->
|
||||
Maybe Version -> Core (Maybe String, String)
|
||||
useCC fc ccs args ret version
|
||||
= case parseCC ["scheme,chez", "scheme", "C__collect_safe", "C"] ccs of
|
||||
Just ("scheme,chez", [sfn]) =>
|
||||
do body <- schemeCall fc sfn (map fst args) ret
|
||||
pure ("", body)
|
||||
pure (Nothing, body)
|
||||
Just ("scheme", [sfn]) =>
|
||||
do body <- schemeCall fc sfn (map fst args) ret
|
||||
pure ("", body)
|
||||
pure (Nothing, body)
|
||||
Just ("C__collect_safe", (cfn :: clib :: _)) => do
|
||||
if unsupportedCallingConvention version
|
||||
then cCall appdir fc cfn clib args ret False
|
||||
else cCall appdir fc cfn clib args ret True
|
||||
then cCall fc cfn clib args ret False
|
||||
else cCall fc cfn clib args ret True
|
||||
Just ("C", (cfn :: clib :: _)) =>
|
||||
cCall appdir fc cfn clib args ret False
|
||||
cCall fc cfn clib args ret False
|
||||
_ => throw (NoForeignCC fc ccs)
|
||||
|
||||
-- For every foreign arg type, return a name, and whether to pass it to the
|
||||
@ -350,28 +375,30 @@ mkStruct _ = pure ""
|
||||
schFgnDef : {auto c : Ref Ctxt Defs} ->
|
||||
{auto l : Ref Loaded (List String)} ->
|
||||
{auto s : Ref Structs (List String)} ->
|
||||
String -> FC -> Name -> NamedDef -> Maybe Version -> Core (String, String)
|
||||
schFgnDef appdir fc n (MkNmForeign cs args ret) version
|
||||
FC -> Name -> NamedDef -> Maybe Version ->
|
||||
Core (Maybe String, String)
|
||||
schFgnDef fc n (MkNmForeign cs args ret) version
|
||||
= do let argns = mkArgs 0 args
|
||||
let allargns = map fst argns
|
||||
let useargns = map fst (filter snd argns)
|
||||
argStrs <- traverse mkStruct args
|
||||
retStr <- mkStruct ret
|
||||
(load, body) <- useCC appdir fc cs (zip useargns args) ret version
|
||||
(load, body) <- useCC fc cs (zip useargns args) ret version
|
||||
defs <- get Ctxt
|
||||
pure (load,
|
||||
concat argStrs ++ retStr ++
|
||||
"(define " ++ schName !(full (gamma defs) n) ++
|
||||
" (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
|
||||
body ++ "))\n")
|
||||
schFgnDef _ _ _ _ _ = pure ("", "")
|
||||
schFgnDef _ _ _ _ = pure (Nothing, "")
|
||||
|
||||
export
|
||||
getFgnCall : {auto c : Ref Ctxt Defs} ->
|
||||
{auto l : Ref Loaded (List String)} ->
|
||||
{auto s : Ref Structs (List String)} ->
|
||||
String -> Maybe Version -> (Name, FC, NamedDef) -> Core (String, String)
|
||||
getFgnCall appdir version (n, fc, d) = schFgnDef appdir fc n d version
|
||||
Maybe Version -> (Name, FC, NamedDef) ->
|
||||
Core (Maybe String, String)
|
||||
getFgnCall version (n, fc, d) = schFgnDef fc n d version
|
||||
|
||||
export
|
||||
startChezPreamble : String
|
||||
@ -391,6 +418,7 @@ startChezPreamble = unlines
|
||||
startChez : String -> String -> String
|
||||
startChez appdir target = startChezPreamble ++ unlines
|
||||
[ "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ "\":$LD_LIBRARY_PATH"
|
||||
, "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\""
|
||||
, "\"$DIR/" ++ target ++ "\" \"$@\""
|
||||
]
|
||||
|
||||
@ -399,6 +427,7 @@ startChezCmd chez appdir target = unlines
|
||||
[ "@echo off"
|
||||
, "set APPDIR=%~dp0"
|
||||
, "set PATH=%APPDIR%\\" ++ appdir ++ ";%PATH%"
|
||||
, "set IDRIS2_INC_SRC=%APPDIR%\\"
|
||||
, "\"" ++ chez ++ "\" --script \"%APPDIR%/" ++ target ++ "\" %*"
|
||||
]
|
||||
|
||||
@ -411,12 +440,14 @@ startChezWinSh chez appdir target = unlines
|
||||
, "DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
|
||||
, "CHEZ=$(cygpath \"" ++ chez ++"\")"
|
||||
, "export PATH=\"$DIR/" ++ appdir ++ "\":$PATH"
|
||||
, "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\""
|
||||
, "\"$CHEZ\" --script \"$DIR/" ++ target ++ "\" \"$@\""
|
||||
]
|
||||
|
||||
||| Compile a TT expression to Chez Scheme
|
||||
compileToSS : Ref Ctxt Defs ->
|
||||
Bool -> String -> ClosedTerm -> (outfile : String) -> Core ()
|
||||
Bool -> -- profiling
|
||||
String -> ClosedTerm -> (outfile : String) -> Core ()
|
||||
compileToSS c prof appdir tm outfile
|
||||
= do ds <- getDirectives Chez
|
||||
libs <- findLibs ds
|
||||
@ -430,17 +461,19 @@ compileToSS c prof appdir tm outfile
|
||||
s <- newRef {t = List String} Structs []
|
||||
chez <- coreLift findChez
|
||||
version <- coreLift $ chezVersion chez
|
||||
fgndefs <- traverse (getFgnCall appdir version) ndefs
|
||||
fgndefs <- traverse (getFgnCall version) ndefs
|
||||
loadlibs <- traverse (loadLib appdir) (mapMaybe fst fgndefs)
|
||||
|
||||
compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
|
||||
let code = fastAppend (map snd fgndefs ++ compdefs)
|
||||
main <- schExp chezExtPrim chezString 0 ctm
|
||||
support <- readDataFile "chez/support.ss"
|
||||
extraRuntime <- getExtraRuntime ds
|
||||
let scm = schHeader chez (map snd libs) ++
|
||||
let scm = schHeader chez (map snd libs) True ++
|
||||
support ++ extraRuntime ++ code ++
|
||||
concat (map fst fgndefs) ++
|
||||
concat loadlibs ++
|
||||
"(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
|
||||
main ++ schFooter prof
|
||||
main ++ schFooter prof True
|
||||
Right () <- coreLift $ writeFile outfile scm
|
||||
| Left err => throw (FileErr outfile err)
|
||||
coreLift_ $ chmodRaw outfile 0o755
|
||||
@ -448,7 +481,8 @@ compileToSS c prof appdir tm outfile
|
||||
|
||||
||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
|
||||
compileToSO : {auto c : Ref Ctxt Defs} ->
|
||||
Bool -> String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
|
||||
Bool -> -- profiling
|
||||
String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
|
||||
compileToSO prof chez appDirRel outSsAbs
|
||||
= do let tmpFileAbs = appDirRel </> "compileChez"
|
||||
let build = "(parameterize ([optimize-level 3] "
|
||||
@ -462,6 +496,35 @@ compileToSO prof chez appDirRel outSsAbs
|
||||
coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
|
||||
pure ()
|
||||
|
||||
||| Compile a TT expression to Chez Scheme using incremental module builds
|
||||
compileToSSInc : Ref Ctxt Defs ->
|
||||
List String -> -- module so files
|
||||
List String -> -- libraries to find and load
|
||||
String -> ClosedTerm -> (outfile : String) -> Core ()
|
||||
compileToSSInc c mods libs appdir tm outfile
|
||||
= do chez <- coreLift findChez
|
||||
tmcexp <- compileTerm tm
|
||||
let ctm = forget tmcexp
|
||||
|
||||
loadlibs <- traverse (loadLib appdir) (nub libs)
|
||||
loadsos <- traverse (loadSO appdir) (nub mods)
|
||||
|
||||
main <- schExp chezExtPrim chezString 0 ctm
|
||||
support <- readDataFile "chez/support.ss"
|
||||
|
||||
let scm = schHeader chez [] False ++
|
||||
support ++
|
||||
concat loadlibs ++
|
||||
concat loadsos ++
|
||||
"(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
|
||||
main ++ schFooter False False
|
||||
|
||||
Right () <- coreLift $ writeFile outfile scm
|
||||
| Left err => throw (FileErr outfile err)
|
||||
coreLift_ $ chmodRaw outfile 0o755
|
||||
pure ()
|
||||
|
||||
|
||||
makeSh : String -> String -> String -> Core ()
|
||||
makeSh outShRel appdir outAbs
|
||||
= do Right () <- coreLift $ writeFile outShRel (startChez appdir outAbs)
|
||||
@ -478,10 +541,9 @@ makeShWindows chez outShRel appdir outAbs
|
||||
| Left err => throw (FileErr outShRel err)
|
||||
pure ()
|
||||
|
||||
||| 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
|
||||
compileExprWhole : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
|
||||
ClosedTerm -> (outfile : String) -> Core (Maybe String)
|
||||
compileExprWhole makeitso c tmpDir outputDir tm outfile
|
||||
= do let appDirRel = outfile ++ "_app" -- relative to build dir
|
||||
let appDirGen = outputDir </> appDirRel -- relative to here
|
||||
coreLift_ $ mkdirAll appDirGen
|
||||
@ -494,7 +556,8 @@ compileExpr makeitso c tmpDir outputDir tm outfile
|
||||
chez <- coreLift $ findChez
|
||||
let prof = profile !getSession
|
||||
compileToSS c (makeitso && prof) appDirGen tm outSsAbs
|
||||
logTime "++ Make SO" $ when makeitso $ compileToSO prof chez appDirGen outSsAbs
|
||||
logTime "++ Make SO" $ when makeitso $
|
||||
compileToSO prof chez appDirGen outSsAbs
|
||||
let outShRel = outputDir </> outfile
|
||||
if isWindows
|
||||
then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)
|
||||
@ -502,6 +565,41 @@ compileExpr makeitso c tmpDir outputDir tm outfile
|
||||
coreLift_ $ chmodRaw outShRel 0o755
|
||||
pure (Just outShRel)
|
||||
|
||||
compileExprInc : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
|
||||
ClosedTerm -> (outfile : String) -> Core (Maybe String)
|
||||
compileExprInc makeitso c tmpDir outputDir tm outfile
|
||||
= do defs <- get Ctxt
|
||||
let Just (mods, libs) = lookup Chez (allIncData defs)
|
||||
| Nothing =>
|
||||
do coreLift $ putStrLn $ "Missing incremental compile data, reverting to whole program compilation"
|
||||
compileExprWhole makeitso c tmpDir outputDir tm outfile
|
||||
let appDirRel = outfile ++ "_app" -- relative to build dir
|
||||
let appDirGen = outputDir </> appDirRel -- relative to here
|
||||
coreLift_ $ mkdirAll appDirGen
|
||||
Just cwd <- coreLift currentDir
|
||||
| Nothing => throw (InternalError "Can't get current directory")
|
||||
let outSsFile = appDirRel </> outfile <.> "ss"
|
||||
let outSoFile = appDirRel </> outfile <.> "so"
|
||||
let outSsAbs = cwd </> outputDir </> outSsFile
|
||||
let outSoAbs = cwd </> outputDir </> outSoFile
|
||||
chez <- coreLift $ findChez
|
||||
compileToSSInc c mods libs appDirGen tm outSsAbs
|
||||
let outShRel = outputDir </> outfile
|
||||
if isWindows
|
||||
then makeShWindows chez outShRel appDirRel outSsFile
|
||||
else makeSh outShRel appDirRel outSsFile
|
||||
coreLift_ $ chmodRaw outShRel 0o755
|
||||
pure (Just outShRel)
|
||||
|
||||
||| 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 s <- getSession
|
||||
if not (wholeProgram s) && (Chez `elem` incrementalCGs !getSession)
|
||||
then compileExprInc makeitso c tmpDir outputDir tm outfile
|
||||
else compileExprWhole makeitso c tmpDir outputDir tm outfile
|
||||
|
||||
||| 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 ()
|
||||
@ -511,7 +609,44 @@ executeExpr c tmpDir tm
|
||||
coreLift_ $ system sh
|
||||
pure ()
|
||||
|
||||
incCompile : Ref Ctxt Defs ->
|
||||
(sourceFile : String) -> Core (Maybe (String, List String))
|
||||
incCompile c sourceFile
|
||||
= do ssFile <- getTTCFileName sourceFile "ss"
|
||||
soFile <- getTTCFileName sourceFile "so"
|
||||
soFilename <- getObjFileName sourceFile "so"
|
||||
cdata <- getIncCompileData False Cases
|
||||
|
||||
d <- getDirs
|
||||
let outputDir = build_dir d </> "ttc"
|
||||
|
||||
let ndefs = namedDefs cdata
|
||||
if isNil ndefs
|
||||
then pure (Just ("", []))
|
||||
-- ^ no code to generate, but still recored that the
|
||||
-- module has been compiled, with no output needed.
|
||||
else do
|
||||
l <- newRef {t = List String} Loaded ["libc", "libc 6"]
|
||||
s <- newRef {t = List String} Structs []
|
||||
chez <- coreLift findChez
|
||||
version <- coreLift $ chezVersion chez
|
||||
fgndefs <- traverse (getFgnCall version) ndefs
|
||||
compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
|
||||
let code = fastAppend (map snd fgndefs ++ compdefs)
|
||||
Right () <- coreLift $ writeFile ssFile code
|
||||
| Left err => throw (FileErr ssFile err)
|
||||
|
||||
-- Compile to .so
|
||||
let tmpFileAbs = outputDir </> "compileChez"
|
||||
let build = "(parameterize ([optimize-level 3] " ++
|
||||
"[compile-file-message #f]) (compile-file " ++
|
||||
show ssFile ++ "))"
|
||||
Right () <- coreLift $ writeFile tmpFileAbs build
|
||||
| Left err => throw (FileErr tmpFileAbs err)
|
||||
coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
|
||||
pure (Just (soFilename, mapMaybe fst fgndefs))
|
||||
|
||||
||| Codegen wrapper for Chez scheme implementation.
|
||||
export
|
||||
codegenChez : Codegen
|
||||
codegenChez = MkCG (compileExpr True) executeExpr
|
||||
codegenChez = MkCG (compileExpr True) executeExpr (Just incCompile) (Just "so")
|
||||
|
@ -217,8 +217,9 @@ compileToSS c chez appdir tm = do
|
||||
++ " (import (chezscheme) (support) " ++ imports ++ ")\n\n"
|
||||
let footer = ")"
|
||||
|
||||
fgndefs <- traverse (Chez.getFgnCall appdir version) cu.definitions
|
||||
fgndefs <- traverse (Chez.getFgnCall version) cu.definitions
|
||||
compdefs <- traverse (getScheme Chez.chezExtPrim Chez.chezString) cu.definitions
|
||||
loadlibs <- traverse (loadLib appdir) (mapMaybe fst fgndefs)
|
||||
|
||||
-- write the files
|
||||
log "compiler.scheme.chez" 3 $ "Generating code for " ++ chezLib
|
||||
@ -226,7 +227,7 @@ compileToSS c chez appdir tm = do
|
||||
[header]
|
||||
++ map snd fgndefs -- definitions using foreign libs
|
||||
++ compdefs
|
||||
++ map fst fgndefs -- foreign library load statements
|
||||
++ loadlibs -- foreign library load statements
|
||||
++ [footer]
|
||||
|
||||
Core.writeFile (appdir </> chezLib <.> "hash") cuHash
|
||||
@ -311,4 +312,4 @@ executeExpr c tmpDir tm
|
||||
||| Codegen wrapper for Chez scheme implementation.
|
||||
export
|
||||
codegenChezSep : Codegen
|
||||
codegenChezSep = MkCG (compileExpr True) executeExpr
|
||||
codegenChezSep = MkCG (compileExpr True) executeExpr Nothing Nothing
|
||||
|
@ -423,4 +423,4 @@ executeExpr c tmpDir tm
|
||||
|
||||
export
|
||||
codegenGambit : Codegen
|
||||
codegenGambit = MkCG compileExpr executeExpr
|
||||
codegenGambit = MkCG compileExpr executeExpr Nothing Nothing
|
||||
|
@ -456,4 +456,4 @@ executeExpr c tmpDir tm
|
||||
|
||||
export
|
||||
codegenRacket : Codegen
|
||||
codegenRacket = MkCG (compileExpr True) executeExpr
|
||||
codegenRacket = MkCG (compileExpr True) executeExpr Nothing Nothing
|
||||
|
@ -31,7 +31,7 @@ import public Libraries.Utils.Binary
|
||||
||| (Increment this when changing anything in the data format)
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 56
|
||||
ttcVersion = 57
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
@ -44,6 +44,7 @@ record TTCFile extra where
|
||||
sourceHash : String
|
||||
ifaceHash : Int
|
||||
importHashes : List (Namespace, Int)
|
||||
incData : List (CG, String, List String)
|
||||
context : List (Name, Binary)
|
||||
userHoles : List Name
|
||||
autoHints : List (Name, Bool)
|
||||
@ -92,14 +93,14 @@ HasNames (Name, Name, Bool) where
|
||||
resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)
|
||||
|
||||
HasNames e => HasNames (TTCFile e) where
|
||||
full gam (MkTTCFile version sourceHash ifaceHash iHashes
|
||||
full gam (MkTTCFile version sourceHash ifaceHash iHashes incData
|
||||
context userHoles
|
||||
autoHints typeHints
|
||||
imported nextVar currentNS nestedNS
|
||||
pairnames rewritenames primnames
|
||||
namedirectives cgdirectives trans
|
||||
extra)
|
||||
= pure $ MkTTCFile version sourceHash ifaceHash iHashes
|
||||
= pure $ MkTTCFile version sourceHash ifaceHash iHashes incData
|
||||
context userHoles
|
||||
!(traverse (full gam) autoHints)
|
||||
!(traverse (full gam) typeHints)
|
||||
@ -130,14 +131,14 @@ HasNames e => HasNames (TTCFile e) where
|
||||
-- I don't think we ever actually want to call this, because after we read
|
||||
-- from the file we're going to add them to learn what the resolved names
|
||||
-- are supposed to be! But for completeness, let's do it right.
|
||||
resolved gam (MkTTCFile version sourceHash ifaceHash iHashes
|
||||
resolved gam (MkTTCFile version sourceHash ifaceHash iHashes incData
|
||||
context userHoles
|
||||
autoHints typeHints
|
||||
imported nextVar currentNS nestedNS
|
||||
pairnames rewritenames primnames
|
||||
namedirectives cgdirectives trans
|
||||
extra)
|
||||
= pure $ MkTTCFile version sourceHash ifaceHash iHashes
|
||||
= pure $ MkTTCFile version sourceHash ifaceHash iHashes incData
|
||||
context userHoles
|
||||
!(traverse (resolved gam) autoHints)
|
||||
!(traverse (resolved gam) typeHints)
|
||||
@ -179,6 +180,7 @@ writeTTCFile b file_in
|
||||
toBuf b (sourceHash file)
|
||||
toBuf b (ifaceHash file)
|
||||
toBuf b (importHashes file)
|
||||
toBuf b (incData file)
|
||||
toBuf b (imported file)
|
||||
toBuf b (extraData file)
|
||||
toBuf b (context file)
|
||||
@ -208,10 +210,12 @@ readTTCFile readall file as b
|
||||
sourceFileHash <- fromBuf b
|
||||
ifaceHash <- fromBuf b
|
||||
importHashes <- fromBuf b
|
||||
incData <- fromBuf b
|
||||
imp <- fromBuf b
|
||||
ex <- fromBuf b
|
||||
if not readall
|
||||
then pure (MkTTCFile ver sourceFileHash ifaceHash importHashes [] [] [] [] []
|
||||
then pure (MkTTCFile ver sourceFileHash ifaceHash importHashes
|
||||
incData [] [] [] [] []
|
||||
0 (mkNamespace "") [] Nothing
|
||||
Nothing
|
||||
(MkPrimNs Nothing Nothing Nothing Nothing)
|
||||
@ -230,7 +234,7 @@ readTTCFile readall file as b
|
||||
nds <- fromBuf b
|
||||
cgds <- fromBuf b
|
||||
trans <- fromBuf b
|
||||
pure (MkTTCFile ver sourceFileHash ifaceHash importHashes
|
||||
pure (MkTTCFile ver sourceFileHash ifaceHash importHashes incData
|
||||
(map (replaceNS cns) defs) uholes
|
||||
autohs typehs imp nextv cns nns
|
||||
pns rws prims nds cgds trans ex)
|
||||
@ -277,6 +281,7 @@ writeToTTC extradata sourceFileName ttcFileName
|
||||
log "ttc.write" 5 $ "Writing " ++ ttcFileName ++ " with source hash " ++ sourceHash ++ " and interface hash " ++ show (ifaceHash defs)
|
||||
writeTTCFile bin
|
||||
(MkTTCFile ttcVersion (sourceHash) (ifaceHash defs) (importHashes defs)
|
||||
(incData defs)
|
||||
gdefs
|
||||
(keys (userHoles defs))
|
||||
(saveAutoHints defs)
|
||||
@ -455,7 +460,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
|
||||
ttc <- readTTCFile True fname as bin
|
||||
let ex = extraData ttc
|
||||
traverse_ (addGlobalDef modNS (currentNS ttc) as) (context ttc)
|
||||
traverse_ addUserHole (userHoles ttc)
|
||||
traverse_ (addUserHole True) (userHoles ttc)
|
||||
setNS (currentNS ttc)
|
||||
when nestedns $ setNestedNS (nestedNS ttc)
|
||||
-- Only do the next batch if the module hasn't been loaded
|
||||
@ -464,6 +469,8 @@ readFromTTC nestedns loc reexp fname modNS importAs
|
||||
-- Set up typeHints and autoHints based on the loaded data
|
||||
do traverse_ (addTypeHint loc) (typeHints ttc)
|
||||
traverse_ addAutoHint (autoHints ttc)
|
||||
addImportedInc modNS (incData ttc)
|
||||
defs <- get Ctxt
|
||||
-- Set up pair/rewrite etc names
|
||||
updatePair (pairnames ttc)
|
||||
updateRewrite (rewritenames ttc)
|
||||
|
@ -40,10 +40,12 @@ record PMDefInfo where
|
||||
holeInfo : HoleInfo -- data if it comes from a solved hole
|
||||
alwaysReduce : Bool -- always reduce, even when quoting etc
|
||||
-- typically for inlinable metavariable solutions
|
||||
externalDecl : Bool -- declared in another module, which may affect how it
|
||||
-- is compiled
|
||||
|
||||
export
|
||||
defaultPI : PMDefInfo
|
||||
defaultPI = MkPMDefInfo NotHole False
|
||||
defaultPI = MkPMDefInfo NotHole False False
|
||||
|
||||
public export
|
||||
record TypeFlags where
|
||||
@ -1104,12 +1106,19 @@ record Defs where
|
||||
-- be interpreted however the specific code generator requires
|
||||
toCompileCase : List Name
|
||||
-- ^ Names which need to be compiled to run time case trees
|
||||
incData : List (CG, String, List String)
|
||||
-- ^ What we've compiled incrementally for this module: codegen,
|
||||
-- object file, any additional CG dependent data (e.g. linker flags)
|
||||
allIncData : List (CG, List String, List String)
|
||||
-- ^ Incrementally compiled files for all imports. Only lists CGs for
|
||||
-- while all modules have associated incremental compile data
|
||||
toIR : NameMap ()
|
||||
-- ^ Names which need to be compiled to IR at the end of processing
|
||||
-- the current module
|
||||
userHoles : NameMap ()
|
||||
userHoles : NameMap Bool
|
||||
-- ^ Metavariables the user still has to fill in. In practice, that's
|
||||
-- everything with a user accessible name and a definition of Hole
|
||||
-- everything with a user accessible name and a definition of Hole.
|
||||
-- The Bool says whether it was introduced in another module.
|
||||
peFailures : NameMap ()
|
||||
-- ^ Partial evaluation names which have failed, so don't bother trying
|
||||
-- again
|
||||
@ -1159,6 +1168,8 @@ initDefs
|
||||
, allImported = []
|
||||
, cgdirectives = []
|
||||
, toCompileCase = []
|
||||
, incData = []
|
||||
, allIncData = []
|
||||
, toIR = empty
|
||||
, userHoles = empty
|
||||
, peFailures = empty
|
||||
@ -1288,10 +1299,12 @@ initHash
|
||||
|
||||
export
|
||||
addUserHole : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
addUserHole n
|
||||
Bool -> -- defined in another module?
|
||||
Name -> -- hole name
|
||||
Core ()
|
||||
addUserHole ext n
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { userHoles $= insert n () } defs)
|
||||
put Ctxt (record { userHoles $= insert n ext } defs)
|
||||
|
||||
export
|
||||
clearUserHole : {auto c : Ref Ctxt Defs} ->
|
||||
@ -2639,3 +2652,47 @@ checkTimer
|
||||
if (t > max)
|
||||
then throw (Timeout action)
|
||||
else pure ()
|
||||
|
||||
-- Update the list of imported incremental compile data, if we're in
|
||||
-- incremental mode for the current CG
|
||||
export
|
||||
addImportedInc : {auto c : Ref Ctxt Defs} ->
|
||||
ModuleIdent -> List (CG, String, List String) -> Core ()
|
||||
addImportedInc modNS inc
|
||||
= do s <- getSession
|
||||
let cg = s.codegen
|
||||
defs <- get Ctxt
|
||||
when (cg `elem` s.incrementalCGs) $
|
||||
case lookup cg inc of
|
||||
Nothing =>
|
||||
-- No incremental compile data for current CG, so we can't
|
||||
-- compile incrementally
|
||||
do recordWarning (GenericWarn ("No incremental compile data for " ++ show modNS))
|
||||
defs <- get Ctxt
|
||||
put Ctxt (record { allIncData $= drop cg } defs)
|
||||
Just (mods, extra) =>
|
||||
put Ctxt (record { allIncData $= addMod cg (mods, extra) }
|
||||
defs)
|
||||
where
|
||||
addMod : CG -> (String, List String) ->
|
||||
List (CG, (List String, List String)) ->
|
||||
List (CG, (List String, List String))
|
||||
addMod cg (mod, all) [] = [(cg, ([mod], all))]
|
||||
addMod cg (mod, all) ((cg', (mods, libs)) :: xs)
|
||||
= if cg == cg'
|
||||
then ((cg, (mod :: mods, libs ++ all)) :: xs)
|
||||
else ((cg', (mods, libs)) :: addMod cg (mod, all) xs)
|
||||
|
||||
drop : CG -> List (CG, a) -> List (CG, a)
|
||||
drop cg [] = []
|
||||
drop cg ((x, v) :: xs)
|
||||
= if cg == x
|
||||
then xs
|
||||
else ((x, v) :: drop cg xs)
|
||||
|
||||
export
|
||||
setIncData : {auto c : Ref Ctxt Defs} ->
|
||||
CG -> (String, List String) -> Core ()
|
||||
setIncData cg res
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { incData $= ((cg, res) :: )} defs)
|
||||
|
@ -65,6 +65,7 @@ data Warning : Type where
|
||||
FC -> Env Term vars -> Term vars -> Warning
|
||||
ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
|
||||
Deprecated : String -> Warning
|
||||
GenericWarn : String -> Warning
|
||||
|
||||
-- All possible errors, carrying a location
|
||||
public export
|
||||
@ -183,6 +184,7 @@ Show Warning where
|
||||
show (UnreachableClause _ _ _) = ":Unreachable clause"
|
||||
show (ShadowingGlobalDefs _ _) = ":Shadowing names"
|
||||
show (Deprecated name) = ":Deprecated " ++ name
|
||||
show (GenericWarn msg) = msg
|
||||
|
||||
|
||||
export
|
||||
@ -359,6 +361,7 @@ getWarningLoc : Warning -> Maybe FC
|
||||
getWarningLoc (UnreachableClause fc _ _) = Just fc
|
||||
getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
|
||||
getWarningLoc (Deprecated _) = Nothing
|
||||
getWarningLoc (GenericWarn _) = Nothing
|
||||
|
||||
export
|
||||
getErrorLoc : Error -> Maybe FC
|
||||
|
@ -207,6 +207,18 @@ getTTCFileName inp ext
|
||||
let bdir = build_dir d
|
||||
pure $ bdir </> "ttc" </> fname
|
||||
|
||||
-- Given a source file, return the name of the corresponding object file.
|
||||
-- As above, but without the build directory
|
||||
export
|
||||
getObjFileName : {auto c : Ref Ctxt Defs} ->
|
||||
String -> String -> Core String
|
||||
getObjFileName inp ext
|
||||
= do -- Get its namespace from the file relative to the working directory
|
||||
-- and generate the ttc file from that
|
||||
ns <- ctxtPathToNS inp
|
||||
let fname = ModuleIdent.toPath ns <.> ext
|
||||
pure $ fname
|
||||
|
||||
-- Given a root executable name, return the name in the build directory
|
||||
export
|
||||
getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String
|
||||
|
@ -164,6 +164,11 @@ record Session where
|
||||
showShadowingWarning : Bool
|
||||
-- Experimental
|
||||
checkHashesInsteadOfModTime : Bool
|
||||
incrementalCGs : List CG
|
||||
wholeProgram : Bool
|
||||
-- Use whole program compilation for executables, no matter what
|
||||
-- incremental CGs are set (intended for overriding any environment
|
||||
-- variables that set incremental compilation)
|
||||
|
||||
public export
|
||||
record PPrinter where
|
||||
@ -212,7 +217,8 @@ export
|
||||
defaultSession : Session
|
||||
defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
|
||||
False False False Nothing Nothing
|
||||
Nothing Nothing False 1000 False True False
|
||||
Nothing Nothing False 1000 False True
|
||||
False [] False
|
||||
|
||||
export
|
||||
defaultElab : ElabDirectives
|
||||
|
@ -904,10 +904,12 @@ TTC PMDefInfo where
|
||||
toBuf b l
|
||||
= do toBuf b (holeInfo l)
|
||||
toBuf b (alwaysReduce l)
|
||||
toBuf b (externalDecl l)
|
||||
fromBuf b
|
||||
= do h <- fromBuf b
|
||||
r <- fromBuf b
|
||||
pure (MkPMDefInfo h r)
|
||||
e <- fromBuf b
|
||||
pure (MkPMDefInfo h r e)
|
||||
|
||||
export
|
||||
TTC TypeFlags where
|
||||
|
@ -475,7 +475,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
|
||||
rhs <- mkDef locs INil tm ty
|
||||
|
||||
logTerm "unify.instantiate" 5 "Definition" rhs
|
||||
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)
|
||||
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs) False
|
||||
let newdef = record { definition =
|
||||
PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) []
|
||||
} mdef
|
||||
@ -1464,7 +1464,7 @@ retryGuess mode smode (hid, (loc, hname))
|
||||
do ty <- getType [] tm
|
||||
logTerm "unify.retry" 5 "Retry Delay" tm
|
||||
pure $ delayMeta r envb !(getTerm ty) tm
|
||||
let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
|
||||
let gdef = record { definition = PMDef (MkPMDefInfo NotHole True False)
|
||||
[] (STerm 0 tm') (STerm 0 tm') [] } def
|
||||
logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm'
|
||||
ignore $ addDef (Resolved hid) gdef
|
||||
@ -1490,7 +1490,7 @@ retryGuess mode smode (hid, (loc, hname))
|
||||
-- All constraints resolved, so turn into a
|
||||
-- proper definition and remove it from the
|
||||
-- hole list
|
||||
[] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
|
||||
[] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True False)
|
||||
[] (STerm 0 tm) (STerm 0 tm) [] } def
|
||||
logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm
|
||||
ignore $ addDef (Resolved hid) gdef
|
||||
|
@ -139,6 +139,10 @@ data CLOpt
|
||||
||| Use SHA256 hashes to determine if a source file needs rebuilding instead
|
||||
||| of modification time.
|
||||
HashesInsteadOfModTime |
|
||||
||| Use incremental code generation, if the backend supports it
|
||||
IncrementalCG String |
|
||||
||| Use whole program compilation - overrides IncrementalCG if set
|
||||
WholeProgram |
|
||||
||| Generate bash completion info
|
||||
BashCompletion String String |
|
||||
||| Generate bash completion script
|
||||
@ -209,6 +213,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
|
||||
(Just "Don't implicitly import Prelude"),
|
||||
MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
|
||||
(Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
|
||||
MkOpt ["--incremental-cg", "--inc"] [Required "backend"] (\f => [IncrementalCG f])
|
||||
(Just "Incremental code generation on given backend"),
|
||||
MkOpt ["--whole-program", "--wp"] [] [WholeProgram]
|
||||
(Just "Use whole program compilation (overrides --inc)"),
|
||||
MkOpt ["--directive"] [Required "directive"] (\d => [Directive d])
|
||||
(Just $ "Pass a directive to the current code generator"),
|
||||
MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])
|
||||
|
@ -43,38 +43,51 @@ findInput [] = Nothing
|
||||
findInput (InputFile f :: fs) = Just f
|
||||
findInput (_ :: fs) = findInput fs
|
||||
|
||||
setIncrementalCG : {auto c : Ref Ctxt Defs} ->
|
||||
String -> Core ()
|
||||
setIncrementalCG cgn
|
||||
= do defs <- get Ctxt
|
||||
case getCG (options defs) cgn of
|
||||
Just cg => setSession (record { incrementalCGs $= (cg :: )} !getSession)
|
||||
Nothing => pure ()
|
||||
|
||||
-- Add extra data from the "IDRIS2_x" environment variables
|
||||
updateEnv : {auto c : Ref Ctxt Defs} ->
|
||||
Core ()
|
||||
updateEnv
|
||||
= do defs <- get Ctxt
|
||||
bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX"
|
||||
the (Core ()) $ case bprefix of
|
||||
case bprefix of
|
||||
Just p => setPrefix p
|
||||
Nothing => setPrefix yprefix
|
||||
bpath <- coreLift $ idrisGetEnv "IDRIS2_PATH"
|
||||
the (Core ()) $ case bpath of
|
||||
case bpath of
|
||||
Just path => do traverseList1_ addExtraDir (map trim (split (==pathSeparator) path))
|
||||
Nothing => pure ()
|
||||
bdata <- coreLift $ idrisGetEnv "IDRIS2_DATA"
|
||||
the (Core ()) $ case bdata of
|
||||
case bdata of
|
||||
Just path => do traverseList1_ addDataDir (map trim (split (==pathSeparator) path))
|
||||
Nothing => pure ()
|
||||
blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"
|
||||
the (Core ()) $ case blibs of
|
||||
case blibs of
|
||||
Just path => do traverseList1_ addLibDir (map trim (split (==pathSeparator) path))
|
||||
Nothing => pure ()
|
||||
pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"
|
||||
the (Core ()) $ case pdirs of
|
||||
case pdirs of
|
||||
Just path => do traverseList1_ addPackageDir (map trim (split (==pathSeparator) path))
|
||||
Nothing => pure ()
|
||||
cg <- coreLift $ idrisGetEnv "IDRIS2_CG"
|
||||
the (Core ()) $ case cg of
|
||||
case cg of
|
||||
Just e => case getCG (options defs) e of
|
||||
Just cg => setCG cg
|
||||
Nothing => throw (InternalError ("Unknown code generator " ++ show e))
|
||||
Nothing => pure ()
|
||||
|
||||
inccgs <- coreLift $ idrisGetEnv "IDRIS2_INC_CGS"
|
||||
case inccgs of
|
||||
Just cgs =>
|
||||
traverse_ setIncrementalCG $
|
||||
map trim (toList (split (==',') cgs))
|
||||
Nothing => pure ()
|
||||
-- IDRIS2_PATH goes first so that it overrides this if there's
|
||||
-- any conflicts. In particular, that means that setting IDRIS2_PATH
|
||||
-- for the tests means they test the local version not the installed
|
||||
|
@ -27,6 +27,7 @@ envs = [
|
||||
MkEnvDesc "IDRIS2_DATA" "Places Idris2 looks for data files",
|
||||
MkEnvDesc "IDRIS2_LIBS" "Places Idris2 looks for libraries (for code generation)",
|
||||
MkEnvDesc "IDRIS2_CG" "Codegen backend",
|
||||
MkEnvDesc "IDRIS2_INC_CGS" "Code generators to use (comma separated) when compiling modules incrementally",
|
||||
MkEnvDesc "CHEZ" "chez executable used in Chez codegen",
|
||||
MkEnvDesc "RACKET" "racket executable used in Racket codegen",
|
||||
MkEnvDesc "RACKET_RACO" "raco executable used in Racket codegen",
|
||||
|
@ -174,6 +174,8 @@ pwarning (ShadowingGlobalDefs _ ns)
|
||||
|
||||
pwarning (Deprecated s)
|
||||
= pure $ pretty "Deprecation warning:" <++> pretty s
|
||||
pwarning (GenericWarn s)
|
||||
= pure $ pretty s
|
||||
|
||||
export
|
||||
perror : {auto c : Ref Ctxt Defs} ->
|
||||
|
@ -341,11 +341,26 @@ copyFile src dest
|
||||
| Left err => pure (Left err)
|
||||
writeToFile dest buf
|
||||
|
||||
installFrom : {auto c : Ref Ctxt Defs} ->
|
||||
installFrom : {auto o : Ref ROpts REPLOpts} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
String -> String -> ModuleIdent -> Core ()
|
||||
installFrom builddir destdir ns
|
||||
= do let ttcfile = ModuleIdent.toPath ns
|
||||
let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
|
||||
objPaths_in <- traverse
|
||||
(\cg =>
|
||||
do Just cgdata <- getCG cg
|
||||
| Nothing => pure Nothing
|
||||
let Just ext = incExt cgdata
|
||||
| Nothing => pure Nothing
|
||||
let srcFile = builddir </> "ttc" </> ttcfile <.> ext
|
||||
let destFile = destdir </> ttcfile <.> ext
|
||||
let Just (dir, _) = splitParent destFile
|
||||
| Nothing => pure Nothing
|
||||
ensureDirectoryExists dir
|
||||
pure $ Just (srcFile, destFile))
|
||||
(incrementalCGs !getSession)
|
||||
let objPaths = mapMaybe id objPaths_in
|
||||
|
||||
let modPath = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
|
||||
let destNest = joinPath modPath
|
||||
@ -361,6 +376,13 @@ installFrom builddir destdir ns
|
||||
| Left err => throw $ InternalError $ unlines
|
||||
[ "Can't copy file " ++ ttcPath ++ " to " ++ destPath
|
||||
, show err ]
|
||||
-- Copy object files, if any. They don't necessarily get created,
|
||||
-- since some modules don't generate any code themselves.
|
||||
traverse_ (\ (obj, dest) =>
|
||||
do coreLift $ putStrLn $ "Installing " ++ obj ++ " to " ++ destPath
|
||||
ignore $ coreLift $ copyFile obj dest)
|
||||
objPaths
|
||||
|
||||
pure ()
|
||||
|
||||
installSrcFrom : {auto c : Ref Ctxt Defs} ->
|
||||
|
@ -1,5 +1,13 @@
|
||||
module Idris.ProcessIdr
|
||||
|
||||
import Compiler.RefC.RefC
|
||||
import Compiler.Scheme.Chez
|
||||
import Compiler.Scheme.ChezSep
|
||||
import Compiler.Scheme.Racket
|
||||
import Compiler.Scheme.Gambit
|
||||
import Compiler.ES.Node
|
||||
import Compiler.ES.Javascript
|
||||
import Compiler.Common
|
||||
import Compiler.Inline
|
||||
|
||||
import Core.Binary
|
||||
@ -29,7 +37,9 @@ import Idris.Pretty
|
||||
|
||||
import Data.List
|
||||
import Libraries.Data.NameMap
|
||||
import Libraries.Utils.Path
|
||||
|
||||
import System
|
||||
import System.File
|
||||
|
||||
%default covering
|
||||
@ -150,6 +160,7 @@ readAsMain fname
|
||||
= do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}
|
||||
True EmptyFC True fname (nsAsModuleIdent emptyNS) emptyNS
|
||||
| Nothing => throw (InternalError "Already loaded")
|
||||
|
||||
replNS <- getNS
|
||||
replNestedNS <- getNestedNS
|
||||
extendSyn syn
|
||||
@ -225,6 +236,25 @@ unchangedHash sourceFileName ttcFileName
|
||||
(storedSourceHash, _) <- readHashes ttcFileName
|
||||
pure $ sourceCodeHash == storedSourceHash
|
||||
|
||||
export
|
||||
getCG : {auto o : Ref ROpts REPLOpts} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
CG -> Core (Maybe Codegen)
|
||||
getCG Chez = pure $ Just codegenChez
|
||||
getCG ChezSep = pure $ Just codegenChezSep
|
||||
getCG Racket = pure $ Just codegenRacket
|
||||
getCG Gambit = pure $ Just codegenGambit
|
||||
getCG Node = pure $ Just codegenNode
|
||||
getCG Javascript = pure $ Just codegenJavascript
|
||||
getCG RefC = pure $ Just codegenRefC
|
||||
getCG (Other s) = getCodegen s
|
||||
|
||||
export
|
||||
findCG : {auto o : Ref ROpts REPLOpts} ->
|
||||
{auto c : Ref Ctxt Defs} -> Core (Maybe Codegen)
|
||||
findCG
|
||||
= do defs <- get Ctxt
|
||||
getCG (codegen (session (options defs)))
|
||||
|
||||
||| Process everything in the module; return the syntax information which
|
||||
||| needs to be written to the TTC (e.g. exported infix operators)
|
||||
@ -341,6 +371,17 @@ process buildmsg sourceFileName ident
|
||||
do defs <- get Ctxt
|
||||
ns <- ctxtPathToNS sourceFileName
|
||||
makeBuildDirectory ns
|
||||
|
||||
traverse_
|
||||
(\cg =>
|
||||
do Just cgdata <- getCG cg
|
||||
| Nothing =>
|
||||
coreLift $ putStrLn $ "No incremental code generator for " ++ show cg
|
||||
Just res <- incCompile cgdata sourceFileName
|
||||
| Nothing => pure ()
|
||||
setIncData cg res)
|
||||
(incrementalCGs !getSession)
|
||||
|
||||
writeToTTC !(get Syn) sourceFileName ttcFileName
|
||||
ttmFileName <- getTTCFileName sourceFileName "ttm"
|
||||
writeToTTM ttmFileName
|
||||
|
@ -207,24 +207,6 @@ getOptions = do
|
||||
, Editor (editor opts)
|
||||
]
|
||||
|
||||
export
|
||||
findCG : {auto o : Ref ROpts REPLOpts} ->
|
||||
{auto c : Ref Ctxt Defs} -> Core Codegen
|
||||
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
|
||||
Javascript => pure codegenJavascript
|
||||
RefC => pure codegenRefC
|
||||
Other s => case !(getCodegen s) of
|
||||
Just cg => pure cg
|
||||
Nothing => do coreLift_ $ putStrLn ("No such code generator: " ++ s)
|
||||
coreLift $ exitWith (ExitFailure 1)
|
||||
|
||||
anyAt : (a -> Bool) -> a -> b -> Bool
|
||||
anyAt p loc _ = p loc
|
||||
|
||||
@ -598,7 +580,11 @@ execExp : {auto c : Ref Ctxt Defs} ->
|
||||
PTerm -> Core REPLResult
|
||||
execExp ctm
|
||||
= do tm_erased <- prepareExp ctm
|
||||
execute !findCG tm_erased
|
||||
Just cg <- findCG
|
||||
| Nothing =>
|
||||
do iputStrLn (reflow "No such code generator available")
|
||||
pure CompilationFailed
|
||||
execute cg tm_erased
|
||||
pure $ Executed ctm
|
||||
|
||||
|
||||
@ -628,7 +614,11 @@ compileExp : {auto c : Ref Ctxt Defs} ->
|
||||
PTerm -> String -> Core REPLResult
|
||||
compileExp ctm outfile
|
||||
= do tm_erased <- prepareExp ctm
|
||||
ok <- compile !findCG tm_erased outfile
|
||||
Just cg <- findCG
|
||||
| Nothing =>
|
||||
do iputStrLn (reflow "No such code generator available")
|
||||
pure CompilationFailed
|
||||
ok <- compile cg tm_erased outfile
|
||||
maybe (pure CompilationFailed)
|
||||
(pure . Compiled)
|
||||
ok
|
||||
|
@ -349,7 +349,20 @@ preOptions (IgnoreShadowingWarnings :: opts)
|
||||
= do setSession (record { showShadowingWarning = False } !getSession)
|
||||
preOptions opts
|
||||
preOptions (HashesInsteadOfModTime :: opts)
|
||||
= do setSession (record {checkHashesInsteadOfModTime = True} !getSession)
|
||||
= do setSession (record { checkHashesInsteadOfModTime = True } !getSession)
|
||||
preOptions opts
|
||||
preOptions (IncrementalCG e :: opts)
|
||||
= do defs <- get Ctxt
|
||||
case getCG (options defs) e of
|
||||
Just cg => do setSession (record { incrementalCGs $= (cg :: )} !getSession)
|
||||
preOptions opts
|
||||
Nothing =>
|
||||
do coreLift $ putStrLn "No such code generator"
|
||||
coreLift $ putStrLn $ "Code generators available: " ++
|
||||
showSep ", " (map fst (availableCGs (options defs)))
|
||||
coreLift $ exitWith (ExitFailure 1)
|
||||
preOptions (WholeProgram :: opts)
|
||||
= do setSession (record { wholeProgram = True } !getSession)
|
||||
preOptions opts
|
||||
preOptions (BashCompletion a b :: _)
|
||||
= do os <- opts a b
|
||||
|
@ -253,7 +253,8 @@ retryDelayed' errmode acc (d@(_, i, hints, elab) :: ds)
|
||||
let ds' = reverse (delayedElab ust) ++ ds
|
||||
|
||||
updateDef (Resolved i) (const (Just
|
||||
(PMDef (MkPMDefInfo NotHole True) [] (STerm 0 tm) (STerm 0 tm) [])))
|
||||
(PMDef (MkPMDefInfo NotHole True False)
|
||||
[] (STerm 0 tm) (STerm 0 tm) [])))
|
||||
logTerm "elab.update" 5 ("Resolved delayed hole " ++ show i) tm
|
||||
logTermNF "elab.update" 5 ("Resolved delayed hole NF " ++ show i) [] tm
|
||||
removeHole i
|
||||
|
@ -54,7 +54,7 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty)
|
||||
-- Record the LHS for this hole in the metadata
|
||||
withCurrentLHS (Resolved idx)
|
||||
addNameLoc fc nm
|
||||
addUserHole nm
|
||||
addUserHole False nm
|
||||
saveHole nm
|
||||
pure (metaval, gexpty)
|
||||
checkHole rig elabinfo nest env fc n_in exp
|
||||
@ -71,6 +71,6 @@ checkHole rig elabinfo nest env fc n_in exp
|
||||
(idx, metaval) <- metaVarI fc rig env' nm ty
|
||||
withCurrentLHS (Resolved idx)
|
||||
addNameLoc fc nm
|
||||
addUserHole nm
|
||||
addUserHole False nm
|
||||
saveHole nm
|
||||
pure (metaval, gnf env ty)
|
||||
|
@ -871,11 +871,16 @@ processDef opts nest env fc n_in cs_in
|
||||
do t <- toFullNames tree_ct
|
||||
pure ("Case tree for " ++ show n ++ ": " ++ show t)
|
||||
|
||||
-- check whether the name was declared in a different source file
|
||||
defs <- get Ctxt
|
||||
let pi = case lookup n (userHoles defs) of
|
||||
Nothing => defaultPI
|
||||
Just e => record { externalDecl = e } defaultPI
|
||||
-- Add compile time tree as a placeholder for the runtime tree,
|
||||
-- but we'll rebuild that in a later pass once all the case
|
||||
-- blocks etc are resolved
|
||||
ignore $ addDef (Resolved nidx)
|
||||
(record { definition = PMDef defaultPI cargs tree_ct tree_ct pats
|
||||
(record { definition = PMDef pi cargs tree_ct tree_ct pats
|
||||
} gdef)
|
||||
|
||||
when (visibility gdef == Public) $
|
||||
|
@ -203,7 +203,7 @@ initDef : {vars : _} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Name -> Env Term vars -> Term vars -> List FnOpt -> Core Def
|
||||
initDef n env ty []
|
||||
= do addUserHole n
|
||||
= do addUserHole False n
|
||||
pure None
|
||||
initDef n env ty (ExternFn :: opts)
|
||||
= do defs <- get Ctxt
|
||||
|
Loading…
Reference in New Issue
Block a user