214 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in 1, bind c in t |
214 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in 1, bind c in t |
215 |
215 |
216 (* example form Leroy 96 about modules; OTT *) |
216 (* example form Leroy 96 about modules; OTT *) |
217 |
217 |
218 nominal_datatype mexp = |
218 nominal_datatype mexp = |
219 Acc path |
219 Acc "path" |
220 | Stru body |
220 | Stru "body" |
221 | Funct x::name sexp m::mexp bind x in m |
221 | Funct x::"name" "sexp" m::"mexp" bind x in m |
222 | FApp mexp path |
222 | FApp "mexp" "path" |
223 | Ascr mexp sexp |
223 | Ascr "mexp" "sexp" |
224 and body = |
224 and body = |
225 Empty |
225 Empty |
226 | Seq c::defn d::body bind "cbinders c" in d |
226 | Seq c::defn d::"body" bind "cbinders c" in d |
227 and defn = |
227 and defn = |
228 Type name tyty |
228 Type "name" "tyty" |
229 | Dty name |
229 | Dty "name" |
230 | DStru name mexp |
230 | DStru "name" "mexp" |
231 | Val name trmtrm |
231 | Val "name" "trmtrm" |
232 and sexp = |
232 and sexp = |
233 Sig sbody |
233 Sig sbody |
234 | SFunc name sexp sexp |
234 | SFunc "name" "sexp" "sexp" |
235 and sbody = |
235 and sbody = |
236 SEmpty |
236 SEmpty |
237 | SSeq C::spec D::sbody bind "Cbinders C" in D |
237 | SSeq C::spec D::sbody bind "Cbinders C" in D |
238 and spec = |
238 and spec = |
239 Type1 name |
239 Type1 "name" |
240 | Type2 name tyty |
240 | Type2 "name" "tyty" |
241 | SStru name sexp |
241 | SStru "name" "sexp" |
242 | SVal name tyty |
242 | SVal "name" "tyty" |
243 and tyty = |
243 and tyty = |
244 Tyref1 name |
244 Tyref1 "name" |
245 | Tyref2 path tyty |
245 | Tyref2 "path" "tyty" |
246 | Fun tyty tyty |
246 | Fun "tyty" "tyty" |
247 and path = |
247 and path = |
248 Sref1 name |
248 Sref1 "name" |
249 | Sref2 path name |
249 | Sref2 "path" "name" |
250 and trmtrm = |
250 and trmtrm = |
251 Tref1 name |
251 Tref1 "name" |
252 | Tref2 path name |
252 | Tref2 "path" "name" |
253 | Lam v::name tyty M::trmtrm bind v in M |
253 | Lam v::"name" "tyty" M::"trmtrm" bind v in M |
254 | App trmtrm trmtrm |
254 | App "trmtrm" "trmtrm" |
255 | Let body trmtrm |
255 | Let "body" "trmtrm" |
256 binder |
256 binder |
257 cbinders :: "defn \<Rightarrow> atom set" |
257 cbinders :: "defn \<Rightarrow> atom set" |
258 and Cbinders :: "spec \<Rightarrow> atom set" |
258 and Cbinders :: "spec \<Rightarrow> atom set" |
259 where |
259 where |
260 "cbinders (Type t T) = {atom t}" |
260 "cbinders (Type t T) = {atom t}" |