{-# 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
    { Val -> PiSigma
vqPiSig :: PiSigma
    , Val -> Name
vqName  :: Name
    , Val -> Domain
vqDom   :: Domain
    , Val -> Val
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 (Val -> Val -> Bool
(Val -> Val -> Bool) -> (Val -> Val -> Bool) -> Eq Val
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Val -> Val -> Bool
== :: Val -> Val -> Bool
$c/= :: Val -> Val -> Bool
/= :: Val -> Val -> Bool
Eq,Eq Val
Eq Val =>
(Val -> Val -> Ordering)
-> (Val -> Val -> Bool)
-> (Val -> Val -> Bool)
-> (Val -> Val -> Bool)
-> (Val -> Val -> Bool)
-> (Val -> Val -> Val)
-> (Val -> Val -> Val)
-> Ord Val
Val -> Val -> Bool
Val -> Val -> Ordering
Val -> Val -> Val
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Val -> Val -> Ordering
compare :: Val -> Val -> Ordering
$c< :: Val -> Val -> Bool
< :: Val -> Val -> Bool
$c<= :: Val -> Val -> Bool
<= :: Val -> Val -> Bool
$c> :: Val -> Val -> Bool
> :: Val -> Val -> Bool
$c>= :: Val -> Val -> Bool
>= :: Val -> Val -> Bool
$cmax :: Val -> Val -> Val
max :: Val -> Val -> Val
$cmin :: Val -> Val -> Val
min :: Val -> Val -> Val
Ord)

-- | Makes constant function if name is empty.
vLam :: Name -> Env -> Expr -> FVal
vLam :: Name -> Env -> Expr -> Val
vLam Name
x Env
env Expr
e
  | Name -> Bool
emptyName Name
x = Val -> Val
VConst (Val -> Val) -> Val -> Val
forall a b. (a -> b) -> a -> b
$ Env -> Expr -> Val
VClos Env
env Expr
e
  | Bool
otherwise   = Name -> Env -> Expr -> Val
VLam Name
x Env
env Expr
e

-- | Is a value a function?  May become more @True@ after forcing the @VUp@.
isFun :: Val -> Bool
isFun :: Val -> Bool
isFun VLam{}                         = Bool
True
isFun VAbs{}                         = Bool
True
isFun VConst{}                       = Bool
True
isFun (VUp Val
_ VQuant{ vqPiSig :: Val -> PiSigma
vqPiSig = PiSigma
Pi }) = Bool
True
isFun Val
_                              = Bool
False

absName :: FVal -> Name
absName :: Val -> Name
absName Val
fv =
  case Val
fv of
    VLam Name
x Env
_ Expr
_              -> Name
x
    VAbs Name
x Int
_ Val
_ Valuation
_            -> Name
x
    VUp Val
_ (VQuant PiSigma
Pi Name
x Domain
_ Val
_) -> Name
x
    Val
_                       -> Name
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)]
valuation :: [(Int,Val)] }
  deriving (Valuation -> Valuation -> Bool
(Valuation -> Valuation -> Bool)
-> (Valuation -> Valuation -> Bool) -> Eq Valuation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Valuation -> Valuation -> Bool
== :: Valuation -> Valuation -> Bool
$c/= :: Valuation -> Valuation -> Bool
/= :: Valuation -> Valuation -> Bool
Eq,Eq Valuation
Eq Valuation =>
(Valuation -> Valuation -> Ordering)
-> (Valuation -> Valuation -> Bool)
-> (Valuation -> Valuation -> Bool)
-> (Valuation -> Valuation -> Bool)
-> (Valuation -> Valuation -> Bool)
-> (Valuation -> Valuation -> Valuation)
-> (Valuation -> Valuation -> Valuation)
-> Ord Valuation
Valuation -> Valuation -> Bool
Valuation -> Valuation -> Ordering
Valuation -> Valuation -> Valuation
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Valuation -> Valuation -> Ordering
compare :: Valuation -> Valuation -> Ordering
$c< :: Valuation -> Valuation -> Bool
< :: Valuation -> Valuation -> Bool
$c<= :: Valuation -> Valuation -> Bool
<= :: Valuation -> Valuation -> Bool
$c> :: Valuation -> Valuation -> Bool
> :: Valuation -> Valuation -> Bool
$c>= :: Valuation -> Valuation -> Bool
>= :: Valuation -> Valuation -> Bool
$cmax :: Valuation -> Valuation -> Valuation
max :: Valuation -> Valuation -> Valuation
$cmin :: Valuation -> Valuation -> Valuation
min :: Valuation -> Valuation -> Valuation
Ord)

