chr-lang (empty) → 0.1.0.0
raw patch · 11 files changed
+1586/−0 lines, 11 filesdep +basedep +chr-coredep +chr-datasetup-changed
Dependencies added: base, chr-core, chr-data, chr-lang, chr-parse, chr-pretty, containers, fgl, hashable, mtl, time, unordered-containers
Files
- ChangeLog.md +5/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- chr-lang.cabal +65/−0
- src-main/Main.hs +87/−0
- src/CHR/Language/Examples/Term/AST.hs +415/−0
- src/CHR/Language/Examples/Term/Run.hs +131/−0
- src/CHR/Language/Examples/Term/Visualizer.hs +569/−0
- src/CHR/Language/GTerm.hs +14/−0
- src/CHR/Language/GTerm/AST.hs +124/−0
- src/CHR/Language/GTerm/Parser.hs +144/−0
+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for chr-lang++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ chr-lang.cabal view
@@ -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
+ src-main/Main.hs view
@@ -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:"+
+ src/CHR/Language/Examples/Term/AST.hs view
@@ -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+
+ src/CHR/Language/Examples/Term/Run.hs view
@@ -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'+ ++{-+-}
+ src/CHR/Language/Examples/Term/Visualizer.hs view
@@ -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 ("</" ++ name ++ ">")++-- | 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\+ \"
+ src/CHR/Language/GTerm.hs view
@@ -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++
+ src/CHR/Language/GTerm/AST.hs view
@@ -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)
+ src/CHR/Language/GTerm/Parser.hs view
@@ -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 ":"++