GitLab will be upgraded on 30 Jan 2023 from 2.00 pm (AEDT) to 3.00 pm (AEDT). During the update, GitLab and Mattermost services will not be available. If you have any concerns with this, please talk to us at N110 (b) CSIT building.

CodeParser.sml 21.5 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
structure CodeParser :> CodeParser =
struct
  open HolKernel TypeBase Parse Term UIRLexer 
  open boolLib
  open finite_mapSyntax
  open listSyntax
  open numSyntax
  open pairSyntax
  open stringSyntax
  open sumSyntax
  open wordsSyntax
  open uvmValuesTheory
  open uvmMemoryTheory
  open uvmIRTheory
  open ParserHelpers
  open TypeParser

  val bin_ops = [
    "ADD", "SUB", "MUL", "SDIV", "SREM", "UDIV", "UREM", "SHL", "LSHR", "ASHR",
    "AND", "OR", "XOR", "FADD", "FSUB", "FMUL", "FDIV", "FREM"
  ]

  val cmp_ops = [
    "EQ", "NE", "SGE", "SGT", "SLE", "SLT", "UGE", "UGT", "ULE", "ULT",
    "FFALSE", "FTRUE", "FOEQ", "FOGT", "FOGE", "FOLT", "FOLE", "FONE", "FORD",
    "FUEQ", "FUGT", "FUGE", "FULT", "FULE", "FUNE", "FUNO"
  ]

  val conv_ops = [
    "TRUNC", "ZEXT", "SEXT", "FPTRUNC", "FPEXT", "FPTOUI", "FPTOSI", "UITOFP",
    "SITOFP", "BITCAST", "REFCAST", "PTRCAST"
  ]

  val insts = bin_ops @ cmp_ops @ conv_ops @ [
    "ID", "SELECT", "EXTRACTVALUE", "INSERTVALUE", "EXTRACTELEMENT",
    "INSERTELEMENT", "SHUFFLEVECTOR", "NEW", "ALLOCA", "NEWHYBRID",
    "ALLOCAHYBRID", "GETIREF", "GETFIELDIREF", "GETELEMENTIREF", "SHIFTIREF",
    "GETVARPARTIREF", "LOAD", "STORE", "CMPXCHG", "ATOMICRMW", "FENCE",
Adam Nelson's avatar
Adam Nelson committed
39
    "NEWTHREAD"
40
41
42
43
44
45
46
  ]

  val terminsts = [
    "RET", "THROW", "CALL", "TAILCALL", "BRANCH", "BRANCH2", "SWITCH", "TRAP",
    "WATCHPOINT", "WPBRANCH", "SWAPSTACK", "COMMINST"
  ]

47
48
49
50
51
  val mem_orders = [
    "NOT_ATOMIC", "RELAXED", "CONSUME", "ACQUIRE", "RELEASE", "ACQ_REL",
    "SEQ_CST"
  ]

52
  val comminsts = [
53
    "uvm.new_stack", "uvm.current_stack"
54
55
  ]

56
57
  val ty_ssa = mk_type("ssavar", [])
  val ty_blabel = mk_type("block_label", [])
58
  val ty_ci = mk_type("comminst", [ty_ssa])
59
60
61
62
63
64
  fun or_const ty = ``:^ty or_const``

  val t_Var = mk_const("INL", ty_ssa --> or_const ty_ssa)
  val t_Const = mk_const("INR", ty_val --> or_const ty_ssa)
  val t_SSA = mk_const("SSA", ty_str --> ty_ssa)
  fun mk_ssa s = mk_comb(t_SSA, fromMLstring s)
65
66
67
  fun mk_some x =
    let val ty = type_of x
    in mk_comb(mk_const("SOME", ty --> mk_type("option", [ty])), x) end
