fixes and try tododrop out

examples/paper/03-dependent-binding.makam

@@ -30,8 +30,8 @@ vmap : [A B] (A -> B -> prop) -> vector N A -> vector N B -> prop.
 vmap P vnil vnil.
 vmap P (vcons X XS) (vcons Y YS) :- P X Y, vmap P XS YS.
 
-(* TODO: flip the meaning of square bracket notation in types
-   
+// TODO: flip the meaning of square bracket notation in types
+(*
    Currently square brackets are used in order to specify which type variables should be treated
    parametrically, whereas I think it makes more sense to explicitly call out variables where ad-hoc
    polymorphism is allowed. This will require quite a bit of adaptation.
@@ -81,8 +81,8 @@ dbind : type -> type -> type -> type.
 dbindbase : B -> dbind A unit B.
 dbindnext : (A -> dbind A T B) -> dbind A (A * T) B.
 
-(* TODO: decide between the two
-
+// TODO: decide between the two representations for dbind
+(*
    The good thing about vectors is that they're well-understood from the dependent types literature,
    and also make for quite pleasant higher-order predicates that are entirely equivalent to lists
    and bindmany. As a result, we could elide a lot of the details in the paper, giving only a few
@@ -100,8 +100,8 @@ dbindnext : (A -> dbind A T B) -> dbind A (A * T) B.
 
    The problem with tuples, of course, is that the higher-order predicates etc. don't look as nice,
    and require quite a bit of ad-hoc polymorphism: the whole type of the tuple has to stay abstract
-   and be pattern-matched above, whereas with vectors we only do ad-hoc polymorphism
-   for the 'dependent' argument.
+   and be pattern-matched over, whereas with vectors we only do ad-hoc polymorphism for the
+   'dependent' argument. I've introduced the `subst` type below to mitigate the issue somewhat.
 
    I quite like the fact that the very basic type system of Makam, together with the ad-hoc
    polymorphism that comes for free in the λProlog world, yields such a nice (I think) and easy to
@@ -224,9 +224,9 @@ case_or_else : term -> patt T unit -> dbind term T term -> term -> term.
    is the branch body, where we bind the same number of variables as the ones
    used in the pattern, and the last argument is the `else` case. *)
 
-(* TODO: add typing rules *)
+// TODO: add typing rules
 
-(* TODO: add explanation for evaluation rules *)
+// TODO: add explanation for evaluation rules
 
 patt_to_term : patt T T' -> term -> subst term T' -> subst term T -> prop.
 patt_to_term patt_var X Subst (scons X Subst).
@@ -254,10 +254,10 @@ eval (case_or_else Scrutinee Pattern Body Else) V :-
 eval (app (lam T2 (fun x => case_or_else (tuple [zero, succ (succ x)]) (patt_tuple (patt_cons patt_zero (patt_cons (patt_succ patt_var) patt_nil))) (dbindnext (fun a => dbindnext (fun b => dbindbase b))) zero)) (tuple [zero, succ (succ (succ zero))])) V ?
 *)
 
-(* TODO: there's some bug here. *)
-
-(* TODO: connect this to literature
+// TODO: there's some bug here
 
+// TODO: connect this to literature
+(*
    How does this compare to Crary's trick in LF? 
    What do standard typing rules for patterns look like?
 *)