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

lib/prelude/nat.idr+4−4

compare with master

unifiedsplit

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

239-- Succ

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

241 S left = S right

242−eqSucc left right refl = refl

242+eqSucc left _ refl = refl

243

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

245 left = right

246−succInjective left right refl = refl

246+succInjective left _ refl = refl

247

248-- Plus

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

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

278

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

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

281−plusConstantRight left right c refl = refl

281+plusConstantRight left _ c refl = refl

282

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

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

285−plusConstantLeft left right c refl = refl

285+plusConstantLeft left _ c refl = refl

286

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

288plusOneSucc n = refl

lib/prelude/vect.idr−1

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

34index fO (x::xs) = x

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

36index fO [] impossible

37−index (fS _) [] impossible

38

37

39--------------------------------------------------------------------------------

38--------------------------------------------------------------------------------

40-- Subvectors

39-- Subvectors

src/Core/CaseTree.hs+14−7

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

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

18 | STerm Term

19 | UnmatchedCase String -- error message

20+ | ImpossibleCase -- already checked to be impossible

20 deriving (Eq, Ord)

21 deriving (Eq, Ord)

21{-!

22{-!

22deriving instance Binary SC

23deriving instance Binary SC

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

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

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

40 show' i (STerm tm) = show tm

41 show' i (STerm tm) = show tm

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

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

43+ show' i ImpossibleCase = "impossible"

42

44

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

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

44

46

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

143 deriving (Show, Eq)

145 deriving (Show, Eq)

144

146

145-- Generate a simple case tree

147-- Generate a simple case tree

146−--

148+-- Work Left to Right at Compile Time

147

149

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

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

149simpleCase tc cover phase fc []

151simpleCase tc cover phase fc []

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

151simpleCase tc cover phase fc cs

153simpleCase tc cover phase fc cs

152 = let proj = phase == RunTime

154 = let proj = phase == RunTime

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

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

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

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

155 chkPats = mapM chkAccessible pats in

157 chkPats = mapM chkAccessible pats in

156 case chkPats of

158 case chkPats of

157 OK pats ->

159 OK pats ->

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

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

159 ns = take numargs args

161 ns = take numargs args

160 (tree, st) = runState

162 (tree, st) = runState

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

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

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

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

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

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

164 Error err -> Error (At fc err)

166 Error err -> Error (At fc err)

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

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

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

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

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

176

178

179+rev CompileTime = id

180+rev _ = reverse

181+

177data Pat = PCon Name Int [Pat]

182data Pat = PCon Name Int [Pat]

178 | PConst Const

183 | PConst Const

179 | PV Name

184 | PV Name

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

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

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

241 = do (ts, v) <- get

246 = do (ts, v) <- get

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

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

248+ case snd ret of

249+ Impossible -> return ImpossibleCase

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

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

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

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

245 cs <- mixture vs ps err

252 cs <- mixture vs ps err

246 return cs

253 return cs

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

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

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

339 SC -> SC

346 SC -> SC

340prune proj (Case n alts)

347prune proj (Case n alts)

341− = let alts' = map pruneAlt $

342− filter notErased alts in

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

343 case alts' of

349 case alts' of

344− [] -> STerm Erased

350+ [] -> ImpossibleCase

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

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

346 else Case n as

352 else Case n as

347 as -> Case n as

353 as -> Case n as

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

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

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

351

357

352 notErased (DefaultCase (STerm Erased)) = False

358 notErased (DefaultCase (STerm Erased)) = False

359+ notErased (DefaultCase ImpossibleCase) = False

353 notErased _ = True

360 notErased _ = True

354

361

355 mkProj n i [] sc = sc

362 mkProj n i [] sc = sc

src/Core/Elaborate.hs+13−12

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

148unique_hole :: Name -> Elab' aux Name

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

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

152 return n'

153 where

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

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

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

318 -- so do nothing

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

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

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

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

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

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

325 unified p

326 unified p

326− let unify = dropGiven dontunify hs

327+ let unify = dropGiven dont hs

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

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

328 end_unify

329 end_unify

329 return (map (updateUnify unify) args)

330 return (map (updateUnify unify) args)

330 where updateUnify hs n = case lookup n hs of

331 where updateUnify hs n = case lookup n hs of

331 Just (P _ t _) -> t

332 Just (P _ t _) -> t

332 _ -> n

333 _ -> 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

338

334

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

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

340apply2 fn elabs =

336apply2 fn elabs =

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

375 when (null claims) (start_unify n)

371 when (null claims) (start_unify n)

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

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

377 claim n (forget t)

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

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

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

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

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

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

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

src/Core/ProofState.hs+24−12

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

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

6

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

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

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

9

10import Core.Typecheck

11import Core.Evaluate

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

24 nextname :: Int, -- name supply

25 pterm :: Term, -- current proof term

26 ptype :: Type, -- original goal

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

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

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

28 solved :: Maybe (Name, Term),

29 solved :: Maybe (Name, Term),

29 problems :: Fails,

30 problems :: Fails,

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

73-- Some utilites on proof and tactic states

74-- Some utilites on proof and tactic states

74

75

75instance Show ProofState where

76instance Show ProofState where

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

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

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

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

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

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

79 wkenv = premises g in

80 wkenv = premises g in

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

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

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

97 showG ps b = showEnv ps (binderTy b)

98 showG ps b = showEnv ps (binderTy b)

98

99

99instance Pretty ProofState where

100instance Pretty ProofState where

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

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

101 if size nm > breakingSize then

102 if size nm > breakingSize then

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

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

103 else

104 else

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

105 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 _ _) =

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

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

107 let wkEnv = premises g in

108 let wkEnv = premises g in

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

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

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

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

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

171newProof n ctxt ty = let h = holeName 0

172newProof n ctxt ty = let h = holeName 0

172 ty' = vToP ty in

173 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, [])

174 Nothing [] []

175 Nothing [] []

175 [] []

176 [] []

176 Nothing ctxt "" False

177 Nothing ctxt "" False

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

351 let (uh, uns) = unified ps

352 let (uh, uns) = unified ps

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

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

353 solved = Just (x, val),

354 solved = Just (x, val),

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

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

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

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

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

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

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

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

487solve_unified ctxt env tm =

489solve_unified ctxt env tm =

488 do ps <- get

490 do ps <- get

489 let (_, ns) = unified ps

491 let (_, ns) = unified ps

492+ let unify = dropGiven (dontunify ps) ns

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

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

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

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

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

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

493− return (updateSolved ns tm)

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

494

505

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

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

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

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

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

519 Nothing -> fail "Nothing to undo."

530 Nothing -> fail "Nothing to undo."

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

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

521processTactic EndUnify ps

532processTactic EndUnify ps

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

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

534+ ns = dropGiven (dontunify ps) ns_in

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

535 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)) $

525 updateSolved ns' (pterm ps)

537 updateSolved ns' (pterm ps)

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

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

527 case probs' of

539 case probs' of

src/Core/TT.hs+2

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

414 | Constant Const

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

416 | Erased

417+ | Impossible -- special case for totality checking

417 | Set UExp

418 | Set UExp

418 deriving (Ord, Functor)

419 deriving (Ord, Functor)

