max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/compiler/ir): export primitives to C++

Browse source 
Remark: we don't need to expose all of them since the C++ code only
generates code in the Lambda_pure fragment.
This commit is contained in:
Leonardo de Moura 2019-04-29 17:10:42 -07:00
parent a32fcf33c7
commit 2db7cd158b
1 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
library/init/lean/compiler/ir.lean
View file

@ -74,6 +74,9 @@ inductive Arg
| var (id : VarId)
| irrelevant
@[export lean.ir.mk_var_arg_core] def mkVarArg (id : VarId) : Arg := Arg.var id
@[export lean.ir.mk_irrelevant_arg_core] def mkIrrelevantArg : Arg := Arg.irrelevant
inductive LitVal
| num (v : Nat)
| str (v : String)
@ -98,6 +101,8 @@ scalar values, and a sequence of other scalar values. -/
structure CtorInfo :=
(name : Name) (cidx : Nat) (usize : Nat) (ssize : Nat)
@[export lean.ir.mk_ctor_info_core] def mkCtorInfo (n : Name) (cidx : Nat) (usize : Nat) (ssize : Nat) : CtorInfo := ⟨n, cidx, usize, ssize⟩
def CtorInfo.beq : CtorInfo → CtorInfo → Bool
| ⟨n₁, cidx₁, usize₁, ssize₁⟩ ⟨n₂, cidx₂, usize₂, ssize₂⟩ :=
n₁ == n₂ && cidx₁ == cidx₂ && usize₁ == usize₂ && ssize₁ == ssize₂
@ -132,9 +137,21 @@ inductive Expr
/- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/
| isTaggedPtr (x : VarId)
@[export lean.ir.mk_ctor_expr_core] def mkCtorExpr (i : CtorInfo) (ys : Array Arg) : Expr := Expr.ctor i ys
@[export lean.ir.mk_proj_expr_core] def mkProjExpr (i : Nat) (x : VarId) : Expr := Expr.proj i x
@[export lean.ir.mk_uproj_expr_core] def mkUProjExpr (i : Nat) (x : VarId) : Expr := Expr.uproj i x
@[export lean.ir.mk_sproj_expr_core] def mkSProjExpr (n : Nat) (x : VarId) : Expr := Expr.sproj n x
@[export lean.ir.mk_fapp_expr_core] def mkFAppExpr (c : FunId) (ys : Array Arg) : Expr := Expr.fap c ys
@[export lean.ir.mk_papp_expr_core] def mkPAppExpr (c : FunId) (ys : Array Arg) : Expr := Expr.pap c ys
@[export lean.ir.mk_app_expr_core] def mkAppExpr (x : VarId) (ys : Array Arg) : Expr := Expr.ap x ys
@[export lean.ir.mk_num_expr_core] def mkNumExpr (v : Nat) : Expr := Expr.lit (LitVal.num v)
@[export lean.ir.mk_str_expr_core] def mkStrExpr (v : String) : Expr := Expr.lit (LitVal.str v)
structure Param :=
(x : Name) (borrowed : Bool) (ty : IRType)
@[export lean.ir.mk_param_core] def mkParam (x : Name) (borrowed : Bool) (ty : IRType) : Param := ⟨x, borrowed, ty⟩
inductive AltCore (FnBody : Type) : Type
| ctor (info : CtorInfo) (b : FnBody) : AltCore
| default (b : FnBody) : AltCore
@ -164,14 +181,27 @@ inductive FnBody
| jmp (j : JoinPointId) (ys : Array Arg)
| unreachable
@[export lean.ir.mk_vdecl_core] def mkVDecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) : FnBody := FnBody.vdecl x ty e b
@[export lean.ir.mk_jdecl_core] def mkJDecl (j : JoinPointId) (xs : Array Param) (ty : IRType) (v : FnBody) (b : FnBody) : FnBody := FnBody.jdecl j xs ty v b
@[export lean.ir.mk_uset_core] def mkUSet (x : VarId) (i : Nat) (y : VarId) (b : FnBody) : FnBody := FnBody.uset x i y b
@[export lean.ir.mk_sset_core] def mkSSet (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) : FnBody := FnBody.sset x i offset y ty b
@[export lean.ir.mk_case_core] def mkCase (tid : Name) (x : VarId) (cs : Array (AltCore FnBody)) : FnBody := FnBody.case tid x cs
@[export lean.ir.mk_ret_core] def mkRet (x : VarId) : FnBody := FnBody.ret x
@[export lean.ir.mk_jmp_core] def mkJmp (j : JoinPointId) (ys : Array Arg) : FnBody := FnBody.jmp j ys
@[export lean.ir.mk_unreachable_core] def mkUnreachable : FnBody := FnBody.unreachable
abbrev Alt := AltCore FnBody
@[pattern] abbrev Alt.ctor := @AltCore.ctor FnBody
@[pattern] abbrev Alt.default := @AltCore.default FnBody
@[export lean.ir.mk_alt_core] def mkAlt (info : CtorInfo) (b : FnBody) : Alt := Alt.ctor info b
inductive Decl
| fdecl (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody)
| extern (f : FunId) (xs : Array Param) (ty : IRType)
@[export lean.ir.mk_decl_core] def mkDecl (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody) : Decl := Decl.fdecl f xs ty b
/-- `Expr.isPure e` return `true` Iff `e` is in the `λPure` fragment. -/
def Expr.isPure : Expr → Bool
| (Expr.ctor _ _) := true