emptyVal :: Valuation
emptyVal :: Valuation
emptyVal  = [(Int, Val)] -> Valuation
Valuation []

sgVal :: Int -> Val -> Valuation
sgVal :: Int -> Val -> Valuation
sgVal Int
i Val
v = [(Int, Val)] -> Valuation
Valuation [(Int
i,Val
v)]

valuateGen :: Int -> Valuation -> Val
valuateGen :: Int -> Valuation -> Val
valuateGen Int
i Valuation
valu = Val -> (Val -> Val) -> Maybe Val -> Val
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> Val
VGen Int
i) Val -> Val
forall a. a -> a
id (Maybe Val -> Val) -> Maybe Val -> Val
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Val)] -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
i ([(Int, Val)] -> Maybe Val) -> [(Int, Val)] -> Maybe Val
forall a b. (a -> b) -> a -> b
$ Valuation -> [(Int, Val)]
valuation Valuation
valu

type TeleVal = [TBinding Val]

data Environ a = Environ
  { forall a. Environ a -> [(Name, a)]
envMap   :: [(Name,a)]          -- the actual map from names to values
  , forall a. Environ a -> Maybe (Measure Val)
envBound :: Maybe (Measure Val) -- optionally the current termination measure
  }
  deriving (Environ a -> Environ a -> Bool
(Environ a -> Environ a -> Bool)
-> (Environ a -> Environ a -> Bool) -> Eq (Environ a)
forall a. Eq a => Environ a -> Environ a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Environ a -> Environ a -> Bool
== :: Environ a -> Environ a -> Bool
$c/= :: forall a. Eq a => Environ a -> Environ a -> Bool
/= :: Environ a -> Environ a -> Bool
Eq, Eq (Environ a)
Eq (Environ a) =>
(Environ a -> Environ a -> Ordering)
-> (Environ a -> Environ a -> Bool)
-> (Environ a -> Environ a -> Bool)
-> (Environ a -> Environ a -> Bool)
-> (Environ a -> Environ a -> Bool)
-> (Environ a -> Environ a -> Environ a)
-> (Environ a -> Environ a -> Environ a)
-> Ord (Environ a)
Environ a -> Environ a -> Bool
Environ a -> Environ a -> Ordering
Environ a -> Environ a -> Environ a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Environ a)
forall a. Ord a => Environ a -> Environ a -> Bool
forall a. Ord a => Environ a -> Environ a -> Ordering
forall a. Ord a => Environ a -> Environ a -> Environ a
$ccompare :: forall a. Ord a => Environ a -> Environ a -> Ordering
compare :: Environ a -> Environ a -> Ordering
$c< :: forall a. Ord a => Environ a -> Environ a -> Bool
< :: Environ a -> Environ a -> Bool
$c<= :: forall a. Ord a => Environ a -> Environ a -> Bool
<= :: Environ a -> Environ a -> Bool
$c> :: forall a. Ord a => Environ a -> Environ a -> Bool
> :: Environ a -> Environ a -> Bool
$c>= :: forall a. Ord a => Environ a -> Environ a -> Bool
>= :: Environ a -> Environ a -> Bool
$cmax :: forall a. Ord a => Environ a -> Environ a -> Environ a
max :: Environ a -> Environ a -> Environ a
$cmin :: forall a. Ord a => Environ a -> Environ a -> Environ a
min :: Environ a -> Environ a -> Environ a
Ord, Int -> Environ a -> ShowS
[Environ a] -> ShowS
Environ a -> String
(Int -> Environ a -> ShowS)
-> (Environ a -> String)
-> ([Environ a] -> ShowS)
-> Show (Environ a)
forall a. Show a => Int -> Environ a -> ShowS
forall a. Show a => [Environ a] -> ShowS
forall a. Show a => Environ a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Environ a -> ShowS
showsPrec :: Int -> Environ a -> ShowS
$cshow :: forall a. Show a => Environ a -> String
show :: Environ a -> String
$cshowList :: forall a. Show a => [Environ a] -> ShowS
showList :: [Environ a] -> ShowS
Show)

type EnvMap = [(Name,Val)]
type Env = Environ Val

-- smart constructors ------------------------------------------------

-- | The value representing type Size.
vSize :: Val
vSize :: Val
vSize = LtLe -> Val -> Val
VBelow LtLe
Le Val
VInfty -- 2012-01-28 non-termination bug I have not found
-- vSize = VSort $ SortC Size

vFinSize :: Val
vFinSize :: Val
vFinSize = LtLe -> Val -> Val
VBelow LtLe
Lt Val
VInfty

-- | Ensure we construct the correct value representing Size.
vSort :: Sort Val -> Val
vSort :: Sort Val -> Val
vSort (SortC Class
Size) = Val
vSize
vSort Sort Val
s            = Sort Val -> Val
VSort Sort Val
s

isVSize :: Val -> Bool
isVSize :: Val -> Bool
isVSize (VSort (SortC Class
Size)) = Bool
True
isVSize (VBelow LtLe
Le Val
VInfty)   = Bool
True
isVSize Val
_                    = Bool
False

vTSize :: Val
vTSize :: Val
vTSize = Sort Val -> Val
VSort (Sort Val -> Val) -> Sort Val -> Val
forall a b. (a -> b) -> a -> b
$ Class -> Sort Val
forall a. Class -> Sort a
SortC Class
TSize

vTopSort :: Val
vTopSort :: Val
vTopSort = Sort Val -> Val
VSort (Sort Val -> Val) -> Sort Val -> Val
forall a b. (a -> b) -> a -> b
$ Val -> Sort Val
forall a. a -> Sort a
Set Val
VInfty

mkClos :: Env -> Expr -> Val
mkClos :: Env -> Expr -> Val
mkClos Env
_   Expr
Infty       = Val
VInfty
mkClos Env
_   Expr
Zero        = Val
VZero
-- mkClos rho (Succ e)    = VSucc (mkClos rho e)  -- violates an invariant!! succeed/crazys
mkClos Env
rho (Below LtLe
ltle Expr
e) = LtLe -> Val -> Val
VBelow LtLe
ltle (Env -> Expr -> Val
mkClos Env
rho Expr
e)
mkClos Env
_   (Proj PrePost
fx Name
n) = PrePost -> Name -> Val
VProj PrePost
fx Name
n
mkClos Env
rho (Var Name
x) = Env -> Name -> Val
forall a. Show a => Environ a -> Name -> a
lookupPure Env
rho Name
x
mkClos Env
rho (Ann Tagged Expr
e) = Env -> Expr -> Val
mkClos Env
rho (Expr -> Val) -> Expr -> Val
forall a b. (a -> b) -> a -> b
$ Tagged Expr -> Expr
forall a. Tagged a -> a
unTag Tagged Expr
e
mkClos Env
rho Expr
e = Env -> Expr -> Val
VClos Env
rho Expr
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 :: Set Name -> EnvMap -> EnvMap
filterEnv Set Name
_  [] = []
filterEnv Set Name
ns ((Name
x,Val
v) : EnvMap
rho) =
  if Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
x Set Name
ns then (Name
x,Val
v) (Name, Val) -> EnvMap -> EnvMap
forall a. a -> [a] -> [a]
: Set Name -> EnvMap -> EnvMap
filterEnv (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete Name
x Set Name
ns) EnvMap
rho
   else Set Name -> EnvMap -> EnvMap
filterEnv Set Name
ns EnvMap
rho

