some more polymorphism.

Author: Gregory Malecha

theories/Programming/Injection.v

@@ -4,12 +4,13 @@ Require Import Coq.Strings.String.
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 
-Class Injection x t := inject : x -> t.
+Polymorphic Class Injection (x : Type) (t : Type) := inject : x -> t.
 (*
 Class Projection x t := { project : t -> x ; pmodify : (x -> x) -> (t -> t) }.
 *)
 
-Instance Injection_refl {T} : Injection T T := { inject := @id T }.
+Polymorphic Instance Injection_refl {T : Type} : Injection T T :=
+{ inject := @id T }.
 
 Instance Injection_ascii_string : Injection ascii string :=
   { inject a := String a EmptyString }.

theories/Programming/Show.v

@@ -13,10 +13,12 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Definition showM : Type :=
-  forall m, Injection ascii m -> Monoid m -> m.
+Set Printing Universes.
 
-Class ShowScheme (T : Type) : Type :=
+Polymorphic Definition showM : Type :=
+  forall m : Type, Injection ascii m -> Monoid m -> m.
+
+Polymorphic Class ShowScheme (T : Type) : Type :=
 { show_mon : Monoid T
 ; show_inj : Injection ascii T
 }.
@@ -31,22 +33,22 @@ Global Instance ShowScheme_string_compose : ShowScheme (string -> string) :=
 ; show_inj := String
 }.
 
-Definition runShow {T} {M : ShowScheme T} (m : showM) : T :=
+Polymorphic Definition runShow {T} {M : ShowScheme T} (m : showM) : T :=
   m _ show_inj show_mon.
 
-Class Show T := show : T -> showM.
+Polymorphic Class Show T := show : T -> showM.
 
-Definition to_string {T} {M : Show T} (v : T) : string :=
+Polymorphic Definition to_string {T} {M : Show T} (v : T) : string :=
   runShow (show v) ""%string.
 
-Definition empty : showM :=
+Polymorphic Definition empty : showM :=
   fun _ _ m => monoid_unit m.
-Definition cat (a b : showM) : showM :=
+Polymorphic Definition cat (a b : showM) : showM :=
   fun _ i m => monoid_plus m (a _ i m) (b _ i m).
-Global Instance Injection_ascii_showM : Injection ascii showM :=
+Global Polymorphic Instance Injection_ascii_showM : Injection ascii showM :=
   fun v => fun _ i _ => i v.
 
-Fixpoint show_exact (s : string) : showM :=
+Polymorphic Fixpoint show_exact (s : string) : showM :=
   match s with
     | EmptyString => empty
     | String a s' => cat (inject a) (show_exact s')
@@ -61,67 +63,20 @@ Module ShowNotation.
   Coercion _inject_char : ascii >-> showM.
 End ShowNotation.
 
-Definition indent (indent : showM) (v : showM) : showM :=
+Polymorphic Definition indent (indent : showM) (v : showM) : showM :=
   let nl := Ascii.ascii_of_nat 10 in
     fun _ inj mon =>
       v _ (fun a => if eq_dec a nl
          then monoid_plus mon (inj a) (indent _ inj mon)
          else inj a) mon.
 
-Section hiding_notation.
+Section sepBy.
   Import ShowNotation.
   Local Open Scope show_scope.
-  Require Import Ascii.
-  Require Import String.
-
-Global Instance unit_Show : Show unit :=
-  { show u := "tt"%string }.
-Global Instance bool_Show : Show bool :=
-  { show b := if b then "true"%string else "false"%string }.
-Global Instance ascii_Show : Show ascii :=
-  fun a =>  "'"%char << a << "'"%char.
-Global Instance string_Show : Show string :=
-  { show s := """"%char << s << """"%char }.
-
-Program Fixpoint nat_show (n:nat) {measure n} : showM :=
-  if Compare_dec.le_gt_dec n 9 then
-    inject (Char.digit2ascii n)
-  else
-    let n' := NPeano.Nat.div n 10 in
-    (@nat_show n' _) << (inject (Char.digit2ascii (n - 10 * n'))).
-Next Obligation.
-  assert (NPeano.Nat.div n 10 < n) ; eauto.
-  eapply NPeano.Nat.div_lt.
-  inversion H; apply Lt.lt_O_Sn.
-  repeat constructor.
-Defined.
-Global Instance nat_Show : Show nat := { show := nat_show }.
-
-Global Instance Show_positive : Show positive :=
-  fun x => nat_show (Pos.to_nat x).
-
-Global Instance Show_Z : Show Z :=
-  fun x =>
-    match x with
-      | Z0 => "0"%char
-      | Zpos p => show p
-      | Zneg p => "-"%char << show p
-    end.
-
-Section pair_Show.
-  Context {A B} {AS:Show A} {BS:Show B}.
-  Global Instance pair_Show : Show (A*B) :=
-    { show p :=
-        let (a,b) := p in
-        "("%char << show a << ","%char << show b << ")"%char
-    }.
-End pair_Show.
-
-Section sepBy.
-  Variable T : Type.
+  Polymorphic Variable T : Type.
   Context {F : Foldable T showM}.
 
