{- |
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 :: Named CMD -> String
ganame cmd :: Named CMD
cmd = "ga_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd

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

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

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

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

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

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