# Theory BoolProgs_Extras

```theory BoolProgs_Extras
imports
BoolProgs
"HOL-Library.Mapping"
begin

context begin interpretation BoolProg_Syntax .

subsection ‹Macros›

text ‹Counters ≈ bounded natural numbers›

(* Vars: offset, number of vars, value *)
fun set_counter :: "nat list ⇒ bexp list ⇒ nat ⇒ nat ⇒ nat ⇒ com"
where
"set_counter vs bs _ 0 _ = vs ::= bs"
| "set_counter vs bs pos (Suc l) 0 = set_counter (pos#vs) (FF#bs) (Suc pos) l 0"
| "set_counter vs bs pos (Suc l) (Suc n) = set_counter (pos#vs) (TT#bs) (Suc pos) l n"

(* Vars: offset, number of vars, value to compare to *)
definition counter_eq :: "nat ⇒ nat ⇒ nat ⇒ bexp" where
"counter_eq pos m n = (if n > m then FF else
let posT = [0..<n] in
let posF = [n..<m] in
let bexps = (map (λx. V (pos + x)) posT) @ (map (λx. Not (V (pos + x))) posF) in
foldl And TT bexps)"

(* Vars: offset, number of vars *)
fun inc_counter :: "nat list ⇒ bexp list ⇒ nat ⇒ nat ⇒ com"
where
"inc_counter vs bs pos 0 = vs ::= bs"
| "inc_counter vs bs pos (Suc n) = IF V pos THEN inc_counter vs bs (Suc pos) n ELSE (pos#vs) ::= (TT#bs)"

fun dec_counter_toggle :: "nat list ⇒ bexp list ⇒ bool ⇒ nat ⇒ com" where
"dec_counter_toggle vs bs False _ = vs ::= bs"
|"dec_counter_toggle vs bs True pos = ((pos - 1)#vs) ::= (FF#bs)"

fun dec_counter' :: "nat list ⇒ bexp list ⇒ bool ⇒ nat ⇒ nat ⇒ com"
where
"dec_counter' vs bs start pos 0 = dec_counter_toggle vs bs start pos"
| "dec_counter' vs bs start pos (Suc n) =
IF Not (V pos) THEN (dec_counter_toggle vs bs start pos)
ELSE dec_counter' vs bs True (Suc pos) n"

(* Vars: offset, number of vars *)
definition dec_counter :: "nat list ⇒ bexp list ⇒ nat ⇒ nat ⇒ com" where
"dec_counter vs bs = dec_counter' vs bs False"

(* Array access via run-time variable. Emulated by checking all possible values.
Vars: ctr: function 'nat ⇒ bexp' - returns true if the counter is of a specific value
act: function 'nat ⇒ com' - action to take with value if counter is value
m: number of values (checked are [0,m[) *)
definition array_access where
"array_access ctr act m = foldl (λbexp c. IF ctr c THEN act c ELSE bexp) SKIP [0..<m]"

definition array_check where
"array_check ctr chk m = foldl (λbexp c. And (Or (Not (ctr c)) (chk c)) (Or (ctr c) bexp)) FF [0..<m]"

subsection ‹Gather statistics›

fun stat' where
"stat' (a,t,c,g) instr = (case instr of
AssI _ _ ⇒ (Suc a,t,c,g)
| TestI _ _ ⇒ (a,Suc t,c,g)
| ChoiceI _ ⇒ (a,t,Suc c,g)
| GotoI _ ⇒ (a,t,c,Suc g))"

definition stats where
"stats ls = foldl stat' (0,0,0,0) ls"

subsection ‹Misc›
(* this is only used for the code setup in Programs/* *)
type_synonym const_map = "(String.literal, bexp) mapping"
type_synonym fun_map = "(String.literal, nat ⇒ bexp) mapping"

definition mapping_from_list :: "('a × 'b) list ⇒ ('a, 'b) mapping"
where
"mapping_from_list = foldl (λm (k,v). Mapping.update k v m) Mapping.empty"
end

end
```