{- |
Description: Motivating Example: Alice works on Stack.pop
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Module for reproducing our motivating 'example' where Alice edits the @pop@ method of a class @Stack@ in Java.
The example is described in detail in Section 2.1 of the paper and shown in Figure 1.
-}
module StackPopAlice where

import Control.Monad.State ( State )
import UUID ( UUID )
import Tree
import AST
import Edits
import Propositions
import Feature
import FeatureTrace
import FeatureColour
import SimpleJava
import System.Terminal
    ( MonadColorPrinter(..) )
import Data.Maybe ( fromJust )

import Example

-- | Feature @SafeStack@ from the paper.
feature_SafeStack :: Feature
feature_SafeStack :: Feature
feature_SafeStack = Feature -> Feature
toFeature "SafeStack"

-- | Feature @ImmutableStack@ from the paper.
feature_ImmutableStack :: Feature
feature_ImmutableStack :: Feature
feature_ImmutableStack = Feature -> Feature
toFeature "ImmutableStack"

{- |
Colours for features and feature formulas used in this example.
We chose terminal colours as close the the colours used in the paper as possible.
-}
featurecolours :: MonadColorPrinter m => FeatureFormulaColourPalette m
featurecolours :: FeatureFormulaColourPalette m
featurecolours p :: FeatureFormula
p
    | FeatureFormula
p FeatureFormula -> FeatureFormula -> Bool
forall a. Eq a => a -> a -> Bool
== (PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ PropositionalFormula Feature -> PropositionalFormula Feature
forall a. PropositionalFormula a -> PropositionalFormula a
PNot (PropositionalFormula Feature -> PropositionalFormula Feature)
-> PropositionalFormula Feature -> PropositionalFormula Feature
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable (Feature -> PropositionalFormula Feature)
-> Feature -> PropositionalFormula Feature
forall a b. (a -> b) -> a -> b
$ Feature
feature_ImmutableStack) = Color m
forall (m :: * -> *). MonadColorPrinter m => Color m
magenta
    | FeatureFormula
p FeatureFormula -> FeatureFormula -> Bool
forall a. Eq a => a -> a -> Bool
== (PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable (Feature -> PropositionalFormula Feature)
-> Feature -> PropositionalFormula Feature
forall a b. (a -> b) -> a -> b
$ Feature
feature_SafeStack) = Color m
forall (m :: * -> *). MonadColorPrinter m => Color m
cyan
    | FeatureFormula
p FeatureFormula -> FeatureFormula -> Bool
forall a. Eq a => a -> a -> Bool
== (PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable (Feature -> PropositionalFormula Feature)
-> Feature -> PropositionalFormula Feature
forall a b. (a -> b) -> a -> b
$ Feature
feature_ImmutableStack) = Color m
forall (m :: * -> *). MonadColorPrinter m => Color m
yellow
    | Bool
otherwise = Color m
forall (m :: * -> *). MonadColorPrinter m => Color m
white

-- | Initial 'AST' of the pop method (version (1)).
startTree :: State UUID SSJavaAST
startTree :: State UUID SSJavaAST
startTree = Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> State UUID SSJavaAST)
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall a b. (a -> b) -> a -> b
$
    Feature
-> Feature
-> [(Feature, Feature)]
-> [Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))]
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_methoddef "void" "pop" [] [
        Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_exprstatement (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature)))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
forall a b. (a -> b) -> a -> b
$ Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_assignment (Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_varref "storage[head--]") "=" (Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_literal "null")
    ]

{- |
'AST' representing the condition checking for an empty stack.
@if (!empty()) { }@
-}
condTree :: State UUID SSJavaAST
condTree :: State UUID SSJavaAST
condTree = Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> State UUID SSJavaAST)
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall a b. (a -> b) -> a -> b
$ Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> [Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))]
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_condition (Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_unaryop "!" (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature)))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
forall a b. (a -> b) -> a -> b
$ Feature
-> [Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))]
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_funccall "empty" []) []

{- | 'AST' of the first line of code that was inserted in version (5) to implement feature ImmutableStack.
@Stack<T> c = clone();@
-}
cloneDef :: State UUID SSJavaAST
cloneDef :: State UUID SSJavaAST
cloneDef = Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> State UUID SSJavaAST)
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall a b. (a -> b) -> a -> b
$ Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_exprstatement (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature)))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
forall a b. (a -> b) -> a -> b
$ Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_assignment (Feature
-> Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_vardecl "Stack<T>" "c") "=" (Feature
-> [Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))]
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_funccall "clone" [])

