Require Import HaskKinds.
Require Import HaskStrongTypes.
Require Import HaskStrong.
-Require Import HaskWeakVars.
Require Import HaskProof.
Section HaskStrongToProof.
Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
match exp as E in Expr Γ Δ ξ τ with
+ | EGlobal Γ Δ ξ _ _ => []
| EVar Γ Δ ξ ev => [ev]
| ELit Γ Δ ξ lit lev => []
| EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
: ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
match exp as E in Expr Γ Δ ξ τ with
+ | EGlobal Γ Δ ξ t wev => 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
end
); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
+ destruct case_EGlobal.
+ apply nd_rule.
+ simpl.
+ destruct t as [t lev].
+ apply (RGlobal _ _ _ _ wev).
+
destruct case_EVar.
apply nd_rule.
unfold mapOptionTree; simpl.
auto.
destruct case_ENote.
+ destruct t.
eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
apply e'.
auto.
End HaskStrongToProof.
-(*
-
-(* Figure 7, production "decl"; actually not used in this formalization *)
-Inductive Decl :=.
-| DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl
-| DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl
-| DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl.
-
-(* Figure 1, production "pgm" *)
-Inductive Pgm Γ Δ :=
- mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
-*)
-