{-# LANGUAGE LambdaCase #-}

module Funcons.Substitution (
    Env(..), subsAndRewritesInEnv, subsAndRewritesToValueInEnv, subsAndRewritesToValue, subsAndRewritesToValuesInEnv, subsAndRewritesToValues,
    envInsert, emptyEnv,
    Levelled(..), substitute_signal, substitute,rewriteTermTo, stepTermTo,
    envRewrite, envStore, lifted_envRewrite, lifted_envStore, 
    fLevel, fsLevel, vLevel, vsLevel, envLookup
    ) where

import Funcons.Types
import Funcons.MSOS

import Control.Applicative
import Control.Monad
import Data.Monoid
import qualified Data.Map as M

-- | An environment mapping meta-variables to funcon terms.
-- This environment is used by a substitution procedure to transform
-- funcon terms from 'FTerm' representation to 'Funcons'.
type Env = M.Map MetaVar Levelled 
data Levelled   = TypeTerm ComputationTypes
                | TypesTerm [ComputationTypes]
                | ValueTerm Values
                | ValuesTerm [Values]
                | FunconTerm Funcons (Maybe (MSOS StepRes)) {- cached step -}
                | FunconsTerm [Funcons]

-- | The empty substitution environment.
-- Bindings are inserted by pattern-matching.
emptyEnv :: Map k a
emptyEnv = Map k a
forall k a. Map k a
M.empty

envLookup :: Env -> MetaVar -> Rewrite Levelled
envLookup :: Env -> MetaVar -> Rewrite Levelled
envLookup Env
env MetaVar
k = case MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
k Env
env of
                    Maybe Levelled
Nothing -> MetaVar -> Rewrite Levelled
forall a. MetaVar -> Rewrite a
internal (MetaVar
"no substitution for variable: " MetaVar -> MetaVar -> MetaVar
forall a. Semigroup a => a -> a -> a
<> MetaVar
k)
                    Just Levelled
lf -> Levelled -> Rewrite Levelled
forall (m :: * -> *) a. Monad m => a -> m a
return Levelled
lf

envInsert :: MetaVar -> Levelled -> Env -> Env
envInsert :: MetaVar -> Levelled -> Env -> Env
envInsert = (Levelled -> Levelled -> Levelled)
-> MetaVar -> Levelled -> Env -> Env
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Levelled -> Levelled -> Levelled
forall p p. p -> p -> p
op
  where op :: p -> p -> p
op p
new p
old = p
new --TODO somehow unify values
  {- 
        isWildCard (ValueTerm VAny) = True
        isWildCard (ValuesTerm [VAny]) = True
        isWildCard (FunconTerm (FValue VAny) _) = True
        isWildCard (FunconsTerm [FValue VAny]) = True
        isWildCard _ = False
  -}
        

{-
tsLevel :: Levelled -> Rewrite [ComputationTypes]
tsLevel = \case TypesTerm ts  -> return ts
                TypeTerm t    -> return [t]
                ValuesTerm vs 
                  | all isSort_ vs -> return $ map downcastSort (map FValue vs)
                  | otherwise     -> internal "not bound to types"
                ValueTerm v | isSort_ v-> return $ [downcastSort v]
-}

vsLevel :: Levelled -> Rewrite [Values]
vsLevel :: Levelled -> Rewrite [Values]
vsLevel = \case FunconsTerm [Funcons]
fs 
                  | (Funcons -> Bool) -> [Funcons] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not(Bool -> Bool) -> (Funcons -> Bool) -> Funcons -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Funcons -> Bool
hasStep) [Funcons]
fs  -> [Values] -> Rewrite [Values]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Funcons -> Values) -> [Funcons] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
downcastValue [Funcons]
fs)
                  | Bool
otherwise           -> MetaVar -> Rewrite [Values]
forall a. MetaVar -> Rewrite a
internal MetaVar
"not bound to values"
                FunconTerm (FValue Values
v) Maybe (MSOS StepRes)
_ -> [Values] -> Rewrite [Values]
forall (m :: * -> *) a. Monad m => a -> m a
return [Values
v]
                FunconTerm Funcons
