summaryrefslogtreecommitdiff
path: root/toplevel/indschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/indschemes.ml')
-rw-r--r--toplevel/indschemes.ml126
1 files changed, 77 insertions, 49 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index b9888dcd..e6b23828 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -15,7 +15,7 @@
declaring new schemes *)
open Pp
-open Flags
+open Errors
open Util
open Names
open Declarations
@@ -26,13 +26,11 @@ open Decl_kinds
open Indrec
open Declare
open Libnames
+open Globnames
open Goptions
open Nameops
open Termops
-open Typeops
-open Inductiveops
open Pretyping
-open Topconstr
open Nametab
open Smartlocate
open Vernacexpr
@@ -53,6 +51,24 @@ let _ =
optread = (fun () -> !elim_flag) ;
optwrite = (fun b -> elim_flag := b) }
+let bifinite_elim_flag = ref false
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "automatic declaration of induction schemes for non-recursive types";
+ optkey = ["Nonrecursive";"Elimination";"Schemes"];
+ optread = (fun () -> !bifinite_elim_flag) ;
+ optwrite = (fun b -> bifinite_elim_flag := b) }
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = true; (* compatibility 2014-09-03*)
+ optname = "automatic declaration of induction schemes for non-recursive types";
+ optkey = ["Record";"Elimination";"Schemes"];
+ optread = (fun () -> !bifinite_elim_flag) ;
+ optwrite = (fun b -> bifinite_elim_flag := b) }
+
let case_flag = ref false
let _ =
declare_bool_option
@@ -69,7 +85,7 @@ let _ =
{ optsync = true;
optdepr = false;
optname = "automatic declaration of boolean equality";
- optkey = ["Boolean";"Equality";"Schemes"];
+ optkey = ["Equality";"Schemes"];
optread = (fun () -> !eq_flag) ;
optwrite = (fun b -> eq_flag := b) }
let _ = (* compatibility *)
@@ -105,14 +121,19 @@ let _ =
(* Util *)
-let define id internal c t =
+let define id internal ctx c t =
let f = declare_constant ~internal in
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = t;
- const_entry_opaque = false },
+ const_entry_polymorphic = true;
+ const_entry_universes = Evd.universe_context ctx;
+ const_entry_opaque = false;
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ },
Decl_kinds.IsDefinition Scheme) in
definition_message id;
kn
@@ -128,7 +149,7 @@ let alarm what internal msg =
| KernelVerbose
| KernelSilent ->
(if debug then
- Flags.if_warn Pp.msg_warning
+ msg_warning
(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
| _ -> errorlabstrm "" msg
@@ -161,14 +182,15 @@ let try_declare_scheme what f internal names kn =
alarm what internal (msg ++ str ".")
| e when Errors.noncritical e ->
alarm what internal
- (str "Unknown exception during scheme creation.")
+ (str "Unknown exception during scheme creation: "++
+ str (Printexc.to_string e))
let beq_scheme_msg mind =
let mib = Global.lookup_mind mind in
(* TODO: mutual inductive case *)
str "Boolean equality on " ++
pr_enum (fun ind -> quote (Printer.pr_inductive (Global.env()) ind))
- (list_tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
+ (List.init (Array.length mib.mind_packets) (fun i -> (mind,i)))
let declare_beq_scheme_with l kn =
try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
@@ -185,12 +207,12 @@ let declare_beq_scheme = declare_beq_scheme_with []
let declare_one_case_analysis_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
- let dep = if kind = InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
+ let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
let kelim = elim_sorts (mib,mip) in
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
apropriate type *)
- if List.mem InType kelim then
+ if Sorts.List.mem InType kelim then
ignore (define_individual_scheme dep KernelVerbose None ind)
(* Induction/recursion schemes *)
@@ -208,18 +230,18 @@ let kinds_from_type =
let declare_one_induction_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
- let from_prop = kind = InProp in
+ let from_prop = kind == InProp in
let kelim = elim_sorts (mib,mip) in
let elims =
- list_map_filter (fun (sort,kind) ->
- if List.mem sort kelim then Some kind else None)
+ List.map_filter (fun (sort,kind) ->
+ if Sorts.List.mem sort kelim then Some kind else None)
(if from_prop then kinds_from_prop else kinds_from_type) in
List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind))
elims
let declare_induction_schemes kn =
let mib = Global.lookup_mind kn in
- if mib.mind_finite then begin
+ if mib.mind_finite <> Decl_kinds.CoFinite then begin
for i = 0 to Array.length mib.mind_packets - 1 do
declare_one_induction_scheme (kn,i);
done;
@@ -229,7 +251,7 @@ let declare_induction_schemes kn =
let declare_eq_decidability_gen internal names kn =
let mib = Global.lookup_mind kn in
- if mib.mind_finite then
+ if mib.mind_finite <> Decl_kinds.CoFinite then
ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
@@ -271,7 +293,7 @@ let declare_congr_scheme ind =
then
ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
else
- msg_warn "Cannot build congruence scheme because eq is not found"
+ msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
end
let declare_sym_scheme ind =
@@ -281,6 +303,7 @@ let declare_sym_scheme ind =
(* Scheme command *)
+let smart_global_inductive y = smart_global_inductive y
let rec split_scheme l =
let env = Global.env() in
match l with
@@ -300,7 +323,7 @@ requested
let names inds recs isdep y z =
let ind = smart_global_inductive y in
let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
- let z' = family_of_sort (interp_sort z) in
+ let z' = interp_elimination_sort z in
let suffix = (
match sort_of_ind with
| InProp ->
@@ -323,7 +346,7 @@ requested
| InType -> recs ^ "t_nodep")
) in
let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
- let newref = (dummy_loc,newid) in
+ let newref = (Loc.ghost,newid) in
((newref,isdep,ind,z)::l1),l2
in
match t with
@@ -334,18 +357,20 @@ requested
let do_mutual_induction_scheme lnamedepindsort =
let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
- and sigma = Evd.empty
and env0 = Global.env() in
- let lrecspec =
- List.map
- (fun (_,dep,ind,sort) -> (ind,dep,interp_elimination_sort sort))
- lnamedepindsort
+ let sigma, lrecspec =
+ List.fold_right
+ (fun (_,dep,ind,sort) (evd, l) ->
+ let evd, indu = Evd.fresh_inductive_instance env0 evd ind in
+ (evd, (indu,dep,interp_elimination_sort sort) :: l))
+ lnamedepindsort (Evd.from_env env0,[])
in
- let listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
- let rec declare decl fi lrecref =
- let decltype = Retyping.get_type_of env0 Evd.empty decl in
- let decltype = refresh_universes decltype in
- let cst = define fi UserVerbose decl (Some decltype) in
+ let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
+ let declare decl fi lrecref =
+ let decltype = Retyping.get_type_of env0 sigma decl in
+ (* let decltype = refresh_universes decltype in *)
+ let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in
+ let cst = define fi UserVerbose sigma proof_output (Some decltype) in
ConstRef cst :: lrecref
in
let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -354,25 +379,25 @@ let do_mutual_induction_scheme lnamedepindsort =
let get_common_underlying_mutual_inductive = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
- match List.filter (fun (_,(mind',_)) -> mind <> mind') l with
+ match List.filter (fun (_,(mind',_)) -> not (eq_mind mind mind')) l with
| (_,ind')::_ ->
raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
| [] ->
- if not (list_distinct (List.map snd (List.map snd all))) then
- error "A type occurs twice";
+ if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
+ then error "A type occurs twice";
mind,
- list_map_filter
+ List.map_filter
(function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
let do_scheme l =
let ischeme,escheme = split_scheme l in
(* we want 1 kind of scheme at a time so we check if the user
tried to declare different schemes at once *)
- if (ischeme <> []) && (escheme <> [])
+ if not (List.is_empty ischeme) && not (List.is_empty escheme)
then
error "Do not declare equality and induction scheme at the same time."
else (
- if ischeme <> [] then do_mutual_induction_scheme ischeme
+ if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme
else
let mind,l = get_common_underlying_mutual_inductive escheme in
declare_beq_scheme_with l mind;
@@ -385,17 +410,19 @@ tried to declare different schemes at once *)
let list_split_rev_at index l =
let rec aux i acc = function
- hd :: tl when i = index -> acc, tl
+ hd :: tl when Int.equal i index -> acc, tl
| hd :: tl -> aux (succ i) (hd :: acc) tl
- | [] -> failwith "list_split_when: Invalid argument"
+ | [] -> failwith "List.split_when: Invalid argument"
in aux 0 [] l
let fold_left' f = function
- [] -> raise (Invalid_argument "fold_left'")
+ [] -> invalid_arg "fold_left'"
| hd :: tl -> List.fold_left f hd tl
let build_combined_scheme env schemes =
- let defs = List.map (fun cst -> (cst, Typeops.type_of_constant env cst)) schemes in
+ let defs = List.map (fun cst -> (* FIXME *)
+ let evd, c = Evd.fresh_constant_instance env Evd.empty cst in
+ (c, Typeops.type_of_constant_in env c)) schemes in
(* let nschemes = List.length schemes in *)
let find_inductive ty =
let (ctx, arity) = decompose_prod ty in
@@ -403,7 +430,7 @@ let build_combined_scheme env schemes =
match kind_of_term last with
| App (ind, args) ->
let ind = destInd ind in
- let (_,spec) = Inductive.lookup_mind_specif env ind in
+ let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
ctx, ind, spec.mind_nrealargs
| _ -> ctx, destInd last, 0
in
@@ -414,8 +441,8 @@ let build_combined_scheme env schemes =
let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
let relargs = rel_vect 0 prods in
let concls = List.rev_map
- (fun (cst, t) ->
- mkApp(mkConst cst, relargs),
+ (fun (cst, t) -> (* FIXME *)
+ mkApp(mkConstU cst, relargs),
snd (decompose_prod_n prods t)) defs in
let concl_bod, concl_typ =
fold_left'
@@ -440,18 +467,19 @@ let do_combined_scheme name schemes =
schemes
in
let body,typ = build_combined_scheme (Global.env ()) csts in
- ignore (define (snd name) UserVerbose body (Some typ));
+ let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in
+ ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ));
fixpoint_message None [snd name]
(**********************************************************************)
let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
-let mutual_inductive_size kn = Array.length (Global.lookup_mind kn).mind_packets
-
let declare_default_schemes kn =
- let n = mutual_inductive_size kn in
- if !elim_flag then declare_induction_schemes kn;
+ let mib = Global.lookup_mind kn in
+ let n = Array.length mib.mind_packets in
+ if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) then
+ declare_induction_schemes kn;
if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
if is_eq_flag() then try_declare_beq_scheme kn;
if !eq_dec_flag then try_declare_eq_decidability kn;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 01:38:52 +0000