Skip to content

Commit

Permalink
document translation of loop combinators
Browse files Browse the repository at this point in the history
  • Loading branch information
owestphal committed Aug 17, 2023
1 parent 4034a46 commit 7824e4f
Showing 1 changed file with 12 additions and 6 deletions.
18 changes: 12 additions & 6 deletions src/Test/IOTasks/Internal/Specification.hs
Original file line number Diff line number Diff line change
Expand Up @@ -98,34 +98,40 @@ exit = E
--
-- The 'whileNot' function takes a condition and a body specification, and constructs a loop structure where:
--
-- * The 'ConditionTerm Bool' argument is the condition to be evaluated at the beginning of each iteration. The loop continues as long as the condition is 'False'.
-- * The 'ConditionTerm' 'Bool' argument is the condition to be evaluated at the beginning of each iteration. The loop continues as long as the condition is 'False'.
-- * The 'Specification' argument is the body of the loop, executed while the condition is 'False'.
--
-- The function assumes that the body specification does not contain a top-level 'exit' marker.
--
-- > whileNot c bdy = tillExit (branch c exit bdy)
whileNot :: ConditionTerm Bool -> Specification -> Specification
whileNot c bdy = TillE (branch c exit bdy) nop
whileNot c bdy = tillExit (branch c exit bdy)

-- | Represents a loop structure in a specification, performing the body while the condition holds.
--
-- The 'while' function takes a condition and a body specification, and constructs a loop structure where:
--
-- * The 'ConditionTerm Bool' argument is the condition to be evaluated at the beginning of each iteration.
-- * The 'ConditionTerm' 'Bool' argument is the condition to be evaluated at the beginning of each iteration.
-- * The 'Specification' argument is the body of the loop, executed while the condition is 'True'.
--
-- The function assumes that the body specification does not contain a top-level 'exit' marker.
--
-- > while c bdy = tillExit (branch c bdy exit)
while :: ConditionTerm Bool -> Specification -> Specification
while c bdy = TillE (branch c bdy exit) nop
while c bdy = tillExit (branch c bdy exit)

-- | Represents a loop structure in a specification, performing the body at least once and then further while the condition does not hold.
--
-- The 'repeatUntil' function takes a body specification and a condition, and constructs a loop structure where:
--
-- * The 'Specification' argument is the body of the loop, executed at least once and then further times while the condition is 'False'.
-- * The 'ConditionTerm Bool' argument is the condition to be evaluated at the end of each iteration. The loop continues until the condition becomes 'True'.
-- * The 'ConditionTerm' 'Bool' argument is the condition to be evaluated at the end of each iteration. The loop continues until the condition becomes 'True'.
--
-- The function assumes that the body specification does not contain a top-level 'exit' marker.
--
-- > repeatUntil bdy c = bdy <> tillExit (branch c exit bdy)
repeatUntil :: Specification -> ConditionTerm Bool -> Specification
repeatUntil bdy c = bdy <> whileNot c bdy
repeatUntil bdy c = bdy <> tillExit (branch c exit bdy)

vars :: Specification -> [SomeVar]
vars = nub . go where
Expand Down

0 comments on commit 7824e4f

Please sign in to comment.