Compatibility fixes

For compatibility with previous library verions, so that we can build
with 0.2.1(+patches) as well as bootstrapping.

INSTALL.md

@@ -37,7 +37,7 @@ of `make` in the following steps.
 - Change the `PREFIX` in `config.mk`. The default is to install in
   `$HOME/.idris2`
 
-If you have an existing Idris 2, go to the alternative Step 2. Otherwise, read on...
+If you have an existing Idris 2, go to Step 3. Otherwise, read on...
 
 Make sure that:
 
@@ -69,7 +69,7 @@ If all is well, to install, type:
 
 ### 3: Installing with an existing Idris 2
 
-If you have an earlier version of this Idris 2 installed
+If you have an earlier version of Idris 2 installed
 
 - `make all`
 - `make install`

src/Core/Core.idr

@@ -517,7 +517,10 @@ for = flip traverse
 
 export
 traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
-traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |]
+traverseList1 f xxs
+    = let x = head xxs
+          xs = tail xxs in
+          [| f x ::: traverse f xs |]
 
 export
 traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
@@ -549,9 +552,11 @@ sequence [] = pure []
 
 export
 traverseList1_ : (a -> Core b) -> List1 a -> Core ()
-traverseList1_ f (x ::: xs) = do
-  f x
-  traverse_ f xs
+traverseList1_ f xxs
+    = do let x = head xxs
+         let xs = tail xxs
+         f x
+         traverse_ f xs
 
 namespace PiInfo
   export

src/Core/Hash.idr

@@ -49,7 +49,7 @@ Hashable a => Hashable (List a) where
 
 export
 Hashable a => Hashable (List1 a) where
-  hashWithSalt h (x ::: xs) = hashWithSalt (h * 33 + hash x) xs
+  hashWithSalt h xxs = hashWithSalt (h * 33 + hash (head xxs)) (tail xxs)
 
 export
 Hashable a => Hashable (Maybe a) where

src/Core/Name/Namespace.idr

@@ -49,9 +49,13 @@ nsAsModuleIdent (MkNS ns) = MkMI ns
 
 export
 mkNamespacedIdent : String -> (Maybe Namespace, String)
-mkNamespacedIdent str = case reverse (split (== '.') str) of
-  (name ::: []) => (Nothing, name)
-  (name ::: ns) => (Just (MkNS ns), name)
+mkNamespacedIdent str
+    = let nns = reverse (split (== '.') str)
+          name = head nns
+          ns = tail nns in
+          case ns of
+               [] => (Nothing, name)
+               _ => (Just (MkNS ns), name)
 
 export
 mkNestedNamespace : Maybe Namespace -> String -> Namespace

src/Core/Options/Log.idr

@@ -93,10 +93,13 @@ Pretty LogLevel where
 export
 parseLogLevel : String -> Maybe LogLevel
 parseLogLevel str = do
-  (c, n) <- case split (== ':') str of
-             n ::: [] => pure (MkLogLevel [], n)
-             ps ::: [n] => pure (mkLogLevel ps, n)
-             _ => Nothing
+  (c, n) <- let nns = split (== ':') str
+                n = head nns
+                ns = tail nns in
+                case ns of
+                     [] => pure (MkLogLevel [], n)
+                     [ns] => pure (mkLogLevel n, ns)
+                     _ => Nothing
   lvl <- parsePositive n
   pure $ c (fromInteger lvl)
 

src/Core/Reflect.idr

@@ -196,9 +196,9 @@ Reify a => Reify (List1 a) where
 
 export
 Reflect a => Reflect (List1 a) where
-  reflect fc defs lhs env (x ::: xs)
-      = do x' <- reflect fc defs lhs env x
-           xs' <- reflect fc defs lhs env xs
+  reflect fc defs lhs env xxs
+      = do x' <- reflect fc defs lhs env (head xxs)
+           xs' <- reflect fc defs lhs env (tail xxs)
            appCon fc defs (NS (mkNamespace "Data.List1") (UN ":::")) [Erased fc False, x', xs']
 
 export

src/Idris/Elab/Implementation.idr

@@ -381,7 +381,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im
              -- parameters
              let upds' = !(traverse (applyCon impName) allmeths)
              let mty_in = substNames vars upds' mty_in
-             let (upds, mty_in) = runState [] (renameIBinds impsp (findImplicits mty_in) mty_in)
+             let (upds, mty_in) = runState Prelude.Nil (renameIBinds impsp (findImplicits mty_in) mty_in)
              -- Finally update the method type so that implicits from the
              -- parameters are passed through to any earlier methods which
              -- appear in the type

src/Parser/Lexer/Source.idr

@@ -125,10 +125,11 @@ mutual
   ||| comment unless the series of uninterrupted dashes is ended with
   ||| a closing brace in which case it is a closing delimiter.
   doubleDash : (k : Nat) -> Lexer
