Skip to content

Commit

Permalink
Add pivot feature. #146 (#147)
Browse files Browse the repository at this point in the history 
* more work on pivot (Ryan)

* pivot is essentially done but finishing it causes cyclic imports

* code formatting and styling #38

* Rename AQL stuff in tests to CQL. #146

* Address @marcosh's comments from #128. #146
  • Loading branch information
@epost
epost authored Aug 7, 2019
1 parent 99cada6 commit b7b6e91
Show file tree
Hide file tree
Showing 25 changed files with 575 additions and 466 deletions.
55 changes: 55 additions & 0 deletions examples/Petri.cql
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@

schema Net = literal : empty {
entities
Input Place Trans Output
foreign_keys
place : Input -> Place
trans : Input -> Trans
place : Output -> Place
trans : Output -> Trans
}

/*
* p1 ->t1-> p2 ->t2-> p3
*/
instance N = literal : Net {
generators
p1 p2 p3 : Place
t1 t2 : Trans
i1 i2 : Input
o1 o2 : Output
equations
i1.place = p1
i1.trans = t1
o1.trans = t1
o1.place = p2

i2.place = p2
i2.trans = t2
o2.trans = t2
o2.place = p3

options
interpret_as_algebra = true
}

/*
entities
i1 i2 o1 o2 p1 p2 p3 t1 t2
foreign_keys
trans : o2 -> t2
place : o2 -> p3
place : o1 -> p2
trans : o1 -> t1
trans : i2 -> t2
place : i2 -> p2
place : i1 -> p1
trans : i1 -> t1
*/
//schema intN = pivot N

//mapping proj = pivot N // intN -> Net

//instance J = pivot N

//instance k = sigma proj J // = I
61 changes: 34 additions & 27 deletions src/Language/CQL.hs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

