module Bergamot.Latex exposing (..)

import Bergamot.Syntax as Syntax exposing (..)
import Bergamot.Rules as Rules exposing (..)
import Bergamot.Utils exposing (..)

import Debug

type Void = Void Void

absurd : Void -> a
absurd (Void v) = absurd v

renderTermViaRules : RuleEnv -> Term Void -> Maybe String
renderTermViaRules env t =
    Call "latex" [Syntax.map absurd t, Var (MkMetavariable "s")]
    |> prove
    |> Rules.andThen reifyProofTree
    |> single env
    |> Maybe.andThen (\(MkProofTree node) ->
        case node.conclusion of
            Call "latex" [_, StringLit s] -> Just s
            _ -> Nothing)

renderRuleViaRules : RuleEnv -> Rule -> Maybe String
renderRuleViaRules env r =
    let
        quotedPrems = List.map (Syntax.andThen quoteMetavariable) r.premises
        quotedConc = Syntax.andThen quoteMetavariable r.conclusion
        buildStr conc prems = String.concat
            [ "\\cfrac{"
            ,   String.join "\\quad " prems
            , "}{" 
            ,   conc
            , "}\\ \\texttt{"
            ,   r.name
            , "}"
            ]
    in
        renderTermViaRules env quotedConc
        |> Maybe.andThen (\conc ->
            sequenceMaybes (List.map (renderTermViaRules env) quotedPrems)
            |> Maybe.map (\prems -> buildStr conc prems))

quoteMetavariable : Metavariable -> Term Void
quoteMetavariable v = Call "metavariable" [StringLit <| metavariableToLatex v]

termToLatex : (a -> String) -> Term a -> String
termToLatex f t =
    case t of
        Call "intlit" [t1]   -> termToLatex f t1
        Call "strlit" [t1]   -> termToLatex f t1
        Call "var" [t1]   -> termToLatex f t1
        Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
        Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
        Call "abs" [t1, t2, t3] -> "\\lambda " ++ termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ ".\\ " ++ termToLatex f t3
        Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2
        Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
        Call "type" [t1, t2, t3] -> termToLatex f t1 ++ "\\vdash " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
        Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
        Call "tarr" [t1, t2] -> termToLatex f t1 ++ "\\to" ++ termToLatex f t2
        Call "extend" [t1, t2, t3] -> termToLatex f t1 ++ ",\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
        Call "inenv" [t1, t2, t3] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ " \\in " ++ termToLatex f t3 
        Call "empty" [] -> "\\varnothing"
        Call s [] -> "\\text{" ++ s ++ "}"
        Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
        Var x -> f x
        IntLit i -> String.fromInt i
        StringLit s -> "\\texttt{" ++ "\"" ++ encodeLatex (encodeStr s) ++ "\"" ++ "}"

metavariableToLatex : Metavariable -> String
metavariableToLatex (MkMetavariable s) =
    let
        noQuestion = String.dropLeft 1 s
    in
        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion

ruleToLatex : Rule -> String
ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"

unificationVarToLatex : UnificationVar -> String
unificationVarToLatex (MkUnificationVar s) = s

proofTreeToLatex : ProofTree -> String
proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"