search

GrammaticalFramework / gf-core

Grammatical Framework core: compiler, shell & runtimes
https://www.grammaticalframework.org
Other
129 stars 35 forks source link

Parsing variable identifiers into higher-order AST #76

Closed inariksit closed 3 years ago

inariksit commented 3 years ago

Reporting this issue from 2016, which hasn't been solved. I get the same error on GF 3.10.4.

The following example based on section 6.9 of the GF book is giving me some trouble.

abstract Binding = { cat Identifier; Prop; fun All : (Identifier -> Prop) -> Prop; Eq : Identifier -> Identifier -> Prop; AnIdentifier : Identifier; } concrete BindingStr of Binding = { lincat Prop, Identifier = {s:Str}; lin All b = { s = "(" ++ "All" ++ b.$0 ++ ")" ++ b.s} ; lin Eq a b = {s = "("++a.s ++ "=" ++ b.s ++ ")" } ; lin AnIdentifier = {s = "defaultId"}; }

Linearizing works:

linearize (All (\v1 -> Eq v1 v1))

( All v1 ) ( v1 = v1 )

However, parsing fails:

linearize (All (\v1 -> Eq v1 v1)) | parse -cat=Prop The parsing is successful but the type checking failed with error(s): Function 'lindef Identifier' is not in scope

Also tried adding "lindef Identifier = \s -> {s = s};", but this still gives the same error.

Also, the first example given in gf-contrib/typetheory/README fails in a similary way.

I am running GF version 3.8. Built on linux/x86_64 with ghc-7.8, flags: interrupt server c-runtime.

Regards, Bjørnar Luteberget.

inariksit commented 3 years ago

(If this is deemed as wontfix, I can volunteer to update the documentation on our website to reflect this.)

krangelov commented 3 years ago

This is definitely a bug which came with the introduction of linref in the language. Since practically no one uses HOAS it was left unnoticed for a long time.

On Tue, 29 Sep 2020 at 13:12, Inari Listenmaa notifications@github.com wrote:

(If this is deemed as wontfix, I can volunteer to update the documentation on our website to reflect this.)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/GrammaticalFramework/gf-core/issues/76#issuecomment-700634234, or unsubscribe https://github.com/notifications/unsubscribe-auth/AEYFSZDOGUFNE2V4CI7G3XDSIG6K3ANCNFSM4R5U64TA .

krangelov commented 3 years ago

It is fixed now. The problem is actually even older. From the time when add syntax for variables with arbitrary non-Latin names.

On Fri, 2 Oct 2020 at 19:18, Krasimir Angelov kr.angelov@gmail.com wrote:

This is definitely a bug which came with the introduction of linref in the language. Since practically no one uses HOAS it was left unnoticed for a long time.

On Tue, 29 Sep 2020 at 13:12, Inari Listenmaa notifications@github.com wrote:

(If this is deemed as wontfix, I can volunteer to update the documentation on our website to reflect this.)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/GrammaticalFramework/gf-core/issues/76#issuecomment-700634234, or unsubscribe https://github.com/notifications/unsubscribe-auth/AEYFSZDOGUFNE2V4CI7G3XDSIG6K3ANCNFSM4R5U64TA .

inariksit commented 3 years ago

Cool, thanks! I understand why a bug like this is left unnoticed :-P My main motivation in bringing it up was just to keep our webpage/tutorial up to date, so that when people are trying out the tutorial, they will actually find it working. (That's why my alternative suggestion was to change the tutorial.) But great that it is fixed now!