src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 63523 54e932f0c30a
parent 63522 2000e1158667
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 19 16:35:51 2016 +0200
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 19 16:50:39 2016 +0200
     1.3 @@ -290,7 +290,7 @@
     1.4  structure Inttriplefunc = FuncFun(type key = int * int * int val ord = triple_int_ord);
     1.5  
     1.6  
     1.7 -(* More parser basics. *)
     1.8 +(* Parse back csdp output. *)
     1.9  
    1.10  local
    1.11  
    1.12 @@ -306,29 +306,22 @@
    1.13  fun signed neg parse = $$ "-" |-- parse >> neg || $$ "+" |-- parse || parse;
    1.14  val exponent = ($$ "e" || $$ "E") |-- signed ~ decimal_nat;
    1.15  
    1.16 -in
    1.17 -
    1.18  val decimal =
    1.19    signed ~ decimal_sig -- Scan.optional exponent 0
    1.20      >> (fn (a, b) => a * rat_pow @10 b);
    1.21  
    1.22 +val csdp_output =
    1.23 +  decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) --| Scan.many Symbol.not_eof
    1.24 +    >> (fn (a, bs) => vector_of_list (a :: map_filter I bs));
    1.25 +
    1.26 +in
    1.27 +
    1.28 +fun parse_csdpoutput s =
    1.29 +  Symbol.scanner "Malformed CSDP output" csdp_output (raw_explode s);
    1.30 +
    1.31  end;
    1.32  
    1.33  
    1.34 -(* Parse back csdp output. *)
    1.35 -
    1.36 -(* FIXME improper use of parser combinators ahead *)
    1.37 -
    1.38 -fun mkparser p s =
    1.39 -  let val (x,rst) = p (raw_explode s)
    1.40 -  in if null rst then x else error "mkparser: unparsed input" end;
    1.41 -
    1.42 -fun ignore _ = ((),[])
    1.43 -fun csdpoutput inp =
    1.44 -  ((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >>
    1.45 -    (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
    1.46 -val parse_csdpoutput = mkparser csdpoutput
    1.47 -
    1.48  (* Try some apparently sensible scaling first. Note that this is purely to   *)
    1.49  (* get a cleaner translation to floating-point, and doesn't affect any of    *)
    1.50  (* the results, in principle. In practice it seems a lot better when there   *)