9907240 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add new Err constructor to disambiguate the CantResolveAlts constructor.

(Ironic?) I did this to facilitate pretty printing of names when Idris cannot disambiguate among alternatives.

commit9907240f5ce10701a69729440f77d68807ca8af4 authorbmsherman <bmsherman@users.noreply.github.com> dateFri 30 May 2014, 22:21 (12 years ago) parentd61641d

11 files changed+30−19

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Core/Evaluate.hs+10−5 src/Idris/Core/TT.hs+2−1 src/Idris/Delaborate.hs+3−1 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+4−1 src/Idris/Erasure.hs+1−1 src/Idris/Interactive.hs+4−4 src/Idris/Parser.hs+1−1 src/Idris/REPL.hs+2−2

src/Idris/AbsSyntax.hs+1−1

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

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

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

280280 [] -> throwError (NoSuchVariable ty)

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

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

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

283283 [ns] -> ns ++ [n]

284284 _ -> [n]

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

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

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

711711 where

712712 cantResolve :: Elab' aux a

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

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

714714

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

716716 Int -> -- most problems

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

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

88 Context, initContext, ctxtAlist, uconstraints, next_tvar,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

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

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

1212 mapDefCtxt,

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

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

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

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

864864 map fst ns

865865

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

867−lookupTy n ctxt

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

869− case tfst def of

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

867+lookupTyName n ctxt = do

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

869+ ty <- case tfst def of

870870 (Function ty _) -> return ty

871871 (TyDecl _ ty) -> return ty

872872 (Operator ty _ _) -> return ty

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

874+ return (name, ty)

875+

876+

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

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

874879

875880isConName :: Name -> Context -> Bool

876881isConName n ctxt = isTConName n ctxt || isDConName n ctxt

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

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

133133 | NoTypeDecl Name

134134 | NotInjective t t t

135135 | CantResolve t

136− | CantResolveAlts [String]

136+ | CantResolveAlts [Name]

137+ | CantResolveTactics [String]

137138 | IncompleteTerm t

138139 | UniverseError

139140 | ProgramLineComment

src/Idris/Delaborate.hs+3−1

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

195195 pprintTerm i (delab i y)

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

197197pprintErr' 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)))

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

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

201203pprintErr' 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

20382038 [c] -> return c

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

20402040 cs -> tclift $ tfail $ At fc

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

2041+ (CantResolveAlts (map fst cs))

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

20432043 let iname = mkiname n ps expn

20442044 let emptyclass = null (class_methods ci)

src/Idris/ElabTerm.hs+4−1

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

15871587 ]

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

15891589reflectErr (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")

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

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

15931596reflectErr UniverseError = Var $ reflErrName "UniverseError"

src/Idris/Erasure.hs+1−1

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

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

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

111111 [] -> Left (NoSuchVariable n)

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

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

113113 where

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

115115

src/Idris/Interactive.hs+4−4

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

162162 mn <- case lookupNames n ctxt of

163163 [x] -> return x

164164 [] -> return n

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

165+ ns -> ierror (CantResolveAlts ns)

166166 i <- getIState

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

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

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

242242 let isProv = checkProv tyline (show n)

243243

244244 ctxt <- getContext

245− mty <- case lookupTy n ctxt of

246− [t] -> return t

245+ mty <- case lookupTyName n ctxt of

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

247247 [] -> ierror (NoSuchVariable n)

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

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

249249 i <- getIState

250250

251251 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

10341034 case lookupCtxtName n (idris_implicits i) of

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

10361036 [] -> throwError (NoSuchVariable n)

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

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

10381038

10391039pLangExt :: IdrisParser LanguageExt

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

src/Idris/REPL.hs+2−2

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

510510 n <- case lookupNames n' ctxt of

511511 [x] -> return x

512512 [] -> return n'

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

513+ ns -> ierror (CantResolveAlts ns)

514514 return n

515515

516516removeProof :: Name -> Idris ()

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

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

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

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

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

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

796796 prover (lit fn) n

797797 -- recheck totality

798798 i <- getIState