backout c6297fa1031a -- strange parsers are required to make this work;
authorwenzelm
Sun Sep 29 00:15:05 2013 +0200 (2013-09-29)
changeset 5397522ee3fb9d596
parent 53974 612505263257
child 53976 da610b507799
backout c6297fa1031a -- strange parsers are required to make this work;
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Sep 28 22:47:17 2013 +0200
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Sep 29 00:15:05 2013 +0200
     1.3 @@ -275,9 +275,11 @@
     1.4     end
     1.5   end;
     1.6  
     1.7 +
     1.8  fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x;
     1.9  
    1.10 -(* More parser basics.                                                       *)
    1.11 +(* More parser basics. *)
    1.12 +(* FIXME improper use of parser combinators ahead *)
    1.13  
    1.14   val numeral = Scan.one isnum
    1.15   val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
    1.16 @@ -298,17 +300,20 @@
    1.17   val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
    1.18      >> (fn (h, x) => h */ pow10 (int_of_rat x));
    1.19  
    1.20 + fun mkparser p s =
    1.21 +  let val (x,rst) = p (raw_explode s)
    1.22 +  in if null rst then x
    1.23 +     else error "mkparser: unparsed input"
    1.24 +  end;;
    1.25 +
    1.26  (* Parse back csdp output.                                                      *)
    1.27 +(* FIXME improper use of parser combinators ahead *)
    1.28  
    1.29   fun ignore _ = ((),[])
    1.30   fun csdpoutput inp =
    1.31     ((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >>
    1.32      (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
    1.33 -
    1.34 - fun parse_csdpoutput s =
    1.35 -  (case Scan.read Symbol.stopper csdpoutput (raw_explode s) of
    1.36 -    SOME x => x
    1.37 -  | NONE => error ("Failed to parse CSDP output: " ^ quote s))
    1.38 + val parse_csdpoutput = mkparser csdpoutput
    1.39  
    1.40  (* Try some apparently sensible scaling first. Note that this is purely to   *)
    1.41  (* get a cleaner translation to floating-point, and doesn't affect any of    *)