diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 126 |
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; |