src/HaskWeakToStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakToStrong: convert HaskWeak to HaskStrong                                                                              *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import Coq.Init.Specif.
  12 Require Import HaskKinds.
  13 Require Import HaskCoreLiterals.
  14 Require Import HaskWeakTypes.
  15 Require Import HaskWeakVars.
  16 Require Import HaskWeak.
  17 Require Import HaskStrongTypes.
  18 Require Import HaskStrong.
  19 Require Import HaskCoreTypes.
  20 Require Import HaskCoreVars.
  21
  22 Open Scope string_scope.
  23 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, HaskTyVar Γ wt.
  24 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, HaskCoVar Γ Δ.
  25
  26 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
  27   unfold TyVarResolver.
  28   refine (fun tv' =>
  29     if eqd_dec tv tv'
  30     then let fresh := @FreshHaskTyVar Γ tv in _
  31     else fun TV ite => φ tv' TV (weakITE ite)).
  32   rewrite <- _H; apply fresh.
  33   Defined.
  34
  35 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
  36   : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
  37   induction tvs.
  38   apply φ.
  39   simpl.
  40   apply upφ.
  41   apply IHtvs.
  42   Defined.
  43
  44 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
  45   intro ht.
  46   refine (substT _ θ).
  47   clear θ.
  48   unfold HaskType in ht.
  49   intros.
  50   apply ht.
  51   apply ICons; [ idtac | apply env ].
  52   apply X.
  53   Defined.
  54
  55 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
  56   induction lk.
  57   intro q; apply q.
  58   simpl.
  59   intro q.
  60   apply IHlk.
  61   inversion θ; subst; auto.
  62   inversion θ; subst.
  63   eapply substPhi.
  64   eapply weakT'.
  65   apply X.
  66   apply q.
  67   Defined.
  68
  69 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
  70 Record StrongAltConPlusJunk {tc:TyCon} :=
  71 { sacpj_sac : @StrongAltCon tc
  72 ; sacpj_φ   : forall Γ          (φ:TyVarResolver Γ  ),  (TyVarResolver (sac_Γ sacpj_sac Γ))
  73 ; sacpj_ψ   : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
  74                 (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)))
  75 }.
  76 Implicit Arguments StrongAltConPlusJunk [ ].
  77 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
  78
  79 (* yes, I know, this is really clumsy *)
  80 Variable emptyφ : TyVarResolver nil.
  81   Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
  82
  83 Definition mkPhi (lv:list WeakTypeVar)
  84   : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
  85   set (upφ'(Γ:=nil) lv emptyφ) as φ'.
  86   rewrite <- app_nil_end in φ'.
  87   apply φ'.
  88   Defined.
  89
  90 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
  91 Definition tyConKinds     tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
  92
  93 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
  94 Notation " ` x " := (@fixkind _ x) (at level 100).
  95
  96 Ltac matchThings T1 T2 S :=
  97   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
  98    [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
  99
 100 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
 101   intros.
 102   unfold InstantiatedTypeEnv in ite.
 103   apply X.
 104   apply (X0::::ite).
 105   Defined.
 106
 107 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 108   intro.
 109   unfold HaskType.
 110   intros.
 111   apply (TAll κ).
 112   eapply mkTAll'.
 113   apply X.
 114   apply X0.
 115   Defined.
 116
 117 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
 118   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
 119   match t with
 120     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
 121     | WTyCon      tc    => let case_WTyCon := tt    in _
 122     | WClassP   c lt    => let case_WClassP := tt   in Error "weakTypeToType: WClassP not implemented"
 123     | WIParam _ ty      => let case_WIParam := tt   in Error "weakTypeToType: WIParam not implemented"
 124     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
 125     | WTyVarTy  v       => let case_WTyVarTy := tt  in _
 126     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
 127     | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody >>= fun tbody' => _
 128     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
 129       weakTypeToType _ φ t1 >>= fun t1' =>
 130       weakTypeToType _ φ t2 >>= fun t2' =>
 131       weakTypeToType _ φ t3 >>= fun t3' => _
 132     | WTyFunApp   tc lt =>
 133       ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
 134         { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
 135         match lt with
 136           | nil    => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 137                         | nil => OK (fun TV _ => TyFunApp_nil)
 138                         | _   => Error "WTyFunApp not applied to enough types"
 139                       end
 140           | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
 141                         match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 142                           | nil    => Error "WTyFunApp applied to too many types"
 143                           | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
 144                                         let case_weakTypeListToTypeList := tt in _
 145                         end
 146         end
 147       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
 148   end ); clear weakTypeToType.
 149
 150   destruct case_WTyVarTy.
 151     apply OK.
 152     exact (haskTypeOfSomeKind (fun TV env => TVar (φ v TV env))).
 153
 154   destruct case_WAppTy.
 155     destruct t1' as  [k1' t1'].
 156     destruct t2' as [k2' t2'].
 157     destruct k1';
 158       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
 159         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
 160       apply (Error "Kind mismatch in WAppTy:: ").
 161
 162   destruct case_weakTypeListToTypeList.
 163     destruct t' as [ k' t' ].
 164     matchThings k k' "Kind mismatch in weakTypeListToTypeList".
 165     subst.
 166     apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
 167
 168   destruct case_WTyFunApp.
 169     apply OK.
 170     eapply haskTypeOfSomeKind.
 171     unfold HaskType; intros.
 172     apply TyFunApp.
 173     apply lt'.
 174     apply X.
 175
 176   destruct case_WTyCon.
 177     apply OK.
 178     eapply haskTypeOfSomeKind.
 179     unfold HaskType; intros.
 180     apply (TCon tc).
 181
 182   destruct case_WCodeTy.
 183     destruct tbody'.
 184     matchThings κ ★ "Kind mismatch in WCodeTy: ".
 185     apply OK.
 186     eapply haskTypeOfSomeKind.
 187     unfold HaskType; intros.
 188     apply TCode.
 189     apply (TVar (φ (@fixkind ★ ec) TV X)).
 190     subst.
 191     apply h.
 192     apply X.
 193
 194   destruct case_WCoFunTy.
 195     destruct t1' as [ k1' t1' ].
 196     destruct t2' as [ k2' t2' ].
 197     destruct t3' as [ k3' t3' ].
 198     matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
 199     subst.
 200     matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
 201     subst.
 202     apply OK.
 203     apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
 204
 205   destruct case_WForAllTy.
 206     destruct t1.
 207     matchThings ★  κ "Kind mismatch in WForAllTy: ".
 208     subst.
 209     apply OK.
 210     apply (@haskTypeOfSomeKind _ ★).
 211     apply (@mkTAll wtv).
 212     apply h.
 213     Defined.
 214
 215
 216
 217 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 218 Section StrongAltCon.
 219   Context (tc : TyCon)(dc:DataCon tc).
 220 (*
 221 Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ).
 222   intro avars.
 223   intro ct.
 224   set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
 225   set (@substφ _ _ avars') as q.
 226   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.
 227   set (@weakTypeToType _ φ' ct) as t.
 228   set (@weakT'' _ Γ t) as t'.
 229   set (@lamer _ _ _ t') as t''.
 230   fold (tyConKinds tc) in t''.
 231   fold (dataConExKinds dc) in t''.
 232   apply (q (tyConKinds tc)).
 233   unfold tyConKinds.
 234   unfold dataConExKinds.
 235   rewrite <- vec2list_map_list2vec.
 236   rewrite <- vec2list_map_list2vec.
 237   rewrite vec2list_list2vec.
 238   rewrite vec2list_list2vec.
 239   apply t''.
 240   Defined.
 241
 242 Definition mkStrongAltCon : @StrongAltCon tc.
 243   refine
 244    {| sac_altcon      := DataAlt dc
 245     ; sac_numCoerVars := length (dataConCoerKinds dc)
 246     ; sac_numExprVars := length (dataConFieldTypes dc)
 247     ; sac_akinds      := tyConKinds tc
 248     ; sac_ekinds      := dataConExKinds dc
 249     ; sac_coercions   := fun Γ avars => let case_sac_coercions := tt in _
 250     ; sac_types       := fun Γ avars => let case_sac_types := tt in _
 251     |}.
 252
 253   destruct case_sac_coercions.
 254     refine (vec_map _ (list2vec (dataConCoerKinds dc))).
 255     intro.
 256     destruct X.
 257     apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
 258
 259   destruct case_sac_types.
 260     refine (vec_map _ (list2vec (dataConFieldTypes dc))).
 261     intro X.
 262     apply (weakTypeToType' avars).
 263     apply X.
 264     Defined.
 265
 266 Lemma weakCV' : forall {Γ}{Δ} Γ',
 267    HaskCoVar Γ Δ
 268    -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
 269   intros.
 270   unfold HaskCoVar in *.
 271   intros; apply (X TV CV).
 272   apply vec_chop' in env; auto.
 273   unfold InstantiatedCoercionEnv in *.
 274   unfold weakCK'' in cenv.
 275   destruct Γ'.
 276   apply cenv.
 277   rewrite <- map_preserves_length in cenv.
 278   apply cenv.
 279   Defined.
 280
 281 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
 282     refine
 283      {| sacpj_sac     := mkStrongAltCon
 284       ; sacpj_φ       := fun Γ φ => (fun htv => weakV' (φ htv))
 285       ; sacpj_ψ       := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
 286       |}.
 287     intro.
 288     unfold sac_Γ.
 289     unfold HaskCoVar in *.
 290     intros.
 291     apply (x TV CV env).
 292     simpl in cenv.
 293     unfold sac_Δ in *.
 294     unfold InstantiatedCoercionEnv in *.
 295     apply vec_chop' in cenv.
 296     apply cenv.
 297     Defined.
 298 *)
 299 End StrongAltCon.
 300 (*
 301 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
 302   destruct alt.
 303   set (c:DataCon _) as dc.
 304   set ((dataConTyCon c):TyCon) as tc' in *.
 305   set (eqd_dec tc tc') as eqpf; destruct eqpf;
 306     [ idtac
 307       | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++dc)) ]; subst.
 308   apply OK.
 309   eapply mkStrongAltConPlusJunk.
 310   simpl in *.
 311   apply dc.
 312
 313   apply OK; refine {| sacpj_sac := {| sac_akinds  := tyConKinds tc
 314                     ; sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 315                     ; sac_altcon := LitAlt h
 316                     |} |}.
 317             intro; intro φ; apply φ.
 318             intro; intro; intro; intro ψ; apply ψ.
 319   apply OK; refine {| sacpj_sac := {| sac_akinds  := tyConKinds tc
 320                     ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 321                       ; sac_altcon := DEFAULT |} |}.
 322             intro; intro φ; apply φ.
 323             intro; intro; intro; intro ψ; apply ψ.
 324 Defined.
 325 Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ ★) :=
 326   match mlr with
 327   | T_Leaf None                         => []
 328   | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
 329   | T_Branch b1 b2                      => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ))
 330   end.
 331 *)
 332
 333
 334 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
 335   fun wev => match wev with weakExprVar _ t => t end.
 336   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 337
 338 (*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*)
 339
 340 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
 341   WeakCoerVar -> HaskCoVar Γ (κ::Δ).
 342   intros.
 343   unfold HaskCoVar.
 344   intros.
 345   apply (ψ X TV CV env).
 346   inversion cenv; auto.
 347   Defined.
 348
 349 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
 350 Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ)
 351   : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ').
 352   intros.
 353   destruct τ  as [τ  l].
 354   destruct τ' as [τ' l'].
 355   destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ].
 356   destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ].
 357   subst.
 358   apply OK.
 359   apply e.
 360   Defined.
 361
 362 Definition weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
 363   intros.
 364   set (weakTypeToType φ t) as wt.
 365   destruct wt; try apply (Error error_message).
 366   destruct h.
 367   matchThings κ κ0 "Kind mismatch in weakTypeToType': ".
 368   subst.
 369   apply OK.
 370   apply h.
 371   Defined.
 372
 373 Definition weakExprToStrongExpr : forall
 374     (Γ:TypeEnv)
 375     (Δ:CoercionEnv Γ)
 376     (φ:TyVarResolver Γ)
 377     (ψ:CoVarResolver Γ Δ)
 378     (ξ:WeakExprVar -> LeveledHaskType Γ ★)
 379     (τ:HaskType Γ ★)
 380     (lev:HaskLevel Γ),
 381     WeakExpr -> ???(Expr Γ Δ ξ (τ @@ lev) ).
 382   refine ((
 383     fix weakExprToStrongExpr
 384     (Γ:TypeEnv)
 385     (Δ:CoercionEnv Γ)
 386     (φ:TyVarResolver Γ)
 387     (ψ:CoVarResolver Γ Δ)
 388     (ξ:WeakExprVar -> LeveledHaskType Γ ★)
 389     (τ:HaskType Γ ★)
 390     (lev:HaskLevel Γ)
 391     (we:WeakExpr) : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
 392     match we with
 393
 394     | WEVar   v                         => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v)
 395
 396     | WELit   lit                       => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev)
 397
 398     | WELam   ev e                      => weakTypeToType' φ ev ★ >>= fun tv =>
 399                                              weakTypeOfWeakExpr e >>= fun t =>
 400                                                weakTypeToType' φ t ★ >>= fun τ' =>
 401                                                  weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((ev,tv@@lev)::nil)) τ' _ e >>= fun e' =>
 402                                                    castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
 403
 404     | WEBrak  ec e tbody                => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
 405                                              castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
 406
 407     | WEEsc   ec e tbody                => weakTypeToType' φ tbody ★ >>= fun tbody' =>
 408                                            match lev with
 409                                              | nil       => Error "ill-leveled escapification"
 410                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e
 411                                                >>= fun e' =>
 412                                                               castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e')
 413                                            end
 414     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 415
 416     | WELet   v ve  ebody               => weakTypeToType' φ v ★  >>= fun tv =>
 417                                              weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 418                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((v,tv@@lev)::nil)) τ lev ebody
 419                                                >>= fun ebody' =>
 420                                                  OK (ELet _ _ _ tv _ lev v ve' ebody')
 421
 422     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 423                                              weakTypeToType' φ t2 ★ >>= fun t2' =>
 424                                                weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
 425                                                  weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
 426                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 427
 428     | WETyLam tv e                      => let φ' := upφ tv φ in
 429                                              weakTypeOfWeakExpr e >>= fun te =>
 430                                                weakTypeToType' φ' te ★ >>= fun τ' =>
 431                                                  weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e
 432                                                  >>= fun e' =>
 433                                                    castExpr "WETyLam1" _ e' >>= fun e'' =>
 434                                                      castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
 435
 436     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 437                                            match te with
 438                                              | WForAllTy wtv te' =>
 439                                                let φ' := upφ wtv φ in
 440                                                  weakTypeToType' φ' te' ★ >>= fun te'' =>
 441                                                    weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
 442                                                      weakTypeToType' φ t wtv >>= fun t' =>
 443                                                        castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 444                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
 445                                            end
 446
 447     (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two
 448      * to get them back working again *)
 449     | WECoApp e t                       => Error "weakExprToStrongExpr: WECoApp  not yet implemented"
 450     | WECoLam cv e                      => Error "weakExprToStrongExpr: WECoLam  not yet implemented"
 451     | WECast  e co                      => Error "weakExprToStrongExpr: WECast   not yet implemented"
 452     | WELetRec rb   e                   => Error "weakExprToStrongExpr: WELetRec not yet implemented"
 453     | WECase  e tbranches tc avars alts => Error "weakExprToStrongExpr: WECase   not yet implemented"
 454     end)).
 455     Defined.
 456