GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-19 09:57:53 +03:00
Code Issues Projects Releases Wiki Activity

Add some more simplification on user defined signatures.

Browse Source 
This is not great, but since we do it, we should do it more consistently.
Avoids a panic in the bench mark suite (more generally, when users write
trivial things in their type signatures, eg. see `pad` in SHA512)
This commit is contained in:
Iavor Diatchki 2018-07-13 11:00:21 -07:00
parent 021e71bd82
commit 6f67924894
2 changed files with 16 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Cryptol/TypeCheck/Kind.hs
View File

@ -25,6 +25,7 @@ import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Monad hiding (withTParams)
import Cryptol.TypeCheck.SimpType(tRebuild)
import Cryptol.TypeCheck.SimpleSolver(simplify)
import Cryptol.TypeCheck.Solve (simplifyAllConstraints
,wfTypeFunction,wfTC)
import Cryptol.Utils.Panic (panic)
@ -47,7 +48,12 @@ checkSchema withWild (P.Forall xs ps t mb) =
do ps1 <- mapM checkProp ps
t1 <- doCheckType t (Just KType)
return (ps1,t1)
return ( Forall xs1 (map tRebuild ps1) (tRebuild t1)
-- XXX: We probably shouldn't do this, as we are changing what the
-- user is doing. We do it so that things are in a propal normal form,
-- but we should probably figure out another time to do this.
let newPs = concatMap pSplitAnd $ map (simplify Map.empty)
$ map tRebuild ps1
return ( Forall xs1 newPs (tRebuild t1)
, [ g { goal = tRebuild (goal g) } | g <- gs ]
)

11
src/Cryptol/TypeCheck/Subst.hs
View File

@ -247,9 +247,16 @@ instance TVars Expr where
EProofAbs p e -> EProofAbs hmm (go e)
where hmm = case pSplitAnd (apSubst su p) of
[p1] -> p1
_ -> panic "apSubst@EProofAbs"
res -> panic "apSubst@EProofAbs"
[ "Predicate split or disappeared after"
, "we applied a substitution." ]
, "we applied a substitution."
, "Predicate:"
, show (pp p)
, "Became:"
, show (map pp res)
, "subst:"
, show (pp su)
]
EProofApp e -> EProofApp (go e)