# HG changeset patch
# User bulwahn
# Date 1280650543 -7200
# Node ID 81f08bbb3be711e8bf37d648d438d0c3d2fe7a54
# Parent  cf08f478093865865840f5b38dbb24a34b23bbfb
adding basic arithmetic support for prolog code generation

diff -r cf08f4780938 -r 81f08bbb3be7 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Aug 01 10:15:43 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Aug 01 10:15:43 2010 +0200
@@ -6,10 +6,14 @@
 
 signature CODE_PROLOG =
 sig
+  datatype arith_op = Plus | Minus
   datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
-    | Number of int;
-  datatype prem = Conj of prem list | NotRel of string * prol_term list
-    | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
+    | Number of int | ArithOp of arith_op * prol_term list;
+  datatype prem = Conj of prem list
+    | Rel of string * prol_term list | NotRel of string * prol_term list
+    | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
+    | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
+      
   type clause = ((string * prol_term list) * prem);
   type logic_program = clause list;
   type constant_table = (string * string) list
@@ -36,17 +40,29 @@
 
 (* internal program representation *)
 
+datatype arith_op = Plus | Minus
+
 datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
-  | Number of int;
+  | Number of int | ArithOp of arith_op * prol_term list;
+
+fun is_Var (Var _) = true
+  | is_Var _ = false
+
+fun is_arith_term (Var _) = true
+  | is_arith_term (Number _) = true
+  | is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands
+  | is_arith_term _ = false
 
 fun string_of_prol_term (Var s) = "Var " ^ s
   | string_of_prol_term (Cons s) = "Cons " ^ s
   | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
   | string_of_prol_term (Number n) = "Number " ^ string_of_int n
 
-datatype prem = Conj of prem list | NotRel of string * prol_term list
-    | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
-
+datatype prem = Conj of prem list
+  | Rel of string * prol_term list | NotRel of string * prol_term list
+  | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
+  | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
+    
 fun dest_Rel (Rel (c, ts)) = (c, ts)
  
 type clause = ((string * prol_term list) * prem);
@@ -83,6 +99,10 @@
   
 (** translation of terms, literals, premises, and clauses **)
 
+fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus
+  | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
+  | translate_arith_const _ = NONE
+
 fun translate_term ctxt constant_table t =
   case try HOLogic.dest_number t of
     SOME (@{typ "int"}, n) => Number n
@@ -91,20 +111,29 @@
         (Free (v, T), []) => Var v 
       | (Const (c, _), []) => Cons (translate_const constant_table c)
       | (Const (c, _), args) =>
-        AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)
+        (case translate_arith_const c of
+          SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
+        | NONE =>                                                             
+            AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
       | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
 
 fun translate_literal ctxt constant_table t =
   case strip_comb t of
     (Const (@{const_name "op ="}, _), [l, r]) =>
-      Eq (pairself (translate_term ctxt constant_table) (l, r))
+      let
+        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')
+      end
   | (Const (c, _), args) =>
       Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
   | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
 
 fun NegRel_of (Rel lit) = NotRel lit
   | NegRel_of (Eq eq) = NotEq eq
-  
+  | NegRel_of (ArithEq eq) = NotArithEq eq
+
 fun translate_prem ctxt constant_table t =  
     case try HOLogic.dest_not t of
       SOME t => NegRel_of (translate_literal ctxt constant_table t)
@@ -164,9 +193,13 @@
 
 (* code printer *)
 
+fun write_arith_op Plus = "+"
+  | write_arith_op Minus = "-"
+
 fun write_term (Var v) = first_upper v
   | write_term (Cons c) = c
-  | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
+  | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+  | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
   | write_term (Number n) = string_of_int n
 
 fun write_rel (pred, args) =
@@ -177,6 +210,8 @@
   | write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
   | write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
   | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
+  | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r
+  | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r
 
 fun write_clause (head, prem) =
   write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")