lean4/tests/ir/tst4.ir

[lean_dbg_print_num] external print_num (s : object)
[lean_dbg_print_str] external print_str (s : object)

def iota (n : uint32) : object :=
entry:
  case n [zero_case, succ_case];
zero_case:
  r  : uint32 := 0;
  r1 : object := box r;
  ret r1;
succ_case:
  one : uint32 := 1;
  n1  : uint32 := sub n one;
  tail := call iota n1;
  head : object := box n1;
  r2 := cnstr 1 2 0;
  set r2 0 head;
  set r2 1 tail;
  ret r2;

def len (o : object) : uint32 :=
entry:
  t : uint32 := tag o;
  case t [null_case, cons_case];
null_case:
  r : uint32 := 0;
  ret r;
cons_case:
  tail := get o 1;
  sz1 := call len tail;
  one : uint32 := 1;
  sz2 : uint32 := add sz1 one;
  ret sz2;

def sum (o : object) : uint32 :=
entry:
  t : uint32 := tag o;
  case t [null_case, cons_case];
null_case:
  r : uint32 := 0;
  ret r;
cons_case:
  head := get o 0;
  n : uint32 := unbox head;
  tail := get o 1;
  sum1 := call sum tail;
  sum2 : uint32 := add sum1 n;
  ret sum2;

def map (f : object) (o : object) : object :=
entry:
  t : uint32 := tag o;
  case t [null_case, cons_case];
null_case:
  ret o;
cons_case:
  head := get o 0;
  tail := get o 1;
  head1 := apply f head;
  tail1 := call map f tail;
  r := cnstr 1 2 0;
  set r 0 head1;
  set r 1 tail1;
  ret r;

def add1 (o : object) : object :=
entry:
  u : uint32   := unbox o;
  one : uint32 := 1;
  r : uint32   := add u one;
  r1 : object  := box r;
  ret r1;

def d_map (f : object) (o : object) : object :=
entry:
  t : uint32 := tag o;
  case t [null_case, cons_case];
null_case:
  ret o;
cons_case:
  s : bool   := is_shared o;
  case s [not_shared_case1, shared_case1];
not_shared_case1:
  head := get o 0;
  tail := get o 1;
  cell : object := o;
  jmp cont1;
shared_case1:
  head := get o 0;
  tail := get o 1;
  inc head;
  inc tail;
  dec_sref o;
  cell := cnstr 1 2 0;
  jmp cont1;
cont1:
  nhead := apply f head;
  ntail := call d_map f tail;
  set cell 0 nhead;
  set cell 1 ntail;
  ret cell;

def d_spec_map (o : object) : object :=
entry:
  t : uint32 := tag o;
  case t [null_case, cons_case];
null_case:
  ret o;
cons_case:
  s : bool   := is_shared o;
  head := get o 0;
  tail := get o 1;
  case s [not_shared_case1, shared_case1];
not_shared_case1:
  cell : object := o;
  jmp cont1;
shared_case1:
  inc head;
  inc tail;
  dec_sref o;
  cell := cnstr 1 2 0;
  jmp cont1;
cont1:
  v1 : uint32 := unbox head;
  one : uint32 := 1;
  v2 : uint32 := add v1 one;
  nhead : object := box v2;
  ntail := call d_spec_map tail;
  set cell 0 nhead;
  set cell 1 ntail;
  ret cell;

def tst : int32 :=
entry:
  n : uint32 := 50000;
  l := call iota n;
  sz := call len l;
  osz : object := box sz;
  call print_num osz;
  sum := call sum l;
  osum : object := box sum;
  call print_num osum;
  fn := closure add1;
  l2 := call map fn l;
  sum2 := call sum l2;
  osum2 : object := box sum2;
  call print_num osum2;
  dec fn;
  dec l;
  dec l2;
  r : int32 := 0;
  ret r;

def d_tst : int32 :=
entry:
  n : uint32 := 50000;
  l := call iota n;
  sz := call len l;
  osz : object := box sz;
  call print_num osz;
  sum := call sum l;
  osum : object := box sum;
  call print_num osum;
  fn := closure add1;
  l2 := call d_map fn l;
  sum2 := call sum l2;
  osum2 : object := box sum2;
  call print_num osum2;
  dec fn;
  dec l2;
  r : int32 := 0;
  ret r;

def d_spec_tst : int32 :=
entry:
  n : uint32 := 50000;
  l := call iota n;
  sz := call len l;
  osz : object := box sz;
  call print_num osz;
  sum := call sum l;
  osum : object := box sum;
  call print_num osum;
  l2 := call d_spec_map l;
  sum2 := call sum l2;
  osum2 : object := box sum2;
  call print_num osum2;
  dec l2;
  r : int32 := 0;
  ret r;

def main : int32 :=
entry:
  n : uint32 := 200;
  jmp loop;
loop:
  case n [zero_case, succ_case];
zero_case:
  r : int32 := 0;
  ret r;
succ_case:
  one : uint32 := 1;
  n : uint32 := sub n one;
  r2 := call tst;
  jmp loop;