summaryrefslogtreecommitdiff
path: root/contrib/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/common.ml11
-rw-r--r--contrib/extraction/common.mli2
-rw-r--r--contrib/extraction/extract_env.ml47
-rw-r--r--contrib/extraction/extract_env.mli2
-rw-r--r--contrib/extraction/extraction.ml29
-rw-r--r--contrib/extraction/extraction.mli8
-rw-r--r--contrib/extraction/g_extraction.ml420
-rw-r--r--contrib/extraction/haskell.ml6
-rw-r--r--contrib/extraction/haskell.mli2
-rw-r--r--contrib/extraction/miniml.mli2
-rw-r--r--contrib/extraction/mlutil.ml38
-rw-r--r--contrib/extraction/mlutil.mli4
-rw-r--r--contrib/extraction/modutil.ml41
-rw-r--r--contrib/extraction/modutil.mli3
-rw-r--r--contrib/extraction/ocaml.ml11
-rw-r--r--contrib/extraction/ocaml.mli2
-rw-r--r--contrib/extraction/scheme.ml2
-rw-r--r--contrib/extraction/scheme.mli2
-rw-r--r--contrib/extraction/table.ml76
-rw-r--r--contrib/extraction/table.mli21
20 files changed, 185 insertions, 144 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 8e441613..8d8438dc 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: common.ml,v 1.51.2.4 2005/12/16 03:07:39 letouzey Exp $ i*)
+(*i $Id: common.ml 7651 2005-12-16 03:19:20Z letouzey $ i*)
open Pp
open Util
@@ -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 =
@@ -285,7 +285,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
@@ -317,7 +317,6 @@ module StdParams = struct
(*i TODO: clash possible i*)
list_firstn ((mp_length mp)-(mp_length pref)) ls
with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
- let base = base_mp mp in
if !modular && (at_toplevel mp)
then snd (list_sep_last ls)
else ls
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 3e5efa0c..2ba51e1c 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: common.mli,v 1.19.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: common.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
open Names
open Miniml
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index d725a1d7..c581c620 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.ml,v 1.74.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: extract_env.ml 6328 2004-11-18 17:31:41Z sacerdot $ i*)
open Term
open Declarations
@@ -19,6 +19,7 @@ open Table
open Extraction
open Modutil
open Common
+open Mod_subst
(*s Obtaining Coq environment. *)
@@ -28,7 +29,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 +53,23 @@ 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 =
+ let r =
+ (* if we meet a constructor we must export the inductive definition *)
+ match r with
+ ConstructRef (r,_) -> IndRef r
+ | _ -> r
+ in
+ v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r)
exception Impossible
@@ -102,7 +112,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 +153,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 +163,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 +173,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 +227,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 +280,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 +324,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 +359,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/extract_env.mli b/contrib/extraction/extract_env.mli
index 8ce64342..a09464a1 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.mli,v 1.13.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: extract_env.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*s This module declares the extraction commands. *)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6bfe861f..a4bf973d 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml,v 1.136.2.4 2005/12/01 11:27:15 letouzey Exp $ i*)
+(*i $Id: extraction.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
(*i*)
open Util
@@ -230,7 +230,7 @@ let rec extract_type env db j c args =
(* We try to reduce. *)
let newc = applist (Declarations.force lbody, args) in
extract_type env db j newc []))
- | Ind ((kn,i) as ip) ->
+ | Ind (kn,i) ->
let s = (extract_ind env kn).ind_packets.(i).ip_sign in
extract_type_app env db (IndRef (kn,i),s) args
| Case _ | Fix _ | CoFix _ -> Tunknown
@@ -295,8 +295,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
(* Everything concerning parameters. *)
(* We do that first, since they are common to all the [mib]. *)
let mip0 = mib.mind_packets.(0) in
- let npar = mip0.mind_nparams in
- let epar = push_rel_context mip0.mind_params_ctxt env in
+ let npar = mib.mind_nparams in
+ let epar = push_rel_context mib.mind_params_ctxt env in
(* First pass: we store inductive signatures together with *)
(* their type var list. *)
let packets =
@@ -354,22 +354,22 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let rec names_prod t = match kind_of_term t with
| Prod(n,_,t) -> n::(names_prod t)
| LetIn(_,_,_,t) -> names_prod t
- | Cast(t,_) -> names_prod t
+ | Cast(t,_,_) -> names_prod t
| _ -> []
in
let field_names =
- list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+ list_skipn mib.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
@@ -384,8 +384,8 @@ 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))
- (find_structure ip).s_PROJ
+ (fun kn -> if Cset.mem kn !projs then add_projection n kn))
+ (lookup_structure ip).s_PROJ
with Not_found -> ()
end;
Record field_glob
@@ -419,7 +419,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
@@ -448,7 +448,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
@@ -515,7 +515,7 @@ let rec extract_term env mle mlt c args =
extract_app env mle mlt (extract_fix env mle i recd) args
| CoFix (i,recd) ->
extract_app env mle mlt (extract_fix env mle i recd) args
- | Cast (c, _) -> extract_term env mle mlt c args
+ | Cast (c,_,_) -> extract_term env mle mlt c args
| Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false
(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
@@ -678,7 +678,6 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
end
else
let mi = extract_ind env kn in
- let params_nb = mi.ind_nparams in
let oi = mi.ind_packets.(i) in
let metas = Array.init (List.length oi.ip_vars) new_meta in
(* The extraction of the head. *)
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index fc5782c9..1dfd7e1a 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.mli,v 1.27.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: extraction.mli 6303 2004-11-16 12:37:40Z sacerdot $ i*)
(*s Extraction from Coq terms to Miniml. *)
@@ -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/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 33a6117d..13b29c7b 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -15,10 +15,7 @@ open Pcoq
open Genarg
open Pp
-let pr_mlname _ _ s =
- spc () ++
- (if !Options.v7 && not (Options.do_translate()) then qs s
- else Pptacticnew.qsnew s)
+let pr_mlname _ _ _ s = spc () ++ qs s
ARGUMENT EXTEND mlname
TYPED AS string
@@ -37,21 +34,6 @@ VERNAC ARGUMENT EXTEND language
| [ "Toplevel" ] -> [ Toplevel ]
END
-(* Temporary for translator *)
-if !Options.v7 then
- let pr_language _ _ = function
- | Ocaml -> str " Ocaml"
- | Haskell -> str " Haskell"
- | Scheme -> str " Scheme"
- | Toplevel -> str " Toplevel"
- in
- let globwit_language = Obj.magic rawwit_language in
- let wit_language = Obj.magic rawwit_language in
- Pptactic.declare_extra_genarg_pprule true
- (rawwit_language, pr_language)
- (globwit_language, pr_language)
- (wit_language, pr_language);
-
(* Extraction commands *)
VERNAC COMMAND EXTEND Extraction
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 3834fe81..c4ed364a 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*)
+(*i $Id: haskell.ml 7653 2005-12-16 04:12:26Z letouzey $ i*)
(*s Production of Haskell syntax. *)
@@ -240,11 +240,11 @@ let pp_one_ind ip pl cv =
prlist_with_sep
(fun () -> (str " ")) (pp_type true pl) l))
in
- str (if cv = [||] then "type " else "data ") ++
+ str (if Array.length cv = 0 then "type " else "data ") ++
pp_global (IndRef ip) ++ str " " ++
prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
(if pl = [] then mt () else str " ") ++
- if cv = [||] then str "= () -- empty inductive"
+ if Array.length cv = 0 then str "= () -- empty inductive"
else
(v 0 (str "= " ++
prvect_with_sep (fun () -> fnl () ++ str " | ") pp_constructor
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 822444bd..106f7868 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: haskell.mli,v 1.15.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
+(*i $Id: haskell.mli 7632 2005-12-01 14:35:21Z letouzey $ i*)
open Pp
open Names
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 7c18f9f5..cf722e4e 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*)
+(*i $Id: miniml.mli 6064 2004-09-06 07:49:51Z letouzey $ i*)
(*s Target language for extraction: a core ML called MiniML. *)
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index c01766b0..facab18e 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.ml,v 1.104.2.3 2005/12/01 16:28:04 letouzey Exp $ i*)
+(*i $Id: mlutil.ml 7574 2005-11-17 15:48:45Z letouzey $ i*)
(*i*)
open Pp
@@ -209,8 +209,8 @@ end
(*s Does a section path occur in a ML type ? *)
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
+ | Tmeta {contents = Some t} -> type_mem_kn kn t
+ | 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
@@ -218,7 +218,7 @@ let rec type_mem_kn kn = function
let type_maxvar t =
let rec parse n = function
- | Tmeta _ -> assert false
+ | Tmeta {contents = Some t} -> parse n t
| Tvar i -> max i n
| Tarr (a,b) -> parse (parse n a) b
| Tglob (_,l) -> List.fold_left parse n l
@@ -228,7 +228,7 @@ let type_maxvar t =
(*s From [a -> b -> c] to [[a;b],c]. *)
let rec type_decomp = function
- | Tmeta _ -> assert false
+ | Tmeta {contents = Some t} -> type_decomp t
| Tarr (a,b) -> let l,h = type_decomp b in a::l, h
| a -> [],a
@@ -241,7 +241,7 @@ let rec type_recomp (l,t) = match l with
(*s Translating [Tvar] to [Tvar'] to avoid clash. *)
let rec var2var' = function
- | Tmeta _ -> assert false
+ | Tmeta {contents = Some t} -> var2var' t
| Tvar i -> Tvar' i
| Tarr (a,b) -> Tarr (var2var' a, var2var' b)
| Tglob (r,l) -> Tglob (r, List.map var2var' l)
@@ -252,16 +252,17 @@ type abbrev_map = global_reference -> ml_type option
(*s Delta-reduction of type constants everywhere in a ML type [t].
[env] is a function of type [ml_type_env]. *)
+
let type_expand env t =
let rec expand = function
- | Tmeta _ -> assert false
- | Tglob (r,l) as t ->
+ | Tmeta {contents = Some t} -> expand t
+ | Tglob (r,l) ->
(match env r with
| Some mlt -> expand (type_subst_list l mlt)
| None -> Tglob (r, List.map expand l))
| Tarr (a,b) -> Tarr (expand a, expand b)
| a -> a
- in expand t
+ in if Table.type_expand () then expand t else t
(*s Idem, but only at the top level of implications. *)
@@ -269,7 +270,7 @@ let is_arrow = function Tarr _ -> true | _ -> false
let type_weak_expand env t =
let rec expand = function
- | Tmeta _ -> assert false
+ | Tmeta {contents = Some t} -> expand t
| Tglob (r,l) as t ->
(match env r with
| Some mlt ->
@@ -290,7 +291,7 @@ let type_neq env t t' = (type_expand env t <> type_expand env t')
let type_to_sign env t =
let rec f = function
- | Tmeta _ -> assert false
+ | Tmeta {contents = Some t} -> f t
| Tarr (a,b) -> (Tdummy <> a) :: (f b)
| _ -> []
in f (type_expand env t)
@@ -304,7 +305,7 @@ let type_expunge env t =
let rec f t s =
if List.mem false s then
match t with
- | Tmeta _ -> assert false
+ | Tmeta {contents = Some t} -> f t s
| Tarr (a,b) ->
let t = f b (List.tl s) in
if List.hd s then Tarr (a, t) else t
@@ -377,7 +378,7 @@ let ast_iter f = function
| MLapp (a,l) -> f a; List.iter f l
| MLcons (_,c,l) -> List.iter f l
| MLmagic a -> f a
- | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> ()
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
(*S Operations concerning De Bruijn indices. *)
@@ -594,11 +595,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
@@ -653,7 +655,7 @@ let check_generalizable_case unsafe br =
(*s Do all branches correspond to the same thing? *)
let check_constant_case br =
- if br = [||] then raise Impossible;
+ if Array.length br = 0 then raise Impossible;
let (r,l,t) = br.(0) in
let n = List.length l in
if ast_occurs_itvl 1 n t then raise Impossible;
@@ -1117,7 +1119,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 eaf38778..1ba1df64 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.mli,v 1.47.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: mlutil.mli 6303 2004-11-16 12:37:40Z sacerdot $ i*)
open Util
open Names
@@ -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 54f0c992..ff8daf46 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.ml,v 1.7.2.4 2005/12/01 17:01:22 letouzey Exp $ i*)
+(*i $Id: modutil.ml 7632 2005-12-01 14:35:21Z letouzey $ i*)
open Names
open Declarations
@@ -16,6 +16,7 @@ open Util
open Miniml
open Table
open Mlutil
+open Mod_subst
(*S Functions upon modules missing in [Modops]. *)
@@ -25,8 +26,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 +118,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
@@ -176,7 +185,7 @@ let ast_iter_references do_term do_cons do_type a =
| MLcons (i,r,_) ->
if lang () = Ocaml then record_iter_references do_term i;
do_cons r
- | MLcase (i,_,v) as a ->
+ | MLcase (i,_,v) ->
if lang () = Ocaml then record_iter_references do_term i;
Array.iter (fun (r,_,_) -> do_cons r) v
| _ -> ()
@@ -307,8 +316,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 +344,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 +364,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 +378,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 +396,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 +415,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/modutil.mli b/contrib/extraction/modutil.mli
index 7f8c4113..f5208c0d 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.mli,v 1.2.2.2 2005/12/01 17:01:22 letouzey Exp $ i*)
+(*i $Id: modutil.mli 7632 2005-12-01 14:35:21Z letouzey $ i*)
open Names
open Declarations
open Environ
open Libnames
open Miniml
+open Mod_subst
(*s Functions upon modules missing in [Modops]. *)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index ff9cfd21..a0620d72 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*)
+(*i $Id: ocaml.ml 7632 2005-12-01 14:35:21Z letouzey $ i*)
(*s Production of Ocaml syntax. *)
@@ -264,7 +264,6 @@ let rec pp_expr par env args =
let tuple = pp_tuple (pp_expr true env []) args' in
pp_par par (pp_global r ++ spc () ++ tuple)
| MLcase (i, t, pv) ->
- let r,_,_ = pv.(0) in
let expr = if i = Coinductive then
(str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
else
@@ -409,7 +408,7 @@ let pp_one_ind prefix ip pl cv =
(fun () -> spc () ++ str "* ") (pp_type true pl) l))
in
pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++
- if cv = [||] then str " unit (* empty inductive *)"
+ if Array.length cv = 0 then str " unit (* empty inductive *)"
else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor
(Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv))
@@ -480,13 +479,13 @@ let pp_mind kn i =
let pp_decl mpl =
local_mpl := mpl;
function
- | Dind (kn,i) as d -> pp_mind kn i
+ | Dind (kn,i) -> pp_mind kn i
| Dtype (r, l, t) ->
if is_inline_custom r then failwith "empty phrase"
else
- let pp_r = pp_global r in
+ let pp_r = pp_global r in
let l = rename_tvars keywords l in
- let ids, def = try
+ let ids, def = try
let ids,s = find_type_custom r in
pp_string_parameters ids, str "=" ++ spc () ++ str s
with not_found ->
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 5015a50d..8c521ccd 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ocaml.mli,v 1.26.6.3 2005/12/01 17:01:22 letouzey Exp $ i*)
+(*i $Id: ocaml.mli 7632 2005-12-01 14:35:21Z letouzey $ i*)
(*s Some utility functions to be reused in module [Haskell]. *)
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 4a881da2..7004a202 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*)
+(*i $Id: scheme.ml 7651 2005-12-16 03:19:20Z letouzey $ i*)
(*s Production of Scheme syntax. *)
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 2a828fb9..ef4a3a63 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: scheme.mli,v 1.6.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
+(*i $Id: scheme.mli 7632 2005-12-01 14:35:21Z letouzey $ i*)
(*s Some utility functions to be reused in module [Haskell]. *)
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 9d73d13f..bd4fe924 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.ml,v 1.35.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
+(*i $Id: table.ml 6555 2005-01-03 19:25:36Z sacerdot $ i*)
open Names
open Term
@@ -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
@@ -207,6 +221,18 @@ let _ = declare_bool_option
optread = auto_inline;
optwrite = (:=) auto_inline_ref}
+(*s Extraction TypeExpand *)
+
+let type_expand_ref = ref true
+
+let type_expand () = !type_expand_ref
+
+let _ = declare_bool_option
+ {optsync = true;
+ optname = "Extraction TypeExpand";
+ optkey = SecondaryTable ("Extraction", "TypeExpand");
+ optread = type_expand;
+ optwrite = (:=) type_expand_ref}
(*s Extraction Optimize *)
@@ -311,14 +337,22 @@ let add_inline_entries b l =
(* Registration of operations for rollback. *)
-let (inline_extraction,_) =
+let (inline_extraction,_) =
declare_object
{(default_object "Extraction Inline") with
cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
export_function = (fun x -> Some x);
classify_function = (fun (_,o) -> Substitute o);
- subst_function = (fun (_,s,(b,l)) -> (b,(List.map (subst_global s) l))) }
+ (*CSC: The following substitution may istantiate a realized parameter.
+ The right solution would be to make the substitution erase the
+ realizer from the table. However, this is not allowed by Coq.
+ In this particular case, though, keeping the realizer is place seems
+ to be harmless since the current code looks for a realizer only
+ when the constant is a parameter. However, if this behaviour changes
+ subtle bugs can happear in the future. *)
+ subst_function =
+ (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))}
let _ = declare_summary "Extraction Inline"
{ freeze_function = (fun () -> !inline_table);
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 6160452a..66662138 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.mli,v 1.25.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
+(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*)
open Names
open Libnames
@@ -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
@@ -68,6 +71,10 @@ val reset_tables : unit -> unit
val auto_inline : unit -> bool
+(*s TypeExpand parameter *)
+
+val type_expand : unit -> bool
+
(*s Optimize parameter *)
type opt_flag =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 05:43:15 +0000