Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
ND Rule
[ Γ > Δ > Σ |- [a ---> s @@ lev ] ]
- [ Γ > Δ > Σ,,[a @@ lev] |- [ s @@ lev ] ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ].
- eapply nd_comp; [ apply nd_llecnac | idtac ].
+ [ Γ > Δ > [a @@ lev],,Σ |- [ s @@ lev ] ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
+ apply nd_id.
apply nd_rule.
apply RVar.
- apply nd_id.
Defined.
Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
intro pf.
eapply nd_comp.
apply pf.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
apply curry.
Defined.
Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
- ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ].
+ ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ].
intro pf.
eapply nd_comp.
eapply pf.
eapply nd_comp.
eapply nd_rule.
eapply RArrange.
- eapply RCanL.
+ eapply RCanR.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
apply curry.
Defined.
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.