projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
add an identity production for Arrange
[coq-hetmet.git]
/
src
/
HaskProofToStrong.v
diff --git
a/src/HaskProofToStrong.v
b/src/HaskProofToStrong.v
index
52f2154
..
b6e8efe
100644
(file)
--- a/
src/HaskProofToStrong.v
+++ b/
src/HaskProofToStrong.v
@@
-239,6
+239,7
@@
Section HaskProofToStrong.
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)
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 _
| RCanL a => let case_RCanL := tt in _
| RCanR a => let case_RCanR := tt in _
| RuCanL a => let case_RuCanL := tt in _
@@
-251,6
+252,9
@@
Section HaskProofToStrong.
| RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
end); clear urule2expr; intros.
| RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
end); clear urule2expr; intros.
+ destruct case_RId.
+ apply X.
+
destruct case_RCanL.
simpl; unfold ujudg2exprType; intros.
simpl in X.
destruct case_RCanL.
simpl; unfold ujudg2exprType; intros.
simpl in X.
@@
-569,7
+573,6
@@
Section HaskProofToStrong.
destruct case_RGlobal.
apply ILeaf; simpl; intros; refine (return ILeaf _ _).
apply EGlobal.
destruct case_RGlobal.
apply ILeaf; simpl; intros; refine (return ILeaf _ _).
apply EGlobal.
- apply wev.
destruct case_RLam.
apply ILeaf.
destruct case_RLam.
apply ILeaf.
@@
-633,7
+636,7
@@
Section HaskProofToStrong.
apply ileaf in q1'.
apply ileaf in q2'.
simpl in *.
apply ileaf in q1'.
apply ileaf in q2'.
simpl in *.
- apply (EApp _ _ _ _ _ _ q1' q2').
+ apply (EApp _ _ _ _ _ _ q2' q1').
destruct case_RLet.
apply ILeaf.
destruct case_RLet.
apply ILeaf.
@@
-715,6
+718,7
@@
Section HaskProofToStrong.
inversion X; subst; clear X.
apply (@ELetRec _ _ _ _ _ _ _ varstypes).
inversion X; subst; clear X.
apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+ auto.
apply (@letrec_helper Γ Δ t varstypes).
rewrite <- pf2 in X1.
rewrite mapOptionTree_compose.
apply (@letrec_helper Γ Δ t varstypes).
rewrite <- pf2 in X1.
rewrite mapOptionTree_compose.