idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

[ doc ] add comments to generated javascript (#2594)

Browse Source
This commit is contained in:
G. Allais 2022-07-18 17:30:56 +01:00 committed by GitHub
parent 8ecb1aaf95
commit 84a504738c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
18 changed files with 285 additions and 136 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
CHANGELOG.md
View File

@ -64,6 +64,9 @@
+ For example, `langversion >= 0.5.1`.
* Alternatives for primitive types of the `Core.TT.Constant` are moved out to a separate data type `PrimTypes`.
Signatures of functions that were working with `Constant` are changed to use `PrimTypes` when appropriate.
* Codegens now take an additional `Ref Syn SyntaxInfo` argument. This empowers
compiler writers to pretty print core terms e.g. to add comments with the
original type annotations in the generated code.
### IDE protocol changes

24
src/Compiler/Common.idr
View File

@ -24,6 +24,7 @@ import Data.List1
import Libraries.Data.NameMap
import Data.String as String
import Idris.Syntax
import Idris.Env
import System.Directory
@ -36,17 +37,19 @@ public export
record Codegen where
constructor MkCG
||| Compile an Idris 2 expression, saving it to a file.
compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
(tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
||| Execute an Idris 2 expression directly.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
(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 ->
incCompileFile : Maybe (Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
(sourcefile : String) ->
Core (Maybe (String, List String)))
||| If incremental compilation is supported, get the output file extension
@ -99,36 +102,39 @@ record CompileData where
||| that executes the `compileExpr` method of the Codegen
export
compile : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Codegen ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile {c} cg tm out
compile {c} {s} cg tm out
= do d <- getDirs
let tmpDir = execBuildDir d
let outputDir = outputDirWithDefault d
ensureDirectoryExists tmpDir
ensureDirectoryExists outputDir
logTime 1 "Code generation overall" $
compileExpr cg c tmpDir outputDir tm out
compileExpr cg c s tmpDir outputDir tm out
||| execute
||| As with `compile`, produce a functon that executes
||| the `executeExpr` method of the given Codegen
export
execute : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Codegen -> ClosedTerm -> Core ()
execute {c} cg tm
execute {c} {s} cg tm
= do d <- getDirs
let tmpDir = execBuildDir d
ensureDirectoryExists tmpDir
executeExpr cg c tmpDir tm
executeExpr cg c s tmpDir tm
export
incCompile : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Codegen -> String -> Core (Maybe (String, List String))
incCompile {c} cg src
incCompile {c} {s} cg src
= do let Just inc = incCompileFile cg
| Nothing => pure Nothing
inc c src
inc c s 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

14
src/Compiler/ES/Ast.idr
View File

@ -7,6 +7,16 @@ import Data.Vect
%default total
public export
data Tag : Type where
||| A data constructor. Use the tag to dispatch / construct.
||| Here the Name is only for documentation purposes and should not
||| be used.
DataCon : (tag : Int) -> (name : Name) -> Tag
||| A type constructor. We do not have a unique tag associated to types
||| and so we match on names instead.
TypeCon : (name : Name) -> Tag
||| A variable in a toplevel function definition
|||
||| When generating the syntax tree of imperative
@ -84,7 +94,7 @@ mutual
||| The tag either represents the name of a type constructor
||| (when we are pattern matching on types) or the index
||| of a data constructor.
ECon : (tag : Either Int Name) -> ConInfo -> List Exp -> Exp
ECon : (tag : Tag) -> ConInfo -> List Exp -> Exp
||| Primitive operation
EOp : {0 arity : Nat} -> PrimFn arity -> Vect arity Exp -> Exp
@ -165,7 +175,7 @@ mutual
public export
record EConAlt (e : Effect) where
constructor MkEConAlt
tag : Either Int Name
tag : Tag
conInfo : ConInfo
body : Stmt (Just e)

95
src/Compiler/ES/Codegen.idr
View File

@ -3,8 +3,11 @@ module Compiler.ES.Codegen
import Compiler.Common
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Options
import Core.Env
import Core.Normalise
import Data.List1
import Data.String
import Compiler.ES.Ast
@ -17,6 +20,10 @@ import Libraries.Data.SortedMap
import Protocol.Hex
import Libraries.Data.String.Extra
import Idris.Pretty.Annotations
import Idris.Syntax
import Idris.Doc.String
import Data.Vect
--------------------------------------------------------------------------------
@ -131,9 +138,9 @@ parameters (noMangle : NoMangleMap)
minimal (MVar v) = var v
minimal (MProjection n v) = minimal v <+> ".a" <+> shown n
tag2es : Either Int Name -> Doc
tag2es (Left x) = shown x
tag2es (Right x) = jsStringDoc $ show x
tag2es : Tag -> (Doc, Maybe Doc)
tag2es (DataCon i n) = (shown i, Just (shown (dropNS n)))
tag2es (TypeCon x) = (jsStringDoc $ show x, Nothing)
constant : Doc -> Doc -> Doc
constant n d = "const" <++> n <+> softEq <+> d <+> ";"
@ -156,14 +163,19 @@ applyObj = applyList "{" "}" softComma
-- Exceptions based on the given `ConInfo`:
-- `NIL` and `NOTHING`-like data constructors are represented as `{h: 0}`,
-- while `CONS`, `JUST`, and `RECORD` come without the header field.
applyCon : ConInfo -> (tag : Either Int Name) -> (args : List Doc) -> Doc
applyCon : ConInfo -> (tag : Tag) -> (args : List Doc) -> Doc
applyCon NIL _ [] = "{h" <+> softColon <+> "0}"
applyCon NOTHING _ [] = "{h" <+> softColon <+> "0}"
applyCon CONS _ as = applyObj (conTags as)
applyCon JUST _ as = applyObj (conTags as)
applyCon RECORD _ as = applyObj (conTags as)
applyCon UNIT _ [] = "undefined"
applyCon _ t as = applyObj (("h" <+> softColon <+> tag2es t)::conTags as)
applyCon _ t as = applyObj (mkCon (tag2es t) :: conTags as)
where
mkCon : (Doc, Maybe Doc) -> Doc
mkCon (t, Nothing) = "h" <+> softColon <+> t
mkCon (t, Just cmt) = "h" <+> softColon <+> t <++> comment cmt
-- applys the given list of arguments to the given function.
app : (fun : Doc) -> (args : List Doc) -> Doc
@ -591,30 +603,32 @@ isFun _ = True
-- case blocks (the first entry in a pair is the value belonging
-- to a `case` statement, the second is the body
--
-- Example: switch "foo.a1" [("0","return 2;")] (Just "return 0;")
-- Example: switch "foo.a1" [(("0", Just "True"),"return 2;")] (Just "return 0;")
-- generates the following code:
-- ```javascript
-- switch(foo.a1) {
-- case 0: return 2;
-- case 0: /* True */ return 2;
-- default: return 0;
-- }
-- ```
switch : (scrutinee : Doc)
-> (alts : List (Doc,Doc))
-> (alts : List ((Doc,Maybe Doc),Doc)) -- match, comment, code
-> (def : Maybe Doc)
-> Doc
switch sc alts def =
let stmt = "switch" <+> paren sc <+> SoftSpace
defcase = concatMap (pure . anyCase "default") def
defcase = concatMap (pure . anyCase "default" Nothing) def
in stmt <+> block (vcat $ map alt alts ++ defcase)
where anyCase : Doc -> Doc -> Doc
anyCase s d =
let b = if isMultiline d then block d else d
in s <+> softColon <+> b
where anyCase : Doc -> Maybe Doc -> Doc -> Doc
anyCase s cmt d =
let b = if isMultiline d then block d else d in
case cmt of
Nothing => s <+> softColon <+> b
Just cmt => s <+> softColon <+> comment cmt <++> b
alt : (Doc,Doc) -> Doc
alt (e,d) = anyCase ("case" <++> e) d
alt : ((Doc,Maybe Doc),Doc) -> Doc
alt ((e, c), d) = anyCase ("case" <++> e) c d
-- creates an argument list for a (possibly multi-argument)
-- anonymous function. An empty argument list is treated
@ -623,7 +637,7 @@ lambdaArgs : (noMangle : NoMangleMap) -> List Var -> Doc
lambdaArgs noMangle [] = "()" <+> lambdaArrow
lambdaArgs noMangle xs = hcat $ (<+> lambdaArrow) . var noMangle <$> xs
insertBreak : (r : Effect) -> (Doc, Doc) -> (Doc, Doc)
insertBreak : (r : Effect) -> (a, Doc) -> (a, Doc)
insertBreak Returns x = x
insertBreak (ErrorWithout _) (pat, exp) = (pat, vcat [exp, "break;"])
@ -678,13 +692,13 @@ mutual
nm <- get NoMangleMap
pure $ switch (minimal nm sc <+> ".h") as d
where
alt : {r : _} -> EConAlt r -> Core (Doc,Doc)
alt (MkEConAlt _ RECORD b) = ("undefined",) <$> stmt b
alt (MkEConAlt _ NIL b) = ("0",) <$> stmt b
alt (MkEConAlt _ CONS b) = ("undefined",) <$> stmt b
alt (MkEConAlt _ NOTHING b) = ("0",) <$> stmt b
alt (MkEConAlt _ JUST b) = ("undefined",) <$> stmt b
alt (MkEConAlt _ UNIT b) = ("undefined",) <$> stmt b
alt : {r : _} -> EConAlt r -> Core ((Doc,Maybe Doc),Doc)
alt (MkEConAlt _ RECORD b) = (("undefined",Just "record"),) <$> stmt b
alt (MkEConAlt _ NIL b) = (("0",Just "nil"),) <$> stmt b
alt (MkEConAlt _ CONS b) = (("undefined",Just "cons"),) <$> stmt b
alt (MkEConAlt _ NOTHING b) = (("0",Just "nothing"),) <$> stmt b
alt (MkEConAlt _ JUST b) = (("undefined",Just "just"),) <$> stmt b
alt (MkEConAlt _ UNIT b) = (("undefined",Just "unit"),) <$> stmt b
alt (MkEConAlt t _ b) = (tag2es t,) <$> stmt b
stmt (ConstSwitch r sc alts def) = do
@ -693,10 +707,10 @@ mutual
ex <- exp sc
pure $ switch ex as d
where
alt : EConstAlt r -> Core (Doc,Doc)
alt : EConstAlt r -> Core ((Doc,Maybe Doc),Doc)
alt (MkEConstAlt c b) = do
d <- stmt b
pure (Text $ jsConstant c, d)
pure ((Text $ jsConstant c, Nothing), d)
stmt (Error x) = pure $ jsCrashExp (jsStringDoc x) <+> ";"
stmt (Block ss s) = do
@ -712,24 +726,38 @@ printDoc Compact y = compact y
printDoc Minimal y = compact y
-- generate code for the given toplevel function.
def : {auto c : Ref ESs ESSt}
def : {auto c : Ref Ctxt Defs}
-> {auto s : Ref Syn SyntaxInfo}
-> {auto e : Ref ESs ESSt}
-> {auto nm : Ref NoMangleMap NoMangleMap}
-> Function
-> Core String
def (MkFunction n as body) = do
reset
defs <- get Ctxt
mty <- do log "compiler.javascript.doc" 50 $ "Looking up \{show n}"
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure Nothing
let UN _ = dropNS n
| _ => pure Nothing
ty <- prettyType (const ()) gdef.type
pure (Just (shown ty))
ref <- getOrRegisterRef n
args <- traverse registerLocal as
mde <- mode <$> get ESs
b <- stmt Returns body >>= stmt
let cmt = comment $ hsep (shown n :: toList ((":" <++>) <$> mty))
case args of
-- zero argument toplevel functions are converted to
-- lazily evaluated constants.
[] => pure $ printDoc mde $
constant (var !(get NoMangleMap) ref) (
"__lazy(" <+> function neutral [] b <+> ")"
)
_ => pure $ printDoc mde $ function (var !(get NoMangleMap) ref) (map (var !(get NoMangleMap)) args) b
[] => pure $ printDoc mde $ vcat
[ cmt
, constant (var !(get NoMangleMap) ref)
("__lazy(" <+> function neutral [] b <+> ")") ]
_ => pure $ printDoc mde $ vcat
[ cmt
, function (var !(get NoMangleMap) ref)
(map (var !(get NoMangleMap)) args) b ]
-- generate code for the given foreign function definition
foreign : {auto c : Ref ESs ESSt}
@ -759,8 +787,9 @@ validJSName name =
||| Compiles the given `ClosedTerm` for the list of supported
||| backends to JS code.
export
compileToES : Ref Ctxt Defs -> (cg : CG) -> ClosedTerm -> List String -> Core String
compileToES c cg tm ccTypes = do
compileToES : Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
(cg : CG) -> ClosedTerm -> List String -> Core String
compileToES c s cg tm ccTypes = do
_ <- initNoMangle "javascript" validJSName
cdata <- getCompileData False Cases tm

8
src/Compiler/ES/Doc.idr
View File

@ -9,6 +9,7 @@ data Doc
= Nil
| LineBreak
| SoftSpace -- this will be ignored in compact printing
| Comment Doc -- this will be ignored in compact printing
| Text String
| Nest Nat Doc
| Seq Doc Doc
@ -27,6 +28,10 @@ public export %inline
shown : Show a => a -> Doc
shown a = Text (show a)
export %inline
comment : Doc -> Doc
comment = Comment
export
FromString Doc where
fromString = Text
@ -37,6 +42,7 @@ isMultiline [] = False
isMultiline LineBreak = True
isMultiline SoftSpace = False
isMultiline (Text x) = False
isMultiline (Comment x) = isMultiline x
isMultiline (Nest k x) = isMultiline x
isMultiline (Seq x y) = isMultiline x || isMultiline y
@ -87,6 +93,7 @@ compact = fastConcat . go
go Nil = []
go LineBreak = []
go SoftSpace = []
go (Comment _) = []
go (Text x) = [x]
go (Nest _ y) = go y
go (Seq x y) = go x ++ go y
@ -101,6 +108,7 @@ pretty = fastConcat . go ""
go _ Nil = []
go s LineBreak = ["\n",s]
go _ SoftSpace = [" "]
go s (Comment x) = "/* " :: go s x ++ [" */"]
go _ (Text x) = [x]
go s (Nest x y) = go (s ++ nSpaces x) y
go s (Seq x y) = go s x ++ go s y

35
src/Compiler/ES/Javascript.idr
View File

@ -10,14 +10,18 @@ import Core.TT
import Core.Options
import Libraries.Utils.Path
import Idris.Syntax
import Data.String
%default covering
||| Compile a TT expression to Javascript
compileToJS : Ref Ctxt Defs ->
ClosedTerm -> Core String
compileToJS c tm = compileToES c Javascript tm ["browser", "javascript"]
compileToJS :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
ClosedTerm -> Core String
compileToJS c s tm = compileToES c s Javascript tm ["browser", "javascript"]
htmlHeader : String
htmlHeader = """
@ -45,22 +49,27 @@ addHeaderAndFooter outfile es =
_ => es
||| Javascript implementation of the `compileExpr` interface.
compileExpr : Ref Ctxt Defs
-> (tmpDir : String)
-> (outputDir : String)
-> ClosedTerm
-> (outfile : String)
-> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile =
do es <- compileToJS c tm
compileExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) ->
(outputDir : String) ->
ClosedTerm ->
(outfile : String) ->
Core (Maybe String)
compileExpr c s tmpDir outputDir tm outfile =
do es <- compileToJS c s tm
let res = addHeaderAndFooter outfile es
let out = outputDir </> outfile
Core.writeFile out res
pure (Just out)
||| Node implementation of the `executeExpr` interface.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm =
executeExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c s tmpDir tm =
throw $ InternalError "Javascript backend is only able to compile, use Node instead"
||| Codegen wrapper for Javascript implementation.

36
src/Compiler/ES/Node.idr
View File

@ -2,6 +2,7 @@
module Compiler.ES.Node
import Idris.Env
import Idris.Syntax
import Compiler.ES.Codegen
@ -26,32 +27,39 @@ findNode = do
pure $ fromMaybe "/usr/bin/env node" path
||| Compile a TT expression to Node
compileToNode : Ref Ctxt Defs -> ClosedTerm -> Core String
compileToNode c tm = compileToES c Node tm ["node", "javascript"]
compileToNode :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
ClosedTerm -> Core String
compileToNode c s tm = compileToES c s Node tm ["node", "javascript"]
||| Node implementation of the `compileExpr` interface.
compileExpr : Ref Ctxt Defs
-> (tmpDir : String)
-> (outputDir : String)
-> ClosedTerm
-> (outfile : String)
-> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile =
do es <- compileToNode c tm
compileExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) ->
(outputDir : String) ->
ClosedTerm ->
(outfile : String) ->
Core (Maybe String)
compileExpr c s tmpDir outputDir tm outfile =
do es <- compileToNode c s tm
let out = outputDir </> outfile
Core.writeFile out es
pure (Just out)
||| Node implementation of the `executeExpr` interface.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm =
executeExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c s tmpDir tm =
do let outn = tmpDir </> "_tmp_node.js"
js <- compileToNode c tm
js <- compileToNode c s tm
Core.writeFile outn js
node <- coreLift findNode
quoted_node <- pure $ "\"" ++ node ++ "\"" -- Windows often have a space in the path.
coreLift_ $ system (quoted_node ++ " " ++ outn)
pure ()
||| Codegen wrapper for Node implementation.
export

5
src/Compiler/ES/ToAst.idr
View File

@ -13,8 +13,9 @@ import Compiler.ES.State
--------------------------------------------------------------------------------
-- used to convert data and type constructor tags
tag : Name -> Maybe Int -> Either Int Name
tag n = maybe (Right n) Left
tag : Name -> Maybe Int -> Tag
tag n Nothing = TypeCon n
tag n (Just i) = DataCon i n
-- creates a single assignment statement.
assign : (e : Effect) -> Exp -> Stmt (Just e)

19
src/Compiler/Interpreter/VMCode.idr
View File

@ -1,13 +1,16 @@
module Compiler.Interpreter.VMCode
import Core.Core
import Core.Context
import Core.Context.Log
import Core.Primitives
import Core.Value
import Compiler.Common
import Compiler.VMCode
import Idris.Syntax
import Libraries.Data.IOArray
import Libraries.Data.NameMap
import Data.Nat
@ -281,11 +284,17 @@ parameters {auto c : Ref Ctxt Defs}
when logCallStack $ coreLift $ putStrLn $ ind ++ "Result: " ++ show res
pure res
compileExpr : Ref Ctxt Defs -> String -> String -> ClosedTerm -> String -> Core (Maybe String)
compileExpr _ _ _ _ _ = Nothing <$ throw {a=()} (InternalError "compile not implemeted for vmcode-interp")
compileExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
String -> String -> ClosedTerm -> String -> Core (Maybe String)
compileExpr _ _ _ _ _ _ = throw (InternalError "compile not implemeted for vmcode-interp")
executeExpr : Ref Ctxt Defs -> String -> ClosedTerm -> Core ()
executeExpr c _ tm = do
executeExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
String -> ClosedTerm -> Core ()
executeExpr c s _ tm = do
cdata <- getCompileData False VMCode tm
st <- newRef State !(initInterpState cdata.vmcode)
ignore $ callFunc [] (MN "__mainExpression" 0) []

14
src/Compiler/RefC/RefC.idr
View File

@ -11,6 +11,8 @@ import Core.Context
import Core.Context.Log
import Core.Directory
import Idris.Syntax
import Data.List
import Libraries.Data.DList
import Data.Nat
@ -1062,12 +1064,13 @@ generateCSourceFile defs outn =
export
compileExpr : UsePhase
-> Ref Ctxt Defs
-> Ref Syn SyntaxInfo
-> (tmpDir : String)
-> (outputDir : String)
-> ClosedTerm
-> (outfile : String)
-> Core (Maybe String)
compileExpr ANF c _ outputDir tm outfile =
compileExpr ANF c s _ outputDir tm outfile =
do let outn = outputDir </> outfile ++ ".c"
let outobj = outputDir </> outfile ++ ".o"
let outexec = outputDir </> outfile
@ -1081,15 +1084,16 @@ compileExpr ANF c _ outputDir tm outfile =
| Nothing => pure Nothing
compileCFile outobj outexec
compileExpr _ _ _ _ _ _ = pure Nothing
compileExpr _ _ _ _ _ _ _ = pure Nothing
export
executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm = do
executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
(execDir : String) -> ClosedTerm -> Core ()
executeExpr c s tmpDir tm = do
do let outfile = "_tmp_refc"
Just _ <- compileExpr ANF c tmpDir tmpDir tm outfile
Just _ <- compileExpr ANF c s tmpDir tmpDir tm outfile
| Nothing => do coreLift_ $ putStrLn "Error: failed to compile"
coreLift_ $ system (tmpDir </> outfile)

58
src/Compiler/Scheme/Chez.idr
View File

@ -21,6 +21,7 @@ import Data.String
import Data.Vect
import Idris.Env
import Idris.Syntax
import System
import System.Directory
@ -534,9 +535,13 @@ makeShWindows chez outShRel appdir outAbs progType
| Left err => throw (FileErr outShRel err)
pure ()
compileExprWhole : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExprWhole makeitso c tmpDir outputDir tm outfile
compileExprWhole :
Bool ->
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExprWhole makeitso c s tmpDir outputDir tm outfile
= do let appDirRel = outfile ++ "_app" -- relative to build dir
let appDirGen = outputDir </> appDirRel -- relative to here
coreLift_ $ mkdirAll appDirGen
@ -558,14 +563,18 @@ compileExprWhole 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
compileExprInc :
Bool ->
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExprInc makeitso c s 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
compileExprWhole makeitso c s tmpDir outputDir tm outfile
let appDirRel = outfile ++ "_app" -- relative to build dir
let appDirGen = outputDir </> appDirRel -- relative to here
coreLift_ $ mkdirAll appDirGen
@ -585,25 +594,34 @@ compileExprInc makeitso c tmpDir outputDir tm outfile
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
compileExpr :
Bool ->
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c s tmpDir outputDir tm outfile
= do sesh <- getSession
if not (wholeProgram sesh) && (Chez `elem` incrementalCGs sesh)
then compileExprInc makeitso c s tmpDir outputDir tm outfile
else compileExprWhole makeitso c s 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 ()
executeExpr c tmpDir tm
= do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
executeExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c s tmpDir tm
= do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpchez"
| Nothing => throw (InternalError "compileExpr returned Nothing")
coreLift_ $ system sh
incCompile : Ref Ctxt Defs ->
(sourceFile : String) -> Core (Maybe (String, List String))
incCompile c sourceFile
incCompile :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(sourceFile : String) -> Core (Maybe (String, List String))
incCompile c s sourceFile
= do
ssFile <- getTTCFileName sourceFile "ss"
soFile <- getTTCFileName sourceFile "so"

20
src/Compiler/Scheme/ChezSep.idr
View File

@ -21,6 +21,7 @@ import Data.List1
import Data.String
import Idris.Env
import Idris.Syntax
import System
import System.Directory
@ -260,9 +261,13 @@ makeShWindows chez outShRel appDirSh targetSh = do
Core.writeFile outShRel (startChezWinSh chez appDirSh targetSh)
||| Chez Scheme implementation of the `compileExpr` interface.
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c tmpDir outputDir tm outfile = do
compileExpr :
Bool ->
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c s tmpDir outputDir tm outfile = do
-- set up paths
Just cwd <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
@ -306,9 +311,12 @@ compileExpr makeitso c tmpDir outputDir tm outfile = do
||| Chez Scheme implementation of the `executeExpr` interface.
||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
= do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
executeExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c s tmpDir tm
= do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpchez"
| Nothing => throw (InternalError "compileExpr returned Nothing")
coreLift_ $ system sh

19
src/Compiler/Scheme/Gambit.idr
View File

@ -18,6 +18,7 @@ import Data.Maybe
import Data.Vect
import Idris.Env
import Idris.Syntax
import System
import System.Directory
@ -374,9 +375,12 @@ compileToSCM c tm outfile
| Left err => throw (FileErr outfile err)
pure $ mapMaybe fst fgndefs
compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile
compileExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c s tmpDir outputDir tm outfile
= do let srcPath = tmpDir </> outfile <.> "scm"
let execPath = outputDir </> outfile
libsname <- compileToSCM c tm srcPath
@ -396,9 +400,12 @@ compileExpr c tmpDir outputDir tm outfile
then pure (Just execPath)
else pure Nothing
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
= do Just sh <- compileExpr c tmpDir tmpDir tm "_tmpgambit"
executeExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c s tmpDir tm
= do Just sh <- compileExpr c s tmpDir tmpDir tm "_tmpgambit"
| Nothing => throw (InternalError "compileExpr returned Nothing")
coreLift_ $ system sh -- TODO: on windows, should add exe extension
pure ()

20
src/Compiler/Scheme/Racket.idr
View File

@ -20,6 +20,7 @@ import Data.String
import Data.Vect
import Idris.Env
import Idris.Syntax
import System
import System.Directory
@ -422,9 +423,13 @@ makeShWindows racket outShRel appdir outAbs
| Left err => throw (FileErr outShRel err)
pure ()
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr mkexec c tmpDir outputDir tm outfile
compileExpr :
Bool ->
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr mkexec c s tmpDir outputDir tm outfile
= do let appDirRel = outfile ++ "_app" -- relative to build dir
let appDirGen = outputDir </> appDirRel -- relative to here
coreLift_ $ mkdirAll appDirGen
@ -460,9 +465,12 @@ compileExpr mkexec c tmpDir outputDir tm outfile
pure (Just outShRel)
else pure Nothing
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
= do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpracket"
executeExpr :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c s tmpDir tm
= do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpracket"
| Nothing => throw (InternalError "compileExpr returned Nothing")
coreLift_ $ system sh

1
src/Core/Options/Log.idr
View File

@ -57,6 +57,7 @@ knownTopics = [
("compiler.inline.eval", Just "Log function definitions before and after inlining."),
("compiler.inline.heuristic", Just "Log names the inlining heuristic(s) have decided to inline."),
("compiler.interpreter", Just "Log the call-stack of the VMCode interpreter."),
("compiler.javascript.doc", Just "Generating doc comments for the JS backend."),
("compiler.refc", Nothing),
("compiler.refc.cc", Nothing),
("compiler.scheme.chez", Nothing),

28
src/Idris/Doc/String.idr
View File

@ -81,6 +81,17 @@ prettyKindedName Nothing nm = nm
prettyKindedName (Just kw) nm
= annotate (Syntax Keyword) (pretty0 kw) <++> nm
export
prettyType : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
(IdrisSyntax -> ann) -> ClosedTerm -> Core (Doc ann)
prettyType syn ty = do
defs <- get Ctxt
ty <- normaliseHoles defs [] ty
ty <- toFullNames ty
ty <- resugar [] ty
pure (prettyBy syn ty)
||| Look up implementations
getImplDocs : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -269,8 +280,8 @@ getDocsForName fc n config
-- should never happen, since we know that the DCon exists:
| Nothing => pure Empty
syn <- get Syn
ty <- resugar [] =<< normaliseHoles defs [] (type def)
let conWithTypeDoc = annotate (Decl con) (hsep [dCon con (prettyName con), colon, prettyBy Syntax ty])
ty <- prettyType Syntax (type def)
let conWithTypeDoc = annotate (Decl con) (hsep [dCon con (prettyName con), colon, ty])
case lookupName con (defDocstrings syn) of
[(n, "")] => pure conWithTypeDoc
[(n, str)] => pure $ vcat
@ -287,8 +298,8 @@ getDocsForName fc n config
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => pure []
ty <- resugar [] =<< normaliseHoles defs [] (type def)
pure [annotate (Decl n) $ prettyBy Syntax ty]
ty <- prettyType Syntax (type def)
pure [annotate (Decl n) ty]
getMethDoc : Method -> Core (List (Doc IdrisDocAnn))
getMethDoc meth
@ -361,11 +372,10 @@ getDocsForName fc n config
Just def <- lookupCtxtExact nm (gamma defs)
-- should never happen, since we know that the DCon exists:
| Nothing => pure Empty
ty <- resugar [] =<< normaliseHoles defs [] (type def)
ty <- prettyType Syntax (type def)
let projDecl = annotate (Decl nm) $
reAnnotate Syntax (prettyRig def.multiplicity) <+> hsep
[ fun nm (prettyName nm)
, colon, prettyBy Syntax ty ]
[ fun nm (prettyName nm), colon, ty ]
case lookupName nm (defDocstrings syn) of
[(_, "")] => pure projDecl
[(_, str)] =>
@ -587,10 +597,10 @@ summarise n -- n is fully qualified
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| _ => pure ""
ty <- normaliseHoles defs [] (type def)
ty <- prettyType Syntax (type def)
pure $ reAnnotate Syntax (prettyRig def.multiplicity)
<+> hsep [ showCategory Syntax def (prettyName n)
, colon, hang 0 (prettyBy Syntax !(resugar [] ty))
, colon, hang 0 ty
]
-- Display all the exported names in the given namespace

20
tests/idris2/api001/LazyCodegen.idr
View File

@ -5,14 +5,22 @@ module Main
import Core.Context
import Compiler.Common
import Idris.Driver
import Idris.Syntax
compile : Ref Ctxt Defs -> (tmpDir : String) -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmp dir term file = do coreLift $ putStrLn "I'd rather not."
pure $ Nothing
compile :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(tmpDir : String) -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs syn tmp dir term file
= do coreLift $ putStrLn "I'd rather not."
pure Nothing
execute : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
execute defs dir term = do coreLift $ putStrLn "Maybe in an hour."
execute :
Ref Ctxt Defs ->
Ref Syn SyntaxInfo ->
(execDir : String) -> ClosedTerm -> Core ()
execute defs syn dir term = do coreLift $ putStrLn "Maybe in an hour."
lazyCodegen : Codegen
lazyCodegen = MkCG compile execute Nothing Nothing

2
tests/node/nomangle001/expected
View File

@ -1,4 +1,6 @@
/* Main.foo : Int -> Int */
function foo($0) {
/* Main.baz : Int -> Int */
function $_baz($0) {
function another_name($0) {
function foo($0){return $0;}