src/HOL/Tools/Predicate_Compile/code_prolog.ML
author bulwahn
Wed Aug 25 16:59:46 2010 +0200 (2010-08-25)
changeset 38727 c7f5f0b7dc7f
parent 38558 32ad17fe2b9c
child 38728 182b180e9804
permissions -rw-r--r--
adding very basic transformation to ensure groundness before negations
bulwahn@38073
     1
(*  Title:      HOL/Tools/Predicate_Compile/code_prolog.ML
bulwahn@38073
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@38073
     3
bulwahn@38073
     4
Prototype of an code generator for logic programming languages (a.k.a. Prolog)
bulwahn@38073
     5
*)
bulwahn@38073
     6
bulwahn@38073
     7
signature CODE_PROLOG =
bulwahn@38073
     8
sig
bulwahn@38727
     9
  type code_options = {ensure_groundness : bool}
bulwahn@38727
    10
  val options : code_options ref
bulwahn@38727
    11
bulwahn@38113
    12
  datatype arith_op = Plus | Minus
bulwahn@38112
    13
  datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
bulwahn@38113
    14
    | Number of int | ArithOp of arith_op * prol_term list;
bulwahn@38113
    15
  datatype prem = Conj of prem list
bulwahn@38113
    16
    | Rel of string * prol_term list | NotRel of string * prol_term list
bulwahn@38113
    17
    | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
bulwahn@38727
    18
    | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term
bulwahn@38727
    19
    | Ground of string * typ;
bulwahn@38727
    20
bulwahn@38079
    21
  type clause = ((string * prol_term list) * prem);
bulwahn@38073
    22
  type logic_program = clause list;
bulwahn@38079
    23
  type constant_table = (string * string) list
bulwahn@38727
    24
    
bulwahn@38727
    25
  val generate : code_options -> Proof.context -> string list -> (logic_program * constant_table)
bulwahn@38079
    26
  val write_program : logic_program -> string
bulwahn@38079
    27
  val run : logic_program -> string -> string list -> int option -> prol_term list list
bulwahn@38073
    28
bulwahn@38079
    29
  val trace : bool Unsynchronized.ref
bulwahn@38073
    30
end;
bulwahn@38073
    31
bulwahn@38073
    32
structure Code_Prolog : CODE_PROLOG =
bulwahn@38073
    33
struct
bulwahn@38073
    34
bulwahn@38079
    35
(* diagnostic tracing *)
bulwahn@38079
    36
bulwahn@38079
    37
val trace = Unsynchronized.ref false
bulwahn@38079
    38
bulwahn@38079
    39
fun tracing s = if !trace then Output.tracing s else () 
bulwahn@38727
    40
bulwahn@38727
    41
(* code generation options *)
bulwahn@38727
    42
bulwahn@38727
    43
type code_options = {ensure_groundness : bool}
bulwahn@38727
    44
bulwahn@38727
    45
val options = Unsynchronized.ref {ensure_groundness = false};
bulwahn@38727
    46
bulwahn@38073
    47
(* general string functions *)
bulwahn@38073
    48
bulwahn@38073
    49
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
bulwahn@38073
    50
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
bulwahn@38073
    51
bulwahn@38073
    52
(* internal program representation *)
bulwahn@38073
    53
bulwahn@38113
    54
datatype arith_op = Plus | Minus
bulwahn@38113
    55
bulwahn@38112
    56
datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
bulwahn@38113
    57
  | Number of int | ArithOp of arith_op * prol_term list;
bulwahn@38113
    58
bulwahn@38113
    59
fun is_Var (Var _) = true
bulwahn@38113
    60
  | is_Var _ = false
bulwahn@38113
    61
bulwahn@38113
    62
fun is_arith_term (Var _) = true
bulwahn@38113
    63
  | is_arith_term (Number _) = true
bulwahn@38113
    64
  | is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands
bulwahn@38113
    65
  | is_arith_term _ = false
bulwahn@38073
    66
bulwahn@38081
    67
fun string_of_prol_term (Var s) = "Var " ^ s
bulwahn@38075
    68
  | string_of_prol_term (Cons s) = "Cons " ^ s
bulwahn@38075
    69
  | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
bulwahn@38112
    70
  | string_of_prol_term (Number n) = "Number " ^ string_of_int n
bulwahn@38075
    71
bulwahn@38113
    72
datatype prem = Conj of prem list
bulwahn@38113
    73
  | Rel of string * prol_term list | NotRel of string * prol_term list
