# HG changeset patch # User wenzelm # Date 877102959 -7200 # Node ID 90f499226ab9679e83cbd1ef395aec32e3b584c3 # Parent 7d391943bc19dd8c0c80560bfbeba7d6279c6ae3 (co) inductive / datatype package adapted to qualified names; diff -r 7d391943bc19 -r 90f499226ab9 src/ZF/add_ind_def.ML --- a/src/ZF/add_ind_def.ML Fri Oct 17 17:40:33 1997 +0200 +++ b/src/ZF/add_ind_def.ML Fri Oct 17 17:42:39 1997 +0200 @@ -87,8 +87,9 @@ val rec_names = map (#1 o dest_Const) rec_hds and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); - val dummy = assert_all Syntax.is_identifier rec_names - (fn a => "Name of recursive set not an identifier: " ^ a); + val rec_base_names = map NameSpace.base rec_names; + val dummy = assert_all Syntax.is_identifier rec_base_names + (fn a => "Base name of recursive set not an identifier: " ^ a); local (*Checking the introduction rules*) val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; @@ -147,7 +148,8 @@ (*A key definition: If no mutual recursion then it equals the one recursive set. If mutual recursion then it differs from all the recursive sets. *) - val big_rec_name = space_implode "_" rec_names; + val big_rec_base_name = space_implode "_" rec_base_names; + val big_rec_name = Sign.full_name sign big_rec_base_name; (*Big_rec... is the union of the mutually recursive sets*) val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); @@ -167,30 +169,34 @@ (*Expects the recursive sets to have been defined already. con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) -fun add_constructs_def (rec_names, con_ty_lists) thy = +fun add_constructs_def (rec_base_names, con_ty_lists) thy = let val dummy = (*has essential ancestors?*) - require_thy thy "Datatype" "(co)datatype definitions" + require_thy thy "Datatype" "(co)datatype definitions"; + + val sign = sign_of thy; + val full_name = Sign.full_name sign; val dummy = writeln" Defining the constructor functions..."; val case_name = "f"; (*name for case variables*) + (** Define the constructors **) (*The empty tuple is 0*) fun mk_tuple [] = Const("0",iT) | mk_tuple args = foldr1 (app Pr.pair) args; - fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k; + fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k; - val npart = length rec_names; (*total # of mutually recursive parts*) + val npart = length rec_base_names; (*total # of mutually recursive parts*) (*Make constructor definition; kpart is # of this mutually recursive part*) fun mk_con_defs (kpart, con_ty_list) = let val ncon = length con_ty_list (*number of constructors*) fun mk_def (((id,T,syn), name, args, prems), kcon) = (*kcon is index of constructor*) - mk_defpair (list_comb (Const(name,T), args), + mk_defpair (list_comb (Const (full_name name, T), args), mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args))) in ListPair.map mk_def (con_ty_list, 1 upto ncon) end; @@ -210,45 +216,49 @@ Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) (*Treatment of a single constructor*) - fun add_case (((id,T,syn), name, args, prems), (opno,cases)) = - if Syntax.is_identifier id - then (opno, - (Free(case_name ^ "_" ^ id, T), args) :: cases) - else (opno+1, - (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: - cases) + fun add_case (((_, T, _), name, args, prems), (opno, cases)) = + if Syntax.is_identifier name then + (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases) + else + (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases); (*Treatment of a list of constructors, for one part*) - fun add_case_list (con_ty_list, (opno,case_lists)) = - let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) - in (opno', case_list :: case_lists) end; + fun add_case_list (con_ty_list, (opno, case_lists)) = + let val (opno', case_list) = foldr add_case (con_ty_list, (opno, [])) + in (opno', case_list :: case_lists) end; (*Treatment of all parts*) val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT); - val big_rec_name = space_implode "_" rec_names; - - val big_case_name = big_rec_name ^ "_case"; + val big_rec_base_name = space_implode "_" rec_base_names; + val big_case_base_name = big_rec_base_name ^ "_case"; + val big_case_name = full_name big_case_base_name; (*The list of all the function variables*) val big_case_args = flat (map (map #1) case_lists); - val big_case_tm = - list_comb (Const(big_case_name, big_case_typ), big_case_args); + val big_case_tm = + list_comb (Const (big_case_name, big_case_typ), big_case_args); - val big_case_def = mk_defpair - (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); + val big_case_def = mk_defpair + (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); - (** Build the new theory **) + + (* Build the new theory *) val const_decs = - (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); + (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); val axpairs = - big_case_def :: flat (ListPair.map mk_con_defs - (1 upto npart, con_ty_lists)) + big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)); - in thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs end; + in + thy + |> Theory.add_consts_i const_decs + |> Theory.add_defs_i axpairs + end; + + end; diff -r 7d391943bc19 -r 90f499226ab9 src/ZF/constructor.ML --- a/src/ZF/constructor.ML Fri Oct 17 17:40:33 1997 +0200 +++ b/src/ZF/constructor.ML Fri Oct 17 17:42:39 1997 +0200 @@ -47,9 +47,11 @@ (*Each equation has the form rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = - Ind_Syntax.mk_tprop - (Ind_Syntax.eq_const $ (big_case_tm $ (list_comb (Const(name,T), args))) - $ (list_comb (case_free, args))) ; + Ind_Syntax.mk_tprop + (Ind_Syntax.eq_const $ + (big_case_tm $ + (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T), args))) $ + (list_comb (case_free, args))); val case_trans = hd con_defs RS Ind_Syntax.def_trans and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans; diff -r 7d391943bc19 -r 90f499226ab9 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Fri Oct 17 17:40:33 1997 +0200 +++ b/src/ZF/ind_syntax.ML Fri Oct 17 17:42:39 1997 +0200 @@ -90,14 +90,15 @@ val read_constructs = map o map o read_construct; (*convert constructor specifications into introduction rules*) -fun mk_intr_tms (rec_tm, constructs) = - let fun mk_intr ((id,T,syn), name, args, prems) = - Logic.list_implies - (map mk_tprop prems, - mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) +fun mk_intr_tms sg (rec_tm, constructs) = + let + fun mk_intr ((id,T,syn), name, args, prems) = + Logic.list_implies + (map mk_tprop prems, + mk_tprop (mem_const $ list_comb (Const (Sign.full_name sg name, T), args) $ rec_tm)) in map mk_intr constructs end; -fun mk_all_intr_tms arg = List.concat (ListPair.map mk_intr_tms arg); +fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg); val Un = Const("op Un", [iT,iT]--->iT) and empty = Const("0", iT) diff -r 7d391943bc19 -r 90f499226ab9 src/ZF/indrule.ML --- a/src/ZF/indrule.ML Fri Oct 17 17:40:33 1997 +0200 +++ b/src/ZF/indrule.ML Fri Oct 17 17:42:39 1997 +0200 @@ -25,7 +25,9 @@ val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms); -val big_rec_name = space_implode "_" Intr_elim.rec_names; +val big_rec_name = + Sign.intern_const sign (space_implode "_" (map NameSpace.base Intr_elim.rec_names)); + val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); val _ = writeln " Proving the induction rule..."; @@ -117,7 +119,7 @@ mutual recursion to invariably be a disjoint sum.*) fun mk_predpair rec_tm = let val rec_name = (#1 o dest_Const o head_of) rec_tm - val pfree = Free(pred_name ^ "_" ^ rec_name, + val pfree = Free(pred_name ^ "_" ^ NameSpace.base rec_name, elem_factors ---> Ind_Syntax.oT) val qconcl = foldr Ind_Syntax.mk_all diff -r 7d391943bc19 -r 90f499226ab9 src/ZF/intr_elim.ML --- a/src/ZF/intr_elim.ML Fri Oct 17 17:40:33 1997 +0200 +++ b/src/ZF/intr_elim.ML Fri Oct 17 17:42:39 1997 +0200 @@ -48,16 +48,16 @@ let val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms; -val big_rec_name = space_implode "_" rec_names; +val big_rec_base_name = space_implode "_" (map NameSpace.base rec_names); -val _ = deny (big_rec_name mem map ! (stamps_of_thy Inductive.thy)) - ("Definition " ^ big_rec_name ^ +val _ = deny (big_rec_base_name mem map ! (stamps_of_thy Inductive.thy)) + ("Definition " ^ big_rec_base_name ^ " would clash with the theory of the same name!"); (*fetch fp definitions from the theory*) val big_rec_def::part_rec_defs = map (get_def Inductive.thy) - (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names); + (case rec_names of [_] => rec_names | _ => big_rec_base_name::rec_names); val sign = sign_of Inductive.thy; diff -r 7d391943bc19 -r 90f499226ab9 src/ZF/thy_syntax.ML --- a/src/ZF/thy_syntax.ML Fri Oct 17 17:40:33 1997 +0200 +++ b/src/ZF/thy_syntax.ML Fri Oct 17 17:42:39 1997 +0200 @@ -97,7 +97,7 @@ \ val dom_sum\t= " ^ sdom_sum ^ "\n\ \ and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n" ^ scons ^ "\n\ - \ val intr_tms\t= Ind_Syntax.mk_all_intr_tms (rec_tms, con_ty_lists)\n\ + \ val intr_tms\t= Ind_Syntax.mk_all_intr_tms (sign_of thy) (rec_tms, con_ty_lists)\n\ \ end;\n\n\ \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ mk_list (map quote rec_names) ^ ", " ^ @@ -114,7 +114,7 @@ \ structure Result = " ^ co ^ "Data_section_Fun\n\ \\t (open " ^ stri_name ^ "\n\ \\t val thy\t\t= thy\n\ - \\t val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\ + \\t val big_rec_name\t= Sign.intern_const (sign_of thy) \"" ^ big_rec_name ^ "\"\n\ \\t val monos\t\t= " ^ monos ^ "\n\ \\t val type_intrs\t= " ^ type_intrs ^ "\n\ \\t val type_elims\t= " ^ type_elims ^ ");\n\