I am trying to implement Logical Foundation’s ImpCEvalFun with an extension for nondeterminism.
In order for the evaluation of programs like:
<{
(X := 1 !! X := 2);
(X := 3);
X = 2 -> skip
}>
Where !! is equivalent to non-deterministic choice and -> represents a guard on which if failing, you need to backtrack and choose an alternative, I need to write my evaluator in continuation-passing style.
I started by implementing a naif version of the step evaluator in CSP:
Fixpoint ceval_step_cont_naif (st: state) (c: com) (cont: list (state * com)) (i: nat) :=
match i with
| O => OutOfGas
| S i' => match c with
| <{skip}> => match cont with
| [] => Success (st, cont)
| (st', <{skip}>) :: cont' => Success (st, cont')
| (st', c') :: cont' => (ceval_step_cont_naif st c' ((st, <{skip}>) :: cont') i')
end
| <{x := v}> => match cont with
| [] => Success ((x !-> aeval st v ; st), cont)
| (st', <{skip}>) :: cont' => Success ((x !-> aeval st v ; st), cont')
| (st', c') :: cont' => (ceval_step_cont_naif
(x !-> aeval st v; st)
c'
(((x !-> aeval st v; st), <{skip}>) :: cont')
i')
end
| <{c1 ; c2}> => match cont with
| [] => (ceval_step_cont_naif
st
c1
((st, c2) :: cont)
i')
| (st', <{skip}>) :: cont' => (ceval_step_cont_naif
st
c1
((st, c2) :: cont')
i')
| (st', c') :: cont' => (ceval_step_cont_naif
st
c1
((st, <{c2 ; c'}>) :: cont')
i')
end
| <{if b then c1 else c2 end}>
=> if (beval st b) then (ceval_step_cont_naif st c1 cont i')
else (ceval_step_cont_naif st c2 cont i')
| <{while b do c' end}>
=> if (beval st b)
then
match cont with
| [] => (ceval_step_cont_naif
st
c'
((st, c) :: cont)
i')
| (st', <{skip}>) :: cont' => (ceval_step_cont_naif
st
c'
((st, c) :: cont')
i')
| (st', c'') :: cont' => (ceval_step_cont_naif
st
c'
((st, <{c ; c''}>) :: cont')
i')
end
else
match cont with
| [] => Success (st, cont)
| (st', <{skip}>) :: cont' => Success (st, cont')
| (st', c'') :: cont' => (ceval_step_cont_naif
st
c''
((st, <{skip}>) :: cont')
i')
end
(* Here we are forcing the order of evaluation to start on the first term *)
| <{c1 !! c2}> => match cont with
| [] => (ceval_step_cont_naif
st
c1
((st, <{skip}>) :: (st, c2) :: cont)
i')
| (st', <{skip}>) :: cont' => (ceval_step_cont_naif
st
c1
((st, <{skip}>) :: (st, c2) :: cont')
i')
| (st', c') :: cont' => (ceval_step_cont_naif
st
c1
((st, c') :: (st, <{c2 ; c'}>) :: cont')
i')
end
| <{b -> c'}> => if (beval st b) then (ceval_step st c' cont i')
else match cont with
| [] => Fail
| [(_, _)] => Fail
| (_, _) :: (st', alt_c) :: cont' => (ceval_step_cont_naif
st'
alt_c
cont'
i')
end
end
end.
However, after noticing a lot of repetition, I tried writing a notation to simplify the “plundering”.
(* Plumbering hiding in continuation-passing style. None is equivalent to default *)
Reserved Notation "'WITH_CONT' cont 'LAST_CMD' f_last 'ELSE' new_st other_c f_cont gas"
(no associativity, at level 60).
Fixpoint ceval_step_cont (st: state) (c: com) (cont: list (state * com)) (i: nat) :=
match i with
| O => OutOfGas
| S i' => match c with
| <{skip}> => WITH_CONT cont
LAST_CMD (fun cont' => Success (st, cont'))
ELSE st None (fun _ cont' => (([], <{skip}>) :: cont')) i'
| <{x := v}> => WITH_CONT cont
LAST_CMD (fun cont' => Success ((x !-> aeval st v ; st), cont'))
ELSE (x !-> aeval st v; st) None (fun _ cont' => ([], <{skip}> :: cont')) i'
| <{c1 ; c2}> => WITH_CONT cont
LAST_CMD (fun cont' => ceval_step_cont st c1 ((st, c2) :: cont') i')
ELSE st c1 (fun c' cont' => ([], <{c2 ; c'}>) :: cont') i'
| <{if b then c1 else c2 end}>
=> if (beval st b) then (ceval_step_cont st c1 cont i')
else (ceval_step_cont st c2 cont i')
| <{while g do b end}>
=> if (beval st g)
then
WITH_CONT cont
LAST_CMD (fun cont' => ceval_step_cont st b (([], c) :: cont')) i'
ELSE st b (fun c' cont' => (([], <{c ; c'}>) :: cont')) i'
else
WITH_CONT cont
LAST_CMD (fun cont => Success (st, cont))
ELSE st None (fun _, cont' => (([], <{skip}>) :: cont')) i'
(* Here we are forcing the order of evaluation to start on the first term *)
| <{c1 !! c2}> => WITH_CONT cont
LAST_CMD (fun cont => ceval_step_cont st c1 (([], <{skip}>) :: (st, c2) :: cont) i')
ELSE st c1 (fun c' cont' => ((st, c') :: (st, <{c2 ; c'}>) :: cont')) i'
| <{b -> c'}> => if (beval st b) then ceval_step st c' cont i'
else match cont with
| [] => Fail
| [(_, _)] => Fail
| (_, _) :: (st', alt_c) :: cont' => ceval_step_cont st' alt_c cont' i'
end
end
end
where "'WITH_CONT' cont 'LAST_CMD' f_last 'ELSE' new_st c f_cont gas" :=
(match cont with
| [] => f_last cont
| (_, <{skip}>) :: cont' => f_last cont'
| (_, c') :: cont' => ceval_step_cont
new_st
(if (c =? None) then c' else c)
(f_cont c' cont')
gas
end)
.
It says that it is expecting a term level 200. I am not very used to working with defining my own notations, and as such, I have tried to look at the documentation of notation, but I haven’t been able to solve this.
Any help would be great. Thanks!