content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./DFOL/AS_DFOL.hs
  Description :  Abstract syntax for first-order logic with dependent types (DFOL)
  Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  k.sojakova@jacobs-university.de
  Stability   :  experimental
  Portability :  portable
  -}
  
  module DFOL.AS_DFOL
    ( NAME
    , DECL
    , SDECL
    , BASIC_SPEC (..)
    , BASIC_ITEM (..)
    , TYPE (..)
    , TERM (..)
    , FORMULA (..)
    , SYMB
    , SYMB_ITEMS (..)
    , SYMB_MAP_ITEMS (..)
    , SYMB_OR_MAP (..)
    , termRecForm
    , termFlatForm
    , typeRecForm
    , typeFlatForm
    , formulaRecForm
    , formulaFlatForm
    , printNames
    , printDecls
    , getVarsFromDecls
    , getVarTypeFromDecls
    , compactDecls
    , expandDecls
    , Translatable (translate)
    , getNewName
    , getFreeVars
    ) where
  
  import Common.AS_Annotation
  import Common.Id
  import Common.Doc
  import Common.DocUtils
  
  import DFOL.Utils
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Data.Data
  import Data.List
  
  type NAME = Token
  type DECL = ([NAME], TYPE)
  type SDECL = (NAME, TYPE)
  
  -- grammar for basic specification
  data BASIC_SPEC = Basic_spec [Annoted BASIC_ITEM]
                    deriving (Show, Typeable)
  
  instance GetRange BASIC_SPEC
  
  data BASIC_ITEM = Decl_item DECL
                  | Axiom_item FORMULA
                    deriving (Show, Typeable)
  
  data TYPE = Sort
            | Form
            | Univ TERM
            | Func [TYPE] TYPE
            | Pi [DECL] TYPE
              deriving (Show, Ord, Typeable, Data)
  
  data TERM = Identifier NAME
            | Appl TERM [TERM]
              deriving (Show, Ord, Typeable, Data)
  
  data FORMULA = T
               | F
               | Pred TERM
               | Equality TERM TERM
               | Negation FORMULA
               | Conjunction [FORMULA]
               | Disjunction [FORMULA]
               | Implication FORMULA FORMULA
               | Equivalence FORMULA FORMULA
               | Forall [DECL] FORMULA
               | Exists [DECL] FORMULA
                 deriving (Show, Ord, Eq, Typeable, Data)
  
  instance GetRange FORMULA
  
  -- grammar for symbols and symbol maps
  type SYMB = NAME
  
  data SYMB_ITEMS = Symb_items [SYMB]
                    deriving (Show, Eq, Typeable, Data)
  
  data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP]
                        deriving (Show, Eq, Typeable, Data)
  
  data SYMB_OR_MAP = Symb SYMB
                   | Symb_map SYMB SYMB
                     deriving (Show, Eq, Typeable, Data)
  
  -- canonical forms
  
  {- converts a term into a form where a function is applied to
     exactly one argument -}
  termRecForm :: TERM -> TERM
  termRecForm (Identifier t) = Identifier t
  termRecForm (Appl f []) = termRecForm f
  termRecForm (Appl f as) =
    Appl (termRecForm $ Appl f $ init as) [termRecForm $ last as]
  
  {- converts a type into a form where each construct takes
     exactly one argument -}
  typeRecForm :: TYPE -> TYPE
  typeRecForm (Func [] a) = typeRecForm a
  typeRecForm (Func (t : ts) a) = Func [typeRecForm t] $ typeRecForm $ Func ts a
  typeRecForm (Pi [] t) = typeRecForm t
  typeRecForm (Pi (([], _) : ds) a) = typeRecForm $ Pi ds a
  typeRecForm (Pi ((n : ns, t) : ds) a) =
    Pi [([n], typeRecForm t)] $ typeRecForm $ Pi ((ns, t) : ds) a
  typeRecForm t = t
  
  {- converts a formula into a form where each quantifier takes
     exactly one argument -}
  formulaRecForm :: FORMULA -> FORMULA
  formulaRecForm (Negation f) = formulaRecForm f
  formulaRecForm (Conjunction fs) = Conjunction $ map formulaRecForm fs
  formulaRecForm (Disjunction fs) = Disjunction $ map formulaRecForm fs
  formulaRecForm (Implication f g) =
    Implication (formulaRecForm f) (formulaRecForm g)
  formulaRecForm (Equivalence f g) =
    Equivalence (formulaRecForm f) (formulaRecForm g)
  formulaRecForm (Forall [] f) = formulaRecForm f
  formulaRecForm (Forall (([], _) : ds) f) = formulaRecForm $ Forall ds f
  formulaRecForm (Forall ((n : ns, t) : ds) f) =
    Forall [([n], t)] $ formulaRecForm $ Forall ((ns, t) : ds) f
  formulaRecForm (Exists [] f) = formulaRecForm f
  formulaRecForm (Exists (([], _) : ds) f) = formulaRecForm $ Exists ds f
  formulaRecForm (Exists ((n : ns, t) : ds) f) =
    Exists [([n], t)] $ formulaRecForm $ Exists ((ns, t) : ds) f
  formulaRecForm t = t
  
  {- determines the flattened form of a term, i.e. the function symbol
     applied and the argument list -}
  termFlatForm :: TERM -> (NAME, [TERM])
  termFlatForm (Identifier x) = (x, [])
  termFlatForm (Appl f as) = (x, bs ++ as)
                            where (x, bs) = termFlatForm f
  
  {- converts a type into a flattened form where each operator binds maximum
     number of arguments -}
  typeFlatForm :: TYPE -> TYPE
  typeFlatForm (Func [] t) = typeFlatForm t
  typeFlatForm (Func ts t) =
    let ts1 = map typeFlatForm ts
        t1 = typeFlatForm t
        in case t1 of
           Func ts2 t2 -> Func (ts1 ++ ts2) t2
           _ -> Func ts1 t1
  typeFlatForm (Pi [] t) = typeFlatForm t
  typeFlatForm (Pi ds t) =
    let ds1 = map (\ (ns, t3) -> (ns, typeFlatForm t3)) ds
        t1 = typeFlatForm t
        in case t1 of
           Pi ds2 t2 -> Pi (compactDecls (ds1 ++ ds2)) t2
           _ -> Pi (compactDecls ds1) t1
  typeFlatForm t = t
  
  {- converts a formula into a flattened form where each quantifier binds maximum
     number of arguments -}
  formulaFlatForm :: FORMULA -> FORMULA
  formulaFlatForm (Negation f) = formulaFlatForm f
  formulaFlatForm (Conjunction []) = T
  formulaFlatForm (Conjunction fs) = Conjunction $ map formulaFlatForm fs
  formulaFlatForm (Disjunction []) = F
  formulaFlatForm (Disjunction fs) = Disjunction $ map formulaFlatForm fs
  formulaFlatForm (Implication f g) =
    Implication (formulaFlatForm f) (formulaFlatForm g)
  formulaFlatForm (Equivalence f g) =
    Equivalence (formulaFlatForm f) (formulaFlatForm g)
  formulaFlatForm (Forall [] f) = formulaFlatForm f
  formulaFlatForm (Forall ds1 f) =
    let f1 = formulaFlatForm f
        in case f1 of
           Forall ds2 f2 -> Forall (compactDecls (ds1 ++ ds2)) f2
           _ -> Forall (compactDecls ds1) f1
  formulaFlatForm (Exists [] f) = formulaFlatForm f
  formulaFlatForm (Exists ds1 f) =
    let f1 = formulaFlatForm f
        in case f1 of
           Exists ds2 f2 -> Exists (compactDecls (ds1 ++ ds2)) f2
           _ -> Exists (compactDecls ds1) f1
  formulaFlatForm t = t
  
  -- substitutions
  
  {- class of types containing identifiers which may be
     substituted by terms -}
  class Translatable a where
     {- substitutions and renamings: the first argument specifies the desired
        term/identifier substitutions and the second the set of identifiers which
        cannot be used as new variable names -}
     translate :: Map.Map NAME TERM -> Set.Set NAME -> a -> a
  
  instance Translatable TERM where
     translate m _ = translateTerm m . termRecForm
  instance Translatable TYPE where
     translate m s t = let s1 = Set.unions $ map getFreeVarsInTerm $ Map.elems m
                           in translateType m (Set.union s s1) (typeRecForm t)
  instance Translatable FORMULA where
     translate m s f = let s1 = Set.unions $ map getFreeVarsInTerm $ Map.elems m
                           in translateFormula m (Set.union s s1)
                                 (formulaRecForm f)
  
  translateTerm :: Map.Map NAME TERM -> TERM -> TERM
  translateTerm m (Identifier x) = Map.findWithDefault (Identifier x) x m
  translateTerm m (Appl f [a]) = Appl (translateTerm m f) [translateTerm m a]
  translateTerm _ t = t
  
  translateType :: Map.Map NAME TERM -> Set.Set NAME -> TYPE -> TYPE
  translateType _ _ Sort = Sort
  translateType _ _ Form = Form
  translateType m s (Univ t) = Univ $ translate m s t
  translateType m s (Func ts t) = Func (map (translate m s) ts) (translate m s t)
  translateType m s (Pi [([x], t)] a) =
    let t1 = translate m s t
        x1 = getNewName x s
        a1 = translate (Map.insert x (Identifier x1) m) (Set.insert x1 s) a
        in Pi [([x1], t1)] a1
  translateType _ _ t = t
  
  translateFormula :: Map.Map NAME TERM -> Set.Set NAME -> FORMULA -> FORMULA
  translateFormula _ _ T = T
  translateFormula _ _ F = F
  translateFormula m s (Pred t) = Pred $ translate m s t
  translateFormula m s (Equality t1 t2) =
    Equality (translate m s t1) (translate m s t2)
  translateFormula m s (Negation f) = Negation $ translate m s f
  translateFormula m s (Conjunction fs) =
    Conjunction $ map (translate m s) fs
  translateFormula m s (Disjunction fs) =
    Disjunction $ map (translate m s) fs
  translateFormula m s (Implication f g) =
    Implication (translate m s f) (translate m s g)
  translateFormula m s (Equivalence f g) =
    Equivalence (translate m s f) (translate m s g)
  translateFormula m s (Forall [([x], t)] f) =
    let t1 = translate m s t
        x1 = getNewName x s
        f1 = translate (Map.insert x (Identifier x1) m) (Set.insert x1 s) f
        in Forall [([x1], t1)] f1
  translateFormula m s (Exists [([x], t)] f) =
    let t1 = translate m s t
        x1 = getNewName x s
        f1 = translate (Map.insert x (Identifier x1) m) (Set.insert x1 s) f
        in Exists [([x1], t1)] f1
  translateFormula _ _ f = f
  
  {- modifies the given name until it is different from each of the names
     in the input set -}
  getNewName :: NAME -> Set.Set NAME -> NAME
  getNewName var names = getNewNameH var names (tokStr var) 0
  
  getNewNameH :: NAME -> Set.Set NAME -> String -> Int -> Token
  getNewNameH var names root i =
    if Set.notMember var names
       then var
       else let newVar = Token (root ++ show i) nullRange
                in getNewNameH newVar names root $ i + 1
  
  -- equality (should be defined via Ord!)
  instance Eq TERM where
      u == v = eqTerm (termRecForm u) (termRecForm v)
  instance Eq TYPE where
      u == v = eqType (typeRecForm u) (typeRecForm v)
  
  eqTerm :: TERM -> TERM -> Bool
  eqTerm (Identifier x1) (Identifier x2) = x1 == x2
  eqTerm (Appl f1 [a1]) (Appl f2 [a2]) = f1 == f2 && a1 == a2
  eqTerm _ _ = False
  
  eqType :: TYPE -> TYPE -> Bool
  eqType Sort Sort = True
  eqType Form Form = True
  eqType (Univ t1) (Univ t2) = t1 == t2
  eqType (Func [t1] s1) (Func [t2] s2) = t1 == t2 && s1 == s2
  eqType (Pi [([n1], t1)] s1) (Pi [([n2], t2)] s2) =
    let syms1 = Set.delete n1 $ getFreeVars s1
        syms2 = Set.delete n2 $ getFreeVars s2
        v = getNewName n1 $ Set.union syms1 syms2
        type1 = translate (Map.singleton n1 (Identifier v)) syms1 s1
        type2 = translate (Map.singleton n2 (Identifier v)) syms2 s2
        in t1 == t2 && type1 == type2
  eqType _ _ = False
  
  -- returns a set of unbound identifiers used within a type
  getFreeVars :: TYPE -> Set.Set NAME
  getFreeVars e = getFreeVarsH $ typeRecForm e
  
  getFreeVarsH :: TYPE -> Set.Set NAME
  getFreeVarsH Sort = Set.empty
  getFreeVarsH Form = Set.empty
  getFreeVarsH (Univ t) = getFreeVarsInTerm t
  getFreeVarsH (Func [t] v) =
    Set.union (getFreeVarsH t) (getFreeVarsH v)
  getFreeVarsH (Pi [([n], t)] a) =
    Set.delete n $ Set.union (getFreeVarsH t) (getFreeVarsH a)
  getFreeVarsH _ = Set.empty
  
  getFreeVarsInTerm :: TERM -> Set.Set NAME
  getFreeVarsInTerm t = getFreeVarsInTermH $ termRecForm t
  
  getFreeVarsInTermH :: TERM -> Set.Set NAME
  getFreeVarsInTermH (Identifier x) = Set.singleton x
  getFreeVarsInTermH (Appl f [a]) =
    Set.union (getFreeVarsInTermH f) (getFreeVarsInTermH a)
  getFreeVarsInTermH _ = Set.empty
  
  -- precedences - needed for pretty printing
  formulaPrec :: FORMULA -> Int
  formulaPrec T = truePrec
  formulaPrec F = falsePrec
  formulaPrec Pred {} = predPrec
  formulaPrec Equality {} = equalPrec
  formulaPrec Negation {} = negPrec
  formulaPrec Disjunction {} = disjPrec
  formulaPrec Conjunction {} = conjPrec
  formulaPrec Implication {} = implPrec
  formulaPrec Equivalence {} = equivPrec
  formulaPrec Forall {} = forallPrec
  formulaPrec Exists {} = existsPrec
  
  typePrec :: TYPE -> Int
  typePrec Sort = sortPrec
  typePrec Form = formPrec
  typePrec Univ {} = univPrec
  typePrec Func {} = funcPrec
  typePrec Pi {} = piPrec
  
  -- pretty printing
  instance Pretty BASIC_SPEC where
      pretty = printBasicSpec
  instance Pretty BASIC_ITEM where
      pretty = printBasicItem
  instance Pretty TYPE where
      pretty = printType . typeFlatForm
  instance Pretty TERM where
      pretty = printTerm
  instance Pretty FORMULA where
      pretty = printFormula . formulaFlatForm
  instance Pretty SYMB_ITEMS where
      pretty = printSymbItems
  instance Pretty SYMB_MAP_ITEMS where
      pretty = printSymbMapItems
  instance Pretty SYMB_OR_MAP where
      pretty = printSymbOrMap
  
  printBasicSpec :: BASIC_SPEC -> Doc
  printBasicSpec (Basic_spec xs) = vcat $ map pretty xs
  
  printBasicItem :: BASIC_ITEM -> Doc
  printBasicItem (Decl_item (ns, t)) = printNames ns <+> text "::" <+> pretty t
  printBasicItem (Axiom_item f) = dot <> pretty f
  
  printType :: TYPE -> Doc
  printType (Sort) = text "Sort"
  printType (Form) = text "Form"
  printType (Univ t) = pretty t
  printType (Func ts t) =
    fsep $ prepPunctuate (text "-> ")
      $ map (printTypeWithPrec funcPrec) (ts ++ [t])
  printType (Pi xs x) = text "Pi" <+> printDecls xs <+> printType x
  
  printTypeWithPrec :: Int -> TYPE -> Doc
  printTypeWithPrec prec t = if typePrec t >= prec
                                then parens $ printType t
                                else printType t
  
  printTerm :: TERM -> Doc
  printTerm t = if null as
                   then pretty x
                   else pretty x <> parens (ppWithCommas as)
                where (x, as) = termFlatForm t
  
  printFormula :: FORMULA -> Doc
  printFormula (T) = text "true"
  printFormula (F) = text "false"
  printFormula (Pred x) = pretty x
  printFormula (Equality x y) = pretty x <+> text "==" <+> pretty y
  printFormula (Negation f) = notDoc <+> printFormulaWithPrec negPrec f
  printFormula (Conjunction xs) = fsep $ prepPunctuate (andDoc <> space)
    $ map (printFormulaWithPrec conjPrec) xs
  printFormula (Disjunction xs) = fsep $ prepPunctuate (orDoc <> space)
    $ map (printFormulaWithPrec disjPrec) xs
  printFormula (Implication x y) =
    printFormulaWithPrec (implPrec - 1) x
    <+> implies
    <+> printFormulaWithPrec (implPrec - 1) y
  printFormula (Equivalence x y) =
    printFormulaWithPrec (equivPrec - 1) x
    <+> equiv
    <+> printFormulaWithPrec (equivPrec - 1) y
  printFormula (Forall xs f) = forallDoc <+> printDecls xs <+> printFormula f
  printFormula (Exists xs f) = exists <+> printDecls xs <+> printFormula f
  
  printFormulaWithPrec :: Int -> FORMULA -> Doc
  printFormulaWithPrec prec f = if formulaPrec f > prec
                                   then parens $ printFormula f
                                   else printFormula f
  
  printSymbItems :: SYMB_ITEMS -> Doc
  printSymbItems (Symb_items xs) = ppWithCommas xs
  
  printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
  printSymbMapItems (Symb_map_items xs) = ppWithCommas xs
  
  printSymbOrMap :: SYMB_OR_MAP -> Doc
  printSymbOrMap (Symb s) = pretty s
  printSymbOrMap (Symb_map s t) = pretty s <+> mapsto <+> pretty t
  
  printNames :: [NAME] -> Doc
  printNames = ppWithCommas
  
  printDecl :: DECL -> Doc
  printDecl (ns, t) = printNames ns <+> colon <+> pretty t
  
  printDecls :: [DECL] -> Doc
  printDecls xs = fsep (punctuate semi $ map printDecl xs) <> dot
  
  -- operations on a list of declarations
  getVarsFromDecls :: [DECL] -> [NAME]
  getVarsFromDecls = concatMap fst
  
  getVarTypeFromDecls :: NAME -> [DECL] -> Maybe TYPE
  getVarTypeFromDecls n ds = case result of
                                  Just (_, t) -> Just t
                                  Nothing -> Nothing
                             where result = find (\ (ns, _) -> elem n ns) ds
  
  compactDecls :: [DECL] -> [DECL]
  compactDecls [] = []
  compactDecls [d] = [d]
  compactDecls (d1 : d2 : ds) =
    let (ns1, t1) = d1
        (ns2, t2) = d2
        in if t1 == t2
              then compactDecls $ (ns1 ++ ns2, t1) : ds
              else d1 : compactDecls (d2 : ds)
  
  expandDecls :: [DECL] -> [SDECL]
  expandDecls = concatMap (\ (ns, t) -> map (\ n -> (n, t)) ns)
  