{- | 'AST' of the second line of code that was inserted in version (5) to implement feature ImmutableStack.
@c.storage[c.head--] = null;@
-}
cloneStorage :: State UUID SSJavaAST
cloneStorage :: State UUID SSJavaAST
cloneStorage = Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> State UUID SSJavaAST)
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall a b. (a -> b) -> a -> b
$ Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_exprstatement (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature)))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
forall a b. (a -> b) -> a -> b
$ Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_assignment (Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_varref "c.storage[c.head--]") "=" (Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_literal "null")

{- | 'AST' of the third line of code that was inserted in version (5) to implement feature ImmutableStack.
@return c;@
-}
cloneRetStatement :: State UUID SSJavaAST
cloneRetStatement :: State UUID SSJavaAST
cloneRetStatement = Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> State UUID SSJavaAST)
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> State UUID SSJavaAST
forall a b. (a -> b) -> a -> b
$ Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_return (Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
 -> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature)))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
forall a b. (a -> b) -> a -> b
$ Feature
-> Tree (StateT UUID Identity (Node SimpleJavaGrammar Feature))
sjava_varref "c"

{- | New return type of the pop method in version (6).
@Stack<T>@
-}
newReturnType :: String
newReturnType :: Feature
newReturnType = "Stack<T>"

{-
Example replaying our motivating example shown in Figure 1 and described in Section 2.1 in our paper.
Alice works on the @pop@ method of a Java class @Stack@.
-}
example :: (MonadColorPrinter m) => State UUID (Example m SimpleJavaGrammar String)
example :: State UUID (Example m SimpleJavaGrammar Feature)
example =
    do
        SSJavaAST
tree_start <- State UUID SSJavaAST
StackPopAlice.startTree
        SSJavaAST
tree_cond <- State UUID SSJavaAST
StackPopAlice.condTree
        SSJavaAST
tree_clonedef <- State UUID SSJavaAST
StackPopAlice.cloneDef
        SSJavaAST
tree_clonestorage <- State UUID SSJavaAST
StackPopAlice.cloneStorage
        SSJavaAST
tree_cloneretstatement <- State UUID SSJavaAST
StackPopAlice.cloneRetStatement
        let
            id_tree_start_body :: UUID
id_tree_start_body = SSJavaAST -> UUID
forall g a. AST g a -> UUID
uuidOf (SSJavaAST -> UUID)
-> (Maybe SSJavaAST -> SSJavaAST) -> Maybe SSJavaAST -> UUID
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe SSJavaAST -> SSJavaAST
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe SSJavaAST -> UUID) -> Maybe SSJavaAST -> UUID
forall a b. (a -> b) -> a -> b
$ SimpleJavaGrammar -> SSJavaAST -> Maybe SSJavaAST
forall g a. Eq g => g -> AST g a -> Maybe (AST g a)
findByGrammarType SimpleJavaGrammar
SJava_Statements SSJavaAST
tree_start
            id_tree_start_storage :: UUID
id_tree_start_storage = SSJavaAST -> UUID
forall g a. AST g a -> UUID
uuidOf (SSJavaAST -> UUID)
-> (Maybe SSJavaAST -> SSJavaAST) -> Maybe SSJavaAST -> UUID
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe SSJavaAST -> SSJavaAST
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe SSJavaAST -> UUID) -> Maybe SSJavaAST -> UUID
forall a b. (a -> b) -> a -> b
$ SimpleJavaGrammar -> SSJavaAST -> Maybe SSJavaAST
forall g a. Eq g => g -> AST g a -> Maybe (AST g a)
findByGrammarType SimpleJavaGrammar
SJava_ExprStatement SSJavaAST
tree_start
            id_tree_cond_body :: UUID
id_tree_cond_body = SSJavaAST -> UUID
forall g a. AST g a -> UUID
uuidOf (SSJavaAST -> UUID)
-> (Maybe SSJavaAST -> SSJavaAST) -> Maybe SSJavaAST -> UUID
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe SSJavaAST -> SSJavaAST
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe SSJavaAST -> UUID) -> Maybe SSJavaAST -> UUID
forall a b. (a -> b) -> a -> b
$ SimpleJavaGrammar -> SSJavaAST -> Maybe SSJavaAST
forall g a. Eq g => g -> AST g a -> Maybe (AST g a)
findByGrammarType SimpleJavaGrammar
SJava_Statements SSJavaAST
tree_cond
            id_tree_start_ret :: UUID
