content: {-# 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 Show
  
  
  instance Language HolLight where
      description _ = "input language of the theorem prover Hol Light\n"
          ++ "for more information please refer to\n"
          ++ "http://www.cl.cam.ac.uk/~jrh13/hol-light/"
  
  instance GetRange Sentence
  
  instance Syntax HolLight () () () () where
      parse_basic_spec HolLight = Nothing {- Just basicSpec
      default implementation should be sufficient -}
  
  instance Sentences HolLight Sentence Sign HolLightMorphism () where
      map_sen HolLight _ = return
      -- other default implementations should be sufficient
  
  -- | Sublogics
  instance SemiLatticeWithTop HolLightSL where
      lub _ _ = Top
      top = Top
  
  instance MinSublogic HolLightSL () where
       minSublogic _ = Top
  
  instance MinSublogic HolLightSL Sign where
      minSublogic _ = Top
  
  instance SublogicName HolLightSL where
      sublogicName = show
  
  instance MinSublogic HolLightSL HolLightMorphism where
      minSublogic _ = Top
  
  instance MinSublogic HolLightSL Sentence where
      minSublogic _ = Top
  
  instance ProjectSublogic HolLightSL () where
      projectSublogic _ = id
  
  instance ProjectSublogic HolLightSL Sign where
      projectSublogic _ = id
  
  instance ProjectSublogic HolLightSL HolLightMorphism where
      projectSublogic _ = id
  
  instance ProjectSublogicM HolLightSL () where
      projectSublogicM _ = 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 = Experimental
        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 = emptySig
             is_subsig HolLight = isSubSig
             subsig_inclusion HolLight = defaultInclusion
             signature_union HolLight = sigUnion
  