Merge branch 'master' of https://github.com/edwinb/Idris2 into add-version-command

Makefile

@@ -2,7 +2,7 @@
 MAJOR=0
 MINOR=0
 PATCH=0
-
+IDRIS2_VERSION="$MAJOR.$MINOR.$PATCH"
 PREFIX ?= ${HOME}/.idris2
 IDRIS_VERSION := $(shell idris --version)
 VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"
@@ -23,7 +23,7 @@ idris2: src/YafflePaths.idr check_version
 	idris --build idris2.ipkg
 
 src/YafflePaths.idr:
-	echo 'module YafflePaths; 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:

src/Core/Context.idr

@@ -1853,27 +1853,25 @@ logC lvl cmsg
                     coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
             else pure ()
 
-
 export
-logTime : {auto c : Ref Ctxt Defs} ->
-          Lazy String -> Core a -> Core a
-logTime str act
-    = do opts <- getSession
-         if logTimings opts
-            then do clock <- coreLift clockTime
-                    let nano = 1000000000
-                    let t = seconds clock * nano + nanoseconds clock
-                    res <- act
-                    clock <- coreLift clockTime
-                    let t' = seconds clock * nano + nanoseconds clock
-                    let time = t' - t
-                    assert_total $ -- We're not dividing by 0
-                       coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
-                                show (time `div` nano) ++ "." ++ 
-                                addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
-                                "s"
-                    pure res
-            else act
+logTimeWhen : {auto c : Ref Ctxt Defs} ->
+              Bool -> Lazy String -> Core a -> Core a
+logTimeWhen p str act
+    = if p
+         then do clock <- coreLift clockTime
+                 let nano = 1000000000
+                 let t = seconds clock * nano + nanoseconds clock
+                 res <- act
+                 clock <- coreLift clockTime
+                 let t' = seconds clock * nano + nanoseconds clock
+                 let time = t' - t
+                 assert_total $ -- We're not dividing by 0
+                    coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
+                             show (time `div` nano) ++ "." ++ 
+                             addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
+                             "s"
+                 pure res
+         else act
   where
     addZeros : List Char -> String
     addZeros [] = "000"
@@ -1881,3 +1879,10 @@ logTime str act
     addZeros [x,y] = "0" ++ cast x ++ cast y
     addZeros str = pack str
 
+export
+logTime : {auto c : Ref Ctxt Defs} ->
+          Lazy String -> Core a -> Core a
+logTime str act
+    = do opts <- getSession
+         logTimeWhen (logTimings opts) str act
+

src/Core/Metadata.idr

@@ -73,6 +73,20 @@ addLHS loc outerenvlen env tm
     toPat (b :: bs) = b :: toPat bs
     toPat [] = []
 
