Skip to content

Commit

Permalink
remove useless constraints #122
Browse files Browse the repository at this point in the history
  • Loading branch information
marcosh committed Nov 20, 2018
1 parent 72557df commit 8342fea
Show file tree
Hide file tree
Showing 14 changed files with 127 additions and 113 deletions.
17 changes: 10 additions & 7 deletions package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -34,14 +34,17 @@ library:
source-dirs: src

ghc-options:
- -Wunused-binds
- -Wunused-foralls
- -Wunused-imports
- -Wincomplete-patterns
- -Wdodgy-exports
- -Wdodgy-imports
- -Wunbanged-strict-patterns
- -Weverything
- -Werror
- -Wno-implicit-prelude
- -Wno-missing-export-lists
- -Wno-missing-import-lists
- -Wno-safe
- -Wno-missing-local-signatures
- -Wno-unsafe
- -Wno-monomorphism-restriction
- -Wno-unused-type-patterns
- -Wno-name-shadowing

executables:
aql-exe:
Expand Down
3 changes: 1 addition & 2 deletions src/Language/AQL.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ import Control.Concurrent
import Control.Exception

-- works
timeout' :: (Show x, NFData x) => Integer -> Err x -> Err x
timeout' :: (NFData x) => Integer -> Err x -> Err x
timeout' i p = unsafePerformIO $ do
m <- newEmptyMVar
computer <- forkIO $ f m p
Expand Down Expand Up @@ -452,7 +452,6 @@ evalInstance prog env (InstanceSigma f' i o) = do
o' <- toOptions (other env) o
r <- evalSigmaInst f'' (fromJust $ ((cast i') :: Maybe (Instance var ty sym en fk att gen sk x y))) o'
return $ InstanceEx r

evalInstance prog env (InstanceDelta f' i o) = do
(MappingEx (f'' :: Mapping var ty sym en fk att en' fk' att')) <- evalMapping prog env f'
(InstanceEx (i' :: Instance var'' ty'' sym'' en'' fk'' att'' gen sk x y)) <- evalInstance prog env i
Expand Down
51 changes: 25 additions & 26 deletions src/Language/Instance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@

module Language.Instance where

import Control.DeepSeq
import qualified Data.Foldable as Foldable
import Data.List hiding (intercalate)
import Data.Map.Strict (Map, unionWith, (!))
Expand All @@ -37,7 +38,6 @@ import Language.Typeside as Typeside
import Prelude hiding (EQ)
import qualified Text.Tabular as T
import qualified Text.Tabular.AsciiArt as Ascii
import Control.DeepSeq



Expand Down Expand Up @@ -108,7 +108,7 @@ down1 _ = error "Anomaly: please report. Function name: down1."

-- | Checks that an instance satisfies its schema.
checkSatisfaction
:: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk, x, y])
:: (Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk, Ord x)
=> Instance var ty sym en fk att gen sk x y
-> Err ()
checkSatisfaction (Instance sch pres' dp' alg) = do
Expand Down Expand Up @@ -160,7 +160,7 @@ aSk :: Algebra var ty sym en fk att gen sk x y -> sk -> Term Void ty sym Void Vo
aSk alg g = nf'' alg $ Sk g


instance (NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData gen, NFData sk, NFData x, NFData y)
instance (NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData x, NFData y)
=> NFData (Algebra var ty sym en fk att gen sk x y)
where
rnf (Algebra s0 e0 nf0 repr0 ty0 nf1 repr1 eqs1) = deepseq s0 $ f e0 $ deepseq nf0 $ deepseq repr0
Expand Down Expand Up @@ -198,7 +198,7 @@ instance (NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, N
=> NFData (Instance var ty sym en fk att gen sk x y) where
rnf (Instance s0 p0 dp0 a0) = deepseq s0 $ deepseq p0 $ deepseq dp0 $ rnf a0

instance (NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData gen, NFData sk)
instance (NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData gen, NFData sk)
=> NFData (Presentation var ty sym en fk att gen sk) where
rnf (Presentation g s e) = deepseq g $ deepseq s $ rnf e

Expand All @@ -211,7 +211,7 @@ data InstanceEx :: * where

-- | Converts an instance to a presentation.
instToCol
:: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk])
:: (ShowOrdN '[var, ty, sym, en, fk, att], Ord gen, Ord sk)
=> Schema var ty sym en fk att
-> Presentation var ty sym en fk att gen sk
-> Collage (()+var) ty sym en fk att gen sk
Expand All @@ -225,7 +225,7 @@ instToCol sch (Presentation gens' sks' eqs') =


-- | Converts an instance into a presentation: adds one equation per fact in the algebra.
algebraToPresentation :: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk], Ord y, Ord x)
algebraToPresentation :: (Ord ty, Ord sym, Ord en, Ord fk, Ord att, Ord y, Ord x)
=> Algebra var ty sym en fk att gen sk x y
-> Presentation var ty sym en fk att x y
algebraToPresentation (alg@(Algebra sch en' _ _ ty' _ _ _)) = Presentation gens' sks' eqs'
Expand Down Expand Up @@ -352,9 +352,9 @@ instance (Show en, Show fk, Show att, Show gen, Show sk) => Show (TalgGen en fk

deriving instance (Ord en, Ord fk, Ord att, Ord gen, Ord sk) => Ord (TalgGen en fk att gen sk)

deriving instance (Eq en, Eq fk, Eq att, Eq gen, Eq sk) => Eq (TalgGen en fk att gen sk)
deriving instance (Eq fk, Eq att, Eq gen, Eq sk) => Eq (TalgGen en fk att gen sk)

assembleGens :: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk], Eq en)
assembleGens :: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk])
=> Collage var ty sym en fk att gen sk -> [Carrier en fk gen] -> Map en (Set (Carrier en fk gen))
assembleGens col [] = Map.fromList $ Prelude.map (\x -> (x,Set.empty)) $ Set.toList $ cens col
assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
Expand All @@ -363,7 +363,7 @@ assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
s = fromJust $ Map.lookup t m

close
:: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk], Eq en)
:: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk])
=> Collage var ty sym en fk att gen sk
-> (EQ var ty sym en fk att gen sk -> Bool)
-> [Term Void Void Void en fk Void gen Void]
Expand All @@ -385,7 +385,7 @@ dedup :: (EQ var ty sym en fk att gen sk -> Bool)
-> [Term Void Void Void en fk Void gen Void]
dedup dp' = nubBy (\x y -> dp' (EQ (upp x, upp y)))

