nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:a746d49b0240
+:331873ebc5cd
 "../Nominal-General/Nominal2_Eqvt"
 "../Nominal-General/Nominal2_Supp"
 "Perm" "Tacs" "Equivp"
 begin
-(* TODO
-we need to also export a cases-rule for nominal datatypes
-size function
-*)
 section{* Interface for nominal_datatype *}
 ML {*
 (* attributes *)
 fun get_cnstr_strs dts =
 map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))
 fun get_bn_fun_strs bn_funs =
 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
-*}
-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 *}
 aux t
 end
 *}
 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 =
 let
 val (lhs, rhs) = eq
 (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
 (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
 in
 ordered'
 end
-*}
-ML {*
-fun define_raw_dts dts bn_funs bn_eqs binds lthy =
-let
-val thy = ProofContext.theory_of lthy
-val thy_name = Context.theory_name thy
-val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
-val dt_full_names = map (Long_Name.qualify thy_name) dt_names
-val dt_full_names' = add_raws dt_full_names
-val dts_env = dt_full_names ~~ dt_full_names'
-val cnstrs = get_cnstr_strs dts
-val cnstrs_ty = get_typed_cnstrs dts
-val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
-val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name
-(Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
-val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
-val bn_fun_strs = get_bn_fun_strs bn_funs
-val bn_fun_strs' = add_raws bn_fun_strs
-val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
-val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
-(bn_fun_strs ~~ bn_fun_strs')
-val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
-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
-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
 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 = Local_Theory.exit_global lthy
+val thy_name = Context.theory_name thy
+val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+val dt_full_names = map (Long_Name.qualify thy_name) dt_names
+val dt_full_names' = add_raws dt_full_names
+val dts_env = dt_full_names ~~ dt_full_names'
+val cnstrs = get_cnstr_strs dts
+val cnstrs_ty = get_typed_cnstrs dts
+val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
+val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name
+(Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
+val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
+val bn_fun_strs = get_bn_fun_strs bn_funs
+val bn_fun_strs' = add_raws bn_fun_strs
+val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
+val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
+(bn_fun_strs ~~ bn_fun_strs')
+val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
+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, 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 {*
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
 *}
 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";
 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
 if get_STEPS lthy > 0
 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
 val {descr, sorts, ...} = dtinfo
 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
 val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info)
 (* definitions of raw permutations by primitive recursion *)
 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 *)
 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
 val qalpha_bns_descr =
 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
 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) =
 else raise TEST lthy7
 (* 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
 val qbns = map #qconst qbns_info
 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)
 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps)
 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs)
 val _ = warning "Proving respects";
 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
 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9;
 val (fv_rsp_pre, lthy10) = fold_map
 val qalphabn_defs = map #def qalpha_info
 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);
 fun note_simp_suffix s th ctxt =
 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
 val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
 val q_eqvt = map (lift_thm lthy19 qtys []) (raw_bn_eqvt @ raw_fv_eqvt);
 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";
 val lthy21 = Class.instantiation (qty_full_names, [], @{sort fs}) thy3;
 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
 *}
 section {* Preparing and parsing of the specification *}
 ML {*
-(* parsing the datatypes and declaring *)
+(* generates the parsed datatypes and
-(* constructors in the local theory    *)
+declares the constructors
-fun prepare_dts dt_strs lthy =
+*)
-let
+fun prepare_dts dt_strs thy =
-val thy = ProofContext.theory_of lthy
+let
+fun inter_fs_sort thy (a, S) =
-fun mk_type full_tname tvrs =
+(a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S))
-Type (full_tname, map (fn a => TFree (a, @{sort "{pt, fs}"})) tvrs)
+fun mk_type tname sorts (cname, cargs, mx) =
-fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) =
-let
-val tys = map (Syntax.read_typ lthy o snd) anno_tys
-val ty = mk_type full_tname tvs
-in
-((cname, tys ---> ty, mx), (cname, tys, mx))
-end
-fun prep_dt (tvs, tname, mx, cnstrs) =
 let
 val full_tname = Sign.full_name thy tname
-val (cnstrs', cnstrs'') =
+val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts)
-split_list (map (prep_cnstr full_tname tvs) cnstrs)
 in
-(cnstrs', (tvs, tname, mx, cnstrs''))
+(cname, cargs ---> ty, mx)
 end
-val (cnstrs, dts) = split_list (map prep_dt dt_strs)
+fun prep_constr (cname, cargs, mx, _) (constrs, sorts) =
+let
-val _ = tracing ("Contructors:\n" ^ cat_lines (map @{make_string} cnstrs))
+val (cargs', sorts') =
-in
+fold_map (Datatype.read_typ thy) (map snd cargs) sorts
-lthy
+|>> map (map_type_tfree (TFree o inter_fs_sort thy))
-|> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
+in
+(constrs @ [(cname, cargs', mx)], sorts')
+end
+fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =
+let
+val (constrs', sorts') =
+fold prep_constr constrs ([], sorts)
+val constr_trms' =
+map (mk_type tname (rev sorts')) constrs'
+in
+(constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts')
+end
+val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []);
+in
+thy
+|> Sign.add_consts_i constr_trms
 |> pair dts
 end
 *}
 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.exit_global lthy')
-|> Local_Theory.theory (Sign.add_consts_i bn_funs')
+|> Sign.add_consts_i bn_funs'
 |> pair (bn_funs', bn_eqs)
 end
 *}
 text {* associates every SOME with the index in the list; drops NONEs *}
 SOME x => x
 | NONE => error ("Cannot find " ^ x ^ " as argument annotation.");
 *}
 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.")
 fun prep_body env bn_str = index_lookup env bn_str
 val env = indexify annos (* for every label, associate the index *)
 in
 map (prep_bclause env) bclause_strs
 end
 in
-map (map prep_bclauses) annos_bclauses
+(map (map prep_bclauses) annos_bclauses, thy)
 end
 *}
 text {*
 adds an empty binding clause for every argument
 *}
 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
 *}
 map2 (map2 complt) args bclauses
 end
 *}
 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 (pre_typ_names, pre_typs) = split_list
-val lthy0 =
+(map (fn (tvs, tname, mx, _) =>
-Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy
+(Binding.name_of tname, (tname, length tvs, mx))) dt_strs)
-val (dts, lthy1) = prepare_dts dt_strs lthy0
-val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1
+(* this theory is used just for parsing *)
-val bclauses = prepare_bclauses dt_strs lthy2
+val thy = ProofContext.theory_of lthy
-val bclauses' = complete dt_strs bclauses
+val tmp_thy = Theory.copy thy
-in
-timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd)
+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 thm_name dts bn_funs bn_eqs bclauses' lthy |> snd)
 end
 *}
 ML {*
 (* nominal datatype parser *)
 local
 structure P = Parse;
 structure S = Scan
-fun triple1 ((x, y), z) = (x, y, z)
+fun triple ((x, y), z) = (x, y, z)
-fun triple2 (x, (y, z)) = (x, y, z)
+fun tuple1 ((x, y, z), u) = (x, y, z, u)
-fun tuple ((x, y, z), u) = (x, y, z, u)
+fun tuple2 (((x, y), z), u) = (x, y, u, z)
-fun tswap (((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 opt_name = Scan.option (P.binding --| Args.colon)
-val _ = Keyword.keyword "list"
 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.type_args -- P.binding -- P.opt_mixfix >> triple) --
-(P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
+(P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1
 (* binding function parser *)
 val bnfun_parser =
 S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
 (* 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)
 *}

changeset 2431	331873ebc5cd
parent 2430	a746d49b0240
child 2434	92dc6cfa3a95