1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
From RecordUpdate Require Import RecordUpdate.
(* Test performance of a large record. Based on
https://github.com/tchajed/coq-record-update/issues/56. *)
(* 500 fields *)
Record Rec := {
field1: unit; field2: unit; field3: unit; field4: unit; field5: unit; field6: unit; field7: unit; field8: unit; field9: unit; field10: unit; field11: unit; field12: unit; field13: unit; field14: unit; field15: unit; field16: unit; field17: unit; field18: unit; field19: unit; field20: unit; field21: unit; field22: unit; field23: unit; field24: unit; field25: unit; field26: unit; field27: unit; field28: unit; field29: unit; field30: unit; field31: unit; field32: unit; field33: unit; field34: unit; field35: unit; field36: unit; field37: unit; field38: unit; field39: unit; field40: unit; field41: unit; field42: unit; field43: unit; field44: unit; field45: unit; field46: unit; field47: unit; field48: unit; field49: unit; field50: unit; field51: unit; field52: unit; field53: unit; field54: unit; field55: unit; field56: unit; field57: unit; field58: unit; field59: unit; field60: unit; field61: unit; field62: unit; field63: unit; field64: unit; field65: unit; field66: unit; field67: unit; field68: unit; field69: unit; field70: unit; field71: unit; field72: unit; field73: unit; field74: unit; field75: unit; field76: unit; field77: unit; field78: unit; field79: unit; field80: unit; field81: unit; field82: unit; field83: unit; field84: unit; field85: unit; field86: unit; field87: unit; field88: unit; field89: unit; field90: unit; field91: unit; field92: unit; field93: unit; field94: unit; field95: unit; field96: unit; field97: unit; field98: unit; field99: unit; field100: unit; field101: unit; field102: unit; field103: unit; field104: unit; field105: unit; field106: unit; field107: unit; field108: unit; field109: unit; field110: unit; field111: unit; field112: unit; field113: unit; field114: unit; field115: unit; field116: unit; field117: unit; field118: unit; field119: unit; field120: unit; field121: unit; field122: unit; field123: unit; field124: unit; field125: unit; field126: unit; field127: unit; field128: unit; field129: unit; field130: unit; field131: unit; field132: unit; field133: unit; field134: unit; field135: unit; field136: unit; field137: unit; field138: unit; field139: unit; field140: unit; field141: unit; field142: unit; field143: unit; field144: unit; field145: unit; field146: unit; field147: unit; field148: unit; field149: unit; field150: unit; field151: unit; field152: unit; field153: unit; field154: unit; field155: unit; field156: unit; field157: unit; field158: unit; field159: unit; field160: unit; field161: unit; field162: unit; field163: unit; field164: unit; field165: unit; field166: unit; field167: unit; field168: unit; field169: unit; field170: unit; field171: unit; field172: unit; field173: unit; field174: unit; field175: unit; field176: unit; field177: unit; field178: unit; field179: unit; field180: unit; field181: unit; field182: unit; field183: unit; field184: unit; field185: unit; field186: unit; field187: unit; field188: unit; field189: unit; field190: unit; field191: unit; field192: unit; field193: unit; field194: unit; field195: unit; field196: unit; field197: unit; field198: unit; field199: unit; field200: unit; field201: unit; field202: unit; field203: unit; field204: unit; field205: unit; field206: unit; field207: unit; field208: unit; field209: unit; field210: unit; field211: unit; field212: unit; field213: unit; field214: unit; field215: unit; field216: unit; field217: unit; field218: unit; field219: unit; field220: unit; field221: unit; field222: unit; field223: unit; field224: unit; field225: unit; field226: unit; field227: unit; field228: unit; field229: unit; field230: unit; field231: unit; field232: unit; field233: unit; field234: unit; field235: unit; field236: unit; field237: unit; field238: unit; field239: unit; field240: unit; field241: unit; field242: unit; field243: unit; field244: unit; field245: unit; field246: unit; field247: unit; field248: unit; field249: unit; field250: unit; field251: unit; field252: unit; field253: unit; field254: unit; field255: unit; field256: unit; field257: unit; field258: unit; field259: unit; field260: unit; field261: unit; field262: unit; field263: unit; field264: unit; field265: unit; field266: unit; field267: unit; field268: unit; field269: unit; field270: unit; field271: unit; field272: unit; field273: unit; field274: unit; field275: unit; field276: unit; field277: unit; field278: unit; field279: unit; field280: unit; field281: unit; field282: unit; field283: unit; field284: unit; field285: unit; field286: unit; field287: unit; field288: unit; field289: unit; field290: unit; field291: unit; field292: unit; field293: unit; field294: unit; field295: unit; field296: unit; field297: unit; field298: unit; field299: unit; field300: unit; field301: unit; field302: unit; field303: unit; field304: unit; field305: unit; field306: unit; field307: unit; field308: unit; field309: unit; field310: unit; field311: unit; field312: unit; field313: unit; field314: unit; field315: unit; field316: unit; field317: unit; field318: unit; field319: unit; field320: unit; field321: unit; field322: unit; field323: unit; field324: unit; field325: unit; field326: unit; field327: unit; field328: unit; field329: unit; field330: unit; field331: unit; field332: unit; field333: unit; field334: unit; field335: unit; field336: unit; field337: unit; field338: unit; field339: unit; field340: unit; field341: unit; field342: unit; field343: unit; field344: unit; field345: unit; field346: unit; field347: unit; field348: unit; field349: unit; field350: unit; field351: unit; field352: unit; field353: unit; field354: unit; field355: unit; field356: unit; field357: unit; field358: unit; field359: unit; field360: unit; field361: unit; field362: unit; field363: unit; field364: unit; field365: unit; field366: unit; field367: unit; field368: unit; field369: unit; field370: unit; field371: unit; field372: unit; field373: unit; field374: unit; field375: unit; field376: unit; field377: unit; field378: unit; field379: unit; field380: unit; field381: unit; field382: unit; field383: unit; field384: unit; field385: unit; field386: unit; field387: unit; field388: unit; field389: unit; field390: unit; field391: unit; field392: unit; field393: unit; field394: unit; field395: unit; field396: unit; field397: unit; field398: unit; field399: unit; field400: unit; field401: unit; field402: unit; field403: unit; field404: unit; field405: unit; field406: unit; field407: unit; field408: unit; field409: unit; field410: unit; field411: unit; field412: unit; field413: unit; field414: unit; field415: unit; field416: unit; field417: unit; field418: unit; field419: unit; field420: unit; field421: unit; field422: unit; field423: unit; field424: unit; field425: unit; field426: unit; field427: unit; field428: unit; field429: unit; field430: unit; field431: unit; field432: unit; field433: unit; field434: unit; field435: unit; field436: unit; field437: unit; field438: unit; field439: unit; field440: unit; field441: unit; field442: unit; field443: unit; field444: unit; field445: unit; field446: unit; field447: unit; field448: unit; field449: unit; field450: unit; field451: unit; field452: unit; field453: unit; field454: unit; field455: unit; field456: unit; field457: unit; field458: unit; field459: unit; field460: unit; field461: unit; field462: unit; field463: unit; field464: unit; field465: unit; field466: unit; field467: unit; field468: unit; field469: unit; field470: unit; field471: unit; field472: unit; field473: unit; field474: unit; field475: unit; field476: unit; field477: unit; field478: unit; field479: unit; field480: unit; field481: unit; field482: unit; field483: unit; field484: unit; field485: unit; field486: unit; field487: unit; field488: unit; field489: unit; field490: unit; field491: unit; field492: unit; field493: unit; field494: unit; field495: unit; field496: unit; field497: unit; field498: unit; field499: unit; field500: unit;
}.
(* takes ~1s on a fast laptop *)
#[export] Instance EtaRec : Settable Rec := _.
(* these should all be very fast *)
Definition do_update_middle (x: Rec) (new: unit) : Rec :=
x <| field278 := tt |>.
Definition do_update_first (x: Rec) (new: unit) : Rec :=
x <| field1 := tt |>.
Definition do_update_last (x: Rec) (new: unit) : Rec :=
x <| field500 := tt |>.
#[local] Instance field1_wf : SetterWf field1.
Proof. apply _. Qed.
|
