---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/LevelSpec.tla
---
------------------------------- MODULE LevelSpec -------------------------------
(***************************************************************************)
(* This module specifies the level-checking for the TLA+ language. See *)
(* Section 17.2 of "Specifying Systems" for a discussion of levels and *)
(* level checking in TLA+. *)
(* *)
(* The semantics of TLA+ requires that, in the following constructs, e *)
(* must have level at most 1 (that is, not contain primed variables) and *)
(* A and B must have level at most 2 (that is, not contain temporal *)
(* operators): *)
(* *)
(* e' [A]_e <<A>>_e ENABLED A UNCHANGED e A \cdot B *)
(* *)
(* Although the semantics doesn't really demand it, we also use level *)
(* checking to rule out some bizarre expressions like *)
(* *)
(* []F + []G *)
(* *)
(* We do this by requiring that an operator argument that can normally be *)
(* a non-Boolean must have level at most 2, so it cannot be a temporal *)
(* formula. Thus, in the expression *)
(* *)
(* {e, f} *)
(* *)
(* we require that e and f have level at most 2. *)
(* *)
(* There is another aspect of level checking that is not described here. *)
(* TLA (as opposed to "raw TLA") does not allow an action like x'=x+1 to *)
(* be used as a temporal formula. Thus, in all the following formulas, F *)
(* and G can have any level other than 2: *)
(* *)
(* []F <<F>> F ~> G F -+-> G \EE x : F \AA x : F *)
(* *)
(* A general algorithm for detecting all violations of this requirement *)
(* is nontrivial. For example, if we have *)
(* *)
(* ----- MODULE M ----- *)
(* CONSTANTS A, Op(_) *)
(* B == Op(A) *)
(* ==================== *)
(* *)
(* ------------- MODULE I ------------- *)
(* VARIABLE x *)
(* C(F) == []F *)
(* INSTANCE M WITH A <- x'=x+1, Op <- C *)
(* ==================================== *)
(* *)
(* then the last instance is illegal because it defines B in module I to *)
(* equal the illegal formula [](x'=x+1). Again, this specification does *)
(* not handle this problem. I presume that the initial version of SANY *)
(* will do a simple check of the level of an expression F or G in the *)
(* expressions listed above, and complain only if the expression has *)
(* explicit level 2. *)
(***************************************************************************)
EXTENDS Integers, Sequences
--------------------------------------------------------------------------------
(****************************)
(* Some Useful Definitions *)
(****************************)
NumMax(i, j) == IF i > j THEN i ELSE j
\* Max is apparently defined in the TLC overridden Naturals module
(*************************************************************************)
(* The maximum of the number i and j. *)
(*************************************************************************)
SetMax(S) == IF S = {} THEN 0
ELSE CHOOSE x \in S: \A y \in S: x >= y
(*************************************************************************)
(* The maximum of the set S of natural numbers. *)
(*************************************************************************)
RecordCombine(S, T) ==
(*************************************************************************)
(* If S and T are sets of records, then this equals the set of all *)
(* records rc(s,t) with s in S and t in T, where rc(s,t) is the record *)
(* obtained by "merging" s and t--that is, forming the record whose set *)
(* of fields is the union of the sets of fields of the two records. *)
(*************************************************************************)
LET rc(s, t) ==
[i \in (DOMAIN s) \union (DOMAIN t) |-> IF i \in DOMAIN s THEN s[i]
ELSE t[i]]
IN {rc(s, t): s \in S, t \in T}
--------------------------------------------------------------------------------
CONSTANT NodeId, Node
(*************************************************************************)
(* We represent a collection of TLA+ modules by a semantic forest, *)
(* composed of nodes that may contain references to other nodes. Each *)
(* module is represented by a tree that may have links to the nodes of *)
(* other modules that it imports. The set NodeId is the set of all node *)
(* identifiers, which can be thought of as the set of references to *)
(* nodes. The constant Node is a function from NodeId to the set (type) *)
(* of all possible semantic nodes. *)
(*************************************************************************)
Null == CHOOSE n: n \notin NodeId
(*************************************************************************)
(* A value that is not a node id. *)
(*************************************************************************)
--------------------------------------------------------------------------------
(***************************************************************************)
(* The Semantic Nodes *)
(* ------------------ *)
(* Here are the kinds of semantic nodes and what they represent *)
(* *)
(* ModuleNode : A module *)
(* InstanceNode : An INSTANCE statement *)
(* OpDefNode : An operator definition. As explained *)
(* below, all built-in TLA+ constructs are *)
(* represented as defined operators. *)
(* ConstantDeclNode : A constant declaration or a formal parameter *)
(* of a definition *)
(* VariableDeclNode : A variable declaration. *)
(* OpDeclNode : A ConstantDeclNode or a VariableDeclNode *)
(* OpApplNode : An application of an operator. *)
(* SubstitutionNode : The sequence of WITH substitutions for an *)
(* INSTANCE statement. *)
(* BoundSymbolNode : A bounded identifier. *)
(* LetInNode : A LET/IN statement. *)
(* ValueNode : A string or number. *)
(* IdentifierNode : An expression consisting of a single symbol. *)
(* Also used to represent an operator argument of *)
(* a second-order operator. *)
(* OpDefOrDeclNode : An OpDefNode or an OpDeclNode. *)
(* ExprNode : An expression, which is an OppApplNode, a *)
(* LetInNode, a ValueNode, an IdentifierNode, *)
(* *)
(* Note: The SANY API apparently includes the following object types and *)
(* kinds not included as semantic nodes in this spec. Here is what they *)
(* correspond to in this spec: *)
(* *)
(* FormalParamNode object : Represented by a ConstantDeclNode. *)
(* *)
(* OpArgNode object : Represented by an IdentifierNode. *)
(* *)
(* For every kind xxxNode of semantic node, we define xxxNodeId to be the *)
(* set of node ids of nodes of kind xxxNode. We use the fact that a *)
(* semantic node has a kind field and an xxxNode object has kind field *)
(* equal to "xxxNode". *)
(***************************************************************************)
Ref(str) == {id \in NodeId: Node[id].kind = str}
ModuleNodeId == Ref("ModuleNode")
InstanceNodeId == Ref("InstanceNodeId")
OpDefNodeId == Ref("OpDefNode")
ConstantDeclNodeId == Ref("ConstantDeclNode")
VariableDeclNodeId == Ref("VariableDeclNode")
OpDeclNodeId == ConstantDeclNodeId \union VariableDeclNodeId
OpApplNodeId == Ref("OpApplNode")
SubstitutionNodeId == Ref("SubstitutionNode")
BoundSymbolNodeId == Ref("BoundSymbolNode")
LetInNodeId == Ref("LetInNode")
ValueNodeId == Ref("ValueNode")
IdentifierNodeId == Ref("IdentifierNode")
OpDefOrDeclNodeId == OpDefNodeId \union OpDeclNodeId
ExprNodeId == OpApplNodeId \union LetInNodeId \union ValueNodeId
\union IdentifierNodeId
--------------------------------------------------------------------------------
(**************************)
(* Level Data Structures *)
(**************************)
LevelValue == 0..3
(*************************************************************************)
(* The set of levels, where *)
(* 0 = constant *)
(* 1 = state function *)
(* 2 = action *)
(* 3 = temporal formula *)
(* (See Section 17.2 of "Specifying Systems".) *)
(*************************************************************************)
(***************************************************************************)
(* To understand level checking, consider the following definition. *)
(* *)
(* Foo(a, b, c) == a /\ ENABLED(b'=c) *)
(* *)
(* Since a level-2 expression cannot be primed and the argument of ENABLED *)
(* can have level at most 2, an expression Foo(exp1, exp2, exp3) is legal *)
(* iff the level of exp2 is at most 1 and the level of exp3 is at most 2. *)
(* An ENABLED expression has level equal to 1. (For simplicity, we *)
(* consider ENABLED (1=1), which is equivalent to TRUE, to have level 1.) *)
(* Hence, the expression Foo(exp1, exp2, exp3) has level equal to the *)
(* maximum of 1 and the level of a. *)
(* *)
(* We can describe the level properties of the operator Foo as follows, *)
(* where n is the semantic OpDefNode corresponding to the definition of *)
(* Foo. We define the level constraints on the arguments of Foo by *)
(* n.maxLevels, where n.maxLevels[i] is the maximum level of the i-th *)
(* argument of Foo. Thus, *)
(* *)
(* n.maxLevels[1] = 3 *)
(* n.maxLevels[2] = 1 *)
(* n.maxLevels[3] = 2 *)
(* *)
(* The level of Foo(exp1, exp2, exp3) is the maximum of 1 and the level of *)
(* exp1. We can express that by saying that it is the maximum of 1 and *)
(* the maximum of the set *)
(* *)
(* {1 * level of exp1, 0 * level of exp2, 0 * level of exp3} *)
(* *)
(* The level of an application of Foo is described by *)
(* *)
(* n.level = 1 *)
(* n.weights[1] = 1 *)
(* n.weights[2] = 0 *)
(* n.weights[3] = 0 *)
(* *)
(* This is all simple enough. Things get complicated for 2nd-order *)
(* operators, which are operators that take an operator as an *)
(* argument--for example *)
(* *)
(* Op2(A(_,_,_), b, c) == A(b, x', c) *)
(* *)
(* The expression Op2(Foo, exp2, exp3) is illegal, because it expands to *)
(* *)
(* Foo(exp2, x', exp3) *)
(* *)
(* and the second of argument of Foo can have level at most 1. In other *)
(* words, we cannot substitute Foo for the first argument of Op2 because *)
(* Foo.maxLevels[2] = 1 and the first argument of Op2 must be able to take *)
(* a second argument of level 2. In general, for an OpDefNode op *)
(* representing a definition of an operator Op, we let *)
(* op.minMaxLevel[i][k] be the minimum value of oparg.maxLevels[k] for the *)
(* i-th argument of Op. Thus, op.minMaxLevels[i] is a sequenced whose *)
(* length is the number of arguments taken by the i-th argument of Op. *)
(* (It equals 0 if the i-th argument of Op is not an operator argument.) *)
(* *)
(* An ideal level-checking algorithm would have the property that it *)
(* considers an expression to be level-correct iff expanding all defined *)
(* operators to obtain an expression that contains only built-in operators *)
(* yields a level-correct expression. The following example indicates the *)
(* complexity of an ideal algorithm that doesn't actually do the *)
(* expansion. *)
(* *)
(* Bar(Op1(_,_)) == Op1(x', x)' *)
(* *)
(* The expression Bar(A) is level-correct iff A is an operator whose level *)
(* does not depend on the level of its first argument--that is, iff *)
(* a.weight[1]=0. To simplify the bookkeeping, we make the conservative *)
(* assumption that any operator parameter may be instantiated with an *)
(* operator whose level depends on the levels of all its arguments. Thus, *)
(* we will disallow this definition of Bar. We will do this even if the *)
(* definition occurs within a LET and we could check that all the actual *)
(* instances of Bar result in level-correct expressions. I can't think of *)
(* any reasonable case where this will disallow a level-correct expression *)
(* that a user is likely to write. *)
(* *)
(* The decision to simplify the bookkeeping results in the following, *)
(* somewhat less unlikely problem. With the definitions *)
(* *)
(* ApplyToPrime(Op(_)) == Op(x') *)
(* EqualsNoPrime(a) == x *)
(* *)
(* the expression ApplyToPrime(EqualsNoPrime)' , which equals x', is *)
(* considered to be illegal. This is because the algorithm to compute the *)
(* level makes the assumption that ApplyToPrime will always be applied to *)
(* operators Op for which the level of Op(exp) depends on the level of *)
(* exp. Hence, SANY's algorithm gives ApplyToPrime(Op) a level of at *)
(* least 2 (primed expression) for any operator Op. A slightly more *)
(* realistic example can be constructed by modifying ApplyToPrime a bit *)
(* and applying it to ENABLED. *)
(* TLC warns users about this bug if it reports an invariant to be *)
(* level-incorrect in tlc2.tool.Spec.processConfigInvariants() with error *)
(* code tlc2.output.EC.TLC_INVARIANT_VIOLATED_LEVEL. *)
(* A corresponding test can be found in test52. Its invariant "Invariant" *)
(* covers the ENABLED scenario. However, the invariant remains disabled *)
(* for as long as this bug is open. The invariant Invariant can be *)
(* re-enabled in test52.cfg once this bug is closed. *)
(* *)
(* To compute the values of op.level, op.weights, and op.minMaxLevel for *)
(* an OpDefNode op corresponding to a definition, a level-checking *)
(* algorithm needs to keep track of the constraints on its formal *)
(* parameters implied by the subexpressions of the definition's body, as *)
(* well has how the level of the body depends on the levels of its *)
(* parameters. For our less than ideal level-checking algorithm, this is *)
(* done by keeping track of sets of objects of the following types. *)
(***************************************************************************)
LevelConstraint == [param: ConstantDeclNodeId, level: LevelValue]
(*************************************************************************)
(* A level constraint lc indicates that the parameter with id lc.param *)
(* can be instantiated only with an expression of level at most *)
(* lc.level. *)
(*************************************************************************)
ArgLevelConstraint ==
(*************************************************************************)
(* An arg-level constraint alc indicates that the operator parameter *)
(* with id alc.param can be instantiated with an operator op only if the *)
(* alc.idx-th argument of op can have level at least alc.level. This *)
(* constraint is vacuous iff alc.level = 0. *)
(*************************************************************************)
[param: ConstantDeclNodeId, idx: Nat \ {0}, level: LevelValue]
ArgLevelParam ==
(*************************************************************************)
(* An arg-level parameter alp indicates that the parameter with id *)
(* alp.param appears in the alp.idx-th argument of the operator with id *)
(* alp.op. *)
(*************************************************************************)
[op: NodeId, idx: Nat \ {0}, param: NodeId]
(***************************************************************************)
(* For later use, we define the following two operators on these data *)
(* types. *)
(***************************************************************************)
MinLevelConstraint(id, LC) ==
(*************************************************************************)
(* If LC is a set of level constraints and id a ConstantDeclNodeId, then *)
(* this equals the minimum level constraint on id implied by the *)
(* elements of LC. (This is 3 if there is none.) *)
(*************************************************************************)
IF \E lc \in LC: lc.param = id
THEN LET minLC == CHOOSE lc \in LC:
/\ lc.param = id
/\ \A olc \in LC:
(olc.param = id) => (olc.level >= lc.level)
IN minLC.level
ELSE 3
MaxArgLevelConstraints(id, ALC) ==
(*************************************************************************)
(* If ALC is a set of arg-level constraints and id a ConstantDeclNodeId, *)
(* then this equals the tuple <<lev_1, ..., lev_n>>, where n is the *)
(* number of arguments taken by the operator parameter op represented by *)
(* node id, such that the arg-level constraints in ALC imply that op *)
(* must be able to take an i-th operator of level at least lev_i, for *)
(* each i. *)
(*************************************************************************)
LET n == Node[id].numberOfArgs
minALC(i) ==
LET isALC(lc) == (lc.param = id) /\ (lc.idx = i)
IN IF \E lc \in ALC: isALC(lc)
THEN LET max == CHOOSE lc \in ALC:
/\ isALC(lc)
/\ \A olc \in ALC:
isALC(olc) => (olc.level <= lc.level)
IN max.level
ELSE 0
IN [i \in 1..n |-> minALC(i)]
LevelConstraintFields ==
(*************************************************************************)
(* A record whose fields consist of fields used for level computations. *)
(* These fields are common to all semantic nodes of type Expr that *)
(* represent expressions, as well as to all OpDef nodes, which represent *)
(* operator definitions. Some of these fields also occur in other *)
(* nodes--like Instance and Module nodes. *)
(* *)
(* In general, an expression will be in the scope of some formal *)
(* parameters, so its level will depend on the level of the expressions *)
(* substituted for some of those parameters. For example, if p and q *)
(* are formal parameters, and x is a declared variable, then the level *)
(* of the expression *)
(* *)
(* ENABLED(p' = x) /\ q *)
(* *)
(* is the maximum of 1 (the level of the ENABLED expression) and the *)
(* level of q. For the ExprNode e that represents this expression, *)
(* e.level equals 1 and e.levelParams is the set whose single element is *)
(* the (id of the) ConstantDeclNode for q. Here's a description *)
(* of the level fields, where the parameter set of e is the set of all *)
(* parameters (formal definition parameters or declared constants) such *)
(* that e appears in the scope of their declarations. *)
(* *)
(* e.level: A level value. If all the parameters appearing in e *)
(* were instantiated with constants, then e.level would be *)
(* the level of the resulting expression. *)
(* *)
(* e.levelParams : A set of parameters from the parameter set of e. *)
(* You can think of these in two equivalent ways: *)
(* - They are the parameters whose levels contribute to the *)
(* level of e. *)
(* - They are the parameters appearing in e that would get *)
(* primed if expression e were primed. *)
(* An element of e.levelParams is called a LEVEL PARAMETER of e. *)
(* *)
(* e.levelConstraints : A set of level constraints, in which *)
(* all the parameters that appear belong to the parameter set *)
(* of e. *)
(* *)
(* e.argLevelConstraints : A set of arg-level constraints, in which *)
(* all the parameters that appear are (operator) parameters of *)
(* the parameter set of e. *)
(* *)
(* e.argLevelParams : A set of arg-level parameters. *)
(* An element alp indicates that there is a subexpression of e *)
(* (or of its definition, if e is a defined operator) *)
(* of the form alp.op(... ), where alp.param is a *)
(* level parameter of the alp.idx-th argument. *)
(* NOTE: For an OpDefNode op, op.argLevelParams can contain *)
(* elements alp with alp.op and/or alp.param (but not both) *)
(* being formal parameters of the definition. This will *)
(* happen if the definition contains a subexpression Op(arg) *)
(* where either Op is a formal parameter or arg contains a *)
(* formal parameter. (These elements are used for level-checking *)
(* an instantiated version of the definition obtained by an *)
(* INSTANCE statement.) *)
(* *)
(* In the computation, we don't bother eliminating redundant elements *)
(* from these sets. For example, a level constraint lc is redundant if *)
(* there is another level constraint lco such that lco.param = lc.param *)
(* and lco.level < lc.level. A more efficient algorithm would eliminate *)
(* the redundant elements from e.levelConstraints and *)
(* e.argLevelConstraints. *)
(*************************************************************************)
[levelParams: SUBSET ConstantDeclNodeId,
levelConstraints: SUBSET LevelConstraint,
argLevelConstraints: SUBSET ArgLevelConstraint,
argLevelParams: SUBSET ArgLevelParam]
--------------------------------------------------------------------------------
(***************************************************************************)
(* Definitions of the Semantic Nodes *)
(* *)
(* A fair amount of information not relevant to level checking, but *)
(* present in the SANY api, has been eliminated from these definitions of *)
(* the semantic node types. For example, some sequences have been changed *)
(* to sets where their order of occurrence is not relevant to level *)
(* checking (but is relevant to correctness of the module). *)
(***************************************************************************)
ModuleNode ==
(*************************************************************************)
(* A semantic node representing a module. *)
(*************************************************************************)
[kind: {"ModuleNode"},
isConstant: BOOLEAN ,
(**********************************************************************)
(* True iff this is a constant module. A constant module is one with *)
(* no VARIABLE declarations and no non-constant operators. We won't *)
(* bother defining this precisely. *)
(* *)
(* Note: In TLA+, the only way to define a constant operator that *)
(* contains a non-constant subexpression is by throwing the *)
(* subexpression away--for example: *)
(* *)
(* Foo(a) == LET Bar(b, c) == b *)
(* IN Bar(a, x') *)
(* *)
(* which is a silly way to write Foo(a) == a. It would thus be safe *)
(* to define a constant module to be one with no declared variables *)
(* and in which all definitions and theorems have level 0. This *)
(* would allow a constant module to have the silly definition above *)
(* of Foo (assuming x is not a declared variable). However, the *)
(* official definition of a constant module prohibits it from having *)
(* definitions like the one above for Foo. *)
(**********************************************************************)
opDecls: SUBSET OpDeclNodeId,
(**********************************************************************)
(* The set declared constants and variables. *)
(**********************************************************************)
opDefs: SUBSET OpDefNodeId,
(***********************************************************************)
(* The top-level operator definitions (ones not defined inside LET's) *)
(* in this module--including definitions incorporated from extended *)
(* and instantiated modules. It includes function definitions *)
(* (definitions of the form f[x \in S] == e) and all definitions *)
(* introduced into the module by module instantiations. (A module *)
(* instantiation creates a new OpDefNode for each OpDefNode in the *)
(* instantiated module.) *)
(***********************************************************************)
instances: SUBSET InstanceNodeId,
(**********************************************************************)
(* The top-level INSTANCEs (ones not defined inside LET's) in this *)
(* module. *)
(**********************************************************************)
innerModules: SUBSET ModuleNodeId,
(**********************************************************************)
(* The top-level submodules that appear in this module. *)
(**********************************************************************)
theorems: SUBSET ExprNodeId,
assumes: SUBSET ExprNodeId,
(**********************************************************************)
(* In this representation, a theorem or assumption node points to an *)
(* ExprNode. *)
(**********************************************************************)
levelConstraints: SUBSET LevelConstraint,
argLevelConstraints: SUBSET ArgLevelConstraint,
argLevelParams: SUBSET ArgLevelParam]
(**********************************************************************)
(* The meanings of these sets of constraints are described with the *)
(* definitions of the constraint data types. The parameters that *)
(* appear in them are the declared constants and variables of the *)
(* module. These constraints are used to check the legality of *)
(* instantiation if this is a constant module. For a non-constant *)
(* module, these fields are not needed, because declared constant *)
(* operators can be instantiated only with constant operators. For a *)
(* constant module, the levelConstraints and argLevelConstraints *)
(* fields reflect only constraints that prevent constants from being *)
(* instantiated with temporal (level 3) formulas. *)
(* *)
(* The MaxLevels method of the api is defined in terms of *)
(* levelConstraints as follows. If id is the NodeId of the i-th *)
(* declared constant, and mod is the ModuleNodeId, then *)
(* *)
(* MaxLevels(i) = *)
(* IF mod.constantModule *)
(* THEN MinLevelConstraint(id, mod.levelConstraints) *)
(* ELSE 0 *)
(**********************************************************************)
OpDefOrDeclNodeFields ==
(*************************************************************************)
(* This defines the fields that are common to the OpDeclNode and *)
(* OpDefNode types. *)
(*************************************************************************)
[name: STRING ,
(**********************************************************************)
(* The name of the operator. (This isn't used in the level *)
(* computation, but it's convenient for keeping track of things when *)
(* running tests of the spec with TLC.) *)
(**********************************************************************)
numberOfArgs: Nat,
(**********************************************************************)
(* The number of arguments of the operator. Operators that can take *)
(* an arbitrary number of arguments are represented by an infinite *)
(* sequence of definitions, one for each possible number of *)
(* arguments. For example, we pretend that there is a sequence of *)
(* operators Tuple0, Tuple1, Tuple2, ... such that <<a, b>> is *)
(* represented as Tuple2(a, b). *)
(**********************************************************************)
level: LevelValue]
(**********************************************************************)
(* For an OpDeclNode op, the value of op.level is 0 except for one *)
(* representing a variable declaration, for which op.level equals 1. *)
(* *)
(* The meaning of op.level for an OpDefNode is described above. *)
(**********************************************************************)
OpDeclNode ==
(*************************************************************************)
(* Represents a declared constant or variable. *)
(*************************************************************************)
RecordCombine([kind: {"ConstantDeclNode", "VariableDeclNode"}],
OpDefOrDeclNodeFields)
OpDefNode ==
(*************************************************************************)
(* Represents a definition, for example the definition of the symbol Foo *)
(* in Foo(A, B) == expr. We also assume imaginary definitions of *)
(* built-in symbols. Unlike in the actual SANY api, we represent a *)
(* construction like {exp : x \in S, y \in T} as something like *)
(* SetCons3(exp, S, T), where SetCons3 is an imaginary operator that *)
(* takes three arguments. (As remarked above, we pretend that every *)
(* operator has a fixed number of arguments, so we pretend that there is *)
(* also a separate OpDefNode for the operator SetCons4 used to represent *)
(* the construction {exp : x \in S, y \in T, z \in U}. *)
(* *)
(* As indicated by the formal semantics, a function definition *)
(* *)
(* f[x \in S] == e *)
(* *)
(* is treated like the definition *)
(* *)
(* f == CHOOSE f : f = [x \in S |-> e] *)
(* *)
(* The level-constraint fields of the OpDefNode for an operator Op *)
(* reflects all the constraints implied by the body of the definition of *)
(* Op for the parameters within whose scope the definition appears. *)
(* However, the argLevelParams field may contain arg-level parameters *)
(* whose op or param field (but not both) is a formal parameter of the *)
(* definition. For example, consider *)
(* *)
(* A(Op(_)) == LET B(c) == Op(c) *)
(* IN B(x') *)
(* *)
(* then the fact that the formal parameter c of B appears in the *)
(* definition of B in the argument of Op tells us that the expression *)
(* B(x') in the definition of A implies that A can be used only with a *)
(* first argument that can take an argument of level 2. This is *)
(* recorded by the arg-level parameter *)
(* *)
(* [op |-> Op, idx |-> 1, param |-> c] *)
(* *)
(* in B.argLevelParams. *)
(*************************************************************************)
RecordCombine(
[kind: {"OpDefNode"},
params: Seq(ConstantDeclNodeId),
(********************************************************************)
(* The formal parameters of the definition. *)
(********************************************************************)
maxLevels: Seq(LevelValue),
weights: Seq({0, 1}),
minMaxLevel: Seq(Seq(LevelValue)),
opLevelCond: Seq(Seq(Seq( BOOLEAN ))),
(********************************************************************)
(* All these fields are described above, except for opLevelCond. *)
(* For an OpDefNode op, op.opLevelCond[i][j][k] is true iff the *)
(* i-th argument of op is an operator argument opArg, and the *)
(* definition of op contains an expression in which the j-th formal *)
(* parameter of the definition of op appears within the k-th *)
(* argument of opArg. As we'll see, this information is needed for *)
(* keeping track of level constraints. *)
(********************************************************************)
body: ExprNodeId \union {Null},
(********************************************************************)
(* The body of the definition. For a built-in operator, it's Null. *)
(********************************************************************)
substitution: SubstitutionNodeId],
(********************************************************************)
(* Suppose that a module M contains the definition *)
(* *)
(* Op(p, q) == expr *)
(* *)
(* and let mOp be the corresponding OpDef node for operator Op. *)
(* Next suppose that another module N contains *)
(* *)
(* MI(x) == INSTANCE M WITH A <- x+1, B <- x*r *)
(* *)
(* This adds to module N the operator MI!Op such that *)
(* *)
(* MI!Op(x, p, q) == Iexpr *)
(* *)
(* where Iexpr is the expression obtained from expr by substituting *)
(* x+1 for A and x*r for B. (In TLA+ we write *)
(* MI(exp1)!Op(exp2,exp3), but this is just syntax; MI!Op is an *)
(* operator that takes 3 arguments.) The INSTANCE statement adds *)
(* to the semantic tree for module N a UserOpDef node miOp for the *)
(* operator MI!Op such that *)
(* *)
(* miOp.name = "MI!Op", *)
(* miOp.numberOfArgs = 3 *)
(* miOp.params[1] = a ref to a ConstantDeclNode for x *)
(* miOp.params[2] = mOp.params[1] *)
(* miOp.params[3] = mOp.params[2] *)
(* miOp.body = mOp.body *)
(* miOp.substitution = a SubstitutionNode representing *)
(* A <- x+1, B <- x*r *)
(* *)
(* For convenience, if Op does not come from an instantiated *)
(* module, we let the substitution field point to a null *)
(* substitution--that is, one whose subFor and subWith fields are *)
(* the empty sequence. *)
(********************************************************************)
RecordCombine(OpDefOrDeclNodeFields, LevelConstraintFields))
InstanceNode ==
(*************************************************************************)
(* Represents a statement of the form *)
(* *)
(* I(param[1], ... , param[p]) == *)
(* INSTANCE M WITH mparam[1] <- mexp[1], ... , mparam[r] <- mexp[r] *)
(* *)
(* or simply *)
(* *)
(* INSTANCE M WITH mparam[1] <- mexp[1], ... , mparam[r] <- mexp[r] *)
(* *)
(* The mparam[i] are assumed to be all the declared constants and *)
(* variables of M. (That is, implicit substitutions of the form *)
(* param <- param are made explicit.) *)
(*************************************************************************)
[kind: {"InstanceNode"},
module: ModuleNodeId,
(********************************************************************)
(* The instantiated module. *)
(********************************************************************)
params: Seq(ConstantDeclNodeId),
(********************************************************************)
(* The formal parameters of the definition. *)
(********************************************************************)
substitution: SubstitutionNodeId,
(********************************************************************)
(* The substitution. If M has no parameters, then this is the null *)
(* substitution with subFor and subWith fields equal to the empty *)
(* sequence. *)
(********************************************************************)
numberOfArgs: Nat,
levelConstraints: SUBSET LevelConstraint,
argLevelConstraints: SUBSET ArgLevelConstraint,
argLevelParams: SUBSET ArgLevelParam]
(**********************************************************************)
(* The level constraints obtained from the instantiation. (There are *)
(* no level parameters for the InstanceNode itself.) *)
(**********************************************************************)
OpDefOrDeclNode == OpDefNode \union OpDeclNode
OpApplNode ==
(*************************************************************************)
(* An OppApplNode represents an operator application. Examples of *)
(* expressions that such a node can represent are: *)
(* *)
(* A \cup B which we think of as \cup(A, B) *)
(* *)
(* (x + y) * (b + c) which we think of as *(+(x,y), +(b,c)) *)
(* *)
(* \E x, y \in S, <<u, v>> \in T : (x+y) > (u+v) which we think of *)
(* here as something like: *)
(* *)
(* \E(S, T, >(+(x,y), +(u,v))) *)
(* *)
(* plus the declarations of x, y, u, and v. (The OpApplNode in the *)
(* actual API maintains the actual structure of the expression, *)
(* Here, we don't bother to distinguish \E x, y, z \in S : P *)
(* from \E <<x, y, z>> \in S : P *)
(*************************************************************************)
RecordCombine(
[kind: {"OpApplNode"},
operator: OpDefOrDeclNodeId,
(********************************************************************)
(* The (id of the) OpDefOrDecl node of the operator. *)
(********************************************************************)
args: Seq(ExprNodeId) \ {<<>>},
(********************************************************************)
(* An OpApplNode has a nonempty sequence of arguments. *)
(********************************************************************)
quantSymbols: SUBSET BoundSymbolNodeId,
(********************************************************************)
(* The bound symbols introduced by the operator application. *)
(********************************************************************)
level: LevelValue],
LevelConstraintFields)
SubstitutionNode ==
(*************************************************************************)
(* The Substitution object s that represents the WITH clause *)
(* *)
(* A <- x+1, B <- x*r *)
(* *)
(* has Len(s.subFor) = Len(s.subWith) = 2 and *)
(* *)
(* s.subFor[1] = the id of the ConstantDecl or VariableDecl *)
(* node for A *)
(* s.subFor[2] = the id of the ConstantDecl or VariableDecl *)
(* node for B *)
(* s.subWith[1] = the id of the ExprNode for x+1 *)
(* s.subWith[2] = the id of the ExprNode for x*r *)
(* *)
(* Note that the nodes referenced in subFor are in the semantic *)
(* tree for the instantiated module, while those referenced in *)
(* subWith are in the semantic tree for the instantiating module. *)
(*************************************************************************)
[kind: {"SubstitutionNode"},
subFor: Seq(OpDeclNodeId),
subWith: Seq(ExprNodeId)]
IdentifierNode ==
(************************************************************************)
(* An IdentifierNode is an ExprNode with a ref field. It represents an *)
(* expression that consists of a single symbol. For example, the *)
(* OppApplNode that represents the expression A * (b + c) will have as *)
(* its list of arguments the subexpressions A and b+c. The *)
(* subexpression A will be an IdentifierNode whose ref field returns *)
(* the OpDefOrDeclNode that declares or defines A. *)
(************************************************************************)
RecordCombine(
[kind: {"IdentifierNode"},
ref: OpDefOrDeclNodeId \union BoundSymbolNodeId,
level: LevelValue],
LevelConstraintFields)
BoundSymbolNode ==
(*************************************************************************)
(* Represents a bounded identifier, like the x in {x \in S : x > 0}. It *)
(* has level 0 except for the bounded symbols introduced by \EE and \AA, *)
(* which have level 1. *)
(*************************************************************************)
[kind: {"BoundSymbolNode"},
name: STRING ,
level: {0, 1}]
LetInNode ==
(*************************************************************************)
(* This node represents a LET expression, for example *)
(* *)
(* LET Foo(a) == a + x *)
(* Bar == Foo(a) + a *)
(* IN body *)
(*************************************************************************)
RecordCombine(
[kind: {"LetInNode"},
opDefs: SUBSET OpDefNodeId,
instances: SUBSET InstanceNodeId,
(********************************************************************)
(* The LET definitions and INSTANCE statements. *)
(********************************************************************)
body: ExprNodeId,
level: LevelValue],
LevelConstraintFields)
ValueNode == RecordCombine(
(*************************************************************************)
(* This node type represents the NumeralNode, DecimalNode, and *)
(* StringNode, of the actual api. *)
(*************************************************************************)
[kind: {"ValueNode"},
level: {0}],
LevelConstraintFields)
ExprNode == OpApplNode \union LetInNode \union ValueNode \union IdentifierNode
SemNode ==
(*************************************************************************)
(* The type (set of all possible) semantic nodes. *)
(*************************************************************************)
ModuleNode \union OpDefOrDeclNode \union InstanceNode \union
ExprNode \union SubstitutionNode \union BoundSymbolNode
--------------------------------------------------------------------------------
(***************************************************************************)
(* "Type Correctness" *)
(***************************************************************************)
TypeOK ==
(*************************************************************************)
(* This expresses the basic type of Node, and also some relations among *)
(* the various fields of semantic nodes that aren't implied by the *)
(* simple data type definitions. *)
(*************************************************************************)
/\ Node \in [NodeId -> SemNode]
/\ \A id \in NodeId:
LET n == Node[id]
IN
/\ (n \in OpDefNode) =>
/\ Len(n.maxLevels) = n.numberOfArgs
/\ Len(n.weights) = n.numberOfArgs
/\ Len(n.params) = n.numberOfArgs
/\ Len(n.minMaxLevel) = n.numberOfArgs
/\ Len(n.opLevelCond) = n.numberOfArgs
/\ \A i \in 1..n.numberOfArgs:
/\ Len(n.minMaxLevel[i]) = Node[n.params[i]].numberOfArgs
/\ Len(n.opLevelCond[i]) = n.numberOfArgs
/\ \A j \in 1..n.numberOfArgs:
Len(n.opLevelCond[i][j]) =
Node[n.params[i]].numberOfArgs
/\ (n \in OpDeclNode) =>
/\ (n.kind = "ConstantDeclNode") => (n.level = 0)
/\ (n.kind = "VariableDeclNode") =>
/\ n.level = 1
/\ n.numberOfArgs = 0
/\ (n \in OpApplNode) =>
(Len(n.args) = Node[n.operator].numberOfArgs)
/\ (n \in SubstitutionNode) => (Len(n.subFor) = Len(n.subWith))
/\ (n \in InstanceNode) =>
/\ n.numberOfArgs = Len(n.params)
/\ (********************************************************)
(* There is a WITH substitution for every parameter of *)
(* the instantiated module. *)
(********************************************************)
LET mparamid ==
(**************************************************)
(* Defines the mparamid[i] to be the parameter *)
(* ids of the WITH clause. *)
(**************************************************)
[i \in 1..Len(Node[n.substitution].subFor) |->
Node[n.substitution].subFor[i]]
M == Node[n.module]
(*************************************************)
(* The ModuleNode of the instantiated module. *)
(*************************************************)
IN M.opDecls = {mparamid[i]: i \in 1..Len(mparamid)}
--------------------------------------------------------------------------------
(***************************************************************************)
(* Level Correctness Conditions *)
(* *)
(* Level checking is defined by the predicate LevelCorrect, which is a *)
(* correctness condition relating the level fields of a semantic node to *)
(* those of its children. From this condition, it's straightforward to *)
(* design a recursive procedure for computing those fields. The *)
(* conditions for each kind of node are defined separately, where the *)
(* predicate xxxNodeLevelCorrect(n) defines the correctness condition on a *)
(* node n of kind xxxNode. The following operators are used in the *)
(* definition of LevelCorrect. *)
(***************************************************************************)
IsOpArg(op, k) == Node[op.params[k]].numberOfArgs > 0
(*************************************************************************)
(* If op is an OpDefNode and k \in 1..op.numberOfArgs, then this is true *)
(* iff the k-th argument of op is an operator argument. *)
(*************************************************************************)
SubstituteInLevelConstraint(rcd, subst) ==
(*************************************************************************)
(* If rcd is a record containing level-constraint fields and subst is a *)
(* substitution, then this is the record consisting of the *)
(* level-constraint fields inferred from those of rcd by the *)
(* substitution. For example, if rcd is an ExprNode representing an *)
(* expression expr, then SubstituteInLevelConstraint(rcd, subst) is the *)
(* record of level constraints for the expression obtained from expr by *)
(* the substitution subst. *)
(*************************************************************************)
LET paramNums == 1..Len(subst.subFor)
(*******************************************************************)
(* The set of substitution parameter numbers. *)
(*******************************************************************)
ParamSubst(id) ==
(*******************************************************************)
(* The set of "substitute parameters" of the parameter whose *)
(* NodeId is id. If id is one of the parameters being substituted *)
(* for in subst, then this is the set of LevelParams of the *)
(* expression being substituted for it; otherwise, it equals {id}. *)
(*******************************************************************)
IF \E i \in paramNums: subst.subFor[i] = id
THEN LET subExpNum == CHOOSE i \in paramNums: subst.subFor[i] = id
IN Node[subst.subWith[subExpNum]].levelParams
ELSE {id}
IsOpParam(i) == Node[subst.subFor[i]].numberOfArgs > 0
(*******************************************************************)
(* True iff substitution parameter i is an operator parameter. *)
(*******************************************************************)
argNums == 1..Len(subst.subFor)
(*******************************************************************)
(* The set of parameter numbers. *)
(*******************************************************************)
SubOp(opid) ==
(*******************************************************************)
(* If opid is the NodeId of an operator parameter, then this *)
(* equals the NodeId of the operator with which this operator is *)
(* substituted for by subst, which is opid itself if subst does *)
(* not substitute for opid. *)
(*******************************************************************)
IF \E i \in paramNums: subst.subFor[i] = opid
THEN LET subExpNum ==
CHOOSE i \in paramNums: subst.subFor[i] = opid
IN Node[subst.subWith[subExpNum]].ref
ELSE opid
IN [levelParams |->
UNION {ParamSubst(id): id \in rcd.levelParams},
levelConstraints |->
(******************************************************************)
(* There are two kinds of level constraints obtained after *)
(* substitution: ones that come from rcd.levelConstraints via *)
(* substitution, and ones that come from elements alp in *)
(* rcd.argLevelParams because alp.op is a substitution parameter *)
(* replaced by a defined operator defOp, and *)
(* defOp.maxLevels[alp.idx] implies level constraints on some *)
(* parameter in the expression substituted for alp.param. *)
(******************************************************************)
LET Sub(lc) ==
(************************************************************)
(* If lc is a level constraint on a parameter param, then *)
(* this is the set of level constraints that implies *)
(* because param might be substituted for. *)
(************************************************************)
{[lc EXCEPT !.param = par]:
par \in ParamSubst(lc.param)}
ALP(i) ==
(************************************************************)
(* The set of arg-level parameters alp such that alp.op is *)
(* the substitution parameter i. *)
(************************************************************)
{alp \in rcd.argLevelParams: alp.op = subst.subFor[i]}
SubInALP(alp) ==
(*************************************************************)
(* The set of arg-level parameters obtained from arg-level *)
(* parameter alp by replacing alp.param with each of its *)
(* substitute parameters. *)
(*************************************************************)
{[alp EXCEPT !.param = par]:
par \in ParamSubst(alp.param)}
SubALP(i) == UNION {SubInALP(alp): alp \in ALP(i)}
(************************************************************)
(* The set of all SubInALP(alp) with alp in ALP(i). *)
(************************************************************)
LC(i, alp) ==
(************************************************************)
(* The level constraint implied by an element alp of *)
(* SubALP(i), if parameter i is an operator parameter *)
(* instantiated by a defined operator. *)
(************************************************************)
[param |-> alp.param,
level |->
Node[Node[subst.subWith[i]].ref].maxLevels[alp.idx]]
OpDefParams ==
{i \in paramNums:
/\ IsOpParam(i)
/\ Node[subst.subWith[i]].ref \in
OpDefNodeId}
IN UNION {Sub(lc): lc \in rcd.levelConstraints}
\union
UNION {{LC(i, alp): alp \in SubALP(i)}: i \in OpDefParams},
argLevelConstraints |->
(******************************************************************)
(* There are two kinds of arg-level constraints produced by the *)
(* substitution: ones obtained by substitution from *)
(* rcd.argLevelConstraints, and ones obtained as follows from an *)
(* element alp of rcd.argLevelParams. Since an operator *)
(* parameter can be instantiated only with an operator, *)
(* ParamSubst(alp.op) consists of a single operator op. If op is *)
(* a declared operator, and the subst substitutes expression exp *)
(* for alp.param, then op must be able to accept argument alp.idx *)
(* of level at least that of exp. (If there's no substitution *)
(* for alp.param, then it is a parameter that has level 0, so it *)
(* generates no non-trivial arg-level constraint.) *)
(******************************************************************)
LET Sub(alc) ==
(************************************************************)
(* The set of arg-level constraints that come from the *)
(* element alc. This set contains zero or one element. *)
(* Note that if subst.subFor[i] is an operator parameter, *)
(* then subst.subWith[i] is an IdentifierNodeId. *)
(************************************************************)
IF \E i \in 1..Len(subst.subFor): subst.subFor[i] = alc.param
THEN LET subExpNum ==
CHOOSE i \in argNums:
subst.subFor[i] = alc.param
IN IF Node[subst.subWith[subExpNum]].ref \in
OpDeclNodeId
THEN {[alc EXCEPT !.param =
Node[subst.subWith[subExpNum]].ref]}
ELSE {}
ELSE {alc}
SubParamALP(i) ==
(*************************************************************)
(* The set of elements alp of rcd.argLevelParams such that *)
(* alp.param is substitution parameter number i. *)
(*************************************************************)
{alp \in rcd.argLevelParams: alp.param = subst.subFor[i]}
ALC(alp, i) ==
(*************************************************************)
(* The set of arg-level constraints (containing 0 or one *)
(* constraint) implied by an arg-level constraint alp in *)
(* SubParamALP(i). Note that such an alp implies a *)
(* constraint iff SubOp(alp.op) is a declared (and not *)
(* defined) operator. *)
(*************************************************************)
IF SubOp(alp.op) \in OpDeclNodeId
THEN {[param |-> SubOp(alp.op),
idx |-> alp.idx,
level |-> Node[subst.subWith[i]].level]}
ELSE {}
ALCSet(i) == UNION {ALC(alp, i): alp \in SubParamALP(i)}
(*************************************************************)
(* The set of all level constraints implied by elements of *)
(* SubParamALP(i). *)
(*************************************************************)
IN UNION {Sub(alc): alc \in rcd.argLevelConstraints}
\union
UNION {ALCSet(i): i \in paramNums},
argLevelParams |->
(******************************************************************)
(* The set of arg-level parameters implied by rcd.argLevelParams *)
(* after performing the substitution. If arg-level parameter alp *)
(* indicates that the parameter with index pId occurs in the j-th *)
(* argument of opParam, then the substitution implies that any *)
(* element of ParamSubst(pId) occurs in the j-th argument of the *)
(* operator with which opParam is replaced by the substitution *)
(* (which may be itself). If opParam is replaced by a defined *)
(* operator (and not a declared one), then this produces a *)
(* legality condition on the substitution, rather than a new *)
(* arg-level parameter. *)
(******************************************************************)
LET Sub(alp) ==
(************************************************************)
(* The set of elements in SubArgLevelParams(ALP, subst) *)
(* that come from the element alp. *)
(************************************************************)
IF SubOp(alp.op) \in OpDeclNodeId
THEN {[alp EXCEPT !.op = SubOp(alp.op), !.param = pId]:
pId \in ParamSubst(alp.param)}
ELSE {}
IN UNION {Sub(alp): alp \in rcd.argLevelParams}]
ReducedLevelConstraint(rcd, paramSet) ==
(*************************************************************************)
(* If rcd is a record with level-constraint fields, then this is the *)
(* record obtained by removing from those level-constraint fields all *)
(* constraints on the parameters in paramSet. *)
(*************************************************************************)
[rcd EXCEPT
!.levelParams = @ \ paramSet,
!.levelConstraints = {lc \in @: lc.param \notin paramSet},
!.argLevelConstraints = {alc \in @: alc.param \notin paramSet},
!.argLevelParams = {alp \in @:
/\ alp.op \notin paramSet
/\ alp.param \notin paramSet}]
--------------------------------------------------------------------------------
(***************************************************************************)
(* The predicate LevelCorrect is defined in terms of the following *)
(* operators, which each define level-correctness for one kind of node. *)
(* In each definition, the first conjunct is the condition for the node to *)
(* be level-correct, unless there is a comment indicating that there is no *)
(* level-correctness condition for that kind of node. In all cases, *)
(* level-correctness of the child nodes is assumed when expressing *)
(* level-correctness of a node. *)
(***************************************************************************)
ModuleNodeLevelCorrect(n) ==
(*************************************************************************)
(* We assume n is a ModuleNode. It is level-correct iff all the *)
(* definitions, instances, theorems, and assumes are, and all the *)
(* assumes have level 0. *)
(* *)
(* The level constraints come from the level constraints of the *)
(* definitions, instances, theorems, and assumes in the obvious way. *)
(*************************************************************************)
LET defParams(opid) ==
(*******************************************************************)
(* The set of node ids of the formal parameter of the definition *)
(* represented by the node with id opid. *)
(*******************************************************************)
{Node[opid].params[i]: i \in 1..Node[opid].numberOfArgs}
nonDefs == n.instances \union n.theorems \union n.assumes
(*******************************************************************)
(* All nodes contributing to the level constraints other than *)
(* OpDef nodes. *)
(*******************************************************************)
allDefs == n.opDefs \union nonDefs
IN
/\ (******************************************************************)
(* Level correctness. *)
(******************************************************************)
\A id \in n.assumes: Node[id].level = 0
/\ n.levelConstraints =
UNION {Node[opid].levelConstraints: opid \in allDefs}
/\ n.argLevelConstraints =
UNION {Node[opid].argLevelConstraints: opid \in allDefs}
/\ n.argLevelParams =
(****************************************************************)
(* We must remove the constraints on formal parameters of the *)
(* definitions. *)
(****************************************************************)
(UNION {ReducedLevelConstraint(
Node[opid],
defParams(opid)).argLevelParams:
opid \in n.opDefs})
\union
UNION {Node[opid].argLevelParams: opid \in nonDefs}
InstanceNodeLevelCorrect(n) ==
(*************************************************************************)
(* We assume n is an InstanceNode representing *)
(* *)
(* I(param[1], ... , param[p]) == *)
(* INSTANCE M WITH mparam[1] <- mexp[1], ... , mparam[r] <- mexp[r] *)
(*************************************************************************)
LET r == Len(Node[n.substitution].subWith)
mexp == [i \in 1..r |-> Node[Node[n.substitution].subWith[i]]]
(*******************************************************************)
(* mexp[i] is an Expr node. *)
(*******************************************************************)
paramIds == {n.params[i]: i \in 1..n.numberOfArgs}
(*******************************************************************)
(* The set of node ids {param[1], ... , param[p]}. *)
(*******************************************************************)
redMexp ==
(*******************************************************************)
(* Defines redMexp[i] to be the record that's the same as mexp[i] *)
(* except with all constraints on the param[i] removed. *)
(*******************************************************************)
[i \in 1..r |-> ReducedLevelConstraint(mexp[i], paramIds)]
M == Node[n.module]
(*******************************************************************)
(* M is the ModuleNode of the instantiated module. *)
(*******************************************************************)
mparamId == [i \in 1..r |-> Node[n.substitution].subFor[i]]
(*******************************************************************)
(* Defines mparamId[i] to be the NodeId for mparam[i]. *)
(*******************************************************************)
mparam == [i \in 1..r |-> Node[mparamId[i]]]
(*******************************************************************)
(* Defines mparam[i] to be the OpDeclNode for this parameter of M. *)
(*******************************************************************)
mOpArg(i) == Node[mexp[i].ref]
(*******************************************************************)
(* If mparam[i] is an operator argument, then mexp[i] is an *)
(* Identifier node for the OpDefOrDeclNode mOpArg(i). *)
(*******************************************************************)
subst == Node[n.substitution]
(*******************************************************************)
(* The substitution node. *)
(*******************************************************************)
MSubConstraints ==
(*******************************************************************)
(* A record consisting of the constraints obtained from M after *)
(* performing the substitutions. The level parameters of M are *)
(* its declared constants. *)
(*******************************************************************)
SubstituteInLevelConstraint(
[levelParams |-> {op \in M.opDecls: Node[op].level = 0},
levelConstraints |-> M.levelConstraints,
argLevelConstraints |-> M.argLevelConstraints,
argLevelParams |-> M.argLevelParams],
subst)
redMSubConstraints ==
(*******************************************************************)
(* The constraint record MSubConstraints with the constraints on *)
(* the param[i] removed. *)
(*******************************************************************)
ReducedLevelConstraint(MSubConstraints, paramIds)
IN (*********************************************************************)
(* There are four level-correctness requirements on the *)
(* instantiation. The first applies to nonconstant modules. The *)
(* last three come from the level constraints of M. These three *)
(* requirements are trivially implied by the first requirement if M *)
(* is a nonconstant module, so they apply only when M is a constant *)
(* module. *)
(*********************************************************************)
/\ (******************************************************************)
(* If M is a nonconstant module, then declared constants of M can *)
(* be instantiated only with constant expressions, and the *)
(* declared variables only with expressions of level 1. *)
(******************************************************************)
~M.isConstant =>
\A i \in 1..r: mexp[i].level <= mparam[i].level
/\ (******************************************************************)
(* A level-constraint on mparam[i] implies a condition on *)
(* mexp[i]. *)
(******************************************************************)
\A i \in 1..r:
mexp[i].level <=
MinLevelConstraint(mparamId[i], M.levelConstraints)
/\ (******************************************************************)
(* If mexp[i] is a defined operator argument, then an arg-level *)
(* constraint on mparam[i] implies a condition on mexp[i]. *)
(******************************************************************)
\A i \in 1..r:
/\ mparam[i].numberOfArgs > 0
/\ mOpArg(i) \in OpDefNode
(***************************************************************)
(* IF param[i] is an operator argument and mexp[i] is a *)
(* defined operator, *)
(***************************************************************)
=> (************************************************************)
(* THEN the operator mexp[i] must satisfy the arg-level *)
(* constraints on param[i]. *)
(************************************************************)
\A j \in 1..mOpArg(i).numberOfArgs:
mOpArg(i).maxLevels[j] >=
MaxArgLevelConstraints(mparamId[i],
M.argLevelConstraints)[j]
/\ (******************************************************************)
(* An arg-level parameter of M asserting that param[j] appears in *)
(* an argument of operator parameter param[i], where mexp[i] is a *)
(* defined operator, implies a condition relating mexp[i] and *)
(* mexp[j]. *)
(******************************************************************)
\A alp \in M.argLevelParams:
\A i, j \in 1..r:
/\ alp.op = mparamId[i]
/\ alp.param = mparamId[j]
/\ mOpArg(i) \in OpDefNode
=> (mexp[j].level <= mOpArg(i).maxLevels[alp.idx])
(*********************************************************************)
(* The level constraints for InstanceNode n are the ones that come *)
(* from performing the substitution in the level constraints of M *)
(* and from the mexp[i], except with constraints on the param[j] *)
(* removed. *)
(*********************************************************************)
/\ n.levelConstraints =
redMSubConstraints.levelConstraints \union
UNION {redMexp[i].levelConstraints: i \in 1..r}
/\ n.argLevelConstraints =
redMSubConstraints.argLevelConstraints \union
UNION {redMexp[i].argLevelConstraints: i \in 1..r}
/\ n.argLevelParams =
redMSubConstraints.argLevelParams \union
UNION {redMexp[i].argLevelParams: i \in 1..r}
OpDefNodeLevelCorrect(n) ==
(*************************************************************************)
(* We assume that n is an OpDefNode that is represents the definition of *)
(* Op(param[1], ... , param[p]) == exp *)
(* *)
(* Note that this definition may have been imported from a statement *)
(* *)
(* Inst(param[1], ... , param[q]) == *)
(* INSTANCE M with *)
(* WITH mparam[1] <- mexp[1], ... , mparam[r] <- mexp[r] *)
(* *)
(* where Op is Inst!MOp. In this case, we let exp be the body of the *)
(* definition of MOp, and subst be the substitution node of the INSTANCE *)
(* statement. We let subExp be the expression obtained by performing *)
(* the substitution. We never explicitly compute subExp. However, we *)
(* do compute some of the level constraints that subExp implies. *)
(* *)
(* Level-correctness of the substitutions, as well as constraints *)
(* imposed by the substitutions on the parameters within whose scope the *)
(* INSTANCE statement appears, are handled by the correctness condition *)
(* on the INSTANCE statement. However, the constraints implied by the *)
(* substitutions on the param[i] can yield constraints on the definition *)
(* of Op. *)
(* *)
(* We consider the ordinary (non-instantiated definition) case to be the *)
(* special case of an instantiated definition with a null substitution. *)
(* *)
(* The definition is level-correct iff expression exp is. *)
(*************************************************************************)
LET p == n.numberOfArgs
param == n.params
paramIds == {param[i]: i \in 1..p}
(*******************************************************************)
(* The set of ids of the formal parameters param[i]. *)
(*******************************************************************)
exp == Node[n.body]
(*******************************************************************)
(* The ExprNode representing the body of the definition. *)
(*******************************************************************)
subst == Node[n.substitution]
r == Len(Node[n.substitution].subWith)
iParamIds == {param[i]: i \in 1..r}
(*******************************************************************)
(* The set of param[i] that come from the INSTANCE. *)
(*******************************************************************)
mparamId == Node[n.substitution].subFor
(*******************************************************************)
(* mparamId[i] is the NodeId of mparam[i]. *)
(*******************************************************************)
mexp == [i \in 1..r |-> Node[Node[n.substitution].subWith[i]]]
(*******************************************************************)
(* mexp[i] is the ExprNode of the i-th WITH expression. *)
(*******************************************************************)
subExp == SubstituteInLevelConstraint(exp, subst)
(*******************************************************************)
(* This is a record containing the level-constraint fields for the *)
(* expression subExp, obtained by performing the substitution *)
(* subst on exp. (We do things in this way so that, if you want *)
(* to ignore the substitution and understand just how things work *)
(* for an ordinary definition, you can just replace subExp with *)
(* exp. Of course, for the null substitution, these fields are *)
(* the same as the corresponding fields of exp.) *)
(*******************************************************************)
IN
/\ n.level =
(****************************************************************)
(* The level of Op is the maximum of *)
(* - The level of exp, and *)
(* - The levels of all mexp[i] such that mparam[i] *)
(* contributes to the level of exp. *)
(****************************************************************)
LET pLevel(i) == IF mparamId[i] \in subExp.levelParams
THEN mexp[i].level
ELSE 0
IN NumMax(exp.level, SetMax({pLevel(i): i \in 1..r}))
/\ n.maxLevels =
(****************************************************************)
(* n.maxLevels[i] is determined by the level constraints on *)
(* param[i] that come from subExp and from the mexp[j]. (The *)
(* latter constraints can only be on param[i] with i \leq q.) *)
(* This is conservative, because it can imply a constraint on *)
(* an INSTANCE parameter (a param[i] with i \leq q) even if *)
(* that parameter doesn't appear in subExp. However, we are *)
(* not keeping enough information to be more liberal, because *)
(* an appearance of that parameter in subExp would imply the *)
(* constraint, even if that appearance doesn't contribute to *)
(* the level of subExp (and hence the parameter doesn't occur *)
(* in subExp.levelParams). *)
(****************************************************************)
[i \in 1..p |->
MinLevelConstraint(
param[i],
subExp.levelConstraints \union
UNION {mexp[j].levelConstraints: j \in 1..r})]
/\ n.weights =
(****************************************************************)
(* n.weights[i] is 1 iff param[i] is a level parameter of *)
(* subExp. *)
(****************************************************************)
[i \in 1..p |-> IF param[i] \in subExp.levelParams THEN 1 ELSE 0]
/\ n.minMaxLevel =
(****************************************************************)
(* n.minMaxLevel[i] is deduced from the arg-level constraints *)
(* on param[i] obtained from subExp and (for i \leq r) from the *)
(* mexp[j]. As with n.maxLevels, this is conservative, *)
(* essentially assuming that any INSTANCE parameter could *)
(* appear in subExp. *)
(****************************************************************)
[i \in 1..p |->
MaxArgLevelConstraints(
param[i],
subExp.argLevelConstraints \union
UNION {mexp[j].argLevelConstraints: j \in 1..r})]
/\ n.opLevelCond =
(****************************************************************)
(* n.opLevelCond[i][j][k] is true iff there is an element of *)
(* subExp.argLevelParams indicating that param[j] occurs inside *)
(* the k-th argument of an instance of param[i] in subExp or in *)
(* some mexp[h]. Again, we are being conservative about *)
(* INSTANCE parameters. Note that the arg-level parameters *)
(* that come from mexp[h] involve only the first r formal *)
(* parameters. *)
(****************************************************************)
[i \in 1..p |->
[j \in 1..p |->
[k \in 1..Node[param[i]].numberOfArgs |->
[op |-> param[i], idx |-> k, param |-> param[j]]
\in subExp.argLevelParams \union
UNION {mexp[h].argLevelParams: h \in 1..r}]]]
/\ n.levelParams = subExp.levelParams \ paramIds
(****************************************************************)
(* The level parameters of Op are the ones that come from *)
(* subExp that are not formal parameters. *)
(****************************************************************)
/\ n.levelConstraints =
(****************************************************************)
(* The level constraints of Op are the ones from subExp that *)
(* don't constrain its formal parameters. The level *)
(* constraints that come from the mexp[j] belong to the *)
(* INSTANCE node. *)
(****************************************************************)
{lc \in subExp.levelConstraints: lc.param \notin paramIds}
/\ n.argLevelConstraints =
(****************************************************************)
(* The arg-level constraints of Op are the ones from subExp *)
(* that don't constraint its formal parameters. Again, the *)
(* arg-level constraints that come from the mexp[j] belong to *)
(* the INSTANCE node. *)
(****************************************************************)
{alc \in subExp.argLevelConstraints: alc.param \notin paramIds}
/\ n.argLevelParams =
(****************************************************************)
(* The arg-level parameters of Op are the ones from subExp such *)
(* that the op and params fields are not both formal parameters *)
(* of Op, and the ones from the mexp[j] in which exactly one of *)
(* those fields is a formal parameter of Op. (The ones in *)
(* which both are formal parameters are represented in *)
(* n.opLevelCond; the ones in which neither are formal *)
(* parameters are in the argLevelParams field of the INSTANCE *)
(* node.) Again we are being conservative with INSTANCE *)
(* parameters. Such conservatism seems necessary--for example, *)
(* in case the INSTANCE occurs within a LET. *)
(****************************************************************)
{alp \in subExp.argLevelParams:
\/ alp.op \notin paramIds
\/ alp.param \notin paramIds}
\union
{alp \in UNION {mexp[j].argLevelParams: j \in 1..r}:
\/
/\ alp.op \in paramIds
/\ alp.param \notin paramIds
\/
/\ alp.op \notin paramIds
/\ alp.param \in paramIds}
(***************************************************************************)
(* The definition of OpApplNodeLevelCorrect is rather complicated. There *)
(* are two cases: an application of a declared operator and of a defined *)
(* operator. These two cases are defined separately as *)
(* DeclaredOpApplNodeLevelCorrect and DefinedOpApplNodeLevelCorrect. *)
(***************************************************************************)
DeclaredOpApplNodeLevelCorrect(n) ==
(*************************************************************************)
(* This definition assumes that n is an OpApplNode representing the *)
(* expression Op(arg[1], ... , arg[p]), where Op is a declared *)
(* operator represented by a Node op with NodeId opid. We let the *)
(* formal parameters of the definition of Op be param[1], ... , *)
(* param[p]. *)
(* *)
(* The expression n is always level-correct (if its arguments are). *)
(*************************************************************************)
LET (*********************************************************************)
(* We first define arg, p, op, and param to have the meanings *)
(* described informally above. *)
(*********************************************************************)
p == Len(n.args)
arg == [i \in 1..p |-> Node[n.args[i]]]
(*******************************************************************)
(* arg[i] is the ExprNode representing the i-th argument of the *)
(* expression represented by n. *)
(*******************************************************************)
opid == n.operator
op == Node[opid]
(*******************************************************************)
(* The OpDefNode of the operator Op.) *)
(* ^^^^^^^^^ *)
(* I believe this shold be OpDeclNode. (LL, Mar 2007) *)
(*******************************************************************)
param == op.params
IN
/\ n.level = NumMax(op.level,
SetMax({arg[i].level: i \in 1..p}))
(****************************************************************)
(* For an operator parameter, we assume that the weights of *)
(* each argument are 1, so the level is the maximum of the *)
(* levels of the arg[i], and of its own level. *)
(* *)
(* Corrected (I hope) on 24 Mar 2007 by LL to include op.level. *)
(****************************************************************)
/\ n.levelParams =
(****************************************************************)
(* The level parameters of n are the Op itself and the *)
(* LevelParams of all the arguments. *)
(****************************************************************)
{opid} \union UNION {arg[i].levelParams: i \in 1..p}
/\ n.levelConstraints =
(****************************************************************)
(* The LevelConstraints of n are all obtained from its *)
(* arguments. *)
(****************************************************************)
UNION {arg[i].levelConstraints: i \in 1..p}
/\ n.argLevelConstraints =
(****************************************************************)
(* There are two source of arg-level constraints for n: the *)
(* ones it implies about Op, and the ones it inherits from its *)
(* arguments. *)
(****************************************************************)
{[op |-> opid, idx |-> i, level |-> arg[i].level]: i \in 1..p}
\union
UNION {arg[i].argLevelConstraints: i \in 1..p}
/\ n.argLevelParams =
(****************************************************************)
(* There are two source of arg-level parameters for n: the ones *)
(* it implies about Op, and the ones it inherits from its *)
(* arguments. *)
(****************************************************************)
(LET ALP(i) ==
(*********************************************************)
(* The arg-level parameters implied about Op by the i-th *)
(* argument of n. *)
(*********************************************************)
{[op |-> opid, idx |-> i, param |-> par]:
par \in arg[i].levelParams}
IN UNION {ALP(i): i \in 1..p})
\union
UNION {arg[i].argLevelParams: i \in 1..p}
DefinedOpApplNodeLevelCorrect(n) ==
(*************************************************************************)
(* This definition assumes that n is an OpApplNode representing the *)
(* expression Op(arg[1], ... , arg[p]), where Op is a defined operator. *)
(* We let the formal parameters of the definition of Op be *)
(* param[1], ... , param[p]. *)
(*************************************************************************)
LET (*********************************************************************)
(* We first define arg, p, op, and param to have the meanings *)
(* described informally above. *)
(*********************************************************************)
p == Len(n.args)
arg == [i \in 1..p |-> Node[n.args[i]]]
(*******************************************************************)
(* arg[i] is the ExprNode representing the i-th argument of the *)
(* expression represented by n. *)
(*******************************************************************)
op == Node[n.operator]
(*******************************************************************)
(* The OpDefNode of the operator Op. *)
(*******************************************************************)
param == op.params
numOpArgs(i) == Node[param[i]].numberOfArgs
(*******************************************************************)
(* If the i-th argument of op is an operator argument, then this *)
(* is the number of arguments that that operator argument takes. *)
(*******************************************************************)
defOpArgs ==
(*******************************************************************)
(* The set of i such that param[i] is an operator argument and *)
(* arg[i] is a defined operator. *)
(*******************************************************************)
{i \in 1..p: IsOpArg(op, i) /\ (arg[i].ref \in OpDefNodeId)}
declOpArgs ==
(*******************************************************************)
(* The set of i such that param[i] is an operator argument and *)
(* arg[i] is an operator parameter. *)
(*******************************************************************)
{i \in 1..p: IsOpArg(op, i) /\ (arg[i].ref \in OpDeclNodeId)}
OpLevelCondIdx(i, j) ==
(*******************************************************************)
(* The set of k such that op.opLevelCond[i][j][k] is defined and *)
(* equals TRUE. *)
(*******************************************************************)
{k \in 1..Node[param[i]].numberOfArgs: op.opLevelCond[i][j][k]}
IN
/\ (******************************************************************)
(* This conjunct expresses level-correctness. For the i-th *)
(* argument, there is one condition derived from n.maxLevels[i] *)
(* and, if it is an operator argument and arg[i] is a defined *)
(* operator, then there is a condition derived from *)
(* n.minMaxLevel[i] and a condition derived from *)
(* n.opLevelCond[i]. *)
(******************************************************************)
\A i \in 1..p:
/\ arg[i].level <= op.maxLevels[i]
(***********************************************************)
(* The level of arg[i] must be \leq op.maxLevels[i]. *)
(***********************************************************)
/\
/\ IsOpArg(op, i)
(********************************************************)
(* IF arg[i] is an operator argument oparg ... *)
(********************************************************)
/\ arg[i].ref \in OpDefNodeId
(********************************************************)
(* ... that is defined (rather than declared) [and *)
(* hence is an IdentifierNode whose ref field is an *)
(* OpDefOrDeclNodeId].) THEN *)
(********************************************************)
=>
/\ (*******************************************************)
(* oparg must be able to take a k-th argument of level *)
(* at least op.minMaxLevel[k]. *)
(*******************************************************)
\A k \in 1..numOpArgs(i):
Node[arg[i].ref].maxLevels[k] >= op.minMaxLevel[i][k]
/\ (*******************************************************)
(* If, in the definition of op, param[j] appears *)
(* inside an expression in the k-th argument of *)
(* param[i], then this means that, if we expand the *)
(* definition of op in this expression, oparg will *)
(* appear in a subexpression in which its k-th *)
(* argument contains arg[j]. Hence, oparg must be *)
(* able to take a k-th argument of level at least *)
(* equal to the level of arg[j]. *)
(*******************************************************)
\A j \in 1..p:
\A k \in 1..numOpArgs(i):
op.opLevelCond[i][j][k] =>
arg[j].level <= arg[i].maxLevels[k]
/\ n.level =
(****************************************************************)
(* The maximum of op.level and the levels of all the arguments *)
(* whose corresponding weights are 1. *)
(****************************************************************)
NumMax(op.level,
SetMax({arg[i].level * op.weights[i]: i \in 1..p}))
/\ n.levelParams =
(****************************************************************)
(* The parameters that contribute to the level of expression n *)
(* are the ones contributing to the level of op, together with *)
(* the ones contributing to the level of each argument that has *)
(* weight 1. *)
(****************************************************************)
op.levelParams \union
LET LP(i) == IF op.weights[i] = 1 THEN arg[i].levelParams
ELSE {}
IN UNION {LP(i): i \in 1..p}
/\ n.levelConstraints =
(****************************************************************)
(* Level constraints obtained from the expression arise from *)
(* the following sources: *)
(****************************************************************)
(****************************************************************)
(* 1. op.levelConstraints : *)
(* Constraints inherited from the definition of op. *)
(****************************************************************)
op.levelConstraints
\union
(****************************************************************)
(* 2. arg[i].levelConstraints : *)
(* Constraints inherited from each argument arg[i]. *)
(****************************************************************)
(UNION {arg[i].levelConstraints: i \in 1..p})
\union
(****************************************************************)
(* 3. op.maxLevels[i] : *)
(* If a parameter par contributes to the level of arg[i], *)
(* then the level of par must be \leq op.maxLevels[i]. *)
(****************************************************************)
(LET LC(i) == {[param |-> par, level |-> op.maxLevels[i]]:
par \in arg[i].levelParams}
IN UNION {LC(i): i \in 1..p})
\union
(****************************************************************)
(* 4. op.opLevelCond : *)
(* If param[i] is an operator parameter, arg[i] is *)
(* a defined operator opArg, and param[j] contributes to *)
(* the level of the k-th argument of some occurrence of *)
(* opArg in the definition of Op, then any parameter par *)
(* contributing to the level of arg[j] must have level at *)
(* most opArg.maxlevels[k]. *)
(****************************************************************)
(LET LC(i, j, k) ==
(*************************************************************)
(* The set of level constraints that would be implied if a *)
(* parameter contributes to the level of arg[j], and *)
(* param[j] appears as the k-th argument of some instance of *)
(* param[i] in the definition of the operator arg[i]. *)
(*************************************************************)
{[param |-> par, level |-> Node[arg[i].ref].maxLevels[k]]:
par \in arg[j].levelParams}
LCE(i, j) ==
(*********************************************************)
(* The set of level constraints in all LC(i,j,k) such *)
(* that param[i] is an operator parameter that takes at *)
(* least k-th arguments, and op.opLevelCond[i][j][k] *)
(* implies that param[j] appears as in k-th argument of *)
(* some instance of param[i] in the definition of Op. *)
(*********************************************************)
UNION {LC(i, j, k): k \in OpLevelCondIdx(i, j)}
IN UNION {LCE(i, j): i \in defOpArgs, j \in 1..p})
\union
(****************************************************************)
(* 5. op.argLevelParams : *)
(* For any arg-level parameter alp in op.argLevelParams, *)
(* if alp.op = param[i] and arg[i] is a defined operator *)
(* opArg, then the level of op.param must be \leq *)
(* opArg.maxLevels[alp.idx]. *)
(****************************************************************)
(LET
ALP(i) ==
(*********************************************************)
(* The set of arg-level parameters in op.argLevelParams *)
(* whose op field is param[i]. *)
(*********************************************************)
{alp \in op.argLevelParams: alp.op = param[i]}
LC(i) ==
(*********************************************************)
(* The level constraints implied by the elements in *)
(* ALP(i). *)
(*********************************************************)
{[param |-> alp.param,
level |-> Node[arg[i].ref].maxLevels[alp.idx]]:
alp \in ALP(i)}
IN UNION {LC(i): i \in defOpArgs})
/\ n.argLevelConstraints =
(****************************************************************)
(* Arg-level constraints implied by the expression arise from *)
(* the following sources: *)
(****************************************************************)
(****************************************************************)
(* 1. op.argLevelConstraints *)
(* Expression n inherits arg-level constraints from the *)
(* definition of op. *)
(****************************************************************)
op.argLevelConstraints
\union
(****************************************************************)
(* 2. arg[i].argLevelConstraints *)
(* Expression n inherits arg-level constraints from its *)
(* arguments. *)
(****************************************************************)
(UNION {arg[i].argLevelConstraints: i \in 1..p})
\union
(****************************************************************)
(* 3. op.minMaxLevel *)
(* If arg[i] is a declared operator, then it must be able *)
(* to take a k-th argument of level op.minMaxLevel[i][k]. *)
(****************************************************************)
(LET
ALC(i) ==
(*********************************************************)
(* If arg[i] is the IdentifierNode of a declared *)
(* operator opArg, then these are the arg-level *)
(* constraints implied by op.minMaxLevel for opArg. *)
(*********************************************************)
{[param |-> arg[i].ref,
idx |-> k,
level |-> op.minMaxLevel[i][k]]:
k \in 1..numOpArgs(i)}
IN UNION {ALC(i): i \in declOpArgs})
\union
(****************************************************************)
(* 4. op.opLevelCond *)
(* If op.opLevelCond[i][j][k] is true and arg[i] is an *)
(* Identifier node referring to the declared operator *)
(* opArg, then opArg must be able to take a k-th argument *)
(* of level arg[j].level. *)
(****************************************************************)
(LET ALC(i, j) ==
(*********************************************************)
(* If arg[i] is a declared operator, then this is the *)
(* set of arg-level constraints implied for that *)
(* operator by arg[j].level. *)
(*********************************************************)
{[param |-> arg[i].ref,
idx |-> k,
level |-> arg[j].level]: k \in OpLevelCondIdx(i, j)}
IN UNION {ALC(i, j): i \in declOpArgs, j \in 1..p})
\union
(****************************************************************)
(* 5. op.argLevelParams *)
(* If an arg-level parameter alp indicates that param[i] *)
(* appears as the k-th argument of a declared operator *)
(* opArg, then n has an arg-level constraint indicating *)
(* that opArg must be able to take a k-th argument of *)
(* level arg[i].level. *)
(****************************************************************)
(LET ALP(i) == {alp \in op.argLevelParams: alp.param = param[i]}
(*********************************************************)
(* The subset of op.argLevelParams whose param field is *)
(* the i-th formal parameter of op. *)
(*********************************************************)
ALC(i) ==
(*********************************************************)
(* The set of arg-level constraints implied by the *)
(* elements of ALP(i). *)
(*********************************************************)
{[param |-> alp.param,
idx |-> alp.idx,
level |-> arg[i].level]: alp \in ALP(i)}
IN UNION {ALC(i): i \in 1..p})
/\ n.argLevelParams =
(****************************************************************)
(* Arg-level parameters implied by the expression arise from *)
(* the following sources: *)
(****************************************************************)
(****************************************************************)
(* 1. arg[i].argLevelParams *)
(* The expression inherits all arg-level parameters from *)
(* its arguments. *)
(****************************************************************)
(UNION {arg[i].argLevelParams: i \in 1..p})
\union
(****************************************************************)
(* 2. Elements alp of op.argLevelParams with neither alp.op or *)
(* alp.param a formal parameter of the definition of op. *)
(****************************************************************)
{alp \in op.argLevelParams:
\A i \in 1..p: (alp.op /= param[i]) /\ (alp.param /= param[i])}
\union
(****************************************************************)
(* 3. Elements alp of op.argLevelParams with alp.op = param[i]. *)
(* If arg[i] is a declared operator opArg, then this *)
(* implies an arg-level parameter asserting that alp.param *)
(* appears in argument alp.idx of opArg. *)
(****************************************************************)
(LET ALP(i) == {alp \in op.argLevelParams: alp.op = param[i]}
(*********************************************************)
(* The set of arg-level parameters alp of op with alp.op *)
(* = param[i]. (Note: we know that alp.param is not a *)
(* formal parameter of op, because op.argLevelParams *)
(* does not contain arg-level parameterss in which both *)
(* the op and param fields are formal parameters of the *)
(* definition of op.) *)
(*********************************************************)
NLP(i) ==
(*********************************************************)
(* The arg-level parameters of the expression implied by *)
(* the elements of ALP(i). *)
(*********************************************************)
{[alp EXCEPT !.op = arg[i].ref]: alp \in ALP(i)}
IN UNION {NLP(i): i \in declOpArgs})
\union
(****************************************************************)
(* 4. Elements alp of op.argLevelParams with alp.param = *)
(* param[i]. *)
(* This implies an arg-level parameter asserting that *)
(* every parameter contributing to the level of arg[i] *)
(* appears in argument alp.idx of an occurrence of *)
(* alp.op. *)
(****************************************************************)
(LET OLP(i) ==
(*********************************************************)
(* The set of all arg-level parameters whose param field *)
(* is param[i]. *)
(*********************************************************)
{alp \in op.argLevelParams: alp.param = param[i]}
ALP(i) ==
(*********************************************************)
(* The set of arg-level parameters obtained from an *)
(* arg-level parameter alp in op.argLevelParams by *)
(* replacing alp.param with an element of *)
(* arg[i].levelParams. *)
(*********************************************************)
{[alp EXCEPT !.param = par]:
alp \in OLP(i), par \in arg[i].levelParams}
IN UNION {ALP(i): i \in declOpArgs})
\union
(****************************************************************)
(* 5. op.opLevelCond *)
(* If op.opLevelCond[i][j][k] = TRUE and arg[i] is a *)
(* declared operator opArg, then there are arg-level *)
(* parameters declaring that every parameter contributing *)
(* to the level of arg[j] appears in argument k of an *)
(* occurrence of opArg. *)
(****************************************************************)
(LET ALP(i, j) ==
(*********************************************************)
(* If arg[i] is a declared operator, then this is the *)
(* set of all all arg-level parameters implied by *)
(* op.opLevelCond[i][j] and arg[j].levelParams. *)
(*********************************************************)
{[op |-> arg[i].ref, idx |-> k, param |-> par]:
k \in OpLevelCondIdx(i, j), par \in arg[j].levelParams}
IN UNION {ALP(i, j): i \in declOpArgs, j \in 1..p})
OpApplNodeLevelCorrect(n) ==
IF n.operator \in OpDeclNodeId THEN DeclaredOpApplNodeLevelCorrect(n)
ELSE DefinedOpApplNodeLevelCorrect(n)
LetInNodeLevelCorrect(n) ==
(*************************************************************************)
(* We assume n is a LetInNode. *)
(* *)
(* A LetInNode is level-correct iff its children are. *)
(* *)
(* The level constraints come from the IN expression together with the *)
(* LET definitions, except that the constraints on the definition's *)
(* formal parameters must be removed from the argLevelParams field of a *)
(* LET definition. *)
(*************************************************************************)
LET exp == Node[n.body]
letIds == n.opDefs \union n.instances
opParams(opid) ==
(*******************************************************************)
(* If opid is an OpDefNodeId, then this is the set of formal *)
(* parameters of the definition represented by Node[opid]. *)
(*******************************************************************)
{Node[opid].params[i]: i \in 1..Node[opid].numberOfArgs}
IN
/\ n.level = exp.level
/\ n.levelParams =
exp.levelParams
/\ n.levelConstraints =
exp.levelConstraints \union
UNION {Node[opid].levelConstraints: opid \in letIds}
/\ n.argLevelConstraints =
exp.argLevelConstraints \union
UNION {Node[opid].argLevelConstraints: opid \in letIds}
/\ n.argLevelParams =
exp.argLevelParams
\union
(UNION {ReducedLevelConstraint(Node[opid],
opParams(opid)).argLevelParams:
opid \in n.opDefs})
\union
UNION {Node[opid].argLevelParams: opid \in n.instances}
IdentifierNodeLevelCorrect(n) ==
(*************************************************************************)
(* An IdentifierNode represents an expression that consists of a single *)
(* symbol, or else an operator argument appearing as the argument in the *)
(* application of a higher-order operator. *)
(* *)
(* It is always level-correct if its ref field is, which will be the *)
(* case except possibly for a defined operator argument *)
(*************************************************************************)
/\ n.level = Node[n.ref].level
(********************************************************************)
(* The level is the level of the symbol's node. *)
(********************************************************************)
/\ IF n.ref \in OpDeclNodeId \union BoundSymbolNodeId
THEN (***************************************************************)
(* The symbol is a declared operator or a bound symbol. In *)
(* this case, all the constraints are empty except for a *)
(* ConstantDeclNode, in which case the set of level parameters *)
(* consists of the symbol itself. *)
(***************************************************************)
/\ n.levelParams = IF n.ref \in ConstantDeclNodeId
THEN {n.ref}
ELSE {}
/\ n.levelConstraints = {}
/\ n.argLevelConstraints = {}
/\ n.argLevelParams = {}
ELSE (***************************************************************)
(* The symbol is a defined operator (appearing as an argument *)
(* to a higher-order operator). Its constraints are the *)
(* constraints of the symbol's OpDefNode. *)
(***************************************************************)
/\ n.levelParams = Node[n.ref].levelParams
/\ n.levelConstraints = Node[n.ref].levelConstraints
/\ n.argLevelConstraints = Node[n.ref].argLevelConstraints
/\ n.argLevelParams = Node[n.ref].argLevelParams
LevelCorrect ==
(*************************************************************************)
(* The following kinds of nodes are always level-correct, and any level *)
(* information they contain is specified by their types. *)
(* OpDeclNode *)
(* ValueNode *)
(* OpDefNode for a built-in operator (one whose OpDefNode has a Null *)
(* body) *)
(* BoundSymbolNode *)
(* *)
(* The following nodes are level-correct iff their children are, and *)
(* they have no level constraints: *)
(* *)
(* SubstitutionNode *)
(*************************************************************************)
\A id \in NodeId:
LET n == Node[id]
IN
/\ (n \in IdentifierNode) => IdentifierNodeLevelCorrect(n)
/\ (n \in OpApplNode) => OpApplNodeLevelCorrect(n)
/\ n \in LetInNode => LetInNodeLevelCorrect(n)
/\ n \in InstanceNode => InstanceNodeLevelCorrect(n)
/\ n \in ModuleNode => ModuleNodeLevelCorrect(n)
/\ (n \in OpDefNode) /\ (n.body /= Null) => OpDefNodeLevelCorrect(n)
================================================================================