From 85edb5149bf5e8aa486337678ad5f7bfe4bc8a1d Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Fri, 3 May 2013 19:43:07 -0400 Subject: [PATCH] First pass at new mode infrastructure plumbing This brings the Mercury mode system all the way out through the planner, though it does not actually really avail itself of any of the improved functionality. It compiles and passes all selftests, but that, too, is hardly saying anything. --- Makefile | 19 +- dyna.cabal | 13 +- examples/expected/papa2.py.out | 20 +- examples/expected/simple.py.out | 10 +- examples/papa2.dyna | 2 +- src/Dyna/Analysis/ANF.hs | 2 +- src/Dyna/Analysis/Aggregation.hs | 18 +- src/Dyna/Analysis/Base.hs | 147 ------- src/Dyna/Analysis/DOpAMine.hs | 133 ++++++ src/Dyna/Analysis/Mode.hs | 303 +------------ src/Dyna/Analysis/Mode/Execution/NamedInst.hs | 110 ++++- .../Analysis/Mode/Execution/NoAliasContext.hs | 190 +++++++++ .../Mode/Execution/NoAliasFunctions.hs | 401 ++++++++++++++++++ src/Dyna/Analysis/Mode/Inst.hs | 52 ++- src/Dyna/Analysis/Mode/Mode.hs | 27 ++ src/Dyna/Analysis/Mode/Selftest/NamedInst.hs | 39 +- src/Dyna/Analysis/Mode/Selftest/Term.hs | 31 ++ src/Dyna/Analysis/Mode/Unification.hs | 10 +- src/Dyna/Analysis/RuleMode.hs | 294 +++++++++---- src/Dyna/{Main => Backend}/BackendDefn.hs | 33 +- src/Dyna/Backend/Backends.hs | 47 ++ src/Dyna/Backend/NoBackend.hs | 128 ++++++ src/Dyna/Backend/Python.hs | 210 ++++----- src/Dyna/Backend/Python/Selftest.hs | 3 + src/Dyna/Main/Driver.hs | 119 +++--- src/Dyna/Main/Exception.hs | 10 + src/Dyna/Main/TestsDriver.hs | 17 +- src/Dyna/ParserHS/Parser.hs | 79 +++- src/Dyna/ParserHS/Selftest.hs | 11 + src/Dyna/Term/Normalized.hs | 39 ++ src/Dyna/XXX/DataUtils.hs | 6 +- src/Dyna/XXX/MonadContext.hs | 50 ++- vimrc | 3 + 33 files changed, 1738 insertions(+), 838 deletions(-) delete mode 100644 src/Dyna/Analysis/Base.hs create mode 100644 src/Dyna/Analysis/DOpAMine.hs create mode 100644 src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs create mode 100644 src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs create mode 100644 src/Dyna/Analysis/Mode/Mode.hs rename src/Dyna/{Main => Backend}/BackendDefn.hs (60%) create mode 100644 src/Dyna/Backend/Backends.hs create mode 100644 src/Dyna/Backend/NoBackend.hs create mode 100644 src/Dyna/Term/Normalized.hs create mode 100644 vimrc diff --git a/Makefile b/Makefile index 38e17e7..c77e9cf 100644 --- a/Makefile +++ b/Makefile @@ -33,7 +33,20 @@ ghcbuild: -o dist/build/dyna-selftests/dyna-selftests \ -outputdir dist/build/dyna-selftests/dyna-selftests-tmp \ -main-is Dyna.Main.TestsDriver Dyna.Main.TestsDriver - + +# Every now and again we need to make a profiling build of some component +# of the tree. Se MAINMOD and MAINFILE and make this target. +profbuild: + mkdir -p dist/pb + ghc --make -isrc \ + -o dist/pb/a.out \ + -outputdir dist/pb \ + -main-is $(MAINMOD) $(MAINFILE) + ghc --make -isrc -osuf p.o -prof -fprof-auto \ + -o dist/pb/a.out \ + -outputdir dist/pb \ + -main-is $(MAINMOD) $(MAINFILE) + tests: dist/build/dyna-selftests/dyna-selftests @@ -45,5 +58,9 @@ clean: rm -rf examples/*.dyna.plan \ examples/*.dyna.*.out \ examples/*.dyna.d + rm -f tags TAGS veryclean: clean rm -rf dist + +tags TAGS: + hasktags -b src diff --git a/dyna.cabal b/dyna.cabal index ed8f9ad..bc5a4c8 100644 --- a/dyna.cabal +++ b/dyna.cabal @@ -29,9 +29,8 @@ Library Exposed-Modules: Dyna.Analysis.ANF, - Dyna.Analysis.Base, Dyna.Analysis.Mode, - Dyna.Main.BackendDefn, + Dyna.Backend.BackendDefn, Dyna.Main.Driver, Dyna.Main.Exception, Dyna.ParserHS.Parser, @@ -42,6 +41,8 @@ Library bytestring >=0.9, charset >=0.3, containers >=0.4, + either >= 3.4, + ghc-prim, HUnit >=1.2, mtl >=2.1, lens >=3.8, @@ -71,6 +72,7 @@ Library -- bytestring >=0.9, -- charset >=0.3, -- containers >=0.4, +-- either >= 3.4, -- haskeline >=0.6, -- mtl >=2.1, -- lens >=3.8, @@ -101,7 +103,9 @@ Executable dyna bytestring >=0.9, charset >=0.3, containers >=0.4, + either >= 3.4, haskeline >=0.6, + ghc-prim, HUnit >=1.2, mtl >=2.1, lens >=3.8, @@ -134,6 +138,8 @@ Test-suite dyna-selftests bytestring >=0.9, charset >=0.3, containers >=0.4, + either >= 3.4, + ghc-prim, HUnit >=1.2, mtl >=2.1, lens >=3.8, @@ -155,6 +161,7 @@ Test-suite dyna-selftests trifecta >= 1.0, unordered-containers>=0.2, utf8-string >=0.3, - wl-pprint-extras >=3.0 + wl-pprint-extras >=3.0, + wl-pprint-terminfo >=3.0 Main-Is: Dyna/Main/TestsDriver.hs diff --git a/examples/expected/papa2.py.out b/examples/expected/papa2.py.out index ddc5332..424292a 100644 --- a/examples/expected/papa2.py.out +++ b/examples/expected/papa2.py.out @@ -84,18 +84,14 @@ t/3 ================= -true/0 -================= - - word/2 ================= -word('.',7) := true -word('Papa',0) := true -word('a',5) := true -word('ate',1) := true -word('caviar',3) := true -word('spoon',6) := true -word('the',2) := true -word('with',4) := true +word('.',7) := True +word('Papa',0) := True +word('a',5) := True +word('ate',1) := True +word('caviar',3) := True +word('spoon',6) := True +word('the',2) := True +word('with',4) := True diff --git a/examples/expected/simple.py.out b/examples/expected/simple.py.out index 0b80033..b8b99a9 100644 --- a/examples/expected/simple.py.out +++ b/examples/expected/simple.py.out @@ -3,17 +3,13 @@ Charts ============ a/0 ================= -a := true +a := True b/0 ================= -b := true +b := True c/0 ================= -c := true - -true/0 -================= - +c := True diff --git a/examples/papa2.dyna b/examples/papa2.dyna index 790583f..ba13f92 100644 --- a/examples/papa2.dyna +++ b/examples/papa2.dyna @@ -6,7 +6,7 @@ phrase(X,I,K,t(X,TY,TZ)) max= phrase(Y,I,J,TY) * phrase(Z,J,K,TZ) * rewrite(X,Y, goal(P) max= phrase("S", 0, *length, P). -best max= pair(*phrase("S", 0, *length, P), P). +best max= pair(phrase("S", 0, *length, P), P). bestScore max= pair(Score,_) is best, Score. bestParse max= pair(_,P) is best, P. diff --git a/src/Dyna/Analysis/ANF.hs b/src/Dyna/Analysis/ANF.hs index 30b1e8f..490fb39 100644 --- a/src/Dyna/Analysis/ANF.hs +++ b/src/Dyna/Analysis/ANF.hs @@ -87,8 +87,8 @@ import qualified Data.Char as C import qualified Data.Map as M -- import qualified Debug.Trace as XT import qualified Dyna.ParserHS.Parser as P -import Dyna.Analysis.Base import Dyna.Term.TTerm +import Dyna.Term.Normalized import Dyna.Term.SurfaceSyntax import Dyna.XXX.DataUtils (mapInOrApp) import Dyna.XXX.PPrint (valign) diff --git a/src/Dyna/Analysis/Aggregation.hs b/src/Dyna/Analysis/Aggregation.hs index 2cb2a0a..3c92691 100644 --- a/src/Dyna/Analysis/Aggregation.hs +++ b/src/Dyna/Analysis/Aggregation.hs @@ -17,6 +17,7 @@ import Dyna.Analysis.ANF import Dyna.Main.Exception import Dyna.Term.TTerm import Dyna.XXX.DataUtils +import Dyna.XXX.Trifecta import Text.PrettyPrint.Free ------------------------------------------------------------------------}}} @@ -27,15 +28,10 @@ type AggMap = M.Map DFunctAr DAgg ------------------------------------------------------------------------}}} -- Associate each item with an aggregator {{{ --- XXX These functions should be rewritten to use Dyna.Main.Exception - --- XXX These functions really would like to have span information, so they --- could report which line of the source caused an error. - procANF :: Rule -> (DFunctAr, DAgg) -procANF r@(Rule _ h a _ _ (AS { as_assgn = as })) = +procANF r@(Rule _ h a _ sp (AS { as_assgn = as })) = case M.lookup h as of - Nothing -> dynacSorry $ "I can't process head-variables" <+> (pretty $ show r) + Nothing -> dynacSorry $ "I can't process head-variables in rule at" <+> (prettySpanLoc sp) Just t -> case t of Left _ -> dynacPanic $ "Malformed head" <+> (pretty $ show r) Right (f,xs) -> ((f,length xs),a) @@ -44,12 +40,12 @@ buildAggMap :: [Rule] -> AggMap buildAggMap = go (M.empty) where go m [] = m - go m (ar:xs) = + go m (ar@(Rule _ _ a _ sp _):xs) = let (d,a) = procANF ar in case mapUpsert d a m of - Left a' -> dynacUserErr $ "Conflicting aggregators in rule" - <+> (pretty $ show ar) - <+> "Expected" + Left a' -> dynacUserErr $ "Conflicting aggregators; rule" + <+> prettySpanLoc sp <+> "uses" <+> (pretty a) + <+> "but I had been lead to expect" <+> pretty a' Right m' -> go m' xs diff --git a/src/Dyna/Analysis/Base.hs b/src/Dyna/Analysis/Base.hs deleted file mode 100644 index e708a6b..0000000 --- a/src/Dyna/Analysis/Base.hs +++ /dev/null @@ -1,147 +0,0 @@ ---------------------------------------------------------------------------- --- | Common, basic definitions of our Analysis modules --- --- Much of this is pending rework once we get to the mode system of Mercury. - -module Dyna.Analysis.Base ( - -- * Normalized Term Representations - NT(..), FDT, NTV, EBF, ENF, EVF, - - -- * Modes - Mode(..), Moded(..), modeOf, isBound, isFree, - ModedVar, varOfMV, ModedNT, evnOfMNT, ntvOfMNT, - - -- * DOpAMine - DOpAMine(..), - - -- * Determinism - Det(..), detOfDop, -) where - --- import qualified Data.ByteString as B -import Dyna.Term.TTerm -import qualified Text.PrettyPrint.Free as PP - -------------------------------------------------------------------------}}} --- Normalized Term Representations {{{ - --- | A Normalized Term, parametric in the variable case -data NT v = NTVar v - | NTBase TBase - deriving (Eq,Ord,Show) - -instance PP.Pretty v => PP.Pretty (NT v) where - pretty (NTVar v) = PP.pretty v - pretty (NTBase t) = PP.pretty t - --- | Normalized Term over 'DVar' (that is, either a primitive or a variable) -type NTV = NT DVar - --- | Flat Dyna Term (that is, a functor over variables) -type FDT = (DFunct,[DVar]) - --- | Either a base case or flat term -type EBF = Either TBase FDT - --- | Either a variable or a functor of variables) -type EVF = Either DVar FDT - --- | Either a constant, another variable, or a flat Dyna term -type ENF = Either NTV FDT - -------------------------------------------------------------------------}}} --- Modes {{{ - -data Mode = MBound | MFree deriving (Eq,Ord,Show) - - -data Moded v = MF DVar - | MB v - deriving (Eq,Ord,Show) - -modeOf :: Moded a -> Mode -modeOf (MF _) = MFree -modeOf (MB _) = MBound - -isBound, isFree :: Moded a -> Bool -isBound = (== MBound) . modeOf -isFree = (== MFree ) . modeOf - -type ModedVar = Moded DVar - -varOfMV :: ModedVar -> DVar -varOfMV (MF x) = x -varOfMV (MB x) = x - -type ModedNT = NT (ModedVar) - -evnOfMNT :: ModedNT -> Either DVar NTV -evnOfMNT (NTVar mv) = case mv of - MB v -> Right (NTVar v) - MF v -> Left v -evnOfMNT (NTBase b) = Right (NTBase b) - -ntvOfMNT :: ModedNT -> NTV -ntvOfMNT (NTVar mx) = NTVar $ varOfMV mx -ntvOfMNT (NTBase b) = NTBase b - -------------------------------------------------------------------------}}} --- DOpAMine {{{ - --- | Dyna OPerational Abstract MachINE --- --- It makes us happy. - --- Opcode Out In Ancillary -data DOpAMine fbs - = OPAsgn DVar NTV -- -+ - | OPCheq DVar DVar -- ++ - - -- | Check that two dvars are not equal. This is used to - -- prevent double-counting of hyper-edges when any of their - -- tails can be made to be the same item by specialization. - -- - -- XXX While inspired by (Eisner, Goldlust, and Smith 2005), - -- it's unclear that this is actually what we should be doing. - -- Oh well, live and learn. - | OPCkne DVar DVar -- ++ - - -- | Check that the input dvar is an interned representation - -- of the given functor (and arity as computed from the list - -- length) and if so, unpack its arguments into those dvars. - | OPPeel [DVar] DVar DFunct -- -+ - - -- | The reverse of OPPeel - | OPWrap DVar [DVar] DFunct -- -+ - - -- | Perform a query - | OPIter (ModedVar) [ModedVar] DFunct -- ?? - Det - (Maybe fbs) - - -- | Perform an arbitrary evaluation query. Semantically, - -- - -- @OPWrap x ys f ; OPIndr z x@ is indistinguishable from - -- @OPIter (MF z) (map MB ys) f DetSemi Nothing@. - | OPIndr DVar DVar -- -+ - deriving (Eq,Ord,Show) - -------------------------------------------------------------------------}}} --- Determinism {{{ - -data Det = Det -- ^ Exactly one answer - | DetSemi -- ^ At most one answer - | DetNon -- ^ Unknown number of answers - deriving (Eq,Ord,Show) - -detOfDop :: DOpAMine fbs -> Det -detOfDop x = case x of - OPAsgn _ _ -> Det - OPCheq _ _ -> DetSemi - OPCkne _ _ -> DetSemi - OPPeel _ _ _ -> DetSemi - OPWrap _ _ _ -> Det - OPIndr _ _ -> DetSemi - OPIter _ _ _ d _ -> d - -------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/DOpAMine.hs b/src/Dyna/Analysis/DOpAMine.hs new file mode 100644 index 0000000..31e018a --- /dev/null +++ b/src/Dyna/Analysis/DOpAMine.hs @@ -0,0 +1,133 @@ +--------------------------------------------------------------------------- +-- | Definition and utility functions for the Dyna OPerational Abstract +-- MachINE. + +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE Rank2Types #-} + +module Dyna.Analysis.DOpAMine where + +import Control.Lens +import Dyna.Analysis.Mode.Det +import Dyna.Analysis.Mode.Execution.NamedInst +import Dyna.Term.Normalized +import Dyna.Term.TTerm +import Text.PrettyPrint.Free + +------------------------------------------------------------------------}}} +-- DOpAMine {{{ + +data ModedVar = MV + { _mv_var :: DVar + , _mv_mi :: NIX DFunct + , _mv_mo :: NIX DFunct + } + deriving (Show) +$(makeLenses ''ModedVar) + +-- | Dyna OPerational Abstract MachINE +-- +-- It makes us happy. +-- +-- The 'bscg' parameter is used to hold on to the backend-specific code +-- generator data in 'OPIter' calls. + +-- Opcode Out In Ancillary +data DOpAMine bscg + = OPAsgn DVar NTV -- -+ + | OPCheq DVar DVar -- ++ + + -- | Check that two dvars are not equal. This is used to + -- prevent double-counting of hyper-edges when any of their + -- tails can be made to be the same item by specialization. + -- + -- XXX While inspired by (Eisner, Goldlust, and Smith 2005), + -- it's unclear that this is actually what we should be doing. + -- Oh well, live and learn. + | OPCkne DVar DVar -- ++ + + -- | Check that the input dvar is an interned representation + -- of the given functor (and arity as computed from the list + -- length) and if so, unpack its arguments into those dvars. + | OPPeel [DVar] DVar DFunct -- -+ + + -- | The reverse of OPPeel + | OPWrap DVar [DVar] DFunct -- -+ + + -- | Perform a query + | OPIter ModedVar [ModedVar] DFunct -- ?? + Det + (Maybe bscg) + + -- | Perform an arbitrary evaluation query. Semantically, + -- + -- @OPWrap x ys f ; OPIndr z x@ is indistinguishable from + -- @OPIter (MF z) (map MB ys) f DetSemi Nothing@. + | OPIndr DVar DVar -- -+ + deriving (Show) + +{- XXX Move DOpAMine to being more functional, rather than a list of + - opcodes? + - + - OPBlock [DOpAMine bscg] + - OPOrElse [DOpAMine bscg] -- choice points! + -} + +{- XXX New DOpAMine opcodes for unification support. + - + - OPMkFree DVar + - + - OPCase DVar [(DFunct, [DVar] -> [DOpAMine bscg])] + - OPCase2 DVar DVar [(DFunct, [DVar] -> [DVar] -> [DOpAMine bscg])] + - + - OPMkAnyFree DVar + - OPWrapAny ... + - OPCaseA DVar (DVar -> [DOpAMine bscg]) + - ((DFunct,[DVar]) -> [DOpAMine bscg]) + - + - OPRec ... ? + -} + +------------------------------------------------------------------------}}} +-- Determinism {{{ + +detOfDop :: DOpAMine fbs -> Det +detOfDop x = case x of + OPAsgn _ _ -> Det + OPCheq _ _ -> DetSemi + OPCkne _ _ -> DetSemi + OPPeel _ _ _ -> DetSemi + OPWrap _ _ _ -> Det + OPIndr _ _ -> DetSemi + OPIter _ _ _ d _ -> d + +------------------------------------------------------------------------}}} +-- Rendering {{{ + +instance Pretty ModedVar where + pretty x = pretty (x^.mv_var) + <> char '@' + <> parens ((pretty $ x^.mv_mi) <> text ">>" <> (pretty $ x^.mv_mo)) + +type BackendRenderDopIter bs e = + ModedVar -> [ModedVar] -> DFunct -> Det -> bs -> Doc e + +-- | Given a mechanism for rendering backend-specific information, +-- pretty-print a 'DOpAMine' opcode. +renderDOpAMine :: BackendRenderDopIter bs e -> DOpAMine bs -> Doc e +renderDOpAMine _ (OPAsgn v n) = text "OPAsgn" <+> pretty v <+> pretty n +renderDOpAMine _ (OPCheq a b) = text "OPCheq" <+> pretty a <+> pretty b +renderDOpAMine _ (OPCkne a b) = text "OPCkne" <+> pretty a <+> pretty b +renderDOpAMine _ (OPIndr a b) = text "OPIndr" <+> pretty a <+> pretty b +renderDOpAMine _ (OPPeel vs v f) = text "OPPeel" <+> pretty vs + <+> pretty v <+> pretty f +renderDOpAMine _ (OPWrap v vs f) = text "OPWrap" <+> pretty v + <+> pretty vs <+> pretty f +renderDOpAMine e (OPIter v vs f d b) = text "OPIter" + <+> pretty v + <+> list (map pretty vs) + <+> squotes (pretty f) + <+> text (show d) + <> maybe empty ((space <>) . braces . e v vs f d) b + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode.hs b/src/Dyna/Analysis/Mode.hs index b87e724..a9bab23 100644 --- a/src/Dyna/Analysis/Mode.hs +++ b/src/Dyna/Analysis/Mode.hs @@ -14,9 +14,6 @@ -- primarily by running computable algorithms over the regular trees of the -- thesis. --- XXX This file is, at this point, mostly detritus from development and --- will be cleaned up real soon now. - -- Header material {{{ {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} @@ -31,304 +28,24 @@ {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wall #-} module Dyna.Analysis.Mode( - - iuWellFormed, iuCompare, iuLeq, iuSub, - -- * Instantiation Key Maps - -- InstKeyMap(..), InstKeyVal(..), - -- * Instantiation contexts - -- IMLookup(..), IMAssign(..), - -- * Modes - -- Mode(..), -- mWellFormed, - module Dyna.Analysis.Mode.Det, module Dyna.Analysis.Mode.Uniq, module Dyna.Analysis.Mode.Inst, + module Dyna.Analysis.Mode.Unification, + module Dyna.Analysis.Mode.Mode, + + module Dyna.Analysis.Mode.Execution.NamedInst + -- module Dyna.Analysis.Mode.InstMap, - module Dyna.Analysis.Mode.Execution.Base, - module Dyna.Analysis.Mode.Execution.Functions, + -- module Dyna.Analysis.Mode.Execution.Base, + -- module Dyna.Analysis.Mode.Execution.Functions, ) where -import Control.Applicative -import Control.Exception(assert) -import Control.Lens -import Control.Monad -import Control.Monad.State -import Control.Monad.Trans.Maybe -import qualified Data.Foldable as F -import qualified Data.Map as M -import qualified Data.Set as S -import qualified Data.Traversable as T -import Dyna.Analysis.Mode.Execution.Base -import Dyna.Analysis.Mode.Execution.Functions import Dyna.Analysis.Mode.Det +import Dyna.Analysis.Mode.Execution.NamedInst import Dyna.Analysis.Mode.Inst --- import Dyna.Analysis.Mode.InstMap +import Dyna.Analysis.Mode.Mode +import Dyna.Analysis.Mode.Unification import Dyna.Analysis.Mode.Uniq -import Dyna.XXX.DataUtils -import Dyna.XXX.MonadContext -import Dyna.XXX.MonadUtils - -------------------------------------------------------------------------}}} --- Instantiation contexts {{{ - -{- -class (Monad m, Ord v) => IMLookup m f v | m -> f v where - vlookup :: v -> m (InstF f v) - -class (Monad m, Ord v, IMLookup m f v) => IMAssign m f v where - vassign :: v -> InstF f v -> m () --} - -{- --- | Very often we need to recurse through the variable context and stop as --- soon as we loop. (Since variables may well be knot-tied to support --- mu-recursive types, for example.) --- --- The folder is applicative -ctxRecurse :: (Ord v, Ord a, IMLookup m f v) - => (a -> InstF f v -> Either [(v,a)] r) -- ^ Single step - -> (r -> m r -> m r) -- ^ Folder - -> r -- ^ Zero answer - -> r -- ^ Cycle answer - -> a -> InstF f v -> m r -ctxRecurse step fold zr cr = go S.empty - where - go stk a i = case step a i of - Left is -> foldM (fold_ stk) zr is - Right r -> return r - - fold_ stk r (v,a) = if S.member (v,a) stk - then fold r (return cr) - else fold r $ do - i <- vlookup v - go (S.insert (v,a) stk) a i --} - -------------------------------------------------------------------------}}} --- Instantiation operations {{{ - - -iuWellFormed :: forall f i m v . - (MCVT m i ~ (InstF f i), MCR m i, Ord i, - MCVT m v ~ (Either i (InstF f (Either v i))), MCR m v, Ord v) - => Uniq -> v -> m Bool -iuWellFormed u0 v0 = evalStateT (q u0 v0) S.empty - where - qe u (Left v) = q u v - qe u (Right i) = lift $ nWellFormed u i - - q :: Uniq -> v -> StateT (S.Set v) m Bool - q u vu = do - looped <- gets $ S.member vu - if looped - then return False - else do - modify $ S.insert vu - i <- lift $ clookup vu - case i of - Left vi -> lift $ nWellFormed u vi - Right i' -> iWellFormed_ qe u i' - - -iuCompare :: forall eiv f i ir m tm v . - (MCVT m i ~ InstF f i, MCR m i, Ord i, Ord f, - MCVT m v ~ Either i ir, MCR m v, Ord v, - tm ~ StateT (S.Set (eiv,ir), S.Set (eiv,eiv)) m, - ir ~ InstF f eiv, - eiv ~ Either i v) - => ( forall m' . (Monad m') - => (eiv -> ir -> m' Bool) - -> (eiv -> eiv -> m' Bool) - -> ir -> ir -> m' Bool) - -> v -> v -> m Bool -iuCompare cmp i0 j0 = evalStateT (qb (Right i0) (Right j0)) (S.empty, S.empty) - where - rq = cmp qa qb - - ll :: eiv -> tm ir - ll = either (liftM (fmap Left) . lift . clookup) lq - where - lq x = do - x' <- lift $ clookup x - either (liftM (fmap Left) . lift . clookup) return x' - - qa (v :: eiv) j = do - already <- gets $ S.member (v,j) . fst - if already - then return True - else do - modify $ over _1 (S.insert (v,j)) - i <- ll v - rq i j - -- XXX? qb vi vj | vi == vj = return True - qb (vi :: eiv) (vj :: eiv) = do - already <- gets $ S.member (vi,vj) . snd - if already - then return True - else do - modify $ over _2 (S.insert (vi,vj)) - i <- ll vi - j <- ll vj - rq i j - -iuLeq, iuSub :: forall f i v m . - (Ord i, Ord f, Ord v, Monad m, - MCVT m i ~ InstF f i, MCR m i, - MCVT m v ~ Either i (InstF f (Either i v)), MCR m v) - => v -> v -> m Bool -iuLeq = iuCompare iLeq_ -iuSub = iuCompare iSub_ - - - -------------------------------------------------------------------------}}} --- Instantiation Maps {{{ - -{- -chkial m = goV S.empty S.empty - where - goV vis stk v = case M.lookup v m of - Just i -> go vis stk i - Nothing -> Left v - - goI vis stk (IAlias v) = - case () of - _ | v `S.member` stk -> Left v -- ERR: cycle - _ | v `S.member` vis -> Right vis -- OK: already cleared - _ -> goV (S.insert v vis) (S.insert v stk) -- WORK: chase cycle - goI vis _ _ = Right vis -- OK: Productive step - --- | Test the well-formedness of an 'InstMap' and return a witness variable --- that is problematic, if any. -imWellFormed :: InstMap f v -> Maybe v -imWellFormed IMNotReached = Nothing -imWellFormed (IM m) = foldr checker S.empty (M.keys m) - - -go S.empty S.empty (M.keys m) - where - go _ _ [] = Nothing - go vis as (v:vs) = - if v `S.elem` vis - then go vis S.empty vs -- Been here and it's OK - else case M.lookup v m of - Nothing -> Just v -- Whoop, that's bad. - Just i -> check vs vis as i --} - -{- -refineIM_ v i i' m s = - case i `iLeqGLB_` i' of - Nothing -> IMNotReached (M.delete v m) (S.insert v s) - -- XXX Just (INotReached _) -> IMNotReached (M.delete v m) (S.insert v s) - Just iglb -> IM (M.insert v iglb m) - -refineIM :: (Ord v, Eq f) => v -> InstF f i -> InstMap f v i -> InstMap f v i -refineIM v i (IM m) = - let i0 = maybe IFree id $ M.lookup v m in - assert (i `iLeq_` i0) $ refineIM_ v i i0 m S.empty -refineIM v _ im@(IMNotReached _ s) | v `S.member` s = im -refineIM v i (IMNotReached m s) = - let i0 = maybe IFree id $ M.lookup v m in - assert (i `iLeq_` i0) $ refineIM_ v i i0 m s --} - - -{- -instance (Monad m, Ord v) => IMLookup (StateT (InstMap f v v) m) f v where - vlookup v = get >>= return . imLookup v --} - - -------------------------------------------------------------------------}}} --- Instantiation Key Maps {{{ - -{- --- | An instantiation key map is the representation of the prolog abstract --- machine's binding patterns. That is, it maps every prolog variable @u@ --- to another variable or an Inst, which in turn recurses to contain either --- prolog variables or defined (possibly recursive) -newtype InstKeyMap f u v = IKM { unIKM :: M.Map u (InstKeyVal f u v) } - -data InstKeyVal f u v = IKVUser u - | IKVName v - | IKVInst (InstF f (Either u v)) - -class (Monad m, Ord u) => IKMLookup m f u v | m -> f u v where - ulookup :: u -> m (InstKeyVal f u v) - -class (Monad m, Ord u, IKMLookup m f u v) => IKMAssign m f u v where - uassign :: u -> InstKeyVal f u v -> m () - -ikmSemiprune :: (Ord u, MonadState (InstKeyMap f u v) m) => u -> m u -ikmSemiprune u = do - m <- gets unIKM - let (u', m') = mapSemiprune q IKVUser u m - put (IKM m') - return u' - where q (IKVUser u') = Just u' - q _ = Nothing - -instance (Monad m, Ord u) => IKMLookup (StateT (InstKeyMap f u v) m) f u v where - ulookup u = do - u' <- ikmSemiprune u - m' <- get - case M.lookup u' (unIKM m') of - Just (IKVUser u'') | u' == u'' -> do - put $ IKM $ M.insert u' (IKVInst IFree) (unIKM m') - return (IKVUser u') - Just (IKVUser _) -> error "ikmSemiprune bug" - Just i -> return i - Nothing -> error "ulookup XXX" -- XXX - -{- -instance (Monad m, Ord u) => IKMAssign (StateT (InstKeyMap f u v) m) f u v where - uassign u ikv = modify (IKM . M.insert u ikv . unIKM) --} - -{- -abstract_unify :: InstKeyMap f u v -> u -> u -> Maybe (InstKeyMap f u v) -abstract_unify ikm u1 u2 = - u1' <- ikmSemiprune u1 ikm - u2' <- ikmSemiprune u2 ikm - abstract_unify_core ikm'' u1' u2' - -abstract_unify_core :: InstKeyMap f u v -> InstKeyVal f u v -> InstKeyVal f u v -> Maybe (InstKeyMap f u v) -abstract_unify_core = undefined --} - --} - -------------------------------------------------------------------------}}} --- Abstract Interpretation {{{ - - - - -------------------------------------------------------------------------}}} --- Mode {{{ - --- XXX While this type works fine for the thesis, for us it's a little bit --- of bad news: we need to have both of these maps in scope as we go about --- reasoning. That means we're going to need to freshen these into our --- current global store and do operations there. It may not be so bad, but --- this also kind of sucks. --- --- It's also another argument in favor of some later attempt to have the --- scope maps canonicalize themselves as we go. - --- | Mode --- --- Definition 3.1.10, p34 --- data Mode f v i = Mode { m_ini :: InstMap f v i --- , m_fin :: InstMap f v i} -{- --- | Well-formedness condition on modes. Definition 3.1.10, p35 -mWellFormedV :: (MCR m v (InstF f v), Ord f, Ord v) => Mode f v v -> m Bool -mWellFormedV (Mode {m_init = mi, m_fin = mf}) = - let kmi = imKeys mi - in andM1 (kmi == (imKeys mf)) $ - setForallM (\v -> imLookup v mf `iLeq` imLookup v mi) kmi --} ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs index d10b5dc..f2819c4 100644 --- a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs +++ b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs @@ -21,17 +21,19 @@ module Dyna.Analysis.Mode.Execution.NamedInst ( -- * Well-formedness predicates nWellFormedUniq, nWellFormedOC, -- * Unary functions - nGround, nUpUniq, nPrune, nExpose, nHide, + nNotEmpty, nGround, nUpUniq, nPrune, nExpose, nHide, -- * Binary comparators nCmp, nEq, nLeq, nSub, -- * Total binary functions nTBin, nLeqGLB, nSubGLB, -- * Partial binary functions nPBin, nLeqGLBRD, nLeqGLBRL, -- nSubLUB, + -- * Mode functions + mWellFormed, ) where import Control.Applicative --- import qualified Control.Arrow as A +import qualified Control.Arrow as A import Control.Lens import Control.Monad.State import Control.Monad.Trans.Either @@ -40,16 +42,16 @@ import qualified Data.HashSet as H import qualified Data.Map as M import qualified Data.Set as S import qualified Data.Traversable as T +-- import qualified Debug.Trace as XT import Dyna.Analysis.Mode.Inst +import Dyna.Analysis.Mode.Mode import Dyna.Analysis.Mode.Unification import Dyna.Analysis.Mode.Uniq import Dyna.Main.Exception import Dyna.XXX.MonadUtils - --- import qualified Debug.Trace as XT - import System.IO.Unsafe (unsafePerformIO) import System.Mem.StableName (makeStableName) +import Text.PrettyPrint.Free ------------------------------------------------------------------------}}} -- Datatype definition {{{ @@ -84,6 +86,37 @@ data NIX f = forall a . (Ord a,Show a) => instance (Show f) => Show (NIX f) where show (NIX r m) = "(NIX ("++ (show r) ++ ") (" ++ (show m) ++ "))" +instance (Pretty f) => Pretty (NIX f) where + pretty (NIX r m) = ri r <> if M.null m + then empty + else align $ indent 2 + ( (text "where") + <+> (vsep $ map rme $ M.toList m)) + where + -- render index + rix = angles . text . show + + -- render map entry + rme (k,v) = rix k <+> equals <+> either pretty ri v + + -- render uniq (XXX own pretty instance instead?) + ru u = text $ case u of + UUnique -> "un" + UMostlyUnique -> "mu" + UShared -> "sh" + UMostlyClobbered -> "mc" + UClobbered -> "cl" + + -- render inst + ri IFree = text "$f" + ri (IAny u) = text "$a@" <> ru u + ri (IUniv u) = text "$u@" <> ru u + ri (IBound u bm b) = ru u + <> (semiBraces $ if b then (text "$b"):rm else rm) + where + rm = map (\(k,vs) -> pretty k <> tupled (map rix vs)) (M.toList bm) + + ------------------------------------------------------------------------}}} -- Utilities {{{ @@ -169,6 +202,7 @@ nWellFormedOC = go H.empty q v a = tsc id a (eml n0 (return . go v) (visit (q v)) m a >> return True) +-- | Is a named inst ground? nGround :: forall f . NIX f -> Bool nGround n0@(NIX i0 m) = evalState (iGround_ q i0) S.empty where @@ -178,8 +212,23 @@ nGround n0@(NIX i0 m) = evalState (iGround_ q i0) S.empty q (Right a) = tsc id a $ ml n0 m a >>= iGround_ q -} --- | Prune the internals of a 'NIX'. This really ought not be needed, but --- it's handy for test generation. +-- | Is there some term not ruled out by this inst? +-- +-- This is mostly useful for the test harness, not actual reasoning, at +-- the moment, since we are not sufficiently precise (i.e. we will miss some +-- empty unification results). +nNotEmpty :: forall f . NIX f -> Bool +nNotEmpty n0@(NIX i0 m0) = evalState (visit i0) S.empty + where + visit IFree = return True + visit (IUniv _) = return True + visit (IAny _) = return True + visit (IBound _ m b) = b `orM1` (anyM $ M.foldr (\fas a -> allM (map rec fas) : a) [] m) + + rec idx = do + already <- gets (S.member idx) + already `orM1` eml n0 (return . nNotEmpty) + (\v -> modify (S.insert idx) >> visit v) m0 idx nCrawl :: forall f . (Ord f) => (forall a . Uniq -> InstF f a) -- ^ Replace free variables @@ -207,30 +256,33 @@ nCrawl fv u0 n0@(NIX i0 m) = F.traverse_ (evac (maybe u (max u) $ iUniq x)) x return () - +-- | Prune the internals of a 'NIX'. This really ought not be needed, but +-- it's handy for test generation. nPrune :: forall f . (Ord f) => NIX f -> NIX f nPrune = nCrawl (const IFree) UUnique -nUpUniq :: forall f . (Ord f) => Uniq -> NIX f -> NIX f -nUpUniq = nCrawl (const IFree) -{- -- | Increase the nonuniqueness of a particular named inst to at least the -- given level. -nUpUniq :: forall f . Uniq -> NIX f -> NIX f +nUpUniq :: forall f . (Ord f) => Uniq -> NIX f -> NIX f + +-- XXX a simplistic, cruft-removing, but inefficient solution. +-- nUpUniq = nCrawl (const IFree) + +{- + - XXX The beginnings of a possibly more efficient implementation +nUpUniq u0 n0@(NIX i0 m) = uncurry NIX $ runState (T.traverse visit i0) m + where + visit a = eml n0 (return . nUpUniq u0) + (T.traverse visit (over inst_uniq (max u0))) +-} nUpUniq u0 n0@(NIX i0 m0) = maybe n0 (\u' -> if u' >= u0 then n0 else NIX i0' m0') (iUniq i0) where reuniq = over inst_uniq (max u0) -{- - reuniq (IFree ) = IFree - reuniq i@(IUniv u' ) = if u' >= u0 then i else IUniv u0 - reuniq i@(IAny u' ) = if u' >= u0 then i else IAny u0 - reuniq i@(IBound u' im ib) = if u' >= u0 then i else IBound u0 im ib --} m0' = M.map (nUpUniq u0 A.+++ reuniq) m0 i0' = reuniq i0 --} +{-# INLINABLE nUpUniq #-} -- | Expose the root ply of a 'NIX' as an Inst which recurses as additional -- 'NIX' elements. @@ -388,6 +440,7 @@ nTBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (tlq li0 ri0) iNBS nbs_ctx %= M.insert k v return k +-- | Total lattice functions nLeqGLB, nSubGLB :: forall f . (Ord f, Show f) => NIX f -> NIX f -> NIX f nLeqGLB = nTBin iLeqGLB_ nSubGLB = nTBin (\_ _ fl fr fm _ -> iSubGLB_ (fl UUnique) (fr UUnique) (fm UUnique)) @@ -488,6 +541,8 @@ nPBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (runEitherT (tlq li0 ri0)) i nbs_ctx %= M.insert k v return k +-- | Partial lattice functions. These raise unification failures if +-- the runtime would fail. nLeqGLBRD, nLeqGLBRL :: forall f . (Ord f, Show f) => NIX f -> NIX f -> Either UnifFail (NIX f) nLeqGLBRD = nPBin iLeqGLBRD_ nLeqGLBRL = nPBin iLeqGLBRL_ @@ -505,3 +560,20 @@ nSubLUB = nPBin (\il ir ll lr m -> iSubLUB_ il ir (ll UClobbered) (lr UClobbered -} ------------------------------------------------------------------------}}} +-- Mode functions {{{ + +-- | Check that all names in a mode are indeed well-formed and that all +-- transitions are according to ≼. +-- +-- This lives in Execution.NamedInst because it requires that we be using +-- named insts within the 'QMode'. +-- +-- See prose, p35. +mWellFormed :: forall f . (Ord f, Show f) => QMode (NIX f) -> Bool +mWellFormed (QMode ats vm@(vti,vto) _) = + (all (nWellFormedUniq UUnique) + $ vti:vto:concatMap (\(i,o) -> [i,o]) ats) + && + (all (uncurry (flip nLeq)) $ vm:ats) + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs b/src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs new file mode 100644 index 0000000..a45e67c --- /dev/null +++ b/src/Dyna/Analysis/Mode/Execution/NoAliasContext.hs @@ -0,0 +1,190 @@ +--------------------------------------------------------------------------- +-- | Basics of actually running the mode system reasoner +-- +-- +-- This is a simplistic context which demonstrates how to perform +-- unification with all the bells and whistles of §3 but without the alias +-- tracking of §5. It will eventually be disconnected from the main source +-- tree (but may still be built as part of the test harness) but will +-- probably linger on as a way to attain understanding. + + +-- Header material {{{ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -Wall #-} + +module Dyna.Analysis.Mode.Execution.NoAliasContext ( + -- * Inst Types + -- ** Naming Conventions + -- $naming + + -- ** Variables + VR(..), vrToNIX, + + -- ** Monad + SIMCT(..), runSIMCT, + -- *** And its context + SIMCtx(..), emptySIMCtx, +)where + +-- import Control.Exception(assert) +import Control.Lens +-- import Control.Monad +import Control.Monad.Error.Class +import Control.Monad.State +import Control.Monad.Trans.Either +import qualified Control.Monad.Trans.State as CMTS +import qualified Control.Monad.Trans.Reader as CMTR +-- import Data.Function +import qualified Data.Map as M +-- import qualified Data.Traversable as T +-- import Data.Unique +import Dyna.Analysis.Mode.Execution.NamedInst +import Dyna.Analysis.Mode.Inst +import Dyna.Analysis.Mode.Unification +-- import Dyna.Main.Exception +import Dyna.Term.TTerm +-- import Dyna.XXX.DataUtils +import Dyna.XXX.MonadContext +-- import qualified Debug.Trace as XT +-- import qualified Text.PrettyPrint.Free as PP + +------------------------------------------------------------------------}}} +-- Variables {{{ + +-- | Variables (and unaliased structure) bindings +data VR f n = + -- | Defined named inst (unaliased) + VRName n + -- | Unaliased structure + | VRStruct (InstF f (VR f n)) + deriving (Eq,Ord,Show) + +-- XXX Boy this is bad +vrToNIX :: VR f (NIX f) -> NIX f +vrToNIX (VRName n) = n +vrToNIX (VRStruct i) = nHide $ fmap vrToNIX i + +------------------------------------------------------------------------}}} +-- Context {{{ +-- Context : Basics {{{ + +-- | Simplistic InstMap Context +data SIMCtx f = SIMCtx { _simctx_map_v :: M.Map DVar (VR f (NIX f)) + } + deriving (Show) +$(makeLenses ''SIMCtx) + +newtype SIMCT m f a = SIMCT { unSIMCT :: StateT (SIMCtx f) (EitherT UnifFail m) a } + deriving (Monad,MonadFix) + +instance (Monad m) => MonadError UnifFail (SIMCT m f) where + throwError e = SIMCT (lift (left e)) + catchError a f = SIMCT (CMTS.liftCatch catchError (unSIMCT a) (unSIMCT . f)) + +instance MonadIO m => MonadIO (SIMCT m f) where + liftIO m = SIMCT $ lift (liftIO m) + +{- + - XXX maybe + +instance (Monad m) => MonadState (SIMCtx f) (SIMCT m f) where + get = SIMCT get + put = SIMCT . get + state = SIMCT . state +-} + +emptySIMCtx :: SIMCtx f +emptySIMCtx = SIMCtx M.empty + +runSIMCT :: SIMCT m f a -> SIMCtx f -> m (Either UnifFail (a, SIMCtx f)) +runSIMCT q x = runEitherT (runStateT (unSIMCT q) x) + +------------------------------------------------------------------------}}} +-- Context : User Variables {{{ + +user_lookup :: (MonadState (SIMCtx f) m, Show f) + => DVar + -> m (VR f (NIX f)) +user_lookup v = do + m <- use simctx_map_v + r <- maybe (error $ "User variable context miss: " ++ (show v)) + return + $ M.lookup v m + -- XT.traceShow ("VL",v,r) $ return () + return r + +type instance MCVT (SIMCT m f) DVar = VR f (NIX f) + +instance (Show f, Monad m) => MCR (SIMCT m f) DVar where + clookup = SIMCT . user_lookup + +instance (Show f, Monad m) => MCW (SIMCT m f) DVar where + cassign v w = SIMCT $ simctx_map_v %= M.insert v w + +-- | This instance is potentially unsafe (see definition 3.2.19, p53 and +-- following prose) as it does not check that there has been no aliasing. +instance (Show f, Monad m) => MCA (SIMCT m f) DVar where + ccanon x = return x + + calias f l r = SIMCT $ do + vl <- user_lookup l + vr <- user_lookup r + x <- unSIMCT $ f vl vr + simctx_map_v %= M.insert l x + simctx_map_v %= M.insert r x + return l + +------------------------------------------------------------------------}}} +-- Context : Transformers {{{ + +-- These instances are used internally to allow us to wrap our workers with +-- different utility parameters. + +type instance MCVT (CMTR.ReaderT r (SIMCT m f)) k = MCVT (SIMCT m f) k + +instance (MCA (SIMCT m f) k) => MCA (CMTR.ReaderT r (SIMCT m f)) k where + ccanon k = lift (ccanon k) + + calias f k1 k2 = CMTR.ask >>= \e -> + lift (calias (\a b -> CMTR.runReaderT (f a b) e) k1 k2) + +instance (MCR (SIMCT m f) k) => MCR (CMTR.ReaderT r (SIMCT m f)) k where + clookup k = lift (clookup k) + +instance (MCW (SIMCT m f) k) => MCW (CMTR.ReaderT r (SIMCT m f)) k where + cassign k v = lift (cassign k v) + +------------------------------------------------------------------------}}} +------------------------------------------------------------------------}}} +-- Haddock Sections {{{ +-- Notes on Naming Conventions {{{ + +-- $naming +-- NAMING CONVENTIONS +-- +-- We have a lot of types flying around, so let's get a shorthand for some +-- of them. Despite the proliferation, much of the implementation is +-- type-directed, so it's not so bad. +-- +-- * @N@ -- 'NIX' f +-- +-- * @I@ -- @'InstF' f ('NI' f)@ +-- +-- * @V@ -- 'VV' +-- +-- * @X@ -- 'VR' f 'NI' +-- +-- * @Y@ -- @InstF f (VR f 'NI')@ + +------------------------------------------------------------------------}}} +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs b/src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs new file mode 100644 index 0000000..1b34abd --- /dev/null +++ b/src/Dyna/Analysis/Mode/Execution/NoAliasFunctions.hs @@ -0,0 +1,401 @@ +--------------------------------------------------------------------------- +-- | Execution-oriented aspects of functions we might actually want to +-- call during mode analysis. +-- +-- The rules for all of these functions is that we should +-- +-- * Destruct user-structure, since that is guaranteed to be finite, +-- and eliminate InstF/InstF cases with the primitive calls. +-- +-- * When neither arm is user structure, we must find a way to call +-- the NamedInst functions. +-- +-- + +-- Header material {{{ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wall #-} + +module Dyna.Analysis.Mode.Execution.NoAliasFunctions ( + -- * Unification + UnifParams(..), unifyVV, unifyVF, unifyUnaliasedNV, + -- * Matching, + subVN, + -- * Modes + doCall, + -- * Misc + leqXX, +) where + +-- import Control.Applicative +-- import Control.Exception +import Control.Lens +import Control.Monad.Error.Class +import Control.Monad.Reader.Class +-- import Control.Monad.Writer.Class +import Control.Monad.State +import Control.Monad.Reader +-- import Control.Monad.Trans.Either +-- import Control.Monad.Trans.RWS +-- import Data.Functor.Identity +import qualified Data.Map as M +-- import qualified Data.Maybe as MA +-- import qualified Data.Set as S +-- import qualified Data.Traversable as T +import Dyna.Analysis.Mode.Execution.NoAliasContext +import Dyna.Analysis.Mode.Execution.NamedInst +import Dyna.Analysis.Mode.Inst +import Dyna.Analysis.Mode.Mode +import Dyna.Analysis.Mode.Unification +import Dyna.Analysis.Mode.Uniq +import Dyna.Main.Exception +import Dyna.Term.TTerm +import Dyna.XXX.DataUtils +import Dyna.XXX.MonadContext +-- import Dyna.XXX.MonadUtils +import qualified Debug.Trace as XT + +------------------------------------------------------------------------}}} +-- Leq {{{ + +type LeqC m f n = (Ord f, Show f, + Monad m, + n ~ NIX f) +leqXX :: (LeqC m f n) + => VR f n -> VR f n -> m Bool +leqXX (VRStruct yl) (VRStruct yr) = iLeq_ leqXY leqXX yl yr +leqXX (VRName nl) (VRStruct yr) = leqNY nl yr +leqXX (VRStruct yl) (VRName nr) = leqYN yl nr +leqXX (VRName nl) (VRName nr) = return $ nLeq nl nr + +leqXY :: (LeqC m f n) + => VR f n -> InstF f (VR f n) -> m Bool +leqXY (VRName nl) yr = iLeq_ leqNY leqNX (nExpose nl) yr +leqXY (VRStruct yl) yr = iLeq_ leqXY leqXX yl yr + +leqNX :: (LeqC m f n) + => NIX f -> VR f n -> m Bool +leqNX nl (VRName nr) = return $ nLeq nl nr +leqNX nl (VRStruct yr) = iLeq_ leqNY leqNX (nExpose nl) yr + +leqNY :: (LeqC m f n) + => NIX f -> InstF f (VR f n) -> m Bool +leqNY nl ir = iLeq_ leqNY leqNX (nExpose nl) ir + +leqYN :: (LeqC m f n) + => InstF f (VR f n) -> NIX f -> m Bool +leqYN il nr = iLeq_ leqXI leqXN il (nExpose nr) + +leqXI :: (LeqC m f n) + => VR f n -> InstF f (NIX f) -> m Bool +leqXI (VRStruct yl) ir = leqYN yl (nHide ir) +leqXI (VRName nl) ir = return $ nLeq nl (nHide ir) + +leqXN :: (LeqC m f n) + => VR f n -> NIX f -> m Bool +leqXN (VRName nl) nr = return $ nLeq nl nr +leqXN (VRStruct yl) nr = leqYN yl nr + +{- +leqDVar :: (LeqC m f n) + => DVar -> DVar -> m Bool +leqDVar vl vr = do + xl <- clookup vl + xr <- clookup vr + leqXX xl xr + +leqVX vl xr = do + xl <- clookup vl + leqXX xl xr +-} + +------------------------------------------------------------------------}}} +-- Unification {{{ + +data UnifParams = UnifParams + { _up_live :: Bool + -- ^ Are we engaged in a live unification? See §3.2.1, + -- p43 and definition 3.2.19, p53 + + , _up_fake :: Bool + -- ^ Absent from the thesis but present in the Mercury + -- implementation is the consideration of "fake" + -- unifications, which are used when refining the + -- outputs of method calls and must be allowed to + -- descend through (Mostly)'Clobbered' material. + -- + -- See @compiler/prog_data.m@'s @unify_is_real@ type. + } +$(makeLenses ''UnifParams) + +-- XXX Ought to have a MonadWriter to produce +-- the actual opcode sequence for unification! +-- the determinism information +-- +-- The former will require that we again modify the core unification logic +-- to not use T.sequence but that we provide a function of type +-- M.Map f [m a] -> m (M.map f [a]). + +-- | Constraints common to unification interface functions +type UnifC' m f n = (Ord f, Show f, + Monad m, + MonadError UnifFail m, + n ~ NIX f) + +-- | Constraints common to all unification functions +type UnifC m f n = (UnifC' m f n, + MonadReader UnifParams m) + + +-- | Name-on-Name unification, which computes a new name for the result. +-- We assume that the sources will be updated by the caller, if +-- applicable. +unifyNN :: UnifC m f n + => Uniq -> n -> n -> m n +unifyNN u a b = do + live <- view up_live + fake <- view up_fake + either throwError (return . nUpUniq u) $ + let f = if (live && not fake) then nLeqGLBRL else nLeqGLBRD + in f a b + +-- | Variable-on-variable unification. +-- +-- Based on definition 3.2.19, p53 +-- +-- Thesis errata: Definition 3.2.19 says that the SCU check occurs only at +-- the top level, but reading the Mercury implementation (see +-- @compiler/inst_util.m@'s @abstractly_unify_inst@) makes it clear that +-- this check occurs at every level of the structure. In particular, +-- @abstractly_unify_inst{,_2,_3}@ calls +-- @abstractly_unify_bound_inst_list{,_2}@, which folds +-- @abstractly_unify_inst_list@, which folds +-- @abstractly_unify_inst@. +-- +unifyVV :: forall f m n . + (UnifC m f n, + MCVT m DVar ~ VR f n, MCR m DVar, MCA m DVar) + => DVar -> DVar -> m DVar +unifyVV vl vr | vl == vr = return vl +unifyVV vl vr = do + live <- view up_live + calias (go live) vl vr + where + go l = if l then \a b -> unifyXX UUnique a b >>= checkAndReunif + else unifyXX UUnique + +checkAndReunif :: forall f m n . + (UnifC m f n) + => VR f n -> m (VR f n) +checkAndReunif x = do + err <- leqXX x (VRStruct $ IAny UUnique) + if err + then unifyXX UUnique x (VRStruct $ IAny UShared) + else throwError UFExDomain + +unifyXX :: (UnifC m f n) + => Uniq -> VR f n -> VR f n -> m (VR f n) +unifyXX u0 (VRName na) (VRName nb) = liftM VRName $ unifyNN u0 na nb +unifyXX u0 (VRName na) (VRStruct yb) = unifyIY u0 (nExpose na) yb +unifyXX u0 (VRStruct ya) (VRName nb) = unifyIY u0 (nExpose nb) ya +unifyXX u0 (VRStruct ya) (VRStruct yb) = unifyYY u0 ya yb + +-- | This is the closest direct analog of @abstractly_unify_inst@. The +-- other unify functions are all dedicated to type shifting to get back +-- to this one (or 'unifyNN'). +unifyYY :: (UnifC m f n) + => Uniq -> InstF f (VR f n) -> InstF f (VR f n) -> m (VR f n) +unifyYY u0 ya yb = do + live <- view up_live + fake <- view up_fake + let f = if (live && not fake) then iLeqGLBRL_ else iLeqGLBRD_ + either throwError (return . VRStruct) =<< f + (\u x -> return $ xUpUniq u x) + (\u x -> return $ xUpUniq u x) + (\u y x -> unifyXY u x y) + (\u y x -> unifyXY u x y) + unifyXX + u0 ya yb + +unifyXY :: (UnifC m f n) + => Uniq -> VR f n -> InstF f (VR f n) -> m (VR f n) +unifyXY u0 (VRStruct ya) yb = unifyYY u0 ya yb +unifyXY u0 (VRName nl) yr = unifyIY u0 (nExpose nl) yr + +unifyNX :: (UnifC m f n) + => Uniq -> n -> VR f n -> m (VR f n) +unifyNX u n (VRName n') = liftM VRName $ unifyNN u n n' +unifyNX u n (VRStruct y) = unifyIY u (nExpose n) y + +unifyIY :: (UnifC m f n) + => Uniq -> InstF f n -> InstF f (VR f n) -> m (VR f n) +unifyIY u0 ia yb = unifyYY u0 (fmap VRName ia) yb + +-- XXX Should stop earlier than it does +xUpUniq :: (Ord f, n ~ NIX f) => Uniq -> VR f n -> VR f n +xUpUniq u (VRName n) = VRName $ nUpUniq u n +xUpUniq u (VRStruct y) = VRStruct $ over inst_uniq (max u) + $ fmap (xUpUniq u) y + +-- | Name-on-Variable unification. This should not be called on names +-- looked up from the context, as that would omit important updates to the +-- context. Instead, only call this on ``freestanding'' named insts which +-- are known for other reasons, such as part of a predicate mode. +-- +-- This function returns the variable given as a convenient shorthand. +-- +-- Based on figure 5.7, p 104. +unifyUnaliasedNV :: forall f m n. + (UnifC m f n, + MCVT m DVar ~ VR f n, MCR m DVar, MCW m DVar) + => n + -> DVar + -> m DVar +unifyUnaliasedNV n0 v0 = do + live <- view up_live + x0 <- clookup v0 + xu <- (go live) n0 x0 + cassign v0 xu + return v0 + where + go l = if l then \a b -> unifyNX UUnique a b >>= checkAndReunif + else unifyNX UUnique + +-- | Variable-on-Functor unification. In our case, since we walk over ANF, +-- where every position has been given a name, we assume the outer functor +-- recurses through a set of variables. +-- +-- See definition 3.2.20, p53. +unifyVF :: forall m f n . + (UnifC' m f n + , MCVT m DVar ~ VR f n, MCR m DVar, MCW m DVar) + => (DVar -> m Bool) -> DVar -> f -> [DVar] -> m DVar +unifyVF lf v f vs = do + vl <- lf v + vi <- clookup v + vis <- mapM clookup vs + + let vvis = zip vs vis + + i'' <- runReaderT (unifyXY UUnique vi (IBound UUnique (M.singleton f vis) False)) + (UnifParams False True) + + -- Unification was successful; now, rip through the results and do the + -- second unification pass. + + (u,vis') <- case i'' of + VRName n'' -> case nExpose n'' of + IBound u (M.toList -> [(f',ris)]) False | f == f' -> do + x <- go unifyNX vl vvis u ris + return (u,x) + _ -> dynacPanicStr "unifyVF impossible NIX result" + VRStruct (IBound u (M.toList -> [(f',ris)]) False) | f == f' -> do + x <- go unifyXX vl vvis u ris + return (u,x) + _ -> dynacPanicStr "unifyVF impossible result" + + -- Store back into the context + + () <- sequence_ $ zipWith (cassign) vs vis' + cassign v (VRStruct $ IBound u (M.singleton f vis') False) + + return v + where + go :: forall a b m' . + (m' ~ ReaderT UnifParams m) + => (Uniq -> a -> b -> m' (VR f (NIX f))) + -> Bool -> [(DVar,b)] -> Uniq -> [a] -> m [VR f (NIX f)] + go uf vl vvis u ris = sequence $ zipWithTails + (\ri (v',oi) -> do + l <- lf v' + runReaderT (uf u ri oi >>= checkAndReunif) + (UnifParams (l && vl) True)) + (\_ -> dynacPanicStr "unifyVF length mismatch") + (\_ -> dynacPanicStr "unifyVF length mismatch") + ris vvis +------------------------------------------------------------------------}}} +-- Matching {{{ + +-- | Constraints common to all subsumption functions +type SubC m f n = (Ord f, Show f, + Monad m, + n ~ NIX f) + +subNN :: (SubC m f n) + => n -> n -> m Bool +subNN a b = XT.traceShow ("SNN",a,b) $ return $ nSub a b + +subXI :: (SubC m f n) + => VR f n -> InstF f (NIX f) -> m Bool +subXI (VRName ln) ri = subNN ln (nHide ri) +subXI (VRStruct ly) ri = subYI ly ri + +subYI :: (SubC m f n) + => InstF f (VR f n) -> InstF f (NIX f) -> m Bool +subYI l r = iSub_ subXI subXN l r + +subXN :: (SubC m f n) + => VR f n -> NIX f -> m Bool +subXN (VRName ln) rn = subNN ln rn +subXN (VRStruct ly) rn = subYI ly (nExpose rn) + +subVN :: forall f m n . + (SubC m f n, + MCVT m DVar ~ VR f n, MCR m DVar) + => DVar + -> n + -> m Bool +subVN v n = XT.traceShow ("SVN",v,n) $ do + vx <- clookup v + subXN vx n + +-- | Enact a particular call. +-- +-- Notice that if this fails the unification variables have been updated and +-- so should be discarded. +-- +-- XXX This doesn't do mode polymorphism, but it at least seems to be +-- vaguely right at the moment. +-- +-- XXX I am confused as to why this is "do all the subs then do all the +-- unifies" but that seems to be how the thesis rule is written unless I +-- misread. +-- +-- Based on Figure 5.7, p104 +doCall :: forall f m m' n . + (m ~ SIMCT m' f, Monad m', + SubC m f n, UnifC' m f n) + => (DVar -> Bool) -- Liveness predicate + -> DVar -> [DVar] -- Call with these arguments + -> QMode n -- Against this pattern + -> m Bool +doCall l r0 as0 (QMode cs0 (rmi,rmo) _) = go (r0:as0) (rmi:map fst cs0) + where + go [] [] = goUnify as0 (rmo:map snd cs0) + go (a:as) (c:cs) = do + sub <- subVN a c + if sub + then go as cs + else throwError UFExDomain + go _ _ = return False + + goUnify [] [] = return True + goUnify (a:as) (c:cs) = runReaderT (unifyUnaliasedNV c a) + (UnifParams (l a) True) + >> goUnify as cs + goUnify _ _ = return False + +------------------------------------------------------------------------}}} +-- Merging {{{ + +-- XXX Unimplemented + + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs index eb9658c..baf7998 100644 --- a/src/Dyna/Analysis/Mode/Inst.hs +++ b/src/Dyna/Analysis/Mode/Inst.hs @@ -14,7 +14,8 @@ -- Because I think it will be easier to understand in the long run, I have -- opted to avoid that -- the InstF functor contains only those constructors -- necessary for building plies of an actual inst. The other (co)products --- needed at runtime may be found in 'Dyna.Analysis.Mode.Execution.Base'. +-- needed at runtime may be found as parts of the +-- 'Dyna.Analysis.Mode.Execution' modules. -- Header material {{{ {-# LANGUAGE DeriveFoldable #-} @@ -92,7 +93,7 @@ data InstF f i = -- -- Note that we are saying nothing about the possible data -- bound by this variable; that would be the job of the type - -- system. + -- system. (XXX Maybe we should change that) | IAny { _inst_uniq :: !Uniq } -- | A bound inst. More specifically, a disjunction of @@ -204,6 +205,18 @@ iIsFree :: InstF f i -> Bool iIsFree IFree = True iIsFree _ = False +-- | The bottom of the 'iLeq' lattice and 'iSub' semi-lattice, representing +-- the empty set of (non-ground) terms. +iNotReached :: Uniq -> InstF f i +iNotReached u = IBound u M.empty False +{-# INLINABLE iNotReached #-} + +-- | Indicator function for 'iNotReached' +iIsNotReached :: InstF f i -> Bool +iIsNotReached (IBound _ m False) = M.null m +iIsNotReached _ = False +{-# INLINABLE iIsNotReached #-} + -- | Is an instantiation ground? -- -- Surrogate for definition 3.2.17, p52 @@ -213,6 +226,20 @@ iGround_ _ (IUniv _) = return True iGround_ _ _ = return False {-# INLINABLE iGround_ #-} +{- +data IPopEst = IPEEmpty | IPESingleton | IPEMany + deriving (Eq,Ord) + +-- | An over-estimate of the number of ground terms contained within this +-- non-ground term. iNotReached +iPopEst :: (Monad m) => (i -> m IPopEst) -> InstF f i -> m IPopEst +iPopEst _ IFree = return IPEMany +iPopEst _ (IAny _) = return IPEMany +iPopEst _ (IUniv _) = return IPEMany +iPopEst _ (IBool _ _ True) = return IPEMany +iPopEst q (IBool _ m False) = XXX +-} + ------------------------------------------------------------------------}}} -- Instantiation States: Binary predicates {{{ @@ -268,9 +295,9 @@ iLeq_ _ _ (IAny _) _ = return $ False iLeq_ _ _ (IUniv u) (IAny u') = return $ u' <= u iLeq_ _ _ (IUniv u) (IUniv u') = return $ u' <= u iLeq_ _ _ (IUniv _) _ = return $ False -iLeq_ q _ (IBound u b _) (IAny u') = andM1 (u' <= u) $ +iLeq_ q _ (IBound u b _) (IAny u') = andM1 (u' <= u) $ mfmamm (\x -> q x (IAny u')) b -iLeq_ q _ (IBound u b _) (IUniv u') = andM1 (u' <= u) $ +iLeq_ q _ (IBound u b _) (IUniv u') = andM1 (u' <= u) $ mfmamm (\x -> q x (IUniv u')) b iLeq_ _ q (IBound u m b) (IBound u' m' b') = andM1 (b <= b' && u' <= u) $ flip mapForallM m $ @@ -421,10 +448,10 @@ iSubGLB_ _ _ q (IBound u m b) (IBound u' m' b') = do -- NOTE: I was briefly concerned that we would have to pass u'' down -- through q, but since the well-formedness criteria may be assumed to -- hold for both m and m' (that is, for all insts contained in m (resp. - -- m'), their uniqueness is <= u (resp. u')), and our recursion is + -- m'), their uniqueness is >= u (resp. u')), and our recursion is -- defined by minimizing uniqueness, the uniqueness of the return is - -- guaranteed to be <= min {u, u'} with no additional effort on our - -- part. + -- guaranteed to be >= min {u, u'} with no additional effort on our + -- part. Contrast this with 'iLeqGLB_' and 'iSubLUB_' m'' <- mergeBoundLB q m m' return $ IBound u'' m'' (b && b') {-# INLINABLE iSubGLB_ #-} @@ -487,17 +514,6 @@ iSubLUB_ _ _ l r q (IBound u m b) (IBound u' m' b') = do ------------------------------------------------------------------------}}} -- Instantiation States: Utility Functions {{{ --- | The bottom of the 'iLeq' lattice and 'iSub' semi-lattice, representing --- the empty set of (non-ground) terms. -iNotReached :: Uniq -> InstF f i -iNotReached u = IBound u M.empty False -{-# INLINABLE iNotReached #-} - --- | Indicator function for 'iNotReached' -iIsNotReached :: InstF f i -> Bool -iIsNotReached (IBound _ m False) = M.null m -iIsNotReached _ = False -{-# INLINABLE iIsNotReached #-} crf :: (Monad m) => a -> m Bool crf = const $ return False diff --git a/src/Dyna/Analysis/Mode/Mode.hs b/src/Dyna/Analysis/Mode/Mode.hs new file mode 100644 index 0000000..aafc736 --- /dev/null +++ b/src/Dyna/Analysis/Mode/Mode.hs @@ -0,0 +1,27 @@ +--------------------------------------------------------------------------- +-- | Query (and update) modes. + +{-# LANGUAGE TemplateHaskell #-} + +module Dyna.Analysis.Mode.Mode where + +import Control.Lens.TH +import Dyna.Analysis.Mode.Det + +-- | A Query Mode is a collection of instantiation transducers. +-- +-- This is a surrogate for defn 3.1.10 (p34) which avoids the need to name +-- variables in a query. Many of the well-formedness conditions fall away, +-- but the subsumption test does not; see 'mWellFormed' +-- +-- XXX In the same way that 'InstF' will need generalization when we replace +-- our mode system, so will this. +data QMode n = QMode + { _qmode_args :: [(n,n)] + , _qmode_result :: (n,n) + , _qmode_det :: Det + } + deriving Show +$(makeLenses ''QMode) + +-- XXX Update Modes diff --git a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs index 73ab6fd..9318e3c 100644 --- a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs +++ b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs @@ -36,36 +36,10 @@ import Test.QuickCheck.Property import qualified Debug.Trace as XT +{- fromList :: Ord k => [(k,v)] -> M.Map k v fromList = M.fromList - --- | Generate an Arbitrary 'NIXM' Entry (i.e. either a closed NIX automata --- or -arbNIXME :: forall f i . (f ~ TestFunct) - => Gen i -> Gen (Either (NIX f) (InstF f i)) -arbNIXME igen = oneof [Left <$> sized (\s -> resize (s`div`2) arbitrary) - ,Right <$> arbInstPly igen] - -arbNIX = do - n <- sized (\s -> choose (1::Int,max 1 s)) -- How many plies? - let nl = [1..n] - let igen = choose (1::Int,n) -- Pick a ply - plies <- vectorOf n (arbNIXME igen) -- Generate plies or recurse - let m = M.fromList $ zip nl plies -- Make the map - root <- arbInstPly igen -- The root - return $ NIX root m - -instance Arbitrary (NIX TestFunct) where - arbitrary = nPrune <$> arbNIX - - shrink n@(NIX r m) = (MA.maybeToList noRecN) ++ subautomata - where - -- Replace all calls out to other automata with references to the root - noRecN = if null (E.lefts $ M.elems m) then Nothing else Just $ NIX r m' - where m' = M.map (either (const $ Right r) Right) m - - -- Pull out all the subautomata - subautomata = E.lefts (M.elems m) +-} nWFU = nWellFormedUniq UUnique @@ -156,6 +130,15 @@ prop_nSubGLB_is_G i1 i2 i3 = nWFU i1 && nWFU i2 && nWFU i3 -- (\i -> property $ i1 `nSub` i && i2 `nSub` i) -- $ nSubLUB i1 i2 +-- | 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 +-- half of the mode. We know that the output half is ≼ the input half. +prop_call_test_sufficient :: NIX TestFunct -> NIX TestFunct -> Property +prop_call_test_sufficient i1 i2 = nWFU i1 && nWFU i2 + && nNotEmpty i1 && nNotEmpty i2 + && nSub i1 i2 + ==> nNotEmpty (nLeqGLB i1 i2) selftest :: TF.Test selftest = moreTries 10000 $ moreTests 400 $(testGroupGenerator) diff --git a/src/Dyna/Analysis/Mode/Selftest/Term.hs b/src/Dyna/Analysis/Mode/Selftest/Term.hs index 954ead7..c78da85 100644 --- a/src/Dyna/Analysis/Mode/Selftest/Term.hs +++ b/src/Dyna/Analysis/Mode/Selftest/Term.hs @@ -1,15 +1,19 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} module Dyna.Analysis.Mode.Selftest.Term where import Control.Applicative import Control.Monad +import qualified Data.Either as E import qualified Data.List as L import qualified Data.Map as M +import qualified Data.Maybe as MA import Dyna.Analysis.Mode.Inst import Dyna.Analysis.Mode.Uniq +import Dyna.Analysis.Mode.Execution.NamedInst import Test.QuickCheck -- XXX orphan instance @@ -40,4 +44,31 @@ arbInstPly n = frequency [ (1,pure IFree) <*> arbitrary) ] +-- | Generate an Arbitrary 'NIXM' Entry (i.e. either a closed NIX automata +-- or a ply) +arbNIXME :: forall f i . (f ~ TestFunct) + => Gen i -> Gen (Either (NIX f) (InstF f i)) +arbNIXME igen = oneof [Left <$> sized (\s -> resize (s`div`2) arbitrary) + ,Right <$> arbInstPly igen] + +arbNIX = do + n <- sized (\s -> choose (1::Int,max 1 s)) -- How many plies? + let nl = [1..n] + let igen = choose (1::Int,n) -- Pick a ply + plies <- vectorOf n (arbNIXME igen) -- Generate plies or recurse + let m = M.fromList $ zip nl plies -- Make the map + root <- arbInstPly igen -- The root + return $ NIX root m + +instance Arbitrary (NIX TestFunct) where + arbitrary = nPrune <$> arbNIX + + shrink n@(NIX r m) = (MA.maybeToList noRecN) ++ subautomata + where + -- Replace all calls out to other automata with references to the root + noRecN = if null (E.lefts $ M.elems m) then Nothing else Just $ NIX r m' + where m' = M.map (either (const $ Right r) Right) m + + -- Pull out all the subautomata + subautomata = E.lefts (M.elems m) diff --git a/src/Dyna/Analysis/Mode/Unification.hs b/src/Dyna/Analysis/Mode/Unification.hs index 7ab6f01..f1c4866 100644 --- a/src/Dyna/Analysis/Mode/Unification.hs +++ b/src/Dyna/Analysis/Mode/Unification.hs @@ -19,20 +19,21 @@ data UnifFail = UFSemiClob -- ^ see 'semidet_clobbered_unify' | UFNotReach -- ^ Some nested unification satisfies 'iNotReached' | UFExDomain -- ^ A partial function was applied outside its domain + deriving (Eq,Ord,Show) ------------------------------------------------------------------------}}} -- Unification {{{ -- | This predicate is used to ensure that we reject any attempt at -- unification which could fail (i.e. is semidet, or, possibly better --- phrased, must traverse the structure of its argument) and may reference --- clobbered state. +-- phrased, must traverse the structure of its argument) and may attempt +-- to read clobbered state. -- -- In words, a unification can enter its arguments whenever -- 1. both inputs are not free variables (a free variable turns -- unification into assignment; two makes it aliasing) -- 2. either input represents more than one possible term - +-- -- The thesis will invoke this function (or rather, its negation) to allow a -- /dead/ unification (i.e., one in which one of the two variables is not -- live going forward) to succeed. Live unifications are probably (yes? @@ -54,6 +55,7 @@ semidet_clobbered_unify i i' = return $ && ( UMostlyClobbered <= MA.fromJust (iUniq i ) || UMostlyClobbered <= MA.fromJust (iUniq i')) -- The above fromJust calls are safe due to the 'iIsFree' guards. +{-# INLINABLE semidet_clobbered_unify #-} iLeqGLBRD_,iLeqGLBRL_ :: (Monad m, Ord f) @@ -71,10 +73,12 @@ iLeqGLBRD_ il ir ml mr m u i1 i2 = do return $ if iIsNotReached io then Left UFNotReach else Right io +{-# INLINABLE iLeqGLBRD_ #-} iLeqGLBRL_ il ir ml mr m u i1 i2 = do scu <- semidet_clobbered_unify i1 i2 if scu then return (Left UFSemiClob) else iLeqGLBRD_ il ir ml mr m u i1 i2 +{-# INLINABLE iLeqGLBRL_ #-} ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/RuleMode.hs b/src/Dyna/Analysis/RuleMode.hs index c5419f9..72aa29c 100644 --- a/src/Dyna/Analysis/RuleMode.hs +++ b/src/Dyna/Analysis/RuleMode.hs @@ -7,6 +7,7 @@ -- Header material {{{ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedStrings #-} @@ -14,7 +15,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} -module Dyna.Analysis.RuleMode ( +module Dyna.Analysis.RuleMode {- ( Mode(..), Moded(..), ModedNT, isBound, isFree, Crux, EvalCrux(..), UnifCrux(..), @@ -29,9 +30,15 @@ module Dyna.Analysis.RuleMode ( QueryEvalMap, combineQueryPlans, adornedQueries -) where - --- import Control.Monad +) -} where + +import Control.Lens ((^.)) +import Control.Monad +import Control.Monad.Error.Class +import Control.Monad.Trans.Either +import Control.Monad.Trans.Reader +import Control.Monad.Identity +import qualified Data.ByteString as B import qualified Data.ByteString.Char8 as BC -- import qualified Data.List as L import qualified Data.Map as M @@ -39,22 +46,34 @@ import qualified Data.Maybe as MA import qualified Data.Set as S -- import qualified Debug.Trace as XT import Dyna.Analysis.ANF -import Dyna.Analysis.Base +import Dyna.Analysis.DOpAMine +import Dyna.Analysis.Mode +import Dyna.Analysis.Mode.Execution.NoAliasContext +import Dyna.Analysis.Mode.Execution.NoAliasFunctions import Dyna.Term.TTerm +import Dyna.Term.Normalized import Dyna.Main.Exception import Dyna.XXX.DataUtils(argmin,mapInOrApp) +import Dyna.XXX.MonadContext import Dyna.XXX.Trifecta (prettySpanLoc) -- import Dyna.XXX.TrifectaTest import Text.PrettyPrint.Free +-- XXX Aaaaany second now +-- import Dyna.Analysis.Mode.Execution.Base +-- import Dyna.Analysis.Mode.Execution.Functions + ------------------------------------------------------------------------}}} -- Bindings {{{ --- | What things have thus far been bound under the plan? -type BindChart = S.Set DVar +-- | For variables that are bound, what are they, and all that? +type BindChart = SIMCtx DFunct -varMode :: BindChart -> DVar -> Mode -varMode c v = if v `S.member` c then MBound else MFree +type BindM m = EitherT UnifFail (SIMCT m DFunct) + +{- +varMode :: BindChart -> DVar -> DInst +varMode c v = maybe (error "BindChart miss") id $ M.lookup v c modedVar :: BindChart -> DVar -> ModedVar modedVar b x = case varMode b x of @@ -64,6 +83,7 @@ modedVar b x = case varMode b x of modedNT :: BindChart -> NTV -> ModedNT modedNT b (NTVar v) = NTVar $ modedVar b v modedNT _ (NTBase b) = NTBase b +-} ------------------------------------------------------------------------}}} -- Cruxes {{{ @@ -82,6 +102,7 @@ cruxIsEval :: Crux v n -> Bool cruxIsEval (Left _) = True cruxIsEval (Right _) = False +{- cruxMode :: BindChart -> Crux DVar NTV -> Crux (ModedVar) (ModedNT) cruxMode c cr = either (Left . evalMode) (Right . unifMode) cr where @@ -92,6 +113,7 @@ cruxMode c cr = either (Left . evalMode) (Right . unifMode) cr CFStruct o is f -> CFStruct (mv o) (map mv is) f CFAssign o i -> CFAssign (mv o) (modedNT c i) mv = modedVar c +-} cruxVars :: Crux DVar NTV -> S.Set DVar cruxVars = either evalVars unifVars @@ -107,8 +129,24 @@ cruxVars = either evalVars unifVars ------------------------------------------------------------------------}}} -- Actions {{{ -type Action fbs = [DOpAMine fbs] +type Actions fbs = [DOpAMine fbs] +data BackendAction fbs = BAct + { bact_dop :: Actions fbs + , bact_outmode :: [(DVar,NIX DFunct)] + } + deriving (Show) + + +-- | Builtin support hook for mode planning. Options are +-- to return +-- +-- * @Left False@ -- This functor is not built in +-- +-- * @Left True@ -- There is no plan for this mode +-- +-- * @Right act@ -- This operation may run according to the plan given. +-- -- XXX Is this really the right type? -- -- Note that there's a big wad of complexity here: we want to announce, for @@ -120,9 +158,7 @@ type Action fbs = [DOpAMine fbs] -- is responsible for dealing with the check insertions. That might be -- wrong. type BackendPossible fbs = (DFunct,[ModedVar],ModedVar) - -> Either Bool (Action fbs) - -type Possible fbs = (Crux (ModedVar) (ModedNT)) -> Maybe (Action fbs) + -> Either Bool (BackendAction fbs) {- mapMaybeModeCompat mis mo = @@ -133,51 +169,95 @@ mapMaybeModeCompat mis mo = return (d,f)) -} -possible :: BackendPossible fbs -> Possible fbs -possible fp cr = case cr of - -- XXX Indirect evaluation is not yet supported - Left (CFEval _ _) -> dynacSorry "Indir eval" +-- | Free, Universal, or Panic. A rather simplistic take on unification. +-- +-- XXX There is nothing good about this. +fup :: forall a m . (Monad m, MCVT m DVar ~ VR DFunct (NIX DFunct), MCR m DVar) + => DVar -> m a -> m a -> m a +fup v cf cu = do + vr <- clookup v + let vi = case vr of + VRName vn -> fmap VRName $ nExpose vn + VRStruct vx -> vx + case vi of + IFree -> cf + IUniv _ -> cu + _ -> dynacPanic "Unexpected instantiation state while planning" + +possible :: (Monad m) + => BackendPossible fbs + -> Crux DVar NTV + -> SIMCT m DFunct (Actions fbs) +possible fp cr = + case cr of + -- XXX Indirect evaluation is not yet supported + Left (CFEval _ _) -> dynacSorry "Indir eval" + + -- XXX This is going to be such a pile. We really, really should have + -- unification crank out a series of DOpAMine opcodes for us, but for + -- the moment, since everything we do is either IFree or IUniv, just use + -- iEq everywhere. -- Assign or check - Right (CFAssign o i) -> - let ni = ntvOfMNT i in - case (evnOfMNT i, o) of - (Left _, MF _) -> Nothing - (Right _, MB o') -> let chk = "_chk" in - Just [ OPAsgn chk ni - , OPCheq chk o'] - (Left i', MB o') -> Just [OPAsgn i' (NTVar o')] - (Right _, MF o') -> Just [OPAsgn o' ni] - - -- Structure building - Right (CFStruct o is funct) -> - case o of - -- If the output is free, the only supported case is when all - -- inputs are known. - MF o' -> if all isBound is - then Just [OPWrap o' (map varOfMV is) funct] - else Nothing - -- On the other hand, if the output is known, then any subset - -- of the inputs may be known and will be checked. - MB o' -> Just $ (OPPeel is' o' funct) - : map (\(c,x) -> (OPCheq c x)) cis - where - mkChks _ (MF i) = (i, Nothing) - mkChks n (MB v) = let chk = BC.pack $ "_chk_" ++ (show n) - in (chk, Just (chk, v)) - - (is',mcis) = unzip $ zipWith mkChks [0::Int ..] is - cis = MA.catMaybes mcis - - Left (CFCall o is funct) -> - case fp (funct,is,o) of - Left False -> Just [OPIter o is funct DetNon Nothing ] - Left True -> Nothing - Right a -> Just a + Right (CFAssign o i) -> + case i of + NTVar v -> fup v (fup o (throwError UFExDomain) + (runReaderT (unifyVV v o) (UnifParams True False) >> return [ OPAsgn v (NTVar o) ])) + (fup o (runReaderT (unifyVV v o) (UnifParams True False) >> return [ OPAsgn o i ]) + (return [ OPCheq o v ])) + NTBase b -> fup o (runReaderT (unifyVU o) (UnifParams True False) >> return [ OPAsgn o i ]) + (let chk = "_chk" in return [ OPAsgn chk i, OPCheq chk o]) + + -- Structure building or unbuilding + Right (CFStruct o is funct) -> fup o (mapM_ isBound is >> bind o >> return [ OPWrap o is funct ]) + (buildPeel) + where + buildPeel = do + (is', mcis) <- zipWithM maybeCheck is newvars >>= return . unzip + let cis = MA.catMaybes mcis + return ([ OPPeel is' o funct ] ++ map (uncurry OPCheq) cis) + + newvars = map (\n -> BC.pack $ "_chk_" ++ (show n)) [0..] + + maybeCheck v nv = fup v (return (v,Nothing)) (return (nv, Just (nv,v))) + + Left (CFCall vo vis funct) -> do + is <- mapM mkMV vis + o <- mkMV vo + case fp (funct,is,o) of + -- Not a built-in, so we assume that it can be iterated in full. + Left False -> do mapM_ bind (vo:vis) + return [OPIter o is funct DetNon Nothing] + Left True -> throwError UFExDomain + Right (BAct a m) -> do runReaderT + (mapM_ (uncurry $ flip unifyUnaliasedNV) m) + (UnifParams True True) -- XXX Live? + return a + where + mo = nHide (IUniv UShared) + unifyVU v = unifyUnaliasedNV mo v + mkMV v = do + vi <- clookup v + return $ MV v (vrToNIX vi) mo + + isBound v = fup v (throwError UFExDomain) (return ()) + bind x = runReaderT (unifyVU x) (UnifParams False False) ------------------------------------------------------------------------}}} -- ANF to Cruxes {{{ +anfVars :: ANFState -> S.Set DVar +anfVars (AS { as_evals = evals, as_unifs = unifs, as_assgn = assgns } ) = + S.unions [ M.foldWithKey (\k v s -> S.insert k (go1 v s)) S.empty evals + , M.foldWithKey (\k v s -> S.insert k (go2 v s)) S.empty assgns + , foldr (\(v1,v2) s -> S.insert v1 (S.insert v2 s)) S.empty unifs + ] + where + go s (_,vs) = S.union s (S.fromList vs) + go1 e s = either (flip S.insert s) (go s) e + go2 e s = either (const s) (go s) e + + eval_cruxes :: ANFState -> [EvalCrux DVar] eval_cruxes = M.foldrWithKey (\o i -> (crux o i :)) [] . as_evals where @@ -201,7 +281,7 @@ type Cost = Double -- XXX I don't understand why this heuristic works, but it seems to exclude -- some of the... less intelligent plans. -simpleCost :: PartialPlan fbs -> Action fbs -> Cost +simpleCost :: PartialPlan fbs -> Actions fbs -> Cost simpleCost (PP { pp_score = osc, pp_plan = pfx }) act = 2 * osc + (1 + loops pfx) * actCost act where @@ -220,9 +300,9 @@ simpleCost (PP { pp_score = osc, pp_plan = pfx }) act = OPIter o is _ d _ -> case d of Det -> 0 DetSemi -> 1 - DetNon -> 2 ** (fromIntegral $ length $ + DetNon -> 2 {- ** (fromIntegral $ length $ filter isFree (o:is)) - - 1 + - 1 -} OPIndr _ _ -> 100 loops = fromIntegral . length . filter isLoop @@ -266,12 +346,24 @@ data PartialPlan fbs = PP { pp_cruxes :: S.Set (Crux DVar NTV) , pp_binds :: BindChart , pp_restrictSearch :: Bool , pp_score :: Cost - , pp_plan :: Action fbs + , pp_plan :: Actions fbs } -stepPartialPlan :: Possible fbs +pp_liveVars :: PartialPlan fbs -> S.Set DVar +pp_liveVars p = S.unions $ map lvs $ S.toList (pp_cruxes p) + where + lvs (Left (CFCall v vs _)) = S.fromList (v:vs) + lvs (Left (CFEval v v')) = S.fromList [v,v'] + lvs (Right (CFStruct v vs _)) = S.fromList (v:vs) + lvs (Right (CFAssign v (NTVar v'))) = S.fromList [v,v'] + lvs (Right (CFAssign v (NTBase _))) = S.singleton v + +-- XXX This does not have a way to signal UFNotReached back to its caller. +-- That is particularly disappointing since any unification producing that +-- means that there's certainly no plan for the whole rule. +stepPartialPlan :: (Crux DVar NTV -> SIMCT Identity DFunct (Actions fbs)) -- ^ Possible actions - -> (PartialPlan fbs -> Action fbs -> Cost) + -> (PartialPlan fbs -> Actions fbs -> Cost) -- ^ Plan scoring function -> Maybe (Maybe DFunctAr, DVar, DVar) -- ^ The 'DFunctAr', intern representation, and @@ -279,8 +371,8 @@ stepPartialPlan :: Possible fbs -- initial /evaluation/ crux, if any. This is used to -- avoid double-counting during updates. See $dupcrux -> PartialPlan fbs - -> Either (Cost, Action fbs) [PartialPlan fbs] -stepPartialPlan steps score mic p = + -> Either (Cost, Actions fbs) [PartialPlan fbs] +stepPartialPlan poss score mic p = -- XT.traceShow ("SPP", mic, pp_binds p, pp_cruxes p) $ if S.null (pp_cruxes p) then Left $ (pp_score p, pp_plan p) @@ -305,39 +397,44 @@ stepPartialPlan steps score mic p = step = S.fold (\crux ps -> let bc = pp_binds p pl = pp_plan p - plan = steps (cruxMode bc crux) - bc' = bc `S.union` cruxVars crux + plan = runIdentity $ runSIMCT (poss crux) bc rc' = S.delete crux (pp_cruxes p) r' = (not $ cruxIsEval crux) || (pp_restrictSearch p) - in maybe ps - (\act -> let act' = handleConflictors act - in PP rc' bc' r' (score p act') (pl ++ act') - : ps) - plan + in either (const ps) + (\(act,bc') -> let act' = handleConflictors act + in PP rc' bc' r' (score p act') (pl ++ act') + : ps) + plan ) [] handleConflictors = case mic of Nothing -> id - Just (mfa,i,ov) -> concatMap $ \dop -> + Just (mfa,i,ov) -> \p -> flip concatMap p (\dop -> case dop of OPIter ov' ivs' f' _ _ | -- We must insert checks whenever this step involves -- an evaluation. As an easy optimisation, if we know -- the 'DFunctAr' being updated, we can elide this check -- when we're evaluating a different 'DFunctAr'. + -- + -- XXX This is not the whole answer since it continues to + -- assume that everything is bound on the way out of an + -- OPIter. Really we should be transforming the ANF to + -- include cruxes for these checks, that way they will get + -- handled by mode analysis as with everything else. (maybe True (== (f',length ivs')) mfa) - && ov > varOfMV ov' + && ov > ov'^.mv_var -> let cv = "_chk" in [ dop - , OPWrap cv (map varOfMV ivs') f' + , OPWrap cv (fmap (^.mv_var) ivs') f' , OPCkne i cv ] - _ -> [dop] + _ -> [dop]) -planner_ :: Possible fbs +planner_ :: (Crux DVar NTV -> SIMCT Identity DFunct (Actions fbs)) -- ^ Available steps - -> (PartialPlan fbs -> Action fbs -> Cost) + -> (PartialPlan fbs -> Actions fbs -> Cost) -- ^ Scoring function -> S.Set (Crux DVar NTV) -- ^ Cruxes to be planned over @@ -348,11 +445,15 @@ planner_ :: Possible fbs -> S.Set DVar -- ^ Any variables bound on the way in, in addition to -- the two given for an initial crux - -> [(Cost, Action fbs)] + -> S.Set DVar + -- ^ Unbound variables in the rule + -> [(Cost, Actions fbs)] -- ^ Plans and their costs -planner_ st sc cr mic bv = runAgenda +planner_ st sc cr mic bv fv = runAgenda $ PP { pp_cruxes = cr - , pp_binds = S.union bv bi + , pp_binds = SIMCtx $ M.fromSet (const $ VRStruct (IUniv UShared)) (S.unions [bv,bi]) + `M.union` + M.fromSet (const $ VRStruct IFree) fv , pp_restrictSearch = False , pp_score = 0 , pp_plan = ip @@ -385,7 +486,7 @@ anfPlanner_ st sc anf mic bv = planner_ st sc cruxes mic bv $ maybe id (\(ic,_,_) -> S.delete ic) mic $ S.fromList $ eval_cruxes anf) -bestPlan :: [(Cost, Action fbs)] -> Maybe (Cost, Action fbs) +bestPlan :: [(Cost, a)] -> Maybe (Cost, a) bestPlan [] = Nothing bestPlan plans = Just $ argmin fst plans @@ -394,30 +495,32 @@ bestPlan plans = Just $ argmin fst plans -- -- XXX This has no idea what to do about non-range-restricted rules. planUpdate_ :: BackendPossible fbs -- ^ Available steps - -> (PartialPlan fbs -> Action fbs -> Cost) -- ^ Scoring function + -> (PartialPlan fbs -> Actions fbs -> Cost) -- ^ Scoring function -> ANFState -- ^ Normal form -> Maybe (EvalCrux DVar, DVar, DVar) -- ^ Initial eval crux - -> [(Cost, Action fbs)] -- ^ If there's a plan... -planUpdate_ bp sc anf mic = anfPlanner_ (possible bp) sc anf mic S.empty + -> S.Set DVar + -> [(Cost, Actions fbs)] -- ^ If there's a plan... +planUpdate_ bp sc anf mic fv = anfPlanner_ (possible bp) sc anf mic S.empty fv planUpdate :: BackendPossible fbs - -> (PartialPlan fbs -> Action fbs -> Cost) + -> (PartialPlan fbs -> Actions fbs -> Cost) -> ANFState -> Maybe (EvalCrux DVar, DVar, DVar) - -> Maybe (Cost, Action fbs) -planUpdate bp sc anf mi = - bestPlan $ planUpdate_ bp sc anf mi + -> S.Set DVar + -> Maybe (Cost, Actions fbs) +planUpdate bp sc anf mi fv = + bestPlan $ planUpdate_ bp sc anf mi fv -planInitializer :: BackendPossible fbs -> Rule -> Maybe (Cost, Action fbs) +planInitializer :: BackendPossible fbs -> Rule -> Maybe (Cost, Actions fbs) planInitializer bp (Rule { r_anf = anf }) = - planUpdate bp simpleCost anf Nothing + planUpdate bp simpleCost anf Nothing (anfVars anf) planEachEval :: BackendPossible fbs -- ^ The backend's primitive support -> (DFunctAr -> Bool) -- ^ Indicator for constant function -> Rule - -> [(Maybe DFunctAr, Maybe (Cost, DVar, DVar, Action fbs))] -planEachEval bp cs (Rule { r_anf = anf }) = - map (\(mfa,cr) -> (mfa, varify $ planUpdate bp simpleCost anf $ Just $ mic cr)) + -> [(Maybe DFunctAr, Maybe (Cost, DVar, DVar, Actions fbs))] +planEachEval bp cs r@(Rule { r_anf = anf }) = + map (\(mfa,cr) -> (mfa, varify $ planUpdate bp simpleCost anf (Just $ mic cr) (anfVars anf))) -- Filter out non-constant evaluations $ MA.mapMaybe (\ec -> case ec of CFCall _ is f | not (cs (f,length is)) @@ -437,6 +540,7 @@ planEachEval bp cs (Rule { r_anf = anf }) = varHead = "__i" varVal = "__v" +{- planGroundBackchain :: BackendPossible fbs -> Rule -> Maybe (Cost, DVar, Action fbs) @@ -447,7 +551,6 @@ planGroundBackchain bp (Rule { r_anf = anf, r_head = h }) = where varify = fmap $ \(c,a) -> (c,h,a) -{- planBackchains :: BackendPossible fbs -> Rule -> M.Map [Mode] (Cost, [DVar], Action fbs) @@ -458,7 +561,7 @@ planBackchains bp (Rule { r_anf = anf, r_head = h }) -- Update plan combination {{{ type UpdateEvalMap fbs = M.Map (Maybe DFunctAr) - [(Rule, Cost, DVar, DVar, Action fbs)] + [(Rule, Cost, DVar, DVar, Actions fbs)] -- | Return all plans for each functor/arity -- @@ -469,7 +572,7 @@ type UpdateEvalMap fbs = M.Map (Maybe DFunctAr) -- timv: might want to fuse these into one circuit -- combineUpdatePlans :: [(Rule,[( Maybe DFunctAr, - Maybe (Cost, DVar, DVar, Action fbs))])] + Maybe (Cost, DVar, DVar, Actions fbs))])] -> UpdateEvalMap fbs combineUpdatePlans = go (M.empty) where @@ -481,7 +584,7 @@ combineUpdatePlans = go (M.empty) case mca of Nothing -> dynacUserErr $ "No update plan for " - <+> (pretty fa) + <+> group (pretty fa) <+> "in rule at" <+> (prettySpanLoc $ r_span fr) Just (c,v1,v2,a) -> go' xs fr ys $ mapInOrApp fa (fr,c,v1,v2,a) m @@ -489,6 +592,7 @@ combineUpdatePlans = go (M.empty) ------------------------------------------------------------------------}}} -- Backward chaining plan combination {{{ +{- type QueryEvalMap fbs = M.Map (Maybe DFunctAr) [(Rule, Cost, DVar, Action fbs)] @@ -515,12 +619,13 @@ combineQueryPlans = go (M.empty) Nothing -> error "No unification for head variable?" Just (Left _) -> error "NTVar head?" Just (Right (f,a)) -> Just (f, length a) - +-} ------------------------------------------------------------------------}}} -- Adorned Queries {{{ +{- -- XXX We really ought to be returning something about math, as well, but -- as all that's handled specially up here... adornedQueries :: Action fbs -> S.Set (DFunct,[Mode],Mode) @@ -530,6 +635,7 @@ adornedQueries = go S.empty go x ((OPIter o is f _ _):as) = go (x `S.union` S.singleton (f, map modeOf is, modeOf o)) as go x (_:as) = go x as +-} ------------------------------------------------------------------------}}} -- Experimental Detritus {{{ diff --git a/src/Dyna/Main/BackendDefn.hs b/src/Dyna/Backend/BackendDefn.hs similarity index 60% rename from src/Dyna/Main/BackendDefn.hs rename to src/Dyna/Backend/BackendDefn.hs index b6756ad..ccb457b 100644 --- a/src/Dyna/Main/BackendDefn.hs +++ b/src/Dyna/Backend/BackendDefn.hs @@ -3,15 +3,19 @@ -- Header material {{{ {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE Rank2Types #-} -module Dyna.Main.BackendDefn where +module Dyna.Backend.BackendDefn where import qualified Data.Set as S import Dyna.Analysis.Aggregation (AggMap) import Dyna.Analysis.ANF (Rule) -import Dyna.Analysis.RuleMode (Action, BackendPossible, Cost, - UpdateEvalMap, QueryEvalMap) -import Dyna.Term.TTerm (DFunctAr) +import Dyna.Analysis.DOpAMine (BackendRenderDopIter, ModedVar) +import Dyna.Analysis.Mode.Det +import Dyna.Analysis.RuleMode ( + Actions, BackendPossible, Cost, + UpdateEvalMap {-, QueryEvalMap -}) +import Dyna.Term.TTerm (DFunct, DFunctAr) import System.IO (Handle) -- XXX The notion of be_constants is not quite right, I think? It is used @@ -21,26 +25,23 @@ import System.IO (Handle) type BackendDriver bs = AggMap -- ^ Aggregation -> UpdateEvalMap bs -- ^ Rule update - -> QueryEvalMap bs -- ^ Rule query - -> [(Rule,Cost,Action bs)] -- ^ Initializers + -- -> QueryEvalMap bs -- ^ Rule query + -> [(Rule,Cost,Actions bs)] -- ^ Initializers -> Handle -- ^ Output -> IO () data Backend = forall bs . Backend - { -- | Builtin support hook for mode planning. Options are - -- to return - -- - -- * @Left False@ -- This functor is not built in - -- - -- * @Left True@ -- There is no plan for this mode - -- - -- * @Right (d,b)@ -- There is a plan here with determinism - -- @d@ and backend-specific data @b@. + { -- | Hook for planner to get builtin information be_builtin :: BackendPossible bs -- | Any constants made available by this backend. + -- + -- XXX , be_constants :: S.Set DFunctAr - + + -- | Debugging hook to render bits of DOpAMine which + -- are "backend-specific" + , be_debug_dop_iter :: forall e . BackendRenderDopIter bs e -- | Backend driver , be_driver :: BackendDriver bs } diff --git a/src/Dyna/Backend/Backends.hs b/src/Dyna/Backend/Backends.hs new file mode 100644 index 0000000..09fd6f8 --- /dev/null +++ b/src/Dyna/Backend/Backends.hs @@ -0,0 +1,47 @@ +--------------------------------------------------------------------------- +-- | Pick among backends + +-- Header material {{{ +{-# LANGUAGE OverloadedStrings #-} + +module Dyna.Backend.Backends ( + backendHelp, backendMap, parseBackend, noBackend +) where + +import Data.Char +import qualified Data.Map as M +import Dyna.Backend.BackendDefn +import Dyna.Backend.NoBackend +import Dyna.Backend.Python +import Dyna.Main.Exception +import Text.PrettyPrint.Free as PP + +------------------------------------------------------------------------}}} +-- Backend Map {{{ + +backendMap :: M.Map String (Doc e,Backend) +backendMap = M.fromList + [ ("none", ("null backend for early stages only", noBackend)) + , ("python", ("generate python code",pythonBackend)) + ] + +------------------------------------------------------------------------}}} +-- Backend Parser {{{ + +parseBackend :: String -> Backend +parseBackend s = maybe (dynacThrow $ InvocationError + $ "Unknown backend:" <+> pretty s) + snd + $ M.lookup (map toLower s) backendMap + +------------------------------------------------------------------------}}} +-- Backend Help Info {{{ + +backendHelp :: Doc e +backendHelp = above "\nBackends available: " + $ indent 4 $ vcat + $ map (\(k,v) -> pretty k <+> colon <+> fst v) + $ M.assocs backendMap + +------------------------------------------------------------------------}}} + diff --git a/src/Dyna/Backend/NoBackend.hs b/src/Dyna/Backend/NoBackend.hs new file mode 100644 index 0000000..5202fb6 --- /dev/null +++ b/src/Dyna/Backend/NoBackend.hs @@ -0,0 +1,128 @@ +--------------------------------------------------------------------------- +-- | A backend that does no code generation. +-- +-- It is anticipated that this will be useful for debugging the earlier +-- stages of the compiler. + +-- Header material {{{ + +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE Rank2Types #-} +module Dyna.Backend.NoBackend (noBackend) where + +import Control.Lens +import Control.Monad +import qualified Data.Map as M +import qualified Data.Set as S +import Dyna.Analysis.ANF +import Dyna.Analysis.DOpAMine +import Dyna.Analysis.Mode +import Dyna.Analysis.RuleMode (Actions,BackendAction(..),Cost) +import Dyna.Backend.BackendDefn +import Dyna.Main.Exception +import Dyna.Term.TTerm +import Dyna.XXX.DataUtils +import Dyna.XXX.PPrint +import Dyna.XXX.Trifecta (prettySpanLoc) +import System.IO +import Text.PrettyPrint.Free + +import qualified Debug.Trace as XT + +------------------------------------------------------------------------}}} +-- Definition {{{ + +noBackend :: Backend +noBackend = Backend + { be_builtin = primPossible + , be_constants = M.keysSet primOps -- XXX + , be_debug_dop_iter = \_ _ _ _ _ -> empty + , be_driver = driver + } + +driver am um {-_-} is fh = hPutStrLn fh "No backend selected; stopping." + +------------------------------------------------------------------------}}} +-- Primitive operations {{{ + +data PrimOp = PO + { po_qm :: QMode (NIX DFunct) + , po_bs :: forall e . Doc e + } + +primOps :: M.Map DFunctAr [QMode (NIX DFunct)] -- XXX ,UMode +primOps = M.fromList + [ let ar = 2 in ( ("+" ,ar) , [miaod ar Det ] + ++ opinvd ar Det ) + , let ar = 2 in ( ("-" ,ar) , [miaod ar Det ] + ++ opinvd ar Det ) + , let ar = 2 in ( ("*" ,ar) , [miaod ar Det ] + ++ opinvd ar DetSemi ) + , let ar = 2 in ( ("/" ,ar) , [miaod ar DetSemi ] + ++ opinvd ar DetSemi ) + , let ar = 2 in ( ("^" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("&" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("|" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("%" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("**" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("<" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("<=" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( (">" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( (">=" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("=" ,ar) , [miaod ar Det ] ) + -- Unary boolean negation + , let ar = 1 in ( ("!" ,ar) , [miaod ar Det ] ) + -- Unary numeric negation + , let ar = 1 in ( ("-" ,ar) , [miaod ar Det ] ) + , let ar = 1 in ( ("mod" ,ar) , [miaod ar Det ] ) + , let ar = 1 in ( ("abs" ,ar) , [miaod ar Det ] ) + , let ar = 1 in ( ("log" ,ar) , [miaod ar Det ] ) + , let ar = 1 in ( ("exp" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("and" ,ar) , [miaod ar Det ] ) + , let ar = 2 in ( ("or" ,ar) , [miaod ar Det ] ) + , let ar = 1 in ( ("not" ,ar) , [miaod ar Det ] ) + ] + +primPossible :: (DFunct,[ModedVar],ModedVar) -> Either Bool (BackendAction ()) +primPossible (f,mvis,mvo) = maybe (Left False) go $ M.lookup (f,length mvis) primOps + where + go :: [QMode (NIX DFunct)] -> Either Bool (BackendAction ()) + go [] = Left True + go (x:xs) = -- XT.traceShow ("PRIMPOSS",mvis,mvo,x) $ + if and (zipWithTails nSub p p qim pim) + then Right $ BAct [OPIter mvo mvis f DetNon (Just ())] qom + else go xs + where + mvs = mvo:mvis + mds = x^.qmode_result : x^.qmode_args + + pim = fmap (^.mv_mi) mvs + qim = fmap fst mds + + qom = zipWithTails (,) p p + (fmap (^.mv_var) mvs) + (fmap snd mds) + + p _ = dynacPanicStr "NoBackend.primPossible length mismatch" + +------------------------------------------------------------------------}}} +-- Utility constructs {{{ + +nuniv, nfree :: NIX DFunct +nuniv = nHide (IUniv UShared) +nfree = nHide (IFree) + +nnIn, nnOut :: (NIX DFunct, NIX DFunct) +nnIn = (nuniv, nuniv) +nnOut = (nfree, nuniv) + +-- | mode ins and out +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) + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Backend/Python.hs b/src/Dyna/Backend/Python.hs index e0fba72..a1802cd 100644 --- a/src/Dyna/Backend/Python.hs +++ b/src/Dyna/Backend/Python.hs @@ -4,13 +4,17 @@ -- See bin/interpreter.py -- Header material {{{ +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE LiberalTypeSynonyms #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE Rank2Types #-} module Dyna.Backend.Python (pythonBackend) where import Control.Applicative ((<*)) import qualified Control.Arrow as A import Control.Exception +import Control.Lens ((^.)) import Control.Monad import qualified Data.ByteString as B import qualified Data.ByteString.UTF8 as BU @@ -23,10 +27,11 @@ import qualified Data.Ord as O import qualified Data.Set as S import qualified Debug.Trace as XT import Dyna.Analysis.ANF -import Dyna.Analysis.Base import Dyna.Analysis.Aggregation +import Dyna.Analysis.DOpAMine +import Dyna.Analysis.Mode import Dyna.Analysis.RuleMode -import Dyna.Main.BackendDefn +import Dyna.Backend.BackendDefn import Dyna.Main.Exception import Dyna.Term.TTerm import qualified Dyna.ParserHS.Parser as P @@ -40,66 +45,101 @@ import qualified Text.Trifecta as T ------------------------------------------------------------------------}}} -- DOpAMine Backend Information {{{ --- At the moment, we pass through a @Maybe ()@ to indicate whether or not --- we're making a call. See the call to pycall in pdope_ below. -type PyDopeBS = () +-- | We can optionally attach a function to an 'OPIter' call, +-- which lets us permute arguments and so on when we go to do code +-- generation without having to re-probe the modes. +newtype PyDopeBS = PDBS (forall e . ModedVar -> [ModedVar] -> Doc e) + +nfree = nHide IFree +nuniv = nHide (IUniv UShared) + +isGround, isFree :: ModedVar -> Bool +isGround v = nGround (v^.mv_mi) +isFree v = nSub (v^.mv_mi) nfree builtins :: BackendPossible PyDopeBS builtins (f,is,o) = case () of - _ | all isBound is && S.member (f,length is) constants - -> case modeOf o of - MFree -> Right [OPIter o is f Det (Just ())] - MBound -> let chkv = "_chk" - in Right $ [ OPIter (MF chkv) is f Det (Just ()) - , OPCheq chkv (varOfMV o) - ] - - _ | f == "+" - -> case (is,o) of - ([x@(MB _),y@(MF _)],MB _) -> Right [OPIter y [o,x] "-" Det $ Just ()] - ([x@(MF _),y@(MB _)],MB _) -> Right [OPIter x [o,y] "-" Det $ Just ()] + _ | all isGround is + -> maybe (Left False) gencall $ M.lookup (f,length is) constants + where + gencall pc = case () of + _ | isFree o -> + Right $ BAct [OPIter o is f Det (Just pc)] + [(o^.mv_var, nuniv)] + _ | isGround o -> + let chkv = "_chk" + fchk = MV chkv nfree nuniv + in Right $ BAct [ OPIter fchk is f Det (Just pc) + , OPCheq chkv (o^.mv_var) ] + [] + _ -> Left True + + -- XXX These next two branches have nothing specific about Python at all + -- and shouldn't be here. Similarly, the corresponding entries in + -- NoBackend also shouldn't be around (possibly). These should be handled + -- much more generically earlier in the pipeline. + _ | f == "+" && isGround o + -> case is of + [x,y] | isGround x && isFree y + -> Right $ BAct [OPIter y [o,x] "-" Det (Just$ PDBS$ infixOp "-")] + [(y^.mv_var, nuniv)] + [x,y] | isFree x && isGround y + -> Right $ BAct [OPIter x [o,y] "-" Det (Just$ PDBS$ infixOp "-")] + [(x^.mv_var, nuniv)] _ -> Left True - _ | f == "-" - -> case (is,o) of - ([x@(MB _),y@(MF _)],MB _) -> Right [OPIter y [x,o] "-" Det $ Just ()] - ([x@(MF _),y@(MB _)],MB _) -> Right [OPIter x [o,y] "+" Det $ Just ()] + _ | f == "-" && isGround o + -> case is of + [x,y] | isGround x && isFree y + -> Right $ BAct [OPIter y [x,o] "-" Det (Just$ PDBS$ infixOp "-")] + [(y^.mv_var, nuniv)] + [x,y] | isFree x && isGround y + -> Right $ BAct [OPIter x [o,y] "+" Det (Just$ PDBS$ infixOp "+")] + [(x^.mv_var, nuniv)] _ -> Left True - _ | S.member (f,length is) constants -> Left True + _ | M.member (f,length is) constants -> Left True _ -> Left False --- XXX This and pycall ought to be merged -constants :: S.Set (DFunct,Int) -constants = S.fromList - [ ("+",2) - , ("-",2) - , ("-",1) -- unary negation - , ("*",2) - , ("/",2) - , ("^",2) - , ("&",2) - , ("|",2) - , ("%",2) - , ("**",2) - , ("<",2) - , ("<=",2) - , (">",2) - , (">=",2) - , ("=",2) - , ("!",1) - , ("mod",1) - , ("abs",1) - , ("log",1) - , ("exp",1) - , ("and",2) - , ("or",2) - , ("not",1) - , ("eval",1) - , ("true",0) - , ("false",0) - , ("null",0) -- XXX is this right? +infixOp op _ vis = sepBy op $ mpv vis +mpv = map (pretty . (^.mv_var)) + +constants :: M.Map (DFunct,Int) PyDopeBS +constants = M.fromList + [(("+",2) , PDBS $ infixOp "+" ) + ,(("-",2) , PDBS $ infixOp "-" ) + ,(("*",2) , PDBS $ infixOp "*" ) + ,(("/",2) , PDBS $ infixOp "/" ) + ,(("^",2) , PDBS $ infixOp "^" ) + ,(("&",2) , PDBS $ infixOp "&" ) + ,(("|",2) , PDBS $ infixOp "|" ) + ,(("%",2) , PDBS $ infixOp "%" ) + ,(("**",2) , PDBS $ infixOp "**" ) + ,(("<",2) , PDBS $ infixOp "<" ) + ,(("<=",2) , PDBS $ infixOp "<=" ) + ,((">",2) , PDBS $ infixOp ">" ) + ,((">=",2) , PDBS $ infixOp ">=" ) + ,(("=",2) , PDBS $ infixOp "=" ) + ,(("!=",2) , PDBS $ infixOp "!=" ) + ,(("and",2) , PDBS $ infixOp "and" ) + ,(("or",2) , PDBS $ infixOp "or" ) + + ,(("true",0) , PDBS $ nullary "True" ) + ,(("false",0) , PDBS $ nullary "False") + ,(("null",0) , PDBS $ nullary "None" ) + + ,(("-",1) , PDBS $ call "-" ) + ,(("!",1) , PDBS $ call "not" ) + ,(("not",1) , PDBS $ call "not" ) + ,(("mod",1) , PDBS $ call "mod" ) + ,(("abs",1) , PDBS $ call "abs" ) + ,(("log",1) , PDBS $ call "log" ) + ,(("exp",1) , PDBS $ call "exp" ) + ,(("$eval",1) , PDBS $ call "$eval" ) ] + where + nullary v _ _ = v + call fn _ vis = fn <> (parens $ sepBy "," $ mpv vis) ------------------------------------------------------------------------}}} -- DOpAMine Printout {{{ @@ -118,48 +158,12 @@ tupledOrUnderscore vs = if length vs > 0 then parens ((sepBy "," $ map pretty vs) <> ",") else text "_" -filterBound = map (\(MF v) -> pretty v) . filter (not.isBound) pslice vs = brackets $ - sepBy "," (map (\x -> case x of (MF _) -> ":" ; (MB v) -> pretty v) vs) + sepBy "," (map (\x -> if nGround (x^.mv_mi) then pretty (x^.mv_var) else ":") vs) <> "," -- add a list comma to ensure getitem is always passed a tuple. -pycall f vs = case (f, length vs) of - ( "*", 2) -> infixOp " * " - ( "+", 2) -> infixOp " + " - ( "-", 2) -> infixOp " - " - ( "/", 2) -> infixOp " / " - ( "^", 2) -> infixOp " ** " - ( "&", 2) -> infixOp " and " -- note: python's 'and' and 'or' operate on more than bool - ( "|", 2) -> infixOp " or " - ( "=", 2) -> infixOp " == " - ( "<", 2) -> infixOp " < " - ( "<=", 2) -> infixOp " <= " - ( ">", 2) -> infixOp " > " - ( ">=", 2) -> infixOp " >= " - ( "==", 2) -> infixOp " == " - ( "!=", 2) -> infixOp " != " - ("mod", 2) -> infixOp " % " - - ("eval", 1) -> call "eval" -- note: security hole. - - ( "abs", 1) -> call "abs" - ( "log", 1) -> call "log" - ( "exp", 1) -> call "exp" - ( "!", 1) -> call "not" - ( "-", 1) -> call "-" - - ( "null", 0) -> "None" - ( "true", 0) -> "True" - ("false", 0) -> "False" - - x -> dynacPanic $ "Python.hs: Unknown request to pycall: " - <> pretty x - - where pretty_vs = map (pretty . varOfMV) vs - call name = name <> (parens $ sepBy ", " $ pretty_vs) - infixOp op = sepBy op $ pretty_vs - +filterGround = map (^.mv_var) . filter (not.nGround.(^.mv_mi)) -- | Render a single dopamine opcode or its surrogate pdope_ :: DOpAMine PyDopeBS -> Doc e @@ -172,8 +176,8 @@ pdope_ (OPCkne v val) = "if" <+> pretty v <+> "==" pdope_ (OPPeel vs i f) = "try:" `above` (indent 4 $ tupledOrUnderscore vs - <+> equals <> " " - <> "peel" <> (parens $ pfas f vs <> comma <> pretty i) + <+> equals + <+> "peel" <> (parens $ pfas f vs <> comma <> pretty i) ) -- you'll get a "TypeError: 'NoneType' is not iterable." `above` "except (TypeError, AssertionError): continue" @@ -183,17 +187,17 @@ pdope_ (OPWrap v vs f) = pretty v <> (parens $ pfas f vs <> comma <> (sepBy "," $ map pretty vs)) -pdope_ (OPIter v vs f _ (Just ())) = pretty (varOfMV v) +pdope_ (OPIter v vs f _ (Just (PDBS c))) = pretty (v^.mv_var) <+> equals - <+> pycall f vs + <+> c v vs pdope_ (OPIter o m f _ Nothing) = let mo = m ++ [o] in - "for" <+> (tupledOrUnderscore $ filterBound mo) + "for" <+> (tupledOrUnderscore $ filterGround mo) <+> "in" <+> functorIndirect "chart" f m <> pslice mo <> colon -- | Render a dopamine sequence's checks and loops above a (indended) core. -pdope :: [DOpAMine PyDopeBS] -> Doc e -> Doc e +pdope :: Actions PyDopeBS -> Doc e -> Doc e pdope _d _e = (indent 4 $ "for _ in [None]:") `above` (indent 8 $ go _d _e) where @@ -223,7 +227,7 @@ findHeadFA (Rule _ h _ _ _ (AS { as_assgn = as })) = Just (Left _) -> error "NTVar head?" Just (Right (f,a)) -> Just (f, length a) -printInitializer :: Handle -> Rule -> Action PyDopeBS -> IO () +printInitializer :: Handle -> Rule -> Actions PyDopeBS -> IO () printInitializer fh rule@(Rule _ h _ r _ _) dope = do displayIO fh $ renderPretty 1.0 100 $ "@initializer" <> parens (uncurry pfa $ MA.fromJust $ findHeadFA rule) @@ -234,7 +238,7 @@ printInitializer fh rule@(Rule _ h _ r _ _) dope = do emit = "emit" <> tupled [pretty h, pretty r] -- XXX INDIR EVAL -printUpdate :: Handle -> Rule -> Maybe DFunctAr -> (DVar, DVar) -> Action PyDopeBS -> IO () +printUpdate :: Handle -> Rule -> Maybe DFunctAr -> (DVar, DVar) -> Actions PyDopeBS -> IO () printUpdate fh rule@(Rule _ h _ r _ _) (Just (f,a)) (hv,v) dope = do displayIO fh $ renderPretty 1.0 100 $ "@register" <> parens (pfa f a) @@ -248,7 +252,7 @@ printUpdate fh rule@(Rule _ h _ r _ _) (Just (f,a)) (hv,v) dope = do -- Driver {{{ driver :: BackendDriver PyDopeBS -driver am um qm is fh = do +driver am um {-qm-} is fh = do -- Aggregation mapping hPutStrLn fh $ "agg_decl = {}" forM_ (M.toList am) $ \((f,a),v) -> do @@ -273,6 +277,7 @@ driver am um qm is fh = do printPlanHeader fh r c printInitializer fh r a +{- hPutStrLn fh $ "# ==Queries==" forM_ (M.toList qm) $ \(fa, ps) -> do @@ -283,12 +288,15 @@ driver am um qm is fh = do -- XXX -- displayIO fh $ renderPretty 1.0 100 $ pdope a "XXX" hPutStrLn fh "" - +-} ------------------------------------------------------------------------}}} -- Export {{{ pythonBackend :: Backend -pythonBackend = Backend builtins constants driver +pythonBackend = Backend builtins + (M.keysSet constants) + (\o is _ _ (PDBS e) -> e o is) + driver ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Backend/Python/Selftest.hs b/src/Dyna/Backend/Python/Selftest.hs index 7e4b3c4..a6cde15 100644 --- a/src/Dyna/Backend/Python/Selftest.hs +++ b/src/Dyna/Backend/Python/Selftest.hs @@ -15,6 +15,9 @@ import Test.Golden ------------------------------------------------------------------------}}} -- Run Backend {{{ +-- XXX There's something wrong here -- if we encounter an ExitFailure and +-- throw an exception, we fail to fail the test or even time out. This +-- might be my fault, or it might be upstream. runDynaPy :: String -> String -> IO () runDynaPy f out = do devnull <- openFile "/dev/null" ReadWriteMode diff --git a/src/Dyna/Main/Driver.hs b/src/Dyna/Main/Driver.hs index d2eb788..73a9e85 100644 --- a/src/Dyna/Main/Driver.hs +++ b/src/Dyna/Main/Driver.hs @@ -8,28 +8,31 @@ -- see what it's like. It won't be hard to -- rip out. {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE Rank2Types #-} module Dyna.Main.Driver where import Control.Applicative ((<*)) import Control.Exception -- import Control.Monad -import Data.Char import qualified Data.Map as M import qualified Data.Maybe as MA import qualified Data.Set as S import Dyna.Analysis.Aggregation import Dyna.Analysis.ANF +import Dyna.Analysis.DOpAMine import Dyna.Analysis.RuleMode -import Dyna.Backend.Python -import Dyna.Main.BackendDefn +import Dyna.Backend.BackendDefn +import Dyna.Backend.Backends import Dyna.Main.Exception import qualified Dyna.ParserHS.Parser as P +-- import Dyna.Term.TTerm +import Dyna.XXX.Trifecta (prettySpanLoc) import System.Console.GetOpt import System.Environment import System.Exit import System.IO -import Text.PrettyPrint.Free +import Text.PrettyPrint.Free as PP import qualified Text.PrettyPrint.ANSI.Leijen as PPA import qualified Text.Trifecta as T import qualified Text.Trifecta.Result as TR @@ -39,6 +42,7 @@ import qualified Text.Trifecta.Result as TR data DumpType = DumpAgg | DumpANF + | DumpDopUpd | DumpParsed deriving (Eq,Ord,Show) @@ -64,28 +68,21 @@ anyDumpStderr :: (?dcfg :: DynacConfig) => Bool anyDumpStderr = M.foldr (\v r -> r || MA.isNothing v) False (dcfg_dumps ?dcfg) -------------------------------------------------------------------------}}} --- Backend {{{ - -noBackend :: Backend -noBackend = Backend - { be_builtin = \_ -> Left False - , be_constants = S.empty - , be_driver = \_ _ _ _ _ -> hPutStrLn stderr - "No backend specified; stopping" - } - -backendmap :: M.Map String (Doc e,Backend) -backendmap = M.fromList - [ ("none", ("null backend for early stages only", noBackend)) - , ("python", ("generate python code",pythonBackend)) - ] - -parseBackend :: String -> Backend -parseBackend s = maybe (dynacThrow $ InvocationError - $ "Unknown backend:" <+> pretty s) - snd - $ M.lookup (map toLower s) backendmap +dumpOpts :: Bool -> [OptDescr Opt] +dumpOpts nos = + mkDumpOpt "agg" DumpAgg "Aggregator summary" + ++ mkDumpOpt "anf" DumpANF "Administrative Normal Form" + ++ mkDumpOpt "dopupd" DumpDopUpd "DOpAMine planning results" + ++ mkDumpOpt "parse" DumpParsed "Parser output" + where + mkDumpOpt arg fl hm = + Option [] ["dump-" ++ arg] (OptArg (OptDump . sfl) "FILE") hm + : if nos + then [ Option [] ["no-dump-" ++ arg] (NoArg (OptDump cfl)) "" ] + else [] + where + sfl x fs = M.insert fl x fs + cfl fs = M.delete fl fs ------------------------------------------------------------------------}}} -- DynacConfiguration {{{ @@ -120,10 +117,7 @@ quickExit QEHelp = where h = "\nUsage: dyna -B backend -o FILE.out FILE.dyna\n\nOption summary:" quickExit QEHelpBackend = do - putDoc $ above "\nBackends available: " - $ indent 4 $ vcat - $ map (\(k,v) -> pretty k <+> colon <+> fst v) - $ M.assocs backendmap + putDoc backendHelp putStrLn "" quickExit QEHelpDump = putStrLn (usageInfo "\nDump options:" $ dumpOpts False) quickExit QEVersion = return () @@ -161,20 +155,6 @@ coreOpts = where obe = OptBackend . parseBackend -dumpOpts :: Bool -> [OptDescr Opt] -dumpOpts nos = - mkDumpOpt "agg" DumpAgg "Aggregator summary" - ++ mkDumpOpt "anf" DumpANF "Administrative Normal Form" - ++ mkDumpOpt "parse" DumpParsed "Parser output" - where - mkDumpOpt arg fl hm = - Option [] ["dump-" ++ arg] (OptArg (OptDump . sfl) "FILE") hm - : if nos - then [ Option [] ["no-dump-" ++ arg] (NoArg (OptDump cfl)) "" ] - else [] - where - sfl x fs = M.insert fl x fs - cfl fs = M.delete fl fs allOptions :: [OptDescr Opt] allOptions = @@ -208,6 +188,21 @@ procArgs argv = do mungeDump f c = c { dcfg_dumps = f $ dcfg_dumps c } setOutput o c = c { dcfg_outFile = if o == "-" then Nothing else Just o } +------------------------------------------------------------------------}}} +-- Showing DOpAMine {{{ + +renderDopUpds :: BackendRenderDopIter bs e -> UpdateEvalMap bs -> Doc e +renderDopUpds ddi um = vsep $ flip map (M.toList um) $ \(fa,ps) -> + pretty fa `above` indent 2 (vsep $ flip map ps $ \(r,c,vi,vo,act) -> + planHeader r c (vi,vo) `above` indent 2 (printUpdate act)) + where + planHeader r c (vi,vo) = + (prettySpanLoc $ r_span r) <+> text "cost=" <> pretty c <+> + text "in=" <> pretty vi <+> text "out=" <> pretty vo + + printUpdate dop = vsep $ map (renderDOpAMine ddi) dop + + ------------------------------------------------------------------------}}} -- Pipeline! {{{ @@ -234,7 +229,7 @@ processFile fileName = bracket openOut hClose go empty aggm) case dcfg_backend ?dcfg of - Backend be_b be_c be_d -> + Backend be_b be_c be_ddi be_d -> let initializers = MA.mapMaybe (\(f,mca) -> (\(c,a) -> (f,c,a)) `fmap` mca) $ map (\x -> (x, planInitializer be_b x)) frs @@ -245,11 +240,15 @@ processFile fileName = bracket openOut hClose go (flip S.member be_c) x)) frs +{- qPlans = combineQueryPlans $ map (\x -> (x, planGroundBackchain be_b x)) frs +-} - in be_d aggm cPlans qPlans initializers out + in do + dump DumpDopUpd (renderDopUpds be_ddi cPlans) + be_d aggm cPlans {- qPlans -} initializers out parse = do pr <- T.parseFromFileEx (P.rawDLines <* T.eof) fileName @@ -270,6 +269,30 @@ main_ argv = do _ -> dynacSorry "We can't do more than one file" main :: IO () -main = getArgs >>= main_ - +main = catch (getArgs >>= main_) printerr + where + printerr x = pe x >> exitFailure + + pe (UserProgramError d) = do + hPutStrLn stderr "FATAL: Encountered error in input program:" + PP.hPutDoc stderr d + pe (UserProgramANSIError d) = do + hPutStrLn stderr "FATAL: Encountered error in input program:" + PPA.hPutDoc stderr d + pe (InvocationError d) = do + hPutStrLn stderr "Invocation error:" + PP.hPutDoc stderr d + quickExit QEHelp + pe (Sorry d) = do + hPutStrLn stderr "Terribly sorry, but you've hit an unsupported feature" + taMsg + PP.hPutDoc stderr d + pe (Panic d) = do + hPutStrLn stderr "Compiler panic!" + taMsg + PP.hPutDoc stderr d + + taMsg = do + hPutStrLn stderr $ "This is almost assuredly not your fault!" + ++ " Please contact a TA." ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Main/Exception.hs b/src/Dyna/Main/Exception.hs index e9fee66..b39cc98 100644 --- a/src/Dyna/Main/Exception.hs +++ b/src/Dyna/Main/Exception.hs @@ -18,6 +18,8 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PPA ------------------------------------------------------------------------}}} -- Dyna Compiler Exceptions {{{ +-- | When things go badly for us, they go badly in one of these ways, +-- ideally. data DynacException = -- | The user program contains an error UserProgramError (PP.Doc TP.Effect) @@ -41,14 +43,22 @@ instance Exception DynacException ------------------------------------------------------------------------}}} -- Utilities {{{ +-- | Utility function for throwing a document to render dynacUserErr, dynacSorry, dynacPanic :: PP.Doc TP.Effect -> a dynacUserErr = throw . UserProgramError dynacSorry = throw . Sorry dynacPanic = throw . Panic +-- | Throw a panic string +dynacPanicStr :: String -> a +dynacPanicStr = throw . Panic . PP.text + +-- | Throw an ANSI error; this is used inside the parser, primarily, due to +-- trifecta's movement to the ANSI prettyprinter. dynacUserANSIErr :: PPA.Doc -> a dynacUserANSIErr = throw . UserProgramANSIError +-- | A type-restricted version of 'throw' dynacThrow :: DynacException -> a dynacThrow = throw diff --git a/src/Dyna/Main/TestsDriver.hs b/src/Dyna/Main/TestsDriver.hs index 98dcd5e..9c3b7ea 100644 --- a/src/Dyna/Main/TestsDriver.hs +++ b/src/Dyna/Main/TestsDriver.hs @@ -1,9 +1,8 @@ -- | Bring together all of our test suites module Dyna.Main.TestsDriver where -import Data.Monoid import Test.Framework -import qualified Dyna.Analysis.Mode.InstSelftest as DAMI +import qualified Dyna.Analysis.Mode.Selftest as DAMS -- import qualified Dyna.Backend.K3.Selftest as DBK3S import qualified Dyna.Backend.Python.Selftest as DBPS import qualified Dyna.ParserHS.Selftest as DPHS @@ -11,18 +10,12 @@ import qualified Dyna.XXX.TrifectaTests as DXT main :: IO () main = defaultMain - [DPHS.selftest - , DXT.selftest - , moreTries 2000 $ DAMI.selftest + [ DPHS.selftest + , DXT.selftest + , DAMS.selftest -- XXX Until this is meaningful... -- ,DBK3S.selftest - ,DBPS.selftest + , DBPS.selftest ] - -moreTries :: Int -> Test -> Test -moreTries n = plusTestOptions - $ mempty - { topt_maximum_unsuitable_generated_tests = Just n - } diff --git a/src/Dyna/ParserHS/Parser.hs b/src/Dyna/ParserHS/Parser.hs index 99d72b7..94607b1 100644 --- a/src/Dyna/ParserHS/Parser.hs +++ b/src/Dyna/ParserHS/Parser.hs @@ -54,6 +54,7 @@ import qualified Data.ByteString as B import qualified Data.CharSet as CS import qualified Data.Data as D import qualified Data.HashSet as H +import qualified Data.Map as M import Data.Semigroup ((<>)) import Data.Monoid (mempty) import Text.Parser.Expression @@ -90,9 +91,19 @@ data Rule = Rule !RuleIx !(Spanned Term) !B.ByteString !(Spanned Term) -- | Pragmas that are recognized by the parser data Pragma = PDispos !SelfDispos !B.ByteString ![ArgDispos] + | POperAdd !PragmaFixity !Integer !B.ByteString + | POperDel !B.ByteString | PMisc !Term deriving (Eq,Show) +data PragmaFixity = PFIn PAssoc | PFPre | PFPost + deriving (Eq,Show) + +-- XXX This is only necessary until parsers upstream cuts a release in which +-- 'Assoc' is 'Eq' and 'Show'. It's already committed upstream, but... +data PAssoc = PAssocNone | PAssocLeft | PAssocRight + deriving (Eq,Show) + data Line = LRule (Spanned Rule) | LPragma Pragma deriving (Eq,Show) @@ -153,6 +164,7 @@ newtype EOT = EOT { unEOT :: forall m . -- Note that this type is hidden with the exception of some accessors below. data PCS = PCS { _pcs_opertab :: EOT + , _pcs_operspec :: M.Map B.ByteString () -- XXX , _pcs_dispostab :: DisposTab , _pcs_ruleix :: Int } @@ -186,8 +198,9 @@ rs x = get >>= runReaderT x defPCS = PCS { _pcs_dispostab = defDisposTab , _pcs_ruleix = 0 + , _pcs_operspec = M.empty -- XXX , _pcs_opertab = EOT $ - -- | The basic expression table for limited expressions. + -- The basic expression table for limited expressions. -- -- Notably, this excludes @,@ (which is important -- syntactically) and @whenever@ and @is@ (which are @@ -198,11 +211,14 @@ defPCS = PCS { _pcs_dispostab = defDisposTab -- XXX timv suggests that this should be assocnone for -- binops as a quick fix. Eventually we should still do -- this properly. + -- + -- XXX this ought to be derived from the default + -- _pcs_operspec rather than being coded as it is. [ [ Prefix $ uf (spanned $ bsf $ symbol "new") ] - , [ Prefix $ uf (spanned $ bsf $ ident dynaPfxOperStyle) ] - , [ Infix (bf (spanned $ bsf $ ident dynaOperStyle)) AssocLeft ] - , [ Infix (bf (spanned $ bsf $ dotOper)) AssocRight ] - , [ Infix (bf (spanned $ bsf $ commaOper)) AssocRight ] + , [ Prefix $ uf (spanned $ prefixOper ) ] + , [ Infix (bf (spanned $ normOper )) AssocLeft ] + , [ Infix (bf (spanned $ dotOper )) AssocRight ] + , [ Infix (bf (spanned $ commaOper)) AssocRight ] ] } @@ -292,7 +308,7 @@ dynaAtomStyle = IdentifierStyle { _styleName = "Atom" , _styleStart = (lower <|> oneOf "$") , _styleLetter = (alphaNum <|> oneOf "_'") - , _styleReserved = H.fromList [ "is", "new", "whenever" ] + , _styleReserved = H.fromList [ "is", "new", "whenever" ] -- XXX maybe not? , _styleHighlight = Constant , _styleReservedHighlight = ReservedOperator } @@ -360,15 +376,21 @@ thenAny p = anyChar -- some character -- to have not-a-space following (to avoid confusion with the end-of-rule -- marker, which is taken to be "dot space" or "dot eof"). dotOper :: (Monad m, TokenParsing m, LookAheadParsing m) - => m [Char] -dotOper = try (lookAhead (thenAny anyChar) *> identNL dynaDotOperStyle) + => m B.ByteString +dotOper = bsf $ try (lookAhead (thenAny anyChar) *> identNL dynaDotOperStyle) -- | A "comma operator" is a comma necessarily followed by something that -- would continue to be an operator (i.e. punctuation). commaOper :: (Monad m, TokenParsing m, LookAheadParsing m) - => m [Char] -commaOper = try ( lookAhead (thenAny $ _styleLetter dynaCommaOperStyle) - *> identNL dynaCommaOperStyle) + => m B.ByteString +commaOper = bsf $ try ( lookAhead (thenAny $ _styleLetter dynaCommaOperStyle) + *> identNL dynaCommaOperStyle) + +-- | A normal operator is handled by trifecta's built-in handling +normOper = bsf $ ident dynaOperStyle + +-- | Prefix operators also handled by trifecta's built-in handling +prefixOper = bsf $ ident dynaPfxOperStyle uf :: (Monad m, Applicative m) => m (Spanned B.ByteString) @@ -442,8 +464,9 @@ rawDRule = evalStateT (unPCM $ unDL $ spanned parseRule) defPCS -- Pragmas {{{ parsePragma = choice - [ symbol "dispos" *> parseDisposition - -- , symbol "oper" *> parseOper + [ -- symbol "aggr" *> parseAggr -- XXX alternate syntax for aggr + symbol "dispos" *> parseDisposition -- in-place dispositions + , symbol "oper" *> parseOper -- new {pre,in,post}fix oper ] where parseDisposition = PDispos <$> selfdis @@ -459,7 +482,35 @@ parsePragma = choice , pure SDInherit ] - parseOper = undefined + parseOper = choice [ try $ symbol "add" *> parseOperAdd + , try $ symbol "del" *> parseOperDel + , parseOperAdd + ] + + where + parseOperAdd = do + (fx,n) <- fixity + prec <- natural + sym <- n + return $ POperAdd fx prec sym + + parseOperDel = POperDel <$> afx + + fixity = choice [ symbol "pre" *> pure (PFPre, pfx) + , symbol "post" *> pure (PFPost, pfx) + , symbol "in" *> ((,) <$> (PFIn <$> assoc) <*> pure ifx) + ] + + pfx = choice [ prefixOper, dotOper, commaOper, justAtom ] + ifx = choice [ normOper , dotOper, commaOper, justAtom ] + afx = choice [ prefixOper, normOper, dotOper, commaOper, justAtom] + + justAtom = bsf $ ident dynaAtomStyle + + assoc = choice [ symbol "none" *> pure PAssocNone + , symbol "left" *> pure PAssocLeft + , symbol "right" *> pure PAssocRight + ] dpragma :: (DeltaParsing m, LookAheadParsing m, MonadReader PCS m) => m Pragma diff --git a/src/Dyna/ParserHS/Selftest.hs b/src/Dyna/ParserHS/Selftest.hs index 848537c..55c7aed 100644 --- a/src/Dyna/ParserHS/Selftest.hs +++ b/src/Dyna/ParserHS/Selftest.hs @@ -63,6 +63,17 @@ case_basicFunctor = e @=? (term sfb) sfb :: (IsString s) => s sfb = "foo(bar)" +case_dollarFunctor :: Assertion +case_dollarFunctor = e @=? (term sfb) + where + e = TFunctor "$foo" + [TFunctor "bar" [] :~ Span (Columns 5 5) (Columns 8 8) sfb + ] + :~ Span (Columns 0 0) (Columns 9 9) sfb + + sfb :: (IsString s) => s + sfb = "$foo(bar)" + case_nestedFunctorsWithArgs :: Assertion case_nestedFunctorsWithArgs = e @=? (term st) where diff --git a/src/Dyna/Term/Normalized.hs b/src/Dyna/Term/Normalized.hs new file mode 100644 index 0000000..310ec3a --- /dev/null +++ b/src/Dyna/Term/Normalized.hs @@ -0,0 +1,39 @@ +--------------------------------------------------------------------------- +-- | Normalized Term Representations of various forms + +module Dyna.Term.Normalized ( + NT(..), FDT, NTV, EBF, ENF, EVF, +) where + +-- import qualified Data.ByteString as B +import Dyna.Term.TTerm +import qualified Text.PrettyPrint.Free as PP + +------------------------------------------------------------------------}}} +-- Normalized Term Representations {{{ + +-- | A Normalized Term, parametric in the variable case +data NT v = NTVar v + | NTBase TBase + deriving (Eq,Ord,Show) + +instance PP.Pretty v => PP.Pretty (NT v) where + pretty (NTVar v) = PP.pretty v + pretty (NTBase t) = PP.pretty t + +-- | Normalized Term over 'DVar' (that is, either a primitive or a variable) +type NTV = NT DVar + +-- | Flat Dyna Term (that is, a functor over variables) +type FDT = (DFunct,[DVar]) + +-- | Either a base case or flat term +type EBF = Either TBase FDT + +-- | Either a variable or a functor of variables) +type EVF = Either DVar FDT + +-- | Either a constant, another variable, or a flat Dyna term +type ENF = Either NTV FDT + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/XXX/DataUtils.hs b/src/Dyna/XXX/DataUtils.hs index 8aa07c2..42fdc8b 100644 --- a/src/Dyna/XXX/DataUtils.hs +++ b/src/Dyna/XXX/DataUtils.hs @@ -108,7 +108,7 @@ zipWithTails fb fl fr = go mergeWithKey :: Ord k => (k -> a -> b -> Maybe c) -> (M.Map k a -> M.Map k c) -> (M.Map k b -> M.Map k c) -> M.Map k a -> M.Map k b -> M.Map k c mergeWithKey f g1 g2 ml mr = - let ol = g1 (M.difference ml mr) - in let or = g2 (M.difference mr ml) + let xl = g1 (M.difference ml mr) + in let xr = g2 (M.difference mr ml) in let mb = M.mapMaybe id $ M.intersectionWithKey f ml mr - in M.unions [ol,or,mb] + in M.unions [xl,xr,mb] diff --git a/src/Dyna/XXX/MonadContext.hs b/src/Dyna/XXX/MonadContext.hs index 96215e3..c026669 100644 --- a/src/Dyna/XXX/MonadContext.hs +++ b/src/Dyna/XXX/MonadContext.hs @@ -2,13 +2,24 @@ -- | Class definitions for "context" monads. -- Header material {{{ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeFamilies #-} module Dyna.XXX.MonadContext( - MCVT, MCA(..), MCD(..), MCF(..), MCM(..), MCN(..), MCR(..), MCW(..), + MCVT, MCA(..), MCD(..), MCF(..), MCM(..), MCNC, MCN(..), MCR(..), MCW(..), ) where +import GHC.Prim (Constraint) +-- import Control.Monad.Trans +-- import Control.Monad.Trans.Either + +------------------------------------------------------------------------}}} +-- Fine-grained context classes {{{ + type family MCVT (m :: * -> *) (k :: *) :: * -- | The monad @m@ has a readable context of type @k -> v@ @@ -20,18 +31,29 @@ class (Monad m) => MCW m k where cassign :: k -> MCVT m k -> m () -- | The monad @m@ is able to merge the assertion @k = v@ into --- its context, provided a mechanism to merge values, if necessary. +-- its context, provided a mechanism to merge values. class (Monad m) => MCM m k where - cmerge :: (MCVT m k -> MCVT m k -> m (MCVT m k)) -> k -> (MCVT m k) -> m () + cmerge :: (MCVT m k -> b -> m (MCVT m k)) + -> k -> b -> m () -- | It is possible to delete keys of type @k@ from the context @m@. class (Monad m) => MCD m k where cdelete :: k -> m (MCVT m k) --- | The monad @m@ is able to fabricate new keys given only a value. --- This is likely especially useful when @m@ is 'MonadFix'. +{- +class (Monad m) => MCN m k where + -- XXX OLD FORM cnew :: (MCVT m k) -> m k + cnew :: (k -> m (MCVT m k)) -> m k +-} + +type family MCNC k (m' :: * -> *) :: Constraint + +-- | The monad @m@ is able to fabricate new keys given a function +-- which can produce a value from a key. Likely, an instance of 'MCN' +-- will require 'MonadFix', but not always; that's the purpose of 'MCNC'. class (Monad m) => MCN m k where - cnew :: (MCVT m k) -> m k + cnew :: (Monad m', MCNC k m') + => (forall a . m a -> m' a) -> (k -> m' (MCVT m k)) -> m' k -- | The monad @m@ is able to generate new entities of type @k@. class (Monad m) => MCF m k where @@ -47,3 +69,19 @@ class (Monad m) => MCA m k where -- object (which need not be either of the inputs, if they -- themselves were aliased, for example). calias :: (MCVT m k -> MCVT m k -> m (MCVT m k)) -> k -> k -> m k + +------------------------------------------------------------------------}}} +-- Context Transformers {{{ + +{- +type instance MCVT (EitherT e m) k = MCVT m k + +instance (MCR m k) => MCR (EitherT e m) k where + clookup k = lift (clookup k) + +instance (MCW m k) => MCW (EitherT e m) k where + cassign k v = lift (cassign k v) +-} + +------------------------------------------------------------------------}}} + diff --git a/vimrc b/vimrc new file mode 100644 index 0000000..8e5ad90 --- /dev/null +++ b/vimrc @@ -0,0 +1,3 @@ +"Run "vim -S vimrc" to source this file and apply project-specific settings + +let g:hdevtools_options = '-g-isrc' -- 2.50.1