MODULE {RulerExpr} {} {}

PRAGMA gendatas
PRAGMA gentypesigs
PRAGMA gencatas
PRAGMA gensems

optpragmas
{
{-# OPTIONS_GHC -fglasgow-exts -XScopedTypeVariables #-}
}

imports
{
import UU.Scanner.Position
import Control.Monad.RWS.Strict
import Control.Monad.Error
import Data.Set(Set)
import qualified Data.Set as Set
import Data.Map(Map)
import qualified Data.Map as Map
import Data.IntMap(IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet(IntSet)
import qualified Data.IntSet as IntSet
import Data.Sequence(Seq)
import qualified Data.Sequence as Seq
import Data.Foldable(toList)
import Data.Typeable
import Data.Monoid
import Data.Maybe
import System.IO
import System.IO.Unsafe
import Opts
import Control.Monad.Identity
import Control.Monad.State.Strict
import Control.Monad.Reader
import Data.List(intersperse)
import Data.Char
import Data.List
}


DATA ExprAGItf
  | AGItf
      expr : Expr

TYPE Stmts = [Stmt]
DATA Stmt
  | Inst
      pos    : Pos
      expr   : Expr
      nm     : Ident
  | Establish
      pos    : Pos
      nm     : Ident
      mbLvl  : {Maybe Level}
  | Equiv
      pos    : Pos
      left   : Expr
      right  : Expr
  | Bind
      pos    : Pos
      left   : Expr
      right  : Expr
  | Fresh
      pos    : Pos
      nms    : {[Ident]}
  | Eval
      pos    : Pos
      expr   : Expr
  | Nop
      pos    : Pos
  | Abstract
      pos    : Pos
      stmt   : Stmt  -- can only be bind/unify + deal with readyness seperately + deal with hierarchy override seperately

TYPE Exprs = [Expr]
DATA Expr
  | Var
      mode   : Mode
      nm     : Ident
  | Field
      fld    : Ident
      nm     : Ident
  | AbstractField
      meta   : Meta
      nm     : Ident
  | Prim
      pos    : Pos
      val    : PrimVal
  | Seq
      stmts  : Stmts
      expr   : Expr
  | Derivation
      pos    : Pos
      visits : Order
      params : Params
      inner  : Ident
      level  : Level
      alts   : Alts
  | External
      pos    : Pos
      nm     : Ident
      params : Params
      level  : Level
  | Merge
      pos    : Pos
      exprs  : Exprs
  | Inherit
      pos    : Pos
      expr   : Expr
      exprs  : Exprs

DATA Meta
  | Any    pos : Pos
  | All    pos : Pos
  | Succ   pos : Pos
  | Pred   pos : Pos
  | Last   pos : Pos
  | First  pos : Pos

DATA Order
  | Relative
      visits : {[Ident]}

DATA Mode
  | Ref
  | Def

DATA Level
  | Intro
  | Skip
  | Hide
  | Abstract
      name  : Ident

TYPE Params = [Param]
DATA Param
  | Input
      visit   : Ident
      inputs  : {[Ident]}
  | Output
      visit   : Ident
      outputs : {[Ident]}

TYPE Scopes = [Scope]
DATA Scope
  | Requires
      inputs  : {[Ident]}
  | Exposes
      outputs : {[Ident]}

TYPE Alts = [Alt]
DATA Alt
  | Alt
      nm     : Ident
      scopes : Scopes
      stmts  : Stmts

SET AllAlts   = Alts Alt
SET AllParams = Params Param
SET AllExprs  = Exprs Expr
SET AllStmts  = Stmts Stmt

DERIVING * : Show, Eq, Ord

--
-- Values
--
-- Performance note: a ValueOpaque may be duplicated many times.
-- This would normally not be a problem, except that it stores a
-- cache of the free variables. Perhaps it is better to actually put a
-- guess-number in the ValueOpaque and reference the cache through
-- this indirection (which would ensure sharing).

{
data Value
  = forall a . RulerValue a => ValueOpaque !Guess !a !IntSet  -- a unique identifier, the actual value, and a cache of the fgv
  | ValueClosure { closureLevelOpt :: !Level
                 , closureLabels   :: !(Set Pos)
                 , closureAlts     :: ![ClosureAlt]
                 , closureOrder    :: ![[Ident]]
                 }
  | ValueThunk { thunkId       :: !Guess
               , thunkClosure  :: !Value
               , thunkLevelOpt :: !Level
               , thunkLabels   :: !(Set Pos)
               , thunkOrder    :: ![Ident]
               , thunkParams   :: !Params
               , thunkBindings :: !(Map Ident Value)
               , thunkBranch   :: !Value
               , thunkVisits   :: !Value
               }
  | ValueExternClosure { extClosureLevelOpt :: !Level
                       , extClosureIdent    :: !Ident
                       , extClosureParams   :: !Params
                       }
  | ValueExternThunk { extThunkId          :: !Guess
                     , extThunkLevelOpt    :: !Level
                     , extThunkIdent       :: !Ident
                     , extThunkParams      :: !Params
                     , extThunkBindings    :: !(Map Ident Value)
                     , extThunkEstablished :: !Value
                     , extThunkOutcome     :: !Value
                     }
  | ValueGuess !Guess
  | ValuePlaceholder !PlaceType
  deriving Typeable

-- represents a single visit to the derivation, giving the name of the visit,
-- the list of remaining statments, and a value representing the next visit.
data Visit = Visit !Ident ![(Ident,Value)] !(Seq Message) !Value | Finish !Status
  deriving (Show, Typeable, Eq, Ord)

data Message = NotifyMsg !String | ErrorMsg !String
  deriving (Typeable, Eq, Ord)

-- the fixed branch, if any
-- contains the selected branch names and the segment of statements for this
-- branch.
data Branch
  = Branch Ident Segment
  deriving (Typeable, Show, Eq, Ord)

data Status = Success | Failure !String deriving (Show, Typeable, Eq, Ord)

data PlaceType = Initialized | Defined | Bottom (Maybe PlaceType) -- bottom stores the original place type that may have been associated to the guess
  deriving (Eq, Ord, Show, Typeable)  -- order: initialized < defined < bottom

-- an alternative of some derivation stored in the closure with environment information
-- the closure-alts are nested. This is due to inheritance between closures.
-- The Ident is the "innername" for this block.
data ClosureAlt
  = ClosureAlt !Params !Ident !(Map Ident Value) !Alt ![ClosureAlt]
  deriving (Show, Typeable)

-- A segment contains a list of statements and a list of substatements
-- the total structure forms a tree of which the next statement to execute is
-- found by an inorder traversal of the tree
data Segment
  = Segment ![ThunkStmt] ![Segment]
  deriving (Show, Typeable, Eq, Ord)

data ThunkStmt
  = ThunkStmt !(Map Ident Value) !Value !Stmt  -- the value indicates if the stmt has already been applied
  deriving (Typeable, Eq, Ord)

instance Show ThunkStmt where
  show (ThunkStmt _ _ s) = show (stmtPos s)

instance Show Value where
  show (ValueOpaque _ v _)                 = "(" ++ show v ++ ")"
  show (ValueClosure _ lbls _ _)           = "<closure:" ++ show (Set.toList lbls) ++ ">"
  show (ValueThunk g _ _ lbls _ _ _ _ _)   = "<thunk:" ++ show g ++ "@" ++ show (Set.toList lbls) ++ ">"
  show (ValueExternClosure _ nm _)         = "<ext-closure:" ++ show nm ++ ">"
  show (ValueExternThunk g _ nm _ _ _ _)   = "<ext-thunk:" ++ show g ++ "@" ++ show nm ++ ">"
  show (ValueGuess g)                      = "#" ++ show g
  show (ValuePlaceholder (Bottom _))       = "!bottom"
  show (ValuePlaceholder Defined)          = "!defined"
  show (ValuePlaceholder Initialized)      = "!init"

instance Eq Value where
  (==) = error "(==) not allowed on Value"

instance Ord Value where
  compare = error "compare not allowed on Value"

instance Eq Pos where
  p1 == p2 = line p1 == line p2 && column p1 == column p2

instance Ord Pos where
  compare p1 p2 = compare [l1,c1] [l2,c2]
    where
      l1 = line p1
      l2 = line p2
      c1 = column p1
      c2 = column p2

instance Show Message where
  show (NotifyMsg s) = s
  show (ErrorMsg s) = "! " ++ s

-- smart constructor for values in the I monad
mkOpaque :: RulerValue a => a -> I Value
mkOpaque v
  = do vars <- fgv IntSet.empty v
       g    <- nextUnique
       return $ ValueOpaque g v vars

-- smart constructor for values that are not allowed to be storing
-- guesses that are still acting as guesses.
-- i.e. fgv computations do not see these guesses anymore.
mkFullyOpaque :: RulerValue a => a -> Value
mkFullyOpaque v = ValueOpaque (-1) v IntSet.empty

visitIdentMain :: Ident
visitIdentMain = ident "__main"

-- Guess pointing to the root of the main derivation
rootGuess :: Guess
rootGuess = 1

-- extract the name of the alternative
altName :: ClosureAlt -> Ident
altName (ClosureAlt _ _ _ (Alt_Alt nm _ _) _) = nm

metaPos :: Meta -> Pos
metaPos (Meta_Any pos)   = pos
metaPos (Meta_All pos)   = pos
metaPos (Meta_Succ pos)  = pos
metaPos (Meta_Pred pos)  = pos
metaPos (Meta_Last pos)  = pos
metaPos (Meta_First pos) = pos
}


--
-- Identifiers
--

{
data Ident
  = Ident String Pos
  deriving Typeable

identName :: Ident -> String
identName (Ident nm _) = nm

identPos :: Ident -> Pos
identPos (Ident _ pos) = pos

ident :: String -> Ident
ident nm = Ident nm noPos

instance Show Ident where
  show (Ident nm _) = nm

instance Eq Ident where
  (Ident nmA _) == (Ident nmB _) = nmA == nmB

instance Ord Ident where
  compare (Ident nmA _) (Ident nmB _) = compare nmA nmB

explainIdent :: Ident -> String
explainIdent ident = show ident ++ " {" ++ explainPos (identPos ident) ++ "}"

explainPos :: Pos -> String
explainPos (Pos l c file) = file ++ ":" ++ show l ++ "," ++ show c

explainBindings :: Map Ident Value -> String
explainBindings = show . Map.assocs
}


--
-- Unification
--

{
type Guess = Int
newtype IndInfo = IndInfo Guess  -- hiding the guess details
  deriving (Show, Typeable, Eq, Ord)

data PrimVal = forall v . RulerValue v => PrimVal v

instance Show PrimVal where
  show (PrimVal v) = show v

instance Eq PrimVal where
  (==) = error "no (==) on PrimVals allowed"

instance Ord PrimVal where
  compare = error "no compare on PrimVals allowed"

class (Typeable a, Show a, Eq a, Ord a, Tabular a) => RulerValue a where
  unify           :: a -> a -> I ()
  unifyS          :: a -> a -> I ()
  fgv             :: IntSet -> a -> I IntSet
  fgvS            :: IntSet -> a -> I IntSet
  dgv             :: a -> I IntSet
  dgvS            :: a -> I IntSet
  expAll          :: (Functor m, Monad m) => (Int -> m (Maybe Value)) -> a -> m a
  expAllS         :: (Functor m, Monad m) => (Int -> m (Maybe Value)) -> a -> m a
  toIndirection   :: IndInfo -> Maybe a -> I a
  fromIndirection :: a -> (Maybe IndInfo, Maybe a)
  rvCast          :: RulerValue b => b -> Maybe a  -- order is important!
  
  -- define unifyS and let unify handle the "var" cases.
  -- unless your data type does not have var cases. In
  -- that case, let unifyS result in an error and override
  -- unify.
  -- Important: always call *unify* and not unifyS, even
  -- from the body of unifyS.
  unify a1 a2
    | b1 && b2  = unifValue (ValueGuess g1) (ValueGuess g2)
    | b1        = assign (ValueGuess g1) a2
    | b2        = assign (ValueGuess g2) a1
    | otherwise = unifyS a1 a2
    where
      (mb1,_) = fromIndirection a1
      (mb2,_) = fromIndirection a2
      (IndInfo g1) = fromJust mb1
      (IndInfo g2) = fromJust mb2
      b1 = isJust mb1
      b2 = isJust mb2

  -- similar as above: define fgvS
  fgv acc a
    | isJust mb = fgv acc (ValueGuess g)
    | otherwise = fgvS acc a
    where
      (mb,_) = fromIndirection a
      (IndInfo g) = fromJust mb

  -- similar as above: define dgvS
  dgv a
    | isJust mb = dgv (ValueGuess g)
    | otherwise = dgvS a
    where
      (mb,_) = fromIndirection a
      (IndInfo g) = fromJust mb

  -- similar to the above: define expAllS
  expAll = expAllRV

  rvCast = cast

expAllRV :: forall a m . (Functor m, Monad m, RulerValue a) => (Int -> m (Maybe Value)) -> a -> m a
expAllRV lk a
    | isJust mb = do v <- expAll lk (ValueGuess g)
                     case v of
                       ValueOpaque _ a' _ -> case cast a' of
                                               Just r  -> return r
                                               Nothing -> fail ("type error: expecting " ++ show (typeOf (undefined :: a)) ++ ", found: " ++show (typeOf a'))
                       ValueGuess _       -> return a
                       _                  -> fail "expAll on a data type encountered neither a variable nor an opaque value"
    | otherwise = expAllS lk a
    where
      (mb,_) = fromIndirection a
      (IndInfo g) = fromJust mb

instance RulerValue Int where
  unify x1 x2 | x1 == x2  = return ()
              | otherwise = failure ("unequal integers: " ++ show x1 ++ " and " ++ show x2)
  unifyS _ _              = abort "do not call unifyS on Int"
  fgv acc _               = return acc
  fgvS _ _                = abort "do not call fgvS on Int"
  dgv _                   = return IntSet.empty
  dgvS _                  = abort "do not call dgvS on Int"
  expAll _                = return
  expAllS _ _             = fail "do not call expAllS on Int"
  toIndirection _ _       = abort "cannot represent a guess as an Int"
  fromIndirection a       = (Nothing, Just a)

instance RulerValue Bool where
  unify b1 b2 | b1 == b2  = return ()
              | otherwise = failure ("unequal booleans: " ++ show b1 ++ " and " ++ show b2)
  unifyS _ _              = abort "do not call unifyS on Bool"
  fgv acc _               = return acc
  fgvS _ _                = abort "do not call fgvS on Bool"
  dgv _                   = return IntSet.empty
  dgvS _                  = abort "do not call dgvS on Bool"
  expAll _                = return
  expAllS _ _             = fail "do not call expAllS on Bool"
  toIndirection _ _       = abort "cannot represent a guess as a Bool"
  fromIndirection a       = (Nothing, Just a)

instance RulerValue Char where
  unify c1 c2 | c1 /= c2  = return ()
              | otherwise = failure ("unequal characters: " ++ show c1 ++ " and " ++ show c2)
  unifyS _ _              = abort "do not call unifyS on Char"
  fgv acc _               = return acc
  fgvS _ _                = abort "do not call fgvS on Char"
  dgv _                   = return IntSet.empty
  dgvS _                  = abort "do not call dgvS on Char"
  expAll _                = return
  expAllS _ _             = fail "do not call expAllS on Char"
  toIndirection _ _       = abort "cannot represent a guess as a Char"
  fromIndirection a       = (Nothing, Just a)

instance (RulerValue a, RulerValue b) => RulerValue (a,b) where
  unify (a,b) (c,d) = unify a c >> unify b d
  unifyS _ _        = abort "do not call unifyS on tuples"
  fgv acc (a,b)     = do acc' <- fgv acc a
                         fgv acc' b
  fgvS _ _          = abort "do not call fgvS on tuples"
  dgv (a,b)         = do a' <- dgv a
                         b' <- dgv b
                         return (IntSet.union a' b')
  dgvS _                  = abort "do not call dgvS on tuples"
  expAll lk (a,b)   = do a' <- expAll lk a
                         b' <- expAll lk b
                         return (a',b')
  expAllS _ _       = fail "do not call expAllS on tuples"
  toIndirection _ _ = abort "cannot represent a guess as a conventional tuple"
  fromIndirection a = (Nothing, Just a)

instance RulerValue a => RulerValue [a] where
  unify l r | length l == length r = sequence_ (zipWith unify l r)
            | otherwise            = failure ("lists of unequal length: " ++ show l ++ " and " ++ show r)
  unifyS _ _                       = abort "do not call unifyS on lists"
  fgv acc l                        = foldl (\r v -> r >>= flip fgv v) (return acc) l
  fgvS _ _                         = abort "do not call fgvS on lists"
  dgv l                            = foldr (\x r -> do r' <- r
                                                       x' <- dgv x
                                                       return (IntSet.union x' r')) (return IntSet.empty) l
  dgvS _                           = abort "do not call dgvS on lists"
  expAll lk ls                     = mapM (expAll lk) ls
  expAllS _ _                      = fail "do not call expAllS on Map"
  toIndirection _ _                = abort "cannot make an indirection of a conventional list"
  fromIndirection a                = (Nothing, Just a)

instance RulerValue Ident where
  unify a b | a == b    = return ()
            | otherwise = failure ("unequal identifiers: " ++ show a ++ " and " ++ show b)
  unifyS _ _            = abort "do not call unifyS on Ident"
  fgv acc _             = return acc
  fgvS _ _              = abort "do not call fgvS on Ident"
  dgv _                 = return IntSet.empty
  dgvS _                = abort "do not call dgvS on Ident"
  expAll _              = return
  expAllS _ _           = fail "do not call expAllS on Ident"
  toIndirection _ _     = abort "cannot represent a guess as an Ident"
  fromIndirection a     = (Nothing, Just a)

instance RulerValue () where
  unify _ _         = return ()
  unifyS _ _        = abort "do not call unifyS on ()"
  fgv acc _         = return acc
  fgvS _ _          = abort "do not call fgvS on ()"
  dgv _             = return IntSet.empty
  dgvS _            = abort "do not call dgvS on ()"
  expAll _          = return
  expAllS _ _       = fail "do not call expAllS on ()"
  toIndirection _ _ = abort "cannot represent a guess as a ()"
  fromIndirection a = (Nothing, Just a)

instance RulerValue Branch where
  unify _ _  = return ()
  unifyS _ _ = abort "do not call unifyS on Branch"
  fgv acc _  = return acc
  fgvS _ _   = abort "do not call fgvS on Branch"
  dgv (Branch _ v) = dgv v
  dgvS _           = abort "do not call dgvS on Branch"
  expAll _  = return
  expAllS _ _       = fail "do not call expAllS on Branch"
  toIndirection _ _ = abort "cannot represent a guess as a Branch"
  fromIndirection a = (Nothing, Just a)

instance RulerValue Segment where
  unify _ _  = return ()
  unifyS _ _ = abort "do not call unifyS on Segment"
  fgv acc _  = return acc
  fgvS _ _   = abort "do not call fgvS on Segment"
  dgv (Segment stmts segs) = do s1 <- dgv stmts
                                s2 <- dgv segs
                                return (s1 `IntSet.union` s2)
  dgvS _           = abort "do not call dgvS on Segment"
  expAll _  = return
  expAllS _ _       = fail "do not call expAllS on Segment"
  toIndirection _ _ = abort "cannot represent a guess as a Segment"
  fromIndirection a = (Nothing, Just a)

instance RulerValue Visit where
  unify _ _  = return ()
  unifyS _ _ = abort "do not call unifyS on Visit"
  fgv acc _  = return acc
  fgvS _ _   = abort "do not call fgvS on Visit"
  dgv (Visit _ bndgs _ v) = do b' <- dgv bndgs
                               v' <- dgv v
                               return (IntSet.unions [b', v'])
  dgv _                     = return IntSet.empty
  dgvS _                    = abort "do not call dgvS on Visit"
  expAll _  = return
  expAllS _ _       = fail "do not call expAllS on Visit"
  toIndirection _ _ = abort "cannot represent a guess as a Visit"
  fromIndirection a = (Nothing, Just a)

instance RulerValue ThunkStmt where
  unify _ _                = return ()
  unifyS _ _               = abort "do not call unifyS on ThunkStmt"
  fgv acc (ThunkStmt mp _ _) = fgv acc mp
  fgvS _ _                   = abort "do not call fgvS on ThunkStmt"
  dgv (ThunkStmt mp d _)   = do m' <- dgv mp
                                d' <- dgv d
                                return (m' `IntSet.union` d')
  dgvS _                   = abort "do not call dgvS on ThunkStmt"
  expAll _                 = return
  expAllS _ _              = fail "do not call expAllS on ThunkStmt"
  toIndirection _ _        = abort "cannot represent a guess as a ThunkStmt"
  fromIndirection a        = (Nothing, Just a)

instance RulerValue a => RulerValue (Map Ident a) where
  unify m1 m2 | not $ Map.null $ Map.difference m1 m2 = failure ("difference between maps not empty")
              | otherwise                             = foldr (>>) (return ()) $ Map.elems $ Map.intersectionWith unify m1 m2
  unifyS _ _  = abort "do not call unifyS on Map"
  fgv acc m = Map.fold (\v r -> r >>= flip fgv v) (return acc) m
  fgvS _ _  = abort "do not call fgvS on Map"
  dgv m = Map.fold (\v r -> do r' <- r
                               v' <- dgv v
                               return (IntSet.union v' r')) (return IntSet.empty) m
  dgvS _      = abort "do not call dgvS on Map"
  expAll lk m = fmap Map.fromList $ mapM (\(k,v) -> expAll lk v >>= \v' -> return (k,v')) (Map.assocs m)
  expAllS _ _       = fail "do not call expAllS on Map"
  toIndirection _ _ = error "Cannot make an indirection from a Map Ident Value"
  fromIndirection a = (Nothing, Just a)

instance RulerValue Value where
  unify v1 v2 =
    let msg v = expAll guessLookup v >>= \v' -> return (if v `eq` v' then show v else show v' ++ " [" ++ show v ++ "]")
        eq (ValueGuess g1) (ValueGuess g2) | g1 == g2 = True
        eq _               _                          = False
    in   ( do withDebugLevel 4 $ do m1 <- msg v1
                                    m2 <- msg v2
                                    message ("unify on value: " ++ m1 ++ " and " ++ m2)
              unifValue v1 v2
         )
       `catchError`
         (  \err -> do m1 <- msg v1
                       m2 <- msg v2
                       extendError False ("unify on " ++ m1 ++ " and " ++ m2 ++ " failed") err
         )
  unifyS _ _ = abort "do not call unifyS on Value"

  fgv acc (ValueOpaque _ _ gs)                   = fgvs (IntSet.union gs acc) gs
  fgv acc (ValueGuess g) | g `IntSet.member` acc = return acc
                         | otherwise             = do subst <- gets ssSubst
                                                      case IntMap.lookup g subst of
                                                        Just v | not (isPlaceholder v) -> fgvFromGuess g acc v
                                                        _                              -> return (IntSet.insert g acc)
  fgv acc _ = return acc
  fgvS _ _  = abort "do not call fgvS on Value"

  dgv (ValueOpaque g a _)                        = do a' <- dgv a
                                                      return (IntSet.insert g a')
  dgv (ValueGuess g)                             = return $ IntSet.singleton g
  dgv (ValueThunk g1 _ _ _ _ _ bndgs br g2) = do b'  <- dgv bndgs
                                                 br' <- dgv br
                                                 g2' <- dgv g2
                                                 return $ IntSet.insert g1 $ IntSet.unions [b', br', g2']
  dgv (ValueExternThunk g1 _ _ _ bndgs v1 v2)    = do b'  <- dgv bndgs
                                                      v1' <- dgv v1
                                                      v2' <- dgv v2
                                                      return $ IntSet.insert g1 $ IntSet.unions [b', v1', v2']
  dgv (ValueClosure _ _ alts _)                  = let altsBindings = concatMap altBindings
                                                       altBindings (ClosureAlt _ _ bndgs _ subs) = bndgs : altsBindings subs
                                                   in do sets <- mapM dgv (altsBindings alts)
                                                         return (IntSet.unions sets)
  dgv _                                          = return IntSet.empty
  dgvS _                                         = abort "do not call dgvS on Value"

  expAll lk v@(ValueGuess g) = do mb <- lk g
                                  case mb of  -- don't expand to a place holder
                                    Nothing                    -> return v
                                    Just v' | isPlaceholder v' -> return v
                                            | otherwise        -> expAll lk v'
  expAll lk (ValueOpaque g v gs) = expAll lk v >>= \v' -> return (ValueOpaque g v' gs)
  expAll _ v                     = return v
  expAllS _ _                    = fail "do not call expAllS on Value"

  toIndirection (IndInfo g) Nothing = return $ ValueGuess g
  toIndirection _ _ = abort "Not allowed to make an indirection out of a Value. A Value should not be exposed to external functions."

  fromIndirection v@(ValueOpaque g a _) = (Just (IndInfo g), Just v)
  fromIndirection (ValueGuess g)        = (Just (IndInfo g), Nothing)
  fromIndirection v                     = (Nothing, Just v)

fgvs :: IntSet -> IntSet -> I IntSet
fgvs acc gs
  = do subst <- gets ssSubst
       let next g acc' | g `IntSet.member` acc' = return acc'
                       | otherwise = case IntMap.lookup g subst of
                                       Just v  -> fgvFromGuess g (IntSet.delete g acc') v
                                       Nothing -> return acc'
       IntSet.fold (\g r -> r >>= next g) (return acc) gs

-- fgv called from the context of a guess. This situation allows us to improve
-- speedups of future fgvs on this guess by merging the result back to the
-- value.
fgvFromGuess :: Guess -> IntSet -> Value -> I IntSet
fgvFromGuess g acc (ValueOpaque u a gs)
  = do gs' <- fgvs gs gs
       when (IntSet.size gs' == IntSet.size gs) $ -- probably referencing the same memory, don't update to keep sharing
         modify (\s -> s { ssSubst = IntMap.insert g (ValueOpaque u a gs') (ssSubst s) })
       return (IntSet.union acc gs')
fgvFromGuess _ acc v = fgv acc v

unifValue :: Value -> Value -> I ()
unifValue (ValueGuess g1) (ValueGuess g2) | g1 == g2 = return ()
unifValue vg@(ValueGuess g) v = bindVar vg v
unifValue v vg@(ValueGuess g) = bindVar vg v
unifValue (ValueOpaque g1 (a1 :: t) gs1) (ValueOpaque g2 a2 gs2)
  | g1 == g2 && g1 > 0 = return ()
  | otherwise          = case cast a2 :: Maybe t of
                           Just a2' -> do unify a1 a2'
                                          -- sharing optimization: after unification the two values are
                                          -- discovered to be the same. Back-patch their references such
                                          -- that they point to the same value
                                          g <- earliestMappedGuess g1 g2
                                          if g > 0
                                           then let v = ValueOpaque g a1 (IntSet.union gs1 gs2)
                                                in do backpatch g1 v
                                                      backpatch g2 v
                                           else return () -- no guess associated with any of the two values
                           Nothing  -> abort ("values have different types: " ++ show (typeOf a1) ++ " and " ++ show (typeOf a2))
unifValue (ValueThunk g1 _ _ _ _ _ _ choice1 outcome1) (ValueThunk g2 _ _ _ _ _ _ choice2 outcome2)
  | g1 == g2  = do unify choice1 choice2
                   unify outcome1 outcome2
  | otherwise = abort ("cannot unify different thunks: " ++ show g1 ++ " and " ++ show g2)
unifValue (ValueClosure _ lbls1 _ _) (ValueClosure _ lbls2 _ _)
  = checkLbls lbls1 lbls2
unifValue (ValueExternClosure _ ident1 _) (ValueExternClosure _ ident2 _)
  | ident1 == ident2 = return ()
  | otherwise        = abort ("extern-closures have different identifiers: " ++ show ident1 ++ " and " ++ show ident2)
unifValue (ValueExternThunk g1 ident1 _ _ _ _ outcome1) (ValueExternThunk g2 ident2 _ _ _ _ outcome2)
   | g1 == g2  = unify outcome1 outcome2
   | otherwise = abort ("cannot unify different thunks: " ++ show g1 ++ " (named " ++ show ident1 ++ ") and " ++ show g2 ++ " (named " ++ show ident2 ++ ")")
unifValue (ValuePlaceholder tp1) (ValuePlaceholder tp2)
  | tp1 == tp2 = return ()
  | otherwise  = abort ("different types of place holders: " ++ show tp1 ++ " and " ++ show tp2)
unifValue (ValuePlaceholder (Bottom _)) v  = errBottom v  -- we don't match anything with a placeholder (unless its the placeholder itself)
unifValue v (ValuePlaceholder (Bottom _))  = errBottom v  --   reason: there is always a variable pointing towards this place holder, so
unifValue (ValuePlaceholder Defined) v     = errDefined v --           match with this variable instead.
unifValue v (ValuePlaceholder Defined)     = errDefined v
unifValue (ValuePlaceholder Initialized) v = errInitialized v
unifValue v (ValuePlaceholder Initialized) = errInitialized v
unifValue v1 v2 = abort ("different types of internal values: " ++ show v1 ++ " and " ++ show v2)

checkLbls :: Set Pos -> Set Pos -> I ()
checkLbls ls1 ls2
  | ls1 == ls2 = return ()
  | otherwise  = abort "labels do not match"

-- if the guess-value is really a guess (after expansion) continue binding,
-- otherwise continue unification with the expanded values
bindVar :: Value -> Value -> I ()
bindVar gv v
  = do gv' <- expand gv
       v'  <- expand v
       case gv' of
         ValueGuess g -> bindVar1 g v'
         _            -> unifValue gv' v'

-- check if v is an indirection. If so, it was actually a variable, and the
-- indirection inserted: follow the indirection
bindVar1 :: Guess -> Value -> I ()
bindVar1 g (ValueGuess g') | g == g' = return ()  -- after expansion we ended up on the same path. No binding (would create cycle). The values are equal.
bindVar1 g (ValueOpaque _ a _)
  | isJust mb = unifValue (ValueGuess g) (ValueGuess g')   -- follow the indirection (n.b. should not be cyclic!)
  where
    (mb,_) = fromIndirection a
    (IndInfo g') = fromJust mb
bindVar1 g v = bindVar2 g v -- otherwise continue with binding

-- deal with the bottom-cases when binding to a variable.
-- if the guess is mapped to bottom then the value may only be a guess
-- (with or without the intialized/defined placeholder) or bottom, but not a
-- concrete value, because this would replace the bottom value.
-- Precondition v must be in expanded form already.
bindVar2 :: Guess -> Value -> I ()
bindVar2 g v
  = do subst <- gets ssSubst
       case IntMap.lookup g subst of
         Just vg | isBottom vg -> case v of
                                    ValueGuess g' -> bindVar3 g' (ValueGuess g)  -- note: essential to map g' to g and not vice versa (because g is bottom)
                                    _             -> errBottom v -- cannot bind a guess mapped to bottom to some concrete value
         _                     -> bindVar3 g v  -- either g is mapped to Defined/Initialized or not mapped to anything

-- perform the occur check and actual binding
bindVar3 :: Guess -> Value -> I ()
bindVar3 g v
  = do withDebugLevel 4 $ debugBindVar g v
       gs <- fgv IntSet.empty v
       if g `IntSet.member` gs
        then failure ("guess " ++ show g ++ " occurs in " ++ show (IntSet.toList gs))
        else case v of
               ValueOpaque gOrig a _ -> do -- perform sharing optimization: replace (and if needed backpatch) gOrig
                                           g' <- earlierMapped gOrig g
                                           let v' = ValueOpaque g' a gs
                                           backpatch gOrig v'
                                           modify (\s -> s { ssSubst = IntMap.insert g v' $ ssSubst s })
               ValueGuess g2 -> do -- creating a mapping g -> g2. Placeholder of g will be lost, so integrate it with potentially one of g2
                                   mbHg  <- getPlaceholder g
                                   mbHg2 <- getPlaceholder g2
                                   let mbH = mergePlaceholdersMaybe mbHg mbHg2
                                   modify (\s -> s { ssSubst = maybe id (\h -> IntMap.insert g2 (ValuePlaceholder h)) mbH $ IntMap.insert g v $ ssSubst s })
               _             -> modify (\s -> s { ssSubst = IntMap.insert g v $ ssSubst s })

-- call this from "bindVar3" to see which bindings are made
debugBindVar :: Guess -> Value -> I ()
debugBindVar g (ValueOpaque _ v _)
  = do v' <- expAll guessLookup v
       message ("binding " ++ show g ++ " to " ++ show v')
debugBindVar g1 (ValueGuess g2)
  = message ("binding " ++ show g1 ++ " to " ++ show g2)
debugBindVar g _ = return ()

errBottom :: Value -> I ()
errBottom v = failure ("cannot bind bottom value to value " ++ show v)

errInitialized :: Value -> I ()
errInitialized v = failure ("cannot bind Initialized placeholder value to value " ++ show v ++ ". The entire place holder needs to be replaced by the value.")

errDefined :: Value -> I ()
errDefined v = failure ("cannot bind Defined placeholder value to value " ++ show v ++ ". The entire place holder needs to be replaced by the value.")

isBottom :: Value -> Bool
isBottom (ValuePlaceholder (Bottom _)) = True
isBottom _                             = False

isPlaceholder :: Value -> Bool
isPlaceholder (ValuePlaceholder _) = True
isPlaceholder _                    = False

mergePlaceholdersMaybe :: Maybe PlaceType -> Maybe PlaceType -> Maybe PlaceType
mergePlaceholdersMaybe mb1 mb2
  = maybe mb2 (\h -> maybe (Just h) (Just . mergePlaceholders h) mb2) mb1

mergePlaceholders :: PlaceType -> PlaceType -> PlaceType
mergePlaceholders (Bottom h1) (Bottom h2) = Bottom (mergePlaceholdersMaybe h1 h2)
mergePlaceholders (Bottom h1) h2          = Bottom (mergePlaceholdersMaybe h1 (Just h2))
mergePlaceholders h1 (Bottom h2)          = Bottom (mergePlaceholdersMaybe (Just h1) h2)
mergePlaceholders h1 h2                   = max h1 h2
}


--
-- Statements again
--

{
unwrapStmt :: ThunkStmt -> Stmt
unwrapStmt (ThunkStmt _ _ stmt) = stmt

stmtPos :: Stmt -> Pos
stmtPos (Stmt_Inst pos _ _)      = pos
stmtPos (Stmt_Establish pos _ _) = pos
stmtPos (Stmt_Equiv pos _ _)     = pos
stmtPos (Stmt_Bind pos _ _)      = pos
stmtPos (Stmt_Fresh pos _)       = pos
stmtPos (Stmt_Eval pos _)        = pos
stmtPos (Stmt_Nop pos)           = pos
stmtPos (Stmt_Abstract pos _)    = pos

exprPos :: Expr -> Pos
exprPos (Expr_Var _ nm)                 = identPos nm
exprPos (Expr_Field fld _)              = identPos fld
exprPos (Expr_AbstractField meta _)     = metaPos meta
exprPos (Expr_Prim pos _)               = pos
exprPos (Expr_Seq stmts _)              = stmtPos (head stmts)
exprPos (Expr_Derivation pos _ _ _ _ _) = pos
exprPos (Expr_External pos _ _ _)       = pos
exprPos (Expr_Merge pos _)              = pos

isStmtFresh (Stmt_Fresh _ _) = True
isStmtFresh _                = False
}


--
-- Idents
--

{
identsParam :: Params -> [Ident]
identsParam = concatMap getIds
  where getIds (Param_Input _ inps)  = inps
        getIds (Param_Output _ outs) = outs

identsScope :: Scopes -> [Ident]
identsScope = concatMap getIds
  where getIds (Scope_Requires inps) = inps
        getIds (Scope_Exposes outs)  = outs

-- The identifiers introduced by an explicit fresh (or inst) instead of
-- using an Expr_Var with Mode_Def
explicitIntroducedIdents :: [Stmt] -> [Ident]
explicitIntroducedIdents = Set.toList . foldr intro Set.empty
  where intro (Stmt_Fresh _ nms) = Set.union (Set.fromList nms)
        intro (Stmt_Inst _ _ nm) = Set.insert nm
        intro _                  = id

inputs :: Params -> [Ident]
inputs = nub . concatMap inputsParam
  where inputsParam (Param_Input _ inps) = inps
        inputsParam _                    = []

outputs :: Params -> [Ident]
outputs = nub . concatMap outputsParam
  where outputsParam (Param_Output _ outs) = outs
        outputsParam _                     = []

-- set of visit names in the 'params'
visits :: Params -> Set Ident
visits = foldr (\p -> Set.insert (v p)) Set.empty
  where v (Param_Input i _)  = i
        v (Param_Output i _) = i

-- all the inputs in the 'params' for the given visit name
visitInputs :: Params -> Ident -> [Ident]
visitInputs p v = nub $ foldr extend [] p
  where extend (Param_Input i inps) r | i == v = inps ++ r
        extend _ r                             = r

-- all the outputs in the 'params' for the given visit name
visitOutputs :: Params -> Ident -> [Ident]
visitOutputs p v = nub $ foldr extend [] p
  where extend (Param_Output i outs) r | i == v = outs ++ r
        extend _ r                              = r

identIntros :: Intros a => a -> [Ident]
identIntros = Set.toList . intros
}


--
-- Introduced identifiers
--
--  Introduced identifiers introduced by derivation-expressions are not
--  taken into account. I.e. an Expr_Var Mode_Def is introduced for the
--  innermost derivation. This also holds for such variables occuring in
--  an Expr_Seq, unless there is a Stmt_Fresh for it.
--

{
class Intros a where
  intros :: a -> Set Ident

instance Intros a => Intros [a] where
  intros = Set.unions . map intros

instance Intros Stmt where
  intros (Stmt_Inst _ expr nm)     = Set.insert nm $ intros expr
  intros (Stmt_Establish _ _ _)    = Set.empty
  intros (Stmt_Equiv _ left right) = intros left `Set.union` intros right
  intros (Stmt_Bind _ left right)  = intros left `Set.union` intros right
  intros (Stmt_Fresh _ nms)        = Set.fromList nms
  intros (Stmt_Eval _ expr)        = intros expr
  intros (Stmt_Nop _)              = Set.empty
  intros (Stmt_Abstract _ stmt)    = intros stmt

instance Intros Expr where
  intros (Expr_Var Mode_Def nm)          = Set.singleton nm
  intros (Expr_Seq stmts expr)           = Set.union (intros stmts) (intros expr) `Set.difference` (Set.fromList $ explicitIntroducedIdents stmts)
  intros (Expr_Merge _ exprs)            = intros exprs
  intros _                               = Set.empty
}


-- Referenced identifiers that are defined by the
-- evaluation/execution of the expression/statement.
-- note: an output of an expression/statement is thus
--       an input of a child derivation and an output
--       of the current derivation.
{
data IdentRef
  = NmRef !Ident
  | FldRef !Ident !Ident
  deriving (Eq, Ord, Show)

class OutputRefs a where
  outputRefs :: a -> I (Set IdentRef)
  
instance OutputRefs a => OutputRefs [a] where
  outputRefs = fmap Set.unions . mapM outputRefs

instance OutputRefs ThunkStmt where
  outputRefs (ThunkStmt _ _ stmt)      = outputRefs stmt

instance OutputRefs Stmt where
  outputRefs (Stmt_Inst _ expr nm)     = fmap (Set.insert $ NmRef nm) (outputRefs expr)
  outputRefs (Stmt_Establish _ _ _)    = return Set.empty
  outputRefs (Stmt_Equiv _ left right) = outputRefs [ left, right ]
  outputRefs (Stmt_Bind _ left right)  = outputRefs [ left, right ]
  outputRefs (Stmt_Fresh _ nms)        = return (Set.fromList $ map NmRef nms)
  outputRefs (Stmt_Eval _ expr)        = outputRefs expr
  outputRefs (Stmt_Nop _)              = return Set.empty
  outputRefs (Stmt_Abstract _ stmt)    = outputRefs stmt

instance OutputRefs Expr where
  outputRefs (Expr_Var Mode_Def nm)    = return $ Set.singleton $ NmRef nm
  outputRefs (Expr_Field fld nm)
    = do mbV <- tryLookupIdent fld
         case mbV of
           Nothing -> return Set.empty
           Just v  -> do v' <- expand v
                         if isGuess v'
                          then return Set.empty
                          else do (isContra, isOutput) <- getFieldInfo fld nm
                                  if isContra  -- a "this" fld
                                   then if isOutput
                                        then return $ Set.singleton $ FldRef fld nm
                                        else return Set.empty
                                   else if isOutput
                                        then return Set.empty
                                        else return $ Set.singleton $ FldRef fld nm
  outputRefs (Expr_AbstractField _ _)  = return Set.empty  -- abstract fields do not participate in override mechanism!
  outputRefs (Expr_Seq stmts expr)     = do refsStmts <- outputRefs stmts
                                            refsExpr  <- outputRefs expr
                                            return (Set.union refsStmts refsExpr `Set.difference` (Set.fromList $ map NmRef $ explicitIntroducedIdents stmts))
  outputRefs (Expr_Merge _ exprs)      = outputRefs exprs
  outputRefs _                         = return Set.empty
}


--
-- Monad
--

{
type I a = ErrorT EvalError (RWS InputState OutputState SharedState) a

data InputState = InputState { isBindings :: !(Map Ident Value), isCalls :: !(Map (Set Pos) (I ())), isStack :: IntSet, isOpts :: !Opts, isBindingsStack :: ![Map Ident Value], isChildOrder :: ![Ident] }
data SharedState = SharedState { ssUnique :: !Int, ssSubst :: !(IntMap Value), ssFailedSpeculatives :: !(Set Pos), ssLastSubstSize :: !Int, ssExtraRoots :: ![[Value]] }
data OutputState = OutputState { osMessages :: !(Seq Message), osDerivations :: ![(Ident, Value)] }

instance Monoid OutputState where
  mempty = OutputState mempty mempty
  mappend (OutputState m1 d1) (OutputState m2 d2) = OutputState (mappend m1 m2) (mappend d1 d2)
  

-- Two error alternatives. One that permits graceful recovery through
-- backtracking, and another which leads to an abort with an evaluation error.
-- retry indicates that error that might be solved by a re-execution in a different order
data EvalError = Recoverable !ErrorReason | Abort !ErrorReason | Retry !Ident
data ErrorReason = ErrorReason !String !String

instance Error EvalError where
  noMsg    = Abort (ErrorReason "" "no more specific error information.")
  strMsg s = Abort (ErrorReason s s)

instance Show EvalError where
  show (Recoverable r)   = "recoverable error: " ++ show r
  show (Abort r)         = "abort: " ++ show r
  show (Retry ident)     = "retry error due to: " ++ explainIdent ident

instance Show ErrorReason where
  show (ErrorReason _ long) = long

showErrShort (Recoverable r) = showReasonShort r
showErrShort (Abort r)       = showReasonShort r
showErrShort (Retry ident)   = "retry error due to: " ++ explainIdent ident

showReasonShort (ErrorReason short _) = short

extendError :: Bool -> String -> EvalError -> I a
extendError alsoShort prefix (Recoverable (ErrorReason short long)) = let ext s = prefix ++ ": " ++ s in throwError $ Recoverable $ ErrorReason (if alsoShort then ext short else short) (ext long)
extendError alsoShort prefix (Abort (ErrorReason short long))       = let ext s = prefix ++ ": " ++ s in throwError $ Abort       $ ErrorReason (if alsoShort then ext short else short) (ext long)
extendError alsoShort _      r@(Retry _)       = throwError r

extendErrorIfRecoverable :: Bool -> String -> EvalError -> I a
extendErrorIfRecoverable alsoShort prefix e@(Recoverable _) = extendError alsoShort prefix e
extendErrorIfRecoverable _         _      e                 = throwError e

abort :: String -> I a
abort str = do errMessage str
               throwError (Abort (ErrorReason str str))

failure :: String -> I a
failure str = do errMessage str
                 throwError (Recoverable (ErrorReason str str))

invalidDeref :: Ident -> I a
invalidDeref ident = throwError (Retry ident)

withDebugLevel :: Int -> I () -> I ()
withDebugLevel threshold m
  = do l <- asks (debugLevel . isOpts)
       if l >= threshold
        then m
        else return ()

message :: String -> I ()
message = message' NotifyMsg

errMessage :: String -> I ()
errMessage = message' ErrorMsg

message' :: (String -> Message) -> String -> I ()
message' f s = let sq  = Seq.singleton (f s)
               in do dump <- asks (dumpMessages . isOpts)
                     if dump
                      then (unsafePerformIO $ hPutStrLn stderr s) `seq` return ()
                      else return ()
                     tell (mempty { osMessages = sq })

-- expand the guesses, with one exception: if a guess points to a placeholder
-- then the guess is returned, not the placeholder.
expand :: Value -> I Value
expand v@(ValueGuess g)
  = do subst <- gets ssSubst
       case IntMap.lookup g subst of
         Nothing -> return v
         Just v' | isPlaceholder v' -> return v
                 | otherwise        -> do vDirect <- expand v'
                                          -- update indirection to keep short chains, updating g to point directly to the value
                                          case vDirect of  -- invariant: both g and gOrig are mapped in the substitution (is guaranteed by the bindVar)
                                            ValueOpaque gOrig a gs | gOrig == g -> return ()  -- g is already pointing to the value
                                                                   | gOrig > g  -> let vNew = ValueOpaque g a gs
                                                                                   in do backpatch gOrig vNew
                                                                                         backpatch g vNew
                                            _                                   -> backpatch g vDirect
                                          return vDirect
expand v = return v

guessLookup :: Int -> I (Maybe Value)
guessLookup g
  = do subst <- gets ssSubst
       return (IntMap.lookup g subst)

lookupIdent :: Ident -> I Value
lookupIdent nm
  = do bindings <- asks isBindings
       case Map.lookup nm bindings of
         Nothing -> abort ("identifier " ++ show nm ++ " (" ++ show (identPos nm) ++ ") not bound in environment: " ++ explainBindings bindings)
         Just v  -> return v

tryLookupIdent :: Ident -> I (Maybe Value)
tryLookupIdent nm
  = do bindings <- asks isBindings
       return $ Map.lookup nm bindings

-- note: requires lexically scoped type variable v to access the typeable dictionary
lookupIdentPrim :: forall v . Typeable v => Ident -> I v
lookupIdentPrim nm
  = do v <- lookupIdent nm
       v' <- expand v
       case v' of
         ValueOpaque _ r _ -> case cast r of
                                Nothing -> abort ("value of " ++ show nm ++ " has incompatible type, expecting: " ++ show (typeOf (undefined :: v)))
                                Just x  -> return x
         _             -> abort (show nm ++ " is not a primitive value")

-- expects a concrete value after expansion and casts it toward the expected type
--  note: requires lexically scoped type variable v
resolve :: forall v . Typeable v => Value -> I v
resolve v
  = do v' <- expand v
       case v' of
         ValueOpaque _ r _ -> case cast r of
                                Nothing -> abort ("value " ++ show v' ++ " has incompatible type, found: " ++ show (typeOf r) ++ ", expecting: " ++ show (typeOf (undefined :: v)))
                                Just x  -> return x
         _                 -> abort (show v' ++ " is not a primitive value")

tryResolve :: forall v . Typeable v => Value -> v -> I v
tryResolve v a
  = do v' <- expand v
       case v' of
         ValueOpaque _ r _ -> resolve v'
         _                 -> return a

lookupField :: Ident -> Ident -> I Value
lookupField fld nm
  = do vFld  <- lookupIdent fld
       vFld' <- expand vFld
       case vFld' of
         ValueThunk _ _ _ _ _ _ bindings _ _   -> case Map.lookup nm bindings of
                                                    Nothing -> abort ("identifier " ++ show nm ++ " not bound in derivation of " ++ show fld ++ ". Bound are: " ++ explainBindings bindings)
                                                    Just v  -> return v
         ValueExternThunk _ _ _ _ bindings _ _ -> case Map.lookup nm bindings of
                                                    Nothing -> abort ("identifier " ++ show nm ++ " not bound in derivation of " ++ show fld  ++ ". Bound are: " ++ explainBindings bindings)
                                                    Just v  -> return v
         _                                     -> invalidDeref fld

-- returns a fresh guess. It has no mapping in the substitution yet. Mappings in
-- the substitution can either be a placeholder, a concrete value, or a guess.
-- If it is mapped to a concrete value, it can never be modified. A guess can
-- only be replaced with an equivalent value.
fresh :: I Value
fresh = do c <- nextUnique
           return (ValueGuess c)

nextUnique :: I Guess
nextUnique
  = do c <- gets ssUnique
       modify (\s -> s { ssUnique = c + 1 })
       return c

-- runs the I-monad-computation with the extra bindings in scope
scopeBindings :: Map Ident Value -> I a -> I a
scopeBindings bindings m
  = local (\is -> is { isBindings = bindings `Map.union` isBindings is, isBindingsStack = bindings : isBindingsStack is }) m

restrictBindings :: Map Ident Value -> I a -> I a
restrictBindings bindings m
  = local (\is -> is { isBindings = bindings, isBindingsStack = bindings : isBindingsStack is }) m

assert :: (Value -> Bool) -> Value -> String -> I ()
assert p v msg
  = do v' <- expand v
       case p v' of
         True -> return ()
         _    -> abort msg

isGuess (ValueGuess _) = True
isGuess _              = False

-- returns the Branch if it is defined in the value, otherwise Nothing
resolveBranch :: Value -> I (Maybe Branch)
resolveBranch v
  = do v' <- expand v
       if isGuess v'
        then return Nothing
        else do b <- resolve v'
                return (Just b)

backtrack :: Value -> [I a] -> I a
backtrack _ [alt] = alt  -- only one alternative: no backtracking + shorter error message
backtrack gBranch alts
  = do prevState <- gets ssSubst
       inpState  <- ask
       let next :: I a -> I a -> I a
           next prev alt
             = do (eErrRes, os) <- tryExec prev
                  let tellAll = tell os
                  case eErrRes of
                    Right r -> do tellAll
                                  return r
                    Left e  -> case e of
                                 Abort _ -> do tellAll
                                               throwError e
                                 Retry ident -> do tellAll
                                                   abort ("A retry exception was caught, due to identifier: " ++ explainIdent ident)
                                 Recoverable r -> local (const inpState) $
                                                    do branch <- expand gBranch
                                                       if isGuess branch
                                                        then do withDebugLevel 2 $ message ("previous branch skipped due to: " ++ show r)
                                                                modify (\s -> s { ssSubst = prevState })
                                                                alt `catchError` extendErrorIfRecoverable False ("while skipping previous branch [" ++ show r ++ "]")
                                                        else do tellAll
                                                                throwError e
       foldl next (failure "backtrack: empty branches") alts

-- tries executing the given command, returning the changes to the output
-- state, while leaving the actual output state unmodified. It is then up to
-- the caller to decide to merge in the changes or not.
-- the shared state (i.e. subsitution, e.d.) is not reverted.
tryExec :: I a -> I (Either EvalError a, OutputState)
tryExec m = censor (const mempty) $ listen $
              ( (m >>= return . Right) `catchError` (return . Left) )

identsDefined     = allIdents isDefinedValue
identsInitialized = allIdents isInitializedValue

-- checks f on all values of the given idents
allIdents :: (Value -> I Bool) -> Map Ident Value -> [Ident] -> I Bool
allIdents f bindings idents
  = allAnd $ map check idents
  where check ident = case Map.lookup ident bindings of
                        Just v  -> f v
                        Nothing -> abort ("Identifier " ++ explainIdent ident ++ " is not bound in: " ++ explainBindings bindings)

isDefinedValue     = matchPlaceholder Defined
isInitializedValue = matchPlaceholder Initialized

checkValueInitialized :: Ident -> I Value -> I Value
checkValueInitialized ident m
  = do v <- m
       b <- isInitializedValue v
       if b
        then return v
        else invalidDeref ident

-- returns a tuple with:
--   is the field contra variant (i.e. a this-field)
--   is the field an output
getFieldInfo :: Ident -> Ident -> I (Bool, Bool)
getFieldInfo fld ident
  = do vFld  <- lookupIdent fld
       vFld' <- expand vFld
       st <- asks isStack
       let (uid,params)    = case vFld' of
                               ValueThunk uid _ _ _ _ params _ _ _     -> (uid, params)
                               ValueExternThunk uid _ _ params _ _ _   -> (uid, params)
           isContravariant = uid `IntSet.member` st  -- dereference of "this"
           isOutput        = ident `elem` outputs params
       return (isContravariant, isOutput)

-- checks if a field is ready based on
-- contra or covariant dereference and
-- whether or not it is an output
isFieldReady :: Bool -> Bool -> Value -> I Bool
isFieldReady isContra isOutput v
  = do if isContra
        then if isOutput
             then return True
             else isDefinedValue v
        else if isOutput
             then isDefinedValue v
             else isInitializedValue v


matchPlaceholder :: PlaceType -> Value -> I Bool
matchPlaceholder h v
  = do v' <- expand v
       case v' of
         ValueGuess g -> do mbH <- getPlaceholder g
                            case mbH of
                              Just h' -> return (h <= h')
                              _       -> return False
         _            -> return True

-- returns the place holder *directly* attached to the guess
getPlaceholder :: Guess -> I (Maybe PlaceType)
getPlaceholder g
  = do subst <- gets ssSubst
       case IntMap.lookup g subst of
         Just (ValuePlaceholder h) -> return (Just h)
         _                         -> return Nothing

-- short-circuiting list combine
doConcat :: [I [a]] -> I [a]
doConcat = foldl (\l r -> do xs <- l
                             if null xs
                              then r
                              else return xs
                 ) (return [])

doAnd :: I Bool -> I Bool -> I Bool
doAnd l r = do b <- l
               if b
                then r
                else return False

allAnd :: [I Bool] -> I Bool
allAnd = foldl (\l r -> doAnd l r) (return True)

doAny :: I Bool -> I Bool -> I Bool
doAny l r = do b <- l
               if b
                then return True
                else r

doFirst :: [I Bool] -> I Bool
doFirst = foldl (\l r -> doAny l r) (return False)

freshBindings :: [Ident] -> I (Map Ident Value)
freshBindings idents
  = do vs <- mapM (const fresh) idents
       return $ Map.fromList $ zip idents vs

markBindingsInitialized :: [Ident] -> Map Ident Value -> I ()
markBindingsInitialized = markBindings markInitialized

markBindingsDefined :: [Ident] -> Map Ident Value -> I ()
markBindingsDefined = markBindings markDefined 

markBindings :: (Value -> I ()) -> [Ident] -> Map Ident Value -> I ()
markBindings f ids bindings
  = mapM_ (\nm -> f (Map.findWithDefault (error "markBindingsInitialized: identifier not in the bindings") nm bindings)) ids

markInitialized = mark Initialized
markDefined     = mark Defined

-- marks the value (iff it is a guess) in the substitution
mark :: PlaceType -> Value -> I ()
mark h v = do v' <- expand v
              case v' of
                ValueGuess g -> modify (\s -> s { ssSubst = IntMap.insert g (ValuePlaceholder h) $ ssSubst s })
                _            -> return ()

expandBindings :: Map Ident Value -> I (Map Ident Value)
expandBindings bindings
  = do elems' <- mapM (\(k,v) -> expAll guessLookup v >>= \v' -> return (k,v')) (Map.assocs bindings)
       return (Map.fromList elems')

-- publishes an established derivation: v must be mapped to a derivation.
established :: Ident -> Value -> I ()
established nm v
  = do tell (mempty { osDerivations = [(nm, v)] })
       modify (\ss -> ss { ssExtraRoots = push (ssExtraRoots ss) })
  where push (xs : xss) = (v : xs) : xss

--
-- Construct a Segment
--
-- use the entire given administration to construct a proper heap for each statement
-- take:
--   1 altGlobals as the basis
--   2 the thunkBindings (currently only containing 'innername', used to be restricted to segmentParams)
--   3 the localsBindings for our alternative for which we have altParams
--   4 the identifiers introduced by fresh, inst, and inline allocation (except those already bound by locals)
createSegment :: Value -> [ClosureAlt] -> I Segment
createSegment thunkValue cAlts
  = do allLocals <- freshBindings localIdents
       rootSegs <- mapM (toSegmentRoot allLocals) cAlts
       return $ if length rootSegs == 1
                then head rootSegs
                else Segment [] rootSegs
  where
    toSegmentRoot allLocals cAlt
      = let nms    = altIdents cAlt
            locals = restrict nms allLocals
        in toSegment locals cAlt

    toSegment locals (ClosureAlt _ innername altGlobals (Alt_Alt _ _ stmts) subAlts)
      = do subSegs <- mapM (toSegment locals) subAlts
           introBindings <- freshBindings (filter (\nm -> not (Map.member nm locals)) $ identIntros stmts)
           let bindings = introBindings
                          `Map.union` locals
                          `Map.union` ( Map.fromList [(ident "__this",thunkValue),(innername,thunkValue)] )
                          `Map.union` altGlobals
           stmts' <- mapM (toStmt bindings) stmts
           return (Segment stmts' subSegs)
    toStmt bindings stmt
      = do gFinished <- fresh  -- fresh variable indicating that the statement is not finished yet
           return (ThunkStmt bindings gFinished stmt)

    -- local variables in scope of the segment
    localIdents = nub $ altsIdents cAlts
    altsIdents = concatMap altIdents
    altIdents (ClosureAlt _ _ _ (Alt_Alt _ scopes _) alts) = identsScope scopes ++ altsIdents alts

    -- reduce the items in the map to only those with the given keys
    restrict ids = Map.filterWithKey (\k _ -> k `elem` ids)


-- all children defined in a segment, obtained in the right order
-- this is actually static info that shouldn't be calculated over and over again
-- all the time
segmentChildren :: Segment -> [Ident]
segmentChildren = nub . chldsSegment
  where chldsSegment (Segment stmts subs) = concatMap chldsStmt stmts ++ concatMap chldsSegment subs
        chldsStmt (ThunkStmt _ _ (Stmt_Inst _ _ nm)) = [nm]
        chldsStmt _                                  = []

-- returns the accessible children that has a certain field
-- if a child is not yet known, it is returned by default
childrenWithField :: Ident -> I [Ident]
childrenWithField nm
  = do order <- asks isChildOrder
       filterM hasField order
  where
    hasField fld
      = do mbChild <- tryLookupIdent fld
           case mbChild of
             Nothing   -> return True  -- by absence: default to True
             Just vFld -> do vFld' <- expand vFld
                             case vFld' of
                               ValueThunk _ _ _ _ _ _ bindings _ _   -> return (Map.member nm bindings)
                               ValueExternThunk _ _ _ _ bindings _ _ -> return (Map.member nm bindings)


-- returns those visits for which the inputs are all defined.
-- there are no duplicate idents in the result list, and returns
-- the visits in an order based on the name.
visitsWithDefinedInputs :: Params -> [Ident] -> Map Ident Value -> I [Ident]
visitsWithDefinedInputs params order bindings
  = fmap snd $ foldl extend (return (True,[])) order
  where
    extend r v
      = do prev@(continue,xs) <- r
           if continue
            then do b <- identsDefined bindings (visitInputs params v)
                    if b
                     then return (True, xs ++ [v])
                     else return (False, xs)
            else return prev

-- links the visit to the last element of the visit-chain
linkVisit :: Value -> Visit -> I ()
linkVisit vG visit
  = do vG' <- expand vG
       case vG' of
         ValueGuess _ -> assign vG' visit
         _            -> do prev <- resolve vG'
                            case prev of
                              Visit _ _ _ next -> linkVisit next visit
                              Finish _         -> abort "cannot link in a new visit in an already finialized visit-chain"

-- checks in the list of ready visits, and the chain of already established
-- visits, that there is a new visit ready to be executed.
isNewVisitReady :: Value -> [Ident] -> I Bool
isNewVisitReady _ [] = return False
isNewVisitReady g vs
  = do val <- expand g
       if isGuess val
        then return True
        else do v <- resolve val
                case v of
                  Visit nm _ _ next | nm == head vs -> isNewVisitReady next (tail vs)
                                    | otherwise     -> return False -- a later visit than is in the order is ready.
                  Finish _                          -> abort "derivation is already finished. Cannot establish it anymore."

-- returns the next visit in the chain given the visit order
nextVisit :: Value -> [Ident] -> I (Ident, Maybe Ident)
nextVisit _ [] = abort "empty visit list"
nextVisit g vs
  = do val <- expand g
       if isGuess val
        then return (head vs, listToMaybe (tail vs))
        else do v <- resolve val
                case v of
                  Visit nm _ _ next | nm == head vs -> nextVisit next (tail vs)
                                    | otherwise     -> abort "wrong visit order encountered"
                  Finish _                          -> abort "derivation is already finished. There is no next visit."

-- checks if the derivation is finished
assertFinished :: Value -> I ()
assertFinished g
  = do val <- expand g
       case val of
         ValueThunk _ _ _ _ _ _ _ _ g'   -> assertFinishedOutcome g'
         ValueExternThunk _ _ _ _ _ _ g' -> assertFinishedOutcome g'
         _                               -> abort ("not a derivation: " ++ show val ++ "[" ++ show g ++ "]")

assertFinishedOutcome :: Value -> I ()
assertFinishedOutcome g
  = do val <- expand g
       if isGuess val
        then abort "the derivation is not finished"
        else do v <- resolve val
                case v of
                  Visit _ _ _ next -> assertFinishedOutcome next
                  Finish _         -> return ()

-- wraps the value and assigns it to the guess
assign :: RulerValue a => Value -> a -> I ()
assign g v = mkOpaque v >>= unify g

-- return in the I-monad. Using 'ireturn' instead of 'return' saves some type signatures.
ireturn :: a -> I a
ireturn = return


-- selects the lowest guess mapped in the substitution, or -1 otherwise.
earliestMappedGuess :: Guess -> Guess -> I Guess
earliestMappedGuess g1 g2
  = let gmin = min g1 g2
        gmax = max g1 g2
    in do subst <- gets ssSubst
          if IntMap.member gmin subst
           then return gmin
           else if IntMap.member gmax subst
                then return gmax
                else return (-1)

-- returns g1 if g1 is mapped an earlier than g2, otherwise returns g2
earlierMapped :: Guess -> Guess -> I Guess
earlierMapped g1 g2
  | g2 < g1   = return g2
  | otherwise = do subst <- gets ssSubst
                   if IntMap.member g1 subst
                    then return g1
                    else return g2

-- update the substitution with a new mapping for g, if g is actually mapped
backpatch :: Guess -> Value -> I ()
backpatch g v
  = do subst <- gets ssSubst
       if IntMap.member g subst
        then modify (\s -> s { ssSubst = IntMap.insert g v subst })
        else return ()
}


--
-- Bind (in terms of unify and some operations on the state)
--

{
-- unifies v1 and v2, while keeping v2 constant
bind :: Value -> Value -> I ()
bind v1 v2
  = do vars <- fmap IntSet.toList $ fgv IntSet.empty v2
       freeze vars
       unify v1 v2
       unfreeze vars

-- for any unbound variable in gs, binds it to a Bottom value
freeze :: [Guess] -> I ()
freeze vars
  = modify (\s -> s { ssSubst = IntMap.unionWith merge candidates (ssSubst s) })
  where
    candidates = IntMap.fromList [ (g, ValuePlaceholder (Bottom Nothing)) | g <- vars ]
    merge _ (ValuePlaceholder h) = ValuePlaceholder (Bottom (Just h))
    merge _ v                    = v

-- remove the frozen variables, replacing them with "ready" placeholders
unfreeze :: [Guess] -> I ()
unfreeze vars
  = modify (\s -> s { ssSubst = foldr (IntMap.alter restore) (ssSubst s) vars })
  where restore (Just (ValuePlaceholder (Bottom mh))) = maybe Nothing (Just . ValuePlaceholder) mh
        restore v                                     = v
}


{

--
-- Inspection monad transformer
--

data ITIn = ITIn { itSubst :: !(IntMap Value), itOpts :: !Opts }

type IT m a = ReaderT ITIn m a

valLookupIT g
  = do subst <- asks itSubst
       case IntMap.lookup g subst of
         Just v | not (isPlaceholder v) -> case v of
                                             ValueGuess g' -> valLookupIT g'
                                             _             -> return (Just v)
         _                              -> return Nothing

valExpand :: (Functor m, Monad m) => Value -> IT m Value
valExpand v@(ValueGuess g)
  = do subst <- asks itSubst
       case IntMap.lookup g subst of
         Just v' | not (isPlaceholder v') -> valExpand v'
         _                                -> return v
valExpand v = return v

runIT :: IT m a -> ITIn -> m a
runIT = runReaderT

-- switch the encapsulated monad
switchStateIT :: (m a -> n b) -> IT m a -> IT n b
switchStateIT = mapReaderT

isNoPlaceholderIT :: (Functor m, Monad m) => Value -> IT m Bool
isNoPlaceholderIT (ValuePlaceholder _) = return False
isNoPlaceholderIT (ValueGuess g)
  = do subst <- asks itSubst
       case IntMap.lookup g subst of
         Just v -> return $ not $ isPlaceholder v
         _      -> return True
isNoPlaceholderIT _ = return True


--
-- Tabular pretty printing
--

type TTM m a = IT (StateT (Int,IntSet) m) a

finishTTM :: (Functor m, Monad m) => TTM m a -> IT m a
finishTTM = switchStateIT (\wm -> evalStateT wm (1,IntSet.empty))

class Show a => Tabular a where
  tablify :: (Functor m, Monad m) => ParensInfo -> Int -> a -> TTM m (Table, Int)

  minTableLength :: a -> Int
  minTableLength = length . show

txtShowTablify :: (Functor m, Monad m, RulerValue a) => a -> TTM m (Table, Int)
txtShowTablify v = do v' <- expAll valLookupIT v
                      let s = show v'
                      return (TableText s, length s)

-- Precedence context information
-- SamePrioNo: add parentheses if the node's prio is strictly higher than the Int
-- SamePrioYes: add parentheses if the node's prio is higher or equal than the Int
data ParensInfo
  = SamePrioNo  !Int
  | SamePrioYes !Int

-- Represents a tabular data structure with references
data Table
  = TableEmpty
  | TableText    !String
  | TableRef     !Int !Guess Table
  | TableBesides !Table !Table
  | TableAbove   !Table !Table
  deriving Show


processReferences :: (Functor m, Monad m) => TTM m a -> (TTM m (Seq (Guess, b)) -> TTM m (Seq (Guess, b))) -> (Guess -> TTM m b) -> TTM m (a, [(Guess, b)], IntSet)
processReferences m g f
  = do a <- m
       gsInit <- gets snd
       s <- g (it gsInit IntSet.empty Seq.empty)
       return (a, toList s, gsInit)
  where
    it todo done acc
      | IntSet.null todo = return acc
      | otherwise = let gs = IntSet.toList todo
                    in do rs <- mapM f gs
                          newGs <- gets snd
                          let done' = IntSet.union todo done
                              todo' = newGs `IntSet.difference` done'
                              acc'  = acc Seq.>< (Seq.fromList (zip gs rs))
                          it todo' done' acc'

-- tablifyGuess uses valExpand. If expansion returns in a guess, then it
-- prints the guess. If it returns in something else, it prints a reference.
tablifyGuess :: (Functor m, Monad m) => Guess -> TTM m (Table, Int)
tablifyGuess g
  = let txtRef g' = TableText ("%" ++ show g')
        txtVar g' = TableText ("#" ++ show g')
        n g'      = 1 + length (show g')
    in do v <- valExpand (ValueGuess g)
          case v of
            ValueGuess g' -> return (txtVar g', n g')
            _             -> do (c,gs) <- get
                                put (c+1, IntSet.insert g gs)
                                return (TableRef c g (txtRef g), n g)

tabTxt :: String -> Table
tabTxt = TableText

tabBesides :: [Table] -> Table
tabBesides = foldr TableBesides TableEmpty

tabAboves :: [Table] -> Table
tabAboves = foldr TableAbove TableEmpty

tabParens = tabPacked "(" ")"
tabBrack = tabPacked "[" "]"
tabCurly = tabPacked "{" "}"

tabPacked :: String -> String -> Table -> Table
tabPacked l r t = tabBesides [ tabTxt l, t, tabTxt r ]

-- a rough estimate of the minimal default size of a component
tabDefaultMinSize :: Int
tabDefaultMinSize = 5

tabConSize :: Int -> [Int] -> Int
tabConSize n ns = n + 3 * length ns + sum ns

tablifyInd :: (Functor m, RulerValue a, Monad m) => ParensInfo -> Int -> IndInfo -> Maybe a -> TTM m (Table, Int)
tablifyInd prio maxSize (IndInfo g) mbVal
  = case mbVal of
      Just v  -> tablify prio maxSize v
      Nothing -> tablify prio maxSize (ValueGuess g)

conRecTablify :: (Functor m, Monad m, Tabular a) => Int -> a -> TTM m (Table, Int)
conRecTablify = tablify (SamePrioYes 9)

conResultTablify :: (Functor m, Monad m) => ParensInfo -> String -> [Table] -> [Int] -> TTM m (Table, Int)
conResultTablify prio nm tbls sizes
  = let t = tabBesides ([ tabTxt (nm ++ " ") ] ++ intersperse (tabTxt " ") tbls)
        needParens = not (null tbls) && sameYes
        sameYes = case prio of
                    SamePrioYes _ -> True
                    SamePrioNo _  -> False
        parensF = if needParens then tabParens else id
        parensS = if needParens then 2 else 0
    in return (parensF t, parensS + length nm + length tbls + sum sizes)

wrapString :: Int -> String -> [String]
wrapString size s = wrapString' (max size 10) 0 s ""

wrapString' _ _ [] acc = [acc]
wrapString' size l xs acc | lx > size     = (if null acc then id else (acc :))
                                            (x : wrapString' size 0 r "")
                          | l + lx > size = acc : wrapString' size lx r x
                          | otherwise     = wrapString' size (l + length x) r (acc ++ x)
                          where
                            (x',r') = break isSpace xs
                            x = x' ++ takeWhile isSpace r'
                            r = dropWhile isSpace r'
                            lx = length x


--
-- tabular instances
--  (for data types introduced in this file)
--

instance Tabular () where
  tablify _ _ = txtShowTablify

instance Tabular Bool where
  tablify _ _ = txtShowTablify

instance Tabular Int where
  tablify _ _ = txtShowTablify

instance Tabular Char where
  tablify _ _ = txtShowTablify

instance Tabular Ident where
  tablify _ _ = txtShowTablify

instance Tabular Branch where
  tablify _ _ = txtShowTablify

instance Tabular Visit where
  tablify _ _ = txtShowTablify

instance Tabular Segment where
  tablify _ _ = txtShowTablify

instance Tabular ThunkStmt where
  tablify _ _ = txtShowTablify

instance Tabular IndInfo where
  tablify prio width (IndInfo g) = tablify prio width g

instance (Tabular a, Tabular b) => Tabular (a,b) where
  tablify _ maxSize (a,b)
    = let size = maxSize - 4 - tabDefaultMinSize
      in do (tabA, sizeA) <- tablify (SamePrioNo 9) size a
            (tabB, sizeB) <- tablify (SamePrioNo 9) (size - sizeA) b
            return (tabParens $ tabBesides [ tabA, tabTxt ", ", tabB ], 4 + sizeA + sizeB)

  minTableLength (a,b) = 4 + minTableLength a + minTableLength b

instance Tabular a => Tabular (Maybe a) where
  tablify _ maxSize Nothing
    = return (tabTxt "Nothing", 7)
  tablify _ maxSize (Just a)
    = do (tabA, sizeA) <- tablify (SamePrioNo 9) (maxSize - 7 - tabDefaultMinSize) a
         return (tabParens $ tabBesides [ tabTxt "Just ", tabA ], 7 + sizeA)
  
  minTableLength Nothing = 7
  minTableLength (Just a) = 7 + minTableLength a

instance Tabular a => Tabular [a] where
  tablify _ maxSize xs
    = let n           = length xs
          minSurround = 2 * max 1 (n-1) 
          minReqSize  = minSurround + max 0 (n-1) * tabDefaultMinSize
          initSize    = maxSize - minReqSize
          extend r x  = do (cs,s,s2) <- r
                           (c,s') <- tablify (SamePrioNo 9) (initSize - s + s2) x
                           return (cs ++ [c], s + s', s2 + tabDefaultMinSize)
      in do (comps, total, _) <- foldl extend (return ([],0,tabDefaultMinSize)) xs
            return (tabBrack $ tabBesides $ intersperse (tabTxt ", ") comps, total + minSurround)

  minTableLength xs = 2 + (2 + tabDefaultMinSize) * length xs

instance RulerValue a => Tabular (Map Ident a) where
  tablify _ maxSize mp
    = let n              = Map.size mp
          ks             = Map.keys mp
          xs             = Map.assocs mp
          ksSize         = sum (map (length.show) ks)
          minSurround    = 2 * max 1 (n-1) + ksSize + 4 * n
          minReqSize     = minSurround + max 0 (n-1) * tabDefaultMinSize
          initSize       = maxSize - minReqSize
          extend r (k,x) = do (cs,s,s2) <- r
                              (c,s') <- tablify (SamePrioNo 9) (initSize - s - s2) x
                              return (cs ++ arr k c, s + s', s2 + tabDefaultMinSize)
          arr k c        = [ tabBesides [ tabTxt (show k ++ " -> "), c ] ]
      in do (comps, total, _) <- foldl extend (return ([], 0, tabDefaultMinSize)) xs
            return (tabCurly $ tabBesides $ intersperse (tabTxt ", ") comps, total + minSurround)

  minTableLength mp = let n      = Map.size mp
                          ks     = Map.keys mp
                          ksSize = sum (map (length.show) ks)
                      in (6 + tabDefaultMinSize) * n + ksSize

instance Tabular Value where
  tablify prio maxSize v
    = case v of
        ValueOpaque _ v' _ -> tablify prio maxSize v'
        ValueGuess g       -> do opts <- asks itOpts
                                 mb <- valLookupIT g
                                 case mb of
                                   Just v' | expansion opts /= ExpandNone &&
                                             maxSize >= minTableLength v' -> tablify prio maxSize v'
                                   Just (ValueOpaque g' _ _)              -> tablifyGuess g'
                                   _                                      -> tablifyGuess g
        _                  -> txtShowTablify v

  minTableLength (ValueOpaque _ v _) = minTableLength v
  minTableLength _ = tabDefaultMinSize
}


--
-- Some data types for primitive values with holes.
-- Instances are generated in Externals.hs
--

{
data PrimInt
  = PI !Int
  | IndPI !IndInfo !(Maybe PrimInt)
  deriving (Eq, Ord, Show, Typeable)

instance Tabular PrimInt where
  tablify _ maxSize (PI i)
    = txtShowTablify i
  tablify prio maxSize (IndPI (IndInfo g) mb)
    = case mb of
        Nothing -> tablifyGuess g
        Just ps -> tablify prio maxSize ps
  minTableLength _ = 0

data PrimString
  = PS !String
  | IndPS !IndInfo !(Maybe PrimString)
  deriving (Show, Typeable, Eq, Ord)

instance Tabular PrimString where
  tablify _ maxSize (PS s)
    = let ss = wrapString maxSize s
          n  = maximum (map length ss)
      in return (tabAboves (map tabTxt ss), n)
  tablify prio maxSize (IndPS (IndInfo g) mb)
    = case mb of
        Nothing -> tablifyGuess g
        Just ps -> tablify prio maxSize ps
}


--
-- Substitution garbage collector
--

{
substCollectGarbage :: Bool -> I ()
substCollectGarbage _ = return ()

{-
-- Disabled garbage collection. Reason: it does not take
-- new Segments into account, so all bindings in ThunkStmts
-- in such a segment are not taken as roots, which may thus
-- be garbage collected.
substCollectGarbage force
  = do lastSize <- gets ssLastSubstSize
       subst    <- gets ssSubst
       let curSize = IntMap.size subst
       if not force && abs (curSize - lastSize) < lastSize
        then return ()  -- skip garbage collection when the substitution is not that big
        else do vRoot <- expand (ValueGuess rootGuess)
                if isGuess vRoot
                 then return ()
                 else do withDebugLevel 3 $ message "running garbage collector"
                         bndgs1  <- asks isBindings
                         bndgs2  <- asks isBindingsStack
                         gBndgs1 <- dgv bndgs1
                         gBndgs2 <- dgv bndgs2
                         extra   <- gets ssExtraRoots
                         gExtra  <- dgv extra
                         let roots = IntSet.insert rootGuess (IntSet.unions [gExtra, gBndgs1, gBndgs2])
                         live <- chase roots roots
                         let subst'   = IntMap.filterWithKey (\k _ -> k `IntSet.member` live) subst
                             newSize  = IntMap.size subst'
                             diff     = curSize - newSize
                         modify (\ss -> ss { ssSubst = subst', ssLastSubstSize = newSize })
                         when (diff > 0) $
                           withDebugLevel 2 $
                             message ("gc: cleanup of " ++ show diff ++ " entries in subsitution. From " ++ show curSize ++ " entries to " ++ show newSize ++ " entries.")
  where
    chase :: IntSet -> IntSet -> I IntSet
    chase acc todo
      | IntSet.null todo = return acc
      | otherwise
          = do let gs = IntSet.toList todo
               gss <- mapM chaseGuess gs
               let todo' = IntSet.unions gss `IntSet.difference` acc
                   acc'  = IntSet.union todo' acc
               chase acc' todo'

    chaseGuess :: Guess -> I IntSet
    chaseGuess g
      = do subst <- gets ssSubst
           case IntMap.lookup g subst of
             Just v  -> dgv v
             Nothing -> return IntSet.empty
-}
}


--
-- Functions for externals, for hiding the Value data type in external functions
-- and data types.
--
-- It is important that this Value data type is hidden!
--

{
-- A PolyInd represents a polymorphic hole, of which the type is discovered
-- later.
data PolyInd a where
  PolyInd   :: IndInfo -> Maybe (PolyInd a) -> PolyInd a
  PolyKnown :: RulerValue b => b -> PolyInd a

-- Trickery! We will only perform "type casts" on the "a" of a PlolyInd when
-- we know exactly what its type is (i.e. take the dictionary from PolyKnown).
-- Therefore, we don't need a Typeable dictionary of a, although we need one
-- to derive it from (PolyInd a). Therefore, we steal the typeOf a dummy data
-- type, that nobody else is supposed to use. We only need it for the
-- type safe cast.
instance Typeable (PolyInd a) where
  typeOf _ = typeOf PolyDummy

data PolyDummy = PolyDummy
  deriving Typeable

instance Show (PolyInd a) where
  show (PolyInd i (Just a)) = show a
  show (PolyInd i Nothing)  = "#" ++ show i
  show (PolyKnown a)        = show a

instance RulerValue (PolyInd a) where
  unify (PolyKnown x) (PolyKnown y)
    = case cast x of
        Nothing -> abort "Unifying two PolyInd values storing different types"
        Just x' -> unify x' y
  unify (PolyInd (IndInfo g1) _) (PolyInd (IndInfo g2) _)
    = unify (ValueGuess g1) (ValueGuess g2)
  unify (PolyInd (IndInfo g) _) (PolyKnown a)
    = do v <- mkOpaque a
         unify (ValueGuess g) v
  unify (PolyKnown a) (PolyInd (IndInfo g) _)
    = do v <- mkOpaque a
         unify v (ValueGuess g)

  unifyS _ _ = abort "do not call unifyS on PolyInd"

  fgv acc (PolyInd (IndInfo g) mbInd)
    = case mbInd of
        Nothing -> fgv acc (ValueGuess g)
        Just a  -> fgv acc a
  fgv acc (PolyKnown a)
    = fgv acc a
  fgvS _ _ = abort "do not call fgv on PolyInd"

  dgv (PolyInd (IndInfo g) mbInd)
    = case mbInd of
        Nothing -> return $ IntSet.singleton g
        Just a  -> do gs <- dgv a
                      return (IntSet.insert g gs)
  dgv (PolyKnown a)
    = dgv a
  dgvS _                  = abort "do not call dgvS on PolyInd"

  expAll lk v@(PolyInd (IndInfo g) mbInd)
    = case mbInd of
        Nothing -> return v
        Just a  -> do a' <- expAll lk a
                      return (PolyInd (IndInfo g) (Just a'))
  expAll lk (PolyKnown a)
    = do a' <- expAll lk a
         return (PolyKnown a')
  expAllS _ _ = fail "do not call expAllS on PolyInd"

  toIndirection i mbInd
    = return (PolyInd i mbInd)

  fromIndirection (PolyInd i mb) = (Just i, mb)
  fromIndirection (PolyKnown a)  = let (ind,mb) = fromIndirection a
                                   in (ind, maybe Nothing (Just . PolyKnown) mb)

  -- assume v in expanded form
  rvCast v
    | isJust mbVal = Just $ PolyKnown (fromJust mbVal)
    | isJust mbInd = Just $ PolyInd (fromJust mbInd) Nothing
    | otherwise    = cast v
    where
      (mbInd, mbVal) = fromIndirection v

instance Tabular (PolyInd a) where
  tablify prio maxSize (PolyInd (IndInfo g) mbInd)
    = case mbInd of
        Nothing -> do mbP <- valLookupIT g
                      case mbP of
                        Just p  -> tablify prio maxSize p
                        Nothing -> tablify prio maxSize (ValueGuess g)
        Just a  -> tablify prio maxSize a
  tablify prio maxSize (PolyKnown a)
    = tablify prio maxSize a
  
  minTableLength (PolyInd _ Nothing)  = 5
  minTableLength (PolyInd _ (Just a)) = minTableLength a
  minTableLength (PolyKnown a)        = minTableLength a

instance Eq (PolyInd a) where
  a == b = case (lastPoly a, lastPoly b) of
             (PolyKnown a1, PolyKnown b1) -> case cast a1 of
                                               Just a2 -> a2 == b1
                                               Nothing -> False -- invalid types cannot be equal
             _                            -> error "PolyInd is not fully known, cannot test equality"

instance Ord (PolyInd a) where
  compare a b = case (lastPoly a, lastPoly b) of
                 (PolyKnown a1, PolyKnown b1) -> case cast a1 of
                                                   Just a2 -> a2 `compare` b1
                                                   Nothing -> error "the two PolyInds are of different types, cannot compare them."
                 _                            -> error "PolyInd is not fully known, cannot compare"

lastPoly :: PolyInd a -> PolyInd a
lastPoly kn@(PolyKnown _)        = kn
lastPoly ind@(PolyInd _ Nothing) = ind
lastPoly (PolyInd _ (Just p))    = lastPoly p

mapInd :: RulerValue a => (a -> I a) -> PolyInd a -> I (PolyInd a)
mapInd f (PolyInd i (Just p))
  = do p' <- mapInd f p
       return p'
mapInd f (PolyKnown b)
  = case cast b of
      Just a -> f a >>= return . PolyKnown
      Nothing -> abort "mapInd: inconsistent types"
mapInd _ p
  = abort "cannot map a function onto a guess"

data Poly = forall a . RulerValue a => Poly a   -- a polymorphic value
newtype PolyArg a = PolyArg Poly

indToPoly :: PolyInd (PolyArg a) -> PolyArg a
indToPoly x@(PolyInd _ _) = PolyArg (Poly x)
indToPoly (PolyKnown x)   = PolyArg (Poly x)

polyToInd :: PolyArg a -> PolyInd a
polyToInd (PolyArg (Poly v))
  | isJust mbInd = PolyInd (fromJust mbInd) Nothing
  | isJust mbVal = PolyKnown (fromJust mbVal)
  where (mbInd,mbVal) = fromIndirection v

resolveToKnown :: PolyInd a -> I (PolyInd a)
resolveToKnown ind@(PolyKnown _) = return ind
resolveToKnown (PolyInd g _)
  = do p <- extResolve g
       case p of
         PolyInd _ Nothing  -> abort "couldnt resolve the polymorphic value to a known value"
         PolyInd _ (Just p) -> resolveToKnown p

-- creates an indirection to the value of a and returns it
extIndirect :: RulerValue a => a -> I a
extIndirect a
  = do a' <- extFresh
       unify a' a
       return a'

-- creates a fresh value a
extFresh :: RulerValue a => I a
extFresh = do c <- nextUnique
              toIndirection (IndInfo c) Nothing

-- expands a value of type a
extExpand :: RulerValue a => a -> I a
extExpand a
    = case fromIndirection a of
        (Just i,_)  -> extResolve i
        (Nothing,_) -> return a

-- resolves a guess to a concrete value (or an indirection in the right domain)
extResolve :: forall a . RulerValue a => IndInfo -> I a
extResolve (IndInfo g)
  = let v = ValueGuess g
    in do v' <- expand v
          case v' of
            ValueGuess g'      -> toIndirection (IndInfo g') Nothing
            ValueOpaque g' r _ -> case rvCast r of
                                    Nothing -> abort ("value " ++ show v' ++ " has incompatible type. Found: " ++ show (typeOf r) ++ ", expecting: " ++ show (typeOf (undefined :: a)))
                                    Just a  -> toIndirection (IndInfo g') $ Just a
            _                  -> abort ("Not an opaque value nor a guess: " ++ show v')
}