← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs
1
 
{-# LANGUAGE CPP #-}
2
 
{-# LANGUAGE DeriveFunctor #-}
3
 
{-# LANGUAGE FlexibleInstances #-}
4
 
{-# LANGUAGE MultiParamTypeClasses #-}
 
1
{-# LANGUAGE CPP                       #-}
 
2
{-# LANGUAGE FlexibleInstances         #-}
 
3
{-# LANGUAGE MultiParamTypeClasses     #-}
5
4
{-# LANGUAGE NoMonomorphismRestriction #-}
6
 
{-# LANGUAGE PatternGuards #-}
7
 
{-# LANGUAGE ScopedTypeVariables #-}
8
 
{-# LANGUAGE TupleSections #-}
9
 
{-# LANGUAGE TypeSynonymInstances #-}
 
5
{-# LANGUAGE PatternGuards             #-}
 
6
{-# LANGUAGE ScopedTypeVariables       #-}
 
7
{-# LANGUAGE TupleSections             #-}
 
8
{-# LANGUAGE TypeSynonymInstances      #-}
10
9
 
11
10
module Agda.TypeChecking.SizedTypes.WarshallSolver where
12
11
 
35
32
-- (Edge'(..), allNodes, emptyGraph, insertEdge, graphToList, graphFromList, nodes, lookupEdge, outgoing, incoming, diagonal, transClos)
36
33
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
37
34
 
38
 
#include "../../undefined.h"
 
35
#include "undefined.h"
39
36
import Agda.Utils.Impossible
40
37
 
41
38
type Graph r f a = Graph.Graph (Node r f) (Node r f) a
44
41
type Nodes r f = Graph.Nodes (Node r f)
45
42
type LabelledEdge r f = Edge' r f Label
46
43
 
47
 
src  = Graph.source
 
44
src :: Edge s t e -> s
 
45
src = Graph.source
 
46
 
 
47
dest :: Edge s t e -> t
48
48
dest = Graph.target
49
49
 
 
50
lookupEdge :: (Ord s, Ord t) => Graph.Graph s t e -> s -> t -> Maybe e
50
51
lookupEdge g s t = Graph.lookup s t g
 
52
 
 
53
graphToList :: (Ord s, Ord t) => Graph.Graph s t e -> [Edge s t e]
51
54
graphToList = Graph.toList
 
55
 
 
56
graphFromList :: (Ord s, Ord t) => [Edge s t e] -> Graph.Graph s t e
52
57
graphFromList = Graph.fromList
53
58
 
 
59
insertEdge :: (Ord s, Ord t, MeetSemiLattice e, Top e) =>
 
60
              Edge s t e -> Graph.Graph s t e -> Graph.Graph s t e
54
61
insertEdge e g
55
62
  | isTop (label e) = g
56
63
  | otherwise       = Graph.insertEdgeWith meet e g
294
301
-- | A graph forest.
295
302
type Graphs r f a = [Graph r f a]
296
303
 
 
304
emptyGraphs :: Graphs r f a
297
305
emptyGraphs = []
298
306
 
299
307
-- | Split a list of graphs @gs@ into those that mention node @n@ and those that do not.
550
558
-- | Lower or upper bound for a flexible variable
551
559
type Bound r f = Map f (Set (SizeExpr' r f))
552
560
 
 
561
emptyBound :: Bound r f
553
562
emptyBound = Map.empty
554
563
 
555
564
data Bounds r f = Bounds
639
648
     Return these edges as a map from target notes to a list of edges.
640
649
     We assume the graph is reflexive-transitive.
641
650
 -}
642
 
commonSuccs :: (Ord r, Ord f, Dioid a) => Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
643
 
commonSuccs hg srcs = intersectAll $  map (buildmap . outgoing hg) srcs
 
651
commonSuccs :: (Ord r, Ord f, Dioid a) =>
 
652
               Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
 
653
commonSuccs hg srcs = intersectAll $ map (buildmap . outgoing hg) srcs
644
654
  where
645
 
   buildmap = Map.fromList . map (\ e -> (dest e, [e]))
 
655
   buildmap            = Map.fromList . map (\ e -> (dest e, [e]))
646
656
   intersectAll []     = Map.empty
647
657
   intersectAll (m:ms) = foldl (Map.intersectionWith (++)) m ms
648
658
 
659
669
   intersectAll (m:ms) = foldl (Map.intersectionWith (++)) m ms
660
670
 
661
671
-- | Compute the sup of two different rigids or a rigid and a constant.
662
 
lub' :: forall r f . (Ord r, Ord f, Show r, Show f) => HypGraph r f -> (Node r f, Offset) -> (Node r f, Offset) -> Maybe (SizeExpr' r f)
 
672
lub' :: forall r f . (Ord r, Ord f, Show r, Show f) =>
 
673
        HypGraph r f -> (Node r f, Offset) -> (Node r f, Offset) -> Maybe (SizeExpr' r f)
663
674
lub' hg (node1, n) (node2, m) = do
664
675
  let sucs     = commonSuccs hg [node1, node2]
665
676
      sucNodes = smallest hg $ Map.keys sucs
887
898
 
888
899
-- * Tests
889
900
 
 
901
testSuccs :: Ord f => Map (Node [Char] f) [Edge' [Char] f Label]
890
902
testSuccs = commonSuccs hg [n1,n2]
891
903
  where
892
904
    n1 = NodeRigid "i"
902
914
         , Graph.Edge n2 n4 $ Label Le 5
903
915
         , Graph.Edge n2 n5 $ Label Le 6
904
916
         ]
 
917
 
905
918
-- testLub = smallest hg $ Map.keys $ commonSuccs hg [n1,n2] --
 
919
testLub :: (Show f, Ord f) => Maybe (SizeExpr' [Char] f)
906
920
testLub = lub hg (Rigid "i" 0) (Rigid "j" 2)
907
921
  where
908
922
    n1 = NodeRigid "i"