37744

1 
(* Title: HOL/Tools/float_syntax.ML


2 
Author: Tobias Nipkow, TU Muenchen

28906

3 

35115

4 
Concrete syntax for floats.

28906

5 
*)


6 


7 
signature FLOAT_SYNTAX =


8 
sig


9 
val setup: theory > theory


10 
end;


11 

35123

12 
structure Float_Syntax: FLOAT_SYNTAX =

28906

13 
struct


14 


15 
(* parse translation *)


16 


17 
local


18 


19 
fun mk_number i =


20 
let

35115

21 
fun mk 0 = Syntax.const @{const_syntax Int.Pls}


22 
 mk ~1 = Syntax.const @{const_syntax Int.Min}


23 
 mk i =


24 
let val (q, r) = Integer.div_mod i 2


25 
in HOLogic.mk_bit r $ (mk q) end;


26 
in Syntax.const @{const_syntax Int.number_of} $ mk i end;

28906

27 


28 
fun mk_frac str =


29 
let

35115

30 
val {mant = i, exp = n} = Syntax.read_float str;


31 
val exp = Syntax.const @{const_syntax Power.power};

28906

32 
val ten = mk_number 10;

35115

33 
val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;


34 
in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;


35 

28906

36 
in


37 


38 
fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str


39 
 float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);


40 


41 
end;


42 


43 


44 
(* theory setup *)


45 


46 
val setup =

35115

47 
Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);

28906

48 


49 
end;