vDef :: DefId -> Val
vDef :: DefId -> Val
vDef DefId
x = DefId -> Val
VDef DefId
x Val -> [Val] -> Val
`VApp` []

vCon :: ConK -> QName -> Val
vCon :: ConK -> QName -> Val
vCon ConK
co QName
n = DefId -> Val
vDef (DefId -> Val) -> DefId -> Val
forall a b. (a -> b) -> a -> b
$ IdKind -> QName -> DefId
DefId (ConK -> IdKind
ConK ConK
co) QName
n
-- vCon co n = vDef $ DefId (ConK (coToConK co)) n

vFun :: Name -> Val
vFun :: Name -> Val
vFun Name
n = DefId -> Val
vDef (DefId -> Val) -> DefId -> Val
forall a b. (a -> b) -> a -> b
$ IdKind -> QName -> DefId
DefId IdKind
FunK (QName -> DefId) -> QName -> DefId
forall a b. (a -> b) -> a -> b
$ Name -> QName
QName Name
n

vDat :: QName -> Val
vDat :: QName -> Val
vDat QName
n = DefId -> Val
vDef (DefId -> Val) -> DefId -> Val
forall a b. (a -> b) -> a -> b
$ IdKind -> QName -> DefId
DefId IdKind
DatK QName
n

vAbs :: Name -> Int -> Val -> FVal
vAbs :: Name -> Int -> Val -> Val
vAbs Name
x Int
i Val
v = Name -> Int -> Val -> Valuation -> Val
VAbs Name
x Int
i Val
v Valuation
emptyVal

arrow , prod :: TVal -> TVal -> TVal
arrow :: Val -> Val -> Val
arrow = PiSigma -> Val -> Val -> Val
quant PiSigma
Pi
prod :: Val -> Val -> Val
prod  = PiSigma -> Val -> Val -> Val
quant PiSigma
Sigma

quant :: PiSigma -> TVal -> Val -> Val
quant :: PiSigma -> Val -> Val -> Val
quant PiSigma
piSig Val
a Val
b = PiSigma -> Name -> Domain -> Val -> Val
VQuant PiSigma
piSig Name
x (Val -> Domain
forall a. a -> Dom a
defaultDomain Val
a) (Val -> Val
VConst Val
b)
  where x :: Name
x   = String -> Name
fresh String
""
-- 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 :: Val -> Val
succSize Val
v = case Val
v of
            Val
VInfty -> Val
VInfty
            VMax [Val]
vs -> [Val] -> Val
maxSize ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ (Val -> Val) -> [Val] -> [Val]
forall a b. (a -> b) -> [a] -> [b]
map Val -> Val
succSize [Val]
vs
            VMeta Int
i Env
rho Int
n -> Int -> Env -> Int -> Val
VMeta Int
i Env
rho (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)  -- TODO: integrate + and mvar
            Val
_ -> Val -> Val
VSucc Val
v

vSucc :: Val -> Val
vSucc :: Val -> Val
vSucc = Val -> Val
succSize

