Update source for modern Idris

TinyIdris-v1/src/Core/CaseBuilder.idr

@@ -10,7 +10,7 @@ import Core.Value
 
 import Data.LengthMatch
 import Data.List
-import Data.Strings
+import Data.String
 
 import Decidable.Equality
 
@@ -22,6 +22,7 @@ data ArgType : List Name -> Type where
      Unknown : ArgType vars
          -- arg's type is not yet known due to a previously stuck argument
 
+covering
 {ns : _} -> Show (ArgType ns) where
   show (Known t) = "Known " ++ show t
   show (Stuck t) = "Stuck " ++ show t
@@ -72,15 +73,15 @@ updatePats {todo = pvar :: ns} env (NBind _ (Pi _ farg) fsc) (p :: ps)
          Unknown =>
             do defs <- get Ctxt
                empty <- clearDefs defs
-               pure (record { argType = Known !(quote empty env farg) } p
+               pure ({ argType := Known !(quote empty env farg) } p
                           :: !(updatePats env !(fsc defs (toClosure env (Ref Bound pvar))) ps))
          _ => pure (p :: ps)
 updatePats env nf (p :: ps)
   = case argType p of
          Unknown =>
             do defs <- get Ctxt
                empty <- clearDefs defs
-               pure (record { argType = Stuck !(quote empty env nf) } p :: ps)
+               pure ({ argType := Stuck !(quote empty env nf) } p :: ps)
          _ => pure (p :: ps)
 
 substInPatInfo : {pvar, vars, todo : _} ->
@@ -90,14 +91,14 @@ substInPatInfo : {pvar, vars, todo : _} ->
                  Core (PatInfo pvar vars, NamedPats vars todo)
 substInPatInfo {pvar} {vars} n tm p ps
     = case argType p of
-           Known ty => pure (record { argType = Known (substName n tm ty) } p, ps)
+           Known ty => pure ({ argType := Known (substName n tm ty) } p, ps)
            Stuck fty =>
              do defs <- get Ctxt
                 empty <- clearDefs defs
                 let env = mkEnv vars
                 case !(nf defs env (substName n tm fty)) of
                      NBind _ (Pi _ farg) fsc =>
-                       pure (record { argType = Known !(quote empty env farg) } p,
+                       pure ({ argType := Known !(quote empty env farg) } p,
                                  !(updatePats env
                                        !(fsc defs (toClosure env
                                              (Ref Bound pvar))) ps))
@@ -259,7 +260,6 @@ checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pa
                             (Just Refl, Yes Refl) => ConMatch prf
                             _ => NoMatch
 checkGroupMatch (CName x tag) ps _ = NoMatch
-checkGroupMatch _ _ _ = NoMatch
 
 data PName : Type where
 
@@ -305,7 +305,7 @@ newPats : (pargs : List Pat) -> LengthMatch pargs ns ->
           NamedPats vars ns
 newPats [] NilMatch rest = []
 newPats (newpat :: xs) (ConsMatch w) (pi :: rest)
-  = record { pat = newpat} pi :: newPats xs w rest
+  = { pat := newpat} pi :: newPats xs w rest
 
 updateNames : List (Name, Pat) -> List (Name, Name)
 updateNames = mapMaybe update
@@ -317,7 +317,7 @@ updateNames = mapMaybe update
 updatePatNames : List (Name, Name) -> NamedPats vars todo -> NamedPats vars todo
 updatePatNames _ [] = []
 updatePatNames ns (pi :: ps)
-    = record { pat $= update } pi :: updatePatNames ns ps
+    = { pat $= update } pi :: updatePatNames ns ps
   where
     update : Pat -> Pat
     update (PCon n i a ps) = PCon n i a (map update ps)
@@ -641,7 +641,7 @@ mutual
            pure (Just !(varRule fn vs fallthrough))
   mixture fn {a} {todo} NoClauses err
       = pure err
--- 
+--
 
 mkPatClause : {auto c : Ref Ctxt Defs} ->
               Name ->

TinyIdris-v1/src/Core/CaseTree.idr

@@ -71,7 +71,7 @@ data Pat : Type where
      PLoc : Name -> Pat
      PUnmatchable : Term [] -> Pat
 
-export
+export covering
 Show Pat where
   show (PCon n t a args) = show n ++ show (t, a) ++ show args
   show (PLoc n) = "{" ++ show n ++ "}"
@@ -104,7 +104,7 @@ mkTerm vars (PUnmatchable tm) = embed tm
 -- Show instances
 
 mutual
-  export
+  export covering
   {vars : _} -> Show (CaseTree vars) where
     show (Case {name} idx prf ty alts)
         = "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of { " ++
@@ -113,7 +113,7 @@ mutual
     show (Unmatched msg) = "Error: " ++ show msg
     show Impossible = "Impossible"
 
-  export
+  export covering
   {vars : _} -> Show (CaseAlt vars) where
     show (ConCase n tag args sc)
         = show n ++ " " ++ showSep " " (map show args) ++ " => " ++

TinyIdris-v1/src/Core/Core.idr

@@ -36,7 +36,7 @@ data Error : Type where
      GenericMsg : String -> Error
      FileErr : String -> FileError -> Error
 
-export
+export covering
 Show Error where
   show (CantConvert env x y)
       = "Type mismatch: " ++ show x ++ " and " ++ show y
@@ -116,6 +116,10 @@ export %inline
 pure : a -> Core a
 pure x = MkCore (pure (pure x))
 
+export %inline
+(>>) : Core a -> (Core b) -> Core b
+(>>) a b = do _ <- a ; b
+
 export
 (<*>) : Core (a -> b) -> Core a -> Core b
 (<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |]
@@ -153,7 +157,7 @@ traverse f xs = traverse' f xs []
 
 export
 traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
-traverseList1 f (x :: xs) = [| f x :: traverse f xs |]
+traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |]
 
 export
 traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
@@ -174,7 +178,7 @@ traverse_ f (x :: xs)
 
 export
 traverseList1_ : (a -> Core b) -> List1 a -> Core ()
-traverseList1_ f (x :: xs) = do
+traverseList1_ f (x ::: xs) = do
   f x
   traverse_ f xs
 

TinyIdris-v1/src/Core/Env.idr

@@ -8,7 +8,7 @@ data Env : (tm : List Name -> Type) -> List Name -> Type where
      Nil : Env tm []
      (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
 
-revOnto : (xs, vs : _) -> reverseOnto xs vs = reverse vs ++ xs
+revOnto : (xs, vs : _) -> List.reverseOnto xs vs = reverse vs ++ xs
 revOnto xs [] = Refl
 revOnto xs (v :: vs)
     = rewrite revOnto (v :: xs) vs in
@@ -28,7 +28,7 @@ revNs (v :: vs) ns
 -- in big environments
 -- Also reversing the names at the end saves significant time over concatenating
 -- when environments get fairly big.
-getBinderUnder : Weaken tm =>
+getBinderUnder : {tm : _} -> Weaken tm =>
                  {vars : _} -> {idx : Nat} ->
                  (ns : List Name) ->
                  (0 p : IsVar x idx vars) -> Env tm vars ->
@@ -39,7 +39,7 @@ getBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env)
     = getBinderUnder (v :: ns) lp env
 
 export
-getBinder : Weaken tm =>
+getBinder : {tm : _} -> Weaken tm =>
             {vars : _} -> {idx : Nat} ->
             (0 p : IsVar x idx vars) -> Env tm vars -> Binder (tm vars)
 getBinder el env = getBinderUnder [] el env

TinyIdris-v1/src/Core/Normalise.idr

@@ -14,7 +14,7 @@ import Data.Vect
 -- part will only be constructed when needed, because it's in Core.
 public export
 data Glued : List Name -> Type where
-     MkGlue : Core (Term vars) -> 
+     MkGlue : Core (Term vars) ->
               (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars
 
 export
@@ -39,7 +39,7 @@ data CaseResult a
      = Result a
      | NoMatch -- case alternative didn't match anything
      | GotStuck -- alternative matched, but got stuck later
- 
+
 -- So that we can call 'eval' with new defs
 evalTop : {free, vars : _} ->
           Defs -> Env Term free -> LocalEnv free vars ->

TinyIdris-v1/src/Core/TT.idr

@@ -125,7 +125,7 @@ data Term : List Name -> Type where
      Erased : Term vars
 
 public export
-interface Weaken (tm : List Name -> Type) where
+interface Weaken (0  tm : List Name -> Type) where
   weaken : {n, vars : _} -> tm vars -> tm (n :: vars)
   weakenNs : {vars : _} -> (ns : List Name) -> tm vars -> tm (ns ++ vars)
 
@@ -384,7 +384,7 @@ nameAt : {vars : _} ->
 nameAt {vars = n :: ns} Z First = n
 nameAt {vars = n :: ns} (S k) (Later p) = nameAt k p
 
-export 
+export covering
 {vars : _} -> Show (Term vars) where
   show tm = let (fn, args) = getFnArgs tm in showApp fn args
     where

TinyIdris-v1/src/Parser/Lexer/Package.idr

@@ -6,7 +6,7 @@ import public Text.Parser
 
 import Data.List
 import Data.List1
-import Data.Strings
+import Data.String
 import Data.String.Extra
 import Utils.String
 
@@ -27,7 +27,7 @@ Show Token where
   show (Comment str) = "Comment: " ++ str
   show EndOfInput = "EndOfInput"
   show Equals = "Equals"
-  show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (List1.toList dsid)
+  show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (toList dsid)
   show Separator = "Separator"
   show Space = "Space"
   show (StringLit s) = "StringLit: " ++ s
@@ -50,7 +50,7 @@ rawTokens =
   ]
   where
     splitNamespace : String -> List1 String
-    splitNamespace = Data.Strings.split (== '.')
+    splitNamespace = split (== '.')
 
 export
 lex : String -> Either (Int, Int, String) (List (TokenData Token))

TinyIdris-v1/src/Parser/Lexer/Source.idr

@@ -4,7 +4,7 @@ import public Parser.Lexer.Common
 
 import Data.List1
 import Data.List
-import Data.Strings
+import Data.String
 import Data.String.Extra
 
 import Utils.Hex
@@ -46,7 +46,7 @@ Show Token where
   -- Identifiers
   show (HoleIdent x) = "hole identifier " ++ x
   show (Ident x) = "identifier " ++ x
-  show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (List1.toList $ reverse xs)
+  show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (toList $ reverse xs)
   show (DotIdent x) = "dot+identifier " ++ x
   show (Symbol x) = "symbol " ++ x
   -- Comments
@@ -222,7 +222,7 @@ rawTokens =
                    else Ident x
     parseNamespace : String -> Token
     parseNamespace ns = case List1.reverse . split (== '.') $ ns of
-                             [ident] => parseIdent ident
+                             (ident ::: []) => parseIdent ident
                              ns      => DotSepIdent ns
 
 export

TinyIdris-v1/src/Parser/Rule/Package.idr

@@ -34,7 +34,7 @@ export
 exactProperty : String -> Rule String
 exactProperty p = terminal ("Expected property " ++ p)
                            (\x => case tok x of
-                                       DotSepIdent [p'] =>
+                                       DotSepIdent (p' ::: []) =>
                                          if p == p' then Just p
                                          else Nothing
                                        _ => Nothing)
@@ -64,7 +64,7 @@ export
 packageName : Rule String
 packageName = terminal "Expected package name"
                        (\x => case tok x of
-                                   DotSepIdent [str] =>
+                                   DotSepIdent (str ::: []) =>
                                      if isIdent AllowDashes str then Just str
                                      else Nothing
                                    _ => Nothing)

TinyIdris-v1/src/Parser/Rule/Source.idr

@@ -6,7 +6,7 @@ import public Parser.Support
 
 import Core.TT
 import Data.List1
-import Data.Strings
+import Data.String
 
 %default total
 
@@ -124,7 +124,7 @@ namespacedIdent
     = terminal "Expected namespaced name"
         (\x => case tok x of
             DotSepIdent ns => Just ns
-            Ident i => Just [i]
+            Ident i => Just (singleton i)
             _ => Nothing)
 
 export
@@ -133,7 +133,7 @@ moduleIdent
     = terminal "Expected module identifier"
         (\x => case tok x of
             DotSepIdent ns => Just ns
-            Ident i => Just [i]
+            Ident i => Just (singleton i)
             _ => Nothing)
 
 export
@@ -168,8 +168,8 @@ init = 0
 
 continueF : SourceEmptyRule () -> (indent : IndentInfo) -> SourceEmptyRule ()
 continueF err indent
-    = do eoi; err
-  <|> do keyword "where"; err
+    = eoi *> err
+  <|> keyword "where" *> err
   <|> do col <- Common.column
          if col <= indent
             then err
@@ -259,9 +259,9 @@ atEndIndent indent
 -- must start, given where the current block entry started
 terminator : ValidIndent -> Int -> SourceEmptyRule ValidIndent
 terminator valid laststart
-    = do eoi
-         pure EndOfBlock
-  <|> do symbol ";"
+    = (eoi *>
+         pure EndOfBlock)
+  <|> symbol ";" *>
          pure (afterSemi valid)
   <|> do col <- column
          afterDedent valid col
@@ -307,7 +307,7 @@ blockEntry valid rule
 blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
                SourceEmptyRule (List ty)
 blockEntries valid rule
-     = do eoi; pure []
+     = eoi *> pure []
    <|> do res <- blockEntry valid rule
           ts <- blockEntries (snd res) rule
           pure (fst res :: ts)

TinyIdris-v1/src/Parser/Unlit.idr

@@ -1,7 +1,7 @@
 module Parser.Unlit
 
 import public Text.Literate
-import Data.Strings
+import Data.String
 
 %default total