View file src/slc/pl.hs - Download

module PL where
 
 import Data.List

 data Proof = SMB String
            | VAR 
            | NXV Proof
            | FNC Proof
            | RED Proof
            | RSL Proof
            | RSR Proof
            | APL Proof Proof
            | LTR Proof Proof
            | RTR Proof Proof
            | EQU Proof Proof			
	deriving (Eq)
	
 data Side = LeftSide | RightSide
	deriving (Eq, Show)

 data Context = Function | Argument | Other
	deriving (Eq, Show)


 -- shift u x increases all variables greater than u in x
 shift :: Proof -> Proof -> Proof
 shift _ (SMB s) = SMB s
 shift VAR VAR = NXV VAR
 shift _ VAR = VAR
 shift (NXV u) (NXV x) = NXV (shift u x)
 shift u (NXV x) = NXV (shift u x)
 shift u (FNC x) = FNC (shift (NXV u) x)
 shift u (RED x) = RED (shift u x)
 shift u (RSL x) = RSL (shift u x)
 shift u (RSR x) = RSR (shift u x)
 shift u (APL x y) = APL (shift u x) (shift u y)
 shift u (LTR x y) = LTR (shift u x) (shift u y)
 shift u (RTR x y) = RTR (shift u x) (shift u y)
 shift u (EQU x y) = EQU (shift u x) (shift u y)

 -- subst u a b (approximatively) replaces u in a by b (a little more complex in fact)
 subst :: Proof -> Proof -> Proof -> Proof
 subst1 :: Proof -> Proof -> Proof -> Proof
 subst u a b = if u == a then b else (if NXV u == a then u else subst1 u a b)
 subst1 _ (SMB s) _ = SMB s
 subst1 _ VAR _ = VAR
 subst1 u (NXV x) b = NXV (subst u x b)
 subst1 u (FNC x) b = FNC (subst (NXV u) x (shift VAR b))
 subst1 u (RED x) b = RED (subst u x b)
 subst1 u (RSL x) b = RSL (subst u x b)
 subst1 u (RSR x) b = RSR (subst u x b)
 subst1 u (APL x y) b = APL (subst u x b) (subst u y b)
 subst1 u (LTR x y) b = LTR (subst u x b) (subst u y b)
 subst1 u (RTR x y) b = RTR (subst u x b) (subst u y b) 
 subst1 u (EQU x y) b = EQU (subst u x b) (subst u y b)

 -- cont x y tests if x contains y 
 cont :: Proof -> Proof -> Bool
 cont1 :: Proof -> Proof -> Bool
 cont x y = if x == y then True else cont1 x y
 cont1 (SMB s) _ = False
 cont1 VAR _ = False
 cont1 (NXV x) y = cont x y
 cont1 (FNC x) y = cont x y
 cont1 (RED x) y = cont x y
 cont1 (RSL x) y = cont x y
 cont1 (RSR x) y = cont x y
 cont1 (APL x y) z = (cont x z) || (cont y z)
 cont1 (LTR x y) z = (cont x z) || (cont y z)
 cont1 (RTR x y) z = (cont x z) || (cont y z)
 cont1 (EQU x y) z = (cont x z) || (cont y z)

 -- red1 does one step of reduction
 red1 :: Proof -> Proof
 red1 (SMB s) = SMB s
 red1 VAR = VAR
 red1 (NXV x) = NXV (red1 x)
 red1 (FNC x) = FNC (red1 x)
 red1 (RED x) = RED (red1 x)
 red1 (RSL x) = RSL (red1 x)
 red1 (RSR x) = RSR (red1 x)
 red1 (APL (FNC x) y) = subst VAR x y
 red1 (APL x y) = APL (red1 x) (red1 y)
 red1 (LTR x y) = LTR (red1 x) (red1 y)
 red1 (RTR x y) = RTR (red1 x) (red1 y) 
 red1 (EQU x y) = EQU (red1 x) (red1 y)

 red2 :: [Proof] -> [Proof]
 red2 [] = []
 red2 (x : l) = (red1 x) : (x : l)

 red3 :: [Proof] -> [Proof]
 red3 [] = []
 red3 (x : l) = case find (\y -> cont x y) l of
	Nothing -> red3 (red2 (x : l))
	Just _ -> x : l

 -- red : reduction
 red :: Proof -> Proof
 red x = case red3 (x : []) of
		[] -> x
		y : m -> y

 side :: Side -> Proof -> Proof
 side _ (SMB s) = SMB s
 side _ VAR = VAR
 side s (NXV x) = NXV (side s x)
 side s (FNC x) = FNC (side s x)
 side s (RED x) = side s (red x)
 side LeftSide (RSL x) = red1 (side LeftSide x)
 side RightSide (RSL x) = side RightSide x
 side LeftSide (RSR x) = side LeftSide x
 side RightSide (RSR x) = red1 (side RightSide x)
 side s (APL x y) = APL (side s x) (side s y)
 side s (LTR x y) = if red (side LeftSide x) == red (side LeftSide y) then (side RightSide (if s == LeftSide then x else y)) else LTR x y
 side s (RTR x y) = if red (side RightSide x) == red (side RightSide y) then (side LeftSide (if s == LeftSide then x else y)) else RTR x y
 side LeftSide (EQU x y) = x
 side RightSide (EQU x y) = y

 left = side LeftSide 
 right = side RightSide 


 contSmb :: Proof -> String -> Bool
 contSmb x s = cont x (SMB s)
 
 abstr :: Proof -> String -> Proof -> Proof
 abstr1 :: Proof -> String -> Proof -> Proof
 abstr d v x = if (contSmb x v) then (abstr1 d v x) else x
 abstr1 d v (EQU x y) = EQU (abstr d v x) (abstr d v y)
 abstr1 d v (SMB s) = if v == s then d else (SMB s)
 abstr1 d v VAR = VAR
 abstr1 d v (NXV x) = NXV (abstr d v x)
 abstr1 d v (FNC x) = FNC (abstr (NXV d) v x)
 abstr1 d v (RED x) = RED (abstr d v x)
 abstr1 d v (RSL x) = RSL (abstr d v x)
 abstr1 d v (RSR x) = RSR (abstr d v x)
 abstr1 d v (APL x y) = APL (abstr d v x) (abstr d v y)
 abstr1 d v (LTR x y) = LTR (abstr d v x) (abstr d v y)
 abstr1 d v (RTR x y) = RTR (abstr d v x) (abstr d v y)
 
 lambda :: String -> Proof -> Proof
 lambda v x = FNC (abstr VAR v x)


 proves x = do
  putStr ("\nThe proof\n  " ++ showproof1 Other 2 x ++ " \nproves\n  " ++ showproof1 Other 2 (left x) ++ "\n= " ++ showproof1 Other 2 (right x) ++ "\n")

 reducesTo x = do
  putStr ("\n  " ++ show x ++ "\nreduces to\n  " ++ show (red x) ++ "\n")

 ident = FNC VAR

 -- Multiple application
 apl2 f x y = APL (APL f x) y
 apl3 f x y z = APL (APL (APL f x) y) z
 
 -- Application with reduction
 apr r x = LTR (LTR (APL r x) (red (left (APL r x)))) (red (right (APL r x)))
 apr2 r x y = apr (apr r x) y
 apr3 r x y z = apr (apr (apr r x) y) z 
					   
 column col s = let l = length (lines s) in if l > 1 then length $ last $ lines s else col + length s 
 
 -- showproof1 ctx col x : user readable representation of x in context ctx at column col
 showproof1 :: Context -> Int -> Proof -> String
 showproof1 _ _ (SMB s) = s
 showproof1 _ _ VAR = "*"
 showproof1 _ col (NXV x) = "'" ++ showproof1 Argument (col+1) x
 showproof1 _ col (FNC x) = "[" ++ showproof1 Other (col+1) x ++ "]"
 showproof1 _ col (RED x) = "@" ++ showproof1 Argument (col+1) x
 showproof1 _ col (RSL x) = "$" ++ showproof1 Argument (col+1) x
 showproof1 _ col (RSR x) = "&" ++ showproof1 Argument (col+1) x
 showproof1 Argument col (APL x y) = "(" ++ showproof1 Other (col+1) (APL x y) ++ ")"
 showproof1 _ col (APL x y) = let s = showproof1 Function col x in s ++ " " ++ showproof1 Argument (column col s + 1) y 
 -- showproof1 _ (LTR x y) = "{ " ++ showproof1 Other x ++ " , " ++ showproof1 Other y ++ " }"
 showproof1 _ col (LTR x y) = "{ " ++ showproof1 Other (col+2) x ++ " ,\n" ++ concat (replicate (col+2) " ") ++ showproof1 Other (col+2) y ++ " }"
 showproof1 _ col (RTR x y) = "< " ++ showproof1 Other (col+2) x ++ " |\n" ++ concat (replicate (col+2) " ") ++ showproof1 Other (col+2) y ++ " >"
 -- showproof1 Other col (EQU x y) = let s = showproof1 Other col x in s ++ " = " ++ showproof1 Other (col + (length s) + 3) y 
 -- showproof1 _ col (EQU x y) = "(" ++ showproof1 Other (col+1) (EQU x y) ++ ")"
 showproof1 _ col (EQU x y) = let s = showproof1 Other (col+1) x in "(" ++ s ++ " = " ++ showproof1 Other (column (col+1) s + 3) y ++ ")" 
  
 -- showproof x = user readable representation of proof x
 showproof = showproof1 Other 0
 
 instance Show Proof where
  show x = showproof x
 

 -- Convert string to proof
 
 pl1 (' ' : s) = pl1 s
 pl1 ('\t' : s) = pl1 s
 pl1 ('\n' : s) = pl1 s
 pl1 ('\r' : s) = pl1 s
 pl1 ('#' : s) = pl1 $ concat $ map (\l -> l ++ "\n") $ tail $ lines s
 pl1 ('(' : s) = pl3 ')' Nothing Nothing s
 pl1 ('*' : s) = (VAR, s)
 pl1 ('\'' : s) = let (x, t) = pl1 s in (NXV x, t)
 pl1 ('[' : s) = let (x, t) = pl3 ']' Nothing Nothing s in (FNC x, t)
 pl1 ('@' : s) = let (x, t) = pl1 s in (RED x, t)
 pl1 ('$' : s) = let (x, t) = pl1 s in (RSL x, t)
 pl1 ('&' : s) = let (x, t) = pl1 s in (RSR x, t)
 pl1 ('-' : s) = let (x, t) = pl1 s in let (y, u) = pl1 t in (apr x y, u)
 pl1 ('{' : s) = let (x, t) = pl3 ',' Nothing Nothing s in let (y, u) = pl3 '}' Nothing Nothing t in (LTR x y, u)
 pl1 ('<' : s) = let (x, t) = pl3 '|' Nothing Nothing s in let (y, u) = pl3 '>' Nothing Nothing t in (RTR x y, u)
 pl1 ('^' : s) = let (x, t) = pl1 s in case x of SMB v -> let (y, u) = pl1 t in (lambda v y, u)
 pl1 ('!' : s) = let (x, t) = pl1 s in case x of SMB x1 -> let (y, u) = pl1 t in let (z, v) = pl1 u in (RED (APL (lambda x1 z) y), v)
 pl1 (c : s) = pl4 [c] s
 
 pl4 s "" = (SMB s, "")
 pl4 s (' ' : t) = (SMB s, t)
 pl4 s ('\t' : t) = (SMB s, t)
 pl4 s ('\n' : t) = (SMB s, t)
 pl4 s ('\r' : t) = (SMB s, t)
 pl4 s (c : t) = if (any.(==)) c " \t\n()*'\\[]-%{,}<|>#=" then (SMB s, (c : t)) else pl4 (s ++ [c]) t
 
 pl2 e (' ' : s) = pl2 e s
 pl2 e ('\t' : s) = pl2 e s
 pl2 e ('\n' : s) = pl2 e s
 pl2 e ('\r' : s) = pl2 e s
 pl2 e "" = (False, Nothing, "")
 pl2 e (c : s) = if c == e then (False, Nothing, s) else if c == '=' then (True, Nothing, s) else let (x, t) = pl1 (c : s) in (False, Just x, t)
 
 pl3 e l Nothing (':' : s) = let (y, t) = pl3 e l Nothing s in (y, t)
 pl3 e l (Just x) (':' : s) = let (y, t) = pl3 e l Nothing s in (APL x y, t)
 pl3 e l x1 s = let x = case x1 of { Nothing -> FNC VAR; Just x2 -> x2 } in case pl2 e s of
	(False, Nothing, t) -> case l of 
	                           Nothing -> (x, t)
	                           Just l -> (EQU l x, t)
	(True, Nothing, t) -> case l of 
	                          Nothing -> pl3 e (Just x) Nothing t
	                          Just l -> pl3 e (Just (EQU l x)) Nothing t		
	(False, Just y, t) -> case x1 of 
	                          Nothing -> pl3 e l (Just y) t
	                          _ -> pl3 e l (Just (APL x y)) t	
							  
 pl s = let (x, t) = pl3 '.' Nothing Nothing s in x
 
 run filename = do
  readFile filename >>= \s -> proves $ pl s


 -- Example of theory
 
 parent = apl2 (SMB "parent")
 grandparent = apl2 (SMB "grandparent")
 allan = SMB "allan"
 brenda = SMB "brenda"
 charles = SMB "charles"

 gpRule1 = lambda "x" $ lambda "y" $ lambda "z" $ 
  EQU (APL (parent (SMB "x") (SMB "y")) $
       APL (parent (SMB "y") (SMB "z")) $
       grandparent (SMB "x") (SMB "z"))
      ident
 gpAxiom1 = EQU (parent allan brenda) ident
 gpAxiom2 = EQU (parent brenda charles) ident
 
 gpTheorem1 = LTR (apr gpAxiom2 (grandparent allan charles))
                  (LTR (apr gpAxiom1 (APL (parent brenda charles) (grandparent allan charles)))
                       (apr3 gpRule1 allan brenda charles))

				
 gpRule1b = pl "^x ^y ^z ( (parent x y : parent y z : grandparent x z) = [*] )"
 gpAxiom1b = pl "parent allan brenda = [*]"
 gpAxiom2b = pl "parent brenda charles = [*]"
 
 gpTheorem1b = LTR (apr gpAxiom2b (grandparent allan charles))
                   (LTR (apr gpAxiom1b (APL (parent brenda charles) (grandparent allan charles)))
                        (apr3 gpRule1b allan brenda charles))
								  
 gpTheorem1c = pl "\
  \ ! gpRule1  ^x ^y ^z ( (parent x y : parent y z : grandparent x z) = [*] ) \
  \ ! gpAxiom1 (parent allan brenda = [*]) \
  \ ! gpAxiom2 (parent brenda charles = [*]) \
  \ ! gpLemma1c (gpRule1 allan brenda charles) \
  \ ! gpLemma2c (gpAxiom1 (parent brenda charles (grandparent allan charles))) \
  \ ! gpLemma3c1 { gpLemma2c , gpLemma1c } \
  \ ! gpLemma3c { { gpLemma3c1 , (parent brenda charles (grandparent allan charles)) } , [*] } \
  \ ! gpLemma4c (gpAxiom2 (grandparent allan charles)) \
  \ ! gpLemma5c { gpLemma4c , gpLemma3c } \
  \ ! gpTheorem1c { grandparent allan charles , gpLemma5c } \
  \ gpTheorem1c "
		
 test = do
  proves gpTheorem1
  proves gpTheorem1b
  proves gpTheorem1c