diff --git a/.gitignore b/.gitignore index e3ca3da4e..3f0afd9a6 100644 --- a/.gitignore +++ b/.gitignore @@ -34,7 +34,7 @@ idris2docs_venv /bootstrap/idris2-0*/ /bootstrap/idris2_app/idris2-boot* /bootstrap/idris2_app/libidris2_support.* -/bootstrap/idris2boot -/bootstrap/idris2boot.rkt +/bootstrap/idris2-boot +/bootstrap/idris2-boot.rkt -/custom.mk \ No newline at end of file +/custom.mk diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index 3e82fbc9c..b9264da59 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -1,6 +1,7 @@ module Data.List import Data.Nat +import Data.List1 public export isNil : List a -> Bool @@ -188,11 +189,11 @@ break : (a -> Bool) -> List a -> (List a, List a) break p xs = span (not . p) xs public export -split : (a -> Bool) -> List a -> List (List a) +split : (a -> Bool) -> List a -> List1 (List a) split p xs = case break p xs of (chunk, []) => [chunk] - (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest) + (chunk, (c :: rest)) => chunk :: toList (split p (assert_smaller xs rest)) public export splitAt : (n : Nat) -> (xs : List a) -> (List a, List a) @@ -243,7 +244,7 @@ tails xs = xs :: case xs of ||| ``` ||| public export -splitOn : Eq a => a -> List a -> List (List a) +splitOn : Eq a => a -> List a -> List1 (List a) splitOn a = split (== a) ||| Replaces all occurences of the first argument with the second argument in a list. @@ -590,8 +591,8 @@ Uninhabited (Prelude.(::) x xs = []) where ||| (::) is injective export -consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} -> - x :: xs = y :: ys -> (x = y, xs = ys) +consInjective : forall x, xs, y, ys . + the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys) consInjective Refl = (Refl, Refl) ||| The empty list is a right identity for append. @@ -606,7 +607,7 @@ appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r appendAssociative [] c r = Refl appendAssociative (_::xs) c r = rewrite appendAssociative xs c r in Refl -revOnto : (xs, vs : _) -> reverseOnto xs vs = reverse vs ++ xs +revOnto : (xs, vs : List a) -> reverseOnto xs vs = reverse vs ++ xs revOnto _ [] = Refl revOnto xs (v :: vs) = rewrite revOnto (v :: xs) vs in @@ -630,4 +631,4 @@ dropFusion (S n) Z l = rewrite plusZeroRightNeutral n in Refl dropFusion (S n) (S m) [] = Refl dropFusion (S n) (S m) (x::l) = rewrite plusAssociative n 1 m in rewrite plusCommutative n 1 in - dropFusion (S n) m l \ No newline at end of file + dropFusion (S n) m l diff --git a/libs/base/Data/List1.idr b/libs/base/Data/List1.idr new file mode 100644 index 000000000..2cbe6c8dd --- /dev/null +++ b/libs/base/Data/List1.idr @@ -0,0 +1,61 @@ +module Data.List1 + +%default total + +public export +record List1 a where + constructor (::) + head : a + tail : List a + +public export +toList : (1 xs : List1 a) -> List a +toList (x :: xs) = x :: xs + +public export +reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a +reverseOnto acc [] = acc +reverseOnto acc (x :: xs) = reverseOnto (x :: toList acc) xs + +public export +reverse : (1 xs : List1 a) -> List1 a +reverse (x :: xs) = reverseOnto [x] xs + +export +fromList : (1 xs : List a) -> Maybe (List1 a) +fromList [] = Nothing +fromList (x :: xs) = Just (x :: xs) + +export +appendl : (1 xs : List1 a) -> (1 ys : List a) -> List1 a +appendl (x :: xs) ys = x :: xs ++ ys + +export +append : (1 xs, ys : List1 a) -> List1 a +append xs ys = appendl xs (toList ys) + +export +lappend : (1 xs : List a) -> (1 ys : List1 a) -> List1 a +lappend [] ys = ys +lappend (x :: xs) ys = append (x :: xs) ys + +export +Functor List1 where + map f (x :: xs) = f x :: map f xs + +export +Foldable List1 where + foldr c n (x :: xs) = c x (foldr c n xs) + +export +Show a => Show (List1 a) where + show = show . toList + +export +Applicative List1 where + pure x = [x] + f :: fs <*> xs = appendl (map f xs) (fs <*> toList xs) + +export +Monad List1 where + (x :: xs) >>= f = appendl (f x) (xs >>= toList . f) diff --git a/libs/base/Data/Strings.idr b/libs/base/Data/Strings.idr index 925182d6c..486c64291 100644 --- a/libs/base/Data/Strings.idr +++ b/libs/base/Data/Strings.idr @@ -1,6 +1,7 @@ module Data.Strings import Data.List +import Data.List1 export singleton : Char -> String @@ -152,7 +153,7 @@ break p = span (not . p) ||| split (== '.') ".AB.C..D" ||| ``` public export -split : (Char -> Bool) -> String -> List String +split : (Char -> Bool) -> String -> List1 String split p xs = map pack (split p (unpack xs)) export @@ -224,15 +225,15 @@ parseNumWithoutSign (c :: cs) acc = ||| ``` public export parsePositive : Num a => String -> Maybe a -parsePositive s = parsePosTrimmed (trim s) +parsePositive s = parsePosTrimmed (trim s) where parsePosTrimmed : String -> Maybe a parsePosTrimmed s with (strM s) parsePosTrimmed "" | StrNil = Nothing - parsePosTrimmed (strCons '+' xs) | (StrCons '+' xs) = + parsePosTrimmed (strCons '+' xs) | (StrCons '+' xs) = map fromInteger (parseNumWithoutSign (unpack xs) 0) - parsePosTrimmed (strCons x xs) | (StrCons x xs) = - if (x >= '0' && x <= '9') + parsePosTrimmed (strCons x xs) | (StrCons x xs) = + if (x >= '0' && x <= '9') then map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0'))) else Nothing @@ -246,15 +247,15 @@ parsePositive s = parsePosTrimmed (trim s) ||| ``` public export parseInteger : (Num a, Neg a) => String -> Maybe a -parseInteger s = parseIntTrimmed (trim s) +parseInteger s = parseIntTrimmed (trim s) where parseIntTrimmed : String -> Maybe a parseIntTrimmed s with (strM s) parseIntTrimmed "" | StrNil = Nothing - parseIntTrimmed (strCons x xs) | (StrCons x xs) = - if (x == '-') + parseIntTrimmed (strCons x xs) | (StrCons x xs) = + if (x == '-') then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0) - else if (x == '+') + else if (x == '+') then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0)) else if (x >= '0' && x <= '9') then map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0'))) diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index 4d5f2f8e4..0c2ced1f7 100644 --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -24,6 +24,7 @@ modules = Control.App, Data.List.Elem, Data.List.Views, Data.List.Quantifiers, + Data.List1, Data.Maybe, Data.Morphisms, Data.Nat, diff --git a/libs/contrib/Data/List/TailRec.idr b/libs/contrib/Data/List/TailRec.idr index fc2f4cb2b..82990a650 100644 --- a/libs/contrib/Data/List/TailRec.idr +++ b/libs/contrib/Data/List/TailRec.idr @@ -20,6 +20,7 @@ import Syntax.PreorderReasoning import Syntax.WithProof import Data.List +import Data.List1 import Data.Vect import Data.Nat @@ -118,14 +119,14 @@ break_ext : (p : a -> Bool) -> (xs : List a) -> Data.List.break p xs = Data.List.TailRec.break p xs break_ext p xs = span_ext (not . p) xs -splitOnto : List (List a) -> (a -> Bool) -> List a -> List (List a) +splitOnto : List (List a) -> (a -> Bool) -> List a -> List1 (List a) splitOnto acc p xs = case Data.List.break p xs of (chunk, [] ) => reverseOnto [chunk] acc (chunk, (c::rest)) => splitOnto (chunk::acc) p rest export -split : (a -> Bool) -> List a -> List (List a) +split : (a -> Bool) -> List a -> List1 (List a) split p xs = splitOnto [] p xs splitOnto_ext : (acc : List (List a)) -> (p : a -> Bool) -> (xs : List a) -> diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 2a403fe1a..e46bdcd30 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -6,6 +6,7 @@ module Network.Socket.Data import Data.List +import Data.List1 import Data.Strings -- ------------------------------------------------------------ [ Type Aliases ] @@ -194,7 +195,7 @@ parseIPv4 str = toInt : String -> Int toInt s = fromInteger $ toInt' s - splitted : List Int + splitted : List1 Int splitted = map toInt (split (\c => c == '.') str) -- --------------------------------------------------------- [ UDP Information ] diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr index b4ca57f9f..518c8755c 100644 --- a/libs/prelude/Prelude/Types.idr +++ b/libs/prelude/Prelude/Types.idr @@ -280,12 +280,12 @@ Ord a => Ord (List a) where namespace List public export - (++) : (1 xs : List a) -> List a -> List a + (++) : (1 xs, ys : List a) -> List a [] ++ ys = ys (x :: xs) ++ ys = x :: xs ++ ys public export - length : (xs : List a) -> Nat + length : List a -> Nat length [] = Z length (x :: xs) = S (length xs) diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index 0bf308728..de943a979 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -2,6 +2,7 @@ module Compiler.ES.ES import Compiler.ES.Imperative import Utils.Hex +import Data.List1 import Data.Strings import Data.SortedMap import Data.String.Extra @@ -271,7 +272,7 @@ makeForeign n x = "lambdaRequire" => do let (libs, def_) = readCCPart def - traverse addRequireToPreamble (split (==',') libs) + traverseList1 addRequireToPreamble (split (==',') libs) pure $ "const " ++ jsName n ++ " = (" ++ def_ ++ ")\n" "support" => do diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 3f8519c3c..f75a070b9 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -14,6 +14,7 @@ import Utils.Hex import Utils.Path import Data.List +import Data.List1 import Data.Maybe import Data.NameMap import Data.Strings @@ -26,11 +27,10 @@ import System.Info %default covering - pathLookup : IO String pathLookup = do path <- getEnv "PATH" - let pathList = split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path + let pathList = List1.toList $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path let candidates = [p ++ "/" ++ x | p <- pathList, x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]] e <- firstExists candidates diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 8a0a7caab..8847007bb 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -4,6 +4,7 @@ import Core.Env import Core.TT import Data.List +import Data.List1 import Data.Vect import Parser.Source @@ -474,6 +475,10 @@ export traverse : (a -> Core b) -> List a -> Core (List b) 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 |] + export traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b) traverseVect f [] = pure [] @@ -491,6 +496,12 @@ traverse_ f (x :: xs) = do f x traverse_ f xs +export +traverseList1_ : (a -> Core b) -> List1 a -> Core () +traverseList1_ f (x :: xs) = do + f x + traverse_ f xs + namespace PiInfo export traverse : (a -> Core b) -> PiInfo a -> Core (PiInfo b) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 65f142cda..2a9093794 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -20,6 +20,7 @@ import Idris.Version import IdrisPaths import Data.List +import Data.List1 import Data.So import Data.Strings import System @@ -47,15 +48,15 @@ updateEnv Nothing => setPrefix yprefix bpath <- coreLift $ getEnv "IDRIS2_PATH" the (Core ()) $ case bpath of - Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path)) + Just path => do traverseList1_ addExtraDir (map trim (split (==pathSeparator) path)) Nothing => pure () bdata <- coreLift $ getEnv "IDRIS2_DATA" the (Core ()) $ case bdata of - Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path)) + Just path => do traverseList1_ addDataDir (map trim (split (==pathSeparator) path)) Nothing => pure () blibs <- coreLift $ getEnv "IDRIS2_LIBS" the (Core ()) $ case blibs of - Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path)) + Just path => do traverseList1_ addLibDir (map trim (split (==pathSeparator) path)) Nothing => pure () cg <- coreLift $ getEnv "IDRIS2_CG" the (Core ()) $ case cg of diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 674b3d35e..c538e1466 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -15,6 +15,8 @@ import Core.Options import Core.TT import Core.Unify +import Data.List +import Data.List1 import Data.So import Data.Strings @@ -40,7 +42,6 @@ import TTImp.ProcessDecls import Utils.Hex -import Data.List import System import System.File @@ -196,7 +197,7 @@ process (CallsWho n) = do todoCmd "calls-who" pure $ NameList [] process (BrowseNamespace ns) - = replWrap $ Idris.REPL.process (Browse (reverse (split (=='.') ns))) + = replWrap $ Idris.REPL.process (Browse (List1.toList $ reverse (split (=='.') ns))) process (NormaliseTerm tm) = do todoCmd "normalise-term" pure $ Term tm diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 613893fa4..f1f94efbe 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -10,6 +10,7 @@ import Core.Options import Core.Unify import Data.List +import Data.List1 import Data.Maybe import Data.So import Data.StringMap @@ -52,8 +53,8 @@ record PkgDesc where sourceloc : Maybe String bugtracker : Maybe String depends : List String -- packages to add to search path - modules : List (List String, String) -- modules to install (namespace, filename) - mainmod : Maybe (List String, String) -- main file (i.e. file to load at REPL) + modules : List (List1 String, String) -- modules to install (namespace, filename) + mainmod : Maybe (List1 String, String) -- main file (i.e. file to load at REPL) executable : Maybe String -- name of executable options : Maybe (FC, String) sourcedir : Maybe String @@ -111,8 +112,8 @@ data DescField : Type where PSourceLoc : FC -> String -> DescField PBugTracker : FC -> String -> DescField PDepends : List String -> DescField - PModules : List (FC, List String) -> DescField - PMainMod : FC -> List String -> DescField + PModules : List (FC, List1 String) -> DescField + PMainMod : FC -> List1 String -> DescField PExec : String -> DescField POpts : FC -> String -> DescField PSourceDir : FC -> String -> DescField @@ -190,8 +191,8 @@ data ParsedMods : Type where data MainMod : Type where addField : {auto c : Ref Ctxt Defs} -> - {auto p : Ref ParsedMods (List (FC, List String))} -> - {auto m : Ref MainMod (Maybe (FC, List String))} -> + {auto p : Ref ParsedMods (List (FC, List1 String))} -> + {auto m : Ref MainMod (Maybe (FC, List1 String))} -> DescField -> PkgDesc -> Core PkgDesc addField (PVersion fc n) pkg = pure $ record { version = n } pkg addField (PAuthors fc a) pkg = pure $ record { authors = a } pkg @@ -233,10 +234,10 @@ addFields xs desc = do p <- newRef ParsedMods [] , mainmod = !(traverseOpt toSource mmod) } added where - toSource : (FC, List String) -> Core (List String, String) - toSource (loc, ns) = pure (ns, !(nsToSource loc ns)) - go : {auto p : Ref ParsedMods (List (FC, List String))} -> - {auto m : Ref MainMod (Maybe (FC, List String))} -> + toSource : (FC, List1 String) -> Core (List1 String, String) + toSource (loc, ns) = pure (ns, !(nsToSource loc (List1.toList ns))) + go : {auto p : Ref ParsedMods (List (FC, List1 String))} -> + {auto m : Ref MainMod (Maybe (FC, List1 String))} -> List DescField -> PkgDesc -> Core PkgDesc go [] dsc = pure dsc go (x :: xs) dsc = go xs !(addField x dsc) @@ -312,7 +313,7 @@ build pkg opts Just exec => do let Just (mainNS, mainFile) = mainmod pkg | Nothing => throw (GenericMsg emptyFC "No main module given") - let mainName = NS mainNS (UN "main") + let mainName = NS (List1.toList mainNS) (UN "main") compileMain mainName mainFile exec runScript (postbuild pkg) @@ -325,10 +326,9 @@ copyFile src dest writeToFile dest buf installFrom : {auto c : Ref Ctxt Defs} -> - String -> String -> String -> List String -> Core () -installFrom _ _ _ [] = pure () + String -> String -> String -> List1 String -> Core () installFrom pname builddir destdir ns@(m :: dns) - = do let ttcfile = joinPath (reverse ns) + = do let ttcfile = joinPath (List1.toList $ reverse ns) let ttcPath = builddir "ttc" ttcfile <.> "ttc" let destPath = destdir joinPath (reverse dns) let destFile = destdir ttcfile <.> "ttc" @@ -352,7 +352,7 @@ install pkg opts -- not used but might be in the future let build = build_dir (dirs (options defs)) runScript (preinstall pkg) let toInstall = maybe (map fst (modules pkg)) - (\m => fst m :: map fst (modules pkg)) + (\ m => fst m :: map fst (modules pkg)) (mainmod pkg) Just srcdir <- coreLift currentDir | Nothing => throw (InternalError "Can't get current directory") @@ -436,9 +436,7 @@ clean pkg opts -- `opts` is not used but might be in the future (\m => fst m :: map fst (modules pkg)) (mainmod pkg) let toClean : List (List String, String) - = mapMaybe (\ks => case ks of - [] => Nothing - (x :: xs) => Just (xs, x)) pkgmods + = map (\ (x :: xs) => (xs, x)) pkgmods Just srcdir <- coreLift currentDir | Nothing => throw (InternalError "Can't get current directory") let d = dirs (options defs) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 054be5cf0..b18d26673 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -9,6 +9,7 @@ import TTImp.TTImp import public Text.Parser import Data.List import Data.List.Views +import Data.List1 import Data.Maybe import Data.Strings @@ -1185,7 +1186,7 @@ fix <|> do keyword "infix"; pure Infix <|> do keyword "prefix"; pure Prefix -namespaceHead : Rule (List String) +namespaceHead : Rule (List1 String) namespaceHead = do keyword "namespace" commit @@ -1200,7 +1201,7 @@ namespaceDecl fname indents ns <- namespaceHead end <- location ds <- blockAfter col (topDecl fname) - pure (PNamespace (MkFC fname start end) ns (concat ds)) + pure (PNamespace (MkFC fname start end) (List1.toList ns) (concat ds)) transformDecl : FileName -> IndentInfo -> Rule PDecl transformDecl fname indents @@ -1614,7 +1615,7 @@ import_ fname indents namespacedIdent) end <- location atEnd indents - pure (MkImport (MkFC fname start end) reexp ns nsAs) + pure (MkImport (MkFC fname start end) reexp (List1.toList ns) (List1.toList nsAs)) export prog : FileName -> SourceEmptyRule Module @@ -1628,7 +1629,7 @@ prog fname imports <- block (import_ fname) ds <- block (topDecl fname) pure (MkModule (MkFC fname start end) - nspace imports doc (collectDefs (concat ds))) + (List1.toList nspace) imports doc (collectDefs (concat ds))) export progHdr : FileName -> SourceEmptyRule Module @@ -1641,7 +1642,7 @@ progHdr fname end <- location imports <- block (import_ fname) pure (MkModule (MkFC fname start end) - nspace imports doc []) + (List1.toList nspace) imports doc []) parseMode : Rule REPLEval parseMode @@ -1854,7 +1855,7 @@ moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse) symbol ":" runParseCmd parseCmd n <- moduleIdent - pure (command n) + pure (command (List1.toList n)) exprArgCmd : ParseCmd -> (PTerm -> REPLCmd) -> String -> CommandDefinition exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse) diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 97c0bba65..ad36f1461 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -11,6 +11,7 @@ import TTImp.Unelab import TTImp.Utils import Data.List +import Data.List1 import Data.Maybe import Data.StringMap @@ -380,17 +381,17 @@ mutual toPRecord (MkImpRecord fc n ps con fs) = do ps' <- traverse (\ (n, c, p, ty) => do ty' <- toPTerm startPrec ty - p' <- mapPiInfo p + p' <- mapPiInfo p pure (n, c, p', ty')) ps fs' <- traverse toPField fs pure (n, ps', Just con, fs') - where + where mapPiInfo : PiInfo RawImp -> Core (PiInfo PTerm) mapPiInfo Explicit = pure Explicit mapPiInfo Implicit = pure Implicit mapPiInfo AutoImplicit = pure AutoImplicit mapPiInfo (DefImplicit p) = pure $ DefImplicit !(toPTerm startPrec p) - + toPFnOpt : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> FnOpt -> Core PFnOpt diff --git a/src/Parser/Lexer/Package.idr b/src/Parser/Lexer/Package.idr index cc106ba66..1a063c73f 100644 --- a/src/Parser/Lexer/Package.idr +++ b/src/Parser/Lexer/Package.idr @@ -5,6 +5,7 @@ import public Text.Lexer import public Text.Parser import Data.List +import Data.List1 import Data.Strings import Data.String.Extra import Utils.String @@ -16,7 +17,7 @@ data Token = Comment String | EndOfInput | Equals - | DotSepIdent (List String) + | DotSepIdent (List1 String) | Separator | Space | StringLit String @@ -26,7 +27,7 @@ Show Token where show (Comment str) = "Comment: " ++ str show EndOfInput = "EndOfInput" show Equals = "Equals" - show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep dsid + show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (List1.toList dsid) show Separator = "Separator" show Space = "Space" show (StringLit s) = "StringLit: " ++ s @@ -48,7 +49,7 @@ rawTokens = , (stringLit, \s => StringLit (stripQuotes s)) ] where - splitNamespace : String -> List String + splitNamespace : String -> List1 String splitNamespace = Data.Strings.split (== '.') export diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 3e0995774..373030894 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -2,6 +2,7 @@ module Parser.Lexer.Source import public Parser.Lexer.Common +import Data.List1 import Data.List import Data.Strings import Data.String.Extra @@ -22,8 +23,8 @@ data Token -- Identifiers | HoleIdent String | Ident String - | DotSepIdent (List String) -- ident.ident - | DotIdent String -- .ident + | DotSepIdent (List1 String) -- ident.ident + | DotIdent String -- .ident | Symbol String -- Comments | Comment String @@ -45,7 +46,7 @@ Show Token where -- Identifiers show (HoleIdent x) = "hole identifier " ++ x show (Ident x) = "identifier " ++ x - show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (reverse xs) + show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (List1.toList $ reverse xs) show (DotIdent x) = "dot+identifier " ++ x show (Symbol x) = "symbol " ++ x -- Comments @@ -96,9 +97,9 @@ 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 = many (is '-') <+> choice {t = List} -- absorb all dashes + [ is '}' <+> toEndComment k -- closing delimiter + , many (isNot '\n') <+> toEndComment (S k) -- line comment ] blockComment : Lexer @@ -220,7 +221,7 @@ rawTokens = parseIdent x = if x `elem` keywords then Keyword x else Ident x parseNamespace : String -> Token - parseNamespace ns = case Data.List.reverse . split (== '.') $ ns of + parseNamespace ns = case List1.reverse . split (== '.') $ ns of [ident] => parseIdent ident ns => DotSepIdent ns diff --git a/src/Parser/Rule/Package.idr b/src/Parser/Rule/Package.idr index 7ff6dbabb..643d4b5f1 100644 --- a/src/Parser/Rule/Package.idr +++ b/src/Parser/Rule/Package.idr @@ -4,6 +4,7 @@ import public Parser.Lexer.Package import public Parser.Rule.Common import Data.List +import Data.List1 %default total @@ -46,14 +47,14 @@ stringLit = terminal "Expected string" _ => Nothing) export -namespacedIdent : Rule (List String) +namespacedIdent : Rule (List1 String) namespacedIdent = terminal "Expected namespaced identifier" (\x => case tok x of DotSepIdent nsid => Just $ reverse nsid _ => Nothing) export -moduleIdent : Rule (List String) +moduleIdent : Rule (List1 String) moduleIdent = terminal "Expected module identifier" (\x => case tok x of DotSepIdent m => Just $ reverse m diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 0c80af3bb..e17479ac4 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -5,6 +5,7 @@ import public Parser.Rule.Common import public Parser.Support import Core.TT +import Data.List1 import Data.Strings %default total @@ -142,21 +143,21 @@ identPart _ => Nothing) export -namespacedIdent : Rule (List String) +namespacedIdent : Rule (List1 String) namespacedIdent = terminal "Expected namespaced name" (\x => case tok x of DotSepIdent ns => Just ns - Ident i => Just $ [i] + Ident i => Just [i] _ => Nothing) export -moduleIdent : Rule (List String) +moduleIdent : Rule (List1 String) moduleIdent = terminal "Expected module identifier" (\x => case tok x of DotSepIdent ns => Just ns - Ident i => Just $ [i] + Ident i => Just [i] _ => Nothing) export @@ -185,8 +186,7 @@ name = opNonNS <|> do reserved : String -> Bool reserved n = n `elem` reservedNames - nameNS : List String -> SourceEmptyRule Name - nameNS [] = pure $ UN "IMPOSSIBLE" + nameNS : List1 String -> SourceEmptyRule Name nameNS [x] = if reserved x then fail $ "can't use reserved name " ++ x @@ -199,12 +199,12 @@ name = opNonNS <|> do opNonNS : Rule Name opNonNS = symbol "(" *> operator <* symbol ")" - opNS : List String -> Rule Name + opNS : List1 String -> Rule Name opNS ns = do symbol ".(" n <- operator symbol ")" - pure (NS ns n) + pure (NS (toList ns) n) export IndentInfo : Type diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 6a89e4f95..44ea8c7c1 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -10,6 +10,7 @@ import TTImp.TTImp import public Text.Parser import Data.List import Data.List.Views +import Data.List1 import Data.Strings topDecl : FileName -> IndentInfo -> Rule ImpDecl @@ -645,7 +646,7 @@ namespaceDecl = do keyword "namespace" commit ns <- namespacedIdent - pure ns + pure (List1.toList ns) directive : FileName -> IndentInfo -> Rule ImpDecl directive fname indents diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 6c4a49fdc..139a9a959 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -995,4 +995,3 @@ mutual 8 => do n <- fromBuf b pure (ILog n) _ => corrupt "ImpDecl" - diff --git a/src/Utils/Binary.idr b/src/Utils/Binary.idr index 9c2d10741..c137b5330 100644 --- a/src/Utils/Binary.idr +++ b/src/Utils/Binary.idr @@ -7,6 +7,7 @@ import Data.Buffer import public Data.IOArray import Data.List import Data.List.Elem +import Data.List1 import Data.Nat import Data.Vect @@ -329,12 +330,12 @@ TTC a => TTC (List a) where traverse_ (toBuf b) xs where ||| Tail-recursive length as buffer sizes can get large - ||| + ||| ||| Once we port to Idris2, can use Data.List.TailRec.length instead length_aux : List a -> Int -> Int length_aux [] len = len length_aux (_::xs) len = length_aux xs (1 + len) - + TailRec_length : List a -> Int TailRec_length xs = length_aux xs 0 @@ -348,6 +349,16 @@ TTC a => TTC (List a) where = do val <- fromBuf b readElems (val :: xs) k +export +TTC a => TTC (List1 a) where + toBuf b xs = toBuf b (List1.toList xs) + + fromBuf b = do + xs <- fromBuf b + case fromList xs of + Nothing => corrupt "List1" + Just xs => pure xs + export {n : Nat} -> TTC a => TTC (Vect n a) where toBuf b xs = writeAll xs diff --git a/tests/Main.idr b/tests/Main.idr index 7d49eb72e..0c5fb049b 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -2,6 +2,7 @@ module Main import Data.Maybe import Data.List +import Data.List1 import Data.Strings import System @@ -271,7 +272,7 @@ firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs pathLookup : List String -> IO (Maybe String) pathLookup names = do path <- getEnv "PATH" - let pathList = split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path + let pathList = List1.toList $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path let candidates = [p ++ "/" ++ x | p <- pathList, x <- names] firstExists candidates @@ -317,7 +318,7 @@ main | _ => do print args putStrLn usage let filteredNonCGTests = - filterTests opts $ concat + filterTests opts $ concat $ the (List (List String)) [ testPaths "ttimp" ttimpTests , testPaths "idris2" idrisTests , testPaths "typedd-book" typeddTests diff --git a/tests/chez/chez020/Popen.idr b/tests/chez/chez020/Popen.idr index 5dcbddf9d..a8e2632e0 100644 --- a/tests/chez/chez020/Popen.idr +++ b/tests/chez/chez020/Popen.idr @@ -1,6 +1,7 @@ import System import System.File import System.Info +import Data.List1 import Data.Strings windowsPath : String -> String diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 0c82655b7..a45efe4f8 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -1,6 +1,6 @@ 1/1: Building refprims (refprims.idr) LOG 0: Name: Prelude.Types.List.++ -LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.Types.List a) (%pi RigW Explicit (Just {arg:2578}) (Prelude.Types.List a) (Prelude.Types.List a)))) +LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.Types.List a) (%pi Rig1 Explicit (Just ys) (Prelude.Types.List a) (Prelude.Types.List a)))) LOG 0: Name: Prelude.Types.Strings.++ LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String)) LOG 0: Resolved name: Prelude.Types.Nat