{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  ATC/Prover.der.hs
Description :  generated ShATermConvertible, Json instances
Copyright   :  (c) DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(derive Typeable instances)

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json
  for the type(s):
'Logic.Prover.ThmStatus'
'Logic.Prover.Theory'
'Logic.Prover.TacticScript'
'Logic.Prover.Reason'
'Logic.Prover.GoalStatus'
'Logic.Prover.ProofStatus'
'Logic.Prover.ProverKind'
'Logic.Prover.FreeDefMorphism'
'Logic.Prover.TheoryMorphism'
'Logic.Prover.CCStatus'
-}

{-
Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
  dependency files:
Logic/Prover.hs
-}

module ATC.Prover () where

import ATC.AS_Annotation
import ATC.OrderedMap
import ATerm.Lib
import Common.AS_Annotation as AS_Anno
import Common.Doc
import Common.DocUtils
import Common.Json.Instances
import Common.ProofUtils
import Common.ProverTools
import Common.Result
import Control.Monad
import Data.Aeson(ToJSON, FromJSON)
import Data.List
import Data.Maybe (isJust)
import Data.Time (TimeOfDay, midnight)
import Data.Typeable
import GHC.Generics(Generic)
import Logic.Prover
import qualified Common.OrderedMap as OMap
import qualified Control.Concurrent as Concurrent
import qualified Data.Map as Map
import qualified Data.Set as Set

{-! for Logic.Prover.ThmStatus derive : ShATermConvertible !-}
{-! for Logic.Prover.Theory derive : ShATermConvertible !-}
{-! for Logic.Prover.TacticScript derive : ShATermConvertible !-}
{-! for Logic.Prover.Reason derive : ShATermConvertible !-}
{-! for Logic.Prover.GoalStatus derive : ShATermConvertible !-}
{-! for Logic.Prover.ProofStatus derive : ShATermConvertible !-}
{-! for Logic.Prover.ProverKind derive : ShATermConvertible !-}
{-! for Logic.Prover.FreeDefMorphism derive : ShATermConvertible !-}
{-! for Logic.Prover.TheoryMorphism derive : ShATermConvertible !-}
{-! for Logic.Prover.CCStatus derive : ShATermConvertible !-}

{-! for Logic.Prover.ThmStatus derive : Json !-}
{-! for Logic.Prover.Theory derive : Json !-}
{-! for Logic.Prover.TacticScript derive : Json !-}
{-! for Logic.Prover.Reason derive : Json !-}
{-! for Logic.Prover.GoalStatus derive : Json !-}
{-! for Logic.Prover.ProofStatus derive : Json !-}
{-! for Logic.Prover.ProverKind derive : Json !-}
{-! for Logic.Prover.FreeDefMorphism derive : Json !-}
{-! for Logic.Prover.TheoryMorphism derive : Json !-}
{-! for Logic.Prover.CCStatus derive : Json !-}

-- Generated by DrIFT, look but don't touch!

instance ShATermConvertible a => ShATermConvertible (Logic.Prover.ThmStatus a) where
  toShATermAux :: ATermTable -> ThmStatus a -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ThmStatus a
xv = case ThmStatus a
xv of
    ThmStatus a :: [a]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [a] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [a]
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ThmStatus" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, ThmStatus a)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ThmStatus" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [a])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [a]
a') ->
      (ATermTable
att1, [a] -> ThmStatus a
forall a. [a] -> ThmStatus a
ThmStatus [a]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ThmStatus a)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.ThmStatus" ShATerm
u

instance (ShATermConvertible sign, ShATermConvertible sen,
          ShATermConvertible proof_tree) => ShATermConvertible (Logic.Prover.Theory sign sen proof_tree) where
  toShATermAux :: ATermTable -> Theory sign sen proof_tree -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Theory sign sen proof_tree
xv = case Theory sign sen proof_tree
xv of
    Theory a :: sign
a b :: ThSens sen (ProofStatus proof_tree)
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 sign
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable
-> ThSens sen (ProofStatus proof_tree) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 ThSens sen (ProofStatus proof_tree)
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Theory" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Theory sign sen proof_tree)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Theory" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, sign)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: sign
a') ->
      case Int
