equal
deleted
inserted
replaced
25 text {* example 2 *} |
25 text {* example 2 *} |
26 |
26 |
27 nominal_datatype trm' = |
27 nominal_datatype trm' = |
28 Var "name" |
28 Var "name" |
29 | App "trm'" "trm'" |
29 | App "trm'" "trm'" |
30 | Lam x::"name" t::"trm'" bind x in t |
30 | Lam x::"name" t::"trm'" bind x in t |
31 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
31 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
32 and pat' = |
32 and pat' = |
33 PN |
33 PN |
34 | PS "name" |
34 | PS "name" |
35 | PD "name" "name" |
35 | PD "name" "name" |
193 bv9 |
193 bv9 |
194 where |
194 where |
195 "bv9 (Var9 x) = {}" |
195 "bv9 (Var9 x) = {}" |
196 | "bv9 (Lam9 x b) = {atom x}" |
196 | "bv9 (Lam9 x b) = {atom x}" |
197 |
197 |
|
198 (* example form Leroy 96 about modules *) |
|
199 |
|
200 nominal_datatype mexp = |
|
201 Acc path |
|
202 | Stru body |
|
203 | Funct x::name sexp m::mexp bind x in m |
|
204 | FApp mexp path |
|
205 | Ascr mexp sexp |
|
206 and body = |
|
207 Empty |
|
208 | Seq c::defn d::body bind "cbinders c" in d |
|
209 and defn = |
|
210 Type name tyty |
|
211 | Dty name |
|
212 | DStru name mexp |
|
213 | Val name trmtrm |
|
214 and sexp = |
|
215 Sig sbody |
|
216 | SFunc name sexp sexp |
|
217 and sbody = |
|
218 SEmpty |
|
219 | SSeq C::spec D::sbody bind "Cbinders C" in D |
|
220 and spec = |
|
221 Type1 name |
|
222 | Type2 name tyty |
|
223 | SStru name sexp |
|
224 | SVal name tyty |
|
225 and tyty = |
|
226 Tyref1 name |
|
227 | Tyref2 path tyty |
|
228 | Fun tyty tyty |
|
229 and path = |
|
230 Sref1 name |
|
231 | Sref2 path name |
|
232 and trmtrm = |
|
233 Tref1 name |
|
234 | Tref2 path name |
|
235 | Lam v::name tyty M::trmtrm bind v in M |
|
236 | App trmtrm trmtrm |
|
237 | Let body trmtrm |
|
238 binder |
|
239 cbinders :: "defn \<Rightarrow> atom set" |
|
240 and Cbinders :: "spec \<Rightarrow> atom set" |
|
241 where |
|
242 "cbinders (Type t T) = {atom t}" |
|
243 | "cbinders (Dty t) = {atom t}" |
|
244 | "cbinders (DStru x s) = {atom x}" |
|
245 | "cbinders (Val v M) = {atom v}" |
|
246 | "Cbinders (Type1 t) = {atom t}" |
|
247 | "Cbinders (Type2 t T) = {atom t}" |
|
248 | "Cbinders (SStru x S) = {atom x}" |
|
249 | "Cbinders (SVal v T) = {atom v}" |
198 |
250 |
199 (* core haskell *) |
251 (* core haskell *) |
200 |
252 |
201 atom_decl var |
253 atom_decl var |
202 atom_decl tvar |
254 atom_decl tvar |