# HG changeset patch # User wenzelm # Date 877338895 -7200 # Node ID ae9c61d6988869d3854f5f77ec99d774f598b873 # Parent 8988ba66c62b832a6a526337035d2038c2335a4c adapted to qualified names; diff -r 8988ba66c62b -r ae9c61d69888 src/HOL/TLA/Action.ML --- a/src/HOL/TLA/Action.ML Mon Oct 20 11:14:16 1997 +0200 +++ b/src/HOL/TLA/Action.ML Mon Oct 20 11:14:55 1997 +0200 @@ -51,7 +51,7 @@ *) fun maybe_unlift th = (case concl_of th of - Const("TrueInt",_) $ p + Const("Intensional.TrueInt",_) $ p => (action_unlift th handle _ => int_unlift th) | _ => th); diff -r 8988ba66c62b -r ae9c61d69888 src/HOL/TLA/Intensional.ML --- a/src/HOL/TLA/Intensional.ML Mon Oct 20 11:14:16 1997 +0200 +++ b/src/HOL/TLA/Intensional.ML Mon Oct 20 11:14:55 1997 +0200 @@ -86,7 +86,7 @@ *) fun maybe_unlift th = (case concl_of th of - Const("TrueInt",_) $ p => int_unlift th + Const("Intensional.TrueInt",_) $ p => int_unlift th | _ => th); simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift); diff -r 8988ba66c62b -r ae9c61d69888 src/HOL/TLA/ROOT.ML --- a/src/HOL/TLA/ROOT.ML Mon Oct 20 11:14:16 1997 +0200 +++ b/src/HOL/TLA/ROOT.ML Mon Oct 20 11:14:55 1997 +0200 @@ -12,6 +12,8 @@ *) Syntax.ambiguity_level := 10000; +reset global_names; + use_thy "TLA"; val TLA_build_completed = (); diff -r 8988ba66c62b -r ae9c61d69888 src/HOL/TLA/hypsubst.ML --- a/src/HOL/TLA/hypsubst.ML Mon Oct 20 11:14:16 1997 +0200 +++ b/src/HOL/TLA/hypsubst.ML Mon Oct 20 11:14:55 1997 +0200 @@ -88,7 +88,7 @@ Is type ty the type of a state variable? Only then do we substitute in applications. This function either returns true or raises Match. *) -fun is_stvar (Type("fun", Type("state",[])::_)) = true; +fun is_stvar (Type("fun", Type("Stfun.state",[])::_)) = true; (*If novars then we forbid Vars in the equality. diff -r 8988ba66c62b -r ae9c61d69888 src/HOL/add_ind_def.ML --- a/src/HOL/add_ind_def.ML Mon Oct 20 11:14:16 1997 +0200 +++ b/src/HOL/add_ind_def.ML Mon Oct 20 11:14:55 1997 +0200 @@ -68,8 +68,9 @@ val rec_names = map (#1 o dest_Const) rec_hds and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); - val _ = assert_all Syntax.is_identifier rec_names - (fn a => "Name of recursive set not an identifier: " ^ a); + val rec_base_names = map Sign.base_name rec_names; + val _ = 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; @@ -136,7 +137,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); @@ -160,86 +162,4 @@ in thy |> Theory.add_defs_i axpairs end -(****************************************************************OMITTED - -(*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 = -* let -* val _ = 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 mk_Pair args; - -* fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k; - -* val npart = length rec_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_inject npart kpart - (mk_inject ncon kcon (mk_tuple args))) -* in ListPair.map mk_def (con_ty_list, (1 upto ncon)) end; - -* (** Define the case operator **) - -* (*Combine split terms using case; yields the case operator for one part*) -* fun call_case case_list = -* let fun call_f (free,args) = - ap_split T free (map (#2 o dest_Free) args) -* in fold_bal (app sum_case) (map call_f case_list) end; - -* (** Generating function variables for the case definition - 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) - -* (*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; - -* (*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"; - -* (*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_def = mk_defpair - (big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); - -* (** Build the new theory **) - -* val const_decs = - (big_case_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)) - -* in thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs end; -****************************************************************) end; diff -r 8988ba66c62b -r ae9c61d69888 src/HOL/datatype.ML --- a/src/HOL/datatype.ML Mon Oct 20 11:14:16 1997 +0200 +++ b/src/HOL/datatype.ML Mon Oct 20 11:14:55 1997 +0200 @@ -4,8 +4,6 @@ Konrad Slind Copyright 1995 TU Muenchen -TODO: - - handle internal / external names *) (** Information about datatypes **) @@ -129,7 +127,7 @@ | subst (funct $ body) = let val (f,b) = strip_comb (funct$body) in - if is_Const f andalso fst(dest_Const f) = fname + if is_Const f andalso Sign.base_name (fst(dest_Const f)) = fname then let val (ls,rest) = (take(rpos,b), drop(rpos,b)); val (xk,rs) = (hd rest,tl rest) @@ -181,9 +179,9 @@ raise RecError "more than one non-variable in pattern" else if not(null(findrep (map fst (ls @ rs @ cargs)))) then raise RecError "repeated variable name in pattern" - else (fst(dest_Const name) handle TERM _ => + else (Sign.base_name (fst(dest_Const name)) handle TERM _ => raise RecError "function is not declared as constant in theory" - ,rpos,ls,fst( dest_Const c),cargs,rs,rhs) + ,rpos,ls, Sign.base_name (fst(dest_Const c)),cargs,rs,rhs) end; (* check function specified for all constructors and sort function terms *) @@ -506,7 +504,7 @@ Logic.mk_equals (Const(fname,dummyT), rhs)) val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair; val varT = Type.varifyT T; - val ftyp = the (Sign.const_type sg fname); + val ftyp = the (Sign.const_type sg (Sign.intern_const sg fname)); in Theory.add_defs_i [defpairT] thy end; in @@ -962,7 +960,10 @@ in fun build_record (thy,(ty,cl),itac) = let val sign = sign_of thy - fun const s = Const(s, the(Sign.const_type sign s)) + val intern_const = Sign.intern_const sign; + fun const s = + let val s' = intern_const s + in Const(s', the (Sign.const_type sign s')) end val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl val {nchotomy,case_cong} = case_thms sign case_rewrites itac val exhaustion = mk_exhaust nchotomy diff -r 8988ba66c62b -r ae9c61d69888 src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Mon Oct 20 11:14:16 1997 +0200 +++ b/src/HOL/thy_syntax.ML Mon Oct 20 11:14:55 1997 +0200 @@ -143,7 +143,8 @@ \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\ \end;\n\ \val dummy = datatypes := Dtype.build_record (thy, " ^ - mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^ + mk_pair ("Sign.intern_tycon (sign_of thy) " ^ quote tname, + mk_list (map (fst o fst) cons)) ^ ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\ \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\ \val dummy = AddIffs " ^ tname ^ ".inject;\n\