--- a/Quot/Nominal/Test.thy Tue Feb 23 16:12:30 2010 +0100
+++ b/Quot/Nominal/Test.thy Tue Feb 23 16:32:04 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 \<Rightarrow> 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
+*}
+