X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=6d4bf16771bb39220b721f2dc498ecca01f37a05;hp=b2521e388917551cb135b3d1c0966b89b274a37b;hb=e8d9db77f48f7710b5eec6cba6fdaf4650a48c88;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index b2521e3..6d4bf16 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -19,9 +19,6 @@ Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreVars.
 
-(* can remove *)
-Require Import HaskStrongToWeak.
-
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
@@ -513,7 +510,14 @@ Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
     | T_Branch b1 b2                                           => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
   end.
 
-(*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
+Definition checkDistinct :
+  forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
+  intros.
+  set (distinct_decidable lv) as q.
+  destruct q.
+  exact (OK d).
+  exact (Error "checkDistinct failed").
+  Defined.
 
 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
@@ -647,8 +651,9 @@ Definition weakExprToStrongExpr : forall
                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
         end) rb
       in binds >>= fun binds' =>
+         checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
            weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>       
-             OK (ELetRec Γ Δ ξ lev τ _ binds' e')
+             OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
 
     | WECase vscrut escrut tbranches tc avars alts =>
         weakTypeOfWeakExpr escrut >>= fun tscrut =>
@@ -703,6 +708,8 @@ Definition weakExprToStrongExpr : forall
         destruct (ξ c).
         simpl.
       apply e1.
+      rewrite mapleaves.
+      apply rb_distinct.
 
     destruct case_pf.
       set (distinct_decidable (vec2list exprvars')) as dec.