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