summaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /plugins/extraction
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml11
-rw-r--r--plugins/extraction/modutil.ml11
2 files changed, 17 insertions, 5 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 73062328..83ebb139 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -155,7 +155,9 @@ let factor_fix env l cb msb =
function
| (l,SFBconst cb') ->
let check' = check_fix env cb' (j+1) in
- if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible;
+ if not (fst check = fst check' &&
+ prec_declaration_equal (snd check) (snd check'))
+ then raise Impossible;
labels.(j+1) <- l;
| _ -> raise Impossible) msb';
labels, recd, msb''
@@ -196,13 +198,14 @@ let rec msid_of_seb = function
| SEBwith (seb,_) -> msid_of_seb seb
| _ -> assert false
-let env_for_mtb_with env mp seb idl =
+let env_for_mtb_with_def env mp seb idl =
let sig_b = match seb with
| SEBstruct(sig_b) -> sig_b
| _ -> assert false
in
let l = label_of_id (List.hd idl) in
- let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in
+ let spot = function (l',SFBconst _) -> l = l' | _ -> false in
+ let before = fst (list_split_when spot sig_b) in
Modops.add_signature mp before empty_delta_resolver env
(* From a [structure_body] (i.e. a list of [structure_field_body])
@@ -241,7 +244,7 @@ let rec extract_sfb_spec env mp = function
and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
| SEBident mp -> Visit.add_mp_all mp; MTident mp
| SEBwith(seb',With_definition_body(idl,cb))->
- let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in
+ let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in
let mt = extract_seb_spec env mp1 (seb,seb') in
(match extract_with_type env' cb with (* cb peut contenir des kn *)
| None -> mt
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9e8dd828..4e0dbcab 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -194,6 +194,15 @@ let signature_of_structure s =
(*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
+let is_modular = function
+ | SEdecl _ -> false
+ | SEmodule _ | SEmodtype _ -> true
+
+let rec search_structure l m = function
+ | [] -> raise Not_found
+ | (lab,d)::_ when lab=l && is_modular d = m -> d
+ | _::fields -> search_structure l m fields
+
let get_decl_in_structure r struc =
try
let base_mp,ll = labels_of_ref r in
@@ -202,7 +211,7 @@ let get_decl_in_structure r struc =
let rec go ll sel = match ll with
| [] -> assert false
| l :: ll ->
- match List.assoc l sel with
+ match search_structure l (ll<>[]) sel with
| SEdecl d -> d
| SEmodtype m -> assert false
| SEmodule m ->