| definition: |
genSpecGroundEquivTest :: [QName] -> QName -> CContext -> CTypeExpr -> CFuncDecl
genSpecGroundEquivTest prefuns qf@(mn,fn) clscon texp =
CFunc (mn, fn ++ satSpecSuffix) ar Public
(CQualType (addShowContext clscon) (propResultType texp))
[simpleRule (map CPVar cvars) $
addPreCond prefuns [qf,qfspec] cvars
(applyF (easyCheckModule,"<~>")
[applyF qf (map CVar cvars),
applyF (mn,toSpecName fn) (map CVar cvars)])]
where
ar = arityOfType texp
cvars = map (\i -> (i,"x" ++ show i)) [1 .. ar]
qfspec = (mn, toSpecName fn)
|
| demand: |
argument 2 |
| deterministic: |
deterministic operation |
| documentation: |
-- Transforms a function declaration into a ground equivalence test -- against the specification (i.e., an operation named `f'spec` exists). -- The generated specification test is of the form -- fSatisfiesSpecification x1...xn = -- f'pre x1...xn ==> (f x1...xn <~> f'spec x1...xn) |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| name: |
genSpecGroundEquivTest |
| precedence: |
no precedence defined |
| result-values: |
{CFunc}
|
| signature: |
[(String, String)] -> (String, String) -> AbstractCurry.Types.CContext -> AbstractCurry.Types.CTypeExpr -> AbstractCurry.Types.CFuncDecl |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |