5a6299b · Idris-dev · git.iko.soy

lib/prelude/nat.idr+4−4

@@ -239,11 +239,11 @@ div left (S right) = div' left left right

239239-- Succ

240240total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->

241241 S left = S right

242−eqSucc left right refl = refl

242+eqSucc left _ refl = refl

243243

244244total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->

245245 left = right

246−succInjective left right refl = refl

246+succInjective left _ refl = refl

247247

248248-- Plus

249249total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right

@@ -278,11 +278,11 @@ plusAssociative (S left) centre right =

278278

279279total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->

280280 (p : left = right) -> left + c = right + c

281−plusConstantRight left right c refl = refl

281+plusConstantRight left _ c refl = refl

282282

283283total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->

284284 (p : left = right) -> c + left = c + right

285−plusConstantLeft left right c refl = refl

285+plusConstantLeft left _ c refl = refl

286286

287287total plusOneSucc : (right : Nat) -> 1 + right = S right

288288plusOneSucc n = refl

lib/prelude/vect.idr−1

@@ -34,7 +34,6 @@ index : Fin n -> Vect a n -> a

3434index fO (x::xs) = x

3535index (fS k) (x::xs) = index k xs

3636index fO [] impossible

37−index (fS _) [] impossible

3837

3938--------------------------------------------------------------------------------

4039-- Subvectors

src/Core/CaseTree.hs+14−7

@@ -17,6 +17,7 @@ data SC = Case Name [CaseAlt] -- invariant: lowest tags first

1717 | ProjCase Term [CaseAlt] -- special case for projections

1818 | STerm Term

1919 | UnmatchedCase String -- error message

20+ | ImpossibleCase -- already checked to be impossible

2021 deriving (Eq, Ord)

2122{-!

2223deriving instance Binary SC

@@ -39,6 +40,7 @@ instance Show SC where

3940 showSep ("\n" ++ indent i) (map (showA i) alts)

4041 show' i (STerm tm) = show tm

4142 show' i (UnmatchedCase str) = "error " ++ show str

43+ show' i ImpossibleCase = "impossible"

4244

4345 indent i = concat $ take i (repeat " ")

4446

@@ -143,7 +145,7 @@ data Phase = CompileTime | RunTime

143145 deriving (Show, Eq)

144146

145147-- Generate a simple case tree

146−--

148+-- Work Left to Right at Compile Time

147149

148150simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] -> TC CaseDef

149151simpleCase tc cover phase fc []

@@ -151,14 +153,14 @@ simpleCase tc cover phase fc []

151153simpleCase tc cover phase fc cs

152154 = let proj = phase == RunTime

153155 pats = map (\ (avs, l, r) ->

154− (avs, reverse (toPats tc l), (l, r))) cs

156+ (avs, rev phase (toPats tc l), (l, r))) cs

155157 chkPats = mapM chkAccessible pats in

156158 case chkPats of

157159 OK pats ->

158160 let numargs = length (fst (head pats))

159161 ns = take numargs args

160162 (tree, st) = runState

161− (match (reverse ns) pats (defaultCase cover)) ([], numargs)

163+ (match (rev phase ns) pats (defaultCase cover)) ([], numargs)

162164 t = CaseDef ns (prune proj tree) (fst st) in

163165 if proj then return (stripLambdas t) else return t

164166 Error err -> Error (At fc err)

@@ -174,6 +176,9 @@ simpleCase tc cover phase fc cs

174176 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

175177 acc (_ : xs) n = acc xs n

176178

179+rev CompileTime = id

180+rev _ = reverse

181+

177182data Pat = PCon Name Int [Pat]

178183 | PConst Const

179184 | PV Name

@@ -240,7 +245,9 @@ match :: [Name] -> [Clause] -> SC -- error case

240245match [] (([], ret) : xs) err

241246 = do (ts, v) <- get

242247 put (ts ++ (map (fst.snd) xs), v)

243− return $ STerm (snd ret) -- run out of arguments

248+ case snd ret of

249+ Impossible -> return ImpossibleCase

250+ tm -> return $ STerm tm -- run out of arguments

244251match vs cs err = do let ps = partition cs

245252 cs <- mixture vs ps err

246253 return cs

@@ -338,10 +345,9 @@ varRule (v : vs) alts err =

338345prune :: Bool -> -- ^ Convert single brances to projections (only useful at runtime)

339346 SC -> SC

340347prune proj (Case n alts)

