Commit 7eba3b90 authored by Sven Keidel's avatar Sven Keidel

Merge branch 'type-changing-traversal'

parents 58891224 e88a71c0
Pipeline #15953 passed with stages
in 31 minutes and 51 seconds
......@@ -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 ((.))
<