Skip to content

Commit

Permalink
Code reads better with do-notation
Browse files Browse the repository at this point in the history
  • Loading branch information
yairchu committed Jun 4, 2023
1 parent 1df00b9 commit 01abdc6
Show file tree
Hide file tree
Showing 4 changed files with 62 additions and 60 deletions.
66 changes: 33 additions & 33 deletions src/Hyper/Class/Unify.hs
Original file line number Diff line number Diff line change
Expand Up @@ -153,39 +153,39 @@ applyBindings ::
UVarOf m # t ->
m (Pure # t)
applyBindings v0 =
semiPruneLookup v0
>>= \(v1, x) ->
let result r = r <$ bindVar binding v1 (UResolved r)
quantify c =
newQuantifiedVariable c
<&> (_Pure . quantifiedVar #)
>>= result
in case x of
UResolving t -> occursError v1 t
UResolved t -> pure t
UUnbound c -> quantify c
USkolem c -> quantify c
UTerm b ->
do
(r, anyChild) <-
htraverse
( Proxy @(Unify m) #>
\c ->
do
get >>= lift . (`unless` bindVar binding v1 (UResolving b))
put True
applyBindings c & lift
)
(b ^. uBody)
& (`runStateT` False)
\\ unifyRecursive (Proxy @m) (Proxy @t)
_Pure # r & if anyChild then result else pure
UToVar{} -> error "lookup not expected to result in var"
UConverted{} -> error "conversion state not expected in applyBindings"
UInstantiated{} ->
-- This can happen in alphaEq,
-- where UInstantiated marks that var from one side matches var in the other.
quantify mempty
do
(v1, x) <- semiPruneLookup v0
let result r = r <$ bindVar binding v1 (UResolved r)
let quantify c =
newQuantifiedVariable c
<&> (_Pure . quantifiedVar #)
>>= result
case x of
UResolving t -> occursError v1 t
UResolved t -> pure t
UUnbound c -> quantify c
USkolem c -> quantify c
UTerm b ->
do
(r, anyChild) <-
htraverse
( Proxy @(Unify m) #>
\c ->
do
get >>= lift . (`unless` bindVar binding v1 (UResolving b))
put True
applyBindings c & lift
)
(b ^. uBody)
& (`runStateT` False)
\\ unifyRecursive (Proxy @m) (Proxy @t)
_Pure # r & if anyChild then result else pure
UToVar{} -> error "lookup not expected to result in var"
UConverted{} -> error "conversion state not expected in applyBindings"
UInstantiated{} ->
-- This can happen in alphaEq,
-- where UInstantiated marks that var from one side matches var in the other.
quantify mempty

-- | Format and throw an occurs check error
occursError ::
Expand Down
46 changes: 23 additions & 23 deletions src/Hyper/Unify/Occurs.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,26 +20,26 @@ occursCheck ::
UVarOf m # t ->
m ()
occursCheck v0 =
semiPruneLookup v0
>>= \(v1, x) ->
case x of
UResolving t -> occursError v1 t
UResolved{} -> pure ()
UUnbound{} -> pure ()
USkolem{} -> pure ()
UTerm b ->
htraverse_
( Proxy @(Unify m) #>
\c ->
do
get >>= lift . (`unless` bindVar binding v1 (UResolving b))
put True
occursCheck c & lift
)
(b ^. uBody)
& (`execStateT` False)
>>= (`when` bindVar binding v1 (UTerm b))
\\ unifyRecursive (Proxy @m) (Proxy @t)
UToVar{} -> error "lookup not expected to result in var (in occursCheck)"
UConverted{} -> error "conversion state not expected in occursCheck"
UInstantiated{} -> error "occursCheck during instantiation"
do
(v1, x) <- semiPruneLookup v0
case x of
UResolving t -> occursError v1 t
UResolved{} -> pure ()
UUnbound{} -> pure ()
USkolem{} -> pure ()
UTerm b ->
htraverse_
( Proxy @(Unify m) #>
\c ->
do
get >>= lift . (`unless` bindVar binding v1 (UResolving b))
put True
occursCheck c & lift
)
(b ^. uBody)
& (`execStateT` False)
>>= (`when` bindVar binding v1 (UTerm b))
\\ unifyRecursive (Proxy @m) (Proxy @t)
UToVar{} -> error "lookup not expected to result in var (in occursCheck)"
UConverted{} -> error "conversion state not expected in occursCheck"
UInstantiated{} -> error "occursCheck during instantiation"
5 changes: 3 additions & 2 deletions test/LangA.hs
Original file line number Diff line number Diff line change
Expand Up @@ -100,8 +100,9 @@ instance (DeBruijnIndex h, TermInfer1Deps env m) => Infer m (LangA h) where
inferBody (ALit x) = newTerm TInt <&> MkANode <&> (ALit x,)
inferBody (AVar x) = inferBody x <&> Lens._1 %~ AVar
inferBody (ALam x) =
inferBody x
>>= \(b, t) -> TFun t & newTerm <&> (ALam b,) . MkANode
do
(b, t) <- inferBody x
TFun t & newTerm <&> (ALam b,) . MkANode
inferBody (AApp x) = inferBody x <&> Lens._1 %~ AApp
inferBody (ATypeSig x) = inferBody x <&> Lens._1 %~ ATypeSig

Expand Down
5 changes: 3 additions & 2 deletions test/LangB.hs
Original file line number Diff line number Diff line change
Expand Up @@ -110,8 +110,9 @@ instance
inferBody (BLet x) = inferBody x <&> Lens._1 %~ BLet
inferBody (BLit x) = newTerm TInt <&> (BLit x,) . MkANode
inferBody (BToNom x) =
inferBody x
>>= \(b, t) -> TNom t & newTerm <&> (BToNom b,) . MkANode
do
(b, t) <- inferBody x
TNom t & newTerm <&> (BToNom b,) . MkANode
inferBody (BRecExtend (RowExtend h v r)) =
do
InferredChild vI vT <- inferChild v
Expand Down

0 comments on commit 01abdc6

Please sign in to comment.