Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Commit

Permalink
Merge pull request #51 from GaloisInc/asTupleType
Browse files Browse the repository at this point in the history
Fix recognizers for tuple values and types.
  • Loading branch information
brianhuffman authored Apr 10, 2020
2 parents d78bf6e + d56ee2a commit 562839d
Showing 1 changed file with 24 additions and 12 deletions.
36 changes: 24 additions & 12 deletions src/Verifier/SAW/Recognizer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -174,21 +174,33 @@ asPairSelector t = do
PairRight x -> return (x, True)
_ -> Nothing

destTupleType :: Term -> [Term]
destTupleType t =
case unwrapTermF t of
FTermF (PairType x y) -> x : destTupleType y
_ -> [t]

destTupleValue :: Term -> [Term]
destTupleValue t =
case unwrapTermF t of
FTermF (PairValue x y) -> x : destTupleType y
_ -> [t]

asTupleType :: Recognizer Term [Term]
asTupleType t = do
ftf <- asFTermF t
case ftf of
UnitType -> return []
PairType x y -> do xs <- asTupleType y; return (x : xs)
_ -> Nothing
asTupleType t =
do ftf <- asFTermF t
case ftf of
UnitType -> Just []
PairType x y -> Just (x : destTupleType y)
_ -> Nothing

asTupleValue :: Recognizer Term [Term]
asTupleValue t = do
ftf <- asFTermF t
case ftf of
UnitValue -> return []
PairValue x y -> do xs <- asTupleValue y; return (x : xs)
_ -> Nothing
asTupleValue t =
do ftf <- asFTermF t
case ftf of
UnitValue -> Just []
PairValue x y -> Just (x : destTupleValue y)
_ -> Nothing

asTupleSelector :: Recognizer Term (Term, Int)
asTupleSelector t = do
Expand Down

0 comments on commit 562839d

Please sign in to comment.