Skip to content

Commit

Permalink
functorial interface wip
Browse files Browse the repository at this point in the history
  • Loading branch information
jtcoolen committed Nov 3, 2024
1 parent d3bd187 commit 1dd0787
Show file tree
Hide file tree
Showing 2 changed files with 272 additions and 2 deletions.
154 changes: 152 additions & 2 deletions src/pari.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,9 @@ type 'kind ty = gen

let t = gen

let register_gc v =
Gc.finalise_last (fun () -> pari_free Ctypes.(coerce gen (ptr void) v)) v

type group = Group
type ring = Ring
type field = Field
Expand All @@ -19,8 +22,155 @@ type number_field = Number_field
type 'a elliptic_curve = Elliptic_curve of 'a
type 'a matrix = private Matrix of 'a

let register_gc v =
Gc.finalise_last (fun () -> pari_free Ctypes.(coerce gen (ptr void) v)) v
module F = struct
module type PARI_t = sig
type t
type k

external of_gen : k ty -> t = "%identity"
external to_gen : t -> k ty = "%identity"
end

module type Ring = sig
type t

val add : t -> t -> t
val mul : t -> t -> t
end

module Natural = struct
type t
end

module type Multiplicative = sig
type t

val mul : t -> t -> t
end

module type Unital = sig
type t

include Multiplicative with type t := t

val one : t
val pow : t -> Natural.t -> t
end

module type Division = sig
type t

include Unital with type t := t

val reciprocal : t -> t
val divide : t -> t -> t
end

module type Domain = sig
type t

include Ring with type t := t

val divides : t -> t -> bool
end

module type IntegralDomain = sig
type t

include Domain with type t := t

val divides : t -> t -> bool
end

module type GCDDomain = sig
type t

include IntegralDomain with type t := t

val gcd : t -> t -> t
val lcm : t -> t -> t
end

module type UFD = sig
type t

include IntegralDomain with type t := t

val factor : t -> (t * int) array
end

module type PID = sig
type t

include UFD with type t := t

val egcd : t -> t -> t * t * t
end

module type EuclideanDomain = sig
type t

include PID with type t := t

val ediv : t -> t -> t * t
val quot : t -> t -> t
val rem : t -> t -> t
val chinese : (t * t) array -> t * t
end

module type Field = sig
type t

include EuclideanDomain with type t := t
include Division with type t := t
end

module type Poly = sig
include PARI_t
include Ring with type t := t
module BaseRing : Ring

val create : BaseRing.t array -> t
end

module Polynomial (R : sig
include PARI_t
include Ring with type t := t
end) : Poly with type k = R.k polynomial = struct
type t = gen
type k = R.k polynomial

external of_gen : k ty -> t = "%identity"
external to_gen : t -> k ty = "%identity"

module BaseRing = R

let add = gadd
let mul = gmul

let create (p : R.t array) : t =
let len = Array.length p in
let size = Signed.Long.of_int (Int.add len 2) in
let p' = cgetg size (Signed.Long.of_int 10 (* t_POL *)) in
let p'' = Ctypes.(coerce gen (ptr gen) p') in
(* TODO: support 32-bit arch *)
let typ = gentostr (type0 @@ R.to_gen p.(0)) in
let v =
if typ = "\"t_POL\"" then Signed.Long.(succ (gvar @@ R.to_gen p.(0)))
else Signed.Long.zero
in
Ctypes.(p' +@ 1 <-@ Signed.Long.(shift_left v Stdlib.(64 - 2 - 16)));
for i = 0 to len - 1 do
Ctypes.(p'' +@ (i + 2) <-@ R.to_gen p.(len - 1 - i))
done;
let p = normalizepol_lg p' size in
register_gc @@ to_gen p;
p
end

type ('t, 'coeff) poly =
(module Poly with type k = 'coeff polynomial and type t = 't)
end

let gentostr = gentostr_raw
let gentobytes x = gentostr x |> String.to_bytes
Expand Down
120 changes: 120 additions & 0 deletions src/pari.mli
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,126 @@ type 'a elliptic_curve = private Elliptic_curve of 'a

val factor : 'a ty -> ('a ty * int) array

module F : sig
module type PARI_t = sig
type t
type k

external of_gen : k ty -> t = "%identity"
external to_gen : t -> k ty = "%identity"
end

module type Ring = sig
type t

val add : t -> t -> t
val mul : t -> t -> t
end

module Natural : sig
type t
end

module type Multiplicative = sig
type t

val mul : t -> t -> t
end

module type Unital = sig
type t

include Multiplicative with type t := t

val one : t
val pow : t -> Natural.t -> t
end

module type Division = sig
type t

include Unital with type t := t

val reciprocal : t -> t
val divide : t -> t -> t
end

module type Domain = sig
type t

include Ring with type t := t

val divides : t -> t -> bool
end

module type IntegralDomain = sig
type t

include Domain with type t := t

val divides : t -> t -> bool
end

module type GCDDomain = sig
type t

include IntegralDomain with type t := t

val gcd : t -> t -> t
val lcm : t -> t -> t
end

module type UFD = sig
type t

include IntegralDomain with type t := t

val factor : t -> (t * int) array
end

module type PID = sig
type t

include UFD with type t := t

val egcd : t -> t -> t * t * t
end

module type EuclideanDomain = sig
type t

include PID with type t := t

val ediv : t -> t -> t * t
val quot : t -> t -> t
val rem : t -> t -> t
val chinese : (t * t) array -> (t * t)
end

module type Field = sig
type t

include EuclideanDomain with type t := t
include Division with type t := t
end

module type Poly = sig
include PARI_t
include Ring with type t := t
module BaseRing : Ring

val create : BaseRing.t array -> t
end

module Polynomial (R : sig
include PARI_t
include Ring with type t := t
end) : Poly with type k = R.k polynomial

type ('t, 'coeff) poly =
(module Poly with type k = 'coeff polynomial and type t = 't)
end

module rec Complex : sig
type t = complex ty

Expand Down

0 comments on commit 1dd0787

Please sign in to comment.