-  doubleDash k = many (is '-') <+> choice            -- absorb all dashes
-    [ is '}' <+> toEndComment k                      -- closing delimiter
-    , many (isNot '\n') <+> toEndComment (S k)       -- line comment
-    ]
+  doubleDash k = with Prelude.(::)
+      many (is '-') <+> choice            -- absorb all dashes
+        [ is '}' <+> toEndComment k                      -- closing delimiter
+        , many (isNot '\n') <+> toEndComment (S k)       -- line comment
+        ]
 
 blockComment : Lexer
 blockComment = is '{' <+> is '-' <+> toEndComment 1

src/TTImp/Elab/App.idr

@@ -458,9 +458,9 @@ mutual
                           fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
 
   export
-  findNamed : Name -> List (Name, RawImp) -> Maybe (List1 (Name, RawImp))
+  findNamed : Name -> List (Name, RawImp) -> Maybe ((Name, RawImp), List (Name, RawImp))
   findNamed n l = case partition ((== n) . fst) l of
-                       (x :: xs, ys) => Just (x ::: (xs ++ ys))
+                       (x :: xs, ys) => Just (x, (xs ++ ys))
                        _ => Nothing
 
   export
@@ -507,7 +507,7 @@ mutual
                argdata [] autoargs namedargs kr expty with (findNamed x namedargs)
    -- We found a compatible named argument
    checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
-                argdata [] autoargs namedargs kr expty | Just ((_, arg) ::: namedargs')
+                argdata [] autoargs namedargs kr expty | Just ((_, arg), namedargs')
     = do let argRig = rig |*| rigb
          checkRestApp rig argRig elabinfo nest env fc
                       tm x aty sc argdata arg [] autoargs namedargs' kr expty
@@ -580,7 +580,7 @@ mutual
                argdata expargs [] namedargs kr expty
       = let argRig = rig |*| rigb in
             case findNamed x namedargs of
-                 Just ((_, arg) ::: namedargs') =>
+                 Just ((_, arg), namedargs') =>
                     checkRestApp rig argRig elabinfo nest env fc
                                  tm x aty sc argdata arg expargs [] namedargs' kr expty
                  Nothing =>
@@ -593,7 +593,7 @@ mutual
             case findNamed x namedargs of
                Nothing => makeImplicit rig argRig elabinfo nest env fc tm
                                        x aty sc argdata expargs autoargs namedargs kr expty
-               Just ((_, arg) ::: namedargs') =>
+               Just ((_, arg), namedargs') =>
                      checkRestApp rig argRig elabinfo nest env fc
                                   tm x aty sc argdata arg expargs autoargs namedargs' kr expty
   -- Check next default argument
@@ -603,7 +603,7 @@ mutual
             case findNamed x namedargs of
                Nothing => makeDefImplicit rig argRig elabinfo nest env fc tm
                                           x arg aty sc argdata expargs autoargs namedargs kr expty
-               Just ((_, arg) ::: namedargs') =>
+               Just ((_, arg), namedargs') =>
                      checkRestApp rig argRig elabinfo nest env fc
                                   tm x aty sc argdata arg expargs autoargs namedargs' kr expty
   -- Invent a function type if we have extra explicit arguments but type is further unknown

src/TTImp/Impossible.idr

@@ -82,7 +82,7 @@ mutual
   processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) [] autos named
      = do defs <- get Ctxt
           case findNamed x named of
-            Just ((_, e) ::: named') =>
+            Just ((_, e), named') =>
                do e' <- mkTerm e (Just ty) [] [] []
                   processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                               [] autos named'
@@ -94,7 +94,7 @@ mutual
                           processArgs (App fc fn e')
                                       !(sc defs (toClosure defaultOpts [] e'))
                                       exps autos named
-            Just ((_, e) ::: named') =>
+            Just ((_, e), named') =>
                do e' <- mkTerm e (Just ty) [] [] []
                   processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                               exps autos named'
@@ -112,7 +112,7 @@ mutual
                            processArgs (App fc fn e')
                                        !(sc defs (toClosure defaultOpts [] e'))
                                        exps [] named
-                     Just ((_, e) ::: named') =>
+                     Just ((_, e), named') =>
                         do e' <- mkTerm e (Just ty) [] [] []
                            processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                                        exps [] named'

src/Text/Lexer/Core.idr

@@ -171,12 +171,12 @@ tokenise pred line col acc tmap str
 export
 lex : TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lex tmap str
-    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
+    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
           (ts, (l, c, fastPack str'))
 
 export
 lexTo : (WithBounds a -> Bool) ->
         TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lexTo pred tmap str
-    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
+    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
           (ts, (l, c, fastPack str'))

src/Utils/Binary.idr

@@ -351,9 +351,9 @@ TTC a => TTC (List a) where
 
 export
 TTC a => TTC (List1 a) where
-  toBuf b (x ::: xs)
-     = do toBuf b x
-          toBuf b xs
+  toBuf b xxs
+     = do toBuf b (head xxs)
+          toBuf b (tail xxs)
 
   fromBuf b = do
     x <- fromBuf b