- Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
- match tt with
- | T_Leaf None => unit
- | T_Leaf (Some x) => x
- | T_Branch b1 b2 => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
- end.
-
- Set Printing Width 130.
-
- Context (hetmet_flatten : WeakExprVar).
- Context (hetmet_id : WeakExprVar).
- Context {unitTy : forall TV, RawHaskType TV ★ }.
- Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
- Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
-
- Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
- fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
-
- Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
- fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
-
- Class garrow :=
- { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
- ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
- ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
- ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
- ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
- ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
- ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
- ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
- ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
- ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
- ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
- ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
- ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
- ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
- ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ]
- ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule []
- [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
- ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
- [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
- [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
- }.
- Context `(gar:garrow).
-
- Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
-
- (*
- * The story:
- * - code types <[t]>@c become garrows c () t
- * - free variables of type t at a level lev deeper than the succedent become garrows c () t
- * - free variables at the level of the succedent become
- *)
- Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
- match exp with
- | TVar _ x => TVar x
- | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes (y v))
- | TApp _ _ x y => TApp (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y)
- | TCon tc => TCon tc
- | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
- (garrowfy_raw_codetypes t)
- | TArrow => TArrow
- | TCode v e => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
- | TyFunApp tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
- end
- with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
- match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
- | TyFunApp_nil => TyFunApp_nil
- | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest)
- end.
- Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
- fun TV ite =>
- garrowfy_raw_codetypes (ht TV ite).
-
- Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite).
-
- Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
- match lev with
- | nil => garrowfy_code_types ht
- | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev']
- end.
-
- Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
- match ht with
- htt @@ lev =>
- garrowfy_leveled_code_types' htt lev @@ nil
- end.