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

module Funcons.Core.Computations.Normal.Storing.Storing where

import Funcons.EDSL

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

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    [(Name
"variables",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"variables" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"variable" [Name -> FTerm
TName Name
"locations",Name -> FTerm
TName Name
"value-types"] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [])]),(Name
"vars",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"vars" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"variable" [Name -> FTerm
TName Name
"locations",Name -> FTerm
TName Name
"value-types"] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [])])]

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"locations",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepLocations),(Name
"locs",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepLocations),(Name
"stores",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepStores),(Name
"store-clear",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepStore_clear),(Name
"initialise-storing",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepInitialise_storing),(Name
"init-storing",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepInitialise_storing),(Name
"variable",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepVariable),(Name
"var",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepVariable),(Name
"allocate-variable",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepAllocate_variable),(Name
"alloc",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepAllocate_variable),(Name
"recycle-variables",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRecycle_variables),(Name
"recycle",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRecycle_variables),(Name
"initialise-variable",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepInitialise_variable),(Name
"init",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepInitialise_variable),(Name
"allocate-initialised-variable",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
NonStrict,Strictness
Strict] Strictness
NonStrict NonStrictFuncon
stepAllocate_initialised_variable),(Name
"alloc-init",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
NonStrict,Strictness
Strict] Strictness
NonStrict NonStrictFuncon
stepAllocate_initialised_variable),(Name
"assign",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepAssign),(Name
"assigned",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepAssigned),(Name
"current-value",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCurrent_value),(Name
"un-assign",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepUn_assign),(Name
"structural-assign",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepStructural_assign),(Name
"structural-assigned",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepStructural_assigned),(Name
"variables",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepVariables),(Name
"vars",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepVariables)]

locations_ :: Funcons
locations_ = Name -> Funcons
FName Name
"locations"
locs_ :: Funcons
locs_ = Name -> Funcons
FName Name
"locations"
stepLocations :: NullaryFuncon
stepLocations = [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
TName Name
"atoms") Env
forall k a. Map k a
env

stores_ :: Funcons
stores_ = Name -> Funcons
FName Name
"stores"
stepStores :: NullaryFuncon
stepStores = [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
"locations",FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]) Env
forall k a. Map k a
env

store_clear_ :: Funcons
store_clear_ = Name -> Funcons
FName Name
"store-clear"
stepStore_clear :: NullaryFuncon
stepStore_clear = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (VPattern
VPWildCard) Env
forall k a. Map k a
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (Name -> [FTerm] -> FTerm
TApp Name
"map" []) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

initialise_storing_ :: [Funcons] -> Funcons
initialise_storing_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"initialise-storing" ([Funcons]
fargs)
init_storing_ :: [Funcons] -> Funcons
init_storing_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"initialise-storing" ([Funcons]
fargs)
stepInitialise_storing :: NonStrictFuncon
stepInitialise_storing [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
"sequential" [Name -> FTerm
TName Name
"store-clear",Name -> [FTerm] -> FTerm
TApp Name
"initialise-giving" [Name -> [FTerm] -> FTerm
TApp Name
"initialise-generating" [MetaVar -> FTerm
TVar MetaVar
"X"]]]) Env
env

variable_ :: [Funcons] -> Funcons
variable_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"variable" ([Funcons]
fargs)
var_ :: [Funcons] -> Funcons
var_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"variable" ([Funcons]
fargs)
stepVariable :: StrictFuncon
stepVariable [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
118)]),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
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
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
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
98)]),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
108)]),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)])])),MetaVar -> FTerm
TVar MetaVar
"_X1",MetaVar -> FTerm
TVar MetaVar
"_X2"]) Env
env

allocate_variable_ :: [Funcons] -> Funcons
allocate_variable_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"allocate-variable" ([Funcons]
fargs)
alloc_ :: [Funcons] -> Funcons
alloc_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"allocate-variable" ([Funcons]
fargs)
stepAllocate_variable :: StrictFuncon
stepAllocate_variable [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    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
"T") (Name -> FTerm
TName Name
"types")] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            Env
env <- FTerm -> [FPattern] -> Env -> MSOS Env
premise (Name -> [FTerm] -> FTerm
TApp Name
"use-atom-not-in" [Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]]) [MetaVar -> FPattern
PMetaVar MetaVar
"L"] Env
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma'") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-override" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"L") ([FTerm] -> FTerm
TSeq [])],MetaVar -> FTerm
TVar MetaVar
"Sigma'"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma''"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma''") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"variable" [MetaVar -> FTerm
TVar MetaVar
"L",MetaVar -> FTerm
TVar MetaVar
"T"]) Env
env

recycle_variables_ :: [Funcons] -> Funcons
recycle_variables_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"recycle-variables" ([Funcons]
fargs)
recycle_ :: [Funcons] -> Funcons
recycle_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"recycle-variables" ([Funcons]
fargs)
stepRecycle_variables :: StrictFuncon
stepRecycle_variables [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] [MSOS StepRes
step1,MSOS StepRes
step2]
    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
