1(* Title: HOL/Tools/numeral.ML 2 Author: Makarius 3 4Logical and syntactic operations on numerals (see also HOL/Tools/hologic.ML). 5*) 6 7signature NUMERAL = 8sig 9 val mk_cnumber: ctyp -> int -> cterm 10 val mk_number_syntax: int -> term 11 val dest_num_syntax: term -> int 12 val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory 13end; 14 15structure Numeral: NUMERAL = 16struct 17 18(* numeral *) 19 20fun dest_num_syntax (Const (@{const_syntax Num.Bit0}, _) $ t) = 2 * dest_num_syntax t 21 | dest_num_syntax (Const (@{const_syntax Num.Bit1}, _) $ t) = 2 * dest_num_syntax t + 1 22 | dest_num_syntax (Const (@{const_syntax Num.One}, _)) = 1; 23 24fun mk_num_syntax n = 25 if n > 0 then 26 (case IntInf.quotRem (n, 2) of 27 (0, 1) => Syntax.const @{const_syntax One} 28 | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n 29 | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n) 30 else raise Match 31 32fun mk_cbit 0 = @{cterm "Num.Bit0"} 33 | mk_cbit 1 = @{cterm "Num.Bit1"} 34 | mk_cbit _ = raise CTERM ("mk_cbit", []); 35 36fun mk_cnumeral i = 37 let 38 fun mk 1 = @{cterm "Num.One"} 39 | mk i = 40 let val (q, r) = Integer.div_mod i 2 in 41 Thm.apply (mk_cbit r) (mk q) 42 end 43 in 44 if i > 0 then mk i else raise CTERM ("mk_cnumeral: negative input", []) 45 end 46 47 48(* number *) 49 50local 51 52val cterm_of = Thm.cterm_of @{context}; 53fun tvar S = (("'a", 0), S); 54 55val zero_tvar = tvar @{sort zero}; 56val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar)); 57 58val one_tvar = tvar @{sort one}; 59val one = cterm_of (Const (@{const_name one_class.one}, TVar one_tvar)); 60 61val numeral_tvar = tvar @{sort numeral}; 62val numeral = cterm_of (Const (@{const_name numeral}, @{typ num} --> TVar numeral_tvar)); 63 64val uminus_tvar = tvar @{sort uminus}; 65val uminus = cterm_of (Const (@{const_name uminus}, TVar uminus_tvar --> TVar uminus_tvar)); 66 67fun instT T v = Thm.instantiate_cterm ([(v, T)], []); 68 69in 70 71fun mk_cnumber T 0 = instT T zero_tvar zero 72 | mk_cnumber T 1 = instT T one_tvar one 73 | mk_cnumber T i = 74 if i > 0 then 75 Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral i) 76 else 77 Thm.apply (instT T uminus_tvar uminus) 78 (Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral (~ i))); 79 80end; 81 82fun mk_number_syntax n = 83 if n = 0 then Syntax.const @{const_syntax Groups.zero} 84 else if n = 1 then Syntax.const @{const_syntax Groups.one} 85 else Syntax.const @{const_syntax numeral} $ mk_num_syntax n; 86 87 88(* code generator *) 89 90local open Basic_Code_Thingol in 91 92fun dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1 93 | dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) = 94 (case dest_num_code t of 95 SOME n => SOME (2 * n) 96 | _ => NONE) 97 | dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) = 98 (case dest_num_code t of 99 SOME n => SOME (2 * n + 1) 100 | _ => NONE) 101 | dest_num_code _ = NONE; 102 103fun add_code number_of preproc print target thy = 104 let 105 fun pretty literals _ thm _ _ [(t, _)] = 106 case dest_num_code t of 107 SOME n => (Code_Printer.str o print literals o preproc) n 108 | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"; 109 in 110 thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of, 111 [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) 112 end; 113 114end; (*local*) 115 116end; 117