1.1 --- a/doc-src/Ref/ref.rao Mon May 05 21:18:01 1997 +0200
1.2 +++ b/doc-src/Ref/ref.rao Tue May 06 12:50:16 1997 +0200
1.3 @@ -1,7 +1,7 @@
1.4 -% This file was generated by '/usr/stud/berghofe/latex/rail/rail' from 'ref.rai'
1.5 +% This file was generated by 'rail' from 'ref.rai'
1.6 \rail@t {lbrace}
1.7 \rail@t {rbrace}
1.8 -\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()); \par name: id | string; \par extension : (section +) 'end' ( () | ml ); \par section : classes | default | types | arities | consts | constdefs | trans | defs | rules | oracle ; \par classes : 'classes' ( ( id ( () | '<' (id + ',') ) ) + ) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id; \par \par arities : 'arities' ((( name + ',' ) '::' arity ) + ) ; \par arity : ( () | '(' (sort + ',') ')' ) id ; \par \par consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
1.9 +\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | ( 'infixr' | 'infixl' ) (() | string) nat | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | ((string | longident) + ',')) (() | verbatim) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
1.10 \rail@o {1}{
1.11 \rail@begin{2}{theoryDef}
1.12 \rail@nont{id}[]
1.13 @@ -35,7 +35,7 @@
1.14 \rail@nont{ml}[]
1.15 \rail@endbar
1.16 \rail@end
1.17 -\rail@begin{10}{section}
1.18 +\rail@begin{13}{section}
1.19 \rail@bar
1.20 \rail@nont{classes}[]
1.21 \rail@nextbar{1}
1.22 @@ -47,20 +47,31 @@
1.23 \rail@nextbar{4}
1.24 \rail@nont{consts}[]
1.25 \rail@nextbar{5}
1.26 -\rail@nont{constdefs}[]
1.27 +\rail@nont{syntax}[]
1.28 \rail@nextbar{6}
1.29 \rail@nont{trans}[]
1.30 \rail@nextbar{7}
1.31 \rail@nont{defs}[]
1.32 \rail@nextbar{8}
1.33 +\rail@nont{constdefs}[]
1.34 +\rail@nextbar{9}
1.35 \rail@nont{rules}[]
1.36 -\rail@nextbar{9}
1.37 +\rail@nextbar{10}
1.38 +\rail@nont{axclass}[]
1.39 +\rail@nextbar{11}
1.40 +\rail@nont{instance}[]
1.41 +\rail@nextbar{12}
1.42 \rail@nont{oracle}[]
1.43 \rail@endbar
1.44 \rail@end
1.45 -\rail@begin{4}{classes}
1.46 +\rail@begin{2}{classes}
1.47 \rail@term{classes}[]
1.48 \rail@plus
1.49 +\rail@nont{classDecl}[]
1.50 +\rail@nextplus{1}
1.51 +\rail@endplus
1.52 +\rail@end
1.53 +\rail@begin{3}{classDecl}
1.54 \rail@nont{id}[]
1.55 \rail@bar
1.56 \rail@nextbar{1}
1.57 @@ -71,8 +82,6 @@
1.58 \rail@cterm{,}[]
1.59 \rail@endplus
1.60 \rail@endbar
1.61 -\rail@nextplus{3}
1.62 -\rail@endplus
1.63 \rail@end
1.64 \rail@begin{1}{default}
1.65 \rail@term{default}[]
1.66 @@ -213,11 +222,36 @@
1.67 \rail@endplus
1.68 \rail@term{)}[]
1.69 \rail@endbar
1.70 -\rail@nont{id}[]
1.71 +\rail@nont{sort}[]
1.72 \rail@end
1.73 -\rail@begin{3}{consts}
1.74 +\rail@begin{2}{consts}
1.75 \rail@term{consts}[]
1.76 \rail@plus
1.77 +\rail@nont{mixfixConstDecl}[]
1.78 +\rail@nextplus{1}
1.79 +\rail@endplus
1.80 +\rail@end
1.81 +\rail@begin{2}{syntax}
1.82 +\rail@term{syntax}[]
1.83 +\rail@bar
1.84 +\rail@nextbar{1}
1.85 +\rail@nont{mode}[]
1.86 +\rail@endbar
1.87 +\rail@plus
1.88 +\rail@nont{mixfixConstDecl}[]
1.89 +\rail@nextplus{1}
1.90 +\rail@endplus
1.91 +\rail@end
1.92 +\rail@begin{2}{mode}
1.93 +\rail@term{(}[]
1.94 +\rail@nont{name}[]
1.95 +\rail@bar
1.96 +\rail@nextbar{1}
1.97 +\rail@term{output}[]
1.98 +\rail@endbar
1.99 +\rail@term{)}[]
1.100 +\rail@end
1.101 +\rail@begin{2}{mixfixConstDecl}
1.102 \rail@nont{constDecl}[]
1.103 \rail@bar
1.104 \rail@nextbar{1}
1.105 @@ -225,8 +259,6 @@
1.106 \rail@nont{mixfix}[]
1.107 \rail@term{)}[]
1.108 \rail@endbar
1.109 -\rail@nextplus{2}
1.110 -\rail@endplus
1.111 \rail@end
1.112 \rail@begin{2}{constDecl}
1.113 \rail@plus
1.114 @@ -241,7 +273,7 @@
1.115 \rail@nont{type}[]
1.116 \rail@endbar
1.117 \rail@end
1.118 -\rail@begin{6}{mixfix}
1.119 +\rail@begin{7}{mixfix}
1.120 \rail@bar
1.121 \rail@nont{string}[]
1.122 \rail@bar
1.123 @@ -259,27 +291,22 @@
1.124 \rail@nont{nat}[]
1.125 \rail@endbar
1.126 \rail@nextbar{4}
1.127 -\rail@nont{infix}[]
1.128 +\rail@bar
1.129 +\rail@term{infixr}[]
1.130 \rail@nextbar{5}
1.131 +\rail@term{infixl}[]
1.132 +\rail@endbar
1.133 +\rail@bar
1.134 +\rail@nextbar{5}
1.135 +\rail@nont{string}[]
1.136 +\rail@endbar
1.137 +\rail@nont{nat}[]
1.138 +\rail@nextbar{6}
1.139 \rail@term{binder}[]
1.140 \rail@nont{string}[]
1.141 \rail@nont{nat}[]
1.142 \rail@endbar
1.143 \rail@end
1.144 -\rail@begin{3}{constdefs}
1.145 -\rail@term{constdefs}[]
1.146 -\rail@plus
1.147 -\rail@nont{id}[]
1.148 -\rail@term{::}[]
1.149 -\rail@bar
1.150 -\rail@nont{string}[]
1.151 -\rail@nextbar{1}
1.152 -\rail@nont{type}[]
1.153 -\rail@endbar
1.154 -\rail@nont{string}[]
1.155 -\rail@nextplus{2}
1.156 -\rail@endplus
1.157 -\rail@end
1.158 \rail@begin{4}{trans}
1.159 \rail@term{translations}[]
1.160 \rail@plus
1.161 @@ -320,6 +347,63 @@
1.162 \rail@nextplus{1}
1.163 \rail@endplus
1.164 \rail@end
1.165 +\rail@begin{3}{constdefs}
1.166 +\rail@term{constdefs}[]
1.167 +\rail@plus
1.168 +\rail@nont{id}[]
1.169 +\rail@term{::}[]
1.170 +\rail@bar
1.171 +\rail@nont{string}[]
1.172 +\rail@nextbar{1}
1.173 +\rail@nont{type}[]
1.174 +\rail@endbar
1.175 +\rail@nont{string}[]
1.176 +\rail@nextplus{2}
1.177 +\rail@endplus
1.178 +\rail@end
1.179 +\rail@begin{3}{axclass}
1.180 +\rail@term{axclass}[]
1.181 +\rail@nont{classDecl}[]
1.182 +\rail@bar
1.183 +\rail@nextbar{1}
1.184 +\rail@plus
1.185 +\rail@nont{id}[]
1.186 +\rail@nont{string}[]
1.187 +\rail@nextplus{2}
1.188 +\rail@endplus
1.189 +\rail@endbar
1.190 +\rail@end
1.191 +\rail@begin{2}{instance}
1.192 +\rail@term{instance}[]
1.193 +\rail@bar
1.194 +\rail@nont{name}[]
1.195 +\rail@term{<}[]
1.196 +\rail@nont{name}[]
1.197 +\rail@nextbar{1}
1.198 +\rail@nont{name}[]
1.199 +\rail@term{::}[]
1.200 +\rail@nont{arity}[]
1.201 +\rail@endbar
1.202 +\rail@nont{witness}[]
1.203 +\rail@end
1.204 +\rail@begin{4}{witness}
1.205 +\rail@bar
1.206 +\rail@nextbar{1}
1.207 +\rail@plus
1.208 +\rail@bar
1.209 +\rail@nont{string}[]
1.210 +\rail@nextbar{2}
1.211 +\rail@nont{longident}[]
1.212 +\rail@endbar
1.213 +\rail@nextplus{3}
1.214 +\rail@cterm{,}[]
1.215 +\rail@endplus
1.216 +\rail@endbar
1.217 +\rail@bar
1.218 +\rail@nextbar{1}
1.219 +\rail@nont{verbatim}[]
1.220 +\rail@endbar
1.221 +\rail@end
1.222 \rail@begin{1}{oracle}
1.223 \rail@term{oracle}[]
1.224 \rail@nont{name}[]