Copyright | (c) Harm Brouwer and Noortje Venhuizen |
---|---|
License | Apache-2.0 |
Maintainer | me@hbrouwer.eu, n.j.venhuizen@rug.nl |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell98 |
PDRS binding
Synopsis
- pdrsBoundPRef :: PRef -> PDRS -> PDRS -> Bool
- pdrsPRefBoundByPRef :: PRef -> PDRS -> PRef -> PDRS -> Bool
- pdrsPBoundPRef :: PRef -> PDRS -> PDRS -> Bool
- pdrsIsFreePVar :: PVar -> PDRS -> Bool
- pdrsBoundPVar :: PVar -> PDRS -> PDRS -> Bool
- pdrsFreePRefs :: PDRS -> PDRS -> [PRef]
- pdrsFreePVars :: PDRS -> PDRS -> [PVar]
Exported
pdrsPRefBoundByPRef :: PRef -> PDRS -> PRef -> PDRS -> Bool #
Returns whether PRef pr1
introduced in local PDRS lp
is bound by
projected referent pr2
in PDRS pdrs
, where:
boundByPRef pr1 lp1 pr2 pdrs
iff
pr1
andpr2
share the same referent; andpr2
is part of some universe inpdrs
(i.e., can bind referents); and- The interpretation site of
pr2
is accessible from both the introduction and interpretation site ofpr1
.
pdrsPBoundPRef :: PRef -> PDRS -> PDRS -> Bool #
Returns whether a referent is bound by some other referent than itself.
pdrsIsFreePVar :: PVar -> PDRS -> Bool #
Returns whether pv
is a free projection variable in PDRS p
, where:
pdrsIsFreePVar pv p
iff
- context
pv
is accessible from the global context, or - there is no context
v
that is accessible frompv
and also from the global context.
pdrsBoundPVar :: PVar -> PDRS -> PDRS -> Bool #
Returns whether a pointer p
in local PDRS lp
is bound by a
label in the global PDRS gp
, where:
pdrsBoundPVar p lp gp
iff
p
is equal to the label of eitherlp
orgp
; or- there exists a PDRS
p
with labelpv
, such thatp
is a subPDRS ofgp
andp
is accessible fromlp
.
Note the correspondence to drsBoundRef.