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".
+ Extract Inlined Constant sortAlts => "sortAlts".
Implicit Arguments sortAlts [[a][b]].
Variable trustMeCoercion : CoreCoercion.
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.
- (* FIXME this doesn't actually work *)
- Extract Inlined Constant dummyVariable => "(Prelude.error ""dummyVariable"")".
+Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
+ fun _ => trustMeCoercion.
-Section HaskWeakToCore.
-
- (* 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).
-
- (* FIXME: do something more intelligent here *)
- Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
- fun _ => trustMeCoercion.
Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
match me with
| 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 (weakTypeToCoreType t))
- | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var)
- (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType 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)
| WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
- | WECase e tbranches tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable (weakTypeToCoreType tbranches)
+ | WECase vscrut e tbranches tc types alts =>
+ CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
(sortAlts ((
fix mkCaseBranches (alts:Tree
??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
(weakExprToCoreExpr e)
end.
-End HaskWeakToCore.
+
+Instance weakExprToString : ToString WeakExpr :=
+ { toString := fun we => toString (weakExprToCoreExpr we) }.