src/Tools/code/code_target.ML
changeset 25936 f43bac9def6e
parent 25771 a81c0ad97133
child 25969 d3f8ab2726ed
     1.1 --- a/src/Tools/code/code_target.ML	Mon Jan 21 08:43:35 2008 +0100
     1.2 +++ b/src/Tools/code/code_target.ML	Mon Jan 21 08:43:36 2008 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val add_pretty_list_string: string -> string -> string
     1.5      -> string -> string list -> theory -> theory;
     1.6    val add_pretty_char: string -> string -> string list -> theory -> theory
     1.7 -  val add_pretty_numeral: string -> bool -> string -> string -> string -> string
     1.8 +  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string -> string
     1.9      -> string -> string -> theory -> theory;
    1.10    val add_pretty_message: string -> string -> string list -> string
    1.11      -> string -> string -> theory -> theory;
    1.12 @@ -234,22 +234,22 @@
    1.13      else NONE
    1.14    end;
    1.15  
    1.16 -fun implode_numeral c_bit0 c_bit1 c_pls c_min c_bit =
    1.17 +fun implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit =
    1.18    let
    1.19 -    fun dest_bit (IConst (c, _)) = if c = c_bit0 then SOME 0
    1.20 -          else if c = c_bit1 then SOME 1
    1.21 -          else NONE
    1.22 -      | dest_bit _ = NONE;
    1.23 +    fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
    1.24 +          else if c = c_bit1 then 1
    1.25 +          else error "Illegal numeral expression: illegal bit"
    1.26 +      | dest_bit _ = error "Illegal numeral expression: illegal bit";
    1.27      fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
    1.28 -          else if c = c_min then SOME ~1
    1.29 -          else NONE
    1.30 +          else if c = c_min then
    1.31 +            if negative then SOME ~1 else NONE
    1.32 +          else error "Illegal numeral expression"
    1.33        | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
    1.34 -          if c = c_bit then case (dest_numeral t1, dest_bit t2)
    1.35 -           of (SOME n, SOME b) => SOME (2 * n + b)
    1.36 -            | _ => NONE
    1.37 -          else NONE
    1.38 -      | dest_numeral _ = NONE;
    1.39 -  in dest_numeral end;
    1.40 +          if c = c_bit then let val (n, b) = (dest_numeral t1, dest_bit t2)
    1.41 +            in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    1.42 +          else error "Illegal numeral expression"
    1.43 +      | dest_numeral _ = error "Illegal numeral expression";
    1.44 +  in dest_numeral #> the_default 0 end;
    1.45  
    1.46  fun implode_monad c_bind t =
    1.47    let
    1.48 @@ -1825,13 +1825,11 @@
    1.49          | NONE => error "Illegal character expression";
    1.50    in (2, pretty) end;
    1.51  
    1.52 -fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =
    1.53 +fun pretty_numeral unbounded negative c_bit0 c_bit1 c_pls c_min c_bit target =
    1.54    let
    1.55      val mk_numeral = #pretty_numeral (pr_pretty target);
    1.56      fun pretty _ _ _ [(t, _)] =
    1.57 -      case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
    1.58 -       of SOME k => (str o mk_numeral unbounded) k
    1.59 -        | NONE => error "Illegal numeral expression";
    1.60 +      (str o mk_numeral unbounded o implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit) t;
    1.61    in (1, pretty) end;
    1.62  
    1.63  fun pretty_message c_char c_nibbles c_nil c_cons target =
    1.64 @@ -2102,14 +2100,14 @@
    1.65      |> add_syntax_const target charr (SOME pr)
    1.66    end;
    1.67  
    1.68 -fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
    1.69 +fun add_pretty_numeral target unbounded negative number_of b0 b1 pls min bit thy =
    1.70    let
    1.71      val b0' = CodeName.const thy b0;
    1.72      val b1' = CodeName.const thy b1;
    1.73      val pls' = CodeName.const thy pls;
    1.74      val min' = CodeName.const thy min;
    1.75      val bit' = CodeName.const thy bit;
    1.76 -    val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;
    1.77 +    val pr = pretty_numeral unbounded negative b0' b1' pls' min' bit' target;
    1.78    in
    1.79      thy
    1.80      |> add_syntax_const target number_of (SOME pr)