584 "\n" ^ Output.output (Pretty.string_of |
584 "\n" ^ Output.output (Pretty.string_of |
585 (Pretty.block [Pretty.str "val () = Codegen.test_fn :=", |
585 (Pretty.block [Pretty.str "val () = Codegen.test_fn :=", |
586 Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1, |
586 Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1, |
587 Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, |
587 Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, |
588 Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) => |
588 Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) => |
589 Pretty.block [Pretty.str ("val " ^ s ^ " ="), Pretty.brk 1, |
589 Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1, |
590 mk_gen sg false [] "" T, Pretty.brk 1, |
590 mk_gen sg false [] "" T, Pretty.brk 1, |
591 Pretty.str (szname ^ ";")]) frees)), |
591 Pretty.str (szname ^ ";")]) frees)), |
592 Pretty.brk 1, Pretty.str "in", Pretty.brk 1, |
592 Pretty.brk 1, Pretty.str "in", Pretty.brk 1, |
593 Pretty.block [Pretty.str "if ", |
593 Pretty.block [Pretty.str "if ", |
594 mk_app false (Pretty.str "testf") (map (Pretty.str o fst) frees), |
594 mk_app false (Pretty.str "testf") (map (Pretty.str o mk_id o fst) frees), |
595 Pretty.brk 1, Pretty.str "then Library.None", |
595 Pretty.brk 1, Pretty.str "then Library.None", |
596 Pretty.brk 1, Pretty.str "else ", |
596 Pretty.brk 1, Pretty.str "else ", |
597 Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" :: |
597 Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" :: |
598 flat (separate [Pretty.str ",", Pretty.brk 1] |
598 flat (separate [Pretty.str ",", Pretty.brk 1] |
599 (map (fn (s, T) => [Pretty.block |
599 (map (fn (s, T) => [Pretty.block |
600 [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1, |
600 [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1, |
601 mk_app false (mk_term_of sg false T) |
601 mk_app false (mk_term_of sg false T) |
602 [Pretty.str s], Pretty.str ")"]]) frees)) @ |
602 [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @ |
603 [Pretty.str "]"])]], |
603 [Pretty.str "]"])]], |
604 Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"])) ^ |
604 Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"])) ^ |
605 "\n\nend;\n"; |
605 "\n\nend;\n"; |
606 val _ = use_text Context.ml_output false s; |
606 val _ = use_text Context.ml_output false s; |
607 fun iter f k = if k > i then None |
607 fun iter f k = if k > i then None |