diff options
| author | Pierre Letouzey | 2017-07-05 11:34:39 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-07-20 20:31:18 +0200 |
| commit | d8b78fff7fefd606dae5038b69f220b4f3dd706b (patch) | |
| tree | d59cca2422e30ead7d5e13fc67859a1352261f54 /plugins/extraction/modutil.ml | |
| parent | 4d858df22bb30d2efbef39a177c28c15c600c885 (diff) | |
Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)
Avoid Anomaly (or Assert False) when a module signature contains
an applied functor followed by a "with Definition" or "with Module"
Also fix the dependency computation in presence of a "with Definition"
Concerning 4720, the code extracted out of this bug report was suboptimal
in Coq 8.4 (it was compilable, but could have probably been tweaked into a
real issue producing faulty code).
But the example of 4720 (and some variants of it) was broken since 8.5,
for the same reasons as 5177 and 5240. And the good news is that after
these repairs, the example of bug 4720 is now extracted to correct code
(the "with" is preserved).
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index a896a8d037..1e0c331901 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -17,10 +17,15 @@ open Mlutil (*S Functions upon ML modules. *) +(** Note: a syntax like [(F M) with ...] is actually legal, see for instance + bug #4720. Hence the code below tries to handle [MTsig], maybe not in + a perfect way, but that should be enough for the use of [se_iter] below. *) + let rec msid_of_mt = function | MTident mp -> mp + | MTsig(mp,_) -> mp | MTwith(mt,_)-> msid_of_mt mt - | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.") + | MTfunsig _ -> assert false (* A functor cannot be inside a MTwith *) (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -36,7 +41,7 @@ let se_iter do_decl do_spec do_mp = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in - mt_iter mt; do_decl (Dtype(r,l,t)) + mt_iter mt; do_spec (Stype(r,l,Some t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in let mp_w = |