module Natural where

import PrelSequent
import Sequent
import PrSequent

type Hypotheses = [(Int,Formula)]

data NatProof =
   Hypo    Int Formula
 | Unknown Ident Formula
 | ConjI  Formula Formula NatProof NatProof
 | ConjE  Formula Formula Formula NatProof Int Int NatProof
 | DisjIl Formula Formula NatProof 
 | DisjIr Formula Formula NatProof
 | DisjE  Formula Formula Formula NatProof Int NatProof Int NatProof
 | ImplI  Formula Formula Int NatProof
 | ImplE  Formula Formula Formula NatProof NatProof Int NatProof
 | UnivI  Formula Ident NatProof
 | UnivE  Formula Formula Formula NatProof Int Int NatProof
 | ExistI Formula Formula Ident NatProof
 | ExistE Formula Formula NatProof Int NatProof
 | FalsE  Formula NatProof

 | MP     Formula Formula NatProof NatProof -- added 7/11/2000

proof2nat = proof2natproof []

proof2natproof :: Hypotheses -> Proof -> NatProof
proof2natproof hypo proof =
 case proof of
   Proof rule sequent proofs ->
     case (rule,sequent,proofs) of
       ("ax",  (_,         [a]),         []) ->
           findHypo hypo a
       ("R&",  (_,         [Conj a b]),  [prem1,prem2]) -> 
           ConjI a b (pn prem1) (pn prem2)
       ("L&",  (Conj a b:_,[c]),         [prem1]) -> 
           ConjE a b c mainprem h1 (h1 + 1) (pn' [a,b] prem1)
             where
               mainprem = findHypo hypo (Conj a b)
               h1       = maximum' (map fst hypo) + 1
       ("Rv1", (_,         [Disj a b]),  [prem1]) -> 
           DisjIl a b (pn prem1)
       ("Rv2", (_,         [Disj a b]),  [prem1]) -> 
           DisjIr a b (pn prem1)
       ("Lv",  (Disj a b:_,[c]),         [prem1,prem2]) -> 
           DisjE a b c mainprem h1 (pn' [a] prem1) h2 (pn' [b] prem2)
             where
               mainprem = findHypo hypo (Disj a b)
               h1       = maximum' (map fst hypo) + 1
               h2       = h1 --- + 1
       ("R->", (_,         [Impl a b]), [prem1]) ->
           ImplI a b h1 (pn' [a] prem1)
             where
               h1       = maximum' (map fst hypo) + 1
       ("R->", (_,         [Neg a]), [prem1]) ->
           ImplI a Falsum h1 (pn' [a] prem1)
             where
               h1       = maximum' (map fst hypo) + 1
       ("R/A", (_,         [Univ x a]),  [prem1]) ->
           UnivI a x (pn prem1)
       ("R/E", (_,         [Exist x a]), [prem1]) ->
           ExistI a a' x (pn prem1)
             where
               a'       = leftFormOf prem1

       ("L->", (Impl a b:_,[c]),         [prem1,prem2]) -> 
           ImplE a b c mainprem (pn prem1) h1 (pn' [b] prem2)
             where
               mainprem = findHypo hypo (Impl a b)
               h1       = maximum' (map fst hypo) + 1


       ("L->", (Neg a:_,[c]),         [prem1,prem2]) -> 
           ImplE a Falsum c mainprem (pn prem1) h1 (pn' [Falsum] prem2)
             where
               mainprem = findHypo hypo (Impl a Falsum)
               h1       = maximum' (map fst hypo) + 1
       ("L_|_", (Falsum:_, [c]),[]) -> 
           FalsE c mainprem
             where
               mainprem = findHypo hypo Falsum
       ("L/A", (Univ x a:_,[c]),         [prem1]) -> 
           UnivE a a' c mainprem h1 (h1 + 1) (pn' [a', Univ x a] prem1)
             where
               a'       = leftFormOf prem1
               mainprem = findHypo hypo (Univ x a)
               h1       = maximum' (map fst hypo) + 1
       ("L/E", (Exist x a:_,[c]),         [prem1]) -> 
           ExistE a c mainprem h1 (pn' [a] prem1)
             where
               mainprem = findHypo hypo (Exist x a)
               h1       = maximum' (map fst hypo) + 1
       _ -> Unknown "undef" (Scheme "?" [])


   _ -> Unknown "undef" (Scheme "?" [])
  where 
     pn           = proof2natproof hypo
     pn' formulae = proof2natproof (freshHypos formulae hypo)
     leftFormOf p = case p of
                      Goal    (a:_,_)   -> a
                      Proof _ (a:_,_) _ -> a
                      _                 -> Scheme "\\mbox{ass.}" []

maximum' []  = 0
maximum' l   = maximum l 

freshHypos :: [Formula] -> Hypotheses -> Hypotheses
freshHypos formulae hypo = zip [nxt ..] formulae ++ hypo where
 nxt = maximum' (map fst hypo) + 1

findHypo :: Hypotheses -> Formula -> NatProof
findHypo hypo formula =
 case lookup formula [(f,n) | (n,f) <- hypo] of
   Just n -> Hypo n formula
   _      -> case formula of
               Neg a         -> findHypo hypo (Impl a Falsum)
               Impl a Falsum -> findHypo hypo (Neg a) 
               _             -> Unknown "\\mbox{ass.}" formula

prNatProof proof =
 case proof of
   Hypo int formula -> 
     "\\discharge{" ++ show int ++ "}{" ++ prLatexFormula 1 formula ++ "}"
   Unknown ident formula ->
     "\\discharge{" ++ ident ++ "}{" ++ prLatexFormula 1 formula ++ "}"
   ConjI   f1 f2 p1 p2 ->
     "\\infer[{\\scriptstyle \\&I}]{" ++++
     prLatexFormula 1 (Conj f1 f2) +++ "}{" ++++
     prNatProof p1 ++++ "&" ++++ prNatProof p2 ++++ "}"
   ConjE   f1 f2 f3 p1 x y p2 ->
     "\\infer[{\\scriptstyle \\&E," +++ show x +++ show y +++ "}]{" ++++
     prLatexFormula 1 f3 +++ "}{" ++++
     prNatProof p1 ++++ "&" ++++ prNatProof p2 ++++ "}"
   DisjIl   f1 f2 p1 ->
     "\\infer[{\\scriptstyle \\vee I1}]{" ++++
     prLatexFormula 1 (Disj f1 f2) +++ "}{" ++++
     prNatProof p1 ++++ "}"
   DisjIr   f1 f2 p1 ->
     "\\infer[{\\scriptstyle \\vee I2}]{" ++++
     prLatexFormula 1 f1 +++ "\\vee" +++ prLatexFormula 1 f2 +++ "}{" ++++
     prNatProof p1 ++++ "}"
   DisjE   f1 f2 f3 p1 x p2 y p3 ->
     "\\infer[{\\scriptstyle \\vee E," +++ show x ++"," +++ show y +++ "}]{" ++++
     prLatexFormula 1 f3 +++ "}{" ++++
     prNatProof p1 ++++ "&" ++++ prNatProof p2 ++++ "&" ++++ prNatProof p3 ++++ "}"
   ImplI   f1 f2 x p1 ->
     "\\infer[{\\scriptstyle \\supset I," +++ show x +++ "}]{" ++++
     prLatexFormula 1 (Impl f1 f2) +++ "}{" ++++
     prNatProof p1 ++++ "}"
   ImplE   f1 f2 f3 p1 p2 y p3 ->
     "\\infer[{\\scriptstyle \\supset E," +++ show y +++ "}]{" ++++
     prLatexFormula 1 f3 +++ "}{" ++++
     prNatProof p1 ++++ "&" ++++ prNatProof p2 ++++ "&" ++++ prNatProof p3 ++++ "}"
   MP   f1 f2 p1 p2 ->
     "\\infer[{\\scriptstyle MP}]{" ++++
     prLatexFormula 1 f2 +++ "}{" ++++
     prNatProof p1 ++++ "&" ++++ prNatProof p2 ++++ "}"
   FalsE   f1 p1 ->
     "\\infer[{\\scriptstyle \\bot E}]{" ++++
     prLatexFormula 1 f1 +++ "}{" ++++
     prNatProof p1 ++++ "}"
   UnivI   f1 x p1 ->
     "\\infer[{\\scriptstyle \\forall I}]{" ++++
     prLatexFormula 1 (Univ x f1) +++ "}{" ++++
     prNatProof p1 ++++ "}"
   UnivE   f1 f2 f3 p1 x y p2 ->
     "\\infer[{\\scriptstyle \\forall E," +++ show x +++ show y +++ "}]{" ++++
     prLatexFormula 1 f3 +++ "}{" ++++
     prNatProof p1 ++++ "&" ++++ prNatProof p2 ++++ "}"
   ExistI  f1 f2 x p1 ->
     "\\infer[{\\scriptstyle \\exists I}]{" ++++
     prLatexFormula 1 (Exist x f1) +++ "}{" ++++
     prNatProof p1 ++++ "}"
   ExistE  f1 f2 p1 x p2 ->
     "\\infer[{\\scriptstyle \\exists E," +++ show x +++ "}]{" ++++
     prLatexFormula 1 f2 +++ "}{" ++++
     prNatProof p1 ++++ "&" ++++ prNatProof p2 ++++ "}"