076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder{-# LANGUAGE DeriveDataTypeable #-}

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder{- |

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederModule : ./CASL/AS_Basic_CASL.der.hs

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederDescription : Abstract syntax of CASL basic specifications

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederCopyright : (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2006

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederMaintainer : Christian.Maeder@dfki.de

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederStability : provisional

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederPortability : portable

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederAbstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

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

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CASL.AS_Basic_CASL where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maederimport Common.Id

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maederimport Common.AS_Annotation

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport Data.Data

c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederimport Data.Function

c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederimport Data.List

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederimport qualified Data.Set as Set

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- DrIFT command

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder{-! global: GetRange !-}

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder deriving (Show, Typeable, Data)

1d330b771706686190ad2f3711ec5769c555c708Christian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata BASIC_ITEMS b s f = Sig_items (SIG_ITEMS s f)

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder {- the Annotation following the keyword is dropped

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder but preceding the keyword is now an Annotation allowed -}

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder | Free_datatype SortsKind [Annoted DATATYPE_DECL] Range

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder -- pos: free, type, semi colons

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder | Sort_gen [Annoted (SIG_ITEMS s f)] Range

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder -- pos: generated, opt. braces

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder | Var_items [VAR_DECL] Range

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder -- pos: var, semi colons

e05956d1da3c97e4d808926f97c6841c4a561991Christian Maeder | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range

fe883661c9d1a5a8b42ac4e8673ec133d9dad354Christian Maeder -- pos: forall, semi colons, dots

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder | Axiom_items [Annoted (FORMULA f)] Range

64558a09e6f6b95d2689d02dd5251339f8ac505bChristian Maeder -- pos: dots

64558a09e6f6b95d2689d02dd5251339f8ac505bChristian Maeder | Ext_BASIC_ITEMS b

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder deriving (Show, Typeable, Data)

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederdata SortsKind = NonEmptySorts | PossiblyEmptySorts deriving (Show, Typeable, Data)

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata SIG_ITEMS s f = Sort_items SortsKind [Annoted (SORT_ITEM f)] Range

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder -- pos: sort, semi colons

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder | Op_items [Annoted (OP_ITEM f)] Range

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder -- pos: op, semi colons

40b9c4f89adc2853a26acdbd11ed760d4ba96cf0Christian Maeder | Pred_items [Annoted (PRED_ITEM f)] Range

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- pos: pred, semi colons

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder | Datatype_items SortsKind [Annoted DATATYPE_DECL] Range

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder -- type, semi colons

6e5180855658f12f9059d9041f447bf0935de344Christian Maeder | Ext_SIG_ITEMS s

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder deriving (Show, Typeable, Data)

e05956d1da3c97e4d808926f97c6841c4a561991Christian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederdata SORT_ITEM f = Sort_decl [SORT] Range

64558a09e6f6b95d2689d02dd5251339f8ac505bChristian Maeder -- pos: commas

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder | Subsort_decl [SORT] SORT Range

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder -- pos: commas, <

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder | Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) Range

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder {- pos: "=", "{", ":", ".", "}"

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder the left anno list stored in Annoted Formula is

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder parsed after the equal sign -}

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder | Iso_decl [SORT] Range

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder -- pos: "="s

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder deriving (Show, Typeable, Data)

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederdata OP_ITEM f = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] Range

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder -- pos: commas, colon, OP_ATTR sep. by commas

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder | Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) Range

b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder -- pos: "="

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder deriving (Show, Typeable, Data)

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata OpKind = Total | Partial deriving (Show, Eq, Ord, Typeable, Data)

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederdata OP_TYPE = Op_type OpKind [SORT] SORT Range

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder -- pos: "*"s, "->" ; if null [SORT] then Range = [] or pos: "?"

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder deriving (Show, Eq, Ord, Typeable, Data)

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder

4be371b81d055e03a5946e4ec333613f313d689bChristian Maederargs_OP_TYPE :: OP_TYPE -> [SORT]

4be371b81d055e03a5946e4ec333613f313d689bChristian Maederargs_OP_TYPE (Op_type _ args _ _) = args

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder

4be371b81d055e03a5946e4ec333613f313d689bChristian Maederres_OP_TYPE :: OP_TYPE -> SORT

4be371b81d055e03a5946e4ec333613f313d689bChristian Maederres_OP_TYPE (Op_type _ _ res _) = res

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder

4be371b81d055e03a5946e4ec333613f313d689bChristian Maederdata OP_HEAD = Op_head OpKind [VAR_DECL] (Maybe SORT) Range

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder -- pos: "(", semicolons, ")", colon

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder deriving (Show, Eq, Ord, Typeable, Data)

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder

4be371b81d055e03a5946e4ec333613f313d689bChristian Maederdata OP_ATTR f = Assoc_op_attr | Comm_op_attr | Idem_op_attr

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder | Unit_op_attr (TERM f)

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder deriving (Show, Eq, Ord, Typeable, Data)

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederdata PRED_ITEM f = Pred_decl [PRED_NAME] PRED_TYPE Range

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder -- pos: commas, colon

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder | Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) Range

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder -- pos: "<=>"

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder deriving (Show, Typeable, Data)

f0920567c5a918c34a69cdb6b56826ef49becfb5Christian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederdata PRED_TYPE = Pred_type [SORT] Range

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

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder deriving (Show, Eq, Ord, Typeable, Data)

37bd4066d4a1d6bf8126681f920165aa9a873d91Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederdata PRED_HEAD = Pred_head [VAR_DECL] Range

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder -- pos: "(",semi colons , ")"

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder deriving (Show, Typeable, Data)

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederdata DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] Range

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- pos: "::=", "|"s

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder deriving (Show, Typeable, Data)

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederdata ALTERNATIVE = Alt_construct OpKind OP_NAME [COMPONENTS] Range

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder -- pos: "(", semi colons, ")" optional "?"

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder | Subsorts [SORT] Range

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder -- pos: sort, commas

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder deriving (Show, Typeable, Data)

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederdata COMPONENTS = Cons_select OpKind [OP_NAME] SORT Range

-- pos: commas, colon or ":?"

| Sort SORT

deriving (Show, Typeable, Data)

data VAR_DECL = Var_decl [VAR] SORT Range

-- pos: commas, colon

deriving (Show, Eq, Ord, Typeable, Data)

varDeclRange :: VAR_DECL -> [Pos]

varDeclRange (Var_decl vs s _) = case vs of

[] -> []

v : _ -> joinRanges [tokenRange v, idRange s]

{- Position definition for FORMULA:

Information on parens are also encoded in Range. 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 Junctor = Con | Dis deriving (Show, Eq, Ord, Typeable, Data)

dualJunctor :: Junctor -> Junctor

dualJunctor Con = Dis

dualJunctor Dis = Con

data Relation = Implication | RevImpl | Equivalence

deriving (Show, Eq, Ord, Typeable, Data)

data Equality = Strong | Existl deriving (Show, Eq, Ord, Typeable, Data)

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

-- pos: QUANTIFIER, semi colons, dot

| Junction Junctor [FORMULA f] Range

-- pos: "/\"s or "\/"s

| Relation (FORMULA f) Relation (FORMULA f) Range

{- pos: "<=>", "=>" or "if"

Note: The first formula is the premise also for "if"!

Explicitly: During parsing, "f2 if f1" is saved as

"Relation f1 RevImpl f2 _" -}

| Negation (FORMULA f) Range

-- pos: not

| Atom Bool Range

-- pos: true or false

| Predication PRED_SYMB [TERM f] Range

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

| Definedness (TERM f) Range

-- pos: def

| Equation (TERM f) Equality (TERM f) Range

-- pos: =e= or =

| Membership (TERM f) SORT Range

-- pos: in

| Mixfix_formula (TERM f)

{- Mixfix_ Term/Token/(..)/[..]/{..}

a formula left original for mixfix analysis -}

| Unparsed_formula String Range

-- pos: first Char in String

| Sort_gen_ax [Constraint] Bool -- flag: belongs to a free type?

| QuantOp OP_NAME OP_TYPE (FORMULA f) -- second order quantifiers

| QuantPred PRED_NAME PRED_TYPE (FORMULA f)

| ExtFORMULA f

-- needed for CASL extensions

deriving (Show, Eq, Ord, Typeable, Data)

mkSort_gen_ax :: [Constraint] -> Bool -> FORMULA f

mkSort_gen_ax = Sort_gen_ax . sortConstraints

is_True_atom :: FORMULA f -> Bool

is_True_atom f = case f of

Atom b _ -> b

_ -> False

is_False_atom :: FORMULA f -> Bool

is_False_atom f = case f of

Atom b _ -> not b

_ -> False

boolForm :: Bool -> FORMULA f

boolForm b = Atom b nullRange

trueForm :: FORMULA f

trueForm = boolForm True

falseForm :: FORMULA f

falseForm = boolForm False

{- In the CASL institution, sort generation constraints have an

additional signature morphism component (Sect. III:2.1.3, p.134 of the

CASL Reference Manual). The extra signature morphism component is

needed because the naive translation of sort generation constraints

along signature morphisms may violate the satisfaction condition,

namely when sorts are identified by the translation, with the effect

that new terms can be formed. We avoid this extra component here and

instead use natural numbers to decorate sorts, in this way retaining

their identity w.r.t. the original signature. The newSort in a

Constraint is implicitly decorated with its index in the list of

Constraints. The opSymbs component collects all the operation symbols

with newSort (with that index!) as a result sort. The argument sorts

of an operation symbol are decorated explicitly via a list [Int] of

integers. The origSort in a Constraint is the original sort

corresponding to the index. A negative index indicates a sort outside

the constraint (i.e. a "parameter sort"). Note that this representation of

sort generation constraints is efficiently tailored towards both the use in

the proof calculus (Chap. IV:2, p. 282 of the CASL Reference Manual)

and the coding into second order logic (p. 429 of Theoret. Comp. Sci. 286).

-}

data Constraint = Constraint { newSort :: SORT,

opSymbs :: [(OP_SYMB, [Int])],

origSort :: SORT }

deriving (Show, Typeable, Data)

instance Ord Constraint where

compare (Constraint s1 cs1 _) (Constraint s2 cs2 _) =

compare (s1, map fst cs1) (s2, map fst cs2)

instance Eq Constraint where

a == b = compare a b == EQ

sortConstraints :: [Constraint] -> [Constraint]

sortConstraints cs = let

nCs = sort cs

iS = map(\ c -> let

Just j = findIndex ((origSort c ==) . origSort) nCs in j) cs

updInd i = if i < 0 then i else iS !! i

in

map (\ (Constraint s os o) ->

Constraint s (sortBy (on compare fst)

$ map (\ (c, is) -> (c, map updInd is)) os) o) nCs

-- | no duplicate sorts, i.e. injective sort map?

isInjectiveList :: Ord a => [a] -> Bool

isInjectiveList l = Set.size (Set.fromList l) == length l

{- | from a Sort_gex_ax, recover:

a traditional sort generation constraint plus a sort mapping -}

recover_Sort_gen_ax :: [Constraint] ->

([SORT], [OP_SYMB], [(SORT, SORT)])

recover_Sort_gen_ax constrs =

if isInjectiveList sorts

-- we can ignore indices

then (sorts, map fst (concatMap opSymbs constrs), [])

{- otherwise, we have to introduce new sorts for the indices

and afterwards rename them into the sorts they denote -}

else (origSorts, indOps, zip origSorts sorts)

where

sorts = map newSort constrs

origSorts = map origSort constrs

indSort s i = if i < 0 then s else origSorts !! i

indOps = concatMap (\ c -> map (indOp $ origSort c) $ opSymbs c) constrs

indOp res (Qual_op_name opn (Op_type k args1 _ pos1) pos, args) =

Qual_op_name opn

(Op_type k (zipWith indSort args1 args) res pos1) pos

indOp _ _ = error

"CASL/AS_Basic_CASL: Internal error: Unqualified OP_SYMB in Sort_gen_ax"

{- | from a Sort_gen_ax, recover:

the sorts, each paired with the constructors -}

recoverSortGen :: [Constraint] -> [(SORT, [OP_SYMB])]

recoverSortGen = map $ \ c -> (newSort c, map fst $ opSymbs c)

{- | from a free Sort_gen_ax, recover:

the sorts, each paired with the constructors

fails (i.e. delivers Nothing) if the sort map is not injective -}

recover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT, [OP_SYMB])]

recover_free_Sort_gen_ax constrs =

if isInjectiveList $ map newSort constrs

then Just $ recoverSortGen constrs

else Nothing

-- | determine whether a formula is a sort generation constraint

isSortGen :: FORMULA f -> Bool

isSortGen f = case f of

Sort_gen_ax _ _ -> True

_ -> False

data QUANTIFIER = Universal | Existential | Unique_existential

deriving (Show, Eq, Ord, Typeable, Data)

data PRED_SYMB = Pred_name PRED_NAME

| Qual_pred_name PRED_NAME PRED_TYPE Range

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

deriving (Show, Eq, Ord, Typeable, Data)

predSymbName :: PRED_SYMB -> PRED_NAME

predSymbName p = case p of

Pred_name n -> n

Qual_pred_name n _ _ -> n

data TERM f = Qual_var VAR SORT Range -- pos: "(", var, colon, ")"

| Application OP_SYMB [TERM f] Range

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

| Sorted_term (TERM f) SORT Range

-- pos: colon

| Cast (TERM f) SORT Range

-- pos: "as"

| Conditional (TERM f) (FORMULA f) (TERM f) Range

-- pos: "when", "else"

| Unparsed_term String Range -- 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 Range

-- pos: colon

| Mixfix_cast SORT Range

-- pos: "as"

| Mixfix_parenthesized [TERM f] Range

