Skip to content

Commit 05ec7e1

Browse files
strubstrub
committed
user reduction: fix some incompleteness issues
Record projectors being operators, they are subject to user defined rules.
1 parent 5628306 commit 05ec7e1

File tree

2 files changed

+115
-89
lines changed

2 files changed

+115
-89
lines changed

‎src/ecCallbyValue.ml

+91-75
Original file line numberDiff line numberDiff line change
@@ -215,18 +215,17 @@ and betared st s bd f args =
215215
betared st s bd f args
216216

217217
(* -------------------------------------------------------------------- *)
218-
and app_red st f1 args =
219-
match f1.f_node with
220-
(* β-reduction *)
221-
| Fquant (Llambda, bd, f2) when not (Args.isempty args) && st.st_ri.beta ->
222-
betared st Subst.subst_id bd f2 args
223-
224-
(* ι-reduction (records projection) *)
225-
| Fop (p, _) when
226-
st.st_ri.iota
218+
and try_reduce_record_projection
219+
(st : state) ((p, _tys) : EcPath.path * ty list) (args : args)
220+
=
221+
let exception Bailout in
222+
223+
try
224+
if not (
225+
st.st_ri.iota
227226
&& EcEnv.Op.is_projection st.st_env p
228227
&& not (Args.isempty args)
229-
-> begin
228+
) then raise Bailout;
230229

231230
let mk, args1 = oget (Args.pop args) in
232231

@@ -235,75 +234,92 @@ and app_red st f1 args =
235234
when (EcEnv.Op.is_record_ctor st.st_env mkp) ->
236235
let v = oget (EcEnv.Op.by_path_opt p st.st_env) in
237236
let v = proj3_2 (EcDecl.operator_as_proj v) in
238-
app_red st (List.nth mkargs v) args1
237+
Some (app_red st (List.nth mkargs v) args1)
239238

240239
| _ ->
241-
f_app f1 args.stack args.resty
242-
end
240+
None
243241

244-
(* ι-reduction (fix-def reduction) *)
245-
| Fop (p, tys)
246-
when st.st_ri.iota && EcEnv.Op.is_fix_def st.st_env p
247-
-> begin
248-
let module E = struct exception NoCtor end in
249-
250-
try
251-
let Args.{ resty = ty; stack = args; } = args in
252-
let op = oget (EcEnv.Op.by_path_opt p st.st_env) in
253-
let fix = EcDecl.operator_as_fix op in
254-
255-
if List.length args < snd (fix.EcDecl.opf_struct) then
256-
raise E.NoCtor;
257-
258-
let args, eargs = List.split_at (snd (fix.EcDecl.opf_struct)) args in
259-
260-
let vargs = Array.of_list args in
261-
let pargs = List.fold_left (fun (opb, acc) v ->
262-
let v = vargs.(v) in
263-
264-
match fst_map (fun x -> x.f_node) (EcFol.destr_app v) with
265-
| (Fop (p, _), cargs) when EcEnv.Op.is_dtype_ctor st.st_env p -> begin
266-
let idx = EcEnv.Op.by_path p st.st_env in
267-
let idx = snd (EcDecl.operator_as_ctor idx) in
268-
match opb with
269-
| EcDecl.OPB_Leaf _ -> assert false
270-
| EcDecl.OPB_Branch bs ->
271-
((Parray.get bs idx).EcDecl.opb_sub, cargs :: acc)
272-
end
273-
| _ -> raise E.NoCtor)
274-
(fix.EcDecl.opf_branches, []) (fst fix.EcDecl.opf_struct)
275-
in
276-
277-
let pargs, (bds, body) =
278-
match pargs with
279-
| EcDecl.OPB_Leaf (bds, body), cargs -> (List.rev cargs, (bds, body))
280-
| _ -> assert false
281-
in
282-
283-
let subst =
284-
List.fold_left2
285-
(fun subst (x, _) fa -> Subst.bind_local subst x fa)
286-
Subst.subst_id fix.EcDecl.opf_args args in
287-
288-
let subst =
289-
List.fold_left2
290-
(fun subst bds cargs ->
291-
List.fold_left2
292-
(fun subst (x, _) fa -> Subst.bind_local subst x fa)
293-
subst bds cargs)
294-
subst bds pargs in
295-
296-
let body = EcFol.form_of_expr EcFol.mhr body in
297-
let body =
298-
Tvar.f_subst ~freshen:true (List.map fst op.EcDecl.op_tparams) tys body in
299-
300-
cbv st subst body (Args.create ty eargs)
301-
with E.NoCtor ->
302-
reduce_user_delta st f1 p tys args
303-
end
242+
with Bailout ->
243+
None
244+
245+
(* -------------------------------------------------------------------- *)
246+
and try_reduce_fixdef
247+
(st : state) ((p, tys) : EcPath.path * ty list) (args : args)
248+
=
249+
let exception Bailout in
250+
251+
try
252+
if not (st.st_ri.iota && EcEnv.Op.is_fix_def st.st_env p) then
253+
raise Bailout;
254+
255+
let Args.{ resty = ty; stack = args; } = args in
256+
let op = oget (EcEnv.Op.by_path_opt p st.st_env) in
257+
let fix = EcDecl.operator_as_fix op in
258+
259+
if List.length args < snd (fix.EcDecl.opf_struct) then
260+
raise Bailout;
261+
262+
let args, eargs = List.split_at (snd (fix.EcDecl.opf_struct)) args in
263+
264+
let vargs = Array.of_list args in
265+
let pargs = List.fold_left (fun (opb, acc) v ->
266+
let v = vargs.(v) in
267+
268+
match fst_map (fun x -> x.f_node) (EcFol.destr_app v) with
269+
| (Fop (p, _), cargs) when EcEnv.Op.is_dtype_ctor st.st_env p -> begin
270+
let idx = EcEnv.Op.by_path p st.st_env in
271+
let idx = snd (EcDecl.operator_as_ctor idx) in
272+
match opb with
273+
| EcDecl.OPB_Leaf _ -> assert false
274+
| EcDecl.OPB_Branch bs ->
275+
((Parray.get bs idx).EcDecl.opb_sub, cargs :: acc)
276+
end
277+
| _ -> raise Bailout)
278+
(fix.EcDecl.opf_branches, []) (fst fix.EcDecl.opf_struct)
279+
in
280+
281+
let pargs, (bds, body) =
282+
match pargs with
283+
| EcDecl.OPB_Leaf (bds, body), cargs -> (List.rev cargs, (bds, body))
284+
| _ -> assert false
285+
in
286+
287+
let subst =
288+
List.fold_left2
289+
(fun subst (x, _) fa -> Subst.bind_local subst x fa)
290+
Subst.subst_id fix.EcDecl.opf_args args in
291+
292+
let subst =
293+
List.fold_left2
294+
(fun subst bds cargs ->
295+
List.fold_left2
296+
(fun subst (x, _) fa -> Subst.bind_local subst x fa)
297+
subst bds cargs)
298+
subst bds pargs in
299+
300+
let body = EcFol.form_of_expr EcFol.mhr body in
301+
let body =
302+
Tvar.f_subst ~freshen:true (List.map fst op.EcDecl.op_tparams) tys body in
303+
304+
Some (cbv st subst body (Args.create ty eargs))
305+
306+
with Bailout ->
307+
None
308+
309+
(* -------------------------------------------------------------------- *)
310+
and app_red st f1 args =
311+
match f1.f_node with
312+
(* β-reduction *)
313+
| Fquant (Llambda, bd, f2) when not (Args.isempty args) && st.st_ri.beta ->
314+
betared st Subst.subst_id bd f2 args
304315

