(*******************************************************************************)
- Context (hetmet_flatten : WeakExprVar).
- Context (hetmet_unflatten : WeakExprVar).
- Context (hetmet_id : WeakExprVar).
Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
(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.
rename l into g.
rename σ into l.
destruct l as [|ec lev]; simpl.
+ (*
destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
set (flatten_type (g wev)) as t.
set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
apply nd_rule.
apply q.
apply INil.
+ *)
unfold flatten_leveled_type. simpl.
apply nd_rule; rewrite globals_do_not_have_code_types.
apply RGlobal.
reflexivity.
destruct case_RCase.
- simpl.
- apply (Prelude_error "Case not supported (BIG FIXME)").
+ destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
+ apply nd_rule.
+ rewrite <- mapOptionTree_compose.
+ replace (mapOptionTree
+ (fun x => flatten_judgment (pcb_judg (snd x)))
+ alts,, [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [flatten_type (caseType tc avars)] @ nil])
+ with
+ (mapOptionTree
+ (fun x => @pcb_judg tc Γ Δ nil (flatten_type tbranches) avars (fst x) (snd x))
+ alts,,
+ [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [caseType tc avars] @ nil]).
+ replace (mapOptionTree flatten_leveled_type
+ (mapOptionTreeAndFlatten
+ (fun x => (snd x)) alts))
+ with (mapOptionTreeAndFlatten
+ (fun x =>
+ (snd x)) alts).
+ apply RCase.
+ admit.
+ admit.
destruct case_SBrak.
simpl.