-> ATermTable -> (ATermTable, ThSens sen (ProofStatus proof_tree))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: ThSens sen (ProofStatus proof_tree)
b') ->
      (ATermTable
att2, sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory sign
a' ThSens sen (ProofStatus proof_tree)
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Theory sign sen proof_tree)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.Theory" ShATerm
u

instance ShATermConvertible Logic.Prover.TacticScript where
  toShATermAux :: ATermTable -> TacticScript -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TacticScript
xv = case TacticScript
xv of
    TacticScript a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TacticScript" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TacticScript)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TacticScript" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> TacticScript
TacticScript String
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TacticScript)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.TacticScript" ShATerm
u

instance ShATermConvertible Logic.Prover.Reason where
  toShATermAux :: ATermTable -> Reason -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Reason
xv = case Reason
xv of
    Reason a :: [String]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [String]
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Reason" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Reason)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Reason" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [String]
a') ->
      (ATermTable
att1, [String] -> Reason
Reason [String]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Reason)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.Reason" ShATerm
u

instance ShATermConvertible Logic.Prover.GoalStatus where
  toShATermAux :: ATermTable -> GoalStatus -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: GoalStatus
xv = case GoalStatus
xv of
    Open a :: Reason
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Reason -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Reason
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Open" [Int
a'] []) ATermTable
att1
    Disproved -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Disproved" [] []) ATermTable
att0
    Proved a :: Bool
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Bool
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Proved" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, GoalStatus)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Open" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Reason)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Reason
a') ->
      (ATermTable
att1, Reason -> GoalStatus
Open Reason
a') }
    ShAAppl "Disproved" [] _ -> (ATermTable
att0, GoalStatus
Disproved)
    ShAAppl "Proved" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      (ATermTable
att1, Bool -> GoalStatus
Proved Bool
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GoalStatus)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.GoalStatus" ShATerm
u

instance ShATermConvertible proof_tree => ShATermConvertible (Logic.Prover.ProofStatus proof_tree) where
  toShATermAux :: ATermTable -> ProofStatus proof_tree -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ProofStatus proof_tree
xv = case ProofStatus proof_tree
xv of
    ProofStatus a :: String
a b :: GoalStatus
b c :: [String]
c d :: String
d e :: proof_tree
e f :: TimeOfDay
f g :: TacticScript
g h :: [String]
h -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> GoalStatus -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 GoalStatus
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [String]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 String
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> proof_tree -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 proof_tree
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> TimeOfDay -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 TimeOfDay
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> TacticScript -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 TacticScript
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att7 [String]
h
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ProofStatus" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f',
                                                Int
g', Int
h'] []) ATermTable
att8
  fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofStatus proof_tree)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ProofStatus" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g, h :: Int
h] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, GoalStatus)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: GoalStatus
b') ->
      case Int -> ATermTable -> (ATermTable, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [String]
c') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: String
d') ->
      case Int -> ATermTable -> (ATermTable, proof_tree)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: proof_tree
e') ->
      case Int -> ATermTable -> (ATermTable, TimeOfDay)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: TimeOfDay
f') ->
      case Int -> ATermTable -> (ATermTable, TacticScript)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: TacticScript
g') ->
      case Int -> ATermTable -> (ATermTable, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: [String]
h') ->
      (ATermTable
att8, String
-> GoalStatus
-> [String]
-> String
-> proof_tree
-> TimeOfDay
-> TacticScript
-> [String]
-> ProofStatus proof_tree
forall proof_tree.
String
-> GoalStatus
-> [String]
-> String
-> proof_tree
-> TimeOfDay
-> TacticScript
-> [String]
-> ProofStatus proof_tree
ProofStatus String
a' GoalStatus
b' [String]
c' String
d' proof_tree
e' TimeOfDay
f' TacticScript
g' [String]
h') }}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ProofStatus proof_tree)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.ProofStatus" ShATerm
u

instance ShATermConvertible Logic.Prover.ProverKind where
  toShATermAux :: ATermTable -> ProverKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ProverKind
xv = case ProverKind
xv of
    ProveGUI -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ProveGUI" [] []) ATermTable
att0
    ProveCMDLautomatic ->
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ProveCMDLautomatic" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, ProverKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ProveGUI" [] _ -> (ATermTable
att0, ProverKind
ProveGUI)
    ShAAppl "ProveCMDLautomatic" [] _ -> (ATermTable
att0, ProverKind
ProveCMDLautomatic)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ProverKind)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.ProverKind" ShATerm
u

instance (ShATermConvertible sentence,
          ShATermConvertible morphism) => ShATermConvertible (Logic.Prover.FreeDefMorphism sentence morphism) where
  toShATermAux :: ATermTable
-> FreeDefMorphism sentence morphism -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FreeDefMorphism sentence morphism
xv = case FreeDefMorphism sentence morphism
xv of
    FreeDefMorphism a :: morphism
a b :: morphism
b c :: [Named sentence]
c d :: Bool
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> morphism -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 morphism
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> morphism -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 morphism
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Named sentence] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Named sentence]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Bool
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FreeDefMorphism" [Int
a', Int
b', Int
c',
                                                    Int
