@@ -1,5 +1,6 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
22 PatternGuards #-}
3+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
34
45module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
56 rt_simplify, simplify, specialise, hnf, convEq, convEq',
@@ -157,6 +158,7 @@ bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
157158unbindEnv :: EnvTT n -> TT n -> TT n
158159unbindEnv [] tm = tm
159160unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
161+unbindEnv env tm = error $ "Impossible case occurred: couldn't unbind env."
160162
161163usable :: Bool -- specialising
162164 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
@@ -764,6 +766,7 @@ instance Show Totality where
764766 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
765767 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++
766768 showSep " --> " (map show ns)
769+ show (Partial (UseUndef n)) = "possibly not total because it uses the undefined name " ++ show n
767770
768771{-!
769772deriving instance Binary Accessibility
@@ -866,22 +869,23 @@ addCasedef :: Name -> ErasureInfo -> CaseInfo ->
866869 [([Name], Term, Term)] -> -- compile time
867870 [([Name], Term, Term)] -> -- inlined
868871 [([Name], Term, Term)] -> -- run time
869− Type -> Context -> Context
872+ Type -> Context -> TC Context
870873addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
871874 tcase covering reflect asserted argtys inacc
872875 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt
873− = let ctxt = definitions uctxt
874− access = case lookupDefAcc n False uctxt of
875− [(_, acc)] -> acc
876− _ -> Public
877− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei,
878− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei,
879− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei,
880− simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei) of
881− (OK (CaseDef args_tot sc_tot _),
882− OK (CaseDef args_ct sc_ct _),
883− OK (CaseDef args_inl sc_inl _),
884− OK (CaseDef args_rt sc_rt _)) ->
876+ = do let ctxt = definitions uctxt
877+ access = case lookupDefAcc n False uctxt of
878+ [(_, acc)] -> acc
879+ _ -> Public
880+ totalityTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei
881+ compileTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei
882+ inlined <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei
883+ runtime <- simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei
884+ ctxt' <- case (totalityTime, compileTime, inlined, runtime) of
885+ (CaseDef args_tot sc_tot _,
886+ CaseDef args_ct sc_ct _,
887+ CaseDef args_inl sc_inl _,
888+ CaseDef args_rt sc_rt _) ->
885889 let inl = alwaysInline -- tcdict
886890 inlc = (inl || small n args_ct sc_ct) && (not asserted)
887891 inlr = inl || small n args_rt sc_rt
@@ -892,28 +896,27 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
892896 op = (CaseOp (ci { case_inlinable = inlc })
893897 ty argtys ps_in ps_tot cdef,
894898 access, Unchecked, EmptyMI)
895− in addDef n op ctxt
896− other -> error ("Error adding case def: " ++ show other)
897− in uctxt { definitions = ctxt' }
899+ in return $ addDef n op ctxt
900+-- other -> tfail (Msg $ "Error adding case def: " ++ show other)
901+ return uctxt { definitions = ctxt' }
898902
899903-- simplify a definition for totality checking
900−simplifyCasedef :: Name -> ErasureInfo -> Context -> Context
904+simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context
901905simplifyCasedef n ei uctxt
902− = let ctxt = definitions uctxt
903− ctxt' = case lookupCtxt n ctxt of
904− [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->
905− ctxt -- nothing to simplify (or already done...)
906− [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->
907− let ps_in' = map simpl ps_in
908− pdef = map debind ps_in' in
909− case simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei of
910− OK (CaseDef args sc _) ->
911− addDef n (CaseOp ci
912− ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),
913− acc, tot, metainf) ctxt
914− Error err -> error (show err)
915− _ -> ctxt in
916− uctxt { definitions = ctxt' }
906+ = do let ctxt = definitions uctxt
907+ ctxt' <- case lookupCtxt n ctxt of
908+ [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->
909+ return ctxt -- nothing to simplify (or already done...)
910+ [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->
911+ do let ps_in' = map simpl ps_in
912+ pdef = map debind ps_in'
913+ CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei
914+ return $ addDef n (CaseOp ci
915+ ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),
916+ acc, tot, metainf) ctxt
917+
918+ _ -> return ctxt
919+ return uctxt { definitions = ctxt' }
917920 where
918921 depat acc (Bind n (PVar t) sc)
919922 = depat (n : acc) (instantiate (P Bound n t) sc)
@@ -1068,6 +1071,7 @@ lookupVal n ctxt
10681071 case tfst def of
10691072 (Function _ htm) -> return (veval ctxt [] htm)
10701073 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
1074+ _ -> []
10711075
10721076lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
10731077lookupTyEnv n env = li n 0 env where