Parsing variable identifiers into higher-order AST

[inariksit]

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]

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

[krangelov]

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 ***@***.***> 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 <#76 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AEYFSZDOGUFNE2V4CI7G3XDSIG6K3ANCNFSM4R5U64TA> .

[krangelov]

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 ***@***.***> 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 ***@***.***> 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 > <#76 (comment)>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AEYFSZDOGUFNE2V4CI7G3XDSIG6K3ANCNFSM4R5U64TA> > . >

[inariksit]

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!