[01:18:28] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 246 seconds) [01:40:52] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [07:25:32] wmacmil: https://gist.github.com/inariksit/5103fd97e9de6d02c67d21c9cda7a908 this is what I talked about on tuesday [07:43:08] using the idea from https://github.com/michmech/plausibility#readme [07:43:39] so the grammar generates all natural numbers, but it only linearises "ok" for those that are divisible by 3 [09:18:40] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 246 seconds) [10:19:01] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [10:23:16] :) @inari [10:42:45] so one additional question I have [10:44:56] suppose you didn't have Int as a predefined category [10:45:13] and you just wanted a program to parse the natural numbers {0 , 1 , 2 , ...} [10:46:01] because aarne has this as an example for computing a tree in the tutorial [10:46:02] > parse -tr "1 + 1" | put_term -transform=compute -tr | l [10:46:02] plus one one [10:46:02] Succ (Succ Zero) [10:46:02] s(s(0)) [10:46:10] but he never gives the concrete syntax [10:46:25] so i don't know if its presumed to use the predefined int category [10:46:59] or if you'd have to have a language with functions zero, one, two, ... , nine [10:47:41] and then basically at the ast level, using semantic definitions, compute [10:48:37] so for instance, appendNat : Nat -> Nat -> Nat [10:49:44] and then define eleven = appendNat one one [10:49:49] or something like that? [10:51:02] because I'm curious if it would be straightforward to extend your gist soas to actually parse strings of the form {0 , 3, 6, ...}, [10:51:23] and my initial supposition that you would need some black magic at the Abstract level? [10:58:26] (ignoring the fact that you might have to have whitespace between numbers which can be fixed with pre/postprocessing) [11:10:49] wmacmil: yes, the lack of concrete syntax for that program is strange [11:11:15] I asked this question on SO, and nobody has answered so far https://stackoverflow.com/questions/55883172/grammatical-framework-linearization-type-field-cannot-be-int-how-to-write-a [11:11:50] I just answered one silly way to deal with ints in https://github.com/GrammaticalFramework/gf-core/issues/91#issuecomment-764332821 [11:12:00] but that's not really a solution [11:12:12] how did your meeting with aarne go? [11:13:51] its later today [11:14:07] ah right [11:14:22] if you find out the answer, let me know :-D [11:14:56] daherb had another solution which was just to output "+1" for each Succ, and then evaluate the string in some external program [11:17:32] also, whatsup with this error [11:17:33] https://stackoverflow.com/questions/55883172/grammatical-framework-linearization-type-field-cannot-be-int-how-to-write-a [11:17:46] Bin> - compiling Bin.gf... [11:17:46] Bin.gf:16: [11:17:46] Happened in the renaming of plusP [11:17:46] data constructor expected but Bin.Succ is found instead [11:18:15] when i try to verbatim use the definition aarne provides in the book [11:28:52] which page? [13:09:15] well i dunno if its an error [13:10:01] but 155 [13:10:10] anyways, the pt command completely doesnt work for me [13:10:15] so i'll just have to ask aarne [13:10:25] i can share a gist if youre interested [13:30:40] yeah please do, I am interested [13:52:41] https://gist.github.com/wmacmil/56c286f0877933507fc800be24a6cc5f [13:53:48] ok now im getting this error [13:53:49] > gr [13:53:49] empty grammar, no abstract [13:53:49] CallStack (from HasCallStack): [13:53:49] error, called at src/runtime/haskell/PGF/Data.hs:100:15 in gf-3.10.4-BNI84g7Cbh1LvYlghrRUOG:PGF.Data [13:53:49] > [13:53:59] which was actually happening earlier [13:54:07] you just need to give -cat=Nat to gr [13:54:37] still, [13:54:38] gr -cat=Nat [13:54:38] empty grammar, no abstract [13:54:38] CallStack (from HasCallStack): [13:54:38] error, called at src/runtime/haskell/PGF/Data.hs:100:15 in gf-3.10.4-BNI84g7Cbh1LvYlghrRUOG:PGF.Data [13:54:39] > [13:54:45] oh you do have flags startcat=Nat [13:55:41] this seems to happen all the time, and i feel like i'm cursed. something works, I don't touch it, and then it doesn't [13:55:45] right, you get that eror because the grammar didn't load [13:56:23] okay let me look at the original error [13:56:29] so does this comment mean it didnt load [13:56:29] gr -cat=Nat [13:56:29] empty grammar, no abstract [13:56:29] CallStack (from HasCallStack): [13:56:29] error, called at src/runtime/haskell/PGF/Data.hs:100:15 in gf-3.10.4-BNI84g7Cbh1LvYlghrRUOG:PGF.Data [13:56:30] > [13:56:34] yes [13:56:47] > - compiling bin.gf... [13:56:47] bin.gf:18: [13:56:47] happened in the renaming of plusn [13:56:47] data constructor expected but bin.succ is found instead [13:56:49] i mean that [13:56:51] sorry [13:56:51] if you only have > in the GF shell, either you have imported the grammar with -retain, or you don't have a grammar loaded [13:56:58] ah yes [13:57:37] does the > - compiling bin.gf... [13:57:37] [13:57:43] > - compiling Bin.gf... write file Bin.gfo [13:57:43] - compiling BinEng.gf... [13:57:43] BinEng.gf: [13:57:43] Warning: no linearization of plusN [13:57:43] write file BinEng.gfo [13:57:44] linking ... OK [13:57:56] even though the file is named Bin.gf mean something [13:57:57] Bin> [13:58:17] when you have the name of the grammar before the >, then it has loaded [13:58:28] so why isn't it even loading [13:58:54] it does when i get rid of the data judgement [13:59:00] i mean def, not data [13:59:21] it's not loading if there's any error [14:00:45] but i don't understand how to debug the fail to load error [14:00:57] because the def keyword works with One [14:01:01] just not plusN [14:01:06] which uses pattern matching [14:01:57] and I also don't know where the Sum thing is coming from [14:02:26] yeah it looks like aarne has forgotten something [14:02:59] or plusN used to be called Sum [14:04:25] one mroe thing to ask aarne [14:04:43] ok, will do [14:04:43] ! [14:05:54] did you get this error too [14:05:55] conflicting information in module Bin [14:05:55] data One : Nat ; [14:05:55] and [14:05:56] def One = Succ Zero ; [14:06:13] I just tried to change fun to data [14:06:26] no i didnt try the data [14:07:07] now i get that when i do [14:07:21] yeah [14:11:13] I got it [14:11:27] data [14:11:27] Zero : Nat ; [14:11:27] Succ : Nat -> Nat ; [14:11:27] fun [14:11:27] plusN : Nat -> Nat -> Nat ; [14:11:29] One : Nat ; [14:11:38] ah! [14:11:39] so zero and succ as data, the rest as fun [14:11:44] def [14:11:44] plusN x Zero = x ; [14:11:44] plusN x (Succ y) = Succ (plusN x y) ; [14:11:45] One = Succ Zero ; [14:11:49] [14:11:57] also I changed Sum to plusN [14:12:00] now it compiles [14:12:39] clever! [14:12:53] for the errata i guess [14:15:09] p -tr "1 + 1" | pt -compute -tr | l [14:15:09] plusN One One [14:15:09] Succ (Succ Zero) [14:15:09] s s 0 [14:15:16] thank you again! [14:15:19] nice! [14:37:47] an additional confusing [14:37:53] I'm not getting this type checking error [14:37:54] ExpEng.gf: [14:37:54] ExpEng.gf:36: [14:37:54] Happened in linearization of Let [14:37:54] type of e.s [14:37:54] expected: {s : Str; p : Predef.Ints 5} [14:37:56] inferred: Str [14:38:07] where Let ld e = mkPrec 0 ("let" ++ ld ++ "in" ++ (usePrec 0 e.s)) ; [14:38:28] Let : [Decl] -> Exp -> Exp ; [14:38:51] lincat Exp = TermPrec ; [14:41:25] what's the Exp grammar? [14:41:45] what i was showing you the other day [14:41:49] the actual thesis work [14:41:50] aha [14:42:19] I need to go now, but just check the lincats and see what's wrong [14:42:30] is lincat [Decl] actually a string? [14:42:32] Str [14:42:49] https://github.com/wmacmil/AgdaGrammar [14:43:04] yea it is [14:43:13] but no worries, thanks again for the enormous amounts of help [14:43:34] okay, so it's the e.s [14:43:41] lincat of Exp is Str, not {s : Str} [14:44:00] but yeah now I'm off [14:44:03] \o [14:44:32] :) [21:54:09] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 264 seconds)