Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
-Variable sortAlts : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b).
+Variable sortAlts : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b).
Extract Inlined Constant sortAlts => "sortAlts".
Implicit Arguments sortAlts [[a][b]].
Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
+Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
+ match wa with
+ | WeakDataAlt cdc => DataAlt cdc
+ | WeakLitAlt lit => LitAlt lit
+ | WeakDEFAULT => DEFAULT
+ end.
+
+Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
+ match wt with
+ | WTyVarTy (weakTypeVar v _) => TyVarTy v
+ | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
+ | WAppTy t1 t2 => match (weakTypeToCoreType t1) with
+ | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
+ | t1' => AppTy t1' (weakTypeToCoreType t2)
+ end
+ | WTyCon tc => TyConApp tc nil
+ | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt)
+ | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt))
+ | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty))
+ | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
+ | WFunTyCon => TyConApp ArrowTyCon nil
+ | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
+ | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
+ (weakTypeToCoreType t3)
+ end.
+
Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
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
- ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+ ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match alts with
| T_Leaf None => nil
| T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2)
| T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
- (mkTriple (ac:AltCon)
+ (mkTriple (weakAltConToCoreAltCon ac)
(app (app
(map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
(map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
Instance weakExprToString : ToString WeakExpr :=
{ toString := fun we => toString (weakExprToCoreExpr we) }.
+