{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ViewPatterns     #-}
-- | Implements naive substitution functions for replacing type and term variables.
module PlutusIR.Transform.Substitute (
      substVar
    , substTyVar
    , typeSubstTyNames
    , termSubstNames
    , termSubstTyNames
    , bindingSubstNames
    , bindingSubstTyNames
    ) where

import PlutusIR

import PlutusCore.Subst (substTyVar, typeSubstTyNames)

import Control.Lens

import Data.Maybe

-- Needs to be different from the PLC version since we have different Terms
-- | Replace a variable using the given function.
substVar :: (name -> Maybe (Term tyname name uni fun a)) -> Term tyname name uni fun a -> Maybe (Term tyname name uni fun a)
substVar :: (name -> Maybe (Term tyname name uni fun a))
-> Term tyname name uni fun a -> Maybe (Term tyname name uni fun a)
substVar name -> Maybe (Term tyname name uni fun a)
nameF (Var a
_ name
n) = name -> Maybe (Term tyname name uni fun a)
nameF name
n
substVar name -> Maybe (Term tyname name uni fun a)
_     Term tyname name uni fun a
_         = Maybe (Term tyname name uni fun a)
forall a. Maybe a
Nothing

-- | Naively substitute names using the given functions (i.e. do not substitute binders).
termSubstNames :: (name -> Maybe (Term tyname name uni fun a)) -> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstNames :: (name -> Maybe (Term tyname name uni fun a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstNames name -> Maybe (Term tyname name uni fun a)
nameF = ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall a b. ASetter a b a b -> (b -> b) -> a -> b
transformOf ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Term tyname name uni fun a) (Term tyname name uni fun a)
termSubterms (\Term tyname name uni fun a
x -> Term tyname name uni fun a
-> Maybe (Term tyname name uni fun a) -> Term tyname name uni fun a
forall a. a -> Maybe a -> a
fromMaybe Term tyname name uni fun a
x ((name -> Maybe (Term tyname name uni fun a))
-> Term tyname name uni fun a -> Maybe (Term tyname name uni fun a)
forall name tyname (uni :: * -> *) fun a.
(name -> Maybe (Term tyname name uni fun a))
-> Term tyname name uni fun a -> Maybe (Term tyname name uni fun a)
substVar name -> Maybe (Term tyname name uni fun a)
nameF Term tyname name uni fun a
x))

-- | Naively substitute type names using the given functions (i.e. do not substitute binders).
termSubstTyNames :: (tyname -> Maybe (Type tyname uni a)) -> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstTyNames :: (tyname -> Maybe (Type tyname uni a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstTyNames tyname -> Maybe (Type tyname uni a)
tynameF = ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Term tyname name uni fun a) (Term tyname name uni fun a)
termSubterms ((tyname -> Maybe (Type tyname uni a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
forall tyname (uni :: * -> *) a name fun.
(tyname -> Maybe (Type tyname uni a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstTyNames tyname -> Maybe (Type tyname uni a)
tynameF) (Term tyname name uni fun a -> Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Type tyname uni a)
  (Type tyname uni a)
-> (Type tyname uni a -> Type tyname uni a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Type tyname uni a)
  (Type tyname uni a)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Term tyname name uni fun a) (Type tyname uni a)
termSubtypes ((tyname -> Maybe (Type tyname uni a))
-> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
(tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
typeSubstTyNames tyname -> Maybe (Type tyname uni a)
tynameF)

-- | Naively substitute names using the given functions (i.e. do not substitute binders).
bindingSubstNames :: (name -> Maybe (Term tyname name uni fun a)) -> Binding tyname name uni fun a -> Binding tyname name uni fun a
bindingSubstNames :: (name -> Maybe (Term tyname name uni fun a))
-> Binding tyname name uni fun a -> Binding tyname name uni fun a
bindingSubstNames name -> Maybe (Term tyname name uni fun a)
nameF = ASetter
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Binding tyname name uni fun a
-> Binding tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Binding tyname name uni fun a) (Term tyname name uni fun a)
bindingSubterms ((name -> Maybe (Term tyname name uni fun a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
forall name tyname (uni :: * -> *) fun a.
(name -> Maybe (Term tyname name uni fun a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstNames name -> Maybe (Term tyname name uni fun a)
nameF)

-- | Naively substitute type names using the given functions (i.e. do not substitute binders).
bindingSubstTyNames :: (tyname -> Maybe (Type tyname uni a)) -> Binding tyname name uni fun a -> Binding tyname name uni fun a
bindingSubstTyNames :: (tyname -> Maybe (Type tyname uni a))
-> Binding tyname name uni fun a -> Binding tyname name uni fun a
bindingSubstTyNames tyname -> Maybe (Type tyname uni a)
tynameF = ASetter
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Binding tyname name uni fun a
-> Binding tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Binding tyname name uni fun a) (Term tyname name uni fun a)
bindingSubterms ((tyname -> Maybe (Type tyname uni a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
forall tyname (uni :: * -> *) a name fun.
(tyname -> Maybe (Type tyname uni a))
-> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstTyNames tyname -> Maybe (Type tyname uni a)
tynameF) (Binding tyname name uni fun a -> Binding tyname name uni fun a)
-> (Binding tyname name uni fun a -> Binding tyname name uni fun a)
-> Binding tyname name uni fun a
-> Binding tyname name uni fun a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Type tyname uni a)
  (Type tyname uni a)
-> (Type tyname uni a -> Type tyname uni a)
-> Binding tyname name uni fun a
-> Binding tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Type tyname uni a)
  (Type tyname uni a)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Binding tyname name uni fun a) (Type tyname uni a)
bindingSubtypes ((tyname -> Maybe (Type tyname uni a))
-> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
(tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
typeSubstTyNames tyname -> Maybe (Type tyname uni a)
tynameF)