Merge with main #211

base/coq/Free.v

@@ -1,6 +1,7 @@
 From Base Require Export Free.Class.
 From Base Require Export Free.ForFree.
 From Base Require Export Free.Induction.
+From Base Require Export Free.Instance.Identity.
 From Base Require Export Free.Malias.
 From Base Require Export Free.Monad.
 From Base Require Export Free.Tactic.ProveInd.

base/coq/Free/Class/Normalform.v

@@ -5,32 +5,37 @@
 
 From Base Require Import Free.Monad.
 
+From Base Require Import Free.Instance.Identity.
+
 Class Normalform (Shape : Type) (Pos : Shape -> Type)
-                 (A B : Type) :=
+                 (A : Type) :=
   {
+    (** The normalized return type. *)
+    nType : Type;
     (** The function is split into two parts due to termination check errors
         for recursive data types. *)
-    nf' : A -> Free Shape Pos B
+    nf' : A -> Free Shape Pos nType
   }.
 
-Definition nf {Shape : Type} {Pos : Shape -> Type} {A B : Type}
-                  `{Normalform Shape Pos A B} (n : Free Shape Pos A)
- : Free Shape Pos B
+(* Normalizes a Free value. *)
+Definition nf {Shape : Type} {Pos : Shape -> Type} {A : Type}
+                  `{Normalform Shape Pos A} (n : Free Shape Pos A)
+ : Free Shape Pos nType
 := n >>= nf'.
 
-Lemma nfImpure {Shape : Type} {Pos : Shape -> Type} {A B : Type}
-                     `{Normalform Shape Pos A B}
+Lemma nfImpure {Shape : Type} {Pos : Shape -> Type} {A : Type}
+                     `{Normalform Shape Pos A}
   : forall s (pf : _ -> Free Shape Pos A),
   nf (impure s pf) = impure s (fun p => nf (pf p)).
 Proof. trivial. Qed.
 
-Lemma nfPure {Shape : Type} {Pos : Shape -> Type} {A B : Type}
-                     `{Normalform Shape Pos A B} : forall (x : A),
+Lemma nfPure {Shape : Type} {Pos : Shape -> Type} {A : Type}
+                     `{Normalform Shape Pos A} : forall (x : A),
   nf (pure x) = nf' x.
 Proof. trivial. Qed.
 
 (* Normalform instance for functions.
    Effects inside of functions are not pulled to the root. *)
 Instance NormalformFunc (Shape : Type) (Pos : Shape -> Type) (A B : Type)
