diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for chr-lang + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2017, Atze Dijkstra + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Atze Dijkstra nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/chr-lang.cabal b/chr-lang.cabal new file mode 100644 --- /dev/null +++ b/chr-lang.cabal @@ -0,0 +1,65 @@ +-- Initial chr-lang.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: chr-lang +version: 0.1.0.0 +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 +Bug-Reports: https://github.com/atzedijkstra/chr/issues +license: BSD3 +license-file: LICENSE +author: Atze Dijkstra +maintainer: atzedijkstra@gmail.com +-- copyright: +category: Development +build-type: Simple +extra-source-files: ChangeLog.md +cabal-version: >=1.10 + +source-repository head + type: git + location: git@github.com:atzedijkstra/chr.git + +library + exposed-modules: + CHR.Language.GTerm, + CHR.Language.GTerm.AST, + CHR.Language.GTerm.Parser, + CHR.Language.Examples.Term.AST, + CHR.Language.Examples.Term.Run, + CHR.Language.Examples.Term.Visualizer + -- other-modules: + -- other-extensions: + default-extensions: + MultiParamTypeClasses, + FunctionalDependencies, + FlexibleContexts, + DeriveGeneric + build-depends: + base >=4.9 && < 5, + containers >= 0.4, + hashable >= 1.2.4, + unordered-containers >= 0.2.7, + fgl >= 5.4, + mtl >= 2, + time >= 1.2, + chr-parse >= 0.1.0.0, + chr-pretty >= 0.1.0.0, + chr-data >= 0.1.0.0, + chr-core >= 0.1.0.0 + hs-source-dirs: src + default-language: Haskell2010 + +executable chr-term + main-is: Main.hs + -- other-modules: + -- other-extensions: + + build-depends: + base >=4.9 && < 5, + chr-data >= 0.1.0.0, + chr-lang + + hs-source-dirs: src-main + default-language: Haskell2010 diff --git a/src-main/Main.hs b/src-main/Main.hs new file mode 100644 --- /dev/null +++ b/src-main/Main.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE TemplateHaskell #-} + +module Main where + +import System.Environment +import System.Console.GetOpt +import System.Exit +import Control.Monad + +import CHR.Data.Lens +import CHR.Language.Examples.Term.Run + +-- | Immediate quit options +data ImmQuit + = ImmQuit_Help + +-- | Program options +data Opts + = Opts + { _optVerbosity :: Verbosity + , _optSucceedOnNoWorkLeft :: Bool + , _optSucceedOnFailedSolve :: Bool + , _optShowVisualization :: Bool + , _optImmQuit :: [ImmQuit] + } + +mkLabel ''Opts + +defaultOpts :: Opts +defaultOpts + = Opts + { _optVerbosity = Verbosity_Quiet + , _optSucceedOnNoWorkLeft = False + , _optSucceedOnFailedSolve = False + , _optShowVisualization = False + , _optImmQuit = [] + } + +-- | Options for 'getOpt' +options :: [OptDescr (Opts -> Opts)] +options = + [ mk "v" ["verbose"] "extra output, debugging output" + (OptArg (maybe (optVerbosity ^= Verbosity_Normal) (\l -> optVerbosity ^= toEnum (read l))) "LEVEL") + , mk "s" ["succeed-only-without-leftover"] "succeed only if no work is left over" + (NoArg $ optSucceedOnNoWorkLeft ^= True) + , mk "" ["succeed-on-failed"] "failed solve is considered also a successful result, with the failed constraint as a residue" + (NoArg $ optSucceedOnFailedSolve ^= True) + , mk "" ["visualize"] "create visualization" + (NoArg $ optShowVisualization ^= True) + , mk "h" ["help"] "print this help" + (NoArg $ optImmQuit ^$= (ImmQuit_Help :)) + ] + where + mk so lo desc o = Option so lo o desc + +-- RunOpt_Verbosity + +main = do + args <- getArgs + progname <- getProgName + + case getOpt Permute options args of + -- options ok + (o,[fn],[]) -> do + let opts = foldl (flip id) defaultOpts o + case _optImmQuit opts of + imm@(_:_) -> forM_ imm $ \iq -> case iq of + ImmQuit_Help -> printUsage progname [] + + -- no immediate quit options + _ -> do + flip runFile fn $ + [RunOpt_Verbosity $ _optVerbosity opts] ++ + (if _optSucceedOnNoWorkLeft opts then [] else [RunOpt_SucceedOnLeftoverWork]) ++ + (if _optShowVisualization opts then [RunOpt_WriteVisualization] else []) ++ + (if _optSucceedOnFailedSolve opts then [RunOpt_SucceedOnFailedSolve] else []) + + (_,_,errs) -> do + printUsage progname errs + exitFailure + + return () + + where + printUsage progname errs = putStrLn $ concat errs ++ usageInfo (header progname) options + header progname = "Usage: " ++ progname ++ " [OPTION...] file\n\nOptions:" + diff --git a/src/CHR/Language/Examples/Term/AST.hs b/src/CHR/Language/Examples/Term/AST.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/Examples/Term/AST.hs @@ -0,0 +1,415 @@ +{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-} + +{-| Simple term language with some builtin guards and predicates + -} + +module CHR.Language.Examples.Term.AST + ( Tm(..) + , C(..) + , G(..) + , P(..) + , POp(..) + , E + , S + + , Var + ) + 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 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 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 + = 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 + = 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 + deriving (Show, Eq, Ord, Typeable, Generic) + +instance VarTerm Tm where + varTermMbKey (Tm_Var v) = Just v + varTermMbKey _ = Nothing + varTermMkKey = Tm_Var + +instance PP Tm where + pp (Tm_Var v ) = pp v -- "v" >|< v + pp (Tm_Con c [] ) = pp c + pp (Tm_Con c as ) = ppParens $ c >#< ppSpaces as + pp (Tm_Lst h mt ) = let l = ppBracketsCommas h in maybe l (\t -> ppParens $ l >#< ":" >#< t) mt + pp (Tm_Op o [a ]) = ppParens $ o >#< a + pp (Tm_Op o [a1,a2]) = ppParens $ a1 >#< o >#< a2 + pp (Tm_Int i ) = pp i + pp (Tm_Str s ) = pp $ show s + pp (Tm_Bool b ) = pp b + +-- 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 instance TrTrKey Tm = Key +type instance TrTrKey C = Key + +type instance TT.TrTrKey Tm = Key +type instance TT.TrTrKey C = Key + +instance TT.TreeTrieKeyable Tm where + toTreeTriePreKey1 (Tm_Var v) = TT.prekey1Wild + toTreeTriePreKey1 (Tm_Int i) = TT.prekey1 $ Key_Int i + toTreeTriePreKey1 (Tm_Str s) = TT.prekey1 $ Key_Str {- $ "Tm_Str:" ++ -} s + toTreeTriePreKey1 (Tm_Bool i) = TT.prekey1 $ Key_Int $ fromEnum i + toTreeTriePreKey1 (Tm_Con c as) = TT.prekey1WithChildren (Key_Str {- $ "Tm_Con:" ++ -} c) as + toTreeTriePreKey1 (Tm_Op op as) = TT.prekey1WithChildren (Key_Op op) as + toTreeTriePreKey1 (Tm_Lst h _ ) = TT.prekey1WithChildren Key_Lst h + +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 = () + +-- | Binary operator +data POp + = + -- binary + PBOp_Add + | PBOp_Sub + | PBOp_Mul + | PBOp_Mod + | PBOp_Lt + | PBOp_Le + + -- unary + | PUOp_Abs + deriving (Eq, Ord, Show, Generic) + +instance PP POp where + pp PBOp_Add = pp "+" + pp PBOp_Sub = pp "-" + pp PBOp_Mul = pp "*" + pp PBOp_Mod = pp "mod" + pp PBOp_Lt = pp "<" + pp PBOp_Le = pp "<=" + pp PUOp_Abs = pp "abs" + +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 + +instance Lk.LookupApply S S where + apply = Lk.union + +instance VarUpdatable S S where + varUpd s = {- Lk.apply s . -} Lk.map (s `varUpd`) -- (|+>) + +instance VarUpdatable Tm S 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 + 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 + chrUnifyM how e t1 t2 = case (t1, t2) of + (Tm_Con c1 as1, Tm_Con c2 as2) | c1 == c2 -> chrUnifyM how e as1 as2 + (Tm_Lst (h1:t1) mt1, Tm_Lst (h2:t2) mt2) -> chrUnifyM how e h1 h2 >> chrUnifyM how e (Tm_Lst t1 mt1) (Tm_Lst t2 mt2) + (Tm_Lst [] (Just t1), l2@(Tm_Lst {})) -> chrUnifyM how e t1 l2 + (l1@(Tm_Lst {}), Tm_Lst [] (Just t2)) -> chrUnifyM how e l1 t2 + (Tm_Lst [] mt1, Tm_Lst [] mt2) -> chrUnifyM how e mt1 mt2 + (Tm_Op o1 as1, Tm_Op o2 as2) | how < CHRMatchHow_Unify && o1 == o2 + -> chrUnifyM how e as1 as2 + (Tm_Op o1 as1, t2 ) | how == CHRMatchHow_Unify -> tmEvalOp o1 as1 >>= \t1 -> chrUnifyM how e t1 t2 + (t1 , Tm_Op o2 as2) | how == CHRMatchHow_Unify -> tmEvalOp o2 as2 >>= \t2 -> chrUnifyM how e t1 t2 + (Tm_Int i1 , Tm_Int i2 ) | i1 == i2 -> chrMatchSuccess + (Tm_Str s1 , Tm_Str s2 ) | s1 == s2 -> chrMatchSuccess + (Tm_Bool b1 , Tm_Bool b2 ) | b1 == b2 -> chrMatchSuccess + _ -> chrMatchResolveCompareAndContinue how (chrUnifyM how e) t1 t2 + +tmEval :: Tm -> CHRMatcher S Tm +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 + +instance CHRPrioEvaluatable E P S where + chrPrioEval e s p = case p of + P_Tm t -> chrPrioEval e s t + chrPrioLift = P_Tm . chrPrioLift + + +-------------------------------------------------------- + +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" + + 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 + + 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 + + asAltBacktrackPrio = asHeadBacktrackPrio + asRulePrio = asHeadBacktrackPrio + + 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" + +-------------------------------------------------------- +-- leq example, backtrack prio specific + diff --git a/src/CHR/Language/Examples/Term/Run.hs b/src/CHR/Language/Examples/Term/Run.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/Examples/Term/Run.hs @@ -0,0 +1,131 @@ +module CHR.Language.Examples.Term.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.GTerm.Parser +import CHR.Solve.MonoBacktrackPrio as MBP +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) + +mbRunOptVerbosity :: [RunOpt] -> Maybe Verbosity +mbRunOptVerbosity [] = Nothing +mbRunOptVerbosity (RunOpt_Verbosity v : _) = Just v +mbRunOptVerbosity (_ : r) = mbRunOptVerbosity r + +-- | 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' + + +{- +-} diff --git a/src/CHR/Language/Examples/Term/Visualizer.hs b/src/CHR/Language/Examples/Term/Visualizer.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/Examples/Term/Visualizer.hs @@ -0,0 +1,569 @@ +{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-} + +module CHR.Language.Examples.Term.Visualizer + ( chrVisualize + ) + where + +import Prelude +import Data.Maybe +import Data.List +import qualified Data.Map as Map +import CHR.Pretty +import qualified CHR.Data.Lookup as Lk +import CHR.Types +import CHR.Types.Rule +import CHR.Language.GTerm.Parser +-- import UHC.Util.CHR.Solve.TreeTrie.Mono +import CHR.Solve.MonoBacktrackPrio as MBP +import CHR.Language.Examples.Term.AST +-- import UHC.Util.CHR.Solve.TreeTrie.Internal +-- import UHC.Util.CHR.Solve.TreeTrie.Internal.Shared +import CHR.Data.Substitutable +import Data.Graph.Inductive.Graph +import Data.Graph.Inductive.Tree + +sortGroupOn :: Ord b => (a -> b) -> [a] -> [[a]] +sortGroupOn f = construct . sortOn f + where + construct [] = [] + construct (y:ys) = group : construct rest + where + group = y : takeWhile ((f y ==) . f) ys + rest = dropWhile ((f y ==) . f) ys + +data NodeData + -- Applied rule with first alt (if it exists) + = NodeRule + { nrLayer :: Int + , nrColumn :: Int + , nrName :: String + , nrRuleVars :: [Tm] + , nrFirstAlt :: Maybe C + } + -- Additional alts of a rule + | NodeAlt + { naLayer :: Int + , naColumn :: Int + , naConstraint :: C + } + -- Added node to make a proper layered graph + -- A proper layered graph is a graph in which all edges + -- go from a layer to the next layer. To satisfy this, + -- we add synthesized nodes on edges that do not skip one + -- or more layers + | NodeSynthesized + { nsLayer :: Int + , nsColumn :: Int + , nsEdgeKind :: EdgeKind + } + +data EdgeKind + = EdgeGuard -- Usage of term in guard of rule. + | EdgeHead -- Usage of term in head of rule. + | EdgeUnify -- Usage of some term that required unification of this node. + | EdgeAlt -- Link between NodeRule and NodeAlt. Both nodes have same layer. + deriving Eq + +type Node' = LNode NodeData +-- | Edge has a kind and a bool that says whether this edge is +-- the last edge of a sequence of edges. The last edge does not +-- end in a synthesized node, the others do. +type Edge' = LEdge (EdgeKind, Bool) +type NodeEdge = (Node', Node', EdgeKind, Bool) + +asEdge :: NodeEdge -> Edge' +asEdge ((from, _), (to, _), kind, isLast) = (from, to, (kind, isLast)) + +-- | Gets the layer of a node +nodeLayer :: Node' -> Int +nodeLayer (_, NodeRule{nrLayer = layer}) = layer +nodeLayer (_, NodeAlt{naLayer = layer}) = layer +nodeLayer (_, NodeSynthesized{nsLayer = layer}) = layer + +-- | Gets the column of a node +nodeColumn :: Node' -> Int +nodeColumn (_, NodeRule{nrColumn = col}) = col +nodeColumn (_, NodeAlt{naColumn = col}) = col +nodeColumn (_, NodeSynthesized{nsColumn = col}) = col + +-- | Sets the column of a node +nodeSetColumn :: Node' -> Int -> Node' +nodeSetColumn (n, d@NodeRule{}) col = (n, d{nrColumn = col}) +nodeSetColumn (n, d@NodeAlt{}) col = (n, d{naColumn = col}) +nodeSetColumn (n, d@NodeSynthesized{}) col = (n, d{nsColumn = col}) + +-- | A map between a term, and the location where it was found combined +-- with the required unifications +type NodeMap = Map.Map Tm (Node', [Node']) +-- | Contains all data needed to build the graph, during traversal of +-- the solve trace +data BuildState = BuildState [Node'] [NodeEdge] NodeMap Int Int +emptyBuildState :: BuildState +emptyBuildState = BuildState [] [] Map.empty 0 0 + +-- | Gives all terms that follow after a unification +replaceInTm :: Tm -> Tm -> Tm -> [Tm] +replaceInTm a b tm + | tm == a || tm == b = [a, b] + | otherwise = case tm of + Tm_Con name tms -> fmap (Tm_Con name) (replaceList tms) + Tm_Lst tms ltm -> do + tms' <- replaceList tms + ltm' <- replaceMaybe ltm + return $ Tm_Lst tms' ltm' + Tm_Op op tms -> fmap (Tm_Op op) (replaceList tms) + x -> [x] + where + replaceList = sequence . fmap (replaceInTm a b) + replaceMaybe Nothing = [Nothing] + replaceMaybe (Just y) = fmap Just $ replaceInTm a b y + +-- | Gives all terms in a constraint +tmsInC :: C -> [Tm] +tmsInC (C_Con s tms) = [Tm_Con s tms] +tmsInC _ = [] + +-- | Gives all terms in a guard +tmsInG :: G -> [Tm] +tmsInG (G_Tm tm) = tmsInTm tm +tmsInG _ = [] + +tmsInTm :: Tm -> [Tm] +tmsInTm tm = tm : children tm + where + children (Tm_Lst as Nothing) = as + children (Tm_Lst as (Just a)) = as ++ [a] + children _ = [] + +-- | Finds all terms that were used for this rule +-- Used by visualizer to draw edges to the origin of +-- these rules. +precedentTms :: Rule C G P P -> [(Tm, EdgeKind)] +precedentTms rule + = fmap (\n -> (n, EdgeHead)) (concatMap tmsInC $ ruleHead rule) + ++ fmap (\n -> (n, EdgeGuard)) (concatMap tmsInG $ ruleGuard rule) + +-- | Adds the constraint (of an alt) to the NodeMap +addConstraint :: C -> Node' -> NodeMap -> NodeMap +addConstraint (CB_Eq a b) = addUnify a b +addConstraint (C_Con s tms) = addTerm $ Tm_Con s tms +addConstraint c = const id + +addTerm :: Tm -> Node' -> NodeMap -> NodeMap +addTerm tm node = Map.insert tm (node, []) + +addUnify :: Tm -> Tm -> Node' -> NodeMap -> NodeMap +addUnify a b node map = Map.foldlWithKey cb map map + where + cb :: NodeMap -> Tm -> (Node', [Node']) -> NodeMap + cb map' tm (n, nodes) = foldl (\map'' key -> Map.insertWith compare key (n, node : nodes) map'') map' (replaceInTm a b tm) + compare x@(_, nodes1) y@(_, nodes2) + | length nodes1 <= length nodes2 = x + | otherwise = y + +-- | Generates nodes and edges for a SolveStep. +-- Stores the resulting terms in the NodeMap. +stepToNodes :: BuildState -> SolveStep' C (MBP.StoredCHR C G P P) S -> BuildState +stepToNodes state@(BuildState _ _ nodeMap nodeId layer) step + = BuildState + nodes + edges'' + nodeMap' + nodeId' + layer' + where + schr = stepChr step + rule = storedChrRule' schr + updRule = varUpd (stepSubst step) rule + alt = maybe [] (fmap $ varUpd $ stepSubst step) $ stepAlt step + (BuildState nodes edges' nodeMap' nodeId' layer', primaryNode) = + createNodes + (maybe "[untitled]" id (ruleName rule)) + (Lk.elems (stepSubst step)) + alt + state + edges'' = + ( fmap (\(n, kind) -> (n, primaryNode, kind, True)) + $ concatMap (\(n, ns, kind) -> (n, kind) : fmap (\x -> (x, EdgeUnify)) ns) + $ mapMaybe + (\(tm, kind) -> fmap + (\(n, ns) -> (n, ns, kind)) + (Map.lookup tm nodeMap)) + (precedentTms updRule) + ) + ++ edges' + +createNodes :: String -> [Tm] -> [C] -> BuildState -> (BuildState, Node') +createNodes name vars alts (BuildState previousNodes previousEdges nodeMap nodeId layer) + = ( BuildState (nodes ++ previousNodes) (edges ++ previousEdges) nodeMap' (nodeId + max 1 (length alts)) (layer + 1) + , primaryNode + ) + where + primaryNode = + (nodeId, NodeRule + { nrLayer = layer + , nrColumn = 0 + , nrName = name + , nrRuleVars = vars + , nrFirstAlt = listToMaybe alts + } + ) + nodes = primaryNode : altNodes + altTms = concatMap tmsInC alts + nodeMap' = foldl updateMap nodeMap nodes + -- Updates node map for a new node + updateMap :: NodeMap -> Node' -> NodeMap + updateMap map node@(_, NodeRule{ nrFirstAlt = Just alt }) = addConstraint alt node map + updateMap map node@(_, NodeAlt{ naConstraint = alt }) = addConstraint alt node map + updateMap map _ = map + + altNode (constraint, i) = (nodeId + i, NodeAlt layer 0 constraint) + altNodes = fmap altNode (drop 1 $ addIndices alts) + edges = (fmap (\n -> (primaryNode, n, EdgeAlt, True)) altNodes) + +-- | Adds synthesized nodes to create a proper layered graph +createSynthesizedNodes :: [Node'] -> [NodeEdge] -> Int -> ([NodeEdge], [Node']) +createSynthesizedNodes nodes es firstNode + = create es firstNode [] [] + where + create :: [NodeEdge] -> Int -> [NodeEdge] -> [Node'] -> ([NodeEdge], [Node']) + create ((edge@(from, to, kind, _)):edges) id accumEdges accumNodes + = create edges id' (es ++ accumEdges) (ns ++ accumNodes) + where + (es, ns, id') = split (nodeLayer from) edge id + create _ _ accumEdges accumNodes = (accumEdges, accumNodes) + split :: Int -> NodeEdge -> Int -> ([NodeEdge], [Node'], Int) + split fromLayer edge@(from, to, kind, _) id + | fromLayer + 1 >= nodeLayer to = ([edge], [], id) + | otherwise = + ( (from, node, kind, False) : edges', + node : nodes', + id' + ) + where + node = (id, (NodeSynthesized (fromLayer + 1) 0 kind)) + (edges', nodes', id') = split (fromLayer + 1) (node, to, kind, True) (id + 1) + +-- | Creates a graph with the visualization +createGraph :: [C] -> [SolveStep' C (MBP.StoredCHR C G P P) S] -> Gr NodeData (EdgeKind, Bool) +createGraph query steps = mkGraph sortedLayers (fmap asEdge edges) + where + -- | Sort the layers by giving each node in a layer an unique nodeColumn value + sortedLayers = sortedFirstLayer ++ sortNodes maxLayerSize (sortedFirstLayer : layers) layeredEdges + -- | Set the nodeColumn values of each of the nodes in the query (the query forms the first layer) + sortedFirstLayer = uniqueColumns firstLayer ((maxLayerSize - length firstLayer) `div` 2) + -- | Extracting [[Node']] from layerNodes + firstLayer : layers = sortGroupOn nodeLayer nodes + -- firstLayer : layers = Map.elems $ layerNodes nodes + -- | For each layer we create a list with the nodes in that layer + -- layerNodes :: [Node'] -> Map.Map Int [Node'] + -- layerNodes ns = foldl (\m x -> Map.insertWith (++) (nodeLayer x) [x] m) Map.empty ns + (state, _) = createNodes "?" [] query emptyBuildState + BuildState nodes' edges' _ id _ = foldr (flip stepToNodes) state steps + (edges, synNodes) = createSynthesizedNodes nodes' edges' id + nodes = nodes' ++ synNodes + maxLayerSize = maximum $ fmap length (firstLayer : layers) + edgesCrossLayer = filter (\(from, to, _, _) -> nodeLayer from /= nodeLayer to) edges + layeredEdges = sortGroupOn (nodeLayer . fst') edgesCrossLayer + +-- | Sort the nodes using the median heuristic +-- | The first layer is left as it was, the second layer is sorted using the first etc. +sortNodes :: Int -> [[Node']] -> [[NodeEdge]] -> [Node'] +sortNodes _ (x:[]) _ = [] +sortNodes maxLayerSize (x:xs:xss) e = medianHeurstic maxLayerSize x xs edges ++ sortNodes maxLayerSize (xs:xss) rest + where + (edges, rest) = + if null e then + ([], []) + else if (nodeLayer $ fst' $ head $ head e) == nodeLayer (head x) then + (head e, tail e) + else + ([], e) + +-- | lowerLayer is the layer to be sorted, upperLayer is assumed to be sorted +-- | The maxLayerSize is used to center the graph (by altering the value given to uniqueColumns) +-- | Documentation for the median heuristic: +-- | https://cs.brown.edu/~rt/gdhandbook/chapters/hierarchical.pdf +-- | http://www.cs.usyd.edu.au/~shhong/fab.pdf +-- | https://books.google.nl/books?id=6hfsCAAAQBAJ&lpg=PA28&dq=median%20heuristic%20sorting%20vertices&hl=nl&pg=PA28#v=onepage&q&f=false +medianHeurstic :: Int -> [Node'] -> [Node'] -> [NodeEdge] -> [Node'] +medianHeurstic maxLayerSize upperLayer lowerLayer e = uniqueColumns sortedMedianList ((maxLayerSize - length lowerLayer) `div` 2) + where + -- | The medianList sorted on the median values + sortedMedianList = sortOn nodeColumn medianList + -- | The list of median values for each of the nodes in lowerLayer + medianList = map (\x -> nodeSetColumn x (median x)) lowerLayer + -- | The median value of the x coördinates of the neighbors + median n + | neighborCount == 0 = 0 + | otherwise = coords !! (ceiling (realToFrac neighborCount / 2) - 1) + where + coords = coordinates n + neighborCount = length coords + -- | The values of the x coördinates of the neighbors + coordinates n = map nodeColumn (neighbors n) + -- | The neighbor nodes of the given Node' n (on a higher layer) + neighbors n = map (fst') (edges n) + -- | All the edges connected to given Node' n + edges n = filter (\(_, (id, _), _, _) -> id == fst n) e + +-- | Ensure that each Node' has an unique nodeColumn (the x coördinate) +-- | The value of the nodeColumn is set to i +uniqueColumns :: [Node'] -> Int -> [Node'] +uniqueColumns (n:ns) i = nodeSetColumn n i : uniqueColumns ns (i + 1) +uniqueColumns _ _ = [] + +fst' :: (a, b, c, d) -> a +fst' (a, _, _, _) = a + +-- | Creates a HTML tag +tag :: String -> PP_Doc -> PP_Doc -> PP_Doc +tag name attr content = (text ("<" ++ name)) >|< attributes attr >|< body content + where + attributes Emp = Emp + attributes a = text " " >|< a + body Emp = text " />" + body content = text ">" >|< content >|< text ("") + +-- | Creates a HTML tag without attributes +tag' :: String -> PP_Doc -> PP_Doc +tag' name = tag name Emp + +-- | Add indices to an array as a tuple with value and index +addIndices :: [a] -> [(a, Int)] +addIndices = flip zip [0..] + +-- | Generates HTML for a node +showNode :: (Node' -> (Int, Int)) -> Node' -> PP_Doc +showNode pos node@(_, NodeRule{nrLayer = layer, nrName = name, nrRuleVars = vars, nrFirstAlt = alt}) = tag "div" + ( + text "class=\"rule\" style=\"top: " + >|< pp (y + 10) + >|< text "px; left: " + >|< pp x + >|< text "px;\"" + ) + ( + tag "span" (text "class=\"" >|< className >|< text "\"") ( + (text name) + >|< (hlist (fmap ((" " >|<) . pp) vars)) + ) + >|< tag' "br" Emp + >|< text "↳" + >|< tag "span" (text "class=\"rule-alt\"") altText + ) + where + (x, y) = pos node + altText = maybe (text ".") pp alt + className = text "rule-text" + showUsage name var = tag "div" (text $ "class=\"" ++ className ++ "\"") (text " ") + where + className = name ++ " var-" ++ var +showNode pos node@(_, NodeAlt{ naConstraint = constraint }) = tag "div" + ( + text "class=\"rule-additional-alt\" style=\"top: " + >|< pp (y + 10) + >|< text "px; left: " + >|< pp x + >|< text "px;\"" + ) + ( + text "↳" + >|< tag "span" (text "class=\"rule-alt\"") (pp constraint) + ) + where + (x, y) = pos node +showNode _ (_, NodeSynthesized{}) = Emp + +-- | Generates HTML for an edge +showEdge :: (Node -> (Int, Int)) -> Edge' -> PP_Doc +showEdge pos (from, to, (kind, isEnd)) = + if kind == EdgeAlt then + -- Edge between rule and alt of same rule + tag "div" + ( + text "class=\"edge-alt\" style=\"top: " + >|< pp y1 + >|< "px; left: " + >|< pp (min x1 x2) + >|< "px; width: " + >|< abs (x2 - x1 - 16) + >|< "px;\"" + ) + (text " ") + else + tag "div" + ( + text "class=\"edge-ver " + >|< text className + >|< text "\" style=\"top: " + >|< pp (y1 + 35) + >|< "px; left: " + >|< pp x1 + >|< "px; height: " + >|< (y2 - y1 - 60 - 6) + >|< "px;\"" + ) + (text " ") + >|< tag "div" + ( + text "class=\"edge-hor" + >|< text (if x2 > x1 then " edge-hor-left " else if x2 < x1 then " edge-hor-right " else " edge-hor-no-curve ") + >|< text className + >|< text "\" style=\"top: " + >|< pp (y2 - 19) + >|< "px; left: " + >|< pp (if x1 < x2 then x1 else x2 + (if isEnd then 0 else (abs (x2 - x1) + 1) `div` 2)) + >|< "px; width: " + >|< pp (abs (x2 - x1) `div` (if isEnd then 1 else 2)) + >|< "px;\"" + ) + (text " ") + >|< (if isEnd then Emp else tag "div" + ( + text "class=\"edge-end edge-end-" + >|< text (if x2 > x1 then "left " else if x2 < x1 then "right " else "no-curve ") + >|< text className + >|< text "\" style=\"top: " + >|< pp (y2 - 3 + 11) + >|< "px; left: " + >|< pp (if x1 < x2 then (x1 + x2) `div` 2 + 6 else x2) + >|< pp "px; width: " + >|< pp (if x1 == x2 then 0 else ((abs (x2 - x1) + 1) `div` 2) - 6) + >|< "px;\"" + ) + (text " ") + ) + where + (x1, y1) = pos from + (x2, y2) = pos to + className = case kind of + EdgeAlt -> "" + EdgeGuard -> "edge-guard" + EdgeHead -> "edge-head" + EdgeUnify -> "edge-unify" + +-- | Creates a visualization for the given query and solve trace. +-- Output is a PP_Doc containing a HTML file. +chrVisualize :: [C] -> SolveTrace' C (MBP.StoredCHR C G P P) S -> PP_Doc +chrVisualize query trace = tag' "html" $ + tag' "head" ( + tag' "title" (text "CHR visualization") + >|< tag' "style" styles + ) + >|< tag' "body" ( + body + ) + where + graph = createGraph query trace + body = ufold reduce Emp graph >|< hlist (fmap (showEdge posId) $ labEdges graph) + reduce (inn, id, node, out) right = showNode pos (id, node) >|< right + nodeCount = length $ nodes graph + pos :: Node' -> (Int, Int) + pos n = ((nodeColumn n) * 200, (nodeLayer n) * 60) + posId :: Node -> (Int, Int) + posId node = pos (node, fromJust $ lab graph node) + +-- | The stylesheet used in the visualization. +styles :: PP_Doc +styles = + text "body {\n\ + \ font-size: 9pt;\n\ + \ font-family: Arial;\n\ + \}\n\ + \.rule {\n\ + \ position: absolute;\n\ + \ white-space: nowrap;\n\ + \}\n\ + \.rule-text {\n\ + \ border: 1px solid #aaa;\n\ + \ background-color: #fff;\n\ + \ display: inline-block;\n\ + \ padding: 2px;\n\ + \ margin: 3px 1px 0;\n\ + \ min-width: 30px;\n\ + \ text-align: center;\n\ + \}\n\ + \.rule-alt {\n\ + \ display: inline-block;\n\ + \ color: #A89942;\n\ + \ background: #fff;\n\ + \}\n\ + \.rule-additional-alt {\n\ + \ position: absolute;\n\ + \ white-space: nowrap;\n\ + \ margin-top: 24px;\n\ + \}\n\ + \.edge-ver {\n\ + \ position: absolute;\n\ + \ width: 0px;\n\ + \ border-left: 6px solid #578999;\n\ + \ opacity: 0.4;\n\ + \ margin-left: 15px;\n\ + \ margin-top: 9px;\n\ + \ z-index: -1;\n\ + \}\n\ + \.edge-hor {\n\ + \ position: absolute;\n\ + \ height: 27px;\n\ + \ border-bottom: 6px solid #578999;\n\ + \ opacity: 0.4;\n\ + \ margin-left: 15px;\n\ + \ margin-top: 8px;\n\ + \ z-index: -1;\n\ + \}\n\ + \.edge-diag {\n\ + \ transform-origin: 50% 50%;\n\ + \ position: absolute;\n\ + \ height: 6px;\n\ + \}\n\ + \.edge-hor-left {\n\ + \ border-bottom-left-radius: 100% 33px;\n\ + \ border-left: 6px solid #578999;\n\ + \}\n\ + \.edge-hor-right {\n\ + \ border-bottom-right-radius: 100% 33px;\n\ + \ border-right: 6px solid #578999;\n\ + \}\n\ + \.edge-hor-no-curve {\n\ + \ border-right: 6px solid #578999;\n\ + \}\n\ + \.edge-end {\n\ + \ position: absolute;\n\ + \ height: 27px;\n\ + \ width: 16px;\n\ + \ border-top: 6px solid #578999;\n\ + \ opacity: 0.4;\n\ + \ margin-left: 15px;\n\ + \ margin-top: 8px;\n\ + \ z-index: -1;\n\ + \}\n\ + \.edge-end-left {\n\ + \ border-top-right-radius: 100% 33px;\n\ + \ border-right: 6px solid #578999;\n\ + \}\n\ + \.edge-end-no-curve {\n\ + \ border-right: 6px solid #578999;\n\ + \ margin-top: 14px;\n\ + \ height: 21px;\n\ + \}\n\ + \.edge-end-right {\n\ + \ border-top-left-radius: 100% 33px;\n\ + \ border-left: 6px solid #578999;\n\ + \}\n\ + \.edge-guard {\n\ + \ border-color: #69B5A7;\n\ + \}\n\ + \.edge-unify {\n\ + \ border-color: #8CBF7A;\n\ + \}\n\ + \.edge-alt {\n\ + \ height: 1px;\n\ + \ background-color: #aaa;\n\ + \ position: absolute;\n\ + \ margin-top: 19px;\n\ + \ z-index: -1;\n\ + \ padding-right: 22px;\n\ + \}\n\ + \" diff --git a/src/CHR/Language/GTerm.hs b/src/CHR/Language/GTerm.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Language/GTerm.hs @@ -0,0 +1,14 @@ +------------------------------------------------------------------------------------------- +--- 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 new file mode 100644 --- /dev/null +++ b/src/CHR/Language/GTerm/AST.hs @@ -0,0 +1,124 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/src/CHR/Language/GTerm/Parser.hs @@ -0,0 +1,144 @@ +{-# 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 ":" + +