hets/CSL/Lemma_Export.hs

{- |
Module      :  ./CSL/Lemma_Export.hs
Description :  Generation of Lemmata for CMDs
Copyright   :  (c) Dominik Dietrich, DFKI Bremen, 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Dominik.Dietrich@dfki.de
Stability   :  provisional
Portability :  portable

Interface for Reduce CAS system.
-}

module CSL.Lemma_Export where

import Common.AS_Annotation
import CSL.AS_BASIC_CSL

-- | generate name for generated lemma out of name of theorem
ganame :: Named CMD -> String
ganame cmd = "ga_" ++ senAttr cmd

-- | generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult
genLemmaFactor :: Named CMD -> EXPRESSION -> Named CMD
genLemmaFactor namedcmd casresult = makeNamed lemmaname lemma
    where Cmd _ exps = sentence namedcmd
          lemma = Cmd "=" [head exps, casresult]
          lemmaname = ganame namedcmd

-- | generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult
genLemmaSolve :: Named CMD -> EXPRESSION -> Named CMD
genLemmaSolve namedcmd casresult = makeNamed lemmaname lemma
    where Cmd _ exps = sentence namedcmd
          lemma = Cmd "=" [head exps, casresult]
          lemmaname = ganame namedcmd

-- | generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult
genLemmaSimplify :: Named CMD -> EXPRESSION -> Named CMD
genLemmaSimplify namedcmd casresult = makeNamed lemmaname lemma
    where Cmd _ exps = sentence namedcmd
          lemma = Cmd "=" [head exps, casresult]
          lemmaname = ganame namedcmd

-- | generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult
genLemmaAsk :: Named CMD -> EXPRESSION -> Named CMD
genLemmaAsk namedcmd casresult = makeNamed lemmaname lemma
      where Cmd _ exps = sentence namedcmd
            lemma = Cmd "=" [head exps, casresult]
            lemmaname = ganame namedcmd

-- | generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult
genLemmaRemainder :: Named CMD -> EXPRESSION -> Named CMD
genLemmaRemainder namedcmd casresult = makeNamed lemmaname lemma
    where Cmd _ exps = sentence namedcmd
          lemma = Cmd "=" [head exps, casresult]
          lemmaname = ganame namedcmd

-- | generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult
genLemmaInt :: Named CMD -> EXPRESSION -> Named CMD
genLemmaInt namedcmd casresult = makeNamed lemmaname lemma
    where Cmd _ exps = sentence namedcmd
          lemma = Cmd "=" [head exps, casresult]
          lemmaname = ganame namedcmd