-- POC of a Pretty Awful Proof Assistant
-- $Id: papa.hs,v 1.2 2025/01/09 11:33:12 oj14ozun Exp $
-- https://wwwcip.cs.fau.de/~oj14ozun/src+etc/papa.hs

import Data.Char

data Obj = Obj Int | Prod Obj Obj | Coprod Obj Obj | Exp Obj Obj | Term | Init
  deriving (Eq, Show)
type Mor = (Obj, Obj)

papa :: String -> ([Obj], [Mor]) -> ([Obj], [Mor])
papa word (os, ms) | all isDigit word = ((Obj $ read word):os, ms)
papa "id" ((a:os), ms) = (os, (a, a) : ms)
papa "." (os, ((a, b) : (b', c) : ms)) | b == b' = (os, (a, c) : ms)
papa "outl" ((a:b:os), ms) = (os, ((Prod a b), a):ms)
papa "outr" ((a:b:os), ms) = (os, ((Prod a b), b):ms)
papa "<,>" (os, (((a, b)):((a', b')):ms)) | a == a' = (os, (a, (Prod b b')):ms)
papa "*" (a:b:os, ms) = (Prod a b:os, ms)
papa "inl" ((a:b:os), ms) = (os, ((a, (Coprod a b))):ms)
papa "inr" ((a:b:os), ms) = (os, ((b, (Coprod a b))):ms)
papa "[,]" (os, ((a, b):(a', b'):ms)) | b == b' = (os, ((Coprod a a'), b) : ms)
papa "+" (a:b:os, ms) = (Coprod a b:os, ms)
papa "uncurry" (os, (((a, (Exp b c))):ms)) = (os, (((Prod a b), c)) : ms)
papa "curry" (os, ((((Prod a b), c)):ms)) = (os, ((a, (Exp b c))) : ms)
papa "eval" (a:b:os, ms) = (os, ((Prod a (Exp a b)), b):ms)
papa "^" (a:b:os, ms) = ((Exp b a):os, ms)
papa "term" (os, ms) = (Term:os, ms)
papa "bang" (a:os, ms) = (os, ((a, Term)):ms)
papa "init" (os, ms) = (Init:os, ms)
papa "cobang" (a:os, ms) = (os, ((Init, a)):ms)
papa ":" (a:b:os, (a', b'):ms) | a == a' && b == b' = (os, ms)
papa _ st = st

main = interact pa >> putStr "\n"
  where pa = show . foldl (flip papa) ([], []) . words

-- Ex. 1: Proof that ∧ is symmetric,    2 1 * 1 2 * 1 2 outl 1 2 outr <,> :
-- Ex. 2: Proof that A ∧ B → A ∨ B,      1 2 + 1 2 * 1 2 inl 1 2 outl . :
-- Ex. 3: Proof that A → ⊤ ∧ A,         term 1 * 1 1 bang 1 id <,> :