corrected translation of integer operators,
authorboehmes
Fri Nov 13 15:06:19 2009 +0100 (2009-11-13)
changeset 3366131a129cc0d10
parent 33660 11574d52169d
child 33662 7be6ee4ee67f
corrected translation of integer operators,
keep argument order for n-ary symbols (conjunction, disjunction),
removed unused code
src/HOL/Boogie/Tools/boogie_loader.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 13 15:02:51 2009 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 13 15:06:19 2009 +0100
     1.3 @@ -58,7 +58,6 @@
     1.4          SOME type_name => ((type_name, false), thy)
     1.5        | NONE =>
     1.6            let
     1.7 -            val bname = Binding.name isa_name
     1.8              val args = Name.variant_list [] (replicate arity "'")
     1.9              val (T, thy') =
    1.10                ObjectLogic.typedecl (Binding.name isa_name, args, NoSyn) thy
    1.11 @@ -324,7 +323,7 @@
    1.12  
    1.13  local
    1.14    fun mk_nary _ t [] = t
    1.15 -    | mk_nary f _ (t :: ts) = fold f ts t
    1.16 +    | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts)
    1.17  
    1.18    fun mk_distinct T ts =
    1.19      Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ 
    1.20 @@ -376,7 +375,6 @@
    1.21        val dT = Term.fastype_of t and rT = mk_wordT (msb - lsb)
    1.22        val nT = @{typ nat}
    1.23        val mk_nat_num = HOLogic.mk_number @{typ nat}
    1.24 -      val m = HOLogic.mk_number @{typ nat}
    1.25      in
    1.26        Const (@{const_name boogie_bv_extract}, [nT, nT, dT] ---> rT) $
    1.27          mk_nat_num msb $ mk_nat_num lsb $ t
    1.28 @@ -451,8 +449,8 @@
    1.29        binexp ">" (binop @{term "op < :: int => _"} o swap) ||
    1.30        binexp ">=" (binop @{term "op <= :: int => _"} o swap) ||
    1.31        binexp "+" (binop @{term "op + :: int => _"}) ||
    1.32 -      binexp "-" (binop @{term "op + :: int => _"}) ||
    1.33 -      binexp "*" (binop @{term "op + :: int => _"}) ||
    1.34 +      binexp "-" (binop @{term "op - :: int => _"}) ||
    1.35 +      binexp "*" (binop @{term "op * :: int => _"}) ||
    1.36        binexp "/" (binop @{term boogie_div}) ||
    1.37        binexp "%" (binop @{term boogie_mod}) ||
    1.38        scan_line "select" num :|-- (fn arity =>