From 3df1f9c476802f8cd2141271b4d40a179faa0349 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Mon, 28 Sep 2020 13:15:22 +0100 Subject: [PATCH] [ fix #63 ] interleaving let binders and local declarations (#691) --- idris2api.ipkg | 1 + libs/base/Data/List.idr | 9 +- .../contrib/Data/String/Parser/Expression.idr | 2 +- src/Core/FC.idr | 33 +++++- src/Idris/Parser.idr | 108 +++++------------- src/Idris/Parser/Let.idr | 90 +++++++++++++++ src/Parser/Lexer/Source.idr | 2 +- src/Parser/Rule/Source.idr | 7 +- src/TTImp/Parser.idr | 6 +- src/TTImp/Utils.idr | 6 +- src/Text/Bounded.idr | 8 ++ src/Text/Parser/Core.idr | 41 +++++-- src/Utils/String.idr | 5 + tests/Main.idr | 2 +- tests/idris2/basic047/InterleavingLets.idr | 62 ++++++++++ tests/idris2/basic047/expected | 3 + tests/idris2/basic047/input | 2 + tests/idris2/basic047/run | 3 + tests/idris2/coverage006/foobar.idr | 4 +- tests/idris2/perror003/PError2.idr | 8 ++ tests/idris2/perror003/expected | 7 +- tests/idris2/perror003/run | 1 + tests/idris2/reflection001/expected | 4 +- 23 files changed, 302 insertions(+), 112 deletions(-) create mode 100644 src/Idris/Parser/Let.idr create mode 100644 tests/idris2/basic047/InterleavingLets.idr create mode 100644 tests/idris2/basic047/expected create mode 100644 tests/idris2/basic047/input create mode 100644 tests/idris2/basic047/run create mode 100644 tests/idris2/perror003/PError2.idr diff --git a/idris2api.ipkg b/idris2api.ipkg index 03490dad4..840b84955 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -81,6 +81,7 @@ modules = Idris.ModTree, Idris.Package, Idris.Parser, + Idris.Parser.Let, Idris.Pretty, Idris.ProcessIdr, Idris.REPL, diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index e8c77e801..484e0b152 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -174,13 +174,20 @@ public export union : Eq a => List a -> List a -> List a union = unionBy (==) +public export +spanBy : (a -> Maybe b) -> List a -> (List b, List a) +spanBy p [] = ([], []) +spanBy p (x :: xs) = case p x of + Nothing => ([], x :: xs) + Just y => let (ys, zs) = spanBy p xs in (y :: ys, zs) + public export span : (a -> Bool) -> List a -> (List a, List a) span p [] = ([], []) span p (x::xs) = if p x then let (ys, zs) = span p xs in - (x::ys, zs) + (x::ys, zs) else ([], x::xs) diff --git a/libs/contrib/Data/String/Parser/Expression.idr b/libs/contrib/Data/String/Parser/Expression.idr index 18a80224b..51f742409 100644 --- a/libs/contrib/Data/String/Parser/Expression.idr +++ b/libs/contrib/Data/String/Parser/Expression.idr @@ -116,6 +116,6 @@ buildExpressionParser a operators simpleExpr = rassocP = mkRassocP amLeft amNon rassocOp termP lassocP = mkLassocP amRight amNon lassocOp termP nassocP = mkNassocP amRight amLeft amNon nassocOp termP - in + in do x <- termP rassocP x <|> lassocP x <|> nassocP x <|> pure x "operator" diff --git a/src/Core/FC.idr b/src/Core/FC.idr index 46d831e92..e96dffd7e 100644 --- a/src/Core/FC.idr +++ b/src/Core/FC.idr @@ -1,9 +1,13 @@ module Core.FC +import Text.Bounded import Text.PrettyPrint.Prettyprinter %default total +------------------------------------------------------------------------ +-- Types + public export FilePos : Type FilePos = (Int, Int) @@ -20,11 +24,8 @@ public export data FC = MkFC FileName FilePos FilePos | EmptyFC -export -Eq FC where - (==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e' - (==) EmptyFC EmptyFC = True - (==) _ _ = False +------------------------------------------------------------------------ +-- Projections export file : FC -> FileName @@ -41,6 +42,16 @@ endPos : FC -> FilePos endPos (MkFC _ _ e) = e endPos EmptyFC = (0, 0) +------------------------------------------------------------------------ +-- Smart constructor + +export +boundToFC : FileName -> WithBounds t -> FC +boundToFC fname b = MkFC fname (start b) (end b) + +------------------------------------------------------------------------ +-- Predicates + -- Return whether a given file position is within the file context (assuming we're -- in the right file) export @@ -57,6 +68,9 @@ onLine x (MkFC _ start end) = x >= fst start && x <= fst end onLine _ _ = False +------------------------------------------------------------------------ +-- Constant values + export emptyFC : FC emptyFC = EmptyFC @@ -67,6 +81,15 @@ toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0) %name FC fc +------------------------------------------------------------------------ +-- Instances + +export +Eq FC where + (==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e' + (==) EmptyFC EmptyFC = True + (==) _ _ = False + export Show FC where show loc = file loc ++ ":" ++ diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 1ada9fd82..67a132405 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -7,11 +7,15 @@ import Parser.Lexer.Source import TTImp.TTImp import public Text.Parser +import Data.Either import Data.List import Data.List.Views import Data.List1 import Data.Maybe import Data.Strings +import Utils.String + +import Idris.Parser.Let %default covering @@ -48,9 +52,6 @@ plhs = MkParseOpts False False %hide Prelude.pure %hide Core.Core.pure -boundToFC : String -> WithBounds t -> FC -boundToFC fname b = MkFC fname (start b) (end b) - atom : FileName -> Rule PTerm atom fname = do x <- bounds $ exactIdent "Type" @@ -533,63 +534,31 @@ mutual = PLam (boundToFC fname pat) rig Explicit pat.val ty (bindAll rest scope) - letBinder : FileName -> IndentInfo -> - Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) - letBinder fname indents - = do b <- bounds (do s <- bounds (MkPair <$> multiplicity <*> expr plhs fname indents) - (rigc, pat) <- pure s.val - ty <- option (PImplicit (boundToFC fname s)) - (do symbol ":" - typeExpr (pnoeq pdef) fname indents) - symbol "=" - val <- expr pnowith fname indents - alts <- block (patAlt fname) - rig <- getMult rigc - pure (rig, pat, ty, val, alts)) - (rig, pat, ty, val, alts) <- the (SourceEmptyRule (RigCount, PTerm, PTerm, PTerm, List PClause)) (pure b.val) - pure (start b, end b, rig, pat, ty, val, alts) + letBlock : FileName -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl)) + letBlock fname indents = bounds (letBinder <||> letDecl) where - buildLets : FileName -> - List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) -> - PTerm -> PTerm - buildLets fname [] sc = sc - buildLets fname ((start, end, rig, pat, ty, val, alts) :: rest) sc - = let fc = MkFC fname start end in - PLet fc rig pat ty val - (buildLets fname rest sc) alts + letBinder : Rule LetBinder + letBinder = do s <- bounds (MkPair <$> multiplicity <*> expr plhs fname indents) + (rigc, pat) <- pure s.val + ty <- option (PImplicit (boundToFC fname s)) + (symbol ":" *> typeExpr (pnoeq pdef) fname indents) + (symbol "=" <|> symbol ":=") + val <- expr pnowith fname indents + alts <- block (patAlt fname) + rig <- getMult rigc + pure (MkLetBinder rig pat ty val alts) - buildDoLets : FileName -> - List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) -> - List PDo - buildDoLets fname [] = [] - buildDoLets fname ((start, end, rig, PRef fc' (UN n), ty, val, []) :: rest) - = let fc = MkFC fname start end in - if lowerFirst n - then DoLet fc (UN n) rig ty val :: buildDoLets fname rest - else DoLetPat fc (PRef fc' (UN n)) ty val [] - :: buildDoLets fname rest - buildDoLets fname ((start, end, rig, pat, ty, val, alts) :: rest) - = let fc = MkFC fname start end in - DoLetPat fc pat ty val alts :: buildDoLets fname rest + letDecl : Rule LetDecl + letDecl = collectDefs . concat <$> nonEmptyBlock (try . topDecl fname) let_ : FileName -> IndentInfo -> Rule PTerm let_ fname indents - = do b <- bounds (do keyword "let" - res <- nonEmptyBlock (letBinder fname) - commitKeyword indents "in" - scope <- typeExpr pdef fname indents - pure (res, scope)) - (res, scope) <- pure b.val - pure (buildLets fname res scope) - - <|> do b <- bounds (do keyword "let" - commit - ds <- nonEmptyBlock (topDecl fname) - commitKeyword indents "in" - scope <- typeExpr pdef fname indents - pure (ds, scope)) - (ds, scope) <- pure b.val - pure (PLocal (boundToFC fname b) (collectDefs (concat ds)) scope) + = do keyword "let" + commit + res <- nonEmptyBlock (letBlock fname) + commitKeyword indents "in" + scope <- typeExpr pdef fname indents + pure (mkLets fname res scope) case_ : FileName -> IndentInfo -> Rule PTerm case_ fname indents @@ -695,10 +664,6 @@ mutual ns (concat actions.val)) _ => fail "Not a namespaced 'do'" - lowerFirst : String -> Bool - lowerFirst "" = False - lowerFirst str = assert_total (isLower (prim__strHead str)) - validPatternVar : Name -> SourceEmptyRule () validPatternVar (UN n) = if lowerFirst n then pure () @@ -718,12 +683,10 @@ mutual (n, val) <- pure b.val pure [DoBind (boundToFC fname b) n val] <|> do keyword "let" - res <- block (letBinder fname) + commit + res <- nonEmptyBlock (letBlock fname) atEnd indents - pure (buildDoLets fname res) - <|> do b <- bounds (keyword "let" *> block (topDecl fname)) - atEnd indents - pure [DoLetLocal (boundToFC fname b) (concat b.val)] + pure (mkDoLets fname res) <|> do b <- bounds (keyword "rewrite" *> expr pdef fname indents) atEnd indents pure [DoRewrite (boundToFC fname b) b.val] @@ -831,7 +794,7 @@ mutual symbol "(" wval <- bracketedExpr fname flags indents ws <- nonEmptyBlock (clause (S withArgs) fname) - pure (flags, wval, ws)) + pure (flags, wval, forget ws)) (flags, wval, ws) <- pure b.val pure (MkWithClause (boundToFC fname (mergeBounds start b)) lhs wval flags.val ws) <|> do end <- bounds (keyword "impossible") @@ -1177,10 +1140,6 @@ getVisibility (Just vis) (Left x :: xs) = fatalError "Multiple visibility modifiers" getVisibility v (_ :: xs) = getVisibility v xs -getRight : Either a b -> Maybe b -getRight (Left _) = Nothing -getRight (Right v) = Just v - constraints : FileName -> IndentInfo -> SourceEmptyRule (List (Maybe Name, PTerm)) constraints fname indents = do tm <- appExpr pdef fname indents @@ -1427,16 +1386,9 @@ topDecl fname indents -- collectDefs : List PDecl -> List PDecl collectDefs [] = [] collectDefs (PDef annot cs :: ds) - = let (cs', rest) = spanMap isClause ds in - PDef annot (cs ++ cs') :: assert_total (collectDefs rest) + = let (cs', rest) = spanBy isClause ds in + PDef annot (cs ++ concat cs') :: assert_total (collectDefs rest) where - spanMap : (a -> Maybe (List b)) -> List a -> (List b, List a) - spanMap f [] = ([], []) - spanMap f (x :: xs) = case f x of - Nothing => ([], x :: xs) - Just y => case spanMap f xs of - (ys, zs) => (y ++ ys, zs) - isClause : PDecl -> Maybe (List PClause) isClause (PDef annot cs) = Just cs diff --git a/src/Idris/Parser/Let.idr b/src/Idris/Parser/Let.idr new file mode 100644 index 000000000..3b0a5c1a1 --- /dev/null +++ b/src/Idris/Parser/Let.idr @@ -0,0 +1,90 @@ +module Idris.Parser.Let + +import Idris.Syntax +import Text.Bounded + +import Data.Either +import Data.List1 + +import Utils.String + +%default total + +------------------------------------------------------------------------ +-- Types + +-- `let ... in ...` is used for two different notions: +-- * pattern-matching let binders to locally take an expression apart +-- * Local definitions that can be recursive + +public export +record LetBinder where + constructor MkLetBinder + letUsage : RigCount + letPattern : PTerm + letBoundType : PTerm + letBoundTerm : PTerm + letUnhappy : List PClause + +public export +LetDecl : Type +LetDecl = List PDecl + +------------------------------------------------------------------------ +-- Let-binding functions + +letFactory : (List (WithBounds LetBinder) -> a -> a) -> + (WithBounds LetDecl -> a -> a) -> + List1 (WithBounds (Either LetBinder LetDecl)) -> + a -> a +letFactory letBind letDeclare blocks scope = foldr mkLet scope groups where + + LetBlock : Type + LetBlock = Either (List1 (WithBounds LetBinder)) (List1 (WithBounds LetDecl)) + + groups : List LetBlock + groups = compress (forget $ map (\ b => bimap (<$ b) (<$ b) b.val) blocks) + + mkLet : LetBlock -> a -> a + mkLet (Left letBinds) = letBind (forget letBinds) + mkLet (Right letDecls) = + let bounds = mergeBounds (head letDecls) (last letDecls) + in letDeclare (concatMap val letDecls <$ bounds) + +export +mkLets : FileName -> + List1 (WithBounds (Either LetBinder LetDecl)) -> + PTerm -> PTerm +mkLets fname = letFactory buildLets + (\ decls, scope => PLocal (boundToFC fname decls) decls.val scope) + + where + + buildLets : List (WithBounds LetBinder) -> PTerm -> PTerm + buildLets [] sc = sc + buildLets (b :: rest) sc + = let (MkLetBinder rig pat ty val alts) = b.val + fc = boundToFC fname b + in PLet fc rig pat ty val (buildLets rest sc) alts + +export +mkDoLets : FileName -> + List1 (WithBounds (Either LetBinder LetDecl)) -> + List PDo +mkDoLets fname lets = letFactory + (\ binds, rest => buildDoLets binds ++ rest) + (\ decls, rest => DoLetLocal (boundToFC fname decls) decls.val :: rest) + lets + [] + + where + + buildDoLets : List (WithBounds LetBinder) -> List PDo + buildDoLets [] = [] + buildDoLets (b :: rest) = let fc = boundToFC fname b in case b.val of + (MkLetBinder rig (PRef fc' (UN n)) ty val []) => + (if lowerFirst n + then DoLet fc (UN n) rig ty val + else DoLetPat fc (PRef fc' (UN n)) ty val [] + ) :: buildDoLets rest + (MkLetBinder rig pat ty val alts) => DoLetPat fc pat ty val alts :: buildDoLets rest diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 4213de9a4..3ef80787c 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -202,7 +202,7 @@ export reservedSymbols : List String reservedSymbols = symbols ++ - ["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!", + ["%", "\\", ":", "=", ":=", "|", "|||", "<-", "->", "=>", "?", "!", "&", "**", "..", "~"] fromBinLit : String -> Integer diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 905622ef6..852681419 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 @@ -431,15 +432,15 @@ blockWithOptHeaderAfter {ty} mincol header item pure (Nothing, ps) export -nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty) +nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List1 ty) nonEmptyBlock item = do symbol "{" commit res <- blockEntry AnyIndent item ps <- blockEntries (snd res) item symbol "}" - pure (fst res :: ps) + pure (fst res ::: ps) <|> do col <- column res <- blockEntry (AtPos col) item ps <- blockEntries (snd res) item - pure (fst res :: ps) + pure (fst res ::: ps) diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 8aac28d11..03365ebef 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -504,7 +504,7 @@ mutual ws <- nonEmptyBlock (clause (S withArgs) fname) end <- location let fc = MkFC fname start end - pure (!(getFn lhs), WithClause fc lhs wval [] (map snd ws)) + pure (!(getFn lhs), WithClause fc lhs wval [] (forget $ map snd ws)) <|> do keyword "impossible" atEnd indents @@ -683,7 +683,7 @@ topDecl fname indents ns <- namespaceDecl ds <- assert_total (nonEmptyBlock (topDecl fname)) end <- location - pure (INamespace (MkFC fname start end) ns ds) + pure (INamespace (MkFC fname start end) ns (forget ds)) <|> do start <- location visOpts <- many visOpt vis <- getVisibility Nothing visOpts @@ -723,7 +723,7 @@ export prog : FileName -> Rule (List ImpDecl) prog fname = do ds <- nonEmptyBlock (topDecl fname) - pure (collectDefs ds) + pure (collectDefs $ forget ds) -- TTImp REPL commands export diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index d8dc6da22..4425e246c 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -7,11 +7,9 @@ import TTImp.TTImp import Data.List import Data.Strings -%default covering +import Utils.String -lowerFirst : String -> Bool -lowerFirst "" = False -lowerFirst str = assert_total (isLower (prim__strHead str)) +%default covering export getUnique : List String -> String -> String diff --git a/src/Text/Bounded.idr b/src/Text/Bounded.idr index 79ff3d587..635bf86d3 100644 --- a/src/Text/Bounded.idr +++ b/src/Text/Bounded.idr @@ -34,6 +34,14 @@ export Functor WithBounds where map f (MkBounded val ir sl sc el ec) = MkBounded (f val) ir sl sc el ec +export +Foldable WithBounds where + foldr c n b = c b.val n + +export +Traversable WithBounds where + traverse f (MkBounded v a b c d e) = (\ v => MkBounded v a b c d e) <$> f v + export irrelevantBounds : ty -> WithBounds ty irrelevantBounds x = MkBounded x True (-1) (-1) (-1) (-1) diff --git a/src/Text/Parser/Core.idr b/src/Text/Parser/Core.idr index 69c65de37..ea24424a5 100644 --- a/src/Text/Parser/Core.idr +++ b/src/Text/Parser/Core.idr @@ -23,6 +23,8 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where EOF : Grammar tok False () Fail : Bool -> String -> Grammar tok c ty + Try : Grammar tok c ty -> Grammar tok c ty + Commit : Grammar tok False () MustWork : Grammar tok c a -> Grammar tok c a @@ -67,21 +69,13 @@ join : {c1,c2 : Bool} -> join {c1 = False} p = SeqEmpty p id join {c1 = True} p = SeqEat p id -||| Give two alternative grammars. If both consume, the combination is -||| guaranteed to consume. -export %inline -(<|>) : {c1,c2 : Bool} -> - Grammar tok c1 ty -> - Lazy (Grammar tok c2 ty) -> - Grammar tok (c1 && c2) ty -(<|>) = Alt - ||| Allows the result of a grammar to be mapped to a different value. export {c : _} -> Functor (Grammar tok c) where map f (Empty val) = Empty (f val) map f (Fail fatal msg) = Fail fatal msg + map f (Try g) = Try (map f g) map f (MustWork g) = MustWork (map f g) map f (Terminal msg g) = Terminal msg (map f . g) map f (Alt x y) = Alt (map f x) (map f y) @@ -94,6 +88,25 @@ Functor (Grammar tok c) where -- so a sequence must be used. map {c = False} f p = SeqEmpty p (Empty . f) +||| Give two alternative grammars. If both consume, the combination is +||| guaranteed to consume. +export %inline +(<|>) : {c1,c2 : Bool} -> + Grammar tok c1 ty -> + Lazy (Grammar tok c2 ty) -> + Grammar tok (c1 && c2) ty +(<|>) = Alt + +infixr 2 <||> +||| Take the tagged disjunction of two grammars. If both consume, the +||| combination is guaranteed to consume. +export +(<||>) : {c1,c2 : Bool} -> + Grammar tok c1 a -> + Lazy (Grammar tok c2 b) -> + Grammar tok (c1 && c2) (Either a b) +(<||>) p q = (Left <$> p) <|> (Right <$> q) + ||| Sequence a grammar with value type `a -> b` and a grammar ||| with value type `a`. If both succeed, apply the function ||| from the first grammar to the value from the second grammar. @@ -132,6 +145,7 @@ mapToken f (Terminal msg g) = Terminal msg (g . map f) mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . map f)) (Empty . f) mapToken f EOF = EOF mapToken f (Fail fatal msg) = Fail fatal msg +mapToken f (Try g) = Try (mapToken f g) mapToken f (MustWork g) = MustWork (mapToken f g) mapToken f Commit = Commit mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x)) @@ -169,6 +183,11 @@ export %inline fatalError : String -> Grammar tok c ty fatalError = Fail True +||| Catch a fatal error +export %inline +try : Grammar tok c ty -> Grammar tok c ty +try = Try + ||| Succeed if the input is empty export %inline eof : Grammar tok False () @@ -202,6 +221,10 @@ mutual ParseResult tok ty doParse com (Empty val) xs = Res com (irrelevantBounds val) xs doParse com (Fail fatal str) xs = Failure com fatal str xs + doParse com (Try g) xs = case doParse com g xs of + -- recover from fatal match but still propagate the 'commit' + Failure com _ msg ts => Failure com False msg ts + res => res doParse com Commit xs = Res True (irrelevantBounds ()) xs doParse com (MustWork g) xs = case assert_total (doParse com g xs) of diff --git a/src/Utils/String.idr b/src/Utils/String.idr index 8403afb8f..b780ca43c 100644 --- a/src/Utils/String.idr +++ b/src/Utils/String.idr @@ -11,3 +11,8 @@ dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs] export stripQuotes : (str : String) -> String stripQuotes str = substr 1 (length str `minus` 2) str + +export +lowerFirst : String -> Bool +lowerFirst "" = False +lowerFirst str = assert_total (isLower (prim__strHead str)) diff --git a/tests/Main.idr b/tests/Main.idr index 92c8a4e7a..a51d42fb0 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -42,7 +42,7 @@ idrisTests "basic031", "basic032", "basic033", "basic034", "basic035", "basic036", "basic037", "basic038", "basic039", "basic040", "basic041", "basic042", "basic043", "basic044", "basic045", - "basic046", + "basic046", "basic047", -- Coverage checking "coverage001", "coverage002", "coverage003", "coverage004", "coverage005", "coverage006", "coverage007", "coverage008", diff --git a/tests/idris2/basic047/InterleavingLets.idr b/tests/idris2/basic047/InterleavingLets.idr new file mode 100644 index 000000000..39a8f79e0 --- /dev/null +++ b/tests/idris2/basic047/InterleavingLets.idr @@ -0,0 +1,62 @@ +data Tag = MkTag + +data Elem : a -> List a ->Type where + Z : Elem a (a :: as) + S : Elem a as -> Elem a (b :: as) + +toNat : Elem as a -> Nat +toNat Z = 0 +toNat (S n) = 1 + toNat n + +Show (Elem as a) where + show = show . toNat + +data Subset : List a -> List a -> Type where + Nil : Subset [] bs + (::) : Elem a bs -> Subset as bs -> Subset (a :: as) bs + +toList : Subset as bs -> List Nat +toList [] = [] +toList (n :: ns) = toNat n :: toList ns + +Show (Subset as bs) where + show = show . toList + +search : {auto prf : a} -> a +search = prf + +test : String +test = + let x : Tag := MkTag + y : Tag := MkTag + + as : List Tag + as = [y,x] + + bs : List Tag + bs = [x,y,y] + + prf : Subset as bs + prf = search + + prf' : Subset as bs := search + + eq : prf === [S (S Z), Z] := Refl + +-- eq' : prf' === [S (S Z), Z] := Refl +-- ^ does not work because prf' is opaque + + in show prf + + +reverse : List a -> List a +reverse xs = + let revOnto : List a -> List a -> List a + revOnto acc [] = acc + revOnto acc (x :: xs) = revOnto (x :: acc) xs + + rev := revOnto [] + + result := rev xs + + in result diff --git a/tests/idris2/basic047/expected b/tests/idris2/basic047/expected new file mode 100644 index 000000000..5854b8046 --- /dev/null +++ b/tests/idris2/basic047/expected @@ -0,0 +1,3 @@ +1/1: Building InterleavingLets (InterleavingLets.idr) +Main> "[2, 0]" +Main> Bye for now! diff --git a/tests/idris2/basic047/input b/tests/idris2/basic047/input new file mode 100644 index 000000000..131b8c414 --- /dev/null +++ b/tests/idris2/basic047/input @@ -0,0 +1,2 @@ +test +:q diff --git a/tests/idris2/basic047/run b/tests/idris2/basic047/run new file mode 100644 index 000000000..218b9daee --- /dev/null +++ b/tests/idris2/basic047/run @@ -0,0 +1,3 @@ +$1 --no-banner --no-color --console-width 0 InterleavingLets.idr < input + +rm -rf build \ No newline at end of file diff --git a/tests/idris2/coverage006/foobar.idr b/tests/idris2/coverage006/foobar.idr index 324dcdc2b..2e51c1b79 100644 --- a/tests/idris2/coverage006/foobar.idr +++ b/tests/idris2/coverage006/foobar.idr @@ -1,6 +1,6 @@ foo : (pf : Nat -> Either (S Z = Z) (Z = S Z)) -> Z = S Z -foo pf = - let baz : Z = S Z +foo pf = + let baz : Z === S Z baz with (pf 0) baz | (Left Refl) impossible baz | (Right pf') = pf' diff --git a/tests/idris2/perror003/PError2.idr b/tests/idris2/perror003/PError2.idr new file mode 100644 index 000000000..cea07347b --- /dev/null +++ b/tests/idris2/perror003/PError2.idr @@ -0,0 +1,8 @@ +foo : Int -> Int +foo x = x + +bar : Int -> Int +bar x = let y := (42 in y + x + +baz : Int -> Int +baz x = x diff --git a/tests/idris2/perror003/expected b/tests/idris2/perror003/expected index 3da3c2f25..df87875cf 100644 --- a/tests/idris2/perror003/expected +++ b/tests/idris2/perror003/expected @@ -1,3 +1,6 @@ 1/1: Building PError (PError.idr) -Error: Parse error at line 5:17: -Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, identifier Int, symbol ->]) +Error: Parse error at line 5:9: +Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier y, symbol =, symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz]) +1/1: Building PError2 (PError2.idr) +Error: Parse error at line 5:9: +Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier y, symbol :=, symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz]) diff --git a/tests/idris2/perror003/run b/tests/idris2/perror003/run index 65133be9c..d9e626dc9 100755 --- a/tests/idris2/perror003/run +++ b/tests/idris2/perror003/run @@ -1,3 +1,4 @@ $1 --no-color --console-width 0 --check PError.idr +$1 --no-color --console-width 0 --check PError2.idr rm -rf build diff --git a/tests/idris2/reflection001/expected b/tests/idris2/reflection001/expected index e313f4aef..d6aa04430 100644 --- a/tests/idris2/reflection001/expected +++ b/tests/idris2/reflection001/expected @@ -23,7 +23,7 @@ quote.idr:37:1--37:21 Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IApp (MkFC "quote.idr" (6, 13) (6, 14)) (IVar (MkFC "quote.idr" (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC "quote.idr" (6, 18) (6, 19)) (IVar (MkFC "quote.idr" (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 18) (6, 19)) (BI 4))) Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False")) -Main> ILocal (MkFC "quote.idr" (10, 8) (12, 22)) [IClaim (MkFC "quote.idr" (10, 12) (11, 15)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994))))) -Main> ILocal (MkFC "quote.idr" (16, 8) (18, 43)) [IClaim (MkFC "quote.idr" (16, 12) (17, 15)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994))) +Main> ILocal (MkFC "quote.idr" (10, 12) (11, 32)) [IClaim (MkFC "quote.idr" (10, 12) (11, 15)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994))))) +Main> ILocal (MkFC "quote.idr" (16, 12) (17, 32)) [IClaim (MkFC "quote.idr" (16, 12) (17, 15)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994))) Main> [UN "names", NS (MkNS ["Prelude"]) (UN "+")] Main> Bye for now!