1structure DiskFilesHeader :> DiskFilesHeader =
2struct
3
4open HolKernel
5
6type id = {Thy:string,Name:string}
7
8datatype pretype = ptv of string | ptop of int * int list
9datatype pre_vc = ptm_v of string * int | ptm_c of int * int
10datatype preterm = app of preterm * preterm | abs of int * preterm
11                 | atom of int
12type prethm = preterm list * preterm
13type 'a array = (int,'a)Binarymap.dict
14type parse_result =
15     id array * pretype array * pre_vc array * (string * prethm) list
16
17infix !
18fun (a ! n) = Binarymap.find (a, n)
19
20fun push (a, item) = Binarymap.insert(a, Binarymap.numItems a, item)
21
22fun convert_pretype (ids : id array) (k, prety, acc : hol_type array) = let
23  val result =
24      case prety of
25        ptv s => mk_vartype s
26      | ptop (opnum, arglist) => let
27          val {Thy,Name} = ids ! opnum
28          val args = map (fn n => acc ! n) arglist
29        in
30          mk_thy_type { Args = args, Thy = Thy, Tyop = Name }
31        end
32in
33  push(acc, result)
34end
35
36fun convert_atom
37      (ids : id array, types : hol_type array)
38      (k, pre_atom, acc : term array)
39  = let
40    val result =
41        case pre_atom of
42          ptm_v (s, tyn) => mk_var(s, types ! tyn)
43        | ptm_c (idn, tyn) => let
44            val {Thy,Name} = ids ! idn
45            val ty = types ! tyn
46          in
47            mk_thy_const {Thy = Thy, Name = Name, Ty = ty}
48          end
49  in
50    push(acc, result)
51  end
52
53fun convert_term (atoms : term array, pre_term) = let
54  fun c t = convert_term(atoms, t)
55in
56  case pre_term of
57    app(t1, t2) => mk_comb(c t1, c t2)
58  | abs(an, t) => mk_abs(atoms ! an, c t)
59  | atom i => atoms ! i
60end
61
62fun convert_thm (atoms : term array, (h,c)) = let
63  val hyps = map (fn pt => convert_term (atoms, pt)) h
64  val c_t = convert_term (atoms, c)
65in
66  mk_thm(hyps, c_t)
67end
68
69fun convert_prethms (ids, types, atoms, named_ths) = let
70  val types = Binarymap.foldl (convert_pretype ids)
71                              (Binarymap.mkDict Int.compare)
72                              types
73  val atoms = Binarymap.foldl (convert_atom (ids, types))
74                              (Binarymap.mkDict Int.compare)
75                              atoms
76in
77  map (fn (s, pth) => (s, convert_thm(atoms, pth))) named_ths
78end
79
80
81
82
83end;
84