{- |
Description: Implementation of feature trace recording as proposed in the paper.
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Implementation of feature trace recording as proposed in the paper (Section 4.2).
-}
module DefaultFeatureTraceRecording where

import Grammar
import Edits
import AST
import FeatureTrace
import FeatureTraceRecording
import Logic
import NullPropositions
import Data.Set
import ListUtil

{- |
This is the default implementation of feature trace recording as proposed in our paper.
For each type of edit, we choose one of the four recording functions from R_ins, R_del, R_mov, and R_up.
Next to these four functions, we support two more default recording function in this library, 'r_id' and 'r_trace'.
We use 'r_id' for technical reasons (e.g., folds, printing) and it does not affect the mappings.
We use 'r_trace' to manually change the feature mappings of a set of nodes without changing the source code.
-}
defaultFeatureTraceRecording :: (Grammar g, Show a, Eq a) => FeatureTraceRecording g a
defaultFeatureTraceRecording :: FeatureTraceRecording g a
defaultFeatureTraceRecording typeOfEdit :: EditType
typeOfEdit =
    RecordingFunction g a -> RecordingFunction g a
forall g a.
(Grammar g, Eq a, Show a) =>
RecordingFunction g a -> RecordingFunction g a
removeTheRedundanciesWeIntroduced (RecordingFunction g a -> RecordingFunction g a)
-> RecordingFunction g a -> RecordingFunction g a
forall a b. (a -> b) -> a -> b
$
    RecordingFunction g a -> RecordingFunction g a
forall g a.
Grammar g =>
RecordingFunction g a -> RecordingFunction g a
nullifyMandatory (RecordingFunction g a -> RecordingFunction g a)
-> RecordingFunction g a -> RecordingFunction g a
forall a b. (a -> b) -> a -> b
$
    case EditType
typeOfEdit of
        Identity -> RecordingFunction g a
forall g a. RecordingFunction g a
r_id
        TraceOnly -> RecordingFunction g a
forall a g. Eq a => RecordingFunction g a
r_trace
        Insert -> RecordingFunction g a
forall a g. (Show a, Eq a) => RecordingFunction g a
r_ins
        Delete -> RecordingFunction g a
forall g a. (Grammar g, Eq a, Show a) => RecordingFunction g a
r_del
        Move -> RecordingFunction g a
forall a g. (Show a, Eq a) => RecordingFunction g a
r_move
        Update -> RecordingFunction g a
forall a g. (Eq a, Show a) => RecordingFunction g a
r_up

{- |
Sets the feature mapping of all mandatory AST nodes to /null/.
-}
nullifyMandatory :: (Grammar g) => RecordingFunction g a -> RecordingFunction g a
nullifyMandatory :: RecordingFunction g a -> RecordingFunction g a
nullifyMandatory wrappee :: RecordingFunction g a
wrappee = \redit :: RecordedEdit g a
redit version :: Version g a
version -> \v :: Node g a
v ->
    if Node g a -> NodeType
forall g a. Grammar g => Node g a -> NodeType
optionaltype Node g a
v NodeType -> NodeType -> Bool
forall a. Eq a => a -> a -> Bool
== NodeType
Mandatory
    then Maybe (PropositionalFormula Feature)
forall a. Maybe a
Nothing
    else RecordingFunction g a
wrappee RecordedEdit g a
redit Version g a
version Node g a
v

{- |
This simplifies feature traces with respect to presence conditions.
See 'FeatureTrace.simplifyFeatureTrace' and 'Simplify.removeRedundancy' for further information.
-}
removeTheRedundanciesWeIntroduced :: (Grammar g, Eq a, Show a) => RecordingFunction g a -> RecordingFunction g a
removeTheRedundanciesWeIntroduced :: RecordingFunction g a -> RecordingFunction g a
removeTheRedundanciesWeIntroduced wrappee :: RecordingFunction g a
wrappee = \redit :: RecordedEdit g a
redit@(edit :: Edit g a
edit, _) version :: Version g a
version@(_, t_old :: AST g a
t_old) ->
    let f_new :: FeatureTrace g a
