From ebf7e5b0dce9e8e2fdd1558a5a24e5ecfecbf40e Mon Sep 17 00:00:00 2001 From: Erik Post Date: Fri, 23 Aug 2019 19:18:05 +0200 Subject: [PATCH] Rearrange code in Term.hs. #148 --- src/Language/CQL/Term.hs | 133 ++++++++++++++++++++------------------- 1 file changed, 67 insertions(+), 66 deletions(-) diff --git a/src/Language/CQL/Term.hs b/src/Language/CQL/Term.hs index 4e53d7f..3369cc0 100644 --- a/src/Language/CQL/Term.hs +++ b/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,41 +78,33 @@ 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 - +deriving instance TyMap Eq '[var, sym, fk, att, gen, sk] => Eq (Term var ty sym en fk att gen sk) -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 +deriving instance TyMap Ord '[var, ty, sym, en, fk, att, gen, sk] => Ord (Term var ty sym en fk att gen sk) -show' :: Show a => a -> String -show' = dropQuotes . show +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 -deriving instance TyMap Ord '[var, ty, sym, en, fk, att, gen, sk] => Ord (Term var ty sym en fk att gen sk) +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 (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 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 @@ -128,6 +112,9 @@ instance (Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk) 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 +195,7 @@ hasTypeType'' t = case t of Fk _ _ -> False ---------------------------------------------------------------------------------------------------------- --- Substitution and simplification of theories +-- Substitution and simplification on terms -- | Experimental subst2 @@ -268,6 +255,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 +389,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) ++ ")"