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