@@ -266,14 +266,17 @@ trans mor (Fk f a) = let x = trans mor a :: Term var' ty sym en' fk' att' gen' s
266
266
trans mor (Att f a) = subst (up14 $ fromJust $ Map. lookup f (m_atts mor)) $ trans mor a
267
267
268
268
269
- subst :: Eq var => Term () ty sym en fk att gen sk ->
270
- Term var ty sym en fk att gen sk -> Term var ty sym en fk att gen sk
271
- subst (Var () ) t = t
272
- subst (Sym f as) t = Sym f $ Prelude. map (\ x -> subst x t) as
273
- subst (Fk f a) t = Fk f $ subst a t
274
- subst (Att f a) t = Att f $ subst a t
275
- subst (Gen g) _ = Gen g
276
- subst (Sk g) _ = Sk g
269
+ subst
270
+ :: Eq var
271
+ => Term () ty sym en fk att gen sk
272
+ -> Term var ty sym en fk att gen sk
273
+ -> Term var ty sym en fk att gen sk
274
+ subst (Var () ) t = t
275
+ subst (Sym f as) t = Sym f $ (\ a -> subst a t) <$> as
276
+ subst (Fk f a ) t = Fk f $ subst a t
277
+ subst (Att f a ) t = Att f $ subst a t
278
+ subst (Gen g ) _ = Gen g
279
+ subst (Sk g ) _ = Sk g
277
280
278
281
279
282
checkDoms' :: forall var ty sym en fk att gen sk en' fk' att' gen' sk' .
@@ -351,9 +354,9 @@ initGround col = (me', mt')
351
354
352
355
closeGround :: (Ord ty , Ord en ) => Collage var ty sym en fk att gen sk -> (Map en Bool , Map ty Bool ) -> (Map en Bool , Map ty Bool )
353
356
closeGround col (me, mt) = (me', mt'')
354
- where mt''= Prelude. foldr (\ (_, (tys,ty)) m -> if and (Prelude. map ( \ ty' -> lookup2 ty' mt') tys) then Map. insert ty True m else m) mt' $ Map. toList $ csyms col
355
- mt' = Prelude. foldr (\ (_, (en,ty)) m -> if lookup2 en me' then Map. insert ty True m else m) mt $ Map. toList $ catts col
356
- me' = Prelude. foldr (\ (_, (en,_)) m -> if lookup2 en me then Map. insert en True m else m) me $ Map. toList $ cfks col
357
+ where mt''= Prelude. foldr (\ (_, (tys,ty)) m -> if and (( flip lookup2 mt') <$> tys) then Map. insert ty True m else m) mt' $ Map. toList $ csyms col
358
+ mt' = Prelude. foldr (\ (_, (en, ty)) m -> if lookup2 en me' then Map. insert ty True m else m) mt $ Map. toList $ catts col
359
+ me' = Prelude. foldr (\ (_, (en, _)) m -> if lookup2 en me then Map. insert en True m else m) me $ Map. toList $ cfks col
357
360
358
361
iterGround :: (Ord ty , Ord en , Show en , Show ty ) => Collage var ty sym en fk att gen sk -> (Map en Bool , Map ty Bool ) -> (Map en Bool , Map ty Bool )
359
362
iterGround col r = if r == r' then r else iterGround col r'
@@ -379,12 +382,12 @@ typeOf'
379
382
typeOf' _ ctx (Var v) = note (" Unbound variable: " ++ show v) $ Map. lookup v ctx
380
383
typeOf' col _ (Gen g) = case Map. lookup g $ cgens col of
381
384
Nothing -> Left $ " Unknown generator: " ++ show g
382
- Just t -> pure $ Right t
385
+ Just t -> Right $ Right t
383
386
typeOf' col _ (Sk s) = case Map. lookup s $ csks col of
384
387
Nothing -> Left $ " Unknown labelled null: " ++ show s
385
- Just t -> pure $ Left t
388
+ Just t -> Right $ Left t
386
389
typeOf' col ctx (xx@ (Fk f a)) = case Map. lookup f $ cfks col of
387
- Nothing -> Left $ " Unknown foreign key: " ++ show f
390
+ Nothing -> Left $ " Unknown foreign key: " ++ show f
388
391
Just (s, t) -> do s' <- typeOf' col ctx a
389
392
if (Right s) == s' then pure $ Right t else Left $ " Expected argument to have entity " ++
390
393
show s ++ " but given " ++ show s' ++ " in " ++ (show xx)
@@ -397,7 +400,7 @@ typeOf' col ctx (xx@(Sym f a)) = case Map.lookup f $ csyms col of
397
400
Nothing -> Left $ " Unknown function symbol: " ++ show f
398
401
Just (s, t) -> do s' <- mapM (typeOf' col ctx) a
399
402
if length s' == length s
400
- then if (fmap Left s) == s'
403
+ then if (Left <$> s) == s'
401
404
then pure $ Left t
402
405
else Left $ " Expected arguments to have types " ++
403
406
show s ++ " but given " ++ show s' ++ " in " ++ (show $ xx)
@@ -409,19 +412,20 @@ typeOfEq'
409
412
=> Collage var ty sym en fk att gen sk
410
413
-> (Ctx var (ty + en ), EQ var ty sym en fk att gen sk )
411
414
-> Err (ty + en )
412
- typeOfEq' col (ctx, EQ (lhs, rhs)) = do lhs' <- typeOf' col ctx lhs
413
- rhs' <- typeOf' col ctx rhs
414
- if lhs' == rhs'
415
- then pure lhs'
416
- else Left $ " Equation lhs has type " ++ show lhs' ++ " but rhs has type " ++ show rhs'
415
+ typeOfEq' col (ctx, EQ (lhs, rhs)) = do
416
+ lhs' <- typeOf' col ctx lhs
417
+ rhs' <- typeOf' col ctx rhs
418
+ if lhs' == rhs'
419
+ then Right $ lhs'
420
+ else Left $ " Equation lhs has type " ++ show lhs' ++ " but rhs has type " ++ show rhs'
417
421
418
422
checkDoms :: (Ord var , Show var , Ord gen , Show gen , Ord sk , Show sk , Ord fk , Show fk , Ord en , Show en , Show ty , Ord ty , Show att , Ord att , Show sym , Ord sym )
419
423
=> Collage var ty sym en fk att gen sk
420
424
-> Err ()
421
425
checkDoms col = do
422
- _ <- mapM f $ Map. elems $ csyms col
423
- _ <- mapM g $ Map. elems $ cfks col
424
- _ <- mapM h $ Map. elems $ catts col
426
+ _ <- mapM f $ Map. elems $ csyms col
427
+ _ <- mapM g $ Map. elems $ cfks col
428
+ _ <- mapM h $ Map. elems $ catts col
425
429
_ <- mapM isEn $ Map. elems $ cgens col
426
430
_ <- mapM isTy $ Map. elems $ csks col
427
431
pure ()
@@ -443,10 +447,10 @@ typeOfCol
443
447
:: (Ord var , Show var , Ord gen , Show gen , Ord sk , Show sk , Ord fk , Show fk , Ord en , Show en , Show ty , Ord ty , Show att , Ord att , Show sym , Ord sym )
444
448
=> Collage var ty sym en fk att gen sk
445
449
-> Err ()
446
- typeOfCol col = do checkDoms col
447
- _ <- mapM (typeOfEq' col) $ Set. toList $ ceqs col
448
- pure ()
449
-
450
+ typeOfCol col = do
451
+ checkDoms col
452
+ mapM_ (typeOfEq' col) $ Set. toList $ ceqs col
453
+ pure ()
450
454
451
455
data RawTerm = RawApp String [RawTerm ]
452
456
deriving Eq
@@ -455,18 +459,14 @@ instance Show RawTerm where
455
459
show (RawApp sym az) = show sym ++ " (" ++ (intercalate " ," . fmap show $ az) ++ " )"
456
460
457
461
upTerm
458
- :: Term var Void Void en fk Void gen Void -> Term var ty sym en fk att gen sk
459
- upTerm
460
- (Var v) = Var v
461
- upTerm
462
- (Fk f a) = Fk f $ upTerm a
463
- upTerm
464
- (Gen g) = Gen g
465
- upTerm
466
- (Sym f _) = absurd f
467
- upTerm
468
- (Sk f) = absurd f
469
- upTerm
470
- (Att f _) = absurd f
462
+ :: Term var Void Void en fk Void gen Void
463
+ -> Term var ty sym en fk att gen sk
464
+ upTerm t = case t of
465
+ Var v -> Var v
466
+ Fk f a -> Fk f $ upTerm a
467
+ Gen g -> Gen g
468
+ Sym f _ -> absurd f
469
+ Sk f -> absurd f
470
+ Att f _ -> absurd f
471
471
472
472
-- Set is not Traversable! Lame
0 commit comments