Skip to content

Commit

Permalink
🔥 aeq.
Browse files Browse the repository at this point in the history
  • Loading branch information
robrix committed Oct 20, 2020
1 parent 3cade2f commit 279129a
Showing 1 changed file with 0 additions and 18 deletions.
18 changes: 0 additions & 18 deletions src/Facet/Surface.hs
Expand Up @@ -12,7 +12,6 @@ module Facet.Surface
, Type(..)
, unForAll
, unTApp
, aeq
-- * Declarations
, Decl(..)
, DDecl(..)
Expand All @@ -24,11 +23,8 @@ module Facet.Surface
, Import(..)
) where

import Control.Applicative (liftA2)
import Control.Effect.Empty
import Data.Function (on)
import Data.List.NonEmpty (NonEmpty)
import Data.Monoid (First(..))
import Facet.Name
import Facet.Syntax
import Text.Parser.Position
Expand Down Expand Up @@ -89,20 +85,6 @@ unTApp :: Has Empty sig m => Type -> m (Spanned Type, Spanned Type)
unTApp = \case{ f :$$ a -> pure (f, a) ; _ -> empty }


aeq :: Type -> Type -> Bool
aeq t1 t2 = case (t1, t2) of
(TFree n1, TFree n2) -> n1 == n2
(TBound n1, TBound n2) -> n1 == n2
(Type, Type) -> True
((n1 ::: t1) :=> b1, (n2 ::: t2) :=> b2) -> n1 == n2 && aeq' t1 t2 && aeq' b1 b2
(f1 :$$ a1, f2 :$$ a2) -> aeq' f1 f2 && aeq' a1 a2
(a1 :-> b1, a2 :-> b2) -> aeq' a1 a2 && aeq' b1 b2
_ -> False
where
aeq' = fmap and . (liftA2 aeq `on` extract)
extract = getFirst . foldMap (First . Just)


-- Declarations

data Decl
Expand Down

0 comments on commit 279129a

Please sign in to comment.