Commit 8a478f52 authored by SimonHalfon's avatar SimonHalfon

Non empty message

parents
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* Module des entiers relatifs, sans typage explicite. Observez la signature inf\'er\'ee *)
module Z_inf =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
Z_inf.op 3 5 ;;
Z_inf.op Z_inf.neutral 8 = 8 ;;
(* Module des entiers relatifs, type Groupe *)
module Z: Group =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
Z.op 3 5 ;;
Z.neutral = 0 ;;
Z.neutral ;;
(*
Les types non specifies dans la signature sont abstraits, et les valeurs non presentes
dans la signature sont oubliees / rendues privees
*)
module Z_nadine: Group =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
let nadine = 12
end ;;
Z_nadine.nadine ;;
Z_nadine.neutral ;;
(* Module des entiers relatifs, type Groupe avec type visible *)
module Z_vt: Group with type t = int =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
Z_vt.op 3 5 ;;
(* On peut restreindre la signature apr\'es coup *)
module Z2: Group = Z_inf ;;
Z2.neutral ;;
(* Mais une fois un type abstrait ou une valeur rendue priv\'ee, on ne peut plus revenir en arri\`ere: *)
module Z_vt2: Group with type t = int = Z ;;
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* Groupe des permutations de 3 elements *)
module Permutations_3: Group =
struct
type elt = A | B | C
type t = elt -> elt
let neutral x = x
let op s t = fun x -> s(t(x))
let inv s = function
| x when x = s(A) -> A
| x when x = s(B) -> B
| x when x = s(C) -> C
| _ -> failwith "nadine"
end ;;
(* Le type elt n'est pas visible depuis l'exterieur *)
Permutations_3.A ;;
Permutations_3.neutral ;;
(* On ne peut pas rendre le type elt visible depuis l'exterieur:
il n'est pas dans la signature *)
module Permutations_3_vtelt: Group with type elt = int =
struct
type elt = int
type t = elt -> elt
let neutral x = x
let op s t = fun x -> s(t(x))
let inv s = function
| x when x = s(0) -> 0
| x when x = s(1) -> 1
| x when x = s(2) -> 2
| _ -> -1
end ;;
(* On ne peut donc pas non plus rendre le type t visible depuis l'exterieur *)
module Permutations_3_vt: Group with type t = A | B | C -> A | B | C =
struct
type elt = A | B | C
type t = elt -> elt
let neutral x = x
let op s t = fun x -> s(t(x))
let inv s = function
| x when x = s(A) -> A
| x when x = s(B) -> B
| x when x = s(C) -> C
end ;;
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* Foncteurs produit cartesien de groupes *)
module Product (G1: Group) (G2: Group): Group =
struct
type t = G1.t * G2.t
let neutral = (G1.neutral, G2.neutral)
let op (x1, x2) (y1, y2) = (G1.op x1 y1, G2.op x2 y2)
let inv (x,y) = (G1.inv x, G2.inv y)
end ;;
(* Avec type visible *)
module Product_vt (G1: Group) (G2: Group): Group with type t = G1.t * G2.t =
struct
type t = G1.t * G2.t
let neutral = (G1.neutral, G2.neutral)
let op (x1, x2) (y1, y2) = (G1.op x1 y1, G2.op x2 y2)
let inv (x,y) = (G1.inv x, G2.inv y)
end ;;
(* Module des entiers relatifs, type Groupe avec type visible *)
module Z_vt: Group with type t = int =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
(* Module des entiers relatifs, type Groupe *)
module Z: Group = Z_vt ;;
module Z2 = Product (Z) (Z) ;;
module Z_vt2 = Product (Z_vt) (Z_vt) ;;
module Z2_vt = Product_vt (Z) (Z) ;;
module Z_vt2_vt = Product_vt (Z_vt) (Z_vt) ;;
Z2.neutral ;;
Z_vt2.neutral ;;
Z2_vt.neutral ;;
Z_vt2_vt.neutral ;;
Z2.neutral = (Z.neutral, Z.neutral) ;;
Z_vt2.neutral = (Z_vt.neutral, Z_vt.neutral) ;;
Z2_vt.neutral = (Z.neutral, Z.neutral) ;;
Z_vt2_vt.neutral = (Z_vt.neutral, Z_vt.neutral) ;;
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* Module des entiers relatifs, type Groupe avec type visible *)
module Z_vt: Group with type t = int =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
(* Module des entiers relatifs, type Groupe *)
module Z: Group = Z_vt ;;
(* Pas de polymorphisme pour les foncteurs *)
module Id (G: Group): Group = G ;;
module Idd (G: Group) = G ;;
module Iddd (G: Group): Group with type t = G.t = G ;;
module Z1 = Id (Z_vt) ;;
module Z2 = Idd (Z_vt) ;;
module Z3 = Iddd (Z_vt) ;;
module Z4 = Id (Z) ;;
module Z5 = Idd (Z) ;;
module Z6 = Iddd (Z) ;;
Z1.neutral ;; (* Equivalent a module Z1: Group = Z_vt *)
Z2.neutral ;;
Z3.neutral ;; (* Sans surprise *)
Z4.neutral ;; (* Sans surprise *)
Z5.neutral ;; (* OCaml ne reinfere pas le type oublie *)
Z6.neutral ;; (* OCaml ne peut pas des-abstraire le type t *)
Z4.neutral = Z.neutral ;;
Z5.neutral = Z.neutral ;;
Z6.neutral = Z.neutral ;;
(* Groupe des permutations de 3 elements *)
module Permutations_3 =
struct
type elt = A | B | C
type t = elt -> elt
let neutral x = x
let op s t = fun x -> s(t(x))
let inv s = function
| x when x = s(A) -> A
| x when x = s(B) -> B
| x when x = s(C) -> C
end ;;
(* Le type elt est visible depuis l'exterieur *)
Permutations_3.A ;;
(* Mais pour appliquer Idd a Permutations_3, il faut le restreindre au type Group *)
module Perm = Idd (Permutations_3) ;;
(* Donc on perd la visibilite *)
Perm.A ;;
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* Foncteurs produit cartesien de groupes, avec type visible *)
module Product (G1: Group) (G2: Group): Group with type t = G1.t * G2.t =
struct
type t = G1.t * G2.t
let neutral = (G1.neutral, G2.neutral)
let op (x1, x2) (y1, y2) = (G1.op x1 y1, G2.op x2 y2)
let inv (x,y) = (G1.inv x, G2.inv y)
end ;;
(* Groupe de cardinal 1 (le seul et l'unique) *)
module Singleton_Group: Group =
struct
type t = unit
let neutral = ()
let op x y = ()
let inv x = ()
end ;;
(* Fonction pour G^n *)
let rec power g = function
| 0 -> (module Singleton_Group: Group)
| 1 -> g
| n -> let gg = power g (n-1) in
let module GG = (val gg: Group) in
let module G = (val g: Group) in
(module (Product (G) (GG)): Group) ;;
(* Module des entiers relatifs, type visible *)
module Z: Group with type t = int =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
module Z3 = (val (power (module Z) 3)) ;;
Z3.neutral ;;
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* Module des entiers relatifs *)
module Z: Group with type t = int =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
[(module Z: Group with type t = int); (module Z: Group)] ;;
(* Signature d'un Groupe *)
module type Group =
sig
type t
val zero: t
val plus: t -> t -> t
val minus: t -> t
end ;;
(* Signature d'un anneau *)
module type Ring =
sig
include Group
val one: t
val times: t -> t -> t
end ;;
(* Groupe des entiers relatifs *)
module Z_Group: Group =
struct
type t = int
let zero = 0
let plus = (+)
let minus x = -x
end ;;
(* Anneau des entiers relatifs *)
module Z_Ring: Ring (* with type t = Z_Group.t *) =
struct
include Z_Group
let one = 1
let times x y = x*y
end ;;
(* Groupe des entiers relatifs *)
module Z_Group: Group with type t = int =
struct
type t = int
let zero = 0
let plus = (+)
let minus x = -x
end ;;
(* Anneau des entiers relatifs *)
module Z_Ring: Ring =
struct
include Z_Group
let one = 1
let times x y = x*y
end ;;
(* Le type t est a nouveau abstrait *)
Z_Ring.one ;;
Z_Ring.zero ;;
Z_Ring.plus (Z_Ring.zero) (Z_Ring.one) = Z_Ring.one ;;
Z_Ring.zero = Z_Group.zero ;; (* Cf exemple ci dessous *)
(* Anneau des entiers relatifs *)
module Z_Ring: Ring with type t = Z_Group.t =
struct
include Z_Group
let one = 1
let times x y = x*y
end ;;
Z_Ring.zero = Z_Group.zero ;;
Z_Ring.zero ;;
(* Ni Syntaxique Ni Semantique *)
module type Cuisine =
sig
type t
val nadine: t
end ;;
module type Grenadine =
sig
include Cuisine
val nardin: t
end ;;
module Nadine: Cuisine =
struct
type t = int
let nadine = 12
end ;;
module Martine: Grenadine =
struct
include Nadine
let nardin = Nadine.nadine
end ;;
Martine.nadine = Nadine.nadine ;;
(*
module type Int =
sig
val n: int
end ;;
module Permutations (N: Int): Group with type t = int array =
struct
let n = N.n
type t = int array
let neutral = Array.init n (fun i -> i)
let op s t = Array.init n (fun i -> s.(t.(i)))
let inv s = s
end ;;
let to_int m =
let module M = (val m : Int) in
M.n
;;
(* let m = (module Z_Group : Group) in let module M = (val m: Group) in M.neutral ;;
let mm = (module Product (M) (Z_Group): Group) in [mm] ;;
*)
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* Foncteurs produit cartesien de groupes, avec type visible *)
module Product (G1: Group) (G2: Group): Group with type t = G1.t * G2.t =
struct
type t = G1.t * G2.t
let neutral = (G1.neutral, G2.neutral)
let op (x1, x2) (y1, y2) = (G1.op x1 y1, G2.op x2 y2)
let inv (x,y) = (G1.inv x, G2.inv y)
end ;;
(* Groupe de cardinal 1 (le seul et l'unique) *)
module Singleton_Group: Group =
struct
type t = unit
let neutral = ()
let op x y = ()
let inv x = ()
end ;;
module type Int =
sig
val n: int
end ;;
module rec Power: functor (G: Group) (N: Int) -> Group =
functor (G: Group) (N: Int) -> Product (G) (Power (G) (N))
(* and GG: functor (G: Group) (N: Int) -> Group =
functor (G: Group) (N: Int) -> Power (G) (N) ;;
*)
*)
(* Signature d'un Groupe *)
module type Group =
sig
type t
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
module type Nadine =
sig
type x
val haha: x
end ;;
module Z: Group =
struct
type t = int
let neutral = 0
let op = (+)
let inv x = -x
end ;;
module ToRing (G: Group): Nadine with type x = G.t list =
struct
type x = G.t list
let haha = [G.neutral]
end ;;
module T = ToRing (Z) ;;
T.haha ;;
List.hd(T.haha) = Z.neutral ;;
(* Ce que j'aurais voulu, c'est une sorte de polymorphisme de foncteurs *)
module Id (A: sig end) = A
module A =
struct
type nadine = int
let cuisine = 12
end ;;
module B = Id(A) ;;
B.cuisine ;;
(* ============ Tentative 1 ============ *)
module type Group =
sig
type t
module Aux: sig (* val nadine: int *) end
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* ==> Le contenu de Aux ne sera pas visible de l'exterieur *)
module Permutations_3 =
struct
type elt = A | B | C
type t = elt -> elt
module Aux =
struct
(* Disjoint Cycles Decomposition *)
let dcd s =
if s(A) = A then [ [A]; [B]; [C] ] else [ [A;B;C] ]
(* let nadine = 12 *)
end
let neutral x = x
let op s t = fun x -> s(t(x))
let inv s = if Aux.dcd s = [] then s else s
end ;;
Permutations_3.Aux.dcd ;;
module Perm: Group = Permutations_3 ;;
Perm.Aux.dcd ;;
(* Perm.Aux.nadine ;; *)
(* ============ Tentative 2 ============ *)
module type Group =
sig
type t
module type S
module Aux: S
val neutral: t
val op: t -> t -> t
val inv: t -> t
end ;;
(* C'est plus subtil: la signature S est abstraite, comme le type t *)
module Permutations_3 =
struct
type elt = A | B | C
type t = elt -> elt
module type S =
sig
val dcd: t -> elt list list
end
module Aux =
struct
let dcd s =
if s(A) = A then [ [A]; [B]; [C] ] else [ [A;B;C] ]
end
let neutral x = x
let op s t = fun x -> s(t(x))
let inv s = if Aux.dcd s = [] then s else s
end ;;
Permutations_3.Aux.dcd ;;
module type S_out = Permutations_3.S ;;
module Aux_out: S_out = Permutations_3.Aux ;;
Aux_out.dcd ;;
module Perm: Group = Permutations_3 ;;
(* Aux.dcd n'est pas visible *)
Perm.Aux.dcd ;;
(* Pourtant Aux est visible *)
module Aux_out2 = Perm.Aux ;;
(* Mais pas Aux.dcd *)
Aux_out2.dcd ;;
(* La raison: la signature S est visible *)
module type S_out2 = Perm.S ;;
(* Mais elle est abstraite *)
module Auxx: S_out2 =
struct
let dcd s = []
end ;;
(* Abstraite, mais bien coherente avec Aux *)
module Aux_out3: S_out2 = Perm.Aux ;;
module Aux_out4: S_out2 = Permutations_3.Aux ;;
(* ============ Tentative 3 ============ *)
(* INCHANGE *)
module type Group =
sig
type t