Re: Real-time OS system state captured by ATS language (and questions)

2016-06-15 Thread Kiwamu Okabe
e chss's int? How to use `lemma_chss`? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-la

Re: Real-time OS system state captured by ATS language (and questions)

2016-06-18 Thread Kiwamu Okabe
etI (pss | tmr_p, MS2ST (POLLING_DELAY), $UN.cast{vtfunc_t}(tmrfunc), bbdp) ``` Are there methods to define envless function typedef includes proof argument? Best regards, -- Kiwamu Okabe -- You received this message because you are subscribed to the Google Groups "ats-lang-users" grou

Re: I found a quine using ATS language

2016-07-01 Thread Kiwamu Okabe
ikipedia.org/wiki/WTFPL -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-users+unsubscr...@googlegroups.com.

[TechnicalReport] "Automatically generate ATS function signature from C header, and incrementally introduce liner type"

2017-02-03 Thread Kiwamu Okabe
's written in Japanese, because it's for PPL2017 which is a Japanese local meeting. But it may be useful, if you can read Japanese documents. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

Re: I'm seeking better way to use global struct

2016-08-19 Thread Kiwamu Okabe
Hi Hongwei, ``` vtypedef struct_foo_impl = $extype_struct"struct foo" of { a = int, p = ptr } ``` And also, we can't use at-view in struct define? I should use cPtr0() in struct? Best regards, -- Kiwamu Okabe -- You received this message because you are subscribed to the Goo

Re: I'm seeking better way to use global struct

2016-08-19 Thread Kiwamu Okabe
tyle, better. The code is well-typed. My thinking is a bad thing? ``` val () = println! !(pfoo->p) // print 10 ``` Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe

Re: I'm seeking better way to use global struct

2016-08-19 Thread Kiwamu Okabe
I can also use same style on primitive type. https://github.com/jats-ug/practice-ats/commit/8c9cb65deed66b814979420e4e06642bf0523e68#diff-d94ce6567e10dc9f5d7c205dc66c3e76R34 Thanks a lot! -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To

Re: I'm seeking better way to use global struct

2016-08-19 Thread Kiwamu Okabe
tally, `$extval` can only maintain viewtype as pointer. Is it right? However, following code is using flat record with well-typed... ``` var buz: @{ a = int, b = ptr } val () = buz.a := 1 ``` Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are sub

Re: I'm seeking better way to use global struct

2016-08-19 Thread Kiwamu Okabe
On Sat, Aug 20, 2016 at 1:54 PM, Hongwei Xi <gmh...@gmail.com> wrote: > In this case, buz is a 'var' (instead of a 'val'). A 'var' is always > a left-value. Thanks. You mean $extval return 'val'. May I use extvar for this purpose? Best regards, -- Kiwamu Okabe at METASEPI DES

Re: I'm seeking better way to use global struct

2016-08-19 Thread Kiwamu Okabe
est way to import struct from C language? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-us

Re: I'm seeking better way to use global struct

2016-08-19 Thread Kiwamu Okabe
think I should pointer to touch global value. Thanks a lot, -- Kiwamu Okabe at METASEPI DESIGN -- 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 t

Re: How to use mutual struct?

2016-08-19 Thread Kiwamu Okabe
Hi Hongwei, On Sat, Aug 20, 2016 at 2:04 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote: > On Sat, Aug 20, 2016 at 1:58 PM, gmhwxi <gmh...@gmail.com> wrote: >> Recursion in views cannot be handled this way. You need to define >> dataviews for this. > > Is it me

How about adding short and ushort primitive type into ATS prelude?

2016-08-20 Thread Kiwamu Okabe
Hi Hongwei, How about adding short and ushort primitive types into ATS prelude? I find needing the primitive types, while seeking C header files in /usr/include. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups &quo

Re: How to use mutual struct?

2016-08-20 Thread Kiwamu Okabe
Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-users+unsubscr...@googlegroups.com. To post to

Re: How to use mutual struct?

2016-08-22 Thread Kiwamu Okabe
On Tue, Aug 23, 2016 at 12:22 AM, gmhwxi <gmh...@gmail.com> wrote: > I see. There is a bit of subtlety here. > > If you write 'p0.x := y0', then the type of 'p0' is required to be non > linear. Uuu-n. Complex. But I think I understand it. Thanks, -- Kiwamu Okabe at METASE

Re: How to use mutual struct?

