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