Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
Require Import HaskWeak.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskCoreVars.
-
-(* can remove *)
-Require Import HaskStrongToWeak.
+Require Import HaskCoreTypes.
Open Scope string_scope.
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
| WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
| WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
| WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
- | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
+ | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
+ >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
| WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
weakTypeToType _ φ t1 >>= fun t1' =>
weakTypeToType _ φ t2 >>= fun t2' =>
end
| tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
- | nil => Error "WTyFunApp applied to too many types"
+ | nil => Error ("WTyFunApp applied to too many types"(* +++ eol +++
+ " tyCon= " +++ toString tc +++ eol +++
+ " tyConKindArgs= " +++ toString (fst (tyFunKind tc)) +++ eol +++
+ " tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
+ " types= " +++ toString lt +++ eol*))
| k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
let case_weakTypeListToTypeList := tt in _
end
try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
apply (Error ("Kind mismatch in WAppTy: "+++err)).
-
+
destruct case_weakTypeListToTypeList.
apply (addErrorMessage "case_weakTypeListToTypeList").
destruct t' as [ k' t' ].
apply OK.
eapply haskTypeOfSomeKind.
unfold HaskType; intros.
- apply TyFunApp.
+ apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
apply lt'.
apply X.
Defined.
Definition coVarKind (wcv:WeakCoerVar) : Kind :=
- match wcv with weakCoerVar _ κ _ _ => κ end.
+ match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
Coercion coVarKind : WeakCoerVar >-> Kind.
Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
| T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
end.
-(*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
+Definition checkDistinct :
+ forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
+ intros.
+ set (distinct_decidable lv) as q.
+ destruct q.
+ exact (OK d).
+ exact (Error "checkDistinct failed").
+ Defined.
+
+(* FIXME: check the kind of the type of the weakexprvar to support >0 *)
+Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
+ refine {| glob_kinds := nil |}.
+ apply wev.
+ intros.
+ apply τ.
+ Defined.
Definition weakExprToStrongExpr : forall
(Γ:TypeEnv)
match we with
| WEVar v => if ig v
- then OK (EGlobal Γ Δ ξ (τ@@lev) v)
+ then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
| WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
| _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
end
- | WECoLam cv e => let (_,_,t1,t2) := cv in
+ | WECoLam cv e => let (_,t1,t2) := cv in
weakTypeOfWeakExpr e >>= fun te =>
weakTypeToTypeOfKind φ te ★ >>= fun te' =>
weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
end) rb
in binds >>= fun binds' =>
+ checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
- OK (ELetRec Γ Δ ξ lev τ _ binds' e')
+ OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
| WECase vscrut escrut tbranches tc avars alts =>
weakTypeOfWeakExpr escrut >>= fun tscrut =>
destruct (ξ c).
simpl.
apply e1.
+ rewrite mapleaves.
+ apply rb_distinct.
destruct case_pf.
set (distinct_decidable (vec2list exprvars')) as dec.