]> hydra-www.ietfng.org Git - dyna2/commitdiff
Small mode-system changes
authorNathaniel Wesley Filardo <nwf@cs.jhu.edu>
Tue, 18 Jun 2013 06:10:25 +0000 (02:10 -0400)
committerNathaniel Wesley Filardo <nwf@cs.jhu.edu>
Tue, 18 Jun 2013 06:10:25 +0000 (02:10 -0400)
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

src/Dyna/Analysis/Mode/Execution/NamedInst.hs
src/Dyna/Analysis/Mode/Inst.hs
src/Dyna/Analysis/Mode/Selftest/NamedInst.hs
src/Dyna/Backend/NoBackend.hs
src/Dyna/Backend/Python/Backend.hs

index 41d246f02a955cf38d0f4d829f684a9334a81573..caec2d1d8580508dbcb213be702375fd8b04ad11 100644 (file)
@@ -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?
 --
index f28ed8ba37ba7deb36aa2abc43457f1f0ee569cd..b00cc44dc358e249b5b2f252050c614dba793c99 100644 (file)
@@ -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_ #-}
index 44afcbf79e7404b72d0207fa44c5b418a51094b6..300d32adbdf866584fe26405d213bb73146b3b1a 100644 (file)
@@ -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
index 5c8f2a5690e19c29944acae800aa7be69512467f..7a1e81f9188f66475aac98324005b9a49d424c67 100644 (file)
@@ -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]
 
 ------------------------------------------------------------------------}}}
index 19e82caf4ff28dfe9e7c5bf198020e855696b48d..6c7139cab400cae82684948453bd307f5aef3937 100644 (file)
@@ -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 "_"