equal
deleted
inserted
replaced
71 | Number of int |
71 | Number of int |
72 | Other of string |
72 | Other of string |
73 |
73 |
74 |
74 |
75 exception NOCUT |
75 exception NOCUT |
76 fun is_prefix [] l = true |
|
77 | is_prefix (h::t) [] = false |
|
78 | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t' |
|
79 fun remove_prefix [] l = l |
76 fun remove_prefix [] l = l |
80 | remove_prefix (h::t) [] = error "can't remove prefix" |
77 | remove_prefix (h::t) [] = error "can't remove prefix" |
81 | remove_prefix (h::t) (h'::t') = remove_prefix t t' |
78 | remove_prefix (h::t) (h'::t') = remove_prefix t t' |
82 fun ccut t [] = raise NOCUT |
79 fun ccut t [] = raise NOCUT |
83 | ccut t s = |
80 | ccut t s = |
84 if is_prefix t s then ([], remove_prefix t s) else |
81 if is_prefix (op =) t s then ([], remove_prefix t s) else |
85 let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end |
82 let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end |
86 fun cut t s = |
83 fun cut t s = |
87 let |
84 let |
88 val t' = explode t |
85 val t' = explode t |
89 val s' = explode s |
86 val s' = explode s |