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}"
print_theorems

text {* examples 2 *}
nominal_datatype trm =
  Var "name"
| 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 "name"
| 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