
diff -r a746d49b0240 -r 331873ebc5cd Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sun Aug 22 14:02:49 2010 +0800
+++ b/Nominal/NewParser.thy	Wed Aug 25 09:02:06 2010 +0800
@@ -5,11 +5,6 @@
         "Perm" "Tacs" "Equivp"
 begin
 
-(* TODO
-
-  we need to also export a cases-rule for nominal datatypes
-  size function
-*)
 
 section{* Interface for nominal_datatype *}
 
@@ -38,16 +33,6 @@
 *}
 
 
-ML {*
-fun add_datatype_wrapper dt_names dts =
-let
-  val conf = Datatype.default_config
-in
-  Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts)
-end
-*}
-
-
 text {* Infrastructure for adding "_raw" to types and terms *}
 
 ML {*
@@ -141,11 +126,12 @@
 *}
 
 ML {*
+(** definition of the raw binding functions **)
+
+(* TODO: needs cleaning *)
 fun find [] _ = error ("cannot find element")
   | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
-*}
 
-ML {*
 fun prep_bn_info lthy dt_names dts eqs = 
 let
   fun aux eq = 
@@ -182,12 +168,33 @@
 in
   ordered'
 end
+
+
+fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
+  if null raw_bn_funs 
+  then ([], [], [], [], lthy)
+  else 
+    let
+      val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
+        Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+
+      val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1)
+      val {fs, simps, inducts, ...} = info
+
+      val raw_bn_induct = (the inducts)
+      val raw_bn_eqs = the simps
+
+      val raw_bn_info = 
+        prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
+    in
+      (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
+    end
 *}
 
 ML {*
 fun define_raw_dts dts bn_funs bn_eqs binds lthy =
 let
-  val thy = ProofContext.theory_of lthy
+  val thy = Local_Theory.exit_global lthy
   val thy_name = Context.theory_name thy
 
   val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
@@ -212,36 +219,15 @@
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
 
-  val (raw_dt_full_names, lthy1) = 
-    add_datatype_wrapper raw_dt_names raw_dts lthy
+  val (raw_dt_full_names, thy1) = 
+    Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy
+
+  val lthy1 = Named_Target.theory_init thy1
 in
   (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
 end
 *}
 
-ML {*
-(* should be in nominal_dt_rawfuns *)
-fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
-  if null raw_bn_funs 
-  then ([], [], [], [], lthy)
-  else 
-    let
-      val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
-        Function_Common.default_config (pat_completeness_simp constr_thms) lthy
-
-      val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1)
-      val {fs, simps, inducts, ...} = info
-
-      val raw_bn_induct = (the inducts)
-      val raw_bn_eqs = the simps
-
-      val raw_bn_info = 
-        prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
-    in
-      (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
-    end
-*}
-
 
 ML {*
 (* for testing porposes - to exit the procedure early *)
@@ -255,7 +241,7 @@
 setup STEPS_setup
 
 ML {*
-fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
+fun nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes *)
   val _ = warning "Definition of raw datatypes";
@@ -269,7 +255,10 @@
 
   val raw_tys = all_dtyps descr sorts
   val raw_full_ty_names = map (fst o dest_Type) raw_tys
-  
+  val tvs = hd raw_tys
+    |> snd o dest_Type
+    |> map dest_TFree  
+
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names  
  
   val raw_cns_info = all_dtyp_constrs_types descr sorts
@@ -289,7 +278,7 @@
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
     if get_STEPS lthy0 > 1 
-    then define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm lthy0
+    then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
@@ -450,7 +439,7 @@
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
   val qperm_descr =
-    map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs
+    map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
 
   val qsize_descr =
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
@@ -469,12 +458,12 @@
   (* definition of the quotient permfunctions and pt-class *)
   val lthy9 = 
     if get_STEPS lthy > 18
-    then define_qperms qtys qty_full_names qperm_descr raw_perm_laws lthy8 
+    then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 
     else raise TEST lthy8
   
   val lthy9a = 
     if get_STEPS lthy > 19
-    then define_qsizes qtys qty_full_names qsize_descr lthy9
+    then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
   val qconstrs = map #qconst qconstrs_info
@@ -482,10 +471,8 @@
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
   val qalpha_bns = map #qconst qalpha_bns_info
-
   
   (* temporary theorem bindings *)
-
   val (_, lthy9') = lthy9a
      |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
      ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
@@ -515,13 +502,13 @@
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
   val bns = raw_bns ~~ bn_nos;
 
-  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy8;
+  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy9';
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
-       resolve_tac bns_rsp_pre' 1)) bns lthy8;
+       resolve_tac bns_rsp_pre' 1)) bns lthy9';
   val bns_rsp = flat (map snd bns_rsp_pre);
 
-  fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
+  fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy9' 1;
 
   val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
 
@@ -560,12 +547,12 @@
   val _ = warning "Lifting permutations";
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
-  val lthy13 = define_qperms qtys qty_full_names dd raw_perm_laws lthy12c
+  val lthy13 = define_qperms qtys qty_full_names [] dd raw_perm_laws lthy12c
   
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = warning "Lifting induction";
-  val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs;
+  val constr_names = map (Long_Name.base_name o fst o dest_Const) [];
   val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys [] raw_induct_thm);
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
@@ -597,7 +584,7 @@
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = warning "Supports";
-  val supports = map (prove_supports lthy20 q_perm) qconstrs;
+  val supports = map (prove_supports lthy20 q_perm) [];
   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
   val thy3 = Local_Theory.exit_global lthy20;
   val _ = warning "Instantiating FS";
@@ -619,38 +606,46 @@
 section {* Preparing and parsing of the specification *}
 
 ML {* 
-(* parsing the datatypes and declaring *)
-(* constructors in the local theory    *)
-fun prepare_dts dt_strs lthy = 
+(* generates the parsed datatypes and 
+   declares the constructors 
+*)
+fun prepare_dts dt_strs thy = 
 let
-  val thy = ProofContext.theory_of lthy
-  
-  fun mk_type full_tname tvrs =
-    Type (full_tname, map (fn a => TFree (a, @{sort "{pt, fs}"})) tvrs)
+  fun inter_fs_sort thy (a, S) = 
+    (a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S)) 
 
-  fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) =
+  fun mk_type tname sorts (cname, cargs, mx) =
   let
-    val tys = map (Syntax.read_typ lthy o snd) anno_tys
-    val ty = mk_type full_tname tvs
+    val full_tname = Sign.full_name thy tname
+    val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts)
   in
