MiniAgda-0.2019.12.13: src/Value.hs
{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}
module Value where
import Prelude hiding (null)
import Control.Applicative
import Control.Monad.Except
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 v = 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 []
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
{-
data MeasVal = MeasVal [Val] -- lexicographic termination measure
deriving (Eq,Ord,Show)
-}
-- 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 = 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 = VSort $ SortC TSize
vTopSort :: Val
vTopSort = VSort $ Set VInfty
mkClos :: Env -> Expr -> Val
mkClos rho Infty = VInfty
mkClos rho 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 rho (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 ns [] = []
filterEnv ns ((x,v) : rho) =
if Set.member x ns then (x,v) : filterEnv (Set.delete x ns) rho
else filterEnv ns rho
vDef id = VDef id `VApp` []
vCon co n = vDef $ DefId (ConK co) n
-- vCon co n = vDef $ DefId (ConK (coToConK co)) n
vFun n = vDef $ DefId FunK $ QName n
vDat n = vDef $ DefId DatK n
{- POSSIBLY BREAKS INVARIANT!
vApp :: Val -> [Val] -> Val
vApp f [] = f
vApp f vs = VApp f vs
-}
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 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 = succSize
-- "multiplication" of sizes
plusSize :: Val -> Val -> Val
plusSize VZero v = v
plusSize v VZero = v
plusSize VInfty v = VInfty
plusSize v 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 v 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 v =
case v of
(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)