Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

A step towards dependent types #362

Open
wants to merge 15 commits into
base: main
Choose a base branch
from
Open

A step towards dependent types #362

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
5fd1311
initial commit
adam-antonik May 22, 2020
a02906d
put type in boot
adam-antonik May 22, 2020
9aded37
remove the not needed
adam-antonik May 22, 2020
37c9642
(maybe) Fix build
adam-antonik May 22, 2020
72bbab4
Only lower top level TLong and TString, others go into Type. Allow T…
adam-antonik May 23, 2020
ed42c49
Don't forget now to handle top tvar correctly
adam-antonik May 23, 2020
174d69c
Merge branch 'master' into dependent
kthielen May 24, 2020
32d2a05
fix field def construction ambiguity (in some compilers)
kthielen May 24, 2020
01fcf6a
construct ref counted pointers explicitly
kthielen May 24, 2020
b91b5b0
avoid storing a global variable to lift the "Type" type
kthielen May 25, 2020
1aeb143
add an sprintf test to demo and validate lower and apply functions ad…
kthielen May 25, 2020
28e53af
std::tuple != tuple. Use tuple
adam-antonik May 27, 2020
81db7c8
merge
adam-antonik May 27, 2020
e725b1a
Merge branch 'master' into dependent
kthielen Jun 30, 2020
6b7ab03
Merge branch 'master' into dependent
kthielen Jul 22, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
84 changes: 39 additions & 45 deletions lib/hobbes/lang/preds/dependent.C
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@

#include <hobbes/reflect.H>
#include <hobbes/lang/expr.H>
#include <hobbes/lang/preds/dependent.H>
#include <hobbes/eval/funcdefs.H>
Expand Down Expand Up @@ -65,17 +65,17 @@ struct MonoTypePtrToExpr : public switchType<ExprPtr> {
}

MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", name)));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", rep)));
fs.push_back(MkRecord::FieldDef(".f0", name));
fs.push_back(MkRecord::FieldDef(".f1", rep));
return ret("Prim", mkrecord(fs, la));
}

ExprPtr with(const Record* r) const {
Exprs entries;
for(auto m : r->members()) {
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", mkarray(m.field, la))));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", switchOf(m.type, *this))));
fs.push_back(MkRecord::FieldDef(".f0", ExprPtr(mkarray(m.field, la))));
fs.push_back(MkRecord::FieldDef(".f1", switchOf(m.type, *this)));
entries.push_back(mkrecord(fs, la));
}
return ret("Record", ExprPtr(new MkArray(entries, la)));
Expand All @@ -85,37 +85,37 @@ struct MonoTypePtrToExpr : public switchType<ExprPtr> {
Exprs entries;
for(auto m : v->members()) {
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", mkarray(m.selector, la))));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", switchOf(m.type, *this))));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f2", constant(static_cast<int>(m.id), la))));
fs.push_back(MkRecord::FieldDef(".f0", ExprPtr(mkarray(m.selector, la))));
fs.push_back(MkRecord::FieldDef(".f1", switchOf(m.type, *this)));
fs.push_back(MkRecord::FieldDef(".f2", constant(static_cast<int>(m.id), la)));
entries.push_back(mkrecord(fs, la));
}
return ret("Variant", ExprPtr(new MkArray(entries, la)));
}

ExprPtr with(const OpaquePtr* op) const {
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", mkarray(op->name(), la))));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", constant(static_cast<int>(op->size()), la))));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f2", constant(op->storedContiguously(), la))));
fs.push_back(MkRecord::FieldDef(".f0", ExprPtr(mkarray(op->name(), la))));
fs.push_back(MkRecord::FieldDef(".f1", constant(static_cast<int>(op->size()), la)));
fs.push_back(MkRecord::FieldDef(".f2", constant(op->storedContiguously(), la)));
return ret("OpaquePtr", mkrecord(fs, la));
}

ExprPtr with(const Exists *e) const {
ExprPtr name = ExprPtr(mkarray(e->absTypeName(), la));
ExprPtr type = switchOf(e->absType(), *this);
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", name)));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", type)));
fs.push_back(MkRecord::FieldDef(".f0", name));
fs.push_back(MkRecord::FieldDef(".f1", type));
return ret("Exists", mkrecord(fs, la));
}

ExprPtr with(const Recursive *e) const {
ExprPtr name = ExprPtr(mkarray(e->recTypeName(), la));
ExprPtr type = switchOf(e->recType(), *this);
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", name)));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", type)));
fs.push_back(MkRecord::FieldDef(".f0", name));
fs.push_back(MkRecord::FieldDef(".f1", type));
return ret("Recursive", mkrecord(fs, la));
}

Expand All @@ -128,8 +128,8 @@ struct MonoTypePtrToExpr : public switchType<ExprPtr> {
ExprPtr arge(new MkArray(args, la));
ExprPtr body = switchOf(tabs->body(), *this);
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", arge)));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", body)));
fs.push_back(MkRecord::FieldDef(".f0", arge));
fs.push_back(MkRecord::FieldDef(".f1", body));
return ret("TAbs", mkrecord(fs, la));
}

Expand All @@ -141,8 +141,8 @@ struct MonoTypePtrToExpr : public switchType<ExprPtr> {
args.push_back(switchOf(t, *this));
}
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", fn)));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", ExprPtr(new MkArray(args, la)))));
fs.push_back(MkRecord::FieldDef(".f0", fn));
fs.push_back(MkRecord::FieldDef(".f1", ExprPtr(new MkArray(args, la))));
return ret("TApp", mkrecord(fs, la));
}