-- "multiplication" of sizes
plusSize :: Val -> Val -> Val
plusSize :: Val -> Val -> Val
plusSize Val
VZero Val
v = Val
v
plusSize Val
v Val
VZero = Val
v
plusSize Val
VInfty Val
_ = Val
VInfty
plusSize Val
_ Val
VInfty = Val
VInfty
plusSize (VMax [Val]
vs) Val
v = [Val] -> Val
maxSize ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ (Val -> Val) -> [Val] -> [Val]
forall a b. (a -> b) -> [a] -> [b]
map (Val -> Val -> Val
plusSize Val
v) [Val]
vs
plusSize Val
v (VMax [Val]
vs) = [Val] -> Val
maxSize ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ (Val -> Val) -> [Val] -> [Val]
forall a b. (a -> b) -> [a] -> [b]
map (Val -> Val -> Val
plusSize Val
v) [Val]
vs
plusSize (VSucc Val
v) Val
v' = Val -> Val
succSize (Val -> Val) -> Val -> Val
forall a b. (a -> b) -> a -> b
$ Val -> Val -> Val
plusSize Val
v Val
v'
plusSize Val
v' (VSucc Val
v) = Val -> Val
succSize (Val -> Val) -> Val -> Val
forall a b. (a -> b) -> a -> b
$ Val -> Val -> Val
plusSize Val
v Val
v'
plusSize (VPlus [Val]
vs) (VPlus [Val]
vs') = [Val] -> Val
VPlus ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ [Val] -> [Val]
forall a. Ord a => [a] -> [a]
List.sort ([Val]
vs [Val] -> [Val] -> [Val]
forall a. [a] -> [a] -> [a]
++ [Val]
vs') -- every summand is a var!  -- TODO: more efficient sorting!
plusSize (VPlus [Val]
vs) Val
v = [Val] -> Val
VPlus ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ Val -> [Val] -> [Val]
forall a. Ord a => a -> [a] -> [a]
List.insert Val
v [Val]
vs
plusSize Val
v (VPlus [Val]
vs) = [Val] -> Val
VPlus ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ Val -> [Val] -> [Val]
forall a. Ord a => a -> [a] -> [a]
List.insert Val
v [Val]
vs
plusSize Val
v Val
v' = [Val] -> Val
VPlus ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ [Val] -> [Val]
forall a. Ord a => [a] -> [a]
List.sort [Val
v,Val
v']

plusSizes :: [Val] -> Val
plusSizes :: [Val] -> Val
plusSizes [] = Val
VZero
plusSizes [Val
v] = Val
v
plusSizes (Val
v:[Val]
vs) = Val
v Val -> Val -> Val
`plusSize` ([Val] -> Val
plusSizes [Val]
vs)

-- maxSize vs = VInfty                 if any v_i=Infty
--            = VMax (sort (nub (flatten vs)) else
-- precondition vs

maxSize :: [Val] -> Val
maxSize :: [Val] -> Val
maxSize [Val]
vs = case Set Val -> [Val]
forall a. Set a -> [a]
Set.toList (Set Val -> [Val]) -> ([Val] -> Set Val) -> [Val] -> [Val]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Val] -> Set Val
forall a. Ord a => [a] -> Set a
Set.fromList ([Val] -> [Val]) -> Maybe [Val] -> Maybe [Val]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Val] -> Maybe [Val]
flatten [Val]
vs of
   Maybe [Val]
Nothing -> Val
VInfty
   Just [] -> Val
VZero
   Just [Val
v] -> Val
v
   Just [Val]
vs' -> [Val] -> Val
VMax [Val]
vs'
  where flatten :: [Val] -> Maybe [Val]
flatten (Val
VZero:[Val]
vs) = [Val] -> Maybe [Val]
flatten [Val]
vs
        flatten (Val
VInfty:[Val]
_) = Maybe [Val]
forall a. Maybe a
Nothing
        flatten (VMax [Val]
vs:[Val]
vs') = [Val] -> Maybe [Val]
flatten [Val]
vs' Maybe [Val] -> ([Val] -> Maybe [Val]) -> Maybe [Val]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Val] -> Maybe [Val]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Val] -> Maybe [Val]) -> ([Val] -> [Val]) -> [Val] -> Maybe [Val]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Val]
vs[Val] -> [Val] -> [Val]
forall a. [a] -> [a] -> [a]
++)
        flatten (Val
v:[Val]
vs) = [Val] -> Maybe [Val]
flatten [Val]
vs Maybe [Val] -> ([Val] -> Maybe [Val]) -> Maybe [Val]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Val] -> Maybe [Val]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Val] -> Maybe [Val]) -> ([Val] -> [Val]) -> [Val] -> Maybe [Val]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Val
vVal -> [Val] -> [Val]
forall a. a -> [a] -> [a]
:)
        flatten [] = [Val] -> Maybe [Val]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
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 :: Sort Val -> Sort Expr
vSortToSort (SortC Class
c)    = Class -> Sort Expr
forall a. Class -> Sort a
SortC Class
c
vSortToSort (Set Val
VInfty) = Expr -> Sort Expr
forall a. a -> Sort a
Set Expr
Infty

