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