packages feed

rest-rewrite 0.1 → 0.1.1

raw patch · 3 files changed

+122/−6 lines, 3 files

Files

rest-rewrite.cabal view
@@ -1,14 +1,19 @@ name:               rest-rewrite build-type:         Simple-version:            0.1+version:            0.1.1 cabal-version:      1.22 category:           Rewriting maintainer:         Zack Grannan <zgrannan@cs.ubc.ca>+author:             Zack Grannan <zgrannan@cs.ubc.ca> license:            BSD3 description:        Rewriting library with online termination checking. synopsis:           Rewriting library with online termination checking license-file:       LICENSE +source-repository head+  type:     git+  location: https://github.com/zgrannan/rest+ library   default-language:  Haskell2010   exposed-modules:@@ -99,6 +104,7 @@     OpOrdering     QuickCheckTests     RPO+    Set     StrictOC     WQO @@ -124,11 +130,13 @@   other-modules:       Arith       BagExample+      Compiler       DSL       Group       Language.REST.AbstractOC       Language.REST.ConcreteOC       Language.REST.Core+      Language.REST.Dot       Language.REST.EquivalenceClass       Language.REST.ExploredTerms       Language.REST.MetaTerm@@ -143,23 +151,23 @@       Language.REST.OrderingConstraints.Strict       Language.REST.PartialOrder       Language.REST.Path+      Language.REST.ProofGen+      Language.REST.RESTDot       Language.REST.RPO       Language.REST.Rest       Language.REST.Rewrite       Language.REST.RewriteRule       Language.REST.RuntimeTerm+      Language.REST.SMT       Language.REST.Types-      Language.REST.WorkStrategy       Language.REST.WQO-      Language.REST.SMT-      Compiler+      Language.REST.WorkStrategy       Lists       Multiset       MultisetOrdering       Nat       NonTerm+      Set       WQODot-      Language.REST.Dot-      Language.REST.RESTDot    hs-source-dirs: src
+ src/Language/REST/ProofGen.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE OverloadedStrings #-}+module Language.REST.ProofGen where++import qualified Data.HashMap.Strict as M+import qualified Data.List as L+import qualified Data.Text as T+import Text.Printf++import Language.REST.Path+import Language.REST.Rewrite+import Language.REST.RuntimeTerm+import Language.REST.Op++-- Hardcoded+opToLH (Op "union") = "mp"+opToLH (Op "toMS")  = "multiset_of"+opToLH (Op op) = T.unpack op++withParens True t = "(" ++ t ++ ")"+withParens False t = t++toLH :: Bool -> RuntimeTerm -> String+-- Hardcoded rules+toLH parens (App "m" [arg]) = withParens parens $ printf "Multiset [%s]" (toLH False arg)+toLH parens (App "cons" [x, xs]) = withParens parens $ printf "%s:%s" (toLH True x) (toLH True xs)++toLH _ (App op [])   = opToLH op+toLH parens (App op args) =+  withParens parens $ printf "%s %s" (opToLH op) (L.intercalate " " $ map (toLH True) args)++toProof :: Path Rewrite RuntimeTerm a -> String+toProof (steps, PathTerm result _) = "    " ++ (L.intercalate "\n=== " $ proofSteps ++ [toLH False result]) ++ "\n*** QED"+  where+    proofSteps :: [String]+    proofSteps = map proofStep $ zip steps [0..]++    proofStep ((Step (PathTerm t _) _ _ True), _)     = toLH False t+    proofStep ((Step (PathTerm t _) (Rewrite lhs rhs name) _ False), i) = toLH False t ++ " ? " ++ toLemma lemma+      where+        lemma = go (subTerms t)++        lemmaName =+          case name of+            Just n  -> T.pack n+            Nothing -> "lemma"++        toLemma s = toLH False (App (Op lemmaName) (map snd $ L.sort $ M.toList s))++        go []            = undefined+        go ((st, f): _) | Just su <- unify lhs st M.empty+                        , f (subst su rhs) == nextTerm+                        = su+        go (_:xs)       = go xs++        nextTerm = if i < (length steps - 1) then (pathTerm . term) (steps !! (i + 1)) else result
+ src/Set.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE OverloadedStrings #-}++module Set where++import Arith as A+import Data.Text+import DSL+import Language.REST.MetaTerm+import Language.REST.Op++import qualified Data.HashSet as S++emptyset  = RWApp "∅" []++x /\ y = RWApp "intersect" [x, y]+x \/ y  = RWApp "union" [x, y]++s0 = RWApp "s₀" []+s1 = RWApp "s₁" []++isSubset t1 t2 = t1 \/ t2 ~> t2++userRWs = S.union A.evalRWs $ S.fromList $+  [+    distribL (/\) (\/)+  , distribR (/\) (\/)+  , distribL (\/) (/\)+  , distribR (\/) (/\)+  --   assocL (\/)+  -- , assocL (/\)+  , x /\ x        ~> x+  , x \/ x        ~> x+  , x \/ emptyset ~> x+  -- , commutes (\/)+  -- , commutes (/\)++  -- Example 1+  , s1 /\ s0      ~> emptyset++  -- Example 2+  -- , s0 \/ s1      ~> s0+  ]++evalRWs = S.union A.userRWs $ S.fromList --+  [ RWApp "t2" [] ~> emptyset+  , isSubset (RWApp "right1" []) (RWApp "right" [])+  ]++disjointExample  = "union(union(left, right1), union(left,right))"+disjointExample2 = "union(left, union(right1, union(left,right)))"++example1 = "f(intersect(union(s₀,s₁), s₀))"+example2 = "f(union(intersect(s₀,s₁), s₀))"