summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Coverage.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Coverage.hs')
-rw-r--r--src/full/Agda/TypeChecking/Coverage.hs73
1 files changed, 48 insertions, 25 deletions
diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs
index e71c431..f110bb8 100644
--- a/src/full/Agda/TypeChecking/Coverage.hs
+++ b/src/full/Agda/TypeChecking/Coverage.hs
@@ -1,9 +1,9 @@
{-# OPTIONS_GHC -fwarn-unused-imports #-}
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TupleSections #-}
{-| Coverage checking, case splitting, and splitting for refine tactics.
@@ -18,19 +18,22 @@ module Agda.TypeChecking.Coverage
, splitResult
) where
+import Prelude hiding (null)
+
import Control.Monad
import Control.Monad.Trans ( lift )
+
+#if !MIN_VERSION_base(4,8,0)
import Control.Applicative hiding (empty)
+#endif
-import Data.List
-import qualified Data.Set as Set
+import Data.List hiding (null)
import Data.Set (Set)
+import qualified Data.Set as Set
import qualified Data.Traversable as Trav
-import Agda.Syntax.Position
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Common hiding (Arg,Dom)
-import qualified Agda.Syntax.Common as C
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
@@ -42,7 +45,7 @@ import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Exception
import Agda.TypeChecking.Monad.Context
-import Agda.TypeChecking.Rules.LHS.Problem (FlexibleVar(..),flexibleVarFromHiding)
+import Agda.TypeChecking.Rules.LHS.Problem (flexibleVarFromHiding)
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.LHS.Instantiate (instantiateTel)
import Agda.TypeChecking.Rules.LHS (instantiatePattern)
@@ -65,6 +68,7 @@ import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
@@ -150,14 +154,14 @@ coverageCheck f t cs = do
whenM (optCompletenessCheck <$> pragmaOptions) $
-- report an error if there are uncovered cases
unless (null pss) $
- setCurrentRange (getRange cs) $
+ setCurrentRange cs $
typeError $ CoverageFailure f (map (map $ fmap namedThing) pss)
-- is = indices of unreachable clauses
let is = Set.toList $ Set.difference (Set.fromList [0..genericLength cs - 1]) used
-- report an error if there are unreachable clauses
unless (null is) $ do
let unreached = map (cs !!) is
- setCurrentRange (getRange unreached) $
+ setCurrentRange unreached $
typeError $ UnreachableClauses f (map clausePats unreached)
return splitTree
@@ -209,7 +213,7 @@ cover f cs sc@(SClause tel perm ps _ target) = do
r <- altM1 (split Inductive sc) xs
case r of
Left err -> case err of
- CantSplit c tel us vs _ -> typeError $ CoverageCantSplitOn c tel us vs
+ CantSplit c tel us vs -> typeError $ CoverageCantSplitOn c tel us vs
NotADatatype a -> enterClosure a $ typeError . CoverageCantSplitType
IrrelevantDatatype a -> enterClosure a $ typeError . CoverageCantSplitIrrelevantType
CoinductiveDatatype a -> enterClosure a $ typeError . CoverageCantSplitType
@@ -286,6 +290,7 @@ fixTarget sc@SClause{ scTel = sctel, scPerm = perm, scPats = ps, scSubst = sigma
[ text "split clause telescope: " <+> prettyTCM sctel
, text "old permutation : " <+> prettyTCM perm
, text "old patterns : " <+> sep (map (prettyTCM . namedArg) ps)
+ , text "substitution : " <+> text (show sigma)
]
reportSDoc "tc.cover.target" 30 $ sep
[ text "target type before substitution (variables may be wrong): " <+> do
@@ -314,6 +319,23 @@ fixTarget sc@SClause{ scTel = sctel, scPerm = perm, scPats = ps, scSubst = sigma
, scSubst = liftS n $ sigma
, scTarget = newTarget
}
+ -- Separate debug printing to find cause of crash (Issue 1374)
+ reportSDoc "tc.cover.target" 30 $ sep
+ [ text "new split clause telescope : " <+> prettyTCM sctel'
+ ]
+ reportSDoc "tc.cover.target" 30 $ sep
+ [ text "new split clause permutation : " <+> prettyTCM perm'
+ ]
+ reportSDoc "tc.cover.target" 30 $ sep
+ [ text "new split clause patterns : " <+> sep (map (prettyTCM . namedArg) ps')
+ ]
+ reportSDoc "tc.cover.target" 30 $ sep
+ [ text "new split clause substitution: " <+> text (show $ scSubst sc')
+ ]
+ reportSDoc "tc.cover.target" 30 $ sep
+ [ text "new split clause target : " <+> do
+ addContext sctel' $ prettyTCM $ fromJust newTarget
+ ]
reportSDoc "tc.cover.target" 20 $ sep
[ text "new split clause"
, prettyTCM sc'
@@ -395,14 +417,12 @@ computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps c = do
unifyIndices flex (raise (size gamma) dtype) conIxs givenIxs
case r of
- NoUnify _ _ _ -> do
- debugNoUnify
- return Nothing
- DontKnow _ -> do
+ NoUnify {} -> debugNoUnify $> Nothing
+
+ DontKnow{} -> do
debugCantSplit
throwException $ CantSplit (conName con) (delta1 `abstract` gamma) conIxs givenIxs
- (map (var . flexVar) flex)
- Unifies sub -> do
+ Unifies sub -> do
debugSubst "sub" sub
-- Substitute the constructor for x in Δ₂: Δ₂' = Δ₂[conv/x]
@@ -411,14 +431,16 @@ computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps c = do
debugTel "delta2'" delta2'
-- Compute a substitution ρ : Δ₁ΓΔ₂' → Δ₁(x:D)Δ₂'
- let rho = liftS (size delta2') $ conv :# raiseS (size gamma)
+ let rho = liftS (size delta2') $ consS conv $ raiseS (size gamma)
-- [ Var i [] | i <- [0..size delta2' - 1] ]
-- ++ [ raise (size delta2') conv ]
-- ++ [ Var i [] | i <- [size delta2' + size gamma ..] ]
-- Plug the hole with the constructor and apply ρ
- -- TODO: Is it really correct to use Nothing here?
- let conp = ConP con Nothing $ map (fmap namedVarP) $ teleArgNames gamma
+ -- Andreas, 2015-05-01 I guess it is fine to use @noConPatternInfo@
+ -- as the result of splitting is never used further down the pipeline.
+ -- After splitting, Agda reloads the file.
+ let conp = ConP con noConPatternInfo $ map (fmap namedVarP) $ teleArgNames gamma
ps = plugHole conp hps
ps' = applySubst rho ps -- Δ₁ΓΔ₂' ⊢ ps'
debugPlugged ps ps'
@@ -585,8 +607,8 @@ split' ind sc@(SClause tel perm ps _ target) (BlockingVar x mcons) = liftTCM $ r
-- Split the telescope at the variable
-- t = type of the variable, Δ₁ ⊢ t
(n, t, delta1, delta2) <- do
- let (tel1, C.Dom info (n, t) : tel2) = genericSplitAt (size tel - x - 1) $ telToList tel
- return (n, C.Dom info t, telFromList tel1, telFromList tel2)
+ let (tel1, Common.Dom info (n, t) : tel2) = genericSplitAt (size tel - x - 1) $ telToList tel
+ return (n, Common.Dom info t, telFromList tel1, telFromList tel2)
-- Compute the one hole context of the patterns at the variable
(hps, hix) <- do
@@ -741,8 +763,9 @@ instance PrettyTCM SplitClause where
, text "target = " <+> do
caseMaybe target empty $ \ t -> do
addContext tel $ prettyTCM t
- , text "subst target = " <+> do
- caseMaybe target empty $ \ t -> do
- addContext tel $ prettyTCM $ applySubst sigma t
+ -- Triggers crash (see Issue 1374).
+ -- , text "subst target = " <+> do
+ -- caseMaybe target empty $ \ t -> do
+ -- addContext tel $ prettyTCM $ applySubst sigma t
]
]