{- |
module: $Header$
description: OpenTheory article files
license: MIT

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

module HOL.OpenTheory.Article
where

import qualified Data.ByteString.Lazy as ByteString
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict 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 Prelude hiding ((<>))
import Text.Parsec.Text.Lazy ()
import Text.PrettyPrint ((<>),(<+>),($+$))
import qualified Text.PrettyPrint as PP

import HOL.Data
import HOL.Name
import HOL.OpenTheory.Interpret (Interpret,interpretConst,interpretTypeOp)
import HOL.Parse
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
-------------------------------------------------------------------------------

newtype Number = Number Integer
  deriving (Number -> Number -> Bool
(Number -> Number -> Bool)
-> (Number -> Number -> Bool) -> Eq Number
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Number -> Number -> Bool
$c/= :: Number -> Number -> Bool
== :: Number -> Number -> Bool
$c== :: Number -> Number -> Bool
Eq,Eq Number
Eq Number
-> (Number -> Number -> Ordering)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Number)
-> (Number -> Number -> Number)
-> Ord Number
Number -> Number -> Bool
Number -> Number -> Ordering
Number -> Number -> Number
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Number -> Number -> Number
$cmin :: Number -> Number -> Number
max :: Number -> Number -> Number
$cmax :: Number -> Number -> Number
>= :: Number -> Number -> Bool
$c>= :: Number -> Number -> Bool
> :: Number -> Number -> Bool
$c> :: Number -> Number -> Bool
<= :: Number -> Number -> Bool
$c<= :: Number -> Number -> Bool
< :: Number -> Number -> Bool
$c< :: Number -> Number -> Bool
compare :: Number -> Number -> Ordering
$ccompare :: Number -> Number -> Ordering
$cp1Ord :: Eq Number
Ord,Int -> Number -> ShowS
[Number] -> ShowS
Number -> String
(Int -> Number -> ShowS)
-> (Number -> String) -> ([Number] -> ShowS) -> Show Number
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Number] -> ShowS
$cshowList :: [Number] -> ShowS
show :: Number -> String
$cshow :: Number -> String
showsPrec :: Int -> Number -> ShowS
$cshowsPrec :: Int -> Number -> ShowS
Show)

instance Printable Number where
  toDoc :: Number -> Doc
toDoc (Number Integer
i) = Integer -> Doc
PP.integer Integer
i

instance Parsable Number where
  parser :: Parsec Text st Number
parser = do
      Integer
i <- Parsec Text st Integer
forall a st. Parsable a => Parsec Text st a
parser
      Number -> Parsec Text st Number
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Number
Number Integer
i)

  fromText :: Text -> Maybe Number
fromText = (Integer -> Number) -> Maybe Integer -> Maybe Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Number
Number (Maybe Integer -> Maybe Number)
-> (Text -> Maybe Integer) -> Text -> Maybe Number
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Maybe Integer
forall a. Parsable a => Text -> Maybe a
fromText

  fromString :: String -> Maybe Number
fromString = (Integer -> Number) -> Maybe Integer -> Maybe Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Number
Number (Maybe Integer -> Maybe Number)
-> (String -> Maybe Integer) -> String -> Maybe Number
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe Integer
forall a. Parsable a => String -> Maybe a
fromString

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

data Object =
    NumberObject Number
  | NameObject Name
  | ListObject [Object]
  | TypeOpObject TypeOp
  | TypeObject Type
  | ConstObject Const
  | VarObject Var
  | TermObject Term
  | ThmObject Thm
  deriving (Object -> Object -> Bool
(Object -> Object -> Bool)
-> (Object -> Object -> Bool) -> Eq Object
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Object -> Object -> Bool
$c/= :: Object -> Object -> Bool
== :: Object -> Object -> Bool
$c== :: Object -> Object -> Bool
Eq,Eq Object
Eq Object
-> (Object -> Object -> Ordering)
-> (Object -> Object -> Bool)
-> (Object -> Object -> Bool)
-> (Object -> Object -> Bool)
-> (Object -> Object -> Bool)
-> (Object -> Object -> Object)
-> (Object -> Object -> Object)
-> Ord Object
Object -> Object -> Bool
Object -> Object -> Ordering
Object -> Object -> Object
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Object -> Object -> Object
$cmin :: Object -> Object -> Object
max :: Object -> Object -> Object
$cmax :: Object -> Object -> Object
>= :: Object -> Object -> Bool
$c>= :: Object -> Object -> Bool
> :: Object -> Object -> Bool
$c> :: Object -> Object -> Bool
<= :: Object -> Object -> Bool
$c<= :: Object -> Object -> Bool
< :: Object -> Object -> Bool
$c< :: Object -> Object -> Bool
compare :: Object -> Object -> Ordering
$ccompare :: Object -> Object -> Ordering
$cp1Ord :: Eq Object
Ord,Int -> Object -> ShowS
[Object] -> ShowS
Object -> String
(Int -> Object -> ShowS)
-> (Object -> String) -> ([Object] -> ShowS) -> Show Object
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Object] -> ShowS
$cshowList :: [Object] -> ShowS
show :: Object -> String
$cshow :: Object -> String
showsPrec :: Int -> Object -> ShowS
$cshowsPrec :: Int -> Object -> ShowS
Show)

