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
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))
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.
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 *)
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).
+Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
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.
| 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.
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.
(* 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".
(*********************************************************************************************************************************)
-(* 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".
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
| 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" ].
-
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
| _ => 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
| 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)
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
| 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
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.
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)".
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 }.
+++ /dev/null
-(*********************************************************************************************************************************)
-(* 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 }.
--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
+
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
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 *)
| 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.
| 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)
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.
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)
| 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.
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.
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)
| 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
.
End HaskStrong.
-Implicit Arguments StrongCaseBranchWithVVs [[n][Γ]].
\ No newline at end of file
+Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
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.
(* 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.
| 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 (* ◯ *)
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)).
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 *)
| 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).
-(* 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).
-(* 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.
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.
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 *)
| 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)
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}.
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
| 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),
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) ->
| 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 Γ) :=
@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 Γ :=
| 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][Γ]].
-
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
| 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.
| 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 :=
| 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) :=
| 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.
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".
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.
(* 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.
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 )
| 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)) :=
| 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))
end.
End HaskWeakToCore.
+
+
--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
+
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.
left; auto.
right; intro X; apply n; inversion X; auto.
Defined.
-
-
-
-
+++ /dev/null
-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.
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).
projects / coq-hetmet.git / commitdiff