9907240 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -278,7 +278,7 @@ addNameHint ty n

278 ty' <- case lookupCtxtName ty (idris_implicits i) of

279 [(tyn, _)] -> return tyn

280 [] -> throwError (NoSuchVariable ty)

281− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))

281+ tyns -> throwError (CantResolveAlts (map fst tyns))

282 let ns' = case lookupCtxt ty' (idris_namehints i) of

283 [ns] -> ns ++ [n]

284 _ -> [n]

src/Idris/Core/Elaborate.hs+1−1

@@ -710,7 +710,7 @@ tryAll :: [(Elab' aux a, String)] -> Elab' aux a

710tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

711 where

712 cantResolve :: Elab' aux a

713− cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

713+ cantResolve = lift $ tfail $ CantResolveTactics (map snd xs)

714

715 tryAll' :: [Elab' aux a] -> -- successes

716 Int -> -- most problems

src/Idris/Core/Evaluate.hs+10−5

@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTyName, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

@@ -863,14 +863,19 @@ lookupNames n ctxt

863 = let ns = lookupCtxtName n (definitions ctxt) in

864 map fst ns

865

866−lookupTy :: Name -> Context -> [Type]

866+lookupTyName :: Name -> Context -> [(Name, Type)]

867−lookupTy n ctxt

867+lookupTyName n ctxt = do

868− = do def <- lookupCtxt n (definitions ctxt)

868+ (name, def) <- lookupCtxtName n (definitions ctxt)

869− case tfst def of

869+ ty <- case tfst def of

870 (Function ty _) -> return ty

871 (TyDecl _ ty) -> return ty

872 (Operator ty _ _) -> return ty

873 (CaseOp _ ty _ _ _ _) -> return ty

874+ return (name, ty)

875+

876+

877+lookupTy :: Name -> Context -> [Type]

878+lookupTy n ctxt = map snd (lookupTyName n ctxt)

874

879

875isConName :: Name -> Context -> Bool

880isConName :: Name -> Context -> Bool

876isConName n ctxt = isTConName n ctxt || isDConName n ctxt

881isConName n ctxt = isTConName n ctxt || isDConName n ctxt

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

@@ -133,7 +133,8 @@ data Err' t

133 | NoTypeDecl Name

134 | NotInjective t t t

135 | CantResolve t

136− | CantResolveAlts [String]

136+ | CantResolveAlts [Name]

137+ | CantResolveTactics [String]

137 | IncompleteTerm t

138 | IncompleteTerm t

138 | UniverseError

139 | UniverseError

139 | ProgramLineComment

140 | ProgramLineComment

src/Idris/Delaborate.hs+3−1

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

195 pprintTerm i (delab i y)

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

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

198− align (cat (punctuate (comma <> space) (map text as)))

198+ align (cat (punctuate (comma <> space) (map annName as)))

199+pprintErr' i (CantResolveTactics ts) = text "Can't resolve tactics:" <+>

200+ align (cat (punctuate (comma <> space) (map text ts)))

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

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

200pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

202pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

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

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

src/Idris/ElabDecls.hs+1−1

@@ -2038,7 +2038,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2038 [c] -> return c

2039 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

2040 cs -> tclift $ tfail $ At fc

2041− (CantResolveAlts (map (show . fst) cs))

2041+ (CantResolveAlts (map fst cs))

2042 let constraint = PApp fc (PRef fc n) (map pexp ps)

2043 let iname = mkiname n ps expn

2044 let emptyclass = null (class_methods ci)

src/Idris/ElabTerm.hs+4−1

@@ -1587,7 +1587,10 @@ reflectErr (NotInjective t1 t2 t3) =

1587 ]

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

1589reflectErr (CantResolveAlts ss) =

1590− raw_apply (Var $ reflErrName "CantResolve")

1590+ raw_apply (Var $ reflErrName "CantResolveAlts")

1591+ [rawList (Var $ (sUN "String")) (map Var ss)]

1592+reflectErr (CantResolveTactics ss) =

1593+ raw_apply (Var $ reflErrName "CantResolveTactics")

1591 [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]

1594 [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]

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

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

1593reflectErr UniverseError = Var $ reflErrName "UniverseError"

1596reflectErr UniverseError = Var $ reflErrName "UniverseError"

src/Idris/Erasure.hs+1−1

@@ -109,7 +109,7 @@ performUsageAnalysis = do

109 getMainName ist = case lookupCtxtName n (idris_implicits ist) of

110 [(n', _)] -> Right n'

111 [] -> Left (NoSuchVariable n)

112− more -> Left (CantResolveAlts (map (show . fst) more))

112+ more -> Left (CantResolveAlts (map fst more))

113 where

114 n = sNS (sUN "main") ["Main"]

115

src/Idris/Interactive.hs+4−4

@@ -162,7 +162,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

162 mn <- case lookupNames n ctxt of

163 [x] -> return x

164 [] -> return n

165− ns -> ierror (CantResolveAlts (map show ns))

165+ ns -> ierror (CantResolveAlts ns)

166 i <- getIState

167 let (top, envlen, _) = case lookup mn (idris_metavars i) of

168 Just (t, e, False) -> (t, e, False)

@@ -242,10 +242,10 @@ makeLemma h fn updatefile l n

242 let isProv = checkProv tyline (show n)

243

244 ctxt <- getContext

245− mty <- case lookupTy n ctxt of

245+ mty <- case lookupTyName n ctxt of

246− [t] -> return t

246+ [(_,t)] -> return t

247 [] -> ierror (NoSuchVariable n)

248− ns -> ierror (CantResolveAlts (map show ns))

248+ ns -> ierror (CantResolveAlts (map fst ns))

249 i <- getIState

250

251 if (not isProv) then do

src/Idris/Parser.hs+1−1

@@ -1034,7 +1034,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1034 case lookupCtxtName n (idris_implicits i) of

1035 [(n', _)] -> return n'

1036 [] -> throwError (NoSuchVariable n)

1037− more -> throwError (CantResolveAlts (map (show . fst) more))

1037+ more -> throwError (CantResolveAlts (map fst more))

1038

1039pLangExt :: IdrisParser LanguageExt

1040pLangExt = (reserved "TypeProviders" >> return TypeProviders)

src/Idris/REPL.hs+2−2

@@ -510,7 +510,7 @@ resolveProof n'

510 n <- case lookupNames n' ctxt of

511 [x] -> return x

512 [] -> return n'

513− ns -> ierror (CantResolveAlts (map show ns))

513+ ns -> ierror (CantResolveAlts ns)

514 return n

515

516removeProof :: Name -> Idris ()

@@ -792,7 +792,7 @@ process h fn (Prove n')

792 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

793 [(n, (_,_,False))] -> return n

794 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

795− ns -> ierror (CantResolveAlts (map show ns))

795+ ns -> ierror (CantResolveAlts (map fst ns))

796 prover (lit fn) n

797 -- recheck totality

798 i <- getIState