1(* ------------------------------------------------------------------------- 2 Support for assembly code parsing and pretty-printing 3 ------------------------------------------------------------------------- *) 4 5structure assemblerLib :> assemblerLib = 6struct 7 8open HolKernel boolLib bossLib 9 10local 11 open IntExtra Nat Set L3 Bitstring BitsN FP32 FP64 FPConvert 12in 13end 14 15(* Turns a quote `...` into a list of strings, removing comments *) 16local 17 val compressNewlines = 18 Substring.full o Substring.translate (fn #"\n" => "\n" | _ => "") 19 fun strip_comments (d, a) s = 20 if Substring.size s = 0 21 then a 22 else let 23 val (l, r) = 24 Substring.splitl (fn c => c <> #"(" andalso c <> #"*") s 25 val a' = a @ [if 0 < d then compressNewlines l else l] 26 in 27 if Substring.isPrefix "(*" r 28 then strip_comments (d + 1, a') (Substring.triml 2 r) 29 else if Substring.isPrefix "*)" r 30 then strip_comments (d - 1, a') (Substring.triml 2 r) 31 else if Substring.size r = 0 32 then a' 33 else let 34 val (r1, r2) = Substring.splitAt (r, 1) 35 in 36 strip_comments (d, if 0 < d then a' else a' @ [r1]) r2 37 end 38 end 39 val lines = String.fields (fn c => c = #"\n") o Substring.concat o 40 strip_comments (0, []) o Substring.full 41in 42 val quote_to_strings = fn [QUOTE s] => lines s | _ => raise General.Bind 43end 44 45type lines = {string : string, line : int} list 46 47exception Assembler of lines 48 49fun printn s = print (s ^ "\n") 50 51val printLines: lines -> unit = 52 List.app (fn {string, line} => 53 printn ("line " ^ Int.toString line ^ " : " ^ string)) 54 55fun dropLastChar "" = "" 56 | dropLastChar s = String.substring (s, 0, String.size s - 1) 57 58fun hex w = StringCvt.padLeft #"0" (Nat.toNativeInt (BitsN.size w) div 4) 59 (L3.lowercase (BitsN.toHexString w)) 60 61fun word n s = Option.valOf (BitsN.fromHexString (s, Nat.fromNativeInt n)) 62 63end 64