From 5a9ff204e8c8db256d87be878b15f7678395dc30 Mon Sep 17 00:00:00 2001 From: Jennifer Paykin Date: Wed, 3 Nov 2021 09:36:18 -0700 Subject: [PATCH 1/2] Adding debugging annotations for SAW-core functions --- saw-core/src/Verifier/SAW/SCTypeCheck.hs | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index 3fb9119d5a..f06ba01a1e 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/saw-core/src/Verifier/SAW/SCTypeCheck.hs @@ -120,6 +120,11 @@ withVar x tp m = withCtx :: [(LocalName, Term)] -> TCM a -> TCM a withCtx = flip (foldr (\(x,tp) -> withVar x tp)) +-- | Run a type-checking computation while remembering the term given +-- TODO: fix this description +withErrorTerm :: Term -> TCM a -> TCM a +withErrorTerm tm m = + catchError m (throwError . ErrorTerm tm) -- | Run a type-checking computation @m@ and tag any error it throws with the -- given position, using the 'ErrorPos' constructor, unless that error is @@ -166,6 +171,7 @@ data TCError | DeclError Text String | ErrorPos Pos TCError | ErrorCtx LocalName Term TCError + | ErrorTerm Term TCError | ExpectedRecursor TypedTerm @@ -250,6 +256,11 @@ prettyTCError e = runReader (helper e) ([], Nothing) where local (\(ctx,_) -> (ctx, Just p)) $ helper err helper (ErrorCtx x _ err) = local (\(ctx,p) -> (x:ctx, p)) $ helper err + helper (ErrorTerm tm err) = do + info <- ppWithPos [ return ("While typechecking term: ") + , ishow tm ] + cont <- helper err + return (info ++ cont) helper (ExpectedRecursor ttm) = ppWithPos [ return "Expected recursor value", ishow (typedVal ttm), ishow (typedType ttm)] @@ -361,13 +372,13 @@ typeInferCompleteInCtx ctx f = -- Type inference for Term dispatches to type inference on TermF Term, but uses -- memoization to avoid repeated work instance TypeInfer Term where - typeInfer (Unshared tf) = typeInfer tf - typeInfer (STApp{ stAppIndex = i, stAppTermF = tf}) = + typeInfer t@(Unshared tf) = withErrorTerm t $ typeInfer tf + typeInfer t@(STApp{ stAppIndex = i, stAppTermF = tf}) = do table <- get case Map.lookup i table of Just x -> return x Nothing -> - do x <- typeInfer tf + do x <- withErrorTerm t $ typeInfer tf x' <- typeCheckWHNF x modify (Map.insert i x') return x' From 04932e9813a032033bbff68ed22725188d381ec1 Mon Sep 17 00:00:00 2001 From: Jennifer Paykin Date: Wed, 3 Nov 2021 16:41:50 -0700 Subject: [PATCH 2/2] Adding calls to withErrorTerm to typeInferComplete instances --- saw-core/src/Verifier/SAW/SCTypeCheck.hs | 28 ++++++++++++++++-------- 1 file changed, 19 insertions(+), 9 deletions(-) diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index f06ba01a1e..9d41822947 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/saw-core/src/Verifier/SAW/SCTypeCheck.hs @@ -120,11 +120,18 @@ withVar x tp m = withCtx :: [(LocalName, Term)] -> TCM a -> TCM a withCtx = flip (foldr (\(x,tp) -> withVar x tp)) --- | Run a type-checking computation while remembering the term given --- TODO: fix this description +-- | Run a type-checking computation @m@ and tag any error it throws with the +-- 'ErrorTerm' constructor withErrorTerm :: Term -> TCM a -> TCM a -withErrorTerm tm m = - catchError m (throwError . ErrorTerm tm) +withErrorTerm tm m = catchError m (throwError . ErrorTerm tm) + +-- | Lift @withErrorTerm@ to `TermF Term` +withErrorTermF :: TermF Term -> TCM a -> TCM a +withErrorTermF tm = withErrorTerm (Unshared tm) + +-- | Lift @withErrorTerm@ to `TermF TypedTerm` +withErrorTypedTermF :: TermF TypedTerm -> TCM a -> TCM a +withErrorTypedTermF tm = withErrorTermF (fmap typedVal tm) -- | Run a type-checking computation @m@ and tag any error it throws with the -- given position, using the 'ErrorPos' constructor, unless that error is @@ -382,7 +389,7 @@ instance TypeInfer Term where x' <- typeCheckWHNF x modify (Map.insert i x') return x' - typeInferComplete trm = TypedTerm trm <$> typeInfer trm + typeInferComplete trm = TypedTerm trm <$> withErrorTerm trm (typeInfer trm) -- Type inference for TermF Term dispatches to that for TermF TypedTerm by -- calling inference on all the sub-components and extending the context inside @@ -411,7 +418,7 @@ instance TypeInfer (TermF Term) where return $ ecType ec typeInfer t = typeInfer =<< mapM typeInferComplete t typeInferComplete tf = - TypedTerm <$> liftTCM scTermF tf <*> typeInfer tf + TypedTerm <$> liftTCM scTermF tf <*> withErrorTermF tf (typeInfer tf) -- Type inference for FlatTermF Term dispatches to that for FlatTermF TypedTerm, -- with special cases for primitives and constants to avoid re-type-checking @@ -421,7 +428,8 @@ instance TypeInfer (FlatTermF Term) where typeInfer (ExtCns ec) = return $ ecType ec typeInfer t = typeInfer =<< mapM typeInferComplete t typeInferComplete ftf = - TypedTerm <$> liftTCM scFlatTermF ftf <*> typeInfer ftf + TypedTerm <$> liftTCM scFlatTermF ftf + <*> withErrorTermF (FTermF ftf) (typeInfer ftf) -- Type inference for TermF TypedTerm is the main workhorse. Intuitively, this @@ -464,7 +472,8 @@ instance TypeInfer (TermF TypedTerm) where return req_tp typeInferComplete tf = - TypedTerm <$> liftTCM scTermF (fmap typedVal tf) <*> typeInfer tf + TypedTerm <$> liftTCM scTermF (fmap typedVal tf) + <*> withErrorTypedTermF tf (typeInfer tf) -- Type inference for FlatTermF TypedTerm is the main workhorse for flat @@ -546,7 +555,8 @@ instance TypeInfer (FlatTermF TypedTerm) where typeCheckWHNF $ typedVal $ ecType ec typeInferComplete ftf = - TypedTerm <$> liftTCM scFlatTermF (fmap typedVal ftf) <*> typeInfer ftf + TypedTerm <$> liftTCM scFlatTermF (fmap typedVal ftf) + <*> withErrorTypedTermF (FTermF ftf) (typeInfer ftf) -- | Check that @fun_tp=Pi x a b@ and that @arg@ has type @a@, and return the -- result of substituting @arg@ for @x@ in the result type @b@, i.e.,