| TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
| TArrow => TArrow
| TCode ec e => let e' := flatten_rawtype e
- in ga_mk_raw ec (unleaves' (take_arg_types e')) [drop_arg_types e']
+ in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
| TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
end
with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
with
+ | RId a => let case_RId := tt in ga_id _ _ _ _ _
| RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
| RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
| RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
match r as R in Arrange A B return
Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
(mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
+ | RId a => let case_RId := tt in RId _
| RCanL a => let case_RCanL := tt in RCanL _
| RCanR a => let case_RCanR := tt in RCanR _
| RuCanL a => let case_RuCanL := tt in RuCanL _
apply nd_rule.
apply RArrange.
induction r; simpl.
+ apply RId.
apply RCanL.
apply RCanR.
apply RuCanL.
apply IHsucc2.
Defined.
+ Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+ t = mapTree (fun _:A => None) q ->
+ Arrange t [].
+ intros T A q.
+ induction q; intros.
+ simpl in H.
+ rewrite H.
+ apply RId.
+ simpl in *.
+ destruct t; try destruct o; inversion H.
+ set (IHq1 _ H1) as x1.
+ set (IHq2 _ H2) as x2.
+ eapply RComp.
+ eapply RRight.
+ rewrite <- H1.
+ apply x1.
+ eapply RComp.
+ apply RCanL.
+ rewrite <- H2.
+ apply x2.
+ Defined.
+
+(* Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
+ t = mapTree (fun _:A => None) q ->
+ Arrange [] t.
+ Defined.*)
+
+ Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
+ sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
+ intro T.
+ refine (fix foo t :=
+ match t with
+ | T_Leaf x => _
+ | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
+ end).
+ intros.
+ destruct x.
+ right; apply tt.
+ left.
+ exists (T_Leaf tt).
+ auto.
+ destruct b1'.
+ destruct b2'.
+ destruct s.
+ destruct s0.
+ subst.
+ left.
+ exists (x,,x0).
+ reflexivity.
+ right; auto.
+ right; auto.
+ Defined.
+
Definition arrange_esc : forall Γ Δ ec succ t,
ND Rule
[Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]
[Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
[(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]].
intros.
- unfold drop_lev.
set (@arrange _ succ (levelMatch (ec::nil))) as q.
+ set (@drop_lev Γ (ec::nil) succ) as q'.
+ assert (@drop_lev Γ (ec::nil) succ=q') as H.
+ reflexivity.
+ unfold drop_lev in H.
+ unfold mkDropFlags in H.
+ rewrite H in q.
+ clear H.
set (arrangeMap _ _ flatten_leveled_type q) as y.
eapply nd_comp.
eapply nd_rule.
eapply RArrange.
apply y.
- idtac.
clear y q.
+ set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
+ destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
+ destruct s.
+
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+ set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply q'' ].
+ clear q''.
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ apply nd_prod.
+ apply nd_rule.
+ apply RArrange.
+ eapply RComp; [ idtac | apply RCanR ].
+ apply RLeft.
+ apply (@arrange_empty_tree _ _ _ _ e).
+
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply (@RVar Γ Δ t nil).
+ apply nd_rule.
+ apply RArrange.
+ eapply RComp.
+ apply RuCanL.
+ apply RRight.
+ apply RWeak.
+(*
+ eapply decide_tree_empty.
+
+ simpl.
+ set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
+ destruct (decide_tree_empty escapified).
+
induction succ.
destruct a.
+ unfold drop_lev.
destruct l.
simpl.
unfold mkDropFlags; simpl.
apply RLeft.
apply RWeak.
apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
+*)
Defined.
Lemma mapOptionTree_distributes
reflexivity.
Qed.
- Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
- sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
- intro T.
- refine (fix foo t :=
- match t with
- | T_Leaf x => _
- | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
- end).
- intros.
- destruct x.
- right; apply tt.
- left.
- exists (T_Leaf tt).
- auto.
- destruct b1'.
- destruct b2'.
- destruct s.
- destruct s0.
- subst.
- left.
- exists (x,,x0).
- reflexivity.
- right; auto.
- right; auto.
- Defined.
-
Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
intros.
induction t.
= @ga_mk Γ (v2t ec)
(mapOptionTree flatten_type (take_arg_types_as_tree t))
[ flatten_type (drop_arg_types_as_tree t)].
-
intros.
unfold flatten_type at 1.
simpl.
unfold ga_mk.
+ apply phoas_extensionality.
+ intros.
unfold v2t.
- admit. (* BIG HUGE CHEAT FIXME *)
+ unfold ga_mk_raw.
+ unfold ga_mk_tree.
+ rewrite <- mapOptionTree_compose.
+ unfold take_arg_types_as_tree.
+ simpl.
+ replace (flatten_type (drop_arg_types_as_tree t) tv ite)
+ with (drop_arg_types (flatten_rawtype (t tv ite))).
+ replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
+ with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
+ (unleaves_
+ (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
+ (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.
+ admit.
Qed.
Definition flatten_proof :
projects / coq-hetmet.git / blobdiff