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.

BundleParser.sml 8.68 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
structure BundleParser :> BundleParser =
struct
  open HolKernel TypeBase Parse Term UIRLexer 
  open boolLib
  open finite_mapSyntax
  open listSyntax
  open pairSyntax
  open stringSyntax
  open sumSyntax
  open uvmErrorsTheory
  open uvmIRTheory
  open ParserHelpers
  open TypeParser
  open ValueParser
  open CodeParser

  val decls : string list = [
    "typedef", "const", "global", "funcsig", "funcdecl", "funcdef"
  ]

  val ty_env = mk_type("environment", [])
  val ty_bundle = ty_env --> or_error ty_env

24
  val ty_gln = mk_type("global_name", [])
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
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
  val ty_tyn = mk_type("type_name", [])
  val ty_sign = mk_type("sig_name", [])
  val ty_constn = mk_type("const_name", [])

  val t_env = mk_var("env", ty_env)

  (* Attempts to look up a member of one of the finite map fields of an
     ``:environment``. Assumes that t_env is already present in the current
     scope. Returns a term of type ``:^vty or_error``.
  *)
  fun get_env_member (field_name : string)
                     (kty : hol_type)
                     (vty : hol_type)
                     (key : term) : term =
    infer_comb("expect", [
      infer_comb("FLOOKUP", [
        infer_comb("environment_" ^ field_name, [t_env], mk_fmap_ty(kty, vty)),
        key
      ], mk_type("option", [vty])),
      infer_comb("InvalidIR",
        (* TODO: Include key in error message *)
        [fromMLstring (field_name ^ " lookup failed")],
        ty_err)
    ], or_error vty)

  fun get_env_type (name : string) : term =
    get_env_member "types" ty_tyn ty_type
      (infer_comb("TypeName", [fromMLstring name], ty_tyn))

  fun get_env_funcsig (name : string) : term =
    get_env_member "funcsigs" ty_sign ty_sig
      (infer_comb("SigName", [fromMLstring name], ty_sign))

  fun get_env_const (name : string) : term =
    mk_lift(
      mk_thy_const{Thy="pair", Name="SND", Ty=mk_prod(ty_type, ty_val) --> ty_val},
      get_env_member "constants" ty_constn (mk_prod(ty_type, ty_val))
        (infer_comb("ConstName", [fromMLstring name], ty_constn)))

  fun add_env_member (field_name : string)
                     (kty : hol_type)
                     (vty : hol_type)
                     (key : term)
                     (value : term) : term =
    let val t_f = mk_var("f", mk_fmap_ty(kty, vty)) in
      infer_comb("environment_" ^ field_name ^ "_fupd", [
        mk_abs(t_f,
          infer_comb("FUPDATE", [t_f, mk_pair(key, value)], mk_fmap_ty(kty, vty))),
        t_env
      ], ty_env)
    end

  fun add_env_type (name : string) (t : term) : term =
    add_env_member "types" ty_tyn ty_type
      (infer_comb("TypeName", [fromMLstring name], ty_tyn)) t

  fun add_env_funcsig (name : string) (s : term) : term =
    add_env_member "funcsigs" ty_sign ty_sig
      (infer_comb("SigName", [fromMLstring name], ty_sign)) s

  fun add_env_const (name : string) (ty : term) (value : term) : term =
    add_env_member "constants" ty_constn (mk_prod(ty_type, ty_val))
      (infer_comb("ConstName", [fromMLstring name], ty_constn)) (mk_pair(ty, value))

  val free_env_context = {
    get_type = get_env_type,
    get_funcsig = get_env_funcsig,
    get_global = get_env_const
  }

95
96
97
98
99
100
101
102
103
104
105
106
107
  type bundle = {
    types : term list,
    globals : term list,
    functions : term list
  }

  val empty_bundle : bundle = {
    types = [], globals = [], functions = []
  }

  fun parse_decl (lines : uir_token list list,
                  {types, globals, functions} : bundle)
                 : bundle =
108
109
110
    let
      val env = free_env_context
      val (header::other_lines) = filter (fn l => l <> []) lines
111
    in
112
113
114
      case header of
        Decl "typedef"::SSA (Global, name)::Eq::rhs =>
          if other_lines = [] then
115
116
117
118
119
120
            let
              val ty = mk_var("ty", ty_type)
              val def = mk_abs(t_env,
                mk_lift(mk_abs(ty, add_env_type name ty), parse_type env rhs))
            in
              {types = types @ [def], globals = globals, functions = functions}
121
122
123
124
            end
          else raise ParseError "non-declaration line after .typedef"
      | Decl "funcsig"::SSA (Global, name)::Eq::rhs =>
          if other_lines = [] then
125
126
127
128
129
130
            let
              val fs = mk_var("fs", ty_sig)
              val def = mk_abs(t_env,
                mk_lift(mk_abs(fs, add_env_funcsig name fs), parse_funcsig env rhs))
            in
              {types = types @ [def], globals = globals, functions = functions}
