Reimplement EQ as a specialisation of underlying newtype EQF a = EQ (…

…a, a). #148
statebox · Jan 21, 2020 · f5b8472 · f5b8472
1 parent 8c543f2
commit f5b8472
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 9 deletions.
diff --git a/src/Language/CQL/Collage.hs b/src/Language/CQL/Collage.hs
@@ -46,7 +46,7 @@ import           Data.Map.Strict       as Map hiding (foldr, size)
 import           Data.Set              as Set hiding (foldr, size)
 import           Data.Void
 import           Language.CQL.Common
-import           Language.CQL.Term     (Ctx, EQ(..), Head(..), Term(..), occsTerm, upp)
+import           Language.CQL.Term     (Ctx, EQ, EQF(..), Head(..), Term(..), occsTerm, upp)
 import qualified Language.CQL.Term     as T (simplifyTheory)
 import           Prelude               hiding (EQ)
 

diff --git a/src/Language/CQL/Instance/Algebra.hs b/src/Language/CQL/Instance/Algebra.hs
@@ -49,7 +49,7 @@ import qualified Data.Set              as Set
 import           Data.Void
 import           Language.CQL.Common   (intercalate, mapl, section, MultiTyMap, TyMap, type (+))
 import           Language.CQL.Schema   as Schema
-import           Language.CQL.Term     (EQ(..), Head(HSk), Term(..), subst, upp, replaceRepeatedly, simplifyTheory)
+import           Language.CQL.Term     (EQ, Head(HSk), Term(..), subst, upp, replaceRepeatedly, simplifyTheory)
 import           Language.CQL.Typeside as Typeside
 import           Prelude               hiding (EQ)
 import qualified Text.Tabular          as T

diff --git a/src/Language/CQL/Morphism.hs b/src/Language/CQL/Morphism.hs
@@ -46,7 +46,7 @@ import           Data.Set              as Set hiding (foldr, size)
 import           Data.Void
 import           Language.CQL.Collage  (Collage(..))
 import           Language.CQL.Common
-import           Language.CQL.Term     (Ctx, Term(..), EQ(..), subst, upp)
+import           Language.CQL.Term     (Ctx, Term(..), EQ, EQF(..), subst, upp)
 import           Prelude               hiding (EQ)
 
 -- | A morphism between 'Collage's.

diff --git a/src/Language/CQL/Term.hs b/src/Language/CQL/Term.hs
@@ -382,13 +382,18 @@ type Theory var ty sym en fk att gen sk = Set (Ctx var (ty+en), EQ var ty sym en
 -- TODO wrap Map class to throw an error (or do something less ad hoc) if a key is ever put twice
 type Ctx k v = Map k v
 
--- Our own pair type for pretty printing purposes
--- | This type indicates that the two terms are equal.
-newtype EQ var ty sym en fk att gen sk
-  = EQ (Term var ty sym en fk att gen sk, Term var ty sym en fk att gen sk) deriving (Ord, Eq)
+-- | A value of this type means the lhs and rhs are equal.
+--   One reason for its existence is to allow pretty-printing.
+type EQ var ty sym en fk att gen sk = EQF (Term var ty sym en fk att gen sk)
 
-instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] => Show (EQ var ty sym en fk att gen sk) where
-  show (EQ (lhs,rhs)) = show lhs ++ " = " ++ show rhs
+newtype EQF a = EQ (a, a)
+
+instance (Show a) => Show (EQF a) where
+  show (EQ (lhs, rhs)) = show lhs ++ " = " ++ show rhs
+
+deriving instance (Ord a) => Ord (EQF a)
+
+deriving instance (Eq a) => Eq (EQF a)
 
 deriving instance TyMap Eq '[var, sym, fk, att, gen, sk] => Eq (Term var ty sym en fk att gen sk)