Merge branch 'master' of github.com:edwinb/Idris2

INSTALL.md

@@ -9,7 +9,7 @@ version 1.3.2 (see https://www.idris-lang.org/download)
 There are several sets of instructions on how to install Idris from source and
 binary.
 
-+ [Official ipkg installer for macOS](http://www.idris-lang.org/pkgs/idris-current.pkg)
++ [Official ipkg installer for macOS](https://www.idris-lang.org/pkgs/idris-current.pkg)
 + [Source build instructions from the Idris GitHub Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions)
 + [Binary installation using Cabal from the Idris Manual](https://idris.readthedocs.io/en/latest/tutorial/starting.html)
 

Notes/IDE-mode.md

@@ -3,7 +3,7 @@ IDE protocol, version 2
 
 The IDE protocol is (or rather, will be) compatible with the IDE protocol for
 Idris 1, as described here:
-http://docs.idris-lang.org/en/latest/reference/ide-protocol.html
+https://idris.readthedocs.io/en/latest/reference/ide-protocol.html
 
 On start up, it reports:
 

README.md

@@ -98,4 +98,4 @@ Things still missing
 Talks
 =====
 
-[![Idris 2 - Type-driven Development of Idris (Curry On - London 2019)](http://img.youtube.com/vi/DRq2NgeFcO0/0.jpg)](http://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)")
+[![Idris 2 - Type-driven Development of Idris (Curry On - London 2019)](https://img.youtube.com/vi/DRq2NgeFcO0/0.jpg)](https://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)")

docs/LICENSE

@@ -7,4 +7,4 @@ rights to Documentation for Idris.
 
 More information concerning the CC0 can be found online at:
 
-    http://creativecommons.org/publicdomain/zero/1.0/
+    https://creativecommons.org/publicdomain/zero/1.0/

docs/Makefile

@@ -9,7 +9,7 @@ BUILDDIR      = _build
 
 # User-friendly check for sphinx-build
 ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
-$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from http://sphinx-doc.org/)
+$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from https://www.sphinx-doc.org/)
 endif
 
 # Internal variables.

docs/README.md

@@ -1,7 +1,7 @@
 # Documentation for the Idris Language.
 
 
-This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](http://sphinx-doc.org) for future inclusion on [Read The Docs](http://www.readthedocs.org).
+This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](https://www.sphinx-doc.org) for future inclusion on [Read The Docs](https://readthedocs.org).
 
 ## Dependencies
 
@@ -12,7 +12,7 @@ To build the manual the following dependencies must be met. We assume that you h
 Python should be installed by default on most systems.
 Sphinx can be installed either through your hosts package manager or using pip/easy_install.
 
-*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx
+*Note* [ReadTheDocs](https://readthedocs.org) works with Sphinx
  `v1.2.2`. If you install a more recent version of sphinx then
  'incorrectly' marked up documentation may get passed the build system
  of readthedocs and be ignored. In the past we had several code-blocks
@@ -45,7 +45,7 @@ rights to Documentation for Idris.
 
 More information concerning the CC0 can be found online at:
 
-    http://creativecommons.org/publicdomain/zero/1.0/
+    https://creativecommons.org/publicdomain/zero/1.0/
 
 
 When contributing material to the manual please bear in mind that the work will be licensed as above.

docs/index.rst

@@ -13,7 +13,7 @@ Documentation for the Idris 2 Language
    Idris Community* has waived all copyright and related or neighboring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 This is a placeholder, to get set up with readthedocs.
 

docs/make.bat

@@ -65,7 +65,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/reference/index.rst

@@ -9,7 +9,7 @@ Idris2 Reference Guide
    Idris Community* has waived all copyright and related or neighboring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 This is a placeholder, to get set up with readthedocs.
 

src/Compiler/Inline.idr

@@ -6,6 +6,7 @@ import Core.FC
 import Core.TT
 
 import Data.Vect
+import Data.LengthMatch
 
 %default covering
 
@@ -21,18 +22,6 @@ weakenNsEnv : (xs : List Name) -> EEnv free vars -> EEnv (xs ++ free) vars
 weakenNsEnv [] env = env
 weakenNsEnv (x :: xs) env = weakenEnv (weakenNsEnv xs env)
 
--- TODO: This is in CaseBuilder too, so tidy it up...
-data LengthMatch : List a -> List b -> Type where
-     NilMatch : LengthMatch [] []
-     ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
-
-checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
-checkLengthMatch [] [] = Just NilMatch
-checkLengthMatch [] (x :: xs) = Nothing
-checkLengthMatch (x :: xs) [] = Nothing
-checkLengthMatch (x :: xs) (y :: ys)
-    = Just (ConsMatch !(checkLengthMatch xs ys))
-
 extend : EEnv free vars -> (args : List (CExp free)) -> (args' : List Name) ->
          LengthMatch args args' -> EEnv free (args' ++ vars)
 extend env [] [] NilMatch = env
@@ -128,11 +117,7 @@ mutual
   eval rec env stk (CCon fc n t args)
       = pure $ unload stk $ CCon fc n t !(traverse (eval rec env []) args)
   eval rec env stk (COp fc p args)
-      = pure $ unload stk $ COp fc p !(mapV (eval rec env []) args)
+      = pure $ unload stk $ COp fc p !(traverseVect (eval rec env []) args)
-    where
-      mapV : (a -> Core b) -> Vect n a -> Core (Vect n b)
-      mapV f [] = pure []
-      mapV f (x :: xs) = pure $ !(f x) :: !(mapV f xs)
   eval rec env stk (CExtPrim fc p args)
       = pure $ unload stk $ CExtPrim fc p !(traverse (eval rec env []) args)
   eval rec env stk (CForce fc e)
@@ -143,28 +128,18 @@ mutual
       = pure $ unload stk (CDelay fc !(eval rec env [] e))
   eval rec env stk (CConCase fc sc alts def)
       = do sc' <- eval rec env [] sc
-           case !(pickAlt rec env stk sc' alts def) of
+           Nothing <- pickAlt rec env stk sc' alts def | Just val => pure val
-                Nothing =>
+           def' <- traverseOpt (eval rec env stk) def
-                   do def' <- case def of
+           pure $ CConCase fc sc'
-                                   Nothing => pure Nothing
-                                   Just d => pure (Just !(eval rec env stk d))
-                      pure $
-                         CConCase fc sc'
                      !(traverse (evalAlt fc rec env stk) alts)
                      def'
-                Just val => pure val
   eval rec env stk (CConstCase fc sc alts def)
       = do sc' <- eval rec env [] sc
-           case !(pickConstAlt rec env stk sc' alts def) of
+           Nothing <- pickConstAlt rec env stk sc' alts def | Just val => pure val
-                Nothing =>
+           def' <- traverseOpt (eval rec env stk) def
-                   do def' <- case def of
+           pure $ CConstCase fc sc'
-                                   Nothing => pure Nothing
-                                   Just d => pure (Just !(eval rec env stk d))
-                      pure $
-                         CConstCase fc sc'
                          !(traverse (evalConstAlt rec env stk) alts)
                          def'
-                Just val => pure val
   eval rec env stk (CPrimVal fc c) = pure $ unload stk $ CPrimVal fc c
   eval rec env stk (CErased fc) = pure $ unload stk $ CErased fc
   eval rec env stk (CCrash fc str) = pure $ unload stk $ CCrash fc str
@@ -182,7 +157,7 @@ mutual
                  List Name -> EEnv free vars -> Stack free -> CConstAlt (vars ++ free) ->
                  Core (CConstAlt free)
   evalConstAlt rec env stk (MkConstAlt c sc)
-      = pure $ MkConstAlt c !(eval rec env stk sc)
+      = MkConstAlt c <$> eval rec env stk sc
 
   pickAlt : {auto c : Ref Ctxt Defs} ->
             List Name -> EEnv free vars -> Stack free ->
@@ -190,9 +165,7 @@ mutual
             Maybe (CExp (vars ++ free)) ->
             Core (Maybe (CExp free))
   pickAlt rec env stk (CCon fc n t args) [] def
-      = case def of
+      = traverseOpt (eval rec env stk) def
-             Nothing => pure Nothing
-             Just d => pure $ Just !(eval rec env stk d)
   pickAlt {vars} {free} rec env stk (CCon fc n t args) (MkConAlt n' t' args' sc :: alts) def
       = if t == t'
            then case checkLengthMatch args args' of
@@ -212,18 +185,16 @@ mutual
                  Maybe (CExp (vars ++ free)) ->
                  Core (Maybe (CExp free))
   pickConstAlt rec env stk (CPrimVal fc c) [] def
-      = case def of
+      = traverseOpt (eval rec env stk) def
-             Nothing => pure Nothing
-             Just d => pure $ Just !(eval rec env stk d)
   pickConstAlt {vars} {free} rec env stk (CPrimVal fc c) (MkConstAlt c' sc :: alts) def
       = if c == c'
-           then pure $ Just !(eval rec env stk sc)
+           then Just <$> eval rec env stk sc
            else pickConstAlt rec env stk (CPrimVal fc c) alts def
   pickConstAlt rec env stk _ _ _ = pure Nothing
 
 inline : {auto c : Ref Ctxt Defs} ->
          CDef -> Core CDef
-inline (MkFun args exp) = pure $ MkFun args !(eval [] [] [] exp)
+inline (MkFun args exp) = MkFun args <$> eval [] [] [] exp
 inline d = pure d
 
 export
@@ -231,14 +202,7 @@ inlineDef : {auto c : Ref Ctxt Defs} ->
             Name -> Core ()
 inlineDef n
     = do defs <- get Ctxt
-         case !(lookupCtxtExact n (gamma defs)) of
+         Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
-              Nothing => pure ()
+         let Just cexpr =  compexpr def             | Nothing => pure ()
-              Just def =>
+         setCompiled n !(inline cexpr)
-                   case compexpr def of
-                        Nothing => pure ()
-                        Just cexpr =>
-                             do -- coreLift $ putStrLn $ show (fullname def) ++ " before: " ++ show cexpr
-                                inlined <- inline cexpr
-                                -- coreLift $ putStrLn $ show (fullname def) ++ " after: " ++ show inlined
-                                setCompiled n inlined
 

src/Core/CaseBuilder.idr

@@ -8,6 +8,8 @@ import Core.Normalise
 import Core.TT
 import Core.Value
 
+import Data.LengthMatch
+
 %default covering
 
 public export
@@ -187,17 +189,6 @@ substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs
     = do pats' <- substInPats fc a (mkTerm vars pat) pats
          pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') rhs)
 
-data LengthMatch : List a -> List b -> Type where
-     NilMatch : LengthMatch [] []
-     ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
-
-checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
-checkLengthMatch [] [] = Just NilMatch
-checkLengthMatch [] (x :: xs) = Nothing
-checkLengthMatch (x :: xs) [] = Nothing
-checkLengthMatch (x :: xs) (y :: ys)
-    = Just (ConsMatch !(checkLengthMatch xs ys))
-
 data Partitions : List (PatClause vars todo) -> Type where
      ConClauses : (cs : List (PatClause vars todo)) ->
                   Partitions ps -> Partitions (cs ++ ps)

src/Core/Core.idr

@@ -2,6 +2,7 @@ module Core.Core
 
 import Core.Env
 import Core.TT
+import Data.Vect
 import Parser.Support
 
 import public Control.Catchable
@@ -356,6 +357,10 @@ export %inline
 map : (a -> b) -> Core a -> Core b
 map f (MkCore a) = MkCore (map (map f) a)
 
+export %inline
+(<$>) : (a -> b) -> Core a -> Core b
+(<$>) f (MkCore a) = MkCore (map (map f) a)
+
 -- Monad (specialised)
 export %inline
 (>>=) : Core a -> (a -> Core b) -> Core b
@@ -398,6 +403,11 @@ export
 traverse : (a -> Core b) -> List a -> Core (List b)
 traverse f xs = traverse' f xs []
 
+export
+traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
+traverseVect f [] = pure []
+traverseVect f (x :: xs) = [| f x :: traverseVect f xs |]
+
 export
 traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)
 traverseOpt f Nothing = pure Nothing

src/Data/LengthMatch.idr

@@ -0,0 +1,14 @@
+module Data.LengthMatch
+
+public export
+data LengthMatch : List a -> List b -> Type where
+     NilMatch : LengthMatch [] []
+     ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
+
+export
+checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
+checkLengthMatch [] [] = Just NilMatch
+checkLengthMatch [] (x :: xs) = Nothing
+checkLengthMatch (x :: xs) [] = Nothing
+checkLengthMatch (x :: xs) (y :: ys)
+    = Just (ConsMatch !(checkLengthMatch xs ys))

src/Idris/Main.idr

@@ -101,7 +101,7 @@ banner : String
 banner = "     ____    __     _         ___                                           \n" ++
          "    /  _/___/ /____(_)____   |__ \\                                          \n" ++
          "    / // __  / ___/ / ___/   __/ /     Version " ++ showVersion version ++ "\n" ++
-         "  _/ // /_/ / /  / (__  )   / __/      http://www.idris-lang.org            \n" ++
+         "  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           \n" ++
          " /___/\\__,_/_/  /_/____/   /____/                                           \n" ++
          "\n" ++
          "Welcome to Idris 2.  Enjoy yourself!"