+-- For giving local variable names types, just substitute the name
+-- rather than storing the whole environment, otherwise we'll repeatedly
+-- store the environment and it'll get big.
+-- We'll need to rethink a bit if we want interactive editing to show
+-- the whole environment - perhaps store each environment just once
+-- along with its source span?
+-- In any case, one could always look at the other names to get their
+-- types directly!
+substEnv : {vars : _} ->
+           FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
+substEnv loc [] tm = tm
+substEnv {vars = x :: _} loc (b :: env) tm 
+    = substEnv loc env (subst (Ref loc Bound x) tm)
+
 export
 addNameType : {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
@@ -81,7 +95,7 @@ addNameType loc n env tm
     = do meta <- get MD
          n' <- getFullName n
          put MD (record { 
-                      names $= ((loc, (n', length env, bindEnv loc env tm)) ::) 
+                      names $= ((loc, (n', 0, substEnv loc env tm)) ::) 
                     } meta)
 
 export

src/Idris/Main.idr

@@ -19,9 +19,9 @@ import Idris.ProcessIdr
 import Idris.REPL
 import Idris.SetOptions
 import Idris.Syntax
-
 import Idris.Socket
 import Idris.Socket.Data
+import Idris.Version
 
 import Data.Vect
 import System
@@ -65,9 +65,9 @@ updatePaths
          addPkgDir "prelude"
          addPkgDir "base"
          addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                        "idris2-" ++ version ++ dirSep ++ "support")
+                        "idris2-" ++ showVersion version ++ dirSep ++ "support")
          addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                        "idris2-" ++ version ++ dirSep ++ "lib")
+                        "idris2-" ++ showVersion version ++ dirSep ++ "lib")
 
 updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
                  Core ()

src/Idris/Package.idr

@@ -16,6 +16,7 @@ import Idris.ProcessIdr
 import Idris.REPLOpts
 import Idris.SetOptions
 import Idris.Syntax
+import Idris.Version
 import Parser.Lexer
 import Parser.Support
 import Utils.Binary
@@ -262,8 +263,8 @@ install pkg
                                (mainmod pkg)
          srcdir <- coreLift currentDir
          -- Make the package installation directory
-         let installPrefix = dir_prefix (dirs (options defs)) ++ 
-                             dirSep ++ "idris2-" ++ version
+         let installPrefix = dir_prefix (dirs (options defs)) ++
+                             dirSep ++ "idris2-" ++ showVersion version
          True <- coreLift $ changeDir installPrefix
              | False => throw (FileErr (name pkg) FileReadError)
          Right _ <- coreLift $ mkdirs [name pkg]

src/Idris/REPL.idr

@@ -295,9 +295,9 @@ processEdit (TypeAt line col name)
                             then throw (UndefinedName (MkFC "(interactive)" (0,0) (0,0)) name)
                             else printResult res
          if res == ""
-            then printResult !(showHole defs [] n num t)
-            else printResult (res ++ "\n\n" ++ "Locally:\n" ++
-                                     !(showHole defs [] n num t))
+            then printResult (nameRoot n ++ " : " ++
+                               !(displayTerm defs t))
+            else pure ()
 processEdit (CaseSplit line col name)
     = do let find = if col > 0
                        then within (line-1, col-1)

src/Idris/SetOptions.idr

@@ -9,6 +9,7 @@ import Core.Unify
 import Idris.CommandLine
 import Idris.REPL
 import Idris.Syntax
+import Idris.Version
 
 import YafflePaths
 
@@ -21,12 +22,12 @@ addPkgDir : {auto c : Ref Ctxt Defs} ->
 addPkgDir p
     = do defs <- get Ctxt
          addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
-                             "idris2-" ++ version ++ dirSep ++ p)
+                             "idris2-" ++ showVersion version ++ dirSep ++ p)
 
 dirOption : Dirs -> DirCommand -> Core ()
 dirOption dirs LibDir
-    = coreLift $ putStrLn 
-         (dir_prefix dirs ++ dirSep ++ "idris2-" ++ version ++ dirSep)
+    = coreLift $ putStrLn
+         (dir_prefix dirs ++ dirSep ++ "idris2-" ++ showVersion version ++ dirSep)
 
 -- Options to be processed before type checking. Return whether to continue.
 export

src/TTImp/Elab/ImplicitBind.idr

@@ -442,8 +442,7 @@ checkBindVar rig elabinfo nest env fc str topexp
                    addNameType fc (UN str) env exp
                    checkExp rig elabinfo env fc tm (gnf env exp) topexp
               Just bty =>
-                do -- TODO: for metadata addNameType loc (UN str) env ty
-                   -- Check rig is consistent with the one in bty, and
+                do -- Check rig is consistent with the one in bty, and
                    -- update if necessary
                    combine (UN str) rig (bindingRig bty)
                    let tm = bindingTerm bty

src/TTImp/Unelab.idr

@@ -132,7 +132,7 @@ mutual
            Just ty <- lookupTyExact n (gamma defs)
                | Nothing => case umode of
                                  ImplicitHoles => pure (Implicit fc True, Erased fc)
-                                 _ => pure (IHole fc (nameRoot n), Erased fc)
+                                 _ => pure (IVar fc n, Erased fc)
            pure (IVar fc !(getFullName n), embed ty)
   unelabTy' umode env (Meta fc n i args)
       = do defs <- get Ctxt

tests/chez/chez008/expected

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

tests/idris2/interactive001/expected

@@ -1,12 +1,5 @@
 1/1: Building LocType (LocType.idr)
 Welcome to Idris 2. Enjoy yourself!
 Main> Main.Vect : Nat -> Type -> Type
-Main>  0 m : Nat
- 0 a : Type
- 0 k : Nat
-   xs : Vect k a
-   x : a
-   ys : Vect m a
--------------------------------------
-xs : Vect k a
+Main> xs : Vect k a
 Main> Bye for now!

tests/idris2/interactive008/expected

@@ -2,15 +2,5 @@
 Welcome to Idris 2. Enjoy yourself!
 Main> \f => \g => \x => g (f x)
 Main> (\x => \zs => x :: zs)
-Main>  0 c : Type
- 0 b : Type
- 0 a : Type
- 0 k : Nat
-   xs : Vect k a
-   x : a
-   ys : Vect k b
-   y : b
-   f : a -> b -> c
--------------------------------------
-f : a -> b -> c
+Main> f : a -> b -> c
 Main> Bye for now!