packages feed

ho-rewriting 0.2.1 → 0.3

raw patch · 6 files changed

+25/−120 lines, 6 filesdep ~compdata

Dependency ranges changed: compdata

Files

− examples/Lib.hs 
@@ -1,103 +0,0 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE NoMonomorphismRestriction #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE RankNTypes #-}--- {-# LANGUAGE PolyKinds #-}-{-# LANGUAGE PartialTypeSignatures #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE GADTs #-}--- {-# OPTIONS_GHC -fno-warn-missing-methods #-}-module Lib-    ( -    ) where--import Data.Comp-import Data.Comp.Derive-import Data.Comp.Ops-import Data.Comp.Render-import Data.Comp.Matching-import Data.Rewriting.Rules-import Data.Rewriting.HigherOrder-import Data.String(IsString(..))-import Data.Maybe(fromMaybe)-import Data.Function (on)-import Data.Monoid-import Data.Proxy-import qualified Data.Set as Set--import Derive--data STUDENT a = Student a a a a deriving Show---data LIT t (a :: *) = L {unL :: t} deriving Show-data LIT a t where-    L :: a -> LIT a t-unL :: LIT a t -> a-unL (L a) = a-deriving instance Show a => Show (LIT a a)-data MAJOR a = English | Math | Physics deriving (Show,Eq)-$(derive [makeFunctor,makeTraversable,makeFoldable,-          makeEqF,makeShowF,smartConstructors,makeShowConstr] [''STUDENT,''LIT,''MAJOR])-$(derive [smartRep] [''MAJOR])-$(derive [makeEqF,makeShowF,smartConstructors,makeShowConstr] [''WILD])-instance Render STUDENT-instance Show t => Render (LIT t)-instance Render WILD-instance Render MAJOR-instance (MetaRep f ~ MetaId) => Render (META f)-instance (MetaRep f ~ MetaId) => ShowConstr (META f) where-    showConstr (Meta (MVar (MetaId rep))) = show rep-type SIG = MAJOR :+: STUDENT :+: LIT String :+: LIT Int :+: LIT Float :+: ADDONS-type ADDONS = VAR :+: LAM :+: APP -- Not needed as written, but allow higher order rewrite rules.--class Major f where-    english :: f a-    math :: f a-    physics :: f a-class St f where-    rStudent :: f Int -> f String -> f Float -> f (MAJOR a) -> f a-instance (Rep (r f),Functor (PF (r f)),STUDENT :<: PF (r f),f :<: SIG) => St (r f) where-    rStudent a b c d = toRep $ toCxt $ iStudent (prep a) (prep b) (prep c) (prep d)-        where prep = fmap (const ()) . deepInject . fromRep-        -extract def = maybe def unL . proj . (\(Term m) -> m) . fromRep-instance (Rep (r f),LIT a :<: PF (r f),LIT a :<: f,Num a) => Num (r f a) where-    fromInteger = toRep . iL . (id :: a -> a) . fromInteger-    signum (extract (0::a) -> a) = toRep $ iL (signum a)-    abs (extract (0::a) -> a) = toRep $ iL (abs a)-    (extract (0::a) -> a) + (extract (0::a) -> b) = toRep $ iL $ a + b-    (extract (1::a) -> a) * (extract (1::a) -> b) = toRep $ iL $ a * b-    (extract (0::a) -> a) - (extract (0::a) -> b) = toRep $ iL $ a - b-instance (Rep (r f),LIT a :<: PF (r f),LIT a :<: f,Fractional a) => Fractional (r f a) where-    fromRational = toRep . iL . (id :: a -> a) . fromRational-    recip (extract (1::a) -> a) = toRep $ iL $ recip a-   -- -}-instance (Rep (r f),LIT a :<: PF (r f),LIT a :<: f,IsString a) => IsString (r f a) where-    fromString = toRep . iL . (id :: a -> a) . fromString--instance Functor f => Rep (Cxt NoHole f) where-    type PF (Cxt NoHole f) = f-    toRep = toCxt-    fromRep = fmap (const ())-    -e3 :: Term SIG-e3 = rStudent 3 "hi" 2 rEnglish--e4 :: Term SIG-e4 = rStudent 3 "hi" 2.0 (toCxt $ deepInject e3)--student_rule :: MetaId String -> Rule (LHS SIG) (RHS SIG)-student_rule x = rStudent 3 (meta x) __ rEnglish ===> rStudent 4 "matched" 3 rMath-a ==> b = toRep a ===> toRep b-main = do-    drawTerm e3-    drawTerm $ stripAnn $ applyFirst app [quantify (student_rule) ] $ prepare e3-    print "hi"
ho-rewriting.cabal view
@@ -1,5 +1,5 @@ name:                ho-rewriting-version:             0.2.1+version:             0.3 synopsis:            Generic rewrite rules with safe treatment of variables and binders description:         This package gives a generic implementation of higher-order                      rewriting. The main idea is to use techniques from embedded@@ -44,7 +44,7 @@   build-depends:     base >=4.7 && <5,     containers,-    compdata ==0.10.*,+    compdata <=0.14,     mtl,     patch-combinators
src/Data/Rewriting/FirstOrder.hs view
@@ -5,10 +5,13 @@   +import Control.Monad (guard, (<=<)) import Control.Monad.Reader import Control.Monad.Writer+import Data.Bifunctor (second) import Data.Function (on)-import Data.List (groupBy)+import Data.Map (Map)+import qualified Data.Map as Map  import Data.Comp import Data.Comp.Ops@@ -37,10 +40,11 @@ -- | Turn a list of candidate mappings into a substitution. Succeeds iff. all mappings for the same -- variable are equal. solveSubst :: EqF f => [(Name, Term f)] -> Maybe (Subst f)-solveSubst s = sequence [fmap (v,) $ solveTerm ts | g <- gs, let (v:_,ts) = unzip g]-  where-    gs = groupBy ((==) `on` fst) s-      -- TODO Make O(n * log n)+solveSubst s =+  sequence+    [ fmap (v, ) $ solveTerm ts+    | (v, ts) <- Map.toList $ Map.fromListWith (++) $ map (second pure) s+    ]  -- | First-order matching. Succeeds if the pattern matches and all occurrences of a given -- meta-variable are matched against equal terms.
src/Data/Rewriting/HigherOrder.hs view
@@ -7,11 +7,12 @@   +import Control.Monad (guard, liftM2, (<=<)) import Control.Monad.Reader import Control.Monad.Writer import qualified Data.Foldable as Foldable+import Data.Bifunctor (second) import Data.Function (on)-import Data.List (groupBy) import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set)@@ -201,10 +202,11 @@ -- variable are alpha-equivalent. solveSubstAlpha :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) =>     Subst (f :&: a) -> Maybe (Subst (f :&: a))-solveSubstAlpha s = sequence [fmap (v,) $ solveTermAlpha ts | g <- gs, let (v:_,ts) = unzip g]-  where-    gs = groupBy ((==) `on` fst) s-      -- TODO Make O(n * log n)+solveSubstAlpha s =+  sequence+    [ fmap (v, ) $ solveTermAlpha ts+    | (v, ts) <- Map.toList $ Map.fromListWith (++) $ map (second pure) s+    ]  -- | Higher-order matching. Succeeds if the pattern matches and all occurrences of a given -- meta-variable are matched against equal terms.@@ -252,7 +254,7 @@  -- | Lookup a name in an alias environment lookAlias :: Name -> Aliases -> Maybe Name-lookAlias n = Map.lookup n . fst+lookAlias n (mp,_) = Map.lookup n mp  -- | Capture-avoiding substitution. Succeeds iff. each meta-variable in 'RHS' -- has a mapping in the substitution.
src/Data/Rewriting/Rules.hs view
@@ -16,6 +16,7 @@ import Data.Comp import Data.Comp.Ops import Data.Patch+import Data.Kind (Type)   @@ -49,8 +50,8 @@ class MetaVar r   where     -- Representation of meta-variable identifiers-    type MetaRep r :: * -> *-    type MetaArg r :: * -> *+    type MetaRep r :: Type -> Type+    type MetaArg r :: Type -> Type     metaExp :: MetaExp r a -> r a  -- | Construct a meta-variable@@ -136,7 +137,7 @@     __ = LHS $ Term $ Inl WildCard  -- | Representation of object variables-type family Var (r :: * -> *) :: * -> *+type family Var (r :: Type -> Type) :: Type -> Type  instance MetaVar (LHS f)   where@@ -158,7 +159,7 @@  class Rep r   where-    type PF r :: * -> *+    type PF r :: Type -> Type     toRep   :: Term (PF r) -> r a     fromRep :: r a -> Term (PF r)
tests/Capture.hs view
@@ -67,3 +67,4 @@       putStrLn $ "Tests " ++ show [i | (i,False) <- zip [0..] tests] ++ " failed"       exitFailure +