2016-08-22 Thread Kiwamu Okabe
:29: note: in definition of macro 'ATStmpdec' #define ATStmpdec(tmp, hit) hit tmp ^~~ Makefile:7: recipe for target 'a.out' failed make: *** [a.out] Error 1 ``` ... Why??? Best regards, -- Kiwamu Okabe -- You received this message because you are subscribed

Re: How to use mutual struct?

2016-08-25 Thread Kiwamu Okabe
), ATSPMVcastfn(takeout_struct_foo, atstkind_type(atstype_ptrk), ar g0))) ; ^~~ ``` I think the generated C code casts it into `void`. Why not `void *`? Best regards, -- Kiwamu Okabe -- You received this message because you are subscribed to the Google Groups "ats-lang-users&q

Re: How to use mutual struct?

2016-09-03 Thread Kiwamu Okabe
into ATS. Sorry for my mis-understanding. But how to use it on pure ATS language? Could you point some code about it? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from

Re: How to use dataview for maintaining pointer of pointer?

2016-09-03 Thread Kiwamu Okabe
means the tuple at the address. However my pptr_v's cons has following at-view: (ptr l_nxt) @ l It means the pointer at the address. Not tuple. They are having same structure at the address? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribe

Re: How to use dataview for maintaining pointer of pointer?

2016-09-03 Thread Kiwamu Okabe
mean we specify the list of address out of pptr_v. I think I understand it. However, I can't understand why we can't use termination metric over dataview. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lan

Re: How to use dataview for maintaining pointer of pointer?

2016-09-03 Thread Kiwamu Okabe
, l0:addr, l1:addr, l2:addr) = > | ppptr_v_cons(a, l0, l1, l2) of (ptr l1 @ l0, pptr_v (a, l1, l2)) We can't use induction? Why not terminate it? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

Re: Why we can dereference pointer with {l:addr}?

2016-09-06 Thread Kiwamu Okabe
ps://github.com/jats-ug/practice-ats/blob/7152c355cd60e63cb728ec75e29984eb2cb59f92/deref_null_ptr/main.dats If dereference pointer only {l:agz} like `my_deref`, we can wrap `may_ret_null` function easily. Or I should use some `opt` things for this situation? It's as easy as the `my_deref`? Best rega

Where may I write statics value at function declaration?

2016-09-06 Thread Kiwamu Okabe
of the function declaration B. top of `__selector` argument declaration C. top of `__cmp` argument declaration Is this declaration suitable for the scandir(3) in C? Or does it have some bad things? As example, B's `l1` scope is not only for `__selector` argument declaration? Best regards, -- Kiwamu

Re: Why we can dereference pointer with {l:addr}?

2016-09-06 Thread Kiwamu Okabe
one. http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/main.html If so, why not choose implicit proving (like `my_deref` function) over dereference at-view? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the

Re: Where may I write statics value at function declaration?

2016-09-06 Thread Kiwamu Okabe
andir" It's a simple mistake of my utility. Thanks a lot, -- Kiwamu Okabe at METASEPI DESIGN -- 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: How to use mutual struct?

2016-08-30 Thread Kiwamu Okabe
On Tue, Aug 30, 2016 at 8:18 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote: > By the way, the "aPtr1 style" code is more large than "at-view style" code: > > $ wc -l mutual_struct{2,3}/main.dats > 44 mutual_struct2/main.dats > 53 mutual_struct3/main.

Re: How to use mutual struct?

2016-08-31 Thread Kiwamu Okabe
tle. At first stage, the ATS code includes some structs from C code. At second state, should I re-write the struct as ATS record? If re-write, I'll get more safe design in ATS code? Or which choose struct/record is not important thing? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You re

Re: How to use mutual struct?

2016-08-30 Thread Kiwamu Okabe
patsopt(TRANS2): there are [1] errors in total. exit(ATS): uncaught exception: _2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025) ``` Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups

ATS can't use keyword as record member?

2016-09-16 Thread Kiwamu Okabe
able to use them is so limiting for real programming... Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ema

Re: We can implement Forth backend for ATS2?

2016-10-07 Thread Kiwamu Okabe
That method can shape large application such like the ATS compiler? -- Kiwamu Okabe at METASEPI DESIGN -- 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 t

Re: COGENT: Certified Compilation for a Functional Systems Language

2016-09-22 Thread Kiwamu Okabe
ut c2ats is still yet too limited... Yes. I can't say it's useful for real programming today. If you have more good idea for c2ats, please send me your issue. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lan

Re: How to use mutual struct?

