-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathReferences.html
2671 lines (2331 loc) · 474 KB
/
References.html
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
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
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
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
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
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>References: Typing Mutable References</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<div id="page">
<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
<li class='section_name'><a href='toc.html'>Table of Contents</a></li>
<li class='section_name'><a href='coqindex.html'>Index</a></li>
<li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>
<div id="main">
<h1 class="libtitle">References<span class="subtitle">Typing Mutable References</span></h1>
<div class="doc">
<div class="paragraph"> </div>
Up to this point, we have considered a variety of <i>pure</i>
language features, including functional abstraction, basic types
such as numbers and booleans, and structured types such as records
and variants. These features form the backbone of most
programming languages -- including purely functional languages
such as Haskell and "mostly functional" languages such as ML, as
well as imperative languages such as C and object-oriented
languages such as Java, C<span class="inlinecode">#</span>, and Scala.
<div class="paragraph"> </div>
However, most practical languages also include various <i>impure</i>
features that cannot be described in the simple semantic framework
we have used so far. In particular, besides just yielding
results, computation in these languages may assign to mutable
variables (reference cells, arrays, mutable record fields, etc.);
perform input and output to files, displays, or network
connections; make non-local transfers of control via exceptions,
jumps, or continuations; engage in inter-process synchronization
and communication; and so on. In the literature on programming
languages, such "side effects" of computation are collectively
referred to as <i>computational effects</i>.
<div class="paragraph"> </div>
In this chapter, we'll see how one sort of computational effect --
mutable references -- can be added to the calculi we have studied.
The main extension will be dealing explicitly with a <i>store</i> (or
<i>heap</i>) and <i>pointers</i> that name store locations. This extension
is fairly straightforward to define; the most interesting part is
the refinement we need to make to the statement of the type
preservation theorem.
</div>
<div class="code">
<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing,-deprecated-hint-without-locality".<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-deprecated-syntactic-definition".<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#"><span class="id" title="library">Strings.String</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#"><span class="id" title="library">Init.Nat</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.Arith.html#"><span class="id" title="library">Arith.Arith</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.PeanoNat.html#"><span class="id" title="library">Arith.PeanoNat</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.micromega.Lia.html#"><span class="id" title="library">Lia</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Maps</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Smallstep.html#"><span class="id" title="library">Smallstep</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#"><span class="id" title="library">Lists.List</span></a>. <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#"><span class="id" title="module">Datatypes</span></a>.<br/>
<span class="id" title="keyword">Check</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#length"><span class="id" title="definition">length</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.PeanoNat.html#Nat"><span class="id" title="module">Nat</span></a>.<br/>
</div>
<div class="doc">
<a id="lab414"></a><h1 class="section">Definitions</h1>
<div class="paragraph"> </div>
Pretty much every programming language provides some form of
assignment operation that changes the contents of a previously
allocated piece of storage. (Coq's internal language Gallina is a
rare exception!)
<div class="paragraph"> </div>
In some languages -- notably ML and its relatives -- the
mechanisms for name-binding and those for assignment are kept
separate. We can have a variable <span class="inlinecode"><span class="id" title="var">x</span></span> whose <i>value</i> is the number
<span class="inlinecode">5</span>, or we can have a variable <span class="inlinecode"><span class="id" title="var">y</span></span> whose value is a
<i>reference</i> (or <i>pointer</i>) to a mutable cell whose current
contents is <span class="inlinecode">5</span>. These are different things, and the difference
is visible to the programmer. We can add <span class="inlinecode"><span class="id" title="var">x</span></span> to another number,
but not assign to it. We can use <span class="inlinecode"><span class="id" title="var">y</span></span> to assign a new value to the
cell that it points to (by writing <span class="inlinecode"><span class="id" title="var">y</span>:=84</span>), but we cannot use <span class="inlinecode"><span class="id" title="var">y</span></span>
directly as an argument to an operation like <span class="inlinecode">+</span>. Instead, we
must explicitly <i>dereference</i> it, writing <span class="inlinecode">!<span class="id" title="var">y</span></span> to obtain its
current contents.
<div class="paragraph"> </div>
In most other languages -- in particular, in all members of the C
family, including Java -- <i>every</i> variable name refers to a
mutable cell, and the operation of dereferencing a variable to
obtain its current contents is implicit.
<div class="paragraph"> </div>
For purposes of formal study, it is useful to keep these
mechanisms separate. The development in this chapter will closely
follow ML's model. Applying the lessons learned here to C-like
languages is a straightforward matter of collapsing some
distinctions and rendering some operations such as dereferencing
implicit instead of explicit.
</div>
<div class="doc">
<a id="lab415"></a><h1 class="section">Syntax</h1>
<div class="paragraph"> </div>
In this chapter, we study adding mutable references to the
simply-typed lambda calculus with natural numbers.
</div>
<div class="code">
<span class="id" title="keyword">Module</span> <a id="STLCRef" class="idref" href="#STLCRef"><span class="id" title="module">STLCRef</span></a>.<br/>
</div>
<div class="doc">
The basic operations on references are <i>allocation</i>,
<i>dereferencing</i>, and <i>assignment</i>.
<div class="paragraph"> </div>
<ul class="doclist">
<li> To allocate a reference, we use the <span class="inlinecode"><span class="id" title="var">ref</span></span> operator, providing
an initial value for the new cell.
<div class="paragraph"> </div>
For example, <span class="inlinecode"><span class="id" title="var">ref</span></span> <span class="inlinecode">5</span> creates a new cell containing the value
<span class="inlinecode">5</span>, and reduces to a reference to that cell.
<div class="paragraph"> </div>
</li>
<li> To read the current value of this cell, we use the
dereferencing operator <span class="inlinecode">!</span>.
<div class="paragraph"> </div>
For example, <span class="inlinecode">!(<span class="id" title="var">ref</span></span> <span class="inlinecode">5)</span> reduces to <span class="inlinecode">5</span>.
<div class="paragraph"> </div>
</li>
<li> To change the value stored in a cell, we use the assignment
operator.
<div class="paragraph"> </div>
If <span class="inlinecode"><span class="id" title="var">r</span></span> is a reference, <span class="inlinecode"><span class="id" title="var">r</span></span> <span class="inlinecode">:=</span> <span class="inlinecode">7</span> will store the value <span class="inlinecode">7</span> in
the cell referenced by <span class="inlinecode"><span class="id" title="var">r</span></span>.
</li>
</ul>
</div>
<div class="doc">
<a id="lab416"></a><h3 class="section">Types</h3>
<div class="paragraph"> </div>
We start with the simply typed lambda calculus over the
natural numbers. Besides the base natural number type and arrow
types, we need to add two more types to deal with
references. First, we need the <i>unit type</i>, which we will use as
the result type of an assignment operation. We then add
<i>reference types</i>.
<div class="paragraph"> </div>
If <span class="inlinecode"><span class="id" title="var">T</span></span> is a type, then <span class="inlinecode"><span class="id" title="var">Ref</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> is the type of references to
cells holding values of type <span class="inlinecode"><span class="id" title="var">T</span></span>.
<br/>
<span class="inlinecode"> <span class="id" title="var">T</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" title="var">Nat</span><br/>
| <span class="id" title="var">Unit</span><br/>
| <span class="id" title="var">T</span> → <span class="id" title="var">T</span><br/>
| <span class="id" title="var">Ref</span> <span class="id" title="var">T</span>
</span>
</div>
<div class="code">
<span class="id" title="keyword">Inductive</span> <a id="STLCRef.ty" class="idref" href="#STLCRef.ty"><span class="id" title="definition, inductive"><span id="STLCRef.ty_rect" class="id"><span id="STLCRef.ty_ind" class="id"><span id="STLCRef.ty_rec" class="id"><span id="STLCRef.ty_sind" class="id">ty</span></span></span></span></span></a> : <span class="id" title="keyword">Type</span> :=<br/>
| <a id="STLCRef.Ty_Nat" class="idref" href="#STLCRef.Ty_Nat"><span class="id" title="constructor">Ty_Nat</span></a> : <a class="idref" href="References.html#ty:1"><span class="id" title="inductive">ty</span></a><br/>
| <a id="STLCRef.Ty_Unit" class="idref" href="#STLCRef.Ty_Unit"><span class="id" title="constructor">Ty_Unit</span></a> : <a class="idref" href="References.html#ty:1"><span class="id" title="inductive">ty</span></a><br/>
| <a id="STLCRef.Ty_Arrow" class="idref" href="#STLCRef.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> : <a class="idref" href="References.html#ty:1"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#ty:1"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#ty:1"><span class="id" title="inductive">ty</span></a><br/>
| <a id="STLCRef.Ty_Ref" class="idref" href="#STLCRef.Ty_Ref"><span class="id" title="constructor">Ty_Ref</span></a> : <a class="idref" href="References.html#ty:1"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#ty:1"><span class="id" title="inductive">ty</span></a>.<br/>
</div>
<div class="doc">
<a id="lab417"></a><h3 class="section">Terms</h3>
<div class="paragraph"> </div>
Besides the usual variables, abstractions, applications,
terms related to natural numbers, and <span class="inlinecode"><span class="id" title="var">unit</span></span>, we need four
more sorts of terms in order to handle mutable references:
<pre>
t <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> ... Terms
| ref t allocation
| !t dereference
| t := t assignment
| l location
</pre>
</div>
<div class="code">
<span class="id" title="keyword">Inductive</span> <a id="STLCRef.tm" class="idref" href="#STLCRef.tm"><span class="id" title="definition, inductive"><span id="STLCRef.tm_rect" class="id"><span id="STLCRef.tm_ind" class="id"><span id="STLCRef.tm_rec" class="id"><span id="STLCRef.tm_sind" class="id">tm</span></span></span></span></span></a> : <span class="id" title="keyword">Type</span> :=<br/>
<span class="comment">(* STLC with numbers: *)</span><br/>
| <a id="STLCRef.tm_var" class="idref" href="#STLCRef.tm_var"><span class="id" title="constructor">tm_var</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_app" class="idref" href="#STLCRef.tm_app"><span class="id" title="constructor">tm_app</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_abs" class="idref" href="#STLCRef.tm_abs"><span class="id" title="constructor">tm_abs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#STLCRef.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_const" class="idref" href="#STLCRef.tm_const"><span class="id" title="constructor">tm_const</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_succ" class="idref" href="#STLCRef.tm_succ"><span class="id" title="constructor">tm_succ</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_pred" class="idref" href="#STLCRef.tm_pred"><span class="id" title="constructor">tm_pred</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_mult" class="idref" href="#STLCRef.tm_mult"><span class="id" title="constructor">tm_mult</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_if<sub>0</sub>" class="idref" href="#STLCRef.tm_if<sub>0</sub>"><span class="id" title="constructor">tm_if<sub>0</sub></span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
<span class="comment">(* New terms: *)</span><br/>
| <a id="STLCRef.tm_unit" class="idref" href="#STLCRef.tm_unit"><span class="id" title="constructor">tm_unit</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_ref" class="idref" href="#STLCRef.tm_ref"><span class="id" title="constructor">tm_ref</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_deref" class="idref" href="#STLCRef.tm_deref"><span class="id" title="constructor">tm_deref</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_assign" class="idref" href="#STLCRef.tm_assign"><span class="id" title="constructor">tm_assign</span></a> : <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
| <a id="STLCRef.tm_loc" class="idref" href="#STLCRef.tm_loc"><span class="id" title="constructor">tm_loc</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="References.html#tm:3"><span class="id" title="inductive">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="var">Declare</span> <span class="id" title="var">Custom</span> <span class="id" title="var">Entry</span> <span class="id" title="var">stlc</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>" class="idref" href="#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">"</span></a><{ e }>" := <span class="id" title="var">e</span> (<span class="id" title="var">e</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="0975a85e562f22315b420c8d1c95dd<sub>06</sub>" class="idref" href="#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">"</span></a>( x )" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::x" class="idref" href="#STLCRef.:stlc::x"><span class="id" title="notation">"</span></a>x" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::x_'->'_x" class="idref" href="#STLCRef.:stlc::x_'->'_x"><span class="id" title="notation">"</span></a>S <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> T" := (<a class="idref" href="References.html#STLCRef.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> <span class="id" title="var">S</span> <span class="id" title="var">T</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::x_x" class="idref" href="#STLCRef.:stlc::x_x"><span class="id" title="notation">"</span></a>x y" := (<a class="idref" href="References.html#STLCRef.tm_app"><span class="id" title="constructor">tm_app</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="fcbb07911888b1a4b268f628a4d64735" class="idref" href="#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">"</span></a>\ x : t , y" :=<br/>
(<a class="idref" href="References.html#STLCRef.tm_abs"><span class="id" title="constructor">tm_abs</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> <span class="id" title="var">y</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
<span class="id" title="var">t</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
<span class="id" title="var">y</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="References.html#STLCRef.tm_var"><span class="id" title="constructor">tm_var</span></a> <a class="idref" href="References.html#STLCRef.tm_var"><span class="id" title="constructor">:</span></a> <a class="idref" href="References.html#STLCRef.tm_var"><span class="id" title="constructor">string</span></a> <a class="idref" href="References.html#STLCRef.tm_var"><span class="id" title="constructor">><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="References.html#STLCRef.tm_var"><span class="id" title="constructor">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="4fd5514b3ffd220ca15884061cca2343" class="idref" href="#4fd5514b3ffd220ca15884061cca2343"><span class="id" title="notation">"</span></a>{ x }" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'Unit'" class="idref" href="#STLCRef.:stlc::'Unit'"><span class="id" title="notation">"</span></a>'Unit'" :=<br/>
(<a class="idref" href="References.html#STLCRef.Ty_Unit"><span class="id" title="constructor">Ty_Unit</span></a>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'unit'" class="idref" href="#STLCRef.:stlc::'unit'"><span class="id" title="notation">"</span></a>'unit'" := <a class="idref" href="References.html#STLCRef.tm_unit"><span class="id" title="constructor">tm_unit</span></a> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'Nat'" class="idref" href="#STLCRef.:stlc::'Nat'"><span class="id" title="notation">"</span></a>'Nat'" := <a class="idref" href="References.html#STLCRef.Ty_Nat"><span class="id" title="constructor">Ty_Nat</span></a> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'succ'_x" class="idref" href="#STLCRef.:stlc::'succ'_x"><span class="id" title="notation">"</span></a>'succ' x" := (<a class="idref" href="References.html#STLCRef.tm_succ"><span class="id" title="constructor">tm_succ</span></a> <span class="id" title="var">x</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
<span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'pred'_x" class="idref" href="#STLCRef.:stlc::'pred'_x"><span class="id" title="notation">"</span></a>'pred' x" := (<a class="idref" href="References.html#STLCRef.tm_pred"><span class="id" title="constructor">tm_pred</span></a> <span class="id" title="var">x</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
<span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="aefa1df20f40a8331bf6423412f1c115" class="idref" href="#aefa1df20f40a8331bf6423412f1c115"><span class="id" title="notation">"</span></a>x * y" := (<a class="idref" href="References.html#STLCRef.tm_mult"><span class="id" title="constructor">tm_mult</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1,<br/>
<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x" class="idref" href="#STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">"</span></a>'if<sub>0</sub>' x 'then' y 'else' z" :=<br/>
(<a class="idref" href="References.html#STLCRef.tm_if<sub>0</sub>"><span class="id" title="constructor">tm_if<sub>0</sub></span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 89,<br/>
<span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
<span class="id" title="var">y</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
<span class="id" title="var">z</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="References.html#STLCRef.tm_const"><span class="id" title="constructor">tm_const</span></a> <a class="idref" href="References.html#STLCRef.tm_const"><span class="id" title="constructor">:</span></a> <a class="idref" href="References.html#STLCRef.tm_const"><span class="id" title="constructor">nat</span></a> <a class="idref" href="References.html#STLCRef.tm_const"><span class="id" title="constructor">><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="References.html#STLCRef.tm_const"><span class="id" title="constructor">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'Ref'_x" class="idref" href="#STLCRef.:stlc::'Ref'_x"><span class="id" title="notation">"</span></a>'Ref' t" :=<br/>
(<a class="idref" href="References.html#STLCRef.Ty_Ref"><span class="id" title="constructor">Ty_Ref</span></a> <span class="id" title="var">t</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 4).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'loc'_x" class="idref" href="#STLCRef.:stlc::'loc'_x"><span class="id" title="notation">"</span></a>'loc' x" := (<a class="idref" href="References.html#STLCRef.tm_loc"><span class="id" title="constructor">tm_loc</span></a> <span class="id" title="var">x</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCRef.:stlc::'ref'_x" class="idref" href="#STLCRef.:stlc::'ref'_x"><span class="id" title="notation">"</span></a>'ref' x" := (<a class="idref" href="References.html#STLCRef.tm_ref"><span class="id" title="constructor">tm_ref</span></a> <span class="id" title="var">x</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2).<br/>
<span class="id" title="keyword">Notation</span> <a id="70f28e5c58264a9753710970e9df6ba<sub>2</sub>" class="idref" href="#70f28e5c58264a9753710970e9df6ba<sub>2</sub>"><span class="id" title="notation">"</span></a>'!' x " := (<a class="idref" href="References.html#STLCRef.tm_deref"><span class="id" title="constructor">tm_deref</span></a> <span class="id" title="var">x</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2).<br/>
<span class="id" title="keyword">Notation</span> <a id="c9336c07d043872f48e6c531eccadb3e" class="idref" href="#c9336c07d043872f48e6c531eccadb3e"><span class="id" title="notation">"</span></a> e<sub>1</sub> ':=' e<sub>2</sub> " := (<a class="idref" href="References.html#STLCRef.tm_assign"><span class="id" title="constructor">tm_assign</span></a> <span class="id" title="var">e<sub>1</sub></span> <span class="id" title="var">e<sub>2</sub></span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 21).<br/>
</div>
<div class="doc">
Intuitively:
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">ref</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> (formally, <span class="inlinecode"><span class="id" title="var">ref</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span>) allocates a new reference cell
with the value <span class="inlinecode"><span class="id" title="var">t</span></span> and reduces to the location of the newly
allocated cell;
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode">!<span class="id" title="var">t</span></span> (formally, <span class="inlinecode"><span class="id" title="var">deref</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span>) reduces to the contents of the
cell referenced by <span class="inlinecode"><span class="id" title="var">t</span></span>;
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">:=</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> (formally, <span class="inlinecode"><span class="id" title="var">assign</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>) assigns <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> to the
cell referenced by <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>; and
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode"><span class="id" title="var">l</span></span> (formally, <span class="inlinecode"><span class="id" title="var">loc</span></span> <span class="inlinecode"><span class="id" title="var">l</span></span>) is a reference to the cell at
location <span class="inlinecode"><span class="id" title="var">l</span></span>. We'll discuss locations later.
</li>
</ul>
<div class="paragraph"> </div>
In informal examples, we'll also freely use the extensions
of the STLC developed in the <a href="MoreStlc.html"><span class="inlineref">MoreStlc</span></a> chapter; however, to keep
the proofs small, we won't bother formalizing them again here. (It
would be easy to do so, since there are no very interesting
interactions between those features and references.)
</div>
<div class="doc">
<a id="lab418"></a><h3 class="section">Typing (Preview)</h3>
<div class="paragraph"> </div>
Informally, the typing rules for allocation, dereferencing, and
assignment will look like this:
<center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule">Gamma <span class="nowrap">|--</span> t<sub>1</sub> ∈ T<sub>1</sub></td>
<td class="infrulenamecol" rowspan="3">
(T_Ref)
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">Gamma <span class="nowrap">|--</span> ref t<sub>1</sub> ∈ Ref T<sub>1</sub></td>
<td></td>
</tr>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule">Gamma <span class="nowrap">|--</span> t<sub>1</sub> ∈ Ref T<sub>1</sub></td>
<td class="infrulenamecol" rowspan="3">
(T_Deref)
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">Gamma <span class="nowrap">|--</span> !t<sub>1</sub> ∈ T<sub>1</sub></td>
<td></td>
</tr>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule">Gamma <span class="nowrap">|--</span> t<sub>1</sub> ∈ Ref T<sub>2</sub></td>
<td></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">Gamma <span class="nowrap">|--</span> t<sub>2</sub> ∈ T<sub>2</sub></td>
<td class="infrulenamecol" rowspan="3">
(T_Assign)
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">Gamma <span class="nowrap">|--</span> t<sub>1</sub> := t<sub>2</sub> : Unit</td>
<td></td>
</tr>
</table></center> The rule for locations will require a bit more machinery, and this
will motivate some changes to the other rules; we'll come back to
this later.
</div>
<div class="doc">
<a id="lab419"></a><h3 class="section">Values and Substitution</h3>
<div class="paragraph"> </div>
Besides abstractions, numbers, and the unit value, we have one new
type of value: locations.
</div>
<div class="code">
<span class="id" title="keyword">Inductive</span> <a id="STLCRef.value" class="idref" href="#STLCRef.value"><span class="id" title="definition, inductive"><span id="STLCRef.value_ind" class="id"><span id="STLCRef.value_sind" class="id">value</span></span></span></a> : <a class="idref" href="References.html#STLCRef.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
| <a id="STLCRef.v_abs" class="idref" href="#STLCRef.v_abs"><span class="id" title="constructor">v_abs</span></a> : <span class="id" title="keyword">∀</span> <a id="x:7" class="idref" href="#x:7"><span class="id" title="binder">x</span></a> <a id="T<sub>2</sub>:8" class="idref" href="#T<sub>2</sub>:8"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="t<sub>1</sub>:9" class="idref" href="#t<sub>1</sub>:9"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
<a class="idref" href="References.html#value:5"><span class="id" title="inductive">value</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">\</span></a><a class="idref" href="References.html#x:7"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">:</span></a><a class="idref" href="References.html#T<sub>2</sub>:8"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">,</span></a> <a class="idref" href="References.html#t<sub>1</sub>:9"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a id="STLCRef.v_nat" class="idref" href="#STLCRef.v_nat"><span class="id" title="constructor">v_nat</span></a> : <span class="id" title="keyword">∀</span> <a id="n:10" class="idref" href="#n:10"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> ,<br/>
<a class="idref" href="References.html#value:5"><span class="id" title="inductive">value</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#n:10"><span class="id" title="variable">n</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a id="STLCRef.v_unit" class="idref" href="#STLCRef.v_unit"><span class="id" title="constructor">v_unit</span></a> :<br/>
<a class="idref" href="References.html#value:5"><span class="id" title="inductive">value</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'unit'"><span class="id" title="notation">unit</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a id="STLCRef.v_loc" class="idref" href="#STLCRef.v_loc"><span class="id" title="constructor">v_loc</span></a> : <span class="id" title="keyword">∀</span> <a id="l:11" class="idref" href="#l:11"><span class="id" title="binder">l</span></a>,<br/>
<a class="idref" href="References.html#value:5"><span class="id" title="inductive">value</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'loc'_x"><span class="id" title="notation">loc</span></a> <a class="idref" href="References.html#l:11"><span class="id" title="variable">l</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="References.html#value"><span class="id" title="inductive">value</span></a> : <span class="id" title="var">core</span>.<br/>
</div>
<div class="doc">
Extending substitution to handle the new syntax of terms is
straightforward: substituting in a pointer leaves it
unchanged.
</div>
<div class="code">
<span class="id" title="keyword">Fixpoint</span> <a id="STLCRef.subst" class="idref" href="#STLCRef.subst"><span class="id" title="definition">subst</span></a> (<a id="x:12" class="idref" href="#x:12"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="s:13" class="idref" href="#s:13"><span class="id" title="binder">s</span></a> : <a class="idref" href="References.html#STLCRef.tm"><span class="id" title="inductive">tm</span></a>) (<a id="t:14" class="idref" href="#t:14"><span class="id" title="binder">t</span></a> : <a class="idref" href="References.html#STLCRef.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="References.html#STLCRef.tm"><span class="id" title="inductive">tm</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="References.html#t:14"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
<span class="comment">(* pure STLC *)</span><br/>
| <a class="idref" href="References.html#STLCRef.tm_var"><span class="id" title="constructor">tm_var</span></a> <span class="id" title="var">y</span> ⇒<br/>
<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#eqb"><span class="id" title="definition">String.eqb</span></a> <a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="keyword">then</span> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="References.html#t:14"><span class="id" title="variable">t</span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">\</span></a><span class="id" title="var">y</span><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">:</span></a><span class="id" title="var">T</span><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">,</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#eqb"><span class="id" title="definition">String.eqb</span></a> <a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="keyword">then</span> <a class="idref" href="References.html#t:14"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">\</span></a><span class="id" title="var">y</span><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">:</span></a><span class="id" title="var">T</span><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">,</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a><a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a><a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a><a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
<span class="comment">(* numbers *)</span><br/>
| <a class="idref" href="References.html#STLCRef.tm_const"><span class="id" title="constructor">tm_const</span></a> <span class="id" title="var">_</span> ⇒<br/>
<a class="idref" href="References.html#t:14"><span class="id" title="variable">t</span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#STLCRef.:stlc::'succ'_x"><span class="id" title="notation">succ</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#STLCRef.:stlc::'succ'_x"><span class="id" title="notation">succ</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#STLCRef.:stlc::'pred'_x"><span class="id" title="notation">pred</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#STLCRef.:stlc::'pred'_x"><span class="id" title="notation">pred</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="References.html#aefa1df20f40a8331bf6423412f1c115"><span class="id" title="notation">×</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="References.html#aefa1df20f40a8331bf6423412f1c115"><span class="id" title="notation">×</span></a> <a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">if<sub>0</sub></span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="References.html#STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="References.html#STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <span class="id" title="var">t<sub>3</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a><a class="idref" href="References.html#STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">if<sub>0</sub></span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="References.html#STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="References.html#STLCRef.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>3</sub></span><a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
<span class="comment">(* unit *)</span><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'unit'"><span class="id" title="notation">unit</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'unit'"><span class="id" title="notation">unit</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
<span class="comment">(* references *)</span><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'ref'_x"><span class="id" title="notation">ref</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'ref'_x"><span class="id" title="notation">ref</span></a> <a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a><a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#70f28e5c58264a9753710970e9df6ba<sub>2</sub>"><span class="id" title="notation">!</span></a><span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#70f28e5c58264a9753710970e9df6ba<sub>2</sub>"><span class="id" title="notation">!</span></a><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a><a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="References.html#c9336c07d043872f48e6c531eccadb3e"><span class="id" title="notation">:=</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a><a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="References.html#c9336c07d043872f48e6c531eccadb3e"><span class="id" title="notation">:=</span></a> <a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">[</span></a><a class="idref" href="References.html#x:12"><span class="id" title="variable">x</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">:=</span></a><a class="idref" href="References.html#s:13"><span class="id" title="variable">s</span></a><a class="idref" href="References.html#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a><br/>
| <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'loc'_x"><span class="id" title="notation">loc</span></a> <span class="id" title="var">_</span> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a> ⇒<br/>
<a class="idref" href="References.html#t:14"><span class="id" title="variable">t</span></a><br/>
<span class="id" title="keyword">end</span><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="b811d80014e4babd27a16e96fb5faa5f" class="idref" href="#b811d80014e4babd27a16e96fb5faa5f"><span class="id" title="notation">"</span></a>'[' x ':=' s ']' t" := (<a class="idref" href="References.html#subst:15"><span class="id" title="definition">subst</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>).<br/>
</div>
<div class="doc">
<a id="lab420"></a><h1 class="section">Pragmatics</h1>
</div>
<div class="doc">
<a id="lab421"></a><h2 class="section">Side Effects and Sequencing</h2>
<div class="paragraph"> </div>
The fact that we've chosen the result of an assignment
expression to be the trivial value <span class="inlinecode"><span class="id" title="var">unit</span></span> allows a nice
abbreviation for <i>sequencing</i>. For example, we can write
<pre>
r:=succ(!r); !r
</pre>
as an abbreviation for
<pre>
(\x:Unit, !r) (r:=succ(!r)).
</pre>
This has the effect of reducing two expressions in order and
returning the value of the second. Restricting the type of the
first expression to <span class="inlinecode"><span class="id" title="var">Unit</span></span> helps the typechecker to catch some
silly errors by permitting us to throw away the first value only
if it is really guaranteed to be trivial.
<div class="paragraph"> </div>
Notice that, if the second expression is also an assignment, then
the type of the whole sequence will be <span class="inlinecode"><span class="id" title="var">Unit</span></span>, so we can validly
place it to the left of another <span class="inlinecode">;</span> to build longer sequences of
assignments:
<pre>
r:=succ(!r); r:=succ(!r); r:=succ(!r); r:=succ(!r); !r
</pre>
Formally, we introduce sequencing as a <i>derived form</i>
<span class="inlinecode"><span class="id" title="var">tseq</span></span> that expands into an abstraction and an application.
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="STLCRef.x" class="idref" href="#STLCRef.x"><span class="id" title="definition">x</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> := "x".<br/>
<span class="id" title="keyword">Definition</span> <a id="STLCRef.y" class="idref" href="#STLCRef.y"><span class="id" title="definition">y</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> := "y".<br/>
<span class="id" title="keyword">Definition</span> <a id="STLCRef.z" class="idref" href="#STLCRef.z"><span class="id" title="definition">z</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> := "z".<br/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="References.html#STLCRef.x"><span class="id" title="definition">x</span></a> : <span class="id" title="var">core</span>.<br/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="References.html#STLCRef.y"><span class="id" title="definition">y</span></a> : <span class="id" title="var">core</span>.<br/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="References.html#STLCRef.z"><span class="id" title="definition">z</span></a> : <span class="id" title="var">core</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="STLCRef.tseq" class="idref" href="#STLCRef.tseq"><span class="id" title="definition">tseq</span></a> <a id="t<sub>1</sub>:17" class="idref" href="#t<sub>1</sub>:17"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:18" class="idref" href="#t<sub>2</sub>:18"><span class="id" title="binder">t<sub>2</sub></span></a> :=<br/>
<a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">\</span></a> <a class="idref" href="References.html#STLCRef.x"><span class="id" title="definition">x</span></a> <a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">:</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'Unit'"><span class="id" title="notation">Unit</span></a><a class="idref" href="References.html#fcbb07911888b1a4b268f628a4d64735"><span class="id" title="notation">,</span></a> <a class="idref" href="References.html#t<sub>2</sub>:18"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="References.html#0975a85e562f22315b420c8d1c95dd<sub>06</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="References.html#t<sub>1</sub>:17"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="cd8fd2f0f5bd1b2ecea4cab15254e7e<sub>4</sub>" class="idref" href="#cd8fd2f0f5bd1b2ecea4cab15254e7e<sub>4</sub>"><span class="id" title="notation">"</span></a>t<sub>1</sub> ; t<sub>2</sub>" := (<a class="idref" href="References.html#STLCRef.tseq"><span class="id" title="definition">tseq</span></a> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/>
</div>
<div class="doc">
<a id="lab422"></a><h2 class="section">References and Aliasing</h2>
<div class="paragraph"> </div>
It is important to bear in mind the difference between the
<i>reference</i> that is bound to some variable <span class="inlinecode"><span class="id" title="var">r</span></span> and the <i>cell</i>
in the store that is pointed to by this reference.
<div class="paragraph"> </div>
If we make a copy of <span class="inlinecode"><span class="id" title="var">r</span></span>, for example by binding its value to
another variable <span class="inlinecode"><span class="id" title="var">s</span></span>, what gets copied is only the <i>reference</i>,
not the contents of the cell itself.
<div class="paragraph"> </div>
For example, after reducing
<pre>
let r = ref 5 in
let s = r in
s := 82;
(!r)+1
</pre>
the cell referenced by <span class="inlinecode"><span class="id" title="var">r</span></span> will contain the value <span class="inlinecode">82</span>, while the
result of the whole expression will be <span class="inlinecode">83</span>. The references <span class="inlinecode"><span class="id" title="var">r</span></span>
and <span class="inlinecode"><span class="id" title="var">s</span></span> are said to be <i>aliases</i> for the same cell.
<div class="paragraph"> </div>
The possibility of aliasing can make programs with references
quite tricky to reason about. For example, the expression
<pre>
r := 5; r := !s
</pre>
assigns <span class="inlinecode">5</span> to <span class="inlinecode"><span class="id" title="var">r</span></span> and then immediately overwrites it with <span class="inlinecode"><span class="id" title="var">s</span></span>'s
current value; this has exactly the same effect as the single
assignment
<pre>
r := !s
</pre>
<i>unless</i> we happen to do it in a context where <span class="inlinecode"><span class="id" title="var">r</span></span> and <span class="inlinecode"><span class="id" title="var">s</span></span> are
aliases for the same cell!
<pre>
let r = ref 0 in
let s = r in
r := 5; r := !s
</pre>
</div>
<div class="doc">
<a id="lab423"></a><h2 class="section">Shared State</h2>
<div class="paragraph"> </div>
Of course, aliasing is also a large part of what makes references
useful. In particular, it allows us to set up "implicit
communication channels" -- shared state -- between different parts
of a program. For example, suppose we define a reference cell and
two functions that manipulate its contents:
<pre>
let c = ref 0 in
let incc = \_:Unit, (c := succ (!c); !c) in
let decc = \_:Unit, (c := pred (!c); !c) in
...
</pre>
<div class="paragraph"> </div>
Note that, since their argument types are <span class="inlinecode"><span class="id" title="var">Unit</span></span>, the
arguments to the abstractions in the definitions of <span class="inlinecode"><span class="id" title="var">incc</span></span> and
<span class="inlinecode"><span class="id" title="var">decc</span></span> are not providing any useful information to the bodies of
these functions (using the wildcard <span class="inlinecode"><span class="id" title="var">_</span></span> as the name of the bound
variable is a reminder of this). Instead, their purpose of these
abstractions is to "slow down" the execution of the function
bodies. Since function abstractions are values, the two <span class="inlinecode"><span class="id" title="keyword">let</span></span>s are
executed simply by binding these functions to the names <span class="inlinecode"><span class="id" title="var">incc</span></span> and
<span class="inlinecode"><span class="id" title="var">decc</span></span>, rather than by actually incrementing or decrementing <span class="inlinecode"><span class="id" title="var">c</span></span>.
Later, each call to one of these functions results in its body
being executed once and performing the appropriate mutation on
<span class="inlinecode"><span class="id" title="var">c</span></span>. Such functions are often called <i>thunks</i>.
<div class="paragraph"> </div>
In the context of these declarations, calling <span class="inlinecode"><span class="id" title="var">incc</span></span> results in
changes to <span class="inlinecode"><span class="id" title="var">c</span></span> that can be observed by calling <span class="inlinecode"><span class="id" title="var">decc</span></span>. For
example, if we replace the <span class="inlinecode">...</span> with <span class="inlinecode">(<span class="id" title="var">incc</span></span> <span class="inlinecode"><span class="id" title="var">unit</span>;</span> <span class="inlinecode"><span class="id" title="var">incc</span></span> <span class="inlinecode"><span class="id" title="var">unit</span>;</span> <span class="inlinecode"><span class="id" title="var">decc</span></span>
<span class="inlinecode"><span class="id" title="var">unit</span>)</span>, the result of the whole program will be <span class="inlinecode">1</span>.
</div>
<div class="doc">
<a id="lab424"></a><h2 class="section">Objects</h2>
<div class="paragraph"> </div>
We can go a step further and write a <i>function</i> that creates <span class="inlinecode"><span class="id" title="var">c</span></span>,
<span class="inlinecode"><span class="id" title="var">incc</span></span>, and <span class="inlinecode"><span class="id" title="var">decc</span></span>, packages <span class="inlinecode"><span class="id" title="var">incc</span></span> and <span class="inlinecode"><span class="id" title="var">decc</span></span> together into a
record, and returns this record:
<pre>
newcounter =
\_:Unit,
let c = ref 0 in
let incc = \_:Unit, (c := succ (!c); !c) in
let decc = \_:Unit, (c := pred (!c); !c) in
{i=incc, d=decc}
</pre>
<div class="paragraph"> </div>
Now, each time we call <span class="inlinecode"><span class="id" title="var">newcounter</span></span>, we get a new record of
functions that share access to the same storage cell <span class="inlinecode"><span class="id" title="var">c</span></span>. The
caller of <span class="inlinecode"><span class="id" title="var">newcounter</span></span> can't get at this storage cell directly,
but can affect it indirectly by calling the two functions. In
other words, we've created a simple form of <i>object</i>.
<pre>
let c<sub>1</sub> = newcounter unit in
let c<sub>2</sub> = newcounter unit in
// Note that we've allocated two separate storage cells now!
let r<sub>1</sub> = c<sub>1</sub>.i unit in
let r<sub>2</sub> = c<sub>2</sub>.i unit in
r<sub>2</sub> // yields 1, not 2!
</pre>
<div class="paragraph"> </div>
<a id="lab425"></a><h4 class="section">Exercise: 1 star, standard, optional (store_draw)</h4>
Draw (on paper) the contents of the store at the point in
execution where the first two <span class="inlinecode"><span class="id" title="keyword">let</span></span>s have finished and the third
one is about to begin.
</div>
<div class="code">
<span class="comment">(* FILL IN HERE *)</span><br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<a id="lab426"></a><h2 class="section">References to Compound Types</h2>
<div class="paragraph"> </div>
A reference cell need not contain just a number: the primitives
we've defined above allow us to create references to values of any
type, including functions. For example, we can use references to
functions to give an (inefficient) implementation of arrays
of numbers, as follows.
<div class="paragraph"> </div>
Write <span class="inlinecode"><span class="id" title="var">NatArray</span></span> for the type <span class="inlinecode"><span class="id" title="var">Ref</span></span> <span class="inlinecode">(<span class="id" title="var">Nat</span>→<span class="id" title="var">Nat</span>)</span>.
<div class="paragraph"> </div>
Recall the <span class="inlinecode"><span class="id" title="var">equal</span></span> function from the <a href="MoreStlc.html"><span class="inlineref">MoreStlc</span></a> chapter:
<pre>
equal =
fix
(\eq:Nat<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span>Nat<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span>Bool,
\m:Nat, \n:Nat,
if m=0 then iszero n
else if n=0 then false
else eq (pred m) (pred n))
</pre>
<div class="paragraph"> </div>
To build a new array, we allocate a reference cell and fill
it with a function that, when given an index, always returns <span class="inlinecode">0</span>.
<pre>
newarray = \_:Unit, ref (\n:Nat,0)
</pre>
<div class="paragraph"> </div>
To look up an element of an array, we simply apply
the function to the desired index.
<pre>
lookup = \a:NatArray, \n:Nat, (!a) n
</pre>
<div class="paragraph"> </div>
The interesting part of the encoding is the <span class="inlinecode"><span class="id" title="var">update</span></span> function. It
takes an array, an index, and a new value to be stored at that index, and
does its job by creating (and storing in the reference) a new function
that, when it is asked for the value at this very index, returns the new
value that was given to <span class="inlinecode"><span class="id" title="var">update</span></span>, while on all other indices it passes the
lookup to the function that was previously stored in the reference.
<pre>
update = \a:NatArray, \m:Nat, \v:Nat,
let oldf = !a in
a := (\n:Nat, if equal m n then v else oldf n);
</pre>
<div class="paragraph"> </div>
References to values containing other references can also be very
useful, allowing us to define data structures such as mutable
lists and trees.
<div class="paragraph"> </div>
<a id="lab427"></a><h4 class="section">Exercise: 2 stars, standard, especially useful (compact_update)</h4>
If we defined <span class="inlinecode"><span class="id" title="var">update</span></span> more compactly like this
<pre>
update = \a:NatArray, \m:Nat, \v:Nat,
a := (\n:Nat, if equal m n then v else (!a) n)
</pre>
would it behave the same?
</div>
<div class="code">
<span class="comment">(* FILL IN HERE *)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(* Do not modify the following line: *)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCRef.manual_grade_for_compact_update" class="idref" href="#STLCRef.manual_grade_for_compact_update"><span class="id" title="definition">manual_grade_for_compact_update</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<a id="lab428"></a><h2 class="section">Null References</h2>
<div class="paragraph"> </div>
There is one final significant difference between our
references and C-style mutable variables: in C-like languages,
variables holding pointers into the heap may sometimes have the
value <span class="inlinecode"><span class="id" title="var">NULL</span></span>. Dereferencing such a "null pointer" is an error,
and results either in a clean exception (Java and C<span class="inlinecode">#</span>) or in
arbitrary and possibly insecure behavior (C and relatives like
C++). Null pointers cause significant trouble in C-like
languages: the fact that any pointer might be null means that any
dereference operation in the program can potentially fail.
<div class="paragraph"> </div>
Even in ML-like languages, there are occasionally situations where
we may or may not have a valid pointer in our hands. Fortunately,
there is no need to extend the basic mechanisms of references to
represent such situations: the sum types introduced in the
<a href="MoreStlc.html"><span class="inlineref">MoreStlc</span></a> chapter already give us what we need.
<div class="paragraph"> </div>
First, we can use sums to build an analog of the <span class="inlinecode"><span class="id" title="var">option</span></span> types
introduced in the <a href="https://softwarefoundations.cis.upenn.edu/lf-current/Lists.html"><span class="inlineref">Lists</span></a> chapter of <i>Logical Foundations</i>.
Define <span class="inlinecode"><span class="id" title="var">Option</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> to be an abbreviation for <span class="inlinecode"><span class="id" title="var">Unit</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" title="var">T</span></span>.
<div class="paragraph"> </div>
Then a "nullable reference to a <span class="inlinecode"><span class="id" title="var">T</span></span>" is simply an element of the
type <span class="inlinecode"><span class="id" title="var">Option</span></span> <span class="inlinecode">(<span class="id" title="var">Ref</span></span> <span class="inlinecode"><span class="id" title="var">T</span>)</span>.
</div>
<div class="doc">
<a id="lab429"></a><h2 class="section">Garbage Collection</h2>
<div class="paragraph"> </div>
A last issue that we should mention before we move on with formalizing
references is storage <i>de</i>-allocation. We have not provided any
primitives for freeing reference cells when they are no longer needed.
Instead, like many modern languages (including OCaml, Haskell, Java,
etc.) we rely on the run-time system to perform <i>garbage collection</i>,
automatically identifying and reusing cells that can no longer be
reached by the program.
<div class="paragraph"> </div>
This is <i>not</i> just a question of taste in language design: it is
extremely difficult to achieve type safety in the presence of an
explicit deallocation operation. One reason for this is the
familiar <i>dangling reference</i> problem: we allocate a cell holding
a number, save a reference to it in some data structure, use it
for a while, then deallocate it and allocate a new cell holding a
boolean, possibly reusing the same storage. Now we can have two
names for the same storage cell -- one with type <span class="inlinecode"><span class="id" title="var">Ref</span></span> <span class="inlinecode"><span class="id" title="var">Nat</span></span> and the
other with type <span class="inlinecode"><span class="id" title="var">Ref</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span>.
<div class="paragraph"> </div>
<a id="lab430"></a><h4 class="section">Exercise: 2 stars, standard (type_safety_violation)</h4>
Show how this can lead to a violation of type safety.
</div>
<div class="code">
<span class="comment">(* FILL IN HERE *)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(* Do not modify the following line: *)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCRef.manual_grade_for_type_safety_violation" class="idref" href="#STLCRef.manual_grade_for_type_safety_violation"><span class="id" title="definition">manual_grade_for_type_safety_violation</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<a id="lab431"></a><h1 class="section">Operational Semantics</h1>
</div>
<div class="doc">
<a id="lab432"></a><h2 class="section">Locations</h2>
<div class="paragraph"> </div>
The most subtle aspect of the treatment of references
appears when we consider how to formalize their operational
behavior. One way to see why is to ask, "What should be the
<i>values</i> of type <span class="inlinecode"><span class="id" title="var">Ref</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>?" The crucial observation that we need
to take into account is that reducing a <span class="inlinecode"><span class="id" title="var">ref</span></span> operator should
<i>do</i> something -- namely, allocate some storage -- and the result
of the operation should be a reference to this storage.
<div class="paragraph"> </div>
What, then, is a reference?
<div class="paragraph"> </div>
The run-time store in most programming-language implementations is
essentially just a big array of bytes. The run-time system keeps
track of which parts of this array are currently in use; when we
need to allocate a new reference cell, we allocate a large enough
segment from the free region of the store (4 bytes for integer
cells, 8 bytes for cells storing <span class="inlinecode"><span class="id" title="var">Float</span></span>s, etc.), record somewhere
that it is being used, and return the index (typically, a 32- or
64-bit integer) of the start of the newly allocated region. These
indices are references.
<div class="paragraph"> </div>
For present purposes, there is no need to be quite so concrete.
We can think of the store as an array of <i>values</i>, rather than an
array of bytes, abstracting away from the different sizes of the
run-time representations of different values. A reference, then,
is simply an index into the store. (If we like, we can even
abstract away from the fact that these indices are numbers, but
for purposes of formalization in Coq it is convenient to use
numbers.) We use the word <i>location</i> instead of <i>reference</i> or
<i>pointer</i> to emphasize this abstract quality.
<div class="paragraph"> </div>
Treating locations abstractly in this way will prevent us from
modeling the <i>pointer arithmetic</i> found in low-level languages
such as C. This limitation is intentional. While pointer
arithmetic is occasionally very useful, especially for
implementing low-level services such as garbage collectors, it
cannot be tracked by most type systems: knowing that location <span class="inlinecode"><span class="id" title="var">n</span></span>
in the store contains a <span class="inlinecode"><span class="id" title="var">float</span></span> doesn't tell us anything useful
about the type of location <span class="inlinecode"><span class="id" title="var">n</span>+4</span>. In C, pointer arithmetic is a
notorious source of type-safety violations.
</div>
<div class="doc">
<a id="lab433"></a><h2 class="section">Stores</h2>
<div class="paragraph"> </div>
Recall that, in the small-step operational semantics for
Imp, the step relation needed to carry along an auxiliary state in
addition to the program being executed. In the same way, once we
have added reference cells to the STLC, our step relation must
carry along a store to keep track of the contents of reference
cells.
<div class="paragraph"> </div>
We could re-use the same functional representation we used for
states in Imp, but for carrying out the proofs in this chapter it
is actually more convenient to represent a store simply as a
<i>list</i> of values. (The reason we didn't use this representation
before is that, in Imp, a program could modify any location at any
time, so states had to be ready to map <i>any</i> variable to a value.
However, in the STLC with references, the only way to create a
reference cell is with <span class="inlinecode"><span class="id" title="var">ref</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>, which puts the value of <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>
in a new reference cell and reduces to the location of the newly
created reference cell. When reducing such an expression, we can
just add a new reference cell to the end of the list representing
the store.)
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="STLCRef.store" class="idref" href="#STLCRef.store"><span class="id" title="definition">store</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="References.html#STLCRef.tm"><span class="id" title="inductive">tm</span></a>.<br/>
</div>
<div class="doc">
We use <span class="inlinecode"><span class="id" title="var">store_lookup</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode"><span class="id" title="var">st</span></span> to retrieve the value of the reference
cell at location <span class="inlinecode"><span class="id" title="var">n</span></span> in the store <span class="inlinecode"><span class="id" title="var">st</span></span>. Note that we must give a
default value to <span class="inlinecode"><span class="id" title="var">nth</span></span> in case we try looking up an index which is
too large. (In fact, we will never actually do this, but <i>proving</i>
that we don't will require a bit of work.)
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="STLCRef.store_lookup" class="idref" href="#STLCRef.store_lookup"><span class="id" title="definition">store_lookup</span></a> (<a id="n:19" class="idref" href="#n:19"><span class="id" title="binder">n</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="st:20" class="idref" href="#st:20"><span class="id" title="binder">st</span></a>:<a class="idref" href="References.html#STLCRef.store"><span class="id" title="definition">store</span></a>) :=<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="References.html#n:19"><span class="id" title="variable">n</span></a> <a class="idref" href="References.html#st:20"><span class="id" title="variable">st</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation"><{</span></a> <a class="idref" href="References.html#STLCRef.:stlc::'unit'"><span class="id" title="notation">unit</span></a> <a class="idref" href="References.html#35fac1f60887e7b37d44f938e80b2dc<sub>6</sub>"><span class="id" title="notation">}></span></a>.<br/>
</div>
<div class="doc">
To update the store, we use the <span class="inlinecode"><span class="id" title="tactic">replace</span></span> function, which replaces
the contents of a cell at a particular index.
</div>
<div class="code">
<span class="id" title="keyword">Fixpoint</span> <a id="STLCRef.replace" class="idref" href="#STLCRef.replace"><span class="id" title="definition">replace</span></a> {<a id="A:21" class="idref" href="#A:21"><span class="id" title="binder">A</span></a>:<span class="id" title="keyword">Type</span>} (<a id="n:22" class="idref" href="#n:22"><span class="id" title="binder">n</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="x:23" class="idref" href="#x:23"><span class="id" title="binder">x</span></a>:<a class="idref" href="References.html#A:21"><span class="id" title="variable">A</span></a>) (<a id="l:24" class="idref" href="#l:24"><span class="id" title="binder">l</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="References.html#A:21"><span class="id" title="variable">A</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="References.html#A:21"><span class="id" title="variable">A</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="References.html#l:24"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a><br/>
| <span class="id" title="var">h</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="References.html#n:22"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> ⇒ <a class="idref" href="References.html#x:23"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span><br/>
| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n'</span> ⇒ <span class="id" title="var">h</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="References.html#replace:25"><span class="id" title="definition">replace</span></a> <span class="id" title="var">n'</span> <a class="idref" href="References.html#x:23"><span class="id" title="variable">x</span></a> <span class="id" title="var">t</span><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">end</span>.<br/>
</div>
<div class="doc">
As might be expected, we will also need some technical
lemmas about <span class="inlinecode"><span class="id" title="tactic">replace</span></span>; they are straightforward to prove.
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="STLCRef.replace_nil" class="idref" href="#STLCRef.replace_nil"><span class="id" title="lemma">replace_nil</span></a> : <span class="id" title="keyword">∀</span> <a id="A:28" class="idref" href="#A:28"><span class="id" title="binder">A</span></a> <a id="n:29" class="idref" href="#n:29"><span class="id" title="binder">n</span></a> (<a id="x:30" class="idref" href="#x:30"><span class="id" title="binder">x</span></a>:<a class="idref" href="References.html#A:28"><span class="id" title="variable">A</span></a>),<br/>
<a class="idref" href="References.html#STLCRef.replace"><span class="id" title="definition">replace</span></a> <a class="idref" href="References.html#n:29"><span class="id" title="variable">n</span></a> <a class="idref" href="References.html#x:30"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span>; <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCRef.length_replace" class="idref" href="#STLCRef.length_replace"><span class="id" title="lemma">length_replace</span></a> : <span class="id" title="keyword">∀</span> <a id="A:31" class="idref" href="#A:31"><span class="id" title="binder">A</span></a> <a id="n:32" class="idref" href="#n:32"><span class="id" title="binder">n</span></a> <a id="x:33" class="idref" href="#x:33"><span class="id" title="binder">x</span></a> (<a id="l:34" class="idref" href="#l:34"><span class="id" title="binder">l</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="References.html#A:31"><span class="id" title="variable">A</span></a>),<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#length"><span class="id" title="definition">length</span></a> (<a class="idref" href="References.html#STLCRef.replace"><span class="id" title="definition">replace</span></a> <a class="idref" href="References.html#n:32"><span class="id" title="variable">n</span></a> <a class="idref" href="References.html#x:33"><span class="id" title="variable">x</span></a> <a class="idref" href="References.html#l:34"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="References.html#l:34"><span class="id" title="variable">l</span></a>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">n</span> <span class="id" title="var">x</span> <span class="id" title="var">l</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">n</span>.<br/>
<span class="id" title="tactic">induction</span> <span class="id" title="var">l</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">n</span>.<br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span>...<br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span>...<br/>
<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHl</span>...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCRef.lookup_replace_eq" class="idref" href="#STLCRef.lookup_replace_eq"><span class="id" title="lemma">lookup_replace_eq</span></a> : <span class="id" title="keyword">∀</span> <a id="l:35" class="idref" href="#l:35"><span class="id" title="binder">l</span></a> <a id="t:36" class="idref" href="#t:36"><span class="id" title="binder">t</span></a> <a id="st:37" class="idref" href="#st:37"><span class="id" title="binder">st</span></a>,<br/>
<a class="idref" href="References.html#l:35"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'<'_x"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="References.html#st:37"><span class="id" title="variable">st</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="References.html#STLCRef.store_lookup"><span class="id" title="definition">store_lookup</span></a> <a class="idref" href="References.html#l:35"><span class="id" title="variable">l</span></a> (<a class="idref" href="References.html#STLCRef.replace"><span class="id" title="definition">replace</span></a> <a class="idref" href="References.html#l:35"><span class="id" title="variable">l</span></a> <a class="idref" href="References.html#t:36"><span class="id" title="variable">t</span></a> <a class="idref" href="References.html#st:37"><span class="id" title="variable">st</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="References.html#t:36"><span class="id" title="variable">t</span></a>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">l</span> <span class="id" title="var">t</span> <span class="id" title="var">st</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="References.html#STLCRef.store_lookup"><span class="id" title="definition">store_lookup</span></a>.<br/>
<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">l</span>.<br/>
<span class="id" title="tactic">induction</span> <span class="id" title="var">st</span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">t'</span> <span class="id" title="var">st'</span>]; <span class="id" title="tactic">intros</span> <span class="id" title="var">l</span> <span class="id" title="var">Hlen</span>.<br/>
- <span class="comment">(* st = <span class="inlinecode"></span> *)</span><br/>
<span class="id" title="tactic">inversion</span> <span class="id" title="var">Hlen</span>.<br/>
- <span class="comment">(* st = t' :: st' *)</span><br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">l</span>; <span class="id" title="tactic">simpl</span>...<br/>
<span class="id" title="tactic">apply</span> <span class="id" title="var">IHst'</span>. <span class="id" title="tactic">simpl</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hlen</span>. <span class="id" title="var">lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCRef.lookup_replace_neq" class="idref" href="#STLCRef.lookup_replace_neq"><span class="id" title="lemma">lookup_replace_neq</span></a> : <span class="id" title="keyword">∀</span> <a id="l<sub>1</sub>:38" class="idref" href="#l<sub>1</sub>:38"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:39" class="idref" href="#l<sub>2</sub>:39"><span class="id" title="binder">l<sub>2</sub></span></a> <a id="t:40" class="idref" href="#t:40"><span class="id" title="binder">t</span></a> <a id="st:41" class="idref" href="#st:41"><span class="id" title="binder">st</span></a>,<br/>
<a class="idref" href="References.html#l<sub>1</sub>:38"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'<>'_x"><span class="id" title="notation">≠</span></a> <a class="idref" href="References.html#l<sub>2</sub>:39"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="References.html#STLCRef.store_lookup"><span class="id" title="definition">store_lookup</span></a> <a class="idref" href="References.html#l<sub>1</sub>:38"><span class="id" title="variable">l<sub>1</sub></span></a> (<a class="idref" href="References.html#STLCRef.replace"><span class="id" title="definition">replace</span></a> <a class="idref" href="References.html#l<sub>2</sub>:39"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="References.html#t:40"><span class="id" title="variable">t</span></a> <a class="idref" href="References.html#st:41"><span class="id" title="variable">st</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="References.html#STLCRef.store_lookup"><span class="id" title="definition">store_lookup</span></a> <a class="idref" href="References.html#l<sub>1</sub>:38"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="References.html#st:41"><span class="id" title="variable">st</span></a>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="References.html#STLCRef.store_lookup"><span class="id" title="definition">store_lookup</span></a>.<br/>
<span class="id" title="tactic">induction</span> <span class="id" title="var">l<sub>1</sub></span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">l<sub>1</sub>'</span>]; <span class="id" title="tactic">intros</span> <span class="id" title="var">l<sub>2</sub></span> <span class="id" title="var">t</span> <span class="id" title="var">st</span> <span class="id" title="var">Hneq</span>.<br/>
- <span class="comment">(* l<sub>1</sub> = 0 *)</span><br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">st</span>.<br/>
+ <span class="comment">(* st = <span class="inlinecode"></span> *)</span> <span class="id" title="tactic">rewrite</span> <a class="idref" href="References.html#STLCRef.replace_nil"><span class="id" title="lemma">replace_nil</span></a>...<br/>
+ <span class="comment">(* st = _ :: _ *)</span> <span class="id" title="tactic">destruct</span> <span class="id" title="var">l<sub>2</sub></span>... <span class="id" title="var">contradict</span> <span class="id" title="var">Hneq</span>...<br/>
- <span class="comment">(* l<sub>1</sub> = S l<sub>1</sub>' *)</span><br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">st</span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">st<sub>2</sub></span>].<br/>
+ <span class="comment">(* st = <span class="inlinecode"></span> *)</span> <span class="id" title="tactic">destruct</span> <span class="id" title="var">l<sub>2</sub></span>...<br/>
+ <span class="comment">(* st = t<sub>2</sub> :: st<sub>2</sub> *)</span><br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">l<sub>2</sub></span>...<br/>
<span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">apply</span> <span class="id" title="var">IHl1'</span>...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>
<div class="doc">
<a id="lab434"></a><h2 class="section">Reduction</h2>
<div class="paragraph"> </div>
Now we can give the rules for the new constructs:
<center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule"> </td>
<td class="infrulenamecol" rowspan="3">
(ST_RefValue)
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">ref v / st <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>></span></span> loc |st| / st,v</td>
<td></td>
</tr>