{- |

Module : $Header$

Copyright : (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2004

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : hets@tzi.de

Stability : provisional

Portability : portable

This is the Abstract Syntax tree of CASL Basic_specs, Symb_items and

Symb_map_items.

Follows Sect. II:2.2 of the CASL Reference Manual.

-}

module CASL.AS_Basic_CASL where

import Common.Id

import Common.AS_Annotation

-- DrIFT command

{-! global: UpPos !-}

data BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]

deriving (Show,Eq)

data BASIC_ITEMS b s f = Sig_items (SIG_ITEMS b s f)

-- the Annotation following the keyword is dropped

-- but preceding the keyword is now an Annotation allowed

| Free_datatype [Annoted DATATYPE_DECL] [Pos]

-- pos: free, type, semi colons

| Sort_gen [Annoted (SIG_ITEMS b s f)] [Pos]

-- pos: generated, opt. braces

| Var_items [VAR_DECL] [Pos]

-- pos: var, semi colons

| Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] [Pos]

-- pos: forall, semi colons, dots

| Axiom_items [Annoted (FORMULA f)] [Pos]

-- pos: dots

| Ext_BASIC_ITEMS b

deriving (Show,Eq)

data SIG_ITEMS b s f = Sort_items [Annoted (SORT_ITEM f)] [Pos]

-- pos: sort, semi colons

| Op_items [Annoted (OP_ITEM f)] [Pos]

-- pos: op, semi colons

| Pred_items [Annoted (PRED_ITEM f)] [Pos]

-- pos: pred, semi colons

| Datatype_items [Annoted DATATYPE_DECL] [Pos]

-- type, semi colons

| Ext_SIG_ITEMS s

deriving (Show,Eq)

data SORT_ITEM f = Sort_decl [SORT] [Pos]

-- pos: commas

| Subsort_decl [SORT] SORT [Pos]

-- pos: commas, <

| Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) [Pos]

-- pos: "=", "{", ":", ".", "}"

-- the left anno list stored in Annoted Formula is

-- parsed after the equal sign

| Iso_decl [SORT] [Pos]

-- pos: "="s

deriving (Show,Eq)

data OP_ITEM f = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] [Pos]

-- pos: commas, colon, OP_ATTR sep. by commas

| Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) [Pos]

-- pos: "="

deriving (Show,Eq)

data OP_TYPE = Total_op_type [SORT] SORT [Pos]

-- pos: "*"s, "->" ; if null [SORT] then [Pos] = []

| Partial_op_type [SORT] SORT [Pos]

-- pos: "*"s, "->?"; if null [SORT] then pos: "?"

deriving (Show,Eq,Ord)

data OP_HEAD = Total_op_head [ARG_DECL] SORT [Pos]

-- pos: "(", semicolons, ")", colon

| Partial_op_head [ARG_DECL] SORT [Pos]

deriving (Show,Eq)

data ARG_DECL = Arg_decl [VAR] SORT [Pos]

-- pos: commas, colon

deriving (Show,Eq)

data OP_ATTR f = Assoc_op_attr | Comm_op_attr | Idem_op_attr

| Unit_op_attr (TERM f)

deriving (Show,Eq)

data PRED_ITEM f = Pred_decl [PRED_NAME] PRED_TYPE [Pos]

-- pos: commas, colon

| Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) [Pos]

-- pos: "<=>"

deriving (Show,Eq)

data PRED_TYPE = Pred_type [SORT] [Pos]

-- pos: if null [SORT] then "(",")" else "*"s

deriving (Show,Eq,Ord)

data PRED_HEAD = Pred_head [ARG_DECL] [Pos]

-- pos: "(",semi colons , ")"

deriving (Show,Eq)

data DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] [Pos]

-- pos: "::=", "|"s

deriving (Show,Eq)

data ALTERNATIVE = Total_construct OP_NAME [COMPONENTS] [Pos]

-- pos: "(", semi colons, ")"

| Partial_construct OP_NAME [COMPONENTS] [Pos]

-- pos: "(", semi colons, ")", "?"

| Subsorts [SORT] [Pos]

-- pos: sort, commas

deriving (Show,Eq)

data COMPONENTS = Total_select [OP_NAME] SORT [Pos]

-- pos: commas, colon

| Partial_select [OP_NAME] SORT [Pos]

-- pos: commas, ":?"

| Sort SORT

deriving (Show,Eq)

data VAR_DECL = Var_decl [VAR] SORT [Pos]

-- pos: commas, colon

deriving (Show,Eq,Ord)

{- Position definition for FORMULA:

Information on parens are also encoded in [Pos]. If there

are more Pos than necessary there is a pair of Pos enclosing the

other Pos informations which encode the brackets of every kind

-}

