{-|
  Module:    HaskHOL.Core.Parser.TermParser
  Copyright: (c) The University of Kansas 2013
  LICENSE:   BSD3

  Maintainer:  ecaustin@ittc.ku.edu
  Stability:   unstable
  Portability: unknown

  This module defines the parser for 'HOLTerm's that satisfies the following BNF
  grammar:

@
  PRETERM            :: APPL_PRETERM binop APPL_PRETERM                     
                      | APPL_PRETERM                                        
                                                                           
  APPL_PRETERM       :: BINDER_PRETERM+                               
                      | BINDER_PRETERM : type                                  
                                                                           
  BINDER_PRETERM     :: tybinder small-type-variables . PRETERM             
                      | binder VARSTRUCT_PRETERM+ . PRETERM                 
                      | let PRETERM and ... and PRETERM in PRETERM          
                      | TYPED_PRETERM                                       
                                                                            
  TYPED_PRETERM      :: TYINST (tyop-var : PRETYPE)+ ATOMIC_PRETERM         
                      | ATOMIC_PRETERM                                   
                                                                            
  VARSTRUCT_PRETERM  :: ATOMIC_PRETERM : type                               
                      | ATOMIC_PRETERM                                      
                                                                           
  ATOMIC_PRETERM     :: ( PRETERM )                                         
                      | [: type]                                 
                      | [ PRETERM; .. ; PRETERM ]                  
                      | if PRETERM then PRETERM else PRETERM                
                      | identifier                                          
@                                                                          
 
  Note that arbitrary atomic preterms, typed or untyped, are allowed as     
  varstructs in order to simplify parsing.  We do not make the same 
  simplification for @TYINST@ terms in order to avoid the mixing of terms, 
  types, and type operators.   

  Also note that a number of advanced HOL term features, mostly relating to sets
  and patterns, are not currently supported by the parser.  These will be added
  in as the relevant logic libraries are added to the system.

  As a heads up, the error messages thrown by this parser leave much to be
  desired.
-}
module HaskHOL.Core.Parser.TermParser
    ( pterm
    ) where

import HaskHOL.Core.Lib hiding (many)
import HaskHOL.Core.State

import HaskHOL.Core.Parser.Lib
import HaskHOL.Core.Parser.TypeParser

-- | Parser for HOL terms.
pterm :: MyParser thry PreTerm
pterm = 
    do mywhiteSpace
       ctxt <- getState
       buildExpressionParser (partitionOps ctxt) pappl

pappl :: MyParser thry PreTerm
pappl = 
    try (do prefs <- pprefixes
            if null prefs
               then fail "pappl: no prefix found"
               else do bod <- pappl
                       return $! foldr PComb bod prefs)
    <|> (do tms <- many1 pbinder
            let tm = mkPComb tms
            pas tm <|> return tm)

pbinder :: MyParser thry PreTerm
pbinder = 
    (do myreserved "let"
        tms <- pterm `sepBy1` myreserved "and"
        myreserved "in"
        bod <- pterm
        case mkLet tms bod of
          Nothing -> fail "pterm: invalid let construction"
          Just tm -> return tm)
    <|> do (ctxt, _) <- getState
           bind <- choiceOp $ binders ctxt
           (do vars <- many1 pvar
               myreservedOp "."
               bod <- pterm
               return $! mkBinders bind vars bod)
            <|> (return $! PVar bind dpty)
    <|> do (ctxt, _) <- getState
           bind <- choiceOp $ tyBinders ctxt
           (do vars <- many1 psmall
               myreservedOp "."
               bod <- pterm
               return $! mkTyBinders bind vars bod)
            <|> (return $! PVar bind dpty)
    <|> ptyped
    where 

ptyped :: MyParser thry PreTerm
ptyped = 
    (do myreserved "TYINST"
        vars <- many1 pinst
        tm <- patomic
        return $! PInst vars tm)
    <|> patomic
    where pinst :: MyParser thry (PreType, String)
          pinst = myparens $ do myreservedOp "_"
                                x <- myidentifier
                                myreservedOp ":"
                                ty <- ptype
                                return (ty, x)
                              

pvar :: MyParser thry PreTerm
pvar =
    do tm <- patomic
       pas tm <|> return tm

pas :: PreTerm -> MyParser thry PreTerm
pas ptm =
    do myreservedOp ":"
       ty <- ptype
       return $! PAs ptm ty