131
132
133
134
135
136
137
138
            end
          else raise ParseError "non-declaration line after .funcsig"
      | Decl "const"::SSA (Global, name)::Type ty::Eq::rhs =>
          (* TODO: Support multi-line constants (for structs, arrays, etc.) *)
          if other_lines = [] then
            let
              val ty' = mk_var("ty'", ty_type)
              val const = mk_var("const", ty_val)
139
140
141
142
143
              val def = mk_abs(t_env, 
                mk_bind(parse_type env ty,
                  mk_abs(ty', mk_lift(
                    mk_abs(const, add_env_const name ty' const),
                    beta_conv(mk_comb(parse_value rhs, ty'))))))
144
            in
145
              {types = types, globals = globals @ [def], functions = functions}
146
147
            end
          else raise ParseError "non-declaration line after .const"
148
149
150
      | [Decl "global", SSA (Global, name), Type ty] =>
          let
            val t_ty  = mk_var("ty", ty_type)
151
            val t_gln = infer_comb("Global", [fromMLstring name], ty_gln)
152
153
            val ty_gl = mk_prod(ty_gln, ty_type)
            val t_gls = mk_var("gls", ty_list ty_gl)
154
            val def = mk_abs(t_env, mk_lift(
155
156
157
158
159
              mk_abs(t_ty, 
                infer_comb("environment_globals_fupd", [
                  mk_abs(t_gls, infer_comb("CONS",
                    [mk_pair(t_gln, t_ty), t_gls], ty_list ty_gl)),
                  add_env_const name t_ty (infer_comb("RefV",
160
                    [t_ty, mk_some(infer_comb("GlobalAddr", [t_gln], ty_addr))], ty_val))
161
                ], ty_env)),
162
163
164
              parse_type env ty))
          in
            {types = types, globals = globals @ [def], functions = functions}
165
          end
166
167
168
169
170
171
      | [Decl "funcdecl", SSA (Global, name), Type fsig] =>
          (* TODO: funcdecl *)
          raise ParseError "funcdecl not yet supported"
      | [Decl "funcdef", SSA (Global, name), Word "VERSION", SSA (Local, v), Type fsig, OpenBrace] =>
          if exists (fn l => l = [CloseBrace]) other_lines then
            if List.last other_lines = [CloseBrace] then
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
              let
                val r = mk_const("REF", mk_type("ref_type", []))
                val ty_fno = mk_type("option", [ty_funcn])
                val fsig' = parse_funcsig env fsig
                val ty = mk_var("ty", ty_type)
                val fr = mk_var("fr", ty_val)
                val fref = mk_abs(t_env, list_mk_lift(
                  list_mk_abs([ty, fr], add_env_const name ty fr), [
                    mk_lift(infer_comb("FuncRef", [r], ty_sig --> ty_type), fsig'),
                    list_mk_lift(
                      infer_comb("FuncRefV", [r], ty_sig --> ty_fno --> ty_val), [fsig',
                        mk_return(infer_comb("SOME", [
                          infer_comb("Func", [fromMLstring name], ty_funcn)], ty_fno))])]))
                val fdef = mk_abs(t_env, mk_lift(
                  infer_comb("generate_function", [t_env, fromMLstring name],
                    mk_type("function", []) --> ty_env),
                  parse_func env fsig' (List.take(other_lines, length other_lines - 1))))
              in
                {types = types, globals = globals @ [fref], functions = functions @ [fdef]}
              end
192
193
194
195
196
197
198
199
            else raise ParseError "non-declaration line after .funcdef's }"
          else raise ParseError "unclosed { in .funcdef"
      | Decl d::_ =>
          if exists (fn x => x = d) decls then
            raise ParseError ("invalid parameters for ." ^ d)
          else
            raise ParseError ("." ^ d ^ " is not a toplevel declaration")
      | _ =>
200
          raise ParseError "expected toplevel declaration"
201
202
203
204
205
206
207
208
209
    end

  fun uir_bundle (quotation : 'a frag list) : term =
    let
      val ty_bind = or_error ty_env --> ty_bundle --> or_error ty_env
      val str = unquote_all quotation
      val lines = map tokenize (String.tokens (fn x => x = #"\n") str)
      val decl_blocks = split_by_header (fn (Decl _::_) => true | _ => false)
        (filter (fn l => l <> []) lines)
210
211
      val {types, globals, functions} =
        foldl parse_decl empty_bundle decl_blocks
212
213
214
215
216
217
218
219
220
    in
      mk_abs(t_env, list_mk_comb(
        mk_thy_const{
          Thy="list",
          Name="FOLDL",
          Ty=ty_bind --> or_error ty_env --> ty_list ty_bundle --> or_error ty_env
        }, [
          mk_thy_const{Thy="sumMonad", Name="bind_left", Ty=ty_bind},
          mk_return t_env,
221
          mk_list(types @ globals @ functions, ty_bundle)
222
223
224
225
        ]))
    end
end