2a70296 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical

2a70296David Raymond Christiansen12 years ago

Setup.hs+9−2

compare with master

unifiedsplit

@@ -57,6 +57,13 @@ usesGMP flags =

57 Just False -> False

58 Nothing -> True

60+execOnly :: S.ConfigFlags -> Bool

61+execOnly flags =

62+ case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of

63+ Just True -> True

64+ Just False -> False

65+ Nothing -> True

66+

60isRelease :: S.ConfigFlags -> Bool

67isRelease :: S.ConfigFlags -> Bool

61isRelease flags =

68isRelease flags =

62 case lookup (FlagName "release") (S.configConfigurationsFlags flags) of

69 case lookup (FlagName "release") (S.configConfigurationsFlags flags) of

@@ -176,7 +183,7 @@ getVersion args flags = do

176 let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo

183 let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo

177 return (Just buildinfo, [])

184 return (Just buildinfo, [])

178

185

179−idrisBuild _ flags _ local = do

186+idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do

180 buildStdLib

187 buildStdLib

181 buildRTS

188 buildRTS

182 where

189 where

@@ -199,7 +206,7 @@ idrisBuild _ flags _ local = do

199-- -----------------------------------------------------------------------------

206-- -----------------------------------------------------------------------------

200-- Copy/Install

207-- Copy/Install

201

208

202−idrisInstall verbosity copy pkg local = do

209+idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do

203 installStdLib

210 installStdLib

204 installRTS

211 installRTS

205 where

212 where

idris.cabal+5

@@ -658,6 +658,11 @@ Flag CI

658 Default: False

659 manual: True

660

661+Flag execonly

662+ Description: Build executables only, skip the libraries and RTS

663+ Default: False

664+ manual: True

665+

661Library

666Library

662 hs-source-dirs: src

667 hs-source-dirs: src

663 Exposed-modules:

668 Exposed-modules:

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

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

libs/prelude/Language/Reflection/Errors.idr+1

@@ -31,6 +31,7 @@ data Err = Msg String

31 | CantResolve TT

32 | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34+ | NoEliminator String TT

34 | UniverseError

35 | UniverseError

35 | ProgramLineComment

36 | ProgramLineComment

36 | Inaccessible TTName

37 | Inaccessible TTName

src/Idris/Core/Binary.hs+9−3

@@ -91,8 +91,8 @@ instance Binary a => Binary (Err' a) where

91 put x

92 put y

93 put z

94− put (CantResolve t) = do putWord8 15

94+ put (CantResolve _ t) = do putWord8 15

95− put t

95+ put t

96 put (CantResolveAlts ns) = do putWord8 16

97 put ns

98 put (IncompleteTerm t) = do putWord8 17

@@ -146,6 +146,9 @@ instance Binary a => Binary (Err' a) where

146 put x1

147 put x2

148 put x3

149+ put (NoEliminator s t) = do putWord8 37

150+ put s

151+ put t

149

152

150 get = do i <- getWord8

153 get = do i <- getWord8

151 case i of

154 case i of

@@ -172,7 +175,7 @@ instance Binary a => Binary (Err' a) where

172 13 -> fmap NoTypeDecl get

175 13 -> fmap NoTypeDecl get

173 14 -> do x <- get ; y <- get ; z <- get

176 14 -> do x <- get ; y <- get ; z <- get

174 return $ NotInjective x y z

177 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

178+ 15 -> fmap (CantResolve False) get

176 16 -> fmap CantResolveAlts get

179 16 -> fmap CantResolveAlts get

177 17 -> fmap IncompleteTerm get

180 17 -> fmap IncompleteTerm get

178 18 -> return UniverseError

181 18 -> return UniverseError

@@ -205,6 +208,9 @@ instance Binary a => Binary (Err' a) where

205 x2 <- get

208 x2 <- get

206 x3 <- get

209 x3 <- get

207 return (ElabDebug x1 x2 x3)

210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

208 _ -> error "Corrupted binary data for Err'"

214 _ -> error "Corrupted binary data for Err'"

209----- Generated by 'derive'

215----- Generated by 'derive'

210

216

src/Idris/Core/DeepSeq.hs+2−1

@@ -80,9 +80,10 @@ instance NFData Err where

80 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

81 rnf (NotInjective x1 x2 x3)

82 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

83− rnf (CantResolve x1) = rnf x1 `seq` ()

83+ rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

84 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

85 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

86+ rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

86 rnf UniverseError = ()

87 rnf UniverseError = ()

87 rnf ProgramLineComment = ()

88 rnf ProgramLineComment = ()

88 rnf (Inaccessible x1) = rnf x1 `seq` ()

89 rnf (Inaccessible x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+30−14

@@ -756,20 +756,20 @@ handleError p t1 t2 proofSearch

756

757try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

758try' t1 t2 proofSearch

759− = do s <- get

759+ = do s <- get

760− ps <- get_probs

760+ ps <- get_probs

761− ulog <- getUnifyLog

761+ ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

762+ case prunStateT 999999 False ps t1 s of

763− OK ((v, _, _), s') -> do put s'

763+ OK ((v, _, _), s') -> do put s'

764− return $! v

764+ return $! v

765− Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

765+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766− if recoverableErr e1 then

766+ if recoverableErr e1 then

767− do case runStateT t2 s of

767+ do case runStateT t2 s of

768− OK (v, s') -> do put s'; return $! v

768+ OK (v, s') -> do put s'; return $! v

769− Error e2 -> if score e1 >= score e2

769+ Error e2 -> if score e1 >= score e2

770− then lift (tfail e1)

770+ then lift (tfail e1)

771− else lift (tfail e2)

771+ else lift (tfail e2)

772− else lift (tfail e1)

772+ else lift (tfail e1)

773 where recoverableErr err@(CantUnify r x y _ _ _)

774 = -- traceWhen r (show err) $

775 r || proofSearch

@@ -782,6 +782,22 @@ try' t1 t2 proofSearch

782 recoverableErr (ElabDebug _ _ _) = False

783 recoverableErr _ = True

784

785+tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

791+ OK ((v, _, _), s') -> do put s'

792+ return $! v

793+ Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

794+ case runStateT (t2 e1) s of

795+ OK (v, s') -> do put s'

796+ return $! v

797+ Error e2 -> if score e1 >= score e2

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

785tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

801tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

786tryWhen True a b = try a b

802tryWhen True a b = try a b

787tryWhen False a b = a

803tryWhen False a b = a

src/Idris/Core/ProofState.hs+8−5

@@ -681,8 +681,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

681 (tmv, tmt) <- lift $ check ctxt env tm

682 let tmt' = normalise ctxt env tmt

683 let (tacn, tacstr, tactt) = if induction

684− then (ElimN, "an eliminator", "Induction")

684+ then (ElimN, "eliminator", "Induction")

685− else (CaseN, "a case function", "Case analysis")

685+ else (CaseN, "case analysis", "Case analysis")

686 case unApply tmt' of

687 (P _ tnm _, tyargs) -> do

688 case lookupTy (SN (tacn tnm)) ctxt of

@@ -717,9 +717,10 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

717 (scv, sct) <- lift $ check ctxt env res'

718 let (scv', _) = specialise ctxt env [] scv

719 return scv'

720− [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

720+ [] -> lift $ tfail $ NoEliminator tacstr tmt'

721 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

722− _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"

722+ _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")

723+ tmt'

723 where scname = sMN 0 "scarg"

724 where scname = sMN 0 "scarg"

724 makeConsArg (nm, ty) = P Bound nm ty

725 makeConsArg (nm, ty) = P Bound nm ty

725 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

726 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

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

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

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

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

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

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

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

942− 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') $

943 return (ps { pterm = tm',

946 return (ps { pterm = tm',

944 unified = (h, []),

947 unified = (h, []),

945 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+10−3

@@ -155,9 +155,11 @@ data Err' t

155 | WithFnType t

156 | NoTypeDecl Name

157 | NotInjective t t t

158− | CantResolve t

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

159+ t

159 | CantResolveAlts [Name]

160 | CantResolveAlts [Name]

160 | IncompleteTerm t

161 | IncompleteTerm t

162+ | NoEliminator String t

161 | UniverseError

163 | UniverseError

162 | UniqueError Universe Name

164 | UniqueError Universe Name

163 | UniqueKindError Universe Name

165 | UniqueKindError Universe Name

@@ -231,7 +233,7 @@ instance Sized Err where

231 size (NoSuchVariable name) = size name

233 size (NoSuchVariable name) = size name

232 size (NoTypeDecl name) = size name

234 size (NoTypeDecl name) = size name

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

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

234− size (CantResolve trm) = size trm

236+ size (CantResolve _ trm) = size trm

235 size (NoRewriting trm) = size trm

237 size (NoRewriting trm) = size trm

236 size (CantResolveAlts _) = 1

238 size (CantResolveAlts _) = 1

237 size (IncompleteTerm trm) = size trm

239 size (IncompleteTerm trm) = size trm

@@ -246,7 +248,7 @@ instance Sized Err where

246

248

247score :: Err -> Int

249score :: Err -> Int

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

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

249−score (CantResolve _) = 20

251+score (CantResolve _ _) = 20

250score (NoSuchVariable _) = 1000

252score (NoSuchVariable _) = 1000

251score (ProofSearchFail e) = score e

253score (ProofSearchFail e) = score e

252score (CantSolveGoal _ _) = 100000

254score (CantSolveGoal _ _) = 100000

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

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

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

935instantiate :: TT n -> TT n -> TT n

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

936instantiate e = subst 0 where

938instantiate e = subst 0 where

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

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

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

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

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

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

945-- that has been substituted.

948-- that has been substituted.

946substV :: TT n -> TT n -> TT n

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

947substV 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)

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

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

949 | otherwise = V x

953 | otherwise = V x

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

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

1038 -- substitution happens...)

1042 -- substitution happens...)

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

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

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

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

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

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

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

1043 (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

src/Idris/Delaborate.hs+7−1

@@ -289,7 +289,7 @@ pprintErr' i (NotInjective p x y) =

289 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

290 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

291 annTm y (pprintTerm i (delab i y))

292−pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

292+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

293pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

294 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

295pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

@@ -299,6 +299,12 @@ pprintErr' i (WithFnType ty) =

299pprintErr' i (CantMatch t) =

300 text "Can't match on" <+> annTm t (pprintTerm i (delab i t))

301pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

302+pprintErr' i (NoEliminator s t)

303+ = text "No " <> text s <> text " for type " <+>

304+ annTm t (pprintTerm i (delab i t)) <$>

305+ text "Please note that 'induction' is experimental." <$>

306+ text "Only types declared with '%elim' can be used." <$>

307+ text "Consider writing a pattern matching definition instead."

302pprintErr' i UniverseError = text "Universe inconsistency"

308pprintErr' i UniverseError = text "Universe inconsistency"

303pprintErr' i (UniqueError NullType n)

309pprintErr' i (UniqueError NullType n)

304 = text "Borrowed name" <+> annName' n (showbasic n)

310 = text "Borrowed name" <+> annName' n (showbasic n)

src/Idris/ElabTerm.hs+48−15

@@ -91,7 +91,7 @@ build ist info emode opts fn tm

91 mapM_ (\n -> when (n `elem` hs) $

92 do focus n

93 g <- goal

94− try (resolveTC True 7 g fn ist)

94+ try (resolveTC True False 7 g fn ist)

95 (movelast n)) ivs

96 ivs <- get_instances

97 hs <- get_holes

@@ -99,7 +99,7 @@ build ist info emode opts fn tm

99 mapM_ (\n -> when (n `elem` hs) $

100 do focus n

101 g <- goal

102− resolveTC True 7 g fn ist) ivs

102+ resolveTC True True 7 g fn ist) ivs

103 tm <- get_term

104 ctxt <- get_context

105 probs <- get_probs

@@ -350,7 +350,7 @@ elab ist info emode opts fn tm

350 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

351 _ -> elab' ina (Just fc) (PRef fc unitCon)

352 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

353− = do g <- goal; resolveTC False 5 g fn ist

353+ = do g <- goal; resolveTC False False 5 g fn ist

354 elab' ina fc (PResolveTC fc')

355 = do c <- getNameFrom (sMN 0 "class")

356 instanceArg c

@@ -569,7 +569,7 @@ elab ist info emode opts fn tm

569 g <- goal

570 hs <- get_holes

571 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

572− then try (resolveTC True 7 g fn ist)

572+ then try (resolveTC True False 7 g fn ist)

573 (movelast n)

574 else movelast n)

575 (ivs' \\ ivs)

@@ -729,7 +729,7 @@ elab ist info emode opts fn tm

729 env <- get_env

730 hs <- get_holes

731 if all (\n -> not (n `elem` hs)) (freeNames g)

732− then try (resolveTC False 7 g fn ist)

732+ then try (resolveTC False False 7 g fn ist)

733 (movelast n)

734 else movelast n)

735 (ivs' \\ ivs)

@@ -1405,14 +1405,25 @@ proofSearch' ist rec ambigok depth prv top n hints

1405-- Resolve type classes. This will only pick up 'normal' instances, never

1406-- named instances (hence using 'tcname' to check it's a generated instance

1407-- name).

1408+resolveTC :: Bool -- using default Int

1409+ -> Bool -- allow metavariables in the goal

1410+ -> Int -- depth

1411+ -> Term -- top level goal

1412+ -> Name -- top level function name

1408−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1413+ -> IState -> ElabD ()

1409resolveTC = resTC' []

1414resolveTC = resTC' []

1410

1415

1411−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

1416+resTC' tcs def mvok 0 topg fn ist = fail $ "Can't resolve type class"

1412−resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True

1417+resTC' tcs def mvok 1 topg fn ist = try' (trivial' ist) (resolveTC def mvok 0 topg fn ist) True

1413−resTC' tcs defaultOn depth topg fn ist

1418+resTC' tcs defaultOn mvok depth topg fn ist

1414− = do compute

1419+ = do compute

1415− g <- goal

1420+ g <- goal

1421+ hs <- get_holes

1422+ let argsok = tcArgsOK g hs

1423+-- trace (show (g,hs,argsok,mvok)) $

1424+ if (not argsok && not mvok)

1425+ then lift $ tfail $ CantResolve True topg

1426+ else do

1416 ptm <- get_term

1427 ptm <- get_term

1417 ulog <- getUnifyLog

1428 ulog <- getUnifyLog

1418 hs <- get_holes

1429 hs <- get_holes

@@ -1429,6 +1440,22 @@ resTC' tcs defaultOn depth topg fn ist

1429 let depth' = if scopeOnly then 2 else depth

1440 let depth' = if scopeOnly then 2 else depth

1430 blunderbuss t depth' stk (stk ++ insts)) True

1441 blunderbuss t depth' stk (stk ++ insts)) True

1431 where

1442 where

1443+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1444+ = True

1445+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1446+ = let (f, as) = unApply ty in

1447+ not $ any (isMeta hs) as

1448+

1449+ isMeta :: [Name] -> Term -> Bool

1450+ isMeta ns (P _ n _) = n `elem` ns

1451+ isMeta _ _ = False

1452+

1453+ notHole hs (P _ n _, c)

1454+ | (P _ cn _, _) <- unApply c,

1455+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1456+ | Constant _ <- c = not (n `elem` hs)

1457+ notHole _ _ = True

1458+

1432 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1459 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1433 | otherwise = (fail "Can't resolve", show n)

1460 | otherwise = (fail "Can't resolve", show n)

1434

1461

@@ -1456,10 +1483,13 @@ resTC' tcs defaultOn depth topg fn ist

1456

1483

1457 blunderbuss t d stk [] = do -- c <- get_env

1484 blunderbuss t d stk [] = do -- c <- get_env

1458 -- ps <- get_probs

1485 -- ps <- get_probs

1459− lift $ tfail $ CantResolve topg

1486+ lift $ tfail $ CantResolve False topg

1460 blunderbuss t d stk (n:ns)

1487 blunderbuss t d stk (n:ns)

1461 | n /= fn && (n `elem` stk || tcname n)

1488 | n /= fn && (n `elem` stk || tcname n)

1489+ = tryCatch (resolve n d)

1490+ (\e -> case e of

1491+ CantResolve True _ -> lift $ tfail e

1462− = try' (resolve n d) (blunderbuss t d stk ns) True

1492+ _ -> blunderbuss t d stk ns)

1463 | otherwise = blunderbuss t d stk ns

1493 | otherwise = blunderbuss t d stk ns

1464

1494

1465 resolve n depth

1495 resolve n depth

@@ -1488,7 +1518,7 @@ resTC' tcs defaultOn depth topg fn ist

1488 let got = fst (unApply t)

1518 let got = fst (unApply t)

1489 let depth' = if tc' `elem` tcs

1519 let depth' = if tc' `elem` tcs

1490 then depth - 1 else depth

1520 then depth - 1 else depth

1491− resTC' (got : tcs) defaultOn depth' topg fn ist)

1521+ resTC' (got : tcs) defaultOn mvok depth' topg fn ist)

1492 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1522 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1493 -- if there's any arguments left, we've failed to resolve

1523 -- if there's any arguments left, we've failed to resolve

1494 hs <- get_holes

1524 hs <- get_holes

@@ -2667,11 +2697,14 @@ reflectErr (NotInjective t1 t2 t3) =

2667 , reflect t2

2697 , reflect t2

2668 , reflect t3

2698 , reflect t3

2669 ]

2699 ]

2670−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2700+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2671reflectErr (CantResolveAlts ss) =

2701reflectErr (CantResolveAlts ss) =

2672 raw_apply (Var $ reflErrName "CantResolveAlts")

2702 raw_apply (Var $ reflErrName "CantResolveAlts")

2673 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2703 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2674reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2704reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2705+reflectErr (NoEliminator str t)

2706+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2707+ reflect t]

2675reflectErr UniverseError = Var $ reflErrName "UniverseError"

2708reflectErr UniverseError = Var $ reflErrName "UniverseError"

2676reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2709reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2677reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2710reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]