341− = let alts' = map pruneAlt $

342− filter notErased alts in

348+ = let alts' = filter notErased (map pruneAlt alts) in

343349 case alts' of

344− [] -> STerm Erased

350+ [] -> ImpossibleCase

345351 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc

346352 else Case n as

347353 as -> Case n as

@@ -350,6 +356,7 @@ prune proj (Case n alts)

350356 pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)

351357

352358 notErased (DefaultCase (STerm Erased)) = False

359+ notErased (DefaultCase ImpossibleCase) = False

353360 notErased _ = True

354361

355362 mkProj n i [] sc = sc

src/Core/Elaborate.hs+13−12

@@ -148,7 +148,7 @@ get_instances = do ES p _ _ <- get

148148unique_hole :: Name -> Elab' aux Name

149149unique_hole n = do ES p _ _ <- get

150150 let bs = bound_in (pterm (fst p)) ++ bound_in (ptype (fst p))

151− n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p) ++ bs)

151+ n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p) ++ bs ++ dontunify (fst p))

152152 return n'

153153 where

154154 bound_in (Bind n b sc) = n : bi b ++ bound_in sc

@@ -317,24 +317,20 @@ apply fn imps =

317317 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

318318 -- so do nothing

319319 ptm <- get_term

320− let dontunify = if null imps then [] -- do all we can

321− else

322− map fst (filter (not.snd) (zip args (map fst imps)))

323320 ES (p, a) s prev <- get

324− let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dontunify)) $

321+ let dont = nub $ dontunify p ++

322+ if null imps then [] -- do all we can

323+ else

324+ map fst (filter (not.snd) (zip args (map fst imps)))

325+ let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

325326 unified p

326− let unify = dropGiven dontunify hs

327− put (ES (p { unified = (n, unify) }, a) s prev)

327+ let unify = dropGiven dont hs

328+ put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

328329 end_unify

329330 return (map (updateUnify unify) args)

330331 where updateUnify hs n = case lookup n hs of

331332 Just (P _ t _) -> t

332333 _ -> n

333− dropGiven du [] = []

334− dropGiven du ((n, P a t ty) : us) | n `elem` du && not (t `elem` du)

335− = (t, P a n ty) : dropGiven du us

336− dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us

337− dropGiven du (u : us) = u : dropGiven du us

338334

339335apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

340336apply2 fn elabs =

@@ -375,6 +371,11 @@ apply_elab n args =

375371 when (null claims) (start_unify n)

376372 let sc' = instantiate (P Bound n t) sc

377373 claim n (forget t)

374+ case i of

375+ Nothing -> return ()

376+ Just _ -> -- don't solve by unification as there is an explicit value

377+ do ES (p, a) s prev <- get

378+ put (ES (p { dontunify = n : dontunify p }, a) s prev)

378379 doClaims sc' is ((n, i) : claims)

379380 doClaims t [] claims = return (reverse claims)

380381 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n

src/Core/ProofState.hs+24−12

@@ -5,7 +5,7 @@

55 evaluation/checking inside the proof system, etc. --}

66

77module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8− Tactic(..), Goal(..), processTactic) where

8+ Tactic(..), Goal(..), processTactic, dropGiven) where

99

1010import Core.Typecheck

1111import Core.Evaluate

@@ -24,6 +24,7 @@ data ProofState = PS { thname :: Name,

2424 nextname :: Int, -- name supply

2525 pterm :: Term, -- current proof term

2626 ptype :: Type, -- original goal

27+ dontunify :: [Name], -- explicitly given by programmer, leave it

2728 unified :: (Name, [(Name, Term)]),

2829 solved :: Maybe (Name, Term),

2930 problems :: Fails,

@@ -73,8 +74,8 @@ data Tactic = Attack

7374-- Some utilites on proof and tactic states

7475

7576instance Show ProofState where

76− show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

77− show (PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _)

77+ show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

78+ show (PS nm (h:hs) _ tm _ _ _ _ _ _ i _ _ ctxt _ _)

7879 = let OK g = goal (Just h) tm

7980 wkenv = premises g in

8081 "Other goals: " ++ show hs ++ "\n" ++

@@ -97,12 +98,12 @@ instance Show ProofState where

9798 showG ps b = showEnv ps (binderTy b)

9899

99100instance Pretty ProofState where

100− pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _) =

101+ pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _ _) =

101102 if size nm > breakingSize then

102103 pretty nm <> colon $$ nest nestingSize (text " no more goals.")

