src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 63523 54e932f0c30a
parent 63522 2000e1158667
child 67091 1393c2340eec
equal deleted inserted replaced
63522:2000e1158667 63523:54e932f0c30a
   288 fun triple_int_ord ((a, b, c), (a', b', c')) =
   288 fun triple_int_ord ((a, b, c), (a', b', c')) =
   289   prod_ord int_ord (prod_ord int_ord int_ord) ((a, (b, c)), (a', (b', c')));
   289   prod_ord int_ord (prod_ord int_ord int_ord) ((a, (b, c)), (a', (b', c')));
   290 structure Inttriplefunc = FuncFun(type key = int * int * int val ord = triple_int_ord);
   290 structure Inttriplefunc = FuncFun(type key = int * int * int val ord = triple_int_ord);
   291 
   291 
   292 
   292 
   293 (* More parser basics. *)
   293 (* Parse back csdp output. *)
   294 
   294 
   295 local
   295 local
   296 
   296 
   297 val decimal_digits = Scan.many1 Symbol.is_ascii_digit
   297 val decimal_digits = Scan.many1 Symbol.is_ascii_digit
   298 val decimal_nat = decimal_digits >> (#1 o Library.read_int);
   298 val decimal_nat = decimal_digits >> (#1 o Library.read_int);
   304     | (a, SOME bs) => a + Rat.of_int (#1 (Library.read_int bs)) / rat_pow @10 (length bs));
   304     | (a, SOME bs) => a + Rat.of_int (#1 (Library.read_int bs)) / rat_pow @10 (length bs));
   305 
   305 
   306 fun signed neg parse = $$ "-" |-- parse >> neg || $$ "+" |-- parse || parse;
   306 fun signed neg parse = $$ "-" |-- parse >> neg || $$ "+" |-- parse || parse;
   307 val exponent = ($$ "e" || $$ "E") |-- signed ~ decimal_nat;
   307 val exponent = ($$ "e" || $$ "E") |-- signed ~ decimal_nat;
   308 
   308 
   309 in
       
   310 
       
   311 val decimal =
   309 val decimal =
   312   signed ~ decimal_sig -- Scan.optional exponent 0
   310   signed ~ decimal_sig -- Scan.optional exponent 0
   313     >> (fn (a, b) => a * rat_pow @10 b);
   311     >> (fn (a, b) => a * rat_pow @10 b);
   314 
   312 
       
   313 val csdp_output =
       
   314   decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) --| Scan.many Symbol.not_eof
       
   315     >> (fn (a, bs) => vector_of_list (a :: map_filter I bs));
       
   316 
       
   317 in
       
   318 
       
   319 fun parse_csdpoutput s =
       
   320   Symbol.scanner "Malformed CSDP output" csdp_output (raw_explode s);
       
   321 
   315 end;
   322 end;
   316 
   323 
   317 
       
   318 (* Parse back csdp output. *)
       
   319 
       
   320 (* FIXME improper use of parser combinators ahead *)
       
   321 
       
   322 fun mkparser p s =
       
   323   let val (x,rst) = p (raw_explode s)
       
   324   in if null rst then x else error "mkparser: unparsed input" end;
       
   325 
       
   326 fun ignore _ = ((),[])
       
   327 fun csdpoutput inp =
       
   328   ((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >>
       
   329     (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
       
   330 val parse_csdpoutput = mkparser csdpoutput
       
   331 
   324 
   332 (* Try some apparently sensible scaling first. Note that this is purely to   *)
   325 (* Try some apparently sensible scaling first. Note that this is purely to   *)
   333 (* get a cleaner translation to floating-point, and doesn't affect any of    *)
   326 (* get a cleaner translation to floating-point, and doesn't affect any of    *)
   334 (* the results, in principle. In practice it seems a lot better when there   *)
   327 (* the results, in principle. In practice it seems a lot better when there   *)
   335 (* are extreme numbers in the original problem.                              *)
   328 (* are extreme numbers in the original problem.                              *)