From: Nathaniel Wesley Filardo Date: Tue, 18 Jun 2013 06:10:25 +0000 (-0400) Subject: Small mode-system changes X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=9158ff0623da026be464ff6b2ecbba666b3a4cae;p=dyna2 Small mode-system changes Mostly cosmetic Fixes a small potential bug (as of yet un-tickled) in Python planner hook Imports a fix to NoBackend planner hook from 4e0fc1726ab4abf1326ea61ae5225f0bb5167707 --- diff --git a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs index 41d246f..caec2d1 100644 --- a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs +++ b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs @@ -23,13 +23,15 @@ module Dyna.Analysis.Mode.Execution.NamedInst ( -- ** 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 @@ -201,14 +203,14 @@ nWellFormedOC n0 = evalStateT (go n0) H.empty (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? -- diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs index f28ed8b..b00cc44 100644 --- a/src/Dyna/Analysis/Mode/Inst.hs +++ b/src/Dyna/Analysis/Mode/Inst.hs @@ -224,9 +224,12 @@ iIsNotReached _ = False -- | 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_ #-} diff --git a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs index 44afcbf..300d32a 100644 --- a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs +++ b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs @@ -147,6 +147,17 @@ prop_nSubGLB_is_G i1 i2 i3 = nWFU i1 && nWFU i2 && nWFU i3 -- (\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 diff --git a/src/Dyna/Backend/NoBackend.hs b/src/Dyna/Backend/NoBackend.hs index 5c8f2a5..7a1e81f 100644 --- a/src/Dyna/Backend/NoBackend.hs +++ b/src/Dyna/Backend/NoBackend.hs @@ -130,9 +130,10 @@ nnOut = (nfree, nuniv) 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] ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Backend/Python/Backend.hs b/src/Dyna/Backend/Python/Backend.hs index 19e82ca..6c7139c 100644 --- a/src/Dyna/Backend/Python/Backend.hs +++ b/src/Dyna/Backend/Python/Backend.hs @@ -72,8 +72,10 @@ nfree = nHide IFree 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 @@ -200,11 +202,11 @@ tupledOrUnderscore vs = parens ((sepBy "," $ map pretty vs) <> ",") 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 "_"