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