OK (eol+++eol+++eol+++
"\begin{preview}"+++eol+++
"$\displaystyle "+++
- toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
+ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
" $"+++eol+++
"\end{preview}"+++eol+++eol+++eol)
)))))))).
(addErrorMessage ("HaskStrong...")
(let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
- hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
+ hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
in (* insert HaskProof-to-HaskProof manipulations here *)
- OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ@@nil) _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' =>
(snd e') >>= fun e'' =>
strongExprToWeakExpr hetmet_brak' hetmet_esc'
Definition judg2exprType (j:Judg) : Type :=
match j with
(Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
- FreshM (ITree _ (fun t => Expr Γ Δ ξ (t @@ l)) τ)
+ FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
end.
- Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
+ Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
intros.
inversion X; auto.
Defined.
Defined.
Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
- forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ (t@@l)) τ).
+ forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
ujudg2exprType Γ ξ Δ h t l ->
Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
ITree (HaskType Γ ★)
- (fun t : HaskType Γ ★ => Expr Γ Δ ξ' (t @@ l))
+ (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
(mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
-> ELetRecBindings Γ Δ ξ' l varstypes.
intros.
prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
((fun sac => FreshM
{ scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
- & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
+ & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
+ (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
intro pcb.
intro X.
simpl in X.
destruct case_RVar.
apply ILeaf; simpl; intros; refine (return ILeaf _ _).
- destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
- apply EVar.
+ destruct vars; simpl in H; inversion H; destruct o. inversion H1.
+ set (@EVar _ _ _ Δ ξ v) as q.
+ rewrite <- H2 in q.
+ simpl in q.
+ apply q.
inversion H.
destruct case_RGlobal.
admit.
Defined.
- Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
- {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [unlev τ] @ getlev τ] ->
- FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
+ Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
+ {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
+ FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
intro pf.
set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
apply closed2expr in cnd.
exists ξ.
apply ileaf in it.
simpl in it.
- destruct τ.
apply it.
apply INone.
Defined.
}.
Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
- Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
+ Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> HaskType Γ ★ -> HaskLevel Γ -> Type :=
(* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
- | EGlobal: forall Γ Δ ξ (g:Global Γ) v lev, Expr Γ Δ ξ (g v @@ lev)
+ | EGlobal: forall Γ Δ ξ (g:Global Γ) v lev, Expr Γ Δ ξ (g v) lev
- | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
- | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
- | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l)
- | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_xi ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l)
- | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_xi ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l)
- | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l))
- | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
- | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l,
- Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l)
- | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t
- | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l)
- | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l,
- Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ @@ l)
- | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l,
- Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l)
+ | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (unlev (ξ ev)) (getlev (ξ ev))
+ | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit) l
+ | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1) l -> Expr Γ Δ ξ t2 l -> Expr Γ Δ ξ (t1) l
+ | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_xi ξ l ((ev,t1)::nil)) t2 l -> Expr Γ Δ ξ (t1--->t2) l
+ | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ tv l ->Expr Γ Δ (update_xi ξ l ((ev,tv)::nil)) t l -> Expr Γ Δ ξ t l
+ | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]>) l -> Expr Γ Δ ξ t (ec::l)
+ | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ t (ec::l) -> Expr Γ Δ ξ (<[ ec |- t ]>) l
+ | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, Expr Γ Δ ξ t1 l -> Expr Γ Δ ξ t2 l
+ | ENote : ∀ Γ Δ ξ t l, Note -> Expr Γ Δ ξ t l -> Expr Γ Δ ξ t l
+ | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l
+ | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l
+ | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l
| ETyLam : ∀ Γ Δ ξ κ σ l,
- Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
+ Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)) (weakL l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
| ECase : forall Γ Δ ξ l tc tbranches atypes,
- Expr Γ Δ ξ (caseType tc atypes @@ l) ->
+ Expr Γ Δ ξ (caseType tc atypes) l ->
Tree ??{ sac : _
& { scb : StrongCaseBranchWithVVs tc atypes sac
& Expr (sac_gamma sac Γ)
(sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l)
- (weakLT' (tbranches@@l)) } } ->
- Expr Γ Δ ξ (tbranches @@ l)
+ (weakT' tbranches)
+ (weakL' l) } } ->
+ Expr Γ Δ ξ tbranches l
| ELetRec : ∀ Γ Δ ξ l τ vars,
distinct (leaves (mapOptionTree (@fst _ _) vars)) ->
let ξ' := update_xi ξ l (leaves vars) in
- ELetRecBindings Γ Δ ξ' l vars ->
- Expr Γ Δ ξ' (τ@@l) ->
- Expr Γ Δ ξ (τ@@l)
+ ELetRecBindings Γ Δ ξ' l vars ->
+ Expr Γ Δ ξ' τ l ->
+ Expr Γ Δ ξ τ 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 : ∀ Γ Δ ξ l v t, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)]
+ | ELR_leaf : ∀ Γ Δ ξ l v t, Expr Γ Δ ξ t l -> ELetRecBindings Γ Δ ξ l [(v,t)]
| ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
.
Context {ToStringVV:ToString VV}.
Context {ToLatexVV:ToLatex VV}.
- Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
+ Fixpoint exprToString {Γ}{Δ}{ξ}{τ}{l}(exp:Expr Γ Δ ξ τ l) : string :=
match exp with
| EVar Γ' _ ξ' ev => "var."+++ toString ev
| EGlobal Γ' _ ξ' g v _ => "global." +++ toString (g:CoreVar)
| EApp Γ' _ _ _ _ _ e1 e2 => "("+++exprToString e1+++")("+++exprToString e2+++")"
| EEsc Γ' _ _ ec t _ e => "~~("+++exprToString e+++")"
| EBrak Γ' _ _ ec t _ e => "<["+++exprToString e+++"]>"
- | ENote _ _ _ _ n e => "note."+++exprToString e
+ | ENote _ _ _ _ n _ e => "note."+++exprToString e
| ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")"
| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)"
| ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2"
| ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
| ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
end.
- Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }.
+ Instance ExprToString Γ Δ ξ τ l : ToString (Expr Γ Δ ξ τ l) := { toString := exprToString }.
End HaskStrong.
Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
apply q.
Qed.
-Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
- match exp as E in Expr Γ Δ ξ τ with
+Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : Tree ??VV :=
+ match exp as E in Expr Γ Δ ξ τ l with
| EGlobal Γ Δ ξ _ _ _ => []
| EVar Γ Δ ξ ev => [ev]
| ELit Γ Δ ξ lit lev => []
| EEsc Γ Δ ξ ec t lev e => expr2antecedent e
| EBrak Γ Δ ξ ec t lev e => expr2antecedent e
| ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
- | ENote Γ Δ ξ t n e => expr2antecedent e
+ | ENote Γ Δ ξ t l n e => expr2antecedent e
| ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
| ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
& Expr (sac_gamma sac Γ)
(sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l)
- (weakLT' (tbranches@@l)) } }
+ (weakT' tbranches) (weakL' l)} }
): Tree ??VV :=
match alts with
| T_Leaf None => []
& Expr (sac_gamma sac Γ)
(sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l)
- (weakLT' (tbranches@@l)) } })
+ (weakT' tbranches) (weakL' l) } })
: { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
destruct alt.
exists x.
??{sac : StrongAltCon &
{scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
- (scbwv_xi scb ξ l) (weakLT' (tbranches @@ l))}}),
+ (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
(mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
(mapOptionTree mkProofCaseBranch alts'))
Qed.
Definition expr2proof :
- forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
- ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev τ] @ getlev τ].
+ forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l),
+ ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l].
- refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
- : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [unlev τ'] @ getlev τ'] :=
- match exp as E in Expr Γ Δ ξ τ with
+ refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp}
+ : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] :=
+ match exp as E in Expr Γ Δ ξ τ l with
| EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
| EVar Γ Δ ξ ev => let case_EVar := tt in _
| ELit Γ Δ ξ lit lev => let case_ELit := tt in _
| EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
- (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
- | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2)
+ | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
- (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
+ (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody)
| ELetRec Γ Δ ξ lev t tree disti branches ebody =>
let ξ' := update_xi ξ lev (leaves tree) in
- let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
+ let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody)
((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
(branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
: 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 Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
+ | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e)
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
end
) _ _ _ _ tree branches)
- | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
- | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
- | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
- | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
- | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
- | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
- | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
- | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECase Γ Δ ξ l tc tbranches atypes e alts' =>
let dcsp :=
((fix mkdcsp (alts:
& Expr (sac_gamma sac Γ)
(sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l)
- (weakLT' (tbranches@@l)) } })
+ (weakT' tbranches) (weakL' l) } })
: ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
match alts as ALTS return ND Rule []
(mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
| T_Leaf (Some x) =>
match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
existT sac (existT scbx ex) =>
- (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
+ (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex)
end
end) alts')
- in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
end
- ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
+ ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp.
destruct case_EGlobal.
apply nd_rule.
auto.
destruct case_ENote.
- destruct t.
eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
apply e'.
auto.
| (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev
end.
- Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
+ Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}{l}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ l)
: InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
-> UniqM WeakExpr :=
- match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
+ match exp as E in @Expr _ _ G D X T L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
| EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
| EGlobal Γ' _ ξ' g v lev => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
| EBrak Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
; bind e' = exprToWeakExpr χ e ite
; return WEBrak hetmet_brak (ec _ ite) e' t'
- | ENote _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite
+ | ENote _ _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite
; return WENote n e'
| ETyApp Γ Δ κ σ τ ξ l e => fun ite => bind t' = typeToWeakType τ ite
; bind e' = exprToWeakExpr χ e ite
; bind tbranches' = @typeToWeakType Γ _ tbranches ite
; bind escrut' = exprToWeakExpr χ escrut ite
; bind branches' =
- ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
+ ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ _ } })
: UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match tree with
| T_Leaf None => return []
end.
- Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
+ Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}{l}(exp:@Expr _ eqVV Γ Δ ξ τ l)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=
match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
Defined.
(* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
-Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
- : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
+Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l)
+ : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l').
apply (addErrorMessage ("castExpr " +++ err_msg)).
intros.
- destruct τ as [τ l].
- destruct τ' as [τ' l'].
destruct (eqd_dec l l'); [ idtac
| apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
" got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
(ig:CoreVar -> bool)
(τ:HaskType Γ ★)
(lev:HaskLevel Γ),
- WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
+ WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ).
refine ((
fix weakExprToStrongExpr
(Γ:TypeEnv)
(ig:CoreVar -> bool)
(τ:HaskType Γ ★)
(lev:HaskLevel Γ)
- (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
+ (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) :=
addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
match we with
| WEVar v => if ig v
- then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
- else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ 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)
+ | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev)
| WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
weakTypeOfWeakExpr ebody >>= fun tbody =>
let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in
let ig' := update_ig ig ((ev:CoreVar)::nil) in
weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
- castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
+ castExpr we "WELam" τ lev (ELam Γ Δ ξ tv tbody' lev ev ebody')
| WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
- castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
+ castExpr we "WEBrak" τ lev (EBrak Γ Δ ξ ec' tbody' lev e')
| WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
match lev with
| nil => Error "ill-leveled escapification"
| ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
- >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
+ >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' lev' e')
end
| WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
- | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
+ | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ _ n e')
| WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
weakExprToStrongExpr _ (weakCE Δ) φ2
(fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
- >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
+ >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
| WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
match te with
weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
- castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
+ castExpr we "WETyApp" _ _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
| _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
end
weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
- castExpr we "WECoApp" _ e' >>= fun e'' =>
+ castExpr we "WECoApp" _ _ e' >>= fun e'' =>
OK (ECoApp Γ Δ κ t1'' t2''
(weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
end
weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' =>
- castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
+ castExpr we "WECoLam" _ _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
| WECast e co => let (t1,t2) := weakCoercionTypes co in
weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
- castExpr we "WECast" _
+ castExpr we "WECast" _ _
(ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
| WELetRec rb e =>
weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
(fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
- Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakLT' (tbranches' @@ lev))}}) :=
+ Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakT' tbranches')(weakL' lev)}}) :=
match t with
| T_Leaf None => OK []
| T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
end) alts >>= fun tree =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
- castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
+ castExpr we "ECase" τ lev (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
end)); try clear binds; try apply ConcatenableString.
destruct case_some.
projects / coq-hetmet.git / commitdiff