CONTEXT RAP IN ENGLISH
--! It is allowed to change texts and/or the order of texts IF AND ONLY IF this is also done in the corresponding Haskell files !--
INCLUDE "ASTdocumentation.adl"
INCLUDE "ASTInterface.ifc"
INCLUDE "Atoms.adl"

{-RJ/20150207: Opmerkingen n.a.v. een vluchtige code-inspectie van dit bestand
1) Het is nu nog wel, maar binnen RAP niet meer, mogelijk om een Pattern, Context en/of Concept dezelfde naam te geven (vanwege de INJectiviteit van relaties als name, ptnm). Deze nieuwe beperking lijkt me onwenselijk.
      Reactie HJO/20150207: Die snap ik niet. Twee Concepten met dezelfde naam zijn hetzelfde Concept. Een Pattern mag dezelfde naam hebben als een Concept. Daarmee zijn de uiteraard niet identiek. Een Pattern is nou een maal geen Concept. Dit is nu zo geregeld in RAP. Als je punt is, dat twee verschillende Concepten best dezelfde naam zouden mogen hebben, dan hebben we een issue. Maar ik denk niet dat je dit bedoelt.
2) VIEWs (zoals 'VIEW Gen') horen m.i. niet in dit bestand thuis, maar daar waar de UI wordt gespecificeerd. IDENTs horen wel in dit bestand thuis.
      Reactie HJO/20150207: Helemaal mee eens. Gaan we doen. 
3) Van "RELATION decprps[Declaration*PropertyRule]" zou ik denken dat hij niet alleen INJ, maar ook SUR moet zijn.
      Reactie HJO/20150207: Dat denk ik ook. Leuk is, dat dit geen invloed heeft op de meatgrinder. Immers, die zorgt alleen maar voor de juiste populatie van Declarations. Als blijkt dat we dan overtredingen krijgen, dan gaan we dat meemaken...
-}

CONCEPT Purpose "" TYPE "Text"
CONCEPT Meaning "" TYPE "Text"
CONCEPT ConceptDefinition "" TYPE "Text"

PATTERN Context
CONCEPT Context "A context is the root of the abstract syntax tree of a valid Ampersand rule specification." 
IDENT Context: Context(name[Context*ContextName])  
--CLASSIFY ContextName ISA Conid
RELATION name[Context*ContextName] [UNI,TOT,INJ]
MEANING "The name of a context."
RELATION patterns[Context*Pattern]
MEANING "The patterns in a context."
RELATION concs[Context*PlainConcept]
MEANING "A concept, mentioned anywhere in a context."
RELATION allDeclarations[Context*Declaration]
MEANING "A relation declared in a context"
RELATION gens[Context*Gen]
MEANING "The user-defined generalization rules in a context."
ENDPATTERN

PATTERN Patterns
CONCEPT Pattern "A pattern is a container for relation declarations and rule definitions"
IDENT Pattern: Pattern(name[Pattern*PatternName])  --TODO: The sign for name is overspecification, but is still required, for otherwise an error will occur in the typechecker.

--CLASSIFY PatternName ISA Conid

RELATION name[Pattern*PatternName] [UNI,TOT,INJ]
MEANING "The name of a pattern."
RELATION rules[Pattern*Rule]
MEANING "The user-defined rules in a pattern."
RELATION declarations[Pattern*Declaration]
MEANING "The relation declarations in a pattern."
RELATION purpose[Pattern*Purpose]
MEANING "The purposes of a pattern."


ENDPATTERN

PATTERN Specialization
VIEW Gen: Gen( TXT "CLASSIFY ", genspc;name , TXT " ISA " , gengen;name )
RULE "eq gen": gengen;gengen~ /\ genspc;genspc~ |- I
MEANING "Two generalization rules are identical when the specific concepts are identical and the generic concepts are identical."

RELATION gengen[Gen*PlainConcept] [UNI,TOT]
MEANING "A generalization rule refers to one more generic concept."
RELATION genspc[Gen*PlainConcept] [UNI,TOT]
MEANING "A generalization rule refers to one more specific concept."