class Objective a where
  toObject :: a -> Object

  fromObject :: Object -> Maybe a

instance Objective Object where
  toObject :: Object -> Object
toObject = Object -> Object
forall a. a -> a
id

  fromObject :: Object -> Maybe Object
fromObject = Object -> Maybe Object
forall a. a -> Maybe a
Just

instance Objective Number where
  toObject :: Number -> Object
toObject = Number -> Object
NumberObject

  fromObject :: Object -> Maybe Number
fromObject (NumberObject Number
i) = Number -> Maybe Number
forall a. a -> Maybe a
Just Number
i
  fromObject Object
_ = Maybe Number
forall a. Maybe a
Nothing

instance Objective Name where
  toObject :: Name -> Object
toObject = Name -> Object
NameObject

  fromObject :: Object -> Maybe Name
fromObject (NameObject Name
n) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
  fromObject Object
_ = Maybe Name
forall a. Maybe a
Nothing

instance Objective a => Objective [a] where
  toObject :: [a] -> Object
toObject = [Object] -> Object
ListObject ([Object] -> Object) -> ([a] -> [Object]) -> [a] -> Object
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Object) -> [a] -> [Object]
forall a b. (a -> b) -> [a] -> [b]
map a -> Object
forall a. Objective a => a -> Object
toObject

  fromObject :: Object -> Maybe [a]
