avoid ML structure aliases (especially single-letter abbreviations)
authorboehmes
Wed Feb 02 14:01:09 2011 +0100 (2011-02-02)
changeset 416918f0531cf34f8
parent 41689 3e39b0e730d6
child 41692 0593a2979cd3
avoid ML structure aliases (especially single-letter abbreviations)
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/z3_interface.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Feb 02 12:34:45 2011 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Feb 02 14:01:09 2011 +0100
     1.3 @@ -58,10 +58,9 @@
     1.4  (* Z3 constructors *)
     1.5  
     1.6  local
     1.7 -  structure I = Z3_Interface
     1.8 -
     1.9 -  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
    1.10 -    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
    1.11 +  fun z3_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME @{typ real}
    1.12 +    | z3_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME @{typ real}
    1.13 +        (*FIXME: delete*)
    1.14      | z3_mk_builtin_typ _ = NONE
    1.15  
    1.16    fun z3_mk_builtin_num _ i T =
    1.17 @@ -76,15 +75,23 @@
    1.18    val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
    1.19    val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    1.20  
    1.21 -  fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.22 -    | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
    1.23 -    | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
    1.24 -    | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
    1.25 -    | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
    1.26 -    | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
    1.27 -    | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
    1.28 -    | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
    1.29 -    | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
    1.30 +  fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.31 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) [ct, cu] =
    1.32 +        SOME (mk_add ct cu)
    1.33 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] =
    1.34 +        SOME (mk_sub ct cu)
    1.35 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] =
    1.36 +        SOME (mk_mul ct cu)
    1.37 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] =
    1.38 +        SOME (mk_div ct cu)
    1.39 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] =
    1.40 +        SOME (mk_lt ct cu)
    1.41 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] =
    1.42 +        SOME (mk_le ct cu)
    1.43 +    | z3_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] =
    1.44 +        SOME (mk_lt cu ct)
    1.45 +    | z3_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] =
    1.46 +        SOME (mk_le cu ct)
    1.47      | z3_mk_builtin_fun _ _ = NONE
    1.48  in
    1.49  
     2.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Feb 02 12:34:45 2011 +0100
     2.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Feb 02 14:01:09 2011 +0100
     2.3 @@ -25,9 +25,6 @@
     2.4  structure Z3_Interface: Z3_INTERFACE =
     2.5  struct
     2.6  
     2.7 -structure U = SMT_Utils
     2.8 -structure B = SMT_Builtin
     2.9 -
    2.10  val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
    2.11  
    2.12  
    2.13 @@ -72,9 +69,9 @@
    2.14      else (thms, extra_thms)
    2.15  
    2.16    val setup_builtins =
    2.17 -    B.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
    2.18 -    B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
    2.19 -    B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
    2.20 +    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
    2.21 +    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
    2.22 +    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
    2.23  in
    2.24  
    2.25  val setup = Context.theory_map (
    2.26 @@ -150,31 +147,41 @@
    2.27  fun mk_nary _ cu [] = cu
    2.28    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
    2.29  
    2.30 -val eq = U.mk_const_pat @{theory} @{const_name HOL.eq} U.destT1
    2.31 -fun mk_eq ct cu = Thm.mk_binop (U.instT' ct eq) ct cu
    2.32 +val eq = SMT_Utils.mk_const_pat @{theory} @{const_name HOL.eq} SMT_Utils.destT1
    2.33 +fun mk_eq ct cu = Thm.mk_binop (SMT_Utils.instT' ct eq) ct cu
    2.34  
    2.35 -val if_term = U.mk_const_pat @{theory} @{const_name If} (U.destT1 o U.destT2)
    2.36 -fun mk_if cc ct cu = Thm.mk_binop (Thm.capply (U.instT' ct if_term) cc) ct cu
    2.37 +val if_term =
    2.38 +  SMT_Utils.mk_const_pat @{theory} @{const_name If}
    2.39 +    (SMT_Utils.destT1 o SMT_Utils.destT2)
    2.40 +fun mk_if cc ct cu =
    2.41 +  Thm.mk_binop (Thm.capply (SMT_Utils.instT' ct if_term) cc) ct cu
    2.42  
    2.43 -val nil_term = U.mk_const_pat @{theory} @{const_name Nil} U.destT1
    2.44 -val cons_term = U.mk_const_pat @{theory} @{const_name Cons} U.destT1
    2.45 +val nil_term =
    2.46 +  SMT_Utils.mk_const_pat @{theory} @{const_name Nil} SMT_Utils.destT1
    2.47 +val cons_term =
    2.48 +  SMT_Utils.mk_const_pat @{theory} @{const_name Cons} SMT_Utils.destT1
    2.49  fun mk_list cT cts =
    2.50 -  fold_rev (Thm.mk_binop (U.instT cT cons_term)) cts (U.instT cT nil_term)
    2.51 +  fold_rev (Thm.mk_binop (SMT_Utils.instT cT cons_term)) cts
    2.52 +    (SMT_Utils.instT cT nil_term)
    2.53  
    2.54 -val distinct = U.mk_const_pat @{theory} @{const_name distinct}
    2.55 -  (U.destT1 o U.destT1)
    2.56 +val distinct = SMT_Utils.mk_const_pat @{theory} @{const_name distinct}
    2.57 +  (SMT_Utils.destT1 o SMT_Utils.destT1)
    2.58  fun mk_distinct [] = mk_true
    2.59    | mk_distinct (cts as (ct :: _)) =
    2.60 -      Thm.capply (U.instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
    2.61 +      Thm.capply (SMT_Utils.instT' ct distinct)
    2.62 +        (mk_list (Thm.ctyp_of_term ct) cts)
    2.63  
    2.64 -val access = U.mk_const_pat @{theory} @{const_name fun_app} U.destT1
    2.65 -fun mk_access array = Thm.capply (U.instT' array access) array
    2.66 +val access =
    2.67 +  SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} SMT_Utils.destT1
    2.68 +fun mk_access array = Thm.capply (SMT_Utils.instT' array access) array
    2.69  
    2.70 -val update = U.mk_const_pat @{theory} @{const_name fun_upd}
    2.71 -  (Thm.dest_ctyp o U.destT1)
    2.72 +val update = SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd}
    2.73 +  (Thm.dest_ctyp o SMT_Utils.destT1)
    2.74  fun mk_update array index value =
    2.75    let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
    2.76 -  in Thm.capply (Thm.mk_binop (U.instTs cTs update) array index) value end
    2.77 +  in
    2.78 +    Thm.capply (Thm.mk_binop (SMT_Utils.instTs cTs update) array index) value
    2.79 +  end
    2.80  
    2.81  val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
    2.82  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
    2.83 @@ -220,10 +227,10 @@
    2.84  (* abstraction *)
    2.85  
    2.86  fun is_builtin_theory_term ctxt t =
    2.87 -  if B.is_builtin_num ctxt t then true
    2.88 +  if SMT_Builtin.is_builtin_num ctxt t then true
    2.89    else
    2.90      (case Term.strip_comb t of
    2.91 -      (Const c, ts) => B.is_builtin_fun ctxt c ts
    2.92 +      (Const c, ts) => SMT_Builtin.is_builtin_fun ctxt c ts
    2.93      | _ => false)
    2.94  
    2.95  end