note to self in HaskWeak
authorAdam Megacz <megacz@cs.berkeley.edu>
Thu, 26 May 2011 03:52:54 +0000 (20:52 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Thu, 26 May 2011 03:52:54 +0000 (20:52 -0700)
src/HaskWeak.v

index 85f5b24..22f0e60 100644 (file)
@@ -20,6 +20,8 @@ Inductive WeakAltCon :=
 Inductive WeakExpr :=
 | WEVar       : WeakExprVar                                                  -> WeakExpr
 | WELit       : HaskLiteral                                                  -> WeakExpr
 Inductive WeakExpr :=
 | WEVar       : WeakExprVar                                                  -> WeakExpr
 | WELit       : HaskLiteral                                                  -> WeakExpr
+
+(* TO DO: add a WEWhere and use the source location to detect which one the user used *)
 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr