[03:09:38] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 264 seconds) [03:42:00] *** Joins: drbean (~drbean@TC210-63-209-186.static.apol.com.tw) [03:55:16] *** Quits: drbean (~drbean@TC210-63-209-186.static.apol.com.tw) (Ping timeout: 240 seconds) [04:04:07] *** Joins: drbean (~drbean@TC210-63-209-156.static.apol.com.tw) [09:26:48] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [09:56:04] *** Quits: drbean (~drbean@TC210-63-209-156.static.apol.com.tw) (Ping timeout: 256 seconds) [10:52:36] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 240 seconds) [11:37:42] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [11:45:34] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 246 seconds) [12:55:26] *** Joins: wmacmil (~wmacmil@c83-250-118-111.bredband.comhem.se) [13:29:50] i'm trying to get GF Semantic definitions to work, specifically, the def judgement [13:30:00] fun [13:30:02] plusN : N -> N -> N ; [13:30:02] def [13:30:02] plusN x Zer = x ; [13:30:02] plusN x (Suc y) = Suc (plusN x y) ; [13:30:25] this is equivalent to what's in the tuturial & aarne's book up to alpha equivalence [13:30:48] and then i get the following when i try to load it [13:30:49] Harper> - compiling Harper.gf... [13:30:49] Harper.gf:30: [13:30:49] Happened in the renaming of plusN [13:30:49] data constructor expected but Harper.Suc is found instead [13:30:49] Languages: HarperEng [13:30:51] 4 msec [13:31:19] def's do go in the Abstract files, correct? [13:32:09] where the constructors are [13:32:10] fun [13:32:11] Zer : N ; [13:32:11] Suc : N -> N ; [13:43:12] *** Joins: drbean (~drbean@TC210-63-209-142.static.apol.com.tw) [14:11:52] also, sepeartely, whats this error [14:11:53] Types> gr | l [14:11:53] Prelude.!!: index too large [14:40:00] yes, defs go to the abstract syntax! here's an example https://github.com/GrammaticalFramework/gf-rgl/blob/master/src/abstract/Transfer.gf [14:40:59] regarding both of these questions, I found this file which Aarne made in 2011 apparently [14:41:10] gf-contrib/typetheory [14:41:42] but he precedes the definitions of def with another judgement, data [14:41:50] ah, right, there's the thing where you need to introduce funs as data instead [14:42:11] https://github.com/GrammaticalFramework/gf-rgl/blob/master/src/abstract/Numeral.gf#L29 [14:42:18] but this wasn't made explicit in the book [14:42:23] see here, all other stuff in the RGL are defined as fun, but numerals as data [14:42:38] but i think i should be able to hack around it, then [14:43:08] there's a pull request on rgl to do that, just because of that reason :-D https://github.com/GrammaticalFramework/gf-rgl/pull/8 [14:43:48] as for the Prelude.!!: index too large error, I usually get it when I do this [14:43:59] say f : A -> B -> C [14:44:03] and I type gr f ? | l [14:44:15] then gf is sad because it tries to linearise a partially applied fun [14:45:19] so maybe gr gets weird with dependent types/HOAS and generates a partial tree, or then you can get this error for other reasons too [14:45:36] can you do l -treebank or gr -tr | l [14:45:47] so you can see what is the tree that it tries to linearise and fails [14:47:23] ok, thank you [14:47:25] *** Quits: drbean (~drbean@TC210-63-209-142.static.apol.com.tw) (Ping timeout: 240 seconds) [14:48:17] so is the Numeral library you referenced above, what happens when I specify number in an Abstract? [14:48:22] NatExp : Int -> Exp; [14:48:51] or is that some completely different under the hood magic [15:01:05] *** Quits: wmacmil (~wmacmil@c83-250-118-111.bredband.comhem.se) (Ping timeout: 256 seconds) [16:31:58] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [17:49:16] the Numeral library is part of the RGL, and it creates trees like this [17:49:16] > gr -cat=Numeral | l -treebank [17:49:16] Numeral: num (pot2as3 (pot2plus pot01 (pot1 n8))) [17:49:17] NumeralEng: one hundred and eighty [17:50:05] Int is a GF builtin literal category, not related to the RGL numerals [17:51:18] in the RGL numerals, there are also categories "Dig" and "Digits" [17:51:19] > gr -cat=Dig | l -treebank [17:51:19] Numeral: D_9 [17:51:19] NumeralEng: 9 [17:51:27] > gr -cat=Digits | l -treebank -bind [17:51:27] Numeral: IIDig D_1 (IIDig D_5 (IIDig D_1 (IDig D_7))) [17:51:28] NumeralEng: 1,517 [17:58:54] Int is a special thing, it's secretly a cat in all grammars, even when you don't write it in the cats [17:59:14] I just tested, apparently you can do it, but it's just ignored, and if you try to give it another lincat than the builtin Int, the compiler complains [20:09:34] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 246 seconds)