theory NoneExamples
imports "../NewParser"
begin

atom_decl name


text {* 
  "Weirdo" example from Peter Sewell's bestiary. 

  This example is not covered by our binding 
  specification.

*}

nominal_datatype weird =
  Foo_var "name"
| Foo_pair "weird" "weird" 
| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
    bind x in p1 p2, 
    bind y in p2 p3

(* e1 occurs in two bodies *)

nominal_datatype exp =
  Var name
| Pair exp exp
| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1
and pat =
  PVar name
| PUnit
| PPair pat pat
binder
  bp :: "pat \<Rightarrow> atom list"
where
  "bp (PVar x) = [atom x]"
| "bp (PUnit) = []"
| "bp (PPair p1 p2) = bp p1 @ bp p2"


(* this example binds bound names and
   so is not respectful *)
(*
nominal_datatype trm =
  Vr "name"
| Lm x::"name" t::"trm"         bind x in t
| Lt left::"trm" right::"trm"   bind "bv left" in right
binder
  bv
where
  "bv (Vr n) = {}"
| "bv (Lm n t) = {atom n} \<union> bv t"
| "bv (Lt l r) = bv l \<union> bv r"
*)

(* this example uses "-" in the binding function; 
   at the moment this is unsupported *)
(*
nominal_datatype trm' =
  Vr' "name"
| Lm' l::"name" r::"trm'"   bind l in r
| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r
binder
  bv'
where
  "bv' (Vr' n) = {atom n}"
| "bv' (Lm' n t) = bv' t - {atom n}"
| "bv' (Lt' l r) = bv' l \<union> bv' r"
*)

(* this example again binds bound names  *)
(*
nominal_datatype trm'' =
  Va'' "name"
| Lm'' n::"name" l::"trm''" bind n in l
and bla'' =
  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
binder
  bv''
where
  "bv'' (Vm'' x) = {}"
| "bv'' (Lm'' x b) = {atom x}"
*)

end