c3f26e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Normalise before case split

c3f26e9Edwin Brady13 years ago

src/Idris/CaseSplit.hs+4−1

compare with master

unifiedsplit

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

54 = do ist <- getIState

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

56 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

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

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

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

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

60-- iputStrLn (show pats)

63-- iputStrLn (show pats)

src/Idris/ElabDecls.hs+7−4

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

1249

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

1251-- happen if elaborating as a pattern clause)

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

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

1253−elabValBind info aspat tm_in

1253+elabValBind info aspat norm tm_in

1254 = do ctxt <- getContext

1255 i <- getIState

1256 let tm = addImpl i tm_in

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

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

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

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

1279 let bargs = getPBtys vtm

1282 let bargs = getPBtys vtm

1280

1283

1281 return (vtm, vty, bargs)

1284 return (vtm, vty, bargs)

1282

1285

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

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

1284elabVal info aspat tm_in

1287elabVal info aspat tm_in

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

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

1286 return (tm, ty)

1289 return (tm, ty)

1287

1290

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

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