Merge branch 'master' into factorisation

CHANGELOG.md

@@ -1,3 +1,23 @@
+Changes since Idris 2 v0.2.0
+----------------------------
+
+Language changes:
+
+* `Bits8`, `Bits16`, `Bits32` and `Bits64` primitive types added, with:
+   + `Num`, `Eq`, `Ord` and `Show` implementations.
+   + Casts from `Integer`, for literals
+   + Casts to `Int` (except `Bits64` which might not fit), `Integer` and `String`
+   + Passed to C FFI as `unsigned`
+   + Primitives added in `Data.Buffer`
+* Elaborator reflection and quoting terms
+   + Requires extension `%language ElabReflection`
+   + API defined in `Language.Reflection`, including functions for getting types
+     of global names, constructors of data types, and adding new top level
+     declarations
+   + Implemented `%macro` function flag, to remove the syntactic noise of
+     invoking elaborator scripts. This means the function must always
+     be fully applied, and is run under `%runElab`
+
 Changes since Idris 2 v0.1.0
 ----------------------------
 

INSTALL.md

@@ -9,7 +9,10 @@ requirements are:
   a Mac, you can install this with `brew install coreutils`.
 
 On Windows, it has been reported that installing via `MSYS2` works
-(https://www.msys2.org/). On Raspberry Pi, you can bootstrap via Racket.
+(https://www.msys2.org/). On Windows older than Windows 8, you may need to
+set an environment variable `OLD_WIN=1` or modify it in `config.mk`.
+
+On Raspberry Pi, you can bootstrap via Racket.
 
 By default, code generation is via Chez Scheme. You can use Racket instead,
 by setting the environment variable `IDRIS2_CG=racket` before running `make`.

config.mk

@@ -4,6 +4,9 @@ PREFIX ?= $(HOME)/.idris2
 
 CC ?= clang
 
+# For Windows targets. Set to 1 to support Windows 7.
+OLD_WIN ?= 0
+
 ##################################################################
 
 RANLIB ?= ranlib

docs/make.bat

@@ -21,7 +21,7 @@ if errorlevel 9009 (
 	echo.may add the Sphinx directory to PATH.
 	echo.
 	echo.If you don't have Sphinx installed, grab it from
-	echo.http://sphinx-doc.org/
+	echo.https://www.sphinx-doc.org/
 	exit /b 1
 )
 

docs/source/app/exceptionsstate.rst

@@ -64,7 +64,7 @@ and is not required at run-time, as explicitly stated in the types of
 These use an ``auto``-implicit to pass around
 a ``State`` with the relevant ``tag`` implicitly, so we refer
 to states by tag alone. In ``helloCount`` earlier, we used an empty type
-\texttt{Counter} as the tag:
+``Counter`` as the tag:
 
 .. code-block:: idris
 

docs/source/faq/faq.rst

@@ -57,5 +57,5 @@ You can find more details in Section :ref:`updates-index`.
 Where can I find more answers?
 ==============================
 
-The `Idris 1 FAQ <http://docs.idris-lang.org/en/latest/faq/faq.html>`_ is
+The `Idris 1 FAQ <https://docs.idris-lang.org/en/latest/faq/faq.html>`_ is
 mostly still relevant.

docs/source/tutorial/conclusions.rst

@@ -10,7 +10,7 @@ dependent types in general, can be obtained from various sources:
 *  `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
    by Edwin Brady, available from `Manning <https://www.manning.com>`_.
 
-*  The Idris web site (http://www.idris-lang.org/) and by asking
+*  The Idris web site (https://www.idris-lang.org/) and by asking
    questions on the mailing list.
 
 *  The IRC channel ``#idris``, on
@@ -30,7 +30,7 @@ dependent types in general, can be obtained from various sources:
 
 *  Existing projects on the ``Idris Hackers`` web space:
    
-   * http://idris-hackers.github.io.
+   * https://idris-hackers.github.io.
 
 *  Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_).  Although these mostly
    describe older versions of Idris.
@@ -41,14 +41,14 @@ dependent types in general, can be obtained from various sources:
        Aspects of Declarative Languages (PADL'12), Claudio Russo and
        Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
        242-257. DOI=10.1007/978-3-642-27694-1_18
-       http://dx.doi.org/10.1007/978-3-642-27694-1_18
+       https://dx.doi.org/10.1007/978-3-642-27694-1_18
 
 .. [#Brady] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
        dependent types. In Proceedings of the 5th ACM workshop on
        Programming languages meets program verification (PLPV
        '11). ACM, New York, NY, USA,
        43-54. DOI=10.1145/1929529.1929536
-       http://doi.acm.org/10.1145/1929529.1929536
+       https://doi.acm.org/10.1145/1929529.1929536
 
 .. [#BradyHammond2010] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
        inefficient engine: using partial evaluation to improve
@@ -56,4 +56,4 @@ dependent types in general, can be obtained from various sources:
        15th ACM SIGPLAN international conference on Functional
        programming (ICFP '10). ACM, New York, NY, USA,
        297-308. DOI=10.1145/1863543.1863587
-       http://doi.acm.org/10.1145/1863543.1863587
+       https://doi.acm.org/10.1145/1863543.1863587

docs/source/tutorial/interactive.rst

@@ -252,5 +252,5 @@ for other editors can be added in a relatively straightforward manner
 by using ``idris2 -–client``.
 More sophisticated support can be added by using the IDE protocol (yet to
 be documented for Idris 2, but which mostly extends to protocol documented for 
-`Idris 1 <http://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.
+`Idris 1 <https://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.
 

docs/source/tutorial/interfaces.rst

@@ -658,4 +658,4 @@ parameter used to find an implementation.
 .. [#ConorRoss] Conor McBride and Ross Paterson. 2008. Applicative programming
        with effects. J. Funct. Program. 18, 1 (January 2008),
        1-13. DOI=10.1017/S0956796807006326
-       http://dx.doi.org/10.1017/S0956796807006326
+       https://dx.doi.org/10.1017/S0956796807006326

docs/source/tutorial/introduction.rst

@@ -6,7 +6,7 @@ Introduction
 
 In conventional programming languages, there is a clear distinction
 between *types* and *values*. For example, in `Haskell
-<http://www.haskell.org>`_, the following are types, representing
+<https://www.haskell.org>`_, the following are types, representing
 integers, characters, lists of characters, and lists of any value
 respectively:
 
@@ -49,7 +49,7 @@ Intended Audience
 
 This tutorial is intended as a brief introduction to the language, and
 is aimed at readers already familiar with a functional language such
-as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
+as `Haskell <https://www.haskell.org>`_ or `OCaml <https://ocaml.org>`_.
 In particular, a certain amount of familiarity with Haskell syntax is
 assumed, although most concepts will at least be explained
 briefly. The reader is also assumed to have some interest in using

docs/source/tutorial/miscellany.rst

@@ -136,7 +136,7 @@ But what about the type of ``Type``? If we ask Idris it reports:
     Type : Type 1
 
 If ``Type`` were its own type, it would lead to an inconsistency due to
-`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
+`Girard’s paradox <https://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
 so internally there is a *hierarchy* of types (or *universes*):
 
 .. code-block:: idris

docs/source/tutorial/starting.rst

@@ -40,9 +40,11 @@ follows::
 
     make bootstrap-racket
 
-This will, by default, install into ``${HOME}/.idris2``. You can change this
-by editing the options in ``config.mk``. For example,
-to install into ``/usr/local``, you can edit the ``PREFIX`` as follows::
+Once you've successfully bootstrapped with any of the above commands, you can
+install with the command ``make install``.  This will, by default, install into
+``${HOME}/.idris2``. You can change this by editing the options in
+``config.mk``. For example, to install into ``/usr/local``, you can edit the
+``PREFIX`` as follows::
 
     PREFIX ?= /usr/local
 

docs/source/tutorial/theorems.rst

@@ -456,4 +456,4 @@ argument.
        control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
        symposium on Principles of programming languages (POPL
        '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
-       http://doi.acm.org/10.1145/96709.96714
+       https://doi.acm.org/10.1145/96709.96714

docs/source/typedd/typedd.rst

@@ -312,6 +312,9 @@ In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also
 since export rules are per-namespace now, rather than per-file, you need to
 export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
 
+In ``ArithCmdDo.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO``
+also have to be ``export``.
+
 In ``StreamFail.idr``, add a ``partial`` annotation to ``labelWith``.
 
 Chapter 12
@@ -322,6 +325,9 @@ Also the ``(>>=)`` operators need to be set as ``export`` since they are in thei
 own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional
 arguments ``div`` and ``rem``.
 
+In ``ArithState.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO``
+also have to be ``export``.
+
 Chapter 13
 ----------
 

docs/source/updates/updates.rst

@@ -334,6 +334,9 @@ There are several ``%language`` pragmas in Idris 1, which define various
 experimental extensions. None of these are available in Idris 2, although
 extensions may be defined in the future.
 
+Also removed was the ``%access`` pragma for default visibility, use visibility
+modifiers on each declaration instead.
+
 ``let`` bindings
 ----------------
 

idris2.ipkg

@@ -39,7 +39,7 @@ modules =
     Core.Normalise,
     Core.Options,
     Core.Primitives,
---     Core.Reflect,
+    Core.Reflect,
     Core.Termination,
     Core.Transform,
     Core.TT,
@@ -118,9 +118,10 @@ modules =
     TTImp.Elab.Lazy,
     TTImp.Elab.Local,
     TTImp.Elab.Prim,
---     TTImp.Elab.Quote,
+    TTImp.Elab.Quote,
     TTImp.Elab.Record,
     TTImp.Elab.Rewrite,
+    TTImp.Elab.RunElab,
     TTImp.Elab.Term,
     TTImp.Elab.Utils,
     TTImp.Impossible,
@@ -135,9 +136,10 @@ modules =
     TTImp.ProcessDef,
     TTImp.ProcessParams,
     TTImp.ProcessRecord,
+    TTImp.ProcessRunElab,
     TTImp.ProcessTransform,
     TTImp.ProcessType,
---     TTImp.Reflect,
+    TTImp.Reflect,
     TTImp.TTImp,
     TTImp.Unelab,
     TTImp.Utils,
@@ -148,6 +150,7 @@ modules =
     Utils.Octal,
     Utils.Shunting,
     Utils.String,
+    Utils.Path,
 
     Yaffle.Main,
     Yaffle.REPL

idris2api.ipkg

@@ -39,7 +39,7 @@ modules =
     Core.Normalise,
     Core.Options,
     Core.Primitives,
---     Core.Reflect,
+    Core.Reflect,
     Core.Termination,
     Core.Transform,
     Core.TT,
@@ -118,7 +118,7 @@ modules =
     TTImp.Elab.Lazy,
     TTImp.Elab.Local,
     TTImp.Elab.Prim,
---     TTImp.Elab.Quote,
+    TTImp.Elab.Quote,
     TTImp.Elab.Record,
     TTImp.Elab.Rewrite,
     TTImp.Elab.Term,
@@ -135,9 +135,10 @@ modules =
     TTImp.ProcessDef,
     TTImp.ProcessParams,
     TTImp.ProcessRecord,
+    TTImp.ProcessRunElab,
     TTImp.ProcessTransform,
     TTImp.ProcessType,
---     TTImp.Reflect,
+    TTImp.Reflect,
     TTImp.TTImp,
     TTImp.Unelab,
     TTImp.Utils,
@@ -148,6 +149,7 @@ modules =
     Utils.Octal,
     Utils.Shunting,
     Utils.String,
+    Utils.Path,
 
     Yaffle.Main,
     Yaffle.REPL

libs/base/Control/App.idr

@@ -58,11 +58,9 @@ data App1Res : Usage -> Type -> Type where
 PrimApp : Type -> Type
 PrimApp a = (1 x : %World) -> AppRes a
 
-export
 prim_app_pure : a -> PrimApp a
 prim_app_pure x = \w => MkAppRes x w
 
-export
 prim_app_bind : (1 act : PrimApp a) -> (1 k : a -> PrimApp b) -> PrimApp b
 prim_app_bind fn k w
     = let MkAppRes x' w' = fn w in k x' w'

libs/base/Control/App/Console.idr

@@ -4,14 +4,30 @@ import public Control.App
 
 public export
 interface Console e where
+  putChar : Char -> App {l} e ()
   putStr : String -> App {l} e ()
-  getStr : App {l} e String
+  getChar : App {l} e Char
+  getLine : App {l} e String
 
 export 
 PrimIO e => Console e where
+  putChar c = primIO $ putChar c
   putStr str = primIO $ putStr str
-  getStr = primIO $ getLine
+  getChar = primIO getChar
+  getLine = primIO getLine
 
 export
 putStrLn : Console e => String -> App {l} e ()
 putStrLn str = putStr (str ++ "\n")
+
+export
+putCharLn : Console e => Char -> App {l} e ()
+putCharLn c = putStrLn $ strCons c ""
+
+export
+print : (Console e, Show a) => a -> App {l} e ()
+print x = putStr $ show x
+
+export
+printLn : (Console e, Show a) => a -> App {l} e ()
+printLn x = putStrLn $ show x

libs/base/Data/Buffer.idr

@@ -32,6 +32,8 @@ freeBuffer buf = pure ()
 
 %foreign "scheme:blodwen-buffer-setbyte"
 prim__setByte : Buffer -> Int -> Int -> PrimIO ()
+%foreign "scheme:blodwen-buffer-setbyte"
+prim__setBits8 : Buffer -> Int -> Bits8 -> PrimIO ()
 
 -- Assumes val is in the range 0-255
 export
@@ -39,14 +41,74 @@ setByte : Buffer -> (loc : Int) -> (val : Int) -> IO ()
 setByte buf loc val
     = primIO (prim__setByte buf loc val)
 
+export
+setBits8 : Buffer -> (loc : Int) -> (val : Bits8) -> IO ()
+setBits8 buf loc val
+    = primIO (prim__setBits8 buf loc val)
+
 %foreign "scheme:blodwen-buffer-getbyte"
 prim__getByte : Buffer -> Int -> PrimIO Int
+%foreign "scheme:blodwen-buffer-getbyte"
+prim__getBits8 : Buffer -> Int -> PrimIO Bits8
 
 export
 getByte : Buffer -> (loc : Int) -> IO Int
 getByte buf loc
     = primIO (prim__getByte buf loc)
 
+export
+getBits8 : Buffer -> (loc : Int) -> IO Bits8
+getBits8 buf loc
+    = primIO (prim__getBits8 buf loc)
+
+%foreign "scheme:blodwen-buffer-setbits16"
+prim__setBits16 : Buffer -> Int -> Bits16 -> PrimIO ()
+
+export
+setBits16 : Buffer -> (loc : Int) -> (val : Bits16) -> IO ()
+setBits16 buf loc val
+    = primIO (prim__setBits16 buf loc val)
+
+%foreign "scheme:blodwen-buffer-getbits16"
+prim__getBits16 : Buffer -> Int -> PrimIO Bits16
+
+export
+getBits16 : Buffer -> (loc : Int) -> IO Bits16
+getBits16 buf loc
+    = primIO (prim__getBits16 buf loc)
+
+%foreign "scheme:blodwen-buffer-setbits32"
+prim__setBits32 : Buffer -> Int -> Bits32 -> PrimIO ()
+
+export
+setBits32 : Buffer -> (loc : Int) -> (val : Bits32) -> IO ()
+setBits32 buf loc val
+    = primIO (prim__setBits32 buf loc val)
+
+%foreign "scheme:blodwen-buffer-getbits32"
+prim__getBits32 : Buffer -> Int -> PrimIO Bits32
+
+export
+getBits32 : Buffer -> (loc : Int) -> IO Bits32
+getBits32 buf loc
+    = primIO (prim__getBits32 buf loc)
+
+%foreign "scheme:blodwen-buffer-setbits64"
+prim__setBits64 : Buffer -> Int -> Bits64 -> PrimIO ()
+
+export
+setBits64 : Buffer -> (loc : Int) -> (val : Bits64) -> IO ()
+setBits64 buf loc val
+    = primIO (prim__setBits64 buf loc val)
+
+%foreign "scheme:blodwen-buffer-getbits64"
+prim__getBits64 : Buffer -> Int -> PrimIO Bits64
+
+export
+getBits64 : Buffer -> (loc : Int) -> IO Bits64
+getBits64 buf loc
+    = primIO (prim__getBits64 buf loc)
+
 %foreign "scheme:blodwen-buffer-setint32"
 prim__setInt32 : Buffer -> Int -> Int -> PrimIO ()
 

libs/base/Data/IOArray.idr

@@ -15,9 +15,13 @@ data ArrayData : Type -> Type where
 export
 record IOArray elem where
   constructor MkIOArray
-  max : Int
+  maxSize : Int
   content : ArrayData (Maybe elem)
 
+export
+max : IOArray elem -> Int
+max = maxSize
+
 export
 newArray : Int -> IO (IOArray elem)
 newArray size

libs/base/Data/IORef.idr

@@ -18,10 +18,12 @@ newIORef val
     = do m <- primIO (prim__newIORef val)
          pure (MkRef m)
 
+%inline
 export
 readIORef : IORef a -> IO a
 readIORef (MkRef m) = primIO (prim__readIORef m)
 
+%inline
 export
 writeIORef : IORef a -> (1 val : a) -> IO ()
 writeIORef (MkRef m) val = primIO (prim__writeIORef m val)

libs/base/Data/List.idr

@@ -12,6 +12,10 @@ isCons : List a -> Bool
 isCons []      = False
 isCons (x::xs) = True
 
+public export
+snoc : List a -> a -> List a
+snoc xs x = xs ++ [x]
+
 public export
 length : List a -> Nat
 length []      = Z
@@ -56,6 +60,12 @@ filter p (x :: xs)
         then x :: filter p xs
         else filter p xs
 
+||| Find the first element of the list that satisfies the predicate.
+public export
+find : (p : a -> Bool) -> (xs : List a) -> Maybe a
+find p [] = Nothing
+find p (x::xs) = if p x then Just x else find p xs
+
 ||| Find associated information in a list using a custom comparison.
 public export
 lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
@@ -561,35 +571,7 @@ Uninhabited ([] = Prelude.(::) x xs) where
 export
 Uninhabited (Prelude.(::) x xs = []) where
   uninhabited Refl impossible
---
--- ||| (::) is injective
--- consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
---                 (x :: xs) = (y :: ys) -> (x = y, xs = ys)
--- consInjective Refl = (Refl, Refl)
---
--- ||| Two lists are equal, if their heads are equal and their tails are equal.
--- consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
---             x = y -> xs = ys -> x :: xs = y :: ys
--- consCong2 Refl Refl = Refl
---
--- ||| Appending pairwise equal lists gives equal lists
--- appendCong2 : {x1 : List a} -> {x2 : List a} ->
---               {y1 : List b} -> {y2 : List b} ->
---               x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2
--- appendCong2 {x1=[]} {y1=(_ :: _)} Refl _ impossible
--- appendCong2 {x1=(_ :: _)} {y1=[]} Refl _ impossible
--- appendCong2 {x1=[]} {y1=[]} _ eq2 = eq2
--- appendCong2 {x1=(_ :: _)} {y1=(_ :: _)} eq1 eq2 =
---   consCong2
---     (fst $ consInjective eq1)
---     (appendCong2 (snd $ consInjective eq1) eq2)
---
--- ||| List.map is distributive over appending.
--- mapAppendDistributive : (f : a -> b) -> (x : List a) -> (y : List a) ->
---                         map f (x ++ y) = map f x ++ map f y
--- mapAppendDistributive _ [] _ = Refl
--- mapAppendDistributive f (_ :: xs) y = cong $ mapAppendDistributive f xs y
---
+
 ||| The empty list is a right identity for append.
 export
 appendNilRightNeutral : (l : List a) ->

libs/base/Language/Reflection.idr

@@ -3,12 +3,40 @@ module Language.Reflection
 import public Language.Reflection.TT
 import public Language.Reflection.TTImp
 
-public export
+-- Elaboration scripts. Where types/terms are returned, binders will have
+-- unique, if not necessarily human readabe, names
+export
 data Elab : Type -> Type where
      Pure : a -> Elab a
      Bind : Elab a -> (a -> Elab b) -> Elab b
+     Fail : String -> Elab a
 
-     Check : TTImp -> Elab a
+     LogMsg : Nat -> String -> Elab ()
+     LogTerm : Nat -> String -> TTImp -> Elab ()
+
+     -- Elaborate a TTImp term to a concrete value
+     Check : {expected : Type} -> TTImp -> Elab expected
+     -- Quote a concrete expression back to a TTImp
+     Quote : val -> Elab TTImp
+     -- Get the current goal type, if known 
+     -- (it might need to be inferred from the solution)
+     Goal : Elab (Maybe TTImp)
+     -- Get the names of local variables in scope
+     LocalVars : Elab (List Name)
+     -- Generate a new unique name, based on the given string
+     GenSym : String -> Elab Name
+     -- Put a name in the current namespace
+     InCurrentNS : Name -> Elab Name
+     -- Get the types of every name which matches.
+     -- There may be ambiguities - returns a list of fully explicit names
+     -- and their types. If there's no results, the name is undefined.
+     GetType : Name -> Elab (List (Name, TTImp))
+     -- Get the type of a local variable
+     GetLocalType : Name -> Elab TTImp
+     -- Get the constructors of a data type. The name must be fully resolved.
+     GetCons : Name -> Elab (List Name)
+     -- Check a group of top level declarations
+     Declare : List Decl -> Elab ()
 
 mutual
   export
@@ -26,3 +54,63 @@ mutual
   export
   Monad Elab where
     (>>=) = Bind
+
+export
+fail : String -> Elab a
+fail = Fail
+
+export
+logMsg : Nat -> String -> Elab ()
+logMsg = LogMsg
+
+export
+logTerm : Nat -> String -> TTImp -> Elab ()
+logTerm = LogTerm
+
+export
+logGoal : Nat -> String -> Elab ()
+logGoal n msg
+    = do g <- Goal
+         case g of
+              Nothing => pure ()
+              Just t => logTerm n msg t
+
+export
+check : {expected : Type} -> TTImp -> Elab expected
+check = Check
+
+export
+quote : val -> Elab TTImp
+quote = Quote
+
+export
+goal : Elab (Maybe TTImp)
+goal = Goal
+
+export
+localVars : Elab (List Name)
+localVars = LocalVars
+
+export
+genSym : String -> Elab Name
+genSym = GenSym
+
+export
+inCurrentNS : Name -> Elab Name
+inCurrentNS = InCurrentNS
+
+export
+getType : Name -> Elab (List (Name, TTImp))
+getType = GetType
+
+export
+getLocalType : Name -> Elab TTImp
+getLocalType = GetLocalType
+
+export
+getCons : Name -> Elab (List Name)
+getCons = GetCons
+
+export
+declare : List Decl -> Elab ()
+declare = Declare

libs/base/Language/Reflection/TT.idr

@@ -1,5 +1,7 @@
 module Language.Reflection.TT
 
+import public Data.List
+
 public export
 FilePos : Type
 FilePos = (Int, Int)
@@ -24,6 +26,10 @@ public export
 data Constant
     = I Int
     | BI Integer
+    | B8 Int
+    | B16 Int
+    | B32 Int
+    | B64 Integer
     | Str String
     | Ch Char
     | Db Double
@@ -31,6 +37,10 @@ data Constant
 
     | IntType
     | IntegerType
+    | Bits8Type
+    | Bits16Type
+    | Bits32Type
+    | Bits64Type
     | StringType
     | CharType
     | DoubleType
@@ -41,11 +51,22 @@ data Name = UN String
           | MN String Int
           | NS (List String) Name
 
+export
+Show Name where
+  show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n
+    where
+      showSep : String -> List String -> String
+      showSep sep [] = ""
+      showSep sep [x] = x
+      showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
+  show (UN x) = x
+  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
+
 public export
 data Count = M0 | M1 | MW
 
 public export
-data PiInfo = ImplicitArg | ExplicitArg | AutoImplicit
+data PiInfo t = ImplicitArg | ExplicitArg | AutoImplicit | DefImplicit t
 
 public export
 data IsVar : Name -> Nat -> List Name -> Type where
@@ -55,25 +76,32 @@ data IsVar : Name -> Nat -> List Name -> Type where
 public export
 data LazyReason = LInf | LLazy | LUnknown
 
+export
+data TT : Type where [external]
+
+{-
 -- Type checked terms in the core TT
 public export
 data TT : List Name -> Type where
-     Local : FC -> (idx : Nat) -> (n : Name) ->
-             (0 prf : IsVar name idx vars) -> TT vars
+     Local : FC -> (idx : Nat) -> (0 prf : IsVar name idx vars) -> TT vars
      Ref : FC -> NameType -> Name -> TT vars
-     Pi : FC -> Count -> PiInfo ->
+     Pi : FC -> Count -> PiInfo (TT vars) ->
           (x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->
           TT vars
-     Lam : FC -> Count -> PiInfo ->
+     Lam : FC -> Count -> PiInfo (TT vars) ->
            (x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->
            TT vars
      App : FC -> TT vars -> TT vars -> TT vars
      TDelayed : FC -> LazyReason -> TT vars -> TT vars
      TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars
-     TForce : FC -> TT vars -> TT vars
+     TForce : FC -> LazyReason -> TT vars -> TT vars
      PrimVal : FC -> Constant -> TT vars
      Erased : FC -> TT vars
      TType : FC -> TT vars
+     -}
+
+public export
+data TotalReq = Total | CoveringOnly | PartialOK
 
 public export
 data Visibility = Private | Export | Public

libs/base/Language/Reflection/TTImp.idr

@@ -1,6 +1,6 @@
 module Language.Reflection.TTImp
 
-import Language.Reflection.TT
+import public Language.Reflection.TT
 
 -- Unchecked terms and declarations in the intermediate language
 mutual
@@ -23,9 +23,9 @@ mutual
   public export
   data TTImp : Type where
        IVar : FC -> Name -> TTImp
-       IPi : FC -> Count -> PiInfo -> Maybe Name ->
+       IPi : FC -> Count -> PiInfo TTImp -> Maybe Name ->
              (argTy : TTImp) -> (retTy : TTImp) -> TTImp
-       ILam : FC -> Count -> PiInfo -> Maybe Name ->
+       ILam : FC -> Count -> PiInfo TTImp -> Maybe Name ->
               (argTy : TTImp) -> (lamTy : TTImp) -> TTImp
        ILet : FC -> Count -> Name ->
               (nTy : TTImp) -> (nVal : TTImp) ->
@@ -61,6 +61,7 @@ mutual
 
        -- Quasiquotation
        IQuote : FC -> TTImp -> TTImp
+       IQuoteName : FC -> Name -> TTImp
        IQuoteDecl : FC -> TTImp -> TTImp
        IUnquote : FC -> TTImp -> TTImp
 
@@ -72,6 +73,7 @@ mutual
        -- bound (either as a pattern variable or a type variable) if unsolved
        -- at the end of elaborator
        Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
+       IWithUnambigNames : FC -> List Name -> TTImp -> TTImp
 
   public export
   data IFieldUpdate : Type where
@@ -87,6 +89,7 @@ mutual
   public export
   data FnOpt : Type where
        Inline : FnOpt
+       TCInline : FnOpt
        -- Flag means the hint is a direct hint, not a function which might
        -- find the result (e.g. chasing parent interface dictionaries)
        Hint : Bool -> FnOpt
@@ -97,10 +100,9 @@ mutual
        ForeignFn : List String -> FnOpt
        -- assume safe to cancel arguments in unification
        Invertible : FnOpt
-       Total : FnOpt
-       Covering : FnOpt
-       PartialOK : FnOpt
+       Totalty : TotalReq -> FnOpt
        Macro : FnOpt
+       SpecArgs : List Name -> FnOpt
 
   public export
   data ITy : Type where
@@ -111,6 +113,8 @@ mutual
        SearchBy : List Name -> DataOpt -- determining arguments
        NoHints : DataOpt -- Don't generate search hints for constructors
        UniqueSearch : DataOpt
+       External : DataOpt
+       NoNewtype : DataOpt
 
   public export
   data Data : Type where
@@ -121,7 +125,7 @@ mutual
 
   public export
   data IField : Type where
-       MkIField : FC -> Count -> PiInfo -> Name -> TTImp ->
+       MkIField : FC -> Count -> PiInfo TTImp -> Name -> TTImp ->
                   IField
 
   public export
@@ -148,10 +152,6 @@ mutual
        IParameters : FC -> List (Name, TTImp) ->
                      List Decl -> Decl
        IRecord : FC -> Visibility -> Record -> Decl
-       INamespace : FC ->
-                    (nested : Bool) ->
-                      -- ^ if True, parent namespaces in the same file can also
-                      -- look inside and see private/export names in full
-                    List String -> List Decl -> Decl
-       ITransform : FC -> TTImp -> TTImp -> Decl
+       INamespace : FC -> List String -> List Decl -> Decl
+       ITransform : FC -> Name -> TTImp -> TTImp -> Decl
        ILog : Nat -> Decl

libs/base/System/Clock.idr

@@ -69,6 +69,7 @@ data OSClock : Type where [external]
 
 ||| Note: Back-ends are required to implement UTC, monotonic time, CPU time
 ||| in current process/thread, and time duration; the rest are optional.
+export
 data ClockTypeMandatory
   = Mandatory
   | Optional

libs/base/System/File.idr

@@ -38,6 +38,10 @@ prim__writeLine : FilePtr -> String -> PrimIO Int
 prim__eof : FilePtr -> PrimIO Int
 %foreign "C:fflush,libc 6"
 prim__flush : FilePtr -> PrimIO Int
+%foreign support "idris2_popen"
+prim__popen : String -> String -> PrimIO FilePtr
+%foreign support "idris2_pclose"
+prim__pclose : FilePtr -> PrimIO ()
 
 %foreign support "idris2_removeFile"
 prim__removeFile : String -> PrimIO Int
@@ -185,6 +189,18 @@ fflush (FHandle f)
     = do primIO (prim__flush f)
          pure ()
 
+export
+popen : String -> Mode -> IO (Either FileError File)
+popen f m = do
+    ptr <- primIO (prim__popen f (modeStr m))
+    if prim__nullAnyPtr ptr /= 0
+        then returnError
+        else pure (Right (FHandle ptr))
+
+export
+pclose : File -> IO ()
+pclose (FHandle h) = primIO (prim__pclose h)
+
 export
 fileAccessTime : (h : File) -> IO (Either FileError Int)
 fileAccessTime (FHandle f)

libs/base/System/Info.idr

@@ -10,3 +10,7 @@ os = prim__os
 export
 codegen : String
 codegen = prim__codegen
+
+export
+isWindows : Bool
+isWindows = os `elem` ["windows", "mingw32", "cygwin32"]

libs/contrib/Data/List/Equalities.idr

@@ -0,0 +1,77 @@
+module Data.List.Equalities
+
+import Data.List
+
+%default total
+
+||| A list constructued using snoc cannot be empty.
+export
+snocNonEmpty : {x : a} -> {xs : List a} -> xs ++ [x] = [] -> Void
+snocNonEmpty {xs = []} prf = uninhabited prf
+snocNonEmpty {xs = y :: ys} prf = uninhabited prf
+
+||| (::) is injective
+export
+consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
+                (x :: xs) = (y :: ys) -> (x = y, xs = ys)
+consInjective Refl = (Refl, Refl)
+
+||| Two lists are equal, if their heads are equal and their tails are equal.
+export
+consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
+            x = y -> xs = ys -> x :: xs = y :: ys
+consCong2 Refl Refl = Refl
+
+||| Equal non-empty lists should result in equal components after destructuring 'snoc'.
+export
+snocCong2 : {x : a} -> {xs : List a} -> {y : a} -> {ys : List a} ->
+            (xs `snoc` x) = (ys `snoc` y) -> (xs = ys, x = y)
+snocCong2 {xs = []} {ys = []} Refl = (Refl, Refl)
+snocCong2 {xs = []} {ys = z :: zs} prf =
+  let nilIsSnoc = snd $ consInjective {xs = []} {ys = zs ++ [y]} prf
+   in void $ snocNonEmpty (sym nilIsSnoc)
+snocCong2 {xs = z :: xs} {ys = []} prf =
+  let snocIsNil = snd $ consInjective {x = z} {xs = xs ++ [x]} {ys = []} prf
+   in void $ snocNonEmpty snocIsNil
+snocCong2 {xs = w :: xs} {ys = z :: ys} prf =
+  let (wEqualsZ, xsSnocXEqualsYsSnocY) = consInjective prf
+      (xsEqualsYS, xEqualsY) = snocCong2 xsSnocXEqualsYsSnocY
+   in (consCong2 wEqualsZ xsEqualsYS, xEqualsY)
+
+||| Appending pairwise equal lists gives equal lists
+export
+appendCong2 : {x1 : List a} -> {x2 : List a} ->
+              {y1 : List b} -> {y2 : List b} ->
+              x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2
+appendCong2 {x1=[]} {y1=(_ :: _)} Refl _ impossible
+appendCong2 {x1=(_ :: _)} {y1=[]} Refl _ impossible
+appendCong2 {x1=[]} {y1=[]} _ eq2 = eq2
+appendCong2 {x1=(_ :: _)} {y1=(_ :: _)} eq1 eq2 =
+  let (hdEqual, tlEqual) = consInjective eq1
+   in consCong2 hdEqual (appendCong2 tlEqual eq2)
+
+||| List.map is distributive over appending.
+export
+mapDistributesOverAppend
+  : (f : a -> b)
+  -> (xs : List a)
+  -> (ys : List a)
+  -> map f (xs ++ ys) = map f xs ++ map f ys
+mapDistributesOverAppend _ [] _ = Refl
+mapDistributesOverAppend f (x :: xs) ys =
+  cong (f x ::) $ mapDistributesOverAppend f xs ys
+
+||| List.length is distributive over appending.
+export
+lengthDistributesOverAppend
+  : (xs, ys : List a)
+  -> length (xs ++ ys) = length xs + length ys
+lengthDistributesOverAppend [] ys = Refl
+lengthDistributesOverAppend (x :: xs) ys =
+  cong S $ lengthDistributesOverAppend xs ys
+
+||| Length of a snoc'd list is the same as Succ of length list.
+export
+lengthSnoc : (x : _) -> (xs : List a) -> length (snoc xs x) = S (length xs)
+lengthSnoc x [] = Refl
+lengthSnoc x (_ :: xs) = cong S (lengthSnoc x xs)

libs/contrib/Data/List/Palindrome.idr

@@ -0,0 +1,60 @@
+module Data.List.Palindrome
+
+import Data.List
+import Data.List.Views
+import Data.List.Views.Extra
+import Data.List.Reverse
+import Data.List.Equalities
+
+%hide Prelude.reverse
+%default total
+
+||| Do geese see God?
+public export
+data Palindrome : (xs : List a) -> Type where
+  Empty  : Palindrome []
+  Single : Palindrome [_]
+  Multi  : Palindrome xs -> Palindrome (x :: (xs `snoc` x))
+
+||| A Palindrome reversed is itself.
+export
+palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
+palindromeReverse [] Empty = Refl
+palindromeReverse [_] Single = Refl
+palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =
+  rewrite reverseAppend ([x] ++ ys) [x] in
+    rewrite reverseAppend [x] ys in
+      rewrite palindromeReverse ys pf in
+        Refl
+
+private
+reversePalindromeEqualsLemma
+  : (x, x' : a)
+  -> (xs : List a)
+  -> reverse (x :: (xs ++ [x'])) = (x :: (xs ++ [x']))
+  -> (reverse xs = xs, x = x')
+reversePalindromeEqualsLemma x x' xs prf = equateInnerAndOuter flipHeadX
+  where
+    flipHeadX : reverse (xs ++ [x']) ++ [x] = x :: (xs ++ [x'])
+    flipHeadX = rewrite (sym (reverseCons x (xs ++ [x']))) in prf
+    flipLastX' : reverse (xs ++ [x']) = x :: xs -> (x' :: reverse xs) = (x :: xs)
+    flipLastX' prf = rewrite (sym $ reverseAppend xs [x']) in prf
+    cancelOuter : (reverse (xs ++ [x'])) = x :: xs -> reverse xs = xs
+    cancelOuter prf = snd (consInjective (flipLastX' prf))
+    equateInnerAndOuter
+      : reverse (xs ++ [x']) ++ [x] = (x :: xs) ++ [x']
+      -> (reverse xs = xs, x = x')
+    equateInnerAndOuter prf =
+      let (prf', xEqualsX') = snocCong2 prf
+       in (cancelOuter prf', xEqualsX')
+
+||| Only Palindromes are equal to their own reverse.
+export
+reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs
+reversePalindrome input prf with (vList input)
+  reversePalindrome [] _ | VNil = Empty
+  reversePalindrome [x] _ | VOne = Single
+  reversePalindrome (x :: (inner `snoc` y)) prf | VCons rec with (reversePalindromeEqualsLemma x y inner prf)
+    reversePalindrome (x :: (inner `snoc` y)) prf | VCons rec | (revInnerIsIdentical, xIsY) =
+      rewrite xIsY in
+        Multi $ reversePalindrome inner revInnerIsIdentical | Force rec

libs/contrib/Data/List/Reverse.idr

@@ -0,0 +1,94 @@
+||| Properties of the reverse function.
+module Data.List.Reverse
+
+import Data.Nat
+import Data.List
+import Data.List.Equalities
+
+%default total
+
+export
+reverseOntoAcc : (xs, ys, zs : List a) ->
+  reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs
+reverseOntoAcc [] _ _ = Refl
+reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs
+
+||| Serves as a specification for reverseOnto.
+export
+reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
+reverseOntoSpec xs ys = reverseOntoAcc ys [] xs
+
+||| The reverse of an empty list is an empty list.  Together with reverseCons,
+||| serves as a specification for reverse.
+export
+reverseNil : reverse [] = []
+reverseNil = Refl
+
+||| The reverse of a cons is the reverse of the tail followed by the head.
+||| Together with reverseNil serves as a specification for reverse.
+export
+reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs `snoc` x
+reverseCons x xs = reverseOntoSpec [x] xs
+
+||| Reversing an append is appending reversals backwards.
+export
+reverseAppend : (xs, ys : List a) ->
+  reverse (xs ++ ys) = reverse ys ++ reverse xs
+reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
+reverseAppend (x :: xs) ys =
+  rewrite reverseCons x (xs ++ ys) in
+    rewrite reverseAppend xs ys in
+      rewrite reverseCons x xs in
+        sym $ appendAssociative (reverse ys) (reverse xs) [x]
+
+||| A slow recursive definition of reverse.
+public export
+0 slowReverse : List a -> List a
+slowReverse [] = []
+slowReverse (x :: xs) = slowReverse xs `snoc` x
+
+||| The iterative and recursive defintions of reverse are the same.
+export
+reverseEquiv : (xs : List a) -> slowReverse xs = reverse xs
+reverseEquiv [] = Refl
+reverseEquiv (x :: xs) =
+  rewrite reverseEquiv xs in
+    rewrite reverseAppend [x] xs in
+      Refl
+
+||| Reversing a singleton list is a no-op.
+export
+reverseSingletonId : (x : a) -> reverse [x] = [x]
+reverseSingletonId _ = Refl
+
+||| Reversing a reverse gives the original.
+export
+reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
+reverseReverseId [] = Refl
+reverseReverseId (x :: xs) =
+  rewrite reverseCons x xs in
+    rewrite reverseAppend (reverse xs) [x] in
+      rewrite reverseReverseId xs in
+        Refl
+
+||| Reversing onto preserves list length.
+export
+reverseOntoLength : (xs, acc : List a) ->
+  length (reverseOnto acc xs) = length acc + length xs
+reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl
+reverseOntoLength (x :: xs) acc =
+  rewrite reverseOntoLength xs (x :: acc) in
+    plusSuccRightSucc (length acc) (length xs)
+
+||| Reversing preserves list length.
+export
+reverseLength : (xs : List a) -> length (reverse xs) = length xs
+reverseLength xs = reverseOntoLength xs []
+
+||| Equal reversed lists are equal.
+export
+reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys
+reverseEqual xs ys prf =
+  rewrite sym $ reverseReverseId xs in
+    rewrite prf in
+      reverseReverseId ys

libs/contrib/Data/List/Views/Extra.idr

@@ -0,0 +1,173 @@
+module Data.List.Views.Extra
+
+import Data.List
+import Data.List.Reverse
+import Data.List.Views
+import Data.Nat
+import Data.List.Equalities
+
+%default total
+
+||| Proof that two numbers differ by at most one
+public export
+data Balanced : Nat -> Nat -> Type where
+  BalancedZ   : Balanced Z Z
+  BalancedL   : Balanced (S Z) Z
+  BalancedRec : Balanced n m -> Balanced (S n) (S m)
+
+%name Balanced bal, b
+
+Uninhabited (Balanced Z (S k)) where
+  uninhabited BalancedZ impossible
+  uninhabited BalancedL impossible
+  uninhabited (BalancedRec rec) impossible
+
+export
+balancedPred : Balanced (S x) (S y) -> Balanced x y
+balancedPred (BalancedRec pred) = pred
+
+export
+mkBalancedEq : {n, m : Nat} -> n = m -> Balanced n m
+mkBalancedEq {n = 0} Refl = BalancedZ
+mkBalancedEq {n = (S k)} Refl = BalancedRec $ mkBalancedEq {n = k} Refl
+
+export
+mkBalancedL : {n, m : Nat} -> n = S m -> Balanced n m
+mkBalancedL {m = 0} Refl = BalancedL
+mkBalancedL {m = S k} Refl = BalancedRec (mkBalancedL Refl)
+
+||| View of a list split into two halves
+|||
+||| The lengths of the lists are guaranteed to differ by at most one
+public export
+data SplitBalanced : List a -> Type where
+  MkSplitBal
+    : {xs, ys : List a}
+    -> Balanced (length xs) (length ys)
+    -> SplitBalanced (xs ++ ys)
+
+private
+splitBalancedHelper
+  : (revLs : List a)
+  -> (rs : List a)
+  -> (doubleSkip : List a)
+  -> (length rs = length revLs + length doubleSkip)
+  -> SplitBalanced (reverse revLs ++ rs)
+splitBalancedHelper revLs rs [] prf = MkSplitBal balancedLeftsAndRights
+  where
+    lengthsEqual : length rs = length revLs
+    lengthsEqual =
+      rewrite sym (plusZeroRightNeutral (length revLs)) in prf
+    balancedLeftsAndRights : Balanced (length (reverse revLs)) (length rs)
+    balancedLeftsAndRights =
+      rewrite reverseLength revLs in
+        rewrite lengthsEqual in
+          mkBalancedEq Refl
+splitBalancedHelper revLs [] (x :: xs) prf =
+  absurd $
+    the (0 = S (plus (length revLs) (length xs)))
+      rewrite plusSuccRightSucc (length revLs) (length xs) in
+        prf
+splitBalancedHelper revLs (x :: rs) [lastItem] prf =
+  rewrite appendAssociative (reverse revLs) [x] rs in
+    rewrite sym (reverseCons x revLs) in
+      MkSplitBal $
+        the (Balanced (length (reverseOnto [x] revLs)) (length rs)) $
+          rewrite reverseCons x revLs in
+            rewrite lengthSnoc x (reverse revLs) in
+              rewrite reverseLength revLs in
+                rewrite lengthsEqual in
+                  mkBalancedL Refl
+  where
+    lengthsEqual : length rs = length revLs
+    lengthsEqual =
+      cong pred $
+        the (S (length rs) = S (length revLs)) $
+          rewrite plusCommutative 1 (length revLs) in prf
+splitBalancedHelper revLs (x :: oneFurther) (_ :: (_ :: twoFurther)) prf =
+  rewrite appendAssociative (reverse revLs) [x] oneFurther in
+    rewrite sym (reverseCons x revLs) in
+      splitBalancedHelper (x :: revLs) oneFurther twoFurther $
+        cong pred $
+          the (S (length oneFurther) = S (S (plus (length revLs) (length twoFurther)))) $
+          rewrite plusSuccRightSucc (length revLs) (length twoFurther) in
+            rewrite plusSuccRightSucc (length revLs) (S (length twoFurther)) in
+              prf
+
+||| Covering function for the `SplitBalanced`
+|||
+||| Constructs the view in linear time
+export
+splitBalanced : (input : List a) -> SplitBalanced input
+splitBalanced input = splitBalancedHelper [] input input Refl
+
+||| The `VList` view allows us to recurse on the middle of a list,
+||| inspecting the front and back elements simultaneously.
+public export
+data VList : List a -> Type where
+  VNil : VList []
+  VOne : VList [x]
+  VCons : {x, y : a} -> {xs : List a} -> (rec : Lazy (VList xs)) -> VList (x :: xs ++ [y])
+
+private
+toVList
+  : (xs : List a)
+  -> SnocList ys
+  -> Balanced (length xs) (length ys)
+  -> VList (xs ++ ys)
+toVList [] Empty BalancedZ = VNil
+toVList [x] Empty BalancedL = VOne
+toVList [] (Snoc x zs rec) prf =
+  absurd $
+    the (Balanced 0 (S (length zs))) $
+      rewrite sym (lengthSnoc x zs) in prf
+toVList (x :: xs) (Snoc y ys srec) prf =
+  rewrite appendAssociative xs ys [y] in
+    VCons $
+      toVList xs srec $
+        balancedPred $
+          rewrite sym (lengthSnoc y ys) in prf
+
+||| Covering function for `VList`
+||| Constructs the view in linear time.
+export
+vList : (xs : List a) -> VList xs
+vList xs with (splitBalanced xs)
+  vList (ys ++ zs) | (MkSplitBal prf) = toVList ys (snocList zs) prf
+
+||| Lazy filtering of a list based on a predicate.
+public export
+data LazyFilterRec : List a -> Type where
+  Exhausted : (skip : List a) -> LazyFilterRec skip
+  Found     : (skip : List a) -- initial non-matching elements
+            -> (head : a)      -- first match
+            -> Lazy (LazyFilterRec rest)
+            -> LazyFilterRec (skip ++ (head :: rest))
+
+||| Covering function for the LazyFilterRec view.
+||| Constructs the view lazily in linear time.
+total export
+lazyFilterRec : (pred : (a -> Bool)) -> (xs : List a) -> LazyFilterRec xs
+lazyFilterRec pred [] = Exhausted []
+lazyFilterRec pred (x :: xs) with (pred x)
+  lazyFilterRec pred (x :: xs) | True = Found [] x (lazyFilterRec pred xs)
+  lazyFilterRec pred (x :: []) | False = Exhausted [x]
+  lazyFilterRec pred (x :: rest@(_ :: xs)) | False = filterHelper [x] rest
+    where
+      filterHelper
+        : (reverseOfSkipped : List a)
+        -> {auto prf1 : NonEmpty reverseOfSkipped}
+        -> (rest : List a)
+        -> {auto prf2 : NonEmpty rest}
+        -> LazyFilterRec (reverse reverseOfSkipped ++ rest)
+      filterHelper revSkipped (y :: xs) with (pred y)
+      filterHelper revSkipped (y :: xs) | True =
+        Found (reverse revSkipped) y (lazyFilterRec pred xs)
+      filterHelper revSkipped (y :: []) | False =
+        rewrite sym (reverseOntoSpec [y] revSkipped) in
+          Exhausted $ reverse (y :: revSkipped)
+      filterHelper revSkipped (y :: (z :: zs)) | False =
+        rewrite appendAssociative (reverse revSkipped) [y] (z :: zs) in
+          rewrite sym (reverseOntoSpec [y] revSkipped) in
+            filterHelper (y :: revSkipped) (z :: zs)
+

libs/contrib/Syntax/WithProof.idr

@@ -1,8 +1,9 @@
 module Syntax.WithProof
 
+prefix 10 @@
+
 ||| Until Idris2 supports the 'with (...) proof p' construct, here's a
 ||| poor-man's replacement.
-prefix 10 @@
 public export
 (@@) : (t : a ) -> (u : a ** t = u)
 (@@) x = ( x ** Refl)

libs/contrib/System/Path.idr

@@ -1,20 +1,21 @@
 module System.Path
 
-import Control.Delayed
 import Data.List
 import Data.Maybe
 import Data.Nat
 import Data.Strings
 import Data.String.Extra
+
 import System.Info
+
 import Text.Token
 import Text.Lexer
 import Text.Parser
 import Text.Quantity
 
-private
-isWindows : Bool
-isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
+infixr 5 </>
+infixr 7 <.>
+
 
 ||| The character that separates directories in the path.
 export
@@ -26,47 +27,48 @@ export
 pathSeparator : Char
 pathSeparator = if isWindows then ';' else ':'
 
-||| Windows' path prefixes.
-|||
-||| @ UNC Windows' Uniform Naming Convention, e.g., a network sharing
-|||   directory: `\\host\c$\Windows\System32`
-||| @ Disk the drive, e.g., "C:". The disk character is in upper case
+||| Windows' path prefixes of path component.
 public export
-data Volumn = UNC String String
-            | Disk Char
+data Volume
+  = 
+  ||| Windows' Uniform Naming Convention, e.g., a network sharing
+  ||| directory: `\\host\c$\Windows\System32`
+  UNC String String |
+  ||| The drive, e.g., "C:". The disk character is in upper case
+  Disk Char
 
-||| A single body of path.
-|||
-||| @ CurDir "."
-||| @ ParentDir ".."
-||| @ Normal common directory or file
+||| A single body of path component.
 public export
-data Body = CurDir
-          | ParentDir
-          | Normal String
+data Body
+  = 
+  ||| Represents "."
+  CurDir |
+  ||| Represents ".."
+  ParentDir |
+  ||| Common directory or file
+  Normal String
 
-||| A cross-platform file system path.
+||| A parsed cross-platform file system path.
 |||
-||| The function `parse` is the most common way to construct a Path
-||| from String, and the function `show` converts in reverse.
+||| The function `parse` constructs a Path component from String,
+||| and the function `show` converts in reverse.
 |||
 ||| Trailing separator is only used for display and is ignored while
 ||| comparing paths.
-|||
-||| @ volumn Windows' path prefix (only on Windows)
-||| @ hasRoot whether the path contains a root
-||| @ body path bodies
-||| @ hasTrailSep whether the path terminates with a separator
 public export
 record Path where
     constructor MkPath
-    volumn : Maybe Volumn
+    ||| Windows' path prefix (only on Windows)
+    volume : Maybe Volume
+    ||| Whether the path contains a root
     hasRoot : Bool
+    ||| Path bodies
     body : List Body
+    ||| Whether the path terminates with a separator
     hasTrailSep : Bool
 
 export
-Eq Volumn where
+Eq Volume where
   (==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2
   (==) (Disk l) (Disk r) = l == r
   (==) _ _ = False
@@ -89,175 +91,6 @@ public export
 emptyPath : Path
 emptyPath = MkPath Nothing False [] False
 
-||| Returns true if the path is absolute.
-|||
-||| - On Unix, a path is absolute if it starts with the root,
-|||   so isAbsolute and hasRoot are equivalent.
-|||
-||| - On Windows, a path is absolute if it has a volumn and starts
-|||   with the root. e.g., `c:\\windows` is absolute, while `c:temp`
-|||   and `\temp` are not. In addition, a path with UNC volumn is absolute.
-export
-isAbsolute : Path -> Bool
-isAbsolute p = if isWindows
-                 then case p.volumn of
-                           Just (UNC _ _) => True
-                           Just (Disk _) => p.hasRoot
-                           Nothing => False
-                 else p.hasRoot
-
-||| Returns true if the path is relative, i.e., not absolute.
-export
-isRelative : Path -> Bool
-isRelative = not . isAbsolute
-
-||| Appends the right path to the left one.
-|||
-||| If the path on the right is absolute, it replaces the left path.
-|||
-||| On Windows:
-|||
-||| - If the right path has a root but no volumn (e.g., `\windows`), it
-|||   replaces everything except for the volumn (if any) of left.
-||| - If the right path has a volumn but no root, it replaces left.
-|||
-||| ```idris example
-||| pure $ !(parse "/usr") `append` !(parse "local/etc")
-||| ```
-export
-append : (left : Path) -> (right : Path) -> Path
-append l r = if isAbsolute r || isJust r.volumn
-                then r
-                else if hasRoot r
-                  then record { volumn = l.volumn } r
-                  else record { body = l.body ++ r.body,
-                                hasTrailSep = r.hasTrailSep } l
-
-||| Returns the path without its final component, if there is one.
-|||
-||| Returns Nothing if the path terminates in a root or volumn.
-export
-parent : Path -> Maybe Path
-parent p = case p.body of
-                [] => Nothing
-                (x::xs) => Just $ record { body = init (x::xs),
-                                           hasTrailSep = False } p
-
-||| Returns a list of all parents of the path, longest first,
-||| self excluded.
-|||
-||| For example, the parent of the path, and the parent of the
-||| parent of the path, and so on. The list terminates in a
-||| root or volumn (if any).
-export
-parents : Path -> List Path
-parents p = drop 1 $ iterate parent p
-
-||| Determines whether base is either one of the parents of full or
-||| is identical to full.
-|||
-||| Trailing separator is ignored.
-export
-startWith : (base : Path) -> (full : Path) -> Bool
-startWith base full = base `elem` (iterate parent full)
-
-||| Returns a path that, when appended onto base, yields full.
-|||
-||| If base is not a prefix of full (i.e., startWith returns false),
-||| returns Nothing.
-stripPrefix : (base : Path) -> (full : Path) -> Maybe Path
-stripPrefix base full
-    = do let MkPath vol1 root1 body1 _ = base
-         let MkPath vol2 root2 body2 trialSep = full
-         if vol1 == vol2 && root1 == root2 then Just () else Nothing
-         body <- stripBody body1 body2
-         pure $ MkPath Nothing False body trialSep
-  where
-    stripBody : (base : List Body) -> (full : List Body) -> Maybe (List Body)
-    stripBody [] ys = Just ys
-    stripBody xs [] = Nothing
-    stripBody (x::xs) (y::ys) = if x == y then stripBody xs ys else Nothing
-
-||| Returns the final body of the path, if there is one.
-|||
-||| If the path is a normal file, this is the file name. If it's the
-||| path of a directory, this is the directory name.
-|||
-||| Returns Nothing if the final body is ".." or "."
-export
-fileName : Path -> Maybe String
-fileName p = case last' p.body of
-                  Just (Normal s) => Just s
-                  _ => Nothing
-
-private
-splitFileName : String -> (String, String)
-splitFileName name
-    = case break (== '.') $ reverse $ unpack name of
-           (_, []) => (name, "")
-           (_, ['.']) => (name, "")
-           (revExt, (dot :: revStem))
-              => ((pack $ reverse revStem), (pack $ reverse revExt))
-
-
-||| Extracts the stem (non-extension) portion of the file name of path.
-|||
-||| The stem is:
-|||
-||| - Nothing, if there is no file name;
-||| - The entire file name if there is no embedded ".";
-||| - The entire file name if the file name begins with "." and has
-|||   no other "."s within;
-||| - Otherwise, the portion of the file name before the final "."
-export
-fileStem : Path -> Maybe String
-fileStem p = pure $ fst $ splitFileName !(fileName p)
-
-||| Extracts the extension of the file name of path.
-|||
-||| The extension is:
-|||
-||| - Nothing, if there is no file name;
-||| - Nothing, if there is no embedded ".";
-||| - Nothing, if the file name begins with "." and has no other "."s within;
-||| - Otherwise, the portion of the file name after the final "."
-export
-extension : Path -> Maybe String
-extension p = pure $ snd $ splitFileName !(fileName p)
-
-||| Updates the file name of the path.
-|||
-||| If no file name, this is equivalent to appending the name;
-||| Otherwise it is equivalent to appending the name to the parent.
-export
-setFileName : (name : String) -> Path -> Path
-setFileName name p = record { body $= updateLastBody name } p
-  where
-    updateLastBody : String -> List Body -> List Body
-    updateLastBody s [] = [Normal s]
-    updateLastBody s [Normal _] = [Normal s]
-    updateLastBody s [x] = x :: [Normal s]
-    updateLastBody s (x::xs) = x :: (updateLastBody s xs)
-
-||| Updates the extension of the path.
-|||
-||| Returns Nothing if no file name.
-|||
-||| If extension is Nothing, the extension is added; otherwise it is replaced.
-export
-setExtension : (ext : String) -> Path -> Maybe Path
-setExtension ext p = do name <- fileName p
-                        let (stem, _) = splitFileName name
-                        pure $ setFileName (stem ++ "." ++ ext) p
-
-public export
-Semigroup Path where
-  (<+>) = append
-
-public export
-Monoid Path where
-  neutral = emptyPath
-
 --------------------------------------------------------------------------------
 -- Show
 --------------------------------------------------------------------------------
@@ -269,7 +102,7 @@ Show Body where
   show (Normal s) = s
 
 export
-Show Volumn where
+Show Volume where
   show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
   show (Disk disk) = singleton disk ++ ":"
 
@@ -277,30 +110,26 @@ Show Volumn where
 export
 Show Path where
   show p = let sep = singleton dirSeparator
-               volStr = fromMaybe "" (map show p.volumn)
+               volStr = fromMaybe "" (map show p.volume)
                rootStr = if p.hasRoot then sep else ""
                bodyStr = join sep $ map show p.body
                trailStr = if p.hasTrailSep then sep else "" in
-           volStr ++ rootStr ++ bodyStr ++ trailStr
+             volStr ++ rootStr ++ bodyStr ++ trailStr
 
 --------------------------------------------------------------------------------
 -- Parser
 --------------------------------------------------------------------------------
 
-private
 data PathTokenKind = PTText | PTPunct Char
 
-private
 Eq PathTokenKind where
   (==) PTText PTText = True
   (==) (PTPunct c1) (PTPunct c2) = c1 == c2
   (==) _ _ = False
 
-private
 PathToken : Type
 PathToken = Token PathTokenKind
 
-private
 TokenKind PathTokenKind where
   TokType PTText = String
   TokType (PTPunct _) = ()
@@ -308,7 +137,6 @@ TokenKind PathTokenKind where
   tokValue PTText x = x
   tokValue (PTPunct _) _ = ()
 
-private
 pathTokenMap : TokenMap PathToken
 pathTokenMap = toTokenMap $
   [ (is '/', PTPunct '/')
@@ -318,18 +146,11 @@ pathTokenMap = toTokenMap $
   , (some $ non $ oneOf "/\\:?", PTText)
   ]
 
-private
-lexPath : String -> Either String (List PathToken)
-lexPath str
-    = case lex pathTokenMap str of
-           (tokens, _, _, "") => Right (map TokenData.tok tokens)
-           (tokens, l, c, rest) => Left ("Unrecognized tokens "
-                                     ++ show rest
-                                     ++ " at col "
-                                     ++ show c)
+lexPath : String -> List PathToken
+lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in 
+                map TokenData.tok tokens
 
 -- match both '/' and '\\' regardless of the platform.
-private
 bodySeparator : Grammar PathToken True ()
 bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')
 
@@ -337,7 +158,6 @@ bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')
 -- Windows can automatically translate '/' to '\\'. The verbatim prefix,
 -- i.e., `\\?\`, disables the translation.
 -- Here, we simply parse and then ignore it.
-private
 verbatim : Grammar PathToken True ()
 verbatim = do count (exactly 2) $ match $ PTPunct '\\'
               match $ PTPunct '?'
@@ -345,8 +165,7 @@ verbatim = do count (exactly 2) $ match $ PTPunct '\\'
               pure ()
 
 -- Example: \\server\share
-private
-unc : Grammar PathToken True Volumn
+unc : Grammar PathToken True Volume
 unc = do count (exactly 2) $ match $ PTPunct '\\'
          server <- match PTText
          bodySeparator
@@ -354,8 +173,7 @@ unc = do count (exactly 2) $ match $ PTPunct '\\'
          Core.pure $ UNC server share
 
 -- Example: \\?\server\share
-private
-verbatimUnc : Grammar PathToken True Volumn
+verbatimUnc : Grammar PathToken True Volume
 verbatimUnc = do verbatim
                  server <- match PTText
                  bodySeparator
@@ -363,8 +181,7 @@ verbatimUnc = do verbatim
                  Core.pure $ UNC server share
 
 -- Example: C:
-private
-disk : Grammar PathToken True Volumn
+disk : Grammar PathToken True Volume
 disk = do text <- match PTText
           disk <- case unpack text of
                        (disk :: xs) => pure disk
@@ -373,48 +190,55 @@ disk = do text <- match PTText
           pure $ Disk (toUpper disk)
 
 -- Example: \\?\C:
-private
-verbatimDisk : Grammar PathToken True Volumn
+verbatimDisk : Grammar PathToken True Volume
 verbatimDisk = do verbatim
                   d <- disk
                   pure d
 
-private
-parseVolumn : Grammar PathToken True Volumn
-parseVolumn = verbatimUnc
+parseVolume : Grammar PathToken True Volume
+parseVolume = verbatimUnc
           <|> verbatimDisk
           <|> unc
           <|> disk
 
-private
 parseBody : Grammar PathToken True Body
 parseBody = do text <- match PTText
                the (Grammar _ False _) $
                    case text of
-                        " " => fail "Empty body"
                         ".." => pure ParentDir
                         "." => pure CurDir
                         s => pure (Normal s)
 
-private
 parsePath : Grammar PathToken False Path
-parsePath = do vol <- optional parseVolumn
-               root <- optional bodySeparator
-               body <- sepBy bodySeparator parseBody
-               trailSep <- optional bodySeparator
+parsePath = do vol <- optional parseVolume
+               root <- optional (some bodySeparator)
+               body <- sepBy (some bodySeparator) parseBody
+               trailSep <- optional (some bodySeparator)
+               let body = filter (\case Normal s => ltrim s /= ""
+                                        _ => True) body
+               let body = case body of
+                               [] => []
+                               (x::xs) => x :: delete CurDir xs
                pure $ MkPath vol (isJust root) body (isJust trailSep)
 
-||| Attempt to parse a String into Path.
+||| Parse a String into Path component.
 |||
-||| Returns a error message if the parser fails.
+||| Returns the path parsed as much as possible from left to right, the 
+||| invalid parts on the right end is ignored.
 |||
-||| The parser is relaxed to accept invalid inputs. Relaxing rules:
+||| Some kind of invalid path is accepted. Relaxing rules:
 |||
-||| - Both slash('/') and backslash('\\') are parsed as directory separator,
-|||   regardless of the platform;
-||| - Invalid characters in path body in allowed, e.g., glob like "/root/*";
-||| - Ignoring the verbatim prefix(`\\?\`) that disables the forward
-|||   slash (Windows only).
+||| - Both slash('/') and backslash('\\') are parsed as valid directory
+|||   separator, regardless of the platform;
+||| - Any characters in path body in allowed, e.g., glob like "/root/*";
+||| - Verbatim prefix(`\\?\`) that disables the forward
+|||   slash (Windows only) is ignored.
+||| - Repeated separators are ignored, so "a/b" and "a//b" both have "a" 
+|||   and "b" as bodies.
+||| - Occurrences of "." are normalized away, except if they are at the
+|||   beginning of the path. For example, "a/./b", "a/b/", "a/b/". and 
+|||   "a/b" all have "a" and "b" as bodies, but "./a/b" starts with an 
+|||   additional `CurDir` body.
 |||
 ||| ```idris example
 ||| parse "C:\\Windows/System32"
@@ -423,18 +247,220 @@ parsePath = do vol <- optional parseVolumn
 ||| parse "/usr/local/etc/*"
 ||| ```
 export
-parse : String -> Either String Path
-parse str = case parse parsePath !(lexPath str) of
-                 Right (p, []) => Right p
-                 Right (p, ts) => Left ("Unrecognised tokens remaining : "
-                                     ++ show (map text ts))
-                 Left (Error msg ts) => Left (msg ++ " : " ++ show (map text ts))
+parse : String -> Path
+parse str = case parse parsePath (lexPath str) of
+                 Right (p, _) => p
+                 _ => emptyPath
 
-||| Attempt to parse the parts of a path and appends together.
+--------------------------------------------------------------------------------
+-- Utils
+--------------------------------------------------------------------------------
+
+isAbsolute' : Path -> Bool
+isAbsolute' p = if isWindows
+                  then case p.volume of
+                            Just (UNC _ _) => True
+                            Just (Disk _) => p.hasRoot
+                            Nothing => False
+                  else p.hasRoot
+
+append' : (left : Path) -> (right : Path) -> Path
+append' l r = if isAbsolute' r || isJust r.volume
+                 then r
+                 else if hasRoot r
+                         then record { volume = l.volume } r
+                         else record { body = l.body ++ r.body,
+                                       hasTrailSep = r.hasTrailSep } l
+
+splitParent' : Path -> Maybe (Path, Path)
+splitParent' p 
+  = case p.body of
+         [] => Nothing
+         (x::xs) => let parentPath = record { body = init (x::xs),
+                                          hasTrailSep = False } p
+                        lastPath = MkPath Nothing False [last (x::xs)] p.hasTrailSep in
+                      Just (parentPath, lastPath)
+
+parent' : Path -> Maybe Path
+parent' p = map fst (splitParent' p) 
+
+fileName' : Path -> Maybe String
+fileName' p = findNormal (reverse p.body)
+  where
+    findNormal : List Body -> Maybe String
+    findNormal ((Normal s)::xs) = Just s
+    findNormal (CurDir::xs) = findNormal xs
+    findNormal _ = Nothing
+    
+setFileName' : (name : String) -> Path -> Path
+setFileName' name p = if isJust (fileName' p)
+                         then append' (fromMaybe emptyPath $ parent' p) (parse name)
+                         else append' p (parse name)
+    
+splitFileName : String -> (String, String)
+splitFileName name
+    = case break (== '.') $ reverse $ unpack name of
+           (_, []) => (name, "")
+           (_, ['.']) => (name, "")
+           (revExt, (dot :: revStem))
+              => ((pack $ reverse revStem), (pack $ reverse revExt))
+
+--------------------------------------------------------------------------------
+-- Manipulations
+--------------------------------------------------------------------------------
+
+||| Returns true if the path is absolute.
+|||
+||| - On Unix, a path is absolute if it starts with the root,
+|||   so isAbsolute and hasRoot are equivalent.
+|||
+||| - On Windows, a path is absolute if it has a volume and starts
+|||   with the root. e.g., `c:\\windows` is absolute, while `c:temp`
+|||   and `\temp` are not. In addition, a path with UNC volume is absolute.
+export
+isAbsolute : String -> Bool
+isAbsolute p = isAbsolute' (parse p)
+
+||| Returns true if the path is relative, i.e., not absolute.
+export
+isRelative : String -> Bool
+isRelative = not . isAbsolute
+
+||| Appends the right path to the left one.
+|||
+||| If the path on the right is absolute, it replaces the left path.
+|||
+||| On Windows:
+|||
+||| - If the right path has a root but no volume (e.g., `\windows`), it
+|||   replaces everything except for the volume (if any) of left.
+||| - If the right path has a volume but no root, it replaces left.
 |||
 ||| ```idris example
-||| parseParts ["/usr", "local/etc"]
+||| "/usr" </> "local/etc"
 ||| ```
 export
-parseParts : (parts : List String) -> Either String Path
-parseParts parts = map concat (traverse parse parts)
+(</>) : (left : String) -> (right : String) -> String
+(</>) l r = show $ append' (parse l) (parse r)
+
+||| Join path elements together.
+|||
+||| ```idris example
+||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
+||| ```
+export
+joinPath : List String -> String
+joinPath xs = foldl (</>) "" xs
+
+||| Returns the parent and child.
+|||
+||| ```idris example
+||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
+||| ```
+export
+splitParent : String -> Maybe (String, String)
+splitParent p = do (a, b) <- splitParent' (parse p)
+                   pure $ (show a, show b)
+
+||| Returns the path without its final component, if there is one.
+|||
+||| Returns Nothing if the path terminates in a root or volume.
+export
+parent : String -> Maybe String
+parent p = map show $ parent' (parse p)
+
+||| Returns a list of all the parents of the path, longest first,
+||| self included.
+|||
+||| ```idris example
+||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
+||| ```
+export
+parents : String -> List String
+parents p = map show $ iterate parent' (parse p)
+
+||| Determines whether base is either one of the parents of full.
+|||
+||| Trailing separator is ignored.
+export
+startWith : (base : String) -> (full : String) -> Bool
+startWith base full = (parse base) `elem` (iterate parent' (parse full))
+
+||| Returns a path that, when appended onto base, yields full.
+|||
+||| If base is not a prefix of full (i.e., startWith returns false),
+||| returns Nothing.
+export
+stripPrefix : (base : String) -> (full : String) -> Maybe String
+stripPrefix base full
+    = do let MkPath vol1 root1 body1 _ = parse base
+         let MkPath vol2 root2 body2 trialSep = parse full
+         if vol1 == vol2 && root1 == root2 then Just () else Nothing
+         body <- stripBody body1 body2
+         pure $ show $ MkPath Nothing False body trialSep
+  where
+    stripBody : (base : List Body) -> (full : List Body) -> Maybe (List Body)
+    stripBody [] ys = Just ys
+    stripBody xs [] = Nothing
+    stripBody (x::xs) (y::ys) = if x == y then stripBody xs ys else Nothing
+
+||| Returns the final body of the path, if there is one.
+|||
+||| If the path is a normal file, this is the file name. If it's the
+||| path of a directory, this is the directory name.
+|||
+||| Returns Nothing if the final body is "..".
+export
+fileName : String -> Maybe String
+fileName p = fileName' (parse p)
+
+||| Extracts the stem (non-extension) portion of the file name of path.
+|||
+||| The stem is:
+|||
+||| - Nothing, if there is no file name;
+||| - The entire file name if there is no embedded ".";
+||| - The entire file name if the file name begins with "." and has
+|||   no other "."s within;
+||| - Otherwise, the portion of the file name before the final "."
+export
+fileStem : String -> Maybe String
+fileStem p = pure $ fst $ splitFileName !(fileName p)
+
+||| Extracts the extension of the file name of path.
+|||
+||| The extension is:
+|||
+||| - Nothing, if there is no file name;
+||| - Nothing, if there is no embedded ".";
+||| - Nothing, if the file name begins with "." and has no other "."s within;
+||| - Otherwise, the portion of the file name after the final "."
+export
+extension : String -> Maybe String
+extension p = pure $ snd $ splitFileName !(fileName p)
+
+||| Updates the file name of the path.
+|||
+||| If no file name, this is equivalent to appending the name;
+||| Otherwise it is equivalent to appending the name to the parent.
+export
+setFileName : (name : String) -> String -> String
+setFileName name p = show $ setFileName' name (parse p)
+
+||| Append a extension to the path.
+|||
+||| Returns the path as it is if no file name.
+|||
+||| If `extension` of the path is Nothing, the extension is added; otherwise
+||| it is replaced.
+||| 
+||| If the ext is empty, the extension is dropped.
+export
+(<.>) : String -> (ext : String) -> String
+(<.>) p ext = let p' = parse p 
+                  ext = pack $ dropWhile (== '.') (unpack ext)
+                  ext = if ltrim ext == "" then "" else "." ++ ext in
+                case fileName' p' of
+                     Just name => let (stem, _) = splitFileName name in
+                                    show $ setFileName' (stem ++ ext) p'
+                     Nothing => p

libs/contrib/Text/Lexer/Core.idr

@@ -101,7 +101,6 @@ strIndex (MkStrLen str len) i
 mkStr : String -> StrLen
 mkStr str = MkStrLen str (length str)
 
-export
 strTail : Nat -> StrLen -> StrLen
 strTail start (MkStrLen str len)
     = MkStrLen (substr start len str) (minus len start)

libs/contrib/contrib.ipkg

@@ -3,6 +3,11 @@ package contrib
 modules = Control.Delayed,
 
           Data.List.TailRec,
+          Data.List.Equalities,
+          Data.List.Reverse,
+          Data.List.Views.Extra,
+          Data.List.Palindrome,
+
           Data.Bool.Extra,
           Data.Fin.Extra,
           Data.Nat.Equational,

libs/prelude/Prelude.idr

@@ -3,6 +3,8 @@ module Prelude
 import public Builtin
 import public PrimIO
 
+%default total
+
 {-
 The Prelude is minimal (since it is effectively part of the language
 specification, this seems to be desirable - we should, nevertheless, aim to
@@ -211,6 +213,22 @@ public export
 Eq Integer where
   x == y = intToBool (prim__eq_Integer x y)
 
+public export
+Eq Bits8 where
+  x == y = intToBool (prim__eq_Bits8 x y)
+
+public export
+Eq Bits16 where
+  x == y = intToBool (prim__eq_Bits16 x y)
+
+public export
+Eq Bits32 where
+  x == y = intToBool (prim__eq_Bits32 x y)
+
+public export
+Eq Bits64 where
+  x == y = intToBool (prim__eq_Bits64 x y)
+
 public export
 Eq Double where
   x == y = intToBool (prim__eq_Double x y)
@@ -289,6 +307,42 @@ Ord Integer where
   (>) x y = intToBool (prim__gt_Integer x y)
   (>=) x y = intToBool (prim__gte_Integer x y)
 
+public export
+Ord Bits8 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits8 x y)
+  (<=) x y = intToBool (prim__lte_Bits8 x y)
+  (>) x y = intToBool (prim__gt_Bits8 x y)
+  (>=) x y = intToBool (prim__gte_Bits8 x y)
+
+public export
+Ord Bits16 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits16 x y)
+  (<=) x y = intToBool (prim__lte_Bits16 x y)
+  (>) x y = intToBool (prim__gt_Bits16 x y)
+  (>=) x y = intToBool (prim__gte_Bits16 x y)
+
+public export
+Ord Bits32 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits32 x y)
+  (<=) x y = intToBool (prim__lte_Bits32 x y)
+  (>) x y = intToBool (prim__gt_Bits32 x y)
+  (>=) x y = intToBool (prim__gte_Bits32 x y)
+
+public export
+Ord Bits64 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits64 x y)
+  (<=) x y = intToBool (prim__lte_Bits64 x y)
+  (>) x y = intToBool (prim__gt_Bits64 x y)
+  (>=) x y = intToBool (prim__gte_Bits64 x y)
+
 public export
 Ord Double where
   compare x y = if x < y then LT else if x == y then EQ else GT
@@ -371,6 +425,7 @@ interface Num ty => Integral ty where
 
 -- Integer
 
+%inline
 public export
 Num Integer where
   (+) = prim__add_Integer
@@ -406,6 +461,7 @@ defaultInteger = %search
 
 -- Int
 
+%inline
 public export
 Num Int where
   (+) = prim__add_Int
@@ -430,6 +486,42 @@ Integral Int where
       = case y == 0 of
              False => prim__mod_Int x y
 
+-- Bits8
+
+%inline
+public export
+Num Bits8 where
+  (+) = prim__add_Bits8
+  (*) = prim__mul_Bits8
+  fromInteger = prim__cast_IntegerBits8
+
+-- Bits16
+
+%inline
+public export
+Num Bits16 where
+  (+) = prim__add_Bits16
+  (*) = prim__mul_Bits16
+  fromInteger = prim__cast_IntegerBits16
+
+-- Bits32
+
+%inline
+public export
+Num Bits32 where
+  (+) = prim__add_Bits32
+  (*) = prim__mul_Bits32
+  fromInteger = prim__cast_IntegerBits32
+
+-- Bits64
+
+%inline
+public export
+Num Bits64 where
+  (+) = prim__add_Bits64
+  (*) = prim__mul_Bits64
+  fromInteger = prim__cast_IntegerBits64
+
 -- Double
 
 public export
@@ -719,8 +811,8 @@ public export
 data Nat =
   ||| Zero.
     Z
-  ||| Successor.
-  | S Nat
+  | ||| Successor.
+  S Nat
 
 %name Nat k, j, i
 
@@ -912,11 +1004,13 @@ public export
   Right x == Right x' = x == x'
   _ == _ = False
 
+%inline
 public export
 Functor (Either e) where
   map f (Left x) = Left x
   map f (Right x) = Right (f x)
 
+%inline
 public export
 Applicative (Either e) where
     pure = Right
@@ -940,8 +1034,8 @@ data List a =
   ||| Empty list
   Nil
 
-  ||| A non-empty list, consisting of a head element and the rest of the list.
-  | (::) a (List a)
+  | ||| A non-empty list, consisting of a head element and the rest of the list.
+  (::) a (List a)
 
 %name List xs, ys, zs
 
@@ -1340,6 +1434,22 @@ export
 Show Integer where
   showPrec = primNumShow prim__cast_IntegerString
 
+export
+Show Bits8 where
+  showPrec = primNumShow prim__cast_Bits8String
+
+export
+Show Bits16 where
+  showPrec = primNumShow prim__cast_Bits16String
+
+export
+Show Bits32 where
+  showPrec = primNumShow prim__cast_Bits32String
+
+export
+Show Bits64 where
+  showPrec = primNumShow prim__cast_Bits64String
+
 export
 Show Double where
   showPrec = primNumShow prim__cast_DoubleString
@@ -1439,6 +1549,7 @@ public export
 Functor IO where
   map f io = io_bind io (\b => io_pure (f b))
 
+%inline
 public export
 Applicative IO where
   pure x = io_pure x

src/Algebra.idr

@@ -4,6 +4,8 @@ import public Algebra.ZeroOneOmega
 import public Algebra.Semiring
 import public Algebra.Preorder
 
+%default total
+
 public export
 RigCount : Type
 RigCount = ZeroOneOmega

src/Algebra/Preorder.idr

@@ -1,5 +1,7 @@
 module Algebra.Preorder
 
+%default total
+
 ||| Preorder defines a binary relation using the `<=` operator
 public export
 interface Preorder a where

src/Algebra/ZeroOneOmega.idr

@@ -3,9 +3,12 @@ module Algebra.ZeroOneOmega
 import Algebra.Semiring
 import Algebra.Preorder
 
+%default total
+
 export
 data ZeroOneOmega = Rig0 | Rig1 | RigW
 
+export
 Preorder ZeroOneOmega where
   Rig0 <= _ = True
   Rig1 <= Rig1 = True

src/Compiler/Common.idr

@@ -22,6 +22,8 @@ import System.Directory
 import System.Info
 import System.File
 
+%default covering
+
 ||| Generic interface to some code generator
 public export
 record Codegen where

src/Compiler/CompileExpr.idr

@@ -501,6 +501,10 @@ getNArgs defs n args = pure $ User n args
 nfToCFType : {auto c : Ref Ctxt Defs} ->
              FC -> (inStruct : Bool) -> NF [] -> Core CFType
 nfToCFType _ _ (NPrimVal _ IntType) = pure CFInt
+nfToCFType _ _ (NPrimVal _ Bits8Type) = pure CFUnsigned
+nfToCFType _ _ (NPrimVal _ Bits16Type) = pure CFUnsigned
+nfToCFType _ _ (NPrimVal _ Bits32Type) = pure CFUnsigned
+nfToCFType _ _ (NPrimVal _ Bits64Type) = pure CFUnsigned
 nfToCFType _ False (NPrimVal _ StringType) = pure CFString
 nfToCFType fc True (NPrimVal _ StringType)
     = throw (GenericMsg fc "String not allowed in a foreign struct")

src/Compiler/Scheme/Chez.idr

@@ -11,6 +11,7 @@ import Core.Name
 import Core.Options
 import Core.TT
 import Utils.Hex
+import Utils.Path
 
 import Data.List
 import Data.Maybe
@@ -29,7 +30,7 @@ import System.Info
 pathLookup : IO String
 pathLookup
     = do path <- getEnv "PATH"
-         let pathList = split (== pathSep) $ fromMaybe "/usr/bin:/usr/local/bin" path
+         let pathList = split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
          let candidates = [p ++ "/" ++ x | p <- pathList,
                                            x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
          e <- firstExists candidates
@@ -165,6 +166,7 @@ data Structs : Type where
 cftySpec : FC -> CFType -> Core String
 cftySpec fc CFUnit = pure "void"
 cftySpec fc CFInt = pure "int"
+cftySpec fc CFUnsigned = pure "unsigned"
 cftySpec fc CFString = pure "string"
 cftySpec fc CFDouble = pure "double"
 cftySpec fc CFChar = pure "char"
@@ -184,7 +186,7 @@ cCall appdir fc cfn clib args ret
          lib <- if clib `elem` loaded
                    then pure ""
                    else do (fname, fullname) <- locate clib
-                           copyLib (appdir ++ dirSep ++ fname, fullname)
+                           copyLib (appdir </> fname, fullname)
                            put Loaded (clib :: loaded)
                            pure $ "(load-shared-object \""
                                     ++ escapeString fname
@@ -372,7 +374,7 @@ compileToSS c appdir tm outfile
 compileToSO : {auto c : Ref Ctxt Defs} ->
               String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
 compileToSO chez appDirRel outSsAbs
-    = do let tmpFileAbs = appDirRel ++ dirSep ++ "compileChez"
+    = do let tmpFileAbs = appDirRel </> "compileChez"
          let build= "(parameterize ([optimize-level 3]) (compile-program " ++
                     show outSsAbs ++ "))"
          Right () <- coreLift $ writeFile tmpFileAbs build
@@ -402,18 +404,18 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr makeitso c execDir tm outfile
     = do let appDirRel = outfile ++ "_app" -- relative to build dir
-         let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
-         coreLift $ mkdirs (splitDir appDirGen)
+         let appDirGen = execDir </> appDirRel -- relative to here
+         coreLift $ mkdirAll appDirGen
          Just cwd <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
-         let outSsFile = appDirRel ++ dirSep ++ outfile ++ ".ss"
-         let outSoFile = appDirRel ++ dirSep ++ outfile ++ ".so"
-         let outSsAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSsFile
-         let outSoAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSoFile
+         let outSsFile = appDirRel </> outfile <.> "ss"
+         let outSoFile = appDirRel </> outfile <.> "so"
+         let outSsAbs = cwd </> execDir </> outSsFile
+         let outSoAbs = cwd </> execDir </> outSoFile
          chez <- coreLift $ findChez
          compileToSS c appDirGen tm outSsAbs
          logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
-         let outShRel = execDir ++ dirSep ++ outfile
+         let outShRel = execDir </> outfile
          if isWindows
             then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) 
             else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)

src/Compiler/Scheme/Common.idr

@@ -63,6 +63,22 @@ 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 Bits8Type) [x, y] = op "b+" [x, y, "8"]
+schOp (Sub Bits8Type) [x, y] = op "b-" [x, y, "8"]
+schOp (Mul Bits8Type) [x, y] = op "b*" [x, y, "8"]
+schOp (Div Bits8Type) [x, y] = op "b/" [x, y, "8"]
+schOp (Add Bits16Type) [x, y] = op "b+" [x, y, "16"]
+schOp (Sub Bits16Type) [x, y] = op "b-" [x, y, "16"]
+schOp (Mul Bits16Type) [x, y] = op "b*" [x, y, "16"]
+schOp (Div Bits16Type) [x, y] = op "b/" [x, y, "16"]
+schOp (Add Bits32Type) [x, y] = op "b+" [x, y, "32"]
+schOp (Sub Bits32Type) [x, y] = op "b-" [x, y, "32"]
+schOp (Mul Bits32Type) [x, y] = op "b*" [x, y, "32"]
+schOp (Div Bits32Type) [x, y] = op "b/" [x, y, "32"]
+schOp (Add Bits64Type) [x, y] = op "b+" [x, y, "64"]
+schOp (Sub Bits64Type) [x, y] = op "b-" [x, y, "64"]
+schOp (Mul Bits64Type) [x, y] = op "b*" [x, y, "64"]
+schOp (Div Bits64Type) [x, y] = op "b/" [x, y, "64"]
 schOp (Add ty) [x, y] = op "+" [x, y]
 schOp (Sub ty) [x, y] = op "-" [x, y]
 schOp (Mul ty) [x, y] = op "*" [x, y]
@@ -70,6 +86,11 @@ 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 IntType) [x, y] = op "blodwen-bits-shl" [x, y, "63"]
+schOp (ShiftL Bits8Type) [x, y] = op "blodwen-bits-shl" [x, y, "8"]
+schOp (ShiftL Bits16Type) [x, y] = op "blodwen-bits-shl" [x, y, "16"]
+schOp (ShiftL Bits32Type) [x, y] = op "blodwen-bits-shl" [x, y, "32"]
+schOp (ShiftL Bits64Type) [x, y] = op "blodwen-bits-shl" [x, y, "64"]
 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]
@@ -114,19 +135,35 @@ 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 Bits8Type StringType) [x] = op "number->string" [x]
+schOp (Cast Bits16Type StringType) [x] = op "number->string" [x]
+schOp (Cast Bits32Type StringType) [x] = op "number->string" [x]
+schOp (Cast Bits64Type 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 Bits8Type IntegerType) [x] = x
+schOp (Cast Bits16Type IntegerType) [x] = x
+schOp (Cast Bits32Type IntegerType) [x] = x
+schOp (Cast Bits64Type 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 Bits8Type IntType) [x] = x
+schOp (Cast Bits16Type IntType) [x] = x
+schOp (Cast Bits32Type 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 Bits8Type) [x] = op "integer->bits8" [x]
+schOp (Cast IntegerType Bits16Type) [x] = op "integer->bits16" [x]
+schOp (Cast IntegerType Bits32Type) [x] = op "integer->bits32" [x]
+schOp (Cast IntegerType Bits64Type) [x] = op "integer->bits64" [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]
@@ -192,6 +229,10 @@ mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- M
 schConstant : (String -> String) -> Constant -> String
 schConstant _ (I x) = show x
 schConstant _ (BI x) = show x
+schConstant _ (B8 x) = show x
+schConstant _ (B16 x) = show x
+schConstant _ (B32 x) = show x
+schConstant _ (B64 x) = show x
 schConstant schString (Str x) = schString x
 schConstant _ (Ch x)
    = if (the Int (cast x) >= 32 && the Int (cast x) < 127)
@@ -201,6 +242,10 @@ schConstant _ (Db x) = show x
 schConstant _ WorldVal = "#f"
 schConstant _ IntType = "#t"
 schConstant _ IntegerType = "#t"
+schConstant _ Bits8Type = "#t"
+schConstant _ Bits16Type = "#t"
+schConstant _ Bits32Type = "#t"
+schConstant _ Bits64Type = "#t"
 schConstant _ StringType = "#t"
 schConstant _ CharType = "#t"
 schConstant _ DoubleType = "#t"

src/Compiler/Scheme/Gambit.idr

@@ -11,6 +11,7 @@ import Core.Name
 import Core.Options
 import Core.TT
 import Utils.Hex
+import Utils.Path
 
 import Data.List
 import Data.Maybe
@@ -122,9 +123,35 @@ data Loaded : Type where
 -- Label for noting which struct types are declared
 data Structs : Type where
 
+notWorld : CFType -> Bool
+notWorld CFWorld = False
+notWorld _ = True
+
+cType : FC -> CFType -> Core String
+cType fc CFUnit = pure "void"
+cType fc CFInt = pure "int"
+cType fc CFString = pure "char *"
+cType fc CFDouble = pure "double"
+cType fc CFChar = pure "char"
+cType fc CFPtr = pure "void *"
+cType fc (CFIORes t) = cType fc t
+cType fc (CFStruct n t) = pure $ "struct " ++ n
+cType 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 <- cType fc retty
+             argspecs <- traverse (cType fc) (reverse . filter notWorld $ args)
+             pure $ rtyspec ++ " (*)(" ++ showSep ", " argspecs ++ ")"
+cType fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
+                       " to foreign function"))
+
 cftySpec : FC -> CFType -> Core String
 cftySpec fc CFUnit = pure "void"
 cftySpec fc CFInt = pure "int"
+cftySpec fc CFUnsigned = pure "unsigned-int"
 cftySpec fc CFString = pure "UTF-8-string"
 cftySpec fc CFDouble = pure "double"
 cftySpec fc CFChar = pure "char"
@@ -138,16 +165,31 @@ cftySpec fc (CFFun s t) = funTySpec [s] t
     funTySpec args (CFFun s t) = funTySpec (s :: args) t
     funTySpec args retty
         = do rtyspec <- cftySpec fc retty
-             argspecs <- traverse (cftySpec fc) (reverse args)
+             argspecs <- traverse (cftySpec fc) (reverse . filter notWorld $ args)
              pure $ "(function (" ++ showSep " " argspecs ++ ") " ++ rtyspec ++ ")"
 cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
                          " to foreign function"))
 
+
+record CCallbackInfo where
+  constructor MkCCallbackInfo
+  schemeArgName : String
+  schemeWrapName : String
+  callbackBody : String
+  argTypes : List String
+  retType : String
+
+record CWrapperDefs where
+  constructor MkCWrapperDefs
+  setBox : String
+  boxDef : String
+  cWrapDef : String
+
 cCall : {auto c : Ref Ctxt Defs} ->
         {auto l : Ref Loaded (List String)} ->
-        FC -> (cfn : String) -> (clib : String) ->
-        List (Name, CFType) -> CFType -> Core String
-cCall fc cfn clib args ret
+        FC -> (cfn : String) -> (fnWrapName : String -> String) -> (clib : String) ->
+        List (Name, CFType) -> CFType -> Core (String, String)
+cCall fc cfn fnWrapName clib args ret
     = do -- loaded <- get Loaded
          -- lib <- if clib `elem` loaded
          --           then pure ""
@@ -157,13 +199,26 @@ cCall fc cfn clib args ret
          --                   pure ""
          argTypes <- traverse (\a => cftySpec fc (snd a)) args
          retType <- cftySpec fc ret
-         let call = "((c-lambda (" ++ showSep " " argTypes ++ ") "
+
+         argsInfo <- traverse buildArg args
+         argCTypes <- traverse (\a => cType fc (snd a)) args
+         retCType <- cType fc ret
+
+         let cWrapperDefs = map buildCWrapperDefs $ mapMaybe snd argsInfo
+         let cFunWrapDeclaration = buildCFunWrapDeclaration cfn retCType argCTypes
+         let wrapDeclarations = cFunWrapDeclaration
+                                ++ concatMap (.boxDef) cWrapperDefs
+                                ++ concatMap (.cWrapDef) cWrapperDefs
+
+         let setBoxes = concatMap (.setBox) cWrapperDefs
+         let call = " ((c-lambda (" ++ showSep " " argTypes ++ ") "
                       ++ retType ++ " " ++ show cfn ++ ") "
-                      ++ showSep " " !(traverse buildArg args) ++ ")"
+                      ++ showSep " " (map fst argsInfo) ++ ")"
+         let body = setBoxes ++ "\n" ++ call
 
          pure $ case ret of -- XXX
-                     CFIORes _ => handleRet retType call
-                     _ => call
+                     CFIORes _ => (handleRet retType body, wrapDeclarations) 
+                     _ => (body, wrapDeclarations)
   where
     mkNs : Int -> List CFType -> List (Maybe String)
     mkNs i [] = []
@@ -175,27 +230,58 @@ cCall fc cfn clib args ret
     applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
     applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as
 
+    replaceChar : Char -> Char -> String -> String
+    replaceChar old new = pack . replaceOn old new . unpack
+
+    buildCWrapperDefs : CCallbackInfo -> CWrapperDefs
+    buildCWrapperDefs (MkCCallbackInfo arg schemeWrap callbackStr argTypes retType) = 
+      let box = schemeWrap ++ "-box"
+          setBox = "\n (set-box! " ++ box ++ " " ++ callbackStr ++ ")"
+          cWrapName = replaceChar '-' '_' schemeWrap
+          boxDef = "\n(define " ++ box ++ " (box #f))\n"
+
+          args =
+            if length argTypes > 0
+              then " " ++ (showSep " " $ map (\i => "farg-" ++ show i) [0 .. (natToInteger $ length argTypes) - 1])
+              else ""
+
+          cWrapDef =
+            "\n(c-define " ++
+            "(" ++ schemeWrap ++ args ++ ")" ++
+            " (" ++ showSep " " argTypes ++ ")" ++
+            " " ++ retType ++
+            " \"" ++ cWrapName ++ "\"" ++ " \"\"" ++
+            "\n ((unbox " ++ box ++ ")" ++ args ++ ")" ++
+            "\n)\n"
+      in MkCWrapperDefs setBox boxDef cWrapDef
+
+    buildCFunWrapDeclaration : String -> String -> List String -> String
+    buildCFunWrapDeclaration name ret args =
+      "\n(c-declare #<<c-declare-end\n" ++
+      ret ++ " " ++ name ++ "(" ++ showSep ", " args ++ ");" ++
+      "\nc-declare-end\n)\n"
+
     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 : String -> List CFType -> CFType -> Core (String, List String, 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
+             pure (mkFun args retty n, argTypes, retType)
 
-    buildArg : (Name, CFType) -> Core String
-    buildArg (n, CFFun s t) = callback (schName n) [s] t
-    buildArg (n, _) = pure $ schName n
+    buildArg : (Name, CFType) -> Core (String, Maybe CCallbackInfo)
+    buildArg (n, CFFun s t) = do
+      let arg = schName n
+      let schemeWrap = fnWrapName arg
+      (callbackBody, argTypes, retType) <- callback arg [s] t
+      pure (schemeWrap, Just $ MkCCallbackInfo arg schemeWrap callbackBody argTypes retType)
+    buildArg (n, _) = pure (schName n, Nothing)
 
 schemeCall : FC -> (sfn : String) ->
              List Name -> CFType -> Core String
@@ -210,16 +296,20 @@ schemeCall fc sfn argns ret
 -- of the function call.
 useCC : {auto c : Ref Ctxt Defs} ->
         {auto l : Ref Loaded (List String)} ->
-        FC -> List String -> List (Name, CFType) -> CFType -> Core (Maybe String, String)
+        FC -> List String -> List (Name, CFType) -> CFType -> Core (Maybe String, (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]) => pure (Nothing, !(schemeCall fc sfn (map fst args) ret))
-           Just ("C", [cfn, clib]) => pure (Just clib, !(cCall fc cfn clib args ret))
-           Just ("C", [cfn, clib, chdr]) => pure (Just clib, !(cCall fc cfn clib args ret))
+           Just ("scheme", [sfn]) => pure (Nothing, (!(schemeCall fc sfn (map fst args) ret), ""))
+           Just ("C", [cfn, clib]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))
+           Just ("C", [cfn, clib, chdr]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))
            _ => useCC fc ccs args ret
+  where
+    fnWrapName : String -> String -> String
+    fnWrapName cfn schemeArgName = schemeArgName ++ "-" ++ cfn ++ "-cFunWrap"
+
 
 -- For every foreign arg type, return a name, and whether to pass it to the
 -- foreign call (we don't pass '%World')
@@ -255,10 +345,11 @@ schFgnDef fc n (MkNmForeign cs args ret)
          let useargns = map fst (filter snd argns)
          argStrs <- traverse mkStruct args
          retStr <- mkStruct ret
-         (lib, body) <- useCC fc cs (zip useargns args) ret
+         (lib, (body, wrapDeclarations)) <- useCC fc cs (zip useargns args) ret
          defs <- get Ctxt
          pure (lib,
                 concat argStrs ++ retStr ++
+                wrapDeclarations ++
                 "(define " ++ schName !(full (gamma defs) n) ++
                 " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
                 body ++ "))\n")
@@ -295,16 +386,16 @@ compileToSCM c tm outfile
 compileExpr : Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr c execDir tm outfile
-    = do let outn = execDir ++ dirSep ++ outfile ++ ".scm"
+    = do let outn = execDir </> outfile <.> "scm"
          libsname <- compileToSCM c tm outn
-         libsfile <- traverse findLibraryFile $ nub $ map (++ ".a") libsname
+         libsfile <- traverse findLibraryFile $ map (<.> "a") (nub libsname)
          gsc <- coreLift findGSC
          let cmd = gsc ++ 
                    " -exe -cc-options \"-Wno-implicit-function-declaration\" -ld-options \"" ++
                    (showSep " " libsfile)  ++ "\" " ++ outn
          ok <- coreLift $ system cmd
          if ok == 0
-            then pure (Just (execDir ++ dirSep ++ outfile))
+            then pure (Just (execDir </> outfile))
             else pure Nothing
 
 executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()

src/Compiler/Scheme/Racket.idr

@@ -11,6 +11,7 @@ import Core.Directory
 import Core.Name
 import Core.TT
 import Utils.Hex
+import Utils.Path
 
 import Data.List
 import Data.Maybe
@@ -107,6 +108,7 @@ data Done : Type where
 cftySpec : FC -> CFType -> Core String
 cftySpec fc CFUnit = pure "_void"
 cftySpec fc CFInt = pure "_int"
+cftySpec fc CFUnsigned = pure "_uint"
 cftySpec fc CFString = pure "_string/utf-8"
 cftySpec fc CFDouble = pure "_double"
 cftySpec fc CFChar = pure "_int8"
@@ -166,7 +168,7 @@ cCall appdir fc cfn libspec args ret
                    then pure ""
                    else do put Loaded (libn :: loaded)
                            (fname, fullname) <- locate libspec
-                           copyLib (appdir ++ dirSep ++ fname, fullname)
+                           copyLib (appdir </> fname, fullname)
                            pure (loadlib libn vers)
 
          argTypes <- traverse (\a => do s <- cftySpec fc (snd a)
@@ -366,16 +368,16 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr mkexec c execDir tm outfile
     = do let appDirRel = outfile ++ "_app" -- relative to build dir
-         let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
-         coreLift $ mkdirs (splitDir appDirGen)
+         let appDirGen = execDir </> appDirRel -- relative to here
+         coreLift $ mkdirAll appDirGen
          Just cwd <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
           
          let ext = if isWindows then ".exe" else ""
-         let outRktFile = appDirRel ++ dirSep ++ outfile ++ ".rkt"
-         let outBinFile = appDirRel ++ dirSep ++ outfile ++ ext
-         let outRktAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outRktFile
-         let outBinAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outBinFile
+         let outRktFile = appDirRel </> outfile <.> "rkt"
+         let outBinFile = appDirRel </> outfile <.> ext
+         let outRktAbs = cwd </> execDir </> outRktFile
+         let outBinAbs = cwd </> execDir </> outBinFile
 
          compileToRKT c appDirGen tm outRktAbs
          raco <- coreLift findRacoExe
@@ -388,7 +390,7 @@ compileExpr mkexec c execDir tm outfile
                   else pure 0
          if ok == 0
             then do -- TODO: add launcher script
-                    let outShRel = execDir ++ dirSep ++ outfile
+                    let outShRel = execDir </> outfile
                     the (Core ()) $ if isWindows
                        then if mkexec
                                then makeShWindows "" outShRel appDirRel outBinFile

src/Control/Delayed.idr

@@ -1,6 +1,8 @@
 ||| Utilities functions for contitionally delaying values.
 module Control.Delayed
 
+%default total
+
 ||| Type-level function for a conditionally infinite type.
 public export
 inf : Bool -> Type -> Type

src/Core/Binary.idr

@@ -30,7 +30,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 29
+ttcVersion = 33
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/CompileExpr.idr

@@ -111,6 +111,7 @@ public export
 data CFType : Type where
      CFUnit : CFType
      CFInt : CFType
+     CFUnsigned : CFType
      CFString : CFType
      CFDouble : CFType
      CFChar : CFType
@@ -290,6 +291,7 @@ export
 Show CFType where
   show CFUnit = "Unit"
   show CFInt = "Int"
+  show CFUnsigned = "Bits_n"
   show CFString = "String"
   show CFDouble = "Double"
   show CFChar = "Char"

src/Core/Context.idr

@@ -149,6 +149,11 @@ data Clause : Type where
                 (env : Env Term vars) ->
                 (lhs : Term vars) -> (rhs : Term vars) -> Clause
 
+export
+Show Clause where
+  show (MkClause {vars} env lhs rhs)
+      = show vars ++ ": " ++ show lhs ++ " = " ++ show rhs
+
 public export
 data DefFlag
     = Inline
@@ -208,6 +213,13 @@ Show SizeChange where
   show Same = "Same"
   show Unknown = "Unknown"
 
+export
+Eq SizeChange where
+  Smaller == Smaller = True
+  Same == Same = True
+  Unknown == Unknown = True
+  _ == _ = False
+
 public export
 record SCCall where
      constructor MkSCCall
@@ -222,6 +234,10 @@ export
 Show SCCall where
   show c = show (fnCall c) ++ ": " ++ show (fnArgs c)
 
+export
+Eq SCCall where
+  x == y = fnCall x == fnCall y && fnArgs x == fnArgs y
+
 public export
 record GlobalDef where
   constructor MkGlobalDef

src/Core/Core.idr

@@ -126,6 +126,7 @@ data Error : Type where
      CyclicImports : List (List String) -> Error
      ForceNeeded : Error
      InternalError : String -> Error
+     UserError : String -> Error
 
      InType : FC -> Name -> Error -> Error
      InCon : FC -> Name -> Error -> Error
@@ -290,6 +291,7 @@ Show Error where
       showMod ns = showSep "." (reverse ns)
   show ForceNeeded = "Internal error when resolving implicit laziness"
   show (InternalError str) = "INTERNAL ERROR: " ++ str
+  show (UserError str) = "Error: " ++ str
 
   show (InType fc n err)
        = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
@@ -363,6 +365,7 @@ getErrorLoc (ModuleNotFound loc _) = Just loc
 getErrorLoc (CyclicImports _) = Nothing
 getErrorLoc ForceNeeded = Nothing
 getErrorLoc (InternalError _) = Nothing
+getErrorLoc (UserError _) = Nothing
 getErrorLoc (InType _ _ err) = getErrorLoc err
 getErrorLoc (InCon _ _ err) = getErrorLoc err
 getErrorLoc (InLHS _ _ err) = getErrorLoc err

src/Core/Directory.idr

@@ -5,27 +5,17 @@ import Core.Core
 import Core.FC
 import Core.Name
 import Core.Options
+import Utils.Path
 
 import Data.List
 import Data.Strings
+import Data.Maybe
 
 import System.Directory
 import System.File
 import System.Info
 
-%default covering
-
-fullPath : String -> List String
-fullPath fp = filter (/="") $ split (==sep) fp
-
-dropExtension : String -> String
-dropExtension fname
-    = case span (/= '.') (reverse fname) of
-           (all, "") => -- no extension
-               reverse all
-           (ext, root) =>
-               -- assert that root can't be empty
-               reverse (assert_total (strTail root))
+%default total
 
 -- Return the name of the first file available in the list
 firstAvailable : List String -> Core (Maybe String)
@@ -37,11 +27,12 @@ firstAvailable (f :: fs)
          pure (Just f)
 
 export
+covering
 readDataFile : {auto c : Ref Ctxt Defs} ->
                String -> Core String
 readDataFile fname
     = do d <- getDirs
-         let fs = map (\p => p ++ dirSep ++ fname) (data_dirs d)
+         let fs = map (\p => p </> fname) (data_dirs d)
          Just f <- firstAvailable fs
             | Nothing => throw (InternalError ("Can't find data file " ++ fname ++
                                                " in any of " ++ show fs))
@@ -57,8 +48,8 @@ findLibraryFile : {auto c : Ref Ctxt Defs} ->
                   String -> Core String
 findLibraryFile fname
     = do d <- getDirs
-         let fs = map (\p => p ++ dirSep ++ fname)
-                      (lib_dirs d ++ map (\x => x ++ dirSep ++ "lib")
+         let fs = map (\p => p </> fname)
+                      (lib_dirs d ++ map (\x => x </> "lib")
                                          (extra_dirs d))
          Just f <- firstAvailable fs
             | Nothing => throw (InternalError ("Can't find library " ++ fname))
@@ -71,9 +62,9 @@ nsToPath : {auto c : Ref Ctxt Defs} ->
            FC -> List String -> Core (Either Error String)
 nsToPath loc ns
     = do d <- getDirs
-         let fnameBase = showSep dirSep (reverse ns)
-         let fs = map (\p => p ++ dirSep ++ fnameBase ++ ".ttc")
-                      ((build_dir d ++ dirSep ++ "ttc") :: extra_dirs d)
+         let fnameBase = joinPath (reverse ns)
+         let fs = map (\p => p </> fnameBase <.> "ttc")
+                      ((build_dir d </> "ttc") :: extra_dirs d)
          Just f <- firstAvailable fs
             | Nothing => pure (Left (ModuleNotFound loc ns))
          pure (Right f)
@@ -85,9 +76,9 @@ nsToSource : {auto c : Ref Ctxt Defs} ->
              FC -> List String -> Core String
 nsToSource loc ns
     = do d <- getDirs
-         let fnameOrig = showSep dirSep (reverse ns)
-         let fnameBase = maybe fnameOrig (\srcdir => srcdir ++ dirSep ++ fnameOrig) (source_dir d)
-         let fs = map (\ext => fnameBase ++ ext)
+         let fnameOrig = joinPath (reverse ns)
+         let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
+         let fs = map (\ext => fnameBase <.> ext)
                       [".idr", ".lidr", ".yaff", ".org", ".md"]
          Just f <- firstAvailable fs
             | Nothing => throw (ModuleNotFound loc ns)
@@ -96,77 +87,59 @@ nsToSource loc ns
 -- Given a filename in the working directory + source directory, return the correct
 -- namespace for it
 export
-pathToNS : String -> Maybe String -> String -> List String
+pathToNS : String -> Maybe String -> String -> Core (List String)
 pathToNS wdir sdir fname
-    = let wsplit = splitSep wdir
-          ssplit = maybe [] splitSep sdir
-          fsplit = splitSep fname
-          wdrop = dropDir wsplit fsplit fsplit
-       in
-      dropDir ssplit wdrop wdrop
-  where
-    dropDir : List String -> List String -> List String -> List String
-    dropDir dir orig [] = []
-    dropDir dir orig (x :: xs)
-        = if dir == xs
-             then [x]
-             else x :: dropDir dir orig xs
+    = let sdir = fromMaybe "" sdir
+          base = if isAbsolute fname then wdir </> sdir else sdir
+        in
+          case stripPrefix base fname of
+               Nothing => throw (UserError ("Source file " ++ show fname
+                                            ++ " is not in the source directory " 
+                                            ++ show (wdir </> sdir)))
+               Just p => pure $ map show $ reverse $ (parse (p <.> "")).body
 
-    splitSep : String -> List String
-    splitSep fname
-        = case span (/=sep) fname of
-               (end, "") => [dropExtension end]
-               (mod, rest) => assert_total (splitSep (strTail rest)) ++ [mod]
+dirExists : String -> IO Bool
+dirExists dir = do Right d <- openDir dir
+                       | Left _ => pure False
+                   closeDir d
+                   pure True 
 
 -- Create subdirectories, if they don't exist
 export
-mkdirs : List String -> IO (Either FileError ())
-mkdirs [] = pure (Right ())
-mkdirs ("." :: ds) = mkdirs ds
-mkdirs ("" :: ds) = mkdirs ds
-mkdirs (d :: ds)
-    = do ok <- changeDir d
-         if ok
-            then do mkdirs ds
-                    changeDir ".."
-                    pure (Right ())
-            else do Right _ <- createDir d
-                        | Left err => pure (Left err)
-                    ok <- changeDir d
-                    mkdirs ds
-                    changeDir ".."
-                    pure (Right ())
-
-isDirSep : Char -> Bool
-isDirSep c = cast c == dirSep
-
-export
-splitDir : String -> List String
-splitDir = split isDirSep
+covering
+mkdirAll : String -> IO (Either FileError ())
+mkdirAll dir = if parse dir == emptyPath 
+                  then pure (Right ())
+                  else do exist <- dirExists dir
+                          if exist 
+                             then pure (Right ())
+                             else do case parent dir of
+                                          Just parent => mkdirAll parent
+                                          Nothing => pure (Right ()) 
+                                     createDir dir
 
 -- Given a namespace (i.e. a module name), make the build directory for the
 -- corresponding ttc file
 export
+covering
 makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
                      List String -> Core ()
 makeBuildDirectory ns
     = do d <- getDirs
-         let bdir = splitDir $ build_dir d
-         let ndirs = case ns of
-                          [] => []
-                          (n :: ns) => ns -- first item is file name
-         let fname = showSep dirSep (reverse ndirs)
-         Right _ <- coreLift $ mkdirs (bdir ++ "ttc" :: reverse ndirs)
-            | Left err => throw (FileErr (build_dir d ++ dirSep ++ fname) err)
+         let bdir = build_dir d </> "ttc"
+         let ns = reverse $ fromMaybe [] (tail' ns) -- first item is file name
+         let ndir = joinPath ns
+         Right _ <- coreLift $ mkdirAll (bdir </> ndir)
+            | Left err => throw (FileErr (build_dir d </> ndir) err)
          pure ()
 
 export
+covering
 makeExecDirectory : {auto c : Ref Ctxt Defs} ->
                     Core ()
 makeExecDirectory
     = do d <- getDirs
-         let edir = splitDir $ exec_dir d
-         Right _ <- coreLift $ mkdirs edir
+         Right _ <- coreLift $ mkdirAll (exec_dir d)
             | Left err => throw (FileErr (exec_dir d) err)
          pure ()
 
@@ -179,17 +152,17 @@ getTTCFileName inp ext
          d <- getDirs
          -- Get its namespace from the file relative to the working directory
          -- and generate the ttc file from that
-         let ns = pathToNS (working_dir d) (source_dir d) inp
-         let fname = showSep dirSep (reverse ns) ++ ext
+         ns <- pathToNS (working_dir d) (source_dir d) inp
+         let fname = joinPath (reverse ns) <.> ext
          let bdir = build_dir d
-         pure $ bdir ++ dirSep ++ "ttc" ++ dirSep ++ fname
+         pure $ bdir </> "ttc" </> fname
 
 -- Given a root executable name, return the name in the build directory
 export
 getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String
 getExecFileName efile
     = do d <- getDirs
-         pure $ build_dir d ++ dirSep ++ efile
+         pure $ build_dir d </> efile
 
 getEntries : Directory -> IO (List String)
 getEntries d
@@ -206,42 +179,25 @@ dirEntries dir
          closeDir d
          pure (Right ds)
 
-findIpkg : List String -> Maybe String
-findIpkg [] = Nothing
-findIpkg (f :: fs)
-    = if isSuffixOf ".ipkg" f
-         then Just f
-         else findIpkg fs
-
-allDirs : String -> List String -> List (String, List String)
-allDirs path [] = []
-allDirs path ("" :: ds) = (dirSep, ds) ::allDirs path ds
-allDirs "" (d :: ds)
-    = let d' = if isWindows then d ++ dirSep else strCons sep d in 
-                (d', ds) :: allDirs d' ds
-allDirs path (d :: ds)
-    = let d' = path ++ strCons sep d in
-                (d', ds) :: allDirs d' ds
-
 -- Find an ipkg file in any of the directories above this one
 -- returns the directory, the ipkg file name, and the directories we've
 -- gone up
 export
-findIpkgFile : IO (Maybe (String, String, List String))
+covering
+findIpkgFile : IO (Maybe (String, String, String))
 findIpkgFile
     = do Just dir <- currentDir
               | Nothing => pure Nothing
-         -- 'paths' are the paths to look for an .ipkg, in order
-         let paths = reverse (allDirs "" (splitDir dir))
-         res <- firstIpkg paths
+         res <- findIpkgFile' dir ""
          pure res
   where
-    firstIpkg : List (String, List String) ->
-                IO (Maybe (String, String, List String))
-    firstIpkg [] = pure Nothing
-    firstIpkg ((d, up) :: ds)
-        = do Right files <- dirEntries d
-                   | Left err => pure Nothing
-             let Just f = findIpkg files
-                   | Nothing => firstIpkg ds
-             pure $ Just (d, f, up)
+    covering
+    findIpkgFile' : String -> String -> IO (Maybe (String, String, String))
+    findIpkgFile' dir up 
+        = do Right files <- dirEntries dir
+                 | Left err => pure Nothing
+             let Just f = find (\f => extension f == Just "ipkg") files
+                 | Nothing => case splitParent dir of
+                                   Just (parent, end) => findIpkgFile' parent (end </> up)
+                                   Nothing => pure Nothing
+             pure $ Just (dir, f, up)

src/Core/Env.idr

@@ -3,6 +3,8 @@ module Core.Env
 import Core.TT
 import Data.List
 
+%default total
+
 -- Environment containing types and values of local variables
 public export
 data Env : (tm : List Name -> Type) -> List Name -> Type where
@@ -119,6 +121,8 @@ export
 abstractFullEnvType : {vars : _} ->
                       FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
 abstractFullEnvType fc [] tm = tm
+abstractFullEnvType fc (Pi c e ty :: env) tm
+    = abstractFullEnvType fc env (Bind fc _ (Pi c e ty) tm)
 abstractFullEnvType fc (b :: env) tm
     = abstractFullEnvType fc env (Bind fc _
 						(Pi (multiplicity b) Explicit (binderType b)) tm)

src/Core/FC.idr

@@ -1,5 +1,7 @@
 module Core.FC
 
+%default total
+
 public export
 FilePos : Type
 FilePos = (Int, Int)

src/Core/GetType.idr

@@ -103,6 +103,10 @@ mutual
   chkConstant : FC -> Constant -> Term vars
   chkConstant fc (I x) = PrimVal fc IntType
   chkConstant fc (BI x) = PrimVal fc IntegerType
+  chkConstant fc (B8 x) = PrimVal fc Bits8Type
+  chkConstant fc (B16 x) = PrimVal fc Bits16Type
+  chkConstant fc (B32 x) = PrimVal fc Bits32Type
+  chkConstant fc (B64 x) = PrimVal fc Bits64Type
   chkConstant fc (Str x) = PrimVal fc StringType
   chkConstant fc (Ch x) = PrimVal fc CharType
   chkConstant fc (Db x) = PrimVal fc DoubleType

src/Core/LinearCheck.idr

@@ -215,7 +215,9 @@ mutual
            Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
                 | _ => throw (UndefinedName fc n)
            let expand = branchZero
-                          False
+                          (case type gdef of
+                                Erased _ _ => True -- defined elsewhere, need to expand
+                                _ => False)
                           (case definition gdef of
                                 (PMDef _ _ _ _ _) => True
                                 _ => False)

src/Core/Metadata.idr

@@ -10,10 +10,10 @@ import Core.TT
 import Core.TTC
 
 import Data.List
-
+import System.File
 import Utils.Binary
 
-import System.File
+%default covering
 
 -- Additional data we keep about the context to support interactive editing
 

src/Core/Normalise.idr

@@ -969,6 +969,7 @@ logEnv lvl msg env
              dumpEnv bs
     dumpEnv {vs = x :: _} (b :: bs)
         = do logTermNF lvl (msg ++ ":" ++ show (multiplicity b) ++ " " ++
+                            show (piInfo b) ++ " " ++
                             show x) bs (binderType b)
              dumpEnv bs
 

src/Core/Options.idr

@@ -4,12 +4,15 @@ import Core.Core
 import Core.Name
 import Core.TT
 import Utils.Binary
+import Utils.Path
 
 import Data.List
 import Data.Strings
 
 import System.Info
 
+%default total
+
 public export
 record Dirs where
   constructor MkDirs
@@ -79,11 +82,15 @@ record PrimNames where
   fromCharName : Maybe Name
 
 public export
-data LangExt = Borrowing -- not yet implemented
+data LangExt
+     = ElabReflection
+     | Borrowing -- not yet implemented
 
 export
 Eq LangExt where
+  ElabReflection == ElabReflection = True
   Borrowing == Borrowing = True
+  _ == _ = False
 
 -- Other options relevant to the current session (so not to be saved in a TTC)
 public export
@@ -129,25 +136,9 @@ record Options where
   primnames : PrimNames
   extensions : List LangExt
 
-export
-isWindows : Bool
-isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
-
-export
-sep : Char
-sep = if isWindows then '\\' else '/'
-
-export
-dirSep : String
-dirSep = cast sep
-
-export
-pathSep : Char
-pathSep = if isWindows then ';' else ':'
-
 defaultDirs : Dirs
 defaultDirs = MkDirs "." Nothing "build" 
-                     ("build" ++ dirSep ++ "exec") 
+                     ("build" </> "exec") 
                      "/usr/local" ["."] [] []
 
 defaultPPrint : PPrinter

src/Core/Primitives.idr

@@ -33,12 +33,20 @@ unaryOp _ _ = Nothing
 castString : Vect 1 (NF vars) -> Maybe (NF vars)
 castString [NPrimVal fc (I i)] = Just (NPrimVal fc (Str (show i)))
 castString [NPrimVal fc (BI i)] = Just (NPrimVal fc (Str (show i)))
+castString [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Str (show i)))
+castString [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Str (show i)))
+castString [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Str (show i)))
+castString [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Str (show i)))
 castString [NPrimVal fc (Ch i)] = Just (NPrimVal fc (Str (stripQuotes (show i))))
 castString [NPrimVal fc (Db i)] = Just (NPrimVal fc (Str (show i)))
 castString _ = Nothing
 
 castInteger : Vect 1 (NF vars) -> Maybe (NF vars)
 castInteger [NPrimVal fc (I i)] = Just (NPrimVal fc (BI (cast i)))
+castInteger [NPrimVal fc (B8 i)] = Just (NPrimVal fc (BI (cast i)))
+castInteger [NPrimVal fc (B16 i)] = Just (NPrimVal fc (BI (cast i)))
+castInteger [NPrimVal fc (B32 i)] = Just (NPrimVal fc (BI (cast i)))
+castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI i))
 castInteger [NPrimVal fc (Ch i)] = Just (NPrimVal fc (BI (cast (cast {to=Int} i))))
 castInteger [NPrimVal fc (Db i)] = Just (NPrimVal fc (BI (cast i)))
 castInteger [NPrimVal fc (Str i)] = Just (NPrimVal fc (BI (cast i)))
@@ -46,11 +54,46 @@ castInteger _ = Nothing
 
 castInt : Vect 1 (NF vars) -> Maybe (NF vars)
 castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (fromInteger i)))
+castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I i))
+castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I i))
+castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I i))
 castInt [NPrimVal fc (Db i)] = Just (NPrimVal fc (I (cast i)))
 castInt [NPrimVal fc (Ch i)] = Just (NPrimVal fc (I (cast i)))
 castInt [NPrimVal fc (Str i)] = Just (NPrimVal fc (I (cast i)))
 castInt _ = Nothing
 
+castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
+castBits8 [NPrimVal fc (BI i)]
+    = let max = prim__shl_Int 1 8 in
+          if i > 0 -- oops, we don't have `rem` yet!
+             then Just (NPrimVal fc (B8 (fromInteger i `mod` max)))
+             else Just (NPrimVal fc (B8 (max + fromInteger i `mod` max)))
+castBits8 _ = Nothing
+
+castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)
+castBits16 [NPrimVal fc (BI i)]
+    = let max = prim__shl_Int 1 16 in
+          if i > 0 -- oops, we don't have `rem` yet!
+             then Just (NPrimVal fc (B16 (fromInteger i `mod` max)))
+             else Just (NPrimVal fc (B16 (max + fromInteger i `mod` max)))
+castBits16 _ = Nothing
+
+castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
+castBits32 [NPrimVal fc (BI i)]
+    = let max = prim__shl_Int 1 32 in
+          if i > 0 -- oops, we don't have `rem` yet!
+             then Just (NPrimVal fc (B32 (fromInteger i `mod` max)))
+             else Just (NPrimVal fc (B32 (max + fromInteger i `mod` max)))
+castBits32 _ = Nothing
+
+castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
+castBits64 [NPrimVal fc (BI i)]
+    = let max = prim__shl_Integer 1 64 in
+          if i > 0 -- oops, we don't have `rem` yet!
+             then Just (NPrimVal fc (B64 (i `mod` max)))
+             else Just (NPrimVal fc (B64 (max + i `mod` max)))
+castBits64 _ = Nothing
+
 castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
 castDouble [NPrimVal fc (I i)] = Just (NPrimVal fc (Db (cast i)))
 castDouble [NPrimVal fc (BI i)] = Just (NPrimVal fc (Db (cast i)))
@@ -107,6 +150,10 @@ strSubstr _ = Nothing
 add : Constant -> Constant -> Maybe Constant
 add (BI x) (BI y) = pure $ BI (x + y)
 add (I x) (I y) = pure $ I (x + y)
+add (B8 x) (B8 y) = pure $ B8 $ (x + y)
+add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` (prim__shl_Int 1 16)
+add (B32 x) (B32 y) = pure $ B32 $ (x + y) `mod` (prim__shl_Int 1 32)
+add (B64 x) (B64 y) = pure $ B64 $ (x + y) `mod` (prim__shl_Integer 1 64)
 add (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x + cast y))
 add (Db x) (Db y) = pure $ Db (x + y)
 add _ _ = Nothing
@@ -120,6 +167,10 @@ sub _ _ = Nothing
 
 mul : Constant -> Constant -> Maybe Constant
 mul (BI x) (BI y) = pure $ BI (x * y)
+mul (B8 x) (B8 y) = pure $ B8 $ (x * y) `mod` (prim__shl_Int 1 8)
+mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` (prim__shl_Int 1 16)
+mul (B32 x) (B32 y) = pure $ B32 $ (x * y) `mod` (prim__shl_Int 1 32)
+mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` (prim__shl_Integer 1 64)
 mul (I x) (I y) = pure $ I (x * y)
 mul (Db x) (Db y) = pure $ Db (x * y)
 mul _ _ = Nothing
@@ -142,25 +193,44 @@ mod _ _ = Nothing
 shiftl : Constant -> Constant -> Maybe Constant
 shiftl (I x) (I y) = pure $ I (shiftL x y)
 shiftl (BI x) (BI y) = pure $ BI (prim__shl_Integer x y)
+shiftl (B8 x) (B8 y) = pure $ B8 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 8)
+shiftl (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 16)
+shiftl (B32 x) (B32 y) = pure $ B32 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 32)
+shiftl (B64 x) (B64 y) = pure $ B64 $ (prim__shl_Integer x y) `mod` (prim__shl_Integer 1 64)
 shiftl _ _ = Nothing
 
 shiftr : Constant -> Constant -> Maybe Constant
 shiftr (I x) (I y) = pure $ I (shiftR x y)
 shiftr (BI x) (BI y) = pure $ BI (prim__shr_Integer x y)
+shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Int x y)
+shiftr (B16 x) (B16 y) = pure $ B16 $ (prim__shr_Int x y)
+shiftr (B32 x) (B32 y) = pure $ B32 $ (prim__shr_Int x y)
+shiftr (B64 x) (B64 y) = pure $ B64 $ (prim__shr_Integer x y)
 shiftr _ _ = Nothing
 
 band : Constant -> Constant -> Maybe Constant
 band (I x) (I y) = pure $ I (prim__and_Int x y)
 band (BI x) (BI y) = pure $ BI (prim__and_Integer x y)
+band (B8 x) (B8 y) = pure $ B8 (prim__and_Int x y)
+band (B16 x) (B16 y) = pure $ B16 (prim__and_Int x y)
+band (B32 x) (B32 y) = pure $ B32 (prim__and_Int x y)
+band (B64 x) (B64 y) = pure $ B64 (prim__and_Integer x y)
 band _ _ = Nothing
 
 bor : Constant -> Constant -> Maybe Constant
 bor (I x) (I y) = pure $ I (prim__or_Int x y)
 bor (BI x) (BI y) = pure $ BI (prim__or_Integer x y)
+bor (B8 x) (B8 y) = pure $ B8 (prim__or_Int x y)
+bor (B16 x) (B16 y) = pure $ B16 (prim__or_Int x y)
+bor (B32 x) (B32 y) = pure $ B32 (prim__or_Int x y)
+bor (B64 x) (B64 y) = pure $ B64 (prim__or_Integer x y)
 bor _ _ = Nothing
 
 bxor : Constant -> Constant -> Maybe Constant
 bxor (I x) (I y) = pure $ I (prim__xor_Int x y)
+bxor (B8 x) (B8 y) = pure $ B8 (prim__xor_Int x y)
+bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Int x y)
+bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Int x y)
 bxor _ _ = Nothing
 
 neg : Constant -> Maybe Constant
@@ -176,6 +246,10 @@ toInt False = I 0
 lt : Constant -> Constant -> Maybe Constant
 lt (I x) (I y) = pure $ toInt (x < y)
 lt (BI x) (BI y) = pure $ toInt (x < y)
+lt (B8 x) (B8 y) = pure $ toInt (x < y)
+lt (B16 x) (B16 y) = pure $ toInt (x < y)
+lt (B32 x) (B32 y) = pure $ toInt (x < y)
+lt (B64 x) (B64 y) = pure $ toInt (x < y)
 lt (Str x) (Str y) = pure $ toInt (x < y)
 lt (Ch x) (Ch y) = pure $ toInt (x < y)
 lt (Db x) (Db y) = pure $ toInt (x < y)
@@ -184,6 +258,10 @@ lt _ _ = Nothing
 lte : Constant -> Constant -> Maybe Constant
 lte (I x) (I y) = pure $ toInt (x <= y)
 lte (BI x) (BI y) = pure $ toInt (x <= y)
+lte (B8 x) (B8 y) = pure $ toInt (x <= y)
+lte (B16 x) (B16 y) = pure $ toInt (x <= y)
+lte (B32 x) (B32 y) = pure $ toInt (x <= y)
+lte (B64 x) (B64 y) = pure $ toInt (x <= y)
 lte (Str x) (Str y) = pure $ toInt (x <= y)
 lte (Ch x) (Ch y) = pure $ toInt (x <= y)
 lte (Db x) (Db y) = pure $ toInt (x <= y)
@@ -192,6 +270,10 @@ lte _ _ = Nothing
 eq : Constant -> Constant -> Maybe Constant
 eq (I x) (I y) = pure $ toInt (x == y)
 eq (BI x) (BI y) = pure $ toInt (x == y)
+eq (B8 x) (B8 y) = pure $ toInt (x == y)
+eq (B16 x) (B16 y) = pure $ toInt (x == y)
+eq (B32 x) (B32 y) = pure $ toInt (x == y)
+eq (B64 x) (B64 y) = pure $ toInt (x == y)
 eq (Str x) (Str y) = pure $ toInt (x == y)
 eq (Ch x) (Ch y) = pure $ toInt (x == y)
 eq (Db x) (Db y) = pure $ toInt (x == y)
@@ -200,6 +282,10 @@ eq _ _ = Nothing
 gte : Constant -> Constant -> Maybe Constant
 gte (I x) (I y) = pure $ toInt (x >= y)
 gte (BI x) (BI y) = pure $ toInt (x >= y)
+gte (B8 x) (B8 y) = pure $ toInt (x >= y)
+gte (B16 x) (B16 y) = pure $ toInt (x >= y)
+gte (B32 x) (B32 y) = pure $ toInt (x >= y)
+gte (B64 x) (B64 y) = pure $ toInt (x >= y)
 gte (Str x) (Str y) = pure $ toInt (x >= y)
 gte (Ch x) (Ch y) = pure $ toInt (x >= y)
 gte (Db x) (Db y) = pure $ toInt (x >= y)
@@ -208,6 +294,10 @@ gte _ _ = Nothing
 gt : Constant -> Constant -> Maybe Constant
 gt (I x) (I y) = pure $ toInt (x > y)
 gt (BI x) (BI y) = pure $ toInt (x > y)
+gt (B8 x) (B8 y) = pure $ toInt (x > y)
+gt (B16 x) (B16 y) = pure $ toInt (x > y)
+gt (B32 x) (B32 y) = pure $ toInt (x > y)
+gt (B64 x) (B64 y) = pure $ toInt (x > y)
 gt (Str x) (Str y) = pure $ toInt (x > y)
 gt (Ch x) (Ch y) = pure $ toInt (x > y)
 gt (Db x) (Db y) = pure $ toInt (x > y)
@@ -297,6 +387,10 @@ crashTy
 castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
 castTo IntType = castInt
 castTo IntegerType = castInteger
+castTo Bits8Type = castBits8
+castTo Bits16Type = castBits16
+castTo Bits32Type = castBits32
+castTo Bits64Type = castBits64
 castTo StringType = castString
 castTo CharType = castChar
 castTo DoubleType = castDouble
@@ -397,24 +491,24 @@ opName Crash = prim $ "crash"
 export
 allPrimitives : List Prim
 allPrimitives =
-    map (\t => MkPrim (Add t) (arithTy t) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
+    map (\t => MkPrim (Add t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
     map (\t => MkPrim (Sub t) (arithTy t) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
-    map (\t => MkPrim (Mul t) (arithTy t) isTotal) [IntType, IntegerType, DoubleType] ++
-    map (\t => MkPrim (Div t) (arithTy t) notCovering) [IntType, IntegerType, DoubleType] ++
-    map (\t => MkPrim (Mod t) (arithTy t) notCovering) [IntType, IntegerType] ++
+    map (\t => MkPrim (Mul t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, DoubleType] ++
+    map (\t => MkPrim (Div t) (arithTy t) notCovering) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, DoubleType] ++
+    map (\t => MkPrim (Mod t) (arithTy t) notCovering) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
     map (\t => MkPrim (Neg t) (predTy t t) isTotal) [IntType, IntegerType, DoubleType] ++
-    map (\t => MkPrim (ShiftL t) (arithTy t) isTotal) [IntType, IntegerType] ++
-    map (\t => MkPrim (ShiftR t) (arithTy t) isTotal) [IntType, IntegerType] ++
+    map (\t => MkPrim (ShiftL t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
+    map (\t => MkPrim (ShiftR t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
 
-    map (\t => MkPrim (BAnd t) (arithTy t) isTotal) [IntType, IntegerType] ++
-    map (\t => MkPrim (BOr t) (arithTy t) isTotal) [IntType, IntegerType] ++
-    map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType] ++
+    map (\t => MkPrim (BAnd t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
+    map (\t => MkPrim (BOr t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
+    map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType, Bits8Type, Bits16Type, Bits32Type] ++
 
-    map (\t => MkPrim (LT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
-    map (\t => MkPrim (LTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
-    map (\t => MkPrim (EQ t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
-    map (\t => MkPrim (GTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
-    map (\t => MkPrim (GT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
+    map (\t => MkPrim (LT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
+    map (\t => MkPrim (LTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
+    map (\t => MkPrim (EQ t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
+    map (\t => MkPrim (GTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
+    map (\t => MkPrim (GT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
 
     [MkPrim StrLength (predTy StringType IntType) isTotal,
      MkPrim StrHead (predTy StringType CharType) notCovering,
@@ -439,8 +533,13 @@ allPrimitives =
      MkPrim DoubleFloor doubleTy isTotal,
      MkPrim DoubleCeiling doubleTy isTotal] ++
 
-    map (\t => MkPrim (Cast t StringType) (predTy t StringType) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
-    map (\t => MkPrim (Cast t IntegerType) (predTy t IntegerType) isTotal) [StringType, IntType, CharType, DoubleType] ++
-    map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, CharType, DoubleType] ++
+    map (\t => MkPrim (Cast t StringType) (predTy t StringType) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
+    map (\t => MkPrim (Cast t IntegerType) (predTy t IntegerType) isTotal) [StringType, IntType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
+    map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, Bits8Type, Bits16Type, Bits32Type, CharType, DoubleType] ++
     map (\t => MkPrim (Cast t DoubleType) (predTy t DoubleType) isTotal) [StringType, IntType, IntegerType] ++
-    map (\t => MkPrim (Cast t CharType) (predTy t CharType) isTotal) [StringType, IntType]
+    map (\t => MkPrim (Cast t CharType) (predTy t CharType) isTotal) [StringType, IntType] ++
+
+    map (\t => MkPrim (Cast t Bits8Type) (predTy t Bits8Type) isTotal) [IntegerType] ++
+    map (\t => MkPrim (Cast t Bits16Type) (predTy t Bits16Type) isTotal) [IntegerType] ++
+    map (\t => MkPrim (Cast t Bits32Type) (predTy t Bits32Type) isTotal) [IntegerType] ++
+    map (\t => MkPrim (Cast t Bits64Type) (predTy t Bits64Type) isTotal) [IntegerType]

src/Core/Reflect.idr

@@ -0,0 +1,592 @@
+module Core.Reflect
+
+import Algebra.Semiring
+
+import Core.Context
+import Core.Env
+import Core.Normalise
+import Core.TT
+import Core.Value
+
+%default covering
+
+public export
+interface Reify a where
+  reify : {vars : _} ->
+          Defs -> NF vars -> Core a
+
+public export
+interface Reflect a where
+  reflect : {vars : _} ->
+            FC -> Defs -> (onLHS : Bool) ->
+            Env Term vars -> a -> Core (Term vars)
+
+export
+getCon : {vars : _} ->
+         FC -> Defs -> Name -> Core (Term vars)
+getCon fc defs n
+    = case !(lookupDefExact n (gamma defs)) of
+           Just (DCon t a _) => resolved (gamma defs) (Ref fc (DataCon t a) n)
+           Just (TCon t a _ _ _ _ _ _) => resolved (gamma defs) (Ref fc (TyCon t a) n)
+           Just _ => resolved (gamma defs) (Ref fc Func n)
+           _ => throw (UndefinedName fc n)
+
+export
+appCon : {vars : _} ->
+         FC -> Defs -> Name -> List (Term vars) -> Core (Term vars)
+appCon fc defs n args
+    = do fn <- getCon fc defs n
+         resolved (gamma defs) (apply fc fn args)
+
+export
+prelude : String -> Name
+prelude n = NS ["Prelude"] (UN n)
+
+export
+builtin : String -> Name
+builtin n = NS ["Builtin"] (UN n)
+
+export
+primio : String -> Name
+primio n = NS ["PrimIO"] (UN n)
+
+export
+reflection : String -> Name
+reflection n = NS ["Reflection", "Language"] (UN n)
+
+export
+reflectiontt : String -> Name
+reflectiontt n = NS ["TT", "Reflection", "Language"] (UN n)
+
+export
+reflectionttimp : String -> Name
+reflectionttimp n = NS ["TTImp", "Reflection", "Language"] (UN n)
+
+export
+cantReify : NF vars -> String -> Core a
+cantReify val ty
+    = throw (GenericMsg (getLoc val) ("Can't reify as " ++ ty))
+
+export
+cantReflect : FC -> String -> Core a
+cantReflect fc ty
+    = throw (GenericMsg fc ("Can't reflect as " ++ ty))
+
+export
+Reify () where
+  reify defs _ = pure ()
+
+export
+Reflect () where
+  reflect fc defs lhs env _ = getCon fc defs (builtin "MkUnit")
+
+export
+Reify String where
+  reify defs (NPrimVal _ (Str str)) = pure str
+  reify defs val = cantReify val "String"
+
+export
+Reflect String where
+  reflect fc defs lhs env x = pure (PrimVal fc (Str x))
+
+export
+Reify Int where
+  reify defs (NPrimVal _ (I v)) = pure v
+  reify defs val = cantReify val "Int"
+
+export
+Reflect Int where
+  reflect fc defs lhs env x = pure (PrimVal fc (I x))
+
+export
+Reify Integer where
+  reify defs (NPrimVal _ (BI v)) = pure v
+  reify defs val = cantReify val "Integer"
+
+export
+Reflect Integer where
+  reflect fc defs lhs env x = pure (PrimVal fc (BI x))
+
+export
+Reify Char where
+  reify defs (NPrimVal _ (Ch v)) = pure v
+  reify defs val = cantReify val "Char"
+
+export
+Reflect Char where
+  reflect fc defs lhs env x = pure (PrimVal fc (Ch x))
+
+export
+Reify Double where
+  reify defs (NPrimVal _ (Db v)) = pure v
+  reify defs val = cantReify val "Double"
+
+export
+Reflect Double where
+  reflect fc defs lhs env x = pure (PrimVal fc (Db x))
+
+export
+Reify Bool where
+  reify defs val@(NDCon _ n _ _ _)
+      = case !(full (gamma defs) n) of
+            NS _ (UN "True") => pure True
+            NS _ (UN "False") => pure False
+            _ => cantReify val "Bool"
+  reify defs val = cantReify val "Bool"
+
+export
+Reflect Bool where
+  reflect fc defs lhs env True = getCon fc defs (prelude "True")
+  reflect fc defs lhs env False = getCon fc defs (prelude "False")
+
+export
+Reify Nat where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "Z"), _) => pure Z
+             (NS _ (UN "S"), [k])
+                 => do k' <- reify defs !(evalClosure defs k)
+                       pure (S k')
+             _ => cantReify val "Nat"
+  reify defs val = cantReify val "Nat"
+
+export
+Reflect Nat where
+  reflect fc defs lhs env Z = getCon fc defs (prelude "Z")
+  reflect fc defs lhs env (S k)
+      = do k' <- reflect fc defs lhs env k
+           appCon fc defs (prelude "S") [k']
+
+export
+Reify a => Reify (List a) where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "Nil"), _) => pure []
+             (NS _ (UN "::"), [_, x, xs])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        xs' <- reify defs !(evalClosure defs xs)
+                        pure (x' :: xs')
+             _ => cantReify val "List"
+  reify defs val = cantReify val "List"
+
+export
+Reflect a => Reflect (List a) where
+  reflect fc defs lhs env [] = appCon fc defs (prelude "Nil") [Erased fc False]
+  reflect fc defs lhs env (x :: xs)
+      = do x' <- reflect fc defs lhs env x
+           xs' <- reflect fc defs lhs env xs
+           appCon fc defs (prelude "::") [Erased fc False, x', xs']
+
+export
+Reify a => Reify (Maybe a) where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "Nothing"), _) => pure Nothing
+             (NS _ (UN "Just"), [_, x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (Just x')
+             _ => cantReify val "Maybe"
+  reify defs val = cantReify val "Maybe"
+
+export
+Reflect a => Reflect (Maybe a) where
+  reflect fc defs lhs env Nothing = appCon fc defs (prelude "Nothing") [Erased fc False]
+  reflect fc defs lhs env (Just x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (prelude "Just") [Erased fc False, x']
+
+export
+(Reify a, Reify b) => Reify (a, b) where
+  reify defs val@(NDCon _ n _ _ [_, _, x, y])
+      = case (!(full (gamma defs) n)) of
+             NS _ (UN "MkPair")
+                 => do x' <- reify defs !(evalClosure defs x)
+                       y' <- reify defs !(evalClosure defs y)
+                       pure (x', y')
+             _ => cantReify val "Pair"
+  reify defs val = cantReify val "Pair"
+
+export
+(Reflect a, Reflect b) => Reflect (a, b) where
+  reflect fc defs lhs env (x, y)
+      = do x' <- reflect fc defs lhs env x
+           y' <- reflect fc defs lhs env y
+           appCon fc defs (builtin "MkPair") [Erased fc False, Erased fc False, x', y']
+
+export
+Reify Name where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "UN"), [str])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       pure (UN str')
+             (NS _ (UN "MN"), [str, i])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       i' <- reify defs !(evalClosure defs i)
+                       pure (MN str' i')
+             (NS _ (UN "NS"), [ns, n])
+                 => do ns' <- reify defs !(evalClosure defs ns)
+                       n' <- reify defs !(evalClosure defs n)
+                       pure (NS ns' n')
+             _ => cantReify val "Name"
+  reify defs val = cantReify val "Name"
+
+export
+Reflect Name where
+  reflect fc defs lhs env (UN x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "UN") [x']
+  reflect fc defs lhs env (MN x i)
+      = do x' <- reflect fc defs lhs env x
+           i' <- reflect fc defs lhs env i
+           appCon fc defs (reflectiontt "MN") [x', i']
+  reflect fc defs lhs env (NS ns n)
+      = do ns' <- reflect fc defs lhs env ns
+           n' <- reflect fc defs lhs env n
+           appCon fc defs (reflectiontt "NS") [ns', n']
+  reflect fc defs lhs env (Resolved i)
+      = case !(full (gamma defs) (Resolved i)) of
+             Resolved _ => cantReflect fc "Name"
+             n => reflect fc defs lhs env n
+  reflect fc defs lhs env val = cantReflect fc "Name"
+
+export
+Reify NameType where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "Bound"), _) => pure Bound
+             (NS _ (UN "Func"), _) => pure Func
+             (NS _ (UN "DataCon"), [t,i])
+                  => do t' <- reify defs !(evalClosure defs t)
+                        i' <- reify defs !(evalClosure defs i)
+                        pure (DataCon t' i')
+             (NS _ (UN "TyCon"), [t,i])
+                  => do t' <- reify defs !(evalClosure defs t)
+                        i' <- reify defs !(evalClosure defs i)
+                        pure (TyCon t' i')
+             _ => cantReify val "NameType"
+  reify defs val = cantReify val "NameType"
+
+export
+Reflect NameType where
+  reflect fc defs lhs env Bound = getCon fc defs (reflectiontt "Bound")
+  reflect fc defs lhs env Func = getCon fc defs (reflectiontt "Func")
+  reflect fc defs lhs env (DataCon t i)
+      = do t' <- reflect fc defs lhs env t
+           i' <- reflect fc defs lhs env i
+           appCon fc defs (reflectiontt "DataCon") [t', i']
+  reflect fc defs lhs env (TyCon t i)
+      = do t' <- reflect fc defs lhs env t
+           i' <- reflect fc defs lhs env i
+           appCon fc defs (reflectiontt "TyCon") [t', i']
+
+export
+Reify Constant where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "I"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (I x')
+             (NS _ (UN "BI"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (BI x')
+             (NS _ (UN "B8"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (B8 x')
+             (NS _ (UN "B16"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (B16 x')
+             (NS _ (UN "B32"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (B32 x')
+             (NS _ (UN "B64"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (B64 x')
+             (NS _ (UN "Str"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (Str x')
+             (NS _ (UN "Ch"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (Ch x')
+             (NS _ (UN "Db"), [x])
+                  => do x' <- reify defs !(evalClosure defs x)
+                        pure (Db x')
+             (NS _ (UN "WorldVal"), [])
+                  => pure WorldVal
+             (NS _ (UN "IntType"), [])
+                  => pure IntType
+             (NS _ (UN "IntegerType"), [])
+                  => pure IntegerType
+             (NS _ (UN "Bits8Type"), [])
+                  => pure Bits8Type
+             (NS _ (UN "Bits16Type"), [])
+                  => pure Bits16Type
+             (NS _ (UN "Bits32Type"), [])
+                  => pure Bits32Type
+             (NS _ (UN "Bits64Type"), [])
+                  => pure Bits64Type
+             (NS _ (UN "StringType"), [])
+                  => pure StringType
+             (NS _ (UN "CharType"), [])
+                  => pure CharType
+             (NS _ (UN "DoubleType"), [])
+                  => pure DoubleType
+             (NS _ (UN "WorldType"), [])
+                  => pure WorldType
+             _ => cantReify val "Constant"
+  reify defs val = cantReify val "Constant"
+
+export
+Reflect Constant where
+  reflect fc defs lhs env (I x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "I") [x']
+  reflect fc defs lhs env (BI x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "BI") [x']
+  reflect fc defs lhs env (B8 x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "B8") [x']
+  reflect fc defs lhs env (B16 x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "B16") [x']
+  reflect fc defs lhs env (B32 x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "B32") [x']
+  reflect fc defs lhs env (B64 x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "B64") [x']
+  reflect fc defs lhs env (Str x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "Str") [x']
+  reflect fc defs lhs env (Ch x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "Ch") [x']
+  reflect fc defs lhs env (Db x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "Db") [x']
+  reflect fc defs lhs env WorldVal
+      = getCon fc defs (reflectiontt "WorldVal")
+  reflect fc defs lhs env IntType
+      = getCon fc defs (reflectiontt "IntType")
+  reflect fc defs lhs env IntegerType
+      = getCon fc defs (reflectiontt "IntegerType")
+  reflect fc defs lhs env Bits8Type
+      = getCon fc defs (reflectiontt "Bits8Type")
+  reflect fc defs lhs env Bits16Type
+      = getCon fc defs (reflectiontt "Bits16Type")
+  reflect fc defs lhs env Bits32Type
+      = getCon fc defs (reflectiontt "Bits32Type")
+  reflect fc defs lhs env Bits64Type
+      = getCon fc defs (reflectiontt "Bits64Type")
+  reflect fc defs lhs env StringType
+      = getCon fc defs (reflectiontt "StringType")
+  reflect fc defs lhs env CharType
+      = getCon fc defs (reflectiontt "CharType")
+  reflect fc defs lhs env DoubleType
+      = getCon fc defs (reflectiontt "DoubleType")
+  reflect fc defs lhs env WorldType
+      = getCon fc defs (reflectiontt "WorldType")
+
+export
+Reify Visibility where
+  reify defs val@(NDCon _ n _ _ _)
+      = case !(full (gamma defs) n) of
+             NS _ (UN "Private") => pure Private
+             NS _ (UN "Export") => pure Export
+             NS _ (UN "Public") => pure Public
+             _ => cantReify val "Visibility"
+  reify defs val = cantReify val "Visibility"
+
+export
+Reflect Visibility where
+  reflect fc defs lhs env Private = getCon fc defs (reflectiontt "Private")
+  reflect fc defs lhs env Export = getCon fc defs (reflectiontt "Export")
+  reflect fc defs lhs env Public = getCon fc defs (reflectiontt "Public")
+
+export
+Reify TotalReq where
+  reify defs val@(NDCon _ n _ _ _)
+      = case !(full (gamma defs) n) of
+             NS _ (UN "Total") => pure Total
+             NS _ (UN "CoveringOnly") => pure CoveringOnly
+             NS _ (UN "PartialOK") => pure PartialOK
+             _ => cantReify val "TotalReq"
+  reify defs val = cantReify val "TotalReq"
+
+export
+Reflect TotalReq where
+  reflect fc defs lhs env Total = getCon fc defs (reflectiontt "Total")
+  reflect fc defs lhs env CoveringOnly = getCon fc defs (reflectiontt "CoveringOnly")
+  reflect fc defs lhs env PartialOK = getCon fc defs (reflectiontt "PartialOK")
+
+export
+Reify RigCount where
+  reify defs val@(NDCon _ n _ _ _)
+      = case !(full (gamma defs) n) of
+             NS _ (UN "M0") => pure erased
+             NS _ (UN "M1") => pure linear
+             NS _ (UN "MW") => pure top
+             _ => cantReify val "Count"
+  reify defs val = cantReify val "Count"
+
+export
+Reflect RigCount where
+  reflect fc defs lhs env r
+      = elimSemi (getCon fc defs (reflectiontt "M0"))
+                 (getCon fc defs (reflectiontt "M1"))
+                 (const (getCon fc defs (reflectiontt "MW")))
+                 r
+
+export
+Reify t => Reify (PiInfo t) where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "ImplicitArg"), _) => pure Implicit
+             (NS _ (UN "ExplicitArg"), _) => pure Explicit
+             (NS _ (UN "AutoImplicit"), _) => pure AutoImplicit
+             (NS _ (UN "DefImplicit"), [_, t])
+                 => do t' <- reify defs !(evalClosure defs t)
+                       pure (DefImplicit t')
+             _ => cantReify val "PiInfo"
+  reify defs val = cantReify val "PiInfo"
+
+export
+Reflect t => Reflect (PiInfo t) where
+  reflect fc defs lhs env Implicit
+      = appCon fc defs (reflectiontt "ImplicitArg") [Erased fc False]
+  reflect fc defs lhs env Explicit
+      = appCon fc defs (reflectiontt "ExplicitArg") [Erased fc False]
+  reflect fc defs lhs env AutoImplicit
+      = appCon fc defs (reflectiontt "AutoImplicit") [Erased fc False]
+  reflect fc defs lhs env (DefImplicit t)
+      = do t' <- reflect fc defs lhs env t
+           appCon fc defs (reflectiontt "DefImplicit") [Erased fc False, t']
+
+export
+Reify LazyReason where
+  reify defs val@(NDCon _ n _ _ _)
+      = case !(full (gamma defs) n) of
+             NS _ (UN "LInf") => pure LInf
+             NS _ (UN "LLazy") => pure LLazy
+             NS _ (UN "LUnknown") => pure LUnknown
+             _ => cantReify val "LazyReason"
+  reify defs val = cantReify val "LazyReason"
+
+export
+Reflect LazyReason where
+  reflect fc defs lhs env LInf = getCon fc defs (reflectiontt "LInf")
+  reflect fc defs lhs env LLazy = getCon fc defs (reflectiontt "LLazy")
+  reflect fc defs lhs env LUnknown = getCon fc defs (reflectiontt "LUnknown")
+
+export
+Reify FC where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (!(full (gamma defs) n), args) of
+             (NS _ (UN "MkFC"), [fn, start, end])
+                   => do fn' <- reify defs !(evalClosure defs fn)
+                         start' <- reify defs !(evalClosure defs start)
+                         end' <- reify defs !(evalClosure defs end)
+                         pure (MkFC fn' start' end')
+             (NS _ (UN "EmptyFC"), _) => pure EmptyFC
+             _ => cantReify val "FC"
+  reify defs val = cantReify val "FC"
+
+export
+Reflect FC where
+  reflect fc defs True env _ = pure $ Erased fc False
+  reflect fc defs lhs env (MkFC fn start end)
+      = do fn' <- reflect fc defs lhs env fn
+           start' <- reflect fc defs lhs env start
+           end' <- reflect fc defs lhs env end
+           appCon fc defs (reflectiontt "MkFC") [fn', start', end']
+  reflect fc defs lhs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")
+
+{-
+-- Reflection of well typed terms: We don't reify terms because that involves
+-- type checking, but we can reflect them
+
+-- TODO: Do we need this? Fix reify if we do.
+
+export
+Reflect (IsVar name idx vs) where
+  reflect fc defs lhs env First
+      = appCon fc defs (reflectiontt "First") [Erased fc False, Erased fc False]
+  reflect fc defs lhs env (Later p)
+      = do p' <- reflect fc defs lhs env p
+           appCon fc defs (reflectiontt "Later")
+                  [Erased fc False, Erased fc False,
+                   Erased fc False, Erased fc False, p']
+
+-- Assume terms are normalised so there's not Let bindings in particular
+export
+Reflect (Term vs) where
+  reflect fc defs lhs env (Local {name} lfc _ idx prf)
+      = do lfc' <- reflect fc defs lhs env lfc
+           idx' <- reflect fc defs lhs env idx
+           appCon fc defs (reflectiontt "Local")
+                  [Erased fc False, Erased fc False, lfc', idx', Erased fc False]
+  reflect fc defs lhs env (Ref rfc nt n)
+      = do rfc' <- reflect fc defs lhs env rfc
+           nt' <- reflect fc defs lhs env nt
+           n' <- reflect fc defs lhs env n
+           appCon fc defs (reflectiontt "Ref")
+                  [Erased fc False, rfc', nt', n']
+  reflect fc defs lhs env (Bind bfc x (Pi c p ty) sc)
+      = do bfc' <- reflect fc defs lhs env bfc
+           x' <- reflect fc defs lhs env x
+           c' <- reflect fc defs lhs env c
+           p' <- reflect fc defs lhs env p
+           ty' <- reflect fc defs lhs env ty
+           sc' <- reflect fc defs lhs env sc
+           appCon fc defs (reflectiontt "Pi")
+                  [Erased fc False, bfc', c', p', x', ty', sc']
+  reflect fc defs lhs env (Bind bfc x (Lam c p ty) sc)
+      = do bfc' <- reflect fc defs lhs env bfc
+           x' <- reflect fc defs lhs env x
+           c' <- reflect fc defs lhs env c
+           p' <- reflect fc defs lhs env p
+           ty' <- reflect fc defs lhs env ty
+           sc' <- reflect fc defs lhs env sc
+           appCon fc defs (reflectiontt "Lam")
+                  [Erased fc False, bfc', c', p', x', ty', sc']
+  reflect fc defs lhs env (App afc fn arg)
+      = do afc' <- reflect fc defs lhs env afc
+           fn' <- reflect fc defs lhs env fn
+           arg' <- reflect fc defs lhs env arg
+           appCon fc defs (reflectiontt "App")
+                  [Erased fc False, afc', fn', arg']
+  reflect fc defs lhs env (TDelayed dfc r tm)
+      = do dfc' <- reflect fc defs lhs env dfc
+           r' <- reflect fc defs lhs env r
+           tm' <- reflect fc defs lhs env tm
+           appCon fc defs (reflectiontt "TDelayed")
+                  [Erased fc False, dfc', r', tm']
+  reflect fc defs lhs env (TDelay dfc r ty tm)
+      = do dfc' <- reflect fc defs lhs env dfc
+           r' <- reflect fc defs lhs env r
+           ty' <- reflect fc defs lhs env ty
+           tm' <- reflect fc defs lhs env tm
+           appCon fc defs (reflectiontt "TDelay")
+                  [Erased fc False, dfc', r', ty', tm']
+  reflect fc defs lhs env (TForce dfc r tm)
+      = do dfc' <- reflect fc defs lhs env dfc
+           r' <- reflect fc defs lhs env r
+           tm' <- reflect fc defs lhs env tm
+           appCon fc defs (reflectiontt "TForce")
+                  [Erased fc False, r', dfc', tm']
+  reflect fc defs lhs env (PrimVal pfc c)
+      = do pfc' <- reflect fc defs lhs env pfc
+           c' <- reflect fc defs lhs env c
+           appCon fc defs (reflectiontt "PrimVal")
+                  [Erased fc False, pfc', c']
+  reflect fc defs lhs env (Erased efc _)
+      = do efc' <- reflect fc defs lhs env efc
+           appCon fc defs (reflectiontt "Erased")
+                  [Erased fc False, efc']
+  reflect fc defs lhs env (TType tfc)
+      = do tfc' <- reflect fc defs lhs env tfc
+           appCon fc defs (reflectiontt "TType")
+                  [Erased fc False, tfc']
+  reflect fc defs lhs env val = cantReflect fc "Term"
+  -}

src/Core/TT.idr

@@ -24,6 +24,11 @@ public export
 data Constant
     = I Int
     | BI Integer
+    | B8 Int -- For now, since we don't have Bits types. We need to
+                -- make sure the Integer remains in range
+    | B16 Int
+    | B32 Int
+    | B64 Integer
     | Str String
     | Ch Char
     | Db Double
@@ -31,6 +36,10 @@ data Constant
 
     | IntType
     | IntegerType
+    | Bits8Type
+    | Bits16Type
+    | Bits32Type
+    | Bits64Type
     | StringType
     | CharType
     | DoubleType
@@ -64,12 +73,20 @@ export
 Show Constant where
   show (I x) = show x
   show (BI x) = show x
+  show (B8 x) = show x
+  show (B16 x) = show x
+  show (B32 x) = show x
+  show (B64 x) = show x
   show (Str x) = show x
   show (Ch x) = show x
   show (Db x) = show x
   show WorldVal = "%MkWorld"
   show IntType = "Int"
   show IntegerType = "Integer"
+  show Bits8Type = "Bits8"
+  show Bits16Type = "Bits16"
+  show Bits32Type = "Bits32"
+  show Bits64Type = "Bits64"
   show StringType = "String"
   show CharType = "Char"
   show DoubleType = "Double"
@@ -79,12 +96,20 @@ export
 Eq Constant where
   (I x) == (I y) = x == y
   (BI x) == (BI y) = x == y
+  (B8 x) == (B8 y) = x == y
+  (B16 x) == (B16 y) = x == y
+  (B32 x) == (B32 y) = x == y
+  (B64 x) == (B64 y) = x == y
   (Str x) == (Str y) = x == y
   (Ch x) == (Ch y) = x == y
   (Db x) == (Db y) = x == y
   WorldVal == WorldVal = True
   IntType == IntType = True
   IntegerType == IntegerType = True
+  Bits8Type == Bits8Type = True
+  Bits16Type == Bits16Type = True
+  Bits32Type == Bits32Type = True
+  Bits64Type == Bits64Type = True
   StringType == StringType = True
   CharType == CharType = True
   DoubleType == DoubleType = True
@@ -97,10 +122,14 @@ constTag : Constant -> Int
 -- 1 = ->, 2 = Type
 constTag IntType = 3
 constTag IntegerType = 4
-constTag StringType = 5
-constTag CharType = 6
-constTag DoubleType = 7
-constTag WorldType = 8
+constTag Bits8Type = 5
+constTag Bits16Type = 6
+constTag Bits32Type = 7
+constTag Bits64Type = 8
+constTag StringType = 9
+constTag CharType = 10
+constTag DoubleType = 11
+constTag WorldType = 12
 constTag _ = 0
 
 -- All the internal operators, parameterised by their arity
@@ -256,6 +285,15 @@ multiplicity (PVar c p ty) = c
 multiplicity (PLet c val ty) = c
 multiplicity (PVTy c ty) = c
 
+export
+piInfo : Binder tm -> PiInfo tm
+piInfo (Lam c x ty) = x
+piInfo (Let c val ty) = Explicit
+piInfo (Pi c x ty) = x
+piInfo (PVar c p ty) = p
+piInfo (PLet c val ty) = Explicit
+piInfo (PVTy c ty) = Explicit
+
 export
 setMultiplicity : Binder tm -> RigCount -> Binder tm
 setMultiplicity (Lam c x ty) c' = Lam c' x ty
@@ -827,26 +865,28 @@ renameVarList prf (MkVar p) = renameLocalRef prf p
 
 export
 renameVars : CompatibleVars xs ys -> Term xs -> Term ys
-renameVars CompatPre tm = tm
-renameVars prf (Local fc r idx vprf)
-    = let MkVar vprf' = renameLocalRef prf vprf in
-          Local fc r _ vprf'
-renameVars prf (Ref fc x name) = Ref fc x name
-renameVars prf (Meta fc n i args)
-    = Meta fc n i (map (renameVars prf) args)
-renameVars prf (Bind fc x b scope)
-    = Bind fc x (map (renameVars prf) b) (renameVars (CompatExt prf) scope)
-renameVars prf (App fc fn arg)
-    = App fc (renameVars prf fn) (renameVars prf arg)
-renameVars prf (As fc s as tm)
-    = As fc s (renameVars prf as) (renameVars prf tm)
-renameVars prf (TDelayed fc r ty) = TDelayed fc r (renameVars prf ty)
-renameVars prf (TDelay fc r ty tm)
-    = TDelay fc r (renameVars prf ty) (renameVars prf tm)
-renameVars prf (TForce fc r x) = TForce fc r (renameVars prf x)
-renameVars prf (PrimVal fc c) = PrimVal fc c
-renameVars prf (Erased fc i) = Erased fc i
-renameVars prf (TType fc) = TType fc
+renameVars compat tm = believe_me tm -- no names in term, so it's identity
+-- This is how we would define it:
+-- renameVars CompatPre tm = tm
+-- renameVars prf (Local fc r idx vprf)
+--     = let MkVar vprf' = renameLocalRef prf vprf in
+--           Local fc r _ vprf'
+-- renameVars prf (Ref fc x name) = Ref fc x name
+-- renameVars prf (Meta fc n i args)
+--     = Meta fc n i (map (renameVars prf) args)
+-- renameVars prf (Bind fc x b scope)
+--     = Bind fc x (map (renameVars prf) b) (renameVars (CompatExt prf) scope)
+-- renameVars prf (App fc fn arg)
+--     = App fc (renameVars prf fn) (renameVars prf arg)
+-- renameVars prf (As fc s as tm)
+--     = As fc s (renameVars prf as) (renameVars prf tm)
+-- renameVars prf (TDelayed fc r ty) = TDelayed fc r (renameVars prf ty)
+-- renameVars prf (TDelay fc r ty tm)
+--     = TDelay fc r (renameVars prf ty) (renameVars prf tm)
+-- renameVars prf (TForce fc r x) = TForce fc r (renameVars prf x)
+-- renameVars prf (PrimVal fc c) = PrimVal fc c
+-- renameVars prf (Erased fc i) = Erased fc i
+-- renameVars prf (TType fc) = TType fc
 
 export
 renameTop : (m : Name) -> Term (n :: vars) -> Term (m :: vars)

src/Core/TTC.idr

@@ -107,32 +107,48 @@ export
 TTC Constant where
   toBuf b (I x) = do tag 0; toBuf b x
   toBuf b (BI x) = do tag 1; toBuf b x
-  toBuf b (Str x) = do tag 2; toBuf b x
-  toBuf b (Ch x) = do tag 3; toBuf b x
-  toBuf b (Db x) = do tag 4; toBuf b x
+  toBuf b (B8 x) = do tag 2; toBuf b x
+  toBuf b (B16 x) = do tag 3; toBuf b x
+  toBuf b (B32 x) = do tag 4; toBuf b x
+  toBuf b (B64 x) = do tag 5; toBuf b x
+  toBuf b (Str x) = do tag 6; toBuf b x
+  toBuf b (Ch x) = do tag 7; toBuf b x
+  toBuf b (Db x) = do tag 8; toBuf b x
 
-  toBuf b WorldVal = tag 5
-  toBuf b IntType = tag 6
-  toBuf b IntegerType = tag 7
-  toBuf b StringType = tag 8
-  toBuf b CharType = tag 9
-  toBuf b DoubleType = tag 10
-  toBuf b WorldType = tag 11
+  toBuf b WorldVal = tag 9
+  toBuf b IntType = tag 10
+  toBuf b IntegerType = tag 11
+  toBuf b Bits8Type = tag 12
+  toBuf b Bits16Type = tag 13
+  toBuf b Bits32Type = tag 14
+  toBuf b Bits64Type = tag 15
+  toBuf b StringType = tag 16
+  toBuf b CharType = tag 17
+  toBuf b DoubleType = tag 18
+  toBuf b WorldType = tag 19
 
   fromBuf b
       = case !getTag of
              0 => do x <- fromBuf b; pure (I x)
              1 => do x <- fromBuf b; pure (BI x)
-             2 => do x <- fromBuf b; pure (Str x)
-             3 => do x <- fromBuf b; pure (Ch x)
-             4 => do x <- fromBuf b; pure (Db x)
-             5 => pure WorldVal
-             6 => pure IntType
-             7 => pure IntegerType
-             8 => pure StringType
-             9 => pure CharType
-             10 => pure DoubleType
-             11 => pure WorldType
+             2 => do x <- fromBuf b; pure (B8 x)
+             3 => do x <- fromBuf b; pure (B16 x)
+             4 => do x <- fromBuf b; pure (B32 x)
+             5 => do x <- fromBuf b; pure (B64 x)
+             6 => do x <- fromBuf b; pure (Str x)
+             7 => do x <- fromBuf b; pure (Ch x)
+             8 => do x <- fromBuf b; pure (Db x)
+             9 => pure WorldVal
+             10 => pure IntType
+             11 => pure IntegerType
+             12 => pure Bits8Type
+             13 => pure Bits16Type
+             14 => pure Bits32Type
+             15 => pure Bits64Type
+             16 => pure StringType
+             17 => pure CharType
+             18 => pure DoubleType
+             19 => pure WorldType
              _ => corrupt "Constant"
 
 export
@@ -662,29 +678,31 @@ export
 TTC CFType where
   toBuf b CFUnit = tag 0
   toBuf b CFInt = tag 1
-  toBuf b CFString = tag 2
-  toBuf b CFDouble = tag 3
-  toBuf b CFChar = tag 4
-  toBuf b CFPtr = tag 5
-  toBuf b CFWorld = tag 6
-  toBuf b (CFFun s t) = do tag 7; toBuf b s; toBuf b t
-  toBuf b (CFIORes t) = do tag 8; toBuf b t
-  toBuf b (CFStruct n a) = do tag 9; toBuf b n; toBuf b a
-  toBuf b (CFUser n a) = do tag 10; toBuf b n; toBuf b a
+  toBuf b CFUnsigned = tag 2
+  toBuf b CFString = tag 3
+  toBuf b CFDouble = tag 4
+  toBuf b CFChar = tag 5
+  toBuf b CFPtr = tag 6
+  toBuf b CFWorld = tag 7
+  toBuf b (CFFun s t) = do tag 8; toBuf b s; toBuf b t
+  toBuf b (CFIORes t) = do tag 9; toBuf b t
+  toBuf b (CFStruct n a) = do tag 10; toBuf b n; toBuf b a
+  toBuf b (CFUser n a) = do tag 11; toBuf b n; toBuf b a
 
   fromBuf b
       = case !getTag of
              0 => pure CFUnit
              1 => pure CFInt
-             2 => pure CFString
-             3 => pure CFDouble
-             4 => pure CFChar
-             5 => pure CFPtr
-             6 => pure CFWorld
-             7 => do s <- fromBuf b; t <- fromBuf b; pure (CFFun s t)
-             8 => do t <- fromBuf b; pure (CFIORes t)
-             9 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
-             10 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
+             2 => pure CFUnsigned
+             3 => pure CFString
+             4 => pure CFDouble
+             5 => pure CFChar
+             6 => pure CFPtr
+             7 => pure CFWorld
+             8 => do s <- fromBuf b; t <- fromBuf b; pure (CFFun s t)
+             9 => do t <- fromBuf b; pure (CFIORes t)
+             10 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
+             11 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
              _ => corrupt "CFType"
 
 export
@@ -944,7 +962,8 @@ TTC GlobalDef where
            let refs = map fromList refsList
            def <- fromBuf b
            if isUserName name
-              then do ty <- fromBuf b; eargs <- fromBuf b;
+              then do ty <- fromBuf b
+                      eargs <- fromBuf b;
                       seargs <- fromBuf b; specargs <- fromBuf b
                       iargs <- fromBuf b;
                       vars <- fromBuf b

src/Core/Termination.idr

@@ -386,7 +386,7 @@ getSC : {auto c : Ref Ctxt Defs} ->
         Defs -> Def -> Core (List SCCall)
 getSC defs (PMDef _ args _ _ pats)
    = do sc <- traverse (findCalls defs) pats
-        pure (concat sc)
+        pure $ nub (concat sc)
 getSC defs _ = pure []
 
 export
@@ -421,8 +421,6 @@ initArgs (S k)
 -- Traverse the size change graph. When we reach a point we've seen before,
 -- at least one of the arguments must have got smaller, otherwise it's
 -- potentially non-terminating
--- TODO: If we encounter a name where we already know its termination status,
--- use that rather than continuing to traverse the graph!
 checkSC : {auto a : Ref APos Arg} ->
           {auto c : Ref Ctxt Defs} ->
           Defs ->
@@ -467,6 +465,11 @@ checkSC defs f args path
     checkCall : List (Name, List (Maybe Arg)) -> SCCall -> Core Terminating
     checkCall path sc
         = do let inpath = fnCall sc `elem` map fst path
+             Just gdef <- lookupCtxtExact (fnCall sc) (gamma defs)
+                  | Nothing => pure IsTerminating -- nothing to check
+             let Unchecked = isTerminating (totality gdef)
+                  | IsTerminating => pure IsTerminating
+                  | _ => pure (NotTerminating (BadCall [fnCall sc]))
              term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
              if not inpath
                 then case term of

src/Core/Transform.idr

@@ -7,6 +7,8 @@ import Core.TT
 
 import Data.NameMap
 
+%default total
+
 unload : List (FC, Term vars) -> Term vars -> Term vars
 unload [] fn = fn
 unload ((fc, arg) :: args) fn = unload args (App fc fn arg)
@@ -35,7 +37,7 @@ addMatch idx p val ms
                            else Nothing
 
 -- LHS of a rule must be a function application, so there's not much work
--- to do here! 
+-- to do here!
 match : MatchVars vars vs ->
         Term vars -> Term vs -> Maybe (MatchVars vars vs)
 match ms (Local _ _ idx p) val
@@ -48,6 +50,7 @@ match ms x y
          then Just ms
          else Nothing
 
+covering
 tryReplace : MatchVars vars vs -> Term vars -> Maybe (Term vs)
 tryReplace ms (Local _ _ idx p) = lookupMatch idx p ms
 tryReplace ms (Ref fc nt n) = pure (Ref fc nt n)
@@ -80,6 +83,7 @@ tryReplace ms (PrimVal fc c) = pure (PrimVal fc c)
 tryReplace ms (Erased fc i) = pure (Erased fc i)
 tryReplace ms (TType fc) = pure (TType fc)
 
+covering
 tryApply : Transform -> Term vs -> Maybe (Term vs)
 tryApply trans@(MkTransform {vars} n _ lhs rhs) tm
    = case match None lhs tm of
@@ -100,6 +104,7 @@ apply (t :: ts) tm
 
 data Upd : Type where
 
+covering
 trans : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref Upd Bool} ->
         Env Term vars -> List (FC, Term vars) -> Term vars ->
@@ -135,6 +140,7 @@ trans env stk (TForce fc r tm)
          pure $ unload stk (TForce fc r tm')
 trans env stk tm = pure $ unload stk tm
 
+covering
 transLoop : {auto c : Ref Ctxt Defs} ->
             Nat -> Env Term vars -> Term vars -> Core (Term vars)
 transLoop Z env tm = pure tm
@@ -148,6 +154,7 @@ transLoop (S k) env tm
             else pure tm'
 
 export
+covering
 applyTransforms : {auto c : Ref Ctxt Defs} ->
                   Env Term vars -> Term vars -> Core (Term vars)
 applyTransforms env tm = transLoop 5 env tm

src/Core/Unify.idr

@@ -1335,7 +1335,7 @@ retry mode c
                              _ => pure cs
   where
     definedN : Name -> Core Bool
-    definedN n
+    definedN n@(NS _ (MN _ _)) -- a metavar will only ever be a MN
         = do defs <- get Ctxt
              Just gdef <- lookupCtxtExact n (gamma defs)
                   | _ => pure False
@@ -1344,6 +1344,7 @@ retry mode c
                   BySearch _ _ _ => pure False
                   Guess _ _ _ => pure False
                   _ => pure True
+    definedN _ = pure True
 
 delayMeta : {vars : _} ->
             LazyReason -> Nat -> Term vars -> Term vars -> Term vars

src/Core/Value.idr

@@ -7,6 +7,8 @@ import Core.TT
 
 import Data.IntMap
 
+%default covering
+
 public export
 record EvalOpts where
   constructor MkEvalOpts

src/Data/ANameMap.idr

@@ -7,6 +7,8 @@ import Data.List
 import Data.NameMap
 import Data.StringMap
 
+%default total
+
 export
 record ANameMap a where
      constructor MkANameMap

src/Data/Bool/Extra.idr

@@ -1,5 +1,7 @@
 module Data.Bool.Extra
 
+%default total
+
 public export
 andSameNeutral : (x : Bool) -> x && x = x
 andSameNeutral False = Refl

src/Data/IntMap.idr

@@ -2,7 +2,7 @@ module Data.IntMap
 
 -- Hand specialised map, for efficiency...
 
-%default covering
+%default total
 
 Key : Type
 Key = Int

src/Data/LengthMatch.idr

@@ -1,5 +1,7 @@
 module Data.LengthMatch
 
+%default total
+
 public export
 data LengthMatch : List a -> List b -> Type where
      NilMatch : LengthMatch [] []

src/Data/List/Extra.idr

@@ -1,6 +1,6 @@
 module Data.List.Extra
 
-%default covering
+%default total
 
 ||| Fetches the element at a given position.
 ||| Returns `Nothing` if the position beyond the list's end.

src/Data/NameMap.idr

@@ -4,7 +4,7 @@ import Core.Name
 
 -- Hand specialised map, for efficiency...
 
-%default covering
+%default total
 
 Key : Type
 Key = Name

src/Data/StringMap.idr

@@ -2,7 +2,7 @@ module Data.StringMap
 
 -- Hand specialised map, for efficiency...
 
-%default covering
+%default total
 
 Key : Type
 Key = String

src/Idris/Desugar.idr

@@ -248,10 +248,11 @@ mutual
   desugarB side ps (PPrimVal fc x) = pure $ IPrimVal fc x
   desugarB side ps (PQuote fc tm)
       = pure $ IQuote fc !(desugarB side ps tm)
+  desugarB side ps (PQuoteName fc n)
+      = pure $ IQuoteName fc n
   desugarB side ps (PQuoteDecl fc x)
-      = do [x'] <- desugarDecl ps x
-              | _ => throw (GenericMsg fc "Can't quote this declaration")
-           pure $ IQuoteDecl fc x'
+      = do xs <- traverse (desugarDecl ps) x
+           pure $ IQuoteDecl fc (concat xs)
   desugarB side ps (PUnquote fc tm)
       = pure $ IUnquote fc !(desugarB side ps tm)
   desugarB side ps (PRunElab fc tm)
@@ -481,7 +482,7 @@ mutual
                 {auto u : Ref UST UState} ->
                 {auto m : Ref MD Metadata} ->
                 List Name -> PTypeDecl -> Core ImpTy
-  desugarType ps (MkPTy fc n ty)
+  desugarType ps (MkPTy fc n d ty)
       = do syn <- get Syn
            pure $ MkImpTy fc n !(bindTypeNames (usingImpl syn)
                                                ps !(desugar AnyExpr ps ty))
@@ -499,11 +500,11 @@ mutual
                      (case ws of
                            [] => rhs'
                            _ => ILocal fc (concat ws) rhs')
-  desugarClause ps arg (MkWithClause fc lhs wval cs)
+  desugarClause ps arg (MkWithClause fc lhs wval flags cs)
       = do cs' <- traverse (desugarClause ps arg) cs
            (bound, blhs) <- bindNames arg !(desugar LHS ps lhs)
            wval' <- desugar AnyExpr (bound ++ ps) wval
-           pure $ WithClause fc blhs wval' cs'
+           pure $ WithClause fc blhs wval' flags cs'
   desugarClause ps arg (MkImpossible fc lhs)
       = do dlhs <- desugar LHS ps lhs
            pure $ ImpossibleClause fc (snd !(bindNames arg dlhs))
@@ -555,7 +556,7 @@ mutual
   getDecl AsType d@(PClaim _ _ _ _ _) = Just d
   getDecl AsType (PData fc vis (MkPData dfc tyn tyc _ _))
       = Just (PData fc vis (MkPLater dfc tyn tyc))
-  getDecl AsType d@(PInterface _ _ _ _ _ _ _ _) = Just d
+  getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d
   getDecl AsType d@(PRecord fc vis n ps _ _)
       = Just (PData fc vis (MkPLater fc n (mkRecType ps)))
     where
@@ -568,7 +569,7 @@ mutual
 
   getDecl AsDef (PClaim _ _ _ _ _) = Nothing
   getDecl AsDef d@(PData _ _ (MkPLater _ _ _)) = Just d
-  getDecl AsDef (PInterface _ _ _ _ _ _ _ _) = Nothing
+  getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing
   getDecl AsDef d@(PRecord _ _ _ _ _ _) = Just d
   getDecl AsDef (PFixity _ _ _ _) = Nothing
   getDecl AsDef (PDirective _ _) = Nothing
@@ -624,8 +625,8 @@ mutual
       toIDef : ImpClause -> Core ImpDecl
       toIDef (PatClause fc lhs rhs)
           = pure $ IDef fc !(getFn lhs) [PatClause fc lhs rhs]
-      toIDef (WithClause fc lhs rhs cs)
-          = pure $ IDef fc !(getFn lhs) [WithClause fc lhs rhs cs]
+      toIDef (WithClause fc lhs rhs flags cs)
+          = pure $ IDef fc !(getFn lhs) [WithClause fc lhs rhs flags cs]
       toIDef (ImpossibleClause fc lhs)
           = pure $ IDef fc !(getFn lhs) [ImpossibleClause fc lhs]
 
@@ -658,7 +659,7 @@ mutual
   desugarDecl ps (PReflect fc tm)
       = throw (GenericMsg fc "Reflection not implemented yet")
 --       pure [IReflect fc !(desugar AnyExpr ps tm)]
-  desugarDecl ps (PInterface fc vis cons_in tn params det conname body)
+  desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
       = do let cons = concatMap expandConstraint cons_in
            cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ map fst params)
                                                          (snd ntm)
@@ -795,6 +796,9 @@ mutual
       = do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
            rhs' <- desugar AnyExpr (bound ++ ps) rhs
            pure [ITransform fc (UN n) blhs rhs']
+  desugarDecl ps (PRunElabDecl fc tm)
+      = do tm' <- desugar AnyExpr ps tm
+           pure [IRunElabDecl fc tm']
   desugarDecl ps (PDirective fc d)
       = case d of
              Hide n => pure [IPragma (\nest, env => hide fc n)]

src/Idris/Elab/Implementation.idr

@@ -215,6 +215,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                unsetFlag fc impName BlockedHint
 
                setFlag fc impName TCInline
+               -- it's the methods we're interested in, not the implementation
+               setFlag fc impName (SetTotal PartialOK)
 
                -- 4. (TODO: Order method bodies to be in declaration order, in
                --    case of dependencies)
@@ -225,9 +227,13 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                log 10 $ "Implementation body: " ++ show body'
                traverse (processDecl [] nest env) body'
 
-               -- 6. Add transnformation rules for top level methods
+               -- 6. Add transformation rules for top level methods
                traverse (addTransform impName upds) (methods cdata)
 
+               -- inline flag has done its job, and outside the interface
+               -- it can hurt, so unset it now
+               unsetFlag fc impName TCInline
+
                -- Reset the open hints (remove the named implementation)
                setOpenHints hs
                pure ()) mbody
@@ -270,7 +276,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     -- inserted in the right place
     mkMethField : List (Name, RigCount, RawImp) ->
                   List (Name, List (Name, RigCount, PiInfo RawImp)) ->
-                  (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> RawImp
+                  (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp
     mkMethField methImps fldTys (topn, n, upds, c, treq, ty)
         = let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys))
               imps = map fst methImps in
@@ -311,8 +317,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     topMethType : List (Name, RawImp) ->
                   Name -> List (Name, RigCount, RawImp) ->
                   List String -> List Name -> List Name ->
-                  (Name, RigCount, TotalReq, (Bool, RawImp)) ->
-                  Core ((Name, Name, List (String, String), RigCount, TotalReq, RawImp),
+                  (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
+                  Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),
                            List (Name, RawImp))
     topMethType methupds impName methImps impsp pnames allmeths (mn, c, treq, (d, mty_in))
         = do -- Get the specialised type by applying the method to the
@@ -353,17 +359,18 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     topMethTypes : List (Name, RawImp) ->
                    Name -> List (Name, RigCount, RawImp) ->
                    List String -> List Name -> List Name ->
-                   List (Name, RigCount, TotalReq, (Bool, RawImp)) ->
-                   Core (List (Name, Name, List (String, String), RigCount, TotalReq, RawImp))
+                   List (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
+                   Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp))
     topMethTypes upds impName methImps impsp pnames allmeths [] = pure []
     topMethTypes upds impName methImps impsp pnames allmeths (m :: ms)
         = do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m
              ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms
              pure (m' :: ms')
 
-    mkTopMethDecl : (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> ImpDecl
+    mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl
     mkTopMethDecl (mn, n, upds, c, treq, mty)
-        = IClaim fc c vis (Totality treq :: opts_in) (MkImpTy fc n mty)
+        = let opts = maybe opts_in (\t => Totality t :: opts_in) treq in
+              IClaim fc c vis opts (MkImpTy fc n mty)
 
     -- Given the method type (result of topMethType) return the mapping from
     -- top level method name to current implementation's method name
@@ -396,10 +403,10 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     updateClause ns (PatClause fc lhs rhs)
         = do lhs' <- updateApp ns lhs
              pure (PatClause fc lhs' rhs)
-    updateClause ns (WithClause fc lhs wval cs)
+    updateClause ns (WithClause fc lhs wval flags cs)
         = do lhs' <- updateApp ns lhs
              cs' <- traverse (updateClause ns) cs
-             pure (WithClause fc lhs' wval cs')
+             pure (WithClause fc lhs' wval flags cs')
     updateClause ns (ImpossibleClause fc lhs)
         = do lhs' <- updateApp ns lhs
              pure (ImpossibleClause fc lhs')
@@ -414,7 +421,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                    "Implementation body can only contain definitions")
 
     addTransform : Name -> List (Name, Name) ->
-                   (Name, RigCount, TotalReq, Bool, RawImp) ->
+                   (Name, RigCount, Maybe TotalReq, Bool, RawImp) ->
                    Core ()
     addTransform iname ns (top, _, _, _, ty)
         = do log 3 $ "Adding transform for " ++ show top ++ " : " ++ show ty ++

src/Idris/Elab/Interface.idr

@@ -23,6 +23,8 @@ import Data.ANameMap
 import Data.List
 import Data.Maybe
 
+%default covering
+
 -- TODO: Check all the parts of the body are legal
 -- TODO: Deal with default superclass implementations
 
@@ -243,9 +245,9 @@ updateIfaceSyn iname cn ps cs ms ds
     findSetTotal (_ :: xs) = findSetTotal xs
 
     totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) ->
-              Core (Name, RigCount, TotalReq, (Bool, RawImp))
+              Core (Name, RigCount, Maybe TotalReq, (Bool, RawImp))
     totMeth (n, c, opts, t)
-        = do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
+        = do let treq = findSetTotal opts
              pure (n, c, treq, t)
 
 export
@@ -393,9 +395,9 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
         changeName : Name -> ImpClause -> ImpClause
         changeName dn (PatClause fc lhs rhs)
             = PatClause fc (changeNameTerm dn lhs) rhs
-        changeName dn (WithClause fc lhs wval cs)
+        changeName dn (WithClause fc lhs wval flags cs)
             = WithClause fc (changeNameTerm dn lhs) wval
-                         (map (changeName dn) cs)
+                         flags (map (changeName dn) cs)
         changeName dn (ImpossibleClause fc lhs)
             = ImpossibleClause fc (changeNameTerm dn lhs)
 

src/Idris/Error.idr

@@ -167,16 +167,17 @@ perror (BadUnboundImplicit _ env n ty)
     = pure $ "Can't bind name " ++ nameRoot n ++ " with type " ++ !(pshow env ty)
                ++ " here. Try binding explicitly."
 perror (CantSolveGoal _ env g)
-    = let (_ ** (env', g')) = dropPis env g in
+    = let (_ ** (env', g')) = dropEnv env g in
           pure $ "Can't find an implementation for " ++ !(pshow env' g')
   where
     -- For display, we don't want to see the full top level type; just the
     -- return type
-    dropPis : {vars : _} ->
+    dropEnv : {vars : _} ->
               Env Term vars -> Term vars ->
               (ns ** (Env Term ns, Term ns))
-    dropPis env (Bind _ n b@(Pi _ _ _) sc) = dropPis (b :: env) sc
-    dropPis env tm = (_ ** (env, tm))
+    dropEnv env (Bind _ n b@(Pi _ _ _) sc) = dropEnv (b :: env) sc
+    dropEnv env (Bind _ n b@(Let _ _ _) sc) = dropEnv (b :: env) sc
+    dropEnv env tm = (_ ** (env, tm))
 
 perror (DeterminingArg _ n i env g)
     = pure $ "Can't find an implementation for " ++ !(pshow env g) ++ "\n" ++
@@ -195,8 +196,8 @@ perror (SolvedNamedHole _ env h tm)
     = pure $ "Named hole " ++ show h ++ " has been solved by unification\n"
               ++ "Result: " ++ !(pshow env tm)
 perror (VisibilityError fc vx x vy y)
-    = pure $ show vx ++ " " ++ sugarName x ++
-             " cannot refer to " ++ show vy ++ " " ++ sugarName y
+    = pure $ show vx ++ " " ++ sugarName !(toFullNames x) ++
+             " cannot refer to " ++ show vy ++ " " ++ sugarName !(toFullNames y)
 perror (NonLinearPattern _ n) = pure $ "Non linear pattern " ++ sugarName n
 perror (BadPattern _ n) = pure $ "Pattern not allowed here: " ++ show n
 perror (NoDeclaration _ n) = pure $ "No type declaration for " ++ show n
@@ -245,6 +246,7 @@ perror (CyclicImports ns)
     showMod ns = showSep "." (reverse ns)
 perror ForceNeeded = pure "Internal error when resolving implicit laziness"
 perror (InternalError str) = pure $ "INTERNAL ERROR: " ++ str
+perror (UserError str) = pure $ "Error: " ++ str
 
 perror (InType fc n err)
     = pure $ "While processing type of " ++ !(prettyName n) ++

src/Idris/IDEMode/Commands.idr

@@ -6,7 +6,7 @@ import public Idris.REPLOpts
 
 import System.File
 
-%default covering
+%default total
 
 public export
 data SExp = SExpList (List SExp)
@@ -186,7 +186,7 @@ escape = pack . concatMap escapeChar . unpack
 
 export
 Show SExp where
-  show (SExpList xs) = "(" ++ showSep " " (map show xs) ++ ")"
+  show (SExpList xs) = assert_total $ "(" ++ showSep " " (map show xs) ++ ")"
   show (StringAtom str) = "\"" ++ escape str ++ "\""
   show (BoolAtom b) = ":" ++ show b
   show (IntegerAtom i) = show i

src/Idris/IDEMode/Holes.idr

@@ -7,14 +7,16 @@ import Idris.Syntax
 
 import Idris.IDEMode.Commands
 
+%default covering
+
 public export
 record HolePremise where
   constructor MkHolePremise
   name         : Name
   type         : PTerm
-  multiplicity : RigCount  
+  multiplicity : RigCount
   isImplicit   : Bool
-  
+
 
 public export
 record HoleData where
@@ -25,7 +27,7 @@ record HoleData where
 
 ||| If input is a hole, return number of locals in scope at binding
 ||| point
-export  
+export
 isHole : GlobalDef -> Maybe Nat
 isHole def
     = case definition def of

src/Idris/IDEMode/MakeClause.idr

@@ -8,6 +8,8 @@ import Data.List
 import Data.Nat
 import Data.Strings
 
+%default total
+
 -- Implement make-with and make-case from the IDE mode
 
 showRHSName : Name -> String

src/Idris/IDEMode/Parser.idr

@@ -14,6 +14,8 @@ import Text.Parser
 import Utils.Either
 import Utils.String
 
+%default total
+
 %hide Text.Lexer.symbols
 %hide Parser.Lexer.Source.symbols
 
@@ -42,6 +44,7 @@ idelex str
                           Comment _ => False
                           _ => True
 
+covering
 sexp : Rule SExp
 sexp
     = do symbol ":"; exactIdent "True"
@@ -67,6 +70,7 @@ ideParser str p
 
 
 export
+covering
 parseSExp : String -> Either (ParseError Token) SExp
 parseSExp inp
     = ideParser inp (do c <- sexp; eoi; pure c)

src/Idris/IDEMode/REPL.idr

@@ -45,6 +45,8 @@ import System.File
 import Network.Socket
 import Network.Socket.Data
 
+%default covering
+
 %foreign "C:fdopen,libc 6"
 prim__fdopen : Int -> String -> PrimIO AnyPtr
 

src/Idris/IDEMode/SyntaxHighlight.idr

@@ -10,6 +10,8 @@ import Idris.IDEMode.Commands
 
 import Data.List
 
+%default covering
+
 data Decoration : Type where
   Typ : Decoration
   Function : Decoration

src/Idris/IDEMode/TokenLine.idr

@@ -4,6 +4,8 @@ module Idris.IDEMode.TokenLine
 import Parser.Lexer.Source
 import Text.Lexer
 
+%default total
+
 public export
 RawName : Type
 RawName = String

src/Idris/Main.idr

@@ -1,38 +1,31 @@
 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 IdrisPaths
+
 import Data.So
 import Data.Strings
-import Data.Vect
 import System
 import System.Directory
 import System.File
+import Utils.Path
 
 import Yaffle.Main
 
-import IdrisPaths
-
 %default covering
 
 findInput : List CLOpt -> Maybe String
@@ -50,15 +43,15 @@ updateEnv
               Nothing => setPrefix yprefix
          bpath <- coreLift $ getEnv "IDRIS2_PATH"
          the (Core ()) $ case bpath of
-              Just path => do traverse_ addExtraDir (map trim (split (==pathSep) path))
+              Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path))
               Nothing => pure ()
          bdata <- coreLift $ getEnv "IDRIS2_DATA"
          the (Core ()) $ case bdata of
-              Just path => do traverse_ addDataDir (map trim (split (==pathSep) path))
+              Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path))
               Nothing => pure ()
          blibs <- coreLift $ getEnv "IDRIS2_LIBS"
          the (Core ()) $ case blibs of
-              Just path => do traverse_ addLibDir (map trim (split (==pathSep) path))
+              Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path))
               Nothing => pure ()
          cg <- coreLift $ getEnv "IDRIS2_CG"
          the (Core ()) $ case cg of
@@ -74,10 +67,10 @@ updateEnv
          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")
+         addDataDir (dir_prefix (dirs (options defs)) </>
+                        ("idris2-" ++ showVersion False version) </> "support")
+         addLibDir (dir_prefix (dirs (options defs)) </>
+                        ("idris2-" ++ showVersion False version) </> "lib")
          Just cwd <- coreLift $ currentDir
               | Nothing => throw (InternalError "Can't get current directory")
          addLibDir cwd
@@ -171,6 +164,7 @@ stMain opts
                  fname <- if findipkg session
                              then findIpkg fname
                              else pure fname
+                 setMainFile fname
                  the (Core ()) $ case fname of
                       Nothing => logTime "Loading prelude" $
                                    when (not $ noprelude session) $

src/Idris/ModTree.idr

@@ -126,7 +126,7 @@ getBuildMods : {auto c : Ref Ctxt Defs} ->
 getBuildMods loc done fname
     = do a <- newRef AllMods []
          d <- getDirs
-         let fname_ns = pathToNS (working_dir d) (source_dir d) fname
+         fname_ns <- pathToNS (working_dir d) (source_dir d) fname
          if fname_ns `elem` map buildNS done
             then pure []
             else
@@ -158,7 +158,7 @@ buildMod loc num len mod
    = do clearCtxt; addPrimitives
         lazyActive True; setUnboundImplicits True
         let src = buildFile mod
-        mttc <- getTTCFileName src ".ttc"
+        mttc <- getTTCFileName src "ttc"
         -- We'd expect any errors in nsToPath to have been caught by now
         -- since the imports have been built! But we still have to check.
         depFilesE <- traverse (nsToPath loc) (imports mod)
@@ -230,12 +230,12 @@ buildDeps fname
               [] => do -- On success, reload the main ttc in a clean context
                        clearCtxt; addPrimitives
                        put MD initMetadata
-                       mainttc <- getTTCFileName fname ".ttc"
-                       log 10 $ "Reloading " ++ show mainttc
+                       mainttc <- getTTCFileName fname "ttc"
+                       log 10 $ "Reloading " ++ show mainttc ++ " from " ++ fname
                        readAsMain mainttc
 
                        -- Load the associated metadata for interactive editing
-                       mainttm <- getTTCFileName fname ".ttm"
+                       mainttm <- getTTCFileName fname "ttm"
                        log 10 $ "Reloading " ++ show mainttm
                        readFromTTM mainttm
                        pure []

src/Idris/Package.idr

@@ -25,6 +25,7 @@ import System.File
 import Text.Parser
 import Utils.Binary
 import Utils.String
+import Utils.Path
 
 import Idris.CommandLine
 import Idris.ModTree
@@ -303,11 +304,11 @@ 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)
+    = do let ttcfile = joinPath (reverse ns)
+         let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
+         let destPath = destdir </> joinPath (reverse dns)
+         let destFile = destdir </> ttcfile <.> "ttc"
+         Right _ <- coreLift $ mkdirAll $ joinPath (reverse dns)
              | Left err => throw (InternalError ("Can't make directories " ++ show (reverse dns)))
          coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
          Right _ <- coreLift $ copyFile ttcPath destFile
@@ -332,11 +333,11 @@ install pkg opts -- not used but might be in the future
          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
+         let installPrefix = dir_prefix (dirs (options defs)) </>
+                             "idris2-" ++ showVersion False version
          True <- coreLift $ changeDir installPrefix
              | False => throw (InternalError ("Can't change directory to " ++ installPrefix))
-         Right _ <- coreLift $ mkdirs [name pkg]
+         Right _ <- coreLift $ mkdirAll (name pkg)
              | Left err => throw (InternalError ("Can't make directory " ++ name pkg))
          True <- coreLift $ changeDir (name pkg)
              | False => throw (InternalError ("Can't change directory to " ++ name pkg))
@@ -344,8 +345,8 @@ install pkg opts -- not used but might be in the future
          -- 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
+                               (srcdir </> build)
+                               (installPrefix </> name pkg)) toInstall
          coreLift $ changeDir srcdir
          runScript (postinstall pkg)
 
@@ -403,8 +404,8 @@ clean pkg opts -- `opts` is not used but might be in the future
                                        (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
+         let builddir = srcdir </> build </> "ttc"
+         let execdir = srcdir </> exec
          -- the usual pair syntax breaks with `No such variable a` here for some reason
          let pkgTrie = the (StringTrie (List String)) $
                        foldl (\trie, ksv =>
@@ -416,7 +417,7 @@ clean pkg opts -- `opts` is not used but might be in the future
                        (\ks => map concat . traverse (deleteBin builddir ks))
                        pkgTrie
          deleteFolder builddir []
-         maybe (pure ()) (\e => delete (execdir ++ dirSep ++ e))
+         maybe (pure ()) (\e => delete (execdir </> e))
                (executable pkg)
          runScript (postclean pkg)
   where
@@ -426,13 +427,13 @@ clean pkg opts -- `opts` is not used but might be in the future
                      coreLift $ putStrLn $ "Removed: " ++ path
 
     deleteFolder : String -> List String -> Core ()
-    deleteFolder builddir ns = delete $ builddir ++ dirSep ++ showSep dirSep ns
+    deleteFolder builddir ns = delete $ builddir </> joinPath 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"
+        = do let ttFile = builddir </> joinPath ns </> mod
+             delete $ ttFile <.> "ttc"
+             delete $ ttFile <.> "ttm"
 
 getParseErrorLoc : String -> ParseError Token -> FC
 getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
@@ -551,6 +552,7 @@ findIpkg fname
    = do Just (dir, ipkgn, up) <- coreLift findIpkgFile
              | Nothing => pure fname
         coreLift $ changeDir dir
+        setWorkingDir dir
         Right (pname, fs) <- coreLift $ parseFile ipkgn
                                  (do desc <- parsePkgDesc ipkgn
                                      eoi
@@ -563,8 +565,8 @@ findIpkg fname
         loadDependencies (depends pkg)
         case fname of
              Nothing => pure Nothing
-             Just src =>
-                do let src' = showSep dirSep (up ++ [src])
+             Just srcpath  =>
+                do let src' = up </> srcpath 
                    setSource src'
                    opts <- get ROpts
                    put ROpts (record { mainfile = Just src' } opts)

src/Idris/Parser.idr

@@ -49,13 +49,17 @@ plhs = MkParseOpts False False
 atom : FileName -> Rule PTerm
 atom fname
     = do start <- location
-         x <- constant
-         end <- location
-         pure (PPrimVal (MkFC fname start end) x)
-  <|> do start <- location
          exactIdent "Type"
          end <- location
          pure (PType (MkFC fname start end))
+  <|> do start <- location
+         x <- name
+         end <- location
+         pure (PRef (MkFC fname start end) x)
+  <|> do start <- location
+         x <- constant
+         end <- location
+         pure (PPrimVal (MkFC fname start end) x)
   <|> do start <- location
          symbol "_"
          end <- location
@@ -80,10 +84,6 @@ atom fname
          pragma "search"
          end <- location
          pure (PSearch (MkFC fname start end) 50)
-  <|> do start <- location
-         x <- name
-         end <- location
-         pure (PRef (MkFC fname start end) x)
 
 whereBlock : FileName -> Int -> Rule (List PDecl)
 whereBlock fname col
@@ -379,6 +379,18 @@ mutual
            symbol ")"
            end <- location
            pure (PQuote (MkFC fname start end) e)
+    <|> do start <- location
+           symbol "`{{"
+           n <- name
+           symbol "}}"
+           end <- location
+           pure (PQuoteName (MkFC fname start end) n)
+    <|> do start <- location
+           symbol "`["
+           ns <- nonEmptyBlock (topDecl fname)
+           symbol "]"
+           end <- location
+           pure (PQuoteDecl (MkFC fname start end) (collectDefs (concat ns)))
     <|> do start <- location
            symbol "~"
            e <- simpleExpr fname indents
@@ -401,6 +413,11 @@ mutual
            symbol "|]"
            end <- location
            pure (PIdiom (MkFC fname start end) e)
+    <|> do start <- location
+           pragma "runElab"
+           e <- expr pdef fname indents
+           end <- location
+           pure (PRunElab (MkFC fname start end) e)
     <|> do start <- location
            pragma "logging"
            lvl <- intLit
@@ -850,13 +867,21 @@ visibility
 tyDecl : FileName -> IndentInfo -> Rule PTypeDecl
 tyDecl fname indents
     = do start <- location
-         n <- name
+         doc   <- option "" documentation
+         n     <- name
          symbol ":"
          mustWork $
-            do ty <- expr pdef fname indents
+            do ty  <- expr pdef fname indents
                end <- location
                atEnd indents
-               pure (MkPTy (MkFC fname start end) n ty)
+               pure (MkPTy (MkFC fname start end) n doc ty)
+
+withFlags : SourceEmptyRule (List WithFlag)
+withFlags
+    = do pragma "syntactic"
+         fs <- withFlags
+         pure $ Syntactic :: fs
+  <|> pure []
 
 mutual
   parseRHS : (withArgs : Nat) ->
@@ -872,11 +897,12 @@ mutual
                  pure (MkPatClause (MkFC fname start end) lhs rhs ws)
      <|> do keyword "with"
             wstart <- location
+            flags <- withFlags
             symbol "("
             wval <- bracketedExpr fname wstart indents
             ws <- nonEmptyBlock (clause (S withArgs) fname)
             end <- location
-            pure (MkWithClause (MkFC fname start end) lhs wval ws)
+            pure (MkWithClause (MkFC fname start end) lhs wval flags ws)
      <|> do keyword "impossible"
             atEnd indents
             end <- location
@@ -933,13 +959,14 @@ mkDataConType fc ret (WithArg a :: xs)
 
 simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
 simpleCon fname ret indents
-    = do start <- location
-         cname <- name
+    = do start  <- location
+         cdoc   <- option "" documentation
+         cname  <- name
          params <- many (argExpr plhs fname indents)
          atEnd indents
          end <- location
-         pure (let cfc = MkFC fname start end in 
-                   MkPTy cfc cname (mkDataConType cfc ret params))
+         pure (let cfc = MkFC fname start end in
+                   MkPTy cfc cname cdoc (mkDataConType cfc ret params))
 
 simpleData : FileName -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
 simpleData fname start n indents
@@ -1003,9 +1030,10 @@ dataDeclBody fname indents
 dataDecl : FileName -> IndentInfo -> Rule PDecl
 dataDecl fname indents
     = do start <- location
-         vis <- visibility
-         dat <- dataDeclBody fname indents
-         end <- location
+         doc   <- option "" documentation
+         vis   <- visibility
+         dat   <- dataDeclBody fname indents
+         end   <- location
          pure (PData (MkFC fname start end) vis dat)
 
 stripBraces : String -> String
@@ -1024,7 +1052,9 @@ onoff
 
 extension : Rule LangExt
 extension
-    = do exactIdent "Borrowing"
+    = do exactIdent "ElabReflection"
+         pure ElabReflection
+  <|> do exactIdent "Borrowing"
          pure Borrowing
 
 totalityOpt : Rule TotalReq
@@ -1128,9 +1158,10 @@ namespaceHead
 namespaceDecl : FileName -> IndentInfo -> Rule PDecl
 namespaceDecl fname indents
     = do start <- location
-         ns <- namespaceHead
-         end <- location
-         ds <- assert_total (nonEmptyBlock (topDecl fname))
+         doc   <- option "" documentation
+         ns    <- namespaceHead
+         end   <- location
+         ds    <- assert_total (nonEmptyBlock (topDecl fname))
          pure (PNamespace (MkFC fname start end) ns (concat ds))
 
 transformDecl : FileName -> IndentInfo -> Rule PDecl
@@ -1144,6 +1175,14 @@ transformDecl fname indents
          end <- location
          pure (PTransform (MkFC fname start end) n lhs rhs)
 
+runElabDecl : FileName -> IndentInfo -> Rule PDecl
+runElabDecl fname indents
+    = do start <- location
+         pragma "runElab"
+         tm <- expr pnowith fname indents
+         end <- location
+         pure (PRunElabDecl (MkFC fname start end) tm)
+
 mutualDecls : FileName -> IndentInfo -> Rule PDecl
 mutualDecls fname indents
     = do start <- location
@@ -1284,29 +1323,33 @@ ifaceParam fname indents
 ifaceDecl : FileName -> IndentInfo -> Rule PDecl
 ifaceDecl fname indents
     = do start <- location
-         vis <- visibility
-         col <- column
+         doc   <- option "" documentation
+         vis   <- visibility
+         col   <- column
          keyword "interface"
          commit
-         cons <- constraints fname indents
-         n <- name
+         cons   <- constraints fname indents
+         n      <- name
          params <- many (ifaceParam fname indents)
-         det <- option [] (do symbol "|"
-                              sepBy (symbol ",") name)
+         det    <- option []
+                     (do symbol "|"
+                         sepBy (symbol ",") name)
          keyword "where"
-         dc <- option Nothing (do exactIdent "constructor"
-                                  n <- name
-                                  pure (Just n))
+         dc <- option Nothing
+                 (do exactIdent "constructor"
+                     n <- name
+                     pure (Just n))
          body <- assert_total (blockAfter col (topDecl fname))
-         end <- location
+         end  <- location
          pure (PInterface (MkFC fname start end)
-                      vis cons n params det dc (collectDefs (concat body)))
+                      vis cons n doc params det dc (collectDefs (concat body)))
 
 implDecl : FileName -> IndentInfo -> Rule PDecl
 implDecl fname indents
-    = do start <- location
+    = do start   <- location
+         doc     <- option "" documentation
          visOpts <- many (visOpt fname)
-         vis <- getVisibility Nothing visOpts
+         vis     <- getVisibility Nothing visOpts
          let opts = mapMaybe getRight visOpts
          col <- column
          option () (keyword "implementation")
@@ -1314,9 +1357,9 @@ implDecl fname indents
                                      iname <- name
                                      symbol "]"
                                      pure (Just iname))
-         impls <- implBinds fname indents
-         cons <- constraints fname indents
-         n <- name
+         impls  <- implBinds fname indents
+         cons   <- constraints fname indents
+         n      <- name
          params <- many (simpleExpr fname indents)
          nusing <- option [] (do keyword "using"
                                  names <- some name
@@ -1331,13 +1374,15 @@ implDecl fname indents
 
 fieldDecl : FileName -> IndentInfo -> Rule (List PField)
 fieldDecl fname indents
-      = do symbol "{"
+      = do doc <- option "" documentation
+           symbol "{"
            commit
            fs <- fieldBody Implicit
            symbol "}"
            atEnd indents
            pure fs
-    <|> do fs <- fieldBody Explicit
+    <|> do doc <- option "" documentation
+           fs <- fieldBody Explicit
            atEnd indents
            pure fs
   where
@@ -1381,15 +1426,16 @@ recordParam fname indents
 recordDecl : FileName -> IndentInfo -> Rule PDecl
 recordDecl fname indents
     = do start <- location
-         vis <- visibility
-         col <- column
+         doc   <- option "" documentation
+         vis   <- visibility
+         col   <- column
          keyword "record"
-         n <- name
+         n       <- name
          paramss <- many (recordParam fname indents)
          let params = concat paramss
          keyword "where"
          dcflds <- blockWithOptHeaderAfter col ctor (fieldDecl fname)
-         end <- location
+         end    <- location
          pure (PRecord (MkFC fname start end)
                        vis n params (fst dcflds) (concat (snd dcflds)))
   where
@@ -1401,21 +1447,23 @@ recordDecl fname indents
 
 claim : FileName -> IndentInfo -> Rule PDecl
 claim fname indents
-    = do start <- location
+    = do start   <- location
+         doc     <- option "" documentation
          visOpts <- many (visOpt fname)
-         vis <- getVisibility Nothing visOpts
+         vis     <- getVisibility Nothing visOpts
          let opts = mapMaybe getRight visOpts
-         m <- multiplicity
+         m   <- multiplicity
          rig <- getMult m
-         cl <- tyDecl fname indents
+         cl  <- tyDecl fname indents
          end <- location
          pure (PClaim (MkFC fname start end) rig vis opts cl)
 
 definition : FileName -> IndentInfo -> Rule PDecl
 definition fname indents
     = do start <- location
-         nd <- clause 0 fname indents
-         end <- location
+         doc   <- option "" documentation
+         nd    <- clause 0 fname indents
+         end   <- location
          pure (PDef (MkFC fname start end) [nd])
 
 fixDecl : FileName -> IndentInfo -> Rule (List PDecl)
@@ -1465,6 +1513,8 @@ topDecl fname indents
          pure [d]
   <|> do d <- usingDecls fname indents
          pure [d]
+  <|> do d <- runElabDecl fname indents
+         pure [d]
   <|> do d <- transformDecl fname indents
          pure [d]
   <|> do d <- directiveDecl fname indents
@@ -1527,27 +1577,29 @@ import_ fname indents
 export
 prog : FileName -> SourceEmptyRule Module
 prog fname
-    = do start <- location
+    = do start  <- location
+         doc    <- option "" documentation
          nspace <- option ["Main"]
-                      (do keyword "module"
-                          namespacedIdent)
-         end <- location
+                     (do keyword "module"
+                         namespacedIdent)
+         end     <- location
          imports <- block (import_ fname)
-         ds <- block (topDecl fname)
+         ds      <- block (topDecl fname)
          pure (MkModule (MkFC fname start end)
-                        nspace imports (collectDefs (concat ds)))
+                        nspace imports doc (collectDefs (concat ds)))
 
 export
 progHdr : FileName -> SourceEmptyRule Module
 progHdr fname
-    = do start <- location
+    = do start  <- location
+         doc    <- option "" documentation
          nspace <- option ["Main"]
-                      (do keyword "module"
-                          namespacedIdent)
-         end <- location
+                     (do keyword "module"
+                         namespacedIdent)
+         end     <- location
          imports <- block (import_ fname)
          pure (MkModule (MkFC fname start end)
-                        nspace imports [])
+                        nspace imports doc [])
 
 parseMode : Rule REPLEval
 parseMode

src/Idris/ProcessIdr.idr

@@ -28,6 +28,8 @@ import Data.NameMap
 
 import System.File
 
+%default covering
+
 processDecl : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
@@ -95,17 +97,12 @@ readImport full imp
 
 readHash : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
-           Import -> Core (List String, Int)
+           Import -> Core (Bool, (List String, Int))
 readHash imp
     = do Right fname <- nsToPath (loc imp) (path imp)
                | Left err => throw err
          h <- readIFaceHash fname
-         -- If the import is a 'public' import, then it forms part of
-         -- our own interface so add its hash to our hash
-         when (reexport imp) $
-            do log 5 $ "Reexporting " ++ show (path imp) ++ " hash " ++ show h
-               addHash h
-         pure (nameAs imp, h)
+         pure (reexport imp, (nameAs imp, h))
 
 prelude : Import
 prelude = MkImport (MkFC "(implicit)" (0, 0) (0, 0)) False
@@ -208,6 +205,12 @@ prim__gc : Int -> PrimIO ()
 gc : IO ()
 gc = primIO $ prim__gc 4
 
+export
+addPublicHash : {auto c : Ref Ctxt Defs} ->
+                (Bool, (List String, Int)) -> Core ()
+addPublicHash (True, (mod, h)) = do addHash mod; addHash h
+addPublicHash _ = pure ()
+
 -- Process everything in the module; return the syntax information which
 -- needs to be written to the TTC (e.g. exported infix operators)
 -- Returns 'Nothing' if it didn't reload anything
@@ -234,7 +237,7 @@ processMod srcf ttcf msg sourcecode
         defs <- get Ctxt
         log 5 $ "Current hash " ++ show (ifaceHash defs)
         log 5 $ show (moduleNS modh) ++ " hashes:\n" ++
-                show (sort hs)
+                show (sort (map snd hs))
         imphs <- readImportHashes ttcf
         log 5 $ "Old hashes from " ++ ttcf ++ ":\n" ++ show (sort imphs)
 
@@ -246,7 +249,7 @@ processMod srcf ttcf msg sourcecode
 
         let ns = moduleNS modh
 
-        if (sort hs == sort imphs && srctime <= ttctime)
+        if (sort (map snd hs) == sort imphs && srctime <= ttctime)
            then -- Hashes the same, source up to date, just set the namespace
                 -- for the REPL
                 do setNS ns
@@ -257,11 +260,13 @@ processMod srcf ttcf msg sourcecode
                             pure (runParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
                       | Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err])
                 initHash
+                traverse addPublicHash (sort hs)
                 resetNextVar
                 when (ns /= ["Main"]) $
                    do let MkFC fname _ _ = headerloc mod
                       d <- getDirs
-                      when (pathToNS (working_dir d) (source_dir d) fname /= ns) $
+                      ns' <- pathToNS (working_dir d) (source_dir d) fname
+                      when (ns /= ns') $
                           throw (GenericMsg (headerloc mod)
                                    ("Module name " ++ showSep "." (reverse ns) ++
                                     " does not match file name " ++ fname))
@@ -289,7 +294,7 @@ processMod srcf ttcf msg sourcecode
                 -- If they haven't changed next time, and the source
                 -- file hasn't changed, no need to rebuild.
                 defs <- get Ctxt
-                put Ctxt (record { importHashes = hs } defs)
+                put Ctxt (record { importHashes = map snd hs } defs)
                 pure (Just errs))
           (\err => pure (Just [err]))
 
@@ -306,7 +311,7 @@ process : {auto c : Ref Ctxt Defs} ->
 process buildmsg file
     = do Right res <- coreLift (readFile file)
                | Left err => pure [FileErr file err]
-         catch (do ttcf <- getTTCFileName file ".ttc"
+         catch (do ttcf <- getTTCFileName file "ttc"
                    Just errs <- logTime ("Elaborating " ++ file) $
                                    processMod file ttcf buildmsg res
                         | Nothing => pure [] -- skipped it
@@ -314,9 +319,10 @@ process buildmsg file
                       then
                         do defs <- get Ctxt
                            d <- getDirs
-                           makeBuildDirectory (pathToNS (working_dir d) (source_dir d) file)
+                           ns <- pathToNS (working_dir d) (source_dir d) file
+                           makeBuildDirectory ns
                            writeToTTC !(get Syn) ttcf
-                           ttmf <- getTTCFileName file ".ttm"
+                           ttmf <- getTTCFileName file "ttm"
                            writeToTTM ttmf
                            pure []
                       else do pure errs)

src/Idris/REPL.idr

@@ -188,7 +188,7 @@ 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)
+printClause l i (WithClause _ lhsraw wvraw flags csraw)
     = do lhs <- pterm lhsraw
          wval <- pterm wvraw
          cs <- traverse (printClause l (i + 2)) csraw

src/Idris/REPLCommon.idr

@@ -13,6 +13,8 @@ import Idris.Syntax
 
 import Data.List
 
+%default covering
+
 -- Output informational messages, unless quiet flag is set
 export
 iputStrLn : {auto o : Ref ROpts REPLOpts} ->

src/Idris/REPLOpts.idr

@@ -5,6 +5,8 @@ import Idris.Syntax
 import Data.Strings
 import System.File
 
+%default total
+
 public export
 data OutputMode
   = IDEMode Integer File File
@@ -45,6 +47,13 @@ getOutput : {auto o : Ref ROpts REPLOpts} -> Core OutputMode
 getOutput = do opts <- get ROpts
                pure (idemode opts)
 
+export
+setMainFile : {auto o : Ref ROpts REPLOpts} ->
+              Maybe String -> Core ()
+setMainFile src
+    = do opts <- get ROpts
+         put ROpts (record { mainfile = src } opts)
+
 export
 setSource : {auto o : Ref ROpts REPLOpts} ->
             String -> Core ()

src/Idris/Resugar.idr

@@ -240,11 +240,10 @@ mutual
   toPTerm p (IDelay fc tm) = pure (PDelay fc !(toPTerm argPrec tm))
   toPTerm p (IForce fc tm) = pure (PForce fc !(toPTerm argPrec tm))
   toPTerm p (IQuote fc tm) = pure (PQuote fc !(toPTerm argPrec tm))
-  toPTerm p (IQuoteDecl fc d)
-      = do md <- toPDecl d
-           case md of
-                Nothing => throw (InternalError "Can't resugar log or pragma")
-                Just d' => pure (PQuoteDecl fc d')
+  toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n)
+  toPTerm p (IQuoteDecl fc ds)
+      = do ds' <- traverse toPDecl ds
+           pure $ PQuoteDecl fc (mapMaybe id ds')
   toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
   toPTerm p (IRunElab fc tm) = pure (PRunElab fc !(toPTerm argPrec tm))
 
@@ -312,9 +311,10 @@ mutual
       = pure (MkPatClause fc !(toPTerm startPrec lhs)
                              !(toPTerm startPrec rhs)
                              [])
-  toPClause (WithClause fc lhs rhs cs)
+  toPClause (WithClause fc lhs rhs flags cs)
       = pure (MkWithClause fc !(toPTerm startPrec lhs)
                               !(toPTerm startPrec rhs)
+                              flags
                               !(traverse toPClause cs))
   toPClause (ImpossibleClause fc lhs)
       = pure (MkImpossible fc !(toPTerm startPrec lhs))
@@ -323,7 +323,7 @@ mutual
                 {auto s : Ref Syn SyntaxInfo} ->
                 ImpTy -> Core PTypeDecl
   toPTypeDecl (MkImpTy fc n ty)
-      = pure (MkPTy fc n !(toPTerm startPrec ty))
+      = pure (MkPTy fc n "" !(toPTerm startPrec ty))
 
   toPData : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
@@ -394,6 +394,8 @@ mutual
       = pure (Just (PTransform fc (show n)
                                   !(toPTerm startPrec lhs)
                                   !(toPTerm startPrec rhs)))
+  toPDecl (IRunElabDecl fc tm)
+      = pure (Just (PRunElabDecl fc !(toPTerm startPrec tm)))
   toPDecl (IPragma _) = pure Nothing
   toPDecl (ILog _) = pure Nothing
 

src/Idris/SetOptions.idr

@@ -5,6 +5,7 @@ import Core.Directory
 import Core.Metadata
 import Core.Options
 import Core.Unify
+import Utils.Path
 
 import Idris.CommandLine
 import Idris.REPL
@@ -16,19 +17,21 @@ import IdrisPaths
 import Data.So
 import System
 
+%default covering
+
 -- 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)
+         addExtraDir (dir_prefix (dirs (options defs)) </>
+                             "idris2-" ++ showVersion False version </> p)
 
 dirOption : Dirs -> DirCommand -> Core ()
 dirOption dirs LibDir
     = coreLift $ putStrLn
-         (dir_prefix dirs ++ dirSep ++ "idris2-" ++ showVersion False version ++ dirSep)
+         (dir_prefix dirs </> "idris2-" ++ showVersion False version)
 
 -- Options to be processed before type checking. Return whether to continue.
 export

src/Idris/Syntax.idr

@@ -53,7 +53,8 @@ mutual
        PSearch : FC -> (depth : Nat) -> PTerm
        PPrimVal : FC -> Constant -> PTerm
        PQuote : FC -> PTerm -> PTerm
-       PQuoteDecl : FC -> PDecl -> PTerm
+       PQuoteName : FC -> Name -> PTerm
+       PQuoteDecl : FC -> List PDecl -> PTerm
        PUnquote : FC -> PTerm -> PTerm
        PRunElab : FC -> PTerm -> PTerm
        PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm
@@ -131,7 +132,7 @@ mutual
 
   public export
   data PTypeDecl : Type where
-       MkPTy : FC -> (n : Name) -> (type : PTerm) -> PTypeDecl
+       MkPTy : FC -> (n : Name) -> (doc: String) -> (type : PTerm) -> PTypeDecl
 
   public export
   data PDataDecl : Type where
@@ -145,7 +146,7 @@ mutual
        MkPatClause : FC -> (lhs : PTerm) -> (rhs : PTerm) ->
                      (whereblock : List PDecl) -> PClause
        MkWithClause : FC -> (lhs : PTerm) -> (wval : PTerm) ->
-                        List PClause -> PClause
+                      List WithFlag -> List PClause -> PClause
        MkImpossible : FC -> (lhs : PTerm) -> PClause
 
   public export
@@ -209,6 +210,7 @@ mutual
                     Visibility ->
                     (constraints : List (Maybe Name, PTerm)) ->
                     Name ->
+                    (doc : String) ->
                     (params : List (Name, PTerm)) ->
                     (det : List Name) ->
                     (conName : Maybe Name) ->
@@ -238,19 +240,20 @@ mutual
        PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl
        PNamespace : FC -> List String -> List PDecl -> PDecl
        PTransform : FC -> String -> PTerm -> PTerm -> PDecl
+       PRunElabDecl : FC -> PTerm -> PDecl
        PDirective : FC -> Directive -> PDecl
 
 definedInData : PDataDecl -> List Name
 definedInData (MkPData _ n _ _ cons) = n :: map getName cons
   where
     getName : PTypeDecl -> Name
-    getName (MkPTy _ n _) = n
+    getName (MkPTy _ n _ _) = n
 definedInData (MkPLater _ n _) = [n]
 
 export
 definedIn : List PDecl -> List Name
 definedIn [] = []
-definedIn (PClaim _ _ _ _ (MkPTy _ n _) :: ds) = n :: definedIn ds
+definedIn (PClaim _ _ _ _ (MkPTy _ n _ _) :: ds) = n :: definedIn ds
 definedIn (PData _ _ d :: ds) = definedInData d ++ definedIn ds
 definedIn (PParameters _ _ pds :: ds) = definedIn pds ++ definedIn ds
 definedIn (PUsing _ _ pds :: ds) = definedIn pds ++ definedIn ds
@@ -339,6 +342,7 @@ record Module where
   headerloc : FC
   moduleNS : List String
   imports : List Import
+  documentation : String
   decls : List PDecl
 
 showCount : RigCount -> String
@@ -350,7 +354,7 @@ showCount = elimSemi
 mutual
   showAlt : PClause -> String
   showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";"
-  showAlt (MkWithClause _ lhs wval cs) = " | <<with alts not possible>>;"
+  showAlt (MkWithClause _ lhs wval flags cs) = " | <<with alts not possible>>;"
   showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;"
 
   showDo : PDo -> String
@@ -403,7 +407,7 @@ mutual
       where
         showAlt : PClause -> String
         showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";"
-        showAlt (MkWithClause _ lhs rhs _) = " | <<with alts not possible>>"
+        showAlt (MkWithClause _ lhs rhs flags _) = " | <<with alts not possible>>"
         showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;"
     showPrec _ (PCase _ tm cs)
         = "case " ++ show tm ++ " of { " ++
@@ -411,7 +415,7 @@ mutual
       where
         showCase : PClause -> String
         showCase (MkPatClause _ lhs rhs _) = show lhs ++ " => " ++ show rhs
-        showCase (MkWithClause _ lhs rhs _) = " | <<with alts not possible>>"
+        showCase (MkWithClause _ lhs rhs flags _) = " | <<with alts not possible>>"
         showCase (MkImpossible _ lhs) = show lhs ++ " impossible"
     showPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form...
         = "let { << definitions >>  } in " ++ showPrec d sc
@@ -437,7 +441,8 @@ mutual
         = showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
     showPrec _ (PSearch _ _) = "%search"
     showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")"
-    showPrec d (PQuoteDecl _ tm) = "`( <<declaration>> )"
+    showPrec d (PQuoteName _ n) = "`{{" ++ showPrec d n ++ "}}"
+    showPrec d (PQuoteDecl _ tm) = "`[ <<declaration>> ]"
     showPrec d (PUnquote _ tm) = "~(" ++ showPrec d tm ++ ")"
     showPrec d (PRunElab _ tm) = "%runElab " ++ showPrec d tm
     showPrec d (PPrimVal _ c) = showPrec d c
@@ -503,7 +508,7 @@ record IFaceInfo where
   iconstructor : Name
   params : List Name
   parents : List RawImp
-  methods : List (Name, RigCount, TotalReq, Bool, RawImp)
+  methods : List (Name, RigCount, Maybe TotalReq, Bool, RawImp)
      -- ^ name, whether a data method, and desugared type (without constraint)
   defaults : List (Name, List ImpClause)
 
@@ -687,8 +692,9 @@ mapPTermM f = goPTerm where
     goPTerm (PQuote fc x) =
       PQuote fc <$> goPTerm x
       >>= f
+    goPTerm t@(PQuoteName _ _) = f t
     goPTerm (PQuoteDecl fc x) =
-      PQuoteDecl fc <$> goPDecl x
+      PQuoteDecl fc <$> traverse goPDecl x
       >>= f
     goPTerm (PUnquote fc x) =
       PUnquote fc <$> goPTerm x
@@ -810,9 +816,10 @@ mapPTermM f = goPTerm where
       MkPatClause fc <$> goPTerm lhs
                      <*> goPTerm rhs
                      <*> goPDecls wh
-    goPClause (MkWithClause fc lhs wVal cls) =
+    goPClause (MkWithClause fc lhs wVal flags cls) =
       MkWithClause fc <$> goPTerm lhs
                       <*> goPTerm wVal
+                      <*> pure flags
                       <*> goPClauses cls
     goPClause (MkImpossible fc lhs) = MkImpossible fc <$> goPTerm lhs
 
@@ -829,9 +836,10 @@ mapPTermM f = goPTerm where
       PUsing fc <$> goPairedPTerms mnts
                 <*> goPDecls ps
     goPDecl (PReflect fc t) = PReflect fc <$> goPTerm t
-    goPDecl (PInterface fc v mnts n nts ns mn ps) =
+    goPDecl (PInterface fc v mnts n doc nts ns mn ps) =
       PInterface fc v <$> goPairedPTerms mnts
                       <*> pure n
+                      <*> pure doc
                       <*> goPairedPTerms nts
                       <*> pure ns
                       <*> pure mn
@@ -852,11 +860,12 @@ mapPTermM f = goPTerm where
     goPDecl p@(PFixity _ _ _ _) = pure p
     goPDecl (PNamespace fc strs ps) = PNamespace fc strs <$> goPDecls ps
     goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b
+    goPDecl (PRunElabDecl fc a) = PRunElabDecl fc <$> goPTerm a
     goPDecl p@(PDirective _ _) = pure p
 
 
     goPTypeDecl : PTypeDecl -> Core PTypeDecl
-    goPTypeDecl (MkPTy fc n t) = MkPTy fc n <$> goPTerm t
+    goPTypeDecl (MkPTy fc n d t) = MkPTy fc n d <$> goPTerm t
 
     goPDataDecl : PDataDecl -> Core PDataDecl
     goPDataDecl (MkPData fc n t opts tdecls) =

src/Idris/Version.idr

@@ -4,6 +4,8 @@ module Idris.Version
 import IdrisPaths
 import Data.List
 
+%default total
+
 ||| Semantic versioning with optional tag
 ||| See [semver](https://semver.org/) for proper definition of semantic versioning
 public export