--PURPOSE RULE specialization
--{+Specialization has the consequence that an atom is not necessarily an instance of one concept only.
--If limes are citrus fruits, then every lime is not only lime but a citrus fruit as well.
---}
--RELATION instanceOf[Atom*Concept] [TOT] 
--RULE specialization : instanceOf;genspc~;gengen |- instanceOf
--MEANING "Every instance of a specialized concept is an instance of the generic concept too."

ENDPATTERN

PATTERN Concept
CONCEPT Concept "A concept is an abstract term representing a set of atomic terms."
CONCEPT PlainConcept "A concept is a name for a category of similar objects."
IDENT PlainConcept: PlainConcept(name[PlainConcept*ConceptName])
CLASSIFY PlainConcept ISA Concept
--CLASSIFY ConceptName ISA Conid


RELATION name[PlainConcept*ConceptName] [UNI,TOT,INJ]
MEANING "The name of a concept."
--RELATION cptos[Concept*AtomID] [SUR]  --HJO20150204: Deze relatie is vervangen door instanceOf~ . Dit heeft te maken met het feit dat één AtomID in meerdere concepten kan voorkomen. 
--MEANING "The population of a concept."
RELATION cptdf[PlainConcept*ConceptDefinition]
MEANING "The definitions of a concept."
RELATION cptpurpose[PlainConcept*Purpose]
MEANING "The purposes of a concept."
RELATION cpttp[PlainConcept*TechnicalType] [UNI]
MEANING "The (technical) type of a concept"

--CONCEPT Order "The order of the is-a-relation between concepts."
--IDENT Order: Order(ordername)
--
--RELATION ordername[Order*String] [UNI,TOT,INJ]
--MEANING "The name of a class of is-a-related concepts."
--RELATION order[Concept*Order] [UNI,TOT]
--MEANING "A concept belongs to a class of is-a-related concepts."
--RULE "order": order~;genspc~;gengen;order |- I
--MEANING "Is-a-related concepts belong to the same class of is-a-related concepts."
--RULE "different order": ???, a closure would be nice...
--MEANING "Concepts, that are not is-a-related, are in different orders of the is-a-relation."

--NOTE: MESSAGEs depend on the edit possibilities of the interface they are used in.
--if you have written messages for interfaces at a certain moment and you add an interface which can violate a message differently, then you should revise those messages, but probably you will forget to do so->risk for awkward messages in new interface
--RULE "referential integrity": src~;sign~;decpopu;left \/ trg~;sign~;decpopu;right |- order;order~;cptos
--MEANING "An atom in the domain or codomain of a relation is an instance of a concept from the same class as the source respectively the target of that relation."
--MESSAGE "If an atom is in some tuple of a relation, then that atom must exist in the concept that is the source respectively target of that relation. Deletion of an atom from a concept is not permitted if that atom is still present in some tuple of some relation. Nor is addition of a tuple permitted if the source or target atom is not present in the related concept. It is a violation of <b>Referential integrity</b> rule for a relation." 
--VIOLATION (TXT "The tuple ", SRC I, TXT " refers to a source or target atom that does not exist." )
ENDPATTERN

PATTERN Sign
VIEW Sign: Sign( TXT "[" , src;name[PlainConcept*ConceptName] , TXT "*" , trg;name[PlainConcept*ConceptName] , TXT "]" )


RELATION src[Sign*Concept] [UNI,TOT]
MEANING "The source of a sign."
RELATION trg[Sign*Concept] [UNI,TOT]
MEANING "The target of a sign."

--IEW PairID: PairID( TXT "<" , left;atomvalue , TXT "*" , right;atomvalue , TXT ">" )
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: RELATION sign[PairID*Sign] [UNI,TOT]
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: MEANING "The sign of a relationship"
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: RELATION left[PairID*AtomID] [UNI,TOT]
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: MEANING "The source of a relationship."
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: RELATION right[PairID*AtomID] [UNI,TOT]
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: MEANING "The target of a relationship."


