restore HaskWeakToStrong functionality that I broke over the weekend

[coq-hetmet.git] / src / HaskWeak.v

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 31accd2..f177e1f 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -43,6 +43,7 @@ Inductive WeakExpr :=
                        WeakExpr.
 
 (* calculate the free WeakVar's in a WeakExpr *)
+(*
 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
   match me with
     | WELit    _        =>     nil
@@ -92,7 +93,7 @@ Definition makeClosedExpression : WeakExpr -> WeakExpr :=
     | nil      => me
     | cv::cvl' => WELam cv (closeExpression me cvl')
   end) me (getWeakExprFreeVars me).
-
+*)
 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
   (WTyCon (haskLiteralToTyCon lit)).
 
@@ -104,25 +105,25 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
     | WEApp   e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
                        match t' with
                          | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
-                         | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
+                         | _ => Error ("found non-function type "+++t'+++" in EApp")
                        end
     | WETyApp e t    => weakTypeOfWeakExpr e >>= fun te =>
                         match te with
                           | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
-                          | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
+                          | _ => Error ("found non-forall type "+++te+++" in ETyApp")
                         end
     | WECoApp e co   => weakTypeOfWeakExpr e >>= fun te =>
                         match te with
                           | WCoFunTy t1 t2 t => OK t
-                          | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
+                          | _ => Error ("found non-coercion type "+++te+++" in ETyApp")
                         end
     | WELam   (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
     | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
-    | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
+    | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
     | WELet   ev ve e            => weakTypeOfWeakExpr e
     | WELetRec rb e              => weakTypeOfWeakExpr e
     | WENote  n e                => weakTypeOfWeakExpr e
-    | WECast  e (weakCoercion t1 t2 _) => OK t2
+    | WECast  e (weakCoercion _ t1 t2 _) => OK t2
     | WECase  scrutinee tbranches tc type_params alts => OK tbranches
 
     (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)