| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 7 | paulosilva | |
| 2 | {-# LANGUAGE TypeSynonymInstances, FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Galculator.Proof | ||
| 9 | Description : | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | -} | ||
| 18 | |||
| 19 | ------------------------------------------------------------------------------- | ||
| 20 | |||
| 21 | module Galculator.Proof ( | ||
| 22 | Proof, | ||
| 23 | ProofSt(..), | ||
| 24 | ProofStep(..), | ||
| 25 | addStep, | ||
| 26 | getOrd | ||
| 27 | ) where | ||
| 28 | |||
| 29 | import Control.GalcError | ||
| 30 | import Control.Monad.Error | ||
| 31 | import Galculator.Rule | ||
| 32 | import Language.Law.Syntax | ||
| 33 | import Language.R.Syntax | ||
| 34 | |||
| 35 | ------------------------------------------------------------------------------- | ||
| 36 | |||
| 37 | data ProofSt = ProofSt { | ||
| 38 | name :: String, | ||
| 39 | expression :: Law, | ||
| 40 | curExpr :: Either RType RType, | ||
| 41 | curProof :: Proof | ||
| 42 | } | ||
| 43 | |||
| 44 | type Proof = [ProofStep] | ||
| 45 | |||
| 46 | instance Show Proof where | ||
| 47 | show = pretty | ||
| 48 | |||
| 49 | ------------------------------------------------------------------------------- | ||
| 50 | |||
| 51 | data ProofStep = | ||
| 52 | RewriteStep RType [RewriteStep] | ||
| 53 | | IndirectProof RType (Either RType RType) [ProofStep] | ||
| 54 | | QED | ||
| 55 | |||
| 56 | ------------------------------------------------------------------------------- | ||
| 57 | |||
| 58 | getOrd :: MonadError GalcError m => Proof -> m (Either RType RType) | ||
| 59 | getOrd [] = throwError NoOrderSetError | ||
| 60 | getOrd (x:_) = case x of | ||
| 61 | IndirectProof _ o _ -> return o | ||
| 62 | _ -> throwError NoOrderSetError | ||
| 63 | |||
| 64 | |||
| 65 | addStep :: ProofStep -> Proof -> Proof | ||
| 66 | addStep stp [] = [stp] | ||
| 67 | addStep stp (x:xs) = | ||
| 68 | case x of | ||
| 69 | IndirectProof e o lst -> | ||
| 70 | if null lst | ||
| 71 | then IndirectProof e o [stp] : xs | ||
| 72 | else case head lst of | ||
| 73 | QED -> stp : x : xs | ||
| 74 | _ -> IndirectProof e o (stp:lst) : xs | ||
| 75 | _ -> stp : x : xs | ||
| 76 | |||
| 77 | ------------------------------------------------------------------------------- | ||
| 78 | |||
| 79 | pretty :: Proof -> String | ||
| 80 | pretty = | ||
| 81 | concatMap sp . reverse | ||
| 82 | where | ||
| 83 | sp :: ProofStep -> String | ||
| 84 | sp (RewriteStep r lrs) = show r ++ "\n\t{ " ++ concatMap slrs lrs ++ " }\n" | ||
| 85 | sp (IndirectProof r (Left o) lps) = "indirect low:\n<" ++ concatMap sip (reverse lps) ++ ">\n" | ||
| 86 | sp (IndirectProof r (Right o) lps) = "indirect up:\n<" ++ concatMap sip (reverse lps) ++ ">\n" | ||
| 87 | sp QED = "Qed" | ||
| 88 | |||
| 89 | slrs (l, _) = "\t " ++ show l ++ "\n" | ||
| 90 | sip (RewriteStep l lrs) = show l ++ "\n\t{ " ++ concatMap slrs lrs ++ " }\n" | ||
| 91 | sip QED = "indirect end\n" | ||
| 92 | sip _ = "" | ||
| 93 | |||
| 94 | ------------------------------------------------------------------------------- |