2016-08-27 Thread Kiwamu Okabe
On Sat, Aug 27, 2016 at 4:54 PM, gmhwxi <gmh...@gmail.com> wrote: > Here is some code that may be helpful: > > https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct.dats Thanks a lot. Now, I'm writing the other solution... -- Kiwamu Okabe at METASEPI

Re: How to use mutual struct?

2016-08-26 Thread Kiwamu Okabe
olution. I have not yet my feeling to decide using either ATS or C language in such situation... Thanks a lot, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving e

Re: How to use mutual struct?

2016-08-27 Thread Kiwamu Okabe
Hi Hongwei, On Sat, Aug 27, 2016 at 5:07 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote: > Now, I'm writing the other solution... My answer is following: https://github.com/jats-ug/practice-ats/blob/334c41e981a67153d92fcca25130533c86277619/mutual_struct2/gen.sats https://github.co

Re: How to use mutual struct?

2016-08-26 Thread Kiwamu Okabe
!bar@l2 | p: ptr(l1)): void = { val () = println! ("foo.x = ", p->x) val () = println! ("bar.x = ", p->p->x) } ``` Is it correct? Best regards, -- Kiwamu Okabe -- You received this message because you are subscribed to the Google Groups "ats-lang-users&quo

Re: How to use mutual struct?

2016-08-26 Thread Kiwamu Okabe
an't catch errors caused by NULL pointer. Truly, we have no method to avoid both miss cast and NULL pointer??? Or we can avoid them, if drop mutual struct/record and use singly-pointer-linked struct/record? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because

Re: How to use mutual struct?

2016-08-26 Thread Kiwamu Okabe
] (foo@l | ptr(l)) } Is it impossible to be supported by ATS compiler? Best regards, -- Kiwamu Okabe -- 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 t

Re: How to use mutual struct?

2016-08-25 Thread Kiwamu Okabe
:13: note: in expansion of macro ‘ATSderef’ ATSINSstore(ATSderef(arg0, atsvoid_t0ype), tmp4__1) ; ^~~~ main_dats.c:1114:1: error: invalid use of void expression ATSINSstore(ATSderef(arg0, atsvoid_t0ype), tmp4__1) ; ^~~ ``` Best regards, -- Kiwamu Okabe at METASEPI DESIGN

Re: COGENT: Certified Compilation for a Functional Systems Language

2016-10-01 Thread Kiwamu Okabe
netbsd-src/blob/5e5e739906b4a97b7b08da1d6cd5eaffa1f1/sys/ufs/ffs/ffs_snapshot.c#L1584 How to translate them into ATS code without any exception, automatically? Some state machine is needed for it? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you

Re: COGENT: Certified Compilation for a Functional Systems Language

2016-10-01 Thread Kiwamu Okabe
id generated code is useful for manually proving?" And also `goto` statement issue is big problem... Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this grou

Re: COGENT: Certified Compilation for a Functional Systems Language

2016-10-01 Thread Kiwamu Okabe
Ah, yes. Memory safety is some easy than proving with at-view. I think I can try this after issue of splitting C headers into treed sats files. Thanks for your advice, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "a

Re: repl

2016-10-10 Thread Kiwamu Okabe
then get a real language that compiles to c/++ > on top of it, to somehow get a repl? > then since it is c/++ it is portable to android, and then also > becomes faster for releases because then it gets compiled. I think it's a good idea. Best regards, -- Kiwamu Okabe at METASEPI

Re: nifty f* -> c

2016-10-22 Thread Kiwamu Okabe
On Sat, Oct 22, 2016 at 3:49 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote: > On Fri, Oct 21, 2016 at 2:47 AM, Raoul Duke <rao...@gmail.com> wrote: >> http://goo.gl/qSf6hF > > Good news for me! https://github.com/FStarLang/kremlin/blob/master/test/ML16.fst This examp

Re: We can implement Forth backend for ATS2?

2016-10-11 Thread Kiwamu Okabe
JavaScript" after building c2ats product. Thanks for your advice, -- Kiwamu Okabe at METASEPI DESIGN -- 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,

Re: Ask/Answer ATS-related questions on StackOverflow

2016-10-16 Thread Kiwamu Okabe
On Mon, Oct 17, 2016 at 12:31 AM, Steinway Wu <steinway...@gmail.com> wrote: > yes... but not a big issue though. hope we could have more people interested > in ATS and ask questions there. Ah, so you are right. I should be more positive. :) -- Kiwamu Okabe at METASEPI DESIGN --

Re: Ask/Answer ATS-related questions on StackOverflow

