<commit_before><program>          ::=  <package>?
                        import org . sireum . _
                        <stmt>*
                        
<package>          ::=  package <name>

<name>             ::=  <id> ⸨ . <id> ⸩*
                   
<stmt>             ::=  <import-stmt>
                     |  <decl-stmt>
                     |  <assign-stmt>
                     |  <if-stmt>
                     |  <while-stmt>
                     |  <for-stmt>
                     |  <return-stmt>
                     |  <proof-stmt>

<import-stmt>      ::=  import <name> <import-suffix>?

<import-suffix>    ::=  . _
                     |  . { <import-sels> }

<import-sels>      ::=  <import-sel> ⸨ , <import-sel> ⸩*

<import-sel>       ::=  <id>
                     |  <id> => <id>

<decl-stmt>        ::=  <var-decl>  
                     |  <def-decl>
                     |  <object-decl>
                     |  <sig-decl>
                     |  <datatype-decl>
                     |  <record-decl>
                     |  <rich-decl>
                     
<var-decl>         ::=  val <id> ⸨ : <type> ⸩? = <exp>
                     |  var <id> ⸨ : <type> ⸩? = <exp>
                     |  var <id> : <type> = _
                     |  val <pattern> = <exp>  
                     |  var <pattern> = <exp>  
                     |  @spec val <id> : <type> = $
                     |  @spec var <id> : <type> = $
                     
<pattern>          ::=  <id> ⸨ : <type> ⸩?
                     |  ⸨ <id> @ ⸩? <name> ( <paterns>? )
                     |  ( <paterns> )
                     |  _ ⸨ : <type> ⸩?

<patterns>         ::=  <pattern> ⸨ , <pattern> ⸩*
                   
<def-decl>         ::=  ⸨ @pure ⸩? def <id> <params>? : <type> = <def-body>
                     |  ⸨ @pure ⸩? def <id> <params>? : <type> = $
                     |  ⸨ @pure ⸩? def <id> <params>? : <type> = <cdef-contract>
                     |  ⸨ @pure ⸩? def <id> <params>? : <type>
                     |  @spec def <id> <params>? : <type> = $
                     |  @spec def <id> <params>? : <type> = <cdef-contract>

<params>           ::=  ( ⸨ <param> ⸨ , param> ⸩* ⸩? )

<param>            ::=  ⸨ @pure ⸩? <id> : <type>

<def-body>         ::=  {
                          <ldef-contract>?
                          <stmt>*                     
                        }

<object-decl>      ::=  object <id> <extends>? { <stmt>* }
                     |  @ext object <id> { <stmt>* }
                        
<extends>          ::=  extends <type> ⸨ with <type> ⸩*

<sig-decl>         ::=  @sig trait <id> <tparams>? <extends>? { <stmt>* }

<tparams>          ::=  [ <tparam> ⸨ , <tparam> ⸩* ]

<tparam>           ::=  <id> ⸨ <: type ⸩?

<datatype-decl>    ::=  @datatype trait <id> <tparams>? <extends>? { <stmt>* }
                     |  @datatype class <id> <tparams>? <dt-params>? <extends>? { <stmt>* }

<dt-params>        ::=  ( ⸨ <dt-param> ⸨ , <dt-param> ⸩* ⸩? )

<dt-param>         ::=  <adt-param-mod>* <id> : <type>

<adt-param-mod>    ::=  @pure
                     |  @hidden

<record-decl>      ::=  @record trait <id> <tparams>? <extends>? { <stmt>* }
                     |  @record class <id> <tparams>? <rd-params>? <extends>? { <stmt>* }

<rd-params>        ::=  ( ⸨ <rd-param> ⸨ , <rd-param> ⸩* ⸩? )

<rd-param>         ::=  <adt-param-mod>* ⸨ var ⸩*  <id> : <type>

<rich-decl>        ::=  @rich trait <id> <tparams> { <stmt>* }
                     |  @rich class <id> <tparams>? <params>? <extends>? { <stmt>* }

<assign-stmt>      ::=  <lhs> = <exp>
                     |  up ( <lhs> ) = <exp>

<lhs>              ::=  <id>
                     |  <lhs> . <id>
                     |  <lhs> ( <exp> )

<if-stmt>          ::=  if ( <exp> ) { <stmt>* } ⸨ else { <stmt>* } ⸩?
                     |  if ( <exp> ) { <stmt>* } else <if-stmt>

<while-stmt>       ::=  while ( <exp> ) {
                          <loop-contract>?
                          <stmt>*
                        }
                     |  do {
                          <stmt>*
                          <loop-contract>?
                        } while ( <exp> )

<for-stmt>         ::=  for ( <for-gen> ) {
                          <loop-contract>?
                          <stmt>*
                        }

<for-gen>          ::=  <id> <- <for-range>

<for-range>        ::=  <exp> until <exp> ⸨ by <exp> ⸩?
                     |  <exp> to <exp> ⸨ by <exp> ⸩?
                     |  <exp>
                     |  <exp> . indices
                     |  <exp> . reverseIndices