"Var") (Name -> FTerm
TName Name
"variables"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"Var+" SeqSortOp
PlusOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"variables") SeqSortOp
PlusOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"recycle-variables" [MetaVar -> FTerm
TVar MetaVar
"Var"],Name -> [FTerm] -> FTerm
TApp Name
"recycle-variables" [MetaVar -> FTerm
TVar MetaVar
"Var+"]]) 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 <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")]] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]]) (Name -> FTerm
TName Name
"true")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"Sigma",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"L"]]) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") 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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")]] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]]) (Name -> FTerm
TName Name
"false")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

initialise_variable_ :: [Funcons] -> Funcons
initialise_variable_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"initialise-variable" ([Funcons]
fargs)
init_ :: [Funcons] -> Funcons
init_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"initialise-variable" ([Funcons]
fargs)
stepInitialise_variable :: StrictFuncon
stepInitialise_variable [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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"Val") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"and" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]],Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"is-value" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"Sigma",MetaVar -> FTerm
TVar MetaVar
"L"]]],Name -> [FTerm] -> FTerm
TApp Name
"is-in-type" [MetaVar -> FTerm
TVar MetaVar
"Val",MetaVar -> FTerm
TVar MetaVar
"T"]]) (Name -> FTerm
TName Name
"true")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (Name -> [FTerm] -> FTerm
TApp Name
"map-override" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"L") (MetaVar -> FTerm
TVar MetaVar
"Val")],MetaVar -> FTerm
TVar MetaVar
"Sigma"]) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") 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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"Val") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"and" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]],Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"is-value" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"Sigma",MetaVar -> FTerm
TVar MetaVar
"L"]]],Name -> [FTerm] -> FTerm
TApp Name
"is-in-type" [MetaVar -> FTerm
TVar MetaVar
"Val",MetaVar -> FTerm
TVar MetaVar
"T"]]) (Name -> FTerm
TName Name
"false")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

allocate_initialised_variable_ :: [Funcons] -> Funcons
allocate_initialised_variable_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"allocate-initialised-variable" ([Funcons]
fargs)
alloc_init_ :: [Funcons] -> Funcons
alloc_init_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"allocate-initialised-variable" ([Funcons]
fargs)
stepAllocate_initialised_variable :: NonStrictFuncon
stepAllocate_initialised_variable [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
"T",FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"Val") (MetaVar -> FTerm
TVar MetaVar
"T")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"give" [Name -> [FTerm] -> FTerm
TApp Name
"allocate-variable" [MetaVar -> FTerm
TVar MetaVar
"T"],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"initialise-variable" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"Val"],Name -> FTerm
TName Name
"given"]]) Env
env

assign_ :: [Funcons] -> Funcons
assign_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"assign" ([Funcons]
fargs)
stepAssign :: StrictFuncon
stepAssign [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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"Val") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"and" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]],Name -> [FTerm] -> FTerm
TApp Name
"is-in-type" [MetaVar -> FTerm
TVar MetaVar
"Val",MetaVar -> FTerm
TVar MetaVar
"T"]]) (Name -> FTerm
TName Name
"true")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (Name -> [FTerm] -> FTerm
TApp Name
"map-override" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"L") (MetaVar -> FTerm
TVar MetaVar
"Val")],MetaVar -> FTerm
TVar MetaVar
"Sigma"]) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") 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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"Val") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"and" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]],Name -> [FTerm] -> FTerm
TApp Name
"is-in-type" [MetaVar -> FTerm
TVar MetaVar
"Val",MetaVar -> FTerm
TVar MetaVar
"T"]]) (Name -> FTerm
TName Name
"false")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

assigned_ :: [Funcons] -> Funcons
assigned_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"assigned" ([Funcons]
fargs)
stepAssigned :: StrictFuncon
stepAssigned [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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")]] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"Sigma",MetaVar -> FTerm
TVar MetaVar
"L"]) [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"Val") (Name -> FTerm
TName Name
"values")]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"Val") 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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")]] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"Sigma",MetaVar -> FTerm
TVar MetaVar
"L"]) ([FTerm] -> FTerm
TSeq [])) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

current_value_ :: [Funcons] -> Funcons
current_value_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"current-value" ([Funcons]
fargs)
stepCurrent_value :: StrictFuncon
stepCurrent_value [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2] []
    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
"Var") (Name -> FTerm
TName Name
"variables")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"assigned" [MetaVar -> FTerm
TVar MetaVar
"Var"]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = 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
"U") (FTerm -> FTerm
TSortComplement (Name -> FTerm
TName Name
"variables"))] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"U") Env
env

