Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
gaTy TV ec
- (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc)))
- (ga_mk_tree' ec ( mapOptionTree drop_arg_types suc) ).
+ (ga_mk_tree' ec ant)
+ (ga_mk_tree' ec suc).
- Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
- fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc).
+ Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+ fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
(*
* The story:
| 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 :=
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)
- (mapOptionTree flatten_type (take_arg_types_as_tree Γ t))
+ (mapOptionTree flatten_type (take_arg_types_as_tree t))
[ flatten_type (drop_arg_types_as_tree t)].
-
intros.
unfold flatten_type at 1.
simpl.
unfold ga_mk.
+ apply extensionality.
+ intros.
unfold v2t.
- admit. (* BIG HUGE CHEAT FIXME *)
+ unfold ga_mk_raw.
+ unfold ga_mk_tree.
+ rewrite <- mapOptionTree_compose.
+ unfold take_arg_types_as_tree.
+ 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))))
+ with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
+ (unleaves
+ (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
+ (fun TV : Kind → Type => take_arg_types ○ t TV))))).
+ reflexivity.
+ unfold flatten_type.
+ clear hetmet_flatten.
+ clear hetmet_unflatten.
+ clear hetmet_id.
+ clear gar.
+ set (t tv ite) as x.
+ admit.
+ admit.
Qed.
Definition flatten_proof :
simpl.
destruct lev.
drop_simplify.
- set (drop_lev (ec :: nil) (take_arg_types_as_tree Γ t @@@ (ec :: nil))) as empty_tree.
+ set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
take_simplify.
rewrite take_lemma'.
simpl.
rewrite krunk.
set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
- set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args.
+ set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
unfold empty_tree.
eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
clear e.
set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
- set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args.
+ set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
Defined.
+ Definition skolemize_and_flatten_proof :
+ forall {h}{c},
+ ND Rule h c ->
+ ND Rule
+ (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
+ (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
+ intros.
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ apply flatten_proof.
+ apply skolemize_proof.
+ apply X.
+ Defined.
+
(* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
* calculate it, and show that the flattening procedure above drives it down by one *)