bulwahn@38113
    74
  | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
bulwahn@38727
    75
  | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term
bulwahn@38727
    76
  | Ground of string * typ;
bulwahn@38727
    77
  
bulwahn@38073
    78
fun dest_Rel (Rel (c, ts)) = (c, ts)
bulwahn@38073
    79
 
bulwahn@38079
    80
type clause = ((string * prol_term list) * prem);
bulwahn@38073
    81
bulwahn@38073
    82
type logic_program = clause list;
bulwahn@38073
    83
bulwahn@38073
    84
(* translation from introduction rules to internal representation *)
bulwahn@38073
    85
bulwahn@38079
    86
(** constant table **)
bulwahn@38079
    87
bulwahn@38079
    88
type constant_table = (string * string) list
bulwahn@38079
    89
bulwahn@38073
    90
(* assuming no clashing *)
bulwahn@38079
    91
fun mk_constant_table consts =
bulwahn@38079
    92
  AList.make (first_lower o Long_Name.base_name) consts
bulwahn@38079
    93
bulwahn@38079
    94
fun declare_consts consts constant_table =
bulwahn@38079
    95
  fold (fn c => AList.update (op =) (c, first_lower (Long_Name.base_name c))) consts constant_table
bulwahn@38079
    96
  
bulwahn@38079
    97
fun translate_const constant_table c =
bulwahn@38079
    98
  case AList.lookup (op =) constant_table c of
bulwahn@38079
    99
    SOME c' => c'
bulwahn@38079
   100
  | NONE => error ("No such constant: " ^ c)
bulwahn@38073
   101
bulwahn@38079
   102
fun inv_lookup _ [] _ = NONE
bulwahn@38079
   103
  | inv_lookup eq ((key, value)::xs) value' =
