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.
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 :=
| 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,
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.
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.
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.
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;
simpl in *.
apply ileaf in source.
apply ILeaf.
- destruct s as [sac pcb].
+ destruct p as [sac pcb].
simpl in *.
split.
intros.
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.
| 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 => []
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 &
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) =
(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
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.
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.