Skip to content

Commit

Permalink
Check-in generated files
Browse files Browse the repository at this point in the history
  • Loading branch information
@nosewings
nosewings committed Aug 27, 2024
1 parent bb23c5a commit a1bcedc
Show file tree
Hide file tree
Showing 19 changed files with 2,463 additions and 1,350 deletions.
119 changes: 94 additions & 25 deletions base/Control/Applicative.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Require Control.Arrow.
Require Control.Category.
Require Data.Tuple.
Require GHC.Base.
Require GHC.Prim.
Require HsToCoq.Unpeel.
Import Control.Arrow.Notations.
Import Control.Category.Notations.
Expand Down Expand Up @@ -45,31 +46,65 @@ Arguments WrapArrow {_} {_} {_} _.

(* Converted value declarations: *)

#[local] Definition Functor__WrappedMonad_fmap {inst_m : Type -> Type}
(* 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' *)

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

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}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
forall {b : Type}, (a -> b) -> WrappedMonad inst_m a -> WrappedMonad inst_m b :=
fun {a : Type} {b : Type} =>
fun arg_0__ arg_1__ =>
match arg_0__, arg_1__ with
| f, WrapMonad v => WrapMonad (GHC.Base.liftM f v)
end.
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.>>_).

#[local] Definition Functor__WrappedMonad_op_zlzd__ {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}, a -> WrappedMonad inst_m b -> WrappedMonad inst_m a :=
fun {a : Type} {b : Type} =>
Functor__WrappedMonad_fmap GHC.Base.∘ GHC.Base.const.
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.>>=_).

#[global]
Program Instance Functor__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
: GHC.Base.Functor (WrappedMonad m) :=
fun _ k__ =>
k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} =>
Functor__WrappedMonad_fmap ;
GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
Functor__WrappedMonad_op_zlzd__ |}.
#[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_).

#[local] Definition Applicative__WrappedMonad_liftA2 {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
Expand All @@ -96,6 +131,32 @@ Program Instance Functor__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
| WrapMonad f, WrapMonad v => WrapMonad (GHC.Base.ap f v)
end.

#[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 :=
fun {a : Type} {b : Type} =>
fun arg_0__ arg_1__ =>
match arg_0__, arg_1__ with
| f, WrapMonad v => WrapMonad (GHC.Base.liftM f v)
end.

#[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__ =>
k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} =>
Functor__WrappedMonad_fmap ;
GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
Functor__WrappedMonad_op_zlzd__ |}.

#[local] Definition Applicative__WrappedMonad_op_ztzg__ {inst_m : Type -> Type}
`{GHC.Base.Monad inst_m}
: forall {a : Type},
Expand Down Expand Up @@ -123,6 +184,16 @@ 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__ =>
k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
Monad__WrappedMonad_op_zgzg__ ;
GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} =>
Monad__WrappedMonad_op_zgzgze__ ;
GHC.Base.return___ := fun {a : Type} => Monad__WrappedMonad_return_ |}.

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

Expand Down Expand Up @@ -222,16 +293,14 @@ Instance Unpeel_WrappedArrow {a} {b} {c}
: HsToCoq.Unpeel.Unpeel (WrappedArrow a b c) (a b c) :=
HsToCoq.Unpeel.Build_Unpeel _ _ unwrapArrow WrapArrow.

Instance Unpeel_WrappedMonad {m} {a}
: HsToCoq.Unpeel.Unpeel (WrappedMonad m a) (m a) :=
HsToCoq.Unpeel.Build_Unpeel _ _ unwrapMonad WrapMonad.

(* External variables:
Type Control.Arrow.Arrow Control.Arrow.arr Control.Arrow.op_zazaza__
Control.Category.op_zgzgzg__ Data.Tuple.uncurry GHC.Base.Applicative
GHC.Base.Functor GHC.Base.Monad GHC.Base.ap GHC.Base.const GHC.Base.fmap__
GHC.Base.id GHC.Base.liftA2__ GHC.Base.liftM GHC.Base.liftM2
GHC.Base.op_z2218U__ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
GHC.Base.op_zlztzg____ GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__
GHC.Base.op_z2218U__ GHC.Base.op_zgzg__ GHC.Base.op_zgzg____
GHC.Base.op_zgzgze__ GHC.Base.op_zgzgze____ GHC.Base.op_zlzd__
GHC.Base.op_zlzd____ GHC.Base.op_zlztzg____ GHC.Base.op_ztzg____ GHC.Base.pure
GHC.Base.pure__ GHC.Base.return_ GHC.Base.return___ GHC.Prim.coerce
HsToCoq.Unpeel.Build_Unpeel HsToCoq.Unpeel.Unpeel
*)
22 changes: 10 additions & 12 deletions base/Data/Bitraversable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Require Data.Bifunctor.
Require Data.Either.
Require Data.Functor.
Require Data.Functor.Const.
Require Data.Functor.Identity.
Require Import Data.Functor.Identity.
Require Data.Functor.Utils.
Require GHC.Base.
Require GHC.Prim.
Expand Down Expand Up @@ -384,21 +384,19 @@ Program Instance Bitraversable__Const
#[global] Definition bimapDefault {t : Type -> Type -> Type} {a : Type} {b
: Type} {c : Type} {d : Type} `{Bitraversable t}
: (a -> b) -> (c -> d) -> t a c -> t b d :=
GHC.Prim.coerce (bitraverse : (a -> Data.Functor.Identity.Identity b) ->
(c -> Data.Functor.Identity.Identity d) ->
t a c -> Data.Functor.Identity.Identity (t b d)).
GHC.Prim.coerce (bitraverse : (a -> Identity b) ->
(c -> Identity d) -> t a c -> Identity (t b d)).

