c6771d2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1884 from david-christiansen/color-issue

c6771d2David Christiansen12 years ago

src/Idris/AbsSyntax.hs+5−1

compare with master

unifiedsplit

@@ -1734,7 +1734,11 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1734 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

1735 = Placeholder

1736 su (PApp fc f@(PRef _ fn) args)

1737− | isDConName fn ctxt

1737+ -- here we use canBeDConName because the impossible pattern

1738+ -- check will not necessarily fully resolve constructor names,

1739+ -- and these bare names will otherwise get in the way of

1740+ -- impossbility checking.

1741+ | canBeDConName fn ctxt

1738 = PApp fc f (fmap (fmap su) args)

1742 = PApp fc f (fmap (fmap su) args)

1739 su (PApp fc f args)

1743 su (PApp fc f args)

1740 = PHidden (PApp fc f args)

1744 = PHidden (PApp fc f args)

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

@@ -173,30 +173,30 @@ elaborating_app = do ES (ps, _) _ _ <- get

173

174-- Some handy gadgets for pulling out bits of state

175

176−-- get the global context

176+-- | Get the global context

177get_context :: Elab' aux Context

178get_context = do ES p _ _ <- get

179 return $! (context (fst p))

180

181−-- update the context

181+-- | Update the context.

182-- (should only be used for adding temporary definitions or all sorts of

183-- stuff could go wrong)

184set_context :: Context -> Elab' aux ()

185set_context ctxt = do ES (p, a) logs prev <- get

186 put (ES (p { context = ctxt }, a) logs prev)

187

188−-- get the proof term

188+-- | get the proof term

189get_term :: Elab' aux Term

190get_term = do ES p _ _ <- get

191 return $! (getProofTerm (pterm (fst p)))

192

193−-- get the proof term

193+-- | get the proof term

194update_term :: (Term -> Term) -> Elab' aux ()

195update_term f = do ES (p,a) logs prev <- get

196 let p' = p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }

