Skip to content

Commit

Permalink
Define tIsNominal and use it (#1733)
Browse files Browse the repository at this point in the history
This defines a `tIsNominal :: Type -> Maybe (NominalType, [Type])` function.
There is one spot in `Cryptol.TypeCheck.Infer` where this can more neatly
replace a manual pattern match on `TNominal`, so I went ahead and did this as
well.

Fixes #1732.
  • Loading branch information
RyanGlScott authored Aug 19, 2024
1 parent 2fb70e6 commit cc3b3fb
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 5 deletions.
7 changes: 2 additions & 5 deletions src/Cryptol/TypeCheck/Infer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -739,11 +739,8 @@ expectRec fs tGoal@(WithSource ty src rng) =
-- an enum, throwing an error if this is not the case.
expectEnum :: Type -> InferM [EnumCon]
expectEnum ty =
case ty of
TUser _ _ ty' ->
expectEnum ty'

TNominal nt _
case tIsNominal ty of
Just (nt, _)
| Enum ecs <- ntDef nt
-> pure ecs

Expand Down
8 changes: 8 additions & 0 deletions src/Cryptol/TypeCheck/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -599,6 +599,14 @@ tIsRec ty = case tNoUser ty of
TRec fs -> Just fs
_ -> Nothing

-- | If the supplied 'Type' is a 'TNominal' type, then return @'Just' (nt, ts)@,
-- where @nt@ and @ts@ are the underlying 'NominalType' and 'Type' arguments.
-- Otherwise, return 'Nothing'.
tIsNominal :: Type -> Maybe (NominalType, [Type])
tIsNominal ty = case tNoUser ty of
TNominal nm ts -> Just (nm, ts)
_ -> Nothing

tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
tIsBinFun f ty = case tNoUser ty of
TCon (TF g) [a,b] | f == g -> Just (a,b)
Expand Down

0 comments on commit cc3b3fb

Please sign in to comment.