out.cpp

#include <iostream>
#include "util/numerics/mpz.h"
#include "library/vm/vm_io.h"
#include "library/vm/vm.h"
#include "init/init.h"

namespace lean {
lean::vm_obj put_nat(lean::vm_obj const &, lean::vm_obj const &);
}

lean::vm_obj ___lean__main();
lean::vm_obj put_seq__lambda_3(lean::vm_obj const &);
lean::vm_obj put_seq__lambda_4(lean::vm_obj const &, lean::vm_obj const &, lean::vm_obj const &);
lean::vm_obj put_seq__rec_2(lean::vm_obj const &);
lean::vm_obj put_seq(lean::vm_obj const &);
lean::vm_obj ___lean__main(){
lean::vm_obj _$local_0 = lean::mk_vm_constructor(1, {lean::mk_vm_nat(1), lean::mk_vm_simple(0)});
lean::vm_obj a = put_seq(_$local_0);
return lean::invoke(a, lean::mk_vm_simple(0));
}

lean::vm_obj mk_native_closure(lean::name const & n, unsigned nargs, lean::vm_obj * args) {
    unsigned idx = lean::get_vm_builtin_idx(n).value();
    return lean::mk_vm_closure(idx, nargs, args);
}

lean::vm_obj mk_native_closure(lean::name const & n) {
    return mk_native_closure(n, 0, nullptr);
}


lean::vm_obj put_seq__lambda_3(lean::vm_obj const & _$local_0){
return lean::mk_vm_simple(0);
}

lean::vm_obj put_seq__lambda_4(lean::vm_obj const & _$local_2, lean::vm_obj const & _$local_1, lean::vm_obj const & _$local_0){
lean::vm_obj _$local_3 = _$local_2;
lean::vm_obj _$local_4 = lean::mk_vm_simple(0);
lean::vm_obj _$local_5 = lean::put_nat(_$local_3, _$local_4);
lean::vm_obj _$local_6 = _$local_1;
lean::vm_obj _$local_7 = lean::mk_vm_simple(0);
return lean::invoke(put_seq__rec_2(_$local_6), _$local_7);
}

lean::vm_obj put_seq__rec_2(lean::vm_obj const & _$local_0){
switch (cidx(_$local_0)){
   case 0: {
     std::cout << "case0" << std::endl;
     return mk_native_closure(lean::name({"put_seq" , "_lambda_3"}), 0, nullptr);
     break;
   }
   case 1: {
     std::cout << "case1" << std::endl;
     lean::vm_obj _$local_1 = cfield(_$local_0, 0);
     lean::vm_obj _$local_2 = cfield(_$local_0, 1);
     lean::vm_obj _$local_3 = _$local_1;
     lean::vm_obj _$local_4 = _$local_2;
     lean::vm_obj args[2] = { _$local_3, _$local_4 };
     return mk_native_closure(lean::name({"put_seq" , "_lambda_4"}), 2, args);
   }
default:
throw std::runtime_error("code-gen error");
   }
}

lean::vm_obj put_seq(lean::vm_obj const & _$local_0){
  std::cout << "put_seq" << std::endl;
  lean::vm_obj _$local_1 = _$local_0;
  return put_seq__rec_2(_$local_1);
}

int main() {
  lean::initialize();
  lean::environment env;
  DECLARE_VM_BUILTIN(lean::name({"main"}), ___lean__main);
  DECLARE_VM_BUILTIN(lean::name({"put_seq" , "_lambda_3"}), put_seq__lambda_3);
  DECLARE_VM_BUILTIN(lean::name({"put_seq" , "_lambda_4"}), put_seq__lambda_4);
  DECLARE_VM_BUILTIN(lean::name({"put_seq" , "_rec_2"}), put_seq__rec_2);
  DECLARE_VM_BUILTIN(lean::name({"put_seq"}), put_seq);
  lean::vm_state S(env);
  lean::scope_vm_state scoped_state(S);
  ___lean__main();
  return 0;