| 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 SEQ(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, _) => (ZERO, F_ERROR) | 
| 
36e5752fa191
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
446diff
changeset | 7 | case (_, ZERO) => (ZERO, F_ERROR) | 
| 788 | 8 | case (ONE, _) => (r2s, F_SEQ_Empty1(f1s, f2s)) | 
| 9 | case (_, ONE) => (r1s, F_SEQ_Empty2(f1s, f2s)) | |
| 446 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 10 | case _ => (SEQ(r1s,r2s), F_SEQ(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 | } | 
| 788 | 13 | ...} | 
| 14 | def F_SEQ_Empty1(f1: Val => Val, f2: Val => Val) = | |
| 15 | (v:Val) => Sequ(f1(Empty), f2(v)) | |
| 16 | def F_SEQ_Empty2(f1: Val => Val, f2: Val => Val) = | |
| 17 | (v:Val) => Sequ(f1(v), f2(Empty)) | |
| 446 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 18 | def F_SEQ(f1: Val => Val, f2: Val => Val) = | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 19 |   (v:Val) => v match {
 | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 20 | case Sequ(v1, v2) => Sequ(f1(v1), f2(v2)) } |