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
|
%% This file uses the Ott tool to specify the grammar, typing and
%% evaluation rules for the call-by-value lambda calculus
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% METAVARIABLES
metavar var, x, y ::=
{{ repr-locally-nameless }}
{{ com variables }}
{{ lex alphanum }}
indexvar index, i ::=
{{ coq nat }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% GRAMMAR (LNgen portion)
grammar
typ, T :: 'typ_' ::= {{ com types }}
| base :: :: base {{ com base type }}
{{ tex \mathsf{o} }}
| T1 -> T2 :: :: arrow {{ com function types }}
exp, e, v :: '' ::= {{ com expressions }}
| x :: :: var {{ com variables }}
| \ x . e :: :: abs
(+ bind x in e +)
{{ com abstractions }}
{{ tex [[\]][[x]].[[e]] }}
| e1 e2 :: :: app {{ com applications }}
| e1 [ x ~> e2 ] :: M :: subst
{{ coq (open_exp_wrt_exp [[x e1]][[e2]]) }}
| ( e ) :: S :: paren
{{ coq ([[e]]) }}
substitutions
single exp x :: subst
freevars
exp x :: fv
parsing
typ_arrow right typ_arrow
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% GRAMMAR (non LNgen portion)
grammar
ctx, G {{ tex \Gamma }} :: '' ::= {{ com typing context }} {{ coq list ( atom * typ ) }}
| empty :: :: Empty {{ coq nil }}
{{ tex \bullet }}
{{ com empty context }}
| G , x : T :: :: Cons {{ coq (([[x]]~[[T]])++[[G]]) }}
{{ com assumption }}
terminals :: 'terminals_' ::=
| \ :: :: lambda {{ tex \lambda }}
| --> :: :: red {{ tex \longrightarrow }}
| ==> :: :: bigred {{ tex \Longrightarrow }}
| -> :: :: arrow {{ tex \rightarrow }}
| |- :: :: turnstile {{ tex \vdash }}
| in :: :: in {{ tex \in }}
| fv :: :: fv {{ tex \mathsf{fv}\! }}
| ~> :: :: leadsto {{ tex \leadsto }}
formula :: 'formula_' ::=
| judgement :: :: judgement
| is_value v :: :: is_value
{{ coq is_value [[v]] }}
| uniq G :: :: uniqG
{{ coq uniq [[G]] }}
{{ tex \mathsf{uniq}[[G]] }}
| x : T in G :: :: inG
{{ coq binds [[x]][[T]][[G]] }}
| x notin fv e :: :: fresh
{{ coq [[x]] \notin fv[[e]] }}
| x notin dom G :: :: notInGx
{{ coq ~ AtomSetImpl.In [[x]] (dom [[G]]) }}
embed
{{ coq
Definition is_value (e : exp) : Prop :=
match e with
| abs _ => True
| _ => False
end.
Module StlcNotations.
Notation "[ z ~> u ] e" := (subst_exp u z e) (at level 0).
Notation open e1 e2 := (open_exp_wrt_exp e1 e2).
End StlcNotations.
}}
defns
JTyping :: '' ::=
defn
G |- e : T :: :: typing :: 'typing_'
{{ com Typing rules }}
by
uniq G
x : T in G
------------ :: var
G |- x : T
G, x:T1 |- e : T2
-------------------------- :: abs
G |- \x. e : T1 -> T2
G |- e1 : T1 -> T2
G |- e2 : T1
------------------ :: app
G |- e1 e2 : T2
defns
JEval :: '' ::=
defn
e --> e' :: :: step :: 'step_'
{{ com Small-step operational semantics }}
by
------------------------------- :: beta
(\x.e1) e2 --> e1 [x ~> e2]
e1 --> e1'
----------------- :: app
e1 e2 --> e1' e2
|
