{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Isabelle/Logic_Isabelle.hs
Description :  Isabelle instance of class Logic
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic)

Instance of class Logic for Isabelle (including Pure, HOL etc.).
-}

module Isabelle.Logic_Isabelle where

import Common.DefaultMorphism
import Common.Id

import Logic.Logic

import Isabelle.ATC_Isabelle ()
import Isabelle.IsaSign
import Isabelle.IsaPrint
import Isabelle.IsaProve

type IsabelleMorphism = DefaultMorphism Sign

{- a dummy datatype for the LogicGraph and for identifying the right
instances -}
data Isabelle = Isabelle deriving Int -> Isabelle -> ShowS
[Isabelle] -> ShowS
Isabelle -> String
(Int -> Isabelle -> ShowS)
-> (Isabelle -> String) -> ([Isabelle] -> ShowS) -> Show Isabelle
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Isabelle] -> ShowS
$cshowList :: [Isabelle] -> ShowS
show :: Isabelle -> String
$cshow :: Isabelle -> String
showsPrec :: Int -> Isabelle -> ShowS
$cshowsPrec :: Int -> Isabelle -> ShowS
Show

instance Language Isabelle where
 description :: Isabelle -> String
description _ =
  "logic of the generic theorem prover Isabelle\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "This logic corresponds to the logic of Isabelle,\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "a weak intuitionistic type theory\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "Also, the logics encoded in Isabelle, like FOL, HOL, HOLCF, ZF " String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "are made available\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "See http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"

instance Logic.Logic.Syntax Isabelle () () () ()
    -- default implementation is fine!

instance GetRange Sentence

instance Sentences Isabelle Sentence Sign IsabelleMorphism () where
      map_sen :: Isabelle -> IsabelleMorphism -> Sentence -> Result Sentence
map_sen Isabelle _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return
      print_named :: Isabelle -> Named Sentence -> Doc
print_named Isabelle = Named Sentence -> Doc
printNamedSen
    -- other default implementations are fine

instance StaticAnalysis Isabelle () Sentence
               () ()
               Sign
               IsabelleMorphism () () where
         empty_signature :: Isabelle -> Sign
empty_signature Isabelle = Sign
emptySign
         is_subsig :: Isabelle -> Sign -> Sign -> Bool
is_subsig Isabelle = Sign -> Sign -> Bool
isSubSign
         subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism
subsig_inclusion Isabelle = Sign -> Sign -> Result IsabelleMorphism
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion

instance Logic Isabelle () () Sentence () ()
               Sign
               IsabelleMorphism () () () where
         stability :: Isabelle -> Stability
stability _ = Stability
Testing
    -- again default implementations are fine
         empty_proof_tree :: Isabelle -> ()
empty_proof_tree _ = ()
         provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()]
provers Isabelle =
           [IsaEditor -> Prover Sign Sentence IsabelleMorphism () ()
isabelleProver IsaEditor
Emacs, IsaEditor -> Prover Sign Sentence IsabelleMorphism () ()
isabelleProver IsaEditor
JEdit, Prover Sign Sentence IsabelleMorphism () ()
isabelleBatchProver]
         cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()]
cons_checkers Isabelle = [ConsChecker Sign Sentence () IsabelleMorphism ()
isabelleConsChecker]

instance LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism
  () () ()