coffee/coffee.pygments
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
This repository has been archived on 2024-06-20. You can view files and clone it, but you cannot make any changes to it's state, such as pushing and creating new issues, pull requests or comments.
coffee.pygments/tests/examplefiles/fstar/example.fst.output
Matthäus G. Chajdas 23d17d472b Update tests.
2022-06-19 10:06:12 +02:00

14459 lines
294 KiB
Text
Generated
Raw Permalink Blame History

'(*' Comment
'\n Copyright 2020 Microsoft Research\n\n Licensed under the Apache License, Version 2.0 ' Comment
'(' Comment
'the "License"' Comment
')' Comment
';\n you may not use this file except in compliance with the License.\n You may obtain a copy of the License at\n\n http://www.apache.org/licenses/LICENSE-2.0\n\n Unless required by applicable law or agreed to in writing, software\n distributed under the License is distributed on an "AS IS" BASIS,\n WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n See the License for the specific language governing permissions and\n limitations under the License.\n' Comment
'*)' Comment
'\n\n' Text
'module' Keyword
' ' Text
'Steel' Name.Namespace
'.' Punctuation
'Semantics' Name.Namespace
'.' Punctuation
'Hoare' Name.Namespace
'.' Punctuation
'MST' Name.Class
'\n\n' Text
'module' Keyword
' ' Text
'P' Name.Class
' ' Text
'=' Operator
' ' Text
'FStar' Name.Namespace
'.' Punctuation
'Preorder' Name.Class
'\n\n' Text
'open' Keyword
' ' Text
'FStar' Name.Namespace
'.' Punctuation
'Tactics' Name.Class
'\n\n' Text
'open' Keyword
' ' Text
'NMST' Name.Class
'\n\n\n' Text
'(*' Comment
'\n ' Comment
'*' Comment
' This module provides a semantic model for a combined effect of\n ' Comment
'*' Comment
' divergence, state, and parallel composition of atomic actions.\n ' Comment
'*' Comment
'\n ' Comment
'*' Comment
' It is built over a monotonic state effect -- so that we can give\n ' Comment
'*' Comment
' lock semantics using monotonicity\n ' Comment
'*' Comment
'\n ' Comment
'*' Comment
' It also builds a generic separation-logic-style program logic\n ' Comment
'*' Comment
' for this effect, in a partial correctness setting.\n\n ' Comment
'*' Comment
' It is also be possible to give a variant of this semantics for\n ' Comment
'*' Comment
' total correctness. However, we specifically focus on partial correctness\n ' Comment
'*' Comment
' here so that this semantics can be instantiated with lock operations,\n ' Comment
'*' Comment
' which may deadlock. See ParTot.fst for a total-correctness variant of\n ' Comment
'*' Comment
' these semantics.\n ' Comment
'*' Comment
'\n ' Comment
'*' Comment
' The program logic is specified in the Hoare-style pre- and postconditions\n' Comment
'*)' Comment
'\n\n\n' Text
"/// Disabling projectors because we don't use them and they increase the typechecking time" Comment
'\n\n' Text
'#' Operator
'push' Name
'-' Operator
'options' Name
' ' Text
'"' Literal.String.Double
'--fuel 0 --ifuel 2 --z3rlimit 20 --print_implicits --print_universes ' Literal.String.Double
'\\\n' Literal.String.Double
" --using_facts_from 'Prims FStar.Pervasives FStar.Preorder MST NMST Steel.Semantics.Hoare.MST'" Literal.String.Double
'"' Literal.String.Double
'\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Begin state defn ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n\n' Text
'/// We start by defining some basic notions for a commutative monoid.' Comment
'\n' Text
'///' Comment
'\n' Text
'/// We could reuse FStar.Algebra.CommMonoid, but this style with' Comment
'\n' Text
'/// quanitifers was more convenient for the proof done here.' Comment
'\n\n\n' Text
'let' Keyword.Declaration
' ' Text
'symmetry' Name
' ' Text
'#' Operator
'a' Name
' ' Text
'(' Operator
'equals' Name
':' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
'.' Operator
' ' Text
'{' Operator
':' Operator
'pattern' Name
' ' Text
'(' Operator
'x' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'y' Name
')' Operator
'}' Operator
'\n ' Text
'x' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'y' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'y' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'x' Name
' ' Text
'// Test' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'transitive' Name
' ' Text
'#' Operator
'a' Name
' ' Text
'(' Operator
'equals' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'z' Name
'.' Operator
' ' Text
'x' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'y' Name
' ' Text
'/\\' Operator
' ' Text
'y' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'z' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'x' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'z' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'associative' Name
' ' Text
'#' Operator
'a' Name
' ' Text
'(' Operator
'equals' Name
':' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'f' Name
':' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
')' Operator
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'z' Name
'.' Operator
'\n ' Text
'f' Name
' ' Text
'x' Name
' ' Text
'(' Operator
'f' Name
' ' Text
'y' Name
' ' Text
'z' Name
')' Operator
' ' Text
'`equals`' Operator.Word
' ' Text
'f' Name
' ' Text
'(' Operator
'f' Name
' ' Text
'x' Name
' ' Text
'y' Name
')' Operator
' ' Text
'z' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'commutative' Name
' ' Text
'#' Operator
'a' Name
' ' Text
'(' Operator
'equals' Name
':' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'f' Name
':' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
'.' Operator
'{' Operator
':' Operator
'pattern' Name
' ' Text
'f' Name
' ' Text
'x' Name
' ' Text
'y' Name
'}' Operator
'\n ' Text
'f' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'f' Name
' ' Text
'y' Name
' ' Text
'x' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'is_unit' Name
' ' Text
'#' Operator
'a' Name
' ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
' ' Text
'(' Operator
'equals' Name
':' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'f' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'y' Name
'.' Operator
' ' Text
'{' Operator
':' Operator
'pattern' Name
' ' Text
'f' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'\\/' Operator
' ' Text
'f' Name
' ' Text
'y' Name
' ' Text
'x' Name
'}' Operator
'\n ' Text
'f' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'y' Name
' ' Text
'/\\' Operator
'\n ' Text
'f' Name
' ' Text
'y' Name
' ' Text
'x' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'y' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'equals_ext' Name
' ' Text
'#' Operator
'a' Name
' ' Text
'(' Operator
'equals' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'f' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'a' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x1' Name
' ' Text
'x2' Name
' ' Text
'y' Name
'.' Operator
' ' Text
'x1' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'x2' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'f' Name
' ' Text
'x1' Name
' ' Text
'y' Name
' ' Text
'`equals`' Operator.Word
' ' Text
'f' Name
' ' Text
'x2' Name
' ' Text
'y' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'fp_heap_0' Name
'\n ' Text
'(' Operator
'#' Operator
'heap' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'hprop' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'interp' Name
':' Operator
'hprop' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'pre' Name
':' Operator
'hprop' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'h' Name
':' Operator
'heap' Name
'{' Operator
'interp' Name
' ' Text
'pre' Name
' ' Text
'h' Name
'}' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'depends_only_on_0' Name
'\n ' Text
'(' Operator
'#' Operator
'heap' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'hprop' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'interp' Name
':' Operator
'hprop' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'disjoint' Name
':' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'join' Name
':' Operator
' ' Text
'(' Operator
'h0' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'h1' Name
':' Operator
'heap' Name
'{' Operator
'disjoint' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
'}' Operator
' ' Text
'->' Operator
' ' Text
'heap' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'q' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'fp' Name
':' Operator
' ' Text
'hprop' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'(' Operator
'h0' Name
':' Operator
'fp_heap_0' Name
' ' Text
'interp' Name
' ' Text
'fp' Name
')' Operator
' ' Text
'(' Operator
'h1' Name
':' Operator
'heap' Name
'{' Operator
'disjoint' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
'}' Operator
')' Operator
'.' Operator
' ' Text
'q' Name
' ' Text
'h0' Name
' ' Text
'<==>' Operator
' ' Text
'q' Name
' ' Text
'(' Operator
'join' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'fp_prop_0' Name
'\n ' Text
'(' Operator
'#' Operator
'heap' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'hprop' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'interp' Name
':' Operator
'hprop' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'disjoint' Name
':' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'join' Name
':' Operator
' ' Text
'(' Operator
'h0' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'h1' Name
':' Operator
'heap' Name
'{' Operator
'disjoint' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
'}' Operator
' ' Text
'->' Operator
' ' Text
'heap' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'fp' Name
':' Operator
'hprop' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'p' Name
':' Operator
'(' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'{' Operator
'p' Name
' ' Text
'`' Keyword
'(' Operator
'depends_only_on_0' Name
' ' Text
'interp' Name
' ' Text
'disjoint' Name
' ' Text
'join' Name
')' Operator
'`' Keyword
' ' Text
'fp' Name
'}' Operator
'\n\n' Text
'noeq' Keyword
'\n' Text
'type' Keyword
' ' Text
'st0' Name
' ' Text
'=' Operator
' ' Text
'{' Operator
'\n ' Text
'mem' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'2' Literal.Number.Integer
';' Operator
'\n ' Text
'core' Name
':' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'mem' Name
';' Operator
'\n\n ' Text
'locks_preorder' Name
':' Operator
'P' Name.Namespace
'.' Punctuation
'preorder' Name
' ' Text
'mem' Name
';' Operator
'\n ' Text
'hprop' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'2' Literal.Number.Integer
';' Operator
'\n ' Text
'locks_invariant' Name
':' Operator
' ' Text
'mem' Name
' ' Text
'->' Operator
' ' Text
'hprop' Name
';' Operator
'\n\n ' Text
'disjoint' Name
':' Operator
' ' Text
'mem' Name
' ' Text
'->' Operator
' ' Text
'mem' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
';' Operator
'\n ' Text
'join' Name
':' Operator
' ' Text
'h0' Name
':' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'h1' Name
':' Operator
'mem' Name
'{' Operator
'disjoint' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
'}' Operator
' ' Text
'->' Operator
' ' Text
'mem' Name
';' Operator
'\n\n ' Text
'interp' Name
':' Operator
' ' Text
'hprop' Name
' ' Text
'->' Operator
' ' Text
'mem' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
';' Operator
'\n\n ' Text
'emp' Name
':' Operator
'hprop' Name
';' Operator
'\n ' Text
'star' Name
':' Operator
' ' Text
'hprop' Name
' ' Text
'->' Operator
' ' Text
'hprop' Name
' ' Text
'->' Operator
' ' Text
'hprop' Name
';' Operator
'\n\n ' Text
'equals' Name
':' Operator
' ' Text
'hprop' Name
' ' Text
'->' Operator
' ' Text
'hprop' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
';' Operator
'\n' Text
'}' Operator
'\n\n\n' Text
'/// disjointness is symmetric' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'disjoint_sym' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'h0' Name
' ' Text
'h1' Name
'.' Operator
' ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
' ' Text
'<==>' Operator
' ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'h1' Name
' ' Text
'h0' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'disjoint_join' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
'.' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'm0' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'join' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'm0' Name
' ' Text
'm2' Name
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'join' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'm2' Name
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'join' Name
' ' Text
'm0' Name
' ' Text
'm2' Name
')' Operator
' ' Text
'm1' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'join_commutative' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st0' Name
' ' Text
'{' Operator
' ' Text
'disjoint_sym' Name
' ' Text
'st' Name
' ' Text
'}' Operator
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'm0' Name
' ' Text
'm1' Name
'.' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'st' Name
'.' Operator
'join' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'=' Operator
'=' Operator
' ' Text
'st' Name
'.' Operator
'join' Name
' ' Text
'm1' Name
' ' Text
'm0' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'join_associative' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st0' Name
'{' Operator
'disjoint_join' Name
' ' Text
'st' Name
'}' Operator
')' Operator
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
'.' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'm0' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'join' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'st' Name
'.' Operator
'join' Name
' ' Text
'm0' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'join' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'st' Name
'.' Operator
'join' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'join' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'm2' Name
'\n\n' Text
'////////////////////////////////////////////////////////////////////////////////' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'interp_extensionality' Name
' ' Text
'#' Operator
'r' Name
' ' Text
'#' Operator
's' Name
' ' Text
'(' Operator
'equals' Name
':' Operator
'r' Name
' ' Text
'->' Operator
' ' Text
'r' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'f' Name
':' Operator
'r' Name
' ' Text
'->' Operator
' ' Text
's' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'h' Name
'.' Operator
' ' Text
'{' Operator
':' Operator
'pattern' Name
' ' Text
'equals' Name
' ' Text
'x' Name
' ' Text
'y' Name
';' Operator
' ' Text
'f' Name
' ' Text
'x' Name
' ' Text
'h' Name
'}' Operator
' ' Text
'equals' Name
' ' Text
'x' Name
' ' Text
'y' Name
' ' Text
'/\\' Operator
' ' Text
'f' Name
' ' Text
'x' Name
' ' Text
'h' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'f' Name
' ' Text
'y' Name
' ' Text
'h' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'affine' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'r0' Name
' ' Text
'r1' Name
' ' Text
's' Name
'.' Operator
' ' Text
'{' Operator
':' Operator
'pattern' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'r0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r1' Name
')' Operator
' ' Text
's' Name
')' Operator
' ' Text
'}' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'r0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r1' Name
')' Operator
' ' Text
's' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'r0' Name
' ' Text
's' Name
'\n\n' Text
'////////////////////////////////////////////////////////////////////////////////' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'depends_only_on' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
' ' Text
'(' Operator
'q' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'fp' Name
':' Operator
' ' Text
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'depends_only_on_0' Name
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'st' Name
'.' Operator
'join' Name
' ' Text
'q' Name
' ' Text
'fp' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'fp_prop' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
' ' Text
'(' Operator
'fp' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'fp_prop_0' Name
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'st' Name
'.' Operator
'join' Name
' ' Text
'fp' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'lemma_weaken_depends_only_on' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st0' Name
'{' Operator
'affine' Name
' ' Text
'st' Name
'}' Operator
')' Operator
'\n ' Text
'(' Operator
'fp0' Name
' ' Text
'fp1' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'q' Name
':' Operator
'fp_prop' Name
' ' Text
'fp0' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
' ' Text
'(' Operator
'q' Name
' ' Text
'`depends_only_on`' Operator.Word
' ' Text
'(' Operator
'fp0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'fp1' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'st_laws' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'(*' Comment
' standard laws about the equality relation ' Comment
'*)' Comment
'\n ' Text
'symmetry' Name
' ' Text
'st' Name
'.' Operator
'equals' Name
' ' Text
'/\\' Operator
'\n ' Text
'transitive' Name
' ' Text
'st' Name
'.' Operator
'equals' Name
' ' Text
'/\\' Operator
'\n ' Text
'interp_extensionality' Name
' ' Text
'st' Name
'.' Operator
'equals' Name
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'/\\' Operator
'\n ' Text
'(*' Comment
' standard laws for star forming a CM ' Comment
'*)' Comment
'\n ' Text
'associative' Name
' ' Text
'st' Name
'.' Operator
'equals' Name
' ' Text
'st' Name
'.' Operator
'star' Name
' ' Text
'/\\' Operator
'\n ' Text
'commutative' Name
' ' Text
'st' Name
'.' Operator
'equals' Name
' ' Text
'st' Name
'.' Operator
'star' Name
' ' Text
'/\\' Operator
'\n ' Text
'is_unit' Name
' ' Text
'st' Name
'.' Operator
'emp' Name
' ' Text
'st' Name
'.' Operator
'equals' Name
' ' Text
'st' Name
'.' Operator
'star' Name
' ' Text
'/\\' Operator
'\n ' Text
'equals_ext' Name
' ' Text
'st' Name
'.' Operator
'equals' Name
' ' Text
'st' Name
'.' Operator
'star' Name
' ' Text
'/\\' Operator
'\n ' Text
'(*' Comment
" We're working in an affine interpretation of SL " Comment
'*)' Comment
'\n ' Text
'affine' Name
' ' Text
'st' Name
' ' Text
'/\\' Operator
'\n ' Text
'(*' Comment
' laws about disjoint and join ' Comment
'*)' Comment
'\n ' Text
'disjoint_sym' Name
' ' Text
'st' Name
' ' Text
'/\\' Operator
'\n ' Text
'disjoint_join' Name
' ' Text
'st' Name
' ' Text
'/\\' Operator
'\n ' Text
'join_commutative' Name
' ' Text
'st' Name
' ' Text
'/\\' Operator
'\n ' Text
'join_associative' Name
' ' Text
'st' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'st' Name
' ' Text
'=' Operator
' ' Text
's' Name
':' Operator
'st0' Name
' ' Text
'{' Operator
' ' Text
'st_laws' Name
' ' Text
's' Name
' ' Text
'}' Operator
'\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' End state defn ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Begin expects, provides, requires, and ensures defns ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n\n' Text
'/// expects (the heap assertion expected by a computation) is simply an st.hprop' Comment
'\n' Text
'///' Comment
'\n' Text
'/// provides, or the post heap assertion, is a st.hprop on [a]-typed result' Comment
'\n\n' Text
'type' Keyword
' ' Text
'post_t' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
' ' Text
'=' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'hprop' Name
'\n\n\n' Text
'/// requires is a heap predicate that depends only on a pre heap assertion' Comment
'\n' Text
'/// (where the notion of `depends only on` is defined above as part of the state definition)' Comment
'\n' Text
'///' Comment
'\n' Text
'/// we call the type l_pre for logical precondition' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'l_pre' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'=' Operator
' ' Text
'fp_prop' Name
' ' Text
'pre' Name
'\n\n\n' Text
'/// ensures is a 2-state postcondition of type heap -> a -> heap -> prop' Comment
'\n' Text
'///' Comment
'\n' Text
'/// To define ensures, we need a notion of depends_only_on_2' Comment
'\n' Text
'///' Comment
'\n' Text
'/// Essentially, in the first heap argument, postconditions depend only on the expects hprop' Comment
'\n' Text
'/// and in the second heap argument, postconditions depend only on the provides hprop' Comment
'\n' Text
'///' Comment
'\n' Text
'/// Also note that the support for depends_only_on_2 is not required from the underlying memory model' Comment
'\n\n\n' Text
'let' Keyword.Declaration
' ' Text
'depends_only_on_0_2' Name
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'heap' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'hprop' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'interp' Name
':' Operator
'hprop' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'disjoint' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'join' Name
':' Operator
'(' Operator
'h0' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'h1' Name
':' Operator
'heap' Name
'{' Operator
'disjoint' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
'}' Operator
' ' Text
'->' Operator
' ' Text
'heap' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'q' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
' ' Text
'(' Operator
'fp_pre' Name
':' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'fp_post' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'hprop' Name
')' Operator
'\n\n ' Text
'=' Operator
' ' Text
'//can join any disjoint heap to the pre-heap and q is still valid' Comment
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'x' Name
' ' Text
'(' Operator
'h_pre' Name
':' Operator
'fp_heap_0' Name
' ' Text
'interp' Name
' ' Text
'fp_pre' Name
')' Operator
' ' Text
'h_post' Name
' ' Text
'(' Operator
'h' Name
':' Operator
'heap' Name
'{' Operator
'disjoint' Name
' ' Text
'h_pre' Name
' ' Text
'h' Name
'}' Operator
')' Operator
'.' Operator
'\n ' Text
'q' Name
' ' Text
'h_pre' Name
' ' Text
'x' Name
' ' Text
'h_post' Name
' ' Text
'<==>' Operator
' ' Text
'q' Name
' ' Text
'(' Operator
'join' Name
' ' Text
'h_pre' Name
' ' Text
'h' Name
')' Operator
' ' Text
'x' Name
' ' Text
'h_post' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'//can join any disjoint heap to the post-heap and q is still valid' Comment
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'x' Name
' ' Text
'h_pre' Name
' ' Text
'(' Operator
'h_post' Name
':' Operator
'fp_heap_0' Name
' ' Text
'interp' Name
' ' Text
'(' Operator
'fp_post' Name
' ' Text
'x' Name
')' Operator
')' Operator
' ' Text
'(' Operator
'h' Name
':' Operator
'heap' Name
'{' Operator
'disjoint' Name
' ' Text
'h_post' Name
' ' Text
'h' Name
'}' Operator
')' Operator
'.' Operator
'\n ' Text
'q' Name
' ' Text
'h_pre' Name
' ' Text
'x' Name
' ' Text
'h_post' Name
' ' Text
'<==>' Operator
' ' Text
'q' Name
' ' Text
'h_pre' Name
' ' Text
'x' Name
' ' Text
'(' Operator
'join' Name
' ' Text
'h_post' Name
' ' Text
'h' Name
')' Operator
')' Operator
'\n\n' Text
'/// Abbreviations for two-state depends' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'fp_prop_0_2' Name
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'heap' Name
' ' Text
'#' Operator
'hprop' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'interp' Name
':' Operator
'hprop' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'disjoint' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'join' Name
':' Operator
'(' Operator
'h0' Name
':' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'h1' Name
':' Operator
'heap' Name
'{' Operator
'disjoint' Name
' ' Text
'h0' Name
' ' Text
'h1' Name
'}' Operator
' ' Text
'->' Operator
' ' Text
'heap' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'fp_pre' Name
':' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'fp_post' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'hprop' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'q' Name
':' Operator
'(' Operator
'heap' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'heap' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'{' Operator
'depends_only_on_0_2' Name
' ' Text
'interp' Name
' ' Text
'disjoint' Name
' ' Text
'join' Name
' ' Text
'q' Name
' ' Text
'fp_pre' Name
' ' Text
'fp_post' Name
'}' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'depends_only_on2' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'q' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'fp_pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'fp_post' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'depends_only_on_0_2' Name
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'st' Name
'.' Operator
'disjoint' Name
' ' Text
'st' Name
'.' Operator
'join' Name
' ' Text
'q' Name
' ' Text
'fp_pre' Name
' ' Text
'fp_post' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'fp_prop2' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st0' Name
')' Operator
' ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
' ' Text
'(' Operator
'fp_pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'fp_post' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'q' Name
':' Operator
'(' Operator
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'{' Operator
'depends_only_on2' Name
' ' Text
'q' Name
' ' Text
'fp_pre' Name
' ' Text
'fp_post' Name
'}' Operator
'\n\n' Text
'/// Finally the type of 2-state postconditions' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'l_post' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
' ' Text
'(' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'=' Operator
' ' Text
'fp_prop2' Name
' ' Text
'pre' Name
' ' Text
'post' Name
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' End expects, provides, requires,\n and ensures defns ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n' Text
'effect' Keyword
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'req' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'Type0' Name.Class
')' Operator
' ' Text
'(' Operator
'ens' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'Type0' Name.Class
')' Operator
' ' Text
'=' Operator
'\n ' Text
'NMSTATE' Name.Class
' ' Text
'a' Name
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'st' Name
'.' Operator
'locks_preorder' Name
' ' Text
'req' Name
' ' Text
'ens' Name
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Begin interface of actions ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n' Text
'/// Actions are essentially state transformers that preserve frames' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'preserves_frame' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'pre' Name
' ' Text
'post' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'(' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'.' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
')' Operator
' ' Text
'm0' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'post' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
')' Operator
')' Operator
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
'frame' Name
')' Operator
'.' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'action_t' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'unit' Keyword.Type
' ' Text
'->' Operator
'\n ' Text
'Mst' Name.Class
' ' Text
'a' Name
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'->' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'/\\' Operator
'\n ' Text
'lpre' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'x' Name
' ' Text
'm1' Name
' ' Text
'->' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'lpost' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'x' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'preserves_frame' Name
' ' Text
'pre' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
'\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' End interface of actions ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Begin definition of the computation AST ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n\n' Text
'/// Gadgets for building lpre- and lpostconditions for various nodes' Comment
'\n\n\n' Text
'/// Return node is parametric in provides and ensures' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'return_lpre' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
' ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
' ' Text
'(' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_pre' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
' ' Text
'lpost' Name
' ' Text
'h' Name
' ' Text
'x' Name
' ' Text
'h' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'frame_lpre' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
' ' Text
'(' Operator
'#' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
'frame' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_pre' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
' ' Text
'lpre' Name
' ' Text
'h' Name
' ' Text
'/\\' Operator
' ' Text
'f_frame' Name
' ' Text
'h' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'frame_lpost' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
'frame' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_post' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
' ' Text
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h0' Name
' ' Text
'x' Name
' ' Text
'h1' Name
' ' Text
'->' Operator
' ' Text
'lpre' Name
' ' Text
'h0' Name
' ' Text
'/\\' Operator
' ' Text
'lpost' Name
' ' Text
'h0' Name
' ' Text
'x' Name
' ' Text
'h1' Name
' ' Text
'/\\' Operator
' ' Text
'f_frame' Name
' ' Text
'h1' Name
'\n\n' Text
'/// The bind rule bakes in weakening of requires / ensures' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'bind_lpre' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post_a' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpre_a' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'lpost_a' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post_a' Name
')' Operator
'\n ' Text
'(' Operator
'lpre_b' Name
':' Operator
'(' Operator
'x' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'l_pre' Name
' ' Text
'(' Operator
'post_a' Name
' ' Text
'x' Name
')' Operator
')' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_pre' Name
' ' Text
'pre' Name
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
' ' Text
'lpre_a' Name
' ' Text
'h' Name
' ' Text
'/\\' Operator
' ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
' ' Text
'h1' Name
'.' Operator
' ' Text
'lpost_a' Name
' ' Text
'h' Name
' ' Text
'x' Name
' ' Text
'h1' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'lpre_b' Name
' ' Text
'x' Name
' ' Text
'h1' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'bind_lpost' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post_a' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpre_a' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'lpost_a' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post_a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'b' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post_b' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'b' Name
')' Operator
'\n ' Text
'(' Operator
'lpost_b' Name
':' Operator
'(' Operator
'x' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'l_post' Name
' ' Text
'(' Operator
'post_a' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post_b' Name
')' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post_b' Name
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h0' Name
' ' Text
'y' Name
' ' Text
'h2' Name
' ' Text
'->' Operator
' ' Text
'lpre_a' Name
' ' Text
'h0' Name
' ' Text
'/\\' Operator
' ' Text
'(' Operator
'exists' Keyword
' ' Text
'x' Name
' ' Text
'h1' Name
'.' Operator
' ' Text
'lpost_a' Name
' ' Text
'h0' Name
' ' Text
'x' Name
' ' Text
'h1' Name
' ' Text
'/\\' Operator
' ' Text
'(' Operator
'lpost_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'h1' Name
' ' Text
'y' Name
' ' Text
'h2' Name
')' Operator
'\n\n' Text
'/// Parallel composition is pointwise' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'par_lpre' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preL' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'lpreL' Name
':' Operator
'l_pre' Name
' ' Text
'preL' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preR' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'lpreR' Name
':' Operator
'l_pre' Name
' ' Text
'preR' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_pre' Name
' ' Text
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preR' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
' ' Text
'lpreL' Name
' ' Text
'h' Name
' ' Text
'/\\' Operator
' ' Text
'lpreR' Name
' ' Text
'h' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'par_lpost' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'aL' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preL' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'postL' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aL' Name
')' Operator
'\n ' Text
'(' Operator
'lpreL' Name
':' Operator
'l_pre' Name
' ' Text
'preL' Name
')' Operator
'\n ' Text
'(' Operator
'lpostL' Name
':' Operator
'l_post' Name
' ' Text
'preL' Name
' ' Text
'postL' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'aR' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preR' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'postR' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aR' Name
')' Operator
'\n ' Text
'(' Operator
'lpreR' Name
':' Operator
'l_pre' Name
' ' Text
'preR' Name
')' Operator
'\n ' Text
'(' Operator
'lpostR' Name
':' Operator
'l_post' Name
' ' Text
'preR' Name
' ' Text
'postR' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_post' Name
' ' Text
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preR' Name
')' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postR' Name
' ' Text
'xR' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h0' Name
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'h1' Name
' ' Text
'->' Operator
' ' Text
'lpreL' Name
' ' Text
'h0' Name
' ' Text
'/\\' Operator
' ' Text
'lpreR' Name
' ' Text
'h0' Name
' ' Text
'/\\' Operator
' ' Text
'lpostL' Name
' ' Text
'h0' Name
' ' Text
'xL' Name
' ' Text
'h1' Name
' ' Text
'/\\' Operator
' ' Text
'lpostR' Name
' ' Text
'h0' Name
' ' Text
'xR' Name
' ' Text
'h1' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'weaker_pre' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'next_pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'(' Operator
'h' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
' ' Text
'(' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'.' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'next_pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'stronger_post' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
' ' Text
'(' Operator
'post' Name
' ' Text
'next_post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
' ' Text
'(' Operator
'h' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
' ' Text
'(' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'.' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'next_post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'weakening_ok' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'wpre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'wpost' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'wlpre' Name
':' Operator
'l_pre' Name
' ' Text
'wpre' Name
')' Operator
'\n ' Text
'(' Operator
'wlpost' Name
':' Operator
'l_post' Name
' ' Text
'wpre' Name
' ' Text
'wpost' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'weaker_pre' Name
' ' Text
'wpre' Name
' ' Text
'pre' Name
' ' Text
'/\\' Operator
'\n ' Text
'stronger_post' Name
' ' Text
'wpost' Name
' ' Text
'post' Name
' ' Text
'/\\' Operator
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'h' Name
'.' Operator
' ' Text
'wlpre' Name
' ' Text
'h' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'lpre' Name
' ' Text
'h' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'h0' Name
' ' Text
'x' Name
' ' Text
'h1' Name
'.' Operator
' ' Text
'lpost' Name
' ' Text
'h0' Name
' ' Text
'x' Name
' ' Text
'h1' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'wlpost' Name
' ' Text
'h0' Name
' ' Text
'x' Name
' ' Text
'h1' Name
')' Operator
'\n\n\n' Text
'/// Setting the flag just to reduce the time to typecheck the type m' Comment
'\n\n' Text
'#' Operator
'push' Name
'-' Operator
'options' Name
' ' Text
'"' Literal.String.Double
'--__temp_no_proj Steel.Semantics.Hoare.MST' Literal.String.Double
'"' Literal.String.Double
'\n' Text
'noeq' Keyword
'\n' Text
'type' Keyword
' ' Text
'm' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
':' Operator
'\n ' Text
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'l_pre' Name
' ' Text
'pre' Name
' ' Text
'->' Operator
'\n ' Text
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'->' Operator
' ' Text
'Type' Name.Class
'\n ' Text
'=' Operator
'\n ' Text
'|' Operator
' ' Text
'Ret' Name.Class
':' Operator
'\n ' Text
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'x' Name
':' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post' Name
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post' Name
' ' Text
'(' Operator
'return_lpre' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'lpost' Name
')' Operator
' ' Text
'lpost' Name
'\n\n ' Text
'|' Operator
' ' Text
'Bind' Name.Class
':' Operator
'\n ' Text
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'post_a' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpre_a' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpost_a' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post_a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'b' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'post_b' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'b' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpre_b' Name
':' Operator
'(' Operator
'x' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'l_pre' Name
' ' Text
'(' Operator
'post_a' Name
' ' Text
'x' Name
')' Operator
')' Operator
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpost_b' Name
':' Operator
'(' Operator
'x' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'l_post' Name
' ' Text
'(' Operator
'post_a' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post_b' Name
')' Operator
' ' Text
'->' Operator
'\n ' Text
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post_a' Name
' ' Text
'lpre_a' Name
' ' Text
'lpost_a' Name
' ' Text
'->' Operator
'\n ' Text
'g' Name
':' Operator
'(' Operator
'x' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'Dv' Name.Class
' ' Text
'(' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'b' Name
' ' Text
'(' Operator
'post_a' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post_b' Name
' ' Text
'(' Operator
'lpre_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'lpost_b' Name
' ' Text
'x' Name
')' Operator
')' Operator
')' Operator
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'b' Name
' ' Text
'pre' Name
' ' Text
'post_b' Name
'\n ' Text
'(' Operator
'bind_lpre' Name
' ' Text
'lpre_a' Name
' ' Text
'lpost_a' Name
' ' Text
'lpre_b' Name
')' Operator
'\n ' Text
'(' Operator
'bind_lpost' Name
' ' Text
'lpre_a' Name
' ' Text
'lpost_a' Name
' ' Text
'lpost_b' Name
')' Operator
'\n\n ' Text
'|' Operator
' ' Text
'Act' Name.Class
':' Operator
'\n ' Text
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'->' Operator
'\n ' Text
'f' Name
':' Operator
'action_t' Name
' ' Text
'#' Operator
'st' Name
' ' Text
'#' Operator
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'\n\n ' Text
'|' Operator
' ' Text
'Frame' Name.Class
':' Operator
'\n ' Text
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'->' Operator
'\n ' Text
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'->' Operator
'\n ' Text
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
'frame' Name
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
' ' Text
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
'\n ' Text
'(' Operator
'frame_lpre' Name
' ' Text
'lpre' Name
' ' Text
'f_frame' Name
')' Operator
'\n ' Text
'(' Operator
'frame_lpost' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'f_frame' Name
')' Operator
'\n\n ' Text
'|' Operator
' ' Text
'Par' Name.Class
':' Operator
'\n ' Text
'#' Operator
'aL' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'preL' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'postL' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aL' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpreL' Name
':' Operator
'l_pre' Name
' ' Text
'preL' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpostL' Name
':' Operator
'l_post' Name
' ' Text
'preL' Name
' ' Text
'postL' Name
' ' Text
'->' Operator
'\n ' Text
'mL' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'aL' Name
' ' Text
'preL' Name
' ' Text
'postL' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'aR' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'preR' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'postR' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aR' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpreR' Name
':' Operator
'l_pre' Name
' ' Text
'preR' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpostR' Name
':' Operator
'l_post' Name
' ' Text
'preR' Name
' ' Text
'postR' Name
' ' Text
'->' Operator
'\n ' Text
'mR' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'aR' Name
' ' Text
'preR' Name
' ' Text
'postR' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'(' Operator
'aL' Name
' ' Text
'&' Operator
' ' Text
'aR' Name
')' Operator
' ' Text
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preR' Name
')' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postR' Name
' ' Text
'xR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'lpreR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpost' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
')' Operator
'\n\n ' Text
'|' Operator
' ' Text
'Weaken' Name.Class
':' Operator
'\n ' Text
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'wpre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'wpost' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'wlpre' Name
':' Operator
'l_pre' Name
' ' Text
'wpre' Name
' ' Text
'->' Operator
'\n ' Text
'wlpost' Name
':' Operator
'l_post' Name
' ' Text
'wpre' Name
' ' Text
'wpost' Name
' ' Text
'->' Operator
'\n ' Text
'_' Name
':' Operator
'squash' Name
' ' Text
'(' Operator
'weakening_ok' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'wlpre' Name
' ' Text
'wlpost' Name
')' Operator
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'wpre' Name
' ' Text
'wpost' Name
' ' Text
'wlpre' Name
' ' Text
'wlpost' Name
'\n' Text
'#' Operator
'pop' Name
'-' Operator
'options' Name
'\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' End definition of the computation AST ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Stepping relation ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n' Text
'/// All steps preserve frames' Comment
'\n\n' Text
'noeq' Keyword
'\n' Text
'type' Keyword
' ' Text
'step_result' Name
' ' Text
'(' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'|' Operator
' ' Text
'Step' Name.Class
':' Operator
'\n ' Text
'next_pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'next_post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'next_pre' Name
' ' Text
'->' Operator
'\n ' Text
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'next_pre' Name
' ' Text
'next_post' Name
' ' Text
'->' Operator
'\n ' Text
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'next_pre' Name
' ' Text
'next_post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'->' Operator
'\n ' Text
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Type of the single-step interpreter ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n\n' Text
'/// Interpreter is setup as a Div function from computation trees to computation trees' Comment
'\n' Text
'///' Comment
'\n' Text
'/// While the requires for the Div is standard (that the expects hprop holds and requires is valid),' Comment
'\n' Text
'/// the ensures is interesting' Comment
'\n' Text
'///' Comment
'\n' Text
'/// As the computation evolves, the requires and ensures associated with the computation graph nodes' Comment
'\n' Text
'/// also evolve' Comment
'\n' Text
'/// But they evolve systematically: preconditions become weaker and postconditions become stronger' Comment
'\n' Text
'///' Comment
'\n' Text
'/// Consider { req } c | st { ens } ~~> { req1 } c1 | st1 { ens1 }' Comment
'\n' Text
'///' Comment
'\n' Text
'/// Then, req st ==> req1 st1 /\\' Comment
'\n' Text
'/// (forall x st_final. ens1 st1 x st_final ==> ens st x st_final)' Comment
'\n\n\n' Text
'unfold' Keyword
'\n' Text
'let' Keyword.Declaration
' ' Text
'step_req' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'Type0' Name.Class
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'->' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'/\\' Operator
'\n ' Text
'lpre' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'weaker_lpre' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'next_pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'next_lpre' Name
':' Operator
'l_pre' Name
' ' Text
'next_pre' Name
')' Operator
'\n ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'lpre' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
'>' Operator
' ' Text
'next_lpre' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'stronger_lpost' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'next_pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'#' Operator
'next_post' Name
'\n ' Text
'(' Operator
'next_lpost' Name
':' Operator
'l_post' Name
' ' Text
'next_pre' Name
' ' Text
'next_post' Name
')' Operator
'\n ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'forall' Keyword
' ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
' ' Text
'(' Operator
'h_final' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'.' Operator
'\n ' Text
'next_lpost' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'x' Name
' ' Text
'h_final' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'lpost' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'x' Name
' ' Text
'h_final' Name
'\n\n' Text
'unfold' Keyword
'\n' Text
'let' Keyword.Declaration
' ' Text
'step_ens' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'Type0' Name.Class
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'r' Name
' ' Text
'm1' Name
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'Step' Name.Class
' ' Text
'next_pre' Name
' ' Text
'next_post' Name
' ' Text
'next_lpre' Name
' ' Text
'next_lpost' Name
' ' Text
'_' Name
' ' Text
'=' Operator
' ' Text
'r' Name
' ' Text
'in' Keyword
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'next_pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'stronger_post' Name
' ' Text
'post' Name
' ' Text
'next_post' Name
' ' Text
'/\\' Operator
'\n ' Text
'next_lpre' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'preserves_frame' Name
' ' Text
'pre' Name
' ' Text
'next_pre' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'weaker_lpre' Name
' ' Text
'lpre' Name
' ' Text
'next_lpre' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'stronger_lpost' Name
' ' Text
'lpost' Name
' ' Text
'next_lpost' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
'\n\n\n' Text
'/// The type of the stepping function' Comment
'\n\n' Text
'type' Keyword
' ' Text
'step_t' Name
' ' Text
'=' Operator
'\n ' Text
'#' Operator
'st' Name
':' Operator
'st' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
' ' Text
'->' Operator
'\n ' Text
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'->' Operator
'\n ' Text
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'->' Operator
'\n ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Auxiliary lemmas ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n' Text
'/// Some AC lemmas on `st.star`' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'apply_assoc' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'p' Name
' ' Text
'q' Name
' ' Text
'r' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
' ' Text
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
')' Operator
' ' Text
'(' Operator
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'equals_ext_left' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'p' Name
' ' Text
'q' Name
' ' Text
'r' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'p' Name
' ' Text
'`st.equals`' Operator.Word
' ' Text
'q' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'`st.equals`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'equals_ext_right' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'p' Name
' ' Text
'q' Name
' ' Text
'r' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'q' Name
' ' Text
'`st.equals`' Operator.Word
' ' Text
'r' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
')' Operator
' ' Text
'`st.equals`' Operator.Word
' ' Text
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'p' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'p' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
';' Operator
'\n ' Text
'}' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'commute_star_right' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'p' Name
' ' Text
'q' Name
' ' Text
'r' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
')' Operator
' ' Text
'`st.equals`' Operator.Word
'\n ' Text
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'equals_ext_right' Name
' ' Text
'p' Name
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
')' Operator
' ' Text
'}' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
')' Operator
';' Operator
'\n ' Text
'}' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'assoc_star_right' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'p' Name
' ' Text
'q' Name
' ' Text
'r' Name
' ' Text
's' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
')' Operator
' ' Text
'`st.equals`' Operator.Word
'\n ' Text
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
')' Operator
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'equals_ext_right' Name
' ' Text
'p' Name
' ' Text
'(' Operator
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
'\n ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
')' Operator
' ' Text
'}' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
')' Operator
';' Operator
'\n ' Text
'}' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'commute_assoc_star_right' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'p' Name
' ' Text
'q' Name
' ' Text
'r' Name
' ' Text
's' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
')' Operator
' ' Text
'`st.equals`' Operator.Word
'\n ' Text
'(' Operator
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
')' Operator
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'equals_ext_right' Name
' ' Text
'p' Name
'\n ' Text
'(' Operator
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'r' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
'\n ' Text
'(' Operator
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
' ' Text
'}' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'q' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'assoc_star_right' Name
' ' Text
'p' Name
' ' Text
'r' Name
' ' Text
'q' Name
' ' Text
's' Name
' ' Text
'}' Operator
'\n ' Text
'p' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'r' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'q' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
's' Name
')' Operator
')' Operator
';' Operator
'\n ' Text
'}' Operator
'\n\n\n' Text
'/// Apply extensionality manually, control proofs' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'apply_interp_ext' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'p' Name
' ' Text
'q' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'm' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'p' Name
' ' Text
'm' Name
' ' Text
'/\\' Operator
' ' Text
'p' Name
' ' Text
'`st.equals`' Operator.Word
' ' Text
'q' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'q' Name
' ' Text
'm' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'weaken_fp_prop' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'frame' Name
' ' Text
"frame'" Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
'\n ' Text
'forall' Keyword
' ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
'.' Operator
'\n ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'forall' Keyword
' ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
"frame'" Name
')' Operator
'.' Operator
'\n ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'depends_only_on_commutes_with_weaker' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'q' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'fp' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'fp_next' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'depends_only_on' Name
' ' Text
'q' Name
' ' Text
'fp' Name
' ' Text
'/\\' Operator
' ' Text
'weaker_pre' Name
' ' Text
'fp_next' Name
' ' Text
'fp' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'depends_only_on' Name
' ' Text
'q' Name
' ' Text
'fp_next' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'h0' Name
':' Operator
'fp_heap_0' Name
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'fp_next' Name
')' Operator
'.' Operator
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'fp_next' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'emp' Name
')' Operator
' ' Text
'h0' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'depends_only_on2_commutes_with_weaker' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'q' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'->' Operator
' ' Text
'prop' Name
')' Operator
'\n ' Text
'(' Operator
'fp' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'fp_next' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'fp_post' Name
':' Operator
'a' Name
' ' Text
'->' Operator
' ' Text
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'depends_only_on2' Name
' ' Text
'q' Name
' ' Text
'fp' Name
' ' Text
'fp_post' Name
' ' Text
'/\\' Operator
' ' Text
'weaker_pre' Name
' ' Text
'fp_next' Name
' ' Text
'fp' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'depends_only_on2' Name
' ' Text
'q' Name
' ' Text
'fp_next' Name
' ' Text
'fp_post' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'h0' Name
':' Operator
'fp_heap_0' Name
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'fp_next' Name
')' Operator
'.' Operator
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'fp_next' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'emp' Name
')' Operator
' ' Text
'h0' Name
')' Operator
'\n\n' Text
'/// Lemmas about preserves_frame' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'preserves_frame_trans' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'hp1' Name
' ' Text
'hp2' Name
' ' Text
'hp3' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'm1' Name
' ' Text
'm2' Name
' ' Text
'm3' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'hp1' Name
' ' Text
'hp2' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
' ' Text
'/\\' Operator
' ' Text
'preserves_frame' Name
' ' Text
'hp2' Name
' ' Text
'hp3' Name
' ' Text
'm2' Name
' ' Text
'm3' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'hp1' Name
' ' Text
'hp3' Name
' ' Text
'm1' Name
' ' Text
'm3' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'#' Operator
'push' Name
'-' Operator
'options' Name
' ' Text
'"' Literal.String.Double
'--warn_error -271' Literal.String.Double
'"' Literal.String.Double
'\n' Text
'let' Keyword.Declaration
' ' Text
'preserves_frame_stronger_post' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'post' Name
' ' Text
'post_s' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'm1' Name
' ' Text
'm2' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'pre' Name
' ' Text
'(' Operator
'post_s' Name
' ' Text
'x' Name
')' Operator
' ' Text
'm1' Name
' ' Text
'm2' Name
' ' Text
'/\\' Operator
' ' Text
'stronger_post' Name
' ' Text
'post' Name
' ' Text
'post_s' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'pre' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'm1' Name
' ' Text
'm2' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'aux' Name
' ' Text
'(' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'm1' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'm2' Name
' ' Text
'/\\' Operator
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
'frame' Name
')' Operator
'.' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm2' Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'[' Operator
'SMTPat' Name.Class
' ' Text
'()' Name.Builtin.Pseudo
']' Operator
'\n ' Text
'=' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'post_s' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'm2' Name
')' Operator
';' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'post_s' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'post_s' Name
' ' Text
'x' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'(' Operator
'post_s' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'post_s' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
';' Operator
'\n ' Text
'}' Operator
';' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'post_s' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'm2' Name
')' Operator
';' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'm2' Name
')' Operator
';' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'apply_assoc' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
')' Operator
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'frame' Name
' ' Text
'}' Operator
'\n ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
';' Operator
'\n ' Text
'}' Operator
';' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm2' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'm2' Name
')' Operator
'\n ' Text
'in' Keyword
'\n ' Text
'()' Name.Builtin.Pseudo
'\n' Text
'#' Operator
'pop' Name
'-' Operator
'options' Name
'\n\n' Text
'#' Operator
'push' Name
'-' Operator
'options' Name
' ' Text
'"' Literal.String.Double
'--z3rlimit 40 --warn_error -271' Literal.String.Double
'"' Literal.String.Double
'\n' Text
'let' Keyword.Declaration
' ' Text
'preserves_frame_star' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'pre' Name
' ' Text
'post' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
' ' Text
'(' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'(' Operator
'post' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'aux' Name
' ' Text
'(' Operator
"frame'" Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
' ' Text
'm0' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
' ' Text
'`st.star`' Operator.Word
'\n ' Text
'(' Operator
'(' Operator
'post' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
"frame'" Name
')' Operator
'.' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'[' Operator
'SMTPat' Name.Class
' ' Text
'()' Name.Builtin.Pseudo
']' Operator
'\n ' Text
'=' Operator
'\n ' Text
'assoc_star_right' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'pre' Name
' ' Text
'frame' Name
' ' Text
"frame'" Name
';' Operator
'\n ' Text
'apply_interp_ext' Name
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'm0' Name
';' Operator
'\n ' Text
'assoc_star_right' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'post' Name
' ' Text
'frame' Name
' ' Text
"frame'" Name
';' Operator
'\n ' Text
'apply_interp_ext' Name
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'post' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'post' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
'\n ' Text
'm1' Name
';' Operator
'\n ' Text
'weaken_fp_prop' Name
' ' Text
'frame' Name
' ' Text
"frame'" Name
' ' Text
'm0' Name
' ' Text
'm1' Name
'\n ' Text
'in' Keyword
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'preserves_frame_star_left' Name
' ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
' ' Text
'(' Operator
'pre' Name
' ' Text
'post' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
' ' Text
'(' Operator
'frame' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'preserves_frame' Name
' ' Text
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pre' Name
')' Operator
' ' Text
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'post' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'aux' Name
' ' Text
'(' Operator
"frame'" Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pre' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
' ' Text
'm0' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
' ' Text
'`st.star`' Operator.Word
'\n ' Text
'(' Operator
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'post' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'f_frame' Name
':' Operator
'fp_prop' Name
' ' Text
"frame'" Name
')' Operator
'.' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'f_frame' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'[' Operator
'SMTPat' Name.Class
' ' Text
'()' Name.Builtin.Pseudo
']' Operator
'\n ' Text
'=' Operator
'\n ' Text
'commute_assoc_star_right' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'frame' Name
' ' Text
'pre' Name
' ' Text
"frame'" Name
';' Operator
'\n ' Text
'apply_interp_ext' Name
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pre' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'm0' Name
';' Operator
'\n ' Text
'commute_assoc_star_right' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'frame' Name
' ' Text
'post' Name
' ' Text
"frame'" Name
';' Operator
'\n ' Text
'apply_interp_ext' Name
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'post' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
')' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'(' Operator
'frame' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'post' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
"frame'" Name
')' Operator
')' Operator
'\n ' Text
'm1' Name
';' Operator
'\n ' Text
'weaken_fp_prop' Name
' ' Text
'frame' Name
' ' Text
"frame'" Name
' ' Text
'm0' Name
' ' Text
'm1' Name
'\n ' Text
'in' Keyword
'\n ' Text
'()' Name.Builtin.Pseudo
'\n' Text
'#' Operator
'pop' Name
'-' Operator
'options' Name
'\n\n\n' Text
'/// Lemma frame_post_for_par is used in the par proof' Comment
'\n' Text
'///' Comment
'\n' Text
'/// E.g. in the par rule, when L takes a step, we can frame the requires of R' Comment
'\n' Text
'/// by using the preserves_frame property of the stepping relation' Comment
'\n' Text
'///' Comment
'\n' Text
'/// However we also need to frame the ensures of R, for establishing stronger_post' Comment
'\n' Text
'///' Comment
'\n' Text
'/// Basically, we need:' Comment
'\n' Text
'///' Comment
'\n' Text
'/// forall x h_final. postR prev_state x h_final <==> postR next_state x h_final' Comment
'\n' Text
'///' Comment
'\n' Text
'/// (the proof only requires the reverse implication, but we can prove iff)' Comment
'\n' Text
'///' Comment
'\n' Text
'/// To prove this, we rely on the framing of all frame fp props provides by the stepping relation' Comment
'\n' Text
'///' Comment
'\n' Text
'/// To use it, we instantiate the fp prop with inst_heap_prop_for_par' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'inst_heap_prop_for_par' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'state' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'fp_prop' Name
' ' Text
'pre' Name
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
'\n ' Text
'forall' Keyword
' ' Text
'x' Name
' ' Text
'final_state' Name
'.' Operator
'\n ' Text
'lpost' Name
' ' Text
'h' Name
' ' Text
'x' Name
' ' Text
'final_state' Name
' ' Text
'<==>' Operator
'\n ' Text
'lpost' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'state' Name
')' Operator
' ' Text
'x' Name
' ' Text
'final_state' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'frame_post_for_par_tautology' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre_f' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post_f' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpost_f' Name
':' Operator
'l_post' Name
' ' Text
'pre_f' Name
' ' Text
'post_f' Name
')' Operator
'\n ' Text
'(' Operator
'm0' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
' ' Text
'(' Operator
'inst_heap_prop_for_par' Name
' ' Text
'lpost_f' Name
' ' Text
'm0' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'frame_post_for_par_aux' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'pre_s' Name
' ' Text
'post_s' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
' ' Text
'(' Operator
'#' Operator
'pre_f' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
' ' Text
'(' Operator
'#' Operator
'post_f' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'lpost_f' Name
':' Operator
'l_post' Name
' ' Text
'pre_f' Name
' ' Text
'post_f' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
'\n ' Text
'preserves_frame' Name
' ' Text
'pre_s' Name
' ' Text
'post_s' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'pre_s' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pre_f' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'm0' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'inst_heap_prop_for_par' Name
' ' Text
'lpost_f' Name
' ' Text
'm0' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'<==>' Operator
'\n ' Text
'inst_heap_prop_for_par' Name
' ' Text
'lpost_f' Name
' ' Text
'm0' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'()' Name.Builtin.Pseudo
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'frame_post_for_par' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'pre_s' Name
' ' Text
'post_s' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'm0' Name
' ' Text
'm1' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre_f' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post_f' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpre_f' Name
':' Operator
'l_pre' Name
' ' Text
'pre_f' Name
')' Operator
'\n ' Text
'(' Operator
'lpost_f' Name
':' Operator
'l_post' Name
' ' Text
'pre_f' Name
' ' Text
'post_f' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
'\n ' Text
'preserves_frame' Name
' ' Text
'pre_s' Name
' ' Text
'post_s' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'pre_s' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pre_f' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'm0' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'(' Operator
'lpre_f' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'<==>' Operator
' ' Text
'lpre_f' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'(' Operator
'forall' Keyword
' ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
' ' Text
'(' Operator
'final_state' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'.' Operator
'\n ' Text
'lpost_f' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'x' Name
' ' Text
'final_state' Name
' ' Text
'<==>' Operator
'\n ' Text
'lpost_f' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'x' Name
' ' Text
'final_state' Name
')' Operator
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'frame_post_for_par_tautology' Name
' ' Text
'lpost_f' Name
' ' Text
'm0' Name
';' Operator
'\n ' Text
'frame_post_for_par_aux' Name
' ' Text
'pre_s' Name
' ' Text
'post_s' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'lpost_f' Name
'\n\n' Text
'/// Finally lemmas for proving that in the par rules preconditions get weaker' Comment
'\n' Text
'/// and postconditions get stronger' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'par_weaker_lpre_and_stronger_lpost_l' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preL' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'lpreL' Name
':' Operator
'l_pre' Name
' ' Text
'preL' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'aL' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'postL' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aL' Name
')' Operator
'\n ' Text
'(' Operator
'lpostL' Name
':' Operator
'l_post' Name
' ' Text
'preL' Name
' ' Text
'postL' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'next_preL' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'next_postL' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aL' Name
')' Operator
'\n ' Text
'(' Operator
'next_lpreL' Name
':' Operator
'l_pre' Name
' ' Text
'next_preL' Name
')' Operator
'\n ' Text
'(' Operator
'next_lpostL' Name
':' Operator
'l_post' Name
' ' Text
'next_preL' Name
' ' Text
'next_postL' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preR' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'lpreR' Name
':' Operator
'l_pre' Name
' ' Text
'preR' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'aR' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'postR' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aR' Name
')' Operator
'\n ' Text
'(' Operator
'lpostR' Name
':' Operator
'l_post' Name
' ' Text
'preR' Name
' ' Text
'postR' Name
')' Operator
'\n ' Text
'(' Operator
'state' Name
' ' Text
'next_state' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
'\n ' Text
'weaker_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'next_lpreL' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'stronger_lpost' Name
' ' Text
'lpostL' Name
' ' Text
'next_lpostL' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'preserves_frame' Name
' ' Text
'preL' Name
' ' Text
'next_preL' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'lpreL' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'state' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'lpreR' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'state' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'state' Name
')' Operator
' ' Text
'state' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'weaker_lpre' Name
'\n ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'lpreR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpre' Name
' ' Text
'next_lpreL' Name
' ' Text
'lpreR' Name
')' Operator
'\n ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'stronger_lpost' Name
'\n ' Text
'(' Operator
'par_lpost' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpost' Name
' ' Text
'next_lpreL' Name
' ' Text
'next_lpostL' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
')' Operator
'\n ' Text
'state' Name
' ' Text
'next_state' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'frame_post_for_par' Name
' ' Text
'preL' Name
' ' Text
'next_preL' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
';' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'weaker_lpre' Name
' ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'lpreR' Name
')' Operator
' ' Text
'(' Operator
'par_lpre' Name
' ' Text
'next_lpreL' Name
' ' Text
'lpreR' Name
')' Operator
' ' Text
'state' Name
' ' Text
'next_state' Name
')' Operator
' ' Text
'by' Keyword
'\n ' Text
'(' Operator
'norm' Name
' ' Text
'[' Operator
'delta_only' Name
' ' Text
'[' Operator
'`' Keyword
'%' Operator
'weaker_lpre' Name
';' Operator
' ' Text
'`' Keyword
'%' Operator
'par_lpre' Name
']' Operator
' ' Text
']' Operator
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'par_weaker_lpre_and_stronger_lpost_r' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preL' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'lpreL' Name
':' Operator
'l_pre' Name
' ' Text
'preL' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'aL' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'postL' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aL' Name
')' Operator
'\n ' Text
'(' Operator
'lpostL' Name
':' Operator
'l_post' Name
' ' Text
'preL' Name
' ' Text
'postL' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'preR' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'lpreR' Name
':' Operator
'l_pre' Name
' ' Text
'preR' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'aR' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'postR' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aR' Name
')' Operator
'\n ' Text
'(' Operator
'lpostR' Name
':' Operator
'l_post' Name
' ' Text
'preR' Name
' ' Text
'postR' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'next_preR' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'next_postR' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aR' Name
')' Operator
'\n ' Text
'(' Operator
'next_lpreR' Name
':' Operator
'l_pre' Name
' ' Text
'next_preR' Name
')' Operator
'\n ' Text
'(' Operator
'next_lpostR' Name
':' Operator
'l_post' Name
' ' Text
'next_preR' Name
' ' Text
'next_postR' Name
')' Operator
'\n ' Text
'(' Operator
'state' Name
' ' Text
'next_state' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
'\n ' Text
'weaker_lpre' Name
' ' Text
'lpreR' Name
' ' Text
'next_lpreR' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'stronger_lpost' Name
' ' Text
'lpostR' Name
' ' Text
'next_lpostR' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'preserves_frame' Name
' ' Text
'preR' Name
' ' Text
'next_preR' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'lpreR' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'state' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'lpreL' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'state' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'state' Name
')' Operator
' ' Text
'state' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'next_preR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'next_state' Name
')' Operator
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'weaker_lpre' Name
'\n ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'lpreR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'next_lpreR' Name
')' Operator
'\n ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'/\\' Operator
'\n ' Text
'stronger_lpost' Name
'\n ' Text
'(' Operator
'par_lpost' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpost' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'next_lpreR' Name
' ' Text
'next_lpostR' Name
')' Operator
'\n ' Text
'state' Name
' ' Text
'next_state' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'commute_star_right' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'state' Name
')' Operator
' ' Text
'preL' Name
' ' Text
'preR' Name
';' Operator
'\n ' Text
'apply_interp_ext' Name
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'state' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preR' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'state' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'preR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preL' Name
')' Operator
')' Operator
'\n ' Text
'state' Name
';' Operator
'\n ' Text
'frame_post_for_par' Name
' ' Text
'preR' Name
' ' Text
'next_preR' Name
' ' Text
'state' Name
' ' Text
'next_state' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
';' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'weaker_lpre' Name
' ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'lpreR' Name
')' Operator
' ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'next_lpreR' Name
')' Operator
' ' Text
'state' Name
' ' Text
'next_state' Name
')' Operator
' ' Text
'by' Keyword
'\n ' Text
'(' Operator
'norm' Name
' ' Text
'[' Operator
'delta_only' Name
' ' Text
'[' Operator
'`' Keyword
'%' Operator
'weaker_lpre' Name
';' Operator
' ' Text
'`' Keyword
'%' Operator
'par_lpre' Name
']' Operator
' ' Text
']' Operator
')' Operator
';' Operator
'\n ' Text
'commute_star_right' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'next_state' Name
')' Operator
' ' Text
'next_preR' Name
' ' Text
'preL' Name
';' Operator
'\n ' Text
'apply_interp_ext' Name
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'next_state' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'next_preR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preL' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'next_state' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'next_preR' Name
')' Operator
')' Operator
'\n ' Text
'next_state' Name
'\n\n' Text
'#' Operator
'push' Name
'-' Operator
'options' Name
' ' Text
'"' Literal.String.Double
'--warn_error -271' Literal.String.Double
'"' Literal.String.Double
'\n' Text
'let' Keyword.Declaration
' ' Text
'stronger_post_par_r' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'aL' Name
' ' Text
'#' Operator
'aR' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'postL' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aL' Name
')' Operator
'\n ' Text
'(' Operator
'postR' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aR' Name
')' Operator
'\n ' Text
'(' Operator
'next_postR' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'aR' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'stronger_post' Name
' ' Text
'postR' Name
' ' Text
'next_postR' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
'\n ' Text
'forall' Keyword
' ' Text
'xL' Name
' ' Text
'xR' Name
' ' Text
'frame' Name
' ' Text
'h' Name
'.' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'next_postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
' ' Text
'=' Operator
'=' Operator
'>' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'aux' Name
' ' Text
'xL' Name
' ' Text
'xR' Name
' ' Text
'frame' Name
' ' Text
'h' Name
'\n ' Text
':' Operator
' ' Text
'Lemma' Name.Class
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'next_postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'h' Name
')' Operator
'\n ' Text
'[' Operator
'SMTPat' Name.Class
' ' Text
'()' Name.Builtin.Pseudo
']' Operator
'\n ' Text
'=' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'next_postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'(' Operator
'next_postR' Name
' ' Text
'xR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postL' Name
' ' Text
'xL' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'next_postR' Name
' ' Text
'xR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
';' Operator
'\n ' Text
'}' Operator
';' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'next_postR' Name
' ' Text
'xR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'h' Name
')' Operator
';' Operator
'\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'postR' Name
' ' Text
'xR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
')' Operator
' ' Text
'h' Name
')' Operator
';' Operator
'\n ' Text
'calc' Name.Exception
' ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
'\n ' Text
'postR' Name
' ' Text
'xR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'(' Operator
'postR' Name
' ' Text
'xR' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postL' Name
' ' Text
'xL' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'(' Operator
'st' Name
'.' Operator
'equals' Name
')' Operator
' ' Text
'{' Operator
' ' Text
'}' Operator
'\n ' Text
'(' Operator
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
';' Operator
'\n ' Text
'}' Operator
'\n ' Text
'in' Keyword
'\n ' Text
'()' Name.Builtin.Pseudo
'\n' Text
'#' Operator
'pop' Name
'-' Operator
'options' Name
'\n\n\n' Text
'(*' Comment
'*' Comment
'*' Comment
'*' Comment
' Begin stepping functions ' Comment
'*' Comment
'*' Comment
'*' Comment
'*)' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_ret' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Ret' Name.Class
'?' Operator
' ' Text
'f' Name
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'NMSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'_' Name
',' Operator
' ' Text
'n' Name
')' Operator
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'Ret' Name.Class
' ' Text
'p' Name
' ' Text
'x' Name
' ' Text
'lp' Name
' ' Text
'=' Operator
' ' Text
'f' Name
' ' Text
'in' Keyword
'\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'p' Name
' ' Text
'x' Name
')' Operator
' ' Text
'p' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'f' Name
',' Operator
' ' Text
'n' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'lpost_ret_act' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'x' Name
':' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'state' Name
':' Operator
'st' Name
'.' Operator
'mem' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'l_post' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post' Name
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'_' Name
' ' Text
'x' Name
' ' Text
'h1' Name
' ' Text
'->' Operator
' ' Text
'lpost' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'state' Name
')' Operator
' ' Text
'x' Name
' ' Text
'h1' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_act' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Act' Name.Class
'?' Operator
' ' Text
'f' Name
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'm0' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'Act' Name.Class
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'f' Name
' ' Text
'=' Operator
' ' Text
'f' Name
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'x' Name
' ' Text
'=' Operator
' ' Text
'f' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'lpost' Name
' ' Text
':' Operator
' ' Text
'l_post' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post' Name
' ' Text
'=' Operator
' ' Text
'lpost_ret_act' Name
' ' Text
'lpost' Name
' ' Text
'x' Name
' ' Text
'm0' Name
' ' Text
'in' Keyword
'\n\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
' ' Text
'lpost' Name
' ' Text
'h' Name
' ' Text
'x' Name
' ' Text
'h' Name
')' Operator
' ' Text
'lpost' Name
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'post' Name
' ' Text
'x' Name
' ' Text
'lpost' Name
')' Operator
'\n\n' Text
'module' Keyword
' ' Text
'M' Name.Class
' ' Text
'=' Operator
' ' Text
'MST' Name.Class
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_bind_ret_aux' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Bind' Name.Class
'?' Operator
' ' Text
'f' Name
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Bind' Name.Class
'?.' Operator
'f' Name
' ' Text
'f' Name
')' Operator
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'M' Name.Namespace
'.' Punctuation
'MSTATE' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'st' Name
'.' Operator
'locks_preorder' Name
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'M' Name.Namespace
'.' Punctuation
'MSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'->' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Bind' Name.Class
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'post_b' Name
' ' Text
'#' Operator
'lpre_b' Name
' ' Text
'#' Operator
'lpost_b' Name
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'p' Name
' ' Text
'x' Name
' ' Text
'_' Name
')' Operator
' ' Text
'g' Name
' ' Text
'->' Operator
'\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'p' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post_b' Name
' ' Text
'(' Operator
'lpre_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'lpost_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'g' Name
' ' Text
'x' Name
')' Operator
',' Operator
' ' Text
'm0' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_bind_ret' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Bind' Name.Class
'?' Operator
' ' Text
'f' Name
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Bind' Name.Class
'?.' Operator
'f' Name
' ' Text
'f' Name
')' Operator
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'NMSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'_' Name
',' Operator
' ' Text
'n' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'step_bind_ret_aux' Name
' ' Text
'f' Name
',' Operator
' ' Text
'n' Name
')' Operator
'\n\n\n' Text
'#' Operator
'push' Name
'-' Operator
'options' Name
' ' Text
'"' Literal.String.Double
'--z3rlimit 40' Literal.String.Double
'"' Literal.String.Double
'\n' Text
'let' Keyword.Declaration
' ' Text
'step_bind' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Bind' Name.Class
'?' Operator
' ' Text
'f' Name
'}' Operator
')' Operator
'\n ' Text
'(' Operator
'step' Name
':' Operator
'step_t' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Bind' Name.Class
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'_' Name
')' Operator
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'step_bind_ret' Name
' ' Text
'f' Name
'\n\n ' Text
'|' Operator
' ' Text
'Bind' Name.Class
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'b' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'post_a' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'post_b' Name
' ' Text
'#' Operator
'lpre_b' Name
' ' Text
'#' Operator
'lpost_b' Name
' ' Text
'f' Name
' ' Text
'g' Name
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'Step' Name.Class
' ' Text
'next_pre' Name
' ' Text
'next_post' Name
' ' Text
'next_lpre' Name
' ' Text
'next_lpost' Name
' ' Text
'f' Name
' ' Text
'=' Operator
' ' Text
'step' Name
' ' Text
'f' Name
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'lpre_b' Name
' ' Text
':' Operator
' ' Text
'(' Operator
'x' Name
':' Operator
'b' Name
' ' Text
'->' Operator
' ' Text
'l_pre' Name
' ' Text
'(' Operator
'next_post' Name
' ' Text
'x' Name
')' Operator
')' Operator
' ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
'\n ' Text
'depends_only_on_commutes_with_weaker' Name
' ' Text
'(' Operator
'lpre_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'post_a' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'next_post' Name
' ' Text
'x' Name
')' Operator
';' Operator
'\n ' Text
'lpre_b' Name
' ' Text
'x' Name
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'lpost_b' Name
' ' Text
':' Operator
' ' Text
'(' Operator
'x' Name
':' Operator
'b' Name
' ' Text
'->' Operator
' ' Text
'l_post' Name
' ' Text
'(' Operator
'next_post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post_b' Name
')' Operator
' ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
'\n ' Text
'depends_only_on2_commutes_with_weaker' Name
' ' Text
'(' Operator
'lpost_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'post_a' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'next_post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post_b' Name
';' Operator
'\n ' Text
'lpost_b' Name
' ' Text
'x' Name
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'g' Name
' ' Text
':' Operator
' ' Text
'(' Operator
'x' Name
':' Operator
'b' Name
' ' Text
'->' Operator
' ' Text
'Dv' Name.Class
' ' Text
'(' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'_' Name
' ' Text
'(' Operator
'next_post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'post_b' Name
' ' Text
'(' Operator
'lpre_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'lpost_b' Name
' ' Text
'x' Name
')' Operator
')' Operator
')' Operator
' ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
'\n ' Text
'Weaken' Name.Class
' ' Text
'(' Operator
'lpre_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'(' Operator
'lpost_b' Name
' ' Text
'x' Name
')' Operator
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'(' Operator
'g' Name
' ' Text
'x' Name
')' Operator
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'm1' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'(' Operator
'bind_lpre' Name
' ' Text
'next_lpre' Name
' ' Text
'next_lpost' Name
' ' Text
'lpre_b' Name
')' Operator
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
'\n ' Text
'by' Keyword
' ' Text
'norm' Name
' ' Text
'(' Operator
'[' Operator
'delta_only' Name
' ' Text
'[' Operator
'`' Keyword
'%' Operator
'bind_lpre' Name
']' Operator
']' Operator
')' Operator
';' Operator
'\n\n ' Text
'Step' Name.Class
' ' Text
'next_pre' Name
' ' Text
'post_b' Name
'\n ' Text
'(' Operator
'bind_lpre' Name
' ' Text
'next_lpre' Name
' ' Text
'next_lpost' Name
' ' Text
'lpre_b' Name
')' Operator
'\n ' Text
'(' Operator
'bind_lpost' Name
' ' Text
'next_lpre' Name
' ' Text
'next_lpost' Name
' ' Text
'lpost_b' Name
')' Operator
'\n ' Text
'(' Operator
'Bind' Name.Class
' ' Text
'f' Name
' ' Text
'g' Name
')' Operator
'\n' Text
'#' Operator
'pop' Name
'-' Operator
'options' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_frame_ret_aux' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'p' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'p' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'p' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Frame' Name.Class
'?' Operator
' ' Text
'f' Name
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Frame' Name.Class
'?.' Operator
'f' Name
' ' Text
'f' Name
')' Operator
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'M' Name.Namespace
'.' Punctuation
'MSTATE' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'st' Name
'.' Operator
'locks_preorder' Name
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'M' Name.Namespace
'.' Punctuation
'MSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'->' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Frame' Name.Class
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'p' Name
' ' Text
'x' Name
' ' Text
'lp' Name
')' Operator
' ' Text
'frame' Name
' ' Text
'f_frame' Name
' ' Text
'->' Operator
'\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'p' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
' ' Text
'p' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
'\n ' Text
'(' Operator
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
' ' Text
'lpost' Name
' ' Text
'h' Name
' ' Text
'x' Name
' ' Text
'h' Name
')' Operator
'\n ' Text
'lpost' Name
'\n ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
' ' Text
'p' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'x' Name
' ' Text
'lpost' Name
')' Operator
',' Operator
' ' Text
'm0' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_frame_ret' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'p' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'p' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'p' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Frame' Name.Class
'?' Operator
' ' Text
'f' Name
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Frame' Name.Class
'?.' Operator
'f' Name
' ' Text
'f' Name
')' Operator
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'NMSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'_' Name
',' Operator
' ' Text
'n' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'step_frame_ret_aux' Name
' ' Text
'f' Name
',' Operator
' ' Text
'n' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_frame' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'p' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'p' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'p' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Frame' Name.Class
'?' Operator
' ' Text
'f' Name
'}' Operator
')' Operator
'\n ' Text
'(' Operator
'step' Name
':' Operator
'step_t' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Frame' Name.Class
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'p' Name
' ' Text
'x' Name
' ' Text
'lp' Name
')' Operator
' ' Text
'frame' Name
' ' Text
'f_frame' Name
' ' Text
'->' Operator
' ' Text
'step_frame_ret' Name
' ' Text
'f' Name
'\n\n ' Text
'|' Operator
' ' Text
'Frame' Name.Class
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'f_pre' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'f' Name
' ' Text
'frame' Name
' ' Text
'f_frame' Name
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'm0' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'Step' Name.Class
' ' Text
'next_fpre' Name
' ' Text
'next_fpost' Name
' ' Text
'next_flpre' Name
' ' Text
'next_flpost' Name
' ' Text
'f' Name
' ' Text
'=' Operator
' ' Text
'step' Name
' ' Text
'f' Name
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'm1' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'preserves_frame_star' Name
' ' Text
'f_pre' Name
' ' Text
'next_fpre' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'frame' Name
';' Operator
'\n\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'(' Operator
'frame_lpre' Name
' ' Text
'next_flpre' Name
' ' Text
'f_frame' Name
')' Operator
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
')' Operator
'\n ' Text
'by' Keyword
' ' Text
'(' Operator
'norm' Name
' ' Text
'[' Operator
'delta_only' Name
' ' Text
'[' Operator
'`' Keyword
'%' Operator
'frame_lpre' Name
']' Operator
']' Operator
')' Operator
';' Operator
'\n\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'next_fpre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'x' Name
' ' Text
'->' Operator
' ' Text
'next_fpost' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'frame' Name
')' Operator
'\n ' Text
'(' Operator
'frame_lpre' Name
' ' Text
'next_flpre' Name
' ' Text
'f_frame' Name
')' Operator
'\n ' Text
'(' Operator
'frame_lpost' Name
' ' Text
'next_flpre' Name
' ' Text
'next_flpost' Name
' ' Text
'f_frame' Name
')' Operator
'\n ' Text
'(' Operator
'Frame' Name.Class
' ' Text
'f' Name
' ' Text
'frame' Name
' ' Text
'f_frame' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_par_ret_aux' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Par' Name.Class
'?' Operator
' ' Text
'f' Name
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Par' Name.Class
'?.' Operator
'mL' Name
' ' Text
'f' Name
')' Operator
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Par' Name.Class
'?.' Operator
'mR' Name
' ' Text
'f' Name
')' Operator
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'M' Name.Namespace
'.' Punctuation
'MSTATE' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'st' Name
'.' Operator
'mem' Name
' ' Text
'st' Name
'.' Operator
'locks_preorder' Name
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'M' Name.Namespace
'.' Punctuation
'MSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'->' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Par' Name.Class
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'aL' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'pL' Name
' ' Text
'xL' Name
' ' Text
'lpL' Name
')' Operator
' ' Text
'#' Operator
'aR' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'pR' Name
' ' Text
'xR' Name
' ' Text
'lpR' Name
')' Operator
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'lpost' Name
' ' Text
':' Operator
' ' Text
'l_post' Name
'\n ' Text
'#' Operator
'st' Name
' ' Text
'#' Operator
'(' Operator
'aL' Name
' ' Text
'&' Operator
' ' Text
'aR' Name
')' Operator
'\n ' Text
'(' Operator
'pL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pR' Name
' ' Text
'xR' Name
')' Operator
'\n ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'pL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pR' Name
' ' Text
'xR' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'fun' Keyword
' ' Text
'h0' Name
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'h1' Name
' ' Text
'->' Operator
' ' Text
'lpL' Name
' ' Text
'h0' Name
' ' Text
'xL' Name
' ' Text
'h1' Name
' ' Text
'/\\' Operator
' ' Text
'lpR' Name
' ' Text
'h0' Name
' ' Text
'xR' Name
' ' Text
'h1' Name
'\n ' Text
'in' Keyword
'\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'pL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'pL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pR' Name
' ' Text
'xR' Name
')' Operator
'\n ' Text
'(' Operator
'fun' Keyword
' ' Text
'h' Name
' ' Text
'->' Operator
' ' Text
'lpL' Name
' ' Text
'h' Name
' ' Text
'xL' Name
' ' Text
'h' Name
' ' Text
'/\\' Operator
' ' Text
'lpR' Name
' ' Text
'h' Name
' ' Text
'xR' Name
' ' Text
'h' Name
')' Operator
'\n ' Text
'lpost' Name
'\n ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'pL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'pR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'lpost' Name
')' Operator
',' Operator
' ' Text
'm0' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_par_ret' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Par' Name.Class
'?' Operator
' ' Text
'f' Name
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Par' Name.Class
'?.' Operator
'mL' Name
' ' Text
'f' Name
')' Operator
' ' Text
'/\\' Operator
' ' Text
'Ret' Name.Class
'?' Operator
' ' Text
'(' Operator
'Par' Name.Class
'?.' Operator
'mR' Name
' ' Text
'f' Name
')' Operator
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'NMSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'_' Name
',' Operator
' ' Text
'n' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'step_par_ret_aux' Name
' ' Text
'f' Name
',' Operator
' ' Text
'n' Name
')' Operator
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_par' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Par' Name.Class
'?' Operator
' ' Text
'f' Name
'}' Operator
')' Operator
'\n ' Text
'(' Operator
'step' Name
':' Operator
'step_t' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Par' Name.Class
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'_' Name
')' Operator
' ' Text
'(' Operator
'Ret' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'_' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'step_par_ret' Name
' ' Text
'f' Name
'\n\n ' Text
'|' Operator
' ' Text
'Par' Name.Class
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'aL' Name
' ' Text
'#' Operator
'preL' Name
' ' Text
'#' Operator
'postL' Name
' ' Text
'#' Operator
'lpreL' Name
' ' Text
'#' Operator
'lpostL' Name
' ' Text
'mL' Name
' ' Text
'#' Operator
'aR' Name
' ' Text
'#' Operator
'preR' Name
' ' Text
'#' Operator
'postR' Name
' ' Text
'#' Operator
'lpreR' Name
' ' Text
'#' Operator
'lpostR' Name
' ' Text
'mR' Name
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'b' Name
' ' Text
'=' Operator
' ' Text
'sample' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'if' Keyword
' ' Text
'b' Name
' ' Text
'then' Keyword
' ' Text
'begin' Name
'\n ' Text
'let' Keyword.Declaration
' ' Text
'm0' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'Step' Name.Class
' ' Text
'next_preL' Name
' ' Text
'next_postL' Name
' ' Text
'next_lpreL' Name
' ' Text
'next_lpostL' Name
' ' Text
'mL' Name
' ' Text
'=' Operator
' ' Text
'step' Name
' ' Text
'mL' Name
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'm1' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'preserves_frame_star' Name
' ' Text
'preL' Name
' ' Text
'next_preL' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'preR' Name
';' Operator
'\n ' Text
'par_weaker_lpre_and_stronger_lpost_l' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'next_lpreL' Name
' ' Text
'next_lpostL' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
';' Operator
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'next_post' Name
' ' Text
'=' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'next_postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'in' Keyword
'\n\n ' Text
'assert' Name.Exception
' ' Text
'(' Operator
'stronger_post' Name
' ' Text
'post' Name
' ' Text
'next_post' Name
')' Operator
' ' Text
'by' Keyword
' ' Text
'(' Operator
'norm' Name
' ' Text
'[' Operator
'delta_only' Name
' ' Text
'[' Operator
'`' Keyword
'%' Operator
'stronger_post' Name
']' Operator
']' Operator
')' Operator
';' Operator
'\n\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'next_preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'preR' Name
')' Operator
' ' Text
'next_post' Name
'\n ' Text
'(' Operator
'par_lpre' Name
' ' Text
'next_lpreL' Name
' ' Text
'lpreR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpost' Name
' ' Text
'next_lpreL' Name
' ' Text
'next_lpostL' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
')' Operator
'\n ' Text
'(' Operator
'Par' Name.Class
' ' Text
'mL' Name
' ' Text
'mR' Name
')' Operator
'\n\n ' Text
'end' Keyword
'\n ' Text
'else' Keyword
' ' Text
'begin' Name
'\n ' Text
'let' Keyword.Declaration
' ' Text
'm0' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'Step' Name.Class
' ' Text
'next_preR' Name
' ' Text
'next_postR' Name
' ' Text
'next_lpreR' Name
' ' Text
'next_lpostR' Name
' ' Text
'mR' Name
' ' Text
'=' Operator
' ' Text
'step' Name
' ' Text
'mR' Name
' ' Text
'in' Keyword
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'm1' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'preserves_frame_star_left' Name
' ' Text
'preR' Name
' ' Text
'next_preR' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'preL' Name
';' Operator
'\n ' Text
'par_weaker_lpre_and_stronger_lpost_r' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'lpreR' Name
' ' Text
'lpostR' Name
' ' Text
'next_lpreR' Name
' ' Text
'next_lpostR' Name
' ' Text
'm0' Name
' ' Text
'm1' Name
';' Operator
'\n\n ' Text
'let' Keyword.Declaration
' ' Text
'next_post' Name
' ' Text
'=' Operator
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'xL' Name
',' Operator
' ' Text
'xR' Name
')' Operator
' ' Text
'->' Operator
' ' Text
'postL' Name
' ' Text
'xL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'next_postR' Name
' ' Text
'xR' Name
')' Operator
' ' Text
'in' Keyword
'\n\n ' Text
'stronger_post_par_r' Name
' ' Text
'postL' Name
' ' Text
'postR' Name
' ' Text
'next_postR' Name
';' Operator
'\n\n ' Text
'Step' Name.Class
' ' Text
'(' Operator
'preL' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'next_preR' Name
')' Operator
' ' Text
'next_post' Name
'\n ' Text
'(' Operator
'par_lpre' Name
' ' Text
'lpreL' Name
' ' Text
'next_lpreR' Name
')' Operator
'\n ' Text
'(' Operator
'par_lpost' Name
' ' Text
'lpreL' Name
' ' Text
'lpostL' Name
' ' Text
'next_lpreR' Name
' ' Text
'next_lpostR' Name
')' Operator
'\n ' Text
'(' Operator
'Par' Name.Class
' ' Text
'mL' Name
' ' Text
'mR' Name
')' Operator
'\n ' Text
'end' Keyword
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'step_weaken' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
'{' Operator
'Weaken' Name.Class
'?' Operator
' ' Text
'f' Name
'}' Operator
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
' ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
' ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'NMSTATE' Name.Class
'?.' Operator
'reflect' Name
' ' Text
'(' Operator
'fun' Keyword
' ' Text
'(' Operator
'_' Name
',' Operator
' ' Text
'n' Name
')' Operator
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'Weaken' Name.Class
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'pre' Name
' ' Text
'#' Operator
'post' Name
' ' Text
'#' Operator
'lpre' Name
' ' Text
'#' Operator
'lpost' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'#' Operator
'_' Name
' ' Text
'f' Name
' ' Text
'=' Operator
' ' Text
'f' Name
' ' Text
'in' Keyword
'\n\n ' Text
'Step' Name.Class
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
' ' Text
'f' Name
',' Operator
' ' Text
'n' Name
')' Operator
'\n\n' Text
'/// Step function' Comment
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'rec' Keyword.Declaration
' ' Text
'step' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'(' Operator
'step_result' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'step_req' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'(' Operator
'step_ens' Name
' ' Text
'f' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Ret' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'step_ret' Name
' ' Text
'f' Name
'\n ' Text
'|' Operator
' ' Text
'Bind' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'step_bind' Name
' ' Text
'f' Name
' ' Text
'step' Name
'\n ' Text
'|' Operator
' ' Text
'Act' Name.Class
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'step_act' Name
' ' Text
'f' Name
'\n ' Text
'|' Operator
' ' Text
'Frame' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'step_frame' Name
' ' Text
'f' Name
' ' Text
'step' Name
'\n ' Text
'|' Operator
' ' Text
'Par' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'step_par' Name
' ' Text
'f' Name
' ' Text
'step' Name
'\n ' Text
'|' Operator
' ' Text
'Weaken' Name.Class
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'step_weaken' Name
' ' Text
'f' Name
'\n\n' Text
'let' Keyword.Declaration
' ' Text
'rec' Keyword.Declaration
' ' Text
'run' Name
'\n ' Text
'(' Operator
'#' Operator
'st' Name
':' Operator
'st' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'a' Name
':' Operator
'Type' Name.Class
' ' Text
'u#' Operator
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'pre' Name
':' Operator
'st' Name
'.' Operator
'hprop' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'post' Name
':' Operator
'post_t' Name
' ' Text
'st' Name
' ' Text
'a' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpre' Name
':' Operator
'l_pre' Name
' ' Text
'pre' Name
')' Operator
'\n ' Text
'(' Operator
'#' Operator
'lpost' Name
':' Operator
'l_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
')' Operator
'\n ' Text
'(' Operator
'f' Name
':' Operator
'm' Name
' ' Text
'st' Name
' ' Text
'a' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'lpre' Name
' ' Text
'lpost' Name
')' Operator
'\n ' Text
':' Operator
' ' Text
'Mst' Name.Class
' ' Text
'a' Name
'\n ' Text
'(' Operator
'requires' Keyword
' ' Text
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'->' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'pre' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'/\\' Operator
'\n ' Text
'lpre' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
')' Operator
'\n ' Text
'(' Operator
'ensures' Keyword
' ' Text
'fun' Keyword
' ' Text
'm0' Name
' ' Text
'x' Name
' ' Text
'm1' Name
' ' Text
'->' Operator
'\n ' Text
'st' Name
'.' Operator
'interp' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
' ' Text
'`st.star`' Operator.Word
' ' Text
'st' Name
'.' Operator
'locks_invariant' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'm1' Name
' ' Text
'/\\' Operator
'\n ' Text
'lpost' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm0' Name
')' Operator
' ' Text
'x' Name
' ' Text
'(' Operator
'st' Name
'.' Operator
'core' Name
' ' Text
'm1' Name
')' Operator
' ' Text
'/\\' Operator
'\n ' Text
'preserves_frame' Name
' ' Text
'pre' Name
' ' Text
'(' Operator
'post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'm1' Name
')' Operator
'\n ' Text
'=' Operator
'\n ' Text
'match' Keyword
' ' Text
'f' Name
' ' Text
'with' Keyword
'\n ' Text
'|' Operator
' ' Text
'Ret' Name.Class
' ' Text
'_' Name
' ' Text
'x' Name
' ' Text
'_' Name
' ' Text
'->' Operator
' ' Text
'x' Name
'\n\n ' Text
'|' Operator
' ' Text
'_' Name
' ' Text
'->' Operator
'\n ' Text
'let' Keyword.Declaration
' ' Text
'm0' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n ' Text
'let' Keyword.Declaration
' ' Text
'Step' Name.Class
' ' Text
'new_pre' Name
' ' Text
'new_post' Name
' ' Text
'_' Name
' ' Text
'_' Name
' ' Text
'f' Name
' ' Text
'=' Operator
' ' Text
'step' Name
' ' Text
'f' Name
' ' Text
'in' Keyword
'\n ' Text
'let' Keyword.Declaration
' ' Text
'm1' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n ' Text
'let' Keyword.Declaration
' ' Text
'x' Name
' ' Text
'=' Operator
' ' Text
'run' Name
' ' Text
'f' Name
' ' Text
'in' Keyword
'\n ' Text
'let' Keyword.Declaration
' ' Text
'm2' Name
' ' Text
'=' Operator
' ' Text
'get' Name
' ' Text
'()' Name.Builtin.Pseudo
' ' Text
'in' Keyword
'\n\n ' Text
'preserves_frame_trans' Name
' ' Text
'pre' Name
' ' Text
'new_pre' Name
' ' Text
'(' Operator
'new_post' Name
' ' Text
'x' Name
')' Operator
' ' Text
'm0' Name
' ' Text
'm1' Name
' ' Text
'm2' Name
';' Operator
'\n ' Text
'preserves_frame_stronger_post' Name
' ' Text
'pre' Name
' ' Text
'post' Name
' ' Text
'new_post' Name
' ' Text
'x' Name
' ' Text
'm0' Name
' ' Text
'm2' Name
';' Operator
'\n ' Text
'x' Name
'\n' Text
Reference in a new issue View git blame Copy permalink