{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./HolLight/Logic_HolLight.hs
Description :  Instance of class Logic for HolLight

Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for HolLight logic
   Also the instances for Syntax and Category.

  Ref.

  <http://www.cl.cam.ac.uk/~jrh13/hol-light/>

-}

module HolLight.Logic_HolLight where

import Logic.Logic

import HolLight.Sign
import HolLight.Sublogic
import HolLight.Sentence (Sentence)
import HolLight.ATC_HolLight ()

import Common.DefaultMorphism
import Common.Id

type HolLightMorphism = DefaultMorphism Sign

-- | Lid for HolLight logic
data HolLight = HolLight deriving Int -> HolLight -> ShowS
[HolLight] -> ShowS
HolLight -> String
(Int -> HolLight -> ShowS)
-> (HolLight -> String) -> ([HolLight] -> ShowS) -> Show HolLight
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HolLight] -> ShowS
$cshowList :: [HolLight] -> ShowS
show :: HolLight -> String
$cshow :: HolLight -> String
showsPrec :: Int -> HolLight -> ShowS
$cshowsPrec :: Int -> HolLight -> ShowS
Show


instance Language HolLight where
    description :: HolLight -> String
description _ = "input language of the theorem prover Hol Light\n"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "for more information please refer to\n"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "http://www.cl.cam.ac.uk/~jrh13/hol-light/"

instance GetRange Sentence

instance Syntax HolLight () () () () where
    parse_basic_spec :: HolLight -> Maybe (PrefixMap -> AParser st ())
parse_basic_spec HolLight = Maybe (PrefixMap -> AParser st ())
forall a. Maybe a
Nothing {- Just basicSpec
    default implementation should be sufficient -}

instance Sentences HolLight Sentence Sign HolLightMorphism () where
    map_sen :: HolLight -> HolLightMorphism -> Sentence -> Result Sentence
map_sen HolLight _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return
    -- other default implementations should be sufficient

-- | Sublogics
instance SemiLatticeWithTop HolLightSL where
    lub :: HolLightSL -> HolLightSL -> HolLightSL
lub _ _ = HolLightSL
Top
    top :: HolLightSL
top = HolLightSL
Top

instance MinSublogic HolLightSL () where
     minSublogic :: () -> HolLightSL
minSublogic _ = HolLightSL
Top

instance MinSublogic HolLightSL Sign where
    minSublogic :: Sign -> HolLightSL
minSublogic _ = HolLightSL
Top

instance SublogicName HolLightSL where
    sublogicName :: HolLightSL -> String
sublogicName = HolLightSL -> String
forall a. Show a => a -> String
show

instance MinSublogic HolLightSL HolLightMorphism where
    minSublogic :: HolLightMorphism -> HolLightSL
minSublogic _ = HolLightSL
Top

instance MinSublogic HolLightSL Sentence where
    minSublogic :: Sentence -> HolLightSL
minSublogic _ = HolLightSL
Top

instance ProjectSublogic HolLightSL () where
    projectSublogic :: HolLightSL -> () -> ()
projectSublogic _ = () -> ()
forall a. a -> a
id

instance ProjectSublogic HolLightSL Sign where
    projectSublogic :: HolLightSL -> Sign -> Sign
projectSublogic _ = Sign -> Sign
forall a. a -> a
id

instance ProjectSublogic HolLightSL HolLightMorphism where
    projectSublogic :: HolLightSL -> HolLightMorphism -> HolLightMorphism
projectSublogic _ = HolLightMorphism -> HolLightMorphism
forall a. a -> a
id

instance ProjectSublogicM HolLightSL () where
    projectSublogicM :: HolLightSL -> () -> Maybe ()
projectSublogicM _ = () -> Maybe ()
forall a. a -> Maybe a
Just

-- | Instance of Logic for propositional logc
instance Logic HolLight
    HolLightSL                -- sublogic
    ()                        -- basic_spec
    Sentence                  -- sentence
    ()                        -- symb_items
    ()                        -- symb_map_items
    Sign                      -- sign
    HolLightMorphism          -- morphism
    ()                        -- symbol
    ()                        -- raw_symbol
    ()                        -- proof_tree
    where
      stability :: HolLight -> Stability
stability HolLight = Stability
Experimental
      empty_proof_tree :: HolLight -> ()
empty_proof_tree _ = ()

-- | Static Analysis for propositional logic
instance StaticAnalysis HolLight
    ()                      -- basic_spec
    Sentence                 -- sentence
    ()                       -- symb_items
    ()                       -- symb_map_items
    Sign                     -- sign
    HolLightMorphism         -- morphism
    ()                       -- symbol
    ()                       -- raw_symbol
        where
           -- basic_analysis HolLight = Just basicHolAnalysis
           empty_signature :: HolLight -> Sign
empty_signature HolLight = Sign
emptySig
           is_subsig :: HolLight -> Sign -> Sign -> Bool
is_subsig HolLight = Sign -> Sign -> Bool
isSubSig
           subsig_inclusion :: HolLight -> Sign -> Sign -> Result HolLightMorphism
subsig_inclusion HolLight = Sign -> Sign -> Result HolLightMorphism
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion
           signature_union :: HolLight -> Sign -> Sign -> Result Sign
signature_union HolLight = Sign -> Sign -> Result Sign
sigUnion