c66df51 · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr+1

compare with master

unifiedsplit

@@ -272,6 +272,7 @@ instance Show Err where

272 show (CantResolve tm) = "CantResolve " ++ show tm

273 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs

274 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm

275+ show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm

275 show UniverseError = "UniverseError"

276 show UniverseError = "UniverseError"

276 show ProgramLineComment = "ProgramLineComment"

277 show ProgramLineComment = "ProgramLineComment"

277 show (Inaccessible n) = "Inaccessible " ++ show n

278 show (Inaccessible n) = "Inaccessible " ++ show n

src/Idris/Core/ProofState.hs+3−1

@@ -940,7 +940,9 @@ processTactic EndUnify ps

940 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

941 (ns'', probs') = updateProblems ps ns' (problems ps)

942 tm' = updateSolved ns'' (pterm ps) in

943− traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $

943+ traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'') ++ "\n" ++

944+ show (pterm ps) ++ "\n" ++

945+ show tm') $

944 return (ps { pterm = tm',

946 return (ps { pterm = tm',

945 unified = (h, []),

947 unified = (h, []),

946 problems = probs',

948 problems = probs',

src/Idris/Core/ProofTerm.hs+3

@@ -172,6 +172,9 @@ updateSolvedTerm' xs x = updateSolved' xs x where

172 else (t, False)

173 updateSolved' xs t@(P _ n@(MN _ _) _)

174 | Just v <- lookup n xs = (v, True)

175+ updateSolved' xs t@(P nt n ty)

176+ = let (ty', ut) = updateSolved' xs ty in

177+ if ut then (P nt n ty', True) else (t, False)

175 updateSolved' xs t = (t, False)

178 updateSolved' xs t = (t, False)

176

179

177 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

180 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

src/Idris/Core/TT.hs+6−1

@@ -155,7 +155,7 @@ data Err' t

155 | WithFnType t

156 | NoTypeDecl Name

157 | NotInjective t t t

158− | CantResolve Bool -- ^ True if postponed, False if fatal

158+ | CantResolve Bool -- True if postponed, False if fatal

159 t

160 | CantResolveAlts [Name]

161 | IncompleteTerm t

@@ -936,6 +936,7 @@ vinstances i t = 0

936-- | Replace the outermost (index 0) de Bruijn variable with the given term

937instantiate :: TT n -> TT n -> TT n

938instantiate e = subst 0 where

939+ subst i (P nt x ty) = P nt x (subst i ty)

939 subst i (V x) | i == x = e

940 subst i (V x) | i == x = e

940 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

941 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

941 subst i (App f a) = App (subst i f) (subst i a)

942 subst i (App f a) = App (subst i f) (subst i a)

@@ -947,6 +948,7 @@ instantiate e = subst 0 where

947-- that has been substituted.

948-- that has been substituted.

948substV :: TT n -> TT n -> TT n

949substV :: TT n -> TT n -> TT n

949substV x tm = dropV 0 (instantiate x tm) where

950substV x tm = dropV 0 (instantiate x tm) where

951+ subst i (P nt x ty) = P nt x (subst i ty)

950 dropV i (V x) | x > i = V (x - 1)

952 dropV i (V x) | x > i = V (x - 1)

951 | otherwise = V x

953 | otherwise = V x

952 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

954 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

@@ -1040,6 +1042,9 @@ subst n v tm = fst $ subst' 0 tm

1040 -- substitution happens...)

1042 -- substitution happens...)

1041 subst' i (V x) | i == x = (v, True)

1043 subst' i (V x) | i == x = (v, True)

1042 subst' i (P _ x _) | n == x = (v, True)

1044 subst' i (P _ x _) | n == x = (v, True)

1045+ subst' i t@(P nt x ty)

1046+ = let (ty', ut) = subst' i ty in

1047+ if ut then (P nt x ty', True) else (t, False)

1043 subst' i t@(Bind x b sc) | x /= n

1048 subst' i t@(Bind x b sc) | x /= n

1044 = let (b', ub) = substB' i b

1049 = let (b', ub) = substB' i b

1045 (sc', usc) = subst' (i+1) sc in

1050 (sc', usc) = subst' (i+1) sc in

src/Idris/Core/Unify.hs+2−2

@@ -100,7 +100,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

100 | (P (TCon _ _) _ _, _) <- unApply x,

101 holeIn env f || f `elem` holes

102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

103− checkCycle names (f, Bind n' (Lam t) x)

103+ checkCycle names (f, Bind n' (Lam t) x)

104 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

105 | (P (TCon _ _) _ _, _) <- unApply x,

106 holeIn env f || f `elem` holes

@@ -110,7 +110,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

110 | (P (DCon _ _ _) _ _, _) <- unApply x,

111 holeIn env f || f `elem` holes

112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

113− checkCycle names (f, Bind n' (Lam t) x)

113+ checkCycle names (f, Bind n' (Lam t) x)

114 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

115 | (P (DCon _ _ _) _ _, _) <- unApply x,

116 holeIn env f || f `elem` holes