Previous Up Next

10  Definition files

Type declarations only use type and ->, and as type constructors can only be applied on proper types, type never appears under more than one -> (1).


type_decl::= Kind <id> <kind>.
kind::= type -> <kind>
 | type
Figure 1: Grammar of type declarations.

Constant declarations have the structure described in 2, with additional constraints on type variables as described in 9.


constant_decl::= Type <id> <type>.
type::=<type> -> <type>
 |<type_atom>
type_atom::=<type_atom> (<type_atom>)
 |<type_atom> <type_variable>
 |<id>
Figure 2: Grammar of constant declarations.

Definitions are given as blocks with a header containing predicate declarations, and an optional body containing a set of clauses, in which uppercase variables are implicitly universally quantified (3). A predicate with no definition clauses is always false; the head of a bodiless clause is always true. A predicate can only depend on predicates defined up to its definition block, so multiple predicates in one block is the only way to achieve mutual recursion. One can see definition blocks as groups of predicates belonging to the same stratum; stratification forbids predicates from the same block to depend negatively one on the other, as usual, but here it also forbids the use of inductive and coinductive in the same block for similar reasons.


definition_block::= Define <declarations> .
 | Define <declarations> by <clauses> .
declarations::=<declaration> , <declarations>
 |<declaration>
declaration::=<flavour> <id> : <type>
flavour::= inductive
 | coinductive
 | 
clauses::=<clause> ; <clauses>
 |<clause>
clause::=<head> := <body>
 |<head>
head::=<id> <atom>*
body::=<formula>
Figure 3: Grammar of predicates declarations and definitions.

Theorems are horn-like formulae which head must be an atom obtained by the application of an already defined predicate (4). For a non-recursive predicate, they can be seen as additional clauses, admissible by the definition with respect to the logic, if not to Bedwyr. Their names holds no semantic value.


theorem::= Theorem <id> : <body> -> <head> . <proof> Qed.
Figure 4: Grammar of theorems specifications.


Previous Up Next