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