CurryInfo: contract-prover-4.0.0 / ContractProver.nondetTrans
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 |