419{-!

420{-!

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

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

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

713 se p env (Constant c) = show c

714 se p env (Constant c) = show c

714 se p env Erased = "[__]"

715 se p env Erased = "[__]"

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

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

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

716

718

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

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

src/Idris/AbsSyntax.hs+2−2

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

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

502 pri (PTrue _) = 0

503 pri (PFalse _) = 0

504− pri (PRefl _) = 1

504+ pri (PRefl _ _) = 1

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

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

507 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

901 match (PQuote _) _ = return []

902 match (PProof _) _ = return []

903 match (PTactics _) _ = return []

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+7−4

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

152 | Defn Name

153 | Info Name

154 | Missing Name

155+ | Pattelab PTerm

155 | DebugInfo Name

156 | DebugInfo Name

156 | Search PTerm

157 | Search PTerm

157 | SetOpt Opt

158 | SetOpt Opt

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

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

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

364 | PTrue FC

365 | PTrue FC

365 | PFalse FC

366 | PFalse FC

366− | PRefl FC

367+ | PRefl FC PTerm

367 | PResolveTC FC

368 | PResolveTC FC

368 | PEq FC PTerm PTerm

369 | PEq FC PTerm PTerm

369 | PPair FC PTerm PTerm

370 | PPair FC PTerm PTerm

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

777

778

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

889 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 ++ "}"

890 se p (PResolveTC _) = "resolvetc"

893 se p (PResolveTC _) = "resolvetc"

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

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

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

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

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

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

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

963 size (PTrue fc) = 1

966 size (PTrue fc) = 1

964 size (PFalse fc) = 1

967 size (PFalse fc) = 1

965− size (PRefl fc) = 1

968+ size (PRefl fc _) = 1

966 size (PResolveTC fc) = 1

969 size (PResolveTC fc) = 1

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

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

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

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

src/Idris/Coverage.hs+54−19

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

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

20-- Eliminate the ones which cannot be well typed

21

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

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

23+genMissing fn args sc

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

24+ = do sc' <- expandTree sc

24− iputStrLn (show sc')

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

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

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

26−

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+

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

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

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

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

58+ let (got, missing) = unzip m

29− return (concat m)

59+ return (concat got, concat missing)

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

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

61+ t <- mkPTerm fn args

31− return []

62+ return ([t], [])

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

64+ t <- mkPTerm fn args

65+ return ([], [])

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

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

67+ t <- mkPTerm fn args

33− return []

68+ return ([], [t])

34−

69+

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

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

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

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

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

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

38− gm args' sc

73+ gm fn args' sc

39−gmAlt args n (ConstCase c sc)

74+gmAlt fn args n (ConstCase c sc)

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

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

41− gm args' sc

76+ gm fn args' sc

42−gmAlt args n (DefaultCase sc)

77+gmAlt fn args n (DefaultCase sc)

43− = do gm args sc

78+ = do gm fn args sc

44

79

45getDefault (DefaultCase sc : _) = sc

80getDefault (DefaultCase sc : _) = sc

46getDefault (_ : cs) = getDefault cs

81getDefault (_ : cs) = getDefault cs

src/Idris/Delaborate.hs+2−1

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

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

38 de env (Constant i) = PConstant i

39 de env Erased = Placeholder

40+ de env Impossible = Placeholder

40 de env (Set i) = PSet

41 de env (Set i) = PSet

41

42

42 dens x | fullname = x

43 dens x | fullname = x

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

47

48

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

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

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

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

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

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

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

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

53 | n == UN "Exists"

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

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

232

233 solveDeferred n

234− let pats = mapMaybe id pats_in

234+ let pats = pats_in

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

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

236− show l ++ " = " ++

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

237− show r) pats))

237+-- show r) pats))

238 ist <- get

239 let tcase = opt_typecase (idris_options ist)

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

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

241 tclift $ sameLength pdef

242 tclift $ sameLength pdef

242 cov <- coverage

243 cov <- coverage

243 pcover <-

244 pcover <-

244 if cov

245 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

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

248 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

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

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

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

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

253 "\nAgainst: " ++

251 "\nAgainst: " ++

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

255 if null missing'

253 if null missing'

256 then return True

254 then return True

257 else return False

255 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

269 else return False

256 else return False

270 pdef' <- applyOpts pdef

257 pdef' <- applyOpts pdef

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

272 ist <- get

258 ist <- get

273-- let wf = wellFounded ist n sc

259-- let wf = wellFounded ist n sc

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

260 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

314-- addIBC (IBCTotal n tot)

300-- addIBC (IBCTotal n tot)

315 [] -> return ()

301 [] -> return ()

316 where

302 where

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

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

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

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

