content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}
  
  module Value where
  
  import Prelude hiding (null)
  
  #if !MIN_VERSION_base(4,8,0)
  import Control.Applicative
  #endif
  import Control.Monad.Except (MonadError)
  
  import qualified Data.List as List
  import Data.Set (Set)
  import qualified Data.Set as Set
  -- import Debug.Trace
  
  import Abstract
  import Polarity
  import Util
  import TraceError -- orM
  
  -- call-by-value
  -- cofuns are not forced
  
  data Val
    -- sizes
    = VInfty
    | VZero
    | VSucc Val
    | VMax [Val]
    | VPlus [Val]
    | VMeta MVar Env Int           -- X rho + n  (n-fold successor of X rho)
    -- types
    | VSort (Sort Val)
    | VMeasured (Measure Val) Val  -- mu -> A  (only in checkPattern)
    | VGuard (Bound Val) Val       -- mu<mu' -> A
    | VBelow LtLe Val              -- domain in bounded size quant.
    | VQuant
      { vqPiSig :: PiSigma
      , vqName  :: Name
      , vqDom   :: Domain
      , vqFun   :: FVal
      }
    | VSing Val TVal               -- Singleton type (TVal not Pi)
    -- functions
    | VLam Name Env Expr
    | VAbs Name Int Val Valuation  -- abstract free variable
    | VConst Val                   -- constant function
    | VUp Val TVal                 -- delayed eta expansion; TVal is a Pi
    -- values
    | VRecord RecInfo EnvMap       -- a record value / fully applied constructor
    | VPair Val Val                -- eager pair
    -- neutrals
    | VGen Int                     -- free variable (de Bruijn level)
    | VDef DefId                   -- co(data/constructor/fun)
                                   -- VDef occurs only inside a VApp!
    | VCase Val TVal Env [Clause]
    | VApp Val [Clos]
    -- closures
    | VProj PrePost Name           -- a projection as an argument to a neutral
    | VClos Env Expr               -- closure for cbn evaluation
    -- don't care
    | VIrr                         -- erased hypothetical inhabitant of empty type
      deriving (Eq,Ord)
  
  -- | Makes constant function if name is empty.
  vLam :: Name -> Env -> Expr -> FVal
  vLam x env e
    | emptyName x = VConst $ VClos env e
    | otherwise   = VLam x env e
  
  -- | Is a value a function?  May become more @True@ after forcing the @VUp@.
  isFun :: Val -> Bool
  isFun VLam{}                         = True
  isFun VAbs{}                         = True
  isFun VConst{}                       = True
  isFun (VUp _ VQuant{ vqPiSig = Pi }) = True
  isFun _                              = False
  
  absName :: FVal -> Name
  absName fv =
    case fv of
      VLam x _ _              -> x
      VAbs x _ _ _            -> x
      VUp _ (VQuant Pi x _ _) -> x
      _                       -> noName
  
  type FVal = Val
  type TVal = Val -- type value
  type Clos = Val
  type Domain = Dom TVal
  
  -- | Valuation of free variables.
  newtype Valuation = Valuation { valuation :: [(Int,Val)] }
    deriving (Eq,Ord)
  
  emptyVal :: Valuation
  emptyVal  = Valuation []
  
  sgVal :: Int -> Val -> Valuation
  sgVal i v = Valuation [(i,v)]
  
  valuateGen :: Int -> Valuation -> Val
  valuateGen i valu = maybe (VGen i) id $ lookup i $ valuation valu
  
  type TeleVal = [TBinding Val]
  
  data Environ a = Environ
    { envMap   :: [(Name,a)]          -- the actual map from names to values
    , envBound :: Maybe (Measure Val) -- optionally the current termination measure
    }
    deriving (Eq, Ord, Show)
  
  type EnvMap = [(Name,Val)]
  type Env = Environ Val
  
  -- smart constructors ------------------------------------------------
  
  -- | The value representing type Size.
  vSize :: Val
  vSize = VBelow Le VInfty -- 2012-01-28 non-termination bug I have not found
  -- vSize = VSort $ SortC Size
  
  vFinSize :: Val
  vFinSize = VBelow Lt VInfty
  
  -- | Ensure we construct the correct value representing Size.
  vSort :: Sort Val -> Val
  vSort (SortC Size) = vSize
  vSort s            = VSort s
  
  isVSize :: Val -> Bool
  isVSize (VSort (SortC Size)) = True
  isVSize (VBelow Le VInfty)   = True
  isVSize _                    = False
  
  vTSize :: Val
  vTSize = VSort $ SortC TSize
  
  vTopSort :: Val
  vTopSort = VSort $ Set VInfty
  
  mkClos :: Env -> Expr -> Val
  mkClos _   Infty       = VInfty
  mkClos _   Zero        = VZero
  -- mkClos rho (Succ e)    = VSucc (mkClos rho e)  -- violates an invariant!! succeed/crazys
  mkClos rho (Below ltle e) = VBelow ltle (mkClos rho e)
  mkClos _   (Proj fx n) = VProj fx n
  mkClos rho (Var x) = lookupPure rho x
  mkClos rho (Ann e) = mkClos rho $ unTag e
  mkClos rho e = VClos rho e
    -- Problem with MetaVars: freeVars of a meta var is unknown in this repr.!
    -- VClos (rho { envMap = filterEnv (freeVars e) (envMap rho)}) e
  
  filterEnv :: Set Name -> EnvMap -> EnvMap
  filterEnv _  [] = []
  filterEnv ns ((x,v) : rho) =
    if Set.member x ns then (x,v) : filterEnv (Set.delete x ns) rho
     else filterEnv ns rho
  
  vDef :: DefId -> Val
  vDef x = VDef x `VApp` []
  
  vCon :: ConK -> QName -> Val
  vCon co n = vDef $ DefId (ConK co) n
  -- vCon co n = vDef $ DefId (ConK (coToConK co)) n
  
  vFun :: Name -> Val
  vFun n = vDef $ DefId FunK $ QName n
  
  vDat :: QName -> Val
  vDat n = vDef $ DefId DatK n
  
  vAbs :: Name -> Int -> Val -> FVal
  vAbs x i v = VAbs x i v emptyVal
  
  arrow , prod :: TVal -> TVal -> TVal
  arrow = quant Pi
  prod  = quant Sigma
  
  quant :: PiSigma -> TVal -> Val -> Val
  quant piSig a b = VQuant piSig x (defaultDomain a) (VConst b)
    where x   = fresh ""
  -- quant piSig a b = VQuant piSig x (defaultDomain a) (Environ [(bla,b)] Nothing) (Var bla)
  --   where x   = fresh ""
  --         bla = fresh "#codom"
  
  
  -- * Sizes ------------------------------------------------------------
  
  -- Sizes form a commutative semiring with multiplication (Plus) and
  -- idempotent addition (Max)
  --
  -- Wellformed size values are polynomials, i.e., sums (Max) of products (Plus).
  -- A monomial m takes one of the forms (k stands for a variable: VGen or VMeta)
  -- 0. VSucc^* VZero
  -- 1. VSucc^* k
  -- 2. VSucc^* (VPlus [k1,...,kn])   where n>=2
  -- A polynomial takes one of the forms
  -- 0. VInfty
  -- 1. m
  -- 2. VMax ms  where length ms >= 2 and each mi different
  {- OLD
  -- - VSucc^* VGen
  -- - VMax vs where each v_i = VSucc^* (VGen k_i) and all k_i different
  --           and vs has length >= 2
  -}
  --
  -- the smart constructors construct wellformed size values using the laws
  -- $ #             = #                Infty
  -- max # k         = #
  -- $ (max i j)     = max ($ i) ($ j)  $ distributes over max
  -- max (max i j) k = max i j k        Assoc-Commut of max
  -- max i i         = i                Idempotency of max
  succSize :: Val -> Val
  succSize v = case v of
              VInfty -> VInfty
              VMax vs -> maxSize $ map succSize vs
              VMeta i rho n -> VMeta i rho (n + 1)  -- TODO: integrate + and mvar
              _ -> VSucc v
  
  vSucc :: Val -> Val
  vSucc = succSize
  
  -- "multiplication" of sizes
  plusSize :: Val -> Val -> Val
  plusSize VZero v = v
  plusSize v VZero = v
  plusSize VInfty _ = VInfty
  plusSize _ VInfty = VInfty
  plusSize (VMax vs) v = maxSize $ map (plusSize v) vs
  plusSize v (VMax vs) = maxSize $ map (plusSize v) vs
  plusSize (VSucc v) v' = succSize $ plusSize v v'
  plusSize v' (VSucc v) = succSize $ plusSize v v'
  plusSize (VPlus vs) (VPlus vs') = VPlus $ List.sort (vs ++ vs') -- every summand is a var!  -- TODO: more efficient sorting!
  plusSize (VPlus vs) v = VPlus $ List.insert v vs
  plusSize v (VPlus vs) = VPlus $ List.insert v vs
  plusSize v v' = VPlus $ List.sort [v,v']
  
  plusSizes :: [Val] -> Val
  plusSizes [] = VZero
  plusSizes [v] = v
  plusSizes (v:vs) = v `plusSize` (plusSizes vs)
  
  -- maxSize vs = VInfty                 if any v_i=Infty
  --            = VMax (sort (nub (flatten vs)) else
  -- precondition vs
  
  maxSize :: [Val] -> Val
  maxSize vs = case Set.toList . Set.fromList <$> flatten vs of
     Nothing -> VInfty
     Just [] -> VZero
     Just [v] -> v
     Just vs' -> VMax vs'
    where flatten (VZero:vs) = flatten vs
          flatten (VInfty:_) = Nothing
          flatten (VMax vs:vs') = flatten vs' >>= return . (vs++)
          flatten (v:vs) = flatten vs >>= return . (v:)
          flatten [] = return []
  
  {-
  maxSize :: [Val] -> Val
  maxSize vs = case flatten [] vs of
     [] -> VInfty
     [v] -> v
     vs' -> VMax vs'
    where flatten acc (VInfty:_) = []
          flatten acc (VMax vs:vs') = flatten (vs ++ acc) vs'
          flatten acc (v:vs) = flatten (v:acc) vs
          flatten acc [] = Set.toList $ Set.fromList acc -- sort, nub
  -}
  
  -- * destructors -------------------------------------------------------
  
  vSortToSort :: Sort Val -> Sort Expr
  vSortToSort (SortC c)    = SortC c
  vSortToSort (Set VInfty) = Set Infty
  
  predSize :: Val -> Maybe Val
  predSize VInfty = Just VInfty
  predSize (VSucc v) = Just v
  predSize (VMax vs) = do vs' <- mapM predSize vs
                          return $ maxSize vs'
  predSize (VMeta v rho n) | n > 0 = return $ VMeta v rho (n-1)
  predSize _ = Nothing -- variable or zero or sum
  
  instance HasPred Val where
    predecessor VInfty = Nothing -- for printing bounds
    predecessor v = predSize v
  
  isFunType :: TVal -> Bool
  isFunType VQuant{ vqPiSig = Pi } = True
  isFunType _                      = False
  
  isDataType :: TVal -> Bool
  isDataType (VApp (VDef (DefId DatK _)) _) = True
  isDataType (VSing _ tv) = isDataType tv
  isDataType _ = False
  
  -- * ugly printing -----------------------------------------------------
  
  instance Show (Sort Val) where
    show (SortC c) = show c
    show (Set VZero) = "Set"
    show (CoSet VInfty) = "Set"
    show (Set v) = parens $ ("Set " ++ show v)
    show (CoSet v) = parens $ ("CoSet " ++ show v)
  
  instance Show Val where
    show v | isVSize v = "Size"
    show (VSort s) = show s
    show VInfty = "#"
    show VZero = "0"
    show (VSucc v) = "($ " ++ show v ++ ")"
    show (VMax vl) = "(max " ++ showVals vl ++ ")"
    show (VPlus (v:vl)) = parens $ foldr (\ v s -> show v ++ " + " ++ s) (show v) vl
    show (VApp v []) = show v
    show (VApp v vl) = "(" ++ show v ++ " " ++ showVals vl ++ ")"
    show (VDef id) = show id
    show (VProj Pre id) = show id
    show (VProj Post id) = "." ++ show id
    show (VPair v1 v2) = "(" ++ show v1 ++ ", " ++ show v2 ++ ")"
    show (VGen k) = "v" ++ show k
    show (VMeta k rho 0) = "?" ++ show k ++ showEnv rho
    show (VMeta k rho 1) = "$?" ++ show k ++ showEnv rho
    show (VMeta k rho n) = "(?" ++ show k ++ showEnv rho ++ " + " ++ show n ++")"
    show (VRecord ri env) = show ri ++ "{" ++ Util.showList "; " (\ (n, v) -> show n ++ " = " ++ show v) env ++ "}"
    show (VCase v vt env cs) = "case " ++ show v ++ " : " ++ show vt ++ " { " ++ showCases cs ++ " } " ++ showEnv env
    show (VClos (Environ [] Nothing) e) = showsPrec precAppR e ""
    show (VClos env e) = "{" ++ show e ++ " " ++ showEnv env ++ "}"
    show (VSing v vt) = "<" ++ show v ++ " : " ++ show vt ++ ">"
    show VIrr  = "."
    show (VMeasured mu tv) = parens $ show mu ++ " -> " ++ show tv
    show (VGuard beta tv) = parens $ show beta ++ " -> " ++ show tv
    show (VBelow ltle v) = show ltle ++ " " ++ show v
  
    show (VQuant pisig x (Domain (VBelow ltle v) _ki dec) bv)
         | (ltle,v) /= (Le,VInfty) =
         parens $ (\ p -> if p==defaultPol then "" else show p) (polarity dec) ++
                  (if erased dec then brackets binding else parens binding)
                   ++ " " ++ show pisig ++ " " ++ showSkipLambda bv
              where binding = show x ++ " " ++ show ltle ++ " " ++ show v
  
    show (VQuant pisig x (Domain av ki dec) bv) =
          parens $ (\ p -> if p==defaultPol then "" else show p) (polarity dec) ++
                  (if erased dec then brackets binding
                    else if emptyName x then s1 else parens binding)
                      ++ " " ++ show pisig ++ " " ++ showSkipLambda bv
               where s1 = s2 ++ s0
                     s2 = show av
                     s3 = show ki
                     s0 = if ki == defaultKind || s2 == s3 then "" else "::" ++ s3
                     binding = if emptyName x then  s1 else show x ++ " : " ++ s1
  
    show (VLam x env e) = "(\\" ++ show x ++ " -> " ++ show e ++ showEnv env ++ ")"
    show (VConst v) = "(\\ _ -> " ++ show v ++ ")"
    show (VAbs x i v valu) = "(\\" ++ show x ++ "@" ++ show i ++ show v ++ showValuation valu ++ ")"
    show (VUp v vt) = "(" ++ show v ++ " Up " ++ show vt ++ ")"
  
  showSkipLambda :: Val -> String
  showSkipLambda = \case
      (VLam _x env e)     -> show e ++ showEnv env
      (VConst v)          -> show v
      (VAbs _x _i v valu) -> show v ++ showValuation valu
      v                   -> show v
  
  showVals :: [Val] -> String
  showVals [] = ""
  showVals (v:vl) = show v ++ (if null vl then "" else " " ++ showVals vl)
  
  -- environment ---------------------------------------------------
  
  emptyEnv :: Environ a
  emptyEnv = Environ [] Nothing
  
  appendEnv :: Environ a -> Environ a -> Environ a
  appendEnv (Environ rho mmeas) (Environ rho' mmeas') =
    Environ (rho ++ rho') (orM mmeas mmeas')
  
  -- | enviroment extension / update
  update :: Environ a -> Name -> a -> Environ a
  update env n v | emptyName n = env
                 | otherwise   = env { envMap = (n,v) : envMap env }
  
  lookupPure :: Show a => Environ a -> Name -> a
  lookupPure rho x =
      case lookup x (envMap rho) of
        Just v -> v
        Nothing -> error $ "lookupPure: unbound identifier " ++ show x ++ " in environment " ++ show rho
  
  lookupEnv :: MonadError TraceError m => Environ a -> Name -> m a
  lookupEnv rho x =
      case lookup x (envMap rho) of
        Just v -> return $ v
        Nothing -> throwErrorMsg $ "lookupEnv: unbound identifier " ++ show x --  ++ " in environment " ++ show rho
  
  showValuation :: Valuation -> String
  showValuation (Valuation [])  = ""
  showValuation (Valuation tau) = "{" ++ Util.showList ", " (\(i,v) -> show i ++ " = " ++ show v) tau ++ "}"
  
  showEnv :: Environ Val -> String
  showEnv (Environ [] Nothing)   = ""
  showEnv (Environ rho Nothing)  = "{" ++ showEnv' rho ++ "}"
  showEnv (Environ [] (Just mu)) = "{ measure=" ++ show mu ++ " }"
  showEnv (Environ rho (Just mu)) = "{" ++ showEnv' rho ++ " | measure=" ++ show mu ++ " }"
  
  showEnv' :: EnvMap -> String
  showEnv' = Util.showList ", " (\ (n,v) -> show n ++ " = " ++ show v)
  