chr-lang 0.1.0.0 → 0.1.0.1
raw patch · 13 files changed
+868/−683 lines, 13 filesdep ~chr-core
Dependency ranges changed: chr-core
Files
- chr-lang.cabal +10/−7
- src/CHR/Language/Examples/Term/AST.hs +69/−274
- src/CHR/Language/Examples/Term/Run.hs +7/−119
- src/CHR/Language/Examples/Term/Visualizer.hs +1/−1
- src/CHR/Language/GTerm.hs +0/−14
- src/CHR/Language/GTerm/AST.hs +0/−124
- src/CHR/Language/GTerm/Parser.hs +0/−144
- src/CHR/Language/Generic.hs +14/−0
- src/CHR/Language/Generic/AST.hs +184/−0
- src/CHR/Language/Generic/Parser.hs +144/−0
- src/CHR/Language/WithTerm.hs +14/−0
- src/CHR/Language/WithTerm/AST.hs +278/−0
- src/CHR/Language/WithTerm/Run.hs +147/−0
chr-lang.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: chr-lang-version: 0.1.0.0+version: 0.1.0.1 synopsis: AST + surface language around chr description: AST + surface language around chr, with executable for parsing and running the evaluator. homepage: https://github.com/atzedijkstra/chr@@ -23,9 +23,12 @@ library exposed-modules:- CHR.Language.GTerm,- CHR.Language.GTerm.AST,- CHR.Language.GTerm.Parser,+ CHR.Language.Generic,+ CHR.Language.Generic.AST,+ CHR.Language.Generic.Parser,+ CHR.Language.WithTerm,+ CHR.Language.WithTerm.AST,+ CHR.Language.WithTerm.Run, CHR.Language.Examples.Term.AST, CHR.Language.Examples.Term.Run, CHR.Language.Examples.Term.Visualizer@@ -37,17 +40,17 @@ FlexibleContexts, DeriveGeneric build-depends:- base >=4.9 && < 5,+ base >=4.8 && < 5, containers >= 0.4, hashable >= 1.2.4, unordered-containers >= 0.2.7, fgl >= 5.4, mtl >= 2,- time >= 1.2,+ time >= 1.8, chr-parse >= 0.1.0.0, chr-pretty >= 0.1.0.0, chr-data >= 0.1.0.0,- chr-core >= 0.1.0.0+ chr-core >= 0.1.0.1 hs-source-dirs: src default-language: Haskell2010
src/CHR/Language/Examples/Term/AST.hs view
@@ -1,18 +1,18 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-} {-| Simple term language with some builtin guards and predicates -} module CHR.Language.Examples.Term.AST- ( Tm(..)- , C(..)- , G(..)- , P(..)+ ( Tm'(..), Tm+ , C+ , G+ , P , POp(..)- , E , S- - , Var+ , E+ + , module CHR.Language.WithTerm ) where @@ -24,14 +24,14 @@ import qualified CHR.Data.TreeTrie as TT import qualified CHR.Data.VecAlloc as VAr import CHR.Pretty as PP--- import UHC.Util.Serialize import CHR.Types import CHR.Types.Core import CHR.Utils import CHR.Data.AssocL import CHR.Data.Lens-import CHR.Language.GTerm-import qualified CHR.Solve.MonoBacktrackPrio as MBP+import CHR.Language.Generic+import CHR.Language.WithTerm+import qualified CHR.Solve.MonoBacktrackPrio as MBP import Data.Typeable import Data.Maybe@@ -47,45 +47,25 @@ -- import UHC.Util.Debug --type Var = -- IVar- String- --data Key- = Key_Int !Int - | Key_Var !Var - | Key_Str !String - | Key_Lst- | Key_Op !POp - | Key_Con !String - deriving (Eq, Ord, Show)--instance PP Key where- pp (Key_Int i) = pp i- pp (Key_Var v) = pp v- pp (Key_Str s) = pp s- pp (Key_Lst ) = ppParens "kl"- pp (Key_Op o) = pp o- pp (Key_Con s) = pp s- -- | Terms-data Tm+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] -- ^ general term structure- | Tm_Lst [Tm] (Maybe Tm) -- ^ special case: list with head segment and term tail- | Tm_Op POp [Tm] -- ^ interpretable (when solving) term structure+ | 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) -instance VarTerm Tm where+type Tm = Tm' POp++instance VarTerm (Tm' op) where varTermMbKey (Tm_Var v) = Just v varTermMbKey _ = Nothing varTermMkKey = Tm_Var -instance PP Tm where+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@@ -96,45 +76,13 @@ pp (Tm_Str s ) = pp $ show s pp (Tm_Bool b ) = pp b --- instance Serialize Tm---- | Constraint-data C- = C_Con String [Tm]- | CB_Eq Tm Tm -- ^ builtin: unification- | CB_Ne Tm Tm -- ^ builtin: non unification- | CB_Fail -- ^ explicit fail- deriving (Show, Eq, Ord, Typeable, Generic)--instance PP C where- pp (C_Con c as) = c >#< ppSpaces as- pp (CB_Eq x y ) = "unify" >#< ppSpaces [x,y]- pp (CB_Ne x y ) = "not-unify" >#< ppSpaces [x,y]- pp (CB_Fail ) = pp "fail"---- instance Serialize C---- | Guard-data G- = G_Eq Tm Tm -- ^ check for equality- | G_Ne Tm Tm -- ^ check for inequality- | G_Tm Tm -- ^ determined by arithmetic evaluation- deriving (Show, Typeable, Generic)--instance PP G where- pp (G_Eq x y) = "is-eq" >#< ppParensCommas [x,y]- pp (G_Ne x y) = "is-ne" >#< ppParensCommas [x,y]- pp (G_Tm t ) = "eval" >#< ppParens t---- instance Serialize G+type C = C' Tm -type instance TrTrKey Tm = Key-type instance TrTrKey C = Key+type G = G' Tm -type instance TT.TrTrKey Tm = Key-type instance TT.TrTrKey C = Key+type instance TT.TrTrKey (Tm' op) = Key' op -instance TT.TreeTrieKeyable Tm where+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@@ -143,12 +91,7 @@ toTreeTriePreKey1 (Tm_Op op as) = TT.prekey1WithChildren (Key_Op op) as toTreeTriePreKey1 (Tm_Lst h _ ) = TT.prekey1WithChildren Key_Lst h -instance TT.TreeTrieKeyable C where- -- Only necessary for non-builtin constraints- toTreeTriePreKey1 (C_Con c as) = TT.prekey1WithChildren (Key_Str {- $ "C_Con:" ++ -} c) as- toTreeTriePreKey1 _ = TT.prekey1Nil--type E = ()+type E = E' Tm -- | Binary operator data POp@@ -174,122 +117,27 @@ pp PBOp_Le = pp "<=" pp PUOp_Abs = pp "abs" -newtype P- = P_Tm Tm- deriving (Eq, Ord, Show, Generic)--instance PP P where- pp (P_Tm t) = pp t---- instance Serialize POp---- instance Serialize P--instance Bounded P where- minBound = P_Tm $ Tm_Int $ fromIntegral $ unPrio $ minBound- maxBound = P_Tm $ Tm_Int $ fromIntegral $ unPrio $ maxBound---- type S = IntMap.IntMap Tm-type S = Map.Map Var Tm--- type S = MapH.HashMap Var Tm--- type S = VAr.VecAlloc Tm--- type S = Lk.DefaultScpsLkup Var Tm--type instance VarLookupKey S = Var-type instance VarLookupVal S = Tm--instance PP S where- pp = ppAssocLV . Lk.toList--type instance ExtrValVarKey G = Var-type instance ExtrValVarKey C = Var-type instance ExtrValVarKey Tm = Var-type instance ExtrValVarKey P = Var--type instance CHRMatchableKey S = Key--instance VarLookup S where- varlookupWithMetaLev _ = Lk.lookup- varlookupKeysSetWithMetaLev _ = Lk.keysSet- varlookupSingletonWithMetaLev _ = Lk.singleton- varlookupEmpty = Lk.empty+type P = P' Tm -instance Lk.LookupApply S S where- apply = Lk.union+type S = S' Tm -instance VarUpdatable S S where- varUpd s = {- Lk.apply s . -} Lk.map (s `varUpd`) -- (|+>)+type instance ExtrValVarKey (Tm' op) = Var -instance VarUpdatable Tm S where+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 VarUpdatable P S where- s `varUpd` p = case p of- P_Tm t -> P_Tm (s `varUpd` t)--instance VarUpdatable G S where- s `varUpd` G_Eq x y = G_Eq (s `varUpd` x) (s `varUpd` y)- s `varUpd` G_Ne x y = G_Ne (s `varUpd` x) (s `varUpd` y)- s `varUpd` G_Tm x = G_Tm (s `varUpd` x)--instance VarUpdatable C S where- s `varUpd` c = case c of- C_Con c as -> C_Con c $ map (s `varUpd`) as- CB_Eq x y -> CB_Eq (s `varUpd` x) (s `varUpd` y)- CB_Ne x y -> CB_Ne (s `varUpd` x) (s `varUpd` y)- c -> c--instance VarExtractable Tm where+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 VarExtractable G where- varFreeSet (G_Eq x y) = Set.unions [varFreeSet x, varFreeSet y]- varFreeSet (G_Ne x y) = Set.unions [varFreeSet x, varFreeSet y]- varFreeSet (G_Tm x ) = varFreeSet x--instance VarExtractable C where- varFreeSet (C_Con _ as) = Set.unions $ map varFreeSet as- varFreeSet (CB_Eq x y ) = Set.unions [varFreeSet x, varFreeSet y]- varFreeSet _ = Set.empty--instance VarExtractable P where- varFreeSet (P_Tm t) = varFreeSet t--instance CHREmptySubstitution S where- chrEmptySubst = Lk.empty--instance IsConstraint C where- cnstrSolvesVia (C_Con _ _) = ConstraintSolvesVia_Rule- cnstrSolvesVia (CB_Eq _ _) = ConstraintSolvesVia_Solve- cnstrSolvesVia (CB_Ne _ _) = ConstraintSolvesVia_Solve- cnstrSolvesVia (CB_Fail ) = ConstraintSolvesVia_Fail--instance CHRCheckable E G S where- chrCheckM e g =- case g of- G_Eq t1 t2 -> chrUnifyM CHRMatchHow_Check e t1 t2- G_Ne t1 t2 -> do- menv <- getl chrmatcherstateEnv- s <- getl chrmatcherstateVarLookup- chrmatcherRun'- (\e -> case e of {CHRMatcherFailure -> chrMatchSuccess; _ -> chrMatchFail})- (\_ _ _ -> chrMatchFail)- (chrCheckM e (G_Eq t1 t2)) menv s- G_Tm t -> do- e <- tmEval t- case e of- Tm_Bool True -> chrMatchSuccess- _ -> chrMatchFail--instance CHRMatchable E Tm S where+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)@@ -305,111 +153,58 @@ (Tm_Bool b1 , Tm_Bool b2 ) | b1 == b2 -> chrMatchSuccess _ -> chrMatchResolveCompareAndContinue how (chrUnifyM how e) t1 t2 -tmEval :: Tm -> CHRMatcher S Tm-tmEval x = case x of+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 :: POp -> [Tm] -> CHRMatcher S Tm-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--instance CHRMatchable E C S where- chrUnifyM how e c1 c2 = do- case (c1, c2) of- (C_Con c1 as1, C_Con c2 as2) | c1 == c2 && length as1 == length as2 - -> sequence_ (zipWith (chrUnifyM how e) as1 as2)- _ -> chrMatchFail- chrBuiltinSolveM e b = case b of- CB_Eq x y -> chrUnifyM CHRMatchHow_Unify e x y- CB_Ne x y -> do- menv <- getl chrmatcherstateEnv- s <- getl chrmatcherstateVarLookup- chrmatcherRun' (\_ -> chrMatchSuccess) (\_ _ _ -> chrMatchFail) (chrBuiltinSolveM e (CB_Eq x y)) menv s--instance CHRMatchable E P S where- chrUnifyM how e p1 p2 = do- case (p1, p2) of- (P_Tm t1 , P_Tm t2 ) -> chrUnifyM how e t1 t2--type instance CHRPrioEvaluatableVal Tm = Prio--instance CHRPrioEvaluatable E Tm S where- chrPrioEval e s t = case chrmatcherRun' (\_ -> Tm_Int $ fromIntegral $ unPrio $ (minBound :: Prio)) (\_ _ x -> x) (tmEval t) emptyCHRMatchEnv (Lk.lifts s) of- Tm_Int i -> fromIntegral i- t -> minBound- chrPrioLift = Tm_Int . fromIntegral--type instance CHRPrioEvaluatableVal P = Prio+ -- 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 -instance CHRPrioEvaluatable E P S where- chrPrioEval e s p = case p of- P_Tm t -> chrPrioEval e s t- chrPrioLift = P_Tm . chrPrioLift+type instance CHRPrioEvaluatableVal (Tm' op) = Prio -------------------------------------------------------- -instance GTermAs C G P P Tm where- asHeadConstraint t = case t of- GTm_Con c a -> forM a asTm >>= (return . C_Con c)- t -> gtermasFail t "not a constraint"+type instance TmOp (Tm' op) = op - asBodyConstraint t = case t of- GTm_Con "Fail" [] -> return CB_Fail- GTm_Con o [a,b] | isJust o' -> do- a <- asTm a- b <- asTm b- return $ fromJust o' a b- where o' = List.lookup o [("==", CB_Eq), ("/=", CB_Ne)]- t -> asHeadConstraint t+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] - asGuard t = case t of- GTm_Con o [a,b] | isJust o' -> do- a <- asTm a- b <- asTm b- return $ fromJust o' a b- where o' = List.lookup o [("==", G_Eq), ("/=", G_Ne)]- t -> fmap G_Tm $ asTm t- - asHeadBacktrackPrio = fmap P_Tm . asTm+instance TmValMk Tm where+ valTmMkInt = Tm_Int - asAltBacktrackPrio = asHeadBacktrackPrio- asRulePrio = asHeadBacktrackPrio+instance TmIs Tm where+ isTmInt (Tm_Int v) = Just v+ isTmInt _ = Nothing - asTm t = case t of- GTm_Con "True" [] -> return $ Tm_Bool True- GTm_Con "False" [] -> return $ Tm_Bool False- GTm_Con o [a] | isJust o' -> do- a <- asTm a- return $ Tm_Op (fromJust o') [a]- where o' = List.lookup o [("Abs", PUOp_Abs)]- GTm_Con o [a,b] | isJust o' -> do- a <- asTm a- b <- asTm b- return $ Tm_Op (fromJust o') [a,b]- where o' = List.lookup o [("+", PBOp_Add), ("-", PBOp_Sub), ("*", PBOp_Mul), ("Mod", PBOp_Mod), ("<", PBOp_Lt), ("<=", PBOp_Le)]- GTm_Con c a -> forM a asTm >>= (return . Tm_Con c)- GTm_Var v -> -- Tm_Var <$> gtermasVar v- return $ Tm_Var v- GTm_Str v -> return $ Tm_Str v- GTm_Int i -> return $ Tm_Int (fromInteger i)- GTm_Nil -> return $ Tm_Lst [] Nothing- t@(GTm_Cns _ _) -> asTmList t >>= (return . uncurry Tm_Lst)- -- t -> gtermasFail t "not a term"+ isTmBool (Tm_Bool v) = Just v+ isTmBool _ = Nothing ------------------------------------------------------------ leq example, backtrack prio specific+
src/CHR/Language/Examples/Term/Run.hs view
@@ -1,131 +1,19 @@ module CHR.Language.Examples.Term.Run- ( RunOpt(..)- , Verbosity(..)+ ( Run.RunOpt(..)+ , Run.Verbosity(..) , runFile ) where -import Data.Maybe-import System.IO-import Data.Time.Clock.POSIX-import Data.Time.Clock.System-import Data.Time.Clock.TAI-import Control.Monad-import Control.Monad.IO.Class-import Control.Monad.State.Class-import qualified Data.Set as Set--import CHR.Parse-import CHR.Scan--import CHR.Data.Substitutable-import CHR.Pretty-import CHR.Utils-import CHR.Data.Lens-import qualified CHR.Data.TreeTrie as TT--- import qualified UHC.Util.CHR.Solve.TreeTrie.Internal.Shared as TT-import qualified CHR.Data.Lookup as Lk-import CHR.Types.Rule-import CHR.Types-import CHR.Language.GTerm.Parser-import CHR.Solve.MonoBacktrackPrio as MBP+import Data.Proxy import CHR.Language.Examples.Term.AST import CHR.Language.Examples.Term.Visualizer -import qualified GHC.Exts as Prim--data RunOpt- = RunOpt_DebugTrace -- ^ include debugging trace in output- | RunOpt_SucceedOnLeftoverWork -- ^ left over unresolvable (non residue) work is also a successful result- | RunOpt_SucceedOnFailedSolve -- ^ failed solve is considered also a successful result, with the failed constraint as a residue- | RunOpt_WriteVisualization -- ^ write visualization (html file) to disk- | RunOpt_Verbosity Verbosity- deriving (Eq)+import qualified CHR.Language.WithTerm.Run as Run -mbRunOptVerbosity :: [RunOpt] -> Maybe Verbosity-mbRunOptVerbosity [] = Nothing-mbRunOptVerbosity (RunOpt_Verbosity v : _) = Just v-mbRunOptVerbosity (_ : r) = mbRunOptVerbosity r+import qualified GHC.Exts as Prim -- | Run file with options-runFile :: [RunOpt] -> FilePath -> IO ()-runFile runopts f = do- -- scan, parse- msg $ "READ " ++ f - mbParse <- parseFile f- case mbParse of- Left e -> putPPLn e- Right (prog, query, varToNmMp) -> do- let verbosity = maximum $ [Verbosity_Quiet] ++ maybeToList (mbRunOptVerbosity runopts) ++ (if RunOpt_DebugTrace `elem` runopts then [Verbosity_ALot] else [])- sopts = defaultCHRSolveOpts- { chrslvOptSucceedOnLeftoverWork = RunOpt_SucceedOnLeftoverWork `elem` runopts- , chrslvOptSucceedOnFailedSolve = RunOpt_SucceedOnFailedSolve `elem` runopts- , chrslvOptGatherDebugInfo = verbosity >= Verbosity_Debug- , chrslvOptGatherTraceInfo = RunOpt_WriteVisualization `elem` runopts || verbosity >= Verbosity_ALot- }- mbp :: CHRMonoBacktrackPrioT C G P P S E IO (SolverResult S)- mbp = do- -- print program- liftIO $ putPPLn $ "Rules" >-< indent 2 (vlist $ map pp prog)- -- liftIO $ putPPLn $ "Rule TT keys" >-< indent 2 (vlist $ map (pp . TT.chrToKey . head . ruleHead) prog)- -- liftIO $ putPPLn $ "Rule TT2 keys" >-< indent 2 (vlist $ map (pp . TT.toTreeTrieKey) prog)- -- freshen query vars- query <- slvFreshSubst Set.empty query >>= \s -> return $ s `varUpd` query- -- print query- liftIO $ putPPLn $ "Query" >-< indent 2 (vlist $ map pp query)- mapM_ addRule prog- mapM_ addConstraintAsWork query- -- solve- liftIO $ msg $ "SOLVE " ++ f- r <- (Prim.inline chrSolve) sopts ()- ppSolverResult verbosity r >>= \sr -> liftIO $ putPPLn $ "Solution" >-< indent 2 sr- if (RunOpt_WriteVisualization `elem` runopts)- then- do- (CHRGlobState{_chrgstTrace = trace}, _) <- get- time <- liftIO getPOSIXTime- let fileName = "visualization-" ++ show (round time) ++ ".html"- liftIO $ writeFile fileName (showPP $ chrVisualize query trace)- liftIO $ msg "VISUALIZATION"- liftIO $ putStrLn $ "Written visualization as " ++ fileName- else (return ())- return r- tBef <- getSystemTime - (_,(gs,_)) <- runCHRMonoBacktrackPrioT- (chrgstVarToNmMp ^= Lk.inverse (flip (,)) varToNmMp $ emptyCHRGlobState)- (emptyCHRBackState {- _chrbstBacktrackPrio=0 -}) {- 0 -}- mbp- tAft <- getSystemTime- let tDif = systemToTAITime tAft `diffAbsoluteTime` systemToTAITime tBef- nSteps = gs ^. MBP.chrgstStatNrSolveSteps-- -- done- msg $ "DONE (" ++ show tDif ++ " / " ++ show nSteps ++ " = " ++ show (tDif / fromIntegral nSteps) ++ ") " ++ f- - where- msg m = putStrLn $ "---------------- " ++ m ++ " ----------------"- -- dummy = undefined :: Rule C G P P---- | run some test programs-mainTerm = do- forM_- [- "typing2"- -- , "queens"- -- , "leq"- -- , "var"- -- , "ruleprio"- -- , "backtrack3"- -- , "unify"- -- , "antisym"- ] $ \f -> do- let f' = "test/" ++ f ++ ".chr"- runFile- [ RunOpt_SucceedOnLeftoverWork- , RunOpt_DebugTrace- ] f'- --{---}+runFile :: [Run.RunOpt] -> FilePath -> IO ()+runFile runopts f = (Prim.inline Run.runFile) (Proxy :: Proxy Tm) runopts chrVisualize f
src/CHR/Language/Examples/Term/Visualizer.hs view
@@ -13,7 +13,7 @@ import qualified CHR.Data.Lookup as Lk import CHR.Types import CHR.Types.Rule-import CHR.Language.GTerm.Parser+import CHR.Language.Generic.Parser -- import UHC.Util.CHR.Solve.TreeTrie.Mono import CHR.Solve.MonoBacktrackPrio as MBP import CHR.Language.Examples.Term.AST
− src/CHR/Language/GTerm.hs
@@ -1,14 +0,0 @@------------------------------------------------------------------------------------------------ Generic terms describing constraints, providing parsing and interpretation to AST of your choice----------------------------------------------------------------------------------------------module CHR.Language.GTerm- ( module CHR.Language.GTerm.AST- , module CHR.Language.GTerm.Parser- )- where--import CHR.Language.GTerm.AST-import CHR.Language.GTerm.Parser--
− src/CHR/Language/GTerm/AST.hs
@@ -1,124 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TupleSections #-}------------------------------------------------------------------------------------------------- Generic terms describing constraints, providing interpretation to AST of your choice----------------------------------------------------------------------------------------------module CHR.Language.GTerm.AST- ( GTm(..)- - , GTermAs(..)- - , GTermAsState(..)- , emptyGTermAsState- - , gtermasVar- - , gtermasFail- )- where--import Data.Char-import Data.Typeable-import GHC.Generics-import Control.Monad.Except-import Control.Monad.State--- import qualified Data.Map as Map-import qualified Data.HashMap.Strict as MapH--import CHR.Pretty as PP-import CHR.Utils-import CHR.Data.Lens-import CHR.Types-import qualified CHR.Data.Lookup as Lk--- import CHR.Types.Core------------------------------------------------------------------------------------------------- Supporting types----------------------------------------------------------------------------------------------data GTermAsState- = GTermAsState- { _gtermasNmToVarMp :: NmToVarMp- }--emptyGTermAsState :: GTermAsState-emptyGTermAsState = GTermAsState emptyNmToVarMp- ------------------------------------------------------------------------------------------------ Lens----------------------------------------------------------------------------------------------mkLabel ''GTermAsState------------------------------------------------------------------------------------------------- Term language/AST------------------------------------------------------------------------------------------------ | Terms-data GTm- = GTm_Var String -- ^ variable (to be substituted)- | GTm_Int Integer -- ^ int value (for arithmetic)- | GTm_Str String -- ^ string value- | GTm_Con String [GTm] -- ^ general term structure- | GTm_Nil -- ^ special case: list nil- | GTm_Cns GTm GTm -- ^ special case: list cons- deriving (Show, Eq, Ord, Typeable, Generic)--instance PP GTm where- pp (GTm_Var v ) = pp v -- "v" >|< v- pp (GTm_Con c [] ) = pp c- pp (GTm_Con c@(h:_) [a1,a2])- | not (isAlpha h) = ppParens $ a1 >#< c >#< a2- pp (GTm_Con c as ) = ppParens $ c >#< ppSpaces as- pp (GTm_Nil ) = pp "[]"- pp (GTm_Cns h t ) = "[" >|< h >#< ":" >#< t >|< "]"- pp (GTm_Int i ) = pp i- pp (GTm_Str s ) = pp $ show s------------------------------------------------------------------------------------------------- Term interpretation in context of CHR------------------------------------------------------------------------------------------------ | Interpretation monad, which is partial-type GTermAsM = StateT GTermAsState (Either PP_Doc)---- | Term interpretation in context of CHR-class GTermAs cnstr guard bprio prio tm- | cnstr -> guard bprio prio tm- , guard -> cnstr bprio prio tm- , bprio -> cnstr guard prio tm- , prio -> cnstr guard bprio tm- , tm -> cnstr guard bprio prio- where- --- asTm :: GTm -> GTermAsM tm- -- | as list, if matches/possible. Only to be invoked for GTm_Cns - asTmList :: GTm -> GTermAsM ([tm], Maybe tm)- asTmList (GTm_Cns h GTm_Nil ) = asTm h >>= \h -> return ([h], Nothing)- asTmList (GTm_Cns h t@(GTm_Cns _ _)) = asTm h >>= \h -> asTmList t >>= \(t,mt) -> return ((h:t),mt)- asTmList (GTm_Cns h t ) = asTm h >>= \h -> asTm t >>= \t -> return ([h], Just t)- asTmList _ = panic "GTermAs.asTmList: should not happen, not intended to be called with non GTm_Cns"- --- asHeadConstraint :: GTm -> GTermAsM cnstr- --- asBodyConstraint :: GTm -> GTermAsM cnstr- --- asGuard :: GTm -> GTermAsM guard- --- asHeadBacktrackPrio :: GTm -> GTermAsM bprio- --- asAltBacktrackPrio :: GTm -> GTermAsM bprio- --- asRulePrio :: GTm -> GTermAsM prio-----gtermasVar :: String -> GTermAsM IVar-gtermasVar s = modL gtermasNmToVarMp $ \m -> maybe (let i = Lk.size m in (i, Lk.insert s i m)) (,m) $ Lk.lookup s m- - -- insertLookupWithKey :: Ord k => (k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)---- | Fail the interpretation-gtermasFail :: GTm -> String -> GTermAsM a-gtermasFail t m = throwError $ "GTerm interpretation failure" >-< indent 2 ("why :" >#< m >-< "term:" >#< t)
− src/CHR/Language/GTerm/Parser.hs
@@ -1,144 +0,0 @@-{-# LANGUAGE RankNTypes #-}--module CHR.Language.GTerm.Parser- ( parseFile- )- where--import qualified Data.Set as Set--import Control.Monad-import Control.Monad.State--import CHR.Parse-import CHR.Scan-import CHR.Pretty--import CHR.Types-import CHR.Types.Rule-import CHR.Language.GTerm.AST------------------------------------------------------------------------------------------------- Scanning options for CHR parsing------------------------------------------------------------------------------------------------ | Scanning options for rule parser-scanOpts :: ScanOpts-scanOpts- = defaultScanOpts- { scoKeywordsTxt = Set.fromList []- , scoKeywordsOps = Set.fromList ["\\", "=>", "==>", "<=>", ".", ":", "::", "@", "|", "\\/", "?"]- , scoOpChars = Set.fromList "!#$%&*+/<=>?@\\^|-:.~"- , scoSpecChars = Set.fromList "()[],`"- }------------------------------------------------------------------------------------------------- Parse interface------------------------------------------------------------------------------------------------ | Parse a file as a CHR spec + queries-parseFile :: GTermAs c g bp rp tm => FilePath -> IO (Either PP_Doc ([Rule c g bp rp], [c], NmToVarMp))-parseFile f = do- toks <- scanFile- (Set.toList $ scoKeywordsTxt scanOpts)- (Set.toList $ scoKeywordsOps scanOpts)- (Set.toList $ scoSpecChars scanOpts)- (Set.toList $ scoOpChars scanOpts)- f- (prog, query) <- parseIOMessage show pProg toks- return $ fmap (\((r,c),s) -> (r, c, _gtermasNmToVarMp s)) $ flip runStateT emptyGTermAsState $ do- prog <- forM prog $ \r@(Rule {ruleHead=hcs, ruleGuard=gs, ruleBodyAlts=as, ruleBacktrackPrio=mbp, rulePrio=mrp}) -> do- mbp <- maybe (return Nothing) (fmap Just . asHeadBacktrackPrio) mbp- mrp <- maybe (return Nothing) (fmap Just . asRulePrio) mrp- hcs <- forM hcs asHeadConstraint- gs <- forM gs asGuard- as <- forM as $ \a@(RuleBodyAlt {rbodyaltBacktrackPrio=mbp, rbodyaltBody=bs}) -> do- mbp <- maybe (return Nothing) (fmap Just . asAltBacktrackPrio) mbp- bs <- forM bs asBodyConstraint- return $ a {rbodyaltBacktrackPrio=mbp, rbodyaltBody=bs}- return $ r {ruleHead=hcs, ruleGuard=gs, ruleBodyAlts=as, ruleBacktrackPrio=mbp, rulePrio=mrp}- query <- forM query asHeadConstraint- return (prog,query)------------------------------------------------------------------------------------------------- Program is set of rules + optional queries----------------------------------------------------------------------------------------------type Pr p = PlainParser Token p---- | CHR Program = rules + optional queries-pProg :: Pr ([Rule GTm GTm GTm GTm], [GTm])-pProg =- pRules <+> pQuery- where- pR = pPre <**>- ( pHead <**>- ( ( (\(g,b) h pre -> pre $ g $ mkR h (length h) b) <$ pKey "<=>"- <|> (\(g,b) h pre -> pre $ g $ mkR h 0 b) <$ (pKey "=>" <|> pKey "==>")- ) <*> pBody- <|> ( (\hr (g,b) hk pre -> pre $ g $ mkR (hr ++ hk) (length hr) b)- <$ pKey "\\" <*> pHead <* pKey "<=>" <*> pBody- )- )- )- where pPre = (\(bp,rp) lbl -> lbl . bp . rp) - <$> (pParens ((,) <$> (flip (=!) <$> pTm_Var <|> pSucceed id)- <* pComma- <*> (flip (=!!) <$> pTm <|> pSucceed id)- ) <* pKey "::" <|> pSucceed (id,id)- )- <*> ((@=) <$> (pConid <|> pVarid) <* pKey "@" <|> pSucceed id)- pHead = pList1Sep pComma pTm_App- pGrd = flip (=|) <$> pList1Sep pComma pTm_Op <* pKey "|" <|> pSucceed id- pBody = pGrd <+> pBodyAlts- pBodyAlts = pListSep (pKey "\\/") pBodyAlt- pBodyAlt- = (\pre b -> pre $ b /\ [])- <$> (flip (\!) <$> pTm <* pKey "::" <|> pSucceed id)- <*> pList1Sep pComma pTm_Op- mkR h len b = Rule h len [] b Nothing Nothing Nothing-- pRules = pList (pR <* pKey ".")-- pQuery = concat <$> pList (pKey "?" *> pList1Sep pComma pTm_Op <* pKey ".")- - pTm- = pTm_Op-- pTm_Op- = pTm_App <**>- ( (\o r l -> GTm_Con o [l,r]) <$> pOp <*> pTm_App- <|> pSucceed id- )- where pOp- = pConsym- <|> pVarsym- <|> pKey "`" *> pConid <* pKey "`"- <|> pCOLON-- pTm_App- = GTm_Con <$> pConid <*> pList1 pTm_Base- <|> (\o l r -> GTm_Con o [l,r]) <$> pParens pVarsym <*> pTm_Base <*> pTm_Base- <|> pTm_Base-- pTm_Base- = pTm_Var- <|> (GTm_Int . read) <$> pInteger- <|> GTm_Str <$> pString- <|> flip GTm_Con [] <$> pConid- <|> pParens pTm- <|> pPacked (pKey "[") (pKey "]")- ( pTm_App <**>- ( (\t h -> foldr1 GTm_Cns (h:t)) <$ pCOLON <*> pList1Sep pCOLON pTm_App- <|> (\t h -> foldr GTm_Cns GTm_Nil (h:t)) <$ pKey "," <*> pList1Sep (pKey ",") pTm_App- <|> pSucceed (`GTm_Cns` GTm_Nil)- )- <|> pSucceed GTm_Nil- )-- pTm_Var- = GTm_Var <$> pVarid-- pCOLON = pKey ":"--
+ src/CHR/Language/Generic.hs view
@@ -0,0 +1,14 @@+-------------------------------------------------------------------------------------------+--- Generic infra describing constraints, providing parsing and interpretation to AST of your choice+-------------------------------------------------------------------------------------------++module CHR.Language.Generic+ ( module CHR.Language.Generic.AST+ , module CHR.Language.Generic.Parser+ )+ where++import CHR.Language.Generic.AST+import CHR.Language.Generic.Parser++
+ src/CHR/Language/Generic/AST.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}++-------------------------------------------------------------------------------------------+--- Generic terms describing constraints, providing interpretation to AST of your choice+-------------------------------------------------------------------------------------------++module CHR.Language.Generic.AST+ ( TmOp+ , TmMk(..)+ , TmIs(..)+ , TmValMk(..)+ + , GTm(..)+ + , GTermAs(..)+ , GTermAsTm(..)+ + , GTermAsM+ + , GTermAsState(..)+ , emptyGTermAsState+ + , gtermasVar+ + , gtermasFail+ )+ where++import Data.Char+import Data.Typeable+import Data.Proxy+import GHC.Generics+import Control.Monad.Except+import Control.Monad.State+-- import qualified Data.Map as Map+import qualified Data.HashMap.Strict as MapH++import CHR.Pretty as PP+import CHR.Utils+import CHR.Data.Lens+import CHR.Types+import qualified CHR.Data.Lookup as Lk+import qualified Data.List as List+-- import CHR.Types.Core++-------------------------------------------------------------------------------------------+--- Supporting types+-------------------------------------------------------------------------------------------++data GTermAsState+ = GTermAsState+ { _gtermasNmToVarMp :: NmToVarMp+ }++emptyGTermAsState :: GTermAsState+emptyGTermAsState = GTermAsState emptyNmToVarMp+ +-------------------------------------------------------------------------------------------+--- Lens+-------------------------------------------------------------------------------------------++mkLabel ''GTermAsState++-------------------------------------------------------------------------------------------+--- Term language/AST+-------------------------------------------------------------------------------------------++-- | Terms+data GTm+ = GTm_Var String -- ^ variable (to be substituted)+ | GTm_Int Integer -- ^ int value (for arithmetic)+ | GTm_Str String -- ^ string value+ | GTm_Con String [GTm] -- ^ general term structure+ | GTm_Nil -- ^ special case: list nil+ | GTm_Cns GTm GTm -- ^ special case: list cons+ deriving (Show, Eq, Ord, Typeable, Generic)++instance PP GTm where+ pp (GTm_Var v ) = pp v -- "v" >|< v+ pp (GTm_Con c [] ) = pp c+ pp (GTm_Con c@(h:_) [a1,a2])+ | not (isAlpha h) = ppParens $ a1 >#< c >#< a2+ pp (GTm_Con c as ) = ppParens $ c >#< ppSpaces as+ pp (GTm_Nil ) = pp "[]"+ pp (GTm_Cns h t ) = "[" >|< h >#< ":" >#< t >|< "]"+ pp (GTm_Int i ) = pp i+ pp (GTm_Str s ) = pp $ show s++-------------------------------------------------------------------------------------------+--- Term interpretation in context of CHR+-------------------------------------------------------------------------------------------++type family TmOp tm :: *++class TmMk tm where+ tmUnaryOps :: Proxy tm -> [(String, TmOp tm)]+ tmBinaryOps :: Proxy tm -> [(String, TmOp tm)]+ + mkTmBool :: Bool -> tm+ mkTmVar :: String -> tm+ mkTmStr :: String -> tm+ mkTmInt :: Integer -> tm+ mkTmCon :: String -> [tm] -> tm+ mkTmLst :: [tm] -> Maybe tm -> tm+ + mkTmUnaryOp :: TmOp tm -> tm -> tm+ mkTmBinaryOp :: TmOp tm -> tm -> tm -> tm++class TmIs tm where+ isTmInt :: tm -> Maybe Int+ isTmBool :: tm -> Maybe Bool+ -- tmValMkInt :: Int -> tm++class TmValMk tm where+ valTmMkInt :: Int -> tm++-- | Interpretation monad, which is partial+type GTermAsM = StateT GTermAsState (Either PP_Doc)++class TmMk tm => GTermAsTm tm where+ asTm :: GTm -> GTermAsM tm+ asTm t = case t of+ GTm_Con "True" [] -> return $ mkTmBool True+ GTm_Con "False" [] -> return $ mkTmBool False+ GTm_Con o [a]+ | Just o' <- List.lookup o (tmUnaryOps (Proxy :: Proxy tm))-> do+ a <- asTm a+ return $ mkTmUnaryOp o' a+ GTm_Con o [a,b]+ | Just o' <- List.lookup o (tmBinaryOps (Proxy :: Proxy tm)) -> do+ a <- asTm a+ b <- asTm b+ return $ mkTmBinaryOp o' a b+ GTm_Con c a -> forM a asTm >>= (return . mkTmCon c)+ GTm_Var v -> -- Tm_Var <$> gtermasVar v+ return $ mkTmVar v+ GTm_Str v -> return $ mkTmStr v+ GTm_Int i -> return $ mkTmInt i+ GTm_Nil -> return $ mkTmLst [] Nothing+ t@(GTm_Cns _ _) -> asTmList t >>= (return . uncurry mkTmLst)+ -- t -> gtermasFail t "not a term"++ -- | as list, if matches/possible. Only to be invoked for GTm_Cns + asTmList :: GTm -> GTermAsM ([tm], Maybe tm)+ asTmList (GTm_Cns h GTm_Nil ) = asTm h >>= \h -> return ([h], Nothing)+ asTmList (GTm_Cns h t@(GTm_Cns _ _)) = asTm h >>= \h -> asTmList t >>= \(t,mt) -> return ((h:t),mt)+ asTmList (GTm_Cns h t ) = asTm h >>= \h -> asTm t >>= \t -> return ([h], Just t)+ asTmList _ = panic "GTermAs.asTmList: should not happen, not intended to be called with non GTm_Cns"++instance {-# OVERLAPPABLE #-} TmMk tm => GTermAsTm tm where++-- | Term interpretation in context of CHR+class GTermAs cnstr guard bprio prio+ | cnstr -> guard bprio prio+ , guard -> cnstr bprio prio + , bprio -> cnstr guard prio + , prio -> cnstr guard bprio + where+ --+ asHeadConstraint :: GTm -> GTermAsM cnstr+ --+ asBodyConstraint :: GTm -> GTermAsM cnstr+ --+ asGuard :: GTm -> GTermAsM guard+ --+ asHeadBacktrackPrio :: GTm -> GTermAsM bprio+ --+ asAltBacktrackPrio :: GTm -> GTermAsM bprio+ --+ asRulePrio :: GTm -> GTermAsM prio++--+gtermasVar :: String -> GTermAsM IVar+gtermasVar s = modL gtermasNmToVarMp $ \m -> maybe (let i = Lk.size m in (i, Lk.insert s i m)) (,m) $ Lk.lookup s m+ + -- insertLookupWithKey :: Ord k => (k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)++-- | Fail the interpretation+gtermasFail :: GTm -> String -> GTermAsM a+gtermasFail t m = throwError $ "GTerm interpretation failure" >-< indent 2 ("why :" >#< m >-< "term:" >#< t)
+ src/CHR/Language/Generic/Parser.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE RankNTypes #-}++module CHR.Language.Generic.Parser+ ( parseFile+ )+ where++import qualified Data.Set as Set++import Control.Monad+import Control.Monad.State++import CHR.Parse+import CHR.Scan+import CHR.Pretty++import CHR.Types+import CHR.Types.Rule+import CHR.Language.Generic.AST++-------------------------------------------------------------------------------------------+--- Scanning options for CHR parsing+-------------------------------------------------------------------------------------------++-- | Scanning options for rule parser+scanOpts :: ScanOpts+scanOpts+ = defaultScanOpts+ { scoKeywordsTxt = Set.fromList []+ , scoKeywordsOps = Set.fromList ["\\", "=>", "==>", "<=>", ".", ":", "::", "@", "|", "\\/", "?"]+ , scoOpChars = Set.fromList "!#$%&*+/<=>?@\\^|-:.~"+ , scoSpecChars = Set.fromList "()[],`"+ }++-------------------------------------------------------------------------------------------+--- Parse interface+-------------------------------------------------------------------------------------------++-- | Parse a file as a CHR spec + queries+parseFile :: GTermAs c g bp rp => FilePath -> IO (Either PP_Doc ([Rule c g bp rp], [c], NmToVarMp))+parseFile f = do+ toks <- scanFile+ (Set.toList $ scoKeywordsTxt scanOpts)+ (Set.toList $ scoKeywordsOps scanOpts)+ (Set.toList $ scoSpecChars scanOpts)+ (Set.toList $ scoOpChars scanOpts)+ f+ (prog, query) <- parseIOMessage show pProg toks+ return $ fmap (\((r,c),s) -> (r, c, _gtermasNmToVarMp s)) $ flip runStateT emptyGTermAsState $ do+ prog <- forM prog $ \r@(Rule {ruleHead=hcs, ruleGuard=gs, ruleBodyAlts=as, ruleBacktrackPrio=mbp, rulePrio=mrp}) -> do+ mbp <- maybe (return Nothing) (fmap Just . asHeadBacktrackPrio) mbp+ mrp <- maybe (return Nothing) (fmap Just . asRulePrio) mrp+ hcs <- forM hcs asHeadConstraint+ gs <- forM gs asGuard+ as <- forM as $ \a@(RuleBodyAlt {rbodyaltBacktrackPrio=mbp, rbodyaltBody=bs}) -> do+ mbp <- maybe (return Nothing) (fmap Just . asAltBacktrackPrio) mbp+ bs <- forM bs asBodyConstraint+ return $ a {rbodyaltBacktrackPrio=mbp, rbodyaltBody=bs}+ return $ r {ruleHead=hcs, ruleGuard=gs, ruleBodyAlts=as, ruleBacktrackPrio=mbp, rulePrio=mrp}+ query <- forM query asHeadConstraint+ return (prog,query)++-------------------------------------------------------------------------------------------+--- Program is set of rules + optional queries+-------------------------------------------------------------------------------------------++type Pr p = PlainParser Token p++-- | CHR Program = rules + optional queries+pProg :: Pr ([Rule GTm GTm GTm GTm], [GTm])+pProg =+ pRules <+> pQuery+ where+ pR = pPre <**>+ ( pHead <**>+ ( ( (\(g,b) h pre -> pre $ g $ mkR h (length h) b) <$ pKey "<=>"+ <|> (\(g,b) h pre -> pre $ g $ mkR h 0 b) <$ (pKey "=>" <|> pKey "==>")+ ) <*> pBody+ <|> ( (\hr (g,b) hk pre -> pre $ g $ mkR (hr ++ hk) (length hr) b)+ <$ pKey "\\" <*> pHead <* pKey "<=>" <*> pBody+ )+ )+ )+ where pPre = (\(bp,rp) lbl -> lbl . bp . rp) + <$> (pParens ((,) <$> (flip (=!) <$> pTm_Var <|> pSucceed id)+ <* pComma+ <*> (flip (=!!) <$> pTm <|> pSucceed id)+ ) <* pKey "::" <|> pSucceed (id,id)+ )+ <*> ((@=) <$> (pConid <|> pVarid) <* pKey "@" <|> pSucceed id)+ pHead = pList1Sep pComma pTm_App+ pGrd = flip (=|) <$> pList1Sep pComma pTm_Op <* pKey "|" <|> pSucceed id+ pBody = pGrd <+> pBodyAlts+ pBodyAlts = pListSep (pKey "\\/") pBodyAlt+ pBodyAlt+ = (\pre b -> pre $ b /\ [])+ <$> (flip (\!) <$> pTm <* pKey "::" <|> pSucceed id)+ <*> pList1Sep pComma pTm_Op+ mkR h len b = Rule h len [] b Nothing Nothing Nothing++ pRules = pList (pR <* pKey ".")++ pQuery = concat <$> pList (pKey "?" *> pList1Sep pComma pTm_Op <* pKey ".")+ + pTm+ = pTm_Op++ pTm_Op+ = pTm_App <**>+ ( (\o r l -> GTm_Con o [l,r]) <$> pOp <*> pTm_App+ <|> pSucceed id+ )+ where pOp+ = pConsym+ <|> pVarsym+ <|> pKey "`" *> pConid <* pKey "`"+ <|> pCOLON++ pTm_App+ = GTm_Con <$> pConid <*> pList1 pTm_Base+ <|> (\o l r -> GTm_Con o [l,r]) <$> pParens pVarsym <*> pTm_Base <*> pTm_Base+ <|> pTm_Base++ pTm_Base+ = pTm_Var+ <|> (GTm_Int . read) <$> pInteger+ <|> GTm_Str <$> pString+ <|> flip GTm_Con [] <$> pConid+ <|> pParens pTm+ <|> pPacked (pKey "[") (pKey "]")+ ( pTm_App <**>+ ( (\t h -> foldr1 GTm_Cns (h:t)) <$ pCOLON <*> pList1Sep pCOLON pTm_App+ <|> (\t h -> foldr GTm_Cns GTm_Nil (h:t)) <$ pKey "," <*> pList1Sep (pKey ",") pTm_App+ <|> pSucceed (`GTm_Cns` GTm_Nil)+ )+ <|> pSucceed GTm_Nil+ )++ pTm_Var+ = GTm_Var <$> pVarid++ pCOLON = pKey ":"++
+ src/CHR/Language/WithTerm.hs view
@@ -0,0 +1,14 @@+-------------------------------------------------------------------------------------------+--- Abstract terms describing constraints, interpretation of ATerm apart from term itself+-------------------------------------------------------------------------------------------++module CHR.Language.WithTerm+ ( module CHR.Language.WithTerm.AST+ -- , module CHR.Language.WithTerm.Run+ )+ where++import CHR.Language.WithTerm.AST+-- import CHR.Language.WithTerm.Run++
+ src/CHR/Language/WithTerm/AST.hs view
@@ -0,0 +1,278 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-}++{-| Simple term language with some builtin guards and predicates + -}++module CHR.Language.WithTerm.AST+ ( Key'(..)+ + , C'(..)+ , G'(..)+ , P'(..)+ , E'+ , S'+ + , Var+ + , TmEval(..)+ + , TmOp+ )+ 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 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+++type Var = -- IVar+ String++data Key' op+ = Key_Int !Int + | Key_Var !Var + | Key_Str !String + | Key_Lst+ | Key_Op !op + | Key_Con !String + deriving (Eq, Ord, Show)++-- type Key = Key' POp++instance PP op => PP (Key' op) where+ pp (Key_Int i) = pp i+ pp (Key_Var v) = pp v+ pp (Key_Str s) = pp s+ pp (Key_Lst ) = ppParens "kl"+ pp (Key_Op o) = pp o+ pp (Key_Con s) = pp s++-- | Constraint+data C' tm+ = C_Con String [tm]+ | CB_Eq tm tm -- ^ builtin: unification+ | CB_Ne tm tm -- ^ builtin: non unification+ | CB_Fail -- ^ explicit fail+ deriving (Show, Eq, Ord, Typeable, Generic)++instance PP tm => PP (C' tm) where+ pp (C_Con c as) = c >#< ppSpaces as+ pp (CB_Eq x y ) = "unify" >#< ppSpaces [x,y]+ pp (CB_Ne x y ) = "not-unify" >#< ppSpaces [x,y]+ pp (CB_Fail ) = pp "fail"++-- | Guard+data G' tm+ = G_Eq tm tm -- ^ check for equality+ | G_Ne tm tm -- ^ check for inequality+ | G_Tm tm -- ^ determined by arithmetic evaluation+ deriving (Show, Typeable, Generic)++instance PP tm => PP (G' tm) where+ pp (G_Eq x y) = "is-eq" >#< ppParensCommas [x,y]+ pp (G_Ne x y) = "is-ne" >#< ppParensCommas [x,y]+ pp (G_Tm t ) = "eval" >#< ppParens t++type instance TT.TrTrKey (C' tm) = Key' (TmOp tm)++instance (TT.TrTrKey (C' tm) ~ TT.TrTrKey tm, TT.TreeTrieKeyable tm) => TT.TreeTrieKeyable (C' tm) where+ -- Only necessary for non-builtin constraints+ toTreeTriePreKey1 (C_Con c as) = TT.prekey1WithChildren (Key_Str {- $ "C_Con:" ++ -} c) as+ toTreeTriePreKey1 _ = TT.prekey1Nil++type E' tm = ()++newtype P' tm+ = P_Tm tm+ deriving (Eq, Ord, Show, Generic)++instance PP tm => PP (P' tm) where+ pp (P_Tm t) = pp t++instance TmMk tm => Bounded (P' tm) where+ minBound = P_Tm $ mkTmInt $ fromIntegral $ unPrio $ minBound+ maxBound = P_Tm $ mkTmInt $ fromIntegral $ unPrio $ maxBound++type S' tm = Map.Map Var tm+-- type S = MapH.HashMap Var Tm+-- type S = VAr.VecAlloc Tm+-- type S = Lk.DefaultScpsLkup Var Tm++type instance VarLookupKey (S' tm) = Var+type instance VarLookupVal (S' tm) = tm++instance PP tm => PP (S' tm) where+ pp = ppAssocLV . Lk.toList++type instance ExtrValVarKey (G' tm) = Var+type instance ExtrValVarKey (C' tm) = Var+type instance ExtrValVarKey (P' tm) = Var++type instance CHRMatchableKey (S' (tm op)) = Key' op++instance VarLookup (S' tm) where+ varlookupWithMetaLev _ = Lk.lookup+ varlookupKeysSetWithMetaLev _ = Lk.keysSet+ varlookupSingletonWithMetaLev _ = Lk.singleton+ varlookupEmpty = Lk.empty++instance Lk.LookupApply (S' tm) (S' tm) where+ apply = Lk.union++instance VarUpdatable tm (S' tm) => VarUpdatable (S' tm) (S' tm) where+ varUpd s = {- Lk.apply s . -} Lk.map (s `varUpd`) -- (|+>)++instance VarUpdatable tm (S' tm) => VarUpdatable (P' tm) (S' tm) where+ s `varUpd` p = case p of+ P_Tm t -> P_Tm (s `varUpd` t)++instance VarUpdatable tm (S' tm) => VarUpdatable (G' tm) (S' tm) where+ s `varUpd` G_Eq x y = G_Eq (s `varUpd` x) (s `varUpd` y)+ s `varUpd` G_Ne x y = G_Ne (s `varUpd` x) (s `varUpd` y)+ s `varUpd` G_Tm x = G_Tm (s `varUpd` x)++instance VarUpdatable tm (S' tm) => VarUpdatable (C' tm) (S' tm) where+ s `varUpd` c = case c of+ C_Con c as -> C_Con c $ map (s `varUpd`) as+ CB_Eq x y -> CB_Eq (s `varUpd` x) (s `varUpd` y)+ CB_Ne x y -> CB_Ne (s `varUpd` x) (s `varUpd` y)+ c -> c++instance (VarExtractable tm, ExtrValVarKey (G' tm) ~ ExtrValVarKey tm) => VarExtractable (G' tm) where+ varFreeSet (G_Eq x y) = Set.unions [varFreeSet x, varFreeSet y]+ varFreeSet (G_Ne x y) = Set.unions [varFreeSet x, varFreeSet y]+ varFreeSet (G_Tm x ) = varFreeSet x++instance (VarExtractable tm, ExtrValVarKey (C' tm) ~ ExtrValVarKey tm) => VarExtractable (C' tm) where+ varFreeSet (C_Con _ as) = Set.unions $ map varFreeSet as+ varFreeSet (CB_Eq x y ) = Set.unions [varFreeSet x, varFreeSet y]+ varFreeSet _ = Set.empty++instance (VarExtractable tm, ExtrValVarKey (P' tm) ~ ExtrValVarKey tm) => VarExtractable (P' tm) where+ varFreeSet (P_Tm t) = varFreeSet t++instance CHREmptySubstitution (S' tm) where+ chrEmptySubst = Lk.empty++instance IsConstraint (C' tm) where+ cnstrSolvesVia (C_Con _ _) = ConstraintSolvesVia_Rule+ cnstrSolvesVia (CB_Eq _ _) = ConstraintSolvesVia_Solve+ cnstrSolvesVia (CB_Ne _ _) = ConstraintSolvesVia_Solve+ cnstrSolvesVia (CB_Fail ) = ConstraintSolvesVia_Fail++instance (CHRMatchable (E' tm) tm (S' tm), TmIs tm, TmEval tm) => CHRCheckable (E' tm) (G' tm) (S' tm) where+ chrCheckM e g =+ case g of+ G_Eq t1 t2 -> chrUnifyM CHRMatchHow_Check e t1 t2+ G_Ne t1 t2 -> do+ menv <- getl chrmatcherstateEnv+ s <- getl chrmatcherstateVarLookup+ chrmatcherRun'+ (\e -> case e of {CHRMatcherFailure -> chrMatchSuccess; _ -> chrMatchFail})+ (\_ _ _ -> chrMatchFail)+ (chrCheckM e (G_Eq t1 t2)) menv s+ G_Tm t -> do+ e <- tmEval t+ case isTmBool e of+ Just True -> chrMatchSuccess+ _ -> chrMatchFail++class TmEval tm where+ tmEval :: tm -> CHRMatcher (S' tm) tm+ tmEvalOp :: TmOp tm -> [tm] -> CHRMatcher (S' tm) tm++instance (VarExtractable tm, CHRMatchable (E' tm) tm (S' tm), ExtrValVarKey (C' tm) ~ ExtrValVarKey tm) => CHRMatchable (E' tm) (C' tm) (S' tm) where+ chrUnifyM how e c1 c2 = do+ case (c1, c2) of+ (C_Con c1 as1, C_Con c2 as2) | c1 == c2 && length as1 == length as2 + -> sequence_ (zipWith (chrUnifyM how e) as1 as2)+ _ -> chrMatchFail+ chrBuiltinSolveM e b = case b of+ CB_Eq x y -> chrUnifyM CHRMatchHow_Unify e x y+ CB_Ne x y -> do+ menv <- getl chrmatcherstateEnv+ s <- getl chrmatcherstateVarLookup+ chrmatcherRun' (\_ -> chrMatchSuccess) (\_ _ _ -> chrMatchFail) (chrBuiltinSolveM e (CB_Eq x y)) menv s++instance (VarExtractable tm, CHRMatchable (E' tm) tm (S' tm), ExtrValVarKey (P' tm) ~ ExtrValVarKey tm) => CHRMatchable (E' tm) (P' tm) (S' tm) where+ chrUnifyM how e p1 p2 = do+ case (p1, p2) of+ (P_Tm t1 , P_Tm t2 ) -> chrUnifyM how e t1 t2++-- type instance CHRPrioEvaluatableVal (Tm' op) = Prio++instance ( TmValMk tm, TmIs tm, TmMk tm, TmEval tm, CHRPrioEvaluatableVal tm ~ Prio+ ) => CHRPrioEvaluatable (E' tm) tm (S' tm) where+ chrPrioEval e s t = case isTmInt $ chrmatcherRun' (\_ -> mkTmInt $ fromIntegral $ unPrio $ (minBound :: Prio)) (\_ _ x -> x) (tmEval t) emptyCHRMatchEnv (Lk.lifts s) of+ Just i -> fromIntegral i+ t -> minBound+ chrPrioLift _ _ = valTmMkInt . fromIntegral++type instance CHRPrioEvaluatableVal (P' tm) = Prio++instance ( CHRPrioEvaluatable (E' tm) tm (S' tm)+ , TmValMk tm, TmIs tm, TmMk tm, TmEval tm, CHRPrioEvaluatableVal tm ~ Prio+ ) => CHRPrioEvaluatable (E' tm) (P' tm) (S' tm) where+ chrPrioEval e s p = case p of+ P_Tm t -> chrPrioEval e s t+ chrPrioLift e s = P_Tm . chrPrioLift e s+++--------------------------------------------------------+++instance GTermAsTm tm => GTermAs (C' tm) (G' tm) (P' tm) (P' tm) where+ asHeadConstraint t = case t of+ GTm_Con c a -> forM a asTm >>= (return . C_Con c)+ t -> gtermasFail t "not a constraint"++ asBodyConstraint t = case t of+ GTm_Con "Fail" [] -> return CB_Fail+ GTm_Con o [a,b]+ | Just o' <- List.lookup o [("==", CB_Eq), ("/=", CB_Ne)] -> do+ a <- asTm a+ b <- asTm b+ return $ o' a b+ t -> asHeadConstraint t++ asGuard t = case t of+ GTm_Con o [a,b]+ | Just o' <- List.lookup o [("==", G_Eq), ("/=", G_Ne)] -> do+ a <- asTm a+ b <- asTm b+ return $ o' a b+ t -> fmap G_Tm $ asTm t+ + asHeadBacktrackPrio = fmap P_Tm . asTm++ asAltBacktrackPrio = asHeadBacktrackPrio+ asRulePrio = asHeadBacktrackPrio+++
+ src/CHR/Language/WithTerm/Run.hs view
@@ -0,0 +1,147 @@+{-# LANGUAGE ScopedTypeVariables, TypeFamilies #-}++module CHR.Language.WithTerm.Run+ ( RunOpt(..)+ , Verbosity(..)++ , runFile+ )+ where++import Data.Maybe+import System.IO+import Data.Time.Clock.POSIX+import Data.Time.Clock.System+import Data.Time.Clock.TAI+import Control.Monad+import Control.Monad.IO.Class+import Control.Monad.State.Class+import qualified Data.Set as Set++import CHR.Parse+import CHR.Scan++import CHR.Data.Substitutable+import CHR.Pretty+import CHR.Utils+import CHR.Data.Lens+import qualified CHR.Data.TreeTrie as TT+-- import qualified UHC.Util.CHR.Solve.TreeTrie.Internal.Shared as TT+import qualified CHR.Data.Lookup as Lk+import CHR.Types.Rule+import CHR.Types+import CHR.Language.Generic.AST+import CHR.Language.Generic.Parser+import CHR.Solve.MonoBacktrackPrio as MBP+import CHR.Language.WithTerm.AST+-- import CHR.Language.Examples.Term.Visualizer++import qualified GHC.Exts as Prim++data RunOpt+ = RunOpt_DebugTrace -- ^ include debugging trace in output+ | RunOpt_SucceedOnLeftoverWork -- ^ left over unresolvable (non residue) work is also a successful result+ | RunOpt_SucceedOnFailedSolve -- ^ failed solve is considered also a successful result, with the failed constraint as a residue+ | RunOpt_WriteVisualization -- ^ write visualization (html file) to disk+ | RunOpt_Verbosity Verbosity+ deriving (Eq)++mbRunOptVerbosity :: [RunOpt] -> Maybe Verbosity+mbRunOptVerbosity [] = Nothing+mbRunOptVerbosity (RunOpt_Verbosity v : _) = Just v+mbRunOptVerbosity (_ : r) = mbRunOptVerbosity r++-- | Run file with options+{-# INLINEABLE runFile #-}+runFile+ :: forall proxy tm+ . ( MonoBacktrackPrio (C' tm) (G' tm) (P' tm) (P' tm) (S' tm) (E' tm) IO+ , VarUpdatable tm (S' tm)+ , TmMk tm+ , PP tm+ )+ => proxy tm+ -> [RunOpt]+ -> ([C' tm] -> SolveTrace' (C' tm) (StoredCHR (C' tm) (G' tm) (P' tm) (P' tm)) (S' tm) -> PP_Doc)+ -> FilePath+ -> IO ()+runFile _ runopts chrVisualize f = do+ -- scan, parse+ msg $ "READ " ++ f + mbParse <- parseFile f+ case mbParse of+ Left e -> putPPLn e+ Right (prog, query, varToNmMp) -> do+ let verbosity = maximum $ [Verbosity_Quiet] ++ maybeToList (mbRunOptVerbosity runopts) ++ (if RunOpt_DebugTrace `elem` runopts then [Verbosity_ALot] else [])+ sopts = defaultCHRSolveOpts+ { chrslvOptSucceedOnLeftoverWork = RunOpt_SucceedOnLeftoverWork `elem` runopts+ , chrslvOptSucceedOnFailedSolve = RunOpt_SucceedOnFailedSolve `elem` runopts+ , chrslvOptGatherDebugInfo = verbosity >= Verbosity_Debug+ , chrslvOptGatherTraceInfo = RunOpt_WriteVisualization `elem` runopts || verbosity >= Verbosity_ALot+ }+ mbp :: CHRMonoBacktrackPrioT (C' tm) (G' tm) (P' tm) (P' tm) (S' tm) (E' tm) IO (SolverResult (S' tm))+ mbp = do+ -- print program+ liftIO $ putPPLn $ "Rules" >-< indent 2 (vlist $ map pp prog)+ -- liftIO $ putPPLn $ "Rule TT keys" >-< indent 2 (vlist $ map (pp . TT.chrToKey . head . ruleHead) prog)+ -- liftIO $ putPPLn $ "Rule TT2 keys" >-< indent 2 (vlist $ map (pp . TT.toTreeTrieKey) prog)+ -- freshen query vars+ query <- slvFreshSubst Set.empty query >>= \s -> return $ s `varUpd` query+ -- print query+ liftIO $ putPPLn $ "Query" >-< indent 2 (vlist $ map pp query)+ mapM_ addRule prog+ mapM_ addConstraintAsWork query+ -- solve+ liftIO $ msg $ "SOLVE " ++ f+ r <- (Prim.inline chrSolve) sopts ()+ ppSolverResult verbosity r >>= \sr -> liftIO $ putPPLn $ "Solution" >-< indent 2 sr+ if (RunOpt_WriteVisualization `elem` runopts)+ then+ do+ (CHRGlobState{_chrgstTrace = trace}, _) <- get+ time <- liftIO getPOSIXTime+ let fileName = "visualization-" ++ show (round time) ++ ".html"+ liftIO $ writeFile fileName (showPP $ chrVisualize query trace)+ liftIO $ msg "VISUALIZATION"+ liftIO $ putStrLn $ "Written visualization as " ++ fileName+ else (return ())+ return r+ tBef <- getSystemTime + (_,(gs,_)) <- runCHRMonoBacktrackPrioT+ (chrgstVarToNmMp ^= Lk.inverse (flip (,)) varToNmMp $ emptyCHRGlobState)+ (emptyCHRBackState {- _chrbstBacktrackPrio=0 -}) {- 0 -}+ mbp+ tAft <- getSystemTime+ let tDif = systemToTAITime tAft `diffAbsoluteTime` systemToTAITime tBef+ nSteps = gs ^. MBP.chrgstStatNrSolveSteps++ -- done+ msg $ "DONE (" ++ show tDif ++ " / " ++ show nSteps ++ " = " ++ show (tDif / fromIntegral nSteps) ++ ") " ++ f+ + where+ msg m = putStrLn $ "---------------- " ++ m ++ " ----------------"+ -- dummy = undefined :: Rule C G P P++{-+-- | run some test programs+mainTerm = do+ forM_+ [+ "typing2"+ -- , "queens"+ -- , "leq"+ -- , "var"+ -- , "ruleprio"+ -- , "backtrack3"+ -- , "unify"+ -- , "antisym"+ ] $ \f -> do+ let f' = "test/" ++ f ++ ".chr"+ runFile+ [ RunOpt_SucceedOnLeftoverWork+ , RunOpt_DebugTrace+ ] f'+-}++{-+-}