projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
cb42497
)
abstract out the kind of environment classifiers (ECKind)
author
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 9 May 2011 04:35:56 +0000
(21:35 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 9 May 2011 04:35:56 +0000
(21:35 -0700)
src/ExtractionMain.v
patch
|
blob
|
history
src/HaskFlattener.v
patch
|
blob
|
history
src/HaskKinds.v
patch
|
blob
|
history
src/HaskProofToLatex.v
patch
|
blob
|
history
src/HaskStrongTypes.v
patch
|
blob
|
history
src/HaskWeakToStrong.v
patch
|
blob
|
history
diff --git
a/src/ExtractionMain.v
b/src/ExtractionMain.v
index
58bc13e
..
e628f26
100644
(file)
--- a/
src/ExtractionMain.v
+++ b/
src/ExtractionMain.v
@@
-335,13
+335,13
@@
Section core2proof.
Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil.
Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil.
Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
- Definition ga_type {TV}(a b c:RawHaskType TV ★) : RawHaskType TV ★ :=
+ Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
TApp (TApp (TApp (@TyFunApp TV
hetmet_PGArrowTyCon
nil _ TyFunApp_nil) a) b) c.
Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
TApp (TApp (TApp (@TyFunApp TV
hetmet_PGArrowTyCon
nil _ TyFunApp_nil) a) b) c.
Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
- Definition ga_type' {Γ}(a b c:HaskType Γ ★) : HaskType Γ ★ :=
+ Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
fun TV ite => TApp (TApp (TApp (@TyFunApp TV
hetmet_PGArrowTyCon
nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
fun TV ite => TApp (TApp (TApp (@TyFunApp TV
hetmet_PGArrowTyCon
nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
diff --git
a/src/HaskFlattener.v
b/src/HaskFlattener.v
index
6d9d7a6
..
60a205f
100644
(file)
--- a/
src/HaskFlattener.v
+++ b/
src/HaskFlattener.v
@@
-196,12
+196,12
@@
Section HaskFlattener.
Context {unitTy : forall TV, RawHaskType TV ★ }.
Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
Context {unitTy : forall TV, RawHaskType TV ★ }.
Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
- Context {gaTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
+ Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
- Definition ga_mk {Γ}(ec:HaskType Γ ★ )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+ Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
Class garrow :=
fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
Class garrow :=
@@
-257,7
+257,7
@@
Section HaskFlattener.
fun TV ite =>
garrowfy_raw_codetypes (ht TV ite).
fun TV ite =>
garrowfy_raw_codetypes (ht TV ite).
- Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
+ Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite).
Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
match lev with
Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
match lev with
@@
-509,7
+509,7
@@
Section HaskFlattener.
*)
Definition garrowfy_arrangement' :
forall Γ (Δ:CoercionEnv Γ)
*)
Definition garrowfy_arrangement' :
forall Γ (Δ:CoercionEnv Γ)
- (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
+ (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
intros Γ Δ ec lev.
ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
intros Γ Δ ec lev.
@@
-554,7
+554,7
@@
Section HaskFlattener.
Definition garrowfy_arrangement :
forall Γ (Δ:CoercionEnv Γ) n
Definition garrowfy_arrangement :
forall Γ (Δ:CoercionEnv Γ) n
- (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
+ (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
ND Rule
[Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
|- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
ND Rule
[Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
|- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
diff --git
a/src/HaskKinds.v
b/src/HaskKinds.v
index
3539e95
..
2200f51
100644
(file)
--- a/
src/HaskKinds.v
+++ b/
src/HaskKinds.v
@@
-37,6
+37,10
@@
Instance KindToString : ToString Kind := { toString := kindToString }.
Notation "'★'" := KindStar.
Notation "a ⇛ b" := (KindArrow a b).
Notation "'★'" := KindStar.
Notation "a ⇛ b" := (KindArrow a b).
+(* the kind of environment classifiers *)
+Definition ECKind := ★ .
+Opaque ECKind.
+
Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
match k with
| ★ => rawLatexMath "\star"
Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
match k with
| ★ => rawLatexMath "\star"
diff --git
a/src/HaskProofToLatex.v
b/src/HaskProofToLatex.v
index
edac1aa
..
0d33b0a
100644
(file)
--- a/
src/HaskProofToLatex.v
+++ b/
src/HaskProofToLatex.v
@@
-126,7
+126,7
@@
Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS
| nil => t''
| lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
(fold_left (fun x y => x+++(rawLatexMath ":")+++y)
| nil => t''
| lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
(fold_left (fun x y => x+++(rawLatexMath ":")+++y)
- (map (fun l:HaskTyVar Γ ★ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
+ (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
end
end); try apply ConcatenableLatexMath.
try apply VarNameMonad.
end
end); try apply ConcatenableLatexMath.
try apply VarNameMonad.
diff --git
a/src/HaskStrongTypes.v
b/src/HaskStrongTypes.v
index
7ce04fb
..
aafbe9b
100644
(file)
--- a/
src/HaskStrongTypes.v
+++ b/
src/HaskStrongTypes.v
@@
-68,7
+68,7
@@
Section Raw.
| TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
| TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
| TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
| TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
| TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
| TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
- | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
+ | TCode : RawHaskType ECKind -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
| TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* S_n *)
with RawHaskTypeList : list Kind -> Type :=
| TyFunApp_nil : RawHaskTypeList nil
| TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* S_n *)
with RawHaskTypeList : list Kind -> Type :=
| TyFunApp_nil : RawHaskTypeList nil
@@
-131,7
+131,7
@@
Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:Coer
(* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
(* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
-Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ★).
+Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ECKind).
Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
@@
-159,7
+159,7
@@
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 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 Γ ★:=
+Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
:= fun TV ite => TCon tc.
fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
:= fun TV ite => TCon tc.
diff --git
a/src/HaskWeakToStrong.v
b/src/HaskWeakToStrong.v
index
b9ac068
..
122db2a
100644
(file)
--- a/
src/HaskWeakToStrong.v
+++ b/
src/HaskWeakToStrong.v
@@
-124,7
+124,8
@@
Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
| WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
| WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
| WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
| WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
| WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
| WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
- | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
+ | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
+ >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
| WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
weakTypeToType _ φ t1 >>= fun t1' =>
weakTypeToType _ φ t2 >>= fun t2' =>
| WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
weakTypeToType _ φ t1 >>= fun t1' =>
weakTypeToType _ φ t2 >>= fun t2' =>