# HG changeset patch # User Cezary Kaliszyk # Date 1266931242 -3600 # Node ID 3b8be8ca46e0a552ffc9fbc7aa134350d12dddb3 # Parent 28aaf6d01e10fe978919da7889c6358c6d65acce# Parent 20f76fde8ef177c7878d1923f54adab2e51ebfac merge diff -r 28aaf6d01e10 -r 3b8be8ca46e0 Quot/Nominal/Test.thy --- a/Quot/Nominal/Test.thy Tue Feb 23 14:19:44 2010 +0100 +++ b/Quot/Nominal/Test.thy Tue Feb 23 14:20:42 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 \ 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 \ 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 *) +