103104 else

104105 pretty nm <> colon <+> text " no more goals."

105− pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) =

106+ pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =

106107 let OK g = goal (Just h) tm in

107108 let wkEnv = premises g in

108109 text "Other goals" <+> colon <+> pretty hs $$

@@ -170,7 +171,7 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

170171newProof :: Name -> Context -> Type -> ProofState

171172newProof n ctxt ty = let h = holeName 0

172173 ty' = vToP ty in

173− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, [])

174+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty [] (h, [])

174175 Nothing [] []

175176 [] []

176177 Nothing ctxt "" False

@@ -351,6 +352,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

351352 let (uh, uns) = unified ps

352353 action (\ps -> ps { holes = holes ps \\ [x],

353354 solved = Just (x, val),

355+ -- dontunify = dontunify ps \\ [x],

354356 -- unified = (uh, uns ++ [(x, val)]),

355357 instances = instances ps \\ [x] })

356358 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

@@ -487,10 +489,19 @@ solve_unified :: RunTactic

487489solve_unified ctxt env tm =

488490 do ps <- get

489491 let (_, ns) = unified ps

490− action (\ps -> ps { holes = holes ps \\ map fst ns })

491− action (\ps -> ps { pterm = updateSolved ns (pterm ps) })

492− action (\ps -> ps { injective = map (tmap (updateSolved ns)) (injective ps) })

493− return (updateSolved ns tm)

492+ let unify = dropGiven (dontunify ps) ns

493+ action (\ps -> ps { holes = holes ps \\ map fst unify })

494+ action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

495+ action (\ps -> ps { injective = map (tmap (updateSolved unify)) (injective ps) })

496+ return (updateSolved unify tm)

497+ where

498+

499+dropGiven du [] = []

500+dropGiven du ((n, P Bound t ty) : us) | n `elem` du && not (t `elem` du)

501+ = (t, P Bound n ty) : dropGiven du us

502+dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us

503+-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us

504+dropGiven du (u : us) = u : dropGiven du us

494505

495506updateSolved xs (Bind n (Hole ty) t)

496507 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

@@ -519,9 +530,10 @@ processTactic Undo ps = case previous ps of

519530 Nothing -> fail "Nothing to undo."

520531 Just pold -> return (pold, "")

521532processTactic EndUnify ps

522− = let (h, ns) = unified ps

533+ = let (h, ns_in) = unified ps

534+ ns = dropGiven (dontunify ps) ns_in

523535 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

524− tm' = -- trace ("Updating " ++ show ns' ++ " in " ++ show (pterm ps)) $

536+ tm' = -- trace ("Updating " ++ show ns') $ -- ++ " in " ++ show (pterm ps)) $

525537 updateSolved ns' (pterm ps)

526538 probs' = updateProblems ns' (problems ps) in

527539 case probs' of

src/Core/TT.hs+2

@@ -414,6 +414,7 @@ data TT n = P NameType n (TT n) -- embed type

414414 | Constant Const

415415 | Proj (TT n) Int -- argument projection; runtime only

416416 | Erased

417+ | Impossible -- special case for totality checking

417418 | Set UExp

418419 deriving (Ord, Functor)

419420{-!

@@ -712,6 +713,7 @@ showEnv' env t dbg = se 10 env t where

712713 se p env (Proj x i) = se 1 env x ++ "!" ++ show i

713714 se p env (Constant c) = show c

714715 se p env Erased = "[__]"

716+ se p env Impossible = "[impossible]"

715717 se p env (Set i) = "Set " ++ show i

716718

717719 sb env n (Lam t) = showb env "\\ " " => " n t

src/Idris/AbsSyntax.hs+2−2

@@ -501,7 +501,7 @@ getPriority i tm = pri tm

501501 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))

502502 pri (PTrue _) = 0

503503 pri (PFalse _) = 0

504− pri (PRefl _) = 1

504+ pri (PRefl _ _) = 1

505505 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

506506 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

507507 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

@@ -901,7 +901,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

901901 match (PQuote _) _ = return []

902902 match (PProof _) _ = return []

903903 match (PTactics _) _ = return []

904− match (PRefl _) (PRefl _) = return []

904+ match (PRefl _ _) (PRefl _ _) = return []

905905 match (PResolveTC _) (PResolveTC _) = return []

906906 match (PTrue _) (PTrue _) = return []

907907 match (PFalse _) (PFalse _) = return []

