From 14d480b97183dfe6f58c8330aa361dab0c76c1d7 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 17 May 2020 15:56:45 +0100 Subject: [PATCH] Everything but the IDE protocol --- src/Compiler/ANF.idr | 266 ++++++++ src/Compiler/Common.idr | 397 ++++++++++++ src/Compiler/LambdaLift.idr | 247 +++++++ src/Compiler/Scheme/Chez.idr | 397 ++++++++++++ src/Compiler/Scheme/Common.idr | 430 ++++++++++++ src/Compiler/Scheme/Gambit.idr | 319 +++++++++ src/Compiler/Scheme/Racket.idr | 343 ++++++++++ src/Compiler/VMCode.idr | 198 ++++++ src/Data/StringTrie.idr | 66 ++ src/Data/These.idr | 48 ++ src/Idris/CommandLine.idr | 259 ++++++++ src/Idris/IDEMode/CaseSplit.idr | 190 ++++++ src/Idris/IDEMode/MakeClause.idr | 52 ++ src/Idris/IDEMode/Parser.idr | 79 +++ src/Idris/IDEMode/REPL.idr | 325 ++++++++++ src/Idris/IDEMode/SyntaxHighlight.idr | 126 ++++ src/Idris/IDEMode/TokenLine.idr | 37 ++ src/Idris/Main.idr | 233 +++++++ src/Idris/Package.idr | 512 +++++++++++++++ src/Idris/REPL.idr | 896 ++++++++++++++++++++++++++ src/Idris/SetOptions.idr | 139 ++++ 21 files changed, 5559 insertions(+) create mode 100644 src/Compiler/ANF.idr create mode 100644 src/Compiler/Common.idr create mode 100644 src/Compiler/LambdaLift.idr create mode 100644 src/Compiler/Scheme/Chez.idr create mode 100644 src/Compiler/Scheme/Common.idr create mode 100644 src/Compiler/Scheme/Gambit.idr create mode 100644 src/Compiler/Scheme/Racket.idr create mode 100644 src/Compiler/VMCode.idr create mode 100644 src/Data/StringTrie.idr create mode 100644 src/Data/These.idr create mode 100644 src/Idris/CommandLine.idr create mode 100644 src/Idris/IDEMode/CaseSplit.idr create mode 100644 src/Idris/IDEMode/MakeClause.idr create mode 100644 src/Idris/IDEMode/Parser.idr create mode 100644 src/Idris/IDEMode/REPL.idr create mode 100644 src/Idris/IDEMode/SyntaxHighlight.idr create mode 100644 src/Idris/IDEMode/TokenLine.idr create mode 100644 src/Idris/Main.idr create mode 100644 src/Idris/Package.idr create mode 100644 src/Idris/REPL.idr create mode 100644 src/Idris/SetOptions.idr diff --git a/src/Compiler/ANF.idr b/src/Compiler/ANF.idr new file mode 100644 index 000000000..ceb8749c1 --- /dev/null +++ b/src/Compiler/ANF.idr @@ -0,0 +1,266 @@ +module Compiler.ANF + +import Compiler.LambdaLift + +import Core.CompileExpr +import Core.Context +import Core.Core +import Core.TT + +import Data.List +import Data.Vect + +%default covering + +-- Convert the lambda lifted form to ANF, with variable names made explicit. +-- i.e. turn intermediate expressions into let bindings. Every argument is +-- a variable as a result. + +mutual + public export + data AVar : Type where + ALocal : Int -> AVar + ANull : AVar + + public export + data ANF : Type where + AV : FC -> AVar -> ANF + AAppName : FC -> Name -> List AVar -> ANF + AUnderApp : FC -> Name -> (missing : Nat) -> (args : List AVar) -> ANF + AApp : FC -> (closure : AVar) -> (arg : AVar) -> ANF + ALet : FC -> (var : Int) -> ANF -> ANF -> ANF + ACon : FC -> Name -> (tag : Maybe Int) -> List AVar -> ANF + AOp : FC -> PrimFn arity -> Vect arity AVar -> ANF + AExtPrim : FC -> Name -> List AVar -> ANF + AConCase : FC -> AVar -> List AConAlt -> Maybe ANF -> ANF + AConstCase : FC -> AVar -> List AConstAlt -> Maybe ANF -> ANF + APrimVal : FC -> Constant -> ANF + AErased : FC -> ANF + ACrash : FC -> String -> ANF + + public export + data AConAlt : Type where + MkAConAlt : Name -> (tag : Maybe Int) -> (args : List Int) -> + ANF -> AConAlt + + public export + data AConstAlt : Type where + MkAConstAlt : Constant -> ANF -> AConstAlt + +public export +data ANFDef : Type where + MkAFun : (args : List Int) -> ANF -> ANFDef + MkACon : (tag : Maybe Int) -> (arity : Nat) -> ANFDef + MkAForeign : (ccs : List String) -> (fargs : List CFType) -> + CFType -> ANFDef + MkAError : ANF -> ANFDef + +mutual + export + Show AVar where + show (ALocal i) = "v" ++ show i + show ANull = "[__]" + + export + Show ANF where + show (AV _ v) = show v + show (AAppName fc n args) + = show n ++ "(" ++ showSep ", " (map show args) ++ ")" + show (AUnderApp fc n m args) + = "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++ + showSep ", " (map show args) ++ ")" + show (AApp fc c arg) + = show c ++ " @ (" ++ show arg ++ ")" + show (ALet fc x val sc) + = "%let v" ++ show x ++ " = " ++ show val ++ " in " ++ show sc + show (ACon fc n t args) + = "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")" + show (AOp fc op args) + = "%op " ++ show op ++ "(" ++ showSep ", " (toList (map show args)) ++ ")" + show (AExtPrim fc p args) + = "%extprim " ++ show p ++ "(" ++ showSep ", " (map show args) ++ ")" + show (AConCase fc sc alts def) + = "%case " ++ show sc ++ " of { " + ++ showSep "| " (map show alts) ++ " " ++ show def + show (AConstCase fc sc alts def) + = "%case " ++ show sc ++ " of { " + ++ showSep "| " (map show alts) ++ " " ++ show def + show (APrimVal _ x) = show x + show (AErased _) = "___" + show (ACrash _ x) = "%CRASH(" ++ show x ++ ")" + + export + Show AConAlt where + show (MkAConAlt n t args sc) + = "%conalt " ++ show n ++ + "(" ++ showSep ", " (map showArg args) ++ ") => " ++ show sc + where + showArg : Int -> String + showArg i = "v" ++ show i + + export + Show AConstAlt where + show (MkAConstAlt c sc) + = "%constalt(" ++ show c ++ ") => " ++ show sc + +export +Show ANFDef where + show (MkAFun args exp) = show args ++ ": " ++ show exp + show (MkACon tag arity) + = "Constructor tag " ++ show tag ++ " arity " ++ show arity + show (MkAForeign ccs args ret) + = "Foreign call " ++ show ccs ++ " " ++ + show args ++ " -> " ++ show ret + show (MkAError exp) = "Error: " ++ show exp + +data AVars : List Name -> Type where + Nil : AVars [] + (::) : Int -> AVars xs -> AVars (x :: xs) + +data Next : Type where + +nextVar : {auto v : Ref Next Int} -> + Core Int +nextVar + = do i <- get Next + put Next (i + 1) + pure i + +lookup : {idx : _} -> (0 p : IsVar x idx vs) -> AVars vs -> Int +lookup First (x :: xs) = x +lookup (Later p) (x :: xs) = lookup p xs + +bindArgs : {auto v : Ref Next Int} -> + List ANF -> Core (List (AVar, Maybe ANF)) +bindArgs [] = pure [] +bindArgs (AV fc var :: xs) + = do xs' <- bindArgs xs + pure $ (var, Nothing) :: xs' +bindArgs (AErased fc :: xs) + = do xs' <- bindArgs xs + pure $ (ANull, Nothing) :: xs' +bindArgs (x :: xs) + = do i <- nextVar + xs' <- bindArgs xs + pure $ (ALocal i, Just x) :: xs' + +letBind : {auto v : Ref Next Int} -> + FC -> List ANF -> (List AVar -> ANF) -> Core ANF +letBind fc args f + = do bargs <- bindArgs args + pure $ doBind [] bargs + where + doBind : List AVar -> List (AVar, Maybe ANF) -> ANF + doBind vs [] = f (reverse vs) + doBind vs ((ALocal i, Just t) :: xs) + = ALet fc i t (doBind (ALocal i :: vs) xs) + doBind vs ((var, _) :: xs) = doBind (var :: vs) xs + +toVect : (n : Nat) -> List a -> Maybe (Vect n a) +toVect Z [] = Just [] +toVect (S k) (x :: xs) + = do xs' <- toVect k xs + pure (x :: xs') +toVect _ _ = Nothing + +mlet : {auto v : Ref Next Int} -> + FC -> ANF -> (AVar -> ANF) -> Core ANF +mlet fc (AV _ var) sc = pure $ sc var +mlet fc val sc + = do i <- nextVar + pure $ ALet fc i val (sc (ALocal i)) + +mutual + anfArgs : {vars : _} -> + {auto v : Ref Next Int} -> + FC -> AVars vars -> + List (Lifted vars) -> (List AVar -> ANF) -> Core ANF + anfArgs fc vs args f + = do args' <- traverse (anf vs) args + letBind fc args' f + + anf : {vars : _} -> + {auto v : Ref Next Int} -> + AVars vars -> Lifted vars -> Core ANF + anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup p vs)) + anf vs (LAppName fc n args) + = anfArgs fc vs args (AAppName fc n) + anf vs (LUnderApp fc n m args) + = anfArgs fc vs args (AUnderApp fc n m) + anf vs (LApp fc f a) + = anfArgs fc vs [f, a] + (\args => case args of + [fvar, avar] => AApp fc fvar avar + _ => ACrash fc "Can't happen (AApp)") + anf vs (LLet fc x val sc) + = do i <- nextVar + let vs' = i :: vs + pure $ ALet fc i !(anf vs val) !(anf vs' sc) + anf vs (LCon fc n t args) + = anfArgs fc vs args (ACon fc n t) + anf vs (LOp {arity} fc op args) + = do args' <- traverse (anf vs) (toList args) + letBind fc args' + (\args => case toVect arity args of + Nothing => ACrash fc "Can't happen (AOp)" + Just argsv => AOp fc op argsv) + anf vs (LExtPrim fc p args) + = anfArgs fc vs args (AExtPrim fc p) + anf vs (LConCase fc scr alts def) + = do scr' <- anf vs scr + alts' <- traverse (anfConAlt vs) alts + def' <- traverseOpt (anf vs) def + mlet fc scr' (\x => AConCase fc x alts' def') + anf vs (LConstCase fc scr alts def) + = do scr' <- anf vs scr + alts' <- traverse (anfConstAlt vs) alts + def' <- traverseOpt (anf vs) def + mlet fc scr' (\x => AConstCase fc x alts' def') + anf vs (LPrimVal fc c) = pure $ APrimVal fc c + anf vs (LErased fc) = pure $ AErased fc + anf vs (LCrash fc err) = pure $ ACrash fc err + + anfConAlt : {vars : _} -> + {auto v : Ref Next Int} -> + AVars vars -> LiftedConAlt vars -> Core AConAlt + anfConAlt vs (MkLConAlt n t args sc) + = do (is, vs') <- bindArgs args vs + pure $ MkAConAlt n t is !(anf vs' sc) + where + bindArgs : (args : List Name) -> AVars vars' -> + Core (List Int, AVars (args ++ vars')) + bindArgs [] vs = pure ([], vs) + bindArgs (n :: ns) vs + = do i <- nextVar + (is, vs') <- bindArgs ns vs + pure (i :: is, i :: vs') + + anfConstAlt : {vars : _} -> + {auto v : Ref Next Int} -> + AVars vars -> LiftedConstAlt vars -> Core AConstAlt + anfConstAlt vs (MkLConstAlt c sc) + = pure $ MkAConstAlt c !(anf vs sc) + +export +toANF : LiftedDef -> Core ANFDef +toANF (MkLFun args scope sc) + = do v <- newRef Next (the Int 0) + (iargs, vsNil) <- bindArgs args [] + let vs : AVars args = rewrite sym (appendNilRightNeutral args) in + vsNil + (iargs', vs) <- bindArgs scope vs + pure $ MkAFun (iargs ++ reverse iargs') !(anf vs sc) + where + bindArgs : {auto v : Ref Next Int} -> + (args : List Name) -> AVars vars' -> + Core (List Int, AVars (args ++ vars')) + bindArgs [] vs = pure ([], vs) + bindArgs (n :: ns) vs + = do i <- nextVar + (is, vs') <- bindArgs ns vs + pure (i :: is, i :: vs') +toANF (MkLCon t a ns) = pure $ MkACon t a +toANF (MkLForeign ccs fargs t) = pure $ MkAForeign ccs fargs t +toANF (MkLError err) + = do v <- newRef Next (the Int 0) + pure $ MkAError !(anf [] err) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr new file mode 100644 index 000000000..5db9da6c1 --- /dev/null +++ b/src/Compiler/Common.idr @@ -0,0 +1,397 @@ +module Compiler.Common + +import Compiler.ANF +import Compiler.CompileExpr +import Compiler.Inline +import Compiler.LambdaLift +import Compiler.VMCode + +import Core.Context +import Core.Directory +import Core.Options +import Core.TT +import Core.TTC +import Utils.Binary + +import Data.IOArray +import Data.List +import Data.NameMap +import Data.Strings + +import System.Directory +import System.Info +import System.File + +||| Generic interface to some code generator +public export +record Codegen where + constructor MkCG + ||| Compile an Idris 2 expression, saving it to a file. + compileExpr : Ref Ctxt Defs -> (execDir : String) -> + ClosedTerm -> (outfile : String) -> Core (Maybe String) + ||| Execute an Idris 2 expression directly. + executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core () + +-- Say which phase of compilation is the last one to use - it saves time if +-- you only ask for what you need. +public export +data UsePhase = Cases | Lifted | ANF | VMCode + +Eq UsePhase where + (==) Cases Cases = True + (==) Lifted Lifted = True + (==) ANF ANF = True + (==) VMCode VMCode = True + (==) _ _ = False + +Ord UsePhase where + compare x y = compare (tag x) (tag y) + where + tag : UsePhase -> Int + tag Cases = 0 + tag Lifted = 0 + tag ANF = 0 + tag VMCode = 0 + +public export +record CompileData where + constructor MkCompileData + mainExpr : CExp [] -- main expression to execute. This also appears in + -- the definitions below as MN "__mainExpression" 0 + namedDefs : List (Name, FC, NamedDef) + lambdaLifted : List (Name, LiftedDef) + -- ^ lambda lifted definitions, if required. Only the top level names + -- will be in the context, and (for the moment...) I don't expect to + -- need to look anything up, so it's just an alist. + anf : List (Name, ANFDef) + -- ^ lambda lifted and converted to ANF (all arguments to functions + -- and constructors transformed to either variables or Null if erased) + vmcode : List (Name, VMDef) + -- ^ A much simplified virtual machine code, suitable for passing + -- to a more low level target such as C + +||| compile +||| Given a value of type Codegen, produce a standalone function +||| that executes the `compileExpr` method of the Codegen +export +compile : {auto c : Ref Ctxt Defs} -> + Codegen -> + ClosedTerm -> (outfile : String) -> Core (Maybe String) +compile {c} cg tm out + = do makeExecDirectory + d <- getDirs + logTime "Code generation overall" $ + compileExpr cg c (exec_dir d) 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} -> + Codegen -> ClosedTerm -> Core () +execute {c} cg tm + = do makeExecDirectory + d <- getDirs + executeExpr cg c (exec_dir d) tm + pure () + +-- 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) +getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe Binary) +getMinimalDef (Decoded def) = pure (def, Nothing) +getMinimalDef (Coded bin) + = do b <- newRef Bin bin + cdef <- fromBuf b + refsRList <- fromBuf b + let refsR = map fromList refsRList + fc <- fromBuf b + mul <- fromBuf b + name <- fromBuf b + let def + = MkGlobalDef fc name (Erased fc False) [] [] [] [] mul + [] Public (MkTotality Unchecked IsCovering) + [] Nothing refsR False False True + None cdef Nothing [] + pure (def, Just bin) + +-- ||| Recursively get all calls in a function definition +getAllDesc : {auto c : Ref Ctxt Defs} -> + List Name -> -- calls to check + IOArray (Int, Maybe Binary) -> + -- which nodes have been visited. If the entry is + -- present, it's visited. Keep the binary entry, if + -- we partially decoded it, so that we can put back + -- the full definition later. + -- (We only need to decode the case tree IR, and + -- it's expensive to decode the whole thing) + Defs -> Core () +getAllDesc [] arr defs = pure () +getAllDesc (n@(Resolved i) :: rest) arr defs + = do Nothing <- coreLift $ readArray arr i + | Just _ => getAllDesc rest arr defs + case !(lookupContextEntry n (gamma defs)) of + Nothing => getAllDesc rest arr defs + Just (_, entry) => + do (def, bin) <- getMinimalDef entry + addDef n def + let refs = refersToRuntime def + if multiplicity def /= erased + then do coreLift $ writeArray arr i (i, bin) + let refs = refersToRuntime def + refs' <- traverse toResolvedNames (keys refs) + getAllDesc (refs' ++ rest) arr defs + else getAllDesc rest arr defs +getAllDesc (n :: rest) arr defs + = getAllDesc rest arr defs + +getNamedDef : {auto c : Ref Ctxt Defs} -> + Name -> Core (Maybe (Name, FC, NamedDef)) +getNamedDef n + = do defs <- get Ctxt + case !(lookupCtxtExact n (gamma defs)) of + Nothing => pure Nothing + Just def => case namedcompexpr def of + Nothing => pure Nothing + Just d => pure (Just (n, location def, d)) + +replaceEntry : {auto c : Ref Ctxt Defs} -> + (Int, Maybe Binary) -> Core () +replaceEntry (i, Nothing) = pure () +replaceEntry (i, Just b) + = do addContextEntry (Resolved i) b + pure () + +natHackNames : List Name +natHackNames + = [UN "prim__add_Integer", + UN "prim__sub_Integer", + UN "prim__mul_Integer", + NS ["Prelude"] (UN "natToInteger"), + NS ["Prelude"] (UN "integerToNat")] + +-- Hmm, these dump functions are all very similar aren't they... +dumpCases : Defs -> String -> List Name -> + Core () +dumpCases defs fn cns + = do cstrs <- traverse dumpCase cns + Right () <- coreLift $ writeFile fn (fastAppend cstrs) + | Left err => throw (FileErr fn err) + pure () + where + fullShow : Name -> String + fullShow (DN _ n) = show n + fullShow n = show n + + dumpCase : Name -> Core String + dumpCase n + = case !(lookupCtxtExact n (gamma defs)) of + Nothing => pure "" + Just d => + case namedcompexpr d of + Nothing => pure "" + Just def => pure (fullShow n ++ " = " ++ show def ++ "\n") + +dumpLifted : String -> List (Name, LiftedDef) -> Core () +dumpLifted fn lns + = do let cstrs = map dumpDef lns + Right () <- coreLift $ writeFile fn (fastAppend cstrs) + | Left err => throw (FileErr fn err) + pure () + where + fullShow : Name -> String + fullShow (DN _ n) = show n + fullShow n = show n + + dumpDef : (Name, LiftedDef) -> String + dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n" + +dumpANF : String -> List (Name, ANFDef) -> Core () +dumpANF fn lns + = do let cstrs = map dumpDef lns + Right () <- coreLift $ writeFile fn (fastAppend cstrs) + | Left err => throw (FileErr fn err) + pure () + where + fullShow : Name -> String + fullShow (DN _ n) = show n + fullShow n = show n + + dumpDef : (Name, ANFDef) -> String + dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n" + +dumpVMCode : String -> List (Name, VMDef) -> Core () +dumpVMCode fn lns + = do let cstrs = map dumpDef lns + Right () <- coreLift $ writeFile fn (fastAppend cstrs) + | Left err => throw (FileErr fn err) + pure () + where + fullShow : Name -> String + fullShow (DN _ n) = show n + fullShow n = show n + + dumpDef : (Name, VMDef) -> String + dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n" + +-- 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 +export +getCompileData : {auto c : Ref Ctxt Defs} -> + UsePhase -> ClosedTerm -> Core CompileData +getCompileData phase tm_in + = do defs <- get Ctxt + sopts <- getSession + let ns = getRefs (Resolved (-1)) tm_in + tm <- toFullNames tm_in + natHackNames' <- traverse toResolvedNames natHackNames + -- make an array of Bools to hold which names we've found (quicker + -- to check than a NameMap!) + asize <- getNextEntry + arr <- coreLift $ newArray asize + logTime "Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs + + let entries = mapMaybe id !(coreLift (toList arr)) + let allNs = map (Resolved . fst) entries + cns <- traverse toFullNames allNs + + -- Do a round of merging/arity fixing for any names which were + -- unknown due to cyclic modules (i.e. declared in one, defined in + -- another) + rcns <- filterM nonErased cns + logTime "Merge lambda" $ traverse_ mergeLamDef rcns + logTime "Fix arity" $ traverse_ fixArityDef rcns + logTime "Forget names" $ traverse_ mkForgetDef rcns + + compiledtm <- fixArityExp !(compileExp tm) + let mainname = MN "__mainExpression" 0 + (liftedtm, ldefs) <- liftBody mainname compiledtm + + namedefs <- traverse getNamedDef rcns + lifted_in <- if phase >= Lifted + then logTime "Lambda lift" $ traverse lambdaLift rcns + else pure [] + + let lifted = (mainname, MkLFun [] [] liftedtm) :: + ldefs ++ 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 [] + + defs <- get Ctxt + maybe (pure ()) + (\f => do coreLift $ putStrLn $ "Dumping case trees to " ++ f + dumpCases defs f rcns) + (dumpcases sopts) + maybe (pure ()) + (\f => do coreLift $ putStrLn $ "Dumping lambda lifted defs to " ++ f + dumpLifted f lifted) + (dumplifted sopts) + maybe (pure ()) + (\f => do coreLift $ putStrLn $ "Dumping ANF defs to " ++ f + dumpANF f anf) + (dumpanf sopts) + maybe (pure ()) + (\f => do coreLift $ putStrLn $ "Dumping VM defs to " ++ f + dumpVMCode f vmcode) + (dumpvmcode sopts) + + -- We're done with our minimal context now, so put it back the way + -- it was. Back ends shouldn't look at the global context, because + -- it'll have to decode the definitions again. + traverse_ replaceEntry entries + 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) + +-- Some things missing from Prelude.File + +||| check to see if a given file exists +export +exists : String -> IO Bool +exists f + = do Right ok <- openFile f Read + | Left err => pure False + closeFile ok + pure True + +-- Parse a calling convention into a backend/target for the call, and +-- a comma separated list of any other location data. +-- e.g. "scheme:display" - call the scheme function 'display' +-- "C:puts,libc,stdio.h" - call the C function 'puts' which is in +-- the library libc and the header stdio.h +-- Returns Nothing if the string is empty (which a backend can interpret +-- however it likes) +export +parseCC : String -> Maybe (String, List String) +parseCC "" = Nothing +parseCC str + = case span (/= ':') str of + (target, "") => Just (trim target, []) + (target, opts) => Just (trim target, + map trim (getOpts + (assert_total (strTail opts)))) + where + getOpts : String -> List String + getOpts "" = [] + getOpts str + = case span (/= ',') str of + (opt, "") => [opt] + (opt, rest) => opt :: getOpts (assert_total (strTail rest)) + +export +dylib_suffix : String +dylib_suffix + = cond [(os `elem` ["windows", "mingw32", "cygwin32"], "dll"), + (os == "darwin", "dylib")] + "so" + +export +locate : {auto c : Ref Ctxt Defs} -> + String -> Core (String, String) +locate libspec + = do -- Attempt to turn libspec into an appropriate filename for the system + let fname + = case words libspec of + [] => "" + [fn] => if '.' `elem` unpack fn + then fn -- full filename given + else -- add system extension + fn ++ "." ++ dylib_suffix + (fn :: ver :: _) => + -- library and version given, build path name as + -- appropriate for the system + cond [(dylib_suffix == "dll", + fn ++ "-" ++ ver ++ ".dll"), + (dylib_suffix == "dylib", + fn ++ "." ++ ver ++ ".dylib")] + (fn ++ "." ++ dylib_suffix ++ "." ++ ver) + + fullname <- catch (findLibraryFile fname) + (\err => -- assume a system library so not + -- in our library path + pure fname) + pure (fname, fullname) + +export +copyLib : (String, String) -> Core () +copyLib (lib, fullname) + = if lib == fullname + then pure () + else do Right bin <- coreLift $ readFromFile fullname + | Left err => throw (FileErr fullname err) + Right _ <- coreLift $ writeToFile lib bin + | Left err => throw (FileErr lib err) + pure () diff --git a/src/Compiler/LambdaLift.idr b/src/Compiler/LambdaLift.idr new file mode 100644 index 000000000..9ebd826e6 --- /dev/null +++ b/src/Compiler/LambdaLift.idr @@ -0,0 +1,247 @@ +module Compiler.LambdaLift + +import Core.CompileExpr +import Core.Context +import Core.Core +import Core.TT + +import Data.List +import Data.Vect + +%default covering + +mutual + public export + data Lifted : List Name -> Type where + LLocal : {idx : Nat} -> FC -> (0 p : IsVar x idx vars) -> Lifted vars + -- A known function applied to exactly the right number of arguments, + -- so the runtime can Just Go + LAppName : FC -> Name -> List (Lifted vars) -> Lifted vars + -- A known function applied to too few arguments, so the runtime should + -- make a closure and wait for the remaining arguments + LUnderApp : FC -> Name -> (missing : Nat) -> + (args : List (Lifted vars)) -> Lifted vars + -- A closure applied to one more argument (so, for example a closure + -- which is waiting for another argument before it can run). + -- The runtime should add the argument to the closure and run the result + -- if it is now fully applied. + LApp : FC -> (closure : Lifted vars) -> (arg : Lifted vars) -> Lifted vars + LLet : FC -> (x : Name) -> Lifted vars -> + Lifted (x :: vars) -> Lifted vars + LCon : FC -> Name -> (tag : Maybe Int) -> List (Lifted vars) -> Lifted vars + LOp : {arity : _} -> + FC -> PrimFn arity -> Vect arity (Lifted vars) -> Lifted vars + LExtPrim : FC -> (p : Name) -> List (Lifted vars) -> Lifted vars + LConCase : FC -> Lifted vars -> + List (LiftedConAlt vars) -> + Maybe (Lifted vars) -> Lifted vars + LConstCase : FC -> Lifted vars -> + List (LiftedConstAlt vars) -> + Maybe (Lifted vars) -> Lifted vars + LPrimVal : FC -> Constant -> Lifted vars + LErased : FC -> Lifted vars + LCrash : FC -> String -> Lifted vars + + public export + data LiftedConAlt : List Name -> Type where + MkLConAlt : Name -> (tag : Maybe Int) -> (args : List Name) -> + Lifted (args ++ vars) -> LiftedConAlt vars + + public export + data LiftedConstAlt : List Name -> Type where + MkLConstAlt : Constant -> Lifted vars -> LiftedConstAlt vars + +public export +data LiftedDef : Type where + -- We take the outer scope and the function arguments separately so that + -- we don't have to reshuffle de Bruijn indices, which is expensive. + -- This should be compiled as a function which takes 'args' first, + -- then 'reverse scope'. + -- (Sorry for the awkward API - it's to do with how the indices are + -- arranged for the variables, and it oculd be expensive to reshuffle them! + -- See Compiler.ANF for an example of how they get resolved to names) + MkLFun : (args : List Name) -> -- function arguments + (scope : List Name) -> -- outer scope + Lifted (scope ++ args) -> LiftedDef + MkLCon : (tag : Maybe Int) -> (arity : Nat) -> (nt : Maybe Nat) -> LiftedDef + MkLForeign : (ccs : List String) -> + (fargs : List CFType) -> + CFType -> + LiftedDef + MkLError : Lifted [] -> LiftedDef + +mutual + export + {vs : _} -> Show (Lifted vs) where + show (LLocal {idx} _ p) = "!" ++ show (nameAt idx p) + show (LAppName fc n args) + = show n ++ "(" ++ showSep ", " (map show args) ++ ")" + show (LUnderApp fc n m args) + = "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++ + showSep ", " (map show args) ++ ")" + show (LApp fc c arg) + = show c ++ " @ (" ++ show arg ++ ")" + show (LLet fc x val sc) + = "%let " ++ show x ++ " = " ++ show val ++ " in " ++ show sc + show (LCon fc n t args) + = "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")" + show (LOp fc op args) + = "%op " ++ show op ++ "(" ++ showSep ", " (toList (map show args)) ++ ")" + show (LExtPrim fc p args) + = "%extprim " ++ show p ++ "(" ++ showSep ", " (map show args) ++ ")" + show (LConCase fc sc alts def) + = "%case " ++ show sc ++ " of { " + ++ showSep "| " (map show alts) ++ " " ++ show def + show (LConstCase fc sc alts def) + = "%case " ++ show sc ++ " of { " + ++ showSep "| " (map show alts) ++ " " ++ show def + show (LPrimVal _ x) = show x + show (LErased _) = "___" + show (LCrash _ x) = "%CRASH(" ++ show x ++ ")" + + export + {vs : _} -> Show (LiftedConAlt vs) where + show (MkLConAlt n t args sc) + = "%conalt " ++ show n ++ + "(" ++ showSep ", " (map show args) ++ ") => " ++ show sc + + export + {vs : _} -> Show (LiftedConstAlt vs) where + show (MkLConstAlt c sc) + = "%constalt(" ++ show c ++ ") => " ++ show sc + +export +Show LiftedDef where + show (MkLFun args scope exp) + = show args ++ show (reverse scope) ++ ": " ++ show exp + show (MkLCon tag arity pos) + = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++ + maybe "" (\n => " (newtype by " ++ show n ++ ")") pos + show (MkLForeign ccs args ret) + = "Foreign call " ++ show ccs ++ " " ++ + show args ++ " -> " ++ show ret + show (MkLError exp) = "Error: " ++ show exp + + +data Lifts : Type where + +record LDefs where + constructor MkLDefs + basename : Name -- top level name we're lifting from + defs : List (Name, LiftedDef) -- new definitions we made + nextName : Int -- name of next definition to lift + +genName : {auto l : Ref Lifts LDefs} -> + Core Name +genName + = do ldefs <- get Lifts + let i = nextName ldefs + put Lifts (record { nextName = i + 1 } ldefs) + pure $ mkName (basename ldefs) i + where + mkName : Name -> Int -> Name + mkName (NS ns b) i = NS ns (mkName b i) + mkName (UN n) i = MN n i + mkName (DN _ n) i = mkName n i + mkName n i = MN (show n) i + +unload : FC -> Lifted vars -> List (Lifted vars) -> Core (Lifted vars) +unload fc f [] = pure f +unload fc f (a :: as) = unload fc (LApp fc f a) as + +mutual + makeLam : {auto l : Ref Lifts LDefs} -> + {vars : _} -> + FC -> (bound : List Name) -> + CExp (bound ++ vars) -> Core (Lifted vars) + makeLam fc bound (CLam _ x sc') = makeLam fc (x :: bound) sc' + makeLam {vars} fc bound sc + = do scl <- liftExp sc + n <- genName + ldefs <- get Lifts + put Lifts (record { defs $= ((n, MkLFun vars bound scl) ::) } ldefs) + -- TODO: an optimisation here would be to spot which variables + -- aren't used in the new definition, and not abstract over them + -- in the new definition. Given that we have to do some messing + -- about with indices anyway, it's probably not costly to do. + pure $ LUnderApp fc n (length bound) (allVars vars) + where + allPrfs : (vs : List Name) -> List (Var vs) + allPrfs [] = [] + allPrfs (v :: vs) = MkVar First :: map weaken (allPrfs vs) + + -- apply to all the variables. 'First' will be first in the last, which + -- is good, because the most recently bound name is the first argument to + -- the resulting function + allVars : (vs : List Name) -> List (Lifted vs) + allVars vs = map (\ (MkVar p) => LLocal fc p) (allPrfs vs) + + liftExp : {vars : _} -> + {auto l : Ref Lifts LDefs} -> + CExp vars -> Core (Lifted vars) + liftExp (CLocal fc prf) = pure $ LLocal fc prf + liftExp (CRef fc n) = pure $ LAppName fc n [] -- probably shouldn't happen! + liftExp (CLam fc x sc) = makeLam fc [x] sc + liftExp (CLet fc x _ val sc) = pure $ LLet fc x !(liftExp val) !(liftExp sc) + liftExp (CApp fc (CRef _ n) args) -- names are applied exactly in compileExp + = pure $ LAppName fc n !(traverse liftExp args) + liftExp (CApp fc f args) + = unload fc !(liftExp f) !(traverse liftExp args) + liftExp (CCon fc n t args) = pure $ LCon fc n t !(traverse liftExp args) + liftExp (COp fc op args) + = pure $ LOp fc op !(traverseArgs args) + where + traverseArgs : Vect n (CExp vars) -> Core (Vect n (Lifted vars)) + traverseArgs [] = pure [] + traverseArgs (a :: as) = pure $ !(liftExp a) :: !(traverseArgs as) + liftExp (CExtPrim fc p args) = pure $ LExtPrim fc p !(traverse liftExp args) + liftExp (CForce fc tm) = liftExp (CApp fc tm [CErased fc]) + liftExp (CDelay fc tm) = liftExp (CLam fc (MN "act" 0) (weaken tm)) + liftExp (CConCase fc sc alts def) + = pure $ LConCase fc !(liftExp sc) !(traverse liftConAlt alts) + !(traverseOpt liftExp def) + where + liftConAlt : CConAlt vars -> Core (LiftedConAlt vars) + liftConAlt (MkConAlt n t args sc) = pure $ MkLConAlt n t args !(liftExp sc) + liftExp (CConstCase fc sc alts def) + = pure $ LConstCase fc !(liftExp sc) !(traverse liftConstAlt alts) + !(traverseOpt liftExp def) + where + liftConstAlt : CConstAlt vars -> Core (LiftedConstAlt vars) + liftConstAlt (MkConstAlt c sc) = pure $ MkLConstAlt c !(liftExp sc) + liftExp (CPrimVal fc c) = pure $ LPrimVal fc c + liftExp (CErased fc) = pure $ LErased fc + liftExp (CCrash fc str) = pure $ LCrash fc str + +export +liftBody : {vars : _} -> + Name -> CExp vars -> Core (Lifted vars, List (Name, LiftedDef)) +liftBody n tm + = do l <- newRef Lifts (MkLDefs n [] 0) + tml <- liftExp {l} tm + ldata <- get Lifts + pure (tml, defs ldata) + +lambdaLiftDef : Name -> CDef -> Core (List (Name, LiftedDef)) +lambdaLiftDef n (MkFun args exp) + = do (expl, defs) <- liftBody n exp + pure ((n, MkLFun args [] expl) :: defs) +lambdaLiftDef n (MkCon t a nt) = pure [(n, MkLCon t a nt)] +lambdaLiftDef n (MkForeign ccs fargs ty) = pure [(n, MkLForeign ccs fargs ty)] +lambdaLiftDef n (MkError exp) + = do (expl, defs) <- liftBody n exp + pure ((n, MkLError expl) :: defs) + +-- Return the lambda lifted definitions required for the given name. +-- If the name hasn't been compiled yet (via CompileExpr.compileDef) then +-- this will return an empty list +-- An empty list an error, because on success you will always get at least +-- one definition, the lifted definition for the given name. +export +lambdaLift : {auto c : Ref Ctxt Defs} -> + Name -> Core (List (Name, LiftedDef)) +lambdaLift n + = do defs <- get Ctxt + Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure [] + let Just cexpr = compexpr def | Nothing => pure [] + lambdaLiftDef n cexpr diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr new file mode 100644 index 000000000..e82779e2a --- /dev/null +++ b/src/Compiler/Scheme/Chez.idr @@ -0,0 +1,397 @@ +module Compiler.Scheme.Chez + +import Compiler.Common +import Compiler.CompileExpr +import Compiler.Inline +import Compiler.Scheme.Common + +import Core.Context +import Core.Directory +import Core.Name +import Core.Options +import Core.TT +import Utils.Hex + +import Data.List +import Data.Maybe +import Data.NameMap +import Data.Strings +import Data.Vect +import System +import System.Info + +%default covering + + +pathLookup : IO String +pathLookup + = do path <- getEnv "PATH" + let pathList = split (== ':') $ fromMaybe "/usr/bin:/usr/local/bin" path + let candidates = [p ++ "/" ++ x | p <- pathList, + x <- ["chez", "chezscheme9.5", "scheme"]] + e <- firstExists candidates + pure $ fromMaybe "/usr/bin/env scheme" e + +findChez : IO String +findChez + = do Just chez <- getEnv "CHEZ" | Nothing => pathLookup + pure chez + +-- Given the chez compiler directives, return a list of pairs of: +-- - the library file name +-- - the full absolute path of the library file name, if it's in one +-- of the library paths managed by Idris +-- If it can't be found, we'll assume it's a system library and that chez +-- will thus be able to find it. +findLibs : {auto c : Ref Ctxt Defs} -> + List String -> Core (List (String, String)) +findLibs ds + = do let libs = mapMaybe (isLib . trim) ds + traverse locate (nub libs) + where + isLib : String -> Maybe String + isLib d + = if isPrefixOf "lib" d + then Just (trim (substr 3 (length d) d)) + else Nothing + +escapeQuotes : String -> String +escapeQuotes s = pack $ foldr escape [] $ unpack s + where + escape : Char -> List Char -> List Char + escape '"' cs = '\\' :: '\"' :: cs + escape c cs = c :: cs + +schHeader : String -> List String -> String +schHeader chez libs + = (if os /= "windows" then "#!" ++ chez ++ " --script\n\n" else "") ++ + "(import (chezscheme))\n" ++ + "(case (machine-type)\n" ++ + " [(i3le ti3le a6le ta6le) (load-shared-object \"libc.so.6\")]\n" ++ + " [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++ + " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++ + " [else (load-shared-object \"libc.so\")])\n\n" ++ + showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeQuotes x ++ "\")") libs) ++ "\n\n" ++ + "(let ()\n" + +schFooter : String +schFooter = ")" + +showChezChar : Char -> String -> String +showChezChar '\\' = ("\\\\" ++) +showChezChar c + = if c < chr 32 || c > chr 126 + then (("\\x" ++ asHex (cast c) ++ ";") ++) + else strCons c + +showChezString : List Char -> String -> String +showChezString [] = id +showChezString ('"'::cs) = ("\\\"" ++) . showChezString cs +showChezString (c ::cs) = (showChezChar c) . showChezString cs + +chezString : String -> String +chezString cs = strCons '"' (showChezString (unpack cs) "\"") + +mutual + tySpec : NamedCExp -> Core String + -- Primitive types have been converted to names for the purpose of matching + -- on types + tySpec (NmCon fc (UN "Int") _ []) = pure "int" + tySpec (NmCon fc (UN "String") _ []) = pure "string" + tySpec (NmCon fc (UN "Double") _ []) = pure "double" + tySpec (NmCon fc (UN "Char") _ []) = pure "char" + tySpec (NmCon fc (NS _ n) _ [_]) + = cond [(n == UN "Ptr", pure "void*")] + (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function"))) + tySpec (NmCon fc (NS _ n) _ []) + = cond [(n == UN "Unit", pure "void"), + (n == UN "AnyPtr", pure "void*")] + (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function"))) + tySpec ty = throw (GenericMsg (getFC ty) ("Can't pass argument of type " ++ show ty ++ " to foreign function")) + + handleRet : String -> String -> String + handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN "") (Just 0) []) + handleRet _ op = mkWorld op + + getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp)) + getFArgs (NmCon fc _ (Just 0) _) = pure [] + getFArgs (NmCon fc _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest) + getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg)) + + chezExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String + chezExtPrim i CCall [ret, NmPrimVal fc (Str fn), fargs, world] + = do args <- getFArgs fargs + argTypes <- traverse tySpec (map fst args) + retType <- tySpec ret + argsc <- traverse (schExp chezExtPrim chezString 0) (map snd args) + pure $ handleRet retType ("((foreign-procedure #f " ++ show fn ++ " (" + ++ showSep " " argTypes ++ ") " ++ retType ++ ") " + ++ showSep " " argsc ++ ")") + chezExtPrim i CCall [ret, fn, args, world] + = pure "(error \"bad ffi call\")" + -- throw (InternalError ("C FFI calls must be to statically known functions (" ++ show fn ++ ")")) + chezExtPrim i GetField [NmPrimVal _ (Str s), _, _, struct, + NmPrimVal _ (Str fld), _] + = do structsc <- schExp chezExtPrim chezString 0 struct + pure $ "(ftype-ref " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ ")" + chezExtPrim i GetField [_,_,_,_,_,_] + = pure "(error \"bad getField\")" + chezExtPrim i SetField [NmPrimVal _ (Str s), _, _, struct, + NmPrimVal _ (Str fld), _, val, world] + = do structsc <- schExp chezExtPrim chezString 0 struct + valsc <- schExp chezExtPrim chezString 0 val + pure $ mkWorld $ + "(ftype-set! " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ + " " ++ valsc ++ ")" + chezExtPrim i SetField [_,_,_,_,_,_,_,_] + = pure "(error \"bad setField\")" + chezExtPrim i SysCodegen [] + = pure $ "\"chez\"" + chezExtPrim i prim args + = schExtCommon chezExtPrim chezString i prim args + +-- Reference label for keeping track of loaded external libraries +data Loaded : Type where + +-- Label for noting which struct types are declared +data Structs : Type where + +cftySpec : FC -> CFType -> Core String +cftySpec fc CFUnit = pure "void" +cftySpec fc CFInt = pure "int" +cftySpec fc CFString = pure "string" +cftySpec fc CFDouble = pure "double" +cftySpec fc CFChar = pure "char" +cftySpec fc CFPtr = pure "void*" +cftySpec fc (CFFun s t) = pure "void*" +cftySpec fc (CFIORes t) = cftySpec fc t +cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")" +cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++ + " to foreign function")) + +cCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + String -> FC -> (cfn : String) -> (clib : String) -> + List (Name, CFType) -> CFType -> Core (String, String) +cCall appdir fc cfn clib args ret + = do loaded <- get Loaded + lib <- if clib `elem` loaded + then pure "" + else do (fname, fullname) <- locate clib + copyLib (appdir ++ dirSep ++ fname, fullname) + put Loaded (clib :: loaded) + pure $ "(load-shared-object \"" + ++ escapeQuotes fname + ++ "\")\n" + argTypes <- traverse (\a => cftySpec fc (snd a)) args + retType <- cftySpec fc ret + let call = "((foreign-procedure #f " ++ show cfn ++ " (" + ++ showSep " " argTypes ++ ") " ++ retType ++ ") " + ++ showSep " " !(traverse buildArg args) ++ ")" + + pure (lib, case ret of + CFIORes _ => handleRet retType call + _ => call) + where + mkNs : Int -> List CFType -> List (Maybe String) + mkNs i [] = [] + mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs + mkNs i (x :: xs) = Just ("cb" ++ show i) :: mkNs (i + 1) xs + + applyLams : String -> List (Maybe String) -> String + applyLams n [] = n + applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as + applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as + + getVal : String -> String + getVal str = "(vector-ref " ++ str ++ "1)" + + mkFun : List CFType -> CFType -> String -> String + mkFun args ret n + = let argns = mkNs 0 args in + "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++ + (applyLams n argns ++ ")") + + notWorld : CFType -> Bool + notWorld CFWorld = False + notWorld _ = True + + callback : String -> List CFType -> CFType -> Core String + callback n args (CFFun s t) = callback n (s :: args) t + callback n args_rev retty + = do let args = reverse args_rev + argTypes <- traverse (cftySpec fc) (filter notWorld args) + retType <- cftySpec fc retty + pure $ + "(let ([c-code (foreign-callable #f " ++ + mkFun args retty n ++ + " (" ++ showSep " " argTypes ++ ") " ++ retType ++ ")])" ++ + " (lock-object c-code) (foreign-callable-entry-point c-code))" + + buildArg : (Name, CFType) -> Core String + buildArg (n, CFFun s t) = callback (schName n) [s] t + buildArg (n, _) = pure $ schName n + +schemeCall : FC -> (sfn : String) -> + List Name -> CFType -> Core String +schemeCall fc sfn argns ret + = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in + case ret of + CFIORes _ => pure $ mkWorld call + _ => pure call + +-- Use a calling convention to compile a foreign def. +-- Returns any preamble needed for loading libraries, and the body of the +-- function call. +useCC : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String) +useCC appdir fc [] args ret + = throw (GenericMsg fc "No recognised foreign calling convention") +useCC appdir fc (cc :: ccs) args ret + = case parseCC cc of + Nothing => useCC appdir fc ccs args ret + Just ("scheme", [sfn]) => + do body <- schemeCall fc sfn (map fst args) ret + pure ("", body) + Just ("C", [cfn, clib]) => cCall appdir fc cfn clib args ret + Just ("C", [cfn, clib, chdr]) => cCall appdir fc cfn clib args ret + _ => useCC appdir fc ccs args ret + +-- For every foreign arg type, return a name, and whether to pass it to the +-- foreign call (we don't pass '%World') +mkArgs : Int -> List CFType -> List (Name, Bool) +mkArgs i [] = [] +mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs +mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs + +mkStruct : {auto s : Ref Structs (List String)} -> + CFType -> Core String +mkStruct (CFStruct n flds) + = do defs <- traverse mkStruct (map snd flds) + strs <- get Structs + if n `elem` strs + then pure (concat defs) + else do put Structs (n :: strs) + pure $ concat defs ++ "(define-ftype " ++ n ++ " (struct\n\t" + ++ showSep "\n\t" !(traverse showFld flds) ++ "))\n" + where + showFld : (String, CFType) -> Core String + showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]" +mkStruct (CFIORes t) = mkStruct t +mkStruct (CFFun a b) = do mkStruct a; mkStruct b +mkStruct _ = pure "" + +schFgnDef : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + {auto s : Ref Structs (List String)} -> + String -> FC -> Name -> NamedDef -> Core (String, String) +schFgnDef appdir fc n (MkNmForeign cs args ret) + = 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 + defs <- get Ctxt + pure (load, + concat argStrs ++ retStr ++ + "(define " ++ schName !(full (gamma defs) n) ++ + " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++ + body ++ "))\n") +schFgnDef _ _ _ _ = pure ("", "") + +getFgnCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + {auto s : Ref Structs (List String)} -> + String -> (Name, FC, NamedDef) -> Core (String, String) +getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d + +startChez : String -> String +startChez target = unlines + [ "#!/bin/sh" + , "" + , "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:$(dirname \"" ++ target ++ "\")\"" + , "\"" ++ target ++ "\" \"$@\"" + ] + +||| Compile a TT expression to Chez Scheme +compileToSS : Ref Ctxt Defs -> + String -> ClosedTerm -> (outfile : String) -> Core () +compileToSS c appdir tm outfile + = do ds <- getDirectives Chez + libs <- findLibs ds + traverse_ copyLib libs + cdata <- getCompileData Cases tm + let ndefs = namedDefs cdata + let ctm = forget (mainExpr cdata) + + defs <- get Ctxt + l <- newRef {t = List String} Loaded ["libc", "libc 6"] + s <- newRef {t = List String} Structs [] + fgndefs <- traverse (getFgnCall appdir) ndefs + compdefs <- traverse (getScheme chezExtPrim chezString) ndefs + let code = fastAppend (map snd fgndefs ++ compdefs) + main <- schExp chezExtPrim chezString 0 ctm + chez <- coreLift findChez + support <- readDataFile "chez/support.ss" + let scm = schHeader chez (map snd libs) ++ + support ++ code ++ + concat (map fst fgndefs) ++ + main ++ schFooter + Right () <- coreLift $ writeFile outfile scm + | Left err => throw (FileErr outfile err) + coreLift $ chmodRaw outfile 0o755 + pure () + +||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off. +compileToSO : {auto c : Ref Ctxt Defs} -> + (appDirRel : String) -> (outSsAbs : String) -> Core () +compileToSO appDirRel outSsAbs + = do let tmpFileAbs = appDirRel ++ dirSep ++ "compileChez" + chez <- coreLift $ findChez + let build= "#!" ++ chez ++ " --script\n" ++ + "(parameterize ([optimize-level 3]) (compile-program \"" ++ + outSsAbs ++ "\"))" + Right () <- coreLift $ writeFile tmpFileAbs build + | Left err => throw (FileErr tmpFileAbs err) + coreLift $ chmodRaw tmpFileAbs 0o755 + coreLift $ system tmpFileAbs + pure () + +makeSh : String -> String -> Core () +makeSh outShRel outAbs + = do Right () <- coreLift $ writeFile outShRel (startChez outAbs) + | Left err => throw (FileErr outShRel err) + pure () + +||| Chez Scheme implementation of the `compileExpr` interface. +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) + 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 outShRel = execDir ++ dirSep ++ outfile + makeSh outShRel (if makeitso then outSoAbs else outSsAbs) + coreLift $ chmodRaw outShRel 0o755 + pure (Just outShRel) + +||| 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 -> (execDir : String) -> ClosedTerm -> Core () +executeExpr c execDir tm + = do Just sh <- compileExpr False c execDir tm "_tmpchez" + | Nothing => throw (InternalError "compileExpr returned Nothing") + coreLift $ system sh + pure () + +||| Codegen wrapper for Chez scheme implementation. +export +codegenChez : Codegen +codegenChez = MkCG (compileExpr True) executeExpr diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr new file mode 100644 index 000000000..44261b996 --- /dev/null +++ b/src/Compiler/Scheme/Common.idr @@ -0,0 +1,430 @@ +module Compiler.Scheme.Common + +import Compiler.Common +import Compiler.CompileExpr +import Compiler.Inline + +import Core.Context +import Core.Name +import Core.TT + +import Data.Bool.Extra +import Data.List +import Data.Vect + +import System.Info + +%default covering + +export +firstExists : List String -> IO (Maybe String) +firstExists [] = pure Nothing +firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs + +schString : String -> String +schString s = concatMap okchar (unpack s) + where + okchar : Char -> String + okchar c = if isAlphaNum c || c =='_' + then cast c + else "C-" ++ show (cast {to=Int} c) + +export +schName : Name -> String +schName (NS ns n) = showSep "-" ns ++ "-" ++ schName n +schName (UN n) = schString n +schName (MN n i) = schString n ++ "-" ++ show i +schName (PV n d) = "pat--" ++ schName n +schName (DN _ n) = schName n +schName (RF n) = "rf--" ++ schString n +schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n +schName (CaseBlock x y) = "case--" ++ show x ++ "-" ++ show y +schName (WithBlock x y) = "with--" ++ show x ++ "-" ++ show y +schName (Resolved i) = "fn--" ++ show i + +export +schConstructor : (String -> String) -> Name -> Maybe Int -> List String -> String +schConstructor _ _ (Just t) args + = "(vector " ++ show t ++ " " ++ showSep " " args ++ ")" +schConstructor schString n Nothing args + = "(vector " ++ schString (show n) ++ " " ++ showSep " " args ++ ")" + +||| Generate scheme for a plain function. +op : String -> List String -> String +op o args = "(" ++ o ++ " " ++ showSep " " args ++ ")" + +||| Generate scheme for a boolean operation. +boolop : String -> List String -> String +boolop o args = "(or (and " ++ op o args ++ " 1) 0)" + +||| Generate scheme for a primitive function. +schOp : PrimFn arity -> Vect arity String -> String +schOp (Add IntType) [x, y] = op "b+" [x, y, "63"] +schOp (Sub IntType) [x, y] = op "b-" [x, y, "63"] +schOp (Mul IntType) [x, y] = op "b*" [x, y, "63"] +schOp (Div IntType) [x, y] = op "b/" [x, y, "63"] +schOp (Add ty) [x, y] = op "+" [x, y] +schOp (Sub ty) [x, y] = op "-" [x, y] +schOp (Mul ty) [x, y] = op "*" [x, y] +schOp (Div IntegerType) [x, y] = op "quotient" [x, y] +schOp (Div ty) [x, y] = op "/" [x, y] +schOp (Mod ty) [x, y] = op "remainder" [x, y] +schOp (Neg ty) [x] = op "-" [x] +schOp (ShiftL ty) [x, y] = op "blodwen-shl" [x, y] +schOp (ShiftR ty) [x, y] = op "blodwen-shr" [x, y] +schOp (BAnd ty) [x, y] = op "blodwen-and" [x, y] +schOp (BOr ty) [x, y] = op "blodwen-or" [x, y] +schOp (BXOr ty) [x, y] = op "blodwen-xor" [x, y] +schOp (LT CharType) [x, y] = boolop "char=?" [x, y] +schOp (GT CharType) [x, y] = boolop "char>?" [x, y] +schOp (LT StringType) [x, y] = boolop "string=?" [x, y] +schOp (GT StringType) [x, y] = boolop "string>?" [x, y] +schOp (LT ty) [x, y] = boolop "<" [x, y] +schOp (LTE ty) [x, y] = boolop "<=" [x, y] +schOp (EQ ty) [x, y] = boolop "=" [x, y] +schOp (GTE ty) [x, y] = boolop ">=" [x, y] +schOp (GT ty) [x, y] = boolop ">" [x, y] +schOp StrLength [x] = op "string-length" [x] +schOp StrHead [x] = op "string-ref" [x, "0"] +schOp StrTail [x] = op "substring" [x, "1", op "string-length" [x]] +schOp StrIndex [x, i] = op "string-ref" [x, i] +schOp StrCons [x, y] = op "string-cons" [x, y] +schOp StrAppend [x, y] = op "string-append" [x, y] +schOp StrReverse [x] = op "string-reverse" [x] +schOp StrSubstr [x, y, z] = op "string-substr" [x, y, z] + +-- `e` is Euler's number, which approximates to: 2.718281828459045 +schOp DoubleExp [x] = op "exp" [x] -- Base is `e`. Same as: `pow(e, x)` +schOp DoubleLog [x] = op "log" [x] -- Base is `e`. +schOp DoubleSin [x] = op "sin" [x] +schOp DoubleCos [x] = op "cos" [x] +schOp DoubleTan [x] = op "tan" [x] +schOp DoubleASin [x] = op "asin" [x] +schOp DoubleACos [x] = op "acos" [x] +schOp DoubleATan [x] = op "atan" [x] +schOp DoubleSqrt [x] = op "sqrt" [x] +schOp DoubleFloor [x] = op "floor" [x] +schOp DoubleCeiling [x] = op "ceiling" [x] + +schOp (Cast IntType StringType) [x] = op "number->string" [x] +schOp (Cast IntegerType StringType) [x] = op "number->string" [x] +schOp (Cast DoubleType StringType) [x] = op "number->string" [x] +schOp (Cast CharType StringType) [x] = op "string" [x] + +schOp (Cast IntType IntegerType) [x] = x +schOp (Cast DoubleType IntegerType) [x] = op "exact-floor" [x] +schOp (Cast CharType IntegerType) [x] = op "char->integer" [x] +schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x] + +schOp (Cast IntegerType IntType) [x] = x +schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x] +schOp (Cast StringType IntType) [x] = op "cast-string-int" [x] +schOp (Cast CharType IntType) [x] = op "char->integer" [x] + +schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x] +schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x] +schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x] + +schOp (Cast IntType CharType) [x] = op "integer->char" [x] + +schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")" + +schOp BelieveMe [_,_,x] = x +schOp Crash [_,msg] = "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))" + +||| Extended primitives for the scheme backend, outside the standard set of primFn +public export +data ExtPrim = CCall | SchemeCall + | NewIORef | ReadIORef | WriteIORef + | NewArray | ArrayGet | ArraySet + | GetField | SetField + | VoidElim + | SysOS | SysCodegen + | Unknown Name + +export +Show ExtPrim where + show CCall = "CCall" + show SchemeCall = "SchemeCall" + show NewIORef = "NewIORef" + show ReadIORef = "ReadIORef" + show WriteIORef = "WriteIORef" + show NewArray = "NewArray" + show ArrayGet = "ArrayGet" + show ArraySet = "ArraySet" + show GetField = "GetField" + show SetField = "SetField" + show VoidElim = "VoidElim" + show SysOS = "SysOS" + show SysCodegen = "SysCodegen" + show (Unknown n) = "Unknown " ++ show n + +||| Match on a user given name to get the scheme primitive +toPrim : Name -> ExtPrim +toPrim pn@(NS _ n) + = cond [(n == UN "prim__schemeCall", SchemeCall), + (n == UN "prim__cCall", CCall), + (n == UN "prim__newIORef", NewIORef), + (n == UN "prim__readIORef", ReadIORef), + (n == UN "prim__writeIORef", WriteIORef), + (n == UN "prim__newArray", NewArray), + (n == UN "prim__arrayGet", ArrayGet), + (n == UN "prim__arraySet", ArraySet), + (n == UN "prim__getField", GetField), + (n == UN "prim__setField", SetField), + (n == UN "void", VoidElim), + (n == UN "prim__os", SysOS), + (n == UN "prim__codegen", SysCodegen) + ] + (Unknown pn) +toPrim pn = Unknown pn + +export +mkWorld : String -> String +mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- MkIORes + +schConstant : (String -> String) -> Constant -> String +schConstant _ (I x) = show x +schConstant _ (BI x) = show x +schConstant schString (Str x) = schString x +schConstant _ (Ch x) + = if (the Int (cast x) >= 32 && the Int (cast x) < 127) + then "#\\" ++ cast x + else "(integer->char " ++ show (the Int (cast x)) ++ ")" +schConstant _ (Db x) = show x +schConstant _ WorldVal = "#f" +schConstant _ IntType = "#t" +schConstant _ IntegerType = "#t" +schConstant _ StringType = "#t" +schConstant _ CharType = "#t" +schConstant _ DoubleType = "#t" +schConstant _ WorldType = "#t" + +schCaseDef : Maybe String -> String +schCaseDef Nothing = "" +schCaseDef (Just tm) = "(else " ++ tm ++ ")" + +export +schArglist : List Name -> String +schArglist [] = "" +schArglist [x] = schName x +schArglist (x :: xs) = schName x ++ " " ++ schArglist xs + +mutual + used : Name -> NamedCExp -> Bool + used n (NmLocal fc n') = n == n' + used n (NmRef _ _) = False + used n (NmLam _ _ sc) = used n sc + used n (NmLet _ _ v sc) = used n v || used n sc + used n (NmApp _ f args) = used n f || anyTrue (map (used n) args) + used n (NmCon _ _ _ args) = anyTrue (map (used n) args) + used n (NmOp _ _ args) = anyTrue (toList (map (used n) args)) + used n (NmExtPrim _ _ args) = anyTrue (map (used n) args) + used n (NmForce _ t) = used n t + used n (NmDelay _ t) = used n t + used n (NmConCase _ sc alts def) + = used n sc || anyTrue (map (usedCon n) alts) + || maybe False (used n) def + used n (NmConstCase _ sc alts def) + = used n sc || anyTrue (map (usedConst n) alts) + || maybe False (used n) def + used n _ = False + + usedCon : Name -> NamedConAlt -> Bool + usedCon n (MkNConAlt _ _ _ sc) = used n sc + + usedConst : Name -> NamedConstAlt -> Bool + usedConst n (MkNConstAlt _ sc) = used n sc + +parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String, + schString : String -> String) + showTag : Name -> Maybe Int -> String + showTag n (Just i) = show i + showTag n Nothing = schString (show n) + + mutual + schConAlt : Int -> String -> NamedConAlt -> Core String + schConAlt i target (MkNConAlt n tag args sc) + = pure $ "((" ++ showTag n tag ++ ") " + ++ bindArgs 1 args !(schExp i sc) ++ ")" + where + bindArgs : Int -> (ns : List Name) -> String -> String + bindArgs i [] body = body + bindArgs i (n :: ns) body + = if used n sc + then "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) " + ++ bindArgs (i + 1) ns body ++ ")" + else bindArgs (i + 1) ns body + + schConUncheckedAlt : Int -> String -> NamedConAlt -> Core String + schConUncheckedAlt i target (MkNConAlt n tag args sc) + = pure $ bindArgs 1 args !(schExp i sc) + where + bindArgs : Int -> (ns : List Name) -> String -> String + bindArgs i [] body = body + bindArgs i (n :: ns) body + = if used n sc + then "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) " + ++ bindArgs (i + 1) ns body ++ ")" + else bindArgs (i + 1) ns body + + schConstAlt : Int -> String -> NamedConstAlt -> Core String + schConstAlt i target (MkNConstAlt c exp) + = pure $ "((equal? " ++ target ++ " " ++ schConstant schString c ++ ") " ++ !(schExp i exp) ++ ")" + + -- oops, no traverse for Vect in Core + schArgs : Int -> Vect n NamedCExp -> Core (Vect n String) + schArgs i [] = pure [] + schArgs i (arg :: args) = pure $ !(schExp i arg) :: !(schArgs i args) + + export + schExp : Int -> NamedCExp -> Core String + schExp i (NmLocal fc n) = pure $ schName n + schExp i (NmRef fc n) = pure $ schName n + schExp i (NmLam fc x sc) + = do sc' <- schExp i sc + pure $ "(lambda (" ++ schName x ++ ") " ++ sc' ++ ")" + schExp i (NmLet fc x val sc) + = do val' <- schExp i val + sc' <- schExp i sc + pure $ "(let ((" ++ schName x ++ " " ++ val' ++ ")) " ++ sc' ++ ")" + schExp i (NmApp fc x []) + = pure $ "(" ++ !(schExp i x) ++ ")" + schExp i (NmApp fc x args) + = pure $ "(" ++ !(schExp i x) ++ " " ++ showSep " " !(traverse (schExp i) args) ++ ")" + schExp i (NmCon fc x tag args) + = pure $ schConstructor schString x tag !(traverse (schExp i) args) + schExp i (NmOp fc op args) + = pure $ schOp op !(schArgs i args) + schExp i (NmExtPrim fc p args) + = schExtPrim i (toPrim p) args + schExp i (NmForce fc t) = pure $ "(" ++ !(schExp i t) ++ ")" + schExp i (NmDelay fc t) = pure $ "(lambda () " ++ !(schExp i t) ++ ")" + schExp i (NmConCase fc sc [] def) + = do tcode <- schExp (i+1) sc + defc <- maybe (pure "'erased") (schExp i) def + let n = "sc" ++ show i + pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) " + ++ defc ++ ")" + schExp i (NmConCase fc sc [alt] Nothing) + = do tcode <- schExp (i+1) sc + let n = "sc" ++ show i + pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) " ++ + !(schConUncheckedAlt (i+1) n alt) ++ ")" + schExp i (NmConCase fc sc alts Nothing) + = do tcode <- schExp (i+1) sc + let n = "sc" ++ show i + pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (vector-ref " ++ n ++ " 0) " + ++ !(showAlts n alts) ++ + "))" + where + showAlts : String -> List NamedConAlt -> Core String + showAlts n [] = pure "" + showAlts n [alt] + = pure $ "(else " ++ !(schConUncheckedAlt (i + 1) n alt) ++ ")" + showAlts n (alt :: alts) + = pure $ !(schConAlt (i + 1) n alt) ++ " " ++ + !(showAlts n alts) + schExp i (NmConCase fc sc alts def) + = do tcode <- schExp (i+1) sc + defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def + let n = "sc" ++ show i + pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (vector-ref " ++ n ++ " 0) " + ++ showSep " " !(traverse (schConAlt (i+1) n) alts) + ++ schCaseDef defc ++ "))" + schExp i (NmConstCase fc sc alts Nothing) + = do tcode <- schExp (i+1) sc + let n = "sc" ++ show i + pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond " + ++ !(showConstAlts n alts) + ++ "))" + where + showConstAlts : String -> List NamedConstAlt -> Core String + showConstAlts n [] = pure "" + showConstAlts n [MkNConstAlt c exp] + = pure $ "(else " ++ !(schExp (i + 1) exp) ++ ")" + showConstAlts n (alt :: alts) + = pure $ !(schConstAlt (i + 1) n alt) ++ " " ++ + !(showConstAlts n alts) + schExp i (NmConstCase fc sc alts def) + = do defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def + tcode <- schExp (i+1) sc + let n = "sc" ++ show i + pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond " + ++ showSep " " !(traverse (schConstAlt (i+1) n) alts) + ++ schCaseDef defc ++ "))" + schExp i (NmPrimVal fc c) = pure $ schConstant schString c + schExp i (NmErased fc) = pure "'erased" + schExp i (NmCrash fc msg) = pure $ "(blodwen-error-quit " ++ show msg ++ ")" + + -- Need to convert the argument (a list of scheme arguments that may + -- have been constructed at run time) to a scheme list to be passed to apply + readArgs : Int -> NamedCExp -> Core String + readArgs i tm = pure $ "(blodwen-read-args " ++ !(schExp i tm) ++ ")" + + fileOp : String -> String + fileOp op = "(blodwen-file-op (lambda () " ++ op ++ "))" + + -- External primitives which are common to the scheme codegens (they can be + -- overridden) + export + schExtCommon : Int -> ExtPrim -> List NamedCExp -> Core String + schExtCommon i SchemeCall [ret, NmPrimVal fc (Str fn), args, world] + = pure $ mkWorld ("(apply " ++ fn ++" " + ++ !(readArgs i args) ++ ")") + schExtCommon i SchemeCall [ret, fn, args, world] + = pure $ mkWorld ("(apply (eval (string->symbol " ++ !(schExp i fn) ++")) " + ++ !(readArgs i args) ++ ")") + schExtCommon i NewIORef [_, val, world] + = pure $ mkWorld $ "(box " ++ !(schExp i val) ++ ")" + schExtCommon i ReadIORef [_, ref, world] + = pure $ mkWorld $ "(unbox " ++ !(schExp i ref) ++ ")" + schExtCommon i WriteIORef [_, ref, val, world] + = pure $ mkWorld $ "(set-box! " + ++ !(schExp i ref) ++ " " + ++ !(schExp i val) ++ ")" + schExtCommon i NewArray [_, size, val, world] + = pure $ mkWorld $ "(make-vector " ++ !(schExp i size) ++ " " + ++ !(schExp i val) ++ ")" + schExtCommon i ArrayGet [_, arr, pos, world] + = pure $ mkWorld $ "(vector-ref " ++ !(schExp i arr) ++ " " + ++ !(schExp i pos) ++ ")" + schExtCommon i ArraySet [_, arr, pos, val, world] + = pure $ mkWorld $ "(vector-set! " ++ !(schExp i arr) ++ " " + ++ !(schExp i pos) ++ " " + ++ !(schExp i val) ++ ")" + schExtCommon i VoidElim [_, _] + = pure "(display \"Error: Executed 'void'\")" + schExtCommon i SysOS [] + = pure $ show os + schExtCommon i (Unknown n) args + = throw (InternalError ("Can't compile unknown external primitive " ++ show n)) + schExtCommon i prim args + = throw (InternalError ("Badly formed external primitive " ++ show prim + ++ " " ++ show args)) + + schDef : {auto c : Ref Ctxt Defs} -> + Name -> NamedDef -> Core String + schDef n (MkNmFun args exp) + = pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist args ++ ") " + ++ !(schExp 0 exp) ++ "))\n" + schDef n (MkNmError exp) + = pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 exp) ++ ")\n" + schDef n (MkNmForeign _ _ _) = pure "" -- compiled by specific back end + schDef n (MkNmCon t a _) = pure "" -- Nothing to compile here + +-- Convert the name to scheme code +-- (There may be no code generated, for example if it's a constructor) +export +getScheme : {auto c : Ref Ctxt Defs} -> + (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String) -> + (schString : String -> String) -> + (Name, FC, NamedDef) -> Core String +getScheme schExtPrim schString (n, fc, d) + = schDef schExtPrim schString n d diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr new file mode 100644 index 000000000..9489bab12 --- /dev/null +++ b/src/Compiler/Scheme/Gambit.idr @@ -0,0 +1,319 @@ +module Compiler.Scheme.Gambit + +import Compiler.Common +import Compiler.CompileExpr +import Compiler.Inline +import Compiler.Scheme.Common + +import Core.Context +import Core.Directory +import Core.Name +import Core.Options +import Core.TT +import Utils.Hex + +import Data.List +import Data.Maybe +import Data.NameMap +import Data.Strings +import Data.Vect +import System +import System.Info + +%default covering + +-- TODO Look for gsi-script, then gsi +findGSI : IO String +findGSI = + do env <- getEnv "GAMBIT_GSI" + pure $ fromMaybe "/usr/bin/env -S gsi-script" env + +-- TODO Look for gsc-script, then gsc +findGSC : IO String +findGSC = + do env <- getEnv "GAMBIT_GSC" + pure $ fromMaybe "/usr/bin/env -S gsc-script" env + +schHeader : String +schHeader = "(declare (block) + (inlining-limit 450) + (standard-bindings) + (extended-bindings) + (not safe) + (optimize-dead-definitions))\n" + +showGambitChar : Char -> String -> String +showGambitChar '\\' = ("\\\\" ++) +showGambitChar c + = if c < chr 32 -- XXX + then (("\\x" ++ asHex (cast c) ++ ";") ++) + else strCons c + +showGambitString : List Char -> String -> String +showGambitString [] = id +showGambitString ('"'::cs) = ("\\\"" ++) . showGambitString cs +showGambitString (c::cs) = (showGambitChar c) . showGambitString cs + +gambitString : String -> String +gambitString cs = strCons '"' (showGambitString (unpack cs) "\"") + +mutual + -- Primitive types have been converted to names for the purpose of matching + -- on types + tySpec : NamedCExp -> Core String + tySpec (NmCon fc (UN "Int") _ []) = pure "int" + tySpec (NmCon fc (UN "String") _ []) = pure "UTF-8-string" + tySpec (NmCon fc (UN "Double") _ []) = pure "double" + tySpec (NmCon fc (UN "Char") _ []) = pure "char" + tySpec (NmCon fc (NS _ n) _ [_]) + = cond [(n == UN "Ptr", pure "(pointer void)")] + (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function"))) + tySpec (NmCon fc (NS _ n) _ []) + = cond [(n == UN "Unit", pure "void"), + (n == UN "AnyPtr", pure "(pointer void)")] + (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function"))) + tySpec ty = throw (GenericMsg (getFC ty) ("Can't pass argument of type " ++ show ty ++ " to foreign function")) + + handleRet : String -> String -> String + handleRet "void" op = op ++ " " ++ mkWorld (schConstructor gambitString (UN "") (Just 0) []) + handleRet _ op = mkWorld op + + getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp)) + getFArgs (NmCon fc _ (Just 0) _) = pure [] + getFArgs (NmCon fc _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest) + getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg)) + + gambitPrim : Int -> ExtPrim -> List NamedCExp -> Core String + gambitPrim i CCall [ret, NmPrimVal fc (Str fn), fargs, world] + = do args <- getFArgs fargs + argTypes <- traverse tySpec (map fst args) + retType <- tySpec ret + argsc <- traverse (schExp gambitPrim gambitString 0) (map snd args) + pure $ handleRet retType ("((c-lambda (" ++ showSep " " argTypes ++ ") " + ++ retType ++ " " ++ show fn ++ ") " + ++ showSep " " argsc ++ ")") + gambitPrim i CCall [ret, fn, args, world] + = pure "(error \"bad ffi call\")" + gambitPrim i GetField [NmPrimVal _ (Str s), _, _, struct, + NmPrimVal _ (Str fld), _] + = do structsc <- schExp gambitPrim gambitString 0 struct + pure $ "(" ++ s ++ "-" ++ fld ++ " " ++ structsc ++ ")" + gambitPrim i GetField [_,_,_,_,_,_] + = pure "(error \"bad getField\")" + gambitPrim i SetField [NmPrimVal _ (Str s), _, _, struct, + NmPrimVal _ (Str fld), _, val, world] + = do structsc <- schExp gambitPrim gambitString 0 struct + valsc <- schExp gambitPrim gambitString 0 val + pure $ mkWorld $ + "(" ++ s ++ "-" ++ fld ++ "-set! " ++ structsc ++ " " ++ valsc ++ ")" + gambitPrim i SetField [_,_,_,_,_,_,_,_] + = pure "(error \"bad setField\")" + gambitPrim i SysCodegen [] + = pure $ "\"gambit\"" + gambitPrim i prim args + = schExtCommon gambitPrim gambitString i prim args + +-- Reference label for keeping track of loaded external libraries +data Loaded : Type where + +-- Label for noting which struct types are declared +data Structs : Type where + +cftySpec : FC -> CFType -> Core String +cftySpec fc CFUnit = pure "void" +cftySpec fc CFInt = pure "int" +cftySpec fc CFString = pure "UTF-8-string" +cftySpec fc CFDouble = pure "double" +cftySpec fc CFChar = pure "char" +cftySpec fc CFPtr = pure "(pointer void)" +cftySpec fc (CFIORes t) = cftySpec fc t +cftySpec fc (CFStruct n t) = pure $ n ++ "*/nonnull" +cftySpec fc (CFFun s t) = funTySpec [s] t + where + funTySpec : List CFType -> CFType -> Core String + funTySpec args (CFFun CFWorld t) = funTySpec args t + funTySpec args (CFFun s t) = funTySpec (s :: args) t + funTySpec args retty + = do rtyspec <- cftySpec fc retty + argspecs <- traverse (cftySpec fc) (reverse args) + pure $ "(function (" ++ showSep " " argspecs ++ ") " ++ rtyspec ++ ")" +cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++ + " to foreign function")) + +cCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> (cfn : String) -> (clib : String) -> + List (Name, CFType) -> CFType -> Core (String, String) +cCall fc cfn clib args ret + = do -- loaded <- get Loaded + -- lib <- if clib `elem` loaded + -- then pure "" + -- else do (fname, fullname) <- locate clib + -- copyLib (fname, fullname) + -- put Loaded (clib :: loaded) + -- pure "" + argTypes <- traverse (\a => cftySpec fc (snd a)) args + retType <- cftySpec fc ret + let call = "((c-lambda (" ++ showSep " " argTypes ++ ") " + ++ retType ++ " " ++ show cfn ++ ") " + ++ showSep " " !(traverse buildArg args) ++ ")" + + pure ("", case ret of -- XXX + CFIORes _ => handleRet retType call + _ => call) + where + mkNs : Int -> List CFType -> List (Maybe String) + mkNs i [] = [] + mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs + mkNs i (x :: xs) = Just ("cb" ++ show i) :: mkNs (i + 1) xs + + applyLams : String -> List (Maybe String) -> String + applyLams n [] = n + applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as + applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as + + mkFun : List CFType -> CFType -> String -> String + mkFun args ret n + = let argns = mkNs 0 args in + "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " + ++ (applyLams n argns ++ ")") + + notWorld : CFType -> Bool + notWorld CFWorld = False + notWorld _ = True + + callback : String -> List CFType -> CFType -> Core String + callback n args (CFFun s t) = callback n (s :: args) t + callback n args_rev retty + = do let args = reverse args_rev + argTypes <- traverse (cftySpec fc) (filter notWorld args) + retType <- cftySpec fc retty + pure $ mkFun args retty n -- FIXME Needs a top-level c-define + + buildArg : (Name, CFType) -> Core String + buildArg (n, CFFun s t) = callback (schName n) [s] t + buildArg (n, _) = pure $ schName n + +schemeCall : FC -> (sfn : String) -> + List Name -> CFType -> Core String +schemeCall fc sfn argns ret + = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in + case ret of + CFIORes _ => pure $ mkWorld call + _ => pure call + +-- Use a calling convention to compile a foreign def. +-- Returns any preamble needed for loading libraries, and the body of the +-- function call. +useCC : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String) +useCC fc [] args ret + = throw (GenericMsg fc "No recognised foreign calling convention") +useCC fc (cc :: ccs) args ret + = case parseCC cc of + Nothing => useCC fc ccs args ret + Just ("scheme", [sfn]) => + do body <- schemeCall fc sfn (map fst args) ret + pure ("", body) + Just ("C", [cfn, clib]) => cCall fc cfn clib args ret + Just ("C", [cfn, clib, chdr]) => cCall fc cfn clib args ret + _ => useCC fc ccs args ret + +-- For every foreign arg type, return a name, and whether to pass it to the +-- foreign call (we don't pass '%World') +mkArgs : Int -> List CFType -> List (Name, Bool) +mkArgs i [] = [] +mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs +mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs + +mkStruct : {auto s : Ref Structs (List String)} -> + CFType -> Core String +mkStruct (CFStruct n flds) + = do defs <- traverse mkStruct (map snd flds) + strs <- get Structs + if n `elem` strs + then pure (concat defs) + else do put Structs (n :: strs) + pure $ concat defs ++ "(define-c-struct " ++ n ++ " " + ++ showSep " " !(traverse showFld flds) ++ ")\n" + where + showFld : (String, CFType) -> Core String + showFld (n, ty) = pure $ "(" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ ")" +mkStruct (CFIORes t) = mkStruct t +mkStruct (CFFun a b) = do mkStruct a; mkStruct b +mkStruct _ = pure "" + +schFgnDef : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + {auto s : Ref Structs (List String)} -> + FC -> Name -> NamedDef -> Core (String, String) +schFgnDef fc n (MkNmForeign cs args ret) + = 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 fc cs (zip useargns args) ret + defs <- get Ctxt + pure (load, + concat argStrs ++ retStr ++ + "(define " ++ schName !(full (gamma defs) n) ++ + " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++ + body ++ "))\n") +schFgnDef _ _ _ = pure ("", "") + +getFgnCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + {auto s : Ref Structs (List String)} -> + (Name, FC, NamedDef) -> Core (String, String) +getFgnCall (n, fc, d) = schFgnDef fc n d + +-- TODO Include libraries from the directives +compileToSCM : Ref Ctxt Defs -> + ClosedTerm -> (outfile : String) -> Core () +compileToSCM c tm outfile + = do cdata <- getCompileData Cases tm + let ndefs = namedDefs cdata + -- let tags = nameTags cdata + let ctm = forget (mainExpr cdata) + + defs <- get Ctxt + l <- newRef {t = List String} Loaded [] + s <- newRef {t = List String} Structs [] + fgndefs <- traverse getFgnCall ndefs + compdefs <- traverse (getScheme gambitPrim gambitString) ndefs + let code = fastAppend (map snd fgndefs ++ compdefs) ++ + concat (map fst fgndefs) + main <- schExp gambitPrim gambitString 0 ctm + support <- readDataFile "gambit/support.scm" + foreign <- readDataFile "gambit/foreign.scm" + let scm = showSep "\n" [schHeader, support, foreign, code, main] + Right () <- coreLift $ writeFile outfile scm + | Left err => throw (FileErr outfile err) + pure () + +-- TODO Include external libraries on compilation +compileExpr : Ref Ctxt Defs -> (execDir : String) -> + ClosedTerm -> (outfile : String) -> Core (Maybe String) +compileExpr c execDir tm outfile + = do let outn = execDir ++ dirSep ++ outfile ++ ".scm" + compileToSCM c tm outn + gsc <- coreLift findGSC + ok <- coreLift $ system (gsc ++ " -exe " ++ outn) + if ok == 0 + then pure (Just outfile) + else pure Nothing + +executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core () +executeExpr c execDir tm + = do let tmp = execDir ++ dirSep ++ "_tmpgambit" + let outn = tmp ++ ".scm" + compileToSCM c tm outn + gsi <- coreLift findGSI + coreLift $ system (gsi ++ " " ++ outn) + pure () + +export +codegenGambit : Codegen +codegenGambit = MkCG compileExpr executeExpr diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr new file mode 100644 index 000000000..24fb267ec --- /dev/null +++ b/src/Compiler/Scheme/Racket.idr @@ -0,0 +1,343 @@ +module Compiler.Scheme.Racket + +import Compiler.Common +import Compiler.CompileExpr +import Compiler.Inline +import Compiler.Scheme.Common + +import Core.Options +import Core.Context +import Core.Directory +import Core.Name +import Core.TT +import Utils.Hex + +import Data.List +import Data.Maybe +import Data.NameMap +import Data.Nat +import Data.Strings +import Data.Vect +import System +import System.Info + +%default covering + +findRacket : IO String +findRacket = + do env <- getEnv "RACKET" + pure $ fromMaybe "/usr/bin/env racket" env + +findRacoExe : IO String +findRacoExe = + do env <- getEnv "RACKET_RACO" + pure $ (fromMaybe "/usr/bin/env raco" env) ++ " exe" + +schHeader : String -> String +schHeader libs + = "#lang racket/base\n" ++ + "(require racket/math)\n" ++ -- for math ops + "(require racket/system)\n" ++ -- for system + "(require srfi/19)\n" ++ -- for file handling and data + "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C + libs ++ + "(let ()\n" + +schFooter : String +schFooter = ")" + +showRacketChar : Char -> String -> String +showRacketChar '\\' = ("\\\\" ++) +showRacketChar c + = if c < chr 32 || c > chr 126 + then (("\\u" ++ pad (asHex (cast c))) ++) + else strCons c + where + pad : String -> String + pad str + = case isLTE (length str) 4 of + Yes _ => pack (List.replicate (minus 4 (length str)) '0') ++ str + No _ => str + +showRacketString : List Char -> String -> String +showRacketString [] = id +showRacketString ('"'::cs) = ("\\\"" ++) . showRacketString cs +showRacketString (c ::cs) = (showRacketChar c) . showRacketString cs + +racketString : String -> String +racketString cs = strCons '"' (showRacketString (unpack cs) "\"") + +mutual + racketPrim : Int -> ExtPrim -> List NamedCExp -> Core String + racketPrim i CCall [ret, fn, args, world] + = throw (InternalError ("Can't compile C FFI calls to Racket yet")) + racketPrim i GetField [NmPrimVal _ (Str s), _, _, struct, + NmPrimVal _ (Str fld), _] + = do structsc <- schExp racketPrim racketString 0 struct + pure $ "(" ++ s ++ "-" ++ fld ++ " " ++ structsc ++ ")" + racketPrim i GetField [_,_,_,_,_,_] + = pure "(error \"bad getField\")" + racketPrim i SetField [NmPrimVal _ (Str s), _, _, struct, + NmPrimVal _ (Str fld), _, val, world] + = do structsc <- schExp racketPrim racketString 0 struct + valsc <- schExp racketPrim racketString 0 val + pure $ mkWorld $ + "(set-" ++ s ++ "-" ++ fld ++ "! " ++ structsc ++ " " ++ valsc ++ ")" + racketPrim i SetField [_,_,_,_,_,_,_,_] + = pure "(error \"bad setField\")" + racketPrim i SysCodegen [] + = pure $ "\"racket\"" + racketPrim i prim args + = schExtCommon racketPrim racketString i prim args + +-- Reference label for keeping track of loaded external libraries +data Loaded : Type where + +-- Label for noting which struct types are declared +data Structs : Type where + +-- Label for noting which foreign names are declared +data Done : Type where + +cftySpec : FC -> CFType -> Core String +cftySpec fc CFUnit = pure "_void" +cftySpec fc CFInt = pure "_int" +cftySpec fc CFString = pure "_string/utf-8" +cftySpec fc CFDouble = pure "_double" +cftySpec fc CFChar = pure "_int8" +cftySpec fc CFPtr = pure "_pointer" +cftySpec fc (CFIORes t) = cftySpec fc t +cftySpec fc (CFStruct n t) = pure $ "_" ++ n ++ "-pointer" +cftySpec fc (CFFun s t) = funTySpec [s] t + where + funTySpec : List CFType -> CFType -> Core String + funTySpec args (CFFun CFWorld t) = funTySpec args t + funTySpec args (CFFun s t) = funTySpec (s :: args) t + funTySpec args retty + = do rtyspec <- cftySpec fc retty + argspecs <- traverse (cftySpec fc) (reverse args) + pure $ "(_fun " ++ showSep " " argspecs ++ " -> " ++ rtyspec ++ ")" +cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++ + " to foreign function")) + +loadlib : String -> String -> String +loadlib libn ver + = "(define-ffi-definer define-" ++ libn ++ + " (ffi-lib \"" ++ libn ++ "\" " ++ ver ++ "))\n" + +getLibVers : String -> (String, String) +getLibVers libspec + = case words libspec of + [] => ("", "") + [fn] => case span (/='.') libspec of + (root, rest) => (root, "") + (fn :: vers) => + (fst (span (/='.') fn), + "'(" ++ showSep " " (map show vers) ++ " #f)" ) + +cToRkt : CFType -> String -> String +cToRkt CFChar op = "(integer->char " ++ op ++ ")" +cToRkt _ op = op + +rktToC : CFType -> String -> String +rktToC CFChar op = "(char->integer " ++ op ++ ")" +rktToC _ op = op + +handleRet : CFType -> String -> String +handleRet CFUnit op = op ++ " " ++ mkWorld (schConstructor racketString (UN "") (Just 0) []) +handleRet ret op = mkWorld (cToRkt ret op) + +cCall : {auto f : Ref Done (List String) } -> + {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> (cfn : String) -> (clib : String) -> + List (Name, CFType) -> CFType -> Core (String, String) +cCall fc cfn libspec args ret + = do loaded <- get Loaded + bound <- get Done + + let (libn, vers) = getLibVers libspec + lib <- if libn `elem` loaded + then pure "" + else do put Loaded (libn :: loaded) + ldata <- locate libspec + copyLib ldata + pure (loadlib libn vers) + + argTypes <- traverse (\a => do s <- cftySpec fc (snd a) + pure (a, s)) args + retType <- cftySpec fc ret + cbind <- if cfn `elem` bound + then pure "" + else do put Done (cfn :: bound) + pure $ "(define-" ++ libn ++ " " ++ cfn ++ + " (_fun " ++ showSep " " (map snd argTypes) ++ " -> " ++ + retType ++ "))\n" + let call = "(" ++ cfn ++ " " ++ + showSep " " !(traverse useArg argTypes) ++ ")" + + pure (lib ++ cbind, case ret of + CFIORes rt => handleRet rt call + _ => call) + where + mkNs : Int -> List CFType -> List (Maybe (String, CFType)) + mkNs i [] = [] + mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs + mkNs i (x :: xs) = Just ("cb" ++ show i, x) :: mkNs (i + 1) xs + + applyLams : String -> List (Maybe (String, CFType)) -> String + applyLams n [] = n + applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as + applyLams n (Just (a, ty) :: as) + = applyLams ("(" ++ n ++ " " ++ cToRkt ty a ++ ")") as + + mkFun : List CFType -> CFType -> String -> String + mkFun args ret n + = let argns = mkNs 0 args in + "(lambda (" ++ showSep " " (map fst (mapMaybe id argns)) ++ ") " ++ + (applyLams n argns ++ ")") + + notWorld : CFType -> Bool + notWorld CFWorld = False + notWorld _ = True + + callback : String -> List CFType -> CFType -> Core String + callback n args (CFFun s t) = callback n (s :: args) t + callback n args_rev retty + = do let args = reverse args_rev + argTypes <- traverse (cftySpec fc) (filter notWorld args) + retType <- cftySpec fc retty + pure $ mkFun args retty n + + useArg : ((Name, CFType), String) -> Core String + useArg ((n, CFFun s t), _) = callback (schName n) [s] t + useArg ((n, ty), _) + = pure $ rktToC ty (schName n) + +schemeCall : FC -> (sfn : String) -> + List Name -> CFType -> Core String +schemeCall fc sfn argns ret + = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in + case ret of + CFIORes _ => pure $ mkWorld call + _ => pure call + +-- Use a calling convention to compile a foreign def. +-- Returns any preamble needed for loading libraries, and the body of the +-- function call. +useCC : {auto f : Ref Done (List String) } -> + {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String) +useCC fc [] args ret + = throw (GenericMsg fc "No recognised foreign calling convention") +useCC fc (cc :: ccs) args ret + = case parseCC cc of + Nothing => useCC fc ccs args ret + Just ("scheme", [sfn]) => + do body <- schemeCall fc sfn (map fst args) ret + pure ("", body) + Just ("C", [cfn, clib]) => cCall fc cfn clib args ret + Just ("C", [cfn, clib, chdr]) => cCall fc cfn clib args ret + _ => useCC fc ccs args ret + +-- For every foreign arg type, return a name, and whether to pass it to the +-- foreign call (we don't pass '%World') +mkArgs : Int -> List CFType -> List (Name, Bool) +mkArgs i [] = [] +mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs +mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs + +mkStruct : {auto s : Ref Structs (List String)} -> + CFType -> Core String +mkStruct (CFStruct n flds) + = do defs <- traverse mkStruct (map snd flds) + strs <- get Structs + if n `elem` strs + then pure (concat defs) + else do put Structs (n :: strs) + pure $ concat defs ++ "(define-cstruct _" ++ n ++ " (" + ++ showSep "\n\t" !(traverse showFld flds) ++ "))\n" + where + showFld : (String, CFType) -> Core String + showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]" +mkStruct (CFIORes t) = mkStruct t +mkStruct (CFFun a b) = do mkStruct a; mkStruct b +mkStruct _ = pure "" + +schFgnDef : {auto f : Ref Done (List String) } -> + {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + {auto s : Ref Structs (List String)} -> + FC -> Name -> NamedDef -> Core (String, String) +schFgnDef fc n (MkNmForeign cs args ret) + = 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 fc cs (zip useargns args) ret + defs <- get Ctxt + pure (concat argStrs ++ retStr ++ load, + "(define " ++ schName !(full (gamma defs) n) ++ + " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++ + body ++ "))\n") +schFgnDef _ _ _ = pure ("", "") + +getFgnCall : {auto f : Ref Done (List String) } -> + {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + {auto s : Ref Structs (List String)} -> + (Name, FC, NamedDef) -> Core (String, String) +getFgnCall (n, fc, d) = schFgnDef fc n d + +compileToRKT : Ref Ctxt Defs -> + ClosedTerm -> (outfile : String) -> Core () +compileToRKT c tm outfile + = do cdata <- getCompileData Cases tm + let ndefs = namedDefs cdata + let ctm = forget (mainExpr cdata) + + defs <- get Ctxt + f <- newRef {t = List String} Done empty + l <- newRef {t = List String} Loaded [] + s <- newRef {t = List String} Structs [] + fgndefs <- traverse getFgnCall ndefs + compdefs <- traverse (getScheme racketPrim racketString) ndefs + let code = fastAppend (map snd fgndefs ++ compdefs) + main <- schExp racketPrim racketString 0 ctm + support <- readDataFile "racket/support.rkt" + let scm = schHeader (concat (map fst fgndefs)) ++ + support ++ code ++ + "(void " ++ main ++ ")\n" ++ + schFooter + Right () <- coreLift $ writeFile outfile scm + | Left err => throw (FileErr outfile err) + coreLift $ chmodRaw outfile 0o755 + pure () + +compileExpr : Ref Ctxt Defs -> (execDir : String) -> + ClosedTerm -> (outfile : String) -> Core (Maybe String) +compileExpr c execDir tm outfile + = do let outSs = execDir ++ dirSep ++ outfile ++ ".rkt" + let outBin = execDir ++ dirSep ++ outfile + compileToRKT c tm outSs + raco <- coreLift findRacoExe + ok <- coreLift $ system (raco ++ " -o " ++ outBin ++ " " ++ outSs) + if ok == 0 + then pure (Just outfile) + else pure Nothing + +executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core () +executeExpr c execDir tm + = do let tmp = execDir ++ dirSep ++ "_tmpracket" + let outn = tmp ++ ".rkt" + compileToRKT c tm outn + racket <- coreLift findRacket + coreLift $ system (racket ++ " " ++ outn) + pure () + +export +codegenRacket : Codegen +codegenRacket = MkCG compileExpr executeExpr + diff --git a/src/Compiler/VMCode.idr b/src/Compiler/VMCode.idr new file mode 100644 index 000000000..43f53aea9 --- /dev/null +++ b/src/Compiler/VMCode.idr @@ -0,0 +1,198 @@ +module Compiler.VMCode + +import Compiler.ANF + +import Core.CompileExpr +import Core.Context +import Core.Core +import Core.TT + +import Data.List +import Data.Maybe +import Data.Vect + +%default covering + +public export +data Reg : Type where + RVal : Reg + Loc : Int -> Reg + Discard : Reg + +-- VM instructions - first Reg is where the result goes, unless stated +-- otherwise. + +-- As long as you have a representation of closures, and an 'apply' function +-- which adds an argument and evaluates if it's fully applied, then you can +-- translate this directly to a target language program. +public export +data VMInst : Type where + DECLARE : Reg -> VMInst + START : VMInst -- start of the main body of the function + ASSIGN : Reg -> Reg -> VMInst + MKCON : Reg -> (tag : Maybe Int) -> (args : List Reg) -> VMInst + MKCLOSURE : Reg -> Name -> (missing : Nat) -> (args : List Reg) -> VMInst + MKCONSTANT : Reg -> Constant -> VMInst + + APPLY : Reg -> (f : Reg) -> (a : Reg) -> VMInst + CALL : Reg -> (tailpos : Bool) -> Name -> (args : List Reg) -> VMInst + OP : Reg -> PrimFn arity -> Vect arity Reg -> VMInst + EXTPRIM : Reg -> Name -> List Reg -> VMInst + + CASE : Reg -> -- scrutinee + (alts : List (Either Int Name, List VMInst)) -> -- based on constructor tag + (def : Maybe (List VMInst)) -> + VMInst + CONSTCASE : Reg -> -- scrutinee + (alts : List (Constant, List VMInst)) -> + (def : Maybe (List VMInst)) -> + VMInst + PROJECT : Reg -> (value : Reg) -> (pos : Int) -> VMInst + NULL : Reg -> VMInst + + ERROR : String -> VMInst + +public export +data VMDef : Type where + MkVMFun : (args : List Int) -> List VMInst -> VMDef + MkVMError : List VMInst -> VMDef + +export +Show Reg where + show RVal = "RVAL" + show (Loc i) = "v" ++ show i + show Discard = "DISCARD" + +export +Show VMInst where + show (DECLARE r) = "DECLARE " ++ show r + show START = "START" + show (ASSIGN r v) = show r ++ " := " ++ show v + show (MKCON r t args) + = show r ++ " := MKCON " ++ show t ++ " (" ++ + showSep ", " (map show args) ++ ")" + show (MKCLOSURE r n m args) + = show r ++ " := MKCLOSURE " ++ show n ++ " " ++ show m ++ " (" ++ + showSep ", " (map show args) ++ ")" + show (MKCONSTANT r c) = show r ++ " := MKCONSTANT " ++ show c + show (APPLY r f a) = show r ++ " := " ++ show f ++ " @ " ++ show a + show (CALL r t n args) + = show r ++ " := " ++ (if t then "TAILCALL " else "CALL ") ++ + show n ++ "(" ++ showSep ", " (map show args) ++ ")" + show (OP r op args) + = show r ++ " := " ++ "OP " ++ + show op ++ "(" ++ showSep ", " (map show (toList args)) ++ ")" + show (EXTPRIM r n args) + = show r ++ " := " ++ "EXTPRIM " ++ + show n ++ "(" ++ showSep ", " (map show args) ++ ")" + + show (CASE scr alts def) + = "CASE " ++ show scr ++ " " ++ show alts ++ " {default: " ++ show def ++ "}" + show (CONSTCASE scr alts def) + = "CASE " ++ show scr ++ " " ++ show alts ++ " {default: " ++ show def ++ "}" + + show (PROJECT r val pos) + = show r ++ " := PROJECT(" ++ show val ++ ", " ++ show pos ++ ")" + show (NULL r) = show r ++ " := NULL" + show (ERROR str) = "ERROR " ++ show str + +export +Show VMDef where + show (MkVMFun args body) = show args ++ ": " ++ show body + show (MkVMError err) = "Error: " ++ show err + +toReg : AVar -> Reg +toReg (ALocal i) = Loc i +toReg ANull = Discard + +toVM : (tailpos : Bool) -> (target : Reg) -> ANF -> List VMInst +toVM t Discard _ = [] +toVM t res (AV fc (ALocal i)) + = [ASSIGN res (Loc i)] +toVM t res (AAppName fc n args) + = [CALL res t n (map toReg args)] +toVM t res (AUnderApp fc n m args) + = [MKCLOSURE res n m (map toReg args)] +toVM t res (AApp fc f a) + = [APPLY res (toReg f) (toReg a)] +toVM t res (ALet fc var val body) + = toVM False (Loc var) val ++ toVM t res body +toVM t res (ACon fc n tag args) + = [MKCON res tag (map toReg args)] +toVM t res (AOp fc op args) + = [OP res op (map toReg args)] +toVM t res (AExtPrim fc p args) + = [EXTPRIM res p (map toReg args)] +toVM t res (AConCase fc (ALocal scr) alts def) + = [CASE (Loc scr) (map toVMConAlt alts) (map (toVM t res) def)] + where + projectArgs : Int -> List Int -> List VMInst + projectArgs i [] = [] + projectArgs i (arg :: args) + = PROJECT (Loc arg) (Loc scr) i :: projectArgs (i + 1) args + + toVMConAlt : AConAlt -> (Either Int Name, List VMInst) + toVMConAlt (MkAConAlt n (Just tag) args code) + = (Left tag, projectArgs 0 args ++ toVM t res code) + toVMConAlt (MkAConAlt n Nothing args code) + = (Right n, projectArgs 0 args ++ toVM t res code) +toVM t res (AConstCase fc (ALocal scr) alts def) + = [CONSTCASE (Loc scr) (map toVMConstAlt alts) (map (toVM t res) def)] + where + toVMConstAlt : AConstAlt -> (Constant, List VMInst) + toVMConstAlt (MkAConstAlt c code) + = (c, toVM t res code) +toVM t res (APrimVal fc c) + = [MKCONSTANT res c] +toVM t res (AErased fc) + = [NULL res] +toVM t res (ACrash fc err) + = [ERROR err] +toVM t res _ + = [NULL res] + +findVars : VMInst -> List Int +findVars (ASSIGN (Loc r) _) = [r] +findVars (MKCON (Loc r) _ _) = [r] +findVars (MKCLOSURE (Loc r) _ _ _) = [r] +findVars (MKCONSTANT (Loc r) _) = [r] +findVars (APPLY (Loc r) _ _) = [r] +findVars (CALL (Loc r) _ _ _) = [r] +findVars (OP (Loc r) _ _) = [r] +findVars (EXTPRIM (Loc r) _ _) = [r] +findVars (CASE _ alts d) + = concatMap findVarAlt alts ++ fromMaybe [] (map (concatMap findVars) d) + where + findVarAlt : (Either Int Name, List VMInst) -> List Int + findVarAlt (t, code) = concatMap findVars code +findVars (CONSTCASE _ alts d) + = concatMap findConstVarAlt alts ++ fromMaybe [] (map (concatMap findVars) d) + where + findConstVarAlt : (Constant, List VMInst) -> List Int + findConstVarAlt (t, code) = concatMap findVars code +findVars (PROJECT (Loc r) _ _) = [r] +findVars _ = [] + +declareVars : List Int -> List VMInst -> List VMInst +declareVars got code + = let vs = concatMap findVars code in + declareAll got vs + where + declareAll : List Int -> List Int -> List VMInst + declareAll got [] = START :: code + declareAll got (i :: is) + = if i `elem` got + then declareAll got is + else DECLARE (Loc i) :: declareAll (i :: got) is + +export +toVMDef : ANFDef -> Maybe VMDef +toVMDef (MkAFun args body) + = Just $ MkVMFun args (declareVars args (toVM True RVal body)) +toVMDef (MkAError body) + = Just $ MkVMError (declareVars [] (toVM True RVal body)) +toVMDef _ = Nothing + +export +allDefs : List (Name, ANFDef) -> List (Name, VMDef) +allDefs = mapMaybe (\ (n, d) => do d' <- toVMDef d; pure (n, d')) diff --git a/src/Data/StringTrie.idr b/src/Data/StringTrie.idr new file mode 100644 index 000000000..0185df2a4 --- /dev/null +++ b/src/Data/StringTrie.idr @@ -0,0 +1,66 @@ +module Data.StringTrie + +import Data.These +import Data.StringMap + +%default total + +-- prefix tree specialised to use `String`s as keys + +public export +record StringTrie a where + constructor MkStringTrie + node : These a (StringMap (StringTrie a)) + +public export +Show a => Show (StringTrie a) where + show (MkStringTrie node) = assert_total $ show node + +public export +Functor StringTrie where + map f (MkStringTrie node) = MkStringTrie $ assert_total $ bimap f (map (map f)) node + +public export +empty : StringTrie a +empty = MkStringTrie $ That empty + +public export +singleton : List String -> a -> StringTrie a +singleton [] v = MkStringTrie $ This v +singleton (k::ks) v = MkStringTrie $ That $ singleton k (singleton ks v) + +-- insert using supplied function to resolve clashes +public export +insertWith : List String -> (Maybe a -> a) -> StringTrie a -> StringTrie a +insertWith [] f (MkStringTrie nd) = + MkStringTrie $ these (This . f . Just) (Both (f Nothing)) (Both . f . Just) nd +insertWith (k::ks) f (MkStringTrie nd) = + MkStringTrie $ these (\x => Both x (singleton k end)) (That . rec) (\x => Both x . rec) nd + where + end : StringTrie a + end = singleton ks (f Nothing) + rec : StringMap (StringTrie a) -> StringMap (StringTrie a) + rec sm = maybe (insert k end sm) (\tm => insert k (insertWith ks f tm) sm) (lookup k sm) + +public export +insert : List String -> a -> StringTrie a -> StringTrie a +insert ks v = insertWith ks (const v) + +-- fold the trie in a depth-first fashion performing monadic actions on values, then keys +-- note that for `Both` the action on node values will be performed first because of `bitraverse` implementation +public export +foldWithKeysM : (Monad m, Monoid b) => (List String -> m b) -> (List String -> a -> m b) -> StringTrie a -> m b +foldWithKeysM {a} {m} {b} fk fv = go [] + where + go : List String -> StringTrie a -> m b + go ks (MkStringTrie nd) = + bifold <$> bitraverse + (fv ks) + (\sm => foldlM + (\x, (k, vs) => do let ks' = ks++[k] + y <- assert_total $ go ks' vs + z <- fk ks' + pure $ x <+> y <+> z) + neutral + (toList sm)) + nd diff --git a/src/Data/These.idr b/src/Data/These.idr new file mode 100644 index 000000000..54326cdd4 --- /dev/null +++ b/src/Data/These.idr @@ -0,0 +1,48 @@ +module Data.These + +%default total + +public export +data These a b = This a | That b | Both a b + +public export +fromEither : Either a b -> These a b +fromEither = either This That + +public export +these : (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c +these l r lr (This a) = l a +these l r lr (That b) = r b +these l r lr (Both a b) = lr a b + +public export +bimap : (f : a -> b) -> (g : c -> d) -> These a c -> These b d +bimap f g (This a) = This (f a) +bimap f g (That b) = That (g b) +bimap f g (Both a b) = Both (f a) (g b) + +public export +(Show a, Show b) => Show (These a b) where + showPrec d (This x) = showCon d "This" $ showArg x + showPrec d (That x) = showCon d "That" $ showArg x + showPrec d (Both x y) = showCon d "Both" $ showArg x ++ showArg y + +public export +Functor (These a) where + map = bimap id + +public export +mapFst : (f : a -> b) -> These a c -> These b c +mapFst f = bimap f id + +public export +bifold : Monoid m => These m m -> m +bifold (This a) = a +bifold (That b) = b +bifold (Both a b) = a <+> b + +public export +bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> These a b -> f (These c d) +bitraverse f g (This a) = [| This (f a) |] +bitraverse f g (That b) = [| That (g b) |] +bitraverse f g (Both a b) = [| Both (f a) (g b) |] diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr new file mode 100644 index 000000000..dfa12ec4e --- /dev/null +++ b/src/Idris/CommandLine.idr @@ -0,0 +1,259 @@ +module Idris.CommandLine + +import IdrisPaths + +import Idris.Version + +import Data.List +import Data.Maybe +import Data.Strings + +import System + +%default total + +public export +data PkgCommand + = Build + | Install + | Clean + | REPL + +export +Show PkgCommand where + show Build = "--build" + show Install = "--install" + show Clean = "--clean" + show REPL = "--repl" + +public export +data DirCommand + = LibDir -- show top level package directory + +export +Show DirCommand where + show LibDir = "--libdir" + +||| CLOpt - possible command line options +public export +data CLOpt + = + ||| Only typecheck the given file + CheckOnly | + ||| The output file from the code generator + OutputFile String | + ||| Execute a given function after checking the source file + ExecFn String | + ||| Use a specific code generator (default chez) + SetCG String | + ||| Don't implicitly import Prelude + NoPrelude | + ||| Show the installation prefix + ShowPrefix | + ||| Display Idris version + Version | + ||| Display help text + Help | + ||| Suppress the banner + NoBanner | + ||| Run Idris 2 in quiet mode + Quiet | + ||| Run Idris 2 in verbose mode (cancels quiet if it's the default) + Verbose | + ||| Add a package as a dependency + PkgPath String | + ||| Build or install a given package, depending on PkgCommand + Package PkgCommand String | + ||| Show locations of data/library directories + Directory DirCommand | + ||| The input Idris file + InputFile String | + ||| Whether or not to run in IdeMode (easily parsable for other tools) + IdeMode | + ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout) + IdeModeSocket String | + ||| Run as a checker for the core language TTImp + Yaffle String | + ||| Dump metadata from a .ttm file + Metadata String | + ||| Dump cases before compiling + DumpCases String | + ||| Dump lambda lifted defs before compiling + DumpLifted String | + ||| Dump ANF defs before compiling + DumpANF String | + ||| Dump VM code defs before compiling + DumpVMCode String | + ||| Run a REPL command then exit immediately + RunREPL String | + FindIPKG | + Timing | + DebugElabCheck | + BlodwenPaths + + +ActType : List String -> Type +ActType [] = List CLOpt +ActType (a :: as) = String -> ActType as + +record OptDesc where + constructor MkOpt + flags : List String + argdescs : List String + action : ActType argdescs + help : Maybe String + +options : List OptDesc +options = [MkOpt ["--check", "-c"] [] [CheckOnly] + (Just "Exit after checking source file"), + MkOpt ["--output", "-o"] ["file"] (\f => [OutputFile f, Quiet]) + (Just "Specify output file"), + MkOpt ["--exec", "-x"] ["name"] (\f => [ExecFn f, Quiet]) + (Just "Execute function after checking source file"), + MkOpt ["--no-prelude"] [] [NoPrelude] + (Just "Don't implicitly import Prelude"), + MkOpt ["--codegen", "--cg"] ["backend"] (\f => [SetCG f]) + (Just "Set code generator (default chez)"), + MkOpt ["--package", "-p"] ["package"] (\f => [PkgPath f]) + (Just "Add a package as a dependency"), + + MkOpt ["--ide-mode"] [] [IdeMode] + (Just "Run the REPL with machine-readable syntax"), + + MkOpt ["--ide-mode-socket"] [] [IdeModeSocket "localhost:38398"] + (Just "Run the ide socket mode on default host and port (localhost:38398)"), + + MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp]) + (Just "Run the ide socket mode on given host and port"), + + MkOpt ["--prefix"] [] [ShowPrefix] + (Just "Show installation prefix"), + MkOpt ["--paths"] [] [BlodwenPaths] + (Just "Show paths"), + MkOpt ["--build"] ["package file"] (\f => [Package Build f]) + (Just "Build modules/executable for the given package"), + MkOpt ["--install"] ["package file"] (\f => [Package Install f]) + (Just "Install the given package"), + MkOpt ["--clean"] ["package file"] (\f => [Package Clean f]) + (Just "Clean intermediate files/executables for the given package"), + + MkOpt ["--libdir"] [] [Directory LibDir] + (Just "Show library directory"), + MkOpt ["--no-banner"] [] [NoBanner] + (Just "Suppress the banner"), + MkOpt ["--quiet", "-q"] [] [Quiet] + (Just "Quiet mode; display fewer messages"), + MkOpt ["--verbose"] [] [Verbose] + (Just "Verbose mode (default)"), + MkOpt ["--version", "-v"] [] [Version] + (Just "Display version string"), + MkOpt ["--help", "-h", "-?"] [] [Help] + (Just "Display help text"), + MkOpt ["--timing"] [] [Timing] + (Just "Display timing logs"), + MkOpt ["--find-ipkg"] [] [FindIPKG] + (Just "Find and use an .ipkg file in a parent directory"), + MkOpt ["--client"] ["REPL command"] (\f => [RunREPL f]) + (Just "Run a REPL command then quit immediately"), + -- Internal debugging options + MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f]) + Nothing, -- run ttimp REPL rather than full Idris + MkOpt ["--ttm" ] ["ttimp file"] (\f => [Metadata f]) + Nothing, -- dump metadata information from the given ttm file + MkOpt ["--dumpcases"] ["output file"] (\f => [DumpCases f]) + Nothing, -- dump case trees to the given file + MkOpt ["--dumplifted"] ["output file"] (\f => [DumpLifted f]) + Nothing, -- dump lambda lifted trees to the given file + MkOpt ["--dumpanf"] ["output file"] (\f => [DumpANF f]) + Nothing, -- dump ANF to the given file + MkOpt ["--dumpvmcode"] ["output file"] (\f => [DumpVMCode f]) + Nothing, -- dump VM Code to the given file + MkOpt ["--debug-elab-check"] [] [DebugElabCheck] + Nothing -- do more elaborator checks (currently conversion in LinearCheck) + ] + +optUsage : OptDesc -> String +optUsage d + = maybe "" -- Don't show anything if there's no help string (that means + -- it's an internal option) + (\h => " " ++ + let optshow = showSep "," (flags d) ++ " " ++ + showSep " " (map (\x => "<" ++ x ++ ">") (argdescs d)) in + optshow ++ pack (List.replicate (minus 26 (length optshow)) ' ') + ++ h ++ "\n") (help d) + where + showSep : String -> List String -> String + showSep sep [] = "" + showSep sep [x] = x + showSep sep (x :: xs) = x ++ sep ++ showSep sep xs + +export +versionMsg : String +versionMsg = "Idris 2, version " ++ showVersion True version + +export +usage : String +usage = versionMsg ++ "\n" ++ + "Usage: idris2 [options] [input file]\n\n" ++ + "Available options:\n" ++ + concatMap optUsage options + +processArgs : String -> (args : List String) -> List String -> ActType args -> + Either String (List CLOpt, List String) +processArgs flag [] xs f = Right (f, xs) +processArgs flag (a :: as) [] f + = Left $ "Missing argument <" ++ a ++ "> for flag " ++ flag +processArgs flag (a :: as) (x :: xs) f + = processArgs flag as xs (f x) + +matchFlag : (d : OptDesc) -> List String -> + Either String (Maybe (List CLOpt, List String)) +matchFlag d [] = Right Nothing -- Nothing left to match +matchFlag d (x :: xs) + = if x `elem` flags d + then do args <- processArgs x (argdescs d) xs (action d) + Right (Just args) + else Right Nothing + +findMatch : List OptDesc -> List String -> + Either String (List CLOpt, List String) +findMatch [] [] = Right ([], []) +findMatch [] (f :: args) = Right ([InputFile f], args) +findMatch (d :: ds) args + = case !(matchFlag d args) of + Nothing => findMatch ds args + Just res => Right res + +parseOpts : List OptDesc -> List String -> Either String (List CLOpt) +parseOpts opts [] = Right [] +parseOpts opts args + = do (cl, rest) <- findMatch opts args + cls <- assert_total (parseOpts opts rest) -- 'rest' smaller than 'args' + pure (cl ++ cls) + +export +getOpts : List String -> Either String (List CLOpt) +getOpts opts = parseOpts options opts + + +export covering +getCmdOpts : IO (Either String (List CLOpt)) +getCmdOpts = do (_ :: opts) <- getArgs + | _ => pure (Left "Invalid command line") + pure $ getOpts opts + +portPart : String -> Maybe String +portPart p = if p == "" + then Nothing + else Just $ assert_total $ prim__strTail p + +||| Extract the host and port to bind the IDE socket to +public export +ideSocketModeHostPort : List CLOpt -> (String, Int) +ideSocketModeHostPort [] = ("localhost", 38398) +ideSocketModeHostPort (IdeModeSocket hp :: _) = + let (h, p) = Strings.break (== ':') hp + port = fromMaybe 38398 (portPart p >>= parsePositive) + host = if h == "" then "localhost" else h + in (host, port) +ideSocketModeHostPort (_ :: rest) = ideSocketModeHostPort rest diff --git a/src/Idris/IDEMode/CaseSplit.idr b/src/Idris/IDEMode/CaseSplit.idr new file mode 100644 index 000000000..abbed9d36 --- /dev/null +++ b/src/Idris/IDEMode/CaseSplit.idr @@ -0,0 +1,190 @@ +module Idris.IDEMode.CaseSplit + +import Core.Context +import Core.Env +import Core.Metadata +import Core.TT +import Core.Value + +import Parser.Lexer +import Parser.Unlit + +import TTImp.Interactive.CaseSplit +import TTImp.TTImp +import TTImp.Utils + +import Idris.IDEMode.TokenLine +import Idris.REPLOpts +import Idris.Resugar +import Idris.Syntax + +import Data.List +import Data.Strings +import System.File + +%default covering + +getLine : Nat -> List String -> Maybe String +getLine Z (l :: ls) = Just l +getLine (S k) (l :: ls) = getLine k ls +getLine _ [] = Nothing + +toStrUpdate : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + (Name, RawImp) -> Core (List (String, String)) +toStrUpdate (UN n, term) + = do clause <- pterm term + pure [(n, show (bracket clause))] + where + bracket : PTerm -> PTerm + bracket tm@(PRef _ _) = tm + bracket tm@(PList _ _) = tm + bracket tm@(PPair _ _ _) = tm + bracket tm@(PUnit _) = tm + bracket tm@(PComprehension _ _ _) = tm + bracket tm@(PPrimVal _ _) = tm + bracket tm = PBracketed emptyFC tm +toStrUpdate _ = pure [] -- can't replace non user names + +dump : SourcePart -> String +dump (Whitespace str) = str +dump (Name n) = n +dump (HoleName n) = "?" ++ n +dump LBrace = "{" +dump RBrace = "}" +dump Equal = "=" +dump (Other str) = str + +data UPD : Type where + +doUpdates : {auto u : Ref UPD (List String)} -> + Defs -> List (String, String) -> List SourcePart -> + Core (List SourcePart) +doUpdates defs ups [] = pure [] +doUpdates defs ups (LBrace :: xs) + = case dropSpace xs of + Name n :: RBrace :: rest => + pure (LBrace :: Name n :: + Whitespace " " :: Equal :: Whitespace " " :: + !(doUpdates defs ups (Name n :: RBrace :: rest))) + Name n :: Equal :: rest => + pure (LBrace :: Name n :: + Whitespace " " :: Equal :: Whitespace " " :: + !(doUpdates defs ups rest)) + _ => pure (LBrace :: !(doUpdates defs ups xs)) + where + dropSpace : List SourcePart -> List SourcePart + dropSpace [] = [] + dropSpace (RBrace :: xs) = RBrace :: xs + dropSpace (Whitespace _ :: xs) = dropSpace xs + dropSpace (x :: xs) = x :: dropSpace xs +doUpdates defs ups (Name n :: xs) + = case lookup n ups of + Nothing => pure (Name n :: !(doUpdates defs ups xs)) + Just up => pure (Other up :: !(doUpdates defs ups xs)) +doUpdates defs ups (HoleName n :: xs) + = do used <- get UPD + n' <- uniqueName defs used n + put UPD (n' :: used) + pure $ HoleName n' :: !(doUpdates defs ups xs) +doUpdates defs ups (x :: xs) + = pure $ x :: !(doUpdates defs ups xs) + +-- State here is a list of new hole names we generated (so as not to reuse any). +-- Update the token list with the string replacements for each match, and return +-- the newly generated strings. +updateAll : {auto u : Ref UPD (List String)} -> + Defs -> List SourcePart -> List (List (String, String)) -> + Core (List String) +updateAll defs l [] = pure [] +updateAll defs l (rs :: rss) + = do l' <- doUpdates defs rs l + rss' <- updateAll defs l rss + pure (concat (map dump l') :: rss') + +-- Turn the replacements we got from 'getSplits' into a list of actual string +-- replacements +getReplaces : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + List (Name, RawImp) -> Core (List (String, String)) +getReplaces updates + = do strups <- traverse toStrUpdate updates + pure (concat strups) + +showImpossible : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + RawImp -> Core String +showImpossible lhs + = do clause <- pterm lhs + pure (show clause ++ " impossible") + +-- Given a list of updates and a line and column, find the relevant line in +-- the source file and return the lines to replace it with +export +updateCase : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + List ClauseUpdate -> Int -> Int -> + Core (List String) +updateCase splits line col + = do opts <- get ROpts + case mainfile opts of + Nothing => throw (InternalError "No file loaded") + Just f => + do Right file <- coreLift $ readFile f + | Left err => throw (FileErr f err) + let thisline = getLine (integerToNat (cast line)) (lines file) + case thisline of + Nothing => throw (InternalError "File too short!") + Just l => + do let valid = mapMaybe getValid splits + let bad = mapMaybe getBad splits + if isNil valid + then traverse showImpossible bad + else do rs <- traverse getReplaces valid + let stok = tokens l + defs <- get Ctxt + u <- newRef UPD (the (List String) []) + updateAll defs stok rs + where + getValid : ClauseUpdate -> Maybe (List (Name, RawImp)) + getValid (Valid _ ups) = Just ups + getValid _ = Nothing + + getBad : ClauseUpdate -> Maybe RawImp + getBad (Impossible lhs) = Just lhs + getBad _ = Nothing + +fnName : Bool -> Name -> String +fnName lhs (UN n) + = if isIdentNormal n then n + else if lhs then "(" ++ n ++ ")" + else "op" +fnName lhs (NS _ n) = fnName lhs n +fnName lhs (DN s _) = s +fnName lhs n = show n + + +export +getClause : {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + Int -> Name -> Core (Maybe String) +getClause l n + = do defs <- get Ctxt + Just (loc, nidx, envlen, ty) <- findTyDeclAt (\p, n => onLine (l-1) p) + | Nothing => pure Nothing + n <- getFullName nidx + argns <- getEnvArgNames defs envlen !(nf defs [] ty) + Just srcLine <- getSourceLine l + | Nothing => pure Nothing + let (mark, src) = isLitLine srcLine + pure (Just (indent mark loc ++ fnName True n ++ concat (map (" " ++) argns) ++ + " = ?" ++ fnName False n ++ "_rhs")) + where + indent : Maybe String -> FC -> String + indent (Just mark) fc + = relit (Just mark) $ pack (replicate (integerToNat (cast (max 0 (snd (startPos fc) - 1)))) ' ') + indent Nothing fc = pack (replicate (integerToNat (cast (snd (startPos fc)))) ' ') diff --git a/src/Idris/IDEMode/MakeClause.idr b/src/Idris/IDEMode/MakeClause.idr new file mode 100644 index 000000000..a5f9ed223 --- /dev/null +++ b/src/Idris/IDEMode/MakeClause.idr @@ -0,0 +1,52 @@ +module Idris.IDEMode.MakeClause + +import Core.Name +import Parser.Lexer +import Parser.Unlit + +import Data.List +import Data.Nat +import Data.Strings + +-- Implement make-with and make-case from the IDE mode + +showRHSName : Name -> String +showRHSName n + = let fn = show (dropNS n) in + if any isOpChar (unpack fn) + then "op" + else fn + +export +makeWith : Name -> String -> String +makeWith n srcline + = let (markerM, src) = isLitLine srcline + isrc : (Nat, String) = + case span isSpace src of + (spc, rest) => (length spc, rest) + indent = fst isrc + src = snd isrc + lhs = pack (readLHS 0 (unpack src)) in + mkWithArg markerM indent lhs ++ "\n" ++ + mkWithPat markerM indent lhs ++ "\n" + where + readLHS : (brackets : Nat) -> List Char -> List Char + readLHS Z ('=' :: rest) = [] + readLHS n ('(' :: rest) = '(' :: readLHS (S n) rest + readLHS n ('{' :: rest) = '{' :: readLHS (S n) rest + readLHS n (')' :: rest) = ')' :: readLHS (pred n) rest + readLHS n ('}' :: rest) = '}' :: readLHS (pred n) rest + readLHS n (x :: rest) = x :: readLHS n rest + readLHS n [] = [] + + pref : Maybe String -> Nat -> String + pref mark ind = relit mark $ pack (replicate ind ' ') + + mkWithArg : Maybe String -> Nat -> String -> String + mkWithArg mark indent lhs + = pref mark indent ++ lhs ++ "with (_)" + + mkWithPat : Maybe String -> Nat -> String -> String + mkWithPat mark indent lhs + = pref mark (indent + 2) ++ lhs ++ "| with_pat = ?" ++ + showRHSName n ++ "_rhs" diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr new file mode 100644 index 000000000..d619fdec1 --- /dev/null +++ b/src/Idris/IDEMode/Parser.idr @@ -0,0 +1,79 @@ +||| Slightly different lexer than the source language because we are more free +||| as to what can be identifiers, and fewer tokens are supported. But otherwise, +||| we can reuse the standard stuff +module Idris.IDEMode.Parser + +import Idris.IDEMode.Commands + +import Text.Parser +import Parser.Lexer +import Parser.Support +import Text.Lexer +import Utils.String + +import Data.List +import Data.Strings + +%hide Text.Lexer.symbols +%hide Parser.Lexer.symbols + +symbols : List String +symbols = ["(", ":", ")"] + +ideTokens : TokenMap Token +ideTokens = + map (\x => (exact x, Symbol)) symbols ++ + [(digits, \x => Literal (cast x)), + (stringLit, \x => StrLit (stripQuotes x)), + (identAllowDashes, \x => NSIdent [x]), + (space, Comment)] + +idelex : String -> Either (Int, Int, String) (List (TokenData Token)) +idelex str + = case lex ideTokens str of + -- Add the EndInput token so that we'll have a line and column + -- number to read when storing spans in the file + (tok, (l, c, "")) => Right (filter notComment tok ++ + [MkToken l c EndInput]) + (_, fail) => Left fail + where + notComment : TokenData Token -> Bool + notComment t = case tok t of + Comment _ => False + _ => True + +sexp : Rule SExp +sexp + = do symbol ":"; exactIdent "True" + pure (BoolAtom True) + <|> do symbol ":"; exactIdent "False" + pure (BoolAtom False) + <|> do i <- intLit + pure (IntegerAtom i) + <|> do str <- strLit + pure (StringAtom str) + <|> do symbol ":"; x <- unqualifiedName + pure (SymbolAtom x) + <|> do symbol "(" + xs <- many sexp + symbol ")" + pure (SExpList xs) + +ideParser : {e : _} -> + String -> Grammar (TokenData Token) e ty -> Either ParseError ty +ideParser str p + = case idelex str of + Left err => Left $ LexFail err + Right toks => + case parse p toks of + Left (Error err []) => + Left $ ParseFail err Nothing [] + Left (Error err (t :: ts)) => + Left $ ParseFail err (Just (line t, col t)) + (map tok (t :: ts)) + Right (val, _) => Right val + +export +parseSExp : String -> Either ParseError SExp +parseSExp inp + = ideParser inp (do c <- sexp; eoi; pure c) diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr new file mode 100644 index 000000000..fc29ba7d7 --- /dev/null +++ b/src/Idris/IDEMode/REPL.idr @@ -0,0 +1,325 @@ +module Idris.IDEMode.REPL + +import Compiler.Scheme.Chez +import Compiler.Scheme.Racket +import Compiler.Scheme.Gambit +import Compiler.Common + +import Core.AutoSearch +import Core.CompileExpr +import Core.Context +import Core.InitPrimitives +import Core.Metadata +import Core.Normalise +import Core.Options +import Core.TT +import Core.Unify + +import Idris.Desugar +import Idris.Error +import Idris.ModTree +import Idris.Parser +import Idris.Resugar +import Idris.REPL +import Idris.Syntax +import Idris.Version + +import Idris.IDEMode.Parser +import Idris.IDEMode.Commands +import Idris.IDEMode.SyntaxHighlight + +import TTImp.Interactive.CaseSplit +import TTImp.Elab +import TTImp.TTImp +import TTImp.ProcessDecls + +import Utils.Hex + +import System + +-- import Idris.Socket +-- import Idris.Socket.Data + +{- +export +socketToFile : Socket -> IO (Either String File) +socketToFile (MkSocket f _ _ _) = do + file <- map FHandle $ foreign FFI_C "fdopen" (Int -> String -> IO Ptr) f "r+" + if !(ferror file) then do + pure (Left "Failed to fdopen socket file descriptor") + else pure (Right file) + +export +initIDESocketFile : String -> Int -> IO (Either String File) +initIDESocketFile h p = do + osock <- socket AF_INET Stream 0 + case osock of + Left fail => do + putStrLn (show fail) + putStrLn "Failed to open socket" + exit 1 + Right sock => do + res <- bind sock (Just (Hostname h)) p + if res /= 0 + then + pure (Left ("Failed to bind socket with error: " ++ show res)) + else do + res <- listen sock + if res /= 0 + then + pure (Left ("Failed to listen on socket with error: " ++ show res)) + else do + putStrLn (show p) + res <- accept sock + case res of + Left err => + pure (Left ("Failed to accept on socket with error: " ++ show err)) + Right (s, _) => + socketToFile s + +getChar : File -> IO Char +getChar (FHandle h) = do + if !(fEOF (FHandle h)) then do + putStrLn "Alas the file is done, aborting" + exit 1 + else do + chr <- map cast $ foreign FFI_C "fgetc" (Ptr -> IO Int) h + if !(ferror (FHandle h)) then do + putStrLn "Failed to read a character" + exit 1 + else pure chr + +getFLine : File -> IO String +getFLine (FHandle h) = do + str <- prim_fread h + if !(ferror (FHandle h)) then do + putStrLn "Failed to read a line" + exit 1 + else pure str + +getNChars : File -> Nat -> IO (List Char) +getNChars i Z = pure [] +getNChars i (S k) + = do x <- getChar i + xs <- getNChars i k + pure (x :: xs) + +-- Read 6 characters. If they're a hex number, read that many characters. +-- Otherwise, just read to newline +getInput : File -> IO String +getInput f + = do x <- getNChars f 6 + case fromHexChars (reverse x) of + Nothing => + do rest <- getFLine f + pure (pack x ++ rest) + Just num => + do inp <- getNChars f (cast num) + pure (pack inp) + + +process : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + IDECommand -> Core REPLResult +process (Interpret cmd) + = interpret cmd +process (LoadFile fname _) + = Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname +process (TypeOf n Nothing) + = Idris.REPL.process (Check (PRef replFC (UN n))) +process (TypeOf n (Just (l, c))) + = Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n))) +process (CaseSplit l c n) + = Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n))) +process (AddClause l n) + = Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n))) +process (ExprSearch l n hs all) + = Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) + (map UN hs) all)) +process (GenerateDef l n) + = Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n))) +process (MakeLemma l n) + = Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n))) +process (MakeCase l n) + = Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n))) +process (MakeWith l n) + = Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n))) +process Version + = Idris.REPL.process ShowVersion +process (Metavariables _) + = Idris.REPL.process Metavars +process GetOptions + = Idris.REPL.process GetOpts + +processCatch : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + IDECommand -> Core REPLResult +processCatch cmd + = do c' <- branch + u' <- get UST + s' <- get Syn + o' <- get ROpts + catch (do res <- process cmd + commit + pure res) + (\err => do put Ctxt c' + put UST u' + put Syn s' + put ROpts o' + msg <- perror err + pure $ REPLError msg) + +idePutStrLn : File -> Integer -> String -> Core () +idePutStrLn outf i msg + = send outf (SExpList [SymbolAtom "write-string", + toSExp msg, toSExp i]) + +returnFromIDE : File -> Integer -> SExp -> Core () +returnFromIDE outf i msg + = do send outf (SExpList [SymbolAtom "return", msg, toSExp i]) + +printIDEResult : File -> Integer -> SExp -> Core () +printIDEResult outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg]) + +printIDEResultWithHighlight : File -> Integer -> SExp -> Core () +printIDEResultWithHighlight outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg + -- TODO return syntax highlighted result + , SExpList []]) + +printIDEError : File -> Integer -> String -> Core () +printIDEError outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "error", toSExp msg ]) + +SExpable REPLEval where + toSExp EvalTC = SymbolAtom "typecheck" + toSExp NormaliseAll = SymbolAtom "normalise" + toSExp Execute = SymbolAtom "execute" + +SExpable REPLOpt where + toSExp (ShowImplicits impl) = SExpList [ SymbolAtom "show-implicits", toSExp impl ] + toSExp (ShowNamespace ns) = SExpList [ SymbolAtom "show-namespace", toSExp ns ] + toSExp (ShowTypes typs) = SExpList [ SymbolAtom "show-types", toSExp typs ] + toSExp (EvalMode mod) = SExpList [ SymbolAtom "eval", toSExp mod ] + toSExp (Editor editor) = SExpList [ SymbolAtom "editor", toSExp editor ] + toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ] + + +sexpName : Name -> SExp +sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [] ] + +displayIDEResult : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + File -> Integer -> REPLResult -> Core () +displayIDEResult outf i (REPLError err) = printIDEError outf i err +displayIDEResult outf i (Evaluated x Nothing) = printIDEResultWithHighlight outf i $ StringAtom $ show x +displayIDEResult outf i (Evaluated x (Just y)) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y +displayIDEResult outf i (Printed xs) = printIDEResultWithHighlight outf i $ StringAtom $ showSep "\n" xs +displayIDEResult outf i (TermChecked x y) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y +displayIDEResult outf i (FileLoaded x) = printIDEResult outf i $ SExpList [] +displayIDEResult outf i (ErrorLoadingFile x err) = printIDEError outf i $ "Error loading file " ++ x ++ ": " ++ show err +displayIDEResult outf i (ErrorsBuildingFile x errs) = printIDEError outf i $ "Error(s) building file " ++ x ++ ": " ++ (showSep "\n" $ map show errs) +displayIDEResult outf i NoFileLoaded = printIDEError outf i "No file can be reloaded" +displayIDEResult outf i (CurrentDirectory dir) = printIDEResult outf i $ StringAtom $ "Current working directory is '" ++ dir ++ "'" +displayIDEResult outf i CompilationFailed = printIDEError outf i "Compilation failed" +displayIDEResult outf i (Compiled f) = printIDEResult outf i $ StringAtom $ "File " ++ f ++ " written" +displayIDEResult outf i (ProofFound x) = printIDEResult outf i $ StringAtom $ show x +--displayIDEResult outf i (Missed cases) = printIDEResult outf i $ showSep "\n" $ map handleMissing cases +displayIDEResult outf i (CheckedTotal xs) = printIDEResult outf i $ StringAtom $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs +displayIDEResult outf i (FoundHoles []) = printIDEResult outf i $ SExpList [] +displayIDEResult outf i (FoundHoles xs) = printIDEResult outf i $ holesSexp + where + holesSexp : SExp + holesSexp = SExpList $ map sexpName xs + +displayIDEResult outf i (LogLevelSet k) = printIDEResult outf i $ StringAtom $ "Set loglevel to " ++ show k +displayIDEResult outf i (OptionsSet opts) = printIDEResult outf i optionsSexp + where + optionsSexp : SExp + optionsSexp = SExpList $ map toSExp opts +displayIDEResult outf i (VersionIs x) = printIDEResult outf i versionSExp + where + semverSexp : SExp + semverSexp = case (semVer x) of + (maj, min, patch) => SExpList (map toSExp [maj, min, patch]) + tagSexp : SExp + tagSexp = case versionTag x of + Nothing => SExpList [ StringAtom "" ] + Just t => SExpList [ StringAtom t ] + versionSExp : SExp + versionSExp = SExpList [ semverSexp, tagSexp ] + + +displayIDEResult outf i (Edited (DisplayEdit xs)) = printIDEResult outf i $ StringAtom $ showSep "\n" xs +displayIDEResult outf i (Edited (EditError x)) = printIDEError outf i x +displayIDEResult outf i (Edited (MadeLemma lit name pty pappstr)) = + printIDEResult outf i $ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr +displayIDEResult outf i _ = pure () + + +handleIDEResult : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + File -> Integer -> REPLResult -> Core () +handleIDEResult outf i Exited = idePutStrLn outf i "Bye for now!" +handleIDEResult outf i other = displayIDEResult outf i other + +loop : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + Core () +loop + = do res <- getOutput + case res of + REPL _ => printError "Running idemode but output isn't" + IDEMode idx inf outf => do + inp <- coreLift $ getInput inf + end <- coreLift $ fEOF inf + if end then pure () + else case parseSExp inp of + Left err => + do printIDEError outf idx ("Parse error: " ++ show err) + loop + Right sexp => + case getMsg sexp of + Just (cmd, i) => + do updateOutput i + res <- processCatch cmd + handleIDEResult outf i res + loop + Nothing => + do printIDEError outf idx ("Unrecognised command: " ++ show sexp) + loop + where + updateOutput : Integer -> Core () + updateOutput idx + = do IDEMode _ i o <- getOutput + | _ => pure () + setOutput (IDEMode idx i o) + -} + +export +replIDE : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + Core () +replIDE = throw (InternalError "Not implemented yet") +-- = do res <- getOutput +-- case res of +-- REPL _ => printError "Running idemode but output isn't" +-- IDEMode _ inf outf => do +-- send outf (version 2 0) +-- loop diff --git a/src/Idris/IDEMode/SyntaxHighlight.idr b/src/Idris/IDEMode/SyntaxHighlight.idr new file mode 100644 index 000000000..dc04a3a84 --- /dev/null +++ b/src/Idris/IDEMode/SyntaxHighlight.idr @@ -0,0 +1,126 @@ +module Idris.IDEMode.SyntaxHighlight + +import Core.Context +import Core.InitPrimitives +import Core.Metadata +import Core.TT + +import Idris.REPL +import Idris.IDEMode.Commands + +import Data.List + +data Decoration : Type where + Typ : Decoration + Function : Decoration + Data : Decoration + Keyword : Decoration + Bound : Decoration + +SExpable Decoration where + toSExp Typ = SymbolAtom "type" + toSExp Function = SymbolAtom "function" + toSExp Data = SymbolAtom "data" + toSExp Keyword = SymbolAtom "keyword" + toSExp Bound = SymbolAtom "bound" + +record Highlight where + constructor MkHighlight + location : FC + name : Name + isImplicit : Bool + key : String + decor : Decoration + docOverview : String + typ : String + ns : String + +SExpable FC where + toSExp (MkFC fname (startLine, startCol) (endLine, endCol)) + = SExpList [ SExpList [ SymbolAtom "filename", StringAtom fname ] + , SExpList [ SymbolAtom "start", IntegerAtom (cast startLine + 1), IntegerAtom (cast startCol + 1) ] + , SExpList [ SymbolAtom "end", IntegerAtom (cast endLine + 1), IntegerAtom (cast endCol + 1) ] + ] + toSExp EmptyFC = SExpList [] + +SExpable Highlight where + toSExp (MkHighlight loc nam impl k dec doc t ns) + = SExpList [ toSExp loc + , SExpList [ SExpList [ SymbolAtom "name", StringAtom (show nam) ] + , SExpList [ SymbolAtom "namespace", StringAtom ns ] + , SExpList [ SymbolAtom "decor", toSExp dec ] + , SExpList [ SymbolAtom "implicit", toSExp impl ] + , SExpList [ SymbolAtom "key", StringAtom k ] + , SExpList [ SymbolAtom "doc-overview", StringAtom doc ] + , SExpList [ SymbolAtom "type", StringAtom t ] + ] + ] + +inFile : String -> (FC, (Name, Nat, ClosedTerm)) -> Bool +inFile fname (MkFC file _ _, _) = file == fname + +||| Output some data using current dialog index +export +printOutput : {auto o : Ref ROpts REPLOpts} -> + SExp -> Core () +printOutput msg + = do opts <- get ROpts + case idemode opts of + REPL _ => pure () + IDEMode i _ f => + send f (SExpList [SymbolAtom "output", + msg, toSExp i]) + + +outputHighlight : {auto opts : Ref ROpts REPLOpts} -> + Highlight -> Core () +outputHighlight h = + printOutput $ SExpList [ SymbolAtom "ok" + , SExpList [ SymbolAtom "highlight-source" + , toSExp hlt + ] + ] + where + hlt : List Highlight + hlt = [h] + +outputNameSyntax : {auto opts : Ref ROpts REPLOpts} -> + (FC, (Name, Nat, ClosedTerm)) -> Core () +outputNameSyntax (fc, (name, _, term)) = + let dec = case term of + (Local fc x idx y) => Just Bound + + -- See definition of NameType in Core.TT for possible values of Ref's nametype field + -- data NameType : Type where + -- Bound : NameType + -- Func : NameType + -- DataCon : (tag : Int) -> (arity : Nat) -> NameType + -- TyCon : (tag : Int) -> (arity : Nat) -> NameType + (Ref fc Bound name) => Just Bound + (Ref fc Func name) => Just Function + (Ref fc (DataCon tag arity) name) => Just Data + (Ref fc (TyCon tag arity) name) => Just Typ + (Meta fc x y xs) => Just Bound + (Bind fc x b scope) => Just Bound + (App fc fn arg) => Just Bound + (As fc x as pat) => Just Bound + (TDelayed fc x y) => Nothing + (TDelay fc x ty arg) => Nothing + (TForce fc x y) => Nothing + (PrimVal fc c) => Just Typ + (Erased fc imp) => Just Bound + (TType fc) => Just Typ + hilite = Prelude.map (\ d => MkHighlight fc name False "" d "" (show term) "") dec + in maybe (pure ()) outputHighlight hilite + +export +outputSyntaxHighlighting : {auto m : Ref MD Metadata} -> + {auto opts : Ref ROpts REPLOpts} -> + String -> + REPLResult -> + Core REPLResult +outputSyntaxHighlighting fname loadResult = do + allNames <- filter (inFile fname) . names <$> get MD +-- decls <- filter (inFile fname) . tydecls <$> get MD + _ <- traverse outputNameSyntax allNames -- ++ decls) + pure loadResult diff --git a/src/Idris/IDEMode/TokenLine.idr b/src/Idris/IDEMode/TokenLine.idr new file mode 100644 index 000000000..8475635a4 --- /dev/null +++ b/src/Idris/IDEMode/TokenLine.idr @@ -0,0 +1,37 @@ +||| Tokenise a source line for easier processing +module Idris.IDEMode.TokenLine + +import Parser.Lexer +import Text.Lexer + +public export +data SourcePart + = Whitespace String + | Name String + | HoleName String + | LBrace + | RBrace + | Equal + | Other String + +holeIdent : Lexer +holeIdent = is '?' <+> identNormal + +srcTokens : TokenMap SourcePart +srcTokens = + [(identNormal, Name), + (holeIdent, \x => HoleName (assert_total (prim__strTail x))), + (space, Whitespace), + (is '{', const LBrace), + (is '}', const RBrace), + (is '=', const Equal), + (any, Other)] + +export +tokens : String -> List SourcePart +tokens str + = case lex srcTokens str of + -- Add the EndInput token so that we'll have a line and column + -- number to read when storing spans in the file + (srctoks, (l, c, rest)) => + map tok srctoks ++ (if rest == "" then [] else [Other rest]) diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr new file mode 100644 index 000000000..30284abcb --- /dev/null +++ b/src/Idris/Main.idr @@ -0,0 +1,233 @@ +module Main + +import Core.Binary +import Core.Context +import Core.Core +import Core.Directory +import Core.InitPrimitives +import Core.Metadata +import Core.Options +import Core.Unify + +import Idris.CommandLine +import Idris.Desugar +import Idris.IDEMode.REPL +import Idris.ModTree +import Idris.Package +import Idris.Parser +import Idris.ProcessIdr +import Idris.REPL +import Idris.SetOptions +import Idris.Syntax +import Idris.Version + +import Data.List +import Data.Strings +import Data.Vect +import System + +import Yaffle.Main + +import IdrisPaths + +%default covering + +yprefix : String +yprefix = "/home/edwin/.idris2" -- TODO! unsafePerformIO (foreign FFI_C "getIdris2_prefix" (IO String)) + +findInput : List CLOpt -> Maybe String +findInput [] = Nothing +findInput (InputFile f :: fs) = Just f +findInput (_ :: fs) = findInput fs + +-- Add extra library directories from the "BLODWEN_PATH" +-- environment variable +updatePaths : {auto c : Ref Ctxt Defs} -> + Core () +updatePaths + = do bprefix <- coreLift $ getEnv "IDRIS2_PREFIX" + the (Core ()) $ case bprefix of + Just p => setPrefix p + Nothing => setPrefix yprefix + bpath <- coreLift $ getEnv "IDRIS2_PATH" + the (Core ()) $ case bpath of + Just path => do traverse_ addExtraDir (map trim (split (==pathSep) path)) + Nothing => pure () + bdata <- coreLift $ getEnv "IDRIS2_DATA" + the (Core ()) $ case bdata of + Just path => do traverse_ addDataDir (map trim (split (==pathSep) path)) + Nothing => pure () + blibs <- coreLift $ getEnv "IDRIS2_LIBS" + the (Core ()) $ case blibs of + Just path => do traverse_ addLibDir (map trim (split (==pathSep) path)) + 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 + -- version + defs <- get Ctxt + addPkgDir "prelude" + addPkgDir "base" + addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++ + "idris2-" ++ showVersion False version ++ dirSep ++ "support") + addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++ + "idris2-" ++ showVersion False version ++ dirSep ++ "lib") + Just cwd <- coreLift $ currentDir + | Nothing => throw (InternalError "Can't get current directory") + addLibDir cwd + +updateREPLOpts : {auto o : Ref ROpts REPLOpts} -> + Core () +updateREPLOpts + = do opts <- get ROpts + ed <- coreLift $ getEnv "EDITOR" + case ed of + Just e => put ROpts (record { editor = e } opts) + Nothing => pure () + +showInfo : {auto c : Ref Ctxt Defs} + -> {auto o : Ref ROpts REPLOpts} + -> List CLOpt + -> Core Bool +showInfo Nil = pure False +showInfo (BlodwenPaths :: _) + = do defs <- get Ctxt + iputStrLn (toString (dirs (options defs))) + pure True +showInfo (_::rest) = showInfo rest + +tryYaffle : List CLOpt -> Core Bool +tryYaffle [] = pure False +tryYaffle (Yaffle f :: _) = do yaffleMain f [] + pure True +tryYaffle (c :: cs) = tryYaffle cs + +tryTTM : List CLOpt -> Core Bool +tryTTM [] = pure False +tryTTM (Metadata f :: _) = do dumpTTM f + pure True +tryTTM (c :: cs) = tryTTM cs + + +banner : String +banner = " ____ __ _ ___ \n" ++ + " / _/___/ /____(_)____ |__ \\ \n" ++ + " / // __ / ___/ / ___/ __/ / Version " ++ showVersion True version ++ "\n" ++ + " _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org \n" ++ + " /___/\\__,_/_/ /_/____/ /____/ Type :? for help \n" ++ + "\n" ++ + "Welcome to Idris 2. Enjoy yourself!" + +checkVerbose : List CLOpt -> Bool +checkVerbose [] = False +checkVerbose (Verbose :: _) = True +checkVerbose (_ :: xs) = checkVerbose xs + +stMain : List CLOpt -> Core () +stMain opts + = do False <- tryYaffle opts + | True => pure () + False <- tryTTM opts + | True => pure () + defs <- initDefs + c <- newRef Ctxt defs + s <- newRef Syn initSyntax + m <- newRef MD initMetadata + addPrimitives + + setWorkingDir "." + updatePaths + let ide = ideMode opts + let ideSocket = ideModeSocket opts + let outmode = if ide then IDEMode 0 stdin stdout else REPL False + let fname = findInput opts + o <- newRef ROpts (REPLOpts.defaultOpts fname outmode) + + finish <- showInfo opts + if finish + then pure () + else do + + -- If there's a --build or --install, just do that then quit + done <- processPackageOpts opts + + when (not done) $ + do True <- preOptions opts + | False => pure () + + when (checkVerbose opts) $ -- override Quiet if implicitly set + setOutput (REPL False) + u <- newRef UST initUState + updateREPLOpts + session <- getSession + when (not $ nobanner session) $ + iputStrLn banner + fname <- if findipkg session + then findIpkg fname + else pure fname + the (Core ()) $ case fname of + Nothing => logTime "Loading prelude" $ + when (not $ noprelude session) $ + readPrelude + Just f => logTime "Loading main file" $ + (loadMainFile f >>= displayErrors) + + doRepl <- postOptions opts + if doRepl then + if ide || ideSocket then + if not ideSocket + then do + setOutput (IDEMode 0 stdin stdout) + replIDE {c} {u} {m} + else do + throw (InternalError "Not implemeted yet") +-- let (host, port) = ideSocketModeHostPort opts +-- f <- coreLift $ initIDESocketFile host port +-- case f of +-- Left err => do +-- coreLift $ putStrLn err +-- coreLift $ exit 1 +-- Right file => do +-- setOutput (IDEMode 0 file file) +-- replIDE {c} {u} {m} + else do + repl {c} {u} {m} + showTimeRecord + else + -- exit with an error code if there was an error, otherwise + -- just exit + do ropts <- get ROpts + showTimeRecord + case errorLine ropts of + Nothing => pure () + Just _ => coreLift $ exitWith (ExitFailure 1) + +-- Run any options (such as --version or --help) which imply printing a +-- message then exiting. Returns wheter the program should continue +quitOpts : List CLOpt -> IO Bool +quitOpts [] = pure True +quitOpts (Version :: _) + = do putStrLn versionMsg + pure False +quitOpts (Help :: _) + = do putStrLn usage + pure False +quitOpts (ShowPrefix :: _) + = do putStrLn yprefix + pure False +quitOpts (_ :: opts) = quitOpts opts + +main : IO () +main = do Right opts <- getCmdOpts + | Left err => + do putStrLn err + putStrLn usage + continue <- quitOpts opts + if continue + then + coreRun (stMain opts) + (\err : Error => + do putStrLn ("Uncaught error: " ++ show err) + exitWith (ExitFailure 1)) + (\res => pure ()) + else pure () diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr new file mode 100644 index 000000000..9f19d0dcc --- /dev/null +++ b/src/Idris/Package.idr @@ -0,0 +1,512 @@ +module Idris.Package + +import Compiler.Common + +import Core.Context +import Core.Core +import Core.Directory +import Core.Metadata +import Core.Options +import Core.Unify + +import Data.List +import Data.StringMap +import Data.Strings +import Data.StringTrie +import Data.These + +import Idris.CommandLine +import Idris.ModTree +import Idris.ProcessIdr +import Idris.REPL +import Idris.REPLOpts +import Idris.SetOptions +import Idris.Syntax +import Idris.Version +import Parser.Lexer +import Parser.Support +import Utils.Binary + +import System +import Text.Parser + +import IdrisPaths + +%default covering + +record PkgDesc where + constructor MkPkgDesc + name : String + version : String + authors : String + maintainers : Maybe String + license : Maybe String + brief : Maybe String + readme : Maybe String + homepage : Maybe String + sourceloc : Maybe String + bugtracker : Maybe String + depends : List String -- packages to add to search path + modules : List (List String, String) -- modules to install (namespace, filename) + mainmod : Maybe (List String, String) -- main file (i.e. file to load at REPL) + executable : Maybe String -- name of executable + options : Maybe (FC, String) + sourcedir : Maybe String + prebuild : Maybe (FC, String) -- Script to run before building + postbuild : Maybe (FC, String) -- Script to run after building + preinstall : Maybe (FC, String) -- Script to run after building, before installing + postinstall : Maybe (FC, String) -- Script to run after installing + preclean : Maybe (FC, String) -- Script to run before cleaning + postclean : Maybe (FC, String) -- Script to run after cleaning + +Show PkgDesc where + show pkg = "Package: " ++ name pkg ++ "\n" ++ + "Version: " ++ version pkg ++ "\n" ++ + "Authors: " ++ authors pkg ++ "\n" ++ + maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++ + maybe "" (\m => "License: " ++ m ++ "\n") (license pkg) ++ + maybe "" (\m => "Brief: " ++ m ++ "\n") (brief pkg) ++ + maybe "" (\m => "ReadMe: " ++ m ++ "\n") (readme pkg) ++ + maybe "" (\m => "HomePage: " ++ m ++ "\n") (homepage pkg) ++ + maybe "" (\m => "SourceLoc: " ++ m ++ "\n") (sourceloc pkg) ++ + maybe "" (\m => "BugTracker: " ++ m ++ "\n") (bugtracker pkg) ++ + "Depends: " ++ show (depends pkg) ++ "\n" ++ + "Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++ + maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++ + maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++ + maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++ + maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++ + maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++ + maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++ + maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++ + maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++ + maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++ + maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg) + +initPkgDesc : String -> PkgDesc +initPkgDesc pname + = MkPkgDesc pname "0" "Anonymous" Nothing Nothing + Nothing Nothing Nothing Nothing Nothing + [] [] + Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing + Nothing Nothing + +data DescField : Type where + PVersion : FC -> String -> DescField + PAuthors : FC -> String -> DescField + PMaintainers : FC -> String -> DescField + PLicense : FC -> String -> DescField + PBrief : FC -> String -> DescField + PReadMe : FC -> String -> DescField + PHomePage : FC -> String -> DescField + PSourceLoc : FC -> String -> DescField + PBugTracker : FC -> String -> DescField + PDepends : List String -> DescField + PModules : List (FC, List String) -> DescField + PMainMod : FC -> List String -> DescField + PExec : String -> DescField + POpts : FC -> String -> DescField + PSourceDir : FC -> String -> DescField + PPrebuild : FC -> String -> DescField + PPostbuild : FC -> String -> DescField + PPreinstall : FC -> String -> DescField + PPostinstall : FC -> String -> DescField + PPreclean : FC -> String -> DescField + PPostclean : FC -> String -> DescField + +field : String -> Rule DescField +field fname + = strField PVersion "version" + <|> strField PAuthors "authors" + <|> strField PMaintainers "maintainers" + <|> strField PLicense "license" + <|> strField PBrief "brief" + <|> strField PReadMe "readme" + <|> strField PHomePage "homepage" + <|> strField PSourceLoc "sourceloc" + <|> strField PBugTracker "bugtracker" + <|> strField POpts "options" + <|> strField POpts "opts" + <|> strField PSourceDir "sourcedir" + <|> strField PPrebuild "prebuild" + <|> strField PPostbuild "postbuild" + <|> strField PPreinstall "preinstall" + <|> strField PPostinstall "postinstall" + <|> strField PPreclean "preclean" + <|> strField PPostclean "postclean" + <|> do exactIdent "depends"; symbol "=" + ds <- sepBy1 (symbol ",") unqualifiedName + pure (PDepends ds) + <|> do exactIdent "modules"; symbol "=" + ms <- sepBy1 (symbol ",") + (do start <- location + ns <- nsIdent + end <- location + pure (MkFC fname start end, ns)) + pure (PModules ms) + <|> do exactIdent "main"; symbol "=" + start <- location + m <- nsIdent + end <- location + pure (PMainMod (MkFC fname start end) m) + <|> do exactIdent "executable"; symbol "=" + e <- unqualifiedName + pure (PExec e) + where + getStr : (FC -> String -> DescField) -> FC -> + String -> Constant -> EmptyRule DescField + getStr p fc fld (Str s) = pure (p fc s) + getStr p fc fld _ = fail $ fld ++ " field must be a string" + + strField : (FC -> String -> DescField) -> String -> Rule DescField + strField p f + = do start <- location + exactIdent f + symbol "=" + c <- constant + end <- location + getStr p (MkFC fname start end) f c + +parsePkgDesc : String -> Rule (String, List DescField) +parsePkgDesc fname + = do exactIdent "package" + name <- unqualifiedName + fields <- many (field fname) + pure (name, fields) + +data ParsedMods : Type where + +data MainMod : Type where + +addField : {auto c : Ref Ctxt Defs} -> + {auto p : Ref ParsedMods (List (FC, List String))} -> + {auto m : Ref MainMod (Maybe (FC, List String))} -> + DescField -> PkgDesc -> Core PkgDesc +addField (PVersion fc n) pkg = pure $ record { version = n } pkg +addField (PAuthors fc a) pkg = pure $ record { authors = a } pkg +addField (PMaintainers fc a) pkg = pure $ record { maintainers = Just a } pkg +addField (PLicense fc a) pkg = pure $ record { license = Just a } pkg +addField (PBrief fc a) pkg = pure $ record { brief = Just a } pkg +addField (PReadMe fc a) pkg = pure $ record { readme = Just a } pkg +addField (PHomePage fc a) pkg = pure $ record { homepage = Just a } pkg +addField (PSourceLoc fc a) pkg = pure $ record { sourceloc = Just a } pkg +addField (PBugTracker fc a) pkg = pure $ record { bugtracker = Just a } pkg +addField (PDepends ds) pkg = pure $ record { depends = ds } pkg +-- we can't resolve source files for modules without knowing the source directory, +-- so we save them for the second pass +addField (PModules ms) pkg = do put ParsedMods ms + pure pkg +addField (PMainMod loc n) pkg = do put MainMod (Just (loc, n)) + pure pkg +addField (PExec e) pkg = pure $ record { executable = Just e } pkg +addField (POpts fc e) pkg = pure $ record { options = Just (fc, e) } pkg +addField (PSourceDir fc a) pkg = pure $ record { sourcedir = Just a } pkg +addField (PPrebuild fc e) pkg = pure $ record { prebuild = Just (fc, e) } pkg +addField (PPostbuild fc e) pkg = pure $ record { postbuild = Just (fc, e) } pkg +addField (PPreinstall fc e) pkg = pure $ record { preinstall = Just (fc, e) } pkg +addField (PPostinstall fc e) pkg = pure $ record { postinstall = Just (fc, e) } pkg +addField (PPreclean fc e) pkg = pure $ record { preclean = Just (fc, e) } pkg +addField (PPostclean fc e) pkg = pure $ record { postclean = Just (fc, e) } pkg + +addFields : {auto c : Ref Ctxt Defs} -> + List DescField -> PkgDesc -> Core PkgDesc +addFields xs desc = do p <- newRef ParsedMods [] + m <- newRef MainMod Nothing + added <- go {p} {m} xs desc + setSourceDir (sourcedir added) + ms <- get ParsedMods + mmod <- get MainMod + pure $ record { modules = !(traverse toSource ms) + , mainmod = !(traverseOpt toSource mmod) + } added + where + toSource : (FC, List String) -> Core (List String, String) + toSource (loc, ns) = pure (ns, !(nsToSource loc ns)) + go : {auto p : Ref ParsedMods (List (FC, List String))} -> + {auto m : Ref MainMod (Maybe (FC, List String))} -> + List DescField -> PkgDesc -> Core PkgDesc + go [] dsc = pure dsc + go (x :: xs) dsc = go xs !(addField x dsc) + +runScript : Maybe (FC, String) -> Core () +runScript Nothing = pure () +runScript (Just (fc, s)) + = do res <- coreLift $ system s + when (res /= 0) $ + throw (GenericMsg fc "Script failed") + +addDeps : {auto c : Ref Ctxt Defs} -> + PkgDesc -> Core () +addDeps pkg + = do defs <- get Ctxt + traverse_ addPkgDir (depends pkg) + +processOptions : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + Maybe (FC, String) -> Core () +processOptions Nothing = pure () +processOptions (Just (fc, opts)) + = do let Right clopts = getOpts (words opts) + | Left err => throw (GenericMsg fc err) + preOptions clopts + pure () + +compileMain : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + Name -> String -> String -> Core () +compileMain mainn mmod exec + = do m <- newRef MD initMetadata + u <- newRef UST initUState + + loadMainFile mmod + compileExp (PRef replFC mainn) exec + pure () + +build : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + PkgDesc -> Core (List Error) +build pkg + = do defs <- get Ctxt + addDeps pkg + processOptions (options pkg) + runScript (prebuild pkg) + let toBuild = maybe (map snd (modules pkg)) + (\m => snd m :: map snd (modules pkg)) + (mainmod pkg) + [] <- buildAll toBuild + | errs => pure errs + + case executable pkg of + Nothing => pure () + Just exec => + do let Just (mainns, mmod) = mainmod pkg + | Nothing => throw (GenericMsg emptyFC "No main module given") + let mainn = NS ["Main"] (UN "main") + compileMain mainn mmod exec + runScript (postbuild pkg) + pure [] + +copyFile : String -> String -> IO (Either FileError ()) +copyFile src dest + = do Right buf <- readFromFile src + | Left err => pure (Left err) + writeToFile dest buf + +installFrom : {auto c : Ref Ctxt Defs} -> + String -> String -> String -> List String -> Core () +installFrom _ _ _ [] = pure () +installFrom pname builddir destdir ns@(m :: dns) + = do let ttcfile = showSep dirSep (reverse ns) + let ttcPath = builddir ++ dirSep ++ "ttc" ++ dirSep ++ ttcfile ++ ".ttc" + let destPath = destdir ++ dirSep ++ showSep dirSep (reverse dns) + let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc" + Right _ <- coreLift $ mkdirs (reverse dns) + | Left err => throw (FileErr pname err) + coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath + Right _ <- coreLift $ copyFile ttcPath destFile + | Left err => throw (FileErr pname err) + pure () + +-- Install all the built modules in prefix/package/ +-- We've already built and checked for success, so if any don't exist that's +-- an internal error. +install : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + PkgDesc -> Core () +install pkg + = do defs <- get Ctxt + let build = build_dir (dirs (options defs)) + runScript (preinstall pkg) + let toInstall = maybe (map fst (modules pkg)) + (\m => fst m :: map fst (modules pkg)) + (mainmod pkg) + Just srcdir <- coreLift currentDir + | Nothing => throw (InternalError "Can't get current directory") + -- Make the package installation directory + let installPrefix = dir_prefix (dirs (options defs)) ++ + dirSep ++ "idris2-" ++ showVersion False version + True <- coreLift $ changeDir installPrefix + | False => throw (FileErr (name pkg) FileReadError) + Right _ <- coreLift $ mkdirs [name pkg] + | Left err => throw (FileErr (name pkg) err) + True <- coreLift $ changeDir (name pkg) + | False => throw (FileErr (name pkg) FileReadError) + + -- We're in that directory now, so copy the files from + -- srcdir/build into it + traverse (installFrom (name pkg) + (srcdir ++ dirSep ++ build) + (installPrefix ++ dirSep ++ name pkg)) toInstall + coreLift $ changeDir srcdir + runScript (postinstall pkg) + +-- Data.These.bitraverse hand specialised for Core +bitraverseC : (a -> Core c) -> (b -> Core d) -> These a b -> Core (These c d) +bitraverseC f g (This a) = [| This (f a) |] +bitraverseC f g (That b) = [| That (g b) |] +bitraverseC f g (Both a b) = [| Both (f a) (g b) |] + +-- Prelude.Monad.foldlM hand specialised for Core +foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a +foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0) + +-- Data.StringTrie.foldWithKeysM hand specialised for Core +foldWithKeysC : Monoid b => (List String -> Core b) -> (List String -> a -> Core b) -> StringTrie a -> Core b +foldWithKeysC {a} {b} fk fv = go [] + where + go : List String -> StringTrie a -> Core b + go ks (MkStringTrie nd) = + map bifold $ bitraverseC + (fv ks) + (\sm => foldlC + (\x, (k, vs) => + do let ks' = ks++[k] + y <- assert_total $ go ks' vs + z <- fk ks' + pure $ x <+> y <+> z) + neutral + (StringMap.toList sm)) + nd + +Semigroup () where + (<+>) _ _ = () + +Monoid () where + neutral = () + +clean : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + PkgDesc -> Core () +clean pkg + = do defs <- get Ctxt + let build = build_dir (dirs (options defs)) + let exec = exec_dir (dirs (options defs)) + runScript (preclean pkg) + let pkgmods = maybe + (map fst (modules pkg)) + (\m => fst m :: map fst (modules pkg)) + (mainmod pkg) + let toClean : List (List String, String) + = mapMaybe (\ks => case ks of + [] => Nothing + (x :: xs) => Just (xs, x)) pkgmods + Just srcdir <- coreLift currentDir + | Nothing => throw (InternalError "Can't get current directory") + let builddir = srcdir ++ dirSep ++ build ++ dirSep ++ "ttc" + let execdir = srcdir ++ dirSep ++ exec + -- the usual pair syntax breaks with `No such variable a` here for some reason + let pkgTrie = the (StringTrie (List String)) $ + foldl (\trie, ksv => + let ks = Builtin.fst ksv + v = Builtin.snd ksv + in + insertWith (reverse ks) (maybe [v] (v::)) trie) empty toClean + foldWithKeysC (deleteFolder builddir) + (\ks => map concat . traverse (deleteBin builddir ks)) + pkgTrie + deleteFolder builddir [] + maybe (pure ()) (\e => delete (execdir ++ dirSep ++ e)) + (executable pkg) + runScript (postclean pkg) + where + delete : String -> Core () + delete path = do Right () <- coreLift $ fileRemove path + | Left err => throw (FileErr (name pkg) err) + coreLift $ putStrLn $ "Removed: " ++ path + + deleteFolder : String -> List String -> Core () + deleteFolder builddir ns = delete $ builddir ++ dirSep ++ showSep dirSep ns + + deleteBin : String -> List String -> String -> Core () + deleteBin builddir ns mod + = do let ttFile = builddir ++ dirSep ++ showSep dirSep ns ++ dirSep ++ mod + delete $ ttFile ++ ".ttc" + delete $ ttFile ++ ".ttm" + +-- Just load the 'Main' module, if it exists, which will involve building +-- it if necessary +runRepl : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + PkgDesc -> Core () +runRepl pkg + = do addDeps pkg + processOptions (options pkg) + throw (InternalError "Not implemented") + +processPackage : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + PkgCommand -> String -> Core () +processPackage cmd file + = do Right (pname, fs) <- coreLift $ parseFile file + (do desc <- parsePkgDesc file + eoi + pure desc) + | Left err => throw (ParseFail (getParseErrorLoc file err) err) + pkg <- addFields fs (initPkgDesc pname) + case cmd of + Build => do [] <- build pkg + | errs => coreLift (exitWith (ExitFailure 1)) + pure () + Install => do [] <- build pkg + | errs => coreLift (exitWith (ExitFailure 1)) + install pkg + Clean => clean pkg + REPL => runRepl pkg + +rejectPackageOpts : List CLOpt -> Core Bool +rejectPackageOpts (Package cmd f :: _) + = do coreLift $ putStrLn ("Package commands (--build, --install, --clean, --repl) must be the only option given") + pure True -- Done, quit here +rejectPackageOpts (_ :: xs) = rejectPackageOpts xs +rejectPackageOpts [] = pure False + +-- If there's a package option, it must be the only option, so reject if +-- it's not +export +processPackageOpts : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + List CLOpt -> Core Bool +processPackageOpts [Package cmd f] + = do processPackage cmd f + pure True +processPackageOpts opts = rejectPackageOpts opts + +-- find an ipkg file in one of the parent directories +-- If it exists, read it, set the current directory to the root of the source +-- tree, and set the relevant command line options before proceeding +export +findIpkg : {auto c : Ref Ctxt Defs} -> + {auto r : Ref ROpts REPLOpts} -> + Maybe String -> Core (Maybe String) +findIpkg fname + = do Just (dir, ipkgn, up) <- coreLift findIpkgFile + | Nothing => pure fname + coreLift $ changeDir dir + Right (pname, fs) <- coreLift $ parseFile ipkgn + (do desc <- parsePkgDesc ipkgn + eoi + pure desc) + | Left err => throw (ParseFail (getParseErrorLoc ipkgn err) err) + pkg <- addFields fs (initPkgDesc pname) + setSourceDir (sourcedir pkg) + processOptions (options pkg) + loadDependencies (depends pkg) + case fname of + Nothing => pure Nothing + Just src => + do let src' = showSep dirSep (up ++ [src]) + setSource src' + opts <- get ROpts + put ROpts (record { mainfile = Just src' } opts) + pure (Just src') + where + dropHead : String -> List String -> List String + dropHead str [] = [] + dropHead str (x :: xs) + = if x == str then xs else x :: xs + loadDependencies : List String -> Core () + loadDependencies = traverse_ addPkgDir diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr new file mode 100644 index 000000000..5257a86d6 --- /dev/null +++ b/src/Idris/REPL.idr @@ -0,0 +1,896 @@ +module Idris.REPL + +import Compiler.Scheme.Chez +import Compiler.Scheme.Racket +import Compiler.Scheme.Gambit +import Compiler.Common + +import Core.AutoSearch +import Core.CaseTree +import Core.CompileExpr +import Core.Context +import Core.Env +import Core.InitPrimitives +import Core.LinearCheck +import Core.Metadata +import Core.Normalise +import Core.Options +import Core.Termination +import Core.TT +import Core.Unify + +import Parser.Unlit + +import Idris.Desugar +import Idris.Error +import Idris.IDEMode.CaseSplit +import Idris.IDEMode.Commands +import Idris.IDEMode.MakeClause +import Idris.ModTree +import Idris.Parser +import Idris.Resugar +import public Idris.REPLCommon +import Idris.Syntax +import Idris.Version + +import TTImp.Elab +import TTImp.Elab.Check +import TTImp.Interactive.CaseSplit +import TTImp.Interactive.ExprSearch +import TTImp.Interactive.GenerateDef +import TTImp.Interactive.MakeLemma +import TTImp.TTImp +import TTImp.ProcessDecls + +import Data.List +import Data.Maybe +import Data.NameMap +import Data.Stream +import Data.Strings + +import System + +%default covering + +showInfo : {auto c : Ref Ctxt Defs} -> + (Name, Int, GlobalDef) -> Core () +showInfo (n, idx, d) + = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++ + show !(toFullNames (definition d))) + coreLift $ putStrLn (show (multiplicity d)) + coreLift $ putStrLn ("Erasable args: " ++ show (eraseArgs d)) + coreLift $ putStrLn ("Detaggable arg types: " ++ show (safeErase d)) + coreLift $ putStrLn ("Specialise args: " ++ show (specArgs d)) + coreLift $ putStrLn ("Inferrable args: " ++ show (inferrable d)) + case compexpr d of + Nothing => pure () + Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr) + coreLift $ putStrLn ("Refers to: " ++ + show !(traverse getFullName (keys (refersTo d)))) + coreLift $ putStrLn ("Refers to (runtime): " ++ + show !(traverse getFullName (keys (refersToRuntime d)))) + when (not (isNil (sizeChange d))) $ + let scinfo = map (\s => show (fnCall s) ++ ": " ++ + show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in + coreLift $ putStrLn $ + "Size change: " ++ showSep ", " scinfo + +isHole : GlobalDef -> Maybe Nat +isHole def + = case definition def of + Hole locs _ => Just locs + PMDef pi _ _ _ _ => + case holeInfo pi of + NotHole => Nothing + SolvedHole n => Just n + _ => Nothing + +showCount : RigCount -> String +showCount = elimSemi + " 0 " + " 1 " + (const " ") + +impBracket : Bool -> String -> String +impBracket False str = str +impBracket True str = "{" ++ str ++ "}" + +showName : Name -> Bool +showName (UN "_") = False +showName (MN _ _) = False +showName _ = True + +tidy : Name -> String +tidy (MN n _) = n +tidy n = show n + +showEnv : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> Env Term vars -> Name -> Nat -> Term vars -> + Core (List (Name, String), String) +showEnv defs env fn (S args) (Bind fc x (Let c val ty) sc) + = showEnv defs env fn args (subst val sc) +showEnv defs env fn (S args) (Bind fc x b sc) + = do ity <- resugar env !(normalise defs env (binderType b)) + let pre = if showName x + then REPL.showCount (multiplicity b) ++ + impBracket (implicitBind b) (tidy x ++ " : " ++ show ity) ++ "\n" + else "" + (envstr, ret) <- showEnv defs (b :: env) fn args sc + pure ((x, pre) :: envstr, ret) + where + implicitBind : Binder (Term vars) -> Bool + implicitBind (Pi _ Explicit _) = False + implicitBind (Pi _ _ _) = True + implicitBind (Lam _ Explicit _) = False + implicitBind (Lam _ _ _) = True + implicitBind _ = False +showEnv defs env fn args ty + = do ity <- resugar env !(normalise defs env ty) + pure ([], "-------------------------------------\n" ++ + nameRoot fn ++ " : " ++ show ity) + +showHole : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> Env Term vars -> Name -> Nat -> Term vars -> + Core String +showHole gam env fn args ty + = do (envs, ret) <- showEnv gam env fn args ty + pp <- getPPrint + let envs' = if showImplicits pp + then envs + else dropShadows envs + pure (concat (map snd envs') ++ ret) + where + dropShadows : List (Name, a) -> List (Name, a) + dropShadows [] = [] + dropShadows ((n, ty) :: ns) + = if n `elem` map fst ns + then dropShadows ns + else (n, ty) :: dropShadows ns + +displayType : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> (Name, Int, GlobalDef) -> + Core String +displayType defs (n, i, gdef) + = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef)) + pure (show (fullname gdef) ++ " : " ++ show tm)) + (\num => showHole defs [] n num (type gdef)) + (isHole gdef) + +getEnvTerm : {vars : _} -> + List Name -> Env Term vars -> Term vars -> + (vars' ** (Env Term vars', Term vars')) +getEnvTerm (n :: ns) env (Bind fc x b sc) + = if n == x + then getEnvTerm ns (b :: env) sc + else (_ ** (env, Bind fc x b sc)) +getEnvTerm _ env tm = (_ ** (env, tm)) + +displayTerm : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> ClosedTerm -> + Core String +displayTerm defs tm + = do ptm <- resugar [] !(normaliseHoles defs [] tm) + pure (show ptm) + +displayPatTerm : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> ClosedTerm -> + Core String +displayPatTerm defs tm + = do ptm <- resugarNoPatvars [] !(normaliseHoles defs [] tm) + pure (show ptm) + +displayClause : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> (vs ** (Env Term vs, Term vs, Term vs)) -> + Core String +displayClause defs (vs ** (env, lhs, rhs)) + = do lhstm <- resugar env !(normaliseHoles defs env lhs) + rhstm <- resugar env !(normaliseHoles defs env rhs) + pure (show lhstm ++ " = " ++ show rhstm) + +displayPats : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Defs -> (Name, Int, GlobalDef) -> + Core String +displayPats defs (n, idx, gdef) + = case definition gdef of + PMDef _ _ _ _ pats + => do ty <- displayType defs (n, idx, gdef) + ps <- traverse (displayClause defs) pats + pure (ty ++ "\n" ++ showSep "\n" ps) + _ => pure (show n ++ " is not a pattern matching definition") + +setOpt : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + REPLOpt -> Core () +setOpt (ShowImplicits t) + = do pp <- getPPrint + setPPrint (record { showImplicits = t } pp) +setOpt (ShowNamespace t) + = do pp <- getPPrint + setPPrint (record { fullNamespace = t } pp) +setOpt (ShowTypes t) + = do opts <- get ROpts + put ROpts (record { showTypes = t } opts) +setOpt (EvalMode m) + = do opts <- get ROpts + put ROpts (record { evalMode = m } opts) +setOpt (Editor e) + = do opts <- get ROpts + put ROpts (record { editor = e } opts) +setOpt (CG e) + = case getCG e of + Just cg => setCG cg + Nothing => iputStrLn "No such code generator available" + +getOptions : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + Core (List REPLOpt) +getOptions = do + pp <- getPPrint + opts <- get ROpts + pure $ [ ShowImplicits (showImplicits pp), ShowNamespace (fullNamespace pp) + , ShowTypes (showTypes opts), EvalMode (evalMode opts) + , Editor (editor opts) + ] + +export +findCG : {auto c : Ref Ctxt Defs} -> Core Codegen +findCG + = do defs <- get Ctxt + case codegen (session (options defs)) of + Chez => pure codegenChez + Racket => pure codegenRacket + Gambit => pure codegenGambit + +anyAt : (FC -> Bool) -> FC -> a -> Bool +anyAt p loc y = p loc + +printClause : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Maybe String -> Nat -> ImpClause -> + Core String +printClause l i (PatClause _ lhsraw rhsraw) + = do lhs <- pterm lhsraw + rhs <- pterm rhsraw + pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs)) +printClause l i (WithClause _ lhsraw wvraw csraw) + = do lhs <- pterm lhsraw + wval <- pterm wvraw + cs <- traverse (printClause l (i + 2)) csraw + pure ((relit l ((pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n")) ++ + showSep "\n" cs)) +printClause l i (ImpossibleClause _ lhsraw) + = do lhs <- pterm lhsraw + pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible")) + + +lookupDefTyName : Name -> Context -> + Core (List (Name, Int, (Def, ClosedTerm))) +lookupDefTyName = lookupNameBy (\g => (definition g, type g)) + +public export +data EditResult : Type where + DisplayEdit : List String -> EditResult + EditError : String -> EditResult + MadeLemma : Maybe String -> Name -> PTerm -> String -> EditResult + +updateFile : {auto r : Ref ROpts REPLOpts} -> + (List String -> List String) -> Core EditResult +updateFile update + = do opts <- get ROpts + let Just f = mainfile opts + | Nothing => pure (DisplayEdit []) -- no file, nothing to do + Right content <- coreLift $ readFile f + | Left err => throw (FileErr f err) + coreLift $ writeFile (f ++ "~") content + coreLift $ writeFile f (unlines (update (lines content))) + pure (DisplayEdit []) + +rtrim : String -> String +rtrim str = reverse (ltrim (reverse str)) + +addClause : String -> Nat -> List String -> List String +addClause c Z xs = rtrim c :: xs +addClause c (S k) (x :: xs) = x :: addClause c k xs +addClause c (S k) [] = [c] + +caseSplit : String -> Nat -> List String -> List String +caseSplit c Z (x :: xs) = rtrim c :: xs +caseSplit c (S k) (x :: xs) = x :: caseSplit c k xs +caseSplit c _ [] = [c] + +proofSearch : Name -> String -> Nat -> List String -> List String +proofSearch n res Z (x :: xs) = replaceStr ("?" ++ show n) res x :: xs + where + replaceStr : String -> String -> String -> String + replaceStr rep new "" = "" + replaceStr rep new str + = if isPrefixOf rep str + then new ++ pack (drop (length rep) (unpack str)) + else assert_total $ strCons (prim__strHead str) + (replaceStr rep new (prim__strTail str)) +proofSearch n res (S k) (x :: xs) = x :: proofSearch n res k xs +proofSearch n res _ [] = [] + +addMadeLemma : Maybe String -> Name -> String -> String -> Nat -> List String -> List String +addMadeLemma lit n ty app line content + = addApp lit line [] (proofSearch n app line content) + where + -- Put n : ty in the first blank line + insertInBlank : Maybe String -> List String -> List String + insertInBlank lit [] = [relit lit $ show n ++ " : " ++ ty ++ "\n"] + insertInBlank lit (x :: xs) + = if trim x == "" + then ("\n" ++ (relit lit $ show n ++ " : " ++ ty ++ "\n")) :: xs + else x :: insertInBlank lit xs + + addApp : Maybe String -> Nat -> List String -> List String -> List String + addApp lit Z acc rest = reverse (insertInBlank lit acc) ++ rest + addApp lit (S k) acc (x :: xs) = addApp lit k (x :: acc) xs + addApp _ (S k) acc [] = reverse acc + +processEdit : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + EditCmd -> Core EditResult +processEdit (TypeAt line col name) + = do defs <- get Ctxt + glob <- lookupCtxtName name (gamma defs) + res <- the (Core String) $ case glob of + [] => pure "" + ts => do tys <- traverse (displayType defs) ts + pure (showSep "\n" tys) + Just (n, num, t) <- findTypeAt (\p, n => within (line-1, col-1) p) + | Nothing => if res == "" + then throw (UndefinedName (MkFC "(interactive)" (0,0) (0,0)) name) + else pure (DisplayEdit [res]) + if res == "" + then pure (DisplayEdit [ nameRoot n ++ " : " ++ + !(displayTerm defs t)]) + else pure (DisplayEdit []) -- ? Why () This means there is a global name and a type at (line,col) +processEdit (CaseSplit upd line col name) + = do let find = if col > 0 + then within (line-1, col-1) + else onLine (line-1) + OK splits <- getSplits (anyAt find) name + | SplitFail err => pure (EditError (show err)) + lines <- updateCase splits (line-1) (col-1) + if upd + then updateFile (caseSplit (unlines lines) (integerToNat (cast (line - 1)))) + else pure $ DisplayEdit lines +processEdit (AddClause upd line name) + = do Just c <- getClause line name + | Nothing => pure (EditError (show name ++ " not defined here")) + if upd + then updateFile (addClause c (integerToNat (cast line))) + else pure $ DisplayEdit [c] +processEdit (ExprSearch upd line name hints all) + = do defs <- get Ctxt + syn <- get Syn + let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn) + case !(lookupDefName name (gamma defs)) of + [(n, nidx, Hole locs _)] => + do tms <- exprSearch replFC name [] + defs <- get Ctxt + restms <- traverse (normaliseHoles defs []) tms + itms <- the (Core (List PTerm)) + (traverse (\tm => + do let (_ ** (env, tm')) = dropLams locs [] tm + resugar env tm') restms) + if all + then pure $ DisplayEdit (map show itms) + else case itms of + [] => pure $ EditError "No search results" + (x :: xs) => + let res = show (the PTerm (if brack + then addBracket replFC x + else x)) in + if upd + then updateFile (proofSearch name res (integerToNat (cast (line - 1)))) + else pure $ DisplayEdit [res] + [(n, nidx, PMDef pi [] (STerm tm) _ _)] => + case holeInfo pi of + NotHole => pure $ EditError "Not a searchable hole" + SolvedHole locs => + do let (_ ** (env, tm')) = dropLams locs [] tm + itm <- resugar env tm' + let res = show (the PTerm (if brack + then addBracket replFC itm + else itm)) + if upd + then updateFile (proofSearch name res (integerToNat (cast (line - 1)))) + else pure $ DisplayEdit [res] + [] => pure $ EditError $ "Unknown name " ++ show name + _ => pure $ EditError "Not a searchable hole" + where + dropLams : {vars : _} -> + Nat -> Env Term vars -> Term vars -> + (vars' ** (Env Term vars', Term vars')) + dropLams Z env tm = (_ ** (env, tm)) + dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc + dropLams _ env tm = (_ ** (env, tm)) +processEdit (GenerateDef upd line name) + = do defs <- get Ctxt + Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p) + | Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line)) + case !(lookupDefExact n' (gamma defs)) of + Just None => + catch + (do Just (fc, cs) <- makeDef (\p, n => onLine line p) n' + | Nothing => processEdit (AddClause upd line name) + Just srcLine <- getSourceLine line + | Nothing => pure (EditError "Source line not found") + let (markM, srcLineUnlit) = isLitLine srcLine + let l : Nat = integerToNat (cast (snd (startPos fc))) + ls <- traverse (printClause markM l) cs + if upd + then updateFile (addClause (unlines ls) (integerToNat (cast line))) + else pure $ DisplayEdit ls) + (\err => pure $ EditError $ "Can't find a definition for " ++ show n' ++ ": " ++ show err) + Just _ => pure $ EditError "Already defined" + Nothing => pure $ EditError $ "Can't find declaration for " ++ show name +processEdit (MakeLemma upd line name) + = do defs <- get Ctxt + syn <- get Syn + let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn) + case !(lookupDefTyName name (gamma defs)) of + [(n, nidx, Hole locs _, ty)] => + do (lty, lapp) <- makeLemma replFC name locs ty + pty <- pterm lty + papp <- pterm lapp + opts <- get ROpts + let pappstr = show (the PTerm (if brack + then addBracket replFC papp + else papp)) + Just srcLine <- getSourceLine line + | Nothing => pure (EditError "Source line not found") + let (markM,_) = isLitLine srcLine + let markML : Nat = length (fromMaybe "" markM) + if upd + then updateFile (addMadeLemma markM name (show pty) pappstr + (max 0 (integerToNat (cast (line - 1))))) + else pure $ MadeLemma markM name pty pappstr + _ => pure $ EditError "Can't make lifted definition" +processEdit (MakeCase upd line name) + = pure $ EditError "Not implemented yet" +processEdit (MakeWith upd line name) + = do Just l <- getSourceLine line + | Nothing => pure (EditError "Source line not available") + pure $ DisplayEdit [makeWith name l] + +public export +data MissedResult : Type where + CasesMissing : Name -> List String -> MissedResult + CallsNonCovering : Name -> List Name -> MissedResult + AllCasesCovered : Name -> MissedResult + +public export +data REPLResult : Type where + Done : REPLResult + REPLError : String -> REPLResult + Executed : PTerm -> REPLResult + RequestedHelp : REPLResult + Evaluated : PTerm -> (Maybe PTerm) -> REPLResult + Printed : List String -> REPLResult + TermChecked : PTerm -> PTerm -> REPLResult + FileLoaded : String -> REPLResult + ErrorLoadingFile : String -> FileError -> REPLResult + ErrorsBuildingFile : String -> List Error -> REPLResult + NoFileLoaded : REPLResult + CurrentDirectory : String -> REPLResult + CompilationFailed: REPLResult + Compiled : String -> REPLResult + ProofFound : PTerm -> REPLResult + Missed : List MissedResult -> REPLResult + CheckedTotal : List (Name, Totality) -> REPLResult + FoundHoles : List Name -> REPLResult + OptionsSet : List REPLOpt -> REPLResult + LogLevelSet : Nat -> REPLResult + VersionIs : Version -> REPLResult + Exited : REPLResult + Edited : EditResult -> REPLResult + +export +execExp : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + PTerm -> Core REPLResult +execExp ctm + = do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm) + inidx <- resolveName (UN "[input]") + (tm, ty) <- elabTerm inidx InExpr [] (MkNested []) + [] ttimp Nothing + tm_erased <- linearCheck replFC linear True [] tm + execute !findCG tm_erased + pure $ Executed ctm + + +export +compileExp : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + PTerm -> String -> Core REPLResult +compileExp ctm outfile + = do inidx <- resolveName (UN "[input]") + ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm) + (tm, gty) <- elabTerm inidx InExpr [] (MkNested []) + [] ttimp Nothing + tm_erased <- linearCheck replFC linear True [] tm + ok <- compile !findCG tm_erased outfile + maybe (pure CompilationFailed) + (pure . Compiled) + ok + +export +loadMainFile : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + String -> Core REPLResult +loadMainFile f + = do resetContext + Right res <- coreLift (readFile f) + | Left err => do setSource "" + pure (ErrorLoadingFile f err) + errs <- logTime "Build deps" $ buildDeps f + updateErrorLine errs + setSource res + case errs of + [] => pure (FileLoaded f) + _ => pure (ErrorsBuildingFile f errs) + + +||| Process a single `REPLCmd` +||| +||| Returns `REPLResult` for display by the higher level shell which +||| is invoking this interactive command processing. +export +process : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + REPLCmd -> Core REPLResult +process (Eval itm) + = do opts <- get ROpts + case evalMode opts of + Execute => do execExp itm; pure (Executed itm) + _ => + do ttimp <- desugar AnyExpr [] itm + inidx <- resolveName (UN "[input]") + -- a TMP HACK to prioritise list syntax for List: hide + -- foreign argument lists. TODO: once the new FFI is fully + -- up and running we won't need this. Also, if we add + -- 'with' disambiguation we can use that instead. + catch (do hide replFC (NS ["PrimIO"] (UN "::")) + hide replFC (NS ["PrimIO"] (UN "Nil"))) + (\err => pure ()) + (tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested []) + [] ttimp Nothing + defs <- get Ctxt + opts <- get ROpts + let norm = nfun (evalMode opts) + ntm <- norm defs [] tm + itm <- resugar [] ntm + logTermNF 5 "Normalised" [] ntm + if showTypes opts + then do ty <- getTerm gty + ity <- resugar [] !(norm defs [] ty) + pure (Evaluated itm (Just ity)) + else pure (Evaluated itm Nothing) + where + emode : REPLEval -> ElabMode + emode EvalTC = InType + emode _ = InExpr + + nfun : {vs : _} -> + REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs) + nfun NormaliseAll = normaliseAll + nfun _ = normalise +process (Check (PRef fc fn)) + = do defs <- get Ctxt + case !(lookupCtxtName fn (gamma defs)) of + [] => throw (UndefinedName fc fn) + ts => do tys <- traverse (displayType defs) ts + pure (Printed tys) +process (Check itm) + = do inidx <- resolveName (UN "[input]") + ttimp <- desugar AnyExpr [] itm + (tm, gty) <- elabTerm inidx InExpr [] (MkNested []) + [] ttimp Nothing + defs <- get Ctxt + itm <- resugar [] !(normaliseHoles defs [] tm) + ty <- getTerm gty + ity <- resugar [] !(normaliseScope defs [] ty) + pure (TermChecked itm ity) +process (PrintDef fn) + = do defs <- get Ctxt + case !(lookupCtxtName fn (gamma defs)) of + [] => throw (UndefinedName replFC fn) + ts => do defs <- traverse (displayPats defs) ts + pure (Printed defs) +process Reload + = do opts <- get ROpts + case mainfile opts of + Nothing => pure NoFileLoaded + Just f => loadMainFile f +process (Load f) + = do opts <- get ROpts + put ROpts (record { mainfile = Just f } opts) + -- Clear the context and load again + loadMainFile f +process (CD dir) + = do setWorkingDir dir + workDir <- getWorkingDir + pure (CurrentDirectory workDir) +process CWD + = do workDir <- getWorkingDir + pure (CurrentDirectory workDir) +process Edit + = do opts <- get ROpts + case mainfile opts of + Nothing => pure NoFileLoaded + Just f => + do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts) + coreLift $ system (editor opts ++ " " ++ f ++ line) + loadMainFile f +process (Compile ctm outfile) + = compileExp ctm outfile +process (Exec ctm) + = execExp ctm +process Help + = pure RequestedHelp +process (ProofSearch n_in) + = do defs <- get Ctxt + [(n, i, ty)] <- lookupTyName n_in (gamma defs) + | [] => throw (UndefinedName replFC n_in) + | ns => throw (AmbiguousName replFC (map fst ns)) + tm <- search replFC top False 1000 n ty [] + itm <- resugar [] !(normaliseHoles defs [] tm) + pure $ ProofFound itm +process (Missing n) + = do defs <- get Ctxt + case !(lookupCtxtName n (gamma defs)) of + [] => throw (UndefinedName replFC n) + ts => map Missed $ traverse (\fn => + do tot <- getTotality replFC fn + the (Core MissedResult) $ case isCovering tot of + MissingCases cs => + do tms <- traverse (displayPatTerm defs) cs + pure $ CasesMissing fn tms + NonCoveringCall ns_in => + do ns <- traverse getFullName ns_in + pure $ CallsNonCovering fn ns + _ => pure $ AllCasesCovered fn) + (map fst ts) +process (Total n) + = do defs <- get Ctxt + case !(lookupCtxtName n (gamma defs)) of + [] => throw (UndefinedName replFC n) + ts => map CheckedTotal $ + traverse (\fn => + do checkTotal replFC fn + tot <- getTotality replFC fn >>= toFullNames + pure $ (fn, tot)) + (map fst ts) +process (DebugInfo n) + = do defs <- get Ctxt + traverse_ showInfo !(lookupCtxtName n (gamma defs)) + pure Done +process (SetOpt opt) + = do setOpt opt + pure Done +process GetOpts + = do opts <- getOptions + pure $ OptionsSet opts +process (SetLog lvl) + = do setLogLevel lvl + pure $ LogLevelSet lvl +process Metavars + = do ms <- getUserHoles + pure $ FoundHoles ms +process (Editing cmd) + = do ppopts <- getPPrint + -- Since we're working in a local environment, don't do the usual + -- thing of printing out the full environment for parameterised + -- calls or calls in where blocks + setPPrint (record { showFullEnv = False } ppopts) + res <- processEdit cmd + setPPrint ppopts + pure $ Edited res +process Quit + = pure Exited +process NOP + = pure Done +process ShowVersion + = pure $ VersionIs version + +processCatch : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + REPLCmd -> Core REPLResult +processCatch cmd + = do c' <- branch + u' <- get UST + s' <- get Syn + o' <- get ROpts + catch (do ust <- get UST + r <- process cmd + commit + pure r) + (\err => do put Ctxt c' + put UST u' + put Syn s' + put ROpts o' + pure $ REPLError !(display err) + ) + +parseEmptyCmd : EmptyRule (Maybe REPLCmd) +parseEmptyCmd = eoi *> (pure Nothing) + +parseCmd : EmptyRule (Maybe REPLCmd) +parseCmd = do c <- command; eoi; pure $ Just c + +export +parseRepl : String -> Either ParseError (Maybe REPLCmd) +parseRepl inp + = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of + Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd) + Just cmd => Right $ Just cmd + where + -- a right load of hackery - we can't tokenise the filename using the + -- ordinary parser. There's probably a better way... + getLoad : Nat -> (String -> REPLCmd) -> String -> Maybe REPLCmd + getLoad n cmd str = Just (cmd (trim (substr n (length str) str))) + + fnameCmd : List (String, String -> REPLCmd) -> String -> Maybe REPLCmd + fnameCmd [] inp = Nothing + fnameCmd ((pre, cmd) :: rest) inp + = if isPrefixOf pre inp + then getLoad (length pre) cmd inp + else fnameCmd rest inp + +export +interpret : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + String -> Core REPLResult +interpret inp + = case parseRepl inp of + Left err => pure $ REPLError (show err) + Right Nothing => pure Done + Right (Just cmd) => processCatch cmd + +mutual + export + replCmd : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + String -> Core () + replCmd "" = pure () + replCmd cmd + = do res <- interpret cmd + displayResult res + + export + repl : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + Core () + repl + = do ns <- getNS + opts <- get ROpts + coreLift (putStr (prompt (evalMode opts) ++ showSep "." (reverse ns) ++ "> ")) + inp <- coreLift getLine + end <- coreLift $ fEOF stdin + if end + then do + -- start a new line in REPL mode (not relevant in IDE mode) + coreLift $ putStrLn "" + iputStrLn "Bye for now!" + else do res <- interpret inp + handleResult res + + where + prompt : REPLEval -> String + prompt EvalTC = "[tc] " + prompt NormaliseAll = "" + prompt Execute = "[exec] " + + handleMissing : MissedResult -> String + handleMissing (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs + handleMissing (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function" + ++ (case ns of + [f] => " " ++ show f + _ => "s: " ++ showSep ", " (map show ns))) + handleMissing (AllCasesCovered fn) = show fn ++ ": All cases covered" + + export + handleResult : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core () + handleResult Exited = iputStrLn "Bye for now!" + handleResult other = do { displayResult other ; repl } + + export + displayResult : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core () + displayResult (REPLError err) = printError err + displayResult (Evaluated x Nothing) = printResult $ show x + displayResult (Evaluated x (Just y)) = printResult $ show x ++ " : " ++ show y + displayResult (Printed xs) = printResult (showSep "\n" xs) + displayResult (TermChecked x y) = printResult $ show x ++ " : " ++ show y + displayResult (FileLoaded x) = printResult $ "Loaded file " ++ x + displayResult (ErrorLoadingFile x err) = printError $ "Error loading file " ++ x ++ ": " ++ show err + displayResult (ErrorsBuildingFile x errs) = printError $ "Error(s) building file " ++ x -- messages already displayed while building + displayResult NoFileLoaded = printError "No file can be reloaded" + displayResult (CurrentDirectory dir) = printResult ("Current working directory is '" ++ dir ++ "'") + displayResult CompilationFailed = printError "Compilation failed" + displayResult (Compiled f) = printResult $ "File " ++ f ++ " written" + displayResult (ProofFound x) = printResult $ show x + displayResult (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases + displayResult (CheckedTotal xs) = printResult $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs + displayResult (FoundHoles []) = printResult $ "No holes" + displayResult (FoundHoles [x]) = printResult $ "1 hole: " ++ show x + displayResult (FoundHoles xs) = printResult $ show (length xs) ++ " holes: " ++ + showSep ", " (map show xs) + displayResult (LogLevelSet k) = printResult $ "Set loglevel to " ++ show k + displayResult (VersionIs x) = printResult $ showVersion True x + displayResult (RequestedHelp) = printResult displayHelp + displayResult (Edited (DisplayEdit [])) = pure () + displayResult (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs + displayResult (Edited (EditError x)) = printError x + displayResult (Edited (MadeLemma lit name pty pappstr)) = printResult (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr) + displayResult (OptionsSet opts) = printResult $ showSep "\n" $ map show opts + displayResult _ = pure () + + displayHelp : String + displayHelp = + showSep "\n" $ map cmdInfo help + where + makeSpace : Nat -> String + makeSpace n = pack $ take n (repeat ' ') + + col : Nat -> Nat -> String -> String -> String -> String + col c1 c2 l m r = + l ++ (makeSpace $ c1 `minus` length l) ++ + m ++ (makeSpace $ c2 `minus` length m) ++ r + + cmdInfo : (List String, CmdArg, String) -> String + cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text + + export + displayErrors : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core () + displayErrors (ErrorLoadingFile x err) = printError $ "File error in " ++ x ++ ": " ++ show err + displayErrors _ = pure () diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr new file mode 100644 index 000000000..81881b60a --- /dev/null +++ b/src/Idris/SetOptions.idr @@ -0,0 +1,139 @@ +module Idris.SetOptions + +import Core.Context +import Core.Directory +import Core.Metadata +import Core.Options +import Core.Unify + +import Idris.CommandLine +import Idris.REPL +import Idris.Syntax +import Idris.Version + +import IdrisPaths + +import System + +-- TODO: Version numbers on dependencies +export +addPkgDir : {auto c : Ref Ctxt Defs} -> + String -> Core () +addPkgDir p + = do defs <- get Ctxt + addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++ + "idris2-" ++ showVersion False version ++ dirSep ++ p) + +dirOption : Dirs -> DirCommand -> Core () +dirOption dirs LibDir + = coreLift $ putStrLn + (dir_prefix dirs ++ dirSep ++ "idris2-" ++ showVersion False version ++ dirSep) + +-- Options to be processed before type checking. Return whether to continue. +export +preOptions : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + List CLOpt -> Core Bool +preOptions [] = pure True +preOptions (NoBanner :: opts) + = do setSession (record { nobanner = True } !getSession) + preOptions opts +-- These things are processed later, but imply nobanner too +preOptions (OutputFile _ :: opts) + = do setSession (record { nobanner = True } !getSession) + preOptions opts +preOptions (ExecFn _ :: opts) + = do setSession (record { nobanner = True } !getSession) + preOptions opts +preOptions (IdeMode :: opts) + = do setSession (record { nobanner = True } !getSession) + preOptions opts +preOptions (CheckOnly :: opts) + = do setSession (record { nobanner = True } !getSession) + preOptions opts +preOptions (Quiet :: opts) + = do setOutput (REPL True) + preOptions opts +preOptions (NoPrelude :: opts) + = do setSession (record { noprelude = True } !getSession) + preOptions opts +preOptions (SetCG e :: opts) + = case getCG e of + Just cg => do setCG cg + preOptions opts + Nothing => + do coreLift $ putStrLn "No such code generator" + coreLift $ putStrLn $ "Code generators available: " ++ + showSep ", " (map fst availableCGs) + coreLift $ exitWith (ExitFailure 1) +preOptions (PkgPath p :: opts) + = do addPkgDir p + preOptions opts +preOptions (Directory d :: opts) + = do defs <- get Ctxt + dirOption (dirs (options defs)) d + pure False +preOptions (Timing :: opts) + = do setLogTimings True + preOptions opts +preOptions (DebugElabCheck :: opts) + = do setDebugElabCheck True + preOptions opts +preOptions (RunREPL _ :: opts) + = do setOutput (REPL True) + setSession (record { nobanner = True } !getSession) + preOptions opts +preOptions (FindIPKG :: opts) + = do setSession (record { findipkg = True } !getSession) + preOptions opts +preOptions (DumpCases f :: opts) + = do setSession (record { dumpcases = Just f } !getSession) + preOptions opts +preOptions (DumpLifted f :: opts) + = do setSession (record { dumplifted = Just f } !getSession) + preOptions opts +preOptions (DumpANF f :: opts) + = do setSession (record { dumpanf = Just f } !getSession) + preOptions opts +preOptions (DumpVMCode f :: opts) + = do setSession (record { dumpvmcode = Just f } !getSession) + preOptions opts +preOptions (_ :: opts) = preOptions opts + +-- Options to be processed after type checking. Returns whether execution +-- should continue (i.e., whether to start a REPL) +export +postOptions : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + List CLOpt -> Core Bool +postOptions [] = pure True +postOptions (OutputFile outfile :: rest) + = do compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile + postOptions rest + pure False +postOptions (ExecFn str :: rest) + = do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str)) + postOptions rest + pure False +postOptions (CheckOnly :: rest) + = do postOptions rest + pure False +postOptions (RunREPL str :: rest) + = do replCmd str + pure False +postOptions (_ :: rest) = postOptions rest + +export +ideMode : List CLOpt -> Bool +ideMode [] = False +ideMode (IdeMode :: _) = True +ideMode (_ :: xs) = ideMode xs + +export +ideModeSocket : List CLOpt -> Bool +ideModeSocket [] = False +ideModeSocket (IdeModeSocket _ :: _) = True +ideModeSocket (_ :: xs) = ideModeSocket xs