-  Definition sepBy (sep : showM) (ls : T) : showM :=
+  Polymorphic Definition sepBy (sep : showM) (ls : T) : showM :=
     match
       fold (fun s acc =>
         match acc with
@@ -135,11 +90,13 @@ Section sepBy.
 End sepBy.
 
 Section sepBy_f.
-  Variable T E : Type.
-  Context {F : Foldable T E}.
-  Variable (f : E -> showM).
+  Import ShowNotation.
+  Local Open Scope show_scope.
+  Polymorphic Variables (T : Type) (E : Type).
+  Polymorphic Context {F : Foldable T E}.
+  Polymorphic Variable (f : E -> showM).
 
-  Definition sepBy_f (sep : showM) (ls : T) : showM :=
+  Polymorphic Definition sepBy_f (sep : showM) (ls : T) : showM :=
     match
       fold (fun s acc =>
         match acc with
@@ -152,12 +109,14 @@ Section sepBy_f.
     end.
 End sepBy_f.
 
-Definition wrap (before after : showM) (x : showM) : showM :=
-  before << x << after.
+Polymorphic Definition wrap (before after : showM) (x : showM) : showM :=
+  cat before (cat x after).
 
 Section sum_Show.
-  Context {A B} {AS:Show A} {BS:Show B}.
-  Global Instance sum_Show : Show (A+B) :=
+  Import ShowNotation.
+  Local Open Scope show_scope.
+  Polymorphic Context {A : Type@{a}} {B : Type@{b}} {AS:Show A} {BS:Show B}.
+  Global Polymorphic Instance sum_Show : Show (A+B) :=
     { show s :=
         let (tag, payload) :=
           match s with
@@ -175,24 +134,73 @@ End sum_Show.
 
 Section foldable_Show.
   Require Import ExtLib.Structures.Reducible.
-  Context {A B} {F : Foldable B A} {BS : Show A}.
+  Polymorphic Context {A:Type} {B:Type} {F : Foldable B A} {BS : Show A}.
 
-  Global Instance foldable_Show : Show B :=
-    { show s := sepBy_f show ", "%string s }.
+  Global Polymorphic  Instance foldable_Show : Show B :=
+    { show s := sepBy_f show (show_exact ", "%string) s }.
 
 End foldable_Show.
 
-End hiding_notation.
-
-Fixpoint iter_show (ss : list showM) : showM :=
+Polymorphic Fixpoint iter_show (ss : list showM) : showM :=
   match ss with
     | nil => empty
     | cons s ss => cat s (iter_show ss)
   end.
 
+Section hiding_notation.
+  Import ShowNotation.
+  Local Open Scope show_scope.
+  Require Import Ascii.
+  Require Import String.
+
+Global Instance unit_Show : Show unit :=
+  { show u := "tt"%string }.
+Global Instance bool_Show : Show bool :=
+  { show b := if b then "true"%string else "false"%string }.
+Global Instance ascii_Show : Show ascii :=
+  fun a =>  "'"%char << a << "'"%char.
+Global Instance string_Show : Show string :=
+  { show s := """"%char << s << """"%char }.
+
+Program Fixpoint nat_show (n:nat) {measure n} : showM :=
+  if Compare_dec.le_gt_dec n 9 then
+    inject (Char.digit2ascii n)
+  else
+    let n' := NPeano.Nat.div n 10 in
+    (@nat_show n' _) << (inject (Char.digit2ascii (n - 10 * n'))).
+Next Obligation.
+  assert (NPeano.Nat.div n 10 < n) ; eauto.
+  eapply NPeano.Nat.div_lt.
+  inversion H; apply Lt.lt_O_Sn.
+  repeat constructor.
+Defined.
+Global Instance nat_Show : Show nat := { show := nat_show }.
+
+Global Instance Show_positive : Show positive :=
+  fun x => nat_show (Pos.to_nat x).
+
+Global Instance Show_Z : Show Z :=
+  fun x =>
+    match x with
+      | Z0 => "0"%char
+      | Zpos p => show p
+      | Zneg p => "-"%char << show p
+    end.
+
+Section pair_Show.
+  Polymorphic Context {A : Type@{a}} {B : Type@{b}} {AS:Show A} {BS:Show B}.
+  Global Polymorphic Instance pair_Show : Show (A*B) :=
+    { show p :=
+        let (a,b) := p in
+        "("%char << show a << ","%char << show b << ")"%char
+    }.
+End pair_Show.
+End hiding_notation.
+
+
 
 (*
 Examples:
 Eval compute in (runShow (show (42,"foo"%string)) : string).
-Eval compute in (runShow (show (inl true : bool+string))
+Eval compute in (runShow (show (inl true : bool+string))).
 *)

theories/Structures/MonadReader.v

@@ -1,31 +1,31 @@
-Require Import Monad.
+Require Import ExtLib.Structures.Monad.
 
 Set Implicit Arguments.
 Set Maximal Implicit Arguments.
 
-Class MonadReader (T : Type) (m : Type -> Type) : Type :=
-{ local : forall {t}, (T -> T) -> m t -> m t
+Polymorphic Class MonadReader (T : Type) (m : Type@{d} -> Type) : Type :=
+{ local : forall {t : Type@{d}}, (T -> T) -> m t -> m t
 ; ask : m T
 }.
 
 Section monadic.
-  Variable m : Type -> Type.
+  Polymorphic Variable m : Type -> Type.
   Context {M : Monad m}.
-  Variable T : Type.
+  Polymorphic Variable T : Type.
   Context {MR : MonadReader T m}.
 
-  Definition asks {U} (f : T -> U) : m U :=
+  Polymorphic Definition asks {U} (f : T -> U) : m U :=
     bind ask (fun x => ret (f x)).
 
 End monadic.
 
 Section SubReader.
-  Variable m : Type -> Type.
+  Polymorphic Variable m : Type -> Type.
   Context {M : Monad m}.
-  Variable T S : Type.
+  Polymorphic Variable T S : Type.
   Context {MR : MonadReader T m}.
 
-  Definition ReaderProd (f : T -> S) (g : S -> T -> T) 
+  Polymorphic Definition ReaderProd (f : T -> S) (g : S -> T -> T)
     : MonadReader S m :=
   {| ask := @asks m M T MR S f
    ; local := fun _T up (c : m _T)  => @local T m MR _ (fun s => g (up (f s)) s) c

theories/Structures/MonadWriter.v

@@ -4,22 +4,23 @@ Require Import ExtLib.Structures.Monoid.
 Set Implicit Arguments.
 Set Maximal Implicit Arguments.
 
-Class MonadWriter (T : Type) (M : Monoid T) (m : Type -> Type) : Type :=
+Polymorphic Class MonadWriter (T : Type@{s}) (M : Monoid T)
+            (m : Type@{d} -> Type) : Type :=
 { tell : T -> m unit
-; listen : forall {A}, m A -> m (A * T)%type
-; pass : forall {A}, m (A * (T -> T))%type -> m A
+; listen : forall {A : Type@{d}}, m A -> m (A * T)%type
+; pass : forall {A : Type@{d}}, m (A * (T -> T))%type -> m A
 }.
 
 Section WriterOps.
-  Context {m : Type -> Type}.
-  Context {S : Type}.
+  Polymorphic Context {m : Type -> Type}.
+  Polymorphic Context {S : Type}.
   Context {Monad_m : Monad m}.
   Variable Monoid_S : Monoid S.
   Context {Writer_m : MonadWriter Monoid_S m}.
 
-  Definition listens {A B} (f : S -> B) (c : m A) : m (A * B) :=
+  Polymorphic Definition listens {A B : Type} (f : S -> B) (c : m A) : m (A * B) :=
     liftM (fun x => (fst x, f (snd x))) (listen c).
 
-  Definition censor {A} (f : S -> S) (c : m A) : m A :=
+  Polymorphic Definition censor {A : Type} (f : S -> S) (c : m A) : m A :=
     pass (liftM (fun x => (x, f)) c).
-End WriterOps.
+End WriterOps.

theories/Structures/Monoid.v

@@ -5,16 +5,16 @@ Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 
 Section Monoid.
-  Variable S : Type.
+  Polymorphic Variable S : Type.
 
-  Record Monoid : Type :=
+  Polymorphic Record Monoid : Type :=
   { monoid_plus : S -> S -> S
   ; monoid_unit : S
   }.
 
   Context {Type_S : type S}.
 
-  Class MonoidLaws (M : Monoid) : Type :=
+  Polymorphic Class MonoidLaws (M : Monoid) : Type :=
   { monoid_assoc :> Associative M.(monoid_plus) equal
   ; monoid_lunit :> LeftUnit M.(monoid_plus) M.(monoid_unit) equal
   ; monoid_runit :> RightUnit M.(monoid_plus) M.(monoid_unit) equal