GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 04:44:39 +03:00
Code Issues Projects Releases Wiki Activity

Some code that is useful for tracing the simplifier when debugging.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2017-06-15 16:50:18 -07:00
parent 7a42065a94
commit 627d5aa269
1 changed files with 16 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/Cryptol/TypeCheck/SimpleSolver.hs
View File

@ -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