-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Normal/Binding/Binding.cbs
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Computations.Normal.Binding.Binding where

import Funcons.EDSL

import Funcons.Operations hiding (Values,libFromList)
entities :: [a]
entities = []

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    [(Name
"identifiers",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"identifiers" [] [FTerm -> DataTypeAltt
DataTypeInclusionn (Name -> FTerm
TName Name
"strings"),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"identifier-tagged" [Name -> FTerm
TName Name
"identifiers",Name -> FTerm
TName Name
"values"] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [])]),(Name
"ids",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"ids" [] [FTerm -> DataTypeAltt
DataTypeInclusionn (Name -> FTerm
TName Name
"strings"),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"identifier-tagged" [Name -> FTerm
TName Name
"identifiers",Name -> FTerm
TName Name
"values"] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [])])]

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"environments",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepEnvironments),(Name
"envs",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepEnvironments),(Name
"identifier-tagged",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIdentifier_tagged),(Name
"id-tagged",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIdentifier_tagged),(Name
"fresh-identifier",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepFresh_identifier),(Name
"initialise-binding",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepInitialise_binding),(Name
"bind-value",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBind_value),(Name
"bind",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBind_value),(Name
"unbind",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepUnbind),(Name
"bound-directly",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBound_directly),(Name
"bound-value",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBound_value),(Name
"bound",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBound_value),(Name
"closed",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepClosed),(Name
"scope",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
Strict,Strictness
NonStrict] Strictness
NonStrict NonStrictFuncon
stepScope),(Name
"accumulate",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepAccumulate),(Name
"collateral",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCollateral),(Name
"bind-recursively",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
Strict,Strictness
NonStrict] Strictness
NonStrict NonStrictFuncon
stepBind_recursively),(Name
"recursive",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
Strict,Strictness
NonStrict] Strictness
NonStrict NonStrictFuncon
stepRecursive),(Name
"re-close",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
Strict,Strictness
NonStrict] Strictness
NonStrict NonStrictFuncon
stepRe_close),(Name
"bind-to-forward-links",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBind_to_forward_links),(Name
"set-forward-links",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSet_forward_links),(Name
"identifiers",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepIdentifiers),(Name
"ids",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepIdentifiers)]

environments_ :: Funcons
environments_ = Name -> Funcons
FName Name
"environments"
envs_ :: Funcons
envs_ = Name -> Funcons
FName Name
"environments"
stepEnvironments :: NullaryFuncon
stepEnvironments = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"maps" [Name -> FTerm
TName Name
"identifiers",FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]) Env
forall k a. Map k a
env

identifier_tagged_ :: [Funcons] -> Funcons
identifier_tagged_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"identifier-tagged" ([Funcons]
fargs)
id_tagged_ :: [Funcons] -> Funcons
id_tagged_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"identifier-tagged" ([Funcons]
fargs)
stepIdentifier_tagged :: StrictFuncon
stepIdentifier_tagged [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [MetaVar -> VPattern
VPMetaVar MetaVar
"_X1",MetaVar -> VPattern
VPMetaVar MetaVar
"_X2"] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"_X1") (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp)) Env
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"_X2") (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp)) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
100)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
102)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
114)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
45)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
97)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
103)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
103)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
100)])])),MetaVar -> FTerm
TVar MetaVar
"_X1",MetaVar -> FTerm
TVar MetaVar
"_X2"]) Env
env

fresh_identifier_ :: Funcons
fresh_identifier_ = Name -> Funcons
FName Name
"fresh-identifier"
stepFresh_identifier :: NullaryFuncon
stepFresh_identifier = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"identifier-tagged" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
103)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
114)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
97)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
100)])])),Name -> FTerm
TName Name
"fresh-atom"]) Env
forall k a. Map k a
env

initialise_binding_ :: [Funcons] -> Funcons
initialise_binding_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"initialise-binding" ([Funcons]
fargs)
stepInitialise_binding :: NonStrictFuncon
stepInitialise_binding [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"initialise-linking" [Name -> [FTerm] -> FTerm
TApp Name
"initialise-generating" [Name -> [FTerm] -> FTerm
TApp Name
"closed" [MetaVar -> FTerm
TVar MetaVar
"X"]]]) Env
env

bind_value_ :: [Funcons] -> Funcons
bind_value_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bind-value" ([Funcons]
fargs)
bind_ :: [Funcons] -> Funcons
bind_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bind-value" ([Funcons]
fargs)
stepBind_value :: StrictFuncon
stepBind_value [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"I") (MetaVar -> FTerm
TVar MetaVar
"V")]) Env
env

