aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml26
-rw-r--r--plugins/extraction/common.mli2
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/ocaml.ml48
-rw-r--r--plugins/extraction/scheme.ml2
6 files changed, 34 insertions, 48 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index ebaa05b53..afa674e9d 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -201,24 +201,19 @@ let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
type visible_layer = { mp : module_path;
content : ((kind*string),unit) Hashtbl.t }
-let pop_visible, push_visible, get_visible, subst_mp =
- let vis = ref [] and sub = ref [empty_subst] in
- register_cleanup (fun () -> vis := []; sub := [empty_subst]);
+let pop_visible, push_visible, get_visible =
+ let vis = ref [] in
+ register_cleanup (fun () -> vis := []);
let pop () =
let v = List.hd !vis in
(* we save the 1st-level-content of MPfile for later use *)
if get_phase () = Impl && modular () && is_modfile v.mp
then add_mpfiles_content v.mp v.content;
- vis := List.tl !vis;
- sub := List.tl !sub
- and push mp o =
- vis := { mp = mp; content = Hashtbl.create 97 } :: !vis;
- let s = List.hd !sub in
- let s = match o with None -> s | Some msid -> add_mp msid mp empty_delta_resolver s in
- sub := s :: !sub
+ vis := List.tl !vis
+ and push mp =
+ vis := { mp = mp; content = Hashtbl.create 97 } :: !vis
and get () = !vis
- and subst mp = subst_mp (List.hd !sub) mp
- in (pop,push,get,subst)
+ in (pop,push,get)
let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
@@ -234,7 +229,7 @@ let add_duplicate, check_duplicate =
incr index;
let ren = "Coq__" ^ string_of_int (!index) in
dups := Gmap.add (mp,l) ren !dups
- and check mp l = Gmap.find (subst_mp mp, l) !dups
+ and check mp l = Gmap.find (mp, l) !dups
in (add,check)
type reset_kind = AllButExternal | Everything
@@ -307,7 +302,7 @@ and mp_renaming =
name in a [string list] form (head is the short name). *)
let ref_renaming_fun (k,r) =
- let mp = subst_mp (modpath_of_r r) in
+ let mp = modpath_of_r r in
let l = mp_renaming mp in
let l = if lang () = Haskell && not (modular ()) then [""] else l in
let s =
@@ -430,7 +425,7 @@ let pp_global k r =
let ls = ref_renaming (k,r) in
assert (List.length ls > 1);
let s = List.hd ls in
- let mp = subst_mp (modpath_of_r r) in
+ let mp = modpath_of_r r in
if mp = top_visible_mp () then
(* simpliest situation: definition of r (or use in the same context) *)
(* we update the visible environment *)
@@ -442,7 +437,6 @@ let pp_global k r =
(* The next function is used only in Ocaml extraction...*)
let pp_module mp =
- let mp = subst_mp mp in
let ls = mp_renaming mp in
if List.length ls = 1 then dottify ls
else match mp with
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 6d33bd8ea..33c14e33a 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -43,7 +43,7 @@ val pp_global : kind -> global_reference -> string
val pp_module : module_path -> string
val top_visible_mp : unit -> module_path
-val push_visible : module_path -> module_path option -> unit
+val push_visible : module_path -> unit
val pop_visible : unit -> unit
val check_duplicate : module_path -> label -> string
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 016bf6778..a426b2274 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -364,7 +364,7 @@ let print_one_decl struc mp decl =
set_phase Pre;
ignore (d.pp_struct struc);
set_phase Impl;
- push_visible mp None;
+ push_visible mp;
msgnl (d.pp_decl decl);
pop_visible ()
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index c199225e4..333bdcddd 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -325,7 +325,7 @@ and pp_module_expr = function
let pp_struct =
let pp_sel (mp,sel) =
- push_visible mp None;
+ push_visible mp;
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 39ec20617..377648422 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -607,8 +607,8 @@ let rec pp_specif = function
pp_alias_spec ren s
with Not_found -> pp_spec s)
| (l,Smodule mt) ->
- let def = pp_module_type (Some l) mt in
- let def' = pp_module_type (Some l) mt in
+ let def = pp_module_type mt in
+ let def' = pp_module_type mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
(try
@@ -616,7 +616,7 @@ let rec pp_specif = function
fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
with Not_found -> Pp.mt ())
| (l,Smodtype mt) ->
- let def = pp_module_type None mt in
+ let def = pp_module_type mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
(try
@@ -624,20 +624,16 @@ let rec pp_specif = function
fnl () ++ str ("module type "^ren^" = ") ++ name
with Not_found -> Pp.mt ())
-and pp_module_type ol = function
+and pp_module_type = function
| MTident kn ->
pp_modname kn
| MTfunsig (mbid, mt, mt') ->
- let typ = pp_module_type None mt in
+ let typ = pp_module_type mt in
let name = pp_modname (MPbound mbid) in
- let def = pp_module_type None mt' in
+ let def = pp_module_type mt' in
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (mp1, sign) ->
- let tvm = top_visible_mp () in
- let mp = match ol with None -> mp1 | Some l -> MPdot (tvm,l) in
- (* References in [sign] are in short form (relative to [msid]).
- In push_visible, [msid-->mp] is added to the current subst. *)
- push_visible mp (Some mp1);
+ push_visible mp1;
let l = map_succeed pp_specif sign in
pop_visible ();
str "sig " ++ fnl () ++
@@ -652,9 +648,9 @@ and pp_module_type ol = function
in
let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l))
in
- push_visible mp_mt None;
+ push_visible mp_mt;
let s =
- pp_module_type None mt ++ str " with type " ++
+ pp_module_type mt ++ str " with type " ++
pp_global Type r ++ ids
in
pop_visible();
@@ -664,9 +660,9 @@ and pp_module_type ol = function
let mp_w =
List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
in
- push_visible mp_mt None;
+ push_visible mp_mt;
let s =
- pp_module_type None mt ++ str " with module " ++ pp_modname mp_w
+ pp_module_type mt ++ str " with module " ++ pp_modname mp_w
in
pop_visible ();
s ++ str " = " ++ pp_modname mp
@@ -685,10 +681,10 @@ let rec pp_structure_elem = function
let typ =
(* virtual printing of the type, in order to have a correct mli later*)
if Common.get_phase () = Pre then
- str ": " ++ pp_module_type (Some l) m.ml_mod_type
+ str ": " ++ pp_module_type m.ml_mod_type
else mt ()
in
- let def = pp_module_expr (Some l) m.ml_mod_expr in
+ let def = pp_module_expr m.ml_mod_expr in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1
(str "module " ++ name ++ typ ++ str " = " ++
@@ -698,7 +694,7 @@ let rec pp_structure_elem = function
fnl () ++ str ("module "^ren^" = ") ++ name
with Not_found -> mt ())
| (l,SEmodtype m) ->
- let def = pp_module_type None m in
+ let def = pp_module_type m in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
(try
@@ -706,21 +702,17 @@ let rec pp_structure_elem = function
fnl () ++ str ("module type "^ren^" = ") ++ name
with Not_found -> mt ())
-and pp_module_expr ol = function
+and pp_module_expr = function
| MEident mp' -> pp_modname mp'
| MEfunctor (mbid, mt, me) ->
let name = pp_modname (MPbound mbid) in
- let typ = pp_module_type None mt in
- let def = pp_module_expr None me in
+ let typ = pp_module_type mt in
+ let def = pp_module_expr me in
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MEapply (me, me') ->
- pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")"
+ pp_module_expr me ++ str "(" ++ pp_module_expr me' ++ str ")"
| MEstruct (mp, sel) ->
- let tvm = top_visible_mp () in
- let mp = match ol with None -> mp | Some l -> MPdot (tvm,l) in
- (* No need to update the subst with [Some msid] below : names are
- already in long form (see [subst_structure] in [Extract_env]). *)
- push_visible mp None;
+ push_visible mp;
let l = map_succeed pp_structure_elem sel in
pop_visible ();
str "struct " ++ fnl () ++
@@ -731,7 +723,7 @@ let do_struct f s =
let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
in
let ppl (mp,sel) =
- push_visible mp None;
+ push_visible mp;
let p = prlist_strict pp sel in
(* for monolithic extraction, we try to simulate the unavailability
of [MPfile] in names by artificially nesting these [MPfile] *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index f7a0b5a53..097df6a61 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -189,7 +189,7 @@ let pp_structure_elem = function
let pp_struct =
let pp_sel (mp,sel) =
- push_visible mp None;
+ push_visible mp;
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 17:14:17 +0000