Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Definition judg2exprType (j:Judg) : Type :=
match j with
- (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
- FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
+ (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
+ FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
end.
- Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
+ Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
intros.
inversion X; auto.
Defined.
inversion pf2.
Defined.
- Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
- forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
+ Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
+ forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
- Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
- ujudg2exprType Γ ξ Δ h t ->
- ujudg2exprType Γ ξ Δ j t
+ Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+ ujudg2exprType Γ ξ Δ h t l ->
+ ujudg2exprType Γ ξ Δ j t l
.
intros Γ Δ.
- refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
- ujudg2exprType Γ ξ Δ h t ->
- ujudg2exprType Γ ξ Δ j t :=
+ refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} :
+ ujudg2exprType Γ ξ Δ h t l ->
+ ujudg2exprType Γ ξ Δ j t l :=
match r as R in Arrange H C return
- ujudg2exprType Γ ξ Δ H t ->
- ujudg2exprType Γ ξ Δ C t
+ ujudg2exprType Γ ξ Δ H t l ->
+ ujudg2exprType Γ ξ Δ C t l
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)
- | RId a => let case_RId := tt in _
- | 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)
+ | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | AId a => let case_AId := tt in _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in _
+ | AuAssoc a b c => let case_AuAssoc := tt in _
+ | AExch a b => let case_AExch := tt in _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
end); clear urule2expr; intros.
- destruct case_RId.
+ destruct case_AId.
apply X.
- destruct case_RCanL.
+ destruct case_ACanL.
simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X ([],,vars)).
simpl; rewrite <- H; auto.
- destruct case_RCanR.
+ destruct case_ACanR.
simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X (vars,,[])).
simpl; rewrite <- H; auto.
- destruct case_RuCanL.
+ destruct case_AuCanL.
simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
simpl in X.
apply (X vars2); auto.
- destruct case_RuCanR.
+ destruct case_AuCanR.
simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
simpl in X.
apply (X vars1); auto.
- destruct case_RAssoc.
+ destruct case_AAssoc.
simpl; unfold ujudg2exprType; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
apply (X (vars1_1,,(vars1_2,,vars2))).
subst; auto.
- destruct case_RCossa.
+ destruct case_AuAssoc.
simpl; unfold ujudg2exprType; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
apply (X ((vars1,,vars2_1),,vars2_2)).
subst; auto.
- destruct case_RExch.
+ destruct case_AExch.
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.
+ destruct case_AWeak.
simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X []).
auto.
- destruct case_RCont.
+ destruct case_ACont.
simpl; unfold ujudg2exprType ; intros.
simpl in X.
apply (X (vars,,vars)).
rewrite <- H.
auto.
- destruct case_RLeft.
+ destruct case_ALeft.
intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
apply (fun q => e ξ q vars2 H2).
simpl.
reflexivity.
- destruct case_RRight.
+ destruct case_ARight.
intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
apply (fun q => e ξ q vars1 H1).
simpl.
reflexivity.
- destruct case_RComp.
+ destruct case_AComp.
apply e2.
apply e1.
apply X.
Defined.
Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
- ITree (LeveledHaskType Γ ★)
- (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
- (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
+ ITree (HaskType Γ ★)
+ (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
+ (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
-> ELetRecBindings Γ Δ ξ' l varstypes.
intros.
induction varstypes.
simpl.
destruct (eqd_dec h0 l).
rewrite <- e0.
+ simpl in X.
+ subst.
apply X.
apply (Prelude_error "level mismatch; should never happen").
apply (Prelude_error "letrec type mismatch; should never happen").
prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
((fun sac => FreshM
{ scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
- & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
+ & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
+ (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
intro pcb.
intro X.
simpl in X.
intros h j r.
refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
- | RArrange a b c d e r => let case_RURule := tt in _
+ | RArrange a b c d e l 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 _
| RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
| RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
| RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
- | RJoin Γ p lri m x q => let case_RJoin := tt in _
- | RVoid _ _ => let case_RVoid := tt in _
+ | RJoin Γ p lri m x q l => let case_RJoin := tt in _
+ | RVoid _ _ l => let case_RVoid := tt in _
| RBrak Σ a b c n m => let case_RBrak := tt in _
| REsc Σ a b c n m => let case_REsc := tt in _
| RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
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.
+ set (@urule2expr a b _ _ e l r0 ξ) as q.
unfold ujudg2exprType.
+ unfold ujudg2exprType in q.
+ apply q with (vars:=vars).
intros.
apply X_ with (vars:=vars0).
auto.
destruct case_RVar.
apply ILeaf; simpl; intros; refine (return ILeaf _ _).
- destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
- apply EVar.
+ destruct vars; simpl in H; inversion H; destruct o. inversion H1.
+ set (@EVar _ _ _ Δ ξ v) as q.
+ rewrite <- H2 in q.
+ simpl in q.
+ apply q.
inversion H.
destruct case_RGlobal.
apply (@ELetRec _ _ _ _ _ _ _ varstypes).
auto.
apply (@letrec_helper Γ Δ t varstypes).
- rewrite <- pf2 in X0.
rewrite mapOptionTree_compose.
- apply X0.
+ rewrite mapOptionTree_compose.
+ rewrite pf2.
+ replace ((mapOptionTree unlev (y @@@ t))) with y.
+ apply X0.
+ clear pf1 X0 X1 pfdist pf2 vars varstypes.
+ induction y; try destruct a; auto.
+ rewrite IHy1 at 1.
+ rewrite IHy2 at 1.
+ reflexivity.
apply ileaf in X1.
+ simpl in X1.
apply X1.
destruct case_RCase.
admit.
Defined.
- Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
- {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
- FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
+ Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
+ {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
+ FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
intro pf.
set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
apply closed2expr in cnd.
auto.
refine (return OK _).
exists ξ.
- apply (ileaf it).
+ apply ileaf in it.
+ simpl in it.
+ apply it.
apply INone.
Defined.
projects / coq-hetmet.git / blobdiff