b894841 · Idris-dev · git.iko.soy

src/Core/TT.hs+4

compare with master

unifiedsplit

@@ -48,6 +48,8 @@ data Err = Msg String

48 -- Int is 'score' - how much we did unify

49 -- Bool indicates recoverability, True indicates more info may make

50 -- unification succeed

51+ | InfiniteUnify Name Term [(Name, Type)]

52+ | CantConvert Term Term [(Name, Type)]

51 | NoSuchVariable Name

53 | NoSuchVariable Name

52 | NoTypeDecl Name

54 | NoTypeDecl Name

53 | NotInjective Term Term Term

55 | NotInjective Term Term Term

@@ -64,6 +66,8 @@ instance Sized Err where

64 size (Msg msg) = length msg

66 size (Msg msg) = length msg

65 size (InternalMsg msg) = length msg

67 size (InternalMsg msg) = length msg

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

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

69+ size (InfiniteUnify _ right _) = size right

70+ size (CantConvert left right _) = size left + size right

67 size (NoSuchVariable name) = size name

71 size (NoSuchVariable name) = size name

68 size (NoTypeDecl name) = size name

72 size (NoTypeDecl name) = size name

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

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

src/Core/Typecheck.hs+8−6

@@ -19,17 +19,19 @@ convertsC ctxt env x y

19 = do c <- convEq ctxt (finalise (normalise ctxt env x))

20 (finalise (normalise ctxt env y))

21 if c then return ()

22− else fail ("Can't convert between " ++

22+ else lift $ tfail (CantConvert

23− showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

23+ (finalise (normalise ctxt env x))

24− showEnv env (finalise (normalise ctxt env y)))

24+ (finalise (normalise ctxt env y)) (errEnv env))

25

26converts :: Context -> Env -> Term -> Term -> TC ()

27converts ctxt env x y = if (finalise (normalise ctxt env x) ==

28 finalise (normalise ctxt env y))

29 then return ()

30− else fail ("Can't convert between " ++

30+ else tfail (CantConvert

31− showEnvDbg env (finalise (normalise ctxt env x)) ++ " and " ++

31+ (finalise (normalise ctxt env x))

32− showEnvDbg env (finalise (normalise ctxt env y)))

32+ (finalise (normalise ctxt env y)) (errEnv env))

33+

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

33

35

34isSet :: Context -> Env -> Term -> TC ()

36isSet :: Context -> Env -> Term -> TC ()

35isSet ctxt env tm = isSet' (normalise ctxt env tm)

37isSet ctxt env tm = isSet' (normalise ctxt env tm)

src/Core/Unify.hs+7−2

@@ -77,12 +77,12 @@ unify ctxt env topx topy

77 | holeIn env x = do UI s i f <- get

78 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)

79 sc 1

80− return [(x, tm)]

80+ checkCycle (x, tm)

81 un' fn bnames tm (P Bound y _)

82 | holeIn env y = do UI s i f <- get

83 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)

84 sc 1

85− return [(y, tm)]

85+ checkCycle (y, tm)

86 un' fn bnames (V i) (P Bound x _)

87 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

88 un' fn bnames (P Bound x _) (V i)

@@ -165,6 +165,11 @@ unify ctxt env topx topy

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

166 return [] -- lift $ tfail err

167

168+ checkCycle p@(x, P _ _ _) = return [p]

169+ checkCycle (x, tm)

170+ | not (x `elem` freeNames tm) = return [(x, tm)]

171+ | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

172+

168 combine bnames as [] = return as

173 combine bnames as [] = return as

169 combine bnames as ((n, t) : bs)

174 combine bnames as ((n, t) : bs)

170 = case lookup n as of

175 = case lookup n as of

src/Idris/Delaborate.hs+15−7

@@ -83,13 +83,14 @@ pshow i (CantUnify _ x y e sc s)

83 case e of

84 Msg "" -> ""

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

86− if (opt_errContext (idris_options i)) then showSc sc else ""

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

87− where showSc [] = ""

87+pshow i (CantConvert x y env)

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

88+ = "Can't unify " ++ show (delab i x) ++ " with " ++ show (delab i y) ++

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

89+ if (opt_errContext (idris_options i)) then showSc i env else ""

90− showbasic n@(UN _) = show n

90+pshow i (InfiniteUnify x tm env)

91− showbasic (MN _ s) = s

91+ = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

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

92+ " would lead to infinite value" ++

93+ if (opt_errContext (idris_options i)) then showSc i env else ""

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

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

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

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

95 show (delab i y)

96 show (delab i y)

@@ -103,3 +104,10 @@ pshow i ProgramLineComment = "Program line next to comment"

103pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

104pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

104pshow i (At f e) = show f ++ ":" ++ pshow i e

105pshow i (At f e) = show f ++ ":" ++ pshow i e

105

106

107+showSc i [] = ""

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

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

110+

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

112+showbasic (MN _ s) = s

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

src/Idris/ElabDecls.hs+4−5

@@ -241,7 +241,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

241 tree@(CaseDef scargs sc _) <- tclift $ simpleCase tcase False CompileTime fc pdef

242 tclift $ sameLength pdef

243 cov <- coverage

244− pcover <-

244+ pmissing <-

245 if cov

246 then do -- missing <- genClauses fc n (map getLHS pdef) cs

247 missing <- genMissing n scargs sc

@@ -250,10 +250,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

250 showSep "\n" (map (showImp True) missing') ++

251 "\nAgainst: " ++

252 showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))

253− if null missing'

253+ return missing'

254− then return True

255− else return False

256− else return False

254+ else return []

255+ let pcover = null pmissing

257 pdef' <- applyOpts pdef

256 pdef' <- applyOpts pdef

258 ist <- get

257 ist <- get

259-- let wf = wellFounded ist n sc

258-- let wf = wellFounded ist n sc