From 693c6f552555f14c085a71e0b03c67d3c051eaa1 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Wed, 16 Mar 2011 01:50:06 -0700 Subject: [PATCH] add crude Monad type class --- src/General.v | 8 ++++++++ src/HaskCoreToWeak.v | 3 +-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/General.v b/src/General.v index 3c82528..7e0af43 100644 --- a/src/General.v +++ b/src/General.v @@ -633,6 +633,12 @@ Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))). Variable eol : string. Extract Constant eol => "'\n':[]". +Class Monad {T:Type->Type} := +{ returnM : forall {a}, a -> T a +; bindM : forall {a}{b}, T a -> (a -> T b) -> T b +}. +Implicit Arguments Monad [ ]. +Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity). (* the Error monad *) Inductive OrError (T:Type) := @@ -709,3 +715,5 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???( rewrite e in v; apply OK; apply v. apply (Error (error_message (length l) n)). Defined. + + diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index c4bd768..055d588 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -218,9 +218,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | WCoerVar _ => Error "found a coercion variable in a case" | WExprVar ev => coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' => - coreExprToWeakExpr e >>= fun e' => expectTyConApp te' nil >>= fun tca => - let (tc,lt) := tca in + let (tc,lt) := tca:(TyCon * list WeakType) in ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar))) : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := match branches with -- 1.7.10.4