f         Maybe (MSOS StepRes)
_  -> MetaVar -> Rewrite [Values]
forall a. MetaVar -> Rewrite a
internal (MetaVar
"not bound to values")  
                ValuesTerm [Values]
vs           -> [Values] -> Rewrite [Values]
forall (m :: * -> *) a. Monad m => a -> m a
return [Values]
vs
                ValueTerm Values
v             -> [Values] -> Rewrite [Values]
forall (m :: * -> *) a. Monad m => a -> m a
return [Values
v]
                TypeTerm ComputationTypes
t              -> [Values] -> Rewrite [Values]
forall (m :: * -> *) a. Monad m => a -> m a
return [ComputationTypes -> Values
forall t. ComputationTypes t -> Values t
ComputationType ComputationTypes
t]
                TypesTerm [ComputationTypes]
ts            -> [Values] -> Rewrite [Values]
forall (m :: * -> *) a. Monad m => a -> m a
return ((ComputationTypes -> Values) -> [ComputationTypes] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map ComputationTypes -> Values
forall t. ComputationTypes t -> Values t
ComputationType [ComputationTypes]
ts)

vLevel :: Levelled -> Rewrite Values
vLevel :: Levelled -> Rewrite Values
vLevel =  \case FunconsTerm [FValue Values
v]  -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
                FunconsTerm [Funcons]
fs          -> MetaVar -> Rewrite Values
forall a. MetaVar -> Rewrite a
internal MetaVar
"not bound to values"
                FunconTerm (FValue Values
v) Maybe (MSOS StepRes)
_ -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
                FunconTerm Funcons
f         Maybe (MSOS StepRes)
_  -> MetaVar -> Rewrite Values
forall a. MetaVar -> Rewrite a
internal (MetaVar
"not bound to value")  
                ValuesTerm [Values
v]          -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
                ValuesTerm [Values]
vs           -> MetaVar -> Rewrite Values
forall a. MetaVar -> Rewrite a
internal (MetaVar
"not bound to value")  
                ValueTerm Values
v             -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
                TypeTerm ComputationTypes
t              -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return (ComputationTypes -> Values
forall t. ComputationTypes t -> Values t
ComputationType ComputationTypes
t)
                TypesTerm [ComputationTypes
t]           -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return (ComputationTypes -> Values
forall t. ComputationTypes t -> Values t
ComputationType ComputationTypes
t)
                TypesTerm [ComputationTypes]
_             -> MetaVar -> Rewrite Values
forall a. MetaVar -> Rewrite a
internal MetaVar
"not bound to a value"