Expand All @@ -153,8 +153,8 @@ struct MonoTypePtrToExpr : public switchType<ExprPtr> {
}
ExprPtr r = switchOf(v->result(), *this);
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", ExprPtr(new MkArray(ps, la)))));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", r)));
fs.push_back(MkRecord::FieldDef(".f0", ExprPtr(new MkArray(ps, la))));
fs.push_back(MkRecord::FieldDef(".f1", r));
return ret("Func", mkrecord(fs, la));
}

Expand All @@ -166,8 +166,8 @@ struct MonoTypePtrToExpr : public switchType<ExprPtr> {
ExprPtr l = switchOf(ar->length(), *this);
ExprPtr t = switchOf(ar->type(), *this);
MkRecord::FieldDefs fs;
fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", t)));
fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", l)));
fs.push_back(MkRecord::FieldDef(".f0", t));
fs.push_back(MkRecord::FieldDef(".f1", l));
return ret("FixedArray", mkrecord(fs, la));

}
Expand Down Expand Up @@ -209,34 +209,34 @@ struct _Record {
};

struct _Variant {
typedef array<std::tuple<array<char>*, Type*, int>>* type;
typedef array<tuple<array<char>*, Type*, unsigned int>>* type;
static MonoTypePtr build(_Variant::type& rec) {
Variant::Members mems;
for(unsigned int i = 0; i < rec->size; ++i) {
mems.push_back(Variant::Member(makeStdString(std::get<0>(rec->data[i])), typeExprToMonoTypePtr(std::get<1>(rec->data[i])), std::get<2>(rec->data[i])));
mems.push_back(Variant::Member(makeStdString(rec->data[i].at<0>()), typeExprToMonoTypePtr(rec->data[i].at<1>()), rec->data[i].at<2>()));
}
return Variant::make(mems);
}
};

struct _OpaquePtr {
typedef std::tuple<array<char>*, int, bool> type;
typedef tuple<array<char>*, int, bool> type;
static MonoTypePtr build(_OpaquePtr::type& op) {
return OpaquePtr::make(makeStdString(std::get<0>(op)), std::get<1>(op), std::get<2>(op));
return OpaquePtr::make(makeStdString(op.at<0>()), op.at<1>(), op.at<2>());
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For what it's worth, the reason for this difference has to do with memory layout. An std::tuple<A,B> doesn't have the same memory layout as an std::pair<A,B>, nor the same memory layout as struct { A a; B b; }. That's the only reason I made the hobbes::tuple<...> type, to get a tuple with standard memory layout -- which is necessary so that tuples in hobbes can be mapped into and out of C++ without cost.

}
};

struct _Exists {
typedef std::pair<array<char>*, Type*> type;
static MonoTypePtr build(_Exists::type& ex) {
return Exists::make(makeStdString(std::get<0>(ex)), typeExprToMonoTypePtr(std::get<1>(ex)));
return Exists::make(makeStdString(ex.first), typeExprToMonoTypePtr(ex.second));
}
};

struct _Recursive {
typedef std::pair<array<char>*, Type*> type;
static MonoTypePtr build(_Recursive::type& ex) {
return Recursive::make(makeStdString(std::get<0>(ex)), typeExprToMonoTypePtr(std::get<1>(ex)));
return Recursive::make(makeStdString(ex.first), typeExprToMonoTypePtr(ex.second));
}
};

Expand Down Expand Up @@ -349,20 +349,15 @@ MonoTypePtr typeExprToMonoTypePtr(Type* t){
}


MonoTypePtr type_; // Filthy hack since I can't seem to get type def from typedb

struct liftType {
static MonoTypePtr type(typedb&) {
return type_;
}
};

template <>
struct lift<Type*, false> : public liftType { };
struct lift<Type*, false> {
static MonoTypePtr type(typedb& tenv) {
return tenv.replaceTypeAliases(primty("Type"));
}
};

bool evalType(cc* ctx, const TEnvPtr& tenv, Definitions* ds, MonoTypePtr& tptr, ExprPtr ex, MonoTypePtr &r) {
try{

ExprPtr e = validateType(tenv, ex, ds);
if (!e) return false;
if (*e->type()->monoType() == *primty("long")) {
Expand All @@ -383,9 +378,8 @@ bool evalType(cc* ctx, const TEnvPtr& tenv, Definitions* ds, MonoTypePtr& tptr,
}


bool decodeTAConstraint(cc*ctx, const TEnvPtr tenv, Definitions* ds, const ConstraintPtr& c, MonoTypePtr& l, MonoTypePtr& r) {
bool decodeTAConstraint(cc* ctx, const TEnvPtr tenv, Definitions* ds, const ConstraintPtr& c, MonoTypePtr& l, MonoTypePtr& r) {
MonoTypePtr tptr = ctx->replaceTypeAliases(primty("Type"));
type_ = tptr;
LexicalAnnotation la;
if (c->name() == TypeApply::constraintName() && c->arguments().size() > 1) {
l = c->arguments()[0];
Expand All @@ -397,18 +391,18 @@ bool decodeTAConstraint(cc*ctx, const TEnvPtr tenv, Definitions* ds, const Const

for(unsigned int i = 2; i < c->arguments().size(); ++i) {
ExprPtr arg;
MonoTypePtr targ = c->arguments()[i];
if (is<TVar>(targ)) {
MonoTypePtr targ = c->arguments()[i];
if (is<TVar>(targ)) {
return false;
}
}
if (TApp* tapp = is<TApp>(targ)) {
if (*tapp->fn() == *primty("quote")) {
if (TExpr* e = is<TExpr>(tapp->args()[0])) {
arg = e->expr();
}
}
}
if (TString* tstr = is<TString>(targ)) {
if (TString* tstr = is<TString>(targ)) {
arg = ExprPtr(mkarray(tstr->value(), la));
}
if (TLong* tlong = is<TLong>(targ)) {
Expand Down