From: Adam Megacz Date: Mon, 30 May 2011 22:22:17 +0000 (-0700) Subject: better error reporting in coreTypeToWeakType; dont use Prelude_error X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=4c5c94487aa2bf5489371f112607f0a4c4f01a94 better error reporting in coreTypeToWeakType; dont use Prelude_error --- diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index f11e63b..7fb0160 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -50,19 +50,12 @@ cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x -coreVarToWeakVar :: Var.Var -> WeakVar -coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v)))) -coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v))) -coreVarToWeakVar v | Var.isCoVar v - = WCoerVar (WeakCoerVar v - (errOrFail (coreTypeToWeakType (Prelude.fst (Coercion.coercionKind (Var.varType v))))) - (errOrFail (coreTypeToWeakType (Prelude.snd (Coercion.coercionKind (Var.varType v)))))) -coreVarToWeakVar _ = - Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" - -errOrFail :: OrError t -> t -errOrFail (OK x) = x -errOrFail (Error s) = Prelude.error s +coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult +coreVarToWeakVar v | Id.isId v = CVTWVR_EVar (Var.varType v) +coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v)) +coreVarToWeakVar v | Var.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coercionKind (Var.varType v))) + (Prelude.snd (Coercion.coercionKind (Var.varType v))) +coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!" rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind ) rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk)) @@ -141,11 +134,9 @@ coreViewDeep t = Prelude.Nothing -> TypeRep.PredTy p Prelude.Just t' -> t' -coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion -coreCoercionToWeakCoercion c = - WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2)) - where - (t1,t2) = Coercion.coercionKind c +getSourceAndTargetTypesOfCoercion :: Type.Type -> (Type.Type,Type.Type) +getSourceAndTargetTypesOfCoercion c = Coercion.coercionKind (Coercion.typeKind c) + {- -- REMEMBER: cotycon applications may be oversaturated case c of diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 4926bff..2e51d0e 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -92,14 +92,15 @@ Section core2proof. (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no * free tyvars in them *) Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ := - match coreVarToWeakVar cv with - | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with + match coreVarToWeakVar' cv with + | OK (WExprVar wev) => match weakTypeToTypeOfKind φ wev ★ with | Error s => Prelude_error ("Error converting weakType of top-level variable "+++ toString cv+++": " +++ s) | OK t => t @@ nil end - | WTypeVar _ => Prelude_error "top-level xi got a type variable" - | WCoerVar _ => Prelude_error "top-level xi got a coercion variable" + | OK (WTypeVar _) => Prelude_error "top-level xi got a type variable" + | OK (WCoerVar _) => Prelude_error "top-level xi got a coercion variable" + | Error s => Prelude_error s end. Definition header : string := @@ -228,8 +229,9 @@ Section core2proof. End CoreToCore. Definition coreVarToWeakExprVarOrError cv := - match coreVarToWeakVar cv with - | WExprVar wv => wv + match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with + | OK (WExprVar wv) => wv + | Error s => Prelude_error s | _ => Prelude_error "IMPOSSIBLE" end. diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index ccd4973..673b999 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -18,8 +18,8 @@ Require Import HaskWeak. Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". -Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion. - Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion". +Variable getSourceAndTargetTypesOfCoercion : CoreCoercion -> (CoreType * CoreType). + Extract Inlined Constant getSourceAndTargetTypesOfCoercion => "getSourceAndTargetTypesOfCoercion". (* extracts the Name from a CoreVar *) Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". @@ -35,12 +35,16 @@ Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType := let (args,rest) := argsrest in OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)). +(* a hack to evade the guardedness check of Fixpoint *) +Variable coreTypeToWeakTypeCheat' : CoreType -> ???WeakType. +Extract Inlined Constant coreTypeToWeakTypeCheat' => "coreTypeToWeakType'". + Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := match ct with | TyVarTy cv => match coreVarToWeakVar cv with - | WExprVar _ => Error "encountered expression variable in a type" - | WTypeVar tv => OK (WTyVarTy tv) - | WCoerVar _ => Error "encountered coercion variable in a type" + | CVTWVR_EVar ct => Error "encountered expression variable in a type" + | CVTWVR_TyVar k => OK (WTyVarTy (weakTypeVar cv k)) + | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a type" end | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2') @@ -56,11 +60,12 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := then match lct with | ((TyVarTy ec)::tbody::nil) => match coreVarToWeakVar ec with - | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody') - | WExprVar _ => Error "encountered expression variable in a modal box type" - | WCoerVar _ => Error "encountered coercion variable in a modal box type" + | CVTWVR_EVar ct => Error "encountered expression variable in a modal box type" + | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a modal box type" + | CVTWVR_TyVar k => coreTypeToWeakType' tbody >>= fun tbody' => + OK (WCodeTy (weakTypeVar ec k) tbody') end - | _ => Error ("mis-applied modal box tycon: " +++ toString ct) + | _ => Error ("mis-applied modal box tycon: " +++ toString ct) end else let tc' := if eqd_dec tc ArrowTyCon then WFunTyCon @@ -75,11 +80,12 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := coreTypeToWeakType' t2 >>= fun t2' => OK (WAppTy (WAppTy WFunTyCon t1') t2') | ForAllTy cv t => match coreVarToWeakVar cv with - | WExprVar _ => Error "encountered expression variable in a type abstraction" - | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t') - | WCoerVar (weakCoerVar v t1' t2') => - coreTypeToWeakType' t >>= fun t3' => - OK (WCoFunTy t1' t2' t3') + | CVTWVR_EVar ct => Error "encountered expression variable in a type abstraction" + | CVTWVR_TyVar k => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy (weakTypeVar cv k) t') + | CVTWVR_CoVar t1 t2 => coreTypeToWeakTypeCheat' t1 >>= fun t1' => + coreTypeToWeakTypeCheat' t2 >>= fun t2' => + coreTypeToWeakType' t >>= fun t3' => + OK (WCoFunTy t1' t2' t3') end | PredTy (ClassP cl lct) => ((fix rec tl := match tl with | nil => OK nil @@ -93,18 +99,35 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := Definition coreTypeToWeakType t := addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)). +Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar := + addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol) + match coreVarToWeakVar cv with + | CVTWVR_EVar ct => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t')) + | CVTWVR_TyVar k => OK (WTypeVar (weakTypeVar cv k)) + | CVTWVR_CoVar t1 t2 => + (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *) + addErrorMessage ("with t2=" +++ toString t2 +++ eol) + ((coreTypeToWeakType t2) >>= fun t2' => + addErrorMessage ("with t1=" +++ toString t1 +++ eol) + (coreTypeToWeakType t1) >>= fun t1' => + OK (WCoerVar (weakCoerVar cv t1' t2'))) + end. +Definition tyConTyVars (tc:CoreTyCon) := + filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)). + Opaque tyConTyVars. +Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc). + (* detects our crude Core-encoding of modal type introduction/elimination forms *) Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) := match ce with | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) => if coreName_eq hetmet_brak_name (coreVarCoreName v) then - match coreVarToWeakVar ec with - | WExprVar _ => None - | WCoerVar _ => None - | WTypeVar tv => match coreVarToWeakVar v with - | WExprVar v' => Some (v',tv,tbody) + match coreVarToWeakVar' ec with + | OK (WTypeVar tv) => match coreVarToWeakVar' v with + | OK (WExprVar v') => Some (v',tv,tbody) | _ => None end + | _ => None end else None | _ => None end. @@ -113,13 +136,12 @@ Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreTyp match ce with | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) => if coreName_eq hetmet_esc_name (coreVarCoreName v) then - match coreVarToWeakVar ec with - | WExprVar _ => None - | WTypeVar tv => match coreVarToWeakVar v with - | WExprVar v' => Some (v',tv,tbody) + match coreVarToWeakVar' ec with + | OK (WTypeVar tv) => match coreVarToWeakVar' v with + | OK (WExprVar v') => Some (v',tv,tbody) | _ => None end - | WCoerVar _ => None + | _ => None end else None | _ => None end. @@ -128,13 +150,12 @@ Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreTyp match ce with | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) => if coreName_eq hetmet_csp_name (coreVarCoreName v) then - match coreVarToWeakVar ec with - | WExprVar _ => None - | WTypeVar tv => match coreVarToWeakVar v with - | WExprVar v' => Some (v',tv,tbody) + match coreVarToWeakVar' ec with + | OK (WTypeVar tv) => match coreVarToWeakVar' v with + | OK (WExprVar v') => Some (v',tv,tbody) | _ => None end - | WCoerVar _ => None + | _ => None end else None | _ => None end. @@ -148,15 +169,32 @@ Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak | _ => Error ("expectTyConApp encountered " +++ toString wt) end. +(* expects to see an EType with a coercion payload *) +Definition coreExprToWeakCoercion t1 t2 (ce:@CoreExpr CoreVar) : ???WeakCoercion := + match ce with + | CoreEType t => (*OK (coreCoercionToWeakCoercion t)*) OK (WCoUnsafe t1 t2) + | _ => Error ("coreExprToWeakCoercion got a " +++ toString ce) + end. + +(* expects to see an EType *) +Definition coreExprToWeakType (ce:@CoreExpr CoreVar) : ???WeakType := + match ce with + | CoreEType t => coreTypeToWeakType t + | _ => Error ("coreExprToWeakType got a " +++ toString ce) + end. + Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match ce with | CoreELit lit => OK (WELit lit) | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e') | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been" | CoreECast e co => coreExprToWeakExpr e >>= fun e' => - OK (WECast e' (coreCoercionToWeakCoercion co)) + let (ct1,ct2) := getSourceAndTargetTypesOfCoercion co + in coreTypeToWeakType ct1 >>= fun t1 => + coreTypeToWeakType ct2 >>= fun t2 => + OK (WECast e' (WCoUnsafe t1 t2)) - | CoreEVar v => match coreVarToWeakVar v with + | CoreEVar v => coreVarToWeakVar' v >>= fun v' => match v' with | WExprVar ev => OK (WEVar ev) | WTypeVar _ => Error "found a type variable inside an EVar!" | WCoerVar _ => Error "found a coercion variable inside an EVar!" @@ -189,20 +227,25 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := end end - | CoreELam v e => match coreVarToWeakVar v with + | CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e') | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e') | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e') end - | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with + | CoreELet (CoreNonRec v ve) e => coreVarToWeakVar' v >>= fun v' => match v' with | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' => coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e') - | WTypeVar _ => match e with - | CoreEType t => Error "saw a type-let" + | WTypeVar tv => match e with + | CoreEType t => coreExprToWeakExpr e >>= fun e' => + coreExprToWeakType ve >>= fun ty' => + OK (WETyApp (WETyLam tv e') ty') | _ => Error "saw (ELet e) where e!=EType" end - | WCoerVar _ => Error "saw an (ELet )" + | WCoerVar (weakCoerVar cv t1 t2) => + coreExprToWeakExpr e >>= fun e' => + coreExprToWeakCoercion t1 t2 ve >>= fun co' => + OK (WECoApp (WECoLam (weakCoerVar cv t1 t2) e') co') end | CoreELet (CoreRec rb) e => @@ -210,7 +253,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match cel with | nil => OK nil | (v',e')::t => coreExprToWeakExprList t >>= fun t' => - match coreVarToWeakVar v' with + coreVarToWeakVar' v' >>= fun v'' => match v'' with | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t') | WTypeVar _ => Error "found a type variable in a recursive let" | WCoerVar _ => Error "found a coercion variable in a recursive let" @@ -220,7 +263,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := OK (WELetRec (unleaves' rb') e') | CoreECase e v tbranches alts => - match coreVarToWeakVar v with + coreVarToWeakVar' v >>= fun v' => match v' with | WTypeVar _ => Error "found a type variable in a case" | WCoerVar _ => Error "found a coercion variable in a case" | WExprVar ev => @@ -237,11 +280,11 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match alt with | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest') | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest') - | DataAlt dc => let vars := map coreVarToWeakVar vars in + | DataAlt dc => let vars := map coreVarToWeakVar' vars in OK (((WeakDataAlt dc), - (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)), - (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)), - (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)), + (filter (map (fun x => match x with OK (WTypeVar v) => Some v | _ => None end) vars)), + (filter (map (fun x => match x with OK (WCoerVar v) => Some v | _ => None end) vars)), + (filter (map (fun x => match x with OK (WExprVar v) => Some v | _ => None end) vars)), e')::rest') end end) alts) @@ -251,7 +294,3 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := OK (WECase ev scrutinee tbranches' tc lt (unleaves branches)) end end. - - - - diff --git a/src/HaskStrong.v b/src/HaskStrong.v index bf51e1a..874b368 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -13,6 +13,7 @@ Require Import HaskLiterals. Require Import HaskTyCons. Require Import HaskStrongTypes. Require Import HaskWeakVars. +Require Import HaskCoreToWeak. Require Import HaskCoreVars. Section HaskStrong. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 24f349b..60e84b6 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -23,7 +23,7 @@ Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Const Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys". Definition dataConExTyVars cdc := - filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)). + filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)). Opaque dataConExTyVars. Definition dataConCoerKinds cdc := filter (map (fun x => match x with EqPred t1 t2 => diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 156c2ce..d8dcf42 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -19,6 +19,7 @@ Require Import HaskWeakToCore. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreVars. +Require Import HaskCoreToWeak. Require Import HaskCoreTypes. Open Scope string_scope. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 3fb7a4b..e7ab943 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -14,6 +14,11 @@ Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskWeakTypes. +Inductive CoreVarToWeakVarResult : Type := +| CVTWVR_EVar : CoreType -> CoreVarToWeakVarResult +| CVTWVR_TyVar : Kind -> CoreVarToWeakVarResult +| CVTWVR_CoVar : CoreType -> CoreType -> CoreVarToWeakVarResult. + (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *) Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar. @@ -42,12 +47,8 @@ Definition haskLiteralToWeakType lit : WeakType := WTyCon (haskLiteralToTyCon lit). Coercion haskLiteralToWeakType : HaskLiteral >-> WeakType. -Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". -Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars". -Definition tyConTyVars (tc:CoreTyCon) := - filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)). - Opaque tyConTyVars. -Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc). +Variable coreVarToWeakVar : CoreVar -> CoreVarToWeakVarResult. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". +Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars". Variable rawTyFunKind : CoreTyCon -> ((list Kind) * Kind). Extract Inlined Constant rawTyFunKind => "rawTyFunKind".