Library zoo_mcas.mcas_2__code
Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.program_logic.identifier.
Require Import zoo_std.list.
Require Import zoo.options.
Notation "'mcas_2٠casn'" := (
in_type "zoo_mcas.mcas_2.state" 0
)(in custom zoo_field
).
Notation "'mcas_2٠before'" := (
in_type "zoo_mcas.mcas_2.state" 1
)(in custom zoo_field
).
Notation "'mcas_2٠after'" := (
in_type "zoo_mcas.mcas_2.state" 2
)(in custom zoo_field
).
Notation "'mcas_2٠loc'" := (
in_type "zoo_mcas.mcas_2.cas" 0
)(in custom zoo_proj
).
Notation "'mcas_2٠state'" := (
in_type "zoo_mcas.mcas_2.cas" 1
)(in custom zoo_proj
).
Notation "'mcas_2٠status'" := (
in_type "zoo_mcas.mcas_2.casn" 0
)(in custom zoo_field
).
Notation "'mcas_2٠proph'" := (
in_type "zoo_mcas.mcas_2.casn" 1
)(in custom zoo_field
).
Notation "'mcas_2٠Undetermined'" := (
in_type "zoo_mcas.mcas_2.status" 0
)(in custom zoo_tag
).
Notation "'mcas_2٠Before'" := (
in_type "zoo_mcas.mcas_2.status" 1
)(in custom zoo_tag
).
Notation "'mcas_2٠After'" := (
in_type "zoo_mcas.mcas_2.status" 2
)(in custom zoo_tag
).
Notation "'mcas_2٠cmps'" := (
in_type "zoo_mcas.mcas_2.status.Undetermined" 0
)(in custom zoo_proj
).
Notation "'mcas_2٠cass'" := (
in_type "zoo_mcas.mcas_2.status.Undetermined" 1
)(in custom zoo_proj
).
Definition mcas_2٠clear : val :=
𝗳𝘂𝗻 "cass" "is_after" →
𝗶𝗳 "is_after" 𝘁𝗵𝗲𝗻 (
list٠iter
(𝗳𝘂𝗻 "cas" →
"cas".<mcas_2٠state> <-{mcas_2٠before}
"cas".<mcas_2٠state>.{mcas_2٠after})
"cass"
) 𝗲𝗹𝘀𝗲 (
list٠iter
(𝗳𝘂𝗻 "cas" →
"cas".<mcas_2٠state> <-{mcas_2٠after}
"cas".<mcas_2٠state>.{mcas_2٠before})
"cass"
).
Definition mcas_2٠status_to_bool : val :=
𝗳𝘂𝗻 "status" →
"status" == §mcas_2٠After.
Definition mcas_2٠finish : val :=
𝗳𝘂𝗻 "gid" "casn" "status" →
𝗺𝗮𝘁𝗰𝗵 "casn".{mcas_2٠status} 𝘄𝗶𝘁𝗵
| mcas_2٠Before →
false
| mcas_2٠After →
true
| mcas_2٠Undetermined "cmps" "cass" 𝗮𝘀 "old_status" →
𝗹𝗲𝘁 "status" =
𝗶𝗳 "status" == §mcas_2٠Before 𝘁𝗵𝗲𝗻 (
§mcas_2٠Before
) 𝗲𝗹𝘀𝗲 𝗶𝗳
list٠∀
(𝗳𝘂𝗻 "cmp" →
!"cmp".<mcas_2٠loc> == "cmp".<mcas_2٠state>)
"cmps"
𝘁𝗵𝗲𝗻 (
§mcas_2٠After
) 𝗲𝗹𝘀𝗲 (
§mcas_2٠Before
)
𝗶𝗻
𝗹𝗲𝘁 "is_after" = mcas_2٠status_to_bool "status" 𝗶𝗻
𝗶𝗳
𝗿𝗲𝘀𝗼𝗹𝘃𝗲
(𝗰𝗮𝘀 "casn".[mcas_2٠status] "old_status" "status")
"casn".{mcas_2٠proph}
("gid", "is_after")
𝘁𝗵𝗲𝗻 (
mcas_2٠clear "cass" "is_after"
) 𝗲𝗹𝘀𝗲 (
()
) ⍮
mcas_2٠status_to_bool "casn".{mcas_2٠status}
𝗲𝗻𝗱.
#[local] Definition __zoo_recs_0 :=
( 𝗿𝗲𝗰𝘀 "determine_as" "casn" "cass" →
𝗹𝗲𝘁 "gid" = 𝗶𝗱 𝗶𝗻
𝗺𝗮𝘁𝗰𝗵 "cass" 𝘄𝗶𝘁𝗵
| [] →
mcas_2٠finish "gid" "casn" §mcas_2٠After
| "cas" :: "continue" 𝗮𝘀 "retry" →
𝗹𝗲𝘁 "loc", "state" = "cas" 𝗶𝗻
𝗹𝗲𝘁 "proph" = 𝗽𝗿𝗼𝗽𝗵 𝗶𝗻
𝗹𝗲𝘁 "old_state" = !"loc" 𝗶𝗻
𝗶𝗳 "state" == "old_state" 𝘁𝗵𝗲𝗻 (
"determine_as" "casn" "continue"
) 𝗲𝗹𝘀𝗲 𝗶𝗳
𝗹𝗲𝘁 "@tmp" =
"state".{mcas_2٠before} == "eval" "old_state"
𝗶𝗻
𝗿𝗲𝘀𝗼𝗹𝘃𝗲 𝘀𝗸𝗶𝗽 "proph" "@tmp" ⍮
"@tmp"
𝘁𝗵𝗲𝗻 (
"lock" "casn" "loc" "old_state" "state" "retry" "continue"
) 𝗲𝗹𝘀𝗲 (
mcas_2٠finish "gid" "casn" §mcas_2٠Before
)
𝗲𝗻𝗱
𝘄𝗶𝘁𝗵 "lock" "casn" "loc" "old_state" "state" "retry" "continue" →
𝗺𝗮𝘁𝗰𝗵 "casn".{mcas_2٠status} 𝘄𝗶𝘁𝗵
| mcas_2٠Before →
false
| mcas_2٠After →
true
| mcas_2٠Undetermined ⎽ ⎽ →
𝗶𝗳
𝗰𝗮𝘀 "loc".[contents] "old_state" "state"
𝘁𝗵𝗲𝗻 (
"determine_as" "casn" "continue"
) 𝗲𝗹𝘀𝗲 (
"determine_as" "casn" "retry"
)
𝗲𝗻𝗱
𝘄𝗶𝘁𝗵 "eval" "state" →
𝗶𝗳 "determine" "state".{mcas_2٠casn} 𝘁𝗵𝗲𝗻 (
"state".{mcas_2٠after}
) 𝗲𝗹𝘀𝗲 (
"state".{mcas_2٠before}
)
𝘄𝗶𝘁𝗵 "determine" "casn" →
𝗺𝗮𝘁𝗰𝗵 "casn".{mcas_2٠status} 𝘄𝗶𝘁𝗵
| mcas_2٠Before →
false
| mcas_2٠After →
true
| mcas_2٠Undetermined ⎽ "cass" →
"determine_as" "casn" "cass"
𝗲𝗻𝗱
)%zoo_recs.
Definition mcas_2٠determine_as :=
ValRecs 0 __zoo_recs_0.
Definition mcas_2٠lock :=
ValRecs 1 __zoo_recs_0.
Definition mcas_2٠eval :=
ValRecs 2 __zoo_recs_0.
Definition mcas_2٠determine :=
ValRecs 3 __zoo_recs_0.
#[global] Instance :
AsValRecs' mcas_2٠determine_as 0 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
#[global] Instance :
AsValRecs' mcas_2٠lock 1 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
#[global] Instance :
AsValRecs' mcas_2٠eval 2 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
#[global] Instance :
AsValRecs' mcas_2٠determine 3 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
Definition mcas_2٠make : val :=
𝗳𝘂𝗻 "v" →
𝗹𝗲𝘁 "_gid" = 𝗶𝗱 𝗶𝗻
𝗹𝗲𝘁 "casn" = { §mcas_2٠After, 𝗽𝗿𝗼𝗽𝗵 } 𝗶𝗻
𝗹𝗲𝘁 "state" = { "casn", "v", "v" } 𝗶𝗻
𝗿𝗲𝗳 "state".
Definition mcas_2٠get : val :=
𝗳𝘂𝗻 "loc" →
mcas_2٠eval !"loc".
Definition mcas_2٠mcas_2 : val :=
𝗳𝘂𝗻 "cmps" "cass" →
𝗹𝗲𝘁 "casn" = { §mcas_2٠After, 𝗽𝗿𝗼𝗽𝗵 } 𝗶𝗻
𝗹𝗲𝘁 "cass" =
list٠map
(𝗳𝘂𝗻 "cas" →
𝗹𝗲𝘁 "loc", "before", "after" = "cas" 𝗶𝗻
𝗹𝗲𝘁 "state" = { "casn", "before", "after" } 𝗶𝗻
("loc", "state"))
"cass"
𝗶𝗻
"casn" <-{mcas_2٠status} ‘mcas_2٠Undetermined@[ "cmps", "cass" ] ⍮
mcas_2٠determine_as "casn" "cass".
Definition mcas_2٠mcas_1 : val :=
𝗿𝗲𝗰 "mcas_1" "acc" "cmps" "cass" →
𝗺𝗮𝘁𝗰𝗵 "cmps" 𝘄𝗶𝘁𝗵
| [] →
mcas_2٠mcas_2 (list٠rev "acc") "cass"
| "cmp" :: "cmps" →
𝗹𝗲𝘁 "loc", "expected" = "cmp" 𝗶𝗻
𝗹𝗲𝘁 "state" = !"loc" 𝗶𝗻
𝗶𝗳 mcas_2٠eval "state" == "expected" 𝘁𝗵𝗲𝗻 (
"mcas_1" (("loc", "state") :: "acc") "cmps" "cass"
) 𝗲𝗹𝘀𝗲 (
false
)
𝗲𝗻𝗱.
Definition mcas_2٠mcas : val :=
𝗳𝘂𝗻 "cmps" "cass" →
mcas_2٠mcas_1 [] "cmps" "cass".
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.program_logic.identifier.
Require Import zoo_std.list.
Require Import zoo.options.
Notation "'mcas_2٠casn'" := (
in_type "zoo_mcas.mcas_2.state" 0
)(in custom zoo_field
).
Notation "'mcas_2٠before'" := (
in_type "zoo_mcas.mcas_2.state" 1
)(in custom zoo_field
).
Notation "'mcas_2٠after'" := (
in_type "zoo_mcas.mcas_2.state" 2
)(in custom zoo_field
).
Notation "'mcas_2٠loc'" := (
in_type "zoo_mcas.mcas_2.cas" 0
)(in custom zoo_proj
).
Notation "'mcas_2٠state'" := (
in_type "zoo_mcas.mcas_2.cas" 1
)(in custom zoo_proj
).
Notation "'mcas_2٠status'" := (
in_type "zoo_mcas.mcas_2.casn" 0
)(in custom zoo_field
).
Notation "'mcas_2٠proph'" := (
in_type "zoo_mcas.mcas_2.casn" 1
)(in custom zoo_field
).
Notation "'mcas_2٠Undetermined'" := (
in_type "zoo_mcas.mcas_2.status" 0
)(in custom zoo_tag
).
Notation "'mcas_2٠Before'" := (
in_type "zoo_mcas.mcas_2.status" 1
)(in custom zoo_tag
).
Notation "'mcas_2٠After'" := (
in_type "zoo_mcas.mcas_2.status" 2
)(in custom zoo_tag
).
Notation "'mcas_2٠cmps'" := (
in_type "zoo_mcas.mcas_2.status.Undetermined" 0
)(in custom zoo_proj
).
Notation "'mcas_2٠cass'" := (
in_type "zoo_mcas.mcas_2.status.Undetermined" 1
)(in custom zoo_proj
).
Definition mcas_2٠clear : val :=
𝗳𝘂𝗻 "cass" "is_after" →
𝗶𝗳 "is_after" 𝘁𝗵𝗲𝗻 (
list٠iter
(𝗳𝘂𝗻 "cas" →
"cas".<mcas_2٠state> <-{mcas_2٠before}
"cas".<mcas_2٠state>.{mcas_2٠after})
"cass"
) 𝗲𝗹𝘀𝗲 (
list٠iter
(𝗳𝘂𝗻 "cas" →
"cas".<mcas_2٠state> <-{mcas_2٠after}
"cas".<mcas_2٠state>.{mcas_2٠before})
"cass"
).
Definition mcas_2٠status_to_bool : val :=
𝗳𝘂𝗻 "status" →
"status" == §mcas_2٠After.
Definition mcas_2٠finish : val :=
𝗳𝘂𝗻 "gid" "casn" "status" →
𝗺𝗮𝘁𝗰𝗵 "casn".{mcas_2٠status} 𝘄𝗶𝘁𝗵
| mcas_2٠Before →
false
| mcas_2٠After →
true
| mcas_2٠Undetermined "cmps" "cass" 𝗮𝘀 "old_status" →
𝗹𝗲𝘁 "status" =
𝗶𝗳 "status" == §mcas_2٠Before 𝘁𝗵𝗲𝗻 (
§mcas_2٠Before
) 𝗲𝗹𝘀𝗲 𝗶𝗳
list٠∀
(𝗳𝘂𝗻 "cmp" →
!"cmp".<mcas_2٠loc> == "cmp".<mcas_2٠state>)
"cmps"
𝘁𝗵𝗲𝗻 (
§mcas_2٠After
) 𝗲𝗹𝘀𝗲 (
§mcas_2٠Before
)
𝗶𝗻
𝗹𝗲𝘁 "is_after" = mcas_2٠status_to_bool "status" 𝗶𝗻
𝗶𝗳
𝗿𝗲𝘀𝗼𝗹𝘃𝗲
(𝗰𝗮𝘀 "casn".[mcas_2٠status] "old_status" "status")
"casn".{mcas_2٠proph}
("gid", "is_after")
𝘁𝗵𝗲𝗻 (
mcas_2٠clear "cass" "is_after"
) 𝗲𝗹𝘀𝗲 (
()
) ⍮
mcas_2٠status_to_bool "casn".{mcas_2٠status}
𝗲𝗻𝗱.
#[local] Definition __zoo_recs_0 :=
( 𝗿𝗲𝗰𝘀 "determine_as" "casn" "cass" →
𝗹𝗲𝘁 "gid" = 𝗶𝗱 𝗶𝗻
𝗺𝗮𝘁𝗰𝗵 "cass" 𝘄𝗶𝘁𝗵
| [] →
mcas_2٠finish "gid" "casn" §mcas_2٠After
| "cas" :: "continue" 𝗮𝘀 "retry" →
𝗹𝗲𝘁 "loc", "state" = "cas" 𝗶𝗻
𝗹𝗲𝘁 "proph" = 𝗽𝗿𝗼𝗽𝗵 𝗶𝗻
𝗹𝗲𝘁 "old_state" = !"loc" 𝗶𝗻
𝗶𝗳 "state" == "old_state" 𝘁𝗵𝗲𝗻 (
"determine_as" "casn" "continue"
) 𝗲𝗹𝘀𝗲 𝗶𝗳
𝗹𝗲𝘁 "@tmp" =
"state".{mcas_2٠before} == "eval" "old_state"
𝗶𝗻
𝗿𝗲𝘀𝗼𝗹𝘃𝗲 𝘀𝗸𝗶𝗽 "proph" "@tmp" ⍮
"@tmp"
𝘁𝗵𝗲𝗻 (
"lock" "casn" "loc" "old_state" "state" "retry" "continue"
) 𝗲𝗹𝘀𝗲 (
mcas_2٠finish "gid" "casn" §mcas_2٠Before
)
𝗲𝗻𝗱
𝘄𝗶𝘁𝗵 "lock" "casn" "loc" "old_state" "state" "retry" "continue" →
𝗺𝗮𝘁𝗰𝗵 "casn".{mcas_2٠status} 𝘄𝗶𝘁𝗵
| mcas_2٠Before →
false
| mcas_2٠After →
true
| mcas_2٠Undetermined ⎽ ⎽ →
𝗶𝗳
𝗰𝗮𝘀 "loc".[contents] "old_state" "state"
𝘁𝗵𝗲𝗻 (
"determine_as" "casn" "continue"
) 𝗲𝗹𝘀𝗲 (
"determine_as" "casn" "retry"
)
𝗲𝗻𝗱
𝘄𝗶𝘁𝗵 "eval" "state" →
𝗶𝗳 "determine" "state".{mcas_2٠casn} 𝘁𝗵𝗲𝗻 (
"state".{mcas_2٠after}
) 𝗲𝗹𝘀𝗲 (
"state".{mcas_2٠before}
)
𝘄𝗶𝘁𝗵 "determine" "casn" →
𝗺𝗮𝘁𝗰𝗵 "casn".{mcas_2٠status} 𝘄𝗶𝘁𝗵
| mcas_2٠Before →
false
| mcas_2٠After →
true
| mcas_2٠Undetermined ⎽ "cass" →
"determine_as" "casn" "cass"
𝗲𝗻𝗱
)%zoo_recs.
Definition mcas_2٠determine_as :=
ValRecs 0 __zoo_recs_0.
Definition mcas_2٠lock :=
ValRecs 1 __zoo_recs_0.
Definition mcas_2٠eval :=
ValRecs 2 __zoo_recs_0.
Definition mcas_2٠determine :=
ValRecs 3 __zoo_recs_0.
#[global] Instance :
AsValRecs' mcas_2٠determine_as 0 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
#[global] Instance :
AsValRecs' mcas_2٠lock 1 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
#[global] Instance :
AsValRecs' mcas_2٠eval 2 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
#[global] Instance :
AsValRecs' mcas_2٠determine 3 __zoo_recs_0 [
mcas_2٠determine_as ;
mcas_2٠lock ;
mcas_2٠eval ;
mcas_2٠determine
].
Definition mcas_2٠make : val :=
𝗳𝘂𝗻 "v" →
𝗹𝗲𝘁 "_gid" = 𝗶𝗱 𝗶𝗻
𝗹𝗲𝘁 "casn" = { §mcas_2٠After, 𝗽𝗿𝗼𝗽𝗵 } 𝗶𝗻
𝗹𝗲𝘁 "state" = { "casn", "v", "v" } 𝗶𝗻
𝗿𝗲𝗳 "state".
Definition mcas_2٠get : val :=
𝗳𝘂𝗻 "loc" →
mcas_2٠eval !"loc".
Definition mcas_2٠mcas_2 : val :=
𝗳𝘂𝗻 "cmps" "cass" →
𝗹𝗲𝘁 "casn" = { §mcas_2٠After, 𝗽𝗿𝗼𝗽𝗵 } 𝗶𝗻
𝗹𝗲𝘁 "cass" =
list٠map
(𝗳𝘂𝗻 "cas" →
𝗹𝗲𝘁 "loc", "before", "after" = "cas" 𝗶𝗻
𝗹𝗲𝘁 "state" = { "casn", "before", "after" } 𝗶𝗻
("loc", "state"))
"cass"
𝗶𝗻
"casn" <-{mcas_2٠status} ‘mcas_2٠Undetermined@[ "cmps", "cass" ] ⍮
mcas_2٠determine_as "casn" "cass".
Definition mcas_2٠mcas_1 : val :=
𝗿𝗲𝗰 "mcas_1" "acc" "cmps" "cass" →
𝗺𝗮𝘁𝗰𝗵 "cmps" 𝘄𝗶𝘁𝗵
| [] →
mcas_2٠mcas_2 (list٠rev "acc") "cass"
| "cmp" :: "cmps" →
𝗹𝗲𝘁 "loc", "expected" = "cmp" 𝗶𝗻
𝗹𝗲𝘁 "state" = !"loc" 𝗶𝗻
𝗶𝗳 mcas_2٠eval "state" == "expected" 𝘁𝗵𝗲𝗻 (
"mcas_1" (("loc", "state") :: "acc") "cmps" "cass"
) 𝗲𝗹𝘀𝗲 (
false
)
𝗲𝗻𝗱.
Definition mcas_2٠mcas : val :=
𝗳𝘂𝗻 "cmps" "cass" →
mcas_2٠mcas_1 [] "cmps" "cass".