A step towards dependent types

include/hobbes/boot/gen/bootdata.H

@@ -1304,6 +1304,32 @@ 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,
+  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 = 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,
@@ -11451,6 +11477,7 @@ unsigned char* module_defs[] = {
 __amapping_hob,
 __arith_hob,
 __convert_hob,
+__dependent_hob,
 __eq_hob,
 __eqord_hob,
 __farray_hob,
@@ -11479,6 +11506,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,

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 <hobbes/lang/tyunqualify.H>
+#include <hobbes/eval/cc.H>
+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

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), TString:[char], TLong:long, TVar:[char]|
+

lib/hobbes/eval/cc.C

@@ -12,7 +12,7 @@
 #include <hobbes/util/codec.H>
 
 #include <hobbes/util/perf.H>
-
+#include <hobbes/lang/preds/dependent.H>
 // structured file support
 #include <hobbes/db/bindings.H>
 
@@ -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);

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<TString>(ts[0])) {
+	    return c->compile(ExprPtr(mkarray(tstr->value(), LexicalAnnotation())));
+    } 
+    if (TLong* tlong = is<TLong>(ts[0])) {
+	    return c->compile(constant(tlong->value(), LexicalAnnotation()));
+    }
+    if (TApp *tapp = is<TApp>(ts[0])) {
+	if (*tapp->fn() == *primty("quote")) {
+		if (TExpr* e = is<TExpr>(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