patomic :: MyParser thry PreTerm
patomic = 
    myparens (pterm <|> (do x <- myoperator
                            return $! PVar x dpty))
    <|> mybrackets 
         ((do myreservedOp ":"
              ty <- ptype
              return $! PApp ty)
          <|> (do tms <- mysemiSep pterm
                  return (foldr (\ x y -> PVar "CONS" dpty `PComb` 
                                          x `PComb` y)
                              (PVar "NILS" dpty) tms)))
    {- <|> mybraces
          ((do tms <- mycommaSep pterm
               return $! foldr (\ x y -> PComb (PComb (PVar "INSERT" dpty) x) y)
                           (PVar "EMPTY" dpty) tms)
           <|> (do tms <- mypipeSep pterm
                   if length tms == 2
                      then -- setabs
                      else if length tms == 3
                      then -- setcompr))
    -}
    <|> (do myreserved "if"
            c <- pterm
            myreserved "then"
            t <- pterm
            myreserved "else"
            e <- pterm
            return $! PComb (PComb (PComb (PVar "COND" dpty) c) t) e)
    <|> (do x <- myidentifier
            return $! PVar x dpty)

pprefixes :: MyParser thry [PreTerm]
pprefixes =
    do (ctxt, _) <- getState
       pref <- myoperator
       let prefOps = sortBy (\ x y -> compare (length y) (length x)) $ 
                       prefixes ctxt
       return $! splitPref pref prefOps []
    where splitPref :: String -> [String] -> [PreTerm] -> [PreTerm]
          splitPref _ [] acc = acc
          splitPref ops prefs@(p:ps) acc =
              case stripPrefix p ops of
                Nothing -> splitPref ops ps acc
                Just ops' -> 
                    let acc' = acc ++ [PVar p dpty] in
                      if null ops' then acc'
                      else splitPref ops' prefs acc'
                

-- helper functions
mkPComb :: [PreTerm] -> PreTerm
mkPComb (tm:[]) = tm
mkPComb (tm:tms) = foldr (flip PComb) tm (reverse tms)
mkPComb _ = error "parser: mkPComb used without many1 parser combinator"

pdestEq :: PreTerm -> Maybe (PreTerm, PreTerm)
pdestEq (PComb (PComb (PVar "=" _) l) r) = Just (l, r)
pdestEq (PComb (PComb (PVar "<=>" _) l) r) = Just (l, r)
pdestEq _ = Nothing

mkLet :: [PreTerm] -> PreTerm -> Maybe PreTerm
mkLet binds bod = case length tms of
                    0 -> Nothing
                    _ -> Just $ foldl PComb letstart tms
    where (vars, tms) = unzip $ mapMaybe pdestEq binds
          letend = PComb (PVar "LET_END" dpty) bod
          ab = foldr PAbs letend vars
          letstart = PComb (PVar "LET" dpty) ab

mkBinder :: String -> PreTerm -> PreTerm -> PreTerm
mkBinder "\\" v bod = PAbs v bod
mkBinder n v bod = PComb (PVar n dpty) $ PAbs v bod

mkBinders :: String -> [PreTerm] -> PreTerm -> PreTerm
mkBinders bind vars bod = foldr (mkBinder bind) bod vars

mkTyBinder :: String -> PreType -> PreTerm -> PreTerm
mkTyBinder "\\\\" v bod = TyPAbs v bod
mkTyBinder n v bod = PComb (PVar n dpty) $ TyPAbs v bod

mkTyBinders :: String -> [PreType] -> PreTerm -> PreTerm
mkTyBinders bind vars bod = foldr (mkTyBinder bind) bod vars

-- build op table for expression parser from context
-- Note: prefix operators are handled separately in pprefixes
partitionOps :: (HOLContext thry, [(String, Int)]) ->
                OperatorTable Char (HOLContext thry, [(String, Int)]) PreTerm
partitionOps (ctxt, _) = map (map mkOp) . 
                         group' (\ (_, (x, _)) (_, (y, _)) -> x == y) $ 
                         infixes ctxt
  where mkOp :: (String, (Int, Assoc)) -> 
                Operator Char (HOLContext thry, [(String, Int)]) PreTerm
        mkOp (name, (_, a)) = 
            Infix (do myreservedOp name
                      return (\ x y -> PComb (PComb (PVar name dpty) x) y)) a