un_assign_ :: [Funcons] -> Funcons
un_assign_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"un-assign" ([Funcons]
fargs)
stepUn_assign :: StrictFuncon
stepUn_assign [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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")]] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]]) (Name -> FTerm
TName Name
"true")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (Name -> [FTerm] -> FTerm
TApp Name
"map-override" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"L") ([FTerm] -> FTerm
TSeq [])],MetaVar -> FTerm
TVar MetaVar
"Sigma"]) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") 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 [Name -> [VPattern] -> VPattern
PADT Name
"variable" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"locations"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"T") (Name -> FTerm
TName Name
"types")]] Env
forall k a. Map k a
env
            Env
env <- Name -> VPattern -> Env -> MSOS Env
getMutPatt Name
"store" (MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma") Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"L",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"Sigma"]]) (Name -> FTerm
TName Name
"false")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

structural_assign_ :: [Funcons] -> Funcons
structural_assign_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"structural-assign" ([Funcons]
fargs)
stepStructural_assign :: StrictFuncon
stepStructural_assign [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4,NullaryFuncon
rewrite5] []
    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
"V1") (Name -> FTerm
TName Name
"variables"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V2") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"assign" [MetaVar -> FTerm
TVar MetaVar
"V1",MetaVar -> FTerm
TVar MetaVar
"V2"]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = 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
"V1") (Name -> FTerm
TName Name
"datatype-values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V2") (Name -> FTerm
TName Name
"datatype-values")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"V1") (FTerm -> FTerm
TSortComplement (Name -> FTerm
TName Name
"variables"))) Env
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (MetaVar -> FTerm
TVar MetaVar
"V1") [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I1") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V1*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)]]) Env
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (MetaVar -> FTerm
TVar MetaVar
"V2") [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I2") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V2*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)]]) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"I1",MetaVar -> FTerm
TVar MetaVar
"I2"]],Name -> [FTerm] -> FTerm
TApp Name
"effect" [Name -> [FTerm] -> FTerm
TApp Name
"tuple" [Name -> [FTerm] -> FTerm
TApp Name
"interleave-map" [Name -> [FTerm] -> FTerm
TApp Name
"structural-assign" [Name -> [FTerm] -> FTerm
TApp Name
"tuple-elements" [Name -> FTerm
TName Name
"given"]],Name -> [FTerm] -> FTerm
TApp Name
"tuple-zip" [Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V1*"],Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V2*"]]]]],Name -> FTerm
TName Name
"null-value"]) Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = 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
"M1") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M2") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M1"]) ([FTerm] -> FTerm
TSet [])) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"],[FTerm] -> FTerm
TSet []]]) Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = 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
"M1") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M2") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"some-element" [Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M1"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"K"]) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"K",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"]]],Name -> [FTerm] -> FTerm
TApp Name
"structural-assign" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"M1",MetaVar -> FTerm
TVar MetaVar
"K"],Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"M2",MetaVar -> FTerm
TVar MetaVar
"K"]],Name -> [FTerm] -> FTerm
TApp Name
"structural-assign" [Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"M1",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"K"]],Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"M2",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"K"]]]]) Env
env
          rewrite5 :: NullaryFuncon
rewrite5 = 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
"V1") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V2") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"V1") (FTerm -> FTerm
TSortComplement (FTerm -> FTerm -> FTerm
TSortUnion (Name -> FTerm
TName Name
"datatype-values") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])))) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"V1",MetaVar -> FTerm
TVar MetaVar
"V2"]]) Env
env

structural_assigned_ :: [Funcons] -> Funcons
structural_assigned_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"structural-assigned" ([Funcons]
fargs)
stepStructural_assigned :: StrictFuncon
stepStructural_assigned [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4] []
    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
"Var") (Name -> FTerm
TName Name
"variables")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"assigned" [MetaVar -> FTerm
TVar MetaVar
"Var"]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = 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
"V") (Name -> FTerm
TName Name
"datatype-values")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"V") (FTerm -> FTerm
TSortComplement (Name -> FTerm
TName Name
"variables"))) Env
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (MetaVar -> FTerm
TVar MetaVar
"V") [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)]]) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"datatype-value" [MetaVar -> FTerm
TVar MetaVar
"I",Name -> [FTerm] -> FTerm
TApp Name
"interleave-map" [Name -> [FTerm] -> FTerm
TApp Name
"structural-assigned" [Name -> FTerm
TName Name
"given"],MetaVar -> FTerm
TVar MetaVar
"V*"]]) Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = 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" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"map" [Name -> [FTerm] -> FTerm
TApp Name
"interleave-map" [Name -> [FTerm] -> FTerm
TApp Name
"structural-assigned" [Name -> FTerm
TName Name
"given"],Name -> [FTerm] -> FTerm
TApp Name
"map-elements" [MetaVar -> FTerm
TVar MetaVar
"M"]]]) Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = 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
"U") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"U") (FTerm -> FTerm
TSortComplement (FTerm -> FTerm -> FTerm
TSortUnion (Name -> FTerm
TName Name
"datatype-values") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])))) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"U") Env
env

variables_ :: Funcons
variables_ = Name -> Funcons
FName Name
"variables"
stepVariables :: NullaryFuncon
stepVariables = Name -> StrictFuncon
rewriteType Name
"variables" []