
diff -r ab942ba2d243 -r 160343d86a6f Quot/Nominal/Test.thy
--- 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 *)
+




