
diff -r 3c32f91fa771 -r 3d54fcc5f41a Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Feb 17 17:51:35 2010 +0100
+++ b/Quot/Nominal/Test.thy	Thu Feb 18 23:07:28 2010 +0100
@@ -5,145 +5,171 @@
 atom_decl name
 
 
-(* test for how to add datatypes *)
+(* tests *)
+ML {*
+Datatype.datatype_cmd;
+Datatype.add_datatype Datatype.default_config;
+
+Primrec.add_primrec_cmd;
+Primrec.add_primrec;
+Primrec.add_primrec_simple;
+*}
+
+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.datatype_cmd
+Datatype.add_datatype Datatype.default_config
   ["foo"]
   [([], @{binding "foo"}, NoSyn, 
-    [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, ["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)
 
-ML{*
-fun filtered_input str = 
-  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 
+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 parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
+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
 *}
 
-(* type plus possible annotation *)
-ML {* 
-val anno_typ =
-  (Scan.option (OuterParse.name --| OuterParse.$$$ "::")) -- OuterParse.typ
+section{* Interface for nominal_datatype *}
+
+text {*
+
+Nominal-Datatype-part:
+
+1st Arg: string list  
+         ^^^^^^^^^^^
+         strings of the types to be defined
+
+2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
+         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+               type(s) to be defined             constructors list
+               (ty args, name, syn)              (name, typs, syn)
+
+Binder-Function-part:
+
+3rd Arg: (binding * typ option * mixfix) list 
+         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    
+            binding function(s)           
+              to be defined               
+            (name, type, syn)             
+
+4th Arg: (attrib * term) list 
+          ^^^^^^^^^^^^^^^^^^^
+          the equations of the binding functions
+          (Trueprop equations)
+
 *}
 
+ML {* Datatype.add_datatype *}
+
 ML {*
-parse (Scan.repeat anno_typ) (filtered_input "x::string bool")
+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 {* OuterParse.enum "," ; OuterParse.and_list1 *}
+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 *)
+local
+  structure P = OuterParse
+in
+
+val _ = OuterKeyword.keyword "bind"
+val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ
 
 (* binding specification *)
-ML {* 
-datatype bind = B of string * string | BS of string * string
- 
-val _ = OuterKeyword.keyword "bind" 
-val _ = OuterKeyword.keyword "bindset" 
-
-val bind_parse_aux =
-    (OuterParse.$$$ "bind" >> (K B)) 
- || (OuterParse.$$$ "bindset" >> (K BS))
-
 (* should use and_list *)
 val bind_parser = 
-  OuterParse.enum ","
-   ((bind_parse_aux -- OuterParse.term) --
-    (OuterParse.$$$ "in" |-- OuterParse.name) >> (fn ((bind, s1), s2) => bind (s1,s2)))
-*}
+  P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
 
 (* datatype parser *)
-ML {*
 val dt_parser =
-  OuterParse.type_args -- OuterParse.binding -- OuterParse.opt_infix -- 
-    (OuterParse.$$$ "=" |-- OuterParse.enum1 "|" 
-       (OuterParse.binding -- (Scan.repeat anno_typ) -- bind_parser -- OuterParse.opt_mixfix))
-*}
+  P.type_args -- P.binding -- P.opt_infix -- 
+    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- (Scan.repeat anno_typ) -- bind_parser -- P.opt_mixfix))
 
 (* function equation parser *)
-ML {*
 val fun_parser = 
-  Scan.optional 
-    ((OuterParse.$$$ "binder") |-- OuterParse.fixes -- SpecParse.where_alt_specs) ([],[])
+  Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
+
+(* main parser *)
+val parser =
+  P.and_list1 dt_parser -- fun_parser
+
+end
 *}
 
-(* main parser *)
-ML {*
-val parser =
-  OuterParse.and_list1 dt_parser -- fun_parser
-*}
 
 (* printing stuff *)
 ML {*
 fun print_str_option NONE = "NONE"
   | print_str_option (SOME s) = (s:bstring)
-*}
 
-ML {*
 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
-*}
 
-ML {*
-fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2
-  | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2
-*}
+fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2
 
-ML {*
 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)))
-*}
 
