{-# LANGUAGE UnicodeSyntax #-}
module Main where

import Prelude.Unicode
import Parser
import Lambda (Params (..), LetPrefixLengths (..), showNameless, showTRNameless,
	synthesise, scoped_Syn_R, dfa_Syn_R, readback_Syn_R, proof_Syn_R, unscoped_Syn_R)
import System.Environment
import Language.HaLex.Minimize
import System.Cmd
import Language.HaLex.FaAsDiGraph (tographviz)
import Language.HaLex.Dfa (Dfa, beautifyDfa)
import Language.HaLex.FaOperations (dfa2ndfa)
import Language.HaLex.Equivalence (equivDfa)
import Spanning
import Text.PrettyPrint.Boxes (render)
import System.Console.GetOpt
import Control.Monad (when)


data Opt
	= Help
	| OptNoVarBacklinks
	| OptNoSBacklinks
	| OptSharedVars
	| OptMaxPrefix
	| OptMinPrefix
	deriving Eq

options = let option s o d = Option [] [s] (NoArg o) d in
	[Option ['h'] ["help"]     (NoArg Help)      "show this usage information",
	 option "no-var-backlinks" OptNoVarBacklinks "no backlinks for variable occurrences",
	 option "no-s-backlinks"   OptNoSBacklinks   "no backlinks for delimiter vertices",
	 option "shared-variables" OptSharedVars     "implicit sharing of variable occurrences",
	 option "max-prefix"       OptMaxPrefix      "maximal (same) prefix lengths for let-bindings",
	 option "min-prefix"       OptMinPrefix      "minimal prefix lengths for let-bindings"]

usage = "maxsharing [options] file1 ..." 

main ∷ IO ()
main = do
	args ← getArgs

	case getOpt Permute options args of
		(opts, files, []) → do
			let params = processOptions opts
			if Help ∈ opts
				then putStr $ usageInfo usage options
				else mapM_ (processFile params) files
		(_,_,errs) → error (concat errs ++ usageInfo usage options)


processOptions options = let has opt = opt ∈ options in Params
	{letPrefixLengths   = if has OptMaxPrefix then MaxPrefix else if has OptMinPrefix then MinPrefix else MaxEagPre,
 	 withVarBacklinks   = not $ has OptNoVarBacklinks,
 	 withSBacklinks     = not $ has OptNoSBacklinks,
 	 withSharedVars     = has OptSharedVars}

processFile ∷ Params → FilePath → IO ()
processFile params f = let syn = synthesise params in do
	λTerm ← parseFile f
	putStrLn "λ-letrec-term:" >> print λTerm
	let λTermSyn = syn λTerm
	putStrLn $ "translation used: " ⧺ show (letPrefixLengths params) ⧺ "\n"
	let scoped = scoped_Syn_R λTermSyn
	putStrLn ("scoped (with adbmals):") >> print scoped
	putStrLn ("scoped (with scope delimiters and nameless abstractions):") >> putStrLn (showNameless scoped)
	putStrLn "derivation:" >> putStrLn (render $ proof_Syn_R λTermSyn)
	let dfa = dfa_Syn_R $ syn scoped
	putStr "DFA: " >> dot (f ⧺ ".dfa") dfa >> putStrLn ""
	let tree = spanning params dfa
	putStrLn "spanning tree:" >> putStrLn (showTRNameless tree)
	putStrLn "readback:" >> print (readback_Syn_R $ syn tree)

	let minDfa = stdMinimizeDfa dfa
	putStr "minimised DFA: " >> dot (f ⧺ ".dfa.min") minDfa >> putStrLn ""
	let minTree = spanning params minDfa
	putStrLn "spanning tree:" >> putStrLn (showTRNameless minTree)
	let minλTerm = readback_Syn_R $ syn minTree
	putStrLn "readback:" >> putStr (show $ unscoped_Syn_R $ syn minλTerm)

	let readbackDfa = dfa_Syn_R $ syn minλTerm
	let (beautifulMinDfa, beautifulReadbackDfa) = (beautifyDfa minDfa, beautifyDfa readbackDfa)
	when (not $ beautifulMinDfa `equivDfa` beautifulReadbackDfa) $ do
		putStrLn "Sanity check failed! Minimised DFA and readback DFA are not equivalent."
		putStrLn $ "(see files with .dfa.min.bf. and .dfa.rb. in their names)" 
		dot (f ⧺ "dfa.min.bf") beautifulMinDfa >> dot (f ⧺ ".dfa.rb") beautifulReadbackDfa

dot ∷ (Show st, Show sy, Ord st, Ord sy) ⇒ String → Dfa st sy → IO ()
dot name dfa = do
	let dotfile = name ⧺ ".dot"
	let pdffile = name ⧺ ".pdf"
	putStrLn $ "writing to files " ⧺ dotfile ⧺ " and " ⧺ pdffile
	writeFile dotfile (tographviz (dfa2ndfa dfa) "g" "circle" "TB" (show . show))
	_ ← system $ "dot -Tpdf -o" ⧺ pdffile ⧺ " " ⧺ dotfile
	return ()