GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-27 12:52:52 +03:00
Code Issues Projects Releases Wiki Activity

Continue exporting width equality proofs comparison/equality.

Browse Source
This commit is contained in:
Joe Hendrix 2019-05-30 22:54:49 -07:00
parent 78927cce64
commit 5c097b45b7
No known key found for this signature in database
GPG Key ID: 8DFA5FF784098C4F
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
base/src/Data/Macaw/CFG/App.hs
View File

@ -21,6 +21,8 @@ module Data.Macaw.CFG.App
, ppAppA
-- * Casting proof objects.
, WidthEqProof(..)
, widthEqProofEq
, widthEqProofCompare
, widthEqTarget
) where
@ -105,7 +107,8 @@ widthEqTarget (WidthEqTrans _ y) = widthEqTarget y
-- Force app to be in template-haskell context.
$(pure [])
-- | We treat proofs as equal if the types are the same.
-- | Compare two proofs, and return truei if the input/output types
-- are the same.
widthEqProofEq :: WidthEqProof xi xo
-> WidthEqProof yi yo
-> Maybe (WidthEqProof xi xo :~: WidthEqProof yi yo)
@ -114,7 +117,7 @@ widthEqProofEq p q = do
Refl <- testEquality (widthEqTarget p) (widthEqTarget q)
pure Refl
-- | We treat proofs as equal if the types are the same.
-- | Compare proofs based on ordering of source and target.
widthEqProofCompare :: WidthEqProof xi xo
-> WidthEqProof yi yo
-> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)