fromObject (ListObject [Object]
l) = (Object -> Maybe a) -> [Object] -> Maybe [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Object -> Maybe a
forall a. Objective a => Object -> Maybe a
fromObject [Object]
l
  fromObject Object
_ = Maybe [a]
forall a. Maybe a
Nothing

instance Objective TypeOp where
  toObject :: TypeOp -> Object
toObject = TypeOp -> Object
TypeOpObject

  fromObject :: Object -> Maybe TypeOp
fromObject (TypeOpObject TypeOp
t) = TypeOp -> Maybe TypeOp
forall a. a -> Maybe a
Just TypeOp
t
  fromObject Object
_ = Maybe TypeOp
forall a. Maybe a
Nothing

instance Objective Type where
  toObject :: Type -> Object
toObject = Type -> Object
TypeObject

  fromObject :: Object -> Maybe Type
fromObject (TypeObject Type
ty) = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
  fromObject Object
_ = Maybe Type
forall a. Maybe a
Nothing

instance Objective Const where
  toObject :: Const -> Object
toObject = Const -> Object
ConstObject

  fromObject :: Object -> Maybe Const
fromObject (ConstObject Const
c) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
  fromObject Object
_ = Maybe Const
forall a. Maybe a
Nothing

instance Objective Var where
  toObject :: Var -> Object
toObject = Var -> Object
VarObject

  fromObject :: Object -> Maybe Var
fromObject (VarObject Var
v) = Var -> Maybe Var
forall a. a -> Maybe a
Just Var
v
  fromObject Object
_ = Maybe Var
forall a. Maybe a
Nothing

instance Objective Term where
  toObject :: Term -> Object
toObject = Term -> Object
TermObject

  fromObject :: Object -> Maybe Term
fromObject (TermObject Term
tm) = Term -> Maybe Term
forall a. a -> Maybe a
Just Term
tm
  fromObject Object
_ = Maybe Term
forall a. Maybe a
Nothing

instance Objective Thm where
  toObject :: Thm -> Object
toObject = Thm -> Object
ThmObject

  fromObject :: Object -> Maybe Thm
fromObject (ThmObject Thm
th) = Thm -> Maybe Thm
forall a. a -> Maybe a
Just Thm
th
  fromObject Object
_ = Maybe Thm
forall a. Maybe a
Nothing

instance (Objective a, Objective b) => Objective (a,b) where
  toObject :: (a, b) -> Object
toObject (a
a,b
b) = [Object] -> Object
ListObject [a -> Object
forall a. Objective a => a -> Object
toObject a
a, b -> Object
forall a. Objective a => a -> Object
toObject b
b]

  fromObject :: Object -> Maybe (a, b)
fromObject (ListObject [Object
x,Object
y]) = do
    a
a <- Object -> Maybe a
forall a. Objective a => Object -> Maybe a
fromObject Object
x
    b
b <- Object -> Maybe b
forall a. Objective a => Object -> Maybe a
fromObject Object
y
    (a, b) -> Maybe (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a,b
b)
  fromObject Object
_ = Maybe (a, b)
forall a. Maybe a
Nothing

sequentObject :: Object -> Object -> Maybe Sequent
sequentObject :: Object -> Object -> Maybe Sequent
sequentObject Object
h Object
c = do
  [Term]
h' <- Object -> Maybe [Term]
forall a. Objective a => Object -> Maybe a
fromObject Object
h
  Term
c' <- Object -> Maybe Term
forall a. Objective a => Object -> Maybe a
fromObject Object
c
  Set TermAlpha -> TermAlpha -> Maybe Sequent
Sequent.mk ([TermAlpha] -> Set TermAlpha
forall a. Ord a => [a] -> Set a
Set.fromList ([TermAlpha] -> Set TermAlpha) -> [TermAlpha] -> Set TermAlpha
forall a b. (a -> b) -> a -> b
$ (Term -> TermAlpha) -> [Term] -> [TermAlpha]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TermAlpha
TermAlpha.mk [Term]
h') (Term -> TermAlpha
TermAlpha.mk Term
c')

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

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

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

push4Object :: (Objective a, Objective b, Objective c, Objective d) =>
               a -> b -> c -> d -> [Object] -> [Object]
push4Object :: a -> b -> c -> d -> [Object] -> [Object]
push4Object a
a b
b c
c d
d [Object]
s = a -> [Object] -> [Object]
forall a. Objective a => a -> [Object] -> [Object]
pushObject a
a ([Object] -> [Object]) -> [Object] -> [Object]
forall a b. (a -> b) -> a -> b
$ b -> c -> d -> [Object] -> [Object]
forall a b c.
(Objective a, Objective b, Objective c) =>
a -> b -> c -> [Object] -> [Object]
push3Object b
b c
c d
d [Object]
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 -> [Object] -> [Object]
push5Object a
a b
b c
c d
d e
e [Object]
s = a -> [Object] -> [Object]
forall a. Objective a => a -> [Object] -> [Object]
pushObject a
a ([Object] -> [Object]) -> [Object] -> [Object]
forall a b. (a -> b) -> a -> b
$ b -> c -> d -> e -> [Object] -> [Object]
forall a b c d.
(Objective a, Objective b, Objective c, Objective d) =>
a -> b -> c -> d -> [Object] -> [Object]
push4Object b
b c
c d
d e
e [Object]
s

popObject :: Objective a => [Object] -> Maybe (a,[Object])
popObject :: [Object] -> Maybe (a, [Object])
popObject [] = Maybe (a, [Object])
forall a. Maybe a
Nothing
popObject (Object
x : [Object]
xs) = (a -> (a, [Object])) -> Maybe a -> Maybe (a, [Object])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
a -> (a
a,[Object]
xs)) (Object -> Maybe a
forall a. Objective a => Object -> Maybe a
fromObject Object
x)

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

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

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

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

instance Printable Object where
  toDoc :: Object -> Doc
toDoc (NumberObject Number
i) = Number -> Doc
forall a. Printable a => a -> Doc
toDoc Number
i
  toDoc (NameObject Name
n) = Name -> Doc
forall a. Printable a => a -> Doc
toDoc Name
n
  toDoc (ListObject [Object]
l) = [Object] -> Doc
forall a. Printable a => a -> Doc
toDoc [Object]
l
  toDoc (TypeOpObject TypeOp
t) = TypeOp -> Doc
forall a. Printable a => a -> Doc
toDoc TypeOp
t
  toDoc (TypeObject Type
ty) = Type -> Doc
forall a. Printable a => a -> Doc
toDoc Type
ty
  toDoc (ConstObject Const
c) = Const -> Doc
forall a. Printable a => a -> Doc
toDoc Const
c
  toDoc (VarObject Var
v) = Var -> Doc
forall a. Printable a => a -> Doc
toDoc Var
v
  toDoc (TermObject Term
tm) = Term -> Doc
forall a. Printable a => a -> Doc
toDoc Term
tm
  toDoc (ThmObject Thm
th) = Thm -> Doc
forall a. Printable a => a -> Doc
toDoc Thm
th

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

data Command =
  -- Special commands
    NumberCommand 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 (Command -> Command -> Bool
(Command -> Command -> Bool)
-> (Command -> Command -> Bool) -> Eq Command
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Command -> Command -> Bool
$c/= :: Command -> Command -> Bool
== :: Command -> Command -> Bool
$c== :: Command -> Command -> Bool
Eq,Eq Command
Eq Command
-> (Command -> Command -> Ordering)
-> (Command -> Command -> Bool)
-> (Command -> Command -> Bool)
-> (Command -> Command -> Bool)
-> (Command -> Command -> Bool)
-> (Command -> Command -> Command)
-> (Command -> Command -> Command)
-> Ord Command
Command -> Command -> Bool
Command -> Command -> Ordering
Command -> Command -> Command
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Command -> Command -> Command
$cmin :: Command -> Command -> Command
max :: Command -> Command -> Command
$cmax :: Command -> Command -> Command
>= :: Command -> Command -> Bool
$c>= :: Command -> Command -> Bool
> :: Command -> Command -> Bool
$c> :: Command -> Command -> Bool
<= :: Command -> Command -> Bool
$c<= :: Command -> Command -> Bool
< :: Command -> Command -> Bool
$c< :: Command -> Command -> Bool
compare :: Command -> Command -> Ordering
$ccompare :: Command -> Command -> Ordering
$cp1Ord :: Eq Command
Ord,Int -> Command -> ShowS
[Command] -> ShowS
Command -> String
(Int -> Command -> ShowS)
-> (Command -> String) -> ([Command] -> ShowS) -> Show Command
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Command] -> ShowS
$cshowList :: [Command] -> ShowS
show :: Command -> String
$cshow :: Command -> String
showsPrec :: Int -> Command -> ShowS
$cshowsPrec :: Int -> Command -> ShowS
Show)

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

