e1c7b0f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add "--errorcontext" flag, and :set and :unset in the REPL.

:set errorcontext will cause unification errors to also dump the current context.

commite1c7b0f75bc8b1d098163e6412ec82b3fe91dd0c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 1 May 2012, 16:03 (14 years ago) parent01dc619

8 files changed+70−31

compare with master

unifiedsplit

src/Core/TT.hs+6−6 src/Core/Unify.hs+5−3 src/Idris/AbsSyntax.hs+31−1 src/Idris/Delaborate.hs+9−2 src/Idris/ElabDecls.hs−4 src/Idris/REPL.hs+11 src/Idris/REPLParser.hs+6 src/Main.hs+2−15

src/Core/TT.hs+6−6

@@ -43,7 +43,7 @@ instance Show FC where

4343 show (FC f l) = f ++ ":" ++ show l

4444

4545data Err = Msg String

46− | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify

46+ | CantUnify Term Term Err [(Name, Type)] Int -- Int is 'score' - how much we did unify

4747 | NoSuchVariable Name

4848 | NotInjective Term Term Term

4949 | CantResolve Term

@@ -56,7 +56,7 @@ data Err = Msg String

5656

5757instance Sized Err where

5858 size (Msg msg) = length msg

59− size (CantUnify left right err score) = size left + size right + size err

59+ size (CantUnify left right err _ score) = size left + size right + size err

6060 size (NoSuchVariable name) = size name

6161 size (NotInjective l c r) = size l + size c + size r

6262 size (CantResolve trm) = size trm

@@ -67,21 +67,21 @@ instance Sized Err where

6767 size (Inaccessible _) = 1

6868

6969score :: Err -> Int

70−score (CantUnify _ _ m s) = s + score m

70+score (CantUnify _ _ m _ s) = s + score m

7171score (CantResolve _) = 20

7272score (NoSuchVariable _) = 1000

7373score _ = 0

7474

7575instance Show Err where

7676 show (Msg s) = s