2016-10-16 Thread Kiwamu Okabe
the end of 2016 | TechCrunch https://techcrunch.com/2016/06/14/apple-will-require-https-connections-for-ios-apps-by-the-end-of-2016/ So sad... -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

Re: Is the word "sort" overloaded as used in ATS?

2017-03-21 Thread Kiwamu Okabe
On Tue, Mar 21, 2017 at 6:02 PM, spearman <pearman...@gmail.com> wrote: > https://spearman.github.io/ Your page is so great work for me! I think I found it at the start point learning ATS language! -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are s

Re: Embedded driver and funcions for bit manipulation.

2017-08-19 Thread Kiwamu Okabe
and use uncertain bit * Enforce that code doesn't start DMA without setup of buffer Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiv

Re: Embedded driver and funcions for bit manipulation.

2017-08-19 Thread Kiwamu Okabe
a slide to explain the constraint-solver. https://www.slideshare.net/master_q/ats2-updates-2017/5 Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group an

Re: Embedded driver and funcions for bit manipulation.

2017-09-02 Thread Kiwamu Okabe
ign. The seL4's approach may be useful for you. https://ts.data61.csiro.au/publications/nicta_full_text/9118.pdf But please remember it needs much human resource. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "

Re: ATS3: What is it?

2018-10-12 Thread Kiwamu Okabe
Could you write this on https://github.com/githwxi/ATS-Xanadu/blob/master/README ? -- 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

Report: An device driver implemented by ATS language

2018-10-13 Thread Kiwamu Okabe
https://translate.google.com/translate?hl=en=ja=en=http%3A%2F%2Fnamakin.hatenablog.com%2Fentry%2F2018%2F08%2F26%2F092439 -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from

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
associativity Thanks. It's clear for me, now. -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-users+unsubs

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

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: 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/ --

Re: ATS3: ATS/Xanadu

2018-10-19 Thread Kiwamu Okabe
ATS3 core. I just say: "We need some ecosystem on ATS3 core, because someone can shape: * Coq's tactic * Package manager such like atspkg * Assembler backend * Debug support with DWARF * Cross compil ...etc... Some of them should be created by me." Best regards, -- Kiwamu Okabe at ME

Re: ATS3: ATS/Xanadu

2018-10-20 Thread Kiwamu Okabe
DWARF with own ATS own DWARF. Maybe. Best, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-users+unsubscr...

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

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: ATS/Xanadu

2018-10-17 Thread Kiwamu Okabe
I slightly learn Prolog for the design of ATS3. My opinion is following: ## Variable is useful ``` $ cat family.pl father(naoyuki, hyogo). father(saburo, naoyuki). father(saburo, shinji). father(yoshihisa, hisako). mother(hisako, hyogo). mother(yoko, naoyuki). mother(yoko, shinji).

Why my code occurs `unsolved constraint` error?

2018-10-29 Thread Kiwamu Okabe
there are some unsolved constraints: please inspect the above reported error message(s) for information. exit(ATS): uncaught exception: _2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025) make: *** [Makefile:75: utf8.dats.c] Error 1 ``` Best regards, -- Kiwamu Okabe at

Re: Why my code occurs `unsolved constraint` error?

2018-11-01 Thread Kiwamu Okabe
/uemacs-bohai/blob/9ecdd06fe09e6433ed0fb4271c0e5b44d2ad8f8d/DATS/utf8.dats Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-users+

Re: Why my code occurs `unsolved constraint` error?

2018-11-01 Thread Kiwamu Okabe
ned the sort [S2RTerr()]. patsopt(TRANS2): there are [8] errors in total. exit(ATS): uncaught exception: _2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025) ``` Where and what should I inject your annotation? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You

Re: Why my code occurs `unsolved constraint` error?

2018-11-01 Thread Kiwamu Okabe
think "Umm it may needs more addr annotation"? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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, sen

Re: Why my code occurs `unsolved constraint` error?

2018-11-08 Thread Kiwamu Okabe
styles are equivalent. Are there some difference on type inference? > Hongwei I love A style, but I should choose B if it has better inference. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang

Re: Why my code occurs `unsolved constraint` error?

2018-11-08 Thread Kiwamu Okabe
me. I should choose `let in` style. -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-users+unsubscr...@googl

Re: Why need `assertloc` for already branched condition?

