|
definition:
|
applyFunc :: TAFuncDecl -> [(Int,TypeExpr)] -> TransStateM TAExpr
applyFunc fdecl targs = do
fv <- getFreshVarIndex
let tsub = maybe (error $ "applyFunc: types\n" ++
show (argTypes (funcType fdecl)) ++ "\n" ++
show (map snd targs) ++ "\ndo not match!")
id
(matchTypes (argTypes (funcType fdecl)) (map snd targs))
(ARule _ orgargs orgexp) = substRule tsub (funcRule fdecl)
exp = rnmAllVars (renameRuleVar fv orgargs) orgexp
setFreshVarIndex (max fv (maximum (0 : args ++ allVars exp) + 1))
return $ simpExpr $ applyArgs exp (drop (length orgargs) args)
where
args = map fst targs
-- renaming function for variables in original rule:
renameRuleVar fv orgargs r = maybe (r + fv)
(args!!)
(elemIndex r (map fst orgargs))
applyArgs e [] = e
applyArgs e (v:vs) =
-- eta-expansion
let et@(FuncType vt rt) = annExpr e
e_v = AComb rt FuncCall (pre "apply", FuncType et vt) [e, AVar vt v]
in applyArgs e_v vs
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
---------------------------------------------------------------------------
-- Applies a function declaration on a list of arguments,
-- which are assumed to be variable indices, and returns
-- the renamed body of the function declaration.
-- All local variables are renamed by adding `freshvar` to them.
-- Also the new fresh variable index is returned.
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,_) |-> _}
|
|
name:
|
applyFunc
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr
-> [(Prelude.Int, FlatCurry.Types.TypeExpr)]
-> Control.Monad.Trans.State.StateT TransState.TransState (Control.Monad.Trans.State.StateT VerifierState.VState Prelude.IO) (FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr)
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|