(* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
* free tyvars in them *)
- Definition ξ (wev:WeakExprVar) : LeveledHaskType Γ ★ :=
- match weakTypeToType' φ wev ★ with
- | Error s => fail ("Error in top-level xi: " +++ s)
- | OK t => t @@ nil
+ Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
+ match coreVarToWeakVar cv with
+ | WExprVar wev => match weakTypeToType' φ wev ★ with
+ | Error s => fail ("Error in top-level xi: " +++ s)
+ | OK t => t @@ nil
+ end
+ | WTypeVar _ => fail "top-level xi got a type variable"
+ | WCoerVar _ => fail "top-level xi got a coercion variable"
end.
Definition header : string :=
Require Import Coq.Init.Specif.
Require Import HaskKinds.
Require Import HaskCoreLiterals.
+Require Import HaskCoreVars.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
Require Import HaskWeak.
Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
:= tv::::ite.
-Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{lev}
+Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
+ match lht with t@@l => t end.
+
+Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
(ftv:Fresh Kind (fun _ => WeakTypeVar))
(fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
- (exp:@Expr WeakExprVar _ Γ Δ ξ lev)
+ (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
: InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr :=
-match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
-| EVar _ _ _ ev => fun ite => WEVar ev
+match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
+| EVar Γ' _ ξ' ev => fun ite => WEVar (weakExprVar ev (@typeToWeakType ftv Γ' ★ (unlev (ξ' ev)) ite))
| ELit _ _ _ lit _ => fun ite => WELit lit
| EApp Γ' _ _ _ _ _ e1 e2 => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
-| ELam Γ' _ _ _ _ _ cv e => fun ite => WELam cv (strongExprToWeakExpr ftv fcv e ite)
-| ELet Γ' _ _ _ _ _ ev e1 e2 => fun ite => WELet ev (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
+| ELam Γ' _ _ _ t _ cv e => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e ite)
+| ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
| EEsc Γ' _ _ ec t _ e => fun ite => WEEsc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
| EBrak Γ' _ _ ec t _ e => fun ite => WEBrak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
| ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
let t2' := typeToWeakType ftv σ₂ ite in
let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite)
end
-with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{lev}{vars}
+with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars}
(ftv:Fresh Kind (fun _ => WeakTypeVar))
(fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
- (elrb:@ELetRecBindings WeakExprVar _ Γ Δ ξ lev vars)
+ (elrb:@ELetRecBindings _ CoreVarEqDecidable Γ Δ ξ τ vars)
: InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) :=
match elrb as E in ELetRecBindings G D X L V
return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with
| ELR_nil _ _ _ _ => fun ite => []
-| ELR_leaf _ _ _ _ cv v e => fun ite => [(v,(strongExprToWeakExpr ftv fcv e ite))]
+| ELR_leaf _ _ _ t cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv t ite)),(strongExprToWeakExpr ftv fcv e ite))]
| ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)
end.
WeakExpr.
(* calculate the free WeakVar's in a WeakExpr *)
+(*
Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
match me with
| WELit _ => nil
| nil => me
| cv::cvl' => WELam cv (closeExpression me cvl')
end) me (getWeakExprFreeVars me).
-
+*)
Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
(WTyCon (haskLiteralToTyCon lit)).
Defined.
(* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
-Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ)
- : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ').
+Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
+ : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
intros.
destruct τ as [τ l].
destruct τ' as [τ' l'].
(Δ:CoercionEnv Γ)
(φ:TyVarResolver Γ)
(ψ:CoVarResolver Γ Δ)
- (ξ:WeakExprVar -> LeveledHaskType Γ ★)
+ (ξ:CoreVar -> LeveledHaskType Γ ★)
(τ:HaskType Γ ★)
(lev:HaskLevel Γ),
- WeakExpr -> ???(Expr Γ Δ ξ (τ @@ lev) ).
+ WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
refine ((
fix weakExprToStrongExpr
(Γ:TypeEnv)
(Δ:CoercionEnv Γ)
(φ:TyVarResolver Γ)
(ψ:CoVarResolver Γ Δ)
- (ξ:WeakExprVar -> LeveledHaskType Γ ★)
+ (ξ:CoreVar -> LeveledHaskType Γ ★)
(τ:HaskType Γ ★)
(lev:HaskLevel Γ)
- (we:WeakExpr) : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
+ (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
match we with
| WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v)
| WELam ev e => weakTypeToType' φ ev ★ >>= fun tv =>
weakTypeOfWeakExpr e >>= fun t =>
weakTypeToType' φ t ★ >>= fun τ' =>
- weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((ev,tv@@lev)::nil)) τ' _ e >>= fun e' =>
+ weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((ev:CoreVar),tv@@lev)::nil))
+ τ' _ e >>= fun e' =>
castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
| WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
| WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv =>
weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
- weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((v,tv@@lev)::nil)) τ lev ebody
+ weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
>>= fun ebody' =>
- OK (ELet _ _ _ tv _ lev v ve' ebody')
+ OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
| WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
weakTypeToType' φ t2 ★ >>= fun t2' =>
then true
else false.
-(* Coq's "decide equality" can't cope here; we have to cheat for now *)
-Axiom compare_weakTypes_axiom : forall w1 w2, if compare_weakTypes w1 w2 then w1=w2 else not (w1=w2).
-
+(*
Instance EqDecidableWeakType : EqDecidable WeakType.
apply Build_EqDecidable.
intros.
left; auto.
right; auto.
Defined.
+*)
Instance WeakTypeToString : ToString WeakType :=
{ toString := coreTypeToString ○ weakTypeToCoreType }.
Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
((map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc)) , (tyFunResultKind tc)).
+(*
(* EqDecidable instances for all of the above *)
Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
apply Build_EqDecidable.
left; auto.
right; intro X; apply n; inversion X; auto.
Defined.
-
-
+*)
Instance WeakVarToString : ToString WeakVar :=
{ toString := fun x => toString (weakVarToCoreVar x) }.
\ No newline at end of file
projects / coq-hetmet.git / commitdiff