2018-11-10 Thread Kiwamu Okabe
nt3.dats: end // end of [S3Ebmul] src/pats_constraint3.dats:| S3Ebmul (x11, x12) => ( src/pats_constraint3.dats: | S3Ebmul (x21, x22) => src/pats_constraint3.dats: ) (* end of [S3Ebmul] *) ``` Above result is hard to understand following: * relationship between `&&` and `bmul`

Re: Why need `assertloc` for already branched condition?

2018-11-11 Thread Kiwamu Okabe
u need; > instead, you can always declare > it on your own. I think above comment doesn't make sense... I would like to use dependent types, which is well defined at prelude or base library. Because it makes manner of code, which is more human readable. Why do I declare my own opera

Re: Why need `assertloc` for already branched condition?

2018-11-09 Thread Kiwamu Okabe
s failed: there are some unsolved constraints: please inspect the above reported error message(s) for information. exit(ATS): uncaught exception: _2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025) ``` Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You

Re: ATS3: ATS/Xanadu

2018-10-10 Thread Kiwamu Okabe
Also I think following are good parts: A. Symbolic execution such like https://github.com/verifast/verifast IDE, because we can watch execution sequence on the IDE. See the following Steps pane on figure 1 at page 4. https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf B.

Re: ATS3: ATS/Xanadu

2018-10-10 Thread Kiwamu Okabe
On Thu, Oct 11, 2018 at 1:40 PM Kiwamu Okabe wrote: > A. Symbolic execution such like https://github.com/verifast/verifast IDE, >because we can watch execution sequence on the IDE. >See the following Steps pane on figure 1 at page 4. >https://people.cs.kuleuven.be/

Re: ATS3: ATS/Xanadu

2018-10-10 Thread Kiwamu Okabe
up to debug it. * The hardware bugs are not caused by ATS language, and stand on hardware registers. * ATS2 has less power to debug such hardware bugs, because the ELF binary has DWARF of C language, not ATS. -- Kiwamu Okabe -- You received this message because you are subscribed to the Google

Re: ATS3: ATS/Xanadu

2018-10-10 Thread Kiwamu Okabe
On Thu, Oct 11, 2018 at 12:07 PM Hongwei Xi wrote: > I hope that I can structure the ATS3 compiler in such a way that you > should be to add DWALF support on your own. Yes. I believe such DWARF support is only hoped by me. -- Kiwamu Okabe at METASEPI DESIGN -- You received this m

Re: ATS2 -> ATS3 Migration Effort

2019-01-15 Thread Kiwamu Okabe
using following library: * https://github.com/vmchale/atspkg/tree/master/language-ats to parse ATS2 code * https://github.com/vmchale/language-xats to print ATS3 code But above ATS3 pretty-printer is not yet written. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this mes

Re: Someone is trying to debug ATS code using DWARF?

2019-05-27 Thread Kiwamu Okabe
Dear Hongwei, On Mon, May 27, 2019 at 7:18 PM Kiwamu Okabe wrote: > Fortunately, I found the following simple method, while learning Vala > language: > > https://gist.github.com/master-q/b8167531a5a0679b9a830ed12a75619f --snip-- > I'll try to write some patch to inject such `#

Re: Someone is trying to debug ATS code using DWARF?

2019-05-27 Thread Kiwamu Okabe
Ah! It's useful!!! ``` (gdb) i b Num Type Disp Enb AddressWhat 1 breakpoint keep y 1.1 y 0x15ee in _057_home_057_kiwamu_057_tmp_057_ats_057_rbtree_057_rbtree_056_dats__rbtree_insert__2__1 at

Re: Someone is trying to debug ATS code using DWARF?

2019-05-28 Thread Kiwamu Okabe
Dear all, I added a Wiki page to explain this post: https://github.com/githwxi/ATS-Postiats/wiki/GDB Thanks, -- Kiwamu Okabe -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving e

Re: Someone is trying to debug ATS code using DWARF?

2019-05-27 Thread Kiwamu Okabe
level=1) global: rbtree_insert$2$5(level=1) global: rbtree_insert$2$6(level=1) global: rbtree_insert$2$7(level=1) global: rbtree_insert$2$8(level=1) global: rbtree_insert$2$9(level=1) ``` Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to th

Re: Someone is trying to debug ATS code using DWARF?

2019-05-27 Thread Kiwamu Okabe
Dear Hongwei, On Tue, May 28, 2019 at 2:15 PM Kiwamu Okabe wrote: > Following means that there are 20 `#line` directives, but gdb only > found 10 of them. > Do you know how to find all of the multiple breakpoints? Sorry. I miss understood it. There are 20 `#line`s, but every insta

