...
 
Commits (31)
......@@ -12,6 +12,9 @@ import Control.Monad.Except (MonadError)
import qualified Control.Monad.Except as M
import Data.Profunctor
import GHC.Exts(IsString(..))
-- | Arrow-based interface for computations that can fail.
class (Arrow c, Profunctor c) => ArrowFail e c | c -> e where
......@@ -25,3 +28,6 @@ instance MonadError e m => ArrowFail e (Kleisli m) where
-- | Simpler version of 'fail'.
fail' :: ArrowFail () c => c a b
fail' = arr (const ()) >>> fail
failString :: (ArrowFail e c, IsString e) => c String x
failString = fromString ^>> fail
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Abstract.Constructor(Constr,isEmpty,isSingleton,widening) where
import Control.DeepSeq
import Data.Order
import Data.Hashable
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.IntMap (IntMap)
import qualified Data.IntMap as IM
import Data.Text (Text)
import Data.Identifiable
import Data.Abstract.Widening
import Data.Abstract.Stable
import GHC.Exts
newtype Constr n = Constr (HashMap Text (IntMap [n])) deriving (Eq,Hashable,NFData)
instance (Identifiable n, Complete n, Show n) => Show (Constr n) where
show cs = show (toList cs)
instance PreOrd n => PreOrd (Constr n) where
Constr m1 Constr m2 =
(m1 `subsetKeys` m2) && forAll (M.intersectionWith (,) m1 m2) (\(a1,a2) ->
(a1 `subsetKeys'` a2) && forAll (IM.intersectionWith (,) a1 a2) (\(ts1,ts2) ->
ts1 ts2))
instance Complete n => Complete (Constr n) where
Constr m1 Constr m2 = Constr (M.unionWith (IM.unionWith (zipWith ())) m1 m2)
widening :: (Identifiable n,Complete n) => Widening n -> Widening (Constr n)
widening w c1@(Constr m1) c2@(Constr m2) =
( if size c1 < size c2 then Unstable else fst (sequenceA (M.intersectionWith (sequenceA <.> IM.intersectionWith (sequenceA <.> zipWith w)) m1 m2))
, c1 c2)
where
(<.>) = (.) . (.)
infixr 9 <.>
instance PreOrd n => LowerBounded (Constr n) where
bottom = Constr M.empty
instance CoComplete n => CoComplete (Constr n) where
Constr m1 Constr m2 = removeEmpty $ Constr (M.intersectionWith (IM.intersectionWith (zipWith ())) m1 m2)
instance (Identifiable n, Complete n) => IsList (Constr n) where
type Item (Constr n) = (Text,[n])
fromList l = Constr $ M.fromListWith (IM.unionWith (zipWith ())) [ (c, IM.singleton (length ts) ts) | (c,ts) <- l]
toList (Constr n) = [ (c,ts) | (c,tss) <- M.toList n, ts <- IM.elems tss ]
instance Hashable n => Hashable (IntMap n) where
hashWithSalt s m = hashWithSalt s (IM.toList m)
isEmpty :: Constr n -> Bool
isEmpty (Constr n) = M.null n
isSingleton :: (n -> Bool) -> Constr n -> Bool
isSingleton isSing (Constr n) = M.size n == 1 && forAll n (\a -> IM.size a == 1 && forAll a (\l -> all isSing l))
size :: (Identifiable n, Complete n) => Constr n -> Int
size c = length (toList c)
removeEmpty :: Constr n -> Constr n
removeEmpty (Constr m) = Constr (M.mapMaybe (\a -> if IM.null a then Nothing else Just a) m)
forAll :: Foldable t => t a -> (a -> Bool) -> Bool
forAll l p = all p l
subsetKeys :: Identifiable a => HashMap a b -> HashMap a b' -> Bool
subsetKeys m1 m2 = all (`M.member` m2) (M.keys m1)
subsetKeys' :: IntMap a -> IntMap a' -> Bool
subsetKeys' m1 m2 = all (`IM.member` m2) (IM.keys m1)
......@@ -67,7 +67,7 @@ instance Functor Maybe where
fmap f m = case m of
Just a -> Just (f a)
Nothing -> Nothing
JustNothing a -> Just (f a)
JustNothing a -> JustNothing (f a)
instance Applicative Maybe where
pure = return
......@@ -93,5 +93,11 @@ instance Traversable Maybe where
fromConcreteMaybe :: Con.Maybe a -> Maybe a
fromConcreteMaybe m = case m of
Con.Just a -> Just a
Con.Nothing -> Nothing
Con.Just a -> Just a
Con.Nothing -> Nothing
toConcreteMaybe :: Maybe a -> Con.Maybe a
toConcreteMaybe m = case m of
Just a -> Con.Just a
JustNothing a -> Con.Just a
Nothing -> Con.Nothing
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveGeneric #-}
module Data.Abstract.Singleton where
import Data.Hashable
import Data.Order
import GHC.Generics (Generic)
data Singleton a = Single a | Any deriving (Eq, Functor, Foldable, Traversable, Generic)
instance Eq a => PreOrd (Singleton a) where
_ Any = True
Single a Single b = a == b
_ _ = False
instance (Hashable a) => Hashable (Singleton a)
instance Eq a => Complete (Singleton a) where
Single a Single b | a == b = Single a
_ _ = Any
instance Eq a => UpperBounded (Singleton a) where
top = Any
instance Show a => Show (Singleton a) where
show (Single a) = "Single " ++ show a
show Any = "NonSingle"
allSingle :: [Singleton a] -> Maybe [a]
allSingle = mapM (\s -> case s of
Single a -> Just a
Any -> Nothing)
......@@ -40,10 +40,17 @@ instance (Identifiable a, Complete b) => Complete (Map a b) where
instance Empty.IsEmpty (Map a b) where
empty = Map M.empty
instance (Identifiable a, PreOrd b) => UpperBounded (Map a b) where
top = Top
keys :: Map a b -> Maybe (HashSet a)
keys Top = Nothing
keys (Map m) = Just (M.keysSet m)
instance Identifiable a => Functor (Map a) where
fmap _ Top = Top
fmap f (Map m) = Map (M.map f m)
widening :: Identifiable a => Widening b -> Widening (Map a b)
widening _ Top Top = (Stable,Top)
widening w (Map m1) (Map m2) | M.keys m1 == M.keys m2 = second Map $ sequenceA $ M.intersectionWith w m1 m2
......@@ -68,7 +75,7 @@ lookup' a = lookup a top
delete :: (Identifiable a, Foldable f) => f a -> Map a b -> Map a b
delete _ Top = Top
delete ks (Map m) = Map (foldr M.delete m ks)
delete as (Map m) = Map (foldr M.delete m as)
filter :: (a -> Bool) -> Map a b -> Map a b
filter _ Top = Top
......
......@@ -10,6 +10,7 @@ module Data.Abstract.TreeGrammar.Terminal(Terminal(..), map, Constr) where
import Prelude hiding (pred,traverse,map,Either(..))
import Control.Monad
import Control.DeepSeq
import Data.Text (Text)
import Data.IntMap (IntMap)
......@@ -44,7 +45,10 @@ class Terminal t where
map :: (Identifiable n', Terminal t) => (n -> n') -> t n -> t n'
map f t = runIdentity (traverse (Identity . f) t)
newtype Constr n = Constr (HashMap Text (IntMap (HashSet [n]))) deriving (Eq)
newtype Constr n = Constr (HashMap Text (IntMap (HashSet [n]))) deriving (Eq,NFData)
instance (Eq n, Hashable n) => Hashable (Constr n) where
hashWithSalt s t = runIdentity (hashWithSalt (\s' -> Identity . Hash.hashWithSalt s') s t)
instance Identifiable n => IsList (Constr n) where
type Item (Constr n) = (Text,[n])
......
......@@ -18,7 +18,18 @@ import Data.Maybe (mapMaybe)
import Text.Printf
newtype Map a b = Map (HashMap a (A.Maybe b)) deriving (Eq,Hashable,NFData)
newtype Map a b = Map (HashMap a (A.Maybe b)) deriving (NFData)
instance (Eq a, Eq b, Hashable a, UpperBounded b) => Eq (Map a b) where
m1 == m2 = let Map m1' = normalize m1
Map m2' = normalize m2
in m1' == m2'
instance (Eq a, Eq b, Hashable a, UpperBounded b, Hashable b) => Hashable (Map a b) where
hashWithSalt s m = let Map m' = normalize m in hashWithSalt s m'
normalize :: (UpperBounded b, Eq b) => Map a b -> Map a b
normalize (Map m) = Map (M.filter (\v -> v /= A.JustNothing top) m)
instance (Identifiable a, PreOrd b) => PreOrd (Map a b) where
() = withMap2 $ \m1 m2 -> all (\(k,v) -> M.lookup k m1 Just v) (M.toList m2)
......@@ -36,6 +47,9 @@ instance (Show a,Show b) => Show (Map a b) where
A.Nothing -> printf "%s❌," (show k)
A.JustNothing x -> printf "%s? -> %s," (show k) (show x)
instance Identifiable a => Functor (Map a) where
fmap f = withMap (fmap (fmap f))
widening :: Identifiable a => Widening b -> Widening (Map a b)
widening w = withMap2 $ \m1 m2 -> sequenceA $ M.intersectionWith (A.widening w) m1 m2
......
......@@ -60,8 +60,12 @@ class PreOrd x => CoComplete x where
class PreOrd x => UpperBounded x where
top :: x
glb :: (Foldable f, CoComplete x) => f x -> x
glb = foldr1 ()
glb1 :: (Foldable f, CoComplete x) => f x -> x
glb1 = foldr1 ()
glb :: (CoComplete x) => x -> [x] -> x
glb x [] = x
glb _ l = glb1 l
instance (PreOrd e, PreOrd a) => PreOrd (Either e a) where
Left e1 Left e2 = e1 e2
......
......@@ -13,7 +13,7 @@ import qualified SortContext as Ctx
import qualified Data.Abstract.Map as S
import qualified Data.HashMap.Lazy as M
import Data.TermEnvironment
import Criterion
import Criterion.Main
......@@ -21,6 +21,7 @@ import Criterion.Main
main :: IO ()
main = do
pcf <- CaseStudy.pcf
arrows <- CaseStudy.arrows
defaultMain [
bgroup "Sort Semantics" [
bench "reduce Add(Zero,y)" $
......@@ -39,6 +40,14 @@ main = do
let ?ctx = signature pcf in
let senv = stratEnv pcf
in nf (eval 5 10 (Call "eval_0_0" [] []) senv ?ctx emptyEnv) (term (Tuple [List (Tuple [Lexical, "Val"]), "Exp"]))
,
bench "arrows" $
let ?ctx = signature arrows in
let senv = stratEnv arrows
input = term "ArrCommand"
val = term "Exp"
env = termEnv [("vars-list", term $ List "Var")]
in nf (eval 4 10 (Call "desugar_arrow_p__0_1" [] [TermVar "vars-list"]) senv ?ctx env) input
]
]
where
......@@ -48,9 +57,13 @@ main = do
numerical :: (?ctx :: Context) => Term
numerical = term Numerical
emptyEnv :: TermEnv
emptyEnv :: TermEnv Term
emptyEnv = S.empty
termEnv :: [(TermVar, Term)] -> TermEnv Term
termEnv = S.fromList
map' = Strategy ["f"] ["l"] (Scope ["x","xs","x'","xs'"] (
Build "l" `Seq`
GuardedChoice
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -585,19 +585,13 @@ rules
[p|ps] -> TuplePat(p, ps)
tuple = map(?VarVar(v);!Var(v)); tuple-exp
tuple = map(\ VarVar(v) -> Var(v) \); tuple-exp
tuple-exp :
[] -> Constr(Unit())
tuple-exp : [] -> Constr(Unit())
tuple-exp : [e] -> e
tuple-exp : [e|es] -> Product(ECons(e, es))
tuple-exp :
[e] -> e
tuple-exp :
[e|es] -> Product(ECons(e, es))
free-pat-vars =
collect-all(?VarVar(_))
free-pat-vars = collect-all(?VarVar(_))
free-decls-vars =
collect-all(
......@@ -621,11 +615,10 @@ rules
, cs
)
map(s) =
rec x([] + [s | x])
map(s): [] -> []
map(s): [x|xs] -> [<s>(x) | <map(s)>(xs)]
collect-all(s) =
collect-all(s, union)
collect-all(s) = collect-all(s, union)
collect-all(s,un) =
rec x(
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
Specification([Signature([Constructors([OpDecl("Zero",ConstType(SortNoArgs("NExp"))),OpDecl("One",ConstType(SortNoArgs("NExp"))),OpDecl("Max",FunType([ConstType(SortNoArgs("NExp")),ConstType(SortNoArgs("NExp"))],ConstType(SortNoArgs("NExp")))),OpDecl("Min",FunType([ConstType(SortNoArgs("NExp")),ConstType(SortNoArgs("NExp"))],ConstType(SortNoArgs("NExp")))),OpDecl("True",ConstType(SortNoArgs("BExp"))),OpDecl("False",ConstType(SortNoArgs("BExp"))),OpDecl("And",FunType([ConstType(SortNoArgs("BExp")),ConstType(SortNoArgs("BExp"))],ConstType(SortNoArgs("BExp")))),OpDecl("Or",FunType([ConstType(SortNoArgs("BExp")),ConstType(SortNoArgs("BExp"))],ConstType(SortNoArgs("BExp")))),OpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),OpDecl("Cons",FunType([ConstType(SortVar("a")),ConstType(Sort("List",[SortVar("a")]))],ConstType(Sort("List",[SortVar("a")])))),OpDeclInj(ConstType(SortTuple([]))),OpDeclInj(FunType([ConstType(SortVar("a"))],ConstType(SortTuple([SortVar("a")])))),OpDeclInj(FunType([ConstType(SortVar("a")),ConstType(SortVar("b"))],ConstType(SortTuple([SortVar("a"),SortVar("b")])))),OpDeclInj(FunType([ConstType(SortVar("a")),ConstType(SortVar("b")),ConstType(SortVar("c"))],ConstType(SortTuple([SortVar("a"),SortVar("b"),SortVar("c")]))))])]),Strategies([RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("True",[])),NoAnnoList(Op("One",[])))),RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("False",[])),NoAnnoList(Op("Zero",[])))),RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("And",[Var("e1"),Var("e2")])),NoAnnoList(Op("Min",[Var("e1"),Var("e2")])))),RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("Or",[Var("e1"),Var("e2")])),NoAnnoList(Op("Max",[Var("e1"),Var("e2")])))),SDef("topdown",[DefaultVarDec("s")],Seq(CallNoArgs(SVar("s")),All(Call(SVar("topdown"),[CallNoArgs(SVar("s"))])))),SDef("bottomup",[DefaultVarDec("s")],Seq(All(Call(SVar("bottomup"),[CallNoArgs(SVar("s"))])),CallNoArgs(SVar("s")))),SDefNoArgs("trans_topdown",Call(SVar("topdown"),[CallNoArgs(SVar("trans"))])),SDefNoArgs("trans_bottomup",Call(SVar("bottomup"),[CallNoArgs(SVar("trans"))]))])])
\ No newline at end of file
Specification([Signature([Constructors([OpDecl("Zero",ConstType(SortNoArgs("NExp"))),OpDecl("One",ConstType(SortNoArgs("NExp"))),OpDecl("Max",FunType([ConstType(SortNoArgs("NExp")),ConstType(SortNoArgs("NExp"))],ConstType(SortNoArgs("NExp")))),OpDecl("Min",FunType([ConstType(SortNoArgs("NExp")),ConstType(SortNoArgs("NExp"))],ConstType(SortNoArgs("NExp")))),OpDecl("True",ConstType(SortNoArgs("BExp"))),OpDecl("False",ConstType(SortNoArgs("BExp"))),OpDecl("And",FunType([ConstType(SortNoArgs("BExp")),ConstType(SortNoArgs("BExp"))],ConstType(SortNoArgs("BExp")))),OpDecl("Or",FunType([ConstType(SortNoArgs("BExp")),ConstType(SortNoArgs("BExp"))],ConstType(SortNoArgs("BExp")))),OpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),OpDecl("Cons",FunType([ConstType(SortVar("a")),ConstType(Sort("List",[SortVar("a")]))],ConstType(Sort("List",[SortVar("a")])))),OpDeclInj(ConstType(SortTuple([]))),OpDeclInj(FunType([ConstType(SortVar("a"))],ConstType(SortTuple([SortVar("a")])))),OpDeclInj(FunType([ConstType(SortVar("a")),ConstType(SortVar("b"))],ConstType(SortTuple([SortVar("a"),SortVar("b")])))),OpDeclInj(FunType([ConstType(SortVar("a")),ConstType(SortVar("b")),ConstType(SortVar("c"))],ConstType(SortTuple([SortVar("a"),SortVar("b"),SortVar("c")]))))])]),Strategies([SDefT("trans_0_0",[],[],GuardedLChoice(Seq(Match(Anno(Op("True",[]),Wld())),Build(Anno(Op("One",[]),Op("Nil",[])))),Id(),GuardedLChoice(Seq(Match(Anno(Op("False",[]),Wld())),Build(Anno(Op("Zero",[]),Op("Nil",[])))),Id(),GuardedLChoice(Scope(["a_1","b_1"],Seq(Match(Anno(Op("And",[Var("a_1"),Var("b_1")]),Wld())),Build(Anno(Op("Min",[Var("a_1"),Var("b_1")]),Op("Nil",[]))))),Id(),Scope(["y_0","z_0"],Seq(Match(Anno(Op("Or",[Var("y_0"),Var("z_0")]),Wld())),Build(Anno(Op("Max",[Var("y_0"),Var("z_0")]),Op("Nil",[]))))))))),SDefT("topdown_1_0",[VarDec("c_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(CallT(SVar("c_1"),[],[]),All(CallT(SVar("topdown_1_0"),[CallT(SVar("c_1"),[],[])],[])))),SDefT("bottomup_1_0",[VarDec("d_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(All(CallT(SVar("bottomup_1_0"),[CallT(SVar("d_1"),[],[])],[])),CallT(SVar("d_1"),[],[]))),SDefT("trans__topdown_0_0",[],[],CallT(SVar("topdown_1_0"),[CallT(SVar("trans_0_0"),[],[])],[])),SDefT("trans__bottomup_0_0",[],[],CallT(SVar("bottomup_1_0"),[CallT(SVar("trans_0_0"),[],[])],[])),SDefT("Anno__Cong_____2_0",[VarDec("i_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("j_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["e_1","f_1","g_1","h_1"],Seq(Match(Anno(Var("e_1"),Var("f_1"))),Seq(Build(Var("e_1")),Seq(CallT(SVar("i_1"),[],[]),Seq(Match(Var("g_1")),Seq(Build(Var("f_1")),Seq(CallT(SVar("j_1"),[],[]),Seq(Match(Var("h_1")),Build(Anno(Var("g_1"),Var("h_1")))))))))))),SDefT("Zero_0_0",[],[],Match(Anno(Op("Zero",[]),Wld()))),SDefT("One_0_0",[],[],Match(Anno(Op("One",[]),Wld()))),SDefT("Max_2_0",[VarDec("k_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("l_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["d_2","b_2","c_2","e_2","f_2"],Seq(Match(Anno(Op("Max",[Var("b_2"),Var("c_2")]),Var("d_2"))),Seq(Build(Var("b_2")),Seq(CallT(SVar("k_1"),[],[]),Seq(Match(Var("e_2")),Seq(Build(Var("c_2")),Seq(CallT(SVar("l_1"),[],[]),Seq(Match(Var("f_2")),Build(Anno(Op("Max",[Var("e_2"),Var("f_2")]),Var("d_2")))))))))))),SDefT("Min_2_0",[VarDec("m_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("n_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["i_2","g_2","h_2","j_2","k_2"],Seq(Match(Anno(Op("Min",[Var("g_2"),Var("h_2")]),Var("i_2"))),Seq(Build(Var("g_2")),Seq(CallT(SVar("m_1"),[],[]),Seq(Match(Var("j_2")),Seq(Build(Var("h_2")),Seq(CallT(SVar("n_1"),[],[]),Seq(Match(Var("k_2")),Build(Anno(Op("Min",[Var("j_2"),Var("k_2")]),Var("i_2")))))))))))),SDefT("True_0_0",[],[],Match(Anno(Op("True",[]),Wld()))),SDefT("False_0_0",[],[],Match(Anno(Op("False",[]),Wld()))),SDefT("And_2_0",[VarDec("o_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("p_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["n_2","l_2","m_2","o_2","p_2"],Seq(Match(Anno(Op("And",[Var("l_2"),Var("m_2")]),Var("n_2"))),Seq(Build(Var("l_2")),Seq(CallT(SVar("o_1"),[],[]),Seq(Match(Var("o_2")),Seq(Build(Var("m_2")),Seq(CallT(SVar("p_1"),[],[]),Seq(Match(Var("p_2")),Build(Anno(Op("And",[Var("o_2"),Var("p_2")]),Var("n_2")))))))))))),SDefT("Or_2_0",[VarDec("q_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("r_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["s_2","q_2","r_2","t_2","u_2"],Seq(Match(Anno(Op("Or",[Var("q_2"),Var("r_2")]),Var("s_2"))),Seq(Build(Var("q_2")),Seq(CallT(SVar("q_1"),[],[]),Seq(Match(Var("t_2")),Seq(Build(Var("r_2")),Seq(CallT(SVar("r_1"),[],[]),Seq(Match(Var("u_2")),Build(Anno(Op("Or",[Var("t_2"),Var("u_2")]),Var("s_2")))))))))))),SDefT("Nil_0_0",[],[],Match(Anno(Op("Nil",[]),Wld()))),SDefT("Cons_2_0",[VarDec("s_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("t_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["x_2","v_2","w_2","y_2","z_2"],Seq(Match(Anno(Op("Cons",[Var("v_2"),Var("w_2")]),Var("x_2"))),Seq(Build(Var("v_2")),Seq(CallT(SVar("s_1"),[],[]),Seq(Match(Var("y_2")),Seq(Build(Var("w_2")),Seq(CallT(SVar("t_1"),[],[]),Seq(Match(Var("z_2")),Build(Anno(Op("Cons",[Var("y_2"),Var("z_2")]),Var("x_2")))))))))))),SDefT("_0_0",[],[],Match(Anno(Op("",[]),Wld()))),SDefT("_1_0",[VarDec("u_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["b_3","a_3","c_3"],Seq(Match(Anno(Op("",[Var("a_3")]),Var("b_3"))),Seq(Build(Var("a_3")),Seq(CallT(SVar("u_1"),[],[]),Seq(Match(Var("c_3")),Build(Anno(Op("",[Var("c_3")]),Var("b_3"))))))))),SDefT("_2_0",[VarDec("v_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("w_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["f_3","d_3","e_3","g_3","h_3"],Seq(Match(Anno(Op("",[Var("d_3"),Var("e_3")]),Var("f_3"))),Seq(Build(Var("d_3")),Seq(CallT(SVar("v_1"),[],[]),Seq(Match(Var("g_3")),Seq(Build(Var("e_3")),Seq(CallT(SVar("w_1"),[],[]),Seq(Match(Var("h_3")),Build(Anno(Op("",[Var("g_3"),Var("h_3")]),Var("f_3")))))))))))),SDefT("_3_0",[VarDec("x_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("y_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("z_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["l_3","i_3","j_3","k_3","m_3","n_3","o_3"],Seq(Match(Anno(Op("",[Var("i_3"),Var("j_3"),Var("k_3")]),Var("l_3"))),Seq(Build(Var("i_3")),Seq(CallT(SVar("x_1"),[],[]),Seq(Match(Var("m_3")),Seq(Build(Var("j_3")),Seq(CallT(SVar("y_1"),[],[]),Seq(Match(Var("n_3")),Seq(Build(Var("k_3")),Seq(CallT(SVar("z_1"),[],[]),Seq(Match(Var("o_3")),Build(Anno(Op("",[Var("m_3"),Var("n_3"),Var("o_3")]),Var("l_3"))))))))))))))),SDefT("DR__UNDEFINE_1_0",[VarDec("a_2",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["q_3","p_3","r_3"],Seq(Match(Anno(Op("DR_UNDEFINE",[Var("p_3")]),Var("q_3"))),Seq(Build(Var("p_3")),Seq(CallT(SVar("a_2"),[],[]),Seq(Match(Var("r_3")),Build(Anno(Op("DR_UNDEFINE",[Var("r_3")]),Var("q_3"))))))))),SDefT("DR__DUMMY_0_0",[],[],Match(Anno(Op("DR_DUMMY",[]),Wld())))])])
This diff is collapsed.
Specification([Signature([Constructors([OpDecl("Zero",ConstType(Sort("NExp",[]))),OpDecl("One",ConstType(Sort("NExp",[]))),OpDecl("Max",FunType([ConstType(Sort("NExp",[])),ConstType(Sort("NExp",[]))],ConstType(Sort("NExp",[])))),OpDecl("Min",FunType([ConstType(Sort("NExp",[])),ConstType(Sort("NExp",[]))],ConstType(Sort("NExp",[])))),OpDecl("True",ConstType(Sort("BExp",[]))),OpDecl("False",ConstType(Sort("BExp",[]))),OpDecl("And",FunType([ConstType(Sort("BExp",[])),ConstType(Sort("BExp",[]))],ConstType(Sort("BExp",[])))),OpDecl("Or",FunType([ConstType(Sort("BExp",[])),ConstType(Sort("BExp",[]))],ConstType(Sort("BExp",[])))),OpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),OpDecl("Cons",FunType([ConstType(SortVar("a")),ConstType(Sort("List",[SortVar("a")]))],ConstType(Sort("List",[SortVar("a")])))),OpDecl("DR_UNDEFINE",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),OpDecl("DR_DUMMY",ConstType(Sort("ATerm",[]))),OpDecl("",ConstType(Sort("Tuple",[Sort("Nil",[])]))),OpDecl("",FunType([ConstType(SortVar("a"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Nil",[])])])))),OpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Nil",[])])])])))),OpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b")),ConstType(SortVar("c"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Cons",[SortVar("c"),Sort("Nil",[])])])])]))))])]),Strategies([SDefT("trans_0_0",[],[],GuardedLChoice(Seq(Match(Anno(Op("True",[]),Wld)),Build(Anno(Op("One",[]),Op("Nil",[])))),Id,GuardedLChoice(Seq(Match(Anno(Op("False",[]),Wld)),Build(Anno(Op("Zero",[]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["a_1","b_1"],Seq(Match(Anno(Op("And",[Var("a_1"),Var("b_1")]),Wld)),Build(Anno(Op("Min",[Var("a_1"),Var("b_1")]),Op("Nil",[]))))),Id,Scope(["y_0","z_0"],Seq(Match(Anno(Op("Or",[Var("y_0"),Var("z_0")]),Wld)),Build(Anno(Op("Max",[Var("y_0"),Var("z_0")]),Op("Nil",[]))))))))),SDefT("topdown_1_0",[VarDec("c_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(CallT(SVar("c_1"),[],[]),All(CallT(SVar("topdown_1_0"),[CallT(SVar("c_1"),[],[])],[])))),SDefT("bottomup_1_0",[VarDec("d_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(All(CallT(SVar("bottomup_1_0"),[CallT(SVar("d_1"),[],[])],[])),CallT(SVar("d_1"),[],[]))),SDefT("trans__topdown_0_0",[],[],CallT(SVar("topdown_1_0"),[CallT(SVar("trans_0_0"),[],[])],[])),SDefT("trans__bottomup_0_0",[],[],CallT(SVar("bottomup_1_0"),[CallT(SVar("trans_0_0"),[],[])],[])),SDefT("Anno__Cong_____2_0",[VarDec("i_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("j_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["e_1","f_1","g_1","h_1"],Seq(Match(Anno(Var("e_1"),Var("f_1"))),Seq(Build(Var("e_1")),Seq(CallT(SVar("i_1"),[],[]),Seq(Match(Var("g_1")),Seq(Build(Var("f_1")),Seq(CallT(SVar("j_1"),[],[]),Seq(Match(Var("h_1")),Build(Anno(Var("g_1"),Var("h_1")))))))))))),SDefT("Zero_0_0",[],[],Match(Anno(Op("Zero",[]),Wld))),SDefT("One_0_0",[],[],Match(Anno(Op("One",[]),Wld))),SDefT("Max_2_0",[VarDec("k_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("l_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["d_2","b_2","c_2","e_2","f_2"],Seq(Match(Anno(Op("Max",[Var("b_2"),Var("c_2")]),Var("d_2"))),Seq(Build(Var("b_2")),Seq(CallT(SVar("k_1"),[],[]),Seq(Match(Var("e_2")),Seq(Build(Var("c_2")),Seq(CallT(SVar("l_1"),[],[]),Seq(Match(Var("f_2")),Build(Anno(Op("Max",[Var("e_2"),Var("f_2")]),Var("d_2")))))))))))),SDefT("Min_2_0",[VarDec("m_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("n_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["i_2","g_2","h_2","j_2","k_2"],Seq(Match(Anno(Op("Min",[Var("g_2"),Var("h_2")]),Var("i_2"))),Seq(Build(Var("g_2")),Seq(CallT(SVar("m_1"),[],[]),Seq(Match(Var("j_2")),Seq(Build(Var("h_2")),Seq(CallT(SVar("n_1"),[],[]),Seq(Match(Var("k_2")),Build(Anno(Op("Min",[Var("j_2"),Var("k_2")]),Var("i_2")))))))))))),SDefT("True_0_0",[],[],Match(Anno(Op("True",[]),Wld))),SDefT("False_0_0",[],[],Match(Anno(Op("False",[]),Wld))),SDefT("And_2_0",[VarDec("o_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("p_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["n_2","l_2","m_2","o_2","p_2"],Seq(Match(Anno(Op("And",[Var("l_2"),Var("m_2")]),Var("n_2"))),Seq(Build(Var("l_2")),Seq(CallT(SVar("o_1"),[],[]),Seq(Match(Var("o_2")),Seq(Build(Var("m_2")),Seq(CallT(SVar("p_1"),[],[]),Seq(Match(Var("p_2")),Build(Anno(Op("And",[Var("o_2"),Var("p_2")]),Var("n_2")))))))))))),SDefT("Or_2_0",[VarDec("q_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("r_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["s_2","q_2","r_2","t_2","u_2"],Seq(Match(Anno(Op("Or",[Var("q_2"),Var("r_2")]),Var("s_2"))),Seq(Build(Var("q_2")),Seq(CallT(SVar("q_1"),[],[]),Seq(Match(Var("t_2")),Seq(Build(Var("r_2")),Seq(CallT(SVar("r_1"),[],[]),Seq(Match(Var("u_2")),Build(Anno(Op("Or",[Var("t_2"),Var("u_2")]),Var("s_2")))))))))))),SDefT("Nil_0_0",[],[],Match(Anno(Op("Nil",[]),Wld))),SDefT("Cons_2_0",[VarDec("s_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("t_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["x_2","v_2","w_2","y_2","z_2"],Seq(Match(Anno(Op("Cons",[Var("v_2"),Var("w_2")]),Var("x_2"))),Seq(Build(Var("v_2")),Seq(CallT(SVar("s_1"),[],[]),Seq(Match(Var("y_2")),Seq(Build(Var("w_2")),Seq(CallT(SVar("t_1"),[],[]),Seq(Match(Var("z_2")),Build(Anno(Op("Cons",[Var("y_2"),Var("z_2")]),Var("x_2")))))))))))),SDefT("_0_0",[],[],Match(Anno(Op("",[]),Wld))),SDefT("_1_0",[VarDec("u_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["b_3","a_3","c_3"],Seq(Match(Anno(Op("",[Var("a_3")]),Var("b_3"))),Seq(Build(Var("a_3")),Seq(CallT(SVar("u_1"),[],[]),Seq(Match(Var("c_3")),Build(Anno(Op("",[Var("c_3")]),Var("b_3"))))))))),SDefT("_2_0",[VarDec("v_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("w_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["f_3","d_3","e_3","g_3","h_3"],Seq(Match(Anno(Op("",[Var("d_3"),Var("e_3")]),Var("f_3"))),Seq(Build(Var("d_3")),Seq(CallT(SVar("v_1"),[],[]),Seq(Match(Var("g_3")),Seq(Build(Var("e_3")),Seq(CallT(SVar("w_1"),[],[]),Seq(Match(Var("h_3")),Build(Anno(Op("",[Var("g_3"),Var("h_3")]),Var("f_3")))))))))))),SDefT("_3_0",[VarDec("x_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("y_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("z_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["l_3","i_3","j_3","k_3","m_3","n_3","o_3"],Seq(Match(Anno(Op("",[Var("i_3"),Var("j_3"),Var("k_3")]),Var("l_3"))),Seq(Build(Var("i_3")),Seq(CallT(SVar("x_1"),[],[]),Seq(Match(Var("m_3")),Seq(Build(Var("j_3")),Seq(CallT(SVar("y_1"),[],[]),Seq(Match(Var("n_3")),Seq(Build(Var("k_3")),Seq(CallT(SVar("z_1"),[],[]),Seq(Match(Var("o_3")),Build(Anno(Op("",[Var("m_3"),Var("n_3"),Var("o_3")]),Var("l_3"))))))))))))))),SDefT("DR__UNDEFINE_1_0",[VarDec("a_2",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Scope(["q_3","p_3","r_3"],Seq(Match(Anno(Op("DR_UNDEFINE",[Var("p_3")]),Var("q_3"))),Seq(Build(Var("p_3")),Seq(CallT(SVar("a_2"),[],[]),Seq(Match(Var("r_3")),Build(Anno(Op("DR_UNDEFINE",[Var("r_3")]),Var("q_3"))))))))),SDefT("DR__DUMMY_0_0",[],[],Match(Anno(Op("DR_DUMMY",[]),Wld)))])])
\ No newline at end of file
module balg
signature
constructors
Zero : NExp
One : NExp
Max : NExp * NExp -> NExp
Min : NExp * NExp -> NExp
True : BExp
False : BExp
And : BExp * BExp -> BExp
Or : BExp * BExp -> BExp
Nil : List(a)
Cons : a * List(a) -> List(a)
: ()
: a -> (a)
: a * b -> (a, b)
: a * b * c -> (a, b, c)
strategies
trans: True() -> One()
trans: False() -> Zero()
trans: And(e1,e2) -> Min(e1,e2)
trans: Or(e1,e2) -> Max(e1,e2)
topdown(s) = s; all(topdown(s))
bottomup(s) = all(bottomup(s)); s
trans_topdown = topdown(trans)
trans_bottomup = bottomup(trans)
\ No newline at end of file
Specification([Signature([Constructors([OpDecl("Zero",ConstType(SortNoArgs("NExp"))),OpDecl("One",ConstType(SortNoArgs("NExp"))),OpDecl("Max",FunType([ConstType(SortNoArgs("NExp")),ConstType(SortNoArgs("NExp"))],ConstType(SortNoArgs("NExp")))),OpDecl("Min",FunType([ConstType(SortNoArgs("NExp")),ConstType(SortNoArgs("NExp"))],ConstType(SortNoArgs("NExp")))),OpDecl("True",ConstType(SortNoArgs("BExp"))),OpDecl("False",ConstType(SortNoArgs("BExp"))),OpDecl("And",FunType([ConstType(SortNoArgs("BExp")),ConstType(SortNoArgs("BExp"))],ConstType(SortNoArgs("BExp")))),OpDecl("Or",FunType([ConstType(SortNoArgs("BExp")),ConstType(SortNoArgs("BExp"))],ConstType(SortNoArgs("BExp")))),OpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),OpDecl("Cons",FunType([ConstType(SortVar("a")),ConstType(Sort("List",[SortVar("a")]))],ConstType(Sort("List",[SortVar("a")])))),OpDeclInj(ConstType(SortTuple([]))),OpDeclInj(FunType([ConstType(SortVar("a"))],ConstType(SortTuple([SortVar("a")])))),OpDeclInj(FunType([ConstType(SortVar("a")),ConstType(SortVar("b"))],ConstType(SortTuple([SortVar("a"),SortVar("b")])))),OpDeclInj(FunType([ConstType(SortVar("a")),ConstType(SortVar("b")),ConstType(SortVar("c"))],ConstType(SortTuple([SortVar("a"),SortVar("b"),SortVar("c")]))))])]),Strategies([RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("True",[])),NoAnnoList(Op("One",[])))),RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("False",[])),NoAnnoList(Op("Zero",[])))),RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("And",[Var("e1"),Var("e2")])),NoAnnoList(Op("Min",[Var("e1"),Var("e2")])))),RDefNoArgs("trans",RuleNoCond(NoAnnoList(Op("Or",[Var("e1"),Var("e2")])),NoAnnoList(Op("Max",[Var("e1"),Var("e2")])))),SDef("topdown",[DefaultVarDec("s")],Seq(CallNoArgs(SVar("s")),All(Call(SVar("topdown"),[CallNoArgs(SVar("s"))])))),SDef("bottomup",[DefaultVarDec("s")],Seq(All(Call(SVar("bottomup"),[CallNoArgs(SVar("s"))])),CallNoArgs(SVar("s")))),SDefNoArgs("trans_topdown",Call(SVar("topdown"),[CallNoArgs(SVar("trans"))])),SDefNoArgs("trans_bottomup",Call(SVar("bottomup"),[CallNoArgs(SVar("trans"))]))])])
\ No newline at end of file
libbalg: \
./balg.str
\ No newline at end of file
Specification([Signature([Constructors([ExtOpDecl("Zero",ConstType(Sort("NExp",[]))),ExtOpDecl("One",ConstType(Sort("NExp",[]))),ExtOpDecl("Max",FunType([ConstType(Sort("NExp",[])),ConstType(Sort("NExp",[]))],ConstType(Sort("NExp",[])))),ExtOpDecl("Min",FunType([ConstType(Sort("NExp",[])),ConstType(Sort("NExp",[]))],ConstType(Sort("NExp",[])))),ExtOpDecl("True",ConstType(Sort("BExp",[]))),ExtOpDecl("False",ConstType(Sort("BExp",[]))),ExtOpDecl("And",FunType([ConstType(Sort("BExp",[])),ConstType(Sort("BExp",[]))],ConstType(Sort("BExp",[])))),ExtOpDecl("Or",FunType([ConstType(Sort("BExp",[])),ConstType(Sort("BExp",[]))],ConstType(Sort("BExp",[])))),ExtOpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),ExtOpDecl("Cons",FunType([ConstType(SortVar("a")),ConstType(Sort("List",[SortVar("a")]))],ConstType(Sort("List",[SortVar("a")])))),ExtOpDecl("DR_UNDEFINE",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),ExtOpDecl("DR_DUMMY",ConstType(Sort("ATerm",[]))),ExtOpDecl("",ConstType(Sort("Tuple",[Sort("Nil",[])]))),ExtOpDecl("",FunType([ConstType(SortVar("a"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Nil",[])])])))),ExtOpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Nil",[])])])])))),ExtOpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b")),ConstType(SortVar("c"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Cons",[SortVar("c"),Sort("Nil",[])])])])]))))])]),Strategies([ExtSDef("trans",[],[]),ExtSDef("topdown",[VarDec("c_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("bottomup",[VarDec("d_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("trans_topdown",[],[]),ExtSDef("trans_bottomup",[],[]),ExtSDef("Anno_Cong__",[VarDec("i_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("j_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Zero",[],[]),ExtSDef("One",[],[]),ExtSDef("Max",[VarDec("k_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("l_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Min",[VarDec("m_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("n_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("True",[],[]),ExtSDef("False",[],[]),ExtSDef("And",[VarDec("o_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("p_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Or",[VarDec("q_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("r_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Nil",[],[]),ExtSDef("Cons",[VarDec("s_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("t_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[],[]),ExtSDef("",[VarDec("u_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[VarDec("v_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("w_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[VarDec("x_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("y_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("z_1",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("DR_UNDEFINE",[VarDec("a_2",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("DR_DUMMY",[],[])])])
\ No newline at end of file
......@@ -23,6 +23,7 @@ case $1 in
prepare arith
prepare go2js
prepare nnf
prepare balg
;;
*)
......
......@@ -32,6 +32,7 @@ data-files:
- case-studies/cca/cca.aterm
- case-studies/go2js/go2js.aterm
- case-studies/nnf/nnf.aterm
- case-studies/balg/balg.aterm
library:
source-dirs:
......
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module AbstractSemantics where
import Prelude hiding ((.),fail)
import SortContext (Context)
import Syntax hiding (Fail,TermPattern(..))
import ValueT
import Control.Arrow.Fix
import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.Abstract.Completion
import Control.Arrow.Transformer.Abstract.Except
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Terminating
import Data.TermEnvironment
import Data.Abstract.FreeCompletion hiding (Top)
import qualified Data.Abstract.FreeCompletion as Free
import Data.Abstract.Except as E
import Data.Abstract.Error as F
import Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Abstract.DiscretePowerset as P
import qualified Data.Abstract.Map as S
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating (Terminating)
import qualified Data.Abstract.Terminating as T
import Data.Abstract.Widening as W
import Data.Order
import qualified Data.Lens as L
import Data.Identifiable
type TypeError = Pow String
type Interp t s x y =
Fix (Strat,t) t
(ValueT t
(ReaderT StratEnv
(EnvironmentT t
(ConstT Context
(ExceptT ()
(ErrorT TypeError
(CompletionT
(TerminatingT
(FixT s () ()
(->)))))))))) x y
runInterp :: forall t x y. (Show t, Complete t, UpperBounded t, Identifiable t) => Interp t _ x y -> Int -> Widening t -> StratEnv -> Context -> TermEnv t -> x -> Terminating (FreeCompletion (Error (Pow String) (Except () (TermEnv t,y))))
runInterp f k termWidening senv0 ctx tenv0 a =
runFixT stackWidening (T.widening resultWidening)
(runTerminatingT
(runCompletionT
(runErrorT
(runExceptT
(runConstT ctx
(runEnvironmentT
(runReaderT
(runValueT f))))))))
(tenv0, (senv0, a))
where
stackWidening :: SW.StackWidening _ (TermEnv t, (StratEnv, (Strat, t)))
stackWidening = SW.filter' (L.second (L.second (L.first stratCall)))
$ SW.groupBy (L.iso' (\(tenv,(senv,(strat,term))) -> ((strat,senv),(term,tenv)))
(\((strat,senv),(term,tenv)) -> (tenv,(senv,(strat,term)))))
$ SW.stack
$ SW.reuseFirst
$ SW.maxSize k
$ SW.fromWidening (termWidening W.** S.widening termWidening)
resultWidening :: Widening (FreeCompletion (Error TypeError (Except () (TermEnv t,t))))
resultWidening = Free.widening (F.widening P.widening (E.widening (\_ _ -> (Stable,())) (S.widening termWidening W.** termWidening)))
......@@ -16,10 +16,13 @@ nnf = caseStudy "nnf"
arrows :: IO Module
arrows = caseStudy "arrows"
balg :: IO Module
balg = caseStudy "balg"
caseStudy :: String -> IO Module
caseStudy name = do
file <- TIO.readFile =<< getDataFileName (printf "case-studies/%s/%s.aterm" name name)
case parseModule =<< A.parseATerm file of
Left e -> fail (show e)
Left e -> fail (printf "parsing of case study %s failed: %s" name (show e))
Right module_ -> return module_
......@@ -19,7 +19,9 @@ import SharedSemantics
import Syntax (TermPattern)
import qualified Syntax as S
import Syntax hiding (Fail,TermPattern(..))
import TermEnv
import Utils
import ValueT
import Control.Arrow
import Control.Arrow.Deduplicate
......@@ -61,18 +63,19 @@ newtype TermEnv = TermEnv (HashMap TermVar Term) deriving (Show,Eq,Hashable)
-- | Concrete interpreter arrow give access to the strategy
-- environment, term environment, and handles anonymous exceptions.
newtype Interp a b = Interp (ReaderT StratEnv (StateT TermEnv (ExceptT () (FailureT String (->)))) a b)
newtype Interp a b = Interp (ValueT Term (ReaderT StratEnv (StateT TermEnv (ExceptT () (FailureT String (->))))) a b)
deriving (Profunctor,Category,Arrow,ArrowChoice)
-- | Executes a concrete interpreter computation.
runInterp :: Interp a b -> StratEnv -> TermEnv -> a -> Error String (Error () (TermEnv,b))
runInterp (Interp f) senv tenv t = runFailureT (runExceptT (runStateT (runReaderT f))) (tenv, (senv, t))
runInterp (Interp f) senv tenv t = runFailureT (runExceptT (runStateT (runReaderT (runValueT f)))) (tenv, (senv, t))
-- | Concrete interpreter function.
eval :: Strat -> StratEnv -> TermEnv -> Term -> Error String (Error () (TermEnv,Term))
eval s = runInterp (eval' s)
-- Instances -----------------------------------------------------------------------------------------
deriving instance IsTerm Term Interp
deriving instance ArrowState TermEnv Interp
deriving instance ArrowReader StratEnv Interp
deriving instance ArrowExcept () Interp
......@@ -81,47 +84,43 @@ deriving instance ArrowDeduplicate Term Term Interp
deriving instance ArrowFail String Interp
instance ArrowApply Interp where app = Interp (lmap (first (\(Interp f) -> f)) app)
instance HasStratEnv Interp where
readStratEnv = Interp (const () ^>> ask)
localStratEnv senv f = proc a -> local f -< (senv,a)
instance IsTermEnv TermEnv Term Interp where
type Join Interp x y = ()
getTermEnv = get
putTermEnv = put
emptyTermEnv = lmap (\() -> TermEnv M.empty) put
lookupTermVar f g = proc (v,TermEnv env,exc) ->
case M.lookup v env of
Just t -> f -< t
Just t -> f -< (t, exc)
Nothing -> g -< exc
insertTerm = arr $ \(v,t,TermEnv env) ->
TermEnv (M.insert v t env)
deleteTermVars = arr $ \(vars,TermEnv env) ->
TermEnv (foldr' M.delete env vars)
unionTermEnvs = arr (\(vars, TermEnv e1, TermEnv e2) ->
TermEnv (M.union e1 (foldr' M.delete e2 vars)))
instance IsTerm Term Interp where
matchTermAgainstConstructor matchSubterms = proc (c,ts,t) -> case t of
instance (ArrowChoice c, ArrowApply c, ArrowExcept () c) => IsTerm Term (ValueT Term c) where
matchCons matchSubterms = proc (c,ts,t) -> case t of
Cons c' ts' | c == c' && eqLength ts ts' -> do
ts'' <- matchSubterms -< (ts,ts')
returnA -< Cons c ts''
_ -> throw -< ()
matchTermAgainstString = proc (s,t) -> case t of
matchString = proc (s,t) -> case t of
StringLiteral s'
| s == s' -> returnA -< t
| otherwise -> throw -< ()
_ -> throw -< ()
matchTermAgainstNumber = proc (n,t) -> case t of
matchNum = proc (n,t) -> case t of
NumberLiteral n'
| n == n' -> returnA -< t
| otherwise -> throw -< ()
_ -> throw -< ()
matchTermAgainstExplode matchCons matchSubterms = proc t -> case t of
matchExplode matchCons' matchSubterms = proc t -> case t of
Cons (Constructor c) ts -> do
matchCons -< (StringLiteral c)
matchCons' -< (StringLiteral c)
matchSubterms -< convertToList ts
returnA -< t
StringLiteral _ -> do
......@@ -130,40 +129,40 @@ instance IsTerm Term Interp where
NumberLiteral _ -> do
matchSubterms -< convertToList []
returnA -< t
buildCons = arr (uncurry Cons)
buildString = arr StringLiteral
buildNum = arr NumberLiteral
buildExplode = proc (c,ts) -> case (c,go ts) of
(StringLiteral c', Just ts') -> returnA -< Cons (Constructor c') ts'
_ -> throw -< ()
where
go l = case l of
Cons "Cons" [x,tl] -> (x:) <$> go tl
Cons "Nil" [] -> Just []
_ -> Nothing
equal = proc (t1,t2) ->
case (t1,t2) of
(Cons c ts, Cons c' ts')
| c == c' && eqLength ts ts' -> do
ts'' <- zipWithA equal -< (ts,ts')
cons -< (c,ts'')
buildCons -< (c,ts'')
(StringLiteral s, StringLiteral s')
| s == s' -> success -< t1
(NumberLiteral n, NumberLiteral n')
| n == n' -> success -< t1
(_,_) -> throw -< ()
convertFromList = proc (c,ts) -> case (c,go ts) of
(StringLiteral c', Just ts') -> returnA -< Cons (Constructor c') ts'
_ -> throw -< ()
where
go t = case t of
Cons "Cons" [x,tl] -> (x:) <$> go tl
Cons "Nil" [] -> Just []
_ -> Nothing
mapSubterms f = proc t ->
case t of
Cons c ts -> do
ts' <- f -< ts
cons -< (c,ts')
buildCons -< (c,ts')
StringLiteral {} -> returnA -< t
NumberLiteral {} -> returnA -< t
cons = arr (uncurry Cons)
numberLiteral = arr NumberLiteral
stringLiteral = arr StringLiteral
instance TermUtils Term where
convertToList ts = case ts of
(x:xs) -> Cons "Cons" [x,convertToList xs]
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.TermEnvironment where
import Prelude hiding ((.))
import Syntax
import qualified ConcreteSemantics as C
import Control.Category
import Control.Arrow
import Control.Arrow.State
import Control.Arrow.Transformer.State
import Control.Arrow.Fix
import Control.Arrow.Fail
import Control.Arrow.Except
import Control.Arrow.Trans
import Control.Arrow.Deduplicate
import Control.Arrow.Const
import Control.Arrow.Abstract.Join
import Data.Order
import qualified Data.Concrete.Powerset as C
import Data.Abstract.FreeCompletion as Free
import Data.Abstract.Map (Map)
import qualified Data.Abstract.Map as S
import qualified Data.Abstract.Maybe as A
import qualified Data.HashMap.Lazy as LM
import Data.Profunctor
import Data.Identifiable
import Data.Coerce
import Data.GaloisConnection
import TermEnv
type TermEnv t = Map TermVar t
type instance Fix x y (EnvironmentT t c) = EnvironmentT t (Fix (Dom (EnvironmentT t) x y) (Cod (EnvironmentT t) x y) c)
newtype EnvironmentT t c x y = EnvironmentT (StateT (TermEnv t) c x y)
deriving (Category,Profunctor,Arrow,ArrowChoice,ArrowJoin,ArrowTrans,ArrowLift,ArrowFail e,ArrowExcept e,ArrowConst r)
deriving instance ArrowFix (Dom (EnvironmentT t) x y) (Cod (EnvironmentT t) x y) c => ArrowFix x y (EnvironmentT t c)
deriving instance (Identifiable t, UpperBounded t, ArrowDeduplicate (Dom (EnvironmentT t) x y) (Cod (EnvironmentT t) x y) c) => ArrowDeduplicate x y (EnvironmentT t c)
deriving instance (PreOrd (c (Dom (EnvironmentT t) x y) (Cod (EnvironmentT t) x y))) => PreOrd (EnvironmentT t c x y)
deriving instance (LowerBounded (c (Dom (EnvironmentT t) x y) (Cod (EnvironmentT t) x y))) => LowerBounded (EnvironmentT t c x y)
deriving instance (Complete (c (Dom (EnvironmentT t) x y) (Cod (EnvironmentT t) x y))) => Complete (EnvironmentT t c x y)
instance (Profunctor c, ArrowApply c) => ArrowApply (EnvironmentT t c) where
app = EnvironmentT $ lmap (first coerce) app
runEnvironmentT :: EnvironmentT t c x y -> c (TermEnv t,x) (TermEnv t,y)
runEnvironmentT (EnvironmentT (StateT f)) = f
instance Complete t => Complete (FreeCompletion (TermEnv t)) where
Lower x Lower y = Lower (x y)
_ _ = Free.Top
instance (Complete t, ArrowChoice c, ArrowJoin c, ArrowTop t (EnvironmentT t c))
=> IsTermEnv (TermEnv t) t (EnvironmentT t c) where
type Join (EnvironmentT t c) ((t,e),e) x = Complete x
getTermEnv = EnvironmentT get
putTermEnv = EnvironmentT put
emptyTermEnv = EnvironmentT $ lmap (\() -> S.empty) put
lookupTermVar f g = proc (v,env,ex) -> do
case S.lookup v env of
A.Just t -> f -< (t,ex)
A.Nothing -> g -< ex
A.JustNothing t -> (f -< (t,ex)) <> (g -< ex)
insertTerm = arr $ \(v,t,env) -> S.insert v t env
deleteTermVars = arr $ \(vars,env) -> S.delete' vars env
instance (Galois (C.Pow C.Term) t, Complete t) => Galois (C.Pow C.TermEnv) (TermEnv t) where
alpha = lub . fmap (\(C.TermEnv e) -> S.fromList (LM.toList (fmap alphaSing e)))
gamma = undefined
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures -Wno-orphans #-}
module SingletonSemantics where
import Prelude hiding ((.),fail)
import qualified ConcreteSemantics as C
import ConcreteSemantics ()
import SharedSemantics as Shared
import AbstractSemantics
import SortContext (Context)
import Syntax hiding (Fail,TermPattern(..))
import Utils
import ValueT
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Except
import Control.Arrow.Fail
import Control.Arrow.Abstract.Join
import Data.Abstract.FreeCompletion hiding (Top)
import qualified Data.Abstract.FreeCompletion as Free
import Data.Abstract.Except as E
import Data.Abstract.Error as F
import Data.Abstract.Singleton
import Data.Abstract.Terminating (Terminating)
import Data.Abstract.Widening as W
import Data.Constructor
import Data.Order
import Data.Profunctor
import Data.Term
import Data.TermEnvironment
import GHC.Exts(IsString(..))
type Term = Singleton C.Term
eval :: Int -> Int -> Strat -> StratEnv -> Context -> TermEnv Term -> Term -> Terminating (FreeCompletion (Error TypeError (Except () (TermEnv Term,Term))))
eval i _ strat senv ctx = runInterp (Shared.eval' strat) i W.finite senv ctx
liftConcrete :: Arrow c => ValueT C.Term c x y -> ValueT t' c x (Singleton y)
liftConcrete (ValueT f) = Single ^<< ValueT f
-- Instances -----------------------------------------------------------------------------------------
instance (ArrowChoice c, ArrowApply c, ArrowJoin c, ArrowConst Context c, ArrowFail e c, ArrowExcept () c, IsString e, LowerBounded (c () Term))
=> IsTerm Term (ValueT Term c) where
matchCons matchSubterms = proc (c,ps,t) -> case t of
Single (C.Cons c' ts) | c == c' && eqLength ps ts -> do
ts' <- matchSubterms -< (ps,map Single ts)
case allSingle ts' of
Nothing -> returnA -< Any
Just cts' -> returnA -< Single $ C.Cons c cts'
Single _ -> throw -< ()
Any -> do
matchSubterms -< (ps, replicate (length ps) Any)
(returnA -< Any) <> (throw -< ())
matchString = proc (s,t) -> case t of
Single ct -> liftConcrete matchString -< (s,ct)
Any -> (returnA -< Any) <> (throw -< ())
matchNum = proc (i,t) -> case t of
Single ct -> liftConcrete matchNum -< (i,ct)
Any -> (returnA -< Any) <> (throw -< ())
matchExplode matchCons' matchSubterms = proc t -> case t of
Single (C.Cons (Constructor c) ts) -> do
matchCons' -< Single $ C.StringLiteral c
matchSubterms -< Single $ convertToList ts
returnA -< t
Single (C.StringLiteral _) -> do
matchSubterms -< Single $ convertToList []
returnA -< t
Single (C.NumberLiteral _) -> do
matchSubterms -< Single $ convertToList []
returnA -< t
Any -> do
matchCons' -< Any
matchSubterms -< Any
returnA -< Any
buildExplode = proc (t, ts) -> case (t, ts) of
(Single ct, Single cts) -> liftConcrete buildExplode -< (ct, cts)
_ -> returnA -< Any
buildCons = proc (c, ts) -> case allSingle ts of
Just cts -> liftConcrete buildCons -< (c, cts)
Nothing -> returnA -< Any
buildNum = liftConcrete buildNum
buildString = liftConcrete buildString
equal = proc (t1,t2) -> case (t1, t2) of
(Single ct1, Single ct2) -> liftConcrete equal -< (ct1, ct2)
_ -> (returnA -< t1) <> (throw -< ())
mapSubterms f = proc t -> case t of
Single ct -> case ct of
C.Cons c ts -> do
ts' <- f -< map Single ts
case allSingle ts' of
Nothing -> returnA -< Any
Just cts' -> returnA -< Single $ C.Cons c cts'
C.StringLiteral {} -> returnA -< t
C.NumberLiteral {} -> returnA -< t
Any -> (returnA -< Any) <> (throw -< ())
instance (Arrow c, Profunctor c) => ArrowTop Term c where
topA = arr (const Any)
instance Complete (FreeCompletion Term) where
Lower x Lower y = Lower (x y)
_ _ = Free.Top
......@@ -10,7 +10,8 @@ import Data.Text(Text, unpack)
import Data.String(IsString(..))
import Data.Hashable(Hashable(..))
import Data.List(intercalate)
import Data.Abstract.Widening(Widening,Stable(..))
import Data.Abstract.Widening(Widening)
import Data.Abstract.Stable
import GHC.Generics(Generic)
......@@ -38,7 +39,7 @@ instance Show Sort where
show x = case x of
Bottom -> "Bottom"
Top -> "Top"
Numerical -> "Int"
Numerical -> "Numerical"
Lexical -> "Lexical"
List s -> "List (" ++ show s ++ ")"
Option s -> "Option (" ++ show s ++ ")"
......@@ -67,7 +68,7 @@ getSortId s = case s of
_ -> Nothing
widening :: Int -> Widening Sort
widening n0 s1 s2 = let s' = go n0 s2 in (if s' == s1 then Stable else Instable,s')
widening n0 s1 s2 = let s' = go n0 s2 in (if s' == s1 then Stable else Unstable,s')
where
go 0 _ = Top
go n s = case s of
......
......@@ -6,7 +6,7 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
module SortContext(
Context, HasContext(..), Sort(..), Signature(..), SortId(..), empty, signatures, sorts,
fromList, insertSignature, insertSubtype, subtype, lookupSort, lookupCons,
fromList, insertSignature, insertSubtype, subtype, lookupSort, lookupCons, numSorts,
lub, glb, isLexical, isList, getListElem, isSingleton, isNumerical, isTuple, filterInconsistentConstructors
) where
......@@ -32,6 +32,9 @@ data Context = Context
empty :: Context
empty = Context M.empty M.empty R.empty
numSorts :: Context -> Int
numSorts ctx = M.size (sorts ctx)
fromList :: [(Constructor,[Sort],Sort)] -> Context
fromList = foldl (\ctx (c,ss,s) -> insertSignature c (Signature ss s) ctx) empty
......@@ -66,8 +69,8 @@ lookupSort Context {..} s0 = do
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)]
Lexical -> [("", Signature [Lexical] Lexical)]
Numerical -> [("", Signature [Numerical] Numerical)]
Sort _ -> fromMaybe [] (M.lookup s sorts)
isLexical :: Context -> Sort -> Bool
......
This diff is collapsed.
......@@ -96,7 +96,7 @@ glb rel s1 s2 = case (s1,s2) of
lower :: SubtypeRelation -> Sort -> [Sort]
lower rel@(SubtypeRelation _ _ gr) s = case s of
Bottom -> [Bottom]
Top -> error "lower set of top is unsupported"
Top -> [Top]
Lexical -> return Lexical
Numerical -> return Numerical
List x -> List <$> lower rel x
......
......@@ -10,6 +10,7 @@ import SortContext (Context,Sort,Signature)
import qualified SortContext as I
import Control.Monad.Except
import Control.Monad.Writer (Writer, tell, runWriter)
import Control.DeepSeq
import Data.ATerm
......@@ -86,6 +87,59 @@ type StratEnv = HashMap StratVar Closure
newtype TermVar = TermVar Text deriving (Eq,Ord,Hashable,NFData)
newtype StratVar = StratVar Text deriving (Eq,Ord,IsString,Hashable,NFData)
liftStrategyScopes :: Strategy -> Strategy
liftStrategyScopes (Strategy svs tvs s) = Strategy svs tvs (liftStratScopes s)
liftStratScopes :: Strat -> Strat
liftStratScopes s =
let (s', vs) = runWriter (liftScopes s) in
if length vs == S.size (S.fromList vs)
then if null vs
then s'
else Scope vs s'
else error $ "found duplicate scope vars " ++ show vs
liftScopes :: Strat -> Writer [TermVar] Strat
liftScopes strat = case strat of
Id -> return Id
Fail -> return Fail
Seq s1 s2 -> do
s1' <- liftScopes s1
s2' <- liftScopes s2
return $ Seq s1' s2'
GuardedChoice s1 s2 s3 -> do
s1' <- liftScopes s1
s2' <- liftScopes s2
s3' <- liftScopes s3
return $ GuardedChoice s1' s2' s3'
One s -> One <$> liftScopes s
Some s -> Some <$> liftScopes s
All s -> All <$> liftScopes s
Scope xs s -> do
tell xs
liftScopes s
Match f -> return $ Match f
Build f -> return $ Build f
Let bnds body -> do
let bnds' = map (\(v,s) -> (v,liftStrategyScopes s)) bnds
body' <- liftScopes body
return $ Let bnds' body'
Call f ss ts -> do
let ss' = map liftStratScopes ss
return $ Call f ss' ts
Prim f ss ts -> do
let ss' = map liftStratScopes ss
return $ Prim f ss' ts
Apply body -> Apply <$> liftScopes body
-- instance Monoid TermVarSet where
-- mempty = TermVarSet mempty
-- mappend (TermVarSet s1) (TermVarSet s2) =
-- if S.null (S.intersection s1 s2)
-- then TermVarSet $ S.union s1 s2
-- else error $ "non-unique scope vars " ++ show (s1,s2)
leftChoice :: Strat -> Strat -> Strat
leftChoice f = GuardedChoice f Id
......@@ -148,21 +202,16 @@ parseSort :: MonadError String m => ATerm -> m Sort
parseSort t = case t of
ATerm "ConstType" [res] -> parseSort res
ATerm "SortNoArgs" [String "String"] -> return $ I.Lexical
ATerm "SortNoArgs" [String "Int"] -> return $ I.Numerical
ATerm "SortNoArgs" [String sortName] -> return $ I.Sort (I.SortId sortName)
ATerm "Sort" [String "String", List []] ->
return $ I.Lexical
ATerm "Sort" [String sortName, List []] ->
return $ I.Sort (I.SortId sortName)
ATerm "Sort" [String "List", List [s]] ->
I.List <$> parseSort s
ATerm "Sort" [String "List", List ss] ->
I.List <$> I.Tuple <$> traverse parseSort ss
ATerm "Sort" [String "Option", List [s]] ->
I.Option <$> parseSort s
ATerm "Sort" [String "Option", List ss] ->
I.Option <$> I.Tuple <$> traverse parseSort ss
ATerm "SortTuple" [List args] ->
I.Tuple <$> traverse parseSort args
ATerm "Sort" [String "String", List []] -> return $ I.Lexical
ATerm "Sort" [String "Int", List []] -> return $ I.Numerical
ATerm "Sort" [String sortName, List []] -> return $ I.Sort (I.SortId sortName)
ATerm "Sort" [String "List", List [s]] -> I.List <$> parseSort s
ATerm "Sort" [String "List", List ss] -> I.List <$> I.Tuple <$> traverse parseSort ss
ATerm "Sort" [String "Option", List [s]] -> I.Option <$> parseSort s
ATerm "Sort" [String "Option", List ss] -> I.Option <$> I.Tuple <$> traverse parseSort ss
ATerm "SortTuple" [List args] -> I.Tuple <$> traverse parseSort args
_ -> throwError $ "unexpected input while parsing sort from aterm: " ++ show t
parseStrategy :: MonadError String m => ATerm -> m (StratVar,Strategy)
......@@ -171,12 +220,12 @@ parseStrategy strat = case strat of
str <- Strategy <$> parseStratVars stratVars
<*> parseTermVars ts
<*> parseStrat body
return (StratVar name, str)
return (StratVar name, liftStrategyScopes str)
ATerm "ExtSDef" [String name, List ts, List stratVars] -> do
str <- Strategy <$> parseStratVars stratVars
<*> parseTermVars ts
<*> return Id
return (StratVar name, str)
return (StratVar name, liftStrategyScopes str)
_ -> throwError $ "unexpected input while parsing strategy from aterm: " ++ show strat
parseStratVars :: MonadError String m => [ATerm] -> m [StratVar]
......@@ -422,6 +471,9 @@ arbitraryTermPattern h w var
class TermVars s where
termVars :: (IsList (f TermVar), Item (f TermVar) ~ TermVar, Monoid (f TermVar)) => s -> f TermVar
instance TermVars Module where
termVars (Module _ strats) = termVars strats
instance (TermVars x,TermVars y) => TermVars (HashMap x y) where
termVars = termVars . M.toList
......
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module TermEnv where
import Prelude hiding ((.),id,all,sequence,curry, uncurry,fail)
import Syntax hiding (Fail,TermPattern(..))
import Control.Arrow hiding ((<+>))
import Control.Arrow.Fail
import Control.Arrow.Trans
import Control.Arrow.Utils
import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Static
import Control.Arrow.Transformer.Reader
import Data.Profunctor
import GHC.Exts(Constraint)
import GHC.Exts(IsString(..))
-- | Arrow-based interface for term environments. Because of the
-- dynamic scoping of stratego, term environments are more like
-- mutable state then conventional environments.
class Arrow c => IsTermEnv env t c | c -> env, env -> t where
-- | Type class constraint used by the abstract instances to join arrow computations.
type family Join (c :: * -> * -> *) x y :: Constraint
-- | Fetch the current term environment.
getTermEnv :: c () env
-- | Fetch the current term environment.
putTermEnv :: c env ()
emptyTermEnv :: c () ()
-- | Lookup a term in the given environment, the first continuation
-- is called in case the term is in the environment and the second
-- continuation otherwise.
lookupTermVar :: (Join c ((t,e),e) x) => c (t,e) x -> c e x -> c (TermVar,env,e) x
-- | Insert a term into the given environment.
insertTerm :: c (TermVar,t,env) env
-- | Delete the specified variables from the given environment.
deleteTermVars :: c ([TermVar],env) env
lookupTermVar' :: (IsTermEnv env t c, Join c ((t,e),e) x) => c (t,e) x -> c e x -> c (TermVar,e) x
lookupTermVar' f g = proc (v,exc) -> do
env <- getTermEnv -< ()
lookupTermVar f g -< (v,env,exc)
lookupTermVarOrFail :: (IsTermEnv env t c, ArrowFail e c, IsString e, Join c ((t,e),e) t) => c TermVar t
lookupTermVarOrFail = proc v -> do
env <- getTermEnv -< ()
lookupTermVar (fst ^>> returnA) fail -< (v, env, fromString $ "Unbound variable " ++ show v)
insertTerm' :: IsTermEnv env t c => c (TermVar,t) ()
insertTerm' = proc (v,t) -> do
env <- getTermEnv -< ()
putTermEnv <<< insertTerm -< (v,t,env)
deleteTermVars' :: IsTermEnv env t c => c [TermVar] ()
deleteTermVars' = proc vs -> do
env <- getTermEnv -< ()
putTermEnv <<< deleteTermVars -< (vs,env)
-- | Add a list of bindings to the given environment.
bindings :: (ArrowChoice c, IsTermEnv env t c) => c ([(TermVar,t)],env) env
bindings = fold ((\(env,(x,y)) -> (x,y,env)) ^>> insertTerm)
deriving instance (Profunctor c, IsTermEnv env t c) => IsTermEnv env t (ConstT r c)
instance (ArrowApply c, Profunctor c, IsTermEnv env t c) => IsTermEnv env t (ReaderT r c) where
type Join (ReaderT r c) ((t,e),e) x = Join c ((t,e),e) x
getTermEnv = lift' getTermEnv
putTermEnv = lift' putTermEnv
emptyTermEnv = lift' emptyTermEnv
lookupTermVar (ReaderT f) (ReaderT g) = ReaderT $ proc (r,x) -> lookupTermVar (proc t -> f -< (r,t)) (proc e -> g -< (r,e)) -<< x
insertTerm = lift' insertTerm
deleteTermVars = lift' deleteTermVars
instance (Profunctor c, Applicative r, IsTermEnv env t c) => IsTermEnv env t (StaticT r c) where
type Join (StaticT r c) ((t,e),e) x = Join c ((t,e),e) x
getTermEnv = StaticT $ pure getTermEnv
putTermEnv = StaticT $ pure putTermEnv
emptyTermEnv = StaticT $ pure emptyTermEnv
lookupTermVar (StaticT f) (StaticT g) = StaticT $ lookupTermVar <$> f <*> g
insertTerm = StaticT $ pure insertTerm
deleteTermVars = StaticT $ pure deleteTermVars
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module ValueT where
import Prelude hiding ((.),fail)
import Control.Category
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Deduplicate
import Control.Arrow.Except
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Trans
import Control.Arrow.Abstract.Join
import Data.Order
import Data.Profunctor
import Data.Coerce
import TermEnv
type instance Fix x y (ValueT t c) = ValueT t (Fix (Dom (ValueT t) x y) (Cod (ValueT t) x y) c)
newtype ValueT t c x y = ValueT { runValueT :: c x y }
deriving (Category,Profunctor,Arrow,ArrowChoice,ArrowJoin,ArrowFail e,ArrowExcept e,ArrowFix a b,ArrowDeduplicate a b,ArrowReader r,IsTermEnv env t,ArrowConst r,ArrowState s)
instance ArrowTrans (ValueT t) where
type Dom (ValueT t) x y = x
type Cod (ValueT t) x y = y
lift = ValueT
unlift = runValueT
instance (Profunctor c, ArrowApply c) => ArrowApply (ValueT t c) where
app = ValueT $ lmap (first coerce) app
deriving instance (PreOrd (c (Dom (ValueT t) x y) (Cod (ValueT t) x y))) => PreOrd (ValueT t c x y)
deriving instance (LowerBounded (c (Dom (ValueT t) x y) (Cod (ValueT t) x y))) => LowerBounded (ValueT t c x y)
deriving instance (Complete (c (Dom (ValueT t) x y) (Cod (ValueT t) x y))) => Complete (ValueT t c x y)
((haskell-mode . ((flycheck-ghc-search-path . ("/home/sven/documents/sturdy/stratego/src/" "/home/sven/documents/sturdy/stratego/.stack-work/dist/x86_64-linux-nix/Cabal-2.2.0.1/build/spec/autogen/")))))
((haskell-mode . ((flycheck-ghc-search-path . ("/home/sven/documents/sturdy/stratego/src/" "/home/sven/documents/sturdy/stratego/.stack-work/dist/x86_64-linux-nix/Cabal-2.4.0.1/build/spec/autogen/")))))
......@@ -32,8 +32,8 @@ spec = do
describe "scope" $ do
it "should hide declare variables" $ do
let tenv = termEnv [("x", term1)]
eval (Scope ["x"] (Build "x")) M.empty tenv term2
`shouldBe` error "unbound term variable x in build statement !x"
-- eval (Scope ["x"] (Build "x")) M.empty tenv term2
-- `shouldBe` error "unbound term variable x in build statement !x"
eval (Scope ["x"] (Match "x")) M.empty tenv term2
`shouldBe` success (tenv,term2)
......
This diff is collapsed.
This diff is collapsed.