Lines Matching defs:and
8 \title{The HasCASL language and its analysis}
19 The HasCASL parser reuses the token (in \texttt{HToken.hs}) and
21 as ids and annotations from the \texttt{Common} directory.
23 The abstract and concrete syntax of HasCASL are given in the summary
26 constructors) for different representation before and after the static
29 (and not on any global information).
34 order -- kinds, types and terms, where predicate types and formulas are
35 special cases of types and terms respectively.
38 constructors and terms from values, i.e. operations or predicates.
40 Classes, type constructors and values may be declared by giving them a name.
41 A type constructor must at least be declared with a kind and a value with a
49 and a subtype can be defined via a predicate.
53 Kinds and classes are basically constructed from the universe class
54 \texttt{Type} (or \emph{star} in Haskell) and the builtin kind constructor
59 type and the intersection kind.
69 (Infix and outfix type constructors are currently only builtin.)
97 with continuity), products (in $\times$ notation) and the lazy
105 \item function arrows have lowest infix priority and associate to the right
140 Generally, there are two flavors of declarations for type constructors and
141 operations: value and pattern notation. In a value declaration a mixfix id is
143 arguments and mixfix components are intermingled and only the (optional)
147 defaults to the \emph{universe} and no result type for an operation indicates
154 and parenthesized arguments should be forbidden.
164 \item There are simple value and pattern declarations.
176 undecidable and not thoroughly checked (but left to a proof tool).
184 Type variables must be simple ids and there kind can either be an anonymous
185 downset (and using $<$ instead of a colon) or an intersection class (where
190 error). Keeping class and type names disjoint is not further enforced.
194 Constructor ids and selector ids within one alternative must be disjoint
198 \subsection{Terms and formulas}
200 For a uniform mixfix- and type- analysis, terms and formulas are not
201 distinguished and all treated as terms. If the first argument of a mixfix
206 Currently, class constraints and sub/supertype information is ignored during
211 only check for a (unique) type and omit subtype reasoning (that may be done
216 Binding terms are quantified formulas, lambda terms, case- and
230 declared previously (with place holders and a signature type).
260 \item[ParseTerm.hs] parsing classes, types, terms and formulas
275 environment and diagnostic messages on standard output.