index dab8cde..60e84b6 100644 (file)
@@ -23,7 +23,7 @@ Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Const
Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".

Definition dataConExTyVars cdc :=
-  filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
+  filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)).
Opaque dataConExTyVars.
Definition dataConCoerKinds cdc :=
filter (map (fun x => match x with EqPred t1 t2 =>
@@ -199,6 +199,8 @@ Notation "t @@  l" := (@mkLeveledHaskType _ _ t l) (at level 20).
Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).

+Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
+
Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
match lht with t@@l => t end.

@@ -212,49 +214,107 @@ Coercion glob_wv : Global >-> WeakExprVar.

(* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
-Definition take_arg_types : forall {TV}{κ}(exp: RawHaskType TV κ), list (RawHaskType TV κ).
-refine (fix take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
-  match exp as E in RawHaskType _ K return κ=K -> list (RawHaskType _ K) with
-  | TApp   κ₁ κ₂ x y      =>
-    fun eqpf =>
-      ((fun q:list (RawHaskType TV κ₂) =>
-        match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> list (RawHaskType _ _) with
-          | TApp   κ₁' κ₂' x' y'      =>
-            fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
-                           | TArrow => fun eqpf'' => _
-                           | _      => fun _      => nil
-                         end (refl_equal _)
-          | _                         => fun _ => nil
-        end (refl_equal _))
-      (take_arg_types TV _ y))
-    | _                     => fun _ => nil
-  end (refl_equal _)).
-  subst; inversion eqpf''; subst.
-  apply (y'::q).
-  Defined.
+Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
+  match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
+    | TApp   κ₁ κ₂ x y      =>
+      (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
+         | KindStar =>
+           match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
+             | KindStar => fun x' =>
+               match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
+                 | TApp κ₁'' κ₂'' w'' x'' =>
+                   match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
+                                                                    list (RawHaskType _ KindStar) with
+                     | KindStar     =>
+                       match w'' with
+                         | TArrow => fun a b => a::b
+                         | _      => fun _ _ => nil
+                       end
+                     | _ => fun _ _ => nil
+                   end x''
+                 | _                      => fun _  => nil
+               end
+             | _        => fun _ _ => nil
+           end
+         | _ => fun _ _ => nil
+       end) x (take_arg_types y)
+    | _                     => nil
+  end.
+
+Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
+  match exp as E in RawHaskType _ K return nat with
+    | TApp   κ₁ κ₂ x y      =>
+      (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
+         | KindStar =>
+           match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
+             | KindStar => fun x' =>
+               match x' return nat -> nat with
+                 | TApp κ₁'' κ₂'' w'' x'' =>
+                   match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
+                     | KindStar     =>
+                       match w'' with
+                         | TArrow => fun a b => S b
+                         | _      => fun _ _ => 0
+                       end
+                     | _ => fun _ _ => 0
+                   end x''
+                 | _                      => fun _  => 0
+               end
+             | _        => fun _ _ => 0
+           end
+         | _ => fun _ _ => 0
+       end) x (count_arg_types y)
+    | _                     => 0
+  end.
+
+  Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
+    intros.
+    induction Γ.
+    apply INil.
+    apply ICons; auto.
+    apply tt.
+    Defined.
+
+Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
+  fun pf =>
+  fun TV ite =>
+    match take_arg_types (ht TV ite) with
+    | nil => Prelude_error "impossible"
+    | x::y => x
+    end.

(* From (t1->(t2->(t3-> ... t))), return t *)
(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
-refine (fix drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : RawHaskType TV κ :=
-  match exp as E in RawHaskType _ K return κ=K -> RawHaskType _ K with
-  | TApp   κ₁ κ₂ x y      =>
-    fun eqpf =>
-      ((fun q:RawHaskType TV κ₂ =>
-        match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> RawHaskType _ _ with
-          | TApp   κ₁' κ₂' x' y'      =>
-            fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
-                           | TArrow => fun eqpf'' => _
-                           | z      => fun _      => TApp x y
-                         end (refl_equal _)
-          | z                         => fun _ => TApp x y
-        end (refl_equal _))
-      (drop_arg_types TV _ y))
-    | z                     => fun _ => z
-  end (refl_equal _)).
-  subst; inversion eqpf''; subst.
-  apply q.
-  Defined.
+  match exp as E in RawHaskType _ K return RawHaskType _ K with
+    | TApp   κ₁ κ₂ x y      =>
+      let q :=
+      (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
+         | KindStar =>
+           match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
+             | KindStar => fun x' =>
+               match x' return  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+                 | TApp κ₁'' κ₂'' w'' x'' =>
+                   match κ₂'' as K2'' return RawHaskType TV K2'' ->  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+                     | KindStar     =>
+                       match w'' with
+                         | TArrow => fun _ b => Some b
+                         | _      => fun _ b => None
+                       end
+                     | _ => fun _ b => None
+                   end x''
+                 | _       => fun _ => None
+               end
+             | _        => fun _ _ => None
+           end
+         | _ => fun _ _ => None
+       end) x (drop_arg_types y)
+      in match q with
+           | None   => TApp x y
+           | Some y => y
+         end
+    | b                     => b
+  end.

@@ -381,10 +441,10 @@ Record StrongAltCon {tc:TyCon} :=
; sac_numExprVars :  nat
; sac_ekinds      :  vec Kind sac_numExTyVars
; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
-; sac_Γ           := fun Γ => app (vec2list sac_ekinds) Γ
-; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
-; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
-; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
+; sac_gamma          := fun Γ => app (vec2list sac_ekinds) Γ
+; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
+; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
+; sac_delta          := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
}.
Coercion sac_tc     : StrongAltCon >-> TyCon.
Coercion sac_altcon : StrongAltCon >-> WeakAltCon.

Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).

-Fixpoint update_ξ
+Fixpoint update_xi
`{EQD_VV:EqDecidable VV}{Γ}
@@ -412,12 +472,12 @@ Fixpoint update_ξ
: VV -> LeveledHaskType Γ ★ :=
match vt with
| nil => ξ
-    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
+    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
end.

-Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
not (In v (map (@fst _ _) varstypes)) ->
-  (update_ξ ξ lev varstypes) v = ξ v.
+  (update_xi ξ lev varstypes) v = ξ v.
intros.
induction varstypes.
reflexivity.