fsLevel :: Levelled -> Rewrite [Funcons]
fsLevel :: Levelled -> Rewrite [Funcons]
fsLevel = \case FunconsTerm [Funcons]
f       -> [Funcons] -> Rewrite [Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return [Funcons]
f
                FunconTerm Funcons
f Maybe (MSOS StepRes)
_      -> [Funcons] -> Rewrite [Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return [Funcons
f]
                ValuesTerm [Values]
vs       -> [Funcons] -> Rewrite [Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs)
                ValueTerm Values
v         -> [Funcons] -> Rewrite [Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return [Values -> Funcons
FValue Values
v]
                TypesTerm [ComputationTypes]
ts        -> [Funcons] -> Rewrite [Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return ((ComputationTypes -> Funcons) -> [ComputationTypes] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map ComputationTypes -> Funcons
sort_ [ComputationTypes]
ts)
                TypeTerm ComputationTypes
t          -> [Funcons] -> Rewrite [Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return [ComputationTypes -> Funcons
sort_ ComputationTypes
t]

fLevel :: p -> Levelled -> Rewrite Funcons
fLevel p
k = \case    
  FunconsTerm [Funcons
f]   -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return Funcons
f
  FunconsTerm [Funcons]
fs    -> MetaVar -> Rewrite Funcons
forall a. MetaVar -> Rewrite a
internal MetaVar
"not bound to a funcon"
  FunconTerm Funcons
f Maybe (MSOS StepRes)
_    -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return Funcons
f
  ValuesTerm [Values
v]    -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (Values -> Funcons
FValue Values
v)
  ValuesTerm [Values]
vs     -> MetaVar -> Rewrite Funcons
forall a. MetaVar -> Rewrite a
internal MetaVar
"not bound to a funcon" 
  ValueTerm Values
v       -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (Values -> Funcons
FValue Values
v)
  TypeTerm ComputationTypes
t        -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (ComputationTypes -> Funcons
sort_ ComputationTypes
t)
  TypesTerm [ComputationTypes
t]     -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (ComputationTypes -> Funcons
sort_ ComputationTypes
t)
  TypesTerm [ComputationTypes]
ts      -> MetaVar -> Rewrite Funcons
forall a. MetaVar -> Rewrite a
internal MetaVar
"not bound to a funcon"

-- substitution

substitute_signal :: FTerm -> Env -> Rewrite Values
substitute_signal :: FTerm -> Env -> Rewrite Values
substitute_signal FTerm
t Env
env = case FTerm
t of
  TVar MetaVar
k        -> Levelled -> Rewrite Values
vLevel (Levelled -> Rewrite Values) -> Levelled -> Rewrite Values
forall a b. (a -> b) -> a -> b
$ Env -> MetaVar -> Levelled
envMaybeLookup Env
env MetaVar
k
  TName Name
nm      -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
nm [])
  TApp Name
nm [FTerm]
terms -> Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
nm ([Funcons] -> Values)
-> ([Values] -> [Funcons]) -> [Values] -> Values
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue  ([Values] -> Values) -> Rewrite [Values] -> Rewrite Values
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FTerm] -> Env -> Rewrite [Values]
subs_flatten [FTerm]
terms Env
env
  TSeq [FTerm]
ts       -> MetaVar -> Rewrite Values
forall a. MetaVar -> Rewrite a
internal MetaVar
"top level sequence during substitution (signal)" 
--  TList ts      -> List <$> subs_flatten ts env
  TSet [FTerm]
ts       -> [Values] -> Values
setval_ ([Values] -> Values) -> Rewrite [Values] -> Rewrite Values
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FTerm] -> Env -> Rewrite [Values]
subs_flatten [FTerm]
ts Env
env
  TMap [FTerm]
ts       -> [Values] -> Values
mapval_ ([Values] -> Values) -> Rewrite [Values] -> Rewrite Values
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FTerm] -> Env -> Rewrite [Values]
subs_flatten [FTerm]
ts Env
env
  TBinding FTerm
x FTerm
y  -> [Values] -> Values
forall t. HasValues t => [Values t] -> Values t
tuple ([Values] -> Values) -> Rewrite [Values] -> Rewrite Values
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FTerm] -> Env -> Rewrite [Values]
subs_flatten [FTerm
x,FTerm
y] Env
env
  TFuncon (FValue Values
v) -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
  FTerm
TAny          -> Values -> Rewrite Values
forall (m :: * -> *) a. Monad m => a -> m a
return Values
forall t. Values t
VAny
  FTerm
_             -> MetaVar -> Rewrite Values
forall a. MetaVar -> Rewrite a
internal MetaVar
"missing case in substitute_signal"
  where subs_flatten :: [FTerm] -> Env -> Rewrite [Values]
        subs_flatten :: [FTerm] -> Env -> Rewrite [Values]
subs_flatten [FTerm]
terms Env
env = ([[Values]] -> [Values]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Values]] -> [Values]) -> Rewrite [[Values]] -> Rewrite [Values]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Rewrite [[Values]] -> Rewrite [Values])
-> Rewrite [[Values]] -> Rewrite [Values]
forall a b. (a -> b) -> a -> b
$ [FTerm] -> (FTerm -> Rewrite [Values]) -> Rewrite [[Values]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FTerm]
terms ((FTerm -> Rewrite [Values]) -> Rewrite [[Values]])
-> (FTerm -> Rewrite [Values]) -> Rewrite [[Values]]
forall a b. (a -> b) -> a -> b
$ \case
              TVar MetaVar
k  -> Levelled -> Rewrite [Values]
vsLevel (Levelled -> Rewrite [Values]) -> Levelled -> Rewrite [Values]
forall a b. (a -> b) -> a -> b
$ Env -> MetaVar -> Levelled
envMaybeLookup Env
env MetaVar
k
              TSeq [FTerm]
