From 627d5aa269907134be01968fb2e5a7b625483f1e Mon Sep 17 00:00:00 2001 From: "Iavor S. Diatchki" Date: Thu, 15 Jun 2017 16:50:18 -0700 Subject: [PATCH] Some code that is useful for tracing the simplifier when debugging. --- src/Cryptol/TypeCheck/SimpleSolver.hs | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/Cryptol/TypeCheck/SimpleSolver.hs b/src/Cryptol/TypeCheck/SimpleSolver.hs index eb6520ac..c9d817db 100644 --- a/src/Cryptol/TypeCheck/SimpleSolver.hs +++ b/src/Cryptol/TypeCheck/SimpleSolver.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE PatternGuards, Trustworthy #-} module Cryptol.TypeCheck.SimpleSolver ( simplify , simplifyStep) where import Cryptol.TypeCheck.Type hiding @@ -9,12 +9,25 @@ import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType) import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq) import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst) +import Cryptol.Utils.Debug(ppTrace) +import Cryptol.TypeCheck.PP + simplify :: Ctxt -> Prop -> Prop simplify ctxt p = case simplifyStep ctxt p of Unsolvable e -> pError e - Unsolved -> p - SolvedIf ps -> pAnd (map (simplify ctxt) ps) + Unsolved -> dbg msg p + where msg = text "unsolved:" <+> pp p + SolvedIf ps -> dbg msg $ pAnd (map (simplify ctxt) ps) + where msg = case ps of + [] -> text "solved:" <+> pp p + _ -> pp p <+> text "~~~>" <+> + vcat (punctuate comma (map pp ps)) + + where + dbg msg x + | False = ppTrace msg x + | otherwise = x simplifyStep :: Ctxt -> Prop -> Solved