--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 11:48:04 2010 +0100
@@ -0,0 +1,251 @@
+theory Test
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp"
+begin
+
+atom_decl name
+
+
+(* test for how to add datatypes *)
+setup {*
+Datatype.datatype_cmd
+  ["foo"]
+  [([], @{binding "foo"}, NoSyn, 
+    [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, ["foo"], NoSyn)])
+  ]
+*}
+
+thm foo.recs
+thm foo.induct
+
+
+ML{*
+fun filtered_input str = 
+  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 
+
+fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
+*}
+
+(* type plus possible annotation *)
+ML {* 
+val anno_typ =
+  (Scan.option (OuterParse.name --| OuterParse.$$$ "::")) -- OuterParse.typ
+*}
+
+ML {*
+parse (Scan.repeat anno_typ) (filtered_input "x::string bool")
+*}
+
+ML {* OuterParse.enum "," ; OuterParse.and_list1 *}
+
+(* 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)))
+*}
+
+(* 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))
+*}
+
+(* function equation parser *)
+ML {*
+val fun_parser = 
+  Scan.optional 
+    ((OuterParse.$$$ "binder") |-- OuterParse.fixes -- SpecParse.where_alt_specs) ([],[])
+*}
+
+(* 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 (NONE, ty) = ty
+  | print_anno_typ (SOME x, ty) = x ^ ":" ^ ty     
+*}
+
+ML {*
+fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2
+  | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2
+*}
+
+ML {*
+fun print_constr (((name, anno_tys), bds), syn) =
+  (Binding.name_of name ^ " of " ^ (commas (map print_anno_typ anno_tys)) ^ "   " 
+   ^ (commas (map print_bind bds)) ^ "  "  
+   ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
+*}
+
+ML {*
+fun single_dt (((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 constrs)
+ |> separate "\n"
+ |> implode
+*}
+
+ML {* fun single_fun_eq (at, s) = 
+  ["function equations: ", s] 
+  |> separate "\n"
+  |> implode
+*}
+
+ML {* fun single_fun_fix (b, _, _) = 
+  ["functions: ", Binding.name_of b] 
+  |> separate "\n"
+  |> implode
+*}
+
+ML {*
+fun print_dts (dts, (funs, feqs)) = 
+let
+   val _ = warning (implode (separate "\n" (map single_dt dts)))
+   val _ = warning (implode (separate "\n" (map single_fun_fix funs)))
+   val _ = warning (implode (separate "\n" (map single_fun_eq feqs)))
+in
+  ()
+end   
+*}
+
+ML {*
+parser;
+Datatype.datatype_cmd; 
+*}
+
+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 =
+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 [] [] thy = thy
+  | fn_defn funs feqs thy =
+let
+  val lthy = Theory_Target.init NONE thy
+  val ctxt = Function_Fun.add_fun_cmd  Function_Common.default_config funs feqs false lthy
+  val thy' = ProofContext.theory_of ctxt
+in
+  thy'
+end
+*}
+
+
+ML {*
+fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =
+let
+  val thy1 = dt_defn (map transp_dt dts) thy
+  val thy2 = fn_defn funs feqs thy1
+  val _ = print_dts (dts, (funs, feqs)) 
+in
+  thy2
+end *}
+
+(* Command Keyword *)
+ML {*
+let
+   val kind = OuterKeyword.thy_decl
+in
+   OuterSyntax.command "nominal_datatype" "test" kind 
+     (parser >> (Toplevel.theory o nominal_datatype2_cmd))
+end
+*}
+
+text {* example 1 *}
+nominal_datatype lam =
+  VAR "name"
+| APP "lam" "lam"
+| LET bp::"bp" t::"lam"   bind "bi bp" in t ("Let _ in _" [100,100] 100)
+and bp = 
+  BP "name" "lam"  ("_ ::= _" [100,100] 100)
+binder
+  bi::"bp \<Rightarrow> name set"
+where
+  "bi (BP x t) = {x}"
+
+
+text {* examples 2 *}
+nominal_datatype trm =
+  Var "string"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"        bindset x in t 
+| Let p::"pat" "trm" t::"trm"   bind "f p" in t
+and pat =
+  PN
+| PS "name"
+| PD "name \<times> name"
+binder
+  f::"pat \<Rightarrow> name set"
+where 
+  "f PN = {}"
+| "f (PS x) = {x}"
+| "f (PD (x,y)) = {x,y}"
+
+nominal_datatype trm2 =
+  Var2 "string"
+| App2 "trm2" "trm2"
+| Lam2 x::"name" t::"trm2"          bindset x in t 
+| Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
+and pat2 =
+  PN2
+| PS2 "name"
+| PD2 "pat2 \<times> pat2"
+binder
+  f2::"pat2 \<Rightarrow> name set"
+where 
+  "f2 PN2 = {}"
+| "f2 (PS2 x) = {x}"
+| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)"
+
+text {* example type schemes *}
+datatype ty = 
+  Var "name" 
+| Fun "ty" "ty"
+
+nominal_datatype tyS = 
+  All xs::"name list" ty::"ty" bindset xs in ty
+
+
+
+
+end
\ No newline at end of file