CurryInfo: verify-non-fail-2.0.0 / Verify.NonFailConditions.genNonFailFunction

genNonFailFunction :: [FuncDecl] -> (QName, NonFailCond) -> (String,FuncDecl)
genNonFailFunction fdecls (qfc,(_,cnd)) =
  maybe (error $ "genNonFailFunction: function '" ++ snd qfc ++ "'' not found!")
        (\fdecl -> genNonFailFunc fdecl)
        (find (\fd -> funcName fd == qfc) fdecls)
 where
  genNonFailFunc (Func (mn,fn) ar vis texp _) =
    (fn,
     Func (mn, encodeContractName $ fn ++ nonfailSuffix) ar vis
          (nftype [1..ar] texp)
          (Rule [1..ar] (if all (`elem` [1..ar]) nfcondvars
                           then nfcondexp
                           else Free (nfcondvars \\ [1..ar]) nfcondexp)))
   where
    nftype []     _     = TCons (pre "Bool") []
    nftype (v:vs) ftype = case ftype of
      FuncType t1 t2 -> FuncType t1 (nftype vs t2)
      ForallType _ t -> nftype (v:vs) t
      _              -> error "Illegal function type in genNonFailFunction"

  nfcondexp = updCombs transClassImplOp (simpExpr cnd)
  nfcondvars = nub (allFreeVars nfcondexp)

  -- transform possible implementation of a class operation, e.g.,
  -- `_impl#minBound#Prelude.Bounded#Prelude.Char#` -> `minBound :: Char`
  transClassImplOp ct qf@(mnf,fnf) args = case splitOn "#" fnf of
    [impl,fname,_,types,_] | impl == "_impl"
       -> maybe (Comb ct (mnf,fname) args)
                (Typed (Comb ct (mnf,fname) args))
                (typeString2TExp types)
    _  -> Comb ct qf args
   where
    typeString2TExp s | s == "Prelude.Bool"      = Just fcBool
                      | s == "Prelude.Char"      = Just fcChar
                      | s == "Prelude.Int"       = Just fcInt
                      | s == "Prelude.Float"     = Just fcFloat
                      | s == "Prelude.Ordering"  = Just fcOrdering
                      | otherwise                = Nothing

argument 2

deterministic operation

--- Generates the function representing the non-fail condition for a given
--- function and non-fail condition.
--- The first argument is the list of all functions of the module.

referentially transparent operation

no fixity defined

{(_,{(,)}) |-> _}

genNonFailFunction

no precedence defined

_

[FlatCurry.Types.FuncDecl]
-> ((String, String), ([(Prelude.Int, FlatCurry.Types.TypeExpr)], FlatCurry.Types.Expr))
-> (String, FlatCurry.Types.FuncDecl)

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term