intuitionistic

intuitionistic.hs

import Data.Maybe
import System.IO.Unsafe
import Debug.Trace


data P = T | F | Var Char | Or P P | And P P | If P P 
  deriving Eq

instance Show P where
  show T = "T"
  show F = "F"
  show (Var p) = [p]
  show (Or p q) = "("++(show p)++"v"++(show q)++")"
  show (And p q) = "("++(show p)++"&"++(show q)++")"
  show (If p q) = "("++(show p)++"->"++(show q)++")"



step ::  [P] -> P -> [String] -> Maybe [([P], P)]
step gamma prop [] = Nothing
step gamma (And phi psi) ("&I":moreR) = Just [(gamma, phi), (gamma, psi)]
step gamma (If phi psi) ("->I":moreR) = Just [(phi:gamma, psi)]
step gamma (Or phi psi) ("vI":moreR) = if head moreR == "1" then Just [(gamma, phi)] else Just [(gamma, psi)] 
step gamma T ("TI":moreR) = Just []
step gamma prop ("Ax":moreR) = if elem prop gamma then Just [] else Nothing
step _ _ _ = Nothing


getRule = getLine

showGamma [] = ""
showGamma [x] = show x
showGamma (x:xs) = (show x)++", "++(showGamma xs)
printGoal a b = "Current Goal:  "++(showGamma $ fst a)++" |- "++(show$snd a)++"\nOther Goals: "++(show b)


prove :: [([P], P)] -> [([P], P)]
prove [] = []
prove goals = if trace (printGoal currentGoal otherGoals) ((snd currentGoal) `elem` (fst currentGoal)) then prove (tail goals) else prove (result++otherGoals)  
              where currentGoal = head goals
                    otherGoals  = tail goals
                    tactic      = step (fst currentGoal) (snd currentGoal) (words $ unsafePerformIO getRule)
                    result      = if isNothing tactic then [currentGoal] else fromJust tactic

theorem prop = prove [([], prop)]


ejemplo = theorem (If (Var 'p') (If (Var 'q') (And (Var 'p') (Var 'q'))))