theory TypeVarsTest

imports "../Nominal2" 

begin

atom_decl var

ML {* trace := true *}

declare [[ML_print_depth = 1000]]

nominal_datatype exp =

          Var var

        | App exp var

        | LetA as::assn body::exp binds "bn as" in "body" "as"

        | Lam x::var body::exp binds x in body

        and assn =

          ANil | ACons var exp assn

        binder

          bn

        where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"

(* NEEDS FIXING

nominal_datatype ('ann::fs) exp2 =

  Var2 var

| App2 "'ann exp2" var

| LetA2 as::"'ann assn2" body::"'ann exp2" binds "bn2 as" in body as

| Lam2 x::var body::"'ann exp2" binds x in body

and ('ann::fs) assn2 =

  ANil2 

| ACons2 var "'ann exp2" 'ann "'ann assn2"

binder

  bn2 :: "('ann::fs) assn2 \<Rightarrow> atom list"

where 

  "bn2 ANil2 = []" 

| "bn2 (ACons2 x a t as) = (atom x) # (bn2 as)"

*)

(* a nominal datatype with type variables and sorts *)

(* the sort constraints need to be attached to the  *)

(* first occurence of the type variables on the     *)

(* right-hand side                                  *)

atom_decl name

class s1

class s2

instance nat :: s1 ..

instance int :: s2 .. 

nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =

  Var3 "name"

| App3 "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"

| Lam3 x::"name" l::"('a, 'b, 'c) lam"  binds x in l

| Foo3 "'a" "'b"

| Bar3 x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)

term Foo

term Bar

thm lam.supp lam.fresh

thm lam.distinct

thm lam.induct

thm lam.exhaust 

thm lam.strong_exhaust

thm lam.fv_defs

thm lam.bn_defs

thm lam.perm_simps

thm lam.eq_iff

thm lam.fv_bn_eqvt

thm lam.size_eqvt

nominal_datatype ('alpha, 'beta, 'gamma) psi =

  PsiNil

| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 

thm psi.supp psi.fresh

nominal_datatype 'a foo = 

  Node x::"name" f::"'a foo" binds x in f

| Leaf "'a"

term "Leaf"

end