{-# LANGUAGE OverloadedStrings #-}
module Funcons.Core.Computations.Normal.Storing.Storing where
import Funcons.EDSL
import Funcons.Operations hiding (Values)
entities = []
types = typeEnvFromList
[("variables",DataTypeMemberss "variables" [] [DataTypeMemberConstructor "variable" [TName "locations",TName "value-types"] (Just [])]),("vars",DataTypeMemberss "vars" [] [DataTypeMemberConstructor "variable" [TName "locations",TName "value-types"] (Just [])])]
funcons = libFromList
[("locations",NullaryFuncon stepLocations),("locs",NullaryFuncon stepLocations),("stores",NullaryFuncon stepStores),("store-clear",NullaryFuncon stepStore_clear),("initialise-storing",NonStrictFuncon stepInitialise_storing),("init-storing",NonStrictFuncon stepInitialise_storing),("variable",StrictFuncon stepVariable),("var",StrictFuncon stepVariable),("allocate-variable",NonStrictFuncon stepAllocate_variable),("alloc",NonStrictFuncon stepAllocate_variable),("recycle-variables",StrictFuncon stepRecycle_variables),("recycle",StrictFuncon stepRecycle_variables),("initialise-variable",StrictFuncon stepInitialise_variable),("init",StrictFuncon stepInitialise_variable),("allocate-initialised-variable",PartiallyStrictFuncon [NonStrict,Strict] NonStrict stepAllocate_initialised_variable),("alloc-init",PartiallyStrictFuncon [NonStrict,Strict] NonStrict stepAllocate_initialised_variable),("assign",StrictFuncon stepAssign),("assigned",StrictFuncon stepAssigned),("un-assign",StrictFuncon stepUn_assign),("structural-assign",StrictFuncon stepStructural_assign),("structural-assigned",StrictFuncon stepStructural_assigned),("current-value",StrictFuncon stepCurrent_value),("variables",NullaryFuncon stepVariables),("vars",NullaryFuncon stepVariables)]
locations_ = FName "locations"
locs_ = FName "locations"
stepLocations = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TName "atoms") env
stores_ = FName "stores"
stepStores = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "maps" [TName "locations",TName "values"]) env
store_clear_ = FName "store-clear"
stepStore_clear = evalRules [] [step1]
where step1 = do
let env = emptyEnv
env <- getMutPatt "store" (VPWildCard) env
putMutTerm "store" (TApp "map" []) env
stepTermTo (TName "none") env
initialise_storing_ fargs = FApp "initialise-storing" (fargs)
init_storing_ fargs = FApp "initialise-storing" (fargs)
stepInitialise_storing fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- fsMatch fargs [PMetaVar "X"] env
rewriteTermTo (TApp "sequential" [TName "store-clear",TApp "initialise-giving" [TApp "initialise-generating" [TVar "X"]]]) env
variable_ fargs = FApp "variable" (fargs)
var_ fargs = FApp "variable" (fargs)
stepVariable fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env
env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) env
env <- sideCondition (SCIsInSort (TVar "_X2") (TName "values")) env
rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'i'),FValue (Ascii 'a'),FValue (Ascii 'b'),FValue (Ascii 'l'),FValue (Ascii 'e')])),TVar "_X1",TVar "_X2"]) env
allocate_variable_ fargs = FApp "allocate-variable" (fargs)
alloc_ fargs = FApp "allocate-variable" (fargs)
stepAllocate_variable fargs =
evalRules [] [step1]
where step1 = do
let env = emptyEnv
env <- lifted_fsMatch fargs [PAnnotated (PMetaVar "VT") (TName "types")] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
putMutTerm "store" (TVar "Sigma") env
env <- premise (TApp "use-atom-not-in" [TApp "dom" [TVar "Sigma"]]) (PMetaVar "L") env
env <- getMutPatt "store" (VPMetaVar "Sigma'") env
env <- lifted_sideCondition (SCPatternMatch (TApp "map-override" [TMap [TVar "L",TName "none"],TVar "Sigma'"]) (VPMetaVar "Sigma''")) env
putMutTerm "store" (TVar "Sigma''") env
stepTermTo (TApp "variable" [TVar "L",TVar "VT"]) env
recycle_variables_ fargs = FApp "recycle-variables" (fargs)
recycle_ fargs = FApp "recycle-variables" (fargs)
stepRecycle_variables fargs =
evalRules [rewrite1] [step1,step2]
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "Var") (TName "variables"),VPAnnotated (VPSeqVar "Var+" PlusOp) (TSortSeq (TName "variables") PlusOp)] env
rewriteTermTo (TApp "sequential" [TApp "recycle-variables" [TVar "Var"],TApp "recycle-variables" [TVar "Var+"]]) env
step1 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "true")) env
putMutTerm "store" (TApp "map-delete" [TVar "Sigma",TSet [TVar "L"]]) env
stepTermTo (TName "none") env
step2 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "false")) env
putMutTerm "store" (TVar "Sigma") env
stepTermTo (TName "fail") env
initialise_variable_ fargs = FApp "initialise-variable" (fargs)
init_ fargs = FApp "initialise-variable" (fargs)
stepInitialise_variable fargs =
evalRules [] [step1,step2]
where step1 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-defined" [TApp "lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "true")) env
putMutTerm "store" (TApp "map-override" [TMap [TVar "L",TVar "Val"],TVar "Sigma"]) env
stepTermTo (TName "none") env
step2 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-defined" [TApp "lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "false")) env
putMutTerm "store" (TVar "Sigma") env
stepTermTo (TName "fail") env
allocate_initialised_variable_ fargs = FApp "allocate-initialised-variable" (fargs)
alloc_init_ fargs = FApp "allocate-initialised-variable" (fargs)
stepAllocate_initialised_variable fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- fsMatch fargs [PMetaVar "VT",PAnnotated (PMetaVar "Val") (TVar "VT")] env
rewriteTermTo (TApp "give" [TApp "allocate-variable" [TVar "VT"],TApp "sequential" [TApp "initialise-variable" [TName "given",TVar "Val"],TName "given"]]) env
assign_ fargs = FApp "assign" (fargs)
stepAssign fargs =
evalRules [] [step1,step2]
where step1 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "true")) env
putMutTerm "store" (TApp "map-override" [TMap [TVar "L",TVar "Val"],TVar "Sigma"]) env
stepTermTo (TName "none") env
step2 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "false")) env
putMutTerm "store" (TVar "Sigma") env
stepTermTo (TName "fail") env
assigned_ fargs = FApp "assigned" (fargs)
stepAssigned fargs =
evalRules [] [step1,step2]
where step1 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "Sigma",TVar "L"]) (VPAnnotated (VPMetaVar "Val") (TName "defined-values"))) env
putMutTerm "store" (TVar "Sigma") env
stepTermTo (TVar "Val") env
step2 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "lookup" [TVar "Sigma",TVar "L"]) (TName "none")) env
putMutTerm "store" (TVar "Sigma") env
stepTermTo (TName "fail") env
un_assign_ fargs = FApp "un-assign" (fargs)
stepUn_assign fargs =
evalRules [] [step1,step2]
where step1 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "true")) env
putMutTerm "store" (TApp "map-override" [TMap [TVar "L",TName "none"],TVar "Sigma"]) env
stepTermTo (TName "none") env
step2 = do
let env = emptyEnv
env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env
env <- getMutPatt "store" (VPMetaVar "Sigma") env
env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "false")) env
putMutTerm "store" (TVar "Sigma") env
stepTermTo (TName "fail") env
structural_assign_ fargs = FApp "structural-assign" (fargs)
stepStructural_assign fargs =
evalRules [rewrite1,rewrite2,rewrite3,rewrite4,rewrite5] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "variables"),VPAnnotated (VPMetaVar "V2") (TName "defined-values")] env
rewriteTermTo (TApp "assign" [TVar "V1",TVar "V2"]) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I1") (TName "ids"),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "defined-values") StarOp)],PADT "datatype-value" [VPAnnotated (VPMetaVar "I2") (TName "ids"),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "defined-values") StarOp)]] env
env <- sideCondition (SCInequality (TVar "I1") (TFuncon (FValue (ADTVal "list" [FValue (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'i'),FValue (Ascii 'a'),FValue (Ascii 'b'),FValue (Ascii 'l'),FValue (Ascii 'e')])))) env
rewriteTermTo (TApp "sequential" [TApp "check-true" [TApp "is-equal" [TVar "I1",TVar "I2"]],TApp "effect" [TApp "tuple" [TApp "interleave-map" [TApp "structural-assign" [TApp "tuple-elements" [TName "given"]],TApp "tuple-zip" [TApp "tuple" [TVar "V1*"],TApp "tuple" [TVar "V2*"]]]]],TName "none"]) env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env
env <- sideCondition (SCEquality (TApp "dom" [TVar "M1"]) (TSet [])) env
rewriteTermTo (TApp "check-true" [TApp "is-equal" [TApp "dom" [TVar "M2"],TSet []]]) env
rewrite4 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env
env <- sideCondition (SCPatternMatch (TApp "some-element" [TApp "dom" [TVar "M1"]]) (VPMetaVar "K")) env
rewriteTermTo (TApp "sequential" [TApp "check-true" [TApp "is-in-set" [TVar "K",TApp "dom" [TVar "M2"]]],TApp "structural-assign" [TApp "lookup" [TVar "M1",TVar "K"],TApp "lookup" [TVar "M2",TVar "K"]],TApp "structural-assign" [TApp "map-delete" [TVar "M1",TSet [TVar "K"]],TApp "map-delete" [TVar "M2",TSet [TVar "K"]]]]) env
rewrite5 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "defined-values"),VPAnnotated (VPMetaVar "V2") (TName "defined-values")] env
env <- sideCondition (SCIsInSort (TVar "V1") (TSortComplement (TSortUnion (TName "variables") (TApp "maps" [TName "values",TName "values"])))) env
rewriteTermTo (TApp "check-true" [TApp "is-equal" [TVar "V1",TVar "V2"]]) env
structural_assigned_ fargs = FApp "structural-assigned" (fargs)
stepStructural_assigned fargs =
evalRules [rewrite1,rewrite2,rewrite3,rewrite4] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "Var") (TName "variables")] env
rewriteTermTo (TApp "assigned" [TVar "Var"]) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I") (TName "ids"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "defined-values") StarOp)]] env
env <- sideCondition (SCInequality (TVar "I") (TFuncon (FValue (ADTVal "list" [FValue (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'i'),FValue (Ascii 'a'),FValue (Ascii 'b'),FValue (Ascii 'l'),FValue (Ascii 'e')])))) env
rewriteTermTo (TApp "datatype-value" [TVar "I",TApp "interleave-map" [TApp "structural-assigned" [TName "given"],TVar "V*"]]) env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TApp "maps" [TName "values",TName "values"])] env
rewriteTermTo (TApp "map" [TApp "interleave-map" [TApp "structural-assigned" [TName "given"],TApp "map-elements" [TVar "M"]]]) env
rewrite4 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "U") (TName "values")] env
env <- sideCondition (SCIsInSort (TVar "U") (TSortComplement (TSortUnion (TName "variables") (TApp "maps" [TName "values",TName "values"])))) env
rewriteTermTo (TVar "U") env
current_value_ fargs = FApp "current-value" (fargs)
stepCurrent_value fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values")] env
rewriteTermTo (TApp "def" [TApp "structural-assigned" [TVar "V"]]) env
variables_ = FName "variables"
stepVariables = rewriteType "variables" []