#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)";
}