language-boogie 0.1.1 → 0.2

raw patch · 16 files changed

+3217/−2322 lines, 16 filesdep +ansi-terminaldep +lensdep +stream-monaddep ~containersdep ~language-boogiePVP ok

version bump matches the API change (PVP)

Dependencies added: ansi-terminal, lens, stream-monad

Dependency ranges changed: containers, language-boogie

API changes (from Hackage documentation)

Files

• Boogaloo.hs +155/−96
• Language/Boogie/AST.hs +6/−5
• Language/Boogie/DataFlow.hs +0/−135
• Language/Boogie/Environment.hs +328/−0
• Language/Boogie/ErrorAccum.hs +66/−0
• Language/Boogie/Generator.hs +61/−0
• Language/Boogie/Heap.hs +120/−0
• Language/Boogie/Interpreter.hs +1308/−846
• Language/Boogie/NormalForm.hs +23/−32
• Language/Boogie/Parser.hs +2/−2
• Language/Boogie/PrettyPrinter.hs +29/−2
• Language/Boogie/Tester.hs +0/−301
• Language/Boogie/TypeChecker.hs +884/−802
• Language/Boogie/Util.hs +208/−86
• Tests.hs +21/−9
• language-boogie.cabal +6/−6

@@ -8,152 +8,211 @@ import qualified Language.Boogie.Parser as Parser (program)
 import Language.Boogie.TypeChecker
 import Language.Boogie.PrettyPrinter
+import Language.Boogie.Heap
+import Language.Boogie.Environment
 import Language.Boogie.Interpreter
-import Language.Boogie.Tester
+import Language.Boogie.Generator
 import System.Environment
 import System.Console.CmdArgs
+import System.Console.ANSI
 import System.Random
 import Data.Time.Calendar
 import Data.List
 import Data.Map (Map, (!))
 import qualified Data.Map as M
 import Control.Monad.State
+import Control.Monad.Stream
 import Control.Applicative
+import Control.Lens hiding (Context, at)
 import Text.PrettyPrint hiding (mode)
 import Text.ParserCombinators.Parsec (parse, parseFromFile)
 
 programName = "boogaloo"
-versionName = "0.1"
-releaseDate = fromGregorian 2012 10 25
+versionName = "0.2"
+releaseDate = fromGregorian 2013 2 5
 
 -- | Execute or test a Boogie program, according to command-line arguments
 main = do
   res <- cmdArgsRun $ mode
   case res of
-    Exec file entry -> executeFromFile file entry
-    args -> testFromFile (file args) (proc_ args) (testMethod args) (verbose args)
+    Exec file proc_ bound random seed btmax invalid nexec pass fail outMax sum debug -> 
+      executeFromFile file proc_ (natToMaybe bound) random seed btmax invalid nexec pass fail (natToMaybe outMax) sum debug
+    Test file proc_ bound outMax debug ->
+      executeFromFile file proc_ (natToMaybe bound) False Nothing Nothing True True True True (natToMaybe outMax) True debug
+    RTest file proc_ bound seed outMax debug ->
+      executeFromFile file proc_ (natToMaybe bound) True seed Nothing True True True True (natToMaybe outMax) True debug      
+  where
+    natToMaybe n
+      | n >= 0      = Just n
+      | otherwise   = Nothing
 
 {- Command line arguments -}
 
 data CommandLineArgs
-    = Exec { file :: String, entry :: String }
-    | Test { file :: String, proc_ :: [String], limits :: (Integer, Integer), dlimits :: (Integer, Integer), verbose :: Bool  }
-    | RTest { file :: String, proc_ :: [String], limits :: (Integer, Integer), dlimits :: (Integer, Integer), tc_count :: Int, seed :: Maybe Int, verbose :: Bool }
+    = Exec { 
+        file :: String, 
+        proc_ :: String,
+        branch_max :: Integer,
+        random_ :: Bool,
+        seed :: Maybe Int,
+        exec_max :: Maybe Int, 
+        invalid :: Bool, 
+        nexec :: Bool,
+        pass :: Bool,
+        fail_ :: Bool,
+        out_max :: Int, 
+        summary_ :: Bool,
+        debug :: Bool
+      }
+    | Test { 
+        file :: String, 
+        proc_ :: String,
+        branch_max :: Integer,
+        out_max :: Int, 
+        debug :: Bool
+      }
+    | RTest { 
+        file :: String, 
+        proc_ :: String,
+        branch_max :: Integer,
+        seed :: Maybe Int,
+        out_max :: Int, 
+        debug :: Bool
+      }
       deriving (Data, Typeable, Show, Eq)
 
+-- | Default branching
+defaultBranch = 128
+
+-- | Default branching in exhaustive testing
+defaultExBranch = 8
+
+-- | Default number of test cases in random testing
+defaultRTC = 100
+
 execute = Exec {
-  entry = "Main"  &= help "Program entry point (must not have in- or out-parameters)" &= typ "PROCEDURE",
-  file  = ""      &= typFile &= argPos 0
+  proc_       = "Main"          &= help "Program entry point (default: Main)" &= typ "PROCEDURE",
+  file        = ""              &= typFile &= argPos 0,
+  branch_max  = defaultBranch   &= help ("Maximum number of possibilities for each non-deterministic choice; " ++
+                                       "unbounded if negative (default: " ++ show defaultBranch ++ ")"),
+  random_     = False           &= help "Make non-deterministic choices randomly (default: false)",
+  seed        = Nothing         &= help "Seed for the random number generator" &= typ "NUM",
+  exec_max    = Nothing         &= help "Maximum number of executions to try (default: unlimited)",
+  invalid     = False           &= help "Display invalid executions (default: false)" &= name "I",
+  nexec       = True            &= help "Display executions that cannot be carried out completely (default: true)" &= name "N",
+  pass        = True            &= help "Display passing executions (default: true)" &= name "P",
+  fail_       = True            &= help "Display failing executions (default: true)" &= name "F",
+  out_max      = 1              &= help "Maximum number of executions to display; unbounded if negative (default: 1)",
+  summary_    = False           &= help "Only print a summary of all executions and a list of unique failures (default: false)" &= name "S",
+  debug       = False           &= help "Debug output (default: false)"
   } &= auto &= help "Execute program"
