338 |
338 |
339 (* core haskell *) |
339 (* core haskell *) |
340 |
340 |
341 atom_decl var |
341 atom_decl var |
342 atom_decl tvar |
342 atom_decl tvar |
343 atom_decl co |
343 |
344 |
344 |
345 datatype sort = |
345 (* there are types, coercion types and regular types *) |
346 TY tvar |
346 nominal_datatype tkind = |
347 | CO co |
|
348 |
|
349 nominal_datatype kind = |
|
350 KStar |
347 KStar |
351 | KFun kind kind |
348 | KFun "tkind" "tkind" |
352 | KEq kind kind |
349 and ckind = |
353 |
350 CKEq "ty" "ty" |
354 (* there are types, coercion types and regular types *) |
351 and ty = |
355 (* |
352 TVar "tvar" |
356 nominal_datatype ty = |
353 | TC "string" |
357 TVar tvar |
354 | TApp "ty" "ty" |
358 | TFun string "ty list" |
355 | TFun "string" "ty list" |
359 | TAll tvar kind_raw ty --"some binding" |
356 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
360 | TSym ty |
357 | TEq "ty" "ty" "ty" |
361 | TCir ty ty |
358 and co = |
362 | TApp ty ty |
359 CC "string" |
363 | TLeft ty |
360 | CApp "co" "co" |
364 | TRight ty |
361 | CFun "string" "co list" |
365 | TEq ty |
362 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
366 | TRightc ty |
363 | CEq "co" "co" "co" |
367 | TLeftc ty |
364 | CSym "co" |
368 | TCoe ty ty |
365 | CCir "co" "co" |
369 *) |
366 | CLeft "co" |
|
367 | CRight "co" |
|
368 | CSim "co" |
|
369 | CRightc "co" |
|
370 | CLeftc "co" |
|
371 | CCoe "co" "co" |
|
372 |
|
373 |
370 typedecl ty --"hack since ty is not yet defined" |
374 typedecl ty --"hack since ty is not yet defined" |
371 |
375 |
372 abbreviation |
376 abbreviation |
373 "atoms A \<equiv> atom ` A" |
377 "atoms A \<equiv> atom ` A" |
374 |
378 |
375 (* does not work yet |
|
376 nominal_datatype trm = |
379 nominal_datatype trm = |
377 Var var |
380 Var "var" |
378 | LAM tv::tvar kind_raw t::trm bind tv in t |
381 | C "string" |
379 | APP trm ty |
382 | LAM tv::"tvar" "kind" t::"trm" bind tv in t |
380 | Lam v::var ty t::trm bind v in t |
383 | APP "trm" "ty" |
381 | App trm trm |
384 | Lam v::"var" "ty" t::"trm" bind v in t |
382 | Let x::var ty trm t::trm bind x in t |
385 | App "trm" "trm" |
383 | Case trm "assoc list" |
386 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
384 | Cast trm ty --"ty is supposed to be a coercion type only" |
387 | Case "trm" "assoc list" |
|
388 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
385 and assoc = |
389 and assoc = |
386 A p::pat t::trm bind "bv p" in t |
390 A p::"pat" t::"trm" bind "bv p" in t |
387 and pat = |
391 and pat = |
388 K string "(tvar \<times> kind_raw) list" "(var \<times> ty) list" |
392 K "string" "(tvar \<times> kind) list" "(var \<times> ty) list" |
389 binder |
393 binder |
390 bv :: "pat \<Rightarrow> atom set" |
394 bv :: "pat \<Rightarrow> atom set" |
391 where |
395 where |
392 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
396 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
393 *) |
|
394 |
397 |
395 (*thm bv_raw.simps*) |
398 (*thm bv_raw.simps*) |
396 |
399 |
397 (* example 3 from Peter Sewell's bestiary *) |
400 (* example 3 from Peter Sewell's bestiary *) |
398 nominal_datatype exp = |
401 nominal_datatype exp = |