diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,6 @@ + +# Revision history for huff + +## 0.1.0.0 + +* Initial release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2015, Trevor Elliott + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Trevor Elliott nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,73 @@ +Huff +==== + +Huff is an implementation of the fast-forward forward-chaining planner in +Haskell. The main interface is the quasi-quoter `huff`, which allows the user to +define re-usable domains that can be used with the planner to solve different +problems. + + +Example +------- + +Consider the blocks world planning domain from [Chapter +11](http://aima.cs.berkeley.edu/2nd-ed/newchap11.pdf) of "Artificial +Intelligence: A Modern Approach". The domain includes two actions, `Move` and +`MoveToTable`, four objects, `A`, `B`, `C`, `Table`, and two predicates, `On` +and `Clear`. Embedding the domain in Haskell using `huff` looks like this: + +```haskell +module Main where + +import Huff + +[huff| + + domain BlocksWorld { + object Obj = A | B | C | Table + + predicate on(Obj,Obj), clear(Obj) + + operator Move(b: Obj, x: Obj, y: Obj) { + requires: on(b,x), clear(b), clear(y) + effect: on(b,y), clear(x), !clear(y) + } + + operator MoveToTable(b: Obj, x: Obj) { + requires: on(b,x), clear(b) + effect: on(b,Table), clear(x) + } + } + +|] + +``` + +The quasi-quoter will introduce five new declarations: +* A data declaration for the `Obj` object +* A data declaration for the `BlocksWorld` domain, that will consist of two + constructors `Move :: Obj -> Obj -> Obj -> BlocksWorld` and `MoveToTable :: + Obj -> Obj -> BlocksWorld` +* Two classes called `Has_on` and `Has_clear`, that define the `on` and `clear` + functions, respectively +* The `blocksWorld` function of the type `[Literal] -> Term -> Spec BlocksWorld` + +The `blocksWorld` function accepts the initial state and goal, and produces a +`Spec BlocksWorld` value that can be used in conjunction with the `findPlan` +function to attempt to find a plan. For example, the problem specified in +chapter 11 Russel and Norvig can be solved as follows: + +```haskell +main = + do mb <- findPlan $ blocksWorld [ on A Table, on B Table, on C Table, clear A + , clear B, clear C ] + [on A B, n B C] + print mb +``` + +Running the example will produce the output: + +```shell +$ find dist-newstyle -name blocksWorld -type f -exec {} \; +Just [MoveTo B Table C, MoveTo A Table B] +``` diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/BlocksWorld.hs b/examples/BlocksWorld.hs new file mode 100644 --- /dev/null +++ b/examples/BlocksWorld.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE QuasiQuotes #-} + +module Main where + +import Huff + +[huff| + + domain BlocksWorld { + + object Obj = A | B | C | Table + + predicate on(Obj,Obj), clear(Obj) + + operator MoveTo(b: Obj, x: Obj, y: Obj) { + requires: on(b,x), clear(b), clear(y) + effect: on(b,y), clear(x), !clear(y) + } + + operator MoveToTable(b: Obj, x: Obj) { + requires: on(b,x), clear(b) + effect: on(b,Table), clear(x) + } + } + +|] + +main = + do mb <- findPlan $ blocksWorld [ on A Table, on B Table, on C Table + , clear A, clear B, clear C ] + [ on A B, on B C ] + + print mb diff --git a/huff.cabal b/huff.cabal new file mode 100644 --- /dev/null +++ b/huff.cabal @@ -0,0 +1,67 @@ +name: huff +version: 0.1.0.0 +synopsis: A fast-foward-based planner +license: BSD3 +license-file: LICENSE +author: Trevor Elliott +maintainer: awesomelyawesome@gmail.com +category: AI +build-type: Simple +cabal-version: >=1.10 + +homepage: https://github.com/elliottt/huff +bug-reports: https://github.com/elliottt/huff/issues +tested-with: GHC == 8.0.1 + +extra-source-files: README.md + CHANGELOG.md + +description: + An implementation of the fast-forward planner, as a quasi-quoter. + +source-repository head + type: git + location: git://github.com/elliottt/huff.git + branch: master + +flag examples + default: False + description: Build the examples + +library + exposed-modules: Huff + + other-modules: Huff.Compile + Huff.Compile.AST + Huff.Compile.Operators + Huff.Compile.Problem + Huff.ConnGraph + Huff.FF.Extract + Huff.FF.Fixpoint + Huff.FF.Planner + Huff.Input + Huff.QQ + Huff.QQ.Lexer + Huff.QQ.Parser + + build-tools: alex + + build-depends: base >=4.9 && <5, + alex-tools, + containers, + heaps, + hashable, + unordered-containers, + text, + array, + template-haskell + + hs-source-dirs: src + default-language: Haskell2010 + +executable blocksWorld + hs-source-dirs: examples + main-is: BlocksWorld.hs + build-depends: base >= 4.9 && < 5, + huff + default-language: Haskell2010 diff --git a/src/Huff.hs b/src/Huff.hs new file mode 100644 --- /dev/null +++ b/src/Huff.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE QuasiQuotes #-} + +module Huff ( + huff, + Spec, + Domain(), + Problem(), + Literal(), + Term(), + module Huff + ) where + +import Huff.Compile.AST (Problem,Term(..),Literal(..)) +import Huff.Input (Spec,Domain,Operator(..)) +import Huff.QQ (huff) +import qualified Huff.FF.Planner as FF + +import Data.Maybe (mapMaybe) + +infixr 3 /\ + +(/\) :: Term -> Term -> Term +p /\ q = TAnd [p,q] + +infixr 4 \/ + +(\/) :: Term -> Term -> Term +p \/ q = TOr [p,q] + +imply :: Term -> Term -> Term +imply = TImply + +class Has_neg a where + neg :: a -> a + +instance Has_neg Literal where + neg (LAtom a) = LNot a + neg (LNot a) = LAtom a + +instance Has_neg Term where + neg = TNot + + +findPlan :: Spec a -> IO (Maybe [a]) +findPlan (prob,dom) = + do mb <- FF.findPlan prob dom + case mb of + Just xs -> return (Just (mapMaybe opVal (FF.resSteps xs))) + Nothing -> return Nothing diff --git a/src/Huff/Compile.hs b/src/Huff/Compile.hs new file mode 100644 --- /dev/null +++ b/src/Huff/Compile.hs @@ -0,0 +1,103 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Huff.Compile ( + compileOperators, + compileProblem, + extractPlan, + module Huff.Compile.AST, + ) where + +import Huff.Compile.AST +import Huff.Compile.Operators +import Huff.Compile.Problem +import qualified Huff.Input as I + +import Data.Maybe (mapMaybe) +import qualified Data.Set as Set +import qualified Data.Text as T + + +-- | Compile operators, but leave off the negation removal step, which must be +-- done in the presence of the problem. The benefit to doing things this way, is +-- that this step can be done at compile time with template-haskell, and the +-- less-complicated negation removal step can be done at runtime, once the +-- problem is known. +compileOperators :: ([Name] -> a -> b) -> TypeMap Name -> [Operator a] -> [Operator b] +compileOperators adjust types ops = + do op <- ops + (env,args,op') <- expandActions types op + let op'' = op' { opVal = adjust args `fmap` opVal op' } + removeDisjunction (removeQuantifiers types env op'') + + +-- | Compile a problem, in the context of the domain. +compileProblem :: TypeMap Name -> [Operator a] -> Problem -> (I.Problem,I.Domain a) +compileProblem types ops prob = (transProblem prob'', I.Domain (map transOperator ops')) + where + (prob',goalOp) = genProblemOperators prob + (negs,ops') = removeNegation (compileOperators adjust types [goalOp] ++ ops) + prob'' = addNegativePreconditions negs prob' + + adjust _ _ = undefined + + +extractPlan :: [I.Operator a] -> [a] +extractPlan = mapMaybe I.opVal + +transProblem :: Problem -> I.Problem +transProblem Problem { .. } = + I.Problem { I.probInit = [ transAtom a | LAtom a <- probInit ] + , I.probGoal = transPre probGoal + } + +transDomain :: Domain a -> I.Domain a +transDomain Domain { .. } = + I.Domain { I.domOperators = map transOperator domOperators } + +transOperator :: Operator a -> I.Operator a +transOperator op @ Operator { .. } = + I.Operator { I.opName = opName + , I.opPre = transPre opPrecond + , I.opEffects = transEff opEffects + , I.opVal = opVal + } + +transPre :: Term -> [I.Fact] +transPre (TAnd ts) = concatMap transPre ts +transPre (TLit (LAtom a)) = [transAtom a] +transPre _ = error "transTerm" + +transEff :: Effect -> [I.Effect] +transEff eff = simple ++ conditional + where + (lits,conds) = splitEffs eff + + simple | null lits = [] + | otherwise = [ foldl addEffect emptyEffect lits ] + + conditional = + [ foldl addEffect eff' q | (p,q) <- conds + , let eff' = emptyEffect { I.ePre = transPre p } ] + + emptyEffect = I.Effect { I.ePre = [], I.eAdd = [], I.eDel = [] } + + addEffect e (LAtom a) = e { I.eAdd = transAtom a : I.eAdd e } + addEffect e (LNot a) = e { I.eDel = transAtom a : I.eDel e } + +-- | Partition an effect into its simple, and conditional effects. +splitEffs :: Effect -> ([Literal],[(Term,[Literal])]) +splitEffs eff = go [] [] (elimEAnd eff) + where + go ls cs (EWhen p q : rest) = go ls ((p,q):cs) rest + go ls cs (ELit l : rest) = go (l:ls) cs rest + go ls cs [] = (ls,cs) + go _ _ _ = error "splitEffs" + +transAtom :: Atom -> I.Fact +transAtom (Atom a as) = I.Fact a (map transArg as) + +transArg :: Arg -> T.Text +transArg (AName n) = n +transArg _ = error "transArg" diff --git a/src/Huff/Compile/AST.hs b/src/Huff/Compile/AST.hs new file mode 100644 --- /dev/null +++ b/src/Huff/Compile/AST.hs @@ -0,0 +1,126 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveTraversable #-} + +module Huff.Compile.AST where + +import Data.Foldable (foldMap) +import qualified Data.Map.Strict as Map +import Data.Monoid (Monoid(..)) +import qualified Data.Text as T + + +data Domain a = Domain { domName :: T.Text + , domObjects :: [Object] + , domPreds :: [Pred] + , domOperators :: [Operator a] + } deriving (Show) + +data Problem = Problem { probInit :: [Literal] + , probGoal :: Term + } deriving (Show) + +data Operator a = Operator { opName :: !T.Text + , opDerived :: !Bool + , opParams :: [Param] + , opVal :: Maybe a + , opPrecond :: Term + , opEffects :: Effect + } deriving (Show,Functor,Foldable,Traversable) + +type Name = T.Text + +type Type = T.Text + +data Typed a = Typed { tValue :: a + , tType :: !Type + } deriving (Show,Eq,Ord) + +-- | Types and all their inhabitants. +newtype TypeMap a = TypeMap { getTypeMap :: Map.Map Type [a] + } deriving (Show) + +instance Monoid (TypeMap a) where + mempty = + TypeMap mempty + + mappend (TypeMap a) (TypeMap b) = + TypeMap (Map.unionWith (++) a b) + +typeMap :: [Typed a] -> TypeMap a +typeMap = foldMap (\ Typed { .. } -> TypeMap (Map.singleton tType [tValue]) ) + +lookupType :: Type -> TypeMap a -> [a] +lookupType k (TypeMap m) = Map.findWithDefault [] k m + + +type Param = Typed Name +type Object = Typed Name + +data Term = TAnd [Term] + | TOr [Term] + | TNot !Term + | TImply !Term !Term + | TExists [Param] !Term + | TForall [Param] !Term + | TLit !Literal + deriving (Show) + +mkTAnd :: [Term] -> Term +mkTAnd [t] = t +mkTAnd ts = TAnd ts + +mkTOr :: [Term] -> Term +mkTOr [t] = t +mkTOr ts = TOr ts + +data Effect = EForall [Param] Effect + | EWhen Term [Literal] + | EAnd [Effect] + | ELit Literal + deriving (Show) + +mkEWhen :: [Term] -> [Literal] -> Effect +mkEWhen [] = mkELitConj +mkEWhen ps = EWhen (mkTAnd ps) + +mkELitConj :: [Literal] -> Effect +mkELitConj xs = EAnd (map ELit xs) + +mkEAnd :: [Effect] -> Effect +mkEAnd [e] = e +mkEAnd es = EAnd es + +elimEAnd :: Effect -> [Effect] +elimEAnd (EAnd es) = concatMap elimEAnd es +elimEAnd e = [e] + +isELit :: Effect -> Bool +isELit ELit{} = True +isELit _ = False + +data Literal = LAtom Atom + | LNot Atom + deriving (Show) + +data App a = App !Name [a] + deriving (Show,Eq,Ord) + +type Atom = App Arg + +pattern Atom n as = App n as + +negAtom :: Atom -> Atom +negAtom (Atom a as) = Atom (T.append "$not-" a) as + +type Pred = App Type + +pattern Pred n ts = App n ts + +data Arg = AName !Name + | AVar !Name + deriving (Show,Eq,Ord) diff --git a/src/Huff/Compile/Operators.hs b/src/Huff/Compile/Operators.hs new file mode 100644 --- /dev/null +++ b/src/Huff/Compile/Operators.hs @@ -0,0 +1,278 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} + +module Huff.Compile.Operators ( + expandActions, + removeQuantifiers, + removeDisjunction, + removeNegation, + ArgEnv, + ) where + +import Huff.Compile.AST + +import Control.Monad (msum) +import Data.Foldable (foldMap) +import qualified Data.Map.Strict as Map +import Data.Monoid (mappend) +import qualified Data.Set as Set +import qualified Data.Text as T + + +-- Expand Actions -------------------------------------------------------------- + +-- | Expand out instances of an operator, based on the types of its parameters. +-- This is similar to the case of existential elimination covered lower down. +expandActions :: TypeMap Name -> Operator a -> [(ArgEnv,[Name],Operator a)] +expandActions types op @ Operator { .. } + + | null opParams = + return (Map.empty, [], op) + + | otherwise = + do (env,args) <- params opParams + let op' = Operator { opName = T.intercalate "-" (opName : args) + , opDerived = True + , opParams = [] + , .. + } + return (env, args, op') + + where + + params (Typed { .. } : ps) = + do (env,args) <- params ps + e <- lookupType tType types + return (Map.insert tValue (AName e) env, e : args) + + params [] = return (Map.empty, []) + + +-- Quantifiers ----------------------------------------------------------------- + +-- | Remove quantifiers used in the preconditions and effects of an operator, by +-- turning forall into conjuction, and exists into disjunction. +-- +-- INVARIANT: This stage removes the TForall and TExists constructors from the +-- pre and post conditions. +removeQuantifiers :: TypeMap Name -> ArgEnv -> Operator a -> Operator a +removeQuantifiers types env Operator { .. } = + Operator { opPrecond = rqTerm types env opPrecond + , opEffects = rqEff types env opEffects + , .. + } + +type ArgEnv = Map.Map Name Arg + +-- | Remove quantifiers from effects. +rqEff :: TypeMap Name -> ArgEnv -> Effect -> Effect +rqEff types env0 = EAnd . go env0 + where + go env (EForall xs e) = + do env' <- params xs env + go env' e + + go env (EAnd es) = + EAnd `fmap` mapM (go env) es + + go env (EWhen p qs) = + return (EWhen (rqTerm types env p) (map (substLit env) qs)) + + go env (ELit l) = + return (ELit (substLit env l)) + + params (Typed { .. } : ps) env = + do e <- lookupType tType types + params ps (Map.insert tValue (AName e) env) + params [] env = return env + +-- | Remove quantifiers from terms. +rqTerm :: TypeMap Name -> ArgEnv -> Term -> Term +rqTerm types = go + where + go env (TAnd ts) = TAnd (map (go env) ts) + go env (TOr ts) = TOr (map (go env) ts) + go env (TNot t) = TNot (go env t) + go env (TImply p q) = TImply (go env p) (go env q) + go env (TForall xs p) = TAnd [ go env' p | env' <- params xs env ] + go env (TExists xs p) = TOr [ go env' p | env' <- params xs env ] + go env (TLit a) = TLit (substLit env a) + + params (Typed { .. } : ps) env = + do e <- lookupType tType types + params ps (Map.insert tValue (AName e) env) + + params [] env = return env + +substLit :: ArgEnv -> Literal -> Literal +substLit env (LNot a) = LNot (substAtom env a) +substLit env (LAtom a) = LAtom (substAtom env a) + +substAtom :: ArgEnv -> Atom -> Atom +substAtom env (Atom s as) = Atom s (map subst as) + where + subst arg = case arg of + AName _ -> arg + AVar n -> Map.findWithDefault arg n env + + +-- Disjunctive Preconditions --------------------------------------------------- + +-- | Generate multiple operators, corresponding to which branch of the +-- disjunction was found to be true. +-- +-- INVARIANT: This stage removes the TOr, TNot, and TImply constructors. +removeDisjunction :: Operator a -> [Operator a] +removeDisjunction Operator { .. } = + case rdOper of + [res] -> return (mkOper res) + _ -> zipWith mkNewOper [1 ..] rdOper + where + + rdOper = do pre <- rdTerm (nnfTerm opPrecond) + eff <- rdEffect (nnfEffect opEffects) + return (pre,eff) + + mkNewOper ix res = + (mkOper res) { opName = T.concat [ opName, "-", T.pack (show (ix :: Int)) ] } + + + mkOper (pre,eff) = + Operator { opPrecond = pre + , opEffects = eff + , opDerived = True + , .. } + +-- | Remove disjunctions, by producing multiple terms. +rdTerm :: Term -> [Term] +rdTerm (TAnd ts) = TAnd `fmap` mapM rdTerm ts +rdTerm (TOr ts) = msum (map rdTerm ts) +rdTerm a@TLit{} = return a +rdTerm TNot{} = error "rdTerm: TNot" +rdTerm TImply{} = error "rdTerm: TImply" +rdTerm TExists{} = error "rdTerm: TExists" +rdTerm TForall{} = error "rdTerm: TForall" + +rdEffect :: Effect -> [Effect] +rdEffect (EWhen t q) = do p <- rdTerm t + return (EWhen p q) +rdEffect (EAnd es) = EAnd `fmap` map rdEffect es +rdEffect e@ELit{} = return e +rdEffect EForall{} = error "nnfEffect: EForall" + +-- | Put a term in negation normal form, pushing all negations down to the +-- literals. +-- +-- INVARIANT: This stage removes the TNot constructor by pushing all negations +-- down to the TLit leaves, and the TImply constructor by translating it to +-- disjunction and negation. +nnfTerm :: Term -> Term + +nnfTerm (TNot (TNot t)) = nnfTerm t +nnfTerm (TNot (TAnd ts)) = TOr (map (nnfTerm . TNot) ts) +nnfTerm (TNot (TOr ts)) = TAnd (map (nnfTerm . TNot) ts) +nnfTerm (TNot (TImply p q)) = TAnd [nnfTerm p, nnfTerm (TNot q)] +nnfTerm (TNot (TLit l)) = TLit (negLit l) + +nnfTerm (TAnd ts) = TAnd (map nnfTerm ts) +nnfTerm (TOr ts) = TOr (map nnfTerm ts) +nnfTerm (TImply p q) = TOr [ nnfTerm (TNot p) , nnfTerm q ] + +nnfTerm t@TLit{} = t + +nnfTerm (TNot TForall{}) = error "nnfTerm: TForall" +nnfTerm (TNot TExists{}) = error "nnfTerm: TExists" +nnfTerm TForall{} = error "nnfTerm: TForall" +nnfTerm TExists{} = error "nnfTerm: TExists" + +nnfEffect :: Effect -> Effect +nnfEffect (EWhen p q) = EWhen (nnfTerm p) q +nnfEffect (EAnd es) = EAnd (map nnfEffect es) +nnfEffect e@ELit{} = e +nnfEffect EForall{} = error "nnfEffect: EForall" + +-- | Negate a literal +negLit :: Literal -> Literal +negLit (LAtom a) = LNot a +negLit (LNot a) = LAtom a + + +-- Negation -------------------------------------------------------------------- + +-- | Remove negations through the addition of special `not` predicates. These +-- generated predicates have the same structure as their counterparts, but imply +-- the presence of the negated effect. +-- +-- INVARIANT: This stage removes all negative literals from the preconditions of +-- operators and conditional effects, replacing them with other literals that +-- correspond to their negation. +removeNegation :: [Operator a] -> (Set.Set Atom, [Operator a]) +removeNegation ops + | Set.null negs = (Set.empty, ops) + | otherwise = (negs, map (cnOper negs) ops) + where + + -- the set of predicates that are are used as negative preconditions + negs = foldMap negPreconds ops + + +negPreconds :: Operator a -> Set.Set Atom +negPreconds Operator { .. } = mappend (negTerms opPrecond) + (negEffects opEffects) + +negTerms :: Term -> Set.Set Atom +negTerms (TAnd ts) = foldMap negTerms ts +negTerms (TLit (LNot a)) = Set.singleton a +negTerms TLit{} = Set.empty +negTerms TNot{} = error "negTerms: TNot" +negTerms TForall{} = error "negTerms: TForall" +negTerms TExists{} = error "negTerms: TExists" +negTerms TOr{} = error "negTerms: TOr" +negTerms TImply{} = error "negTerms: TImply" + +-- | The set of atoms used as negative preconditions for conditional effects. +negEffects :: Effect -> Set.Set Atom +negEffects (EAnd es) = foldMap negEffects es +negEffects (EWhen p _) = negTerms p +negEffects _ = Set.empty + + +cnOper :: Set.Set Atom -> Operator a -> Operator a +cnOper negs Operator { .. } = + Operator { opPrecond = cnTerms opPrecond + , opEffects = cnEffects negs opEffects + , .. } + +-- | Convert all dependencies on !p to dependencies on not-p. +cnTerms :: Term -> Term +cnTerms (TAnd ts) = TAnd (map cnTerms ts) +cnTerms (TLit l) = TLit (cnLiteral l) +cnTerms TNot{} = error "cnTerm: TNot" +cnTerms TForall{} = error "cnTerm: TForall" +cnTerms TExists{} = error "cnTerm: TExists" +cnTerms TOr{} = error "cnTerm: TOr" +cnTerms TImply{} = error "cnTerm: TImply" + +cnEffects :: Set.Set Atom -> Effect -> Effect +cnEffects negs = go + where + go (EAnd es) = EAnd (map go es) + go (EWhen p ls) = EWhen (cnTerms p) (concatMap adjust ls) + go (ELit l) = mkEAnd (map ELit (adjust l)) + go _ = error "cnEffects" + + -- this is an add effect, so assert the atom, and delete its negated version + adjust l@(LAtom a) + | a `Set.member` negs = [ l, LNot (negAtom a) ] + + -- this is a delete effect, so remove the atom, and assert its negated version + adjust l@(LNot a) + | a `Set.member` negs = [ l, LAtom (negAtom a) ] + + adjust l = [l] + +-- | Convert negative literals to positive ones of the form ``$not-p''. +cnLiteral :: Literal -> Literal +cnLiteral (LNot a) = LAtom (negAtom a) +cnLiteral l = l diff --git a/src/Huff/Compile/Problem.hs b/src/Huff/Compile/Problem.hs new file mode 100644 --- /dev/null +++ b/src/Huff/Compile/Problem.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} + +module Huff.Compile.Problem ( + genProblemOperators, + addNegativePreconditions, + ) where + +import Huff.Compile.AST + +import qualified Data.Set as Set + + +-- | Generate operators from the problem description. This corresponds to the +-- "Initial Conditions and Goals" section. +genProblemOperators :: Problem -> (Problem, Operator a) +genProblemOperators Problem { .. } = (prob, goalOp) + where + + goalAtom = LAtom (Atom "$goal-achieved" []) + + prob = Problem { probGoal = TLit goalAtom + , .. + } + + goalOp = Operator { opName = "$goal-operator" + , opDerived = True + , opParams = [] + , opPrecond = probGoal + , opEffects = ELit goalAtom + , opVal = Nothing + } + + +-- | Modify the initial state to include assumptions about negative +-- preconditions. +addNegativePreconditions :: Set.Set Atom -> Problem -> Problem +addNegativePreconditions negs Problem { .. } = + Problem { probInit = initNegs negs probInit, .. } + + +-- | Generate the initial state, given the set of atoms that show up as negative +-- preconditions, and the existing initial state. +initNegs :: Set.Set Atom -> [Literal] -> [Literal] + +-- pass non-negative atoms through, that are mentioned in the initial state +initNegs negs (LAtom a : ls) + | a `Set.member` negs = LAtom a : initNegs (Set.delete a negs) ls + | otherwise = LAtom a : initNegs negs ls + +-- we can safely remove negative initial conditions that aren't used as negative +-- preconditions +initNegs negs (LNot a : ls) + | a `Set.member` negs = LAtom (negAtom a) : initNegs (Set.delete a negs) ls + | otherwise = initNegs (Set.delete a negs) ls + +-- the remaining set of atoms are depended on as negative preconditions, but +-- unset in the initial state. their negative variants are set. +initNegs negs [] = + [ LAtom (negAtom a) | a <- Set.toList negs ] diff --git a/src/Huff/ConnGraph.hs b/src/Huff/ConnGraph.hs new file mode 100644 --- /dev/null +++ b/src/Huff/ConnGraph.hs @@ -0,0 +1,407 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ParallelListComp #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecursiveDo #-} + +module Huff.ConnGraph ( + -- * Connection Graph + ConnGraph() + , resetConnGraph + , buildConnGraph + , IsNode(..) + + -- ** Facts + , Fact() + , markTrue, isTrue + , markGoal, isGoal + , requiresFact + , addsFact + , delsFact + + -- ** Effects + , Effect() + , isInPlan, markInPlan + , activatePrecondition + , effectAdds + , effectDels + , effectPre + , effectOp + + , Level + + , State, applyEffect + , Goals + , Facts + , Effects + + -- * Debugging + , printConnGraph + , printEffects, printEffect + , printFacts, printFact + ) where + +import qualified Huff.Input as I + +import Control.Monad (zipWithM,foldM,unless) +import Data.Function (on) +import Data.Hashable (Hashable(..)) +import Data.IORef + (IORef,newIORef,readIORef,writeIORef,atomicModifyIORef') +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Data.Text as T + + +-- Connection Graph ------------------------------------------------------------ + +type Facts a = Set.Set (Fact a) +type Goals a = Set.Set (Fact a) +type State a = Set.Set (Fact a) +type Effects a = Set.Set (Effect a) + +type Level = Int + +data ConnGraph a = ConnGraph { cgFacts :: !(Facts a) + , cgEffects :: !(Effects a) + , cgDirtyFacts :: !(IORef [Fact a]) + , cgDirtyEffects :: !(IORef [Effect a]) + } + + +data Fact a = Fact { fId :: !Int + , fProp :: !I.Fact + , fLevel :: !(IORef (Maybe Level)) + + , fIsTrue:: !(IORef (Maybe Level)) + , fIsGoal:: !(IORef Bool) + + , fDirty :: !(IORef Bool) + , fDirtyList :: !(IORef [Fact a]) + + , fPreCond :: Effects a + -- ^ Effects that require this fact + , fAdd :: Effects a + -- ^ Effects that add this fact + , fDel :: Effects a + -- ^ Effects that delete this fact + } + +instance Show (Fact a) where + showsPrec p Fact { .. } = showParen (p >= 10) + $ showString "Fact " + . shows fId + . showString " " + . showParen True (shows fProp) + +instance Hashable (Fact a) where + hashWithSalt s Fact { .. } = hashWithSalt s fId + +markTrue :: Fact a -> Level -> IO () +markTrue f l = + do dirty f + writeIORef (fIsTrue f) (Just l) + +isTrue :: Fact a -> IO (Maybe Level) +isTrue Fact { .. } = readIORef fIsTrue + + +markGoal :: Fact a -> IO () +markGoal f = + do dirty f + writeIORef (fIsGoal f) True + +isGoal :: Fact a -> IO Bool +isGoal Fact { .. } = readIORef fIsGoal + + +instance Eq (Fact a) where + (==) = (==) `on` fId + (/=) = (/=) `on` fId + {-# INLINE (==) #-} + {-# INLINE (/=) #-} + +instance Ord (Fact a) where + compare = compare `on` fId + {-# INLINE compare #-} + +data Effect a = Effect { eId :: !Int + , ePre :: Facts a + , eNumPre :: !Int + , eAdds :: Facts a + , eDels :: Facts a + , eOp :: !(I.Operator a) + -- ^ The operator that this effect came from + + , eDirty :: !(IORef Bool) + , eDirtyList :: !(IORef [Effect a]) + + , eInPlan :: !(IORef Bool) + -- ^ Whether or not this effect is a member of the + -- current relaxed plan + + , eIsInH :: !(IORef Bool) + -- ^ If this action is part of the helpful action set + + , eLevel :: !(IORef (Maybe Level)) + -- ^ Membership level for this effect + , eActivePre :: !(IORef Level) + -- ^ Active preconditions for this effect + } + +instance Show (Effect a) where + showsPrec p Effect { .. } = showParen (p >= 10) + $ showString "Effect: " + . showParen True (shows eId) + + +markInPlan :: Effect a -> IO () +markInPlan e = + do dirty e + writeIORef (eInPlan e) True + +isInPlan :: Effect a -> IO Bool +isInPlan Effect { .. } = readIORef eInPlan + +effectOp :: Effect a -> I.Operator a +effectOp Effect { .. } = eOp + + +instance Eq (Effect a) where + (==) = (==) `on` eId + (/=) = (/=) `on` eId + {-# INLINE (==) #-} + {-# INLINE (/=) #-} + +instance Ord (Effect a) where + compare = compare `on` eId + {-# INLINE compare #-} + + +-- Node Operations ------------------------------------------------------------- + +class IsNode node where + dirty :: node a -> IO () + activate :: node a -> Level -> IO () + getLevel :: node a -> IO (Maybe Level) + +instance IsNode Fact where + dirty f = + do isDirty <- readIORef (fDirty f) + unless isDirty (atomicModifyIORef' (fDirtyList f) (\fs -> (f:fs, ()))) + + activate f l = + do dirty f + writeIORef (fLevel f) (Just l) + + getLevel Fact { .. } = readIORef fLevel + +instance IsNode Effect where + dirty e = + do isDirty <- readIORef (eDirty e) + unless isDirty (atomicModifyIORef' (eDirtyList e) (\xs -> (e:xs, ()))) + + activate e l = + do dirty e + writeIORef (eLevel e) (Just l) + + getLevel Effect { .. } = readIORef eLevel + + +-- | The effects that have this fact as a precondition. +requiresFact :: Fact a -> Effects a +requiresFact Fact { .. } = fPreCond + +-- | The effects that add this fact to the state. +addsFact :: Fact a -> Effects a +addsFact Fact { .. } = fAdd + +-- | The effects that delete this fact from the state. +delsFact :: Fact a -> Effects a +delsFact Fact { .. } = fDel + +-- | Increment the number of activated preconditions, and return a boolean that +-- indicates whether or not the effect has been activated. +activatePrecondition :: Effect a -> IO Bool +activatePrecondition eff = + do dirty eff + atomicModifyIORef' (eActivePre eff) $ \ n -> + let n' = n + 1 + in (n', n' >= eNumPre eff) + +effectAdds :: Effect a -> Facts a +effectAdds Effect { .. } = eAdds +{-# INLINE effectAdds #-} + +effectDels :: Effect a -> Facts a +effectDels Effect { .. } = eDels +{-# INLINE effectDels #-} + +effectPre :: Effect a -> Facts a +effectPre Effect { .. } = ePre +{-# INLINE effectPre #-} + + +-- Utility Functions ----------------------------------------------------------- + +-- | Apply an effect to the state given, returning a new state. +applyEffect :: Effect a -> State a -> State a +applyEffect Effect { .. } s = (s Set.\\ eDels) `Set.union` eAdds + + +-- Input Processing ------------------------------------------------------------ + +-- | Translate a domain and problem into a description of the initial state, the +-- goal state, and the connection graph. The translation process includes +-- adding a special empty fact that all effects with no preconditions will have +-- as a precondition. The empty fact is also added to the initial state, in the +-- event that the problem has an empty initial state. +buildConnGraph :: I.Domain a -> I.Problem -> IO (State a,Goals a,ConnGraph a) +buildConnGraph dom prob = + do cgDirtyFacts <- newIORef [] + cgDirtyEffects <- newIORef [] + + rec (pres,adds,dels,effs) <- + foldM (mkEffect cgDirtyEffects emptyFact factMap) + (Map.empty,Map.empty,Map.empty,[]) allEffs + + emptyFact <- mkFact cgDirtyFacts pres adds dels 0 (I.Fact "" []) + + facts <- zipWithM (mkFact cgDirtyFacts pres adds dels) [1 ..] allFacts + let factMap = Map.fromList (zip allFacts facts) + + + let resolveFacts fs = Set.fromList (map (factMap Map.!) fs) + + -- translate the initial state and goal + state = Set.insert emptyFact (resolveFacts (I.probInit prob)) + goal = resolveFacts (I.probGoal prob) + + cgFacts = Set.fromList facts + cgEffects = Set.fromList effs + + + return (state, goal, ConnGraph { .. }) + + where + + -- all ground facts + allFacts = Set.toList (I.probFacts prob `Set.union` I.domFacts dom) + + -- all ground effects, extended with the preconditions from their operators + allEffs = [ (ix, op, eff) | ix <- [0 .. ] + | op <- I.domOperators dom + , eff <- I.expandEffects op ] + + + mkFact fDirtyList pres adds dels fId fProp = + do fLevel <- newIORef Nothing + fIsTrue <- newIORef Nothing + fIsGoal <- newIORef False + fDirty <- newIORef False + + return Fact { fPreCond = Map.findWithDefault Set.empty fProp pres + , fAdd = Map.findWithDefault Set.empty fProp adds + , fDel = Map.findWithDefault Set.empty fProp dels + , .. } + + mkEffect eDirtyList emptyFact facts (pres,adds,dels,effs) (eId,op,e) = + do eLevel <- newIORef Nothing + eActivePre <- newIORef 0 + eInPlan <- newIORef False + eIsInH <- newIORef False + + eDirty <- newIORef False + + let refs fs = Set.fromList (map (facts Map.!) fs) + + -- When the preconditions for this fact are empty, make it depend on + -- the special empty fact. + ePre | null (I.ePre e) = Set.singleton emptyFact + | otherwise = refs (I.ePre e) + + eff = Effect { eNumPre = length (I.ePre e) + , eAdds = refs (I.eAdd e) + , eDels = refs (I.eDel e) + , eOp = op + , .. } + + eff' = Set.singleton eff + merge f m = Map.insertWith Set.union f eff' m + + + return ( foldr merge pres (I.ePre e) + , foldr merge adds (I.eAdd e) + , foldr merge dels (I.eDel e) + , eff : effs ) + + +-- Resetting ------------------------------------------------------------------- + +-- | Reset dirty references in the plan graph to their initial state. +resetConnGraph :: ConnGraph a -> IO () +resetConnGraph ConnGraph { .. } = + do facts <- atomicModifyIORef' cgDirtyFacts (\xs -> ([], xs)) + mapM_ resetFact facts + + effs <- atomicModifyIORef' cgDirtyEffects (\xs -> ([], xs)) + mapM_ resetEffect effs + +resetFact :: Fact a -> IO () +resetFact Fact { .. } = + do writeIORef fLevel Nothing + writeIORef fIsTrue Nothing + writeIORef fIsGoal False + writeIORef fDirty False + +resetEffect :: Effect a -> IO () +resetEffect Effect { .. } = + do writeIORef eLevel Nothing + writeIORef eActivePre 0 + writeIORef eInPlan False + writeIORef eIsInH False + writeIORef eDirty False + + +-- Utilities ------------------------------------------------------------------- + +printConnGraph :: ConnGraph a -> IO () +printConnGraph cg = + do printFacts cg + printEffects cg + +printFacts :: ConnGraph a -> IO () +printFacts ConnGraph { .. } = mapM_ printFact cgFacts + +printFact :: Fact a -> IO () +printFact Fact { .. } = + do putStrLn ("Fact: (" ++ show fId ++ ") " ++ show fProp) + + lev <- readIORef fLevel + true <- readIORef fIsTrue + goal <- readIORef fIsGoal + + putStr $ unlines + [ " level: " ++ show lev + , " is true: " ++ show true + , " is goal: " ++ show goal + , " required by:" ++ show (map eId (Set.toList fPreCond)) + , " added by: " ++ show (map eId (Set.toList fAdd)) + , " deleted by: " ++ show (map eId (Set.toList fDel)) + ] + +printEffects :: ConnGraph a -> IO () +printEffects cg = mapM_ printEffect (cgEffects cg) + +printEffect :: Effect a -> IO () +printEffect Effect { .. } = + do let I.Operator { .. } = eOp + putStrLn ("Effect (" ++ show eId ++ ") " ++ T.unpack opName) + + lev <- readIORef eLevel + + putStr $ unlines + [ " level: " ++ show lev + , " requires: " ++ show (map fProp (Set.toList ePre)) + , " adds: " ++ show (map fProp (Set.toList eAdds)) + , " dels: " ++ show (map fProp (Set.toList eDels)) + ] diff --git a/src/Huff/FF/Extract.hs b/src/Huff/FF/Extract.hs new file mode 100644 --- /dev/null +++ b/src/Huff/FF/Extract.hs @@ -0,0 +1,199 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE MultiWayIf #-} + +module Huff.FF.Extract where + +import Huff.ConnGraph + +import Control.Monad ( foldM, filterM, guard ) +import Data.IORef ( readIORef, writeIORef ) +import qualified Data.IntMap.Strict as IM +import Data.Maybe ( isNothing ) +import Data.Monoid ( mappend ) +import qualified Data.Set as Set + + +-- | A map from fact level to the goals that appear there. +type GoalSet a = IM.IntMap (Goals a) + +-- | Construct the initial goal set for a set of presumed solved goals in the +-- connection graph. If the goals have not been solved, the level returned will +-- be Nothing. +-- +-- NOTE: in fast-forward, when a goal with level INFINITY is encountered, this +-- process returns immediately the value INFINITY, and doesn't complete the goal +-- set. +goalSet :: Goals a -> IO (Maybe (Level,GoalSet a)) +goalSet goals = go 0 IM.empty (Set.toList goals) + where + go !m !gs (fact:fs) = + do mb <- getLevel fact + case mb of + + Nothing -> + return Nothing + + Just i -> + do markGoal fact + go (max m i) (IM.insertWith mappend i (Set.singleton fact) gs) fs + + go !m !gs [] = return (Just (m,gs)) + + +-- | The difficulty heuristic for an effect: the lowest level where one of the +-- effect's preconditions appears. +difficulty :: Effect a -> IO Level +difficulty eff = foldM minPrecondLevel maxBound (Set.toList (effectPre eff)) + where + minPrecondLevel l fact = + do mb <- getLevel fact + case mb of + Just l' -> return $! min l l' + Nothing -> return l + +-- | Extract a plan from a fixed connection graph. +extractPlan :: Goals a -> IO (Maybe (Int,GoalSet a)) +extractPlan goals0 = + do mb <- goalSet goals0 + case mb of + Just (m,gs) -> solveGoals 0 m gs + Nothing -> return Nothing + where + + -- solve goals that are added at this fact level. + solveGoals plan level gs + | level > 0 = + do (plan',gs') <- + case IM.lookup level gs of + Just goals -> foldM (solveGoal level) (plan,gs) (Set.toList goals) + Nothing -> return (plan,gs) + + solveGoals plan' (level - 1) gs' + + | otherwise = + return (Just (plan,gs)) + + solveGoal level acc@(plan,gs) f = + do -- the goal was solved by something else at this level + mb <- isTrue f + case mb of + Just trueLevel | trueLevel == level -> + return acc + + _ -> + do eff <- pickBest (level - 1) (Set.toList (addsFact f)) + markInPlan eff + gs' <- foldM (filterGoals level) gs (Set.toList (effectPre eff)) + mapM_ (markAdd level) (Set.toList (effectAdds eff)) + let plan' = 1 + plan + plan' `seq` return (plan',gs') + + -- insert goals into the goal set for the level where they become true + filterGoals level gs fact = + do true <- isTrue fact + goal <- isGoal fact + Just l <- getLevel fact + + let existingGoal = + or [ maybe False (== level) true + -- ^ the fact was added by something else at this level + + , goal + -- ^ the fact is already a goal + + , l == 0 + -- ^ the fact exists in the initial layer + ] + + if existingGoal + then return gs + else do markGoal fact + return (IM.insertWith mappend l (Set.singleton fact) gs) + + + -- mark the fact as being added at level i + markAdd i fact = markTrue fact i + + + -- pick the best effect that achieved this goal in the given layer, using the + -- difficulty heuristic + pickBest _ [] = fail "extractPlan: invalid connection graph" + pickBest _ [e] = return e + pickBest level es = snd `fmap` foldM check (maxBound,error "pickBest") es + where + check acc@(d,_) eff = + do mb <- getLevel eff + case mb of + + Just l | l == level -> + do d' <- difficulty eff + let acc' | d' < d = (d',eff) + | otherwise = acc + return $! acc' + + _ -> return acc + + +-- Helpful Actions ------------------------------------------------------------- + +-- | All applicable actions from the state. +allActions :: State a -> IO (Effects a) +allActions s = foldM enabledEffects Set.empty (Set.toList s) + where + enabledEffects effs fact = + foldM checkEffect effs (Set.toList (requiresFact fact)) + + checkEffect effs eff = + do mb <- getLevel eff + case mb of + Just 0 -> return $! Set.insert eff effs + _ -> return effs + +-- | Helpful actions are those in the first layer of the relaxed plan, that +-- contribute something directly to the next layer. +helpfulActions :: Effects a -> Goals a -> IO [Effect a] +helpfulActions effs goals + | Set.null goals = return (Set.toList effs) + | otherwise = filterM isHelpful (Set.toList effs) + where + isHelpful eff = + do inPlan <- isInPlan eff + return (inPlan && not (Set.null (Set.intersection goals (effectAdds eff)))) + + +-- Added Goal Deletion --------------------------------------------------------- + +-- | True when the plan currently represented in the graph deletes a goal along +-- the way. +addedGoalDeletion :: Goals a -> IO Bool +addedGoalDeletion goals = go Set.empty (Set.toList goals) + where + go seen (fact : gs) = + do (seen',mb) <- foldM checkDels (seen,Just Set.empty) + (Set.toList (addsFact fact)) + case mb of + Just gs' -> go seen' (Set.toList gs' ++ gs) + Nothing -> return True + + go _ [] = return False + + checkDels acc@(seen,next) eff + + | isNothing next || eff `Set.member` seen = + return acc + + | otherwise = + do inPlan <- isInPlan eff + + let next' + | inPlan = + do guard (Set.null (goals `Set.intersection` effectDels eff)) + facts <- next + return (effectPre eff `Set.union` facts) + + | otherwise = + next + + + next' `seq` return (Set.insert eff seen, next') diff --git a/src/Huff/FF/Fixpoint.hs b/src/Huff/FF/Fixpoint.hs new file mode 100644 --- /dev/null +++ b/src/Huff/FF/Fixpoint.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE RecordWildCards #-} + +module Huff.FF.Fixpoint ( + buildFixpoint + ) where + +import Huff.ConnGraph + +import Data.Foldable (foldlM) +import Data.IORef ( readIORef, writeIORef ) +import Data.Monoid ( mconcat ) +import qualified Data.Set as Set + + +-- Predicates ------------------------------------------------------------------ + +-- | Loop until the goal state is activated in the connection graph. As the +-- connection graph should only be built from domains that can activate all +-- facts, and delete effects are ignored, this operation will terminate. The +-- set of effects returned is the set of effects that are immediately applicable +-- to the initial state. +buildFixpoint :: ConnGraph a -> State a -> Goals a -> IO Int +buildFixpoint gr s0 g = + do resetConnGraph gr + loop 0 s0 + where + loop level facts = + do effs <- mconcat `fmap` traverse (activateFact level) (Set.toList facts) + done <- allGoalsReached g + if done + then return level + else do facts' <- mconcat `fmap` mapM (activateEffect level) + (Set.toList effs) + if Set.null facts' + then return level + else loop (level + 1) facts' + + +-- | All goals have been reached if they are all activated in the connection +-- graph. +allGoalsReached :: Goals a -> IO Bool +allGoalsReached g = go goals + where + goals = Set.toList g + + -- require that all goals have a level that isn't infinity. + go (fact:rs) = + do mb <- getLevel fact + case mb of + Just{} -> go rs + Nothing -> return False + + go [] = return True + + +-- | Set a fact to true at this level of the relaxed graph. Return any effects +-- that were enabled by adding this fact. +activateFact :: Level -> Fact a -> IO (Effects a) +activateFact level fact = + do activate fact level + foldlM addedPrecond Set.empty (requiresFact fact) + + where + + addedPrecond effs eff = + do -- skip effects that are already activated + mb <- getLevel eff + case mb of + + Just{} -> + return effs + + Nothing -> + do activated <- activatePrecondition eff + if activated + then return (Set.insert eff effs) + else return effs + + +-- | Add an effect at level i, and return all of its add effects. +activateEffect :: Level -> Effect a -> IO (Facts a) +activateEffect level e = + do activate e level + return (effectAdds e) diff --git a/src/Huff/FF/Planner.hs b/src/Huff/FF/Planner.hs new file mode 100644 --- /dev/null +++ b/src/Huff/FF/Planner.hs @@ -0,0 +1,299 @@ +{-# LANGUAGE RecordWildCards #-} +module Huff.FF.Planner ( + Plan, Result(..), resSteps, + findPlan + ) where + +import Huff.ConnGraph +import Huff.FF.Extract + ( extractPlan, allActions, helpfulActions + , addedGoalDeletion ) +import Huff.FF.Fixpoint +import qualified Huff.Input as I + +import Control.Monad ( unless ) +import Data.Foldable (foldl') +import Data.Function ( on ) +import qualified Data.HashMap.Strict as HM +import qualified Data.HashSet as HS +import Data.Hashable (Hashable(..)) +import qualified Data.Heap as Heap +import Data.IORef ( IORef, newIORef, readIORef, writeIORef ) +import qualified Data.IntMap.Strict as IM +import Data.List ( sortBy ) +import Data.Maybe ( isJust, fromMaybe, catMaybes ) +import Data.Ord ( comparing ) +import qualified Data.Set as Set + + +type Plan a = Result (I.Operator a) + +data Result a = EnforcedHillClimbing [a] + | GreedyBFS [a] + deriving (Show) + +resSteps :: Result a -> [a] +resSteps (EnforcedHillClimbing as) = as +resSteps (GreedyBFS as) = as + +findPlan :: I.Problem -> I.Domain a -> IO (Maybe (Plan a)) +findPlan prob dom = + do (s0,goal,cg) <- buildConnGraph dom prob + hash <- newHash + mbRoot <- rootNode cg (mkKey s0) goal + case mbRoot of + Nothing -> return Nothing + Just root -> + do mb <- enforcedHillClimbing hash cg root goal + if isJust mb + then return $! mkPlan cg EnforcedHillClimbing mb + else do res <- greedyBestFirst hash cg root goal + return $! mkPlan cg GreedyBFS res + where + + mkPlan cg m (Just effs) = Just (m (map effectOp effs)) + mkPlan _ _ Nothing = Nothing + + getOper cg eff = return (effectOp eff) + + +-- Enforced Hill Climbing ------------------------------------------------------ + +type Steps a = [Effect a] + +enforcedHillClimbing :: Hash a -> ConnGraph a -> Node a -> Goals a + -> IO (Maybe (Steps a)) +enforcedHillClimbing hash cg root goal = + loop root + + where + + loop n = + do mb <- findBetterState hash cg n goal + case mb of + + Just n' + | nodeMeasure n' == 0 -> return (Just (extractPath n')) + | otherwise -> loop n' + + Nothing -> return Nothing + +-- | Find a state whose heuristic value is strictly smaller than the current +-- state. +findBetterState :: Hash a -> ConnGraph a -> Node a -> Goals a + -> IO (Maybe (Node a)) +findBetterState hash cg n goal = + do let Heuristic { .. } = nodeHeuristic n + acts <- helpfulActions hActions hGoals + succs <- successors True hash cg n goal acts + case filter (not . deletesGoal) succs of + n' : _ | nodeMeasure n' < nodeMeasure n -> return (Just n') + _ -> return Nothing + + +-- Greedy Best-first Search ---------------------------------------------------- + +greedyBestFirst :: Hash a -> ConnGraph a -> Node a -> Goals a + -> IO (Maybe (Steps a)) +greedyBestFirst hash cg root goal = + go HS.empty $ Heap.singleton root + { nodeHeuristic = (nodeHeuristic root) { hMeasure = maxBound }} + + where + + go seen queue = case Heap.uncons queue of + + Just (n @ Node { .. }, rest) + | nodeMeasure n == 0 -> + return (Just (extractPath n)) + + -- don't generate children for nodes that have already been visited + | nodeState `HS.member` seen -> + go seen rest + + | otherwise -> + do children <- successors False hash cg n goal (Set.toList (hActions nodeHeuristic)) + go (HS.insert nodeState seen) (foldr Heap.insert rest children) + + Nothing -> + return Nothing + + +-- Utilities ------------------------------------------------------------------- + +-- | Search nodes. +data Node a = Node { nodeState :: Key a + -- ^ The state after the effect was applied + , nodePathMeasure :: !Int + -- ^ The cost of this path + , nodeParent :: Maybe (Node a,Effect a) + -- ^ The state before this one in the plan, and the effect + -- that caused the difference + , nodeHeuristic :: !(Heuristic a) + -- ^ The actions applied in the first and second layers of + -- the relaxed graph for this node. + } deriving (Show) + +instance Eq (Node a) where + (==) = (==) `on` nodeState + {-# INLINE (==) #-} + +-- NOTE: changing the implementation of compare for Node will result in +-- different search strategies. For example, changing it from 'aStarMeasure' to +-- just 'nodeMeasure' will switch from A* to greedy-best-first search. +instance Ord (Node a) where + compare = compare `on` aStarMeasure + {-# INLINE compare #-} + +rootNode :: ConnGraph a -> Key a -> Goals a -> IO (Maybe (Node a)) +rootNode cg nodeState goal = + do mbH <- measureState False cg nodeState goal + case mbH of + Just nodeHeuristic -> + return $ Just Node { nodeParent = Nothing + , nodePathMeasure = 0 + , .. + } + + Nothing -> + return Nothing + +childNode :: Node a -> Key a -> Effect a -> Heuristic a -> Node a +childNode parent nodeState ref nodeHeuristic = + Node { nodeParent = Just (parent,ref) + , nodePathMeasure = nodePathMeasure parent + 1 + , .. + } + +deletesGoal :: Node a -> Bool +deletesGoal Node { nodeHeuristic = Heuristic { .. } } = hDeletesGoal + +aStarMeasure :: Node a -> Int +aStarMeasure n = nodePathMeasure n + nodeMeasure n + +-- | The distance that this node is from the goal state. +nodeMeasure :: Node a -> Int +nodeMeasure Node { nodeHeuristic = Heuristic { .. } } = hMeasure + +-- | Extract the set of effects applied to get to this state. This ignores the +-- root node, as it represents the initial state. +extractPath :: Node a -> [Effect a] +extractPath = go [] + where + go plan Node { .. } = + case nodeParent of + Just (p,op) -> go (op : plan) p + Nothing -> plan + + +-- | Apply effects to the current state, returning the valid choices ordered by +-- their heuristic value. +successors :: Bool -> Hash a -> ConnGraph a -> Node a -> Goals a -> [Effect a] + -> IO [Node a] +successors checkGD hash cg parent goal refs = + do mbs <- mapM heuristic refs + return $! sortBy (comparing nodeMeasure) (catMaybes mbs) + + where + + heuristic nodeOp = + do let key = mkKey (applyEffect nodeOp (keyState (nodeState parent))) + mbH <- computeHeuristic checkGD hash cg key goal + return $ do h <- mbH + return (childNode parent key nodeOp h) + + +data Heuristic a = Heuristic { hMeasure :: !Int + -- ^ The heuristic value for this state. + , hActions :: Effects a + -- ^ All actions from the first layer of the + -- relaxed planning graph + , hGoals :: Goals a + -- ^ The goals generated by layer 1 of the relaxed + -- planning graph + , hDeletesGoal :: Bool + -- ^ True when this state will cause a goal to be + -- deleted (it fails the added goal deletion + -- heuristic). If this check has been disabled, + -- this value simply shows up as 'False'. + } deriving (Show) + +-- | The Heuristic value that suggests no action. +badHeuristic :: Heuristic a +badHeuristic = Heuristic { hMeasure = maxBound + , hActions = Set.empty + , hGoals = Set.empty + , hDeletesGoal = False + } + +-- compute the heuristic value for the state that results after applying the +-- given effect, and hash it. +computeHeuristic :: Bool -> Hash a -> ConnGraph a -> Key a -> Goals a + -> IO (Maybe (Heuristic a)) +computeHeuristic checkGD hash cg key goal = + do mb <- lookupState hash key + case mb of + -- return the cached heuristic + Just h' -> return (Just h') + + -- compute and cache the heuristic + Nothing -> do mbH <- measureState checkGD cg key goal + hashState hash key (fromMaybe badHeuristic mbH) + return mbH + +-- | Compute the size of the relaxed plan produced by the given starting state +-- and goals. +measureState :: Bool -> ConnGraph a -> Key a -> Goals a + -> IO (Maybe (Heuristic a)) +measureState checkGD cg (Key s _) goal = + do _ <- buildFixpoint cg s goal + mb <- extractPlan goal + hActions <- allActions s + + hDeletesGoal <- + if checkGD + then addedGoalDeletion goal + else return False + + return $! do (hMeasure,gs) <- mb + let hGoals = fromMaybe Set.empty (IM.lookup 1 gs) + return Heuristic { .. } + + +-- State Hashing --------------------------------------------------------------- + +data Key a = Key (State a) !Int + deriving (Show) + +mkKey :: State a -> Key a +mkKey s = Key s (foldl' hashWithSalt (-2578643520546668380) s) + +keyState :: Key a -> State a +keyState (Key s _) = s + +instance Eq (Key a) where + Key s1 h1 == Key s2 h2 = h1 == h2 && s1 == s2 + +instance Hashable (Key a) where + hashWithSalt s (Key _ i) = hashWithSalt s i + +data Hash a = + Hash { shHash :: !(IORef (HM.HashMap (Key a) (Heuristic a))) } + +newHash :: IO (Hash a) +newHash = + do shHash <- newIORef HM.empty + return Hash { .. } + +-- | Add a new entry in the hash for a state. +hashState :: Hash a -> Key a -> Heuristic a -> IO () +hashState h key val = + do mb <- lookupState h key + unless (isJust mb) $ + do states <- readIORef (shHash h) + writeIORef (shHash h) $! HM.insert key val states + +lookupState :: Hash a -> Key a -> IO (Maybe (Heuristic a)) +lookupState Hash { .. } key = + do states <- readIORef shHash + return $! HM.lookup key states diff --git a/src/Huff/Input.hs b/src/Huff/Input.hs new file mode 100644 --- /dev/null +++ b/src/Huff/Input.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} + +module Huff.Input where + +import qualified Data.Set as Set +import Data.String ( IsString(..) ) +import qualified Data.Text as T + + +type Spec a = (Problem,Domain a) + +data Problem = Problem { probInit :: [Fact] + , probGoal :: [Fact] + } deriving (Show) + +-- | A collection of named operators. +newtype Domain a = Domain { domOperators :: [Operator a] + } deriving (Show) + +-- | Operators, consisting of preconditions and effects. +data Operator a = Operator { opName :: !T.Text + , opPre :: [Fact] + , opEffects :: [Effect] + , opVal :: Maybe a + } deriving (Show) + +-- | Effects, optionally guarded by additional conditions. +data Effect = Effect { ePre :: [Fact] + , eAdd :: [Fact] + , eDel :: [Fact] + } deriving (Show,Eq,Ord) + +-- | A fact is a predicate, applied to zero or more constants. +data Fact = Fact !T.Text [T.Text] + deriving (Show,Eq,Ord) + +instance IsString Fact where + fromString str = Fact (fromString str) [] + + +-- Utilities ------------------------------------------------------------------- + +probFacts :: Problem -> Set.Set Fact +probFacts Problem { .. } = Set.fromList (probInit ++ probGoal) + +domFacts :: Domain a -> Set.Set Fact +domFacts Domain { .. } = Set.unions (map opFacts domOperators) + +opFacts :: Operator a -> Set.Set Fact +opFacts Operator { .. } = + Set.unions (Set.fromList opPre : map effFacts opEffects) + +effFacts :: Effect -> Set.Set Fact +effFacts Effect { .. } = Set.fromList (ePre ++ eAdd ++ eDel) + + +-- | Emit effects that have the operator's precondition guarding their effects. +expandEffects :: Operator a -> [Effect] +expandEffects Operator { .. } = map addPrecond opEffects + where + addPrecond Effect { .. } = Effect { ePre = opPre ++ ePre, .. } diff --git a/src/Huff/QQ.hs b/src/Huff/QQ.hs new file mode 100644 --- /dev/null +++ b/src/Huff/QQ.hs @@ -0,0 +1,201 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TemplateHaskell #-} + +module Huff.QQ ( huff ) where + +import Huff.Compile as AST hiding (Name) +import qualified Huff.Input as Input +import Huff.QQ.Lexer (SourcePos(..)) +import Huff.QQ.Parser (parseQQ) + +import Control.Monad (forM) +import Data.Char (toLower) +import Data.Function (on) +import qualified Data.Text as T +import qualified Data.Map.Strict as Map +import Language.Haskell.TH +import Language.Haskell.TH.Syntax +import Language.Haskell.TH.Quote (QuasiQuoter(..)) + + +huff :: QuasiQuoter +huff = QuasiQuoter { quoteExp = notSupported "expressions" + , quotePat = notSupported "patterns" + , quoteType = notSupported "types" + , quoteDec = huffDecs + } + where + notSupported n _ = fail ("huff: Quasi-quotation is not supported for " ++ n) + +huffDecs :: String -> Q [Dec] +huffDecs str = + do loc <- location + runIO (print loc) + let (line,col) = loc_start loc + let start = SourcePos { sourceIndex = 0 + , sourceLine = line + , sourceColumn = col } + case parseQQ start str of + Left err -> fail ("huff: " ++ show err) + Right ds -> + do dss <- mapM genDomain ds + return (concat dss) + +-- | Translate the domain into one data declaration per `type`, as well as one +-- big data declaration for the domain, with one constructor per operator. +-- Additionally, write out an altered version of the domain, that will produce +-- values of the new domain type. +genDomain :: Domain T.Text -> Q [Dec] +genDomain d@Domain { .. } = + do let types = mkTypeMap domObjects + objs <- mapM genObjectDecl (Map.toList types) + dom <- genDomainDecl domName domOperators + predss <- mapM genPredicate domPreds + domValue <- genDomainValue d + return (dom : domValue ++ objs ++ concat predss) + +mkTypeMap :: [Object] -> Map.Map T.Text [T.Text] +mkTypeMap = foldl step Map.empty + where + step acc Typed { .. } = Map.alter (update tValue) tType acc + update val Nothing = Just [val] + update val (Just vs) = Just (val:vs) + +-- | Generate a data declaration from an object definition. +-- +-- INVARIANT: all objects are assumed to have the same type. +genObjectDecl :: (T.Text,[T.Text]) -> Q Dec +genObjectDecl (ty,objs) = + do show <- [t| Show |] + let cons = [ NormalC (mkName (T.unpack obj)) [] | obj <- objs ] + return (DataD [] (mkName (T.unpack ty)) [] Nothing cons [show]) + +-- | Generate a specialized predicate that can produce either a literal, or a +-- term. Produces one type-class per predicate, with instances for literals and +-- terms. +genPredicate :: AST.Pred -> Q [Dec] +genPredicate (App f xs) = + do let clsName = mkName ("Has_" ++ T.unpack f) + var = mkName "a" + pred = mkName (T.unpack f) + arrow x = AppT (AppT ArrowT x) + + params = take (length xs) [ mkName ("x" ++ show x) | x <- [ 1 .. ] ] + + instLiteral <- [t| $(conT clsName) Literal |] + instTerm <- [t| $(conT clsName) Term |] + + let mkArg p = [| AName (T.pack (show $(varE p))) |] + litBody <- [| LAtom (App $(text f) $(listE (map mkArg params))) |] + + termBody <- [| TLit $(foldl appE (varE pred) (map varE params)) |] + + return [ ClassD [] clsName [PlainTV var] [] + [ SigD pred (foldr arrow (VarT var) [ ConT (mkName (T.unpack x)) | x <- xs ]) + ] + + , InstanceD Nothing [] instLiteral + [ FunD pred [ Clause (map VarP params) (NormalB litBody) [] ] + ] + + , InstanceD Nothing [] instTerm + [ FunD pred [ Clause (map VarP params) (NormalB termBody) [] ] + ] + ] + +genDomainDecl :: T.Text -> [Operator T.Text] -> Q Dec +genDomainDecl dom ops = + do show <- [t| Show |] + let tyName = mkName (T.unpack dom) + cons <- mapM mkOpCon ops + return (DataD [] tyName [] Nothing cons [show]) + + +mkOpCon :: Operator T.Text -> Q Con +mkOpCon op = + do let conName = mkName (T.unpack (opName op)) + fields <- forM (opParams op) $ \ Typed { .. } -> + do let tyName = mkName (T.unpack tType) + bangType (bang noSourceUnpackedness noSourceStrictness) (conT tyName) + + return (NormalC conName fields) + + +genDomainValue :: Domain T.Text -> Q [Dec] +genDomainValue Domain { .. } = + do let n = mkDomVar (T.unpack domName) + typesC = typeMap domObjects + + mkCon args name = + let con x = ConE (mkName (T.unpack x)) + in foldl AppE (con name) (map con args) + + opsC = compileOperators mkCon typesC domOperators + + body <- + [d| $(varP n) = + let types = $(liftTypes typesC) + ops = $(listE (map liftOperator opsC)) + in \ start goal -> + if null goal + then error "invalid goal specification" + else compileProblem types ops (Problem start (foldr1 (/\) goal)) + |] + + let domType = mkName (T.unpack domName) + sigType <- [t| [AST.Literal] -> [AST.Term] -> Input.Spec $(conT domType) |] + let sig = SigD n sigType + + return (sig:body) + +liftTypes :: TypeMap T.Text -> Q Exp +liftTypes (TypeMap ts) = [| TypeMap (Map.fromList $(listE (map mkPair (Map.toList ts)))) |] + where + mkPair (k,xs) = [| ($(text k), $(listE (map text xs))) |] + +text :: T.Text -> Q Exp +text str = [| T.pack $(lift (T.unpack str)) |] + +-- | Lift a grounded operator. +liftOperator :: Operator Exp -> Q Exp +liftOperator Operator { .. } = + [| Operator { opName = $(text opName) + , opDerived = $(lift opDerived) + , opParams = [] + , opVal = $(liftVal opVal) + , opPrecond = $(liftTerm opPrecond) + , opEffects = $(liftEffect opEffects) + } |] + where + liftVal :: Maybe Exp -> Q Exp + liftVal Nothing = [| Nothing |] + liftVal (Just e) = [| Just $(return e) |] + +-- | Lift a precondition from a grounded operator. +liftTerm :: Term -> Q Exp +liftTerm (TAnd ts) = [| TAnd $(listE (map liftTerm ts)) |] +liftTerm (TOr ts) = [| TOr $(listE (map liftTerm ts)) |] +liftTerm (TLit lit) = [| TLit $(liftLit lit) |] +liftTerm t = fail ("Compilation pass missed something: " ++ show t) + +liftLit :: Literal -> Q Exp +liftLit (LAtom a) = [| LAtom $(liftAtom a) |] +liftLit (LNot a) = [| LNot $(liftAtom a) |] + +liftAtom :: Atom -> Q Exp +liftAtom (App f xs) = [| App $(text f) $(listE (map liftArg xs)) |] + +liftArg :: Arg -> Q Exp +liftArg (AName n) = [| AName $(text n) |] +liftArg (AVar n) = [| AVar $(text n) |] + +-- | Lift effects from a grounded operator. +liftEffect :: Effect -> Q Exp +liftEffect (EWhen p qs) = [| EWhen $(liftTerm p) $(listE (map liftLit qs)) |] +liftEffect (EAnd es) = [| EAnd $(listE (map liftEffect es)) |] +liftEffect (ELit lit) = [| ELit $(liftLit lit) |] +liftEffect e = fail ("Compilation pass missed something: " ++ show e) + +mkDomVar :: String -> Name +mkDomVar (h:tl) = mkName (toLower h : tl) +mkDomVar [] = error "Invalid domain name: no name given" diff --git a/src/Huff/QQ/Lexer.x b/src/Huff/QQ/Lexer.x new file mode 100644 --- /dev/null +++ b/src/Huff/QQ/Lexer.x @@ -0,0 +1,104 @@ +-- vim: ft=haskell + +{ +{-# OPTIONS_GHC -w #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TemplateHaskell #-} + +module Huff.QQ.Lexer ( + lexer, + Token(..), + Keyword(..), + Lexeme(..), + SourcePos(..), + SourceRange(..) + ) where + +import AlexTools +import Data.Char (isAscii) +import qualified Data.Text as T + +} + +$upper = [A-Z] +$lower = [a-z] +$number = [0-9] + +@ident = $lower [$upper $lower $number _]* +@conident = $upper [$upper $lower $number _]* + +:- + +<0> { + +-- skip whitespace +$white+ ; + +"{" { keyword K_lbrace } +"}" { keyword K_rbrace } +"(" { keyword K_lparen } +")" { keyword K_rparen } +"=" { keyword K_assign } +"|" { keyword K_pipe } +"," { keyword K_comma } +":" { keyword K_colon } +"!" { keyword K_not } +"domain" { keyword K_domain } +"predicate" { keyword K_predicate } +"operator" { keyword K_operator } +"requires" { keyword K_requires } +"effect" { keyword K_effect } +"object" { keyword K_object } + +@ident { matchText >>= \t -> lexeme (TIdent t) } +@conident { matchText >>= \t -> lexeme (TConIdent t) } + +. { lexeme TError } + +} + + +{ +-- Lexer ----------------------------------------------------------------------- + +data Token = TKeyword !Keyword + | TIdent !T.Text + | TConIdent !T.Text + | TError + deriving (Show) + +data Keyword = K_domain + | K_object + | K_predicate + | K_operator + | K_requires + | K_effect + + | K_lbrace + | K_rbrace + | K_lparen + | K_rparen + + | K_assign + | K_pipe + | K_comma + | K_colon + | K_not + deriving (Show) + +keyword :: Keyword -> Action () [Lexeme Token] +keyword kw = lexeme (TKeyword kw) + +data Error = E_lexical !SourcePos + deriving (Show) + +lexer :: SourcePos -> String -> [Lexeme Token] +lexer start str = $makeLexer simpleLexer input + where + input = (initialInput (T.pack str)) { inputPos = start } + +alexGetByte = makeAlexGetByte $ \ c -> + if isAscii c + then toEnum (fromEnum c) + else 0x1 +} diff --git a/src/Huff/QQ/Parser.y b/src/Huff/QQ/Parser.y new file mode 100644 --- /dev/null +++ b/src/Huff/QQ/Parser.y @@ -0,0 +1,160 @@ +{ +-- vim: ft=haskell +{-# OPTIONS_GHC -w #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RecordWildCards #-} +module Huff.QQ.Parser where + +import Huff.Compile.AST +import Huff.QQ.Lexer (lexer,Lexeme(..),Token(..),Keyword(..),SourcePos,sourceFrom) + +import qualified Data.Text as T + +} + +%tokentype { Lexeme Token } + +%token + IDENT { $$ @ Lexeme { lexemeToken = TIdent {} } } + CONIDENT { $$ @ Lexeme { lexemeToken = TConIdent {} } } + + 'domain' { KW K_domain $$ } + 'object' { KW K_object $$ } + 'predicate' { KW K_predicate $$ } + 'operator' { KW K_operator $$ } + 'requires' { KW K_requires $$ } + 'effect' { KW K_effect $$ } + '{' { KW K_lbrace $$ } + '}' { KW K_rbrace $$ } + '(' { KW K_lparen $$ } + ')' { KW K_rparen $$ } + ',' { KW K_comma $$ } + '=' { KW K_assign $$ } + '|' { KW K_pipe $$ } + ':' { KW K_colon $$ } + '!' { KW K_not $$ } + +%monad { Parse } +%error { parseError } + +%name domains domains + +%% + +-- Domains --------------------------------------------------------------------- + +domains :: { [Domain T.Text] } + : list1(domain) { $1 } + +domain :: { Domain T.Text } + : 'domain' CONIDENT '{' list(domain_elem) '}' + { foldr id (Domain (lexemeText $2) [] [] []) $4 } + +domain_elem :: { Domain T.Text -> Domain T.Text } + : object_decl { $1 } + | predicate_decl { $1 } + | operator_decl { $1 } + +object_decl :: { Domain T.Text -> Domain T.Text } + : 'object' type '=' sep1(CONIDENT, '|') + { let { objs = [ Typed lexemeText $2 | Lexeme { .. } <- $4 ] } + in \dom -> dom { domObjects = objs ++ domObjects dom } } + +type :: { Type } + : CONIDENT { lexemeText $1 } + +predicate_decl :: { Domain T.Text -> Domain T.Text } + : 'predicate' sep1(predicate_spec, ',') + { foldr (.) id $2 } + +predicate_spec :: { Domain T.Text -> Domain T.Text } + : IDENT '(' sep1(type, ',') ')' + { \dom -> dom { domPreds = App (lexemeText $1) $3 : domPreds dom } } + +operator_decl :: { Domain T.Text -> Domain T.Text } + : 'operator' CONIDENT '(' sep(param, ',') ')' '{' + 'requires' ':' sep1(term, ',') + 'effect' ':' sep1(effect, ',') + '}' + { let { op = Operator { opName = lexemeText $2 + , opDerived = False + , opParams = $4 + , opVal = Just (lexemeText $2) + , opPrecond = TAnd $9 + , opEffects = EAnd $12 + } } + in \dom -> dom { domOperators = op : domOperators dom } } + +param :: { Param } + : IDENT ':' type { Typed (lexemeText $1) $3 } + + +-- Expressions ----------------------------------------------------------------- + +term :: { Term } + : atom { TLit (LAtom $1) } + | '!' term { TNot $2 } + +effect :: { Effect } + : literal { ELit $1 } + +literal :: { Literal } + : atom { LAtom $1 } + | '!' atom { LNot $2 } + +atom :: { Atom } + : IDENT '(' sep1(arg, ',') ')' + { App (lexemeText $1) $3 } + +arg :: { Arg } + : IDENT { AVar (lexemeText $1) } + | CONIDENT { AName (lexemeText $1) } + + +-- Utilities ------------------------------------------------------------------- + +opt(p) + : {- empty -} { Nothing } + | p { Just $1 } + +list(p) + : {- empty -} { [] } + | list_rev1(p) { reverse $1 } + +list1(p) + : list_rev1(p) { reverse $1 } + +list_rev1(p) + : p { [$1] } + | list_rev1(p) p { $2 : $1 } + +sep(p,q) + : {- empty -} { [] } + | sep_rev(p,q) { reverse $1 } + +sep1(p,q) + : sep_rev(p,q) { reverse $1 } + +sep_rev(p,q) + : p { [$1] } + | sep_rev(p,q) q p { $3 : $1 } + +{ + +type Parse = Either ParseError + +data ParseError = ParseError (Maybe SourcePos) + deriving (Show) + +parseError :: [Lexeme Token] -> Parse a +parseError (tok:_) = Left (ParseError (Just (sourceFrom (lexemeRange tok)))) +parseError [] = Left (ParseError Nothing) + +pattern KW k loc <- Lexeme { lexemeToken = TKeyword k, lexemeRange = loc } + +parseQQ :: SourcePos -> String -> Parse [Domain T.Text] +parseQQ start str = domains toks + where + toks = lexer start str + +}