{-# 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))
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
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 ].
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.
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.
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
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
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
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 =>
(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'
(* 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.
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 ].
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 ].
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 ].
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 ].
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_ ].
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 ].
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.
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 ].
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.
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 ].
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 _ _ _ _ _
[Γ > Δ > 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.
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.
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.
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.
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'.
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 _
| 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 _
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").
Transparent flatten_judgment.
idtac.
unfold flatten_judgment.
- unfold getjlev.
destruct lev.
apply nd_rule. apply RVar.
repeat drop_simplify.
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.
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.
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 ].
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.
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.
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.
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 [ ].
(* 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)
| 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).
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))
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"
| 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 :=
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.
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 Γ Δ ξ τ.
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.
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.
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.
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.
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 _).
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 _
| 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.
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.
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").
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.
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.
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 _
| 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 _
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.
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.
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.
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.
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.
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.
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 [].
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.
auto.
refine (return OK _).
exists ξ.
- apply (ileaf it).
+ apply ileaf in it.
+ simpl in it.
+ destruct τ.
+ apply it.
apply INone.
Defined.
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)
| 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 Γ ★) :=
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 Γ ★),
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 _
| 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 _
destruct case_RArrange.
simpl.
- destruct (getjlev x).
+ destruct l.
apply nd_rule.
apply SFlat.
apply RArrange.
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.
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.
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.
{ 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 [[Γ]].
| 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,
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)
{Γ} 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.
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 ].
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.
| 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
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.
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.
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 ->
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.
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.
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.
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.
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.
(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'))
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 _
| 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')
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 []
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.
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.
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.
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.
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 Γ Δ ξ τ)
; 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
; 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
; 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'
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.
; 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.
Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
-Fixpoint update_ξ
+Fixpoint update_xi
`{EQD_VV:EqDecidable VV}{Γ}
(ξ:VV -> LeveledHaskType Γ ★)
(lev:HaskLevel Γ)
: 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.
Require Import HaskKinds.
Require Import HaskLiterals.
Require Import HaskTyCons.
+Require Import HaskCoreVars.
Require Import HaskWeakVars.
Require Import HaskWeakTypes.
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
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'
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.
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.
(* 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.
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)).
| 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
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'".
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.
; 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.
Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
-Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
+Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
intros.
refine (ψ X >>= _).
| 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')
| 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')
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')
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
(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))
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)) =>
>>= 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 [ _ ]
projects / coq-hetmet.git / commitdiff