From ed4cd39d593a680885471080efc0722334022baf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Mar 2019 16:46:10 -0800
Subject: [PATCH] feat(library/init/lean/compiler/ir): new IR for Lean

It is currently implemented in C++. The plan is to move the procedures
for inserting inc/dec, reset/reuse, and inferring borrow inferences to
Lean. Another goal is to make sure new IR optimizations can be
implemented in Lean, and to avoid backend optimizations that would
have to be duplicated in each backend (e.g., `emit_proj_inc_reset_seq`
at `emit_cpp.cpp`).

cc @kha
---
 library/init/lean/compiler/ir.lean | 73 ++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 library/init/lean/compiler/ir.lean

diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean
new file mode 100644
index 0000000000..578f1f6567
--- /dev/null
+++ b/library/init/lean/compiler/ir.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import init.lean.name
+prelude
+
+namespace lean
+namespace ir
+
+abbreviation varid := name
+abbreviation fid := name
+
+inductive type
+| float | uint8 | uint16 | uint32 | uint64 | usize
+| neutral | object | xobject
+
+inductive arg
+| var (id : varid)
+| neutral
+
+inductive litval
+| num (v : nat)
+| str (v : string)
+
+structure ctor_info :=
+(id : name) (cidx : nat) (usize : nat) (ssize : nat)
+
+inductive expr
+| reset (x : varid)
+| reuse (x : varid) (i : ctor_info) (ys : list arg)
+| ctor (i : ctor_info) (ys : list arg)
+| proj (i : nat) (x : varid)
+| uproj (i : nat) (x : varid)
+| sproj (n : nat) (x : varid)
+| fap (c : fid) (ys : list arg)
+| pap (c : fid) (ys : list arg)
+| ap  (x : varid) (ys : list arg)
+| box (ty : type) (x : varid)
+| unbox (x : varid)
+| lit (v : litval)
+| is_shared (x : varid)
+| is_boxed_val (x : varid)
+
+structure param :=
+(x : name) (borrowed : bool) (ty : type)
+
+inductive alt (fnbody : Type) : Type
+| ctor (info : ctor_info) (b : fnbody) : alt
+| default (b : fnbody) : alt
+
+inductive fnbody
+| vdecl (x : varid) (ty : type) (e : expr) (b : fnbody)
+| jdecl (jp : name) (xs : list param) (e : expr) (b : fnbody)
+| set (x : varid) (i : nat) (y : varid) (b : fnbody)
+| uset (x : varid) (i : nat) (y : varid) (b : fnbody)
+| sset (x : varid) (i : nat) (offset : nat) (ty : type) (y : varid) (b : fnbody)
+| release (x : varid) (i : nat) (b : fnbody)
+| inc (x : varid) (n : nat) (b : fnbody)
+| dec (x : varid) (n : nat) (b : fnbody)
+| incref (x : varid) (n : nat) (b : fnbody)
+| decref (x : varid) (n : nat) (b : fnbody)
+| case (tid : name) (cs : list (alt fnbody))
+| ret (x : varid)
+| jmp (lbl : name) (ys : list arg)
+
+inductive decl
+| fdecl  (f : fid) (xs : list param) (ty : type) (b : fnbody)
+| extern (f : fid) (xs : list param) (ty : type)
+
+end ir
+end lean