namespace http://cds.omdoc.org/qmt❚
theory QMTTypes =
query ❙
prop ❙
basetp ❙
tp ❙
❚
theory QMTQuery =
// Precedence -16xxxx❙
// <<left>> union|intersection|difference <<right>> ❙
Union # 1 or 2 prec -169000 ❙
Intersection # 1 and 2 prec -169000❙
Difference # 1 but not 2 prec -169000❙
Tuple # (* 1,… *) prec -160000❙
Projection # L1 of 2 prec -160000❙
// binders ❙
Let # let V1 := 2 in 3 prec -168000❙
Mapping # 2 map V1 *=>* 3 prec -168000❙
BigUnion # <* 3 | V1 in 2 *> prec -168000❙
Comprehension # {* V1 in 2 | 3 *} prec -168000 ❙
// select [from <<start>> until <<end>>]|<<index>> of <<query>>❙
Slice # select from L1 until L2 of 3 prec -160004❙
SliceFrom # select from L1 of 2 prec -160003❙
SliceUntil # select until L1 of 2 prec -160002❙
Element # select L1 of 2 prec -160001❙
// component|subobject <<spec>> of <<query>>❙
Component # component L1 of 2 prec -160000❙
SubObject # subobject L1 of 2 prec -160000❙
I # use L1 for 2 prec -160000 ❙
Closure # closure of 1 prec -160000❙
Singleton # {* 1 *} prec -160000❙
// related to <<query>> by <<relation>>❙
Related # related to 1 by 2 prec -160000❙
// leaf case ❙
Literal # literal 1 prec -160000❙
Literals # literals 1,… prec -160000❙
Paths # paths 1 prec -160000❙
QueryFunctionApply # function L1 2 prec -160000❙
❚
theory QMTJudgements =
// Precedence -15xxxx❙
/T Equality of two terms ❙
Equals # V1 2 *==* 3 prec -150000❙
/T One type has a specific term ❙
Types # V1 2 *:* 3 prec -150000❙
❚
theory QMTProp =
// Precedence -14xxxx❙
/T unary type relation ❙
IsA # 1 isa L2 prec -140000❙
/T ancestor relation between paths ❙
PrefixOf # 1 *<<* 2 prec -140000❙
/T element relation between elements and sets ❙
IsIn # 1 contains 2 prec -140000❙
/T emptiness of a set ❙
IsEmpty # empty 1 prec -140000❙
/T equality of elements ❙
Equal # 1 *=* 2 prec -140000❙
/T negation ❙
Not # *!* 1 prec -140000❙
/T And ❙
And # 1 *&&* 2 prec -140000❙
/T Or ❙
Or # 1 *||* 2 prec -140000❙
/T Forall ❙
Forall # forall V1 in 2 *.* 3 prec -140000❙
/T Exists ❙
Exists # exists V1 in 2 *.* 3 prec -140000❙
/T Holds ❙
Holds # holds 1 2 prec -140000❙
❚
theory QMTRelationExp =
// Precedence -13xxxx❙
/T base case: an atomic binary relation ❙
ToObject # object 1 prec -130000❙
/T base case: the inverse of an atomic binary relation ❙
ToSubject # subject 1 prec -130000❙
/T the transitive closure of a relation ❙
Transitive # *+ 1 prec -130000❙
/T the symmetric closure of a relation ❙
Symmetric # symmetric 1 prec -130000❙
/T the union of a list of relations ❙
Choice # choice 1,… prec -130000❙
/T the composition of a list of relations ❙
Sequence # sequence 1,… prec -130000❙
/T the reflexive relation ❙
Reflexive # reflexive 1 prec -130000❙
/T the reflexive relation restricted to a set of paths ❙
HasType # hastype 1,… *--* 2,… prec -130000❙
❚
theory QMTBinaries =
// Precedence -12xxxx❙
DependsOn # dependson prec -120000 ❙
HasMeta # hasmeta prec -120000 ❙
Includes # includes prec -120000 ❙
HasDomain # hasdomain prec -120000 ❙
HasCodomain # hascodomain prec -120000 ❙
IsInstanceOf # isinstanceof prec -120000 ❙
RefersTo # refers prec -120000 ❙
Declares # declares prec -120000 ❙
IsAliasFor # isaliasfor prec -120000 ❙
IsAlignedWith # isalignedwith prec -120000 ❙
❚
theory QMTUnaries =
// Precedence -12xxxx❙
IsDocument # document prec -120000 ❙
IsTheory # theory prec -120000 ❙
IsView # view prec -120000 ❙
IsStructure # structure prec -120000 ❙
IsConstant # constant prec -120000 ❙
IsPattern # pattern prec -120000 ❙
IsInstance # instance prec -120000 ❙
IsDerivedDeclaration # deriveddeclaration prec -120000 ❙
IsConAss # conass prec -120000 ❙
IsStrAss # strass prec -120000 ❙
IsNotation # notation prec -120000 ❙
❚
theory QMTLiterals =
// TODO: Literals ❙
❚
theory QMT =
// include the MMT base in notations
include ?mmt ❙
// TODO: Precedence ❙
include ?QMTQuery ❙
include ?QMTProp ❙
include ?QMTRelationExp ❙
include ?QMTJudgements ❙
include ?QMTUnaries ❙
include ?QMTBinaries ❙
include ?QMTLiterals ❙
include ?QMTTypes ❙
❚