-- GeNeRaTeD fOr: ../../CBS/Funcons/Computations/Control flow/Abnormal/Failing/dereference.aterm
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Computations.ControlFlow.Abnormal.Failing.Dereference where

import Funcons.EDSL

entities = []

types = typeEnvFromList
    []

funcons = libFromList
    [("dereference",StrictFuncon stepDereference)]

-- |
-- /dereference(P)/ fails if the pointer /P/ is /null/ , otherwise it returns
--   the value referenced by /P/ .
dereference_ fargs = FApp "dereference" (FTuple fargs)
stepDereference fargs =
    evalRules [rewrite1,rewrite2] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "reference" [VPMetaVar "V"]] env
            rewriteTermTo (TVar "V") env
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "null" []] env
            rewriteTo (FName "fail")