f_new = RecordingFunction g a
wrappee RecordedEdit g a
redit Version g a
version
        t_new :: AST g a
t_new = Edit g a -> AST g a -> AST g a
forall g a. Edit g a -> AST g a -> AST g a
run Edit g a
edit AST g a
t_old
        d :: Set (Node g a)
d = Edit g a -> AST g a -> Set (Node g a)
forall g a. Edit g a -> AST g a -> Set (Node g a)
delta Edit g a
edit AST g a
t_old in
        FeatureTrace g a -> AST g a -> Set (Node g a) -> FeatureTrace g a
forall g a.
(Grammar g, Show a, Eq a) =>
FeatureTrace g a -> AST g a -> Set (Node g a) -> FeatureTrace g a
FeatureTrace.simplifyFeatureTraceOfNodes FeatureTrace g a
f_new AST g a
t_new Set (Node g a)
d

{- |
Feature trace recording for identity edit:
When nothing is changed, nothing has to be recorded.
-}
r_id :: RecordingFunction g a
r_id :: RecordingFunction g a
r_id _ (f_old :: FeatureTrace g a
f_old, _) = FeatureTrace g a
f_old

{- |
Feature trace recording on an identity edit with non-empty delta.
This function allows changing feature traces manually (i.e., without actual source code changes).
Have a look at 'Edits.edit_trace_only' for further information.
-}
r_trace :: (Eq a) => RecordingFunction g a
r_trace :: RecordingFunction g a
r_trace (edit :: Edit g a
edit, context :: Maybe (PropositionalFormula Feature)
context) (f_old :: FeatureTrace g a
f_old, t_old :: AST g a
t_old) =
    let d :: Set (Node g a)
d = Edit g a -> AST g a -> Set (Node g a)
forall g a. Edit g a -> AST g a -> Set (Node g a)
delta Edit g a
edit AST g a
t_old in
    \v :: Node g a
v ->
        if Node g a -> Set (Node g a) -> Bool
forall a. Ord a => a -> Set a -> Bool
member Node g a
v Set (Node g a)
d
        then Maybe (PropositionalFormula Feature)
context
        else FeatureTrace g a
f_old Node g a
v

{- The recording functions from Section 4 in the paper. -}

-- | Equation 2 in the paper: R_ins records feature traces upon insertions. 
r_ins :: (Show a, Eq a) => RecordingFunction g a
r_ins :: RecordingFunction g a
r_ins (edit :: Edit g a
edit, context :: Maybe (PropositionalFormula Feature)
context) (f_old :: FeatureTrace g a
f_old, t_old :: AST g a
t_old) =
    \v :: Node g a
v ->
        if Node g a -> Set (Node g a) -> Bool
forall a. Ord a => a -> Set a -> Bool
member Node g a
v (Set (Node g a) -> Bool) -> Set (Node g a) -> Bool
forall a b. (a -> b) -> a -> b
$ Edit g a -> AST g a -> Set (Node g a)
forall g a. Edit g a -> AST g a -> Set (Node g a)
delta Edit g a
edit AST g a
t_old
        then Maybe (PropositionalFormula Feature)
context
        else FeatureTrace g a
f_old Node g a
v

-- | Equation 2 in the paper: R_del records feature traces upon deletions. 
r_del :: (Grammar g, Eq a, Show a) => RecordingFunction g a
r_del :: RecordingFunction g a
r_del (edit :: Edit g a
edit, context :: Maybe (PropositionalFormula Feature)
context) (f_old :: FeatureTrace g a
f_old, t_old :: AST g a
t_old) =
    \v :: Node g a
v ->
        let pcv :: Maybe (PropositionalFormula Feature)
