mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
Implementations and errors
- Added initial implementations for terms and values - Error messages converted to pretty printer - Colorization for error messages - Color and console width option both as command line and repl command
This commit is contained in:
Giuseppe Lomurno
G. Allais
parent
df4f990b3c
commit
5e9837828a
@ -7,6 +7,8 @@ import Data.List
|
||||
import Data.List1
|
||||
import Data.Vect
|
||||
import Parser.Source
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
|
||||
import public Data.IORef
|
||||
import System
|
||||
@ -44,6 +46,15 @@ Show DotReason where
|
||||
show UserDotted = "User dotted"
|
||||
show UnknownDot = "Unknown reason"
|
||||
|
||||
export
|
||||
Pretty DotReason where
|
||||
pretty NonLinearVar = reflow "Non linear pattern variable"
|
||||
pretty VarApplied = reflow "Variable applied to arguments"
|
||||
pretty NotConstructor = reflow "Not a constructor application or primitive"
|
||||
pretty ErasedArg = reflow "Erased argument"
|
||||
pretty UserDotted = reflow "User dotted"
|
||||
pretty UnknownDot = reflow "Unknown reason"
|
||||
|
||||
-- All possible errors, carrying a location
|
||||
public export
|
||||
data Error : Type where
|
||||
|
||||
@ -8,7 +8,8 @@ import Data.List
|
||||
import Data.NameMap
|
||||
import Data.Vect
|
||||
import Decidable.Equality
|
||||
import Text.PrettyPrint.PrettyPrinter
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
|
||||
import public Algebra
|
||||
|
||||
@ -101,8 +102,8 @@ Pretty Constant where
|
||||
pretty (B16 x) = pretty x
|
||||
pretty (B32 x) = pretty x
|
||||
pretty (B64 x) = pretty x
|
||||
pretty (Str x) = pretty x
|
||||
pretty (Ch x) = pretty x
|
||||
pretty (Str x) = dquotes (pretty x)
|
||||
pretty (Ch x) = squotes (pretty x)
|
||||
pretty (Db x) = pretty x
|
||||
pretty WorldVal = pretty "%MkWorld"
|
||||
pretty IntType = pretty "Int"
|
||||
@ -557,6 +558,12 @@ Show Visibility where
|
||||
show Export = "export"
|
||||
show Public = "public export"
|
||||
|
||||
export
|
||||
Pretty Visibility where
|
||||
pretty Private = pretty "private"
|
||||
pretty Export = pretty "export"
|
||||
pretty Public = pretty "public" <+> pretty "export"
|
||||
|
||||
export
|
||||
Eq Visibility where
|
||||
Private == Private = True
|
||||
@ -610,6 +617,16 @@ Show PartialReason where
|
||||
show (RecPath ns)
|
||||
= "possibly not terminating due to recursive path " ++ showSep " -> " (map show ns)
|
||||
|
||||
export
|
||||
Pretty PartialReason where
|
||||
pretty NotStrictlyPositive = reflow "not strictly positive"
|
||||
pretty (BadCall [n])
|
||||
= reflow "possibly not terminating due to call to" <++> pretty n
|
||||
pretty (BadCall ns)
|
||||
= reflow "possibly not terminating due to calls to" <++> concatWith (surround (comma <+> space)) (pretty <$> ns)
|
||||
pretty (RecPath ns)
|
||||
= reflow "possibly not terminating due to recursive path" <++> concatWith (surround (pretty " -> ")) (pretty <$> ns)
|
||||
|
||||
public export
|
||||
data Terminating
|
||||
= Unchecked
|
||||
@ -622,6 +639,12 @@ Show Terminating where
|
||||
show IsTerminating = "terminating"
|
||||
show (NotTerminating p) = show p
|
||||
|
||||
export
|
||||
Pretty Terminating where
|
||||
pretty Unchecked = reflow "not yet checked"
|
||||
pretty IsTerminating = pretty "terminating"
|
||||
pretty (NotTerminating p) = pretty p
|
||||
|
||||
public export
|
||||
data Covering
|
||||
= IsCovering
|
||||
@ -637,6 +660,15 @@ Show Covering where
|
||||
show (NonCoveringCall cs)
|
||||
= "not covering due to calls to functions " ++ showSep ", " (map show cs)
|
||||
|
||||
export
|
||||
Pretty Covering where
|
||||
pretty IsCovering = pretty "covering"
|
||||
pretty (MissingCases c) = reflow "not covering all cases"
|
||||
pretty (NonCoveringCall [f])
|
||||
= reflow "not covering due to call to function" <++> pretty f
|
||||
pretty (NonCoveringCall cs)
|
||||
= reflow "not covering due to calls to functions" <++> concatWith (surround (comma <+> space)) (pretty <$> cs)
|
||||
|
||||
-- Totality status of a definition. We separate termination checking from
|
||||
-- coverage checking.
|
||||
public export
|
||||
@ -658,6 +690,13 @@ Show Totality where
|
||||
showTot t IsCovering = show t
|
||||
showTot t c = show c ++ "; " ++ show t
|
||||
|
||||
export
|
||||
Pretty Totality where
|
||||
pretty (MkTotality IsTerminating IsCovering) = pretty "total"
|
||||
pretty (MkTotality IsTerminating c) = pretty c
|
||||
pretty (MkTotality t IsCovering) = pretty t
|
||||
pretty (MkTotality t c) = pretty c <+> semi <++> pretty t
|
||||
|
||||
export
|
||||
unchecked : Totality
|
||||
unchecked = MkTotality Unchecked IsCovering
|
||||
|
||||
@ -73,6 +73,10 @@ data CLOpt
|
||||
Quiet |
|
||||
||| Run Idris 2 in verbose mode (cancels quiet if it's the default)
|
||||
Verbose |
|
||||
||| Set the console width for REPL output
|
||||
ConsoleWidth Nat |
|
||||
||| Whether to use color in the console output
|
||||
Color Bool |
|
||||
||| Set the log level globally
|
||||
Logging Nat |
|
||||
||| Add a package as a dependency
|
||||
@ -214,6 +218,12 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
|
||||
(Just "Suppress the banner"),
|
||||
MkOpt ["--quiet", "-q"] [] [Quiet]
|
||||
(Just "Quiet mode; display fewer messages"),
|
||||
MkOpt ["--consolewidth"] [RequiredNat "console width"] (\l => [ConsoleWidth l])
|
||||
(Just "Width for console output (0 for unbounded) (120 by default)"),
|
||||
MkOpt ["--color", "--colour"] [] ([Color True])
|
||||
(Just "Forces colored console output (enabled by default)"),
|
||||
MkOpt ["--no-color", "--no-colour"] [] ([Color False])
|
||||
(Just "Disables colored console output"),
|
||||
MkOpt ["--verbose"] [] [Verbose]
|
||||
(Just "Verbose mode (default)"),
|
||||
MkOpt ["--log"] [RequiredNat "log level"] (\l => [Logging l])
|
||||
|
||||
@ -47,19 +47,21 @@ pshowNoNorm env tm
|
||||
ploc : {auto o : Ref ROpts REPLOpts} ->
|
||||
FC -> Core (Doc IdrisAnn)
|
||||
ploc EmptyFC = pure emptyDoc
|
||||
ploc (MkFC _ s e) = do
|
||||
ploc fc@(MkFC fn s e) = do
|
||||
let sr = fromInteger $ cast $ fst s
|
||||
let sc = fromInteger $ cast $ snd s
|
||||
let er = fromInteger $ cast $ fst e
|
||||
let ec = fromInteger $ cast $ snd e
|
||||
let nsize = length $ show (er + 1)
|
||||
let head = annotate FileCtxt (pretty fc)
|
||||
let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe)
|
||||
source <- lines <$> getCurrentElabSource
|
||||
if sr == er
|
||||
then do
|
||||
let line = maybe emptyDoc pretty (elemAt source sr)
|
||||
let emph = spaces (cast sc) <+> pretty (Extra.replicate (ec `minus` sc) '^')
|
||||
pure $ space <+> pretty (sr + 1) <++> pipe <++> align (vsep [line, emph])
|
||||
else pure $ vsep (addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source))
|
||||
let line = (annotate FileCtxt pipe) <++> maybe emptyDoc pretty (elemAt source sr)
|
||||
let emph = (annotate FileCtxt pipe) <++> spaces (cast sc) <+> annotate Error (pretty (Extra.replicate (ec `minus` sc) '^'))
|
||||
pure $ vsep [emptyDoc, head, firstRow, annotate FileCtxt (space <+> pretty (sr + 1)) <++> align (vsep [line, emph]), emptyDoc]
|
||||
else pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source)) <+> line
|
||||
where
|
||||
extractRange : Nat -> Nat -> List String -> List String
|
||||
extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
|
||||
@ -67,7 +69,7 @@ ploc (MkFC _ s e) = do
|
||||
pad size s = replicate (size `minus` length s) '0' ++ s
|
||||
addLineNumbers : Nat -> Nat -> List (Doc IdrisAnn) -> List (Doc IdrisAnn)
|
||||
addLineNumbers size st xs =
|
||||
snd $ foldl (\(i, s), l => (S i, snoc s (space <+> pretty (pad size $ show $ i + 1) <++> pipe <++> l))) (st, []) xs
|
||||
snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs
|
||||
|
||||
export
|
||||
perror : {auto c : Ref Ctxt Defs} ->
|
||||
@ -76,88 +78,80 @@ perror : {auto c : Ref Ctxt Defs} ->
|
||||
Error -> Core (Doc IdrisAnn)
|
||||
perror (Fatal err) = perror err
|
||||
perror (CantConvert fc env l r)
|
||||
= pure $ vsep [ reflow "Mismatch between" <+> colon
|
||||
, indent 4 !(pshow env l)
|
||||
= pure $ errorDesc (hsep [ reflow "Mismatch between" <+> colon
|
||||
, code !(pshow env l)
|
||||
, pretty "and"
|
||||
, indent 4 !(pshow env r)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
, code !(pshow env r) <+> dot
|
||||
]) <+> line <+> !(ploc fc)
|
||||
perror (CantSolveEq fc env l r)
|
||||
= pure $ vsep [ reflow "Can't solve constraint between" <+> colon
|
||||
, indent 4 !(pshow env l)
|
||||
= pure $ errorDesc (hsep [ reflow "Can't solve constraint between" <+> colon
|
||||
, code !(pshow env l)
|
||||
, pretty "and"
|
||||
, indent 4 !(pshow env r)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
, code !(pshow env r) <+> dot
|
||||
]) <+> line <+> !(ploc fc)
|
||||
perror (PatternVariableUnifies fc env n tm)
|
||||
= pure $ vsep [ reflow "Pattern variable" <++> pretty (showPVar n) <++> reflow "unifies with" <+> colon
|
||||
, indent 4 !(pshow env tm)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
= pure $ errorDesc (hsep [ reflow "Pattern variable"
|
||||
, code (prettyVar n)
|
||||
, reflow "unifies with" <+> colon
|
||||
, code !(pshow env tm) <+> dot
|
||||
]) <+> line <+> !(ploc fc)
|
||||
where
|
||||
showPVar : Name -> String
|
||||
showPVar (PV n _) = showPVar n
|
||||
showPVar n = show n
|
||||
prettyVar : Name -> Doc IdrisAnn
|
||||
prettyVar (PV n _) = prettyVar n
|
||||
prettyVar n = pretty n
|
||||
perror (CyclicMeta fc env n tm)
|
||||
= pure $ reflow "Cycle detected in solution of metavariable" <++> pretty !(prettyName n) <++> equals
|
||||
<++> !(pshow env tm) <++> pretty "at" <+> colon <+> line
|
||||
<+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Cycle detected in solution of metavariable" <++> meta (pretty !(prettyName n)) <++> equals
|
||||
<++> code !(pshow env tm)) <+> line <+> !(ploc fc)
|
||||
perror (WhenUnifying _ env x y err)
|
||||
= pure $ reflow "When unifying" <++> !(pshow env x) <++> pretty "and"
|
||||
<++> !(pshow env y) <+> line
|
||||
<+> !(perror err)
|
||||
= pure $ errorDesc (reflow "When unifying" <++> code !(pshow env x) <++> pretty "and"
|
||||
<++> code !(pshow env y)) <+> dot <+> line <+> !(perror err)
|
||||
perror (ValidCase fc env (Left tm))
|
||||
= pure $ !(pshow env tm) <++> reflow "is not a valid impossible case at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a valid impossible case.")
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (ValidCase _ env (Right err))
|
||||
= pure $ reflow "Impossible pattern gives an error" <+> colon <+> line <+> !(perror err)
|
||||
= pure $ errorDesc (reflow "Impossible pattern gives an error" <+> colon) <+> line <+> !(perror err)
|
||||
perror (UndefinedName fc x)
|
||||
= pure $ reflow "Undefined name" <++> pretty (show x)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Undefined name" <++> code (pretty x) <+> dot) <++> line <+> !(ploc fc)
|
||||
perror (InvisibleName fc n (Just ns))
|
||||
= pure $ pretty "Name" <++> pretty (show n) <++> reflow "is inaccessible since"
|
||||
<++> concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "is not explicitly imported at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (pretty "Name" <++> code (pretty n) <++> reflow "is inaccessible since"
|
||||
<++> code (concatWith (surround dot) (pretty <$> reverse ns)) <++> reflow "is not explicitly imported.")
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (InvisibleName fc x Nothing)
|
||||
= pure $ pretty "Name" <++> pretty (show x) <++> reflow "is private at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (pretty "Name" <++> code (pretty x) <++> reflow "is private.") <+> line <+> !(ploc fc)
|
||||
perror (BadTypeConType fc n)
|
||||
= pure $ reflow "Return type of" <++> pretty (show n) <++> reflow "must be Type at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be" <++> code (pretty "Type")
|
||||
<+> dot) <+> line <+> !(ploc fc)
|
||||
perror (BadDataConType fc n fam)
|
||||
= pure $ reflow "Return type of" <++> pretty (show n) <++> reflow "must be in"
|
||||
<++> pretty (show !(toFullNames fam)) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be in"
|
||||
<++> code (pretty !(toFullNames fam))) <++> line <+> !(ploc fc)
|
||||
perror (NotCovering fc n IsCovering)
|
||||
= pure $ reflow "Internal error" <++> parens (reflow "Coverage of" <++> pretty (show n))
|
||||
= pure $ errorDesc (reflow "Internal error" <++> parens (reflow "Coverage of" <++> code (pretty n)))
|
||||
perror (NotCovering fc n (MissingCases cs))
|
||||
= pure $ vsep [ pretty !(prettyName n) <++> reflow "is not covering at" <+> colon
|
||||
, !(ploc fc)
|
||||
, reflow "Missing cases" <+> colon
|
||||
, indent 4 (vsep !(traverse (pshow []) cs))
|
||||
]
|
||||
= pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not covering.")
|
||||
<+> line <+> !(ploc fc) <+> line
|
||||
<+> reflow "Missing cases" <+> colon <+> line
|
||||
<+> indent 4 (vsep !(traverse (pshow []) cs))
|
||||
perror (NotCovering fc n (NonCoveringCall ns))
|
||||
= pure $ vsep [ pretty !(prettyName n) <++> reflow "is not covering at" <+> colon
|
||||
, !(ploc fc)
|
||||
, reflow "Calls non covering function" <+>
|
||||
= pure $ errorDesc (pretty !(prettyName n) <++> reflow "is not covering.")
|
||||
<+> line <+> !(ploc fc) <+> line
|
||||
<+> reflow "Calls non covering function" <+>
|
||||
case ns of
|
||||
[fn] => space <+> pretty (show fn)
|
||||
_ => pretty 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty . show <$> ns)
|
||||
]
|
||||
[fn] => space <+> pretty fn
|
||||
_ => pretty 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty <$> ns)
|
||||
perror (NotTotal fc n r)
|
||||
= pure $ vsep [ pretty !(prettyName n) <++> reflow "is not total" <+> colon
|
||||
, pretty (show r)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
= pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not total," <++> pretty r)
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (LinearUsed fc count n)
|
||||
= pure $ reflow "There are" <++> pretty (show count) <++> reflow "uses of linear name" <++> pretty (sugarName n)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "There are" <++> pretty count <++> reflow "uses of linear name"
|
||||
<++> code (pretty (sugarName n)) <+> dot)
|
||||
<++> line <+> !(ploc fc)
|
||||
perror (LinearMisuse fc n exp ctx)
|
||||
= if isErased exp
|
||||
then pure $ pretty (show n) <++> reflow "is not accessible in this context at" <+> colon <+> line <+> !(ploc fc)
|
||||
else pure $ reflow "Trying to use" <++> prettyRig exp <++> pretty "name" <++> pretty (sugarName n) <++>
|
||||
pretty "in" <++> prettyRel ctx <++> pretty "context at" <+> colon <+> line <+> !(ploc fc)
|
||||
then pure $ errorDesc (code (pretty n) <++> reflow "is not accessible in this context.")
|
||||
<+> line <+> !(ploc fc)
|
||||
else pure $ errorDesc (reflow "Trying to use" <++> prettyRig exp <++> pretty "name"
|
||||
<++> code (pretty (sugarName n)) <++> pretty "in" <++> prettyRel ctx <++> pretty "context.")
|
||||
<+> line <+> !(ploc fc)
|
||||
where
|
||||
prettyRig : RigCount -> Doc ann
|
||||
prettyRig = elimSemi (pretty "irrelevant")
|
||||
@ -169,45 +163,43 @@ perror (LinearMisuse fc n exp ctx)
|
||||
(pretty "relevant")
|
||||
(const $ pretty "non-linear")
|
||||
perror (BorrowPartial fc env tm arg)
|
||||
= pure $ !(pshow env tm) <++>
|
||||
reflow "borrows argument" <++> !(pshow env arg) <++>
|
||||
reflow "so must be fully applied at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code !(pshow env tm) <++> reflow "borrows argument" <++> code !(pshow env arg)
|
||||
<++> reflow "so must be fully applied.")
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (BorrowPartialType fc env tm)
|
||||
= pure $ !(pshow env tm) <++>
|
||||
reflow "borrows, so must return a concrete type at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code !(pshow env tm) <++>
|
||||
reflow "borrows, so must return a concrete type.") <+> line <+> !(ploc fc)
|
||||
perror (AmbiguousName fc ns)
|
||||
= pure $ pretty "Ambiguous name" <++> pretty (show ns) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (pretty "Ambiguous name" <++> code (pretty ns))
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (AmbiguousElab fc env ts)
|
||||
= do pp <- getPPrint
|
||||
setPPrint (record { fullNamespace = True } pp)
|
||||
let res = vsep [ reflow "Ambiguous elaboration at" <+> colon
|
||||
, !(ploc fc)
|
||||
, reflow "Possible correct results" <+> colon
|
||||
let res = vsep [ errorDesc (reflow "Ambiguous elaboration. Possible results" <+> colon)
|
||||
, indent 4 (vsep !(traverse (pshow env) ts))
|
||||
]
|
||||
] <+> line <+> !(ploc fc)
|
||||
setPPrint pp
|
||||
pure res
|
||||
perror (AmbiguousSearch fc env tgt ts)
|
||||
= pure $ vsep [ reflow "Multiple solutions found in search of" <+> colon
|
||||
= pure $ vsep [ errorDesc (reflow "Multiple solutions found in search of" <+> colon)
|
||||
, indent 4 !(pshowNoNorm env tgt)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
, reflow "Possible correct results" <+> colon
|
||||
, indent 4 (vsep !(traverse (pshowNoNorm env) ts))
|
||||
]
|
||||
perror (AmbiguityTooDeep fc n ns)
|
||||
= pure $ reflow "Maximum ambiguity depth exceeded in" <++> pretty (show !(getFullName n))
|
||||
<+> colon <++> concatWith (surround (pretty " --> ")) (pretty . show <$> !(traverse getFullName ns))
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Maximum ambiguity depth exceeded in" <++> code (pretty !(getFullName n))
|
||||
<+> colon) <+> line <+> concatWith (surround (pretty " --> ")) (pretty <$> !(traverse getFullName ns))
|
||||
<++> line <+> !(ploc fc)
|
||||
perror (AllFailed ts)
|
||||
= case allUndefined ts of
|
||||
Just e => perror e
|
||||
_ => pure $ reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon <+> line
|
||||
_ => pure $ errorDesc (reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon) <+> line
|
||||
<+> vsep !(traverse pAlterror ts)
|
||||
where
|
||||
pAlterror : (Maybe Name, Error) -> Core (Doc IdrisAnn)
|
||||
pAlterror (Just n, err)
|
||||
= pure $ pretty "If" <++> pretty (show !(aliasName !(getFullName n))) <+> colon <++> !(perror err) <+> line
|
||||
= pure $ pretty "If" <++> code (pretty !(aliasName !(getFullName n))) <+> colon <++> !(perror err)
|
||||
pAlterror (Nothing, err)
|
||||
= pure $ reflow "Possible error" <+> colon <+> line <+> indent 4 !(perror err)
|
||||
|
||||
@ -217,39 +209,39 @@ perror (AllFailed ts)
|
||||
allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es
|
||||
allUndefined _ = Nothing
|
||||
perror (RecordTypeNeeded fc _)
|
||||
= pure $ reflow "Can't infer type for this record update at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Can't infer type for this record update.") <+> line <+> !(ploc fc)
|
||||
perror (NotRecordField fc fld Nothing)
|
||||
= pure $ pretty fld <++> reflow "is not part of a record type at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code (pretty fld) <++> reflow "is not part of a record type.") <+> line <+> !(ploc fc)
|
||||
perror (NotRecordField fc fld (Just ty))
|
||||
= pure $ reflow "Record type" <++> pretty (show !(getFullName ty)) <++> reflow "has no field" <++> pretty fld
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Record type" <++> code (pretty !(getFullName ty)) <++> reflow "has no field"
|
||||
<++> code (pretty fld) <+> dot) <+> line <+> !(ploc fc)
|
||||
perror (NotRecordType fc ty)
|
||||
= pure $ pretty (show !(getFullName ty)) <++> reflow "is not a record type at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code (pretty !(getFullName ty)) <++> reflow "is not a record type.") <+> line <+> !(ploc fc)
|
||||
perror (IncompatibleFieldUpdate fc flds)
|
||||
= pure $ reflow "Field update" <++> concatWith (surround (pretty "->")) (pretty <$> flds)
|
||||
<++> reflow "not compatible with other updates at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (InvalidImplicits fc env [Just n] tm)
|
||||
= pure $ pretty (show n) <++> reflow "is not a valid implicit argument in" <++> !(pshow env tm)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code (pretty n) <++> reflow "is not a valid implicit argument in" <++> !(pshow env tm)
|
||||
<+> dot) <+> line <+> !(ploc fc)
|
||||
perror (InvalidImplicits fc env ns tm)
|
||||
= pure $ concatWith (surround (comma <+> space)) (pretty . show <$> ns)
|
||||
<++> reflow "are not valid implicit arguments in" <++> !(pshow env tm)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (concatWith (surround (comma <+> space)) (code . pretty <$> ns)
|
||||
<++> reflow "are not valid implicit arguments in" <++> !(pshow env tm) <+> dot)
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (TryWithImplicits fc env imps)
|
||||
= pure $ reflow "Need to bind implicits"
|
||||
<++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Need to bind implicits"
|
||||
<++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps) <+> dot)
|
||||
<+> line <+> !(ploc fc)
|
||||
where
|
||||
tshow : {vars : _} ->
|
||||
Env Term vars -> (Name, Term vars) -> Core (Doc IdrisAnn)
|
||||
tshow env (n, ty) = pure $ pretty (show n) <++> colon <++> !(pshow env ty)
|
||||
tshow env (n, ty) = pure $ pretty n <++> colon <++> code !(pshow env ty)
|
||||
perror (BadUnboundImplicit fc env n ty)
|
||||
= pure $ reflow "Can't bind name" <++> pretty (nameRoot n) <++> reflow "with type" <++> !(pshow env ty)
|
||||
<++> reflow "here at" <+> colon <+> line <+> !(ploc fc) <+> line <+> reflow "Try binding explicitly."
|
||||
= pure $ errorDesc (reflow "Can't bind name" <++> code (pretty (nameRoot n)) <++> reflow "with type" <++> code !(pshow env ty)
|
||||
<+> colon) <+> line <+> !(ploc fc) <+> line <+> reflow "Try binding explicitly."
|
||||
perror (CantSolveGoal fc env g)
|
||||
= let (_ ** (env', g')) = dropEnv env g in
|
||||
pure $ reflow "Can't find an implementation for" <++> !(pshow env' g')
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env' g')
|
||||
<+> dot) <+> line <+> !(ploc fc)
|
||||
where
|
||||
-- For display, we don't want to see the full top level type; just the
|
||||
-- return type
|
||||
@ -261,101 +253,105 @@ perror (CantSolveGoal fc env g)
|
||||
dropEnv env tm = (_ ** (env, tm))
|
||||
|
||||
perror (DeterminingArg fc n i env g)
|
||||
= pure $ reflow "Can't find an implementation for" <++> !(pshow env g) <+> line
|
||||
<+> reflow "since I can't infer a value for argument" <++> pretty (show n)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env g) <+> line
|
||||
<+> reflow "since I can't infer a value for argument" <++> code (pretty n) <+> dot)
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (UnsolvedHoles hs)
|
||||
= pure $ reflow "Unsolved holes" <+> colon <+> line <+> prettyHoles hs
|
||||
= pure $ errorDesc (reflow "unsolved holes" <+> colon) <+> line <+> !(prettyHoles hs)
|
||||
where
|
||||
prettyHoles : List (FC, Name) -> Doc IdrisAnn
|
||||
prettyHoles [] = emptyDoc
|
||||
prettyHoles : List (FC, Name) -> Core (Doc IdrisAnn)
|
||||
prettyHoles [] = pure emptyDoc
|
||||
prettyHoles ((fc, n) :: hs)
|
||||
= pretty (show n) <++> reflow "introduced at" <++> pretty (show fc) <+> line <+> prettyHoles hs
|
||||
= pure $ meta (pretty n) <++> reflow "introduced at:" <++> !(ploc fc) <+> !(prettyHoles hs)
|
||||
perror (CantInferArgType fc env n h ty)
|
||||
= pure $ reflow "Can't infer type for argument" <++> pretty (show n) <+> line
|
||||
<+> pretty "Got" <++> !(pshow env ty) <++> reflow "with hole" <++> pretty (show h)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Can't infer type for argument" <++> code (pretty n)) <+> line
|
||||
<+> pretty "Got" <++> code !(pshow env ty) <++> reflow "with hole" <++> meta (pretty h) <+> dot
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (SolvedNamedHole fc env h tm)
|
||||
= pure $ reflow "Named hole" <++> pretty (show h) <++> reflow "has been solved by unification" <+> line
|
||||
<+> pretty "Result" <+> colon <++> !(pshow env tm)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Named hole" <++> meta (pretty h) <++> reflow "has been solved by unification.") <+> line
|
||||
<+> pretty "Result" <+> colon <++> code !(pshow env tm)
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (VisibilityError fc vx x vy y)
|
||||
= pure $ pretty (show vx) <++> pretty (sugarName !(toFullNames x))
|
||||
<++> reflow "cannot refer to" <++> pretty (show vy) <++> pretty (sugarName !(toFullNames y))
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (keyword (pretty vx) <++> code (pretty (sugarName !(toFullNames x)))
|
||||
<++> reflow "cannot refer to" <++> keyword (pretty vy) <++> code (pretty (sugarName !(toFullNames y))))
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (NonLinearPattern fc n)
|
||||
= pure $ reflow "Non linear pattern" <++> pretty (sugarName n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Non linear pattern" <++> code (pretty (sugarName n)) <+> dot) <+> line <+> !(ploc fc)
|
||||
perror (BadPattern fc n)
|
||||
= pure $ reflow "Pattern not allowed here" <+> colon <++> pretty (show n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Pattern not allowed here" <+> colon <++> code (pretty n) <+> dot) <+> line <+> !(ploc fc)
|
||||
perror (NoDeclaration fc n)
|
||||
= pure $ reflow "No type declaration for" <++> pretty (show n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (AlreadyDefined fc n) = pure $ pretty (show n) <++> reflow "is already defined"
|
||||
= pure $ errorDesc (reflow "No type declaration for" <++> code (pretty n) <+> dot) <+> line <+> !(ploc fc)
|
||||
perror (AlreadyDefined fc n) = pure $ errorDesc (code (pretty n) <++> reflow "is already defined.") <+> line <+> !(ploc fc)
|
||||
perror (NotFunctionType fc env tm)
|
||||
= pure $ !(pshow env tm) <++> reflow "is not a function type at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a function type.") <+> line <+> !(ploc fc)
|
||||
perror (RewriteNoChange fc env rule ty)
|
||||
= pure $ reflow "Rewriting by" <++> !(pshow env rule)
|
||||
<++> reflow "did not change type" <++> !(pshow env ty)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Rewriting by" <++> code !(pshow env rule)
|
||||
<++> reflow "did not change type" <++> code !(pshow env ty) <+> dot)
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (NotRewriteRule fc env rule)
|
||||
= pure $ !(pshow env rule) <++> reflow "is not a rewrite rule type at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (code !(pshow env rule) <++> reflow "is not a rewrite rule type.") <+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n DifferingArgNumbers)
|
||||
= pure $ reflow "Patterns for" <++> pretty !(prettyName n) <++> reflow "have differing numbers of arguments at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "have differing numbers of arguments.")
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n DifferingTypes)
|
||||
= pure $ reflow "Patterns for" <++> pretty !(prettyName n) <++> reflow "require matching on different types at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "require matching on different types.")
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n UnknownType)
|
||||
= pure $ reflow "Can't infer type to match in" <++> pretty !(prettyName n) <++> pretty "at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Can't infer type to match in" <++> code (pretty !(prettyName n)) <+> dot)
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n (NotFullyApplied cn))
|
||||
= pure $ pretty "Constructor" <++> pretty (show !(toFullNames cn)) <++> reflow "is not fully applied at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (pretty "Constructor" <++> code (pretty !(toFullNames cn)) <++> reflow "is not fully applied.")
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n (MatchErased (_ ** (env, tm))))
|
||||
= pure $ reflow "Attempt to match on erased argument" <++> !(pshow env tm) <++> pretty "in"
|
||||
<++> pretty !(prettyName n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Attempt to match on erased argument" <++> code !(pshow env tm) <++> pretty "in"
|
||||
<++> code (pretty !(prettyName n)) <+> dot) <+> line <+> !(ploc fc)
|
||||
perror (BadDotPattern fc env reason x y)
|
||||
= pure $ reflow "Can't match on" <++> !(pshow env x)
|
||||
<++> parens (pretty (show reason)) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env x)
|
||||
<++> parens (pretty reason) <+> dot) <+> line <+> !(ploc fc)
|
||||
perror (MatchTooSpecific fc env tm)
|
||||
= pure $ reflow "Can't match on" <++> !(pshow env tm)
|
||||
<++> reflow "as it has a polymorphic type at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env tm)
|
||||
<++> reflow "as it has a polymorphic type.") <+> line <+> !(ploc fc)
|
||||
perror (BadImplicit fc str)
|
||||
= pure $ reflow "Can't infer type for unbound implicit name" <++> pretty str <++> pretty "at" <+> colon
|
||||
= pure $ errorDesc (reflow "Can't infer type for unbound implicit name" <++> code (pretty str) <+> dot)
|
||||
<+> line <+> !(ploc fc) <+> line <+> reflow "Try making it a bound implicit."
|
||||
perror (BadRunElab fc env script)
|
||||
= pure $ reflow "Bad elaborator script" <++> !(pshow env script)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (GenericMsg fc str) = pure $ pretty str <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
= pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script) <+> dot)
|
||||
<+> line <+> !(ploc fc)
|
||||
perror (GenericMsg fc str) = pure $ pretty str <+> line <+> !(ploc fc)
|
||||
perror (TTCError msg)
|
||||
= pure $ reflow "Error in TTC file" <+> colon <++> pretty (show msg)
|
||||
= pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> pretty (show msg))
|
||||
<++> parens (pretty "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files")
|
||||
perror (FileErr fname err)
|
||||
= pure $ reflow "File error in" <++> pretty fname <++> colon <++> pretty (show err)
|
||||
= pure $ errorDesc (reflow "File error in" <++> pretty fname <++> colon) <++> pretty (show err)
|
||||
perror (ParseFail _ err)
|
||||
= pure $ pretty (show err)
|
||||
perror (ModuleNotFound _ ns)
|
||||
= pure $ concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "not found"
|
||||
= pure $ errorDesc (concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "not found")
|
||||
perror (CyclicImports ns)
|
||||
= pure $ reflow "Module imports form a cycle" <+> colon <++> concatWith (surround (pretty " -> ")) (prettyMod <$> ns)
|
||||
= pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (prettyMod <$> ns)
|
||||
where
|
||||
prettyMod : List String -> Doc IdrisAnn
|
||||
prettyMod ns = concatWith (surround dot) (pretty <$> reverse ns)
|
||||
perror ForceNeeded = pure $ reflow "Internal error when resolving implicit laziness"
|
||||
perror (InternalError str) = pure $ reflow "INTERNAL ERROR" <+> colon <++> pretty str
|
||||
perror (UserError str) = pure $ pretty "Error" <+> colon <++> pretty str
|
||||
perror ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
|
||||
perror (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty str
|
||||
perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty str
|
||||
|
||||
perror (InType fc n err)
|
||||
= pure $ reflow "While processing type of" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
= pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot
|
||||
, !(perror err)
|
||||
]
|
||||
perror (InCon fc n err)
|
||||
= pure $ reflow "While processing constructor" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
= pure $ hsep [ errorDesc (reflow "While processing constructor" <++> code (pretty !(prettyName n))) <+> dot
|
||||
, !(perror err)
|
||||
]
|
||||
perror (InLHS fc n err)
|
||||
= pure $ reflow "While processing left hand side of" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
= pure $ hsep [ errorDesc (reflow "While processing left hand side of" <++> code (pretty !(prettyName n))) <+> dot
|
||||
, !(perror err)
|
||||
]
|
||||
perror (InRHS fc n err)
|
||||
= pure $ reflow "While processing right hand side of" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
= pure $ hsep [ errorDesc (reflow "While processing right hand side of" <++> code (pretty !(prettyName n))) <+> dot
|
||||
, !(perror err)
|
||||
]
|
||||
|
||||
export
|
||||
pwarning : {auto c : Ref Ctxt Defs} ->
|
||||
@ -363,9 +359,9 @@ pwarning : {auto c : Ref Ctxt Defs} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
Warning -> Core (Doc IdrisAnn)
|
||||
pwarning (UnreachableClause fc env tm)
|
||||
= pure $ annotate Warning (pretty "Warning" <+> colon)
|
||||
<++> pretty "unreachable clause" <+> colon
|
||||
<++> !(pshow env tm)
|
||||
= pure $ errorDesc (reflow "Unreachable clause:"
|
||||
<++> code !(pshow env tm))
|
||||
<+> line <+> !(ploc fc)
|
||||
|
||||
prettyMaybeLoc : Maybe FC -> Doc IdrisAnn
|
||||
prettyMaybeLoc Nothing = emptyDoc
|
||||
@ -376,8 +372,8 @@ display : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
Error -> Core (Doc IdrisAnn)
|
||||
display err
|
||||
= pure $ prettyMaybeLoc (getErrorLoc err) <+> !(perror err)
|
||||
display err = do
|
||||
pure $ annotate Error (pretty "Error:") <++> !(perror err)
|
||||
|
||||
export
|
||||
displayWarning : {auto c : Ref Ctxt Defs} ->
|
||||
@ -385,4 +381,4 @@ displayWarning : {auto c : Ref Ctxt Defs} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
Warning -> Core (Doc IdrisAnn)
|
||||
displayWarning w
|
||||
= pure $ prettyMaybeLoc (getWarningLoc w) <+> !(pwarning w)
|
||||
= pure $ annotate Warning (pretty "Warning:") <++> !(pwarning w)
|
||||
|
||||
@ -1785,6 +1785,9 @@ data CmdArg : Type where
|
||||
||| The command takes a string
|
||||
StringArg : CmdArg
|
||||
|
||||
||| The command takes a on or off.
|
||||
OnOffArg : CmdArg
|
||||
|
||||
||| The command takes multiple arguments.
|
||||
Args : List CmdArg -> CmdArg
|
||||
|
||||
@ -1799,6 +1802,7 @@ Show CmdArg where
|
||||
show FileArg = "<file>"
|
||||
show ModuleArg = "<module>"
|
||||
show StringArg = "<module>"
|
||||
show OnOffArg = "(on|off)"
|
||||
show (Args args) = showSep " " (map show args)
|
||||
|
||||
export
|
||||
@ -1925,6 +1929,19 @@ numberArgCmd parseCmd command doc = (names, NumberArg, doc, parse)
|
||||
i <- intLit
|
||||
pure (command (fromInteger i))
|
||||
|
||||
onOffArgCmd : ParseCmd -> (Bool -> REPLCmd) -> String -> CommandDefinition
|
||||
onOffArgCmd parseCmd command doc = (names, OnOffArg, doc, parse)
|
||||
where
|
||||
names : List String
|
||||
names = extractNames parseCmd
|
||||
|
||||
parse : Rule REPLCmd
|
||||
parse = do
|
||||
symbol ":"
|
||||
runParseCmd parseCmd
|
||||
i <- onOffLit
|
||||
pure (command i)
|
||||
|
||||
compileArgsCmd : ParseCmd -> (PTerm -> String -> REPLCmd) -> String -> CommandDefinition
|
||||
compileArgsCmd parseCmd command doc
|
||||
= (names, Args [FileArg, ExprArg], doc, parse)
|
||||
@ -1961,6 +1978,8 @@ parserCommandsForHelp =
|
||||
, nameArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a name"
|
||||
, moduleArgCmd (ParseIdentCmd "browse") Browse "Browse contents of a namespace"
|
||||
, numberArgCmd (ParseREPLCmd ["log", "logging"]) SetLog "Set logging level"
|
||||
, numberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth "Set the width of the console output (0 for unbounded)"
|
||||
, onOffArgCmd (ParseREPLCmd ["color", "colour"]) SetColor "Whether to use color for the console output (enabled by default)"
|
||||
, noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)"
|
||||
, noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
|
||||
, noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text"
|
||||
|
||||
@ -5,51 +5,51 @@ import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Render.Terminal
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
|
||||
import Idris.REPLOpts
|
||||
import Idris.Syntax
|
||||
|
||||
%default covering
|
||||
|
||||
public export
|
||||
data SyntaxAnn
|
||||
= Typ
|
||||
| Function
|
||||
| Data
|
||||
| Keyword
|
||||
| Bound
|
||||
| Pragma
|
||||
| Meta
|
||||
|
||||
public export
|
||||
data IdrisAnn
|
||||
= Warning
|
||||
| Error
|
||||
| ErrorDesc
|
||||
| FileCtxt
|
||||
| Syntax SyntaxAnn
|
||||
| Code
|
||||
| Meta
|
||||
| Keyword
|
||||
| Pragma
|
||||
|
||||
export
|
||||
colorAnn : IdrisAnn -> AnsiStyle
|
||||
colorAnn Warning = color Yellow
|
||||
colorAnn Error = color BrightRed
|
||||
colorAnn Warning = color Yellow <+> bold
|
||||
colorAnn Error = color BrightRed <+> bold
|
||||
colorAnn ErrorDesc = bold
|
||||
colorAnn FileCtxt = color BrightBlue
|
||||
colorAnn (Syntax Typ) = color Magenta
|
||||
colorAnn (Syntax Function) = neutral
|
||||
colorAnn (Syntax Data) = color Blue
|
||||
colorAnn (Syntax Keyword) = color Red
|
||||
colorAnn (Syntax Bound) = color Green
|
||||
colorAnn (Syntax Pragma) = color BrightMagenta
|
||||
colorAnn (Syntax Meta) = color Magenta
|
||||
colorAnn Code = color Magenta
|
||||
colorAnn Keyword = color Red
|
||||
colorAnn Pragma = color BrightMagenta
|
||||
colorAnn Meta = color Green
|
||||
|
||||
export
|
||||
errorDesc : Doc IdrisAnn -> Doc IdrisAnn
|
||||
errorDesc = annotate ErrorDesc
|
||||
|
||||
export
|
||||
keyword : Doc IdrisAnn -> Doc IdrisAnn
|
||||
-- keyword = annotate (Syntax Keyword)
|
||||
keyword = id
|
||||
keyword = annotate Keyword
|
||||
|
||||
meta : String -> Doc IdrisAnn
|
||||
-- meta s = annotate (Syntax Meta) (pretty s)
|
||||
meta s = pretty s
|
||||
export
|
||||
meta : Doc IdrisAnn -> Doc IdrisAnn
|
||||
meta = annotate Meta
|
||||
|
||||
export
|
||||
code : Doc IdrisAnn -> Doc IdrisAnn
|
||||
code = annotate Code
|
||||
|
||||
ite : Doc IdrisAnn -> Doc IdrisAnn -> Doc IdrisAnn -> Doc IdrisAnn
|
||||
-- ite x t e = keyword (pretty "if") <++> x <++> hang 3 (fillSep [keyword (pretty "then") <++> t, keyword (pretty "else") <++> e])
|
||||
ite x t e = (pretty "if") <++> x <++> hang 3 (fillSep [(pretty "then") <++> t, (pretty "else") <++> e])
|
||||
ite x t e = keyword (pretty "if") <++> x <++> align (fillSep [keyword (pretty "then") <++> t, keyword (pretty "else") <++> e])
|
||||
|
||||
let_ : Doc IdrisAnn
|
||||
let_ = keyword (pretty "let")
|
||||
@ -84,13 +84,9 @@ default_ = keyword (pretty "default")
|
||||
rewrite_ : Doc IdrisAnn
|
||||
rewrite_ = keyword (pretty "rewrite")
|
||||
|
||||
pragma : String -> Doc IdrisAnn
|
||||
-- pragma s = annotate (Syntax Pragma) (pretty s)
|
||||
pragma s = (pretty s)
|
||||
|
||||
bound : Doc IdrisAnn -> Doc IdrisAnn
|
||||
-- bound = annotate (Syntax Bound)
|
||||
bound = id
|
||||
export
|
||||
pragma : Doc IdrisAnn -> Doc IdrisAnn
|
||||
pragma = annotate Pragma
|
||||
|
||||
prettyParens : (1 _ : Bool) -> Doc ann -> Doc ann
|
||||
prettyParens False s = s
|
||||
@ -189,16 +185,15 @@ mutual
|
||||
else go d f <++> braces (pretty n <++> equals <++> pretty a)
|
||||
go d (PImplicitApp _ f (Just n) a) =
|
||||
go d f <++> braces (pretty n <++> equals <++> go d a)
|
||||
go d (PSearch _ _) = pragma "%search"
|
||||
go d (PSearch _ _) = pragma (pretty "%search")
|
||||
go d (PQuote _ tm) = pretty '`' <+> parens (go d tm)
|
||||
go d (PQuoteName _ n) = pretty '`' <+> braces (braces (pretty n))
|
||||
go d (PQuoteDecl _ tm) = pretty '`' <+> brackets (angles (angles (pretty "declaration")))
|
||||
go d (PUnquote _ tm) = pretty '~' <+> parens (go d tm)
|
||||
go d (PRunElab _ tm) = pragma "%runElab" <++> go d tm
|
||||
go d (PRunElab _ tm) = pragma (pretty "%runElab") <++> go d tm
|
||||
go d (PPrimVal _ c) = pretty c
|
||||
go d (PHole _ _ n) = meta (strCons '?' n)
|
||||
-- go d (PType _) = annotate (Syntax Typ) (pretty "Type")
|
||||
go d (PType _) = (pretty "Type")
|
||||
go d (PHole _ _ n) = meta (pretty (strCons '?' n))
|
||||
go d (PType _) = pretty "Type"
|
||||
go d (PAs _ n p) = pretty n <+> pretty '@' <+> go d p
|
||||
go d (PDotted _ p) = dot <+> go d p
|
||||
go d (PImplicit _) = pretty '_'
|
||||
@ -242,3 +237,24 @@ mutual
|
||||
go d (PPostfixProjsSection fc fields args) =
|
||||
parens (dot <+> concatWith (surround dot) (go d <$> fields) <+> fillSep (go App <$> args))
|
||||
go d (PWithUnambigNames fc ns rhs) = with_ <++> pretty ns <++> go d rhs
|
||||
|
||||
export
|
||||
render : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String
|
||||
render doc = do
|
||||
consoleWidth <- getConsoleWidth
|
||||
color <- getColor
|
||||
let opts = MkLayoutOptions $ if consoleWidth == 0
|
||||
then Unbounded
|
||||
else AvailablePerLine (cast consoleWidth) 1
|
||||
let layout = layoutPretty opts doc
|
||||
pure $ renderString $ if color then reAnnotateS colorAnn layout else unAnnotateS layout
|
||||
|
||||
export
|
||||
renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String
|
||||
renderWithoutColor doc = do
|
||||
consoleWidth <- getConsoleWidth
|
||||
let opts = MkLayoutOptions $ if consoleWidth == 0
|
||||
then Unbounded
|
||||
else AvailablePerLine (cast consoleWidth) 1
|
||||
let layout = layoutPretty opts doc
|
||||
pure $ renderString $ unAnnotateS layout
|
||||
|
||||
@ -54,6 +54,7 @@ import Data.NameMap
|
||||
import Data.Stream
|
||||
import Data.Strings
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
import Text.PrettyPrint.Prettyprinter.Render.Terminal
|
||||
|
||||
import System
|
||||
@ -534,6 +535,8 @@ data REPLResult : Type where
|
||||
FoundHoles : List HoleData -> REPLResult
|
||||
OptionsSet : List REPLOpt -> REPLResult
|
||||
LogLevelSet : Nat -> REPLResult
|
||||
ConsoleWidthSet : Nat -> REPLResult
|
||||
ColorSet : Bool -> REPLResult
|
||||
VersionIs : Version -> REPLResult
|
||||
DefDeclared : REPLResult
|
||||
Exited : REPLResult
|
||||
@ -766,6 +769,12 @@ process GetOpts
|
||||
process (SetLog lvl)
|
||||
= do setLogLevel lvl
|
||||
pure $ LogLevelSet lvl
|
||||
process (SetConsoleWidth n)
|
||||
= do setConsoleWidth n
|
||||
pure $ ConsoleWidthSet n
|
||||
process (SetColor b)
|
||||
= do setColor b
|
||||
pure $ ColorSet b
|
||||
process Metavars
|
||||
= do defs <- get Ctxt
|
||||
let ctxt = gamma defs
|
||||
@ -819,9 +828,8 @@ processCatch cmd
|
||||
put UST u'
|
||||
put Syn s'
|
||||
put ROpts o'
|
||||
pmsg <- display err
|
||||
let msg = reAnnotateS colorAnn $ layoutPretty defaultLayoutOptions pmsg -- FIXME: tmp
|
||||
pure $ REPLError $ renderString msg
|
||||
msg <- display err >>= render
|
||||
pure $ REPLError msg
|
||||
)
|
||||
|
||||
parseEmptyCmd : SourceEmptyRule (Maybe REPLCmd)
|
||||
@ -929,36 +937,64 @@ mutual
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
|
||||
displayResult (REPLError err) = printError err
|
||||
displayResult (Evaluated x Nothing) = printResult $ show x
|
||||
displayResult (Evaluated x (Just y)) = printResult $ show x ++ " : " ++ show y
|
||||
displayResult (Printed xs) = printResult (showSep "\n" xs)
|
||||
displayResult (TermChecked x y) = printResult $ show x ++ " : " ++ show y
|
||||
displayResult (FileLoaded x) = printResult $ "Loaded file " ++ x
|
||||
displayResult (ModuleLoaded x) = printResult $ "Imported module " ++ x
|
||||
displayResult (ErrorLoadingModule x err) = printError $ "Error loading module " ++ x ++ ": " ++ (renderString (layoutPretty defaultLayoutOptions (reAnnotate colorAnn !(perror err)))) -- FIXME: tmp
|
||||
displayResult (ErrorLoadingFile x err) = printError $ "Error loading file " ++ x ++ ": " ++ show err
|
||||
displayResult (ErrorsBuildingFile x errs) = printError $ "Error(s) building file " ++ x -- messages already displayed while building
|
||||
displayResult NoFileLoaded = printError "No file can be reloaded"
|
||||
displayResult (CurrentDirectory dir) = printResult ("Current working directory is '" ++ dir ++ "'")
|
||||
displayResult CompilationFailed = printError "Compilation failed"
|
||||
displayResult (Compiled f) = printResult $ "File " ++ f ++ " written"
|
||||
displayResult (ProofFound x) = printResult $ show x
|
||||
displayResult (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases
|
||||
displayResult (CheckedTotal xs) = printResult $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
|
||||
displayResult (FoundHoles []) = printResult $ "No holes"
|
||||
displayResult (FoundHoles [x]) = printResult $ "1 hole: " ++ show x.name
|
||||
displayResult (FoundHoles xs) = printResult $ show (length xs) ++ " holes: " ++
|
||||
showSep ", " (map (show . name) xs)
|
||||
displayResult (LogLevelSet k) = printResult $ "Set loglevel to " ++ show k
|
||||
displayResult (VersionIs x) = printResult $ showVersion True x
|
||||
displayResult (RequestedHelp) = printResult displayHelp
|
||||
displayResult (Evaluated x Nothing) = do
|
||||
term <- render (prettyTerm x)
|
||||
printResult term
|
||||
displayResult (Evaluated x (Just y)) = do
|
||||
term <- render (prettyTerm x <++> colon <++> code (prettyTerm y))
|
||||
printResult term
|
||||
displayResult (Printed xs) = do
|
||||
xs' <- render (vsep (pretty <$> xs))
|
||||
printResult xs'
|
||||
displayResult (TermChecked x y) = do
|
||||
term <- render (prettyTerm x <++> colon <++> code (prettyTerm y))
|
||||
printResult term
|
||||
displayResult (FileLoaded x) = do
|
||||
msg <- render (reflow "Loaded file" <++> pretty x)
|
||||
printResult msg
|
||||
displayResult (ModuleLoaded x) = do
|
||||
msg <- render (reflow "Imported module" <++> pretty x)
|
||||
printResult msg
|
||||
displayResult (ErrorLoadingModule x err) = do
|
||||
msg <- render (reflow "Error loading module" <++> pretty x <+> colon <++> !(perror err))
|
||||
printError msg
|
||||
displayResult (ErrorLoadingFile x err) = do
|
||||
msg <- render (reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err))
|
||||
printError msg
|
||||
displayResult (ErrorsBuildingFile x errs) = do
|
||||
msg <- render (reflow "Error(s) building file" <++> pretty x)
|
||||
printError msg -- messages already displayed while building
|
||||
displayResult NoFileLoaded = printError !(render (reflow "No file can be reloaded"))
|
||||
displayResult (CurrentDirectory dir) = do
|
||||
msg <- render (reflow "Current working directory is" <++> squotes (pretty dir))
|
||||
printResult msg
|
||||
displayResult CompilationFailed = printError !(render (reflow "Compilation failed"))
|
||||
displayResult (Compiled f) = do
|
||||
msg <- render (pretty "File" <++> pretty f <++> pretty "written")
|
||||
printResult msg
|
||||
displayResult (ProofFound x) = printResult !(render (prettyTerm x))
|
||||
displayResult (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases -- FIXME
|
||||
displayResult (CheckedTotal xs) = do
|
||||
msg <- render (vsep (map (\(fn, tot) => pretty fn <++> pretty "is" <++> pretty tot) xs))
|
||||
printResult msg
|
||||
displayResult (FoundHoles []) = printResult !(render (reflow "No holes"))
|
||||
displayResult (FoundHoles [x]) = printResult !(render (reflow "1 hole" <+> colon <++> pretty x.name))
|
||||
displayResult (FoundHoles xs) = do
|
||||
let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs)
|
||||
msg <- render (pretty (length xs) <++> pretty "holes" <+> colon <++> holes)
|
||||
printResult msg
|
||||
displayResult (LogLevelSet k) = printResult !(render (reflow "Set loglevel to" <++> pretty k))
|
||||
displayResult (ConsoleWidthSet k) = printResult !(render (reflow "Set consolewidth to" <++> pretty k))
|
||||
displayResult (ColorSet b) = printResult !(render (reflow (if b then "Set color on" else "Set color off")))
|
||||
displayResult (VersionIs x) = printResult !(render (pretty (showVersion True x)))
|
||||
displayResult (RequestedHelp) = printResult displayHelp -- FIXME
|
||||
displayResult (Edited (DisplayEdit [])) = pure ()
|
||||
displayResult (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs
|
||||
displayResult (Edited (EditError x)) = printError x
|
||||
displayResult (Edited (MadeLemma lit name pty pappstr)) = printResult (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
|
||||
displayResult (Edited (MadeWith lit wapp)) = printResult $ showSep "\n" (map (relit lit) wapp)
|
||||
displayResult (Edited (MadeCase lit cstr)) = printResult $ showSep "\n" (map (relit lit) cstr)
|
||||
displayResult (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
|
||||
displayResult (OptionsSet opts) = printResult !(render (vsep (pretty <$> opts)))
|
||||
displayResult _ = pure ()
|
||||
|
||||
export
|
||||
@ -983,5 +1019,7 @@ mutual
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
|
||||
displayErrors (ErrorLoadingFile x err) = printError $ "File error in " ++ x ++ ": " ++ show err
|
||||
displayErrors (ErrorLoadingFile x err) = do
|
||||
msg <- render (reflow "File error in" <++> pretty x <+> colon <++> pretty (show err))
|
||||
printError msg
|
||||
displayErrors _ = pure ()
|
||||
|
||||
@ -61,12 +61,10 @@ emitError err
|
||||
= do opts <- get ROpts
|
||||
case idemode opts of
|
||||
REPL _ =>
|
||||
do pmsg <- reAnnotate colorAnn <$> display err
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
do msg <- display err >>= render
|
||||
coreLift $ putStrLn msg
|
||||
IDEMode i _ f =>
|
||||
do pmsg <- reAnnotate colorAnn <$> perror err
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
do msg <- perror err >>= renderWithoutColor
|
||||
case getErrorLoc err of
|
||||
Nothing => iputStrLn msg
|
||||
Just fc =>
|
||||
@ -91,12 +89,10 @@ emitWarning w
|
||||
= do opts <- get ROpts
|
||||
case idemode opts of
|
||||
REPL _ =>
|
||||
do pmsg <- reAnnotate colorAnn <$> displayWarning w
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
do msg <- displayWarning w >>= render
|
||||
coreLift $ putStrLn msg
|
||||
IDEMode i _ f =>
|
||||
do pmsg <- reAnnotate colorAnn <$> pwarning w
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
do msg <- pwarning w >>= renderWithoutColor
|
||||
case getWarningLoc w of
|
||||
Nothing => iputStrLn msg
|
||||
Just fc =>
|
||||
|
||||
@ -34,12 +34,14 @@ record REPLOpts where
|
||||
-- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
|
||||
-- better to stick it now.
|
||||
extraCodegens : List (String, Codegen)
|
||||
consoleWidth : Nat
|
||||
color : Bool
|
||||
|
||||
export
|
||||
defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
|
||||
defaultOpts fname outmode cgs
|
||||
= MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim"
|
||||
Nothing outmode "" Nothing Nothing cgs
|
||||
Nothing outmode "" Nothing Nothing cgs 120 True
|
||||
where
|
||||
litStyle : Maybe String -> Maybe LiterateStyle
|
||||
litStyle Nothing = Nothing
|
||||
@ -141,3 +143,23 @@ getCodegen : {auto o : Ref ROpts REPLOpts} ->
|
||||
String -> Core (Maybe Codegen)
|
||||
getCodegen s = do opts <- get ROpts
|
||||
pure $ lookup s (extraCodegens opts)
|
||||
|
||||
export
|
||||
getConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Core Nat
|
||||
getConsoleWidth = do opts <- get ROpts
|
||||
pure $ opts.consoleWidth
|
||||
|
||||
export
|
||||
setConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Nat -> Core ()
|
||||
setConsoleWidth n = do opts <- get ROpts
|
||||
put ROpts (record { consoleWidth = n } opts)
|
||||
|
||||
export
|
||||
getColor : {auto o : Ref ROpts REPLOpts} -> Core Bool
|
||||
getColor = do opts <- get ROpts
|
||||
pure $ opts.color
|
||||
|
||||
export
|
||||
setColor : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
|
||||
setColor b = do opts <- get ROpts
|
||||
put ROpts (record { color = b } opts)
|
||||
|
||||
@ -118,6 +118,12 @@ preOptions (DumpVMCode f :: opts)
|
||||
preOptions (Logging n :: opts)
|
||||
= do setSession (record { logLevel = n } !getSession)
|
||||
preOptions opts
|
||||
preOptions (ConsoleWidth n :: opts)
|
||||
= do setConsoleWidth n
|
||||
preOptions opts
|
||||
preOptions (Color b :: opts)
|
||||
= do setColor b
|
||||
preOptions opts
|
||||
preOptions (_ :: opts) = preOptions opts
|
||||
|
||||
-- Options to be processed after type checking. Returns whether execution
|
||||
|
||||
@ -15,6 +15,8 @@ import Data.ANameMap
|
||||
import Data.List
|
||||
import Data.NameMap
|
||||
import Data.StringMap
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
|
||||
%default covering
|
||||
|
||||
@ -360,6 +362,12 @@ Show REPLEval where
|
||||
show NormaliseAll = "normalise"
|
||||
show Execute = "execute"
|
||||
|
||||
export
|
||||
Pretty REPLEval where
|
||||
pretty EvalTC = pretty "typecheck"
|
||||
pretty NormaliseAll = pretty "normalise"
|
||||
pretty Execute = pretty "execute"
|
||||
|
||||
public export
|
||||
data REPLOpt : Type where
|
||||
ShowImplicits : Bool -> REPLOpt
|
||||
@ -378,6 +386,14 @@ Show REPLOpt where
|
||||
show (Editor editor) = "editor = " ++ show editor
|
||||
show (CG str) = "cg = " ++ str
|
||||
|
||||
export
|
||||
Pretty REPLOpt where
|
||||
pretty (ShowImplicits impl) = pretty "showimplicits" <++> equals <++> pretty impl
|
||||
pretty (ShowNamespace ns) = pretty "shownamespace" <++> equals <++> pretty ns
|
||||
pretty (ShowTypes typs) = pretty "showtypes" <++> equals <++> pretty typs
|
||||
pretty (EvalMode mod) = pretty "eval" <++> equals <++> pretty mod
|
||||
pretty (Editor editor) = pretty "editor" <++> equals <++> pretty editor
|
||||
pretty (CG str) = pretty "cg" <++> equals <++> pretty str
|
||||
|
||||
public export
|
||||
data EditCmd : Type where
|
||||
@ -417,6 +433,8 @@ data REPLCmd : Type where
|
||||
Doc : Name -> REPLCmd
|
||||
Browse : List String -> REPLCmd
|
||||
SetLog : Nat -> REPLCmd
|
||||
SetConsoleWidth : Nat -> REPLCmd
|
||||
SetColor : Bool -> REPLCmd
|
||||
Metavars : REPLCmd
|
||||
Editing : EditCmd -> REPLCmd
|
||||
ShowVersion : REPLCmd
|
||||
|
||||
@ -70,6 +70,15 @@ intLit
|
||||
IntegerLit i => Just i
|
||||
_ => Nothing)
|
||||
|
||||
export
|
||||
onOffLit : Rule Bool
|
||||
onOffLit
|
||||
= terminal "Expected on or off"
|
||||
(\x => case tok x of
|
||||
Ident "on" => Just True
|
||||
Ident "off" => Just False
|
||||
_ => Nothing)
|
||||
|
||||
export
|
||||
strLit : Rule String
|
||||
strLit
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Total.idr < input
|
||||
$1 --no-color --no-banner Total.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,2 +1,2 @@
|
||||
$1 --no-banner Pythag.idr < input
|
||||
$1 --no-color --no-banner Pythag.idr < input
|
||||
rm -rf build
|
||||
|
||||
@ -1,2 +1,2 @@
|
||||
$1 --no-banner IORef.idr < input
|
||||
$1 --no-color --no-banner IORef.idr < input
|
||||
rm -rf build
|
||||
|
||||
@ -1,2 +1,2 @@
|
||||
$1 -p contrib --no-banner Buffer.idr < input
|
||||
$1 --no-color -p contrib --no-banner Buffer.idr < input
|
||||
rm -rf build test.buf
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Filter.idr < input
|
||||
$1 --no-color --no-banner Filter.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -15,13 +15,17 @@ Main> Main.strangeId':
|
||||
strangeId' _
|
||||
Main> Bye for now!
|
||||
1/1: Building TypeCase2 (TypeCase2.idr)
|
||||
TypeCase2.idr:5:14--5:17:While processing left hand side
|
||||
of strangeId at TypeCase2.idr:5:1--6:1:
|
||||
Can't match on Nat (Erased argument) at:
|
||||
Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument).
|
||||
|
||||
TypeCase2.idr:5:14--5:17
|
||||
|
|
||||
5 | strangeId {a=Nat} x = x+1
|
||||
^^^
|
||||
TypeCase2.idr:9:5--9:8:While processing left hand side
|
||||
of foo at TypeCase2.idr:9:1--10:1:
|
||||
Can't match on Nat (Erased argument) at:
|
||||
| ^^^
|
||||
|
||||
Error: While processing left hand side of foo. Can't match on Nat (Erased argument).
|
||||
|
||||
TypeCase2.idr:9:5--9:8
|
||||
|
|
||||
9 | foo Nat = "Nat"
|
||||
^^^
|
||||
| ^^^
|
||||
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
$1 --no-banner TypeCase.idr < input
|
||||
$1 --no-banner TypeCase2.idr --check
|
||||
$1 --no-color --no-banner TypeCase.idr < input
|
||||
$1 --no-color --no-banner TypeCase2.idr --check
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner TypeCase.idr < input
|
||||
$1 --no-color --no-banner TypeCase.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Nat.idr < input
|
||||
$1 --no-color --no-banner Nat.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner uni.idr < input
|
||||
$1 --no-color --no-banner uni.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -9,6 +9,6 @@ case `uname -s` in
|
||||
esac
|
||||
|
||||
${MAKE} all > /dev/null
|
||||
$1 --no-banner CB.idr < input
|
||||
$1 --no-color --no-banner CB.idr < input
|
||||
rm -rf build
|
||||
${MAKE} clean > /dev/null
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner bangs.idr < input
|
||||
$1 --no-color --no-banner bangs.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,2 +1,2 @@
|
||||
$1 --no-banner array.idr < input
|
||||
$1 --no-color --no-banner array.idr < input
|
||||
rm -rf build
|
||||
|
||||
@ -9,6 +9,6 @@ case `uname -s` in
|
||||
esac
|
||||
|
||||
${MAKE} all > /dev/null
|
||||
$1 --no-banner Struct.idr < input
|
||||
$1 --no-color --no-banner Struct.idr < input
|
||||
rm -rf build
|
||||
${MAKE} clean > /dev/null
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner -p network Echo.idr < input
|
||||
$1 --no-color --no-banner -p network Echo.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Numbers.idr < input
|
||||
$1 --no-color --no-banner Numbers.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -16,5 +16,5 @@ IDRIS2_EXEC="$(basename "$1")"
|
||||
|
||||
cd "folder with spaces" || exit
|
||||
|
||||
"$IDRIS2_DIR/$IDRIS2_EXEC" --no-banner Main.idr < ../input
|
||||
"$IDRIS2_DIR/$IDRIS2_EXEC" --no-color --no-banner Main.idr < ../input
|
||||
rm -rf build
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
./gen_expected.sh
|
||||
$1 --no-banner dir.idr < input
|
||||
$1 --no-color --no-banner dir.idr < input
|
||||
cat testdir/test.txt
|
||||
rm -rf build testdir
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner File.idr < input
|
||||
$1 --no-color --no-banner File.idr < input
|
||||
|
||||
rm -rf build testout.txt
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner partial.idr < input
|
||||
$1 --no-color --no-banner partial.idr < input
|
||||
|
||||
rm -rf build testout.txt
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
POPEN_CMD="$1 --version" $1 --no-banner Popen.idr < input
|
||||
POPEN_CMD="$1 --version" $1 --no-color --no-banner Popen.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Bits.idr < input
|
||||
$1 --no-color --no-banner Bits.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -9,6 +9,6 @@ case `uname -s` in
|
||||
esac
|
||||
|
||||
${MAKE} all > /dev/null
|
||||
$1 --no-banner usealloc.idr < input
|
||||
$1 --no-color --no-banner usealloc.idr < input
|
||||
rm -rf build
|
||||
${MAKE} clean > /dev/null
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner File.idr < input
|
||||
$1 --no-color --no-banner File.idr < input
|
||||
|
||||
rm -rf build test.txt
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Envy.idr < input
|
||||
$1 --no-color --no-banner Envy.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner runst.idr < input
|
||||
$1 --no-color --no-banner runst.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -10,6 +10,7 @@ modules = Dummy
|
||||
|
||||
main = Dummy
|
||||
executable = check_dir
|
||||
opts = "--no-color"
|
||||
|
||||
builddir = "custom_build"
|
||||
outputdir = "custom_output"
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner -p contrib StringParser.idr < input
|
||||
$1 --no-color --no-banner -p contrib StringParser.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 numbers.idr -x main
|
||||
$1 --no-color numbers.idr -x main
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --ide-mode < input
|
||||
$1 --no-color --ide-mode < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
$1 --version | awk '{print $4}' | ./gen_expected.sh
|
||||
$1 --ide-mode < input
|
||||
$1 --no-color --version | awk '{print $4}' | ./gen_expected.sh
|
||||
$1 --no-color --ide-mode < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --ide-mode < input
|
||||
$1 --no-color --ide-mode < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner -p idris2 -p contrib -p network LazyCodegen.idr -o lazy-idris2 > /dev/null
|
||||
./build/exec/lazy-idris2 --no-banner --cg lazy Hello.idr -o hello
|
||||
$1 --no-color --no-banner -p idris2 -p contrib -p network LazyCodegen.idr -o lazy-idris2 > /dev/null
|
||||
./build/exec/lazy-idris2 --no-color --no-banner --cg lazy Hello.idr -o hello
|
||||
rm -rf build
|
||||
@ -1,11 +1,11 @@
|
||||
1/1: Building Vect (Vect.idr)
|
||||
Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
|
||||
Main> (interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat
|
||||
Mismatch between:
|
||||
S Z
|
||||
and
|
||||
Z
|
||||
at:
|
||||
Main> Error: When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat.
|
||||
Mismatch between: S Z and Z.
|
||||
|
||||
(interactive):1:28--1:51
|
||||
|
|
||||
1 | zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
|
||||
^^^^^^^^^^^^^^^^^^^^^^^
|
||||
| ^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude Vect.idr < input
|
||||
$1 --no-color --no-banner --no-prelude Vect.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude Do.idr < input
|
||||
$1 --no-color --no-banner --no-prelude Do.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,12 +1,13 @@
|
||||
1/1: Building Ambig1 (Ambig1.idr)
|
||||
Main> Bye for now!
|
||||
1/1: Building Ambig2 (Ambig2.idr)
|
||||
Ambig2.idr:26:21--26:27:While processing right hand side
|
||||
of keepUnique at Ambig2.idr:26:1--28:1:
|
||||
Ambiguous elaboration at:
|
||||
26 | keepUnique {b} xs = toList (fromList xs)
|
||||
^^^^^^
|
||||
Possible correct results:
|
||||
Error: While processing right hand side of keepUnique. Ambiguous elaboration. Possible results:
|
||||
Main.Set.toList ?arg
|
||||
Main.Vect.toList ?arg
|
||||
|
||||
Ambig2.idr:26:21--26:27
|
||||
|
|
||||
26 | keepUnique {b} xs = toList (fromList xs)
|
||||
| ^^^^^^
|
||||
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
echo ':q' | $1 --no-banner --no-prelude Ambig1.idr
|
||||
echo ':q' | $1 --no-banner --no-prelude Ambig2.idr
|
||||
echo ':q' | $1 --no-color --no-banner --no-prelude Ambig1.idr
|
||||
echo ':q' | $1 --no-color --no-banner --no-prelude Ambig2.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude Wheres.idr < input
|
||||
$1 --no-color --no-banner --no-prelude Wheres.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,5 +1,9 @@
|
||||
1/1: Building NoInfer (NoInfer.idr)
|
||||
NoInfer.idr:1:7--1:8:Unsolved holes:
|
||||
Main.{_:1} introduced at NoInfer.idr:1:7--1:8
|
||||
Error: unsolved holes:
|
||||
Main.{_:1} introduced at:
|
||||
NoInfer.idr:1:7--1:8
|
||||
|
|
||||
1 | foo : ? -> Int
|
||||
| ^
|
||||
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
echo ':q' | $1 --no-banner --no-prelude NoInfer.idr
|
||||
echo ':q' | $1 --no-color --no-banner --no-prelude NoInfer.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude PMLet.idr < input
|
||||
$1 --no-color --no-banner --no-prelude PMLet.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude DoLocal.idr < input
|
||||
$1 --no-color --no-banner --no-prelude DoLocal.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude If.idr < input
|
||||
$1 --no-color --no-banner --no-prelude If.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude LetCase.idr < input
|
||||
$1 --no-color --no-banner --no-prelude LetCase.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner --no-prelude Comp.idr < input
|
||||
$1 --no-color --no-banner --no-prelude Comp.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,14 +1,17 @@
|
||||
1/1: Building Dots1 (Dots1.idr)
|
||||
1/1: Building Dots2 (Dots2.idr)
|
||||
Dots2.idr:2:7--2:8:While processing left hand side of foo at Dots2.idr:2:1--4:1:
|
||||
Can't match on ?x [no locals in scope] (Non linear pattern variable) at:
|
||||
Error: While processing left hand side of foo. Can't match on ?x [no locals in scope] (Non linear pattern variable).
|
||||
|
||||
Dots2.idr:2:7--2:8
|
||||
|
|
||||
2 | foo x x = x + x
|
||||
^
|
||||
| ^
|
||||
|
||||
1/1: Building Dots3 (Dots3.idr)
|
||||
Dots3.idr:5:29--5:30:While processing left hand side
|
||||
of addBaz at Dots3.idr:5:1--6:1:
|
||||
Pattern variable z unifies with:
|
||||
?y [no locals in scope]
|
||||
at:
|
||||
Error: While processing left hand side of addBaz. Pattern variable z unifies with: ?y [no locals in scope].
|
||||
|
||||
Dots3.idr:5:29--5:30
|
||||
|
|
||||
5 | addBaz (x + y) (AddThings x z) = x + y
|
||||
^
|
||||
| ^
|
||||
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
$1 --check Dots1.idr
|
||||
$1 --check Dots2.idr
|
||||
$1 --check Dots3.idr
|
||||
$1 --no-color --check Dots1.idr
|
||||
$1 --no-color --check Dots2.idr
|
||||
$1 --no-color --check Dots3.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check VIndex.idr
|
||||
$1 --no-color --check VIndex.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check Implicits.idr
|
||||
$1 --no-color --check Implicits.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,11 +1,16 @@
|
||||
1/1: Building Rewrite (Rewrite.idr)
|
||||
Rewrite.idr:15:25--15:57:While processing right hand side
|
||||
of wrongCommutes at Rewrite.idr:15:1--17:1:
|
||||
Rewriting by m + k = k + m did not change type S k + m = m + S k at:
|
||||
Error: While processing right hand side of wrongCommutes. Rewriting by m + k = k + m did not change
|
||||
type S k + m = m + S k.
|
||||
|
||||
Rewrite.idr:15:25--15:57
|
||||
|
|
||||
15 | wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
Rewrite.idr:19:26--19:43:While processing right hand side
|
||||
of wrongCommutes2 at Rewrite.idr:19:1--20:1:
|
||||
Nat is not a rewrite rule type at:
|
||||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
Error: While processing right hand side of wrongCommutes2. Nat is not a rewrite rule type.
|
||||
|
||||
Rewrite.idr:19:26--19:43
|
||||
|
|
||||
19 | wrongCommutes2 (S k) m = rewrite m in ?bar
|
||||
^^^^^^^^^^^^^^^^^
|
||||
| ^^^^^^^^^^^^^^^^^
|
||||
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check Rewrite.idr
|
||||
$1 --no-color --check Rewrite.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check George.idr
|
||||
$1 --no-color --check George.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,33 +1,27 @@
|
||||
1/1: Building Eta (Eta.idr)
|
||||
Eta.idr:14:10--14:14:While processing right hand side
|
||||
of etaBad at Eta.idr:14:1--15:1:
|
||||
When
|
||||
unifying \x => (\y => (MkTest ?_ ?_)) = \x => (\y => (MkTest ?_ ?_)) and MkTest = \x => (\y => (MkTest ?_ ?_))
|
||||
Mismatch between:
|
||||
Nat
|
||||
and
|
||||
Integer
|
||||
at:
|
||||
Error: While processing right hand side of etaBad. When
|
||||
unifying \x => (\y => (MkTest ?_ ?_)) = \x => (\y => (MkTest ?_ ?_)) and MkTest = \x => (\y => (MkTest ?_ ?_)).
|
||||
Mismatch between: Nat and Int.
|
||||
|
||||
Eta.idr:14:10--14:14
|
||||
|
|
||||
14 | etaBad = Refl
|
||||
^^^^
|
||||
| ^^^^
|
||||
|
||||
1/1: Building Eta2 (Eta2.idr)
|
||||
Eta2.idr:2:8--2:12:While processing right hand side
|
||||
of test at Eta2.idr:2:1--4:1:
|
||||
When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_)
|
||||
Mismatch between:
|
||||
a
|
||||
and
|
||||
Nat
|
||||
at:
|
||||
Error: While processing right hand side of test. When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_).
|
||||
Mismatch between: a and Nat.
|
||||
|
||||
Eta2.idr:2:8--2:12
|
||||
|
|
||||
2 | test = Refl
|
||||
^^^^
|
||||
Eta2.idr:5:44--5:48:While processing right hand side
|
||||
of test2 at Eta2.idr:5:1--6:1:
|
||||
When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_)
|
||||
Mismatch between:
|
||||
a
|
||||
and
|
||||
Nat
|
||||
at:
|
||||
| ^^^^
|
||||
|
||||
Error: While processing right hand side of test2. When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_).
|
||||
Mismatch between: a and Nat.
|
||||
|
||||
Eta2.idr:5:44--5:48
|
||||
|
|
||||
5 | test2 = {a : _} -> the (S = \x : a => S _) Refl
|
||||
^^^^
|
||||
| ^^^^
|
||||
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
$1 --check Eta.idr
|
||||
$1 --check Eta2.idr
|
||||
$1 --no-color --check Eta.idr
|
||||
$1 --no-color --check Eta2.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner CaseInf.idr < input
|
||||
$1 --no-color --no-banner CaseInf.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,6 +1,8 @@
|
||||
1/1: Building Fin (Fin.idr)
|
||||
Fin.idr:34:7--34:8:While processing right hand side
|
||||
of bar at Fin.idr:34:1--36:1:
|
||||
Can't find an implementation for IsJust (integerToFin 8 5) at:
|
||||
Error: While processing right hand side of bar. Can't find an implementation for IsJust (integerToFin 8 5).
|
||||
|
||||
Fin.idr:34:7--34:8
|
||||
|
|
||||
34 | bar = 8
|
||||
^
|
||||
| ^
|
||||
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check Fin.idr
|
||||
$1 --no-color --check Fin.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner CaseBlock.idr < input
|
||||
$1 --no-color --no-banner CaseBlock.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Mut.idr < input
|
||||
$1 --no-color --no-banner Mut.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner CaseDep.idr < input
|
||||
$1 --no-color --no-banner CaseDep.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,13 +1,17 @@
|
||||
1/1: Building Erase (Erase.idr)
|
||||
Erase.idr:5:5--5:10:While processing left hand side
|
||||
of bad at Erase.idr:5:1--6:1:
|
||||
Can't match on False (Erased argument) at:
|
||||
Error: While processing left hand side of bad. Can't match on False (Erased argument).
|
||||
|
||||
Erase.idr:5:5--5:10
|
||||
|
|
||||
5 | bad False = True
|
||||
^^^^^
|
||||
Erase.idr:19:18--19:21:While processing left hand side
|
||||
of minusBad at Erase.idr:19:1--20:1:
|
||||
Can't match on LeZ (Erased argument) at:
|
||||
| ^^^^^
|
||||
|
||||
Error: While processing left hand side of minusBad. Can't match on LeZ (Erased argument).
|
||||
|
||||
Erase.idr:19:18--19:21
|
||||
|
|
||||
19 | minusBad (S k) Z LeZ = S k
|
||||
^^^
|
||||
| ^^^
|
||||
|
||||
Main> \m => minus (S (S m)) m prf
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Erase.idr < input
|
||||
$1 --no-color --no-banner Erase.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Params.idr < input
|
||||
$1 --no-color --no-banner Params.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner PatLam.idr < input
|
||||
$1 --no-color --no-banner PatLam.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner < input
|
||||
$1 --no-color --no-banner < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check Erl.idr
|
||||
$1 --no-color --check Erl.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check Temp.idr
|
||||
$1 --no-color --check Temp.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
unset IDRIS2_PATH
|
||||
|
||||
$1 --no-banner --no-prelude < input
|
||||
$1 --no-color --no-banner --no-prelude < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Params.idr < input
|
||||
$1 --no-color --no-banner Params.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,11 +1,9 @@
|
||||
1/1: Building arity (arity.idr)
|
||||
arity.idr:4:16--4:21:While processing right hand side
|
||||
of foo at arity.idr:4:1--7:1:
|
||||
When unifying (1 _ : Nat) -> MyN and MyN
|
||||
Mismatch between:
|
||||
(1 _ : Nat) -> MyN
|
||||
and
|
||||
MyN
|
||||
at:
|
||||
Error: While processing right hand side of foo. When unifying (1 _ : Nat) -> MyN and MyN.
|
||||
Mismatch between: (1 _ : Nat) -> MyN and MyN.
|
||||
|
||||
arity.idr:4:16--4:21
|
||||
|
|
||||
4 | foo x y = case MkN x of
|
||||
^^^^^
|
||||
| ^^^^^
|
||||
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check arity.idr
|
||||
$1 --no-color --check arity.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,6 +1,8 @@
|
||||
1/1: Building erased (erased.idr)
|
||||
erased.idr:7:17--7:21:While processing left hand side
|
||||
of nameOf at erased.idr:7:1--8:1:
|
||||
Can't match on Bool (Erased argument) at:
|
||||
Error: While processing left hand side of nameOf. Can't match on Bool (Erased argument).
|
||||
|
||||
erased.idr:7:17--7:21
|
||||
|
|
||||
7 | nameOf (MyMaybe Bool) = "MyMaybe Bool"
|
||||
^^^^
|
||||
| ^^^^
|
||||
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check erased.idr
|
||||
$1 --no-color --check erased.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Idiom.idr < input
|
||||
$1 --no-color --no-banner Idiom.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,11 +1,15 @@
|
||||
1/1: Building unboundimps (unboundimps.idr)
|
||||
unboundimps.idr:18:11--18:13:While processing type
|
||||
of len' at unboundimps.idr:18:1--18:20:
|
||||
Undefined name xs at:
|
||||
Error: While processing type of len'. Undefined name xs.
|
||||
|
||||
unboundimps.idr:18:11--18:13
|
||||
|
|
||||
18 | len': Env xs -> Nat
|
||||
^^
|
||||
unboundimps.idr:19:16--19:17:While processing type
|
||||
of append' at unboundimps.idr:19:1--19:49:
|
||||
Undefined name n at:
|
||||
| ^^
|
||||
|
||||
Error: While processing type of append'. Undefined name n.
|
||||
|
||||
unboundimps.idr:19:16--19:17
|
||||
|
|
||||
19 | append' : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
^
|
||||
| ^
|
||||
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check unboundimps.idr
|
||||
$1 --no-color --check unboundimps.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,11 +1,9 @@
|
||||
1/1: Building lets (lets.idr)
|
||||
lets.idr:22:39--22:40:While processing right hand side
|
||||
of dolet2 at lets.idr:21:1--26:1:
|
||||
When unifying Maybe Int and Maybe String
|
||||
Mismatch between:
|
||||
Int
|
||||
and
|
||||
String
|
||||
at:
|
||||
Error: While processing right hand side of dolet2. When unifying Maybe Int and Maybe String.
|
||||
Mismatch between: Int and String.
|
||||
|
||||
lets.idr:22:39--22:40
|
||||
|
|
||||
22 | = do let Just x' : Maybe String = x
|
||||
^
|
||||
| ^
|
||||
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check lets.idr
|
||||
$1 --no-color --check lets.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner using.idr < input
|
||||
$1 --no-color --no-banner using.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner defimp.idr < input
|
||||
$1 --no-color --no-banner defimp.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
echo ':q' | $1 --no-banner --no-prelude Comments.idr
|
||||
echo ':q' | $1 --no-banner Issue279.idr
|
||||
echo ':q' | $1 --no-color --no-banner --no-prelude Comments.idr
|
||||
echo ':q' | $1 --no-color --no-banner Issue279.idr
|
||||
|
||||
rm -rf build
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Resugar.idr < input
|
||||
$1 --no-color --no-banner Resugar.idr < input
|
||||
|
||||
rm -rf build
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Main.idr < input
|
||||
$1 --no-color --no-banner Main.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
echo ":q" | $1 --no-banner Default.idr
|
||||
echo ":q" | $1 --no-color --no-banner Default.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --check QDo.idr
|
||||
$1 --no-color --check QDo.idr
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Vect.idr < input
|
||||
$1 --no-color --no-banner Vect.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
$1 --no-banner Vect.idr < input
|
||||
$1 --no-color --no-banner Vect.idr < input
|
||||
|
||||
rm -rf build
|
||||
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user