diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 767 |
1 files changed, 767 insertions, 0 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml new file mode 100644 index 00000000..685b84fc --- /dev/null +++ b/plugins/extraction/table.ml @@ -0,0 +1,767 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Term +open Declarations +open Nameops +open Namegen +open Summary +open Libobject +open Goptions +open Libnames +open Util +open Pp +open Miniml + +(*S Utilities about [module_path] and [kernel_names] and [global_reference] *) + +let occur_kn_in_ref kn = function + | IndRef (kn',_) + | ConstructRef ((kn',_),_) -> kn = kn' + | ConstRef _ -> false + | VarRef _ -> assert false + +let repr_of_r = function + | ConstRef kn -> repr_con kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> repr_mind kn + | VarRef _ -> assert false + +let modpath_of_r r = + let mp,_,_ = repr_of_r r in mp + +let label_of_r r = + let _,_,l = repr_of_r r in l + +let rec base_mp = function + | MPdot (mp,l) -> base_mp mp + | mp -> mp + +let is_modfile = function + | MPfile _ -> true + | _ -> false + +let raw_string_of_modfile = function + | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f))) + | _ -> assert false + +let rec modfile_of_mp = function + | (MPfile _) as mp -> mp + | MPdot (mp,_) -> modfile_of_mp mp + | _ -> raise Not_found + +let current_toplevel () = fst (Lib.current_prefix ()) + +let is_toplevel mp = + mp = initial_path || mp = current_toplevel () + +let at_toplevel mp = + is_modfile mp || is_toplevel mp + +let rec mp_length mp = + let mp0 = current_toplevel () in + let rec len = function + | mp when mp = mp0 -> 1 + | MPdot (mp,_) -> 1 + len mp + | _ -> 1 + in len mp + +let visible_con kn = at_toplevel (base_mp (con_modpath kn)) + +let rec prefixes_mp mp = match mp with + | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') + | _ -> MPset.singleton mp + +let rec get_nth_label_mp n = function + | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp + | _ -> failwith "get_nth_label: not enough MPdot" + +let common_prefix_from_list mp0 mpl = + let prefixes = prefixes_mp mp0 in + let rec f = function + | [] -> None + | mp :: l -> if MPset.mem mp prefixes then Some mp else f l + in f mpl + +let rec parse_labels ll = function + | MPdot (mp,l) -> parse_labels (l::ll) mp + | mp -> mp,ll + +let labels_of_mp mp = parse_labels [] mp + +let rec parse_labels2 ll mp1 = function + | mp when mp1=mp -> mp,ll + | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp + | mp -> mp,ll + +let labels_of_ref r = + let mp_top = current_toplevel () in + let mp,_,l = repr_of_r r in + parse_labels2 [l] mp_top mp + +let rec add_labels_mp mp = function + | [] -> mp + | l :: ll -> add_labels_mp (MPdot (mp,l)) ll + + +(*S The main tables: constants, inductives, records, ... *) + +(* Theses tables are not registered within coq save/undo mechanism + since we reset their contents at each run of Extraction *) + +(*s Constants tables. *) + +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 (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. *) + +let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t) +let init_inductives () = inductives := Mindmap.empty +let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives +let lookup_ind kn = Mindmap.find kn !inductives + +(*s Recursors table. *) + +let recursors = ref Cset.empty +let init_recursors () = recursors := Cset.empty + +let add_recursors env kn = + let make_kn id = make_con (mind_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 := Cset.add kn_rec (Cset.add kn_rect !recursors)) + mib.mind_packets + +let is_recursor = function + | ConstRef kn -> Cset.mem kn !recursors + | _ -> false + +(*s Record tables. *) + +let projs = ref (Refmap.empty : int Refmap.t) +let init_projs () = projs := Refmap.empty +let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs +let is_projection r = Refmap.mem r !projs +let projection_arity r = Refmap.find r !projs + +(*s Table of used axioms *) + +let info_axioms = ref Refset.empty +let log_axioms = ref Refset.empty +let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty +let add_info_axiom r = info_axioms := Refset.add r !info_axioms +let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms +let add_log_axiom r = log_axioms := Refset.add r !log_axioms + +(*s Extraction mode: modular or monolithic *) + +let modular_ref = ref false + +let set_modular b = modular_ref := b +let modular () = !modular_ref + +(*s Printing. *) + +(* The following functions work even on objects not in [Global.env ()]. + WARNING: for inductive objects, an extract_inductive must have been + done before. *) + +let safe_basename_of_global = function + | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l + | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename + | ConstructRef ((kn,i),j) -> + (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) + | _ -> assert false + +let string_of_global r = + try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) + with _ -> string_of_id (safe_basename_of_global r) + +let safe_pr_global r = str (string_of_global r) + +(* idem, but with qualification, and only for constants. *) + +let safe_pr_long_global r = + try Printer.pr_global r + with _ -> match r with + | ConstRef kn -> + let mp,_,l = repr_con kn in + str ((string_of_mp mp)^"."^(string_of_label l)) + | _ -> assert false + +let pr_long_mp mp = + let lid = repr_dirpath (Nametab.dirpath_of_module mp) in + str (String.concat "." (List.map string_of_id (List.rev lid))) + +let pr_long_global ref = pr_path (Nametab.path_of_global ref) + +(*S Warning and Error messages. *) + +let err s = errorlabstrm "Extraction" s + +let warning_axioms () = + let info_axioms = Refset.elements !info_axioms in + if info_axioms = [] then () + else begin + let s = if List.length info_axioms = 1 then "axiom" else "axioms" in + msg_warning + (str ("The following "^s^" must be realized in the extracted code:") + ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) + ++ str "." ++ fnl ()) + end; + let log_axioms = Refset.elements !log_axioms in + if log_axioms = [] then () + else begin + let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" + in + msg_warning + (str ("The following logical "^s^" encountered:") ++ + hov 1 + (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") + ++ + str "Having invalid logical axiom in the environment when extracting" ++ + spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ + fnl ()) + end + +let warning_both_mod_and_cst q mp r = + msg_warning + (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ + str "do you mean module " ++ + pr_long_mp mp ++ + str " or object " ++ + pr_long_global r ++ str " ?" ++ fnl () ++ + str "First choice is assumed, for the second one please use " ++ + str "fully qualified name." ++ fnl ()) + +let error_axiom_scheme r i = + err (str "The type scheme axiom " ++ spc () ++ + safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ + str " type variable(s).") + +let check_inside_module () = + if Lib.is_modtype () then + err (str "You can't do that within a Module Type." ++ fnl () ++ + str "Close it and try again.") + else if Lib.is_module () then + msg_warning + (str "Extraction inside an opened module is experimental.\n" ++ + str "In case of problem, close it first.\n") + +let check_inside_section () = + if Lib.sections_are_opened () then + err (str "You can't do that within a section." ++ fnl () ++ + str "Close it and try again.") + +let warning_id s = + msg_warning (str ("The identifier "^s^ + " contains __ which is reserved for the extraction")) + +let error_constant r = + err (safe_pr_global r ++ str " is not a constant.") + +let error_inductive r = + err (safe_pr_global r ++ spc () ++ str "is not an inductive type.") + +let error_nb_cons () = + err (str "Not the right number of constructors.") + +let error_module_clash mp1 mp2 = + err (str "The Coq modules " ++ pr_long_mp mp1 ++ str " and " ++ + pr_long_mp mp2 ++ str " have the same ML name.\n" ++ + str "This is not supported yet. Please do some renaming first.") + +let error_unknown_module m = + err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") + +let error_scheme () = + err (str "No Scheme modular extraction available yet.") + +let error_not_visible r = + err (safe_pr_global r ++ str " is not directly visible.\n" ++ + str "For example, it may be inside an applied functor.\n" ++ + str "Use Recursive Extraction to get the whole environment.") + +let error_MPfile_as_mod mp b = + let s1 = if b then "asked" else "required" in + let s2 = if b then "extract some objects of this module or\n" else "" in + err (str ("Extraction of file "^(raw_string_of_modfile mp)^ + ".v as a module is "^s1^".\n"^ + "Monolithic Extraction cannot deal with this situation.\n"^ + "Please "^s2^"use (Recursive) Extraction Library instead.\n")) + +let error_record r = + err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++ + fnl () ++ str "To help extraction, please use an explicit name.") + +let msg_non_implicit r n id = + let name = match id with + | Anonymous -> "" + | Name id -> "(" ^ string_of_id id ^ ") " + in + "The " ^ (ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) + +let error_non_implicit msg = + err (str (msg ^ " still occurs after extraction.") ++ + fnl () ++ str "Please check the Extraction Implicit declarations.") + +let check_loaded_modfile mp = match base_mp mp with + | MPfile dp -> + if not (Library.library_is_loaded dp) then begin + match base_mp (current_toplevel ()) with + | MPfile dp' when dp<>dp' -> + err (str ("Please load library "^(string_of_dirpath dp^" first."))) + | _ -> () + end + | _ -> () + +let info_file f = + Flags.if_verbose message + ("The file "^f^" has been created by extraction.") + + +(*S The Extraction auxiliary commands *) + +(* The objects defined below should survive an arbitrary time, + so we register them to coq save/undo mechanism. *) + +(*s Extraction AutoInline *) + +let auto_inline_ref = ref false + +let auto_inline () = !auto_inline_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction AutoInline"; + optkey = ["Extraction"; "AutoInline"]; + 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 = ["Extraction"; "TypeExpand"]; + optread = type_expand; + optwrite = (:=) type_expand_ref} + +(*s Extraction Optimize *) + +type opt_flag = + { opt_kill_dum : bool; (* 1 *) + opt_fix_fun : bool; (* 2 *) + opt_case_iot : bool; (* 4 *) + opt_case_idr : bool; (* 8 *) + opt_case_idg : bool; (* 16 *) + opt_case_cst : bool; (* 32 *) + opt_case_fun : bool; (* 64 *) + opt_case_app : bool; (* 128 *) + opt_let_app : bool; (* 256 *) + opt_lin_let : bool; (* 512 *) + opt_lin_beta : bool } (* 1024 *) + +let kth_digit n k = (n land (1 lsl k) <> 0) + +let flag_of_int n = + { opt_kill_dum = kth_digit n 0; + opt_fix_fun = kth_digit n 1; + opt_case_iot = kth_digit n 2; + opt_case_idr = kth_digit n 3; + opt_case_idg = kth_digit n 4; + opt_case_cst = kth_digit n 5; + opt_case_fun = kth_digit n 6; + opt_case_app = kth_digit n 7; + opt_let_app = kth_digit n 8; + opt_lin_let = kth_digit n 9; + opt_lin_beta = kth_digit n 10 } + +(* For the moment, we allow by default everything except : + - the type-unsafe optimization [opt_case_idg] + - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta] + (may lead to complexity blow-up, subsumed by finer reductions + when inlining recursors). +*) + +let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*) + +let int_flag_ref = ref int_flag_init +let opt_flag_ref = ref (flag_of_int int_flag_init) + +let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n + +let optims () = !opt_flag_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction Optimize"; + optkey = ["Extraction"; "Optimize"]; + optread = (fun () -> !int_flag_ref <> 0); + optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} + +let _ = declare_int_option + { optsync = true; + optname = "Extraction Flag"; + optkey = ["Extraction";"Flag"]; + optread = (fun _ -> Some !int_flag_ref); + optwrite = (function + | None -> chg_flag 0 + | Some i -> chg_flag (max i 0))} + + +(*s Extraction Lang *) + +type lang = Ocaml | Haskell | Scheme + +let lang_ref = ref Ocaml + +let lang () = !lang_ref + +let (extr_lang,_) = + declare_object + {(default_object "Extraction Lang") with + cache_function = (fun (_,l) -> lang_ref := l); + load_function = (fun _ (_,l) -> lang_ref := l)} + +let _ = declare_summary "Extraction Lang" + { freeze_function = (fun () -> !lang_ref); + unfreeze_function = ((:=) lang_ref); + init_function = (fun () -> lang_ref := Ocaml) } + +let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) + +(*s Extraction Inline/NoInline *) + +let empty_inline_table = (Refset.empty,Refset.empty) + +let inline_table = ref empty_inline_table + +let to_inline r = Refset.mem r (fst !inline_table) + +let to_keep r = Refset.mem r (snd !inline_table) + +let add_inline_entries b l = + let f b = if b then Refset.add else Refset.remove in + let i,k = !inline_table in + inline_table := + (List.fold_right (f b) l i), + (List.fold_right (f (not b)) l k) + +(* Registration of operations for rollback. *) + +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); + classify_function = (fun o -> Substitute o); + 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); + unfreeze_function = ((:=) inline_table); + init_function = (fun () -> inline_table := empty_inline_table) } + +(* Grammar entries. *) + +let extraction_inline b l = + check_inside_section (); + let refs = List.map Nametab.global l in + List.iter + (fun r -> match r with + | ConstRef _ -> () + | _ -> error_constant r) refs; + Lib.add_anonymous_leaf (inline_extraction (b,refs)) + +(* Printing part *) + +let print_extraction_inline () = + let (i,n)= !inline_table in + let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in + msg + (str "Extraction Inline:" ++ fnl () ++ + Refset.fold + (fun r p -> + (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++ + str "Extraction NoInline:" ++ fnl () ++ + Refset.fold + (fun r p -> + (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) n (mt ())) + +(* Reset part *) + +let (reset_inline,_) = + declare_object + {(default_object "Reset Extraction Inline") with + cache_function = (fun (_,_)-> inline_table := empty_inline_table); + load_function = (fun _ (_,_)-> inline_table := empty_inline_table)} + +let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) + +(*s Extraction Implicit *) + +type int_or_id = ArgInt of int | ArgId of identifier + +let implicits_table = ref Refmap.empty + +let implicits_of_global r = + try Refmap.find r !implicits_table with Not_found -> [] + +let add_implicits r l = + let typ = Global.type_of_global r in + let rels,_ = + decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + let names = List.rev_map fst rels in + let n = List.length names in + let check = function + | ArgInt i -> + if 1 <= i && i <= n then i + else err (int i ++ str " is not a valid argument number for " ++ + safe_pr_global r) + | ArgId id -> + (try list_index (Name id) names + with Not_found -> + err (str "No argument " ++ pr_id id ++ str " for " ++ + safe_pr_global r)) + in + let l' = List.map check l in + implicits_table := Refmap.add r l' !implicits_table + +(* Registration of operations for rollback. *) + +let (implicit_extraction,_) = + declare_object + {(default_object "Extraction Implicit") with + cache_function = (fun (_,(r,l)) -> add_implicits r l); + load_function = (fun _ (_,(r,l)) -> add_implicits r l); + classify_function = (fun o -> Substitute o); + subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l)) + } + +let _ = declare_summary "Extraction Implicit" + { freeze_function = (fun () -> !implicits_table); + unfreeze_function = ((:=) implicits_table); + init_function = (fun () -> implicits_table := Refmap.empty) } + +(* Grammar entries. *) + +let extraction_implicit r l = + check_inside_section (); + Lib.add_anonymous_leaf (implicit_extraction (Nametab.global r,l)) + + +(*s Extraction Blacklist of filenames not to use while extracting *) + +let blacklist_table = ref Idset.empty + +let modfile_ids = ref [] +let modfile_mps = ref MPmap.empty + +let reset_modfile () = + modfile_ids := Idset.elements !blacklist_table; + modfile_mps := MPmap.empty + +let string_of_modfile mp = + try MPmap.find mp !modfile_mps + with Not_found -> + let id = id_of_string (raw_string_of_modfile mp) in + let id' = next_ident_away id !modfile_ids in + let s' = string_of_id id' in + modfile_ids := id' :: !modfile_ids; + modfile_mps := MPmap.add mp s' !modfile_mps; + s' + +(* same as [string_of_modfile], but preserves the capital/uncapital 1st char *) + +let file_of_modfile mp = + let s0 = match mp with + | MPfile f -> string_of_id (List.hd (repr_dirpath f)) + | _ -> assert false + in + let s = String.copy (string_of_modfile mp) in + if s.[0] <> s0.[0] then s.[0] <- s0.[0]; + s + +let add_blacklist_entries l = + blacklist_table := + List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s))) + l !blacklist_table + +(* Registration of operations for rollback. *) + +let (blacklist_extraction,_) = + declare_object + {(default_object "Extraction Blacklist") with + cache_function = (fun (_,l) -> add_blacklist_entries l); + load_function = (fun _ (_,l) -> add_blacklist_entries l); + classify_function = (fun o -> Libobject.Keep o); + subst_function = (fun (_,x) -> x) + } + +let _ = declare_summary "Extraction Blacklist" + { freeze_function = (fun () -> !blacklist_table); + unfreeze_function = ((:=) blacklist_table); + init_function = (fun () -> blacklist_table := Idset.empty) } + +(* Grammar entries. *) + +let extraction_blacklist l = + let l = List.rev_map string_of_id l in + Lib.add_anonymous_leaf (blacklist_extraction l) + +(* Printing part *) + +let print_extraction_blacklist () = + msgnl + (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table)) + +(* Reset part *) + +let (reset_blacklist,_) = + declare_object + {(default_object "Reset Extraction Blacklist") with + cache_function = (fun (_,_)-> blacklist_table := Idset.empty); + load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)} + +let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) + +(*s Extract Constant/Inductive. *) + +(* UGLY HACK: to be defined in [extraction.ml] *) +let use_type_scheme_nb_args, register_type_scheme_nb_args = + let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r + +let customs = ref Refmap.empty + +let add_custom r ids s = customs := Refmap.add r (ids,s) !customs + +let is_custom r = Refmap.mem r !customs + +let is_inline_custom r = (is_custom r) && (to_inline r) + +let find_custom r = snd (Refmap.find r !customs) + +let find_type_custom r = Refmap.find r !customs + +let custom_matchs = ref Refmap.empty + +let add_custom_match r s = + custom_matchs := Refmap.add r s !custom_matchs + +let indref_of_match pv = + if Array.length pv = 0 then raise Not_found; + match pv.(0) with + | (ConstructRef (ip,_), _, _) -> IndRef ip + | _ -> raise Not_found + +let is_custom_match pv = + try Refmap.mem (indref_of_match pv) !custom_matchs + with Not_found -> false + +let find_custom_match pv = + Refmap.find (indref_of_match pv) !custom_matchs + +(* Registration of operations for rollback. *) + +let (in_customs,_) = + declare_object + {(default_object "ML extractions") with + cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); + load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); + classify_function = (fun o -> Substitute o); + subst_function = + (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) + } + +let _ = declare_summary "ML extractions" + { freeze_function = (fun () -> !customs); + unfreeze_function = ((:=) customs); + init_function = (fun () -> customs := Refmap.empty) } + +let (in_custom_matchs,_) = + declare_object + {(default_object "ML extractions custom matchs") with + cache_function = (fun (_,(r,s)) -> add_custom_match r s); + load_function = (fun _ (_,(r,s)) -> add_custom_match r s); + classify_function = (fun o -> Substitute o); + subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s)) + } + +let _ = declare_summary "ML extractions custom match" + { freeze_function = (fun () -> !custom_matchs); + unfreeze_function = ((:=) custom_matchs); + init_function = (fun () -> custom_matchs := Refmap.empty) } + +(* Grammar entries. *) + +let extract_constant_inline inline r ids s = + check_inside_section (); + let g = Nametab.global r in + match g with + | ConstRef kn -> + let env = Global.env () in + let typ = Typeops.type_of_constant env kn in + let typ = Reduction.whd_betadeltaiota env typ in + if Reduction.is_arity env typ + then begin + let nargs = use_type_scheme_nb_args env typ in + if List.length ids <> nargs then error_axiom_scheme g nargs + end; + Lib.add_anonymous_leaf (inline_extraction (inline,[g])); + Lib.add_anonymous_leaf (in_customs (g,ids,s)) + | _ -> error_constant g + + +let extract_inductive r s l optstr = + check_inside_section (); + let g = Nametab.global r in + match g with + | IndRef ((kn,i) as ip) -> + let mib = Global.lookup_mind kn in + let n = Array.length mib.mind_packets.(i).mind_consnames in + if n <> List.length l then error_nb_cons (); + Lib.add_anonymous_leaf (inline_extraction (true,[g])); + Lib.add_anonymous_leaf (in_customs (g,[],s)); + Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s))) + optstr; + list_iter_i + (fun j s -> + let g = ConstructRef (ip,succ j) in + Lib.add_anonymous_leaf (inline_extraction (true,[g])); + Lib.add_anonymous_leaf (in_customs (g,[],s))) l + | _ -> error_inductive g + + + +(*s Tables synchronization. *) + +let reset_tables () = + init_terms (); init_types (); init_inductives (); init_recursors (); + init_projs (); init_axioms (); reset_modfile () |