Merge branch 'master' of github.com:idris-lang/Idris-dev

Setup.hs

@@ -1,11 +1,15 @@
 {-# LANGUAGE CPP #-}
 
+#if !defined(MIN_VERSION_Cabal)
+# define MIN_VERSION_Cabal(x,y,z) 0
+#endif
+
 import Control.Monad
 import Data.IORef
 import Control.Exception (SomeException, catch)
 
 import Distribution.Simple
-import Distribution.Simple.BuildPaths (autogenModulesDir)
+import Distribution.Simple.BuildPaths
 import Distribution.Simple.InstallDirs as I
 import Distribution.Simple.LocalBuildInfo as L
 import qualified Distribution.Simple.Setup as S
@@ -56,32 +60,37 @@ windres verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation
 
 usesGMP :: S.ConfigFlags -> Bool
 usesGMP flags =
-  case lookup (FlagName "gmp") (S.configConfigurationsFlags flags) of
+  case lookup (mkFlagName "gmp") (S.configConfigurationsFlags flags) of
     Just True -> True
     Just False -> False
     Nothing -> False
 
 execOnly :: S.ConfigFlags -> Bool
 execOnly flags =
-  case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of
+  case lookup (mkFlagName "execonly") (S.configConfigurationsFlags flags) of
     Just True -> True
     Just False -> False
     Nothing -> False
 
 isRelease :: S.ConfigFlags -> Bool
 isRelease flags =
-    case lookup (FlagName "release") (S.configConfigurationsFlags flags) of
+    case lookup (mkFlagName "release") (S.configConfigurationsFlags flags) of
       Just True -> True
       Just False -> False
       Nothing -> False
 
 isFreestanding :: S.ConfigFlags -> Bool
 isFreestanding flags =
-  case lookup (FlagName "freestanding") (S.configConfigurationsFlags flags) of
+  case lookup (mkFlagName "freestanding") (S.configConfigurationsFlags flags) of
     Just True -> True
     Just False -> False
     Nothing -> False
 
+#if !(MIN_VERSION_Cabal(2,0,0))
+mkFlagName :: String -> FlagName
+mkFlagName = FlagName
+#endif
+
 -- -----------------------------------------------------------------------------
 -- Clean
 
@@ -151,20 +160,22 @@ generateToolchainModule verbosity srcDir toolDir = do
     createDirectoryIfMissingVerbose verbosity True srcDir
     rewriteFile toolPath (commonContent ++ toolContent)
 
-idrisConfigure _ flags _ local = do
+idrisConfigure _ flags pkgdesc local = do
     configureRTS
-    generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))
-    if isFreestanding $ configFlags local
-        then do
-                toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"
-                generateToolchainModule verbosity (autogenModulesDir local) toolDir
-                targetDir <- lookupEnv "IDRIS_LIB_DIR"
-                case targetDir of
-                     Just d -> generateTargetModule verbosity (autogenModulesDir local) d
-                     Nothing -> error $ "Trying to build freestanding without a target directory."
-                                  ++ " Set it by defining IDRIS_LIB_DIR."
-        else
-                generateToolchainModule verbosity (autogenModulesDir local) Nothing
+    withLibLBI pkgdesc local $ \_ libcfg -> do
+      let libAutogenDir = autogenComponentModulesDir local libcfg
+      generateVersionModule verbosity libAutogenDir (isRelease (configFlags local))
+      if isFreestanding $ configFlags local
+          then do
+                  toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"
+                  generateToolchainModule verbosity libAutogenDir toolDir
+                  targetDir <- lookupEnv "IDRIS_LIB_DIR"
+                  case targetDir of
+                       Just d -> generateTargetModule verbosity libAutogenDir d
+                       Nothing -> error $ "Trying to build freestanding without a target directory."
+                                    ++ " Set it by defining IDRIS_LIB_DIR."
+          else
+                  generateToolchainModule verbosity libAutogenDir Nothing
     where
       verbosity = S.fromFlag $ S.configVerbosity flags
       version   = pkgVersion . package $ localPkgDescr local
@@ -175,6 +186,10 @@ idrisConfigure _ flags _ local = do
       -- the file after configure.
       configureRTS = make verbosity ["-C", "rts", "clean"]
 
+#if !(MIN_VERSION_Cabal(2,0,0))
+      autogenComponentModulesDir lbi _ = autogenModulesDir lbi
+#endif
+
 idrisPreSDist args flags = do
   let dir = S.fromFlag (S.sDistDirectory flags)
   let verb = S.fromFlag (S.sDistVerbosity flags)

