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