Require Import HaskCoreVars.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskProof.
Require Import NaturalDeduction.
Require Import HaskWeakToStrong.
Open Scope nd_scope.
+Set Printing Width 130.
(*
* The flattening transformation. Currently only TWO-level languages are
*)
Section HaskFlattener.
- Inductive TreeFlags {T:Type} : Tree T -> Type :=
- | tf_leaf_true : forall x, TreeFlags (T_Leaf x)
- | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
- | tf_branch : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
-
- Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
- match t as T return TreeFlags T with
- | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
- | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
- end.
-
- (* take and drop are not exact inverses *)
-
- (* drop replaces each leaf where the flag is set with a [] *)
- Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
- match tf with
- | tf_leaf_true x => []
- | tf_leaf_false x => Σ
- | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2)
- end.
-
- (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
- Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
- match tf with
- | tf_leaf_true x => Some Σ
- | tf_leaf_false x => None
- | tf_branch b1 b2 tb1 tb2 =>
- match take tb1 with
- | None => take tb2
- | Some b1' => match take tb2 with
- | None => Some b1'
- | Some b2' => Some (b1',,b2')
- end
- end
- end.
-
- Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
- match t with
- | None => []
- | Some x => x
- end.
-
- Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool :=
- fun t =>
- match t with
- | None => b
- | Some x => f x
- end.
-
- (* "Arrange" objects are parametric in the type of the leaves of the tree *)
- Definition arrangeMap :
- forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
- Arrange Σ₁ Σ₂ ->
- Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
- intros.
- induction X; simpl.
- apply RCanL.
- apply RCanR.
- apply RuCanL.
- apply RuCanR.
- apply RAssoc.
- apply RCossa.
- apply RExch.
- apply RWeak.
- apply RCont.
- apply RLeft; auto.
- apply RRight; auto.
- eapply RComp; [ apply IHX1 | apply IHX2 ].
- Defined.
-
- Definition bnot (b:bool) : bool := if b then false else true.
-
- Definition swapMiddle {T} (a b c d:Tree ??T) :
- Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
- eapply RComp.
- apply RCossa.
- eapply RComp.
- eapply RLeft.
- eapply RComp.
- eapply RAssoc.
- eapply RRight.
- apply RExch.
- eapply RComp.
- eapply RLeft.
- eapply RCossa.
- eapply RAssoc.
- Defined.
-
Definition arrange :
forall {T} (Σ:Tree ??T) (f:T -> bool),
- Arrange Σ (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))).
+ Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
intros.
induction Σ.
simpl.
simpl.
apply RuCanL.
simpl in *.
- eapply RComp; [ idtac | apply swapMiddle ].
+ eapply RComp; [ idtac | apply arrangeSwapMiddle ].
eapply RComp.
eapply RLeft.
apply IHΣ2.
Definition arrange' :
forall {T} (Σ:Tree ??T) (f:T -> bool),
- Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ.
+ Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
intros.
induction Σ.
simpl.
simpl.
apply RCanL.
simpl in *.
- eapply RComp; [ apply swapMiddle | idtac ].
+ eapply RComp; [ apply arrangeSwapMiddle | idtac ].
eapply RComp.
eapply RLeft.
apply IHΣ2.
apply IHΣ1.
Defined.
- Definition minus' n m :=
- match m with
- | 0 => n
- | _ => match n with
- | 0 => 0
- | _ => n - m
- end
- end.
-
Ltac eqd_dec_refl' :=
match goal with
| [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
[ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
end.
- 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_unflatten : WeakExprVar).
Context (hetmet_id : WeakExprVar).
Context {unitTy : forall TV, RawHaskType TV ★ }.
Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
(* In a tree of types, replace any type at depth "lev" or greater None *)
Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
- mkFlags (setNone false (levelMatch lev)) tt.
+ mkFlags (liftBoolFunc false (levelMatch lev)) tt.
Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
- drop (mkDropFlags lev tt).
+ dropT (mkDropFlags lev tt).
(* The opposite: replace any type which is NOT at level "lev" with None *)
Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
- mkFlags (setNone true (bnot ○ levelMatch lev)) tt.
+ mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
- mapOptionTree (fun x => garrowfy_code_types (unlev x)) (drop (mkTakeFlags lev tt)).
+ mapOptionTree (fun x => garrowfy_code_types (unlev x)) (dropT (mkTakeFlags lev tt)).
(*
mapOptionTree (fun x => garrowfy_code_types (unlev x))
- (maybeTree (take tt (mkFlags (
+ (maybeTree (takeT tt (mkFlags (
fun t => match t with
| Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
| _ => true
end
) tt))).
+
+ Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
+ match t with
+ | None => []
+ | Some x => x
+ end.
*)
Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
end.
+ (* AXIOMS *)
+
Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
+ Axiom garrowfy_commutes_with_substT :
+ forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
+ garrowfy_code_types (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))
+ (garrowfy_code_types τ).
+
+ Axiom garrowfy_commutes_with_HaskTAll :
+ forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+ garrowfy_code_types (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
+
+ Axiom garrowfy_commutes_with_HaskTApp :
+ forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+ garrowfy_code_types (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
+ HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))) (FreshHaskTyVar κ).
+
+ Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
+ garrowfy_leveled_code_types (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types t).
+
+ Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
+ garrowfy_code_types (g v) = g v.
+
(* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
* levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
* picks nil *)
ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
intros.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
+ eapply nd_comp; [ idtac
+ | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod.
apply X.
apply ga_comp.
Defined.
+ Definition precompose Γ Δ ec : forall a x y z lev,
+ ND Rule
+ [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
+ [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
+ intros.
+ eapply nd_comp.
+ apply nd_rlecnac.
+ eapply nd_comp.
+ eapply nd_prod.
+ apply nd_id.
+ eapply ga_comp.
+
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+
+ apply nd_rule.
+ apply RLet.
+ Defined.
+
Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
- ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
intros.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec a b @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec b c) lev) ].
- eapply nd_comp; [ apply nd_llecnac | idtac ].
- apply nd_prod.
+ eapply nd_comp.
apply X.
- apply ga_comp.
+ apply precompose.
Defined.
Definition postcompose : ∀ Γ Δ ec lev a b c,
apply q.
Defined.
-(*
+ (* useful for cutting down on the pretty-printed noise
+
Notation "` x" := (take_lev _ x) (at level 20).
Notation "`` x" := (mapOptionTree unlev x) (at level 20).
Notation "``` x" := (drop_lev _ x) (at level 20).
-*)
+ *)
Definition garrowfy_arrangement' :
forall Γ (Δ:CoercionEnv Γ)
(ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
| RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
| RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
| RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
- | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
+ | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
| RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
| RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
| RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
reflexivity.
Qed.
- Axiom garrowfy_commutes_with_substT :
- forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
- garrowfy_code_types (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))
- (garrowfy_code_types τ).
-
- Axiom garrowfy_commutes_with_HaskTAll :
- forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
- garrowfy_code_types (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
-
- Axiom garrowfy_commutes_with_HaskTApp :
- forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
- garrowfy_code_types (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
- HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))) (FreshHaskTyVar κ).
-
- Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
- garrowfy_leveled_code_types (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types t).
-
- Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
- garrowfy_code_types (g v) = g v.
-
Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
intro T.
right; auto.
Defined.
-
Definition flatten_proof :
forall {h}{c},
ND Rule h c ->
refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
(mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
apply arrange_brak.
- apply (Prelude_error "found Brak at depth >0 (a)").
+ apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
destruct case_REsc.
simpl.
(* environment has non-empty leaves *)
apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
- apply (Prelude_error "found Esc at depth >0 (a)").
+ apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
destruct case_RNote.
simpl.
apply nd_rule.
apply q.
apply INil.
+ destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
+ set (garrowfy_code_types (g wev)) as t.
+ set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+ simpl in q.
+ apply nd_rule.
+ apply q.
+ apply INil.
apply nd_rule; rewrite globals_do_not_have_code_types.
apply RGlobal.
- apply (Prelude_error "found RGlobal at depth >0").
+ apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
destruct case_RLam.
Opaque drop_lev.
simpl.
destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
apply flatten_coercion; auto.
- apply (Prelude_error "RCast at level >0").
+ apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
destruct case_RJoin.
simpl.
- destruct (getjlev x); destruct (getjlev q).
- apply nd_rule.
- apply RJoin.
- apply (Prelude_error "RJoin at depth >0").
- apply (Prelude_error "RJoin at depth >0").
- apply (Prelude_error "RJoin at depth >0").
+ destruct (getjlev x); destruct (getjlev q);
+ [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
+ apply (Prelude_error "RJoin at depth >0").
destruct case_RApp.
simpl.
replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
apply (Prelude_error "FIXME: ga_apply").
reflexivity.
+
(*
- Notation "` x" := (take_lev _ x) (at level 20).
+ Notation "` x" := (take_lev _ x).
Notation "`` x" := (mapOptionTree unlev x) (at level 20).
Notation "``` x" := ((drop_lev _ x)) (at level 20).
Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
- Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
+ Notation "!<[@]> x" := (mapOptionTree garrowfy_leveled_code_types x) (at level 1).
*)
+
destruct case_RLet.
- apply (Prelude_error "FIXME: RLet").
-(*
simpl.
destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
- destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
repeat drop_simplify.
repeat take_simplify.
- rename σ₁ into a.
- rename σ₂ into b.
- rewrite mapOptionTree_distributes.
- rewrite mapOptionTree_distributes.
- set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A.
- set (take_lev (ec :: lev) Σ₁) as A'.
- set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B.
- set (take_lev (ec :: lev) Σ₂) as B'.
simpl.
eapply nd_comp.
- Focus 2.
- eapply nd_rule.
- eapply RLet.
-
- apply nd_prod.
-
- apply boost.
- apply ga_second.
-
- eapply nd_comp.
- Focus 2.
+ eapply nd_prod; [ idtac | apply nd_id ].
eapply boost.
- apply ga_comp.
+ apply ga_second.
eapply nd_comp.
- eapply nd_rule.
- eapply RArrange.
- eapply RCanR.
-
+ eapply nd_prod.
+ apply nd_id.
eapply nd_comp.
- Focus 2.
eapply nd_rule.
eapply RArrange.
- eapply RExch.
- idtac.
-
- eapply nd_comp.
- apply nd_llecnac.
- eapply nd_comp.
- Focus 2.
- eapply nd_rule.
- apply RJoin.
- apply nd_prod.
+ apply RCanR.
+ eapply precompose.
- eapply nd_rule.
- eapply RVar.
+ apply nd_rule.
+ apply RLet.
- apply nd_id.
-*)
destruct case_RVoid.
simpl.
apply nd_rule.
apply RAppT.
apply Δ.
apply Δ.
- apply (Prelude_error "ga_apply").
+ apply (Prelude_error "found type application at level >0; this is not supported").
destruct case_RAbsT.
simpl. destruct lev; simpl.
apply nd_id.
apply Δ.
apply Δ.
- apply (Prelude_error "AbsT at depth>0").
+ apply (Prelude_error "found type abstraction at level >0; this is not supported").
destruct case_RAppCo.
simpl. destruct lev; simpl.
apply RAppCo.
apply flatten_coercion.
apply γ.
- apply (Prelude_error "AppCo at depth>0").
+ apply (Prelude_error "found coercion application at level >0; this is not supported").
destruct case_RAbsCo.
simpl. destruct lev; simpl.
unfold garrowfy_code_types.
simpl.
apply (Prelude_error "AbsCo not supported (FIXME)").
- apply (Prelude_error "AbsCo at depth>0").
+ apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
destruct case_RLetRec.
rename t into lev.
+ simpl.
apply (Prelude_error "LetRec not supported (FIXME)").
destruct case_RCase.
simpl.
- apply (Prelude_error "Case not supported (FIXME)").
+ apply (Prelude_error "Case not supported (BIG FIXME)").
Defined.
projects / coq-hetmet.git / blobdiff