From 976b9bb93bf6ab296b3ac60dcdb4e87b1c665376 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 7 Mar 2011 05:41:51 -0800 Subject: [PATCH] add HaskStrongToProof --- src/Extraction-prefix.hs | 59 ++-- src/Extraction.v | 95 +++++- src/HaskStrongToProof.v | 774 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 899 insertions(+), 29 deletions(-) create mode 100644 src/HaskStrongToProof.v diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 28ea4f1..f9bdbe3 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -1,17 +1,6 @@ {-# OPTIONS_GHC -fno-warn-unused-binds #-} -module Extraction ( coqCoreToStringPass ) +module CoqPass ( coqPassCoreToString, coqPassCoreToCore ) where ---import HsSyn ---import TcType ---import CoreFVs ---import CoreUtils ---import Var ---import BasicTypes ---import Bag ---import VarSet ---import SrcLoc ---import Data.List - import qualified MkCore import qualified TysWiredIn import qualified TysPrim @@ -32,11 +21,23 @@ import qualified DataCon import qualified CoreSyn import qualified Class import qualified Data.Char - import Data.Bits ((.&.), shiftL, (.|.)) import Prelude ( (++), (+), (==), Show, show, Char ) +import qualified Prelude +import qualified GHC.Base + +-- crude way of casting Coq "error monad" into Haskell exceptions +errOrFail :: OrError a -> a +errOrFail (OK x) = x +errOrFail (Error s) = Prelude.error s -dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc) +-- to do: this could be moved into Coq +coreVarToWeakVar :: Var.Var -> WeakVar +coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v)))) +coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v))) +coreVarToWeakVar v | Var.isCoVar v = Prelude.error "FIXME coerVarSort not fully implemented" +coreVarToWeakVar _ = + Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" nat2int :: Nat -> Prelude.Int nat2int O = 0 @@ -67,12 +68,28 @@ coreKindToKind k = else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions" else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: " (Outputable.showSDoc (Outputable.ppr k))) -coreVarSort :: Var.Var -> CoreVarSort -coreVarSort v | Id.isId v = CoreExprVar (Var.varType{-AsType-} v) -coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v)) -coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v) -coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" - -outputableToString :: Outputable -> String +outputableToString :: Outputable.Outputable a => a -> Prelude.String outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x)) +checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool +-- checkTypeEquality t1 t2 = Type.coreEqType (coreViewDeep t1) (coreViewDeep t2) +-- checkTypeEquality t1 t2 = Type.tcEqType (coreViewDeep t1) (coreViewDeep t2) +checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) + +--showType t = outputableToString (Type.expandTypeSynonyms t) +showType t = outputableToString (coreViewDeep t) + +coreViewDeep :: Type.Type -> Type.Type +coreViewDeep t = + case t of + TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv + TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res) + TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg) + TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg) + TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys) + in case Type.coreView t' of + Prelude.Nothing -> t' + Prelude.Just t'' -> t'' + TypeRep.PredTy p -> case Type.coreView t of + Prelude.Nothing -> TypeRep.PredTy p + Prelude.Just t' -> t' diff --git a/src/Extraction.v b/src/Extraction.v index 542b5d4..22564a2 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -4,9 +4,31 @@ Set Printing Width 1300000. Require Import Coq.Lists.List. Require Import Coq.Strings.Ascii. Require Import Coq.Strings.String. -Require Import Main. + +Require Import Preamble. +Require Import General. + +Require Import NaturalDeduction. +Require Import NaturalDeductionToLatex. + +Require Import HaskKinds. +Require Import HaskCoreLiterals. Require Import HaskCoreVars. +Require Import HaskCoreTypes. Require Import HaskCore. +Require Import HaskWeakVars. +Require Import HaskWeakTypes. +Require Import HaskWeak. +Require Import HaskStrongTypes. +Require Import HaskStrong. +Require Import HaskProof. +Require Import HaskCoreToWeak. +Require Import HaskWeakToStrong. +Require Import HaskStrongToProof. +(*Require Import HaskProofToStrong.*) +Require Import HaskProofToLatex. +(*Require Import HaskStrongToWeak.*) +Require Import HaskWeakToCore. Open Scope string_scope. Extraction Language Haskell. @@ -40,12 +62,69 @@ Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .& Unset Extraction Optimize. Unset Extraction AutoInline. -Definition coqCoreToStringPass (s:@CoreExpr CoreVar) : string - := "FIXME". -(* -Definition coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar - := -*) +Axiom fail : forall {A}, string -> A. + Extract Inlined Constant fail => "Prelude.error". + +Section core2proof. + Context (ce:@CoreExpr CoreVar). + + Definition Γ : TypeEnv := nil. + + Definition Δ : CoercionEnv Γ := nil. + + Definition φ : CoreVar->HaskTyVar Γ := + fun cv => (fun TV env => fail "unbound tyvar"). + (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*) + + Definition ψ : CoreVar->HaskCoVar nil Δ + := fun cv => fail ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)). + + (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no + * free tyvars in them *) + Definition ξ : WeakExprVar -> WeakType * list WeakTypeVar + := fun (v:WeakExprVar) => ((v:WeakType),nil). + + Definition header : string := + "\documentclass[9pt]{article}"+++eol+++ + "\usepackage{amsmath}"+++eol+++ + "\usepackage{amssymb}"+++eol+++ + "\usepackage{proof}"+++eol+++ + "\usepackage{mathpartir}"+++eol+++ + "\usepackage{trfrac}"+++eol+++ + "\pdfpagewidth 50in"+++eol+++ + "\pdfpageheight 10in"+++eol+++ + "\def\code#1#2{\Box_{#1} #2}"+++eol+++ + "\begin{document}"+++eol. + + Definition footer : string := + eol+++"\end{document}"+++eol. + + Definition handleExpr (ce:@CoreExpr CoreVar) : string := + match coreExprToWeakExpr ce with + | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n "+++s) + | OK me => + match weakExprToStrongExpr (*(makeClosedExpression me)*) me Γ Δ φ ψ ξ nil with + | Indexed_Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s) + | Indexed_OK τ e => match e with + | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s) + | OK e' => header +++ (nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')) +++ footer + end + end + end. + + Definition handleBind (bind:@CoreBind CoreVar) : string := + match bind with + | CoreNonRec _ e => handleExpr e + | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) "" + end. + + Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string := + fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "". + + Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := + lbinds. + +End core2proof. -Extraction "Extraction.hs" coqCoreToStringPass. +Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v new file mode 100644 index 0000000..c0a0bb3 --- /dev/null +++ b/src/HaskStrongToProof.v @@ -0,0 +1,774 @@ +(*********************************************************************************************************************************) +(* HaskStrongToProof: convert HaskStrong to HaskProof *) +(*********************************************************************************************************************************) + +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. + +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 + * expansion on an entire uniform proof *) +Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ)) + := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)). +Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ)) + := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)). + +Definition pivotContext {Γ}{Δ} a b c τ : + @ND _ (@URule Γ Δ) + [ Γ >> Δ > (a,,b),,c |- τ] + [ Γ >> Δ > (a,,c),,b |- τ]. + set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q. + simpl in *. + eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ]. + eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ]. + apply q. + Defined. + +Definition copyAndPivotContext {Γ}{Δ} a b c τ : + @ND _ (@URule Γ Δ) + [ Γ >> Δ > (a,,b),,(c,,b) |- τ] + [ Γ >> Δ > (a,,c),,b |- τ]. + set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q. + simpl in *. + eapply nd_comp; [ idtac | apply q ]. + clear q. + eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ]. + set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q. + simpl in *. + eapply nd_comp ; [ idtac | apply q ]. + clear q. + apply nd_rule. + apply RAssoc. + Defined. + + + +Context {VV:Type}{eqd_vv:EqDecidable VV}. + + (* maintenance of Xi *) + Definition dropVar (lv:list VV)(v:VV) : ??VV := + if fold_left + (fun a b:bool => if a then true else if b then true else false) + (map (fun lvv => if eqd_dec lvv v then true else false) lv) + false + then None + else Some v. + (* later: use mapOptionTreeAndFlatten *) + Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV := + mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end). + +Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := + match exp as E in Expr Γ Δ ξ τ with + | EVar Γ Δ ξ ev => [ev] + | ELit Γ Δ ξ lit lev => [] + | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) + | ELam Γ Δ ξ t1 t2 lev v pf e => stripOutVars (v::nil) (expr2antecedent e) + | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev)) + | EEsc Γ Δ ξ ec t lev e => expr2antecedent e + | EBrak Γ Δ ξ ec t lev e => expr2antecedent e + | ECast Γ Δ ξ γ t1 t2 lev wfco e => expr2antecedent e + | ENote Γ Δ ξ t n e => expr2antecedent e + | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => expr2antecedent e + | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => expr2antecedent e + | ETyApp Γ Δ κ σ τ ξ l pf e => expr2antecedent e + | ELetRec Γ Δ ξ l τ vars branches body => + let branch_context := eLetRecContext branches + in let all_contexts := (expr2antecedent body),,branch_context + in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts + | ECase Γ Δ ξ lev tc avars tbranches e' alts => + ((fix varsfromalts (alts: + Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc avars + & Expr (sac_Γ scb Γ) + (sac_Δ scb Γ avars (weakCK'' Δ)) + (scbwv_ξ scb ξ lev) + (weakLT' (tbranches@@lev)) } + ): Tree ??VV := + match alts with + | T_Leaf None => [] + | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h)) + | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2) + end) alts),,(expr2antecedent e') +end +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_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. + +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_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_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_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2) + end. + + +Lemma stripping_nothing_is_inert + {Γ:TypeEnv} + (ξ:VV -> LeveledHaskType Γ) + tree : + stripOutVars nil tree = tree. + induction tree. + simpl; destruct a; reflexivity. + unfold stripOutVars. + fold stripOutVars. + simpl. + fold (stripOutVars nil). + rewrite IHtree1. + rewrite IHtree2. + reflexivity. + Qed. + + + +Definition arrangeContext + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + ctx (* initial context *) + τ (* type of succedent *) + (ξ:VV -> LeveledHaskType Γ) + : + + (* a proof concluding in a context where that variable does not appear *) + sum (ND (@URule Γ Δ) + [Γ >> Δ > mapOptionTree ξ ctx |- τ] + [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] |- τ]) + + (* or a proof concluding in a context where that variable appears exactly once in the left branch *) + (ND (@URule Γ Δ) + [Γ >> Δ > mapOptionTree ξ ctx |- τ] + [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]). + + induction ctx; simpl in *. + + refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *. + + (* nonempty leaf *) + destruct case_Some. + unfold stripOutVars in *; simpl. + unfold dropVar. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + destruct (eqd_dec v v'); simpl in *. + + (* where the leaf is v *) + apply inr. + subst. + apply nd_rule. + apply RuCanL. + + (* where the leaf is NOT v *) + apply inl. + apply nd_rule. + apply RuCanR. + + (* empty leaf *) + destruct case_None. + apply inl; simpl in *. + apply nd_rule. + apply RuCanR. + + (* branch *) + refine ( + match IHctx1 with + | inr lpf => + match IHctx2 with + | inr rpf => let case_Both := tt in _ + | inl rpf => let case_Left := tt in _ + end + | inl lpf => + match IHctx2 with + | inr rpf => let case_Right := tt in _ + | inl rpf => let case_Neither := tt in _ + end + end); clear IHctx1; clear IHctx2. + + destruct case_Neither. + apply inl. + eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ]. + exact (nd_comp + (* order will not matter because these are central as morphisms *) + (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) + (ext_left _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))). + + + destruct case_Right. + apply inr. + fold (stripOutVars (v::nil)). + set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q. + simpl in *. + eapply nd_comp. + apply q. + clear q. + clear lpf. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ]. + set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ] + [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v]) |- τ]) as qq. + apply qq. + clear qq. + apply rpf. + + destruct case_Left. + apply inr. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + fold (stripOutVars (v::nil)). + eapply nd_comp; [ idtac | eapply pivotContext ]. + set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'. + set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq. + simpl in *. + eapply nd_comp; [ idtac | apply qq ]. + clear qq rpf' rpf. + set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q. + apply q. + clear q. + apply lpf. + + destruct case_Both. + apply inr. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + fold (stripOutVars (v::nil)). + eapply nd_comp; [ idtac | eapply copyAndPivotContext ]. + exact (nd_comp + (* order will not matter because these are central as morphisms *) + (ext_right _ _ _ lpf) + (ext_left _ _ _ rpf)). + + Defined. + +(* same as before, but use RWeak if necessary *) +Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : + ND (@URule Γ Δ) + [Γ >> Δ>mapOptionTree ξ ctx |- τ] + [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]. + set (arrangeContext Γ Δ v ctx τ ξ) as q. + destruct q; auto. + eapply nd_comp; [ apply n | idtac ]. + clear n. + refine (ext_left _ _ _ (nd_rule (RWeak _ _))). + Defined. + +Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, + ND (@URule Γ Δ) + [Γ >> Δ>(mapOptionTree ξ ctx) |- z] + [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z]. + + induction v. + destruct a. + unfold mapOptionTree in *. + simpl in *. + fold (mapOptionTree ξ) in *. + intros. + apply arrangeContextAndWeaken. + + unfold mapOptionTree; simpl in *. + intros. + rewrite (@stripping_nothing_is_inert Γ); auto. + apply nd_rule. + apply RuCanR. + intros. + unfold mapOptionTree in *. + simpl in *. + fold (mapOptionTree ξ) in *. + set (mapOptionTree ξ) as X in *. + + set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'. + unfold stripOutVars in IHv2'. + simpl in IHv2'. + fold (stripOutVars (leaves v2)) in IHv2'. + fold (stripOutVars (leaves v1)) in IHv2'. + unfold X in IHv2'. + unfold mapOptionTree in IHv2'. + simpl in IHv2'. + fold (mapOptionTree ξ) in IHv2'. + fold X in IHv2'. + set (nd_comp (IHv1 _ _) IHv2') as qq. + eapply nd_comp. + apply qq. + clear qq IHv2' IHv2 IHv1. + + assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)). + admit. + rewrite H. + clear H. + + (* FIXME TOTAL BOGOSITY *) + assert ((stripOutVars (leaves v2) v1) = v1). + admit. + rewrite H. + clear H. + + apply nd_rule. + apply RCossa. + Defined. + +Definition update_ξ'' {Γ} ξ tree lev := +(update_ξ ξ + (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩) + (leaves tree))). + +Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ) v tree lev : + mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree) + = mapOptionTree ξ (stripOutVars (v :: nil) tree). + induction tree; simpl in *; try reflexivity; auto. + + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *. + destruct a; simpl; try reflexivity. + unfold update_ξ. + simpl. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + unfold update_ξ. + unfold dropVar. + simpl. + set (eqd_dec v v0) as q. + assert (q=eqd_dec v v0). + reflexivity. + destruct q. + reflexivity. + rewrite <- H. + reflexivity. + auto. + unfold mapOptionTree. + unfold mapOptionTree in IHtree1. + unfold mapOptionTree in IHtree2. + simpl in *. + simpl in IHtree1. + fold (stripOutVars (v::nil)). + rewrite <- IHtree1. + rewrite <- IHtree2. + reflexivity. + Qed. + + + +Lemma updating_stripped_tree_is_inert' + {Γ} lev + (ξ:VV -> LeveledHaskType Γ) + tree tree2 : + mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2) + = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2). +admit. + Qed. + +Lemma updating_stripped_tree_is_inert'' + {Γ} + (ξ:VV -> LeveledHaskType Γ) + v tree lev : + mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree) + = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree). +admit. + Qed. + +(* +Lemma updating_stripped_tree_is_inert''' + {Γ} + (ξ:VV -> LeveledHaskType Γ) +{T} + (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree +: + mapOptionTree (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree) + = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree). +admit. + Qed. +*) + +(* IDEA: use multi-conclusion proofs instead *) +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) + | 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), + + eLetRecTypes branches = + mapOptionTree (update_ξ'' ξ tree lev) + (mapOptionTree (@fst _ _) tree). + intros. + induction branches. + reflexivity. + simpl. + unfold update_ξ. + unfold mapOptionTree; simpl. +admit. +admit. + Qed. + +Lemma letRecSubproofsToND Γ Δ ξ lev tree branches + : LetRecSubproofs Γ Δ ξ lev tree branches -> + ND Rule [] + [ Γ > Δ > + mapOptionTree ξ (eLetRecContext branches) + |- + eLetRecTypes branches + ]. + intro X. + induction X; intros; simpl in *. + apply nd_rule. + apply REmptyGroup. + unfold mapOptionTree. + simpl. + apply n. + eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod; auto. + Defined. + + +Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ) tree z lev, + mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z. +admit. + Qed. + + + +Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : + forall branches body, + ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] -> + LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches -> + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]]. + + (* NOTE: how we interpret stuff here affects the order-of-side-effects *) + simpl. + intro branches. + intro body. + intro pf. + intro lrsp. + set ((update_ξ ξ + (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩) + (leaves tree)))) as ξ' in *. + set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx. + set (mapOptionTree (@fst _ _) tree) as pctx. + set (mapOptionTree ξ' pctx) as passback. + set (fun a b => @RLetRec Γ Δ a b passback) as z. + eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. + clear z. + + set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'. + unfold passback in *; clear passback. + unfold pctx in *; clear pctx. + eapply UND_to_ND in q'. + + unfold ξ' in *. + set (@updating_stripped_tree_is_inert') as zz. + unfold update_ξ'' in *. + rewrite zz in q'. + clear zz. + clear ξ'. + simpl in q'. + + eapply nd_comp; [ idtac | apply q' ]. + clear q'. + unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)). + + simpl. + + set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. + + eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod; auto. + rewrite dork in q. + set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz. + unfold update_ξ'' in *. + rewrite <- zz in q. + apply q. + Defined. + +(* +Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx), + unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars). +admit. + Qed. +*) +Lemma cheat : forall {T} (a b:T), a=b. + admit. + Defined. + +Definition expr2proof : + forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]]. + + refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp} + : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] := + match exp as E in Expr Γ Δ ξ τ with + | 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 + let e1' := expr2proof _ _ _ _ e1 in + let e2' := expr2proof _ _ _ _ e2 in _ + | ELam Γ Δ ξ t1 t2 lev v pf e => let case_ELam := tt in + let e' := expr2proof _ _ _ _ e in _ + | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in + let pf_let := (expr2proof _ _ _ _ ev) in + let pf_body := (expr2proof _ _ _ _ ebody) in _ + | ELetRec Γ Δ ξ lev t tree branches ebody => + let e' := expr2proof _ _ _ _ ebody in + let ξ' := update_ξ'' ξ tree lev in + let subproofs := ((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 Γ Δ ξ t l v e => (fun e' => let case_elr_leaf := tt in _) (expr2proof _ _ _ _ e) + | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) + end + ) _ _ _ _ tree branches) in + let case_ELetRec := tt in _ + | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in let e' := expr2proof _ _ _ _ e in _ + | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in let e' := expr2proof _ _ _ _ e in _ + | ECast Γ Δ ξ γ t1 t2 lev wfco e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _ + | ENote Γ Δ ξ t n e => let case_ENote := tt in let e' := expr2proof _ _ _ _ e in _ + | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in let e' := expr2proof _ _ _ _ e in _ + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _ + | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _ + | ETyApp Γ Δ κ σ τ ξ l pf e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _ + | ECase Γ Δ ξ lev tbranches tc avars e alts => +(* + let dcsp := + ((fix mkdcsp (alts: + Tree ??{ scb : StrongCaseBranchWithVVs tc avars + & 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 + | 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) + end +); clear exp ξ' τ' Γ' Δ'; simpl in *. + + destruct case_EVar. + apply nd_rule. + unfold mapOptionTree; simpl. + destruct (ξ ev). + apply RVar. + + destruct case_ELit. + apply nd_rule. + apply RLit. + + destruct case_EApp. + unfold mapOptionTree; simpl; fold (mapOptionTree ξ). + eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod; auto. + + destruct case_ELam; intros. + unfold mapOptionTree; simpl; fold (mapOptionTree ξ). + eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ]. + set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'. + set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx. + apply UND_to_ND in pfx. + unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx. + unfold ξ' in pfx. + fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx. + rewrite updating_stripped_tree_is_inert in pfx. + unfold update_ξ in pfx. + destruct (eqd_dec v v). + eapply nd_comp; [ idtac | apply pfx ]. + clear pfx. + apply e'. + assert False. + apply n. + auto. + inversion H. + apply pf. + + destruct case_ELet; intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod; [ idtac | apply pf_let]. + clear pf_let. + eapply nd_comp; [ apply pf_body | idtac ]. + clear pf_body. + fold (@mapOptionTree VV). + fold (mapOptionTree ξ). + set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'. + set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n. + unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n. + unfold ξ' in n. + rewrite updating_stripped_tree_is_inert in n. + unfold update_ξ in n. + destruct (eqd_dec lev lev). + unfold ξ'. + unfold update_ξ. + apply UND_to_ND in n. + apply n. + assert False. apply n0; auto. inversion H. + + destruct case_EEsc. + eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ]. + apply e'. + + destruct case_EBrak; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ]. + apply e'. + + destruct case_ECast. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast with (γ:=γ)]. + apply e'. + auto. + + destruct case_ENote. + eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ]. + apply e'. + auto. + + destruct case_ETyApp; 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'. + auto. + auto. + + destruct case_ECoApp; 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. + assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))). + apply update_ξ_and_reapply. + rewrite H. + simpl in q. + unfold mapOptionTree in q; simpl in q. + set (@updating_stripped_tree_is_inert''') as u. + unfold mapOptionTree in u. + rewrite u in q. + clear u H. + unfold weakenX' in *. + admit. + unfold mapOptionTree in *. + replace + (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0)) + with + (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. + +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 Γ Δ. +*) -- 1.7.10.4