Quelle word_lib.ML Sprache: SML

(*  Title:      HOL/Library/Tools/word_lib.ML
    Author:     Sascha Boehme, TU Muenchen and Thomas Sewell, NICTA

Helper routines for operating on the word type.
*)

signature WORD_LIB =
sig
  val dest_binT: typ -> int
  val is_wordT: typ -> bool
  val dest_wordT: typ -> int
  val mk_wordT: int -> typ
end

structure Word_Lib: WORD_LIB =
struct

fun dest_binT T =
  (case T of
    Type (\<^type_name>\<open>Numeral_Type.num0\<close>, _) => 0
  | Type (\<^type_name>\<open>Numeral_Type.num1\<close>, _) => 1
  | Type (\<^type_name>\<open>Numeral_Type.bit0\<close>, [T]) => 2 * dest_binT T
  | Type (\<^type_name>\<open>Numeral_Type.bit1\<close>, [T]) => 1 + 2 * dest_binT T
  | _ => raise TYPE ("dest_binT", [T], []))

fun is_wordT (Type (\<^type_name>\<open>word\<close>, _)) = true
  | is_wordT _ = false

fun dest_wordT (Type (\<^type_name>\<open>word\<close>, [T])) = dest_binT T
  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])

fun mk_bitT i T =
  if i = 0
  then Type (\<^type_name>\<open>Numeral_Type.bit0\<close>, [T])
  else Type (\<^type_name>\<open>Numeral_Type.bit1\<close>, [T])

fun mk_binT size =
  if size = 0 then \<^typ>\<open>Numeral_Type.num0\<close>
  else if size = 1 then \<^typ>\<open>Numeral_Type.num1\<close>
  else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end

fun mk_wordT size =
  if size >= 0 then Type (\<^type_name>\<open>word\<close>, [mk_binT size])
  else raise TYPE ("mk_wordT: " ^ string_of_int size, [], [])

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.