projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
more efficient encoding of function types
[coq-hetmet.git]
/
src
/
HaskFlattener.v
diff --git
a/src/HaskFlattener.v
b/src/HaskFlattener.v
index
09f7070
..
ed3ca43
100644
(file)
--- a/
src/HaskFlattener.v
+++ b/
src/HaskFlattener.v
@@
-260,7
+260,7
@@
Section HaskFlattener.
| TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
| TArrow => TArrow
| TCode ec e => let e' := flatten_rawtype e
| TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
| TArrow => TArrow
| TCode ec e => let e' := flatten_rawtype e
- in ga_mk_raw ec (unleaves (take_arg_types e')) [drop_arg_types e']
+ in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
| TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
end
with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
| TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
end
with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
@@
-538,6
+538,7
@@
Section HaskFlattener.
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
with
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
with
+ | RId a => let case_RId := tt in ga_id _ _ _ _ _
| RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
| RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
| RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
| RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
| RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
| RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
@@
-592,6
+593,7
@@
Section HaskFlattener.
match r as R in Arrange A B return
Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
(mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
match r as R in Arrange A B return
Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
(mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
+ | RId a => let case_RId := tt in RId _
| RCanL a => let case_RCanL := tt in RCanL _
| RCanR a => let case_RCanR := tt in RCanR _
| RuCanL a => let case_RuCanL := tt in RuCanL _
| RCanL a => let case_RCanL := tt in RCanL _
| RCanR a => let case_RCanR := tt in RCanR _
| RuCanL a => let case_RuCanL := tt in RuCanL _
@@
-621,6
+623,7
@@
Section HaskFlattener.
apply nd_rule.
apply RArrange.
induction r; simpl.
apply nd_rule.
apply RArrange.
induction r; simpl.
+ apply RId.
apply RCanL.
apply RCanR.
apply RuCanL.
apply RCanL.
apply RCanR.
apply RuCanL.
@@
-852,9
+855,6
@@
Section HaskFlattener.
apply IHt2.
Defined.
apply IHt2.
Defined.
- Axiom extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
- (forall tv ite, f tv ite = g tv ite) -> f=g.
-
Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
flatten_type (<[ ec |- t ]>)
= @ga_mk Γ (v2t ec)
Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
flatten_type (<[ ec |- t ]>)
= @ga_mk Γ (v2t ec)
@@
-864,7
+864,7
@@
Section HaskFlattener.
unfold flatten_type at 1.
simpl.
unfold ga_mk.
unfold flatten_type at 1.
simpl.
unfold ga_mk.
- apply extensionality.
+ apply phoas_extensionality.
intros.
unfold v2t.
unfold ga_mk_raw.
intros.
unfold v2t.
unfold ga_mk_raw.
@@
-874,9
+874,9
@@
Section HaskFlattener.
simpl.
replace (flatten_type (drop_arg_types_as_tree t) tv ite)
with (drop_arg_types (flatten_rawtype (t tv ite))).
simpl.
replace (flatten_type (drop_arg_types_as_tree t) tv ite)
with (drop_arg_types (flatten_rawtype (t tv ite))).
- replace (unleaves (take_arg_types (flatten_rawtype (t tv ite))))
+ replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
- (unleaves
+ (unleaves_
(take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
(fun TV : Kind → Type => take_arg_types ○ t TV))))).
reflexivity.
(take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
(fun TV : Kind → Type => take_arg_types ○ t TV))))).
reflexivity.