src/Idris/AbsSyntaxTree.hs+7−4

@@ -152,6 +152,7 @@ data Command = Quit

152152 | Defn Name

153153 | Info Name

154154 | Missing Name

155+ | Pattelab PTerm

155156 | DebugInfo Name

156157 | Search PTerm

157158 | SetOpt Opt

@@ -363,7 +364,7 @@ data PTerm = PQuote Raw

363364 | PCase FC PTerm [(PTerm, PTerm)]

364365 | PTrue FC

365366 | PFalse FC

366− | PRefl FC

367+ | PRefl FC PTerm

367368 | PResolveTC FC

368369 | PEq FC PTerm PTerm

369370 | PPair FC PTerm PTerm

@@ -777,7 +778,7 @@ prettyImp impl = prettySe 10

777778

778779 sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r

779780 prettySe p (PHidden tm) = text "." <> prettySe 0 tm

780− prettySe p (PRefl _) = text "refl"

781+ prettySe p (PRefl _ _) = text "refl"

781782 prettySe p (PResolveTC _) = text "resolvetc"

782783 prettySe p (PTrue _) = text "()"

783784 prettySe p (PFalse _) = text "_|_"

@@ -886,7 +887,9 @@ showImp impl tm = se 10 tm where

886887 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)

887888 where sc (l, r) = se 10 l ++ " => " ++ se 10 r

888889 se p (PHidden tm) = "." ++ se 0 tm

889− se p (PRefl _) = "refl"

890+ se p (PRefl _ t)

891+ | not impl = "refl"

892+ | otherwise = "refl {" ++ se 10 t ++ "}"

890893 se p (PResolveTC _) = "resolvetc"

891894 se p (PTrue _) = "()"

892895 se p (PFalse _) = "_|_"

@@ -962,7 +965,7 @@ instance Sized PTerm where

962965 size (PCase fc trm bdy) = 1 + size trm + size bdy

963966 size (PTrue fc) = 1

964967 size (PFalse fc) = 1

965− size (PRefl fc) = 1

968+ size (PRefl fc _) = 1

966969 size (PResolveTC fc) = 1

967970 size (PEq fc left right) = 1 + size left + size right

968971 size (PPair fc left right) = 1 + size left + size right

src/Idris/Coverage.hs+54−19

@@ -19,28 +19,63 @@ import Control.Monad.State

1919-- Generate the LHSes which are missing from a case tree

2020-- Eliminate the ones which cannot be well typed

2121

22−genMissing :: [Name] -> SC -> Idris [PTerm]

23−genMissing args sc = do sc' <- expandTree sc

