Commit 186693e4 authored by Sven Keidel's avatar Sven Keidel Committed by Jente Hidskes

Switch context representation for sort semantics

parent e4d787d8
......@@ -14,7 +14,7 @@ import Prelude hiding (fail,Just,Nothing)
import qualified ConcreteSemantics as C
import SharedSemantics
import Signature hiding (Top)
import SortContext(Context,Signature(..),Sort(Sort),SortId(..),sorts)
import Soundness
import Syntax hiding (Fail)
import Utils
......@@ -53,7 +53,7 @@ import Data.Hashable
import qualified Data.Map as M
import Data.Monoidal
import Data.Order
import Data.Term hiding (wildcard)
import Data.Term
import Data.Text (Text)
import TreeAutomata
......@@ -107,20 +107,20 @@ sortToNonterm sort = case sort of
Sort (SortId nt) -> nt
_ -> error "Parametric polymorphism is not yet supported"
toRhs :: (Constructor,Fun) -> Rhs Constr
toRhs (Constructor constr, Fun sorts _) = Ctor (Constr constr) (map sortToNonterm sorts)
toRhs :: (Constructor,Signature) -> Rhs Constr
toRhs (Constructor constr, Signature ss _) = Ctor (Constr constr) (map sortToNonterm ss)
toProd :: (Sort, [(Constructor,Fun)]) -> (Nonterm, [Rhs Constr])
toProd :: (Sort, [(Constructor,Signature)]) -> (Nonterm, [Rhs Constr])
toProd (sort, rhss) = (sortToNonterm sort, map toRhs rhss)
createGrammar :: Signature -> GrammarBuilder Constr
createGrammar (Signature (_, sorts) _) = grammar startSymbol prods
createGrammar :: Context -> GrammarBuilder Constr
createGrammar ctx = grammar startSymbol prods
where
startSymbol = "Start"
startProd = (startSymbol, map (Eps . sortToNonterm) (LM.keys sorts))
startProd = (startSymbol, map (Eps . sortToNonterm) (LM.keys (sorts ctx)))
-- TODO: what to do with these builtins?
builtins = [("String", [ Ctor (Constr "String") []]) ]
prods = M.fromList $ startProd : map toProd (LM.toList sorts) ++ builtins
prods = M.fromList $ startProd : map toProd (LM.toList (sorts ctx)) ++ builtins
-- Instances -----------------------------------------------------------------------------------------
deriving instance Category (Interp s)
......@@ -182,7 +182,7 @@ instance (PreOrd x, Complete (FreeCompletion x)) => Complete (FreeCompletion [x]
_ _ = Top
instance IsTerm Term (Interp s) where
matchTermAgainstConstructor matchSubterms = proc (Constructor c,ps,Term g) -> do
matchTermAgainstConstructor matchSubterms = proc (Constructor c,ps,Term g) ->
lubA (proc (c',ts) -> case c' of
Constr c'' | c'' == c && eqLength ps ts -> do
ts' <- matchSubterms -< (ps,ts)
......
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Signature(Signature(..), HasSignature(..), Sort(..), Fun(..), SortId(..),
empty, insertType, lookupType, insertSubtype, subtype, inhabitants) where
import Sort
import SubtypeRelation (SubtypeRelation)
import qualified SubtypeRelation as R
import Data.Constructor
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Maybe
import Control.Arrow
type Context = (HashMap Constructor Fun, HashMap Sort [(Constructor,Fun)])
data Signature = Signature Context SubtypeRelation deriving (Show,Eq)
data Fun = Fun [Sort] Sort deriving (Show,Eq)
empty :: Signature
empty = Signature (M.empty, M.empty) R.empty
insertType :: Constructor -> Fun -> Signature -> Signature
insertType con ty@(Fun _ sort) (Signature (cons,sorts) sub) =
Signature (M.insert con ty cons, M.insertWith (\[v] l -> v:l) sort [(con,ty)] sorts) sub
insertSubtype :: Sort -> Sort -> Signature -> Signature
insertSubtype ty1 ty2 (Signature ctx sub) = Signature ctx (R.insert ty1 ty2 sub)
lookupType :: Constructor -> Signature -> Maybe Fun
lookupType c (Signature (cons,_) _) = M.lookup c cons
subtype :: Signature -> Sort -> Sort -> Bool
subtype (Signature _ rel) = R.subtype rel
inhabitants :: Signature -> Sort -> [(Constructor,Fun)]
inhabitants sig@(Signature (_,sorts) rel) s0 = do
s <- R.lower rel s0
case s of
Bottom -> []
Top -> error "Calculating inhabitants from sort top is not allowed"
Coproduct a b -> inhabitants sig a ++ inhabitants sig b
List a -> [("Cons", Fun [a, List a] (List a)), ("Nil", Fun [] (List a))]
Option a -> [("Some", Fun [a] (Option a)), ("None", Fun [] (Option a))]
Tuple as -> [("", Fun as (Tuple as))]
Sort "String" -> [("", Fun [] "String")]
Sort "INT" -> [("", Fun [] "INT")]
Sort x -> fromMaybe (error $ "Sort not found: " ++ show x)
(M.lookup s sorts)
class Arrow c => HasSignature c where
getSignature :: c () Signature
-- instance HasSignature c => PreOrd Sort c where
-- (⊑) = proc (s1,s2) -> do
-- sig <- getSignature -< ()
-- returnA -< subtype sig s1 s2
......@@ -7,10 +7,11 @@ import Data.Text(Text, unpack)
import Data.String(IsString(..))
import Data.Hashable(Hashable(..))
import Data.List(intercalate)
import Data.Abstract.Widening(Widening)
newtype SortId = SortId Text deriving (Show,Eq,Ord,Hashable,IsString)
data Sort = Bottom | Top | Coproduct Sort Sort | List Sort | Option Sort | Tuple [Sort] | Sort SortId deriving (Eq)
data Sort = Bottom | Top | Numerical | Lexical | List Sort | Option Sort | Tuple [Sort] | Sort SortId deriving (Eq)
instance IsString Sort where
fromString = Sort . fromString
......@@ -19,17 +20,19 @@ instance Hashable Sort where
hashWithSalt s x = case x of
Bottom -> s `hashWithSalt` (1::Int)
Top -> s `hashWithSalt` (2::Int)
Coproduct t1 t2 -> s `hashWithSalt` (3::Int) `hashWithSalt` t1 `hashWithSalt` t2
Sort t -> s `hashWithSalt` (4::Int) `hashWithSalt` t
List t -> s `hashWithSalt` (5::Int) `hashWithSalt` t
Option t -> s `hashWithSalt` (6::Int) `hashWithSalt` t
Tuple ts -> s `hashWithSalt` (7::Int) `hashWithSalt` ts
Numerical -> s `hashWithSalt` (3::Int)
Lexical -> s `hashWithSalt` (4::Int)
Sort t -> s `hashWithSalt` (5::Int) `hashWithSalt` t
List t -> s `hashWithSalt` (6::Int) `hashWithSalt` t
Option t -> s `hashWithSalt` (7::Int) `hashWithSalt` t
Tuple ts -> s `hashWithSalt` (8::Int) `hashWithSalt` ts
instance Show Sort where
show x = case x of
Bottom -> "Bottom"
Top -> "Top"
Coproduct s1 s2 -> show s1 ++ "+" ++ show s2
Numerical -> "Int"
Lexical -> "String"
List s -> "List (" ++ show s ++ ")"
Option s -> "Option (" ++ show s ++ ")"
Sort (SortId s) -> unpack s
......@@ -55,3 +58,13 @@ getSortId :: Sort -> Maybe SortId
getSortId s = case s of
Sort i -> Just i
_ -> Nothing
widening :: Int -> Widening Sort
widening n0 _ = go n0
where
go 0 _ = Top
go n s = case s of
List s' -> List (go (n-1) s')
Option s' -> Option (go (n-1) s')
Tuple ss -> Tuple (map (go (n-1)) ss)
_ -> s
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module SortContext(
Context, HasContext(..), Sort(..), Signature(..), SortId(..), empty, signatures, sorts,
fromList, insertSignature, insertSubtype, subtype, lookupSort, lookupCons,
lub, glb, isLexical, isList, isSingleton
) where
import Sort
import SubtypeRelation (SubtypeRelation)
import qualified SubtypeRelation as R
import Data.Constructor
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Maybe
import Data.Foldable
import Control.Arrow
data Signature = Signature [Sort] Sort deriving (Show,Eq)
data Context = Context
{ signatures :: HashMap Constructor [Signature]
, sorts :: HashMap Sort [(Constructor,Signature)]
, subtypes :: SubtypeRelation
} deriving (Show,Eq)
empty :: Context
empty = Context M.empty M.empty R.empty
fromList :: [(Constructor,[Sort],Sort)] -> Context
fromList = foldl (\ctx (c,ss,s) -> insertSignature c (Signature ss s) ctx) empty
insertSignature :: Constructor -> Signature -> Context -> Context
insertSignature con sig@(Signature _ sort) (Context cons sorts sub) =
Context { signatures = M.insertWith (\[v] l -> v:l) con [sig] cons
, sorts = M.insertWith (\[v] l -> v:l) sort [(con,sig)] sorts
, subtypes = sub
}
insertSubtype :: Sort -> Sort -> Context -> Context
insertSubtype ty1 ty2 ctx = ctx { subtypes = R.insert ty1 ty2 (subtypes ctx) }
subtype :: Context -> Sort -> Sort -> Bool
subtype Context {..} = R.subtype subtypes
lub :: Context -> Sort -> Sort -> Sort
lub Context {..} = R.lub subtypes
glb :: Context -> Sort -> Sort -> Sort
glb Context {..} = R.glb subtypes
lookupCons :: Context -> Constructor -> [Signature]
lookupCons Context {..} c = fold $ M.lookup c signatures
lookupSort :: Context -> Sort -> [(Constructor,Signature)]
lookupSort Context {..} s0 = do
s <- R.lower subtypes s0
case s of
Bottom -> []
Top -> error "Calculating inhabitants from sort top is not allowed"
List a -> [("Cons", Signature [a, List a] (List a)), ("Nil", Signature [] (List a))]
Option a -> [("Some", Signature [a] (Option a)), ("None", Signature [] (Option a))]
Tuple as -> [("", Signature as (Tuple as))]
Lexical -> [("", Signature [] Lexical)]
Numerical -> [("", Signature [] Numerical)]
Sort _ -> fromMaybe [] (M.lookup s sorts)
isLexical :: Context -> Sort -> Bool
isLexical ctx = subtype ctx Lexical
isList :: Context -> Sort -> Bool
isList ctx = subtype ctx (List Bottom)
isSingleton :: Context -> Sort -> Bool
isSingleton ctx s = case s of
Bottom -> True
Numerical -> False
Lexical -> False
Sort _ -> length (lookupSort ctx s) == 1
Option _ -> False
List _ -> False
Tuple ss -> all (isSingleton ctx) ss
Top -> False
class Arrow c => HasContext c where
getContext :: c () Context
This diff is collapsed.
module SubtypeRelation(SubtypeRelation,empty,insert,subtype,lower,lub) where
module SubtypeRelation(SubtypeRelation,empty,insert,subtype,lower,lub,glb) where
import Sort
import Utils
......@@ -38,8 +38,8 @@ subtype :: SubtypeRelation -> Sort -> Sort -> Bool
subtype rel@(SubtypeRelation _ _ gr) s1 s2 = case (s1,s2) of
(Bottom,_) -> True
(_,Top) -> True
(x, Coproduct a b) -> subtype rel x a || subtype rel x b
(Coproduct a b, x) -> subtype rel a x && subtype rel b x
(Lexical,Lexical) -> True
(Numerical,Numerical) -> True
(List x,List y) -> subtype rel x y
(Option x,Option y) -> subtype rel x y
(Tuple xs,Tuple ys)
......@@ -54,16 +54,48 @@ subtype rel@(SubtypeRelation _ _ gr) s1 s2 = case (s1,s2) of
(_,_) -> False
lub :: SubtypeRelation -> Sort -> Sort -> Sort
lub rel s1 s2
| subtype rel s1 s2 = s2
| subtype rel s2 s1 = s1
| otherwise = Coproduct s1 s2
lub rel s1 s2 = case (s1,s2) of
(Bottom,_) -> s2
(_,Bottom) -> s1
(Top,_) -> Top
(List x,List y) -> List (lub rel x y)
(Option x,Option y) -> Option (lub rel x y)
(Tuple xs,Tuple ys) -> Tuple (zipWith (lub rel) xs ys)
(Lexical,Lexical) -> Lexical
(Numerical,Numerical) -> Numerical
(Sort _,_)
| subtype rel s1 s2 -> s2
| subtype rel s2 s1 -> s1
(_,Sort _)
| subtype rel s1 s2 -> s2
| subtype rel s2 s1 -> s1
_ -> Top
glb :: SubtypeRelation -> Sort -> Sort -> Sort
glb rel s1 s2 = case (s1,s2) of
(Bottom,_) -> Bottom
(_,Bottom) -> Bottom
(Top,_) -> s2
(_,Top) -> s1
(List x,List y) -> List (glb rel x y)
(Option x,Option y) -> Option (glb rel x y)
(Tuple xs,Tuple ys) -> Tuple (zipWith (glb rel) xs ys)
(Lexical,Lexical) -> Lexical
(Numerical,Numerical) -> Numerical
(Sort _,_)
| subtype rel s1 s2 -> s1
| subtype rel s2 s1 -> s2
(_,Sort _)
| subtype rel s1 s2 -> s1
| subtype rel s2 s1 -> s2
_ -> Bottom
lower :: SubtypeRelation -> Sort -> [Sort]
lower rel@(SubtypeRelation _ _ gr) s = case s of
Bottom -> [Bottom]
Top -> error "lower set of top is unsupported"
Coproduct x y -> [x,y]
Lexical -> return Lexical
Numerical -> return Numerical
List x -> List <$> lower rel x
Option x -> Option <$> lower rel x
Tuple xs -> Tuple <$> permutations (lower rel <$> xs)
......
......@@ -3,8 +3,8 @@
{-# LANGUAGE OverloadedStrings #-}
module Syntax where
import Signature (Signature,Sort,Fun)
import qualified Signature as I
import SortContext (Context,Sort,Signature)
import qualified SortContext as I
import Control.Monad.Except
......@@ -53,7 +53,7 @@ data TermPattern
-- | Stratego source code is organized in modules consisting of a
-- signature describing possible shapes of terms and named strategies.
data Module = Module Signature Strategies deriving (Show,Eq)
data Module = Module Context Strategies deriving (Show,Eq)
type Strategies = HashMap StratVar Strategy
......@@ -78,7 +78,7 @@ leftChoice f = GuardedChoice f Id
stratEnv :: Module -> StratEnv
stratEnv (Module _ senv) = fmap (`Closure` M.empty) senv
signature :: Module -> Signature
signature :: Module -> Context
signature (Module sig _) = sig
patternVars :: TermPattern -> Set TermVar
......@@ -106,12 +106,12 @@ parseModule t = case t of
Module <$> parseSignature sig <*> (M.fromList <$> traverse parseStrategy strats)
_ -> throwError $ "unexpected input while parsing module from aterm: " ++ show t
parseSignature :: MonadError String m => ATerm -> m Signature
parseSignature :: MonadError String m => ATerm -> m Context
parseSignature s = case s of
ATerm "Signature" [List sig] -> parseConstructors sig I.empty
_ -> throwError $ "unexpected input while parsing signature from aterm: " ++ show s
where
parseConstructors :: MonadError String m => [ATerm] -> Signature -> m Signature
parseConstructors :: MonadError String m => [ATerm] -> Context -> m Context
parseConstructors ts sig = case ts of
ATerm "Constructors" [List constrs]:rest -> do
sig' <- foldM parseDeclaration sig constrs
......@@ -119,13 +119,13 @@ parseSignature s = case s of
[] -> return sig
_ -> throwError $ "unexpected input while parsing signature from aterm: " ++ show ts
parseDeclaration :: MonadError String m => Signature -> ATerm -> m Signature
parseDeclaration :: MonadError String m => Context -> ATerm -> m Context
parseDeclaration sig t
| containsSortVar t = return sig
| otherwise = case t of
ATerm "OpDecl" [String con, body] -> do
typ <- parseFun body
return $ I.insertType (Constructor con) typ sig
return $ I.insertSignature (Constructor con) typ sig
ATerm "OpDeclInj" [f@(ATerm "FunType" [_, ATerm "ConstType" [ATerm "SortTuple" _]])] ->
parseDeclaration sig $ ATerm "OpDecl" [String "", f]
ATerm "OpDeclInj" [ATerm "FunType" [List[ty1], ty2]] ->
......@@ -140,10 +140,10 @@ parseDeclaration sig t
containsSortVar (List ts) = any containsSortVar ts
containsSortVar _ = False
parseFun :: MonadError String m => ATerm -> m Fun
parseFun :: MonadError String m => ATerm -> m Signature
parseFun t = case t of
ATerm "ConstType" [res] -> I.Fun [] <$> parseSort res
ATerm "FunType" [List args,res] -> I.Fun <$> traverse parseSort args <*> parseSort res
ATerm "ConstType" [res] -> I.Signature [] <$> parseSort res
ATerm "FunType" [List args,res] -> I.Signature <$> traverse parseSort args <*> parseSort res
_ -> throwError $ "unexpected input while parsing function type from aterm: " ++ show t
parseSort :: MonadError String m => ATerm -> m Sort
......
......@@ -23,7 +23,7 @@ library
Data.Constructor,
Data.Term,
Syntax,
Signature,
SortContext,
Utils,
SubtypeRelation,
Sort,
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment