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.
This commit is contained in:
Leonardo de Moura
parent
74d08e47e5
commit
6ada62a3ee
17 changed files with 203 additions and 31 deletions
|
|
@ -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₂
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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 _)⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 }⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -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<unsigned>(reducibility_hints_kind::Regular), 0, sizeof(unsigned));
|
||||
cnstr_set_scalar<unsigned>(r, 0, h);
|
||||
return reducibility_hints(r);
|
||||
}
|
||||
|
||||
unsigned reducibility_hints::get_height() const {
|
||||
return is_regular() ? cnstr_get_scalar<unsigned>(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<unsigned char>(raw(), sizeof(object*), static_cast<unsigned char>(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<unsigned char>(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<unsigned char>(raw(), sizeof(object*)*3, static_cast<unsigned char>(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<unsigned char>(raw(), sizeof(object*)*2, static_cast<unsigned char>(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<unsigned char>(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<unsigned char>(raw(), sizeof(object*), static_cast<unsigned char>(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<unsigned char>(raw(), sizeof(object*)*5) != 0; }
|
||||
bool inductive_val::is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5 + 1) != 0; }
|
||||
bool inductive_val::is_reflexive() const { return cnstr_get_scalar<unsigned char>(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<unsigned char>(raw(), sizeof(object*)*5, static_cast<unsigned char>(is_unsafe));
|
||||
}
|
||||
|
||||
bool constructor_val::is_unsafe() const { return cnstr_get_scalar<unsigned char>(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<unsigned char>(raw(), sizeof(object*)*7 + 1, static_cast<unsigned char>(is_unsafe));
|
||||
}
|
||||
|
||||
bool recursor_val::is_k() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*7) != 0; }
|
||||
bool recursor_val::is_unsafe() const { return cnstr_get_scalar<unsigned char>(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<unsigned>(declaration_kind::Inductive), lparams, nparams, types, 1));
|
||||
cnstr_set_scalar<unsigned char>(r.raw(), inductive_decl_scalar_offset(), static_cast<unsigned char>(is_unsafe));
|
||||
|
|
|
|||
|
|
@ -39,14 +39,10 @@ class reducibility_hints : public object_ref {
|
|||
public:
|
||||
static reducibility_hints mk_opaque() { return reducibility_hints(box(static_cast<unsigned>(reducibility_hints_kind::Opaque))); }
|
||||
static reducibility_hints mk_abbreviation() { return reducibility_hints(box(static_cast<unsigned>(reducibility_hints_kind::Abbreviation))); }
|
||||
static reducibility_hints mk_regular(unsigned h) {
|
||||
object * r = alloc_cnstr(static_cast<unsigned>(reducibility_hints_kind::Regular), 0, sizeof(unsigned));
|
||||
cnstr_set_scalar<unsigned>(r, 0, h);
|
||||
return reducibility_hints(r);
|
||||
}
|
||||
static reducibility_hints mk_regular(unsigned h);
|
||||
reducibility_hints_kind kind() const { return static_cast<reducibility_hints_kind>(obj_tag(raw())); }
|
||||
bool is_regular() const { return kind() == reducibility_hints_kind::Regular; }
|
||||
unsigned get_height() const { return is_regular() ? cnstr_get_scalar<unsigned>(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<names const &>(cnstr_get_ref(*this, 3)); }
|
||||
names const & get_cnstrs() const { return static_cast<names const &>(cnstr_get_ref(*this, 4)); }
|
||||
unsigned get_ncnstrs() const { return length(get_cnstrs()); }
|
||||
bool is_rec() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5) != 0; }
|
||||
bool is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5 + 1) != 0; }
|
||||
bool is_reflexive() const { return cnstr_get_scalar<unsigned char>(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<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
|
||||
unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value(); }
|
||||
unsigned get_nfields() const { return static_cast<nat const &>(cnstr_get_ref(*this, 4)).get_small_value(); }
|
||||
bool is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5) != 0; }
|
||||
bool is_unsafe() const;
|
||||
};
|
||||
|
||||
/*
|
||||
|
|
@ -380,8 +376,8 @@ public:
|
|||
unsigned get_nminors() const { return static_cast<nat const &>(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<recursor_rules const &>(cnstr_get_ref(*this, 6)); }
|
||||
bool is_k() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*7) != 0; }
|
||||
bool is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*7 + 1) != 0; }
|
||||
bool is_k() const;
|
||||
bool is_unsafe() const;
|
||||
};
|
||||
|
||||
enum class quot_kind { Type, Mk, Lift, Ind };
|
||||
|
|
|
|||
|
|
@ -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<binder_info>(cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*4));
|
||||
else return binder_info();
|
||||
}
|
||||
|
||||
expr local_decl::mk_ref() const {
|
||||
return mk_fvar(get_name());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -41,10 +41,7 @@ public:
|
|||
if (cnstr_tag(raw()) == 0) return none_expr();
|
||||
return some_expr(static_cast<expr const &>(cnstr_get_ref(raw(), 4)));
|
||||
}
|
||||
binder_info get_info() const {
|
||||
if (cnstr_tag(raw()) == 0) return static_cast<binder_info>(cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*4));
|
||||
else return binder_info();
|
||||
}
|
||||
binder_info get_info() const;
|
||||
expr mk_ref() const;
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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<pos_info> 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<position>(end_pos ? some(position(*end_pos)) : optional<position>()),
|
||||
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<message_severity>(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 << ": ";
|
||||
|
|
|
|||
|
|
@ -43,12 +43,7 @@ structure message :=
|
|||
class message : public object_ref {
|
||||
public:
|
||||
message(std::string const & filename, pos_info const & pos, optional<pos_info> 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<position>(end_pos ? some(position(*end_pos)) : optional<position>()),
|
||||
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<pos_info>(), severity, caption, text) {}
|
||||
|
|
@ -66,9 +61,7 @@ public:
|
|||
auto pos = static_cast<option_ref<position> const &>(cnstr_get_ref(*this, 2)).get();
|
||||
return pos ? some(pos->to_pos_info()) : optional<pos_info>();
|
||||
}
|
||||
message_severity get_severity() const {
|
||||
return cnstr_get_scalar<message_severity>(raw(), sizeof(void*) * 5);
|
||||
}
|
||||
message_severity get_severity() const;
|
||||
std::string get_caption() const { return static_cast<string_ref const &>(cnstr_get_ref(*this, 3)).to_std_string(); }
|
||||
std::string get_text() const { return static_cast<string_ref const &>(cnstr_get_ref(*this, 4)).to_std_string(); }
|
||||
|
||||
|
|
|
|||
|
|
@ -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<uint8>(raw(), 3*sizeof(object*), false);
|
||||
|
|
|
|||
|
|
@ -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<unsigned char>(raw(), 3*sizeof(object*), static_cast<unsigned char>(inst_implicit));
|
||||
}
|
||||
|
||||
bool projection_info::is_inst_implicit() const { return cnstr_get_scalar<unsigned char>(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);
|
||||
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ public:
|
|||
name const & get_constructor() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
|
||||
unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
|
||||
unsigned get_i() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
|
||||
bool is_inst_implicit() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*3) != 0; }
|
||||
bool is_inst_implicit() const;
|
||||
};
|
||||
|
||||
/** \brief Mark \c p as a projection in the given environment and store that
|
||||
|
|
|
|||
|
|
@ -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<unsigned>(data_value_kind::Bool), 0, 1)) {
|
||||
cnstr_set_scalar<unsigned char>(raw(), 0, v);
|
||||
}
|
||||
|
||||
bool data_value::get_bool() const {
|
||||
lean_assert(kind() == data_value_kind::Bool);
|
||||
return static_cast<bool>(cnstr_get_scalar<unsigned char>(raw(), 0));
|
||||
}
|
||||
|
||||
bool operator==(data_value const & a, data_value const & b) {
|
||||
if (a.kind() != b.kind()) return false;
|
||||
switch (a.kind()) {
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ public:
|
|||
explicit data_value(char const * v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::String), mk_string(v))) {}
|
||||
explicit data_value(string_ref const & v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::String), v.raw())) { inc(v.raw()); }
|
||||
explicit data_value(nat const & v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::Nat), v.raw())) { inc(v.raw()); }
|
||||
explicit data_value(bool v):object_ref(alloc_cnstr(static_cast<unsigned>(data_value_kind::Bool), 0, 1)) { cnstr_set_scalar<unsigned char>(raw(), 0, v); }
|
||||
explicit data_value(bool v);
|
||||
explicit data_value(name const & v):object_ref(mk_cnstr(static_cast<unsigned>(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<string_ref const &>(cnstr_get_ref(*this, 0)); }
|
||||
nat const & get_nat() const { lean_assert(kind() == data_value_kind::Nat); return static_cast<nat const &>(cnstr_get_ref(*this, 0)); }
|
||||
name const & get_name() const { lean_assert(kind() == data_value_kind::Name); return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
|
||||
bool get_bool() const { lean_assert(kind() == data_value_kind::Bool); return static_cast<bool>(cnstr_get_scalar<unsigned char>(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);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue