Module IdentifyCases

This module provides transforms FlatCurry programs for concolic evaluation:

• For every case expression a fresh identifier is introduced for the scrutinized expression. For instance the expression
  case e of p1 -> e1; ... ; pn -> en
  is transformed to
  let cid = e in case cid of p1 -> e1; ... ; pn -> en
  where cid is a fresh identifier
• Furthermore, cases with boolean expressions as arguments are normalized in the following form:
  case c1 && c2 of case c1 of True -> e1 is transformed to True -> case c2 of False -> e2 True -> e1 False -> e2 False -> e2
  Disjunctions are transformed in a similar way.

Author: Jan Tikovsky

Version: August 2017

Summary of exported operations:

get :: ICM Int

put :: Int -> ICM ()

freshID :: ICM Int    Generate a fresh identifier

idCases :: [AFuncDecl a] -> ([AFuncDecl (a,Maybe Int,Bool)],Int)    Annotate case expressions with fresh identifiers and mark literals

idFunc :: AFuncDecl (a,Maybe Int,Bool) -> ICM (AFuncDecl (a,Maybe Int,Bool))

idRule :: ARule (a,Maybe Int,Bool) -> ICM (ARule (a,Maybe Int,Bool))

idExpr :: AExpr (a,Maybe Int,Bool) -> ICM (AExpr (a,Maybe Int,Bool))

Exported datatypes:

---

ICM

Identify Cases Monad

Constructors:

• IC :: (VarIndex -> (a,VarIndex)) -> ICM a

  Fields:

  • runICM :: (VarIndex -> (a,VarIndex))

---

Exported operations:

get :: ICM Int

put :: Int -> ICM ()

freshID :: ICM Int    Generate a fresh identifier

idCases :: [AFuncDecl a] -> ([AFuncDecl (a,Maybe Int,Bool)],Int)    Annotate case expressions with fresh identifiers and mark literals

idFunc :: AFuncDecl (a,Maybe Int,Bool) -> ICM (AFuncDecl (a,Maybe Int,Bool))

idRule :: ARule (a,Maybe Int,Bool) -> ICM (ARule (a,Maybe Int,Bool))

idExpr :: AExpr (a,Maybe Int,Bool) -> ICM (AExpr (a,Maybe Int,Bool))