module.bnf 1.07 KB
Newer Older
1 2 3 4 5 6 7
\begin{syntax}
  module ::= "module" uident label* mdecl* "end"
  \
  mdecl ::= decl                                ; theory declaration
    | "type" mtype-decl ("with" mtype-decl)*    ; mutable types
    | "let" lident label* pgm-defn              ;
    | "let" "rec" recfun ("with" recfun)*  ;
8
    | "val" lident label* pgm-decl        ;
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
    | "exception" lident label* type?           ;
    | "use" imp-exp "module" tqualid ("as" uident-opt)?     ;
    | "namespace" "import"? uident-opt mdecl* "end" ;
  \
  mtype-decl ::= lident label* ("'" lident label*)* mtype-defn;
  \
  mtype-defn ::=                                     ; abstract type
    | "=" type                                       ; alias type
    | "=" "|"? type-case ("|" type-case)*            ; algebraic type
    | "=" "{|" mrecord-field (";" mrecord-field)* "|}" ; record type
  \
  mrecord-field ::= "mutable"? lident label* ":" type
  \
  pgm-decl ::= ":" type-v    ;
    | type-v-param+ ":" type-c    ;
  \
  pgm-defn ::= type-v-param+ (":" type)? "=" triple ;
    | "=" "fun" type-v-param+ "->" triple ;
\end{syntax}