=-=
=-<
<-=
<-<
>-=
>->
=-|   |-<
<-|   |-=
<-|   |-<
>-|   |-=
>-|   |->

<return-stmt>      ::=  return <exp>?

<proof-stmt>       ::=  assert(<exp>)
                     |  assert(<exp>, <string-exp>)
                     |  assume(<exp>)
                     |  assume(<exp>, <string-exp>)
                     |  l""" <l-proof> """

<exp>              ::=

<l-proof>          ::=  <fact>
                     |  <theorem>
                     |  <invariant>
                     |  <sequent>
                     |  <proof>

<cdef-contract>    ::=  c""" <def-contract> """

<ldef-contract>    ::=  l""" <def-contract> """
<commit_msg>Updated.<commit_after><program>          ::=  <package>?
                        import org . sireum . _
                        <stmt>*
                        
<package>          ::=  package <name>

<name>             ::=  <ID> ⸨ . <ID> ⸩*
                   
<stmt>             ::=  <import-stmt>
                     |  <decl-stmt>
                     |  <assign-stmt>
                     |  <print-stmt>
                     |  <if-stmt>
                     |  <match-stmt>
                     |  <while-stmt>
                     |  <for-stmt>
                     |  <return-stmt>
                     |  <proof-stmt>

<import-stmt>      ::=  import <name> <import-suffix>?

<import-suffix>    ::=  . _
                     |  . { <import-sels> }

<import-sels>      ::=  <import-sel> ⸨ , <import-sel> ⸩*

<import-sel>       ::=  <ID>
                     |  <ID> => <ID>

<decl-stmt>        ::=  <var-decl>  
                     |  <def-decl>
                     |  <object-decl>
                     |  <sig-decl>
                     |  <datatype-decl>
                     |  <record-decl>
                     |  <rich-decl>
                     
<var-decl>         ::=  val <ID> ⸨ : <type> ⸩? = <exp>
                     |  var <ID> ⸨ : <type> ⸩? = <exp>
                     |  var <ID> : <type> = _
                     |  val <pattern> = <exp>  
                     |  var <pattern> = <exp>  
                     |  @spec val <ID> : <type> = $
                     |  @spec var <ID> : <type> = $

<type>             ::=  <name> <type-args>?
                     |  ( <type> ⸨ , <type> ⸩+ )
                     |  <type> => <type>

<type-args>        ::=  [ <type> ⸨ , <type> ⸩* ]

<pattern>          ::=  <ID> ⸨ : <type> ⸩?
                     |  ⸨ <ID> @ ⸩? <name> ( <paterns>? )
                     |  ( <paterns> )
                     |  _ ⸨ : <type> ⸩?

<patterns>         ::=  <pattern> ⸨ , <pattern> ⸩*
                   
<def-decl>         ::=  ⸨ @pure ⸩? def <ID> <params>? : <type> = <def-body>
                     |  ⸨ @pure ⸩? def <ID> <params>? : <type> = $
                     |  ⸨ @pure ⸩? def <ID> <params>? : <type> = <cdef-contract>
                     |  ⸨ @pure ⸩? def <ID> <params>? : <type>
                     |  @spec def <ID> <params>? : <type> = $
                     |  @spec def <ID> <params>? : <type> = <cdef-contract>

<params>           ::=  ( ⸨ <param> ⸨ , param> ⸩* ⸩? )

<param>            ::=  ⸨ @pure ⸩? <ID> : <type>

<def-body>         ::=  {
                          <ldef-contract>?
                          <stmt>*                     
                        }

<object-decl>      ::=  object <ID> <extends>? { <stmt>* }
                     |  @ext object <ID> { <stmt>* }
                        
<extends>          ::=  extends <type> ⸨ with <type> ⸩*

<sig-decl>         ::=  @sig ⸨ sealed ⸩? trait <ID> <type-params>? <extends>? { <stmt>* }

<type-params>      ::=  [ <type-param> ⸨ , <type-param> ⸩* ]

<type-param>       ::=  <ID> ⸨ <: type ⸩?

<datatype-decl>    ::=  @datatype trait <ID> <type-params>? <extends>? { <stmt>* }
                     |  @datatype class <ID> <type-params>? <dt-params>? <extends>? { <stmt>* }

<dt-params>        ::=  ( ⸨ <dt-param> ⸨ , <dt-param> ⸩* ⸩? )

<dt-param>         ::=  <adt-param-mod>* <ID> : <type>

<adt-param-mod>    ::=  @pure
                     |  @hidden

<record-decl>      ::=  @record trait <ID> <type-params>? <extends>? { <stmt>* }
                     |  @record class <ID> <type-params>? <rd-params>? <extends>? { <stmt>* }

<rd-params>        ::=  ( ⸨ <rd-param> ⸨ , <rd-param> ⸩* ⸩? )

<rd-param>         ::=  <adt-param-mod>* ⸨ var ⸩*  <ID> : <type>

