Posted: Apr 13, 2012 5:47 pm
VazScep wrote:
Code: Select all
`-- Basic conversions and conversionalsmodule Conversions whereimport Bootstrap hiding (matchMP)import Propositionalimport Utilsimport Control.Monad.Error-- Conversions wrap functions which take terms and derive equations. Each -- equation has an lhs which is the original term.newtype Conv a = Conv (Term a -> [Theorem a])applyC :: Conv a -> Term a -> [Theorem a]applyC (Conv c) term = c term-- Use a conversion to rewrite a theoremconvMP :: Conv String -> Theorem String -> [Theorem String]convMP c thm = do eq  <- applyC c (theoremTerm thm)                  imp <- matchMP eqMP eq                  mp imp thm-- Apply a conversion to the antecedent of a conditionalantC :: Conv String -> Conv StringantC (Conv c) = Conv f  where f (p :=>: q) = c p >>= matchMP substLeft'          where substLeft' = instM (Var . avoid (vars q)) [("p",q)] substLeft        f _          = []  -- Apply a conversion to the consequent of a conditional        conclC :: Conv String -> Conv StringconclC (Conv c) = Conv f  where f (p :=>: q) = c q >>= matchMP substRight'          where substRight' = instM (Var . avoid (vars p)) [("p",p)] substRight        f _          = []-- Apply a conversion to the body of a negationnotC :: Conv String -> Conv StringnotC (Conv c) = Conv f   where f (Not p) = c p >>= matchMP substNot        f _       = []        -- Attempt the left conversion, and if it fails, attempt the rightorC :: Conv a -> Conv a -> Conv aorC (Conv c) (Conv c') = Conv f  where f t = c t `mplus` c' t        -- Try all conversions which succeedtryC :: [Conv a] -> Conv atryC = foldr orC failC-- Apply a conversion based on the term to be convertedifC :: (Term a -> Bool) -> Conv a -> Conv aifC p c = Conv (\t -> if p t then applyC c t else [])-- Apply one conversion after anotherthenC :: Conv String -> Conv String -> Conv StringthenC c c' = Conv f  where f t = do thm   <- applyC c t                 r     <- rhs (theoremTerm thm)                 thm'  <- applyC c' r                 thm'' <- matchMP trans thm                 matchMP thm'' thm'        rhs (Not ((p :=>: q) :=>: Not (r :=>: s))) | p == s && q == r = return q        rhs _  = []        -- The zero for orConv and identity for thenConv: always succeedsallC :: Conv StringallC = Conv (\t -> return \$ instL [t] reflEq)-- The identity for orConv and zero for thenConv: always failsfailC :: Conv afailC = Conv (const [])-- Sequence conversionseveryC :: [Conv String] -> Conv StringeveryC = foldl thenC allC        isImp :: Term a -> Bool isImp (p :=>: q) = TrueisImp _          = FalseisNeg :: Term a -> BoolisNeg (Not p) = TrueisNeg _       = False-- Apply a conversion to the first applicable term on a depth first searchdepthConv1 :: Conv String -> Conv StringdepthConv1 c = tryC [ c                    , ifC isNeg (notC c')                    , ifC isImp (antC c' `orC` conclC c') ]  where c' = depthConv1 c`
This is a pretty rich combinator language already, with some nice algebraic structure, but the goal here is to be able to write lots of new more sophisticated conversions by composing the primitive conversions. It's kind of overkill for propositional logic, but when you're working in higher-order theories, you want to use this sort of language to build powerful rewrite based automation and domain specific rewriting automation.

Hey, trying to give this one a go, but it fails to compile, several missing symbols:
Code: Select all
`Conversions.hs:20:26: Not in scope: `matchMP'Conversions.hs:20:34: Not in scope: `eqMP'Conversions.hs:26:32: Not in scope: `matchMP'Conversions.hs:27:69: Not in scope: `substLeft'Conversions.hs:33:32: Not in scope: `matchMP'Conversions.hs:34:70: Not in scope: `substRight'Conversions.hs:40:29: Not in scope: `matchMP'Conversions.hs:40:37: Not in scope: `substNot'Conversions.hs:62:27: Not in scope: `matchMP'Conversions.hs:62:35: Not in scope: `trans'Conversions.hs:63:18: Not in scope: `matchMP'Conversions.hs:69:39: Not in scope: `reflEq'`