Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
@TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
+
Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
- TApp (TApp (@TyFunApp TV hetmet_PGArrow_tensor_TyCon (ECKind::nil) _ (TyFunApp_cons _ _ ec TyFunApp_nil)) a) b.
+ (@TyFunApp TV
+ hetmet_PGArrow_tensor_TyCon
+ (ECKind::★ ::★ ::nil) ★
+ (TyFunApp_cons _ _ ec
+ (TyFunApp_cons _ _ a
+ (TyFunApp_cons _ _ b
+ TyFunApp_nil)))).
+
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).
Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
(addErrorMessage ("HaskStrong...")
- (let haskProof := flatten_proof hetmet_flatten' hetmet_unflatten'
+ (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
in (* insert HaskProof-to-HaskProof manipulations here *)
OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
hetmet_pga_applyr
hetmet_pga_curryl
*)
+
.
End core2proof.
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:
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.
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 *)
end
end.
- Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
- intros.
- induction Γ.
- apply INil.
- apply ICons; auto.
- apply tt.
- Defined.
-
- Fixpoint grab (n:nat) {T} (l:list T) : T :=
- match l with
- | nil => Prelude_error "grab failed"
- | h::t => match n with
- | 0 => h
- | S n' => grab n' t
- end
- end.
+ Fixpoint take_trustme {Γ}
+ (n:nat)
+ (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
+ : list (HaskType Γ ★) :=
- Fixpoint count' (n:nat)(ln:list nat) : list nat :=
match n with
- | 0 => ln
- | S n' => count' n' (n'::ln)
+ | 0 => nil
+ | S n' => (fun TV ite => match l TV ite with
+ | nil => Prelude_error "impossible"
+ | a::b => a
+ end)
+ ::
+ take_trustme n' (fun TV ite => match l TV ite with
+ | nil => Prelude_error "impossible"
+ | a::b => b
+ end)
end.
-
- Definition count (n:nat) := count' n nil.
-
- Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) :=
- map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))).
-
- Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) :=
- (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))).
+
+ Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
+ unleaves
+ (take_trustme
+ (count_arg_types (ht _ (ite_unit _)))
+ (fun TV ite => take_arg_types (ht TV ite))).
Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
fun TV ite => drop_arg_types (ht TV ite).
Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★),
take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2).
intros.
- unfold take_arg_types_as_tree; simpl.
- unfold rebundle at 1.
+ unfold take_arg_types_as_tree at 1.
+ simpl.
admit.
Qed.
left; auto.
Defined.
+ Opaque take_arg_types_as_tree.
Definition skolemize_proof :
forall {h}{c},
ND Rule h c ->
apply RGlobal.
destruct case_RLam.
- simpl.
destruct lev.
- apply nd_rule.
- apply SFlat.
- apply RLam.
+ apply nd_rule.
+ apply SFlat.
+ simpl.
+ apply RLam.
+ simpl.
rewrite take_works.
rewrite drop_works.
apply nd_rule.
- apply SFlat.
- apply RArrange.
- apply RCossa.
+ apply SFlat.
+ apply RArrange.
+ apply RCossa.
destruct case_RCast.
simpl.
simpl.
apply (Prelude_error "CASE: BIG FIXME").
Defined.
+ Transparent take_arg_types_as_tree.
End HaskSkolemizer.
| _ => nil
end.
+Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
+ match exp as E in RawHaskType _ K return nat with
+ | TApp κ₁ κ₂ x y =>
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
+ | KindStar => fun x' =>
+ match x' return nat -> nat with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun a b => S b
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end x''
+ | _ => fun _ => 0
+ end
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end) x (count_arg_types y)
+ | _ => 0
+ end.
+
+ Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
+ intros.
+ induction Γ.
+ apply INil.
+ apply ICons; auto.
+ apply tt.
+ Defined.
+
+Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
+ fun pf =>
+ fun TV ite =>
+ match take_arg_types (ht TV ite) with
+ | nil => Prelude_error "impossible"
+ | x::y => x
+ end.
+
(* From (t1->(t2->(t3-> ... t))), return t *)
(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
projects / coq-hetmet.git / commitdiff