319− (vs, x', y')

305+ (vs, x', y')

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

307+ (vs, x', Impossible)

308+

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

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

321 depat acc x = (acc, x)

310 depat acc x = (acc, x)

322

311

323 getLHS (_, l, _) = l

312 getLHS (_, l, _) = l

324

313

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

326

316

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

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

328 = do l <- sameLength xs

318 = do l <- sameLength xs

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

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

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

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

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

359 do let lhs_tm = orderPats (getInferTerm lhs')

349 do let lhs_tm = orderPats (getInferTerm lhs')

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

351+ OK _ -> return True

352+ _ -> return False

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

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

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

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

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

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

363 Error _ -> return False

356 Error _ -> return False

364

357

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

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

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

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

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

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

368 case b of

361 case b of

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

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

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

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

372 = do ctxt <- getContext

366 = do ctxt <- getContext

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

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

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

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

424 i <- get

418 i <- get

425 checkInferred fc (delab' i crhs True) rhs

419 checkInferred fc (delab' i crhs True) rhs

426− return $ Just (clhs, crhs)

420+ return $ Right (clhs, crhs)

427 where

421 where

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

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

429 pinfo ns ps i

423 pinfo ns ps i

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

508 addDeferred def'

502 addDeferred def'

509 mapM_ (elabCaseBlock info) is

503 mapM_ (elabCaseBlock info) is

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

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

511− return $ Just (clhs, crhs)

505+ return $ Right (clhs, crhs)

512 where

506 where

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

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

514 getImps _ = []

508 getImps _ = []

src/Idris/ElabTerm.hs+8−19

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

112 | otherwise = try (resolveTC 2 fn ist)

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

114 instanceArg c)

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

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

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

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

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

118 pimp (MN 0 "b") Placeholder,

119 pexp l, pexp r])

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

211 elabE (True, a) val

212 elabE (True, a) sc

213 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'

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

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

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

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

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

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

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

242 = unzip $

229 = unzip $

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

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

244 (zip ns args)

231 (zip ns args)

232+ try

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

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

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

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

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

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

248 [] False (reverse ns')

236 [] False (reverse ns')

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

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

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

317

305

318 elabArgs ina failed retry [] _

306 elabArgs ina failed retry [] _

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

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

320− elabArgs ina [] False ns ts

308+-- elabArgs ina [] False ns ts

321 | otherwise = return ()

309 | otherwise = return ()

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

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

323 = elabArgs ina failed r ns args

311 = elabArgs ina failed r ns args

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

387pruneByType t _ as = as

375pruneByType t _ as = as

388

376

389trivial :: IState -> ElabD ()

377trivial :: 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)

391 return ())

380 return ())

392 (do env <- get_env

381 (do env <- get_env

393 tryAll (map fst env)

382 tryAll (map fst env)

src/Idris/IBC.hs+10−4

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

21import Paths_idris

22

23ibcVersion :: Word8

24−ibcVersion = 21

24+ibcVersion = 22

25

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

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

493 Erased -> putWord8 6

494 Set x1 -> do putWord8 7

495 put x1

496+ Impossible -> putWord8 8

496 get

497 get

497 = do i <- getWord8

498 = do i <- getWord8

498 case i of

499 case i of

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

517 6 -> return Erased

518 6 -> return Erased

518 7 -> do x1 <- get

519 7 -> do x1 <- get

519 return (Set x1)

520 return (Set x1)

521+ 8 -> return Impossible

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

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

521

523

522instance Binary SC where

524instance Binary SC where

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

532 put x1

534 put x1

533 UnmatchedCase x1 -> do putWord8 3

535 UnmatchedCase x1 -> do putWord8 3

534 put x1

536 put x1

537+ ImpossibleCase -> do putWord8 4

535 get

538 get

536 = do i <- getWord8

539 = do i <- getWord8

537 case i of

540 case i of

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

545 return (STerm x1)

548 return (STerm x1)

546 3 -> do x1 <- get

549 3 -> do x1 <- get

547 return (UnmatchedCase x1)

550 return (UnmatchedCase x1)

551+ 4 -> return ImpossibleCase

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

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

549

553

550

554

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

1072 put x1

1076 put x1

1073 PFalse x1 -> do putWord8 9

1077 PFalse x1 -> do putWord8 9

1074 put x1

1078 put x1

1075− PRefl x1 -> do putWord8 10

1079+ PRefl x1 x2 -> do putWord8 10

1076− put x1

1080+ put x1

1081+ put x2

1077 PResolveTC x1 -> do putWord8 11

1082 PResolveTC x1 -> do putWord8 11

1078 put x1

1083 put x1

1079 PEq x1 x2 x3 -> do putWord8 12

1084 PEq x1 x2 x3 -> do putWord8 12

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

1153 9 -> do x1 <- get

1158 9 -> do x1 <- get

1154 return (PFalse x1)

1159 return (PFalse x1)

1155 10 -> do x1 <- get

1160 10 -> do x1 <- get

1161+ x2 <- get

1156− return (PRefl x1)

1162+ return (PRefl x1 x2)

1157 11 -> do x1 <- get

1163 11 -> do x1 <- get

1158 return (PResolveTC x1)

1164 return (PResolveTC x1)

1159 12 -> do x1 <- get

1165 12 -> do x1 <- get

src/Idris/Parser.hs+4−1

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

665pSimpleExpr syn =

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

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

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

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

670 <|> pProofExpr syn

673 <|> pProofExpr syn

671 <|> pTacticsExpr syn

674 <|> pTacticsExpr syn

src/Idris/Prover.hs+2−2

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

60 fail (pshow i a)

61

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

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

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

64 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

66 let OK ty = goalAtFocus ps

67 let OK env = envAtFocus ps

68 putStrLn . render $

src/Idris/REPL.hs+7−2

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

323 compile target f m

324 where fc = FC "main" 0

325process 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+

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

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

327 case lookupDef Nothing n (tt_ctxt i) of

332 case lookupDef Nothing n (tt_ctxt i) of

328 [CaseOp _ _ _ args t _ _]

333 [CaseOp _ _ _ args t _ _]

329− -> do tms <- genMissing args t

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

330− iputStrLn (show tms)

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

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

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

332 _ -> iputStrLn $ "Ambiguous name"

337 _ -> iputStrLn $ "Ambiguous name"

333process fn Metavars

338process fn Metavars

src/Idris/REPLParser.hs+1

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

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

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

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

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

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

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

53 <|> do eof; return NOP

54 <|> do eof; return NOP

54

55

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)

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

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

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

63+ update Nil stop _ impossible

63

64

65+ total

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

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

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

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

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

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

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

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

70+ envUpdate stop _ Nil impossible

68

71

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

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

70 envTail (x :: xs) = xs

73 envTail (x :: xs) = xs

test/test015/test015.idr+9−5

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

5

6data Bit : Nat -> Set where

7 b0 : Bit 0

8− b1 : Bit 1

8+ b1 : Bit 1

9

10instance Show (Bit n) where

11+ show = show' where

12+ show' : Bit x -> String

11− show b0 = "0"

13+ show' b0 = "0"

12− show b1 = "1"

14+ show' b1 = "1"

13

15

14infixl 5 #

16infixl 5 #

15

17

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

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

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

19

21

20instance Show (Binary w k) where

22instance Show (Binary w k) where

23+ show = show' where

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

21− show zero = ""

25+ show' zero = ""

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

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

23

27

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

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

25pad zero = zero # b0

29pad zero = zero # b0

tutorial/examples/binary.idr+5−3

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

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

7

8instance Show (Binary n) where

9+ show = show' where

10+ show' : Binary n' -> String

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

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

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

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

11− show bEnd = ""

13+ show' bEnd = ""

12

14

13data Parity : Nat -> Set where

15data Parity : Nat -> Set where

14 even : Parity (n + n)

16 even : Parity (n + n)