src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 38113 81f08bbb3be7
parent 38112 cf08f4780938
child 38114 0f06e3cc04a6
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Aug 01 10:15:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Aug 01 10:15:43 2010 +0200
     1.3 @@ -6,10 +6,14 @@
     1.4  
     1.5  signature CODE_PROLOG =
     1.6  sig
     1.7 +  datatype arith_op = Plus | Minus
     1.8    datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
     1.9 -    | Number of int;
    1.10 -  datatype prem = Conj of prem list | NotRel of string * prol_term list
    1.11 -    | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
    1.12 +    | Number of int | ArithOp of arith_op * prol_term list;
    1.13 +  datatype prem = Conj of prem list
    1.14 +    | Rel of string * prol_term list | NotRel of string * prol_term list
    1.15 +    | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
    1.16 +    | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
    1.17 +      
    1.18    type clause = ((string * prol_term list) * prem);
    1.19    type logic_program = clause list;
    1.20    type constant_table = (string * string) list
    1.21 @@ -36,17 +40,29 @@
    1.22  
    1.23  (* internal program representation *)
    1.24  
    1.25 +datatype arith_op = Plus | Minus
    1.26 +
    1.27  datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
    1.28 -  | Number of int;
    1.29 +  | Number of int | ArithOp of arith_op * prol_term list;
    1.30 +
    1.31 +fun is_Var (Var _) = true
    1.32 +  | is_Var _ = false
    1.33 +
    1.34 +fun is_arith_term (Var _) = true
    1.35 +  | is_arith_term (Number _) = true
    1.36 +  | is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands
    1.37 +  | is_arith_term _ = false
    1.38  
    1.39  fun string_of_prol_term (Var s) = "Var " ^ s
    1.40    | string_of_prol_term (Cons s) = "Cons " ^ s
    1.41    | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
    1.42    | string_of_prol_term (Number n) = "Number " ^ string_of_int n
    1.43  
    1.44 -datatype prem = Conj of prem list | NotRel of string * prol_term list
    1.45 -    | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
    1.46 -
    1.47 +datatype prem = Conj of prem list
    1.48 +  | Rel of string * prol_term list | NotRel of string * prol_term list
    1.49 +  | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
    1.50 +  | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
    1.51 +    
    1.52  fun dest_Rel (Rel (c, ts)) = (c, ts)
    1.53   
    1.54  type clause = ((string * prol_term list) * prem);
    1.55 @@ -83,6 +99,10 @@
    1.56    
    1.57  (** translation of terms, literals, premises, and clauses **)
    1.58  
    1.59 +fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus
    1.60 +  | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
    1.61 +  | translate_arith_const _ = NONE
    1.62 +
    1.63  fun translate_term ctxt constant_table t =
    1.64    case try HOLogic.dest_number t of
    1.65      SOME (@{typ "int"}, n) => Number n
    1.66 @@ -91,20 +111,29 @@
    1.67          (Free (v, T), []) => Var v 
    1.68        | (Const (c, _), []) => Cons (translate_const constant_table c)
    1.69        | (Const (c, _), args) =>
    1.70 -        AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)
    1.71 +        (case translate_arith_const c of
    1.72 +          SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
    1.73 +        | NONE =>                                                             
    1.74 +            AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
    1.75        | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
    1.76  
    1.77  fun translate_literal ctxt constant_table t =
    1.78    case strip_comb t of
    1.79      (Const (@{const_name "op ="}, _), [l, r]) =>
    1.80 -      Eq (pairself (translate_term ctxt constant_table) (l, r))
    1.81 +      let
    1.82 +        val l' = translate_term ctxt constant_table l
    1.83 +        val r' = translate_term ctxt constant_table r
    1.84 +      in
    1.85 +        (if is_Var l' andalso is_arith_term r' then ArithEq else Eq) (l', r')
    1.86 +      end
    1.87    | (Const (c, _), args) =>
    1.88        Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
    1.89    | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
    1.90  
    1.91  fun NegRel_of (Rel lit) = NotRel lit
    1.92    | NegRel_of (Eq eq) = NotEq eq
    1.93 -  
    1.94 +  | NegRel_of (ArithEq eq) = NotArithEq eq
    1.95 +
    1.96  fun translate_prem ctxt constant_table t =  
    1.97      case try HOLogic.dest_not t of
    1.98        SOME t => NegRel_of (translate_literal ctxt constant_table t)
    1.99 @@ -164,9 +193,13 @@
   1.100  
   1.101  (* code printer *)
   1.102  
   1.103 +fun write_arith_op Plus = "+"
   1.104 +  | write_arith_op Minus = "-"
   1.105 +
   1.106  fun write_term (Var v) = first_upper v
   1.107    | write_term (Cons c) = c
   1.108 -  | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
   1.109 +  | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
   1.110 +  | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
   1.111    | write_term (Number n) = string_of_int n
   1.112  
   1.113  fun write_rel (pred, args) =
   1.114 @@ -177,6 +210,8 @@
   1.115    | write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
   1.116    | write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
   1.117    | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
   1.118 +  | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r
   1.119 +  | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r
   1.120  
   1.121  fun write_clause (head, prem) =
   1.122    write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")