Add paranoid option in Check, disabled by default

Ignore-this: 883d1e986ddb705c9d940267ae335697

darcs-hash:20111021102508-e29d1-1de6f9faca27cd8ec6c892a8913809017151cdc5.gz

src/Language/Inch/Check.lhs

@@ -18,11 +18,16 @@
 > import Language.Inch.Syntax
 
 
+Set this to True in order to verify the context regularly:
+
+> paranoid = False
+
+
 > traceContext s = getContext >>= \ g -> mtrace (s ++ "\n" ++ renderMe g)
 
 > defines :: Context -> Var () k -> Bool
 > defines B0                 _            = False
-> defines (g :< A (b := _))  a | a =?= b  = True
+> defines (_ :< A (b := _))  a | a =?= b  = True
 > defines (g :< _)           a            = defines g a
 
 > goodCx :: Context -> Bool
@@ -36,19 +41,19 @@
 
 > goodTyDef :: Context -> TyDef k -> Bool
 > goodTyDef g (Some t)  = goodTy g t
-> goodTyDef g Hole      = True
-> goodTyDef g Fixed     = True
-> goodTyDef g Exists    = True
+> goodTyDef _ Hole      = True
+> goodTyDef _ Fixed     = True
+> goodTyDef _ Exists    = True
 
 > goodFV :: FV t () => Context -> t -> Bool
 > goodFV g = getAll . fvFoldMap (All . defines g)
 
 > goodLayer :: Context -> TmLayer -> Bool
 > goodLayer g (PatternTop (_ ::: s))  = goodTy g s
-> goodLayer g CaseTop                 = True
-> goodLayer g FunTop                  = True
-> goodLayer g GenMark                 = True
-> goodLayer g GuardTop                = True
+> goodLayer _ CaseTop                 = True
+> goodLayer _ FunTop                  = True
+> goodLayer _ GenMark                 = True
+> goodLayer _ GuardTop                = True
 > goodLayer g (LamBody (_ ::: t))     = goodTy g t
 > goodLayer g (LetBindings bs)        = goodBindings g bs
 > goodLayer g (LetBody bs)            = goodBindings g bs
@@ -63,16 +68,17 @@
 > goodDecl :: Context -> Declaration () -> Bool
 > goodDecl g (SigDecl _ t)        = goodTy g t
 > goodDecl g (DataDecl _ _ cs _)  = all (\ (_ ::: t) -> goodTy g t) cs
-> goodDecl g (FunDecl _ _)        = True
+> goodDecl _ (FunDecl _ _)        = True
 
 
 > verifyContext :: Bool -> String -> Contextual ()
-> verifyContext before s = do
+> verifyContext before s | paranoid = do
 >     g <- getContext
 >     unless (goodCx g) $ do
 >         traceContext $ "verifyContext: failed " ++ (if before then "before " else "after ") ++ s
 >         erk "Game over."
 >     return ()
+> verifyContext _ _ = return ()
 
 > wrapVerify :: String -> Contextual t -> Contextual t
 > wrapVerify s m = verifyContext True s *> m <* verifyContext False s