Merge branch 'master' into add-version-command

Makefile

@@ -23,7 +23,8 @@ idris2: src/YafflePaths.idr check_version
 	idris --build idris2.ipkg
 
 src/YafflePaths.idr:
-	@echo "module YafflePaths; export yprefix : String; yprefix = \"${PREFIX}\"; export yversion : ((Nat,Nat,Nat), String); yversion = ((${MAJOR},${MINOR},${PATCH}), \"\")" > src/YafflePaths.idr
+	echo 'module YafflePaths; export yversion : ((Nat,Nat,Nat), String); yversion = ((${MAJOR},${MINOR},${PATCH}), \"\")" > src/YafflePaths.idr
+	echo 'export yprefix : String; yprefix = "${PREFIX}"' >> src/YafflePaths.idr
 
 prelude:
 	make -C libs/prelude IDRIS2=../../idris2
@@ -56,16 +57,16 @@ install: all install-exec install-libs
 
 install-exec: idris2
 	mkdir -p ${PREFIX}/bin
-	mkdir -p ${PREFIX}/idris2/lib
+	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
-	mkdir -p ${PREFIX}/idris2/support/chez
+	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
-	mkdir -p ${PREFIX}/idris2/support/chicken
+	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chicken
-	mkdir -p ${PREFIX}/idris2/support/racket
+	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket
 	install idris2 ${PREFIX}/bin
