edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-03 10:14:53 +03:00
Code Issues Projects Releases Wiki Activity

Add errors, REPLCommon now builds

Browse Source
This commit is contained in:
Edwin Brady 2019-06-01 15:53:16 +01:00
parent 2e2622c38b
commit d82f6c5080
5 changed files with 71 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Core/Context.idr
View File

@ -1113,6 +1113,13 @@ getPPrint
= do defs <- get Ctxt
pure (printing (options defs))
export
setPPrint : {auto c : Ref Ctxt Defs} ->
PPrinter -> Core ()
setPPrint ppopts
= do defs <- get Ctxt
put Ctxt (record { options->printing = ppopts } defs)
export
getDirs : {auto c : Ref Ctxt Defs} -> Core Dirs
getDirs

34
src/Core/Core.idr
View File

@ -37,8 +37,8 @@ data Error
| InvisibleName FC Name
| BadTypeConType FC Name
| BadDataConType FC Name Name
-- | NotCovering FC Name Covering
-- | NotTotal FC Name PartialReason
| NotCovering FC Name Covering
| NotTotal FC Name PartialReason
| LinearUsed FC Nat Name
| LinearMisuse FC Name RigCount RigCount
| BorrowPartial FC (Env Term vars) (Term vars) (Term vars)
@ -120,19 +120,19 @@ Show Error where
= show fc ++ ":Return type of " ++ show n ++ " must be Type"
show (BadDataConType fc n fam)
= show fc ++ ":Return type of " ++ show n ++ " must be in " ++ show fam
-- show (NotCovering fc n cov)
-- = show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++
-- case cov of
-- IsCovering => "Oh yes it is (Internal error!)"
-- MissingCases cs => "Missing cases:\n\t" ++
-- showSep "\n\t" (map show cs)
-- NonCoveringCall ns => "Calls non covering function"
-- ++ (case ns of
-- [fn] => " " ++ show fn
-- _ => "s: " ++ showSep ", " (map show ns))
--
-- show (NotTotal fc n r)
-- = show fc ++ ":" ++ show n ++ " is not total"
show (NotCovering fc n cov)
= show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++
case cov of
IsCovering => "Oh yes it is (Internal error!)"
MissingCases cs => "Missing cases:\n\t" ++
showSep "\n\t" (map show cs)
NonCoveringCall ns => "Calls non covering function"
++ (case ns of
[fn] => " " ++ show fn
_ => "s: " ++ showSep ", " (map show ns))
show (NotTotal fc n r)
= show fc ++ ":" ++ show n ++ " is not total"
show (LinearUsed fc count n)
= show fc ++ ":There are " ++ show count ++ " uses of linear name " ++ show n
show (LinearMisuse fc n exp ctx)
@ -251,8 +251,8 @@ getErrorLoc (UndefinedName loc y) = Just loc
getErrorLoc (InvisibleName loc y) = Just loc
getErrorLoc (BadTypeConType loc y) = Just loc
getErrorLoc (BadDataConType loc y z) = Just loc
-- getErrorLoc (NotCovering loc _ _) = Just loc
-- getErrorLoc (NotTotal loc _ _) = Just loc
getErrorLoc (NotCovering loc _ _) = Just loc
getErrorLoc (NotTotal loc _ _) = Just loc
getErrorLoc (LinearUsed loc k y) = Just loc
getErrorLoc (LinearMisuse loc y z w) = Just loc
getErrorLoc (BorrowPartial loc _ _ _) = Just loc

10
src/Core/Options.idr
View File

@ -172,6 +172,16 @@ defaults = MkOptions defaultDirs defaultPPrint defaultSession
(MkPrimNs Nothing Nothing Nothing)
[] []
-- Reset the options which are set by source files
export
clearNames : Options -> Options
clearNames = record { pairnames = Nothing,
rewritenames = Nothing,
primnames = MkPrimNs Nothing Nothing Nothing,
namedirectives = [],
extensions = []
}
export
setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
Options -> Options

51
src/Idris/Error.idr
View File