instance Parsable Command where
  parser :: Parsec Text st Command
parser = String -> Parsec Text st Command
forall a. HasCallStack => String -> a
error String
"Parsec Command parser not implemented"

  fromText :: Text -> Maybe Command
fromText = Text -> Maybe Command
regular
    where
      regular :: Text -> Maybe Command
regular Text
t =
         case Text -> Map Text Command -> Maybe Command
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
t Map Text Command
regulars of
           Just Command
c -> Command -> Maybe Command
forall a. a -> Maybe a
Just Command
c
           Maybe Command
Nothing -> Text -> Maybe Command
special Text
t

      special :: Text -> Maybe Command
special Text
t =
         case Text -> Maybe Name
forall a. Parsable a => Text -> Maybe a
fromText Text
t of
           Just Name
n -> Command -> Maybe Command
forall a. a -> Maybe a
Just (Command -> Maybe Command) -> Command -> Maybe Command
forall a b. (a -> b) -> a -> b
$ Name -> Command
NameCommand Name
n
           Maybe Name
Nothing -> (Number -> Command) -> Maybe Number -> Maybe Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Number -> Command
NumberCommand (Maybe Number -> Maybe Command) -> Maybe Number -> Maybe Command
forall a b. (a -> b) -> a -> b
$ Text -> Maybe Number
forall a. Parsable a => Text -> Maybe a
fromText Text
t

      regulars :: Map Text Command
regulars = [(Text, Command)] -> Map Text Command
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Text, Command)] -> Map Text Command)
-> [(Text, Command)] -> Map Text Command
forall a b. (a -> b) -> a -> b
$ ((Command, String) -> (Text, Command))
-> [(Command, String)] -> [(Text, Command)]
forall a b. (a -> b) -> [a] -> [b]
map (Command, String) -> (Text, Command)
forall b. (b, String) -> (Text, b)
mk [(Command, String)]
regularCommands
        where
          mk :: (b, String) -> (Text, b)
mk (b
c,String
s) = (String -> Text
Text.pack String
s, b
c)

instance Printable Command where
  toDoc :: Command -> Doc
toDoc =
      Command -> Doc
go
    where
      regulars :: Map Command Doc
regulars = [(Command, Doc)] -> Map Command Doc
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Command, Doc)] -> Map Command Doc)
-> [(Command, Doc)] -> Map Command Doc
forall a b. (a -> b) -> a -> b
$ ((Command, String) -> (Command, Doc))
-> [(Command, String)] -> [(Command, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Command
c,String
s) -> (Command
c, String -> Doc
PP.text String
s)) [(Command, String)]
regularCommands

      go :: Command -> Doc
