| definition: |
nondetTrans :: [(QName,Bool)] -> Int -> Term -> (Term,Int)
nondetTrans ndinfo ix trm = case trm of
TConst _ -> (trm,ix)
TSVar _ -> (trm,ix)
TComb f args -> let (targs,i1) = nondetTransL ndinfo ix args
in if maybe False
(\qn -> maybe False id (lookup qn ndinfo))
(untransOpName (qidName f))
then (TComb (addChoiceType f) (TSVar i1 : targs), i1+1)
else (TComb f targs, i1)
Forall vs arg -> let (targ,ix1) = nondetTrans ndinfo ix arg
in (Forall vs targ, ix1)
Exists vs arg -> let (targ,ix1) = nondetTrans ndinfo ix arg
in (Exists vs targ, ix1)
ESMT.Let bs e -> let (tbt,ix1) = nondetTransL ndinfo ix (map snd bs)
(te,ix2) = nondetTrans ndinfo ix1 e
in (ESMT.Let (zip (map fst bs) tbt) te, ix2)
where
addChoiceType (Id n) = Id n
addChoiceType (As n tp) = As n (SComb "Func" [SComb "Choice" [], tp])
|
| demand: |
argument 3 |
| deterministic: |
deterministic operation |
| documentation: |
-- Translate a term w.r.t. non-determinism information by -- adding fresh `Choice` variable arguments to non-deterministic operations. -- The fresh variable index is passed as a state. |
| failfree: |
(_, _, _) |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{(_,_,{TConst}) |-> {(,)} || (_,_,{TSVar}) |-> {(,)} || (_,_,{TComb}) |-> {(,)} || (_,_,{Forall}) |-> {(,)} || (_,_,{Exists}) |-> {(,)} || (_,_,{Let}) |-> {(,)}}
|
| name: |
nondetTrans |
| precedence: |
no precedence defined |
| result-values: |
{(,)}
|
| signature: |
[((String, String), Prelude.Bool)] -> Prelude.Int -> ESMT.Term -> (ESMT.Term, Prelude.Int) |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |