{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

-- | Reduction algorithm.
--
-- Preserves ranges and taints affected values.
module Descript.BasicInj.Process.Reduce.SrcAnn
  ( interpret
  , reducePhase
  , reduceReg
  ) where

import Descript.BasicInj.Process.Reduce.PropTrans
import Descript.BasicInj.Process.Reduce.Match
import qualified Descript.BasicInj.Data.Value.Reg as Reg
import qualified Descript.BasicInj.Data.Value.In as In
import qualified Descript.BasicInj.Data.Value.Out as Out
import Descript.BasicInj.Data
import Descript.Misc
import Data.Monoid
import Core.Data.Functor
import Data.Functor.Identity
import Data.Foldable
import Data.Proxy
import Data.Maybe
import Core.Data.List
import Core.Data.List.Assoc hiding (Value)
import qualified Data.List.NonEmpty as NonEmpty
import Control.Monad
import Control.Monad.Trans.Writer

-- | Interprets the program - reduces its query using its reducers.
interpret :: (TaintAnn an) => Depd Program an -> Reg.Value an
interpret dprog = reduceReg phase0 qval
  where phase0 = reduceAppPhases $ reduceCtx $ dmodule dprog
        qval = queryVal $ dquery dprog

-- | Macro-reduces each of the phases using reducers from the above
-- phase, adding reducers from the above phase along the way, then
-- returns the last phase (which will reduce the query).
reduceAppPhases :: ReduceCtx () -> PhaseCtx ()
reduceAppPhases (ReduceCtx () t xs) = foldl' reduceAppPhase t $ NonEmpty.toList xs

-- | Macro-reduces the second phase using reducers from the first.
-- Then combines the phases.
reduceAppPhase :: PhaseCtx () -> PhaseCtx () -> PhaseCtx ()
reduceAppPhase mctx x = mctx <> reducePhase mctx x

-- | Macro-reduces the second phase using reducers from the first.
reducePhase :: (TaintAnn an) => PhaseCtx () -> PhaseCtx an -> PhaseCtx an
reducePhase mctx (PhaseCtx ann xs)
  = PhaseCtx ann $ map (reduceReducer mctx) xs

-- | Macro-reduces the input and output (ctx is macros).
reduceReducer :: (TaintAnn an) => PhaseCtx () -> Reducer an -> Reducer an
reduceReducer ctx (Reducer ann input' output')
  = reduceReducerOut ctx ann (reduceInput' ctx input') output'

-- | Continues reducing the output using effects from the reduced input,
-- then creates the reduced reducer.
reduceReducerOut :: (TaintAnn an)
                 => PhaseCtx ()
                 -> an
                 -> (In.Value an, PropTranses)
                 -> Out.Value an
                 -> Reducer an
reduceReducerOut ctx ann (newIn, outTranses) output'
  = Reducer ann newIn newOut
  where newOut = reduceOutput ctx $ apPropTranses newIn_ outTranses output'
        newIn_ = remAnns newIn

-- | Applies the context's reducers to the value, until they can't
-- be applied anymore.
reduceReg :: (TaintAnn an)
          => PhaseCtx ()
          -> Reg.Value an
          -> Reg.Value an
reduceReg = reduceNorm

-- | Applies the context's reducers to the output value, until they
-- can't be applied anymore.
reduceOutput :: (TaintAnn an)
             => PhaseCtx ()
             -> Out.Value an
             -> Out.Value an
reduceOutput = reduceNorm

-- | Applies the context's reducers to the value, until they can't be
-- applied anymore.
reduceNorm :: (NormReducePart p, TaintAnn an)
           => PhaseCtx ()
           -> GenValue p an
           -> GenValue p an
reduceNorm ctx = reduceRest reduceNorm ctx . reduceProps ctx

-- | Applies the context's reducers to the input value, until they can't
-- be applied anymore.
--
-- This also returns transformers which should be applied to the output.
-- Every time a record in the input matches, the corresponding property
-- in the output is transformed to a union of all the locations of that
-- property in the reducer's output.
reduceInput' :: (TaintAnn an)
             => PhaseCtx ()
             -> In.Value an
             -> (In.Value an, PropTranses)
reduceInput' ctx = runWriter . reduceInput ctx

reduceInput :: (TaintAnn an)
            => PhaseCtx ()
            -> In.Value an
            -> Writer PropTranses (In.Value an)
reduceInput ctx = reduceInRest reduceInput ctx <=< reduceInProps ctx

-- | Applies the context's reducers to the value's properties,
-- until they can't be applied anymore.
reduceProps :: (NormReducePart p, TaintAnn an)
            => PhaseCtx ()
            -> GenValue p an
            -> GenValue p an
reduceProps ctx (Value ann parts)
  = Value ann $ map (reducePartProps ctx) parts

reduceInProps :: (TaintAnn an)
              => PhaseCtx ()
              -> In.Value an
              -> Writer PropTranses (In.Value an)
reduceInProps ctx (Value ann parts)
  = Value ann <$> traverse (reduceInPartProps ctx) parts

class (ReducePart p, (PartPropVal p ~ GenValue p)) => NormReducePart p where
  reducePartProps :: (TaintAnn an) => PhaseCtx () -> p an -> p an

instance NormReducePart Reg.Part where
  reducePartProps _ (Reg.PartPrim prim) = Reg.PartPrim prim
  reducePartProps ctx (Reg.PartRecord record)
    = Reg.PartRecord $ reduceRecordProps ctx record

reduceInPartProps :: (TaintAnn an)
                  => PhaseCtx ()
                  -> In.Part an
                  -> Writer PropTranses (In.Part an)
reduceInPartProps _ (In.PartPrim prim) = pure $ In.PartPrim prim
reduceInPartProps _ (In.PartPrimType ptype) = pure $ In.PartPrimType ptype
reduceInPartProps ctx (In.PartRecord record)
  = In.PartRecord <$> reduceInRecordProps ctx record

instance NormReducePart Out.Part where
  reducePartProps _ (Out.PartPrim prim) = Out.PartPrim prim
  reducePartProps ctx (Out.PartRecord record)
    = Out.PartRecord $ reduceOutRecordProps ctx record
  reducePartProps _ (Out.PartPropPath path) = Out.PartPropPath path
  reducePartProps ctx (Out.PartInjApp app)
    = Out.PartInjApp $ reduceInjAppProps ctx app

reduceRecordProps :: (TaintAnn an)
                  => PhaseCtx ()
                  -> Reg.Record an
                  -> Reg.Record an
reduceRecordProps = mapPropVals . reduceReg

reduceInRecordProps :: (TaintAnn an)
                    => PhaseCtx ()
                    -> In.Record an
                    -> Writer PropTranses (In.Record an)
reduceInRecordProps ctx (Record ann head' props)
  = Record ann head' <$> traverse (reduceInRecordProp ctx head_) props
  where head_ = remAnns head'

reduceInRecordProp :: (TaintAnn an)
                   => PhaseCtx ()
                   -> FSymbol ()
                   -> In.Property an
                   -> Writer PropTranses (In.Property an)
reduceInRecordProp ctx head_ (Property ann key val)
    = Property ann key <$> val'
  where val'
          = censor (subPropTranses pelem)
          $ In.traverseOptVal (reduceInput ctx) val
        pelem = PathElem () key_ head_
        key_ = remAnns key

reduceOutRecordProps :: (TaintAnn an)
                     => PhaseCtx ()
                     -> Out.Record an
                     -> Out.Record an
reduceOutRecordProps = mapPropVals . reduceOutput

reduceInjAppProps :: (TaintAnn an)
                  => PhaseCtx ()
                  -> Out.InjApp an
                  -> Out.InjApp an
reduceInjAppProps = Out.mapInjAppParams . Out.mapInjParamVal . reduceOutput

-- | Applies the context's reducers to the value's head.
-- If the value reduced, applies the given reducer to reduce it more.
-- Otherwise just returns it as-is.
reduceRest :: (NormReducePart p, TaintAnn an)
           => (PhaseCtx () -> GenValue p an -> GenValue p an)
           -> PhaseCtx () -> GenValue p an -> GenValue p an
reduceRest reduceMore ctx value
  = case reduceOnce ctx value of
         Failure () -> value
         Success next -> reduceMore ctx next

reduceInRest :: (TaintAnn an)
             => (PhaseCtx () -> In.Value an -> Writer PropTranses (In.Value an))
             -> PhaseCtx () -> In.Value an -> Writer PropTranses (In.Value an)
reduceInRest reduceInMore ctx value
  = mapWriterT continue $ reduceInOnce ctx value
  where continue = runWriterT . continue'
        continue' (Failure ()) = pure value
        continue' (Success (next, effTrs)) = do
          tell effTrs
          reduceInMore ctx next

-- | Applies the context's reducers to the value once, returning a new
-- value if it reduced, or a failure if it couldn't be reduced at all.
reduceOnce :: (NormReducePart p, TaintAnn an)
           => PhaseCtx ()
           -> GenValue p an
           -> UResult (GenValue p an)
reduceOnce ctx value
  | next =@= value = Failure ()
  | otherwise = Success next
  where next = tryReduceOnce ctx value

reduceInOnce :: (TaintAnn an)
             => PhaseCtx ()
             -> In.Value an
             -> WriterT PropTranses (Result ()) (In.Value an)
reduceInOnce ctx value
  = mapWriterT continue $ tryReduceInOnce ctx value
  where continue = continue' . runIdentity
        continue' (next, effTrs)
          | next =@= value = Failure ()
          | otherwise = Success (next, effTrs)

-- | Applies the context's reducers to the value once. If none of them
-- could be applied (the value didn't reduce), just returns the same value.
tryReduceOnce :: (NormReducePart p, TaintAnn an)
              => PhaseCtx ()
              -> GenValue p an
              -> GenValue p an
tryReduceOnce (PhaseCtx () reducers) value
  = foldl' (flip tryReduceIndiv) value reducers

tryReduceInOnce :: (TaintAnn an)
                => PhaseCtx ()
                -> In.Value an
                -> Writer PropTranses (In.Value an)
tryReduceInOnce (PhaseCtx () reducers) value
  = foldM (flip tryReduceInIndiv) value reducers

-- | Applies the individual reducer to the value if it can be applied.
-- Otherwise just returns the value.
tryReduceIndiv :: (NormReducePart p, TaintAnn an)
               => Reducer ()
               -> GenValue p an
               -> GenValue p an
tryReduceIndiv reducer value
  = case reduceIndiv reducer value of
         Failure () -> value
         Success next -> next

tryReduceInIndiv :: (TaintAnn an)
                 => Reducer ()
                 -> In.Value an
                 -> Writer PropTranses (In.Value an)
tryReduceInIndiv reducer value
  = mapWriterT continue $ reduceInIndiv reducer value
  where continue = Identity . continue'
        continue' (Failure ()) = (value, [])
        continue' (Success (next, effTrs)) = (next, effTrs)

-- | Applies the individual reducer to the value if it can be applied.
-- Otherwise returns a failure.
reduceIndiv :: (NormReducePart p, TaintAnn an)
            => Reducer ()
            -> GenValue p an
            -> UResult (GenValue p an)
reduceIndiv reducer
  = fmap (produce $ output reducer)
  . consume (input reducer)

reduceInIndiv :: (TaintAnn an)
              => Reducer ()
              -> In.Value an
              -> WriterT PropTranses (Result ()) (In.Value an)
reduceInIndiv reducer
  = WriterT
  . fmap (produceIn $ output reducer)
  . consume (input reducer)

-- | Tries to match the input value to the given value.
consume :: (ReducePart p, TaintAnn an)
        => In.Value ()
        -> GenValue p an
        -> UResult (Match (GenValue p an))
consume (Value () inParts) value
  = foldM (flip consumePartInMatch) (emptyValMatch value) inParts

emptyValMatch :: (Ann v, TaintAnn an)
              => GenValue v an
              -> Match (GenValue v an)
emptyValMatch x
  = Match
  { matched = Value (taint $ postInsertAnn $ getAnn x) []
  , leftover = x
  }

consumePartInMatch :: (ReducePart p, TaintAnn an)
                   => In.Part ()
                   -> Match (GenValue p an)
                   -> UResult (Match (GenValue p an))
consumePartInMatch = matchAgainF . consumePartInValue

consumePartInValue :: (ReducePart p, TaintAnn an)
                   => In.Part ()
                   -> GenValue p an
                   -> UResult (Match (GenValue p an))
consumePartInValue (In.PartPrim inPrim) (Value ann parts)
  = reValue ann parts <<$>> consumePrimInParts inPrim parts
consumePartInValue (In.PartPrimType inType) (Value ann parts)
  = reValue ann parts <<$>> consumePrimTypeInParts inType parts
consumePartInValue (In.PartRecord inRec) (Value ann parts)
  = reValue ann parts <<$>> consumeRecordInParts inRec parts

consumePrimInParts :: (ReducePart p, TaintAnn an)
                   => Prim ()
                   -> [p an]
                   -> UResult (Match [p an])
consumePrimInParts _ [] = Failure ()
consumePrimInParts inPrim (part : parts)
  | inPart /@= part
  = mapLeftover (part :) <$> consumePrimInParts inPrim parts
  | otherwise
  = Success Match
  { matched = [part]
  , leftover = parts
  }
  where inPart = primToPart Proxy inPrim

consumePrimTypeInParts :: (ReducePart p, TaintAnn an)
                       => PrimType ()
                       -> [p an]
                       -> UResult (Match [p an])
consumePrimTypeInParts _ [] = Failure ()
consumePrimTypeInParts inType (part : parts)
  = case consumePrimTypeInPart inType part of
         Failure ()
            -> mapLeftover (part :)
           <$> consumePrimTypeInParts inType parts
         Success ()
           -> Success Match
            { matched = [part]
            , leftover = parts
            }

consumePrimTypeInPart :: (ReducePart p, TaintAnn an)
                      => PrimType ()
                      -> p an
                      -> UResult ()
consumePrimTypeInPart inType part
  = case partToPrim part of
         Nothing -> Failure ()
         Just prim
           | prim `isPrimInstance` inType -> Success ()
           | otherwise -> Failure ()

consumeRecordInParts :: (ReducePart p, TaintAnn an)
                     => In.Record ()
                     -> [p an]
                     -> UResult (Match [p an])
consumeRecordInParts _ [] = Failure ()
consumeRecordInParts inRec (part : parts)
  = case consumeRecordInPart inRec part of
         Failure ()
            -> mapLeftover (part :)
           <$> consumeRecordInParts inRec parts
         Success (Match partMatch partLeftover)
           -> Success Match
            { matched = maybeToList partMatch
            , leftover = partLeftover ?: parts
            }

consumeRecordInPart :: (ReducePart p, TaintAnn an)
                    => In.Record ()
                    -> p an
                    -> UResult (Match (Maybe (p an)))
consumeRecordInPart inRec part
  = case partToRec part of
         Nothing -> Failure ()
         Just record -> recToPart Proxy <<<$>>> consumeRecord inRec record

class (GenPart p, ReducePropVal (PartPropVal p)) => ReducePart p where

instance ReducePart Reg.Part
instance ReducePart In.Part
instance ReducePart Out.Part

consumeRecord :: (ReducePropVal v, TaintAnn an)
              => In.Record ()
              -> GenRecord v an
              -> UResult (Match (Maybe (GenRecord v an)))
consumeRecord (Record () inRecHead inRecProps) (Record ann recHead recProps)
        | inRecHead /@= recHead = Failure ()
        | otherwise
        = reRecord ann recHead recProps
  <<<$>>> bimapMatch Just justIfNonEmptyList
      <$> consumeProperties inRecProps recProps

consumeProperties :: (ReducePropVal v, TaintAnn an)
                  => [In.Property ()]
                  -> [GenProperty v an]
                  -> UResult (Match [GenProperty v an])
consumeProperties _ [] = Success $ pure []
consumeProperties inProps (prop : props)
  = case consumePropertiesInProperty inProps prop of
         Failure () -> Failure ()
         Success match
            -> addPropValMatch prop match
           <$> consumeProperties inProps props

consumePropertiesInProperty :: (ReducePropVal v, TaintAnn an)
                            => [In.Property ()]
                            -> GenProperty v an
                            -> UResult (Match (Maybe (v an)))
consumePropertiesInProperty inProps (Property _ propKey propVal)
  = case glookupForce propKey_ inProps of
         In.NothingValue
           -> Success Match
            { matched = Just propVal
            , leftover = Nothing
            }
         In.JustValue inPropVal
            -> bimapMatch Just justIfNonEmptyPropVal
           <$> consumePropVal inPropVal propVal
  where propKey_ = remAnns propKey

addPropValMatch :: (GenPropVal v, TaintAnn an)
                => GenProperty v an
                -> Match (Maybe (v an))
                -> Match [GenProperty v an]
                -> Match [GenProperty v an]
addPropValMatch (Property ann propKey oldPropVal) newPropVal props
  = (?:) <$> prop <*> props
  where prop = reProperty ann propKey oldPropVal <<$>> newPropVal

class (GenPropVal v) => ReducePropVal v where
  consumePropVal :: (TaintAnn an)
                 => In.Value ()
                 -> v an
                 -> UResult (Match (v an))
  justIfNonEmptyPropVal :: v an -> Maybe (v an)

instance (ReducePart p) => ReducePropVal (GenValue p) where
  consumePropVal = consume
  justIfNonEmptyPropVal = justIfNonEmptyVal

instance ReducePropVal In.OptValue where
  consumePropVal = consumeOptVal
  justIfNonEmptyPropVal = justIfNonEmptyOptVal

consumeOptVal :: (TaintAnn an)
              => In.Value ()
              -> In.OptValue an
              -> UResult (Match (In.OptValue an))
consumeOptVal _ In.NothingValue = Failure ()
consumeOptVal input' (In.JustValue x)
  = In.JustValue <<$>> consume input' x

justIfNonEmptyOptVal :: In.OptValue an -> Maybe (In.OptValue an)
justIfNonEmptyOptVal In.NothingValue = Just In.NothingValue
justIfNonEmptyOptVal (In.JustValue x) = In.JustValue <$> justIfNonEmptyVal x

justIfNonEmptyVal :: GenValue v an -> Maybe (GenValue v an)
justIfNonEmptyVal x
  | isEmpty x = Nothing
  | otherwise = Just x

justIfNonEmptyList :: [a] -> Maybe [a]
justIfNonEmptyList x
  | null x = Nothing
  | otherwise = Just x

-- | Resolves the property paths in the output value using the given
-- value, and combines the result with the given value.
produce :: (TaintAnn an)
        => (NormReducePart p)
        => Out.Value ()
        -> Match (GenValue p an)
        -> GenValue p an
produce output' (Match matched' leftover')
  = leftover' `appGend` resolve output' matched_
  where matched_ = remAnns matched'

produceIn :: (TaintAnn an)
          => Out.Value ()
          -> Match (In.Value an)
          -> (In.Value an, PropTranses)
produceIn output' match
  = (produceInMain output' match, transProps output' matched_)
  where matched_ = remAnns $ matched match

-- | Resolves the property paths in the output value using the given
-- value, and combines the result with the given value.
produceInMain :: (TaintAnn an)
              => Out.Value ()
              -> Match (In.Value an)
              -> In.Value an
produceInMain output' (Match matched' leftover')
  = leftover' `appGend` resolveIn' output' matched_
  where matched_ = remAnns matched'

-- | Resolves all property paths in the output value using the given value.
-- Replaces all paths with the corresponding properties in the given
-- value.
resolve :: (NormReducePart p)
        => Out.Value ()
        -> GenValue p ()
        -> GenValue p ()
resolve (Value () outParts) value
  = mconcat $ map resolvePart outParts
  where resolvePart (Out.PartPrim prim)
          = singletonValue $ primToPart Proxy prim
        resolvePart (Out.PartRecord record)
          = singletonValue
          $ recToPart Proxy
          $ mapPropVals (`resolve` value)
            record
        resolvePart (Out.PartPropPath path) = resolvePropPath path value
        resolvePart (Out.PartInjApp app) = resolveInjApp app value

resolveIn' :: Out.Value () -> In.Value () -> In.Value ()
resolveIn' output' value
  = case resolveIn output' $ In.JustValue value of
         In.NothingValue -> error "Bad macro - reduces input to free bind"
         In.JustValue x -> x

resolveIn :: Out.Value ()
          -> In.OptValue ()
          -> In.OptValue ()
resolveIn (Value () outParts) value
  = mconcat $ map resolvePart outParts
  where resolvePart (Out.PartPrim prim)
          = In.JustValue $ singletonValue $ primToPart Proxy prim
        resolvePart (Out.PartRecord record)
          = In.JustValue
          $ singletonValue
          $ recToPart Proxy
          $ mapPropVals (`resolveIn` value)
            record
        resolvePart (Out.PartPropPath path) = resolveInPropPath path value
        resolvePart (Out.PartInjApp app) = In.JustValue $ resolveInInjApp app value

-- | Resolves the property path using the given value.
-- Replaces it with the corresponding property in the given value.
resolvePropPath :: (NormReducePart p)
                => PropPath ()
                -> GenValue p ()
                -> GenValue p ()
resolvePropPath (PropPath () xs) = resolveSubpath $ NonEmpty.toList xs

resolveInPropPath :: PropPath ()
                  -> In.OptValue ()
                  -> In.OptValue ()
resolveInPropPath (PropPath () xs) = resolveInSubpath $ NonEmpty.toList xs

resolveSubpath :: (NormReducePart p)
               => [PathElem ()]
               -> GenValue p ()
               -> GenValue p ()
resolveSubpath [] = id
resolveSubpath (x : xs) = resolveSubpath xs . resolveElem x

resolveInSubpath :: [PathElem ()]
                 -> In.OptValue ()
                 -> In.OptValue ()
resolveInSubpath [] = id
resolveInSubpath (x : xs) = resolveInSubpath xs . resolveInElem x

resolveElem :: (NormReducePart p)
            => PathElem ()
            -> GenValue p ()
            -> GenValue p ()
resolveElem (PathElem () keyRef' headRef')
  = forceLookupProp keyRef' . forceRecWithHead headRef'

resolveInElem :: PathElem ()
              -> In.OptValue ()
              -> In.OptValue ()
resolveInElem _ In.NothingValue
  = error "Bad macro - references property of free bind"
resolveInElem (PathElem () keyRef' headRef') (In.JustValue val)
  = forceLookupProp keyRef' $ forceRecWithHead headRef' val

-- | Finds the injected function, resolves the arguments, then applies
-- the function with every possible primitive combination until it
-- returns a result.
resolveInjApp :: (NormReducePart p)
              => Out.InjApp ()
              -> GenValue p ()
              -> GenValue p ()
resolveInjApp app x = applyInj func params
  where func = forceLookupFunc $ Out.funcId app
        params = map ((`resolve` x) . Out.injParamVal) $ Out.params app

resolveInInjApp :: Out.InjApp ()
                -> In.OptValue ()
                -> In.Value ()
resolveInInjApp app x = applyInj func params
  where func = forceLookupFunc $ Out.funcId app
        params
          = mapMaybe (In.optValToMaybeVal . (`resolveIn` x) . Out.injParamVal)
          $ Out.params app

-- Applies the function with every possible primitive combination given
-- the arguments until it returns a result. Fails if no combinations work.
applyInj :: (GenPart p) => InjFunc -> [GenValue p ()] -> GenValue p ()
applyInj func params
  = case tryApplyInj func params of
         Failure () -> error "Injected function couldn't be applied to parameters"
         Success out -> out

-- Applies the function with every possible primitive combination given
-- the arguments until it returns a result.
tryApplyInj :: (GenPart p)
            => InjFunc
            -> [GenValue p ()]
            -> UResult (GenValue p ())
tryApplyInj = applyInjUsing []

applyInjUsing :: (GenPart p)
              => [Prim ()]
              -> InjFunc
              -> [GenValue p ()]
              -> UResult (GenValue p ())
applyInjUsing revSelParams func []
  = case func selParams of
         Nothing -> Failure ()
         Just out -> Success $ singletonValue $ primToPart Proxy out
  where selParams = reverse revSelParams
applyInjUsing revSelParams func (nextParam : restParams)
  = asum $ map applyInjUsingNext $ primParts nextParam
  where applyInjUsingNext nextSelParam = applyInjUsing (nextSelParam : revSelParams) func restParams

transProps :: Out.Value () -> In.Value () -> PropTranses
transProps output' = map (`transPath` output') . pathsInVal

pathsInVal :: In.Value () -> [PropPath ()]
pathsInVal (Value () parts) = concatMap pathsInPart parts

pathsInPart :: In.Part () -> [PropPath ()]
pathsInPart (In.PartPrim _) = []
pathsInPart (In.PartPrimType _) = []
pathsInPart (In.PartRecord record) = pathsInRecord record

pathsInRecord :: In.Record () -> [PropPath ()]
pathsInRecord (Record () head' props) = concatMap (pathsInProp head') props

pathsInProp :: FSymbol ()
            -> In.Property ()
            -> [PropPath ()]
pathsInProp head' (Property () key val)
  = immPath elem' : map (subPath elem') (pathsInOptVal val)
  where elem' = PathElem () key head'

pathsInOptVal :: In.OptValue () -> [PropPath ()]
pathsInOptVal In.NothingValue = []
pathsInOptVal (In.JustValue x) = pathsInVal x

transPath :: PropPath () -> Out.Value () -> PropTrans
transPath inPath = PropTrans inPath . transOutsInVal inPath

transOutsInVal :: PropPath () -> Out.Value () -> [SubPropPath ()]
transOutsInVal inPath (Value () parts) = concatMap (transOutsInPart inPath) parts

transOutsInPart :: PropPath () -> Out.Part () -> [SubPropPath ()]
transOutsInPart _ (Out.PartPrim _) = []
transOutsInPart inPath (Out.PartRecord record)
  = transOutsInRecord inPath record
transOutsInPart inPath (Out.PartPropPath path)
  = transOutsInPath inPath path
transOutsInPart inPath (Out.PartInjApp app)
  = transOutsInInjApp inPath app

transOutsInRecord :: PropPath () -> Out.Record () -> [SubPropPath ()]
transOutsInRecord inPath (Record () head' props)
  = concatMap (transOutsInProp inPath head') props

transOutsInProp :: PropPath () -> FSymbol () -> Out.Property () -> [SubPropPath ()]
transOutsInProp inPath head' (Property () key val)
  = map (elem' :) $ transOutsInVal inPath val
  where elem' = PathElem () key head'

-- | Name is misleading out of context - the old property path will
-- transform into the location of this property path if both paths are
-- equal.
transOutsInPath :: PropPath () -> PropPath () -> [SubPropPath ()]
transOutsInPath inPath path
  | inPath == path = [[]]
  | otherwise = []

transOutsInInjApp :: PropPath () -> Out.InjApp () -> [SubPropPath ()]
transOutsInInjApp _ _
  = error "Macros deconstructing injected applications is unsupported. \
          \Wrap the injected application in a regular record, then \
          \deconstruct that record instead."