id_tree_start_ret = SSJavaAST -> UUID
forall g a. AST g a -> UUID
uuidOf (SSJavaAST -> UUID)
-> (Maybe SSJavaAST -> SSJavaAST) -> Maybe SSJavaAST -> UUID
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe SSJavaAST -> SSJavaAST
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe SSJavaAST -> UUID) -> Maybe SSJavaAST -> UUID
forall a b. (a -> b) -> a -> b
$ SimpleJavaGrammar -> SSJavaAST -> Maybe SSJavaAST
forall g a. Eq g => g -> AST g a -> Maybe (AST g a)
findByGrammarType SimpleJavaGrammar
SJava_Type SSJavaAST
tree_start
        Example m SimpleJavaGrammar Feature
-> State UUID (Example m SimpleJavaGrammar Feature)
forall (m :: * -> *) a. Monad m => a -> m a
return Example :: forall (m :: * -> *) g a.
Feature
-> Version g a
-> History g a
-> FeatureFormulaColourPalette m
-> Example m g a
Example {
            name :: Feature
Example.name = "Motivating Example: Alice works on Stack.pop",
            colours :: FeatureFormulaColourPalette m
Example.colours = FeatureFormulaColourPalette m
forall (m :: * -> *).
MonadColorPrinter m =>
FeatureFormulaColourPalette m
featurecolours,
            startVersion :: Version SimpleJavaGrammar Feature
Example.startVersion = (FeatureTrace SimpleJavaGrammar Feature
forall g a. FeatureTrace g a
emptyTrace, SSJavaAST
tree_start),
            history :: History SimpleJavaGrammar Feature
history = [Edit SimpleJavaGrammar Feature]
-> [FeatureFormula] -> History SimpleJavaGrammar Feature
forall a b. [a] -> [b] -> [(a, b)]
zip [ -- Edits
                SSJavaAST -> UUID -> UUID -> Edit SimpleJavaGrammar Feature
forall a g. Eq a => AST g a -> UUID -> UUID -> Edit g a
edit_ins_tree SSJavaAST
tree_cond UUID
id_tree_start_body 0
              , UUID -> UUID -> UUID -> Edit SimpleJavaGrammar Feature
forall g a.
(Grammar g, Eq a, Show a) =>
UUID -> UUID -> UUID -> Edit g a
edit_move_tree UUID
id_tree_start_storage UUID
id_tree_cond_body 0
              , UUID -> Edit SimpleJavaGrammar Feature
forall a g. Eq a => UUID -> Edit g a
edit_del_tree UUID
id_tree_start_storage
              , SSJavaAST -> UUID -> UUID -> Edit SimpleJavaGrammar Feature
forall a g. Eq a => AST g a -> UUID -> UUID -> Edit g a
edit_ins_tree SSJavaAST
tree_clonestorage UUID
id_tree_cond_body 0
              , SSJavaAST -> UUID -> UUID -> Edit SimpleJavaGrammar Feature
forall a g. Eq a => AST g a -> UUID -> UUID -> Edit g a
edit_ins_tree SSJavaAST
tree_clonedef UUID
id_tree_start_body 0
              , SSJavaAST -> UUID -> UUID -> Edit SimpleJavaGrammar Feature
forall a g. Eq a => AST g a -> UUID -> UUID -> Edit g a
edit_ins_tree SSJavaAST
tree_cloneretstatement UUID
id_tree_start_body 2
              , UUID
-> SimpleJavaGrammar -> Feature -> Edit SimpleJavaGrammar Feature
forall g a. (Grammar g, Show a, Eq a) => UUID -> g -> a -> Edit g a
edit_update UUID
id_tree_start_ret SimpleJavaGrammar
SJava_Type Feature
newReturnType
            ] [ -- corresponding feature contexts
                PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable Feature
feature_SafeStack
              , FeatureFormula
forall a. Maybe a
Nothing
              , PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable Feature
feature_ImmutableStack
              , PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable Feature
feature_ImmutableStack
              , PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable Feature
feature_ImmutableStack
              , PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable Feature
feature_ImmutableStack
              , PropositionalFormula Feature -> FeatureFormula
forall a. a -> Maybe a
Just (PropositionalFormula Feature -> FeatureFormula)
-> PropositionalFormula Feature -> FeatureFormula
forall a b. (a -> b) -> a -> b
$ Feature -> PropositionalFormula Feature
forall a. a -> PropositionalFormula a
PVariable Feature
feature_ImmutableStack
            ]
        }