{- non-emtpy term list

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

| Mixfix_bracketed [TERM f] Range

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

| Mixfix_braced [TERM f] Range

{- also for list-notation

pos: "{", "}" -}

| ExtTERM f

deriving (Show, Eq, Ord, Typeable, Data)

-- | state after mixfix- but before overload resolution

varOrConst :: Token -> TERM f

varOrConst t = Application (Op_name $ simpleIdToId t) [] $ tokPos t

data OP_SYMB = Op_name OP_NAME

| Qual_op_name OP_NAME OP_TYPE Range

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

deriving (Show, Eq, Ord, Typeable, Data)

opSymbName :: OP_SYMB -> OP_NAME

opSymbName o = case o of

Op_name n -> n

Qual_op_name n _ _ -> n

-- * short cuts for terms and formulas

-- | create binding if variables are non-null

mkForallRange :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f

mkForallRange vl f ps =

if null vl then f else Quantification Universal vl f ps

mkForall :: [VAR_DECL] -> FORMULA f -> FORMULA f

mkForall vl f = mkForallRange vl f nullRange

-- | create an existential binding

mkExist :: [VAR_DECL] -> FORMULA f -> FORMULA f

mkExist vs f = Quantification Existential vs f nullRange

-- | convert a singleton variable declaration into a qualified variable

toQualVar :: VAR_DECL -> TERM f

toQualVar (Var_decl v s ps) =

if isSingle v then Qual_var (head v) s ps else error "toQualVar"

mkRel :: Relation -> FORMULA f -> FORMULA f -> FORMULA f

mkRel r f f' = Relation f r f' nullRange

mkImpl :: FORMULA f -> FORMULA f -> FORMULA f

mkImpl = mkRel Implication

mkAnyEq :: Equality -> TERM f -> TERM f -> FORMULA f

mkAnyEq e f f' = Equation f e f' nullRange

mkExEq :: TERM f -> TERM f -> FORMULA f

mkExEq = mkAnyEq Existl

mkStEq :: TERM f -> TERM f -> FORMULA f

mkStEq = mkAnyEq Strong

mkEqv :: FORMULA f -> FORMULA f -> FORMULA f

mkEqv = mkRel Equivalence

mkAppl :: OP_SYMB -> [TERM f] -> TERM f

mkAppl op_symb fs = Application op_symb fs nullRange

mkPredication :: PRED_SYMB -> [TERM f] -> FORMULA f

mkPredication symb fs = Predication symb fs nullRange

-- | turn sorted variable into variable delcaration

mkVarDecl :: VAR -> SORT -> VAR_DECL

mkVarDecl v s = Var_decl [v] s nullRange

-- | turn sorted variable into term

mkVarTerm :: VAR -> SORT -> TERM f

mkVarTerm v = toQualVar . mkVarDecl v

-- | optimized conjunction

conjunctRange :: [FORMULA f] -> Range -> FORMULA f

conjunctRange fs ps = case fs of

[] -> Atom True ps

[phi] -> phi

_ -> Junction Con fs ps

conjunct :: [FORMULA f] -> FORMULA f

conjunct fs = conjunctRange fs nullRange

disjunctRange :: [FORMULA f] -> Range -> FORMULA f

disjunctRange fs ps = case fs of

[] -> Atom False ps

[phi] -> phi

_ -> Junction Dis fs ps

disjunct :: [FORMULA f] -> FORMULA f

disjunct fs = disjunctRange fs nullRange

mkQualOp :: OP_NAME -> OP_TYPE -> OP_SYMB

mkQualOp f ty = Qual_op_name f ty nullRange

mkQualPred :: PRED_NAME -> PRED_TYPE -> PRED_SYMB

mkQualPred f ty = Qual_pred_name f ty nullRange

negateForm :: FORMULA f -> Range -> FORMULA f

negateForm f r = case f of

Atom b ps -> Atom (not b) ps

Negation nf _ -> nf

_ -> Negation f r

mkNeg :: FORMULA f -> FORMULA f

mkNeg f = negateForm f nullRange

mkVarDeclStr :: String -> SORT -> VAR_DECL

mkVarDeclStr = mkVarDecl . mkSimpleId

-- * type synonyms

type CASLFORMULA = FORMULA ()

type CASLTERM = TERM ()

type OP_NAME = Id

type PRED_NAME = Id

type SORT = Id

type VAR = Token

data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq, Ord, Typeable, Data)

symbItemsName :: SYMB_ITEMS -> [String]

symbItemsName (Symb_items _ syms _ ) =

map (\x -> case x of

Symb_id i -> show i

Qual_id i _ _ -> show i) syms

data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq, Ord, Typeable, Data)

data SYMB_KIND = Implicit | Sorts_kind

| Ops_kind | Preds_kind

deriving (Show, Eq, Ord, Typeable, Data)

data SYMB = Symb_id Id

| Qual_id Id TYPE Range

-- pos: colon

deriving (Show, Eq, Ord, Typeable, Data)

data TYPE = O_type OP_TYPE

| P_type PRED_TYPE

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

deriving (Show, Eq, Ord, Typeable, Data)

data SYMB_OR_MAP = Symb SYMB

| Symb_map SYMB SYMB Range

-- pos: "|->"

deriving (Show, Eq, Ord, Typeable, Data)