Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
Ah... ``` $ git grep infix0 | cat docgen/SYNTAX/fixity.txt:#infix0 foo2 bar2 docgen/SYNTAX/fixity.txt:#infix0 baz of 71 prelude/fixity.sats:#infix0 < <= > >= of 40 prelude/fixity.sats:#infix0 = != == !== of 30 prelude/fixity.sats:#infix0 := of 0 // HX: assign prelude/fixity.sats:#infix0 :=: of 0

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
On Mon, Oct 22, 2018 at 11:59 AM Hongwei Xi wrote: > It is all explained here: > > https://github.com/githwxi/ATS-Xanadu/blob/master/docgen/SYNTAX/fixity.txt > > #infix0 : infix with no associativity > #infixl : infix with left associativity > #infixr : infix with right associativity Thanks.

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
On Mon, Oct 22, 2018 at 11:43 AM Kiwamu Okabe wrote: > How about introduce your infix syntax such like Haskell? > > "Infix Functions In Haskell" > https://wuciawe.github.io/functional%20programming/haskell/2016/07/03/infix-functions-in-haskell.html > > The infix syntax in Haskell has: > > A.

Re: repl?

2018-10-21 Thread Hongwei Xi
A few years back, I looked into to the possibility of using CINT build an REPL for ATS2. Now Cling seems to be under active development: https://root.cern.ch/cling If one wants something performant, this route seems to be promising. On Sun, Oct 21, 2018 at 8:34 PM Vanessa McHale wrote: >

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
I have question: what is different on following?: * #infix0 * #infixl * #infixr How about introduce your infix syntax such like Haskell? "Infix Functions In Haskell" https://wuciawe.github.io/functional%20programming/haskell/2016/07/03/infix-functions-in-haskell.html The infix syntax in

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
As a translator English to Japanese, I would like to choose `po4a` tool. https://po4a.org/index.php.en It can maintain translations on gettext, and be easy to track original update. Could you choose your document format from followings which are supported by po4a: * manpages * POD * XML

Re: ATS3: syntax

2018-10-21 Thread Hongwei Xi
>> text (simple text files with some formatting, markdown, or AsciiDoc) I choose this one: Text + Markdown is what I like most these days :) On Sun, Oct 21, 2018 at 8:17 PM Kiwamu Okabe wrote: > As a translator English to Japanese, I would like to choose `po4a` tool. > >

Re: repl?

2018-10-21 Thread Vanessa McHale
FWIW, I have written ATS2 code that compiles to C which is then wrapped with a Haskell library that GHCi is able to interact with. Have a look here: https://github.com/vmchale/hs-ats/tree/master/fast-arithmetic. You can run cabal new-repl and then λ:> import Numeric.Combinatorics λ:> 400

Re: ATS3: syntax

2018-10-21 Thread Vanessa McHale
You can use pandoc to get manpages, TeX, etc. if you'd like :) On 10/21/18 7:21 PM, Hongwei Xi wrote: > > >> text (simple text files with some formatting, markdown, or AsciiDoc) > > I choose this one: Text + Markdown is what I like most these days :) > > On Sun, Oct 21, 2018 at 8:17 PM Kiwamu

Re: ATS3: ATS/Xanadu

2018-10-21 Thread Kiwamu Okabe
On Sun, Oct 21, 2018 at 8:05 AM Hongwei Xi wrote: > I hope > to be able to export theorems needed by a ATS program to external > theorem-provers. > I think a particular focus should be on automated theorem-proving. Do you use Z3 such like F*? https://www.fstar-lang.org/ -- Kiwamu Okabe at

Re: ATS3: ATS/Xanadu

2018-10-21 Thread gmhwxi
Yes, you can already use ATS2 with Z3: https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ATS-extsolve-z3 On Sunday, October 21, 2018 at 3:19:39 AM UTC-4, Kiwamu Okabe wrote: > > On Sun, Oct 21, 2018 at 8:05 AM Hongwei Xi <...> wrote: > > I hope > > to be able to export theorems

Re: repl?

2018-10-21 Thread gmhwxi
Yes, I have a plan to implement an REPL for ATS3. I expect it to be used primarily for the purpose of learning and debugging. I actually use ATS as a scripting language regularly. Here is an example I put up a while ago: https://github.com/ats-lang/ATS-CodeBook/tree/master/RECIPE/CSV-parsing I

Re: repl?

2018-10-21 Thread Raoul Duke
as i naive day job programmer, i hope that repl/interpreter doesnt have to imply any lack of feature support, so one could still do types & templates & bears oh my. -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this

Re: repl?

2018-10-21 Thread Vanessa McHale
I'm not sure how well that would work. Are there any other heavily-ML-style languages with a REPL? I know Haskell has one but its syntax lends itself to such things. Having a JIT would be wonderful (especially if ATS3 is to be a compilation target) but it's outside of my area of expertise. On

ATS3: syntax

2018-10-21 Thread gmhwxi
I will be working on documenting the syntax of ATS3 from time to time: https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/SYNTAX This is also time for me to clarify my own thoughts. Whenever I implemented ATS in the past, I felt rushed to get things done. This time I am trying to take

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
I think we need `ATS-Xanadu/docgen/SYNTAX/README.md` for table of contents. -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
On Mon, Oct 22, 2018 at 9:04 AM gmhwxi wrote: > Proofs are part of dynamics. As far syntax design is concerned, writing a > proof > is pretty much like writing a program. OK. I should re-draw my big picture: http://jats-ug.metasepi.org/draw/flow.png -- Kiwamu Okabe at METASEPI DESIGN -- You

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
Why not introduce Proof stuff at `overview.txt `? I believe ATS3 stands on: * Dynamics * Proofs * Statics http://cs.likai.org/ats/ml-programmers-guide-to-ats And also the Proofs are important parts for me. -- You received this message because you are subscribed to the Google Groups

Re: ATS3: syntax

2018-10-21 Thread Kiwamu Okabe
If `ATS-Xanadu/docgen/SYNTAX` is a specification document, not a tutorial, we do not need to choose any format such like markdown, TeX, SGML, XML, HTML, etc... Let's choose your style as plain text such like RFC: https://www.rfc-editor.org/in-notes/rfc-index.txt But we need TOC. -- You

Re: ATS3: syntax

2018-10-21 Thread gmhwxi
Proofs are part of dynamics. As far syntax design is concerned, writing a proof is pretty much like writing a program. -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send

Re: ATS3: syntax

2018-10-21 Thread gmhwxi
I don't want to take the RFC route. At least not for now. ATS is too rich and complex to be handle in this way. I am writing some notes now. In these notes, I plan to mostly talk about various syntax entities in ATS3 and also use concrete examples to illustrate them. Once I have written enough