From 57e387249da84dac0f1c5a9411e3900831ce2d81 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 27 May 2011 14:30:24 -0700 Subject: [PATCH] HaskProof: make the succedent level part of the judgment --- src/ExtractionMain.v | 28 +++---- src/HaskFlattener.v | 191 ++++++++++++++++++----------------------------- src/HaskProof.v | 59 ++++++++------- src/HaskProofToLatex.v | 16 ++-- src/HaskProofToStrong.v | 71 ++++++++++-------- src/HaskSkolemizer.v | 50 +++++-------- src/HaskStrongToProof.v | 16 ++-- src/HaskStrongTypes.v | 2 + 8 files changed, 194 insertions(+), 239 deletions(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 6364a5a..77326e0 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -234,8 +234,8 @@ Section core2proof. Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} : ND Rule - [ Γ > Δ > Σ |- [a ---> s @@ lev ] ] - [ Γ > Δ > [a @@ lev],,Σ |- [ s @@ lev ] ]. + [ Γ > Δ > Σ |- [a ---> s ]@lev ] + [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. @@ -246,8 +246,8 @@ Section core2proof. Defined. Definition fToC1 {Γ}{Δ}{a}{s}{lev} : - ND Rule [] [ Γ > Δ > [ ] |- [a ---> s @@ lev ] ] -> - ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s @@ lev ] ]. + ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] -> + ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ]. intro pf. eapply nd_comp. apply pf. @@ -256,8 +256,8 @@ Section core2proof. Defined. Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} : - ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) @@ lev ] ] -> - ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ]. + ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] -> + ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ]. intro pf. eapply nd_comp. eapply pf. @@ -338,7 +338,7 @@ Section core2proof. Defined. Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y - : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ]. + : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ]. apply nd_rule. refine (@RGlobal Γ Δ l {| glob_wv := coreVarToWeakExprVarOrError cv @@ -357,7 +357,7 @@ Section core2proof. Defined. Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z - : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ]. + : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ]. apply nd_rule. refine (@RGlobal Γ Δ l {| glob_wv := coreVarToWeakExprVarOrError cv @@ -377,7 +377,7 @@ Section core2proof. Defined. Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q - : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ]. + : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l]. apply nd_rule. refine (@RGlobal Γ Δ l {| glob_wv := coreVarToWeakExprVarOrError cv @@ -418,10 +418,10 @@ Section core2proof. Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten. Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id. - Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := - addErrorMessage ("input CoreSyn: " +++ toString ce) - (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( - coreExprToWeakExpr ce >>= fun we => + Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := + addErrorMessage ("input CoreSyn: " +++ toString cex) + (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) ( + coreExprToWeakExpr cex >>= fun we => addErrorMessage ("WeakExpr: " +++ toString we) ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we))) ((weakTypeOfWeakExpr we) >>= fun t => @@ -434,7 +434,7 @@ Section core2proof. (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten' hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e) in (* insert HaskProof-to-HaskProof manipulations here *) - OK ((@proof2expr nat _ FreshNat _ _ _ _ (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' diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 08485a1..9b3a163 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -308,68 +308,47 @@ Section HaskFlattener. Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v, flatten_type (g v) = g v. - (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different - * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it - * picks nil *) - Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end. - Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) := - match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end. - Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ := - match tt with - | T_Leaf None => nil - | T_Leaf (Some (_ @@ lev)) => lev - | T_Branch b1 b2 => - match getjlev b1 with - | nil => getjlev b2 - | lev => lev - end - end. - (* "n" is the maximum depth remaining AFTER flattening *) Definition flatten_judgment (j:Judg) := match j as J return Judg with - Γ > Δ > ant |- suc => - match getjlev suc with - | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant - |- mapOptionTree flatten_leveled_type suc - - | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant) - |- [ga_mk (v2t ec) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant)) - (mapOptionTree (flatten_type ○ unlev) suc ) - @@ nil] (* we know the level of all of suc *) - end + | Γ > Δ > ant |- suc @ nil => Γ > Δ > mapOptionTree flatten_leveled_type ant + |- mapOptionTree flatten_type suc @ nil + | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant) + |- [ga_mk (v2t ec) + (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant)) + (mapOptionTree flatten_type suc ) + ] @ nil end. Class garrow := - { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ] - ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ] - ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ] - ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ] - ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ] - ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ] - ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ] - ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ] - ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ] - ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ] - ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ] - ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ] - ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ] - ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ] - ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ] + { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a ]@l ] + ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a ]@l ] + ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a ]@l ] + ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) ]@l ] + ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) ]@l ] + ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ] + ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ] + ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ] + ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] ]@l ] + ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) ]@l ] + ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ] + ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ] + ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ] + ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ] + ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ] ; ga_apply : ∀ Γ Δ ec l a a' b c, - ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ] + ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ] ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ] - [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ] + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ] + [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ] }. Context `(gar:garrow). Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20). Definition boost : forall Γ Δ ant x y {lev}, - ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] -> - ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ]. + ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] -> + ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. @@ -385,8 +364,8 @@ Section HaskFlattener. Definition precompose Γ Δ ec : forall a x y z lev, ND Rule - [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ] - [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. + [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ] + [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. @@ -398,8 +377,8 @@ Section HaskFlattener. Definition precompose' Γ Δ ec : forall a b x y z lev, ND Rule - [ Γ > Δ > a,,b |- [@ga_mk _ ec y z @@ lev] ] - [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z @@ lev] ]. + [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ] + [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ]. @@ -408,8 +387,8 @@ Section HaskFlattener. Definition postcompose_ Γ Δ ec : forall a x y z lev, ND Rule - [ Γ > Δ > a |- [@ga_mk _ ec x y @@ lev] ] - [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. + [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ] + [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. @@ -419,8 +398,8 @@ Section HaskFlattener. Defined. Definition postcompose Γ Δ ec : forall x y z lev, - ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y @@ lev] ] -> - ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. + ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] -> + ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. eapply nd_comp; [ idtac | eapply postcompose_ ]. @@ -428,8 +407,8 @@ Section HaskFlattener. Defined. Definition first_nd : ∀ Γ Δ ec lev a b c Σ, - ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] - [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. + ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] + [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. @@ -441,8 +420,8 @@ Section HaskFlattener. Defined. Definition firstify : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ]. intros. eapply nd_comp. apply X. @@ -451,8 +430,8 @@ Section HaskFlattener. Definition second_nd : ∀ Γ Δ ec lev a b c Σ, ND Rule - [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] - [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. + [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] + [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. @@ -464,8 +443,8 @@ Section HaskFlattener. Defined. Definition secondify : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ]. intros. eapply nd_comp. apply X. @@ -474,8 +453,8 @@ Section HaskFlattener. Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x, ND Rule - [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ] - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]. + [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ] + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. @@ -502,17 +481,17 @@ Section HaskFlattener. forall Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2), ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2)) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ]. + (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ]. intros Γ Δ ec lev. refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2): ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2)) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] := + (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] := match r as R in Arrange A B return ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B)) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]] + (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil] with | RId a => let case_RId := tt in ga_id _ _ _ _ _ | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _ @@ -556,11 +535,11 @@ Section HaskFlattener. [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1) |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) - (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]] + (mapOptionTree (flatten_type ) succ) ]@nil] [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2) |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2)) - (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]. + (mapOptionTree (flatten_type ) succ) ]@nil]. intros. refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))). apply nd_rule. @@ -586,16 +565,12 @@ Section HaskFlattener. Defined. Definition flatten_arrangement'' : - forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2), - ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ]) - (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]). + forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2), + ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l]) + (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]). intros. simpl. - set (getjlev succ) as succ_lev. - assert (succ_lev=getjlev succ). - reflexivity. - - destruct succ_lev. + destruct l. apply nd_rule. apply RArrange. induction r; simpl. @@ -618,9 +593,9 @@ Section HaskFlattener. Defined. Definition ga_join Γ Δ Σ₁ Σ₂ a b ec : - ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] -> - ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] -> - ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]]. + ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] -> + ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] -> + ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil]. intro pfa. intro pfb. apply secondify with (c:=a) in pfb. @@ -647,8 +622,8 @@ Section HaskFlattener. ND Rule [Γ > Δ > [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],, - mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]] - [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]. + mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil] + [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]. intros. unfold drop_lev. @@ -757,10 +732,10 @@ Section HaskFlattener. Definition arrange_esc : forall Γ Δ ec succ t, ND Rule - [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]] + [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil] [Γ > Δ > [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],, - mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]]. + mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]. intros. set (@arrange _ succ (levelMatch (ec::nil))) as q. set (@drop_lev Γ (ec::nil) succ) as q'. @@ -950,7 +925,7 @@ Section HaskFlattener. destruct case_SFlat. refine (match r as R in Rule H C with - | RArrange Γ Δ a b x d => let case_RArrange := tt in _ + | RArrange Γ Δ a b x l d => let case_RArrange := tt in _ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ | RVar Γ Δ σ lev => let case_RVar := tt in _ @@ -964,8 +939,8 @@ Section HaskFlattener. | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ - | RJoin Γ p lri m x q => let case_RJoin := tt in _ - | RVoid _ _ => let case_RVoid := tt in _ + | RJoin Γ p lri m x q l => let case_RJoin := tt in _ + | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ @@ -973,7 +948,7 @@ Section HaskFlattener. end); clear X h c. destruct case_RArrange. - apply (flatten_arrangement'' Γ Δ a b x d). + apply (flatten_arrangement'' Γ Δ a b x _ d). destruct case_RBrak. apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen"). @@ -1006,7 +981,6 @@ Section HaskFlattener. Transparent flatten_judgment. idtac. unfold flatten_judgment. - unfold getjlev. destruct lev. apply nd_rule. apply RVar. repeat drop_simplify. @@ -1063,21 +1037,18 @@ Section HaskFlattener. destruct case_RJoin. simpl. - destruct (getjlev x); destruct (getjlev q); - [ apply nd_rule; apply RJoin | idtac | idtac | idtac ]; + destruct l; + [ apply nd_rule; apply RJoin | idtac ]; apply (Prelude_error "RJoin at depth >0"). destruct case_RApp. simpl. - destruct lev as [|ec lev]. simpl. apply nd_rule. - unfold flatten_leveled_type at 4. - unfold flatten_leveled_type at 2. + destruct lev as [|ec lev]. + unfold flatten_type at 1. simpl. - replace (flatten_type (tx ---> te)) - with (flatten_type tx ---> flatten_type te). + apply nd_rule. apply RApp. - reflexivity. repeat drop_simplify. repeat take_simplify. @@ -1154,7 +1125,9 @@ Section HaskFlattener. destruct case_RVoid. simpl. apply nd_rule. + destruct l. apply RVoid. + apply (Prelude_error "RVoid at level >0"). destruct case_RAppT. simpl. destruct lev; simpl. @@ -1170,9 +1143,6 @@ Section HaskFlattener. destruct case_RAbsT. simpl. destruct lev; simpl. - unfold flatten_leveled_type at 4. - unfold flatten_leveled_type at 2. - simpl. rewrite flatten_commutes_with_HaskTAll. rewrite flatten_commutes_with_HaskTApp. eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ]. @@ -1201,8 +1171,6 @@ Section HaskFlattener. destruct case_RAppCo. simpl. destruct lev; simpl. - unfold flatten_leveled_type at 4. - unfold flatten_leveled_type at 2. unfold flatten_type. simpl. apply nd_rule. @@ -1221,27 +1189,15 @@ Section HaskFlattener. destruct case_RLetRec. rename t into lev. simpl. destruct lev; simpl. - replace (getjlev (y @@@ nil)) with (nil: (HaskLevel Γ)). - replace (mapOptionTree flatten_leveled_type (y @@@ nil)) - with ((mapOptionTree flatten_type y) @@@ nil). - unfold flatten_leveled_type at 2. - simpl. - unfold flatten_leveled_type at 3. - simpl. apply nd_rule. set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q. - simpl in q. + replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil). apply q. induction y; try destruct a; auto. simpl. rewrite IHy1. rewrite IHy2. reflexivity. - induction y; try destruct a; auto. - simpl. - rewrite <- IHy1. - rewrite <- IHy2. - reflexivity. apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)"). destruct case_RCase. @@ -1260,7 +1216,6 @@ Section HaskFlattener. rewrite mapOptionTree_compose. rewrite unlev_relev. rewrite <- mapOptionTree_compose. - unfold flatten_leveled_type at 4. simpl. rewrite krunk. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. diff --git a/src/HaskProof.v b/src/HaskProof.v index 2b6aa3c..d92dd6b 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -29,9 +29,10 @@ Inductive Judg := forall Γ:TypeEnv, forall Δ:CoercionEnv Γ, Tree ??(LeveledHaskType Γ ★) -> - Tree ??(LeveledHaskType Γ ★) -> + Tree ??(HaskType Γ ★) -> + HaskLevel Γ -> Judg. - Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). + Notation "Γ > Δ > a '|-' s '@' l" := (mkJudg Γ Δ a s l) (at level 52, Δ at level 50, a at level 52, s at level 50, l at level 50). (* information needed to define a case branch in a HaskProof *) Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} := @@ -39,7 +40,7 @@ Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{ava ; pcb_judg := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ) > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev) (vec2list (sac_types sac Γ avars)))) - |- [weakLT' (branchtype @@ lev)] + |- [weakT' branchtype ] @ weakL' lev }. Implicit Arguments ProofCaseBranch [ ]. @@ -63,58 +64,58 @@ Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type := (* Figure 3, production $\vdash_E$, all rules *) Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := -| RArrange : ∀ Γ Δ Σ₁ Σ₂ Σ, Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁ |- Σ ] [Γ > Δ > Σ₂ |- Σ ] +| RArrange : ∀ Γ Δ Σ₁ Σ₂ Σ l, Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁ |- Σ @l] [Γ > Δ > Σ₂ |- Σ @l] (* λ^α rules *) -| RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]] -| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l)]] +| RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t]@(v::l) ] [Γ > Δ > Σ |- [<[v|-t]> ] @l] +| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> ] @l] [Γ > Δ > Σ |- [t]@(v::l) ] (* Part of GHC, but not explicitly in System FC *) -| RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@l]] -| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@l]] +| RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ ] @l] [Γ > Δ > Σ |- [τ ] @l] +| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v ] @l] (* SystemFC rules *) -| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]] -| RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v @@l]] -| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]] +| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ ] @l] +| RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v ] @l] +| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te] @l] [Γ>Δ> Σ |- [tx--->te ] @l] | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, - HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] + HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l] -| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] +| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l, Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ @l ] (* order is important here; we want to be able to skolemize without introducing new RExch'es *) -| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] +| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l] -| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁@@l]],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ @@l]] -| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂@@l] ],,[Γ>Δ> Σ₂ |- [σ₁@@l]]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ @@l]] +| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l] +| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l] -| RVoid : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] +| RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ] -| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]] +| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l] | RAbsT : ∀ Γ Δ Σ κ σ l, - Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]] - [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]] + Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)] + [Γ>Δ > Σ |- [HaskTAll κ σ ]@l] | RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l, - Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]] + Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ]@l] [Γ>Δ> Σ |- [σ ]@l] | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l, - Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] - [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] + Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ ]@l] + [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ ]@l] -| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁])@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ] +| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev] | RCase : forall Γ Δ lev tc Σ avars tbranches (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }), Rule ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),, - [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ]) - [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches @@ lev ] ] + [Γ > Δ > Σ |- [ caseType tc avars ] @lev]) + [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev] . (* A rule is considered "flat" if it is neither RBrak nor REsc *) (* TODO: change this to (if RBrak/REsc -> False) *) Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := -| Flat_RArrange : ∀ Γ Δ h c r a , Rule_Flat (RArrange Γ Δ h c r a) +| Flat_RArrange : ∀ Γ Δ h c r a l , Rule_Flat (RArrange Γ Δ h c r a l) | Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n) | Flat_RLit : ∀ Γ Δ Σ τ , Rule_Flat (RLit Γ Δ Σ τ ) | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l) @@ -126,8 +127,8 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 ) | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l) | Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l) -| Flat_RJoin : ∀ q a b c d e , Rule_Flat (RJoin q a b c d e) -| Flat_RVoid : ∀ q a , Rule_Flat (RVoid q a) +| Flat_RJoin : ∀ q a b c d e l, Rule_Flat (RJoin q a b c d e l) +| Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l) | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x) | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev). diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 61a0bdb..4319a1c 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -146,9 +146,9 @@ Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS Definition judgmentToRawLatexMath (j:Judg) : LatexMath := match match j return VarNameStoreM LatexMath with - | mkJudg Γ Δ Σ₁ Σ₂ => + | mkJudg Γ Δ Σ₁ Σ₂ l => bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁) - ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂) + ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂) ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂' end with varNameStoreM f => fst (f (varNameStore 0 0 0)) @@ -176,7 +176,7 @@ Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string := Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := match r with - | RArrange _ _ _ _ _ r => nd_uruleToRawLatexMath r + | RArrange _ _ _ _ _ _ r => nd_uruleToRawLatexMath r | RNote _ _ _ _ _ _ => "Note" | RLit _ _ _ _ => "Lit" | RVar _ _ _ _ => "Var" @@ -190,12 +190,12 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RApp _ _ _ _ _ _ _ => "App" | RLet _ _ _ _ _ _ _ => "Let" | RWhere _ _ _ _ _ _ _ _ => "Where" - | RJoin _ _ _ _ _ _ => "RJoin" + | RJoin _ _ _ _ _ _ _ => "RJoin" | RLetRec _ _ _ _ _ _ => "LetRec" | RCase _ _ _ _ _ _ _ _ => "Case" | RBrak _ _ _ _ _ _ => "Brak" | REsc _ _ _ _ _ _ => "Esc" - | RVoid _ _ => "RVoid" + | RVoid _ _ _ => "RVoid" end. Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool := @@ -217,9 +217,9 @@ Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool := end. Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool := match r with - | RArrange _ _ _ _ _ r => nd_hideURule r - | RVoid _ _ => true - | RJoin _ _ _ _ _ _ => true + | RArrange _ _ _ _ _ _ r => nd_hideURule r + | RVoid _ _ _ => true + | RJoin _ _ _ _ _ _ _ => true | _ => false end. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 69e8bb1..78c2e41 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -27,8 +27,8 @@ Section HaskProofToStrong. Definition judg2exprType (j:Judg) : Type := match j with - (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> - FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ) + (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> + FreshM (ITree _ (fun t => Expr Γ Δ ξ (t @@ l)) τ) end. Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ. @@ -222,23 +222,23 @@ Section HaskProofToStrong. inversion pf2. Defined. - Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type := - forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ). + Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type := + forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ (t@@l)) τ). - Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★), - ujudg2exprType Γ ξ Δ h t -> - ujudg2exprType Γ ξ Δ j t + Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★), + ujudg2exprType Γ ξ Δ h t l -> + ujudg2exprType Γ ξ Δ j t l . intros Γ Δ. - refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} : - ujudg2exprType Γ ξ Δ h t -> - ujudg2exprType Γ ξ Δ j t := + refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} : + ujudg2exprType Γ ξ Δ h t l -> + ujudg2exprType Γ ξ Δ j t l := match r as R in Arrange H C return - ujudg2exprType Γ ξ Δ H t -> - ujudg2exprType Γ ξ Δ C t + ujudg2exprType Γ ξ Δ H t l -> + ujudg2exprType Γ ξ Δ C t l 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) + | 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) | RId a => let case_RId := tt in _ | RCanL a => let case_RCanL := tt in _ | RCanR a => let case_RCanR := tt in _ @@ -249,7 +249,7 @@ Section HaskProofToStrong. | RExch a b => let case_RExch := tt in _ | RWeak a => let case_RWeak := tt in _ | RCont a => let case_RCont := tt in _ - | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g) + | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g) end); clear urule2expr; intros. destruct case_RId. @@ -353,9 +353,9 @@ Section HaskProofToStrong. Defined. Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' : - ITree (LeveledHaskType Γ ★) - (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t) - (mapOptionTree (ξ' ○ (@fst _ _)) varstypes) + ITree (HaskType Γ ★) + (fun t : HaskType Γ ★ => Expr Γ Δ ξ' (t @@ l)) + (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes) -> ELetRecBindings Γ Δ ξ' l varstypes. intros. induction varstypes. @@ -371,6 +371,8 @@ Section HaskProofToStrong. simpl. destruct (eqd_dec h0 l). rewrite <- e0. + simpl in X. + subst. apply X. apply (Prelude_error "level mismatch; should never happen"). apply (Prelude_error "letrec type mismatch; should never happen"). @@ -511,7 +513,7 @@ Section HaskProofToStrong. intros h j r. refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with - | RArrange a b c d e r => let case_RURule := tt in _ + | RArrange a b c d e l r => 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 _ @@ -525,8 +527,8 @@ Section HaskProofToStrong. | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _ - | RJoin Γ p lri m x q => let case_RJoin := tt in _ - | RVoid _ _ => let case_RVoid := tt in _ + | RJoin Γ p lri m x q l => let case_RJoin := tt in _ + | RVoid _ _ l => let case_RVoid := 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 _ @@ -535,12 +537,10 @@ Section HaskProofToStrong. destruct case_RURule. apply ILeaf. simpl. intros. - set (@urule2expr a b _ _ e r0 ξ) as q. - set (fun z => q z) as q'. - simpl in q'. - apply q' with (vars:=vars). - clear q' q. + set (@urule2expr a b _ _ e l r0 ξ) as q. unfold ujudg2exprType. + unfold ujudg2exprType in q. + apply q with (vars:=vars). intros. apply X_ with (vars:=vars0). auto. @@ -763,10 +763,18 @@ Section HaskProofToStrong. apply (@ELetRec _ _ _ _ _ _ _ varstypes). auto. apply (@letrec_helper Γ Δ t varstypes). - rewrite <- pf2 in X0. rewrite mapOptionTree_compose. - apply X0. + rewrite mapOptionTree_compose. + rewrite pf2. + replace ((mapOptionTree unlev (y @@@ t))) with y. + apply X0. + clear pf1 X0 X1 pfdist pf2 vars varstypes. + induction y; try destruct a; auto. + rewrite IHy1 at 1. + rewrite IHy2 at 1. + reflexivity. apply ileaf in X1. + simpl in X1. apply X1. destruct case_RCase. @@ -845,7 +853,7 @@ Section HaskProofToStrong. Defined. Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★) - {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] -> + {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [unlev τ] @ getlev τ] -> FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}). intro pf. set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd. @@ -862,7 +870,10 @@ Section HaskProofToStrong. auto. refine (return OK _). exists ξ. - apply (ileaf it). + apply ileaf in it. + simpl in it. + destruct τ. + apply it. apply INone. Defined. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index b037bb0..bb4dc92 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -82,19 +82,7 @@ Section HaskSkolemizer. end. (* rules of skolemized proofs *) - Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end. - Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) := - match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end. - Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ := - match tt with - | T_Leaf None => nil - | T_Leaf (Some (_ @@ lev)) => lev - | T_Branch b1 b2 => - match getjlev b1 with - | nil => getjlev b2 - | lev => lev - end - end. + Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end. Fixpoint take_trustme {Γ} (n:nat) @@ -184,13 +172,13 @@ Section HaskSkolemizer. | SFlat : forall h c, Rule h c -> SRule h c | SBrak : forall Γ Δ t ec Σ l, SRule - [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] - [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]] + [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t ] @ (ec::l)] + [Γ > Δ > Σ |- [<[ec |- t]> ] @l] | SEsc : forall Γ Δ t ec Σ l, SRule - [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]] - [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] + [Γ > Δ > Σ |- [<[ec |- t]> ] @l] + [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t ] @ (ec::l)] . Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) := @@ -201,11 +189,9 @@ Section HaskSkolemizer. Definition skolemize_judgment (j:Judg) : Judg := match j with - Γ > Δ > Σ₁ |- Σ₂ => - match getjlev Σ₂ with - | nil => j - | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂ - end + | Γ > Δ > Σ₁ |- Σ₂ @ nil => j + | Γ > Δ > Σ₁ |- Σ₂ @ lev => + Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂ @@@ lev) |- mapOptionTree drop_arg_types_as_tree Σ₂ @ lev end. Definition check_hof : forall {Γ}(t:HaskType Γ ★), @@ -232,7 +218,7 @@ Section HaskSkolemizer. intros. refine (match X as R in Rule H C with - | RArrange Γ Δ a b x d => let case_RArrange := tt in _ + | RArrange Γ Δ a b x l d => let case_RArrange := tt in _ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ | RVar Γ Δ σ lev => let case_RVar := tt in _ @@ -246,8 +232,8 @@ Section HaskSkolemizer. | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ - | RJoin Γ p lri m x q => let case_RJoin := tt in _ - | RVoid _ _ => let case_RVoid := tt in _ + | RJoin Γ p lri m x q l => let case_RJoin := tt in _ + | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ @@ -256,7 +242,7 @@ Section HaskSkolemizer. destruct case_RArrange. simpl. - destruct (getjlev x). + destruct l. apply nd_rule. apply SFlat. apply RArrange. @@ -363,13 +349,11 @@ Section HaskSkolemizer. destruct case_RJoin. simpl. - destruct (getjlev x). - destruct (getjlev q). + destruct l. apply nd_rule. apply SFlat. apply RJoin. apply (Prelude_error "found RJoin at level >0"). - apply (Prelude_error "found RJoin at level >0"). destruct case_RApp. simpl. @@ -446,6 +430,11 @@ Section HaskSkolemizer. destruct case_RVoid. simpl. + destruct l. + apply nd_rule. + apply SFlat. + apply RVoid. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RuCanL ]. apply nd_rule. apply SFlat. apply RVoid. @@ -474,17 +463,16 @@ Section HaskSkolemizer. destruct case_RLetRec. simpl. destruct t. - destruct (getjlev (y @@@ nil)). apply nd_rule. apply SFlat. apply (@RLetRec Γ Δ lri x y nil). apply (Prelude_error "RLetRec at depth>0"). - apply (Prelude_error "RLetRec at depth>0"). destruct case_RCase. simpl. apply (Prelude_error "CASE: BIG FIXME"). Defined. + Transparent take_arg_types_as_tree. End HaskSkolemizer. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 0ad9214..791fdf5 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -955,7 +955,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) | lrsp_leaf : forall v t e , - (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) -> + (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t]@lev]) -> LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e) | lrsp_cons : forall t1 t2 b1 b2, LetRecSubproofs Γ Δ ξ lev t1 b1 -> @@ -965,7 +965,7 @@ Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ l Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : LetRecSubproofs Γ Δ ξ lev tree branches -> ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches) - |- (mapOptionTree (@snd _ _) tree) @@@ lev ]. + |- (mapOptionTree (@snd _ _) tree) @ lev ]. intro X; induction X; intros; simpl in *. apply nd_rule. apply RVoid. @@ -980,9 +980,9 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), - ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> + ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] -> LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches -> - ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]]. + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) intro branches. @@ -1021,7 +1021,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. rewrite <- mapOptionTree_compose in q''. rewrite <- ξlemma. - eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ]. clear q'. clear q''. simpl. @@ -1030,8 +1030,6 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod; auto. - rewrite ξlemma. - apply q. Defined. Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : @@ -1097,10 +1095,10 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e Definition expr2proof : forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), - ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]]. + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev τ] @ getlev τ]. refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp} - : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] := + : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [unlev τ'] @ getlev τ'] := match exp as E in Expr Γ Δ ξ τ with | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _ | EVar Γ Δ ξ ev => let case_EVar := tt in _ diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 1287b0b..24f349b 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -199,6 +199,8 @@ Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20). Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20). Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). +Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end. + Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) := match lht with t@@l => t end. -- 1.7.10.4