{-
	Initial code for a 'proof printer': show a Metamath proof in a format
	that resembles a calculational proof.

	TODO:

	 - Print out a ProofTree Expression using the following rules: (1)
	   begin with the top level; (2) indentation = number of items on the
	   stack after this proof step.   Make it look like a calculation.

	 - Fold 1-step subproofs into the calculation.

	 - Choose the 'main' subproof not to be the first subproof (= rule (2),
	   above), but the longest one (or other heuristic?).

	 - Show special inference rules ($a/$p statements), like ax-mp, mtbir,
	   etc. in special ways, so that the calculations become nicer.  Preferably
	   automatically based on the content of the $a/$p statement.
	
-}

module HmmPrinter
	(mmPrintTheoremProof
	)

where

import HmmImpl


mmPrintTheoremProof :: Database -> Label -> String
mmPrintTheoremProof db lab = mmPrintProof proof
	where
		stat = findStatement db lab
		(_, _, Theorem _ _ proof) = stat

mmPrintProof :: Proof -> String
mmPrintProof proof = show tree
	where
		tree = onlyExpressions $ onlyEssential $ fromRight $ mmComputeSubtheorems (fromRight $ mmComputeProofTree proof)

onlyEssential :: ProofTree (Statement, Expression, DVRSet) -> ProofTree (Statement, Expression, DVRSet)
onlyEssential (Apply (stat, expr, dvrSet) subtrees) =
	Apply (stat, expr, dvrSet) $ map onlyEssential $ map fst $ filter isEssential $ zip subtrees (getHypotheses stat)
	where
		isEssential :: (ProofTree (Statement, Expression, DVRSet), Statement) -> Bool
		isEssential (_, st) = isDollarE st

onlyExpressions :: ProofTree (Statement, Expression, DVRSet) -> ProofTree Expression
onlyExpressions (Apply (_, expr, _) subtrees) = Apply expr (map onlyExpressions subtrees)