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