c3f26e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Normalise before case split

Allows case split to work on type synonyms. Fixes #805.

commitc3f26e9a5320eead07a8422b92bc276d68bbf827 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 21 Apr 2014, 15:14 (13 years ago) parent9abed6a

2 files changed+11−5

compare with master

unifiedsplit

src/Idris/CaseSplit.hs+4−1 src/Idris/ElabDecls.hs+7−4

src/Idris/CaseSplit.hs+4−1

@@ -54,7 +54,10 @@ split n t'

5454 = do ist <- getIState

5555 -- Make sure all the names in the term are accessible

5656 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')

57− (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')

57+ (tm, ty, pats) <- elabValBind toplevel True True (addImplPat ist t')

58+ -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

59+ -- need to do anything special to find out what family each argument

60+ -- is in

5861 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)

5962-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))

6063-- iputStrLn (show pats)

src/Idris/ElabDecls.hs+7−4

@@ -1249,8 +1249,8 @@ elabPE info fc caller r =

12491249

12501250-- Elaborate a value, returning any new bindings created (this will only

12511251-- happen if elaborating as a pattern clause)

1252−elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

1253−elabValBind info aspat tm_in

1252+elabValBind :: ElabInfo -> Bool -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

1253+elabValBind info aspat norm tm_in

12541254 = do ctxt <- getContext

12551255 i <- getIState

12561256 let tm = addImpl i tm_in

@@ -1275,14 +1275,17 @@ elabValBind info aspat tm_in

12751275 logLvl 3 ("Value: " ++ show vtm)

12761276-- recheckC (fileFC "(input)") [] tm'

12771277-- logLvl 2 (show vtm)

1278− (vtm, vty) <- recheckC (fileFC "(input)") [] vtm

1278+ (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm

1279+

1280+ let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

1281+ else vtm_in

12791282 let bargs = getPBtys vtm

12801283

12811284 return (vtm, vty, bargs)

12821285

12831286elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

12841287elabVal info aspat tm_in

1285− = do (tm, ty, _) <- elabValBind info aspat tm_in

1288+ = do (tm, ty, _) <- elabValBind info aspat False tm_in

12861289 return (tm, ty)

12871290

12881291-- checks if the clause is a possible left hand side. Returns the term if