ts -> (FTerm -> Rewrite Values) -> [FTerm] -> Rewrite [Values]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((FTerm -> Env -> Rewrite Values) -> Env -> FTerm -> Rewrite Values
forall a b c. (a -> b -> c) -> b -> a -> c
flip FTerm -> Env -> Rewrite Values
substitute_signal Env
env) [FTerm]
ts
              FTerm
term    -> (Values -> [Values] -> [Values]
forall a. a -> [a] -> [a]
:[]) (Values -> [Values]) -> Rewrite Values -> Rewrite [Values]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Values
substitute_signal FTerm
term Env
env

        envMaybeLookup :: Env -> MetaVar -> Levelled
        envMaybeLookup :: Env -> MetaVar -> Levelled
envMaybeLookup Env
env MetaVar
k = case MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
k Env
env of
                            Maybe Levelled
Nothing -> Values -> Levelled
ValueTerm Values
forall t. Values t
VAny
                            Just Levelled
lf -> Levelled
lf


substitute :: FTerm ->  Env -> Rewrite Funcons
substitute :: FTerm -> Env -> Rewrite Funcons
substitute (TVar MetaVar
k) Env
env = Env -> MetaVar -> Rewrite Levelled
envLookup Env
env MetaVar
k Rewrite Levelled
-> (Levelled -> Rewrite Funcons) -> Rewrite Funcons
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MetaVar -> Levelled -> Rewrite Funcons
forall p. p -> Levelled -> Rewrite Funcons
fLevel MetaVar
k
substitute (TName Name
nm) Env
env = Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (Funcons -> Rewrite Funcons) -> Funcons -> Rewrite Funcons
forall a b. (a -> b) -> a -> b
$ Name -> Funcons
FName Name
nm
substitute (TApp Name
nm [FTerm]
terms) Env
env = Name -> [Funcons] -> Funcons
FApp Name
nm ([Funcons] -> Funcons) -> Rewrite [Funcons] -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm]
terms Env
env
substitute (TSeq [FTerm]
terms) Env
env = MetaVar -> Rewrite Funcons
forall a. MetaVar -> Rewrite a
internal (MetaVar
"top level sequence during substitution: " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ [FTerm] -> MetaVar
forall a. Show a => a -> MetaVar
show [FTerm]
terms)
-- e.g. print(V+:values+) -- standard-out![V+] -> ()
--substitute (TList terms) env = FList <$> subsFlatten terms env 
substitute (TSet [FTerm]
terms)  Env
env = [Funcons] -> Funcons
FSet ([Funcons] -> Funcons) -> Rewrite [Funcons] -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm]
terms Env
env
substitute (TMap [FTerm]
terms)  Env
env = [Funcons] -> Funcons
FMap ([Funcons] -> Funcons) -> Rewrite [Funcons] -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm]
terms Env
env
substitute (TBinding FTerm
x FTerm
y) Env
env = Funcons -> [Funcons] -> Funcons
FBinding (Funcons -> [Funcons] -> Funcons)
-> Rewrite Funcons -> Rewrite ([Funcons] -> Funcons)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
x Env
env Rewrite ([Funcons] -> Funcons)
-> Rewrite [Funcons] -> Rewrite Funcons
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm
y] Env
env
substitute (TFuncon Funcons
f) Env
env = Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return Funcons
f
substitute (TSortUnion FTerm
t1 FTerm
t2) Env
env = Funcons -> Funcons -> Funcons
FSortUnion (Funcons -> Funcons -> Funcons)
-> Rewrite Funcons -> Rewrite (Funcons -> Funcons)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t1 Env
env Rewrite (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t2 Env
env
substitute (TSortInter FTerm
t1 FTerm
t2) Env
env = Funcons -> Funcons -> Funcons
FSortInter (Funcons -> Funcons -> Funcons)
-> Rewrite Funcons -> Rewrite (Funcons -> Funcons)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t1 Env
env Rewrite (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t2 Env
env
substitute (TSortComplement FTerm
t1) Env
env = Funcons -> Funcons
FSortComplement (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t1 Env
env
substitute (TSortSeq FTerm
t1 SeqSortOp
op) Env
env = (Funcons -> SeqSortOp -> Funcons)
-> SeqSortOp -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> SeqSortOp -> Funcons
FSortSeq SeqSortOp
op (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t1 Env
env
substitute (TSortPower FTerm
t1 FTerm
t2) Env
env = Funcons -> Funcons -> Funcons
FSortPower (Funcons -> Funcons -> Funcons)
-> Rewrite Funcons -> Rewrite (Funcons -> Funcons)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t1 Env
env Rewrite (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t2 Env
env
substitute (TSortComputes FTerm
t1) Env
env = Funcons -> Funcons
FSortComputes (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t1 Env
env
-- special case for thunks/continuations
substitute (TSortComputesFrom (TSeq []) FTerm
t2) Env
env = 
    Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
nulltype_ (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t2 Env
env
substitute (TSortComputesFrom FTerm
t1 FTerm
t2) Env
env = 
    Funcons -> Funcons -> Funcons
FSortComputesFrom (Funcons -> Funcons -> Funcons)
-> Rewrite Funcons -> Rewrite (Funcons -> Funcons)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t1 Env
env Rewrite (Funcons -> Funcons) -> Rewrite Funcons -> Rewrite Funcons
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FTerm -> Env -> Rewrite Funcons
substitute FTerm
t2 Env
env
substitute FTerm
TAny Env
env = MetaVar -> Rewrite Funcons
forall a. MetaVar -> Rewrite a
internal MetaVar
"missing substitution (wildcard)"

-- flatten out sequence-variables
subsFlatten :: [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten :: [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm]
terms Env
env = [[Funcons]] -> [Funcons]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Funcons]] -> [Funcons])
-> Rewrite [[Funcons]] -> Rewrite [Funcons]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([FTerm] -> (FTerm -> Rewrite [Funcons]) -> Rewrite [[Funcons]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FTerm]
terms ((FTerm -> Rewrite [Funcons]) -> Rewrite [[Funcons]])
-> (FTerm -> Rewrite [Funcons]) -> Rewrite [[Funcons]]
forall a b. (a -> b) -> a -> b
$ \case 
                            TVar MetaVar
k  -> Env -> MetaVar -> Rewrite Levelled
envLookup Env
env MetaVar
k Rewrite Levelled
-> (Levelled -> Rewrite [Funcons]) -> Rewrite [Funcons]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Levelled -> Rewrite [Funcons]
fsLevel
                            TSeq [FTerm]
ts -> [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm]
ts Env
env
                            FTerm
term    -> (Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:[]) (Funcons -> [Funcons]) -> Rewrite Funcons -> Rewrite [Funcons]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite Funcons
substitute FTerm
term Env
env)

-- Version of subsAndRewritesToValue that 'caches' computational steps:
-- If after rewriting a computational step is produced the
--  step and associated funcon replace the term in the environment
--  (if the term consists of just a meta-variable)
-- This function immediately returns a computational step when
--  a given term has a cached step
-- If the term is not just a meta-variable, this function behaves normally
subsAndRewritesInEnv :: FTerm -> Env -> Rewrite (Rewritten, Env)
subsAndRewritesInEnv :: FTerm -> Env -> Rewrite (Rewritten, Env)
subsAndRewritesInEnv (TVar MetaVar
x) Env
env 
  | Just (FunconTerm Funcons
f (Just MSOS StepRes
step)) <- MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
x Env
env = 
      (Rewritten, Env) -> Rewrite (Rewritten, Env)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Rewritten, Env) -> Rewrite (Rewritten, Env))
-> (Rewritten, Env) -> Rewrite (Rewritten, Env)
forall a b. (a -> b) -> a -> b
$ (Funcons -> MSOS StepRes -> Rewritten
CompTerm Funcons
f MSOS StepRes
step, Env
env)
subsAndRewritesInEnv FTerm
term Env
env  = do 
  Funcons
f <- FTerm -> Env -> Rewrite Funcons
substitute FTerm
term Env
env
  Rewritten
res <- Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f
  case FTerm
term of 
    TVar MetaVar
x -> case Rewritten
res of 
     ValTerm [Values]
vs       -> (Rewritten, Env) -> Rewrite (Rewritten, Env)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewritten
res, MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
x ([Values] -> Levelled
ValuesTerm [Values]
vs) Env
env)
     CompTerm Funcons
f MSOS StepRes
step  -> (Rewritten, Env) -> Rewrite (Rewritten, Env)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewritten
res, MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
x (Funcons -> Maybe (MSOS StepRes) -> Levelled
FunconTerm Funcons
f (MSOS StepRes -> Maybe (MSOS StepRes)
forall a. a -> Maybe a
Just MSOS StepRes
step)) Env
env)
    FTerm
_      -> (Rewritten, Env) -> Rewrite (Rewritten, Env)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewritten
res, Env
env)

