remove RLet and RWhere

[coq-hetmet.git] / src / HaskSkolemizer.v

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index bfbdf0e..435b687 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -9,6 +9,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.

+Require Import NaturalDeductionContext.

 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 

@@ -82,19 +83,7 @@ Section HaskSkolemizer.
     end.
 
   (* rules of skolemized proofs *)
     end.
 
   (* rules of skolemized proofs *)

-  Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
-  Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
-    match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
-  Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
-    match tt with
-      | T_Leaf None              => nil
-      | T_Leaf (Some (_ @@ lev)) => lev
-      | T_Branch b1 b2 =>
-        match getjlev b1 with
-          | nil => getjlev b2
-          | lev => lev
-        end
-    end.
+  Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end.

 
   Fixpoint take_trustme {Γ}
     (n:nat)
 
   Fixpoint take_trustme {Γ}
     (n:nat)

@@ -130,20 +119,20 @@ Section HaskSkolemizer.
   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 
   Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 
   Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,

-    Arrange ([tx @@ lev],, take_arg_types_as_tree te @@@ lev)
+    Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)

       (take_arg_types_as_tree (tx ---> te) @@@ lev).
     intros.
       (take_arg_types_as_tree (tx ---> te) @@@ lev).
     intros.

-    destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+    destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).

       rewrite <- e.
       simpl.
       rewrite <- e.
       simpl.

-      apply RId.
+      apply AId.

     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).

-      apply RCanR.
+      apply ACanR.

         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").
         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").

@@ -152,19 +141,19 @@ Section HaskSkolemizer.
 
   Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
     Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
 
   Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
     Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)

-      ([tx @@ lev],, take_arg_types_as_tree te @@@ lev).
+      ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).

     intros.
     intros.

-    destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+    destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).

       rewrite <- e.
       simpl.
       rewrite <- e.
       simpl.

-      apply RId.
+      apply AId.

     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).

-      apply RuCanR.
+      apply AuCanR.

         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").
         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").

@@ -184,13 +173,13 @@ Section HaskSkolemizer.
   | SFlat  : forall h c, Rule h c -> SRule h c
   | SBrak  : forall Γ Δ t ec Σ l,
     SRule
   | SFlat  : forall h c, Rule h c -> SRule h c
   | SBrak  : forall Γ Δ t ec Σ l,
     SRule

-    [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
-    [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
+    [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        ] @ (ec::l)]
+    [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]

 
   | SEsc   : forall Γ Δ t ec Σ l,
     SRule
 
   | SEsc   : forall Γ Δ t ec Σ l,
     SRule

-    [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
-    [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
+    [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]
+    [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t         ] @ (ec::l)]

     .
 
   Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
     .
 
   Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=

@@ -201,11 +190,9 @@ Section HaskSkolemizer.
 
   Definition skolemize_judgment (j:Judg) : Judg :=
     match j with
 
   Definition skolemize_judgment (j:Judg) : Judg :=
     match j with

-      Γ > Δ > Σ₁ |- Σ₂ =>
-        match getjlev Σ₂ with
-          | nil => j
-          | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂
-        end
+      | Γ > Δ > Σ₁ |- Σ₂ @ nil       => j
+        | Γ > Δ > Σ₁ |- Σ₂ @ lev => 
+          Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂ @@@ lev) |- mapOptionTree drop_arg_types_as_tree Σ₂ @ lev

     end.
 
   Definition check_hof : forall {Γ}(t:HaskType Γ ★),
     end.
 
   Definition check_hof : forall {Γ}(t:HaskType Γ ★),

@@ -232,7 +219,7 @@ Section HaskSkolemizer.
     intros.
 
     refine (match X as R in Rule H C with
     intros.
 
     refine (match X as R in Rule H C with

-      | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
+      | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _

       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _

@@ -244,18 +231,19 @@ Section HaskSkolemizer.
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _

-      | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
-      | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
-      | RVoid    _ _                   => let case_RVoid := tt   in _
-      | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
-      | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
+      | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
+      | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
+      | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
+      | RVoid    _ _           l       => let case_RVoid := tt   in _
+      | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
+      | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _

       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
       end); clear X h c.
 
       destruct case_RArrange.
         simpl.
       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
       end); clear X h c.
 
       destruct case_RArrange.
         simpl.

-        destruct (getjlev x).
+        destruct l. 

         apply nd_rule.
         apply SFlat.
         apply RArrange.
         apply nd_rule.
         apply SFlat.
         apply RArrange.

@@ -263,7 +251,7 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply RArrange.
         apply nd_rule.
         apply SFlat.
         apply RArrange.

-        apply RRight.
+        apply ARight.

         apply d.
 
       destruct case_RBrak.
         apply d.
 
       destruct case_RBrak.

@@ -300,7 +288,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
         rewrite H.
         rewrite H0.
         simpl.

-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].

         apply nd_rule.
         apply SFlat.
         apply RLit.
         apply nd_rule.
         apply SFlat.
         apply RLit.

@@ -315,7 +303,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
         rewrite H.
         rewrite H0.
         simpl.

-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].

         apply nd_rule.
         apply SFlat.
         apply RVar.
         apply nd_rule.
         apply SFlat.
         apply RVar.

@@ -330,7 +318,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
         rewrite H.
         rewrite H0.
         simpl.

-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].

         apply nd_rule.
         apply SFlat.
         apply RGlobal.
         apply nd_rule.
         apply SFlat.
         apply RGlobal.

