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

…a, a). #148
statebox · Aug 23, 2019 · ffb6ef1 · ffb6ef1
1 parent cad5118
commit ffb6ef1
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)