e1c7b0f · Idris-dev · git.iko.soy

src/Core/TT.hs+6−6

compare with master

unifiedsplit

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

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

44

45data 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

47 | NoSuchVariable Name

48 | NotInjective Term Term Term

49 | CantResolve Term

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

56

57instance Sized Err where

58 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

60 size (NoSuchVariable name) = size name

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

62 size (CantResolve trm) = size trm

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

67 size (Inaccessible _) = 1

68

69score :: Err -> Int

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

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

71score (CantResolve _) = 20

72score (NoSuchVariable _) = 1000

73score _ = 0

74

75instance Show Err where

76 show (Msg s) = s

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

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

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

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

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

80 show _ = "Error"

81

82instance Pretty Err where

83 pretty (Msg m) = text m

84− pretty (CantUnify l r e i) =

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

85 if size l + size r > breakingSize then

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

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

src/Core/Unify.hs+5−3

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

99 un' fn bnames x y

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

101 | 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

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

104 return [] -- lift $ tfail err

105

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

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

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

121 let err = CantUnify topx topy

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

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

123− s

123+ (errEnv env) s

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

125 return [] -- lift $ tfail err

126

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

132 sc 1

133 combine bnames as bs

134

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

136+

135holeIn :: Env -> Name -> Bool

137holeIn :: Env -> Name -> Bool

136holeIn env n = case lookup n env of

138holeIn env n = case lookup n env of

137 Just (Hole _) -> True

139 Just (Hole _) -> True

src/Idris/AbsSyntax.hs+31−1

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

29 opt_typeintype :: Bool,

30 opt_coverage :: Bool,

31 opt_showimp :: Bool,

32+ opt_errContext :: Bool,

32 opt_repl :: Bool,

33 opt_repl :: Bool,

33 opt_verbose :: Bool,

34 opt_verbose :: Bool,

34 opt_ibcsubdir :: FilePath,

35 opt_ibcsubdir :: FilePath,

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

36 }

37 }

37 deriving (Show, Eq)

38 deriving (Show, Eq)

38

39

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

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

40

41

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

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

42-- without typechecking).

43-- without typechecking).

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

281logLevel = do i <- get

282logLevel = do i <- get

282 return (opt_logLevel (idris_options i))

283 return (opt_logLevel (idris_options i))

283

284

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+

284useREPL :: Idris Bool

295useREPL :: Idris Bool

285useREPL = do i <- get

296useREPL = do i <- get

286 return (opt_repl (idris_options i))

297 return (opt_repl (idris_options i))

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

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

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

384 | Info Name | DebugInfo Name

395 | Info Name | DebugInfo Name

385 | Search PTerm

396 | Search PTerm

397+ | SetOpt Opt | UnsetOpt Opt

386 | NOP

398 | NOP

387

399

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+

388-- Parsed declarations

418-- Parsed declarations

389

419

390data Fixity = Infixl { prec :: Int }

420data Fixity = Infixl { prec :: Int }

src/Idris/Delaborate.hs+9−2

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

70

71pshow :: IState -> Err -> String

72pshow i (Msg s) = s

73−pshow i (CantUnify x y e s)

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

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

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

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

77 case e of

78 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

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

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

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

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

82 show (delab i y)

89 show (delab i y)

src/Idris/ElabDecls.hs−4

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

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

781 -- trace (show newd) $

782 decls ++ [newd]

783−

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

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

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

787 | otherwise = decls

783 | otherwise = decls

788

784

789 warnMissing decls ns meth

785 warnMissing decls ns meth

src/Idris/REPL.hs+11

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

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

245process fn NOP = return ()

246

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+

247classInfo :: ClassInfo -> Idris ()

256classInfo :: ClassInfo -> Idris ()

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

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

249 mapM_ dumpMethod (class_methods ci)

258 mapM_ dumpMethod (class_methods ci)

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

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

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

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

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

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

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

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

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

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

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

296 ]

307 ]

297

308

src/Idris/REPLParser.hs+6

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

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

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

41 <|> 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))

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

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

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

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

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

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

45 <|> do eof; return NOP

47 <|> do eof; return NOP

46

48

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

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

30-- on with the REPL.

31

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−

47main = do xs <- getArgs

32main = do xs <- getArgs

48 opts <- parseArgs xs

33 opts <- parseArgs xs

49 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

34 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

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

83 makeOption TypeCase = setTypeCase True

68 makeOption TypeCase = setTypeCase True

84 makeOption TypeInType = setTypeInType True

69 makeOption TypeInType = setTypeInType True

85 makeOption NoCoverage = setCoverage False

70 makeOption NoCoverage = setCoverage False

71+ makeOption ErrContext = setErrContext True

86 makeOption _ = return ()

72 makeOption _ = return ()

87

73

88getFile :: Opt -> Maybe String

74getFile :: Opt -> Maybe String

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

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

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

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

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

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

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

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

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

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

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

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

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

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