# HG changeset patch # User Christian Urban # Date 1267205905 -3600 # Node ID 6a133abb7633d87dcfbbeddeff30aa93353e2cb6 # Parent ea46a354f3822cc26ac2a275960c09e72275bd9e generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders" diff -r ea46a354f382 -r 6a133abb7633 Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Feb 26 18:21:39 2010 +0100 +++ b/Nominal/Parser.thy Fri Feb 26 18:38:25 2010 +0100 @@ -31,6 +31,10 @@ (Trueprop equations) *} +ML {* + +*} + text {*****************************************************} ML {* (* nominal datatype parser *) @@ -38,6 +42,7 @@ structure P = OuterParse 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" @@ -46,15 +51,15 @@ (* binding specification *) (* maybe use and_list *) val bind_parser = - P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) + P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name) >> swap) val constr_parser = P.binding -- Scan.repeat anno_typ (* datatype parser *) val dt_parser = - (P.type_args -- P.binding -- P.opt_infix >> P.triple1) -- - (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> P.triple_swap)) >> tuple + (P.type_args -- P.binding -- P.opt_mixfix >> P.triple1) -- + (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> tswap)) >> tuple (* function equation parser *) val fun_parser = @@ -132,6 +137,8 @@ end *} +ML {* Primrec.add_primrec *} + ML {* fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy = let @@ -151,8 +158,8 @@ val bn_fun_strs' = add_raws bn_fun_strs val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' - val bn_funs' = map (fn (bn, opt_ty, mx) => - (raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs + val bn_funs' = map (fn (bn, ty, mx) => + (raw_bind bn, SOME (replace_typ dt_env ty), mx)) bn_funs val bn_eqs' = map (fn trm => (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs @@ -175,8 +182,10 @@ *} ML {* -fun get_constrs2 thy dts = +fun get_constrs2 lthy dts = let + val thy = ProofContext.theory_of lthy + (* makes a full named type out of a binding with tvars applied to it *) fun mk_type thy bind tvrs = Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs) @@ -187,44 +196,104 @@ end *} +ML {* +fun find_all _ [] _ = [] + | find_all eq ((y, z)::xs) x = + if eq (x, y) + then z::find_all eq xs x + else find_all eq xs x +*} + +ML {* +fun mk_env xs = + let + fun mapp (_: int) [] = [] + | mapp i ((a, _) :: xs) = + case a of + NONE => mapp (i + 1) xs + | SOME x => (x, i) :: mapp (i + 1) xs + in mapp 0 xs end + +fun env_lookup xs x = + case AList.lookup (op =) xs x of + SOME x => x + | NONE => error ("cannot find " ^ x ^ " in the binding specification.") +*} + ML {* fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = let - val thy = ProofContext.theory_of lthy - fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx); (* adding the types for parsing datatypes *) - val lthy_tmp = lthy + val lthy_tmp1 = lthy |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) - fun prep_cnstr lthy (((cname, atys), mx), binders) = - (cname, map (Syntax.read_typ lthy o snd) atys, mx) - - fun prep_dt lthy (tvs, tname, mx, cnstrs) = - (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) - (* parsing the datatypes *) - val dts_prep = map (prep_dt lthy_tmp) dt_strs - + val dts_prep = + let + fun prep_cnstr lthy (cname, anno_tys, mx, _) = + (cname, map (Syntax.read_typ lthy o snd) anno_tys, mx) + + fun prep_dt lthy (tvs, tname, mx, cnstrs) = + (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) + in + map (prep_dt lthy_tmp1) dt_strs + end + (* adding constructors for parsing functions *) - val lthy_tmp2 = lthy_tmp - |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 thy dts_prep)) + val lthy_tmp2 = lthy_tmp1 + |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 lthy dts_prep)) - val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2) + (* parsing the function specification *) + val (bn_fun_prep, bn_eq_prep) = + let + val ((bn_fun_aux, bn_eq_aux), _) = Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2 + + fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) + fun prep_bn_eq (attr, t) = t + in + (map prep_bn_fun bn_fun_aux, map prep_bn_eq bn_eq_aux) + end - fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx) - - fun prep_bn_eq (attr, t) = t + (* adding functions for parsing binders *) + val lthy_tmp3 = lthy_tmp2 + |> Local_Theory.theory (Sign.add_consts_i bn_fun_prep) - val bn_fun_prep = map prep_bn_fun bn_fun_aux - val bn_eq_prep = map prep_bn_eq bn_eq_aux + (* parsing the binding structure *) + val binds = + let + fun prep_bn env str = + (case Syntax.read_term lthy_tmp3 str of + Free (x, _) => (env_lookup env x, NONE) + | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T))) + | _ => error (str ^ " not allowed as binding specification.")) + + fun prep_typ env (opt_name, _) = + (case opt_name of + NONE => [] + | SOME x => find_all (op=) env x) + + fun prep_binds (_, anno_tys, _, bind_strs) = + let + val env = mk_env anno_tys + val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs + in + map (prep_typ binds) anno_tys + end + in + map ((map prep_binds) o #4) dt_strs + end + + val _ = tracing (PolyML.makestring binds) in - nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd + nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd end *} (* Command Keyword *) + + ML {* let val kind = OuterKeyword.thy_decl diff -r ea46a354f382 -r 6a133abb7633 Nominal/Term1.thy --- a/Nominal/Term1.thy Fri Feb 26 18:21:39 2010 +0100 +++ b/Nominal/Term1.thy Fri Feb 26 18:38:25 2010 +0100 @@ -39,7 +39,7 @@ alpha_rtrm1 ("_ \1 _" [100, 100] 100) and alpha_bp ("_ \1b _" [100, 100] 100) thm alpha_rtrm1_alpha_bp.intros -thm fv_rtrm1_fv_bp.simps +thm fv_rtrm1_fv_bp.simps[no_vars] local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} thm alpha1_inj diff -r ea46a354f382 -r 6a133abb7633 Nominal/Test.thy --- a/Nominal/Test.thy Fri Feb 26 18:21:39 2010 +0100 +++ b/Nominal/Test.thy Fri Feb 26 18:38:25 2010 +0100 @@ -17,6 +17,8 @@ typ lam_raw term VAR_raw +term APP_raw +term LET_raw term Test.BP_raw thm bi_raw.simps @@ -172,7 +174,7 @@ nominal_datatype foo8 = Foo0 "name" -| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in foo +| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" and bar8 = Bar0 "name" | Bar1 "name" s::"name" b::"bar8" bind s in b @@ -285,7 +287,7 @@ nominal_datatype trm = Var var -| LAM tv::tvar kind t::trm bind v in t +| LAM tv::tvar kind t::trm bind tv in t | APP trm ty | Lam v::var ty t::trm bind v in t | App trm trm