hets/HasCASL/As.hs

{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./HasCASL/As.hs
Description :  abstract syntax for HasCASL
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

abstract syntax for HasCASL,
   more liberal than Concrete-Syntax.txt,
   annotations are almost as for CASL
-}

module HasCASL.As where

import Common.Id
import Common.Keywords
import Common.AS_Annotation

import Data.Data
import qualified Data.Set as Set

import Common.Doc
import Common.DocUtils

-- * abstract syntax entities with small utility functions

-- | annotated basic items
data BasicSpec = BasicSpec [Annoted BasicItem] deriving (Show, Typeable, Data)

-- | the possible items
data BasicItem =
    SigItems SigItems
  | ProgItems [Annoted ProgEq] Range
  -- pos "program", dots
  | ClassItems Instance [Annoted ClassItem] Range
  -- pos "class", ";"s
  | GenVarItems [GenVarDecl] Range
  -- pos "var", ";"s
  | FreeDatatype [Annoted DatatypeDecl] Range
  -- pos "free", "type", ";"s
  | GenItems [Annoted SigItems] Range
  {- pos "generated" "{", ";"s, "}"
  or "generated" "type" ";"s -}
  | AxiomItems [GenVarDecl] [Annoted Term] Range
  -- pos "forall" (if GenVarDecl not empty), dots
  | Internal [Annoted BasicItem] Range
    -- pos "internal" "{", ";"s, "}"
    deriving (Show, Typeable, Data)

-- | signature items are types or functions
data SigItems =
    TypeItems Instance [Annoted TypeItem] Range {- including sort
    pos "type", ";"s -}
  | OpItems OpBrand [Annoted OpItem] Range
    -- pos "op", ";"s
    deriving (Show, Typeable, Data)

-- | indicator for predicate, operation or function
data OpBrand = Pred | Op | Fun deriving (Eq, Ord, Typeable, Data)

-- | test if the function was declared as predicate
isPred :: OpBrand -> Bool
isPred b = case b of
    Pred -> True
    _ -> False

instance Show OpBrand where
    show b = case b of
        Pred -> predS
        Op -> opS
        Fun -> functS

-- | indicator in 'ClassItems' and 'TypeItems'
data Instance = Instance | Plain deriving (Eq, Ord, Typeable, Data)

instance Show Instance where
    show i = case i of
        Instance -> instanceS
        Plain -> ""

-- | a class item
data ClassItem = ClassItem ClassDecl [Annoted BasicItem] Range
  deriving (Show, Typeable, Data)
                 -- pos "{", ";"s "}"

-- | declaring class identifiers
data ClassDecl = ClassDecl [Id] Kind Range deriving (Show, Typeable, Data)
               -- pos ","s

-- | co- or contra- variance indicator
data Variance = InVar | CoVar | ContraVar | NonVar
  deriving (Eq, Ord, Typeable, Data)

instance Show Variance where
    show v = case v of
        InVar -> plusS ++ minusS
        CoVar -> plusS
        ContraVar -> minusS
        NonVar -> ""

-- | (higher) kinds
data AnyKind a =
    ClassKind a
  | FunKind Variance (AnyKind a) (AnyKind a) Range
    -- pos "+" or "-"
    deriving (Show, Typeable, Data)

instance Ord a => Eq (AnyKind a) where
   k1 == k2 = compare k1 k2 == EQ

instance Ord a => Ord (AnyKind a) where
   compare k1 k2 = case (k1, k2) of
       (ClassKind c1, ClassKind c2) -> compare c1 c2
       (ClassKind _, _) -> LT
       (FunKind v1 k3 k4 _, FunKind v2 k5 k6 _) ->
           compare (v1, k3, k4) (v2, k5, k6)
       _ -> GT

type Kind = AnyKind Id
type RawKind = AnyKind ()

-- | the possible type items
data TypeItem =
    TypeDecl [TypePattern] Kind Range
    -- pos ","s
  | SubtypeDecl [TypePattern] Type Range
  -- pos ","s, "<"
  | IsoDecl [TypePattern] Range
  -- pos "="s
  | SubtypeDefn TypePattern Vars Type (Annoted Term) Range
  -- pos "=", "{", ":", dot, "}"
  | AliasType TypePattern (Maybe Kind) TypeScheme Range
  -- pos ":="
  | Datatype DatatypeDecl
    deriving (Show, Typeable, Data)

-- | a tuple pattern for 'SubtypeDefn'
data Vars = Var Id | VarTuple [Vars] Range
  deriving (Show, Eq, Ord, Typeable, Data)

