From 5fd13113b8cc4428c6aba5040e6801e405f3681c Mon Sep 17 00:00:00 2001 From: adam-antonik Date: Fri, 22 May 2020 18:09:40 +0100 Subject: [PATCH 01/11] initial commit --- include/hobbes/lang/preds/dependent.H | 37 ++ lib/hobbes/eval/cc.C | 6 +- lib/hobbes/eval/func.C | 29 ++ lib/hobbes/lang/preds/dependent.C | 550 ++++++++++++++++++++++++++ 4 files changed, 621 insertions(+), 1 deletion(-) create mode 100644 include/hobbes/lang/preds/dependent.H create mode 100644 lib/hobbes/lang/preds/dependent.C diff --git a/include/hobbes/lang/preds/dependent.H b/include/hobbes/lang/preds/dependent.H new file mode 100644 index 000000000..2ff8c575e --- /dev/null +++ b/include/hobbes/lang/preds/dependent.H @@ -0,0 +1,37 @@ +#ifndef HOBBES_LANG_TYPEPREDS_DEPENDENT_HPP_INCLUDED +#define HOBBES_LANG_TYPEPREDS_DEPENDENT_HPP_INCLUDED + +#include +#include +namespace hobbes{ + class TypeApply : public Unqualifier { + private: + cc*c; + public: + TypeApply(cc*c) : c(c) {}; + static std::string constraintName(); + bool refine(const TEnvPtr&, const ConstraintPtr& cst, MonoTypeUnifier* u, Definitions*); + ExprPtr unqualify(const TEnvPtr& tenv, const ConstraintPtr& cst, const ExprPtr& e, Definitions*) const; + bool satisfied(const TEnvPtr&, const ConstraintPtr& cst, Definitions*) const; + bool satisfiable(const TEnvPtr& tenv, const ConstraintPtr& cst, Definitions*) const; + void explain(const TEnvPtr&, const ConstraintPtr& cst, const ExprPtr& e, Definitions*, annmsgs* msgs); + PolyTypePtr lookup(const std::string& vn) const; + SymSet bindings() const; + FunDeps dependencies(const ConstraintPtr&) const; + }; + + class TypeValueLower : public Unqualifier { + public: + static std::string constraintName(); + bool refine(const TEnvPtr&, const ConstraintPtr& cst, MonoTypeUnifier* u, Definitions*); + ExprPtr unqualify(const TEnvPtr& tenv, const ConstraintPtr& cst, const ExprPtr& e, Definitions*) const; + bool satisfied(const TEnvPtr&, const ConstraintPtr& cst, Definitions*) const; + bool satisfiable(const TEnvPtr& tenv, const ConstraintPtr& cst, Definitions*) const; + void explain(const TEnvPtr&, const ConstraintPtr& cst, const ExprPtr& e, Definitions*, annmsgs* msgs); + PolyTypePtr lookup(const std::string& vn) const; + SymSet bindings() const; + FunDeps dependencies(const ConstraintPtr&) const; + }; +} + +#endif diff --git a/lib/hobbes/eval/cc.C b/lib/hobbes/eval/cc.C index 43fdd96ca..f892ff1d0 100644 --- a/lib/hobbes/eval/cc.C +++ b/lib/hobbes/eval/cc.C @@ -12,7 +12,7 @@ #include #include - +#include // structured file support #include @@ -131,6 +131,10 @@ cc::cc() : // initialize structured storage support initStorageFileDefs(fv, *this); + + // initialize dependent types + this->tenv->bind(TypeValueLower::constraintName(), UnqualifierPtr(new TypeValueLower())); + this->tenv->bind(TypeApply::constraintName(), UnqualifierPtr(new TypeApply(this))); // boot compileBootCode(*this); diff --git a/lib/hobbes/eval/func.C b/lib/hobbes/eval/func.C index 5e1169551..42677ae91 100644 --- a/lib/hobbes/eval/func.C +++ b/lib/hobbes/eval/func.C @@ -503,6 +503,34 @@ public: } }; +class tvlower : public op { +public: + llvm::Value* apply(jitcc* c, const MonoTypes& ts, const MonoTypePtr&, const Exprs& es) { + if (TString* tstr = is(ts[0])) { + return c->compile(ExprPtr(mkarray(tstr->value(), LexicalAnnotation()))); + } + if (TLong* tlong = is(ts[0])) { + return c->compile(constant(tlong->value(), LexicalAnnotation())); + } + if (TApp *tapp = is(ts[0])) { + if (*tapp->fn() == *primty("quote")) { + if (TExpr* e = is(tapp->args()[0])) { + return c->compile(e->expr()); + } + } + } + + throw annotated_error(*es[0], "Invalid usage of .TypeValueLower"); + } + + PolyTypePtr type(typedb&) const { + static MonoTypePtr tg0(TGen::make(0)); + static MonoTypePtr tg1(TGen::make(1)); + static PolyTypePtr idty(new PolyType(2, qualtype(Func::make(tuplety(list(tg0)), tg1)))); + return idty; + } +}; + // allocate fresh values / primitives class newPrimfn : public op { public: @@ -1022,6 +1050,7 @@ void initDefOperators(cc* c) { BINDF("id", new idexp()); BINDF(".cast", new castexp()); BINDF("unsafeCast", new castexp()); // perhaps qualify this so that 'memory-representation equivalence' can be decided safely at compile-time? + BINDF(".typeValueLower", new tvlower()); // allocate space for some type BINDF("newPrim", new newPrimfn(false)); // <-- don't 0-fill memory diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C new file mode 100644 index 000000000..ee08a368f --- /dev/null +++ b/lib/hobbes/lang/preds/dependent.C @@ -0,0 +1,550 @@ + +#include +#include +#include + +namespace hobbes{ + +static bool tvalueToMonoTypePtr(const TEnvPtr& tenv, Definitions* ds, const MonoTypePtr& in, MonoTypePtr& out) { + if (is(in)) { + out = arrayty(primty("char")); + return true; + } + if (is(in)) { + out = primty("long"); + return true; + } + if (TApp *tapp = is(in)) { + if (*tapp->fn() == *primty("quote")) { + if (TExpr* e = is(tapp->args()[0])) { + out = validateType(tenv, e->expr(), ds)->type()->monoType(); + return true; + } + } + } + return false; +} + + +struct MonoTypePtrToExpr : public switchType { + TEnvPtr tenv; + MonoTypePtr(type); + LexicalAnnotation la; + MonoTypePtrToExpr(const TEnvPtr tenv, const MonoTypePtr& type) : tenv(tenv), type(type) {} + + ExprPtr roll(ExprPtr e) const { + return fncall(var("roll", la), list(e), la); + } + + ExprPtr ret(const char * name, ExprPtr e) const { + ExprPtr o = fncall(var("roll", la), list(ExprPtr(new MkVariant(name, e, la))), la); + return ExprPtr(new Assump(o, qualtype(type), la));; + } + + ExprPtr with(const TVar*) const { + // We only want to see actual types + return ExprPtr(); + } + + ExprPtr with(const TGen*) const { + // I don't think we can get one of these here, and we don't want it. + return ExprPtr(); + } + + ExprPtr with(const TExpr *) const { + // We can't put an arbitrary value in a Type, can we do something else? + return ExprPtr(); + } + + ExprPtr with(const Prim* prim) const { + ExprPtr name(mkarray(prim->name(), la)); + ExprPtr rep; + if (prim->representation()) { + rep = ExprPtr(new MkVariant(".f1", switchOf(prim->representation(), *this), la)); + } else { + rep = var("nothing", la); + } + + MkRecord::FieldDefs fs; + 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(".f0", 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))); + } + + ExprPtr with(const Variant* v) const { + Exprs entries; + for(auto m : v->members()) { + MkRecord::FieldDefs fs; + fs.push_back(MkRecord::FieldDef(".f0", mkarray(m.selector, la))); + fs.push_back(MkRecord::FieldDef(".f1", switchOf(m.type, *this))); + fs.push_back(MkRecord::FieldDef(".f2", constant(static_cast(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(".f0", mkarray(op->name(), la))); + fs.push_back(MkRecord::FieldDef(".f1", constant(static_cast(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(".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(".f0", name)); + fs.push_back(MkRecord::FieldDef(".f1", type)); + return ret("Recursive", mkrecord(fs, la)); + } + + ExprPtr with(const TAbs* tabs) const { + Exprs args; + args.resize(tabs->args().size()); + for(auto s : tabs->args()) { + args.push_back(ExprPtr(mkarray(s, la))); + } + ExprPtr arge(new MkArray(args, la)); + ExprPtr body = switchOf(tabs->body(), *this); + MkRecord::FieldDefs fs; + fs.push_back(MkRecord::FieldDef(".f0", arge)); + fs.push_back(MkRecord::FieldDef(".f1", body)); + return ret("TAbs", mkrecord(fs, la)); + } + + ExprPtr with(const TApp* tapp) const { + + ExprPtr fn = switchOf(tapp->fn(), *this); + Exprs args; + for(auto t : tapp->args()) { + args.push_back(switchOf(t, *this)); + } + MkRecord::FieldDefs fs; + fs.push_back(MkRecord::FieldDef(".f0", fn)); + fs.push_back(MkRecord::FieldDef(".f1", ExprPtr(new MkArray(args, la)))); + return ret("TApp", mkrecord(fs, la)); + } + + ExprPtr with(const Func* v) const { + Exprs ps; + for(auto p : v->parameters()) { + ps.push_back(switchOf(p, *this)); + } + ExprPtr r = switchOf(v->result(), *this); + MkRecord::FieldDefs fs; + fs.push_back(MkRecord::FieldDef(".f0", ExprPtr(new MkArray(ps, la)))); + fs.push_back(MkRecord::FieldDef(".f1", r)); + return ret("Func", mkrecord(fs, la)); + } + + ExprPtr with(const Array* ar) const { + return ret("Array", switchOf(ar->type(), *this)); + } + + ExprPtr with(const FixedArray* ar) const { + ExprPtr l = switchOf(ar->length(), *this); + ExprPtr t = switchOf(ar->type(), *this); + MkRecord::FieldDefs fs; + fs.push_back(MkRecord::FieldDef(".f0", t)); + fs.push_back(MkRecord::FieldDef(".f1", l)); + return ret("FixedArray", mkrecord(fs, la)); + + } + + ExprPtr with(const TString* tstr) const { + return ExprPtr(mkarray(tstr->value(), la)); + } + + ExprPtr with(const TLong* tlong) const { + return constant(tlong->value(), la); + } + +}; + + +struct Type; +MonoTypePtr typeExprToMonoTypePtr(Type*); + +struct _Prim { + typedef std::pair*, variant> type; + static MonoTypePtr build(_Prim::type& p){ + MonoTypePtr aty; + if (Type** at = p.second.get()) { + aty = typeExprToMonoTypePtr(*at); + } + return primty(makeStdString(p.first).c_str(), aty); + } +}; + +struct _Record { + typedef array*, Type*>>* type; + static MonoTypePtr build(_Record::type& rec) { + Record::Members mems; + for(unsigned int i = 0; i < rec->size; ++i) { + mems.push_back(Record::Member(makeStdString(rec->data[i].first), typeExprToMonoTypePtr(rec->data[i].second))); + } + return Record::make(mems); + } +}; + +struct _Variant { + typedef array*, Type*, 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]))); + } + return Variant::make(mems); + } +}; + +struct _OpaquePtr { + typedef std::tuple*, 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)); + } +}; + +struct _Exists { + typedef std::pair*, Type*> type; + static MonoTypePtr build(_Exists::type& ex) { + return Exists::make(makeStdString(std::get<0>(ex)), typeExprToMonoTypePtr(std::get<1>(ex))); + } +}; + +struct _Recursive { + typedef std::pair*, Type*> type; + static MonoTypePtr build(_Recursive::type& ex) { + return Recursive::make(makeStdString(std::get<0>(ex)), typeExprToMonoTypePtr(std::get<1>(ex))); + } +}; + +struct _TAbs { + typedef std::pair*>*, Type*> type; + static MonoTypePtr build(_TAbs::type& tabs) { + str::seq s; + for(unsigned int i = 0; i < tabs.first->size; ++i) { + s.push_back(makeStdString(tabs.first->data[i])); + } + return TAbs::make(s, typeExprToMonoTypePtr(tabs.second)); + } +}; + +struct _TApp { + typedef std::pair*> type; + static MonoTypePtr build(_TApp::type& tapp) { + MonoTypes ms; + for(unsigned int i = 0; i < tapp.second->size; ++i) { + ms.push_back(typeExprToMonoTypePtr(tapp.second->data[i])); + } + return TApp::make(typeExprToMonoTypePtr(tapp.first), ms); + } +}; + +struct _Func { + typedef std::pair*, Type*> type; + static MonoTypePtr build(_Func::type& f) { + Record::Members mems; + for(unsigned int i = 0; i < f.first->size; ++i) { + mems.push_back(Record::Member(".f" + str::from(i), typeExprToMonoTypePtr(f.first->data[i]))); + } + return Func::make(Record::make(mems), typeExprToMonoTypePtr(f.second)); + } +}; + +struct _Array { + typedef Type* type; + static MonoTypePtr build(_Array::type& ar) { + return Array::make(typeExprToMonoTypePtr(ar)); + } +}; + +struct _FixedArray { + typedef std::pair type; + static MonoTypePtr build(_FixedArray::type& far) { + return FixedArray::make(typeExprToMonoTypePtr(far.first), typeExprToMonoTypePtr(far.second)); + } +}; + +struct Type { + typedef variant<_Prim::type, _Record::type, _Variant::type, _OpaquePtr::type, _Exists::type, _Recursive::type, _TAbs::type, _TApp::type, _Func::type, _Array::type, _FixedArray::type> def; + def data; +}; + +#define BUILD(x) x ::build(*reinterpret_cast< x ::type*>(t->data.unsafePayload())) +MonoTypePtr typeExprToMonoTypePtr(Type* t){ + switch (t->data.unsafeTag()) { + case 0: + return BUILD(_Prim); + case 1: + return BUILD(_Record); + case 2: + return BUILD(_Variant); + case 3: + return BUILD(_OpaquePtr); + case 4: + return BUILD(_Exists); + case 5: + return BUILD(_Recursive); + case 6: + return BUILD(_TAbs); + case 7: + return BUILD(_TApp); + case 8: + return BUILD(_Func); + case 9: + return BUILD(_Array); + case 10: + return BUILD(_FixedArray); + } + return MonoTypePtr(); +} + + +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 : public liftType { }; + +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")) { + r = MonoTypePtr(TLong::make(ctx->compileFn(e)())); + return true; + } else if (*e->type()->monoType() == *arrayty(primty("char"))) { + array * hs = ctx->compileFn*()>(e)(); + r = MonoTypePtr(TString::make(std::string(hs->data, hs->data + hs->size))); + return true; + } else if (*e->type()->monoType() == *tptr) { + Type* te = ctx->compileFn(e)(); + r = typeExprToMonoTypePtr(te); + return true; + } else { + return false; + } + } catch(...) { return false; } +} + + +bool decodeTAConstraint(cc*ctx, const TEnvPtr tenv, Definitions* ds, const ConstraintPtr& c, MonoTypePtr& l, MonoTypePtr& r) { + MonoTypePtr tptr = ctx->replaceTypeAliases(primty("Type")); + type_ = tptr; + if (c->name() == TypeApply::constraintName() && c->arguments().size() > 1) { + l = c->arguments()[0]; + if (TApp * tapp = is(c->arguments()[1])) { + if(tapp->args().size() == 1 && *tapp->fn() == *primty("quote")) { + if (TExpr* te = is(tapp->args()[0])) { + ExprPtr f = te->expr(); + Exprs args; + + for(unsigned int i = 2; i < c->arguments().size(); ++i) { + ExprPtr arg; + if (TApp* tapp = is(c->arguments()[i])) { + if (*tapp->fn() == *primty("quote")) { + if (TExpr* e = is(tapp->args()[0])) { + arg = e->expr(); + } + } + } + if(!arg) {arg = switchOf(c->arguments()[i], MonoTypePtrToExpr(tenv, tptr));} + if (arg) { + args.push_back(arg); + } else { + return false; + } + } + + if(evalType(ctx, tenv, ds, tptr, fncall(f, args, LexicalAnnotation()), r)) { + return true; + } + // This doesn't seem to work how I'd hoped, closures don't get eval'ed + // properly. + if(evalType(ctx, tenv, ds, tptr, closcall(f, args, LexicalAnnotation()), r)) { + return true; + } + return false; + } + } + } + } + return false; +} + + +std::string TypeApply::constraintName() { + return "TypeApply"; +} + +bool TypeApply::refine(const TEnvPtr& tenv, const ConstraintPtr& cst, MonoTypeUnifier* u, Definitions* ds) { + MonoTypePtr l, r; + if(decodeTAConstraint(this->c, tenv, ds, cst, l, r)){ + size_t uc = u->size(); + mgu(l, r, u); + bool ret= uc != u->size(); + return ret; + } + return false; +} + +struct TAUnqualify : public switchExprTyFn { + ConstraintPtr c; + TAUnqualify(const ConstraintPtr& c) : c(c) { } + + QualTypePtr withTy(const QualTypePtr& qt) const { + return removeConstraint(this->c, qt); + } + +}; + +ExprPtr TypeApply::unqualify(const TEnvPtr&, const ConstraintPtr& cst, const ExprPtr& e, Definitions*) const { + return switchOf(e, TAUnqualify(cst)); +} + +bool TypeApply::satisfied(const TEnvPtr& tenv, const ConstraintPtr& cst, Definitions* ds) const { + MonoTypePtr l, r; + if(decodeTAConstraint(this->c, tenv, ds, cst, l, r)){ + bool ret = *l == *r; + return ret; + } + return false; +} + +bool TypeApply::satisfiable(const TEnvPtr& tenv, const ConstraintPtr& cst, Definitions* ds) const { + for(auto a : cst->arguments()) { + if (is(a)) return true; + } + return satisfied(tenv, cst, ds); +} + +void TypeApply::explain(const TEnvPtr&, const ConstraintPtr&, const ExprPtr&, Definitions*, annmsgs*) { +} + +PolyTypePtr TypeApply::lookup(const std::string&) const { + return PolyTypePtr(); +} + +SymSet TypeApply::bindings() const { + return SymSet(); +} + +FunDeps TypeApply::dependencies(const ConstraintPtr&) const { + return FunDeps(); +} + + + +static bool decodeTVLConstraint(const TEnvPtr& tenv, const ConstraintPtr& c, Definitions *ds, MonoTypePtr* l, MonoTypePtr* r) { + if (c->name() == TypeValueLower::constraintName() && c->arguments().size() == 2) { + *r = c->arguments()[1]; + return tvalueToMonoTypePtr(tenv, ds, c->arguments()[0], *l); + } + return false; +} + +std::string TypeValueLower::constraintName() { + return "TypeValueLower"; +} + +bool TypeValueLower::refine(const TEnvPtr& tenv, const ConstraintPtr& cst, MonoTypeUnifier* u, Definitions* ds) { + MonoTypePtr l, r; + if(decodeTVLConstraint(tenv, cst, ds, &l, &r)){ + size_t uc = u->size(); + mgu(l, r, u); + return uc != u->size(); + } + return false; +} + +struct TVLUnqualify : public switchExprTyFn { + ConstraintPtr c; + TVLUnqualify(const ConstraintPtr& c) : c(c) { } + + QualTypePtr withTy(const QualTypePtr& qt) const { + return removeConstraint(this->c, qt); + } + + ExprPtr with(const Var* vn) const { + if (vn->value() == "typeValueLower") { + return wrapWithTy(vn->type(), new Var(".typeValueLower", vn->la())); + } else { + return wrapWithTy(vn->type(), new Var(vn->value(), vn->la())); + } + } +}; + +ExprPtr TypeValueLower::unqualify(const TEnvPtr&, const ConstraintPtr& cst, const ExprPtr& e, Definitions*) const { + return switchOf(e, TVLUnqualify(cst)); +} + +bool TypeValueLower::satisfied(const TEnvPtr& tenv, const ConstraintPtr& cst, Definitions* ds) const { + MonoTypePtr l, r; + if(decodeTVLConstraint(tenv, cst, ds, &l, &r)){ + return *l == *r; + } + return false; +} + +bool TypeValueLower::satisfiable(const TEnvPtr& tenv, const ConstraintPtr& cst, Definitions* ds) const { + if (is(cst->arguments()[0])) { + return true; + } + MonoTypePtr l, r; + if(decodeTVLConstraint(tenv, cst, ds, &l, &r)){ + return unifiable(tenv, l, r); + } + return false; +} + +void TypeValueLower::explain(const TEnvPtr&, const ConstraintPtr&, const ExprPtr&, Definitions*, annmsgs*) { +} + +PolyTypePtr TypeValueLower::lookup(const std::string& vn) const { + if (vn == "typeValueLower") { + return polytype(2, qualtype(list(ConstraintPtr(new Constraint(constraintName(), list(tgen(0), tgen(1))))), functy(list(tgen(0)), tgen(1)))); + } else { + return PolyTypePtr(); + } +} + +SymSet TypeValueLower::bindings() const { + SymSet r; + r.insert("typeValueLower"); + return r; +} + +FunDeps TypeValueLower::dependencies(const ConstraintPtr&) const { + FunDeps result; + return result; +} +} From a02906d046d5aba3fe5c774cd5a404d135c46654 Mon Sep 17 00:00:00 2001 From: adam-antonik Date: Fri, 22 May 2020 18:11:50 +0100 Subject: [PATCH 02/11] put type in boot --- include/hobbes/boot/gen/bootdata.H | 25 +++++++++++++++++++++++++ lib/hobbes/boot/dependent.hob | 3 +++ 2 files changed, 28 insertions(+) create mode 100644 lib/hobbes/boot/dependent.hob diff --git a/include/hobbes/boot/gen/bootdata.H b/include/hobbes/boot/gen/bootdata.H index 4b47de5f6..1a5fa9fd1 100644 --- a/include/hobbes/boot/gen/bootdata.H +++ b/include/hobbes/boot/gen/bootdata.H @@ -1304,6 +1304,29 @@ unsigned char __convert_hob[] = { 0x73, 0x74, 0x29, 0x3b, 0x7d, 0x0a, 0x0a }; unsigned int __convert_hob_len = 4759; +unsigned char __dependent_hob[] = { + 0x0a, 0x74, 0x79, 0x70, 0x65, 0x20, 0x54, 0x79, 0x70, 0x65, 0x20, 0x3d, + 0x20, 0x5e, 0x78, 0x2e, 0x7c, 0x50, 0x72, 0x69, 0x6d, 0x3a, 0x28, 0x5b, + 0x63, 0x68, 0x61, 0x72, 0x5d, 0x20, 0x2a, 0x20, 0x28, 0x28, 0x29, 0x20, + 0x2b, 0x20, 0x78, 0x29, 0x29, 0x2c, 0x20, 0x52, 0x65, 0x63, 0x6f, 0x72, + 0x64, 0x3a, 0x5b, 0x5b, 0x63, 0x68, 0x61, 0x72, 0x5d, 0x2a, 0x78, 0x5d, + 0x2c, 0x20, 0x56, 0x61, 0x72, 0x69, 0x61, 0x6e, 0x74, 0x3a, 0x5b, 0x5b, + 0x63, 0x68, 0x61, 0x72, 0x5d, 0x2a, 0x78, 0x2a, 0x69, 0x6e, 0x74, 0x5d, + 0x2c, 0x20, 0x4f, 0x70, 0x61, 0x71, 0x75, 0x65, 0x50, 0x74, 0x72, 0x3a, + 0x28, 0x5b, 0x63, 0x68, 0x61, 0x72, 0x5d, 0x2a, 0x69, 0x6e, 0x74, 0x2a, + 0x62, 0x6f, 0x6f, 0x6c, 0x29, 0x2c, 0x20, 0x45, 0x78, 0x69, 0x73, 0x74, + 0x73, 0x3a, 0x28, 0x5b, 0x63, 0x68, 0x61, 0x72, 0x5d, 0x2a, 0x78, 0x29, + 0x2c, 0x20, 0x52, 0x65, 0x63, 0x75, 0x72, 0x73, 0x69, 0x76, 0x65, 0x3a, + 0x28, 0x5b, 0x63, 0x68, 0x61, 0x72, 0x5d, 0x2a, 0x78, 0x29, 0x2c, 0x20, + 0x54, 0x41, 0x62, 0x73, 0x3a, 0x28, 0x5b, 0x5b, 0x63, 0x68, 0x61, 0x72, + 0x5d, 0x5d, 0x2a, 0x78, 0x29, 0x2c, 0x20, 0x54, 0x41, 0x70, 0x70, 0x3a, + 0x28, 0x78, 0x2a, 0x5b, 0x78, 0x5d, 0x29, 0x2c, 0x20, 0x46, 0x75, 0x6e, + 0x63, 0x3a, 0x28, 0x5b, 0x78, 0x5d, 0x2a, 0x78, 0x29, 0x2c, 0x20, 0x41, + 0x72, 0x72, 0x61, 0x79, 0x3a, 0x78, 0x2c, 0x20, 0x46, 0x69, 0x78, 0x65, + 0x64, 0x41, 0x72, 0x72, 0x61, 0x79, 0x3a, 0x28, 0x78, 0x2a, 0x78, 0x29, + 0x7c, 0x0a, 0x0a +}; +unsigned int __dependent_hob_len = 231; unsigned char __eq_hob[] = { 0x2f, 0x2a, 0x0a, 0x20, 0x2a, 0x20, 0x65, 0x71, 0x75, 0x61, 0x6c, 0x69, 0x74, 0x79, 0x2f, 0x65, 0x71, 0x75, 0x69, 0x76, 0x61, 0x6c, 0x65, 0x6e, @@ -11451,6 +11474,7 @@ unsigned char* module_defs[] = { __amapping_hob, __arith_hob, __convert_hob, +__dependent_hob, __eq_hob, __eqord_hob, __farray_hob, @@ -11479,6 +11503,7 @@ unsigned int module_lens[] = { __amapping_hob_len, __arith_hob_len, __convert_hob_len, +__dependent_hob_len, __eq_hob_len, __eqord_hob_len, __farray_hob_len, diff --git a/lib/hobbes/boot/dependent.hob b/lib/hobbes/boot/dependent.hob new file mode 100644 index 000000000..7c0de695c --- /dev/null +++ b/lib/hobbes/boot/dependent.hob @@ -0,0 +1,3 @@ + +type Type = ^x.|Prim:([char] * (() + x)), Record:[[char]*x], Variant:[[char]*x*int], OpaquePtr:([char]*int*bool), Exists:([char]*x), Recursive:([char]*x), TAbs:([[char]]*x), TApp:(x*[x]), Func:([x]*x), Array:x, FixedArray:(x*x)| + From 9aded3701e612f1f0ef584d8c63f41065e13503a Mon Sep 17 00:00:00 2001 From: adam-antonik Date: Fri, 22 May 2020 19:46:50 +0100 Subject: [PATCH 03/11] remove the not needed --- lib/hobbes/lang/preds/dependent.C | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C index ee08a368f..76e4fff00 100644 --- a/lib/hobbes/lang/preds/dependent.C +++ b/lib/hobbes/lang/preds/dependent.C @@ -28,7 +28,7 @@ static bool tvalueToMonoTypePtr(const TEnvPtr& tenv, Definitions* ds, const Mono struct MonoTypePtrToExpr : public switchType { TEnvPtr tenv; - MonoTypePtr(type); + MonoTypePtr type; LexicalAnnotation la; MonoTypePtrToExpr(const TEnvPtr tenv, const MonoTypePtr& type) : tenv(tenv), type(type) {} From 37c96422b46f94b298186c82d3d78cb7afec1c41 Mon Sep 17 00:00:00 2001 From: adam-antonik Date: Fri, 22 May 2020 20:22:26 +0100 Subject: [PATCH 04/11] (maybe) Fix build --- lib/hobbes/lang/preds/dependent.C | 44 +++++++++++++++---------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C index 76e4fff00..2211db006 100644 --- a/lib/hobbes/lang/preds/dependent.C +++ b/lib/hobbes/lang/preds/dependent.C @@ -66,8 +66,8 @@ struct MonoTypePtrToExpr : public switchType { } MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", name)); - fs.push_back(MkRecord::FieldDef(".f1", rep)); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", name))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", rep))); return ret("Prim", mkrecord(fs, la)); } @@ -75,8 +75,8 @@ struct MonoTypePtrToExpr : public switchType { Exprs entries; for(auto m : r->members()) { MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", mkarray(m.field, la))); - fs.push_back(MkRecord::FieldDef(".f1", switchOf(m.type, *this))); + 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)))); entries.push_back(mkrecord(fs, la)); } return ret("Record", ExprPtr(new MkArray(entries, la))); @@ -86,9 +86,9 @@ struct MonoTypePtrToExpr : public switchType { Exprs entries; for(auto m : v->members()) { MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", mkarray(m.selector, la))); - fs.push_back(MkRecord::FieldDef(".f1", switchOf(m.type, *this))); - fs.push_back(MkRecord::FieldDef(".f2", constant(static_cast(m.id), la))); + 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(m.id), la)))); entries.push_back(mkrecord(fs, la)); } return ret("Variant", ExprPtr(new MkArray(entries, la))); @@ -96,9 +96,9 @@ struct MonoTypePtrToExpr : public switchType { ExprPtr with(const OpaquePtr* op) const { MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", mkarray(op->name(), la))); - fs.push_back(MkRecord::FieldDef(".f1", constant(static_cast(op->size()), la))); - fs.push_back(MkRecord::FieldDef(".f2", constant(op->storedContiguously(), la))); + 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(op->size()), la)))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f2", constant(op->storedContiguously(), la)))); return ret("OpaquePtr", mkrecord(fs, la)); } @@ -106,8 +106,8 @@ struct MonoTypePtrToExpr : public switchType { ExprPtr name = ExprPtr(mkarray(e->absTypeName(), la)); ExprPtr type = switchOf(e->absType(), *this); MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", name)); - fs.push_back(MkRecord::FieldDef(".f1", type)); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", name))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", type))); return ret("Exists", mkrecord(fs, la)); } @@ -115,8 +115,8 @@ struct MonoTypePtrToExpr : public switchType { ExprPtr name = ExprPtr(mkarray(e->recTypeName(), la)); ExprPtr type = switchOf(e->recType(), *this); MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", name)); - fs.push_back(MkRecord::FieldDef(".f1", type)); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", name))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", type))); return ret("Recursive", mkrecord(fs, la)); } @@ -129,8 +129,8 @@ struct MonoTypePtrToExpr : public switchType { ExprPtr arge(new MkArray(args, la)); ExprPtr body = switchOf(tabs->body(), *this); MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", arge)); - fs.push_back(MkRecord::FieldDef(".f1", body)); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", arge))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", body))); return ret("TAbs", mkrecord(fs, la)); } @@ -142,8 +142,8 @@ struct MonoTypePtrToExpr : public switchType { args.push_back(switchOf(t, *this)); } MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", fn)); - fs.push_back(MkRecord::FieldDef(".f1", ExprPtr(new MkArray(args, la)))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", fn))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", ExprPtr(new MkArray(args, la))))); return ret("TApp", mkrecord(fs, la)); } @@ -154,8 +154,8 @@ struct MonoTypePtrToExpr : public switchType { } ExprPtr r = switchOf(v->result(), *this); MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", ExprPtr(new MkArray(ps, la)))); - fs.push_back(MkRecord::FieldDef(".f1", r)); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", ExprPtr(new MkArray(ps, la))))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", r))); return ret("Func", mkrecord(fs, la)); } @@ -167,8 +167,8 @@ struct MonoTypePtrToExpr : public switchType { ExprPtr l = switchOf(ar->length(), *this); ExprPtr t = switchOf(ar->type(), *this); MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", t)); - fs.push_back(MkRecord::FieldDef(".f1", l)); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f0", t))); + fs.push_back(MkRecord::FieldDef(std::make_pair(".f1", l))); return ret("FixedArray", mkrecord(fs, la)); } From 72bbab4c8b45f42d23dcd607ad943058957121c4 Mon Sep 17 00:00:00 2001 From: adam-antonik Date: Sat, 23 May 2020 15:01:51 +0100 Subject: [PATCH 05/11] Only lower top level TLong and TString, others go into Type. Allow Type to contain TVars, maybe returning them is useful --- include/hobbes/boot/gen/bootdata.H | 7 +++- lib/hobbes/boot/dependent.hob | 2 +- lib/hobbes/lang/preds/dependent.C | 59 ++++++++++++++++++++++++------ 3 files changed, 53 insertions(+), 15 deletions(-) diff --git a/include/hobbes/boot/gen/bootdata.H b/include/hobbes/boot/gen/bootdata.H index 1a5fa9fd1..c441cd96a 100644 --- a/include/hobbes/boot/gen/bootdata.H +++ b/include/hobbes/boot/gen/bootdata.H @@ -1324,9 +1324,12 @@ unsigned char __dependent_hob[] = { 0x63, 0x3a, 0x28, 0x5b, 0x78, 0x5d, 0x2a, 0x78, 0x29, 0x2c, 0x20, 0x41, 0x72, 0x72, 0x61, 0x79, 0x3a, 0x78, 0x2c, 0x20, 0x46, 0x69, 0x78, 0x65, 0x64, 0x41, 0x72, 0x72, 0x61, 0x79, 0x3a, 0x28, 0x78, 0x2a, 0x78, 0x29, - 0x7c, 0x0a, 0x0a + 0x2c, 0x20, 0x54, 0x53, 0x74, 0x72, 0x69, 0x6e, 0x67, 0x3a, 0x5b, 0x63, + 0x68, 0x61, 0x72, 0x5d, 0x2c, 0x20, 0x54, 0x4c, 0x6f, 0x6e, 0x67, 0x3a, + 0x6c, 0x6f, 0x6e, 0x67, 0x2c, 0x20, 0x54, 0x56, 0x61, 0x72, 0x3a, 0x5b, + 0x63, 0x68, 0x61, 0x72, 0x5d, 0x7c, 0x0a, 0x0a }; -unsigned int __dependent_hob_len = 231; +unsigned int __dependent_hob_len = 272; unsigned char __eq_hob[] = { 0x2f, 0x2a, 0x0a, 0x20, 0x2a, 0x20, 0x65, 0x71, 0x75, 0x61, 0x6c, 0x69, 0x74, 0x79, 0x2f, 0x65, 0x71, 0x75, 0x69, 0x76, 0x61, 0x6c, 0x65, 0x6e, diff --git a/lib/hobbes/boot/dependent.hob b/lib/hobbes/boot/dependent.hob index 7c0de695c..9dffd78af 100644 --- a/lib/hobbes/boot/dependent.hob +++ b/lib/hobbes/boot/dependent.hob @@ -1,3 +1,3 @@ -type Type = ^x.|Prim:([char] * (() + x)), Record:[[char]*x], Variant:[[char]*x*int], OpaquePtr:([char]*int*bool), Exists:([char]*x), Recursive:([char]*x), TAbs:([[char]]*x), TApp:(x*[x]), Func:([x]*x), Array:x, FixedArray:(x*x)| +type Type = ^x.|Prim:([char] * (() + x)), Record:[[char]*x], Variant:[[char]*x*int], OpaquePtr:([char]*int*bool), Exists:([char]*x), Recursive:([char]*x), TAbs:([[char]]*x), TApp:(x*[x]), Func:([x]*x), Array:x, FixedArray:(x*x), TString:[char], TLong:long, TVar:[char]| diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C index 2211db006..fb508c4db 100644 --- a/lib/hobbes/lang/preds/dependent.C +++ b/lib/hobbes/lang/preds/dependent.C @@ -41,19 +41,18 @@ struct MonoTypePtrToExpr : public switchType { return ExprPtr(new Assump(o, qualtype(type), la));; } - ExprPtr with(const TVar*) const { - // We only want to see actual types - return ExprPtr(); + ExprPtr with(const TVar* tv) const { + return ret("TVar", ExprPtr(mkarray(tv->name(), la))); } ExprPtr with(const TGen*) const { // I don't think we can get one of these here, and we don't want it. - return ExprPtr(); + throw std::runtime_error("TGen in TypeApply"); } ExprPtr with(const TExpr *) const { // We can't put an arbitrary value in a Type, can we do something else? - return ExprPtr(); + throw std::runtime_error("TExpr in TypeApply"); } ExprPtr with(const Prim* prim) const { @@ -174,11 +173,11 @@ struct MonoTypePtrToExpr : public switchType { } ExprPtr with(const TString* tstr) const { - return ExprPtr(mkarray(tstr->value(), la)); + return ret("TString", ExprPtr(mkarray(tstr->value(), la))); } ExprPtr with(const TLong* tlong) const { - return constant(tlong->value(), la); + return ret("TLong", constant(tlong->value(), la)); } }; @@ -288,8 +287,29 @@ struct _FixedArray { } }; +struct _TString { + typedef array* type; + static MonoTypePtr build(_TString::type& str) { + return TString::make(std::string(str->data, str->data + str->size)); + } +}; + +struct _TLong { + typedef long type; + static MonoTypePtr build(_TLong::type& l) { + return TLong::make(l); + } +}; + +struct _TVar { + typedef array* type; + static MonoTypePtr build(_TString::type& str) { + return TVar::make(std::string(str->data, str->data + str->size)); + } +}; + struct Type { - typedef variant<_Prim::type, _Record::type, _Variant::type, _OpaquePtr::type, _Exists::type, _Recursive::type, _TAbs::type, _TApp::type, _Func::type, _Array::type, _FixedArray::type> def; + typedef variant<_Prim::type, _Record::type, _Variant::type, _OpaquePtr::type, _Exists::type, _Recursive::type, _TAbs::type, _TApp::type, _Func::type, _Array::type, _FixedArray::type, _TString, _TLong, _TVar> def; def data; }; @@ -318,6 +338,12 @@ MonoTypePtr typeExprToMonoTypePtr(Type* t){ return BUILD(_Array); case 10: return BUILD(_FixedArray); + case 11: + return BUILD(_TString); + case 12: + return BUILD(_TLong); + case 13: + return BUILD(_TVar); } return MonoTypePtr(); } @@ -360,6 +386,7 @@ 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) { MonoTypePtr tptr = ctx->replaceTypeAliases(primty("Type")); type_ = tptr; + LexicalAnnotation la; if (c->name() == TypeApply::constraintName() && c->arguments().size() > 1) { l = c->arguments()[0]; if (TApp * tapp = is(c->arguments()[1])) { @@ -370,14 +397,22 @@ bool decodeTAConstraint(cc*ctx, const TEnvPtr tenv, Definitions* ds, const Const for(unsigned int i = 2; i < c->arguments().size(); ++i) { ExprPtr arg; - if (TApp* tapp = is(c->arguments()[i])) { + MonoTypePtr targ = c->arguments()[i]; + if (TApp* tapp = is(targ)) { if (*tapp->fn() == *primty("quote")) { if (TExpr* e = is(tapp->args()[0])) { arg = e->expr(); } } } - if(!arg) {arg = switchOf(c->arguments()[i], MonoTypePtrToExpr(tenv, tptr));} + if (TString* tstr = is(targ)) { + arg = ExprPtr(mkarray(tstr->value(), la)); + } + if (TLong* tlong = is(targ)) { + arg = constant(tlong->value(), la); + } + + if(!arg) {arg = switchOf(targ, MonoTypePtrToExpr(tenv, tptr));} if (arg) { args.push_back(arg); } else { @@ -385,12 +420,12 @@ bool decodeTAConstraint(cc*ctx, const TEnvPtr tenv, Definitions* ds, const Const } } - if(evalType(ctx, tenv, ds, tptr, fncall(f, args, LexicalAnnotation()), r)) { + if(evalType(ctx, tenv, ds, tptr, fncall(f, args, la), r)) { return true; } // This doesn't seem to work how I'd hoped, closures don't get eval'ed // properly. - if(evalType(ctx, tenv, ds, tptr, closcall(f, args, LexicalAnnotation()), r)) { + if(evalType(ctx, tenv, ds, tptr, closcall(f, args, la), r)) { return true; } return false; From ed42c495663e45ce7bb7c95a28b222f22973a7cb Mon Sep 17 00:00:00 2001 From: adam-antonik Date: Sat, 23 May 2020 15:16:26 +0100 Subject: [PATCH 06/11] Don't forget now to handle top tvar correctly --- lib/hobbes/lang/preds/dependent.C | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C index fb508c4db..7a6387d70 100644 --- a/lib/hobbes/lang/preds/dependent.C +++ b/lib/hobbes/lang/preds/dependent.C @@ -398,6 +398,9 @@ 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(targ)) { + return false; + } if (TApp* tapp = is(targ)) { if (*tapp->fn() == *primty("quote")) { if (TExpr* e = is(tapp->args()[0])) { From 32d2a056f12047a3c783bab3cd10d2919cb1fa1b Mon Sep 17 00:00:00 2001 From: Kalani Thielen Date: Sun, 24 May 2020 00:14:17 -0400 Subject: [PATCH 07/11] fix field def construction ambiguity (in some compilers) --- lib/hobbes/lang/preds/dependent.C | 44 +++++++++++++++---------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C index 7a6387d70..c06116f8e 100644 --- a/lib/hobbes/lang/preds/dependent.C +++ b/lib/hobbes/lang/preds/dependent.C @@ -65,8 +65,8 @@ struct MonoTypePtrToExpr : public switchType { } 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)); } @@ -74,8 +74,8 @@ struct MonoTypePtrToExpr : public switchType { 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", 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))); @@ -85,9 +85,9 @@ struct MonoTypePtrToExpr : public switchType { 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(m.id), la)))); + fs.push_back(MkRecord::FieldDef(".f0", mkarray(m.selector, la))); + fs.push_back(MkRecord::FieldDef(".f1", switchOf(m.type, *this))); + fs.push_back(MkRecord::FieldDef(".f2", constant(static_cast(m.id), la))); entries.push_back(mkrecord(fs, la)); } return ret("Variant", ExprPtr(new MkArray(entries, la))); @@ -95,9 +95,9 @@ struct MonoTypePtrToExpr : public switchType { 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(op->size()), la)))); - fs.push_back(MkRecord::FieldDef(std::make_pair(".f2", constant(op->storedContiguously(), la)))); + fs.push_back(MkRecord::FieldDef(".f0", mkarray(op->name(), la))); + fs.push_back(MkRecord::FieldDef(".f1", constant(static_cast(op->size()), la))); + fs.push_back(MkRecord::FieldDef(".f2", constant(op->storedContiguously(), la))); return ret("OpaquePtr", mkrecord(fs, la)); } @@ -105,8 +105,8 @@ struct MonoTypePtrToExpr : public switchType { 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)); } @@ -114,8 +114,8 @@ struct MonoTypePtrToExpr : public switchType { 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)); } @@ -128,8 +128,8 @@ struct MonoTypePtrToExpr : public switchType { 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)); } @@ -141,8 +141,8 @@ struct MonoTypePtrToExpr : public switchType { 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)); } @@ -153,8 +153,8 @@ struct MonoTypePtrToExpr : public switchType { } 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)); } @@ -166,8 +166,8 @@ struct MonoTypePtrToExpr : public switchType { 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)); } From 01fcf6a6c16eb2ab289b608aac184fa62767bb4e Mon Sep 17 00:00:00 2001 From: Kalani Thielen Date: Sun, 24 May 2020 00:38:58 -0400 Subject: [PATCH 08/11] construct ref counted pointers explicitly --- lib/hobbes/lang/preds/dependent.C | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C index c06116f8e..e26c05b9c 100644 --- a/lib/hobbes/lang/preds/dependent.C +++ b/lib/hobbes/lang/preds/dependent.C @@ -74,7 +74,7 @@ struct MonoTypePtrToExpr : public switchType { Exprs entries; for(auto m : r->members()) { MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", mkarray(m.field, la))); + 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)); } @@ -85,7 +85,7 @@ struct MonoTypePtrToExpr : public switchType { Exprs entries; for(auto m : v->members()) { MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", mkarray(m.selector, 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(m.id), la))); entries.push_back(mkrecord(fs, la)); @@ -95,7 +95,7 @@ struct MonoTypePtrToExpr : public switchType { ExprPtr with(const OpaquePtr* op) const { MkRecord::FieldDefs fs; - fs.push_back(MkRecord::FieldDef(".f0", mkarray(op->name(), la))); + fs.push_back(MkRecord::FieldDef(".f0", ExprPtr(mkarray(op->name(), la)))); fs.push_back(MkRecord::FieldDef(".f1", constant(static_cast(op->size()), la))); fs.push_back(MkRecord::FieldDef(".f2", constant(op->storedContiguously(), la))); return ret("OpaquePtr", mkrecord(fs, la)); From b91b5b001bcda6510d90da4d4679be89e609d1a3 Mon Sep 17 00:00:00 2001 From: Kalani Thielen Date: Mon, 25 May 2020 17:29:17 -0400 Subject: [PATCH 09/11] avoid storing a global variable to lift the "Type" type --- lib/hobbes/lang/preds/dependent.C | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C index e26c05b9c..5e0432164 100644 --- a/lib/hobbes/lang/preds/dependent.C +++ b/lib/hobbes/lang/preds/dependent.C @@ -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 : public liftType { }; + struct lift { + 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")) { @@ -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]; @@ -397,10 +391,10 @@ 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(targ)) { + MonoTypePtr targ = c->arguments()[i]; + if (is(targ)) { return false; - } + } if (TApp* tapp = is(targ)) { if (*tapp->fn() == *primty("quote")) { if (TExpr* e = is(tapp->args()[0])) { @@ -408,7 +402,7 @@ bool decodeTAConstraint(cc*ctx, const TEnvPtr tenv, Definitions* ds, const Const } } } - if (TString* tstr = is(targ)) { + if (TString* tstr = is(targ)) { arg = ExprPtr(mkarray(tstr->value(), la)); } if (TLong* tlong = is(targ)) { From 1aeb1433c5bcacfa79f00c39a065d37527758467 Mon Sep 17 00:00:00 2001 From: Kalani Thielen Date: Mon, 25 May 2020 17:56:42 -0400 Subject: [PATCH 10/11] add an sprintf test to demo and validate lower and apply functions added in this PR --- test/DependentTypes.C | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 test/DependentTypes.C diff --git a/test/DependentTypes.C b/test/DependentTypes.C new file mode 100644 index 000000000..97b96d85a --- /dev/null +++ b/test/DependentTypes.C @@ -0,0 +1,41 @@ + +#include +#include "test.H" + +using namespace hobbes; +static cc& c() { static __thread cc* x = 0; if (!x) { x = new cc(); } return *x; } + +TEST(DependentTypes, SPrintf) { + compile(&c(), c().readModule(R"END( +primty x = roll(|Prim=(x, nothing :: (() + Type))|) :: Type +arrayty x = roll(|Array=x|) :: Type +tstringty x = roll(|TString=x|) :: Type +mktuplety x = roll(|Record=map(\v.(".f"++show(v.0), v.1), zip([0L..size(x)-1], x))|) :: Type + +process :: ([char], int) -> ^x.(() + ((Type * Type * Type) * x)) +process x idx = match x with + | '(?
[^%]*)(?%s)(?.*)' -> cons((tstringty(pre), tstringty(".f" ++ show(idx)), arrayty(primty("char"))), process(suf, idx+1))
+ | '(?
[^%]*)(?%d)(?.*)' -> cons((tstringty(pre), tstringty(".f" ++ show(idx)), primty("int")), process(suf, idx+1))
+ | _ -> cons((tstringty(x), primty("unit"), primty("unit")), nil())
+
+doSPrintf x = let t = toArray(process(x, 0)) in mktuplety(map(\x.mktuplety([x.0, x.1, x.2]), t))
+
+
+class SPrintF a t where
+  sprintf_ :: (a, t) -> [char]
+instance (a=((str * () * ()) * ())) => SPrintF a _ where
+  sprintf_ r t = typeValueLower(unsafeCast(())::str)
+instance (a=((str * acc * [char]) * t)) => SPrintF a _ where
+  sprintf_ r t = concat([typeValueLower(unsafeCast(())::str), fieldValue(t)::(_/acc::_)=>_, sprintf_(tupleTail(r), t)])
+instance (a=((str * acc * int) * t)) => SPrintF a _ where
+  sprintf_ r t = concat([typeValueLower(unsafeCast(())::str), showInt(fieldValue(t)::(_/acc::_)=>_), sprintf_(tupleTail(r), t)])
+
+mkSPrintFType :: (TypeApply a `doSPrintf` x) => x -> a
+mkSPrintFType x = unsafeCast()
+
+sprintf fmt args = sprintf_(mkSPrintFType(fmt), args)
+  )END"));
+
+  EXPECT_EQ(makeStdString(c().compileFn*()>("sprintf(`\"Hello %s %d!\"`, (\"World\", 3))")()), "Hello World 3!");
+}
+

From 28e53af553cffa1a351b74b4280ee75331bea1e5 Mon Sep 17 00:00:00 2001
From: adam-antonik 
Date: Wed, 27 May 2020 09:39:18 +0100
Subject: [PATCH 11/11] std::tuple != tuple.  Use tuple

---
 lib/hobbes/lang/preds/dependent.C | 84 ++++++++++++++-----------------
 1 file changed, 39 insertions(+), 45 deletions(-)

diff --git a/lib/hobbes/lang/preds/dependent.C b/lib/hobbes/lang/preds/dependent.C
index 7a6387d70..a6b1896e1 100644
--- a/lib/hobbes/lang/preds/dependent.C
+++ b/lib/hobbes/lang/preds/dependent.C
@@ -1,4 +1,4 @@
-
+#include 
 #include 
 #include 
 #include 
@@ -65,8 +65,8 @@ struct MonoTypePtrToExpr : public switchType {
     }
 
     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));
   } 
 
@@ -74,8 +74,8 @@ struct MonoTypePtrToExpr : public switchType {
     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)));
@@ -85,9 +85,9 @@ struct MonoTypePtrToExpr : public switchType {
     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(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(m.id), la)));
       entries.push_back(mkrecord(fs, la));
     }
     return ret("Variant", ExprPtr(new MkArray(entries, la)));