-    ((cname, tys ---> ty, mx), (cname, tys, mx))
+    (cname, cargs ---> ty, mx)
+  end
+
+  fun prep_constr (cname, cargs, mx, _) (constrs, sorts) =
+  let 
+    val (cargs', sorts') = 
+      fold_map (Datatype.read_typ thy) (map snd cargs) sorts
+      |>> map (map_type_tfree (TFree o inter_fs_sort thy)) 
+  in 
+    (constrs @ [(cname, cargs', mx)], sorts') 
   end
   
-  fun prep_dt (tvs, tname, mx, cnstrs) = 
-  let
-    val full_tname = Sign.full_name thy tname
-    val (cnstrs', cnstrs'') = 
-      split_list (map (prep_cnstr full_tname tvs) cnstrs)
-  in
-    (cnstrs', (tvs, tname, mx, cnstrs''))
-  end 
+  fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =
+  let 
+    val (constrs', sorts') = 
+      fold prep_constr constrs ([], sorts)
 
-  val (cnstrs, dts) = split_list (map prep_dt dt_strs)
+    val constr_trms' = 
+      map (mk_type tname (rev sorts')) constrs'
+  in 
+    (constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts') 
+  end
 
-  val _ = tracing ("Contructors:\n" ^ cat_lines (map @{make_string} cnstrs))
+  val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []);
 in
-  lthy
-  |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
+  thy
+  |> Sign.add_consts_i constr_trms
   |> pair dts
 end
 *}
@@ -658,17 +653,19 @@
 ML {*
 (* parsing the binding function specification and *)
 (* declaring the functions in the local theory    *)
-fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
+fun prepare_bn_funs bn_fun_strs bn_eq_strs thy =
 let
-  val ((bn_funs, bn_eqs), _) = 
+  val lthy = Named_Target.theory_init thy
+
+  val ((bn_funs, bn_eqs), lthy') = 
     Specification.read_spec bn_fun_strs bn_eq_strs lthy
 
   fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
   
   val bn_funs' = map prep_bn_fun bn_funs
 in
-  lthy
-  |> Local_Theory.theory (Sign.add_consts_i bn_funs')
+  (Local_Theory.exit_global lthy')
+  |> Sign.add_consts_i bn_funs'
   |> pair (bn_funs', bn_eqs) 
 end 
 *}
@@ -691,14 +688,14 @@
 *}
 
 ML {*
-fun prepare_bclauses dt_strs lthy = 
+fun prepare_bclauses dt_strs thy = 
 let
   val annos_bclauses =
     get_cnstrs dt_strs
     |> map (map (fn (_, antys, _, bns) => (map fst antys, bns)))
 
   fun prep_binder env bn_str =
-    case (Syntax.read_term lthy bn_str) of
+    case (Syntax.read_term_global thy bn_str) of
       Free (x, _) => (NONE, index_lookup env x)
     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
     | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
@@ -720,7 +717,7 @@
     map (prep_bclause env) bclause_strs
   end
 in
-  map (map prep_bclauses) annos_bclauses
+  (map (map prep_bclauses) annos_bclauses, thy)
 end
 *}
 
@@ -732,7 +729,8 @@
 ML {*
 fun included i bcs = 
 let
-  fun incl (BC (_, bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
+  fun incl (BC (_, bns, bds)) = 
+    member (op =) (map snd bns) i orelse member (op =) bds i
 in
   exists incl bcs 
 end
@@ -757,17 +755,28 @@
 *}
 
 ML {*
-fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
+fun nominal_datatype2_cmd (opt_thm_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
 let
-  fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
-  val lthy0 = 
-    Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy
-  val (dts, lthy1) = prepare_dts dt_strs lthy0
-  val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1
-  val bclauses = prepare_bclauses dt_strs lthy2
-  val bclauses' = complete dt_strs bclauses 
+  val (pre_typ_names, pre_typs) = split_list
+    (map (fn (tvs, tname, mx, _) =>
+      (Binding.name_of tname, (tname, length tvs, mx))) dt_strs)
+
+  (* this theory is used just for parsing *)
+  val thy = ProofContext.theory_of lthy  
+  val tmp_thy = Theory.copy thy 
+
+  val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = 
+    tmp_thy
+    |> Sign.add_types pre_typs
+    |> prepare_dts dt_strs 
+    ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 
+    ||>> prepare_bclauses dt_strs 
+
+  val bclauses' = complete dt_strs bclauses
+  val thm_name = 
+    the_default (Binding.name (space_implode "_" pre_typ_names)) opt_thm_name 
 in
-  timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd)
+  timeit (fn () => nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses' lthy |> snd)
 end
 *}
 
@@ -777,33 +786,32 @@
   structure P = Parse;
   structure S = Scan
 
-  fun triple1 ((x, y), z) = (x, y, z)
-  fun triple2 (x, (y, z)) = (x, y, z)
-  fun tuple ((x, y, z), u) = (x, y, z, u)
-  fun tswap (((x, y), z), u) = (x, y, u, z)
+  fun triple ((x, y), z) = (x, y, z)
+  fun tuple1 ((x, y, z), u) = (x, y, z, u)
+  fun tuple2 (((x, y), z), u) = (x, y, u, z)
+  fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
 in
 
 val _ = Keyword.keyword "bind"
-val _ = Keyword.keyword "set"
-val _ = Keyword.keyword "res"
-val _ = Keyword.keyword "list"
+
+val opt_name = Scan.option (P.binding --| Args.colon)
 
 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
 
 val bind_mode = P.$$$ "bind" |--
   S.optional (Args.parens 
-    (P.$$$ "list" >> K Lst || P.$$$ "set" >> K Set || P.$$$ "res" >> K Res)) Lst
+    (Args.$$$ "list" >> K Lst || Args.$$$ "set" >> K Set || Args.$$$ "res" >> K Res)) Lst
 
 val bind_clauses = 
-  P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
+  P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)
 
 val cnstr_parser =
-  P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
+  P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2
 
 (* datatype parser *)
 val dt_parser =
-  (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- 
-    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
+  (P.type_args -- P.binding -- P.opt_mixfix >> triple) -- 
+    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1
 
 (* binding function parser *)
 val bnfun_parser = 
@@ -811,12 +819,11 @@
 
 (* main parser *)
 val main_parser =
-  P.and_list1 dt_parser -- bnfun_parser >> triple2
+  opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3
 
 end
 
 (* Command Keyword *)
-
 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
   (main_parser >> nominal_datatype2_cmd)
 *}




