MiniAgda-0.2025.7.23: src/Value.hs
{-# 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)