go (NumberCommand Number
i) = Number -> Doc
forall a. Printable a => a -> Doc
toDoc Number
i
      go (NameCommand Name
n) = Name -> Doc
forall a. Printable a => a -> Doc
toDoc Name
n
      go Command
DefineTypeOpLegacyCommand = Command -> Doc
legacy Command
DefineTypeOpCommand
      go Command
c = case Command -> Map Command Doc -> Maybe Doc
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Command
c Map Command Doc
regulars of
               Just Doc
d -> Doc
d
               Maybe Doc
Nothing -> String -> Doc
forall a. HasCallStack => String -> a
error (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Unprintable command: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Command -> String
forall a. Show a => a -> String
show Command
c

      legacy :: Command -> Doc
legacy Command
c = Command -> Doc
go Command
c Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"(legacy)"

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

type Version = Number

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

versionCommand :: Version -> Command -> Maybe Command
versionCommand :: Number -> Command -> Maybe Command
versionCommand (Number Integer
5) Command
DefineTypeOpCommand = Command -> Maybe Command
forall a. a -> Maybe a
Just Command
DefineTypeOpLegacyCommand
versionCommand Number
_ Command
VersionCommand = Maybe Command
forall a. Maybe a
Nothing
versionCommand Number
v Command
c = if Number -> Command -> Bool
supportedCommand Number
v Command
c then Command -> Maybe Command
forall a. a -> Maybe a
Just Command
c else Maybe Command
forall a. Maybe a
Nothing

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

data State =
    State
      {State -> [Object]
stack :: [Object],
       State -> Map Number Object
dict :: Map Number Object,
       State -> Set Thm
theorems :: Set Thm}
  deriving (State -> State -> Bool
(State -> State -> Bool) -> (State -> State -> Bool) -> Eq State
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: State -> State -> Bool
$c/= :: State -> State -> Bool
== :: State -> State -> Bool
$c== :: State -> State -> Bool
Eq,Eq State
Eq State
-> (State -> State -> Ordering)
-> (State -> State -> Bool)
-> (State -> State -> Bool)
-> (State -> State -> Bool)
-> (State -> State -> Bool)
-> (State -> State -> State)
-> (State -> State -> State)
-> Ord State
State -> State -> Bool
State -> State -> Ordering
State -> State -> State
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: State -> State -> State
$cmin :: State -> State -> State
max :: State -> State -> State
$cmax :: State -> State -> State
>= :: State -> State -> Bool
$c>= :: State -> State -> Bool
> :: State -> State -> Bool
$c> :: State -> State -> Bool
<= :: State -> State -> Bool
$c<= :: State -> State -> Bool
< :: State -> State -> Bool
$c< :: State -> State -> Bool
compare :: State -> State -> Ordering
$ccompare :: State -> State -> Ordering
$cp1Ord :: Eq State
Ord,Int -> State -> ShowS
[State] -> ShowS
State -> String
(Int -> State -> ShowS)
-> (State -> String) -> ([State] -> ShowS) -> Show State
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [State] -> ShowS
$cshowList :: [State] -> ShowS
show :: State -> String
$cshow :: State -> String
showsPrec :: Int -> State -> ShowS
$cshowsPrec :: Int -> State -> ShowS
Show)

pushState :: Objective a => a -> State -> State
pushState :: a -> State -> State
pushState a
a State
state = State
state {stack :: [Object]
stack = a -> [Object] -> [Object]
forall a. Objective a => a -> [Object] -> [Object]
pushObject a
a ([Object] -> [Object]) -> [Object] -> [Object]
forall a b. (a -> b) -> a -> b
$ State -> [Object]
stack State
state}

push2State :: (Objective a, Objective b) => a -> b -> State -> State
push2State :: a -> b -> State -> State
push2State a
a b
b State
state = State
state {stack :: [Object]
stack = a -> b -> [Object] -> [Object]
forall a b.
(Objective a, Objective b) =>
a -> b -> [Object] -> [Object]
push2Object a
a b
b ([Object] -> [Object]) -> [Object] -> [Object]
forall a b. (a -> b) -> a -> b
$ State -> [Object]
stack State
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
push5State a
a b
b c
c d
d e
e State
state =
    State
state {stack :: [Object]
stack = a -> b -> c -> d -> e -> [Object] -> [Object]
forall a b c d e.
(Objective a, Objective b, Objective c, Objective d,
 Objective e) =>
a -> b -> c -> d -> e -> [Object] -> [Object]
push5Object a
a b
b c
c d
d e
e ([Object] -> [Object]) -> [Object] -> [Object]
forall a b. (a -> b) -> a -> b
$ State -> [Object]
stack State
state}

popState :: Objective a => State -> Maybe (a,State)
popState :: State -> Maybe (a, State)
popState State
state = do
  (a
a,[Object]
s) <- [Object] -> Maybe (a, [Object])
forall a. Objective a => [Object] -> Maybe (a, [Object])
popObject ([Object] -> Maybe (a, [Object]))
-> [Object] -> Maybe (a, [Object])
forall a b. (a -> b) -> a -> b
$ State -> [Object]
stack State
state
  (a, State) -> Maybe (a, State)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, State
state {stack :: [Object]
stack = [Object]
s})

pop2State :: (Objective a, Objective b) => State -> Maybe (a,b,State)
pop2State :: State -> Maybe (a, b, State)
pop2State State
state = do
  (a
a,b
b,[Object]
s) <- [Object] -> Maybe (a, b, [Object])
forall a b.
(Objective a, Objective b) =>
[Object] -> Maybe (a, b, [Object])
pop2Object ([Object] -> Maybe (a, b, [Object]))
-> [Object] -> Maybe (a, b, [Object])
forall a b. (a -> b) -> a -> b
$ State -> [Object]
stack State
state
  (a, b, State) -> Maybe (a, b, State)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, b
b, State
state {stack :: [Object]
stack = [Object]
s})

