-- ** Well-formedness predicates
nWellFormedUniq, nWellFormedOC,
-- ** Inquiries
- nAllNotEmpty, nSomeNotEmpty, nGround, nUpUniq,
+ nAllNotEmpty, nSomeNotEmpty, nGround,
-- ** Construction
nHide, nShallow, nDeep,
-- ** Destruction
nExpose,
-- ** Internals
nPrune,
+ -- ** Rewrites
+ nUpUniq,
-- * Binary comparators
nCmp, nEq, nLeq, nSub,
-- * Total binary functions
(eml n0 (lift . go) (visit q) m a >> return True)
-- | Is a named inst ground?
+--
+-- Note that 'ground' here means 'ground' like the thesis means ground
+-- (see def 3.2.17, p52), which includes everything from UUnique to
+-- UClobbered. This may not be what you mean.
nGround :: forall f . NIX f -> Bool
nGround n0@(NIX i0 m) = evalState (iGround_ q i0) S.empty
where
q a = tsc id a $ eml n0 (return . nGround) (iGround_ q) m a
- {-
- q (Left a) = return $ nGround a
- q (Right a) = tsc id a $ ml n0 m a >>= iGround_ q
- -}
-- | Is there some term not ruled out by this inst?
--
-- | Is an instantiation ground?
--
--- Surrogate for definition 3.2.17, p52
+-- Surrogate for definition 3.2.17, p52.
+--
+-- Note that 'ground' terms include UClobbered terms; this may not be what
+-- you meant.
iGround_ :: (Monad m) => (i -> m Bool) -> InstF f i -> m Bool
-iGround_ q (IBound UUnique b _) = mfmamm q b
+iGround_ q (IBound _ b _) = mfmamm q b
iGround_ _ (IUniv _) = return True
iGround_ _ _ = return False
{-# INLINABLE iGround_ #-}
-- (\i -> property $ i1 `nSub` i && i2 `nSub` i)
-- $ nSubLUB i1 i2
+-- | Check that nGround and (`nLeq` $ nHide $ IUniv UUnique) are the same
+-- function. The former is defined inductively and is therefore probably
+-- faster.
+prop_nGround_nLeq_IUniv :: NIX TestFunct -> QCP.Property
+prop_nGround_nLeq_IUniv i1 = nGround i1 QCP.==> (i1 `nLeq` niu)
+
+prop_nLeq_IUniv_nGround :: NIX TestFunct -> QCP.Property
+prop_nLeq_IUniv_nGround i1 = (i1 `nLeq` niu) QCP.==> nGround i1
+
+niu = nHide (IUniv UUnique)
+
-- | When we enact a call, the rules (figure 3.13, p45; see also 'doCall')
-- tell us that we first check that the incoming variables are all ⊑ the
-- input half of the mode, then unify the input variables with the output
miaod ar = QMode (replicate ar nnIn) nnOut
-- | One-Place INVersion
-opinvd ar d = fmap (\x -> QMode x nnIn d) (go [] ar)
- where
- go _ 0 = []
- go sfx n = (replicate n nnOut ++ sfx) : go (nnIn:sfx) (n-1)
+opinvd ar d = map (\x -> QMode x nnIn d)
+ $ map (\n -> (replicate (n-1) nnIn)
+ ++ nnOut
+ : (replicate (ar-n) nnIn))
+ [1..ar]
------------------------------------------------------------------------}}}
nuniv = nHide (IUniv UShared)
isGround, isFree :: ModedVar -> Bool
-isGround v = nGround (v^.mv_mi)
-isFree v = nSub (v^.mv_mi) nfree
+-- | Note that isGround here is not quite the same as 'nGround': we do not
+-- accept clobbered parameters.
+isGround v = (v^.mv_mi) `nSub` nuniv
+isFree v = (v^.mv_mi) `nSub` nfree
builtins :: BackendPossible PyDopeBS
builtins (f,is,o) = case () of
pslice :: [ModedVar] -> Doc e
pslice vs = brackets $
- sepBy "," (map (\x -> if nGround (x^.mv_mi) then pretty (x^.mv_var) else ":") vs)
+ sepBy "," (map (\x -> if isGround x then pretty (x^.mv_var) else ":") vs)
<> "," -- add a comma to ensure getitem is always passed a tuple.
ground2underscore :: ModedVar -> Doc e
-ground2underscore x = if nGround (x^.mv_mi) then "_" else pretty (x^.mv_var)
+ground2underscore x = if isGround x then "_" else pretty (x^.mv_var)
piterate :: [ModedVar] -> Doc e
piterate vs = if length vs == 0 then "_"