equal
deleted
inserted
replaced
448 end; |
448 end; |
449 |
449 |
450 |
450 |
451 (* target *) |
451 (* target *) |
452 |
452 |
453 val sanitize_name = (*FIXME*) |
453 val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) |
454 let |
454 let |
455 fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s |
455 fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s |
456 orelse s = "'" orelse s = "_"; |
456 orelse s = "'" orelse s = "_"; |
457 val is_junk = not o is_valid andf Symbol.is_regular; |
457 val is_junk = not o is_valid andf Symbol.is_regular; |
458 val junk = Scan.many is_junk; |
458 val junk = Scan.many is_junk; |
463 ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); |
463 ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); |
464 in |
464 in |
465 explode #> scan_valids #> implode |
465 explode #> scan_valids #> implode |
466 end; |
466 end; |
467 |
467 |
468 fun type_name "Product_Type.*" = "prod" |
468 val type_name = sanitize_name o Long_Name.base_name; |
469 | type_name "Sum_Type.+" = "sum" |
|
470 | type_name s = sanitize_name (Long_Name.base_name s); |
|
471 |
469 |
472 fun resort_terms pp algebra consts constraints ts = |
470 fun resort_terms pp algebra consts constraints ts = |
473 let |
471 let |
474 fun matchings (Const (c_ty as (c, _))) = (case constraints c |
472 fun matchings (Const (c_ty as (c, _))) = (case constraints c |
475 of NONE => I |
473 of NONE => I |