--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: PURPOSE RULE "type consistency"
{-In Ampersand, every pair has a signature.
For example, the pair $\langle\id{Pete},5\rangle$ may have the signature $[\id{Person},\id{Rank}]$.
Ampersand is called a type consistent language, because every pair in a relation has the same signature as the relation itself.
For instance, as long as $\id{Person}$ and $\id{Rank}$ are different concepts,
the pairs $\langle\id{Pete},5\rangle$ and $\langle5,\id{Pete}\rangle$ cannot be in the same relation.

In a compiler, type consistency is ensured by a type system.
In a repository, the type of any expression does not depend on the contents of the relations in it.
As a consequence, the type of an expression can be computed based on the types of its constituent relations only.
-}
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: RULE "type consistency" : sign=in[PairID*Declaration];sign
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: MEANING "Type consistency means that all pairs in a relation have the same signature."
ENDPATTERN

PATTERN Declaration
--VIEW Declaration: Declaration( name , TXT "::", sign;src;name[PlainConcept*ConceptName] ,TXT " * ", sign;trg;name[PlainConcept*ConceptName] )
--IDENT Declaration: Declaration( name, sign;src;name, sign;trg;name )
CLASSIFY Declaration ISA Relation
RULE "eq declaration": name;name~ /\ sign;src;(sign;src)~ /\ sign;trg;(sign;trg)~ |- I[Declaration]
MEANING "The unique signature of a relation consists of a relation name, a source concept, and a target concept."
--CLASSIFY DeclarationName ISA Varid
RELATION name[Declaration*DeclarationName] [UNI] --TODO: Should be TOT, but this is only true for user-defined declarations. TODO: I[<Concept>] is a declaration? And what about V?? In Haskell, it currently is.
MEANING "The name of a relation."
RELATION sign[Declaration*Sign] [UNI] --TODO: Should be TOT, but this is only true for user-defined declarations. TODO: I[<Concept>] is a declaration? And what about V?? In Haskell, it currently is.
MEANING "The sign of a declaration."
RELATION decprps[Declaration*PropertyRule] [INJ]
MEANING "The properties of a relation."

CONCEPT PropertyRule "A property rule is a rule, that is a property of a user-declared relation"
CLASSIFY PropertyRule ISA Rule
CONCEPT Property "UNI<|>TOT<|>INJ<|>SUR<|>RFX<|>IRF<|>SYM<|>ASY<|>TRN<|>PROP"
RULE "property enum": I[Property] |- 'UNI' \/ 'TOT' \/ 'INJ' \/ 'SUR' \/ 'RFX' \/ 'IRF' \/ 'SYM' \/ 'ASY' \/ 'TRN' \/ 'PROP'
MEANING "There are eleven tokens, that can be used to define properties on a relation. -> is syntactic suger for UNI and TOT; UNI means univalent; TOT means total; INJ means injective; SUR means surjective; RFX means reflexive; IRF means irreflexive; SYM means symmetric; ASY means antisymmetric; TRN means transitive; and PROP means symmetric and antisymmetric."
RELATION decprL[Declaration*String] [UNI]
MEANING "The prefix of the pragma of a relation."
RELATION decprM[Declaration*String] [UNI]
MEANING "The infix of the pragma of a relation."
RELATION decprR[Declaration*String] [UNI]
MEANING "The suffix of the pragma of a relation."
RELATION decmean[Declaration * Meaning]
MEANING "The meanings of a relation."
RELATION decpurpose[Declaration * Purpose]
MEANING "The purposes of a relation."
RELATION in[PairID*Declaration]
MEANING "The population of a relation."

--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: RULE "entity integrity of relation": left;left~ /\ right;right~ /\ in;in~ |- I
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: MEANING "There cannot be two relationships in the population of a relation with the same source and same target."
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: MESSAGE "Every tuple in a relation is unique, or, no two tuples in the population of a relation may have the same source and target atoms. Addition of a duplicate tuple is not permitted. It is a violation of the <b>Entity integrity</b> rule for this relation."
--HJO,20150420, uitgezet, vanwege gebruik van Atoms.adl: VIOLATION (TXT "A tuple with the same source and target atoms ", SRC I, TXT " already exists." )

--RULE "typed domain": decpopu;left;cptos~;order  |- sign;src;order
--MEANING "The atoms in the domain of a relation belong to the same class as the source of that relation."
--MESSAGE "You try to add a tuple with a source atom, that is not in the population of the source of the relation. This is a violation of the type of the tuple. TIP: enter text in the left input field to get a shorter pick list. Note on ISA-relations: You can make an atom more specific by moving it to the population of a more specific concept."
--VIOLATION (TXT "Source atom ", TGT I, TXT " is not in the population of ", SRC sign;src)

