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
|
From Coq Require Import Ascii.
From mininix Require Export utils.
From stdpp Require Import options.
Module Import evallang.
Inductive expr :=
| EString (s : string)
| EId (ds : option expr) (x : string)
| EEval (ds : gmap string expr) (ee : expr)
| EAbs (ex e : expr)
| EApp (e1 e2 : expr).
Module parser.
Inductive token :=
| TId (s : string)
| TString (s : string)
| TColon
| TExclamation
| TParenL
| TParenR.
Inductive token_state :=
TSString (s : string) | TSId (s : string) | TSOther.
Definition token_state_push (st : token_state) (k : list token) : list token :=
match st with
| TSId s => TId (String.rev s) :: k
| _ => k
end.
Fixpoint tokenize_go (sin : string) (st : token_state)
(k : list token) : option (list token) :=
match sin, st with
| "", TSString _ => None (* no closing "" *)
| "", _ => Some (reverse (token_state_push st k))
| String "\" (String """" sin), TSString s =>
tokenize_go sin (TSString (String """" s)) k
| String """" sin, TSString s =>
tokenize_go sin TSOther (TString (String.rev s) :: k)
| String a sin, TSString s => tokenize_go sin (TSString (String a s)) k
| String ":" sin, _ => tokenize_go sin TSOther (TColon :: token_state_push st k)
| String "!" sin, _ => tokenize_go sin TSOther (TExclamation :: token_state_push st k)
| String "(" sin, _ => tokenize_go sin TSOther (TParenL :: token_state_push st k)
| String ")" sin, _ => tokenize_go sin TSOther (TParenR :: token_state_push st k)
| String """" sin, _ => tokenize_go sin (TSString "") k
| String a sin, TSOther =>
if Ascii.is_space a then tokenize_go sin TSOther k
else tokenize_go sin (TSId (String a EmptyString)) k
| String a sin, TSId s =>
if Ascii.is_space a then tokenize_go sin TSOther (TId (String.rev s) :: k)
else tokenize_go sin (TSId (String a s)) k
end.
Definition tokenize (sin : string) : option (list token) :=
tokenize_go sin TSOther [].
Inductive stack_item :=
| SExpr (e : expr)
| SAbsR (e : expr)
| SEval
| SParenL.
Definition stack_push (e : expr) (k : list stack_item) : list stack_item :=
match k with
| SExpr e1 :: k => SExpr (EApp e1 e) :: k
| SEval :: k => SExpr (EEval ∅ e) :: k
| _ => SExpr e :: k
end.
Fixpoint stack_pop_go (e : expr)
(k : list stack_item) : option (expr * list stack_item) :=
match k with
| SAbsR e1 :: k => stack_pop_go (EAbs e1 e) k
| _ => Some (e, k)
end.
Definition stack_pop (k : list stack_item) : option (expr * list stack_item) :=
match k with
| SExpr e :: k => stack_pop_go e k
| _ => None
end.
Fixpoint parse_go (ts : list token) (k : list stack_item) : option expr :=
match ts with
| [] => '(e, k) ← stack_pop k; guard (k = []);; Some e
| TString x :: ts => parse_go ts (stack_push (EString x) k)
| TId "eval" :: TExclamation :: ts => parse_go ts (SEval :: k)
| TId x :: TColon :: ts => parse_go ts (SAbsR (EString x) :: k)
| TId x :: ts => parse_go ts (stack_push (EId None x) k)
| TColon :: ts =>
'(e, k) ← stack_pop k;
parse_go ts (SAbsR e :: k)
| TParenL :: ts => parse_go ts (SParenL :: k)
| TParenR :: ts =>
'(e, k) ← stack_pop k;
match k with
| SParenL :: k => parse_go ts (stack_push e k)
| _ => None
end
| _ => None
end.
Definition parse (sin : string) : option expr :=
ts ← tokenize sin; parse_go ts [].
End parser.
Definition parse := parser.parse.
Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
match e with
| EString s => EString s
| EId ds' x => EId (ds !! x ∪ ds') x
| EEval ds' ee => EEval (ds ∪ ds') (subst ds ee)
| EAbs ex e => EAbs (subst ds ex) (subst ds e)
| EApp e1 e2 => EApp (subst ds e1) (subst ds e2)
end.
Reserved Infix "-->" (right associativity, at level 55).
Inductive step : expr → expr → Prop :=
| Sβ x e1 e2 : EApp (EAbs (EString x) e1) e2 --> subst {[x:=e2]} e1
| SId e x : EId (Some e) x --> e
| SEvalString ds s e : parse s = Some e → EEval ds (EString s) --> subst ds e
| SAbsL ex1 ex1' e : ex1 --> ex1' → EAbs ex1 e --> EAbs ex1' e
| SAppL e1 e1' e2 : e1 --> e1' → EApp e1 e2 --> EApp e1' e2
| SEval ds e1 e1' : e1 --> e1' → EEval ds e1 --> EEval ds e1'
where "e1 --> e2" := (step e1 e2).
Infix "-->*" := (rtc step) (right associativity, at level 55).
Definition final (e : expr) : Prop :=
match e with
| EString _ => True
| EAbs (EString _) _ => True
| _ => False
end.
Definition stuck (e : expr) : Prop :=
nf step e ∧ ¬final e.
End evallang.
|
