1 (* Title: state_fun.ML |
1 (* Title: state_fun.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Norbert Schirmer, TU Muenchen |
3 Author: Norbert Schirmer, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 |
6 signature STATE_FUN = |
7 structure StateFun = |
7 sig |
|
8 val lookupN : string |
|
9 val updateN : string |
|
10 |
|
11 val mk_constr : Context.theory -> Term.typ -> Term.term |
|
12 val mk_destr : Context.theory -> Term.typ -> Term.term |
|
13 |
|
14 val lookup_simproc : MetaSimplifier.simproc |
|
15 val update_simproc : MetaSimplifier.simproc |
|
16 val ex_lookup_eq_simproc : MetaSimplifier.simproc |
|
17 val ex_lookup_ss : MetaSimplifier.simpset |
|
18 val lazy_conj_simproc : MetaSimplifier.simproc |
|
19 val string_eq_simp_tac : int -> Tactical.tactic |
|
20 |
|
21 val setup : Context.theory -> Context.theory |
|
22 end; |
|
23 |
|
24 structure StateFun: STATE_FUN = |
8 struct |
25 struct |
9 |
26 |
10 val lookupN = "StateFun.lookup"; |
27 val lookupN = "StateFun.lookup"; |
11 val updateN = "StateFun.update"; |
28 val updateN = "StateFun.update"; |
12 |
29 |
13 |
30 val sel_name = HOLogic.dest_string; |
14 fun dest_nib c = |
|
15 let val h = List.last (String.explode c) |
|
16 in if #"0" <= h andalso h <= #"9" then Char.ord h - Char.ord #"0" |
|
17 else if #"A" <= h andalso h <= #"F" then Char.ord h - Char.ord #"A" + 10 |
|
18 else raise Match |
|
19 end; |
|
20 |
|
21 fun dest_chr (Const ("List.char.Char",_)$Const (c1,_)$(Const (c2,_))) = |
|
22 let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2) |
|
23 in if Char.isPrint c then c else raise Match end |
|
24 | dest_chr _ = raise Match; |
|
25 |
|
26 fun dest_string (Const ("List.list.Nil",_)) = [] |
|
27 | dest_string (Const ("List.list.Cons",_)$c$cs) = dest_chr c::dest_string cs |
|
28 | dest_string _ = raise TERM ("dest_string",[]); |
|
29 |
|
30 fun sel_name n = String.implode (dest_string n); |
|
31 |
31 |
32 fun mk_name i t = |
32 fun mk_name i t = |
33 (case try sel_name t of |
33 (case try sel_name t of |
34 SOME name => name |
34 SOME name => name |
35 | NONE => (case t of |
35 | NONE => (case t of |