Created
April 1, 2020 19:02
-
-
Save nishantjr/4a9bd4570e07f5330d6f4ab67a2d6634 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Kore version 0.0.1.0 | |
Git: | |
revision: c2c9bca46d87a2e5237b40680cd667b5856ab3e2 | |
branch: HEAD | |
last commit: 2020 Apr 1 13:21:24 -0500 | |
Build date: 2020 Apr 02 00:31:47 +0530 | |
[1/60] run: execution t/kool/dynamic-dispatch-1.dfy | |
FAILED: .build/t/kool/dynamic-dispatch-1.dfy.execution-run | |
./kdafny run --definition "execution" "t/kool/dynamic-dispatch-1.dfy" > ".build/t/kool/dynamic-dispatch-1.dfy.execution-run" || (cat .build/t/kool/dynamic-dispatch-1.dfy.execution-run ; false) | |
kore-exec: [2020-04-02 00:31:56.412331544] Error (ErrorException): | |
While applying axiom: | |
left: | |
/* Fn Sfc */ | |
Lbl'-LT-'generatedTop'-GT-'{}( | |
/* Fn Sfc */ | |
Lbl'-LT-'T'-GT-'{}( | |
/* Fn Sfc */ | |
Lbl'-LT-'threads'-GT-'{}( | |
/* Fn Sfc */ | |
/* builtin: */ | |
Lbl'Unds'ThreadCellMap'Unds'{}( | |
/* element: */ LblThreadCellMapItem{}( | |
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{}, | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'thread'-GT-'{}( | |
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{}, | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'k'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortExp{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsLSqBUndsRSqBUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa */ | |
VarK0:SortExp{}, | |
/* Fl Fn D Sfa */ | |
VarHOLE:SortExps{} | |
) | |
), | |
/* Fl Fn D Sfa */ VarDotVar4:SortK{} | |
) | |
), | |
/* Fl Fn D Sfa */ Var'Unds'1:SortControlCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'2:SortEnvCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'3:SortHoldsCell{} | |
) | |
), | |
/* opaque child: */ /* Fl Fn D Sfa */ | |
VarDotVar2:SortThreadCellMap{} | |
) | |
), | |
/* Fl Fn D Sfa */ Var'Unds'4:SortStoreCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'5:SortBusyCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'6:SortTerminatedCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'7:SortInputCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'8:SortOutputCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'9:SortNextLocCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'10:SortClassesCell{} | |
), | |
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{} | |
) | |
requires: | |
/* Spa */ | |
\equals{SortBool{}, SortGeneratedTopCell{}}( | |
/* Fn Spa */ | |
Lbl'Unds'andBool'Unds'{}( | |
/* Fl Fn D Spa */ | |
Lbl'Unds'andBool'Unds'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true"), | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true") | |
), | |
/* Fn Spa */ | |
LblnotBool'Unds'{}( | |
/* Fn Spa */ | |
LblisKResult{}( | |
/* Fl Fn D Spa */ | |
kseq{}( | |
/* Fl Fn D Spa */ | |
/* Inj: */ inj{SortExps{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ VarHOLE:SortExps{} | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true") | |
) | |
existentials: | |
[] | |
right: | |
/* Fn Spa */ | |
Lbl'-LT-'generatedTop'-GT-'{}( | |
/* Fn Spa */ | |
Lbl'-LT-'T'-GT-'{}( | |
/* Fn Spa */ | |
Lbl'-LT-'threads'-GT-'{}( | |
/* Fn Spa */ | |
/* builtin: */ | |
Lbl'Unds'ThreadCellMap'Unds'{}( | |
/* element: */ LblThreadCellMapItem{}( | |
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{}, | |
/* Fl Fn D Spa */ | |
Lbl'-LT-'thread'-GT-'{}( | |
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{}, | |
/* Fl Fn D Spa */ | |
Lbl'-LT-'k'-GT-'{}( | |
/* Fl Fn D Spa */ | |
kseq{}( | |
/* Fl Fn D Spa */ | |
/* Inj: */ inj{SortExps{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ VarHOLE:SortExps{} | |
), | |
/* Fl Fn D Spa */ | |
kseq{}( | |
/* Fl Fn D Spa */ | |
Lbl'Hash'freezer'UndsLSqBUndsRSqBUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps0'Unds'{}( | |
/* Fl Fn D Spa */ | |
kseq{}( | |
/* Fl Fn D Spa */ | |
/* Inj: */ inj{SortExp{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ | |
VarK0:SortExp{} | |
), | |
/* Fl Fn D Sfa Cl */ | |
dotk{}() | |
) | |
), | |
/* Fl Fn D Sfa */ VarDotVar4:SortK{} | |
) | |
) | |
), | |
/* Fl Fn D Sfa */ Var'Unds'1:SortControlCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'2:SortEnvCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'3:SortHoldsCell{} | |
) | |
), | |
/* opaque child: */ /* Fl Fn D Sfa */ | |
VarDotVar2:SortThreadCellMap{} | |
) | |
), | |
/* Fl Fn D Sfa */ Var'Unds'4:SortStoreCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'5:SortBusyCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'6:SortTerminatedCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'7:SortInputCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'8:SortOutputCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'9:SortNextLocCell{}, | |
/* Fl Fn D Sfa */ Var'Unds'10:SortClassesCell{} | |
), | |
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{} | |
) | |
ensures: | |
/* D Sfa */ \top{SortGeneratedTopCell{}}() | |
from the initial configuration: | |
\and{SortGeneratedTopCell{}}( | |
/* term: */ | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'generatedTop'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'T'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'threads'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
/* builtin: */ | |
/* concrete element: */ LblThreadCellMapItem{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'id'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("0") | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'thread'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'id'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("0") | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'k'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortExp{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa */ | |
LbllookupMember'LParUndsCommUndsRParUnds'DAFNY'Unds'Exp'Unds'List'Unds'Id{}( | |
/* Fl Fn D Sfa */ | |
/* builtin: */ | |
Lbl'Unds'List'Unds'{}( | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("1") | |
) | |
) | |
) | |
), | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
Lbl'Stop'Map{}() | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(), | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblthis'Unds'DAFNY-SYNTAX'Unds'Exp{}() | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'control'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'fstack'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
/* builtin: */ | |
LblListItem{}( | |
/* Fl Fn D Sfc */ | |
LblfstackFrame'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Map'Unds'K'Unds'List'Unds'Type'Unds'K{}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}(), | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
), | |
/* Fl Fn D Sfa */ | |
/* builtin: */ Lbl'Stop'List{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortCrntObjCell{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'crntObj'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'crntClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'envStack'-GT-'{}( | |
/* Fl Fn D Sfa */ | |
/* builtin: */ | |
Lbl'Stop'List{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'LocationCell{}() | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'xstack'-GT-'{}( | |
/* Fl Fn D Sfa */ | |
/* builtin: */ Lbl'Stop'List{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'returnType'-GT-'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'crntObj'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'crntClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'envStack'-GT-'{}( | |
/* Fl Fn D Sfa */ | |
/* builtin: */ | |
Lbl'Unds'List'Unds'{}( | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("1") | |
) | |
) | |
) | |
), | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
Lbl'Stop'Map{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'LocationCell{}() | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'env'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'holds'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'store'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
/* builtin: */ | |
Lbl'Unds'Map'Unds'{}( | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("0") | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortVal{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ | |
LblobjectClosure'LParUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Id'Unds'List{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"), | |
/* Fl Fn D Sfa */ | |
/* builtin: */ | |
Lbl'Unds'List'Unds'{}( | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("1") | |
) | |
) | |
) | |
), | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("1") | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortVal{}, SortKItem{}}( | |
/* Fl Fn D Sfc */ | |
LblmethodClosure'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Type'Unds'Id'Unds'Int'Unds'Params'Unds'Stmt{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Unds'-'-GT-UndsUnds'DAFNY-SYNTAX'Unds'Type'Unds'Types'Unds'Type{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("0"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortBlock{}, SortStmt{}}( | |
/* Fl Fn D Sfc */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortVal{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}("\x0a") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'busy'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'terminated'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}() | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'input'-GT-'{}( | |
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}() | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'output'-GT-'{}( | |
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'nextLoc'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("2") | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'classes'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
/* builtin: */ | |
Lbl'Unds'ClassDataCellMap'Unds'{}( | |
/* concrete element: */ LblClassDataCellMapItem{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'classData'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'baseClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'declarations'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmts{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}() | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("1") | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
Lbl'Unds'ClassDataCellMap'Unds'{}( | |
/* concrete element: */ LblClassDataCellMapItem{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'classData'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'baseClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'declarations'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmts{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}() | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("2") | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
/* concrete element: */ LblClassDataCellMapItem{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main") | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'classData'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'baseClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object") | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'declarations'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortKItem{}}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfc */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortVal{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}("\x0a") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
) | |
)) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'generatedCounter'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") | |
) | |
), | |
\and{SortGeneratedTopCell{}}( | |
/* predicate: */ | |
/* D Sfa */ \top{SortGeneratedTopCell{}}(), | |
/* substitution: */ | |
\top{SortGeneratedTopCell{}}() | |
)) | |
with the unifier: | |
\and{_PREDICATE{}}( | |
/* term: */ | |
/* D Sfa */ \top{_PREDICATE{}}(), | |
\and{_PREDICATE{}}( | |
/* predicate: */ | |
\and{_PREDICATE{}}( | |
/* Sfc */ | |
\ceil{SortBool{}, _PREDICATE{}}( | |
/* Fn Sfc */ | |
LblisKResult{}( | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortExps{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ VarHOLE:SortExps{} | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Sfc */ | |
\equals{SortBool{}, _PREDICATE{}}( | |
/* Fn Sfc */ | |
LblnotBool'Unds'{}( | |
/* Fn Sfc */ | |
LblisKResult{}( | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortExps{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ VarHOLE:SortExps{} | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true") | |
), | |
/* Sfa */ | |
\equals{SortExp{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa */ | |
LbllookupMember'LParUndsCommUndsRParUnds'DAFNY'Unds'Exp'Unds'List'Unds'Id{}( | |
/* Fl Fn D Sfa */ | |
/* builtin: */ | |
Lbl'Unds'List'Unds'{}( | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("1") | |
) | |
) | |
) | |
), | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}() | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsLSqBUndsRSqBUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa */ VarK0:SortExp{}, | |
/* Fl Fn D Sfa */ VarHOLE:SortExps{} | |
) | |
) | |
)), | |
/* substitution: */ | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortIdCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{}, | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'id'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spc */ | |
\equals{SortControlCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'1:SortControlCell{}, | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'control'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'fstack'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
/* builtin: */ | |
LblListItem{}( | |
/* Fl Fn D Sfc */ | |
LblfstackFrame'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Map'Unds'K'Unds'List'Unds'Type'Unds'K{}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}(), | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
), | |
/* Fl Fn D Sfa */ | |
/* builtin: */ Lbl'Stop'List{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortCrntObjCell{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'crntObj'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'crntClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'envStack'-GT-'{}( | |
/* Fl Fn D Sfa */ | |
/* builtin: */ Lbl'Stop'List{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'LocationCell{}() | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'xstack'-GT-'{}( | |
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'returnType'-GT-'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main") | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'crntObj'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'crntClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'envStack'-GT-'{}( | |
/* Fl Fn D Sfa */ | |
/* builtin: */ | |
Lbl'Unds'List'Unds'{}( | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("1") | |
) | |
) | |
) | |
), | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ Lbl'Stop'LocationCell{}() | |
) | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spc */ | |
\equals{SortClassesCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'10:SortClassesCell{}, | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'classes'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
/* builtin: */ | |
Lbl'Unds'ClassDataCellMap'Unds'{}( | |
/* concrete element: */ LblClassDataCellMapItem{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'classData'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'baseClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'declarations'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmts{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}() | |
) | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("1") | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
Lbl'Unds'ClassDataCellMap'Unds'{}( | |
/* concrete element: */ LblClassDataCellMapItem{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'classData'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'baseClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'declarations'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmts{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}() | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("2") | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
), | |
/* concrete element: */ LblClassDataCellMapItem{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main") | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'classData'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'className'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'baseClass'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object") | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'declarations'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
kseq{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortKItem{}}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfc */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortVal{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}("\x0a") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
) | |
)) | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortEnvCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'2:SortEnvCell{}, | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'env'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Map{}() | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortHoldsCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'3:SortHoldsCell{}, | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'holds'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Map{}() | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spc */ | |
\equals{SortStoreCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'4:SortStoreCell{}, | |
/* Fl Fn D Sfc */ | |
Lbl'-LT-'store'-GT-'{}( | |
/* Fl Fn D Sfc */ | |
/* builtin: */ | |
Lbl'Unds'Map'Unds'{}( | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("0") | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortVal{}, SortKItem{}}( | |
/* Fl Fn D Sfa */ | |
LblobjectClosure'LParUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Id'Unds'List{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"), | |
/* Fl Fn D Sfa */ | |
/* builtin: */ | |
Lbl'Unds'List'Unds'{}( | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Main") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortInt{}}("1") | |
) | |
) | |
) | |
), | |
LblListItem{}( | |
/* Fl Fn D Sfa Cl */ | |
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"Object"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ Lbl'Stop'Map{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortInt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("1") | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortVal{}, SortKItem{}}( | |
/* Fl Fn D Sfc */ | |
LblmethodClosure'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Type'Unds'Id'Unds'Int'Unds'Params'Unds'Stmt{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Unds'-'-GT-UndsUnds'DAFNY-SYNTAX'Unds'Type'Unds'Types'Unds'Type{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}() | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"), | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ \dv{SortInt{}}("0"), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortBlock{}, SortStmt{}}( | |
/* Fl Fn D Sfc */ | |
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C1"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}( | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortDecl{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortType{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"C2"), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
), | |
/* Fl Fn D Sfc */ | |
/* Inj: */ inj{SortStmt{}, SortStmts{}}( | |
/* Fl Fn D Sfa */ | |
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}( | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o1") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m1") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}(" ") | |
), | |
/* Fl Fn D Sfa */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortId{}, SortExp{}}( | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"o2") | |
), | |
/* Fl Fn D Sfa Cl */ | |
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ | |
"m2") | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
), | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortVals{}, SortExps{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortString{}, SortVal{}}( | |
/* Fl Fn D Sfa Cl */ | |
/* builtin: */ | |
\dv{SortString{}}("\x0a") | |
), | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}() | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortBusyCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'5:SortBusyCell{}, | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'busy'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}() | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortTerminatedCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'6:SortTerminatedCell{}, | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'terminated'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}() | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortInputCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'7:SortInputCell{}, | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'input'-GT-'{}( | |
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}() | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortOutputCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'8:SortOutputCell{}, | |
/* Fl Fn D Sfa */ | |
Lbl'-LT-'output'-GT-'{}( | |
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}() | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortNextLocCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ Var'Unds'9:SortNextLocCell{}, | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'nextLoc'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("2") | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortGeneratedCounterCell{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}, | |
/* Fl Fn D Sfa Cl */ | |
Lbl'-LT-'generatedCounter'-GT-'{}( | |
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") | |
) | |
), | |
\and{_PREDICATE{}}( | |
/* Spa */ | |
\equals{SortThreadCellMap{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ VarDotVar2:SortThreadCellMap{}, | |
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'ThreadCellMap{}() | |
), | |
/* Spa */ | |
\equals{SortK{}, _PREDICATE{}}( | |
/* Fl Fn D Sfa */ VarDotVar4:SortK{}, | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cl */ | |
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(), | |
/* Fl Fn D Sfa Cl */ | |
kseq{}( | |
/* Fl Fn D Sfa Cli */ | |
/* Inj: */ inj{SortStmt{}, SortKItem{}}( | |
/* Fl Fn D Sfa Cl */ | |
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}( | |
/* Fl Fn D Sfa Cl */ | |
Lblthis'Unds'DAFNY-SYNTAX'Unds'Exp{}() | |
) | |
), | |
/* Fl Fn D Sfa Cl */ dotk{}() | |
) | |
) | |
) | |
))))))))))))) | |
)) | |
Failed substitution coverage check! | |
The substitution (above, in the unifier) did not cover the axiom variables: | |
VarHOLE:SortExps{} VarK0:SortExp{} | |
in the left-hand side of the axiom. | |
CallStack (from HasCallStack): | |
error, called at src/Kore/Step/Step.hs:394:6 in kore-0.0.1.0-CDi4oyRprcp5AMiB47zztY:Kore.Step.Step | |
[Error] Critical: Haskell Backend execution failed with code 1 and produced no | |
output. | |
ninja: build stopped: subcommand failed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment