Require Import General.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
-Require Import HaskGeneral.
-Require Import HaskLiterals.
+Require Import HaskKinds.
+Require Import HaskCoreLiterals.
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".
Extract Inlined Constant mkCoreLet => "sortAlts".
Implicit Arguments sortAlts [[a][b]].
-Variable unsafeCoerce : CoreCoercion.
- Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
+Variable trustMeCoercion : CoreCoercion.
+ Extract Inlined Constant trustMeCoercion => "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.
(* 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.
-Coercion weakVarToCoreVar : WeakVar >-> CoreVar.
+ (* FIXME this doesn't actually work *)
+ Extract Inlined Constant dummyVariable => "(Prelude.error ""dummyVariable"")".
Section HaskWeakToCore.
Context (hetmet_brak_var : CoreVar).
Context (hetmet_esc_var : CoreVar).
+ (* FIXME: do something more intelligent here *)
Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
- fun _ => unsafeCoerce.
+ fun _ => trustMeCoercion.
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)
+ | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
| WECoApp e co => CoreEApp (weakExprToCoreExpr e )
(CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
| WENote n e => CoreENote n (weakExprToCoreExpr e )
| WETyLam (weakTypeVar tv _ ) e => CoreELam tv (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 (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var)
+ (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
+ | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var)
+ (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
| 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 e tbranches tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable (weakTypeToCoreType tbranches)
(sortAlts ((
fix mkCaseBranches (alts:Tree
??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
| T_Leaf None => nil
| T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2)
| T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
- (mkTriple ac
+ (mkTriple (ac:AltCon)
(app (app
(map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
(map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
end.
End HaskWeakToCore.
+
+