lambdabot-4.1: scripts/FT/FTbase.hs
-- Copyright 2006, Sascha Boehme.
-- Main module of the application.
module Main (main) where
import FreeTheorems
import PredefinedTypes
import Control.Monad
import Data.List
import System.Environment
import System.Console.GetOpt
import System.IO
import Text.ParserCombinators.Parsec (ParseError)
computeResult' :: String -> String
computeResult' t =
let model = FixModel
omitIns = True
in
case parseTypeString t of
Left error -> "There was an error in the type: "++show error
Right nt ->
let (th, td) = generateTheorem model nt
(th2, td2) = foldl instantiateRelation (th, td)
(extractRelationVariables th)
tm2 = if omitIns then omitInstantiations th2 else th2
ls2 = extractLiftRelations (th2, td2) omitIns
in (printAsText tm2)
++ (concatMap (\l -> "\n\n"++(printAsText l)) ls2)
main = putStr . computeResult' =<< getLine
-- Entry point for the application.
-- The function parses the command line arguments. Then, it starts the
-- computation with the given values.
{-
main :: IO ()
main = do
arguments <- getArgs
case getOpt Permute options arguments of
(opts, _, []) -> let (info, os) = checkOpt opts
in if info
then putStrLn showInfo
else case os of
Left errors -> showErrors errors
Right (t,m,o) -> putStrLn
$ computeResult t m o
(_, _, errors) -> showErrors errors
where
showErrors errors = do
mapM (\s -> hPutStr stderr ("Error: " ++ s)) errors
hPutStr stderr (usageInfo "Usage: ftbase [OPTIONS]" options)
showInfo =
xmlTag "info" [] (concat
[ concatMap (\(n,i) -> xmlData n i) getSupportedAlgebraicDatatypes
, concatMap (\(n,i) -> xmlType n i) getSupportedTypeSynonyms
, concatMap (\(n,t) -> xmlPred n t) predefinedTypes
])
where
xmlData n i = xmlEmptyTag "data" [("name", n), ("arity", show i)]
xmlType n i = xmlEmptyTag "type" [("name", n), ("arity", show i)]
xmlPred n t = xmlTag "predefined" [("name", n)] t
-}
--------------------------------------------------------------------------------
--
-- Parsing of command line arguments.
--
-- Abstract description of command line options.
data Flag = Type String
| Model LanguageModel
| Info
| OmitInstantiations
deriving (Eq, Show)
-- The command line options.
options :: [OptDescr Flag]
options =
[ Option ['t'] ["type"]
(ReqArg Type "TYPE")
"the type from which to generate a theorem"
, Option ['b'] ["basic-model"]
(NoArg (Model BasicModel))
"use the basic model"
, Option ['f'] ["fix-model"]
(NoArg (Model FixModel))
"use the fix model"
, Option ['o'] ["omit-instantiations"]
(NoArg OmitInstantiations)
"omit instantiations in the generated theorem"
, Option ['i'] ["info"]
(NoArg Info)
"show available constructors and predefined types"
]
-- Checks if the detected command line options are correct, i.e. if flags of
-- each kind are occurring only once. If so, the corresponding values are
-- returned.
checkOpt :: [Flag] -> (Bool, Either [String] (LanguageModel, String, Bool))
checkOpt flags =
let om = foldr (checkModel) (Left "missing model\n") flags
ot = case foldr (checkType) (Left "missing type\n") flags of
Left e -> Left e
Right t -> if length (words t) > 0
then Right t
else Left "missing type\n"
oi = any (\f -> f == Info) flags
oo = any (\f -> f == OmitInstantiations) flags
extractError = either (\e -> [e]) (\_ -> [])
errors = extractError om ++ extractError ot
in case (om,ot) of
(Right m, Right t) -> (oi, Right (m, t, oo))
otherwise -> (oi, Left errors)
where
checkModel (Model m) (Left _) = Right m
checkModel (Model _) (Right _) = Left "only one model can be given\n"
checkModel _ x = x
checkType (Type t) (Left _) = Right t
checkType (Type _) (Right _) = Left "only one type can be given\n"
checkType _ x = x
--------------------------------------------------------------------------------
--
-- Computation of output
--
-- Parses the given string and creates either an error message or valid output.
computeResult :: LanguageModel -> String -> Bool -> String
computeResult model t omitIns =
case parseTypeString t of
Left error -> xmlTag "error" [("type", t)] (xmlClean (show error))
Right nt ->
let (th, td) = generateTheorem model nt
tm = if omitIns then omitInstantiations th else th
ls = extractLiftRelations (th, td) omitIns
(th2, td2) = foldl instantiateRelation (th, td)
(extractRelationVariables th)
tm2 = if omitIns then omitInstantiations th2 else th2
ls2 = extractLiftRelations (th2, td2) omitIns
in xmlTag "model" [] (show model)
++ xmlTag "type" [] (xmlClean (printAsText nt))
++ xmlTag "fundamental" [] (concat
[ xmlTag "theorem" [] (xmlClean (printAsText tm))
, concatMap (\l -> xmlTag "lift" [] (xmlClean (printAsText l))) ls
])
++ xmlTag "reduced" [] (concat
[ xmlTag "theorem" [] (xmlClean (printAsText tm2))
, concatMap (\l -> xmlTag "lift" [] (xmlClean (printAsText l))) ls2
])
-- Parses a type string and returns the named type obtained from parsing or an
-- error if no type was found. The function works as follows:
--
-- * If the input contains "::", then it is parsed as a named type.
--
-- * If the input is only one word, the function tries to find a type with
-- that name in the list of predefined types. If it can be found, that type
-- is parsed as a named type.
--
-- * Otherwise the input is parsed as a type without name, while a new name is
-- generated.
parseTypeString :: String -> Either ParseError NamedType
parseTypeString string =
let wlist = words string
in if (containsTwoColons string)
then parseNamedType string
else let (w:ws) = wlist
in if (ws == [])
then case lookup w predefinedTypes of
Nothing -> parseType acceptName string
Just t -> parseNamedType (w ++ " :: " ++ t)
else parseType acceptName string
where
containsTwoColons str =
case str of
':' : ':' : cs -> True
_ : c : cs -> containsTwoColons (c:cs)
otherwise -> False
acceptName name =
let (predefinedNames, _) = unzip predefinedTypes
in name `notElem` predefinedNames
--------------------------------------------------------------------------------
--
-- XML functions
--
-- Creates an XML tag.
xmlTag :: String -> [(String, String)] -> String -> String
xmlTag n as c =
"<" ++ n
++ foldl (\s (k,v) -> s ++ " " ++ k ++ "=\"" ++ xmlClean v ++ "\"") "" as
++ ">" ++ c ++ "</" ++ n ++ ">"
-- Creates an empty XML tag.
xmlEmptyTag :: String -> [(String, String)] -> String
xmlEmptyTag n as =
"<" ++ n
++ foldl (\s (k,v) -> s ++ " " ++ k ++ "=\"" ++ xmlClean v ++ "\"") "" as
++ "/>"
-- Replaces XML special characters.
xmlClean :: String -> String
xmlClean = concatMap replaceSymbol
where
replaceSymbol '&' = "&"
replaceSymbol '>' = ">"
replaceSymbol '<' = "<"
replaceSymbol c = [c]