Mercurial > hg > Papers > 2021 > soto-prosym

view Paper/src/agda-hoare-interpret.agda.replaced @ 14:393c839f987b default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
DONE
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sat, 08 Jan 2022 12:41:39 +0900
parents 339fb67b4375
children
line wrap: on
line source

{-!$\#$! TERMINATING !$\#$!-}
interpret : Env !$\rightarrow$! Comm !$\rightarrow$! Env
interpret env Skip = env
interpret env Abort = env
interpret env (PComm x) = x env
interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
interpret env (If x then else) with x env
... | true = interpret env then
... | false = interpret env else
interpret env (While x comm) with x env
... | true = interpret (interpret env comm) (While x comm)
... | false = env