theory.bnf 1.66 KB
Newer Older
1
\begin{syntax}
2
  theory ::= "theory" uident-nq label* decl* "end"
3
  \
4
  decl ::= "type" type-decl ("with" type-decl)* ;
5
    | "constant" constant-decl ;
6 7
    | "function" function-decl ("with" logic-decl)* ;
    | "predicate" predicate-decl ("with" logic-decl)* ;
8
    | "inductive" inductive-decl ("with" inductive-decl)* ;
9
    | "coinductive" inductive-decl ("with" inductive-decl)* ;
10 11 12
    | "axiom" ident-nq ":" formula 	   ;
    | "lemma" ident-nq ":" formula 	   ;
    | "goal"  ident-nq ":" formula 	   ;
13 14
    | "use" imp-exp tqualid ("as" uident)?     ;
    | "clone" imp-exp tqualid ("as" uident)? subst? ;
15 16
    | "scope" "import"? uident-nq decl* "end" ;
    | "import" uident ;
17
  \
18 19 20
  logic-decl ::= function-decl ;
    | predicate-decl
  \
21 22
  constant-decl ::= lident-nq label* ":" type ;
    | lident-nq label* ":" type "=" term
23
  \
24 25
  function-decl ::= lident-nq label* type-param* ":" type ;
    | lident-nq label* type-param* ":" type "=" term
26
  \
27 28
  predicate-decl ::= lident-nq label* type-param* ;
    | lident-nq label* type-param* "=" formula
29
  \
30
  inductive-decl ::= lident-nq label* type-param* "=" ;
31 32
                     "|"? ind-case ("|" ind-case)* ;
  \
33
  ind-case ::= ident-nq label* ":" formula ;
34
  \
35 36 37 38 39
  imp-exp ::= ("import" | "export")?
  \
  subst ::= "with" ("," subst-elt)+
  \
  subst-elt ::= "type" lqualid "=" lqualid ;
40 41
    | "function" lqualid "=" lqualid          ;
    | "predicate" lqualid "=" lqualid         ;
42
    | "scope" (uqualid | ".") "=" (uqualid | ".")  ;
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
43 44
    | "lemma" qualid 	  		   ;
    | "goal"  qualid			   ;
45
  \
46
  tqualid ::= uident | ident ("." ident)* "." uident ;
47 48
  \
  type-decl ::= lident-nq label* ("'" lident-nq label*)* type-defn; %
49
\end{syntax}