# HG changeset patch
# User bulwahn
# Date 1282748388 -7200
# Node ID 182b180e98041c86915834f579ce73a04c606f7f
# Parent  c7f5f0b7dc7f9e37f7399edf1ced1480300323c2
improving ensure_groundness in prolog generation; added further example

diff -r c7f5f0b7dc7f -r 182b180e9804 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:46 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:48 2010 +0200
@@ -187,4 +187,12 @@
 
 values 2 "{y. notB y}"
 
+inductive notAB :: "abc * abc \<Rightarrow> bool"
+where
+  "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
+
+code_pred notAB .
+
+values 5 "{y. notAB y}"
+
 end
diff -r c7f5f0b7dc7f -r 182b180e9804 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:46 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:48 2010 +0200
@@ -56,6 +56,9 @@
 datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
   | Number of int | ArithOp of arith_op * prol_term list;
 
+fun maybe_AppF (c, []) = Cons c
+  | maybe_AppF (c, xs) = AppF (c, xs)
+
 fun is_Var (Var _) = true
   | is_Var _ = false
 
@@ -136,7 +139,7 @@
         val l' = translate_term ctxt constant_table l
         val r' = translate_term ctxt constant_table r
       in
-        (if is_Var l' andalso is_arith_term r' then ArithEq else Eq) (l', r')
+        (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r')
       end
   | (Const (c, _), args) =>
       Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
@@ -204,32 +207,49 @@
   | add_ground_typ (Ground (_, T)) = insert (op =) T
   | add_ground_typ _ = I
 
-fun mk_ground_impl ctxt (Type (Tcon, [])) constant_table =
-  let
-    fun mk_impl (constr_name, T) constant_table =
-      if binder_types T = [] then
+fun mk_relname (Type (Tcon, Targs)) =
+  first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
+  | mk_relname _ = raise Fail "unexpected type"
+
+(* This is copied from "pat_completeness.ML" *)
+fun inst_constrs_of thy (T as Type (name, _)) =
+  map (fn (Cn,CT) =>
+    Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+    (the (Datatype.get_constrs thy name))
+  | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
+  
+fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) =
+  if member (op =) seen T then ([], (seen, constant_table))
+  else
+    let
+      val rel_name = mk_relname T
+      fun mk_impl (Const (constr_name, T)) (seen, constant_table) =
         let
           val constant_table' = declare_consts [constr_name] constant_table
-          val clause = (("is_" ^ first_lower (Long_Name.base_name Tcon),
-            [Cons (translate_const constant_table' constr_name)]), Conj [])
+          val (rec_clauses, (seen', constant_table'')) =
+            fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table')
+          val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T)))    
+          fun mk_prem v T = Rel (mk_relname T, [v])
+          val clause =
+            ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
+             Conj (map2 mk_prem vars (binder_types T)))
         in
-          (clause, constant_table')
+          (clause :: flat rec_clauses, (seen', constant_table''))
         end
-        else raise Fail "constructor with arguments" 
-    val constrs = the (Datatype.get_constrs (ProofContext.theory_of ctxt) Tcon)
-  in fold_map mk_impl constrs constant_table end
-  | mk_ground_impl ctxt (Type (Tcon, _)) constant_table =
-    raise Fail "type constructor with type arguments"
-  
+      val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T
+    in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end
+ | mk_ground_impl ctxt T (seen, constant_table) =
+   raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T)
+
 fun replace_ground (Conj prems) = Conj (map replace_ground prems)
-  | replace_ground (Ground (x, Type (Tcon, []))) =
-    Rel ("is_" ^ first_lower (Long_Name.base_name Tcon), [Var x])  
+  | replace_ground (Ground (x, T)) =
+    Rel (mk_relname T, [Var x])  
   | replace_ground p = p
   
 fun add_ground_predicates ctxt (p, constant_table) =
   let
     val ground_typs = fold (add_ground_typ o snd) p []
-    val (grs, constant_table') = fold_map (mk_ground_impl ctxt) ground_typs constant_table
+    val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table)
     val p' = map (apsnd replace_ground) p
   in
     ((flat grs) @ p', constant_table')
@@ -290,7 +310,7 @@
   Scan.many1 Symbol.is_ascii_digit
 
 val scan_atom =
-  Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_quasi s)
+  Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
 
 val scan_var =
   Scan.many1