Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[WIP] migrating to GHC 8.10 and Coq 8.18. #205

Draft
wants to merge 24 commits into
base: master
Choose a base branch
from
Draft

[WIP] migrating to GHC 8.10 and Coq 8.18. #205

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
466f702
WIP migrating to GHC 8.10 and Coq 8.18.
lastland Jan 30, 2024
c0d5a10
Use /usr/bin/echo for non-FHS systems
nosewings Jun 25, 2024
c0e79f0
Use lia instead of omega in examples
nosewings Jun 25, 2024
b48f979
Add GHC.Maybe edits in tests
nosewings Jun 25, 2024
cbd3c9e
Emit derived instances for GHC >=8.10
Jul 17, 2024
c92b6be
Fix some instance orders
Jul 17, 2024
597d581
Merge `GHC.Maybe` into `GHC.Base`
Jul 25, 2024
ef11afa
Fix last commit
Jul 25, 2024
b0045b5
Avoid representation polymorphism in `$` and `$!`
Jul 25, 2024
d15f7f3
Documentation fix
Jul 31, 2024
c86c82d
Add `GeneralizedNewtypeDeriving` hack
nosewings Aug 22, 2024
8b4f82d
`Data.Monoid` edits
nosewings Aug 22, 2024
8c96aae
`Data.Semigroup.Internal` edits
nosewings Aug 22, 2024
7d48c59
Remove `Data.Ord` midamble
nosewings Aug 22, 2024
0820bac
Don't generate an `option` type
nosewings Aug 22, 2024
36fa552
Add `foldMap'` to `default_foldable`
nosewings Aug 23, 2024
10e3c52
Make `Data.Monoid` depend on `Control.Monad.Fail`
nosewings Aug 23, 2024
7867392
Add `Data.Foldable` edits
nosewings Aug 23, 2024
8cbc60f
Add `Data.Traversable` edits
nosewings Aug 23, 2024
d80cc67
Fix `Data.OldList`
nosewings Aug 23, 2024
6967c8a
Fix `Data.Bitraversable`
nosewings Aug 23, 2024
7383331
Minor comment fix
nosewings Aug 24, 2024
bb23c5a
Fix `Data.Functor.Compose`
nosewings Aug 27, 2024
a1bcedc
Check-in generated files
nosewings Aug 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions base/Control/Applicative.h2ci
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
constructors:
Control.Applicative.WrappedArrow: ! '[Qualified "Control.Applicative" "WrapArrow"]'
Control.Applicative.WrappedMonad: ! '[Qualified "Control.Applicative" "WrapMonad"]'
constructorFields:
Control.Applicative.WrapMonad: RecordFields [Qualified "Control.Applicative" "unwrapMonad"]
Control.Applicative.WrapArrow: RecordFields [Qualified "Control.Applicative" "unwrapArrow"]
recordFieldTypes:
Control.Applicative.unwrapMonad: Qualified "Control.Applicative" "WrappedMonad"
Control.Applicative.unwrapArrow: Qualified "Control.Applicative" "WrappedArrow"
constructorTypes:
Control.Applicative.WrapMonad: Qualified "Control.Applicative" "WrappedMonad"
Control.Applicative.WrapArrow: Qualified "Control.Applicative" "WrappedArrow"
constructors:
Control.Applicative.WrappedMonad: '[Qualified "Control.Applicative" "WrapMonad"]'
Control.Applicative.WrappedArrow: '[Qualified "Control.Applicative" "WrapArrow"]'
recordFieldTypes:
Control.Applicative.unwrapMonad: Qualified "Control.Applicative" "WrappedMonad"
Control.Applicative.unwrapArrow: Qualified "Control.Applicative" "WrappedArrow"
112 changes: 59 additions & 53 deletions base/Control/Applicative.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,17 +34,48 @@ Arguments WrapMonad {_} {_} _.

Arguments WrapArrow {_} {_} {_} _.

