{- |
Module      :  $Header$
Description :  Sentence for HolLight logic
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  portable

Definition of sentences for HolLight logic

  Ref.

  <http://www.cl.cam.ac.uk/~jrh13/hol-light/>

-}
module HolLight.Sentence where

import Common.DocUtils
import Common.Doc
import HolLight.Helper
import HolLight.Term
import Data.Maybe (fromJust, catMaybes, isNothing)
import qualified Data.Char as Char

data Sentence = Sentence {
  term :: Term,
  proof :: Maybe HolProof
  } deriving (Eq, Ord, Show)

instance Pretty Sentence where
  pretty = ppPrintTerm . term

ppPrintTerm :: Term -> Doc
ppPrintTerm = printTerm 0

precParens :: Int -> Doc -> Doc
precParens prec = if prec /= 0 then parens else id

replacePt :: Term -> HolParseType -> Term
replacePt tm pt = case tm of
  Var s t _ -> Var s t (HolTermInfo (pt, Nothing))
  Const s t _ -> Const s t (HolTermInfo (pt, Nothing))
  _ -> tm

printTerm :: Int -> Term -> Doc
printTerm prec tm =
 let _1 = case destNumeral tm of
         Just i -> Just (text (show i))
         _ -> Nothing in
  let _2 = case destList tm of
         Just tms -> case typeOf tm of
           Just t -> case destType t of
             Just (_, x : _) -> case destType x of
               Just ("char", _) -> let cs = map codeOfTerm tms
                 in if any isNothing cs then Nothing
                    else Just (quotes (text (foldr ((:) . Char.chr) []
                                              (catMaybes cs))))
               _ -> Nothing
             _ -> Nothing
           _ -> Nothing
         _ -> Nothing in
 let _3 = if isNothing _2 then case destList tm of
            Just tms -> Just (brackets (printTermSequence "; " 0 tms))
            _ -> Nothing
       else Nothing in
 let _4 = if isGabs tm then Just (printBinder prec tm)
       else Nothing in
 let (s, _, args, hop) = case stripComb tm of
               (hop', args') -> case fromJust (typeOf hop') of
               {- not really sure in which cases (typeOf hop) == Nothing,
               but shouldn't happen if i understand the original
               ocaml code correctly -}
                  ty0' ->
                    let s0 = nameOf hop' in
                    case reverseInterface (s0, hop') of
                      (s', Just pt) -> (s', ty0', args', replacePt hop' pt)
                      _ -> (s0, ty0', args', hop') in
 let _5 = case (s, isConst tm, args == []) of
         ("EMPTY", True, True) -> Just (braces empty)
         ("UNIV", True, True) -> case typeOf tm of
            Just t -> case destFunTy t of
              Just (ty, _) -> Just (parens (hcat [text ":", ppPrintType ty]))
              _ -> Nothing
            _ -> Nothing
         ("INSERT", _, _) ->
            let (mems, oth) = splitlist (destBinary' "INSERT") tm
            in case (isConst oth, destConst oth) of
                 (True, Just ("EMPTY", _)) -> Just (braces (printTermSequence
                                                     ", " 14 mems))
                 _ -> Nothing
         ("GSPEC", _, _) -> case rand tm of
            Just rtm -> case body rtm of
              Just b -> let (evs, bod) = stripExists b
                        in case destComb bod of
                             Nothing -> Nothing
                             Just (bod1, fabs) ->
                               case destComb bod1 of
                                 Nothing -> Nothing
                                 Just (bod2, babs) ->
                                   case rator bod2 of
                                     Nothing -> Nothing
                                     Just c ->
                                       case destConst c of
                                         Just ("SETSPEC", _) ->
                                          Just (braces (hcat [
                                           printTerm 0 fabs,
                                           text " | ",
                                           printTermSequence "," 14 evs,
                                           text " | ",
                                           printTerm 0 babs
                                          ]))
                                         _ -> Nothing
              _ -> Nothing
            _ -> Nothing
         _ -> Nothing in
 let _6 = case destLet tm of
         Just (e : eqs, _) -> case mkEq e of
           Just e' -> let eqs' = map (\ (v, t) -> mkEq (v, t)) eqs
             in if any (Nothing ==) eqs' then Nothing else
                Just (precParens prec
                        (hcat [
                          text "let ",
                          printTerm 0 e',
                          vcat (map (\ eq -> hcat [
                               text "and ",
                               printTerm 0 eq]) (catMaybes eqs')
                                ++ [text " in", text ""])
                        ]))
           _ -> Nothing
         _ -> Nothing in
 let _7 = if s == "DECIMAL" && length args > 2 then
         case (destNumeral (head args), destNumeral (args !! 1)) of
           (Just n_num, Just n_den) -> if not (powerof10 n_den) then Nothing
             else let s_num = text (show (n_num `quot` n_den)) in
                  let s_den = text (concat (tail (map (: [])
                                    (show (n_den + (n_num `mod` n_den)))
                                   )))
                   in Just (hcat [text "#", s_num, if n_den == 1 then empty
                                            else text ".",
                            s_den])
           _ -> Nothing
       else Nothing in
 let _8 = if s == "_MATCH" && length args == 2 then
         case destClauses (args !! 1) of
           Just cls -> Just (precParens prec (vcat [
             hcat [text "match ",
              printTerm 0 (head args),
              text " with"],
             printClauses cls]))
           _ -> Nothing
       else Nothing in
 let _9 = if s == "_FUNCTION" && length args == 1 then
            case destClauses (head args) of
              Just cls -> Just (precParens prec (vcat [
                  text "function",
                  printClauses cls
                ]))
              _ -> Nothing
          else Nothing in
 let _10 = if s == "COND" && length args == 3 then
         Just (precParens prec (vcat [
          hcat [text "if ", printTerm 0 (head args)],
          hcat [text " then ", printTerm 0 (args !! 1)],
          hcat [text " else ", printTerm 0 (args !! 2)]
         ]))
       else Nothing in
 let _11 = if isPrefix hop && length args == 1 then
          Just ((if prec == 1000 then parens else id)
                (if all Char.isAlphaNum s || s == "--"
                    || (
                        case destComb (head args) of
                          Just (l, _) -> let (s0, _) = (nameOf l, typeOf l)
                            in fst (reverseInterface (s0, hop)) == "--"
                               || (case destConst l of
                                    Just (f, _) -> f `elem` ["real_of_num",
                                                          "int_of_num"]
                                    _ -> False)
                          _ -> False)
                    || s == "~" then hcat
                        [text s, printTerm 999 (head args), text " "]
                 else hcat [text s, printTerm 999 (head args)]))
        else Nothing in
 let _12 = if parsesAsBinder hop && length args == 1 && isGabs (head args)
           then Just (printBinder prec tm)
           else Nothing in
 let _13 = if canGetInfixStatus hop && length args == 2 then
          let bargs = if aright hop then
                        let (tms, tmt) = splitlist (destBinary hop) tm
                                         in tms ++ [tmt]
                      else
                        let (tmt, tms) = revSplitlist (destBinary hop) tm
                                         in tmt : tms in
          let (newprec, unspaced_binops) = (getPrec hop, [",", "..", "$"])
          in Just ((if newprec <= prec then parens else id) (hcat
                    (printTerm newprec (head bargs) :
                     map (\ x ->
                      if s `elem` unspaced_binops then hcat [text s,
                                                       printTerm newprec x]
                      else hcat
                       [text " ", text s, text " ", printTerm newprec x]
                     ) (tail bargs)
                  )))
        else Nothing in
 let _14 = if (isConst hop || isVar hop) && args == [] then
             let s' = if parsesAsBinder hop || canGetInfixStatus hop
                         || isPrefix tm then parens (text s) else text s
             in Just s'
           else Nothing in
 let _15 = case destComb tm of
              Just (l, r) -> let mem = case destConst l of
                                        Just (s', _) -> s' `elem`
                                          ["real_of_num", "int_of_num"]
                                        _ -> False
                            in Just ((if prec == 1000 then parens else id)
                                         (if not mem
                                          then hcat [printTerm 999 l, text " ",
                                                     printTerm 1000 r]
                                          else hcat [printTerm 999 l,
                                                     printTerm 1000 r]))
              _ -> Nothing
 in head (catMaybes [_1, _2, _3, _4, _5, _6, _7, _8, _9,
                     _10, _11, _12, _13, _14, _15, Just empty])

printTermSequence :: String -> Int -> [Term] -> Doc
printTermSequence sep' prec tms =
  if tms == [] then empty
  else hcat (punctuate (text sep') (map (printTerm prec) tms))

printBinder :: Int -> Term -> Doc
printBinder prec tm =
    let absf = isGabs tm in
    let s' = if absf then Just "\\"
             else case rator tm of
                   Just r -> Just (nameOf r)
                   Nothing -> Nothing in
    case s' of
     Just s -> let collectvs tm'
                    | absf =
                       if isAbs tm' then
                        case destAbs tm' of
                         Just (v, t) -> let (vs, bod) = collectvs t
                                        in ((False, v) : vs, bod)
                         _ -> ([], tm')
                       else if isGabs tm' then
                        case destGabs tm' of
                         Just (v, t) -> let (vs, bod) = collectvs t
                                        in ((True, v) : vs, bod)
                         _ -> ([], tm')
                       else ([], tm')
                    | isComb tm' =
                       case rator tm' of
                        Just r'' -> if nameOf r'' == s then
                         case rand tm' of
                          Just r'
                           | isAbs r' ->
                              case destAbs r' of
                               Just (v, t) -> let (vs, bod) = collectvs t
                                              in ((False, v) : vs, bod)
                               _ -> ([], tm')
                           | isGabs r' ->
                              case destGabs r' of
                               Just (v, t) -> let (vs, bod) = collectvs t
                                              in ((True, v) : vs, bod)
                               _ -> ([], tm')
                           | otherwise -> ([], tm')
                          _ -> ([], tm')
                         else ([], tm')
                        _ -> ([], tm')
                    | otherwise = ([], tm') in
       let (vs, bod) = collectvs tm in
         precParens prec (hcat ([
           text s,
           if all Char.isAlphaNum s then text " " else empty]
           ++ map (\ (b, x) -> hcat [
                 (if b then parens else id) (printTerm 0 x),
                 text " "] )
               (init vs)
           ++ [
            if fst (last vs) then text "(" else empty,
            printTerm 0 (snd (last vs)),
            if fst (last vs) then text ")" else empty,
            text ".",
            if length vs == 1 then text " " else empty,
            printTerm 0 bod
           ]
          ))
     _ -> empty

printClauses :: [[Term]] -> Doc
printClauses cls = case cls of
  [] -> empty
  c : cls' -> vcat (printClause c :
   map (\ cl -> hcat [text "| ", printClause cl]) cls')

printClause :: [Term] -> Doc
printClause cl = case cl of
  [p, g, r] -> hcat [printTerm 1 p,
                   text " when ",
                   printTerm 1 g,
                   text " -> ",
                   printTerm 1 r]
  [p, r] -> hcat [printTerm 1 p,
                 text " -> ",
                 printTerm 1 r]
  _ -> empty
