{-# LANGUAGE TemplateHaskell #-}
module Persistence.Schema.MappingType where

import Data.List (isPrefixOf)
import Database.Persist.TH

data MappingType = LocalDef | LocalThmOpen | LocalThmProved
                 | GlobalDef | GlobalThmOpen | GlobalThmProved
                 | HidingDef
                 | FreeDef | CofreeDef | NPFreeDef | MinimizeDef
                 | HidingOpen | HidingProved
                 | FreeOpen | CofreeOpen | NPFreeOpen | MinimizeOpen
                 | FreeProved | CofreeProved | NPFreeProved | MinimizeProved
                   deriving MappingType -> MappingType -> Bool
(MappingType -> MappingType -> Bool)
-> (MappingType -> MappingType -> Bool) -> Eq MappingType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MappingType -> MappingType -> Bool
$c/= :: MappingType -> MappingType -> Bool
== :: MappingType -> MappingType -> Bool
$c== :: MappingType -> MappingType -> Bool
Eq

instance Show MappingType where
  show :: MappingType -> String
show LocalDef = "local_def"
  show LocalThmOpen = "local_thm_open"
  show LocalThmProved = "local_thm_proved"
  show GlobalDef = "global_def"
  show GlobalThmOpen = "global_thm_open"
  show GlobalThmProved = "global_thm_proved"
  show HidingDef = "hiding_def"
  show FreeDef = "free_def"
  show CofreeDef = "cofree_def"
  show NPFreeDef = "np_free_def"
  show MinimizeDef = "minimize_def"
  show HidingOpen = "hiding_open"
  show HidingProved = "hiding_proved"
  show FreeOpen = "free_open"
  show CofreeOpen = "cofree_open"
  show NPFreeOpen = "np_free_open"
  show MinimizeOpen = "minimize_open"
  show FreeProved = "free_proved"
  show CofreeProved = "cofree_proved"
  show NPFreeProved = "np_free_proved"
  show MinimizeProved = "minimize_proved"

instance Read MappingType where
  readsPrec :: Int -> ReadS MappingType
readsPrec _ input :: String
input
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
LocalDef String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
LocalDef, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
LocalDef) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
LocalThmOpen String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
LocalThmOpen, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
LocalThmOpen) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
LocalThmProved String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
LocalThmProved, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
LocalThmProved) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
GlobalDef String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
GlobalDef, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
GlobalDef) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
GlobalThmOpen String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
GlobalThmOpen, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
GlobalThmOpen) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
GlobalThmProved String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
GlobalThmProved, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
GlobalThmProved) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
HidingDef String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
HidingDef, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
HidingDef) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
FreeDef String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
FreeDef, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
FreeDef) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
CofreeDef String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
CofreeDef, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
CofreeDef) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
NPFreeDef String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
NPFreeDef, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
NPFreeDef) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
MinimizeDef String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
MinimizeDef, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
MinimizeDef) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
HidingOpen String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
HidingOpen, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
HidingOpen) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
HidingProved String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
HidingProved, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
HidingProved) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
FreeOpen String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
FreeOpen, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
FreeOpen) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
CofreeOpen String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
CofreeOpen, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
CofreeOpen) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
NPFreeOpen String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
NPFreeOpen, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
NPFreeOpen) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
MinimizeOpen String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
MinimizeOpen, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
MinimizeOpen) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
FreeProved String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
FreeProved, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
FreeProved) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
CofreeProved String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
CofreeProved, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
CofreeProved) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
NPFreeProved String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
NPFreeProved, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
NPFreeProved) String
input)]
    | MappingType -> String
forall a. Show a => a -> String
show MappingType
MinimizeProved String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
input = [(MappingType
MinimizeProved, Int -> ShowS
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ MappingType -> String
forall a. Show a => a -> String
show MappingType
MinimizeProved) String
input)]
    | Bool
otherwise = []

derivePersistField "MappingType"