mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-23 22:22:07 +03:00
PTerm and error intial prettyprinting
This commit is contained in:
Giuseppe Lomurno
G. Allais
parent
63b8504e42
commit
df4f990b3c
@ -77,6 +77,7 @@ modules =
|
||||
Idris.ModTree,
|
||||
Idris.Package,
|
||||
Idris.Parser,
|
||||
Idris.Pretty,
|
||||
Idris.ProcessIdr,
|
||||
Idris.REPL,
|
||||
Idris.REPLCommon,
|
||||
|
||||
@ -2,7 +2,7 @@ module Text.PrettyPrint.Prettyprinter.Render.Terminal
|
||||
|
||||
import Data.Maybe
|
||||
import Data.Strings
|
||||
import Control.ANSI
|
||||
import public Control.ANSI
|
||||
import Control.Monad.ST
|
||||
import Text.PrettyPrint.Prettyprinter.Doc
|
||||
|
||||
@ -39,7 +39,7 @@ strike = pure $ SetStyle Striked
|
||||
export
|
||||
renderString : SimpleDocStream AnsiStyle -> String
|
||||
renderString sdoc = fromMaybe "<internal pretty printing error>" $ runST $ do
|
||||
styleStackRef <- newSTRef {a = List (List SGR)} [neutral]
|
||||
styleStackRef <- newSTRef {a = List AnsiStyle} [neutral]
|
||||
outputRef <- newSTRef {a = String} neutral
|
||||
go styleStackRef outputRef sdoc
|
||||
readSTRef styleStackRef >>= \case
|
||||
|
||||
@ -1,5 +1,7 @@
|
||||
module Core.FC
|
||||
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
@ -71,4 +73,11 @@ Show FC where
|
||||
showPos (startPos loc) ++ "--" ++
|
||||
showPos (endPos loc)
|
||||
|
||||
|
||||
export
|
||||
Pretty FC where
|
||||
pretty loc = pretty (file loc) <+> colon
|
||||
<+> prettyPos (startPos loc) <+> pretty "--"
|
||||
<+> prettyPos (endPos loc)
|
||||
where
|
||||
prettyPos : FilePos -> Doc ann
|
||||
prettyPos (l, c) = pretty (l + 1) <+> colon <+> pretty (c + 1)
|
||||
|
||||
@ -2,6 +2,8 @@ module Core.Name
|
||||
|
||||
import Data.List
|
||||
import Decidable.Equality
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
|
||||
%default total
|
||||
|
||||
@ -87,6 +89,18 @@ Show Name where
|
||||
show (WithBlock outer i) = "with block in " ++ outer
|
||||
show (Resolved x) = "$resolved" ++ show x
|
||||
|
||||
export
|
||||
Pretty Name where
|
||||
pretty (NS ns n) = concatWith (surround dot) (pretty <$> reverse ns) <+> dot <+> pretty n
|
||||
pretty (UN x) = pretty x
|
||||
pretty (MN x y) = braces (pretty x <+> colon <+> pretty y)
|
||||
pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d)
|
||||
pretty (DN str _) = pretty str
|
||||
pretty (Nested (outer, idx) inner) = pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner
|
||||
pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
|
||||
pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
|
||||
pretty (Resolved x) = pretty "$resolved" <+> pretty x
|
||||
|
||||
export
|
||||
Eq Name where
|
||||
(==) (NS ns n) (NS ns' n') = n == n' && ns == ns'
|
||||
|
||||
@ -8,6 +8,7 @@ import Data.List
|
||||
import Data.NameMap
|
||||
import Data.Vect
|
||||
import Decidable.Equality
|
||||
import Text.PrettyPrint.PrettyPrinter
|
||||
|
||||
import public Algebra
|
||||
|
||||
@ -92,6 +93,29 @@ Show Constant where
|
||||
show DoubleType = "Double"
|
||||
show WorldType = "%World"
|
||||
|
||||
export
|
||||
Pretty Constant where
|
||||
pretty (I x) = pretty x
|
||||
pretty (BI x) = pretty x
|
||||
pretty (B8 x) = pretty x
|
||||
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 (Db x) = pretty x
|
||||
pretty WorldVal = pretty "%MkWorld"
|
||||
pretty IntType = pretty "Int"
|
||||
pretty IntegerType = pretty "Int"
|
||||
pretty Bits8Type = pretty "Bits8"
|
||||
pretty Bits16Type = pretty "Bits16"
|
||||
pretty Bits32Type = pretty "Bits32"
|
||||
pretty Bits64Type = pretty "Bits64"
|
||||
pretty StringType = pretty "String"
|
||||
pretty CharType = pretty "Char"
|
||||
pretty DoubleType = pretty "Double"
|
||||
pretty WorldType = pretty "%World"
|
||||
|
||||
export
|
||||
Eq Constant where
|
||||
(I x) == (I y) = x == y
|
||||
|
||||
@ -10,6 +10,7 @@ import Core.Value
|
||||
import Idris.REPLOpts
|
||||
import Idris.Resugar
|
||||
import Idris.Syntax
|
||||
import Idris.Pretty
|
||||
|
||||
import Parser.Source
|
||||
|
||||
@ -18,6 +19,9 @@ import Data.List.Extra
|
||||
import Data.Maybe
|
||||
import Data.Stream
|
||||
import Data.Strings
|
||||
import Data.String.Extra
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
import System.File
|
||||
|
||||
%default covering
|
||||
@ -25,148 +29,187 @@ import System.File
|
||||
pshow : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
Env Term vars -> Term vars -> Core String
|
||||
Env Term vars -> Term vars -> Core (Doc IdrisAnn)
|
||||
pshow env tm
|
||||
= do defs <- get Ctxt
|
||||
itm <- resugar env !(normaliseHoles defs env tm)
|
||||
pure (show itm)
|
||||
pure (prettyTerm itm)
|
||||
|
||||
pshowNoNorm : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
Env Term vars -> Term vars -> Core String
|
||||
Env Term vars -> Term vars -> Core (Doc IdrisAnn)
|
||||
pshowNoNorm env tm
|
||||
= do defs <- get Ctxt
|
||||
itm <- resugar env tm
|
||||
pure (show itm)
|
||||
pure (prettyTerm itm)
|
||||
|
||||
ploc : {auto o : Ref ROpts REPLOpts} ->
|
||||
FC -> Core String
|
||||
ploc EmptyFC = pure ""
|
||||
FC -> Core (Doc IdrisAnn)
|
||||
ploc EmptyFC = pure emptyDoc
|
||||
ploc (MkFC _ s e) = do
|
||||
let sr = integerToNat $ cast $ fst s
|
||||
let sc = integerToNat $ cast $ snd s
|
||||
let er = integerToNat $ cast $ fst e
|
||||
let ec = integerToNat $ cast $ snd e
|
||||
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)
|
||||
source <- lines <$> getCurrentElabSource
|
||||
pure $ if sr == er
|
||||
then show (sr + 1) ++ "\t" ++ fromMaybe "" (elemAt source sr)
|
||||
++ "\n\t" ++ repeatChar sc ' ' ++ repeatChar (ec `minus` sc) '^' ++ "\n"
|
||||
else addLineNumbers sr $ extractRange sr er source
|
||||
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))
|
||||
where
|
||||
extractRange : Nat -> Nat -> List a -> List a
|
||||
extractRange : Nat -> Nat -> List String -> List String
|
||||
extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
|
||||
repeatChar : Nat -> Char -> String
|
||||
repeatChar n c = pack $ take n (repeat c)
|
||||
addLineNumbers : Nat -> List String -> String
|
||||
addLineNumbers st xs = snd $ foldl (\(i, s), l => (S i, s ++ show (i + 1) ++ "\t" ++ l ++ "\n")) (st, "") xs
|
||||
pad : Nat -> String -> String
|
||||
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
|
||||
|
||||
export
|
||||
perror : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
Error -> Core String
|
||||
Error -> Core (Doc IdrisAnn)
|
||||
perror (Fatal err) = perror err
|
||||
perror (CantConvert fc env l r)
|
||||
= pure $ "Mismatch between:\n\t" ++ !(pshow env l) ++ "\nand\n\t" ++ !(pshow env r) ++ "\nat:\n" ++ !(ploc fc)
|
||||
= pure $ vsep [ reflow "Mismatch between" <+> colon
|
||||
, indent 4 !(pshow env l)
|
||||
, pretty "and"
|
||||
, indent 4 !(pshow env r)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
perror (CantSolveEq fc env l r)
|
||||
= pure $ "Can't solve constraint between:\n\t" ++ !(pshow env l) ++
|
||||
"\nand\n\t" ++ !(pshow env r) ++ "\nat:\n" ++ !(ploc fc)
|
||||
= pure $ vsep [ reflow "Can't solve constraint between" <+> colon
|
||||
, indent 4 !(pshow env l)
|
||||
, pretty "and"
|
||||
, indent 4 !(pshow env r)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
perror (PatternVariableUnifies fc env n tm)
|
||||
= pure $ "Pattern variable " ++ showPVar n ++
|
||||
" unifies with:\n\t" ++ !(pshow env tm) ++ "\nat:\n" ++ !(ploc fc)
|
||||
= pure $ vsep [ reflow "Pattern variable" <++> pretty (showPVar n) <++> reflow "unifies with" <+> colon
|
||||
, indent 4 !(pshow env tm)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
where
|
||||
showPVar : Name -> String
|
||||
showPVar (PV n _) = showPVar n
|
||||
showPVar n = show n
|
||||
perror (CyclicMeta fc env n tm)
|
||||
= pure $ "Cycle detected in solution of metavariable "
|
||||
++ show !(prettyName n) ++ " = "
|
||||
++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Cycle detected in solution of metavariable" <++> pretty !(prettyName n) <++> equals
|
||||
<++> !(pshow env tm) <++> pretty "at" <+> colon <+> line
|
||||
<+> !(ploc fc)
|
||||
perror (WhenUnifying _ env x y err)
|
||||
= pure $ "When unifying " ++ !(pshow env x) ++ " and " ++ !(pshow env y) ++ "\n"
|
||||
++ !(perror err)
|
||||
= pure $ reflow "When unifying" <++> !(pshow env x) <++> pretty "and"
|
||||
<++> !(pshow env y) <+> line
|
||||
<+> !(perror err)
|
||||
perror (ValidCase fc env (Left tm))
|
||||
= pure $ !(pshow env tm) ++ " is not a valid impossible case at:\n" ++ !(ploc fc)
|
||||
= pure $ !(pshow env tm) <++> reflow "is not a valid impossible case at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
perror (ValidCase _ env (Right err))
|
||||
= pure $ "Impossible pattern gives an error:\n" ++ !(perror err)
|
||||
perror (UndefinedName fc x) = pure $ "Undefined name " ++ show x ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ 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)
|
||||
perror (InvisibleName fc n (Just ns))
|
||||
= pure $ "Name " ++ show n ++ " is inaccessible since " ++
|
||||
showSep "." (reverse ns) ++ " is not explicitly imported at:\n" ++ !(ploc fc)
|
||||
= 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)
|
||||
perror (InvisibleName fc x Nothing)
|
||||
= pure $ "Name " ++ show x ++ " is private at:\n" ++ !(ploc fc)
|
||||
= pure $ pretty "Name" <++> pretty (show x) <++> reflow "is private at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (BadTypeConType fc n)
|
||||
= pure $ "Return type of " ++ show n ++ " must be Type at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Return type of" <++> pretty (show n) <++> reflow "must be Type at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (BadDataConType fc n fam)
|
||||
= pure $ "Return type of " ++ show n ++ " must be in "
|
||||
++ show !(toFullNames fam) ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Return type of" <++> pretty (show n) <++> reflow "must be in"
|
||||
<++> pretty (show !(toFullNames fam)) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (NotCovering fc n IsCovering)
|
||||
= pure $ "Internal error (Coverage of " ++ show n ++ ")"
|
||||
= pure $ reflow "Internal error" <++> parens (reflow "Coverage of" <++> pretty (show n))
|
||||
perror (NotCovering fc n (MissingCases cs))
|
||||
= pure $ !(prettyName n) ++ " is not covering at:\n" ++ !(ploc fc) ++ "Missing cases:\n\t" ++
|
||||
showSep "\n\t" !(traverse (pshow []) cs)
|
||||
= pure $ vsep [ pretty !(prettyName n) <++> reflow "is not covering at" <+> colon
|
||||
, !(ploc fc)
|
||||
, reflow "Missing cases" <+> colon
|
||||
, indent 4 (vsep !(traverse (pshow []) cs))
|
||||
]
|
||||
perror (NotCovering fc n (NonCoveringCall ns))
|
||||
= pure $ !(prettyName n) ++ " is not covering at:\n" ++ !(ploc fc) ++ "\n\t" ++
|
||||
"Calls non covering function"
|
||||
++ case ns of
|
||||
[fn] => " " ++ show fn
|
||||
_ => "s: " ++ showSep ", " (map show ns)
|
||||
= pure $ vsep [ pretty !(prettyName n) <++> reflow "is not covering at" <+> colon
|
||||
, !(ploc fc)
|
||||
, reflow "Calls non covering function" <+>
|
||||
case ns of
|
||||
[fn] => space <+> pretty (show fn)
|
||||
_ => pretty 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty . show <$> ns)
|
||||
]
|
||||
perror (NotTotal fc n r)
|
||||
= pure $ !(prettyName n) ++ " is not total:\n\t" ++ show r ++ "\nat:\n" ++ !(ploc fc)
|
||||
= pure $ vsep [ pretty !(prettyName n) <++> reflow "is not total" <+> colon
|
||||
, pretty (show r)
|
||||
, pretty "at" <+> colon
|
||||
, !(ploc fc)
|
||||
]
|
||||
perror (LinearUsed fc count n)
|
||||
= pure $ "There are " ++ show count ++ " uses of linear name " ++ sugarName n ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "There are" <++> pretty (show count) <++> reflow "uses of linear name" <++> pretty (sugarName n)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (LinearMisuse fc n exp ctx)
|
||||
= if isErased exp
|
||||
then pure $ show n ++ " is not accessible in this context at:\n" ++ !(ploc fc)
|
||||
else pure $ "Trying to use " ++ showRig exp ++ " name " ++ sugarName n ++
|
||||
" in " ++ showRel ctx ++ " context at:\n" ++ !(ploc fc)
|
||||
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)
|
||||
where
|
||||
showRig : RigCount -> String
|
||||
showRig = elimSemi "irrelevant"
|
||||
"linear"
|
||||
(const "unrestricted")
|
||||
prettyRig : RigCount -> Doc ann
|
||||
prettyRig = elimSemi (pretty "irrelevant")
|
||||
(pretty "linear")
|
||||
(const $ pretty "unrestricted")
|
||||
|
||||
showRel : RigCount -> String
|
||||
showRel = elimSemi "irrelevant"
|
||||
"relevant"
|
||||
(const "non-linear")
|
||||
prettyRel : RigCount -> Doc ann
|
||||
prettyRel = elimSemi (pretty "irrelevant")
|
||||
(pretty "relevant")
|
||||
(const $ pretty "non-linear")
|
||||
perror (BorrowPartial fc env tm arg)
|
||||
= pure $ !(pshow env tm) ++
|
||||
" borrows argument " ++ !(pshow env arg) ++
|
||||
" so must be fully applied at:\n" ++ !(ploc fc)
|
||||
= pure $ !(pshow env tm) <++>
|
||||
reflow "borrows argument" <++> !(pshow env arg) <++>
|
||||
reflow "so must be fully applied at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (BorrowPartialType fc env tm)
|
||||
= pure $ !(pshow env tm) ++
|
||||
" borrows, so must return a concrete type at:\n" ++ !(ploc fc)
|
||||
perror (AmbiguousName fc ns) = pure $ "Ambiguous name " ++ show ns ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ !(pshow env tm) <++>
|
||||
reflow "borrows, so must return a concrete type at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (AmbiguousName fc ns)
|
||||
= pure $ pretty "Ambiguous name" <++> pretty (show ns) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (AmbiguousElab fc env ts)
|
||||
= do pp <- getPPrint
|
||||
setPPrint (record { fullNamespace = True } pp)
|
||||
let res = "Ambiguous elaboration at:\n" ++ !(ploc fc) ++ "Possible correct results:\n\t" ++
|
||||
showSep "\n\t" !(traverse (pshow env) ts)
|
||||
let res = vsep [ reflow "Ambiguous elaboration at" <+> colon
|
||||
, !(ploc fc)
|
||||
, reflow "Possible correct results" <+> colon
|
||||
, indent 4 (vsep !(traverse (pshow env) ts))
|
||||
]
|
||||
setPPrint pp
|
||||
pure res
|
||||
perror (AmbiguousSearch fc env tgt ts)
|
||||
= pure $ "Multiple solutions found in search of:\n\t"
|
||||
++ !(pshowNoNorm env tgt)
|
||||
++ "\nat:\n" ++ !(ploc fc)
|
||||
++ "\nPossible correct results:\n\t" ++
|
||||
showSep "\n\t" !(traverse (pshowNoNorm env) ts)
|
||||
= pure $ vsep [ 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 $ "Maximum ambiguity depth exceeded in " ++ show !(getFullName n)
|
||||
++ ": " ++ showSep " --> " (map show !(traverse getFullName ns)) ++ " at:\n" ++ !(ploc fc)
|
||||
= 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)
|
||||
perror (AllFailed ts)
|
||||
= case allUndefined ts of
|
||||
Just e => perror e
|
||||
_ => pure $ "Sorry, I can't find any elaboration which works. All errors:\n" ++
|
||||
showSep "\n" !(traverse pAlterror ts)
|
||||
_ => pure $ reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon <+> line
|
||||
<+> vsep !(traverse pAlterror ts)
|
||||
where
|
||||
pAlterror : (Maybe Name, Error) -> Core String
|
||||
pAlterror : (Maybe Name, Error) -> Core (Doc IdrisAnn)
|
||||
pAlterror (Just n, err)
|
||||
= pure $ "If " ++ show !(aliasName !(getFullName n)) ++ ": "
|
||||
++ !(perror err) ++ "\n"
|
||||
= pure $ pretty "If" <++> pretty (show !(aliasName !(getFullName n))) <+> colon <++> !(perror err) <+> line
|
||||
pAlterror (Nothing, err)
|
||||
= pure $ "Possible error:\n\t" ++ !(perror err)
|
||||
= pure $ reflow "Possible error" <+> colon <+> line <+> indent 4 !(perror err)
|
||||
|
||||
allUndefined : List (Maybe Name, Error) -> Maybe Error
|
||||
allUndefined [] = Nothing
|
||||
@ -174,34 +217,39 @@ perror (AllFailed ts)
|
||||
allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es
|
||||
allUndefined _ = Nothing
|
||||
perror (RecordTypeNeeded fc _)
|
||||
= pure $ "Can't infer type for this record update at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Can't infer type for this record update at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (NotRecordField fc fld Nothing)
|
||||
= pure $ fld ++ " is not part of a record type at:\n" ++ !(ploc fc)
|
||||
= pure $ pretty fld <++> reflow "is not part of a record type at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (NotRecordField fc fld (Just ty))
|
||||
= pure $ "Record type " ++ show !(getFullName ty) ++ " has no field " ++ fld ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Record type" <++> pretty (show !(getFullName ty)) <++> reflow "has no field" <++> pretty fld
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (NotRecordType fc ty)
|
||||
= pure $ show !(getFullName ty) ++ " is not a record type at:\n" ++ !(ploc fc)
|
||||
= pure $ pretty (show !(getFullName ty)) <++> reflow "is not a record type at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (IncompatibleFieldUpdate fc flds)
|
||||
= pure $ "Field update " ++ showSep "->" flds ++
|
||||
" not compatible with other updates at:\n" ++ !(ploc fc)
|
||||
= 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 $ show n ++ " is not a valid implicit argument in " ++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ pretty (show n) <++> reflow "is not a valid implicit argument in" <++> !(pshow env tm)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (InvalidImplicits fc env ns tm)
|
||||
= pure $ showSep ", " (map show ns) ++
|
||||
" are not valid implicit arguments in " ++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ concatWith (surround (comma <+> space)) (pretty . show <$> ns)
|
||||
<++> reflow "are not valid implicit arguments in" <++> !(pshow env tm)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (TryWithImplicits fc env imps)
|
||||
= pure $ "Need to bind implicits "
|
||||
++ showSep ", " !(traverse (tshow env) imps) ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Need to bind implicits"
|
||||
<++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
where
|
||||
tshow : {vars : _} ->
|
||||
Env Term vars -> (Name, Term vars) -> Core String
|
||||
tshow env (n, ty) = pure $ show n ++ " : " ++ !(pshow env ty)
|
||||
Env Term vars -> (Name, Term vars) -> Core (Doc IdrisAnn)
|
||||
tshow env (n, ty) = pure $ pretty (show n) <++> colon <++> !(pshow env ty)
|
||||
perror (BadUnboundImplicit fc env n ty)
|
||||
= pure $ "Can't bind name " ++ nameRoot n ++ " with type " ++ !(pshow env ty)
|
||||
++ " here at:\n" ++ !(ploc fc) ++ "Try binding explicitly."
|
||||
= 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."
|
||||
perror (CantSolveGoal fc env g)
|
||||
= let (_ ** (env', g')) = dropEnv env g in
|
||||
pure $ "Can't find an implementation for " ++ !(pshow env' g') ++ " at:\n" ++ !(ploc fc)
|
||||
pure $ reflow "Can't find an implementation for" <++> !(pshow env' g')
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
where
|
||||
-- For display, we don't want to see the full top level type; just the
|
||||
-- return type
|
||||
@ -213,109 +261,128 @@ perror (CantSolveGoal fc env g)
|
||||
dropEnv env tm = (_ ** (env, tm))
|
||||
|
||||
perror (DeterminingArg fc n i env g)
|
||||
= pure $ "Can't find an implementation for " ++ !(pshow env g) ++ "\n" ++
|
||||
"since I can't infer a value for argument " ++ show n ++ " at:\n" ++ !(ploc fc)
|
||||
= 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)
|
||||
perror (UnsolvedHoles hs)
|
||||
= pure $ "Unsolved holes:\n" ++ showHoles hs
|
||||
= pure $ reflow "Unsolved holes" <+> colon <+> line <+> prettyHoles hs
|
||||
where
|
||||
showHoles : List (FC, Name) -> String
|
||||
showHoles [] = ""
|
||||
showHoles ((fc, n) :: hs) = show n ++ " introduced at " ++ show fc ++ "\n"
|
||||
++ showHoles hs
|
||||
prettyHoles : List (FC, Name) -> Doc IdrisAnn
|
||||
prettyHoles [] = emptyDoc
|
||||
prettyHoles ((fc, n) :: hs)
|
||||
= pretty (show n) <++> reflow "introduced at" <++> pretty (show fc) <+> line <+> prettyHoles hs
|
||||
perror (CantInferArgType fc env n h ty)
|
||||
= pure $ "Can't infer type for argument " ++ show n ++ "\n" ++
|
||||
"Got " ++ !(pshow env ty) ++ " with hole " ++ show h ++ " at:\n" ++ !(ploc fc)
|
||||
= 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)
|
||||
perror (SolvedNamedHole fc env h tm)
|
||||
= pure $ "Named hole " ++ show h ++ " has been solved by unification\n"
|
||||
++ "Result: " ++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
|
||||
= 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)
|
||||
perror (VisibilityError fc vx x vy y)
|
||||
= pure $ show vx ++ " " ++ sugarName !(toFullNames x) ++
|
||||
" cannot refer to " ++ show vy ++ " " ++ sugarName !(toFullNames y) ++ " at:\n" ++ !(ploc fc)
|
||||
perror (NonLinearPattern fc n) = pure $ "Non linear pattern " ++ sugarName n ++ " at:\n" ++ !(ploc fc)
|
||||
perror (BadPattern fc n) = pure $ "Pattern not allowed here: " ++ show n ++ " at:\n" ++ !(ploc fc)
|
||||
perror (NoDeclaration fc n) = pure $ "No type declaration for " ++ show n ++ " at:\n" ++ !(ploc fc)
|
||||
perror (AlreadyDefined fc n) = pure $ show n ++ " is already defined"
|
||||
= 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)
|
||||
perror (NonLinearPattern fc n)
|
||||
= pure $ reflow "Non linear pattern" <++> pretty (sugarName n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (BadPattern fc n)
|
||||
= pure $ reflow "Pattern not allowed here" <+> colon <++> pretty (show n) <++> pretty "at" <+> colon <+> 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"
|
||||
perror (NotFunctionType fc env tm)
|
||||
= pure $ !(pshow env tm) ++ " is not a function type at:\n" ++ !(ploc fc)
|
||||
= pure $ !(pshow env tm) <++> reflow "is not a function type at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (RewriteNoChange fc env rule ty)
|
||||
= pure $ "Rewriting by " ++ !(pshow env rule) ++
|
||||
" did not change type " ++ !(pshow env ty) ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Rewriting by" <++> !(pshow env rule)
|
||||
<++> reflow "did not change type" <++> !(pshow env ty)
|
||||
<++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (NotRewriteRule fc env rule)
|
||||
= pure $ !(pshow env rule) ++ " is not a rewrite rule type at:\n" ++ !(ploc fc)
|
||||
= pure $ !(pshow env rule) <++> reflow "is not a rewrite rule type at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n DifferingArgNumbers)
|
||||
= pure $ "Patterns for " ++ !(prettyName n) ++ " have differing numbers of arguments at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Patterns for" <++> pretty !(prettyName n) <++> reflow "have differing numbers of arguments at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n DifferingTypes)
|
||||
= pure $ "Patterns for " ++ !(prettyName n) ++ " require matching on different types at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Patterns for" <++> pretty !(prettyName n) <++> reflow "require matching on different types at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n UnknownType)
|
||||
= pure $ "Can't infer type to match in " ++ !(prettyName n) ++ " at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Can't infer type to match in" <++> pretty !(prettyName n) <++> pretty "at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n (NotFullyApplied cn))
|
||||
= pure $ "Constructor " ++ show !(toFullNames cn) ++ " is not fully applied at:\n" ++ !(ploc fc)
|
||||
= pure $ pretty "Constructor" <++> pretty (show !(toFullNames cn)) <++> reflow "is not fully applied at"
|
||||
<+> colon <+> line <+> !(ploc fc)
|
||||
perror (CaseCompile fc n (MatchErased (_ ** (env, tm))))
|
||||
= pure $ "Attempt to match on erased argument " ++ !(pshow env tm) ++
|
||||
" in " ++ !(prettyName n) ++ " at\n:" ++ !(ploc fc)
|
||||
= pure $ reflow "Attempt to match on erased argument" <++> !(pshow env tm) <++> pretty "in"
|
||||
<++> pretty !(prettyName n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (BadDotPattern fc env reason x y)
|
||||
= pure $ "Can't match on " ++ !(pshow env x) ++
|
||||
" (" ++ show reason ++ ") at\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Can't match on" <++> !(pshow env x)
|
||||
<++> parens (pretty (show reason)) <++> pretty "at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (MatchTooSpecific fc env tm)
|
||||
= pure $ "Can't match on " ++ !(pshow env tm) ++
|
||||
" as it has a polymorphic type at:\n" ++ !(ploc fc)
|
||||
= pure $ reflow "Can't match on" <++> !(pshow env tm)
|
||||
<++> reflow "as it has a polymorphic type at" <+> colon <+> line <+> !(ploc fc)
|
||||
perror (BadImplicit fc str)
|
||||
= pure $ "Can't infer type for unbound implicit name " ++ str ++ " at\n" ++
|
||||
!(ploc fc) ++ "Try making it a bound implicit."
|
||||
= pure $ reflow "Can't infer type for unbound implicit name" <++> pretty str <++> pretty "at" <+> colon
|
||||
<+> line <+> !(ploc fc) <+> line <+> reflow "Try making it a bound implicit."
|
||||
perror (BadRunElab fc env script)
|
||||
= pure $ "Bad elaborator script " ++ !(pshow env script) ++ " at:\n" ++ !(ploc fc)
|
||||
perror (GenericMsg fc str) = pure $ str ++ " at:\n" ++ !(ploc fc)
|
||||
perror (TTCError msg) = pure $ "Error in TTC file: " ++ show msg ++ " (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)"
|
||||
= 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)
|
||||
perror (TTCError msg)
|
||||
= pure $ 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 $ "File error in " ++ fname ++ ": " ++ show err
|
||||
= pure $ reflow "File error in" <++> pretty fname <++> colon <++> pretty (show err)
|
||||
perror (ParseFail _ err)
|
||||
= pure $ show err
|
||||
= pure $ pretty (show err)
|
||||
perror (ModuleNotFound _ ns)
|
||||
= pure $ showSep "." (reverse ns) ++ " not found"
|
||||
= pure $ concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "not found"
|
||||
perror (CyclicImports ns)
|
||||
= pure $ "Module imports form a cycle: " ++ showSep " -> " (map showMod ns)
|
||||
= pure $ reflow "Module imports form a cycle" <+> colon <++> concatWith (surround (pretty " -> ")) (prettyMod <$> ns)
|
||||
where
|
||||
showMod : List String -> String
|
||||
showMod ns = showSep "." (reverse ns)
|
||||
perror ForceNeeded = pure "Internal error when resolving implicit laziness"
|
||||
perror (InternalError str) = pure $ "INTERNAL ERROR: " ++ str
|
||||
perror (UserError str) = pure $ "Error: " ++ str
|
||||
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 (InType fc n err)
|
||||
= pure $ "While processing type of " ++ !(prettyName n) ++
|
||||
" at " ++ show fc ++ ":\n" ++ !(perror err)
|
||||
= pure $ reflow "While processing type of" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
perror (InCon fc n err)
|
||||
= pure $ "While processing constructor " ++ !(prettyName n) ++
|
||||
" at " ++ show fc ++ ":\n" ++ !(perror err)
|
||||
= pure $ reflow "While processing constructor" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
perror (InLHS fc n err)
|
||||
= pure $ "While processing left hand side of " ++ !(prettyName n) ++
|
||||
" at " ++ show fc ++ ":\n" ++ !(perror err)
|
||||
= pure $ reflow "While processing left hand side of" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
perror (InRHS fc n err)
|
||||
= pure $ "While processing right hand side of " ++ !(prettyName n) ++
|
||||
" at " ++ show fc ++ ":\n" ++ !(perror err)
|
||||
= pure $ reflow "While processing right hand side of" <++> pretty !(prettyName n)
|
||||
<++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err)
|
||||
|
||||
export
|
||||
pwarning : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
Warning -> Core String
|
||||
Warning -> Core (Doc IdrisAnn)
|
||||
pwarning (UnreachableClause fc env tm)
|
||||
= pure $ "Warning: unreachable clause: " ++ !(pshow env tm)
|
||||
= pure $ annotate Warning (pretty "Warning" <+> colon)
|
||||
<++> pretty "unreachable clause" <+> colon
|
||||
<++> !(pshow env tm)
|
||||
|
||||
prettyMaybeLoc : Maybe FC -> Doc IdrisAnn
|
||||
prettyMaybeLoc Nothing = emptyDoc
|
||||
prettyMaybeLoc (Just fc) = annotate FileCtxt (pretty fc) <+> colon
|
||||
|
||||
export
|
||||
display : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
Error -> Core String
|
||||
Error -> Core (Doc IdrisAnn)
|
||||
display err
|
||||
= pure $ maybe "" (\f => show f ++ ":") (getErrorLoc err) ++
|
||||
!(perror err)
|
||||
= pure $ prettyMaybeLoc (getErrorLoc err) <+> !(perror err)
|
||||
|
||||
export
|
||||
displayWarning : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
Warning -> Core String
|
||||
Warning -> Core (Doc IdrisAnn)
|
||||
displayWarning w
|
||||
= pure $ maybe "" (\f => show f ++ ":") (getWarningLoc w) ++
|
||||
!(pwarning w)
|
||||
= pure $ prettyMaybeLoc (getWarningLoc w) <+> !(pwarning w)
|
||||
|
||||
@ -25,6 +25,7 @@ import Idris.Error
|
||||
import Idris.ModTree
|
||||
import Idris.Package
|
||||
import Idris.Parser
|
||||
import Idris.Pretty
|
||||
import Idris.Resugar
|
||||
import Idris.REPL
|
||||
import Idris.Syntax
|
||||
@ -42,6 +43,9 @@ import TTImp.ProcessDecls
|
||||
|
||||
import Utils.Hex
|
||||
|
||||
import Data.List
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Render.String
|
||||
import System
|
||||
import System.File
|
||||
|
||||
@ -241,7 +245,8 @@ processCatch cmd
|
||||
put UST u'
|
||||
put Syn s'
|
||||
put ROpts o'
|
||||
msg <- perror err
|
||||
pmsg <- perror err
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
pure $ REPL $ REPLError msg)
|
||||
|
||||
idePutStrLn : File -> Integer -> String -> Core ()
|
||||
|
||||
244
src/Idris/Pretty.idr
Normal file
244
src/Idris/Pretty.idr
Normal file
@ -0,0 +1,244 @@
|
||||
module Idris.Pretty
|
||||
|
||||
import Control.ANSI.SGR -- FIXME: tmp
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Render.Terminal
|
||||
import Text.PrettyPrint.Prettyprinter.Util
|
||||
|
||||
import Idris.Syntax
|
||||
|
||||
%default covering
|
||||
|
||||
public export
|
||||
data SyntaxAnn
|
||||
= Typ
|
||||
| Function
|
||||
| Data
|
||||
| Keyword
|
||||
| Bound
|
||||
| Pragma
|
||||
| Meta
|
||||
|
||||
public export
|
||||
data IdrisAnn
|
||||
= Warning
|
||||
| Error
|
||||
| FileCtxt
|
||||
| Syntax SyntaxAnn
|
||||
|
||||
export
|
||||
colorAnn : IdrisAnn -> AnsiStyle
|
||||
colorAnn Warning = color Yellow
|
||||
colorAnn Error = color BrightRed
|
||||
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
|
||||
|
||||
keyword : Doc IdrisAnn -> Doc IdrisAnn
|
||||
-- keyword = annotate (Syntax Keyword)
|
||||
keyword = id
|
||||
|
||||
meta : String -> Doc IdrisAnn
|
||||
-- meta s = annotate (Syntax Meta) (pretty s)
|
||||
meta s = pretty s
|
||||
|
||||
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])
|
||||
|
||||
let_ : Doc IdrisAnn
|
||||
let_ = keyword (pretty "let")
|
||||
|
||||
in_ : Doc IdrisAnn
|
||||
in_ = keyword (pretty "in")
|
||||
|
||||
case_ : Doc IdrisAnn
|
||||
case_ = keyword (pretty "case")
|
||||
|
||||
of_ : Doc IdrisAnn
|
||||
of_ = keyword (pretty "of")
|
||||
|
||||
do_ : Doc IdrisAnn
|
||||
do_ = keyword (pretty "do")
|
||||
|
||||
with_ : Doc IdrisAnn
|
||||
with_ = keyword (pretty "with")
|
||||
|
||||
record_ : Doc IdrisAnn
|
||||
record_ = keyword (pretty "record")
|
||||
|
||||
impossible_ : Doc IdrisAnn
|
||||
impossible_ = keyword (pretty "impossible")
|
||||
|
||||
auto_ : Doc IdrisAnn
|
||||
auto_ = keyword (pretty "auto")
|
||||
|
||||
default_ : Doc IdrisAnn
|
||||
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
|
||||
|
||||
prettyParens : (1 _ : Bool) -> Doc ann -> Doc ann
|
||||
prettyParens False s = s
|
||||
prettyParens True s = parens s
|
||||
|
||||
prettyCon : Prec -> Doc ann -> Doc ann -> Doc ann
|
||||
prettyCon d conName conArgs = prettyParens (d >= App) (conName <++> conArgs)
|
||||
|
||||
prettyRig : RigCount -> Doc ann
|
||||
prettyRig = elimSemi (pretty '0' <+> space)
|
||||
(pretty '1' <+> space)
|
||||
(const emptyDoc)
|
||||
|
||||
mutual
|
||||
prettyAlt : PClause -> Doc IdrisAnn
|
||||
prettyAlt (MkPatClause _ lhs rhs _) =
|
||||
space <+> pipe <++> prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs <+> semi
|
||||
prettyAlt (MkWithClause _ lhs wval flags cs) =
|
||||
space <+> pipe <++> angles (angles (reflow "with alts not possible")) <+> semi
|
||||
prettyAlt (MkImpossible _ lhs) =
|
||||
space <+> pipe <++> prettyTerm lhs <++> impossible_ <+> semi
|
||||
|
||||
prettyCase : PClause -> Doc IdrisAnn
|
||||
prettyCase (MkPatClause _ lhs rhs _) =
|
||||
prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs
|
||||
prettyCase (MkWithClause _ lhs rhs flags _) =
|
||||
space <+> pipe <++> angles (angles (reflow "with alts not possible"))
|
||||
prettyCase (MkImpossible _ lhs) =
|
||||
prettyTerm lhs <++> impossible_
|
||||
|
||||
prettyDo : PDo -> Doc IdrisAnn
|
||||
prettyDo (DoExp _ tm) = prettyTerm tm
|
||||
prettyDo (DoBind _ n tm) = pretty n <++> pretty "<-" <++> prettyTerm tm
|
||||
prettyDo (DoBindPat _ l tm alts) =
|
||||
prettyTerm l <++> pretty "<-" <++> prettyTerm tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
|
||||
prettyDo (DoLet _ l rig _ tm) =
|
||||
let_ <++> prettyRig rig <+> pretty l <++> equals <++> prettyTerm tm
|
||||
prettyDo (DoLetPat _ l _ tm alts) =
|
||||
let_ <++> prettyTerm l <++> equals <++> prettyTerm tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
|
||||
prettyDo (DoLetLocal _ ds) =
|
||||
let_ <++> braces (angles (angles (pretty "definitions")))
|
||||
prettyDo (DoRewrite _ rule) = rewrite_ <+> prettyTerm rule
|
||||
|
||||
prettyUpdate : PFieldUpdate -> Doc IdrisAnn
|
||||
prettyUpdate (PSetField path v) =
|
||||
concatWith (surround dot) (pretty <$> path) <++> equals <++> prettyTerm v
|
||||
prettyUpdate (PSetFieldApp path v) =
|
||||
concatWith (surround dot) (pretty <$> path) <++> pretty '$' <+> equals <++> prettyTerm v
|
||||
|
||||
export
|
||||
prettyTerm : PTerm -> Doc IdrisAnn
|
||||
prettyTerm = go Open
|
||||
where
|
||||
go : Prec -> PTerm -> Doc IdrisAnn
|
||||
go d (PRef _ n) = pretty n
|
||||
go d (PPi _ rig Explicit Nothing arg ret) =
|
||||
go d arg <++> pretty "->" <++> go d ret
|
||||
go d (PPi _ rig Explicit (Just n) arg ret) =
|
||||
parens (prettyRig rig <+> pretty n <++> colon <++> go d arg) <++> pretty "->" <++> go d ret
|
||||
go d (PPi _ rig Implicit Nothing arg ret) =
|
||||
braces (prettyRig rig <+> pretty '_' <++> colon <++> go d arg) <++> pretty "->" <++> go d ret
|
||||
go d (PPi _ rig Implicit (Just n) arg ret) =
|
||||
braces (prettyRig rig <+> pretty n <++> colon <++> go d arg) <++> pretty "->" <++> go d ret
|
||||
go d (PPi _ rig AutoImplicit Nothing arg ret) =
|
||||
go d arg <++> pretty "=>" <++> go d ret
|
||||
go d (PPi _ rig AutoImplicit (Just n) arg ret) =
|
||||
braces (auto_ <++> prettyRig rig <+> pretty n <+> colon <+> go d arg) <++> pretty "->" <++> go d ret
|
||||
go d (PPi _ rig (DefImplicit t) Nothing arg ret) =
|
||||
braces (default_ <++> go App t <++> prettyRig rig <+> pretty '_' <++> colon <++> go d arg) <++> pretty "->" <++> go d ret
|
||||
go d (PPi _ rig (DefImplicit t) (Just n) arg ret) =
|
||||
braces (default_ <++> go App t <++> prettyRig rig <+> pretty n <++> colon <++> go d arg) <++> pretty "->" <++> go d ret
|
||||
go d (PLam _ rig _ n (PImplicit _) sc) =
|
||||
backslash <+> prettyRig rig <+> go d n <++> pretty "=>" <++> go d sc
|
||||
go d (PLam _ rig _ n ty sc) =
|
||||
backslash <+> prettyRig rig <+> go d n <++> colon <++> go d ty <++> pretty "=>" <++> go d sc
|
||||
go d (PLet _ rig n (PImplicit _) val sc alts) =
|
||||
let_ <++> prettyRig rig <+> go d n <++> equals <++> go d val <++> in_ <++> go d sc
|
||||
go d (PLet _ rig n ty val sc alts) =
|
||||
let_ <++> prettyRig rig <+> go d n <++> colon <++> go d ty <++> equals <++> go d val <+> hang 4 (fillSep (prettyAlt <$> alts)) <++> in_ <++> go d sc
|
||||
go d (PCase _ tm cs) =
|
||||
case_ <+> go d tm <++> of_ <++> braces (concatWith (surround semi) (prettyCase <$> cs))
|
||||
go d (PLocal _ ds sc) =
|
||||
let_ <++> braces (angles (angles (pretty "definitions"))) <++> in_ <++> go d sc
|
||||
go d (PUpdate _ fs) =
|
||||
record_ <++> braces (concatWith (surround (comma <+> space)) (prettyUpdate <$> fs))
|
||||
go d (PApp _ f a) = go App f <++> go App a
|
||||
go d (PWithApp _ f a) = go d f <++> pipe <++> go d a
|
||||
go d (PImplicitApp _ f Nothing a) = go d f <++> pretty '@' <+> braces (go d a)
|
||||
go d (PDelayed _ LInf ty) = prettyCon d (pretty "Inf") (go App ty)
|
||||
go d (PDelayed _ _ ty) = prettyCon d (pretty "Lazy") (go App ty)
|
||||
go d (PDelay _ tm) = prettyCon d (pretty "Delay") (go App tm)
|
||||
go d (PForce _ tm) = prettyCon d (pretty "Force") (go App tm)
|
||||
go d (PImplicitApp _ f (Just n) (PRef _ a)) =
|
||||
if n == a
|
||||
then go d f <++> braces (pretty n)
|
||||
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 (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 (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 (PAs _ n p) = pretty n <+> pretty '@' <+> go d p
|
||||
go d (PDotted _ p) = dot <+> go d p
|
||||
go d (PImplicit _) = pretty '_'
|
||||
go d (PInfer _) = pretty '?'
|
||||
go d (POp _ op x y) = go d x <++> pretty op <++> go d y
|
||||
go d (PPrefixOp _ op x) = pretty op <+> go d x
|
||||
go d (PSectionL _ op x) = parens (pretty op <++> go d x)
|
||||
go d (PSectionR _ x op) = parens (go d x <++> pretty op)
|
||||
go d (PEq fc l r) = go d l <++> equals <++> go d r
|
||||
go d (PBracketed _ tm) = parens (go d tm)
|
||||
go d (PDoBlock _ ns ds) = do_ <++> concatWith (surround (space <+> semi <+> space)) (prettyDo <$> ds)
|
||||
go d (PBang _ tm) = pretty '!' <+> go d tm
|
||||
go d (PIdiom _ tm) = enclose (pretty "[|") (pretty "|]") (go d tm)
|
||||
go d (PList _ xs) = brackets (concatWith (surround (comma <+> space)) (go d <$> xs))
|
||||
go d (PPair _ l r) = parens (go d l <+> comma <++> go d r)
|
||||
go d (PDPair _ l (PImplicit _) r) = parens (go d l <++> pretty "**" <++> go d r)
|
||||
go d (PDPair _ l ty r) = parens (go d l <++> colon <++> go d ty <++> pretty "**" <++> go d r)
|
||||
go d (PUnit _) = pretty "()"
|
||||
go d (PIfThenElse _ x t e) = ite (go d x) (go d t) (go d e)
|
||||
go d (PComprehension _ ret es) =
|
||||
brackets (go d (dePure ret) <++> pipe <++> concatWith (surround (comma <+> space)) (prettyDo . deGuard <$> es))
|
||||
where
|
||||
dePure : PTerm -> PTerm
|
||||
dePure tm@(PApp _ (PRef _ n) arg) = if dropNS n == UN "pure" then arg else tm
|
||||
dePure tm = tm
|
||||
|
||||
deGuard : PDo -> PDo
|
||||
deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) = if dropNS n == UN "guard" then DoExp fc arg else tm
|
||||
deGuard tm = tm
|
||||
go d (PRewrite _ rule tm) = rewrite_ <++> go d rule <++> in_ <++> go d tm
|
||||
go d (PRange _ start Nothing end) =
|
||||
brackets (go d start <++> pretty ".." <++> go d end)
|
||||
go d (PRange _ start (Just next) end) =
|
||||
brackets (go d start <+> comma <++> go d next <++> pretty ".." <++> go d end)
|
||||
go d (PRangeStream _ start Nothing) = brackets (go d start <++> pretty "..")
|
||||
go d (PRangeStream _ start (Just next)) =
|
||||
brackets (go d start <+> comma <++> go d next <++> pretty "..")
|
||||
go d (PUnifyLog _ lvl tm) = go d tm
|
||||
go d (PPostfixProjs fc rec fields) =
|
||||
go d rec <++> dot <+> concatWith (surround dot) (go d <$> fields)
|
||||
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
|
||||
@ -32,6 +32,7 @@ import Idris.IDEMode.MakeClause
|
||||
import Idris.IDEMode.Holes
|
||||
import Idris.ModTree
|
||||
import Idris.Parser
|
||||
import Idris.Pretty
|
||||
import Idris.ProcessIdr
|
||||
import Idris.Resugar
|
||||
import public Idris.REPLCommon
|
||||
@ -52,6 +53,8 @@ import Data.Maybe
|
||||
import Data.NameMap
|
||||
import Data.Stream
|
||||
import Data.Strings
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Render.Terminal
|
||||
|
||||
import System
|
||||
import System.File
|
||||
@ -816,7 +819,9 @@ processCatch cmd
|
||||
put UST u'
|
||||
put Syn s'
|
||||
put ROpts o'
|
||||
pure $ REPLError !(display err)
|
||||
pmsg <- display err
|
||||
let msg = reAnnotateS colorAnn $ layoutPretty defaultLayoutOptions pmsg -- FIXME: tmp
|
||||
pure $ REPLError $ renderString msg
|
||||
)
|
||||
|
||||
parseEmptyCmd : SourceEmptyRule (Maybe REPLCmd)
|
||||
@ -930,7 +935,7 @@ mutual
|
||||
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 ++ ": " ++ !(perror err)
|
||||
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"
|
||||
|
||||
@ -10,8 +10,11 @@ import Idris.Error
|
||||
import Idris.IDEMode.Commands
|
||||
import public Idris.REPLOpts
|
||||
import Idris.Syntax
|
||||
import Idris.Pretty
|
||||
|
||||
import Data.List
|
||||
import Text.PrettyPrint.Prettyprinter
|
||||
import Text.PrettyPrint.Prettyprinter.Render.Terminal
|
||||
|
||||
%default covering
|
||||
|
||||
@ -58,10 +61,12 @@ emitError err
|
||||
= do opts <- get ROpts
|
||||
case idemode opts of
|
||||
REPL _ =>
|
||||
do msg <- display err
|
||||
do pmsg <- reAnnotate colorAnn <$> display err
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
coreLift $ putStrLn msg
|
||||
IDEMode i _ f =>
|
||||
do msg <- perror err
|
||||
do pmsg <- reAnnotate colorAnn <$> perror err
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
case getErrorLoc err of
|
||||
Nothing => iputStrLn msg
|
||||
Just fc =>
|
||||
@ -86,10 +91,12 @@ emitWarning w
|
||||
= do opts <- get ROpts
|
||||
case idemode opts of
|
||||
REPL _ =>
|
||||
do msg <- displayWarning w
|
||||
do pmsg <- reAnnotate colorAnn <$> displayWarning w
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
coreLift $ putStrLn msg
|
||||
IDEMode i _ f =>
|
||||
do msg <- pwarning w
|
||||
do pmsg <- reAnnotate colorAnn <$> pwarning w
|
||||
let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp
|
||||
case getWarningLoc w of
|
||||
Nothing => iputStrLn msg
|
||||
Just fc =>
|
||||
|
||||
@ -15,13 +15,13 @@ 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
|
||||
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
|
||||
9 foo Nat = "Nat"
|
||||
^^^
|
||||
|
||||
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:
|
||||
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:
|
||||
9 | foo Nat = "Nat"
|
||||
^^^
|
||||
|
||||
@ -2,11 +2,10 @@
|
||||
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
|
||||
S Z
|
||||
and
|
||||
Z
|
||||
Z
|
||||
at:
|
||||
1 zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
|
||||
^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
1 | zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
|
||||
^^^^^^^^^^^^^^^^^^^^^^^
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,11 +1,12 @@
|
||||
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:
|
||||
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)
|
||||
^^^^^^
|
||||
26 | keepUnique {b} xs = toList (fromList xs)
|
||||
^^^^^^
|
||||
Possible correct results:
|
||||
Main.Set.toList ?arg
|
||||
Main.Vect.toList ?arg
|
||||
Main.Set.toList ?arg
|
||||
Main.Vect.toList ?arg
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,15 +1,14 @@
|
||||
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
|
||||
2 foo x x = x + x
|
||||
^
|
||||
|
||||
Can't match on ?x [no locals in scope] (Non linear pattern variable) at:
|
||||
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:
|
||||
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]
|
||||
?y [no locals in scope]
|
||||
at:
|
||||
5 addBaz (x + y) (AddThings x z) = x + y
|
||||
^
|
||||
|
||||
5 | addBaz (x + y) (AddThings x z) = x + y
|
||||
^
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
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:
|
||||
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:
|
||||
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:
|
||||
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:
|
||||
19 wrongCommutes2 (S k) m = rewrite m in ?bar
|
||||
^^^^^^^^^^^^^^^^^
|
||||
|
||||
19 | wrongCommutes2 (S k) m = rewrite m in ?bar
|
||||
^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,32 +1,33 @@
|
||||
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 ?_ ?_
|
||||
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
|
||||
Nat
|
||||
and
|
||||
Integer
|
||||
Integer
|
||||
at:
|
||||
14 etaBad = Refl
|
||||
^^^^
|
||||
|
||||
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 ?_
|
||||
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
|
||||
a
|
||||
and
|
||||
Nat
|
||||
Nat
|
||||
at:
|
||||
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 ?_
|
||||
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
|
||||
a
|
||||
and
|
||||
Nat
|
||||
Nat
|
||||
at:
|
||||
5 test2 = {a : _} -> the (S = \x : a => S _) Refl
|
||||
^^^^
|
||||
|
||||
5 | test2 = {a : _} -> the (S = \x : a => S _) Refl
|
||||
^^^^
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
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:
|
||||
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:
|
||||
34 bar = 8
|
||||
^
|
||||
|
||||
34 | bar = 8
|
||||
^
|
||||
|
||||
@ -1,13 +1,13 @@
|
||||
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
|
||||
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
|
||||
19 minusBad (S k) Z LeZ = S k
|
||||
^^^
|
||||
|
||||
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:
|
||||
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:
|
||||
19 | minusBad (S k) Z LeZ = S k
|
||||
^^^
|
||||
Main> \m => minus (S (S m)) m prf
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
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:
|
||||
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
|
||||
(1 _ : Nat) -> MyN
|
||||
and
|
||||
MyN
|
||||
MyN
|
||||
at:
|
||||
4 foo x y = case MkN x of
|
||||
^^^^^
|
||||
|
||||
4 | foo x y = case MkN x of
|
||||
^^^^^
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
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
|
||||
7 nameOf (MyMaybe Bool) = "MyMaybe Bool"
|
||||
^^^^
|
||||
|
||||
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:
|
||||
7 | nameOf (MyMaybe Bool) = "MyMaybe Bool"
|
||||
^^^^
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
1/1: Building unboundimps (unboundimps.idr)
|
||||
unboundimps.idr:18:11--18:13:While processing type of len' at unboundimps.idr:18:1--18:20:
|
||||
unboundimps.idr:18:11--18:13:While processing type
|
||||
of len' at unboundimps.idr:18:1--18:20:
|
||||
Undefined name xs at:
|
||||
18 len': Env xs -> Nat
|
||||
^^
|
||||
|
||||
unboundimps.idr:19:16--19:17:While processing type of append' at unboundimps.idr:19:1--19:49:
|
||||
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:
|
||||
19 append' : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
^
|
||||
|
||||
19 | append' : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
^
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
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:
|
||||
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
|
||||
Int
|
||||
and
|
||||
String
|
||||
String
|
||||
at:
|
||||
22 = do let Just x' : Maybe String = x
|
||||
^
|
||||
|
||||
22 | = do let Just x' : Maybe String = x
|
||||
^
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
1/1: Building Cover (Cover.idr)
|
||||
Cover.idr:16:1--16:7:While processing left hand side of badBar at Cover.idr:16:1--17:1:
|
||||
Cover.idr:16:1--16:7:While processing left hand side
|
||||
of badBar at Cover.idr:16:1--17:1:
|
||||
Can't match on 0 as it has a polymorphic type at:
|
||||
16 badBar Z = Z
|
||||
^^^^^^
|
||||
|
||||
16 | badBar Z = Z
|
||||
^^^^^^
|
||||
Main> Main.foo:
|
||||
foo (0, S _)
|
||||
foo (S _, _)
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
1/1: Building Cover (Cover.idr)
|
||||
Cover.idr:14:1--14:4:While processing left hand side of bad at Cover.idr:14:1--15:1:
|
||||
Cover.idr:14:1--14:4:While processing left hand side
|
||||
of bad at Cover.idr:14:1--15:1:
|
||||
Can't match on Just (fromInteger 0) as it has a polymorphic type at:
|
||||
14 bad (Just 0) _ = False
|
||||
^^^
|
||||
|
||||
14 | bad (Just 0) _ = False
|
||||
^^^
|
||||
Main> Main.okay:
|
||||
okay (S _) IsNat
|
||||
okay False IsBool
|
||||
|
||||
@ -1,9 +1,7 @@
|
||||
1/1: Building eq (eq.idr)
|
||||
eq.idr:27:1--27:23:badeq x y p is not a valid impossible case at:
|
||||
27 badeq x y p impossible
|
||||
^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
27 | badeq x y p impossible
|
||||
^^^^^^^^^^^^^^^^^^^^^^
|
||||
eq.idr:30:1--30:26:badeqL xs ys p is not a valid impossible case at:
|
||||
30 badeqL xs ys p impossible
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
30 | badeqL xs ys p impossible
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,6 +1,5 @@
|
||||
1/1: Building casetot (casetot.idr)
|
||||
casetot.idr:12:1--13:1:main is not covering at:
|
||||
12 main : IO ()
|
||||
13 main = do
|
||||
|
||||
Calls non covering function Main.case block in case block in main
|
||||
12 | main : IO ()
|
||||
13 | main = do
|
||||
Calls non covering function Main.case block in case block in main
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
1/1: Building Error (Error.idr)
|
||||
Error.idr:6:19--6:20:While processing right hand side of wrong at Error.idr:6:1--7:1:
|
||||
Error.idr:6:19--6:20:While processing right hand side
|
||||
of wrong at Error.idr:6:1--7:1:
|
||||
When unifying a and Vect ?k ?a
|
||||
Mismatch between:
|
||||
a
|
||||
a
|
||||
and
|
||||
Vect ?k ?a
|
||||
Vect ?k ?a
|
||||
at:
|
||||
6 wrong x xs = x :: x
|
||||
^
|
||||
|
||||
6 | wrong x xs = x :: x
|
||||
^
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
1/1: Building Error (Error.idr)
|
||||
Error.idr:6:17--6:19:While processing right hand side of wrong at Error.idr:6:1--7:1:
|
||||
Error.idr:6:17--6:19:While processing right hand side
|
||||
of wrong at Error.idr:6:1--7:1:
|
||||
Undefined name ys at:
|
||||
6 wrong xs = x :: ys
|
||||
^^
|
||||
|
||||
6 | wrong xs = x :: ys
|
||||
^^
|
||||
|
||||
@ -1,33 +1,31 @@
|
||||
1/1: Building Error (Error.idr)
|
||||
Error.idr:12:18--12:19:While processing right hand side of wrong at Error.idr:12:1--13:1:
|
||||
Error.idr:12:18--12:19:While processing right hand side
|
||||
of wrong at Error.idr:12:1--13:1:
|
||||
Sorry, I can't find any elaboration which works. All errors:
|
||||
If Main.length: When unifying Nat and Vect ?n ?a
|
||||
Mismatch between:
|
||||
Nat
|
||||
Nat
|
||||
and
|
||||
Vect ?n ?a
|
||||
Vect ?n ?a
|
||||
at:
|
||||
12 wrong x = length x
|
||||
^
|
||||
|
||||
12 | wrong x = length x
|
||||
^
|
||||
|
||||
If Prelude.List.length: When unifying Nat and List ?a
|
||||
Mismatch between:
|
||||
Nat
|
||||
Nat
|
||||
and
|
||||
List ?a
|
||||
List ?a
|
||||
at:
|
||||
12 wrong x = length x
|
||||
^
|
||||
|
||||
12 | wrong x = length x
|
||||
^
|
||||
|
||||
If Prelude.Strings.length: When unifying Nat and String
|
||||
Mismatch between:
|
||||
Nat
|
||||
Nat
|
||||
and
|
||||
String
|
||||
String
|
||||
at:
|
||||
12 wrong x = length x
|
||||
^
|
||||
|
||||
12 | wrong x = length x
|
||||
^
|
||||
|
||||
|
||||
@ -1,25 +1,25 @@
|
||||
1/1: Building Error1 (Error1.idr)
|
||||
Error1.idr:8:9--9:1:While processing right hand side of wrong at Error1.idr:8:1--9:1:
|
||||
Error1.idr:8:9--9:1:While processing right hand side
|
||||
of wrong at Error1.idr:8:1--9:1:
|
||||
Can't find an implementation for Show (Vect 4 Integer) at:
|
||||
8 wrong = show (the (Vect _ _) [1,2,3,4])
|
||||
|
||||
8 | wrong = show (the (Vect _ _) [1,2,3,4])
|
||||
1/1: Building Error2 (Error2.idr)
|
||||
Error2.idr:13:38--13:45:While processing right hand side of show at Error2.idr:13:3--15:1:
|
||||
Error2.idr:13:38--13:45:While processing right hand side
|
||||
of show at Error2.idr:13:3--15:1:
|
||||
Multiple solutions found in search of:
|
||||
Show (Vect k Integer)
|
||||
Show (Vect k Integer)
|
||||
at:
|
||||
13 show (x :: xs) = show x ++ ", " ++ show xs
|
||||
^^^^^^^
|
||||
|
||||
13 | show (x :: xs) = show x ++ ", " ++ show xs
|
||||
^^^^^^^
|
||||
Possible correct results:
|
||||
Show implementation at Error2.idr:11:1--15:1
|
||||
Show implementation at Error2.idr:7:1--11:1
|
||||
Error2.idr:16:9--17:1:While processing right hand side of wrong at Error2.idr:16:1--17:1:
|
||||
Show implementation at Error2.idr:11:1--15:1
|
||||
Show implementation at Error2.idr:7:1--11:1
|
||||
Error2.idr:16:9--17:1:While processing right hand side
|
||||
of wrong at Error2.idr:16:1--17:1:
|
||||
Multiple solutions found in search of:
|
||||
Show (Vect 1 Integer)
|
||||
Show (Vect 1 Integer)
|
||||
at:
|
||||
16 wrong = show (the (Vect _ _) [1])
|
||||
|
||||
16 | wrong = show (the (Vect _ _) [1])
|
||||
Possible correct results:
|
||||
Show implementation at Error2.idr:11:1--15:1
|
||||
Show implementation at Error2.idr:7:1--11:1
|
||||
Show implementation at Error2.idr:11:1--15:1
|
||||
Show implementation at Error2.idr:7:1--11:1
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
1/1: Building IfErr (IfErr.idr)
|
||||
IfErr.idr:4:11--4:17:While processing right hand side of foo at IfErr.idr:4:1--6:1:
|
||||
IfErr.idr:4:11--4:17:While processing right hand side
|
||||
of foo at IfErr.idr:4:1--6:1:
|
||||
Can't find an implementation for Eq a at:
|
||||
4 foo x y = x == y
|
||||
^^^^^^
|
||||
|
||||
IfErr.idr:7:11--7:17:While processing right hand side of bar at IfErr.idr:7:1--8:1:
|
||||
4 | foo x y = x == y
|
||||
^^^^^^
|
||||
IfErr.idr:7:11--7:17:While processing right hand side
|
||||
of bar at IfErr.idr:7:1--8:1:
|
||||
Can't find an implementation for Eq Wibble at:
|
||||
7 bar x y = x == y
|
||||
^^^^^^
|
||||
|
||||
7 | bar x y = x == y
|
||||
^^^^^^
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
1/1: Building IfErr (IfErr.idr)
|
||||
IfErr.idr:15:10--15:30:While processing right hand side of test at IfErr.idr:15:1--17:1:
|
||||
IfErr.idr:15:10--15:30:While processing right hand side
|
||||
of test at IfErr.idr:15:1--17:1:
|
||||
Can't find an implementation for Eq Foo at:
|
||||
15 test x = showIfEq MkFoo MkBar
|
||||
^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
IfErr.idr:23:9--23:29:While processing right hand side of test2 at IfErr.idr:23:1--25:1:
|
||||
15 | test x = showIfEq MkFoo MkBar
|
||||
^^^^^^^^^^^^^^^^^^^^
|
||||
IfErr.idr:23:9--23:29:While processing right hand side
|
||||
of test2 at IfErr.idr:23:1--25:1:
|
||||
Can't find an implementation for Show Foo at:
|
||||
23 test2 = showIfEq MkFoo MkBar
|
||||
^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
23 | test2 = showIfEq MkFoo MkBar
|
||||
^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,10 +1,10 @@
|
||||
1/1: Building CongErr (CongErr.idr)
|
||||
CongErr.idr:4:11--4:19:While processing right hand side of fsprf at CongErr.idr:4:1--5:1:
|
||||
CongErr.idr:4:11--4:19:While processing right hand side
|
||||
of fsprf at CongErr.idr:4:1--5:1:
|
||||
Can't solve constraint between:
|
||||
?_ x
|
||||
?_ x
|
||||
and
|
||||
FS x
|
||||
FS x
|
||||
at:
|
||||
4 fsprf p = cong _ p
|
||||
^^^^^^^^
|
||||
|
||||
4 | fsprf p = cong _ p
|
||||
^^^^^^^^
|
||||
|
||||
@ -1,3 +1,4 @@
|
||||
1/1: Building Loop (Loop.idr)
|
||||
Loop.idr:2:11--2:19:While processing right hand side of example at Loop.idr:2:1--3:1:
|
||||
Loop.idr:2:11--2:19:While processing right hand side
|
||||
of example at Loop.idr:2:1--3:1:
|
||||
Main.example is already defined
|
||||
|
||||
@ -3,11 +3,9 @@
|
||||
3/3: Building Test (Test.idr)
|
||||
Test.idr:5:9--5:12:While processing type of thing at Test.idr:5:1--5:19:
|
||||
Undefined name Nat at:
|
||||
5 thing : Nat -> Nat
|
||||
^^^
|
||||
|
||||
5 | thing : Nat -> Nat
|
||||
^^^
|
||||
Test.idr:6:1--8:1:No type declaration for Test.thing at:
|
||||
6 thing x = mult x (plus x x)
|
||||
7
|
||||
|
||||
6 | thing x = mult x (plus x x)
|
||||
7 |
|
||||
Test> Bye for now!
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
1/1: Building Deps (Deps.idr)
|
||||
Deps.idr:18:13--18:14:While processing right hand side of badcard at Deps.idr:18:3--19:3:
|
||||
Deps.idr:18:13--18:14:While processing right hand side
|
||||
of badcard at Deps.idr:18:3--19:3:
|
||||
k is not accessible in this context at:
|
||||
18 badcard = k
|
||||
^
|
||||
|
||||
18 | badcard = k
|
||||
^
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
1/1: Building TypeInt (TypeInt.idr)
|
||||
TypeInt.idr:14:25--14:49:While processing constructor MkRecord at TypeInt.idr:14:3--14:61:
|
||||
TypeInt.idr:14:25--14:49:While processing
|
||||
constructor MkRecord at TypeInt.idr:14:3--14:61:
|
||||
Can't find an implementation for Interface ?s at:
|
||||
14 MkRecord : Value s -> DependentValue {s} value -> Record s
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
14 | MkRecord : Value s -> DependentValue {s} value -> Record s
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,26 +1,26 @@
|
||||
1/1: Building gnu (gnu.idr)
|
||||
gnu.idr:47:27--47:32:While processing right hand side of TestSurprise1 at gnu.idr:47:1--49:1:
|
||||
gnu.idr:47:27--47:32:While processing right hand side
|
||||
of TestSurprise1 at gnu.idr:47:1--49:1:
|
||||
Multiple solutions found in search of:
|
||||
Gnu
|
||||
Gnu
|
||||
at:
|
||||
47 TestSurprise1 gnu1 gnu2 = Guess
|
||||
^^^^^
|
||||
|
||||
47 | TestSurprise1 gnu1 gnu2 = Guess
|
||||
^^^^^
|
||||
Possible correct results:
|
||||
gnu1
|
||||
gnu2
|
||||
gnu.idr:50:21--50:26:While processing right hand side of TestSurprise2 at gnu.idr:50:1--52:1:
|
||||
gnu1
|
||||
gnu2
|
||||
gnu.idr:50:21--50:26:While processing right hand side
|
||||
of TestSurprise2 at gnu.idr:50:1--52:1:
|
||||
Multiple solutions found in search of:
|
||||
Gnu
|
||||
Gnu
|
||||
at:
|
||||
50 TestSurprise2 f g = Guess
|
||||
^^^^^
|
||||
|
||||
50 | TestSurprise2 f g = Guess
|
||||
^^^^^
|
||||
Possible correct results:
|
||||
f ()
|
||||
g ()
|
||||
gnu.idr:53:19--53:24:While processing right hand side of TestSurprise3 at gnu.idr:53:1--54:1:
|
||||
f ()
|
||||
g ()
|
||||
gnu.idr:53:19--53:24:While processing right hand side
|
||||
of TestSurprise3 at gnu.idr:53:1--54:1:
|
||||
Can't find an implementation for Gnu at:
|
||||
53 TestSurprise3 f = Guess
|
||||
^^^^^
|
||||
|
||||
53 | TestSurprise3 f = Guess
|
||||
^^^^^
|
||||
|
||||
@ -1,12 +1,12 @@
|
||||
1/1: Building TwoNum (TwoNum.idr)
|
||||
TwoNum.idr:4:7--4:8:While processing right hand side of f at TwoNum.idr:2:1--5:1:
|
||||
TwoNum.idr:4:7--4:8:While processing right hand side
|
||||
of f at TwoNum.idr:2:1--5:1:
|
||||
While processing right hand side of f,g at TwoNum.idr:4:3--5:1:
|
||||
Multiple solutions found in search of:
|
||||
Num a
|
||||
Num a
|
||||
at:
|
||||
4 g = 0
|
||||
^
|
||||
|
||||
4 | g = 0
|
||||
^
|
||||
Possible correct results:
|
||||
conArg
|
||||
conArg
|
||||
conArg
|
||||
conArg
|
||||
|
||||
@ -1,7 +1,6 @@
|
||||
Main> (interactive):1:1--1:25:Undefined name fromMaybe at:
|
||||
1 fromMaybe "test" Nothing
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
1 | fromMaybe "test" Nothing
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
Main> Imported module Data.Maybe
|
||||
Main> "test"
|
||||
Main> Imported module Data.Strings
|
||||
|
||||
@ -4,40 +4,38 @@ Main> S Z
|
||||
Main> S (S Z)
|
||||
Main> S Z
|
||||
Main> (interactive):1:15--1:16:x is not accessible in this context at:
|
||||
1 efn (\x, y => x) -- Bad
|
||||
^
|
||||
|
||||
Main> (interactive):1:5--1:9:When unifying Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat
|
||||
1 | efn (\x, y => x) -- Bad
|
||||
^
|
||||
Main> (interactive):1:5--1:9:When
|
||||
unifying Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat
|
||||
Mismatch between:
|
||||
Nat -> Nat -> Nat
|
||||
Nat -> Nat -> Nat
|
||||
and
|
||||
(0 _ : Nat) -> Nat -> Nat
|
||||
(0 _ : Nat) -> Nat -> Nat
|
||||
at:
|
||||
1 efn plus -- Bad
|
||||
^^^^
|
||||
|
||||
Main> (interactive):1:5--1:8:When unifying (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat
|
||||
1 | efn plus -- Bad
|
||||
^^^^
|
||||
Main> (interactive):1:5--1:8:When
|
||||
unifying (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat
|
||||
Mismatch between:
|
||||
(1 _ : Nat) -> Nat -> Nat
|
||||
(1 _ : Nat) -> Nat -> Nat
|
||||
and
|
||||
(0 _ : Nat) -> Nat -> Nat
|
||||
(0 _ : Nat) -> Nat -> Nat
|
||||
at:
|
||||
1 efn lin -- Bad
|
||||
^^^
|
||||
|
||||
1 | efn lin -- Bad
|
||||
^^^
|
||||
Main> (interactive):1:20--1:21:x is not accessible in this context at:
|
||||
1 efn (\x, y => plus x y) -- Bad
|
||||
^
|
||||
|
||||
1 | efn (\x, y => plus x y) -- Bad
|
||||
^
|
||||
Main> S (S Z)
|
||||
Main> S (S Z)
|
||||
Main> (interactive):1:6--1:12:When unifying (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat
|
||||
Main> (interactive):1:6--1:12:When
|
||||
unifying (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat
|
||||
Mismatch between:
|
||||
(0 _ : Nat) -> Nat -> Nat
|
||||
(0 _ : Nat) -> Nat -> Nat
|
||||
and
|
||||
Nat -> Nat -> Nat
|
||||
Nat -> Nat -> Nat
|
||||
at:
|
||||
1 okfn ignore -- Bad
|
||||
^^^^^^
|
||||
|
||||
1 | okfn ignore -- Bad
|
||||
^^^^^^
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
1/1: Building ZFun (ZFun.idr)
|
||||
ZFun.idr:13:7--13:15:While processing right hand side of bar at ZFun.idr:13:1--15:1:
|
||||
ZFun.idr:13:7--13:15:While processing right hand side
|
||||
of bar at ZFun.idr:13:1--15:1:
|
||||
Main.test is not accessible in this context at:
|
||||
13 bar = test foo -- bad!
|
||||
^^^^^^^^
|
||||
|
||||
13 | bar = test foo -- bad!
|
||||
^^^^^^^^
|
||||
Main> [tc] Main> 10
|
||||
[tc] Main> Bye for now!
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
1/1: Building LCase (LCase.idr)
|
||||
LCase.idr:7:11--10:13:While processing right hand side of foo at LCase.idr:6:1--12:1:
|
||||
LCase.idr:7:11--10:13:While processing right hand side
|
||||
of foo at LCase.idr:6:1--12:1:
|
||||
There are 0 uses of linear name y at:
|
||||
7 = let 1 test = the Nat $ case z of
|
||||
8 Z => Z
|
||||
9 (S k) => S z
|
||||
10 in
|
||||
|
||||
07 | = let 1 test = the Nat $ case z of
|
||||
08 | Z => Z
|
||||
09 | (S k) => S z
|
||||
10 | in
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
1/1: Building param (param.idr)
|
||||
1/1: Building parambad (parambad.idr)
|
||||
parambad.idr:7:7--7:10:While processing right hand side of U at parambad.idr:7:3--8:1:
|
||||
parambad.idr:7:7--7:10:While processing right hand side
|
||||
of U at parambad.idr:7:3--8:1:
|
||||
Name Main.X.foo is private at:
|
||||
7 U = foo
|
||||
^^^
|
||||
|
||||
7 | U = foo
|
||||
^^^
|
||||
|
||||
@ -1,8 +1,7 @@
|
||||
1/1: Building Dummy (Dummy.idr)
|
||||
Dummy> (interactive):1:4--1:13:Undefined name undefined at:
|
||||
1 :t undefined
|
||||
^^^^^^^^^
|
||||
|
||||
1 | :t undefined
|
||||
^^^^^^^^^
|
||||
Dummy> Dummy.something : String
|
||||
Dummy> "Something something"
|
||||
Dummy> Dummy.Proxy : Type -> Type
|
||||
|
||||
@ -1,13 +1,11 @@
|
||||
1/1: Building Main (Main.idr)
|
||||
Main.idr:41:5--43:1:complex postfix projections require %language PostfixProjections at:
|
||||
41 + rect.(x . topLeft) -- disallowed without %language PostfixProjections
|
||||
42
|
||||
43 bad2 : Double
|
||||
|
||||
41 | + rect.(x . topLeft) -- disallowed without %language PostfixProjections
|
||||
42 |
|
||||
43 | bad2 : Double
|
||||
Main.idr:44:9--44:24:postfix projection sections require %language PostfixProjections at:
|
||||
44 bad2 = (.oopFoldl 0 (+)) -- disallowed without %language PostfixProjections
|
||||
^^^^^^^^^^^^^^^
|
||||
|
||||
44 | bad2 = (.oopFoldl 0 (+)) -- disallowed without %language PostfixProjections
|
||||
^^^^^^^^^^^^^^^
|
||||
Main> 4.2
|
||||
Main> 4.2
|
||||
Main> 10.8
|
||||
@ -16,13 +14,12 @@ Main> 4.2
|
||||
Main> [1.1, 4.2]
|
||||
Main> (interactive):1:1--1:4:When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point
|
||||
Mismatch between:
|
||||
(?a -> ?b) -> ?f ?a -> ?f ?b
|
||||
(?a -> ?b) -> ?f ?a -> ?f ?b
|
||||
and
|
||||
Point
|
||||
Point
|
||||
at:
|
||||
1 map .x [MkPoint 1 2, MkPoint 3 4]
|
||||
^^^
|
||||
|
||||
1 | map .x [MkPoint 1 2, MkPoint 3 4]
|
||||
^^^
|
||||
Main> [2.5, 2.5]
|
||||
Main> 8.1
|
||||
Main> [8.1, 8.1]
|
||||
|
||||
@ -1,14 +1,14 @@
|
||||
1/1: Building quote (quote.idr)
|
||||
quote.idr:25:19--25:22:While processing right hand side of bad at quote.idr:22:1--27:1:
|
||||
quote.idr:25:19--25:22:While processing right hand side
|
||||
of bad at quote.idr:22:1--27:1:
|
||||
When unifying Int and TTImp
|
||||
Mismatch between:
|
||||
Int
|
||||
Int
|
||||
and
|
||||
TTImp
|
||||
TTImp
|
||||
at:
|
||||
25 xfn ~(val))
|
||||
^^^
|
||||
|
||||
25 | xfn ~(val))
|
||||
^^^
|
||||
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) (10, 28)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 28)) 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, 30)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 30)) (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)))))
|
||||
|
||||
@ -5,23 +5,23 @@ LOG 0: Name: Prelude.Types.Strings.++
|
||||
LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String))
|
||||
LOG 0: Resolved name: Prelude.Types.Nat
|
||||
LOG 0: Constructors: [Prelude.Types.Z, Prelude.Types.S]
|
||||
refprims.idr:43:10--43:27:While processing right hand side of dummy1 at refprims.idr:43:1--45:1:
|
||||
refprims.idr:43:10--43:27:While processing right hand side
|
||||
of dummy1 at refprims.idr:43:1--45:1:
|
||||
Error during reflection: Not really trying at:
|
||||
43 dummy1 = %runElab logPrims
|
||||
^^^^^^^^^^^^^^^^^
|
||||
|
||||
refprims.idr:46:10--46:30:While processing right hand side of dummy2 at refprims.idr:46:1--48:1:
|
||||
43 | dummy1 = %runElab logPrims
|
||||
^^^^^^^^^^^^^^^^^
|
||||
refprims.idr:46:10--46:30:While processing right hand side
|
||||
of dummy2 at refprims.idr:46:1--48:1:
|
||||
Error during reflection: Still not trying at:
|
||||
46 dummy2 = %runElab logDataCons
|
||||
^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
refprims.idr:49:10--49:25:While processing right hand side of dummy3 at refprims.idr:49:1--51:1:
|
||||
46 | dummy2 = %runElab logDataCons
|
||||
^^^^^^^^^^^^^^^^^^^^
|
||||
refprims.idr:49:10--49:25:While processing right hand side
|
||||
of dummy3 at refprims.idr:49:1--51:1:
|
||||
Error during reflection: Undefined name at:
|
||||
49 dummy3 = %runElab logBad
|
||||
^^^^^^^^^^^^^^^
|
||||
|
||||
refprims.idr:52:10--52:28:While processing right hand side of dummy4 at refprims.idr:52:1--54:1:
|
||||
49 | dummy3 = %runElab logBad
|
||||
^^^^^^^^^^^^^^^
|
||||
refprims.idr:52:10--52:28:While processing right hand side
|
||||
of dummy4 at refprims.idr:52:1--54:1:
|
||||
Error during reflection: failed after generating Main.{plus:XXXX} at:
|
||||
52 dummy4 = %runElab tryGenSym
|
||||
^^^^^^^^^^^^^^^^^^
|
||||
|
||||
52 | dummy4 = %runElab tryGenSym
|
||||
^^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,13 +1,13 @@
|
||||
1/1: Building refdecl (refdecl.idr)
|
||||
refdecl.idr:13:16--13:29:While processing right hand side of bad at refdecl.idr:13:1--14:1:
|
||||
refdecl.idr:13:16--13:29:While processing right hand side
|
||||
of bad at refdecl.idr:13:1--14:1:
|
||||
When unifying Elab () and Elab a
|
||||
Mismatch between:
|
||||
()
|
||||
()
|
||||
and
|
||||
a
|
||||
a
|
||||
at:
|
||||
13 bad = %runElab mkDecls `(94)
|
||||
^^^^^^^^^^^^^
|
||||
|
||||
13 | bad = %runElab mkDecls `(94)
|
||||
^^^^^^^^^^^^^
|
||||
Main> 9400
|
||||
Main> Bye for now!
|
||||
|
||||
@ -2,8 +2,8 @@
|
||||
LOG 0: [x, y]
|
||||
LOG 0: Left: ((Prelude.Types.plus x) y)
|
||||
LOG 0: Right: ((Prelude.Types.plus y) x)
|
||||
refleq.idr:24:16--24:21:While processing right hand side of commutes at refleq.idr:24:1--25:1:
|
||||
refleq.idr:24:16--24:21:While processing right hand side
|
||||
of commutes at refleq.idr:24:1--25:1:
|
||||
Error during reflection: Not done at:
|
||||
24 commutes x y = prove
|
||||
^^^^^
|
||||
|
||||
24 | commutes x y = prove
|
||||
^^^^^
|
||||
|
||||
@ -1,39 +1,31 @@
|
||||
1/1: Building Holes (Holes.idr)
|
||||
Holes.idr:4:64--4:85:While processing type of Vect_ext at Holes.idr:4:1--5:11:
|
||||
Undefined name ~=~ at:
|
||||
4 Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
|
||||
^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
|
||||
^^^^^^^^^^^^^^^^^^^^^
|
||||
Holes.idr:7:26--7:31:While processing type of Weird at Holes.idr:7:1--7:31:
|
||||
Undefined name ~=~ at:
|
||||
7 Weird : (v: Vect n a) -> v = v
|
||||
^^^^^
|
||||
|
||||
7 | Weird : (v: Vect n a) -> v = v
|
||||
^^^^^
|
||||
Holes.idr:8:1--10:1:No type declaration for Main.Weird at:
|
||||
8 Weird v = Vect_ext ?hole0 ?hole1 ?hole2
|
||||
9
|
||||
10 f : Bool -> Nat
|
||||
|
||||
08 | Weird v = Vect_ext ?hole0 ?hole1 ?hole2
|
||||
09 |
|
||||
10 | f : Bool -> Nat
|
||||
Holes.idr:10:5--10:9:While processing type of f at Holes.idr:10:1--10:16:
|
||||
Undefined name Bool at:
|
||||
10 f : Bool -> Nat
|
||||
^^^^
|
||||
|
||||
10 | f : Bool -> Nat
|
||||
^^^^
|
||||
Holes.idr:11:1--12:1:No type declaration for Main.f at:
|
||||
11 f True = 0
|
||||
12 f True = ?help
|
||||
|
||||
11 | f True = 0
|
||||
12 | f True = ?help
|
||||
Main> (interactive):1:4--1:8:Undefined name help at:
|
||||
1 :t help
|
||||
^^^^
|
||||
|
||||
1 | :t help
|
||||
^^^^
|
||||
Main> (interactive):1:4--1:9:Undefined name hole0 at:
|
||||
1 :t hole0
|
||||
^^^^^
|
||||
|
||||
1 | :t hole0
|
||||
^^^^^
|
||||
Main> (interactive):1:4--1:9:Undefined name hole1 at:
|
||||
1 :t hole1
|
||||
^^^^^
|
||||
|
||||
1 | :t hole1
|
||||
^^^^^
|
||||
Main> Unknown name hole1
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,10 +1,10 @@
|
||||
1/1: Building iftype (iftype.idr)
|
||||
iftype.idr:15:15--15:19:While processing right hand side of isInListBad at iftype.idr:15:1--16:1:
|
||||
iftype.idr:15:15--15:19:While processing right hand side
|
||||
of isInListBad at iftype.idr:15:1--16:1:
|
||||
Can't solve constraint between:
|
||||
if c then "Foo" else "Baz"
|
||||
if c then "Foo" else "Baz"
|
||||
and
|
||||
if c then "Foo" else "Bar"
|
||||
if c then "Foo" else "Bar"
|
||||
at:
|
||||
15 isInListBad = Here
|
||||
^^^^
|
||||
|
||||
15 | isInListBad = Here
|
||||
^^^^
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
1/1: Building Main (Main.idr)
|
||||
Main.idr:27:26--27:72:While processing right hand side of dpairWithExtraInfoBad at Main.idr:27:1--28:1:
|
||||
Main.idr:27:26--27:72:While processing right hand side
|
||||
of dpairWithExtraInfoBad at Main.idr:27:1--28:1:
|
||||
When unifying [MN 0, MN 0] and [MN 0]
|
||||
Mismatch between:
|
||||
[MN 0]
|
||||
[MN 0]
|
||||
and
|
||||
[]
|
||||
[]
|
||||
at:
|
||||
27 dpairWithExtraInfoBad = [([MN 0] ** CLocal {x=MN 0} (First {ns=[MN 0]}))]
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
27 | dpairWithExtraInfoBad = [([MN 0] ** CLocal {x=MN 0} (First {ns=[MN 0]}))]
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,20 +1,19 @@
|
||||
1/1: Building UnboundImplicits (UnboundImplicits.idr)
|
||||
UnboundImplicits.idr:6:22--6:23:While processing constructor Foo at UnboundImplicits.idr:6:1--9:1:
|
||||
UnboundImplicits.idr:6:22--6:23:While processing
|
||||
constructor Foo at UnboundImplicits.idr:6:1--9:1:
|
||||
Undefined name n at:
|
||||
6 record Foo (x : Vect n Nat) where
|
||||
^
|
||||
|
||||
6 | record Foo (x : Vect n Nat) where
|
||||
^
|
||||
UnboundImplicits.idr:9:24--9:25:Undefined name n at:
|
||||
9 parameters (Foo : Vect n Nat)
|
||||
^
|
||||
|
||||
UnboundImplicits.idr:14:25--14:26:While processing constructor Foo at UnboundImplicits.idr:14:1--15:12:
|
||||
9 | parameters (Foo : Vect n Nat)
|
||||
^
|
||||
UnboundImplicits.idr:14:25--14:26:While processing
|
||||
constructor Foo at UnboundImplicits.idr:14:1--15:12:
|
||||
Undefined name n at:
|
||||
14 interface Foo (a : Vect n Nat) where
|
||||
^
|
||||
|
||||
UnboundImplicits.idr:17:30--17:31:While processing type of Functor implementation at UnboundImplicits.idr:17:1--18:1 at UnboundImplicits.idr:17:1--18:1:
|
||||
14 | interface Foo (a : Vect n Nat) where
|
||||
^
|
||||
UnboundImplicits.idr:17:30--17:31:While processing type
|
||||
of Functor implementation at UnboundImplicits.idr:17:1--18:1 at UnboundImplicits.idr:17:1--18:1:
|
||||
Undefined name n at:
|
||||
17 implementation Functor (Vect n) where
|
||||
^
|
||||
|
||||
17 | implementation Functor (Vect n) where
|
||||
^
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
1/1: Building anyfail (anyfail.idr)
|
||||
anyfail.idr:21:1--21:48:showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is not a valid impossible case at:
|
||||
21 showing _ SomethingVeryComplicatedIs impossible
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
anyfail.idr:21:1--21:48:showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is
|
||||
not a valid impossible case at:
|
||||
21 | showing _ SomethingVeryComplicatedIs impossible
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
1/1: Building lammult (lammult.idr)
|
||||
lammult.idr:2:15--2:24:While processing right hand side of badmap at lammult.idr:2:1--3:1:
|
||||
lammult.idr:2:15--2:24:While processing right hand side
|
||||
of badmap at lammult.idr:2:1--3:1:
|
||||
When unifying (0 _ : ?a) -> ?b and ?a -> ?b
|
||||
Mismatch between:
|
||||
(0 _ : ?a) -> ?b
|
||||
(0 _ : ?a) -> ?b
|
||||
and
|
||||
?a -> ?b
|
||||
?a -> ?b
|
||||
at:
|
||||
2 badmap = map (\0 x => 2)
|
||||
^^^^^^^^^
|
||||
|
||||
2 | badmap = map (\0 x => 2)
|
||||
^^^^^^^^^
|
||||
|
||||
@ -1,28 +1,28 @@
|
||||
1/1: Building lazybug (lazybug.idr)
|
||||
lazybug.idr:5:22--5:34:While processing right hand side of main at lazybug.idr:5:1--7:1:
|
||||
lazybug.idr:5:22--5:34:While processing right hand side
|
||||
of main at lazybug.idr:5:1--7:1:
|
||||
Can't solve constraint between:
|
||||
Bool
|
||||
Bool
|
||||
and
|
||||
Lazy Bool
|
||||
Lazy Bool
|
||||
at:
|
||||
5 main = printLn $ or (map id bools)
|
||||
^^^^^^^^^^^^
|
||||
|
||||
lazybug.idr:8:23--8:42:While processing right hand side of main2 at lazybug.idr:8:1--10:1:
|
||||
5 | main = printLn $ or (map id bools)
|
||||
^^^^^^^^^^^^
|
||||
lazybug.idr:8:23--8:42:While processing right hand side
|
||||
of main2 at lazybug.idr:8:1--10:1:
|
||||
Can't solve constraint between:
|
||||
Bool
|
||||
Bool
|
||||
and
|
||||
Lazy Bool
|
||||
Lazy Bool
|
||||
at:
|
||||
8 main2 = printLn $ or (map (\x => x) bools)
|
||||
^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
lazybug.idr:14:22--14:27:While processing right hand side of main4 at lazybug.idr:14:1--15:1:
|
||||
8 | main2 = printLn $ or (map (\x => x) bools)
|
||||
^^^^^^^^^^^^^^^^^^^
|
||||
lazybug.idr:14:22--14:27:While processing right hand side
|
||||
of main4 at lazybug.idr:14:1--15:1:
|
||||
Can't solve constraint between:
|
||||
Bool
|
||||
Bool
|
||||
and
|
||||
Lazy Bool
|
||||
Lazy Bool
|
||||
at:
|
||||
14 main4 = printLn $ or bools
|
||||
^^^^^
|
||||
|
||||
14 | main4 = printLn $ or bools
|
||||
^^^^^
|
||||
|
||||
@ -1,10 +1,10 @@
|
||||
1/1: Building boom (boom.idr)
|
||||
boom.idr:23:42--23:66:While processing right hand side of with block in eraseVar at boom.idr:23:3--24:3:
|
||||
boom.idr:23:42--23:66:While processing right hand side
|
||||
of with block in eraseVar at boom.idr:23:3--24:3:
|
||||
Can't solve constraint between:
|
||||
S (countGreater thr xs)
|
||||
S (countGreater thr xs)
|
||||
and
|
||||
countGreater thr xs
|
||||
countGreater thr xs
|
||||
at:
|
||||
23 eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
23 | eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
@ -1,12 +1,11 @@
|
||||
1/1: Building partial (partial.idr)
|
||||
partial.idr:5:1--6:19:foo is not covering at:
|
||||
5 total
|
||||
6 foo : Maybe a -> a
|
||||
5 | total
|
||||
6 | foo : Maybe a -> a
|
||||
Missing cases:
|
||||
foo Nothing
|
||||
foo Nothing
|
||||
partial.idr:13:1--14:37:qsortBad is not total:
|
||||
possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad
|
||||
possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad
|
||||
at:
|
||||
13 total
|
||||
14 qsortBad : Ord a => List a -> List a
|
||||
|
||||
13 | total
|
||||
14 | qsortBad : Ord a => List a -> List a
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
1/1: Building partial (partial.idr)
|
||||
partial.idr:11:1--13:1:foo is not covering at:
|
||||
11 Foo (Maybe Int) where
|
||||
12 foo Nothing = ()
|
||||
11 | Foo (Maybe Int) where
|
||||
12 | foo Nothing = ()
|
||||
Missing cases:
|
||||
foo (Just _)
|
||||
foo (Just _)
|
||||
|
||||
@ -1,83 +1,77 @@
|
||||
1/1: Building Main (Main.idr)
|
||||
Main> (interactive):1:66--1:81:Sorry, I can't find any elaboration which works. All errors:
|
||||
Main> (interactive):1:66--1:81:Sorry, I can't find any elaboration which works. All
|
||||
errors:
|
||||
If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors:
|
||||
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
|
||||
Mismatch between:
|
||||
?_ -> IO ()
|
||||
?_ -> IO ()
|
||||
and
|
||||
IO ?b
|
||||
IO ?b
|
||||
at:
|
||||
1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^
|
||||
|
||||
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^
|
||||
|
||||
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b
|
||||
Mismatch between:
|
||||
?_ -> IO ()
|
||||
?_ -> IO ()
|
||||
and
|
||||
IO ?b
|
||||
IO ?b
|
||||
at:
|
||||
1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
|
||||
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
|
||||
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
|
||||
Mismatch between:
|
||||
?_ -> IO ()
|
||||
?_ -> IO ()
|
||||
and
|
||||
IO ?b
|
||||
IO ?b
|
||||
at:
|
||||
1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
|
||||
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
|
||||
Mismatch between:
|
||||
?_ -> IO ()
|
||||
?_ -> IO ()
|
||||
and
|
||||
IO ?b
|
||||
IO ?b
|
||||
at:
|
||||
1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^
|
||||
|
||||
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^
|
||||
|
||||
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b
|
||||
Mismatch between:
|
||||
?_ -> IO ()
|
||||
?_ -> IO ()
|
||||
and
|
||||
IO ?b
|
||||
IO ?b
|
||||
at:
|
||||
1 do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
|
||||
|
||||
Main> (interactive):1:61--1:66:Can't find an implementation for Num () at:
|
||||
1 with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^
|
||||
|
||||
1 | with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
|
||||
^^^^^
|
||||
Main> (interactive):1:4--1:6:Ambiguous elaboration at:
|
||||
1 :t []
|
||||
^^
|
||||
1 | :t []
|
||||
^^
|
||||
Possible correct results:
|
||||
PrimIO.Nil
|
||||
Prelude.Nil
|
||||
Data.Vect.Nil
|
||||
PrimIO.Nil
|
||||
Prelude.Nil
|
||||
Data.Vect.Nil
|
||||
Main> [] : Vect 0 ?elem
|
||||
Main> [] : List ?a
|
||||
Main> (interactive):1:34--1:41:When unifying Vect 0 ?elem and List ?a
|
||||
Mismatch between:
|
||||
Vect 0 ?elem
|
||||
Vect 0 ?elem
|
||||
and
|
||||
List ?a
|
||||
List ?a
|
||||
at:
|
||||
1 :t with [Vect.Nil, Prelude.(::)] [1,2,3]
|
||||
^^^^^^^
|
||||
|
||||
1 | :t with [Vect.Nil, Prelude.(::)] [1,2,3]
|
||||
^^^^^^^
|
||||
Main> the (Maybe Integer) (pure 4) : Maybe Integer
|
||||
Main> Parse error: Unrecognised command (next tokens: [identifier t, with, symbol [, symbol ], literal 4, end of input])
|
||||
Main> Bye for now!
|
||||
|
||||
@ -15,13 +15,13 @@ 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
|
||||
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
|
||||
9 foo Nat = "Nat"
|
||||
^^^
|
||||
|
||||
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:
|
||||
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:
|
||||
9 | foo Nat = "Nat"
|
||||
^^^
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
1/1: Building DLFail (DLFail.idr)
|
||||
DLFail.idr:3:20--3:29:While processing left hand side of describe_list_end at DLFail.idr:3:1--4:1:
|
||||
Can't match on ?xs ++ [?x] (Not a constructor application or primitive) at
|
||||
3 describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs
|
||||
^^^^^^^^^
|
||||
|
||||
DLFail.idr:3:20--3:29:While processing left hand side
|
||||
of describe_list_end at DLFail.idr:3:1--4:1:
|
||||
Can't match on ?xs ++ [?x] (Not a constructor application or primitive) at:
|
||||
3 | describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs
|
||||
^^^^^^^^^
|
||||
1/13: Building DataStore (DataStore.idr)
|
||||
2/13: Building DescribeList (DescribeList.idr)
|
||||
3/13: Building DescribeList2 (DescribeList2.idr)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user