* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
- | WExprVar wev => match weakTypeToType' φ wev ★ with
+ | WExprVar wev => match weakTypeToType'' φ wev ★ with
| Error s => Prelude_error ("Error in top-level xi: " +++ s)
| OK t => t @@ nil
end
+
+
+CoInductive Fresh A T :=
+{ next : forall a:A, (T a * Fresh A T)
+; split : Fresh A T * Fresh A T
+}.
+
+
+
+
+
Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
let (t1,t2) := coreCoercionKind cc
in coreTypeToWeakType t1 >>= fun t1' =>
coreTypeToWeakType t2 >>= fun t2' =>
- OK (weakCoercion t1' t2' cc).
+ OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
match ce with
(* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
- Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{sac:@StrongAltCon tc}{atypes:IList _ (HaskType Γ) (tyConKind sac)} :=
- { scbwv_sac := sac
+ Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} :=
+ { scbwv_sac : @StrongAltCon tc
; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list
Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l)
| ETyLam : ∀ Γ Δ ξ κ σ l,
Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
- | ECase : forall Γ Δ ξ l tc tbranches sac atypes,
+ | ECase : forall Γ Δ ξ l tc tbranches atypes,
Expr Γ Δ ξ (caseType tc atypes @@ l) ->
- Tree ??{ scb : StrongCaseBranchWithVVs tc sac atypes
+ Tree ??{ scb : StrongCaseBranchWithVVs tc atypes
& Expr (sac_Γ scb Γ)
(sac_Δ scb Γ atypes (weakCK'' Δ))
(scbwv_ξ scb ξ l)
(* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *)
with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type :=
| ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l []
- | ELR_leaf : ∀ Γ Δ ξ t l v, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)]
+ | ELR_leaf : ∀ Γ Δ ξ l v, Expr Γ Δ ξ (unlev (ξ v) @@ l) -> ELetRecBindings Γ Δ ξ l [(v,unlev (ξ v))]
| ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
.
Require Import HaskKinds.
Require Import HaskStrongTypes.
Require Import HaskStrong.
+Require Import HaskWeakVars.
Require Import HaskProof.
-Axiom fail : forall {A}, string -> A.
- Extract Inlined Constant fail => "Prelude.error".
-
Section HaskStrongToProof.
(* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
let branch_context := eLetRecContext branches
in let all_contexts := (expr2antecedent body),,branch_context
in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
- | ECase Γ Δ ξ l tc tbranches sac atypes e' alts =>
+ | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
((fix varsfromalts (alts:
- Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes
+ Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
& Expr (sac_Γ scb Γ)
(sac_Δ scb Γ atypes (weakCK'' Δ))
(scbwv_ξ scb ξ l)
with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => expr2antecedent e
+ | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
end.
-(*
-Definition caseBranchRuleInfoFromEStrongAltCon
- `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) :
- @StrongAltConRuleInfo n tc Γ lev tbranches.
- set (ecase2antecedent _ _ _ _ _ _ _ _ ecb) as Σ.
- destruct ecb.
- apply Build_StrongAltConRuleInfo with (pcb_scb := alt)(pcb_Σ := mapOptionTree ξ Σ).
- Defined.
-
-Definition judgFromEStrongAltCon
- `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) :
- Judg.
- apply caseBranchRuleInfoFromEStrongAltCon in ecb.
- destruct ecb.
- eapply pcb_judg.
- Defined.
+Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
+ (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
+ & Expr (sac_Γ scb Γ)
+ (sac_Δ scb Γ atypes (weakCK'' Δ))
+ (scbwv_ξ scb ξ l)
+ (weakLT' (tbranches@@l)) })
+ : ProofCaseBranch tc Γ Δ l tbranches atypes.
+ exact
+ {| pcb_scb := projT1 alt
+ ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
+ |}.
+ Defined.
-Implicit Arguments caseBranchRuleInfoFromEStrongAltCon [ [Γ] [Δ] [ξ] [lev] [tc] [avars] [tbranches] ].
-*)
-Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ ★) : HaskType Γ ★ := match lht with t @@ l => t end.
Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => [unlev (ξ v) @@ lev]
+ | ELR_leaf Γ Δ ξ lev v e => [ξ v]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
end.
Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => [v]
+ | ELR_leaf Γ Δ ξ lev v e => [v]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
end.
Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => [(v, ξ v)]
+ | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
end.
rewrite H.
clear H.
- (* FIXME TOTAL BOGOSITY *)
+ (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
assert ((stripOutVars (leaves v2) v1) = v1).
admit.
rewrite H.
Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
| lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
| lrsp_leaf : forall v e,
- (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [((unlev (ξ v) @@ lev))]]) ->
- LetRecSubproofs Γ Δ ξ lev [(v, (unlev (ξ v)))] (ELR_leaf _ _ _ _ _ _ e)
+ (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
+ LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
| lrsp_cons : forall t1 t2 b1 b2,
LetRecSubproofs Γ Δ ξ lev t1 b1 ->
LetRecSubproofs Γ Δ ξ lev t2 b2 ->
LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
-Lemma dork : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
+Lemma cheat9 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
eLetRecTypes branches =
mapOptionTree (update_ξ'' ξ tree lev)
apply REmptyGroup.
unfold mapOptionTree.
simpl.
- apply n.
+admit.
+(* apply n.*)
eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
- rewrite dork in q.
+ rewrite cheat9 in q.
set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
unfold update_ξ'' in *.
rewrite <- zz in q.
admit.
Qed.
*)
-Lemma cheat : forall {T} (a b:T), a=b.
- admit.
- Defined.
+
+Lemma cheat0 : forall Γ Δ ξ l tc tbranches atypes e alts',
+mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
+=
+(*
+((mapOptionTreeAndFlatten
+(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
+ (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
+*)
+((mapOptionTreeAndFlatten pcb_freevars
+ (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
+admit.
+Defined.
+
+Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
+ admit.
+ Defined.
+Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t.
+admit.
+Defined.
Definition expr2proof :
forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
: LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
| ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
- | ELR_leaf Γ Δ ξ t l v e => (fun e' => let case_elr_leaf := tt in _) (expr2proof _ _ _ _ e)
+ | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
end
) _ _ _ _ tree branches) in
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _
| ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _
| ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _
- | ECase Γ Δ ξ l tc tbranches sac atypes e alts =>
-(*
+ | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
let dcsp :=
((fix mkdcsp (alts:
- Tree ??{ scb : StrongCaseBranchWithVVs tc avars
+ Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
& Expr (sac_Γ scb Γ)
- (sac_Δ scb Γ avars (weakCK'' Δ))
- (scbwv_ξ scb ξ lev)
- (weakLT' (tbranches@@lev)) })
- : ND Rule [] (mapOptionTree judgFromEStrongAltCon alts) :=
- match alts as ALTS return ND Rule [] (mapOptionTree judgFromEStrongAltCon ALTS) with
+ (sac_Δ scb Γ atypes (weakCK'' Δ))
+ (scbwv_ξ scb ξ l)
+ (weakLT' (tbranches@@l)) })
+ : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
+ match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
| T_Leaf None => let case_nil := tt in _
| T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
- | T_Branch b1 b2 => let case_branch := tt in _
- end) alts)
- in *) let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | T_Branch b1 b2 => let case_branch := tt in _
+ end) alts')
+ in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
end
-); clear exp ξ' τ' Γ' Δ'; simpl in *.
+); clear exp ξ' τ' Γ' Δ'.
destruct case_EVar.
apply nd_rule.
auto.
inversion H.
- destruct case_ELet; intros.
+ destruct case_ELet; intros; simpl in *.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; [ idtac | apply pf_let].
apply e'.
auto.
- destruct case_ETyApp; intros.
+ destruct case_ETyApp; simpl in *; intros.
eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
apply e'.
auto.
- destruct case_ECoLam; intros.
- eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
- apply e'.
-
- destruct case_ECoApp; intros.
+ destruct case_ECoApp; simpl in *; intros.
eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
apply e'.
auto.
- destruct case_ETyLam; intros.
- eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
- unfold mapOptionTree in e'.
- rewrite mapOptionTree_compose in e'.
- unfold mapOptionTree.
- apply e'.
-
- destruct case_ECase.
- unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
- apply (fail "ECase not implemented").
- (*
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
- eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
- rewrite <- mapOptionTree_compose.
- apply dcsp.
- apply e'.
- *)
-
- destruct case_elr_leaf; intros.
- assert (unlev (ξ0 v) = t0).
- apply cheat.
- set (@lrsp_leaf Γ0 Δ0 ξ0 l v) as q.
- rewrite H in q.
- apply q.
- apply e'0.
-
- destruct case_ELetRec; intros.
- set (@letRecSubproofsToND') as q.
- simpl in q.
- apply q.
- clear q.
- apply e'.
- apply subproofs.
-
- (*
destruct case_leaf.
unfold pcb_judg.
simpl.
- clear mkdcsp alts0 o ecb Γ Δ ξ lev tc avars e alts u.
repeat rewrite <- mapOptionTree_compose in *.
- set (nd_comp ecb'
- (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ (unshape corevars) _ _))) as q.
- idtac.
+ set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
+ (unleaves (vec2list (scbwv_exprvars (projT1 x))))
+ (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
+ _ _
+ ))) as q.
+
+rewrite cheat2 in q.
+rewrite cheat1.
+unfold weakCK'' in q.
+simpl in q.
+admit.
+(*
+replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
+ (expr2antecedent (projT2 x))))
+with (mapOptionTree (scbwv_ξ (projT1 x) ξ l)
+ (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
+ (expr2antecedent (projT2 x)))).
+rewrite <- cheat1 in q.
+rewrite vec2list_map_list2vec in q.
+unfold mapOptionTree.
+fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★)
+ (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)).
+admit.
+*)
+admit.
+
+(*
+assert (
+
+unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x))))
+=
+unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l).
+admit.
+Set Printing Implicit.
+idtac.
+rewrite <- H.
+
assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))).
apply update_ξ_and_reapply.
rewrite H.
(coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0).
apply q.
apply cheat.
+*)
destruct case_branch.
simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod.
apply (mkdcsp b1).
apply (mkdcsp b2).
- *)
- Defined.
+ destruct case_ECase.
+ rewrite cheat0.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
+ rewrite <- mapOptionTree_compose.
+ apply dcsp.
+ apply e'.
+
+ destruct case_ELetRec; simpl in *; intros.
+ set (@letRecSubproofsToND') as q.
+ simpl in q.
+ apply q.
+ clear q.
+ apply e'.
+ apply subproofs.
+
+ (*
+ destruct case_ECoLam; simpl in *; intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
+ apply e'.
+
+ destruct case_ETyLam; intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
+ unfold mapOptionTree in e'.
+ rewrite mapOptionTree_compose in e'.
+ unfold mapOptionTree.
+ apply e'.
+ *)
+ Admitted.
End HaskStrongToProof.
Inductive Pgm Γ Δ :=
mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
*)
+
Require Import HaskStrongTypes.
Require Import HaskStrong.
-CoInductive Fresh A T :=
-{ next : forall a:A, (T a * Fresh A T)
-; split : Fresh A T * Fresh A T
-}.
+Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
+ : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=
+ match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) *
+ (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
+ | nil => (f,(vec_nil,ite))
+ | k::lk' =>
+ let (f',varsite') := mfresh f lk' ite
+ in let (vars,ite') := varsite'
+ in let (v,f'') := next _ _ f' k
+ in (f'',((v:::vars),v::::ite'))
+ end.
Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
{struct rht} : WeakType :=
Variable unsafeCoerce : WeakCoercion. Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
Definition strongCoercionToWeakCoercion {Γ}{Δ}{ck}(τ:HaskCoercion Γ Δ ck)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
- : WeakCoercion.
- unfold HaskCoercion in τ.
- admit.
- Defined.
+ : WeakCoercion := unsafeCoerce.
(* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's
* for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *)
Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
:= tv::::ite.
-Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
- match lht with t@@l => t end.
-
Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
(ftv:Fresh Kind (fun _ => WeakTypeVar))
(fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
| ETyApp Γ Δ κ σ τ ξ l e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite)
| ELetRec _ _ _ _ _ vars elrb e =>fun ite=>WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite)(strongExprToWeakExpr ftv fcv e ite)
| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
-| ECase Γ Δ ξ l tc tbranches sac atypes e alts =>
+| ECase Γ Δ ξ l tc tbranches atypes e alts =>
fun ite => WECase
(strongExprToWeakExpr ftv fcv e ite)
(@typeToWeakType ftv Γ _ tbranches ite)
tc
(ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes))
((fix caseBranches
- (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes
+ (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
& Expr (sac_Γ scb Γ)
(sac_Δ scb Γ atypes (weakCK'' Δ))
(update_ξ (weakLT'○ξ) (vec2list (vec_map
match tree with
| T_Leaf None => []
| T_Leaf (Some x) => let (scb,e) := x in
- (*[(sac_altcon scb,
- nil, (* FIXME *)
- nil, (* FIXME *)
- (*map (fun t => typeToWeakType ftv t ite') (vec2list (sac_types scb))*)nil, (* FIXME *)
- strongExprToWeakExpr ftv fcv e (weakITE' ite))]*) []
+ let (ftv',evarsite') := mfresh ftv _ ite in
+ let fcv' := fcv in
+ let (evars,ite') := evarsite' in
+ [(sac_altcon scb,
+ vec2list evars,
+ nil (*FIXME*),
+ map (fun vt => weakExprVar (fst vt) (typeToWeakType ftv' (snd vt) ite')) (vec2list (scbwv_varstypes scb)),
+ strongExprToWeakExpr ftv' fcv' e ite'
+ )]
| T_Branch b1 b2 => (caseBranches b1),,(caseBranches b2)
end
) alts)
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 _ _ _ t cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv t ite)),(strongExprToWeakExpr ftv fcv e ite))]
+| ELR_leaf _ _ ξ' cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv e ite))]
| ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)
end.
Require Import General.
Require Import HaskKinds.
Require Import HaskCoreLiterals.
-Require Import HaskCoreTypes. (* FIXME *)
-Require Import HaskCoreVars. (* FIXME *)
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
Require Import HaskWeakTypes.
-Require Import HaskWeakVars. (* FIXME *)
-Require Import HaskCoreToWeak. (* FIXME *)
+Require Import HaskWeakVars.
+Require Import HaskCoreToWeak.
Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
@InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
+
Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
:= fun TV env => TAll κ (σ TV env).
Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
+Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
+ match lht with t@@l => t end.
apply weakCK.
apply IHκ.
Defined.
+(*
Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
match κ as K return list (HaskCoercionKind (app K Γ)) with
| nil => hck
| _ => map weakCK' hck
end.
+*)
+Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
+ map weakCK' hck.
Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
; sac_numExprVars : nat
; sac_ekinds : vec Kind sac_numExTyVars
; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
-; sac_Γ := fun Γ => app (tyConKind tc) Γ
+; 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)) Δ
end
| WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
| WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
- | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
+ | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
| WELet ev ve e => weakTypeOfWeakExpr e
| WELetRec rb e => weakTypeOfWeakExpr e
| WENote n e => weakTypeOfWeakExpr e
- | WECast e (weakCoercion t1 t2 _) => OK t2
+ | WECast e (weakCoercion _ t1 t2 _) => OK t2
| WECase scrutinee tbranches tc type_params alts => OK tbranches
(* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
-(* a dummy variable which is never referenced but needed for a binder *)
-Variable dummyVariable : CoreVar.
- (* FIXME this doesn't actually work *)
- Extract Inlined Constant dummyVariable => "(Prelude.error ""dummyVariable"")".
-
Section HaskWeakToCore.
(* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
Context (hetmet_brak_var : CoreVar).
Context (hetmet_esc_var : CoreVar).
- (* FIXME: do something more intelligent here *)
Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
fun _ => trustMeCoercion.
- Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
+ Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar :=
match me with
| WEVar (weakExprVar v _) => CoreEVar v
| WELit lit => CoreELit lit
- | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
- | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
- | WECoApp e co => CoreEApp (weakExprToCoreExpr e )
+ | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2)
+ | WETyApp e t => CoreEApp (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t))
+ | WECoApp e co => CoreEApp (weakExprToCoreExpr f e )
(CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
- | WENote n e => CoreENote n (weakExprToCoreExpr e )
- | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e )
- | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e )
- | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e )
- | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
+ | WENote n e => CoreENote n (weakExprToCoreExpr f e )
+ | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr f e )
+ | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr f e )
+ | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr f e )
+ | WECast e co => CoreECast (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co)
| WEBrak (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var)
(CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
| WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var)
(CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
- | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
- | WECase e tbranches tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable (weakTypeToCoreType tbranches)
+ | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr f ve)) (weakExprToCoreExpr f e)
+ | WECase e tbranches tc types alts => let (v,f') := next _ _ f tt in
+ CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches)
(sortAlts ((
fix mkCaseBranches (alts:Tree
??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
(map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
(map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
(map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
- (weakExprToCoreExpr e))::nil
+ (weakExprToCoreExpr f' e))::nil
end
) alts))
| WELetRec mlr e => CoreELet (CoreRec
((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
match mlr with
| T_Leaf None => nil
- | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
+ | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr f e))::nil
| T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2)
end) mlr))
- (weakExprToCoreExpr e)
+ (weakExprToCoreExpr f e)
end.
End HaskWeakToCore.
Defined.
+Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
(* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
Section StrongAltCon.
Context (tc : TyCon)(dc:DataCon tc).
-(*
-Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ).
+
+Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
+ -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
intro avars.
intro ct.
- set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
+ set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
set (@substφ _ _ avars') as q.
set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
set (@weakTypeToType _ φ' ct) as t.
- set (@weakT'' _ Γ t) as t'.
- set (@lamer _ _ _ t') as t''.
+ destruct t as [|t]; try apply (Error error_message).
+ destruct t as [tk t].
+ matchThings tk ★ "weakTypeToType'".
+ subst.
+ apply OK.
+ set (@weakT'' _ Γ _ t) as t'.
+ set (@lamer _ _ _ _ t') as t''.
fold (tyConKinds tc) in t''.
fold (dataConExKinds dc) in t''.
- apply (q (tyConKinds tc)).
+ apply q.
+ clear q.
unfold tyConKinds.
unfold dataConExKinds.
rewrite <- vec2list_map_list2vec.
{| sac_altcon := DataAlt dc
; sac_numCoerVars := length (dataConCoerKinds dc)
; sac_numExprVars := length (dataConFieldTypes dc)
- ; sac_akinds := tyConKinds tc
; sac_ekinds := dataConExKinds dc
; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
; sac_types := fun Γ avars => let case_sac_types := tt in _
refine (vec_map _ (list2vec (dataConCoerKinds dc))).
intro.
destruct X.
- apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
+ unfold tyConKind in avars.
+ set (@weakTypeToType' Γ) as q.
+ unfold tyConKinds in q.
+ rewrite <- vec2list_map_list2vec in q.
+ rewrite vec2list_list2vec in q.
+ apply (
+ match
+ q avars w >>= fun t1 =>
+ q avars w0 >>= fun t2 =>
+ OK (mkHaskCoercionKind t1 t2)
+ with
+ | Error s => Prelude_error s
+ | OK y => y
+ end).
destruct case_sac_types.
refine (vec_map _ (list2vec (dataConFieldTypes dc))).
intro X.
- apply (weakTypeToType' avars).
- apply X.
+ unfold tyConKind in avars.
+ set (@weakTypeToType' Γ) as q.
+ unfold tyConKinds in q.
+ rewrite <- vec2list_map_list2vec in q.
+ rewrite vec2list_list2vec in q.
+ set (q avars X) as y.
+ apply (match y with
+ | Error s =>Prelude_error s
+ | OK y' => y'
+ end).
Defined.
-
+
+
Lemma weakCV' : forall {Γ}{Δ} Γ',
HaskCoVar Γ Δ
-> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
intros.
unfold HaskCoVar in *.
intros; apply (X TV CV).
- apply vec_chop' in env; auto.
+ apply ilist_chop' in env; auto.
unfold InstantiatedCoercionEnv in *.
unfold weakCK'' in cenv.
destruct Γ'.
+ rewrite <- map_preserves_length in cenv.
apply cenv.
rewrite <- map_preserves_length in cenv.
apply cenv.
apply vec_chop' in cenv.
apply cenv.
Defined.
-*)
+
+ Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
+ intros.
+ induction Δ.
+ reflexivity.
+ simpl.
+ rewrite IHΔ.
+ reflexivity.
+ Qed.
+
End StrongAltCon.
-(*
+
Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
destruct alt.
set (c:DataCon _) as dc.
set ((dataConTyCon c):TyCon) as tc' in *.
set (eqd_dec tc tc') as eqpf; destruct eqpf;
[ idtac
- | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++dc)) ]; subst.
+ | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
apply OK.
eapply mkStrongAltConPlusJunk.
simpl in *.
apply dc.
- apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
- ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
+ apply OK; refine {| sacpj_sac := {|
+ sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
; sac_altcon := LitAlt h
|} |}.
intro; intro φ; apply φ.
- intro; intro; intro; intro ψ; apply ψ.
- apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
- ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
+ intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
+ rewrite weakCK'_nil_inert. apply ψ.
+ apply OK; refine {| sacpj_sac := {|
+ sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
; sac_altcon := DEFAULT |} |}.
intro; intro φ; apply φ.
- intro; intro; intro; intro ψ; apply ψ.
+ intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
+ rewrite weakCK'_nil_inert. apply ψ.
Defined.
-Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ ★) :=
- match mlr with
- | T_Leaf None => []
- | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
- | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ))
- end.
-*)
-
Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
fun wev => match wev with weakExprVar _ t => t end.
Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
-(*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*)
+Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
WeakCoerVar -> HaskCoVar Γ (κ::Δ).
apply e.
Defined.
-Definition weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
+Definition coVarKind (wcv:WeakCoerVar) : Kind :=
+ match wcv with weakCoerVar _ κ _ _ => κ end.
+ Coercion coVarKind : WeakCoerVar >-> Kind.
+
+Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
intros.
set (weakTypeToType φ t) as wt.
destruct wt; try apply (Error error_message).
destruct h.
- matchThings κ κ0 "Kind mismatch in weakTypeToType': ".
+ matchThings κ κ0 "Kind mismatch in weakTypeToType'': ".
subst.
apply OK.
apply h.
Defined.
+Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
+ match t with
+ | T_Leaf None => []
+ | T_Leaf (Some (wev,e)) => match weakTypeToType'' φ wev ★ with
+ | Error _ => []
+ | OK t' => [((wev:CoreVar),t')]
+ end
+ | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
+ end.
+
+
+Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
+match lk as LK return ???(IList Kind (HaskType Γ) LK) with
+ | nil => match wtl with
+ | nil => OK INil
+ | _ => Error "length mismatch in mkAvars"
+ end
+ | k::lk' => match wtl with
+ | nil => Error "length mismatch in mkAvars"
+ | wt::wtl' =>
+ weakTypeToType'' φ wt k >>= fun t =>
+ mkAvars wtl' lk' φ >>= fun rest =>
+ OK (ICons _ _ t rest)
+ end
+end.
+
Definition weakExprToStrongExpr : forall
(Γ:TypeEnv)
(Δ:CoercionEnv Γ)
| WELit lit => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev)
- | WELam ev e => weakTypeToType' φ ev ★ >>= fun tv =>
+ | WELam ev e => weakTypeToType'' φ ev ★ >>= fun tv =>
weakTypeOfWeakExpr e >>= fun t =>
- weakTypeToType' φ t ★ >>= fun τ' =>
+ weakTypeToType'' φ t ★ >>= fun τ' =>
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' =>
castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
- | WEEsc ec e tbody => weakTypeToType' φ tbody ★ >>= fun tbody' =>
+ | WEEsc ec e tbody => weakTypeToType'' φ tbody ★ >>= fun tbody' =>
match lev with
| nil => Error "ill-leveled escapification"
| ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e
end
| WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
- | WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv =>
+ | WELet v ve ebody => weakTypeToType'' φ v ★ >>= fun tv =>
weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
>>= fun ebody' =>
OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
| WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
- weakTypeToType' φ t2 ★ >>= fun t2' =>
+ weakTypeToType'' φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
OK (EApp _ _ _ _ _ _ e1' e2')
| WETyLam tv e => let φ' := upφ tv φ in
weakTypeOfWeakExpr e >>= fun te =>
- weakTypeToType' φ' te ★ >>= fun τ' =>
+ weakTypeToType'' φ' te ★ >>= fun τ' =>
weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e
>>= fun e' =>
castExpr "WETyLam1" _ e' >>= fun e'' =>
match te with
| WForAllTy wtv te' =>
let φ' := upφ wtv φ in
- weakTypeToType' φ' te' ★ >>= fun te'' =>
+ weakTypeToType'' φ' te' ★ >>= fun te'' =>
weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
- weakTypeToType' φ t wtv >>= fun t' =>
+ weakTypeToType'' φ t wtv >>= fun t' =>
castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
| _ => Error ("weakTypeToType: WETyApp body with type "+++te)
end
(* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two
* to get them back working again *)
- | WECoApp e t => Error "weakExprToStrongExpr: WECoApp not yet implemented"
- | WECoLam cv e => Error "weakExprToStrongExpr: WECoLam not yet implemented"
- | WECast e co => Error "weakExprToStrongExpr: WECast not yet implemented"
- | WELetRec rb e => Error "weakExprToStrongExpr: WELetRec not yet implemented"
- | WECase e tbranches tc avars alts => Error "weakExprToStrongExpr: WECase not yet implemented"
+ | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
+ match te with
+ | WCoFunTy t1 t2 t3 =>
+ weakTypeToType φ t1 >>= fun t1' =>
+ match t1' with
+ haskTypeOfSomeKind κ t1'' =>
+ weakTypeToType'' φ t2 κ >>= fun t2'' =>
+ weakTypeToType'' φ t3 ★ >>= fun t3'' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
+ castExpr "WECoApp" _ e' >>= fun e'' =>
+ OK (ECoApp Γ Δ κ t1'' t2''
+ (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
+ end
+ | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
+ end
+
+ | WECoLam cv e => let (_,_,t1,t2) := cv in
+ weakTypeOfWeakExpr e >>= fun te =>
+ weakTypeToType'' φ te ★ >>= fun te' =>
+ weakTypeToType'' φ t1 cv >>= fun t1' =>
+ weakTypeToType'' φ t2 cv >>= fun t2' =>
+ weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
+ castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
+
+ | WECast e co => let (κ,t1,t2,_) := co in
+ weakTypeToType'' φ t1 ★ >>= fun t1' =>
+ weakTypeToType'' φ t2 ★ >>= fun t2' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
+ castExpr "WECast" _
+ (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
+
+ | WELetRec rb e =>
+ let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
+ in let binds :=
+ (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
+ : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
+ match t with
+ | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
+ | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
+ | T_Branch b1 b2 =>
+ binds b1 >>= fun b1' =>
+ binds b2 >>= fun b2' =>
+ OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
+ end) rb
+ in binds >>= fun binds' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
+ OK (ELetRec Γ Δ ξ lev τ _ binds' e')
+
+ | WECase e tbranches tc avars alts =>
+ mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+ weakTypeToType'' φ tbranches ★ >>= fun tbranches' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' =>
+(fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+ ??{scb
+ : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars'
+ &
+ Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))
+ (scbwv_ξ scb ξ lev) (weakLT' (tbranches' @@ lev))}) :=
+ match t with
+ | T_Leaf None => OK []
+ | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
+ mkStrongAltConPlusJunk' tc ac >>= fun sac =>
+ list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' =>
+ let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
+ weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ)
+ (scbwv_ξ scb ξ lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+ let case_case := tt in OK [ _ ]
+ | T_Branch b1 b2 =>
+ mkTree b1 >>= fun b1' =>
+ mkTree b2 >>= fun b2' =>
+ OK (b1',,b2')
+ end
+) alts >>= fun tree =>
+ castExpr "ECase" _ (ECase Γ Δ ξ lev tc tbranches' avars' e' tree)
end)).
+
+ destruct case_some.
+ simpl.
+ destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
+ matchThings h (unlev (ξ' wev)) "LetRec".
+ destruct wev.
+ rewrite matchTypeVars_pf.
+ clear matchTypeVars_pf.
+ set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
+ destruct e''; try apply (Error error_message).
+ apply OK.
+ apply ELR_leaf.
+ apply e1.
+
+ destruct case_case.
+ clear mkTree t o e' p e p0 p1 p2 alts weakExprToStrongExpr ebranch.
+ exists scb.
+ apply ebranch'.
Defined.
Require Import HaskWeakTypes.
(* TO DO: finish this *)
-Inductive WeakCoercion : Type := weakCoercion : WeakType -> WeakType -> CoreCoercion -> WeakCoercion.
+Inductive WeakCoercion : Type := weakCoercion : Kind -> WeakType -> WeakType -> CoreCoercion -> WeakCoercion.
(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
-Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar.
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
(* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *)
Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar.
Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
match wv with
- | WExprVar (weakExprVar v _ ) => v
- | WTypeVar (weakTypeVar v _ ) => v
- | WCoerVar (weakCoerVar v _ _ ) => v
+ | WExprVar (weakExprVar v _ ) => v
+ | WTypeVar (weakTypeVar v _ ) => v
+ | WCoerVar (weakCoerVar v _ _ _) => v
end.
Coercion weakVarToCoreVar : WeakVar >-> CoreVar.
projects / coq-hetmet.git / commitdiff