chr-lang-0.1.0.1: src/CHR/Language/Examples/Term/AST.hs
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-}
{-| Simple term language with some builtin guards and predicates
-}
module CHR.Language.Examples.Term.AST
( Tm'(..), Tm
, C
, G
, P
, POp(..)
, S
, E
, module CHR.Language.WithTerm
)
where
import CHR.Data.VarLookup
import qualified CHR.Data.Lookup as Lk
import qualified CHR.Data.Lookup.Stacked as Lk
import qualified CHR.Data.Lookup.Scoped as Lk hiding (empty)
import CHR.Data.Substitutable
import qualified CHR.Data.TreeTrie as TT
import qualified CHR.Data.VecAlloc as VAr
import CHR.Pretty as PP
import CHR.Types
import CHR.Types.Core
import CHR.Utils
import CHR.Data.AssocL
import CHR.Data.Lens
import CHR.Language.Generic
import CHR.Language.WithTerm
import qualified CHR.Solve.MonoBacktrackPrio as MBP
import Data.Typeable
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.HashMap.Strict as MapH
import qualified Data.IntMap as IntMap
import qualified Data.Set as Set
import qualified Data.List as List
import Control.Monad
import Control.Monad.IO.Class
import Control.Applicative
import GHC.Generics (Generic)
-- import UHC.Util.Debug
-- | Terms
data Tm' op
= Tm_Var Var -- ^ variable (to be substituted)
| Tm_Int Int -- ^ int value (for arithmetic)
| Tm_Str String
| Tm_Bool Bool -- ^ bool value
| Tm_Con String [Tm' op] -- ^ general term structure
| Tm_Lst [Tm' op] (Maybe (Tm' op)) -- ^ special case: list with head segment and term tail
| Tm_Op op [Tm' op] -- ^ interpretable (when solving) term structure
deriving (Show, Eq, Ord, Typeable, Generic)
type Tm = Tm' POp
instance VarTerm (Tm' op) where
varTermMbKey (Tm_Var v) = Just v
varTermMbKey _ = Nothing
varTermMkKey = Tm_Var
instance PP op => PP (Tm' op) where
pp (Tm_Var v ) = pp v -- "v" >|< v
pp (Tm_Con c [] ) = pp c
pp (Tm_Con c as ) = ppParens $ c >#< ppSpaces as
pp (Tm_Lst h mt ) = let l = ppBracketsCommas h in maybe l (\t -> ppParens $ l >#< ":" >#< t) mt
pp (Tm_Op o [a ]) = ppParens $ o >#< a
pp (Tm_Op o [a1,a2]) = ppParens $ a1 >#< o >#< a2
pp (Tm_Int i ) = pp i
pp (Tm_Str s ) = pp $ show s
pp (Tm_Bool b ) = pp b
type C = C' Tm
type G = G' Tm
type instance TT.TrTrKey (Tm' op) = Key' op
instance TT.TreeTrieKeyable (Tm' op) where
toTreeTriePreKey1 (Tm_Var v) = TT.prekey1Wild
toTreeTriePreKey1 (Tm_Int i) = TT.prekey1 $ Key_Int i
toTreeTriePreKey1 (Tm_Str s) = TT.prekey1 $ Key_Str {- $ "Tm_Str:" ++ -} s
toTreeTriePreKey1 (Tm_Bool i) = TT.prekey1 $ Key_Int $ fromEnum i
toTreeTriePreKey1 (Tm_Con c as) = TT.prekey1WithChildren (Key_Str {- $ "Tm_Con:" ++ -} c) as
toTreeTriePreKey1 (Tm_Op op as) = TT.prekey1WithChildren (Key_Op op) as
toTreeTriePreKey1 (Tm_Lst h _ ) = TT.prekey1WithChildren Key_Lst h
type E = E' Tm
-- | Binary operator
data POp
=
-- binary
PBOp_Add
| PBOp_Sub
| PBOp_Mul
| PBOp_Mod
| PBOp_Lt
| PBOp_Le
-- unary
| PUOp_Abs
deriving (Eq, Ord, Show, Generic)
instance PP POp where
pp PBOp_Add = pp "+"
pp PBOp_Sub = pp "-"
pp PBOp_Mul = pp "*"
pp PBOp_Mod = pp "mod"
pp PBOp_Lt = pp "<"
pp PBOp_Le = pp "<="
pp PUOp_Abs = pp "abs"
type P = P' Tm
type S = S' Tm
type instance ExtrValVarKey (Tm' op) = Var
instance VarUpdatable (Tm' op) (S' (Tm' op)) where
s `varUpd` t = case fromMaybe t $ Lk.lookupResolveVal varTermMbKey t s of
Tm_Con c as -> Tm_Con c $ s `varUpd` as
Tm_Lst h mt -> Tm_Lst (s `varUpd` h) (s `varUpd` mt)
Tm_Op o as -> Tm_Op o $ s `varUpd` as
t -> t
instance VarExtractable (Tm' op) where
varFreeSet (Tm_Var v) = Set.singleton v
varFreeSet (Tm_Con _ as) = Set.unions $ map varFreeSet as
varFreeSet (Tm_Lst h mt) = Set.unions $ map varFreeSet $ maybeToList mt ++ h
varFreeSet (Tm_Op _ as) = Set.unions $ map varFreeSet as
varFreeSet _ = Set.empty
instance (Eq op, TmEval (Tm' op)) => CHRMatchable E (Tm' op) (S' (Tm' op)) where
chrUnifyM how e t1 t2 = case (t1, t2) of
(Tm_Con c1 as1, Tm_Con c2 as2) | c1 == c2 -> chrUnifyM how e as1 as2
(Tm_Lst (h1:t1) mt1, Tm_Lst (h2:t2) mt2) -> chrUnifyM how e h1 h2 >> chrUnifyM how e (Tm_Lst t1 mt1) (Tm_Lst t2 mt2)
(Tm_Lst [] (Just t1), l2@(Tm_Lst {})) -> chrUnifyM how e t1 l2
(l1@(Tm_Lst {}), Tm_Lst [] (Just t2)) -> chrUnifyM how e l1 t2
(Tm_Lst [] mt1, Tm_Lst [] mt2) -> chrUnifyM how e mt1 mt2
(Tm_Op o1 as1, Tm_Op o2 as2) | how < CHRMatchHow_Unify && o1 == o2
-> chrUnifyM how e as1 as2
(Tm_Op o1 as1, t2 ) | how == CHRMatchHow_Unify -> tmEvalOp o1 as1 >>= \t1 -> chrUnifyM how e t1 t2
(t1 , Tm_Op o2 as2) | how == CHRMatchHow_Unify -> tmEvalOp o2 as2 >>= \t2 -> chrUnifyM how e t1 t2
(Tm_Int i1 , Tm_Int i2 ) | i1 == i2 -> chrMatchSuccess
(Tm_Str s1 , Tm_Str s2 ) | s1 == s2 -> chrMatchSuccess
(Tm_Bool b1 , Tm_Bool b2 ) | b1 == b2 -> chrMatchSuccess
_ -> chrMatchResolveCompareAndContinue how (chrUnifyM how e) t1 t2
instance TmEval Tm where
-- tmEval :: TmEvalOp Tm' op => Tm' op -> CHRMatcher (S' (Tm' op)) (Tm' op)
tmEval x = case x of
Tm_Int _ -> return x
Tm_Var v -> Lk.lookupResolveAndContinueM varTermMbKey chrMatchSubst chrMatchFailNoBinding tmEval v
Tm_Op o xs -> tmEvalOp o xs
_ -> chrMatchFail
-- tmEvalOp :: op -> [Tm' op] -> CHRMatcher (S' (Tm' op)) (Tm' op)
tmEvalOp o xs = do
xs <- forM xs tmEval
case (o, xs) of
(PUOp_Abs, [Tm_Int x]) -> ret $ abs x
(PBOp_Add, [Tm_Int x, Tm_Int y]) -> ret $ x + y
(PBOp_Sub, [Tm_Int x, Tm_Int y]) -> ret $ x - y
(PBOp_Mul, [Tm_Int x, Tm_Int y]) -> ret $ x * y
(PBOp_Mod, [Tm_Int x, Tm_Int y]) -> ret $ x `mod` y
(PBOp_Lt , [Tm_Int x, Tm_Int y]) -> retb $ x < y
(PBOp_Le , [Tm_Int x, Tm_Int y]) -> retb $ x <= y
where ret x = return $ Tm_Int x
retb x = return $ Tm_Bool x
type instance CHRPrioEvaluatableVal (Tm' op) = Prio
--------------------------------------------------------
type instance TmOp (Tm' op) = op
instance TmMk Tm where
tmUnaryOps _ = [("Abs", PUOp_Abs)]
tmBinaryOps _ = [("+", PBOp_Add), ("-", PBOp_Sub), ("*", PBOp_Mul), ("Mod", PBOp_Mod), ("<", PBOp_Lt), ("<=", PBOp_Le)]
mkTmBool = Tm_Bool
mkTmVar = Tm_Var
mkTmStr = Tm_Str
mkTmInt = Tm_Int . fromIntegral
mkTmCon = Tm_Con
mkTmLst = Tm_Lst
mkTmUnaryOp = \o a -> Tm_Op o [a]
mkTmBinaryOp = \o a b -> Tm_Op o [a,b]
instance TmValMk Tm where
valTmMkInt = Tm_Int
instance TmIs Tm where
isTmInt (Tm_Int v) = Just v
isTmInt _ = Nothing
isTmBool (Tm_Bool v) = Just v
isTmBool _ = Nothing