src/HOL/Tools/Predicate_Compile/code_prolog.ML
author wenzelm
Thu Aug 26 12:06:00 2010 +0200 (2010-08-26)
changeset 38755 a37d39fe32f8
parent 38735 cb9031a9dccf
child 38797 abe92b33ac9f
permissions -rw-r--r--
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
     1 (*  Title:      HOL/Tools/Predicate_Compile/code_prolog.ML
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 
     4 Prototype of an code generator for logic programming languages (a.k.a. Prolog)
     5 *)
     6 
     7 signature CODE_PROLOG =
     8 sig
     9   type code_options = {ensure_groundness : bool}
    10   val options : code_options ref
    11 
    12   datatype arith_op = Plus | Minus
    13   datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
    14     | Number of int | ArithOp of arith_op * prol_term list;
    15   datatype prem = Conj of prem list
    16     | Rel of string * prol_term list | NotRel of string * prol_term list
    17     | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
    18     | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term
    19     | Ground of string * typ;
    20 
    21   type clause = ((string * prol_term list) * prem);
    22   type logic_program = clause list;
    23   type constant_table = (string * string) list
    24     
    25   val generate : code_options -> Proof.context -> string -> (logic_program * constant_table)
    26   val write_program : logic_program -> string
    27   val run : logic_program -> string -> string list -> int option -> prol_term list list
    28 
    29   val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
    30 
    31   val trace : bool Unsynchronized.ref
    32 end;
    33 
    34 structure Code_Prolog : CODE_PROLOG =
    35 struct
    36 
    37 (* diagnostic tracing *)
    38 
    39 val trace = Unsynchronized.ref false
    40 
    41 fun tracing s = if !trace then Output.tracing s else () 
    42 
    43 (* code generation options *)
    44 
    45 type code_options = {ensure_groundness : bool}
    46 
    47 val options = Unsynchronized.ref {ensure_groundness = false};
    48 
    49 (* general string functions *)
    50 
    51 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    52 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    53 
    54 (* internal program representation *)
    55 
    56 datatype arith_op = Plus | Minus
    57 
    58 datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
    59   | Number of int | ArithOp of arith_op * prol_term list;
    60 
    61 fun dest_Var (Var v) = v
    62 
    63 fun add_vars (Var v) = insert (op =) v
    64   | add_vars (ArithOp (_, ts)) = fold add_vars ts
    65   | add_vars (AppF (_, ts)) = fold add_vars ts
    66   | add_vars _ = I
    67 
    68 fun map_vars f (Var v) = Var (f v)
    69   | map_vars f (ArithOp (opr, ts)) = ArithOp (opr, map (map_vars f) ts)
    70   | map_vars f (AppF (fs, ts)) = AppF (fs, map (map_vars f) ts)
    71   | map_vars f t = t
    72   
    73 fun maybe_AppF (c, []) = Cons c
    74   | maybe_AppF (c, xs) = AppF (c, xs)
    75 
    76 fun is_Var (Var _) = true
    77   | is_Var _ = false
    78 
    79 fun is_arith_term (Var _) = true
    80   | is_arith_term (Number _) = true
    81   | is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands
    82   | is_arith_term _ = false
    83 
    84 fun string_of_prol_term (Var s) = "Var " ^ s
    85   | string_of_prol_term (Cons s) = "Cons " ^ s
    86   | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
    87   | string_of_prol_term (Number n) = "Number " ^ string_of_int n
    88 
    89 datatype prem = Conj of prem list
    90   | Rel of string * prol_term list | NotRel of string * prol_term list
    91   | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
    92   | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term
    93   | Ground of string * typ;
    94 
    95 fun dest_Rel (Rel (c, ts)) = (c, ts)
    96 
    97 fun map_term_prem f (Conj prems) = Conj (map (map_term_prem f) prems)
    98   | map_term_prem f (Rel (r, ts)) = Rel (r, map f ts)
    99   | map_term_prem f (NotRel (r, ts)) = NotRel (r, map f ts)
   100   | map_term_prem f (Eq (l, r)) = Eq (f l, f r)
   101   | map_term_prem f (NotEq (l, r)) = NotEq (f l, f r)
   102   | map_term_prem f (ArithEq (l, r)) = ArithEq (f l, f r)
   103   | map_term_prem f (NotArithEq (l, r)) = NotArithEq (f l, f r)
   104   | map_term_prem f (Ground (v, T)) = Ground (dest_Var (f (Var v)), T)
   105 
   106 fun fold_prem_terms f (Conj prems) = fold (fold_prem_terms f) prems
   107   | fold_prem_terms f (Rel (_, ts)) = fold f ts
   108   | fold_prem_terms f (NotRel (_, ts)) = fold f ts
   109   | fold_prem_terms f (Eq (l, r)) = f l #> f r
   110   | fold_prem_terms f (NotEq (l, r)) = f l #> f r
   111   | fold_prem_terms f (ArithEq (l, r)) = f l #> f r
   112   | fold_prem_terms f (NotArithEq (l, r)) = f l #> f r
   113   | fold_prem_terms f (Ground (v, T)) = f (Var v)
   114   
   115 type clause = ((string * prol_term list) * prem);
   116 
   117 type logic_program = clause list;
   118 
   119 (* translation from introduction rules to internal representation *)
   120 
   121 (** constant table **)
   122 
   123 type constant_table = (string * string) list
   124 
   125 (* assuming no clashing *)
   126 fun mk_constant_table consts =
   127   AList.make (first_lower o Long_Name.base_name) consts
   128 
   129 fun declare_consts consts constant_table =
   130   fold (fn c => AList.update (op =) (c, first_lower (Long_Name.base_name c))) consts constant_table
   131   
   132 fun translate_const constant_table c =
   133   case AList.lookup (op =) constant_table c of
   134     SOME c' => c'
   135   | NONE => error ("No such constant: " ^ c)
   136 
   137 fun inv_lookup _ [] _ = NONE
   138   | inv_lookup eq ((key, value)::xs) value' =
   139       if eq (value', value) then SOME key
   140       else inv_lookup eq xs value';
   141 
   142 fun restore_const constant_table c =
   143   case inv_lookup (op =) constant_table c of
   144     SOME c' => c'
   145   | NONE => error ("No constant corresponding to "  ^ c)
   146 
   147 (** translation of terms, literals, premises, and clauses **)
   148 
   149 fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus
   150   | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
   151   | translate_arith_const _ = NONE
   152 
   153 fun mk_nat_term constant_table n =
   154   let
   155     val zero = translate_const constant_table @{const_name "Groups.zero_class.zero"}
   156     val Suc = translate_const constant_table @{const_name "Suc"}
   157   in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end
   158 
   159 fun translate_term ctxt constant_table t =
   160   case try HOLogic.dest_number t of
   161     SOME (@{typ "int"}, n) => Number n
   162   | SOME (@{typ "nat"}, n) => mk_nat_term constant_table n
   163   | NONE =>
   164       (case strip_comb t of
   165         (Free (v, T), []) => Var v 
   166       | (Const (c, _), []) => Cons (translate_const constant_table c)
   167       | (Const (c, _), args) =>
   168         (case translate_arith_const c of
   169           SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
   170         | NONE =>                                                             
   171             AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
   172       | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
   173 
   174 fun translate_literal ctxt constant_table t =
   175   case strip_comb t of
   176     (Const (@{const_name "op ="}, _), [l, r]) =>
   177       let
   178         val l' = translate_term ctxt constant_table l
   179         val r' = translate_term ctxt constant_table r
   180       in
   181         (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r')
   182       end
   183   | (Const (c, _), args) =>
   184       Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
   185   | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
   186 
   187 fun NegRel_of (Rel lit) = NotRel lit
   188   | NegRel_of (Eq eq) = NotEq eq
   189   | NegRel_of (ArithEq eq) = NotArithEq eq
   190 
   191 fun mk_groundness_prems t = map Ground (Term.add_frees t [])
   192   
   193 fun translate_prem options ctxt constant_table t =  
   194     case try HOLogic.dest_not t of
   195       SOME t =>
   196         if #ensure_groundness options then
   197           Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
   198         else
   199           NegRel_of (translate_literal ctxt constant_table t)
   200     | NONE => translate_literal ctxt constant_table t
   201     
   202 fun imp_prems_conv cv ct =
   203   case Thm.term_of ct of
   204     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   205   | _ => Conv.all_conv ct
   206 
   207 fun Trueprop_conv cv ct =
   208   case Thm.term_of ct of
   209     Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
   210   | _ => raise Fail "Trueprop_conv"
   211 
   212 fun preprocess_intro thy rule =
   213   Conv.fconv_rule
   214     (imp_prems_conv
   215       (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
   216     (Thm.transfer thy rule)
   217 
   218 fun translate_intros options ctxt gr const constant_table =
   219   let
   220     val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
   221     val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
   222     val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
   223       |> declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}]
   224     fun translate_intro intro =
   225       let
   226         val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
   227         val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
   228         val prems' = Conj (map (translate_prem options ctxt' constant_table') prems)
   229         val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
   230       in clause end
   231   in (map translate_intro intros', constant_table') end
   232 
   233 val preprocess_options = Predicate_Compile_Aux.Options {
   234   expected_modes = NONE,
   235   proposed_modes = NONE,
   236   proposed_names = [],
   237   show_steps = false,
   238   show_intermediate_results = false,
   239   show_proof_trace = false,
   240   show_modes = false,
   241   show_mode_inference = false,
   242   show_compilation = false,
   243   show_caught_failures = false,
   244   skip_proof = true,
   245   no_topmost_reordering = false,
   246   function_flattening = true,
   247   specialise = false,
   248   fail_safe_function_flattening = false,
   249   no_higher_order_predicate = [],
   250   inductify = false,
   251   detect_switches = true,
   252   compilation = Predicate_Compile_Aux.Pred
   253 }
   254 
   255 fun depending_preds_of (key, intros) =
   256   fold Term.add_const_names (map Thm.prop_of intros) []
   257 
   258 fun add_edges edges_of key G =
   259   let
   260     fun extend' key (G, visited) = 
   261       case try (Graph.get_node G) key of
   262           SOME v =>
   263             let
   264               val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v))
   265               val (G', visited') = fold extend'
   266                 (subtract (op =) (key :: visited) new_edges) (G, key :: visited)
   267             in
   268               (fold (Graph.add_edge o (pair key)) new_edges G', visited')
   269             end
   270         | NONE => (G, visited)
   271   in
   272     fst (extend' key (G, []))
   273   end
   274 
   275 fun generate options ctxt const =
   276   let 
   277     fun strong_conn_of gr keys =
   278       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
   279     val gr = Predicate_Compile_Core.intros_graph_of ctxt
   280     val gr' = add_edges depending_preds_of const gr
   281     val scc = strong_conn_of gr' [const]
   282     val constant_table = mk_constant_table (flat scc)
   283   in
   284     apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
   285   end
   286   
   287 (* add implementation for ground predicates *)
   288 
   289 fun add_ground_typ (Conj prems) = fold add_ground_typ prems
   290   | add_ground_typ (Ground (_, T)) = insert (op =) T
   291   | add_ground_typ _ = I
   292 
   293 fun mk_relname (Type (Tcon, Targs)) =
   294   first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
   295   | mk_relname _ = raise Fail "unexpected type"
   296 
   297 (* This is copied from "pat_completeness.ML" *)
   298 fun inst_constrs_of thy (T as Type (name, _)) =
   299   map (fn (Cn,CT) =>
   300     Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
   301     (the (Datatype.get_constrs thy name))
   302   | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
   303   
   304 fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) =
   305   if member (op =) seen T then ([], (seen, constant_table))
   306   else
   307     let
   308       val rel_name = mk_relname T
   309       fun mk_impl (Const (constr_name, T)) (seen, constant_table) =
   310         let
   311           val constant_table' = declare_consts [constr_name] constant_table
   312           val (rec_clauses, (seen', constant_table'')) =
   313             fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table')
   314           val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T)))    
   315           fun mk_prem v T = Rel (mk_relname T, [v])
   316           val clause =
   317             ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
   318              Conj (map2 mk_prem vars (binder_types T)))
   319         in
   320           (clause :: flat rec_clauses, (seen', constant_table''))
   321         end
   322       val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T
   323     in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end
   324  | mk_ground_impl ctxt T (seen, constant_table) =
   325    raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T)
   326 
   327 fun replace_ground (Conj prems) = Conj (map replace_ground prems)
   328   | replace_ground (Ground (x, T)) =
   329     Rel (mk_relname T, [Var x])  
   330   | replace_ground p = p
   331   
   332 fun add_ground_predicates ctxt (p, constant_table) =
   333   let
   334     val ground_typs = fold (add_ground_typ o snd) p []
   335     val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table)
   336     val p' = map (apsnd replace_ground) p
   337   in
   338     ((flat grs) @ p', constant_table')
   339   end
   340     
   341 (* rename variables to prolog-friendly names *)
   342 
   343 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
   344 
   345 fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming)
   346 
   347 fun dest_Char (Symbol.Char c) = c
   348 
   349 fun is_prolog_conform v =
   350   forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
   351 
   352 fun mk_conform avoid v =
   353   let 
   354     val v' = space_implode "" (map (dest_Char o Symbol.decode)
   355       (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
   356         (Symbol.explode v)))
   357     val v' = if v' = "" then "var" else v'
   358   in Name.variant avoid (first_upper v') end
   359   
   360 fun mk_renaming v renaming =
   361   (v, mk_conform (map snd renaming) v) :: renaming
   362 
   363 fun rename_vars_clause ((rel, args), prem) =
   364   let
   365     val vars = fold_prem_terms add_vars prem (fold add_vars args [])
   366     val renaming = fold mk_renaming vars []
   367   in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end
   368   
   369 val rename_vars_program = map rename_vars_clause
   370   
   371 (* code printer *)
   372 
   373 fun write_arith_op Plus = "+"
   374   | write_arith_op Minus = "-"
   375 
   376 fun write_term (Var v) = v
   377   | write_term (Cons c) = c
   378   | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
   379   | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
   380   | write_term (Number n) = string_of_int n
   381 
   382 fun write_rel (pred, args) =
   383   pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
   384 
   385 fun write_prem (Conj prems) = space_implode ", " (map write_prem prems)
   386   | write_prem (Rel p) = write_rel p  
   387   | write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
   388   | write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
   389   | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
   390   | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r
   391   | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r
   392 
   393 fun write_clause (head, prem) =
   394   write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
   395 
   396 fun write_program p =
   397   cat_lines (map write_clause p) 
   398 
   399 (** query templates **)
   400 
   401 fun query_first rel vnames =
   402   "eval :- once("  ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
   403   "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
   404   "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
   405   
   406 fun query_firstn n rel vnames =
   407   "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
   408     rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^
   409     "writelist([]).\n" ^
   410     "writelist([(" ^ space_implode ", " vnames ^ ")|T]) :- " ^
   411     "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
   412     "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
   413   
   414 val prelude =
   415   "#!/usr/bin/swipl -q -t main -f\n\n" ^
   416   ":- use_module(library('dialect/ciao/aggregates')).\n" ^
   417   ":- style_check(-singleton).\n" ^
   418   ":- style_check(-discontiguous).\n" ^ 	
   419   ":- style_check(-atom).\n\n" ^
   420   "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
   421   "main :- halt(1).\n"
   422 
   423 (* parsing prolog solution *)
   424 val scan_number =
   425   Scan.many1 Symbol.is_ascii_digit
   426 
   427 val scan_atom =
   428   Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
   429 
   430 val scan_var =
   431   Scan.many1
   432     (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
   433 
   434 val scan_ident =
   435   Scan.repeat (Scan.one
   436     (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
   437 
   438 fun dest_Char (Symbol.Char s) = s
   439 
   440 val string_of = concat o map (dest_Char o Symbol.decode)
   441 
   442 val is_atom_ident = forall Symbol.is_ascii_lower
   443 
   444 val is_var_ident =
   445   forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
   446 
   447 fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0
   448 
   449 fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms)
   450   || (scan_term >> single)) xs
   451 and scan_term xs =
   452   ((scan_number >> (Number o int_of_symbol_list))
   453   || (scan_var >> (Var o string_of))
   454   || ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")"))
   455     >> (fn (f, ts) => AppF (string_of f, ts)))
   456   || (scan_atom >> (Cons o string_of))) xs
   457 
   458 val parse_term = fst o Scan.finite Symbol.stopper
   459     (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
   460   o explode
   461   
   462 fun parse_solutions sol =
   463   let
   464     fun dest_eq s = case space_explode "=" s of
   465         (l :: r :: []) => parse_term (unprefix " " r)
   466       | _ => raise Fail "unexpected equation in prolog output"
   467     fun parse_solution s = map dest_eq (space_explode ";" s)
   468   in
   469     map parse_solution (fst (split_last (space_explode "\n" sol)))
   470   end 
   471   
   472 (* calling external interpreter and getting results *)
   473 
   474 fun run p query_rel vnames nsols =
   475   let
   476     val cmd = Path.named_root
   477     val query = case nsols of NONE => query_first | SOME n => query_firstn n
   478     val p' = rename_vars_program p
   479     val _ = tracing "Renaming variable names..."
   480     val renaming = fold mk_renaming vnames [] 
   481     val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
   482     val prog = prelude ^ query query_rel vnames' ^ write_program p'
   483     val _ = tracing ("Generated prolog program:\n" ^ prog)
   484     val prolog_file = File.tmp_path (Path.basic "prolog_file")
   485     val _ = File.write prolog_file prog
   486     val (solution, _) = bash_output ("/usr/local/bin/swipl -f " ^ File.shell_path prolog_file)
   487     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
   488     val tss = parse_solutions solution
   489   in
   490     tss
   491   end
   492 
   493 (* values command *)
   494 
   495 fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
   496   | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
   497   | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number") 
   498   | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
   499   | restore_term ctxt constant_table (AppF (f, args), T) =
   500     let
   501       val thy = ProofContext.theory_of ctxt
   502       val c = restore_const constant_table f
   503       val cT = Sign.the_const_type thy c
   504       val (argsT, resT) = strip_type cT
   505       val subst = Sign.typ_match thy (resT, T) Vartab.empty
   506       val argsT' = map (Envir.subst_type subst) argsT
   507     in
   508       list_comb (Const (c, Envir.subst_type subst cT),
   509         map (restore_term ctxt constant_table) (args ~~ argsT'))
   510     end
   511 
   512 fun values ctxt soln t_compr =
   513   let
   514     val options = !options
   515     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
   516       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
   517     val (body, Ts, fp) = HOLogic.strip_psplits split;
   518     val output_names = Name.variant_list (Term.add_free_names body [])
   519       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   520     val output_frees = rev (map2 (curry Free) output_names Ts)
   521     val body = subst_bounds (output_frees, body)
   522     val (pred as Const (name, T), all_args) =
   523       case strip_comb body of
   524         (Const (name, T), all_args) => (Const (name, T), all_args)
   525       | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
   526     val vnames =
   527       case try (map (fst o dest_Free)) all_args of
   528         SOME vs => vs
   529       | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args))
   530     val _ = tracing "Preprocessing specification..."
   531     val T = Sign.the_const_type (ProofContext.theory_of ctxt) name
   532     val t = Const (name, T)
   533     val thy' =
   534       Theory.copy (ProofContext.theory_of ctxt)
   535       |> Predicate_Compile.preprocess preprocess_options t
   536     val ctxt' = ProofContext.init_global thy'
   537     val _ = tracing "Generating prolog program..."
   538     val (p, constant_table) = generate options ctxt' name
   539       |> (if #ensure_groundness options then add_ground_predicates ctxt' else I)
   540     val _ = tracing "Running prolog program..."
   541     val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
   542     val _ = tracing "Restoring terms..."
   543     val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
   544     fun mk_insert x S =
   545       Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
   546     fun mk_set_compr in_insert [] xs =
   547        rev ((Free ("...", fastype_of t_compr)) ::
   548         (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
   549       | mk_set_compr in_insert (t :: ts) xs =
   550         let
   551           val frees = Term.add_frees t []
   552         in
   553           if null frees then
   554             mk_set_compr (t :: in_insert) ts xs
   555           else
   556             let
   557               val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
   558               val set_compr =
   559                 HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
   560                   frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
   561             in
   562               mk_set_compr [] ts
   563                 (set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))  
   564             end
   565         end
   566   in
   567       foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
   568         (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
   569   end
   570 
   571 fun values_cmd print_modes soln raw_t state =
   572   let
   573     val ctxt = Toplevel.context_of state
   574     val t = Syntax.read_term ctxt raw_t
   575     val t' = values ctxt soln t
   576     val ty' = Term.type_of t'
   577     val ctxt' = Variable.auto_fixes t' ctxt
   578     val _ = tracing "Printing terms..."
   579     val p = Print_Mode.with_modes print_modes (fn () =>
   580       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   581         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   582   in Pretty.writeln p end;
   583 
   584 
   585 (* renewing the values command for Prolog queries *)
   586 
   587 val opt_print_modes =
   588   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
   589 
   590 val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
   591   (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
   592    >> (fn ((print_modes, soln), t) => Toplevel.keep
   593         (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
   594 
   595 (* quickcheck generator *)
   596 
   597 (* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
   598 
   599 fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
   600   | strip_imp_prems _ = [];
   601 
   602 fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
   603   | strip_imp_concl A = A : term;
   604 
   605 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   606 
   607 fun quickcheck ctxt report t size =
   608   let
   609     val thy = Theory.copy (ProofContext.theory_of ctxt)
   610     val (vs, t') = strip_abs t
   611     val vs' = Variable.variant_frees ctxt [] vs
   612     val Ts = map snd vs'
   613     val t'' = subst_bounds (map Free (rev vs'), t')
   614     val (prems, concl) = strip_horn t''
   615     val constname = "quickcheck"
   616     val full_constname = Sign.full_bname thy constname
   617     val constT = Ts ---> @{typ bool}
   618     val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
   619     val const = Const (full_constname, constT)
   620     val t = Logic.list_implies
   621       (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
   622        HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
   623     val tac = fn _ => Skip_Proof.cheat_tac thy1
   624     val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
   625     val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
   626     val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
   627     val ctxt' = ProofContext.init_global thy3
   628     val _ = tracing "Generating prolog program..."
   629     val (p, constant_table) = generate {ensure_groundness = true} ctxt' full_constname
   630       |> add_ground_predicates ctxt'
   631     val _ = tracing "Running prolog program..."
   632     val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
   633       (SOME 1)
   634     val _ = tracing "Restoring terms..."
   635     val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
   636     val empty_report = ([], false)
   637   in
   638     (res, empty_report)
   639   end; 
   640 
   641 end;