# HG changeset patch # User wenzelm # Date 1149638488 -7200 # Node ID f860b7a984455e3e57fc6aa7c1c42ef1f39d3b42 # Parent 854404b8f7389c5ad9852fae726abebec42d7bb2 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround; diff -r 854404b8f738 -r f860b7a98445 src/HOL/Library/word_setup.ML --- a/src/HOL/Library/word_setup.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/HOL/Library/word_setup.ML Wed Jun 07 02:01:28 2006 +0200 @@ -35,8 +35,8 @@ then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th) else NONE | g _ _ _ = NONE - (*lcp** val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***) - val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g + (*lcp** val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***) + val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g in Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]); thy diff -r 854404b8f738 -r f860b7a98445 src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Wed Jun 07 02:01:28 2006 +0200 @@ -147,7 +147,7 @@ (foldr (fn ((f, p), prf) => (case head_of (strip_abs_body f) of Free (s, T) => - let val T' = Type.varifyT T + let val T' = Logic.varifyT T in Abst (s, SOME T', Proofterm.prf_abstract_over (Var ((s, 0), T')) (AbsP ("H", SOME p, prf))) end @@ -164,8 +164,7 @@ fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) = let - val sg = sign_of thy; - val cert = cterm_of sg; + val cert = cterm_of thy; val rT = TFree ("'P", HOLogic.typeS); val rT' = TVar (("'P", 0), HOLogic.typeS); @@ -187,7 +186,7 @@ val (rs, prems) = split_list (map (make_casedist_prem T) constrs); val r = Const (case_name, map fastype_of rs ---> T --> rT); - val y = Var (("y", 0), Type.varifyT T); + val y = Var (("y", 0), Logic.legacy_varifyT T); val y' = Free ("y", T); val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems, @@ -208,10 +207,10 @@ val P = Var (("P", 0), rT' --> HOLogic.boolT); val prf = forall_intr_prf (y, forall_intr_prf (P, foldr (fn ((p, r), prf) => - forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), + forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p), prf))) (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))) (prems ~~ rs))); - val r' = Logic.varify (Abs ("y", Type.varifyT T, + val r' = Logic.legacy_varify (Abs ("y", Logic.legacy_varifyT T, list_abs (map dest_Free rs, list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))); diff -r 854404b8f738 -r f860b7a98445 src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/HOL/Tools/function_package/termination.ML Wed Jun 07 02:01:28 2006 +0200 @@ -31,7 +31,7 @@ fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom = let val domT = domain_type (fastype_of f) - val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom + val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom val DT = type_of D val idomT = HOLogic.dest_setT DT diff -r 854404b8f738 -r f860b7a98445 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Jun 07 02:01:28 2006 +0200 @@ -60,9 +60,9 @@ val params = map dest_Var ts; val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr), - map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ + map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ filter_out (equal Extraction.nullT) (map - (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), + (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), NoSyn); in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn, map constr_of_intr intrs) diff -r 854404b8f738 -r f860b7a98445 src/Pure/IsaPlanner/term_lib.ML --- a/src/Pure/IsaPlanner/term_lib.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/IsaPlanner/term_lib.ML Wed Jun 07 02:01:28 2006 +0200 @@ -661,15 +661,15 @@ fun change_vars_to_frees (a$b) = (change_vars_to_frees a) $ (change_vars_to_frees b) | change_vars_to_frees (Abs(s,ty,t)) = - (Abs(s,Type.varifyT ty,change_vars_to_frees t)) - | change_vars_to_frees (Var((s,i),ty)) = (Free(s,Type.unvarifyT ty)) + (Abs(s, Logic.legacy_varifyT ty,change_vars_to_frees t)) + | change_vars_to_frees (Var((s,i),ty)) = (Free(s, Logic.legacy_unvarifyT ty)) | change_vars_to_frees l = l; fun change_frees_to_vars (a$b) = (change_frees_to_vars a) $ (change_frees_to_vars b) | change_frees_to_vars (Abs(s,ty,t)) = - (Abs(s,Type.varifyT ty,change_frees_to_vars t)) - | change_frees_to_vars (Free(s,ty)) = (Var((s,0),Type.varifyT ty)) + (Abs(s, Logic.legacy_varifyT ty,change_frees_to_vars t)) + | change_frees_to_vars (Free(s,ty)) = (Var((s,0), Logic.legacy_varifyT ty)) | change_frees_to_vars l = l; diff -r 854404b8f738 -r f860b7a98445 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Wed Jun 07 02:01:28 2006 +0200 @@ -499,7 +499,7 @@ in thy |> Sign.add_const_constraint_i (c, NONE) - |> pair (c, Type.unvarifyT ty) + |> pair (c, Logic.legacy_unvarifyT ty) end; fun check_defs0 thy raw_defs c_req = let @@ -508,8 +508,8 @@ val c_given = map get_c raw_defs; fun eq_c ((c1 : string, ty1), (c2, ty2)) = let - val ty1' = Type.varifyT ty1; - val ty2' = Type.varifyT ty2; + val ty1' = Logic.legacy_varifyT ty1; + val ty2' = Logic.legacy_varifyT ty2; in c1 = c2 andalso Sign.typ_instance thy (ty1', ty2') @@ -649,8 +649,8 @@ fun extract_lookup thy sortctxt raw_typ_def raw_typ_use = let - val typ_def = Type.varifyT raw_typ_def; - val typ_use = Type.varifyT raw_typ_use; + val typ_def = Logic.legacy_varifyT raw_typ_def; + val typ_use = Logic.legacy_varifyT raw_typ_use; val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty; fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0); fun mk_class_deriv thy subclasses superclass = @@ -682,14 +682,14 @@ fun extract_classlookup thy (c, raw_typ_use) = let val raw_typ_def = Sign.the_const_constraint thy c; - val typ_def = Type.varifyT raw_typ_def; + val typ_def = Logic.legacy_varifyT raw_typ_def; fun reorder_sortctxt ctxt = case lookup_const_class thy c of NONE => ctxt | SOME class => let val data = the_class_data thy class; - val sign = (Type.varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c; + val sign = (Logic.legacy_varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c; val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty; val v : string = case Vartab.lookup match_tab (#var data, 0) of SOME (_, TVar ((v, _), _)) => v; diff -r 854404b8f738 -r f860b7a98445 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Wed Jun 07 02:01:28 2006 +0200 @@ -605,7 +605,7 @@ |> fold_map (ensure_def_class thy tabs) clss |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i)))) and mk_fun thy tabs (c, ty) trns = - case CodegenTheorems.get_funs thy (c, Type.varifyT ty) + case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty) (* FIXME *) of SOME (ty, eq_thms) => let val sortctxt = ClassPackage.extract_sortctxt thy ty; @@ -849,7 +849,7 @@ fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns = let - val ty_def = (op ---> o apfst tl o strip_type o Type.unvarifyT o Sign.the_const_type thy) c; + val ty_def = (op ---> o apfst tl o strip_type o Logic.legacy_unvarifyT o Sign.the_const_type thy) c; val ty' = (op ---> o apfst tl o strip_type) ty; val idf = idf_of_const thy tabs (c, ty); in diff -r 854404b8f738 -r f860b7a98445 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Wed Jun 07 02:01:28 2006 +0200 @@ -619,7 +619,7 @@ fun preprocess_term thy raw_t = let - val t = (Term.map_term_types Type.varifyT o Logic.varify) raw_t; + val t = Logic.legacy_varify raw_t; val x = variant (add_term_names (t, [])) "a"; val t_eq = Logic.mk_equals (Free (x, fastype_of t), t); (*fake definition*) diff -r 854404b8f738 -r f860b7a98445 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/codegen.ML Wed Jun 07 02:01:28 2006 +0200 @@ -558,7 +558,7 @@ (**** retrieve definition of constant ****) fun is_instance thy T1 T2 = - Sign.typ_instance thy (T1, Type.varifyT T2); + Sign.typ_instance thy (T1, Logic.legacy_varifyT T2); fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) => s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); diff -r 854404b8f738 -r f860b7a98445 src/Pure/defs.ML --- a/src/Pure/defs.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/defs.ML Wed Jun 07 02:01:28 2006 +0200 @@ -33,7 +33,7 @@ let val prt_args = if null args then [] - else [Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)]; + else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)]; in Pretty.block (Pretty.str c :: prt_args) end; fun plain_args args = diff -r 854404b8f738 -r f860b7a98445 src/Pure/display.ML --- a/src/Pure/display.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/display.ML Wed Jun 07 02:01:28 2006 +0200 @@ -169,7 +169,7 @@ fun prt_sort S = Sign.pretty_sort thy S; fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]); fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty); - val prt_typ_no_tvars = prt_typ o Type.freeze_type; + val prt_typ_no_tvars = prt_typ o Logic.unvarifyT; fun prt_term t = Pretty.quote (Sign.pretty_term thy t); val prt_term_no_vars = prt_term o Logic.unvarify; fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; diff -r 854404b8f738 -r f860b7a98445 src/Pure/logic.ML --- a/src/Pure/logic.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/logic.ML Wed Jun 07 02:01:28 2006 +0200 @@ -67,8 +67,14 @@ val set_rename_prefix: string -> unit val list_rename_params: string list * term -> term val assum_pairs: int * term -> (term*term)list + val varifyT: typ -> typ + val unvarifyT: typ -> typ val varify: term -> term val unvarify: term -> term + val legacy_varifyT: typ -> typ + val legacy_unvarifyT: typ -> typ + val legacy_varify: term -> term + val legacy_unvarify: term -> term val get_goal: term -> int -> term val goal_params: term -> int -> term * term list val prems_of_goal: term -> int -> term list @@ -492,7 +498,7 @@ all T $ Abs(c, T, list_rename_params (cs, t)) | list_rename_params (cs, B) = B; -(*** Treatmsent of "assume", "erule", etc. ***) +(*** Treatment of "assume", "erule", etc. ***) (*Strips assumptions in goal yielding HS = [Hn,...,H1], params = [xm,...,x1], and B, @@ -529,22 +535,46 @@ in pairrev (Hs,[]) end; -(*Converts Frees to Vars and TFrees to TVars*) -fun varify (Const(a, T)) = Const (a, Type.varifyT T) - | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T) - | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T) - | varify (t as Bound _) = t - | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body) - | varify (f $ t) = varify f $ varify t; + +(* global schematic variables *) + +fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); +fun bad_fixed x = "Illegal fixed variable: " ^ quote x; + +fun varifyT ty = ty |> Term.map_atyps + (fn TFree (a, S) => TVar ((a, 0), S) + | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); + +fun unvarifyT ty = ty |> Term.map_atyps + (fn TVar ((a, 0), S) => TFree (a, S) + | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) + | TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); -(*Inverse of varify.*) -fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T) - | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T) - | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T) - | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T) (*non-0 index!*) - | unvarify (t as Bound _) = t - | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body) - | unvarify (f $ t) = unvarify f $ unvarify t; +fun varify tm = + tm |> Term.map_aterms + (fn Free (x, T) => Var ((x, 0), T) + | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) + | t => t) + |> Term.map_term_types varifyT; + +fun unvarify tm = + tm |> Term.map_aterms + (fn Var ((x, 0), T) => Free (x, T) + | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) + | Free (x, _) => raise TERM (bad_fixed x, [tm]) + | t => t) + |> Term.map_term_types unvarifyT; + +val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T); +val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T); + +val legacy_varify = + Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #> + Term.map_term_types legacy_varifyT; + +val legacy_unvarify = + Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #> + Term.map_term_types legacy_unvarifyT; (* goal states *) diff -r 854404b8f738 -r f860b7a98445 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/sign.ML Wed Jun 07 02:01:28 2006 +0200 @@ -721,7 +721,7 @@ fun gen_add_consts prep_typ authentic raw_args thy = let - val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy; + val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy; fun prep (raw_c, raw_T, raw_mx) = let val (c, mx) = Syntax.const_mixfix raw_c raw_mx; @@ -755,7 +755,7 @@ val (c, mx) = Syntax.const_mixfix raw_c raw_mx; val c' = Syntax.constN ^ full_name thy c; - val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg) + val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg) handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); val T = Term.fastype_of t; in @@ -772,7 +772,7 @@ let val c = int_const thy raw_c; fun prepT raw_T = - let val T = Type.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T))) + let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T))) in cert_term thy (Const (c, T)); T end handle TYPE (msg, _, _) => error msg; in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end; diff -r 854404b8f738 -r f860b7a98445 src/Pure/theory.ML --- a/src/Pure/theory.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/theory.ML Wed Jun 07 02:01:28 2006 +0200 @@ -240,7 +240,7 @@ val consts = Sign.consts_of thy; fun prep const = let val Const (c, T) = Sign.no_vars pp (Const const) - in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end; + in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end; val lhs_vars = Term.add_tfreesT (#2 lhs) []; val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v => @@ -267,7 +267,7 @@ (case Sign.const_constraint thy c of NONE => error ("Undeclared constant " ^ quote c) | SOME declT => declT); - val T' = Type.varifyT T; + val T' = Logic.varifyT T; fun message txt = [Pretty.block [Pretty.str "Specification of constant ", diff -r 854404b8f738 -r f860b7a98445 src/Pure/type.ML --- a/src/Pure/type.ML Wed Jun 07 02:01:27 2006 +0200 +++ b/src/Pure/type.ML Wed Jun 07 02:01:28 2006 +0200 @@ -40,8 +40,6 @@ (*special treatment of type vars*) val strip_sorts: typ -> typ val no_tvars: typ -> typ - val varifyT: typ -> typ - val unvarifyT: typ -> typ val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list val freeze_thaw_type: typ -> typ * (typ -> typ) val freeze_type: typ -> typ @@ -228,10 +226,7 @@ commas_quote (map (Term.string_of_vname o #1) vs), [T], [])); -(* varify, unvarify *) - -val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S)); -val unvarifyT = map_type_tvar (fn ((a, 0), S) => TFree (a, S) | v => TVar v); +(* varify *) fun varify (t, fixed) = let