-(* TODO: replace with the proper thing *)
-ML {*
-fun is_atom ty = ty = "Test.name"
-*}
-
-ML {*
-fun fv_bds s bds set =
-  case bds of
-    [] => set
-  | B (s1, s2) :: tl => 
-      if s2 = s then 
-        fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
-      else fv_bds s tl set
-  | BS (s1, s2) :: tl =>
-    (* TODO: This is just a copy *)
-      if s2 = s then 
-        fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
-      else fv_bds s tl set
-*}
-
-(* TODO: After variant_frees, check that the new names correspond to the ones given by user
-   so that 'bind' is matched with variables correctly *)
-ML {*
-fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) =
-let
-  fun prepare_name (NONE, ty) = ("", ty)
-    | prepare_name (SOME n, ty) = (n, ty);
-  val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys));
-  val var_strs = map (Syntax.string_of_term lthy) vars;
-  fun fv_var (t as Free (s, (ty as Type (tyS, _)))) =
-    if is_atom tyS then HOLogic.mk_set ty [t] else
-    if (Long_Name.base_name tyS) mem dt_names then
-      fv_bds s bds (Free ("rfv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else
-    HOLogic.mk_set @{typ name} []
-  val fv_eq =
-    if null vars then HOLogic.mk_set @{typ name} []
-    else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars)
-  val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq)
-in
-  prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str
-end
-*}
-
-ML {*
-fun single_dt lthy (((s2, s3), syn), constrs) =
+fun print_single_dt lthy (((s2, s3), syn), constrs) =
    ["constructor declaration"]
  @ ["type arguments: "] @ s2 
  @ ["datatype name: ", Binding.name_of s3] 
@@ -151,57 +177,30 @@
  @ ["constructors: "] @ (map (print_constr lthy) constrs)
  |> separate "\n"
  |> implode
-*}
 
-ML {*
-fun fv_dt lthy dt_names (((s2, s3), syn), constrs) =
-    map (fv_constr lthy ("rfv_" ^ Binding.name_of s3) dt_names) constrs
- |> separate "\n"
- |> implode
-*}
-
-ML {* fun single_fun_eq lthy (at, s) = 
+fun print_single_fun_eq lthy (at, s) = 
   ["function equations: ", (Syntax.string_of_term lthy s)] 
   |> separate "\n"
   |> implode
-*}
 
-ML {* fun single_fun_fix (b, _, _) = 
+fun print_single_fun_fix lthy (b, _, _) = 
   ["functions: ", Binding.name_of b] 
   |> separate "\n"
   |> implode
-*}
 
-ML {*
 fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
-*}
 
-ML {*
 fun print_dts (dts, (funs, feqs)) lthy =
 let
-  val _ = warning (implode (separate "\n" (map (single_dt lthy) dts)));
-  val _ = warning (implode (separate "\n" (map single_fun_fix funs)));
-  val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs)));
+  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
 *}
 
 ML {*
-fun fv_dts  (dts, (funs, feqs)) lthy =
-let
-  val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts)));
-in
-  lthy
-end
-*}
-
-ML {*
-parser;
-Datatype.datatype_cmd; 
-*}
-
-ML {*
 fun transp_ty_arg (anno, ty) = ty
 
 fun transp_constr (((constr_name, ty_args), bind), mx) = 
@@ -225,35 +224,39 @@
 fun fn_defn [] [] lthy = lthy
   | fn_defn funs feqs lthy =
       Function_Fun.add_fun Function_Common.default_config funs feqs false lthy
-*}
 
-ML {*
 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 nominal_datatype2_cmd (dts, (funs, feqs)) thy =
+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 parse_dt lthy (((ty_args, ty_name), mx), constrs) =
+   (((ty_args, ty_name), mx), map (parse_constr lthy) constrs);
+*}
+
+ML {*
+fun nominal_datatype2_cmd (dt_strs, (fun_strs, feq_strs)) thy =
 let
-  val thy' = dt_defn (map transp_dt dts) thy
+  val thy' = dt_defn (map transp_dt dt_strs) thy
   val lthy = Theory_Target.init NONE thy'
-  val lthy' = fn_defn_cmd funs feqs lthy
-  fun parse_fun (b, NONE, m) = (b, NONE, m)
-    | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy' ty), m);
-  val funs = map parse_fun funs
-  fun parse_feq (b, t) = (b, Syntax.read_prop lthy' t);
-  val feqs = map parse_feq feqs
-  fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy' ty);
-  fun parse_constr (((constr_name, ty_args), bind), mx) =
-    (((constr_name, map parse_anno_ty ty_args), bind), mx);
-  fun parse_dt (((ty_args, ty_name), mx), constrs) =
-   (((ty_args, ty_name), mx), map parse_constr constrs);
-  val dts = map parse_dt dts
-  val _ = print_dts (dts, (funs, feqs)) lthy
+  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'
 in
-   fv_dts (dts, (funs, feqs)) lthy
-|> Local_Theory.exit_global
+  Local_Theory.exit_global lthy'
 end
 *}
 
@@ -284,7 +287,7 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"        bindset x in t 
+| Lam x::"name" t::"trm"        bind x in t 
 | Let p::"pat" "trm" t::"trm"   bind "f p" in t
 and pat =
   PN
@@ -300,7 +303,7 @@
 nominal_datatype trm2 =
   Var2 "name"
 | App2 "trm2" "trm2"
-| Lam2 x::"name" t::"trm2"          bindset x in t 
+| Lam2 x::"name" t::"trm2"          bind x in t 
 | Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
 and pat2 =
   PN2
@@ -319,7 +322,7 @@
 | Fun "ty" "ty"
 
 nominal_datatype tyS = 
-  All xs::"name list" ty::"ty" bindset xs in ty
+  All xs::"name list" ty::"ty" bind xs in ty
 
 
 




