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
[http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
------------------------------------------------------------------------------
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<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