data FORMULA f = Quantification QUANTIFIER [VAR_DECL] (FORMULA f) [Pos]

-- pos: QUANTIFIER, semi colons, dot

| Conjunction [FORMULA f] [Pos]

-- pos: "/\"s

| Disjunction [FORMULA f] [Pos]

-- pos: "\/"s

| Implication (FORMULA f) (FORMULA f) Bool [Pos]

-- pos: "=>" or "if" (True -> "=>")

| Equivalence (FORMULA f) (FORMULA f) [Pos]

-- pos: "<=>"

| Negation (FORMULA f) [Pos]

-- pos: not

| True_atom [Pos]

-- pos: true

| False_atom [Pos]

-- pos: false

| Predication PRED_SYMB [TERM f] [Pos]

-- pos: opt. "(",commas,")"

| Definedness (TERM f) [Pos]

-- pos: def

| Existl_equation (TERM f) (TERM f) [Pos]

-- pos: =e=

| Strong_equation (TERM f) (TERM f) [Pos]

-- pos: =

| Membership (TERM f) SORT [Pos]

-- pos: in

| Mixfix_formula (TERM f) -- Mixfix_ Term/Token/(..)/[..]/{..}

-- a formula left original for mixfix analysis

| Unparsed_formula String [Pos]

-- pos: first Char in String

| Sort_gen_ax [SORT] [OP_SYMB] -- qualified OP_SYMB

-- needed for CASL extensions

| ExtFORMULA f

deriving (Show,Eq,Ord)

data QUANTIFIER = Universal | Existential | Unique_existential

deriving (Show,Eq,Ord)

data PRED_SYMB = Pred_name PRED_NAME

| Qual_pred_name PRED_NAME PRED_TYPE [Pos]

-- pos: "(", pred, colon, ")"

deriving (Show,Eq,Ord)

data TERM f = Simple_id SIMPLE_ID -- "Var" might be a better constructor

| Qual_var VAR SORT [Pos]

-- pos: "(", var, colon, ")"

| Application OP_SYMB [TERM f] [Pos]

-- pos: parens around TERM f if any and seperating commas

| Sorted_term (TERM f) SORT [Pos]

-- pos: colon

| Cast (TERM f) SORT [Pos]

-- pos: "as"

| Conditional (TERM f) (FORMULA f) (TERM f) [Pos]

-- pos: "when", "else"

| Unparsed_term String [Pos] -- SML-CATS

-- A new intermediate state

| Mixfix_qual_pred PRED_SYMB -- as part of a mixfix formula

| Mixfix_term [TERM f] -- not starting with Mixfix_sorted_term/cast

| Mixfix_token Token -- NO-BRACKET-TOKEN, LITERAL, PLACE

| Mixfix_sorted_term SORT [Pos]

-- pos: colon

| Mixfix_cast SORT [Pos]

-- pos: "as"

| Mixfix_parenthesized [TERM f] [Pos] -- non-emtpy term list

-- pos: "(", commas, ")"

| Mixfix_bracketed [TERM f] [Pos]

-- pos: "[", commas, "]"

| Mixfix_braced [TERM f] [Pos] -- also for list-notation

-- pos: "{", "}"

deriving (Show,Eq,Ord)

data OP_SYMB = Op_name OP_NAME

| Qual_op_name OP_NAME OP_TYPE [Pos]

-- pos: "(", op, colon, ")"

deriving (Show,Eq,Ord)

type OP_NAME = Id

type PRED_NAME = Id

type SORT = Id

type VAR = SIMPLE_ID

-----

data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] [Pos]

-- pos: SYMB_KIND, commas

deriving (Show,Eq)

data SYMB_ITEMS_LIST = Symb_items_list [SYMB_ITEMS] [Pos]

-- pos: commas

deriving (Show,Eq)

data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] [Pos]

-- pos: SYMB_KIND, commas

deriving (Show,Eq)

data SYMB_MAP_ITEMS_LIST = Symb_map_items_list [SYMB_MAP_ITEMS] [Pos]

-- pos: commas

deriving (Show,Eq)

data SYMB_KIND = Implicit | Sorts_kind

| Ops_kind | Preds_kind

deriving (Show,Eq)

data SYMB = Symb_id Id

| Qual_id Id TYPE [Pos]

-- pos: colon

deriving (Show,Eq)

data TYPE = O_type OP_TYPE

| P_type PRED_TYPE

| A_type SORT -- ambiguous pred or (constant total) op

deriving (Show,Eq)

data SYMB_OR_MAP = Symb SYMB

| Symb_map SYMB SYMB [Pos]

-- pos: "|->"

deriving (Show,Eq)