Many thanks.. Both the replies are great and clarified many things to me..
Now, I am able to use Anthony fix in my function...:).. The working
translator function is
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 (real_to_math_real (snd (dest_comb t)))
else failwith failstring
end;
sml_of_hol_real_exp ``exp 0.4``;
> val it = 1.49182469764 : real
On Fri, May 27, 2016 at 12:09 PM, Anthony Fox <ac...@cam.ac.uk> wrote:
> 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> 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_______________________________________________
> hol-info mailing list
> 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
>
>
>
--
Thanks and best regards,
Waqar Ahmed
Ph.D Candidate,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad,
Pakistan
------------------------------------------------------------------------------
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
