From: Adam Megacz Date: Sat, 19 Mar 2011 21:15:34 +0000 (-0700) Subject: improve HaskProofToStrong, although its messier now X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=4359342db4052c77b802ce256856df71387e7a62 improve HaskProofToStrong, although its messier now --- diff --git a/src/Extraction.v b/src/Extraction.v index 66a69da..43d404f 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -1,9 +1,9 @@ (* need this or the Haskell extraction fails *) Set Printing Width 1300000. -Require Import Coq.Lists.List. Require Import Coq.Strings.Ascii. Require Import Coq.Strings.String. +Require Import Coq.Lists.List. Require Import Preamble. Require Import General. @@ -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. @@ -33,13 +33,14 @@ Require Import HaskWeakToCore. Open Scope string_scope. Extraction Language Haskell. +(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*) +(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*) +(*Extract Inlined Constant map => "Prelude.map".*) + (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *) Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. Extract Inductive list => "([])" [ "([])" "(:)" ]. -(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*) -(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*) -Extract Inlined Constant map => "Prelude.map". -Extract Inductive string => "Prelude.String" [ "([])" "(:)" ]. +Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. Extract Inductive prod => "(,)" [ "(,)" ]. Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. @@ -47,10 +48,9 @@ Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. Extract Inductive unit => "()" [ "()" ]. Extract Inlined Constant string_dec => "(==)". Extract Inlined Constant ascii_dec => "(==)". -Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. (* adapted from ExtrOcamlString.v *) -Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'". +Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'". Extract Constant zero => "'\000'". Extract Constant one => "'\001'". Extract Constant shift => "shiftAscii". @@ -58,10 +58,10 @@ Extract Constant shift => "shiftAscii". Unset Extraction Optimize. Unset Extraction AutoInline. - Variable Name : Type. Extract Inlined Constant Name => "Name.Name". Variable mkSystemName : Unique -> string -> nat -> Name. - Extract Inlined Constant mkSystemName => "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))". + Extract Inlined Constant mkSystemName => + "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))". Variable mkTyVar : Name -> Kind -> CoreVar. Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))". Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar. @@ -116,6 +116,7 @@ Section core2proof. eol+++"\end{document}"+++ eol. + Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string := addErrorMessage ("input CoreSyn: " +++ ce) (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) ( @@ -162,6 +163,124 @@ Section core2proof. Context (hetmet_esc : WeakExprVar). Context (uniqueSupply : UniqSupply). + Definition useUniqueSupply {T}(ut:UniqM T) : ???T := + match ut with + uniqM f => + f uniqueSupply >>= fun x => OK (snd x) + end. + + Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }. + intros. + induction ln. + exists O. + intros. + inversion H. + destruct IHln as [n pf]. + exists (plus (S n) a). + intros. + destruct H. + omega. + fold (@In _ n' ln) in H. + set (pf n' H) as q. + omega. + Defined. + + Definition FreshNat : @FreshMonad nat. + refine {| FMT := fun T => nat -> prod nat T + ; FMT_fresh := _ + |}. + Focus 2. + intros. + refine ((S H),_). + set (larger tl) as q. + destruct q as [n' pf]. + exists n'. + intros. + set (pf _ H0) as qq. + omega. + + refine {| returnM := fun a (v:a) => _ |}. + intro n. exact (n,v). + intros. + set (X H) as q. + destruct q as [n' v]. + set (X0 v n') as q'. + exact q'. + Defined. + + Definition unFresh {T} : @FreshM _ FreshNat T -> T. + intros. + destruct X. + exact O. + apply t. + Defined. + + Definition env := ★::nil. + Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _). + Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]]. + eapply nd_comp. + eapply nd_comp. + eapply nd_rule. + apply RVar. + eapply nd_rule. + eapply (RURule _ _ _ _ (RuCanL _ _)) . + eapply nd_rule. + eapply RLam. + Defined. +(* + Definition TInt : HaskType nil ★. + assert (tyConKind' intPrimTyCon = ★). + admit. + rewrite <- H. + unfold HaskType; intros. + apply TCon. + Defined. + + Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]]. + apply nd_rule. + apply RVar. + Defined. + + Definition idtype := + HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))). + + Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]]. + eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ]. + apply idproof0. + Defined. +*) +(* + Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := + addErrorMessage ("input CoreSyn: " +++ ce) + (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) ( + coreExprToWeakExpr ce >>= fun we => + addErrorMessage ("WeakExpr: " +++ we) + ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we)) + ((weakTypeOfWeakExpr we) >>= fun t => + (addErrorMessage ("WeakType: " +++ t) + ((weakTypeToTypeOfKind φ t ★) >>= fun τ => + addErrorMessage ("HaskType: " +++ τ) + ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => + (let haskProof := @expr2proof _ _ _ _ _ _ e + in (* insert HaskProof-to-HaskProof manipulations here *) + (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof)) + >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e')) +(* + >>= fun e' => + Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e')) + *) +) +)))))))). +(* Error "X").*) +(* + strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e') + INil + >>= fun q => Error (toString q) + ))))))))). +*) +*) + Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := addErrorMessage ("input CoreSyn: " +++ ce) (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) ( @@ -173,13 +292,18 @@ Section core2proof. ((weakTypeToTypeOfKind φ t ★) >>= fun τ => ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => - (* insert HaskStrong-to-HaskStrong manipulations here *) - strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply e INil - >>= fun q => OK (weakExprToCoreExpr q) -(* - OK (weakExprToCoreExpr we) -*) - )))))))). + + (addErrorMessage ("HaskStrong...") + (let haskProof := @expr2proof _ _ _ _ _ _ e + in (* insert HaskProof-to-HaskProof manipulations here *) + OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) + >>= fun e' => + (snd e') >>= fun e'' => + strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e'') INil + >>= fun q => + OK (weakExprToCoreExpr q) + )))))))))). Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) := match coreToCoreExpr' ce with @@ -212,6 +336,7 @@ Section core2proof. end. End core2proof. - +(*Set Extraction Optimize.*) +(*Set Extraction AutoInline.*) Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore. diff --git a/src/General.v b/src/General.v index 7aefcf0..2d8a35c 100644 --- a/src/General.v +++ b/src/General.v @@ -792,4 +792,16 @@ Notation "'failM' x" := (uniqM (fun _ => Error x)) (at level 100). + + +Record FreshMonad {T:Type} := +{ FMT : Type -> Type +; FMT_Monad :> Monad FMT +; FMT_fresh : forall tl:list T, FMT { t:T & @In _ t tl -> False } +}. +Implicit Arguments FreshMonad [ ]. +Coercion FMT : FreshMonad >-> Funclass. + + + Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error". diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 40268e2..ece5801 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -16,51 +16,243 @@ Require Import HaskProof. Section HaskProofToStrong. - Context {VV:Type} {eqdec_vv:EqDecidable VV}. + Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}. - Definition Exprs Γ Δ ξ τ := - ITree _ (fun τ => Expr Γ Δ ξ τ) τ. + Definition fresh := FMT_fresh freshM. + Definition FreshM := FMT freshM. + Definition FreshMon := FMT_Monad freshM. + Existing Instance FreshMon. + + Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★. + + Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type := + match j with + mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars -> + FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ) + end. Definition judg2exprType (j:Judg) : Type := match j with - (Γ > Δ > Σ |- τ) => forall (ξ:VV -> LeveledHaskType Γ ★ ) vars, Σ=mapOptionTree ξ vars -> Exprs Γ Δ ξ τ + (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> + FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ) end. - Definition judges2exprType (j:Tree ??Judg) : Type := - ITree _ judg2exprType j. + Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ. + intros. + inversion X; auto. + Defined. - Definition urule2expr Γ Δ : forall h j (r:@URule Γ Δ h j), - judges2exprType (mapOptionTree UJudg2judg h) -> judges2exprType (mapOptionTree UJudg2judg j). + Definition ileaf `(it:ITree X F [t]) : F t. + inversion it. + apply X0. + Defined. - intros h j r. + Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) l1 l2 q, + update_ξ ξ (app l1 l2) q = update_ξ (update_ξ ξ l2) l1 q. + intros. + induction l1. + reflexivity. + simpl. + destruct a; simpl. + rewrite IHl1. + reflexivity. + Qed. + + Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t). + intros. + induction t. + destruct a; auto. + simpl; rewrite H; auto. + simpl; rewrite IHt1; rewrite IHt2; auto. + Qed. + + Lemma quark {T} (l1:list T) l2 vf : + (In vf (app l1 l2)) <-> + (In vf l1) \/ (In vf l2). + induction l1. + simpl; auto. + split; intro. + right; auto. + inversion H. + inversion H0. + auto. + split. + + destruct IHl1. + simpl in *. + intro. + destruct H1. + left; left; auto. + set (H H1) as q. + destruct q. + left; right; auto. + right; auto. + simpl. + + destruct IHl1. + simpl in *. + intro. + destruct H1. + destruct H1. + left; auto. + right; apply H0; auto. + right; apply H0; auto. + Qed. + + Lemma splitter {T} (l1:list T) l2 vf : + (In vf (app l1 l2) → False) + -> (In vf l1 → False) /\ (In vf l2 → False). + intros. + split; intros; apply H; rewrite quark. + auto. + auto. + Qed. + + Lemma helper + : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z), + (In vf (leaves tl) -> False) -> + mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl = + mapOptionTree ξ tl. + intros. + induction tl; + try destruct a; + simpl in *. + set (eqd_dec vf t) as x in *. + destruct x. + subst. + assert False. + apply H. + left; auto. + inversion H0. + auto. + auto. + apply splitter in H. + destruct H. + rewrite (IHtl1 H). + rewrite (IHtl2 H0). + reflexivity. + Qed. + + Lemma fresh_lemma' Γ + : forall types vars Σ ξ, Σ = mapOptionTree ξ vars -> + FreshM { varstypes : _ + | mapOptionTree (update_ξ(Γ:=Γ) ξ (leaves varstypes)) vars = Σ + /\ mapOptionTree (update_ξ ξ (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = types }. + induction types. + intros; destruct a. + refine (bind vf = fresh (leaves vars) ; return _). + apply FreshMon. + destruct vf as [ vf vf_pf ]. + exists [(vf,l)]. + split; auto. + simpl. + set (helper VV _ vars vf ξ l vf_pf) as q. + rewrite q. + symmetry; auto. + simpl. + destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto. + refine (return _). + exists []; auto. + intros vars Σ ξ pf; refine (bind x2 = IHtypes2 vars Σ ξ pf; _). + apply FreshMon. + destruct x2 as [vt2 [pf21 pf22]]. + refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,types2) (update_ξ ξ (leaves vt2)) _; return _). + apply FreshMon. + simpl. + rewrite pf21. + rewrite pf22. + reflexivity. + clear IHtypes1 IHtypes2. + destruct x1 as [vt1 [pf11 pf12]]. + exists (vt1,,vt2); split; auto. + + set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q. + set (mapOptionTree_extensional _ _ q) as q'. + rewrite q'. + clear q' q. + inversion pf11. + reflexivity. + + simpl. + set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q. + set (mapOptionTree_extensional _ _ q) as q'. + rewrite q'. + rewrite q'. + clear q' q. + rewrite <- mapOptionTree_compose. + rewrite <- mapOptionTree_compose. + rewrite <- mapOptionTree_compose in *. + rewrite pf12. + inversion pf11. + rewrite <- mapOptionTree_compose. + reflexivity. + Defined. - refine (match r as R in URule H C - return judges2exprType (mapOptionTree UJudg2judg H) -> judges2exprType (mapOptionTree UJudg2judg C) 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 ); intros. + Lemma fresh_lemma Γ ξ vars Σ Σ' + : Σ = mapOptionTree ξ vars -> + FreshM { vars' : _ + | mapOptionTree (update_ξ(Γ:=Γ) ξ ((vars',Σ')::nil)) vars = Σ + /\ mapOptionTree (update_ξ ξ ((vars',Σ')::nil)) [vars'] = [Σ'] }. + intros. + set (fresh_lemma' Γ [Σ'] vars Σ ξ H) as q. + refine (q >>>= fun q' => return _). + apply FreshMon. + clear q. + destruct q' as [varstypes [pf1 pf2]]. + destruct varstypes; try destruct o; try destruct p; simpl in *. + destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]. + inversion pf2; subst. + exists v. + destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]. + split; auto. + inversion pf2. + inversion pf2. + Defined. + + Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★), + FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }. + intros. + set (fresh_lemma' Γ Σ [] [] ξ0 (refl_equal _)) as q. + refine (q >>>= fun q' => return _). + apply FreshMon. + clear q. + destruct q' as [varstypes [pf1 pf2]]. + exists (mapOptionTree (@fst _ _) varstypes). + exists (update_ξ ξ0 (leaves varstypes)). + symmetry; auto. + Defined. + + Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★), + ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j. + + refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} : + ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j := + match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with + | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r) + | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r) + | 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); clear urule2expr; intros. destruct case_RCanL. apply ILeaf; simpl; intros. inversion X. simpl in X0. - apply (X0 ξ ([],,vars)). + apply (X0 ([],,vars)). simpl; rewrite <- H; auto. destruct case_RCanR. apply ILeaf; simpl; intros. inversion X. simpl in X0. - apply (X0 ξ (vars,,[])). + apply (X0 (vars,,[])). simpl; rewrite <- H; auto. destruct case_RuCanL. @@ -68,14 +260,14 @@ Section HaskProofToStrong. destruct vars; try destruct o; inversion H. inversion X. simpl in X0. - apply (X0 ξ vars2); auto. + apply (X0 vars2); auto. destruct case_RuCanR. apply ILeaf; simpl; intros. destruct vars; try destruct o; inversion H. inversion X. simpl in X0. - apply (X0 ξ vars1); auto. + apply (X0 vars1); auto. destruct case_RAssoc. apply ILeaf; simpl; intros. @@ -83,7 +275,7 @@ Section HaskProofToStrong. simpl in X0. destruct vars; try destruct o; inversion H. destruct vars1; try destruct o; inversion H. - apply (X0 ξ (vars1_1,,(vars1_2,,vars2))). + apply (X0 (vars1_1,,(vars1_2,,vars2))). subst; auto. destruct case_RCossa. @@ -92,242 +284,469 @@ Section HaskProofToStrong. simpl in X0. destruct vars; try destruct o; inversion H. destruct vars2; try destruct o; inversion H. - apply (X0 ξ ((vars1,,vars2_1),,vars2_2)). + apply (X0 ((vars1,,vars2_1),,vars2_2)). subst; auto. destruct case_RLeft. - (* this will require recursion *) - admit. + destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ]. + destruct o; [ idtac | apply INone ]. + destruct u; simpl in *. + apply ILeaf; simpl; intros. + destruct vars; try destruct o; inversion H. + set (fun q => ileaf (e ξ q)) as r'. + simpl in r'. + apply r' with (vars:=vars2). + clear r' e. + clear r0. + induction h0. + destruct a. + destruct u. + simpl in X. + apply ileaf in X. + apply ILeaf. + simpl. + simpl in X. + intros. + apply X with (vars:=vars1,,vars). + simpl. + rewrite H0. + rewrite H1. + reflexivity. + apply INone. + apply IBranch. + apply IHh0_1. inversion X; auto. + apply IHh0_2. inversion X; auto. + auto. destruct case_RRight. - (* this will require recursion *) - admit. + destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ]. + destruct o; [ idtac | apply INone ]. + destruct u; simpl in *. + apply ILeaf; simpl; intros. + destruct vars; try destruct o; inversion H. + set (fun q => ileaf (e ξ q)) as r'. + simpl in r'. + apply r' with (vars:=vars1). + clear r' e. + clear r0. + induction h0. + destruct a. + destruct u. + simpl in X. + apply ileaf in X. + apply ILeaf. + simpl. + simpl in X. + intros. + apply X with (vars:=vars,,vars2). + simpl. + rewrite H0. + rewrite H2. + reflexivity. + apply INone. + apply IBranch. + apply IHh0_1. inversion X; auto. + apply IHh0_2. inversion X; auto. + auto. destruct case_RExch. apply ILeaf; simpl; intros. inversion X. simpl in X0. destruct vars; try destruct o; inversion H. - apply (X0 ξ (vars2,,vars1)). + apply (X0 (vars2,,vars1)). inversion H; subst; auto. destruct case_RWeak. apply ILeaf; simpl; intros. inversion X. simpl in X0. - apply (X0 ξ []). + apply (X0 []). auto. destruct case_RCont. apply ILeaf; simpl; intros. inversion X. simpl in X0. - apply (X0 ξ (vars,,vars)). + apply (X0 (vars,,vars)). simpl. rewrite <- H. auto. Defined. - Definition rule2expr : forall h j (r:Rule h j), judges2exprType h -> judges2exprType j. + Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ : + ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c. + intro it. + induction c. + destruct a. + destruct u; simpl in *. + apply ileaf in it. + apply ILeaf. + simpl in *. + intros; apply it with (vars:=vars); auto. + apply INone. + apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto. + Defined. + + Definition letrec_helper Γ Δ l varstypes ξ' : + ITree (LeveledHaskType Γ ★) + (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t) + (mapOptionTree (ξ' ○ (@fst _ _)) varstypes) + -> ELetRecBindings Γ Δ ξ' l + (mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) ⟩) varstypes). + intros. + induction varstypes. + destruct a; simpl in *. + destruct p. + destruct l0 as [τ l']. + simpl. + apply ileaf in X. simpl in X. + assert (unlev (ξ' v) = τ). + admit. + rewrite <- H. + apply ELR_leaf. + rewrite H. + destruct (ξ' v). + rewrite <- H. + simpl. + assert (h0=l). admit. + rewrite H0 in X. + apply X. + + apply ELR_nil. + + simpl; apply ELR_branch. + apply IHvarstypes1. + simpl in X. + inversion X; auto. + apply IHvarstypes2. + simpl in X. + inversion X; auto. + + Defined. + + +(* + Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) tys : + forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars, + judg2exprType (pcb_judg pcb) -> FreshM + {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars & + Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ)) + (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev))}. + intros. + simpl in X. + destruct pcb. + simpl in *. + refine (bind ξvars = fresh_lemma' Γ pcb_freevars Σ [] ξ _ ; _). apply FreshMon. + destruct ξvars as [vars [ξ' + Defined. +*) + + Lemma itree_mapOptionTree : forall T T' F (f:T->T') t, + ITree _ F (mapOptionTree f t) -> + ITree _ (F ○ f) t. + intros. + induction t; try destruct a; simpl in *. + apply ILeaf. + inversion X; auto. + apply INone. + apply IBranch. + apply IHt1; inversion X; auto. + apply IHt2; inversion X; auto. + Defined. + + Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j. intros h j r. - refine (match r as R in Rule H C return judges2exprType H -> judges2exprType C with - | RURule a b c d e => let case_RURule := tt in _ - | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ - | RLit Γ Δ l _ => let case_RLit := tt in _ - | RVar Γ Δ σ p => let case_RVar := tt in _ - | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ - | RLam Γ Δ Σ tx te x => let case_RLam := tt in _ - | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _ - | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _ - | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _ - | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _ - | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ 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); intros. + refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with + | RURule a b c d e => let case_RURule := tt in _ + | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ + | RLit Γ Δ l _ => let case_RLit := tt in _ + | RVar Γ Δ σ p => let case_RVar := tt in _ + | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ + | RLam Γ Δ Σ tx te x => let case_RLam := tt in _ + | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _ + | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _ + | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _ + | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _ + | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ + | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ + | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ + | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _ + | REmptyGroup _ _ => let case_REmptyGroup := tt in _ + | RBrak Σ a b c n m => let case_RBrak := tt in _ + | REsc Σ a b c n m => let case_REsc := tt in _ + | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ + | RLetRec Γ Δ lri x y => let case_RLetRec := tt in _ + end); intro X_; try apply ileaf in X_; simpl in X_. destruct case_RURule. - eapply urule2expr. - apply e. - apply X. + destruct d; try destruct o. + apply ILeaf; destruct u; simpl; intros. + set (@urule2expr a b _ _ e ξ) as q. + set (fun z => ileaf (q z)) as q'. + simpl in q'. + apply q' with (vars:=vars). + clear q' q. + apply bridge. + apply X_. + auto. + apply no_urules_with_empty_conclusion in e; inversion e; auto. + apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto. destruct case_RBrak. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon. apply EBrak. - inversion X. - set (X0 ξ vars H) as X'. - inversion X'. - apply X1. + apply (ileaf X). destruct case_REsc. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon. apply EEsc. - inversion X. - set (X0 ξ vars H) as X'. - inversion X'. - apply X1. + apply (ileaf X). destruct case_RNote. - apply ILeaf; simpl; intros; apply ILeaf. - inversion X. - apply ENote. - apply n. - simpl in X0. - set (X0 ξ vars H) as x1. - inversion x1. - apply X1. + apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon. + apply ENote; auto. + apply (ileaf X). destruct case_RLit. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (return ILeaf _ _). apply ELit. destruct case_RVar. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (return ILeaf _ _). destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2. apply EVar. inversion H. destruct case_RGlobal. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (return ILeaf _ _). apply EGlobal. apply wev. destruct case_RLam. - apply ILeaf; simpl; intros; apply ILeaf. - (* need a fresh variable here *) - admit. + apply ILeaf. + simpl in *; intros. + refine (fresh_lemma _ ξ vars _ (tx@@x) H >>>= (fun pf => _)). + apply FreshMon. + destruct pf as [ vnew [ pf1 pf2 ]]. + set (update_ξ ξ ((⟨vnew, tx @@ x ⟩) :: nil)) as ξ' in *. + refine (X_ ξ' (vars,,[vnew]) _ >>>= _). + apply FreshMon. + simpl. + rewrite pf1. + rewrite <- pf2. + simpl. + reflexivity. + intro hyp. + refine (return _). + apply ILeaf. + apply ELam with (ev:=vnew). + apply ileaf in hyp. + simpl in hyp. + unfold ξ' in hyp. + apply hyp. destruct case_RCast. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon. eapply ECast. apply x. - inversion X. - simpl in X0. - set (X0 ξ vars H) as q. - inversion q. - apply X1. + apply ileaf in X. simpl in X. + apply X. destruct case_RBindingGroup. apply ILeaf; simpl; intros. - inversion X. - inversion X0. - inversion X1. + inversion X_. + apply ileaf in X. + apply ileaf in X0. + simpl in *. destruct vars; inversion H. - destruct o; inversion H5. - set (X2 _ _ H5) as q1. - set (X3 _ _ H6) as q2. + destruct o; inversion H3. + refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _). + apply FreshMon. + apply FreshMon. apply IBranch; auto. destruct case_RApp. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf. + inversion X_. inversion X. inversion X0. - inversion X1. - destruct vars; try destruct o; inversion H. - set (X2 _ _ H5) as q1. - set (X3 _ _ H6) as q2. - eapply EApp. - inversion q1. - apply X4. - inversion q2. - apply X4. + simpl in *. + intros. + destruct vars. try destruct o; inversion H. + simpl in H. + inversion H. + set (X1 ξ vars1 H5) as q1. + set (X2 ξ vars2 H6) as q2. + refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _). + apply FreshMon. + apply FreshMon. + apply ILeaf. + apply ileaf in q1'. + apply ileaf in q2'. + simpl in *. + apply (EApp _ _ _ _ _ _ q1' q2'). destruct case_RLet. - apply ILeaf; simpl; intros; apply ILeaf. - (* FIXME: need a var here, and other work *) - admit. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)). + apply FreshMon. + destruct pf as [ vnew [ pf1 pf2 ]]. + set (update_ξ ξ ((⟨vnew, σ₂ @@ p ⟩) :: nil)) as ξ' in *. + inversion X_. + apply ileaf in X. + apply ileaf in X0. + simpl in *. + refine (X0 ξ vars2 _ >>>= fun X0' => _). + apply FreshMon. + auto. + refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _). + apply FreshMon. + rewrite H1. + simpl. + rewrite pf2. + rewrite pf1. + rewrite H1. + reflexivity. + refine (return _). + apply ILeaf. + apply ileaf in X0'. + apply ileaf in X1'. + simpl in *. + apply ELet with (ev:=vnew)(tv:=σ₂). + apply X0'. + apply X1'. destruct case_REmptyGroup. apply ILeaf; simpl; intros. + refine (return _). apply INone. destruct case_RAppT. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon. apply ETyApp. - inversion X. - set (X0 _ _ H) as q. - inversion q. - apply X1. + apply (ileaf X). destruct case_RAbsT. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon. + rewrite mapOptionTree_compose. + rewrite <- H. + reflexivity. + apply ileaf in X. simpl in *. apply ETyLam. - inversion X. - simpl in *. - set (X0 (weakLT ○ ξ) vars) as q. - rewrite mapOptionTree_compose in q. - rewrite <- H in q. - set (q (refl_equal _)) as q'. - inversion q'. - apply X1. + apply X. destruct case_RAppCo. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon. + auto. eapply ECoApp. apply γ. - inversion X. - set (X0 _ _ H) as q. - inversion q. - apply X1. + apply (ileaf X). destruct case_RAbsCo. - apply ILeaf; simpl; intros; apply ILeaf. + apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon. + auto. eapply ECoLam. - inversion X. - set (X0 _ _ H) as q. - inversion q; auto. + apply (ileaf X). destruct case_RLetRec. - admit. + apply ILeaf; simpl; intros. + refine (bind ξvars = fresh_lemma' _ y _ _ _ H; _). apply FreshMon. + destruct ξvars as [ varstypes [ pf1 pf2 ]]. + refine (X_ ((update_ξ ξ (leaves varstypes))) + (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon. + simpl. + rewrite pf2. + rewrite pf1. + auto. + apply ILeaf. + destruct x as [τ l]. + inversion X; subst; clear X. + + (* getting rid of this will require strengthening RLetRec *) + assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) varstypes) = varstypes) as HHH. + admit. + + apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes)); + rewrite mapleaves; rewrite <- map_compose; simpl; + [ idtac + | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ]. + + clear X0. + rewrite <- mapOptionTree_compose in X1. + set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) as ξ' in *. + rewrite <- mapleaves. + rewrite HHH. + + apply (letrec_helper _ _ _ _ _ X1). destruct case_RCase. - admit. + apply ILeaf. +simpl. +intros. +apply (Prelude_error "FIXME"). - Defined. + +(* + apply ILeaf; simpl; intros. + inversion X_. + clear X_. + subst. + apply ileaf in X0. + simpl in X0. + set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *. + refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _). + apply FreshMon. + destruct vars; try destruct o; inversion H; clear H. + rename vars1 into varsalts. + rename vars2 into varsΣ. + + refine (X0 ξ varsΣ _ >>>= fun X => return ILeaf _ _); auto. apply FreshMon. + clear X0. + eapply (ECase _ _ _ _ _ _ _ (ileaf X1)). + clear X1. + + destruct ξvars as [varstypes [pf1 pf2]]. + + apply itree_mapOptionTree in X. + refine (itree_to_tree (itmap _ X)). + apply case_helper. +*) + 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) + | cnd_weak => let case_nil := tt in INone _ _ + | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd') + | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2) end)); clear closed2expr'; intros; subst. - - destruct case_nil. - apply INone. - - destruct case_rule. - eapply rule2expr. - apply r. - apply rest. - - destruct case_branch. - apply IBranch. - apply rest1. - apply rest2. Defined. - Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ ★ & Expr Γ Δ ξ τ }. + Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★) + {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] -> + FreshM (???{ ξ : _ & 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. + apply ileaf in cnd. + simpl in *. + clear pf. + refine (bind ξvars = manyFresh _ Σ ξ0; _). + apply FreshMon. + destruct ξvars as [vars ξpf]. + destruct ξpf as [ξ pf]. + refine (cnd ξ vars _ >>>= fun it => _). + apply FreshMon. + auto. + refine (return OK _). + exists ξ. + apply (ileaf it). Defined. End HaskProofToStrong.