Require Import Coq.Lists.List.
Require Import General.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskCoreTypes.
Require Import HaskCoreVars.
Require Import HaskWeakTypes.
| TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
| TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
| TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
- | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
+ | TCode : RawHaskType ECKind -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
| TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* S_n *)
with RawHaskTypeList : list Kind -> Type :=
| TyFunApp_nil : RawHaskTypeList nil
(* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
-Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ★).
+Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ECKind).
Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
(cv:HaskTyVar Γ κ) : HaskType Γ ★
:= fun TV env => σ TV env (cv TV env).
-Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
+Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
:= fun TV ite => TCon tc.
Coercion glob_tf : Global >-> Funclass.
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 *)
+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 *)
+Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
+ 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.
projects / coq-hetmet.git / blobdiff