- : Normalform Shape Pos (A -> B) (A -> B) :=
+ : Normalform Shape Pos (A -> B) :=
   { nf' := pure }.

base/coq/Free/Handlers.v

@@ -18,9 +18,9 @@ Require Import Coq.Lists.List.
 Section NoEffect.
 
   (* Identity handler *)
-  Definition handleNoEffect {A B : Type}
-                            `{Normalform _ _ A B}
-                            (p : Free Identity.Shape Identity.Pos A) : B
+  Definition handleNoEffect {A : Type}
+                            `{Normalform _ _ A}
+                            (p : Free Identity.Shape Identity.Pos A)
   :=  run (nf p).
 
 End NoEffect.
@@ -32,50 +32,50 @@ Section OneEffect.
   Definition SMId := Comb.Shape Maybe.Shape Identity.Shape.
   Definition PMId := Comb.Pos Maybe.Pos Identity.Pos.
 
-  Definition handleMaybe {A B : Type}
-                         `{Normalform SMId PMId A B}
+  Definition handleMaybe {A : Type}
+                         `{Normalform SMId PMId A}
                          (p : Free SMId PMId A)
-   : option B := run (runMaybe (nf p)).
+   : option nType := run (runMaybe (nf p)).
 
   (* Error :+: Identity handler *)
 
   Definition SErrId := Comb.Shape (Error.Shape string) Identity.Shape.
   Definition PErrId := Comb.Pos (@Error.Pos string) Identity.Pos.
 
-  Definition handleError {A B : Type}
-  `{Normalform SErrId PErrId A B}
-  (p : Free SErrId PErrId A) : (B + string)
+  Definition handleError {A : Type}
+  `{Normalform SErrId PErrId A}
+  (p : Free SErrId PErrId A) : (nType + string)
   := run (runError (nf p)).
 
 
   (* ND :+: Identity handler *)
   Definition SNDId := Comb.Shape ND.Shape Identity.Shape.
   Definition PNDId := Comb.Pos ND.Pos Identity.Pos.
 
-  Definition handleND {A B : Type}
-    `{Normalform SNDId PNDId A B}
-    (p : Free SNDId PNDId A) : list B
+  Definition handleND {A : Type}
+    `{Normalform SNDId PNDId A}
+    (p : Free SNDId PNDId A) : list nType
   := collectVals (run (runChoice (nf p))).
 
   (* Trace :+: Identity handler *)
 
   Definition STrcId := Comb.Shape Trace.Shape Identity.Shape.
   Definition PTrcId := Comb.Pos Trace.Pos Identity.Pos.
 
-  Definition handleTrace {A B : Type}
-                        `{Normalform STrcId PTrcId A B}
+  Definition handleTrace {A : Type}
+                        `{Normalform STrcId PTrcId A}
                          (p : Free STrcId PTrcId A)
-    : (B * list string) :=
+    : (nType * list string) :=
     collectMessages (run (runTracing (nf p))).
 
   (* Share :+: Identity handler *)
 
   Definition SShrId := Comb.Shape Share.Shape Identity.Shape.
   Definition PShrId := Comb.Pos Share.Pos Identity.Pos.
 
-  Definition handleShare {A B : Type}
-                         `{Normalform SShrId PShrId A B}
-                         (p : Free SShrId PShrId A) : B :=
+  Definition handleShare {A : Type}
+                         `{Normalform SShrId PShrId A}
+                         (p : Free SShrId PShrId A) : nType :=
    run (runEmptySharing (0,0) (nf p)).
 
 End OneEffect.
@@ -92,9 +92,9 @@ Section TwoEffects.
   Definition PShrND := Comb.Pos Share.Pos (Comb.Pos ND.Pos Identity.Pos).
 
 
-  Definition handleShareND {A B : Type}
-                           `{Normalform SShrND PShrND A B}
-                           (p : Free SShrND PShrND A) : (list B)
+  Definition handleShareND {A : Type}
+                           `{Normalform SShrND PShrND A}
+                           (p : Free SShrND PShrND A) : (list nType)
   := collectVals (run (runChoice (runNDSharing (0,0) (nf p)))).
 
   (* Share :+: Trace :+: Identity handler *)
@@ -103,31 +103,31 @@ Section TwoEffects.
   Definition PShrTrc := Comb.Pos Share.Pos (Comb.Pos Trace.Pos Identity.Pos).
 
 
-  Definition handleShareTrace {A B : Type}
-                              `{Normalform SShrTrc PShrTrc A B}
+  Definition handleShareTrace {A : Type}
+                              `{Normalform SShrTrc PShrTrc A}
                               (p : Free SShrTrc PShrTrc A)
-    : (B * list string) :=
+    : (nType * list string) :=
     collectMessages (run (runTracing (runTraceSharing (0,0) (nf p)))).
 
   (* Share :+: Maybe :+: Identity handler *)
 
   Definition SShrMaybe := Comb.Shape Share.Shape (Comb.Shape Maybe.Shape Identity.Shape).
   Definition PShrMaybe := Comb.Pos Share.Pos (Comb.Pos Maybe.Pos Identity.Pos).
 
-  Definition handleShareMaybe {A B : Type}
-                              `{Normalform SShrMaybe PShrMaybe A B}
-                              (p : Free SShrMaybe PShrMaybe A) : option B :=
+  Definition handleShareMaybe {A : Type}
+                              `{Normalform SShrMaybe PShrMaybe A}
+                              (p : Free SShrMaybe PShrMaybe A) : option nType :=
     run (runMaybe (runEmptySharing (0,0) (nf p))).
 
   (* ND :+: Maybe :+: Identity handler *)
 
   Definition SNDMaybe := Comb.Shape ND.Shape (Comb.Shape Maybe.Shape Identity.Shape).
   Definition PNDMaybe := Comb.Pos ND.Pos (Comb.Pos Maybe.Pos Identity.Pos).
 
-  Definition handleNDMaybe {A B : Type}
-                           `{Normalform SNDMaybe PNDMaybe A B}
+  Definition handleNDMaybe {A : Type}
+                           `{Normalform SNDMaybe PNDMaybe A}
                            (p : Free SNDMaybe PNDMaybe A)
-    : option (list B) := match run (runMaybe (runChoice (nf p))) with
+    : option (list nType) := match run (runMaybe (runChoice (nf p))) with
                          | None => None
                          | Some t => Some (collectVals t)
                          end.
@@ -137,20 +137,20 @@ Section TwoEffects.
   Definition SMaybeTrc := Comb.Shape Maybe.Shape (Comb.Shape Trace.Shape Identity.Shape).
   Definition PMaybeTrc := Comb.Pos Maybe.Pos (Comb.Pos Trace.Pos Identity.Pos).
 
-  Definition handleMaybeTrace {A B : Type}
-                            `{Normalform SMaybeTrc PMaybeTrc A B}
+  Definition handleMaybeTrace {A : Type}
+                            `{Normalform SMaybeTrc PMaybeTrc A}
                             (p : Free SMaybeTrc PMaybeTrc A)
-    : option B * list string :=
+    : option nType * list string :=
     collectMessages (run (runTracing (runMaybe (nf p)))).
 
   (* Share :+: Error :+: Identity handler *)
 
   Definition SShrErr := Comb.Shape Share.Shape (Comb.Shape (Error.Shape string) Identity.Shape).
   Definition PShrErr := Comb.Pos Share.Pos (Comb.Pos (@Error.Pos string) Identity.Pos).
 
-  Definition handleShareError {A B : Type}
-                              `{Normalform SShrErr PShrErr A B}
-                              (p : Free SShrErr PShrErr A) : (B + string)
+  Definition handleShareError {A : Type}
+                              `{Normalform SShrErr PShrErr A}
+                              (p : Free SShrErr PShrErr A) : (nType + string)
   := run (runError (runEmptySharing (0,0) (nf p))).
 
 
@@ -159,9 +159,9 @@ Section TwoEffects.
   Definition SNDErr := Comb.Shape ND.Shape (Comb.Shape (Error.Shape string) Identity.Shape).
   Definition PNDErr := Comb.Pos ND.Pos (Comb.Pos (@Error.Pos string)  Identity.Pos).
 
-  Definition handleNDError {A B : Type}
-                           `{Normalform SNDErr PNDErr A B}
-                           (p : Free SNDErr PNDErr A) : list B + string
+  Definition handleNDError {A : Type}
+                           `{Normalform SNDErr PNDErr A}
+                           (p : Free SNDErr PNDErr A) : list nType + string
   := match run (runError (runChoice (nf p))) with
      | inl t => inl (collectVals t)
      | inr e => inr e
@@ -175,23 +175,23 @@ Section TwoEffects.
   Definition SErrorTrc := Comb.Shape (Error.Shape string) (Comb.Shape Trace.Shape Identity.Shape).
   Definition PErrorTrc := Comb.Pos (@Error.Pos string) (Comb.Pos Trace.Pos Identity.Pos).
 
-  Definition handleErrorTrc {A B : Type}
-                            `{Normalform SErrorTrc PErrorTrc A B}
+  Definition handleErrorTrc {A : Type}
+                            `{Normalform SErrorTrc PErrorTrc A}
                              (p : Free SErrorTrc PErrorTrc A)
-   : (B + string) * list string
+   : (nType + string) * list string
   := collectMessages (run (runTracing (runError (nf p)))).
 
   (* Trace :+: ND :+: Identity handler *)
 
   Definition STrcND := Comb.Shape Trace.Shape (Comb.Shape ND.Shape Identity.Shape).
   Definition PTrcND := Comb.Pos Trace.Pos (Comb.Pos ND.Pos Identity.Pos).
 
-  Definition handleTraceND {A B : Type}
-                           `{Normalform STrcND PTrcND A B}
+  Definition handleTraceND {A : Type}
+                           `{Normalform STrcND PTrcND A}
                            (p : Free STrcND PTrcND A)
-    : list (B * list string) :=
-    map (@collectMessages B)
-                    (@collectVals (B * list (option Sharing.ID * string))
+    : list (nType * list string) :=
+    map (@collectMessages nType)
+                    (@collectVals (nType * list (option Sharing.ID * string))
                                   (run (runChoice (runTracing (nf p))))).
 
 End TwoEffects.
@@ -214,13 +214,13 @@ Section ThreeEffects.
       (Comb.Pos ND.Pos
         (Comb.Pos Maybe.Pos Identity.Pos)).
 
-  Definition handleShareNDMaybe {A B : Type}
-                                `{Normalform SShrNDMaybe PShrNDMaybe A B}
+  Definition handleShareNDMaybe {A : Type}
+                                `{Normalform SShrNDMaybe PShrNDMaybe A}
                                 (p : Free SShrNDMaybe PShrNDMaybe A)
-    : option (list B) :=
+    : option (list nType) :=
     match (run (runMaybe (runChoice (runNDSharing (0,0) (nf p))))) with
     | None   => None
-    | Some t => Some (@collectVals B t)
+    | Some t => Some (@collectVals nType t)
     end.
 
   (* Maybe :+: Share :+: Trace :+: Identity handler *)
@@ -235,10 +235,10 @@ Section ThreeEffects.
       (Comb.Pos Share.Pos
         (Comb.Pos Trace.Pos Identity.Pos)).
 
-  Definition handleMaybeShareTrace {A B : Type}
-                                   `{Normalform SMaybeShrTrc PMaybeShrTrc A B}
+  Definition handleMaybeShareTrace {A : Type}
+                                   `{Normalform SMaybeShrTrc PMaybeShrTrc A}
                                    (p : Free SMaybeShrTrc PMaybeShrTrc A)
-    : option B * list string :=
+    : option nType * list string :=
     collectMessages (run (runTracing (runTraceSharing (0,0) (runMaybe (nf p))))).
 
 
@@ -254,10 +254,10 @@ Section ThreeEffects.
       (Comb.Pos Maybe.Pos
         (Comb.Pos Trace.Pos Identity.Pos)).
 
-  Definition handleNDMaybeTrc {A B : Type}
-                               `{Normalform SNDMaybeTrc PNDMaybeTrc A B}
+  Definition handleNDMaybeTrc {A : Type}
+                               `{Normalform SNDMaybeTrc PNDMaybeTrc A}
                                (p : Free SNDMaybeTrc PNDMaybeTrc A)
-    : (option (list B) * list string) :=
+    : (option (list nType) * list string) :=
     let (val,log) := (collectMessages (run (runTracing (runMaybe (runChoice (nf p))))))
     in match val with
        | None => (None, log)
@@ -277,10 +277,10 @@ Section ThreeEffects.
       (Comb.Pos ND.Pos
         (Comb.Pos (@Error.Pos string) Identity.Pos)).
 
-  Definition handleShareNDError {A B : Type}
-                                  `{Normalform SShrNDErr PShrNDErr A B}
+  Definition handleShareNDError {A : Type}
+                                  `{Normalform SShrNDErr PShrNDErr A}
                                   (p : Free SShrNDErr PShrNDErr A)
-   : list B + string
+   : list nType + string
   := match run (runError (runChoice (runNDSharing (0,0) (nf p)))) with
      | inl t => inl (collectVals t)
      | inr e => inr e
@@ -298,10 +298,10 @@ Section ThreeEffects.
       (Comb.Pos Share.Pos
         (Comb.Pos Trace.Pos Identity.Pos)).
 
-  Definition handleErrorShareTrace {A B : Type}
-                                   `{Normalform SErrShrTrc PErrShrTrc A B}
+  Definition handleErrorShareTrace {A : Type}
+                                   `{Normalform SErrShrTrc PErrShrTrc A}
                                    (p : Free SErrShrTrc PErrShrTrc A)
-   : (B + string) * list string
+   : (nType + string) * list string
   := collectMessages (run (runTracing (runTraceSharing (0,0) (runError (nf p))))).
 
   (* ND :+: Error :+: Trace :+: Identity handler *)
@@ -316,10 +316,10 @@ Section ThreeEffects.
       (Comb.Pos (@Error.Pos string)
         (Comb.Pos Trace.Pos Identity.Pos)).
 
-  Definition handleNDErrorTrace {A B : Type}
-                                `{Normalform SNDErrTrc PNDErrTrc A B}
+  Definition handleNDErrorTrace {A : Type}
+                                `{Normalform SNDErrTrc PNDErrTrc A}
                                 (p : Free SNDErrTrc PNDErrTrc A)
-   : (list B + string) * list string
+   : (list nType + string) * list string
   := match collectMessages (run (runTracing (runError (runChoice (nf p))))) with
      | (inl t, log) => (inl (collectVals t), log)
      | (inr e, log) => (inr e, log)

base/coq/Free/Instance/Identity.v

@@ -1,7 +1,7 @@
 (** * Definition of the identity monad in terms of the free monad. *)
 
-From Base Require Import Free.
-From Base Require Import Free.Instance.Comb.
+From Base Require Import Free.Class.Injectable.
+From Base Require Import Free.Monad.
 From Base Require Import Free.Util.Void.
 
 Module Identity.

base/coq/Prelude/Bool.v

@@ -40,7 +40,7 @@ End SecBool.
 (* Normalform instance for Bool *)
 
 Instance NormalformBool (Shape : Type) (Pos : Shape -> Type)
-  : Normalform Shape Pos (Bool Shape Pos) (Bool Identity.Shape Identity.Pos)
+  : Normalform Shape Pos (Bool Shape Pos)
   := { nf' := pure }.
 
 (* ShareableArgs instance for Bool *)

base/coq/Prelude/Integer.v

@@ -99,7 +99,7 @@ End SecInteger.
 (* Normalform instance for Integer *)
 
 Instance NormalformInteger (Shape : Type) (Pos : Shape -> Type)
-  : Normalform Shape Pos (Integer Shape Pos) (Integer Identity.Shape Identity.Pos)
+  : Normalform Shape Pos (Integer Shape Pos)
   := { nf' := pure }.
 
 (* ShareableArgs instance for Integer *)