Re: ATS-Temptory

2019-05-29 Thread Kiwamu Okabe
On Wed, May 29, 2019 at 3:53 PM Richard wrote: > Assert that the value is true. > > For the definition of tt, see > https://github.com/githwxi/ATS-Temptory/blob/master/libats/basics_pre.sats#L66 Thanks. I think I should learn basic library to understand ATS-Temptory, again. --

Re: ATS-Temptory

2019-05-29 Thread Kiwamu Okabe
What's `val-tt`? -- Kiwamu Okabe -- 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 ats-lang-users+unsubscr...@googlegroups.com. To post to this g

Re: Someone is trying to debug ATS code using DWARF?

2019-05-27 Thread Kiwamu Okabe
Dear all. On Sat, Mar 7, 2015 at 6:44 PM Kiwamu Okabe wrote: > Someone is trying to debug ATS code using DWARF? Fortunately, I found the following simple method, while learning Vala language: https://gist.github.com/master-q/b8167531a5a0679b9a830ed12a75619f ``` $ gcc -g -I /home/kiwamu/

Re: Read IO and Write IO

2019-08-09 Thread Kiwamu Okabe
Dear Hongwei, On Thu, Aug 8, 2019 at 10:24 PM gmhwxi wrote: > We can introduce an abstrace linear VIEW IO: I have a just question. "Why do we separate the IO functions from the pure function?" Unfortunately, I have not felt that such separation is useful... Best regards, --

Re: Tracking effects in ATS

2019-08-08 Thread Kiwamu Okabe
ll,can} optionally introduce effect. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lan

Re: Read IO and Write IO

2019-08-09 Thread Kiwamu Okabe
ite my code without any IO? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lan

Re: Read IO and Write IO

2019-08-09 Thread Kiwamu Okabe
On Sat, Aug 10, 2019 at 10:17 AM Hongwei Xi wrote: > Yes, you should be able to program in the same way as you do now. Thanks. It's good news to port my idiomaticca project to ATS3. -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Gro

A toy translator C to ATS

2019-07-18 Thread Kiwamu Okabe
such as: * Support break, continue, and goto. (Should use some kind of CFG?) * Support pointers using at-view. * Support C headers using .sats files. * Use val instead of var. * Simplify ATS code. Example: reduce multiple let. * Support ATS3. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received

Re: A toy translator C to ATS

2019-07-19 Thread Kiwamu Okabe
our issues with best-effort. https://github.com/metasepi/idiomaticca/issues Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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

Re: Are you interested in building tools for ATS3?

2019-12-16 Thread Kiwamu Okabe
/SATS/dynexp3.sats] is not available for staloading. patsopt(TRANS1): there are [10] errors in total. exit(ATS): uncaught exception: _2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025) make: *** [Makefile:72: BUILD/intrep0_sats.c] Error 1 rm BUILD/intrep0_sats.c ``` Best r

Re: How to assign a `shared` value onto a member of vtype?

2020-08-29 Thread Kiwamu Okabe
ared_unref` not the same? Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-lang-users+unsubscr...@goo

Re: How to assign a `shared` value onto a member of vtype?

2020-08-29 Thread Kiwamu Okabe
entioned by you. But I think I define it but don't use it, because the function ends with `ignoret`. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and s

Re: How to assign a `shared` value onto a member of vtype?

2020-08-29 Thread Kiwamu Okabe
(a:vt@ype) = [l:addr] (a@l | ptr l) ``` Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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 ats-

Re: How to assign a `shared` value onto a member of vtype?

2020-08-29 Thread Kiwamu Okabe
commit/366bb929794285c977339c328daa31c278a28645 I don't know the following technique. ``` var opts: ip6_pktopts with opts_pf // --snip-- val () = assertloc(x = addr@opts) ``` Thank you a lot, Dambaev! -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats

Re: How to assign a `shared` value onto a member of vtype?

2020-08-30 Thread Kiwamu Okabe
Dear Hongwei, On Sun, Aug 30, 2020 at 11:04 PM gmhwxi wrote: > You could also do it by using a type-annotation: --snip-- > prval () = view@opts := (pf_opts: (ip6_pktopts?)@opts) Thank you. It's a new usage for me. -- Kiwamu Okabe at METASEPI DESIGN -- You received this message b

Re: Solving compiler error

2020-08-30 Thread Kiwamu Okabe
assertloc, $showtype and GDB. I'm so happy if you write a show article about $showtype on the Wiki. Because I often forget the usage. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

  1   2   >