From 53d4f1ce851b924cab5dc39419179a366001cbca Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 16:46:56 -0700 Subject: [PATCH] more formatting fixes --- src/HaskCore.v | 13 +------------ src/HaskCoreLiterals.v | 2 +- src/HaskCoreToWeak.v | 28 +++++++++++++++------------- 3 files changed, 17 insertions(+), 26 deletions(-) diff --git a/src/HaskCore.v b/src/HaskCore.v index 244139a..abd1428 100644 --- a/src/HaskCore.v +++ b/src/HaskCore.v @@ -39,16 +39,5 @@ Extract Inductive CoreExpr => Extract Inductive CoreBind => "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ]. -(* extracts the Name from a CoreVar *) -Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". - -(* the magic wired-in name for the modal type introduction form *) -Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name". - -(* the magic wired-in name for the modal type elimination form *) -Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name". - Variable coreExprToString : @CoreExpr CoreVar -> string. Extract Inlined Constant coreExprToString => "outputableToString". - -Instance CoreExprToString : ToString (@CoreExpr CoreVar) := - { toString := coreExprToString }. \ No newline at end of file +Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }. \ No newline at end of file diff --git a/src/HaskCoreLiterals.v b/src/HaskCoreLiterals.v index 24432ee..05cace2 100644 --- a/src/HaskCoreLiterals.v +++ b/src/HaskCoreLiterals.v @@ -44,7 +44,7 @@ Extract Inductive HaskLiteral => "Literal.Literal" Extract Inductive HaskFunctionOrData => "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ]. -Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString". +Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString". Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }. (* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *) diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 63c7e95..d47ab0c 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -15,8 +15,19 @@ Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. -Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon). -Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". +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". + +(* extracts the Name from a CoreVar *) +Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". + +(* the magic wired-in name for the modal type introduction form *) +Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name". + +(* the magic wired-in name for the modal type elimination form *) +Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name". Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := match ct with @@ -71,8 +82,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | PredTy (EqPred _ _) => Error "hit a bare EqPred" end. -Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". -Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t). +Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)). (* detects our crude Core-encoding of modal type introduction/elimination forms *) Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) := @@ -86,6 +96,7 @@ match ce with end else None | _ => None end. + Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) := match ce with | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) @@ -98,15 +109,6 @@ match ce with | _ => None end. -Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion. - Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion". -(* - let (t1,t2) := coreCoercionKind cc - in coreTypeToWeakType t1 >>= fun t1' => - coreTypeToWeakType t2 >>= fun t2' => - OK (WCoUnsafe t1' t2'). -*) - (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *) Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) := match wt with -- 1.7.10.4