CurryInfo: contract-prover-4.0.0 / ContractProver.applyFunc

 
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

 no demanded arguments

 deterministic operation

 
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.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_) |-> _}

 applyFunc

 no precedence defined

 _

 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)

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term