@@ -95,9 +95,9 @@ struct MonoTypePtrToExpr : public switchType {
 
   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(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(op->size()), la)));
+    fs.push_back(MkRecord::FieldDef(".f2", constant(op->storedContiguously(), la)));
     return ret("OpaquePtr", mkrecord(fs, la));
   }
 
@@ -105,8 +105,8 @@ struct MonoTypePtrToExpr : public switchType {
     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));
   }
 
@@ -114,8 +114,8 @@ struct MonoTypePtrToExpr : public switchType {
     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));
   }
 
@@ -128,8 +128,8 @@ struct MonoTypePtrToExpr : public switchType {
     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));
   }
 
@@ -141,8 +141,8 @@ struct MonoTypePtrToExpr : public switchType {
       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));
   }
 
@@ -153,8 +153,8 @@ struct MonoTypePtrToExpr : public switchType {
     }
     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));
   }
 
@@ -166,8 +166,8 @@ struct MonoTypePtrToExpr : public switchType {
     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));
 
   }
@@ -209,34 +209,34 @@ struct _Record {
 };
 
 struct _Variant {
-  typedef array*, Type*, int>>* type;
+  typedef array*, 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*, int, bool> type;
+  typedef tuple*, 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>());
   }
 };
 
 struct _Exists {
   typedef std::pair*, 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*, 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));
   }
 };
 
@@ -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 : public liftType { };
+  struct lift {
+    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")) {
@@ -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];
@@ -397,10 +391,10 @@ 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(targ)) {
+            MonoTypePtr targ = c->arguments()[i];
+            if (is(targ)) {
               return false;
-	    }
+            }
             if (TApp* tapp = is(targ)) {
               if (*tapp->fn() == *primty("quote")) {
                 if (TExpr* e = is(tapp->args()[0])) {
@@ -408,7 +402,7 @@ bool decodeTAConstraint(cc*ctx, const TEnvPtr tenv, Definitions* ds, const Const
                 }
               }
             }
-	    if (TString* tstr = is(targ)) {
+            if (TString* tstr = is(targ)) {
               arg = ExprPtr(mkarray(tstr->value(), la));
             }
             if (TLong* tlong = is(targ)) {