{- |
module: $Header$
description: OpenTheory interface
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.OpenTheory
where

import Control.Monad (guard)
import qualified Data.ByteString.Lazy as ByteString
import qualified Data.Char as Char
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Encoding as Text.Encoding
import Text.PrettyPrint ((<>),(<+>),($+$))
import qualified Text.PrettyPrint as PP

import HOL.Data
import HOL.Name
import HOL.Print
import qualified HOL.Rule as Rule
import HOL.Sequent (Sequent)
import qualified HOL.Sequent as Sequent
import qualified HOL.Subst as Subst
import qualified HOL.Term as Term
import qualified HOL.TermAlpha as TermAlpha
import HOL.Theory (Theory)
import qualified HOL.Theory as Theory
import HOL.Thm (Thm)
import qualified HOL.Thm as Thm
import qualified HOL.Type as Type
import qualified HOL.TypeVar as TypeVar
import qualified HOL.Var as Var

-------------------------------------------------------------------------------
-- Numbers
-------------------------------------------------------------------------------

type Number = Integer

parseNumber :: String -> Maybe Number
parseNumber =
    number
  where
    number [] = Nothing
    number ['0'] = Just 0
    number ('-' : s) = fmap negate $ positive s
    number s = positive s

    positive [] = Nothing
    positive ('0' : _) = Nothing
    positive s = digits 0 s

    digits z [] = Just z
    digits z (c : cs) = do
      guard (Char.isDigit c)
      let d = toInteger $ Char.digitToInt c
      digits (z * 10 + d) cs

-------------------------------------------------------------------------------
-- Interpretations
-------------------------------------------------------------------------------

-------------------------------------------------------------------------------
-- Objects
-------------------------------------------------------------------------------

data Object =
    NumObject Number
  | NameObject Name
  | ListObject [Object]
  | TypeOpObject TypeOp
  | TypeObject Type
  | ConstObject Const
  | VarObject Var
  | TermObject Term
  | ThmObject Thm
  deriving (Eq,Ord,Show)

class Objective a where
  toObject :: a -> Object

  fromObject :: Object -> Maybe a

instance Objective Object where
  toObject = id

  fromObject = Just

instance Objective Integer where
  toObject = NumObject

  fromObject (NumObject i) = Just i
  fromObject _ = Nothing

instance Objective Name where
  toObject = NameObject

  fromObject (NameObject n) = Just n
  fromObject _ = Nothing

instance Objective a => Objective [a] where
  toObject = ListObject . map toObject

  fromObject (ListObject l) = mapM fromObject l
  fromObject _ = Nothing

instance Objective TypeOp where
  toObject = TypeOpObject

  fromObject (TypeOpObject t) = Just t
  fromObject _ = Nothing

instance Objective Type where
  toObject = TypeObject

  fromObject (TypeObject ty) = Just ty
  fromObject _ = Nothing

instance Objective Const where
  toObject = ConstObject

  fromObject (ConstObject c) = Just c
  fromObject _ = Nothing

instance Objective Var where
  toObject = VarObject

  fromObject (VarObject v) = Just v
  fromObject _ = Nothing

instance Objective Term where
  toObject = TermObject

  fromObject (TermObject tm) = Just tm
  fromObject _ = Nothing

instance Objective Thm where
  toObject = ThmObject

  fromObject (ThmObject th) = Just th
  fromObject _ = Nothing

instance (Objective a, Objective b) => Objective (a,b) where
  toObject (a,b) = ListObject [toObject a, toObject b]

  fromObject (ListObject [x,y]) = do
    a <- fromObject x
    b <- fromObject y
    return (a,b)
  fromObject _ = Nothing

sequentObject :: Object -> Object -> Maybe Sequent
sequentObject h c = do
  h' <- fromObject h
  c' <- fromObject c
  Sequent.mk (Set.fromList $ map TermAlpha.mk h') (TermAlpha.mk c')

pushObject :: Objective a => a -> [Object] -> [Object]
pushObject a s = toObject a : s

push2Object :: (Objective a, Objective b) => a -> b -> [Object] -> [Object]
push2Object a b s = pushObject a $ pushObject b s

push3Object :: (Objective a, Objective b, Objective c) =>
               a -> b -> c -> [Object] -> [Object]
push3Object a b c s = pushObject a $ push2Object b c s

push4Object :: (Objective a, Objective b, Objective c, Objective d) =>
               a -> b -> c -> d -> [Object] -> [Object]
push4Object a b c d s = pushObject a $ push3Object b c d s

push5Object :: (Objective a, Objective b, Objective c, Objective d,
                Objective e) => a -> b -> c -> d -> e -> [Object] -> [Object]
push5Object a b c d e s = pushObject a $ push4Object b c d e s

popObject :: Objective a => [Object] -> Maybe (a,[Object])
popObject [] = Nothing
popObject (x : xs) = fmap (\a -> (a,xs)) (fromObject x)

pop2Object :: (Objective a, Objective b) => [Object] -> Maybe (a,b,[Object])
pop2Object s = do
  (a,s') <- popObject s
  (b,s'') <- popObject s'
  return (a,b,s'')

pop3Object :: (Objective a, Objective b, Objective c) =>
              [Object] -> Maybe (a,b,c,[Object])
pop3Object s = do
  (a,s') <- popObject s
  (b,c,s'') <- pop2Object s'
  return (a,b,c,s'')

pop4Object :: (Objective a, Objective b, Objective c, Objective d) =>
              [Object] -> Maybe (a,b,c,d,[Object])
pop4Object s = do
  (a,s') <- popObject s
  (b,c,d,s'') <- pop3Object s'
  return (a,b,c,d,s'')

pop5Object :: (Objective a, Objective b, Objective c, Objective d,
               Objective e) => [Object] -> Maybe (a,b,c,d,e,[Object])
pop5Object s = do
  (a,s') <- popObject s
  (b,c,d,e,s'') <- pop4Object s'
  return (a,b,c,d,e,s'')

instance Printable Object where
  toDoc (NumObject i) = toDoc i
  toDoc (NameObject n) = toDoc n
  toDoc (ListObject l) = toDoc l
  toDoc (TypeOpObject t) = toDoc t
  toDoc (TypeObject ty) = toDoc ty
  toDoc (ConstObject c) = toDoc c
  toDoc (VarObject v) = toDoc v
  toDoc (TermObject tm) = toDoc tm
  toDoc (ThmObject th) = toDoc th

-------------------------------------------------------------------------------
-- Commands
-------------------------------------------------------------------------------

data Command =
  -- Special commands
    NumCommand Number
  | NameCommand Name
  -- Regular commands
  | AbsTermCommand
  | AbsThmCommand
  | AppTermCommand
  | AppThmCommand
  | AssumeCommand
  | AxiomCommand
  | BetaConvCommand
  | ConsCommand
  | ConstCommand
  | ConstTermCommand
  | DeductAntisymCommand
  | DefCommand
  | DefineConstCommand
  | DefineConstListCommand
  | DefineTypeOpCommand
  | EqMpCommand
  | HdTlCommand
  | NilCommand
  | OpTypeCommand
  | PopCommand
  | PragmaCommand
  | ProveHypCommand
  | RefCommand
  | ReflCommand
  | RemoveCommand
  | SubstCommand
  | SymCommand
  | ThmCommand
  | TransCommand
  | TypeOpCommand
  | VarCommand
  | VarTermCommand
  | VarTypeCommand
  | VersionCommand
  -- Legacy commands
  | DefineTypeOpLegacyCommand
  deriving (Eq,Ord,Show)

regularCommands :: [(Command,String)]
regularCommands =
    [(AbsTermCommand,"absTerm"),
     (AbsThmCommand,"absThm"),
     (AppTermCommand,"appTerm"),
     (AppThmCommand,"appThm"),
     (AssumeCommand,"assume"),
     (AxiomCommand,"axiom"),
     (BetaConvCommand,"betaConv"),
     (ConsCommand,"cons"),
     (ConstCommand,"const"),
     (ConstTermCommand,"constTerm"),
     (DeductAntisymCommand,"deductAntisym"),
     (DefCommand,"def"),
     (DefineConstCommand,"defineConst"),
     (DefineConstListCommand,"defineConstList"),
     (DefineTypeOpCommand,"defineTypeOp"),
     (EqMpCommand,"eqMp"),
     (HdTlCommand,"hdTl"),
     (NilCommand,"nil"),
     (OpTypeCommand,"opType"),
     (PopCommand,"pop"),
     (PragmaCommand,"pragma"),
     (ProveHypCommand,"proveHyp"),
     (RefCommand,"ref"),
     (ReflCommand,"refl"),
     (RemoveCommand,"remove"),
     (SubstCommand,"subst"),
     (SymCommand,"sym"),
     (ThmCommand,"thm"),
     (TransCommand,"trans"),
     (TypeOpCommand,"typeOp"),
     (VarCommand,"var"),
     (VarTermCommand,"varTerm"),
     (VarTypeCommand,"varType"),
     (VersionCommand,"version")]

parseCommand :: Text -> Maybe Command
parseCommand =
    regular
  where
    regulars = Map.fromList $ map (\(c,s) -> (Text.pack s, c)) regularCommands

    regular t =
       case Map.lookup t regulars of
         Just c -> Just c
         Nothing -> special $ Text.unpack t

    special s =
       case parseName s of
         Just n -> Just $ NameCommand n
         Nothing -> fmap NumCommand $ parseNumber s

instance Printable Command where
  toDoc =
      go
    where
      regulars = Map.fromList $ map (\(c,s) -> (c, PP.text s)) regularCommands

      go (NumCommand i) = PP.integer i
      go (NameCommand n) = toDoc n
      go DefineTypeOpLegacyCommand = legacy DefineTypeOpCommand
      go c = case Map.lookup c regulars of
               Just d -> d
               Nothing -> error $ "Unprintable command: " ++ show c

      legacy c = go c <+> PP.text "(legacy)"

-------------------------------------------------------------------------------
-- OpenTheory article file versions
-------------------------------------------------------------------------------

type Version = Number

supportedCommand :: Version -> Command -> Bool
supportedCommand 5 DefineConstListCommand = False
supportedCommand 5 DefineTypeOpCommand = False
supportedCommand 5 HdTlCommand = False
supportedCommand 5 PragmaCommand = False
supportedCommand 5 ProveHypCommand = False
supportedCommand 5 SymCommand = False
supportedCommand 5 TransCommand = False
supportedCommand 5 VersionCommand = False
supportedCommand 6 DefineTypeOpLegacyCommand = False
supportedCommand _ _ = True

versionCommand :: Version -> Command -> Maybe Command
versionCommand 5 DefineTypeOpCommand = Just DefineTypeOpLegacyCommand
versionCommand _ VersionCommand = Nothing
versionCommand v c = if supportedCommand v c then Just c else Nothing

-------------------------------------------------------------------------------
-- Execution state
-------------------------------------------------------------------------------

data State =
    State
      {stack :: [Object],
       dict :: Map Number Object,
       theorems :: Set Thm}
  deriving (Eq,Ord,Show)

pushState :: Objective a => a -> State -> State
pushState a state = state {stack = pushObject a $ stack state}

push2State :: (Objective a, Objective b) => a -> b -> State -> State
push2State a b state = state {stack = push2Object a b $ stack state}

push5State :: (Objective a, Objective b, Objective c, Objective d,
               Objective e) => a -> b -> c -> d -> e -> State -> State
push5State a b c d e state =
    state {stack = push5Object a b c d e $ stack state}

popState :: Objective a => State -> Maybe (a,State)
popState state = do
  (a,s) <- popObject $ stack state
  return (a, state {stack = s})

pop2State :: (Objective a, Objective b) => State -> Maybe (a,b,State)
pop2State state = do
  (a,b,s) <- pop2Object $ stack state
  return (a, b, state {stack = s})

pop3State :: (Objective a, Objective b, Objective c) =>
             State -> Maybe (a,b,c,State)
pop3State state = do
  (a,b,c,s) <- pop3Object $ stack state
  return (a, b, c, state {stack = s})

pop5State :: (Objective a, Objective b, Objective c, Objective d,
              Objective e) => State -> Maybe (a,b,c,d,e,State)
pop5State state = do
  (a,b,c,d,e,s) <- pop5Object $ stack state
  return (a, b, c, d, e, state {stack = s})

peekState :: Objective a => State -> Maybe a
peekState = fmap fst . popState

defState :: Number -> Object -> State -> State
defState k x state = state {dict = Map.insert k x $ dict state}

refState :: Number -> State -> Maybe Object
refState k state = Map.lookup k $ dict state

removeState :: Number -> State -> Maybe (Object,State)
removeState k state = do
  let d = dict state
  x <- Map.lookup k d
  let s = state {dict = Map.delete k d}
  return (x,s)

thmState :: Thm -> State -> State
thmState th state = state {theorems = Set.insert th $ theorems state}

initialState :: State
initialState =
    State
      {stack = [],
       dict = Map.empty,
       theorems = Set.empty}

executeCommand :: Theory -> State -> Command -> Maybe State
executeCommand thy state cmd =
    case cmd of
      NumCommand i -> Just $ pushState i state
      NameCommand n -> Just $ pushState n state
      AbsTermCommand -> do
        (b,v,s) <- pop2State state
        let tm = Term.mkAbs v b
        return $ pushState tm s
      AbsThmCommand -> do
        (b,v,s) <- pop2State state
        th <- Thm.mkAbs v b
        return $ pushState th s
      AppTermCommand -> do
        (x,f,s) <- pop2State state
        tm <- Term.mkApp f x
        return $ pushState tm s
      AppThmCommand -> do
        (x,f,s) <- pop2State state
        th <- Thm.mkApp f x
        return $ pushState th s
      AssumeCommand -> do
        (tm,s) <- popState state
        th <- Thm.assume tm
        return $ pushState th s
      AxiomCommand -> do
        (c,h,s) <- pop2State state
        sq <- sequentObject h c
        th <- Theory.lookupThm thy sq
        return $ pushState th s
      BetaConvCommand -> do
        (tm,s) <- popState state
        th <- Thm.betaConv tm
        return $ pushState th s
      ConsCommand -> do
        (t,h,s) <- pop2State state
        return $ pushState ((h :: Object) : t) s
      ConstCommand -> do
        (n,s) <- popState state
        c <- Theory.lookupConst thy n
        return $ pushState c s
      ConstTermCommand -> do
        (ty,c,s) <- pop2State state
        let tm = Term.mkConst c ty
        return $ pushState tm s
      DeductAntisymCommand -> do
        (th1,th0,s) <- pop2State state
        let th = Thm.deductAntisym th0 th1
        return $ pushState th s
      DefCommand -> do
        (k,state') <- popState state
        x <- peekState state'
        return $ defState k x state'
      DefineConstCommand -> do
        (tm,n,s) <- pop2State state
        (c,th) <- Thm.defineConst n tm
        return $ push2State th c s
      DefineConstListCommand -> do
        (th,nvs,s) <- pop2State state
        (cs,def) <- Rule.defineConstList nvs th
        return $ push2State def cs s
      DefineTypeOpCommand -> do
        (th,tvn,rn,an,tn,s) <- pop5State state
        let tv = map TypeVar.mk tvn
        (t,a,r,ar,ra) <- Thm.defineTypeOp tn an rn tv th
        return $ push5State ra ar r a t s
      DefineTypeOpLegacyCommand -> do
        (th,tvn,rn,an,tn,s) <- pop5State state
        let tv = map TypeVar.mk tvn
        (t,a,r,ar,ra) <- Rule.defineTypeOpLegacy tn an rn tv th
        return $ push5State ra ar r a t s
      EqMpCommand -> do
        (th1,th0,s) <- pop2State state
        th <- Thm.eqMp th0 th1
        return $ pushState th s
      HdTlCommand -> do
        (l,s) <- popState state
        (h,t) <- case l of
                   [] -> Nothing
                   x : xs -> Just (x,xs)
        return $ push2State t (h :: Object) s
      NilCommand -> Just $ pushState ([] :: [Object]) state
      OpTypeCommand -> do
        (tys,t,s) <- pop2State state
        let ty = Type.mkOp t tys
        return $ pushState ty s
      PopCommand -> do
        (_,s) <- (popState :: State -> Maybe (Object,State)) state
        return s
      PragmaCommand -> do
        (_,s) <- (popState :: State -> Maybe (Object,State)) state
        return s
      ProveHypCommand -> do
        (th1,th0,s) <- pop2State state
        th <- Rule.proveHyp th0 th1
        return $ pushState th s
      RefCommand -> do
        (k,s) <- popState state
        x <- refState k s
        return $ pushState x s
      ReflCommand -> do
        (tm,s) <- popState state
        let th = Thm.refl tm
        return $ pushState th s
      RemoveCommand -> do
        (k,s) <- popState state
        (x,s') <- removeState k s
        return $ pushState x s'
      SubstCommand -> do
        (th,(nty,vtm),s) <- pop2State state
        let vty = map (\(n,ty) -> (TypeVar.mk n, ty)) nty
        sub <- Subst.fromList vty vtm
        let th' = Thm.subst sub th
        return $ pushState th' s
      SymCommand -> do
        (th,s) <- popState state
        th' <- Rule.sym th
        return $ pushState th' s
      ThmCommand -> do
        (c,h,th,s) <- pop3State state
        sq <- sequentObject h c
        th' <- Rule.alphaSequent sq th
        return $ thmState th' s
      TransCommand -> do
        (th1,th0,s) <- pop2State state
        th <- Rule.trans th0 th1
        return $ pushState th s
      TypeOpCommand -> do
        (n,s) <- popState state
        t <- Theory.lookupTypeOp thy n
        return $ pushState t s
      VarCommand -> do
        (ty,n,s) <- pop2State state
        let v = Var.mk n ty
        return $ pushState v s
      VarTermCommand -> do
        (v,s) <- popState state
        let tm = Term.mkVar v
        return $ pushState tm s
      VarTypeCommand -> do
        (n,s) <- popState state
        let ty = Type.mkVar $ TypeVar.mk n
        return $ pushState ty s
      _ -> Nothing

instance Printable State where
  toDoc state =
      stackDoc (stack state) $+$
      dictDoc (dict state) $+$
      theoremsDoc (theorems state)
    where
      stackDoc s = PP.text "stack =" <+> (PP.brackets $ objsDoc 5 s)

      dictDoc d = PP.text "dictionary =" <+> (PP.braces $ PP.int $ Map.size d)

      theoremsDoc e = PP.text "theorems =" <+> (PP.braces $ PP.int $ Set.size e)

      objsDoc k s =
          PP.sep $ PP.punctuate PP.comma ds
        where
          ds = if x <= 1 then map toDoc s
               else map toDoc (take k s) ++ [dx]
          dx = dots <> PP.int x <+> PP.text "more objects" <> dots
          dots = PP.text "..."
          x = length s - k

-------------------------------------------------------------------------------
-- Reading an OpenTheory article file
-------------------------------------------------------------------------------

type LineNumber = Integer

readArticle :: Theory -> FilePath -> IO (Set Thm)
readArticle thy art = do
    bs <- ByteString.readFile art
    let txt = Text.Encoding.decodeUtf8 bs
    let ls = zip [1..] $ Text.lines txt
    let (v,cs) = getVersion $ map parse $ filter notComment ls
    let s = List.foldl' execute initialState $ map (version v) cs
    return $ theorems s
  where
    notComment :: (LineNumber,Text) -> Bool
    notComment (_,t) = Text.null t || Text.head t /= '#'

    parse :: (LineNumber,Text) -> (LineNumber,Command)
    parse (l,t) =
        case parseCommand t of
          Just c -> (l,c)
          Nothing -> error $ err "unparseable command" l (show t)

    getVersion :: [(LineNumber,Command)] -> (Version,[(LineNumber,Command)])
    getVersion ((l, NumCommand v) : (_,VersionCommand) : cs) =
        if v == 6 then (v,cs)
        else error $ err "bad version number" l (show v)
    getVersion cs = (5,cs)

    version :: Version -> (LineNumber,Command) -> (LineNumber,Command)
    version v (l,c) =
        case versionCommand v c of
          Just c' -> (l,c')
          Nothing -> error $ err "unsupported command" l e
                     where e = "command " ++ toString c ++
                               " not supported in version " ++ show v ++
                               " article files"

    execute :: State -> (LineNumber,Command) -> State
    execute s (l,c) =
        case executeCommand thy s c of
          Just s' -> s'
          Nothing -> error $ err e l (toString s)
                     where e = "couldn't execute command " ++ toString c

    err :: String -> LineNumber -> String -> String
    err e l s = art ++ ":" ++ show l ++ ": " ++ e ++ ":\n" ++ s