9a7f7d9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make 'case' more flexible with dependent types

Implicit variables remain implicit in the generated case (or, more accurately, variables which are unused in the rhs are made implicit on the lhs), meaning that it is no longer necessary for each branch to target the same type or for each case of the scrutinee to have the same type. In other words, case is now allowed provided that it does not affect the form of any variable which is explicitly used in the case block. Example, which is now allowed but wasn't before: app : Vect n a -> Vect m a -> Vect (n + m) a app xs ys = case xs of [] => ys (x :: xs) => x :: app xs ys

commit9a7f7d9a34614925561da1d8518c5e805aa10b88 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 10 Jul 2015, 11:13 (11 years ago) parent203945b

4 files changed+27−8

compare with master

unifiedsplit

CHANGELOG+3 src/Idris/AbsSyntaxTree.hs+2 src/Idris/Elab/Term.hs+21−5 test/proof003/test015.idr+1−3

CHANGELOG+3

@@ -19,6 +19,9 @@ New in 0.9.19:

1919 format sent by the IDE mode, and is saved in a file with the extension ".idh".

2020* Use predicates instead of boolean equality proofs as preconditions

2121 on List functions

22+* More flexible 'case' construct, allowing each branch to target different

23+ types, provided that the case analysis does not affect the form of any

24+ variable used in the right hand side of the case.

2225

2326New in 0.9.18:

2427--------------

src/Idris/AbsSyntaxTree.hs+2

@@ -2043,10 +2043,12 @@ allNamesIn tm = nub $ ni [] tm

20432043 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f

20442044 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc

20452045 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2046+ ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc

20462047 ni env (PHidden tm) = ni env tm

20472048 ni env (PRewrite _ l r _) = ni env l ++ ni env r

20482049 ni env (PTyped l r) = ni env l ++ ni env r

20492050 ni env (PPair _ _ l r) = ni env l ++ ni env r

2051+ ni env (PDPair _ _ (PRef _ n) Placeholder r) = n : ni env r

20502052 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

20512053 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

20522054 ni env (PAlternative a ls) = concatMap (ni env) ls

src/Idris/Elab/Term.hs+21−5

@@ -967,7 +967,7 @@ elab ist info emode opts fn tm

967967 -- if the scrutinee is one of the 'args' in env, we should

968968 -- inspect it directly, rather than adding it as a new argument

969969 let newdef = PClauses fc [] cname'

970− (caseBlock fc cname'

970+ (caseBlock fc cname' scr

971971 (map (isScr scr) (reverse args')) opts)

972972 -- elaborate case

973973 updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } )

@@ -1161,9 +1161,10 @@ elab ist info emode opts fn tm

11611161 isScr (PRef _ n) (n', b) = (n', (n == n', b))

11621162 isScr _ (n', b) = (n', (False, b))

11631163

1164− caseBlock :: FC -> Name ->

1165− [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]

1166− caseBlock fc n env opts

1164+ caseBlock :: FC -> Name

1165+ -> PTerm -- original scrutinee

1166+ -> [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]

1167+ caseBlock fc n scr env opts

11671168 = let args' = findScr env

11681169 args = map mkarg (map getNmScr args') in

11691170 map (mkClause args) opts

@@ -1189,18 +1190,33 @@ elab ist info emode opts fn tm

11891190 mkarg (n, s) = (PRef fc n, s)

11901191 -- may be shadowed names in the new pattern - so replace the

11911192 -- old ones with an _

1193+ -- Also, names which don't appear on the rhs should not be

1194+ -- fixed on the lhs, or this restricts the kind of matching

1195+ -- we can do to non-dependent types.

11921196 mkClause args (l, r)

11931197 = let args' = map (shadowed (allNamesIn l)) args

1198+ args'' = map (implicitable (allNamesIn r ++

1199+ keepscrName scr)) args'

11941200 lhs = PApp (getFC fc l) (PRef NoFC n)

1195− (map (mkLHSarg l) args') in

1201+ (map (mkLHSarg l) args'') in

11961202 PClause (getFC fc l) n lhs [] r []

11971203

1204+ -- Keep scrutinee available if it's just a name (this makes

1205+ -- the names in scope look better when looking at a hole on

1206+ -- the rhs of a case)

1207+ keepscrName (PRef _ n) = [n]

1208+ keepscrName _ = []

1209+

11981210 mkLHSarg l (tm, True) = pexp l

11991211 mkLHSarg l (tm, False) = pexp tm

12001212

12011213 shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)

12021214 shadowed new t = t

12031215

1216+ implicitable rhs (PRef _ n, s) | n `notElem` rhs = (Placeholder, s)

1217+ implicitable rhs t = t

1218+

1219+

12041220 getFC d (PApp fc _ _) = fc

12051221 getFC d (PRef fc _) = fc

12061222 getFC d (PAlternative _ (x:_)) = getFC d x

test/proof003/test015.idr+1−3

@@ -106,9 +106,7 @@ Main.ntbEven = proof {

106106-- There is almost certainly an easier proof. I don't care, for now :)

107107

108108Main.adc_lemma_2 = proof {

109− intro w,v,num0,bit0

110− intro b0,v1,num1,bit1,b1

111− intro c,bc,x,bX,x1,bX1

109+ intro w,v,num0,v1,num1,x,bx,x1,bx1,bit0,b0,bit1,b1,c,bc

112110 rewrite sym (plusZeroRightNeutral x);

113111 rewrite sym (plusZeroRightNeutral v1);

114112 rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));