adapted to authentic syntax -- actual types are verbatim;
authorwenzelm
Wed Mar 03 00:32:14 2010 +0100 (2010-03-03)
changeset 35430df2862dc23a8
parent 35429 afa8cf9e63d8
child 35431 8758fe1fc9f8
adapted to authentic syntax -- actual types are verbatim;
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/HOL/Typerep.thy
src/HOL/ex/Numeral.thy
src/Sequents/Sequents.thy
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Mar 03 00:28:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Mar 03 00:32:14 2010 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
     1.8 +fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
     1.9        let val t' =
    1.10          if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
    1.11          else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
     2.1 --- a/src/HOL/Tools/record.ML	Wed Mar 03 00:28:22 2010 +0100
     2.2 +++ b/src/HOL/Tools/record.ML	Wed Mar 03 00:32:14 2010 +0100
     2.3 @@ -697,10 +697,8 @@
     2.4    let
     2.5      fun get_sort env xi =
     2.6        the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
     2.7 -    val map_sort = Sign.intern_sort thy;
     2.8    in
     2.9 -    Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
    2.10 -    |> Sign.intern_tycons thy
    2.11 +    Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
    2.12    end;
    2.13  
    2.14  
    2.15 @@ -752,8 +750,8 @@
    2.16  
    2.17                      val more' = mk_ext rest;
    2.18                    in
    2.19 -                    (* FIXME authentic syntax *)
    2.20 -                    list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more'])
    2.21 +                    list_comb
    2.22 +                      (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
    2.23                    end
    2.24                | NONE => err ("no fields defined for " ^ ext))
    2.25            | NONE => err (name ^ " is no proper field"))
    2.26 @@ -857,7 +855,7 @@
    2.27      val T = decode_type thy t;
    2.28      val varifyT = varifyT (Term.maxidx_of_typ T);
    2.29  
    2.30 -    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts) o Sign.extern_typ thy;
    2.31 +    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
    2.32  
    2.33      fun strip_fields T =
    2.34        (case T of
    2.35 @@ -922,8 +920,7 @@
    2.36  
    2.37      fun mk_type_abbr subst name alphas =
    2.38        let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
    2.39 -        Syntax.term_of_typ (! Syntax.show_sorts)
    2.40 -          (Sign.extern_typ thy (Envir.norm_type subst abbrT))
    2.41 +        Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
    2.42        end;
    2.43  
    2.44      fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
    2.45 @@ -946,14 +943,14 @@
    2.46  
    2.47  fun record_ext_type_tr' name =
    2.48    let
    2.49 -    val ext_type_name = suffix ext_typeN name;
    2.50 +    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
    2.51      fun tr' ctxt ts =
    2.52        record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
    2.53    in (ext_type_name, tr') end;
    2.54  
    2.55  fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
    2.56    let
    2.57 -    val ext_type_name = suffix ext_typeN name;
    2.58 +    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
    2.59      fun tr' ctxt ts =
    2.60        record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
    2.61          (list_comb (Syntax.const ext_type_name, ts));
    2.62 @@ -1949,8 +1946,7 @@
    2.63          val (args', more) = chop_last args;
    2.64          fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
    2.65          fun build Ts =
    2.66 -          fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args'))
    2.67 -            more;
    2.68 +          fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
    2.69        in
    2.70          if more = HOLogic.unit
    2.71          then build (map_range recT (parent_len + 1))
    2.72 @@ -1960,27 +1956,25 @@
    2.73      val r_rec0 = mk_rec all_vars_more 0;
    2.74      val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
    2.75  
    2.76 -    fun r n = Free (rN, rec_schemeT n)
    2.77 +    fun r n = Free (rN, rec_schemeT n);
    2.78      val r0 = r 0;
    2.79 -    fun r_unit n = Free (rN, recT n)
    2.80 +    fun r_unit n = Free (rN, recT n);
    2.81      val r_unit0 = r_unit 0;
    2.82 -    val w = Free (wN, rec_schemeT 0)
    2.83 +    val w = Free (wN, rec_schemeT 0);
    2.84  
    2.85  
    2.86      (* print translations *)
    2.87  
    2.88 -    val external_names = Name_Space.external_names (Sign.naming_of ext_thy);
    2.89 -
    2.90      val record_ext_type_abbr_tr's =
    2.91        let
    2.92 -        val trnames = external_names (hd extension_names);
    2.93 +        val trname = hd extension_names;
    2.94          val last_ext = unsuffix ext_typeN (fst extension);
    2.95 -      in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
    2.96 +      in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
    2.97  
    2.98      val record_ext_type_tr's =
    2.99        let
   2.100          (*avoid conflict with record_type_abbr_tr's*)
   2.101 -        val trnames = if parent_len > 0 then external_names extension_name else [];
   2.102 +        val trnames = if parent_len > 0 then [extension_name] else [];
   2.103        in map record_ext_type_tr' trnames end;
   2.104  
   2.105      val advanced_print_translation =
     3.1 --- a/src/HOL/Tools/typedef.ML	Wed Mar 03 00:28:22 2010 +0100
     3.2 +++ b/src/HOL/Tools/typedef.ML	Wed Mar 03 00:32:14 2010 +0100
     3.3 @@ -118,7 +118,7 @@
     3.4      fun add_def theory =
     3.5        if def then
     3.6          theory
     3.7 -        |> Sign.add_consts_i [(name, setT', NoSyn)]   (* FIXME authentic syntax *)
     3.8 +        |> Sign.add_consts_i [(name, setT', NoSyn)]
     3.9          |> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
    3.10          |-> (fn [th] => pair (SOME th))
    3.11        else (NONE, theory);
     4.1 --- a/src/HOL/Typerep.thy	Wed Mar 03 00:28:22 2010 +0100
     4.2 +++ b/src/HOL/Typerep.thy	Wed Mar 03 00:32:14 2010 +0100
     4.3 @@ -33,7 +33,7 @@
     4.4  typed_print_translation {*
     4.5  let
     4.6    fun typerep_tr' show_sorts (*"typerep"*)
     4.7 -          (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
     4.8 +          (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
     4.9            (Const (@{const_syntax TYPE}, _) :: ts) =
    4.10          Term.list_comb
    4.11            (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
     5.1 --- a/src/HOL/ex/Numeral.thy	Wed Mar 03 00:28:22 2010 +0100
     5.2 +++ b/src/HOL/ex/Numeral.thy	Wed Mar 03 00:32:14 2010 +0100
     5.3 @@ -327,7 +327,7 @@
     5.4        val k = int_of_num' n;
     5.5        val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
     5.6      in case T
     5.7 -     of Type (@{type_syntax fun}, [_, T']) =>
     5.8 +     of Type (@{type_name fun}, [_, T']) =>
     5.9           if not (! show_types) andalso can Term.dest_Type T' then t'
    5.10           else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
    5.11        | T' => if T' = dummyT then t' else raise Match
     6.1 --- a/src/Sequents/Sequents.thy	Wed Mar 03 00:28:22 2010 +0100
     6.2 +++ b/src/Sequents/Sequents.thy	Wed Mar 03 00:32:14 2010 +0100
     6.3 @@ -65,7 +65,7 @@
     6.4  
     6.5  (* parse translation for sequences *)
     6.6  
     6.7 -fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t);
     6.8 +fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
     6.9  
    6.10  fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
    6.11        Const (@{const_syntax SeqO'}, dummyT) $ f