content: {-# 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
  