{- |
Module      :  ./Common/ProofUtils.hs
Description:   functions useful for all prover connections in Hets
Copyright   :  (c) Klaus Luettich, C. Maeder, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Functions useful for all prover connections in Hets

Some were moved from Isabelle.Translate and some others from
Isabelle.IsaProve.
-}

module Common.ProofUtils where

import Data.Char
import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.AS_Annotation
import Common.Utils (number)

{-
 * generic names are added

 * disambiguation of duplicate assigned names

is done by toThSens

 * translation of special characters with the aid of the provided function

is done by prepareSenNames

Warning: all sentence names are disambiguated by adding a natural number.
If that does not work for a certain reasoner you can hand in a function
which uses a different alghorithm.
-}

-- | translate special characters in sentence names
prepareSenNames :: (String -> String) -> [Named a] -> [Named a]
prepareSenNames :: (String -> String) -> [Named a] -> [Named a]
prepareSenNames = (Named a -> Named a) -> [Named a] -> [Named a]
forall a b. (a -> b) -> [a] -> [b]
map ((Named a -> Named a) -> [Named a] -> [Named a])
-> ((String -> String) -> Named a -> Named a)
-> (String -> String)
-> [Named a]
-> [Named a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> Named a -> Named a
forall a b s. (a -> b) -> SenAttr s a -> SenAttr s b
reName

-- | disambiguate sentence names
disambiguateSens :: Set.Set String -> [Named a] -> [Named a]
disambiguateSens :: Set String -> [Named a] -> [Named a]
disambiguateSens =
    Int
-> (Named a -> String)
-> (String -> Named a -> Named a)
-> Set String
-> [Named a]
-> [Named a]
forall a.
Int
-> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a]
genericDisambigSens 0 Named a -> String
forall s a. SenAttr s a -> a
senAttr ((String -> Named a -> Named a)
 -> Set String -> [Named a] -> [Named a])
-> (String -> Named a -> Named a)
-> Set String
-> [Named a]
-> [Named a]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> Named a -> Named a
forall a b s. (a -> b) -> SenAttr s a -> SenAttr s b
reName ((String -> String) -> Named a -> Named a)
-> (String -> String -> String) -> String -> Named a -> Named a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall a b. a -> b -> a
const

-- | generically disambiguate lists with names
genericDisambigSens :: Int -> (a -> String) -> (String -> a -> a)
                    -> Set.Set String -> [a] -> [a]
genericDisambigSens :: Int
-> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a]
genericDisambigSens _ _ _ _ [] = []
genericDisambigSens c :: Int
c sel :: a -> String
sel upd :: String -> a -> a
upd nameSet :: Set String
nameSet (ax :: a
ax : rest :: [a]
rest) =
  let name :: String
name = a -> String
sel a
ax in case String -> Set String -> (Set String, Bool, Set String)
forall a. Ord a => a -> Set a -> (Set a, Bool, Set a)
Set.splitMember String
name Set String
nameSet of
  (_, False, _) ->
      a
ax a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int
-> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a]
forall a.
Int
-> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a]
genericDisambigSens Int
c a -> String
sel String -> a -> a
upd (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
name Set String
nameSet) [a]
rest
  (_, _, greater :: Set String
greater) -> let
      n :: Int
n = (Int -> Bool) -> (Int -> Int) -> Int -> Int
forall a. (a -> Bool) -> (a -> a) -> a -> a
until (Bool -> Bool
not (Bool -> Bool) -> (Int -> Bool) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Set String -> Bool) -> Set String -> String -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set String
greater (String -> Bool) -> (Int -> String) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ('_' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show)
              (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
      name' :: String
name' = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n
      in String -> a -> a
upd String
name' a
ax a -> [a] -> [a]
forall a. a -> [a] -> [a]
:
         Int
-> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a]
forall a.
Int
-> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a]
genericDisambigSens Int
n a -> String
sel String -> a -> a
upd (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
name' Set String
nameSet) [a]
rest

nameAndDisambiguate :: [Named a] -> [Named a]
nameAndDisambiguate :: [Named a] -> [Named a]
nameAndDisambiguate = Set String -> [Named a] -> [Named a]
forall a. Set String -> [Named a] -> [Named a]
disambiguateSens Set String
forall a. Set a
Set.empty ([Named a] -> [Named a])
-> ([Named a] -> [Named a]) -> [Named a] -> [Named a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named a] -> [Named a]
forall a. [Named a] -> [Named a]
nameSens

-- | name unlabeled axioms with "Axnnn"
nameSens :: [Named a] -> [Named a]
nameSens :: [Named a] -> [Named a]
nameSens =
  ((Named a, Int) -> Named a) -> [(Named a, Int)] -> [Named a]
forall a b. (a -> b) -> [a] -> [b]
map (\ (sen :: Named a
sen, no :: Int
no) ->
       if Named a -> String
forall s a. SenAttr s a -> a
senAttr Named a
sen String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then (String -> String) -> Named a -> Named a
forall a b s. (a -> b) -> SenAttr s a -> SenAttr s b
reName (String -> String -> String
forall a b. a -> b -> a
const (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ "Ax" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
no) Named a
sen else Named a
sen)
    ([(Named a, Int)] -> [Named a])
-> ([Named a] -> [(Named a, Int)]) -> [Named a] -> [Named a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named a] -> [(Named a, Int)]
forall a. [a] -> [(a, Int)]
number

-- | collect the mapping of new to old names
collectNameMapping :: [Named a] -> [Named a] -> Map.Map String String
collectNameMapping :: [Named a] -> [Named a] -> Map String String
collectNameMapping ns :: [Named a]
ns os :: [Named a]
os = if (Named a -> Bool) -> [Named a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> (Named a -> String) -> Named a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named a -> String
forall s a. SenAttr s a -> a
senAttr) [Named a]
os
  then String -> Map String String
forall a. HasCallStack => String -> a
error "Common.ProofUtils.collectNameMapping"
  else [(String, String)] -> Map String String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, String)] -> Map String String)
