From 2ec43bc871b579bac89707988c4855ee1d6c8eda Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 17:40:24 -0700 Subject: [PATCH] reshuffle definitions in an attempt to iron out inter-file dependenceies --- src/Extraction.v | 2 +- src/HaskCore.v | 9 ++-- src/HaskCoreToWeak.v | 36 ++++++++++----- src/HaskCoreTypes.v | 20 +++----- src/HaskCoreVars.v | 16 +++++++ ...{HaskCoreLiterals.v => HaskLiteralsAndTyCons.v} | 32 +++++++------ src/HaskProof.v | 2 +- src/HaskProofToLatex.v | 2 +- src/HaskStrong.v | 4 +- src/HaskStrongToProof.v | 14 ------ src/HaskStrongToWeak.v | 14 +++--- src/HaskStrongTypes.v | 6 +-- src/HaskWeak.v | 21 ++++----- src/HaskWeakToCore.v | 38 ++++++++++++++-- src/HaskWeakToStrong.v | 13 +++--- src/HaskWeakTypes.v | 42 ++++------------- src/HaskWeakVars.v | 48 ++------------------ 17 files changed, 145 insertions(+), 174 deletions(-) rename src/{HaskCoreLiterals.v => HaskLiteralsAndTyCons.v} (74%) diff --git a/src/Extraction.v b/src/Extraction.v index ae55381..53b1185 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -12,7 +12,7 @@ Require Import NaturalDeduction. Require Import NaturalDeductionToLatex. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. diff --git a/src/HaskCore.v b/src/HaskCore.v index abd1428..9024828 100644 --- a/src/HaskCore.v +++ b/src/HaskCore.v @@ -7,7 +7,7 @@ Require Import Preamble. Require Import General. Require Import Coq.Strings.String. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreTypes. Require Import HaskCoreVars. @@ -18,7 +18,7 @@ Inductive CoreExpr {b:Type} := | CoreEApp : CoreExpr -> CoreExpr -> CoreExpr | CoreELam : b -> CoreExpr -> CoreExpr | CoreELet : CoreBind -> CoreExpr -> CoreExpr -| CoreECase : CoreExpr -> b -> CoreType -> list (@triple AltCon (list b) CoreExpr) -> CoreExpr +| CoreECase : CoreExpr -> b -> CoreType -> list (@triple CoreAltCon (list b) CoreExpr) -> CoreExpr | CoreECast : CoreExpr -> CoreCoercion -> CoreExpr | CoreENote : Note -> CoreExpr -> CoreExpr | CoreEType : CoreType -> CoreExpr @@ -40,4 +40,7 @@ Extract Inductive CoreBind => "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ]. 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 }. + +Variable coreTypeOfCoreExpr : @CoreExpr CoreVar -> CoreType. + Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType". diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 1be33fd..c4bd768 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -7,7 +7,7 @@ Require Import Preamble. Require Import General. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -15,6 +15,9 @@ Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. +Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". +Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". + Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion. @@ -84,37 +87,46 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := 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) := +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 - | WTypeVar tv => Some (v,tv,tbody) | WCoerVar _ => None + | WTypeVar tv => match coreVarToWeakVar v with + | WExprVar v' => Some (v',tv,tbody) + | _ => None + end end else None | _ => None end. -Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) := +Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) := 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 => Some (v,tv,tbody) + | WTypeVar tv => match coreVarToWeakVar v with + | WExprVar v' => Some (v',tv,tbody) + | _ => None + end | WCoerVar _ => None end else None | _ => None end. -Definition isCSP (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) := +Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) := 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 => Some (v,tv,tbody) + | WTypeVar tv => match coreVarToWeakVar v with + | WExprVar v' => Some (v',tv,tbody) + | _ => None + end | WCoerVar _ => None end else None | _ => None @@ -209,18 +221,18 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := coreExprToWeakExpr e >>= fun e' => expectTyConApp te' nil >>= fun tca => let (tc,lt) := tca in - ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar))) - : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := + ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar))) + : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := match branches with | nil => OK nil | (mkTriple alt vars e)::rest => mkBranches rest >>= fun rest' => coreExprToWeakExpr e >>= fun e' => match alt with - | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest') - | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest') + | 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 - OK (((DataAlt dc), + OK (((WeakDataAlt dc), (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)), (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)), (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)), diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index 33ed7a7..8aa81ee 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -9,17 +9,12 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. Require Import HaskCoreVars. +Require Import HaskLiteralsAndTyCons. -Variable CoreTyCon : Type. Extract Inlined Constant CoreTyCon => "TyCon.TyCon". -Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon". -Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name". Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion". -Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class". Variable classTyCon : Class_ -> CoreTyCon. Extract Inlined Constant classTyCon => "Class.classTyCon". -Variable tyConToString : CoreTyCon -> string. Extract Inlined Constant tyConToString => "outputableToString". -Variable dataConToString : CoreDataCon-> string. Extract Inlined Constant dataConToString => "outputableToString". -Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName". - Extraction Inline CoreIPName. +Variable coreTyConToString : CoreTyCon -> string. Extract Inlined Constant coreTyConToString => "outputableToString". +Variable coreDataConToString : CoreDataCon -> string. Extract Inlined Constant coreDataConToString => "outputableToString". (* this exracts onto TypeRep.Type, on the nose *) Inductive CoreType := @@ -44,10 +39,6 @@ Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined C Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)". -(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *) -Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". -Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon". - (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *) Variable coreTyCon_eq : EqDecider CoreTyCon. Extract Inlined Constant coreTyCon_eq => "(==)". Variable tyCon_eq : EqDecider TyCon. Extract Inlined Constant tyCon_eq => "(==)". @@ -62,5 +53,6 @@ Instance CoreNameEqDecidable : EqDecidable CoreName := { eqd_dec := coreName Instance CoreTypeToString : ToString CoreType := { toString := coreTypeToString }. Instance CoreNameToString : ToString CoreName := { toString := coreNameToString }. Instance CoreCoercionToString : ToString CoreCoercion := { toString := coreCoercionToString }. -Instance CoreDataConToString : ToString CoreDataCon := { toString := dataConToString }. -Instance CoreTyConToString : ToString CoreTyCon := { toString := tyConToString }. +Instance CoreDataConToString : ToString CoreDataCon := { toString := coreDataConToString }. +Instance CoreTyConToString : ToString CoreTyCon := { toString := coreTyConToString }. + diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v index 562b478..d158f05 100644 --- a/src/HaskCoreVars.v +++ b/src/HaskCoreVars.v @@ -6,6 +6,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Coq.Strings.String. +Require Import HaskLiteralsAndTyCons. (* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *) Variable CoreVar : Type. Extract Inlined Constant CoreVar => "Var.Var". @@ -13,3 +14,18 @@ Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Variable coreVarToString : CoreVar -> string. Extract Inlined Constant coreVarToString => "outputableToString". Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec := coreVar_eq }. Instance CoreVarToString : ToString CoreVar := { toString := coreVarToString }. + +Variable CoreTyCon : Type. Extract Inlined Constant CoreTyCon => "TyCon.TyCon". + +(* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *) +Inductive triple {A B C:Type} := +| mkTriple : A -> B -> C -> triple. +Notation "a ** b ** c" := (mkTriple a b c) (at level 20). +Extract Inductive triple => "(,,)" [ "(,,)" ]. + +Inductive CoreAltCon := +| DataAlt : CoreDataCon -> CoreAltCon +| LitAlt : HaskLiteral -> CoreAltCon +| DEFAULT : CoreAltCon. +Extract Inductive CoreAltCon => + "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ]. diff --git a/src/HaskCoreLiterals.v b/src/HaskLiteralsAndTyCons.v similarity index 74% rename from src/HaskCoreLiterals.v rename to src/HaskLiteralsAndTyCons.v index 05cace2..24fc00f 100644 --- a/src/HaskCoreLiterals.v +++ b/src/HaskLiteralsAndTyCons.v @@ -1,5 +1,5 @@ (*********************************************************************************************************************************) -(* HaskCoreLiterals: representation of compile-time constants (literals) *) +(* HaskLiteralsAndTyCons: representation of compile-time constants (literals) *) (*********************************************************************************************************************************) Generalizable All Variables. @@ -7,7 +7,12 @@ Require Import Preamble. Require Import General. Require Import Coq.Strings.String. Require Import HaskKinds. -Require Import HaskCoreTypes. + +Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon". + +(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *) +Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". +Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon". (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *) Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int". @@ -16,6 +21,11 @@ Variable HaskFastString : Type. Extract Inlined Constant HaskFastS Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer". Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational". +Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name". +Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class". +Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName". + Extraction Inline CoreIPName. + (* This type extracts exactly onto GHC's Literal.Literal type *) Inductive HaskLiteral := | HaskMachChar : HaskChar -> HaskLiteral @@ -47,19 +57,6 @@ Extract Inductive HaskFunctionOrData => 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: *) -Inductive triple {A B C:Type} := -| mkTriple : A -> B -> C -> triple. -Notation "a ** b ** c" := (mkTriple a b c) (at level 20). -Extract Inductive triple => "(,,)" [ "(,,)" ]. - -Inductive AltCon := -| DataAlt : CoreDataCon -> AltCon -| LitAlt : HaskLiteral -> AltCon -| DEFAULT : AltCon. -Extract Inductive AltCon => - "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ]. - (* the TyCons for each of the literals above *) Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon". Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon". @@ -84,3 +81,8 @@ match lit with | HaskMachDouble _ => doublePrimTyCon | HaskMachLabel _ _ _ => addrPrimTyCon end. + +Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString". +Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString". +Instance TyConToString : ToString TyCon := { toString := tyConToString }. +Instance TyFunToString : ToString TyFun := { toString := tyFunToString }. diff --git a/src/HaskProof.v b/src/HaskProof.v index efb9220..6474665 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -14,7 +14,7 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. Require Import HaskCoreTypes. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskStrongTypes. (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index f315603..7624c31 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -12,7 +12,7 @@ Require Import Coq.Lists.List. Require Import HaskKinds. Require Import HaskWeakVars. Require Import HaskWeakTypes. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskProof. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 2c418bd..8efd0af 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -8,10 +8,10 @@ Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskWeakVars. Require Import HaskCoreTypes. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskStrongTypes. +Require Import HaskWeakVars. Section HaskStrong. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 3798a36..1efc666 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -12,7 +12,6 @@ Require Import Coq.Init.Specif. Require Import HaskKinds. Require Import HaskStrongTypes. Require Import HaskStrong. -Require Import HaskWeakVars. Require Import HaskProof. Section HaskStrongToProof. @@ -783,16 +782,3 @@ Definition expr2proof : End HaskStrongToProof. -(* - -(* Figure 7, production "decl"; actually not used in this formalization *) -Inductive Decl :=. -| DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl -| DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl -| DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl. - -(* Figure 1, production "pgm" *) -Inductive Pgm Γ Δ := - mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ. -*) - diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index f7fc56e..71994c6 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -10,15 +10,13 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. Require Import HaskKinds. -Require Import HaskCoreLiterals. -Require Import HaskCoreVars. -Require Import HaskCoreTypes. -Require Import HaskCore. +Require Import HaskLiteralsAndTyCons. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. Require Import HaskStrongTypes. Require Import HaskStrong. +Require Import HaskCoreVars. Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ) : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) := @@ -73,8 +71,8 @@ Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Pre Section strongExprToWeakExpr. - Context (hetmet_brak : CoreVar). - Context (hetmet_esc : CoreVar). + Context (hetmet_brak : WeakExprVar). + Context (hetmet_esc : WeakExprVar). Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ} (ftv:Fresh Kind (fun _ => WeakTypeVar)) @@ -110,7 +108,7 @@ Section strongExprToWeakExpr. (update_ξ (weakLT'○ξ) (vec2list (vec_map (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb)))) (weakLT' (tbranches@@l)) }) - : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) := + : Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) := match tree with | T_Leaf None => [] | T_Leaf (Some x) => let (scb,e) := x in @@ -145,4 +143,4 @@ Section strongExprToWeakExpr. | ELR_leaf _ _ ξ' cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv fev e ite))] | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv fev b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv fev b2 ite) end. -End strongExprToWeakExpr. \ No newline at end of file +End strongExprToWeakExpr. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index e79927a..9bc4219 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -8,7 +8,7 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import General. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreTypes. Require Import HaskCoreVars. Require Import HaskWeakTypes. @@ -353,7 +353,7 @@ Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) (* like a GHC DataCon, but using PHOAS representation for types and coercions *) Record StrongAltCon {tc:TyCon} := { sac_tc := tc -; sac_altcon : AltCon +; sac_altcon : WeakAltCon ; sac_numExTyVars : nat ; sac_numCoerVars : nat ; sac_numExprVars : nat @@ -365,7 +365,7 @@ Record StrongAltCon {tc:TyCon} := ; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ }. Coercion sac_tc : StrongAltCon >-> TyCon. -Coercion sac_altcon : StrongAltCon >-> AltCon. +Coercion sac_altcon : StrongAltCon >-> WeakAltCon. Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ. diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 60b7d04..d5d66c0 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -7,14 +7,15 @@ Require Import Preamble. Require Import General. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskCoreLiterals. -Require Import HaskCore. -Require Import HaskCoreVars. -Require Import HaskCoreTypes. -Require Import HaskCoreTypes. +Require Import HaskLiteralsAndTyCons. Require Import HaskWeakVars. Require Import HaskWeakTypes. +Inductive WeakAltCon := +| WeakDataAlt : CoreDataCon -> WeakAltCon +| WeakLitAlt : HaskLiteral -> WeakAltCon +| WeakDEFAULT : WeakAltCon. + Inductive WeakExpr := | WEVar : WeakExprVar -> WeakExpr | WELit : HaskLiteral -> WeakExpr @@ -33,20 +34,18 @@ Inductive WeakExpr := (* from Weak to Core; it lets us dodge a possibly-failing type *) (* calculation. The CoreVar argument is the GlobalVar for the hetmet_brak *) (* or hetmet_esc identifier *) -| WEBrak : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr -| WEEsc : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr -| WECSP : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr +| WEBrak : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr +| WEEsc : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr +| WECSP : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr | WECase : forall (vscrut:WeakExprVar) (scrutinee:WeakExpr) (tbranches:WeakType) (tc:TyCon) (type_params:list WeakType) - (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)), + (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)), WeakExpr. Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType := (WTyCon (haskLiteralToTyCon lit)). -Variable coreTypeOfCoreExpr : @CoreExpr CoreVar -> CoreType. - Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType". diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 9607d5f..c97a63c 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -8,7 +8,7 @@ Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -20,7 +20,7 @@ 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). +Variable sortAlts : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b). Extract Inlined Constant sortAlts => "sortAlts". Implicit Arguments sortAlts [[a][b]]. @@ -31,6 +31,35 @@ Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion. Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)". +Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". +Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". + +Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon := + match wa with + | WeakDataAlt cdc => DataAlt cdc + | WeakLitAlt lit => LitAlt lit + | WeakDEFAULT => DEFAULT + end. + +Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType := + match wt with + | WTyVarTy (weakTypeVar v _) => TyVarTy v + | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2) + | WAppTy t1 t2 => match (weakTypeToCoreType t1) with + | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil)) + | t1' => AppTy t1' (weakTypeToCoreType t2) + end + | WTyCon tc => TyConApp tc nil + | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt) + | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt)) + | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty)) + | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t) + | WFunTyCon => TyConApp ArrowTyCon nil + | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil) + | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2))) + (weakTypeToCoreType t3) + end. + Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion := mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). @@ -70,12 +99,12 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches) (sortAlts (( fix mkCaseBranches (alts:Tree - ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := + ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := match alts with | T_Leaf None => nil | T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2) | T_Leaf (Some (ac,tvars,cvars,evars,e)) => - (mkTriple (ac:AltCon) + (mkTriple (weakAltConToCoreAltCon ac) (app (app (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars) (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars)) @@ -99,3 +128,4 @@ Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType := Instance weakExprToString : ToString WeakExpr := { toString := fun we => toString (weakExprToCoreExpr we) }. + diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 04e1055..2593a5c 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -10,14 +10,13 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. Require Import HaskWeakToCore. Require Import HaskStrongTypes. Require Import HaskStrong. -Require Import HaskCoreTypes. Require Import HaskCoreVars. Open Scope string_scope. @@ -260,7 +259,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds Definition mkStrongAltCon : @StrongAltCon tc. refine - {| sac_altcon := DataAlt dc + {| sac_altcon := WeakDataAlt dc ; sac_numCoerVars := length (dataConCoerKinds dc) ; sac_numExprVars := length (dataConFieldTypes dc) ; sac_ekinds := dataConExKinds dc @@ -349,7 +348,7 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. End StrongAltCon. -Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc). +Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc). destruct alt. set (c:DataCon _) as dc. set ((dataConTyCon c):TyCon) as tc' in *. @@ -363,14 +362,14 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP apply OK; refine {| sacpj_sac := {| sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil - ; sac_altcon := LitAlt h + ; sac_altcon := WeakLitAlt h |} |}. intro; intro φ; apply φ. intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. rewrite weakCK'_nil_inert. apply ψ. apply OK; refine {| sacpj_sac := {| sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil - ; sac_altcon := DEFAULT |} |}. + ; sac_altcon := WeakDEFAULT |} |}. intro; intro φ; apply φ. intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. rewrite weakCK'_nil_inert. apply ψ. @@ -591,7 +590,7 @@ Definition weakExprToStrongExpr : forall let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in mkAvars avars (tyConKind tc) φ >>= fun avars' => weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' => - (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree + (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' & Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) := match t with diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index 8f55346..4d6500d 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -8,17 +8,8 @@ Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. -Require Import HaskCoreTypes. - -Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)". -Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)". -Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon. -Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon. - -Instance TyConToString : ToString TyCon := { toString := tyConToString }. -Instance TyFunToString : ToString TyFun := { toString := tyConToString }. (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *) Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. @@ -87,28 +78,13 @@ match wc with | WCoUnsafe t1 t2 => (t1,t2) end. -Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". -Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". -Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType := - match wt with - | WTyVarTy (weakTypeVar v _) => TyVarTy v - | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2) - | WAppTy t1 t2 => match (weakTypeToCoreType t1) with - | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil)) - | t1' => AppTy t1' (weakTypeToCoreType t2) - end - | WTyCon tc => TyConApp tc nil - | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt) - | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt)) - | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty)) - | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t) - | WFunTyCon => TyConApp ArrowTyCon nil - | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil) - | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2))) - (weakTypeToCoreType t3) - end. - -Instance WeakTypeToString : ToString WeakType := - { toString := coreTypeToString ○ weakTypeToCoreType }. +(* this is a trick to allow circular definitions, post-extraction *) +Variable weakTypeToString : WeakType -> string. + Extract Inlined Constant weakTypeToString => "(coreTypeToString . weakTypeToCoreType)". +Instance WeakTypeToString : ToString WeakType := { toString := weakTypeToString }. +Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)". +Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)". +Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon. +Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 44e267d..61eafca 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -8,7 +8,7 @@ Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskWeakTypes. @@ -46,54 +46,12 @@ Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Const Definition tyConTyVars (tc:CoreTyCon) := General.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). +Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc). Variable rawTyFunKind : CoreTyCon -> Kind. Extract Inlined Constant rawTyFunKind => "(coreKindToKind . TyCon.tyConKind)". Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) := splitKind (rawTyFunKind tc). -(* -(* EqDecidable instances for all of the above *) -Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar. - apply Build_EqDecidable. - intros. - destruct v1 as [cv1 t1a t1b]. - destruct v2 as [cv2 t2a t2b]. - destruct (eqd_dec cv1 cv2); subst. - destruct (eqd_dec t1a t2a); subst. - destruct (eqd_dec t1b t2b); subst. - left; auto. - right; intro; apply n; inversion H; subst; auto. - right; intro; apply n; inversion H; subst; auto. - right; intro; apply n; inversion H; subst; auto. - Defined. - -Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar. - apply Build_EqDecidable. - intros. - destruct v1 as [cv1 k1]. - destruct v2 as [cv2 k2]. - destruct (eqd_dec cv1 cv2); subst. - destruct (eqd_dec k1 k2); subst. - left; auto. - right; intro; apply n; inversion H; subst; auto. - right; intro; apply n; inversion H; subst; auto. - Defined. - -Instance WeakVarEqDecidable : EqDecidable WeakVar. - apply Build_EqDecidable. - induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto; - destruct (eqd_dec w w0); subst. - left; auto. - right; intro X; apply n; inversion X; auto. - left; auto. - right; intro X; apply n; inversion X; auto. - left; auto. - right; intro X; apply n; inversion X; auto. - Defined. -*) - Instance WeakVarToString : ToString WeakVar := - { toString := fun x => toString (weakVarToCoreVar x) }. \ No newline at end of file + { toString := fun x => toString (weakVarToCoreVar x) }. -- 1.7.10.4