3edbd8e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Handle impossible cases on defineFunction

3edbd8eDavid Raymond Christiansen11 years ago

src/Idris/Elab/Term.hs+23−3

compare with master

unifiedsplit

@@ -1782,6 +1782,25 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1782 pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)

1783 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs

1784

1785+ requireError :: Err -> ElabD a -> ElabD ()

1786+ requireError orErr elab =

1787+ do state <- get

1788+ case runStateT elab state of

1789+ OK (_, state') -> lift (tfail orErr)

1790+ Error e -> return ()

1791+

1792+ -- create a fake TT term for the LHS of an impossible case

1793+ fakeTT :: Raw -> Term

1794+ fakeTT (Var n) =

1795+ case lookupNameDef n (tt_ctxt ist) of

1796+ [(n', TyDecl nt _)] -> P nt n' Erased

1797+ _ -> P Ref n Erased

1798+ fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)

1799+ fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)

1800+ fakeTT RType = TType (UVar (-1))

1801+ fakeTT (RUType u) = UType u

1802+ fakeTT (RConstant c) = Constant c

1803+

1785 defineFunction :: RFunDefn Raw -> ElabD ()

1804 defineFunction :: RFunDefn Raw -> ElabD ()

1786 defineFunction (RDefineFun n clauses) =

1805 defineFunction (RDefineFun n clauses) =

1787 do ctxt <- get_context

1806 do ctxt <- get_context

@@ -1794,10 +1813,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1794 lift $ converts ctxt [] lty rty

1813 lift $ converts ctxt [] lty rty

1795 return $ Right (lhs', rhs')

1814 return $ Right (lhs', rhs')

1796 RMkImpossibleClause lhs ->

1815 RMkImpossibleClause lhs ->

1816+ do requireError (Msg "Not an impossible case") . lift $

1797− do lhs' <- fmap fst . lift $ check ctxt [] lhs

1817+ check ctxt [] lhs

1798− return $ Left lhs')

1818+ return $ Left (fakeTT lhs))

1799 let clauses'' = map (\case Right c -> pullVars c

1819 let clauses'' = map (\case Right c -> pullVars c

1800− Left lhs -> let (ns, lhs') = patvars [] lhs'

1820+ Left lhs -> let (ns, lhs') = patvars [] lhs

1801 in (ns, lhs', Impossible))

1821 in (ns, lhs', Impossible))

1802 clauses'

1822 clauses'

1803 let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''

1823 let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''

test/meta004/expected+3

@@ -0,0 +1,3 @@

1+meta004.idr:48:1-9:

2+While running an elaboration script, the following error occurred:

3+Not an impossible case

test/meta004/meta004.idr+23

@@ -1,3 +1,4 @@

1+import Data.Fin

1import Language.Reflection.Utils

2import Language.Reflection.Utils

2import Pruviloj.Core

3import Pruviloj.Core

@@ -23,3 +24,25 @@ total

23p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b

24p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b

24p Z right = Refl

25p Z right = Refl

25p (S left) right = Refl

26p (S left) right = Refl

27+

28+

29+-- Test handling of impossible clauses in function definitions

30+foo : Fin Z -> Nat

31+bar : Nat -> Fin Z

32+

33+doit : Elab ()

34+doit = defineFunction $

35+ DefineFun `{foo} [MkImpossibleClause

36+ (RBind `{{n}}

37+ (PVar (Var `{Nat}))

38+ (RApp (Var `{foo})

39+ (RApp (Var `{FZ}) (Var `{{n}}))))]

40+

41+domore : Elab ()

42+domore = defineFunction $

43+ DefineFun `{foo} [MkImpossibleClause $

44+ RBind `{{k}} (PVar `(Nat)) $

45+ RApp (Var `{bar}) (Var `{{k}})]

46+

47+%runElab doit

48+%runElab domore