From: Adam Megacz Date: Sat, 28 May 2011 14:15:59 +0000 (-0700) Subject: Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=649b9b9ce6db92cc131a1c048c1d9c8719180c58;hp=ada4d4ef74dbd3ca46b4f80eec68e10b903d75f4 Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet --- diff --git a/examples/Demo.hs b/examples/Demo.hs index afedde6..4c53aa5 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -1,15 +1,21 @@ {-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-} module Demo (demo) where + --demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]> --- demo const mult = <[ let q = ~~(const (1::Int)) in ~~mult q q ]> +demo const mult = + <[ let twelve = ~~(const (12::Int)) + four = ~~(const ( 4::Int)) + in ~~mult four (~~mult four twelve) + ]> +{- demo const mult = <[ let twelve = ~~(const (12::Int)) in let four = ~~(const (4::Int)) in ~~mult four twelve ]> - +-} {- demo const mult = <[ let twelve = ~~(const (12::Int)) diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index c63fd15..2c53283 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -46,8 +46,8 @@ data GArrowSkeleton m :: * -> * -> * GAS_copy :: GArrowSkeleton m x (x,x) GAS_swap :: GArrowSkeleton m (x,y) (y,x) GAS_merge :: GArrowSkeleton m (x,y) z - GAS_loopl :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y - GAS_loopr :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y + GAS_loopl :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y + GAS_loopr :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y GAS_misc :: m x y -> GArrowSkeleton m x y instance Category (GArrowSkeleton m) where 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/General.v b/src/General.v index 5d19e9c..ae27b9f 100644 --- a/src/General.v +++ b/src/General.v @@ -866,6 +866,8 @@ Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))). (* boolean "not" *) Definition bnot (b:bool) : bool := if b then false else true. +Definition band (b1 b2:bool) : bool := if b1 then b2 else false. +Definition bor (b1 b2:bool) : bool := if b1 then true else b2. (* string stuff *) Variable eol : string. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 308e669..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. @@ -1220,8 +1188,17 @@ Section HaskFlattener. destruct case_RLetRec. rename t into lev. - simpl. - apply (Prelude_error "LetRec not supported (FIXME)"). + simpl. destruct lev; simpl. + apply nd_rule. + set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as 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. + apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)"). destruct case_RCase. simpl. @@ -1239,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 a8b311e..d92dd6b 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -29,17 +29,18 @@ 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} := { pcb_freevars : Tree ??(LeveledHaskType Γ ★) -; pcb_judg := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ) +; 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 6ba094e..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 Γ Δ ξ τ. @@ -42,7 +42,7 @@ Section HaskProofToStrong. Defined. Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q, - update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q. + update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q. intros. induction l1. reflexivity. @@ -122,7 +122,7 @@ Section HaskProofToStrong. Lemma fresh_lemma'' Γ : forall types ξ lev, FreshM { varstypes : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. admit. Defined. @@ -130,8 +130,8 @@ Section HaskProofToStrong. Lemma fresh_lemma' Γ : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars -> FreshM { varstypes : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ - /\ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ + /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. induction types. intros; destruct a. @@ -164,7 +164,7 @@ Section HaskProofToStrong. intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _). apply FreshMon. destruct x2 as [vt2 [pf21 [pf22 pfdist]]]. - refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev + refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev (leaves vt2)) _ _; return _). apply FreshMon. simpl. @@ -204,8 +204,8 @@ Section HaskProofToStrong. Lemma fresh_lemma Γ ξ vars Σ Σ' lev : Σ = mapOptionTree ξ vars -> FreshM { vars' : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ - /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }. + | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ + /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }. intros. set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q. refine (q >>>= fun q' => return _). @@ -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"). @@ -419,7 +421,7 @@ Section HaskProofToStrong. prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} -> ((fun sac => FreshM { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac - & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)). + & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)). intro pcb. intro X. simpl in X. @@ -445,10 +447,10 @@ Section HaskProofToStrong. cut (distinct (vec2list localvars'')). intro H'''. set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb. - refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _). + refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _). apply FreshMon. simpl. - unfold scbwv_ξ. + unfold scbwv_xi. rewrite vars_pf. rewrite <- mapOptionTree_compose. clear localvars_pf1. @@ -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. @@ -581,7 +581,7 @@ Section HaskProofToStrong. refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)). apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *. + set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *. refine (X_ ξ' (vars,,[vnew]) _ >>>= _). apply FreshMon. simpl. @@ -648,7 +648,7 @@ Section HaskProofToStrong. apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. @@ -687,7 +687,7 @@ Section HaskProofToStrong. apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. @@ -751,7 +751,7 @@ Section HaskProofToStrong. apply ILeaf; simpl; intros. refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon. destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]]. - refine (X_ ((update_ξ ξ t (leaves varstypes))) + refine (X_ ((update_xi ξ t (leaves varstypes))) (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon. simpl. rewrite pf2. @@ -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. @@ -824,7 +832,7 @@ Section HaskProofToStrong. clear q. destruct q' as [varstypes [pf1 [pf2 distpf]]]. exists (mapOptionTree (@fst _ _) varstypes). - exists (update_ξ ξ l (leaves varstypes)). + exists (update_xi ξ l (leaves varstypes)). symmetry; auto. refine (return _). exists []. @@ -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/HaskStrong.v b/src/HaskStrong.v index d52acb9..ed3cd92 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -25,7 +25,7 @@ Section HaskStrong. { scbwv_exprvars : vec VV (sac_numExprVars sac) ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars) ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types sac Γ atypes) - ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) + ; scbwv_xi := fun ξ lev => update_xi (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) }. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. @@ -37,8 +37,8 @@ Section HaskStrong. | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l) | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l) - | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) - | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) + | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_xi ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) + | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_xi ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l)) | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l) | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, @@ -55,15 +55,15 @@ Section HaskStrong. Expr Γ Δ ξ (caseType tc atypes @@ l) -> Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } } -> Expr Γ Δ ξ (tbranches @@ l) | ELetRec : ∀ Γ Δ ξ l τ vars, distinct (leaves (mapOptionTree (@fst _ _) vars)) -> - let ξ' := update_ξ ξ l (leaves vars) in + let ξ' := update_xi ξ l (leaves vars) in ELetRecBindings Γ Δ ξ' l vars -> Expr Γ Δ ξ' (τ@@l) -> Expr Γ Δ ξ (τ@@l) diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 5f3baa3..791fdf5 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -330,7 +330,7 @@ Lemma updating_stripped_tree_is_inert' {Γ} lev (ξ:VV -> LeveledHaskType Γ ★) lv tree2 : - mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) + mapOptionTree (update_xi ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2). induction tree2. @@ -459,10 +459,10 @@ Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (ap inversion H; auto. Qed. -Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : +Lemma update_xiv_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : forall v1 v2, distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) -> - mapOptionTree (update_ξ ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (update_xi ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) = mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). induction varstypes; intros. destruct a; simpl; [ idtac | reflexivity ]. @@ -510,11 +510,11 @@ Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstyp repeat rewrite ass_app in *; auto. Qed. -Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : +Lemma update_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : distinct (map (@fst _ _) (leaves varstypes)) -> - mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). - set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q. + set (update_xiv_lemma' Γ ξ lev varstypes [] []) as q. simpl in q. rewrite <- app_nil_end in q. apply q. @@ -543,9 +543,9 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } } ): Tree ??VV := match alts with @@ -563,9 +563,9 @@ end. Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } }) : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. destruct alt. @@ -943,7 +943,7 @@ Definition factorContextRightAndWeaken'' Defined. Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev : - mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) + mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) = mapOptionTree ξ (stripOutVars (v :: nil) tree). set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p. rewrite p. @@ -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_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> - LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches -> - ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches 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]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) intro branches. @@ -995,10 +995,10 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : apply disti. rewrite mapleaves in disti'. - set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma. + set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma. rewrite <- mapOptionTree_compose in ξlemma. - set ((update_ξ ξ lev (leaves tree))) as ξ' in *. + set ((update_xi ξ 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. @@ -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,19 +1030,17 @@ 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} : forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac, forall l ξ, - vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) = + vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) = vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)). intros. - unfold scbwv_ξ. + unfold scbwv_xi. unfold scbwv_varstypes. - set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l) + set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l) (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes)))) ) as q. rewrite <- mapleaves' in q. @@ -1068,8 +1066,8 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e (alts':Tree ??{sac : StrongAltCon & {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac & - Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}), + Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches @@ l))}}), (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) (mapOptionTree mkProofCaseBranch alts')) @@ -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 _ @@ -1111,7 +1109,7 @@ Definition expr2proof : | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree disti branches ebody => - let ξ' := update_ξ ξ lev (leaves tree) in + let ξ' := update_xi ξ lev (leaves tree) in let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree') @@ -1134,9 +1132,9 @@ Definition expr2proof : let dcsp := ((fix mkdcsp (alts: Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } }) : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := match alts as ALTS return ND Rule [] @@ -1179,13 +1177,13 @@ Definition expr2proof : destruct case_ELam; intros. unfold mapOptionTree; simpl; fold (mapOptionTree ξ). eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ]. - set (update_ξ ξ lev ((v,t1)::nil)) as ξ'. + set (update_xi ξ lev ((v,t1)::nil)) as ξ'. set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. eapply RArrange in pfx. unfold mapOptionTree in pfx; simpl in pfx. unfold ξ' in pfx. rewrite updating_stripped_tree_is_inert in pfx. - unfold update_ξ in pfx. + unfold update_xi in pfx. destruct (eqd_dec v v). eapply nd_comp; [ idtac | apply (nd_rule pfx) ]. clear pfx. @@ -1203,15 +1201,15 @@ Definition expr2proof : eapply nd_comp; [ apply pf_body | idtac ]. fold (@mapOptionTree VV). fold (mapOptionTree ξ). - set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. + set (update_xi ξ v ((lev,tv)::nil)) as ξ'. set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') 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. + unfold update_xi in n. destruct (eqd_dec lev lev). unfold ξ'. - unfold update_ξ. + unfold update_xi. eapply RArrange in n. apply (nd_rule n). assert False. apply n0; auto. inversion H. @@ -1266,15 +1264,15 @@ Definition expr2proof : rewrite mapleaves'. simpl. rewrite <- mapOptionTree_compose. - unfold scbwv_ξ. + unfold scbwv_xi. rewrite <- mapleaves'. rewrite vec2list_map_list2vec. - unfold sac_Γ. + unfold sac_gamma. rewrite <- (scbwv_coherent scbx l ξ). rewrite <- vec2list_map_list2vec. rewrite mapleaves'. set (@factorContextRightAndWeaken'') as q. - unfold scbwv_ξ. + unfold scbwv_xi. set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z. unfold scbwv_varstypes in z. rewrite vec2list_map_list2vec in z. @@ -1285,7 +1283,7 @@ Definition expr2proof : replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). apply q. - apply (sac_Δ sac Γ atypes (weakCK'' Δ)). + apply (sac_delta sac Γ atypes (weakCK'' Δ)). rewrite leaves_unleaves. apply (scbwv_exprvars_distinct scbx). rewrite leaves_unleaves. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index 25ecd7b..d86d05b 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -95,16 +95,16 @@ Section HaskStrongToWeak. Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}. - Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar := + Definition update_chi (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar := fun vv' => if eqd_dec vv vv' then OK ev' else χ vv'. - Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar := + Fixpoint update_chi' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar := match varsexprs with | nil => χ - | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev + | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev end. Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ) @@ -116,12 +116,12 @@ Section HaskStrongToWeak. ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g)) | ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite ; bind ev' = mkWeakExprVar tv' - ; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite + ; bind e' = exprToWeakExpr (update_chi χ cv ev') e ite ; return WELam ev' e' | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => bind tv' = typeToWeakType t ite ; bind e1' = exprToWeakExpr χ e1 ite ; bind ev' = mkWeakExprVar tv' - ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite + ; bind e2' = exprToWeakExpr (update_chi χ ev ev') e2 ite ; return WELet ev' e1' e2' | ELit _ _ _ lit _ => fun ite => return WELit lit | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite @@ -172,7 +172,7 @@ Section HaskStrongToWeak. ; bind v' = mkWeakExprVar tleaf ; return ((fst vt),v')) varstypes) - ; let χ' := update_χ' χ exprvars in + ; let χ' := update_chi' χ exprvars in bind e'' = exprToWeakExpr χ' e (snd evars_ite) ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')] | T_Branch b1 b2 => bind b1' = caseBranches b1 @@ -188,7 +188,7 @@ Section HaskStrongToWeak. ; bind v' = mkWeakExprVar tleaf ; return ((fst vt),v')) (leaves vars)) - ; let χ' := update_χ' χ vars' in + ; let χ' := update_chi' χ vars' in bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite ; bind e' = exprToWeakExpr χ' e ite ; return WELetRec elrb' e' diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 764e95f..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. @@ -439,10 +441,10 @@ Record StrongAltCon {tc:TyCon} := ; sac_numExprVars : nat ; sac_ekinds : vec Kind sac_numExTyVars ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds) -; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ -; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars -; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars -; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ +; sac_gamma := fun Γ => app (vec2list sac_ekinds) Γ +; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars +; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars +; sac_delta := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ }. Coercion sac_tc : StrongAltCon >-> TyCon. Coercion sac_altcon : StrongAltCon >-> WeakAltCon. @@ -462,7 +464,7 @@ Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★. Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18). -Fixpoint update_ξ +Fixpoint update_xi `{EQD_VV:EqDecidable VV}{Γ} (ξ:VV -> LeveledHaskType Γ ★) (lev:HaskLevel Γ) @@ -470,12 +472,12 @@ Fixpoint update_ξ : VV -> LeveledHaskType Γ ★ := match vt with | nil => ξ - | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v' + | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v' end. -Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v, +Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v, not (In v (map (@fst _ _) varstypes)) -> - (update_ξ ξ lev varstypes) v = ξ v. + (update_xi ξ lev varstypes) v = ξ v. intros. induction varstypes. reflexivity. diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 22f0e60..670d8bd 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -9,6 +9,7 @@ Require Import Coq.Lists.List. Require Import HaskKinds. Require Import HaskLiterals. Require Import HaskTyCons. +Require Import HaskCoreVars. Require Import HaskWeakVars. Require Import HaskWeakTypes. @@ -52,3 +53,59 @@ Inductive WeakExpr := Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType := (WTyCon (haskLiteralToTyCon lit)). +(* +Fixpoint weakExprVarOccursFree (wvf:WeakExprVar)(we:WeakExpr) : bool := + match we with + | WEVar wv => if eqd_dec (wvf:CoreVar) (wv:CoreVar) then true else false + | WELit lit => false + | WEApp e1 e2 => weakExprVarOccursFree wvf e1 || weakExprVarOccursFree wvf e2 + | WETyApp e t => weakExprVarOccursFree wvf e + | WECoApp e co => weakExprVarOccursFree wvf e + | WENote n e => weakExprVarOccursFree wvf e + | WELam ev e => if eqd_dec (wvf:CoreVar) (ev:CoreVar) then false else weakExprVarOccursFree wvf e + | WETyLam tv e => weakExprVarOccursFree wvf e + | WECoLam cv e => weakExprVarOccursFree wvf e + | WECast e co => weakExprVarOccursFree wvf e + | WEBrak v wtv e t => weakExprVarOccursFree wvf e + | WEEsc v wtv e t => weakExprVarOccursFree wvf e + | WECSP v wtv e t => weakExprVarOccursFree wvf e + | WELet v ebind ebody => weakExprVarOccursFree wvf ebind + || if eqd_dec (wvf:CoreVar) (v:CoreVar) then false else weakExprVarOccursFree wvf ebody + | WECase vs es tb tc tys alts => + if weakExprVarOccursFree wvf es + then true + else (fix weakExprVarOccursFreeBranches (alts:Tree ??(_)) : bool := + match alts with + | T_Leaf None => false + | T_Leaf (Some (_,_,_,v',e')) => + if fold_left bor (map (fun v'':WeakExprVar => if eqd_dec (wvf:CoreVar) (v'':CoreVar) then true else false ) v') false + then false + else weakExprVarOccursFree wvf e' + | T_Branch b1 b2 => weakExprVarOccursFreeBranches b1 || + weakExprVarOccursFreeBranches b2 + end) alts + | WELetRec mlr e => false + end. + +(* some very simple-minded cleanups to produce "prettier" expressions *) +Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr := + match me with + | WEVar wv => WEVar wv + | WELit lit => WELit lit + | WEApp e1 e2 => WEApp (simplifyWeakExpr e1) (simplifyWeakExpr e2) + | WETyApp e t => WETyApp (simplifyWeakExpr e ) t + | WECoApp e co => CoreEApp (simplifyWeakExpr e ) co + | WENote n e => CoreENote n (simplifyWeakExpr e ) + | WELam ev e => CoreELam ev (simplifyWeakExpr e ) + | WETyLam tv e => CoreELam tv (simplifyWeakExpr e ) + | WECoLam cv e => CoreELam cv (simplifyWeakExpr e ) + | WECast e co => CoreECast (simplifyWeakExpr e ) co + | WEBrak v wtv e t => WEBrak v wtv (simplifyWeakExpr e ) t + | WEEsc v wtv e t => WEEsc v wtv (simplifyWeakExpr e ) t + | WECSP v wtv e t => WECSP v wtv (simplifyWeakExpr e ) t + | WELet v ebind ebody => WELet v (simplifyWeakExpr ebind) (simplifyWeakExpr ebody) + | WECase vs es tb tc tys alts => WECase vs es tb tc tys (* FIXME alts *) + (* un-letrec-ify multi branch letrecs *) + | WELetRec mlr e => WELetRec mlr (simplifyWeakExpr e ) + end. +*) \ No newline at end of file diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 7dd93ad..1565637 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -25,7 +25,7 @@ Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ). -Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). +Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). unfold TyVarResolver. refine (fun tv' => if eqd_dec tv tv' @@ -34,12 +34,12 @@ Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:K rewrite <- _H; apply fresh. Defined. -Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ) +Definition upPhi2 {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ) : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). induction tvs. apply φ. simpl. - apply upφ. + apply upPhi. apply IHtvs. Defined. @@ -54,7 +54,7 @@ Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ: apply X. Defined. -Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. +Definition substphi {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. induction lk. intro q; apply q. simpl. @@ -71,8 +71,8 @@ Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *) Record StrongAltConPlusJunk {tc:TyCon} := { sacpj_sac : @StrongAltCon tc -; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ)) -; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)) +; sacpj_phi : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_gamma sacpj_sac Γ)) +; sacpj_psi : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_delta sacpj_sac Γ atypes (weakCK'' Δ)) }. Implicit Arguments StrongAltConPlusJunk [ ]. Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon. @@ -83,9 +83,9 @@ Variable emptyφ : TyVarResolver nil. Definition mkPhi (lv:list WeakTypeVar) : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)). - set (upφ'(Γ:=nil) lv emptyφ) as φ'. - rewrite <- app_nil_end in φ'. - apply φ'. + set (upPhi2(Γ:=nil) lv emptyφ) as φ2. + rewrite <- app_nil_end in φ2. + apply φ2. Defined. Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)). @@ -125,7 +125,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented" | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _ | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _ - | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _ + | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upPhi wtv φ) t >>= fun t => _ | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _ | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in @@ -240,9 +240,9 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds intro ct. apply (addErrorMessage "weakTypeToType'"). set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'. - set (@substφ _ _ avars') as q. - set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'. - set (@weakTypeToType _ φ' ct) as t. + set (@substphi _ _ avars') as q. + set (upPhi2 (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ2. + set (@weakTypeToType _ φ2 ct) as t. destruct t as [|t]; try apply (Error error_message). destruct t as [tk t]. matchThings tk ★ "weakTypeToType'". @@ -327,17 +327,17 @@ Lemma weakCV' : forall {Γ}{Δ} Γ', Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. refine {| sacpj_sac := mkStrongAltCon - ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv')) - ; sacpj_ψ := + ; sacpj_phi := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv')) + ; sacpj_psi := fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv'))) |}. intro. - unfold sac_Γ. + unfold sac_gamma. unfold HaskCoVar in *. intros. apply (x TV CV env). simpl in cenv. - unfold sac_Δ in *. + unfold sac_delta in *. unfold InstantiatedCoercionEnv in *. apply vec_chop' in cenv. apply cenv. @@ -371,13 +371,13 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAlt ; sac_altcon := WeakLitAlt h |} |}. intro; intro φ; apply φ. - intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. + intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl. rewrite weakCK'_nil_inert. apply ψ. apply OK; refine {| sacpj_sac := {| sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil ; sac_altcon := WeakDEFAULT |} |}. intro; intro φ; apply φ. - intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. + intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl. rewrite weakCK'_nil_inert. apply ψ. Defined. @@ -387,7 +387,7 @@ Definition weakExprVarToWeakType : WeakExprVar -> WeakType := Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ. -Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) : +Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) : WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)). intros. refine (ψ X >>= _). @@ -567,7 +567,7 @@ Definition weakExprToStrongExpr : forall | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv => weakTypeOfWeakExpr ebody >>= fun tbody => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => - let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in + let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in let ig' := update_ig ig ((ev:CoreVar)::nil) in weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' => castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody') @@ -591,7 +591,7 @@ Definition weakExprToStrongExpr : forall | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv => weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil)) + weakExprToStrongExpr Γ Δ φ ψ (update_xi ξ lev (((v:CoreVar),tv)::nil)) (update_ig ig ((v:CoreVar)::nil)) τ lev ebody >>= fun ebody' => OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody') @@ -602,18 +602,18 @@ Definition weakExprToStrongExpr : forall weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' => OK (EApp _ _ _ _ _ _ e1' e2') - | WETyLam tv e => let φ' := upφ tv φ in + | WETyLam tv e => let φ2 := upPhi tv φ in weakTypeOfWeakExpr e >>= fun te => - weakTypeToTypeOfKind φ' te ★ >>= fun τ' => - weakExprToStrongExpr _ (weakCE Δ) φ' + weakTypeToTypeOfKind φ2 te ★ >>= fun τ' => + weakExprToStrongExpr _ (weakCE Δ) φ2 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e') | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => match te with | WForAllTy wtv te' => - let φ' := upφ wtv φ in - weakTypeToTypeOfKind φ' te' ★ >>= fun te'' => + let φ2 := upPhi wtv φ in + weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' => weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' => castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e') @@ -641,7 +641,7 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ te ★ >>= fun te' => weakTypeToTypeOfKind φ t1 cv >>= fun t1' => weakTypeToTypeOfKind φ t2 cv >>= fun t2' => - weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' => + weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' => castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') | WECast e co => let (t1,t2) := weakCoercionTypes co in @@ -652,7 +652,7 @@ Definition weakExprToStrongExpr : forall (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') | WELetRec rb e => - let ξ' := update_ξ ξ lev _ in + let ξ' := update_xi ξ lev _ in let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in let binds := (fix binds (t:Tree ??(WeakExprVar * WeakExpr)) @@ -679,7 +679,7 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' => (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac & - Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) := + Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakLT' (tbranches' @@ lev))}}) := match t with | T_Leaf None => OK [] | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => @@ -688,9 +688,9 @@ Definition weakExprToStrongExpr : forall >>= fun exprvars' => (let case_pf := tt in _) >>= fun pf => let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in - weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) - (sacpj_ψ sac _ _ avars' ψ) - (scbwv_ξ scb ξ lev) + weakExprToStrongExpr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ)) (sacpj_phi sac _ φ) + (sacpj_psi sac _ _ avars' ψ) + (scbwv_xi scb ξ lev) (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb)))) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' => let case_case := tt in OK [ _ ]