From: Adam Megacz Date: Mon, 7 Mar 2011 13:41:56 +0000 (-0800) Subject: add HaskProofToStrong skeleton implementation X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=c9082c6556689b31f4ae649c3280f09fb71546ff add HaskProofToStrong skeleton implementation --- diff --git a/src/Extraction.v b/src/Extraction.v index 363e17f..1a26e58 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -25,7 +25,7 @@ Require Import HaskProof. Require Import HaskCoreToWeak. Require Import HaskWeakToStrong. Require Import HaskStrongToProof. -(*Require Import HaskProofToStrong.*) +Require Import HaskProofToStrong. Require Import HaskProofToLatex. Require Import HaskStrongToWeak. Require Import HaskWeakToCore. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v new file mode 100644 index 0000000..5039004 --- /dev/null +++ b/src/HaskProofToStrong.v @@ -0,0 +1,159 @@ +(*********************************************************************************************************************************) +(* HaskProofToStrong: convert HaskProof to HaskStrong *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.Init.Specif. +Require Import HaskKinds. +Require Import HaskStrongTypes. +Require Import HaskStrong. +Require Import HaskProof. + +Section HaskProofToStrong. + + Context + {VV:Type} + {eqdec_vv:EqDecidable VV} + {fresh: forall (l:list VV), { lf:VV & distinct (lf::l) }}. + + Definition Exprs (Γ:TypeEnv)(Δ:CoercionEnv Γ)(ξ:VV -> LeveledHaskType Γ)(τ:Tree ??(LeveledHaskType Γ)) := + ITree _ (fun τ => Expr Γ Δ ξ τ) τ. + + Definition judg2exprType (j:Judg) : Type := + match j with + (Γ > Δ > Σ |- τ) => { ξ:VV -> LeveledHaskType Γ & Exprs Γ Δ ξ τ } + end. + + (* reminder: need to pass around uniq-supplies *) + Definition rule2expr + : forall h j + (r:Rule h [j]), + ITree _ judg2exprType h -> + judg2exprType j. + + intros. + destruct j. + refine (match r as R in Rule H C return C=[Γ > Δ > t |- t0] -> _ with + | RURule a b c d e => let case_RURule := tt in _ + | RNote x n z => let case_RNote := tt in _ + | RLit Γ Δ l _ => let case_RLit := tt in _ + | RVar Γ Δ σ p => let case_RVar := tt in _ + | RLam Γ Δ Σ tx te p x => let case_RLam := tt in _ + | RCast Γ Δ Σ σ τ γ p x => let case_RCast := tt in _ + | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _ + | RAppT Γ Δ Σ κ σ τ p y => let case_RAppT := tt in _ + | RAppCo Γ Δ Σ κ σ₁ σ₂ σ γ p => let case_RAppCo := tt in _ + | RAbsCo Γ Δ Σ κ σ cc σ₁ σ₂ p y => let case_RAbsCo := tt in _ + | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ + | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ + | RLetRec Γ p lri x y => let case_RLetRec := tt in _ + | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _ + | REmptyGroup _ _ => let case_REmptyGroup := tt in _ + | RCase Σ Γ T κlen κ θ ldcd τ => let case_RCase := tt in _ + | RBrak Σ a b c n m => let case_RBrak := tt in _ + | REsc Σ a b c n m => let case_REsc := tt in _ + end (refl_equal _) ); intros. + + destruct case_RURule. + destruct d; [ destruct o | idtac ]; inversion H; subst. + clear H. + destruct u. + refine (match e as R in URule H C return C=[a >> b > t1 |- t2] -> _ with + | RLeft h c ctx r => let case_RLeft := tt in _ + | RRight h c ctx r => let case_RRight := tt in _ + | RCanL t a => let case_RCanL := tt in _ + | RCanR t a => let case_RCanR := tt in _ + | RuCanL t a => let case_RuCanL := tt in _ + | RuCanR t a => let case_RuCanR := tt in _ + | RAssoc t a b c => let case_RAssoc := tt in _ + | RCossa t a b c => let case_RCossa := tt in _ + | RExch t a b => let case_RExch := tt in _ + | RWeak t a => let case_RWeak := tt in _ + | RCont t a => let case_RCont := tt in _ + end (refl_equal _) ); intros. + + destruct case_RCanL. admit. + destruct case_RCanR. admit. + destruct case_RuCanL. admit. + destruct case_RuCanR. admit. + destruct case_RAssoc. admit. + destruct case_RCossa. admit. + destruct case_RLeft. admit. + destruct case_RRight. admit. + destruct case_RExch. admit. + destruct case_RWeak. admit. + destruct case_RCont. admit. + destruct case_RBrak. admit. + destruct case_REsc. admit. + destruct case_RNote. admit. + destruct case_RLit. admit. + destruct case_RVar. admit. + destruct case_RLam. admit. + destruct case_RCast. admit. + destruct case_RBindingGroup. admit. + destruct case_RApp. admit. + destruct case_RLet. admit. + destruct case_REmptyGroup. admit. + destruct case_RAppT. admit. + destruct case_RAbsT. admit. + destruct case_RAppCo. admit. + destruct case_RAbsCo. admit. + destruct case_RLetRec. admit. + destruct case_RCase. admit. + Defined. + + Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c. + refine (( + fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j := + match pn in @ClosedND _ _ J return ITree _ judg2exprType J with + | cnd_weak => let case_nil := tt in _ + | cnd_rule h c cnd' r => let case_rule := tt in (fun rest => _) (closed2expr' _ cnd') + | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2) + end)); clear closed2expr'; intros; subst. + + destruct case_nil. + apply INone. + + destruct case_rule. + set (@rule2expr h) as q. + destruct c. + destruct o. + apply ILeaf. + eapply rule2expr. + apply r. + apply rest. + + apply no_rules_with_empty_conclusion in r. + inversion r. + auto. + + simpl. + apply systemfc_all_rules_one_conclusion in r. + inversion r. + + destruct case_branch. + apply IBranch. + apply rest1. + apply rest2. + Defined. + + Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ & Expr Γ Δ ξ τ }. + intro pf. + set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd. + apply closed2expr in cnd. + inversion cnd; subst. + simpl in X. + clear cnd pf. + destruct X. + exists x. + inversion e. + subst. + apply X. + Defined. + +End HaskProofToStrong.