77− show (CantUnify l r e i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

78− ++ show e ++ " " ++ show i

77+ show (CantUnify l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

78+ ++ show e ++ " in " ++ show sc ++ " " ++ show i

7979 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

8080 show _ = "Error"

8181

8282instance Pretty Err where

8383 pretty (Msg m) = text m

84− pretty (CantUnify l r e i) =

84+ pretty (CantUnify l r e _ i) =

8585 if size l + size r > breakingSize then

8686 text "Cannot unify" <+> colon $$

8787 nest nestingSize (pretty l <+> text "and" <+> pretty r) $$

src/Core/Unify.hs+5−3

@@ -99,7 +99,7 @@ unify ctxt env topx topy

9999 un' fn bnames x y

100100 | OK True <- convEq' ctxt x y = do sc 1; return []

101101 | otherwise = do UI s i f <- get

102− let err = CantUnify topx topy (CantUnify x y (Msg "") s) s

102+ let err = CantUnify topx topy (CantUnify x y (Msg "") [] s) (errEnv env) s

103103 put (UI s i ((x, y, env, err) : f))

104104 return [] -- lift $ tfail err

105105

@@ -119,8 +119,8 @@ unify ctxt env topx topy

119119 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

120120 uB bnames x y = do UI s i f <- get

121121 let err = CantUnify topx topy

122− (CantUnify (binderTy x) (binderTy y) (Msg "") s)

123− s

122+ (CantUnify (binderTy x) (binderTy y) (Msg "") [] s)

123+ (errEnv env) s

124124 put (UI s i ((binderTy x, binderTy y, env, err) : f))

125125 return [] -- lift $ tfail err

126126

@@ -132,6 +132,8 @@ unify ctxt env topx topy

132132 sc 1

133133 combine bnames as bs

134134

135+errEnv = map (\(x, b) -> (x, binderTy b))

136+

135137holeIn :: Env -> Name -> Bool

136138holeIn env n = case lookup n env of

137139 Just (Hole _) -> True

src/Idris/AbsSyntax.hs+31−1

@@ -29,6 +29,7 @@ data IOption = IOption { opt_logLevel :: Int,

2929 opt_typeintype :: Bool,

3030 opt_coverage :: Bool,

3131 opt_showimp :: Bool,

32+ opt_errContext :: Bool,

3233 opt_repl :: Bool,

3334 opt_verbose :: Bool,

3435 opt_ibcsubdir :: FilePath,

@@ -36,7 +37,7 @@ data IOption = IOption { opt_logLevel :: Int,

3637 }

3738 deriving (Show, Eq)

3839

39−defaultOpts = IOption 0 False False True False True True "" []

40+defaultOpts = IOption 0 False False True False False True True "" []

4041

4142-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

4243-- without typechecking).

@@ -281,6 +282,16 @@ logLevel :: Idris Int

281282logLevel = do i <- get

282283 return (opt_logLevel (idris_options i))

283284

285+setErrContext :: Bool -> Idris ()

286+setErrContext t = do i <- get

287+ let opts = idris_options i

288+ let opt' = opts { opt_errContext = t }

289+ put (i { idris_options = opt' })

290+

291+errContext :: Idris Bool

292+errContext = do i <- get

293+ return (opt_errContext (idris_options i))

294+

284295useREPL :: Idris Bool

285296useREPL = do i <- get

286297 return (opt_repl (idris_options i))

@@ -383,8 +394,27 @@ data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name

383394 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

384395 | Info Name | DebugInfo Name

385396 | Search PTerm

397+ | SetOpt Opt | UnsetOpt Opt

386398 | NOP

387399

400+data Opt = Filename String

401+ | Ver

402+ | Usage

403+ | NoPrelude

404+ | NoREPL

405+ | OLogging Int

406+ | Output String

407+ | TypeCase

408+ | TypeInType

409+ | NoCoverage

410+ | ErrContext

411+ | ShowImpl

412+ | Verbose

413+ | IBCSubDir String

414+ | ImportDir String

415+ deriving Eq

416+

417+

388418-- Parsed declarations

389419

390420data Fixity = Infixl { prec :: Int }

src/Idris/Delaborate.hs+9−2

@@ -70,13 +70,20 @@ delab' ist tm fullname = de [] tm

7070

7171pshow :: IState -> Err -> String

7272pshow i (Msg s) = s

73−pshow i (CantUnify x y e s)

73+pshow i (CantUnify x y e sc s)

7474 = "Can't unify " ++ show (delab i x)

7575 ++ " with " ++ show (delab i y) ++

7676-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

7777 case e of

7878 Msg "" -> ""

79− _ -> "\n\nSpecifically:\n\t " ++ pshow i e

79+ _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

80+ if (opt_errContext (idris_options i)) then showSc sc else ""

81+ where showSc [] = ""

82+ showSc xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

83+ showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)

84+ showbasic n@(UN _) = show n

85+ showbasic (MN _ s) = s

86+ showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

8087pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

8188 " when unifying " ++ show (delab i x) ++ " and " ++

8289 show (delab i y)

src/Idris/ElabDecls.hs−4

@@ -780,10 +780,6 @@ elabInstance info syn fc cs n ps t ds

780780 = let newd = expandParamsD i (\n -> meth) [] [def] clauses in

781781 -- trace (show newd) $

782782 decls ++ [newd]

783−

784−-- [PClauses fc [Inlinable,TCGen] meth

785−-- [PClause fc meth (PApp fc (PRef fc meth) []) []

786−-- (PApp fc (PRef fc def) []) []]]

787783 | otherwise = decls

788784

789785 warnMissing decls ns meth

src/Idris/REPL.hs+11

@@ -244,6 +244,15 @@ process fn Metavars

244244 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

245245process fn NOP = return ()

246246

247+process fn (SetOpt ErrContext) = setErrContext True

248+process fn (UnsetOpt ErrContext) = setErrContext False

249+process fn (SetOpt ShowImpl) = setImpShow True

250+process fn (UnsetOpt ShowImpl) = setImpShow False

251+

252+process fn (SetOpt _) = iputStrLn "Not a valid option"

253+process fn (UnsetOpt _) = iputStrLn "Not a valid option"

254+

255+

247256classInfo :: ClassInfo -> Idris ()

248257classInfo ci = do iputStrLn "Methods:\n"

249258 mapM_ dumpMethod (class_methods ci)

@@ -292,6 +301,8 @@ help =

292301 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

293302 ([":exec",":execute"], "", "Compile to an executable and run"),

294303 ([":?",":h",":help"], "", "Display this help text"),

304+ ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),

305+ ([":unset"], "<option>", "Unset an option"),

295306 ([":q",":quit"], "", "Exit the Idris system")

296307 ]

297308

src/Idris/REPLParser.hs+6

@@ -39,8 +39,14 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

3939 <|> try (do cmd ["u", "universes"]; eof; return Universes)

4040 <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))

4141 <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))

42+ <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

43+ <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

4244 <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))

4345 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

4446 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

4547 <|> do eof; return NOP

4648

49+pOption :: IParser Opt

50+pOption = do discard (symbol "errorcontext"); return ErrContext

51+ <|> do discard (symbol "showimplicits"); return ShowImpl

52+

src/Main.hs+2−15

@@ -29,21 +29,6 @@ import Paths_idris

2929-- Main program reads command line options, parses the main program, and gets

3030-- on with the REPL.

3131

32−data Opt = Filename String

33− | Ver

34− | Usage

35− | NoPrelude

36− | NoREPL

37− | OLogging Int

38− | Output String

39− | TypeCase

40− | TypeInType

41− | NoCoverage

42− | Verbose

43− | IBCSubDir String

44− | ImportDir String

45− deriving Eq

46−

4732main = do xs <- getArgs

4833 opts <- parseArgs xs

4934 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

@@ -83,6 +68,7 @@ runIdris opts =

8368 makeOption TypeCase = setTypeCase True

8469 makeOption TypeInType = setTypeInType True

8570 makeOption NoCoverage = setCoverage False

71+ makeOption ErrContext = setErrContext True

8672 makeOption _ = return ()

8773

8874getFile :: Opt -> Maybe String

@@ -119,6 +105,7 @@ parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns

119105parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

120106parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

121107parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)

108+parseArgs ("--errorcontext":ns) = liftM (ErrContext : ) (parseArgs ns)

122109parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

123110parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

124111parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)