Skip to content

Commit

Permalink
Some cleanup and explicit typing. 148.
Browse files Browse the repository at this point in the history
  • Loading branch information
epost committed Aug 11, 2019
1 parent c8cc768 commit ed19924
Show file tree
Hide file tree
Showing 7 changed files with 70 additions and 62 deletions.
18 changes: 9 additions & 9 deletions src/Language/CQL.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ import Language.Typeside as T
import Prelude hiding (EQ, exp)
import System.IO.Unsafe

-- | Timesout a computation after @i@ microseconds.
-- | Times out a computation after @i@ microseconds.
timeout' :: NFData x => Integer -> Err x -> Err x
timeout' i p = unsafePerformIO $ do
m <- newEmptyMVar
Expand Down Expand Up @@ -240,15 +240,15 @@ typecheckSchemaExp p x = case x of
-- | The result of evaluating an CQL program.
type Env = KindCtx TypesideEx SchemaEx InstanceEx MappingEx QueryEx TransformEx Options

-- | Simple three phase evaluation and reporting.
-- | Parse, typecheck, and evaluate the CQL program.
runProg :: String -> Err (Prog, Types, Env)
runProg p = do
p1 <- parseCqlProgram p
ops <- toOptions defaultOptions $ other p1
o <- findOrder p1
p2 <- typecheckCqlProgram o p1 newTypes
p3 <- evalCqlProgram o p1 $ newEnv ops
return (p1, p2, p3)
runProg srcText = do
progE <- parseCqlProgram srcText
opts <- toOptions defaultOptions $ other progE
o <- findOrder progE
typesE <- typecheckCqlProgram o progE newTypes
envE <- evalCqlProgram o progE $ newEnv opts
return (progE, typesE, envE)

evalCqlProgram :: [(String,Kind)] -> Prog -> Env -> Err Env
evalCqlProgram [] _ env = pure env
Expand Down
16 changes: 11 additions & 5 deletions src/Language/Common.hs
Original file line number Diff line number Diff line change
Expand Up @@ -100,12 +100,14 @@ note :: b -> Maybe a -> Either b a
note n = maybe (Left n) Right

data Kind = CONSTRAINTS | TYPESIDE | SCHEMA | INSTANCE | MAPPING | TRANSFORM | QUERY | COMMAND | GRAPH | COMMENT | SCHEMA_COLIMIT
deriving (Show, Eq, Ord)
deriving (Show, Eq, Ord)

type ID = Integer

sepTup :: (Show a1, Show a2) => String -> (a1, a2) -> String
sepTup sep (k,v) = show k ++ sep ++ show v
-- | Drop quotes if argument doesn't contain a space.
dropQuotes :: String -> String
dropQuotes s = if ' ' `elem` s then Prelude.filter (not . ('\"' ==)) s
else s

section :: String -> String -> String
section heading body = heading ++ "\n" ++ indentLines body
Expand All @@ -116,6 +118,9 @@ indentLines = foldMap (\l -> tab <> l <> "\n"). lines
tab :: String
tab = " "

sepTup :: (Show a1, Show a2) => String -> (a1, a2) -> String
sepTup sep (k,v) = show k ++ sep ++ show v

-- | A version of intercalate that works on Foldables instead of just List,
-- | adapted from PureScript.
intercalate :: (Foldable f, Monoid m) => m -> f m -> m
Expand All @@ -127,8 +132,9 @@ intercalate sep xs = snd (foldl go (True, mempty) xs)
mapl :: Foldable f => (a -> b) -> f a -> [b]
mapl fn = fmap fn . Foldable.toList

toLowercase :: String -> String
toLowercase = Prelude.map toLower
-- | Converts a String to lowercase, like DataList.Extra.lower.
lower :: String -> String
lower = fmap toLower

-- | Heterogenous membership in a list
elem' :: (Typeable t, Typeable a, Eq a) => t -> [a] -> Bool
Expand Down
46 changes: 27 additions & 19 deletions src/Language/Instance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -258,16 +258,17 @@ data InstanceEx :: * where
algebraToPresentation :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk], 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'
algebraToPresentation alg@(Algebra sch en' _ _ _ ty' _ _ _) =
Presentation gens' sks' eqs'
where
gens' = Map.fromList $ reify en' $ Schema.ens sch
sks' = Map.fromList $ reify ty' $ Typeside.tys $ Schema.typeside sch
eqs1 = concatMap fksToEqs reified
eqs2 = concatMap attsToEqs reified
eqs' = Set.fromList $ eqs1 ++ eqs2
reified = reify en' $ Schema.ens sch
fksToEqs (x, e) = Prelude.map (\(fk , _) -> fkToEq x fk ) $ fksFrom' sch e
attsToEqs (x, e) = Prelude.map (\(att, _) -> attToEq x att) $ attsFrom' sch e
fksToEqs (x, e) = (\(fk , _) -> fkToEq x fk ) <$> fksFrom' sch e
attsToEqs (x, e) = (\(att, _) -> attToEq x att) <$> attsFrom' sch e
fkToEq x fk = EQ (Fk fk (Gen x), Gen $ aFk alg fk x)
attToEq x att = EQ (Att att (Gen x), upp $ aAtt alg att x)