197 put (ES (p', a) logs prev)

198

199−-- get the local context at the currently in focus hole

199+-- | get the local context at the currently in focus hole

200get_env :: Elab' aux Env

201get_env = do ES p _ _ <- get

202 lift $ envAtFocus (fst p)

@@ -213,14 +213,14 @@ get_probs :: Elab' aux Fails

213get_probs = do ES p _ _ <- get

214 return $! (problems (fst p))

215

216−-- Return recently solved names (that is, the names solved since the

216+-- | Return recently solved names (that is, the names solved since the

217-- last call to get_recents)

218get_recents :: Elab' aux [Name]

219get_recents = do ES (p, a) l prev <- get

220 put (ES (p { recents = [] }, a) l prev)

221 return (recents p)

222

223−-- get the current goal type

223+-- | get the current goal type

224goal :: Elab' aux Type

225goal = do ES p _ _ <- get

226 b <- lift $ goalAtFocus (fst p)

@@ -233,7 +233,7 @@ is_guess = do ES p _ _ <- get

233 Guess _ _ -> return True

234 _ -> return False

235

236−-- Get the guess at the current hole, if there is one

236+-- | Get the guess at the current hole, if there is one

237get_guess :: Elab' aux Type

238get_guess = do ES p _ _ <- get

239 b <- lift $ goalAtFocus (fst p)

@@ -241,7 +241,7 @@ get_guess = do ES p _ _ <- get

241 Guess t v -> return $! v

242 _ -> fail "Not a guess"

243

244−-- typecheck locally

244+-- | Typecheck locally

245get_type :: Raw -> Elab' aux Type

246get_type tm = do ctxt <- get_context

247 env <- get_env

@@ -254,7 +254,7 @@ get_type_val tm = do ctxt <- get_context

254 (val, ty) <- lift $ check ctxt env tm

255 return $! (finalise val, finalise ty)

256

257−-- get holes we've deferred for later definition

257+-- | get holes we've deferred for later definition

258get_deferred :: Elab' aux [Name]

259get_deferred = do ES p _ _ <- get

260 return $! (deferred (fst p))

@@ -271,17 +271,18 @@ checkInjective (tm, l, r) = do ctxt <- get_context

271 isInj ctxt (Bind _ (Pi _ _ _) sc) = True

272 isInj ctxt _ = False

273

274−-- get instance argument names

274+-- | get instance argument names

275get_instances :: Elab' aux [Name]

276get_instances = do ES p _ _ <- get

277 return $! (instances (fst p))

278

279−-- get auto argument names

279+-- | get auto argument names

280get_autos :: Elab' aux [(Name, [Name])]

281get_autos = do ES p _ _ <- get

282 return $! (autos (fst p))

283

284−-- given a desired hole name, return a unique hole name

284+-- | given a desired hole name, return a unique hole name

285+unique_hole :: Name -> Elab' aux Name

285unique_hole = unique_hole' False

286unique_hole = unique_hole' False

286

287

287unique_hole' :: Bool -> Name -> Elab' aux Name

288unique_hole' :: Bool -> Name -> Elab' aux Name

src/Idris/Core/Evaluate.hs+29−24

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

11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

13 mapDefCtxt,

14− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,

14+ lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

16 isUniverse) where

@@ -971,47 +971,52 @@ isConName n ctxt = isTConName n ctxt || isDConName n ctxt

971

972isTConName :: Name -> Context -> Bool

973isTConName n ctxt

974− = or $ do def <- lookupCtxt n (definitions ctxt)

974+ = case lookupDefExact n ctxt of

975− case tfst def of

976− (TyDecl (TCon _ _) _) -> return True

975+ Just (TyDecl (TCon _ _) _) -> True

977− _ -> return False

976+ _ -> False

978

977

978+-- | Check whether a resolved name is certainly a data constructor

979isDConName :: Name -> Context -> Bool

980isDConName n ctxt

981+ = case lookupDefExact n ctxt of

982+ Just (TyDecl (DCon _ _ _) _) -> True

983+ _ -> False

984+

985+-- | Check whether any overloading of a name is a data constructor

986+canBeDConName :: Name -> Context -> Bool

987+canBeDConName n ctxt

981 = or $ do def <- lookupCtxt n (definitions ctxt)

988 = or $ do def <- lookupCtxt n (definitions ctxt)

982 case tfst def of

989 case tfst def of

983− (TyDecl (DCon _ _ _) _) -> return True

990+ (TyDecl (DCon _ _ _) _) -> return True

984− _ -> return False

991+ _ -> return False

985

992

986isFnName :: Name -> Context -> Bool

993isFnName :: Name -> Context -> Bool

987isFnName n ctxt

994isFnName n ctxt

988− = let def = lookupCtxtExact n (definitions ctxt) in

995+ = case lookupDefExact n ctxt of

989− case def of

990− Just (Function _ _, _, _, _) -> True

996+ Just (Function _ _) -> True

991− Just (Operator _ _ _, _, _, _) -> True

997+ Just (Operator _ _ _) -> True

992− Just (CaseOp _ _ _ _ _ _, _, _, _) -> True

998+ Just (CaseOp _ _ _ _ _ _) -> True

993− _ -> False

999+ _ -> False

994

1000

995isTCDict :: Name -> Context -> Bool

1001isTCDict :: Name -> Context -> Bool

996isTCDict n ctxt

1002isTCDict n ctxt

997− = let def = lookupCtxtExact n (definitions ctxt) in

1003+ = case lookupDefExact n ctxt of

998− case def of

999− Just (Function _ _, _, _, _) -> False

1004+ Just (Function _ _) -> False

1000− Just (Operator _ _ _, _, _, _) -> False

1005+ Just (Operator _ _ _) -> False

1001− Just (CaseOp ci _ _ _ _ _, _, _, _) -> tc_dictionary ci

1006+ Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci

1002− _ -> False

1007+ _ -> False

1003

1008

1004lookupP :: Name -> Context -> [Term]

1009lookupP :: Name -> Context -> [Term]

1005lookupP n ctxt

1010lookupP n ctxt

1006 = do def <- lookupCtxt n (definitions ctxt)

1011 = do def <- lookupCtxt n (definitions ctxt)

1007 p <- case def of

1012 p <- case def of

1008− (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1013+ (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1009− (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1014+ (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1010 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1015 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1011− (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1016+ (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1012 case snd p of

1017 case snd p of

1013− Hidden -> []

1018+ Hidden -> []

1014− _ -> return (fst p)

1019+ _ -> return (fst p)

1015

1020

1016lookupDefExact :: Name -> Context -> Maybe Def

1021lookupDefExact :: Name -> Context -> Maybe Def

1017lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

1022lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

src/Idris/Coverage.hs+10−11

@@ -18,18 +18,18 @@ import Debug.Trace

19import Control.Monad.State.Strict

21−-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the

21+-- | Generate a pattern from an 'impossible' LHS.

22+--

23+-- We need this to eliminate the pattern clauses which have been

22−-- pattern clauses which have been provided explicitly from new clause

24+-- provided explicitly from new clause generation.

23−-- generation.)

24−

25mkPatTm :: PTerm -> Idris Term

26mkPatTm t = do i <- getIState

27 let timp = addImpl' True [] [] i t

28 evalStateT (toTT (mapPT deNS timp)) 0

29 where

30 toTT (PRef _ n) = do i <- lift getIState

31− case lookupDef n (tt_ctxt i) of

31+ case lookupNameDef n (tt_ctxt i) of

32− [TyDecl nt _] -> return $ P nt n Erased

32+ [(n', TyDecl nt _)] -> return $ P nt n' Erased

33 _ -> return $ P Ref n Erased

34 toTT (PApp _ t args) = do t' <- toTT t

35 args' <- mapM (toTT . getTm) args

@@ -44,13 +44,12 @@ mkPatTm t = do i <- getIState

44 deNS (PRef f (NS n _)) = PRef f n

45 deNS t = t

47−-- Given a list of LHSs, generate a extra clauses which cover the remaining

47+-- | Given a list of LHSs, generate a extra clauses which cover the remaining

48−-- cases. The ones which haven't been provided are marked 'absurd' so that the

48+-- cases. The ones which haven't been provided are marked 'absurd' so

49−-- checker will make sure they can't happen.

49+-- that the checker will make sure they can't happen.

50−

50+--

51-- This will only work after the given clauses have been typechecked and the

52-- names are fully explicit!

53−

54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]

53genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]

55genClauses fc n xs given

54genClauses fc n xs given

56 = do i <- getIState

55 = do i <- getIState

src/Idris/Delaborate.hs+2−2

@@ -308,7 +308,7 @@ pprintErr' i (ElaboratingArg f x _ e)

308 where whatIsName = let ctxt = tt_ctxt i

309 in if isTConName f ctxt

310 then text "type constructor" <> space

311− else if isConName f ctxt

311+ else if isDConName f ctxt

312 then text "constructor" <> space

313 else if isFnName f ctxt

314 then text "function" <> space

@@ -488,7 +488,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

488 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

489 _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

490 _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty

491− _ | otherwise -> annot

491+ _ | otherwise -> annot

492 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

493 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

494 let o = overview (fst docs)

test/totality006/expected+1

@@ -1,2 +1,3 @@

1totality006.idr:8:1:Main.prf is not total as there are missing cases

2totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

3+totality006b.idr:10:1:totality006b.blargh is not total as there are missing cases

test/totality006/run+1

@@ -1,4 +1,5 @@

1#!/usr/bin/env bash

2idris $@ totality006.idr --check

3idris $@ totality006a.idr --check

4+idris $@ totality006b.idr --check

4rm -f *.ibc

5rm -f *.ibc

test/totality006/totality006b.idrnew file+14

@@ -0,0 +1,14 @@

1+module totality006b

3+import Data.So

6+-- There are approaches to impossibility checking that break on this

7+-- case but not on test006.idr, due to the extra computation.

8+total

9+blargh : (xs, ys : List a) -> So (length xs > length ys) -> GT (length xs) (length ys)

10+blargh [] [] Oh impossible

11+blargh [] (y :: xs) so = absurd so

12+blargh (y :: xs) [] Oh = LTESucc LTEZero

13+

14+-- Missing: blargh (y :: xs) (z :: ys) x = ?blargh_rhs_3