unbind_ :: [Funcons] -> Funcons
unbind_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"unbind" ([Funcons]
fargs)
stepUnbind :: StrictFuncon
stepUnbind [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"I") ([FTerm] -> FTerm
TSeq [])]) Env
env

bound_directly_ :: [Funcons] -> Funcons
bound_directly_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bound-directly" ([Funcons]
fargs)
stepBound_directly :: StrictFuncon
stepBound_directly [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers")] Env
forall k a. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getInhPatt Name
"environment" [MetaVar -> VPattern
VPMetaVar MetaVar
"Rho"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"Rho",MetaVar -> FTerm
TVar MetaVar
"I"]) [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")]) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers")] Env
forall k a. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getInhPatt Name
"environment" [MetaVar -> VPattern
VPMetaVar MetaVar
"Rho"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"Rho",MetaVar -> FTerm
TVar MetaVar
"I"]) []) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

bound_value_ :: [Funcons] -> Funcons
bound_value_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bound-value" ([Funcons]
fargs)
bound_ :: [Funcons] -> Funcons
bound_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bound-value" ([Funcons]
fargs)
stepBound_value :: StrictFuncon
stepBound_value [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"follow-if-link" [Name -> [FTerm] -> FTerm
TApp Name
"bound-directly" [MetaVar -> FTerm
TVar MetaVar
"I"]]) Env
env

closed_ :: [Funcons] -> Funcons
closed_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"closed" ([Funcons]
fargs)
stepClosed :: NonStrictFuncon
stepClosed [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] [MSOS StepRes
step1]
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] Env
forall k a. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getInhPatt Name
"environment" [VPattern
VPWildCard] Env
env
            Env
env <- Name -> FTerm -> Env -> MSOS Env -> MSOS Env
forall a. Name -> FTerm -> Env -> MSOS a -> MSOS a
withInhTerm Name
"environment" (Name -> [FTerm] -> FTerm
TApp Name
"map" []) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [MetaVar -> FPattern
PMetaVar MetaVar
"X'"] Env
env)
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"closed" [MetaVar -> FTerm
TVar MetaVar
"X'"]) Env
env

scope_ :: [Funcons] -> Funcons
scope_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"scope" ([Funcons]
fargs)
stepScope :: NonStrictFuncon
stepScope [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] [MSOS StepRes
step1]
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated FPattern
PWildCard (Name -> FTerm
TName Name
"environments"),FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"Rho1") (Name -> FTerm
TName Name
"environments"),MetaVar -> FPattern
PMetaVar MetaVar
"X"] Env
forall k a. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getInhPatt Name
"environment" [MetaVar -> VPattern
VPMetaVar MetaVar
"Rho0"] Env
env
            Env
env <- Name -> FTerm -> Env -> MSOS Env -> MSOS Env
forall a. Name -> FTerm -> Env -> MSOS a -> MSOS a
withInhTerm Name
"environment" (Name -> [FTerm] -> FTerm
TApp Name
"map-override" [MetaVar -> FTerm
TVar MetaVar
"Rho1",MetaVar -> FTerm
TVar MetaVar
"Rho0"]) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [MetaVar -> FPattern
PMetaVar MetaVar
"X'"] Env
env)
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"scope" [MetaVar -> FTerm
TVar MetaVar
"Rho1",MetaVar -> FTerm
TVar MetaVar
"X'"]) Env
env

accumulate_ :: [Funcons] -> Funcons
accumulate_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"accumulate" ([Funcons]
fargs)
stepAccumulate :: NonStrictFuncon
stepAccumulate [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4] [MSOS StepRes
step1]
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"Rho1") (Name -> FTerm
TName Name
"environments"),MetaVar -> FPattern
PMetaVar MetaVar
"D2"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"scope" [MetaVar -> FTerm
TVar MetaVar
"Rho1",Name -> [FTerm] -> FTerm
TApp Name
"map-override" [MetaVar -> FTerm
TVar MetaVar
"D2",MetaVar -> FTerm
TVar MetaVar
"Rho1"]]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"map" []) Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"D1"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"D1") Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"D1",MetaVar -> FPattern
PMetaVar MetaVar
"D2",MetaVar -> SeqSortOp -> FPattern
PSeqVar MetaVar
"D+" SeqSortOp
PlusOp] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"accumulate" [MetaVar -> FTerm
TVar MetaVar
"D1",Name -> [FTerm] -> FTerm
TApp Name
"accumulate" [MetaVar -> FTerm
TVar MetaVar
"D2",MetaVar -> FTerm
TVar MetaVar
"D+"]]) Env
env
          step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"D1",MetaVar -> FPattern
