Lines Matching refs:params
1152 def emit_named(name, params, string):
1154 # params.names
1156 if(name in params.names):
1157 print(string, file=params.output)
1158 print(file=params.output)
1161 def emit_named_ptr_proof(fn_name, params, name, type_map, toptps, prf_prefix, substs):
1171 emit_named(fn_name, params, make_proof(prf_prefix + '_direct', substs, params.sorry))
1182 emit_named(fn_name, params, make_proof(prf_prefix + '_path', substs, params.sorry))
1220 def resolve(self, params, symtab):
1223 self.make_classes(params)
1280 def generate_hol_proofs(self, params, type_map):
1281 output = params.output
1295 substs, params.sorry), file=output)
1299 substs, params.sorry), file=output)
1303 substs, params.sorry), file=output)
1316 if not params.skip_modifies:
1317 emit_named("%(name)s_get_%(tagname)s" % substs, params,
1322 params.sorry))
1323 emit_named("%(name)s_ptr_get_%(tagname)s" % substs, params,
1328 params.sorry))
1330 emit_named("%s_get_%s" % (self.name, self.tagname), params,
1331 make_proof('get_tag_spec', substs, params.sorry))
1333 emit_named("%s_%s_equals" % (self.name, self.tagname), params,
1334 make_proof('get_tag_equals_spec', substs, params.sorry))
1337 emit_named_ptr_proof("%s_ptr_get_%s" % (self.name, self.tagname), params, self.name,
1338 type_map, params.toplevel_types,
1348 if not params.skip_modifies:
1349 emit_named("%s_%s_new" % (self.name, ref.name), params,
1356 params.sorry))
1358 emit_named("%s_%s_ptr_new" % (self.name, ref.name), params,
1365 params.sorry))
1369 emit_named("%s_%s_new" % (self.name, ref.name), params,
1373 params.sorry))
1375 emit_named_ptr_proof("%s_%s_ptr_new" % (self.name, ref.name), params, self.name,
1376 type_map, params.toplevel_types,
1395 emit_named("%s_%s_new" % (self.name, ref.name), params,
1401 params.sorry))
1403 emit_named_ptr_proof("%s_%s_ptr_new" % (self.name, ref.name), params, self.name,
1404 type_map, params.toplevel_types,
1436 if not params.skip_modifies:
1438 params,
1445 params.sorry))
1448 params,
1455 params.sorry))
1459 params,
1460 make_proof('union_get_spec', substs, params.sorry))
1463 if not params.skip_modifies:
1465 params,
1473 params.sorry))
1476 params,
1483 params.sorry))
1487 params,
1488 make_proof('union_set_spec', substs, params.sorry))
1492 params, self.name, type_map, params.toplevel_types,
1497 params, self.name, type_map, params.toplevel_types,
1500 def generate_hol_defs(self, params):
1501 output = params.output
1515 if ref.generate_hol_defs(params, \
1643 params.sorry)
1679 def generate(self, params):
1680 output = params.output
1724 emit_named("%s_get_%s" % (self.name, self.tagname), params, fs)
1740 emit_named("%s_%s_equals" % (self.name, self.tagname), params, fs)
1756 emit_named("%s_ptr_get_%s" % (self.name, self.tagname), params, fs)
1836 emit_named("%s_%s_new" % (self.name, name), params, generator)
1837 emit_named("%s_%s_ptr_new" % (self.name, name), params, ptr_generator)
1889 params, union_reader_template % subs)
1893 params, union_writer_template % subs)
1897 params, ptr_union_reader_template % subs)
1901 params, ptr_union_writer_template % subs)
1988 def make_classes(self, params):
2095 if params.showclasses:
2157 def generate_hol_defs(self, params, suppressed_field=None, \
2159 output = params.output
2226 def generate_hol_proofs(self, params, type_map):
2227 output = params.output
2243 substs, params.sorry), file=output)
2247 substs, params.sorry), file=output)
2251 substs, params.sorry), file=output)
2263 if not params.skip_modifies:
2264 emit_named("%s_new" % self.name, params,
2270 params.sorry))
2282 emit_named("%s_new" % self.name, params,
2287 params.sorry))
2289 emit_named_ptr_proof("%s_ptr_new" % self.name, params, self.name,
2290 type_map, params.toplevel_types,
2308 if not params.skip_modifies:
2310 emit_named("%s_get_%s" % (self.name, field), params,
2316 params.sorry))
2319 emit_named("%s_ptr_get_%s" % (self.name, field), params,
2325 params.sorry))
2329 emit_named("%s_get_%s" % (self.name, field), params,
2330 make_proof('get_spec', substs, params.sorry))
2332 if not params.skip_modifies:
2334 emit_named("%s_set_%s" % (self.name, field), params,
2341 params.sorry))
2343 emit_named("%s_ptr_set_%s" % (self.name, field), params,
2349 params.sorry))
2353 emit_named("%s_set_%s" % (self.name, field), params,
2354 make_proof('set_spec', substs, params.sorry))
2356 emit_named_ptr_proof("%s_ptr_get_%s" % (self.name, field), params, self.name,
2357 type_map, params.toplevel_types,
2359 emit_named_ptr_proof("%s_ptr_set_%s" % (self.name, field), params, self.name,
2360 type_map, params.toplevel_types,
2363 def generate(self, params):
2364 output = params.output
2445 emit_named("%s_new" % self.name, params, generator)
2446 emit_named("%s_ptr_new" % self.name, params, ptr_generator)
2488 emit_named("%s_get_%s" % (self.name, field), params,
2492 emit_named("%s_set_%s" % (self.name, field), params,
2496 emit_named("%s_ptr_get_%s" % (self.name, field), params,
2500 emit_named("%s_ptr_set_%s" % (self.name, field), params,
2575 params = {}