68
69
70
71
72
73
74
75
76
77
78
79
80

  fun ir_const (name : string) (ty : hol_type) : term =
    mk_thy_const { Thy="uvmIR", Name=name, Ty=ty }

  fun ir_ap(name, xs, ty_out) =
    let val ty = foldr (op -->) ty_out (map (#1 o dest_sum o type_of) xs) in
      (* print ("\nname: " ^ name ^ ", ty: " ^ type_to_string ty); *)
      list_mk_lift(ir_const name ty, xs)
    end

  (* Reads an SSA variable, replacing global variables with constants using the
     given context. Returns a term of type ``:ssavar or_const or_error``.
  *)
81
82
  fun ssa_var _ (Local, v) = mk_return(mk_comb(t_Var, mk_ssa v))
    | ssa_var (env : env_context) (Global, v) = mk_lift(t_Const, #get_global env v)
83

84
  fun parse_mem_order (ord : string) : term =
Adam Nelson's avatar
Adam Nelson committed
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
    if exists (fn x => x = ord) mem_orders then
      mk_const(ord, mk_type("memory_order", []))
    else
      raise ParseError (ord ^ " is not a memory order")

  fun parse_new_stack_clause (env : env_context) (tokens : uir_token list)
                             : (term * uir_token list) =
    let
      val ty = mk_type("new_stack_clause", [or_const ty_ssa])
      val ty_pair = mk_prod(or_const ty_ssa, ty_type)
    in
    case tokens of
      Word "PASS_VALUES" :: Type tys :: Parens vals :: rest =>
        (mk_lift(mk_const("PassValues", ty_list ty_pair --> ty),
          mk_sequence(
            map (fn (ty, v) =>
              case v of
                SSA v => list_mk_lift(
                    mk_const(",", or_const ty_ssa --> ty_type --> ty_pair),
104
                    [ssa_var env v, ty])
Adam Nelson's avatar
Adam Nelson committed
105
106
107
108
109
              | _ => raise ParseError "PASS_VALUES expected SSA arguments")
              (ListPair.zipEq(parse_type_list env tys, vals)),
            ty_pair)), rest)
    | Word "THROW_EXC" :: SSA exc :: rest =>
        (mk_lift(mk_const("ThrowExc", or_const ty_ssa --> ty),
110
          ssa_var env exc), rest)
Adam Nelson's avatar
Adam Nelson committed
111
112
    | _ => raise ParseError "expected newStackClause (PASS_VALUES or THROW_EXC)"
    end
113

114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
  fun lhs0 (lhs : uir_token) (inst : string) =
    case lhs of
      Parens [] => ()
    | _ => raise ParseError(inst ^ " does not return a value")

  fun lhs1 (lhs : uir_token) (inst : string) =
    case lhs of
      SSA (Local, v) => mk_return(mk_ssa v)
    | Parens [SSA (Local, v)] => mk_return(mk_ssa v)
    | _ => raise ParseError(inst ^ " returns exactly 1 value")

  fun lhs_n (lhs : uir_token) (inst : string) =
    case lhs of
      (SSA (Local, v)) => mk_list([mk_ssa v], ty_ssa)
    | (Parens vs) =>
        let fun var (SSA (Local, v)) = mk_ssa v
              | var _ = raise ParseError(inst ^ " lhs contains non-SSA-var")
        in mk_list(map var vs, ty_ssa) end
    | _ => raise ParseError(inst ^ " lhs contains non-SSA-var")

134
135
136
137
138
139
140
  (* Parses a list of tokens into a Mu IR instruction. Returns a term of type
     ``:ssavar instruction or_error``.
  *)
  fun parse_inst (env : env_context) (tokens : uir_token list) : term =
    let
      val ty_inst = mk_type("instruction", [ty_ssa])
      val ty_expr = mk_type("expression", [or_const ty_ssa])
141
142
143
144
      val t_ref = mk_return(mk_const("REF", ty_reft))
      val t_ptr = mk_return(mk_const("PTR", ty_reft))
      val t_na = mk_return(mk_const("NOT_ATOMIC", mk_type("memory_order", [])))
      val t_void = mk_return(mk_const("Void", ty_type))
Adam Nelson's avatar
Adam Nelson committed
145
146
147
148
      val t_null = mk_return(infer_comb("INR", [infer_comb("RefV", [
          mk_const("Void", ty_type),
          mk_const("NONE", ``:addr option``)
        ], ty_val)], ``:ssavar or_const``))
149
150
151
152
153
154
155
156
157
158
159
160
161
      fun two_tys tys = 
        let
          val (t1, rest) = take_one_type tys
          val (t2, rest') = take_one_type rest
          val _ = case rest' of
                    [] => ()
                  | _ => raise ParseError "expected exactly 2 types in <...>"
        in (parse_type env t1, parse_type env t2) end
      fun ssa_noconst (Local, v) = mk_return(mk_ssa v)
        | ssa_noconst (Global, v) = raise ParseError(
            "global name @" ^ v ^ " used in illegal location")
      val (lhs, rhs) = case tokens of l::Eq::r => (l, r) | _ => (Parens [], tokens)
      fun mk_assign(inst : string, expr : term) =
162
        ir_ap("Assign", [mk_return (lhs_n lhs inst), expr], ty_inst)
163
    in case rhs of
164
165
166
    (* Identity instruction *)
      [Word "ID", Type ty, SSA i] =>
        let val ty' = parse_type env ty in
167
          mk_assign("ID", ir_ap("Id", [ty', ssa_var env i], ty_expr))
168
169
170
171
172
        end
    (* TODO: Compound value operations *)
    (* IRef instructions *)
    | [Word "GETIREF", Type ty, SSA opnd] =>
        mk_assign("GETIREF", ir_ap("GetIRef",
173
          [parse_type env ty, ssa_var env opnd], ty_expr))
174
175
176
177
178
179
180
181
182
    (* TODO: PTR variants of iref instructions *)
    | [Word "GETFIELDIREF", Type tys, SSA opnd] =>
        let
          val (t1, rest) = take_one_type tys
          val index = case rest of [Int n] => Arbint.toNat n
          | _ => raise ParseError "GETFIELDIREF expected field index after type"
        in
          mk_assign("GETFIELDIREF", ir_ap("GetFieldIRef", [
            t_ref, parse_type env t1, mk_return(lift_num ty_num index),
183
            ssa_var env opnd
184
185
186
187
188
          ], ty_expr))
        end
    | [Word "GETELEMIREF", Type tys, SSA opnd, SSA index] =>
        let val (t1, t2) = two_tys tys in
          mk_assign("GETELEMIREF", ir_ap("GetElementIRef", [
189
            t_ref, t1, t2, ssa_var env opnd, ssa_var env index
190
191
192
193
194
          ], ty_expr))
        end
    | [Word "SHIFTIREF", Type tys, SSA opnd, SSA index] =>
        let val (t1, t2) = two_tys tys in
          mk_assign("SHIFTIREF", ir_ap("ShiftIRef", [
195
            t_ref, t1, t2, ssa_var env opnd, ssa_var env index
196
197
198
199
          ], ty_expr))
        end
    | [Word "GETVARPARTIREF", Type ty, SSA opnd] =>
        mk_assign("GETVARPARTIREF", ir_ap("GetVarPartIRef",
200
          [t_ref, parse_type env ty, ssa_var env opnd], ty_expr))
201
202
    (* Load *)
    | [Word "LOAD", Type ty, SSA src] => ir_ap("Load",
203
        [lhs1 lhs "LOAD", t_ref, parse_type env ty, ssa_noconst src, t_na], ty_inst)
204
    | [Word "LOAD", Word "PTR", Type ty, SSA src] => ir_ap("Load",
205
        [lhs1 lhs "LOAD", t_ptr, parse_type env ty, ssa_noconst src, t_na], ty_inst)
206
    | [Word "LOAD", Word ord, Type ty, SSA src] => ir_ap("Load", [
207
          lhs1 lhs "LOAD", t_ref, parse_type env ty, ssa_noconst src,
208
209
210
          mk_return(parse_mem_order ord)
        ], ty_inst)
    | [Word "LOAD", Word "PTR", Word ord, Type ty, SSA src] => ir_ap("Load", [
211
          lhs1 lhs "LOAD", t_ptr, parse_type env ty, ssa_noconst src,
212
213
214
215
          mk_return(parse_mem_order ord)
        ], ty_inst)
    (* Store *)
    | [Word "STORE", Type ty, SSA dst, SSA src] =>
216
        let val _ = lhs0 lhs "STORE"
217
218
            val ty' = parse_type env ty
        in ir_ap("Store", [
219
             ssa_var env src, t_ref, ty', ssa_noconst dst, t_na
220
221
222
           ], ty_inst)
        end
    | [Word "STORE", Word "PTR", Type ty, SSA dst, SSA src] =>
223
        let val _ = lhs0 lhs "STORE"
224
225
            val ty' = parse_type env ty
        in ir_ap("Store", [
226
             ssa_var env src, t_ptr, ty', ssa_noconst dst, t_na
227
228
229
           ], ty_inst)
        end
    | [Word "STORE", Word ord, Type ty, SSA dst, SSA src] =>
230
        let val _ = lhs0 lhs "STORE"
231
232
            val ty' = parse_type env ty
        in ir_ap("Store", [
233
             ssa_var env src, t_ref, ty', ssa_noconst dst,
234
235
236
237
             mk_return(parse_mem_order ord)
           ], ty_inst)
        end
    | [Word "STORE", Word "PTR", Word ord, Type ty, SSA dst, SSA src] =>
238
        let val _ = lhs0 lhs "STORE"
239
240
            val ty' = parse_type env ty
        in ir_ap("Store", [
241
             ssa_var env src, t_ptr, ty', ssa_noconst dst,
242
243
244
245
246
247
248
249
             mk_return(parse_mem_order ord)
           ], ty_inst)
        end
    (* Fence *)
    | [Word "FENCE", Word ord] =>
        ir_ap("Fence", [mk_return(parse_mem_order ord)], ty_inst)
    (* New, Alloca *)
    | [Word "NEW", Type ty] =>
250
        ir_ap("New", [lhs1 lhs "NEW", parse_type env ty], ty_inst)
251
    | [Word "ALLOCA", Type ty] =>
252
        ir_ap("Alloca", [lhs1 lhs "ALLOCA", parse_type env ty], ty_inst)
253
254
    | [Word "NEWHYBRID", Type tys, SSA len] =>
        let val (t1, t2) = two_tys tys in
255
          ir_ap("NewHybrid", [lhs1 lhs "NEWHYBRID", t1, t2, ssa_var env len],
256
257
258
259
260
            ty_inst)
        end
    | [Word "ALLOCAHYBRID", Type tys, SSA len] =>
        let val (t1, t2) = two_tys tys in
          ir_ap("AllocaHybrid", [
261
            lhs1 lhs "ALLOCAHYBRID", t1, t2, ssa_var env len
262
263
          ], ty_inst)
        end
Adam Nelson's avatar
Adam Nelson committed
264
265
266
267
268
    (* New Thread *)
    | Word "NEWTHREAD" :: SSA stack :: rest =>
        let val (nsc, nil) = parse_new_stack_clause env rest in
          case nil of
            [] => ir_ap("NewThread", [
269
                    lhs1 lhs "NEWTHREAD",
270
                    ssa_var env stack,
271
                    t_null, nsc
Adam Nelson's avatar
Adam Nelson committed
272
273
274
                  ], ty_inst)
          | _ => raise ParseError "invalid arguments for NEWTHREAD"
        end
275
276
    (* Binary operations *)
    | [Word opn, Type ty, SSA l, SSA r] =>
277
278
279
280
        let val ty' = parse_type env ty in mk_assign(opn,
          if exists (fn x => x = opn) bin_ops then
            ir_ap("BinOp", [
              mk_return(ir_const opn (mk_type("bin_op", []))),
281
              ty', ssa_var env l, ssa_var env r
282
283
284
285
            ], ty_expr)
          else if exists (fn x => x = opn) cmp_ops then
            ir_ap("CmpOp", [
              mk_return(ir_const opn (mk_type("cmp_op", []))),
286
              ty', ssa_var env l, ssa_var env r
287
288
            ], ty_expr)
          else raise ParseError (opn ^ " is not a binary operation"))
289
290
291
292
        end
    (* Conversion operations *)
    | [Word opn, Type tys, SSA opnd] =>
        if exists (fn x => x = opn) conv_ops then
293
294
          let val (t1', t2') = two_tys tys in mk_assign(opn,
            ir_ap("ConvOp", [
295
              mk_return(mk_thy_const{Thy="uvmTypes", Name=opn, Ty=``:convtype``}),
296
              t1', t2', ssa_var env opnd
297
            ], ty_expr))
298
299
300
301
302
303
304
305
306
307
308
309
          end
        else raise ParseError (opn ^ " is not a conversion operation")
    | Word opn::_ =>
        if exists (fn x => x = opn) insts then
          raise ParseError ("invalid arguments for " ^ opn)
        else if exists (fn x => x = opn) terminsts then
          raise ParseError (opn ^ " can only be used in terminating position")
        else
          raise ParseError (opn ^ " is not an instruction")
    | _ => raise ParseError "expected instruction"
    end

310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
  fun parse_comminst (env : env_context)
                     (name : string)
                     (tokens : uir_token list)
                     : (term * uir_token list) =
    let
      fun fsig (SSA (Global, v)) = #get_funcsig env v
        | fsig _ = raise ParseError "expected global SSA variable in <[]>"
      fun arg (SSA v) = ssa_var env v
        | arg _ = raise ParseError "expected SSA variable in ()"
      val (flags, t1) =
        case tokens of Brackets xs::t1 => (xs, t1) | _ => ([], tokens)
      val (types, t2) =
        case t1 of
          Type [Brackets _]::_ => ([], t1)
        | Type xs::t2 => (parse_type_list env xs, t2)
        | _ => ([], t1)
      val (fsigs, t3) =
        case t2 of Type [Brackets xs]::t3 => (map fsig xs, t3) | _ => ([], t2)
      val (args, t4) =
        case t3 of Parens xs::t4 => (map arg xs, t4) | _ => ([], t3)
    in ((
      case (name, flags, types, fsigs, args) of
        ("uvm.new_stack", [], [], [s], [f]) => ir_ap("NewStack", [s, f], ty_ci)
      | ("uvm.current_stack", [], [], [], []) =>
          mk_return(mk_const("CurrentStack", ty_ci))
      | _ =>
        if exists (fn x => x = name) comminsts then
          raise ParseError ("invalid arguments for " ^ name)
        else
          raise ParseError ("unsupported common instruction: " ^ name)),
      t4)
    end

343
344
345
346
347
  (* Parses a list of tokens into a Mu IR terminating instruction. Returns a
     term of type ``:ssavar terminst or_error``.
  *)
  fun parse_terminst (env : env_context) (tokens : uir_token list) : term =
    let
348
      fun param (SSA v) = ssa_var env v
349
350
351
        | param _ = raise ParseError "expected SSA variable"
      fun params vs = mk_sequence(map param vs, or_const ty_ssa)
      val ty_dest = ``:ssavar destination``
352
      val ty_destopt = mk_type("option", [ty_dest])
353
      val x = mk_var("x", ty_list (or_const ty_ssa))
354
355
356
      fun dest label vs = mk_lift(
        mk_abs(x, mk_pair(infer_comb("BlockLabel",
          [fromMLstring label], ty_blabel), x)),
357
        params vs)
358
      fun calldata(fsig, callee, args) =
359
        let val fsig' = parse_funcsig env fsig in
360
361
        lift_record(mk_type("calldata", [ty_ssa]), [
          ("name", mk_bind(
362
            ssa_var env callee,
363
364
            mk_const("get_callee",
              or_const ty_ssa --> or_error (mk_sum(ty_ssa, ty_funcn))))),
365
          ("signature", fsig'),
366
367
368
369
          ("args", params args),
          ("convention",
              mk_return(mk_const("Mu", mk_type("callconvention", []))))
        ])
370
        end
371
372
373
      fun exc_clause [SSA (Local, l1), Parens a1, SSA (Local, l2), Parens a2] =
            lift_record(mk_type("resumption_data", [ty_ssa]), [
              ("normal_dest", dest l1 a1),
374
              ("exceptional_dest", mk_lift(
375
376
377
378
379
380
                mk_const("SOME", ty_dest --> ty_destopt), dest l2 a2))
            ])
        | exc_clause [SSA (Local, l1), Parens a1] =
            lift_record(mk_type("resumption_data", [ty_ssa]), [
              ("normal_dest", dest l1 a1),
              ("exceptional_dest", mk_return(mk_const("NONE", ty_destopt)))
381
382
383
384
385
            ])
        | exc_clause _ = raise ParseError "invalid syntax for EXC clause"
      val ty_inst = mk_type("terminst", [ty_ssa])
    in case tokens of
      [Word "RET", Parens vs] => ir_ap("Ret", [params vs], ty_inst)
Adam Nelson's avatar
Adam Nelson committed
386
    | [Word "THROW", v] => ir_ap("Throw", [param v], ty_inst)
387
388
    | [Word "CALL", Type _, SSA _, Parens _] =>
        raise ParseError "terminating CALL must have an EXC clause"
389
390
    | [_, Eq, Word "CALL", Type _, SSA _, Parens _] =>
        raise ParseError "terminating CALL must have an EXC clause"
391
    | [Word "CALL", Type fsig, SSA callee, Parens args, Word "EXC", Parens exc] =>
392
393
394
395
396
397
398
399
400
        ir_ap("Call", [
          mk_return(mk_list([], ty_ssa)),
          calldata(fsig, callee, args),
          exc_clause exc], ty_inst)
    | [lhs, Eq, Word "CALL", Type fsig, SSA callee, Parens args, Word "EXC", Parens exc] =>
        ir_ap("Call", [
          mk_return(lhs_n lhs "CALL"),
          calldata(fsig, callee, args),
          exc_clause exc], ty_inst)
401
402
403
404
405
406
407
408
409
410
    | [Word "TAILCALL", Type fsig, SSA callee, Parens args] =>
        ir_ap("TailCall", [calldata(fsig, callee, args)], ty_inst)
    | [Word "BRANCH", SSA (Local, label), Parens vs] =>
        ir_ap("Branch1", [dest label vs], ty_inst)
    | [Word "BRANCH2", SSA cond,
          SSA (Local, l1), Parens a1, SSA (Local, l2), Parens a2] =>
        let val ty_int1 = mk_return(mk_comb(
                  mk_const("Int", ty_num --> ty_type),
                  lift_num ty_num Arbnum.one))
        in ir_ap("Branch2",
411
            [ssa_var env cond, dest l1 a1, dest l2 a2],
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
            ty_inst)
        end
    | Word "SWITCH"::_ =>
        (* TODO: SWITCH *)
        raise ParseError "SWITCH is not yet implemented"
    | Word "TRAP"::_ =>
        (* TODO: TRAP *)
        raise ParseError "TRAP is not yet implemented"
    | Word "WATCHPOINT"::_ =>
        (* TODO: WATCHPOINT *)
        raise ParseError "WATCHPOINT is not yet implemented"
    | Word "WPBRANCH"::_ =>
        (* TODO: WPBRANCH *)
        raise ParseError "WPBRANCH is not yet implemented"
    | Word "SWAPSTACK"::_ =>
        (* TODO: SWAPSTACK *)
        raise ParseError "SWAPSTACK is not yet implemented"
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
    | Word "COMMINST"::SSA (Global, name)::args =>
        let val (ci, rest) = parse_comminst env name args in
          case rest of
            [Word "EXC", Parens exc] => ir_ap("CommInst",
              [mk_return(mk_list([], ty_ssa)), ci, exc_clause exc],
              ty_inst)
          | _ => raise ParseError "terminating COMMINST must have an EXC clause"
        end
    | lhs::Eq::Word "COMMINST"::SSA (Global, name)::args =>
        let val (ci, rest) = parse_comminst env name args in
          case rest of
            [Word "EXC", Parens exc] => ir_ap("CommInst",
              [mk_return(lhs_n lhs "COMMINST"), ci, exc_clause exc],
              ty_inst)
          | _ => raise ParseError "terminating COMMINST must have an EXC clause"
        end
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
    | _::Eq::_ =>
        raise ParseError "assignment is not valid in terminating position"
    | Word opn::_ =>
        if exists (fn x => x = opn) terminsts then
          raise ParseError ("invalid arguments for " ^ opn)
        else if exists (fn x => x = opn) insts then
          raise ParseError (opn ^ " is not a terminating instruction")
        else
          raise ParseError (opn ^ " is not an instruction")
    | _ => raise ParseError "expected terminating instruction"
    end

  fun parse_block (env : env_context) (lines : uir_token list list) : string * term =
    let
      val (header::all_insts) = filter (fn l => l <> []) lines
      val inst_lines = List.take(all_insts, length all_insts - 1)
      val terminst_line = List.last all_insts
      val x = mk_var("x", ty_type)
      fun get_args (Type t::SSA (Local, v)::rest) accum =
            get_args rest (
              mk_lift(mk_abs(x, mk_pair(mk_ssa v, x)), parse_type env t)::accum)
466
        | get_args [] accum = List.rev accum
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
        | get_args _ _ = raise ParseError "expected <type> %arg in block args"
      val inst_ty = mk_type("instruction", [ty_ssa])
    in case header of
      [SSA (Local, label), Parens arg_tokens, Colon] =>
        (label, lift_record(mk_type("bblock", [ty_ssa]), [
          ("args",
              mk_sequence(get_args arg_tokens [], mk_prod(ty_ssa, ty_type))),
          ("body",
              mk_sequence(map (parse_inst env) inst_lines, inst_ty)),
          ("exit", parse_terminst env terminst_line),
          ("keepalives", mk_return(mk_list([], ty_ssa)))
        ]))
    | _ => raise ParseError "expected block header"
    end

  fun parse_func (env : env_context) (fsig : term) (lines : uir_token list list) : term =
    let
      val block_tokens = split_by_header (fn l => List.last l = Colon)
                                         (filter (fn l => l <> []) lines)
      val ty_bb = mk_type("bblock", [ty_ssa])
      val ty_lb = mk_prod(ty_blabel, ty_bb)
      val ty_bbmap = mk_fmap_ty(ty_blabel, ty_bb)
      val t_b = mk_var("b", ty_bb)
      val blocks = mk_sequence(
        map (fn block => let val (l, b) = parse_block env block in mk_lift(
               mk_abs(t_b,
                 mk_pair(infer_comb("BlockLabel", [fromMLstring l], ty_blabel), t_b)),
               b)
             end)
            block_tokens,
        ty_lb)
    in
      lift_record(mk_type("function", []), [
        ("signature", fsig),
        ("entry_block", mk_lift(mk_const("FST", ty_lb --> ty_blabel),
                          mk_lift(mk_const("HD", ty_list ty_lb --> ty_lb),
                            blocks))),
        ("blocks", mk_lift(
                     infer_comb("FOLDL", [
                         mk_const("FUPDATE", ty_bbmap --> ty_lb --> ty_bbmap),
                         mk_const("FEMPTY", ty_bbmap)],
                       ty_list ty_lb --> ty_bbmap),
                      blocks))
      ])
    end

  fun uir_inst (env : env_context) (quotation : 'a frag list) : term =
    parse_inst env (tokenize (unquote_all quotation))

  fun uir_terminst (env : env_context) (quotation : 'a frag list) : term =
    parse_terminst env (tokenize (unquote_all quotation))

  fun uir_block (env : env_context) (quotation : 'a frag list) : string * term =
    let
      val str = unquote_all quotation
      val lines = map tokenize (String.tokens (fn x => x = #"\n") str)
    in parse_block env lines end

  fun uir_func (env : env_context) (fsig : term) (quotation : 'a frag list) : term =
    let
      val str = unquote_all quotation
      val lines = map tokenize (String.tokens (fn x => x = #"\n") str)
    in parse_func env fsig lines end
end