--RULE "typed codomain": decpopu;right;cptos~;order |- sign;trg;order
--MEANING "The atoms in the codomain of a relation belong to the same class as the target of that relation."
--MESSAGE "You try to add a tuple with a target atom, that is not in the population of the target of the relation. This is a violation of the type of the tuple. TIP: enter text in the right input field to get a shorter pick list. Note on ISA-relations: You can make an atom more specific by moving it to the population of a more specific concept."
--VIOLATION (TXT "Target atom ", TGT I, TXT " is not in the population of ", SRC sign;trg)
ENDPATTERN

PATTERN Expression
--IDENT ExpressionID : ExpressionID(exprvalue)  -- @Stef wat wordt hiermee bedoeld? stel wat is de exprvalue van bijvoorbeeld de expressie 'r;t~' ?? Waarom onderscheid in Expression en ExpressonID??

RELATION exprvalue[ExpressionID*Expression] --[UNI,TOT]
MEANING "The value of an expression."
RELATION relsMentionedIn[ExpressionID*Declaration]
MEANING "The user-declared relations in an expression."

-- TODO: HJO: @Stef: 20150407: Is onderstaand deel van dit PATTERN nog relevant? ik denk het niet. Zo ja, hoe dan? Zo nee: verwijderen.
{-CLASSIFY RelationRef ISA Expression

CONCEPT RelationRef "A relation reference (aka relation token) is an expression that refers to a user-declared relation"  
VIEW RelationRef: RelationRef( name , TXT "[" , relsgn;src;name[PlainConcept*ConceptName] , TXT "*" , relsgn;trg;name[PlainConcept*ConceptName] , TXT "]")

RELATION name[RelationRef*DeclarationName] [UNI,TOT]
MEANING "A relation reference has the name of the relation that is being referred to."
RELATION relsgn[RelationRef*Sign] [UNI,TOT]
MEANING "A relation reference has the sign of the relation that is being referred to."
RELATION reldcl[RelationRef*Declaration] [UNI,TOT]
MEANING "A relation reference has the relation that is being referred to."
RULE "rel name is decl name": name = reldcl;name[Declaration*DeclarationName]
MEANING "A relation reference has the same name as the relation to which it refers."
RULE "rel sign sub of decl sign": reldcl = name;name[Declaration*DeclarationName]~ /\ relsgn;subsgn;sign~
MEANING "A relation reference refers to the relation with the same name, the signature of which is larger or equal to the signature of the relation reference."
-}ENDPATTERN

PATTERN Rules
IDENT Rule: Rule(name[Rule*RuleName])
--CLASSIFY RuleName ISA ADLid
RELATION name[Rule*RuleName] [UNI,TOT,INJ]
MEANING "The name of a rule."
RELATION sign[Rule*Sign] [UNI,TOT]
RELATION rrexp[Rule*ExpressionID] [UNI,TOT]
MEANING "The rule expressed in relation algebra."
RELATION rrmean[Rule * Meaning]
MEANING "The meanings of a rule."
RELATION rrpurpose[Rule * Purpose]
MEANING "The purposes of a rule."
RELATION declaredthrough[PropertyRule*Property] [TOT]
MEANING "A property is defined as part of the declaration of relation."

ENDPATTERN

PROCESS Plugs -- This pattern documents the semantics of plugs as of november 2014.
RELATION maintains[Plug*Rule]
RELATION in[PlainConcept*Plug] [TOT]
RELATION in[Declaration*Plug] [TOT]

-- Rules
RULE "rule allocation" : maintains;rrexp;relsMentionedIn |- in~
MEANING "A plug, which maintains a rule, must contain every relation that is mentioned explicitly in that rule."

ROLE Ampersand MAINTAINS "All isas in one plug"
RULE "All isas in one plug" : (-(genspc~;gengen;in) \/ in) /\ (-(gengen~;genspc;in) \/ in)
MEANING "If a concept is stored in a plug, then every generalization of that concept is stored in the same plug."
ENDPROCESS

PATTERN ToDo -- This pattern contains stuff still to be done.
RELATION rrviols[Rule*Violation]
ENDPATTERN
ENDCONTEXT