-      
-test_ = Test {
-  proc_   = []      &= help "Procedures to test" &= typ "PROCEDURE",
-  limits  = (-3, 3) &= help "Interval of input values to try for an integer variable" &= typ "NUM, NUM",
-  dlimits = (0, 2)  &= help dlimitsMsg &= typ "NUM, NUM" ,
-  file    = ""      &= typFile &= argPos 0,
-  verbose = False   &= help verboseMsg
+  
+test = Test {
+  proc_       = "Main"          &= help "Program entry point (default: Main)" &= typ "PROCEDURE",
+  file        = ""              &= typFile &= argPos 0,
+  branch_max  = defaultExBranch &= help ("Maximum number of possibilities for each non-deterministic choice; " ++
+                                         "unbounded if negative (default: " ++ show defaultExBranch ++ ")"),
+  out_max     = -1              &= help "Maximum number of test cases; unbounded if negative (default: -1)",
+  debug       = False           &= help "Debug output (default: false)"
   } &= help "Test program exhaustively"
   
 rtest = RTest {
-  proc_     = []        &= help "Procedures to test" &= typ "PROCEDURE",
-  limits    = (-32, 32) &= help "Interval of input values to draw from for an integer variable" &= typ "NUM, NUM",
-  dlimits   = (0, 2)    &= help dlimitsMsg &= typ "NUM, NUM",
-  tc_count  = 10        &= help "Number of test cases to generate per procedure implementation" &= name "n" &= typ "NUM",
-  seed      = Nothing   &= help "Seed for the random number generator" &= typ "NUM",
-  file      = ""        &= typFile &= argPos 0,
-  verbose = False       &= help verboseMsg
+  proc_       = "Main"          &= help "Program entry point (default: Main)" &= typ "PROCEDURE",
+  file        = ""              &= typFile &= argPos 0,
+  branch_max  = defaultBranch   &= help ("Maximum number of possibilities for each non-deterministic choice; " ++
+                                         "unbounded if negative (default: " ++ show defaultBranch ++ ")"),
+  seed        = Nothing         &= help "Seed for the random number generator" &= typ "NUM",
+  out_max     = defaultRTC      &= help ("Number of test cases; unbounded if negative (default: " ++ show defaultRTC ++")"),
+  debug       = False           &= help "Debug output (default: false)"
   } &= help "Test program on random inputs"
-  
-dlimitsMsg = "Given a map with an integer domain, different range values will be tried for domain values in this interval"
-verboseMsg = "Output all executed test cases"
-    
-mode = cmdArgsMode $ modes [execute, test_, rtest] &= 
+      
+mode = cmdArgsMode $ modes [execute, test, rtest] &= 
   help "Boogie interpreter" &= 
   program programName &= 
   summary (programName ++ " v" ++ versionName ++ ", " ++ showGregorian releaseDate)
-  
--- | Set up a test method depending on command-line arguments  
-testMethod :: CommandLineArgs -> Program -> Context -> [Id] -> IO [TestCase]
-testMethod (Test _ _ limits dlimits _ ) program context procNames = 
-  let settings = ExhaustiveSettings {
-      esIntRange = interval limits,
-      esIntMapDomainRange = interval dlimits,
-      esGenericTypeRange = defaultGenericTypeRange context,
-      esMapTypeRange = defaultMapTypeRange context
-    }
-  in return $ testProgram settings program context procNames
-testMethod (RTest _ _ limits dlimits tc_count seed _) program context procNames = do
-  defaultGen <- getStdGen
-  randomGen <- case seed of
-    Nothing -> getStdGen
-    Just s -> return $ mkStdGen s
-  let settings = RandomSettings {
-      rsRandomGen = randomGen,
-      rsCount = tc_count,
-      rsIntLimits = limits,
-      rsIntMapDomainRange = interval dlimits,
-      rsGenericTypeRange = defaultGenericTypeRange context,
-      rsMapTypeRange = defaultMapTypeRange context     
-    }  
-  return $ testProgram settings program context procNames
     
 {- Interfacing internal modules -}
 
--- | Execute procedure entryPoint from file
+-- | Execute procedure proc_ from file
 -- | and output either errors or the final values of global variables
-executeFromFile :: String -> String -> IO ()
-executeFromFile file entryPoint = runOnFile printFinalState file
-  where
-    printFinalState p context = case M.lookup entryPoint (ctxProcedures context) of
-      Nothing -> print (text "Cannot find program entry point" <+> text entryPoint)
-      Just sig -> if not (goodEntryPoint sig)
-        then print (text "Program entry point" <+> text entryPoint <+> text "does not have the required signature" <+> doubleQuotes (sigDoc [] []))
-        else case executeProgram p context entryPoint of
-          Left err -> print err
-          Right env -> (print . varsDoc . envGlobals) env
-    goodEntryPoint sig = null (psigTypeVars sig) && null (psigArgTypes sig) && null (psigRetTypes sig)
-
--- | Test procedures procNames from file with a testMethod
--- | and output the test outcomes
-testFromFile :: String -> [String] -> (Program -> Context -> [String] -> IO [TestCase]) -> Bool -> IO ()
-testFromFile file procNames testMethod printAll = runOnFile printTestOutcomes file
+executeFromFile :: String -> String -> Maybe Integer -> Bool -> Maybe Int -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> IO ()
+executeFromFile file proc_ branch_max random seed exec_max invalid nexec pass fail out_max summary debug = runOnFile printFinalState file
   where
-    printTestOutcomes p context = do
-      let (present, missing) = partition (`M.member` ctxProcedures context) procNames
-      when (not (null missing)) $ print (text "Cannot find procedures under test:" <+> commaSep (map text missing))
-      testResults <- testMethod p context present
-      print $ testSessionSummary testResults
-      when printAll $ putStr "\n" >> mapM_ print testResults
+    printFinalState p context = case M.lookup proc_ (ctxProcedures context) of
+      Nothing -> printError (text "Cannot find procedure" <+> text proc_)
+      Just _ -> do
+        rGen <- case seed of
+          Nothing -> getStdGen
+          Just s -> return $ mkStdGen s      
+        let generator = if random then randomGenerator rGen branch_max else exhaustiveGenerator branch_max
+        let outs = (maybeTake out_max . filter keep . maybeTake exec_max) (outcomes p context generator)
+        if summary
+          then do
+            let sum = testSessionSummary outs 
+            print $ summaryDoc sum
+            zipWithM_ (printOne "Failure") [0..] (sUniqueFailures sum)
+          else if null outs
+            then printAux $ text "No executions to display"
+            else zipWithM_ (printOne "Execution") [0..] outs
+    outcomes p context generator = if exec_max == Just 1 || (keepAll && out_max == Just 1)
+      then [executeProgramDet p context branch_max proc_]
+      else executeProgram p context generator branch_max proc_
+    keepAll = invalid && nexec && pass && fail
+    maybeTake mLimit = case mLimit of
+      Nothing -> id
+      Just n -> take n
+    keep tc = 
+      (if invalid then True else (not . isInvalid) tc) &&
+      (if nexec then True else (not . isNonexecutable) tc) &&
+      (if pass then True else (not . isPass) tc) &&
+      (if fail then True else (not . isFail) tc)
+    printTestCase tc = do
+      print $ testCaseSummary debug tc
+      case tcFailure tc of
+        Just err -> do
+          printNewline
+          printError $ runtimeFailureDoc debug err
+          when debug (printSeparate $ finalStateDoc True tc)
+        Nothing -> printSeparate $ finalStateDoc debug tc
+    printOne title n tc = do
+      when (n > 0) $ do printNewline; printNewline
+      printAux $ text title <+> integer n
+      printTestCase tc
 
 -- | Parse file, type-check the resulting program, then execute command on the resulting program and type context
 runOnFile :: (Program -> Context -> IO ()) -> String -> IO ()      
 runOnFile command file = do 
   parseResult <- parseFromFile Parser.program file
   case parseResult of
-    Left parseErr -> print parseErr
-    Right p -> case checkProgram p of
-      Left typeErrs -> print (typeErrorsDoc typeErrs)
+    Left parseErr -> printError parseErr
+    Right p -> case typeCheckProgram p of
+      Left typeErrs -> printError (typeErrorsDoc typeErrs)
       Right context -> command p context
       
+{- Output -}
+
+-- | Output errors in red
+printError e = do
+  setSGR [SetColor Foreground Vivid Red]
+  print e
+  setSGR [Reset]
+  
+-- | Output auxiliary messages in khaki  
+printAux msg = do
+  setSGR [SetColor Foreground Dull Yellow]
+  print msg
+  setSGR [Reset]
+  
+printNewline = putStr "\n"  
+  
+printSeparate doc = when (not (isEmpty doc)) (do printNewline; print doc)
+      
 {- Helpers for testing internal functions -}      
       
 -- | Harness for testing various internal functions
 harness file = runOnFile printOutcome file
   where
     printOutcome p context = do
-      let env = execState (collectDefinitions p) emptyEnv { envTypeContext = context }
-      print $ envGlobals env
-      
--- | Test that print . parse == print . parse . print .parse      
-testParser :: String -> IO ()      
-testParser file = do
-  result <- parseFromFile Parser.program file
-  case (result) of
-    Left err -> print err
-    Right p -> do
-      case parse Parser.program ('*' : file) (show p) of
-        Left err -> print err
-        Right p' -> if p == p'
-          then putStr ("Passed.\n")
-          else putStr ("Failed with different ASTs.\n")
-          +      let env = head (toList (execStateT (preprocess p) (initEnv context (exhaustiveGenerator (Just defaultBranch)) (Just defaultBranch))))
+      -- print $ memoryDoc True (env^.envMemory)
+      print $ abstractStoreDoc (env ^. envConstraints . amGlobals)

@@ -13,13 +13,14 @@ {- Types -}
 
 -- | Type
-data Type = BoolType | IntType |
-  MapType [Id] [Type] Type |
-  Instance Id [Type]
+data Type = BoolType |        -- ^ bool 
+  IntType |                   -- ^ int
+  MapType [Id] [Type] Type |  -- 'MapType' @type_vars domains range@ : arrow type (used for maps, function and procedure signatures)
+  IdType Id [Type]            -- 'IdType' @name args@: type denoted by an identifier (either type constructor, possibly with arguments, or a type variable)
   deriving Eq -- syntactic equality
 
 -- | 'nullaryType' @id@ : type denoted by @id@ without arguments
-nullaryType id = Instance id []
+nullaryType id = IdType id []
 
 -- | Dummy type used during type checking to denote error
 noType = nullaryType "NoType"
@@ -111,7 +112,7 @@ {- Specs -}
 
 -- | Types of specification clauses
-data SpecType = Inline | Precondition | Postcondition | LoopInvariant | Where
+data SpecType = Inline | Precondition | Postcondition | LoopInvariant | Where | Axiom
   deriving Eq
 
 -- | Specification clause

@@ -1,135 +0,0 @@--- | Data-flow analysis on Boogie code
-module Language.Boogie.DataFlow (liveVariables, liveInputVariables) where
-
-import Language.Boogie.AST
-import Language.Boogie.Util
-import Language.Boogie.Position hiding (gen)
-import Language.Boogie.BasicBlocks
-import Data.List
-import Data.Map (Map, (!))
-import qualified Data.Map as M
-import Data.Set (Set)
-import qualified Data.Set as S
-
-{- Interface -}
-
--- | 'liveInputVariables' @sig def@ : 
--- Input parameters (in the order they appear in @sig@) and global names, 
--- whose initial value might be read by the procedure implementation @def@
-liveInputVariables :: PSig -> PDef -> ([Id], [Id])
-liveInputVariables sig def = let
-  body = pdefBody def
-  liveVars = liveVariables (attachContractChecks sig def)
-  liveLocals = filter (`elem` liveVars) (map itwId (fst body))
-  liveIns = filter (`elem` liveVars) (pdefIns def)
-  liveOuts = filter (`elem` liveVars) (pdefOuts def)
-  liveGlobals = liveVars \\ (liveLocals ++ liveIns ++ liveOuts)
-  in (liveIns, liveGlobals)
-  
--- | Identifiers whose initial value might be read in body
-liveVariables :: Map Id [Statement] -> [Id]
-liveVariables body = let
-    empty = M.map (const S.empty) body
-    insertExitBlock i = M.insert i (transition (body ! i) S.empty)
-    entry0 = S.foldr insertExitBlock empty (exitBlocks body)
-    changed0 = M.keysSet body <-> exitBlocks body
-    oldVariables = S.unions (map (\block -> S.unions (map genOld block)) (M.elems body))
-  in S.toList (oldVariables `S.union` (analyse body entry0 empty changed0 ! startLabel))
-
-{- Implementation -}
-
--- | Analyse live variable in body, 
--- starting from live variables at the entry to each block entry,
--- live variables at the exit of each block exit,
--- and the set of blocks whose exit set might have changed changed.
-analyse :: Map Id [Statement] -> Map Id (Set Id) -> Map Id (Set Id) -> Set Id -> Map Id (Set Id)
-analyse body entry exit changed = if S.null changed
-  then entry
-  else let 
-      (i, changed') = S.deleteFindMax changed
-      newExit = setUnions $ S.map (entry !) (successors body i)
-      newEntry = transition (body ! i) newExit
-      exit' = M.insert i newExit exit
-      entry' = M.insert i newEntry entry
-      changed'' = if entry ! i == newEntry then changed' else changed' <+> predecessors body i
-    in analyse body entry' exit' changed''
-
-(<+>) = (S.union)
-(<->) = (S.\\)
--- | Union of a set of sets
-setUnions sets = S.foldl S.union S.empty sets
-
--- | Variables that are live before a sequence of statements sts,
--- if the final live variables are exit
-transition :: [Statement] -> Set Id -> Set Id
-transition sts exit = foldr transition1 exit sts
-  where
-    transition1 st exit = exit <-> kill st <+> gen st
-
--- | Variables that are not live anymore as a result of st    
-kill :: Statement -> Set Id
-kill st = case node st of
-  Havoc ids     -> S.fromList ids
-  Assign lhss _ -> S.fromList (map fst lhss)
-  Call lhss _ _ -> S.fromList lhss
-  otherwise -> S.empty
-
--- | Variables that become live as a result of st
-gen :: Statement -> Set Id
-gen st = genTwoState fst st
-
--- | Variables whose pre-state is mentioned in st
-genOld :: Statement -> Set Id
-genOld st = genTwoState snd st
-  
--- | Variables mentioned in st in either current state or old state
-genTwoState :: (([Id], [Id]) -> [Id]) -> Statement -> Set Id
-genTwoState select st = case node st of
-  Predicate (SpecClause _ _ e) -> (S.fromList . select . freeVarsTwoState) e
-  Assign lhss rhss -> let 
-    allSubscipts = concat $ concatMap snd lhss
-    subsciptedLhss = [fst lhs | lhs <- lhss, not (null (snd lhs))] -- Left-hand sides with a subscript are also read (consider desugaring)
-    in S.unions (map (S.fromList . select . freeVarsTwoState) (rhss ++ allSubscipts)) <+> S.fromList subsciptedLhss
-  Call _ _ args -> S.unions (map (S.fromList . select . freeVarsTwoState) args)
-  CallForall _ args -> S.unions (map (S.fromList . select . freeVarsTwoState') args)
-  otherwise -> S.empty
-  where 
-    freeVarsTwoState' Wildcard = ([], [])
-    freeVarsTwoState' (Expr e) = freeVarsTwoState e
-    
--- | Blocks in body that end with a return statement
-exitBlocks :: Map Id [Statement] -> Set Id
-exitBlocks body = M.keysSet $ M.filter isExit body
-  where
-    isExit block = case node (last block) of
-      Return -> True
-      _ -> False
-      
--- | Blocks in body that have an outgoing edge to label
-predecessors :: Map Id [Statement] -> Id -> Set Id
-predecessors body label = M.keysSet $ M.filter (goesTo label) body
-  where
-    goesTo label block = case node (last block) of
-      Goto lbs -> label `elem` lbs
-      _ -> False
-      
--- | Blocks in body that have an incoming edge from label  
-successors :: Map Id [Statement] -> Id -> Set Id
-successors body label = case node (last (body ! label)) of
-  Goto lbs -> S.fromList lbs
-  _ -> S.empty
-  
--- | Body of the implementation def of procedure sig with pre- and postcondition checks embedded;
--- (used to extract live variables from contracts)
-attachContractChecks :: PSig -> PDef -> Map Id [Statement]
-attachContractChecks sig def = let
-  preChecks = map (attachPos (pdefPos def) . Predicate . subst sig) (psigRequires sig)
-  postChecks = map (attachPos (pdefPos def) . Predicate . subst sig) (psigEnsures sig)
-  subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
-  attachPreChecks = M.adjust (preChecks ++) startLabel (snd (pdefBody def))
-  attachPostChecks block = let jump = last block
-    in case node jump of
-      Return -> init block ++ postChecks ++ [jump]
-      _ -> block
-  in M.map attachPostChecks attachPreChecks  
-      

@@ -0,0 +1,328 @@+{-# LANGUAGE TemplateHaskell, Rank2Types #-}
+
+-- | Execution state for the interpreter
+module Language.Boogie.Environment ( 
+  MapRepr (..),
+  emptyMap,
+  stored,
+  Value (..),
+  valueFromInteger,
+  vnot,
+  unValueBool,
+  unValueMap,
+  flattenMap,
+  mapSource,
+  mapValues,
+  refIdTypeName,
+  ucTypeName,
+  deepDeref,
+  objectEq,
+  mustAgree,
+  mustDisagree,
+  valueDoc,
+  Store,
+  emptyStore,
+  functionConst,
+  userStore,
+  storeDoc,
+  Memory,
+  StoreLens,
+  memLocals,
+  memGlobals,
+  memOld,
+  memConstants,
+  memHeap,
+  emptyMemory,
+  visibleVariables,
+  memoryDoc,
+  AbstractMemory,
+  amLocals,
+  amGlobals,
+  amHeap,
+  Environment,
+  envMemory,
+  envProcedures,
+  envConstraints,
+  envTypeContext,
+  envGenerator,
+  envCustomCount,
+  envQBound,
+  envInOld,
+  initEnv,
+  lookupProcedure,
+  lookupNameConstraints,
+  lookupMapConstraints,
+  lookupCustomCount,
+  addProcedureImpl,
+  addGlobalDefinition,
+  addMapDefinition,
+  addMapConstraint,
+  setCustomCount,
+  withHeap,
+) where
+
+import Language.Boogie.Util
+import Language.Boogie.Position
+import Language.Boogie.Tokens (nonIdChar)
+import Language.Boogie.AST
+import Language.Boogie.Heap
+import Language.Boogie.Generator
+import Language.Boogie.TypeChecker (Context)
+import Language.Boogie.PrettyPrinter
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
+import Control.Lens hiding (Context, at)
+import Text.PrettyPrint
+
+{- Values -}
+
+-- | Representation of a map value
+data MapRepr = 
+  Source (Map [Value] Value) |    -- ^ Map that comes directly from a non-deterministic choice, possibly with some key-value pairs defined
+  Derived Ref (Map [Value] Value) -- ^ Map that is derived from another map by redefining values at some keys
+  deriving (Eq, Ord)
+  
+-- | Representation of an empty map  
+emptyMap = Source M.empty
+
+-- | Key-value pairs stored explicitly in a map representation
+stored :: MapRepr -> Map [Value] Value
+stored (Source vals) = vals
+stored (Derived _ override) = override
+  
+-- | Pretty-printed map representation  
+mapReprDoc :: MapRepr -> Doc
+mapReprDoc repr = case repr of
+  Source vals -> brackets (commaSep (map itemDoc (M.toList vals)))
+  Derived base override -> refDoc base <> 
+    brackets (commaSep (map itemDoc (M.toList override))) 
+  where
+    keysDoc keys = ((if length keys > 1 then parens else id) . commaSep . map valueDoc) keys
+    itemDoc (keys, v) = keysDoc keys  <+> text "->" <+> valueDoc v
+
+-- | Run-time value
+data Value = IntValue Integer |  -- ^ Integer value
+  BoolValue Bool |               -- ^ Boolean value
+  CustomValue Id Int |           -- ^ Value of a user-defined type
+  MapValue MapRepr |             -- ^ Value of a map type: consists of an optional reference to the base map (if derived from base by updating) and key-value pairs that override base
+  Reference Ref                  -- ^ Reference to a map stored in the heap
+  deriving (Eq, Ord)
+  
+-- | 'valueFromInteger' @t n@: value of type @t@ with an integer code @n@
+valueFromInteger :: Type -> Integer -> Value  
+valueFromInteger IntType n        = IntValue n
+valueFromInteger (IdType id _) n  = CustomValue id (fromInteger n)
+valueFromInteger _ _              = error "cannot create a boolean or map value from integer" 
+  
+unValueBool (BoolValue b) = b  
+vnot (BoolValue b) = BoolValue (not b)
+
+unValueMap (MapValue repr) = repr
+
+-- | Pretty-printed value
+valueDoc :: Value -> Doc
+valueDoc (IntValue n) = integer n
+valueDoc (BoolValue False) = text "false"
+valueDoc (BoolValue True) = text "true"
+valueDoc (MapValue repr) = mapReprDoc repr
+valueDoc (CustomValue t n) = text t <+> int n
+valueDoc (Reference r) = refDoc r
+
+instance Show Value where
+  show v = show (valueDoc v)
+  
+{- Map operations -}
+
+-- | Source reference and key-value pairs of a reference in a heap
+flattenMap :: Heap Value -> Ref -> (Ref, (Map [Value] Value))
+flattenMap h r = case unValueMap $ h `at` r of
+  Source vals -> (r, vals)
+  Derived base override -> let (s, v) = flattenMap h base
+    in (s, override `M.union` v)
+    
+-- | First component of 'flattenMap'
+mapSource h r = flattenMap h r ^. _1
+
+-- | Second component of 'flattenMap'
+mapValues h r = flattenMap h r ^. _2
+
+-- | Dummy user-defined type used to differentiate map values
+refIdTypeName = nonIdChar : "RefId"
+
+-- | Dummy user-defined type used to mark entities whose definitions are currently being evaluated
+ucTypeName = nonIdChar : "UC"
+
+-- | 'deepDeref' @h v@: Completely dereference value @v@ given heap @h@ (so that no references are left in @v@)
+deepDeref :: Heap Value -> Value -> Value
+deepDeref h v = deepDeref' v
+  where
+    deepDeref' (Reference r) = let vals = mapValues h r
+      in MapValue . Source $ (M.map deepDeref' . M.mapKeys (map deepDeref') . M.filter (not . isAux)) vals -- Here we do not assume that keys contain no references, as this is used for error reporting
+    deepDeref' (MapValue _) = internalError "Attempt to dereference a map directly"
+    deepDeref' v = v
+    isAux (CustomValue id _) | id == refIdTypeName = True
+    isAux _ = False
+
+-- | 'objectEq' @h v1 v2@: is @v1@ equal to @v2@ in the Boogie semantics? Nothing if cannot be determined.
+objectEq :: Heap Value -> Value -> Value -> Maybe Bool
+objectEq h (Reference r1) (Reference r2) = if r1 == r2
+  then Just True -- Equal references point to equal maps
+  else let 
+    (s1, vals1) = flattenMap h r1
+    (s2, vals2) = flattenMap h r2
+    in if mustDisagree h vals1 vals2
+      then Just False
+      else if s1 == s2 && mustAgree h vals1 vals2
+        then Just True
+        else Nothing
+objectEq _ (MapValue _) (MapValue _) = internalError "Attempt to compare two maps"
+objectEq _ v1 v2 = Just $ v1 == v2
+
+mustEq h v1 v2 = case objectEq h v1 v2 of
+  Just True -> True
+  _ -> False  
+mustNeq h v1 v2 = case objectEq h v1 v2 of
+  Just False -> True
+  _ -> False  
+mayEq h v1 v2 = not $ mustNeq h v1 v2
+mayNeq h v1 v2 = not $ mustEq h v1 v2
+
+mustDisagree h vals1 vals2 = M.foldl (||) False $ (M.intersectionWith (mustNeq h) vals1 vals2)
+
+mustAgree h vals1 vals2 = let common = M.intersectionWith (mustEq h) vals1 vals2 in
+      M.size vals1 == M.size common && M.size vals2 == M.size common && M.foldl (&&) True common
+  
+{- Store -}  
+
+-- | Store: stores variable values at runtime 
+type Store = Map Id Value
+
+-- | A store with no variables
+emptyStore :: Store
+emptyStore = M.empty
+
+-- | Pretty-printed store
+storeDoc :: Store -> Doc
+storeDoc vars = vsep $ map varDoc (M.toList vars)
+  where varDoc (id, val) = text id <+> text "=" <+> valueDoc val
+  
+-- | 'userStore' @heap store@ : @store@ with all reference values completely dereferenced given @heap@, and all auxiliary values removed
+userStore :: Heap Value -> Store -> Store
+userStore heap store = M.map (deepDeref heap) store
+
+-- | 'functionConst' @name@ : name of a map constant that corresponds function @name@
+-- (must be distinct from all global names)
+functionConst name = "function " ++ name
+
+{- Memory -}
+
+-- | Memory: stores concrete values associated with names and references
+data Memory = Memory {
+  _memLocals :: Store,      -- ^ Local variable store
+  _memGlobals :: Store,     -- ^ Global variable store
+  _memOld :: Store,         -- ^ Old global variable store (in two-state contexts)
+  _memConstants :: Store,   -- ^ Constant and function cache
+  _memHeap :: Heap Value    -- ^ Heap
+} deriving Eq
+
+makeLenses ''Memory
+
+-- | Lens that selects a store from memory
+type StoreLens = SimpleLens Memory Store
+
+-- | Empty memory
+emptyMemory = Memory {
+  _memLocals = emptyStore,
+  _memGlobals = emptyStore,
+  _memOld = emptyStore,
+  _memConstants = emptyStore,
+  _memHeap = emptyHeap
+}
+
+-- | Visible values of all identifiers in a memory (locals shadow globals) 
+visibleVariables :: Memory -> Store
+visibleVariables mem = (mem^.memLocals) `M.union` (mem^.memGlobals) `M.union` (mem^.memConstants)
+
+-- | 'memoryDoc' @debug mem@ : either user or debug representation of @mem@, depending on @debug@
+memoryDoc :: Bool -> Memory -> Doc
+memoryDoc debug mem = vsep $ [text "Locals:" <+> storeDoc (storeRepr $ mem^.memLocals),
+  text "Globals:" <+> storeDoc (storeRepr $ (mem^.memGlobals) `M.union` (mem^.memConstants)),
+  text "Old values:" <+> storeDoc (storeRepr $ mem^.memOld)]
+  ++ if debug then [text "Heap:" <+> heapDoc (mem^.memHeap)] else []
+  where
+    storeRepr store = if debug then store else userStore (mem^.memHeap) store
+    
+instance Show Memory where
+  show mem = show $ memoryDoc True mem
+  
+{- Abstract memory -}
+
+-- | Abstract memory: stores constraints associated with names and references
+data AbstractMemory = AbstractMemory {
+  _amLocals :: AbstractStore,       -- ^ Local name constraints
+  _amGlobals :: AbstractStore,      -- ^ Global name constraints
+  _amHeap :: Map Ref ConstraintSet  -- ^ Reference constraints
+}
+
+makeLenses ''AbstractMemory
+
+-- | Empty abstract memory
+emptyAbstractMemory = AbstractMemory {
+  _amLocals = M.empty,
+  _amGlobals = M.empty,
+  _amHeap = M.empty
+}
+
+{- Environment -}
+  
+-- | Execution state
+data Environment m = Environment
+  {
+    _envMemory :: Memory,                   -- ^ Concrete values
+    _envConstraints :: AbstractMemory,      -- ^ Abstract values
+    _envProcedures :: Map Id [PDef],        -- ^ Procedure implementations
+    _envTypeContext :: Context,             -- ^ Type context
+    _envGenerator :: Generator m,           -- ^ Input generator (used for non-deterministic choices)
+    _envCustomCount :: Map Id Int,          -- ^ For each user-defined type, number of distinct values of this type already generated
+    _envQBound :: Maybe Integer,            -- ^ Maximum number of values to try for a quantified variable (unbounded if Nothing)
+    _envInOld :: Bool                       -- ^ Is an old expression currently being evaluated?
+  }
+  
+makeLenses ''Environment
+   
+-- | 'initEnv' @tc gen@: Initial environment in a type context @tc@ with a value generator @gen@  
+initEnv tc gen qbound = Environment
+  {
+    _envMemory = emptyMemory,
+    _envConstraints = emptyAbstractMemory,
+    _envProcedures = M.empty,
+    _envTypeContext = tc,
+    _envGenerator = gen,
+    _envCustomCount = M.empty,
+    _envQBound = qbound,
+    _envInOld = False
+  }
+  
+combineGetters f g1 g2 = to $ \env -> (env ^. g1) `f` (env ^. g2)
+  
+-- | 'lookupGetter' @getter def key env@ : lookup @key@ in a map accessible with @getter@ from @env@; if it does not occur return @def@
+lookupGetter getter def key env = case M.lookup key (env ^. getter) of
+  Nothing -> def
+  Just val -> val
+  
+-- Environment queries  
+lookupProcedure = lookupGetter envProcedures []  
+lookupNameConstraints = lookupGetter (combineGetters M.union (envConstraints.amLocals) (envConstraints.amGlobals)) ([], [])
+lookupMapConstraints = lookupGetter (envConstraints.amHeap) ([], [])
+lookupCustomCount = lookupGetter envCustomCount 0
+
+-- Environment modifications  
+addProcedureImpl name def env = over envProcedures (M.insert name (lookupProcedure name env ++ [def])) env
+addGlobalDefinition name def env = over (envConstraints.amGlobals) (M.insert name (over _1 (++ [def]) (lookupGetter (envConstraints.amGlobals) ([], []) name env))) env
+addMapDefinition r def env = over (envConstraints.amHeap) (M.insert r (over _1 (++ [def]) (lookupMapConstraints r env))) env
+addMapConstraint r constraint env = over (envConstraints.amHeap) (M.insert r (over _2 (++ [constraint]) (lookupMapConstraints r env))) env
+setCustomCount t n = over envCustomCount (M.insert t n)
+withHeap f env = let (res, h') = f (env^.envMemory.memHeap) 
+  in (res, set (envMemory.memHeap) h' env )  

@@ -0,0 +1,66 @@+-- | This monad transformer adds the ability to accumulate errors from several ErrorT computations
+-- and report them all at once.
+module Language.Boogie.ErrorAccum where
+
+import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.Trans.Error
+
+-- | Error accumulator: 
+-- used in combination with ErrorT to store intermediate computation results, 
+-- when errors should be accumulated rather than reported immediately  
+newtype ErrorAccumT e m a = ErrorAccumT { runErrorAccumT :: m ([e], a) }
+
+instance (ErrorList e, Monad m) => Monad (ErrorAccumT e m) where
+  -- | Attach an empty list of errors to a succesful computation
+  return x  = ErrorAccumT $ return ([], x)
+  -- | The bind strategy is to concatenate error lists
+  m >>= k   = ErrorAccumT $ do
+    (errs, res) <- runErrorAccumT m
+    (errs', res') <- runErrorAccumT $ k res
+    return (errs ++ errs', res')
+    
+instance ErrorList e => MonadTrans (ErrorAccumT e) where
+  lift m = ErrorAccumT $ do
+    a <- m
+    return ([], a)  
+    
+-- | Transform an error computation and default value into an error accumlator
+accum :: (ErrorList e, Monad m) => ErrorT [e] m a -> a -> ErrorAccumT e m a
+accum c def = ErrorAccumT (errToAccum def `liftM` runErrorT c)
+  where
+    errToAccum def (Left errs)  = (errs, def)
+    errToAccum def (Right x)    = ([], x)
+        
+-- | Transform an error accumlator back into a regular error computation  
+report :: (ErrorList e, Monad m) => ErrorAccumT e m a -> ErrorT [e] m a
+report accum = ErrorT (accumToErr `liftM` runErrorAccumT accum)
+  where
+    accumToErr ([], x) = Right x
+    accumToErr (es, _) = Left es  
+
+-- | 'mapAccum' @f def xs@ :
+-- Apply @f@ to all @xs@, accumulating errors and reporting them at the end
+mapAccum :: (ErrorList e, Monad m) => (a -> ErrorT [e] m b) -> b -> [a] -> ErrorT [e] m [b]
+mapAccum f def xs = report $ mapM (acc f) xs  
+  where
+    acc f x  = accum (f x) def
+   
+-- | 'mapAccumA_' @f xs@ :
+-- Apply @f@ to all @xs@ throwing away the result, accumulating errors
+mapAccumA_ :: (ErrorList e, Monad m) => (a -> ErrorT [e] m ()) -> [a] -> ErrorAccumT e m ()
+mapAccumA_ f xs = mapM_ (acc f) xs  
+  where
+    acc f x  = accum (f x) ()
+    
+-- | Same as 'mapAccumA_', but reporting errors at the end
+mapAccum_ :: (ErrorList e, Monad m) => (a -> ErrorT [e] m ()) -> [a] -> ErrorT [e] m ()
+mapAccum_ f xs = report $ mapAccumA_ f xs  
+
+-- | 'zipWithAccum_' @f xs ys@ :
+-- Apply type checking @f@ to all @xs@ and @ys@ throwing away the result,
+-- accumulating errors and reporting them at the end
+zipWithAccum_ :: (ErrorList e, Monad m) => (a -> b -> ErrorT [e] m ()) -> [a] -> [b] -> ErrorT [e] m ()
+zipWithAccum_ f xs ys = report $ zipWithM_ (acc f) xs ys  
+  where
+    acc f x y  = accum (f x y) ()

@@ -0,0 +1,61 @@+-- | Deterministic and non-deterministic input generators
+module Language.Boogie.Generator where
+
+import Control.Monad.Identity hiding (join)
+import Control.Monad.Stream
+import System.Random
+
+-- | Input generator
+data Generator m = Generator {
+  genBool :: m Bool,        -- Generate a boolean
+  genInteger :: m Integer,  -- Generate an arbitrary precision integer
+  genIndex :: Int -> m Int  -- Generate a natural smaller than a given bound
+  }
+  
+-- | Always generates the same default value
+defaultGenerator :: Generator Identity  
+defaultGenerator = Generator {
+  genBool = Identity False,
+  genInteger = Identity 0,
+  genIndex = Identity . const 0
+}
+
+-- | Generates all possible values once, in a predefined order
+exhaustiveGenerator :: Maybe Integer -> Generator Stream
+exhaustiveGenerator mBound = Generator {
+  genBool = return False `mplus` return True,
+  genInteger = case mBound of
+    Nothing -> allIntegers
+    Just b -> fromInterval $ intInterval b,
+  genIndex = \n -> fromInterval $ case mBound of
+    Nothing -> natInterval n
+    Just b -> natInterval $ fromInteger (b `min` toInteger n)
+}
+  where
+    allIntegers = fromList [0, -1..] `mplus` fromList [1..]
+    fromInterval (a, b)
+      | b < a = mzero
+      | a >= 0 || b <= 0 = fromList [a..b]
+      | otherwise = fromList [0, -1..a] `mplus` fromList [1..b]
+
+-- | Generated values randomly; the same value can be generated multiple times
+randomGenerator :: StdGen -> Maybe Integer -> Generator Stream
+randomGenerator rGen mBound = Generator {
+  genBool = fromList $ randoms rGen,
+  genInteger = fromList $ case mBound of
+    Nothing -> randoms rGen
+    Just b -> randomRs (intInterval b) rGen,
+  genIndex = \n -> fromList $ case mBound of
+    Nothing -> randomRs (natInterval n) rGen
+    Just b -> randomRs (natInterval $ fromInteger (b `min` toInteger n)) rGen
+}
+
+-- | 'intInterval' @n@: interval centered around 0 of size n
+intInterval n = let n2 = n `div` 2 in (-n2, n - n2 - 1)
+
+-- | 'natInterval' @n@: interval starting from 0 of size n
+natInterval n = (0, n - 1)
+
+-- | Convert a (possibly infinite) nonempty list into a stream      
+fromList :: [a] -> Stream a
+fromList xs = foldr1 mplus (map return xs)

@@ -0,0 +1,120 @@+{-# LANGUAGE TemplateHaskell #-}
+
+-- | Generic heap with reference counting.
+-- This module provides relatively low-level interface to the heap data structure, while keeping its internal representation hidden and consistent.
+module Language.Boogie.Heap (
+  Ref,
+  refDoc,
+  Heap,
+  emptyHeap,
+  at,
+  alloc,
+  hasGarbage,
+  dealloc,
+  update,
+  incRefCount,
+  decRefCount,
+  heapDoc
+) where
+
+import Language.Boogie.AST
+import Language.Boogie.PrettyPrinter
+import Language.Boogie.Util
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
+import Text.PrettyPrint
+import Control.Lens hiding (Context, at)
+
+-- | Reference (index in the heap)
+type Ref = Int
+
+-- | Pretty-printed reference
+refDoc :: Ref -> Doc
+refDoc r = text ("ref_" ++ show r)
+
+-- | Heap
+data Heap a = Heap {
+    _hValCounts :: Map Ref (a, Int),   -- ^ Mapping of references of values and reference counts
+    _hGarbage :: Set Ref,              -- ^ Set of unused references (exactly those references for which snd hValCounts = 0, stored for efficiency)
+    _hFree :: Set Ref,                 -- ^ Set of references that have been removed from the heap and are ready to be reused (stored for efficiency)
+    _hFresh :: Ref                     -- ^ Smallest reference that has never been used
+  } deriving Eq
+  
+makeLenses ''Heap  
+
+{- Initialization -}
+
+-- | Empty heap
+emptyHeap = Heap {
+  _hValCounts = M.empty,
+  _hGarbage = S.empty,
+  _hFree = S.empty,
+  _hFresh = 0
+}
+
+{- Access -}
+
+-- | 'at' @h r@: value of @r@ in heap @h@
+at :: Show a => Heap a -> Ref -> a
+at h r = case M.lookup r (h^.hValCounts) of
+  Nothing -> internalError . show $ text "Cannot find reference" <+> refDoc r <+> text "in heap" $+$ heapDoc h
+  Just (v, c) -> v
+  
+-- | Does the heap have any garbage?
+hasGarbage :: Heap a -> Bool
+hasGarbage h = h ^. hGarbage . to S.null . to not
+
+{- Modification -}  
+  
+-- | 'alloc' @v h@ : choose a free reference in heap @h@ and store value @v@ in there; return the reference and the updated heap
+alloc :: a -> Heap a -> (Ref, Heap a)
+alloc v h = let (r, h') = getFreshRef h in (r, insert r v h')
+  where
+    getFreshRef h = if h ^. hFree . to S.null
+      then let r = h^.hFresh in (r, h & hFresh .~ r + 1)
+      else let (r, f') = S.deleteFindMin (h^.hFree) in (r, h & hFree .~ f')
+    insert r v h = h & (over hValCounts (M.insert r (v, 0))) . (over hGarbage (S.insert r))
+
+-- | Collect some garbage reference in the heap and return that reference and the new heap;
+-- the heap must have garbage
+dealloc :: Heap a -> (Ref, Heap a)
+dealloc h = let (r, g') = S.deleteFindMin (h^.hGarbage) in (r, 
+  h & (over hValCounts (M.delete r)) .
+      (hGarbage .~ g') .
+      (over hFree (S.insert r)) 
+  )
+    
+-- | 'update' @r v h@ : set the value at reference @r@ to @v@ in @h@;
+-- @r@ must be present in @h@
+update :: Ref -> a -> Heap a -> Heap a
+update r v = over hValCounts (M.adjust (over _1 (const v)) r)
+
+-- | 'incRefCount' @r h@ : increase reference count of @r@ in @h@;
+-- @r@ must be present in @h@
+incRefCount :: Ref -> Heap a -> Heap a
+incRefCount r h = let (v, c) = (h^.hValCounts) ! r
+  in h & (over hValCounts (M.insert r (v, c + 1))) .
+         (over hGarbage (if c == 0 then S.delete r else id)
+     )
+
+-- | 'decRefCount' @r h@ : decrease reference count of @r@ in @h@;
+-- @r@ must be present in @h@          
+decRefCount :: Ref -> Heap a -> Heap a
+decRefCount r h = let (v, c) = (h^.hValCounts) ! r
+  in h & (over hValCounts (M.insert r (v, c - 1))) .
+         (over hGarbage (if c == 1 then S.insert r else id))
+          
+{- Ouput -}          
+
+-- | Pretty-printed heap
+heapDoc :: Show a => Heap a -> Doc
+heapDoc h = (vsep $ map entryDoc (M.toList (h^.hValCounts))) $+$
+  text "Garbage" <+> braces (commaSep (map refDoc (S.toList (h^.hGarbage)))) $+$
+  text "Free" <+> braces (commaSep (map refDoc (S.toList (h^.hFree))))
+  where entryDoc (ref, (val, count)) = refDoc ref <> braces (int count) <+> text "->" <+> text (show val)
+  
+instance Show a => Show (Heap a) where
+  show h = show $ heapDoc h
+  

@@ -1,846 +1,1308 @@-{-# LANGUAGE FlexibleContexts #-}
-
--- | Interpreter for Boogie 2
-module Language.Boogie.Interpreter (
-  -- * Executing programs
-  executeProgram,
-  -- * State
-  Value (..),
-  Environment (..),
-  emptyEnv,
-  lookupFunction,
-  lookupProcedure,
-  modifyTypeContext,
-  setV,
-  setAll,
-  -- * Executions
-  Execution,
-  SafeExecution,
-  execSafely,
-  execUnsafely,
-  -- * Run-time failures
-  FailureSource (..),
-  InternalCode,
-  StackFrame (..),
-  StackTrace,
-  RuntimeFailure (..),  
-  FailureKind (..),
-  failureKind,
-  -- * Executing parts of programs
-  eval,
-  exec,
-  execProcedure,
-  collectDefinitions,
-  -- * Pretty-printing
-  valueDoc,
-  varsDoc,
-  functionsDoc,
-  runtimeFailureDoc
-  ) where
-
-import Language.Boogie.AST
-import Language.Boogie.Util
-import Language.Boogie.Intervals
-import Language.Boogie.Position
-import Language.Boogie.Tokens (nonIdChar)
-import Language.Boogie.PrettyPrinter
-import Language.Boogie.TypeChecker
-import Language.Boogie.NormalForm
-import Language.Boogie.BasicBlocks
-import Data.List
-import Data.Map (Map, (!))
-import qualified Data.Map as M
-import Control.Monad.Error hiding (join)
-import Control.Applicative hiding (empty)
-import Control.Monad.State hiding (join)
-import Text.PrettyPrint
-
-{- Interface -}
-
--- | 'executeProgram' @p tc entryPoint@ :
--- Execute program @p@ in type context @tc@ starting from procedure @entryPoint@, 
--- and return the final environment;
--- requires that @entryPoint@ have no in- or out-parameters
-executeProgram :: Program -> Context -> Id -> Either RuntimeFailure Environment
-executeProgram p tc entryPoint = finalEnvironment
-  where
-    initEnvironment = emptyEnv { envTypeContext = tc }
-    finalEnvironment = case runState (runErrorT programExecution) initEnvironment of
-      (Left err, _) -> Left err
-      (_, env)      -> Right env            
-    programExecution = do
-      execUnsafely $ collectDefinitions p
-      execCall [] entryPoint [] noPos
-              
-{- State -}
-
--- | Run-time value
-data Value = IntValue Integer |   -- ^ Integer value
-  BoolValue Bool |                -- ^ Boolean value
-  MapValue (Map [Value] Value) |  -- ^ Value of a map type
-  CustomValue Integer             -- ^ Value of a user-defined type (values with the same code are considered equal)
-  deriving (Eq, Ord)
-      
--- | Default value of a type (used to initialize variables)  
-defaultValue :: Type -> Value
-defaultValue BoolType         = BoolValue False  
-defaultValue IntType          = IntValue 0
-defaultValue (MapType _ _ _)  = MapValue M.empty
-defaultValue (Instance _ _)   = CustomValue 0
-
--- | Pretty-printed value
-valueDoc :: Value -> Doc
-valueDoc (IntValue n) = integer n
-valueDoc (BoolValue False) = text "false"
-valueDoc (BoolValue True) = text "true"
-valueDoc (MapValue m) = brackets (commaSep (map itemDoc (M.toList m)))
-  where itemDoc (keys, v) = commaSep (map valueDoc keys) <+> text "->" <+>  valueDoc v
-valueDoc (CustomValue n) = text "custom_" <> integer n
-
-instance Show Value where
-  show v = show (valueDoc v)
-
--- | Execution state
-data Environment = Environment
-  {
-    envLocals :: Map Id Value,          -- ^ Local variable names to values
-    envGlobals :: Map Id Value,         -- ^ Global variable names to values
-    envOld :: Map Id Value,             -- ^ Global variable names to old values (in two-state contexts)
-    envConstants :: Map Id Expression,  -- ^ Constant names to expressions
-    envFunctions :: Map Id [FDef],      -- ^ Function names to definitions
-    envProcedures :: Map Id [PDef],     -- ^ Procedure names to definitions
-    envTypeContext :: Context           -- ^ Type context
-  }
-   
--- | Empty environment   
-emptyEnv = Environment
-  {
-    envLocals = M.empty,
-    envGlobals = M.empty,
-    envOld = M.empty,
-    envConstants = M.empty,
-    envFunctions = M.empty,
-    envProcedures = M.empty,
-    envTypeContext = emptyContext
-  }
-  
--- | 'lookupFunction' @id env@ : All definitions of function @id@ in @env@
-lookupFunction id env = case M.lookup id (envFunctions env) of
-  Nothing -> []
-  Just defs -> defs    
-  
--- | 'lookupProcedure' @id env@ : All definitions of procedure @id@ in @env@  
-lookupProcedure id env = case M.lookup id (envProcedures env) of
-  Nothing -> []
-  Just defs -> defs  
-
-setGlobal id val env = env { envGlobals = M.insert id val (envGlobals env) }    
-setLocal id val env = env { envLocals = M.insert id val (envLocals env) }
-addConstantDef id def env = env { envConstants = M.insert id def (envConstants env) }
-addFunctionDefs id defs env = env { envFunctions = M.insert id (lookupFunction id env ++ defs) (envFunctions env) }
-addProcedureDef id def env = env { envProcedures = M.insert id (def : (lookupProcedure id env)) (envProcedures env) } 
-modifyTypeContext f env = env { envTypeContext = f (envTypeContext env) }
-
--- | Pretty-printed mapping of variables to values
-varsDoc :: Map Id Value -> Doc
-varsDoc vars = vsep $ map varDoc (M.toList vars)
-  where varDoc (id, val) = text id <+> text "=" <+> valueDoc val
-  
--- | Pretty-printed set of function definitions
-functionsDoc :: Map Id [FDef] -> Doc  
-functionsDoc funcs = vsep $ map funcDoc (M.toList funcs)
-  where 
-    funcDoc (id, defs) = vsep $ map (funcsDefDoc id) defs
-    funcsDefDoc id (FDef formals guard body) = exprDoc guard <+> text "->" <+> 
-      text id <> parens (commaSep (map text formals)) <+> text "=" <+> exprDoc body
-      
-{- Executions -}
-
--- | Computations with 'Environment' as state, which can result in either @a@ or 'RuntimeFailure'
-type Execution a = ErrorT RuntimeFailure (State Environment) a
-
--- | Computations with 'Environment' as state, which always result in @a@
-type SafeExecution a = State Environment a
-
--- | 'execUnsafely' @computation@ : Execute a safe @computation@ in an unsafe environment
-execUnsafely :: SafeExecution a -> Execution a
-execUnsafely computation = ErrorT (Right <$> computation)
-
--- | 'execSafely' @computation handler@ : Execute an unsafe @computation@ in a safe environment, handling errors that occur in @computation@ with @handler@
-execSafely :: Execution a -> (RuntimeFailure -> SafeExecution a) -> SafeExecution a
-execSafely computation handler = do
-  eres <- runErrorT computation
-  either handler return eres
-  
--- | Computations that perform a cleanup at the end
-class Monad m => Finalizer m where
-  finally :: m a -> m () -> m a
-    
-instance (Monad m) => Finalizer (StateT s m) where
-  finally main cleanup = do
-    res <- main
-    cleanup
-    return res
-
-instance (Error e, Monad m) => Finalizer (ErrorT e m) where
-  finally main cleanup = do
-    res <- main `catchError` (\err -> cleanup >> throwError err)
-    cleanup
-    return res  
-          
--- | 'setV' @id val@ : set value of variable @id@ to @val@;
--- @id@ has to be declared in the current type context
-setV id val = do
-  tc <- gets envTypeContext
-  if M.member id (localScope tc)
-    then modify $ setLocal id val
-    else modify $ setGlobal id val      
-    
--- | 'setAll' @ids vals@ : set values of variables @ids@ to @vals@;
--- all @ids@ have to be declared in the current type context
-setAll ids vals = zipWithM_ setV ids vals
-
--- | Run execution in the old environment
-old :: Execution a -> Execution a
-old execution = do
-  env <- get
-  put env { envGlobals = envOld env }
-  res <- execution
-  put env
-  return res
-
--- | Save current values of global variables in the "old" environment, return the previous "old" environment
-saveOld :: Execution (Map Id Value)  
-saveOld = do
-  env <- get
-  put env { envOld = envGlobals env }
-  return $ envOld env
-
--- | Set the "old" environment to olds  
-restoreOld :: Map Id Value -> Execution ()  
-restoreOld olds = do
-  env <- get
-  put env { envOld = olds }
-  
--- | Enter local scope (apply localTC to the type context and assign actuals to formals),
--- execute computation,
--- then restore type context and local variables to their initial values
-executeLocally :: (MonadState Environment m, Finalizer m) => (Context -> Context) -> [Id] -> [Value] -> m a -> m a
-executeLocally localTC formals actuals computation = do
-  oldEnv <- get
-  modify $ modifyTypeContext localTC
-  setAll formals actuals
-  computation `finally` unwind oldEnv
-  where
-    -- | Restore type context and the values of local variables 
-    unwind oldEnv = do
-      env <- get
-      put env { envTypeContext = envTypeContext oldEnv, envLocals = envLocals oldEnv }
-              
-{- Nondeterminism -}  
-  
--- | Generate a value of type t,
--- such that when it is set, guard does not fail.
--- Fail if cannot find such a value.
--- (So far just returns the default value, but will be more elaborate in the future)
-generateValue :: Type -> (Value -> Execution ()) -> (Execution ()) -> Execution Value          
-generateValue t set guard = let newValue = defaultValue t in
-  do
-    set newValue 
-    guard
-    return newValue  
-  
-{- Runtime failures -}
-
-data FailureSource = 
-  SpecViolation SpecClause |    -- ^ Violation of user-defined specification
-  DivisionByZero |              -- ^ Division by zero  
-  UnsupportedConstruct String | -- ^ Language construct is not yet supported (should disappear in later versions)
-  InfiniteDomain Id Interval |  -- ^ Quantification over an infinite set
-  NoImplementation Id |         -- ^ Call to a procedure with no implementation
-  InternalFailure InternalCode  -- ^ Must be cought inside the interpreter and never reach the user
-  deriving Eq
-
--- | Information about a procedure or function call  
-data StackFrame = StackFrame {
-  callPos :: SourcePos, -- ^ Source code position of the call
-  callName :: Id        -- ^ Name of procedure or function
-} deriving Eq
-
-type StackTrace = [StackFrame]
-
--- | Failures that occur during execution
-data RuntimeFailure = RuntimeFailure {
-  rtfSource :: FailureSource,   -- ^ Source of the failure
-  rtfPos :: SourcePos,          -- ^ Location where the failure occurred
-  rtfEnv :: Environment,        -- ^ Environment at the time of failure
-  rtfTrace :: StackTrace        -- ^ Stack trace from the program entry point to the procedure where the failure occurred
-}
-
--- | Throw a run-time failure
-throwRuntimeFailure source pos = do
-  env <- get
-  throwError (RuntimeFailure source pos env [])
-
--- | Push frame on the stack trace of a runtime failure
-addStackFrame frame (RuntimeFailure source pos env trace) = throwError (RuntimeFailure source pos env (frame : trace))
-
--- | Kinds of run-time failures
-data FailureKind = Error | -- ^ Error state reached (assertion violation)
-  Unreachable | -- ^ Unreachable state reached (assumption violation)
-  Nonexecutable -- ^ The state is OK in Boogie semantics, but the execution cannot continue due to the limitations of the interpreter
-  deriving Eq
-
--- | Kind of a run-time failure
-failureKind :: RuntimeFailure -> FailureKind
-failureKind err = case rtfSource err of
-  SpecViolation (SpecClause _ True _) -> Unreachable
-  SpecViolation (SpecClause _ False _) -> Error
-  DivisionByZero -> Error
-  _ -> Nonexecutable
-  
-instance Error RuntimeFailure where
-  noMsg    = RuntimeFailure (UnsupportedConstruct "unknown") noPos emptyEnv []
-  strMsg s = RuntimeFailure (UnsupportedConstruct s) noPos emptyEnv []
-  
--- | Pretty-printed run-time failure
-runtimeFailureDoc err = failureSourceDoc (rtfSource err) <+> posDoc (rtfPos err) $+$ 
-  text "with" <+> varsDoc revelantVars $+$
-  vsep (map stackFrameDoc (reverse (rtfTrace err)))
-  where
-    failureSourceDoc (SpecViolation (SpecClause specType isFree e)) = text (clauseName specType isFree) <+> doubleQuotes (exprDoc e) <+> defPosition specType e <+> text "violated"
-    failureSourceDoc (DivisionByZero) = text "Division by zero"
-    failureSourceDoc (InfiniteDomain var int) = text "Variable" <+> text var <+> text "quantified over an infinite domain" <+> text (show int)
-    failureSourceDoc (NoImplementation name) = text "Procedure" <+> text name <+> text "with no implementation called"
-    failureSourceDoc (UnsupportedConstruct s) = text "Unsupported construct" <+> text s
-    
-    clauseName Inline isFree = if isFree then "Assumption" else "Assertion"  
-    clauseName Precondition isFree = if isFree then "Free precondition" else "Precondition"  
-    clauseName Postcondition isFree = if isFree then "Free postcondition" else "Postcondition"  
-    clauseName LoopInvariant isFree = if isFree then "Free loop invariant" else "Loop invariant"  
-    clauseName Where True = "Where clause"  -- where clauses cannot be non-free  
-    
-    defPosition Inline _ = empty
-    defPosition LoopInvariant _ = empty
-    defPosition _ e = text "defined" <+> posDoc (position e)
-    
-    revelantVars = let env = rtfEnv err      
-      in M.filterWithKey (\k _ -> isRelevant k) (envLocals env `M.union` envGlobals env)
-      
-    isRelevant k = case rtfSource err of
-      SpecViolation (SpecClause _ _ expr) -> k `elem` freeVars expr
-      _ -> False
-    
-    stackFrameDoc f = text "in call to" <+> text (callName f) <+> posDoc (callPos f)
-    posDoc pos
-      | pos == noPos = text "from the environment"
-      | otherwise = text "at" <+> text (sourceName pos) <+> text "line" <+> int (sourceLine pos)
-
-instance Show RuntimeFailure where
-  show err = show (runtimeFailureDoc err)
-  
--- | Internal error codes 
-data InternalCode = NotLinear
-  deriving Eq
-
-throwInternalFailure code = throwRuntimeFailure (InternalFailure code) noPos
-
-{- Expressions -}
-
--- | Semantics of unary operators
-unOp :: UnOp -> Value -> Value
-unOp Neg (IntValue n)   = IntValue (-n)
-unOp Not (BoolValue b)  = BoolValue (not b)
-
--- | Semi-strict semantics of binary operators:
--- 'binOpLazy' @op lhs@ : returns the value of @lhs op@ if already defined, otherwise Nothing 
-binOpLazy :: BinOp -> Value -> Maybe Value
-binOpLazy And     (BoolValue False) = Just $ BoolValue False
-binOpLazy Or      (BoolValue True)  = Just $ BoolValue True
-binOpLazy Implies (BoolValue False) = Just $ BoolValue True
-binOpLazy Explies (BoolValue True)  = Just $ BoolValue True
-binOpLazy _ _                       = Nothing
-
--- | Strict semantics of binary operators
-binOp :: SourcePos -> BinOp -> Value -> Value -> Execution Value 
-binOp pos Plus    (IntValue n1) (IntValue n2)   = return $ IntValue (n1 + n2)
-binOp pos Minus   (IntValue n1) (IntValue n2)   = return $ IntValue (n1 - n2)
-binOp pos Times   (IntValue n1) (IntValue n2)   = return $ IntValue (n1 * n2)
-binOp pos Div     (IntValue n1) (IntValue n2)   = if n2 == 0 
-                                                then throwRuntimeFailure DivisionByZero pos
-                                                else return $ IntValue (fst (n1 `euclidean` n2))
-binOp pos Mod     (IntValue n1) (IntValue n2)   = if n2 == 0 
-                                                then throwRuntimeFailure DivisionByZero pos
-                                                else return $ IntValue (snd (n1 `euclidean` n2))
-binOp pos Leq     (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 <= n2)
-binOp pos Ls      (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 < n2)
-binOp pos Geq     (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 >= n2)
-binOp pos Gt      (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 > n2)
-binOp pos And     (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 && b2)
-binOp pos Or      (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 || b2)
-binOp pos Implies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 <= b2)
-binOp pos Explies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 >= b2)
-binOp pos Equiv   (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 == b2)
-binOp pos Eq      v1 v2                         = return $ BoolValue (v1 == v2)
-binOp pos Neq     v1 v2                         = return $ BoolValue (v1 /= v2)
-binOp pos Lc      v1 v2                         = throwRuntimeFailure (UnsupportedConstruct "orders") pos
-
--- | Euclidean division used by Boogie for integer division and modulo
-euclidean :: Integer -> Integer -> (Integer, Integer)
-a `euclidean` b =
-  case a `quotRem` b of
-    (q, r) | r >= 0    -> (q, r)
-           | b >  0    -> (q - 1, r + b)
-           | otherwise -> (q + 1, r - b)
-
--- | Evaluate an expression;
--- can have a side-effect of initializing variables that were not previously defined
-eval :: Expression -> Execution Value
-eval expr = case node expr of
-  TT -> return $ BoolValue True
-  FF -> return $ BoolValue False
-  Numeral n -> return $ IntValue n
-  Var id -> evalVar id (position expr)
-  Application id args -> evalApplication id args (position expr) Nothing
-  MapSelection m args -> evalMapSelection m args (position expr)
-  MapUpdate m args new -> evalMapUpdate m args new
-  Old e -> old $ eval e
-  IfExpr cond e1 e2 -> evalIf cond e1 e2
-  Coercion e t -> evalCoercion e t
-  UnaryExpression op e -> unOp op <$> eval e
-  BinaryExpression op e1 e2 -> evalBinary op e1 e2
-  Quantified Lambda _ _ _ -> throwRuntimeFailure (UnsupportedConstruct "lambda expressions") (position expr)
-  Quantified Forall tv vars e -> vnot <$> evalExists tv vars (enot e) (position expr)
-    where vnot (BoolValue b) = BoolValue (not b)
-  Quantified Exists tv vars e -> evalExists tv vars e (position expr)
-  
-evalVar id pos = do
-  tc <- gets envTypeContext
-  case M.lookup id (localScope tc) of
-    Just t -> lookup envLocals setLocal t
-    Nothing -> case M.lookup id (ctxGlobals tc) of
-      Just t -> lookup envGlobals setGlobal t
-      Nothing -> case M.lookup id (ctxConstants tc) of
-        Just t -> do
-          constants <- gets envConstants
-          case M.lookup id constants of
-            Just e -> eval e
-            Nothing -> return $ defaultValue t -- ToDo: cache constant value?
-        Nothing -> (error . show) (text "encountered unknown identifier during execution:" <+> text id) 
-  where
-    lookup getter setter t = do
-      vars <- gets getter
-      case M.lookup id vars of
-        Just val -> return val
-        Nothing -> generateValue t (modify . setter id) (checkWhere id pos)
-  
-evalApplication name args pos mRetType = do
-  defs <- gets (lookupFunction name)  
-  evalDefs defs
-  where
-    -- | If the guard of one of function definitions evaluates to true, apply that definition; otherwise return the default value
-    evalDefs :: [FDef] -> Execution Value
-    evalDefs [] = defaultValue . returnType <$> gets envTypeContext
-    evalDefs (FDef formals guard body : defs) = do
-      argsV <- mapM eval args
-      applicable <- evalLocally formals argsV guard `catchError` addStackFrame frame
-      case applicable of
-        BoolValue True -> evalLocally formals argsV body `catchError` addStackFrame frame 
-        BoolValue False -> evalDefs defs
-    evalLocally formals actuals expr = do
-      sig <- funSig name <$> gets envTypeContext
-      executeLocally (enterFunction sig formals args mRetType) formals actuals (eval expr)
-    returnType tc = case mRetType of
-      Nothing -> exprType tc (gen $ Application name args)
-      Just t -> t
-    frame = StackFrame pos name
-    
-evalMapSelection m args pos = do 
-  tc <- gets envTypeContext
-  let rangeType = exprType tc (gen $ MapSelection m args)
-  mV <- eval m
-  argsV <- mapM eval args
-  case mV of 
-    MapValue map -> case M.lookup argsV map of
-      Nothing -> 
-        case mapVariable tc (node m) of
-        Nothing -> return $ defaultValue rangeType -- The underlying map comes from a constant or function, nothing to check
-        Just v -> generateValue rangeType (\_ -> return ()) (checkWhere v pos) -- The underlying map comes from a variable: check the where clause
-        -- Decided not to cache map access so far, because it leads to strange effects when the map is passed as an argument and can take a lot of memory 
-        -- Just v -> generateValue rangeType (cache v map argsV) (checkWhere v pos) -- The underlying map comes from a variable: check the where clause and cache the value
-      Just v -> return v
-  where
-    mapVariable tc (Var v) = if M.member v (allVars tc)
-      then Just v
-      else Nothing
-    mapVariable tc (MapUpdate m _ _) = mapVariable tc (node m)
-    mapVariable tc _ = Nothing 
-    -- cache m map args val = setV m (MapValue (M.insert args val map))
-    
-evalMapUpdate m args new = do
-  mV <- eval m
-  argsV <- mapM eval args
-  newV <- eval new
-  case mV of 
-    MapValue map -> return $ MapValue (M.insert argsV newV map)
-  
-evalIf cond e1 e2 = do
-  v <- eval cond
-  case v of
-    BoolValue True -> eval e1    
-    BoolValue False -> eval e2    
-    
-evalCoercion (Pos pos (Application f args)) t = do
-  c <- gets envTypeContext
-  let t' = resolve c t
-  evalApplication f args pos (Just t') 
-evalCoercion e _ = eval e
-  
-evalBinary op e1 e2 = do
-  left <- eval e1
-  case binOpLazy op left of
-    Just result -> return result
-    Nothing -> do
-      right <- eval e2
-      binOp (position e1) op left right
-
--- | Finite domain      
-type Domain = [Value]      
-
-evalExists :: [Id] -> [IdType] -> Expression -> SourcePos -> Execution Value      
-evalExists tv vars e pos = do
-  tc <- gets envTypeContext
-  case node $ normalize tc (attachPos pos $ Quantified Exists tv vars e) of
-    Quantified Exists tv' vars' e' -> evalExists' tv' vars' e'
-
-evalExists' :: [Id] -> [IdType] -> Expression -> Execution Value    
-evalExists' tv vars e = do
-  results <- executeLocally (enterQuantified tv vars) [] [] evalWithDomains
-  return $ BoolValue (any isTrue results)
-  where
-    evalWithDomains = do
-      doms <- domains e varNames
-      evalForEach varNames doms
-    -- | evalForEach vars domains: evaluate e for each combination of possible values of vars, drown from respective domains
-    evalForEach :: [Id] -> [Domain] -> Execution [Value]
-    evalForEach [] [] = replicate 1 <$> eval e
-    evalForEach (var : vars) (dom : doms) = concat <$> forM dom (fixOne vars doms var)
-    -- | Fix the value of var to val, then evaluate e for each combination of values for the rest of vars
-    fixOne :: [Id] -> [Domain] -> Id -> Value -> Execution [Value]
-    fixOne vars doms var val = do
-      setV var val
-      evalForEach vars doms
-    isTrue (BoolValue b) = b
-    varNames = map fst vars
-      
-{- Statements -}
-
--- | Execute a basic statement
--- (no jump, if or while statements allowed)
-exec :: Statement -> Execution ()
-exec stmt = case node stmt of
-  Predicate specClause -> execPredicate specClause (position stmt)
-  Havoc ids -> execHavoc ids (position stmt)
-  Assign lhss rhss -> execAssign lhss rhss
-  Call lhss name args -> execCall lhss name args (position stmt)
-  CallForall name args -> return () -- ToDo: assume (forall args :: pre ==> post)?
-  
-execPredicate specClause pos = do
-  b <- eval $ specExpr specClause
-  case b of 
-    BoolValue True -> return ()
-    BoolValue False -> throwRuntimeFailure (SpecViolation specClause) pos
-    
-execHavoc ids pos = do
-  tc <- gets envTypeContext
-  mapM_ (havoc tc) ids 
-  where
-    havoc tc id = generateValue (exprType tc . gen . Var $ id) (setV id) (checkWhere id pos) 
-    
-execAssign lhss rhss = do
-  rVals <- mapM eval rhss'
-  setAll lhss' rVals
-  where
-    lhss' = map fst (zipWith simplifyLeft lhss rhss)
-    rhss' = map snd (zipWith simplifyLeft lhss rhss)
-    simplifyLeft (id, []) rhs = (id, rhs)
-    simplifyLeft (id, argss) rhs = (id, mapUpdate (gen $ Var id) argss rhs)
-    mapUpdate e [args] rhs = gen $ MapUpdate e args rhs
-    mapUpdate e (args1 : argss) rhs = gen $ MapUpdate e args1 (mapUpdate (gen $ MapSelection e args1) argss rhs)
-    
-execCall lhss name args pos = do
-  tc <- gets envTypeContext
-  defs <- gets (lookupProcedure name)
-  case defs of
-    [] -> throwRuntimeFailure (NoImplementation name) pos
-    def : _ -> do
-      let lhssExpr = map (attachPos (ctxPos tc) . Var) lhss
-      retsV <- execProcedure (procSig name tc) def args lhssExpr `catchError` addStackFrame frame
-      setAll lhss retsV
-  where
-    frame = StackFrame pos name
-    
--- | Execute program consisting of blocks starting from the block labeled label.
--- Return the location of the exit point.
-execBlock :: Map Id [Statement] -> Id -> Execution SourcePos
-execBlock blocks label = let
-  block = blocks ! label
-  statements = init block
-  in do
-    mapM exec statements
-    case last block of
-      Pos pos Return -> return pos
-      Pos _ (Goto lbs) -> tryOneOf blocks lbs
-  
--- | tryOneOf blocks labels: try executing blocks starting with each of labels,
--- until we find one that does not result in an assumption violation      
-tryOneOf :: Map Id [Statement] -> [Id] -> Execution SourcePos        
-tryOneOf blocks (l : lbs) = execBlock blocks l `catchError` retry
-  where
-    retry err 
-      | failureKind err == Unreachable && not (null lbs) = tryOneOf blocks lbs
-      | otherwise = throwError err
-  
--- | 'execProcedure' @sig def args lhss@ :
--- Execute definition @def@ of procedure @sig@ with actual arguments @args@ and call left-hand sides @lhss@
-execProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Execution [Value]
-execProcedure sig def args lhss = let 
-  ins = pdefIns def
-  outs = pdefOuts def
-  blocks = snd (pdefBody def)
-  exitPoint pos = if pos == noPos 
-    then pdefPos def  -- Fall off the procedure body: take the procedure definition location
-    else pos          -- A return statement inside the body
-  execBody = do
-    checkPreconditions sig def
-    olds <- saveOld
-    pos <- exitPoint <$> execBlock blocks startLabel
-    checkPostonditions sig def pos
-    restoreOld olds
-    mapM (eval . attachPos (pdefPos def) . Var) outs
-  in do
-    argsV <- mapM eval args
-    executeLocally (enterProcedure sig def args lhss) ins argsV execBody
-    
-{- Specs -}
-
--- | Assert preconditions of definition def of procedure sig
-checkPreconditions sig def = mapM_ (exec . attachPos (pdefPos def) . Predicate . subst sig) (psigRequires sig)
-  where 
-    subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
-
--- | Assert postconditions of definition def of procedure sig at exitPoint    
-checkPostonditions sig def exitPoint = mapM_ (exec . attachPos exitPoint . Predicate . subst sig) (psigEnsures sig)
-  where 
-    subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
-
--- | Assume where clause of variable at a program location pos
--- (pos will be reported as the location of the failure instead of the location of the variable definition).
-checkWhere id pos = do
-  whereClauses <- ctxWhere <$> gets envTypeContext
-  case M.lookup id whereClauses of
-    Nothing -> return ()
-    Just w -> (exec . attachPos pos . Predicate . SpecClause Where True) w
-
-{- Preprocessing -}
-
--- | Collect constant, function and procedure definitions from the program
-collectDefinitions :: Program -> SafeExecution ()
-collectDefinitions (Program decls) = mapM_ processDecl decls
-  where
-    processDecl (Pos _ (FunctionDecl name _ args _ (Just body))) = processFunctionBody name args body
-    processDecl (Pos pos (ProcedureDecl name _ args rets _ (Just body))) = processProcedureBody name pos (map noWhere args) (map noWhere rets) body
-    processDecl (Pos pos (ImplementationDecl name _ args rets bodies)) = mapM_ (processProcedureBody name pos args rets) bodies
-    processDecl (Pos _ (AxiomDecl expr)) = processAxiom expr
-    processDecl _ = return ()
-  
-processFunctionBody name args body = let
-  formals = map (formalName . fst) args
-  guard = gen TT
-  in
-    modify $ addFunctionDefs name [FDef formals guard body]
-  where
-    formalName Nothing = dummyFArg 
-    formalName (Just n) = n    
-
-processProcedureBody name pos args rets body = do
-  sig <- procSig name <$> gets envTypeContext
-  modify $ addProcedureDef name (PDef argNames retNames (paramsRenamed sig) (flatten body) pos) 
-  where
-    argNames = map fst args
-    retNames = map fst rets
-    flatten (locals, statements) = (concat locals, M.fromList (toBasicBlocks statements))
-    paramsRenamed sig = map itwId (psigParams sig) /= (argNames ++ retNames)     
-
-processAxiom expr = do
-  extractConstantDefs expr
-  extractFunctionDefs expr []
-  
-{- Constant and function definitions -}
-
--- | Extract constant definitions from a boolean expression bExpr
-extractConstantDefs :: Expression -> SafeExecution ()
-extractConstantDefs bExpr = case node bExpr of  
-  BinaryExpression Eq (Pos _ (Var c)) rhs -> modify $ addConstantDef c rhs -- c == rhs: remember rhs as a definition for c
-  _ -> return ()
-
--- | Extract function definitions from a boolean expression bExpr, using guards extracted from the exclosing expression.
--- bExpr of the form "(forall x :: P(x, c) ==> f(x, c) == rhs(x, c) && B) && A",
--- with zero or more bound variables x and zero or more constants c,
--- produces a definition "f(x, x') = rhs(x, x')" with a guard "P(x) && x' == c"
-extractFunctionDefs :: Expression -> [Expression] -> SafeExecution ()
-extractFunctionDefs bExpr guards = extractFunctionDefs' (node bExpr) guards
-
-extractFunctionDefs' (BinaryExpression Eq (Pos _ (Application f args)) rhs) outerGuards = do
-  c <- gets envTypeContext
-  -- Only possible if each argument is either a variables or does not involve variables and there are no extra variables in rhs:
-  if all (simple c) args && closedRhs c
-    then do    
-      let (formals, guards) = unzip (extractArgs c)
-      let allGuards = concat guards ++ outerGuards
-      let guard = if null allGuards then gen TT else foldl1 (|&|) allGuards
-      modify $ addFunctionDefs f [FDef formals guard rhs]
-    else return ()
-  where
-    simple _ (Pos p (Var _)) = True
-    simple c e = null $ freeVars e `intersect` M.keys (ctxIns c)
-    closedRhs c = null $ (freeVars rhs \\ concatMap freeVars args) `intersect` M.keys (ctxIns c)
-    extractArgs c = zipWith (extractArg c) args [0..]
-    -- | Formal argument name and guards extracted from an actual argument at position i
-    extractArg :: Context -> Expression -> Integer -> (String, [Expression])
-    extractArg c (Pos p e) i = let 
-      x = freshArgName i 
-      xExpr = attachPos p $ Var x
-      in 
-        case e of
-          Var arg -> if arg `M.member` ctxIns c 
-            then (arg, []) -- Bound variable of the enclosing quantifier: use variable name as formal, no additional guards
-            else (x, [xExpr |=| Pos p e]) -- Constant: use fresh variable as formal (will only appear in the guard), add equality guard
-          _ -> (x, [xExpr |=| Pos p e])
-    freshArgName i = f ++ (nonIdChar : show i)
-extractFunctionDefs' (BinaryExpression Implies cond bExpr) outerGuards = extractFunctionDefs bExpr (cond : outerGuards)
-extractFunctionDefs' (BinaryExpression And bExpr1 bExpr2) outerGuards = do
-  extractFunctionDefs bExpr1 outerGuards
-  extractFunctionDefs bExpr2 outerGuards
-extractFunctionDefs' (Quantified Forall tv vars bExpr) outerGuards = executeLocally (enterQuantified tv vars) [] [] (extractFunctionDefs bExpr outerGuards)
-extractFunctionDefs' _ _ = return ()
-   
-{- Quantification -}
-
--- | Sets of interval constraints on integer variables
-type Constraints = Map Id Interval
-            
--- | The set of domains for each variable in vars, outside which boolean expression boolExpr is always false.
--- Fails if any of the domains are infinite or cannot be found.
-domains :: Expression -> [Id] -> Execution [Domain]
-domains boolExpr vars = do
-  initC <- foldM initConstraints M.empty vars
-  finalC <- inferConstraints boolExpr initC 
-  forM vars (domain finalC)
-  where
-    initConstraints c var = do
-      tc <- gets envTypeContext
-      case M.lookup var (allVars tc) of
-        Just BoolType -> return c
-        Just IntType -> return $ M.insert var top c
-        _ -> throwRuntimeFailure (UnsupportedConstruct "quantification over a map or user-defined type") (position boolExpr)
-    domain c var = do
-      tc <- gets envTypeContext
-      case M.lookup var (allVars tc) of
-        Just BoolType -> return $ map BoolValue [True, False]
-        Just IntType -> do
-          case c ! var of
-            int | isBottom int -> return []
-            Interval (Finite l) (Finite u) -> return $ map IntValue [l..u]
-            int -> throwRuntimeFailure (InfiniteDomain var int) (position boolExpr)
-
--- | Starting from initial constraints, refine them with the information from boolExpr,
--- until fixpoint is reached or the domain for one of the variables is empty.
--- This function terminates because the interval for each variable can only become smaller with each iteration.
-inferConstraints :: Expression -> Constraints -> Execution Constraints
-inferConstraints boolExpr constraints = do
-  constraints' <- foldM refineVar constraints (M.keys constraints)
-  if bot `elem` M.elems constraints'
-    then return $ M.map (const bot) constraints'  -- if boolExpr does not have a satisfying assignment to one variable, then it has none to all variables
-    else if constraints == constraints'
-      then return constraints'                    -- if a fixpoint is reached, return it
-      else inferConstraints boolExpr constraints' -- otherwise do another iteration
-  where
-    refineVar :: Constraints -> Id -> Execution Constraints
-    refineVar c id = do
-      int <- inferInterval boolExpr c id
-      return $ M.insert id (meet (c ! id) int) c 
-
--- | Infer an interval for variable x, outside which boolean expression booExpr is always false, 
--- assuming all other quantified variables satisfy constraints;
--- boolExpr has to be in negation-prenex normal form.
-inferInterval :: Expression -> Constraints -> Id -> Execution Interval
-inferInterval boolExpr constraints x = (case node boolExpr of
-  FF -> return bot
-  BinaryExpression And be1 be2 -> liftM2 meet (inferInterval be1 constraints x) (inferInterval be2 constraints x)
-  BinaryExpression Or be1 be2 -> liftM2 join (inferInterval be1 constraints x) (inferInterval be2 constraints x)
-  BinaryExpression Eq ae1 ae2 -> do
-    (a, b) <- toLinearForm (ae1 |-| ae2) constraints x
-    if 0 <: a && 0 <: b
-      then return top
-      else return $ -b // a
-  BinaryExpression Leq ae1 ae2 -> do
-    (a, b) <- toLinearForm (ae1 |-| ae2) constraints x
-    if isBottom a || isBottom b
-      then return bot
-      else if 0 <: a && not (isBottom (meet b nonPositives))
-        then return top
-        else return $ join (lessEqual (-b // meet a positives)) (greaterEqual (-b // meet a negatives))
-  BinaryExpression Ls ae1 ae2 -> inferInterval (ae1 |<=| (ae2 |-| num 1)) constraints x
-  BinaryExpression Geq ae1 ae2 -> inferInterval (ae2 |<=| ae1) constraints x
-  BinaryExpression Gt ae1 ae2 -> inferInterval (ae2 |<=| (ae1 |-| num 1)) constraints x
-  -- Quantifier can only occur here if it is alternating with the enclosing one, hence no domain can be inferred 
-  _ -> return top
-  ) `catchError` handleNotLinear
-  where      
-    lessEqual int | isBottom int = bot
-                  | otherwise = Interval NegInf (upper int)
-    greaterEqual int  | isBottom int = bot
-                      | otherwise = Interval (lower int) Inf
-    handleNotLinear err = case rtfSource err of
-      InternalFailure NotLinear -> return top
-      _ -> throwError err                      
-
--- | Linear form (A, B) represents a set of expressions a*x + b, where a in A and b in B
-type LinearForm = (Interval, Interval)
-
--- | If possible, convert arithmetic expression aExpr into a linear form over variable x,
--- assuming all other quantified variables satisfy constraints.
-toLinearForm :: Expression -> Constraints -> Id -> Execution LinearForm
-toLinearForm aExpr constraints x = case node aExpr of
-  Numeral n -> return (0, fromInteger n)
-  Var y -> if x == y
-    then return (1, 0)
-    else case M.lookup y constraints of
-      Just int -> return (0, int)
-      Nothing -> const aExpr
-  Application name args -> if null $ M.keys constraints `intersect` freeVars aExpr
-    then const aExpr
-    else throwInternalFailure NotLinear
-  MapSelection m args -> if null $ M.keys constraints `intersect` freeVars aExpr
-    then const aExpr
-    else throwInternalFailure NotLinear
-  Old e -> old $ toLinearForm e constraints x
-  UnaryExpression Neg e -> do
-    (a, b) <- toLinearForm e constraints x
-    return (-a, -b)
-  BinaryExpression op e1 e2 -> do
-    left <- toLinearForm e1 constraints x
-    right <- toLinearForm e2 constraints x 
-    combineBinOp op left right
-  where
-    const e = do
-      v <- eval e
-      case v of
-        IntValue n -> return (0, fromInteger n)
-    combineBinOp Plus   (a1, b1) (a2, b2) = return (a1 + a2, b1 + b2)
-    combineBinOp Minus  (a1, b1) (a2, b2) = return (a1 - a2, b1 - b2)
-    combineBinOp Times  (a, b)   (0, k)   = return (k * a, k * b)
-    combineBinOp Times  (0, k)   (a, b)   = return (k * a, k * b)
-    combineBinOp _ _ _ = throwInternalFailure NotLinear                      
-  +{-# LANGUAGE FlexibleContexts, Rank2Types #-}
+
+-- | Interpreter for Boogie 2
+module Language.Boogie.Interpreter (
+  -- * Executing programs
+  executeProgramDet,
+  executeProgram,
+  executeProgramGeneric,
+  -- * Run-time failures
+  FailureSource (..),
+  -- InternalCode,
+  StackFrame (..),
+  StackTrace,
+  RuntimeFailure (..),  
+  runtimeFailureDoc,
+  FailureKind (..),
+  failureKind,
+  -- * Execution outcomes
+  TestCase (..),
+  isPass,
+  isInvalid,
+  isNonexecutable,
+  isFail,
+  testCaseSummary,  
+  finalStateDoc,
+  Summary (..),
+  testSessionSummary,
+  summaryDoc,
+  -- * Executing parts of programs
+  eval,
+  exec,
+  execProcedure,
+  preprocess
+  ) where
+
+import Language.Boogie.Environment  
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Heap
+import Language.Boogie.Generator
+import Language.Boogie.Intervals
+import Language.Boogie.Position
+import Language.Boogie.Tokens (nonIdChar)
+import Language.Boogie.PrettyPrinter
+import Language.Boogie.TypeChecker
+import Language.Boogie.NormalForm
+import Language.Boogie.BasicBlocks
+import Data.Maybe
+import Data.List
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
+import Control.Monad.Error hiding (join)
+import Control.Applicative hiding (empty)
+import Control.Monad.State hiding (join)
+import Control.Monad.Identity hiding (join)
+import Control.Monad.Stream
+import Control.Lens hiding (Context, at)
+import Text.PrettyPrint
+
+{- Interface -}
+
+-- | 'executeProgram' @p tc entryPoint@ :
+-- Execute program @p@ /non-deterministically/ in type context @tc@ starting from procedure @entryPoint@ 
+-- and return an infinite list of possible outcomes (each either runtime failure or the final variable store).
+-- Whenever a value is unspecified, all values of the required type are tried exhaustively.
+executeProgram :: Program -> Context -> Generator Stream -> Maybe Integer -> Id -> [TestCase]
+executeProgram p tc gen qbound entryPoint = toList $ executeProgramGeneric p tc gen qbound entryPoint
+
+-- | 'executeProgramDet' @p tc entryPoint@ :
+-- Execute program @p@ /deterministically/ in type context @tc@ starting from procedure @entryPoint@ 
+-- and return a single outcome.
+-- Whenever a value is unspecified, a default value of the required type is used.
+executeProgramDet :: Program -> Context -> Maybe Integer -> Id -> TestCase
+executeProgramDet p tc qbound entryPoint = runIdentity $ executeProgramGeneric p tc defaultGenerator qbound entryPoint
+      
+-- | 'executeProgramGeneric' @p tc generator qbound entryPoint@ :
+-- Execute program @p@ in type context @tc@ with input generator @generator@, starting from procedure @entryPoint@,
+-- and return the outcome(s) embedded into the generator's monad.
+executeProgramGeneric :: (Monad m, Functor m) => Program -> Context -> Generator m -> Maybe Integer -> Id -> m (TestCase)
+executeProgramGeneric p tc generator qbound entryPoint = result <$> runStateT (runErrorT programExecution) (initEnv tc generator qbound)
+  where
+    programExecution = do
+      execUnsafely $ preprocess p
+      execRootCall
+    sig = procSig entryPoint tc
+    execRootCall = do
+      let params = psigParams sig
+      let defaultBinding = M.fromList $ zip (psigTypeVars sig) (repeat defaultType)
+      let paramTypes = map (typeSubst defaultBinding) (map itwType params)
+      envTypeContext %= setLocals (M.fromList $ zip (map itwId params) paramTypes)
+      execCallBySig (assumePreconditions sig) (map itwId (psigRets sig)) (map (gen . Var . itwId) (psigArgs sig)) noPos
+    defaultType = BoolType      
+    result (Left err, env) = TestCase sig (env^.envMemory) (Just err)
+    result (_, env)      = TestCase sig (env^.envMemory) Nothing    
+            
+{- Executions -}
+
+-- | Computations with 'Environment' as state, which can result in either @a@ or 'RuntimeFailure'
+type Execution m a = ErrorT RuntimeFailure (StateT (Environment m) m) a
+
+-- | Computations with 'Environment' as state, which always result in @a@
+type SafeExecution m a = StateT (Environment m) m a
+
+-- | 'execUnsafely' @computation@ : Execute a safe @computation@ in an unsafe environment
+execUnsafely :: (Monad m, Functor m) => SafeExecution m a -> Execution m a
+execUnsafely computation = ErrorT (Right <$> computation)
+
+-- | 'execSafely' @computation handler@ : Execute an unsafe @computation@ in a safe environment, handling errors that occur in @computation@ with @handler@
+execSafely :: (Monad m, Functor m) => Execution m a -> (RuntimeFailure -> SafeExecution m a) -> SafeExecution m a
+execSafely computation handler = do
+  eres <- runErrorT computation
+  either handler return eres
+  
+-- | Computations that perform a cleanup at the end
+class Monad s => Finalizer s where
+  finally :: s a -> s () -> s a
+    
+instance Monad m => Finalizer (StateT s m) where
+  finally main cleanup = do
+    res <- main
+    cleanup
+    return res
+
+instance (Error e, Monad m) => Finalizer (ErrorT e m) where
+  finally main cleanup = do
+    res <- main `catchError` (\err -> cleanup >> throwError err)
+    cleanup
+    return res
+    
+-- | Run execution in the old environment
+old :: (Monad m, Functor m) => Execution m a -> Execution m a
+old execution = do
+  oldEnv <- get
+  envMemory.memGlobals .= oldEnv^.envMemory.memOld
+  envInOld .= True            
+  res <- execution
+  env <- get
+  envMemory.memOld .= env^.envMemory.memGlobals
+  envMemory.memGlobals .= (oldEnv^.envMemory.memGlobals) `M.union` (env^.envMemory.memGlobals)   -- Include freshly initialized globals into both old and new states
+  envInOld .= oldEnv^.envInOld                      
+  return res
+
+-- | Save current values of global variables in memOld, return the previous memory
+saveOld :: (Monad m, Functor m) => Execution m Memory 
+saveOld = do
+  mem <- use envMemory
+  let globals = mem^.memGlobals
+  envMemory.memOld .= globals
+  mapM_ incRefCountValue (M.elems globals) -- Each value stored in globals is now pointed by an additional (old) variable
+  return $ mem
+
+-- | 'restoreOld' @oldMem@ : reset 'memOld' to its value from @oldMem@
+restoreOld :: (Monad m, Functor m) => Memory -> Execution m ()  
+restoreOld oldMem = do
+  mem <- use envMemory
+  let (oldOlds, newOlds) = M.partitionWithKey (\var _ -> M.member var (oldMem^.memGlobals)) (mem^.memOld)
+  envMemory.memOld .= (oldMem^.memOld) `M.union` newOlds -- Add old values for freshly initialized globals (they are valid up until the program entry point, so could be accessed until the end of the program)
+  mapM_ decRefCountValue (M.elems oldOlds) -- Old values for previously initialized varibles go out of scope
+    
+-- | Enter local scope (apply localTC to the type context and assign actuals to formals),
+-- execute computation,
+-- then restore type context and local variables to their initial values
+executeLocally :: (MonadState (Environment m) s, Finalizer s) => (Context -> Context) -> [Id] -> [Id] -> [Value] -> AbstractStore -> s a -> s a
+executeLocally localTC locals formals actuals localConstraints computation = do
+  oldEnv <- get
+  envTypeContext %= localTC
+  envMemory.memLocals %= deleteAll locals
+  envConstraints.amLocals .= localConstraints
+  zipWithM_ (setVar memLocals) formals actuals -- All formals are fresh, can use emptyStore for current values
+  computation `finally` unwind oldEnv
+  where
+    -- | Restore type context and the values of local variables 
+    unwind oldEnv = do
+      mapM_ (unsetVar memLocals) locals
+      env <- get
+      envTypeContext .= oldEnv^.envTypeContext
+      envMemory.memLocals .= deleteAll locals (env^.envMemory.memLocals) `M.union` (oldEnv^.envMemory.memLocals)
+      envConstraints.amLocals .= oldEnv^.envConstraints.amLocals -- Constraints cannot be initialized in a nested context, so here we can just restore old locals
+                              
+{- Runtime failures -}
+
+data FailureSource = 
+  SpecViolation SpecClause |          -- ^ Violation of user-defined specification
+  DivisionByZero |                    -- ^ Division by zero  
+  UnsupportedConstruct String |       -- ^ Language construct is not yet supported (should disappear in later versions)
+  InfiniteDomain Id Interval |        -- ^ Quantification over an infinite set
+  MapEquality Value Value |           -- ^ Equality of two maps cannot be determined
+  InternalException InternalCode      -- ^ Must be cought inside the interpreter and never reach the user
+  deriving Eq
+
+-- | Information about a procedure or function call  
+data StackFrame = StackFrame {
+  callPos :: SourcePos,    -- ^ Source code position of the call
+  callName :: Id           -- ^ Name of procedure or function
+} deriving Eq
+
+type StackTrace = [StackFrame]
+
+-- | Failures that occur during execution
+data RuntimeFailure = RuntimeFailure {
+  rtfSource :: FailureSource,   -- ^ Source of the failure
+  rtfPos :: SourcePos,          -- ^ Location where the failure occurred
+  rtfMemory :: Memory,          -- ^ Memory state at the time of failure
+  rtfTrace :: StackTrace        -- ^ Stack trace from the program entry point to the procedure where the failure occurred
+}
+
+-- | Throw a run-time failure
+throwRuntimeFailure source pos = do
+  mem <- use envMemory
+  throwError (RuntimeFailure source pos mem [])
+
+-- | Push frame on the stack trace of a runtime failure
+addStackFrame frame (RuntimeFailure source pos mem trace) = throwError (RuntimeFailure source pos mem (frame : trace))
+
+-- | Kinds of run-time failures
+data FailureKind = Error | -- ^ Error state reached (assertion violation)
+  Unreachable | -- ^ Unreachable state reached (assumption violation)
+  Nonexecutable -- ^ The state is OK in Boogie semantics, but the execution cannot continue due to the limitations of the interpreter
+  deriving Eq
+
+-- | Kind of a run-time failure
+failureKind :: RuntimeFailure -> FailureKind
+failureKind err = case rtfSource err of
+  SpecViolation (SpecClause _ True _) -> Unreachable
+  SpecViolation (SpecClause _ False _) -> Error
+  DivisionByZero -> Error
+  _ -> Nonexecutable
+  
+instance Error RuntimeFailure where
+  noMsg    = RuntimeFailure (UnsupportedConstruct "unknown") noPos emptyMemory []
+  strMsg s = RuntimeFailure (UnsupportedConstruct s) noPos emptyMemory []
+  
+-- | Pretty-printed run-time failure
+runtimeFailureDoc debug err = 
+  let store = (if debug then id else userStore ((rtfMemory err)^.memHeap)) (M.filterWithKey (\k _ -> isRelevant k) (visibleVariables (rtfMemory err)))
+      sDoc = storeDoc store 
+  in failureSourceDoc (rtfSource err) <+> posDoc (rtfPos err) <+> 
+  (if isEmpty sDoc then empty else text "with") $+$ nest 2 sDoc $+$
+  vsep (map stackFrameDoc (reverse (rtfTrace err)))
+  where
+    failureSourceDoc (SpecViolation (SpecClause specType isFree e)) = text (clauseName specType isFree) <+> doubleQuotes (exprDoc e) <+> defPosition specType e <+> text "violated"
+    failureSourceDoc (DivisionByZero) = text "Division by zero"
+    failureSourceDoc (InfiniteDomain var int) = text "Variable" <+> text var <+> text "quantified over an infinite domain" <+> text (show int)
+    failureSourceDoc (MapEquality m1 m2) = text "Cannot determine equality of map values" <+> valueDoc m1 <+> text "and" <+> valueDoc m2
+    failureSourceDoc (UnsupportedConstruct s) = text "Unsupported construct" <+> text s
+    
+    clauseName Inline isFree = if isFree then "Assumption" else "Assertion"  
+    clauseName Precondition isFree = if isFree then "Free precondition" else "Precondition"  
+    clauseName Postcondition isFree = if isFree then "Free postcondition" else "Postcondition"  
+    clauseName LoopInvariant isFree = if isFree then "Free loop invariant" else "Loop invariant"  
+    clauseName Where True = "Where clause"  -- where clauses cannot be non-free  
+    clauseName Axiom True = "Axiom"  -- axioms cannot be non-free  
+    
+    defPosition Inline _ = empty
+    defPosition LoopInvariant _ = empty
+    defPosition _ e = text "defined" <+> posDoc (position e)
+    
+    isRelevant k = case rtfSource err of
+      SpecViolation (SpecClause _ _ expr) -> k `elem` freeVars expr
+      _ -> False
+    
+    stackFrameDoc f = text "in call to" <+> text (callName f) <+> posDoc (callPos f)
+    posDoc pos
+      | pos == noPos = text "from the environment"
+      | otherwise = text "at" <+> text (sourceName pos) <+> text "line" <+> int (sourceLine pos)
+
+instance Show RuntimeFailure where
+  show err = show (runtimeFailureDoc True err)
+  
+-- | Do two runtime failures represent the same fault?
+-- Yes if the same property failed at the same program location
+-- or, for preconditions, for the same caller   
+sameFault f f' = rtfSource f == rtfSource f' && 
+  case rtfSource f of
+    SpecViolation (SpecClause Precondition False _) -> last (rtfTrace f) == last (rtfTrace f')
+    _ -> rtfPos f == rtfPos f'    
+  
+instance Eq RuntimeFailure where
+  f == f' = sameFault f f'
+    
+-- | Internal error codes 
+data InternalCode = NotLinear | UnderConstruction Int
+  deriving Eq
+
+throwInternalException code = throwRuntimeFailure (InternalException code) noPos
+
+{- Execution results -}
+    
+-- | Description of an execution
+data TestCase = TestCase {
+  tcProcedure :: PSig,              -- ^ Root procedure (entry point) of the execution
+  tcMemory :: Memory,               -- ^ Final memory state (at the exit from the root procedure) 
+  tcFailure :: Maybe RuntimeFailure -- ^ Failure the execution eded with, or Nothing if the execution ended in a valid state
+}
+
+-- | 'isPass' @tc@: Does @tc@ end in a valid state?
+isPass :: TestCase -> Bool
+isPass (TestCase _ _ Nothing) =  True
+isPass _ =          False
+
+-- | 'isInvalid' @tc@: Does @tc@ and in an unreachable state?
+isInvalid :: TestCase -> Bool 
+isInvalid (TestCase _ _ (Just err))
+  | failureKind err == Unreachable = True
+isInvalid _                        = False
+
+-- | 'isNonexecutable' @tc@: Does @tc@ end in a non-executable state?
+isNonexecutable :: TestCase -> Bool 
+isNonexecutable (TestCase _ _ (Just err))
+  | failureKind err == Nonexecutable  = True
+isNonexecutable _                     = False
+
+-- | 'isFail' @tc@: Does @tc@ end in an error state?
+isFail :: TestCase -> Bool
+isFail tc = not (isPass tc || isInvalid tc || isNonexecutable tc)
+
+-- | 'testCaseSummary' @debug tc@ : Summary of @tc@'s inputs and outcome,
+-- displayed in user or debug format depending on 'debug'
+testCaseSummary :: Bool -> TestCase -> Doc
+testCaseSummary debug tc@(TestCase sig mem mErr) = text (psigName sig) <> 
+  parens (commaSep (map (inDoc . itwId) (psigArgs sig))) <>
+  (if M.null globalInputsRepr then empty else parens (commaSep (map globDoc (M.toList globalInputsRepr)))) <+>
+  outcomeDoc tc
+  where
+    storeRepr store = if debug then store else userStore (mem^.memHeap) store
+    removeEmptyMaps store = M.filter (\val -> val /= MapValue emptyMap) store
+    localsRepr = storeRepr $ mem^.memLocals
+    globalInputsRepr = removeEmptyMaps . storeRepr $ (mem^.memOld) `M.union` (mem^.memConstants)
+    inDoc name = valueDoc $ localsRepr ! name    
+    globDoc (name, val) = text name <+> text "=" <+> valueDoc val
+    outcomeDoc tc 
+      | isPass tc = text "passed"
+      | isInvalid tc = text "invalid"
+      | isNonexecutable tc = text "non-executable"
+      | otherwise = text "failed"
+      
+-- | 'finalStateDoc' @debug tc@ : outputs of @tc@, 
+-- displayed in user or debug format depending on 'debug' 
+finalStateDoc :: Bool -> TestCase -> Doc
+finalStateDoc debug tc@(TestCase sig mem mErr) = vsep $
+    (if M.null outsRepr then [] else [text "Outs:" <+> storeDoc outsRepr]) ++
+    (if M.null globalsRepr then [] else [text "Globals:" <+> storeDoc globalsRepr]) ++ 
+    (if debug then [text "Heap:" <+> heapDoc (mem^.memHeap)] else [])
+  where
+    storeRepr store = if debug then store else userStore (mem^.memHeap) store
+    outNames = map itwId (psigRets sig)
+    outsRepr = storeRepr $ M.filterWithKey (\k _ -> k `elem` outNames) (mem^.memLocals)
+    globalsRepr = storeRepr $ mem^.memGlobals
+    
+-- | Test cases are considered equivalent from a user perspective
+-- | if they are testing the same procedure and result in the same outcome
+equivalent tc1 tc2 = tcProcedure tc1 == tcProcedure tc2 && tcFailure tc1 == tcFailure tc2      
+
+-- | Test session summary
+data Summary = Summary {
+  sPassCount :: Int,            -- ^ Number of passing test cases
+  sFailCount :: Int,            -- ^ Number of failing test cases
+  sInvalidCount :: Int,         -- ^ Number of invalid test cases
+  sNonExecutableCount :: Int,   -- ^ Number of nonexecutable test cases
+  sUniqueFailures :: [TestCase] -- ^ Unique failing test cases
+}
+
+totalCount s = sPassCount s + sFailCount s + sInvalidCount s + sNonExecutableCount s
+
+-- | Pretty-printed test session summary
+summaryDoc :: Summary -> Doc
+summaryDoc summary = 
+  text "Test cases:" <+> int (totalCount summary) $+$
+  text "Passed:" <+> int (sPassCount summary) $+$
+  text "Invalid:" <+> int (sInvalidCount summary) $+$
+  text "Non executable:" <+> int (sNonExecutableCount summary) $+$
+  text "Failed:" <+> int (sFailCount summary) <+> parens (int (length (sUniqueFailures summary)) <+> text "unique") <>
+  (if null (sUniqueFailures summary) then empty else newline)
+  
+instance Show Summary where show s = show (summaryDoc s)
+
+-- | Summary of a set of test cases   
+testSessionSummary :: [TestCase] -> Summary
+testSessionSummary tcs = let 
+  passing = filter isPass tcs
+  failing = filter isFail tcs
+  invalid = filter isInvalid tcs
+  nexec = filter isNonexecutable tcs
+  in Summary {
+    sPassCount = length passing,
+    sFailCount = length failing,
+    sInvalidCount = length invalid,  
+    sNonExecutableCount = length nexec,
+    sUniqueFailures = nubBy equivalent failing
+  }    
+
+{- Basic executions -}      
+
+-- | 'generate' @f@ : computation that extracts @f@ from the generator
+generate :: (Monad m, Functor m) => (Generator m -> m a) -> Execution m a
+generate f = do    
+  gen <- use envGenerator
+  lift (lift (f gen))
+      
+-- | 'generateValue' @t pos@ : choose a value of type @t@ at source position @pos@;
+-- fail if @t@ is a type variable
+generateValue :: (Monad m, Functor m) => Type -> SourcePos -> Execution m Value
+generateValue t pos = case t of
+  IdType x [] | isTypeVar [] x -> throwRuntimeFailure (UnsupportedConstruct ("choice of a value from unknown type " ++ show t)) pos
+  -- Maps are initializaed lazily, allocate an empty map on the heap:
+  MapType _ _ _ -> allocate $ MapValue emptyMap
+  BoolType -> BoolValue <$> generate genBool
+  IntType -> IntValue <$> generate genInteger
+  IdType id _ -> do
+    n <- gets $ lookupCustomCount id
+    i <- generate (`genIndex` (n + 1))
+    when (i == n) $ modify (setCustomCount id (n + 1))
+    return $ CustomValue id i
+  
+-- | 'generateValueLike' @v@ : choose a value of the same type as @v@
+generateValueLike :: (Monad m, Functor m) => Value -> Execution m Value
+generateValueLike (BoolValue _) = generateValue BoolType noPos
+generateValueLike (IntValue _) = generateValue IntType noPos
+generateValueLike (CustomValue t _) = generateValue (IdType t []) noPos
+generateValueLike (Reference _) = allocate $ MapValue emptyMap
+generateValueLike (MapValue _) = internalError "Attempt to generateValueLike a map value directly"
+        
+-- | 'incRefCountValue' @val@ : if @val@ is a reference, increase its count
+incRefCountValue val = case val of
+  Reference r -> envMemory.memHeap %= incRefCount r
+  _ -> return ()    
+
+-- | 'decRefCountValue' @val@ : if @val@ is a reference, decrease its count  
+decRefCountValue val = case val of
+  Reference r -> envMemory.memHeap %= decRefCount r
+  _ -> return ()     
+    
+-- | 'unsetVar' @getter name@ : if @name@ was associated with a reference in @getter@, decrease its reference count
+unsetVar getter name = do
+  store <- use $ envMemory.getter
+  case M.lookup name store of    
+    Just (Reference r) -> do          
+      envMemory.memHeap %= decRefCount r
+    _ -> return ()
+
+-- | 'setVar' @setter name val@ : set value of variable @name@ to @val@ using @setter@
+setVar setter name val = do
+  incRefCountValue val
+  envMemory.setter %= M.insert name val
+
+-- | 'resetVar' @lens name val@ : set value of variable @name@ to @val@ using @lens@;
+-- if @name@ was associated with a reference, decrease its reference count
+resetVar :: (Monad m, Functor m) => StoreLens -> Id -> Value -> Execution m ()  
+resetVar lens name val = do
+  unsetVar lens name
+  setVar lens name val
+            
+-- | 'resetAnyVar' @name val@ : set value of a constant, global or local variable @name@ to @val@
+resetAnyVar name val = do
+  tc <- use envTypeContext
+  if M.member name (localScope tc)
+    then resetVar memLocals name val
+    else if M.member name (ctxGlobals tc)
+      then resetVar memGlobals name val
+      else resetVar memConstants name val
+      
+-- | 'forgetVar' @lens name@ : forget value of variable @name@ in @lens@;
+-- if @name@ was associated with a reference, decrease its reference count      
+forgetVar :: (Monad m, Functor m) => StoreLens -> Id -> Execution m ()
+forgetVar lens name = do
+  unsetVar lens name
+  envMemory.lens %= M.delete name
+      
+-- | 'forgetAnyVar' @name@ : forget value of a constant, global or local variable @name@ to @val@      
+forgetAnyVar name = do
+  tc <- use envTypeContext
+  if M.member name (localScope tc)
+    then forgetVar memLocals name
+    else if M.member name (ctxGlobals tc)
+      then forgetVar memGlobals name
+      else forgetVar memConstants name
+      
+-- | 'setMapValue' @r index val@ : map @index@ to @val@ in the map referenced by @r@
+-- (@r@ has to be a source map)
+setMapValue r index val = do
+  MapValue (Source baseVals) <- readHeap r
+  envMemory.memHeap %= update r (MapValue (Source (M.insert index val baseVals)))
+  incRefCountValue val
+  
+-- | 'forgetMapValue' @r index@ : forget value at @index@ in the map referenced by @r@  
+-- (@r@ has to be a source map)
+forgetMapValue r index = do
+  MapValue (Source baseVals) <- readHeap r
+  case M.lookup index baseVals of
+    Nothing -> return ()
+    Just val -> do
+      decRefCountValue val
+      envMemory.memHeap %= update r (MapValue (Source (M.delete index baseVals)))
+        
+-- | 'readHeap' @r@: current value of reference @r@ in the heap
+readHeap r = flip at r <$> use (envMemory.memHeap)
+    
+-- | 'allocate' @v@: store @v@ at a fresh location in the heap and return that location
+allocate :: (Monad m, Functor m) => Value -> Execution m Value
+allocate v = Reference <$> (state . withHeap . alloc) v
+  
+-- | Remove all unused references from the heap  
+collectGarbage :: (Monad m, Functor m) => Execution m ()  
+collectGarbage = do
+  h <- use (envMemory.memHeap)
+  when (hasGarbage h) (do
+    r <- state $ withHeap dealloc
+    let MapValue repr = h `at` r
+    case repr of
+      Source _ -> return ()
+      Derived base _ -> envMemory.memHeap %= decRefCount base
+    mapM_ decRefCountValue (M.elems $ stored repr)
+    envConstraints.amHeap %= M.delete r
+    collectGarbage)
+
+{- Expressions -}
+
+-- | Semantics of unary operators
+unOp :: UnOp -> Value -> Value
+unOp Neg (IntValue n)   = IntValue (-n)
+unOp Not (BoolValue b)  = BoolValue (not b)
+
+-- | Semi-strict semantics of binary operators:
+-- 'binOpLazy' @op lhs@ : returns the value of @lhs op@ if already defined, otherwise Nothing 
+binOpLazy :: BinOp -> Value -> Maybe Value
+binOpLazy And     (BoolValue False) = Just $ BoolValue False
+binOpLazy Or      (BoolValue True)  = Just $ BoolValue True
+binOpLazy Implies (BoolValue False) = Just $ BoolValue True
+binOpLazy Explies (BoolValue True)  = Just $ BoolValue True
+binOpLazy _ _                       = Nothing
+
+-- | Strict semantics of binary operators
+binOp :: (Monad m, Functor m) => SourcePos -> BinOp -> Value -> Value -> Execution m Value 
+binOp pos Plus    (IntValue n1) (IntValue n2)   = return $ IntValue (n1 + n2)
+binOp pos Minus   (IntValue n1) (IntValue n2)   = return $ IntValue (n1 - n2)
+binOp pos Times   (IntValue n1) (IntValue n2)   = return $ IntValue (n1 * n2)
+binOp pos Div     (IntValue n1) (IntValue n2)   = if n2 == 0 
+                                                then throwRuntimeFailure DivisionByZero pos
+                                                else return $ IntValue (fst (n1 `euclidean` n2))
+binOp pos Mod     (IntValue n1) (IntValue n2)   = if n2 == 0 
+                                                then throwRuntimeFailure DivisionByZero pos
+                                                else return $ IntValue (snd (n1 `euclidean` n2))
+binOp pos Leq     (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 <= n2)
+binOp pos Ls      (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 < n2)
+binOp pos Geq     (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 >= n2)
+binOp pos Gt      (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 > n2)
+binOp pos And     (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 && b2)
+binOp pos Or      (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 || b2)
+binOp pos Implies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 <= b2)
+binOp pos Explies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 >= b2)
+binOp pos Equiv   (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 == b2)
+binOp pos Eq      v1 v2                         = evalEquality v1 v2
+binOp pos Neq     v1 v2                         = vnot <$> evalEquality v1 v2
+binOp pos Lc      v1 v2                         = throwRuntimeFailure (UnsupportedConstruct "orders") pos
+
+-- | Euclidean division used by Boogie for integer division and modulo
+euclidean :: Integer -> Integer -> (Integer, Integer)
+a `euclidean` b =
+  case a `quotRem` b of
+    (q, r) | r >= 0    -> (q, r)
+           | b >  0    -> (q - 1, r + b)
+           | otherwise -> (q + 1, r - b)
+         
+-- | Evaluate an expression;
+-- can have a side-effect of initializing variables that were not previously defined
+eval :: (Monad m, Functor m) => Expression -> Execution m Value
+eval expr = case node expr of
+  TT -> return $ BoolValue True
+  FF -> return $ BoolValue False
+  Numeral n -> return $ IntValue n
+  Var name -> evalVar name (position expr)
+  Application name args -> evalMapSelection (functionExpr name) args (position expr)
+  MapSelection m args -> evalMapSelection m args (position expr)
+  MapUpdate m args new -> evalMapUpdate m args new (position expr)
+  Old e -> old $ eval e
+  IfExpr cond e1 e2 -> evalIf cond e1 e2
+  Coercion e t -> eval e
+  UnaryExpression op e -> unOp op <$> eval e
+  BinaryExpression op e1 e2 -> evalBinary op e1 e2
+  Quantified Lambda _ _ _ -> throwRuntimeFailure (UnsupportedConstruct "lambda expressions") (position expr)
+  Quantified Forall tv vars e -> vnot <$> evalExists tv vars (enot e) (position expr)
+  Quantified Exists tv vars e -> evalExists tv vars e (position expr)
+  where
+    functionExpr name = gen . Var $ functionConst name
+  
+evalVar :: (Monad m, Functor m) => Id -> SourcePos -> Execution m Value  
+evalVar name pos = do
+  tc <- use envTypeContext
+  case M.lookup name (localScope tc) of
+    Just t -> evalVarWith t memLocals False
+    Nothing -> case M.lookup name (ctxGlobals tc) of
+      Just t -> do
+        inOld <- use envInOld
+        evalVarWith t memGlobals (not inOld) -- Unless we are evaluating and old expression, also initialize the old value of the global
+      Nothing -> case M.lookup name (ctxConstants tc) of
+        Just t -> evalVarWith t memConstants False
+        Nothing -> (internalError . show) (text "Encountered unknown identifier during execution:" <+> text name) 
+  where  
+    evalVarWith :: (Monad m, Functor m) => Type -> StoreLens -> Bool -> Execution m Value
+    evalVarWith t lens initOld = do
+      s <- use $ envMemory.lens
+      case M.lookup name s of         -- Lookup a cached value
+        Just val -> wellDefined val
+        Nothing -> do                 -- If not found, look for an applicable definition
+          definedValue <- checkNameDefinitions name t pos
+          case definedValue of
+            Just val -> do
+              setVar lens name val
+              checkNameConstraints name pos
+              forgetVar lens name
+              return val
+            Nothing -> do             -- If not found, choose a value non-deterministically
+              chosenValue <- generateValue t pos
+              setVar lens name chosenValue
+              when initOld $ setVar memOld name chosenValue
+              checkNameConstraints name pos
+              return chosenValue
+        
+rejectMapIndex pos idx = case idx of
+  Reference r -> throwRuntimeFailure (UnsupportedConstruct "map as an index") pos
+  _ -> return ()
+      
+evalMapSelection m args pos = do   
+  argsV <- mapM eval args  
+  Reference r <- eval m  
+  h <- use $ envMemory.memHeap
+  let (s, vals) = flattenMap h r
+  case M.lookup argsV vals of    -- Lookup a cached value
+    Just val -> wellDefined val
+    Nothing -> do                           -- If not found, look for an applicable definition
+      tc <- use envTypeContext
+      let mapType = exprType tc m    
+      definedValue <- checkMapDefinitions s mapType args argsV pos
+      case definedValue of
+        Just val -> do
+          setMapValue s argsV val
+          checkMapConstraints s mapType args argsV pos
+          forgetMapValue s argsV
+          return val
+        Nothing -> do                       -- If not found, choose a value non-deterministically
+          mapM_ (rejectMapIndex pos) argsV
+          let rangeType = exprType tc (gen $ MapSelection m args)
+          chosenValue <- generateValue rangeType pos
+          setMapValue s argsV chosenValue
+          checkMapConstraints s mapType args argsV pos
+          return chosenValue  
+        
+evalMapUpdate m args new pos = do
+  Reference r <- eval m
+  argsV <- mapM eval args
+  mapM_ (rejectMapIndex pos) argsV
+  newV <- eval new
+  MapValue repr <- readHeap r
+  let 
+    (newSource, newRepr) = case repr of 
+      Source _ -> (r, Derived r (M.singleton argsV newV))
+      Derived base override -> (base, Derived base (M.insert argsV newV override))
+  mapM_ incRefCountValue (M.elems $ stored newRepr)
+  envMemory.memHeap %= incRefCount newSource
+  allocate $ MapValue newRepr
+  
+evalIf cond e1 e2 = do
+  v <- eval cond
+  case v of
+    BoolValue True -> eval e1    
+    BoolValue False -> eval e2    
+      
+evalBinary op e1 e2 = do
+  left <- eval e1
+  case binOpLazy op left of
+    Just result -> return result
+    Nothing -> do
+      right <- eval e2
+      binOp (position e1) op left right
+
+-- | Finite domain      
+type Domain = [Value]      
+
+evalExists :: (Monad m, Functor m) => [Id] -> [IdType] -> Expression -> SourcePos -> Execution m Value      
+evalExists tv vars e pos = let Quantified Exists tv' vars' e' = node $ normalize (attachPos pos $ Quantified Exists tv vars e)
+  in evalExists' tv' vars' e'
+
+evalExists' :: (Monad m, Functor m) => [Id] -> [IdType] -> Expression -> Execution m Value    
+evalExists' tv vars e = do
+  localConstraints <- use $ envConstraints.amLocals
+  BoolValue <$> executeLocally (enterQuantified tv vars) (map fst vars) [] [] localConstraints evalWithDomains
+  where
+    evalWithDomains = do
+      doms <- domains e varNames
+      evalForEach varNames doms
+    -- | evalForEach vars domains: evaluate e for each combination of possible values of vars, drown from respective domains
+    evalForEach :: (Monad m, Functor m) => [Id] -> [Domain] -> Execution m Bool
+    evalForEach [] [] = unValueBool <$> eval e
+    evalForEach (var : vars) (dom : doms) = anyM (fixOne vars doms var) dom
+    -- | Fix the value of var to val, then evaluate e for each combination of values for the rest of vars
+    fixOne :: (Monad m, Functor m) => [Id] -> [Domain] -> Id -> Value -> Execution m Bool
+    fixOne vars doms var val = do
+      resetVar memLocals var val
+      evalForEach vars doms
+    varNames = map fst vars
+      
+{- Statements -}
+
+-- | Execute a basic statement
+-- (no jump, if or while statements allowed)
+exec :: (Monad m, Functor m) => Statement -> Execution m ()
+exec stmt = case node stmt of
+    Predicate specClause -> execPredicate specClause (position stmt)
+    Havoc ids -> execHavoc ids (position stmt)
+    Assign lhss rhss -> execAssign lhss rhss
+    Call lhss name args -> execCall name lhss args (position stmt)
+    CallForall name args -> return ()
+  >> collectGarbage
+  
+execPredicate specClause pos = do
+  b <- eval $ specExpr specClause
+  case b of 
+    BoolValue True -> return ()
+    BoolValue False -> throwRuntimeFailure (SpecViolation specClause) pos      
+    
+execHavoc names pos = do
+  mapM_ havoc names 
+  where
+    havoc name = do
+      tc <- use envTypeContext
+      let t = exprType tc . gen . Var $ name
+      definedValue <- checkNameDefinitions name t pos
+      case definedValue of
+        Just val -> do
+          resetAnyVar name val
+          checkNameConstraints name pos
+        Nothing -> do
+          chosenValue <- generateValue t pos
+          resetAnyVar name chosenValue
+          checkNameConstraints name pos
+    
+execAssign lhss rhss = do
+  rVals <- mapM eval rhss'
+  zipWithM_ resetAnyVar lhss' rVals
+  where
+    lhss' = map fst (zipWith simplifyLeft lhss rhss)
+    rhss' = map snd (zipWith simplifyLeft lhss rhss)
+    simplifyLeft (id, []) rhs = (id, rhs)
+    simplifyLeft (id, argss) rhs = (id, mapUpdate (gen $ Var id) argss rhs)
+    mapUpdate e [args] rhs = gen $ MapUpdate e args rhs
+    mapUpdate e (args1 : argss) rhs = gen $ MapUpdate e args1 (mapUpdate (gen $ MapSelection e args1) argss rhs)
+    
+execCall name lhss args pos = do
+  sig <- procSig name <$> use envTypeContext
+  execCallBySig sig lhss args pos
+    
+execCallBySig sig lhss args pos = do
+  defs <- gets $ lookupProcedure (psigName sig)
+  tc <- use envTypeContext
+  (sig', def) <- selectDef tc defs
+  let lhssExpr = map (attachPos (ctxPos tc) . Var) lhss
+  retsV <- execProcedure sig' def args lhssExpr `catchError` addFrame
+  zipWithM_ resetAnyVar lhss retsV
+  where
+    selectDef tc [] = return (assumePostconditions sig, dummyDef tc)
+    selectDef tc defs = do
+      i <- generate (`genIndex` length defs)
+      return (sig, defs !! i)
+    params = psigParams sig
+    paramConstraints tc = M.filterWithKey (\k _ -> k `elem` map itwId params) $ foldr asUnion M.empty $ map (extractConstraints tc . itwWhere) params
+    -- For procedures with no implementation: dummy definition that just havocs all modifiable globals
+    dummyDef tc = PDef {
+        pdefIns = map itwId (psigArgs sig),
+        pdefOuts = map itwId (psigRets sig),
+        pdefParamsRenamed = False,
+        pdefBody = ([], (M.fromList . toBasicBlocks . singletonBlock . gen . Havoc . psigModifies) sig),
+        pdefConstraints = paramConstraints tc,
+        pdefPos = noPos
+      }
+    addFrame err = addStackFrame (StackFrame pos (psigName sig)) err
+        
+-- | Execute program consisting of blocks starting from the block labeled label.
+-- Return the location of the exit point.
+execBlock :: (Monad m, Functor m) => Map Id [Statement] -> Id -> Execution m SourcePos
+execBlock blocks label = let
+  block = blocks ! label
+  statements = init block
+  in do
+    mapM exec statements
+    case last block of
+      Pos pos Return -> return pos
+      Pos _ (Goto lbs) -> tryOneOf blocks lbs
+  
+-- | tryOneOf blocks labels: try executing blocks starting with each of labels,
+-- until we find one that does not result in an assumption violation      
+tryOneOf :: (Monad m, Functor m) => Map Id [Statement] -> [Id] -> Execution m SourcePos        
+tryOneOf blocks (l : lbs) = execBlock blocks l `catchError` retry
+  where
+    retry err 
+      | failureKind err == Unreachable && not (null lbs) = tryOneOf blocks lbs
+      | otherwise = throwError err
+  
+-- | 'execProcedure' @sig def args lhss@ :
+-- Execute definition @def@ of procedure @sig@ with actual arguments @args@ and call left-hand sides @lhss@
+execProcedure :: (Monad m, Functor m) => PSig -> PDef -> [Expression] -> [Expression] -> Execution m [Value]
+execProcedure sig def args lhss = let 
+  ins = pdefIns def
+  outs = pdefOuts def
+  blocks = snd (pdefBody def)
+  localConstraints = pdefConstraints def
+  exitPoint pos = if pos == noPos 
+    then pdefPos def  -- Fall off the procedure body: take the procedure definition location
+    else pos          -- A return statement inside the body
+  execBody = do
+    checkPreconditions sig def    
+    pos <- exitPoint <$> execBlock blocks startLabel
+    checkPostonditions sig def pos    
+    mapM (eval . attachPos (pdefPos def) . Var) outs
+  in do
+    argsV <- mapM eval args
+    mem <- saveOld
+    executeLocally (enterProcedure sig def args lhss) (pdefLocals def) ins argsV localConstraints execBody `finally` restoreOld mem
+    
+{- Specs -}
+
+-- | Assert preconditions of definition def of procedure sig
+checkPreconditions sig def = mapM_ (exec . attachPos (pdefPos def) . Predicate . subst sig) (psigRequires sig)
+  where 
+    subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
+
+-- | Assert postconditions of definition def of procedure sig at exitPoint    
+checkPostonditions sig def exitPoint = mapM_ (exec . attachPos exitPoint . Predicate . subst sig) (psigEnsures sig)
+  where 
+    subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
+        
+-- | 'wellDefined' @val@ : throw an exception if @val@ is under construction
+wellDefined (CustomValue t n) | t == ucTypeName = throwInternalException $ UnderConstruction n
+wellDefined val = return val
+  
+-- | 'checkDefinitions' @typeGuard evalLocally myCode defs pos@ : return the result of the first applicable definition from @defs@;
+-- if none are applicable return 'Nothing', 
+-- unless an under construction value different from @myCode@ has been evaluated, in which case rethrow the UnderConstruction exception;
+-- use @typeGuard tv formalTypes@ to decide if a definition with type variables @tv@ and types of formals @formalTypes@ is applicable to the current invocation; 
+-- use @evalLocally formals@ to evaluate expressions inside a definition with arguments @formals@;
+-- @pos@ is the position of the definition invocation
+checkDefinitions :: (Monad m, Functor m) => ([Id] -> [Type] -> Bool) -> ([Id] -> Expression -> Execution m Value) -> Int -> [FDef] -> SourcePos -> Execution m (Maybe Value)
+checkDefinitions typeGuard evalLocally myCode defs pos = checkDefinitions' typeGuard evalLocally myCode Nothing defs pos 
+
+checkDefinitions' _ _ _ Nothing [] _ = return Nothing
+checkDefinitions' _ _ _ (Just code) [] _ = throwInternalException (UnderConstruction code)
+checkDefinitions' typeGuard evalLocally myCode mCode (FDef name tv formals guard body : defs) pos = tryDefinitions `catchError` ucHandler
+  where
+    tryDefinitions = do      
+      mVal <- applyDefinition (evalLocally (map fst formals)) guard body
+      case mVal of
+        Just val -> return mVal
+        Nothing -> checkDefinitions' typeGuard evalLocally myCode mCode defs pos 
+    ucHandler err = case rtfSource err of
+      InternalException (UnderConstruction code) -> if code == myCode
+        then checkDefinitions' typeGuard evalLocally myCode mCode defs pos
+        else checkDefinitions' typeGuard evalLocally myCode (Just code) defs pos
+      _ -> throwError err
+    applyDefinition evaluation guard body = if typeGuard tv (map snd formals)
+      then do
+        applicable <- case guard of
+          Pos _ TT -> return $ BoolValue True -- optimization for trivial guards
+          _ -> evaluation guard `catchError` addFrame
+        case applicable of
+          BoolValue False -> return Nothing
+          BoolValue True -> (Just <$> evaluation body) `catchError` addFrame
+      else return Nothing
+    addFrame = addStackFrame (StackFrame pos name)
+    
+-- | 'checkNameDefinitions' @name t pos@ : return a value for @name@ of type @t@ mentioned at @pos@, if there is an applicable definition
+checkNameDefinitions :: (Monad m, Functor m) => Id -> Type -> SourcePos -> Execution m (Maybe Value)    
+checkNameDefinitions name t pos = do
+  n <- gets $ lookupCustomCount ucTypeName
+  resetAnyVar name $ CustomValue ucTypeName n  
+  modify $ setCustomCount ucTypeName (n + 1)
+  defs <- fst <$> gets (lookupNameConstraints name)
+  let simpleDefs = [simpleDef | simpleDef <- defs, null $ fdefArgs simpleDef] -- Ignore forall-definition, they will be attached to the map value by checkNameConstraints
+  checkDefinitions (\_ _ -> True) (\_ -> eval) n simpleDefs pos `finally` cleanup n
+  where  
+    cleanup n = do
+      forgetAnyVar name
+      modify $ setCustomCount ucTypeName n
+        
+-- | 'checkMapDefinitions' @r t args actuals pos@ : return a value at index @actuals@ 
+-- in the map of type @t@ referenced by @r@ mentioned at @pos@, if there is an applicable definition 
+checkMapDefinitions :: (Monad m, Functor m) => Ref -> Type -> [Expression] -> [Value] -> SourcePos -> Execution m (Maybe Value)    
+checkMapDefinitions r t args actuals pos = do
+  n <- gets $ lookupCustomCount ucTypeName
+  setMapValue r actuals $ CustomValue ucTypeName n  
+  modify $ setCustomCount ucTypeName (n + 1)  
+  defs <- fst <$> gets (lookupMapConstraints r)
+  tc <- use envTypeContext
+  let argTypes = map (exprType tc) args
+  checkDefinitions (typeGuard argTypes) evalLocally n defs pos `finally` cleanup n
+  where  
+    sig = fsigFromType t
+    typeGuard argTypes tv formalTypes = isJust $ unifier tv formalTypes argTypes
+    evalLocally formals expr = if null formals
+        then eval expr
+        else executeLocally (enterFunction sig formals args) formals formals actuals M.empty (eval expr)
+    cleanup n = do
+      forgetMapValue r actuals
+      modify $ setCustomCount ucTypeName n      
+
+-- | 'applyConstraint' @name evaluation guard body pos@ : 
+-- check for an entity @name@ that @guard@ ==> @body@, using @evaluation@ to evaluate both @guard@ and @body@;
+-- (@pos@ is the position of the constraint invocation)      
+applyConstraint name evaluation guard body pos = do
+  applicable <- case guard of
+    Pos _ TT -> return $ BoolValue True -- optimization for trivial guards
+    _ -> evaluation guard `catchError` addFrame
+  case applicable of
+    BoolValue True -> do
+      satisfied <- evaluation body `catchError` addFrame
+      case satisfied of 
+        BoolValue True -> return ()
+        BoolValue False -> throwRuntimeFailure (SpecViolation $ SpecClause Axiom True body) pos
+    BoolValue False -> return ()
+  where
+    addFrame = addStackFrame (StackFrame pos name)
+    
+-- | 'checkNameConstraints' @name pos@: assume all constraints of entity @name@ mentioned at @pos@;
+-- is @name@ is of map type, attach all its forall-definitions and forall-contraints to the corresponding reference 
+checkNameConstraints name pos = do
+  (defs, constraints) <- gets $ lookupNameConstraints name
+  mapM_ checkConstraint constraints
+  mapM_ attachDefinition defs
+  where
+    checkConstraint (FDef _ [] [] guard body) = applyConstraint name eval guard body pos -- Simple constraint: assume it
+    checkConstraint constr = do             -- Forall-constraint: attach to the map value
+      Reference r <- evalVar name pos
+      modify $ addMapConstraint r constr
+    attachDefinition (FDef _ [] [] _ _) = return ()  -- Simple definition: ignore
+    attachDefinition def = do                     -- Forall definition: attach to the map value
+      Reference r <- evalVar name pos
+      modify $ addMapDefinition r def
+      
+-- | 'checkMapConstraints' @r t args actuals pos@ : assume all constraints for the value at index @actuals@ 
+-- in the map of type @t@ referenced by @r@ mentioned at @pos@
+checkMapConstraints r t args actuals pos = do
+  constraints <- snd <$> gets (lookupMapConstraints r)
+  tc <- use envTypeContext
+  let argTypes = map (exprType tc) args
+  let typeGuard tv formalTypes = isJust $ unifier tv formalTypes argTypes
+  mapM_ (checkConstraint typeGuard) constraints        
+  where
+    checkConstraint typeGuard (FDef name tv formals guard body) = if typeGuard tv (map snd formals)
+      then applyConstraint name (evalLocally (map fst formals)) guard body pos
+      else return ()
+    evalLocally formalNames expr = do
+      let sig = fsigFromType t
+      executeLocally (enterFunction sig formalNames args) formalNames formalNames actuals M.empty (eval expr)
+
+{- Preprocessing -}
+
+-- | Collect procedure implementations, and constant/function/global variable constraints
+preprocess :: (Monad m, Functor m) => Program -> SafeExecution m ()
+preprocess (Program decls) = mapM_ processDecl decls
+  where
+    processDecl decl = case node decl of
+      FunctionDecl name _ args _ mBody -> processFunction name args mBody
+      ProcedureDecl name _ args rets _ (Just body) -> processProcedureBody name (position decl) (map noWhere args) (map noWhere rets) body
+      ImplementationDecl name _ args rets bodies -> mapM_ (processProcedureBody name (position decl) args rets) bodies
+      AxiomDecl expr -> processAxiom expr
+      VarDecl vars -> mapM_ processAxiom (map itwWhere vars)
+      _ -> return ()
+  
+processFunction name args mBody = do
+  sig <- funSig name <$> use envTypeContext
+  envTypeContext %= \tc -> tc { ctxConstants = M.insert (functionConst name) (fsigType sig) (ctxConstants tc) }  
+  case mBody of
+    Nothing -> return ()
+    Just body -> modify $ addGlobalDefinition (functionConst name) (FDef name (fsigTypeVars sig) formals (conjunction []) body)
+  where    
+    formals = over (mapped._1) formalName args
+    formalName Nothing = dummyFArg 
+    formalName (Just n) = n    
+    
+processProcedureBody name pos args rets body = do
+  tc <- use envTypeContext
+  let params = psigParams $ procSig name tc
+  let paramsRenamed = map itwId params /= (argNames ++ retNames)    
+  let flatBody = (map (mapItwType (resolve tc)) (concat $ fst body), M.fromList (toBasicBlocks $ snd body))
+  let allLocals = params ++ fst flatBody
+  let localConstraints = M.filterWithKey (\k _ -> k `elem` map itwId allLocals) $ foldr asUnion M.empty $ map (extractConstraints tc . itwWhere) allLocals
+  modify $ addProcedureImpl name (PDef argNames retNames paramsRenamed flatBody localConstraints pos) 
+  where
+    argNames = map fst args
+    retNames = map fst rets
+
+processAxiom expr = do
+  tc <- use envTypeContext
+  envConstraints.amGlobals %= (`asUnion` extractConstraints tc expr)
+  
+{- Constant and function constraints -}
+
+-- | 'extractConstraints' @bExpr@ : extract definitions and constraints from @bExpr@
+extractConstraints :: Context -> Expression -> AbstractStore
+extractConstraints tc bExpr = extractConstraints' tc [] (negationNF bExpr)
+
+extractConstraints' :: Context -> [Expression] -> Expression -> AbstractStore
+extractConstraints' tc guards bExpr = case (node bExpr) of
+  Quantified Forall tv vars bExpr' -> extractConstraints' (enterQuantified tv vars tc) guards bExpr'
+  Quantified Exists _ _ _ -> M.empty
+  BinaryExpression And bExpr1 bExpr2 -> let
+    constraints1 = extractConstraints' tc guards bExpr1
+    constraints2 = extractConstraints' tc guards bExpr2
+    in constraints1 `asUnion` constraints2
+  BinaryExpression Or bExpr1 bExpr2 -> let
+    constraints1 = extractConstraints' tc ((negationNF $ enot bExpr1) : guards) bExpr2
+    constraints2 = extractConstraints' tc ((negationNF $ enot bExpr2) : guards) bExpr1
+    in constraints1 `asUnion` constraints2
+  BinaryExpression Eq expr1 expr2 -> let
+    defs1 = extractDefsAtomic expr1 expr2
+    defs2 = extractDefsAtomic expr2 expr1
+    constraints = extractConstraintsAtomic
+    in foldr1 asUnion [defs1, defs2, constraints]
+  _ -> extractConstraintsAtomic
+  where
+    fvExpr = freeVars bExpr
+    fvGuards = concatMap freeVars guards
+    allFV = fvExpr ++ fvGuards
+    tv = ctxTypeVars tc
+    vars = M.toList $ ctxIns tc
+    usedVars = [(v, t) | (v, t) <- vars, v `elem` allFV]
+  
+    extractDefsAtomic lhs rhs = case node lhs of
+      Var name -> addDefFor name [] rhs
+      MapSelection (Pos _ (Var name)) args -> addDefFor name args rhs
+      Application name args -> addDefFor (functionConst name) args rhs
+      _ -> M.empty
+    addDefFor name args rhs = let
+        argTypes = map (exprType tc) args
+        (formals, argGuards) = unzip $ extractArgs (map fst usedVars) args
+        allGuards = concat argGuards ++ guards
+        extraVars = [(v, t) | (v, t) <- usedVars, v `notElem` formals]
+      in if length formals == length args && null extraVars -- Only possible if all arguments are simple and there are no extra variables
+        then M.singleton name ([FDef name tv (zip formals argTypes) (conjunction allGuards) rhs], [])
+        else M.empty
+    
+    extractConstraintsAtomic = case usedVars of -- This is a compromise: quantified expressions constrain names they mention of any arity but zero (ToDo: think about it)
+      [] -> foldr asUnion M.empty $ map addSimpleConstraintFor fvExpr
+      _ -> foldr asUnion M.empty $ map addForallConstraintFor (freeSelections bExpr ++ over (mapped._1) functionConst (applications bExpr))
+    addSimpleConstraintFor name = M.singleton name ([], [FDef name [] [] (conjunction guards) bExpr])
+    addForallConstraintFor (name, args) = let
+        argTypes = map (exprType tc) args
+        (formals, argGuards) = unzip $ extractArgs (map fst usedVars) args
+        allArgGuards = concat argGuards
+        extraVars = [(v, t) | (v, t) <- usedVars, v `notElem` formals]
+        constraint = if null extraVars
+          then conjunction guards |=>| bExpr
+          else attachPos (position bExpr) $ Quantified Forall tv extraVars (conjunction guards |=>| bExpr) -- outer guards are inserted into the body, because they might contain extraVars
+      in if length formals == length args -- Only possible if all arguments are simple
+        then M.singleton name ([], [FDef name tv (zip formals argTypes) (conjunction allArgGuards) constraint])
+        else M.empty
+            
+-- | 'extractArgs' @vars args@: extract simple arguments from @args@;
+-- an argument is simple if it is either one of variables in @vars@ or does not contain any of @vars@;
+-- in the latter case the argument is represented as a fresh name and a constraint
+extractArgs :: [Id] -> [Expression] -> [(Id, [Expression])]
+extractArgs vars args = foldl extractArg [] (zip args [0..])
+  where
+    extractArg res ((Pos p e), i) = let 
+      x = freshArgName i 
+      xExpr = attachPos p $ Var x
+      in res ++
+        case e of
+          Var arg -> if arg `elem` vars
+            then if arg `elem` map fst res
+              then [(x, [xExpr |=| Pos p e])]      -- Bound variable that already occurred: use fresh variable as formal, add equality guard
+              else [(arg, [])]                     -- New bound variable: use variable name as formal, no additional guards
+            else [(x, [xExpr |=| Pos p e])]        -- Constant: use fresh variable as formal, add equality guard
+          _ -> if null $ freeVars (Pos p e) `intersect` nonfixedBV
+                  then [(x, [xExpr |=| Pos p e])]  -- Expression where all bound variables are already fixed: use fresh variable as formal, add equality guard
+                  else []                          -- Expression involving non-fixed bound variables: not a simple argument, omit
+    freshArgName i = nonIdChar : show i
+    varArgs = [v | (Pos p (Var v)) <- args]
+    nonfixedBV = vars \\ varArgs    
+       
+{- Quantification -}
+
+-- | Sets of interval constraints on integer variables
+type IntervalConstraints = Map Id Interval
+            
+-- | The set of domains for each variable in vars, outside which boolean expression boolExpr is always false.
+-- Fails if any of the domains are infinite or cannot be found.
+domains :: (Monad m, Functor m) => Expression -> [Id] -> Execution m [Domain]
+domains boolExpr vars = do
+  initC <- foldM initConstraints M.empty vars
+  finalC <- inferConstraints boolExpr initC 
+  forM vars (domain finalC)
+  where
+    initConstraints c var = do
+      tc <- use envTypeContext
+      qbound <- use envQBound
+      case M.lookup var (allVars tc) of
+        Just BoolType         -> return c
+        Just (MapType _ _ _)  -> throwRuntimeFailure (UnsupportedConstruct "quantification over a map") (position boolExpr)
+        Just t                -> return $ M.insert var (defaultDomain qbound t) c        
+    defaultDomain qbound t = case qbound of
+      Nothing -> top
+      Just n -> let 
+        (lower, upper) = case t of
+          IntType -> intInterval n
+          IdType _ _ -> natInterval n
+        in Interval (Finite lower) (Finite upper)
+    domain c var = do
+      tc <- use envTypeContext
+      case M.lookup var (allVars tc) of
+        Just BoolType -> return $ map BoolValue [True, False]
+        Just t -> do
+          case c ! var of
+            int | isBottom int -> return []
+            Interval (Finite l) (Finite u) -> return $ map (valueFromInteger t) [l..u]
+            int -> throwRuntimeFailure (InfiniteDomain var int) (position boolExpr)
+
+-- | Starting from initial constraints, refine them with the information from boolExpr,
+-- until fixpoint is reached or the domain for one of the variables is empty.
+-- This function terminates because the interval for each variable can only become smaller with each iteration.
+inferConstraints :: (Monad m, Functor m) => Expression -> IntervalConstraints -> Execution m IntervalConstraints
+inferConstraints boolExpr constraints = do
+  constraints' <- foldM refineVar constraints (M.keys constraints)
+  if bot `elem` M.elems constraints'
+    then return $ M.map (const bot) constraints'  -- if boolExpr does not have a satisfying assignment to one variable, then it has none to all variables
+    else if constraints == constraints'
+      then return constraints'                    -- if a fixpoint is reached, return it
+      else inferConstraints boolExpr constraints' -- otherwise do another iteration
+  where
+    refineVar :: (Monad m, Functor m) => IntervalConstraints -> Id -> Execution m IntervalConstraints
+    refineVar c id = do
+      int <- inferInterval boolExpr c id
+      return $ M.insert id (meet (c ! id) int) c 
+
+-- | Infer an interval for variable x, outside which boolean expression booExpr is always false, 
+-- assuming all other quantified variables satisfy constraints;
+-- boolExpr has to be in negation-prenex normal form.
+inferInterval :: (Monad m, Functor m) => Expression -> IntervalConstraints -> Id -> Execution m Interval
+inferInterval boolExpr constraints x = (case node boolExpr of
+  FF -> return bot
+  BinaryExpression And be1 be2 -> liftM2 meet (inferInterval be1 constraints x) (inferInterval be2 constraints x)
+  BinaryExpression Or be1 be2 -> liftM2 join (inferInterval be1 constraints x) (inferInterval be2 constraints x)
+  BinaryExpression Eq ae1 ae2 -> do
+    (a, b) <- toLinearForm (ae1 |-| ae2) constraints x
+    if 0 <: a && 0 <: b
+      then return top
+      else return $ -b // a
+  BinaryExpression Leq ae1 ae2 -> do
+    (a, b) <- toLinearForm (ae1 |-| ae2) constraints x
+    if isBottom a || isBottom b
+      then return bot
+      else if 0 <: a && not (isBottom (meet b nonPositives))
+        then return top
+        else return $ join (lessEqual (-b // meet a positives)) (greaterEqual (-b // meet a negatives))
+  BinaryExpression Ls ae1 ae2 -> inferInterval (ae1 |<=| (ae2 |-| num 1)) constraints x
+  BinaryExpression Geq ae1 ae2 -> inferInterval (ae2 |<=| ae1) constraints x
+  BinaryExpression Gt ae1 ae2 -> inferInterval (ae2 |<=| (ae1 |-| num 1)) constraints x
+  -- Quantifier can only occur here if it is alternating with the enclosing one, hence no domain can be inferred 
+  _ -> return top
+  ) `catchError` handleNotLinear
+  where      
+    lessEqual int | isBottom int = bot
+                  | otherwise = Interval NegInf (upper int)
+    greaterEqual int  | isBottom int = bot
+                      | otherwise = Interval (lower int) Inf
+    handleNotLinear err = case rtfSource err of
+      InternalException NotLinear -> return top
+      _ -> throwError err                      
+
+-- | Linear form (A, B) represents a set of expressions a*x + b, where a in A and b in B
+type LinearForm = (Interval, Interval)
+
+-- | If possible, convert arithmetic expression aExpr into a linear form over variable x,
+-- assuming all other quantified variables satisfy constraints.
+toLinearForm :: (Monad m, Functor m) => Expression -> IntervalConstraints -> Id -> Execution m LinearForm
+toLinearForm aExpr constraints x = case node aExpr of
+  Numeral n -> return (0, fromInteger n)
+  Var y -> if x == y
+    then return (1, 0)
+    else case M.lookup y constraints of
+      Just int -> return (0, int)
+      Nothing -> const aExpr
+  Application name args -> if null $ M.keys constraints `intersect` freeVars aExpr
+    then const aExpr
+    else throwInternalException NotLinear
+  MapSelection m args -> if null $ M.keys constraints `intersect` freeVars aExpr
+    then const aExpr
+    else throwInternalException NotLinear
+  Old e -> old $ toLinearForm e constraints x
+  UnaryExpression Neg e -> do
+    (a, b) <- toLinearForm e constraints x
+    return (-a, -b)
+  BinaryExpression op e1 e2 -> do
+    left <- toLinearForm e1 constraints x
+    right <- toLinearForm e2 constraints x 
+    combineBinOp op left right
+  where
+    const e = do
+      v <- eval e
+      case v of
+        IntValue n -> return (0, fromInteger n)
+    combineBinOp Plus   (a1, b1) (a2, b2) = return (a1 + a2, b1 + b2)
+    combineBinOp Minus  (a1, b1) (a2, b2) = return (a1 - a2, b1 - b2)
+    combineBinOp Times  (a, b)   (0, k)   = return (k * a, k * b)
+    combineBinOp Times  (0, k)   (a, b)   = return (k * a, k * b)
+    combineBinOp _ _ _ = throwInternalException NotLinear
+    
+{- Map equality -}
+
+-- | 'evalEquality' @v1 v2@ : Evaluate @v1 == v2@
+evalEquality :: (Monad m, Functor m) => Value -> Value -> Execution m Value
+evalEquality v1 v2 = do
+  h <- use $ envMemory.memHeap
+  case objectEq h v1 v2 of
+    Just b -> return $ BoolValue b
+    Nothing -> decideEquality v1 v2  -- No evidence yet if two maps are equal or not, make a non-deterministic choice
+  where
+    decideEquality (Reference r1) (Reference r2) = do
+      h <- use $ envMemory.memHeap
+      let (s1, vals1) = flattenMap h r1
+      let (s2, vals2) = flattenMap h r2
+      mustEqual <- generate genBool                     -- Decide if maps should be considered equal right away
+      if mustEqual
+        then do makeEq v1 v2; return $ BoolValue True               -- Make the maps equal and return True
+        else if s1 == s2                                            -- Otherwise: if the maps come from the same source
+          then decideOverrideEquality r1 vals1 r2 vals2               -- Then the difference must be in overrides
+          else if mustAgree h vals1 vals2                             -- Otherwise: if the difference cannot be in overrides
+            then do makeSourceNeq s1 s2; return $ BoolValue False       -- Then make the sources incompatible and return False
+            else do                                                     -- Otherwise we can freely choose if the difference is in the source or in the overrides
+              compareOverrides <- generate genBool                      -- Make a choice
+              if compareOverrides
+                then decideOverrideEquality r1 vals1 r2 vals2           -- decide equality based on overrides
+                else do makeSourceNeq s1 s2; return $ BoolValue False   -- otherwise make the sources incompatible and return False
+    decideOverrideEquality r1 vals1 r2 vals2 = 
+      let diff = if hasMapValues $ vals1 `M.intersection` vals2                               -- If there are maps stored at common indexes
+                    then vals1 `M.union` vals2                                                -- then even values at a common index might be different
+                    else (vals2 `M.difference` vals1) `M.union` (vals1 `M.difference` vals2)  -- otherwise only values at non-shared indexes might be different
+      in do
+        (i, val) <- (`M.elemAt` diff) <$> generate (`genIndex` M.size diff) -- Choose an index at which the values might be different
+        val1 <- lookupStored r1 i val
+        val2 <- lookupStored r2 i val
+        BoolValue answer <- evalEquality val1 val2
+        when answer $ makeEq v1 v2
+        return $ BoolValue answer 
+    hasMapValues m
+      | M.null m  = False
+      | otherwise = case M.findMin m of
+        (_, Reference _) -> True
+        _ -> False      
+    lookupStored r i template = do
+      h <- use $ envMemory.memHeap
+      let (s, vals) = flattenMap h r    
+      case M.lookup i vals of
+        Just v -> return v
+        Nothing -> do
+          v <- generateValueLike template
+          setMapValue s i v
+          return v
+    makeSourceNeq s1 s2 = do
+      setMapValue s1 [special s1, special s2] (special s1)
+      setMapValue s2 [special s1, special s2] (special s2)
+    special r = CustomValue refIdTypeName $ fromIntegral r
+          
+-- | Ensure that two compatible values are equal
+makeEq :: (Monad m, Functor m) => Value -> Value -> Execution m ()
+makeEq (Reference r1) (Reference r2) = do
+  h <- use $ envMemory.memHeap
+  let (s1, vals1) = flattenMap h r1
+  let (s2, vals2) = flattenMap h r2
+  zipWithM_ makeEq (M.elems $ vals1 `M.intersection` vals2) (M.elems $ vals2 `M.intersection` vals1) -- Enforce that the values at shared indexes are equal
+  if s1 == s2
+    then do -- Same source; compatible, but nonequal overrides
+      mapM_ (uncurry $ setMapValue s1) (M.toList $ vals2 `M.difference` vals1) -- Store values only defined in r2 in the source
+      mapM_ (uncurry $ setMapValue s1) (M.toList $ vals1 `M.difference` vals2) -- Store values only defined in r1 in the source
+    else do -- Different sources
+      Reference newSource <- allocate . MapValue . Source $ vals1 `M.union` vals2
+      mapM_ decRefCountValue (M.elems (vals2 `M.intersection` vals1)) -- Take care of references from vals2 that are no longer used
+      derive r1 newSource
+      derive r2 newSource
+      mergeConstraints s1 s2 newSource
+  where
+    derive r newSource = do
+      deriveBaseOf r newSource M.empty
+      envMemory.memHeap %= update r (MapValue (Derived newSource M.empty))      
+      envMemory.memHeap %= incRefCount newSource      
+    deriveBaseOf r newSource diffR = do
+      MapValue repr <- readHeap r
+      case repr of
+        Source _ -> return ()
+        Derived base override -> do
+          let diffBase = override `M.union` diffR -- The difference between base and newSource
+          h <- use $ envMemory.memHeap
+          let vals = mapValues h base
+          deriveBaseOf base newSource diffBase
+          newVals <- foldM addMissing (vals `M.intersection` diffBase) (M.toList $ diffBase `M.difference` vals) -- Choose arbitrary values for all keys in diffBase that are not defined for base
+          envMemory.memHeap %= update base (MapValue (Derived newSource newVals))
+          envMemory.memHeap %= incRefCount newSource
+          envMemory.memHeap %= decRefCount base
+    addMissing vals (key, oldVal) = do
+      newVal <- generateValueLike oldVal
+      incRefCountValue newVal
+      return $ M.insert key newVal vals
+    mergeConstraints s1 s2 newSource = do
+      (defs1, constraints1) <- gets $ lookupMapConstraints s1
+      (defs2, constraints2) <- gets $ lookupMapConstraints s2
+      envConstraints.amHeap %= M.insert newSource (defs1 ++ defs2, constraints1 ++ constraints2)
+makeEq (MapValue _) (MapValue _) = internalError "Attempt to call makeEq on maps directly" 
+makeEq _ _ = return ()  

@@ -11,55 +11,46 @@ -- | Negation normal form of a Boolean expression:
 -- no negation above boolean connectives, quantifiers or relational operators;
 -- no boolean connectives except @&&@ and @||@
-negationNF :: Context -> Expression -> Expression
-negationNF c boolExpr = case node boolExpr of
+negationNF :: Expression -> Expression
+negationNF boolExpr = case node boolExpr of
   UnaryExpression Not e -> case node e of
-    UnaryExpression Not e' -> negationNF c e'
-    BinaryExpression And e1 e2 -> negationNF c (enot e1) ||| negationNF c (enot e2)
-    BinaryExpression Or e1 e2 -> negationNF c (enot e1) |&| negationNF c (enot e2)
-    BinaryExpression Implies e1 e2 -> negationNF c e1 |&| negationNF c (enot e2)
-    BinaryExpression Equiv e1 e2 -> (negationNF c e1 |&| negationNF c (enot e2)) |&| (negationNF c (enot e1) |&| negationNF c e2)
-    BinaryExpression Eq e1 e2 -> case exprType c e1 of
-      BoolType -> negationNF c (enot (e1 |<=>| e2))
-      _ -> e1 |!=| e2
-    BinaryExpression Neq e1 e2 -> case exprType c e1 of
-      BoolType -> negationNF c (e1 |<=>| e2)
-      _ -> e1 |=| e2
+    UnaryExpression Not e' -> negationNF e'
+    BinaryExpression And e1 e2 -> negationNF (enot e1) ||| negationNF (enot e2)
+    BinaryExpression Or e1 e2 -> negationNF (enot e1) |&| negationNF (enot e2)
+    BinaryExpression Implies e1 e2 -> negationNF e1 |&| negationNF (enot e2)
+    BinaryExpression Equiv e1 e2 -> (negationNF e1 |&| negationNF (enot e2)) |&| (negationNF (enot e1) |&| negationNF e2)
+    BinaryExpression Eq e1 e2 -> e1 |!=| e2
+    BinaryExpression Neq e1 e2 -> e1 |=| e2
     BinaryExpression Leq ae1 ae2 -> ae1 |>| ae2
     BinaryExpression Ls ae1 ae2 -> ae1 |>=| ae2
     BinaryExpression Geq ae1 ae2 -> ae1 |<| ae2
     BinaryExpression Gt ae1 ae2 -> ae1 |<=| ae2
-    Quantified Forall tv vars e' -> attachPos (position e) $ Quantified Exists tv vars (negationNF (enterQuantified tv vars c) (enot e'))
-    Quantified Exists tv vars e' -> attachPos (position e) $ Quantified Forall tv vars (negationNF (enterQuantified tv vars c) (enot e'))
-    _ -> boolExpr
-  BinaryExpression Implies e1 e2 -> negationNF c (enot e1) ||| negationNF c e2
-  BinaryExpression Equiv e1 e2 -> (negationNF c (enot e1) ||| negationNF c e2) |&| (negationNF c e1 ||| negationNF c (enot e2))
-  BinaryExpression Eq e1 e2 -> case exprType c e1 of
-    BoolType -> negationNF c (e1 |<=>| e2)
-    _ -> boolExpr
-  BinaryExpression Neq e1 e2 -> case exprType c e1 of
-    BoolType -> negationNF c (enot (e1 |<=>| e2))
+    Quantified Forall tv vars e' -> attachPos (position e) $ Quantified Exists tv vars (negationNF (enot e'))
+    Quantified Exists tv vars e' -> attachPos (position e) $ Quantified Forall tv vars (negationNF (enot e'))
     _ -> boolExpr
-  BinaryExpression op e1 e2 | op == And || op == Or -> inheritPos2 (BinaryExpression op) (negationNF c e1) (negationNF c e2)    
-  Quantified qop tv vars e -> attachPos (position boolExpr) $ Quantified qop tv vars (negationNF (enterQuantified tv vars c) e)
+  BinaryExpression Implies e1 e2 -> negationNF (enot e1) ||| negationNF e2
+  BinaryExpression Equiv e1 e2 -> (negationNF (enot e1) ||| negationNF e2) |&| (negationNF e1 ||| negationNF (enot e2))
+  BinaryExpression op e1 e2 | op == And || op == Or -> inheritPos2 (BinaryExpression op) (negationNF e1) (negationNF e2)    
+  Quantified qop tv vars e -> attachPos (position boolExpr) $ Quantified qop tv vars (negationNF e)
   _ -> boolExpr
 
 -- | Prenex normal form of a Boolean expression:
 -- all quantifiers are pushed to the outside and any two quantifiers of the same kind in a row are glued together.
 -- Requires expression to be in the negation normal form.  
 prenexNF :: Expression -> Expression
-prenexNF boolExpr = (glue . rawPrenex) boolExpr
+prenexNF boolExpr = glue $ rawPrenex boolExpr
   where
     -- | Push all quantifiers to the front
     rawPrenex boolExpr = case node boolExpr of
       -- We only have to consider && and || because boolExpr is in negation normal form
       BinaryExpression op e1 e2 | op == And || op == Or -> merge (++ "1") (++ "2") op (rawPrenex e1) (rawPrenex e2)
+      Quantified qop tv vars e -> attachPos (position boolExpr) $ Quantified qop tv vars (rawPrenex e)
       _ -> boolExpr
     merge r1 r2 op e1 e2 = attachPos (position e1) (merge' r1 r2 op e1 e2)
-    merge' r1 r2 op (Pos _ (Quantified qop tv vars e)) e2 = case renameBound r1 (Quantified qop tv vars e) of
-      Quantified qop tv' vars' e' -> Quantified qop tv' vars' (merge r1 r2 op e' e2)
-    merge' r1 r2 op e1 (Pos _ (Quantified qop tv vars e)) = case renameBound r2 (Quantified qop tv vars e) of
-      Quantified qop tv' vars' e' -> Quantified qop tv' vars' (merge r1 r2 op e1 e')
+    merge' r1 r2 op (Pos _ be1@(Quantified _ _ _ _)) e2 = let Quantified qop tv' vars' e' = renameBound r1 be1
+      in Quantified qop tv' vars' (merge r1 r2 op e' e2)
+    merge' r1 r2 op e1 (Pos _ be2@(Quantified _ _ _ _)) = let Quantified qop tv' vars' e' = renameBound r2 be2
+      in Quantified qop tv' vars' (merge r1 r2 op e1 e')
     merge' _ _ op e1 e2 = BinaryExpression op e1 e2
     -- | Rename all bound variables and type variables in a quantified expression with a renaming function r
     renameBound r (Quantified qop tv vars e) = Quantified qop (map r tv) (map (renameVar r tv) vars) (exprSubst (varBinding r (map fst vars)) e)
@@ -76,5 +67,5 @@       _ -> boolExpr
 
 -- | Negation and prenex normal form of a Boolean expression
-normalize :: Context -> Expression -> Expression      
-normalize c boolExpr = prenexNF $ negationNF c boolExpr
+normalize :: Expression -> Expression      
+normalize boolExpr = prenexNF $ negationNF boolExpr

@@ -104,7 +104,7 @@   do
     x <- identifier
     xs <- option [] typeCtorArgs
-    return $ Instance x [] : xs,
+    return $ IdType x [] : xs,
   do
     x <- mapType
     return [x]
@@ -118,7 +118,7 @@   do
     id <- identifier
     args <- option [] typeCtorArgs
-    return $ Instance id args
+    return $ IdType id args
   ] <?> "type"
 
 {- Expressions -}

@@ -7,6 +7,10 @@   exprDoc,
   statementDoc,
   declDoc,
+  -- * Functions and procedures
+  fdefDoc,
+  constraintSetDoc,
+  abstractStoreDoc,
   -- * Utility
   newline,
   vsep,
@@ -17,12 +21,14 @@   optionMaybe,
   unOpDoc,
   binOpDoc,
-  sigDoc
+  sigDoc,
+  nestDef
 ) where
 
 import Language.Boogie.AST
 import Language.Boogie.Position
 import Language.Boogie.Tokens
+import Language.Boogie.Util
 import Data.Maybe
 import Data.Map (Map, (!))
 import qualified Data.Map as M
@@ -63,7 +69,7 @@ typeDoc (MapType fv domains range) = typeArgsDoc fv <> 
   brackets (commaSep (map typeDoc domains)) <+>
   typeDoc range
-typeDoc (Instance id args) = text id <+> hsep (map typeDoc args)
+typeDoc (IdType id args) = text id <+> hsep (map typeDoc args)
 
 instance Show Type where show t = show (typeDoc t)
 
@@ -276,6 +282,27 @@   text "returns" <+>
   parens (commaSep (map idTypeDoc rets)) $+$
   vsep (map bodyDoc bodies)
+  
+{- Functions and procedures -}
+
+-- | 'fdefDoc' @isDef fdef@ : @fdef@ pretty-printed as definition if @isDef@ and as constraint otherwise
+fdefDoc :: Bool -> FDef -> Doc
+fdefDoc isDef (FDef name tv formals guard expr) = 
+  text name <>
+  (if null tv then empty else angles (commaSep (map text tv))) <+> 
+  (if null formals then empty else parens (commaSep (map idTypeDoc formals))) <+> 
+  (if node guard == TT then empty else brackets (exprDoc guard)) <+> 
+  (if isDef then text "=" else text ":") <+>
+  exprDoc expr
+
+-- | Pretty-printed constraint set  
+constraintSetDoc :: ConstraintSet -> Doc   
+constraintSetDoc cs = vsep (map (fdefDoc True) (fst cs)) $+$ vsep (map (fdefDoc False) (snd cs))
+
+-- | Pretty-printed abstract store
+abstractStoreDoc :: AbstractStore -> Doc
+abstractStoreDoc vars = vsep $ map varDoc (M.toList vars)
+  where varDoc (name, cs) = text name $+$ nestDef (constraintSetDoc cs)  
   
 {- Misc -}
   

@@ -1,301 +0,0 @@--- | Automated specification-based tester
-module Language.Boogie.Tester (
-  -- * Running tests
-  testProgram,
-  testSessionSummary,
-  -- * Configurng test sessions
-  TestSettings (..),
-  defaultGenericTypeRange,
-  defaultMapTypeRange,
-  ExhaustiveSettings (..),
-  RandomSettings (..),
-  -- * Testing results
-  Outcome (..),
-  outcomeDoc,
-  TestCase (..),
-  testCaseDoc,
-  Summary (..),
-  summaryDoc
-) where
-
-import Language.Boogie.AST
-import Language.Boogie.Util
-import Language.Boogie.Position
-import Language.Boogie.TypeChecker
-import Language.Boogie.Tokens
-import Language.Boogie.PrettyPrinter
-import Language.Boogie.Interpreter
-import Language.Boogie.DataFlow
-import System.Random
-import Data.Maybe
-import Data.List
-import Data.Map (Map, (!))
-import qualified Data.Map as M
-import Control.Monad.Error
-import Control.Applicative
-import Control.Monad.State
-import Text.PrettyPrint
-
-{- Interface -}
-    
--- | 'testProgram' @settings p tc procNames@ : 
--- Test all implementations of all procedures @procNames@ from program @p@ in type context @tc@;
--- requires that all @procNames@ exist in @tc@
-testProgram :: TestSettings s => s -> Program -> Context -> [Id] -> [TestCase]
-testProgram settings p tc procNames = evalState testExecution (settings, initEnvironment)
-  where
-    initEnvironment = emptyEnv { envTypeContext = tc }
-    testExecution = do
-      changeState snd (mapSnd . const) $ collectDefinitions p
-      concat <$> forM procNames testProcedure
-    -- | Test all implementations of procedure name
-    testProcedure name = do
-      sig <- gets (procSig name . envTypeContext . snd) 
-      defs <- gets (lookupProcedure name . snd)
-      concat <$> forM defs (testImplementation sig)
-      
--- | Summary of a set of test cases   
-testSessionSummary :: [TestCase] -> Summary
-testSessionSummary tcs = let 
-  passing = [ x | x@(TestCase _ _ _ _ Pass)         <- tcs ]
-  failing = [ x | x@(TestCase _ _ _ _ (Fail _))     <- tcs ]
-  invalid = [ x | x@(TestCase _ _ _ _ (Invalid _))  <- tcs ]
-  in Summary {
-    sPassCount = length passing,
-    sFailCount = length failing,
-    sInvalidCount = length invalid,  
-    sUniqueFailures = nubBy equivalent failing
-  }
-            
-{- Testing session parameters -}
-
--- | Test session parameters
-class TestSettings s where
-  -- | How should input values for an integer variable be generated?
-  generateIntInput :: State s [Integer]
-  -- | How should input values for a boolean variable be generated?
-  generateBoolInput :: State s [Bool]
-  -- | How should input values for several variables be combined?
-  combineInputs :: (a -> State s [b]) -> [a] -> State s [[b]]
-  -- | Settings for generating map domains (always exhaustive)
-  mapDomainSettings :: s -> ExhaustiveSettings
-  -- | Range of instances for a type parameter of a generic procedure under test 
-  genericTypeRange :: s -> [Type]
-  -- | Range of instances for a type parameter of a polymorphic map
-  mapTypeRange :: s -> [Type]
-  
--- | Default range for instantiating procedure type parameters:
--- using a single type bool is enough unless the program contains a function or a map that allows differentiating between types at runtime
-defaultGenericTypeRange _ = [BoolType]
-
--- | Default range for instantiating polymorphic maps:
--- all nullary type constructors
-defaultMapTypeRange context = [BoolType, IntType] ++ [Instance name [] | name <- M.keys (M.filter (== 0) (ctxTypeConstructors context))]  
-  
--- | Settings for exhaustive testing  
-data ExhaustiveSettings = ExhaustiveSettings {
-  esIntRange :: [Integer],            -- ^ Input range for an integer variable
-  esIntMapDomainRange :: [Integer],   -- ^ Input range for an integer map domain
-  esGenericTypeRange :: [Type],       -- ^ Range of instances for a type parameter of a generic procedure under test 
-  esMapTypeRange :: [Type]            -- ^ Range of instances for a type parameter of a polymorphic map
-}
-
-instance TestSettings ExhaustiveSettings where
-  -- | Return all integers within limits  
-  generateIntInput = gets esIntRange
-  -- | Return both booleans
-  generateBoolInput = return [False, True]      
-  -- | Use all combinations of inputs for each variable   
-  combineInputs genOne args = sequence <$> mapM genOne args
-  mapDomainSettings s = s { esIntRange = esIntMapDomainRange s }  
-  genericTypeRange = esGenericTypeRange
-  mapTypeRange = esMapTypeRange
-  
--- | Settings for random testing  
-data RandomSettings = RandomSettings {
-  rsRandomGen :: StdGen,              -- ^ Random number generator
-  rsCount :: Int,                     -- ^ Number of test cases to be generated (currently per type in 'rsGenericTypeRange', if the procedure under test is generic)
-  rsIntLimits :: (Integer, Integer),  -- ^ Lower and upper bound for integer inputs
-  rsIntMapDomainRange :: [Integer],   -- ^ Input range for an integer map domain
-  rsGenericTypeRange :: [Type],       -- ^ Range of instances for a type parameter of a generic procedure under test 
-  rsMapTypeRange :: [Type]            -- ^ Range of instances for a type parameter of a polymorphic map
-}
-
-setRandomGen gen rs = rs { rsRandomGen = gen }
-
-instance TestSettings RandomSettings where
-  -- | Generate rsCount random values within limits
-  generateIntInput = do
-    randomGen <- gets rsRandomGen
-    limits <- gets rsIntLimits
-    n <- gets rsCount
-    changeState rsRandomGen setRandomGen $ replicateM n (state (randomR limits))
-    
-  -- | Generate rsCount random values within limits  
-  generateBoolInput = do
-    randomGen <- gets rsRandomGen
-    n <- gets rsCount
-    changeState rsRandomGen setRandomGen $ replicateM n (state random)    
-  
-  -- | Generate rsCount random tuples of values
-  combineInputs genOne args = transpose <$> mapM genOne args
-  
-  -- | Integer map domains are intervals [0..rsIntMapDomainSize s - 1]  
-  mapDomainSettings s = ExhaustiveSettings { 
-    esIntRange = rsIntMapDomainRange s,
-    esIntMapDomainRange = rsIntMapDomainRange s,
-    esGenericTypeRange = rsGenericTypeRange s,
-    esMapTypeRange = rsMapTypeRange s
-    }  
-      
-  genericTypeRange = rsGenericTypeRange
-  mapTypeRange = rsMapTypeRange
-
--- | Executions that have access to testing session parameters
-type TestSession s a = State (s, Environment) a
-        
-{- Reporting results -}
-
-instance Eq RuntimeFailure where
-  -- Runtime errors are considered equivalent if the same property failed at the same program location 
-  f == f'   =  rtfSource f == rtfSource f' && rtfPos f == rtfPos f' 
-
--- | Outcome of a test case        
-data Outcome = Pass | Fail RuntimeFailure | Invalid RuntimeFailure
-  deriving Eq
-
--- | Pretty-printed outcome  
-outcomeDoc :: Outcome -> Doc
-outcomeDoc Pass = text "passed"
-outcomeDoc (Fail err) = text "failed: " <+> runtimeFailureDoc err
-outcomeDoc (Invalid err) = text "invalid: " <+> runtimeFailureDoc err
-
-instance Show Outcome where show o = show (outcomeDoc o)
-
--- | Description of a test case
-data TestCase = TestCase {
-  tcProcedure :: Id,      -- ^ Procedure under test
-  tcLiveIns :: [Id],      -- ^ Input parameters for which an input value was generated
-  tcLiveGlobals :: [Id],  -- ^ Global variables for which an input value was generated
-  tcInput :: [Value],     -- ^ Values for in-parameters
-  tcOutcome :: Outcome    -- ^ Outcome
-} deriving Eq
-
--- | Pretty-printed test case
-testCaseDoc :: TestCase -> Doc
-testCaseDoc (TestCase procName liveIns liveGlobals input outcome) = text procName <> 
-  parens (commaSep (zipWith argDoc (liveIns ++ (map ("var " ++) liveGlobals)) input)) <+>
-  outcomeDoc outcome
-  where
-    argDoc name val = text name <+> text "=" <+> valueDoc val
-
-instance Show TestCase where show tc = show (testCaseDoc tc)
-
--- | Test cases are considered equivalent from a user perspective
--- | if they are testing the same procedure and result in the same outcome
-equivalent tc1 tc2 = tcProcedure tc1 == tcProcedure tc2 && tcOutcome tc1 == tcOutcome tc2      
-
--- | Test session summary
-data Summary = Summary {
-  sPassCount :: Int,            -- ^ Number of passing test cases
-  sFailCount :: Int,            -- ^ Number of failing test cases
-  sInvalidCount :: Int,         -- ^ Number of invalid test cases
-  sUniqueFailures :: [TestCase] -- ^ Unique failing test cases
-}
-
-totalCount s = sPassCount s + sFailCount s + sInvalidCount s
-
--- | Pretty-printed test session summary
-summaryDoc :: Summary -> Doc
-summaryDoc summary = 
-  text "Test cases:" <+> int (totalCount summary) $+$
-  text "Passed:" <+> int (sPassCount summary) $+$
-  text "Invalid:" <+> int (sInvalidCount summary) $+$
-  text "Failed:" <+> int (sFailCount summary) <+> parens (int (length (sUniqueFailures summary)) <+> text "unique") $+$
-  vsep (map testCaseDoc (sUniqueFailures summary))
-  
-instance Show Summary where show s = show (summaryDoc s)  
-    
-{- Test execution -}
-
--- | Test implementation def of procedure sig on all inputs prescribed by the testing strategy
-testImplementation :: TestSettings s => PSig -> PDef -> TestSession s [TestCase] 
-testImplementation sig def = do
-  let paramTypes = map itwType (psigParams sig)
-  tc <- gets (envTypeContext . snd)
-  typeRange <- gets (genericTypeRange . fst)
-  -- all types the procedure signature should be instantiated with:
-  let typeInputs = generateInputTypes typeRange tc { ctxTypeVars = psigTypeVars sig } paramTypes  
-  concat <$> mapM typeTestCase typeInputs
-  where
-    -- | Execute procedure instantiated with typeInputs on all value inputs
-    typeTestCase :: TestSettings s => [Type] -> TestSession s [TestCase]
-    typeTestCase typeInputs = do
-      -- fresh name for a parameter at position index; to be used as actual parameter
-      let localName index = [nonIdChar] ++ show index
-      let localNames = map localName [0..length (psigParams sig) - 1]
-      -- declare local variables localNames with appropriate types:
-      modify $ mapSnd (modifyTypeContext (`setLocals` (M.fromList $ zip localNames typeInputs)))
-      tc <- gets (envTypeContext . snd)
-      
-      -- names of actual in- and out-parameters
-      let (inParams, outParams) = splitAt (length (psigArgs sig)) localNames      
-      
-      -- names of input variables (variables for which input values are generated);
-      -- input variables can be either in-parameters or global variables 
-      let (liveIns, liveGlobals) = liveInputVariables sig def
-      let livePositions = map (fromJust . (`elemIndex` pdefIns def)) liveIns 
-      let liveActualIns = map localName livePositions
-      let liveGlobalVars = filter (`M.member` ctxGlobals tc) liveGlobals
-      let inputVars = liveActualIns ++ liveGlobalVars
-            
-      -- types of input variables
-      let inTypes = map (typeInputs !!) livePositions ++ map (ctxGlobals tc !) liveGlobalVars      
-      
-      let execTestCase input = changeState snd (mapSnd . const) $ testCase inParams outParams inputVars input
-      let reportTestCase input = TestCase (psigName sig) liveIns liveGlobalVars input <$> execTestCase input
-      -- all inputs the procedure should be tested on:
-      let genInputs = combineInputs (generateInputValue tc) inTypes
-      inputs <- changeState fst (mapFst . const) genInputs 
-      mapM reportTestCase inputs
-    -- | Assign inputVals to inputVars, and execute procedure with actual in-parameter variables inParams and actual out-parameter variables outParams;
-    -- | inputVars contain some inParams and some globals variables
-    testCase :: [Id] -> [Id] -> [Id] -> [Value] -> SafeExecution Outcome
-    testCase inParams outParams inputVars inputVals = do
-      setAll inputVars inputVals
-      let inExpr = map (gen . Var) inParams
-      let outExpr = map (gen . Var) outParams
-      execSafely (execProcedure (assumePreconditions sig) def inExpr outExpr >> return Pass) failureReport
-    -- | Test case outcome in case of a runtime error err
-    failureReport err = if failureKind err == Unreachable || failureKind err == Nonexecutable
-      then return $ Invalid err
-      else return $ Fail err
-            
-{- Input generation -}
-    
--- | generateInputValue c t: generate all values of type t in context c          
-generateInputValue :: TestSettings s => Context -> Type -> State s [Value]
-generateInputValue _ BoolType = map BoolValue <$> generateBoolInput
-generateInputValue _ IntType = map IntValue <$> generateIntInput
-generateInputValue c (MapType tv domains range) = do
-  typeRange <- gets mapTypeRange
-  let polyTypes = generateInputTypes typeRange c { ctxTypeVars = tv } (range : domains)
-  -- A polymorphic map is a union of monomorphic maps with all possible instantiations for type variables:
-  maps <- combineInputs monomorphicMap polyTypes
-  return $ map (MapValue . M.unions) maps
-  where
-    monomorphicMap (range : domains) = do 
-      -- Domain is always generated deterministically: 
-      args <- withLocalState mapDomainSettings (combineInputs (generateInputValue c) domains)
-      rets <- combineInputs (generateInputValue c) (replicate (length args) range)
-      return $ map (\r -> M.fromList (zip args r)) rets
-generateInputValue _ (Instance _ _) = map CustomValue <$> generateIntInput
-
--- | All instantiations of types ts in context c, with a range of instances for a single type variables range 
-generateInputTypes :: [Type] -> Context -> [Type] -> [[Type]]
-generateInputTypes range c ts = do
-  let freeVars = filter (\x -> any (x `isFreeIn`) ts) (ctxTypeVars c)
-  actuals <- replicateM (length freeVars) range
-  let binding = M.fromList (zip freeVars actuals)
-  return $ map (typeSubst binding) ts
-  

@@ -1,805 +1,887 @@ -- | Type checker for Boogie 2
 module Language.Boogie.TypeChecker (
   -- * Checking programs
-  checkProgram,
-  exprType,
-  resolve,
-  TypeError (..),
-  typeErrorsDoc,
-  Checked,  
-  -- * Typechecking context
-  Context (..),
-  emptyContext,
-  typeNames,
-  globalScope,
-  localScope,
-  mutableVars,
-  allVars,
-  allNames,
-  funProcNames,
-  funSig,
-  procSig,
-  setGlobals,
-  setIns,
-  setLocals,
-  setConstants,
-  enterFunction,
-  enterProcedure,
-  enterQuantified
-) where
-
-import Language.Boogie.AST
-import Language.Boogie.Util
-import Language.Boogie.Position
-import Language.Boogie.PrettyPrinter
-import Data.List
-import Data.Maybe
-import Data.Map (Map, (!))
-import qualified Data.Map as M
-import Control.Monad.Error
-import Control.Monad.Trans.Error hiding (throwError)
-import Control.Applicative
-import Text.PrettyPrint
-
-{- Interface -}
-
--- | 'checkProgram' @p@ : Check program @p@ and return the type information in the global part of the context
-checkProgram :: Program -> Checked Context
-checkProgram (Program decls) = do
-  pass1  <- foldAccum collectTypes emptyContext decls                            -- collect type names from type declarations
-  _pass2 <- mapAccum_ (checkTypeSynonyms pass1) decls                            -- check values of type synonyms
-  _pass3 <- mapAccum_ (checkCycles pass1 decls) (M.keys (ctxTypeSynonyms pass1)) -- check that type synonyms do not form a cycle 
-  pass4  <- foldAccum checkSignatures pass1 decls                                -- check variable, constant, function and procedure signatures
-  pass5  <- foldAccum checkBodies pass4 decls                                    -- check axioms, function and procedure bodies, constant parent info
-  return pass5
-  
--- | 'exprType' @c expr@ :
--- Type of @expr@ in context @c@;
--- fails if expr contains type errors.    
-exprType :: Context -> Expression -> Type
-exprType c expr = case checkExpression c expr of
-  Left _ -> (error . show) (text "encountered ill-typed expression during execution:" <+> exprDoc expr)
-  Right t -> t
-  
--- | 'enterFunction' @sig formals actuals mRetType c@ :
--- Local context of function @sig@ with formal arguments @formals@ and actual arguments @actuals@
--- in a context where the return type is exprected to be @mRetType@ (if known)
-enterFunction :: FSig -> [Id] -> [Expression] -> Maybe Type -> Context -> Context 
-enterFunction sig formals actuals mRetType c = c 
-  {
-    ctxTypeVars = [],
-    ctxIns = M.fromList (zip formals argTypes),
-    ctxLocals = M.empty,
-    ctxModifies = [],
-    ctxTwoState = False,
-    ctxInLoop = False
-  }
-  where 
-    inst = case fInstance c sig actuals mRetType of
-      Left _ -> (error . show) (text "encountered ill-typed function application during execution:" <+> 
-        text (fsigName sig) <+> parens (commaSep (map text formals)) <+>
-        text "to actual arguments" <+> parens (commaSep (map exprDoc actuals)))
-      Right u -> typeSubst u
-    argTypes = map inst (fsigArgTypes sig)
-
--- | 'enterProcedure' @sig def actuals lhss c@ :
--- Local context of procedure @sig@ with definition @def@ and actual arguments @actuals@
--- in a call with left-hand sides @lhss@
-enterProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Context -> Context 
-enterProcedure sig def actuals lhss c = c 
-  {
-    ctxTypeVars = [],
-    ctxIns = M.fromList $ zip ins inTypes,
-    ctxLocals = M.union (M.fromList $ zip localNames localTypes) (M.fromList $ zip outs outTypes),
-    ctxWhere = foldl addWhere (ctxWhere c) (zip (ins ++ outs ++ localNames) (paramWhere ++ localWhere)), 
-    ctxModifies = psigModifies sig,
-    ctxTwoState = True,
-    ctxInLoop = False
-  }
-  where
-    ins = pdefIns def
-    outs = pdefOuts def
-    locals = fst (pdefBody def)
-    inst = case pInstance c sig actuals lhss of
-      Left _ -> (error . show) (text "encountered ill-typed procedure call during execution:" <+> 
-        text (psigName sig) <+> text "with actual arguments" <+> parens (commaSep (map exprDoc actuals)) <+>
-        text "and left-hand sides" <+> parens (commaSep (map exprDoc lhss)))
-      Right u -> typeSubst u
-    inTypes = map inst (psigArgTypes sig)
-    outTypes = map inst (psigRetTypes sig)
-    localTypes = map (inst . itwType) locals
-    localNames = map itwId locals
-    addWhere m (id, w) = M.insert id w m
-    localWhere = map itwWhere locals
-    paramWhere = map (paramSubst sig def . itwWhere) (psigArgs sig ++ psigRets sig)
-   
--- | Local context of a quantified expression   
-enterQuantified :: [Id] -> [IdType] -> Context -> Context 
-enterQuantified tv vars c = c' 
-  {
-    ctxIns = foldl addIn (ctxIns c) vars
-  }
-  where
-    c' = c { ctxTypeVars = tv }
-    addIn ins (id, t) = M.insert id (resolve c' t) ins
-
-{- Errors -}
-
--- | Type error with a source position and a pretty-printed message
-data TypeError = TypeError SourcePos Doc
-
-instance ErrorList TypeError where
-  listMsg s = [TypeError noPos (text s)]
-
--- | Pretty-printed type error  
-typeErrorDoc (TypeError pos msgDoc) = text "Type error in" <+> text (show pos) $+$ msgDoc  
-  
--- | Pretty-printed list of type errors
-typeErrorsDoc errs = (vsep . punctuate newline . map typeErrorDoc) errs
-  
--- | Result of type checking: either 'a' or a type error
-type Checked a = Either [TypeError] a
-
--- | Throw a single type error
-throwTypeError pos msgDoc = throwError [TypeError pos msgDoc]
-
--- | Error accumulator: used to store intermediate type checking results, when errors should be accumulated rather than reported immediately
-data ErrorAccum a = ErrorAccum [TypeError] a
-
-instance Monad ErrorAccum where
-  return x                = ErrorAccum [] x
-  ErrorAccum errs x >>= f = case (f x) of
-    ErrorAccum es v -> ErrorAccum (errs ++ es) v
-
--- | Transform a type checking result and default value into an error accumlator
-accum :: Checked a -> a -> ErrorAccum a
-accum cx y = case cx of
-  Left e -> ErrorAccum e y
-  Right x -> ErrorAccum [] x    
-  
--- | Transform an error accumulator back into a rgeular type checking result  
-report :: ErrorAccum a -> Checked a
-report (ErrorAccum [] x) = Right x
-report (ErrorAccum es _) = Left es  
-
--- | 'foldAccum' @f c nodes@ :
--- Apply type checking @f@ to all @nodes@ in the initial context @c@,
--- accumulating errors from all @nodes@ and reporting them at the end;
--- in case of success the modified context is passed on and in case of failure the context is unchanged
-foldAccum :: (a -> b -> Checked a) -> a -> [b] -> Checked a
-foldAccum f c nodes = report $ foldM (acc f) c nodes
-  where
-    acc f x y = accum (f x y) x
-    
--- | 'mapAccum' @f def nodes@ :
--- Apply type checking @f@ to all @nodes@,
--- accumulating errors from all @nodes@ and reporting them at the end
-mapAccum :: (b -> Checked c) -> c -> [b] -> Checked [c]
-mapAccum f def nodes = report $ mapM (acc f) nodes  
-  where
-    acc f x  = accum (f x) def
-   
--- | 'mapAccumA_' @f nodes@ :
--- Apply type checking @f@ to all @nodes@ throwing away the result,
--- accumulating errors from all @nodes@
-mapAccumA_ :: (a -> Checked ()) -> [a] -> ErrorAccum ()
-mapAccumA_ f nodes = mapM_ (acc f) nodes  
-  where
-    acc f x  = accum (f x) ()
-    
--- | Same as 'mapAccumA_', but reporting the error at the end
-mapAccum_ :: (a -> Checked ()) -> [a] -> Checked ()
-mapAccum_ f nodes = report $ mapAccumA_ f nodes  
-
--- | 'zipWithAccum_' @f xs ys@ :
--- Apply type checking @f@ to all @xs@ and @ys@ throwing away the result,
--- accumulating errors from all nodes and reporting them at the end
-zipWithAccum_ :: (a -> b -> Checked ()) -> [a] -> [b] -> Checked ()
-zipWithAccum_ f xs ys = report $ zipWithM_ (acc f) xs ys  
-  where
-    acc f x y  = accum (f x y) ()
-  
-{- Context -}
-
--- | Typechecking context
-data Context = Context
-  {
-    -- Global context:
-    ctxTypeConstructors :: Map Id Int,      -- ^ type constructor arity
-    ctxTypeSynonyms :: Map Id ([Id], Type), -- ^ type synonym values
-    ctxGlobals :: Map Id Type,              -- ^ global variable types (type synonyms resolved)
-    ctxConstants :: Map Id Type,            -- ^ constant types (type synonyms resolved)
-    ctxFunctions :: Map Id FSig,            -- ^ function signatures (type synonyms resolved)
-    ctxProcedures :: Map Id PSig,           -- ^ procedure signatures (type synonyms resolved)
-    ctxWhere :: Map Id Expression,          -- ^ where clauses of variables (global and local)
-    
-    -- Local context:
-    ctxTypeVars :: [Id],                    -- ^ free type variables
-    ctxIns :: Map Id Type,                  -- ^ input parameter types
-    ctxLocals :: Map Id Type,               -- ^ local variable types
-    ctxModifies :: [Id],                    -- ^ variables in the modifies clause of the enclosing procedure
-    ctxLabels :: [Id],                      -- ^ all labels of the enclosing procedure body
-    ctxEncLabels :: [Id],                   -- ^ labels of all enclosing statements
-    ctxTwoState :: Bool,                    -- ^ is the context two-state? (procedure body or postcondition)
-    ctxInLoop :: Bool,                      -- ^ is context inside a loop body?
-    ctxPos :: SourcePos                     -- ^ position in the source code
-  }
-
--- | Empty context  
-emptyContext = Context {
-    ctxTypeConstructors = M.empty,
-    ctxTypeSynonyms     = M.empty,
-    ctxGlobals          = M.empty,
-    ctxConstants        = M.empty,
-    ctxFunctions        = M.empty,
-    ctxProcedures       = M.empty,
-    ctxWhere            = M.empty,
-    ctxTypeVars         = [],
-    ctxIns              = M.empty,
-    ctxLocals           = M.empty,
-    ctxModifies         = [],
-    ctxLabels           = [],
-    ctxEncLabels        = [],
-    ctxTwoState         = False,
-    ctxInLoop           = False,
-    ctxPos              = noPos
-  }
-
-setGlobals ctx g    = ctx { ctxGlobals = g }
-setIns ctx i        = ctx { ctxIns = i }
-setLocals ctx l     = ctx { ctxLocals = l }
-setConstants ctx c  = ctx { ctxConstants = c }
-
--- | Type constructors and synonyms
-typeNames c = M.keys (ctxTypeConstructors c) ++ M.keys (ctxTypeSynonyms c)
--- | Global variables and constants
-globalScope c = M.union (ctxGlobals c) (ctxConstants c)
--- | Input parameters and local variables
-localScope c = M.union (ctxIns c) (ctxLocals c)
--- | All variables that can be assigned to (local variables and global variables)
-mutableVars c = M.union (ctxGlobals c) (ctxLocals c)
--- | All variables that can have where clauses (everything except constants)
-allVars c = M.union (localScope c) (ctxGlobals c)
--- | All variables and constants (local-scope preferred)
-allNames c = M.union (localScope c) (globalScope c)
--- | Names of functions and procedures
-funProcNames c = M.keys (ctxFunctions c) ++ M.keys (ctxProcedures c)
--- | Function signature by name
-funSig name c = ctxFunctions c ! name
--- | Procedure signature by name
-procSig name c = ctxProcedures c ! name    
-  
-{- Types -}
-  
--- | Check that a type variable is fresh and add it to context  
-checkTypeVar :: Context -> Id -> Checked Context
-checkTypeVar c v
-  | v `elem` typeNames c = throwTypeError (ctxPos c) (text v <+> text "already used as a type constructor or synonym")
-  | v `elem` ctxTypeVars c = throwTypeError (ctxPos c) (text "Multiple decalartions of type variable" <+> text v)
-  | otherwise = return c { ctxTypeVars = v : ctxTypeVars c }
-
--- | 'checkType' @c t@ : check that @t@ is a correct type in context @c@ (i.e. that all type names exist and have correct number of arguments)
-checkType :: Context -> Type -> Checked ()
-checkType c (MapType tv domains range) = do
-  c' <- foldAccum checkTypeVar c tv
-  mapAccum_ (checkType c') (domains ++ [range])
-checkType c (Instance name args)
-  | name `elem` ctxTypeVars c && null args = return ()
-  | M.member name (ctxTypeConstructors c) = if n == length args 
-    then mapAccum_ (checkType c) args
-    else throwTypeError (ctxPos c) (text "Wrong number of arguments" <+> int (length args) <+> text "given to the type constructor" <+> text name <+> 
-      parens (text "expected" <+> int n))
-  | M.member name (ctxTypeSynonyms c) = if length formals == length args
-    then mapAccum_ (checkType c) args
-    else throwTypeError (ctxPos c) (text "Wrong number of arguments " <+> int (length args) <+> text "given to the type synonym" <+> text name <+> 
-      parens (text "expected" <+> int (length formals)))
-  | otherwise = throwTypeError (ctxPos c) (text "Not in scope: type constructor or synonym" <+> text name)
-    where 
-      n = ctxTypeConstructors c ! name
-      formals = fst (ctxTypeSynonyms c ! name)
-checkType _ _ = return ()
-
--- | 'resolve' @c t@ : type @t@ with all type synonyms resolved according to binding in @c@
-resolve :: Context -> Type -> Type
-resolve c (MapType tv domains range) = MapType tv (map (resolve c') domains) (resolve c' range)
-  where c' = c { ctxTypeVars = ctxTypeVars c ++ tv }
-resolve c (Instance name args) 
-  | name `elem` ctxTypeVars c = Instance name args
-  | otherwise = case M.lookup name (ctxTypeSynonyms c) of
-    Nothing -> Instance name (map (resolve c) args)
-    Just (formals, t) -> resolve c (typeSubst (M.fromList (zip formals args)) t)
-resolve _ t = t
-
--- | 'fInstance' @c sig actuals mRetType@ :
--- Instantiation of type variables in a function signature @sig@ given the actual arguments @actuals@ in a context @c@
--- and possibly a return type @mRetType@ (if known from the context)
-fInstance :: Context -> FSig -> [Expression] -> Maybe Type -> Checked TypeBinding
-fInstance c sig actuals mRetType = case mRetType of
-    Nothing -> if not (null retOnlyTVs) 
-      then throwTypeError (ctxPos c) (text "Cannot infer type arguments from the context:" <+> commaSep (map text retOnlyTVs) <+> text "(insert a coercion)")
-      else do
-        actualTypes <- mapAccum (checkExpression c) noType actuals
-        case oneSidedUnifier (fsigTypeVars sig) (fsigArgTypes sig) (ctxTypeVars c) actualTypes of
-          Nothing -> throwTypeError (ctxPos c) (text "Could not match formal argument types" <+> 
-            doubleQuotes (commaSep (map typeDoc (fsigArgTypes sig))) <+>
-            text "against actual argument types" <+> 
-            doubleQuotes (commaSep (map typeDoc actualTypes)) <+>
-            text "in the call to" <+> text (fsigName sig))
-          Just u -> return u
-    Just retType -> do
-      actualTypes <- mapAccum (checkExpression c) noType actuals
-      case oneSidedUnifier (fsigTypeVars sig) (fsigRetType sig : fsigArgTypes sig) (ctxTypeVars c) (retType : actualTypes) of
-        Nothing -> throwTypeError (ctxPos c) (text "Could not match function signature" <+> 
-          doubleQuotes (sigDoc (fsigArgTypes sig) [fsigRetType sig]) <+>
-          text "against actual types" <+> 
-          doubleQuotes (sigDoc actualTypes [retType]) <+>
-          text "in the call to" <+> text (fsigName sig))
-        Just u -> return u
-  where
-    tvs = fsigTypeVars sig
-    retOnlyTVs = filter (not . freeInArgs) tvs
-    freeInArgs tv = any (tv `isFreeIn`) (fsigArgTypes sig)
-      
--- | 'pInstance' @c sig actuals lhss@ : 
--- Instantiation of type variables in a procedure @sig@ given the actual arguments @actuals@ and call left-hand sides @lhss@, in a context @c@
-pInstance :: Context -> PSig -> [Expression] -> [Expression] -> Checked TypeBinding
-pInstance c sig actuals lhss = do
-  actualTypes <- mapAccum (checkExpression c) noType actuals
-  lhssTypes <- mapAccum (checkExpression c) noType lhss
-  case oneSidedUnifier (psigTypeVars sig) (psigArgTypes sig ++ psigRetTypes sig) (ctxTypeVars c) (actualTypes ++ lhssTypes) of
-    Nothing -> throwTypeError (ctxPos c) (text "Could not match procedure signature" <+> 
-      doubleQuotes (sigDoc (psigArgTypes sig) (psigRetTypes sig)) <+>
-      text "against actual types" <+> 
-      doubleQuotes (sigDoc actualTypes lhssTypes) <+>
-      text "in the call to" <+> text (psigName sig))
-    Just u -> return u    
-  
-{- Expressions -}
-
--- | 'checkExpression' @c expr@ :
--- Check that @expr@ is a valid expression in context @c@ and return its type
--- (requires all types in the context be valid and type synonyms be resolved)
-checkExpression :: Context -> Expression -> Checked Type
-checkExpression c (Pos pos e) = case e of
-  TT -> return BoolType
-  FF -> return BoolType
-  Numeral n -> return IntType
-  Var id -> case M.lookup id (allNames c) of
-    Nothing -> throwTypeError pos (text "Not in scope: variable or constant" <+> text id)
-    Just t -> return t
-  Application id args -> checkApplication cPos id args Nothing
-  MapSelection m args -> checkMapSelection cPos m args
-  MapUpdate m args val -> checkMapUpdate cPos m args val
-  Old e1 -> if ctxTwoState c
-    then checkExpression c { ctxLocals = M.empty } e1
-    else throwTypeError pos (text "Old expression in a single state context")
-  IfExpr cond e1 e2 -> checkIfExpression cPos cond e1 e2
-  Coercion e t -> checkCoercion cPos e t
-  UnaryExpression op e1 -> checkUnaryExpression cPos op e1
-  BinaryExpression op e1 e2 -> checkBinaryExpression cPos op e1 e2
-  Quantified qop tv vars e -> checkQuantified cPos qop tv vars e
-  where
-    cPos = c { ctxPos = pos }
-
--- @mRetType@ stores function return type if known from the context (currently: if used inside a coercion);
--- it is a temporary workaround for generic return types of functions    
-checkApplication :: Context -> Id -> [Expression] -> Maybe Type -> Checked Type
-checkApplication c id args mRetType = case M.lookup id (ctxFunctions c) of
-  Nothing -> throwTypeError (ctxPos c) (text "Not in scope: function" <+> text id)
-  Just sig -> do
-    u <- fInstance c sig args mRetType
-    return $ typeSubst u (fsigRetType sig)
-    
-checkMapSelection :: Context -> Expression -> [Expression] -> Checked Type
-checkMapSelection c m args = do
-  mType <- checkExpression c m
-  case mType of
-    MapType tv domainTypes rangeType -> do
-      actualTypes <- mapAccum (checkExpression c) noType args
-      case oneSidedUnifier tv domainTypes (ctxTypeVars c) actualTypes of
-        Nothing -> throwTypeError (ctxPos c) (text "Could not match map domain types" <+> doubleQuotes (commaSep (map typeDoc domainTypes)) <+>
-          text "against map selection types" <+> doubleQuotes (commaSep (map typeDoc actualTypes)) <+>
-          text "for the map" <+> exprDoc m)
-        Just u -> return (typeSubst u rangeType)
-    t -> throwTypeError (ctxPos c) (text "Map selection applied to a non-map" <+> exprDoc m <+> text "of type" <+> doubleQuotes (typeDoc t))
-  
-checkMapUpdate :: Context -> Expression -> [Expression] -> Expression -> Checked Type
-checkMapUpdate c m args val = do 
-  t <- checkMapSelection c m args
-  actualT <- checkExpression c val
-  if t <==> actualT 
-    then checkExpression c m 
-    else throwTypeError (ctxPos c) (text "Update value type" <+> doubleQuotes (typeDoc actualT) <+> text "different from map range type" <+> doubleQuotes (typeDoc t))
-    
-checkIfExpression :: Context -> Expression -> Expression -> Expression -> Checked Type    
-checkIfExpression c cond e1 e2 = do
-  compareType c "if-expression condition" BoolType cond
-  t <- checkExpression c e1
-  compareType c "else-part of the if-expression" t e2
-  return t
-  
-checkCoercion :: Context -> Expression -> Type -> Checked Type
-checkCoercion c e t = do
-  checkType c t
-  let t' = resolve c t
-  case node e of
-    Application id args -> checkApplication cPos id args (Just t')
-    _ -> compareType c "coerced expression" t' e >> return t'
-  where cPos = c { ctxPos = position e }
-    
-checkUnaryExpression :: Context -> UnOp -> Expression -> Checked Type
-checkUnaryExpression c op e
-  | op == Neg = matchType IntType IntType
-  | op == Not = matchType BoolType BoolType
-  where 
-    matchType t ret = do
-      t' <- checkExpression c e
-      if t' <==> t then return ret else throwTypeError (ctxPos c) (errorMsg t' op)
-    errorMsg t op = text "Invalid argument type" <+> doubleQuotes (typeDoc t) <+> text "to unary operator" <+> unOpDoc op
-  
-checkBinaryExpression :: Context -> BinOp -> Expression -> Expression -> Checked Type
-checkBinaryExpression c op e1 e2
-  | elem op [Plus, Minus, Times, Div, Mod] = matchTypes (\t1 t2 -> t1 <==> IntType && t2 <==> IntType) IntType
-  | elem op [And, Or, Implies, Explies, Equiv] = matchTypes (\t1 t2 -> t1 <==> BoolType && t2 <==> BoolType) BoolType
-  | elem op [Ls, Leq, Gt, Geq] = matchTypes (\t1 t2 -> t1 <==> IntType && t2 <==> IntType) BoolType
-  | elem op [Eq, Neq] = matchTypes (\t1 t2 -> isJust (unifier (ctxTypeVars c) [t1] [t2])) BoolType
-  | op == Lc = matchTypes (<==>) BoolType
-  where 
-    matchTypes pred ret = do
-      t1 <- checkExpression c e1
-      t2 <- checkExpression c e2
-      if pred t1 t2 then return ret else throwTypeError (ctxPos c) (errorMsg t1 t2 op)
-    errorMsg t1 t2 op = text "Invalid argument types" <+> doubleQuotes (typeDoc t1) <+> text "and" <+> doubleQuotes (typeDoc t2) <+> text "to binary operator" <+> binOpDoc op
-    
-checkQuantified :: Context -> QOp -> [Id] -> [IdType] -> Expression -> Checked Type
-checkQuantified c Lambda tv vars e = do
-  c' <- foldAccum checkTypeVar c tv
-  quantifiedScope <- foldAccum (checkIdType localScope ctxIns setIns) c' vars
-  if not (null missingTV)
-    then throwTypeError (ctxPos c) (text "Type variable(s) must occur among the types of lambda parameters:" <+> commaSep (map text missingTV)) 
-    else do
-      rangeType <- checkExpression quantifiedScope e
-      return $ MapType tv varTypes rangeType
-  where
-    varTypes = map snd vars
-    missingTV = filter (not . freeInVars) tv    
-    freeInVars v = any (v `isFreeIn`) varTypes      
-checkQuantified c qop tv vars e = do
-  c' <- foldAccum checkTypeVar c tv
-  quantifiedScope <- foldAccum (checkIdType localScope ctxIns setIns) c' vars
-  compareType quantifiedScope "quantified expression" BoolType e
-  return BoolType
-    
-{- Statements -}
-
--- | 'checkStatement' @c st@ :
--- Check that @st@ is a valid statement in context @c@
-checkStatement :: Context -> Statement -> Checked ()
-checkStatement c (Pos pos s) = case s of
-  Predicate (SpecClause _ _ e) -> compareType cPos "predicate" BoolType e
-  Havoc vars -> checkLefts cPos (nub vars) (length (nub vars))
-  Assign lhss rhss -> checkAssign cPos lhss rhss
-  Call lhss name args -> checkCall cPos lhss name args
-  CallForall name args -> checkCallForall cPos name args
-  If cond thenBlock elseBlock -> checkIf cPos cond thenBlock elseBlock
-  While cond invs b -> checkWhile cPos cond invs b
-  Goto ids -> checkGoto cPos ids
-  Break Nothing -> checkSimpleBreak cPos
-  Break (Just l) -> checkLabelBreak cPos l
-  _ -> return ()
-  where
-    cPos = c { ctxPos = pos }
-
-checkAssign :: Context -> [(Id , [[Expression]])] -> [Expression] -> Checked ()
-checkAssign c lhss rhss = do
-  checkLefts c (map fst lhss) (length rhss)
-  rTypes <- mapAccum (checkExpression c) noType rhss
-  zipWithAccum_ (compareType c "assignment left-hand side") rTypes (map selectExpr lhss) 
-  where
-    selectExpr (id, selects) = foldl mapSelectExpr (attachPos (ctxPos c) (Var id)) selects
-        
-checkCall :: Context -> [Id] -> Id -> [Expression] -> Checked ()
-checkCall c lhss name args = case M.lookup name (ctxProcedures c) of
-  Nothing -> throwTypeError (ctxPos c) (text "Not in scope: procedure" <+> text name)
-  Just sig -> let illegalModifies = psigModifies sig \\ ctxModifies c in
-    if not (null illegalModifies) 
-    then throwTypeError (ctxPos c) (text "Call modifies a global variable that is not in the enclosing procedure's modifies clause:" <+> commaSep (map text illegalModifies))
-    else do
-      checkLefts c lhss (length $ psigRetTypes sig)
-      let lhssExpr = map (attachPos (ctxPos c) . Var) lhss
-      pInstance c sig args lhssExpr >> return ()      
-        
-checkCallForall :: Context -> Id -> [WildcardExpression] -> Checked ()
-checkCallForall c name args = case M.lookup name (ctxProcedures c) of
-  Nothing -> throwTypeError (ctxPos c) (text "Not in scope: procedure" <+> text name)
-  Just sig -> if not (null (psigModifies sig)) 
-    then throwTypeError (ctxPos c) (text "Call forall to a procedure with a non-empty modifies clause")
-    else pInstance c sig { psigArgs = concrete (psigArgs sig) } concreteArgs [] >> return ()
-  where
-    concreteArgs = [e | (Expr e) <- args]
-    concrete at = [at !! i | i <- [0..length args - 1], isConcrete (args !! i)]
-    isConcrete Wildcard = False
-    isConcrete (Expr _) = True
-    
-checkIf :: Context -> WildcardExpression -> Block -> (Maybe Block) -> Checked ()
-checkIf c cond thenBlock elseBlock = report $ do
-  case cond of
-    Wildcard -> return ()
-    Expr e -> accum (compareType c "branching condition" BoolType e) ()
-  accum (checkBlock c thenBlock) ()
-  case elseBlock of
-    Nothing -> return ()
-    Just b -> accum (checkBlock c b) ()
-    
-checkWhile :: Context -> WildcardExpression -> [SpecClause] -> Block -> Checked ()
-checkWhile c cond invs body = report $ do
-  case cond of  
-    Wildcard -> return ()
-    Expr e -> accum (compareType c "loop condition" BoolType e) ()
-  mapAccumA_ (compareType c "loop invariant" BoolType) (map specExpr invs)
-  accum (checkBlock c {ctxInLoop = True} body) ()
-
-checkGoto :: Context -> [Id] -> Checked ()  
-checkGoto c ids = if not (null unknownLabels)
-  then throwTypeError (ctxPos c) (text "Not in scope: label(s)" <+> commaSep (map text unknownLabels))
-  else return ()
-  where
-    unknownLabels = ids \\ ctxLabels c 
-    
-checkSimpleBreak :: Context -> Checked ()
-checkSimpleBreak c = if not (ctxInLoop c)
-  then throwTypeError (ctxPos c) (text "Break statement outside a loop")
-  else return ()
-  
-checkLabelBreak :: Context -> Id -> Checked ()
-checkLabelBreak c l = if not (l `elem` ctxEncLabels c)
-  then throwTypeError (ctxPos c) (text "Break label" <+> text l <+> text "does not label an enclosing statement")
-  else return ()
-  
-{- Blocks -}
-
--- | 'collectLabels' @c block@ : 
--- Check that all labels in @block@ and nested blocks are unique and add them to the context
-collectLabels :: Context -> Block -> Checked Context
-collectLabels c block = foldAccum checkLStatement c block
-  where
-    checkLStatement c (Pos pos (ls, (Pos _ st))) = do
-      c' <- foldM (addLabel pos) c ls
-      case st of
-        If _ thenBlock mElseBlock -> do 
-          c'' <- collectLabels c' thenBlock
-          case mElseBlock of
-            Nothing -> return c''
-            Just elseBlock -> collectLabels c'' elseBlock
-        While _ _ bodyBlock -> collectLabels c' bodyBlock
-        _ -> return c'
-    addLabel pos c l = if l `elem` ctxLabels c 
-      then throwTypeError pos (text "Multiple occurrences of label" <+> text l <+> text "in a procedure body")
-      else return c {ctxLabels = l : ctxLabels c}
-
--- | Check every statement in a block
-checkBlock :: Context -> Block -> Checked ()    
-checkBlock c block = mapAccum_ (checkLStatement c) block
-  where
-    checkLStatement c (Pos _ (ls, st)) = checkStatement c { ctxEncLabels = ctxEncLabels c ++ ls} st
-    
-{- Declarations -}
-
--- | Collect type names from type declarations
-collectTypes :: Context -> Decl -> Checked Context
-collectTypes c (Pos pos d) = case d of
-  TypeDecl ts -> foldM checkTypeDecl c { ctxPos = pos } ts
-  otherwise -> return c  
-
--- | Check uniqueness of type constructors and synonyms, and them in the context  
-checkTypeDecl :: Context -> NewType -> Checked Context 
-checkTypeDecl c (NewType name formals value)
-  | name `elem` (typeNames c) = throwTypeError (ctxPos c) (text "Multiple declarations of type constructor or synonym" <+> text name) 
-  | otherwise = case value of
-    Nothing -> return c { ctxTypeConstructors = M.insert name (length formals) (ctxTypeConstructors c) }
-    Just t -> return c { ctxTypeSynonyms = M.insert name (formals, t) (ctxTypeSynonyms c) }
-
--- | Check that type arguments of type synonyms are fresh and values are valid types
-checkTypeSynonyms :: Context -> Decl -> Checked ()
-checkTypeSynonyms c (Pos pos d) = case d of
-  TypeDecl ts -> mapAccum_ (checkNewType c { ctxPos = pos }) ts
-  otherwise -> return ()
-  where
-    checkNewType c (NewType name formals (Just t)) = do
-      c' <- foldAccum checkTypeVar c formals 
-      checkType c' t
-    checkNewType _ _ = return ()
-
--- | Check if type synonym declarations have cyclic dependences (program is passed for the purpose of error reporting)
-checkCycles :: Context -> [Decl] -> Id -> Checked ()
-checkCycles c decls id = checkCyclesWith c id (value id)
-  where
-    checkCyclesWith c id t = case t of
-      Instance name args -> do
-        if M.member name (ctxTypeSynonyms c)
-          then if id == name 
-            then throwTypeError firstPos (text "Cycle in the definition of type synonym" <+> text id) 
-            else checkCyclesWith c id (value name)
-          else return ()
-        mapAccum_ (checkCyclesWith c id) args
-      MapType _ domains range -> mapAccum_ (checkCyclesWith c id) (range:domains)
-      _ -> return ()
-    value name = snd (ctxTypeSynonyms c ! name)
-    firstPos = head [pos | Pos pos (TypeDecl ts) <- decls, id `elem` map tId ts]
-
--- | Check variable, constant, function and procedures and add them to context
-checkSignatures :: Context -> Decl -> Checked Context
-checkSignatures c (Pos pos d) = case d of
-  VarDecl vars -> foldAccum (checkIdType globalScope ctxGlobals setGlobals) cPos (map noWhere vars)
-  ConstantDecl _ ids t _ _ -> foldAccum (checkIdType globalScope ctxConstants setConstants) cPos (zip ids (repeat t))
-  FunctionDecl name tv args ret _ -> checkFunctionSignature cPos name tv args ret
-  ProcedureDecl name tv args rets specs _ -> checkProcSignature cPos name tv args rets specs
-  otherwise -> return c
-  where
-    cPos = c { ctxPos = pos }
-
--- | 'checkIdType' @scope get set c idType@ : 
--- Check that declaration @idType@ is fresh in @scope@, and if so add it to @get c@ using @set c@
-checkIdType :: (Context -> Map Id Type) -> (Context -> Map Id Type) -> (Context -> Map Id Type -> Context) -> Context -> IdType -> Checked Context
-checkIdType scope get set c (i, t)   
-  | M.member i (scope c) = throwTypeError (ctxPos c) (text "Multiple declarations of variable or constant" <+> text i)
-  | otherwise = checkType c t >> return (c `set` M.insert i (resolve c t) (get c))
-
--- | Check uniqueness of function name, types of formals and add function to context
-checkFunctionSignature :: Context -> Id -> [Id] -> [FArg] -> FArg -> Checked Context
-checkFunctionSignature c name tv args ret
-  | name `elem` funProcNames c = throwTypeError (ctxPos c) (text "Multiple declarations of function or procedure" <+> text name)
-  | otherwise = do
-    c' <- foldAccum checkTypeVar c tv
-    foldAccum checkFArg c' params
-    if not (null missingTV) 
-      then throwTypeError (ctxPos c) (text "Type variable(s) must occur in function arguments or return type:" <+> commaSep (map text missingTV))
-      else return $ addFSig c name (FSig name tv argTypes retType) 
-    where
-      params = args ++ [ret]
-      checkFArg c (Just id, t) = checkIdType ctxIns ctxIns setIns c (id, t)
-      checkFArg c (Nothing, t) = checkType c t >> return c
-      missingTV = filter (not . freeInParams) tv
-      freeInParams v = any (v `isFreeIn`) (map snd params)
-      addFSig c name sig = c { ctxFunctions = M.insert name sig (ctxFunctions c) }
-      argTypes = map (resolve c . snd) args
-      retType = (resolve c . snd) ret
-      
--- | Check uniqueness of procedure name, types of formals and add procedure to context      
-checkProcSignature :: Context -> Id -> [Id] -> [IdTypeWhere] -> [IdTypeWhere] -> [Contract] -> Checked Context
-checkProcSignature c name tv args rets specs
-  | name `elem` funProcNames c = throwTypeError (ctxPos c) (text "Multiple declarations of function or procedure" <+> text name)
-  | otherwise = do
-    c' <- foldAccum checkTypeVar c tv
-    foldAccum checkPArg c' params
-    if not (null missingTV) 
-      then throwTypeError (ctxPos c) (text "Type variable(s) must occur in procedure in- our out-parameters:" <+> commaSep (map text missingTV))
-      else return $ addPSig c name (PSig name tv (map resolveType args) (map resolveType rets) specs)
-    where
-      params = args ++ rets
-      checkPArg c arg = checkIdType ctxIns ctxIns setIns c (noWhere arg)
-      missingTV = filter (not . freeInParams) tv
-      freeInParams v = any (v `isFreeIn`) (map itwType params)
-      addPSig c name sig = c { ctxProcedures = M.insert name sig (ctxProcedures c) }
-      resolveType (IdTypeWhere id t w) = IdTypeWhere id (resolve c t) w
-
--- | Check axioms, function and procedure bodies      
-checkBodies :: Context -> Decl -> Checked Context
-checkBodies c (Pos pos d) = case d of
-  VarDecl vars -> foldAccum checkWhere cPos vars
-  ConstantDecl _ ids t (Just edges) _ -> checkParentInfo cPos ids t (map snd edges) >> return c
-  FunctionDecl name tv args ret (Just body) -> checkFunction cPos name tv args body >> return c
-  AxiomDecl e -> checkAxiom cPos e >> return c
-  ProcedureDecl name tv args rets specs mb -> checkProcedure cPos tv args rets specs mb >> return c
-  ImplementationDecl name tv args rets bodies -> checkImplementation cPos name tv args rets bodies >> return c
-  otherwise -> return c
-  where
-    cPos = c { ctxPos = pos }  
-  
--- | Check that where-part is a valid boolean expression
-checkWhere :: Context -> IdTypeWhere -> Checked Context
-checkWhere c var = do
-   -- Where clauses are always in single-state context:
-  compareType c { ctxTwoState = False } "where clause" BoolType (itwWhere var)
-  return c { ctxWhere = M.insert (itwId var) (itwWhere var) (ctxWhere c) }
-
--- | Check that identifiers in parents are distinct constants of a proper type and do not occur among ids
-checkParentInfo :: Context -> [Id] -> Type -> [Id] -> Checked ()
-checkParentInfo c ids t parents = if length parents /= length (nub parents)
-  then throwTypeError (ctxPos c) (text "Parent list contains duplicates:" <+> commaSep (map text parents))
-  else mapAccum_ checkParent parents
-  where
-    checkParent p = case M.lookup p (ctxConstants c) of
-      Nothing -> throwTypeError (ctxPos c) (text "Not in scope: constant" <+> text p)
-      Just t' -> if not (t <==> t')
-        then throwTypeError (ctxPos c) (text "Parent type" <+> doubleQuotes (typeDoc t') <+> text "is different from constant type" <+> doubleQuotes (typeDoc t))
-        else if p `elem` ids
-          then throwTypeError (ctxPos c) (text "Constant" <+> text p <+> text "is decalred to be its own parent")
-          else return ()    
-
--- | Check that axiom is a valid boolean expression    
-checkAxiom :: Context -> Expression -> Checked ()
-checkAxiom c e = compareType c {ctxGlobals = M.empty } "axiom" BoolType e
-  
--- | Check that function body is a valid expression of the same type as the function return type
-checkFunction :: Context -> Id -> [Id] -> [FArg] -> Expression -> Checked ()
-checkFunction c name tv args body = do 
-  functionScope <- foldAccum addFArg c { ctxTypeVars = tv } args
-  compareType functionScope { ctxGlobals = M.empty } "function body" retType body
-  where 
-    addFArg c (Just id, t) = checkIdType ctxIns ctxIns setIns c (id, t)
-    addFArg c  _ = return c
-    sig = funSig name c
-    retType = fsigRetType sig
-        
--- | Check where-parts of procedure arguments and statements in its body
-checkProcedure :: Context -> [Id] -> [IdTypeWhere] -> [IdTypeWhere] -> [Contract] -> (Maybe Body) -> Checked ()
-checkProcedure c tv args rets specs mb = do 
-  cArgs <- foldAccum (checkIdType localScope ctxIns setIns) c { ctxTypeVars = tv } (map noWhere args)
-  _ <- foldAccum checkWhere cArgs args
-  mapAccum_ (compareType cArgs "precondition" BoolType . specExpr) (preconditions specs)
-  cRets <- foldAccum (checkIdType localScope ctxLocals setLocals) cArgs (map noWhere rets)
-  _ <- foldAccum checkWhere cRets rets
-  mapAccum_ (compareType cRets {ctxTwoState = True} "postcondition" BoolType . specExpr) (postconditions specs)
-  if not (null invalidModifies)
-    then throwTypeError (ctxPos c) (text "Identifier in a modifies clause does not denote a global variable:" <+> commaSep (map text invalidModifies))
-    else case mb of
-      Nothing -> return ()
-      Just body -> checkBody cRets { ctxModifies = modifies specs, ctxTwoState = True } body
-  where invalidModifies = modifies specs \\ M.keys (ctxGlobals c)
-  
--- | Check procedure body  
-checkBody :: Context -> Body -> Checked ()
-checkBody c body = do
-  bodyScope <- foldAccum (checkIdType localScope ctxLocals setLocals) c (map noWhere (concat (fst body)))
-  _ <- foldAccum checkWhere bodyScope (concat (fst body))
-  bodyScope' <- collectLabels bodyScope (snd body)
-  checkBlock bodyScope' (snd body)
-
--- | Check that implementation corresponds to a known procedure and matches its signature, then check all bodies
-checkImplementation :: Context -> Id -> [Id] -> [IdType] -> [IdType] -> [Body] -> Checked ()  
-checkImplementation c name tv args rets bodies = case M.lookup name (ctxProcedures c) of
-    Nothing -> throwTypeError (ctxPos c) (text "Not in scope: procedure" <+> text name)
-    Just sig -> case boundUnifier [] (psigTypeVars sig) (psigArgTypes sig ++ psigRetTypes sig) tv (argTypes ++ retTypes) of
-      Nothing -> throwTypeError (ctxPos c) (text "Could not match procedure signature" <+> 
-        doubleQuotes (sigDoc (psigArgTypes sig) (psigRetTypes sig)) <+>
-        text "against implementation signature" <+>
-        doubleQuotes (sigDoc argTypes retTypes) <+>
-        text "in the implementation of" <+> text name)
-      Just _ -> do
-        cArgs <- foldAccum (checkIdType localScope ctxIns setIns) c { ctxTypeVars = tv } args
-        cRets <- foldAccum (checkIdType localScope ctxLocals setLocals) cArgs rets
-        mapAccum_ (checkBody cRets { ctxModifies = (psigModifies sig), ctxTwoState = True }) bodies
-  where
-    argTypes = map (resolve c . snd) args
-    retTypes = map (resolve c . snd) rets        
-    
-{- Misc -}
-
--- | 'compareType' @c msg t e@
--- Check that @e@ is a valid expression in context @c@ and its type is @t@;
--- in case of type error use @msg@ as a description for @e@
--- (requires type synonyms in t be resolved)
-compareType :: Context -> String -> Type -> Expression -> Checked ()
-compareType c msg t e = do
-  t' <- checkExpression c e
-  if t <==> t' 
-    then return ()
-    else throwTypeError (ctxPos c) (text "Type of" <+> text msg <+> doubleQuotes (typeDoc t') <+> text "is different from" <+> doubleQuotes (typeDoc t))
-    
--- 'checkLefts' @c ids n@ : 
--- Check that there are @n@ @ids@, all @ids@ are unique and denote mutable variables
-checkLefts :: Context -> [Id] -> Int -> Checked ()
-checkLefts c vars n = if length vars /= n 
-  then throwTypeError (ctxPos c) (text "Expected" <+> int n <+> text "left-hand sides and got" <+> int (length vars))
-  else if vars /= nub vars
-    then throwTypeError (ctxPos c) (text "Variable occurs more than once among left-handes of a parallel assignment")
-    else if not (null immutableLhss)
-      then throwTypeError (ctxPos c) (text "Assignment to immutable variable(s):" <+> commaSep (map text immutableLhss))
-      else if not (null invalidGlobals)
-        then throwTypeError (ctxPos c) (text "Assignment to a global variable that is not in the enclosing procedure's modifies clause:" <+> commaSep (map text invalidGlobals))
-        else return ()      
-  where 
-    immutableLhss = vars \\ M.keys (mutableVars c)
-    invalidGlobals = (vars \\ M.keys (ctxLocals c)) \\ ctxModifies c
-  +  typeCheckProgram,
+  exprType,
+  resolve,
+  TypeError (..),
+  typeErrorsDoc,
+  -- * Typing context
+  Context (..),
+  emptyContext,
+  typeNames,
+  globalScope,
+  localScope,
+  mutableVars,
+  allVars,
+  allNames,
+  funProcNames,
+  funSig,
+  procSig,
+  setLocals,
+  enterFunction,
+  enterProcedure,
+  enterQuantified
+) where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.ErrorAccum
+import Language.Boogie.Position
+import Language.Boogie.PrettyPrinter
+import Data.List
+import Data.Maybe
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Control.Monad.Trans.Error
+import Control.Applicative
+import Control.Monad.State
+import Text.PrettyPrint
+
+{- Interface -}
+
+-- | Check program and return type errors if present, and the global typing context otherwise 
+typeCheckProgram :: Program -> Either [TypeError] Context
+typeCheckProgram p = case runState (runErrorT (checkProgram p)) emptyContext of
+  (Left errs, _)  -> Left errs
+  (_, ctx)        -> Right ctx            
+  
+-- | 'exprType' @c expr@ :
+-- Type of @expr@ in context @c@;
+-- fails if expr contains type errors.    
+exprType :: Context -> Expression -> Type
+exprType c expr = case evalState (runErrorT (checkExpression expr)) c of
+  Left _ -> (error . show) (text "encountered ill-typed expression during execution:" <+> exprDoc expr)
+  Right t -> t
+  
+-- | 'enterFunction' @sig formals actuals mRetType c@ :
+-- Local context of function @sig@ with formal arguments @formals@ and actual arguments @actuals@
+-- in a context where the return type is exprected to be @mRetType@ (if known)
+enterFunction :: FSig -> [Id] -> [Expression] -> Context -> Context 
+enterFunction sig formals actuals c = c 
+  {
+    ctxTypeVars = [],
+    ctxIns = M.fromList (zip formals argTypes),
+    ctxLocals = M.empty,
+    ctxModifies = [],
+    ctxTwoState = False,
+    ctxInLoop = False
+  }
+  where 
+    inst = case evalState (runErrorT (fInstance sig actuals)) c of
+      Left _ -> (error . show) (text "encountered ill-typed function application during execution:" <+> 
+        text (fsigName sig) <+> parens (commaSep (map text formals)) <+>
+        text "to actual arguments" <+> parens (commaSep (map exprDoc actuals)))
+      Right sig' -> sig'
+    argTypes = fsigArgTypes inst
+
+-- | 'enterProcedure' @sig def actuals lhss c@ :
+-- Local context of procedure @sig@ with definition @def@ and actual arguments @actuals@
+-- in a call with left-hand sides @lhss@
+enterProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Context -> Context 
+enterProcedure sig def actuals lhss c = c 
+  {
+    ctxTypeVars = [],
+    ctxIns = M.fromList $ zip ins inTypes,
+    ctxLocals = M.union (M.fromList $ zip localNames localTypes) (M.fromList $ zip outs outTypes),
+    ctxModifies = psigModifies sig,
+    ctxTwoState = True,
+    ctxInLoop = False
+  }
+  where
+    ins = pdefIns def
+    outs = pdefOuts def
+    locals = fst (pdefBody def)
+    inst = case evalState (runErrorT (pInstance sig actuals lhss)) c of
+      Left _ -> (error . show) (text "encountered ill-typed procedure call during execution:" <+> 
+        text (psigName sig) <+> text "with actual arguments" <+> parens (commaSep (map exprDoc actuals)) <+>
+        text "and left-hand sides" <+> parens (commaSep (map exprDoc lhss)))
+      Right u -> u
+    inTypes = map (typeSubst inst) (psigArgTypes sig)
+    outTypes = map (typeSubst inst) (psigRetTypes sig)
+    localTypes = map (typeSubst inst . itwType) locals
+    localNames = map itwId locals
+   
+-- | Local context of a quantified expression   
+enterQuantified :: [Id] -> [IdType] -> Context -> Context 
+enterQuantified tv vars c = c' 
+  {
+    ctxIns = foldl addIn (ctxIns c) vars
+  }
+  where
+    c' = c { ctxTypeVars = tv }
+    addIn ins (id, t) = M.insert id (resolve c' t) ins
+    
+{- Context -}
+
+-- | Typing context
+data Context = Context
+  {
+    -- Scope context (specific to an AST node, gets restored when type cher leaves the node):
+      -- Global:
+    ctxTypeConstructors :: Map Id Int,      -- ^ type constructor arity
+    ctxTypeSynonyms :: Map Id ([Id], Type), -- ^ type synonym values
+    ctxGlobals :: Map Id Type,              -- ^ global variable types (type synonyms resolved)
+    ctxConstants :: Map Id Type,            -- ^ constant types (type synonyms resolved)
+    ctxFunctions :: Map Id FSig,            -- ^ function signatures (type synonyms resolved)
+    ctxProcedures :: Map Id PSig,           -- ^ procedure signatures (type synonyms resolved)
+      -- Local:
+    ctxTypeVars :: [Id],                    -- ^ free type variables
+    ctxIns :: Map Id Type,                  -- ^ input parameter types
+    ctxLocals :: Map Id Type,               -- ^ local variable types
+    ctxModifies :: [Id],                    -- ^ variables in the modifies clause of the enclosing procedure
+    ctxLabels :: [Id],                      -- ^ all labels of the enclosing procedure body
+    ctxEncLabels :: [Id],                   -- ^ labels of all enclosing statements
+    ctxTwoState :: Bool,                    -- ^ is the context two-state? (procedure body or postcondition)
+    ctxInLoop :: Bool,                      -- ^ is context inside a loop body?
+    ctxPos :: SourcePos,                    -- ^ position in the source code
+    -- Persistent context (not specific to any node, never gets restored):
+    ctxFreshTVCount :: Integer              -- ^ number of fresh type variables already generated
+  }
+
+-- | Empty context  
+emptyContext = Context {
+    ctxTypeConstructors = M.empty,
+    ctxTypeSynonyms     = M.empty,
+    ctxGlobals          = M.empty,
+    ctxConstants        = M.empty,
+    ctxFunctions        = M.empty,
+    ctxProcedures       = M.empty,
+    ctxTypeVars         = [],
+    ctxIns              = M.empty,
+    ctxLocals           = M.empty,
+    ctxModifies         = [],
+    ctxLabels           = [],
+    ctxEncLabels        = [],
+    ctxTwoState         = False,
+    ctxInLoop           = False,
+    ctxPos              = noPos,
+    ctxFreshTVCount     = 0
+  }
+
+setGlobals g ctx    = ctx { ctxGlobals = g }
+setConstants c ctx  = ctx { ctxConstants = c }
+setTypeVars tv ctx  = ctx { ctxTypeVars = tv }
+setIns i ctx        = ctx { ctxIns = i }
+setLocals l ctx     = ctx { ctxLocals = l }
+setModifies m ctx   = ctx { ctxModifies = m }
+setLabels lbs ctx   = ctx { ctxLabels = lbs }
+setTwoState b ctx   = ctx { ctxTwoState = b }
+setInLoop b ctx     = ctx { ctxInLoop = b }
+setPos p ctx        = ctx { ctxPos = p }
+
+-- | Type constructors and synonyms
+typeNames c = M.keys (ctxTypeConstructors c) ++ M.keys (ctxTypeSynonyms c)
+-- | Global variables and constants
+globalScope c = M.union (ctxGlobals c) (ctxConstants c)
+-- | Input parameters and local variables
+localScope c = M.union (ctxIns c) (ctxLocals c)
+-- | All variables that can be assigned to (local variables and global variables)
+mutableVars c = M.union (ctxGlobals c) (ctxLocals c)
+-- | All variables that can have where clauses (everything except constants)
+allVars c = M.union (localScope c) (ctxGlobals c)
+-- | All variables and constants (local-scope preferred)
+allNames c = M.union (localScope c) (globalScope c)
+-- | Names of functions and procedures
+funProcNames c = M.keys (ctxFunctions c) ++ M.keys (ctxProcedures c)
+-- | Function signature by name
+funSig name c = ctxFunctions c ! name
+-- | Procedure signature by name
+procSig name c = ctxProcedures c ! name
+
+-- | Return a fresh type variable name and a modified context
+genFreshTV c = (freshTVName $ ctxFreshTVCount c, c { ctxFreshTVCount = ctxFreshTVCount c + 1 })
+
+-- | 'locally' @check@ : perform @check@ and then restores the scoped part of the context
+locally :: Typing a -> Typing a
+locally check = do
+  c <- get
+  res <- check `catchError` (\err -> restore c >> throwError err)
+  restore c
+  return res
+  where
+    restore c = do
+      n <- gets ctxFreshTVCount
+      put c { ctxFreshTVCount = n }
+
+{- Errors -}
+
+-- | Type error with a source position and a pretty-printed message
+data TypeError = TypeError SourcePos Doc
+
+instance ErrorList TypeError where
+  listMsg s = [TypeError noPos (text s)]
+
+-- | Pretty-printed type error  
+typeErrorDoc (TypeError pos msgDoc) = text "Type error in" <+> text (show pos) $+$ msgDoc  
+  
+-- | Pretty-printed list of type errors
+typeErrorsDoc errs = (vsep . punctuate newline . map typeErrorDoc) errs
+  
+-- | Throw a single type error
+throwTypeError msgDoc = do
+  pos <- gets ctxPos
+  throwError [TypeError pos msgDoc]
+  
+-- | 'typeMismatch' @doc1 ts1 doc2 ts2 contextDoc@ : throw an error because types @ts1@ do not match @ts2@;
+-- use @doc1@ and @doc2@ to describe @ts1@ and @ts2@ correspondingly; use @contextDoc@ to describe the context of mismatch
+typeMismatch doc1 ts1 doc2 ts2 contextDoc = throwTypeError $ 
+  text "Cannot match" <+> doc1 <+> doubleQuotes (commaSep (map typeDoc ts1)) <+> 
+  text "against" <+>      doc2 <+> doubleQuotes (commaSep (map typeDoc ts2)) <+>
+  contextDoc  
+
+-- | Computation with typing context as state, which can result in either a list of type errors or a    
+type Typing a = ErrorT [TypeError] (State Context) a
+  
+{- Types -}
+  
+-- | Check that a type variable is fresh and add it to context  
+checkTypeVar :: Id -> Typing ()
+checkTypeVar v = do
+  typeNames <- gets typeNames
+  typeVars <- gets ctxTypeVars
+  if v `elem` typeNames
+    then throwTypeError (text v <+> text "already used as a type constructor or synonym")
+    else if  v `elem` typeVars
+      then throwTypeError (text "Multiple decalartions of type variable" <+> text v)
+      else modify $ setTypeVars (v : typeVars)
+
+-- | Check that all type names exist and have correct number of arguments
+checkType :: Type -> Typing ()
+checkType (MapType tv domains range) = do
+  mapAccum_ checkTypeVar tv
+  mapAccum_ (locally . checkType) (domains ++ [range])  
+  if not (null missingTV)
+    then throwTypeError (text "Type variable(s) must occur in the domains or range of the map type:" <+> commaSep (map text missingTV)) 
+    else return ()
+  where
+    missingTV = filter (not . freeInComponents) tv    
+    freeInComponents v = any (v `isFreeIn`) (range : domains)      
+  
+checkType (IdType name args) = do
+  tv <- gets ctxTypeVars
+  tc <- gets ctxTypeConstructors
+  ts <- gets ctxTypeSynonyms
+  cases tv tc ts
+  where
+    cases tv tc ts 
+      | name `elem` tv && null args = return ()
+      | M.member name tc = let n = tc ! name in
+        if n == length args 
+          then mapAccum_ (locally . checkType) args
+          else throwTypeError (text "Wrong number of arguments" <+> int (length args) <+> text "given to the type constructor" <+> text name <+>  parens (text "expected" <+> int n))
+      | M.member name ts = let formals = fst (ts ! name) in
+        if length formals == length args
+          then mapAccum_ (locally . checkType) args
+          else throwTypeError (text "Wrong number of arguments " <+> int (length args) <+> text "given to the type synonym" <+> text name <+> parens (text "expected" <+> int (length formals)))
+      | otherwise = throwTypeError (text "Not in scope: type constructor or synonym" <+> text name)
+checkType _ = return ()
+
+-- | 'resolve' @c t@ : type @t@ with all type synonyms resolved according to binding in @c@
+resolve :: Context -> Type -> Type
+resolve c (MapType tv domains range) = MapType tv (map (resolve c') domains) (resolve c' range)
+  where c' = c { ctxTypeVars = ctxTypeVars c ++ tv }
+resolve c (IdType name args) 
+  | name `elem` ctxTypeVars c = IdType name args
+  | otherwise = case M.lookup name (ctxTypeSynonyms c) of
+    Nothing -> IdType name (map (resolve c) args)
+    Just (formals, t) -> resolve c (typeSubst (M.fromList (zip formals args)) t)
+resolve _ t = t
+
+-- | 'withFreshTV' @tv types@ : generate fresh names for @tv@ and replace their occurrences in @types@
+withFreshTV :: [Id] -> [Type] -> Typing ([Id], [Type])
+withFreshTV tv types = do
+  tv' <- replicateM (length tv) (state $ genFreshTV)
+  let binding = fromTVNames tv tv'
+  return (tv', map (typeSubst binding) types)
+
+-- | 'fInstance' @sig actuals@ :
+-- Function signature @sig@ with type variables instantiated given the actual arguments @actuals@
+fInstance :: FSig -> [Expression] -> Typing FSig
+fInstance (FSig name tv argTypes retType) actuals = do
+  actualTypes <- mapAccum (locally . checkExpression) noType actuals
+  (_, newRetType : newArgTypes) <- withFreshTV tv (retType : argTypes)
+  case unifier [] newArgTypes actualTypes of
+    Nothing -> typeMismatch (text "formal argument types") argTypes (text "actual argument types") actualTypes (text "in the call to" <+> text name)
+    Just u -> return $ FSig name [] (map (typeSubst u) newArgTypes) (typeSubst u newRetType)
+      
+-- | 'pInstance' @sig actuals lhss@ : 
+-- Instantiation of type variables in a procedure @sig@ given the actual arguments @actuals@ and call left-hand sides @lhss@
+-- (type binding is returned in terms of original type variables of @sig@, so that types of locals can be calculated)
+pInstance :: PSig -> [Expression] -> [Expression] -> Typing TypeBinding
+pInstance sig actuals lhss = do
+  actualTypes <- mapAccum (locally . checkExpression) noType actuals
+  lhssTypes <- mapAccum (locally . checkExpression) noType lhss
+  let name = psigName sig
+  let tv = psigTypeVars sig
+  let argTypes = psigArgTypes sig
+  let retTypes = psigRetTypes sig
+  (newTV, newParamTypes) <- withFreshTV tv (argTypes ++ retTypes)
+  let (newArgTypes, newRetTypes) = splitAt (length argTypes) newParamTypes
+  case unifier [] newArgTypes actualTypes of
+    Nothing -> typeMismatch (text "in-parameter types") argTypes (text "actual argument types") actualTypes (text "in the call to" <+> text name)
+    Just u1 -> case unifier [] (map (typeSubst u1) newRetTypes) lhssTypes of
+      Nothing -> typeMismatch (text "out-parameter types") (map (typeSubst (renameTypeVars newTV tv u1)) retTypes) (text "call left-hand side types") lhssTypes (text "in the call to" <+> text name)
+      Just u2 -> return $ renameTypeVars newTV tv (u1 `M.union` u2)
+  
+{- Expressions -}
+
+-- | 'checkExpression' @c expr@ :
+-- Check that @expr@ is a valid expression and return its type
+-- (requires all types in the context be valid and type synonyms be resolved)
+checkExpression :: Expression -> Typing Type
+checkExpression (Pos pos e) = do
+  modify $ setPos pos
+  case e of
+    TT -> return BoolType
+    FF -> return BoolType
+    Numeral n -> return IntType
+    Var id -> checkVar id
+    Application id args -> checkApplication id args
+    MapSelection m args -> checkMapSelection m args
+    MapUpdate m args val -> checkMapUpdate m args val
+    Old e' -> checkOld e'
+    IfExpr cond e1 e2 -> checkIfExpression cond e1 e2
+    Coercion e t -> checkCoercion e t
+    UnaryExpression op e1 -> checkUnaryExpression op e1
+    BinaryExpression op e1 e2 -> checkBinaryExpression op e1 e2
+    Quantified qop tv vars e -> checkQuantified qop tv vars e
+    
+checkVar :: Id -> Typing Type
+checkVar id = do
+  cnames <- gets allNames
+  case M.lookup id cnames of
+    Nothing -> throwTypeError (text "Not in scope: variable or constant" <+> text id)
+    Just t -> return t    
+
+checkApplication :: Id -> [Expression] -> Typing Type
+checkApplication id args = do
+  cfun <- gets ctxFunctions
+  case M.lookup id cfun of
+    Nothing -> throwTypeError (text "Not in scope: function" <+> text id)
+    Just sig -> do
+      inst <- locally $ fInstance sig args
+      return $ fsigRetType inst
+    
+checkMapSelection :: Expression -> [Expression] -> Typing Type
+checkMapSelection m args = do
+  mType <- locally $ checkExpression m
+  selectTypes <- mapAccum (locally . checkExpression) noType args
+  case mType of
+    MapType tv domainTypes rangeType -> do
+      (_, newRangeType : newDomainTypes) <- withFreshTV tv (rangeType : domainTypes)
+      case unifier [] newDomainTypes selectTypes of
+        Nothing -> typeMismatch (text "map domain types") domainTypes (text "map selection types") selectTypes (text "for map" <+> exprDoc m)
+        Just u -> return (typeSubst u newRangeType)
+    t -> do
+      freshRange <- nullaryType <$> state genFreshTV
+      case unifier [] [t] [MapType [] selectTypes freshRange] of
+        -- t is not a free variable:
+        Nothing -> throwTypeError (text "Map selection applied to a non-map" <+> exprDoc m <+> text "of type" <+> doubleQuotes (typeDoc t))
+        -- t is a free variable:
+        Just u -> return $ typeSubst u freshRange
+  
+checkMapUpdate :: Expression -> [Expression] -> Expression -> Typing Type
+checkMapUpdate m args val = do
+  mType <- locally $ checkExpression m
+  selectTypes <- mapAccum (locally . checkExpression) noType args
+  updateType <- locally $ checkExpression val
+  case mType of
+    MapType tv domainTypes rangeType -> do
+      (newTV, (newRangeType : newDomainTypes)) <- withFreshTV tv (rangeType : domainTypes)
+      case unifier [] newDomainTypes selectTypes of
+        Nothing -> typeMismatch (text "map domain types") domainTypes (text "map selection types") selectTypes (text "for map" <+> exprDoc m)
+        Just u1 -> case unifier [] [typeSubst u1 newRangeType] [updateType] of
+          Nothing -> typeMismatch (text "map range type") [typeSubst (renameTypeVars newTV tv u1) rangeType] (text "map update type") [updateType] (text "for map" <+> exprDoc m)
+          Just u2 -> return $ typeSubst (u1 `M.union` u2) mType -- mType does not contain fresh names for tv, so only free type variables that came from outside will be substituted      
+    t -> do
+      case unifier [] [t] [MapType [] selectTypes updateType] of
+        -- t is not a free variable:
+        Nothing -> throwTypeError (text "Map update applied to a non-map" <+> exprDoc m <+> text "of type" <+> doubleQuotes (typeDoc t))
+        -- t is a free variable:
+        Just u -> return $ typeSubst u t
+    
+checkOld :: Expression -> Typing Type    
+checkOld e = do
+  twoState <- gets ctxTwoState
+  if twoState
+    then do
+      modify $ setLocals M.empty
+      locally $ checkExpression e
+    else throwTypeError (text "Old expression in a single state context")    
+    
+checkIfExpression :: Expression -> Expression -> Expression -> Typing Type    
+checkIfExpression cond e1 e2 = do
+  locally $ checkMatch (text "if-expression condition") BoolType cond
+  t1 <- locally $ checkExpression e1
+  t2 <- locally $ checkExpression e2
+  case unifier [] [t1] [t2] of
+    Nothing -> typeMismatch (text "type of then-part") [t1] (text "type of else-part") [t2] (text "in if-expression")
+    Just u -> return $ typeSubst u t1
+  
+checkCoercion :: Expression -> Type -> Typing Type
+checkCoercion e t = do
+  locally $ checkType t
+  t' <- (flip resolve) t <$> get
+  locally $ checkMatch (text "coerced expression") t' e
+  return t'
+    
+checkUnaryExpression :: UnOp -> Expression -> Typing Type
+checkUnaryExpression op e
+  | op == Neg = checkMatch (msg op) IntType e >> return IntType
+  | op == Not = checkMatch (msg op) BoolType e >> return BoolType
+  where 
+    msg op = text "operand to" <+> unOpDoc op
+  
+checkBinaryExpression :: BinOp -> Expression -> Expression -> Typing Type
+checkBinaryExpression op e1 e2
+  | elem op [Plus, Minus, Times, Div, Mod] = matchOperands IntType IntType IntType
+  | elem op [And, Or, Implies, Explies, Equiv] = matchOperands BoolType BoolType BoolType
+  | elem op [Ls, Leq, Gt, Geq] = matchOperands IntType IntType BoolType
+  | elem op [Eq, Neq] = do 
+    ctv <- gets ctxTypeVars; 
+    t1 <- locally $ checkExpression e1; 
+    t2 <- locally $ checkExpression e2;
+    case unifier ctv [t1] [t2] of
+      Nothing -> typeMismatch (text "type of left operand") [t1] (text "type of right operand") [t2] (text "to" <+> binOpDoc op)
+      Just _ -> return BoolType
+  | op == Lc = do 
+    t1 <- locally $ checkExpression e1; 
+    t2 <- locally $ checkExpression e2;
+    case unifier [] [t1] [t2] of
+      Nothing -> typeMismatch (text "type of left operand") [t1] (text "type of right operand") [t2] (text "to" <+> binOpDoc op)
+      Just _ -> return BoolType
+  where 
+    matchOperands t1 t2 ret = do
+      locally $ checkMatch (msgLeft op) t1 e1
+      locally $ checkMatch (msgRight op) t2 e2
+      return ret
+    msgLeft op = text "left operand to" <+> binOpDoc op
+    msgRight op = text "right operand to" <+> binOpDoc op
+    
+checkQuantified :: QOp -> [Id] -> [IdType] -> Expression -> Typing Type
+checkQuantified Lambda tv vars e = do
+  mapAccum_ checkTypeVar tv
+  mapAccum_ (checkIdType localScope ctxIns setIns) vars
+  if not (null missingTV)
+    then throwTypeError (text "Type variable(s) must occur among the types of lambda parameters:" <+> commaSep (map text missingTV)) 
+    else do
+      rangeType <- locally $ checkExpression e
+      return $ MapType tv varTypes rangeType
+  where
+    varTypes = map snd vars
+    missingTV = filter (not . freeInVars) tv    
+    freeInVars v = any (v `isFreeIn`) varTypes      
+checkQuantified qop tv vars e = do
+  mapAccum_ checkTypeVar tv
+  mapAccum_ (checkIdType localScope ctxIns setIns) vars
+  checkMatch (text "scoped expression") BoolType e
+  return BoolType
+    
+{- Statements -}
+
+-- | 'checkStatement' @c st@ :
+-- Check that @st@ is a valid statement
+checkStatement :: Statement -> Typing ()
+checkStatement (Pos pos s) = do
+  modify $ setPos pos
+  case s of
+    Predicate (SpecClause _ _ e) -> checkMatch (text "predicate") BoolType e
+    Havoc vars -> checkLefts (nub vars) (length (nub vars))
+    Assign lhss rhss -> checkAssign lhss rhss
+    Call lhss name args -> checkCall lhss name args
+    CallForall name args -> checkCallForall name args
+    If cond thenBlock elseBlock -> checkIf cond thenBlock elseBlock
+    While cond invs b -> checkWhile cond invs b
+    Goto ids -> checkGoto ids
+    Break Nothing -> checkSimpleBreak
+    Break (Just l) -> checkLabelBreak l
+    _ -> return ()
+
+checkAssign :: [(Id , [[Expression]])] -> [Expression] -> Typing ()
+checkAssign lhss rhss = do
+  locally $ checkLefts (map fst lhss) (length rhss)
+  rTypes <- mapAccum (locally . checkExpression) noType rhss
+  cpos <- gets ctxPos
+  let selectExpr (id, selects) = foldl mapSelectExpr (attachPos cpos (Var id)) selects
+  zipWithAccum_ (\t e -> locally $ checkMatch (text "assignment left-hand side") t e) rTypes (map selectExpr lhss)
+        
+checkCall :: [Id] -> Id -> [Expression] -> Typing ()
+checkCall lhss name args = do
+  cprocs <- gets ctxProcedures
+  case M.lookup name cprocs of
+    Nothing -> throwTypeError (text "Not in scope: procedure" <+> text name)
+    Just sig -> do
+      cmods <- gets ctxModifies
+      let illegalModifies = psigModifies sig \\ cmods
+      if not (null illegalModifies) 
+        then throwTypeError (text "Call modifies a global variable that is not in the enclosing procedure's modifies clause:" <+> commaSep (map text illegalModifies))
+        else do
+          locally $ checkLefts lhss (length $ psigRetTypes sig)
+          pos <- gets ctxPos
+          let lhssExpr = map (attachPos pos . Var) lhss
+          pInstance sig args lhssExpr >> return ()      
+        
+checkCallForall :: Id -> [WildcardExpression] -> Typing ()
+checkCallForall name args = do
+  cprocs <- gets ctxProcedures
+  case M.lookup name cprocs of
+    Nothing -> throwTypeError (text "Not in scope: procedure" <+> text name)
+    Just sig -> if not (null (psigModifies sig)) 
+      then throwTypeError (text "Call forall to a procedure with a non-empty modifies clause")
+      else pInstance sig { psigArgs = concrete (psigArgs sig) } concreteArgs [] >> return ()
+  where
+    concreteArgs = [e | (Expr e) <- args]
+    concrete at = [at !! i | i <- [0..length args - 1], isConcrete (args !! i)]
+    isConcrete Wildcard = False
+    isConcrete (Expr _) = True
+    
+checkIf :: WildcardExpression -> Block -> (Maybe Block) -> Typing ()
+checkIf cond thenBlock elseBlock = report $ do
+  case cond of
+    Wildcard -> return ()
+    Expr e -> accum (locally $ checkMatch (text "branching condition") BoolType e) ()
+  accum (locally $ checkBlock thenBlock) ()
+  case elseBlock of
+    Nothing -> return ()
+    Just b -> accum (locally $ checkBlock b) ()
+    
+checkWhile :: WildcardExpression -> [SpecClause] -> Block -> Typing ()
+checkWhile cond invs body = report $ do
+  case cond of  
+    Wildcard -> return ()
+    Expr e -> accum (locally $ checkMatch (text "loop condition") BoolType e) ()
+  mapAccumA_ (locally . checkMatch (text "loop invariant") BoolType) (map specExpr invs)
+  lift . modify $ setInLoop True
+  accum (checkBlock body) ()
+
+checkGoto :: [Id] -> Typing ()  
+checkGoto ids = do
+  clbs <- gets ctxLabels
+  let unknownLabels = ids \\ clbs
+  if not (null unknownLabels)
+    then throwTypeError (text "Not in scope: label(s)" <+> commaSep (map text unknownLabels))
+    else return ()
+    
+checkSimpleBreak :: Typing ()
+checkSimpleBreak = do
+  inLoop <- gets ctxInLoop
+  if not inLoop
+    then throwTypeError (text "Break statement outside a loop")
+    else return ()
+  
+checkLabelBreak :: Id -> Typing ()
+checkLabelBreak l = do
+  clbs <- gets ctxEncLabels
+  if not (l `elem` clbs)
+    then throwTypeError (text "Break label" <+> text l <+> text "does not label an enclosing statement")
+    else return ()
+  
+{- Blocks -}
+
+-- | 'collectLabels' @block@ : 
+-- Check that all labels in @block@ and nested blocks are unique and add them to the context
+collectLabels :: Block -> Typing ()
+collectLabels block = mapAccum_ checkLStatement block
+  where
+    checkLStatement (Pos pos (ls, st)) = do
+      modify $ setPos pos
+      mapM_ addLabel ls
+      case node st of
+        If _ thenBlock mElseBlock -> do 
+          collectLabels thenBlock
+          case mElseBlock of
+            Nothing -> return ()
+            Just elseBlock -> collectLabels elseBlock
+        While _ _ bodyBlock -> collectLabels bodyBlock
+        _ -> return ()
+    addLabel l = do
+      clbs <- gets ctxLabels
+      if l `elem` clbs
+        then throwTypeError (text "Multiple occurrences of label" <+> text l <+> text "in a procedure body")
+        else modify $ setLabels (l : clbs)
+
+-- | Check every statement in a block
+checkBlock :: Block -> Typing ()    
+checkBlock block = mapAccum_ (locally . checkLStatement) block
+  where
+    checkLStatement (Pos _ (ls, st)) = do
+      modify $ \c -> c { ctxEncLabels = ctxEncLabels c ++ ls }
+      checkStatement st
+    
+{- Declarations -}
+
+-- | Collect type names from type declarations
+collectTypes :: Decl -> Typing ()
+collectTypes (Pos pos d) = do
+  modify $ setPos pos
+  case d of
+    TypeDecl ts -> mapM_ checkTypeDecl ts
+    otherwise -> return ()  
+
+-- | Check uniqueness of type constructors and synonyms, and them in the context  
+checkTypeDecl :: NewType -> Typing ()
+checkTypeDecl (NewType name formals value) = do
+  ctn <- gets typeNames
+  if name `elem` ctn
+    then throwTypeError (text "Multiple declarations of type constructor or synonym" <+> text name)
+    else case value of
+      Nothing -> modify $ \c -> c { ctxTypeConstructors = M.insert name (length formals) (ctxTypeConstructors c) }
+      Just t -> modify $ \c -> c { ctxTypeSynonyms = M.insert name (formals, t) (ctxTypeSynonyms c) }
+
+-- | Check that type arguments of type synonyms are fresh and values are valid types
+checkTypeSynonyms :: Decl -> Typing ()
+checkTypeSynonyms (Pos pos d) = do
+  modify $ setPos pos
+  case d of
+    TypeDecl ts -> mapAccum_ (locally . checkNewType) ts
+    otherwise -> return ()
+  where
+    checkNewType (NewType name formals (Just t)) = do
+      mapAccum_ checkTypeVar formals 
+      checkType t
+    checkNewType _ = return ()
+
+-- | Check if type synonym declarations have cyclic dependences (program is passed for the purpose of error reporting)
+checkCycles :: [Decl] -> Id -> Typing ()
+checkCycles decls id = do
+  typeSynonyms <- gets ctxTypeSynonyms
+  checkCyclesWith typeSynonyms id (value typeSynonyms id)
+  where
+    checkCyclesWith typeSynonyms id t = case t of
+      IdType name args -> do
+        locally $ if M.member name typeSynonyms
+          then if id == name 
+            then do
+              modify $ setPos firstPos
+              throwTypeError (text "Cycle in the definition of type synonym" <+> text id) 
+            else checkCyclesWith typeSynonyms id (value typeSynonyms name)
+          else return ()
+        mapAccum_ (locally . checkCyclesWith typeSynonyms id) args
+      MapType _ domains range -> mapAccum_ (locally . checkCyclesWith typeSynonyms id) (range:domains)
+      _ -> return ()
+    value typeSynonyms name = snd (typeSynonyms ! name)
+    firstPos = head [pos | Pos pos (TypeDecl ts) <- decls, id `elem` map tId ts]
+
+-- | Check variable, constant, function and procedures and add them to context
+checkSignatures :: Decl -> Typing ()
+checkSignatures (Pos pos d) = do
+  modify $ setPos pos
+  case d of
+    VarDecl vars -> mapAccum_ (checkIdType globalScope ctxGlobals setGlobals) (map noWhere vars)
+    ConstantDecl _ ids t _ _ -> mapAccum_ (checkIdType globalScope ctxConstants setConstants) (zip ids (repeat t))
+    FunctionDecl name tv args ret _ -> checkFunctionSignature name tv args ret
+    ProcedureDecl name tv args rets specs _ -> checkProcSignature name tv args rets specs
+    otherwise -> return ()
+
+-- | 'checkIdType' @scope getter setter idType@ : 
+-- Check that declaration @idType@ is fresh in @scope@, and if so add it to @getter@ using @setter@
+checkIdType :: (Context -> Map Id Type) -> (Context -> Map Id Type) -> (Map Id Type -> Context -> Context) -> IdType -> Typing ()
+checkIdType scope getter setter (i, t) = do
+  s <- gets scope
+  if M.member i s
+    then throwTypeError (text "Multiple declarations of variable or constant" <+> text i)
+    else do 
+      locally $ checkType t
+      modify $ \c -> M.insert i (resolve c t) (getter c) `setter` c
+
+-- | Check uniqueness of function name, types of formals and add function to context
+checkFunctionSignature :: Id -> [Id] -> [FArg] -> FArg -> Typing ()
+checkFunctionSignature name tv args ret = do
+  cnames <- gets funProcNames
+  if name `elem` cnames 
+    then throwTypeError (text "Multiple declarations of function or procedure" <+> text name)
+    else do
+      locally checkParams
+      let freeInParams v = any (v `isFreeIn`) (map snd params)
+      let missingTV = filter (not . freeInParams) tv
+      if not (null missingTV) 
+        then throwTypeError (text "Type variable(s) must occur in function arguments or return type:" <+> commaSep (map text missingTV))
+        else do
+          argTypes <- gets $ \c -> map (resolve c . snd) args
+          retType <- gets $ \c -> (resolve c . snd) ret        
+          modify $ addFSig name (FSig name tv argTypes retType) 
+  where
+    params = args ++ [ret]
+    checkParams = do
+      mapAccum_ checkTypeVar tv
+      mapAccum_ checkFArg params      
+    checkFArg (Just id, t) = checkIdType ctxIns ctxIns setIns (id, t)
+    checkFArg (Nothing, t) = locally $ checkType t
+    addFSig name sig c = c { ctxFunctions = M.insert name sig (ctxFunctions c) }
+      
+-- | Check uniqueness of procedure name, types of formals and add procedure to context      
+checkProcSignature :: Id -> [Id] -> [IdTypeWhere] -> [IdTypeWhere] -> [Contract] -> Typing ()
+checkProcSignature name tv args rets specs = do
+  cnames <- gets funProcNames
+  if name `elem` cnames
+    then throwTypeError (text "Multiple declarations of function or procedure" <+> text name)
+    else do
+      locally checkParams
+      let freeInParams v = any (v `isFreeIn`) (map itwType params)
+      let missingTV = filter (not . freeInParams) tv
+      if not (null missingTV) 
+        then throwTypeError(text "Type variable(s) must occur in procedure in- our out-parameters:" <+> commaSep (map text missingTV))
+        else do
+          argTypes <- gets $ \c -> map (mapItwType (resolve c)) args
+          retTypes <- gets $ \c -> map (mapItwType (resolve c)) rets               
+          modify $ addPSig name (PSig name tv argTypes retTypes specs)
+  where
+    params = args ++ rets
+    checkParams = do
+      mapAccum_ checkTypeVar tv
+      mapAccum_ checkPArg params    
+    checkPArg arg = checkIdType ctxIns ctxIns setIns (noWhere arg)    
+    addPSig name sig c = c { ctxProcedures = M.insert name sig (ctxProcedures c) }
+
+-- | Check axioms, function and procedure bodies      
+checkBodies :: Decl -> Typing ()
+checkBodies (Pos pos d) = do
+  modify $ setPos pos
+  case d of
+    VarDecl vars -> mapAccum_ checkWhere vars
+    ConstantDecl _ ids t (Just edges) _ -> locally $ checkParentInfo ids t (map snd edges)
+    AxiomDecl e -> locally $ checkAxiom e
+    FunctionDecl name tv args ret (Just body) -> locally $ checkFunction name tv args body
+    ProcedureDecl name tv args rets specs mb -> locally $ checkProcedure tv args rets specs mb
+    ImplementationDecl name tv args rets bodies -> locally $ checkImplementation name tv args rets bodies
+    otherwise -> return ()
+  
+-- | Check that where-part is a valid boolean expression
+checkWhere :: IdTypeWhere -> Typing ()
+checkWhere var = do
+  locally $ do
+    modify $ setTwoState False
+    checkMatch (text "where clause") BoolType (itwWhere var)
+
+-- | 'checkParentInfo' @ids t parents@ : Check that identifiers in @parents@ are distinct constants of type @t@ and do not occur among @ids@
+checkParentInfo :: [Id] -> Type -> [Id] -> Typing ()
+checkParentInfo ids t parents = if length parents /= length (nub parents)
+  then throwTypeError (text "Parent list contains duplicates:" <+> commaSep (map text parents))
+  else mapAccum_ (locally . checkParent) parents
+  where
+    checkParent p = do
+      cconst <- gets ctxConstants
+      case M.lookup p cconst of
+        Nothing -> throwTypeError (text "Not in scope: constant" <+> text p)
+        Just t' -> case unifier [] [t] [t'] of
+          Nothing -> typeMismatch (text "type of parent" <+> text p) [t'] (text "constant type") [t] Text.PrettyPrint.empty
+          Just _ -> if p `elem` ids
+            then throwTypeError (text "Constant" <+> text p <+> text "is decalred to be its own parent")
+            else return ()    
+
+-- | Check that axiom is a valid boolean expression    
+checkAxiom :: Expression -> Typing ()
+checkAxiom e = do
+  modify $ setGlobals M.empty 
+  checkMatch (text "axiom") BoolType e
+  
+-- | Check that function body is a valid expression of the same type as the function return type
+checkFunction :: Id -> [Id] -> [FArg] -> Expression -> Typing ()
+checkFunction name tv args body = do
+  modify $ setTypeVars tv
+  mapAccum_ addFArg args
+  modify $ setGlobals M.empty
+  retType <- gets $ fsigRetType . funSig name
+  checkMatch (text "function body") retType body
+  where 
+    addFArg (Just id, t) = checkIdType ctxIns ctxIns setIns (id, t)
+    addFArg _ = return ()
+        
+-- | Check where-parts of procedure arguments and statements in its body
+checkProcedure :: [Id] -> [IdTypeWhere] -> [IdTypeWhere] -> [Contract] -> (Maybe Body) -> Typing ()
+checkProcedure tv args rets specs mb = do 
+  modify $ setTypeVars tv
+  mapAccum_ (checkIdType localScope ctxIns setIns) (map noWhere args)
+  locally $ mapAccum_ checkWhere args
+  mapAccum_ (locally . checkMatch (text "precondition") BoolType . specExpr) (preconditions specs)
+  mapAccum_ (checkIdType localScope ctxLocals setLocals) (map noWhere rets)
+  locally $ mapAccum_ checkWhere rets
+  modify $ setTwoState True
+  mapAccum_ (locally . checkMatch (text "postcondition") BoolType . specExpr) (postconditions specs)
+  cglobs <- gets ctxGlobals
+  let invalidModifies = modifies specs \\ M.keys cglobs
+  if not (null invalidModifies)
+    then throwTypeError (text "Identifier in a modifies clause does not denote a global variable:" <+> commaSep (map text invalidModifies))
+    else case mb of
+      Nothing -> return ()
+      Just body -> do
+        modify $ setModifies (modifies specs)
+        checkBody body
+  
+-- | Check procedure body  
+checkBody :: Body -> Typing ()
+checkBody body = do
+  mapAccum_ (checkIdType localScope ctxLocals setLocals) (map noWhere (concat (fst body)))
+  locally $ mapAccum_ checkWhere (concat (fst body))
+  collectLabels (snd body)
+  checkBlock (snd body)
+
+-- | Check that implementation corresponds to a known procedure and matches its signature, then check all bodies
+checkImplementation :: Id -> [Id] -> [IdType] -> [IdType] -> [Body] -> Typing ()  
+checkImplementation name tv args rets bodies = do
+  cprocs <- gets ctxProcedures
+  case M.lookup name cprocs of
+    Nothing -> throwTypeError (text "Not in scope: procedure" <+> text name)
+    Just sig -> do
+      argTypes <- gets $ \c -> map (resolve c . snd) args
+      retTypes <- gets $ \c -> map (resolve c . snd) rets        
+      case unifier [] [psigType sig] [MapType tv argTypes (tupleType retTypes)] of
+        Nothing -> throwTypeError (text "Could not match procedure signature" <+> 
+          doubleQuotes (sigDoc (psigArgTypes sig) (psigRetTypes sig)) <+>
+          text "against implementation signature" <+>
+          doubleQuotes (sigDoc argTypes retTypes) <+>
+          text "in the implementation of" <+> text name)
+        Just _ -> do
+          modify $ setTypeVars tv
+          mapAccum_ (checkIdType localScope ctxIns setIns) args
+          mapAccum_ (checkIdType localScope ctxLocals setLocals) rets
+          modify $ setTwoState True
+          modify $ setModifies (psigModifies sig)
+          mapAccum_ (locally . checkBody) bodies
+          
+{- Program -}
+
+-- | Check program in several passes
+checkProgram :: Program -> Typing ()
+checkProgram (Program decls) = do
+  mapAccum_ collectTypes decls                          -- collect type names from type declarations
+  locally $ mapAccum_ checkTypeSynonyms decls           -- check values of type synonyms
+  typeSynonyms <- gets $ M.keys . ctxTypeSynonyms
+  locally $ mapAccum_ (checkCycles decls) typeSynonyms  -- check that type synonyms do not form a cycle 
+  mapAccum_ checkSignatures decls                       -- check variable, constant, function and procedure signatures
+  mapAccum_ checkBodies decls                           -- check axioms, function and procedure bodies, constant parent info          
+    
+{- Misc -}
+
+-- | 'checkMatch' @msg t e@
+-- Check that @e@ is a valid expression and its type matches @t@;
+-- in case of type error use @msg@ as a description for @e@
+-- (requires type synonyms in t be resolved)
+checkMatch :: Doc -> Type -> Expression -> Typing ()
+checkMatch edoc t e = do
+  t' <- locally $ checkExpression e
+  case unifier [] [t] [t'] of
+    Nothing -> typeMismatch (text "type of" <+> edoc) [t'] (text "expected type") [t] Text.PrettyPrint.empty
+    Just u -> return ()
+    
+-- 'checkLefts' @ids n@ : 
+-- Check that there are @n@ @ids@, all @ids@ are unique and denote mutable variables
+checkLefts :: [Id] -> Int -> Typing ()
+checkLefts vars n = if length vars /= n 
+  then throwTypeError (text "Expected" <+> int n <+> text "left-hand sides and got" <+> int (length vars))
+  else if vars /= nub vars
+    then throwTypeError (text "Variable occurs more than once among left-handes of a parallel assignment")
+    else do
+      mv <- gets $ M.keys . mutableVars
+      let immutableLhss = vars \\ mv
+      if not (null immutableLhss)
+        then throwTypeError (text "Assignment to immutable variable(s):" <+> commaSep (map text immutableLhss))
+        else do
+          clocs <- gets $ M.keys . ctxLocals
+          cmods <- gets ctxModifies
+          let invalidGlobals = (vars \\ clocs) \\ cmods
+          if not (null invalidGlobals)
+            then throwTypeError (text "Assignment to a global variable that is not in the enclosing procedure's modifies clause:" <+> commaSep (map text invalidGlobals))
+            else return ()
+            

@@ -3,11 +3,13 @@   -- * Types
   TypeBinding,
   typeSubst,
+  renameTypeVars,
+  fromTVNames,
   isFreeIn,
+  isTypeVar,
   unifier,
-  oneSidedUnifier,
-  boundUnifier,
-  (<==>),
+  freshTVName,
+  tupleType,  
   -- * Expressions
   freeVarsTwoState,
   freeVars,
@@ -15,14 +17,22 @@   VarBinding,
   exprSubst,
   paramSubst,
+  freeSelections,
+  applications,
   -- * Specs
   preconditions,
   postconditions,
   modifies,
   assumePreconditions,
-  -- * Funstions and procedures
+  assumePostconditions,
+  -- * Functions and procedures
   FSig (..),
+  fsigType,
+  fsigFromType,
   FDef (..),
+  ConstraintSet,
+  AbstractStore,
+  asUnion,
   PSig (..),
   psigParams,
   psigArgTypes,
@@ -30,19 +40,25 @@   psigModifies,
   psigRequires,
   psigEnsures,
+  psigType,
   PDef (..),
+  pdefLocals,
   -- * Code generation
   num, eneg, enot,
   (|+|), (|-|), (|*|), (|/|), (|%|), (|=|), (|!=|), (|<|), (|<=|), (|>|), (|>=|), (|&|), (|||), (|=>|), (|<=>|),
+  conjunction,
   assume,
   -- * Misc
   interval,
   fromRight,
-  mapFst,
-  mapSnd,
-  mapBoth,
+  deleteAll,
+  restrictDomain,
+  removeDomain,
+  mapItwType,
+  anyM,
   changeState,
-  withLocalState
+  withLocalState,
+  internalError
 ) where
 
 import Language.Boogie.AST
@@ -50,10 +66,14 @@ import Language.Boogie.Tokens
 import Data.Maybe
 import Data.List
-import Data.Map (Map)
+import Data.Map (Map, (!))
 import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
 import Control.Applicative
 import Control.Monad.State
+import Control.Monad.Stream
+import Control.Lens
 
 {- Types -}
 
@@ -66,41 +86,56 @@ typeSubst :: TypeBinding -> Type -> Type
 typeSubst _ BoolType = BoolType
 typeSubst _ IntType = IntType
-typeSubst binding (Instance id []) = case M.lookup id binding of
+typeSubst binding (IdType id []) = case M.lookup id binding of
   Just t -> t
-  Nothing -> Instance id []
-typeSubst binding (Instance id args) = Instance id (map (typeSubst binding) args)
+  Nothing -> IdType id []
+typeSubst binding (IdType id args) = IdType id (map (typeSubst binding) args)
 typeSubst binding (MapType bv domains range) = MapType bv (map (typeSubst removeBound) domains) (typeSubst removeBound range)
   where removeBound = deleteAll bv binding
   
--- | 'fromTVNames' @tvs tvs'@ : type binding that replaces type variables @tvs@ with type variables @tvs'@
-fromTVNames :: [Id] -> [Id] -> TypeBinding
-fromTVNames tvs tvs' = M.fromList (zip tvs (map nullaryType tvs'))
-  
--- | @x@ `isFreeIn` @t@ : does @x@ occur as a free type variable in @t@?
--- @x@ must not be a name of a type constructor
+-- | 'renameTypeVars' @tv newTV binding@ : @binding@ with each occurrence of one of @tv@ replaced with corresponding @newTV@ 
+-- (in both domain and range)
+renameTypeVars :: [Id] -> [Id] -> TypeBinding -> TypeBinding
+renameTypeVars tv newTV binding = let
+    tvMap = M.fromList $ zip tv newTV 
+    replace tv = M.findWithDefault tv tv tvMap
+    tvToType = fromTVNames tv newTV
+  in M.map (typeSubst tvToType) (M.mapKeys replace binding)
+    
+-- | @x@ `isFreeIn` @t@ : does @x@ occur free in @t@?
 isFreeIn :: Id -> Type -> Bool
-x `isFreeIn` (Instance y []) = x == y
-x `isFreeIn` (Instance y args) = any (x `isFreeIn`) args
+x `isFreeIn` (IdType y []) = x == y
+x `isFreeIn` (IdType y args) = any (x `isFreeIn`) args
 x `isFreeIn` (MapType bv domains range) = x `notElem` bv && any (x `isFreeIn`) (range:domains)
-_ `isFreeIn` _ = False
+_ `isFreeIn` _ = False  
   
--- | 'unifier' @fv xs ys@ : most general unifier of @xs@ and @ys@ with shared free type variables @fv@
+-- | 'fromTVNames' @tvs tvs'@ : type binding that replaces type variables @tvs@ with type variables @tvs'@
+fromTVNames :: [Id] -> [Id] -> TypeBinding
+fromTVNames tvs tvs' = M.fromList (zip tvs (map nullaryType tvs'))
+
+-- | 'freshTVName @n@ : Fresh type variable with a unique identifier n
+freshTVName n = nonIdChar : (show n)
+
+-- | 'isTypeVar' @contextTypeVars v@ : Is @v@ either one of  @contextTypeVars@ or a freash type variable generated by 'freshTVName'?
+isTypeVar :: [Id] -> Id -> Bool
+isTypeVar contextTypeVars v = head v == nonIdChar || v `elem` contextTypeVars
+    
+-- | 'unifier' @fv xs ys@ : most general unifier of @xs@ and @ys@ with shared free type variables of the context @fv@
 unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBinding
 unifier _ [] [] = Just M.empty
 unifier fv (IntType:xs) (IntType:ys) = unifier fv xs ys
 unifier fv (BoolType:xs) (BoolType:ys) = unifier fv xs ys
-unifier fv ((Instance id1 args1):xs) ((Instance id2 args2):ys) | id1 == id2 = unifier fv (args1 ++ xs) (args2 ++ ys)
-unifier fv ((Instance id []):xs) (y:ys) | id `elem` fv = 
+unifier fv ((IdType id1 args1):xs) ((IdType id2 args2):ys) | id1 == id2 = unifier fv (args1 ++ xs) (args2 ++ ys)
+unifier fv ((IdType id []):xs) (y:ys) | isTypeVar fv id = 
   if id `isFreeIn` y then Nothing 
   else M.insert id y <$> unifier fv (update xs) (update ys)
     where update = map (typeSubst (M.singleton id y))
-unifier fv (x:xs) ((Instance id []):ys) | id `elem` fv = 
+unifier fv (x:xs) ((IdType id []):ys) | isTypeVar fv id = 
   if id `isFreeIn` x then Nothing 
   else M.insert id x <$> unifier fv (update xs) (update ys)
     where update = map (typeSubst (M.singleton id x))
 unifier fv ((MapType bv1 domains1 range1):xs) ((MapType bv2 domains2 range2):ys) =
-  case boundUnifier fv bv1 (range1:domains1) bv2 (range2:domains2) of
+  case forallUnifier fv bv1 (range1:domains1) bv2 (range2:domains2) of
     Nothing -> Nothing
     Just u -> M.union u <$> (unifier fv (update u xs) (update u ys))
   where
@@ -111,52 +146,38 @@ -- New names for type variables @tvs@ that are disjoint from @tvs'@
 -- (if @tvs@ does not have duplicates, then result also does not have duplicates)
 removeClashesWith :: [Id] -> [Id] -> [Id]
-removeClashesWith tvs tvs' = map freshName tvs
+removeClashesWith tvs tvs' = map changeName tvs
   where
     -- new name for tv that does not coincide with any tvs'
-    freshName tv = if tv `elem` tvs' then replicate (level + 1) nonIdChar ++ tv else tv
-    -- maximum number of nonIdChar characters at the beginning of a tvs'; by prepending (level + 1) nonIdChar charactes to tv we make is different from all tvs'
-    level = maximum [fromJust (findIndex (\c -> c /= nonIdChar) id) | id <- tvs']
-
--- | 'oneSidedUnifier' @fv xs tv ys@ : 
--- Most general unifier of @xs@ and @ys@,
--- where only @xs@ contain free variables (@fv@),
--- while @ys@ contain rigid type variables @tv@, which might clash with @fv@
-oneSidedUnifier :: [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding    
-oneSidedUnifier fv xs tv ys = M.map old <$> unifier fv xs (map new ys)
-  where
-    freshTV = tv `removeClashesWith` fv
-    new = typeSubst (fromTVNames tv freshTV)
-    old = typeSubst (fromTVNames freshTV tv)
-
--- | 'boundUnifier' @fv bv1 xs bv2 ys@ :   
+    changeName tv = if tv `elem` tvs' then tv ++ replicate (level + 1) nonIdChar else tv
+    -- maximum number of nonIdChar characters at the end of any tvs or tvs'; 
+    -- by appending (level + 1) nonIdChar charactes to tv we make is different from all tvs' and unchanged tvs
+    level = maximum [fromJust (findIndex (\c -> c /= nonIdChar) (reverse id)) | id <- tvs ++ tvs']
+    
+-- | 'forallUnifier' @fv bv1 xs bv2 ys@ :   
 -- Most general unifier of @xs@ and @ys@,
--- where @bv1@ are bound type variables in @xs@ and @bv2@ are bound type variables in @ys@,
+-- where @bv1@ are universally quantified type variables in @xs@ and @bv2@ are universally quantified type variables in @ys@,
 -- and @fv@ are free type variables of the enclosing context
-boundUnifier :: [Id] -> [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding
-boundUnifier fv bv1 xs bv2 ys = if length bv1 /= length bv2 || length xs /= length ys 
+forallUnifier :: [Id] -> [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding
+forallUnifier fv bv1 xs bv2 ys = if length bv1 /= length bv2 || length xs /= length ys 
   then Nothing
   else case unifier (fv ++ bv1) xs (map withFreshBV ys) of
     Nothing -> Nothing
-    Just u -> if all isFreshBV (M.elems (bound u)) && not (any hasFreshBV (M.elems (free u)))
-      then Just (free u)
-      else Nothing
-    where
-      freshBV = bv2 `removeClashesWith` bv1
-      withFreshBV = typeSubst (fromTVNames bv2 freshBV)
-      -- does a type correspond to one of the fresh bound variables of m2?
-      isFreshBV (Instance id []) = id `elem` freshBV
-      isFreshBV _ = False
-      -- does type t contain any fresh bound variables of m2?
-      hasFreshBV t = any (`isFreeIn` t) freshBV
-      -- binding restricted to free variables
-      free = deleteAll bv1
-      -- binding restricted to bound variables
-      bound = deleteAll (fv \\ bv1)
-      
--- | Semantic equivalence on types
--- (equality up to renaming of bound type variables)
-t1 <==> t2 = isJust (unifier [] [t1] [t2])       
+    Just u -> let (boundU, freeU) = M.partitionWithKey (\k _ -> k `elem` bv1) u
+      in if all isFreshBV (M.elems boundU) && not (any hasFreshBV (M.elems freeU))
+        then Just freeU
+        else Nothing
+  where
+    freshBV = bv2 `removeClashesWith` bv1
+    withFreshBV = typeSubst (fromTVNames bv2 freshBV)
+    -- does a type correspond to one of the renamed bound variables?
+    isFreshBV (IdType id []) = id `elem` freshBV
+    isFreshBV _ = False
+    -- does type t contain any fresh bound variables of m2?
+    hasFreshBV t = any (`isFreeIn` t) freshBV
+
+-- | Internal tuple type constructor (used for representing procedure returns as a single type)
+tupleType ts = IdType "*Tuple" ts
   
 {- Expressions -}
 
@@ -168,14 +189,14 @@ freeVarsTwoState' TT = ([], [])
 freeVarsTwoState' (Numeral _) = ([], [])
 freeVarsTwoState' (Var x) = ([x], [])
-freeVarsTwoState' (Application name args) = mapBoth (nub . concat) (unzip (map freeVarsTwoState args))
-freeVarsTwoState' (MapSelection m args) =  mapBoth (nub . concat) (unzip (map freeVarsTwoState (m : args)))
-freeVarsTwoState' (MapUpdate m args val) =  mapBoth (nub . concat) (unzip (map freeVarsTwoState (val : m : args)))
+freeVarsTwoState' (Application name args) = over both (nub . concat) (unzip (map freeVarsTwoState args))
+freeVarsTwoState' (MapSelection m args) =  over both (nub . concat) (unzip (map freeVarsTwoState (m : args)))
+freeVarsTwoState' (MapUpdate m args val) =  over both (nub . concat) (unzip (map freeVarsTwoState (val : m : args)))
 freeVarsTwoState' (Old e) = let (state, old) = freeVarsTwoState e in ([], state ++ old)
-freeVarsTwoState' (IfExpr cond e1 e2) = mapBoth (nub . concat) (unzip [freeVarsTwoState cond, freeVarsTwoState e1, freeVarsTwoState e2])
+freeVarsTwoState' (IfExpr cond e1 e2) = over both (nub . concat) (unzip [freeVarsTwoState cond, freeVarsTwoState e1, freeVarsTwoState e2])
 freeVarsTwoState' (Coercion e _) = freeVarsTwoState e
 freeVarsTwoState' (UnaryExpression _ e) = freeVarsTwoState e
-freeVarsTwoState' (BinaryExpression _ e1 e2) = mapBoth (nub . concat) (unzip [freeVarsTwoState e1, freeVarsTwoState e2])
+freeVarsTwoState' (BinaryExpression _ e1 e2) = over both (nub . concat) (unzip [freeVarsTwoState e1, freeVarsTwoState e2])
 freeVarsTwoState' (Quantified _ _ boundVars e) = let (state, old) = freeVarsTwoState e in (state \\ map fst boundVars, old)
 
 -- | Free variables in an expression, in current state
@@ -221,8 +242,47 @@ paramSubst :: PSig -> PDef -> Expression -> Expression  
 paramSubst sig def = if not (pdefParamsRenamed def) 
   then id 
-  else exprSubst (paramBinding sig def)   
+  else exprSubst (paramBinding sig def)
+  
+-- | 'freeSelections' @expr@ : all map selections that occur in @expr@, where the map is a free variable
+freeSelections :: Expression -> [(Id, [Expression])]
+freeSelections expr = freeSelections' $ node expr
 
+freeSelections' FF = []
+freeSelections' TT = []
+freeSelections' (Numeral _) = []
+freeSelections' (Var x) = []
+freeSelections' (Application name args) = nub . concat $ map freeSelections args
+freeSelections' (MapSelection m args) = case node m of 
+ Var name -> (name, args) : (nub . concat $ map freeSelections args)
+ _ -> nub . concat $ map freeSelections (m : args)
+freeSelections' (MapUpdate m args val) =  nub . concat $ map freeSelections (val : m : args)
+freeSelections' (Old e) = internalError "freeSelections should only be applied in single-state context"
+freeSelections' (IfExpr cond e1 e2) = nub . concat $ [freeSelections cond, freeSelections e1, freeSelections e2]
+freeSelections' (Coercion e _) = freeSelections e
+freeSelections' (UnaryExpression _ e) = freeSelections e
+freeSelections' (BinaryExpression _ e1 e2) = nub . concat $ [freeSelections e1, freeSelections e2]
+freeSelections' (Quantified _ _ boundVars e) = let boundVarNames = map fst boundVars 
+  in [(m, args) | (m, args) <- freeSelections e, m `notElem` boundVarNames]
+  
+-- | 'applications' @expr@ : all function applications that occur in @expr@
+applications :: Expression -> [(Id, [Expression])]
+applications expr = applications' $ node expr
+
+applications' FF = []
+applications' TT = []
+applications' (Numeral _) = []
+applications' (Var x) = []
+applications' (Application name args) = (name, args) : (nub . concat $ map applications args)
+applications' (MapSelection m args) = nub . concat $ map applications (m : args)
+applications' (MapUpdate m args val) =  nub . concat $ map applications (val : m : args)
+applications' (Old e) = internalError "applications should only be applied in single-state context"
+applications' (IfExpr cond e1 e2) = nub . concat $ [applications cond, applications e1, applications e2]
+applications' (Coercion e _) = applications e
+applications' (UnaryExpression _ e) = applications e
+applications' (BinaryExpression _ e1 e2) = nub . concat $ [applications e1, applications e2]
+applications' (Quantified _ _ _ e) = applications e  
+
 {- Specs -}
 
 -- | 'preconditions' @specs@ : all precondition clauses in @specs@  
@@ -252,6 +312,13 @@   where
     assumePrecondition (Requires _ e) = Requires True e
     assumePrecondition c = c
+    
+-- | Make all postconditions in contracts free  
+assumePostconditions :: PSig -> PSig
+assumePostconditions sig = sig { psigContracts = map assumePostcondition (psigContracts sig) }
+  where
+    assumePostcondition (Ensures _ e) = Ensures True e
+    assumePostcondition c = c    
 
 {- Functions and procedures -}
 
@@ -263,12 +330,33 @@     fsigRetType :: Type     -- ^ Return type
   }
   
+-- | Function signature as a map type  
+fsigType sig = MapType (fsigTypeVars sig) (fsigArgTypes sig) (fsigRetType sig)
+
+-- | Map type as a function signature 
+fsigFromType (MapType tv domainTypes rangeType) = FSig "" tv domainTypes rangeType 
+
+instance Eq FSig where
+  s1 == s2 = fsigName s1 == fsigName s2
+  
 -- | Function definition
 data FDef = FDef {
-    fdefArgs  :: [Id],       -- ^ Argument names (in the same order as 'fsigArgTypes' in the corresponding signature)
-    fdefGuard :: Expression, -- ^ Condition under which this definition applies    
-    fdefBody  :: Expression  -- ^ Body 
+    fdefName  :: Id,            -- ^ Entity to which the definition belongs
+    fdefTV    :: [Id],          -- ^ Type variables
+    fdefArgs  :: [IdType],      -- ^ Arguments (types may be less general than in the corresponding signature)
+    fdefGuard :: Expression,    -- ^ Condition under which the definition applies
+    fdefBody  :: Expression     -- ^ Body 
   }
+
+-- | Constraint set: contains a list of definitions and a list of constraints
+type ConstraintSet = ([FDef], [FDef])
+
+-- | Abstract store: maps names to their constraints
+type AbstractStore = Map Id ConstraintSet
+
+-- | Union of abstract stores (values at the same key are concatenated)
+asUnion :: AbstractStore -> AbstractStore -> AbstractStore
+asUnion s1 s2 = M.unionWith (\(d1, c1) (d2, c2) -> (d1 ++ d2, c1 ++ c2)) s1 s2
  
 -- | Procedure signature 
 data PSig = PSig {
@@ -279,28 +367,37 @@     psigContracts :: [Contract]   -- ^ Contracts
   }
   
+instance Eq PSig where
+  s1 == s2 = psigName s1 == psigName s2  
+  
 -- | All parameters of a procedure signature 
 psigParams sig = psigArgs sig ++ psigRets sig
 -- | Types of in-parameters of a procedure signature
 psigArgTypes = (map itwType) . psigArgs
 -- | Types of out-parameters of a procedure signature
 psigRetTypes = (map itwType) . psigRets
+-- | Procedure signature as a map type
+psigType sig = MapType (psigTypeVars sig) (psigArgTypes sig) (tupleType $ psigRetTypes sig) 
 -- | Modifies clauses of a procedure signature
 psigModifies = modifies . psigContracts
 -- | Preconditions of a procedure signature
 psigRequires = preconditions . psigContracts
 -- | Postconditions of a procedure signature
-psigEnsures = postconditions . psigContracts    
+psigEnsures = postconditions . psigContracts
   
 -- | Procedure definition;
 -- a single procedure might have multiple definitions (one per body)
 data PDef = PDef { 
-    pdefIns :: [Id],            -- ^ In-parameter names (in the same order as 'psigArgs' in the corresponding signature)
-    pdefOuts :: [Id],           -- ^ Out-parameter names (in the same order as 'psigRets' in the corresponding signature)
-    pdefParamsRenamed :: Bool,  -- ^ Are any parameter names in this definition different for the procedure signature? (used for optimizing parameter renaming, True is a safe default)
-    pdefBody :: BasicBody,      -- ^ Body
-    pdefPos :: SourcePos        -- ^ Location of the (first line of the) procedure definition in the source
+    pdefIns :: [Id],                  -- ^ In-parameter names (in the same order as 'psigArgs' in the corresponding signature)
+    pdefOuts :: [Id],                 -- ^ Out-parameter names (in the same order as 'psigRets' in the corresponding signature)
+    pdefParamsRenamed :: Bool,        -- ^ Are any parameter names in this definition different for the procedure signature? (used for optimizing parameter renaming, True is a safe default)
+    pdefBody :: BasicBody,            -- ^ Body
+    pdefConstraints :: AbstractStore, -- ^ Constraints on local names
+    pdefPos :: SourcePos              -- ^ Location of the (first line of the) procedure definition in the source
   }
+  
+-- | All local names of a procedure definition  
+pdefLocals def = pdefIns def ++ pdefOuts def ++ map itwId (fst (pdefBody def))
 
 {- Code generation -}
 
@@ -323,6 +420,9 @@ e1 |=>|   e2 = inheritPos2 (BinaryExpression Implies) e1 e2
 e1 |<=>|  e2 = inheritPos2 (BinaryExpression Equiv) e1 e2
 assume e = attachPos (position e) (Predicate (SpecClause Inline True e))
+
+conjunction [] = gen TT
+conjunction es = foldl1 (|&|) es
   
 {- Misc -}
 
@@ -337,19 +437,41 @@ deleteAll :: Ord k => [k] -> Map k a -> Map k a
 deleteAll keys m = foldr M.delete m keys
 
-mapFst f (x, y) = (f x, y)
-mapSnd f (x, y) = (x, f y)
-mapBoth f (x, y) = (f x, f y)
+-- | 'restrictDomain' @keys m@ : map @m@ restricted on the set of keys @keys@
+restrictDomain :: Ord k => Set k -> Map k a -> Map k a
+restrictDomain keys m = M.filterWithKey (\k _ -> k `S.member` keys) m
 
+-- | 'removeDomain' @keys m@ : map @m@ with the set of keys @keys@ removed from its domain
+removeDomain :: Ord k => Set k -> Map k a -> Map k a
+removeDomain keys m = M.filterWithKey (\k _ -> k `S.notMember` keys) m
+
+mapItwType f (IdTypeWhere i t w) = IdTypeWhere i (f t) w
+
+-- | Monadic version of 'any' (executes boolean-valued computation for all arguments in a list until the first True is found) 
+anyM :: Monad m => (a -> m Bool) -> [a] -> m Bool
+anyM _ [] = return False
+anyM pred (x : xs) = do
+  res <- pred x
+  if res then return True else anyM pred xs
+  
+-- | Monadic version of 'all' (executes boolean-valued computation for all arguments in a list until the first False is found) 
+allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
+allM _ [] = return True
+allM pred (x : xs) = do
+  res <- pred x
+  if not res then return False else allM pred xs  
+
 -- | Execute a computation with state of type @t@ inside a computation with state of type @s@
-changeState :: (s -> t) -> (t -> s -> s) -> State t a -> State s a
+changeState :: Monad m => (s -> t) -> (t -> s -> s) -> StateT t m a -> StateT s m a
 changeState getter modifier e = do
   st <- gets getter
-  let (res, st') = runState e st
+  (res, st') <- lift $ runStateT e st
   modify $ modifier st'
   return res  
 
 -- | 'withLocalState' @localState e@ :
 -- Execute @e@ in current state modified by @localState@, and then restore current state
-withLocalState :: (s -> t) -> State t a -> State s a
+withLocalState :: Monad m => (s -> t) -> StateT t m a -> StateT s m a
 withLocalState localState e = changeState localState (flip const) e
+      
+internalError msg = error $ "Internal interpreter error (consider submitting a bug report):\n" ++ msg      

@@ -3,7 +3,9 @@ import Language.Boogie.Parser
 import Language.Boogie.PrettyPrinter
 import Language.Boogie.TypeChecker
-import Language.Boogie.Interpreter
+import Language.Boogie.Interpreter hiding (TestCase)
+import qualified Language.Boogie.Interpreter as I
+import Language.Boogie.Generator
 import Data.Map (Map, (!))
 import qualified Data.Map as M
 import System.FilePath
@@ -28,12 +30,22 @@   testCase (typeCheckerFailure 3)   "IfThenElse",
   testCase (typeCheckerFailure 4)   "Lambda",
   testCase (typeCheckerFailure 12)  "UpdateExprTyping",
-  testCase (typeCheckerFailure 1)   "TypeVarClash"
+  testCase (typeCheckerFailure 1)   "TypeVarClash",
+  testCase (typeCheckerFailure 8)   "GenericReturn",
+  testCase (typeCheckerFailure 3)   "MissingTV",
+  testCase typeCheckerSuccess       "DafnyPrelude",
+  testCase typeCheckerSuccess       "VccPrelude"
   ]
 
 interpreterTests = TestLabel "Interpreter" $ TestList [
   testCase interpreterSuccess "NoGuards",
-  testCase interpreterSuccess "EmptyDomains"
+  testCase interpreterSuccess "EmptyDomains",
+  testCase interpreterSuccess "MapInit",
+  testCase interpreterSuccess "MapLocals",
+  testCase interpreterSuccess "OldND",
+  testCase interpreterSuccess "OldMaps",
+  testCase interpreterSuccess "MapEquality",
+  testCase interpreterSuccess "Constraints"
   ]
   
 -- | Directory with test programs  
@@ -66,7 +78,7 @@   parseResult <- parseFromFile program file
   case parseResult of
     Left parseErr -> assertFailure (show parseErr)
-    Right p -> case checkProgram p of
+    Right p -> case typeCheckProgram p of
       Left typeErrs -> let m = length typeErrs in assertBool ("Expected " ++ show n ++ " type errors and got " ++ show m) (m == n)
       Right context -> assertFailure ("Expected " ++ show n ++ " type errors and got 0")
       
@@ -75,7 +87,7 @@   parseResult <- parseFromFile program file
   case parseResult of
     Left parseErr -> assertFailure (show parseErr)
-    Right p -> case checkProgram p of
+    Right p -> case typeCheckProgram p of
       Left typeErrs -> assertFailure (show (typeErrorsDoc typeErrs))
       Right context -> return ()
       
@@ -84,9 +96,9 @@   parseResult <- parseFromFile program file
   case parseResult of
     Left parseErr -> assertFailure (show parseErr)
-    Right p -> case checkProgram p of
+    Right p -> case typeCheckProgram p of
       Left typeErrs -> assertFailure (show (typeErrorsDoc typeErrs))
-      Right context -> case executeProgram p context entryPoint of
-        Left err -> assertFailure (show err)
-        Right env -> return ()
+      Right context -> case (head . filter (not . isInvalid)) (executeProgram p context (exhaustiveGenerator Nothing) Nothing entryPoint) of
+        I.TestCase _ _ (Just err) -> assertFailure (show err)
+        otherwise -> return ()
 

@@ -1,5 +1,5 @@ name:                language-boogie
-version:             0.1.1
+version:             0.2
 synopsis:            Interpreter and language infrastructure for Boogie.
 description:         Boogaloo is an interpreter and run-time assertion checker for the Boogie intermediate verification language.
                      The package also provides a language infrastructure library, including a Boogie AST, parser, type checker, and pretty-printer.
@@ -26,19 +26,19 @@   Default:     False
 
 library
-  exposed-modules:     Language.Boogie.Util, Language.Boogie.TypeChecker, Language.Boogie.Tokens, Language.Boogie.Tester, Language.Boogie.PrettyPrinter, Language.Boogie.Position, Language.Boogie.Parser, Language.Boogie.Interpreter, Language.Boogie.BasicBlocks, Language.Boogie.AST, Language.Boogie.DataFlow, Language.Boogie.NormalForm, Language.Boogie.Intervals
+  exposed-modules:     Language.Boogie.Util, Language.Boogie.TypeChecker, Language.Boogie.Tokens, Language.Boogie.PrettyPrinter, Language.Boogie.Position, Language.Boogie.Parser, Language.Boogie.NormalForm, Language.Boogie.Intervals, Language.Boogie.Interpreter, Language.Boogie.Heap, Language.Boogie.Generator, Language.Boogie.ErrorAccum, Language.Boogie.Environment, Language.Boogie.BasicBlocks, Language.Boogie.AST
   -- other-modules:       
-  build-depends:       base ==4.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, containers ==0.4.*, mtl ==2.1.*, pretty ==1.1.*, parsec ==3.1.*, transformers ==0.3.*
-  
+  build-depends:       base ==4.*, random ==1.0.*, containers >=0.4 && <0.6, mtl ==2.1.*, pretty ==1.1.*, parsec ==3.1.*, transformers ==0.3.*, stream-monad ==0.4.*, random ==1.0.*, lens ==3.7.*
+    
 executable boogaloo
   main-is:             Boogaloo.hs             
-  build-depends:       base ==4.*, language-boogie ==0.1.*, containers ==0.4.*, parsec ==3.1.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*  
+  build-depends:       base ==4.*, language-boogie ==0.2.*, containers >=0.4 && <0.6, parsec ==3.1.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*, stream-monad ==0.4.*, ansi-terminal ==0.5.*, random ==1.0.*, lens ==3.7.*
   If !flag(boogaloo)
     buildable: False  
   
 executable boogaloo-tests
   main-is:             Tests.hs
-  build-depends:       base ==4.*, language-boogie ==0.1.*, containers ==0.4.*, filepath ==1.3.*, parsec ==3.1.*, HUnit ==1.2.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*    
+  build-depends:       base ==4.*, language-boogie ==0.2.*, containers >=0.4 && <0.6, filepath ==1.3.*, parsec ==3.1.*, HUnit ==1.2.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*, stream-monad ==0.4.*, random ==1.0.*, lens ==3.7.*
   If !flag(tests)
     buildable: False