This module contains a transformation from possibly non-deterministically defined operations into purely deterministic operations. The transformation is based on the "planned choices" approach described in this paper:
S. Antoy, M. Hanus, and S. Libby: Proving non-deterministic computations in Agda. In Proc. of the 24th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2016), volume 234 of Electronic Proceedings in Theoretical Computer Science, pages 180--195. Open Publishing Association, 2017.
Thus, an additional "choice plan" argument is added to each non-deterministic operation. This plan determines the branches chosen by the operation to compute some value.
This transformation can be used to verify non-determinstic operations by showing their correct behavior for all possible plans.
Author: Michael Hanus
Version: September 2019
nondetOfFuncDecls
:: [AFuncDecl TypeExpr] -> [((String,String),Bool)]
Returns the non-determinism status for all functions in a list of function declarations. |
addChoiceFuncDecl
:: [((String,String),Bool)] -> (TypeExpr,(String,String),(String,String),(String,String)) -> AFuncDecl TypeExpr -> AFuncDecl TypeExpr
Add a "choice plan" argument to a function declaration for all non-deterministic functions (according to first argument). |
Returns the non-determinism status for all functions in a list of function declarations. It is assumed that this list contains the declarations of all functions occurring in these declarations. It is implemented by a very simple fixpoint iteration. This is sufficient for the small lists considered in this application. |
Add a "choice plan" argument to a function declaration for all
non-deterministic functions (according to first argument).
The first argument maps qualified function names into a Boolean flag
which is true if the function is (or might be) non-deterministic.
The second argument is a tuple cpType -- the type of the choice plan chooseF :: cpType -> Bool -- the name of the choose operation lchoiceF :: cpType -> cpType -- the name of the lchoice operation rchoiceF :: cpType -> cpType -- the name of the lchoice operation For instance, these types and operations can be implemented as follows in Curry: data Choice = Plan Bool Choice Choice choose :: Choice -> Bool choose (Plan True _ _) = True choose (Plan False _ _) = False lchoice :: Choice -> Choice lchoice (Plan _ l _) = l rchoice :: Choice -> Choice rchoice (Plan _ _ r) = r As an example, consider the following operations: insert :: a -> [a] -> [a] insert x [] = [x] insert x (y:ys) = x : y: ys ? y : insert x ys perm :: [a] -> [a] perm [] = [] perm (x:xs) = insert x (perm xs) Since both operations are non-deterministic, they are transformed into the following code: insert :: Choice -> a -> [a] -> [a] insert _ x [] = [x] insert c x (y:ys) = if choose c then x : y: ys else y : insert (lchoice c) x ys perm :: Choice -> [a] -> [a] perm _ [] = [] perm c (x:xs) = insert (lchoice c) x (perm (rchoice c) xs) |