Pass around lists of strings for error messages

This allows us to get back an error message in Saturated Solinas in
OCaml on P256 x32 in reasonable time without blowing the stack.

There's the slight oddity that the list of string in the success case is
joined by the empty string, but the list of string in the error case is
joined by newline.  Probably meanas that I chose the wrong abstraction
barrier somewhere.

5 files changed, 87 insertions, 65 deletions

diff --git a/src/Experiments/NewPipeline/CLI.v b/src/Experiments/NewPipeline/CLI.v
index 24e26e4f4..ba240d093 100644
--- a/src/Experiments/NewPipeline/CLI.v
+++ b/src/Experiments/NewPipeline/CLI.v
@@ -72,8 +72,8 @@ Module ForExtraction.
   Local Notation NewLine := (String "010" "") (only parsing).
 
   Definition CollectErrors
-             (res : list (string * Pipeline.ErrorT (list string)) + string)
-    : list (list string) + list string
+             (res : list (string * Pipeline.ErrorT (list string)) + list string)
+    : list (list string) + list (list string)
     := match res with
        | inl res
          => let header := hd "" (List.map (@fst _ _) res) in
@@ -82,7 +82,12 @@ Module ForExtraction.
                   (fun '(name, res) rest
                    => match res, rest with
                       | ErrorT.Error err, rest
-                        => let cur := ("In " ++ name ++ ": " ++ show false err) in
+                        => let in_name := ("In " ++ name ++ ":") in
+                           let cur :=
+                               match show_lines false err with
+                               | [serr] => [in_name ++ " " ++ serr]
+                               | serr => in_name::serr
+                               end in
                            let rest := match rest with inl _ => nil | inr rest => rest end in
                            inr (cur :: rest)
                       | ErrorT.Success v, inr ls => inr ls
@@ -93,10 +98,10 @@ Module ForExtraction.
                   res in
             match res with
             | inl ls => inl ls
-            | inr err => inr (header::err)
+            | inr err => inr ([header]::err)
             end
        | inr res
-         => inr (res::nil)
+         => inr [res]
        end.
 
   Module UnsaturatedSolinas.
@@ -105,7 +110,7 @@ Module ForExtraction.
                (s : string)
                (c : string)
                (machine_wordsize : string)
-    : list (string * Pipeline.ErrorT (list string)) + string
+    : list (string * Pipeline.ErrorT (list string)) + list string
       := let str_n := n in
          let n : nat := parse_n n in
          let str_machine_wordsize := machine_wordsize in
@@ -114,11 +119,11 @@ Module ForExtraction.
          let machine_wordsize := parse_machine_wordsize machine_wordsize in
          match parse_s s, parse_c c with
          | None, None
-           => inr ("Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")")
+           => inr ["Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")"]
          | None, _
-           => inr ("Could not parse s (" ++ s ++ ")")
+           => inr ["Could not parse s (" ++ s ++ ")"]
          | _, None
-           => inr ("Could not parse c (" ++ c ++ ")")
+           => inr ["Could not parse c (" ++ c ++ ")"]
          | Some s, Some c
            => let header :=
                   ((["/* Autogenerated */";
@@ -142,16 +147,17 @@ Module ForExtraction.
                (s : string)
                (c : string)
                (machine_wordsize : string)
-      : list string + string
+      : list string + list string
       := match CollectErrors (PipelineLines n s c machine_wordsize) with
          | inl ls
            => inl
                (List.map (fun s => String.concat NewLine s ++ NewLine ++ NewLine)
                          ls)
-         | inr ls
-           => inr (String.concat
-                    (NewLine ++ NewLine)
-                    ls)
+         | inr nil => inr nil
+         | inr (l :: ls)
+           => inr (l ++ (List.flat_map
+                           (fun e => NewLine :: e)
+                           ls))%list
          end.
 
     Definition Pipeline
@@ -161,7 +167,7 @@ Module ForExtraction.
                (c : string)
                (machine_wordsize : string)
                (success : list string -> A)
-               (error : string -> A)
+               (error : list string -> A)
       : A
       := match ProcessedLines n s c machine_wordsize with
          | inl s => success s
@@ -172,7 +178,7 @@ Module ForExtraction.
                {A}
                (argv : list string)
                (success : list string -> A)
-               (error : string -> A)
+               (error : list string -> A)
       : A
       := match argv with
          | _::n::s::c::machine_wordsize::nil
@@ -180,9 +186,9 @@ Module ForExtraction.
                n s c machine_wordsize
                success
                error
-         | nil => error "empty argv"
+         | nil => error ["empty argv"]
          | prog::args
-           => error ("Expected arguments n, s, c, machine_wordsize, got " ++ show false (List.length args) ++ " arguments in " ++ prog)
+           => error ["Expected arguments n, s, c, machine_wordsize, got " ++ show false (List.length args) ++ " arguments in " ++ prog]
          end.
   End UnsaturatedSolinas.
 
@@ -191,18 +197,18 @@ Module ForExtraction.
                (s : string)
                (c : string)
                (machine_wordsize : string)
-    : list (string * Pipeline.ErrorT (list string)) + string
+    : list (string * Pipeline.ErrorT (list string)) + list string
       := let str_machine_wordsize := machine_wordsize in
          let str_c := c in
          let str_s := s in
          let machine_wordsize := parse_machine_wordsize machine_wordsize in
          match parse_s s, parse_c c with
          | None, None
-           => inr ("Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")")
+           => inr ["Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")"]
          | None, _
-           => inr ("Could not parse s (" ++ s ++ ")")
+           => inr ["Could not parse s (" ++ s ++ ")"]
          | _, None
-           => inr ("Could not parse c (" ++ c ++ ")")
+           => inr ["Could not parse c (" ++ c ++ ")"]
          | Some s, Some c
            => let header :=
                   ((["/* Autogenerated */";
@@ -224,16 +230,17 @@ Module ForExtraction.
                (s : string)
                (c : string)
                (machine_wordsize : string)
-      : list string + string
+      : list string + list string
       := match CollectErrors (PipelineLines s c machine_wordsize) with
          | inl ls
            => inl
                (List.map (fun s => String.concat NewLine s ++ NewLine ++ NewLine)
                          ls)
-         | inr ls
-           => inr (String.concat
-                    (NewLine ++ NewLine)
-                    ls)
+         | inr nil => inr nil
+         | inr (l :: ls)
+           => inr (l ++ (List.flat_map
+                           (fun e => NewLine :: e)
+                           ls))%list
          end.
 
     Definition Pipeline
@@ -242,7 +249,7 @@ Module ForExtraction.
                (c : string)
                (machine_wordsize : string)
                (success : list string -> A)
-               (error : string -> A)
+               (error : list string -> A)
       : A
       := match ProcessedLines s c machine_wordsize with
          | inl s => success s
@@ -253,7 +260,7 @@ Module ForExtraction.
                {A}
                (argv : list string)
                (success : list string -> A)
-               (error : string -> A)
+               (error : list string -> A)
       : A
       := match argv with
          | _::s::c::machine_wordsize::nil
@@ -261,9 +268,9 @@ Module ForExtraction.
                s c machine_wordsize
                success
                error
-         | nil => error "empty argv"
+         | nil => error ["empty argv"]
          | prog::args
-           => error ("Expected arguments s, c, machine_wordsize, got " ++ show false (List.length args) ++ " arguments in " ++ prog)
+           => error ["Expected arguments s, c, machine_wordsize, got " ++ show false (List.length args) ++ " arguments in " ++ prog]
          end.
   End SaturatedSolinas.
 End ForExtraction.
diff --git a/src/Experiments/NewPipeline/CStringification.v b/src/Experiments/NewPipeline/CStringification.v
index c3644d3ec..e774efd54 100644
--- a/src/Experiments/NewPipeline/CStringification.v
+++ b/src/Experiments/NewPipeline/CStringification.v
@@ -218,6 +218,10 @@ Module Compilers.
                           ++ show_f
                     end%list)
                end.
+          Global Instance show_lines_expr {t} : ShowLines (@expr.expr base_type ident (fun _ => string) t)
+            := fun with_parens e => snd (@show_expr_lines t e 1%positive with_parens).
+          Global Instance show_lines_Expr {t} : ShowLines (@expr.Expr base_type ident t)
+            := fun with_parens e => show_lines with_parens (e _).
           Global Instance show_expr {t} : Show (@expr.expr base_type ident (fun _ => string) t)
             := fun with_parens e => String.concat NewLine (snd (@show_expr_lines t e 1%positive with_parens)).
           Global Instance show_Expr {t} : Show (@expr.Expr base_type ident t)
diff --git a/src/Experiments/NewPipeline/StandaloneHaskellMain.v b/src/Experiments/NewPipeline/StandaloneHaskellMain.v
index 5333f7c92..d9ada8451 100644
--- a/src/Experiments/NewPipeline/StandaloneHaskellMain.v
+++ b/src/Experiments/NewPipeline/StandaloneHaskellMain.v
@@ -46,7 +46,7 @@ Module UnsaturatedSolinas.
               (prog::argv)
               (fun res => printf_string
                          (String.concat "" res))
-              (fun err => raise_failure _ err)).
+              (fun err => raise_failure _ (String.concat String.NewLine err))).
 End UnsaturatedSolinas.
 
 Module SaturatedSolinas.
@@ -58,5 +58,5 @@ Module SaturatedSolinas.
               (prog::argv)
               (fun res => printf_string
                          (String.concat "" res))
-              (fun err => raise_failure _ err)).
+              (fun err => raise_failure _ (String.concat String.NewLine err))).
 End SaturatedSolinas.
diff --git a/src/Experiments/NewPipeline/StandaloneOCamlMain.v b/src/Experiments/NewPipeline/StandaloneOCamlMain.v
index c9336ad50..5696cdc12 100644
--- a/src/Experiments/NewPipeline/StandaloneOCamlMain.v
+++ b/src/Experiments/NewPipeline/StandaloneOCamlMain.v
@@ -25,7 +25,7 @@ Axiom string_length : string -> int.
 Axiom string_get : string -> int -> Ascii.ascii.
 Axiom sys_argv : list string.
 Axiom string_init : int -> (int -> Ascii.ascii) -> string.
-Axiom raise_failure : forall A, string -> A.
+Axiom raise_Failure : forall A, string -> A.
 
 Extract Inductive int
 => int [ "0" "Pervasives.succ" ]
@@ -39,7 +39,7 @@ Extract Inlined Constant string_length => "String.length".
 Extract Inlined Constant string_get => "String.get".
 Extract Constant sys_argv => "Array.to_list Sys.argv".
 Extract Inlined Constant string_init => "String.init".
-Extract Constant raise_failure => "fun x -> Printf.printf ""%s\n\n%!"" x; raise (Failure x)".
+Extract Constant raise_Failure => "fun x -> raise (Failure x)".
 
 Fixpoint nat_of_int (x : int) : nat
   := match x with
@@ -77,16 +77,28 @@ Fixpoint list_iter {A} (f : A -> unit) (ls : list A) : unit
      | nil => tt
      end.
 
+Definition printf_list_string (strs : list String.string) : unit
+  := list_iter
+       (fun ls
+        => list_iter printf_char (String.to_list ls))
+       strs.
+Definition printf_list_string_with_newlines (strs : list String.string) : unit
+  := match strs with
+     | nil => printf_list_string nil
+     | str :: strs => printf_list_string (str :: List.map (String.String Ascii.NewLine) strs)
+     end.
+
+Definition raise_failure {A} (msg : list String.string) : A
+  := seq (fun _ => printf_list_string_with_newlines msg)
+         (fun _ => raise_Failure _ (string_of_Coq_string (String.concat String.NewLine msg))).
+
 Module UnsaturatedSolinas.
   Definition main : unit
     := let argv := List.map string_to_Coq_string sys_argv in
        ForExtraction.UnsaturatedSolinas.PipelineMain
          argv
-         (fun res => list_iter
-                       (fun ls
-                        => list_iter printf_char (String.to_list ls))
-                       res)
-         (fun err => raise_failure _ (string_of_Coq_string err)).
+         printf_list_string
+         raise_failure.
 End UnsaturatedSolinas.
 
 Module SaturatedSolinas.
@@ -94,9 +106,6 @@ Module SaturatedSolinas.
     := let argv := List.map string_to_Coq_string sys_argv in
        ForExtraction.SaturatedSolinas.PipelineMain
          argv
-         (fun res => list_iter
-                    (fun ls
-                     => list_iter printf_char (String.to_list ls))
-                    res)
-         (fun err => raise_failure _ (string_of_Coq_string err)).
+         printf_list_string
+         raise_failure.
 End SaturatedSolinas.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 6168dfd22..a1a97b873 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -547,37 +547,39 @@ Module Pipeline.
                     (fun '(b1, b2) => "The bounds " ++ show false b1 ++ " are looser than the expected bounds " ++ show false b2)
                     bs)).
 
-    Global Instance show_ErrorMessage : Show ErrorMessage
+    Global Instance show_lines_ErrorMessage : ShowLines ErrorMessage
       := fun parens e
-         => maybe_wrap_parens
+         => maybe_wrap_parens_lines
               parens
               match e with
               | Computed_bounds_are_not_tight_enough t computed_bounds expected_bounds syntax_tree arg_bounds
-                => ("Computed bounds " ++ show true computed_bounds ++ " are not tight enough (expected bounds not looser than " ++ show true expected_bounds ++ ")." ++ NewLine)
-                     ++ (explain_too_loose_bounds (t:=type.base _) computed_bounds expected_bounds ++ NewLine)
-                     ++ match ToString.C.ToFunctionString
-                                "f" syntax_tree None arg_bounds with
-                        | Some E_str
-                          => ("When doing bounds analysis on the syntax tree:" ++ NewLine)
-                               ++ E_str ++ NewLine
-                               ++ "with input bounds " ++ show true arg_bounds ++ "." ++ NewLine
-                        | None => "(Unprintible syntax tree used in bounds analysis)" ++ NewLine
-                        end
-              | Bounds_analysis_failed => "Bounds analysis failed."
+                => ((["Computed bounds " ++ show true computed_bounds ++ " are not tight enough (expected bounds not looser than " ++ show true expected_bounds ++ ")."]%string)
+                      ++ [explain_too_loose_bounds (t:=type.base _) computed_bounds expected_bounds]
+                      ++ match ToString.C.ToFunctionLines
+                                 "f" syntax_tree None arg_bounds with
+                         | Some E_lines
+                           => ["When doing bounds analysis on the syntax tree:"]
+                                ++ E_lines ++ [""]
+                                ++ ["with input bounds " ++ show true arg_bounds ++ "." ++ NewLine]%string
+                         | None => ["(Unprintible syntax tree used in bounds analysis)" ++ NewLine]%string
+                         end)%list
+              | Bounds_analysis_failed => ["Bounds analysis failed."]
               | Type_too_complicated_for_cps t
-                => "Type too complicated for cps: " ++ show false t
+                => ["Type too complicated for cps: " ++ show false t]
               | Value_not_leZ descr lhs rhs
-                => "Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs
+                => ["Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs]
               | Value_not_leQ descr lhs rhs
-                => "Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs
+                => ["Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs]
               | Value_not_ltZ descr lhs rhs
-                => "Value not < (" ++ descr ++ ") : expected " ++ show false lhs ++ " < " ++ show false rhs
+                => ["Value not < (" ++ descr ++ ") : expected " ++ show false lhs ++ " < " ++ show false rhs]
               | Values_not_provably_distinctZ descr lhs rhs
-                => "Values not provalby distinct (" ++ descr ++ ") : expected " ++ show true lhs ++ " ≠ " ++ show true rhs
+                => ["Values not provalby distinct (" ++ descr ++ ") : expected " ++ show true lhs ++ " ≠ " ++ show true rhs]
               | Values_not_provably_equalZ descr lhs rhs
-                => "Values not provalby equal (" ++ descr ++ ") : expected " ++ show true lhs ++ " = " ++ show true rhs
-              | Stringification_failed t e => "Stringification failed on the syntax tree:" ++ NewLine ++ show false e
+                => ["Values not provalby equal (" ++ descr ++ ") : expected " ++ show true lhs ++ " = " ++ show true rhs]
+              | Stringification_failed t e => ["Stringification failed on the syntax tree:"] ++ show_lines false e
               end.
+    Local Instance show_ErrorMessage : Show ErrorMessage
+      := fun parens err => String.concat NewLine (show_lines parens err).
   End show.
 
   Definition invert_result {T} (v : ErrorT T)