CurryInfo: contract-prover-4.0.0 / ContractProver.applyFunc

definition: Info
 
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) =
    -- simple hack for eta-expansion since the type annotations are not used:
    let e_v =  AComb failed FuncCall
                     (pre "apply", failed) [e, AVar failed v]
    in applyArgs e_v vs
demand: Info
 no demanded arguments
deterministic: Info
 deterministic operation
documentation: Info
 
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: Info
 <FAILING>
indeterministic: Info
 referentially transparent operation
infix: Info
 no fixity defined
iotype: Info
 {(_,_) |-> _}
name: Info
 applyFunc
precedence: Info
 no precedence defined
result-values: Info
 _
signature: Info
 FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr
-> [(Prelude.Int, FlatCurry.Types.TypeExpr)]
-> Control.Monad.Trans.State.StateT TransState Prelude.IO (FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr)
solution-complete: Info
 operation might suspend on free variables
terminating: Info
 possibly non-terminating
totally-defined: Info
 possibly non-reducible on same data term