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.

ParserHelpers.sml 4.55 KB
Newer Older
1
2
structure ParserHelpers :> ParserHelpers =
struct
Adam R. Nelson's avatar
Adam R. Nelson committed
3
4
5
6
7
8
9
10
  open HolKernel Term Parse TypeBase
  open sumSyntax
  open listSyntax
  open sumMonadTheory
  open uvmTypesTheory
  open uvmErrorsTheory
  open uvmValuesTheory
  open uvmMemoryTheory
11
12
13
14
15
16
17
18
19
20

  exception ParseError of string
  type env_context = {
    get_type: string -> term,
    get_funcsig: string -> term,
    get_global: string -> term
  }

  val mock_context = {
    get_type = fn _ => ``ARB``,
21
22
23
24
    get_funcsig = fn name =>
      case name of
        "sig" => ``OK (<| arg_types := []; return_types := [] |>): funcsig or_error``
      | _ => ``ARB``,
25
26
27
28
29
    get_global = fn _ => ``ARB``
  }
  
  val ty_num = mk_type("num", [])
  val ty_str = ``:string``
Adam R. Nelson's avatar
Adam R. Nelson committed
30
31
32
33
34
  val ty_type = mk_type("uvm_type", [])
  val ty_reft = mk_type("ref_type", [])
  val ty_sig  = mk_type("funcsig", [])
  val ty_addr = mk_type("addr", [])
  val ty_funcn = mk_type("func_name", [])
35
36
  val ty_sid = mk_type("stack_id", [])
  val ty_tid = mk_type("thread_id", [])
Adam R. Nelson's avatar
Adam R. Nelson committed
37
38
  val ty_iaddr = mk_type("gen_iaddr", [ty_addr])
  val ty_err = mk_type("gen_uvm_error", [ty_addr, ty_funcn])
39
  val ty_val = mk_type("gen_value", [ty_addr, ty_funcn, ty_sid, ty_tid])
40
  fun ty_list ty = mk_type("list", [ty])
Adam R. Nelson's avatar
Adam R. Nelson committed
41
  fun or_error ty = sumSyntax.mk_sum(ty, ty_err)
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
  
  fun infer_comb(name : string, args : term list, out_ty : hol_type) =
    let
      val ty = foldr (op -->) out_ty (map type_of args)
      val f = mk_const(name, ty) handle HOL_ERR err => (
        print ("\nTYPE ERROR for " ^ name);
        print ("\nInvalid type: " ^ type_to_string ty);
        print "\nArgs:";
        List.app (fn t => print ("\n -  " ^ term_to_string t)) args;
        print "\n";
        raise HOL_ERR {
          message="Function " ^ name ^ " is not of type " ^ type_to_string ty,
          origin_function="infer_comb",
          origin_structure="ParseUIR"
        })
    in list_mk_comb(f, args) end

59
60
61
62
  fun mk_some x =
    let val ty = type_of x
    in mk_comb(mk_const("SOME", ty --> mk_type("option", [ty])), x) end

63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
  fun mk_return t = infer_comb("INL", [t], or_error (type_of t))

  fun mk_bind(lhs, rhs) =
    let val (_, ty_out) = strip_fun (type_of rhs) in
      infer_comb("bind_left", [lhs, rhs], ty_out)
    end

  fun mk_sequence(xs, ty) =
    infer_comb("sequence_left", [mk_list(xs, or_error ty)], or_error (ty_list ty))

  local open List in
    fun mk_lift(f, x) =
      let
        val (ty_f_init, ty_f_last) = strip_fun(type_of f)
        val ty_out = foldr (op -->) ty_f_last (drop(ty_f_init, 1))
      in
        infer_comb("lift_left", [f, x], or_error ty_out)
      end

    fun list_mk_lift(f, (x::ys)) =
          let val (ty_ins, ty_out) = strip_fun (type_of f) in
            foldl
              (fn ((arg, ty), acc) => list_mk_comb(
                mk_thy_const{
                  Thy="sumMonad",
                  Name="ap_left",
                  Ty=type_of acc --> type_of arg --> or_error ty
                }, [acc, arg]))
              (mk_lift(f, x))
              (tabulate(length ys, fn n => (
                nth(ys, n),
                foldr (op -->) ty_out (drop(ty_ins, n+2)))))
          end
      | list_mk_lift(f, []) = mk_return f

    fun lift_record(ty : hol_type, fields : (string * term) list) =
      let
        val vs = map (fn (s, t) => mk_var(s, #1 (sumSyntax.dest_sum (type_of t)))) fields
      in
        list_mk_lift(
          list_mk_abs(vs, mk_record(ty, tabulate(length fields,
            fn n => (#1 (nth(fields, n)), nth(vs, n))))),
          map #2 fields)
      end
  end

Adam R. Nelson's avatar
Adam R. Nelson committed
109
110
111
112
113
  fun ty_pat (name : string) (xs : term list) =
    list_mk_comb(mk_thy_const{
      Thy="uvmTypes", Name=name, Ty=foldr (op -->) ty_type (map type_of xs)
    }, xs)

114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
  (* Converts a QUOTE into a string, removing the leading location comment *)
  fun unquote (QUOTE str) = (
        case CharVector.findi (fn (_, c) => c = #")") str of
          SOME (i, _) => String.extract(str, i + 1, NONE)
        | NONE => str)
    | unquote (ANTIQUOTE _) = raise ParseError "antiquote not supported"

  (* Unquotes and concatenates a list of QUOTEs. *)
  fun unquote_all (quotes : 'a frag list) : string =
    String.concat (map unquote quotes)

  exception StartsWithNonHeader

  fun split_by_header (is_header : 'a -> bool) (xs : 'a list) : 'a list list =
    let
      fun split_fold ((next, (acc, out)) : 'a * ('a list * 'a list list))
                     : 'a list * 'a list list =
        if is_header next then ([], (next::acc)::out) else (next::acc, out)
      val (remaining : 'a list, out : 'a list list) =
        List.foldr split_fold ([], []) xs
    in
      case remaining of [] => out | _ => raise StartsWithNonHeader
    end
end