equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 structure Mirabelle_Arith : MIRABELLE_ACTION = |
5 structure Mirabelle_Arith : MIRABELLE_ACTION = |
6 struct |
6 struct |
7 |
7 |
8 fun arith_action {pre, timeout, log, ...} = |
8 fun arith_tag id = "#" ^ string_of_int id ^ " arith: " |
|
9 |
|
10 fun init _ = I |
|
11 fun done _ _ = () |
|
12 |
|
13 fun run id {pre, timeout, log, ...} = |
9 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
14 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
10 then log "arith: succeeded" |
15 then log (arith_tag id ^ "succeeded") |
11 else () |
16 else () |
12 handle TimeLimit.TimeOut => log "arith: timeout" |
17 handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout") |
13 |
18 |
14 fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action) |
19 fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) |
15 |
20 |
16 end |
21 end |