From 93ac0d63048027161f816c451a7954fb8a6470c0 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 15 May 2011 00:55:19 -0700 Subject: [PATCH 1/1] add an identity production for Arrange --- src/HaskProof.v | 2 ++ src/HaskProofToLatex.v | 1 + src/HaskProofToStrong.v | 4 ++++ 3 files changed, 7 insertions(+) diff --git a/src/HaskProof.v b/src/HaskProof.v index ee536b0..d9c6a7e 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -45,6 +45,7 @@ Implicit Arguments ProofCaseBranch [ ]. (* Figure 3, production $\vdash_E$, Uniform rules *) Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type := +| RId : forall a , Arrange a a | RCanL : forall a , Arrange ( [],,a ) ( a ) | RCanR : forall a , Arrange ( a,,[] ) ( a ) | RuCanL : forall a , Arrange ( a ) ( [],,a ) @@ -176,6 +177,7 @@ Definition arrangeMap : Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂). intros. induction X; simpl. + apply RId. apply RCanL. apply RCanR. apply RuCanL. diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index d35a870..61b358f 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -161,6 +161,7 @@ Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string := match r with | RLeft _ _ _ r => nd_uruleToRawLatexMath r | RRight _ _ _ r => nd_uruleToRawLatexMath r + | RId _ => "Id" | RCanL _ => "CanL" | RCanR _ => "CanR" | RuCanL _ => "uCanL" diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 19f2f62..b6e8efe 100644 --- 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) + | 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 _ @@ -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. + destruct case_RId. + apply X. + destruct case_RCanL. simpl; unfold ujudg2exprType; intros. simpl in X. -- 1.7.10.4