2540 | cs => mk_string cs) |
2540 | cs => mk_string cs) |
2541 | string_ast_tr asts = raise AST ("string_tr", asts); |
2541 | string_ast_tr asts = raise AST ("string_tr", asts); |
2542 in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end; |
2542 in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end; |
2543 *} |
2543 *} |
2544 |
2544 |
2545 ML {* |
|
2546 structure HOList = |
|
2547 struct |
|
2548 |
|
2549 local |
|
2550 val thy = the_context (); |
|
2551 in |
|
2552 val typ_string = Type (Sign.intern_type thy "string", []); |
|
2553 fun typ_list ty = Type (Sign.intern_type thy "list", [ty]); |
|
2554 fun term_list ty f [] = Const (Sign.intern_const thy "Nil", typ_list ty) |
|
2555 | term_list ty f (x::xs) = Const (Sign.intern_const thy "Cons", |
|
2556 ty --> typ_list ty --> typ_list ty) $ f x $ term_list ty f xs; |
|
2557 end; |
|
2558 |
|
2559 fun int_of_nibble h = |
|
2560 if "0" <= h andalso h <= "9" then ord h - ord "0" |
|
2561 else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10 |
|
2562 else raise Match; |
|
2563 |
|
2564 fun nibble_of_int i = |
|
2565 if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10); |
|
2566 |
|
2567 fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) = |
|
2568 let |
|
2569 fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s |
|
2570 | dest_nibble _ = raise Match; |
|
2571 in |
|
2572 (SOME (dest_nibble c1 * 16 + dest_nibble c2) |
|
2573 handle Fail _ => NONE | Match => NONE) |
|
2574 end |
|
2575 | dest_char _ = NONE; |
|
2576 |
|
2577 val print_list = Pretty.enum "," "[" "]"; |
|
2578 |
|
2579 fun print_char c = |
|
2580 let |
|
2581 val i = ord c |
|
2582 in if i < 32 |
|
2583 then prefix "\\" (string_of_int i) |
|
2584 else c |
|
2585 end; |
|
2586 |
|
2587 val print_string = quote; |
|
2588 |
|
2589 fun term_string s = |
|
2590 let |
|
2591 val ty_n = Type ("List.nibble", []); |
|
2592 val ty_c = Type ("List.char", []); |
|
2593 val ty_l = Type ("List.list", [ty_c]); |
|
2594 fun mk_nib n = Const ("List.nibble.Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10)), ty_n); |
|
2595 fun mk_char c = |
|
2596 if Symbol.is_ascii c andalso Symbol.is_printable c then |
|
2597 Const ("List.char.Char", ty_n --> ty_n --> ty_c) $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16) |
|
2598 else error ("Printable ASCII character expected: " ^ quote c); |
|
2599 fun mk_string c t = Const ("List.list.Cons", ty_c --> ty_l --> ty_l) |
|
2600 $ mk_char c $ t; |
|
2601 in fold_rev mk_string (explode s) (Const ("List.list.Nil", ty_l)) end; |
|
2602 |
|
2603 end; |
|
2604 *} |
|
2605 |
|
2606 print_ast_translation {* |
2545 print_ast_translation {* |
2607 let |
2546 let |
2608 fun dest_nib (Syntax.Constant c) = |
2547 fun dest_nib (Syntax.Constant c) = |
2609 (case explode c of |
2548 (case explode c of |
2610 ["N", "i", "b", "b", "l", "e", h] => HOList.int_of_nibble h |
2549 ["N", "i", "b", "b", "l", "e", h] => HOLogic.int_of_nibble h |
2611 | _ => raise Match) |
2550 | _ => raise Match) |
2612 | dest_nib _ = raise Match; |
2551 | dest_nib _ = raise Match; |
2613 |
2552 |
2614 fun dest_chr c1 c2 = |
2553 fun dest_chr c1 c2 = |
2615 let val c = chr (dest_nib c1 * 16 + dest_nib c2) |
2554 let val c = chr (dest_nib c1 * 16 + dest_nib c2) |
2644 [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] () |
2583 [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] () |
2645 and gen_list aG i = gen_list' aG i i; |
2584 and gen_list aG i = gen_list' aG i i; |
2646 *} |
2585 *} |
2647 "char" ("string") |
2586 "char" ("string") |
2648 attach (term_of) {* |
2587 attach (term_of) {* |
2649 val nibbleT = Type ("List.nibble", []); |
2588 val term_of_char = HOLogic.mk_char; |
2650 |
|
2651 fun term_of_char c = |
|
2652 Const ("List.char.Char", nibbleT --> nibbleT --> Type ("List.char", [])) $ |
|
2653 Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c div 16), nibbleT) $ |
|
2654 Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c mod 16), nibbleT); |
|
2655 *} |
2589 *} |
2656 attach (test) {* |
2590 attach (test) {* |
2657 fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z"))); |
2591 fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z"))); |
2658 *} |
2592 *} |
2659 |
2593 |
2676 (Haskell "!((_),/ (_))") |
2610 (Haskell "!((_),/ (_))") |
2677 |
2611 |
2678 code_instance list :: eq and char :: eq |
2612 code_instance list :: eq and char :: eq |
2679 (Haskell - and -) |
2613 (Haskell - and -) |
2680 |
2614 |
2681 code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool" |
2615 code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool" |
2682 (Haskell infixl 4 "==") |
2616 (Haskell infixl 4 "==") |
2683 |
2617 |
2684 code_const "Code_Generator.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
2618 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
2685 (Haskell infixl 4 "==") |
2619 (Haskell infixl 4 "==") |
2686 |
2620 |
2687 code_reserved SML |
2621 code_reserved SML |
2688 list char |
2622 list char |
2689 |
2623 |
2697 let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false) |
2631 let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false) |
2698 (gr, HOLogic.dest_list t) |
2632 (gr, HOLogic.dest_list t) |
2699 in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE; |
2633 in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE; |
2700 |
2634 |
2701 fun char_codegen thy defs gr dep thyname b t = |
2635 fun char_codegen thy defs gr dep thyname b t = |
2702 case (Option.map chr o HOList.dest_char) t |
2636 case (Option.map chr o HOLogic.dest_char) t |
2703 of SOME c => |
2637 of SOME c => |
2704 if Symbol.is_printable c |
2638 if Symbol.is_printable c |
2705 then SOME (gr, (Pretty.quote o Pretty.str) c) |
2639 then SOME (gr, (Pretty.quote o Pretty.str) c) |
2706 else NONE |
2640 else NONE |
2707 | NONE => NONE; |
2641 | NONE => NONE; |
2709 in |
2643 in |
2710 |
2644 |
2711 Codegen.add_codegen "list_codegen" list_codegen |
2645 Codegen.add_codegen "list_codegen" list_codegen |
2712 #> Codegen.add_codegen "char_codegen" char_codegen |
2646 #> Codegen.add_codegen "char_codegen" char_codegen |
2713 #> CodegenSerializer.add_pretty_list "SML" "List.list.Nil" "List.list.Cons" |
2647 #> CodegenSerializer.add_pretty_list "SML" "List.list.Nil" "List.list.Cons" |
2714 HOList.print_list NONE (7, "::") |
2648 (Pretty.enum "," "[" "]") NONE (7, "::") |
2715 #> CodegenSerializer.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons" |
2649 #> CodegenSerializer.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons" |
2716 HOList.print_list (SOME (HOList.print_char, HOList.print_string)) (5, ":") |
2650 (Pretty.enum "," "[" "]") (SOME (HOLogic.print_char, HOLogic.print_string)) (5, ":") |
2717 #> CodegenPackage.add_appconst |
2651 #> CodegenPackage.add_appconst |
2718 ("List.char.Char", CodegenPackage.appgen_char HOList.dest_char) |
2652 ("List.char.Char", CodegenPackage.appgen_char HOLogic.dest_char) |
2719 |
2653 |
2720 end; |
2654 end; |
2721 *} |
2655 *} |
2722 |
2656 |
2723 |
2657 |