-> [(String, String)] -> Map String String
forall a b. (a -> b) -> a -> b
$ (Named a -> Named a -> (String, String))
-> [Named a] -> [Named a] -> [(String, String)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ n :: Named a
n o :: Named a
o -> (Named a -> String
forall s a. SenAttr s a -> a
senAttr Named a
n, Named a -> String
forall s a. SenAttr s a -> a
senAttr Named a
o)) [Named a]
ns [Named a]
os

lookupCharMap :: Char -> String
lookupCharMap :: Char -> String
lookupCharMap c :: Char
c = String -> Char -> Map Char String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ("Slash_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Char -> Int
ord Char
c)) Char
c Map Char String
charMap

-- | a separate Map speeds up lookup
charMap :: Map.Map Char String
charMap :: Map Char String
charMap = [(Char, String)] -> Map Char String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
 [(' ' , "Space"),
  ('\n', "Newline"),
  ('\t', "Tab"),
  ('!' , "Exclam"),
  ('"' , "Quot"),
  ('#' , "Hash"),
  ('$' , "Dollar"),
  ('%' , "Percent"),
  ('&' , "Amp"),
  ('\'', "Prime"), -- Apostrophe?
  ('(' , "OBr"),
  (')' , "CBr"),
  ('*' , "x"),
  ('+' , "Plus"),
  (',' , "Comma"),
  ('-' , "Minus"),
  ('.' , "Period"), -- Dot?
  ('/' , "Slash"), -- Div?
  (':' , "Colon"),
  (';' , "Semi"),
  ('<' , "Lt"),
  ('=' , "Eq"),
  ('>' , "Gt"),
  ('?' , "Quest"),
  ('@' , "At"),
  ('[' , "OSqBr"),
  ('\\' , "Bslash"),
  (']' , "CSqBr"),
  ('^' , "Caret"), -- Hat?
  ('`' , "Grave"),
  ('{' , "LBrace"),
  ('|' , "VBar"),
  ('}' , "RBrace"),
  ('~' , "Tilde"),
  ('\160', "nbsp"),
  ('\161', "iexcl"),
  ('\162', "cent"),
  ('\163', "pound"),
  ('\164', "curren"),
  ('\165', "yen"),
  ('\166', "brvbar"),
  ('\167', "sect"),
  ('\168', "uml"),
  ('\169', "copy"),
  ('\170', "ordf"),
  ('\171', "laquo"),
  ('\172', "not"),
  ('\173', "shy"),
  ('\174', "reg"),
  ('\175', "macr"),
  ('\176', "deg"),
  ('\177', "plusmn"),
  ('\178', "sup2"),
  ('\179', "sup3"),
  ('\180', "acute"),
  ('\181', "micro"),
  ('\182', "para"),
  ('\183', "middot"),
  ('\184', "cedil"),
  ('\185', "sup1"),
  ('\186', "ordm"),
  ('\187', "raquo"),
  ('\188', "quarter"),
  ('\189', "half"),
  ('\190', "frac34"),
  ('\191', "iquest"),
  ('\192', "Agrave"),
  ('\193', "Aacute"),
  ('\194', "Acirc"),
  ('\195', "Atilde"),
  ('\196', "Auml"),
  ('\197', "Aring"),
  ('\198', "AElig"),
  ('\199', "Ccedil"),
  ('\200', "Egrave"),
  ('\201', "Eacute"),
  ('\202', "Ecirc"),
  ('\203', "Euml"),
  ('\204', "Igrave"),
  ('\205', "Iacute"),
  ('\206', "Icirc"),
  ('\207', "Iuml"),
  ('\208', "ETH"),
  ('\209', "Ntilde"),
  ('\210', "Ograve"),
  ('\211', "Oacute"),
  ('\212', "Ocirc"),
  ('\213', "Otilde"),
  ('\214', "Ouml"),
  ('\215', "Times"),
  ('\216', "OSlash"),
  ('\217', "Ugrave"),
  ('\218', "Uacute"),
  ('\219', "Ucirc"),
  ('\220', "Uuml"),
  ('\221', "Yacute"),
  ('\222', "THORN"),
  ('\223', "szlig"),
  ('\224', "agrave"),
  ('\225', "aacute"),
  ('\226', "acirc"),
  ('\227', "atilde"),
  ('\228', "auml"),
  ('\229', "aring"),
  ('\230', "aelig"),
  ('\231', "ccedil"),
  ('\232', "egrave"),
  ('\233', "eacute"),
  ('\234', "ecirc"),
  ('\235', "euml"),
  ('\236', "igrave"),
  ('\237', "iacute"),
  ('\238', "icirc"),
  ('\239', "iuml"),
  ('\240', "eth"),
  ('\241', "ntilde"),
  ('\242', "ograve"),
  ('\243', "oacute"),
  ('\244', "ocirc"),
  ('\245', "otilde"),
  ('\246', "ouml"),
  ('\247', "Divide"),
  ('\248', "oslash"),
  ('\249', "ugrave"),
  ('\250', "uacute"),
  ('\251', "ucirc"),
  ('\252', "uuml"),
  ('\253', "yacute"),
  ('\254', "thorn"),
  ('\255', "yuml")]