From 6ada62a3eec55a08a0a0ca6cb418401b4bcd6134 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Feb 2020 13:00:22 -0800 Subject: [PATCH] feat: export helper functions Motivation: prevent changes in the scalar fields layout from breaking C++ code. Ideally, we should do that for all constructors, and implement a tool that creates the C++ functions automatically for us. We don't do it because we will delete most of this code after we finish the Lean4 transition. --- src/Init/Lean/Data/KVMap.lean | 5 +++ src/Init/Lean/Declaration.lean | 63 ++++++++++++++++++++++++++++++- src/Init/Lean/LocalContext.lean | 11 ++++++ src/Init/Lean/Message.lean | 3 ++ src/Init/Lean/MetavarContext.lean | 4 ++ src/Init/Lean/ProjFns.lean | 6 +++ src/kernel/declaration.cpp | 56 ++++++++++++++++++++++++++- src/kernel/declaration.h | 20 ++++------ src/kernel/local_ctx.cpp | 9 +++++ src/kernel/local_ctx.h | 5 +-- src/library/messages.cpp | 15 ++++++++ src/library/messages.h | 11 +----- src/library/metavar_context.cpp | 2 + src/library/projection.cpp | 5 +++ src/library/projection.h | 2 +- src/util/kvmap.cpp | 13 +++++++ src/util/kvmap.h | 4 +- 17 files changed, 203 insertions(+), 31 deletions(-) diff --git a/src/Init/Lean/Data/KVMap.lean b/src/Init/Lean/Data/KVMap.lean index 8b0623cac4..283d0be6e4 100644 --- a/src/Init/Lean/Data/KVMap.lean +++ b/src/Init/Lean/Data/KVMap.lean @@ -17,6 +17,11 @@ inductive DataValue | ofNat (v : Nat) | ofInt (v : Int) +@[export lean_mk_bool_data_value] def mkBoolDataValueEx (b : Bool) : DataValue := DataValue.ofBool b +@[export lean_data_value_bool] def DataValue.getBoolEx : DataValue → Bool +| DataValue.ofBool b => b +| _ => false + def DataValue.beq : DataValue → DataValue → Bool | DataValue.ofString s₁, DataValue.ofString s₂ => s₁ = s₂ | DataValue.ofNat n₁, DataValue.ofNat n₂ => n₂ = n₂ diff --git a/src/Init/Lean/Declaration.lean b/src/Init/Lean/Declaration.lean index edaf91d4a3..58b5938f6c 100644 --- a/src/Init/Lean/Declaration.lean +++ b/src/Init/Lean/Declaration.lean @@ -36,6 +36,14 @@ inductive ReducibilityHints | «abbrev» : ReducibilityHints | regular : UInt32 → ReducibilityHints +@[export lean_mk_reducibility_hints_regular] +def mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints := ReducibilityHints.regular h +@[export lean_reducibility_hints_get_height] +def ReducibilityHints.getHeightEx (h : ReducibilityHints) : UInt32 := +match h with +| ReducibilityHints.regular h => h +| _ => 0 + namespace ReducibilityHints instance : Inhabited ReducibilityHints := ⟨opaque⟩ @@ -58,9 +66,19 @@ instance ConstantVal.inhabited : Inhabited ConstantVal := ⟨{ name := arbitrary structure AxiomVal extends ConstantVal := (isUnsafe : Bool) +@[export lean_mk_axiom_val] +def mkAxiomValEx (name : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : AxiomVal := +{ name := name, lparams := lparams, type := type, isUnsafe := isUnsafe } +@[export lean_axiom_val_is_unsafe] def AxiomVal.isUnsafeEx (v : AxiomVal) : Bool := v.isUnsafe + structure DefinitionVal extends ConstantVal := (value : Expr) (hints : ReducibilityHints) (isUnsafe : Bool) +@[export lean_mk_definition_val] +def mkDefinitionValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (isUnsafe : Bool) : DefinitionVal := +{ name := name, lparams := lparams, type := type, value := val, hints := hints, isUnsafe := isUnsafe } +@[export lean_definition_val_is_unsafe] def DefinitionVal.isUnsafeEx (v : DefinitionVal) : Bool := v.isUnsafe + structure TheoremVal extends ConstantVal := (value : Task Expr) @@ -68,10 +86,15 @@ structure TheoremVal extends ConstantVal := structure OpaqueVal extends ConstantVal := (value : Expr) (isUnsafe : Bool) +@[export lean_mk_opaque_val] +def mkOpaqueValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (isUnsafe : Bool) : OpaqueVal := +{ name := name, lparams := lparams, type := type, value := val, isUnsafe := isUnsafe } +@[export lean_opaque_val_is_unsafe] def OpaqueVal.isUnsafeEx (v : OpaqueVal) : Bool := v.isUnsafe + structure Constructor := (name : Name) (type : Expr) -structure inductiveType := +structure InductiveType := (name : Name) (type : Expr) (ctors : List Constructor) /-- Declaration object that can be sent to the kernel. -/ @@ -82,7 +105,16 @@ inductive Declaration | opaqueDecl (val : OpaqueVal) | quotDecl | mutualDefnDecl (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` -| inductDecl (lparams : List Name) (nparams : Nat) (types : List inductiveType) (isUnsafe : Bool) +| inductDecl (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) + +@[export lean_mk_inductive_decl] +def mkInductiveDeclEs (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) : Declaration := +Declaration.inductDecl lparams nparams types isUnsafe +@[export lean_is_unsafe_inductive_decl] +def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool +| Declaration.inductDecl _ _ _ isUnsafe => isUnsafe +| _ => false + /-- The kernel compiles (mutual) inductive declarations (see `inductiveDecls`) into a set of - `Declaration.inductDecl` (for each inductive datatype in the mutual Declaration), @@ -103,6 +135,15 @@ structure InductiveVal extends ConstantVal := (isUnsafe : Bool) (isReflexive : Bool) +@[export lean_mk_inductive_val] +def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams nindices : Nat) + (all ctors : List Name) (isRec isUnsafe isReflexive : Bool) : InductiveVal := +{ name := name, lparams := lparams, type := type, nparams := nparams, nindices := nindices, all := all, ctors := ctors, + isRec := isRec, isUnsafe := isUnsafe, isReflexive := isReflexive } +@[export lean_inductive_val_is_rec] def InductiveVal.isRecEx (v : InductiveVal) : Bool := v.isRec +@[export lean_inductive_val_is_unsafe] def InductiveVal.isUnsafeEx (v : InductiveVal) : Bool := v.isUnsafe +@[export lean_inductive_val_is_reflexive] def InductiveVal.isReflexiveEx (v : InductiveVal) : Bool := v.isReflexive + namespace InductiveVal def nctors (v : InductiveVal) : Nat := v.ctors.length end InductiveVal @@ -114,6 +155,11 @@ structure ConstructorVal extends ConstantVal := (nfields : Nat) -- Number of fields (i.e., arity - nparams) (isUnsafe : Bool) +@[export lean_mk_constructor_val] +def mkConstructorValEx (name : Name) (lparams : List Name) (type : Expr) (induct : Name) (cidx nparams nfields : Nat) (isUnsafe : Bool) : ConstructorVal := +{ name := name, lparams := lparams, type := type, induct := induct, cidx := cidx, nparams := nparams, nfields := nfields, isUnsafe := isUnsafe } +@[export lean_constructor_val_is_unsafe] def ConstructorVal.isUnsafeEx (v : ConstructorVal) : Bool := v.isUnsafe + instance ConstructorVal.inhabited : Inhabited ConstructorVal := ⟨{ toConstantVal := arbitrary _, induct := arbitrary _, cidx := 0, nparams := 0, nfields := 0, isUnsafe := true }⟩ @@ -133,6 +179,14 @@ structure RecursorVal extends ConstantVal := (k : Bool) -- It supports K-like reduction (isUnsafe : Bool) +@[export lean_mk_recursor_val] +def mkRecursorValEx (name : Name) (lparams : List Name) (type : Expr) (all : List Name) (nparams nindices nmotives nminors : Nat) + (rules : List RecursorRule) (k isUnsafe : Bool) : RecursorVal := +{ name := name, lparams := lparams, type := type, all := all, nparams := nparams, nindices := nindices, + nmotives := nmotives, nminors := nminors, rules := rules, k := k, isUnsafe := isUnsafe } +@[export lean_recursor_k] def RecursorVal.kEx (v : RecursorVal) : Bool := v.k +@[export lean_recursor_is_unsafe] def RecursorVal.isUnsafeEx (v : RecursorVal) : Bool := v.isUnsafe + namespace RecursorVal def getMajorIdx (v : RecursorVal) : Nat := v.nparams + v.nmotives + v.nminors + v.nindices @@ -151,6 +205,11 @@ inductive QuotKind structure QuotVal extends ConstantVal := (kind : QuotKind) +@[export lean_mk_quot_val] +def mkQuotValEx (name : Name) (lparams : List Name) (type : Expr) (kind : QuotKind) : QuotVal := +{ name := name, lparams := lparams, type := type, kind := kind } +@[export lean_quot_val_kind] def QuotVal.kindEx (v : QuotVal) : QuotKind := v.kind + /-- Information associated with constant declarations. -/ inductive ConstantInfo | axiomInfo (val : AxiomVal) diff --git a/src/Init/Lean/LocalContext.lean b/src/Init/Lean/LocalContext.lean index 4b907ba0fc..40099452dd 100644 --- a/src/Init/Lean/LocalContext.lean +++ b/src/Init/Lean/LocalContext.lean @@ -15,6 +15,17 @@ inductive LocalDecl | cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) | ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) +@[export lean_mk_local_decl] +def mkLocalDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) : LocalDecl := +LocalDecl.cdecl index fvarId userName type bi +@[export lean_mk_let_decl] +def mkLetDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : LocalDecl := +LocalDecl.ldecl index fvarId userName type val +@[export lean_local_decl_binder_info] +def LocalDecl.binderInfoEx : LocalDecl → BinderInfo +| LocalDecl.cdecl _ _ _ _ bi => bi +| _ => BinderInfo.default + namespace LocalDecl instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _)⟩ diff --git a/src/Init/Lean/Message.lean b/src/Init/Lean/Message.lean index 5ee4707a15..f300e5b1a4 100644 --- a/src/Init/Lean/Message.lean +++ b/src/Init/Lean/Message.lean @@ -118,6 +118,9 @@ structure Message := (caption : String := "") (data : MessageData) +@[export lean_mk_message] +def mkMessageEx (fileName : String) (pos : Position) (endPos : Option Position) (severity : MessageSeverity) (caption : String) (text : String) : Message := +{ fileName := fileName, pos := pos, endPos := endPos, severity := severity, caption := caption, data := text } namespace Message protected def toString (msg : Message) : String := diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean index 58f9f5ea5a..2f379a287a 100644 --- a/src/Init/Lean/MetavarContext.lean +++ b/src/Init/Lean/MetavarContext.lean @@ -256,6 +256,10 @@ structure MetavarDecl := (localInstances : LocalInstances) (kind : MetavarKind) +@[export lean_mk_metavar_decl] +def mkMetavarDeclEx (userName : Name) (lctx : LocalContext) (type : Expr) (depth : Nat) (localInstances : LocalInstances) (kind : MetavarKind) : MetavarDecl := +{ userName := userName, lctx := lctx, type := type, depth := depth, localInstances := localInstances, kind := kind } + namespace MetavarDecl instance : Inhabited MetavarDecl := ⟨{ lctx := arbitrary _, type := arbitrary _, depth := 0, localInstances := #[], kind := MetavarKind.natural }⟩ end MetavarDecl diff --git a/src/Init/Lean/ProjFns.lean b/src/Init/Lean/ProjFns.lean index 552e660103..75222dec2e 100644 --- a/src/Init/Lean/ProjFns.lean +++ b/src/Init/Lean/ProjFns.lean @@ -16,6 +16,12 @@ structure ProjectionFunctionInfo := (i : Nat) -- The field index associated with the auxiliary projection function. (fromClass : Bool) -- `true` if the structure is a class +@[export lean_mk_projection_info] +def mkProjectionInfoEx (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo := +{ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass } +@[export lean_projection_info_from_class] +def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass + instance ProjectionFunctionInfo.inhabited : Inhabited ProjectionFunctionInfo := ⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩ diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 20d6d331b2..177009ca88 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -9,6 +9,20 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" namespace lean { + +extern "C" object * lean_mk_reducibility_hints_regular(uint32 h); +extern "C" uint32 lean_reducibility_hints_get_height(object * o); + +reducibility_hints reducibility_hints::mk_regular(unsigned h) { + object * r = alloc_cnstr(static_cast(reducibility_hints_kind::Regular), 0, sizeof(unsigned)); + cnstr_set_scalar(r, 0, h); + return reducibility_hints(r); +} + +unsigned reducibility_hints::get_height() const { + return is_regular() ? cnstr_get_scalar(raw(), 0) : 0; +} + int compare(reducibility_hints const & h1, reducibility_hints const & h2) { if (h1.kind() == h2.kind()) { if (h1.kind() == reducibility_hints_kind::Regular) { @@ -41,6 +55,9 @@ constant_val::constant_val(name const & n, names const & lparams, expr const & t object_ref(mk_cnstr(0, n, lparams, type)) { } +extern "C" object * lean_mk_axiom_val(object * n, object * lparams, object * type, uint8 is_unsafe); +extern "C" uint8 lean_axiom_val_is_unsafe(object * v); + axiom_val::axiom_val(name const & n, names const & lparams, expr const & type, bool is_unsafe): object_ref(mk_cnstr(0, constant_val(n, lparams, type), 1)) { cnstr_set_scalar(raw(), sizeof(object*), static_cast(is_unsafe)); @@ -48,6 +65,9 @@ axiom_val::axiom_val(name const & n, names const & lparams, expr const & type, b bool axiom_val::is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)) != 0; } +extern "C" object * lean_mk_definition_val(object * n, object * lparams, object * type, object * value, object * hints, uint8 is_unsafe); +extern "C" uint8 lean_definition_val_is_unsafe(object * v); + definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_unsafe): object_ref(mk_cnstr(0, constant_val(n, lparams, type), val, hints, 1)) { cnstr_set_scalar(raw(), sizeof(object*)*3, static_cast(is_unsafe)); @@ -65,6 +85,9 @@ expr theorem_val::get_value() const { return expr(v, true); } +extern "C" object * lean_mk_opaque_val(object * n, object * lparams, object * type, object * value, uint8 is_unsafe); +extern "C" uint8 lean_opaque_val_is_unsafe(object * v); + opaque_val::opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe): object_ref(mk_cnstr(0, constant_val(n, lparams, type), val, 1)) { cnstr_set_scalar(raw(), sizeof(object*)*2, static_cast(is_unsafe)); @@ -72,6 +95,9 @@ opaque_val::opaque_val(name const & n, names const & lparams, expr const & type, bool opaque_val::is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*2) != 0; } +extern "C" object * lean_mk_quot_val(object * n, object * lparams, object * type, object * value, uint8 k); +extern "C" uint8 lean_quot_val_kind(object * v); + quot_val::quot_val(name const & n, names const & lparams, expr const & type, quot_kind k): object_ref(mk_cnstr(0, constant_val(n, lparams, type), 1)) { cnstr_set_scalar(raw(), sizeof(object*), static_cast(k)); @@ -83,6 +109,12 @@ recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const & object_ref(mk_cnstr(0, cnstr, nat(nfields), rhs)) { } +extern "C" object * lean_mk_inductive_val(object * n, object * lparams, object * type, object * nparams, object * nindices, + object * all, object * cnstrs, uint8 rec, uint8 unsafe, uint8 is_refl); +extern "C" uint8 lean_inductive_val_is_rec(object * v); +extern "C" uint8 lean_inductive_val_is_unsafe(object * v); +extern "C" uint8 lean_inductive_val_is_reflexive(object * v); + inductive_val::inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams, unsigned nindices, names const & all, names const & cnstrs, bool rec, bool unsafe, bool is_refl): object_ref(mk_cnstr(0, constant_val(n, lparams, type), nat(nparams), nat(nindices), all, cnstrs, 3)) { @@ -94,11 +126,28 @@ inductive_val::inductive_val(name const & n, names const & lparams, expr const & lean_assert(is_reflexive() == is_refl); } -constructor_val::constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_unsafe): +bool inductive_val::is_rec() const { return cnstr_get_scalar(raw(), sizeof(object*)*5) != 0; } +bool inductive_val::is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*5 + 1) != 0; } +bool inductive_val::is_reflexive() const { return cnstr_get_scalar(raw(), sizeof(object*)*5 + 2) != 0; } + +extern "C" object * lean_mk_constructor_val(object * n, object * lparams, object * type, object * induct, + object * cidx, object * nparams, object * nfields, uint8 unsafe); +extern "C" uint8 lean_constructor_val_is_unsafe(object * v); + +constructor_val::constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned + nfields, bool is_unsafe): object_ref(mk_cnstr(0, constant_val(n, lparams, type), induct, nat(cidx), nat(nparams), nat(nfields), 1)) { cnstr_set_scalar(raw(), sizeof(object*)*5, static_cast(is_unsafe)); } +bool constructor_val::is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*5) != 0; } + +extern "C" object * lean_mk_recursor_val(object * n, object * lparams, object * type, object * all, + object * nparams, object * nindices, object * nmotives, object * nminors, + object * rules, uint8 k, uint8 unsafe); +extern "C" uint8 lean_recursor_val_k(object * v); +extern "C" uint8 lean_recursor_val_is_unsafe(object * v); + recursor_val::recursor_val(name const & n, names const & lparams, expr const & type, names const & all, unsigned nparams, unsigned nindices, unsigned nmotives, unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe): @@ -108,6 +157,8 @@ recursor_val::recursor_val(name const & n, names const & lparams, expr const & t cnstr_set_scalar(raw(), sizeof(object*)*7 + 1, static_cast(is_unsafe)); } +bool recursor_val::is_k() const { return cnstr_get_scalar(raw(), sizeof(object*)*7) != 0; } +bool recursor_val::is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*7 + 1) != 0; } bool declaration::is_unsafe() const { switch (kind()) { @@ -217,6 +268,9 @@ inductive_type::inductive_type(name const & id, expr const & type, constructors static unsigned inductive_decl_scalar_offset() { return sizeof(object*)*3; } +extern "C" object * lean_mk_inductive_decl(object * lparams, object * nparams, object * types, uint8 unsafe); +extern "C" uint8 lean_is_unsafe_inductive_decl(object * d); + declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe) { declaration r(mk_cnstr(static_cast(declaration_kind::Inductive), lparams, nparams, types, 1)); cnstr_set_scalar(r.raw(), inductive_decl_scalar_offset(), static_cast(is_unsafe)); diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 5fed11b8bd..88975cdbb5 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -39,14 +39,10 @@ class reducibility_hints : public object_ref { public: static reducibility_hints mk_opaque() { return reducibility_hints(box(static_cast(reducibility_hints_kind::Opaque))); } static reducibility_hints mk_abbreviation() { return reducibility_hints(box(static_cast(reducibility_hints_kind::Abbreviation))); } - static reducibility_hints mk_regular(unsigned h) { - object * r = alloc_cnstr(static_cast(reducibility_hints_kind::Regular), 0, sizeof(unsigned)); - cnstr_set_scalar(r, 0, h); - return reducibility_hints(r); - } + static reducibility_hints mk_regular(unsigned h); reducibility_hints_kind kind() const { return static_cast(obj_tag(raw())); } bool is_regular() const { return kind() == reducibility_hints_kind::Regular; } - unsigned get_height() const { return is_regular() ? cnstr_get_scalar(raw(), 0) : 0; } + unsigned get_height() const; void serialize(serializer & s) const { s.write_object(raw()); } static reducibility_hints deserialize(deserializer & d) { return reducibility_hints(d.read_object(), true); } }; @@ -302,9 +298,9 @@ public: names const & get_all() const { return static_cast(cnstr_get_ref(*this, 3)); } names const & get_cnstrs() const { return static_cast(cnstr_get_ref(*this, 4)); } unsigned get_ncnstrs() const { return length(get_cnstrs()); } - bool is_rec() const { return cnstr_get_scalar(raw(), sizeof(object*)*5) != 0; } - bool is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*5 + 1) != 0; } - bool is_reflexive() const { return cnstr_get_scalar(raw(), sizeof(object*)*5 + 2) != 0; } + bool is_rec() const; + bool is_unsafe() const; + bool is_reflexive() const; }; /* @@ -327,7 +323,7 @@ public: unsigned get_cidx() const { return static_cast(cnstr_get_ref(*this, 2)).get_small_value(); } unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 3)).get_small_value(); } unsigned get_nfields() const { return static_cast(cnstr_get_ref(*this, 4)).get_small_value(); } - bool is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*5) != 0; } + bool is_unsafe() const; }; /* @@ -380,8 +376,8 @@ public: unsigned get_nminors() const { return static_cast(cnstr_get_ref(*this, 5)).get_small_value(); } unsigned get_major_idx() const { return get_nparams() + get_nmotives() + get_nminors() + get_nindices(); } recursor_rules const & get_rules() const { return static_cast(cnstr_get_ref(*this, 6)); } - bool is_k() const { return cnstr_get_scalar(raw(), sizeof(object*)*7) != 0; } - bool is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*7 + 1) != 0; } + bool is_k() const; + bool is_unsafe() const; }; enum class quot_kind { Type, Mk, Lift, Ind }; diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp index 3e076b9c47..9d0bce5f80 100644 --- a/src/kernel/local_ctx.cpp +++ b/src/kernel/local_ctx.cpp @@ -13,6 +13,10 @@ namespace lean { static expr * g_dummy_type; static local_decl * g_dummy_decl; +extern "C" object * lean_mk_local_decl(object * index, object * fvarid, object * user_name, object * type, uint8 bi); +extern "C" object * lean_mk_let_decl(object * index, object * fvarid, object * user_name, object * type, object * val); +extern "C" uint8 lean_local_decl_binder_info(object * d); + local_decl::local_decl():object_ref(*g_dummy_decl) {} local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, expr const & v): @@ -30,6 +34,11 @@ local_decl::local_decl(local_decl const & d, expr const & t, expr const & v): local_decl::local_decl(local_decl const & d, expr const & t): local_decl(d.get_idx(), d.get_name(), d.get_user_name(), t, d.get_info()) {} +binder_info local_decl::get_info() const { + if (cnstr_tag(raw()) == 0) return static_cast(cnstr_get_scalar(raw(), sizeof(object*)*4)); + else return binder_info(); +} + expr local_decl::mk_ref() const { return mk_fvar(get_name()); } diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h index 9f8d0117c3..fdd3d6aba8 100644 --- a/src/kernel/local_ctx.h +++ b/src/kernel/local_ctx.h @@ -41,10 +41,7 @@ public: if (cnstr_tag(raw()) == 0) return none_expr(); return some_expr(static_cast(cnstr_get_ref(raw(), 4))); } - binder_info get_info() const { - if (cnstr_tag(raw()) == 0) return static_cast(cnstr_get_scalar(raw(), sizeof(object*)*4)); - else return binder_info(); - } + binder_info get_info() const; expr mk_ref() const; }; diff --git a/src/library/messages.cpp b/src/library/messages.cpp index c45d6645dd..819164a4fa 100644 --- a/src/library/messages.cpp +++ b/src/library/messages.cpp @@ -9,10 +9,25 @@ Author: Gabriel Ebner #include "library/trace.h" namespace lean { +extern "C" object * lean_mk_message(object * filename, object * pos, object * end_pos, uint8 severity, + object * caption, object * text); +extern "C" uint8 lean_message_severity(object * msg); + +message::message(std::string const & filename, pos_info const & pos, optional const & end_pos, + message_severity severity, std::string const & caption, std::string const & text) : + object_ref(mk_cnstr(0, string_ref(filename), position(pos), + option_ref(end_pos ? some(position(*end_pos)) : optional()), + string_ref(caption), string_ref(text), sizeof(message_severity))) { + cnstr_set_scalar(raw(), sizeof(void*) * 5, severity); +} message::message(parser_exception const & ex) : message(ex.get_file_name(), *ex.get_pos(), ERROR, ex.get_msg()) {} +message_severity message::get_severity() const { + return cnstr_get_scalar(raw(), sizeof(void*) * 5); +} + std::ostream & operator<<(std::ostream & out, message const & msg) { if (msg.get_severity() != INFORMATION) { out << msg.get_filename() << ":" << msg.get_pos().first << ":" << msg.get_pos().second << ": "; diff --git a/src/library/messages.h b/src/library/messages.h index 1d26b492fd..c3717bf9ef 100644 --- a/src/library/messages.h +++ b/src/library/messages.h @@ -43,12 +43,7 @@ structure message := class message : public object_ref { public: message(std::string const & filename, pos_info const & pos, optional const & end_pos, - message_severity severity, std::string const & caption, std::string const & text) : - object_ref(mk_cnstr(0, string_ref(filename), position(pos), - option_ref(end_pos ? some(position(*end_pos)) : optional()), - string_ref(caption), string_ref(text), sizeof(message_severity))) { - cnstr_set_scalar(raw(), sizeof(void*) * 5, severity); - } + message_severity severity, std::string const & caption, std::string const & text); message(std::string const & filename, pos_info const & pos, message_severity severity, std::string const & caption, std::string const & text) : message(filename, pos, optional(), severity, caption, text) {} @@ -66,9 +61,7 @@ public: auto pos = static_cast const &>(cnstr_get_ref(*this, 2)).get(); return pos ? some(pos->to_pos_info()) : optional(); } - message_severity get_severity() const { - return cnstr_get_scalar(raw(), sizeof(void*) * 5); - } + message_severity get_severity() const; std::string get_caption() const { return static_cast(cnstr_get_ref(*this, 3)).to_std_string(); } std::string get_text() const { return static_cast(cnstr_get_ref(*this, 4)).to_std_string(); } diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp index a2a91554c5..ba8ac3e82d 100644 --- a/src/library/metavar_context.cpp +++ b/src/library/metavar_context.cpp @@ -16,6 +16,8 @@ namespace lean { static name * g_meta_prefix; static expr * g_dummy_type; +extern "C" object * lean_mk_metavar_decl(object * user_name, object * lctx, object * type, object * depth, object * local_insts, uint8 k); + metavar_decl::metavar_decl(name const & user_name, local_context const & lctx, expr const & type): object_ref(mk_cnstr(0, user_name, lctx, type, 1)) { cnstr_set_scalar(raw(), 3*sizeof(object*), false); diff --git a/src/library/projection.cpp b/src/library/projection.cpp index 195650dc27..de448d70da 100644 --- a/src/library/projection.cpp +++ b/src/library/projection.cpp @@ -13,11 +13,16 @@ Author: Leonardo de Moura #include "library/projection.h" namespace lean { +extern "C" object * lean_mk_projection_info(object * ctor_name, object * nparams, object * i, uint8 from_class); +extern "C" uint8 lean_projection_info_from_class(object * info); + projection_info::projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit): object_ref(mk_cnstr(0, c, nat(nparams), nat(i))) { cnstr_set_scalar(raw(), 3*sizeof(object*), static_cast(inst_implicit)); } +bool projection_info::is_inst_implicit() const { return cnstr_get_scalar(raw(), sizeof(object*)*3) != 0; } + extern "C" object* lean_add_projection_info(object* env, object* p, object* ctor, object* nparams, object* i, uint8 fromClass); extern "C" object* lean_get_projection_info(object* env, object* p); diff --git a/src/library/projection.h b/src/library/projection.h index 72c176acaf..7d8d53ef8a 100644 --- a/src/library/projection.h +++ b/src/library/projection.h @@ -34,7 +34,7 @@ public: name const & get_constructor() const { return static_cast(cnstr_get_ref(*this, 0)); } unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 1)).get_small_value(); } unsigned get_i() const { return static_cast(cnstr_get_ref(*this, 2)).get_small_value(); } - bool is_inst_implicit() const { return cnstr_get_scalar(raw(), sizeof(object*)*3) != 0; } + bool is_inst_implicit() const; }; /** \brief Mark \c p as a projection in the given environment and store that diff --git a/src/util/kvmap.cpp b/src/util/kvmap.cpp index 59bc68c36e..282fc849ae 100644 --- a/src/util/kvmap.cpp +++ b/src/util/kvmap.cpp @@ -7,6 +7,19 @@ Author: Leonardo de Moura #include "util/kvmap.h" namespace lean { +extern "C" object * lean_mk_bool_data_value(bool b); +extern "C" uint8 lean_data_value_bool(object * v); + +data_value::data_value(bool v): + object_ref(alloc_cnstr(static_cast(data_value_kind::Bool), 0, 1)) { + cnstr_set_scalar(raw(), 0, v); +} + +bool data_value::get_bool() const { + lean_assert(kind() == data_value_kind::Bool); + return static_cast(cnstr_get_scalar(raw(), 0)); +} + bool operator==(data_value const & a, data_value const & b) { if (a.kind() != b.kind()) return false; switch (a.kind()) { diff --git a/src/util/kvmap.h b/src/util/kvmap.h index da9d46bb6b..2c3ef66af0 100644 --- a/src/util/kvmap.h +++ b/src/util/kvmap.h @@ -25,7 +25,7 @@ public: explicit data_value(char const * v):object_ref(mk_cnstr(static_cast(data_value_kind::String), mk_string(v))) {} explicit data_value(string_ref const & v):object_ref(mk_cnstr(static_cast(data_value_kind::String), v.raw())) { inc(v.raw()); } explicit data_value(nat const & v):object_ref(mk_cnstr(static_cast(data_value_kind::Nat), v.raw())) { inc(v.raw()); } - explicit data_value(bool v):object_ref(alloc_cnstr(static_cast(data_value_kind::Bool), 0, 1)) { cnstr_set_scalar(raw(), 0, v); } + explicit data_value(bool v); explicit data_value(name const & v):object_ref(mk_cnstr(static_cast(data_value_kind::Name), v.raw())) { inc(v.raw()); } data_value():data_value(false) {} data_value(data_value const & other):object_ref(other) {} @@ -40,7 +40,7 @@ public: string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast(cnstr_get_ref(*this, 0)); } nat const & get_nat() const { lean_assert(kind() == data_value_kind::Nat); return static_cast(cnstr_get_ref(*this, 0)); } name const & get_name() const { lean_assert(kind() == data_value_kind::Name); return static_cast(cnstr_get_ref(*this, 0)); } - bool get_bool() const { lean_assert(kind() == data_value_kind::Bool); return static_cast(cnstr_get_scalar(raw(), 0)); } + bool get_bool() const; friend bool operator==(data_value const & a, data_value const & b); friend bool operator<(data_value const & a, data_value const & b);