Lean: Implement type abbreviations and introduce kid->id renaming

[javra]

#829 takes priority

This translates

default Order dec
$include <prelude.sail>

type xlen       : Int = 64
type xlen_bytes : Int = 8
type xlenbits         = bits(xlen)

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

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

to

import Out.Sail.Sail

def xlen : Int := 64

def xlen_bytes : Int := 8

def xlenbits := BitVec 64

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

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

def initialize_registers : Unit :=
  ()

(Yes, the type abbreviation and the context things are largely orthogonal)

[tobiasgrosser]

Very nice. Can you add a comment why the constraint 'm >= 'n' does not reappear in lean?

[javra]

@tobiasgrosser My idea would be to ignore the constraints like the Coq exporter does, but use them to derive useful lemmas that would accompany the generated (potentially partial) functions. I think that fits the usage paradigm of Lean pretty well, for example signExtend or zeroExtend in the Lean BitVec library are total functions, only when needing to use their properties will we have to restrict the arguments

[tobiasgrosser]

That's fine with me. However, it might be useful to add this as a comment into the source code (or test cases).

[github-actions]

Test Results

   12 files  ±0     24 suites  ±0   0s ⏱️ ±0s
  739 tests +1    739 ✅ +1  0 💤 ±0  0 ❌ ±0 
2 467 runs  +1  2 466 ✅ +1  1 💤 ±0  0 ❌ ±0 

Results for commit a218708. ± Comparison against base commit fd18b93.

♻️ This comment has been updated with latest results.

[javra]

@tobiasgrosser Good idea to have that while we're working on the translation. Added a definition docstring containing the information for now. Once we're actually using all that information, I'd opt for removing that docstring though, it will really clutter the output otherwise...