From: Adam Megacz Date: Mon, 7 Mar 2011 13:41:46 +0000 (-0800) Subject: give HaskWeak its own type representation, fix numerous bugs X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=bcb16a7fa1ff772f12807c4587609fd756b7762e give HaskWeak its own type representation, fix numerous bugs --- diff --git a/Makefile b/Makefile index ba1fb28..f16abc1 100644 --- a/Makefile +++ b/Makefile @@ -5,13 +5,9 @@ allfiles := $(coqfiles) $(shell find src -name \*.hs) default: build/CoqPass.hs build/CoqPass.hs: build/Makefile.coq $(allfiles) - - # first we build with -dont-load-proofs, since that runs very quickly - cd build; make -f Makefile.coq OPT="-dont-load-proofs" Main.vo - - # however the final extraction must be done without -dont-load-proofs cd build; make -f Makefile.coq Extraction.vo - cat src/Extraction-prefix.hs build/Extraction.hs > build/CoqPass.hs + cat src/Extraction-prefix.hs > build/CoqPass.hs + cat build/Extraction.hs | grep -v '^module' | grep -v '^import' >> build/CoqPass.hs build/Makefile.coq: $(coqfiles) mkdir -p build diff --git a/src/General.v b/src/General.v index c78daa1..b58bb96 100644 --- a/src/General.v +++ b/src/General.v @@ -13,7 +13,7 @@ Require Import Preamble. Generalizable All Variables. Require Import Omega. - +Definition EqDecider T := forall (n1 n2:T), sumbool (n1=n2) (not (n1=n2)). Class EqDecidable (T:Type) := { eqd_type := T ; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2)) @@ -113,6 +113,17 @@ Lemma tree_dec_eq : inversion H; auto. Defined. +Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A), + (mapOptionTree (g ○ f) l) = (mapOptionTree g (mapOptionTree f l)). + induction l. + destruct a. + reflexivity. + reflexivity. + simpl. + rewrite IHl1. + rewrite IHl2. + reflexivity. + Qed. @@ -322,8 +333,12 @@ Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbo auto. Defined. - - +Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T). + apply Build_EqDecidable. + intros. + apply list_eq_dec. + apply eqd_dec. + Defined. (*******************************************************************************) (* Length-Indexed Lists *) @@ -414,6 +429,28 @@ Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (leng inversion v; subst; auto. Defined. +Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n. + induction v; auto. + simpl. + omega. + Qed. + +Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v). + induction v; auto. + simpl. rewrite IHv. + reflexivity. + Qed. + +Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v. + induction v; auto. + set (vec2list (list2vec (a :: v))) as q. + rewrite <- IHv. + unfold q. + clear q. + simpl. + reflexivity. + Qed. + Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20). @@ -530,6 +567,7 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3), +Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))). @@ -548,28 +586,18 @@ Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) := end. Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20). -Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) := - match n as N return ???(vec _ N) with - | O => match l with - | nil => OK vec_nil - | _ => Error "list2vecOrError: list was too long" - end - | S n' => match l with - | nil => Error "list2vecOrError: list was too short" - | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'') - end - end. - Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type := | Indexed_Error : forall error_message:string, Indexed f (Error error_message) | Indexed_OK : forall t, f t -> Indexed f (OK t) . -Ltac xauto := try apply Indexed_Error; try apply Indexed_OK. - - - +Require Import Coq.Arith.EqNat. +Instance EqDecidableNat : EqDecidable nat. + apply Build_EqDecidable. + intros. + apply eq_nat_dec. + Defined. (* for a type with decidable equality, we can maintain lists of distinct elements *) Section DistinctList. @@ -599,3 +627,10 @@ Section DistinctList. | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2) end. End DistinctList. + +Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n). + set (list2vec l) as v. + destruct (eqd_dec (length l) n). + rewrite e in v; apply OK; apply v. + apply (Error (error_message (length l) n)). + Defined. diff --git a/src/HaskCore.v b/src/HaskCore.v index 64699fd..3d5f860 100644 --- a/src/HaskCore.v +++ b/src/HaskCore.v @@ -6,8 +6,8 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Coq.Strings.String. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreLiterals. Require Import HaskCoreTypes. Require Import HaskCoreVars. @@ -42,14 +42,6 @@ Extract Inductive CoreBind => (* extracts the Name from a CoreVar *) Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". -Extract Constant ArrowTyCon => "Type.funTyCon". (* Figure 7, (->) *) -Extract Constant CoFunConst => "TyCon.TyCon". Extraction Implicit CoFunConst [ 1 ]. -Extract Constant TyFunConst => "TyCon.TyCon". Extraction Implicit TyFunConst [ 1 ]. - -(*Extract Inlined Constant getDataCons => "TyCon.tyConDataCons".*) -Variable mkTyConApp : forall n, TyCon n -> list CoreType -> CoreType. - Extract Inlined Constant mkTyConApp => "Type.mkTyConApp". - (* 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". diff --git a/src/HaskLiterals.v b/src/HaskCoreLiterals.v similarity index 74% rename from src/HaskLiterals.v rename to src/HaskCoreLiterals.v index f41bcfb..d332ccf 100644 --- a/src/HaskLiterals.v +++ b/src/HaskCoreLiterals.v @@ -1,12 +1,13 @@ (*********************************************************************************************************************************) -(* HaskLiterals: representation of compile-time constants (literals) *) +(* HaskCoreLiterals: representation of compile-time constants (literals) *) (*********************************************************************************************************************************) Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Coq.Strings.String. -Require Import HaskGeneral. +Require Import HaskKinds. +Require Import HaskCoreTypes. (* 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". @@ -43,18 +44,26 @@ Extract Inductive HaskLiteral => "Literal.Literal" Extract Inductive HaskFunctionOrData => "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ]. +Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString". + +(* 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 => "(,,)" [ "(,,)" ]. + (* the TyCons for each of the literals above *) -Variable addrPrimTyCon : TyCon 0. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon". -Variable intPrimTyCon : TyCon 0. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon". -Variable wordPrimTyCon : TyCon 0. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon". -Variable int64PrimTyCon : TyCon 0. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon". -Variable word64PrimTyCon : TyCon 0. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon". -Variable floatPrimTyCon : TyCon 0. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon". -Variable doublePrimTyCon : TyCon 0. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon". -Variable charPrimTyCon : TyCon 0. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon". +Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon". +Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon". +Variable wordPrimTyCon : TyCon. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon". +Variable int64PrimTyCon : TyCon. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon". +Variable word64PrimTyCon : TyCon. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon". +Variable floatPrimTyCon : TyCon. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon". +Variable doublePrimTyCon : TyCon. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon". +Variable charPrimTyCon : TyCon. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon". (* retrieves the TyCon for a given Literal *) -Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon 0 := +Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon := match lit with | HaskMachNullAddr => addrPrimTyCon | HaskMachChar _ => charPrimTyCon @@ -68,18 +77,9 @@ match lit with | HaskMachLabel _ _ _ => addrPrimTyCon end. -Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString". - -(* 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 : forall {n:nat}(tc:TyCon n){m q r:nat}, @DataCon n tc m q r -> AltCon +| DataAlt : CoreDataCon -> AltCon | LitAlt : HaskLiteral -> AltCon -| DEFAULT : AltCon. +| DEFAULT : AltCon. Extract Inductive AltCon => "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ]. - diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 3555a8a..d269cd1 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -6,16 +6,75 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreLiterals. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. Require Import HaskWeakVars. +Require Import HaskWeakTypes. Require Import HaskWeak. +(* this distinguishes SystemFC "type functions" (true) which are always fully applied from "type constructors" which aren't *) +Variable isFamilyTyCon : TyCon -> bool. Extract Inlined Constant isFamilyTyCon => "TyCon.isFamilyTyCon". + + +Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon). + Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". +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" + end + + | AppTy t1 t2 => coreTypeToWeakType t2 >>= fun t2' => coreTypeToWeakType t1 >>= fun t1' => OK (WAppTy t1' t2') + + | TyConApp tc lct => + let recurse := ((fix rec tl := match tl with + | nil => OK nil + | a::b => coreTypeToWeakType a >>= fun a' => rec b >>= fun b' => OK (a'::b') + end) lct) + in if (isFamilyTyCon tc) + then recurse >>= fun recurse' => OK (WTyFunApp tc recurse') + else if eqd_dec tc ModalBoxTyCon + 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" + end + | _ => Error "mis-applied modal box tycon" + end + else let tc' := if eqd_dec tc ArrowTyCon + then WFunTyCon + else WTyCon tc + in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc') + | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType t1 >>= fun t1' => + coreTypeToWeakType t2 >>= fun t2' => + coreTypeToWeakType t3 >>= fun t3' => + OK (WCoFunTy t1' t2' t3') + | FunTy t1 t2 => coreTypeToWeakType t1 >>= fun t1' => + 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" + | WTypeVar tv => coreTypeToWeakType t >>= fun t' => OK (WForAllTy tv t') + | WCoerVar _ => Error "encountered coercion variable in a type" + end + | PredTy (ClassP cl lct) => ((fix rec tl := match tl with + | nil => OK nil + | a::b => coreTypeToWeakType a >>= fun a' => + rec b >>= fun b' => OK (a'::b') + end) lct) >>= fun lct' => OK (WClassP cl lct') + | PredTy (IParam ipn ct) => coreTypeToWeakType ct >>= fun ct' => OK (WIParam ipn ct') + | PredTy (EqPred _ _) => Error "hit a bare EqPred" + end. + (* detects our crude Core-encoding of modal type introduction/elimination forms *) Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) := match ce with @@ -40,9 +99,11 @@ match ce with | _ => None end. -Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion := +Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion := let (t1,t2) := coreCoercionKind cc - in weakCoercion t1 t2 cc. + in coreTypeToWeakType t1 >>= fun t1' => + coreTypeToWeakType t2 >>= fun t2' => + OK (weakCoercion t1' t2' cc). Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match ce with @@ -50,7 +111,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | 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)) + coreCoercionToWeakCoercion co >>= fun co' => + OK (WECast e' co') | CoreEVar v => match coreVarToWeakVar v with | WExprVar ev => OK (WEVar ev) @@ -59,12 +121,20 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := end | CoreEApp e1 e2 => match isBrak e1 with - | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e' t) + | Some (tv,t) => + coreExprToWeakExpr e2 >>= fun e' => + coreTypeToWeakType t >>= fun t' => + OK (WEBrak tv e' t') | None => match isEsc e1 with - | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e' t) + | Some (tv,t) => + coreExprToWeakExpr e2 >>= fun e' => + coreTypeToWeakType t >>= fun t' => + OK (WEEsc tv e' t') | None => coreExprToWeakExpr e1 >>= fun e1' => match e2 with - | CoreEType t => OK (WETyApp e1' t) + | CoreEType t => + coreTypeToWeakType t >>= fun t' => + OK (WETyApp e1' t') | _ => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2') end end @@ -105,10 +175,11 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | WTypeVar _ => Error "found a type variable in a case" | WCoerVar _ => Error "found a coercion variable in a case" | WExprVar ev => - coreExprToWeakExpr e - >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' => - match te' with - | TyConApp _ tc lt => + coreExprToWeakExpr e >>= fun e' => + weakTypeOfWeakExpr e' >>= fun te' => + (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end) + >>= 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)) := match branches with @@ -119,20 +190,18 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match alt with | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest') | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest') - | DataAlt _ _ _ _ tc' dc => let vars := map coreVarToWeakVar vars in - OK (((DataAlt _ dc), + | DataAlt dc => let vars := map coreVarToWeakVar vars in + OK (((DataAlt 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)), e')::rest') end end) alts) - >>= fun branches => coreExprToWeakExpr e - >>= fun scrutinee => - list2vecOrError lt _ >>= fun lt' => - OK (WELet ev scrutinee (WECase (WEVar ev) tbranches tc lt' (unleaves branches))) - | _ => Error "found a case whose scrutinee's type wasn't a TyConApp" - end + >>= fun branches => + coreExprToWeakExpr e >>= fun scrutinee => + coreTypeToWeakType tbranches >>= fun tbranches' => + OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches))) end end. diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index a567196..4a7a056 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -6,49 +6,62 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Coq.Strings.String. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import Coq.Lists.List. +Require Import HaskKinds. Require Import HaskCoreVars. -Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name". -Variable coreName_eq : forall (a b:CoreName), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreName_eq => "(==)". -Axiom coreName_eq_refl : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)). -Instance CoreNameEqDecidable : EqDecidable CoreName := -{ eqd_dec := coreName_eq -}. - -Inductive CoreIPName : Type -> Type := . Extract Inductive CoreIPName => "CoreSyn.IPName" [ ]. +Variable TyCon : Type. Extract Inlined Constant TyCon => "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 CoreCoFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". +Variable CoreTyFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". +Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class". +Variable classTyCon : Class_ -> TyCon. Extract Inlined Constant classTyCon => "Class.classTyCon". +Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString". +Variable dataConToString : CoreDataCon-> string. Extract Inlined Constant dataConToString => "outputableToString". +Variable tyFunToString : CoreTyFunConst -> string. Extract Inlined Constant tyFunToString => "outputableToString". +Variable coFunToString : CoreCoFunConst -> string. Extract Inlined Constant coFunToString => "outputableToString". +Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring". +Variable CoreIPName : Type -> Type. + Extract Constant CoreIPName "’a" => "BasicTypes.IPName". + Extraction Inline CoreIPName. (* this exracts onto TypeRep.Type, on the nose *) Inductive CoreType := -| TyVarTy : CoreVar -> CoreType -| AppTy : CoreType -> CoreType -> CoreType (* first arg must be AppTy or TyVarTy*) -| TyConApp : forall {n}, TyCon n -> list CoreType -> CoreType -| FunTy : CoreType -> CoreType -> CoreType (* technically redundant since we have FunTyCon *) -| ForAllTy : CoreVar -> CoreType -> CoreType -| PredTy : PredType -> CoreType +| TyVarTy : CoreVar -> CoreType +| AppTy : CoreType -> CoreType -> CoreType (* first arg must be AppTy or TyVarTy*) +| TyConApp : TyCon -> list CoreType -> CoreType +| FunTy : CoreType -> CoreType -> CoreType (* technically redundant since we have FunTyCon *) +| ForAllTy : CoreVar -> CoreType -> CoreType +| PredTy : PredType -> CoreType with PredType := -| ClassP : forall {n}, Class_ n -> list CoreType -> PredType -| IParam : CoreIPName CoreName -> CoreType -> PredType -| EqPred : CoreType -> CoreType -> PredType. +| ClassP : Class_ -> list CoreType -> PredType +| IParam : CoreIPName CoreName -> CoreType -> PredType +| EqPred : CoreType -> CoreType -> PredType. Extract Inductive CoreType => "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ]. Extract Inductive PredType => "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ]. +(* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *) +Variable tyCon_eq : EqDecider TyCon. Extract Inlined Constant tyCon_eq => "(==)". +Variable dataCon_eq : EqDecider CoreDataCon. Extract Inlined Constant dataCon_eq => "(==)". +Variable coreName_eq : EqDecider CoreName. Extract Inlined Constant coreName_eq => "(==)". +Variable coretype_eq_dec : EqDecider CoreType. Extract Inlined Constant coretype_eq_dec => "checkTypeEquality". +Instance CoreTypeEqDecidable : EqDecidable CoreType := { eqd_dec := coretype_eq_dec }. +Instance TyConEqDecidable : EqDecidable TyCon := { eqd_dec := tyCon_eq }. +Instance DataConEqDecidable : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }. +Instance CoreNameEqDecidable : EqDecidable CoreName := { eqd_dec := coreName_eq }. + +(* Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString". -Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". +*) +Variable coreTypeToString : CoreType -> string. + Extract Inlined Constant coreTypeToString => "showType". -Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion". +Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". -Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. - Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". - -Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)). - Extract Inlined Constant coretype_eq_dec => "Type.coreEqType". - Instance CoreTypeEqDecidable : EqDecidable CoreType. - apply Build_EqDecidable. - apply coretype_eq_dec. - Defined. +Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". +Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". -Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v index a55c09b..6e61128 100644 --- a/src/HaskCoreVars.v +++ b/src/HaskCoreVars.v @@ -5,14 +5,10 @@ Generalizable All Variables. Require Import Preamble. Require Import General. -Require Import HaskGeneral. (* 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". Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreVar_eq => "(==)". Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)). -Instance CoreVarEqDecidable : EqDecidable CoreVar := -{ eqd_dec := coreVar_eq -(*; eqd_dec_reflexive := coreVar_eq_refl*) -}. +Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec := coreVar_eq }. diff --git a/src/HaskGeneral.v b/src/HaskGeneral.v deleted file mode 100644 index 0c9ba33..0000000 --- a/src/HaskGeneral.v +++ /dev/null @@ -1,73 +0,0 @@ -(*********************************************************************************************************************************) -(* HaskGeneral: Definitions shared by all four representations (Core, Weak, Strong, Proof) *) -(*********************************************************************************************************************************) - -Generalizable All Variables. -Require Import Preamble. -Require Import General. -Require Import Coq.Strings.String. -Open Scope nat_scope. - -(* all Figure references are to the System FC1 paper *) - -(* Figure 1: production T; index is the number of type constructors *) -Variable TyCon : nat -> Type. Extract Inlined Constant TyCon => "TyCon.TyCon". - -(* Figure 1: production "K" *) -Variable DataCon : ∀n, TyCon n - -> nat (* number of existential tyvars associated with this datacon *) - -> nat (* number of coercion variables associated with this datacon *) - -> nat (* number of value variables (fields) associated with this datacon *) - -> Type. Extract Inlined Constant DataCon => "DataCon.DataCon". - -Variable CoFunConst : nat -> Type. (* production "C"; extracts to TyCon.TyCon *) -Variable TyFunConst : nat -> Type. (* production "Sn"; extracts to TyCon.TyCon *) - -(* magic TyCons *) -Variable ArrowTyCon : TyCon 2. (* the TyCon for (->), the regular old function-space type constructor *) -Variable CoercionTyCon : TyCon 2. (* the TyCon for (+>), the coercion type constructor *) -Variable hetMetCodeTypeTyCon : TyCon 2. Extract Inlined Constant hetMetCodeTypeTyCon => "TysWiredIn.hetMetCodeTypeTyCon". -Variable Class_ : nat -> Type. Extract Inlined Constant Class_ => "Class.Class". -Variable classTyCon : ∀ n, Class_ n -> TyCon n. Extract Inlined Constant classTyCon => "Class.classTyCon". -Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note". -Implicit Arguments DataCon [ [n] ]. - -(* Figure 7: production κ, ι *) -Inductive Kind : Type := - | KindType : Kind (* ★ - the kind of boxed types*) - | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *) - | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *) - | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *) - | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *) - | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *). - -Notation "'★'" := KindType. -Notation "a ⇛ b" := (KindTypeFunction a b). - -Instance KindEqDecidable : EqDecidable Kind. - apply Build_EqDecidable. - induction v1. - destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. - destruct v2; try (right; intro q; inversion q; fail) ; auto. - destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto; - right; intro; subst; inversion H; subst; apply n; auto. - destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. - destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. - destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. - destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. - Defined. - -Variable tyConToString : forall n, TyCon n -> string. Extract Inlined Constant tyConToString => "outputableToString". -Variable tyFunToString : ∀ n, TyFunConst n -> string. Extract Inlined Constant tyFunToString => "outputableToString". -Variable coFunToString : ∀ n, CoFunConst n -> string. Extract Inlined Constant coFunToString => "outputableToString". -Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring". - - -Axiom tycons_distinct : ~(ArrowTyCon=hetMetCodeTypeTyCon). -(* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *) -Variable tyCon_eq : forall {k}(n1 n2:TyCon k), sumbool (n1=n2) (not (n1=n2)). - Extract Inlined Constant tyCon_eq => "(==)". -Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s), sumbool (n1=n2) (not (n1=n2)). - Extract Inlined Constant dataCon_eq => "(==)". -Instance TyConEqDecidable {n} : EqDecidable (TyCon n) := { eqd_dec := tyCon_eq }. -Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) := { eqd_dec := dataCon_eq }. diff --git a/src/HaskKinds.v b/src/HaskKinds.v new file mode 100644 index 0000000..b063b56 --- /dev/null +++ b/src/HaskKinds.v @@ -0,0 +1,38 @@ +(*********************************************************************************************************************************) +(* HaskKinds: Definitions shared by all four representations (Core, Weak, Strong, Proof) *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Open Scope nat_scope. + +Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note". +Variable nat2string : nat -> string. Extract Inlined Constant nat2string => "nat2string". + +(* Figure 7: production κ, ι *) +Inductive Kind : Type := + | KindType : Kind (* ★ - the kind of boxed types*) + | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *) + | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *) + | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *) + | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *) + | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *). + +Notation "'★'" := KindType. +Notation "a ⇛ b" := (KindTypeFunction a b). + +Instance KindEqDecidable : EqDecidable Kind. + apply Build_EqDecidable. + induction v1. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; auto. + destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto; + right; intro; subst; inversion H; subst; apply n; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + Defined. + diff --git a/src/HaskProof.v b/src/HaskProof.v index 2508976..8da87e8 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -12,8 +12,9 @@ Require Import General. Require Import NaturalDeduction. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreTypes. +Require Import HaskCoreLiterals. Require Import HaskStrongTypes. (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid @@ -48,14 +49,15 @@ Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg := Coercion UJudg2judg : UJudg >-> Judg. (* information needed to define a case branch in a HaskProof *) -Record ProofCaseBranch {n}{tc:TyCon n}{Γ}{lev}{branchtype : HaskType Γ}{avars} := -{ pcb_scb : @StrongCaseBranch n tc Γ avars -; pcb_freevars : Tree ??(LeveledHaskType Γ) -; pcb_judg := scb_Γ pcb_scb > scb_Δ pcb_scb - > (mapOptionTree weakLT' pcb_freevars),,(unleaves (vec2list (scb_types pcb_scb))) - |- [weakLT' (branchtype @@ lev)] +Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ}{avars} := +{ pcb_scb : @StrongAltCon tc +; pcb_freevars : Tree ??(LeveledHaskType Γ) +; pcb_judg := sac_Γ pcb_scb Γ > sac_Δ pcb_scb Γ avars (map weakCK' Δ) + > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev) + (vec2list (sac_types pcb_scb Γ avars)))) + |- [weakLT' (branchtype @@ lev)] }. -Coercion pcb_scb : ProofCaseBranch >-> StrongCaseBranch. +Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon. Implicit Arguments ProofCaseBranch [ ]. (* Figure 3, production $\vdash_E$, Uniform rules *) @@ -98,19 +100,19 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RAbsT : ∀ Γ Δ Σ κ σ l, Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]] [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]] -| RAppCo : forall Γ Δ Σ κ σ₁ σ₂ σ γ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> - Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂:κ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]] +| RAppCo : forall Γ Δ Σ σ₁ σ₂ σ γ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> + Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]] | RAbsCo : ∀ Γ Δ Σ κ σ σ₁ σ₂ l, Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] - [Γ > Δ > Σ |- [σ₁∼∼σ₂:κ⇒ σ @@l]] + [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] | RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ] -| RCase : forall Γ Δ lev n tc Σ avars tbranches - (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)), +| RCase : forall Γ Δ lev tc Σ avars tbranches + (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)), Rule ((mapOptionTree pcb_judg alts),, - [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ]) + [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ]) [Γ > Δ > (mapOptionTreeAndFlatten pcb_freevars alts),,Σ |- [ tbranches @@ lev ] ] . Coercion RURule : URule >-> Rule. @@ -125,12 +127,12 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RCast : ∀ Γ Δ Σ σ τ γ q l, Rule_Flat (RCast Γ Δ Σ σ τ γ q l) | Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q ) | Flat_RAppT : ∀ Γ Δ Σ κ σ τ q l, Rule_Flat (RAppT Γ Δ Σ κ σ τ q l) -| Flat_RAppCo : ∀ Γ Δ Σ κ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ κ σ₁ σ₂ σ γ q l) +| Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l) | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x ) | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l) | Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l) | Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e) -| Flat_RCase : ∀ Σ Γ T κlen κ θ l x q, Rule_Flat (RCase Σ Γ T κlen κ θ l x q). +| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x ). (* given a proof that uses only uniform rules, we can produce a general proof *) Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index e239205..493e6ce 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -9,15 +9,15 @@ Require Import NaturalDeduction. Require Import NaturalDeductionToLatex. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreLiterals. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskProof. +Require Import HaskCoreTypes. (* escapifies any characters which might cause trouble for LaTeX *) Variable sanitizeForLatex : string -> string. Extract Inlined Constant sanitizeForLatex => "sanitizeForLatex". -Variable nat2string : nat -> string. Extract Inlined Constant nat2string => "nat2string". Open Scope string_scope. Section ToLatex. @@ -71,24 +71,20 @@ Section ToLatex. Fixpoint type2latex (needparens:bool)(n:nat)(t:RawHaskType nat) {struct t} : string := match t with | TVar v => tyvar2greek v - | TCon _ tc => "\text{\tt{"+++sanitizeForLatex (tyConToString _ tc) +++"}}" - | TCoerc κ => "{\text{\tt{(+>)}}}_{"+++ kind2latex κ +++"}" + | TCon tc => "\text{\tt{"+++sanitizeForLatex (tyConToString tc) +++"}}" + | TCoerc t1 t2 t => "{("+++type2latex false n t1+++"{\sim}" + +++type2latex false n t2+++")}\Rightarrow{" + +++type2latex needparens n t+++"}" + | (TApp (TApp TArrow t1) t2) => + (if needparens + then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")" + else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)) + | TArrow => "\text{\tt{(->)}}" | TApp t1 t2 => - match (match t1 with - | TApp (TCon 2 tc) t1' => - if (tyCon_eq tc ArrowTyCon) - then inl _ (if needparens - then "("+++(type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2)+++")" - else (type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2)) - else inr _ tt - | _ => inr _ tt - end) with - | inl x => x - | _ => if needparens + if needparens then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")" else (type2latex true n t1)+++" "+++(type2latex false n t2) - end - | TFCApp n tfc lt => "{\text{\tt{"+++sanitizeForLatex (tyFunToString _ tfc) +++"}}}"+++ + | TFCApp tfc lt => "{\text{\tt{"+++sanitizeForLatex (tyConToString tfc) +++"}}}"+++ "_{"+++(nat2string n)+++"}"+++ fold_left (fun x y => " \ "+++x+++y) ((fix type2latex_vec (needparens:bool)(n:nat){m}(lt:vec (RawHaskType nat) m) @@ -169,14 +165,14 @@ Section ToLatex. | RCast Γ _ Σ σ τ γ p x => "Cast" | RAbsT Γ Σ κ σ a p => "AbsT" | RAppT Γ _ Σ κ σ τ p y => "AppT" - | RAppCo Γ _ Σ κ _ σ₁ σ₂ σ γ p => "AppCo" + | RAppCo Γ _ Σ _ σ₁ σ₂ σ γ p => "AppCo" | RAbsCo Γ Σ κ σ cc σ₁ σ₂ p y q => "AbsCo" | RApp Γ _ Σ₁ Σ₂ tx te p => "App" | RLet Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let" | REmptyGroup _ a => "REmptyGroup" | RBindingGroup _ a b c d e => "RBindingGroup" | RLetRec Γ _ p lri q => "LetRec" - | RCase Σ Γ T κlen κ ldcd τ _ _ => "Case" + | RCase Σ Γ T κlen κ ldcd τ _ => "Case" | RBrak Σ _ a b c _ => "Brak" | REsc Σ _ a b c _ => "Esc" end. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 2582fb4..50e7ab3 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -7,8 +7,9 @@ Require Import Preamble. Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreTypes. +Require Import HaskCoreLiterals. Require Import HaskStrongTypes. Section HaskStrong. @@ -17,13 +18,15 @@ Section HaskStrong. Context `{EQD_VV:EqDecidable VV}. (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) - Record StrongCaseBranchWithVVs {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := - { scbwv_scb : @StrongCaseBranch n tc Γ atypes - ; scbwv_exprvars : vec VV (saci_numExprVars scbwv_scb) - ; scbwv_varstypes := vec2list (vec_zip scbwv_exprvars (scb_types scbwv_scb)) + Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:vec (HaskType Γ) tc} := + { scbwv_sac : @StrongAltCon tc + ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac) + ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes) + ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list + (vec_map (fun x => ((fst x),(snd x @@ weakL' lev))) scbwv_varstypes)) }. - Implicit Arguments StrongCaseBranchWithVVs [[n][Γ]]. - Coercion scbwv_scb : StrongCaseBranchWithVVs >-> StrongCaseBranch. + Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. + Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon. Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> LeveledHaskType Γ -> Type := | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) @@ -36,15 +39,18 @@ Section HaskStrong. | ECast : ∀ Γ Δ ξ γ t1 t2 l, Δ ⊢ᴄᴏ γ : t1 ∼ t2 -> Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t | ETyApp : ∀ Γ Δ κ σ τ ξ l, Γ ⊢ᴛy τ : κ -> Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l) - | ECoLam : ∀ Γ Δ κ σ σ₁ σ₂ ξ l, Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ :κ ⇒ σ @@ l) - | ECoApp : ∀ Γ Δ κ γ σ₁ σ₂ σ ξ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> Expr Γ Δ ξ (σ₁ ∼∼ σ₂ : κ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l) + | ECoLam : ∀ Γ Δ κ σ σ₁ σ₂ ξ l, Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ @@ l) + | ECoApp : ∀ Γ Δ γ σ₁ σ₂ σ ξ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l) | ETyLam : ∀ Γ Δ ξ κ σ l, Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l) - | ECase : forall Γ Δ ξ l n (tc:TyCon n) atypes tbranches, + | ECase : forall Γ Δ ξ l tc atypes tbranches, Expr Γ Δ ξ (caseType tc atypes @@ l) -> Tree ??{ scb : StrongCaseBranchWithVVs tc atypes - & Expr (scb_Γ scb) (scb_Δ scb) (update_ξ (weakLT'○ξ) (scbwv_varstypes scb)) (weakLT' (tbranches@@l)) } -> + & Expr (sac_Γ scb Γ) + (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) + (weakLT' (tbranches@@l)) } -> Expr Γ Δ ξ (tbranches @@ l) | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in @@ -60,4 +66,4 @@ Section HaskStrong. . End HaskStrong. -Implicit Arguments StrongCaseBranchWithVVs [[n][Γ]]. \ No newline at end of file +Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 614a09c..916afe1 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -4,11 +4,82 @@ Generalizable All Variables. Require Import Preamble. -Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import General. +Require Import HaskKinds. +Require Import HaskCoreLiterals. +Require Import HaskCoreTypes. (* FIXME *) +Require Import HaskCoreVars. (* FIXME *) +Require Import HaskWeakTypes. +Require Import HaskWeakVars. (* FIXME *) +Require Import HaskCoreToWeak. (* FIXME *) + +Variable CoFunConst : nat -> Type. (* FIXME *) +Variable TyFunConst : nat -> Type. (* FIXME *) + +Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon". + +Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars". +Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta". +Variable dataConOrigArgTys_:CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_ =>"DataCon.dataConOrigArgTys". +Variable getTyConTyVars_ : TyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "TyCon.tyConTyVars". + +(* FIXME: might be a better idea to panic here than simply drop things that look wrong *) +Definition tyConTyVars (tc:TyCon) := + filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)). + Opaque tyConTyVars. +Definition dataConExTyVars cdc := + filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)). + Opaque dataConExTyVars. +Definition dataConCoerKinds cdc := + filter (map (fun x => match x with EqPred t1 t2 => + match ( + coreTypeToWeakType t1 >>= fun t1' => + coreTypeToWeakType t2 >>= fun t2' => + OK (t1',t2')) + with OK z => Some z + | _ => None + end + | _ => None + end) (dataConEqTheta_ cdc)). + Opaque dataConCoerKinds. +Definition dataConFieldTypes cdc := + filter (map (fun x => match coreTypeToWeakType x with + | OK z => Some z + | _ => None + end) (dataConOrigArgTys_ cdc)). + +Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc). + Coercion tyConNumKinds : TyCon >-> nat. + +Inductive DataCon : TyCon -> Type := + mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc). + Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end. + Coercion mkDataCon : CoreDataCon >-> DataCon. + Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon. + (*Opaque DataCon.*) + +Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool. + intros. + destruct dc1. + destruct dc2. + exact (if eqd_dec cdc cdc0 then true else false). + Defined. + +Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2). + +Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc). + intros. + apply Build_EqDecidable. + intros. + set (trust_compare_datacons _ v1 v2) as x. + set (compare_datacons tc v1 v2) as y. + assert (y=compare_datacons tc v1 v2). reflexivity. + destruct y; rewrite <- H in x. + left; auto. + right; auto. + Defined. (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *) Section Raw. @@ -19,13 +90,14 @@ Section Raw. (* Figure 7: ρ, σ, τ, ν *) Inductive RawHaskType : Type := | TVar : TV -> RawHaskType (* a *) - | TCon : ∀n, TyCon n -> RawHaskType (* T *) - | TCoerc : Kind -> RawHaskType (* (+>) *) + | TCon : TyCon -> RawHaskType (* T *) + | TArrow : RawHaskType (* (->) *) + | TCoerc : RawHaskType -> RawHaskType -> RawHaskType -> RawHaskType (* (+>) *) | TApp : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) - | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *) + | TFCApp : forall tc:TyCon, vec RawHaskType tc -> RawHaskType (* S_n *) | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *) | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *). - + (* the "kind" of a coercion is a pair of types *) Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind. @@ -40,8 +112,8 @@ Section Raw. | CoType : RawHaskType -> RawHaskCoer (* τ *) | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *) - | CoCFApp : ∀n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) - | CoTFApp : ∀n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) + | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) + | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *) | CoSym : RawHaskCoer -> RawHaskCoer (* sym *) | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) @@ -51,15 +123,14 @@ Section Raw. End CV. End Raw. -Implicit Arguments TCon [ [TV] [n]]. -Implicit Arguments TFCApp [ [TV] [n]]. +Implicit Arguments TCon [ [TV] ]. +Implicit Arguments TFCApp [ [TV] ]. Implicit Arguments RawHaskType [ ]. Implicit Arguments RawHaskCoer [ ]. Implicit Arguments RawCoercionKind [ ]. -Notation "t1 ---> t2" := (fun TV env => (@TApp _ (@TApp _ (@TCon TV _ ArrowTyCon) (t1 TV env)) (t2 TV env))). -Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" := - (fun TV env => @TApp _ (@TApp _ (@TCon _ _ ArrowTyCon) (@TApp _ (@TApp _ (@TCoerc _ κ) (φ₁ TV env)) (φ₂ TV env))) (φ₃ TV env)). +Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))). +Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)). @@ -94,10 +165,13 @@ Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), Definition HaskTApp {Γ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(cv:HaskTyVar Γ) : HaskType Γ := fun TV env => σ TV env (cv TV env). Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env). -Definition HaskTCon {Γ}{n}(tc:TyCon n) : HaskType Γ := fun TV ite => TCon tc. +Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ := fun TV ite => TCon tc. Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite). Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ := fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite). +Definition unMkHaskCoercionKind {Γ}(hck:HaskCoercionKind Γ) : (HaskType Γ * HaskType Γ) := + ((fun TV ite => match (hck TV ite) with mkRawCoercionKind t1 _ => t1 end), + (fun TV ite => match (hck TV ite) with mkRawCoercionKind _ t2 => t2 end)). (* PHOAS substitution on types *) @@ -108,15 +182,16 @@ Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> Raw | TVar x => x | TAll k y => TAll k (fun v => flattenT (y (TVar v))) | TApp x y => TApp (flattenT x) (flattenT y) - | TCon n tc => TCon tc - | TCoerc k => TCoerc k + | TCon tc => TCon tc + | TCoerc t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t) + | TArrow => TArrow | TCode v e => TCode (flattenT v) (flattenT e) - | TFCApp n tfc lt => TFCApp tfc + | TFCApp tfc lt => TFCApp tfc ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n := match expv in vec _ N return vec (RawHaskType TV) N with | vec_nil => vec_nil | x:::y => (flattenT x):::(flatten_vec _ y) - end) n lt) + end) _ lt) end) (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)). Notation "t @@ l" := (@mkLeveledHaskType _ t l) (at level 20). @@ -125,21 +200,6 @@ Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). -(* like a GHC DataCon, but using PHOAS representation for types and coercions *) -Record StrongAltConInfo {n}{tc:TyCon n} := -{ saci_numExTyVars : nat -; saci_numCoerVars : nat -; saci_numExprVars : nat -; saci_akinds : vec Kind n -; saci_ekinds : vec Kind saci_numExTyVars -; saci_kinds := app (vec2list saci_akinds) (vec2list saci_ekinds) -; saci_coercions : vec (HaskType saci_kinds * HaskType saci_kinds) saci_numCoerVars -; saci_types : vec (HaskType saci_kinds) saci_numExprVars -}. -Implicit Arguments StrongAltConInfo [[n]]. - -Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) := - fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc). @@ -151,7 +211,7 @@ Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) := -(* FIXME: it's a mess below this point *) +(* yeah, things are kind of messy below this point *) Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite. @@ -209,6 +269,15 @@ Definition lamer {a}{b}{c}(lt:HaskType (app (app a b) c)) : HaskType (app a (a rewrite <- ass_app in lt. exact lt. Defined. +Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ) := + let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT t1) (weakT t2). +Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ) := + let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT' t1) (weakT' t2). +Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := +match κ as K return list (HaskCoercionKind (app K Γ)) with + | nil => hck + | _ => map weakCK' hck +end. Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ). induction κ; auto. apply weakL; auto. Defined. Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end. @@ -237,11 +306,31 @@ Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV := fun TV ite tv => (f TV (weakITE ite) tv). +(* like a GHC DataCon, but using PHOAS representation for types and coercions *) +Record StrongAltCon {tc:TyCon} := +{ sac_altcon : AltCon +; sac_numExTyVars : nat +; sac_numCoerVars : nat +; sac_numExprVars : nat +; sac_akinds : vec Kind tc +; sac_ekinds : vec Kind sac_numExTyVars +; sac_kinds := app (vec2list sac_akinds) (vec2list sac_ekinds) +; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ +; sac_coercions : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars +; sac_types : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskType (sac_Γ Γ)) sac_numExprVars +; sac_Δ := fun Γ (atypes:vec (HaskType Γ) tc) Δ => app (vec2list (sac_coercions Γ atypes)) Δ +}. +Coercion sac_altcon : StrongAltCon >-> AltCon. + +Definition caseType {Γ:TypeEnv}(tc:TyCon)(atypes:vec (HaskType Γ) tc) := + fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc). + + (***************************************************************************************************) (* Well-Formedness of Types and Coercions *) (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *) -Inductive TypeFunctionDecl (n:nat)(tfc:TyFunConst n)(vk:vec Kind n) : Type := - mkTFD : Kind -> TypeFunctionDecl n tfc vk. +Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type := + mkTFD : Kind -> TypeFunctionDecl tfc vk. (* Figure 8, upper half *) @@ -257,8 +346,8 @@ Inductive WellKinded_RawHaskType (TV:Type) | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ , (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) -> WellKinded_RawHaskType TV _ env (TAll κ σ) ★ - | TySCon : forall Γ env n tfc lt vk ι , - @TypeFunctionDecl n tfc vk -> + | TySCon : forall Γ env tfc lt vk ι , + @TypeFunctionDecl tfc vk -> ListWellKinded_RawHaskType TV Γ _ env lt vk -> WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι with ListWellKinded_RawHaskType (TV:Type) @@ -270,32 +359,42 @@ with ListWellKinded_RawHaskType (TV:Type) ListWellKinded_RawHaskType TV Γ n env lt lk -> ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk). -(* -Fixpoint kindOfRawHaskType {TV}(rht:RawHaskType Kind) : Kind := +Variable kindOfTyCon : forall (tc:TyCon), Kind. + Extract Inlined Constant kindOfTyCon => "(\x -> Prelude.error ""not implemented yet"")". + +Fixpoint kindOfRawHaskType (rht:RawHaskType Kind) : ???Kind := match rht with - | TVar k => k - | TCon n tc => ̱★ (* FIXME: use the StrongAltConInfo *) - | TCoerc k => k ⇛ (k ⇛ (★ ⇛ ★ )) - | TApp ht1 ht2 : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) - | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *) - | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *) - | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *). -*) + | TVar k => OK k + | TCon tc => OK (kindOfTyCon tc) + | TCoerc t1 t2 t => OK (★ ⇛ ★ ) + | TArrow => OK (★ ⇛ ★ ⇛ ★ ) + | TApp ht1 ht2 => kindOfRawHaskType ht1 >>= fun k1 => + kindOfRawHaskType ht2 >>= fun k2 => + match k1 with + | k1' ⇛ k2' => if eqd_dec k1' k1 then OK k2' else Error "kind mismatch" + | _ => Error "attempt to apply a non-functional kind" + end + | TFCApp tc rht' => Error "calculating kind of TFCApp is not yet implemented" + | TAll k t' => kindOfRawHaskType (t' k) >>= fun k' => OK (k ⇛ k') + | TCode t1 t2 => OK ★ +end. + +Definition kindITE (Γ:TypeEnv) : InstantiatedTypeEnv Kind Γ := + list2vec Γ. + +Definition kindOfType {Γ}(ht:HaskType Γ) : ???Kind := + kindOfRawHaskType (ht Kind (kindITE Γ)). + Definition WellKindedHaskType Γ (ht:HaskType Γ) κ := forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ. Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ). - - (* "decl", production for "axiom" *) Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type := { axd_τ : vec TV n -> RawHaskType TV ; axd_σ : vec TV n -> RawHaskType TV }. - - - Section WFCo. Context {TV:Type}. Context {CV:Type}. @@ -311,8 +410,7 @@ Section WFCo. Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ), @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> - @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=. -(* + @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop := | CoTVar':∀ Γ Δ t e c σ τ, (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t @@ -320,6 +418,7 @@ Section WFCo. | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t + (* | SComp :∀ Γ Δ t e γ n S σ τ κ, ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV), @@ -327,17 +426,15 @@ Section WFCo. ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) -> ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) -> e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t - + *) | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ , (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ)) -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t - | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ, (t ⊢ᴛy TApp σ₁ σ₂:κ)-> (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)-> (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) -> e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t - | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV), t ⊢ᴛy v TV t : κ -> (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) -> @@ -350,7 +447,6 @@ Section WFCo. | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )-> ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc) where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)). -*) End WFCo. Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) := @@ -358,9 +454,9 @@ Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:Hask @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)). Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b). - Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)). - Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18). +Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)). +Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18). Fixpoint update_ξ `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ := @@ -368,29 +464,3 @@ Fixpoint update_ξ | nil => ξ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v' end. - - - - - - - - - - - - - - - - -(* just like GHC's AltCon, but using PHOAS types and coercions *) -Record StrongCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := -{ scb_saci : @StrongAltConInfo _ tc -; scb_Γ : TypeEnv := app (vec2list (saci_ekinds scb_saci)) Γ -; scb_Δ : CoercionEnv scb_Γ -; scb_types : vec (LeveledHaskType (app (vec2list (saci_ekinds scb_saci)) Γ)) (saci_numExprVars scb_saci) -}. -Coercion scb_saci : StrongCaseBranch >-> StrongAltConInfo. -Implicit Arguments StrongCaseBranch [[n][Γ]]. - diff --git a/src/HaskWeak.v b/src/HaskWeak.v index ee2111c..31accd2 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -6,12 +6,13 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreLiterals. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCoreTypes. Require Import HaskWeakVars. +Require Import HaskWeakTypes. Inductive WeakExpr := | WEVar : WeakExprVar -> WeakExpr @@ -21,21 +22,23 @@ Inductive WeakExpr := | WECast : WeakExpr -> WeakCoercion -> WeakExpr | WENote : Note -> WeakExpr -> WeakExpr | WEApp : WeakExpr -> WeakExpr -> WeakExpr -| WETyApp : WeakExpr -> CoreType -> WeakExpr +| WETyApp : WeakExpr -> WeakType -> WeakExpr | WECoApp : WeakExpr -> WeakCoercion -> WeakExpr | WELam : WeakExprVar -> WeakExpr -> WeakExpr | WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr | WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr -(* the CoreType argument is used only when going back from Weak to Core; it lets us dodge a possibly-failing type calculation *) -| WEBrak : WeakTypeVar -> WeakExpr -> CoreType -> WeakExpr -| WEEsc : WeakTypeVar -> WeakExpr -> CoreType -> WeakExpr +(* the WeakType argument in WEBrak/WEEsc is used only when going back *) +(* from Weak to Core; it lets us dodge a possibly-failing type *) +(* calculation *) +| WEBrak : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr +| WEEsc : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr (* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *) | WECase : forall (scrutinee:WeakExpr) - (tbranches:CoreType) - {n:nat}(tc:TyCon n) - (type_params:vec CoreType n) + (tbranches:WeakType) + (tc:TyCon) + (type_params:list WeakType) (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)), WeakExpr. @@ -56,8 +59,8 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar := | WETyLam cv e => getWeakExprFreeVars e | WECoLam cv e => getWeakExprFreeVars e - (* the messy fixpoints below are required by Coq's termination conditions *) - | WECase scrutinee tbranches n tc type_params alts => + (* the messy fixpoints below are required by Coq's termination conditions; trust me, I tried to get rid of them *) + | WECase scrutinee tbranches tc type_params alts => mergeDistinctLists (getWeakExprFreeVars scrutinee) ( ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) {struct alts} : list WeakExprVar := @@ -65,7 +68,7 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar := | T_Leaf None => nil | T_Leaf (Some (DEFAULT,_,_,_,e)) => getWeakExprFreeVars e | T_Leaf (Some (LitAlt lit,_,_,_,e)) => getWeakExprFreeVars e - | T_Leaf (Some ((DataAlt _ _ _ _ _ dc), tvars, cvars, evars,e)) => removeFromDistinctList' evars (getWeakExprFreeVars e) + | T_Leaf (Some ((DataAlt dc), tvars, cvars, evars,e)) => removeFromDistinctList' evars (getWeakExprFreeVars e) | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2) end) alts)) | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) := @@ -90,74 +93,46 @@ Definition makeClosedExpression : WeakExpr -> WeakExpr := | cv::cvl' => WELam cv (closeExpression me cvl') end) me (getWeakExprFreeVars me). -(* messy first-order capture-avoiding substitution on CoreType's *) -Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) : CoreType := - match te with - | TyVarTy tv' => if eqd_dec tv tv' then tsubst else te - | AppTy t1 t2 => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst) - | FunTy t1 t2 => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst) - | ForAllTy tv' t => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst) - | PredTy (EqPred t1 t2) => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)) - | PredTy (IParam ip ty) => PredTy (IParam ip (replaceCoreVar ty tv tsubst)) - | PredTy (ClassP _ c lt) => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) := - match lt with - | nil => nil - | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t) - end) lt)) - | TyConApp _ tc lt => TyConApp tc ((fix replaceCoreDistinctList (lt:list CoreType) := - match lt with - | nil => nil - | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t) - end) lt) - end. +Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType := + (WTyCon (haskLiteralToTyCon lit)). (* calculate the CoreType of a WeakExpr *) -Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType := +Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType := match ce with | WEVar (weakExprVar v t) => OK t - | WELit lit => OK (haskLiteralToCoreType lit) - | WEApp e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' => + | WELit lit => OK (weakTypeOfLiteral lit) + | WEApp e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' => match t' with - | (TyConApp 2 tc (t1::t2::nil)) => - if (tyCon_eq tc ArrowTyCon) - then OK t2 - else Error ("found non-function type "+++(weakTypeToString t')+++" in EApp") + | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2 | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp") end - | WETyApp e t => coreTypeOfWeakExpr e >>= fun te => + | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => match te with - | ForAllTy v ct => OK (replaceCoreVar ct v t) + | WForAllTy v ct => OK (replaceWeakTypeVar ct v t) | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp") end - | WECoApp e co => coreTypeOfWeakExpr e >>= fun te => + | WECoApp e co => weakTypeOfWeakExpr e >>= fun te => match te with - | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) => - if (tyCon_eq tc ArrowTyCon) - then OK t3 - else Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp") + | WCoFunTy t1 t2 t => OK t | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp") end - | WELam (weakExprVar ev vt) e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon (vt::t'::nil)) - | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => match tv with weakTypeVar tvc _ => OK (ForAllTy tvc t') end - | WECoLam (weakCoerVar cv φ₁ φ₂) e => - coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon ((PredTy (EqPred φ₁ φ₂))::t'::nil)) - | WELet ev ve e => coreTypeOfWeakExpr e - | WELetRec rb e => coreTypeOfWeakExpr e - | WENote n e => coreTypeOfWeakExpr e + | WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t') + | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t') + | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t') + | WELet ev ve e => weakTypeOfWeakExpr e + | WELetRec rb e => weakTypeOfWeakExpr e + | WENote n e => weakTypeOfWeakExpr e | WECast e (weakCoercion t1 t2 _) => OK t2 - | WECase scrutinee tbranches n tc type_params alts => OK tbranches + | WECase scrutinee tbranches tc type_params alts => OK tbranches (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *) - | WEBrak ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ => - OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end - | WEEsc ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ => + | WEBrak ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t') + | WEEsc ec e _ => weakTypeOfWeakExpr e >>= fun t' => match t' with - | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) => - if (tyCon_eq tc hetMetCodeTypeTyCon) - then if eqd_dec ecc ec' then OK t'' + | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') => + if eqd_dec ec ec' then OK t'' else Error "level mismatch in escapification" - else Error "ill-typed escapification" | _ => Error "ill-typed escapification" - end end + end end. diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 6e6a87d..f0a8300 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -7,13 +7,15 @@ Require Import Preamble. Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreLiterals. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. 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". @@ -22,8 +24,8 @@ Variable sortAlts : forall {a}{b}, list (@triple AltCon a b) -> list (@triple A Extract Inlined Constant mkCoreLet => "sortAlts". Implicit Arguments sortAlts [[a][b]]. -Variable unsafeCoerce : CoreCoercion. - Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce". +Variable trustMeCoercion : CoreCoercion. + Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce". (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *) Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. @@ -31,14 +33,8 @@ Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. (* a dummy variable which is never referenced but needed for a binder *) Variable dummyVariable : CoreVar. - -Definition weakVarToCoreVar (wv:WeakVar) : CoreVar := -match wv with -| WExprVar (weakExprVar v _ ) => v -| WTypeVar (weakTypeVar v _ ) => v -| WCoerVar (weakCoerVar v _ _ ) => v -end. -Coercion weakVarToCoreVar : WeakVar >-> CoreVar. + (* FIXME this doesn't actually work *) + Extract Inlined Constant dummyVariable => "(Prelude.error ""dummyVariable"")". Section HaskWeakToCore. @@ -46,15 +42,16 @@ Section HaskWeakToCore. Context (hetmet_brak_var : CoreVar). Context (hetmet_esc_var : CoreVar). + (* FIXME: do something more intelligent here *) Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion := - fun _ => unsafeCoerce. + fun _ => trustMeCoercion. Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := match me with | WEVar (weakExprVar v _) => CoreEVar v | WELit lit => CoreELit lit | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2) - | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType t) + | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t)) | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co))) | WENote n e => CoreENote n (weakExprToCoreExpr e ) @@ -62,10 +59,12 @@ Section HaskWeakToCore. | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (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 t) - | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var) (CoreEType (TyVarTy ec))) (CoreEType t) + | 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)) | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e) - | WECase e tbranches n tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable tbranches + | WECase e tbranches tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable (weakTypeToCoreType tbranches) (sortAlts (( fix mkCaseBranches (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := @@ -73,7 +72,7 @@ Section HaskWeakToCore. | T_Leaf None => nil | T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2) | T_Leaf (Some (ac,tvars,cvars,evars,e)) => - (mkTriple ac + (mkTriple (ac:AltCon) (app (app (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars) (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars)) @@ -92,3 +91,5 @@ Section HaskWeakToCore. end. End HaskWeakToCore. + + diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v new file mode 100644 index 0000000..b295cf1 --- /dev/null +++ b/src/HaskWeakTypes.v @@ -0,0 +1,132 @@ +(*********************************************************************************************************************************) +(* HaskWeakTypes: types HaskWeak *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import HaskKinds. +Require Import HaskCoreLiterals. +Require Import HaskCoreVars. +Require Import HaskCoreTypes. + +(* TO DO: mark the TyCon used for hetmet as a "type family" so GHC keeps it fully-applied-at-all-times *) + +(* a WeakTypeVar merely wraps a CoreVar and includes its Kind *) +Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. + +(* + * WeakType is much like CoreType, but: + * 1. avoids mutually-inductive definitions + * 2. gives special cases for the tycons which have their own typing rules so we can pattern-match on them + * 3. separates type functions from type constructors, and uses a normal "AppTy" for applying the latter + *) +Inductive WeakType := +| WTyVarTy : WeakTypeVar -> WeakType +| WAppTy : WeakType -> WeakType -> WeakType +| WTyFunApp : TyCon -> list WeakType -> WeakType +| WTyCon : TyCon -> WeakType +| WFunTyCon : WeakType (* never use (WTyCon ArrowCon); always use this! *) +| WCodeTy : WeakTypeVar -> WeakType -> WeakType (* never use the raw tycon *) +| WCoFunTy : WeakType -> WeakType -> WeakType -> WeakType +| WForAllTy : WeakTypeVar -> WeakType -> WeakType +| WClassP : Class_ -> list WeakType -> WeakType +| WIParam : CoreIPName CoreName -> WeakType -> WeakType. + +(* EqDecidable instances for WeakType *) +Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar. + 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. + +(* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *) +Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". +Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". + +(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *) +Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) := + match wt with + | WTyCon tc => Some (tc,acc) + | WAppTy t1 t2 => isTyConApp t1 (t2::acc) + | _ => None + end. + +(* messy first-order NON-CAPTURE-AVOIDING substitution on WeakType's *) +Fixpoint replaceWeakTypeVar (te:WeakType)(tv:WeakTypeVar)(tsubst:WeakType) : WeakType := + match te with + | WTyVarTy tv' => if eqd_dec tv tv' then tsubst else te + | WAppTy t1 t2 => WAppTy (replaceWeakTypeVar t1 tv tsubst) (replaceWeakTypeVar t2 tv tsubst) + | WForAllTy tv' t => if eqd_dec tv tv' then te else WForAllTy tv' (replaceWeakTypeVar t tv tsubst) + | WCoFunTy t1 t2 t => WCoFunTy (replaceWeakTypeVar t1 tv tsubst) + (replaceWeakTypeVar t2 tv tsubst) (replaceWeakTypeVar t tv tsubst) + | WIParam ip ty => WIParam ip (replaceWeakTypeVar ty tv tsubst) + | WClassP c lt => WClassP c ((fix replaceCoreDistinctList (lt:list WeakType) := + match lt with + | nil => nil + | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t) + end) lt) + | WTyFunApp tc lt => WTyFunApp tc ((fix replaceCoreDistinctList (lt:list WeakType) := + match lt with + | nil => nil + | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t) + end) lt) + | WTyCon tc => WTyCon tc + | WFunTyCon => WFunTyCon + | WModalBoxTyCon => WModalBoxTyCon + end. + +(* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *) +Definition normalizeWeakType (wt:WeakType) : WeakType := wt. + +Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType := + match wt with + | WTyVarTy (weakTypeVar v _) => TyVarTy v + | 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 tc lt => TyConApp tc (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 weakTypeToCoreType (wt:WeakType) := + weakTypeToCoreType' (normalizeWeakType wt). + +Definition compare_weakTypes (w1 w2:WeakType) := + if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2) + then true + else false. + +(* Coq's "decide equality" can't cope here; we have to cheat for now *) +Axiom compare_weakTypes_axiom : forall w1 w2, if compare_weakTypes w1 w2 then w1=w2 else not (w1=w2). + +Instance EqDecidableWeakType : EqDecidable WeakType. + apply Build_EqDecidable. + intros. + set (compare_weakTypes_axiom v1 v2) as x. + set (compare_weakTypes v1 v2) as y. + assert (y=compare_weakTypes v1 v2). reflexivity. + destruct y; rewrite <- H in x. + left; auto. + right; auto. + Defined. + +Definition weakTypeToString : WeakType -> string := + coreTypeToString ○ weakTypeToCoreType. + diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 2e242c8..782c2a2 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -7,49 +7,47 @@ Require Import Preamble. Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import HaskKinds. +Require Import HaskCoreLiterals. Require Import HaskCoreVars. Require Import HaskCoreTypes. +Require Import HaskWeakTypes. -Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. +(* TO DO: finish this *) +Inductive WeakCoercion : Type := weakCoercion : WeakType -> WeakType -> CoreCoercion -> WeakCoercion. -Inductive WeakCoercion : Type := weakCoercion : CoreType -> CoreType -> CoreCoercion -> WeakCoercion. +(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *) +Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar. -Inductive WeakCoerVar := weakCoerVar : CoreVar -> CoreType -> CoreType -> WeakCoerVar. - -Inductive WeakExprVar := weakExprVar : CoreVar -> CoreType -> WeakExprVar. +(* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *) +Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar. +(* a WeakVar is one of the three sorts *) Inductive WeakVar : Type := | WExprVar : WeakExprVar -> WeakVar | WTypeVar : WeakTypeVar -> WeakVar | WCoerVar : WeakCoerVar -> WeakVar. -Coercion WExprVar : WeakExprVar >-> WeakVar. -Coercion WTypeVar : WeakTypeVar >-> WeakVar. -Coercion WCoerVar : WeakCoerVar >-> WeakVar. - - -Definition haskLiteralToCoreType lit : CoreType := - TyConApp (haskLiteralToTyCon lit) nil. - -Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt. - -Definition weakTypeToString : CoreType -> string := - coreTypeToString ○ weakTypeToCoreType. + Coercion WExprVar : WeakExprVar >-> WeakVar. + Coercion WTypeVar : WeakTypeVar >-> WeakVar. + Coercion WCoerVar : WeakCoerVar >-> WeakVar. + +Definition weakTypeVarToKind (tv:WeakTypeVar) : Kind := + match tv with weakTypeVar _ k => k end. + Coercion weakTypeVarToKind : WeakTypeVar >-> Kind. + +Definition weakVarToCoreVar (wv:WeakVar) : CoreVar := + match wv with + | WExprVar (weakExprVar v _ ) => v + | WTypeVar (weakTypeVar v _ ) => v + | WCoerVar (weakCoerVar v _ _ ) => v + end. + Coercion weakVarToCoreVar : WeakVar >-> CoreVar. + +Definition haskLiteralToWeakType lit : WeakType := + WTyCon (haskLiteralToTyCon lit). + Coercion haskLiteralToWeakType : HaskLiteral >-> WeakType. (* EqDecidable instances for all of the above *) -Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar. - 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 WeakCoerVarEqDecidable : EqDecidable WeakCoerVar. apply Build_EqDecidable. intros. @@ -87,7 +85,3 @@ Instance WeakVarEqDecidable : EqDecidable WeakVar. left; auto. right; intro X; apply n; inversion X; auto. Defined. - - - - diff --git a/src/Main.v b/src/Main.v deleted file mode 100644 index bbadc14..0000000 --- a/src/Main.v +++ /dev/null @@ -1,23 +0,0 @@ -Require Import Preamble. -Require Import General. - -Require Import NaturalDeduction. -Require Import NaturalDeductionToLatex. - -Require Import HaskGeneral. -Require Import HaskLiterals. -Require Import HaskCoreVars. -Require Import HaskCoreTypes. -Require Import HaskCore. -Require Import HaskWeakVars. -Require Import HaskWeak. -Require Import HaskCoreToWeak. -Require Import HaskStrongTypes. -Require Import HaskStrong. -Require Import HaskProof. -(*Require Import HaskProofToStrong.*) -(*Require Import HaskStrongToProof.*) -(*Require Import HaskStrongToWeak.*) -(*Require Import HaskWeakToStrong.*) -Require Import HaskWeakToCore. -Require Import HaskProofToLatex. diff --git a/src/Preamble.v b/src/Preamble.v index 026d6d1..6abdd71 100644 --- a/src/Preamble.v +++ b/src/Preamble.v @@ -91,7 +91,7 @@ Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99). Reserved Notation "Γ '+' x : c" (at level 50, x at level 99). Reserved Notation "Γ '++' x : a ∼ b" (at level 50, x at level 99). -Reserved Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" (at level 11, φ₂ at level 99, right associativity). +Reserved Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" (at level 11, φ₂ at level 99, right associativity). Reserved Notation "Γ > past : present '⊢ᴇ' succedent" (at level 52, past at level 99, present at level 50, succedent at level 50).