Rearrange code in Term.hs. #148

src/Language/CQL/Term.hs

@@ -49,14 +49,6 @@ import Data.Void
 import Language.CQL.Common
 import Prelude hiding (EQ)
 
-data RawTerm = RawApp String [RawTerm]
- deriving Eq
-
-instance Show RawTerm where
- show (RawApp sym az) = show sym ++ "(" ++ (intercalate "," . fmap show $ az) ++ ")"
-
---------------------------------------------------------------------------------------------
--- Terms
 
 data Term var ty sym en fk att gen sk
  -- | Variable.
@@ -86,48 +78,40 @@ data Head ty sym en fk att gen sk
  | HSk sk
  deriving (Eq, Ord)
 
-instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] =>
- NFData (Term var ty sym en fk att gen sk) where
- rnf x = case x of
- Var v -> rnf v
- Sym f a -> let _ = rnf f in rnf a
- Fk f a -> let _ = rnf f in rnf a
- Att f a -> let _ = rnf f in rnf a
- Gen a -> rnf a
- Sk a -> rnf a
-
-instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] =>
- NFData (EQ var ty sym en fk att gen sk) where
- rnf (EQ (x, y)) = deepseq x $ rnf y
-
-
-instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] =>
- Show (Term var ty sym en fk att gen sk)
- where
- show x = case x of
- Var v -> show' v
- Gen g -> show' g
- Sk s -> show' s
- Fk fk a -> show' a ++ "." ++ show' fk
- Att att a -> show' a ++ "." ++ show' att
- Sym sym [] -> show' sym
- Sym sym az -> show' sym ++ "(" ++ (intercalate "," . fmap show' $ az) ++ ")"
- where
-
-show' :: Show a => a -> String
-show' = dropQuotes . show
+deriving instance TyMap Eq '[var, sym, fk, att, gen, sk] => Eq (Term var ty sym en fk att gen sk)
 
 deriving instance TyMap Ord '[var, ty, sym, en, fk, att, gen, sk] => Ord (Term var ty sym en fk att gen sk)
 
-instance (Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk)
- => Show (Head ty sym en fk att gen sk) where
+instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] => NFData (Term var ty sym en fk att gen sk) where
+ rnf x = case x of
+ Var v -> rnf v
+ Sym f a -> let _ = rnf f in rnf a
+ Fk f a -> let _ = rnf f in rnf a
+ Att f a -> let _ = rnf f in rnf a
+ Gen a -> rnf a
+ Sk a -> rnf a
+
+instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] => Show (Term var ty sym en fk att gen sk) where
+ show x = case x of
+ Var v -> show' v
+ Gen g -> show' g
+ Sk s -> show' s
+ Fk fk a -> show' a ++ "." ++ show' fk
+ Att att a -> show' a ++ "." ++ show' att
+ Sym sym [] -> show' sym
+ Sym sym az -> show' sym ++ "(" ++ (intercalate "," . fmap show' $ az) ++ ")"
+
+instance TyMap Show '[ty, sym, en, fk, att, gen, sk] => Show (Head ty sym en fk att gen sk) where
  show x = case x of
  HSym sym -> show' sym
  HFk fk -> show' fk
  HAtt att -> show' att
  HGen gen -> show' gen
  HSk sk -> show' sk
 
+show' :: Show a => a -> String
+show' = dropQuotes . show
+
 -- | Maps functions through a term.
 mapTerm
  :: (var -> var')
@@ -208,7 +192,7 @@ hasTypeType'' t = case t of
  Fk _ _ -> False
 
 ----------------------------------------------------------------------------------------------------------
--- Substitution and simplification of theories
+-- Substitution and simplification on terms
 
 -- | Experimental
 subst2
@@ -268,6 +252,41 @@ occurs h x = case x of
  Att h' a -> h == HAtt h' || occurs h a
  Sym h' as -> h == HSym h' || any (occurs h) as
 
+
+--------------------------------------------------------------------------------------------------------------------
+-- Equality, especially on Terms
+
+-- | 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)
+
+newtype EQF a = EQ (a, a)
+
+instance Functor EQF where
+ fmap f (EQ (l, r)) = EQ (f l, f r)
+
+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)
+
+instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] => NFData (EQ var ty sym en fk att gen sk) where
+ rnf (EQ (x, y)) = deepseq x $ rnf y
+
+hasTypeType' :: EQ Void ty sym en fk att gen sk -> Bool
+hasTypeType' (EQ (lhs, _)) = hasTypeType lhs
+
+
+--------------------------------------------------------------------------------------------------------------------
+-- Theories
+
+type Theory var ty sym en fk att gen sk = Set (Ctx var (ty+en), EQ var ty sym en fk att gen sk)
+
+-- TODO wrap Map class to throw an error (or do something less ad hoc) if a key is ever inserted twice
+type Ctx k v = Map k v
+
 -- | If there is one, finds an equation of the form @empty |- gen/sk = term@,
 -- where @gen@ does not occur in @term@.
 findSimplifiableEq
@@ -367,31 +386,10 @@ instance Up x (x + y) where
 instance Up y (x + y) where
  upgr = Right
 
---------------------------------------------------------------------------------------------------------------------
--- Theories
-
-type Theory var ty sym en fk att gen sk = Set (Ctx var (ty+en), EQ var ty sym en fk att gen sk)
-
--- 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
-
--- | 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)
+--------------------------------------------------------------------------------
 
-newtype EQF a = EQ (a, a)
-
-instance Functor EQF where
- fmap f (EQ (l, r)) = EQ (f l, f r)
-
-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)
+data RawTerm = RawApp String [RawTerm]
+ deriving Eq
 
-hasTypeType' :: EQ Void ty sym en fk att gen sk -> Bool
-hasTypeType' (EQ (lhs, _)) = hasTypeType lhs
+instance Show RawTerm where
+ show (RawApp sym az) = show sym ++ "(" ++ (intercalate "," . fmap show $ az) ++ ")"