Require Import General.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
-Require Import HaskGeneral.
+Require Import HaskKinds.
Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Require Import HaskWeakVars.
+Require Import HaskWeakTypes.
Require Import HaskWeak.
+Require Import HaskCoreToWeak.
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).
- Extract Inlined Constant mkCoreLet => "sortAlts".
+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 unsafeCoerce : CoreCoercion.
- Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
-
-(* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *)
-Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
- Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
-
-(* a dummy variable which is never referenced but needed for a binder *)
-Variable dummyVariable : CoreVar.
-
-Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
-match wv with
-| WExprVar (weakExprVar v _ ) => v
-| WTypeVar (weakTypeVar v _ ) => v
-| WCoerVar (weakCoerVar v _ _ ) => v
-end.
-
-Section HaskWeakToCore.
+Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
+ match wa with
+ | WeakDataAlt cdc => DataAlt cdc
+ | WeakLitAlt lit => LitAlt lit
+ | WeakDEFAULT => DEFAULT
+ end.
- (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
- Context (hetmet_brak_var : CoreVar).
- Context (hetmet_esc_var : CoreVar).
+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 : WeakCoercion -> CoreCoercion :=
- fun _ => unsafeCoerce.
+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+ CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
- Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
+Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
match me with
| WEVar (weakExprVar v _) => CoreEVar v
| WELit lit => CoreELit lit
| WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
- | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType t)
- | WECoApp e co => CoreEApp (weakExprToCoreExpr e )
- (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
+ | 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 )
+ | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e )
| WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
- | WEBrak (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var) (CoreEType (TyVarTy ec))) (CoreEType t)
- | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var) (CoreEType (TyVarTy ec))) (CoreEType t)
+ | 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 e tbranches n tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable tbranches
+ | WECase vscrut escrut tbranches tc types alts =>
+ CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
(sortAlts ((
- fix mkCaseBranches (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) :=
+ fix mkCaseBranches (alts:Tree
+ ??(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,lwv,e)) =>
- (mkTriple ac (map weakVarToCoreVar lwv) (weakExprToCoreExpr e))::nil
+ | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
+ (mkTriple (weakAltConToCoreAltCon ac)
+ (app (app
+ (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
+ (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
+ (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
+ (weakExprToCoreExpr e))::nil
end
) alts))
| WELetRec mlr e => CoreELet (CoreRec
(weakExprToCoreExpr e)
end.
-End HaskWeakToCore.
\ No newline at end of file
+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+ coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
+
+Instance weakExprToString : ToString WeakExpr :=
+ { toString := fun we => toString (weakExprToCoreExpr we) }.
+
+