diff --git a/INSTALL.md b/INSTALL.md index d22a5aa..99fdd83 100644 --- a/INSTALL.md +++ b/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) diff --git a/Notes/IDE-mode.md b/Notes/IDE-mode.md index 02a2947..1789d04 100644 --- a/Notes/IDE-mode.md +++ b/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: diff --git a/README.md b/README.md index fb180c2..df639df 100644 --- a/README.md +++ b/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)") diff --git a/docs/LICENSE b/docs/LICENSE index d1580a4..897ab8f 100644 --- a/docs/LICENSE +++ b/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/ diff --git a/docs/Makefile b/docs/Makefile index 21b2726..9baab9d 100644 --- a/docs/Makefile +++ b/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. diff --git a/docs/README.md b/docs/README.md index 15511d3..1698219 100644 --- a/docs/README.md +++ b/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. diff --git a/docs/index.rst b/docs/index.rst index 5972443..7c7eccf 100644 --- a/docs/index.rst +++ b/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. diff --git a/docs/make.bat b/docs/make.bat index 566f3c8..9c772a9 100644 --- a/docs/make.bat +++ b/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 ) diff --git a/docs/reference/index.rst b/docs/reference/index.rst index a884f58..00d2305 100644 --- a/docs/reference/index.rst +++ b/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. diff --git a/src/Compiler/Inline.idr b/src/Compiler/Inline.idr index baa957e..39e1ad8 100644 --- a/src/Compiler/Inline.idr +++ b/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) - 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) + = pure $ unload stk $ COp fc p !(traverseVect (eval rec env []) args) 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 => - do def' <- case def of - 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 + Nothing <- pickAlt rec env stk sc' alts def | Just val => pure val + def' <- traverseOpt (eval rec env stk) def + pure $ CConCase fc sc' + !(traverse (evalAlt fc rec env stk) alts) + def' 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 => - do def' <- case def of - 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 + Nothing <- pickConstAlt rec env stk sc' alts def | Just val => pure val + def' <- traverseOpt (eval rec env stk) def + pure $ CConstCase fc sc' + !(traverse (evalConstAlt rec env stk) alts) + def' 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 - Nothing => pure Nothing - Just d => pure $ Just !(eval rec env stk d) + = traverseOpt (eval rec env stk) def 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 - Nothing => pure Nothing - Just d => pure $ Just !(eval rec env stk d) + = traverseOpt (eval rec env stk) def 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 - Nothing => pure () - Just def => - 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 + Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure () + let Just cexpr = compexpr def | Nothing => pure () + setCompiled n !(inline cexpr) diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr index 007e551..8587f2a 100644 --- a/src/Core/CaseBuilder.idr +++ b/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) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 18ca980..ab59dc9 100644 --- a/src/Core/Core.idr +++ b/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 diff --git a/src/Data/LengthMatch.idr b/src/Data/LengthMatch.idr new file mode 100644 index 0000000..bac69ba --- /dev/null +++ b/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)) diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index c429888..bd30548 100644 --- a/src/Idris/Main.idr +++ b/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!"