-(*
- Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ toString ce)
- (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
- coreExprToWeakExpr ce >>= fun we =>
- addErrorMessage ("WeakExpr: " +++ toString we)
- ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
- ((weakTypeOfWeakExpr we) >>= fun t =>
- (addErrorMessage ("WeakType: " +++ toString t)
- ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
- addErrorMessage ("HaskType: " +++ toString τ)
- ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
- (let haskProof := @expr2proof _ _ _ _ _ _ e
- in (* insert HaskProof-to-HaskProof manipulations here *)
- (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
- >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
-(*
- >>= fun e' =>
- Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
- *)
-)
-)))))))).
-(* Error "X").*)
-(*
- strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
- (projT2 e')
- INil
- >>= fun q => Error (toString q)
- ))))))))).
-*)*)
-
-
- Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ toString ce)
- (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
- coreExprToWeakExpr ce >>= fun we =>
+ Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
+ : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
+ apply nd_rule.
+ refine (@RGlobal Γ Δ l
+ {| glob_wv := coreVarToWeakExprVarOrError cv
+ ; glob_kinds := κ₁ :: κ₂ :: nil
+ ; glob_tf := mkGlob2'(Γ:=Γ) f
+ |} (ICons _ _ x (ICons _ _ y INil))).
+ Defined.
+
+ Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
+ IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
+ intros.
+ inversion X; subst.
+ inversion X1; subst.
+ inversion X3; subst.
+ apply f; auto.
+ Defined.
+
+ Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
+ : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
+ apply nd_rule.
+ refine (@RGlobal Γ Δ l
+ {| glob_wv := coreVarToWeakExprVarOrError cv
+ ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
+ ; glob_tf := mkGlob3'(Γ:=Γ) f
+ |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
+ Defined.
+
+ Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
+ IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
+ intros.
+ inversion X; subst.
+ inversion X1; subst.
+ inversion X3; subst.
+ inversion X5; subst.
+ apply f; auto.
+ Defined.
+
+ Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
+ : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
+ apply nd_rule.
+ refine (@RGlobal Γ Δ l
+ {| glob_wv := coreVarToWeakExprVarOrError cv
+ ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
+ ; glob_tf := mkGlob4'(Γ:=Γ) f
+ |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
+ Defined.
+
+ Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
+
+ Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
+ { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
+ ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
+ ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
+ ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
+ ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
+ ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+ ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+ ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat ec a) (gat ec b)
+ ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
+ ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
+ ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+ ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+ ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
+(* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
+(* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
+(* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
+(* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
+ ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
+ ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
+ ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
+ ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
+ }.
+
+ Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
+ Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
+ Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
+ Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
+ Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
+
+ Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+ addErrorMessage ("input CoreSyn: " +++ toString cex)
+ (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
+ coreExprToWeakExpr cex >>= fun we =>