Lean: support for implicit arguments in function application

[javra]

This closes #948.

Translates

default Order dec

$include <prelude.sail>

val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
function EXTZ(m, v) = sail_zero_extend(v, m)

val foo : bits(8) -> bits(16)
function foo x = {
  EXTZ(x)
}

to

import Out.Sail.Sail

open Sail

abbrev SailM := StateM Unit

/-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
  (Sail.BitVec.zeroExtend v m)

def foo (x : (BitVec 8)) : (BitVec 16) :=
  (EXTZ x)

def initialize_registers (lit : Unit) : Unit :=
  ()

[github-actions]

Test Results

   12 files  ±0     25 suites  ±0   0s ⏱️ ±0s
  763 tests +1    763 ✅ +1  0 💤 ±0  0 ❌ ±0 
2 707 runs  +1  2 707 ✅ +1  0 💤 ±0  0 ❌ ±0 

Results for commit 72a0c10. ± Comparison against base commit e4386bb.

♻️ This comment has been updated with latest results.

[bacam]

It would be rare / non-existant, but I think this might break on mutually recursive functions with implicit arguments because one of the functions wouldn't be added until after it is used. If so, we could query the function's type to find the implicit arguments at the point of use.

[javra]

Do you think querying the type on the call site might be the better approach generally?

[bacam]

It would involve less plumbing, certainly.

[javra]

What would be the canonical way to lookup the type?

[bacam]

What would be the canonical way to lookup the type?

Env.get_val_spec