ho-rewriting 0.2 → 0.2.1
raw patch · 5 files changed
+110/−11 lines, 5 filesdep ~base
Dependency ranges changed: base
Files
- README.md +2/−2
- examples/Lib.hs +103/−0
- ho-rewriting.cabal +4/−7
- src/Data/Rewriting/HigherOrder.hs +1/−1
- tests/Capture.hs +0/−1
README.md view
@@ -2,5 +2,5 @@ Some examples are found in the [examples directory](examples). For more information, see "Lightweight Higher-Order Rewriting in Haskell": - * [Paper](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight.pdf)- * [Slides](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_slides.pdf)+ * [Paper](https://emilaxelsson.github.io/documents/axelsson2015lightweight.pdf)+ * [Slides](https://emilaxelsson.github.io/documents/axelsson2015lightweight_slides.pdf)
+ examples/Lib.hs view
@@ -0,0 +1,103 @@+{-# 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+version: 0.2.1 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@@ -10,15 +10,15 @@ more information, see \"Lightweight Higher-Order Rewriting in Haskell\" (presented at TFP 2015): .- * Paper: <http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight.pdf>+ * Paper: <https://emilaxelsson.github.io/documents/axelsson2015lightweight.pdf> .- * Slides: <http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_slides.pdf>+ * Slides: <https://emilaxelsson.github.io/documents/axelsson2015lightweight_slides.pdf> homepage: https://github.com/emilaxelsson/ho-rewriting bug-reports: https://github.com/emilaxelsson/ho-rewriting/issues license: BSD3 license-file: LICENSE author: Emil Axelsson-maintainer: emax@chalmers.se+maintainer: 78emil@gmail.com copyright: Copyright (c) 2015, Emil Axelsson category: Language build-type: Simple@@ -65,9 +65,6 @@ TemplateHaskell TupleSections UndecidableInstances-- default-language:- Haskell2010 test-suite capture type: exitcode-stdio-1.0
src/Data/Rewriting/HigherOrder.hs view
@@ -252,7 +252,7 @@ -- | Lookup a name in an alias environment lookAlias :: Name -> Aliases -> Maybe Name-lookAlias n (mp,_) = Map.lookup n mp+lookAlias n = Map.lookup n . fst -- | Capture-avoiding substitution. Succeeds iff. each meta-variable in 'RHS' -- has a mapping in the substitution.
tests/Capture.hs view
@@ -67,4 +67,3 @@ putStrLn $ "Tests " ++ show [i | (i,False) <- zip [0..] tests] ++ " failed" exitFailure -