- | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2)
- | WETyApp e t => CoreEApp (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t))
- | WECoApp e co => CoreEApp (weakExprToCoreExpr f e )
- (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
- | WENote n e => CoreENote n (weakExprToCoreExpr f e )
- | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr f e )
- | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr f e )
- | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr f e )
- | WECast e co => CoreECast (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co)
- | WEBrak (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var)
- (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
- | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var)
- (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
- | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr f ve)) (weakExprToCoreExpr f e)
- | WECase e tbranches tc types alts => let (v,f') := next _ _ f tt in
- CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches)
+ | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
+ | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
+ | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) (CoreECoercion (weakCoercionToCoreCoercion co))
+ | WENote n e => CoreENote n (weakExprToCoreExpr e )
+ | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e )
+ | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e )
+ | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e )
+ | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
+ | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp
+ ((CoreEType (TyVarTy ec))::
+ (CoreEType (weakTypeToCoreType t))::
+ (weakExprToCoreExpr e)::
+ nil)
+ (CoreEVar v)
+ | WEEsc v (weakTypeVar ec _) e t => fold_left CoreEApp
+ ((CoreEType (TyVarTy ec))::
+ (CoreEType (weakTypeToCoreType t))::
+ (weakExprToCoreExpr e)::
+ nil)
+ (CoreEVar v)
+ | WECSP v (weakTypeVar ec _) e t => fold_left CoreEApp
+ ((CoreEType (TyVarTy ec))::
+ (CoreEType (weakTypeToCoreType t))::
+ (weakExprToCoreExpr e)::
+ nil)
+ (CoreEVar v)
+ | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
+ | WECase vscrut escrut tbranches tc types alts =>
+ CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)