predSize :: Val -> Maybe Val
predSize :: Val -> Maybe Val
predSize Val
VInfty = Val -> Maybe Val
forall a. a -> Maybe a
Just Val
VInfty
predSize (VSucc Val
v) = Val -> Maybe Val
forall a. a -> Maybe a
Just Val
v
predSize (VMax [Val]
vs) = do vs' <- (Val -> Maybe Val) -> [Val] -> Maybe [Val]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Val -> Maybe Val
predSize [Val]
vs
                        return $ maxSize vs'
predSize (VMeta Int
v Env
rho Int
n) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Val -> Maybe Val
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Maybe Val) -> Val -> Maybe Val
forall a b. (a -> b) -> a -> b
$ Int -> Env -> Int -> Val
VMeta Int
v Env
rho (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
predSize Val
_ = Maybe Val
forall a. Maybe a
Nothing -- variable or zero or sum

instance HasPred Val where
  predecessor :: Val -> Maybe Val
predecessor Val
VInfty = Maybe Val
forall a. Maybe a
Nothing -- for printing bounds
  predecessor Val
v = Val -> Maybe Val
predSize Val
v

isFunType :: TVal -> Bool
isFunType :: Val -> Bool
isFunType VQuant{ vqPiSig :: Val -> PiSigma
vqPiSig = PiSigma
Pi } = Bool
True
isFunType Val
_                      = Bool
False

isDataType :: TVal -> Bool
isDataType :: Val -> Bool
isDataType (VApp (VDef (DefId IdKind
DatK QName
_)) [Val]
_) = Bool
True
isDataType (VSing Val
_ Val
tv) = Val -> Bool
isDataType Val
tv
isDataType Val
_ = Bool
False

-- * ugly printing -----------------------------------------------------

instance Show (Sort Val) where
  show :: Sort Val -> String
show (SortC Class
c) = Class -> String
forall a. Show a => a -> String
show Class
c
  show (Set Val
VZero) = String
"Set"
  show (CoSet Val
VInfty) = String
"Set"
  show (Set Val
v) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (String
"Set " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v)
  show (CoSet Val
v) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (String
"CoSet " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v)

instance Show Val where
  show :: Val -> String
show Val
v | Val -> Bool
isVSize Val
v = String
"Size"
  show (VSort Sort Val
s) = Sort Val -> String
forall a. Show a => a -> String
show Sort Val
s
  show Val
VInfty = String
"#"
  show Val
VZero = String
"0"
  show (VSucc Val
v) = String
"($ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (VMax [Val]
vl) = String
"(max " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Val] -> String
showVals [Val]
vl String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (VPlus (Val
v:[Val]
vl)) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (Val -> ShowS) -> String -> [Val] -> String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Val
v String
s -> Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) (Val -> String
forall a. Show a => a -> String
show Val
v) [Val]
vl
  show (VApp Val
v []) = Val -> String
forall a. Show a => a -> String
show Val
v
  show (VApp Val
v [Val]
vl) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Val] -> String
showVals [Val]
vl String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (VDef DefId
id) = DefId -> String
forall a. Show a => a -> String
show DefId
id
  show (VProj PrePost
Pre Name
id) = Name -> String
forall a. Show a => a -> String
show Name
id
  show (VProj PrePost
Post Name
id) = String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
id
  show (VPair Val
v1 Val
v2) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (VGen Int
k) = String
"v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
  show (VMeta Int
k Env
rho Int
0) = String
"?" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
showEnv Env
rho
  show (VMeta Int
k Env
rho Int
1) = String
"$?" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
showEnv Env
rho
  show (VMeta Int
k Env
rho Int
n) = String
"(?" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
showEnv Env
rho String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
  show (VRecord RecInfo
ri EnvMap
env) = RecInfo -> String
forall a. Show a => a -> String
show RecInfo
ri String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ((Name, Val) -> String) -> EnvMap -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
"; " (\ (Name
n, Val
v) -> Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v) EnvMap
env String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (VCase Val
v Val
vt Env
env [Clause]
cs) = String
"case " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
vt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" { " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Clause] -> String
showCases [Clause]
cs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" } " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
showEnv Env
env
  show (VClos (Environ [] Maybe (Measure Val)
Nothing) Expr
e) = Int -> Expr -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
precAppR Expr
e String
""
  show (VClos Env
env Expr
e) = String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
showEnv Env
env String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (VSing Val
v Val
vt) = String
"<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
vt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
  show Val
