add support for flattening recursive-let

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index d70cd58..e0226d8 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -307,6 +307,8 @@ Section core2proof.
     (hetmet_pga_applyr : CoreVar)
     (hetmet_pga_curryl : CoreVar)
     (hetmet_pga_curryr : CoreVar)
     (hetmet_pga_applyr : CoreVar)
     (hetmet_pga_curryl : CoreVar)
     (hetmet_pga_curryr : CoreVar)

+    (hetmet_pga_loopl : CoreVar)
+    (hetmet_pga_loopr : CoreVar)

     .
 
 
     .
 
 

@@ -411,6 +413,8 @@ Section core2proof.
 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)

+    ; ga_loopl     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopl (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+    ; ga_loopr     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopr (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))

     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"

@@ -529,7 +533,10 @@ Section core2proof.
     (hetmet_pga_applyl : CoreVar)
     (hetmet_pga_applyr : CoreVar)
     (hetmet_pga_curryl : CoreVar)
     (hetmet_pga_applyl : CoreVar)
     (hetmet_pga_applyr : CoreVar)
     (hetmet_pga_curryl : CoreVar)

-    (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
+    (hetmet_pga_curryr : CoreVar)
+    (hetmet_pga_loopl : CoreVar)
+    (hetmet_pga_loopr : CoreVar)
+    : list (@CoreBind CoreVar) :=

     coqPassCoreToCore'
        do_flatten
        do_skolemize
     coqPassCoreToCore'
        do_flatten
        do_skolemize

@@ -556,6 +563,8 @@ Section core2proof.
        hetmet_pga_copy 
        hetmet_pga_drop 
        hetmet_pga_swap 
        hetmet_pga_copy 
        hetmet_pga_drop 
        hetmet_pga_swap 

+       hetmet_pga_loopl 
+       hetmet_pga_loopr 

        lbinds
        (*
        hetmet_pga_applyl 
        lbinds
        (*
        hetmet_pga_applyl 

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 1731aad..c19f81a 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -272,6 +272,8 @@ Section HaskFlattener.
   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]

+  ; ga_loopl     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
+  ; ga_loopr     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ]

   ; ga_comp      : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ] 
   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
   ; ga_comp      : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ] 
   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]

@@ -991,7 +993,11 @@ Section HaskFlattener.
       unfold x1.
       rewrite drop_to_nothing.
       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
       unfold x1.
       rewrite drop_to_nothing.
       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).

-      admit. (* OK *)
+        induction Σ₁₂; try destruct a; auto.
+        simpl.
+        rewrite <- IHΣ₁₂1 at 2.
+        rewrite <- IHΣ₁₂2 at 2.
+        reflexivity.

       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
       set (mapOptionTree flatten_type Σ₁₂) as a.
       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
       set (mapOptionTree flatten_type Σ₁₂) as a.
       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.

@@ -1031,7 +1037,11 @@ Section HaskFlattener.
         eapply RArrange.
         eapply ARight.
         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
         eapply RArrange.
         eapply ARight.
         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).

-        admit (* FIXME *).
+          induction Σ; try destruct a; auto.
+          simpl.
+          rewrite <- IHΣ1 at 2.
+          rewrite <- IHΣ2 at 2.
+          reflexivity.

         idtac.
         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
         apply boost.
         idtac.
         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
         apply boost.

@@ -1066,7 +1076,11 @@ Section HaskFlattener.
         eapply RArrange.
         eapply ALeft.
         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
         eapply RArrange.
         eapply ALeft.
         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).

-        admit (* FIXME *).
+          induction Σ; try destruct a; auto.
+          simpl.
+          rewrite <- IHΣ1 at 2.
+          rewrite <- IHΣ2 at 2.
+          reflexivity.

         idtac.
         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
         apply boost.
         idtac.
         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
         apply boost.

@@ -1082,10 +1096,13 @@ Section HaskFlattener.
 
     destruct case_RVoid.
       simpl.
 
     destruct case_RVoid.
       simpl.

-      apply nd_rule.

       destruct l.
       destruct l.

+      apply nd_rule.

       apply RVoid.
       apply RVoid.

-      apply (Prelude_error "RVoid at level >0").
+      drop_simplify.
+      take_simplify.
+      simpl.
+      apply ga_id.

         
     destruct case_RAppT.
       simpl. destruct lev; simpl.
         
     destruct case_RAppT.
       simpl. destruct lev; simpl.

@@ -1156,7 +1173,31 @@ Section HaskFlattener.
         rewrite IHy1.
         rewrite IHy2.
         reflexivity.
         rewrite IHy1.
         rewrite IHy2.
         reflexivity.

-      apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
+      repeat drop_simplify.
+      repeat take_simplify.
+      simpl.
+      rewrite drop_to_nothing.
+      eapply nd_comp.
+        eapply nd_rule.
+        eapply RArrange.
+        eapply AComp.
+        eapply ARight.
+        apply arrangeCancelEmptyTree with (q:=y).
+          induction y; try destruct a; auto.
+          simpl.
+          rewrite <- IHy1.
+          rewrite <- IHy2.
+          reflexivity.
+        apply ACanL.
+        rewrite take_lemma'.
+        set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'.
+        set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''.
+        replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y).
+        apply boost.
+        apply ga_loopl.
+        rewrite <- mapOptionTree_compose.
+        simpl.
+        reflexivity.

 
     destruct case_RCase.
       simpl.
 
     destruct case_RCase.
       simpl.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 5e6fac4..f98800d 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -85,7 +85,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ ]@l]
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
 
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ ]@l]
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
 

-| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
+| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]

 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 0d90d4c..3dbc81f 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -964,7 +964,7 @@ Section HaskProofToStrong.
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
     refine (X_ ((update_xi ξ t (leaves varstypes)))
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
     refine (X_ ((update_xi ξ t (leaves varstypes)))

-      (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
+      ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_.  apply FreshMon.

     simpl.
     rewrite pf2.
     rewrite pf1.
     simpl.
     rewrite pf2.
     rewrite pf1.

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 435b687..8764102 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -492,7 +492,30 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply (@RLetRec Γ Δ lri x y nil).
         apply nd_rule.
         apply SFlat.
         apply (@RLetRec Γ Δ lri x y nil).

-        apply (Prelude_error "RLetRec at depth>0").
+        destruct (decide_tree_empty (mapOptionTreeAndFlatten take_arg_types_as_tree y @@@ (h :: t)));
+          [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
+        destruct (eqd_dec y (mapOptionTree drop_arg_types_as_tree y));
+          [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
+        rewrite <- e.
+        clear e.
+        eapply nd_comp.
+          eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply ALeft.
+          eapply AComp.
+          eapply ARight.
+          destruct s.
+          apply (arrangeCancelEmptyTree _ _ e).
+          apply ACanL.
+        eapply nd_comp.
+          eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AuAssoc.
+        eapply nd_rule.
+          eapply SFlat.
+          eapply RLetRec.

 
       destruct case_RCase.
         simpl.
 
       destruct case_RCase.
         simpl.

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 1f1229d..114f2d9 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -997,7 +997,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 

-  set (@factorContextRightAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
+  set (@factorContextLeftAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.

   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
   set (q' disti) as q''.
   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
   set (q' disti) as q''.