aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/common.ml8
-rw-r--r--contrib/extraction/extract_env.ml37
-rw-r--r--contrib/extraction/extraction.ml12
-rw-r--r--contrib/extraction/extraction.mli6
-rw-r--r--contrib/extraction/mlutil.ml11
-rw-r--r--contrib/extraction/mlutil.mli2
-rw-r--r--contrib/extraction/modutil.ml36
-rw-r--r--contrib/extraction/table.ml50
-rw-r--r--contrib/extraction/table.mli15
9 files changed, 102 insertions, 75 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0af215f252..359257c886 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -143,7 +143,7 @@ let create_modular_renamings struc =
in
(* 1) creates renamings of objects *)
let add upper r =
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
let l = mp_create_modular_renamings mp in
let s = modular_rename upper (id_of_global r) in
global_ids := Idset.add (id_of_string s) !global_ids;
@@ -184,7 +184,7 @@ let create_modular_renamings struc =
List.iter contents_first_level used_modules;
let used_modules' = List.rev used_modules in
let needs_qualify r =
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
if (is_modfile mp) && mp <> current_module &&
(clash mp [] (List.hd (get_renamings r)) used_modules')
then to_qualify := Refset.add r !to_qualify
@@ -239,7 +239,7 @@ let rec mp_create_mono_renamings mp =
let create_mono_renamings struc =
let { up = u ; down = d } = struct_get_references_list struc in
let add upper r =
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
let l = mp_create_mono_renamings mp in
let mycase = if upper then uppercase_id else lowercase_id in
let id =
@@ -278,7 +278,7 @@ module StdParams = struct
let pp_global mpl r =
let ls = get_renamings r in
let s = List.hd ls in
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
let ls =
if mp = List.hd mpl then [s] (* simpliest situation *)
else
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index f9be3d9b03..78fb578e99 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -28,7 +28,7 @@ let toplevel_env () =
| (_,kn), Lib.Leaf o ->
let mp,_,l = repr_kn kn in
let seb = match Libobject.object_tag o with
- | "CONSTANT" -> SEBconst (Global.lookup_constant kn)
+ | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn))
| "INDUCTIVE" -> SEBmind (Global.lookup_mind kn)
| "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l)))
| "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn)
@@ -52,14 +52,16 @@ let environment_until dir_opt =
| _ -> assert false
in parse (Library.loaded_libraries ())
-type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
+type visit =
+ { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t }
let in_kn v kn = KNset.mem kn v.kn
+let in_ref v ref = Refset.mem ref v.ref
let in_mp v mp = MPset.mem mp v.mp
let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn)
-let visit_ref v r = visit_kn v (kn_of_r r)
+let visit_ref v r = v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r)
exception Impossible
@@ -102,7 +104,7 @@ let get_spec_references v s =
let rec extract_msig env v mp = function
| [] -> []
| (l,SPBconst cb) :: msig ->
- let kn = make_kn mp empty_dirpath l in
+ let kn = make_con mp empty_dirpath l in
let s = extract_constant_spec env kn cb in
if logical_spec s then extract_msig env v mp msig
else begin
@@ -143,9 +145,9 @@ let rec extract_msb env v mp all = function
| (l,SEBconst cb) :: msb ->
(try
let vl,recd,msb = factor_fix env l cb msb in
- let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in
+ let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in
let ms = extract_msb env v mp all msb in
- let b = array_exists (in_kn v) vkn in
+ let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in
if all || b then
let d = extract_fixpoint env vkn recd in
if (not b) && (logical_decl d) then ms
@@ -153,8 +155,8 @@ let rec extract_msb env v mp all = function
else ms
with Impossible ->
let ms = extract_msb env v mp all msb in
- let kn = make_kn mp empty_dirpath l in
- let b = in_kn v kn in
+ let kn = make_con mp empty_dirpath l in
+ let b = in_ref v (ConstRef kn) in
if all || b then
let d = extract_constant env kn cb in
if (not b) && (logical_decl d) then ms
@@ -163,7 +165,7 @@ let rec extract_msb env v mp all = function
| (l,SEBmind mib) :: msb ->
let ms = extract_msb env v mp all msb in
let kn = make_kn mp empty_dirpath l in
- let b = in_kn v kn in
+ let b = in_ref v (IndRef (kn,0)) in (* 0 is dummy *)
if all || b then
let d = Dind (kn, extract_inductive env kn) in
if (not b) && (logical_decl d) then ms
@@ -217,12 +219,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
let mono_environment refs mpl =
let l = environment_until None in
let v =
- let add_kn r = KNset.add (kn_of_r r) in
- let kns = List.fold_right add_kn refs KNset.empty in
+ let add_ref r = Refset.add r in
+ let refs = List.fold_right add_ref refs Refset.empty in
let add_mp mp = MPset.union (prefixes_mp mp) in
let mps = List.fold_right add_mp mpl MPset.empty in
- let mps = KNset.fold (fun k -> add_mp (modpath k)) kns mps in
- { kn = kns; mp = mps }
+ let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in
+ { kn = KNset.empty; ref = refs; mp = mps }
in
let env = Global.env () in
List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m))
@@ -270,10 +272,9 @@ let extraction qid =
else begin
let prm =
{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
- let kn = kn_of_r r in
let struc = optimize_struct prm None (mono_environment [r] []) in
let d = get_decl_in_structure r struc in
- print_one_decl struc (modpath kn) d;
+ print_one_decl struc (modpath_of_r r) d;
reset_tables ()
end
@@ -315,7 +316,7 @@ let extraction_module m =
let b = is_modfile mp in
let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
let l = environment_until None in
- let v = { kn = KNset.empty ; mp = prefixes_mp mp } in
+ let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in
let env = Global.env () in
let struc =
List.rev_map
@@ -350,7 +351,9 @@ let extraction_library is_rec m =
| Scheme -> error_scheme ()
| _ ->
let dir_m = dir_module_of_id m in
- let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in
+ let v =
+ { kn = KNset.empty; ref = Refset.empty;
+ mp = MPset.singleton (MPfile dir_m) } in
let l = environment_until (Some dir_m) in
let struc =
let env = Global.env () in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0bf5d6bcde..52ff05439e 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -358,16 +358,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let field_names =
list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
assert (List.length field_names = List.length typ);
- let projs = ref KNset.empty in
+ let projs = ref Cset.empty in
let mp,d,_ = repr_kn kn in
let rec select_fields l typs = match l,typs with
| [],[] -> []
| (Name id)::l, typ::typs ->
if type_eq (mlt_env env) Tdummy typ then select_fields l typs
else
- let knp = make_kn mp d (label_of_id id) in
+ let knp = make_con mp d (label_of_id id) in
if not (List.mem false (type_to_sign (mlt_env env) typ)) then
- projs := KNset.add knp !projs;
+ projs := Cset.add knp !projs;
(ConstRef knp) :: (select_fields l typs)
| Anonymous::l, typ::typs ->
if type_eq (mlt_env env) Tdummy typ then select_fields l typs
@@ -382,7 +382,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let n = nb_default_params env mip0.mind_nf_arity in
List.iter
(option_iter
- (fun kn -> if KNset.mem kn !projs then add_projection n kn))
+ (fun kn -> if Cset.mem kn !projs then add_projection n kn))
(find_structure ip).s_PROJ
with Not_found -> ()
end;
@@ -417,7 +417,7 @@ and extract_type_cons env db dbmap c i =
and mlt_env env r = match r with
| ConstRef kn ->
(try
- if not (visible_kn kn) then raise Not_found;
+ if not (visible_con kn) then raise Not_found;
match lookup_term kn with
| Dtype (_,vl,mlt) -> Some mlt
| _ -> None
@@ -446,7 +446,7 @@ let type_expunge env = type_expunge (mlt_env env)
let record_constant_type env kn opt_typ =
try
- if not (visible_kn kn) then raise Not_found;
+ if not (visible_con kn) then raise Not_found;
lookup_type kn
with Not_found ->
let typ = match opt_typ with
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 31fdd0580c..b26a577e2d 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -17,12 +17,12 @@ open Environ
open Libnames
open Miniml
-val extract_constant : env -> kernel_name -> constant_body -> ml_decl
+val extract_constant : env -> constant -> constant_body -> ml_decl
-val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec
+val extract_constant_spec : env -> constant -> constant_body -> ml_spec
val extract_fixpoint :
- env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl
+ env -> constant array -> (constr, types) prec_declaration -> ml_decl
val extract_inductive : env -> kernel_name -> ml_ind
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 3d4ab11a67..b8764d85d0 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -210,7 +210,7 @@ end
let rec type_mem_kn kn = function
| Tmeta _ -> assert false
- | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l
+ | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l
| Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
| _ -> false
@@ -594,11 +594,12 @@ let rec linear_beta_red a t = match a,t with
linear beta reductions at modified positions. *)
let rec ast_glob_subst s t = match t with
- | MLapp ((MLglob (ConstRef kn)) as f, a) ->
+ | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
let a = List.map (ast_glob_subst s) a in
- (try linear_beta_red a (KNmap.find kn s)
+ (try linear_beta_red a (Refmap.find refe s)
with Not_found -> MLapp (f, a))
- | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t)
+ | MLglob ((ConstRef kn) as refe) ->
+ (try Refmap.find refe s with Not_found -> t)
| _ -> ast_map (ast_glob_subst s) t
@@ -1117,7 +1118,7 @@ let inline_test t =
let manual_inline_list =
let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in
- List.map (fun s -> (make_kn mp empty_dirpath (mk_label s)))
+ List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))
[ "well_founded_induction_type"; "well_founded_induction";
"Acc_rect"; "Acc_rec" ; "Acc_iter" ]
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index bc4de489d3..05e773c5d8 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -101,7 +101,7 @@ val ast_lift : int -> ml_ast -> ml_ast
val ast_pop : ml_ast -> ml_ast
val ast_subst : ml_ast -> ml_ast -> ml_ast
-val ast_glob_subst : ml_ast KNmap.t -> ml_ast -> ml_ast
+val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
val normalize : ml_ast -> ml_ast
val optimize_fix : ml_ast -> ml_ast
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index caa72b34f4..1a40a83307 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -25,8 +25,9 @@ open Mlutil
let add_structure mp msb env =
let add_one env (l,elem) =
let kn = make_kn mp empty_dirpath l in
+ let con = make_con mp empty_dirpath l in
match elem with
- | SEBconst cb -> Environ.add_constant kn cb env
+ | SEBconst cb -> Environ.add_constant con cb env
| SEBmind mib -> Environ.add_mind kn mib env
| SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env
| SEBmodtype mtb -> Environ.add_modtype kn mtb env
@@ -116,8 +117,15 @@ let rec parse_labels ll = function
let labels_of_mp mp = parse_labels [] mp
-let labels_of_kn kn =
- let mp,_,l = repr_kn kn in parse_labels [l] mp
+let labels_of_ref r =
+ let mp,_,l =
+ match r with
+ ConstRef con -> repr_con con
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> repr_kn kn
+ | VarRef _ -> assert false
+ in
+ parse_labels [l] mp
let rec add_labels_mp mp = function
| [] -> mp
@@ -307,8 +315,7 @@ let signature_of_structure s =
let get_decl_in_structure r struc =
try
- let kn = kn_of_r r in
- let base_mp,ll = labels_of_kn kn in
+ let base_mp,ll = labels_of_ref r in
if not (at_toplevel base_mp) then error_not_visible r;
let sel = List.assoc base_mp struc in
let rec go ll sel = match ll with
@@ -336,16 +343,16 @@ let get_decl_in_structure r struc =
let dfix_to_mlfix rv av i =
let rec make_subst n s =
if n < 0 then s
- else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s)
+ else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
in
- let s = make_subst (Array.length rv - 1) KNmap.empty
+ let s = make_subst (Array.length rv - 1) Refmap.empty
in
let rec subst n t = match t with
- | MLglob (ConstRef kn) ->
- (try MLrel (n + (KNmap.find kn s)) with Not_found -> t)
+ | MLglob ((ConstRef kn) as refe) ->
+ (try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
| _ -> ast_map_lift subst n t
in
- let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in
+ let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
let c = Array.map (subst 0) av
in MLfix(i, ids, c)
@@ -356,7 +363,7 @@ let rec optim prm s = function
| Dterm (r,t,typ) :: l ->
let t = normalize (ast_glob_subst !s t) in
let i = inline r t in
- if i then s := KNmap.add (kn_of_r r) t !s;
+ if i then s := Refmap.add r t !s;
if not i || prm.modular || List.mem r prm.to_appear
then
let d = match optimize_fix t with
@@ -370,10 +377,9 @@ let rec optim prm s = function
let rec optim_se top prm s = function
| [] -> []
| (l,SEdecl (Dterm (r,a,t))) :: lse ->
- let kn = kn_of_r r in
let a = normalize (ast_glob_subst !s a) in
let i = inline r a in
- if i then s := KNmap.add kn a !s;
+ if i then s := Refmap.add r a !s;
if top && i && not prm.modular && not (List.mem r prm.to_appear)
then optim_se top prm s lse
else
@@ -389,7 +395,7 @@ let rec optim_se top prm s = function
let fake_body = MLfix (0,[||],[||]) in
for i = 0 to Array.length rv - 1 do
if inline rv.(i) fake_body
- then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s
+ then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
else all := false
done;
if !all && top && not prm.modular
@@ -408,6 +414,6 @@ and optim_me prm s = function
| MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me)
let optimize_struct prm before struc =
- let subst = ref (KNmap.empty : ml_ast KNmap.t) in
+ let subst = ref (Refmap.empty : ml_ast Refmap.t) in
option_iter (fun l -> ignore (optim prm subst l)) before;
List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 17628698da..7c010ab4f0 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -22,10 +22,23 @@ open Miniml
(*S Utilities concerning [module_path] and [kernel_names] *)
-let kn_of_r r = match r with
- | ConstRef kn -> kn
- | IndRef (kn,_) -> kn
- | ConstructRef ((kn,_),_) -> kn
+let occur_kn_in_ref kn =
+ function
+ | IndRef (kn',_)
+ | ConstructRef ((kn',_),_) -> kn = kn'
+ | ConstRef _ -> false
+ | VarRef _ -> assert false
+
+let modpath_of_r r = match r with
+ | ConstRef kn -> con_modpath kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> modpath kn
+ | VarRef _ -> assert false
+
+let label_of_r r = match r with
+ | ConstRef kn -> con_label kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> label kn
| VarRef _ -> assert false
let current_toplevel () = fst (Lib.current_prefix ())
@@ -45,21 +58,22 @@ let at_toplevel mp =
is_modfile mp || is_toplevel mp
let visible_kn kn = at_toplevel (base_mp (modpath kn))
+let visible_con kn = at_toplevel (base_mp (con_modpath kn))
(*S The main tables: constants, inductives, records, ... *)
(*s Constants tables. *)
-let terms = ref (KNmap.empty : ml_decl KNmap.t)
-let init_terms () = terms := KNmap.empty
-let add_term kn d = terms := KNmap.add kn d !terms
-let lookup_term kn = KNmap.find kn !terms
+let terms = ref (Cmap.empty : ml_decl Cmap.t)
+let init_terms () = terms := Cmap.empty
+let add_term kn d = terms := Cmap.add kn d !terms
+let lookup_term kn = Cmap.find kn !terms
-let types = ref (KNmap.empty : ml_schema KNmap.t)
-let init_types () = types := KNmap.empty
-let add_type kn s = types := KNmap.add kn s !types
-let lookup_type kn = KNmap.find kn !types
+let types = ref (Cmap.empty : ml_schema Cmap.t)
+let init_types () = types := Cmap.empty
+let add_type kn s = types := Cmap.add kn s !types
+let lookup_type kn = Cmap.find kn !types
(*s Inductives table. *)
@@ -70,22 +84,22 @@ let lookup_ind kn = KNmap.find kn !inductives
(*s Recursors table. *)
-let recursors = ref KNset.empty
-let init_recursors () = recursors := KNset.empty
+let recursors = ref Cset.empty
+let init_recursors () = recursors := Cset.empty
let add_recursors env kn =
- let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in
+ let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in
let mib = Environ.lookup_mind kn env in
Array.iter
(fun mip ->
let id = mip.mind_typename in
let kn_rec = make_kn (Nameops.add_suffix id "_rec")
and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
- recursors := KNset.add kn_rec (KNset.add kn_rect !recursors))
+ recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
mib.mind_packets
let is_recursor = function
- | ConstRef kn -> KNset.mem kn !recursors
+ | ConstRef kn -> Cset.mem kn !recursors
| _ -> false
(*s Record tables. *)
@@ -109,7 +123,7 @@ let reset_tables () =
done before. *)
let id_of_global = function
- | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l
+ | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
| IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
| ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
| _ -> assert false
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index d2fcf67d7e..0b69a74120 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -35,7 +35,9 @@ val check_inside_section : unit -> unit
(*s utilities concerning [module_path]. *)
-val kn_of_r : global_reference -> kernel_name
+val occur_kn_in_ref : kernel_name -> global_reference -> bool
+val modpath_of_r : global_reference -> module_path
+val label_of_r : global_reference -> label
val current_toplevel : unit -> module_path
val base_mp : module_path -> module_path
@@ -43,14 +45,15 @@ val is_modfile : module_path -> bool
val is_toplevel : module_path -> bool
val at_toplevel : module_path -> bool
val visible_kn : kernel_name -> bool
+val visible_con : constant -> bool
(*s Some table-related operations *)
-val add_term : kernel_name -> ml_decl -> unit
-val lookup_term : kernel_name -> ml_decl
+val add_term : constant -> ml_decl -> unit
+val lookup_term : constant -> ml_decl
-val add_type : kernel_name -> ml_schema -> unit
-val lookup_type : kernel_name -> ml_schema
+val add_type : constant -> ml_schema -> unit
+val lookup_type : constant -> ml_schema
val add_ind : kernel_name -> ml_ind -> unit
val lookup_ind : kernel_name -> ml_ind
@@ -58,7 +61,7 @@ val lookup_ind : kernel_name -> ml_ind
val add_recursors : Environ.env -> kernel_name -> unit
val is_recursor : global_reference -> bool
-val add_projection : int -> kernel_name -> unit
+val add_projection : int -> constant -> unit
val is_projection : global_reference -> bool
val projection_arity : global_reference -> int
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-16 02:32:52 +0000