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