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
|
(* $Id$ *)
open Util
open Names
open Generic
open Term
(* Given a term with variables in it, and second-order substitution,
this function will apply the substitution. The special
operator "XTRA[$SOAPP]" is used to represent the second-order
substitution.
(1) second-order substitutions: $SOAPP(SOLAM;... soargs ...)
This operation will take the term SOLAM, which must be
of the form [x1][x2]...[xn]B and replace the xi with the
soargs. If any of the soargs are variables, then we will
rename the binders for these variables to the name of the
xi.
*)
let list_assign_1 l n e =
let rec assrec = function
| (1, h::t) -> e :: t
| (n, h::t) -> h :: (assrec (n-1,t))
| (_, []) -> failwith "list_assign_1"
in
assrec (n,l)
(* [propagate_name spine_map argt new_na]
* if new_na is a real name, and argt is a (Rel idx)
* then the entry for idx in the spine_map
* is replaced with new_na. In any case, a new spine_map is returned.
*)
let propagate_name smap argt new_na =
match argt,new_na with
| (Rel idx, (Name _ as na)) ->
(try list_assign_1 smap idx na with Failure _ -> smap)
| (_, _) -> smap
let is_soapp_operator = function
| DOPN(XTRA "$SOAPP",cl) -> true
| DOP2(XTRA "$SOAPP",_,_) -> true
| _ -> false
let dest_soapp_operator = function
| DOPN(XTRA "$SOAPP",cl) -> (array_hd cl,array_list_of_tl cl)
| DOP2(XTRA "$SOAPP",c1,c2) -> (c1,[c2])
| _ -> failwith "dest_soapp_operator"
let solam_names =
let rec namrec acc = function
| DLAM(na,b) -> namrec (na::acc) b
| _ -> List.rev acc
in
namrec []
let do_propsoapp smap (solam,soargs) =
let rec propsolam smap solam soargs =
match (solam,soargs) with
| ((DLAM(na,b)), (arg::argl)) ->
propsolam (propagate_name smap arg na) b argl
| ((DLAM _), []) -> error "malformed soapp"
| (_, (_::_)) -> error "malformed soapp"
| (_, []) -> smap
in
propsolam smap solam soargs
let propsoapp smap t =
if is_soapp_operator t then
do_propsoapp smap (dest_soapp_operator t)
else
smap
(* [propagate_names spine_map t]
* walks t, looking for second-order applications.
* Each time it finds one, it tries to propagate
* backwards any names that it can for arguments of
* the application which are debruijn references.
*)
let propagate_names =
let rec proprec smap t =
let (smap,t) =
(match t with
| DOP0 oper -> (smap,t)
| DOP1(op,c) ->
let (smap',c') = proprec smap c in
(smap',DOP1(op,c'))
| DOP2(op,c1,c2) ->
let (smap',c1') = proprec smap c1 in
let (smap'',c2') = proprec smap c2 in
(smap'',DOP2(op,c1',c2'))
| DOPN(op,cl) ->
let cllist = Array.to_list cl in
let (smap',cl'list) =
List.fold_right
(fun c (smap,acc) ->
let (smap',c') = proprec smap c in (smap',c'::acc))
cllist (smap,[])
in
(smap',DOPN(op,Array.of_list cl'list))
| DOPL(op,cl) ->
let cllist = cl in
let (smap',cl'list) =
List.fold_right
(fun c (smap,acc) ->
let (smap',c') = proprec smap c in (smap',c'::acc))
cllist (smap,[])
in
(smap',DOPL(op,cl'list))
| DLAM(na,c) ->
let (lna', c') = proprec (na::smap) c in
(List.tl lna', DLAM(List.hd lna', c'))
| DLAMV(na,cl) ->
let cllist = Array.to_list cl in
let (lna',cl'list) =
List.fold_right
(fun c (smap,acc) ->
let (smap',c') = proprec smap c in (smap',c'::acc))
cllist (na::smap,[])
in
(List.tl lna',DLAMV(List.hd lna',Array.of_list cl'list))
| Rel i -> (smap,t)
| VAR id -> (smap,t))
in
(propsoapp smap t,t)
in
proprec
let socontract =
let rec lamrec sigma x y =
match x,y with
| (h::t, DLAM(_,c)) -> lamrec (h::sigma) t c
| ([], t) -> substl sigma t
| ((_::_), _) -> error "second-order app with mismatched arguments"
in
lamrec []
(* [soeval t]
* evaluates t, by contracting any second-order redexes
*)
let rec soeval t=
match t with
| DOP0 _ -> t
| Rel _ -> t
| VAR _ -> t
| DOP1(op,c) -> DOP1(op,soeval c)
| DLAM(na,c) -> DLAM(na,soeval c)
| DLAMV(na,cl) -> DLAMV(na,Array.map soeval cl)
| DOP2(op,c1,c2) ->
let c1' = soeval c1
and c2' = soeval c2 in
if is_soapp_operator t then
socontract [c2'] c1'
else
DOP2(op,c1',c2')
| DOPN(op,cl) ->
let cl' = Array.map soeval cl in
if is_soapp_operator t then
let lam = array_hd cl' in
let args = Array.to_list (array_tl cl') in
socontract args lam
else
DOPN(op,cl')
| DOPL(op,cl) ->
let cl' = List.map soeval cl in
if is_soapp_operator t then
let lam = List.hd cl'
and args = List.tl cl' in
socontract args lam
else
DOPL(op,cl')
let rec try_soeval t =
match t with
| DOP0 _ -> t
| Rel _ -> t
| VAR _ -> t
| DOP1(op,c) -> DOP1(op,try_soeval c)
| DLAM(na,c) -> DLAM(na,try_soeval c)
| DLAMV(na,cl) -> DLAMV(na,Array.map try_soeval cl)
| DOP2(op,c1,c2) ->
let c1' = try_soeval c1
and c2' = try_soeval c2 in
if is_soapp_operator t then
(try socontract [c2'] c1'
with (Failure _ | UserError _) -> DOP2(op,c1',c2'))
else
DOP2(op,c1',c2')
| DOPN(op,cl) ->
let cl' = Array.map try_soeval cl in
if is_soapp_operator t then
let lam = array_hd cl'
and args = Array.to_list (array_tl cl') in
(try socontract args lam
with (Failure _ | UserError _) -> DOPN(op,cl'))
else
DOPN(op,cl')
| DOPL(op,cl) ->
let cl' = List.map try_soeval cl in
if is_soapp_operator t then
let lam = List.hd cl'
and args = List.tl cl' in
(try socontract args lam
with (Failure _ | UserError _) -> DOPL(op,cl'))
else
DOPL(op,cl')
let soexecute t =
let (_,t) = propagate_names [] t in
soeval t
let try_soexecute t =
let (_,t) =
try propagate_names [] t
with (Failure _ | UserError _) -> ([],t)
in
try_soeval t
|
