Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Coq.Lists.List.
+Require Import General.
Require Import HaskKinds.
Require Import HaskLiteralsAndTyCons.
Require Import HaskCoreVars.
Require Import HaskWeakTypes.
Require Import HaskWeak.
-Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
-
Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
| WCoerVar _ => Error "found a coercion variable in a case"
| WExprVar ev =>
coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
- coreExprToWeakExpr e >>= fun e' =>
expectTyConApp te' nil >>= fun tca =>
- let (tc,lt) := tca in
+ let (tc,lt) := tca:(TyCon * list WeakType) in
((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
: ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match branches with
| LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
| DataAlt dc => let vars := map coreVarToWeakVar vars in
OK (((WeakDataAlt dc),
- (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
- (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
- (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
+ (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
+ (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
+ (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
e')::rest')
end
end) alts)