close1 :: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk], Eq en)
close1 :: (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk])
=> Collage var ty sym en fk att gen sk -> (EQ var ty sym en fk att gen sk -> Bool) -> Term Void Void Void en fk Void gen Void -> [ (Term Void Void Void en fk Void gen Void) ]
close1 col _ e = e:(fmap (\(x,_) -> Fk x e) l)
where t = typeOf col e
Expand Down Expand Up @@ -422,14 +422,14 @@ instance Deps InstanceExp where

getOptionsInstance :: InstanceExp -> [(String, String)]
getOptionsInstance x = case x of
InstanceVar _ -> []
InstanceInitial _ -> []
InstanceDelta _ _ o -> o
InstanceSigma _ _ o -> o
InstancePi _ _ -> undefined
InstanceEval _ _ -> undefined
InstanceCoEval _ _ -> undefined
InstanceRaw (InstExpRaw' _ _ _ o _) -> o
InstanceVar _ -> []
InstanceInitial _ -> []
InstanceDelta _ _ o -> o
InstanceSigma _ _ o -> o
InstancePi _ _ -> undefined
InstanceEval _ _ -> undefined
InstanceCoEval _ _ -> undefined
InstanceRaw (InstExpRaw' _ _ _ o _) -> o


----------------------------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -476,7 +476,7 @@ split'' ens2 tys2 ((w, ei):tl) =
else Left $ "Not an entity or type: " ++ show ei

evalInstanceRaw'
:: forall var ty sym en fk att . (ShowOrdN '[var, ty, sym, en, fk, att], Typeable ty, Typeable sym, Typeable en, Typeable fk, Typeable att)
:: forall var ty sym en fk att . (Ord ty, Ord sym, Ord en, Ord fk, Ord att, Typeable ty, Typeable sym, Typeable en, Typeable fk, Typeable att)
=> Schema var ty sym en fk att
-> InstExpRaw'
-> [Presentation var ty sym en fk att Gen Sk]
Expand Down Expand Up @@ -567,7 +567,7 @@ emptyInstance ts'' = Instance ts''
-- Functorial data migration

subs
:: (ShowOrdN '[var, ty, sym, en, fk, att, en', fk', att', gen, sk], Eq en')
:: (Ord ty, Ord sym, Ord en, Ord fk, Ord att, Ord en', Ord fk', Ord att', Ord gen, Ord sk)
=> Mapping var ty sym en fk att en' fk' att'
-> Presentation var ty sym en fk att gen sk
-> Presentation var ty sym en' fk' att' gen sk
Expand Down Expand Up @@ -606,7 +606,7 @@ changeEn' fks' atts' t = case t of
Att h _ -> absurd h

evalSigmaInst
:: (ShowOrdN '[var, ty, sym, en, fk, att, en', fk', att', gen, sk], Eq x, Eq y, Eq en')
:: (ShowOrdN '[var, ty, sym, en', fk', att', gen, sk], Ord en, Ord fk, Ord att)
=> Mapping var ty sym en fk att en' fk' att'
-> Instance var ty sym en fk att gen sk x y -> Options
-> Err (Instance var ty sym en' fk' att' gen sk (Carrier en' fk' gen) (TalgGen en' fk' att' gen sk))
Expand All @@ -624,8 +624,7 @@ mapGen _ _ = undefined

evalDeltaAlgebra
:: forall var ty sym en fk att gen sk x y en' fk' att'
. ( Show var, Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk, Show x, Show y, Show en', Show fk', Show att'
, Ord var, Ord ty, Ord sym, Ord en, Ord fk, Ord att, Ord gen, Ord sk, Ord x, Ord y, Ord en', Ord fk', Ord att')
. (Ord en, Ord fk, Ord att, Ord x)
=> Mapping var ty sym en fk att en' fk' att'
-> Instance var ty sym en' fk' att' gen sk x y
-> Algebra var ty sym en fk att (en, x) y (en, x) y
Expand All @@ -651,7 +650,7 @@ evalDeltaAlgebra (Mapping src' _ ens' fks0 atts0)


evalDeltaInst
:: forall var ty sym en fk att gen sk x y en' fk' att' . (ShowOrdN '[var, ty, sym, en, fk, att, gen, sk, x, y, en', fk', att'])
:: forall var ty sym en fk att gen sk x y en' fk' att' . (Ord ty, Ord sym, Ord en, Ord fk, Ord att, Ord x, Ord y)
=> Mapping var ty sym en fk att en' fk' att'
-> Instance var ty sym en' fk' att' gen sk x y -> Options
-> Err (Instance var ty sym en fk att (en,x) y (en,x) y)
Expand Down Expand Up @@ -699,7 +698,7 @@ instance (Show var, Show ty, Show sym, Show en, Show fk, Show att, Show gen, Sho
prettyTypeEqns = intercalate "\n" (Set.map show teqs')

prettyEntity
:: (Show var, Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk, Show x, Show y, Eq en)
:: (Show ty, Show sym, Show en, Show fk, Show att, Show x, Show y, Eq en)
=> Algebra var ty sym en fk att gen sk x y
-> en
-> String
Expand All @@ -721,7 +720,7 @@ prettyEntity alg@(Algebra sch en' _ _ _ _ _ _) es =

-- TODO unquote identifiers; stick fks and attrs in separate `Group`s?
prettyEntityTable
:: (Show var, Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk, Show x, Show y, Eq en)
:: (Show ty, Show sym, Show en, Show fk, Show att, Show x, Show y, Eq en)
=> Algebra var ty sym en fk att gen sk x y
-> en
-> String
Expand Down
16 changes: 8 additions & 8 deletions src/Language/Mapping.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
--{-# LANGUAGE DisambiguateRecordFields #-}

module Language.Mapping where
import Control.DeepSeq
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
Expand All @@ -29,7 +30,6 @@ import Language.Common
import Language.Schema as Schema
import Language.Term
import Prelude hiding (EQ)
import Control.DeepSeq

-- | Morphism of schemas.
data Mapping var ty sym en fk att en' fk' att'
Expand Down Expand Up @@ -87,15 +87,15 @@ mapToMor (Mapping src' dst' ens' fks' atts') = Morphism (schToCol src') (schToCo

-- | Checks well-typedness of underlying theory.
typecheckMapping
:: (ShowOrdN '[var, ty], ShowOrdTypeableN '[sym, en, fk, att, en', fk', att'])
:: (ShowOrdN '[var, ty, sym, en, fk, att, en', fk', att'])
=> Mapping var ty sym en fk att en' fk' att'
-> Err ()
typecheckMapping m = typeOfMor $ mapToMor m

-- | Given @F@ checks that each @S |- p = q -> T |- F p = F q@.
validateMapping
:: forall var ty sym en fk att en' fk' att'
. (ShowOrdN '[var, ty], ShowOrdTypeableN '[sym, en, fk, att, en', fk', att'])
. (ShowOrdN '[var, ty, sym, en, fk, att, en', fk', att'])
=> Mapping var ty sym en fk att en' fk' att'
-> Err ()
validateMapping (m@(Mapping src' dst' ens' _ _)) = do
Expand Down Expand Up @@ -132,9 +132,9 @@ data MappingExp where

getOptionsMapping :: MappingExp -> [(String, String)]
getOptionsMapping x = case x of
MappingVar _ -> []
MappingId _ -> []
MappingComp _ _ -> []
MappingVar _ -> []
MappingId _ -> []
MappingComp _ _ -> []
MappingRaw (MappingExpRaw' _ _ _ _ _ o _) -> o

instance Deps MappingExp where
Expand Down Expand Up @@ -186,7 +186,7 @@ data MappingExpRaw' =
} deriving (Eq, Show)

evalMappingRaw'
:: forall var ty sym en fk att en' fk' att' . (ShowOrdN '[var, ty], ShowOrdTypeableN '[sym, en, fk, att, en', fk', att'])
:: forall var ty sym en fk att en' fk' att' . (ShowOrdTypeableN '[en, en'], Typeable sym, Ord fk, Typeable fk, Ord att, Typeable att, Ord fk', Typeable fk', Ord att', Typeable att')
=> Schema var ty sym en fk att -> Schema var ty sym en' fk' att'
-> MappingExpRaw'
-> [Mapping var ty sym en fk att en' fk' att']
Expand Down Expand Up @@ -235,7 +235,7 @@ evalMappingRaw' src' dst' (MappingExpRaw' _ _ ens0 fks0 atts0 _ _) is = do
g' v _ _ (RawApp x []) | v == x = Var ()
g' v fks'' atts'' (RawApp x (a:[])) | elem' x fks'' = Fk (fromJust $ cast x) $ g' v fks'' atts'' a
g' _ _ _ _ = error "impossible"
g :: Typeable sym => String ->[fk']-> [att'] -> RawTerm -> Term () ty sym en' fk' att' Void Void
g :: String ->[fk']-> [att'] -> RawTerm -> Term () ty sym en' fk' att' Void Void
g v _ _ (RawApp x []) | v == x = Var ()
g v fks'' atts'' (RawApp x (a:[])) | elem' x fks'' = Fk (fromJust $ cast x) $ g' v fks'' atts'' a
g v fks'' atts'' (RawApp x (a:[])) | elem' x atts'' = Att (fromJust $ cast x) $ g' v fks'' atts'' a
Expand Down
6 changes: 3 additions & 3 deletions src/Language/Options.hs
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
{-# LANGUAGE EmptyDataDeriving #-}

module Language.Options where
import Data.Void
import Language.Common
import Text.Read
import Data.Void

data Options = Options {
iOps :: IntOption -> Integer,
Expand Down Expand Up @@ -68,8 +68,8 @@ toBoolOption (k,v) = case matches of
boolDef :: BoolOption -> Bool
boolDef o = case o of
Program_Allow_Nontermination_Unsafe -> False
Allow_Empty_Sorts_Unsafe -> False
Program_Allow_Nonconfluence_Unsafe -> False
Allow_Empty_Sorts_Unsafe -> False
Program_Allow_Nonconfluence_Unsafe -> False

-- | Default values for Integer options.
intDef :: IntOption -> Integer
Expand Down
6 changes: 3 additions & 3 deletions src/Language/Parser.hs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module Language.Parser where

import Data.Map as Map
import Data.Maybe
import Language.Common as C
import Language.Parser.Instance as I
import Language.Parser.LexerRules
Expand All @@ -11,7 +12,6 @@ import Language.Parser.Transform as TT
import Language.Parser.Typeside as T'
import Language.Program as P
import Text.Megaparsec
import Data.Maybe


parseAqlProgram' :: Parser (String, Exp)
Expand Down Expand Up @@ -75,5 +75,5 @@ toProg' o ((v,e):p) = case e of

parseAqlProgram :: String -> Err Prog
parseAqlProgram s = case runParser parseAqlProgram'' "" s of
Left err -> Left $ "Parse error: " ++ (parseErrorPretty err)
Right (o,x) -> pure $ toProg' o x
Left err -> Left $ "Parse error: " ++ (parseErrorPretty err)
Right (o,x) -> pure $ toProg' o x
2 changes: 1 addition & 1 deletion src/Language/Parser/Instance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ instRawParser = do
pure $ x
where p t = do i <- optional $ do
_ <- constant "imports"
many instExpParser
many instExpParser
e <- optional $ do
_ <- constant "generators"
y <- many genParser
Expand Down
4 changes: 2 additions & 2 deletions src/Language/Parser/Transform.hs
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
module Language.Parser.Transform (transExpParser) where

import Data.Maybe
import Language.Transform
import Text.Megaparsec
import Language.Parser.Instance
import Language.Parser.LexerRules
import Language.Parser.Mapping
import Language.Parser.Parser
import Language.Term
import Language.Transform
import Text.Megaparsec


gParser :: Parser (String, RawTerm)
Expand Down
4 changes: 2 additions & 2 deletions src/Language/Parser/Typeside.hs
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ eqParser = do o <- p
r <- rawTermParser
return (o,l,r) --(fromMaybe [] o, l, r)
where p = do _ <- constant "forall"
g <- sepBy varParser $ constant ","
g <- sepBy varParser $ constant ","
_ <- constant "."
return $ concat g

Expand Down Expand Up @@ -64,7 +64,7 @@ typesideLiteralSectionParser :: Parser X.TypesideRaw'
typesideLiteralSectionParser = do
i <- optional $ do
_ <- constant "imports"
many typesideExpParser
many typesideExpParser
t <- optional $ do
_ <- constant "types"
many identifier
Expand Down
Loading

0 comments on commit 8342fea

Please sign in to comment.