docs/reference/partial-evaluation.rst

@@ -4,15 +4,15 @@ Static Arguments and Partial Evaluation
 
 As of version 0.9.15, Idris has support for *partial evaluation* of
 statically known arguments. This involves creating specialised versions
-of functions with arguments annotated as ``[static]``.
+of functions with arguments annotated as ``%static``.
 
 (This is an implementation of the partial evaluator described in `this
 ICFP 2010
 paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
 Please refer to this for more precise definitions of what follows.)
 
-Partial evaluation is switched on by default. It can be disabled with
-the ``--no-partial-eval`` flag.
+Partial evaluation is switched off by default since Idris 1.0. It can
+be enabled with the ``--partial-eval`` flag.
 
 Introductory Example
 --------------------
@@ -66,18 +66,18 @@ Automatic specialisation of ``pow``
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The trick is to mark the statically known arguments with the
-``[static]`` flag:
+``%static`` flag:
 
 ::
 
-    my_pow : Nat -> [static] Nat -> Nat
+    my_pow : Nat -> %static Nat -> Nat
     my_pow k Z = 1
     my_pow k (S j) = mult k (my_pow k j)
 
 When an argument is annotated in this way, Idris will try to create a
 specialised version whenever it accounts a call with a concrete value
 (i.e. a constant, constructor form, or globally defined function) in a
-``[static]`` position. If ``my_pow`` is defined this way, and ``powFn``
+``%static`` position. If ``my_pow`` is defined this way, and ``powFn``
 defined as above, we can see the effect by typing ``:printdef powFn`` at
 the REPL:
 
@@ -108,7 +108,7 @@ Specialising Type Classes
 -------------------------
 
 Type class dictionaries are very often statically known, so Idris
-automatically marks any type class constraint as ``[static]`` and builds
+automatically marks any type class constraint as ``%static`` and builds
 specialised versions of top level functions where the class is
 instantiated. For example, given:
 
@@ -177,7 +177,7 @@ writing ``map`` as follows:
 
 ::
 
-    my_map : [static] (a -> b) -> List a -> List b
+    my_map : %static (a -> b) -> List a -> List b
     my_map f [] = []
     my_map f (x :: xs) = f x :: my_map f xs
 
@@ -246,11 +246,11 @@ Then, a function which calculates the factorial of its input:
                 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
 
 The interpreter's type is written as follows, marking the expression to
-be evaluated as ``[static]``:
+be evaluated as ``%static``:
 
 ::
 
-    interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t
+    interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t
 
 This means that if we write an Idris program to calculate a factorial by
 calling ``interp`` on ``eFac``, the resulting definition will be

idris.cabal

@@ -97,6 +97,14 @@ source-repository head
   type:     git
   location: git://github.com/idris-lang/Idris-dev.git
 
+custom-setup
+  setup-depends:
+    Cabal >= 1.10 && <2.1,
+    base  >= 4 && <5,
+    directory,
+    filepath,
+    process
+
 Flag FFI
   Description:  Build support for libffi
   Default:      False
@@ -265,11 +273,11 @@ Library
                 , ansi-wl-pprint < 0.7
                 , array >= 0.4.0.1 && < 0.6
                 , base64-bytestring < 1.1
-                , binary >= 0.7 && < 0.9
+                , binary >= 0.8.4.1 && < 0.9
                 , blaze-html >= 0.6.1.3 && < 0.10
                 , blaze-markup >= 0.5.2.1 && < 0.9
                 , bytestring < 0.11
-                , cheapskate < 0.1.1
+                , cheapskate >= 0.1.1 && < 0.2
                 , code-page >= 0.1 && < 0.2
                 , containers >= 0.5 && < 0.6
                 , deepseq < 1.5

libs/contrib/Text/Lexer.idr

@@ -23,11 +23,11 @@ public export
 inf : Bool -> Type -> Type
 inf True t = Inf t
 inf False t = t
-  
+
 ||| Sequence two recognisers. If either consumes a character, the sequence
 ||| is guaranteed to consume a character.
 export %inline
-(<+>) : {c1 : Bool} -> 
+(<+>) : {c1 : Bool} ->
         Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
 (<+>) {c1 = False} = SeqEmpty
 (<+>) {c1 = True} = SeqEat
@@ -59,6 +59,17 @@ export
 many : Lexer -> Recognise False
 many l = some l <|> Empty
 
+||| Recognise many instances of `l` until an instance of `end` is
+||| encountered.
+|||
+||| Useful for defining comments.
+export
+manyTill : (l : Lexer)
+        -> (end : Lexer) -> Recognise False
+manyTill l end = end
+             <|> (l <+> manyTill l end)
+             <|> Empty
+
 ||| Recognise any character
 export
 any : Lexer
@@ -86,7 +97,7 @@ getString : StrLen -> String
 getString (MkStrLen str n) = str
 
 strIndex : StrLen -> Nat -> Maybe Char
-strIndex (MkStrLen str len) i 
+strIndex (MkStrLen str len) i
     = if i >= len then Nothing
                   else Just (assert_total (prim__strIndex str (cast i)))
 
@@ -102,25 +113,25 @@ strTail start (MkStrLen str len)
 scan : Recognise c -> Nat -> StrLen -> Maybe Nat
 scan Empty idx str = pure idx
 scan Fail idx str = Nothing
-scan (Pred f) idx str 
+scan (Pred f) idx str
     = do c <- strIndex str idx
          if f c
             then Just (idx + 1)
             else Nothing
-scan (SeqEat r1 r2) idx str 
+scan (SeqEat r1 r2) idx str
     = do idx' <- scan r1 idx str
          -- TODO: Can we prove totality instead by showing idx has increased?
          assert_total (scan r2 idx' str)
-scan (SeqEmpty r1 r2) idx str 
+scan (SeqEmpty r1 r2) idx str
     = do idx' <- scan r1 idx str
          scan r2 idx' str
-scan (Alt r1 r2) idx str 
+scan (Alt r1 r2) idx str
     = case scan r1 idx str of
            Nothing => scan r2 idx str
            Just idx => Just idx
 
 takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
-takeToken lex str 
+takeToken lex str
     = do i <- scan lex 0 str -- i must be > 0 if successful
          pure (substr 0 i (getString str), strTail i str)
 
@@ -134,7 +145,7 @@ export
 exact : String -> Lexer
 exact str with (unpack str)
   exact str | [] = Fail -- Not allowed, Lexer has to consume
-  exact str | (x :: xs) 
+  exact str | (x :: xs)
       = foldl SeqEmpty (is x) (map is xs)
 
 ||| Recognise a whitespace character
@@ -185,8 +196,8 @@ record TokenData a where
 
 fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
 fspanEnd k p "" = (k, "")
-fspanEnd k p xxs 
-    = assert_total $ 
+fspanEnd k p xxs
+    = assert_total $
       let x = prim__strHead xxs
           xs = prim__strTail xxs in
           if p x then fspanEnd (S k) p xs
@@ -195,14 +206,14 @@ fspanEnd k p xxs
 -- Faster version of 'span' from the prelude (avoids unpacking)
 export
 fspan : (Char -> Bool) -> String -> (String, String)
-fspan p xs 
+fspan p xs
     = let (end, rest) = fspanEnd 0 p xs in
           (substr 0 end xs, rest)
 
 tokenise : (line : Int) -> (col : Int) ->
-           List (TokenData a) -> TokenMap a -> 
+           List (TokenData a) -> TokenMap a ->
            StrLen -> (List (TokenData a), (Int, Int, StrLen))
-tokenise line col acc tmap str 
+tokenise line col acc tmap str
     = case getFirstToken tmap str of
            Just (tok, line', col', rest) =>
            -- assert total because getFirstToken must consume something
@@ -213,7 +224,7 @@ tokenise line col acc tmap str
     countNLs str = List.length (filter (== '\n') str)
 
     getCols : String -> Int -> Int
-    getCols x c 
+    getCols x c
          = case fspan (/= '\n') (reverse x) of
                 (incol, "") => c + cast (length incol)
                 (incol, _) => cast (length incol)
@@ -223,7 +234,7 @@ tokenise line col acc tmap str
     getFirstToken ((lex, fn) :: ts) str
         = case takeToken lex str of
                Just (tok, rest) => Just (MkToken line col (fn tok),
-                                         line + cast (countNLs (unpack tok)), 
+                                         line + cast (countNLs (unpack tok)),
                                          getCols tok col, rest)
                Nothing => getFirstToken ts str
 
@@ -235,4 +246,3 @@ export
 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
                    (ts, (l, c, getString str'))
-