src/HOL/Main.thy
changeset 12024 b3661262541e
parent 11533 0c0d2332e8f0
child 12439 e90a4f5a27f0
     1.1 --- a/src/HOL/Main.thy	Sat Nov 03 01:33:54 2001 +0100
     1.2 +++ b/src/HOL/Main.thy	Sat Nov 03 01:35:11 2001 +0100
     1.3 @@ -1,21 +1,98 @@
     1.4  (*  Title:      HOL/Main.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   2000 TU Muenchen
     1.8 -
     1.9 -Theory Main includes everything.
    1.10 -Note that theory PreList already includes most HOL theories.
    1.11 +    Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
    1.12 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.13  *)
    1.14  
    1.15 -theory Main = Map + String + Hilbert_Choice:
    1.16 +header {* Main HOL *}
    1.17 +
    1.18 +theory Main = Map + Hilbert_Choice:
    1.19  
    1.20 -(*belongs to theory List*)
    1.21 +text {*
    1.22 +  Theory @{text Main} includes everything.  Note that theory @{text
    1.23 +  PreList} already includes most HOL theories.
    1.24 +*}
    1.25 +
    1.26 +text {* Belongs to theory List. *}
    1.27  declare lists_mono [mono]
    1.28  declare map_cong [recdef_cong]
    1.29  lemmas rev_induct [case_names Nil snoc] = rev_induct
    1.30    and rev_cases [case_names Nil snoc] = rev_exhaust
    1.31  
    1.32 -(** configuration of code generator **)
    1.33 +
    1.34 +subsection {* Characters and strings *}
    1.35 +
    1.36 +datatype nibble =
    1.37 +    Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    1.38 +  | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    1.39 +
    1.40 +datatype char = Char nibble nibble
    1.41 +  -- "Note: canonical order of character encoding coincides with standard term ordering"
    1.42 +
    1.43 +types string = "char list"
    1.44 +
    1.45 +syntax
    1.46 +  "_Char" :: "xstr => char"    ("CHR _")
    1.47 +  "_String" :: "xstr => string"    ("_")
    1.48 +
    1.49 +parse_ast_translation {*
    1.50 +  let
    1.51 +    val constants = Syntax.Appl o map Syntax.Constant;
    1.52 +
    1.53 +    fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10));
    1.54 +    fun mk_char c =
    1.55 +      if Symbol.is_ascii c andalso Symbol.is_printable c then
    1.56 +        constants ["Char", mk_nib (ord c div 16), mk_nib (ord c mod 16)]
    1.57 +      else error ("Printable ASCII character expected: " ^ quote c);
    1.58 +
    1.59 +    fun mk_string [] = Syntax.Constant "Nil"
    1.60 +      | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
    1.61 +
    1.62 +    fun char_ast_tr [Syntax.Variable xstr] =
    1.63 +        (case Syntax.explode_xstr xstr of
    1.64 +          [c] => mk_char c
    1.65 +        | _ => error ("Single character expected: " ^ xstr))
    1.66 +      | char_ast_tr asts = raise AST ("char_ast_tr", asts);
    1.67 +
    1.68 +    fun string_ast_tr [Syntax.Variable xstr] =
    1.69 +        (case Syntax.explode_xstr xstr of
    1.70 +          [] => constants [Syntax.constrainC, "Nil", "string"]
    1.71 +        | cs => mk_string cs)
    1.72 +      | string_ast_tr asts = raise AST ("string_tr", asts);
    1.73 +  in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
    1.74 +*}
    1.75 +
    1.76 +print_ast_translation {*
    1.77 +  let
    1.78 +    fun dest_nib (Syntax.Constant c) =
    1.79 +        (case explode c of
    1.80 +          ["N", "i", "b", "b", "l", "e", h] =>
    1.81 +            if "0" <= h andalso h <= "9" then ord h - ord "0"
    1.82 +            else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
    1.83 +            else raise Match
    1.84 +        | _ => raise Match)
    1.85 +      | dest_nib _ = raise Match;
    1.86 +
    1.87 +    fun dest_chr c1 c2 =
    1.88 +      let val c = chr (dest_nib c1 * 16 + dest_nib c2)
    1.89 +      in if Symbol.is_printable c then c else raise Match end;
    1.90 +
    1.91 +    fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
    1.92 +      | dest_char _ = raise Match;
    1.93 +
    1.94 +    fun xstr cs = Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
    1.95 +
    1.96 +    fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", xstr [dest_chr c1 c2]]
    1.97 +      | char_ast_tr' _ = raise Match;
    1.98 +
    1.99 +    fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
   1.100 +            xstr (map dest_char (Syntax.unfold_ast "_args" args))]
   1.101 +      | list_ast_tr' ts = raise Match;
   1.102 +  in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
   1.103 +*}
   1.104 +
   1.105 +
   1.106 +subsection {* Configuration of the code generator *}
   1.107  
   1.108  types_code
   1.109    "bool"  ("bool")