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