subsAndRewritesToValue :: FTerm -> Env -> Rewrite Values
subsAndRewritesToValue :: FTerm -> Env -> Rewrite Values
subsAndRewritesToValue FTerm
f Env
env = (Values, Env) -> Values
forall a b. (a, b) -> a
fst ((Values, Env) -> Values)
-> Rewrite (Values, Env) -> Rewrite Values
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite (Values, Env)
subsAndRewritesToValueInEnv FTerm
f Env
env

-- Important optimisation:
-- If the given term is a var, 
--    update the env to store the rewritten value.
subsAndRewritesToValueInEnv :: FTerm -> Env -> Rewrite (Values, Env)
subsAndRewritesToValueInEnv :: FTerm -> Env -> Rewrite (Values, Env)
subsAndRewritesToValueInEnv (TVar MetaVar
x) Env
env 
  -- assumed to be already rewritten (because cached step is present)
  | Just (FunconTerm Funcons
f (Just MSOS StepRes
step)) <- MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
x Env
env = Rewrite (Values, Env)
forall a. Rewrite a
rewriteToValErr
subsAndRewritesToValueInEnv FTerm
term Env
env = do
  Funcons
f <- FTerm -> Env -> Rewrite Funcons
substitute FTerm
term Env
env 
  Values
v <- Funcons -> Rewrite Values
rewritesToValue Funcons
f
  case FTerm