@@ -346,9 +334,9 @@ Section HaskSkolemizer.
         apply nd_rule.
           apply SFlat.
           apply RArrange.
         apply nd_rule.
           apply SFlat.
           apply RArrange.

-          eapply RComp.
-          apply RCossa.
-          apply RLeft.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.

           apply take_arrange.
 
       destruct case_RCast.
           apply take_arrange.
 
       destruct case_RCast.

@@ -360,16 +348,6 @@ Section HaskSkolemizer.
         apply γ.
         apply (Prelude_error "found RCast at level >0").
 
         apply γ.
         apply (Prelude_error "found RCast at level >0").
 

-      destruct case_RJoin.
-        simpl.
-        destruct (getjlev x).
-        destruct (getjlev q).
-        apply nd_rule.
-        apply SFlat.
-        apply RJoin.
-        apply (Prelude_error "found RJoin at level >0").
-        apply (Prelude_error "found RJoin at level >0").
-

       destruct case_RApp.
         simpl.
         destruct lev.
       destruct case_RApp.
         simpl.
         destruct lev.

@@ -383,56 +361,106 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
         rewrite H.
         rewrite H0.
         simpl.

-        set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
-        clear q.
+        eapply nd_comp.
+        eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+        eapply nd_rule.
+        eapply SFlat.
+        eapply RArrange.
+        eapply ALeft.
+        eapply take_unarrange.
+
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
+        eapply nd_comp; [ apply nd_exch | idtac ].
+        eapply nd_rule; eapply SFlat; eapply RCut.
+
+      destruct case_RCut.
+        simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
+        set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
+        set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
+        destruct (decide_tree_empty (Σ₁₂'' @@@ (h::l)));
+          [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+        destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+        rewrite <- e.
+        clear e.
+        destruct s.
+        eapply nd_comp.
+          eapply nd_prod.
+          eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AComp.
+          eapply ALeft.
+          eapply arrangeCancelEmptyTree with (q:=x).
+          apply e.
+          apply ACanR.
+          apply nd_id.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].

         apply nd_prod.
         apply nd_prod.

+        apply nd_id.
+        eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.
+          eapply AId.
+
+      destruct case_RLeft.
+        simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+        set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+        set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+        destruct (decide_tree_empty (Σ' @@@ (h::l)));
+          [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+        destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+        rewrite <- e.
+        clear Σ'' e.
+        destruct s.
+        set (arrangeUnCancelEmptyTree _ _ e) as q.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].

         apply nd_rule.
         apply nd_rule.

-        apply SFlat.
-        apply RArrange.
-        apply RCanR.
-        apply nd_rule.
-          apply SFlat.
-          apply RArrange.
-          eapply RComp; [ idtac | eapply RAssoc ].
-          apply RLeft.
-          eapply RComp; [ idtac | apply RExch ].
-          apply take_unarrange.
+        eapply SFlat.
+        eapply RLeft.
+        
+      destruct case_RRight.
+        simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+        set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+        set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+        destruct (decide_tree_empty (Σ' @@@ (h::l)));
+          [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+        destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+        rewrite <- e.
+        clear Σ'' e.
+        destruct s.
+        set (arrangeUnCancelEmptyTree _ _ e) as q.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ].  (* yuck *)
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
+        eapply nd_rule.
+        eapply SFlat.
+        apply RRight.

 
 

-      destruct case_RLet.
+      destruct case_RVoid.

         simpl.
         simpl.

-        destruct lev.
-        apply nd_rule.
-        apply SFlat.
-        apply RLet.
-        set (check_hof σ₂) as hof_tx.
-        destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
-        destruct a.
-        rewrite H.
-        rewrite H0.
-        set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
-        clear q.
-        apply nd_prod.
-        apply nd_rule.
-        apply SFlat.
-        apply RArrange.
-        apply RCanR.
-        eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        destruct l.

         apply nd_rule.
         apply SFlat.
         apply nd_rule.
         apply SFlat.

-        apply RArrange.
-        apply RLeft.
-        eapply RExch.
-
-      destruct case_RVoid.
-        simpl.
+        apply RVoid.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].

         apply nd_rule.
         apply SFlat.
         apply RVoid.
         apply nd_rule.
         apply SFlat.
         apply RVoid.

@@ -461,17 +489,16 @@ Section HaskSkolemizer.
       destruct case_RLetRec.
         simpl.
         destruct t.
       destruct case_RLetRec.
         simpl.
         destruct t.

-        destruct (getjlev (y @@@ nil)).

         apply nd_rule.
         apply SFlat.
         apply (@RLetRec Γ Δ lri x y nil).
         apply (Prelude_error "RLetRec at depth>0").
         apply nd_rule.
         apply SFlat.
         apply (@RLetRec Γ Δ lri x y nil).
         apply (Prelude_error "RLetRec at depth>0").

-        apply (Prelude_error "RLetRec at depth>0").

 
       destruct case_RCase.
         simpl.
         apply (Prelude_error "CASE: BIG FIXME").
         Defined.
 
       destruct case_RCase.
         simpl.
         apply (Prelude_error "CASE: BIG FIXME").
         Defined.

+

   Transparent take_arg_types_as_tree.
 
 End HaskSkolemizer.
   Transparent take_arg_types_as_tree.
 
 End HaskSkolemizer.