src/Pure/codegen.ML
author berghofe
Tue Sep 27 12:13:17 2005 +0200 (2005-09-27)
changeset 17666 4708ab4626a5
parent 17638 6de497c99e4c
child 18098 227ecb2cfa3d
permissions -rw-r--r--
Optimized unfold_attr.
     1 (*  Title:      Pure/codegen.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Generic code generator.
     6 *)
     7 
     8 signature CODEGEN =
     9 sig
    10   val quiet_mode : bool ref
    11   val message : string -> unit
    12   val mode : string list ref
    13   val margin : int ref
    14 
    15   datatype 'a mixfix =
    16       Arg
    17     | Ignore
    18     | Module
    19     | Pretty of Pretty.T
    20     | Quote of 'a;
    21 
    22   type deftab
    23   type node
    24   type codegr
    25   type 'a codegen
    26 
    27   val add_codegen: string -> term codegen -> theory -> theory
    28   val add_tycodegen: string -> typ codegen -> theory -> theory
    29   val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory
    30   val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
    31   val preprocess: theory -> thm list -> thm list
    32   val preprocess_term: theory -> term -> term
    33   val print_codegens: theory -> unit
    34   val generate_code: theory -> string list -> string -> (string * string) list ->
    35     (string * string) list * codegr
    36   val generate_code_i: theory -> string list -> string -> (string * term) list ->
    37     (string * string) list * codegr
    38   val assoc_consts: (xstring * string option * (term mixfix list *
    39     (string * string) list)) list -> theory -> theory
    40   val assoc_consts_i: (xstring * typ option * (term mixfix list *
    41     (string * string) list)) list -> theory -> theory
    42   val assoc_types: (xstring * (typ mixfix list *
    43     (string * string) list)) list -> theory -> theory
    44   val get_assoc_code: theory -> string -> typ ->
    45     (term mixfix list * (string * string) list) option
    46   val get_assoc_type: theory -> string ->
    47     (typ mixfix list * (string * string) list) option
    48   val codegen_error: codegr -> string -> string -> 'a
    49   val invoke_codegen: theory -> deftab -> string -> string -> bool ->
    50     codegr * term -> codegr * Pretty.T
    51   val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
    52     codegr * typ -> codegr * Pretty.T
    53   val mk_id: string -> string
    54   val mk_qual_id: string -> string * string -> string
    55   val mk_const_id: string -> string -> codegr -> codegr * (string * string)
    56   val get_const_id: string -> codegr -> string * string
    57   val mk_type_id: string -> string -> codegr -> codegr * (string * string)
    58   val get_type_id: string -> codegr -> string * string
    59   val thyname_of_type: string -> theory -> string
    60   val thyname_of_const: string -> theory -> string
    61   val rename_terms: term list -> term list
    62   val rename_term: term -> term
    63   val new_names: term -> string list -> string list
    64   val new_name: term -> string -> string
    65   val if_library: 'a -> 'a -> 'a
    66   val get_defn: theory -> deftab -> string -> typ ->
    67     ((typ * (string * (term list * term))) * int option) option
    68   val is_instance: theory -> typ -> typ -> bool
    69   val parens: Pretty.T -> Pretty.T
    70   val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
    71   val eta_expand: term -> term list -> int -> term
    72   val strip_tname: string -> string
    73   val mk_type: bool -> typ -> Pretty.T
    74   val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
    75   val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
    76   val test_fn: (int -> (string * term) list option) ref
    77   val test_term: theory -> int -> int -> term -> (string * term) list option
    78   val eval_result: term ref
    79   val eval_term: theory -> term -> term
    80   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
    81   val mk_deftab: theory -> deftab
    82 
    83   val get_node: codegr -> string -> node
    84   val add_edge: string * string -> codegr -> codegr
    85   val add_edge_acyclic: string * string -> codegr -> codegr
    86   val del_nodes: string list -> codegr -> codegr
    87   val map_node: string -> (node -> node) -> codegr -> codegr
    88   val new_node: string * node -> codegr -> codegr
    89 end;
    90 
    91 structure Codegen : CODEGEN =
    92 struct
    93 
    94 val quiet_mode = ref true;
    95 fun message s = if !quiet_mode then () else writeln s;
    96 
    97 val mode = ref ([] : string list);
    98 
    99 val margin = ref 80;
   100 
   101 (**** Mixfix syntax ****)
   102 
   103 datatype 'a mixfix =
   104     Arg
   105   | Ignore
   106   | Module
   107   | Pretty of Pretty.T
   108   | Quote of 'a;
   109 
   110 fun is_arg Arg = true
   111   | is_arg Ignore = true
   112   | is_arg _ = false;
   113 
   114 fun quotes_of [] = []
   115   | quotes_of (Quote q :: ms) = q :: quotes_of ms
   116   | quotes_of (_ :: ms) = quotes_of ms;
   117 
   118 fun args_of [] xs = ([], xs)
   119   | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs)
   120   | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
   121   | args_of (_ :: ms) xs = args_of ms xs;
   122 
   123 fun num_args x = length (List.filter is_arg x);
   124 
   125 
   126 (**** theory data ****)
   127 
   128 (* preprocessed definition table *)
   129 
   130 type deftab =
   131   (typ *              (* type of constant *)
   132     (string *         (* name of theory containing definition of constant *)
   133       (term list *    (* parameters *)
   134        term)))        (* right-hand side *)
   135   list Symtab.table;
   136 
   137 (* code dependency graph *)
   138 
   139 type nametab = (string * string) Symtab.table * unit Symtab.table;
   140 
   141 fun merge_nametabs ((tab, used), (tab', used')) =
   142   (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
   143 
   144 type node =
   145   (exn option *    (* slot for arbitrary data *)
   146    string *        (* name of structure containing piece of code *)
   147    string);        (* piece of code *)
   148 
   149 type codegr =
   150   node Graph.T *
   151   (nametab *       (* table for assigned constant names *)
   152    nametab);       (* table for assigned type names *)
   153 
   154 val emptygr : codegr = (Graph.empty,
   155   ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)));
   156 
   157 (* type of code generators *)
   158 
   159 type 'a codegen =
   160   theory ->    (* theory in which generate_code was called *)
   161   deftab ->    (* definition table (for efficiency) *)
   162   codegr ->    (* code dependency graph *)
   163   string ->    (* node name of caller (for recording dependencies) *)
   164   string ->    (* module name of caller (for modular code generation) *)
   165   bool ->      (* whether to parenthesize generated expression *)
   166   'a ->        (* item to generate code from *)
   167   (codegr * Pretty.T) option;
   168 
   169 (* parameters for random testing *)
   170 
   171 type test_params =
   172   {size: int, iterations: int, default_type: typ option};
   173 
   174 fun merge_test_params
   175   {size = size1, iterations = iterations1, default_type = default_type1}
   176   {size = size2, iterations = iterations2, default_type = default_type2} =
   177   {size = Int.max (size1, size2),
   178    iterations = Int.max (iterations1, iterations2),
   179    default_type = case default_type1 of
   180        NONE => default_type2
   181      | _ => default_type1};
   182 
   183 val default_test_params : test_params =
   184   {size = 10, iterations = 100, default_type = NONE};
   185 
   186 fun set_size size ({iterations, default_type, ...} : test_params) =
   187   {size = size, iterations = iterations, default_type = default_type};
   188 
   189 fun set_iterations iterations ({size, default_type, ...} : test_params) =
   190   {size = size, iterations = iterations, default_type = default_type};
   191 
   192 fun set_default_type s thy ({size, iterations, ...} : test_params) =
   193   {size = size, iterations = iterations,
   194    default_type = SOME (typ_of (read_ctyp thy s))};
   195 
   196 (* data kind 'Pure/codegen' *)
   197 
   198 structure CodegenData = TheoryDataFun
   199 (struct
   200   val name = "Pure/codegen";
   201   type T =
   202     {codegens : (string * term codegen) list,
   203      tycodegens : (string * typ codegen) list,
   204      consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
   205      types : (string * (typ mixfix list * (string * string) list)) list,
   206      attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
   207      preprocs: (stamp * (theory -> thm list -> thm list)) list,
   208      modules: codegr Symtab.table,
   209      test_params: test_params};
   210 
   211   val empty =
   212     {codegens = [], tycodegens = [], consts = [], types = [], attrs = [],
   213      preprocs = [], modules = Symtab.empty, test_params = default_test_params};
   214   val copy = I;
   215   val extend = I;
   216 
   217   fun merge _
   218     ({codegens = codegens1, tycodegens = tycodegens1,
   219       consts = consts1, types = types1, attrs = attrs1,
   220       preprocs = preprocs1, modules = modules1, test_params = test_params1},
   221      {codegens = codegens2, tycodegens = tycodegens2,
   222       consts = consts2, types = types2, attrs = attrs2,
   223       preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
   224     {codegens = merge_alists' codegens1 codegens2,
   225      tycodegens = merge_alists' tycodegens1 tycodegens2,
   226      consts = merge_alists consts1 consts2,
   227      types = merge_alists types1 types2,
   228      attrs = merge_alists attrs1 attrs2,
   229      preprocs = merge_alists' preprocs1 preprocs2,
   230      modules = Symtab.merge (K true) (modules1, modules2),
   231      test_params = merge_test_params test_params1 test_params2};
   232 
   233   fun print _ ({codegens, tycodegens, ...} : T) =
   234     Pretty.writeln (Pretty.chunks
   235       [Pretty.strs ("term code generators:" :: map fst codegens),
   236        Pretty.strs ("type code generators:" :: map fst tycodegens)]);
   237 end);
   238 
   239 val _ = Context.add_setup [CodegenData.init];
   240 val print_codegens = CodegenData.print;
   241 
   242 
   243 (**** access parameters for random testing ****)
   244 
   245 fun get_test_params thy = #test_params (CodegenData.get thy);
   246 
   247 fun map_test_params f thy =
   248   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   249     CodegenData.get thy;
   250   in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
   251     consts = consts, types = types, attrs = attrs, preprocs = preprocs,
   252     modules = modules, test_params = f test_params} thy
   253   end;
   254 
   255 
   256 (**** access modules ****)
   257 
   258 fun get_modules thy = #modules (CodegenData.get thy);
   259 
   260 fun map_modules f thy =
   261   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   262     CodegenData.get thy;
   263   in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
   264     consts = consts, types = types, attrs = attrs, preprocs = preprocs,
   265     modules = f modules, test_params = test_params} thy
   266   end;
   267 
   268 
   269 (**** add new code generators to theory ****)
   270 
   271 fun add_codegen name f thy =
   272   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   273     CodegenData.get thy
   274   in (case AList.lookup (op =) codegens name of
   275       NONE => CodegenData.put {codegens = (name, f) :: codegens,
   276         tycodegens = tycodegens, consts = consts, types = types,
   277         attrs = attrs, preprocs = preprocs, modules = modules,
   278         test_params = test_params} thy
   279     | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   280   end;
   281 
   282 fun add_tycodegen name f thy =
   283   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   284     CodegenData.get thy
   285   in (case AList.lookup (op =) tycodegens name of
   286       NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
   287         codegens = codegens, consts = consts, types = types,
   288         attrs = attrs, preprocs = preprocs, modules = modules,
   289         test_params = test_params} thy
   290     | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   291   end;
   292 
   293 
   294 (**** code attribute ****)
   295 
   296 fun add_attribute name att thy =
   297   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   298     CodegenData.get thy
   299   in (case AList.lookup (op =) attrs name of
   300       NONE => CodegenData.put {tycodegens = tycodegens,
   301         codegens = codegens, consts = consts, types = types,
   302         attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
   303         preprocs = preprocs, modules = modules,
   304         test_params = test_params} thy
   305     | SOME _ => error ("Code attribute " ^ name ^ " already declared"))
   306   end;
   307 
   308 fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
   309 
   310 val code_attr =
   311   Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
   312     (#attrs (CodegenData.get thy)))));
   313 
   314 val _ = Context.add_setup
   315  [Attrib.add_attributes
   316   [("code", (code_attr, K Attrib.undef_local_attribute),
   317      "declare theorems for code generation")]];
   318 
   319 
   320 (**** preprocessors ****)
   321 
   322 fun add_preprocessor p thy =
   323   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   324     CodegenData.get thy
   325   in CodegenData.put {tycodegens = tycodegens,
   326     codegens = codegens, consts = consts, types = types,
   327     attrs = attrs, preprocs = (stamp (), p) :: preprocs,
   328     modules = modules, test_params = test_params} thy
   329   end;
   330 
   331 fun preprocess thy ths =
   332   let val {preprocs, ...} = CodegenData.get thy
   333   in Library.foldl (fn (ths, (_, f)) => f thy ths) (ths, preprocs) end;
   334 
   335 fun preprocess_term thy t =
   336   let
   337     val x = Free (variant (add_term_names (t, [])) "x", fastype_of t);
   338     (* fake definition *)
   339     val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
   340       (Logic.mk_equals (x, t));
   341     fun err () = error "preprocess_term: bad preprocessor"
   342   in case map prop_of (preprocess thy [eq]) of
   343       [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
   344     | _ => err ()
   345   end;
   346     
   347 fun unfold_attr (thy, eqn) =
   348   let
   349     val names = term_consts
   350       (fst (Logic.dest_equals (prop_of eqn)));
   351     fun prep thy = map (fn th =>
   352       let val prop = prop_of th
   353       in
   354         if forall (fn name => exists_Const (equal name o fst) prop) names
   355         then rewrite_rule [eqn] (Thm.transfer thy th)
   356         else th
   357       end)
   358   in (add_preprocessor prep thy, eqn) end;
   359 
   360 val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];
   361 
   362 
   363 (**** associate constants with target language code ****)
   364 
   365 fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
   366   let
   367     val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   368       CodegenData.get thy;
   369     val cname = Sign.intern_const thy s;
   370   in
   371     (case Sign.const_type thy cname of
   372        SOME T =>
   373          let val T' = (case tyopt of
   374                 NONE => T
   375               | SOME ty =>
   376                   let val U = prep_type thy ty
   377                   in if Sign.typ_instance thy (U, T) then U
   378                     else error ("Illegal type constraint for constant " ^ cname)
   379                   end)
   380          in (case AList.lookup (op =) consts (cname, T') of
   381              NONE => CodegenData.put {codegens = codegens,
   382                tycodegens = tycodegens,
   383                consts = ((cname, T'), syn) :: consts,
   384                types = types, attrs = attrs, preprocs = preprocs,
   385                modules = modules, test_params = test_params} thy
   386            | SOME _ => error ("Constant " ^ cname ^ " already associated with code"))
   387          end
   388      | _ => error ("Not a constant: " ^ s))
   389   end) (thy, xs);
   390 
   391 val assoc_consts_i = gen_assoc_consts (K I);
   392 val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp);
   393 
   394 
   395 (**** associate types with target language types ****)
   396 
   397 fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>
   398   let
   399     val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   400       CodegenData.get thy;
   401     val tc = Sign.intern_type thy s
   402   in
   403     (case AList.lookup (op =) types tc of
   404        NONE => CodegenData.put {codegens = codegens,
   405          tycodegens = tycodegens, consts = consts,
   406          types = (tc, syn) :: types, attrs = attrs,
   407          preprocs = preprocs, modules = modules, test_params = test_params} thy
   408      | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
   409   end) (thy, xs);
   410 
   411 fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s;
   412 
   413 
   414 (**** make valid ML identifiers ****)
   415 
   416 fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
   417   Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
   418 
   419 fun dest_sym s = (case split_last (snd (take_prefix (equal "\\") (explode s))) of
   420     ("<" :: "^" :: xs, ">") => (true, implode xs)
   421   | ("<" :: xs, ">") => (false, implode xs)
   422   | _ => sys_error "dest_sym");
   423 
   424 fun mk_id s = if s = "" then "" else
   425   let
   426     fun check_str [] = []
   427       | check_str xs = (case take_prefix is_ascii_letdig xs of
   428           ([], " " :: zs) => check_str zs
   429         | ([], z :: zs) =>
   430           if size z = 1 then string_of_int (ord z) :: check_str zs
   431           else (case dest_sym z of
   432               (true, "isub") => check_str zs
   433             | (true, "isup") => "" :: check_str zs
   434             | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
   435         | (ys, zs) => implode ys :: check_str zs);
   436     val s' = space_implode "_"
   437       (List.concat (map (check_str o Symbol.explode) (NameSpace.unpack s)))
   438   in
   439     if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   440   end;
   441 
   442 fun mk_long_id (p as (tab, used)) module s =
   443   let
   444     fun find_name [] = sys_error "mk_long_id"
   445       | find_name (ys :: yss) =
   446           let
   447             val s' = NameSpace.pack ys
   448             val s'' = NameSpace.append module s'
   449           in case Symtab.lookup used s'' of
   450               NONE => ((module, s'),
   451                 (Symtab.update_new (s, (module, s')) tab,
   452                  Symtab.update_new (s'', ()) used))
   453             | SOME _ => find_name yss
   454           end
   455   in case Symtab.lookup tab s of
   456       NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
   457     | SOME name => (name, p)
   458   end;
   459 
   460 (* module:  module name for caller                                        *)
   461 (* module': module name for callee                                        *)
   462 (* if caller and callee reside in different modules, use qualified access *)
   463 
   464 fun mk_qual_id module (module', s) =
   465   if module = module' orelse module' = "" then s else module' ^ "." ^ s;
   466 
   467 fun mk_const_id module cname (gr, (tab1, tab2)) =
   468   let
   469     val ((module, s), tab1') = mk_long_id tab1 module cname
   470     val s' = mk_id s;
   471     val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s'
   472   in ((gr, (tab1', tab2)), (module, s'')) end;
   473 
   474 fun get_const_id cname (gr, (tab1, tab2)) =
   475   case Symtab.lookup (fst tab1) cname of
   476     NONE => error ("get_const_id: no such constant: " ^ quote cname)
   477   | SOME (module, s) =>
   478       let
   479         val s' = mk_id s;
   480         val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s'
   481       in (module, s'') end;
   482 
   483 fun mk_type_id module tyname (gr, (tab1, tab2)) =
   484   let
   485     val ((module, s), tab2') = mk_long_id tab2 module tyname
   486     val s' = mk_id s;
   487     val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s'
   488   in ((gr, (tab1, tab2')), (module, s'')) end;
   489 
   490 fun get_type_id tyname (gr, (tab1, tab2)) =
   491   case Symtab.lookup (fst tab2) tyname of
   492     NONE => error ("get_type_id: no such type: " ^ quote tyname)
   493   | SOME (module, s) =>
   494       let
   495         val s' = mk_id s;
   496         val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s'
   497       in (module, s'') end;
   498 
   499 fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab);
   500 
   501 fun get_node (gr, x) k = Graph.get_node gr k;
   502 fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
   503 fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x);
   504 fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x);
   505 fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
   506 fun new_node p (gr, x) = (Graph.new_node p gr, x);
   507 
   508 fun theory_of_type s thy = 
   509   if Sign.declared_tyname thy s
   510   then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy)
   511   else NONE;
   512 
   513 fun theory_of_const s thy = 
   514   if Sign.declared_const thy s
   515   then SOME (if_none (get_first (theory_of_const s) (Theory.parents_of thy)) thy)
   516   else NONE;
   517 
   518 fun thyname_of_type s thy = (case theory_of_type s thy of
   519     NONE => error ("thyname_of_type: no such type: " ^ quote s)
   520   | SOME thy' => Context.theory_name thy');
   521 
   522 fun thyname_of_const s thy = (case theory_of_const s thy of
   523     NONE => error ("thyname_of_const: no such constant: " ^ quote s)
   524   | SOME thy' => Context.theory_name thy');
   525 
   526 fun rename_terms ts =
   527   let
   528     val names = foldr add_term_names
   529       (map (fst o fst) (Drule.vars_of_terms ts)) ts;
   530     val reserved = names inter ThmDatabase.ml_reserved;
   531     val (illegal, alt_names) = split_list (List.mapPartial (fn s =>
   532       let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
   533     val ps = (reserved @ illegal) ~~
   534       variantlist (map (suffix "'") reserved @ alt_names, names);
   535 
   536     fun rename_id s = AList.lookup (op =) ps s |> the_default s;
   537 
   538     fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
   539       | rename (Free (a, T)) = Free (rename_id a, T)
   540       | rename (Abs (s, T, t)) = Abs (s, T, rename t)
   541       | rename (t $ u) = rename t $ rename u
   542       | rename t = t;
   543   in
   544     map rename ts
   545   end;
   546 
   547 val rename_term = hd o rename_terms o single;
   548 
   549 
   550 (**** retrieve definition of constant ****)
   551 
   552 fun is_instance thy T1 T2 =
   553   Sign.typ_instance thy (T1, Type.varifyT T2);
   554 
   555 fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
   556   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   557 
   558 fun get_aux_code xs = List.mapPartial (fn (m, code) =>
   559   if m = "" orelse m mem !mode then SOME code else NONE) xs;
   560 
   561 fun mk_deftab thy =
   562   let
   563     val axmss = map (fn thy' =>
   564       (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy'))))
   565       (thy :: Theory.ancestors_of thy);
   566     fun prep_def def = (case preprocess thy [def] of
   567       [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor");
   568     fun dest t =
   569       let
   570         val (lhs, rhs) = Logic.dest_equals t;
   571         val (c, args) = strip_comb lhs;
   572         val (s, T) = dest_Const c
   573       in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
   574       end handle TERM _ => NONE;
   575     fun add_def thyname (defs, (name, t)) = (case dest t of
   576         NONE => defs
   577       | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of
   578           NONE => defs
   579         | SOME (s, (T, (args, rhs))) => Symtab.update
   580             (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
   581             if_none (Symtab.lookup defs s) []) defs))
   582   in
   583     foldl (fn ((thyname, axms), defs) =>
   584       Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
   585   end;
   586 
   587 fun get_defn thy defs s T = (case Symtab.lookup defs s of
   588     NONE => NONE
   589   | SOME ds =>
   590       let val i = find_index (is_instance thy T o fst) ds
   591       in if i >= 0 then
   592           SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i)
   593         else NONE
   594       end);
   595 
   596 
   597 (**** invoke suitable code generator for term / type ****)
   598 
   599 fun codegen_error (gr, _) dep s =
   600   error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
   601 
   602 fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first
   603    (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
   604       NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
   605         Sign.string_of_term thy t)
   606     | SOME x => x);
   607 
   608 fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first
   609    (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
   610       NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
   611         Sign.string_of_typ thy T)
   612     | SOME x => x);
   613 
   614 
   615 (**** code generator for mixfix expressions ****)
   616 
   617 fun parens p = Pretty.block [Pretty.str "(", p, Pretty.str ")"];
   618 
   619 fun pretty_fn [] p = [p]
   620   | pretty_fn (x::xs) p = Pretty.str ("fn " ^ x ^ " =>") ::
   621       Pretty.brk 1 :: pretty_fn xs p;
   622 
   623 fun pretty_mixfix _ _ [] [] _ = []
   624   | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs =
   625       p :: pretty_mixfix module module' ms ps qs
   626   | pretty_mixfix module module' (Ignore :: ms) ps qs =
   627       pretty_mixfix module module' ms ps qs
   628   | pretty_mixfix module module' (Module :: ms) ps qs =
   629       (if module <> module'
   630        then cons (Pretty.str (module' ^ ".")) else I)
   631       (pretty_mixfix module module' ms ps qs)
   632   | pretty_mixfix module module' (Pretty p :: ms) ps qs =
   633       p :: pretty_mixfix module module' ms ps qs
   634   | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
   635       q :: pretty_mixfix module module' ms ps qs;
   636 
   637 
   638 (**** default code generators ****)
   639 
   640 fun eta_expand t ts i =
   641   let
   642     val (Ts, _) = strip_type (fastype_of t);
   643     val j = i - length ts
   644   in
   645     foldr (fn (T, t) => Abs ("x", T, t))
   646       (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
   647   end;
   648 
   649 fun mk_app _ p [] = p
   650   | mk_app brack p ps = if brack then
   651        Pretty.block (Pretty.str "(" ::
   652          separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"])
   653      else Pretty.block (separate (Pretty.brk 1) (p :: ps));
   654 
   655 fun new_names t xs = variantlist (map mk_id xs,
   656   map (fst o fst o dest_Var) (term_vars t) union
   657   add_term_names (t, ThmDatabase.ml_reserved));
   658 
   659 fun new_name t x = hd (new_names t [x]);
   660 
   661 fun if_library x y = if "library" mem !mode then x else y;
   662 
   663 fun default_codegen thy defs gr dep module brack t =
   664   let
   665     val (u, ts) = strip_comb t;
   666     fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack)
   667   in (case u of
   668       Var ((s, i), T) =>
   669         let
   670           val (gr', ps) = codegens true (gr, ts);
   671           val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
   672         in SOME (gr'', mk_app brack (Pretty.str (s ^
   673            (if i=0 then "" else string_of_int i))) ps)
   674         end
   675 
   676     | Free (s, T) =>
   677         let
   678           val (gr', ps) = codegens true (gr, ts);
   679           val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
   680         in SOME (gr'', mk_app brack (Pretty.str s) ps) end
   681 
   682     | Const (s, T) =>
   683       (case get_assoc_code thy s T of
   684          SOME (ms, aux) =>
   685            let val i = num_args ms
   686            in if length ts < i then
   687                default_codegen thy defs gr dep module brack (eta_expand u ts i)
   688              else
   689                let
   690                  val (ts1, ts2) = args_of ms ts;
   691                  val (gr1, ps1) = codegens false (gr, ts1);
   692                  val (gr2, ps2) = codegens true (gr1, ts2);
   693                  val (gr3, ps3) = codegens false (gr2, quotes_of ms);
   694                  val (gr4, _) = invoke_tycodegen thy defs dep module false
   695                    (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
   696                  val (module', suffix) = (case get_defn thy defs s T of
   697                      NONE => (if_library (thyname_of_const s thy) module, "")
   698                    | SOME ((U, (module', _)), NONE) =>
   699                        (if_library module' module, "")
   700                    | SOME ((U, (module', _)), SOME i) =>
   701                        (if_library module' module, " def" ^ string_of_int i));
   702                  val node_id = s ^ suffix;
   703                  fun p module' = mk_app brack (Pretty.block
   704                    (pretty_mixfix module module' ms ps1 ps3)) ps2
   705                in SOME (case try (get_node gr4) node_id of
   706                    NONE => (case get_aux_code aux of
   707                        [] => (gr4, p module)
   708                      | xs => (add_edge (node_id, dep) (new_node
   709                          (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4),
   710                            p module'))
   711                  | SOME (_, module'', _) =>
   712                      (add_edge (node_id, dep) gr4, p module''))
   713                end
   714            end
   715        | NONE => (case get_defn thy defs s T of
   716            NONE => NONE
   717          | SOME ((U, (thyname, (args, rhs))), k) =>
   718              let
   719                val module' = if_library thyname module;
   720                val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
   721                val node_id = s ^ suffix;
   722                val (gr', (ps, def_id)) = codegens true (gr, ts) |>>>
   723                  mk_const_id module' (s ^ suffix);
   724                val p = mk_app brack (Pretty.str (mk_qual_id module def_id)) ps
   725              in SOME (case try (get_node gr') node_id of
   726                  NONE =>
   727                    let
   728                      val _ = message ("expanding definition of " ^ s);
   729                      val (Ts, _) = strip_type T;
   730                      val (args', rhs') =
   731                        if not (null args) orelse null Ts then (args, rhs) else
   732                          let val v = Free (new_name rhs "x", hd Ts)
   733                          in ([v], betapply (rhs, v)) end;
   734                      val (gr1, p') = invoke_codegen thy defs node_id module' false
   735                        (add_edge (node_id, dep)
   736                           (new_node (node_id, (NONE, "", "")) gr'), rhs');
   737                      val (gr2, xs) = codegens false (gr1, args');
   738                      val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T);
   739                      val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U);
   740                    in (map_node node_id (K (NONE, module', Pretty.string_of
   741                        (Pretty.block (separate (Pretty.brk 1)
   742                          (if null args' then
   743                             [Pretty.str ("val " ^ snd def_id ^ " :"), ty]
   744                           else Pretty.str ("fun " ^ snd def_id) :: xs) @
   745                         [Pretty.str " =", Pretty.brk 1, p', Pretty.str ";"])) ^ "\n\n")) gr4,
   746                      p)
   747                    end
   748                | SOME _ => (add_edge (node_id, dep) gr', p))
   749              end))
   750 
   751     | Abs _ =>
   752       let
   753         val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
   754         val t = strip_abs_body u
   755         val bs' = new_names t bs;
   756         val (gr1, ps) = codegens true (gr, ts);
   757         val (gr2, p) = invoke_codegen thy defs dep module false
   758           (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
   759       in
   760         SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @
   761           [Pretty.str ")"])) ps)
   762       end
   763 
   764     | _ => NONE)
   765   end;
   766 
   767 fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) =
   768       SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i)))
   769   | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
   770       SOME (gr, Pretty.str s)
   771   | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   772       (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
   773          NONE => NONE
   774        | SOME (ms, aux) =>
   775            let
   776              val (gr', ps) = foldl_map
   777                (invoke_tycodegen thy defs dep module false)
   778                (gr, fst (args_of ms Ts));
   779              val (gr'', qs) = foldl_map
   780                (invoke_tycodegen thy defs dep module false)
   781                (gr', quotes_of ms);
   782              val module' = if_library (thyname_of_type s thy) module;
   783              val node_id = s ^ " (type)";
   784              fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
   785            in SOME (case try (get_node gr'') node_id of
   786                NONE => (case get_aux_code aux of
   787                    [] => (gr'', p module')
   788                  | xs => (fst (mk_type_id module' s
   789                        (add_edge (node_id, dep) (new_node (node_id,
   790                          (NONE, module', space_implode "\n" xs ^ "\n")) gr''))),
   791                      p module'))
   792              | SOME (_, module'', _) =>
   793                  (add_edge (node_id, dep) gr'', p module''))
   794            end);
   795 
   796 val _ = Context.add_setup
   797  [add_codegen "default" default_codegen,
   798   add_tycodegen "default" default_tycodegen];
   799 
   800 
   801 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
   802 
   803 fun add_to_module name s = AList.map_entry (op =) name (suffix s);
   804 
   805 fun output_code gr module xs =
   806   let
   807     val code = List.mapPartial (fn s =>
   808       let val c as (_, module', _) = Graph.get_node gr s
   809       in if module = "" orelse module = module' then SOME (s, c) else NONE end)
   810         (rev (Graph.all_preds gr xs));
   811     fun string_of_cycle (a :: b :: cs) =
   812           let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
   813             if a = a' then Option.map (pair x)
   814               (find_first (equal b o #2 o Graph.get_node gr)
   815                 (Graph.imm_succs gr x))
   816             else NONE) code
   817           in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
   818       | string_of_cycle _ = ""
   819   in
   820     if module = "" then
   821       let
   822         val modules = distinct (map (#2 o snd) code);
   823         val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
   824           (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
   825           (List.concat (map (fn (s, (_, module, _)) => map (pair module)
   826             (filter_out (equal module) (map (#2 o Graph.get_node gr)
   827               (Graph.imm_succs gr s)))) code));
   828         val modules' =
   829           rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
   830       in
   831         foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
   832           (map (rpair "") modules') code
   833       end handle Graph.CYCLES (cs :: _) =>
   834         error ("Cyclic dependency of modules:\n" ^ commas cs ^
   835           "\n" ^ string_of_cycle cs)
   836     else [(module, implode (map (#3 o snd) code))]
   837   end;
   838 
   839 fun gen_generate_code prep_term thy modules module =
   840   setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
   841   let
   842     val _ = assert (module <> "" orelse
   843         "library" mem !mode andalso forall (equal "" o fst) xs)
   844       "missing module name";
   845     val graphs = get_modules thy;
   846     val defs = mk_deftab thy;
   847     val gr = new_node ("<Top>", (NONE, module, ""))
   848       (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
   849         (Graph.merge (fn ((_, module, _), (_, module', _)) =>
   850            module = module') (gr, gr'),
   851          (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
   852            (map (fn s => case Symtab.lookup graphs s of
   853                 NONE => error ("Undefined code module: " ^ s)
   854               | SOME gr => gr) modules))
   855       handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks);
   856     fun expand (t as Abs _) = t
   857       | expand t = (case fastype_of t of
   858           Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
   859     val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   860       (invoke_codegen thy defs "<Top>" module false (gr, t)))
   861         (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs);
   862     val code = List.mapPartial
   863       (fn ("", _) => NONE
   864         | (s', p) => SOME (Pretty.string_of (Pretty.block
   865           [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps;
   866     val code' = space_implode "\n\n" code ^ "\n\n";
   867     val code'' =
   868       List.mapPartial (fn (name, s) =>
   869           if "library" mem !mode andalso name = module andalso null code
   870           then NONE
   871           else SOME (name, mk_struct name s))
   872         ((if null code then I
   873           else add_to_module module code')
   874            (output_code (fst gr') (if_library "" module) ["<Top>"]))
   875   in
   876     (code'', del_nodes ["<Top>"] gr')
   877   end));
   878 
   879 val generate_code_i = gen_generate_code (K I);
   880 val generate_code = gen_generate_code
   881   (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT);
   882 
   883 
   884 (**** Reflection ****)
   885 
   886 val strip_tname = implode o tl o explode;
   887 
   888 fun pretty_list xs = Pretty.block (Pretty.str "[" ::
   889   List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
   890   [Pretty.str "]"]);
   891 
   892 fun mk_type p (TVar ((s, i), _)) = Pretty.str
   893       (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T")
   894   | mk_type p (TFree (s, _)) = Pretty.str (strip_tname s ^ "T")
   895   | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   896       [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","),
   897        Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]);
   898 
   899 fun mk_term_of gr module p (TVar ((s, i), _)) = Pretty.str
   900       (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
   901   | mk_term_of gr module p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   902   | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
   903       (Pretty.block (separate (Pretty.brk 1)
   904         (Pretty.str (mk_qual_id module
   905           (get_type_id' (fn s' => "term_of_" ^ s') s gr)) ::
   906         List.concat (map (fn T =>
   907           [mk_term_of gr module true T, mk_type true T]) Ts))));
   908 
   909 
   910 (**** Test data generators ****)
   911 
   912 fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str
   913       (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
   914   | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   915   | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I)
   916       (Pretty.block (separate (Pretty.brk 1)
   917         (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
   918           (if s mem xs then "'" else "")) ::
   919          map (mk_gen gr module true xs a) Ts @
   920          (if s mem xs then [Pretty.str a] else []))));
   921 
   922 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
   923 
   924 fun test_term thy sz i t =
   925   let
   926     val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
   927       "Term to be tested contains type variables";
   928     val _ = assert (null (term_vars t))
   929       "Term to be tested contains schematic variables";
   930     val frees = map dest_Free (term_frees t);
   931     val frees' = frees ~~
   932       map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
   933     val (code, gr) = setmp mode ["term_of", "test"]
   934       (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
   935     val s = setmp print_mode [] (fn () => "structure TestTerm =\nstruct\n\n" ^
   936       space_implode "\n" (map snd code) ^
   937       "\nopen Generated;\n\n" ^ Pretty.string_of
   938         (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
   939           Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1,
   940           Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
   941             Pretty.blk (0, separate Pretty.fbrk (map (fn ((s, T), s') =>
   942               Pretty.block [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1,
   943               mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
   944               Pretty.str "i;"]) frees')),
   945             Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
   946             Pretty.block [Pretty.str "if ",
   947               mk_app false (Pretty.str "testf") (map (Pretty.str o snd) frees'),
   948               Pretty.brk 1, Pretty.str "then NONE",
   949               Pretty.brk 1, Pretty.str "else ",
   950               Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" ::
   951                 List.concat (separate [Pretty.str ",", Pretty.brk 1]
   952                   (map (fn ((s, T), s') => [Pretty.block
   953                     [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
   954                      mk_app false (mk_term_of gr "Generated" false T)
   955                        [Pretty.str s'], Pretty.str ")"]]) frees')) @
   956                   [Pretty.str "]"])]],
   957             Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
   958       "\n\nend;\n") ();
   959     val _ = use_text Context.ml_output false s;
   960     fun iter f k = if k > i then NONE
   961       else (case (f () handle Match =>
   962           (warning "Exception Match raised in generated code"; NONE)) of
   963         NONE => iter f (k+1) | SOME x => SOME x);
   964     fun test k = if k > sz then NONE
   965       else (priority ("Test data size: " ^ string_of_int k);
   966         case iter (fn () => !test_fn k) 1 of
   967           NONE => test (k+1) | SOME x => SOME x);
   968   in test 0 end;
   969 
   970 fun test_goal ({size, iterations, default_type}, tvinsts) i st =
   971   let
   972     val thy = Toplevel.theory_of st;
   973     fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
   974       | strip t = t;
   975     val (gi, frees) = Logic.goal_params
   976       (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
   977     val gi' = ObjectLogic.atomize_term thy (map_term_types
   978       (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
   979         getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
   980   in case test_term (Toplevel.theory_of st) size iterations gi' of
   981       NONE => writeln "No counterexamples found."
   982     | SOME cex => writeln ("Counterexample found:\n" ^
   983         Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
   984           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
   985             Sign.pretty_term thy t]) cex)))
   986   end;
   987 
   988 
   989 (**** Evaluator for terms ****)
   990 
   991 val eval_result = ref (Bound 0);
   992 
   993 fun eval_term thy = setmp print_mode [] (fn t =>
   994   let
   995     val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
   996       "Term to be evaluated contains type variables";
   997     val _ = assert (null (term_vars t) andalso null (term_frees t))
   998       "Term to be evaluated contains variables";
   999     val (code, gr) = setmp mode ["term_of"]
  1000       (generate_code_i thy [] "Generated") [("result", t)];
  1001     val s = "structure EvalTerm =\nstruct\n\n" ^
  1002       space_implode "\n" (map snd code) ^
  1003       "\nopen Generated;\n\n" ^ Pretty.string_of
  1004         (Pretty.block [Pretty.str "val () = Codegen.eval_result :=",
  1005           Pretty.brk 1,
  1006           mk_app false (mk_term_of gr "Generated" false (fastype_of t))
  1007             [Pretty.str "result"],
  1008           Pretty.str ";"])  ^
  1009       "\n\nend;\n";
  1010     val _ = use_text Context.ml_output false s
  1011   in !eval_result end);
  1012 
  1013 fun print_evaluated_term s = Toplevel.keep (fn state =>
  1014   let
  1015     val state' = Toplevel.enter_forward_proof state;
  1016     val ctxt = Proof.context_of state';
  1017     val t = eval_term (Proof.theory_of state') (ProofContext.read_term ctxt s);
  1018     val T = Term.type_of t;
  1019   in
  1020     writeln (Pretty.string_of
  1021       (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
  1022         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
  1023   end);
  1024 
  1025 
  1026 (**** Interface ****)
  1027 
  1028 val str = setmp print_mode [] Pretty.str;
  1029 
  1030 fun parse_mixfix rd s =
  1031   (case Scan.finite Symbol.stopper (Scan.repeat
  1032      (   $$ "_" >> K Arg
  1033       || $$ "?" >> K Ignore
  1034       || $$ "\\<module>" >> K Module
  1035       || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
  1036       || $$ "{" |-- $$ "*" |-- Scan.repeat1
  1037            (   $$ "'" |-- Scan.one Symbol.not_eof
  1038             || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
  1039          $$ "*" --| $$ "}" >> (Quote o rd o implode)
  1040       || Scan.repeat1
  1041            (   $$ "'" |-- Scan.one Symbol.not_eof
  1042             || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
  1043                  (Scan.one Symbol.not_eof)) >> (Pretty o str o implode)))
  1044        (Symbol.explode s) of
  1045      (p, []) => p
  1046    | _ => error ("Malformed annotation: " ^ quote s));
  1047 
  1048 val _ = Context.add_setup
  1049   [assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
  1050      [("term_of",
  1051        "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
  1052       ("test",
  1053        "fun gen_fun_type _ G i =\n\
  1054        \  let\n\
  1055        \    val f = ref (fn x => raise ERROR);\n\
  1056        \    val _ = (f := (fn x =>\n\
  1057        \      let\n\
  1058        \        val y = G i;\n\
  1059        \        val f' = !f\n\
  1060        \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
  1061        \  in (fn x => !f x) end;\n")]))]];
  1062 
  1063 
  1064 structure P = OuterParse and K = OuterKeyword;
  1065 
  1066 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
  1067   (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
  1068 
  1069 val parse_attach = Scan.repeat (P.$$$ "attach" |--
  1070   Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
  1071     (P.verbatim >> strip_whitespace));
  1072 
  1073 val assoc_typeP =
  1074   OuterSyntax.command "types_code"
  1075   "associate types with target language types" K.thy_decl
  1076     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
  1077      (fn xs => Toplevel.theory (fn thy => assoc_types
  1078        (map (fn ((name, mfx), aux) => (name, (parse_mixfix
  1079          (typ_of o read_ctyp thy) mfx, aux))) xs) thy)));
  1080 
  1081 val assoc_constP =
  1082   OuterSyntax.command "consts_code"
  1083   "associate constants with target language code" K.thy_decl
  1084     (Scan.repeat1
  1085        (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
  1086         P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
  1087      (fn xs => Toplevel.theory (fn thy => assoc_consts
  1088        (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix
  1089          (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux)))
  1090            xs) thy)));
  1091 
  1092 fun parse_code lib =
  1093   Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
  1094   (if lib then Scan.optional P.name "" else P.name) --
  1095   Scan.option (P.$$$ "file" |-- P.name) --
  1096   (if lib then Scan.succeed []
  1097    else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --|
  1098   P.$$$ "contains" --
  1099   (   Scan.repeat1 (P.name --| P.$$$ "=" -- P.term)
  1100    || Scan.repeat1 (P.term >> pair "")) >>
  1101   (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
  1102      let
  1103        val mode'' = if lib then "library" ins (mode' \ "library")
  1104          else mode' \ "library";
  1105        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
  1106      in ((case opt_fname of
  1107          NONE => use_text Context.ml_output false
  1108            (space_implode "\n" (map snd code))
  1109        | SOME fname =>
  1110            if lib then
  1111              app (fn (name, s) => File.write
  1112                  (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
  1113                (("ROOT", implode (map (fn (name, _) =>
  1114                    "use \"" ^ name ^ ".ML\";\n") code)) :: code)
  1115            else File.write (Path.unpack fname) (snd (hd code)));
  1116            if lib then thy
  1117            else map_modules (Symtab.update (module, gr)) thy)
  1118      end));
  1119 
  1120 val code_libraryP =
  1121   OuterSyntax.command "code_library"
  1122     "generates code for terms (one structure for each theory)" K.thy_decl
  1123     (parse_code true);
  1124 
  1125 val code_moduleP =
  1126   OuterSyntax.command "code_module"
  1127     "generates code for terms (single structure, incremental)" K.thy_decl
  1128     (parse_code false);
  1129 
  1130 val params =
  1131   [("size", P.nat >> (K o set_size)),
  1132    ("iterations", P.nat >> (K o set_iterations)),
  1133    ("default_type", P.typ >> set_default_type)];
  1134 
  1135 val parse_test_params = P.short_ident :-- (fn s =>
  1136   P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
  1137 
  1138 fun parse_tyinst xs =
  1139   (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
  1140     fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs;
  1141 
  1142 fun app [] x = x
  1143   | app (f :: fs) x = app fs (f x);
  1144 
  1145 val test_paramsP =
  1146   OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
  1147     (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
  1148       (fn fs => Toplevel.theory (fn thy =>
  1149          map_test_params (app (map (fn f => f thy) fs)) thy)));
  1150 
  1151 val testP =
  1152   OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
  1153   (Scan.option (P.$$$ "[" |-- P.list1
  1154     (   parse_test_params >> (fn f => fn thy => apfst (f thy))
  1155      || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
  1156     (fn (ps, g) => Toplevel.keep (fn st =>
  1157       test_goal (app (getOpt (Option.map
  1158           (map (fn f => f (Toplevel.sign_of st))) ps, []))
  1159         (get_test_params (Toplevel.theory_of st), [])) g st)));
  1160 
  1161 val valueP =
  1162   OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
  1163     (P.term >> (Toplevel.no_timing oo print_evaluated_term));
  1164 
  1165 val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
  1166 
  1167 val _ = OuterSyntax.add_parsers
  1168   [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
  1169 
  1170 end;