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.
| WExprVar _ => Error "encountered expression variable in a modal box type"
| WCoerVar _ => Error "encountered coercion variable in a modal box type"
end
- | _ => Error ("mis-applied modal box tycon: " +++ ct)
+ | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
end
else let tc' := if eqd_dec tc ArrowTyCon
then WFunTyCon
match wt with
| WTyCon tc => OK (tc,acc)
| WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
- | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
- | _ => Error ("expectTyConApp encountered " +++ wt)
+ | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
+ | _ => Error ("expectTyConApp encountered " +++ toString wt)
end.
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
| 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)