Definition unwrapMonad {m : Type -> Type} {a} (arg_0__ : WrappedMonad m a) :=
#[global] Definition unwrapMonad {m : Type -> Type} {a} (arg_0__
: WrappedMonad m a) :=
let 'WrapMonad unwrapMonad := arg_0__ in
unwrapMonad.

Definition unwrapArrow {a : Type -> Type -> Type} {b} {c} (arg_0__
#[global] Definition unwrapArrow {a : Type -> Type -> Type} {b} {c} (arg_0__
: WrappedArrow a b c) :=
let 'WrapArrow unwrapArrow := arg_0__ in
unwrapArrow.

(* Converted value declarations: *)

(* Skipping all instances of class `GHC.Show.Show', including
`Control.Applicative.Show__ZipList' *)

(* Skipping instance `Control.Applicative.Eq___ZipList' of class
`GHC.Base.Eq_' *)

(* Skipping instance `Control.Applicative.Ord__ZipList' of class
`GHC.Base.Ord' *)

(* Skipping all instances of class `GHC.Read.Read', including
`Control.Applicative.Read__ZipList' *)

(* Skipping instance `Control.Applicative.Functor__ZipList' of class
`GHC.Base.Functor' *)

(* Skipping instance `Control.Applicative.Foldable__ZipList' of class
`Data.Foldable.Foldable' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
`Control.Applicative.Generic__ZipList' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
`Control.Applicative.Generic1__TYPE__ZipList__LiftedRep' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
`Control.Applicative.Generic__WrappedArrow' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
`Control.Applicative.Generic1__TYPE__WrappedArrow__LiftedRep' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
`Control.Applicative.Generic__WrappedMonad' *)

Expand All @@ -55,27 +86,27 @@ Instance Unpeel_WrappedMonad {m} {a}
: HsToCoq.Unpeel.Unpeel (WrappedMonad m a) (m a) :=
HsToCoq.Unpeel.Build_Unpeel _ _ unwrapMonad WrapMonad.

Local Definition Monad__WrappedMonad_op_zgzg__ {inst_m : Type -> Type}
#[local] Definition Monad__WrappedMonad_op_zgzg__ {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type},
WrappedMonad inst_m a -> WrappedMonad inst_m b -> WrappedMonad inst_m b :=
fun {a : Type} {b : Type} => GHC.Prim.coerce _GHC.Base.>>_.
fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>_).

Local Definition Monad__WrappedMonad_op_zgzgze__ {inst_m : Type -> Type}
#[local] Definition Monad__WrappedMonad_op_zgzgze__ {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type},
WrappedMonad inst_m a ->
(a -> WrappedMonad inst_m b) -> WrappedMonad inst_m b :=
fun {a : Type} {b : Type} => GHC.Prim.coerce _GHC.Base.>>=_.
fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>=_).

Local Definition Monad__WrappedMonad_return_ {inst_m : Type -> Type}
#[local] Definition Monad__WrappedMonad_return_ {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type}, a -> WrappedMonad inst_m a :=
fun {a : Type} => GHC.Prim.coerce GHC.Base.return_.
fun {a : Type} => GHC.Prim.coerce (GHC.Base.return_).

Local Definition Applicative__WrappedMonad_liftA2 {inst_m : Type -> Type}
#[local] Definition Applicative__WrappedMonad_liftA2 {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type},
Expand All @@ -88,8 +119,8 @@ Local Definition Applicative__WrappedMonad_liftA2 {inst_m : Type -> Type}
| f, WrapMonad x, WrapMonad y => WrapMonad (GHC.Base.liftM2 f x y)
end.

Local Definition Applicative__WrappedMonad_op_zlztzg__ {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
#[local] Definition Applicative__WrappedMonad_op_zlztzg__ {inst_m
: Type -> Type} `{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type},
WrappedMonad inst_m (a -> b) ->
Expand All @@ -100,7 +131,7 @@ Local Definition Applicative__WrappedMonad_op_zlztzg__ {inst_m : Type -> Type}
| WrapMonad f, WrapMonad v => WrapMonad (GHC.Base.ap f v)
end.

Local Definition Functor__WrappedMonad_fmap {inst_m : Type -> Type}
#[local] Definition Functor__WrappedMonad_fmap {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type}, (a -> b) -> WrappedMonad inst_m a -> WrappedMonad inst_m b :=
Expand All @@ -110,13 +141,14 @@ Local Definition Functor__WrappedMonad_fmap {inst_m : Type -> Type}
| f, WrapMonad v => WrapMonad (GHC.Base.liftM f v)
end.

Local Definition Functor__WrappedMonad_op_zlzd__ {inst_m : Type -> Type}
#[local] Definition Functor__WrappedMonad_op_zlzd__ {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type}, a -> WrappedMonad inst_m b -> WrappedMonad inst_m a :=
fun {a : Type} {b : Type} =>
Functor__WrappedMonad_fmap GHC.Base.∘ GHC.Base.const.

#[global]
Program Instance Functor__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
: GHC.Base.Functor (WrappedMonad m) :=
fun _ k__ =>
Expand All @@ -125,7 +157,7 @@ Program Instance Functor__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
Functor__WrappedMonad_op_zlzd__ |}.

Local Definition Applicative__WrappedMonad_op_ztzg__ {inst_m : Type -> Type}
#[local] Definition Applicative__WrappedMonad_op_ztzg__ {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type},
Expand All @@ -134,11 +166,12 @@ Local Definition Applicative__WrappedMonad_op_ztzg__ {inst_m : Type -> Type}
fun a1 a2 =>
Applicative__WrappedMonad_op_zlztzg__ (GHC.Base.id GHC.Base.<$ a1) a2.

Local Definition Applicative__WrappedMonad_pure {inst_m : Type -> Type}
#[local] Definition Applicative__WrappedMonad_pure {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type}, a -> WrappedMonad inst_m a :=
fun {a : Type} => WrapMonad GHC.Base.∘ GHC.Base.pure.

#[global]
Program Instance Applicative__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad
m}
: GHC.Base.Applicative (WrappedMonad m) :=
Expand All @@ -151,6 +184,7 @@ Program Instance Applicative__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad
Applicative__WrappedMonad_op_ztzg__ ;
GHC.Base.pure__ := fun {a : Type} => Applicative__WrappedMonad_pure |}.

#[global]
Program Instance Monad__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
: GHC.Base.Monad (WrappedMonad m) :=
fun _ k__ =>
Expand All @@ -160,40 +194,10 @@ Program Instance Monad__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
Monad__WrappedMonad_op_zgzgze__ ;
GHC.Base.return___ := fun {a : Type} => Monad__WrappedMonad_return_ |}.

(* Skipping all instances of class `GHC.Generics.Generic', including
`Control.Applicative.Generic__WrappedArrow' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
`Control.Applicative.Generic1__TYPE__WrappedArrow__LiftedRep' *)

(* Skipping all instances of class `GHC.Show.Show', including
`Control.Applicative.Show__ZipList' *)

(* Skipping instance `Control.Applicative.Eq___ZipList' of class
`GHC.Base.Eq_' *)

(* Skipping instance `Control.Applicative.Ord__ZipList' of class
`GHC.Base.Ord' *)

(* Skipping all instances of class `GHC.Read.Read', including
`Control.Applicative.Read__ZipList' *)

(* Skipping instance `Control.Applicative.Functor__ZipList' of class
`GHC.Base.Functor' *)

(* Skipping instance `Control.Applicative.Foldable__ZipList' of class
`Data.Foldable.Foldable' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
`Control.Applicative.Generic__ZipList' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
`Control.Applicative.Generic1__TYPE__ZipList__LiftedRep' *)

(* Skipping all instances of class `GHC.Base.Alternative', including
`Control.Applicative.Alternative__WrappedMonad' *)

Local Definition Functor__WrappedArrow_fmap {inst_a : Type -> Type -> Type}
#[local] Definition Functor__WrappedArrow_fmap {inst_a : Type -> Type -> Type}
{inst_b : Type} `{Control.Arrow.Arrow inst_a}
: forall {a : Type},
forall {b : Type},
Expand All @@ -204,14 +208,15 @@ Local Definition Functor__WrappedArrow_fmap {inst_a : Type -> Type -> Type}
| f, WrapArrow a => WrapArrow (a Control.Category.>>> Control.Arrow.arr f)
end.

Local Definition Functor__WrappedArrow_op_zlzd__ {inst_a : Type -> Type -> Type}
{inst_b : Type} `{Control.Arrow.Arrow inst_a}
#[local] Definition Functor__WrappedArrow_op_zlzd__ {inst_a
: Type -> Type -> Type} {inst_b : Type} `{Control.Arrow.Arrow inst_a}
: forall {a : Type},
forall {b : Type},
a -> WrappedArrow inst_a inst_b b -> WrappedArrow inst_a inst_b a :=
fun {a : Type} {b : Type} =>
Functor__WrappedArrow_fmap GHC.Base.∘ GHC.Base.const.

#[global]
Program Instance Functor__WrappedArrow {a : Type -> Type -> Type} {b : Type}
`{Control.Arrow.Arrow a}
: GHC.Base.Functor (WrappedArrow a b) :=
Expand All @@ -221,7 +226,7 @@ Program Instance Functor__WrappedArrow {a : Type -> Type -> Type} {b : Type}
GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
Functor__WrappedArrow_op_zlzd__ |}.

Local Definition Applicative__WrappedArrow_liftA2 {inst_a
#[local] Definition Applicative__WrappedArrow_liftA2 {inst_a
: Type -> Type -> Type} {inst_b : Type} `{Control.Arrow.Arrow inst_a}
: forall {a : Type},
forall {b : Type},
Expand All @@ -237,15 +242,15 @@ Local Definition Applicative__WrappedArrow_liftA2 {inst_a
Control.Arrow.arr (Data.Tuple.uncurry f))
end.

Local Definition Applicative__WrappedArrow_op_zlztzg__ {inst_a
#[local] Definition Applicative__WrappedArrow_op_zlztzg__ {inst_a
: Type -> Type -> Type} {inst_b : Type} `{Control.Arrow.Arrow inst_a}
: forall {a : Type},
forall {b : Type},
WrappedArrow inst_a inst_b (a -> b) ->
WrappedArrow inst_a inst_b a -> WrappedArrow inst_a inst_b b :=
fun {a : Type} {b : Type} => Applicative__WrappedArrow_liftA2 GHC.Base.id.

Local Definition Applicative__WrappedArrow_op_ztzg__ {inst_a
#[local] Definition Applicative__WrappedArrow_op_ztzg__ {inst_a
: Type -> Type -> Type} {inst_b : Type} `{Control.Arrow.Arrow inst_a}
: forall {a : Type},
forall {b : Type},
Expand All @@ -255,11 +260,12 @@ Local Definition Applicative__WrappedArrow_op_ztzg__ {inst_a
fun a1 a2 =>
Applicative__WrappedArrow_op_zlztzg__ (GHC.Base.id GHC.Base.<$ a1) a2.

Local Definition Applicative__WrappedArrow_pure {inst_a : Type -> Type -> Type}
{inst_b : Type} `{Control.Arrow.Arrow inst_a}
#[local] Definition Applicative__WrappedArrow_pure {inst_a
: Type -> Type -> Type} {inst_b : Type} `{Control.Arrow.Arrow inst_a}
: forall {a : Type}, a -> WrappedArrow inst_a inst_b a :=
fun {a : Type} => fun x => WrapArrow (Control.Arrow.arr (GHC.Base.const x)).

#[global]
Program Instance Applicative__WrappedArrow {a : Type -> Type -> Type} {b : Type}
`{Control.Arrow.Arrow a}
: GHC.Base.Applicative (WrappedArrow a b) :=
Expand Down
Loading
Loading