Posted:

**Apr 13, 2012 5:47 pm**VazScep wrote: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.

- Code: Select all
`-- Basic conversions and conversionals`

module Conversions where

import Bootstrap hiding (matchMP)

import Propositional

import Utils

import 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 theorem

convMP :: 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 conditional

antC :: Conv String -> Conv String

antC (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 String

conclC (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 negation

notC :: Conv String -> Conv String

notC (Conv c) = Conv f

where f (Not p) = c p >>= matchMP substNot

f _ = []

-- Attempt the left conversion, and if it fails, attempt the right

orC :: Conv a -> Conv a -> Conv a

orC (Conv c) (Conv c') = Conv f

where f t = c t `mplus` c' t

-- Try all conversions which succeed

tryC :: [Conv a] -> Conv a

tryC = foldr orC failC

-- Apply a conversion based on the term to be converted

ifC :: (Term a -> Bool) -> Conv a -> Conv a

ifC p c = Conv (\t -> if p t then applyC c t else [])

-- Apply one conversion after another

thenC :: Conv String -> Conv String -> Conv String

thenC 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 succeeds

allC :: Conv String

allC = Conv (\t -> return $ instL [t] reflEq)

-- The identity for orConv and zero for thenConv: always fails

failC :: Conv a

failC = Conv (const [])

-- Sequence conversions

everyC :: [Conv String] -> Conv String

everyC = foldl thenC allC

isImp :: Term a -> Bool

isImp (p :=>: q) = True

isImp _ = False

isNeg :: Term a -> Bool

isNeg (Not p) = True

isNeg _ = False

-- Apply a conversion to the first applicable term on a depth first search

depthConv1 :: Conv String -> Conv String

depthConv1 c = tryC [ c

, ifC isNeg (notC c')

, ifC isImp (antC c' `orC` conclC c') ]

where c' = depthConv1 c

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'