term of TVar MetaVar
var  -> (Values, Env) -> Rewrite (Values, Env)
forall (m :: * -> *) a. Monad m => a -> m a
return (Values
v, MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var (Values -> Levelled
ValueTerm Values
v) Env
env)
               FTerm
_         -> (Values, Env) -> Rewrite (Values, Env)
forall (m :: * -> *) a. Monad m => a -> m a
return (Values
v, Env
env)

subsAndRewritesToValues :: FTerm -> Env -> Rewrite [Values]
subsAndRewritesToValues :: FTerm -> Env -> Rewrite [Values]
subsAndRewritesToValues FTerm
f Env
env = ([Values], Env) -> [Values]
forall a b. (a, b) -> a
fst (([Values], Env) -> [Values])
-> Rewrite ([Values], Env) -> Rewrite [Values]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTerm -> Env -> Rewrite ([Values], Env)
subsAndRewritesToValuesInEnv FTerm
f Env
env

subsAndRewritesToValuesInEnv :: FTerm -> Env -> Rewrite ([Values], Env)
subsAndRewritesToValuesInEnv :: FTerm -> Env -> Rewrite ([Values], Env)
subsAndRewritesToValuesInEnv (TVar MetaVar
x) Env
env 
  -- assumed to be already rewritten (because cached step is present)
  | Just (FunconTerm Funcons
f (Just MSOS StepRes
step)) <- MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
x Env
env = Rewrite ([Values], Env)
forall a. Rewrite a
rewriteToValErr
subsAndRewritesToValuesInEnv FTerm
term Env
env = do
  [Funcons]
fs  <- [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm
term] Env
env 
  [Values]
vs  <- [[Values]] -> [Values]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Values]] -> [Values]) -> Rewrite [[Values]] -> Rewrite [Values]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> Rewrite [Values]) -> [Funcons] -> Rewrite [[Values]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Rewrite [Values]
rewritesToValues [Funcons]
fs
  case FTerm
term of TVar MetaVar
var  -> ([Values], Env) -> Rewrite ([Values], Env)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values]
vs, MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var ([Values] -> Levelled
ValuesTerm [Values]
vs) Env
env)
               FTerm
_         -> ([Values], Env) -> Rewrite ([Values], Env)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values]
vs, Env
env)


-- | Variant of 'rewriteTo' that applies substitution.
rewriteTermTo :: FTerm -> Env -> Rewrite Rewritten
rewriteTermTo :: FTerm -> Env -> Rewrite Rewritten
rewriteTermTo FTerm
fterm Env
env = [FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm
fterm] Env
env Rewrite [Funcons]
-> ([Funcons] -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  [Funcons
f] -> Funcons -> Rewrite Rewritten
rewriteTo Funcons
f
  [Funcons]
fs  -> [Funcons] -> Rewrite Rewritten
rewriteSeqTo [Funcons]
fs 

-- | Variant of 'stepTo' that applies substitution.
stepTermTo :: FTerm -> Env -> MSOS StepRes 
stepTermTo :: FTerm -> Env -> MSOS StepRes
stepTermTo FTerm
fterm Env
env = Rewrite [Funcons] -> MSOS [Funcons]
forall a. Rewrite a -> MSOS a
liftRewrite ([FTerm] -> Env -> Rewrite [Funcons]
subsFlatten [FTerm
fterm] Env
env) MSOS [Funcons] -> ([Funcons] -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
  [Funcons
f] -> Funcons -> MSOS StepRes
stepTo Funcons
f
  [Funcons]
fs  -> [Funcons] -> MSOS StepRes
stepSeqTo [Funcons]
fs

lifted_envStore :: MetaVar -> FTerm -> Env -> MSOS Env
lifted_envStore :: MetaVar -> FTerm -> Env -> MSOS Env
lifted_envStore MetaVar
m FTerm
t Env
e = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (MetaVar -> FTerm -> Env -> Rewrite Env
envStore MetaVar
m FTerm
t Env
e)

envStore :: MetaVar -> FTerm -> Env -> Rewrite Env
envStore :: MetaVar -> FTerm -> Env -> Rewrite Env
envStore MetaVar
var FTerm
term Env
env = FTerm -> Env -> Rewrite Funcons
substitute FTerm
term Env
env Rewrite Funcons -> (Funcons -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    (FValue Values
v)    -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Rewrite Env) -> Env -> Rewrite Env
forall a b. (a -> b) -> a -> b
$ MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var (Values -> Levelled
ValueTerm Values
v) Env
env
    Funcons
fct           -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Rewrite Env) -> Env -> Rewrite Env
forall a b. (a -> b) -> a -> b
$ MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var (Funcons -> Maybe (MSOS StepRes) -> Levelled
FunconTerm Funcons
fct Maybe (MSOS StepRes)
forall a. Maybe a
Nothing) Env
env

lifted_envRewrite :: MetaVar -> Env -> MSOS Env
lifted_envRewrite :: MetaVar -> Env -> MSOS Env
lifted_envRewrite MetaVar
m Env
e = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (MetaVar -> Env -> Rewrite Env
envRewrite MetaVar
m Env
e)

-- | Apply as many rewrites as possible to the term bound to the
-- given variable in the meta-environment
envRewrite :: MetaVar -> Env -> Rewrite Env
envRewrite :: MetaVar -> Env -> Rewrite Env
envRewrite MetaVar
var Env
env = do
    Env -> MetaVar -> Rewrite Levelled
envLookup Env
env MetaVar
var Rewrite Levelled -> (Levelled -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      FunconTerm Funcons
fct Maybe (MSOS StepRes)
Nothing -> Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
fct Rewrite Rewritten -> (Rewritten -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        ValTerm [Values]
vs    -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Rewrite Env) -> Env -> Rewrite Env
forall a b. (a -> b) -> a -> b
$ MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var ([Values] -> Levelled
ValuesTerm [Values]
vs) Env
env
        CompTerm Funcons
f MSOS StepRes
fs -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Rewrite Env) -> Env -> Rewrite Env
forall a b. (a -> b) -> a -> b
$ MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var (Funcons -> Maybe (MSOS StepRes) -> Levelled
FunconTerm Funcons
f (MSOS StepRes -> Maybe (MSOS StepRes)
forall a. a -> Maybe a
Just MSOS StepRes
fs)) Env
env
      Levelled
_ -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env