305-
| Fop(p, tys) ->
306-
reduce_user_delta st f1 p tys args
316+
(* op reduction (ι-reduction / delta / user-defined rules) *)
317+
| Fop (p, tys) ->
318+
List.find_map_opt
319+
(fun f -> f st (p, tys) args)
320+
[ try_reduce_record_projection
321+
; try_reduce_fixdef]
322+
|> ofdfl (fun () -> reduce_user_delta st f1 p tys args)
307323

308324
| _ ->
309325
f_app f1 args.stack args.resty

‎src/ecReduction.ml

+24-14
Original file line numberDiff line numberDiff line change
@@ -947,21 +947,27 @@ let reduce_head simplify ri env hyps f =
947947

948948
(* ι-reduction (records projection) *)
949949
| Fapp ({ f_node = Fop (p, _); }, args)
950-
when ri.iota && EcEnv.Op.is_projection env p ->
951-
begin match args with
952-
| mk :: args ->
953-
begin match mk.f_node with
954-
| Fapp ({ f_node = Fop (mkp, _) }, mkargs) ->
955-
if not (EcEnv.Op.is_record_ctor env mkp) then raise nohead;
956-
let v = oget (EcEnv.Op.by_path_opt p env) in
957-
let v = proj3_2 (EcDecl.operator_as_proj v) in
958-
let v = List.nth mkargs v in
959-
f_app v args f.f_ty
950+
when ri.iota && EcEnv.Op.is_projection env p -> begin
960951

961-
| _ -> raise needsubterm
962-
end
963-
| _ -> raise nohead
952+
try
953+
reduce_user_gen simplify ri env hyps f
954+
with NotRed NoHead -> begin
955+
begin match args with
956+
| mk :: args ->
957+
begin match mk.f_node with
958+
| Fapp ({ f_node = Fop (mkp, _) }, mkargs) ->
959+
if not (EcEnv.Op.is_record_ctor env mkp) then raise nohead;
960+
let v = oget (EcEnv.Op.by_path_opt p env) in
961+
let v = proj3_2 (EcDecl.operator_as_proj v) in
962+
let v = List.nth mkargs v in
963+
f_app v args f.f_ty
964+
965+
| _ -> raise needsubterm
966+
end
967+
| _ -> raise nohead
964968
end
969+
end
970+
end
965971

966972
(* ι-reduction (tuples projection) *)
967973
| Fproj(f1, i) -> begin
@@ -1081,7 +1087,11 @@ let reduce_head simplify ri env hyps f =
10811087
with NotRed _ -> raise needsubterm
10821088
end
10831089

1084-
| Fapp(_, _) -> raise needsubterm
1090+
| Fapp _ -> begin
1091+
try
1092+
reduce_user_gen simplify ri env hyps f
1093+
with NotRed _ -> raise needsubterm
1094+
end
10851095

10861096
| Fquant((Lforall | Lexists), _, _) ->
10871097
reduce_quant ri env hyps f

0 commit comments

Comments
 (0)