pop3State :: (Objective a, Objective b, Objective c) =>
             State -> Maybe (a,b,c,State)
pop3State :: State -> Maybe (a, b, c, State)
pop3State State
state = do
  (a
a,b
b,c
c,[Object]
s) <- [Object] -> Maybe (a, b, c, [Object])
forall a b c.
(Objective a, Objective b, Objective c) =>
[Object] -> Maybe (a, b, c, [Object])
pop3Object ([Object] -> Maybe (a, b, c, [Object]))
-> [Object] -> Maybe (a, b, c, [Object])
forall a b. (a -> b) -> a -> b
$ State -> [Object]
stack State
state
  (a, b, c, State) -> Maybe (a, b, c, State)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, b
b, c
c, State
state {stack :: [Object]
stack = [Object]
s})

pop5State :: (Objective a, Objective b, Objective c, Objective d,
              Objective e) => State -> Maybe (a,b,c,d,e,State)
pop5State :: State -> Maybe (a, b, c, d, e, State)
pop5State State
state = do
  (a
a,b
b,c
c,d
d,e
e,[Object]
s) <- [Object] -> Maybe (a, b, c, d, e, [Object])
forall a b c d e.
(Objective a, Objective b, Objective c, Objective d,
 Objective e) =>
[Object] -> Maybe (a, b, c, d, e, [Object])
pop5Object ([Object] -> Maybe (a, b, c, d, e, [Object]))
-> [Object] -> Maybe (a, b, c, d, e, [Object])
forall a b. (a -> b) -> a -> b
$ State -> [Object]
stack State
state
  (a, b, c, d, e, State) -> Maybe (a, b, c, d, e, State)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, b
b, c
c, d
d, e
e, State
state {stack :: [Object]
stack = [Object]
s})

peekState :: Objective a => State -> Maybe a
peekState :: State -> Maybe a
peekState = ((a, State) -> a) -> Maybe (a, State) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, State) -> a
forall a b. (a, b) -> a
fst (Maybe (a, State) -> Maybe a)
-> (State -> Maybe (a, State)) -> State -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> Maybe (a, State)
forall a. Objective a => State -> Maybe (a, State)
popState

defState :: Number -> Object -> State -> State
defState :: Number -> Object -> State -> State
defState Number
k Object
x State
state = State
state {dict :: Map Number Object
dict = Number -> Object -> Map Number Object -> Map Number Object
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Number
k Object
x (Map Number Object -> Map Number Object)
-> Map Number Object -> Map Number Object
forall a b. (a -> b) -> a -> b
$ State -> Map Number Object
dict State
state}

refState :: Number -> State -> Maybe Object
refState :: Number -> State -> Maybe Object
refState Number
k State
state = Number -> Map Number Object -> Maybe Object
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Number
k (Map Number Object -> Maybe Object)
-> Map Number Object -> Maybe Object
forall a b. (a -> b) -> a -> b
$ State -> Map Number Object
dict State
state

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

