| author | Christian Urban <urbanc@in.tum.de> | 
| Wed, 06 Nov 2019 23:17:05 +0000 | |
| changeset 683 | 9acbe46df3fd | 
| parent 453 | a5525c780b96 | 
| child 788 | 0a3ba0769a61 | 
| 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 
a5525c780b96
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
446diff
changeset | 6 | case (ZERO, _) => (ZERO, F_ERROR) | 
| 
a5525c780b96
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
446diff
changeset | 7 | case (_, ZERO) => (ZERO, F_ERROR) | 
| 
a5525c780b96
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
446diff
changeset | 8 | case (ONE, _) => (r2s, F_SEQ_Void1(f1s, f2s)) | 
| 
a5525c780b96
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
446diff
changeset | 9 | case (_, ONE) => (r1s, F_SEQ_Void2(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 | } | 
| 
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_SEQ_Void1(f1: Val => Val, f2: Val => Val) = | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 16 | (v:Val) => Sequ(f1(Void), f2(v)) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 17 | def F_SEQ_Void2(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) => Sequ(f1(v), f2(Void)) | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 19 | 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 | 20 |   (v:Val) => v match {
 | 
| 
16742bf62365
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 21 | case Sequ(v1, v2) => Sequ(f1(v1), f2(v2)) } |