X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=a5f42618b89ea2de829e7cb8e842ee82870c7510;hp=46e6af587aacd66728a8ab7c2fae454d2a77bfdc;hb=bebffa435dbc5afd126f6972fbf220977455854d;hpb=4a32fb619ddda1fedb0855a0c7acad0a41704da8 diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 46e6af5..a5f4261 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -239,11 +239,11 @@ Section HaskFlattener. Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ := gaTy TV ec - (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc))) - (ga_mk_tree' ec ( mapOptionTree drop_arg_types suc) ). + (ga_mk_tree' ec ant) + (ga_mk_tree' ec suc). - Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := - fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc). + Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := + fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite). (* * The story: @@ -260,7 +260,7 @@ Section HaskFlattener. | 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 := @@ -538,6 +538,7 @@ Section HaskFlattener. (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 _ _ _ _ _ @@ -592,6 +593,7 @@ Section HaskFlattener. 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 _ @@ -621,6 +623,7 @@ Section HaskFlattener. apply nd_rule. apply RArrange. induction r; simpl. + apply RId. apply RCanL. apply RCanR. apply RuCanL. @@ -719,24 +722,116 @@ Section HaskFlattener. 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. @@ -760,6 +855,7 @@ Section HaskFlattener. apply RLeft. apply RWeak. apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported"). +*) Defined. Lemma mapOptionTree_distributes @@ -768,32 +864,6 @@ Section HaskFlattener. 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. @@ -855,15 +925,36 @@ Section HaskFlattener. Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t, flatten_type (<[ ec |- t ]>) = @ga_mk Γ (v2t ec) - (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) + (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 : @@ -1136,7 +1227,7 @@ Section HaskFlattener. simpl. destruct lev. drop_simplify. - set (drop_lev (ec :: nil) (take_arg_types_as_tree Γ t @@@ (ec :: nil))) as empty_tree. + set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree. take_simplify. rewrite take_lemma'. simpl. @@ -1149,7 +1240,7 @@ Section HaskFlattener. rewrite krunk. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest. - set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args. + set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. unfold empty_tree. eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ]. refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _). @@ -1183,7 +1274,7 @@ Section HaskFlattener. clear e. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. - set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args. + set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. @@ -1222,6 +1313,20 @@ Section HaskFlattener. apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported"). Defined. + Definition skolemize_and_flatten_proof : + forall {h}{c}, + ND Rule h c -> + ND Rule + (mapOptionTree (flatten_judgment ○ skolemize_judgment) h) + (mapOptionTree (flatten_judgment ○ skolemize_judgment) c). + intros. + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + apply flatten_proof. + apply skolemize_proof. + apply X. + Defined. + (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to * calculate it, and show that the flattening procedure above drives it down by one *)