Skip to content

Commit

Permalink
Reimplement EQ as a specialisation of underlying newtype EQF a = EQ (…
Browse files Browse the repository at this point in the history
…a, a). #148
  • Loading branch information
epost committed Aug 23, 2019
1 parent cad5118 commit ffb6ef1
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 9 deletions.
2 changes: 1 addition & 1 deletion src/Language/CQL/Collage.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion src/Language/CQL/Instance/Algebra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Language/CQL/Morphism.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
17 changes: 11 additions & 6 deletions src/Language/CQL/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit ffb6ef1

Please sign in to comment.