Add ErrorT monad, and Show class

4 files changed, 116 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 45fa23cb1..271f7585f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6450,6 +6450,7 @@ src/Util/Curry.v
 src/Util/Decidable.v
 src/Util/DefaultedTypes.v
 src/Util/Equality.v
+src/Util/ErrorT.v
 src/Util/Factorize.v
 src/Util/FixCoqMistakes.v
 src/Util/FixedWordSizes.v
@@ -6516,6 +6517,7 @@ src/Util/Strings/Decimal.v
 src/Util/Strings/Equality.v
 src/Util/Strings/HexString.v
 src/Util/Strings/OctalString.v
+src/Util/Strings/Show.v
 src/Util/Strings/String.v
 src/Util/Tactics/BreakMatch.v
 src/Util/Tactics/CacheTerm.v
@@ -6563,6 +6565,7 @@ src/Util/Tactics/VM.v
 src/Util/ZRange/BasicLemmas.v
 src/Util/ZRange/CornersMonotoneBounds.v
 src/Util/ZRange/Operations.v
+src/Util/ZRange/Show.v
 src/Util/ZUtil/AddGetCarry.v
 src/Util/ZUtil/AddModulo.v
 src/Util/ZUtil/CC.v
diff --git a/src/Util/ErrorT.v b/src/Util/ErrorT.v
new file mode 100644
index 000000000..ab8634e2c
--- /dev/null
+++ b/src/Util/ErrorT.v
@@ -0,0 +1,23 @@
+Require Import Crypto.Util.Notations.
+
+Inductive ErrorT {ErrT T} :=
+| Success (v : T)
+| Error (msg : ErrT).
+
+Global Arguments ErrorT : clear implicits.
+Delimit Scope error_scope with error.
+Bind Scope error_scope with ErrorT.
+
+Definition invert_result {ErrT T} (v : ErrorT ErrT T)
+  := match v return match v with Success _ => T | _ => ErrT end with
+     | Success v => v
+     | Error msg => msg
+     end.
+
+Definition bind {A B ErrT} (x : ErrorT ErrT A) (k : A -> ErrorT ErrT B) : ErrorT ErrT B
+  := match x with
+     | Success v => k v
+     | Error msg => Error msg
+     end.
+
+Notation "x <- y ; f" := (bind y (fun x => f%error)) : error_scope.
diff --git a/src/Util/Strings/Show.v b/src/Util/Strings/Show.v
new file mode 100644
index 000000000..6b5f785a8
--- /dev/null
+++ b/src/Util/Strings/Show.v
@@ -0,0 +1,82 @@
+Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.QArith.QArith_base.
+Require Import Coq.Strings.String Coq.Strings.Ascii.
+Require Crypto.Util.Strings.String.
+Require Import Crypto.Util.Strings.HexString.
+Require Import Crypto.Util.Strings.Decimal.
+Local Open Scope string_scope.
+
+Class Show T := show : bool (* parens *) -> T -> string.
+
+Definition maybe_wrap_parens (parens : bool) (s : string)
+  := if parens then "(" ++ s ++ ")" else s.
+
+Global Instance show_unit : Show unit := fun _ _ => "tt".
+Global Instance show_True : Show True := fun _ _ => "I".
+Global Instance show_False : Show False := fun _ pf => match pf with end.
+Global Instance show_Empty_set : Show Empty_set := fun _ pf => match pf with end.
+Global Instance show_bool : Show bool := fun _ b => if b then "true" else "false".
+Global Instance show_option {T} `{Show T} : Show (option T)
+  := fun p v
+     => match v with
+       | Some v
+         => maybe_wrap_parens
+             p
+             ("Some " ++ show true v)
+       | None => "None"
+       end.
+Global Instance show_list {T} `{Show T} : Show (list T)
+  := fun _ ls => "[" ++ String.concat ", " (List.map (show false) ls) ++ "]".
+Global Instance show_prod {A B} `{Show A, Show B} : Show (A * B)
+  := fun _ '(a, b) => "(" ++ show false a ++ ", " ++ show true b ++ ")".
+Global Instance show_string : Show string := fun _ s => """" ++ s ++ """".
+Global Instance show_ascii : Show ascii := fun _ ch => String "'" (String ch "'").
+
+Module Export Decimal.
+  Global Instance show_positive : Show positive
+    := fun _ p
+       => decimal_string_of_pos p.
+  Global Instance show_N : Show N
+    := fun _ n
+       => match n with
+         | N0 => "0"
+         | Npos p => show false p
+         end.
+  Global Instance show_nat : Show nat
+    := fun _ n => show false (N.of_nat n).
+  Global Instance show_Z : Show Z
+    := fun _ z
+       => match z with
+         | Zneg p => "-" ++ show false p
+         | Z0 => "0"
+         | Zpos p => show false p
+         end.
+  Global Instance show_Q : Show Q
+    := fun parens q
+       => if (Qden q =? 1)%positive
+         then show parens (Qnum q)
+         else maybe_wrap_parens
+                parens
+                (show true (Qnum q) ++ " / " ++ show true (Qden q)).
+End Decimal.
+
+Module Hex.
+  Definition show_positive : Show positive
+    := fun _ p => HexString.of_pos p.
+  Definition show_Z : Show Z
+    := fun _ z => HexString.of_Z z.
+  Definition show_N : Show N
+    := fun _ n
+       => match n with
+         | N0 => "0"
+         | Npos p => show_positive false p
+         end.
+  Definition show_nat : Show nat
+    := fun _ n => show_N false (N.of_nat n).
+  Definition show_Q : Show Q
+    := fun parens q
+       => if (Qden q =? 1)%positive
+         then show_Z parens (Qnum q)
+         else maybe_wrap_parens
+                parens
+                (show_Z true (Qnum q) ++ " / " ++ show_positive true (Qden q)).
+End Hex.
diff --git a/src/Util/ZRange/Show.v b/src/Util/ZRange/Show.v
new file mode 100644
index 000000000..2fac57b16
--- /dev/null
+++ b/src/Util/ZRange/Show.v
@@ -0,0 +1,8 @@
+Require Import Coq.Strings.String.
+Require Import Crypto.Util.Strings.Show.
+Require Import Crypto.Util.ZRange.
+Local Open Scope string_scope.
+
+Global Instance show_zrange : Show zrange
+  := fun _ r
+     => "[" ++ Hex.show_Z false (lower r) ++ " ~> " ++ Hex.show_Z false (upper r) ++ "]".