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+ −
+ −
+ −
+ −