(* Skipping definition `Data.Bitraversable.bifoldMapDefault' *)

(* External variables:
Type op_zt__ pair Data.Bifoldable.Bifoldable Data.Bifunctor.Bifunctor
Identity Type op_zt__ pair Data.Bifoldable.Bifoldable Data.Bifunctor.Bifunctor
Data.Either.Either Data.Either.Left Data.Either.Right Data.Functor.op_zlzdzg__
Data.Functor.Const.Const Data.Functor.Const.Mk_Const
Data.Functor.Identity.Identity Data.Functor.Utils.Mk_StateL
Data.Functor.Utils.Mk_StateR Data.Functor.Utils.runStateL
Data.Functor.Utils.runStateR GHC.Base.Applicative GHC.Base.flip GHC.Base.id
GHC.Base.liftA2 GHC.Base.op_z2218U__ GHC.Prim.coerce GHC.Tuple.pair2
GHC.Tuple.pair3 GHC.Tuple.pair4 GHC.Tuple.pair5 GHC.Tuple.pair6 GHC.Tuple.pair7
GHC.Tuple.pair_type GHC.Tuple.quad_type GHC.Tuple.quint_type GHC.Tuple.sept_type
GHC.Tuple.sext_type GHC.Tuple.triple_type
Data.Functor.Utils.Mk_StateL Data.Functor.Utils.Mk_StateR
Data.Functor.Utils.runStateL Data.Functor.Utils.runStateR GHC.Base.Applicative
GHC.Base.flip GHC.Base.id GHC.Base.liftA2 GHC.Base.op_z2218U__ GHC.Prim.coerce
GHC.Tuple.pair2 GHC.Tuple.pair3 GHC.Tuple.pair4 GHC.Tuple.pair5 GHC.Tuple.pair6
GHC.Tuple.pair7 GHC.Tuple.pair_type GHC.Tuple.quad_type GHC.Tuple.quint_type
GHC.Tuple.sept_type GHC.Tuple.sext_type GHC.Tuple.triple_type
*)
102 changes: 95 additions & 7 deletions base/Data/Either.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,91 @@ Arguments Right {_} {_} _.

(* Converted value declarations: *)

#[local] Definition Eq___Either_op_zeze__ {inst_a : Type} {inst_b : Type}
`{GHC.Base.Eq_ inst_a} `{GHC.Base.Eq_ inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> bool :=
fun arg_0__ arg_1__ =>
match arg_0__, arg_1__ with
| Left a1, Left b1 => ((a1 GHC.Base.== b1))
| Right a1, Right b1 => ((a1 GHC.Base.== b1))
| _, _ => false
end.

#[local] Definition Eq___Either_op_zsze__ {inst_a : Type} {inst_b : Type}
`{GHC.Base.Eq_ inst_a} `{GHC.Base.Eq_ inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> bool :=
fun x y => negb (Eq___Either_op_zeze__ x y).

#[global]
Program Instance Eq___Either {a : Type} {b : Type} `{GHC.Base.Eq_ a}
`{GHC.Base.Eq_ b}
: GHC.Base.Eq_ (Either a b) :=
fun _ k__ =>
k__ {| GHC.Base.op_zeze____ := Eq___Either_op_zeze__ ;
GHC.Base.op_zsze____ := Eq___Either_op_zsze__ |}.

#[local] Definition Ord__Either_op_zl__ {inst_a : Type} {inst_b : Type}
`{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> bool :=
fun a b =>
match a with
| Left a1 => match b with | Left b1 => (a1 GHC.Base.< b1) | _ => true end
| Right a1 => match b with | Right b1 => (a1 GHC.Base.< b1) | _ => false end
end.

#[local] Definition Ord__Either_op_zlze__ {inst_a : Type} {inst_b : Type}
`{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> bool :=
fun a b => negb (Ord__Either_op_zl__ b a).

#[local] Definition Ord__Either_op_zg__ {inst_a : Type} {inst_b : Type}
`{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> bool :=
fun a b => Ord__Either_op_zl__ b a.

#[local] Definition Ord__Either_op_zgze__ {inst_a : Type} {inst_b : Type}
`{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> bool :=
fun a b => negb (Ord__Either_op_zl__ a b).

#[local] Definition Ord__Either_compare {inst_a : Type} {inst_b : Type}
`{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> comparison :=
fun a b =>
match a with
| Left a1 => match b with | Left b1 => (GHC.Base.compare a1 b1) | _ => Lt end
| Right a1 => match b with | Right b1 => (GHC.Base.compare a1 b1) | _ => Gt end
end.

#[local] Definition Ord__Either_max {inst_a : Type} {inst_b : Type}
`{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> Either inst_a inst_b :=
fun x y => if Ord__Either_op_zlze__ x y : bool then y else x.

#[local] Definition Ord__Either_min {inst_a : Type} {inst_b : Type}
`{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
: Either inst_a inst_b -> Either inst_a inst_b -> Either inst_a inst_b :=
fun x y => if Ord__Either_op_zlze__ x y : bool then x else y.

#[global]
Program Instance Ord__Either {a : Type} {b : Type} `{GHC.Base.Ord a}
`{GHC.Base.Ord b}
: GHC.Base.Ord (Either a b) :=
fun _ k__ =>
k__ {| GHC.Base.op_zl____ := Ord__Either_op_zl__ ;
GHC.Base.op_zlze____ := Ord__Either_op_zlze__ ;
GHC.Base.op_zg____ := Ord__Either_op_zg__ ;
GHC.Base.op_zgze____ := Ord__Either_op_zgze__ ;
GHC.Base.compare__ := Ord__Either_compare ;
GHC.Base.max__ := Ord__Either_max ;
GHC.Base.min__ := Ord__Either_min |}.

(* Skipping all instances of class `GHC.Read.Read', including
`Data.Either.Read__Either' *)

(* Skipping all instances of class `GHC.Show.Show', including
`Data.Either.Show__Either' *)

#[local] Definition Functor__Either_fmap {inst_a : Type}
: forall {a : Type},
forall {b : Type}, (a -> b) -> Either inst_a a -> Either inst_a b :=
Expand Down Expand Up @@ -199,11 +284,14 @@ Program Instance Monad__Either {e : Type} : GHC.Base.Monad (Either e) :=
end.

(* External variables:
Type bool cons false list nil op_zt__ pair true Coq.Lists.List.flat_map
GHC.Base.Applicative GHC.Base.Functor GHC.Base.Monad GHC.Base.Semigroup
GHC.Base.const GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr GHC.Base.id
GHC.Base.liftA2__ GHC.Base.op_z2218U__ GHC.Base.op_zgzg____
GHC.Base.op_zgzgze____ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____ GHC.Base.op_ztzg____
GHC.Base.pure GHC.Base.pure__ GHC.Base.return___
Gt Lt Type bool comparison cons false list negb nil op_zt__ pair true
Coq.Lists.List.flat_map GHC.Base.Applicative GHC.Base.Eq_ GHC.Base.Functor
GHC.Base.Monad GHC.Base.Ord GHC.Base.Semigroup GHC.Base.compare
GHC.Base.compare__ GHC.Base.const GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr
GHC.Base.id GHC.Base.liftA2__ GHC.Base.max__ GHC.Base.min__ GHC.Base.op_z2218U__
GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg____ GHC.Base.op_zgze____
GHC.Base.op_zgzg____ GHC.Base.op_zgzgze____ GHC.Base.op_zl__ GHC.Base.op_zl____
GHC.Base.op_zlzd__ GHC.Base.op_zlzd____ GHC.Base.op_zlze____
GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____ GHC.Base.op_zsze____
GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__ GHC.Base.return___
*)
Loading

0 comments on commit a1bcedc

Please sign in to comment.