24− iputStrLn (show sc')

25− gm (map (\x -> P Bound x Erased) args) sc'

26−

27−gm :: [TT Name] -> SC -> Idris [PTerm]

28−gm args (Case n alts) = do m <- mapM (gmAlt args n) alts

29− return (concat m)

30−gm args (STerm tm) = do iputStrLn ("Covered: " ++ show args)

31− return []

32−gm args (UnmatchedCase _) = do iputStrLn ("Missing: " ++ show args)

33− return []

34−

35−gmAlt args n (ConCase cn t cargs sc)

22+genMissing :: Name -> [Name] -> SC -> Idris [PTerm]

23+genMissing fn args sc

24+ = do sc' <- expandTree sc

25+ logLvl 5 $ "Checking missing cases for " ++ show fn ++ "\n" ++ (show sc')

26+ (got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'

27+ return $ filter (\x -> not (x `elem` got)) missing

28+

29+-- Make a term to feed to the pattern matcher from a LHS declared impossible

30+-- (we can't type check it, but we need the case analysis to check for covering...)

31+

32+mkPatTm :: PTerm -> Idris Term

33+mkPatTm t = do i <- get

34+ let timp = addImpl' True [] i t

35+ evalStateT (toTT timp) 0

36+ where

37+ toTT (PRef _ n) = do i <- lift $ get

38+ case lookupDef Nothing n (tt_ctxt i) of

39+ [TyDecl nt _] -> return $ P nt n Erased

40+ _ -> return $ P Ref n Erased

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

42+ args' <- mapM (toTT . getTm) args

43+ return $ mkApp t' args'

44+ toTT _ = do v <- get

45+ put (v + 1)

46+ return (P Bound (MN v "imp") Erased)

47+

48+mkPTerm :: Name -> [TT Name] -> Idris PTerm

49+mkPTerm f args = do i <- get

50+ let fapp = mkApp (P Bound f Erased) (map eraseName args)

51+ return $ delab i fapp

52+ where eraseName (App f a) = App (eraseName f) (eraseName a)

53+ eraseName (P _ (MN _ _) _) = Erased

54+ eraseName t = t

55+

56+gm :: Name -> [TT Name] -> SC -> Idris ([PTerm], [PTerm])

57+gm fn args (Case n alts) = do m <- mapM (gmAlt fn args n) alts

58+ let (got, missing) = unzip m

59+ return (concat got, concat missing)

60+gm fn args (STerm tm) = do logLvl 3 ("Covered: " ++ show args)

61+ t <- mkPTerm fn args

62+ return ([t], [])

63+gm fn args ImpossibleCase = do logLvl 3 ("Impossible: " ++ show args)

64+ t <- mkPTerm fn args

65+ return ([], [])

66+gm fn args (UnmatchedCase _) = do logLvl 3 ("Missing: " ++ show args)

67+ t <- mkPTerm fn args

68+ return ([], [t])

69+

70+gmAlt fn args n (ConCase cn t cargs sc)

3671 = do let args' = map (subst n (mkApp (P Bound cn Erased)

3772 (map (\x -> P Bound x Erased) cargs))) args

38− gm args' sc

39−gmAlt args n (ConstCase c sc)

73+ gm fn args' sc

74+gmAlt fn args n (ConstCase c sc)

4075 = do let args' = map (subst n (Constant c)) args

41− gm args' sc

42−gmAlt args n (DefaultCase sc)

43− = do gm args sc

76+ gm fn args' sc

77+gmAlt fn args n (DefaultCase sc)

78+ = do gm fn args sc

4479

4580getDefault (DefaultCase sc : _) = sc

4681getDefault (_ : cs) = getDefault cs

src/Idris/Delaborate.hs+2−1

@@ -37,6 +37,7 @@ delab' ist tm fullname = de [] tm

3737 de env (Bind n _ sc) = de ((n,n):env) sc

3838 de env (Constant i) = PConstant i

3939 de env Erased = Placeholder

40+ de env Impossible = Placeholder

4041 de env (Set i) = PSet

4142

4243 dens x | fullname = x

@@ -47,7 +48,7 @@ delab' ist tm fullname = de [] tm

4748

4849 deFn env (App f a) args = deFn env f (a:args)

4950 deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)

50− | n == eqCon = PRefl un

51+ | n == eqCon = PRefl un (de env r)

5152 | n == UN "lazy" = de env r

5253 deFn env (P _ n _) [ty, Bind x (Lam _) r]

5354 | n == UN "Exists"

src/Idris/ElabDecls.hs+25−31

@@ -231,23 +231,21 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

231231 pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs

232232

233233 solveDeferred n

234− let pats = mapMaybe id pats_in

235− logLvl 3 (showSep "\n" (map (\ (l,r) ->

236− show l ++ " = " ++

237− show r) pats))

234+ let pats = pats_in

235+-- logLvl 3 (showSep "\n" (map (\ (l,r) ->

236+-- show l ++ " = " ++

237+-- show r) pats))

238238 ist <- get

239239 let tcase = opt_typecase (idris_options ist)

240240 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats

241+ tree@(CaseDef scargs sc _) <- tclift $ simpleCase tcase False CompileTime fc pdef

241242 tclift $ sameLength pdef

242243 cov <- coverage

243244 pcover <-

244245 if cov

245− then do missing <- genClauses fc n (map getLHS pdef) cs

246+ then do -- missing <- genClauses fc n (map getLHS pdef) cs

247+ missing <- genMissing n scargs sc

246248 missing' <- filterM (checkPossible info fc True n) missing

247−-- let missing' = mapMaybe (\x -> case x of

248−-- Nothing -> Nothing

249−-- Just t -> Just $ delab ist t)

250−-- poss

251249 logLvl 3 $ "Must be unreachable:\n" ++