-	install support/chez/* ${PREFIX}/idris2/support/chez
+	install support/chez/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
-	install support/chicken/* ${PREFIX}/idris2/support/chicken
+	install support/chicken/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chicken
-	install support/racket/* ${PREFIX}/idris2/support/racket
+	install support/racket/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket
 
 install-libs: libs
 	make -C libs/prelude install IDRIS2=../../idris2
 	make -C libs/base install IDRIS2=../../idris2
-	make -C libs/network install IDRIS2=../../idris2
+	make -C libs/network install IDRIS2=../../idris2 IDRIS2_VERSION=${IDRIS2_VERSION}

idris2.ipkg

@@ -98,6 +98,7 @@ modules =
     TTImp.Elab.Record,
     TTImp.Elab.Rewrite,
     TTImp.Elab.Term,
+    TTImp.Elab.Utils,
     TTImp.Interactive.CaseSplit,
     TTImp.Interactive.ExprSearch,
     TTImp.Interactive.GenerateDef,

libs/network/Echo.idr

@@ -33,12 +33,6 @@ runServer = do
       putStrLn ("Received: " ++ str)
       Right n <- send s ("echo: " ++ str)
         | Left err => putStrLn ("Server failed to send data with error: " ++ show err)
-      -- This might be printed either before or after the client prints
-      -- what it's received, and I think there's enough to check it's
-      -- working without this message so I've removed it. If you disagree,
-      -- please put it back, but also please make sure it's synchronised
-      -- such that the messages are always printed in the same order. - EB
-      -- putStrLn ("Server sent " ++ show n ++ " bytes")
       pure ()
 
 runClient : Port -> IO ()
@@ -51,9 +45,10 @@ runClient serverPort = do
     else do
       Right n <- send sock ("hello world!")
         | Left err => putStrLn ("Client failed to send data with error: " ++ show err)
-      putStrLn ("Client sent " ++ show n ++ " bytes")
       Right (str, _) <- recv sock 1024
         | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
+      -- assuming that stdout buffers get flushed in between system calls, this is "guaranteed"
+      -- to be printed after the server prints its own message
       putStrLn ("Received: " ++ str)
 
 main : IO ()

libs/network/Makefile

@@ -28,7 +28,7 @@ endif
 
 DYLIBTARGET = $(LIBNAME)$(SHLIB_SUFFIX)
 LIBTARGET = $(LIBNAME).a
-TARGET=${HOME}/.idris2
+TARGET=`${IDRIS2} --libdir`
 
 build: $(DYLIBTARGET) $(IDRIS_SRCS)
 	@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
@@ -40,8 +40,8 @@ $(DYLIBTARGET) : $(OBJS)
 install:
 	@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
 	${IDRIS2} --install network.ipkg
-	@if ! [ -d $(TARGET)/idris2/network/lib ]; then mkdir $(TARGET)/idris2/network/lib; fi
+	@if ! [ -d $(TARGET)/network/lib ]; then mkdir $(TARGET)/network/lib; fi
-	install $(DYLIBTARGET) $(HDRS) $(TARGET)/idris2/network/lib
+	install $(DYLIBTARGET) $(HDRS) $(TARGET)/network/lib
 
 clean :
 	rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build

libs/network/expected

@@ -1,3 +1,2 @@
-Client sent 12 bytes
 Received: hello world!
 Received: echo: hello world!

src/Compiler/CompileExpr.idr

@@ -93,6 +93,7 @@ natHack (CApp fc (CRef fc' (NS ["Prelude"] (UN "mult"))) args)
     = CApp fc (CRef fc' (UN "prim__mul_Integer")) args
 natHack (CApp fc (CRef fc' (NS ["Nat", "Data"] (UN "minus"))) args)
     = CApp fc (CRef fc' (UN "prim__sub_Integer")) args
+natHack (CLam fc x exp) = CLam fc x (natHack exp)
 natHack t = t
 
 isNatCon : Name -> Bool
@@ -158,7 +159,7 @@ mutual
   toCExpTm tags n (Bind fc x (Lam _ _ _) sc)
       = pure $ CLam fc x !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Let Rig0 val _) sc)
-      = pure $ CLet fc x (CErased fc) !(toCExp tags n sc)
+      = pure $ shrinkCExp (DropCons SubRefl) !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Let _ val _) sc)
       = pure $ CLet fc x !(toCExp tags n val) !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Pi c e ty) sc)

src/Core/Binary.idr

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

src/Core/CompileExpr.idr

@@ -30,9 +30,9 @@ mutual
        COp : FC -> PrimFn arity -> Vect arity (CExp vars) -> CExp vars
        -- Externally defined primitive operations
        CExtPrim : FC -> (p : Name) -> List (CExp vars) -> CExp vars
-       -- A forced (evaluated) value (TODO: is this right?)
+       -- A forced (evaluated) value
        CForce : FC -> CExp vars -> CExp vars
-       -- A delayed value (lazy? TODO: check)
+       -- A delayed value
        CDelay : FC -> CExp vars -> CExp vars
        -- A case match statement
        CConCase : FC -> (sc : CExp vars) -> List (CConAlt vars) -> Maybe (CExp vars) -> CExp vars
@@ -212,6 +212,51 @@ mutual
   embedConstAlt : CConstAlt args -> CConstAlt (args ++ vars)
   embedConstAlt (MkConstAlt c sc) = MkConstAlt c (embed sc)
 
+mutual
+  -- Shrink the scope of a compiled expression, replacing any variables not
+  -- in the remaining set with Erased
+  export
+  shrinkCExp : SubVars newvars vars -> CExp vars -> CExp newvars
+  shrinkCExp sub (CLocal fc prf) 
+      = case subElem prf sub of
+             Nothing => CErased fc
+             Just (MkVar prf') => CLocal fc prf'
+  shrinkCExp _ (CRef fc x) = CRef fc x
+  shrinkCExp sub (CLam fc x sc) 
+      = let sc' = shrinkCExp (KeepCons sub) sc in
+            CLam fc x sc'
+  shrinkCExp sub (CLet fc x val sc) 
+      = let sc' = shrinkCExp (KeepCons sub) sc in
+            CLet fc x (shrinkCExp sub val) sc'
+  shrinkCExp sub (CApp fc x xs)
+      = CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (CCon fc x tag xs)
+      = CCon fc x tag (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (COp fc x xs)
+      = COp fc x (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (CExtPrim fc p xs)
+      = CExtPrim fc p (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (CForce fc x) = CForce fc (shrinkCExp sub x)
+  shrinkCExp sub (CDelay fc x) = CDelay fc (shrinkCExp sub x)
+  shrinkCExp sub (CConCase fc sc xs def)
+      = CConCase fc (shrinkCExp sub sc) 
+                 (assert_total (map (shrinkConAlt sub) xs))
+                 (assert_total (map (shrinkCExp sub) def))
+  shrinkCExp sub (CConstCase fc sc xs def)
+      = CConstCase fc (shrinkCExp sub sc) 
+                   (assert_total (map (shrinkConstAlt sub) xs))
+                   (assert_total (map (shrinkCExp sub) def))
+  shrinkCExp _ (CPrimVal fc x) = CPrimVal fc x
+  shrinkCExp _ (CErased fc) = CErased fc
+  shrinkCExp _ (CCrash fc x) = CCrash fc x
+
+  shrinkConAlt : SubVars newvars vars -> CConAlt vars -> CConAlt newvars
+  shrinkConAlt sub (MkConAlt x tag args sc)
+        = MkConAlt x tag args (shrinkCExp (subExtend args sub) sc)
+
+  shrinkConstAlt : SubVars newvars vars -> CConstAlt vars -> CConstAlt newvars
+  shrinkConstAlt sub (MkConstAlt x sc) = MkConstAlt x (shrinkCExp sub sc)
+
 mutual
   export
   Weaken CExp where

src/Core/Context.idr

@@ -162,6 +162,7 @@ record GlobalDef where
   location : FC
   fullname : Name -- original unresolved name
   type : ClosedTerm
+  eraseArgs : List Nat -- which argument positions to erase at runtime
   multiplicity : RigCount
   vars : List Name -- environment name is defined in
   visibility : Visibility
@@ -422,7 +423,7 @@ export
 newDef : FC -> Name -> RigCount -> List Name -> 
          ClosedTerm -> Visibility -> Def -> GlobalDef
 newDef fc n rig vars ty vis def 
-    = MkGlobalDef fc n ty rig vars vis unchecked [] empty False False False def
+    = MkGlobalDef fc n ty [] rig vars vis unchecked [] empty False False False def
                   Nothing []
 
 public export
@@ -817,7 +818,7 @@ addBuiltin : {auto x : Ref Ctxt Defs} ->
              Name -> ClosedTerm -> Totality ->
              PrimFn arity -> Core ()
 addBuiltin n ty tot op 
-    = do addDef n (MkGlobalDef emptyFC n ty RigW [] Public tot 
+    = do addDef n (MkGlobalDef emptyFC n ty [] RigW [] Public tot 
                                [Inline] empty False False True (Builtin op)
                                Nothing []) 
          pure ()
@@ -1267,6 +1268,13 @@ addOpenHint hintn_in
          hintn <- toResolvedNames hintn_in
          put Ctxt (record { openHints $= insert hintn () } defs)
 
+export
+dropOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core ()
+dropOpenHint hintn_in
+    = do defs <- get Ctxt
+         hintn <- toResolvedNames hintn_in
+         put Ctxt (record { openHints $= delete hintn } defs)
+
 export
 setOpenHints : {auto c : Ref Ctxt Defs} -> NameMap () -> Core ()
 setOpenHints hs

src/Core/TT.idr

@@ -231,29 +231,23 @@ Show RigCount where
   show Rig1 = "Rig1"
   show RigW = "RigW"
 
+fromInt : Int -> RigCount
+fromInt 0 = Rig0
+fromInt 1 = Rig1
+fromInt _ = RigW
+
+toInt : RigCount -> Int
+toInt Rig0 = 0
+toInt Rig1 = 1
+toInt RigW = 2
+
 export
 rigPlus : RigCount -> RigCount -> RigCount
-rigPlus Rig0 Rig0 = Rig0
+rigPlus a b = fromInt (toInt a + toInt b)
-rigPlus Rig0 Rig1 = Rig1
-rigPlus Rig0 RigW = RigW
-rigPlus Rig1 Rig0 = Rig1
-rigPlus Rig1 Rig1 = RigW
-rigPlus Rig1 RigW = RigW
-rigPlus RigW Rig0 = RigW
-rigPlus RigW Rig1 = RigW
-rigPlus RigW RigW = RigW
 
 export
 rigMult : RigCount -> RigCount -> RigCount
-rigMult Rig0 Rig0 = Rig0
+rigMult a b = fromInt (toInt a * toInt b)
-rigMult Rig0 Rig1 = Rig0
-rigMult Rig0 RigW = Rig0
-rigMult Rig1 Rig0 = Rig0
-rigMult Rig1 Rig1 = Rig1
-rigMult Rig1 RigW = RigW
-rigMult RigW Rig0 = Rig0
-rigMult RigW Rig1 = RigW
-rigMult RigW RigW = RigW
 
 public export
 data Binder : Type -> Type where
@@ -795,6 +789,12 @@ subExtend : (ns : List Name) -> SubVars xs ys -> SubVars (ns ++ xs) (ns ++ ys)
 subExtend [] sub = sub
 subExtend (x :: xs) sub = KeepCons (subExtend xs sub)
 
+export
+subInclude : (ns : List Name) -> SubVars xs ys -> SubVars (xs ++ ns) (ys ++ ns)
+subInclude ns SubRefl = SubRefl
+subInclude ns (DropCons p) = DropCons (subInclude ns p)
+subInclude ns (KeepCons p) = KeepCons (subInclude ns p)
+
 mutual
   export
   shrinkBinder : Binder (Term vars) -> SubVars newvars vars -> 

src/Core/TTC.idr

@@ -846,6 +846,7 @@ TTC GlobalDef where
            when (isUserName (fullname gdef)) $
               do toBuf b (location gdef)
                  toBuf b (type gdef)
+                 toBuf b (eraseArgs gdef)
                  toBuf b (multiplicity gdef)
                  toBuf b (vars gdef)
                  toBuf b (visibility gdef)
@@ -863,17 +864,17 @@ TTC GlobalDef where
            let refs = map fromList refsList
            if isUserName name
               then do loc <- fromBuf b; 
-                      ty <- fromBuf b; mul <- fromBuf b
+                      ty <- fromBuf b; eargs <- fromBuf b; 
-                      vars <- fromBuf b
+                      mul <- fromBuf b; vars <- fromBuf b
                       vis <- fromBuf b; tot <- fromBuf b
                       fl <- fromBuf b
                       inv <- fromBuf b
                       c <- fromBuf b
                       sc <- fromBuf b
-                      pure (MkGlobalDef loc name ty mul vars vis 
+                      pure (MkGlobalDef loc name ty eargs mul vars vis 
                                         tot fl refs inv c True def cdef sc)
               else do let fc = emptyFC
-                      pure (MkGlobalDef fc name (Erased fc)
+                      pure (MkGlobalDef fc name (Erased fc) []
                                         RigW [] Public unchecked [] refs
                                         False False True def cdef [])
 

src/Idris/CommandLine.idr

@@ -1,5 +1,6 @@
 module Idris.CommandLine
 
+import YafflePaths
 import Data.String
 import Idris.Version
 import YafflePaths
@@ -13,7 +14,6 @@ data PkgCommand
       | Clean
       | REPL
 
-
 export
 Show PkgCommand where
   show Build = "--build"
@@ -21,6 +21,14 @@ Show PkgCommand where
   show Clean = "--clean"
   show REPL = "--repl"
 
+public export
+data DirCommand
+      = LibDir -- show top level package directory
+
+export
+Show DirCommand where
+  show LibDir = "--libdir"
+
 ||| CLOpt - possible command line options
 public export
 data CLOpt
@@ -47,6 +55,8 @@ data CLOpt
   PkgPath String |
    ||| Build or install a given package, depending on PkgCommand
   Package PkgCommand String |
+   ||| Show locations of data/library directories
+  Directory DirCommand |
    ||| The input Idris file
   InputFile String |
    ||| Whether or not to run in IdeMode (easily parsable for other tools)
@@ -104,6 +114,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
            MkOpt ["--clean"] ["package file"] (\f => [Package Clean f])
               (Just "Clean intermediate files/executables for the given package"),
 
+           MkOpt ["--libdir"] [] [Directory LibDir]
+              (Just "Show library directory"),
            MkOpt ["--quiet", "-q"] [] [Quiet]
               (Just "Quiet mode; display fewer messages"),
            MkOpt ["--version", "-v"] [] [Version]

src/Idris/Elab/Implementation.idr

@@ -37,22 +37,37 @@ bindConstraints fc p [] ty = ty
 bindConstraints fc p ((n, ty) :: rest) sc
     = IPi fc RigW p n ty (bindConstraints fc p rest sc)
 
-addDefaults : FC -> List Name -> List (Name, List ImpClause) ->
+addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) ->
               List ImpDecl -> 
               (List ImpDecl, List Name) -- Updated body, list of missing methods
-addDefaults fc ms defs body
+addDefaults fc impName allms defs body
-    = let missing = dropGot ms body in
+    = let missing = dropGot allms body in
           extendBody [] missing body
   where
+    -- Given the list of missing names, if any are among the default definitions,
+    -- add them to the body
     extendBody : List Name -> List Name -> List ImpDecl -> 
                  (List ImpDecl, List Name)
     extendBody ms [] body = (body, ms)
     extendBody ms (n :: ns) body
         = case lookup n defs of
                Nothing => extendBody (n :: ms) ns body
-               Just cs => extendBody ms ns 
+               Just cs => 
-                              (IDef fc n (map (substLocClause fc) cs) :: body)
+                    -- If any method names appear in the clauses, they should
+                    -- be applied to the constraint name __con because they
+                    -- are going to be referring to the present implementation.
+                    -- That is, default method implementations could depend on
+                    -- other methods.
+                    -- (See test idris2/interface014 for an example!)
+                    let mupdates 
+                            = map (\n => (n, IImplicitApp fc (IVar fc n)
+                                                          (Just (UN "__con"))
+                                                          (IVar fc impName))) allms
+                        cs' = map (substNamesClause [] mupdates) cs in
+                        extendBody ms ns 
+                             (IDef fc n (map (substLocClause fc) cs') :: body)
 
+    -- Find which names are missing from the body
     dropGot : List Name -> List ImpDecl -> List Name
     dropGot ms [] = ms
     dropGot ms (IDef _ n _ :: ds)
@@ -139,13 +154,12 @@ elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody
 
                -- 1.5. Lookup default definitions and add them to to body
                let (body, missing)
-                     = addDefaults fc (map (dropNS . fst) (methods cdata)) 
+                     = addDefaults fc impName (map (dropNS . fst) (methods cdata)) 
                                       (defaults cdata) body_in
 
                log 5 $ "Added defaults: body is " ++ show body
                log 5 $ "Missing methods: " ++ show missing
 
-
                -- 2. Elaborate top level function types for this interface
                defs <- get Ctxt
                fns <- topMethTypes [] impName methImps impsp (params cdata)

src/Idris/Main.idr

@@ -65,9 +65,9 @@ updatePaths
          addPkgDir "prelude"
          addPkgDir "base"
          addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                        "idris2" ++ dirSep ++ "support")
+                        "idris2-" ++ version ++ dirSep ++ "support")
          addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                        "idris2" ++ dirSep ++ "lib")
+                        "idris2-" ++ version ++ dirSep ++ "lib")
 
 updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
                  Core ()
@@ -122,7 +122,8 @@ stMain opts
            done <- processPackageOpts opts
 
            when (not done) $
-              do preOptions opts
+              do True <- preOptions opts
+                     | False => pure ()
 
                  u <- newRef UST initUState
                  updateREPLOpts

src/Idris/ModTree.idr

@@ -85,14 +85,17 @@ mkModTree loc done mod
                          Nothing =>
                            do (file, modInfo) <- readHeader loc mod
                               let imps = map path (imports modInfo)
-                              ms <- traverse (mkModTree loc done) imps
+                              ms <- traverse (mkModTree loc (mod :: done)) imps
                               let mt = MkModTree mod (Just file) ms
                               all <- get AllMods
                               put AllMods ((mod, mt) :: all)
                               pure mt
                          Just m => pure m)
                 -- Couldn't find source, assume it's in a package directory
-                (\err => pure (MkModTree mod Nothing []))
+                (\err => 
+                    case err of
+                         CyclicImports _ => throw err
+                         _ => pure (MkModTree mod Nothing []))
 
 -- Given a module tree, returns the modules in the reverse order they need to
 -- be built, including their dependencies
@@ -112,7 +115,6 @@ mkBuildMods acc mod
 
 -- Given a main file name, return the list of modules that need to be
 -- built for that main file, in the order they need to be built
-export
 getBuildMods : {auto c : Ref Ctxt Defs} ->
                {auto o : Ref ROpts REPLOpts} ->
                FC -> (mainFile : String) -> 

src/Idris/Package.idr

@@ -22,6 +22,7 @@ import Utils.Binary
 
 import System
 import Text.Parser
+import YafflePaths
 
 %default covering
 
@@ -206,6 +207,7 @@ processOptions (Just (fc, opts))
     = do let Right clopts = getOpts (words opts)
                 | Left err => throw (GenericMsg fc err)
          preOptions clopts
+         pure ()
 
 build : {auto c : Ref Ctxt Defs} ->
         {auto s : Ref Syn SyntaxInfo} ->
@@ -260,7 +262,8 @@ install pkg
                                (mainmod pkg)
          srcdir <- coreLift currentDir
          -- Make the package installation directory
-         let installPrefix = dir_prefix (dirs (options defs)) ++ dirSep ++ "idris2"
+         let installPrefix = dir_prefix (dirs (options defs)) ++ 
+                             dirSep ++ "idris2-" ++ version
          True <- coreLift $ changeDir installPrefix
              | False => throw (FileErr (name pkg) FileReadError)
          Right _ <- coreLift $ mkdirs [name pkg]

src/Idris/REPL.idr

@@ -53,6 +53,7 @@ showInfo (n, idx, d)
     = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++
                               show !(toFullNames (definition d)))
          coreLift $ putStrLn (show (multiplicity d))
+         coreLift $ putStrLn ("Erasable args: " ++ show (eraseArgs d))
          case compexpr d of
               Nothing => pure ()
               Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr)

src/Idris/SetOptions.idr

@@ -10,6 +10,8 @@ import Idris.CommandLine
 import Idris.REPL
 import Idris.Syntax
 
+import YafflePaths
+
 import System
 
 -- TODO: Version numbers on dependencies
@@ -19,14 +21,19 @@ addPkgDir : {auto c : Ref Ctxt Defs} ->
 addPkgDir p
     = do defs <- get Ctxt
          addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                             "idris2" ++ dirSep ++ p)
+                             "idris2-" ++ version ++ dirSep ++ p)
 
--- Options to be processed before type checking
+dirOption : Dirs -> DirCommand -> Core ()
+dirOption dirs LibDir
+    = coreLift $ putStrLn 
+         (dir_prefix dirs ++ dirSep ++ "idris2-" ++ version ++ dirSep)
+
+-- Options to be processed before type checking. Return whether to continue.
 export
 preOptions : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
-             List CLOpt -> Core ()
+             List CLOpt -> Core Bool
-preOptions [] = pure ()
+preOptions [] = pure True
 preOptions (Quiet :: opts)
     = do setOutput (REPL True)
          preOptions opts
@@ -45,8 +52,13 @@ preOptions (SetCG e :: opts)
 preOptions (PkgPath p :: opts)
     = do addPkgDir p
          preOptions opts
+preOptions (Directory d :: opts)
+    = do defs <- get Ctxt
+         dirOption (dirs (options defs)) d
+         pure False
 preOptions (Timing :: opts)
-    = setLogTimings True
+    = do setLogTimings True
+         preOptions opts
 preOptions (_ :: opts) = preOptions opts
 
 -- Options to be processed after type checking. Returns whether execution

src/TTImp/Elab/Ambiguity.idr

@@ -119,6 +119,11 @@ stripDelay defs tm = tm
 
 data TypeMatch = Concrete | Poly | NoMatch
 
+Show TypeMatch where
+  show Concrete = "Concrete"
+  show Poly = "Poly"
+  show NoMatch = "NoMatch"
+
 mutual
   mightMatchD : Defs -> NF vars -> NF [] -> Core TypeMatch
   mightMatchD defs l r 
@@ -200,8 +205,9 @@ couldBe {vars} defs ty@(NType _) app
 couldBe defs ty app = pure $ Just (False, app)
 
 
-notOverloadable : Defs -> RawImp -> Core Bool
+notOverloadable : Defs -> (Bool, RawImp) -> Core Bool
-notOverloadable defs fn = notOverloadableFn (getFn fn)
+notOverloadable defs (True, fn) = pure True
+notOverloadable defs (concrete, fn) = notOverloadableFn (getFn fn)
   where
     notOverloadableFn : RawImp -> Core Bool
     notOverloadableFn (IVar _ n)
@@ -227,9 +233,10 @@ pruneByType target alts
          matches_in <- traverse (couldBe defs target) alts
          let matches = mapMaybe id matches_in
          res <- if or (map Delay (map fst matches))
-                -- if there's any concrete matches, drop the ones marked
+                -- if there's any concrete matches, drop the non-concrete
-                -- as '%allow_overloads' from the possible set
+                -- matches marked as '%allow_overloads' from the possible set
-                   then filterCore (notOverloadable defs) (map snd matches)
+                   then do keep <- filterCore (notOverloadable defs) matches
+                           pure (map snd keep)
                    else pure (map snd matches)
          if isNil res
             then pure alts -- if none of them work, better to show all the errors

src/TTImp/Elab/App.idr

@@ -48,7 +48,6 @@ getNameType rigc env fc x
                                DCon t a => DataCon t a
                                TCon t a _ _ _ _ => TyCon t a
                                _ => Func
-                 addNameType fc x env (embed (type def))
                  pure (Ref fc nt (Resolved i), gnf env (embed (type def)))
   where
     isLet : Binder t -> Bool

src/TTImp/Elab/Utils.idr

@@ -0,0 +1,40 @@
+module TTImp.Elab.Utils
+
+import Core.Context
+import Core.Core
+import Core.Env
+import Core.Normalise
+import Core.TT
+import Core.Value
+
+import TTImp.TTImp
+
+findErasedFrom : Defs -> Nat -> NF [] -> Core (List Nat)
+findErasedFrom defs pos (NBind fc x (Pi c _ _) scf)
+    = do sc <- scf defs (toClosure defaultOpts [] (Erased fc))
+         rest <- findErasedFrom defs (1 + pos) sc
+         case c of
+              Rig0 => pure (pos :: rest)
+              _ => pure rest
+findErasedFrom defs pos tm = pure []
+
+-- Find the argument positions in the given type which are guaranteed to be
+-- erasable
+export
+findErased : {auto c : Ref Ctxt Defs} ->
+             ClosedTerm -> Core (List Nat)
+findErased tm 
+    = do defs <- get Ctxt
+         tmnf <- nf defs [] tm
+         findErasedFrom defs 0 tmnf
+
+export
+updateErasable : {auto c : Ref Ctxt Defs} ->
+                 Name -> Core ()
+updateErasable n
+    = do defs <- get Ctxt
+         Just gdef <- lookupCtxtExact n (gamma defs)
+              | Nothing => pure ()
+         es <- findErased (type gdef)
+         addDef n (record { eraseArgs = es } gdef)
+         pure ()

src/TTImp/Interactive/ExprSearch.idr

@@ -124,11 +124,12 @@ searchName fc rigc opts env target topty defining (n, ndef)
          ures <- unify InSearch fc env target appTy
          let [] = constraints ures
              | _ => pure []
-         -- Search the explicit arguments first
+         -- Search the explicit arguments first, they may resolve other holes
-         args' <- traverse (searchIfHole fc opts defining topty env)
+         traverse (searchIfHole fc opts defining topty env)
-                           (filter explicit args)
+                  (filter explicit args)
          args' <- traverse (searchIfHole fc opts defining topty env)
                            args
+
          let cs = mkCandidates fc (Ref fc namety n) args'
          logC 10 (do strs <- traverse (\t => pure (show !(toFullNames t) ++ "\n")) cs
                      pure ("Candidates: " ++ concat strs))

src/TTImp/ProcessData.idr

@@ -11,6 +11,7 @@ import Core.Value
 
 import TTImp.BindImplicits
 import TTImp.Elab.Check
+import TTImp.Elab.Utils
 import TTImp.Elab
 import TTImp.TTImp
 
@@ -201,8 +202,9 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
          addToSave n
          log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
 
+         let connames = map conName cons
          when (not (NoHints `elem` opts)) $
-              traverse_ (\x => addHintFor fc (Resolved tidx) x True False) (map conName cons)
+              traverse_ (\x => addHintFor fc (Resolved tidx) x True False) connames
 
-         pure ()
+         traverse_ updateErasable (Resolved tidx :: connames)
 

src/TTImp/ProcessDef.idr

@@ -626,8 +626,10 @@ processDef opts nest env fc n_in cs_in
          when (not (elem InCase opts)) $
            compileRunTime
 
+         md <- get MD -- don't need the metadata collected on the coverage check
          cov <- checkCoverage nidx mult cs tree_ct
          setCovering fc n cov
+         put MD md
 
   where
     simplePat : Term vars -> Bool

src/TTImp/ProcessType.idr

@@ -12,6 +12,7 @@ import Core.Value
 
 import TTImp.BindImplicits
 import TTImp.Elab.Check
+import TTImp.Elab.Utils
 import TTImp.Elab
 import TTImp.TTImp
 
@@ -101,7 +102,12 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          -- TODO: Check name visibility
 
          def <- initDef n env ty opts
-         addDef (Resolved idx) (newDef fc n rig vars (abstractEnvType tfc env ty) vis def)
+         let fullty = abstractEnvType tfc env ty
+         erased <- findErased fullty
+
+         addDef (Resolved idx) 
+                (record { eraseArgs = erased }
+                        (newDef fc n rig vars fullty vis def))
          -- Flag it as checked, because we're going to check the clauses 
          -- from the top level.
          -- But, if it's a case block, it'll be checked as part of the top

src/TTImp/TTImp.idr

@@ -815,7 +815,7 @@ mutual
   export
   TTC ImpDecl where
     toBuf b (IClaim fc c vis xs d) 
-        = do tag 0; toBuf b c; toBuf b fc; toBuf b vis; toBuf b xs; toBuf b d
+        = do tag 0; toBuf b fc; toBuf b c; toBuf b vis; toBuf b xs; toBuf b d
     toBuf b (IData fc vis d) 
         = do tag 1; toBuf b fc; toBuf b vis; toBuf b d
     toBuf b (IDef fc n xs) 

src/TTImp/Utils.idr

@@ -111,6 +111,7 @@ mutual
       = IForce fc (substNames bound ps t)
   substNames bound ps tm = tm
 
+  export
   substNamesClause : List Name -> List (Name, RawImp) -> 
                      ImpClause -> ImpClause 
   substNamesClause bound ps (PatClause fc lhs rhs)

src/Utils/Binary.idr

@@ -111,9 +111,12 @@ initBinaryS s
              | Nothing => throw (InternalError "Buffer creation failed")
          newRef Bin (newBinary buf)
 
-extendBinary : Binary -> Core Binary
+extendBinary : Int -> Binary -> Core Binary
-extendBinary (MkBin buf l s u)
+extendBinary need (MkBin buf l s u)
-    = do let s' = s * 2
+    = do let newsize = s * 2
+         let s' = if newsize < need 
+                     then newsize + need
+                     else newsize
          Just buf' <- coreLift $ resizeBuffer buf s'
              | Nothing => throw (InternalError "Buffer expansion failed")
          pure (MkBin buf' l s' u)
@@ -133,7 +136,7 @@ TTC Bits8 where
             then
               do coreLift $ setByte (buf chunk) (loc chunk) val
                  put Bin (appended 1 chunk)
-            else do chunk' <- extendBinary chunk
+            else do chunk' <- extendBinary 1 chunk
                     coreLift $ setByte (buf chunk') (loc chunk') val
                     put Bin (appended 1 chunk')
 
@@ -164,7 +167,7 @@ TTC Int where
             then 
               do coreLift $ setInt (buf chunk) (loc chunk) val
                  put Bin (appended 4 chunk)
-            else do chunk' <- extendBinary chunk
+            else do chunk' <- extendBinary 4 chunk
                     coreLift $ setInt (buf chunk') (loc chunk') val
                     put Bin (appended 4 chunk')
 
@@ -187,7 +190,7 @@ TTC String where
               then
                 do coreLift $ setString (buf chunk) (loc chunk) val
                    put Bin (appended req chunk)
-              else do chunk' <- extendBinary chunk
+              else do chunk' <- extendBinary req chunk
                       coreLift $ setString (buf chunk') (loc chunk') val
                       put Bin (appended req chunk')
 
@@ -199,7 +202,8 @@ TTC String where
                 do val <- coreLift $ getString (buf chunk) (loc chunk) len
                    put Bin (incLoc len chunk)
                    pure val
-              else throw (TTCError (EndOfBuffer "String"))
+              else throw (TTCError (EndOfBuffer ("String length " ++ show len ++ 
+                                                 " at " ++ show (loc chunk))))
 
 export
 TTC Binary where
@@ -212,7 +216,7 @@ TTC Binary where
               do coreLift $ copyData (buf val) 0 len
                                      (buf chunk) (loc chunk)
                  put Bin (appended len chunk)
-            else do chunk' <- extendBinary chunk
+            else do chunk' <- extendBinary len chunk
                     coreLift $ copyData (buf val) 0 len
                                         (buf chunk') (loc chunk')
                     put Bin (appended len chunk')
@@ -255,7 +259,7 @@ TTC Double where
             then 
               do coreLift $ setDouble (buf chunk) (loc chunk) val
                  put Bin (appended 8 chunk)
-            else do chunk' <- extendBinary chunk
+            else do chunk' <- extendBinary 8 chunk
                     coreLift $ setDouble (buf chunk') (loc chunk') val
                     put Bin (appended 8 chunk')
 

tests/Main.idr

@@ -32,14 +32,14 @@ idrisTests
        "coverage001", "coverage002", "coverage003", "coverage004",
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",
-       "import001", "import002", "import003",
+       "import001", "import002", "import003", "import004",
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",
        "interface009", "interface010", "interface011", "interface012",
-       "interface013",
+       "interface013", "interface014",
        "lazy001",
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007",
@@ -61,8 +61,8 @@ typeddTests
 
 chezTests : List String
 chezTests
-   = ["chez001", "chez002", "chez003", "chez004",
+   = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006", 
-      "chez005", "chez006", "chez007"]
+      "chez007", "chez008"]
 
 ideModeTests : List String
 ideModeTests

tests/chez/chez008/Nat.idr

@@ -0,0 +1,11 @@
+myS : Nat -> Nat
+myS n = S n
+
+myS_crash : Nat -> Nat
+myS_crash = S
+
+main : IO ()
+main = do
+  printLn (S Z)
+  printLn (myS Z)
+  printLn (myS_crash Z)

tests/chez/chez008/expected

@@ -0,0 +1,6 @@
+1
+1
+1
+1/1: Building Nat (Nat.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> Main> Bye for now!

tests/chez/chez008/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez008/run

@@ -0,0 +1,3 @@
+$1 Nat.idr < input
+
+rm -rf build

tests/idris2/error004/expected

@@ -2,7 +2,7 @@
 Error1.idr:8:9--9:1:While processing right hand side of Main.wrong at Error1.idr:8:1--9:1:
 Can't find an implementation for Show (Vect (S (S (S (S Z)))) Integer)
 1/1: Building Error2 (Error2.idr)
-Error2.idr:11:1--15:1:While processing right hand side of Main.showPrec at Error2.idr:11:1--15:1:
+Error2.idr:13:38--15:1:While processing right hand side of Main.show at Error2.idr:13:3--15:1:
 Multiple solutions found in search. Possible correct results:
 	Show implementation at Error2.idr:11:1--15:1
 	Show implementation at Error2.idr:7:1--11:1

tests/idris2/import004/Cycle1.idr

@@ -0,0 +1,3 @@
+module Cycle1
+
+import Cycle2

tests/idris2/import004/Cycle2.idr

@@ -0,0 +1,3 @@
+module Cycle2
+
+import Cycle1

tests/idris2/import004/Loop.idr

@@ -0,0 +1,3 @@
+module Loop
+
+import Loop

tests/idris2/import004/expected

@@ -0,0 +1,2 @@
+Uncaught error: Module imports form a cycle: Cycle2 -> Cycle1 -> Cycle1
+Uncaught error: Module imports form a cycle: Loop -> Loop

tests/idris2/import004/run

@@ -0,0 +1,4 @@
+$1 Cycle1.idr
+$1 Loop.idr
+
+rm -rf build

tests/idris2/interface014/DepInt.idr

@@ -0,0 +1,13 @@
+import Control.Monad.Identity
+
+public export
+interface Foo (sA : Type) where
+  A : Type
+  Elem : A -> sA -> Type
+  Empty : sA -> Type
+  Empty as = (a : A) -> Not (Elem a as)
+
+public export
+implementation Foo (Identity Bool) where
+  A = Bool
+  Elem x (Id y) = x = y

tests/idris2/interface014/expected

@@ -0,0 +1 @@
+1/1: Building DepInt (DepInt.idr)

tests/idris2/interface014/run

@@ -0,0 +1,3 @@
+$1 DepInt.idr --check
+
+rm -rf build