VIrr  = String
"."
  show (VMeasured Measure Val
mu Val
tv) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Measure Val -> String
forall a. Show a => a -> String
show Measure Val
mu String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
tv
  show (VGuard Bound Val
beta Val
tv) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bound Val -> String
forall a. Show a => a -> String
show Bound Val
beta String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
tv
  show (VBelow LtLe
ltle Val
v) = LtLe -> String
forall a. Show a => a -> String
show LtLe
ltle String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v

  show (VQuant PiSigma
pisig Name
x (Domain (VBelow LtLe
ltle Val
v) Kind
_ki Dec
dec) Val
bv)
       | (LtLe
ltle,Val
v) (LtLe, Val) -> (LtLe, Val) -> Bool
forall a. Eq a => a -> a -> Bool
/= (LtLe
Le,Val
VInfty) =
       ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (\ Pol
p -> if Pol
pPol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
==Pol
defaultPol then String
"" else Pol -> String
forall a. Show a => a -> String
show Pol
p) (Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                (if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then ShowS
brackets String
binding else ShowS
parens String
binding)
                 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PiSigma -> String
forall a. Show a => a -> String
show PiSigma
pisig String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
showSkipLambda Val
bv
            where binding :: String
binding = Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LtLe -> String
forall a. Show a => a -> String
show LtLe
ltle String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v

  show (VQuant PiSigma
pisig Name
x (Domain Val
av Kind
ki Dec
dec) Val
bv) =
        ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (\ Pol
p -> if Pol
pPol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
==Pol
defaultPol then String
"" else Pol -> String
forall a. Show a => a -> String
show Pol
p) (Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                (if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then ShowS
brackets String
binding
                  else if Name -> Bool
emptyName Name
x then String
s1 else ShowS
parens String
binding)
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PiSigma -> String
forall a. Show a => a -> String
show PiSigma
pisig String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
showSkipLambda Val
bv
             where s1 :: String
s1 = String
s2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s0
                   s2 :: String
s2 = Val -> String
forall a. Show a => a -> String
show Val
av
                   s3 :: String
s3 = Kind -> String
forall a. Show a => a -> String
show Kind
ki
                   s0 :: String
s0 = if Kind
ki Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
defaultKind Bool -> Bool -> Bool
|| String
s2 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s3 then String
"" else String
"::" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s3
                   binding :: String
binding = if Name -> Bool
emptyName Name
x then  String
s1 else Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s1

  show (VLam Name
x Env
env Expr
e) = String
"(\\" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
showEnv Env
env String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (VConst Val
v) = String
"(\\ _ -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (VAbs Name
x Int
i Val
v Valuation
valu) = String
"(\\" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ Valuation -> String
showValuation Valuation
valu String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (VUp Val
v Val
vt) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" Up " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
vt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

showSkipLambda :: Val -> String
showSkipLambda :: Val -> String
showSkipLambda = \case
    (VLam Name
_x Env
env Expr
e)     -> Expr -> String
forall a. Show a => a -> String
show Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
showEnv Env
env
    (VConst Val
v)          -> Val -> String
forall a. Show a => a -> String
show Val
v
    (VAbs Name
_x Int
_i Val
v Valuation
valu) -> Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ Valuation -> String
showValuation Valuation
valu
    Val
v                   -> Val -> String
forall a. Show a => a -> String
show Val
v

showVals :: [Val] -> String
showVals :: [Val] -> String
showVals [] = String
""
showVals (Val
v:[Val]
vl) = Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if [Val] -> Bool
forall a. Null a => a -> Bool
null [Val]
vl then String
"" else String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Val] -> String
showVals [Val]
vl)