Expand Down Expand Up @@ -376,7 +377,7 @@ initialInstance p dp' sch = Instance sch p dp'' $ initialAlgebra
teqs'' = concatMap (\(e, EQ (lhs,rhs)) -> fmap (\x -> EQ (nf'' this $ subst' lhs x, nf'' this $ subst' rhs x)) (Set.toList $ en' e)) $ Set.toList $ obs_eqs sch
teqs' = Set.union (Set.fromList teqs'') (Set.map (\(EQ (lhs,rhs)) -> EQ (nf'' this lhs, nf'' this rhs)) (Set.filter hasTypeType' $ eqs0 p))


-- | Assemble Skolem terms (labeled nulls).
assembleSks
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
=> Collage var ty sym en fk att gen sk
Expand All @@ -391,7 +392,7 @@ assembleSks col ens' = unionWith Set.union sks' $ fromListAccum gens'
ret = Map.fromSet (const Set.empty) $ ctys col

-- | Inlines type-algebra equations of the form @gen = term@.
-- The hard work is delegtated to functions from the Term module.
-- The hard work is delegated to functions from the 'Term' module.
simplifyAlg
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk, x, y])
=> Algebra var ty sym en fk att gen sk x y
Expand Down Expand Up @@ -420,8 +421,11 @@ deriving instance TyMap Ord '[en, fk, att, gen, sk] => Ord (TalgGen en fk att ge

deriving instance TyMap Eq '[fk, att, gen, sk] => Eq (TalgGen en fk att gen sk)

