# HG changeset patch # User Christian Urban # Date 1266939100 -3600 # Node ID c179ad9d2446874bee3a701a78290ba2d3b48113 # Parent 20f76fde8ef177c7878d1923f54adab2e51ebfac declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types diff -r 20f76fde8ef1 -r c179ad9d2446 Quot/Nominal/Test.thy --- a/Quot/Nominal/Test.thy Tue Feb 23 13:33:01 2010 +0100 +++ b/Quot/Nominal/Test.thy Tue Feb 23 16:31:40 2010 +0100 @@ -75,7 +75,7 @@ (* main parser *) val main_parser = - P.and_list1 dt_parser -- fun_parser + (P.and_list1 dt_parser) -- fun_parser end *} @@ -120,154 +120,68 @@ *} ML {* -fun nominal_dt_decl dt_names dts bn_funs bn_eqs lthy = +fun raw_dts_decl dt_names dts lthy = let val conf = Datatype.default_config - + val dt_names' = map add_raw dt_names val dts' = raw_dts dt_names dts - val constr_strs = get_constr_strs dts +in + Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts') lthy +end +*} + +ML {* +fun raw_bn_fun_decl dt_names cnstr_names bn_funs bn_eqs lthy = +let val bn_fun_strs = get_bn_fun_strs bn_funs val bn_funs' = map (fn (bn, opt_ty, mx) => (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs val bn_eqs' = map (fn trm => - (Attrib.empty_binding, raw_term (constr_strs @ bn_fun_strs) dt_names trm)) bn_eqs + (Attrib.empty_binding, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs in - lthy - |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')) - ||>> Primrec.add_primrec bn_funs' bn_eqs' + (*Primrec.add_primrec bn_funs' bn_eqs' lthy*) + ((), lthy) end *} -local_setup {* +ML {* +fun nominal_datatype2 dts bn_funs bn_eqs lthy = let - val T0 = Type ("Test.foo", []) - val T1 = T0 --> @{typ "nat"} + val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts + val ctrs_names = get_constr_strs dts in -nominal_dt_decl - ["foo"] - [([], @{binding "foo"}, NoSyn, - [(@{binding "myzero"}, [], NoSyn),(@{binding "mysuc"}, [Type ("Test.foo", [])], NoSyn)])] - [(@{binding "Bar"}, SOME T1, NoSyn)] - [HOLogic.mk_Trueprop (HOLogic.mk_eq - (Free ("Bar", T1) $ Const ("Test.foo_raw.myzero", T0), @{term "0::nat"})), - HOLogic.mk_Trueprop (HOLogic.mk_eq - (Free ("Bar", T1) $ (Const ("Test.foo_raw.mysuc", T0 --> T0) $ Free ("n", T0)), @{term "0::nat"}))] - #> snd -end -*} - -typ foo_raw -thm foo_raw.induct -term myzero_raw -term mysuc_raw -thm Bar_raw.simps - -(* printing stuff *) - -ML {* -fun print_str_option NONE = "NONE" - | print_str_option (SOME s) = (s:bstring) - -fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty - | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty - -fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2 - -fun print_constr lthy (((name, anno_tys), bds), syn) = - (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " - ^ (commas (map print_bind bds)) ^ " " - ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) - -fun print_single_dt lthy (((s2, s3), syn), constrs) = - ["constructor declaration"] - @ ["type arguments: "] @ s2 - @ ["datatype name: ", Binding.name_of s3] - @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)] - @ ["constructors: "] @ (map (print_constr lthy) constrs) - |> separate "\n" - |> implode - -fun print_single_fun_eq lthy (at, s) = - ["function equations: ", (Syntax.string_of_term lthy s)] - |> separate "\n" - |> implode - -fun print_single_fun_fix lthy (b, _, _) = - ["functions: ", Binding.name_of b] - |> separate "\n" - |> implode - -fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3 - -fun print_dts (dts, (funs, feqs)) lthy = -let - val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts))); - val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs))); - val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs))); -in - () + lthy + |> raw_dts_decl dts_names dts + ||>> raw_bn_fun_decl dts_names ctrs_names bn_funs bn_eqs end *} ML {* -fun transp_ty_arg (anno, ty) = ty - -fun transp_constr (((constr_name, ty_args), bind), mx) = - (constr_name, map transp_ty_arg ty_args, mx) - -fun transp_dt (((ty_args, ty_name), mx), constrs) = - (ty_args, ty_name, mx, map transp_constr constrs) -*} - -ML {* -fun dt_defn dts thy = +fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy = let - val names = map (fn (_, s, _, _) => Binding.name_of s) dts - val thy' = Datatype.datatype_cmd names dts thy -in - thy' -end -*} - -ML {* -fun fn_defn [] [] lthy = lthy - | fn_defn funs feqs lthy = - Function_Fun.add_fun Function_Common.default_config funs feqs false lthy + val lthy_tmp = lthy + |> (Local_Theory.theory + (Sign.add_types (map (fn ((tvs, tname, mx), _) => + (tname, length tvs, mx)) dt_strs))) -fun fn_defn_cmd [] [] lthy = lthy - | fn_defn_cmd funs feqs lthy = - Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy -*} - -ML {* -fun parse_fun lthy (b, NONE, m) = (b, NONE, m) - | parse_fun lthy (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m) - -fun parse_feq lthy (b, t) = (b, Syntax.read_prop lthy t); - -fun parse_anno_ty lthy (anno, ty) = (anno, Syntax.read_typ lthy ty); - -fun parse_constr lthy (((constr_name, ty_args), bind), mx) = - (((constr_name, map (parse_anno_ty lthy) ty_args), bind), mx); + fun prep_cnstr lthy (((cname, atys), mx), binders) = + (cname, map (Syntax.read_typ lthy o snd) atys, mx) -fun parse_dt lthy (((ty_args, ty_name), mx), constrs) = - (((ty_args, ty_name), mx), map (parse_constr lthy) constrs); -*} + fun prep_dt lthy ((tvs, tname, mx), cnstrs) = + (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) + + fun prep_bn_fun lthy (bn, ty_str, mx) = + (bn, Option.map (Syntax.read_typ lthy) ty_str, mx) -ML {* -fun nominal_datatype2_cmd (dt_strs, (fun_strs, feq_strs)) thy = -let - val thy' = dt_defn (map transp_dt dt_strs) thy - val lthy = Theory_Target.init NONE thy' - val lthy' = fn_defn_cmd fun_strs feq_strs lthy - val funs = map (parse_fun lthy') fun_strs - val feqs = map (parse_feq lthy') feq_strs - val dts = map (parse_dt lthy') dt_strs - val _ = print_dts (dts, (funs, feqs)) lthy' + fun prep_bn_eq lthy (attr, trm_str) = Syntax.read_term lthy trm_str + + val dts_prep = map (prep_dt lthy_tmp) dt_strs + val bn_fun_prep = map (prep_bn_fun lthy_tmp) bn_fun_strs + val bn_eq_prep = map (prep_bn_eq lthy_tmp) bn_eq_strs in - Local_Theory.exit_global lthy' + nominal_datatype2 dts_prep bn_fun_prep [] lthy |> snd end *} @@ -276,8 +190,8 @@ let val kind = OuterKeyword.thy_decl in - OuterSyntax.command "nominal_datatype" "test" kind - (parser >> (Toplevel.theory o nominal_datatype2_cmd)) + OuterSyntax.local_theory "nominal_datatype" "test" kind + (main_parser >> nominal_datatype2_cmd) end *} @@ -292,6 +206,11 @@ bi::"bp \ name set" where "bi (BP x t) = {x}" + +typ lam_raw +term VAR_raw +term BP_raw + print_theorems text {* examples 2 *} @@ -341,5 +260,50 @@ end -(* probably can be done with a clever morphism trick *) +(* printing stuff *) + +ML {* +fun print_str_option NONE = "NONE" + | print_str_option (SOME s) = (s:bstring) + +fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty + | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty + +fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2 + +fun print_constr lthy (((name, anno_tys), bds), syn) = + (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " + ^ (commas (map print_bind bds)) ^ " " + ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) +fun print_single_dt lthy (((s2, s3), syn), constrs) = + ["constructor declaration"] + @ ["type arguments: "] @ s2 + @ ["datatype name: ", Binding.name_of s3] + @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)] + @ ["constructors: "] @ (map (print_constr lthy) constrs) + |> separate "\n" + |> implode + +fun print_single_fun_eq lthy (at, s) = + ["function equations: ", (Syntax.string_of_term lthy s)] + |> separate "\n" + |> implode + +fun print_single_fun_fix lthy (b, _, _) = + ["functions: ", Binding.name_of b] + |> separate "\n" + |> implode + +fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3 + +fun print_dts (dts, (funs, feqs)) lthy = +let + val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts))); + val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs))); + val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs))); +in + () +end +*} +