# HG changeset patch
# User bulwahn
# Date 1284967576 -7200
# Node ID a50c0ae2312c789015055a2d4990121ebf9674bc
# Parent  6605c1e87c7fba171ae9b17b4107b051525e36c6
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog

diff -r 6605c1e87c7f -r a50c0ae2312c src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Sep 20 09:26:15 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Sep 20 09:26:16 2010 +0200
@@ -662,6 +662,18 @@
   
 val rename_vars_program = map rename_vars_clause
 
+(* post processing of generated prolog program *)
+
+fun post_process ctxt options (p, constant_table) =
+  (p, constant_table)
+  |> (if #ensure_groundness options then
+        add_ground_predicates ctxt (#limited_types options)
+      else I)
+  |> add_limited_predicates (#limited_predicates options)
+  |> apfst (fold replace (#replacing options))
+  |> apfst (reorder_manually (#manual_reorder options))
+  |> apfst rename_vars_program
+
 (* code printer *)
 
 fun write_arith_op Plus = "+"
@@ -809,12 +821,10 @@
 
 fun run (timeout, system) p (query_rel, args) vnames nsols =
   let
-    val p' = rename_vars_program p
-    val _ = tracing "Renaming variable names..."
     val renaming = fold mk_renaming (fold add_vars args vnames) [] 
     val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
     val args' = map (rename_vars_term renaming) args
-    val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p'
+    val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
     val _ = tracing ("Generated prolog program:\n" ^ prog)
     val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
       (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
@@ -902,12 +912,7 @@
     val ctxt' = ProofContext.init_global thy'
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
-      |> (if #ensure_groundness options then
-          add_ground_predicates ctxt' (#limited_types options)
-        else I)
-      |> add_limited_predicates (#limited_predicates options)
-      |> apfst (fold replace (#replacing options))
-      |> apfst (reorder_manually (#manual_reorder options))
+      |> post_process ctxt' options
     val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table
     val args' = map (translate_term ctxt constant_table') all_args
     val _ = tracing "Running prolog program..."
@@ -983,10 +988,7 @@
     val ctxt' = ProofContext.init_global thy3
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate (NONE, true) ctxt' full_constname
-      |> add_ground_predicates ctxt' (#limited_types options)
-      |> add_limited_predicates (#limited_predicates options)
-      |> apfst (fold replace (#replacing options))
-      |> apfst (reorder_manually (#manual_reorder options))
+      |> post_process ctxt' (set_ensure_groundness options)
     val _ = tracing "Running prolog program..."
     val system_config = System_Config.get (Context.Proof ctxt)
     val tss = run (#timeout system_config, #prolog_system system_config)