bulwahn@38079
   104
      if eq (value', value) then SOME key
bulwahn@38079
   105
      else inv_lookup eq xs value';
bulwahn@38079
   106
bulwahn@38079
   107
fun restore_const constant_table c =
bulwahn@38079
   108
  case inv_lookup (op =) constant_table c of
bulwahn@38079
   109
    SOME c' => c'
bulwahn@38079
   110
  | NONE => error ("No constant corresponding to "  ^ c)
bulwahn@38727
   111
bulwahn@38079
   112
(** translation of terms, literals, premises, and clauses **)
bulwahn@38079
   113
bulwahn@38113
   114
fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus
bulwahn@38113
   115
  | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
bulwahn@38113
   116
  | translate_arith_const _ = NONE
bulwahn@38113
   117
bulwahn@38079
   118
fun translate_term ctxt constant_table t =
bulwahn@38112
   119
  case try HOLogic.dest_number t of
bulwahn@38112
   120
    SOME (@{typ "int"}, n) => Number n
bulwahn@38112
   121
  | NONE =>
bulwahn@38112
   122
      (case strip_comb t of
bulwahn@38112
   123
        (Free (v, T), []) => Var v 
bulwahn@38112
   124
      | (Const (c, _), []) => Cons (translate_const constant_table c)
bulwahn@38112
   125
      | (Const (c, _), args) =>
bulwahn@38113
   126
        (case translate_arith_const c of
bulwahn@38113
   127
          SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
bulwahn@38113
   128
        | NONE =>                                                             
bulwahn@38113
   129
            AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
bulwahn@38112
   130
      | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
bulwahn@38073
   131
bulwahn@38079
   132
fun translate_literal ctxt constant_table t =
bulwahn@38073
   133
  case strip_comb t of
bulwahn@38079
   134
    (Const (@{const_name "op ="}, _), [l, r]) =>
bulwahn@38113
   135
      let
bulwahn@38113
   136
        val l' = translate_term ctxt constant_table l
bulwahn@38113
   137
        val r' = translate_term ctxt constant_table r
bulwahn@38113
   138
      in
bulwahn@38113
   139
        (if is_Var l' andalso is_arith_term r' then ArithEq else Eq) (l', r')
bulwahn@38113
   140
      end
bulwahn@38079
   141
  | (Const (c, _), args) =>
bulwahn@38079
   142
      Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
bulwahn@38073
   143
  | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
bulwahn@38073
   144
bulwahn@38073
   145
fun NegRel_of (Rel lit) = NotRel lit
bulwahn@38073
   146
  | NegRel_of (Eq eq) = NotEq eq
bulwahn@38113
   147
  | NegRel_of (ArithEq eq) = NotArithEq eq
bulwahn@38113
   148
bulwahn@38727
   149
fun mk_groundness_prems t = map Ground (Term.add_frees t [])
bulwahn@38727
   150
  
bulwahn@38727
   151
fun translate_prem options ctxt constant_table t =  
bulwahn@38073
   152
    case try HOLogic.dest_not t of
bulwahn@38727
   153
      SOME t =>
bulwahn@38727
   154
        if #ensure_groundness options then
bulwahn@38727
   155
          Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
bulwahn@38727
   156
        else
bulwahn@38727
   157
          NegRel_of (translate_literal ctxt constant_table t)
bulwahn@38079
   158
    | NONE => translate_literal ctxt constant_table t
bulwahn@38114
   159
    
bulwahn@38114
   160
fun imp_prems_conv cv ct =
bulwahn@38114
   161
  case Thm.term_of ct of
bulwahn@38114
   162
    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
bulwahn@38114
   163
  | _ => Conv.all_conv ct
bulwahn@38114
   164
bulwahn@38114
   165
fun Trueprop_conv cv ct =
bulwahn@38114
   166
  case Thm.term_of ct of
haftmann@38558
   167
    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
bulwahn@38114
   168
  | _ => raise Fail "Trueprop_conv"
bulwahn@38114
   169
bulwahn@38114
   170
fun preprocess_intro thy rule =
bulwahn@38114
   171
  Conv.fconv_rule
bulwahn@38114
   172
    (imp_prems_conv
bulwahn@38114
   173
      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
bulwahn@38114
   174
    (Thm.transfer thy rule)
bulwahn@38114
   175
bulwahn@38727
   176
fun translate_intros options ctxt gr const constant_table =
bulwahn@38073
   177
  let
bulwahn@38114
   178
    val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
bulwahn@38073
   179
    val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
bulwahn@38079
   180
    val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
bulwahn@38073
   181
    fun translate_intro intro =
bulwahn@38073
   182
      let
bulwahn@38073
   183
        val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
bulwahn@38727
   184
        val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
bulwahn@38727
   185
        val prems' = Conj (map (translate_prem options ctxt' constant_table') prems)
bulwahn@38079
   186
        val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
bulwahn@38073
   187
      in clause end
bulwahn@38079
   188
  in (map translate_intro intros', constant_table') end
bulwahn@38073
   189
bulwahn@38727
   190
fun generate options ctxt const =
bulwahn@38073
   191
  let 
bulwahn@38073
   192
     fun strong_conn_of gr keys =
bulwahn@38073
   193
      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
bulwahn@38073
   194
    val gr = Predicate_Compile_Core.intros_graph_of ctxt
bulwahn@38073
   195
    val scc = strong_conn_of gr const
bulwahn@38079
   196
    val constant_table = mk_constant_table (flat scc)
bulwahn@38073
   197
  in
bulwahn@38727
   198
    apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
bulwahn@38073
   199
  end
bulwahn@38727
   200
  
bulwahn@38727
   201
(* add implementation for ground predicates *)
bulwahn@38073
   202
bulwahn@38727
   203
fun add_ground_typ (Conj prems) = fold add_ground_typ prems
bulwahn@38727
   204
  | add_ground_typ (Ground (_, T)) = insert (op =) T
bulwahn@38727
   205
  | add_ground_typ _ = I
bulwahn@38073
   206
bulwahn@38727
   207
fun mk_ground_impl ctxt (Type (Tcon, [])) constant_table =
bulwahn@38073
   208
  let
bulwahn@38727
   209
    fun mk_impl (constr_name, T) constant_table =
bulwahn@38727
   210
      if binder_types T = [] then
bulwahn@38727
   211
        let
bulwahn@38727
   212
          val constant_table' = declare_consts [constr_name] constant_table
bulwahn@38727
   213
          val clause = (("is_" ^ first_lower (Long_Name.base_name Tcon),
bulwahn@38727
   214
            [Cons (translate_const constant_table' constr_name)]), Conj [])
bulwahn@38727
   215
        in
bulwahn@38727
   216
          (clause, constant_table')
bulwahn@38727
   217
        end
bulwahn@38727
   218
        else raise Fail "constructor with arguments" 
bulwahn@38727
   219
    val constrs = the (Datatype.get_constrs (ProofContext.theory_of ctxt) Tcon)
bulwahn@38727
   220
  in fold_map mk_impl constrs constant_table end
bulwahn@38727
   221
  | mk_ground_impl ctxt (Type (Tcon, _)) constant_table =
bulwahn@38727
   222
    raise Fail "type constructor with type arguments"
bulwahn@38727
   223
  
bulwahn@38727
   224
fun replace_ground (Conj prems) = Conj (map replace_ground prems)
bulwahn@38727
   225
  | replace_ground (Ground (x, Type (Tcon, []))) =
bulwahn@38727
   226
    Rel ("is_" ^ first_lower (Long_Name.base_name Tcon), [Var x])  
bulwahn@38727
   227
  | replace_ground p = p
bulwahn@38727
   228
  
bulwahn@38727
   229
fun add_ground_predicates ctxt (p, constant_table) =
bulwahn@38727
   230
  let
bulwahn@38727
   231
    val ground_typs = fold (add_ground_typ o snd) p []
bulwahn@38727
   232
    val (grs, constant_table') = fold_map (mk_ground_impl ctxt) ground_typs constant_table
bulwahn@38727
   233
    val p' = map (apsnd replace_ground) p
bulwahn@38073
   234
  in
bulwahn@38727
   235
    ((flat grs) @ p', constant_table')
bulwahn@38073
   236
  end
bulwahn@38727
   237
    
bulwahn@38073
   238
(* code printer *)
bulwahn@38073
   239
bulwahn@38113
   240
fun write_arith_op Plus = "+"
bulwahn@38113
   241
  | write_arith_op Minus = "-"
bulwahn@38113
   242
bulwahn@38081
   243
fun write_term (Var v) = first_upper v
bulwahn@38079
   244
  | write_term (Cons c) = c
bulwahn@38113
   245
  | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
bulwahn@38113
   246
  | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
bulwahn@38112
   247
  | write_term (Number n) = string_of_int n
bulwahn@38073
   248
bulwahn@38073
   249
fun write_rel (pred, args) =
bulwahn@38073
   250
  pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
bulwahn@38073
   251
bulwahn@38073
   252
fun write_prem (Conj prems) = space_implode ", " (map write_prem prems)
bulwahn@38073
   253
  | write_prem (Rel p) = write_rel p  
bulwahn@38073
   254
  | write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
bulwahn@38073
   255
  | write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
bulwahn@38073
   256
  | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
bulwahn@38113
   257
  | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r
bulwahn@38113
   258
  | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r
bulwahn@38073
   259
bulwahn@38073
   260
fun write_clause (head, prem) =
bulwahn@38073
   261
  write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
bulwahn@38073
   262
bulwahn@38073
   263
fun write_program p =
bulwahn@38073
   264
  cat_lines (map write_clause p) 
bulwahn@38073
   265
bulwahn@38078
   266
(** query templates **)
bulwahn@38078
   267
bulwahn@38073
   268
fun query_first rel vnames =
bulwahn@38073
   269
  "eval :- once("  ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
bulwahn@38082
   270
  "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
bulwahn@38082
   271
  "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
bulwahn@38077
   272
  
bulwahn@38077
   273
fun query_firstn n rel vnames =
bulwahn@38077
   274
  "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
bulwahn@38077
   275
    rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^
bulwahn@38077
   276
    "writelist([]).\n" ^
bulwahn@38077
   277
    "writelist([(" ^ space_implode ", " vnames ^ ")|T]) :- " ^
bulwahn@38079
   278
    "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
bulwahn@38079
   279
    "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
bulwahn@38077
   280
  
bulwahn@38073
   281
val prelude =
bulwahn@38073
   282
  "#!/usr/bin/swipl -q -t main -f\n\n" ^
bulwahn@38077
   283
  ":- use_module(library('dialect/ciao/aggregates')).\n" ^
bulwahn@38073
   284
  ":- style_check(-singleton).\n\n" ^
bulwahn@38073
   285
  "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
bulwahn@38073
   286
  "main :- halt(1).\n"
bulwahn@38075
   287
bulwahn@38075
   288
(* parsing prolog solution *)
bulwahn@38115
   289
val scan_number =
bulwahn@38115
   290
  Scan.many1 Symbol.is_ascii_digit
bulwahn@38075
   291
bulwahn@38075
   292
val scan_atom =
bulwahn@38078
   293
  Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_quasi s)
bulwahn@38075
   294
bulwahn@38075
   295
val scan_var =
bulwahn@38078
   296
  Scan.many1
bulwahn@38078
   297
    (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
bulwahn@38075
   298
bulwahn@38076
   299
val scan_ident =
bulwahn@38076
   300
  Scan.repeat (Scan.one
bulwahn@38076
   301
    (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
bulwahn@38076
   302
bulwahn@38075
   303
fun dest_Char (Symbol.Char s) = s
bulwahn@38075
   304
bulwahn@38075
   305
val string_of = concat o map (dest_Char o Symbol.decode)
bulwahn@38075
   306
bulwahn@38076
   307
val is_atom_ident = forall Symbol.is_ascii_lower
bulwahn@38076
   308
bulwahn@38076
   309
val is_var_ident =
bulwahn@38076
   310
  forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
bulwahn@38078
   311
bulwahn@38115
   312
fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0
bulwahn@38115
   313
bulwahn@38078
   314
fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms)
bulwahn@38078
   315
  || (scan_term >> single)) xs
bulwahn@38078
   316
and scan_term xs =
bulwahn@38115
   317
  ((scan_number >> (Number o int_of_symbol_list))
bulwahn@38115
   318
  || (scan_var >> (Var o string_of))
bulwahn@38078
   319
  || ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")"))
bulwahn@38079
   320
    >> (fn (f, ts) => AppF (string_of f, ts)))
bulwahn@38078
   321
  || (scan_atom >> (Cons o string_of))) xs
bulwahn@38079
   322
bulwahn@38075
   323
val parse_term = fst o Scan.finite Symbol.stopper
bulwahn@38077
   324
    (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
bulwahn@38075
   325
  o explode
bulwahn@38075
   326
  
bulwahn@38079
   327
fun parse_solutions sol =
bulwahn@38075
   328
  let
bulwahn@38077
   329
    fun dest_eq s = case space_explode "=" s of
bulwahn@38075
   330
        (l :: r :: []) => parse_term (unprefix " " r)
bulwahn@38078
   331
      | _ => raise Fail "unexpected equation in prolog output"
bulwahn@38079
   332
    fun parse_solution s = map dest_eq (space_explode ";" s)
bulwahn@38075
   333
  in
bulwahn@38079
   334
    map parse_solution (fst (split_last (space_explode "\n" sol)))
bulwahn@38075
   335
  end 
bulwahn@38073
   336
  
bulwahn@38073
   337
(* calling external interpreter and getting results *)
bulwahn@38073
   338
bulwahn@38077
   339
fun run p query_rel vnames nsols =
bulwahn@38073
   340
  let
bulwahn@38073
   341
    val cmd = Path.named_root
bulwahn@38077
   342
    val query = case nsols of NONE => query_first | SOME n => query_firstn n 
bulwahn@38077
   343
    val prog = prelude ^ query query_rel vnames ^ write_program p
bulwahn@38079
   344
    val _ = tracing ("Generated prolog program:\n" ^ prog)
bulwahn@38073
   345
    val prolog_file = File.tmp_path (Path.basic "prolog_file")
bulwahn@38073
   346
    val _ = File.write prolog_file prog
bulwahn@38077
   347
    val (solution, _) = bash_output ("/usr/local/bin/swipl -f " ^ File.shell_path prolog_file)
bulwahn@38079
   348
    val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
bulwahn@38079
   349
    val tss = parse_solutions solution
bulwahn@38073
   350
  in
bulwahn@38079
   351
    tss
bulwahn@38073
   352
  end
bulwahn@38073
   353
bulwahn@38075
   354
(* values command *)
bulwahn@38075
   355
bulwahn@38081
   356
fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
bulwahn@38115
   357
  | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
bulwahn@38115
   358
  | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number") 
bulwahn@38079
   359
  | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
bulwahn@38079
   360
  | restore_term ctxt constant_table (AppF (f, args), T) =
bulwahn@38079
   361
    let
bulwahn@38079
   362
      val thy = ProofContext.theory_of ctxt
bulwahn@38079
   363
      val c = restore_const constant_table f
bulwahn@38079
   364
      val cT = Sign.the_const_type thy c
bulwahn@38079
   365
      val (argsT, resT) = strip_type cT
bulwahn@38079
   366
      val subst = Sign.typ_match thy (resT, T) Vartab.empty
bulwahn@38079
   367
      val argsT' = map (Envir.subst_type subst) argsT
bulwahn@38079
   368
    in
bulwahn@38079
   369
      list_comb (Const (c, Envir.subst_type subst cT),
bulwahn@38079
   370
        map (restore_term ctxt constant_table) (args ~~ argsT'))
bulwahn@38079
   371
    end
bulwahn@38079
   372
bulwahn@38075
   373
fun values ctxt soln t_compr =
bulwahn@38075
   374
  let
bulwahn@38727
   375
    val options = !options
bulwahn@38075
   376
    val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
bulwahn@38075
   377
      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
bulwahn@38075
   378
    val (body, Ts, fp) = HOLogic.strip_psplits split;
bulwahn@38075
   379
    val output_names = Name.variant_list (Term.add_free_names body [])
bulwahn@38075
   380
      (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
bulwahn@38080
   381
    val output_frees = rev (map2 (curry Free) output_names Ts)
bulwahn@38075
   382
    val body = subst_bounds (output_frees, body)
bulwahn@38075
   383
    val (pred as Const (name, T), all_args) =
bulwahn@38075
   384
      case strip_comb body of
bulwahn@38075
   385
        (Const (name, T), all_args) => (Const (name, T), all_args)
bulwahn@38075
   386
      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
bulwahn@38075
   387
    val vnames =
bulwahn@38075
   388
      case try (map (fst o dest_Free)) all_args of
bulwahn@38075
   389
        SOME vs => vs
bulwahn@38075
   390
      | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args))
bulwahn@38079
   391
    val _ = tracing "Generating prolog program..."
bulwahn@38727
   392
    val (p, constant_table) = generate options ctxt [name]
bulwahn@38727
   393
      |> (if #ensure_groundness options then add_ground_predicates ctxt else I)
bulwahn@38079
   394
    val _ = tracing "Running prolog program..."
bulwahn@38079
   395
    val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
bulwahn@38079
   396
    val _ = tracing "Restoring terms..."
bulwahn@38115
   397
    val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
bulwahn@38115
   398
    fun mk_insert x S =
bulwahn@38115
   399
      Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
bulwahn@38115
   400
    fun mk_set_compr in_insert [] xs =
bulwahn@38115
   401
       rev ((Free ("...", fastype_of t_compr)) ::
bulwahn@38115
   402
        (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
bulwahn@38115
   403
      | mk_set_compr in_insert (t :: ts) xs =
bulwahn@38115
   404
        let
bulwahn@38115
   405
          val frees = Term.add_frees t []
bulwahn@38115
   406
        in
bulwahn@38115
   407
          if null frees then
bulwahn@38115
   408
            mk_set_compr (t :: in_insert) ts xs
bulwahn@38115
   409
          else
bulwahn@38115
   410
            let
bulwahn@38115
   411
              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t)
bulwahn@38115
   412
              val set_compr =
bulwahn@38115
   413
                HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
bulwahn@38115
   414
                  frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
bulwahn@38115
   415
            in
bulwahn@38115
   416
              set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)  
bulwahn@38115
   417
            end
bulwahn@38115
   418
        end
bulwahn@38075
   419
  in
bulwahn@38115
   420
      foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
bulwahn@38115
   421
        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts))) tss) [])
bulwahn@38075
   422
  end
bulwahn@38075
   423
bulwahn@38075
   424
fun values_cmd print_modes soln raw_t state =
bulwahn@38075
   425
  let
bulwahn@38075
   426
    val ctxt = Toplevel.context_of state
bulwahn@38075
   427
    val t = Syntax.read_term ctxt raw_t
bulwahn@38075
   428
    val t' = values ctxt soln t
bulwahn@38075
   429
    val ty' = Term.type_of t'
bulwahn@38075
   430
    val ctxt' = Variable.auto_fixes t' ctxt
bulwahn@38115
   431
    val _ = tracing "Printing terms..."
bulwahn@38075
   432
    val p = Print_Mode.with_modes print_modes (fn () =>
bulwahn@38075
   433
      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
bulwahn@38075
   434
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
bulwahn@38075
   435
  in Pretty.writeln p end;
bulwahn@38075
   436
bulwahn@38075
   437
bulwahn@38075
   438
(* renewing the values command for Prolog queries *)
bulwahn@38075
   439
bulwahn@38075
   440
val opt_print_modes =
bulwahn@38075
   441
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
bulwahn@38075
   442
bulwahn@38075
   443
val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
bulwahn@38077
   444
  (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
bulwahn@38075
   445
   >> (fn ((print_modes, soln), t) => Toplevel.keep
haftmann@38504
   446
        (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
bulwahn@38075
   447
bulwahn@38073
   448
end;