Quelle numeral_syntax.ML Sprache: SML

(*  Title:      ZF/Tools/numeral_syntax.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Concrete syntax for generic numerals.
*)

signature NUMERAL_SYNTAX =
sig
  val make_binary: int -> int list
  val dest_binary: int list -> int
end;

structure Numeral_Syntax: NUMERAL_SYNTAX =
struct

(* bits *)

fun mk_bit 0 = Syntax.const \<^const_syntax>\<open>zero\<close>
  | mk_bit 1 = Syntax.const \<^const_syntax>\<open>succ\<close> $ Syntax.const \<^const_syntax>\<open>zero\<close>
  | mk_bit _ = raise Fail "mk_bit";

fun dest_bit (Const (\<^const_syntax>\<open>zero\<close>, _)) = 0
  | dest_bit (Const (\<^const_syntax>\<open>one\<close>, _)) = 1
  | dest_bit (Const (\<^const_syntax>\<open>succ\<close>, _) $ Const (\<^const_syntax>\<open>zero\<close>, _)) = 1
  | dest_bit _ = raise Match;

(* bit strings *)

fun make_binary 0 = []
  | make_binary ~1 = [~1]
  | make_binary n = (n mod 2) :: make_binary (n div 2);

fun dest_binary [] = 0
  | dest_binary (b :: bs) = b + 2 * dest_binary bs;

(*try to handle superfluous leading digits nicely*)
fun prefix_len _ [] = 0
  | prefix_len pred (x :: xs) =
      if pred x then 1 + prefix_len pred xs else 0;

fun mk_bin i =
  let
    fun term_of [] = Syntax.const \<^const_syntax>\<open>Pls\<close>
      | term_of [~1] = Syntax.const \<^const_syntax>\<open>Min\<close>
      | term_of (b :: bs) = Syntax.const \<^const_syntax>\<open>Bit\<close> $ term_of bs $ mk_bit b;
  in term_of (make_binary i) end;

fun bin_of (Const (\<^const_syntax>\<open>Pls\<close>, _)) = []
  | bin_of (Const (\<^const_syntax>\<open>Min\<close>, _)) = [~1]
  | bin_of (Const (\<^const_syntax>\<open>Bit\<close>, _) $ bs $ b) = dest_bit b :: bin_of bs
  | bin_of _ = raise Match;

(*Leading 0s and (for negative numbers) -1s cause complications, though they
  should never arise in normal use. The formalization used in HOL prevents
  them altogether.*)
fun show_int t =
  let
    val rev_digs = bin_of t;
    val (c, zs) =
      (case rev rev_digs of
         ~1 :: bs => (\<^syntax_const>\<open>_Neg_Int\<close>, prefix_len (equal 1) bs)
      | bs => (\<^syntax_const>\<open>_Int\<close>,  prefix_len (equal 0) bs));
    val num = string_of_int (abs (dest_binary rev_digs));
  in (c, implode (replicate zs "0") ^ num) end;

(* translation of integer constant tokens to and from binary *)

fun int_tr [Free (s, _)] =
      Syntax.const \<^const_syntax>\<open>integ_of\<close> $ mk_bin (#value (Lexicon.read_num s))
  | int_tr ts = raise TERM ("int_tr", ts);

fun neg_int_tr [Free (s, _)] =
      Syntax.const \<^const_syntax>\<open>integ_of\<close> $ mk_bin (~ (#value (Lexicon.read_num s)))
  | neg_int_tr ts = raise TERM ("neg_int_tr", ts);

fun integ_of_tr' [t] =
      let val (c, s) = show_int t
      in Syntax.const c $ Syntax.free s end
  | integ_of_tr' _ = raise Match;

val _ = Theory.setup
(Sign.parse_translation
   [(\<^syntax_const>\<open>_Int\<close>, K int_tr),
    (\<^syntax_const>\<open>_Neg_Int\<close>, K neg_int_tr)] #>
  Sign.print_translation
   [(\<^const_syntax>\<open>integ_of\<close>, K integ_of_tr')]);

end;

quality100%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

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.