Everything but the IDE protocol

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)

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 ()

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

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

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 (LTE CharType) [x, y] = boolop "char<=?" [x, y]
+schOp (EQ CharType) [x, y] = boolop "char=?" [x, y]
+schOp (GTE 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 (LTE StringType) [x, y] = boolop "string<=?" [x, y]
+schOp (EQ StringType) [x, y] = boolop "string=?" [x, y]
+schOp (GTE 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

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

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
+

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'))

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

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) |]

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

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)))) ' ')

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"

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)

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

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

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])

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 ()

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

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 ()

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