{-
SPDX-License-Identifier: AGPL-3.0-only
Expand Down Expand Up @@ -57,7 +58,7 @@ import Language.Schema as S
import Language.Term as Term
import Language.Transform as Tr
import Language.Typeside as T
import Prelude hiding (EQ)
import Prelude hiding (EQ, exp)
import System.IO.Unsafe

-- | Timesout a computation after @i@ microseconds.
Expand All @@ -66,8 +67,7 @@ timeout' i p = unsafePerformIO $ do
m <- newEmptyMVar
computer <- forkIO $ f m p
_ <- forkIO $ s m computer
ret <- takeMVar m
return ret
takeMVar m
where
secs = (fromIntegral i) * 1000000
f m p0 = do
Expand All @@ -88,8 +88,8 @@ timeout' i p = unsafePerformIO $ do
class Typecheck e e' where
typecheck :: Types -> e -> Err e'

-- | Checks that e.g. in sigma F I that F : S -> T and I : S-Inst.
-- Checking that S is well-formed is done by @validate@.
-- | Checks that e.g. in @sigma F I@ that @F : S -> T and I : S-Inst@.
-- Checking that @S@ is well-formed is done by 'validate'.
typecheckCqlProgram :: [(String,Kind)] -> Prog -> Types -> Err Types
typecheckCqlProgram [] _ x = pure x
typecheckCqlProgram ((v, k):l) prog ts = do
Expand Down Expand Up @@ -126,7 +126,7 @@ instance Typecheck QueryExp (SchemaExp, SchemaExp) where

typecheckTransExp :: Types -> TransformExp -> Err (InstanceExp, InstanceExp)
typecheckTransExp p (TransformVar v) = note ("Undefined transform: " ++ show v) $ Map.lookup v $ transforms p
typecheckTransExp _ (TransformId s) = pure (s, s)
typecheckTransExp _ (TransformId s) = pure (s, s)

typecheckTransExp p (TransformComp f g) = do
(a, b) <- typecheckTransExp p f
Expand Down Expand Up @@ -169,7 +169,7 @@ typecheckTransExp p (TransformRaw r) = do
l' <- typecheckInstExp p $ transraw_src r
r' <- typecheckInstExp p $ transraw_dst r
if l' == r'
then pure $ (transraw_src r, transraw_src r)
then pure (transraw_src r, transraw_src r)
else Left "Mapping has non equal schemas"

typecheckTransExp _ _ = error "todo"
Expand Down Expand Up @@ -209,6 +209,7 @@ typecheckInstExp p (InstanceDelta f' i _) = do
if t == t'
then pure s
else Left "(Delta): Instance not on mapping target."
typecheckInstExp _ (InstancePivot _) = undefined --todo: requires breaking import cycle

typecheckInstExp _ _ = error "todo"

Expand All @@ -222,9 +223,9 @@ typecheckTypesideExp p x = case x of
typecheckSchemaExp
:: Types -> SchemaExp -> Either String TypesideExp
typecheckSchemaExp p x = case x of
SchemaRaw r -> pure $ schraw_ts r
SchemaVar v -> note ("Undefined schema: " ++ show v) $ Map.lookup v $ schemas p
SchemaInitial t -> do { _ <- typecheckTypesideExp p t ; return t }
SchemaRaw r -> pure $ schraw_ts r
SchemaVar v -> note ("Undefined schema: " ++ show v) $ Map.lookup v $ schemas p
SchemaInitial t -> do { _ <- typecheckTypesideExp p t ; return t }
SchemaCoProd l r -> do
l' <- typecheckSchemaExp p l
r' <- typecheckSchemaExp p r
Expand Down Expand Up @@ -258,7 +259,7 @@ evalCqlProgram ((v,k):l) prog env = do
evalCqlProgram l prog $ setEnv env v t

findOrder :: Prog -> Err [(String, Kind)]
findOrder (p@(KindCtx t s i m q tr _)) = do
findOrder p@(KindCtx t s i m q tr _) = do
ret <- tsort g
pure $ reverse ret
where
Expand Down Expand Up @@ -296,7 +297,7 @@ getKindCtx g v k = case k of
_ -> error "todo"
where
n :: forall x. Maybe x -> Err x
n x = note ("Undefined " ++ show k ++ ": " ++ v) x
n = note ("Undefined " ++ show k ++ ": " ++ v)

setEnv :: Env -> String -> Val -> Env
setEnv env v val = case val of
Expand Down Expand Up @@ -331,7 +332,7 @@ instance Evalable InstanceExp InstanceEx where
where
checkCons (InstanceEx i) True = if freeTalg i
then pure ()
else Left $ "Warning: type algebra not free. Set require_consistency = false to continue."
else Left "Warning: type algebra not free. Set require_consistency = false to continue."
checkCons _ False = pure ()
getOptions = getOptionsInstance

Expand Down Expand Up @@ -361,7 +362,7 @@ getOptions' e = case e of
------------------------------------------------------------------------------------------------------------

evalTypeside :: Prog -> Env -> TypesideExp -> Err TypesideEx
evalTypeside _ _ TypesideInitial = pure $ TypesideEx $ initialTypeside
evalTypeside _ _ TypesideInitial = pure $ TypesideEx initialTypeside

evalTypeside p e (TypesideRaw r) = do
x <- mapM (evalTypeside p e) $ tsraw_imports r
Expand All @@ -387,7 +388,7 @@ evalTransform p env (TransformId s) = do
evalTransform p env (TransformComp f g) = do
(TransformEx (f' :: Transform var ty sym en fk att gen sk x y gen' sk' x' y' )) <- evalTransform p env f
(TransformEx (g' :: Transform var2 ty2 sym2 en2 fk2 att2 gen2 sk2 x2 y2 gen'2 sk'2 x'2 y'2)) <- evalTransform p env g
z <- composeTransform f' $ (fromJust $ ((cast g') :: Maybe (Transform var ty sym en fk att gen' sk' x' y' gen'2 sk'2 x'2 y'2)))
z <- composeTransform f' (fromJust (cast g' :: Maybe (Transform var ty sym en fk att gen' sk' x' y' gen'2 sk'2 x'2 y'2)))
pure $ TransformEx z

evalTransform p env (TransformRaw r) = do
Expand All @@ -400,28 +401,28 @@ evalTransform prog env (TransformSigma f' i o) = do
(MappingEx (f'' :: Mapping var ty sym en fk att en' fk' att')) <- evalMapping prog env f'
(TransformEx (i' :: Transform var'' ty'' sym'' en'' fk'' att'' gen sk x y gen' sk' x' y')) <- evalTransform prog env i
o' <- toOptions (other env) o
r <- evalSigmaTrans f'' (fromJust $ ((cast i') :: Maybe (Transform var ty sym en fk att gen sk x y gen' sk' x' y'))) o'
r <- evalSigmaTrans f'' (fromJust (cast i' :: Maybe (Transform var ty sym en fk att gen sk x y gen' sk' x' y'))) o'
pure $ TransformEx r

evalTransform prog env (TransformDelta f' i o) = do
(MappingEx (f'' :: Mapping var ty sym en' fk' att' en fk att)) <- evalMapping prog env f'
(TransformEx (i' :: Transform var'' ty'' sym'' en'' fk'' att'' gen sk x y gen' sk' x' y')) <- evalTransform prog env i
o' <- toOptions (other env) o
r <- evalDeltaTrans f'' (fromJust $ ((cast i') :: Maybe (Transform var ty sym en fk att gen sk x y gen' sk' x' y'))) o'
r <- evalDeltaTrans f'' (fromJust (cast i' :: Maybe (Transform var ty sym en fk att gen sk x y gen' sk' x' y'))) o'
pure $ TransformEx r

evalTransform prog env (TransformSigmaDeltaUnit 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
o' <- toOptions (other env) o
r <- evalDeltaSigmaUnit f'' (fromJust $ ((cast i') :: Maybe (Instance var ty sym en fk att gen sk x y))) o'
r <- evalDeltaSigmaUnit f'' (fromJust (cast i' :: Maybe (Instance var ty sym en fk att gen sk x y))) o'
pure $ TransformEx r

evalTransform prog env (TransformSigmaDeltaCoUnit 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
o' <- toOptions (other env) o
r <- evalDeltaSigmaCoUnit f'' (fromJust $ ((cast i') :: Maybe (Instance var ty sym en' fk' att' gen sk x y))) o'
r <- evalDeltaSigmaCoUnit f'' (fromJust (cast i' :: Maybe (Instance var ty sym en' fk' att' gen sk x y))) o'
pure $ TransformEx r

evalTransform _ _ _ = error "todo"
Expand All @@ -433,12 +434,14 @@ evalMapping _ env (MappingVar v) = note ("Could not find " ++ show v ++ " in ctx
evalMapping p env (MappingComp f g) = do
(MappingEx (f' :: Mapping var ty sym en fk att en' fk' att' )) <- evalMapping p env f
(MappingEx (g' :: Mapping var2 ty2 sym2 en2 fk2 att2 en'2 fk'2 att'2)) <- evalMapping p env g
z <- composeMapping f' $ (fromJust $ ((cast g') :: Maybe (Mapping var ty sym en' fk' att' en'2 fk'2 att'2)))
z <- composeMapping f' $ (fromJust (cast g' :: Maybe (Mapping var ty sym en' fk' att' en'2 fk'2 att'2)))
pure $ MappingEx z

evalMapping p env (MappingId s) = do
(SchemaEx s') <- evalSchema p env s
pure $ MappingEx $ foldr (\en' (Mapping s'' t e f' a) -> Mapping s'' t (Map.insert en' en' e) (f'' en' s' f') (g' en' s' a)) (Mapping s' s' Map.empty Map.empty Map.empty) (S.ens s')
pure $ MappingEx $ foldr
(\en' (Mapping s'' t e f' a) -> Mapping s'' t (Map.insert en' en' e) (f'' en' s' f') (g' en' s' a))
(Mapping s' s' Map.empty Map.empty Map.empty) (S.ens s')
where
f'' en' s' f''' = foldr (\(fk, _) m -> Map.insert fk (Fk fk $ Var ()) m) f''' $ fksFrom' s' en'
g' en' s' f''' = foldr (\(fk, _) m -> Map.insert fk (Att fk $ Var ()) m) f''' $ attsFrom' s' en'
Expand Down Expand Up @@ -467,8 +470,13 @@ evalSchema prog env (SchemaRaw r) = do
evalSchema _ _ _ = undefined


evalInstance :: Prog -> Env -> InstanceExp -> Either [Char] InstanceEx
evalInstance _ env (InstanceVar v) = note ("Could not find " ++ show v ++ " in ctx") $ Map.lookup v $ instances env
evalInstance :: Prog -> Env -> InstanceExp -> Either String InstanceEx
evalInstance _ env (InstanceVar v) = note ("Could not find " ++ show v ++ " in ctx") $ Map.lookup v $ instances env

evalInstance prog env (InstancePivot i) = do
InstanceEx i' <- evalInstance prog env i
let (_, i'', _) = pivot i'
return $ InstanceEx i''

evalInstance prog env (InstanceInitial s) = do
SchemaEx ts'' <- evalSchema prog env s
Expand All @@ -483,15 +491,14 @@ evalInstance prog env (InstanceSigma 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
o' <- toOptions (other env) o
r <- evalSigmaInst f'' (fromJust $ ((cast i') :: Maybe (Instance var ty sym en fk att gen sk x y))) 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
o' <- toOptions (other env) o
r <- evalDeltaInst f'' (fromJust $ ((cast i') :: Maybe (Instance var ty sym en' fk' att' gen sk x y))) o'
r <- evalDeltaInst f'' (fromJust (cast i' :: Maybe (Instance var ty sym en' fk' att' gen sk x y))) o'
return $ InstanceEx r

evalInstance _ _ _ = error "todo"


16 changes: 8 additions & 8 deletions src/Language/Common.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,15 +64,15 @@ fromListAccum ((k,v):kvs) = Map.insert k op (fromListAccum kvs)
op = maybe (Set.singleton v) (Set.insert v) (Map.lookup k r)
r = fromListAccum kvs

showCtx :: (Show a1, Show a2) => Map a1 a2 -> [Char]
showCtx m = intercalate " " $ Prelude.map (\(k,v) -> show k ++ " : " ++ show v) $ Map.toList m
showCtx :: (Show a1, Show a2) => Map a1 a2 -> String
showCtx m = unwords $ Prelude.map (\(k,v) -> show k ++ " : " ++ show v) $ Map.toList m

fromList'' :: (Show k, Ord k) => [k] -> Err (Set k)
fromList'' [] = return Set.empty
fromList'' (k:l) = do
l' <- fromList'' l
if Set.member k l'
then Left $ "Duplicate binding: " ++ (show k)
then Left $ "Duplicate binding: " ++ show k
else pure $ Set.insert k l'

-- | Converts a map to a finite list, returning an error when there are duplicate bindings.
Expand All @@ -81,7 +81,7 @@ toMapSafely [] = return Map.empty
toMapSafely ((k,v):l) = do
l' <- toMapSafely l
if Map.member k l'
then Left $ "Duplicate binding: " ++ (show k)
then Left $ "Duplicate binding: " ++ show k
else pure $ Map.insert k v l'

showCtx'' :: (Show a1, Show a2) => Map a1 a2 -> String
Expand All @@ -102,16 +102,16 @@ type Err = Either String

-- generic helper inspired by https://pursuit.purescript.org/search?q=note
note :: b -> Maybe a -> Either b a
note n x = maybe (Left n) Right x
note n = maybe (Left n) Right

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

type ID = Integer


showCtx' :: (Show a1, Show a2) => Map a1 a2 -> [Char]
showCtx' m = intercalate "\n\t" $ fmap (\(k,v) -> show k ++ " : " ++ show v) $ Map.toList m
showCtx' :: (Show a1, Show a2) => Map a1 a2 -> String
showCtx' m = intercalate "\n\t" $ (\(k,v) -> show k ++ " : " ++ show v) <$> Map.toList m

-- | A version of intercalate that works on Foldables instead of just List,
-- | adapted from PureScript.
Expand All @@ -129,7 +129,7 @@ toLowercase = Prelude.map toLower

-- | Heterogenous membership in a list
elem' :: (Typeable t, Typeable a, Eq a) => t -> [a] -> Bool
elem' x ys = maybe False (flip elem ys) (cast x)
elem' x ys = maybe False (`elem` ys) (cast x)

-- | Heterogenous membership in the keys of a map list
member' :: (Typeable t, Typeable a, Eq a) => t -> Map a v -> Bool
Expand Down
14 changes: 6 additions & 8 deletions src/Language/Congruence.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ import Language.Internal
decide :: Ord t => [(Term t, Term t)] -> Term t -> Term t -> Bool
decide theory lhs rhs = not result
where
conjunctions = fmap (\(l, r) -> Equal l r) theory
conjunctions = fmap (uncurry Equal) theory
Identity result = hasModel (Conjunction $ NotEqual lhs rhs : conjunctions)


Expand All @@ -56,11 +56,11 @@ hasModel (Conjunction conjunctions) = runUnionFind $ do


merge :: Monad m => Graph t -> (Vert t, Vert t) -> UnionFindT (LNode t) m ()
merge gr (u,v) = do
merge gr (u,v) =
unless (equivalent u v) $ do
pu <- predOfAllVertEquivTo u
pv <- predOfAllVertEquivTo v
union u v
u `union` v
needMerging <- filterM (notEquivalentButCongruent gr)
[ (x,y) | x <- pu, y <- pv ]
traverse_ (merge gr) needMerging
Expand All @@ -76,12 +76,10 @@ notEquivalentButCongruent gr (x,y) = do

-- testing
congruent :: (Monad m) => Graph t -> Vert t -> Vert t -> UnionFindT (LNode t) m Bool
congruent gr x y = do
congruent gr x y =
if outDegree gr x /= outDegree gr y
then return False
else and <$> zipWithM equivalent
(successors gr x)
(successors gr y)
then return False
else and <$> zipWithM equivalent (successors gr x) (successors gr y)

{--
constructModel :: Monad m => Graph -> UnionFindT (LNode Text) m Satisfiability
Expand Down
6 changes: 3 additions & 3 deletions src/Language/Graph.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ along with this program. If not, see <https://www.gnu.org/licenses/>.

module Language.Graph where

import Prelude
import Prelude

data Graph a = Graph { vertices :: [a], edges :: [(a, a)] } deriving Show

Expand All @@ -32,10 +32,10 @@ connections :: (Eq a) => ((a, a) -> a) -> a -> Graph a -> [(a, a)]
connections f0 x (Graph _ e) = filter ((==x) . f0) e

outbound :: Eq b => b -> Graph b -> [(b, b)]
outbound a = connections fst a
outbound = connections fst

inbound :: Eq a => a -> Graph a -> [(a, a)]
inbound a = connections snd a
inbound = connections snd

-- | Topological sort.
tsort :: (Eq a) => Graph a -> Either String [a]
Expand Down
Loading

0 comments on commit b7b6e91

Please sign in to comment.