1- {-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-}
1+ {-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RankNTypes, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-}
22module Analysis.Concrete
33( Concrete (.. )
44, concrete
@@ -20,7 +20,6 @@ import Control.Effect.NonDet
2020import Control.Effect.Reader hiding (Local )
2121import Control.Effect.State
2222import Control.Monad ((<=<) , guard )
23- import qualified Data.Core as Core
2423import Data.File
2524import Data.Function (fix )
2625import qualified Data.IntMap as IntMap
@@ -30,7 +29,6 @@ import qualified Data.Map as Map
3029import Data.Name
3130import Data.Semigroup (Last (.. ))
3231import qualified Data.Set as Set
33- import Data.Term
3432import Data.Text (Text , pack )
3533import Data.Traversable (for )
3634import Prelude hiding (fail )
@@ -41,17 +39,17 @@ type Env = Map.Map User Precise
4139newtype FrameId = FrameId { unFrameId :: Precise }
4240 deriving (Eq , Ord , Show )
4341
44- data Concrete
45- = Closure Loc User ( Term ( Core. Ann :+: Core. Core ) User ) Env
42+ data Concrete term
43+ = Closure Loc User term Env
4644 | Unit
4745 | Bool Bool
4846 | String Text
4947 | Record Env
5048 deriving (Eq , Ord , Show )
5149 -- NB: We derive the 'Semigroup' instance for 'Concrete' to take the second argument. This is equivalent to stating that the return value of an imperative sequence of statements is the value of its final statement.
52- deriving Semigroup via Last Concrete
50+ deriving Semigroup via Last ( Concrete term )
5351
54- recordFrame :: Concrete -> Maybe Env
52+ recordFrame :: Concrete term -> Maybe Env
5553recordFrame (Record frame) = Just frame
5654recordFrame _ = Nothing
5755
@@ -60,44 +58,64 @@ newtype Frame = Frame
6058 }
6159 deriving (Eq , Ord , Show )
6260
63- type Heap = IntMap. IntMap Concrete
61+ type Heap term = IntMap. IntMap ( Concrete term )
6462
6563data Edge = Lexical | Import
6664 deriving (Eq , Ord , Show )
6765
6866
6967-- | Concrete evaluation of a term to a value.
7068--
71- -- >>> map fileBody (snd (concrete [File (Loc "bool" emptySpan) (Core.bool True)]))
69+ -- >>> map fileBody (snd (concrete eval [File (Loc "bool" emptySpan) (Core.bool True)]))
7270-- [Right (Bool True)]
73- concrete :: [File (Term (Core. Ann :+: Core. Core ) User )] -> (Heap , [File (Either (Loc , String ) Concrete )])
7471concrete
72+ :: (Foldable term , Show (term User ))
73+ => (forall sig m
74+ . (Carrier sig m , Member (Reader Loc ) sig , MonadFail m )
75+ => Analysis (term User ) Precise (Concrete (term User )) m
76+ -> (term User -> m (Concrete (term User )))
77+ -> (term User -> m (Concrete (term User )))
78+ )
79+ -> [File (term User )]
80+ -> (Heap (term User ), [File (Either (Loc , String ) (Concrete (term User )))])
81+ concrete eval
7582 = run
7683 . runFresh
7784 . runHeap
78- . traverse runFile
79-
80- runFile :: ( Carrier sig m
81- , Effect sig
82- , Member Fresh sig
83- , Member (State Heap ) sig
84- )
85- => File (Term (Core. Ann :+: Core. Core ) User )
86- -> m (File (Either (Loc , String ) Concrete ))
87- runFile file = traverse run file
85+ . traverse (runFile eval)
86+
87+ runFile
88+ :: ( Carrier sig m
89+ , Effect sig
90+ , Foldable term
91+ , Member Fresh sig
92+ , Member (State (Heap (term User ))) sig
93+ , Show (term User )
94+ )
95+ => (forall sig m
96+ . (Carrier sig m , Member (Reader Loc ) sig , MonadFail m )
97+ => Analysis (term User ) Precise (Concrete (term User )) m
98+ -> (term User -> m (Concrete (term User )))
99+ -> (term User -> m (Concrete (term User )))
100+ )
101+ -> File (term User )
102+ -> m (File (Either (Loc , String ) (Concrete (term User ))))
103+ runFile eval file = traverse run file
88104 where run = runReader (fileLoc file)
89105 . runFailWithLoc
90106 . runReader @ Env mempty
91107 . fix (eval concreteAnalysis)
92108
93109concreteAnalysis :: ( Carrier sig m
110+ , Foldable term
94111 , Member Fresh sig
95112 , Member (Reader Env ) sig
96113 , Member (Reader Loc ) sig
97- , Member (State Heap ) sig
114+ , Member (State ( Heap ( term User )) ) sig
98115 , MonadFail m
116+ , Show (term User )
99117 )
100- => Analysis Precise Concrete m
118+ => Analysis ( term User ) Precise ( Concrete ( term User )) m
101119concreteAnalysis = Analysis {.. }
102120 where alloc _ = fresh
103121 bind name addr m = local (Map. insert name addr) m
@@ -133,7 +151,7 @@ concreteAnalysis = Analysis{..}
133151 pure (val >>= lookupConcrete heap n)
134152
135153
136- lookupConcrete :: Heap -> User -> Concrete -> Maybe Precise
154+ lookupConcrete :: Heap term -> User -> Concrete term -> Maybe Precise
137155lookupConcrete heap name = run . evalState IntSet. empty . runNonDet . inConcrete
138156 where -- look up the name in a concrete value
139157 inConcrete = inFrame <=< maybeA . recordFrame
@@ -150,7 +168,7 @@ lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete
150168 maybeA = maybe empty pure
151169
152170
153- runHeap :: StateC Heap m a -> m (Heap , a )
171+ runHeap :: StateC ( Heap term ) m a -> m (Heap term , a )
154172runHeap = runState mempty
155173
156174
@@ -159,7 +177,7 @@ runHeap = runState mempty
159177-- > λ let (heap, res) = concrete [ruby]
160178-- > λ writeFile "/Users/rob/Desktop/heap.dot" (export (addressStyle heap) (heapAddressGraph heap))
161179-- > λ :!dot -Tsvg < ~/Desktop/heap.dot > ~/Desktop/heap.svg
162- heapGraph :: (Precise -> Concrete -> a ) -> (Either Edge User -> Precise -> G. Graph a ) -> Heap -> G. Graph a
180+ heapGraph :: (Precise -> Concrete term -> a ) -> (Either Edge User -> Precise -> G. Graph a ) -> Heap term -> G. Graph a
163181heapGraph vertex edge h = foldr (uncurry graph) G. empty (IntMap. toList h)
164182 where graph k v rest = (G. vertex (vertex k v) `G.connect` outgoing v) `G.overlay` rest
165183 outgoing = \ case
@@ -169,14 +187,14 @@ heapGraph vertex edge h = foldr (uncurry graph) G.empty (IntMap.toList h)
169187 Closure _ _ _ env -> foldr (G. overlay . edge (Left Lexical )) G. empty env
170188 Record frame -> Map. foldrWithKey (\ k -> G. overlay . edge (Right k)) G. empty frame
171189
172- heapValueGraph :: Heap -> G. Graph Concrete
190+ heapValueGraph :: Heap term -> G. Graph ( Concrete term )
173191heapValueGraph h = heapGraph (const id ) (const fromAddr) h
174192 where fromAddr addr = maybe G. empty G. vertex (IntMap. lookup addr h)
175193
176- heapAddressGraph :: Heap -> G. Graph (EdgeType , Precise )
194+ heapAddressGraph :: Heap term -> G. Graph (EdgeType term , Precise )
177195heapAddressGraph = heapGraph (\ addr v -> (Value v, addr)) (fmap G. vertex . (,) . either Edge Slot )
178196
179- addressStyle :: Heap -> G. Style (EdgeType , Precise ) Text
197+ addressStyle :: Heap term -> G. Style (EdgeType term , Precise ) Text
180198addressStyle heap = (G. defaultStyle vertex) { G. edgeAttributes }
181199 where vertex (_, addr) = pack (show addr) <> " = " <> maybe " ?" fromConcrete (IntMap. lookup addr heap)
182200 edgeAttributes _ (Slot name, _) = [" label" G. := name]
@@ -191,12 +209,13 @@ addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes }
191209 Record _ -> " {}"
192210 showPos (Pos l c) = pack (show l) <> " :" <> pack (show c)
193211
194- data EdgeType
212+ data EdgeType term
195213 = Edge Edge
196214 | Slot User
197- | Value Concrete
215+ | Value ( Concrete term )
198216 deriving (Eq , Ord , Show )
199217
200218
201219-- $setup
202220-- >>> :seti -XOverloadedStrings
221+ -- >>> import qualified Data.Core as Core
0 commit comments