-- environment ---------------------------------------------------

emptyEnv :: Environ a
emptyEnv :: forall a. Environ a
emptyEnv = [(Name, a)] -> Maybe (Measure Val) -> Environ a
forall a. [(Name, a)] -> Maybe (Measure Val) -> Environ a
Environ [] Maybe (Measure Val)
forall a. Maybe a
Nothing

appendEnv :: Environ a -> Environ a -> Environ a
appendEnv :: forall a. Environ a -> Environ a -> Environ a
appendEnv (Environ [(Name, a)]
rho Maybe (Measure Val)
mmeas) (Environ [(Name, a)]
rho' Maybe (Measure Val)
mmeas') =
  [(Name, a)] -> Maybe (Measure Val) -> Environ a
forall a. [(Name, a)] -> Maybe (Measure Val) -> Environ a
Environ ([(Name, a)]
rho [(Name, a)] -> [(Name, a)] -> [(Name, a)]
forall a. [a] -> [a] -> [a]
++ [(Name, a)]
rho') (Maybe (Measure Val) -> Maybe (Measure Val) -> Maybe (Measure Val)
forall e (m :: * -> *) a. MonadError e m => m a -> m a -> m a
orM Maybe (Measure Val)
mmeas Maybe (Measure Val)
mmeas')

-- | enviroment extension / update
update :: Environ a -> Name -> a -> Environ a
update :: forall a. Environ a -> Name -> a -> Environ a
update Environ a
env Name
n a
v | Name -> Bool
emptyName Name
n = Environ a
env
               | Bool
otherwise   = Environ a
env { envMap = (n,v) : envMap env }

lookupPure :: Show a => Environ a -> Name -> a
lookupPure :: forall a. Show a => Environ a -> Name -> a
lookupPure Environ a
rho Name
x =
    case Name -> [(Name, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (Environ a -> [(Name, a)]
forall a. Environ a -> [(Name, a)]
envMap Environ a
rho) of
      Just a
v -> a
v
      Maybe a
Nothing -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"lookupPure: unbound identifier " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in environment " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Environ a -> String
forall a. Show a => a -> String
show Environ a
rho

lookupEnv :: MonadError TraceError m => Environ a -> Name -> m a
lookupEnv :: forall (m :: * -> *) a.
MonadError TraceError m =>
Environ a -> Name -> m a
lookupEnv Environ a
rho Name
x =
    case Name -> [(Name, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (Environ a -> [(Name, a)]
forall a. Environ a -> [(Name, a)]
envMap Environ a
rho) of
      Just a
v -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ a
v
      Maybe a
Nothing -> String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"lookupEnv: unbound identifier " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x --  ++ " in environment " ++ show rho

showValuation :: Valuation -> String
showValuation :: Valuation -> String
showValuation (Valuation [])  = String
""
showValuation (Valuation [(Int, Val)]
tau) = String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ((Int, Val) -> String) -> [(Int, Val)] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
", " (\(Int
i,Val
v) -> Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v) [(Int, Val)]
tau String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"

showEnv :: Environ Val -> String
showEnv :: Env -> String
showEnv (Environ [] Maybe (Measure Val)
Nothing)   = String
""
showEnv (Environ EnvMap
rho Maybe (Measure Val)
Nothing)  = String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvMap -> String
showEnv' EnvMap
rho String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
showEnv (Environ [] (Just Measure Val
mu)) = String
"{ measure=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Measure Val -> String
forall a. Show a => a -> String
show Measure Val
mu String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" }"
showEnv (Environ EnvMap
rho (Just Measure Val
mu)) = String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvMap -> String
showEnv' EnvMap
rho String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" | measure=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Measure Val -> String
forall a. Show a => a -> String
show Measure Val
mu String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" }"

showEnv' :: EnvMap -> String
showEnv' :: EnvMap -> String
showEnv' = String -> ((Name, Val) -> String) -> EnvMap -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
", " (\ (Name
n,Val
v) -> Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v)