namespace http://cds.omdoc.org/urtheories❚

import example http://cds.omdoc.org/examples❚
import rules scala://moduleexpressions.mmt.kwarc.info❚
import operators scala://operators.moduleexpressions.mmt.kwarc.info❚
import metaops scala://meta.operators.moduleexpressions.mmt.kwarc.info❚

theory ModExp =
	constant theory   # THY❙
	constant morphism # MOR 1 2❙
	constant diagram # DIAG ❙

	complextheory   # block {| L1T,… |} prec -1000005❙
	complexmorphism # [| L1D,… |] prec -1000005❙

	identity        # IDENTITY 1   prec -1❙
	composition     # COMPOSE 1;… prec -1❙

	// morphismapplication # %L2d!_1 APPLY 2❙


	rule rules?TheoryTypeInhabitable❙
	rule rules?MorphTypeInhabitable❙
	rule rules?DiagramTypeInhabitable ❙

	rule rules?TheoryTypeUniverse❙

	rule rules?AnonymousTheoryInfer❙
	rule rules?AnonymousDiagramInfer ❙
	rule rules?ComplexTheoryInfer❙

	rule rules?MorphCheck❙
	rule rules?DiagramCheck ❙

	rule rules?MorphismApplicationTerm❙
	rule rules?MorphismApplicationCompute❙
❚

theory Combinators =
	include ?ModExp❙

	// Yasmine's diagram operators
	   =========================== ❙
	empty # EMPTY 1❙
	rule metaops?ComputeEmpty ❙

	extends  # 1 EXTENDED_BY { %L1_L2,… } prec -1000000 ❙
	rule metaops?ComputeExtends ❙

	rename1 # L1 ⟿ L2 prec -500000❙
	rename # 1 RENAMING { 2,… } prec -1000000 ❙
	rule operators?ComputeRename ❙

	combine  # COMBINE 1 { 2,… } 3 { 4,… } prec -2000000❙
	translate # MIXIN 1 { 2,… } 3 { 4,… } prec -2000000 ❙
	// rule operators?ComputeMixin ❙
	rule operators?ComputeCombine ❙

	hom # HOM 1 ❙
	rule operators?ComputeHom ❙

	// Navid's diagram operators
	   =========================== ❙
	pushout_inclusion # PUSHOUT 1 ALONG 2 prec -2000000 ❙
	rule operators?ComputePushoutAlongInclusion ❙

	diagram_accessor # 1 . 2 prec -3000000 ❙
	rule metaops?ComputeDiagramAccess❙

	// The diag from file operator expects a filename as first argument given as a string ❙
	include ?Strings ❙
	diagram_from_file # DIAG FROM FILE 1 prec -2000000 ❙
	rule metaops?ComputeDiagramFromFile ❙

	diagram_union # 1UNION… prec -2000000 ❙
	rule metaops?ComputeDiagramUnion ❙

	// diagram_difference_by_diagram # 1 WITHOUT DIAG 2 prec -2000000 ❙
	// rule metaops?ComputeDiagramDifferenceByDiagram ❙

	diagram_difference_by_label # 1 WITHOUT LABEL 2 prec -2000000 ❙
	rule metaops?ComputeDiagramDifferenceByLabel ❙

	diagram_prefix # PREFIX 1 BY 2 prec -2000000 ❙
	rule metaops?ComputePrefixedDiagram ❙

	diagram_closure # CLOSE 1 WITHIN DOCUMENT prec -2000000 ❙
	rule metaops?ComputeDiagramClosure ❙

	// Currently deactivated as Navid's Generalizer ComputationRule not finished
	   generalizer # GENERALIZE 1 ALONG 2 prec -2000000 ❙
❚

theory LFComb =
	include ?LF❙
	include ?Combinators❙
❚