thmState :: Thm -> State -> State
thmState :: Thm -> State -> State
thmState Thm
th State
state = State
state {theorems :: Set Thm
theorems = Thm -> Set Thm -> Set Thm
forall a. Ord a => a -> Set a -> Set a
Set.insert Thm
th (Set Thm -> Set Thm) -> Set Thm -> Set Thm
forall a b. (a -> b) -> a -> b
$ State -> Set Thm
theorems State
state}

initialState :: State
initialState :: State
initialState =
    State :: [Object] -> Map Number Object -> Set Thm -> State
State
      {stack :: [Object]
stack = [],
       dict :: Map Number Object
dict = Map Number Object
forall k a. Map k a
Map.empty,
       theorems :: Set Thm
theorems = Set Thm
forall a. Set a
Set.empty}

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

instance Printable State where
  toDoc :: State -> Doc
toDoc State
state =
      [Object] -> Doc
forall a. Printable a => [a] -> Doc
stackDoc (State -> [Object]
stack State
state) Doc -> Doc -> Doc
$+$
      Map Number Object -> Doc
forall k a. Map k a -> Doc
dictDoc (State -> Map Number Object
dict State
state) Doc -> Doc -> Doc
$+$
      Set Thm -> Doc
forall a. Set a -> Doc
theoremsDoc (State -> Set Thm
theorems State
state)
    where
      stackDoc :: [a] -> Doc
stackDoc [a]
s = String -> Doc
PP.text String
"stack =" Doc -> Doc -> Doc
<+> (Doc -> Doc
PP.brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> Doc
forall a. Printable a => Int -> [a] -> Doc
objsDoc Int
5 [a]
s)

      dictDoc :: Map k a -> Doc
