Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions

Hash: SHA1

Hi Florian,

2013-07-03 19:33 Florian Haftmann:
> Concerning »actively maintained«, there is somebody (namely me)
> who will look after your issue.

Thanks for your encouraging reply!

And, @Cornelius, thanks for your experience report.

> I welcome your effort to carry Isabelle out of the ML/Haskell 
> subculture, but there is one caveat: the code generator for Scala 
> translates HOL's calculus into a functional Scala program without 
> attempting any transformation to idiomize it towards Scala as 
> written by experienced Scala programmes.

I am nowhere near an _experienced_ Scala programmer yet, but
sufficiently capable of writing wrapper functions that, e.g., convert
set[Nat] to List[Int], so this is fine with me.  Replying to
@Cornelius, my application so far is small enough to only require a
few wrapper _functions_, but I'll consider your suggestion of doing
something object-oriented.

Are you suggesting that the code generator creates nicer output for
other target languages?  (I'm just curious; I'm not planning to use
any other language than Scala for now.)

> For illustration, have a look at the generated code.  I never
> heard of any reports how feasible the code is to incorporate in
> bigger Scala applications.

For now, our applications won't be more than thin wrappers around the
generated code, providing some console or file I/O, in a medium-term
perspective maybe a GUI or web interface.  But really just to obtain
input for the Isabelle-generated functions from an end user, and for
displaying the output of the Isabelle-generated functions back to the
end user.



- -- 
Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
  Submission until 12 July;
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
  Submission until 15 July;
→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
Version: GnuPG v2.0.20 (GNU/Linux)
Comment: Using GnuPG with Thunderbird -


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.