28906

1 
(* ID: $Id$


2 
Authors: Tobias Nipkow, TU Muenchen


3 


4 
Concrete syntax for floats


5 
*)


6 


7 
signature FLOAT_SYNTAX =


8 
sig


9 
val setup: theory > theory


10 
end;


11 


12 
structure FloatSyntax: FLOAT_SYNTAX =


13 
struct


14 


15 
(* parse translation *)


16 


17 
local


18 


19 
fun mk_number i =


20 
let


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


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


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


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


25 
in Syntax.const @{const_name Int.number_of} $ mk i end;


26 


27 
fun mk_frac str =


28 
let


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

32603

30 
val exp = Syntax.const @{const_name Power.power};

28906

31 
val ten = mk_number 10;


32 
val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);

32603

33 
in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end

28906

34 
in


35 


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


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


38 


39 
end;


40 


41 


42 
(* theory setup *)


43 


44 
val setup =


45 
Sign.add_trfuns ([], [("_Float", float_tr)], [], []);


46 


47 
end;
