| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Mon, 20 Oct 2025 22:18:21 +0200 | |
| changeset 1013 | 1a23d87d1700 | 
| parent 788 | 3b1136fb6bee | 
| permissions | -rw-r--r-- | 
| 446 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1 | def simp(r: Rexp): (Rexp, Val => Val) = r match {
 | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 2 |   case ALT(r1, r2) => {
 | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 3 | val (r1s, f1s) = simp(r1) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 4 | val (r2s, f2s) = simp(r2) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 5 |     (r1s, r2s) match {
 | 
| 453 
36e5752fa191
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
446diff
changeset | 6 | case (ZERO, _) => (r2s, F_RIGHT(f2s)) | 
| 
36e5752fa191
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
446diff
changeset | 7 | case (_, ZERO) => (r1s, F_LEFT(f1s)) | 
| 446 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 8 | case _ => | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 9 | if (r1s == r2s) (r1s, F_LEFT(f1s)) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 10 | else (ALT (r1s, r2s), F_ALT(f1s, f2s)) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 11 | } | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 12 | } | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 13 | ... | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 14 | } | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 15 | def F_RIGHT(f: Val => Val) = (v:Val) => Right(f(v)) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 16 | def F_LEFT(f: Val => Val) = (v:Val) => Left(f(v)) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 17 | def F_ALT(f1: Val => Val, f2: Val => Val) = | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 18 |   (v:Val) => v match {
 | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 19 | case Right(v) => Right(f2(v)) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 20 | case Left(v) => Left(f1(v)) } |