1 (* Title: Tools/Spec_Check/gen_construction.ML |
|
2 Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen |
|
3 Author: Christopher League |
|
4 |
|
5 Constructing generators and pretty printing function for complex types. |
|
6 *) |
|
7 |
|
8 signature GEN_CONSTRUCTION = |
|
9 sig |
|
10 val register : string * (string * string) -> theory -> theory |
|
11 type mltype |
|
12 val parse_pred : string -> string * mltype |
|
13 val build_check : Proof.context -> string -> mltype * string -> string |
|
14 (*val safe_check : string -> mltype * string -> string*) |
|
15 val string_of_bool : bool -> string |
|
16 val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string |
|
17 end; |
|
18 |
|
19 structure Gen_Construction : GEN_CONSTRUCTION = |
|
20 struct |
|
21 |
|
22 (* Parsing ML types *) |
|
23 |
|
24 datatype mltype = Var | Con of string * mltype list | Tuple of mltype list; |
|
25 |
|
26 (*Split string into tokens for parsing*) |
|
27 fun split s = |
|
28 let |
|
29 fun split_symbol #"(" = "( " |
|
30 | split_symbol #")" = " )" |
|
31 | split_symbol #"," = " ," |
|
32 | split_symbol #":" = " :" |
|
33 | split_symbol c = Char.toString c |
|
34 fun is_space c = c = #" " |
|
35 in String.tokens is_space (String.translate split_symbol s) end; |
|
36 |
|
37 (*Accept anything that is not a recognized symbol*) |
|
38 val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;")); |
|
39 |
|
40 (*Turn a type list into a nested Con*) |
|
41 fun make_con [] = raise Empty |
|
42 | make_con [c] = c |
|
43 | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]); |
|
44 |
|
45 (*Parse a type*) |
|
46 fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s |
|
47 |
|
48 and parse_type_arg s = (parse_tuple || parse_type_single) s |
|
49 |
|
50 and parse_type_single s = (parse_con || parse_type_basic) s |
|
51 |
|
52 and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s |
|
53 |
|
54 and parse_list s = |
|
55 ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s |
|
56 |
|
57 and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s |
|
58 |
|
59 and parse_con s = ((parse_con_nest |
|
60 || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl) |
|
61 || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl)) |
|
62 >> (make_con o rev)) s |
|
63 |
|
64 and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s |
|
65 |
|
66 and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s |
|
67 |
|
68 and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single) |
|
69 >> (fn (t, tl) => Tuple (t :: tl))) s; |
|
70 |
|
71 (*Parse entire type + name*) |
|
72 fun parse_function s = |
|
73 let |
|
74 val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":") |
|
75 val (name, ty) = p (split s) |
|
76 val stop = Scan.stopper (fn _ => ";") (fn s => s = ";"); |
|
77 val (typ, _) = Scan.finite stop parse_type ty |
|
78 in (name, typ) end; |
|
79 |
|
80 (*Create desired output*) |
|
81 fun parse_pred s = |
|
82 let |
|
83 val (name, Con ("->", t :: _)) = parse_function s |
|
84 in (name, t) end; |
|
85 |
|
86 (* Construct Generators and Pretty Printers *) |
|
87 |
|
88 (*copied from smt_config.ML *) |
|
89 fun string_of_bool b = if b then "true" else "false" |
|
90 |
|
91 fun string_of_ref f r = f (!r) ^ " ref"; |
|
92 |
|
93 val initial_content = Symtab.make |
|
94 [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")), |
|
95 ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")), |
|
96 ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")), |
|
97 ("unit", ("gen_unit", "fn () => \"()\"")), |
|
98 ("int", ("Generator.int", "string_of_int")), |
|
99 ("real", ("Generator.real", "string_of_real")), |
|
100 ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")), |
|
101 ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")), |
|
102 ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")), |
|
103 ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")), |
|
104 ("term", ("Generator.term 10", "ML_Syntax.print_term"))] |
|
105 |
|
106 structure Data = Theory_Data |
|
107 ( |
|
108 type T = (string * string) Symtab.table |
|
109 val empty = initial_content |
|
110 val extend = I |
|
111 fun merge data : T = Symtab.merge (K true) data |
|
112 ) |
|
113 |
|
114 fun data_of ctxt tycon = |
|
115 (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of |
|
116 SOME data => data |
|
117 | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon)) |
|
118 |
|
119 val generator_of = fst oo data_of |
|
120 val printer_of = snd oo data_of |
|
121 |
|
122 fun register (ty, data) = Data.map (Symtab.update (ty, data)) |
|
123 |
|
124 (* |
|
125 fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table); |
|
126 *) |
|
127 |
|
128 fun combine dict [] = dict |
|
129 | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts) |
|
130 |
|
131 fun compose_generator _ Var = "Generator.int" |
|
132 | compose_generator ctxt (Con (s, types)) = |
|
133 combine (generator_of ctxt s) (map (compose_generator ctxt) types) |
|
134 | compose_generator ctxt (Tuple t) = |
|
135 let |
|
136 fun tuple_body t = space_implode "" |
|
137 (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^ |
|
138 compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t)))) |
|
139 fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a)) |
|
140 in |
|
141 "fn r0 => let " ^ tuple_body t ^ |
|
142 "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end" |
|
143 end; |
|
144 |
|
145 fun compose_printer _ Var = "Int.toString" |
|
146 | compose_printer ctxt (Con (s, types)) = |
|
147 combine (printer_of ctxt s) (map (compose_printer ctxt) types) |
|
148 | compose_printer ctxt (Tuple t) = |
|
149 let |
|
150 fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a)) |
|
151 fun tuple_body t = space_implode " ^ \", \" ^ " |
|
152 (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n) |
|
153 (t ~~ (1 upto (length t)))) |
|
154 in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end; |
|
155 |
|
156 (*produce compilable string*) |
|
157 fun build_check ctxt name (ty, spec) = |
|
158 "Spec_Check.checkGen (Context.the_local_context ()) (" |
|
159 ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\"" |
|
160 ^ name ^ "\", Property.pred (" ^ spec ^ "));"; |
|
161 |
|
162 (*produce compilable string - non-eqtype functions*) |
|
163 (* |
|
164 fun safe_check name (ty, spec) = |
|
165 let |
|
166 val default = |
|
167 (case AList.lookup (op =) (!gen_table) "->" of |
|
168 NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"") |
|
169 | SOME entry => entry) |
|
170 in |
|
171 (gen_table := |
|
172 AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table); |
|
173 build_check name (ty, spec) before |
|
174 gen_table := AList.update (op =) ("->", default) (!gen_table)) |
|
175 end; |
|
176 *) |
|
177 |
|
178 end; |
|
179 |
|