74189
|
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 |
|