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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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.