Skip to content

Instantly share code, notes, and snippets.

@lemmy

lemmy/Generator.tla

Created April 13, 2019 00:57
Show Gist options
  • Save lemmy/6c820425e683b7535d513b9506fe0e37 to your computer and use it in GitHub Desktop.
Save lemmy/6c820425e683b7535d513b9506fe0e37 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Generator.tla
-----------------------------------------------------------------------------
(***************************************************************************)
(* THE ALGORITHM *)
(***************************************************************************)
(**************************************
--algorithm Subexpression
variables
(*************************************************************************)
(* The input variables. *)
(*************************************************************************)
ops = MCops,
args = MCargs,
(***********************************************************************)
(* The sequences op and args described above. *)
(***********************************************************************)
expectedArity = MCexpectedArity,
(***********************************************************************)
(* The arity of the operator expected, or -1 if expecting a definition *)
(* name. It is 0 iff an expression is expected. The result should be *)
(* an OpArg node if expectedArity > 0, it should be an expression node *)
(* if expectedArity = 0, and it should be a UserDefinedOpKind or a *)
(* ThmOrAssumpDefKind if expectedArity < 0. *)
(***********************************************************************)
(*************************************************************************)
(* The major variables of the algorithm. *)
(*************************************************************************)
substInPrefix = << >> ,
(***********************************************************************)
(* The sequence of SubstInNode or APSubstInNode sequence that will be *)
(* appended to body of the resulting OpApplNode *)
(***********************************************************************)
params = << >> ,
(***********************************************************************)
(* The sequence of FormalParamNode objects that are the formal *)
(* parameters if this produces a Lambda expression. A Lambda *)
(* expression will be produced iff this is non-empty *)
(***********************************************************************)
allArgs = << >> ,
(***********************************************************************)
(* The sequence of all arguments. *)
(***********************************************************************)
curNode = null,
(***********************************************************************)
(* If params = << >>, then the OpDefNode for the OpApplNode that is *)
(* produced. If params # << >>, then the Expr node that will form the *)
(* body of the Lambda expression. *)
(* *)
(* Note: in the Java implementation, this will actually be a ref to *)
(* the node--in terms of this spec, a NodeId. *)
(***********************************************************************)
subExprOf = "null",
(***********************************************************************)
(* The node UserDefinedOpDefKind or ThmOrAssumpDefKind within which *)
(* this subexpression is defined. *)
(***********************************************************************)
result = null,
(***********************************************************************)
(* The actual output node. *)
(***********************************************************************)
(*************************************************************************)
(* The local variables. *)
(*************************************************************************)
idx = 1,
(***********************************************************************)
(* The element of the arrays op and args that the algorithm is *)
(* currently examining. *)
(***********************************************************************)
mode = "FindingOpName",
(***********************************************************************)
(* The current mode describing what kind of selector it is expecting *)
(* next. Its other possible values are "FollowingLabels" and *)
(* "FindingSubExpr". *)
(***********************************************************************)
prevMode = "",
(***********************************************************************)
(* The mode for the previously examined selector. *)
(***********************************************************************)
curContext = GlobalContext,
(***********************************************************************)
(* The context for looking up operator or label names. *)
(***********************************************************************)
curName = "" ,
(***********************************************************************)
(* When looking up an operator name, which may be something like *)
(* "Foo!Bar!Baz", this is the part that has been found so far. *)
(***********************************************************************)
opDefArityFound = 0,
opDefArgs = << >>,
(***********************************************************************)
(* The total arity and the sequence of arguments found so far for the *)
(* current operator--for example, opDefArityFound will equal 2 if the *)
(* algorithm has so far processed "Foo(a, b)!Bar" *)
(***********************************************************************)
firstFindingOpName = TRUE,
(***********************************************************************)
(* True iff have entered the FindingOpName only once (initially). *)
(***********************************************************************)
opNode,
newName,
newNode,
nodeArity,
temp
(***************************************************************************)
(* A macro used for reporting an error and terminating the execution. *)
(***************************************************************************)
macro Error(msg) begin print msg ;
if debug then (**************************************)
(* Force the +cal translator to *)
(* insert a label so the error trace *)
(* shows the final state. *)
(**************************************)
idx := idx ;
idx := idx ;
assert FALSE
else goto Done
end if
end macro ;
begin
(*************************************************************************)
(* An assertion that checks that ops and args are consistent with each *)
(* other and with the value of expectedArity. In an implementation, *)
(* some of these should be guaranteed by the context (e.g., Len(ops) = *)
(* Len(args) while others will be checked as part of the processing for *)
(* the particular value of idx. *)
(*************************************************************************)
assert /\ expectedArity \in Int
/\ ops \in Seq(STRING)
/\ args \in Seq(Seq(NodeId))
/\ Len(ops) = Len(args)
/\ \A i \in 1..Len(ops) :
/\ \/ ops[i] \in {"<<", ">>", "@", ":"} \cup NumberOp
\/ expectedArity # 0
=> args[i] = << >>
/\ (ops[i] = "null") => (Len(args[i]) > 0) ;
(*************************************************************************)
(* The outer "for" loop on idx. *)
(*************************************************************************)
while idx <= Len(ops) do
if mode = "FindingOpName" then
newName := IF IsName(ops[idx])
THEN IF curName = "" THEN ops[idx]
ELSE curName \o "!" \o ops[idx]
ELSE null ;
if /\ curName = ""
/\ ~ IsName(ops[idx])
then (*****************************************************************)
(* I think that this error can only happen for idx = 1, and *)
(* should never happen in the implementation because the parser *)
(* should not allow a compound name that doesn't begin with a *)
(* name. *)
(*****************************************************************)
Error("Need an operator or label name or step number here")
end if;
newNode := IF newName # null THEN LookUp(newName, curContext) ELSE null ;
if newNode = null
then Error ("Unknown operator")
end if;
curNode := newNode ;
curName := newName ;
if curNode.kind \in
{UserDefinedOpKind, ThmOrAssumpDefKind,
ModuleInstanceKind, ConstantDeclKind, VariableDeclKind,
FormalParamKind, BuiltInKind, BoundSymbolKind}
then if curNode.kind \in
{ConstantDeclKind, VariableDeclKind, FormalParamKind,
BuiltInKind, BoundSymbolKind}
then if idx # 1
then Error("Abort: Impossible naming of declaration "
\o "or built-in operator.")
else if Len(ops) # 1
then Error("Can't take subexpression of this");
end if
end if
end if ;
nodeArity := Arity(curNode) ;
if expectedArity = 0
then if opDefArityFound + Len(args[idx]) # nodeArity
then Error("Wrong number of arguments")
end if ;
if \E i \in 1..Len(args[idx]) :
Arity(Node[args[idx][i]]) #
ParamArity(curNode, i + opDefArityFound)
then Error("Argument has wrong arity")
else opDefArgs := opDefArgs \o args[idx] ;
end if ;
else if expectedArity > 0
then if \E i \in 1..Len(curNode.params) :
curNode.params[i].arity > 0
then Error("Higher-order operator selected "
\o "as operator argument")
end if
\* else Error(
\* "Abort: Don't yet handle expectedArity < 0")
end if
end if ;
opDefArityFound := nodeArity ;
if curNode.kind \in {UserDefinedOpKind, ThmOrAssumpDefKind,
ConstantDeclKind, VariableDeclKind,
FormalParamKind, BoundSymbolKind}
then if /\ curNode.kind = UserDefinedOpKind
/\ ~ curNode.defined
/\ ~ Len(ops) = 1
then Error("Can't refer to subexpression of "
\o "operator inside its definition")
end if;
if /\ firstFindingOpName
/\ curNode.kind \in {UserDefinedOpKind, ThmOrAssumpDefKind}
then subExprOf := curNode
end if;
if idx # Len(ops)
then params := params \o curNode.params ;
curName := "" ;
if IsName(ops[idx+1])
then mode := "FollowingLabels"
else mode := "FindingSubExpr" ;
end if ;
allArgs := allArgs \o opDefArgs ;
opDefArityFound := 0 ;
opDefArgs := << >> ;
newNode := Node[curNode.body] ;
while newNode.kind = SubstInKind do
substInPrefix := substInPrefix \o <<newNode>>;
newNode := Node[newNode.body];
end while ;
(********************************************)
(* If the next op is an OpSel, then need to *)
(* skip over SubstInNodes, which are *)
(* invisible to the user. *)
(********************************************)
if mode = "FindingSubExpr"
then curNode := newNode
end if;
end if ;
else \* curNode.kind = ModuleInstanceKind
if (idx = Len(ops))
then Error("Operator name incomplete")
end if
end if
else Error("Unexpected node kind") ;
end if ;
prevMode := "FindingOpName" ;
elsif mode = "FollowingLabels" then
if prevMode = "FindingOpName"
then assert curNode.kind \in {UserDefinedOpKind, ThmOrAssumpDefKind} ;
newNode := LookUp(ops[idx], curNode.labels) ;
else assert curNode.kind = LabelKind ;
newNode := LookUp(ops[idx], curNode.labels) ;
end if ;
if newNode = null
then Error("Label not found")
end if;
curNode := newNode ;
if expectedArity = 0
then if Len(args[idx]) # curNode.arity
then Error("bad arity")
end if ;
if \E i \in 1..Len(args[idx]) :
Arity(Node[args[idx][i]]) # 0
then Error("Operator argument given to label")
end if;
allArgs := allArgs \o args[idx] ;
end if;
params := params \o curNode.params ;
if /\ idx < Len(ops)
/\ ~IsName(ops[idx+1])
then mode := "FindingSubExpr"
end if ;
if \/ mode = "FindingSubExpr"
\/ idx = Len(ops)
then curNode := Node[curNode.body]
end if;
prevMode := "FollowingLabels";
elsif mode = "FindingSubExpr" then
if ops[idx] = ":" then
if \/ prevMode \notin {"FindingOpName", "FollowingLabels"}
\/ ~ \/ /\ idx = Len(ops)
/\ prevMode = "FindingOpName"
\/ /\ idx < Len(ops)
/\ IsName(ops[idx+1])
then Error("`!:' can be used only after a name and either at the " \o
"end after an operator name or before an operator name.")
end if
elsif curNode.kind = LetInKind then
if ArgNum(ops[idx], 1) = 1
then curNode := Node[curNode.body]
else Error("A Let/In has only a single operand")
end if ;
elsif curNode.kind = OpApplKind then
opNode := Node[curNode.operator] ;
if opNode.kind
\in {FormalParamKind, ConstantDeclKind, UserDefinedOpKind} then
(******************************************************************)
(* Selecting an argument from something of the form Op(...). *)
(******************************************************************)
temp := ArgNum(ops[idx], opNode.arity) ;
if temp = -1
then Error("Nonexistent operand specified")
else curNode := Node[curNode.operands[temp]]
end if
elsif opNode.kind = BuiltInKind then
\* See configuration/ConfigConstants for a list of all
\* BuiltInKind operators.
if opNode.name \in {"$RcdConstructor", "$SetOfRcds"} then
(*****************************************************************)
(* curNode represents an expression *)
(* [a_1 |-> e_1, ... , a_n |-> e_n] or *)
(* [a_1 : e_1, ... , a_n : e_n] *)
(* Its i-th argument is the $Pair node (a_i, e_i) *)
(*****************************************************************)
temp := ArgNum(ops[idx], Len(curNode.operands)) ;
if temp = -1
then Error("Incorrect subexpression number")
end if ;
curNode := Node[curNode.operands[temp]] ;
if \/ curNode.kind # OpApplKind
\/ Node[curNode.operator].kind # BuiltInKind
\/ Node[curNode.operator].name # "$Pair"
then Error ("Expecting $Pair(...)")
else curNode := Node[curNode.operands[2]]
end if
elsif opNode.name \in {"$Case"} then
(*****************************************************************)
(* The i-th clause is a $Pair node, where for the OTHER clause *)
(* the 1st element is null. *)
(*****************************************************************)
if idx = Len(ops)
then Error( "CASE subexpression must be of form !i!j")
end if ;
temp := ArgNum( ops[idx], Len(curNode.operands)) ;
if temp = -1
then Error("Incorrect subexpression name")
end if ;
curNode := Node[curNode.operands[temp]] ;
if \/ curNode.kind # OpApplKind
\/ Node[curNode.operator].kind # BuiltInKind
\/ Node[curNode.operator].name # "$Pair"
then Error ("Expecting $Pair(...)")
end if ;
idx := idx+1 ;
temp := ArgNum(ops[idx], 2);
if temp = -1
then Error("Incorrect subexpression name")
end if ;
curNode := Node[curNode.operands[temp]] ;
if curNode = null
then Error("Selecting OTHER")
end if
elsif opNode.name = "$Except" then
(****************************************************************)
(* For *)
(* [exp_1 ELSE !... = exp_2, ... , !.. = exp_n] *)
(* argument number i chooses exp_i. For i > 1, exp_i is the *)
(* second argument of a $Pair operator. *)
(****************************************************************)
temp := ArgNum(ops[idx], Len(curNode.operands));
if temp = -1
then Error("Bad argument selector.")
end if;
curNode := Node[curNode.operands[temp]] ;
if temp > 1
then if \/ curNode.kind # OpApplKind
\/ Node[curNode.operator].kind # BuiltInKind
\/ Node[curNode.operator].name # "$Pair"
then Error("Unexpected expression node found.")
else curNode := Node[curNode.operands[2]]
end if
end if
else
(*****************************************************************)
(* Operator handled by standard procedure. *)
(*****************************************************************)
if /\ Len(curNode.unboundedBoundSymbols) = 0
/\ Len(curNode.boundedBoundSymbols) = 0
then (**********************************************************)
(* Current subexpression has no bound variables. *)
(**********************************************************)
temp := ArgNum(ops[idx], Len(curNode.operands)) ;
if temp = -1
then Error("Incorrect subexpression selector")
end if;
curNode := Node[curNode.operands[temp]] ;
else
(**********************************************************)
(* Current subexpression has bound variables. If *)
(* selector is "@" or null, then choosing body and adding *)
(* parameters. Otherwise, must be selecting one of the *)
(* bounds. *)
(**********************************************************)
if ops[idx] \in {"null", "@"}
then (***************************************************)
(* Set temp to the sequence of parameters. *)
(***************************************************)
temp := IF Len(curNode.unboundedBoundSymbols) > 0
THEN curNode.unboundedBoundSymbols
ELSE SeqSeqToSeq(
curNode.boundedBoundSymbols);
params := params \o
[i \in 1.. Len(temp) |->
[name |-> temp[i], arity |-> 0]] ;
allArgs := allArgs \o args[idx] ;
if /\ ops[idx] = "null"
/\ Len(args[idx]) # Len(temp)
then Error("Wrong number of selector arguments");
end if;
curNode := Node[curNode.operands[1]];
else temp := ArgNum(ops[idx], Len(curNode.ranges)) ;
if temp = -1
then Error ("Selecting non-existent range") ;
else curNode := Node[curNode.ranges[temp]]
end if
end if
end if
end if \* opNode.name = ...
else Error("Applying subexpression chooser to an expr" \o
" with no choosable subexpressions")
end if \* opNode.kind = ...
elsif curNode.kind = AssumeProveKind then
temp := ArgNum(ops[idx], 1 + Len(curNode.assumes)) ;
if temp = -1
then Error("Illegal argument number")
else if temp <= Len(curNode.assumes)
then curNode := Node[curNode.assumes[temp]]
else curNode := Node[curNode.prove]
end if
end if
elsif curNode.kind = OpArgKind then
(*********************************************************************)
(* The only kind of OpArgNode that has a subpart is a Lambda *)
(* expression. *)
(*********************************************************************)
opNode := Node[curNode.op] ;
if \/ opNode.kind # UserDefinedOpKind
\/ opNode.name # "LAMBDA" then
Error("Selecting from operator argument that has no sub-part")
elsif ops[idx] \notin {"null", "@"} then
Error("Incorrect selection from LAMBDA")
elsif /\ ops[idx] = "null"
/\ Len(args[idx]) # Len(opNode.params) then
Error("Incorrect number of arguments for LAMBDA")
else params := params \o opNode.params ;
allArgs := allArgs \o args[idx] ;
curNode := Node[opNode.body] ;
end if
elsif curNode.kind \in {UserDefinedOpKind, BuiltInKind} then
Error("Abort: should not have been able to choose this node.")
elsif curNode.kind \in {AtNodeKind, DecimalKind, NumeralKind, StringKind,
FormalParamKind, ConstantDeclKind, VariableDeclKind,
BoundSymbolKind} then
Error("Selected part has no subexpression")
elsif curNode.kind = LabelKind then
(*********************************************************************)
(* Skip over label. *)
(*********************************************************************)
curNode := Node[curNode.body] ;
idx := idx - 1 ;
else
Error("Unexpected node kind found in expression")
end if; \* ops[idx] = ":"
if idx # Len(ops)
then if IsName(ops[idx+1])
then while curNode.kind = LabelKind do
curNode := Node[curNode.body]
end while ;
if curNode.kind = LetInKind
then curContext := curNode.context ;
mode := "FindingOpName" ;
firstFindingOpName := FALSE;
else Error("A name not following the selector of a LET")
end if
else if ops[idx+1] = ":"
then Error("!: should not follow an operand selector")
end if ;
end if ;
end if ; \* ops[idx] = ":"
prevMode := "FindingSubExpr";
else Error("Bad value of mode")
end if ; \* mode = ...
idx := idx + 1;
end while ;
if curNode.kind = AssumeProveKind
then Error("Selecting ASSUME/PROVE instead of expression")
end if;
if expectedArity < 0
then if \/ prevMode # "FindingOpName"
\/ curNode.kind \notin {UserDefinedOpKind, ThmOrAssumpDefKind}
then Error("Should have selected a definition, but didn't.")
end if;
result := curNode ;
goto Finished
end if;
if expectedArity > 0
then temp := Len(params) + IF \/ prevMode = "FindingOpName"
\/ curNode.kind = OpArgKind
THEN Arity(curNode)
ELSE 0 ;
if expectedArity # temp
then Error("Expect arity = " \o ToString(expectedArity)
\o ", but found arity = " \o ToString(temp))
end if
end if;
(*************************************************************************)
(* If found an operator def and there are parameters or substitutions, *)
(* then set curNode to the operator applied to new parameters, add those *)
(* parameters to params and add the arguments to allArgs. Note: need to *)
(* do this even if operator takes no parameters because we need to put *)
(* the operator in a LAMBDA expression whose body is an expression *)
(*************************************************************************)
if /\ prevMode = "FindingOpName"
/\ Len(params) + Len(substInPrefix) > 0
then temp := [i \in 1..Len(curNode.params) |->
[curNode.params[i] EXCEPT !.name = "New " \o @]] ;
(****************************************************************)
(* temp := new formal parameters for the operator, with the *)
(* same arities as the original parameters. *)
(****************************************************************)
curNode := [kind |-> OpApplKind,
operands |-> temp,
operator |-> curNode,
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>] ;
params := params \o temp ;
allArgs := allArgs \o opDefArgs ;
end if ;
if curNode.kind = OpArgKind
then if expectedArity = 0 then
Error("Selected Operator Argument when expression expected.")
elsif expectedArity # Len(params) + curNode.arity then
Error("Selected operator has wrong arity.")
else
if Len(params) + Len(substInPrefix) > 0
then (********************************************************)
(* If curNode is a LAMBDA, then this will eventually *)
(* produce an OpArg node whose operator is a LAMBDA *)
(* whose body is an OpApplNode that applies the *)
(* curNode's LAMBDA to parameters of the outer LAMBDA. *)
(* This result can be simplified to a LAMBDA whose body *)
(* is the body of curNode. However, that *)
(* simplification is what one will get by selecting the *)
(* body of the LAMBDA, so we keep this complicated *)
(* expression in this case. *)
(********************************************************)
temp := [i \in 1..curNode.arity |->
[name |-> "NewParam" \o NumToString(i),
arity |-> 0]] ;
curNode := [kind |-> OpApplKind,
operands |-> temp,
operator |-> Node[curNode.op],
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>] ;
params := params \o temp
end if
end if
end if ;
if curNode.kind \in {UserDefinedOpKind, ConstantDeclKind, VariableDeclKind,
FormalParamKind, BuiltInKind, BoundSymbolKind,
ThmOrAssumpDefKind} then
(***********************************************************************)
(* There are no params or substitutions, so this is an easy case. *)
(***********************************************************************)
if expectedArity > 0 then
result := [kind |-> OpArgKind,
name |-> curNode.name,
op |-> curNode,
arity |-> expectedArity]
elsif expectedArity = 0 then
result := [kind |-> OpApplKind,
operands |-> opDefArgs,
operator |-> curNode,
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>,
subExprOf |-> subExprOf]
end if
elsif curNode.kind = OpArgKind then
(***********************************************************************)
(* There are no params or substitutions, so this is an easy case. *)
(***********************************************************************)
result := curNode ;
else (******************************************************************)
(* curNode should be an expression node. *)
(******************************************************************)
temp := Len(substInPrefix) ;
while temp > 0 do
curNode := [kind |-> SubstInKind,
body |-> curNode ,
subst |-> substInPrefix[temp].subst ] ;
temp := temp - 1;
end while;
if expectedArity > 0
then if Len(params) # expectedArity
then Error ("Selection has wrong arity")
end if ;
result := [kind |-> OpArgKind,
op |-> [kind |-> UserDefinedOpKind,
name |-> "LAMBDA",
body |-> curNode,
params |-> params,
arity |-> Len(params),
defined |-> TRUE,
source |-> null],
name |-> "LAMBDA"]
else if Len(params) # Len(allArgs)
then Error("Abort: number of params # num of args")
end if ;
if Len(params) = 0
then (******************************************************)
(* This is the one case with expectedArity = 0 in *)
(* which the result is not a newly-constructed node. *)
(* In this case, we construct a dummy label node so *)
(* we have a node to which the implementation can *)
(* attach the syntax node. *)
(******************************************************)
result := [kind |-> LabelKind,
name |-> "$Subexpression",
arity |-> 0,
params |-> << >>,
body |-> curNode,
subExprOf |-> subExprOf]
else result := [kind |-> OpApplKind,
operator |-> [kind |-> UserDefinedOpKind,
name |-> "LAMBDA",
body |-> curNode,
params |-> params,
arity |-> Len(params),
defined |-> TRUE,
source |-> null],
operands |-> allArgs,
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>,
subExprOf |-> subExprOf]
end if
end if
end if;
Finished:
print "Result: " ;
print result ;
end algorithm
*********************************************************************)
\* BEGIN TRANSLATION
VARIABLES ops, args, expectedArity, substInPrefix, params, allArgs, curNode,
subExprOf, result, idx, mode, prevMode, curContext, curName,
opDefArityFound, opDefArgs, firstFindingOpName, opNode, newName,
newNode, nodeArity, temp, pc
vars == << ops, args, expectedArity, substInPrefix, params, allArgs, curNode,
subExprOf, result, idx, mode, prevMode, curContext, curName,
opDefArityFound, opDefArgs, firstFindingOpName, opNode, newName,
newNode, nodeArity, temp, pc >>
Init == (* Global variables *)
/\ ops = MCops
/\ args = MCargs
/\ expectedArity = MCexpectedArity
/\ substInPrefix = << >>
/\ params = << >>
/\ allArgs = << >>
/\ curNode = null
/\ subExprOf = "null"
/\ result = null
/\ idx = 1
/\ mode = "FindingOpName"
/\ prevMode = ""
/\ curContext = GlobalContext
/\ curName = ""
/\ opDefArityFound = 0
/\ opDefArgs = << >>
/\ firstFindingOpName = TRUE
/\ opNode = {}
/\ newName = {}
/\ newNode = {}
/\ nodeArity = {}
/\ temp = {}
/\ pc = "Lbl_1"
Lbl_1 == /\ pc = "Lbl_1"
/\ Assert(/\ expectedArity \in Int
/\ ops \in Seq(STRING)
/\ args \in Seq(Seq(NodeId))
/\ Len(ops) = Len(args)
/\ \A i \in 1..Len(ops) :
/\ \/ ops[i] \in {"<<", ">>", "@", ":"} \cup NumberOp
\/ expectedArity # 0
=> args[i] = << >>
/\ (ops[i] = "null") => (Len(args[i]) > 0),
"Failure of assertion at line line 1901, column 3.")
/\ pc' = "Lbl_2"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, idx, mode,
prevMode, curContext, curName, opDefArityFound,
opDefArgs, firstFindingOpName, opNode, newName,
newNode, nodeArity, temp >>
Lbl_2 == /\ pc = "Lbl_2"
/\ IF idx <= Len(ops)
THEN /\ IF mode = "FindingOpName"
THEN /\ newName' = IF IsName(ops[idx])
THEN IF curName = "" THEN ops[idx]
ELSE curName \o "!" \o ops[idx]
ELSE null
/\ IF /\ curName = ""
/\ ~ IsName(ops[idx])
THEN /\ PrintT("Need an operator or label name or step number here")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_3"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_4"
/\ UNCHANGED idx
/\ UNCHANGED << params, allArgs, curNode,
opNode, newNode, temp >>
ELSE /\ IF mode = "FollowingLabels"
THEN /\ IF prevMode = "FindingOpName"
THEN /\ Assert(curNode.kind \in {UserDefinedOpKind, ThmOrAssumpDefKind},
"Failure of assertion at line line 2022, column 13.")
/\ newNode' = LookUp(ops[idx], curNode.labels)
ELSE /\ Assert(curNode.kind = LabelKind,
"Failure of assertion at line line 2024, column 13.")
/\ newNode' = LookUp(ops[idx], curNode.labels)
/\ IF newNode' = null
THEN /\ PrintT("Label not found")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_21"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_22"
/\ UNCHANGED idx
/\ UNCHANGED << params, allArgs,
curNode, opNode,
temp >>
ELSE /\ IF mode = "FindingSubExpr"
THEN /\ IF ops[idx] = ":"
THEN /\ IF \/ prevMode \notin {"FindingOpName", "FollowingLabels"}
\/ ~ \/ /\ idx = Len(ops)
/\ prevMode = "FindingOpName"
\/ /\ idx < Len(ops)
/\ IsName(ops[idx+1])
THEN /\ PrintT("!: can occur only after a name and either " \o
"at the end or before a name")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_28"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_62"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode,
opNode,
temp >>
ELSE /\ IF curNode.kind = LetInKind
THEN /\ IF ArgNum(ops[idx], 1) = 1
THEN /\ curNode' = Node[curNode.body]
/\ pc' = "Lbl_62"
/\ UNCHANGED idx
ELSE /\ PrintT("A Let/In has only a single operand")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_29"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED curNode
/\ UNCHANGED << params,
allArgs,
opNode,
temp >>
ELSE /\ IF curNode.kind = OpApplKind
THEN /\ opNode' = Node[curNode.operator]
/\ IF opNode'.kind
\in {FormalParamKind, ConstantDeclKind, UserDefinedOpKind}
THEN /\ temp' = ArgNum(ops[idx], opNode'.arity)
/\ IF temp' = -1
THEN /\ PrintT("Nonexistent operand specified")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_30"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED curNode
ELSE /\ curNode' = Node[curNode.operands[temp']]
/\ pc' = "Lbl_62"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs >>
ELSE /\ IF opNode'.kind = BuiltInKind
THEN /\ IF opNode'.name \in {"$RcdConstructor", "$SetOfRcds"}
THEN /\ temp' = ArgNum(ops[idx], Len(curNode.operands))
/\ IF temp' = -1
THEN /\ PrintT("Incorrect subexpression number")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_31"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_32"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode >>
ELSE /\ IF opNode'.name \in {"$Case"}
THEN /\ IF idx = Len(ops)
THEN /\ PrintT("CASE subexpression must be of form !i!j")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_35"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_36"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode,
temp >>
ELSE /\ IF opNode'.name = "$Except"
THEN /\ temp' = ArgNum(ops[idx], Len(curNode.operands))
/\ IF temp' = -1
THEN /\ PrintT("Bad argument selector.")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_45"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_46"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode >>
ELSE /\ IF /\ Len(curNode.unboundedBoundSymbols) = 0
/\ Len(curNode.boundedBoundSymbols) = 0
THEN /\ temp' = ArgNum(ops[idx], Len(curNode.operands))
/\ IF temp' = -1
THEN /\ PrintT("Incorrect subexpression selector")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_49"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_50"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode >>
ELSE /\ IF ops[idx] \in {"null", "@"}
THEN /\ temp' = IF Len(curNode.unboundedBoundSymbols) > 0
THEN curNode.unboundedBoundSymbols
ELSE SeqSeqToSeq(
curNode.boundedBoundSymbols)
/\ params' = params \o
[i \in 1.. Len(temp') |->
[name |-> temp'[i], arity |-> 0]]
/\ allArgs' = allArgs \o args[idx]
/\ IF /\ ops[idx] = "null"
/\ Len(args[idx]) # Len(temp')
THEN /\ PrintT("Wrong number of selector arguments")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_51"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_52"
/\ UNCHANGED idx
/\ UNCHANGED curNode
ELSE /\ temp' = ArgNum(ops[idx], Len(curNode.ranges))
/\ IF temp' = -1
THEN /\ PrintT("Selecting non-existent range")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_53"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED curNode
ELSE /\ curNode' = Node[curNode.ranges[temp']]
/\ pc' = "Lbl_62"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs >>
ELSE /\ PrintT("Applying subexpression chooser to an expr" \o
" with no choosable subexpressions")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_54"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode,
temp >>
ELSE /\ IF curNode.kind = AssumeProveKind
THEN /\ temp' = ArgNum(ops[idx], 1 + Len(curNode.assumes))
/\ IF temp' = -1
THEN /\ PrintT("Illegal argument number")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_55"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED curNode
ELSE /\ IF temp' <= Len(curNode.assumes)
THEN /\ curNode' = Node[curNode.assumes[temp']]
ELSE /\ curNode' = Node[curNode.prove]
/\ pc' = "Lbl_62"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
opNode >>
ELSE /\ IF curNode.kind = OpArgKind
THEN /\ opNode' = Node[curNode.op]
/\ IF \/ opNode'.kind # UserDefinedOpKind
\/ opNode'.name # "LAMBDA"
THEN /\ PrintT("Selecting from operator argument that has no sub-part")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_56"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode >>
ELSE /\ IF ops[idx] \notin {"null", "@"}
THEN /\ PrintT("Incorrect selection from LAMBDA")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_57"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode >>
ELSE /\ IF /\ ops[idx] = "null"
/\ Len(args[idx]) # Len(opNode'.params)
THEN /\ PrintT("Incorrect number of arguments for LAMBDA")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_58"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode >>
ELSE /\ params' = params \o opNode'.params
/\ allArgs' = allArgs \o args[idx]
/\ curNode' = Node[opNode'.body]
/\ pc' = "Lbl_62"
/\ UNCHANGED idx
ELSE /\ IF curNode.kind \in {UserDefinedOpKind, BuiltInKind}
THEN /\ PrintT("Abort: should not have been able to choose this node.")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_59"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED curNode
ELSE /\ IF curNode.kind \in {AtNodeKind, DecimalKind, NumeralKind, StringKind,
FormalParamKind, ConstantDeclKind, VariableDeclKind,
BoundSymbolKind}
THEN /\ PrintT("Selected part has no subexpression")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_60"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED curNode
ELSE /\ IF curNode.kind = LabelKind
THEN /\ curNode' = Node[curNode.body]
/\ idx' = idx - 1
/\ pc' = "Lbl_62"
ELSE /\ PrintT("Unexpected node kind found in expression")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_61"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED curNode
/\ UNCHANGED << params,
allArgs,
opNode >>
/\ UNCHANGED temp
ELSE /\ PrintT("Bad value of mode")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_67"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED << params,
allArgs,
curNode,
opNode,
temp >>
/\ UNCHANGED newNode
/\ UNCHANGED newName
ELSE /\ IF curNode.kind = AssumeProveKind
THEN /\ PrintT("Selecting ASSUME/PROVE instead of expression")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_69"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_70"
/\ UNCHANGED idx
/\ UNCHANGED << params, allArgs, curNode, opNode, newName,
newNode, temp >>
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, subExprOf,
result, mode, prevMode, curContext, curName,
opDefArityFound, opDefArgs, firstFindingOpName,
nodeArity >>
Lbl_68 == /\ pc = "Lbl_68"
/\ idx' = idx + 1
/\ pc' = "Lbl_2"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_4 == /\ pc = "Lbl_4"
/\ newNode' = IF newName # null THEN LookUp(newName, curContext) ELSE null
/\ IF newNode' = null
THEN /\ PrintT("Unknown operator")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_5"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_6"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, nodeArity, temp >>
Lbl_5 == /\ pc = "Lbl_5"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1932, column 11.")
/\ pc' = "Lbl_6"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_6 == /\ pc = "Lbl_6"
/\ curNode' = newNode
/\ curName' = newName
/\ IF curNode'.kind \in
{UserDefinedOpKind, ThmOrAssumpDefKind,
ModuleInstanceKind, ConstantDeclKind, VariableDeclKind,
FormalParamKind, BuiltInKind, BoundSymbolKind}
THEN /\ IF curNode'.kind \in
{ConstantDeclKind, VariableDeclKind, FormalParamKind,
BuiltInKind, BoundSymbolKind}
THEN /\ IF idx # 1
THEN /\ PrintT("Abort: Impossible naming of declaration "
\o "or built-in operator.")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_7"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ IF Len(ops) # 1
THEN /\ PrintT("Can't take subexpression of this")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_8"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_9"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_9"
/\ UNCHANGED idx
ELSE /\ PrintT("Unexpected node kind")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_19"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, mode, prevMode,
curContext, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_9 == /\ pc = "Lbl_9"
/\ nodeArity' = Arity(curNode)
/\ IF expectedArity = 0
THEN /\ IF opDefArityFound + Len(args[idx]) # nodeArity'
THEN /\ PrintT("Wrong number of arguments")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_10"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_11"
/\ UNCHANGED idx
ELSE /\ IF expectedArity > 0
THEN /\ IF \E i \in 1..Len(curNode.params) :
curNode.params[i].arity > 0
THEN /\ PrintT("Higher-order operator selected "
\o "as operator argument")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_13"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_14"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_14"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode, temp >>
Lbl_11 == /\ pc = "Lbl_11"
/\ IF \E i \in 1..Len(args[idx]) :
Arity(Node[args[idx][i]]) #
ParamArity(curNode, i + opDefArityFound)
THEN /\ PrintT("Argument has wrong arity")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_12"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED opDefArgs
ELSE /\ opDefArgs' = opDefArgs \o args[idx]
/\ pc' = "Lbl_14"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_12 == /\ pc = "Lbl_12"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1959, column 26.")
/\ pc' = "Lbl_14"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_10 == /\ pc = "Lbl_10"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1954, column 25.")
/\ pc' = "Lbl_11"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_13 == /\ pc = "Lbl_13"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1965, column 32.")
/\ pc' = "Lbl_14"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_14 == /\ pc = "Lbl_14"
/\ opDefArityFound' = nodeArity
/\ IF curNode.kind \in {UserDefinedOpKind, ThmOrAssumpDefKind,
ConstantDeclKind, VariableDeclKind,
FormalParamKind, BoundSymbolKind}
THEN /\ IF /\ curNode.kind = UserDefinedOpKind
/\ ~ curNode.defined
/\ ~ Len(ops) = 1
THEN /\ PrintT("Can't refer to subexpression of "
\o "operator inside its definition")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_15"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_16"
/\ UNCHANGED idx
ELSE /\ IF (idx = Len(ops))
THEN /\ PrintT("Operator name incomplete")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_18"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_20"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArgs, firstFindingOpName,
opNode, newName, newNode, nodeArity, temp >>
Lbl_16 == /\ pc = "Lbl_16"
/\ IF /\ firstFindingOpName
/\ curNode.kind \in {UserDefinedOpKind, ThmOrAssumpDefKind}
THEN /\ subExprOf' = curNode
ELSE /\ TRUE
/\ UNCHANGED subExprOf
/\ IF idx # Len(ops)
THEN /\ params' = params \o curNode.params
/\ curName' = ""
/\ IF IsName(ops[idx+1])
THEN /\ mode' = "FollowingLabels"
ELSE /\ mode' = "FindingSubExpr"
/\ allArgs' = allArgs \o opDefArgs
/\ opDefArityFound' = 0
/\ opDefArgs' = << >>
/\ newNode' = Node[curNode.body]
/\ pc' = "Lbl_17"
ELSE /\ pc' = "Lbl_20"
/\ UNCHANGED << params, allArgs, mode, curName,
opDefArityFound, opDefArgs, newNode >>
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, curNode,
result, idx, prevMode, curContext,
firstFindingOpName, opNode, newName, nodeArity, temp >>
Lbl_17 == /\ pc = "Lbl_17"
/\ IF newNode.kind = SubstInKind
THEN /\ substInPrefix' = substInPrefix \o <<newNode>>
/\ newNode' = Node[newNode.body]
/\ pc' = "Lbl_17"
/\ UNCHANGED curNode
ELSE /\ IF mode = "FindingSubExpr"
THEN /\ curNode' = newNode
ELSE /\ TRUE
/\ UNCHANGED curNode
/\ pc' = "Lbl_20"
/\ UNCHANGED << substInPrefix, newNode >>
/\ UNCHANGED << ops, args, expectedArity, params, allArgs, subExprOf,
result, idx, mode, prevMode, curContext, curName,
opDefArityFound, opDefArgs, firstFindingOpName,
opNode, newName, nodeArity, temp >>
Lbl_15 == /\ pc = "Lbl_15"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1979, column 25.")
/\ pc' = "Lbl_16"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_18 == /\ pc = "Lbl_18"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2012, column 25.")
/\ pc' = "Lbl_20"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_7 == /\ pc = "Lbl_7"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1944, column 26.")
/\ pc' = "Lbl_9"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_8 == /\ pc = "Lbl_8"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1947, column 33.")
/\ pc' = "Lbl_9"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_19 == /\ pc = "Lbl_19"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2015, column 9.")
/\ pc' = "Lbl_20"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_20 == /\ pc = "Lbl_20"
/\ prevMode' = "FindingOpName"
/\ pc' = "Lbl_68"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, idx, mode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_3 == /\ pc = "Lbl_3"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 1928, column 11.")
/\ pc' = "Lbl_4"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_22 == /\ pc = "Lbl_22"
/\ curNode' = newNode
/\ IF expectedArity = 0
THEN /\ IF Len(args[idx]) # curNode'.arity
THEN /\ PrintT("bad arity")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_23"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_24"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_27"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_24 == /\ pc = "Lbl_24"
/\ IF \E i \in 1..Len(args[idx]) :
Arity(Node[args[idx][i]]) # 0
THEN /\ PrintT("Operator argument given to label")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_25"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_26"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_25 == /\ pc = "Lbl_25"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2037, column 20.")
/\ pc' = "Lbl_26"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_26 == /\ pc = "Lbl_26"
/\ allArgs' = allArgs \o args[idx]
/\ pc' = "Lbl_27"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
curNode, subExprOf, result, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_23 == /\ pc = "Lbl_23"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2033, column 20.")
/\ pc' = "Lbl_24"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_27 == /\ pc = "Lbl_27"
/\ params' = params \o curNode.params
/\ IF /\ idx < Len(ops)
/\ ~IsName(ops[idx+1])
THEN /\ mode' = "FindingSubExpr"
ELSE /\ TRUE
/\ UNCHANGED mode
/\ IF \/ mode' = "FindingSubExpr"
\/ idx = Len(ops)
THEN /\ curNode' = Node[curNode.body]
ELSE /\ TRUE
/\ UNCHANGED curNode
/\ prevMode' = "FollowingLabels"
/\ pc' = "Lbl_68"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, allArgs,
subExprOf, result, idx, curContext, curName,
opDefArityFound, opDefArgs, firstFindingOpName,
opNode, newName, newNode, nodeArity, temp >>
Lbl_21 == /\ pc = "Lbl_21"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2028, column 13.")
/\ pc' = "Lbl_22"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_62 == /\ pc = "Lbl_62"
/\ IF idx # Len(ops)
THEN /\ IF IsName(ops[idx+1])
THEN /\ pc' = "Lbl_63"
/\ UNCHANGED idx
ELSE /\ IF ops[idx+1] = ":"
THEN /\ PrintT("!: should not follow an operand selector")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_65"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_66"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_66"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_63 == /\ pc = "Lbl_63"
/\ IF curNode.kind = LabelKind
THEN /\ curNode' = Node[curNode.body]
/\ pc' = "Lbl_63"
/\ UNCHANGED << idx, mode, curContext, firstFindingOpName >>
ELSE /\ IF curNode.kind = LetInKind
THEN /\ curContext' = curNode.context
/\ mode' = "FindingOpName"
/\ firstFindingOpName' = FALSE
/\ pc' = "Lbl_66"
/\ UNCHANGED idx
ELSE /\ PrintT("A name not following the selector of a LET")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_64"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
/\ UNCHANGED << mode, curContext,
firstFindingOpName >>
/\ UNCHANGED curNode
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, prevMode, curName,
opDefArityFound, opDefArgs, opNode, newName, newNode,
nodeArity, temp >>
Lbl_64 == /\ pc = "Lbl_64"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2263, column 26.")
/\ pc' = "Lbl_66"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_65 == /\ pc = "Lbl_65"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2266, column 26.")
/\ pc' = "Lbl_66"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_66 == /\ pc = "Lbl_66"
/\ prevMode' = "FindingSubExpr"
/\ pc' = "Lbl_68"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, idx, mode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_28 == /\ pc = "Lbl_28"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2060, column 14.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_29 == /\ pc = "Lbl_29"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2067, column 14.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_30 == /\ pc = "Lbl_30"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2079, column 17.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_32 == /\ pc = "Lbl_32"
/\ curNode' = Node[curNode.operands[temp]]
/\ IF \/ curNode'.kind # OpApplKind
\/ Node[curNode'.operator].kind # BuiltInKind
\/ Node[curNode'.operator].name # "$Pair"
THEN /\ PrintT("Expecting $Pair(...)")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_33"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_34"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_34 == /\ pc = "Lbl_34"
/\ curNode' = Node[curNode.operands[2]]
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_33 == /\ pc = "Lbl_33"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2100, column 18.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_31 == /\ pc = "Lbl_31"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2094, column 18.")
/\ pc' = "Lbl_32"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_36 == /\ pc = "Lbl_36"
/\ temp' = ArgNum( ops[idx], Len(curNode.operands))
/\ IF temp' = -1
THEN /\ PrintT("Incorrect subexpression name")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_37"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_38"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity >>
Lbl_37 == /\ pc = "Lbl_37"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2114, column 18.")
/\ pc' = "Lbl_38"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_38 == /\ pc = "Lbl_38"
/\ curNode' = Node[curNode.operands[temp]]
/\ IF \/ curNode'.kind # OpApplKind
\/ Node[curNode'.operator].kind # BuiltInKind
\/ Node[curNode'.operator].name # "$Pair"
THEN /\ PrintT("Expecting $Pair(...)")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_39"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_40"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_39 == /\ pc = "Lbl_39"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2120, column 18.")
/\ pc' = "Lbl_40"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_40 == /\ pc = "Lbl_40"
/\ idx' = idx+1
/\ temp' = ArgNum(ops[idx'], 2)
/\ IF temp' = -1
THEN /\ PrintT("Incorrect subexpression name")
/\ IF debug
THEN /\ pc' = "Lbl_41"
ELSE /\ pc' = "Done"
ELSE /\ pc' = "Lbl_43"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity >>
Lbl_41 == /\ pc = "Lbl_41"
/\ idx' = idx
/\ pc' = "Lbl_42"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_42 == /\ pc = "Lbl_42"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2125, column 18.")
/\ pc' = "Lbl_43"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_43 == /\ pc = "Lbl_43"
/\ curNode' = Node[curNode.operands[temp]]
/\ IF curNode' = null
THEN /\ PrintT("Selecting OTHER")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_44"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_62"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_44 == /\ pc = "Lbl_44"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2129, column 18.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_35 == /\ pc = "Lbl_35"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2110, column 18.")
/\ pc' = "Lbl_36"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_46 == /\ pc = "Lbl_46"
/\ curNode' = Node[curNode.operands[temp]]
/\ IF temp > 1
THEN /\ IF \/ curNode'.kind # OpApplKind
\/ Node[curNode'.operator].kind # BuiltInKind
\/ Node[curNode'.operator].name # "$Pair"
THEN /\ PrintT("Unexpected expression node found.")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_47"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_48"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_62"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_48 == /\ pc = "Lbl_48"
/\ curNode' = Node[curNode.operands[2]]
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_47 == /\ pc = "Lbl_47"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2148, column 26.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_45 == /\ pc = "Lbl_45"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2141, column 19.")
/\ pc' = "Lbl_46"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_50 == /\ pc = "Lbl_50"
/\ curNode' = Node[curNode.operands[temp]]
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_49 == /\ pc = "Lbl_49"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2164, column 25.")
/\ pc' = "Lbl_50"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_52 == /\ pc = "Lbl_52"
/\ curNode' = Node[curNode.operands[1]]
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_51 == /\ pc = "Lbl_51"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2189, column 32.")
/\ pc' = "Lbl_52"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_53 == /\ pc = "Lbl_53"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2194, column 32.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_54 == /\ pc = "Lbl_54"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2201, column 12.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_55 == /\ pc = "Lbl_55"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2209, column 18.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_56 == /\ pc = "Lbl_56"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2224, column 9.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_57 == /\ pc = "Lbl_57"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2226, column 9.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_58 == /\ pc = "Lbl_58"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2229, column 9.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_59 == /\ pc = "Lbl_59"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2236, column 7.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_60 == /\ pc = "Lbl_60"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2241, column 10.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_61 == /\ pc = "Lbl_61"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2250, column 8.")
/\ pc' = "Lbl_62"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_67 == /\ pc = "Lbl_67"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2272, column 8.")
/\ pc' = "Lbl_68"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_69 == /\ pc = "Lbl_69"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2280, column 10.")
/\ pc' = "Lbl_70"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_70 == /\ pc = "Lbl_70"
/\ IF expectedArity < 0
THEN /\ IF \/ prevMode # "FindingOpName"
\/ curNode.kind \notin {UserDefinedOpKind, ThmOrAssumpDefKind}
THEN /\ PrintT("Should have selected a definition, but didn't.")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_71"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_72"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_73"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_72 == /\ pc = "Lbl_72"
/\ result' = curNode
/\ pc' = "Finished"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_71 == /\ pc = "Lbl_71"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2286, column 17.")
/\ pc' = "Lbl_72"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_73 == /\ pc = "Lbl_73"
/\ IF expectedArity > 0
THEN /\ temp' = Len(params) + IF \/ prevMode = "FindingOpName"
\/ curNode.kind = OpArgKind
THEN Arity(curNode)
ELSE 0
/\ IF expectedArity # temp'
THEN /\ PrintT("Expect arity = " \o ToString(expectedArity)
\o ", but found arity = " \o ToString(temp'))
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_74"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_75"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_75"
/\ UNCHANGED << idx, temp >>
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity >>
Lbl_74 == /\ pc = "Lbl_74"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2298, column 18.")
/\ pc' = "Lbl_75"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_75 == /\ pc = "Lbl_75"
/\ IF /\ prevMode = "FindingOpName"
/\ Len(params) + Len(substInPrefix) > 0
THEN /\ temp' = [i \in 1..Len(curNode.params) |->
[curNode.params[i] EXCEPT !.name = "New " \o @]]
/\ curNode' = [kind |-> OpApplKind,
operands |-> temp',
operator |-> curNode,
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>]
/\ params' = params \o temp'
/\ allArgs' = allArgs \o opDefArgs
ELSE /\ TRUE
/\ UNCHANGED << params, allArgs, curNode, temp >>
/\ IF curNode'.kind = OpArgKind
THEN /\ IF expectedArity = 0
THEN /\ PrintT("Selected Operator Argument when expression expected.")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_76"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ IF expectedArity # Len(params') + curNode'.arity
THEN /\ PrintT("Selected operator has wrong arity.")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_77"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ IF Len(params') + Len(substInPrefix) > 0
THEN /\ pc' = "Lbl_78"
ELSE /\ pc' = "Lbl_79"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_79"
/\ UNCHANGED idx
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, subExprOf,
result, mode, prevMode, curContext, curName,
opDefArityFound, opDefArgs, firstFindingOpName,
opNode, newName, newNode, nodeArity >>
Lbl_76 == /\ pc = "Lbl_76"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2332, column 12.")
/\ pc' = "Lbl_79"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_77 == /\ pc = "Lbl_77"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2334, column 12.")
/\ pc' = "Lbl_79"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_78 == /\ pc = "Lbl_78"
/\ temp' = [i \in 1..curNode.arity |->
[name |-> "NewParam" \o NumToString(i),
arity |-> 0]]
/\ curNode' = [kind |-> OpApplKind,
operands |-> temp',
operator |-> Node[curNode.op],
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>]
/\ params' = params \o temp'
/\ pc' = "Lbl_79"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, allArgs,
subExprOf, result, idx, mode, prevMode, curContext,
curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity >>
Lbl_79 == /\ pc = "Lbl_79"
/\ IF curNode.kind \in {UserDefinedOpKind, ConstantDeclKind, VariableDeclKind,
FormalParamKind, BuiltInKind, BoundSymbolKind,
ThmOrAssumpDefKind}
THEN /\ IF expectedArity > 0
THEN /\ result' = [kind |-> OpArgKind,
name |-> curNode.name,
op |-> curNode,
arity |-> expectedArity]
ELSE /\ IF expectedArity = 0
THEN /\ result' = [kind |-> OpApplKind,
operands |-> opDefArgs,
operator |-> curNode,
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>,
subExprOf |-> subExprOf]
ELSE /\ TRUE
/\ UNCHANGED result
/\ pc' = "Finished"
/\ UNCHANGED temp
ELSE /\ IF curNode.kind = OpArgKind
THEN /\ result' = curNode
/\ pc' = "Finished"
/\ UNCHANGED temp
ELSE /\ temp' = Len(substInPrefix)
/\ pc' = "Lbl_80"
/\ UNCHANGED result
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity >>
Lbl_80 == /\ pc = "Lbl_80"
/\ IF temp > 0
THEN /\ curNode' = [kind |-> SubstInKind,
body |-> curNode ,
subst |-> substInPrefix[temp].subst ]
/\ temp' = temp - 1
/\ pc' = "Lbl_80"
/\ UNCHANGED idx
ELSE /\ IF expectedArity > 0
THEN /\ IF Len(params) # expectedArity
THEN /\ PrintT("Selection has wrong arity")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_81"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_82"
/\ UNCHANGED idx
ELSE /\ IF Len(params) # Len(allArgs)
THEN /\ PrintT("Abort: number of params # num of args")
/\ IF debug
THEN /\ idx' = idx
/\ pc' = "Lbl_83"
ELSE /\ pc' = "Done"
/\ UNCHANGED idx
ELSE /\ pc' = "Lbl_84"
/\ UNCHANGED idx
/\ UNCHANGED << curNode, temp >>
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity >>
Lbl_82 == /\ pc = "Lbl_82"
/\ result' = [kind |-> OpArgKind,
op |-> [kind |-> UserDefinedOpKind,
name |-> "LAMBDA",
body |-> curNode,
params |-> params,
arity |-> Len(params),
defined |-> TRUE,
source |-> null],
name |-> "LAMBDA"]
/\ pc' = "Finished"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_84 == /\ pc = "Lbl_84"
/\ IF Len(params) = 0
THEN /\ result' = [kind |-> LabelKind,
name |-> "$Subexpression",
arity |-> 0,
params |-> << >>,
body |-> curNode,
subExprOf |-> subExprOf]
ELSE /\ result' = [kind |-> OpApplKind,
operator |-> [kind |-> UserDefinedOpKind,
name |-> "LAMBDA",
body |-> curNode,
params |-> params,
arity |-> Len(params),
defined |-> TRUE,
source |-> null],
operands |-> allArgs,
unboundedBoundSymbols |-> <<>>,
boundedBoundSymbols |-> << >>,
ranges |-> << >>,
subExprOf |-> subExprOf]
/\ pc' = "Finished"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, idx, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_81 == /\ pc = "Lbl_81"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2400, column 22.")
/\ pc' = "Lbl_82"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Lbl_83 == /\ pc = "Lbl_83"
/\ idx' = idx
/\ Assert(FALSE,
"Failure of assertion at line line 1887, column 38 of macro called at line 2412, column 22.")
/\ pc' = "Lbl_84"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, mode, prevMode,
curContext, curName, opDefArityFound, opDefArgs,
firstFindingOpName, opNode, newName, newNode,
nodeArity, temp >>
Finished == /\ pc = "Finished"
/\ PrintT("Result: ")
/\ PrintT(result)
/\ pc' = "Done"
/\ UNCHANGED << ops, args, expectedArity, substInPrefix, params,
allArgs, curNode, subExprOf, result, idx, mode,
prevMode, curContext, curName, opDefArityFound,
opDefArgs, firstFindingOpName, opNode, newName,
newNode, nodeArity, temp >>
Next == Lbl_1 \/ Lbl_2 \/ Lbl_68 \/ Lbl_4 \/ Lbl_5 \/ Lbl_6 \/ Lbl_9
\/ Lbl_11 \/ Lbl_12 \/ Lbl_10 \/ Lbl_13 \/ Lbl_14 \/ Lbl_16 \/ Lbl_17
\/ Lbl_15 \/ Lbl_18 \/ Lbl_7 \/ Lbl_8 \/ Lbl_19 \/ Lbl_20 \/ Lbl_3
\/ Lbl_22 \/ Lbl_24 \/ Lbl_25 \/ Lbl_26 \/ Lbl_23 \/ Lbl_27 \/ Lbl_21
\/ Lbl_62 \/ Lbl_63 \/ Lbl_64 \/ Lbl_65 \/ Lbl_66 \/ Lbl_28 \/ Lbl_29
\/ Lbl_30 \/ Lbl_32 \/ Lbl_34 \/ Lbl_33 \/ Lbl_31 \/ Lbl_36 \/ Lbl_37
\/ Lbl_38 \/ Lbl_39 \/ Lbl_40 \/ Lbl_41 \/ Lbl_42 \/ Lbl_43 \/ Lbl_44
\/ Lbl_35 \/ Lbl_46 \/ Lbl_48 \/ Lbl_47 \/ Lbl_45 \/ Lbl_50 \/ Lbl_49
\/ Lbl_52 \/ Lbl_51 \/ Lbl_53 \/ Lbl_54 \/ Lbl_55 \/ Lbl_56 \/ Lbl_57
\/ Lbl_58 \/ Lbl_59 \/ Lbl_60 \/ Lbl_61 \/ Lbl_67 \/ Lbl_69 \/ Lbl_70
\/ Lbl_72 \/ Lbl_71 \/ Lbl_73 \/ Lbl_74 \/ Lbl_75 \/ Lbl_76 \/ Lbl_77
\/ Lbl_78 \/ Lbl_79 \/ Lbl_80 \/ Lbl_82 \/ Lbl_84 \/ Lbl_81 \/ Lbl_83
\/ Finished
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
NotDone == pc # "Done"
(*************************************************************************)
(* To print a trace of an execution that doesn't produce an error, add *)
(* "INVARIANT NotDone" to Subexpression.cfg . *)
(*************************************************************************)
=============================================================================
************************* end file Subexpression.tla ****************************/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment