formal markup of constants;
authorwenzelm
Sun Feb 14 00:26:48 2010 +0100 (2010-02-14)
changeset 3512433976519c888
parent 35123 e286d5df187a
child 35125 acace7e30357
formal markup of constants;
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Sat Feb 13 23:24:57 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sun Feb 14 00:26:48 2010 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4        let
     1.5          val (_, (tname, dts, constrs)) = nth descr index;
     1.6          val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
     1.7 -        val T = Type (tname, map mk_ty dts)
     1.8 +        val T = Type (tname, map mk_ty dts);
     1.9        in
    1.10          SOME {case_name = case_name,
    1.11            constructors = map (fn (cname, dts') =>
    1.12 @@ -70,12 +70,13 @@
    1.13  fun default_names names ts =
    1.14    map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
    1.15  
    1.16 -fun strip_constraints (Const ("_constrain", _) $ t $ tT) =
    1.17 +fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
    1.18        strip_constraints t ||> cons tT
    1.19    | strip_constraints t = (t, []);
    1.20  
    1.21 -fun mk_fun_constrain tT t = Syntax.const "_constrain" $ t $
    1.22 -  (Syntax.free "fun" $ tT $ Syntax.free "dummy");
    1.23 +fun mk_fun_constrain tT t =
    1.24 +  Syntax.const @{syntax_const "_constrain"} $ t $
    1.25 +    (Syntax.free "fun" $ tT $ Syntax.free "dummy");    (* FIXME @{type_syntax} (!?) *)
    1.26  
    1.27  
    1.28  (*---------------------------------------------------------------------------
    1.29 @@ -145,7 +146,7 @@
    1.30                          (replicate (length rstp) "x")
    1.31                      in
    1.32                        [((prfx, gvars @ map Free (xs ~~ Ts)),
    1.33 -                        (Const ("HOL.undefined", res_ty), (~1, false)))]
    1.34 +                        (Const (@{const_name HOL.undefined}, res_ty), (~1, false)))]
    1.35                      end
    1.36                    else in_group
    1.37                in
    1.38 @@ -265,12 +266,13 @@
    1.39  
    1.40  fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
    1.41    let
    1.42 -    fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
    1.43 -      (Syntax.const "_case1" $ pat $ rhs);
    1.44 +    fun string_of_clause (pat, rhs) =
    1.45 +      Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
    1.46      val _ = map (no_repeat_vars ctxt o fst) clauses;
    1.47      val rows = map_index (fn (i, (pat, rhs)) =>
    1.48        (([], [pat]), (rhs, (i, true)))) clauses;
    1.49 -    val rangeT = (case distinct op = (map (type_of o snd) clauses) of
    1.50 +    val rangeT =
    1.51 +      (case distinct op = (map (type_of o snd) clauses) of
    1.52          [] => case_error "no clauses given"
    1.53        | [T] => T
    1.54        | _ => case_error "all cases must have the same result type");
    1.55 @@ -283,14 +285,16 @@
    1.56      val patts1 = map
    1.57        (fn (_, tag, [pat]) => (pat, tag)
    1.58          | _ => case_error "error in pattern-match translation") patts;
    1.59 -    val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
    1.60 +    val patts2 = Library.sort (int_ord o pairself row_of_pat) patts1
    1.61      val finals = map row_of_pat patts2
    1.62      val originals = map (row_of_pat o #2) rows
    1.63 -    val _ = case subtract (op =) finals originals of
    1.64 -        [] => ()
    1.65 -        | is => (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
    1.66 -          ("The following clauses are redundant (covered by preceding clauses):\n" ^
    1.67 -           cat_lines (map (string_of_clause o nth clauses) is));
    1.68 +    val _ =
    1.69 +        case subtract (op =) finals originals of
    1.70 +          [] => ()
    1.71 +        | is =>
    1.72 +            (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
    1.73 +              ("The following clauses are redundant (covered by preceding clauses):\n" ^
    1.74 +               cat_lines (map (string_of_clause o nth clauses) is));
    1.75    in
    1.76      (case_tm, patts2)
    1.77    end;
    1.78 @@ -308,10 +312,10 @@
    1.79        val thy = ProofContext.theory_of ctxt;
    1.80        (* replace occurrences of dummy_pattern by distinct variables *)
    1.81        (* internalize constant names                                 *)
    1.82 -      fun prep_pat ((c as Const ("_constrain", _)) $ t $ tT) used =
    1.83 +      fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
    1.84              let val (t', used') = prep_pat t used
    1.85              in (c $ t' $ tT, used') end
    1.86 -        | prep_pat (Const ("dummy_pattern", T)) used =
    1.87 +        | prep_pat (Const (@{const_name dummy_pattern}, T)) used =
    1.88              let val x = Name.variant used "x"
    1.89              in (Free (x, T), x :: used) end
    1.90          | prep_pat (Const (s, T)) used =
    1.91 @@ -333,17 +337,17 @@
    1.92                (t' $ u', used'')
    1.93              end
    1.94          | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
    1.95 -      fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
    1.96 +      fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
    1.97              let val (l', cnstrts) = strip_constraints l
    1.98              in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts)
    1.99              end
   1.100          | dest_case1 t = case_error "dest_case1";
   1.101 -      fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
   1.102 +      fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
   1.103          | dest_case2 t = [t];
   1.104        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
   1.105        val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
   1.106          (if err then Error else Warning) []
   1.107 -        (fold (fn tT => fn t => Syntax.const "_constrain" $ t $ tT)
   1.108 +        (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
   1.109             (flat cnstrts) t) cases;
   1.110      in case_tm end
   1.111    | case_tr _ _ _ ts = case_error "case_tr";
   1.112 @@ -377,7 +381,7 @@
   1.113          fun count_cases (_, _, true) = I
   1.114            | count_cases (c, (_, body), false) =
   1.115                AList.map_default op aconv (body, []) (cons c);
   1.116 -        val is_undefined = name_of #> equal (SOME "HOL.undefined");
   1.117 +        val is_undefined = name_of #> equal (SOME @{const_name HOL.undefined});
   1.118          fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
   1.119        in case ty_info tab cname of
   1.120            SOME {constructors, case_name} =>
   1.121 @@ -394,7 +398,8 @@
   1.122                  val cases' = sort (int_ord o swap o pairself (length o snd))
   1.123                    (fold_rev count_cases cases []);
   1.124                  val R = type_of t;
   1.125 -                val dummy = if d then Const ("dummy_pattern", R)
   1.126 +                val dummy =
   1.127 +                  if d then Const (@{const_name dummy_pattern}, R)
   1.128                    else Free (Name.variant used "x", R)
   1.129                in
   1.130                  SOME (x, map mk_case (case find_first (is_undefined o fst) cases' of
   1.131 @@ -435,7 +440,8 @@
   1.132        else [(pat, rhs)]
   1.133    | _ => [(pat, rhs)];
   1.134  
   1.135 -fun gen_strip_case dest t = case dest [] t of
   1.136 +fun gen_strip_case dest t =
   1.137 +  case dest [] t of
   1.138      SOME (x, clauses) =>
   1.139        SOME (x, maps (strip_case'' dest) clauses)
   1.140    | NONE => NONE;
   1.141 @@ -453,7 +459,7 @@
   1.142      fun mk_clause (pat, rhs) =
   1.143        let val xs = Term.add_frees pat []
   1.144        in
   1.145 -        Syntax.const "_case1" $
   1.146 +        Syntax.const @{syntax_const "_case1"} $
   1.147            map_aterms
   1.148              (fn Free p => Syntax.mark_boundT p
   1.149                | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
   1.150 @@ -463,10 +469,12 @@
   1.151                    if member (op =) xs (s, T) then Syntax.mark_bound s else x
   1.152                | t => t) rhs
   1.153        end
   1.154 -  in case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
   1.155 -      SOME (x, clauses) => Syntax.const "_case_syntax" $ x $
   1.156 -        foldr1 (fn (t, u) => Syntax.const "_case2" $ t $ u)
   1.157 -          (map mk_clause clauses)
   1.158 +  in
   1.159 +    case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
   1.160 +      SOME (x, clauses) =>
   1.161 +        Syntax.const @{syntax_const "_case_syntax"} $ x $
   1.162 +          foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   1.163 +            (map mk_clause clauses)
   1.164      | NONE => raise Match
   1.165    end;
   1.166  
     2.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Sat Feb 13 23:24:57 2010 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sun Feb 14 00:26:48 2010 +0100
     2.3 @@ -229,7 +229,7 @@
     2.4  
     2.5  val trfun_setup =
     2.6    Sign.add_advanced_trfuns ([],
     2.7 -    [("_case_syntax", Datatype_Case.case_tr true info_of_constr)],
     2.8 +    [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr)],
     2.9      [], []);
    2.10  
    2.11