<rich-decl>        ::=  @rich trait <ID> <type-params> { <stmt>* }
                     |  @rich class <ID> <type-params>? <params>? <extends>? { <stmt>* }

<assign-stmt>      ::=  <lhs> = <exp>
                     |  up ( <lhs> ) = <exp>

<lhs>              ::=  <ID>
                     |  <lhs> . <ID>
                     |  <lhs> ( <exp> )

<print-stmt>       ::=  print ( <print-arg> ⸨ , <print-arg> ⸩* )
                     |  println ( ⸨ <print-arg> ⸨ , <print-arg> ⸩* ⸩? )

<print-arg>        ::=  <exp>
                     |  <string-exp>

<if-stmt>          ::=  if ( <exp> ) { <stmt>* } ⸨ else { <stmt>* } ⸩?
                     |  if ( <exp> ) { <stmt>* } else <if-stmt>

<match-stmt>       ::=  <exp> match { <match-case>* }

<match-case>       ::=  case <lit> => <stmt>*
                     |  case <pattern> ⸨ if <exp> ⸩? => <stmt>*

<while-stmt>       ::=  while ( <exp> ) {
                          <loop-contract>?
                          <stmt>*
                        }
                     |  do {
                          <stmt>*
                          <loop-contract>?
                        } while ( <exp> )

<for-stmt>         ::=  for ( <for-gen> ) {
                          <loop-contract>?
                          <stmt>*
                        }

<for-gen>          ::=  <ID> <- <for-range>

<for-range>        ::=  <exp>
                     |  <exp> . indices
                     |  <exp> . reverseIndices
                     |  <exp> =-= <exp>
                     |  <exp> =-< <exp>
                     |  <exp> <-= <exp>
                     |  <exp> <-< <exp>
                     |  <exp> >-= <exp>
                     |  <exp> >-> <exp>
                     |  <exp> =- ( <exp>  ) -< <exp>
                     |  <exp> <- ( <exp>  ) -= <exp>
                     |  <exp> <- ( <exp>  ) -< <exp>
                     |  <exp> >- ( <exp>  ) -= <exp>
                     |  <exp> >- ( <exp>  ) -> <exp>

<return-stmt>      ::=  return <exp>?

<proof-stmt>       ::=  assert(<exp>)
                     |  assert(<exp>, <string-exp>)
                     |  assume(<exp>)
                     |  assume(<exp>, <string-exp>)
                     |  l""" <l-proof> """

<exp>              ::=  <lit>
                     |  <string-interpolation>
                     |  <name>
                     |  <exp> _
                     |  ( <exp> ⸨ , <exp> ⸩* )
                     |  <exp> . <ID> <args>?
                     |  <exp> <args>
                     |  <exp> ( <up> ⸨ , <up> ⸩* )
                     |  <unary-op> <exp>
                     |  <exp> <binary-op> <exp>
                     |  if ( <exp> ) <exp> else <exp>

<lit>              ::=  <INT>
                     |  <FLOAT>
                     |  <STRING>
                     |  z"<INT>"
                     |  z8"<INT>"
                     |  z16"<INT>"
                     |  z32"<INT>"
                     |  z64"<INT>"
                     |  n"<INT>"
                     |  n8"<INT>"
                     |  n16"<INT>"
                     |  n32"<INT>"
                     |  n64"<INT>"
                     |  s8"<INT>"
                     |  s16"<INT>"
                     |  s32"<INT>"
                     |  s64"<INT>"
                     |  u8"<INT>"
                     |  u16"<INT>"
                     |  u32"<INT>"
                     |  u64"<INT>"
                     |  f32"<FLOAT>"
                     |  f64"<FLOAT>"
                     |  r"<REAL>"

<args>             ::=  <type-args>? ( ⸨ <exp> ⸨ , <exp> ⸩* ⸩? )

<up>               ::= <exp> -> <exp>
                     | <id> = <exp>

<unary-op>         ::=  !
                     |  +
                     |  -
                     |  ~
                     |  ¬

<binary-op>        ::=  +
                     |  -
                     |  *
                     |  /
                     |  %
                     |  ==
                     |  !=
                     |  <<
                     |  >>
                     |  >>>
                     |  <
                     |  <=
                     |  >
                     |  >=
                     |  &
                     |  |
                     |  |^
                     |  ≡
                     |  ≠
                     |  ≤
                     |  ≥
                     |  ∧
                     |  ∨
                     |  ⊻
                     |  →

<l-proof>          ::=  <fact>
                     |  <invariant>
                     |  <sequent>
                     |  <proof>
                     |  <theorem>

<cdef-contract>    ::=  c""" <def-contract> """

<ldef-contract>    ::=  l""" <def-contract> """

{'fraction_non_alphanumeric': 0.1886074095768048, 'fraction_numerical': 0.0023429491872895007, 'mean_word_length': 0.810098065200106, 'pattern_counts': {'":': 0, '<': 577, '<?xml version=': 0, '>': 580, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2175552', 'n_tokens_mistral': 4985, 'n_tokens_neox': 4686, 'n_words': 826}