| author | Christian Urban <urbanc@in.tum.de> | 
| Sun, 05 Aug 2018 21:37:35 +0100 | |
| changeset 553 | a05c412b1550 | 
| 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: 
446 
diff
changeset
 | 
6  | 
case (ZERO, _) => (ZERO, F_ERROR)  | 
| 
 
a5525c780b96
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
446 
diff
changeset
 | 
7  | 
case (_, ZERO) => (ZERO, F_ERROR)  | 
| 
 
a5525c780b96
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
446 
diff
changeset
 | 
8  | 
case (ONE, _) => (r2s, F_SEQ_Void1(f1s, f2s))  | 
| 
 
a5525c780b96
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
446 
diff
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)) }  |