assembleGens :: (MultiTyMap '[Show, Ord, NFData] '[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
:: (MultiTyMap '[Show, Ord, NFData] '[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 (, Set.empty) $ Set.toList $ cens col
assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
where
Expand All @@ -447,9 +451,10 @@ close1m
-> [Term Void Void Void en fk Void gen Void]
close1m dp' col = dedup dp' . concatMap (close1 col dp')

dedup :: (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]
dedup
:: (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]
dedup dp' = nubBy (\x y -> dp' (EQ (upp x, upp y)))

close1
Expand Down Expand Up @@ -519,7 +524,7 @@ data InstExpRaw' =
, instraw_oeqs :: [(RawTerm, RawTerm)]
, instraw_options :: [(String, String)]
, instraw_imports :: [InstanceExp]
} deriving (Eq,Show)
} deriving (Eq, Show)

type Gen = String
type Sk = String
Expand Down Expand Up @@ -770,7 +775,8 @@ evalDeltaAlgebra (Mapping src' _ ens' fks0 atts0)


evalDeltaInst
:: forall var ty sym en fk att gen sk x y en' fk' att' . (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, x, y])
:: forall var ty sym en fk att gen sk x y en' fk' att'
. (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, x, 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 All @@ -779,7 +785,7 @@ evalDeltaInst m i _ = pure $ Instance (src m) (algebraToPresentation alg) eq' al
alg = evalDeltaAlgebra m i
eq' (EQ (l, r)) = dp i $ EQ (translateTerm l, translateTerm r)

--translateTerm :: Term Void ty sym en fk att (en, x) y -> Term Void ty sym en' fk' att' gen sk
translateTerm :: Term Void ty sym en fk att (en, x) y -> Term Void ty sym en' fk' att' gen sk
translateTerm t = case t of
Var v -> absurd v
Sym s' as -> Sym s' $ translateTerm <$> as
Expand Down Expand Up @@ -827,7 +833,8 @@ instance (TyMap Show '[var, ty, sym, en, fk, att, gen, sk, x, y], Eq en, Eq fk,
prettyTypeEqns = Set.map show teqs'

prettyEntity
:: (TyMap Show '[ty, sym, en, fk, att, x, y], Eq en)
:: forall var ty sym en fk att gen sk x y
. (TyMap Show '[ty, sym, en, fk, att, x, y], Eq en)
=> Algebra var ty sym en fk att gen sk x y
-> en
-> String
Expand All @@ -836,28 +843,29 @@ prettyEntity alg@(Algebra sch en' _ _ _ _ _ _ _) es =
"--------------------------------------------------------------------------------\n" ++
intercalate "\n" (prettyEntityRow es `mapl` en' es)
where
-- prettyEntityRow :: en -> x -> String
prettyEntityRow :: en -> x -> String
prettyEntityRow en'' e =
show e ++ ": " ++
intercalate "," (prettyFk e <$> fksFrom' sch en'') ++ ", " ++
intercalate "," (prettyAtt e <$> attsFrom' sch en'')

-- prettyAtt :: x -> (att, w) -> String
prettyAtt :: x -> (att, w) -> String
prettyAtt x (att,_) = show att ++ " = " ++ prettyTerm (aAtt alg att x)
prettyFk x (fk, _) = show fk ++ " = " ++ show (aFk alg fk x)
prettyTerm = show

-- TODO unquote identifiers; stick fks and attrs in separate `Group`s?
prettyEntityTable
:: (TyMap Show '[ty, sym, en, fk, att, x, y], Eq en)
:: forall var ty sym en fk att gen sk x y
. (TyMap Show '[ty, sym, en, fk, att, x, y], Eq en)
=> Algebra var ty sym en fk att gen sk x y
-> en
-> String
prettyEntityTable alg@(Algebra sch en' _ _ _ _ _ _ _) es =
show es ++ " (" ++ show (Set.size (en' es)) ++ ")\n" ++
Ascii.render show id id tbl
where
-- tbl :: T.Table x String String
tbl :: T.Table x String String
tbl = T.Table
(T.Group T.SingleLine (T.Header <$> Foldable.toList (en' es)))
(T.Group T.SingleLine (T.Header <$> prettyColumnHeaders))
Expand All @@ -875,7 +883,7 @@ prettyEntityTable alg@(Algebra sch en' _ _ _ _ _ _ _) es =

prettyFk x (fk, _) = show $ aFk alg fk x

-- prettyAtt :: x -> (att, w) -> String
prettyAtt :: x -> (att, ty) -> String
prettyAtt x (att,_) = prettyTerm $ aAtt alg att x

prettyTerm = show
8 changes: 4 additions & 4 deletions src/Language/Options.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ along with this program. If not, see <https://www.gnu.org/licenses/>.
module Language.Options where

import Data.Void
import Language.Common
import Language.Common (Err, intercalate, lower)
import Text.Read

data Options = Options {
Expand Down Expand Up @@ -59,7 +59,7 @@ toIntegerOption (k, v) = case matches of
[] -> Left $ "No option called " ++ k
(x:_) -> do { a <- parseInt v ; return (x, a) }
where
matches = [ k' | k' <- opsI, toLowercase (show k') == k ]
matches = [ k' | k' <- opsI, lower (show k') == k ]
parseInt :: String -> Err Integer
parseInt x = case readMaybe x of
Nothing -> Left $ "Not an int: " ++ x
Expand All @@ -71,15 +71,15 @@ toStringOption (k,v) = case matches of
[] -> Left $ "No option called " ++ k
(x:_) -> return (x, v)
where
matches = [ k' | k' <- opsS, toLowercase (show k') == k ]
matches = [ k' | k' <- opsS, lower (show k') == k ]


toBoolOption :: (String, String) -> Err (BoolOption, Bool)
toBoolOption (k,v) = case matches of
[] -> Left $ "No option called " ++ k
(x:_) -> do { a <- parseBool v ; return (x, a) }
where
matches = [ k' | k' <- opsB, toLowercase (show k') == k ]
matches = [ k' | k' <- opsB, lower (show k') == k ]
parseBool z = case z of
"true" -> Right True
"false" -> Right False
Expand Down
20 changes: 10 additions & 10 deletions src/Language/Program.hs
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ instance NFData Val where
ValT x -> rnf x
ValQ x -> rnf x

-- | Equivalent to Ctx (String + ... + String) (ts + ... + t)
-- | Isomorphic to @Ctx (String + ... + String) (ts + ... + t)@.
data KindCtx ts s i m q t o
= KindCtx
{ typesides :: Ctx String ts
Expand All @@ -90,8 +90,8 @@ data KindCtx ts s i m q t o
, other :: o
}

-- | CQL programs
type Prog = KindCtx TypesideExp SchemaExp InstanceExp MappingExp QueryExp TransformExp [(String, String)]
-- | A CQL program.
type Prog = KindCtx TypesideExp SchemaExp InstanceExp MappingExp QueryExp TransformExp [(String, String)]

newProg :: KindCtx ts s i m q t [a]
newProg = newEnv []
Expand Down Expand Up @@ -122,10 +122,10 @@ instance TyMap Show '[ts, s, i, m, q, t, o] => Show (KindCtx ts s i m q t o) whe
showCtx m = unlines $ (\(k,v) -> show k ++ " = " ++ show v ++ "\n") <$> Map.toList m

allVars :: KindCtx ts s i m q t o -> [(String, Kind)]
allVars x =
fmap (, TYPESIDE ) (keys $ typesides x) ++
fmap (, SCHEMA ) (keys $ schemas x) ++
fmap (, INSTANCE ) (keys $ instances x) ++
fmap (, MAPPING ) (keys $ mappings x) ++
fmap (, QUERY ) (keys $ queries x) ++
fmap (, TRANSFORM) (keys $ transforms x)
allVars ctx =
(fmap (, TYPESIDE ) . keys . typesides $ ctx) <>
(fmap (, SCHEMA ) . keys . schemas $ ctx) <>
(fmap (, INSTANCE ) . keys . instances $ ctx) <>
(fmap (, MAPPING ) . keys . mappings $ ctx) <>
(fmap (, QUERY ) . keys . queries $ ctx) <>
(fmap (, TRANSFORM) . keys . transforms $ ctx)
2 changes: 1 addition & 1 deletion src/Language/Schema.hs
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ evalSchemaRaw' x (SchemaExpRaw' _ ens'x fks'x atts'x peqs oeqs _ _) is = do
let rhs' = procTerm v (keys' fks') (keys' atts') rhs
rest <- procOeqs fks' atts' eqs'
if not $ hasTypeType'' lhs'
then Left $ "Bad obs equation: " ++ show lhs ++ " == " ++ show rhs
then Left $ "Bad observation equation: " ++ show lhs ++ " == " ++ show rhs
else pure $ Set.insert (en, EQ (lhs', rhs')) rest

infer _ (Just t) _ _ _ _ = return t
Expand Down
22 changes: 8 additions & 14 deletions src/Language/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -90,25 +90,23 @@ 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 -> dropQuotes $ show v
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

dropQuotes :: String -> String
dropQuotes s = if '\"' `elem` s then Prelude.filter (not . ('\"' ==)) s
else s

deriving instance TyMap Ord '[var, ty, sym, en, fk, att, gen, sk] => Ord (Term var ty sym en fk att gen sk)

-- | A symbol (non-variable).
Expand Down Expand Up @@ -154,7 +152,7 @@ mapTerm v t r e f a g s x = case x of
mapVar :: var -> Term () ty sym en fk att gen sk -> Term var ty sym en fk att gen sk
mapVar v = mapTerm (const v) id id id id id id id

-- | The number of variable and symbol occurances in a term.
-- | The number of variable and symbol occurrences in a term.
size :: Term var ty sym en fk att gen sk -> Integer
size x = case x of
Var _ -> 1
Expand Down Expand Up @@ -223,9 +221,9 @@ hasTypeType'' t = case t of
-- | Experimental
subst2
:: forall ty2 sym2 en2 fk2 att2 gen2 sk2 ty3 sym3 en3 fk3 att3 gen3 sk3 var sym en fk att gen sk var3
. (Eq var, Up sym2 sym, Up fk2 fk, Up att2 att, Up gen2 gen, Up sk2 sk, Up en2 en,
Up var3 var, Up sym3 sym, Up fk3 fk, Up att3 att, Up gen3 gen, Up sk3 sk, Up en3 en,
Up sym3 sym2, Up fk3 fk2, Up att3 att2, Up gen3 gen2, Up sk3 sk2, Up en3 en2, Up ty3 ty2)
. (Eq var, Up sym2 sym, Up fk2 fk, Up att2 att, Up gen2 gen, Up sk2 sk, Up en2 en,
Up var3 var, Up sym3 sym, Up fk3 fk, Up att3 att, Up gen3 gen, Up sk3 sk, Up en3 en,
Up sym3 sym2, Up fk3 fk2, Up att3 att2, Up gen3 gen2, Up sk3 sk2, Up en3 en2, Up ty3 ty2)
=> Term () ty2 sym2 en2 fk2 att2 gen2 sk2
-> Term var3 ty3 sym3 en3 fk3 att3 gen3 sk3
-> Term var ty2 sym en fk att gen sk
Expand Down Expand Up @@ -278,7 +276,7 @@ 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

-- | If there is one, finds an equation of the form empty |- @gen/sk = term@,
-- | If there is one, finds an equation of the form empty |- @gen/sk = term@,
-- where @gen@ does not occur in @term@.
findSimplifiable
:: (Eq ty, Eq sym, Eq en, Eq fk, Eq att, Eq gen, Eq sk)
Expand Down Expand Up @@ -668,7 +666,3 @@ typeOfEq' col (ctx, EQ (lhs, rhs)) = do
if lhs' == rhs'
then Right lhs'
else Left $ "Equation lhs has type " ++ show lhs' ++ " but rhs has type " ++ show rhs'



--Set is not Traversable! Lame

0 comments on commit ed19924

Please sign in to comment.