dictDoc Map k a
d = String -> Doc
PP.text String
"dictionary =" Doc -> Doc -> Doc
<+> (Doc -> Doc
PP.braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc
PP.int (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ Map k a -> Int
forall k a. Map k a -> Int
Map.size Map k a
d)

      theoremsDoc :: Set a -> Doc
theoremsDoc Set a
e = String -> Doc
PP.text String
"theorems =" Doc -> Doc -> Doc
<+> (Doc -> Doc
PP.braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc
PP.int (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ Set a -> Int
forall a. Set a -> Int
Set.size Set a
e)

      objsDoc :: Int -> [a] -> Doc
objsDoc Int
k [a]
s =
          [Doc] -> Doc
PP.sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
PP.punctuate Doc
PP.comma [Doc]
ds
        where
          ds :: [Doc]
ds = if Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 then (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Printable a => a -> Doc
toDoc [a]
s
               else (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Printable a => a -> Doc
toDoc (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
k [a]
s) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
dx]
          dx :: Doc
dx = Doc
dots Doc -> Doc -> Doc
<> Int -> Doc
PP.int Int
x Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"more objects" Doc -> Doc -> Doc
<> Doc
dots
          dots :: Doc
dots = String -> Doc
PP.text String
"..."
          x :: Int
x = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k

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

type LineNumber = Integer

readArticle :: Theory -> Interpret -> FilePath -> IO (Set Thm)
readArticle :: Theory -> Interpret -> String -> IO (Set Thm)
readArticle Theory
thy Interpret
int String
art = do
    ByteString
bs <- String -> IO ByteString
ByteString.readFile String
art
    let txt :: Text
txt = ByteString -> Text
Text.Encoding.decodeUtf8 ByteString
bs
    let ls :: [(Integer, Text)]
ls = [Integer] -> [Text] -> [(Integer, Text)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
1..] ([Text] -> [(Integer, Text)]) -> [Text] -> [(Integer, Text)]
forall a b. (a -> b) -> a -> b
$ Text -> [Text]
Text.lines Text
txt
    let (Number
v,[(Integer, Command)]
cs) = [(Integer, Command)] -> (Number, [(Integer, Command)])
getVersion ([(Integer, Command)] -> (Number, [(Integer, Command)]))
-> [(Integer, Command)] -> (Number, [(Integer, Command)])
forall a b. (a -> b) -> a -> b
$ ((Integer, Text) -> (Integer, Command))
-> [(Integer, Text)] -> [(Integer, Command)]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Text) -> (Integer, Command)
parseCmd ([(Integer, Text)] -> [(Integer, Command)])
-> [(Integer, Text)] -> [(Integer, Command)]
forall a b. (a -> b) -> a -> b
$ ((Integer, Text) -> Bool) -> [(Integer, Text)] -> [(Integer, Text)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Integer, Text) -> Bool
notComment [(Integer, Text)]
ls
    let s :: State
s = (State -> (Integer, Command) -> State)
-> State -> [(Integer, Command)] -> State
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' State -> (Integer, Command) -> State
execute State
initialState ([(Integer, Command)] -> State) -> [(Integer, Command)] -> State
forall a b. (a -> b) -> a -> b
$ ((Integer, Command) -> (Integer, Command))
-> [(Integer, Command)] -> [(Integer, Command)]
forall a b. (a -> b) -> [a] -> [b]
map (Number -> (Integer, Command) -> (Integer, Command)
version Number
v) [(Integer, Command)]
cs
    Set Thm -> IO (Set Thm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Thm -> IO (Set Thm)) -> Set Thm -> IO (Set Thm)
forall a b. (a -> b) -> a -> b
$ State -> Set Thm
theorems State
s
  where
    notComment :: (LineNumber,Text) -> Bool
    notComment :: (Integer, Text) -> Bool
notComment (Integer
_,Text
t) = Text -> Bool
Text.null Text
t Bool -> Bool -> Bool
|| Text -> Char
Text.head Text
t Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'#'

    parseCmd :: (LineNumber,Text) -> (LineNumber,Command)
    parseCmd :: (Integer, Text) -> (Integer, Command)
parseCmd (Integer
l,Text
t) =
        case Text -> Maybe Command
forall a. Parsable a => Text -> Maybe a
fromText Text
t of
          Just Command
c -> (Integer
l,Command
c)
          Maybe Command
Nothing -> String -> (Integer, Command)
forall a. HasCallStack => String -> a
error (String -> (Integer, Command)) -> String -> (Integer, Command)
forall a b. (a -> b) -> a -> b
$ String -> Integer -> ShowS
err String
"unparseable command" Integer
l (Text -> String
forall a. Show a => a -> String
show Text
t)

    getVersion :: [(LineNumber,Command)] -> (Version,[(LineNumber,Command)])
    getVersion :: [(Integer, Command)] -> (Number, [(Integer, Command)])
getVersion ((Integer
l, NumberCommand Number
v) : (Integer
_,Command
VersionCommand) : [(Integer, Command)]
cs) =
        if Number
v Number -> Number -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Number
Number Integer
6 then (Number
v,[(Integer, Command)]
cs)
        else String -> (Number, [(Integer, Command)])
forall a. HasCallStack => String -> a
error (String -> (Number, [(Integer, Command)]))
-> String -> (Number, [(Integer, Command)])
forall a b. (a -> b) -> a -> b
$ String -> Integer -> ShowS
err String
"bad version number" Integer
l (Number -> String
forall a. Show a => a -> String
show Number
v)
    getVersion [(Integer, Command)]
cs = (Integer -> Number
Number Integer
5, [(Integer, Command)]
cs)

    version :: Version -> (LineNumber,Command) -> (LineNumber,Command)
    version :: Number -> (Integer, Command) -> (Integer, Command)
version Number
v (Integer
l,Command
c) =
        case Number -> Command -> Maybe Command
versionCommand Number
v Command
c of
          Just Command
c' -> (Integer
l,Command
c')
          Maybe Command
Nothing -> String -> (Integer, Command)
forall a. HasCallStack => String -> a
error (String -> (Integer, Command)) -> String -> (Integer, Command)
forall a b. (a -> b) -> a -> b
$ String -> Integer -> ShowS
err String
"unsupported command" Integer
l String
e
                     where e :: String
e = String
"command " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Command -> String
forall a. Printable a => a -> String
toString Command
c String -> ShowS
forall a. [a] -> [a] -> [a]
++
                               String
" not supported in version " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Number -> String
forall a. Show a => a -> String
show Number
v String -> ShowS
forall a. [a] -> [a] -> [a]
++
                               String
" article files"

    execute :: State -> (LineNumber,Command) -> State
    execute :: State -> (Integer, Command) -> State
execute State
s (Integer
l,Command
c) =
        case Theory -> Interpret -> State -> Command -> Maybe State
executeCommand Theory
thy Interpret
int State
s Command
c of
          Just State
s' -> State
s'
          Maybe State
Nothing -> String -> State
forall a. HasCallStack => String -> a
error (String -> State) -> String -> State
forall a b. (a -> b) -> a -> b
$ String -> Integer -> ShowS
err String
e Integer
l (State -> String
forall a. Printable a => a -> String
toString State
s)
                     where e :: String
e = String
"couldn't execute command " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Command -> String
forall a. Printable a => a -> String
toString Command
c

    err :: String -> LineNumber -> String -> String
    err :: String -> Integer -> ShowS
err String
e Integer
l String
s = String
art String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s