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 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
*}

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)))
*}

ML Local_Theory.exit_global

(* TODO: replace with proper thing *)
ML {*
fun is_atom ty = ty = "name"
*}

ML {* @{term "A \<union> B"} *}

(* TODO: After variant_frees, check that the new names correspond to the ones given by user *)
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 tyS mem dt_names then Free ("fv_" ^ tyS, dummyT) $ t else
    @{term "{}"}
  val fv_eq = 
    if null vars then HOLogic.mk_set @{typ atom} []
    else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars)
  val fv_eq_str = Syntax.string_of_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) =
   ["constructor declaration"]
 @ ["type arguments: "] @ s2 
 @ ["datatype name: ", Binding.name_of s3] 
 @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
 @ ["constructors: "] @ (map (print_constr lthy) constrs)
 |> separate "\n"
 |> implode
*}

ML {*
fun fv_dt lthy dt_names (((s2, s3), syn), constrs) =
    map (fv_constr lthy ("fv_" ^ Binding.name_of s3) dt_names) constrs
 |> separate "\n"
 |> implode
*}

ML {* fun single_fun_eq lthy (at, s) = 
  ["function equations: ", (Syntax.string_of_term lthy s)] 
  |> separate "\n"
  |> implode
*}

ML {* fun single_fun_fix (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 (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) = 
  (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 [] [] lthy = lthy
  | fn_defn funs feqs lthy =
      Function_Fun.add_fun  Function_Common.default_config funs feqs false lthy
*}

ML {*
fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =
let
  val thy' = dt_defn (map transp_dt dts) thy
  val lthy = Theory_Target.init NONE thy'
  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
in
   fn_defn funs feqs lthy
|> print_dts (dts, (funs, feqs))
|> Local_Theory.exit_global
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