A starting point might be to use the function real_to_arbrat in binary_ieeeLib.
https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/floating-point
For example, the following is one method to get a result:
fun arbrat_to_math_real x =
Real./ (Real.fromInt (Arbint.toInt (Arbrat.numerator x)),
Real.fromInt (Arbnum.toInt (Arbrat.denominator x)))
val real_to_math_real = arbrat_to_math_real o real_to_arbrat
Math.exp (real_to_math_real ``0.4``)
> val it = 1.491824698: real
Anthony
> On 27 May 2016, at 07:56, Michael Norrish <michael.norr...@nicta.com.au>
> wrote:
>
> It depends on what term-structure you expect to see as the argument to exp.
> If, for example, you were only going to see integer literals there, you could
> just use realSyntax.int_of_term:
>
> > realSyntax.int_of_term ``4:real``;
> val it = 4i: Arbint.int
> > realSyntax.int_of_term ``-5:real``;
> val it = -5i: Arbint.int
>
> But if you expected to see fractions there too, you would have to combine the
> above with realSyntax.dest_div:
>
> > realSyntax.dest_div ``4 / 5 : real``;
> val it = (``4``, ``5``): term * term
>
> Note that decimal numbers are really fractions:
>
> > realSyntax.dest_div ``3.14``;
> val it = (``314``, ``100``): term * term
>
> It would be nice to combine all of the above to give a
>
> realLit_to_rat
>
> function of type term -> Arbrat.rat.
>
> You could presumably special-case other interesting constants like pi and e,
> though you'd have to then decide what precision you wanted in your rational
> output. Note also that Arbrat.rat is not the same type as the SML
> implementation's real type.
>
> Michael
>
>> On 27 May 2016, at 15:14, Waqar Ahmad <12phdwah...@seecs.edu.pk
>> <mailto:12phdwah...@seecs.edu.pk>> wrote:
>>
>> Hi all,
>>
>> I am trying to translate some defined HOL4 functions to their equivalent
>> functions in SML. For instance, there is a function "exp ": real->real in a
>> HOL4 'transcTheory' and I want to compute it using a similar SML function
>> `Math.exp`.
>>
>> So, I have written a translator function as follows:
>>
>> fun sml_of_hol_real_exp t =
>> let val failstring = "Symbolic expression could not be translated in a
>> number" in
>> if fst (dest_comb t) = ``exp:real->real`` then
>>
>> Math.exp <TERM TO REAL> (snd (dest_comb t))
>> else failwith failstring
>> end;
>>
>> A possible usage of above function can be sml_of_hol_real_exp ``exp 0.4``;
>>
>> Now, I need a kind of operator in place of <TERM TO REAL> that can give an
>> argument to Math.exp function for computation... Can anybody have an idea
>> about this?
>>
>> --
>> Thanks and best regards,
>>
>> Waqar Ahmed
>>
>>
>> ------------------------------------------------------------------------------
>> What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
>> patterns at an interface-level. Reveals which users, apps, and protocols are
>> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
>> J-Flow, sFlow and other flows. Make informed decisions using capacity
>> planning
>> reports.https://ad.doubleclick.net/ddm/clk/305295220;132659582;e_______________________________________________
>>
>> <https://ad.doubleclick.net/ddm/clk/305295220;132659582;e_______________________________________________>
>> hol-info mailing list
>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
> The information in this e-mail may be confidential and subject to legal
> professional privilege and/or copyright. National ICT Australia Limited
> accepts no liability for any damage caused by this email or its attachments.
> ------------------------------------------------------------------------------
> What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
> patterns at an interface-level. Reveals which users, apps, and protocols are
> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
> J-Flow, sFlow and other flows. Make informed decisions using capacity
> planning reports.
> https://ad.doubleclick.net/ddm/clk/305295220;132659582;e_______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