d'] []) ATermTable
att4
  fromShATermAux :: Int
-> ATermTable -> (ATermTable, FreeDefMorphism sentence morphism)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "FreeDefMorphism" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, morphism)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: morphism
a') ->
      case Int -> ATermTable -> (ATermTable, morphism)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: morphism
b') ->
      case Int -> ATermTable -> (ATermTable, [Named sentence])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [Named sentence]
c') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Bool
d') ->
      (ATermTable
att4, morphism
-> morphism
-> [Named sentence]
-> Bool
-> FreeDefMorphism sentence morphism
forall sentence morphism.
morphism
-> morphism
-> [Named sentence]
-> Bool
-> FreeDefMorphism sentence morphism
FreeDefMorphism morphism
a' morphism
b' [Named sentence]
c' Bool
d') }}}}
    u :: ShATerm
u -> String
-> ShATerm -> (ATermTable, FreeDefMorphism sentence morphism)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.FreeDefMorphism" ShATerm
u

instance (ShATermConvertible sign, ShATermConvertible sen,
          ShATermConvertible mor,
          ShATermConvertible proof_tree) => ShATermConvertible (Logic.Prover.TheoryMorphism sign sen mor proof_tree) where
  toShATermAux :: ATermTable
-> TheoryMorphism sign sen mor proof_tree -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TheoryMorphism sign sen mor proof_tree
xv = case TheoryMorphism sign sen mor proof_tree
xv of
    TheoryMorphism a :: Theory sign sen proof_tree
a b :: Theory sign sen proof_tree
b c :: mor
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Theory sign sen proof_tree -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Theory sign sen proof_tree
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Theory sign sen proof_tree -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Theory sign sen proof_tree
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> mor -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 mor
c
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TheoryMorphism" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int
-> ATermTable
-> (ATermTable, TheoryMorphism sign sen mor proof_tree)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TheoryMorphism" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Theory sign sen proof_tree)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Theory sign sen proof_tree
a') ->
      case Int -> ATermTable -> (ATermTable, Theory sign sen proof_tree)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Theory sign sen proof_tree
b') ->
      case Int -> ATermTable -> (ATermTable, mor)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: mor
c') ->
      (ATermTable
att3, Theory sign sen proof_tree
-> Theory sign sen proof_tree
-> mor
-> TheoryMorphism sign sen mor proof_tree
forall sign sen mor proof_tree.
Theory sign sen proof_tree
-> Theory sign sen proof_tree
-> mor
-> TheoryMorphism sign sen mor proof_tree
TheoryMorphism Theory sign sen proof_tree
a' Theory sign sen proof_tree
b' mor
c') }}}
    u :: ShATerm
u -> String
-> ShATerm -> (ATermTable, TheoryMorphism sign sen mor proof_tree)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.TheoryMorphism" ShATerm
u

instance ShATermConvertible proof_tree => ShATermConvertible (Logic.Prover.CCStatus proof_tree) where
  toShATermAux :: ATermTable -> CCStatus proof_tree -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CCStatus proof_tree
xv = case CCStatus proof_tree
xv of
    CCStatus a :: proof_tree
a b :: TimeOfDay
b c :: Maybe Bool
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> proof_tree -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 proof_tree
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TimeOfDay -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TimeOfDay
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe Bool
c
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CCStatus" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, CCStatus proof_tree)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "CCStatus" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, proof_tree)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: proof_tree
a') ->
      case Int -> ATermTable -> (ATermTable, TimeOfDay)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TimeOfDay
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe Bool
c') ->
      (ATermTable
att3, proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
CCStatus proof_tree
a' TimeOfDay
b' Maybe Bool
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CCStatus proof_tree)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.CCStatus" ShATerm
u

deriving instance GHC.Generics.Generic (Logic.Prover.ThmStatus a)
instance Data.Aeson.ToJSON a => Data.Aeson.ToJSON (Logic.Prover.ThmStatus a) where
instance Data.Aeson.FromJSON a => Data.Aeson.FromJSON (Logic.Prover.ThmStatus a) where

deriving instance GHC.Generics.Generic (Logic.Prover.Theory sign sen proof_tree)
instance (Data.Aeson.ToJSON sign, Data.Aeson.ToJSON sen,
          Data.Aeson.ToJSON proof_tree) => Data.Aeson.ToJSON (Logic.Prover.Theory sign sen proof_tree) where
instance (Data.Aeson.FromJSON sign, Data.Aeson.FromJSON sen,
          Data.Aeson.FromJSON proof_tree) => Data.Aeson.FromJSON (Logic.Prover.Theory sign sen proof_tree) where

deriving instance GHC.Generics.Generic Logic.Prover.TacticScript
instance Data.Aeson.ToJSON Logic.Prover.TacticScript where
instance Data.Aeson.FromJSON Logic.Prover.TacticScript where

deriving instance GHC.Generics.Generic Logic.Prover.Reason
instance Data.Aeson.ToJSON Logic.Prover.Reason where
instance Data.Aeson.FromJSON Logic.Prover.Reason where

deriving instance GHC.Generics.Generic Logic.Prover.GoalStatus
instance Data.Aeson.ToJSON Logic.Prover.GoalStatus where
instance Data.Aeson.FromJSON Logic.Prover.GoalStatus where

deriving instance GHC.Generics.Generic (Logic.Prover.ProofStatus proof_tree)
instance Data.Aeson.ToJSON proof_tree => Data.Aeson.ToJSON (Logic.Prover.ProofStatus proof_tree) where
instance Data.Aeson.FromJSON proof_tree => Data.Aeson.FromJSON (Logic.Prover.ProofStatus proof_tree) where

deriving instance GHC.Generics.Generic Logic.Prover.ProverKind
instance Data.Aeson.ToJSON Logic.Prover.ProverKind where
instance Data.Aeson.FromJSON Logic.Prover.ProverKind where

deriving instance GHC.Generics.Generic (Logic.Prover.FreeDefMorphism sentence morphism)
instance (Data.Aeson.ToJSON sentence,
          Data.Aeson.ToJSON morphism) => Data.Aeson.ToJSON (Logic.Prover.FreeDefMorphism sentence morphism) where
instance (Data.Aeson.FromJSON sentence,
          Data.Aeson.FromJSON morphism) => Data.Aeson.FromJSON (Logic.Prover.FreeDefMorphism sentence morphism) where

deriving instance GHC.Generics.Generic (Logic.Prover.TheoryMorphism sign sen mor proof_tree)
instance (Data.Aeson.ToJSON sign, Data.Aeson.ToJSON sen,
          Data.Aeson.ToJSON mor,
          Data.Aeson.ToJSON proof_tree) => Data.Aeson.ToJSON (Logic.Prover.TheoryMorphism sign sen mor proof_tree) where
instance (Data.Aeson.FromJSON sign, Data.Aeson.FromJSON sen,
          Data.Aeson.FromJSON mor,
          Data.Aeson.FromJSON proof_tree) => Data.Aeson.FromJSON (Logic.Prover.TheoryMorphism sign sen mor proof_tree) where

deriving instance GHC.Generics.Generic (Logic.Prover.CCStatus proof_tree)
instance Data.Aeson.ToJSON proof_tree => Data.Aeson.ToJSON (Logic.Prover.CCStatus proof_tree) where
instance Data.Aeson.FromJSON proof_tree => Data.Aeson.FromJSON (Logic.Prover.CCStatus proof_tree) where