Internal error with `Ints`

[WolframKahl]

In the reference manual I find

lessInt | Integer -> Integer -> PBool | test order of integers

and

Ints n is a subtype of Integer

I therefore would expect being able to apply lessInt to Ints values, but with

-- A.gf
abstract A = {
  cat Expr ;
  fun EOne : Expr ;
  fun EMax : Expr -> Expr -> Expr ;
}

and

-- C.gf
concrete C of A = open Prelude in {
  lincat Expr = Predef.Ints 5 ;
  lin
    EOne = 1 ;
    EMax x y = case Predef.lessInt x y of {
        Predef.PTrue => y ;
        Predef.PFalse => x
      } ;
}  

, gf-3.10 produces:

- compiling C.gf... Internal error in Compute.ConcreteNew:
    Applying Predef.lessInt: Expected a static value of type Int, got a dynamic value

My original attempt was to use lessInt for a better implementation of lessPrec in
a custom copy of prelude/Formal.gf with more than five precedence levels:

    lessPrec : Prec -> Prec -> Bool ;
    lessPrec p q = case Predef.lessInt p q of {
        Predef.PTrue => True ;
        Predef.PFalse => False
      } ;

This produces:

 Internal error in Compute.ConcreteNew:
    Applying Predef.lessInt: Expected a value of type Int, got VP (VGen 0 []) (LIdent (Id {rawId2utf8 = "p"}))

In this context, I also found it surprising that prelude/Predef.gf actually has

  oper lessInt: Int -> Int -> PBool    = variants {} ; -- test order of integers

with Int, instead of with Integer as the reference manual appears to suggest.

[inariksit]

Hi @WolframKahl ,

It seems that the reference manual just needs updating s/Integer/Int/.

The actual problem is the internal error in Compute.ConcreteNew. The comments in Predef.gf say "Applying them [the opers] to run-time variables leads to compiler errors that are often only detected at the code generation time."

So calling lessInt on an argument of a function is prohibited. (For a longer explanation on what is allowed and what is not, see this blog post. The post talks about string gluing and pattern matching, but exactly the same rules apply to all the Predef opers.)

However, Ints n for any n is still a parameter type, so it is possible to pattern match them at runtime. Here's an example.

abstract Numbers = {
  cat
    Nat ;
  fun
    Zero : Nat ;
    Succ : Nat -> Nat ;
}

And concrete:

concrete NumbersCnc of Numbers = open Predef, Prelude in {
  lincat
    Nat = {n : Ints 10} ;
  lin
    Zero = {n = 0} ;
    Succ x = {n = myPlus1 ! x.n} ;

  oper

    myPlus1 : Ints 10 => Ints 10 = table {
      0 => 1 ;
      1 => 2 ;
      2 => 3 ;
      3 => 4 ;
      4 => 5 ;
      5 => 6 ;
      6 => 7 ;
      7 => 8 ;
      8 => 9 ;
      _ => 10
      } ;
}

Let's test this in the GF shell:

$ gf
…

> i -retain NumbersCnc.gf 

> cc Zero
{n = 0; lock_Nat = <>}

> cc Succ Zero
{n = 1; lock_Nat = <>}

> cc Succ (Succ (Succ (Succ (Succ Zero))))
{n = 5; lock_Nat = <>}

Obviously, this doesn't scale up, and is very tedious to write. Just demonstrating that it is possible to pattern match Ints n at runtime.

Maybe @aarneranta or @krangelov can share more insight here, is it possible to do something more interesting on Int?

[WolframKahl]

My first point was that as user, I don't expect to see internal errors, but assume that the developers would like to be informed when I do see one, since with an internal error, the system is blaming its developers for a situation it cannot handle. 😉

My second point was that the fact that the reference manual says

Ints n is a subtype of Integer

leads me to expect that

    lessInt : Ints 16 -> Ints 16 -> Bool

is available, and since 16 is a compile-time constant, I am optimistically hoping that the corresponding table
will be generated at compile time if the system needs this as a table.

I did find the lessPrec definition in Formal.gf, and the fact that it looked quite ad-hoc made me wonder whether much performance can be gained that way --- I am currently using a systematic approach with:

    lessPrec : Prec -> Prec -> Bool ;
    -- lessPrec p q = case Predef.lessInt p q of {
    --     Predef.PTrue => True ;
    --     Predef.PFalse => False
    --   } ;
    lessPrec p q = case <<p,q> : Prec * Prec> of {
        <16, _> => False ;
        <_, 16> => True ;
        <15, _> => False ;
        <_, 15> => True ;
        <14, _> => False ;
        <_, 14> => True ;
        <13, _> => False ;
        <_, 13> => True ;
        <12, _> => False ;
        <_, 12> => True ;
        <11, _> => False ;
        <_, 11> => True ;
        <10, _> => False ;
        <_, 10> => True ;
        <9, _> => False ;
        <_, 9> => True ;
        <8, _> => False ;
        <_, 8> => True ;
        <7, _> => False ;
        <_, 7> => True ;
        <6, _> => False ;
        <_, 6> => True ;
        <5, _> => False ;
        <_, 5> => True ;
        <4, _> => False ;
        <_, 4> => True ;
        <3, _> => False ;
        <_, 3> => True ;
        <2, _> => False ;
        <_, 2> => True ;
        <1, _> => False ;
        <_, 1> => True ;
        _ => False
        } ;

But I am guessing that even spelling out all 289 cases would not make a performance difference in the compiled result?

[inariksit]

My first point was that as user, I don't expect to see internal errors, but assume that the developers would like to be informed when I do see one, since with an internal error, the system is blaming its developers for a situation it cannot handle. 😉

Fair enough. I'll amend my pending PR #93 to add a better error message for this too.

and since 16 is a compile-time constant, I am optimistically hoping that the corresponding table
will be generated at compile time if the system needs this as a table.

Yeah, I would expect that too. Clearly Ints 16 is a finite parameter type, and behaves as such when pattern matching. My guess is that lessInt itself is the problem here. Could e.g. @krangelov clarify this?

But I am guessing that even spelling out all 289 cases would not make a performance difference in the compiled result?

I don't know the answer to this either.