-- | the lhs of most type items
data TypePattern =
    TypePattern Id [TypeArg] Range
    -- pos "("s, ")"s
  | TypePatternToken Token
  | MixfixTypePattern [TypePattern]
  | BracketTypePattern BracketKind [TypePattern] Range
  -- pos brackets (no parenthesis)
  | TypePatternArg TypeArg Range
    -- pos "(", ")"
    deriving (Show, Typeable, Data)

-- | types based on variable or constructor names and applications
data Type =
    TypeName Id RawKind Int
    -- Int == 0 means constructor, negative are bound variables
  | TypeAppl Type Type
  | ExpandedType Type Type    {- an alias type with its expansion
  only the following variants are parsed -}
  | TypeAbs TypeArg Type Range
  | KindedType Type (Set.Set Kind) Range
  -- pos ":"
  | TypeToken Token
  | BracketType BracketKind [Type] Range
  -- pos "," (between type arguments)
  | MixfixType [Type]
    deriving (Show, Typeable, Data)

-- | change the type within a scheme
mapTypeOfScheme :: (Type -> Type) -> TypeScheme -> TypeScheme
mapTypeOfScheme f (TypeScheme args t ps) = TypeScheme args (f t) ps

{- | a type with bound type variables. The bound variables within the
scheme should have negative numbers in the order given by the type
argument list. The type arguments store proper kinds (including
downsets) whereas the kind within the type names are only raw
kinds. -}
data TypeScheme = TypeScheme [TypeArg] Type Range
  deriving (Show, Eq, Ord, Typeable, Data)
    {- pos "forall", ";"s,  dot (singleton list)
    pos "\" "("s, ")"s, dot for type aliases -}

-- | indicator for partial or total functions
data Partiality = Partial | Total deriving (Eq, Ord, Typeable, Data)

instance Show Partiality where
    show p = case p of
        Partial -> quMark
        Total -> exMark

-- | function declarations or definitions
data OpItem =
    OpDecl [PolyId] TypeScheme [OpAttr] Range
    -- pos ","s, ":", ","s, "assoc", "comm", "idem", "unit"
  | OpDefn PolyId [[VarDecl]] TypeScheme Term Range
    -- pos "("s, ";"s, ")"s, ":" and "="
    deriving (Show, Typeable, Data)

-- | attributes without arguments for binary functions
data BinOpAttr = Assoc | Comm | Idem deriving (Eq, Ord, Typeable, Data)

instance Show BinOpAttr where
    show a = case a of
        Assoc -> assocS
        Comm -> commS
        Idem -> idemS

-- | possible function attributes (including a term as a unit element)
data OpAttr =
    BinOpAttr BinOpAttr Range
  | UnitOpAttr Term Range deriving (Show, Typeable, Data)

instance Eq OpAttr where
    o1 == o2 = compare o1 o2 == EQ

instance Ord OpAttr where
    compare o1 o2 = case (o1, o2) of
        (BinOpAttr b1 _, BinOpAttr b2 _) -> compare b1 b2
        (BinOpAttr _ _, _) -> LT
        (UnitOpAttr t1 _, UnitOpAttr t2 _) -> compare t1 t2
        _ -> GT

-- | a polymorphic data type declaration with a deriving clause
data DatatypeDecl =
    DatatypeDecl TypePattern Kind [Annoted Alternative] [Id] Range
    -- pos "::=", "|"s, "deriving"
    deriving (Show, Typeable, Data)

{- | Alternatives are subtypes or a constructor with a list of
(curried) tuples as arguments. Only the components of the first tuple
can be addressed by the places of the mixfix constructor. -}
data Alternative =
    Constructor Id [[Component]] Partiality Range
    -- pos: "("s, ";"s, ")"s, "?"
  | Subtype [Type] Range
    -- pos: "type", ","s
    deriving (Show, Typeable, Data)

{- | A component is a type with on optional (only pre- or postfix)
   selector function. -}
data Component =
    Selector Id Partiality Type SeparatorKind Range
    -- pos ",", ":" or ":?"
  | NoSelector Type
    deriving (Show, Eq, Ord, Typeable, Data)

-- | the possible quantifiers
data Quantifier = Universal | Existential | Unique
  deriving (Show, Eq, Ord, Typeable, Data)

-- | the possibly type annotations of terms
data TypeQual = OfType | AsType | InType | Inferred
  deriving (Show, Eq, Ord, Typeable, Data)

-- | an indicator of (otherwise equivalent) let or where equations
data LetBrand = Let | Where | Program deriving (Show, Eq, Ord, Typeable, Data)

-- | the possible kinds of brackets (that should match when parsed)
data BracketKind = Parens | Squares | Braces | NoBrackets
  deriving (Show, Eq, Ord, Typeable, Data)

-- | the brackets as strings for printing
getBrackets :: BracketKind -> (String, String)
getBrackets b = case b of
    Parens -> ("(", ")")
    Squares -> ("[", "]")
    Braces -> ("{", "}")
    NoBrackets -> ("", "") -- for printing only

data InstKind = UserGiven | Infer deriving (Show, Eq, Ord, Typeable, Data)

{- | The possible terms and patterns. Formulas are also kept as
terms. Local variables and constants are kept separatetly. The variant
'ResolvedMixTerm' is an intermediate representation for type checking
only. -}
data Term =
    QualVar VarDecl
    -- pos "(", "var", ":", ")"
  | QualOp OpBrand PolyId TypeScheme [Type] InstKind Range
  -- pos "(", "op", ":", ")"
  | ApplTerm Term Term Range  {- analysed
  pos? -}
  | TupleTerm [Term] Range    {- special application
  pos "(", ","s, ")" -}
  | TypedTerm Term TypeQual Type Range
  -- pos ":", "as" or "in"
  | AsPattern VarDecl Term Range
  {- pos "@"
  patterns are terms constructed by the first six variants -}
  | QuantifiedTerm Quantifier [GenVarDecl] Term Range
  {- pos quantifier, ";"s, dot
  only "forall" may have a TypeVarDecl -}
  | LambdaTerm [Term] Partiality Term Range
  -- pos "\", dot (plus "!")
  | CaseTerm Term [ProgEq] Range
  -- pos "case", "of", "|"s
  | LetTerm LetBrand [ProgEq] Term Range
  -- pos "where", ";"s
  | ResolvedMixTerm Id [Type] [Term] Range
  | TermToken Token
  | MixTypeTerm TypeQual Type Range
  | MixfixTerm [Term]
  | BracketTerm BracketKind [Term] Range
    -- pos brackets, ","s
    deriving (Show, Eq, Ord, Typeable, Data)

-- | an equation or a case as pair of a pattern and a term
data ProgEq = ProgEq Term Term Range deriving (Show, Eq, Ord, Typeable, Data)
            -- pos "=" (or "->" following case-of)

-- | an identifier with an optional list of type declarations
data PolyId = PolyId Id [TypeArg] Range deriving (Show, Eq, Ord, Typeable, Data)
              -- pos "[", ",", "]"

{- | an indicator if variables were separated by commas or by separate
declarations -}
data SeparatorKind = Comma | Other deriving (Show, Typeable, Data)

-- ignore all separator kinds in comparisons
instance Eq SeparatorKind where
    _ == _ = True

-- Ord must be consistent with Eq
instance Ord SeparatorKind where
   compare _ _ = EQ

-- | a variable with its type
data VarDecl = VarDecl Id Type SeparatorKind Range
  deriving (Show, Eq, Ord, Typeable, Data)
               -- pos "," or ":"

-- | the kind of a type variable (or a type argument in schemes)
data VarKind = VarKind Kind | Downset Type | MissingKind
 deriving (Show, Eq, Ord, Typeable, Data)

-- | a (simple) type variable with its kind (or supertype)
data TypeArg =
    TypeArg Id Variance VarKind RawKind Int SeparatorKind Range
    -- pos "," or ":", "+" or "-"
    deriving (Show, Typeable, Data)

-- | a value or type variable
data GenVarDecl =
    GenVarDecl VarDecl
  | GenTypeVarDecl TypeArg
    deriving (Show, Eq, Ord, Typeable, Data)

{- * symbol data types
symbols -}
data SymbItems =
    SymbItems SymbKind [Symb] [Annotation] Range
  deriving (Show, Eq, Ord, Typeable, Data)
    -- pos: kind, commas

-- | mapped symbols
data SymbMapItems =
    SymbMapItems SymbKind [SymbOrMap] [Annotation] Range
  deriving (Show, Eq, Ord, Typeable, Data)
    -- pos: kind commas

-- | kind of symbols
data SymbKind =
    Implicit
  | SyKtype
  | SyKsort
  | SyKfun
  | SyKop
  | SyKpred
  | SyKclass
    deriving (Show, Eq, Ord, Typeable, Data)

instance Pretty SymbKind where
  pretty symbol_kind = case symbol_kind of
    Implicit -> text "implicit"
    SyKtype -> text "type"
    SyKsort -> text "sort"
    SyKfun -> text "fun"
    SyKop -> text "op"
    SyKpred -> text "pred"
    SyKclass -> text "class"

-- | type annotated symbols
data Symb = Symb Id (Maybe SymbType) Range
  deriving (Show, Eq, Ord, Typeable, Data)
            -- pos: colon (or empty)

-- | type for symbols
data SymbType = SymbType TypeScheme deriving (Show, Eq, Ord, Typeable, Data)

-- | mapped symbol
data SymbOrMap = SymbOrMap Symb (Maybe Symb) Range
  deriving (Show, Eq, Ord, Typeable, Data)
                   -- pos: "|->" (or empty)

-- * equality instances ignoring positions

instance Eq Type where
    t1 == t2 = compare t1 t2 == EQ

instance Ord Type where
  compare ty1 ty2 = case (ty1, ty2) of
    (TypeName i1 k1 v1, TypeName i2 k2 v2) ->
        if v1 == 0 && v2 == 0 then compare (i1, k1) (i2, k2)
        else compare (v1, k1) (v2, k2)
    (TypeAppl f1 a1, TypeAppl f2 a2) -> compare (f1, a1) (f2, a2)
    (TypeAbs v1 a1 _, TypeAbs v2 a2 _) -> compare (v1, a1) (v2, a2)
    (TypeToken t1, TypeToken t2) -> compare t1 t2
    (BracketType b1 l1 _, BracketType b2 l2 _) -> compare (b1, l1) (b2, l2)
    (KindedType t1 k1 _, KindedType t2 k2 _) -> compare (t1, k1) (t2, k2)
    (MixfixType l1, MixfixType l2) -> compare l1 l2
    (ExpandedType _ t1, t2) -> compare t1 t2
    (t1, ExpandedType _ t2) -> compare t1 t2
    (TypeName {}, _) -> LT
    (_, TypeName {}) -> GT
    (TypeAppl {}, _) -> LT
    (_, TypeAppl {}) -> GT
    (TypeAbs {}, _) -> LT
    (_, TypeAbs {}) -> GT
    (TypeToken _, _) -> LT
    (_, TypeToken _) -> GT
    (BracketType {}, _) -> LT
    (_, BracketType {}) -> GT
    (KindedType {}, _) -> LT
    (_, KindedType {}) -> GT

-- used within quantified formulas
instance Eq TypeArg where
    t1 == t2 = compare t1 t2 == EQ
instance Ord TypeArg where
    compare (TypeArg i1 v1 e1 r1 c1 _ _) (TypeArg i2 v2 e2 r2 c2 _ _) =
        if c1 < 0 && c2 < 0 then compare (v1, e1, r1, c1) (v2, e2, r2, c2)
        else compare (i1, v1, e1, r1, c1) (i2, v2, e2, r2, c2)

-- * compute better position

-- | get a reasonable position for a list with an additional position list
bestRange :: GetRange a => [a] -> Range -> Range
bestRange l (Range ps) = Range (rangeToList (getRange l) ++ ps)

instance GetRange OpAttr where
  getRange a = case a of
    BinOpAttr _ r -> r
    UnitOpAttr _ r -> r

instance GetRange Type where
  getRange ty = case ty of
    TypeName i _ _ -> posOfId i
    TypeAppl t1 t2 -> getRange [t1, t2]
    TypeAbs _ t ps -> bestRange [t] ps
    ExpandedType t1 t2 -> getRange [t1, t2]
    TypeToken t -> tokPos t
    BracketType _ ts ps -> bestRange ts ps
    KindedType t _ ps -> bestRange [t] ps
    MixfixType ts -> getRange ts

instance GetRange Term where
   getRange trm = case trm of
    QualVar v -> getRange v
    QualOp _ (PolyId i _ _) _ _ _ qs -> bestRange [i] qs
    ResolvedMixTerm i _ _ _ -> posOfId i
    ApplTerm t1 t2 ps -> bestRange [t1, t2] ps
    TupleTerm ts ps -> bestRange ts ps
    TypedTerm t _ _ ps -> bestRange [t] ps
    QuantifiedTerm _ _ t ps -> bestRange [t] ps
    LambdaTerm _ _ t ps -> bestRange [t] ps
    CaseTerm t _ ps -> bestRange [t] ps
    LetTerm _ _ t ps -> bestRange [t] ps
    TermToken t -> tokPos t
    MixTypeTerm _ t ps -> bestRange [t] ps
    MixfixTerm ts -> getRange ts
    BracketTerm _ ts ps -> bestRange ts ps
    AsPattern v _ ps -> bestRange [v] ps

instance GetRange TypePattern where
  getRange pat = case pat of
    TypePattern t _ ps -> bestRange [t] ps
    TypePatternToken t -> tokPos t
    MixfixTypePattern ts -> getRange ts
    BracketTypePattern _ ts ps -> bestRange ts ps
    TypePatternArg (TypeArg t _ _ _ _ _ _) ps -> bestRange [t] ps

instance GetRange VarDecl where
    getRange (VarDecl v _ _ p) = bestRange [v] p

instance GetRange TypeArg where
    getRange (TypeArg v _ _ _ _ _ p) = bestRange [v] p

instance GetRange TypeScheme where
    getRange (TypeScheme args t ps) = bestRange args $ bestRange [t] ps

instance GetRange BasicSpec