1788N/A{-# LANGUAGE DeriveDataTypeable #-}
1788N/ADescription : Abstract syntax of CASL basic specifications
1788N/ACopyright : (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2006
1788N/AMaintainer : Christian.Maeder@dfki.de
1788N/AAbstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.
1788N/A Follows Sect. II:2.2 of the CASL Reference Manual.
1788N/Adata BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]
1788N/A deriving (Show, Typeable, Data)
1788N/Adata BASIC_ITEMS b s f = Sig_items (SIG_ITEMS s f)
1788N/A {- the Annotation following the keyword is dropped
1788N/A but preceding the keyword is now an Annotation allowed -}
1788N/A | Free_datatype SortsKind [Annoted DATATYPE_DECL] Range
1788N/A -- pos: free, type, semi colons
1788N/A | Sort_gen [Annoted (SIG_ITEMS s f)] Range
1788N/A -- pos: generated, opt. braces
1788N/A | Var_items [VAR_DECL] Range
1788N/A | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range
1788N/A -- pos: forall, semi colons, dots
1788N/A | Axiom_items [Annoted (FORMULA f)] Range
1788N/A deriving (Show, Typeable, Data)
1788N/Adata SortsKind = NonEmptySorts | PossiblyEmptySorts deriving (Show, Typeable, Data)
1788N/Adata SIG_ITEMS s f = Sort_items SortsKind [Annoted (SORT_ITEM f)] Range
1788N/A | Op_items [Annoted (OP_ITEM f)] Range
1788N/A | Pred_items [Annoted (PRED_ITEM f)] Range
1788N/A | Datatype_items SortsKind [Annoted DATATYPE_DECL] Range
1788N/A deriving (Show, Typeable, Data)
1788N/Adata SORT_ITEM f = Sort_decl [SORT] Range
| Subsort_decl [SORT] SORT Range
| Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) Range
{- pos: "=", "{", ":", ".", "}"
the left anno list stored in Annoted Formula is
parsed after the equal sign -}
deriving (Show, Typeable, Data)
data OP_ITEM f = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] Range
-- pos: commas, colon, OP_ATTR sep. by commas
| Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) Range
deriving (Show, Typeable, Data)
data OpKind = Total | Partial deriving (Show, Eq, Ord, Typeable, Data)
data OP_TYPE = Op_type OpKind [SORT] SORT Range
-- pos: "*"s, "->" ; if null [SORT] then Range = [] or pos: "?"
deriving (Show, Eq, Ord, Typeable, Data)
args_OP_TYPE :: OP_TYPE -> [SORT]
args_OP_TYPE (Op_type _ args _ _) = args
res_OP_TYPE :: OP_TYPE -> SORT
res_OP_TYPE (Op_type _ _ res _) = res
data OP_HEAD = Op_head OpKind [VAR_DECL] (Maybe SORT) Range
-- pos: "(", semicolons, ")", colon
deriving (Show, Eq, Ord, Typeable, Data)
data OP_ATTR f = Assoc_op_attr | Comm_op_attr | Idem_op_attr
deriving (Show, Eq, Ord, Typeable, Data)
data PRED_ITEM f = Pred_decl [PRED_NAME] PRED_TYPE Range
| Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) Range
deriving (Show, Typeable, Data)
data PRED_TYPE = Pred_type [SORT] Range
-- pos: if null [SORT] then "(",")" else "*"s
deriving (Show, Eq, Ord, Typeable, Data)
data PRED_HEAD = Pred_head [VAR_DECL] Range
-- pos: "(",semi colons , ")"
deriving (Show, Typeable, Data)
data DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] Range
deriving (Show, Typeable, Data)
data ALTERNATIVE = Alt_construct OpKind OP_NAME [COMPONENTS] Range
-- pos: "(", semi colons, ")" optional "?"
deriving (Show, Typeable, Data)
data COMPONENTS = Cons_select OpKind [OP_NAME] SORT Range
-- pos: commas, colon or ":?"
deriving (Show, Typeable, Data)
data VAR_DECL = Var_decl [VAR] SORT Range
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
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
| 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
| Predication PRED_SYMB [TERM f] Range
-- pos: opt. "(",commas,")"
| Definedness (TERM f) Range
| Equation (TERM f) Equality (TERM f) Range
| Membership (TERM f) SORT Range
| Mixfix_formula (TERM f)
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)
-- 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
is_False_atom :: FORMULA f -> Bool
is_False_atom f = case f of
boolForm :: Bool -> FORMULA f
boolForm b = Atom b nullRange
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])],
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]
Just j = findIndex ((origSort c ==) . origSort) nCs in j) cs
updInd i = if i < 0 then i else iS !! i
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
{- | 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 =
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)
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) =
(Op_type k (zipWith indSort args1 args) res pos1) pos
{- | 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
-- | determine whether a formula is a sort generation constraint
isSortGen :: FORMULA f -> Bool
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
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
| Cast (TERM f) SORT Range
| Conditional (TERM f) (FORMULA f) (TERM f) Range
| Unparsed_term String Range -- SML-CATS
-- A new intermediate state
| Mixfix_qual_pred PRED_SYMB -- as part of a mixfix formula
| Mixfix_token Token -- NO-BRACKET-TOKEN, LITERAL, PLACE
| Mixfix_sorted_term SORT Range
| Mixfix_parenthesized [TERM f] Range
| Mixfix_bracketed [TERM f] Range
| Mixfix_braced [TERM f] Range
{- also for list-notation
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
-- * short cuts for terms and formulas
-- | create binding if variables are non-null
mkForallRange :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
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
mkStEq :: TERM f -> TERM f -> FORMULA f
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
conjunct :: [FORMULA f] -> FORMULA f
conjunct fs = conjunctRange fs nullRange
disjunctRange :: [FORMULA f] -> Range -> FORMULA f
disjunctRange fs ps = case fs of
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
mkNeg :: FORMULA f -> FORMULA f
mkNeg f = negateForm f nullRange
mkVarDeclStr :: String -> SORT -> VAR_DECL
mkVarDeclStr = mkVarDecl . mkSimpleId
type CASLFORMULA = FORMULA ()
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 _ ) =
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
deriving (Show, Eq, Ord, Typeable, Data)
deriving (Show, Eq, Ord, Typeable, Data)
data TYPE = O_type OP_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
deriving (Show, Eq, Ord, Typeable, Data)