252250 showSep "\n" (map (showImp True) missing') ++

253251 "\nAgainst: " ++

@@ -255,20 +253,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

255253 if null missing'

256254 then return True

257255 else return False

258−-- -- if there's missing cases, add a catch all case. If it's

259−-- -- unreachable, we're still covering

260−-- do let mrhs = P Ref (MN 0 "reach?") undefined

261−-- let (f,as) = unApply $ depat (head missing')

262−-- let arity = length as

263−-- let mlhs = mkApp f (map (\a -> P Bound (MN a "v") undefined)

264−-- [0..arity-1])

265−-- let untree@(CaseDef _ sc _) = simpleCase tcase True

266−-- (pdef ++ [(mlhs, mrhs)])

267−-- logLvl 5 $ "Tree is " ++ show sc

268−-- return False

269256 else return False

270257 pdef' <- applyOpts pdef

271− tree@(CaseDef _ sc _) <- tclift $ simpleCase tcase pcover CompileTime fc pdef

272258 ist <- get

273259-- let wf = wellFounded ist n sc

274260 let tot = if pcover || AssertTotal `elem` opts

@@ -314,15 +300,19 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

314300-- addIBC (IBCTotal n tot)

315301 [] -> return ()

316302 where

317− debind (x, y) = let (vs, x') = depat [] x

318− (_, y') = depat [] y in

319− (vs, x', y')

303+ debind (Right (x, y)) = let (vs, x') = depat [] x

304+ (_, y') = depat [] y in

305+ (vs, x', y')

306+ debind (Left x) = let (vs, x') = depat [] x in

307+ (vs, x', Impossible)

308+

320309 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)

321310 depat acc x = (acc, x)

322311

323312 getLHS (_, l, _) = l

324313

325− simpl ctxt (x, y) = (x, simplify ctxt [] y)

314+ simpl ctxt (Right (x, y)) = Right (x, simplify ctxt [] y)

315+ simpl ctxt t = t

326316

327317 sameLength ((_, x, _) : xs)

328318 = do l <- sameLength xs

@@ -357,17 +347,21 @@ checkPossible info fc tcgen fname lhs_in

357347 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of

358348 OK ((lhs', _, _), _) ->

359349 do let lhs_tm = orderPats (getInferTerm lhs')

360− b <- inferredDiff fc (delab' i lhs_tm True) lhs

361− return (not b) -- then return (Just lhs_tm) else return Nothing

350+ case recheck ctxt [] (forget lhs_tm) lhs_tm of

351+ OK _ -> return True

352+ _ -> return False

353+-- b <- inferredDiff fc (delab' i lhs_tm True) lhs

354+-- return (not b) -- then return (Just lhs_tm) else return Nothing

362355-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

363356 Error _ -> return False

364357

365−elabClause :: ElabInfo -> Bool -> PClause -> Idris (Maybe (Term, Term))

358+elabClause :: ElabInfo -> Bool -> PClause -> Idris (Either Term (Term, Term))

366359elabClause info tcgen (PClause fc fname lhs_in [] PImpossible [])

367360 = do b <- checkPossible info fc tcgen fname lhs_in

368361 case b of

369362 True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

370− False -> return Nothing

363+ False -> do ptm <- mkPatTm lhs_in

364+ return (Left ptm)

371365elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

372366 = do ctxt <- getContext

373367 -- Build the LHS as an "Infer", and pull out its type and

@@ -423,7 +417,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

423417 Error _ -> ierror (At fc (CantUnify False clhsty crhsty (Msg "") [] 0))

424418 i <- get

425419 checkInferred fc (delab' i crhs True) rhs

426− return $ Just (clhs, crhs)

420+ return $ Right (clhs, crhs)

427421 where

428422 decorate x = UN (show fname ++ "#" ++ show x)

429423 pinfo ns ps i

@@ -508,7 +502,7 @@ elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)

508502 addDeferred def'

509503 mapM_ (elabCaseBlock info) is

510504 (crhs, crhsty) <- recheckC fc [] rhs'

511− return $ Just (clhs, crhs)

505+ return $ Right (clhs, crhs)

512506 where

513507 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

514508 getImps _ = []

src/Idris/ElabTerm.hs+8−19

@@ -112,8 +112,8 @@ elab ist info pattern tcgen fn tm

112112 | otherwise = try (resolveTC 2 fn ist)

113113 (do c <- unique_hole (MN 0 "c")

114114 instanceArg c)

115− elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

116− pimp (MN 0 "x") Placeholder])

115+ elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

116+ pimp (MN 0 "x") t])

117117 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

118118 pimp (MN 0 "b") Placeholder,

119119 pexp l, pexp r])

@@ -211,19 +211,6 @@ elab ist info pattern tcgen fn tm

211211 elabE (True, a) val

212212 elabE (True, a) sc

213213 solve

214−-- elab' ina (PTyped val ty)

215−-- = do tyn <- unique_hole (MN 0 "castty")

216−-- claim tyn RSet

217−-- valn <- unique_hole (MN 0 "castval")

218−-- claim valn (Var tyn)

219−-- focus tyn

220−-- elabE True ty

221−-- focus valn

222−-- elabE True val

223−-- elab' ina (PApp fc (PRef _ dsl) [arg])

224−-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)

225−-- = let dsl' = expandDo d (getTm arg) in

226−-- trace (show dsl') $ elab' ina dsl'

227214 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

228215 = do let args = {- case lookupCtxt f (inblock info) of

229216 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

@@ -242,7 +229,8 @@ elab ist info pattern tcgen fn tm

242229 = unzip $

243230 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

244231 (zip ns args)

245− try (elabArgs (ina || not isinf, guarded)

232+ try

233+ (elabArgs (ina || not isinf, guarded)

246234 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

247235 (elabArgs (ina || not isinf, guarded)

248236 [] False (reverse ns')

@@ -316,8 +304,8 @@ elab ist info pattern tcgen fn tm

316304 (map pexp args ++ [pexp l])) [] r []

317305

318306 elabArgs ina failed retry [] _

319− | retry = let (ns, ts) = unzip (reverse failed) in

320− elabArgs ina [] False ns ts

307+-- | retry = let (ns, ts) = unzip (reverse failed) in

308+-- elabArgs ina [] False ns ts

321309 | otherwise = return ()

322310 elabArgs ina failed r (n:ns) ((_, Placeholder) : args)

323311 = elabArgs ina failed r ns args

@@ -387,7 +375,8 @@ pruneByType (P _ n _) c as

387375pruneByType t _ as = as

388376

389377trivial :: IState -> ElabD ()

390−trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0))

378+trivial ist = try (do elab ist toplevel False False (MN 0 "tac")

379+ (PRefl (FC "prf" 0) Placeholder)

391380 return ())

392381 (do env <- get_env

393382 tryAll (map fst env)

src/Idris/IBC.hs+10−4

@@ -21,7 +21,7 @@ import System.Directory

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 21

24+ibcVersion = 22

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

@@ -493,6 +493,7 @@ instance (Binary n) => Binary (TT n) where

493493 Erased -> putWord8 6

494494 Set x1 -> do putWord8 7

495495 put x1

496+ Impossible -> putWord8 8

496497 get

497498 = do i <- getWord8

498499 case i of

@@ -517,6 +518,7 @@ instance (Binary n) => Binary (TT n) where

517518 6 -> return Erased

518519 7 -> do x1 <- get

519520 return (Set x1)

521+ 8 -> return Impossible

520522 _ -> error "Corrupted binary data for TT"

521523

522524instance Binary SC where

@@ -532,6 +534,7 @@ instance Binary SC where

532534 put x1

533535 UnmatchedCase x1 -> do putWord8 3

534536 put x1

537+ ImpossibleCase -> do putWord8 4

535538 get

536539 = do i <- getWord8

537540 case i of

@@ -545,6 +548,7 @@ instance Binary SC where

545548 return (STerm x1)

546549 3 -> do x1 <- get

547550 return (UnmatchedCase x1)

551+ 4 -> return ImpossibleCase

548552 _ -> error "Corrupted binary data for SC"

549553

550554

@@ -1072,8 +1076,9 @@ instance Binary PTerm where

10721076 put x1

10731077 PFalse x1 -> do putWord8 9

10741078 put x1

1075− PRefl x1 -> do putWord8 10

1076− put x1

1079+ PRefl x1 x2 -> do putWord8 10

1080+ put x1

1081+ put x2

10771082 PResolveTC x1 -> do putWord8 11

10781083 put x1

10791084 PEq x1 x2 x3 -> do putWord8 12

@@ -1153,7 +1158,8 @@ instance Binary PTerm where

11531158 9 -> do x1 <- get

11541159 return (PFalse x1)

11551160 10 -> do x1 <- get

1156− return (PRefl x1)

1161+ x2 <- get

1162+ return (PRefl x1 x2)

11571163 11 -> do x1 <- get

11581164 return (PResolveTC x1)

11591165 12 -> do x1 <- get

src/Idris/Parser.hs+4−1

@@ -665,7 +665,10 @@ pTacticsExpr syn = do

665665pSimpleExpr syn =

666666 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)

667667 <|> do lchar '?'; x <- pName; return (PMetavar x)

668− <|> do reserved "refl"; fc <- pfc; return (PRefl fc)

668+ <|> do reserved "refl"; fc <- pfc;

669+ tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';

670+ return t)

671+ return (PRefl fc tm)

669672-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)

670673 <|> pProofExpr syn

671674 <|> pTacticsExpr syn

src/Idris/Prover.hs+2−2

@@ -60,9 +60,9 @@ elabStep st e = do case runStateT e st of

6060 fail (pshow i a)

6161

6262dumpState :: IState -> ProofState -> IO ()

63−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) =

63+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _ _) =

6464 putStrLn . render $ pretty nm <> colon <+> text "No more goals."

65−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do

65+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ _ problems i _ _ ctxy _ _) = do

6666 let OK ty = goalAtFocus ps

6767 let OK env = envAtFocus ps

6868 putStrLn . render $

src/Idris/REPL.hs+7−2

@@ -323,11 +323,16 @@ process fn (Compile target f)

323323 compile target f m

324324 where fc = FC "main" 0

325325process fn (LogLvl i) = setLogLevel i

326+-- Elaborate as if LHS of a pattern (debug command)

327+process fn (Pattelab t)

328+ = do (tm, ty) <- elabVal toplevel True t

329+ iputStrLn $ show tm ++ "\n\n : " ++ show ty

330+

326331process fn (Missing n) = do i <- get

327332 case lookupDef Nothing n (tt_ctxt i) of

328333 [CaseOp _ _ _ args t _ _]

329− -> do tms <- genMissing args t

330− iputStrLn (show tms)

334+ -> do tms <- genMissing n args t

335+ iputStrLn (showSep "\n" (map (showImp True) tms))

331336 [] -> iputStrLn $ show n ++ " undefined"

332337 _ -> iputStrLn $ "Ambiguous name"

333338process fn Metavars

src/Idris/REPLParser.hs+1

@@ -49,6 +49,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

4949 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

5050 <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))

5151 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

52+ <|> try (do cmd ["patt"]; t <- pFullExpr defaultSyntax; return (Pattelab t))

5253 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

5354 <|> do eof; return NOP

5455

test/test014/resimp.idr+3

@@ -60,11 +60,14 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

6060 update : (gam : Vect Ty n) -> HasType gam i b -> Ty -> Vect Ty n

6161 update (x :: xs) stop y = y :: xs

6262 update (x :: xs) (pop k) y = x :: update xs k y

63+ update Nil stop _ impossible

6364

65+ total

6466 envUpdate : (p:HasType gam i a) -> (val:interpTy b) ->

6567 Env gam -> Env (update gam p b)

6668 envUpdate stop val (x :: xs) = val :: xs

6769 envUpdate (pop k) val (x :: xs) = x :: envUpdate k val xs

70+ envUpdate stop _ Nil impossible

6871

6972 envTail : Env (a :: gam) -> Env gam

7073 envTail (x :: xs) = xs

test/test015/test015.idr+9−5

@@ -5,11 +5,13 @@ import system

55

66data Bit : Nat -> Set where

77 b0 : Bit 0

8− b1 : Bit 1

8+ b1 : Bit 1

99

1010instance Show (Bit n) where

11− show b0 = "0"

12− show b1 = "1"

11+ show = show' where

12+ show' : Bit x -> String

13+ show' b0 = "0"

14+ show' b1 = "1"

1315

1416infixl 5 #

1517

@@ -18,8 +20,10 @@ data Binary : (width : Nat) -> (value : Nat) -> Set where

1820 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

1921

2022instance Show (Binary w k) where

21− show zero = ""

22− show (bin # bit) = show bin ++ show bit

23+ show = show' where

24+ show' : Binary w' k' -> String

25+ show' zero = ""

26+ show' (bin # bit) = show bin ++ show bit

2327

2428pad : Binary w n -> Binary (S w) n

2529pad zero = zero # b0

tutorial/examples/binary.idr+5−3

@@ -6,9 +6,11 @@ data Binary : Nat -> Set where

66 bI : Binary n -> Binary (S (n + n))

77

88instance Show (Binary n) where

9− show (bO x) = show x ++ "0"

10− show (bI x) = show x ++ "1"

11− show bEnd = ""

9+ show = show' where

10+ show' : Binary n' -> String

11+ show' (bO x) = show x ++ "0"

12+ show' (bI x) = show x ++ "1"

13+ show' bEnd = ""

1214

1315data Parity : Nat -> Set where

1416 even : Parity (n + n)