From: Adam Megacz Date: Tue, 21 Jun 2011 03:02:25 +0000 (-0700) Subject: add crude support for flattening with LetRec and Case at level zero X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=3161a8a65cb0190e83d32bde613c3b64dfe31739 add crude support for flattening with LetRec and Case at level zero --- diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 59636bf..b352398 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -1196,8 +1196,26 @@ Section HaskFlattener. reflexivity. destruct case_RCase. - simpl. - apply (Prelude_error "Case not supported (BIG FIXME)"). + destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl. + apply nd_rule. + rewrite <- mapOptionTree_compose. + replace (mapOptionTree + (fun x => flatten_judgment (pcb_judg (snd x))) + alts,, [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [flatten_type (caseType tc avars)] @ nil]) + with + (mapOptionTree + (fun x => @pcb_judg tc Γ Δ nil (flatten_type tbranches) avars (fst x) (snd x)) + alts,, + [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [caseType tc avars] @ nil]). + replace (mapOptionTree flatten_leveled_type + (mapOptionTreeAndFlatten + (fun x => (snd x)) alts)) + with (mapOptionTreeAndFlatten + (fun x => + (snd x)) alts). + apply RCase. + admit. + admit. destruct case_SBrak. simpl. diff --git a/src/HaskProof.v b/src/HaskProof.v index f98800d..84eaa0b 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -36,14 +36,13 @@ Inductive Judg := Notation "Γ > Δ > a '|-' s '@' l" := (mkJudg Γ Δ a s l) (at level 52, Δ at level 50, a at level 52, s at level 50, l at level 50). (* information needed to define a case branch in a HaskProof *) -Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} := -{ pcb_freevars : Tree ??(LeveledHaskType Γ ★) -; pcb_judg := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ) +Definition pcb_judg + {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} + (pcb_freevars : Tree ??(LeveledHaskType Γ ★)) := + sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ) > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev) (vec2list (sac_types sac Γ avars)))) - |- [weakT' branchtype ] @ weakL' lev -}. -Implicit Arguments ProofCaseBranch [ ]. + |- [weakT' branchtype ] @ weakL' lev. (* Figure 3, production $\vdash_E$, all rules *) Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := @@ -87,11 +86,11 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev] | RCase : forall Γ Δ lev tc Σ avars tbranches - (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }), + (alts:Tree ??( (@StrongAltCon tc) * (Tree ??(LeveledHaskType Γ ★)) )), Rule - ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),, + ((mapOptionTree (fun x => @pcb_judg tc Γ Δ lev tbranches avars (fst x) (snd x)) alts),, [Γ > Δ > Σ |- [ caseType tc avars ] @lev]) - [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev] + [Γ > Δ > (mapOptionTreeAndFlatten (fun x => (snd x)) alts),,Σ |- [ tbranches ] @ lev] . Definition RCut' : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l, diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 3dbc81f..f50c586 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -393,9 +393,9 @@ Section HaskProofToStrong. exists x; auto. Defined. - Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x }) - : ITree { x:X & F x } (fun x => J (projT1 x)) t - -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t). + Definition fix_indexing X Y (J:X->Type)(t:Tree ??(X*Y)) + : ITree (X * Y) (fun x => J (fst x)) t + -> ITree X (fun x:X => J x) (mapOptionTree (@fst _ _) t). intro it. induction it; simpl in *. apply INone. @@ -418,12 +418,13 @@ Section HaskProofToStrong. Defined. Definition case_helper tc Γ Δ lev tbranches avars ξ : - forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac}, - prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} -> + forall pcb:(StrongAltCon * Tree ??(LeveledHaskType Γ ★)), + prod (judg2exprType (@pcb_judg tc Γ Δ lev tbranches avars (fst pcb) (snd pcb))) + {vars' : Tree ??VV & (snd 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) - (weakT' tbranches) (weakL' lev) }) (projT1 pcb)). + (weakT' tbranches) (weakL' lev) }) (fst pcb)). intro pcb. intro X. simpl in X. @@ -435,7 +436,7 @@ Section HaskProofToStrong. destruct s as [vars vars_pf]. refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars - (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _). + (mapOptionTree weakLT' pcb) (weakLT' ○ ξ) (weakL' lev) _ ; _). apply FreshMon. rewrite vars_pf. rewrite <- mapOptionTree_compose. @@ -470,14 +471,15 @@ Section HaskProofToStrong. Defined. Definition gather_branch_variables - Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon & - ProofCaseBranch tc Γ Δ lev tbranches avars sac}) + Γ Δ + (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev + (alts:Tree ??(@StrongAltCon tc * Tree ??(LeveledHaskType Γ ★))) : forall vars, - mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars - -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts) - -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q))) - { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' }) + mapOptionTreeAndFlatten (fun x => snd x) alts = mapOptionTree ξ vars + -> ITree Judg judg2exprType (mapOptionTree (fun x => @pcb_judg tc Γ Δ lev avars tbranches (fst x) (snd x)) alts) + -> ITree _ (fun q => prod (judg2exprType (@pcb_judg tc Γ Δ lev avars tbranches (fst q) (snd q))) + { vars' : _ & (snd q) = mapOptionTree ξ vars' }) alts. induction alts; intro vars; @@ -487,7 +489,7 @@ Section HaskProofToStrong. simpl in *. apply ileaf in source. apply ILeaf. - destruct s as [sac pcb]. + destruct p as [sac pcb]. simpl in *. split. intros. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 8764102..eaf1341 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -518,8 +518,17 @@ Section HaskSkolemizer. eapply RLetRec. destruct case_RCase. - simpl. - apply (Prelude_error "CASE: BIG FIXME"). + destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl. + apply nd_rule. + apply SFlat. + rewrite <- mapOptionTree_compose. + assert + ((mapOptionTree (fun x => skolemize_judgment (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts) = + (mapOptionTree (fun x => (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts)). + admit. + rewrite H. + set (@RCase Γ Δ nil tc Σ avars tbranches alts) as q. + apply q. Defined. Transparent take_arg_types_as_tree. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 114f2d9..8ae0d09 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -549,23 +549,6 @@ match elrb with | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2) end. -Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} -(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_gamma sac Γ) - (sac_delta sac Γ atypes (weakCK'' Δ)) - (scbwv_xi scb ξ l) - (weakT' tbranches) (weakL' l) } }) - : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. - destruct alt. - exists x. - exact - {| pcb_freevars := mapOptionTree ξ - (stripOutVars (vec2list (scbwv_exprvars (projT1 s))) - (expr2antecedent (projT2 s))) - |}. - Defined. - - Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) := match elrb with | ELR_nil Γ Δ ξ lev => [] @@ -1057,6 +1040,21 @@ Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : Qed. +Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} +(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) + (weakT' tbranches) (weakL' l) } }) + : @StrongAltCon tc * Tree ??(LeveledHaskType Γ ★). + destruct alt. + split. + apply x. + apply (mapOptionTree ξ + (stripOutVars (vec2list (scbwv_exprvars (projT1 s))) + (expr2antecedent (projT2 s)))). + Defined. + Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e (alts':Tree ??{sac : StrongAltCon & @@ -1064,7 +1062,7 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}), - (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) + (mapOptionTreeAndFlatten (fun x => snd x) (mapOptionTree mkProofCaseBranch alts')) ,, mapOptionTree ξ (expr2antecedent e) = @@ -1131,13 +1129,15 @@ Definition expr2proof : (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l) } }) - : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := + : ND Rule [] (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) alts) := match alts as ALTS return ND Rule [] - (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with + (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) ALTS) with | T_Leaf None => let case_nil := tt in _ | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2) | T_Leaf (Some x) => - match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with + match x as X return ND Rule [] [@pcb_judg tc Γ Δ l tbranches atypes + (fst (mkProofCaseBranch X)) + (snd (mkProofCaseBranch X))] with existT sac (existT scbx ex) => (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex) end @@ -1250,10 +1250,10 @@ Definition expr2proof : destruct case_leaf. clear o x alts alts' e. - eapply nd_comp; [ apply e' | idtac ]. + simpl. + apply (fun x => nd_comp e' x). clear e'. - apply nd_rule. - apply RArrange. + unfold pcb_judg. simpl. rewrite mapleaves'. simpl. @@ -1262,26 +1262,40 @@ Definition expr2proof : rewrite <- mapleaves'. rewrite vec2list_map_list2vec. unfold sac_gamma. - rewrite <- (scbwv_coherent scbx l ξ). rewrite <- vec2list_map_list2vec. rewrite mapleaves'. - set (@factorContextRightAndWeaken'') as q. - unfold scbwv_xi. set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z. unfold scbwv_varstypes in z. rewrite vec2list_map_list2vec in z. rewrite fst_zip in z. rewrite <- z. clear z. + unfold sac_gamma in *. + simpl in *. + Unset Printing Implicit. + idtac. + apply nd_rule. + apply RArrange. + set (scbwv_exprvars_distinct scbx) as q'. + rewrite <- leaves_unleaves in q'. + apply (AComp (@factorContextRightAndWeaken'' _ (weakCE' Δ) _ _ (expr2antecedent ex) q')). + clear q'. - replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with - (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). - apply q. - apply (sac_delta sac Γ atypes (weakCK'' Δ)). - rewrite leaves_unleaves. - apply (scbwv_exprvars_distinct scbx). + set (scbwv_coherent scbx l ξ) as H. rewrite leaves_unleaves. - reflexivity. + unfold scbwv_varstypes. + apply ALeft. + rewrite <- mapleaves'. + rewrite <- mapleaves'. + rewrite mapleaves'. + rewrite vec2list_map_list2vec. + rewrite <- H. + clear H. + rewrite <- mapleaves'. + rewrite vec2list_map_list2vec. + unfold scbwv_xi. + unfold scbwv_varstypes. + apply AId. destruct case_nil. apply nd_id0.