Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
- Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
- match j with
- mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
- FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
- end.
-
Definition judg2exprType (j:Judg) : Type :=
match j with
(Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
inversion pf2.
Defined.
- Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
- ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
-
- refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
- ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
- match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
- | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RCanL t a => let case_RCanL := tt in _
- | RCanR t a => let case_RCanR := tt in _
- | RuCanL t a => let case_RuCanL := tt in _
- | RuCanR t a => let case_RuCanR := tt in _
- | RAssoc t a b c => let case_RAssoc := tt in _
- | RCossa t a b c => let case_RCossa := tt in _
- | RExch t a b => let case_RExch := tt in _
- | RWeak t a => let case_RWeak := tt in _
- | RCont t a => let case_RCont := tt in _
+ Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
+ forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
+
+ Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t
+ .
+ intros Γ Δ.
+ refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t :=
+ match r as R in Arrange H C return
+ ujudg2exprType Γ ξ Δ H t ->
+ ujudg2exprType Γ ξ Δ C t
+ with
+ | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RCanL a => let case_RCanL := tt in _
+ | RCanR a => let case_RCanR := tt in _
+ | RuCanL a => let case_RuCanL := tt in _
+ | RuCanR a => let case_RuCanR := tt in _
+ | RAssoc a b c => let case_RAssoc := tt in _
+ | RCossa a b c => let case_RCossa := tt in _
+ | RExch a b => let case_RExch := tt in _
+ | RWeak a => let case_RWeak := tt in _
+ | RCont a => let case_RCont := tt in _
+ | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
end); clear urule2expr; intros.
destruct case_RCanL.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 ([],,vars)).
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X ([],,vars)).
simpl; rewrite <- H; auto.
destruct case_RCanR.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 (vars,,[])).
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X (vars,,[])).
simpl; rewrite <- H; auto.
destruct case_RuCanL.
- apply ILeaf; simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
- inversion X.
- simpl in X0.
- apply (X0 vars2); auto.
+ simpl in X.
+ apply (X vars2); auto.
destruct case_RuCanR.
- apply ILeaf; simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
- inversion X.
- simpl in X0.
- apply (X0 vars1); auto.
+ simpl in X.
+ apply (X vars1); auto.
destruct case_RAssoc.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
destruct vars; try destruct o; inversion H.
destruct vars1; try destruct o; inversion H.
- apply (X0 (vars1_1,,(vars1_2,,vars2))).
+ apply (X (vars1_1,,(vars1_2,,vars2))).
subst; auto.
destruct case_RCossa.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
destruct vars; try destruct o; inversion H.
destruct vars2; try destruct o; inversion H.
- apply (X0 ((vars1,,vars2_1),,vars2_2)).
+ apply (X ((vars1,,vars2_1),,vars2_2)).
subst; auto.
+ destruct case_RExch.
+ simpl; unfold ujudg2exprType ; intros.
+ simpl in X.
+ destruct vars; try destruct o; inversion H.
+ apply (X (vars2,,vars1)).
+ inversion H; subst; auto.
+
+ destruct case_RWeak.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X []).
+ auto.
+
+ destruct case_RCont.
+ simpl; unfold ujudg2exprType ; intros.
+ simpl in X.
+ apply (X (vars,,vars)).
+ simpl.
+ rewrite <- H.
+ auto.
+
destruct case_RLeft.
- destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
- destruct o; [ idtac | apply INone ].
- destruct u; simpl in *.
- apply ILeaf; simpl; intros.
+ intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
- set (fun q => ileaf (e ξ q)) as r'.
- simpl in r'.
- apply r' with (vars:=vars2).
- clear r' e.
- clear r0.
- induction h0.
- destruct a.
- destruct u.
+ apply (fun q => e ξ q vars2 H2).
+ clear r0 e H2.
simpl in X.
- apply ileaf in X.
- apply ILeaf.
simpl.
- simpl in X.
+ unfold ujudg2exprType.
intros.
apply X with (vars:=vars1,,vars).
- simpl.
rewrite H0.
rewrite H1.
+ simpl.
reflexivity.
- apply INone.
- apply IBranch.
- apply IHh0_1. inversion X; auto.
- apply IHh0_2. inversion X; auto.
- auto.
-
+
destruct case_RRight.
- destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
- destruct o; [ idtac | apply INone ].
- destruct u; simpl in *.
- apply ILeaf; simpl; intros.
+ intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
- set (fun q => ileaf (e ξ q)) as r'.
- simpl in r'.
- apply r' with (vars:=vars1).
- clear r' e.
- clear r0.
- induction h0.
- destruct a.
- destruct u.
+ apply (fun q => e ξ q vars1 H1).
+ clear r0 e H2.
simpl in X.
- apply ileaf in X.
- apply ILeaf.
simpl.
- simpl in X.
+ unfold ujudg2exprType.
intros.
apply X with (vars:=vars,,vars2).
- simpl.
rewrite H0.
- rewrite H2.
+ inversion H.
+ simpl.
reflexivity.
- apply INone.
- apply IBranch.
- apply IHh0_1. inversion X; auto.
- apply IHh0_2. inversion X; auto.
- auto.
- destruct case_RExch.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- destruct vars; try destruct o; inversion H.
- apply (X0 (vars2,,vars1)).
- inversion H; subst; auto.
-
- destruct case_RWeak.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 []).
- auto.
-
- destruct case_RCont.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 (vars,,vars)).
- simpl.
- rewrite <- H.
- auto.
+ destruct case_RComp.
+ apply e2.
+ apply e1.
+ apply X.
Defined.
- Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
- ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
- intro it.
- induction c.
- destruct a.
- destruct u; simpl in *.
- apply ileaf in it.
- apply ILeaf.
- simpl in *.
- intros; apply it with (vars:=vars); auto.
- apply INone.
- apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
- Defined.
-
Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
ITree (LeveledHaskType Γ ★)
(fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
admit.
Defined.
- Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
- match t with
- | T_Leaf None => return []
- | T_Leaf (Some x) => bind x' = x ; return [x']
- | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
- end.
-
Definition gather_branch_variables
Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
ProofCaseBranch tc Γ Δ lev tbranches avars sac})
intros h j r.
refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
- | RURule a b c d e => let case_RURule := tt in _
+ | RArrange a b c d e r => let case_RURule := tt in _
| RNote Γ Δ Σ τ l n => let case_RNote := tt in _
| RLit Γ Δ l _ => let case_RLit := tt in _
| RVar Γ Δ σ p => let case_RVar := tt in _
| RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
end); intro X_; try apply ileaf in X_; simpl in X_.
- destruct case_RURule.
- destruct d; try destruct o.
- apply ILeaf; destruct u; simpl; intros.
- set (@urule2expr a b _ _ e ξ) as q.
- set (fun z => ileaf (q z)) as q'.
+ destruct case_RURule.
+ apply ILeaf. simpl. intros.
+ set (@urule2expr a b _ _ e r0 ξ) as q.
+ set (fun z => q z) as q'.
simpl in q'.
apply q' with (vars:=vars).
clear q' q.
- apply bridge.
- apply X_.
+ unfold ujudg2exprType.
+ intros.
+ apply X_ with (vars:=vars0).
+ auto.
auto.
- apply no_urules_with_empty_conclusion in e; inversion e; auto.
- apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
destruct case_RBrak.
apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
apply ileaf in X.
apply ileaf in X0.
simpl in *.
- refine (X0 ξ vars2 _ >>>= fun X0' => _).
+ refine (X ξ vars2 _ >>>= fun X0' => _).
apply FreshMon.
auto.
- refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+
+ refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
apply FreshMon.
rewrite H1.
simpl.
rewrite pf1.
rewrite H1.
reflexivity.
+
refine (return _).
apply ILeaf.
apply ileaf in X0'.
projects / coq-hetmet.git / blobdiff