diff --git a/chr-lang.cabal b/chr-lang.cabal --- a/chr-lang.cabal +++ b/chr-lang.cabal @@ -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 diff --git a/src/CHR/Language/Examples/Term/AST.hs b/src/CHR/Language/Examples/Term/AST.hs --- a/src/CHR/Language/Examples/Term/AST.hs +++ b/src/CHR/Language/Examples/Term/AST.hs @@ -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 + diff --git a/src/CHR/Language/Examples/Term/Run.hs b/src/CHR/Language/Examples/Term/Run.hs --- a/src/CHR/Language/Examples/Term/Run.hs +++ b/src/CHR/Language/Examples/Term/Run.hs @@ -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 diff --git a/src/CHR/Language/Examples/Term/Visualizer.hs b/src/CHR/Language/Examples/Term/Visualizer.hs --- a/src/CHR/Language/Examples/Term/Visualizer.hs +++ b/src/CHR/Language/Examples/Term/Visualizer.hs @@ -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 diff --git a/src/CHR/Language/GTerm.hs b/src/CHR/Language/GTerm.hs deleted file mode 100644 --- a/src/CHR/Language/GTerm.hs +++ /dev/null @@ -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 - - diff --git a/src/CHR/Language/GTerm/AST.hs b/src/CHR/Language/GTerm/AST.hs deleted file mode 100644 --- a/src/CHR/Language/GTerm/AST.hs +++ /dev/null @@ -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) diff --git a/src/CHR/Language/GTerm/Parser.hs b/src/CHR/Language/GTerm/Parser.hs deleted file mode 100644 --- a/src/CHR/Language/GTerm/Parser.hs +++ /dev/null @@ -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 ":" - - diff --git a/src/CHR/Language/Generic.hs b/src/CHR/Language/Generic.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/Generic.hs @@ -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 + + diff --git a/src/CHR/Language/Generic/AST.hs b/src/CHR/Language/Generic/AST.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/Generic/AST.hs @@ -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) diff --git a/src/CHR/Language/Generic/Parser.hs b/src/CHR/Language/Generic/Parser.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/Generic/Parser.hs @@ -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 ":" + + diff --git a/src/CHR/Language/WithTerm.hs b/src/CHR/Language/WithTerm.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/WithTerm.hs @@ -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 + + diff --git a/src/CHR/Language/WithTerm/AST.hs b/src/CHR/Language/WithTerm/AST.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/WithTerm/AST.hs @@ -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 + + + diff --git a/src/CHR/Language/WithTerm/Run.hs b/src/CHR/Language/WithTerm/Run.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/WithTerm/Run.hs @@ -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' +-} + +{- +-}