--- a/Quot/Nominal/Test.thy Sun Feb 21 22:39:11 2010 +0100
+++ b/Quot/Nominal/Test.thy Tue Feb 23 13:32:35 2010 +0100
@@ -17,51 +17,6 @@
section {* test for setting up a primrec on the ML-level *}
-datatype simple = Foo
-
-local_setup {*
-Primrec.add_primrec [(@{binding "Bar"}, SOME @{typ "simple \<Rightarrow> nat"}, NoSyn)]
- [(Attrib.empty_binding, HOLogic.mk_Trueprop @{term "Bar Foo = Suc 0"})] #> snd
-*}
-thm Bar.simps
-
-lemma "Bar Foo = XXX"
-apply(simp)
-oops
-
-section {* test for setting up a datatype on the ML-level *}
-setup {*
-Datatype.add_datatype Datatype.default_config
- ["foo"]
- [([], @{binding "foo"}, NoSyn,
- [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, [Type ("Test.foo", [])], NoSyn)])
- ] #> snd
-*}
-
-ML {*
- PolyML.makestring (#descr (Datatype.the_info @{theory} "Test.foo"))
-*}
-
-thm foo.recs
-thm foo.induct
-
-(* adds "_raw" to the end of constants and types *)
-ML {*
-fun raw_str [] s = s
- | raw_str (s'::ss) s = (if s = s' then s ^ "_str" else raw_str ss s)
-
-val raw_strs = map raw_str
-
-fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts)
- | raw_typ ty_strs T = T
-
-fun raw_term trm_strs ty_strs (Const (a, T)) = Const (raw_str trm_strs a, raw_typ ty_strs T)
- | raw_term trm_strs ty_strs (Abs (a, T, t)) = Abs (a, T, raw_term trm_strs ty_strs t)
- | raw_term trm_strs ty_strs (t $ u) = (raw_term trm_strs ty_strs t) $ (raw_term trm_strs ty_strs u)
-
-fun raw_binding bn = Binding.suffix_name "_raw" bn
-*}
-
section{* Interface for nominal_datatype *}
text {*
@@ -80,48 +35,17 @@
Binder-Function-part:
3rd Arg: (binding * typ option * mixfix) list
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
binding function(s)
to be defined
(name, type, syn)
-4th Arg: (attrib * term) list
- ^^^^^^^^^^^^^^^^^^^
+4th Arg: term list
+ ^^^^^^^^^
the equations of the binding functions
(Trueprop equations)
-
*}
-ML {* Datatype.add_datatype *}
-
-ML {*
-fun raw_definitions dt_names dts bn_funs bn_eqs lthy =
-let
- val conf = Datatype.default_config
- val bn_funs' = map (fn (bn, ty) => (raw_binding bn, ty, NoSyn)) bn_funs
- val bn_eqs' = map (pair Attrib.empty_binding) bn_eqs
-in
- lthy
- |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts))
- ||>> Primrec.add_primrec bn_funs' bn_eqs'
-end
-*}
-
-ML {* @{binding "zero"} *}
-
-local_setup {*
-raw_definitions
- ["foo'"]
- [([], @{binding "foo'"}, NoSyn,
- [(@{binding "zero'"}, [], NoSyn),(@{binding "suc'"}, [Type ("Test.foo'", [])], NoSyn)])]
- [(@{binding "Bar'"}, SOME @{typ "simple \<Rightarrow> nat"})]
- [HOLogic.mk_Trueprop @{term "Bar'_raw Foo = Suc 0"}]
- #> snd
-*}
-
-typ foo'
-thm Bar'.simps
-
text {*****************************************************}
ML {*
(* nominal datatype parser *)
@@ -137,24 +61,111 @@
val bind_parser =
P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
+val constr_parser =
+ P.binding -- Scan.repeat anno_typ
+
(* datatype parser *)
val dt_parser =
- P.type_args -- P.binding -- P.opt_infix --
- (P.$$$ "=" |-- P.enum1 "|" (P.binding -- (Scan.repeat anno_typ) -- bind_parser -- P.opt_mixfix))
+ ((P.type_args -- P.binding -- P.opt_infix) >> P.triple1) --
+ (P.$$$ "=" |-- P.enum1 "|" ((constr_parser -- bind_parser -- P.opt_mixfix) >> P.triple_swap))
(* function equation parser *)
val fun_parser =
Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
(* main parser *)
-val parser =
+val main_parser =
P.and_list1 dt_parser -- fun_parser
end
*}
+(* adds "_raw" to the end of constants and types *)
+ML {*
+fun add_raw s = s ^ "_raw"
+fun raw_bind bn = Binding.suffix_name "_raw" bn
+
+fun raw_str [] s = s
+ | raw_str (s'::ss) s =
+ if (Long_Name.base_name s) = s'
+ then add_raw s
+ else raw_str ss s
+
+fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts)
+ | raw_typ ty_strs T = T
+
+fun raw_aterm trm_strs (Const (a, T)) = Const (raw_str trm_strs a, T)
+ | raw_aterm trm_strs (Free (a, T)) = Free (raw_str trm_strs a, T)
+ | raw_aterm trm_strs trm = trm
+
+fun raw_term trm_strs ty_strs trm =
+ trm |> Term.map_aterms (raw_aterm trm_strs) |> map_types (raw_typ ty_strs)
+
+fun raw_dts ty_strs dts =
+let
+ fun raw_dts_aux1 (bind, tys, mx) =
+ (raw_bind bind, map (raw_typ ty_strs) 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 get_constr_strs dts =
+ flat (map (fn (_, _, _, constrs) => map (fn (bn, _, _) => Binding.name_of bn) constrs) dts)
+
+fun get_bn_fun_strs bn_funs =
+ map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
+*}
+
+ML {*
+fun nominal_dt_decl dt_names dts bn_funs bn_eqs 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
+ 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
+in
+ lthy
+ |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts'))
+ ||>> Primrec.add_primrec bn_funs' bn_eqs'
+end
+*}
+
+local_setup {*
+let
+ val T0 = Type ("Test.foo", [])
+ val T1 = T0 --> @{typ "nat"}
+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)
@@ -328,3 +339,7 @@
end
+
+
+(* probably can be done with a clever morphism trick *)
+