Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
-Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
-
Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
match wa with
| WeakDataAlt cdc => DataAlt cdc
| 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 )
+ | 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))::
nil)
(CoreEVar v)
| WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
- | WECase vscrut e tbranches tc types alts =>
- CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
+ | WECase vscrut escrut tbranches tc types alts =>
+ CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
(sortAlts ((
fix mkCaseBranches (alts:Tree
??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=