PMetaVar MetaVar
"D2"] Env
forall k a. Map k a
env
            Env
env <- FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"D1") [MetaVar -> FPattern
PMetaVar MetaVar
"D1'"] Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"accumulate" [MetaVar -> FTerm
TVar MetaVar
"D1'",MetaVar -> FTerm
TVar MetaVar
"D2"]) Env
env

collateral_ :: [Funcons] -> Funcons
collateral_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"collateral" ([Funcons]
fargs)
stepCollateral :: StrictFuncon
stepCollateral [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"Rho*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"environments") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"map-unite" [MetaVar -> FTerm
TVar MetaVar
"Rho*"]]) Env
env

bind_recursively_ :: [Funcons] -> Funcons
bind_recursively_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bind-recursively" ([Funcons]
fargs)
stepBind_recursively :: NonStrictFuncon
stepBind_recursively [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers"),MetaVar -> FPattern
PMetaVar MetaVar
"E"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"recursive" [[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"I"],Name -> [FTerm] -> FTerm
TApp Name
"bind-value" [MetaVar -> FTerm
TVar MetaVar
"I",MetaVar -> FTerm
TVar MetaVar
"E"]]) Env
env

recursive_ :: [Funcons] -> Funcons
recursive_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"recursive" ([Funcons]
fargs)
stepRecursive :: NonStrictFuncon
stepRecursive [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"SI") (Name -> [FTerm] -> FTerm
TApp Name
"sets" [Name -> FTerm
TName Name
"identifiers"]),MetaVar -> FPattern
PMetaVar MetaVar
"D"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"re-close" [Name -> [FTerm] -> FTerm
TApp Name
"bind-to-forward-links" [MetaVar -> FTerm
TVar MetaVar
"SI"],MetaVar -> FTerm
TVar MetaVar
"D"]) Env
env

re_close_ :: [Funcons] -> Funcons
re_close_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"re-close" ([Funcons]
fargs)
stepRe_close :: NonStrictFuncon
stepRe_close [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"M") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [Name -> FTerm
TName Name
"identifiers",Name -> FTerm
TName Name
"links"]),MetaVar -> FPattern
PMetaVar MetaVar
"D"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"accumulate" [Name -> [FTerm] -> FTerm
TApp Name
"scope" [MetaVar -> FTerm
TVar MetaVar
"M",MetaVar -> FTerm
TVar MetaVar
"D"],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"set-forward-links" [MetaVar -> FTerm
TVar MetaVar
"M"],Name -> [FTerm] -> FTerm
TApp Name
"map" []]]) Env
env

bind_to_forward_links_ :: [Funcons] -> Funcons
bind_to_forward_links_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bind-to-forward-links" ([Funcons]
fargs)
stepBind_to_forward_links :: StrictFuncon
stepBind_to_forward_links [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SI") (Name -> [FTerm] -> FTerm
TApp Name
"sets" [Name -> FTerm
TName Name
"identifiers"])] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"map-unite" [Name -> [FTerm] -> FTerm
TApp Name
"interleave-map" [Name -> [FTerm] -> FTerm
TApp Name
"bind-value" [Name -> FTerm
TName Name
"given",Name -> [FTerm] -> FTerm
TApp Name
"fresh-link" [Name -> FTerm
TName Name
"values"]],Name -> [FTerm] -> FTerm
TApp Name
"set-elements" [MetaVar -> FTerm
TVar MetaVar
"SI"]]]) Env
env

set_forward_links_ :: [Funcons] -> Funcons
set_forward_links_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"set-forward-links" ([Funcons]
fargs)
stepSet_forward_links :: StrictFuncon
stepSet_forward_links [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [Name -> FTerm
TName Name
"identifiers",Name -> FTerm
TName Name
"links"])] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"effect" [Name -> [FTerm] -> FTerm
TApp Name
"interleave-map" [Name -> [FTerm] -> FTerm
TApp Name
"set-link" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"M",Name -> FTerm
TName Name
"given"],Name -> [FTerm] -> FTerm
TApp Name
"bound-value" [Name -> FTerm
TName Name
"given"]],Name -> [FTerm] -> FTerm
TApp Name
"set-elements" [Name -> [FTerm] -> FTerm
TApp Name
"map-domain" [MetaVar -> FTerm
TVar MetaVar
"M"]]]]) Env
env

identifiers_ :: Funcons
identifiers_ = Name -> Funcons
FName Name
"identifiers"
stepIdentifiers :: NullaryFuncon
stepIdentifiers = Name -> StrictFuncon
rewriteType Name
"identifiers" []