Name.invent_list;
authorwenzelm
Tue Jul 11 12:17:01 2006 +0200 (2006-07-11)
changeset 20076def4ad161528
parent 20075 a7e183bfebef
child 20077 4fc9a4fef219
Name.invent_list;
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_theorems.ML
src/Pure/display.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 11 12:17:00 2006 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 11 12:17:01 2006 +0200
     1.3 @@ -194,8 +194,7 @@
     1.4    let
     1.5      fun rew_term Ts t =
     1.6        let
     1.7 -        val frees = map Free (variantlist
     1.8 -          (replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
     1.9 +        val frees = map Free (Name.invent_list (add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
    1.10          val t' = r (subst_bounds (frees, t));
    1.11          fun strip [] t = t
    1.12            | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Jul 11 12:17:00 2006 +0200
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Jul 11 12:17:01 2006 +0200
     2.3 @@ -297,7 +297,7 @@
     2.4            val rangeT = Term.range_type typ handle Match =>
     2.5              err_in_mfix "Missing structure argument for indexed syntax" mfix;
     2.6  
     2.7 -          val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
     2.8 +          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
     2.9            val (xs1, xs2) = chop (find_index is_index args) xs;
    2.10            val i = Ast.Variable "i";
    2.11            val lhs = Ast.mk_appl (Ast.Constant indexed_const)
     3.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 11 12:17:00 2006 +0200
     3.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 11 12:17:01 2006 +0200
     3.3 @@ -384,7 +384,7 @@
     3.4  (* dependent / nondependent quantifiers *)
     3.5  
     3.6  fun variant_abs' (x, T, B) =
     3.7 -  let val x' = variant (add_term_names (B, [])) x in
     3.8 +  let val x' = Name.variant (add_term_names (B, [])) x in
     3.9      (x', subst_bound (mark_boundT (x', T), B))
    3.10    end;
    3.11  
     4.1 --- a/src/Pure/Tools/class_package.ML	Tue Jul 11 12:17:00 2006 +0200
     4.2 +++ b/src/Pure/Tools/class_package.ML	Tue Jul 11 12:17:01 2006 +0200
     4.3 @@ -174,7 +174,7 @@
     4.4      val (clsvar, const_sign) = the_consts_sign thy class;
     4.5      fun add_var sort used =
     4.6        let
     4.7 -        val v = hd (Term.invent_names used "'a" 1)
     4.8 +        val [v] = Name.invent_list used "'a" 1
     4.9        in ((v, sort), v::used) end;
    4.10      val (vsorts, _) =
    4.11        [clsvar]
    4.12 @@ -405,7 +405,8 @@
    4.13    let
    4.14      val pp = Sign.pp theory;
    4.15      val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity);
    4.16 -    val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
    4.17 +    val ty_inst =
    4.18 +      Type (tyco, map2 (curry TVar o rpair 0) (Name.invent_list [] "'a" (length asorts)) asorts)
    4.19      val name = case raw_name
    4.20       of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco)
    4.21        | _ => raw_name;
    4.22 @@ -473,7 +474,7 @@
    4.23      theory
    4.24      |> fold_map get_remove_contraint (map fst cs)
    4.25      ||>> add_defs defs
    4.26 -    |-> (fn (cs, def_thms) => 
    4.27 +    |-> (fn (cs, def_thms) =>
    4.28         fold register_def def_thms
    4.29      #> note_all
    4.30      #> do_proof (after_qed cs) arity)
    4.31 @@ -525,9 +526,10 @@
    4.32        in (export_name, map (Name o NameSpace.append thm_name_base) prop_names) end;
    4.33      val notes_tab_proto = map mk_thm_names prop_tab;
    4.34      fun test_note thy thmref =
    4.35 -      can (Locale.note_thmss PureThy.corollaryK loc_name 
    4.36 +      can (Locale.note_thmss PureThy.corollaryK loc_name
    4.37          [(("", []), [(thmref, [])])]) (Theory.copy thy);
    4.38 -    val notes_tab = map_filter (fn (export_name, thm_names) => case filter (test_note theory) thm_names
    4.39 +    val notes_tab = map_filter (fn (export_name, thm_names) =>
    4.40 +     case filter (test_note theory) thm_names
    4.41       of [] => NONE
    4.42        | thm_names' => SOME (export_name, thm_names')) notes_tab_proto;
    4.43      val _ = writeln ("fishing for ");
     5.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Jul 11 12:17:00 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Jul 11 12:17:01 2006 +0200
     5.3 @@ -173,7 +173,7 @@
     5.4          case (find_first (fn {lhs, ...} => Sign.typ_equiv thy (ty, lhs))
     5.5              (Theory.definitions_of thy c))
     5.6           of SOME {module, ...} => NameSpace.append module nsp_overl
     5.7 -          | NONE => if c = "op ="
     5.8 +          | NONE => if c = "op ="   (* FIXME depends on object-logic!? *)
     5.9                then
    5.10                  NameSpace.append
    5.11                    ((thyname_of_tyco thy o fst o dest_Type o hd o fst o strip_type) ty)
    5.12 @@ -839,7 +839,7 @@
    5.13          if length ts < imin then
    5.14            let
    5.15              val d = imin - length ts;
    5.16 -            val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d;
    5.17 +            val vs = Name.invent_list (add_term_names (Const (f, ty), [])) "x" d;
    5.18              val tys = Library.take (d, ((fst o strip_type) ty));
    5.19            in
    5.20              trns
    5.21 @@ -936,8 +936,8 @@
    5.22      val (ts', t) = split_last ts;
    5.23      val (tys, dty) = (split_last o fst o strip_type) ty;
    5.24      fun gen_names i =
    5.25 -      variantlist (replicate i "x", foldr add_term_names
    5.26 -       (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts);
    5.27 +      Name.invent_list (foldr add_term_names
    5.28 +       (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) "xa" i;
    5.29      fun cg_case_d (((cname, i), ty), t) trns =
    5.30        let
    5.31          val vs = gen_names i;
    5.32 @@ -1012,7 +1012,7 @@
    5.33              end) ((#2 o #constants o Consts.dest o #consts o Sign.rep_sg) thy)
    5.34        |> (fn (overltab1, overltab2) =>
    5.35              let
    5.36 -              val c = "op =";
    5.37 +              val c = "op =";   (* FIXME depends on object-logic!? *)
    5.38                val ty = Sign.the_const_type thy c;
    5.39                fun inst tyco =
    5.40                  let
    5.41 @@ -1020,7 +1020,7 @@
    5.42                      tyco
    5.43                      |> Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy)
    5.44                      |> (fn SOME (Type.LogicalType i, _) => i)
    5.45 -                    |> Term.invent_names [] "'a"
    5.46 +                    |> Name.invent_list [] "'a"
    5.47                      |> map (fn v => (TVar ((v, 0), Sign.defaultS thy)))
    5.48                      |> (fn tys => Type (tyco, tys))
    5.49                  in map_atyps (fn _ => ty_inst) ty end;
     6.1 --- a/src/Pure/Tools/codegen_theorems.ML	Tue Jul 11 12:17:00 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Tue Jul 11 12:17:01 2006 +0200
     6.3 @@ -216,7 +216,7 @@
     6.4          val lhs = (fst o Logic.dest_equals) t;
     6.5          val tys = (fst o strip_type o type_of) lhs;
     6.6          val used = fold_aterms (fn Var ((v, _), _) => insert (op =) v | _ => I) lhs [];
     6.7 -        val vs = Term.invent_names used "x" (length tys);
     6.8 +        val vs = Name.invent_list used "x" (length tys);
     6.9        in
    6.10          map2 (fn v => fn ty => Var ((v, 0), ty)) vs tys
    6.11        end;
    6.12 @@ -676,7 +676,7 @@
    6.13      fun mk_lhs vs ((co1, tys1), (co2, tys2)) =
    6.14        let
    6.15          val dty = Type (dtco, map TFree vs);
    6.16 -        val (xs1, xs2) = chop (length tys1) (Term.invent_names [] "x" (length tys1 + length tys2));
    6.17 +        val (xs1, xs2) = chop (length tys1) (Name.invent_list [] "x" (length tys1 + length tys2));
    6.18          val frees1 = map2 (fn x => fn ty => Free (x, ty)) xs1 tys1;
    6.19          val frees2 = map2 (fn x => fn ty => Free (x, ty)) xs2 tys2;
    6.20          fun zip_co co xs tys = list_comb (Const (co,
     7.1 --- a/src/Pure/display.ML	Tue Jul 11 12:17:00 2006 +0200
     7.2 +++ b/src/Pure/display.ML	Tue Jul 11 12:17:01 2006 +0200
     7.3 @@ -191,7 +191,7 @@
     7.4      val tfrees = map (fn v => TFree (v, []));
     7.5      fun pretty_type syn (t, (Type.LogicalType n, _)) =
     7.6            if syn then NONE
     7.7 -          else SOME (prt_typ (Type (t, tfrees (Term.invent_names [] "'a" n))))
     7.8 +          else SOME (prt_typ (Type (t, tfrees (Name.invent_list [] "'a" n))))
     7.9        | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
    7.10            if syn <> syn' then NONE
    7.11            else SOME (Pretty.block
     8.1 --- a/src/Pure/type_infer.ML	Tue Jul 11 12:17:00 2006 +0200
     8.2 +++ b/src/Pure/type_infer.ML	Tue Jul 11 12:17:01 2006 +0200
     8.3 @@ -245,7 +245,7 @@
     8.4  
     8.5      val used' = fold add_names ts (fold add_namesT Ts used);
     8.6      val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
     8.7 -    val names = Term.invent_names used' (prfx ^ "'a") (length parms);
     8.8 +    val names = Name.invent_list used' (prfx ^ "'a") (length parms);
     8.9    in
    8.10      ListPair.app elim (parms, names);
    8.11      (map simple_typ_of Ts, map simple_term_of ts)