pcv = AST g a -> FeatureTrace g a -> FeatureTrace g a
forall g a.
(Grammar g, Show a, Eq a) =>
AST g a -> FeatureTrace g a -> FeatureTrace g a
pc AST g a
t_old FeatureTrace g a
f_old Node g a
v in
        if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Node g a -> Set (Node g a) -> Bool
forall a. Ord a => a -> Set a -> Bool
member Node g a
v (Set (Node g a) -> Bool) -> Set (Node g a) -> Bool
forall a b. (a -> b) -> a -> b
$ Edit g a -> AST g a -> Set (Node g a)
forall g a. Edit g a -> AST g a -> Set (Node g a)
delta Edit g a
edit AST g a
t_old
        then FeatureTrace g a
f_old Node g a
v
        else (if Maybe (PropositionalFormula Feature) -> Bool
forall a. NullableFormula a -> Bool
isnull Maybe (PropositionalFormula Feature)
context Bool -> Bool -> Bool
&& Bool -> Bool
not (Maybe (PropositionalFormula Feature) -> Bool
forall a. NullableFormula a -> Bool
isnull Maybe (PropositionalFormula Feature)
pcv)
              then Maybe (PropositionalFormula Feature)
forall l. Logic l => l
lfalse
              {-
              Due to our logical operators with null,
              two of the cases of R_del in the paper can actually be collapsed
              into this single formula.
              -}
              else [Maybe (PropositionalFormula Feature)]
-> Maybe (PropositionalFormula Feature)
forall l. Logic l => [l] -> l
land [Maybe (PropositionalFormula Feature)
pcv, Maybe (PropositionalFormula Feature)
-> Maybe (PropositionalFormula Feature)
forall l. Logic l => l -> l
lnot Maybe (PropositionalFormula Feature)
context] 
        )

-- | Equation 3 in the paper: R_move records feature traces upon moves. 
r_move :: (Show a, Eq a) => RecordingFunction g a
r_move :: RecordingFunction g a
r_move (edit :: Edit g a
edit, context :: Maybe (PropositionalFormula Feature)
context) (f_old :: FeatureTrace g a
f_old, t_old :: AST g a
t_old) =
    \v :: Node g a
v ->
        if Node g a -> Set (Node g a) -> Bool
forall a. Ord a => a -> Set a -> Bool
member Node g a
v (Set (Node g a) -> Bool) -> Set (Node g a) -> Bool
forall a b. (a -> b) -> a -> b
$ Edit g a -> AST g a -> Set (Node g a)
forall g a. Edit g a -> AST g a -> Set (Node g a)
delta Edit g a
edit AST g a
t_old
        then [Maybe (PropositionalFormula Feature)]
-> Maybe (PropositionalFormula Feature)
forall l. Logic l => [l] -> l
land [FeatureTrace g a
f_old Node g a
v, Maybe (PropositionalFormula Feature)
context]
        else FeatureTrace g a
f_old Node g a
v

-- | Equation 5 in the paper: R_up records feature traces upon updates. 
r_up :: (Eq a, Show a) => RecordingFunction g a
r_up :: RecordingFunction g a
r_up (edit :: Edit g a
edit, context :: Maybe (PropositionalFormula Feature)
context) (f_old :: FeatureTrace g a
f_old, t_old :: AST g a
t_old) =
    \v :: Node g a
v ->
        if (Maybe (PropositionalFormula Feature) -> Bool
forall a. NullableFormula a -> Bool
notnull Maybe (PropositionalFormula Feature)
context) Bool -> Bool -> Bool
&& (Node g a -> Set (Node g a) -> Bool
forall a. Ord a => a -> Set a -> Bool
member Node g a
v (Set (Node g a) -> Bool) -> Set (Node g a) -> Bool
forall a b. (a -> b) -> a -> b
$ Edit g a -> AST g a -> Set (Node g a)
forall g a. Edit g a -> AST g a -> Set (Node g a)
delta Edit g a
edit AST g a
t_old)
        then Maybe (PropositionalFormula Feature)
context
        else FeatureTrace g a
f_old Node g a
v