# HG changeset patch # User Christian Urban # Date 1272095363 -7200 # Node ID d33781f9d2c7f0fc78bcde7eadb6ca73ed3b5d17 # Parent 0913f697fe73b6a6c7617aa97d7966573b893d73 merged diff -r 0913f697fe73 -r d33781f9d2c7 Nominal-General/Nominal2_Atoms.thy --- a/Nominal-General/Nominal2_Atoms.thy Fri Apr 23 11:12:38 2010 +0200 +++ b/Nominal-General/Nominal2_Atoms.thy Sat Apr 24 09:49:23 2010 +0200 @@ -126,14 +126,59 @@ apply(simp add: atom_image_cong) done +lemma supp_finite_at_set_aux: + fixes S::"('a::at) set" + assumes a: "finite S" + shows "supp S = atom ` S" +proof + show "supp S \ ((atom::'a::at \ atom) ` S)" + apply(rule supp_is_subset) + apply(simp add: supports_def) + apply(rule allI)+ + apply(rule impI) + apply(rule swap_fresh_fresh) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(rule finite_imageI) + apply(simp add: a) + done +next + have "supp ((atom::'a::at \ atom) ` S) \ supp ((op `) (atom::'a::at \ atom)) \ supp S" + by (simp add: supp_fun_app) + moreover + have "supp ((op `) (atom::'a::at \ atom)) = {}" + apply(rule supp_fun_eqvt) + apply(perm_simp) + apply(simp) + done + moreover + have "supp ((atom::'a::at \ atom) ` S) = ((atom::'a::at \ atom) ` S)" + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + done + ultimately + show "((atom::'a::at \ atom) ` S) \ supp S" by simp +qed + + lemma supp_at_insert: fixes S::"('a::at) set" assumes a: "finite S" shows "supp (insert a S) = supp a \ supp S" - using a - apply (simp add: supp_finite_at_set) - apply (simp add: supp_at_base) - done + using a by (simp add: supp_finite_at_set supp_at_base) + section {* A swapping operation for concrete atoms *} diff -r 0913f697fe73 -r d33781f9d2c7 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Fri Apr 23 11:12:38 2010 +0200 +++ b/Nominal-General/Nominal2_Base.thy Sat Apr 24 09:49:23 2010 +0200 @@ -1081,12 +1081,18 @@ unfolding fresh_def by auto +lemma supp_fun_eqvt: + assumes a: "\p. p \ f = f" + shows "supp f = {}" + unfolding supp_def + using a by simp + + lemma fresh_fun_eqvt_app: assumes a: "\p. p \ f = f" shows "a \ x \ a \ f x" proof - - from a have "supp f = {}" - unfolding supp_def by simp + from a have "supp f = {}" by (simp add: supp_fun_eqvt) then show "a \ x \ a \ f x" unfolding fresh_def using supp_fun_app diff -r 0913f697fe73 -r d33781f9d2c7 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Fri Apr 23 11:12:38 2010 +0200 +++ b/Nominal/Ex/ExPS8.thy Sat Apr 24 09:49:23 2010 +0200 @@ -11,41 +11,41 @@ the reference. *) ML {* val _ = recursive := false *} -nominal_datatype exp8 = +nominal_datatype exp = EVar name | EUnit -| EPair exp8 exp8 -| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *) +| EPair exp exp +| ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *) and fnclause = - K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *) + K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *) and fnclauses = S fnclause | ORs fnclause fnclauses -and lrb8 = +and lrb = Clause fnclauses -and lrbs8 = - Single lrb8 -| More lrb8 lrbs8 -and pat8 = +and lrbs = + Single lrb +| More lrb lrbs +and pat = PVar name | PUnit -| PPair pat8 pat8 +| PPair pat pat binder - b_lrbs8 :: "lrbs8 \ atom set" and - b_pat :: "pat8 \ atom set" and + b_lrbs :: "lrbs \ atom set" and + b_pat :: "pat \ atom set" and b_fnclauses :: "fnclauses \ atom set" and b_fnclause :: "fnclause \ atom set" and - b_lrb8 :: "lrb8 \ atom set" + b_lrb :: "lrb \ atom set" where - "b_lrbs8 (Single l) = b_lrb8 l" -| "b_lrbs8 (More l ls) = b_lrb8 l \ b_lrbs8 ls" + "b_lrbs (Single l) = b_lrb l" +| "b_lrbs (More l ls) = b_lrb l \ b_lrbs ls" | "b_pat (PVar x) = {atom x}" | "b_pat (PUnit) = {}" | "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" | "b_fnclauses (S fc) = (b_fnclause fc)" | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" -| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" -| "b_fnclause (K x pat exp8) = {atom x}" +| "b_lrb (Clause fcs) = (b_fnclauses fcs)" +| "b_fnclause (K x pat exp) = {atom x}" thm exp7_lrb_lrbs.eq_iff thm exp7_lrb_lrbs.supp diff -r 0913f697fe73 -r d33781f9d2c7 Nominal/NewParser.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/NewParser.thy Sat Apr 24 09:49:23 2010 +0200 @@ -0,0 +1,531 @@ +theory NewParser +imports "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Supp" + "Perm" "Equivp" "Rsp" "Lift" +begin + +section{* Interface for nominal_datatype *} + +text {* + +Nominal-Datatype-part: + + +1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + type(s) to be defined constructors list + (ty args, name, syn) (name, typs, syn) + +Binder-Function-part: + +2rd Arg: (binding * typ option * mixfix) list + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + binding function(s) + to be defined + (name, type, syn) + +3th Arg: term list + ^^^^^^^^^ + the equations of the binding functions + (Trueprop equations) +*} + +text {*****************************************************} +ML {* OuterParse.triple2 *} + +ML {* +(* nominal datatype parser *) +local + structure P = OuterParse; + structure S = Scan + + fun triple1 ((x, y), z) = (x, y, z) + fun triple2 (x, (y, z)) = (x, y, z) + fun tuple ((x, y, z), u) = (x, y, z, u) + fun tswap (((x, y), z), u) = (x, y, u, z) +in + +val _ = OuterKeyword.keyword "bind" +val _ = OuterKeyword.keyword "bind_set" +val _ = OuterKeyword.keyword "bind_res" + +val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ + +val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" + +val bind_clauses = + P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) + +val cnstr_parser = + P.binding -- Scan.repeat anno_typ + +(* datatype parser *) +val dt_parser = + (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- + (P.$$$ "=" |-- P.enum1 "|" (cnstr_parser -- bind_clauses -- P.opt_mixfix >> tswap)) >> tuple + +(* binding function parser *) +val bnfun_parser = + Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) + +(* main parser *) +val main_parser = + (P.and_list1 dt_parser) -- bnfun_parser >> triple2 + +end +*} + +ML {* +datatype bmodes = + BEmy of int +| BLst of ((term option * int) list) * (int list) +| BSet of ((term option * int) list) * (int list) +| BRes of ((term option * int) list) * (int list) +*} + +ML {* +fun get_cnstrs dts = + map (fn (_, _, _, constrs) => constrs) dts + +fun get_typed_cnstrs dts = + flat (map (fn (_, bn, _, constrs) => + (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) + +fun get_cnstr_strs dts = + map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) + +fun get_bn_fun_strs bn_funs = + map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs +*} + +ML {* +fun add_primrec_wrapper funs eqs lthy = + if null funs then (([], []), lthy) + else + let + val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs + val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs + in + Primrec.add_primrec funs' eqs' lthy + end +*} + +ML {* +fun add_datatype_wrapper dt_names dts = +let + val conf = Datatype.default_config +in + Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) +end +*} + +ML {* +fun add_raw s = s ^ "_raw" +fun add_raws ss = map add_raw ss +fun raw_bind bn = Binding.suffix_name "_raw" bn + +fun replace_str ss s = + case (AList.lookup (op=) ss s) of + SOME s' => s' + | NONE => s + +fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) + | replace_typ ty_ss T = T + +fun raw_dts ty_ss dts = +let + fun raw_dts_aux1 (bind, tys, mx) = + (raw_bind bind, map (replace_typ ty_ss) tys, mx) + + fun raw_dts_aux2 (ty_args, bind, mx, constrs) = + (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) +in + map raw_dts_aux2 dts +end + +fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) + | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) + | replace_aterm trm_ss trm = trm + +fun replace_term trm_ss ty_ss trm = + trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) +*} + +ML {* +fun rawify_dts dt_names dts dts_env = +let + val raw_dts = raw_dts dts_env dts + val raw_dt_names = add_raws dt_names +in + (raw_dt_names, raw_dts) +end +*} + +ML {* +fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = +let + val bn_funs' = map (fn (bn, ty, mx) => + (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs + + val bn_eqs' = map (fn (attr, trm) => + (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs +in + (bn_funs', bn_eqs') +end +*} + +ML {* +fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses = +let + fun rawify_bnds bnds = + map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds + + fun rawify_bclause (BEmy n) = BEmy n + | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) + | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) + | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) + +in + map (map (map rawify_bclause)) bclauses +end +*} + +text {* What does the prep_bn code do ? *} + +ML {* +fun strip_bn_fun t = + case t of + Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y + | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y + | Const (@{const_name bot}, _) => [] + | Const (@{const_name Nil}, _) => [] + | (f as Free _) $ Bound i => [(i, SOME f)] + | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) +*} + +ML {* +fun find [] _ = error ("cannot find element") + | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y +*} + +ML {* +fun prep_bn dt_names dts eqs = +let + fun aux eq = + let + val (lhs, rhs) = eq + |> strip_qnt_body "all" + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + val (bn_fun, [cnstr]) = strip_comb lhs + val (_, ty) = dest_Free bn_fun + val (ty_name, _) = dest_Type (domain_type ty) + val dt_index = find_index (fn x => x = ty_name) dt_names + val (cnstr_head, cnstr_args) = strip_comb cnstr + val rhs_elements = strip_bn_fun rhs + val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements + in + (dt_index, (bn_fun, (cnstr_head, included))) + end + fun order dts i ts = + let + val dt = nth dts i + val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) + val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts + in + map (find ts') cts + end + + val unordered = AList.group (op=) (map aux eqs) + val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered + val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' +in + ordered +end +*} + + +ML {* +fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = +let + val thy = ProofContext.theory_of lthy + val thy_name = Context.theory_name thy + + val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts + val dt_full_names = map (Long_Name.qualify thy_name) dt_names + val dt_full_names' = add_raws dt_full_names + val dts_env = dt_full_names ~~ dt_full_names' + + val cnstrs = get_cnstr_strs dts + val cnstrs_ty = get_typed_cnstrs dts + val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs + val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name + (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty + val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' + + val bn_fun_strs = get_bn_fun_strs bn_funs + val bn_fun_strs' = add_raws bn_fun_strs + val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' + val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) + (bn_fun_strs ~~ bn_fun_strs') + + val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env + + val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs + + val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds + + val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) + +in + lthy + |> add_datatype_wrapper raw_dt_names raw_dts + ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs + ||>> pair raw_bclauses + ||>> pair raw_bns +end +*} + +ML {* +fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = +let + val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy2) = + raw_nominal_decls dts bn_funs bn_eqs bclauses lthy + +in + ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2) +end +*} + +section {* Preparing and parsing of the specification *} + +ML {* +(* parsing the datatypes and declaring *) +(* constructors in the local theory *) +fun prepare_dts dt_strs lthy = +let + val thy = ProofContext.theory_of lthy + + fun mk_type full_tname tvrs = + Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs) + + fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) = + let + val tys = map (Syntax.read_typ lthy o snd) anno_tys + val ty = mk_type full_tname tvs + in + ((cname, tys ---> ty, mx), (cname, tys, mx)) + end + + fun prep_dt (tvs, tname, mx, cnstrs) = + let + val full_tname = Sign.full_name thy tname + val (cnstrs', cnstrs'') = + split_list (map (prep_cnstr full_tname tvs) cnstrs) + in + (cnstrs', (tvs, tname, mx, cnstrs'')) + end + + val (cnstrs, dts) = split_list (map prep_dt dt_strs) +in + lthy + |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) + |> pair dts +end +*} + +ML {* +(* parsing the binding function specification and *) +(* declaring the functions in the local theory *) +fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = +let + val ((bn_funs, bn_eqs), _) = + Specification.read_spec bn_fun_strs bn_eq_strs lthy + + fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) + + val bn_funs' = map prep_bn_fun bn_funs +in + lthy + |> Local_Theory.theory (Sign.add_consts_i bn_funs') + |> pair (bn_funs', bn_eqs) +end +*} + +text {* associates every SOME with the index in the list; drops NONEs *} +ML {* +fun indexify xs = +let + fun mapp _ [] = [] + | mapp i (NONE :: xs) = mapp (i + 1) xs + | mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs +in + mapp 0 xs +end + +fun index_lookup xs x = + case AList.lookup (op=) xs x of + SOME x => x + | NONE => error ("Cannot find " ^ x ^ " as argument annotation."); +*} + +ML {* +fun prepare_bclauses dt_strs lthy = +let + val annos_bclauses = + get_cnstrs dt_strs + |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) + + fun prep_binder env bn_str = + case (Syntax.read_term lthy bn_str) of + Free (x, _) => (NONE, index_lookup env x) + | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) + | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") + + fun prep_body env bn_str = index_lookup env bn_str + + fun prep_mode "bind" = BLst + | prep_mode "bind_set" = BSet + | prep_mode "bind_res" = BRes + + fun prep_bclause env (mode, binders, bodies) = + let + val binders' = map (prep_binder env) binders + val bodies' = map (prep_body env) bodies + in + prep_mode mode (binders', bodies') + end + + fun prep_bclauses (annos, bclause_strs) = + let + val env = indexify annos (* for every label, associate the index *) + in + map (prep_bclause env) bclause_strs + end +in + map (map prep_bclauses) annos_bclauses +end +*} + +ML {* +fun included i bcs = +let + fun incl (BEmy j) = i = j + | incl (BLst (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) + | incl (BSet (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) + | incl (BRes (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) +in + exists incl bcs +end +*} + +ML {* +fun complete dt_strs bclauses = +let + val args = + get_cnstrs dt_strs + |> map (map (fn (_, antys, _, _) => length antys)) + + fun complt n bcs = + let + fun add bcs i = (if included i bcs then [] else [BEmy i]) + in + bcs @ (flat (map_range (add bcs) n)) + end +in + map2 (map2 complt) args bclauses +end +*} + +ML {* +fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = +let + fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) + + val lthy0 = + Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy + val (dts, lthy1) = + prepare_dts dt_strs lthy0 + val ((bn_funs, bn_eqs), lthy2) = + prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 + val bclauses = prepare_bclauses dt_strs lthy2 + val bclauses' = complete dt_strs bclauses +in + nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd +end + + +(* Command Keyword *) + +val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl + (main_parser >> nominal_datatype2_cmd) + +*} + + + +atom_decl name + +nominal_datatype exp = + EVar name +| EUnit +| EPair q1::exp q2::exp bind_set q1 q2 in q1 q2 +| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l + +and fnclause = + K x::name p::pat f::exp bind_res "b_pat p" in f + +and fnclauses = + S fnclause +| ORs fnclause fnclauses + +and lrb = + Clause fnclauses + +and lrbs = + Single lrb +| More lrb lrbs + +and pat = + PVar name +| PUnit +| PPair pat pat + +binder + b_lrbs :: "lrbs \ atom set" and + b_pat :: "pat \ atom set" and + b_fnclauses :: "fnclauses \ atom set" and + b_fnclause :: "fnclause \ atom set" and + b_lrb :: "lrb \ atom set" + +where + "b_lrbs (Single l) = b_lrb l" +| "b_lrbs (More l ls) = b_lrb l \ b_lrbs ls" +| "b_pat (PVar x) = {atom x}" +| "b_pat (PUnit) = {}" +| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" +| "b_fnclauses (S fc) = (b_fnclause fc)" +| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" +| "b_lrb (Clause fcs) = (b_fnclauses fcs)" +| "b_fnclause (K x pat exp) = {atom x}" + +typ exp_raw +thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] +thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] + +text {* + Why does it take so long to define the nominal + datatype? Is it the function definitions? + +*} + + +end + + + diff -r 0913f697fe73 -r d33781f9d2c7 Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Apr 23 11:12:38 2010 +0200 +++ b/Nominal/Parser.thy Sat Apr 24 09:49:23 2010 +0200 @@ -625,9 +625,14 @@ map_index (prep_typ binds) annos end + val result = map (map (map (map (fn (a, b, c) => + (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) + (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) + + val _ = warning (@{make_string} result) + in - map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) - (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) + result end *} @@ -660,6 +665,51 @@ end *} +atom_decl name + +nominal_datatype exp = + EVar name +| EUnit +| EPair exp exp +| ELetRec l::lrbs e::exp bind "b_lrbs l" in e + +and fnclause = + K x::name p::pat f::exp bind "b_pat p" in f + +and fnclauses = + S fnclause +| ORs fnclause fnclauses + +and lrb = + Clause fnclauses + +and lrbs = + Single lrb +| More lrb lrbs + +and pat = + PVar name +| PUnit +| PPair pat pat + +binder + b_lrbs :: "lrbs \ atom set" and + b_pat :: "pat \ atom set" and + b_fnclauses :: "fnclauses \ atom set" and + b_fnclause :: "fnclause \ atom set" and + b_lrb :: "lrb \ atom set" + +where + "b_lrbs (Single l) = b_lrb l" +| "b_lrbs (More l ls) = b_lrb l \ b_lrbs ls" +| "b_pat (PVar x) = {atom x}" +| "b_pat (PUnit) = {}" +| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" +| "b_fnclauses (S fc) = (b_fnclause fc)" +| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" +| "b_lrb (Clause fcs) = (b_fnclauses fcs)" +| "b_fnclause (K x pat exp) = {atom x}" + end