@ -3,6 +3,7 @@ module Idris.Error
import Core.CaseTree
import Core.Core
import Core.Context
import Core.Env
import Core.Options
import Idris.Resugar
@ -14,15 +15,15 @@ import Parser.Support
pshow : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Env Term vars -> Term vars -> Core FC String
Env Term vars -> Term vars -> Core String
pshow env tm
= do defs <- get Ctxt
itm <- resugar env (normaliseHoles defs env tm)
itm <- resugar env !(normaliseHoles defs env tm)
pure (show itm)
pshowNoNorm : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Env Term vars -> Term vars -> Core FC String
Env Term vars -> Term vars -> Core String
pshowNoNorm env tm
= do defs <- get Ctxt
itm <- resugar env tm
@ -31,17 +32,18 @@ pshowNoNorm env tm
export
perror : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Error FC -> Core FC String
{-
Error -> Core String
perror (Fatal err) = perror err
perror (CantConvert _ env l r)
= pure $ "Mismatch between:\n\t" ++ !(pshow env l) ++ "\nand\n\t" ++ !(pshow env r)
perror (CantSolveEq _ env l r)
= pure $ "Can't solve constraint between:\n\t" ++ !(pshow env l) ++
"\nand\n\t" ++ !(pshow env r)
perror (Cycle _ env l r)
= pure $ "Solving constraint between:\n\t" ++ !(pshow env l) ++
"\nand\n\t" ++ !(pshow env r) ++ "\nwould lead to infinite value"
perror (PatternVariableUnifies _ env n tm)
= pure $ "Pattern variable " ++ show n ++
"unifies with:\n\t" ++ !(pshow env tm)
perror (CyclicMeta _ n)
= pure $ "Cycle detected in solution of metavariable " ++ show n
perror (WhenUnifying _ env x y err)
= pure $ "When unifying " ++ !(pshow env x) ++ " and " ++ !(pshow env y) ++ "\n"
++ !(perror err)
@ -80,14 +82,12 @@ perror (LinearMisuse fc n exp ctx)
where
showRig : RigCount -> String
showRig Rig0 = "irrelevant"
showRig (Rig1 False) = "linear"
showRig (Rig1 True) = "borrowed"
showRig Rig1 = "linear"
showRig RigW = "unrestricted"
showRel : RigCount -> String
showRel Rig0 = "irrelevant"
showRel (Rig1 False) = "relevant"
showRel (Rig1 True) = "borrowed"
showRel Rig1 = "relevant"
showRel RigW = "non-linear"
perror (BorrowPartial fc env tm arg)
= pure $ !(pshow env tm) ++
@ -113,13 +113,13 @@ perror (AllFailed ts)
_ => pure $ "Sorry, I can't find any elaboration which works. All errors:\n" ++
showSep "\n" !(traverse pAlterror ts)
where
pAlterror : (Maybe Name, Error FC) -> Core FC String
pAlterror : (Maybe Name, Error) -> Core String
pAlterror (Just n, err)
= pure $ "If " ++ show n ++ ": " ++ !(perror err) ++ "\n"
pAlterror (Nothing, err)
= pure $ "Possible error:\n\t" ++ !(perror err)
allUndefined : List (Maybe Name, Error FC) -> Maybe (Error FC)
allUndefined : List (Maybe Name, Error) -> Maybe Error
allUndefined [] = Nothing
allUndefined [(_, UndefinedName loc e)] = Just (UndefinedName loc e)
allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es
@ -135,26 +135,29 @@ perror (NotRecordType fc ty)
perror (IncompatibleFieldUpdate fc flds)
= pure $ "Field update " ++ showSep "->" flds ++
" not compatible with other updates"
perror (InvalidImplicit _ env n tm)
perror (InvalidImplicits _ env [n] tm)
= pure $ show n ++ " is not a valid implicit argument in " ++ !(pshow env tm)
perror (InvalidImplicits _ env ns tm)
= pure $ showSep ", " (map show ns) ++
" are not valid implicit arguments in " ++ !(pshow env tm)
perror (TryWithImplicits _ env imps)
= pure $ "Need to bind implicits "
++ showSep ", " !(traverse (tshow env) imps)
where
tshow : Env Term vars -> (Name, Term vars) -> Core FC String
tshow : Env Term vars -> (Name, Term vars) -> Core String
tshow env (n, ty) = pure $ show n ++ " : " ++ !(pshow env ty)
perror (CantSolveGoal _ g)
= let (_ ** (env', g')) = dropPis [] g in
perror (CantSolveGoal _ env g)
= let (_ ** (env', g')) = dropPis env g in
pure $ "Can't find an implementation for " ++ !(pshow env' g')
where
-- For display, we don't want to see the full top level type; just the
-- return type
dropPis : Env Term vars -> Term vars ->
(ns ** (Env Term ns, Term ns))
dropPis env (Bind n b@(Pi _ _ _) sc) = dropPis (b :: env) sc
dropPis env (Bind _ n b@(Pi _ _ _) sc) = dropPis (b :: env) sc
dropPis env tm = (_ ** (env, tm))
perror (DeterminingArg _ n env g)
perror (DeterminingArg _ 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
perror (UnsolvedHoles hs)
@ -229,11 +232,11 @@ perror (InLHS fc n err)
perror (InRHS fc n err)
= pure $ "While processing right hand side of " ++ show (sugarName n) ++
" at " ++ show fc ++ ":\n" ++ !(perror err)
-}
export
display : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Error FC -> Core FC String
display err = pure $ maybe "" (\f => show f ++ ":") (getAnnot err) ++
!(perror err)
Error -> Core String
display err
= pure $ maybe "" (\f => show f ++ ":") (getErrorLoc err) ++
!(perror err)

20
src/Idris/REPLCommon.idr
View File

@ -54,7 +54,7 @@ export
emitError : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
{auto s : Ref Syn SyntaxInfo} ->
Error FC -> Core FC ()
Error -> Core ()
emitError err
= do opts <- get ROpts
case idemode opts of
@ -63,7 +63,7 @@ emitError err
coreLift $ putStrLn msg
IDEMode i _ f =>
do msg <- perror err
case getAnnot err of
case getErrorLoc err of
Nothing => iputStrLn msg
Just fc =>
send f (SExpList [SymbolAtom "warning",
@ -83,26 +83,26 @@ getFCLine fc = fst (startPos fc)
export
updateErrorLine : {auto o : Ref ROpts REPLOpts} ->
List (Error FC) -> Core FC ()
List Error -> Core ()
updateErrorLine []
= do opts <- get ROpts
put ROpts (record { errorLine = Nothing } opts)
updateErrorLine (e :: es)
= do opts <- get ROpts
put ROpts (record { errorLine = map getFCLine (getAnnot e) } opts)
put ROpts (record { errorLine = map getFCLine (getErrorLoc e) } opts)
export
resetContext : {auto u : Ref Ctxt Defs} ->
{auto u : Ref UST (UState FC)} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref Meta (Metadata FC)} ->
Core FC ()
{auto m : Ref MD Metadata} ->
Core ()
resetContext
= do defs <- get Ctxt
put Ctxt (record { options = clearNames (options defs) } initCtxt)
put Ctxt (record { options = clearNames (options defs) } !initDefs)
addPrimitives
put UST initUState
put Syn initSyntax
put Meta initMetadata
put Syn !initSyntax
put MD initMetadata