#line 708 "/home/ubuntu/felix/src/packages/grammar.fdoc"
//$ Assertion statements.
//$ See also functions to find pre- and post-conditions.
syntax assertions {
  requires statements;

  stmt = assertion_stmt;

  //$ The usual assert statement.
  //$ Abort the program if the argument expression evaluates to false
  //$ when control flows through the assert statement.
  //$ Cannot be switched off!
  private assertion_stmt := "assert" sexpr ";" =># "`(ast_assert ,_sr ,_2)";

  //$ Static assert: type expression of kind BOOL required
  private assertion_stmt := "static-assert" stype ";" =># "`(ast_static_assert ,_sr ,_2)";

  //$ Define an axiom with a general predicate.
  //$ An axiom is a function which is true for all arguments.
  //$ Axioms are core assertions about invariants which
  //$ can be used to specify semantics and form the basis
  //$ of reasoning about semantics which goes beyond
  //$ structure.
  private assertion_stmt  := "axiom" sdeclname sfun_arg ":" sexpr ";" =>#
    """
      `(ast_axiom ,_sr ,(first _2) ,(second _2) ,_3 (Predicate ,_5))
    """;

  //$ A variant of an axiom which expresses the semantic
  //$ equality of two expressions. Do not confuse this
  //$ with an expresion containing run time equality (==).
  //$ Semantic equality means that one expression could be
  //$ replaced by the other without any observable difference
  //$ in behaviour in any program, this can be asserted even
  //$ if the type does not provide an equality operator (==).
  private assertion_stmt  := "axiom" sdeclname sfun_arg ":" sexpr "=" sexpr ";" =>#
    """
      `(ast_axiom ,_sr ,(first _2) ,(second _2) ,_3 (Equation (,_5 ,_7)))
    """;

  //$ A lemma is a proposition which it is expected could
  //$ be proved by a good automatic theorem prover,
  //$ given the axioms. This is the predicate form.
  private assertion_stmt  := "lemma" sdeclname sfun_arg ":" sexpr ";" =>#
    """
      `(ast_lemma ,_sr ,(first _2) ,(second _2) ,_3 (Predicate ,_5))
    """;

  //$ A lemma is a proposition which it is expected could
  //$ be proved by a good automatic theorem prover,
  //$ given the axioms. This is the equational form.
  private assertion_stmt  := "lemma" sdeclname sfun_arg ":" sexpr "=" sexpr ";" =>#
    """
      `(ast_lemma ,_sr ,(first _2) ,(second _2) ,_3 (Equation (,_5 ,_7)))
    """;

  //$ A theorem is a proposition which it is expected could
  //$ NOT be proved by a good automatic theorem prover,
  //$ given the axioms.  In the future, we might like to
  //$ provide a "proof sketch" which a suitable tool could
  //$ fill in. For the present, you can give a proof as
  //$ plain text in a string as a hint to the reader.
  //$
  //$ This is the predicative form.
  private assertion_stmt  := "theorem" sdeclname sfun_arg ":" sexpr proof? ";" =>#
    """
      `(ast_axiom ,_sr ,(first _2) ,(second _2) ,_3 (Predicate ,_5))
    """;
    proof := "proof" sstring;

  //$ A theorem is a proposition which it is expected could
  //$ NOT be proved by a good automatic theorem prover,
  //$ given the axioms.  In the future, we might like to
  //$ provide a "proof sketch" which a suitable tool could
  //$ fill in. For the present, you can give a proof as
  //$ plain text in a string as a hint to the reader.
  //$
  //$ This is the equational form.
  private assertion_stmt  := "theorem" sdeclname sfun_arg ":" sexpr "=" sexpr proof? ";" =>#
    """
      `(ast_axiom ,_sr ,(first _2) ,(second _2) ,_3 (Equation (,_5 ,_7)))
    """;

  //$ A reduction is a special kind of proposition of equational
  //$ form which also directs the compiler to actually replace
  //$ the LHS expression with the RHS expression when found.
  //$
  //$ Reductions allow powerful high level optimisations,
  //$ such as eliminating two successive list reversals.
  //$
  //$ The client must take great care that reductions don't
  //$ lead to infinite loops. Confluence isn't required but
  //$ is probably desirable.
  //$
  //$ Reductions should be used sparingly because searching
  //$ for patterns to reduce is applied to every sub-expression
  //$ of every expression in the whole program, repeatedly
  //$ after any reduction is applied, and this whole process
  //$ is done at several different places in the program,
  //$ to try to effect the reductions. Particularly both
  //$ before and after inlining, since that can destroy
  //$ or create candidate patterns.

  private assertion_stmt  := "reduce" sname "|"? sreductions ";"  =>#
    """
      `(ast_reduce ,_sr ,_2 ,_4)
    """;

     private sreduce_args := "(" stypeparameter_comma_list ")" =># "_2";
     private sreduction := stvarlist sreduce_args ":" sexpr "=>" sexpr =># "`(,_1 ,_2 ,_4 ,_6)";
     private sreductions := sreduction =># "`(,_1)";
     private sreductions := sreduction "|" sreductions =># "(cons _1 _3)";
}