src/HOL/Main.thy
author wenzelm
Sat Nov 03 01:35:11 2001 +0100 (2001-11-03)
changeset 12024 b3661262541e
parent 11533 0c0d2332e8f0
child 12439 e90a4f5a27f0
permissions -rw-r--r--
moved String into Main;
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Main HOL *}
     8 
     9 theory Main = Map + Hilbert_Choice:
    10 
    11 text {*
    12   Theory @{text Main} includes everything.  Note that theory @{text
    13   PreList} already includes most HOL theories.
    14 *}
    15 
    16 text {* Belongs to theory List. *}
    17 declare lists_mono [mono]
    18 declare map_cong [recdef_cong]
    19 lemmas rev_induct [case_names Nil snoc] = rev_induct
    20   and rev_cases [case_names Nil snoc] = rev_exhaust
    21 
    22 
    23 subsection {* Characters and strings *}
    24 
    25 datatype nibble =
    26     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    27   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    28 
    29 datatype char = Char nibble nibble
    30   -- "Note: canonical order of character encoding coincides with standard term ordering"
    31 
    32 types string = "char list"
    33 
    34 syntax
    35   "_Char" :: "xstr => char"    ("CHR _")
    36   "_String" :: "xstr => string"    ("_")
    37 
    38 parse_ast_translation {*
    39   let
    40     val constants = Syntax.Appl o map Syntax.Constant;
    41 
    42     fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10));
    43     fun mk_char c =
    44       if Symbol.is_ascii c andalso Symbol.is_printable c then
    45         constants ["Char", mk_nib (ord c div 16), mk_nib (ord c mod 16)]
    46       else error ("Printable ASCII character expected: " ^ quote c);
    47 
    48     fun mk_string [] = Syntax.Constant "Nil"
    49       | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
    50 
    51     fun char_ast_tr [Syntax.Variable xstr] =
    52         (case Syntax.explode_xstr xstr of
    53           [c] => mk_char c
    54         | _ => error ("Single character expected: " ^ xstr))
    55       | char_ast_tr asts = raise AST ("char_ast_tr", asts);
    56 
    57     fun string_ast_tr [Syntax.Variable xstr] =
    58         (case Syntax.explode_xstr xstr of
    59           [] => constants [Syntax.constrainC, "Nil", "string"]
    60         | cs => mk_string cs)
    61       | string_ast_tr asts = raise AST ("string_tr", asts);
    62   in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
    63 *}
    64 
    65 print_ast_translation {*
    66   let
    67     fun dest_nib (Syntax.Constant c) =
    68         (case explode c of
    69           ["N", "i", "b", "b", "l", "e", h] =>
    70             if "0" <= h andalso h <= "9" then ord h - ord "0"
    71             else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
    72             else raise Match
    73         | _ => raise Match)
    74       | dest_nib _ = raise Match;
    75 
    76     fun dest_chr c1 c2 =
    77       let val c = chr (dest_nib c1 * 16 + dest_nib c2)
    78       in if Symbol.is_printable c then c else raise Match end;
    79 
    80     fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
    81       | dest_char _ = raise Match;
    82 
    83     fun xstr cs = Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
    84 
    85     fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", xstr [dest_chr c1 c2]]
    86       | char_ast_tr' _ = raise Match;
    87 
    88     fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
    89             xstr (map dest_char (Syntax.unfold_ast "_args" args))]
    90       | list_ast_tr' ts = raise Match;
    91   in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
    92 *}
    93 
    94 
    95 subsection {* Configuration of the code generator *}
    96 
    97 types_code
    98   "bool"  ("bool")
    99   "*"     ("prod")
   100   "list"  ("list")
   101 
   102 consts_code
   103   "op ="    ("(_ =/ _)")
   104 
   105   "True"    ("true")
   106   "False"   ("false")
   107   "Not"     ("not")
   108   "op |"    ("(_ orelse/ _)")
   109   "op &"    ("(_ andalso/ _)")
   110   "If"      ("(if _/ then _/ else _)")
   111 
   112   "Pair"    ("(_,/ _)")
   113   "fst"     ("fst")
   114   "snd"     ("snd")
   115 
   116   "Nil"     ("[]")
   117   "Cons"    ("(_ ::/ _)")
   118   
   119 end