diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 460 |
1 files changed, 460 insertions, 0 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml new file mode 100644 index 00000000..58f77b90 --- /dev/null +++ b/toplevel/indschemes.ml @@ -0,0 +1,460 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id$ *) + +(* Created by Hugo Herbelin from contents related to inductive schemes + initially developed by Christine Paulin (induction schemes), Vincent + Siles (decidable equality and boolean equality) and Matthieu Sozeau + (combined scheme) in file command.ml, Sep 2009 *) + +(* This file provides entry points for manually or automatically + declaring new schemes *) + +open Pp +open Flags +open Util +open Names +open Declarations +open Entries +open Term +open Inductive +open Decl_kinds +open Indrec +open Declare +open Libnames +open Goptions +open Nameops +open Termops +open Typeops +open Inductiveops +open Pretyping +open Topconstr +open Nametab +open Smartlocate +open Vernacexpr +open Ind_tables +open Auto_ind_decl +open Eqschemes +open Elimschemes + +(* Flags governing automatic synthesis of schemes *) + +let elim_flag = ref true +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of induction schemes"; + optkey = ["Elimination";"Schemes"]; + optread = (fun () -> !elim_flag) ; + optwrite = (fun b -> elim_flag := b) } + +let case_flag = ref true +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of case analysis schemes"; + optkey = ["Case";"Analysis";"Schemes"]; + optread = (fun () -> !case_flag) ; + optwrite = (fun b -> case_flag := b) } + +let eq_flag = ref true +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of boolean equality"; + optkey = ["Boolean";"Equality";"Schemes"]; + optread = (fun () -> !eq_flag) ; + optwrite = (fun b -> eq_flag := b) } +let _ = (* compatibility *) + declare_bool_option + { optsync = true; + optname = "automatic declaration of boolean equality"; + optkey = ["Equality";"Scheme"]; + optread = (fun () -> !eq_flag) ; + optwrite = (fun b -> eq_flag := b) } + +let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2 + +let eq_dec_flag = ref false +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of decidable equality"; + optkey = ["Decidable";"Equality";"Schemes"]; + optread = (fun () -> !eq_dec_flag) ; + optwrite = (fun b -> eq_dec_flag := b) } + +let rewriting_flag = ref false +let _ = + declare_bool_option + { optsync = true; + optname ="automatic declaration of rewriting schemes for equality types"; + optkey = ["Rewriting";"Schemes"]; + optread = (fun () -> !rewriting_flag) ; + optwrite = (fun b -> rewriting_flag := b) } + +(* Util *) + +let define id internal c t = + (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *) + let f = match internal with + | KernelSilent -> declare_internal_constant + | _ -> declare_constant in + let kn = f id + (DefinitionEntry + { const_entry_body = c; + const_entry_type = t; + const_entry_opaque = false; + const_entry_boxed = Flags.boxed_definitions() }, + Decl_kinds.IsDefinition Scheme) in + definition_message id; + kn + +(* Boolean equality *) + +let declare_beq_scheme_gen internal names kn = + ignore (define_mutual_scheme beq_scheme_kind internal names kn) + +let alarm what internal msg = + let debug = false in + (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *) + match internal with + | KernelSilent -> + (if debug then + Flags.if_verbose Pp.msg_warning + (hov 0 msg ++ fnl () ++ what ++ str " not defined.")) + | _ -> errorlabstrm "" msg + +let try_declare_scheme what f internal names kn = + try f internal names kn + with + | ParameterWithoutEquality cst -> + alarm what internal + (str "Boolean equality not found for parameter " ++ pr_con cst ++ + str".") + | InductiveWithProduct -> + alarm what internal + (str "Unable to decide equality of functional arguments.") + | InductiveWithSort -> + alarm what internal + (str "Unable to decide equality of type arguments.") + | NonSingletonProp ind -> + alarm what internal + (str "Cannot extract computational content from proposition " ++ + quote (Printer.pr_inductive (Global.env()) ind) ++ str ".") + | EqNotFound (ind',ind) -> + alarm what internal + (str "Boolean equality on " ++ + quote (Printer.pr_inductive (Global.env()) ind') ++ + strbrk " is missing.") + | UndefinedCst s -> + alarm what internal + (strbrk "Required constant " ++ str s ++ str " undefined.") + | AlreadyDeclared msg -> + alarm what internal (msg ++ str ".") + | _ -> + alarm what internal + (str "Unknown exception during scheme creation.") + +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)) + +let declare_beq_scheme_with l kn = + try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn + +(* TODO : maybe switch to KernelVerbose to have the right behaviour *) +let try_declare_beq_scheme kn = + (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle + proof-irrelevance; improve decidability by depending on decidability + for the parameters rather than on the bl and lb properties *) + try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn + +let declare_beq_scheme = declare_beq_scheme_with [] + +(* Case analysis schemes *) +(* TODO: maybe switch to KernelVerbose *) +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 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 + ignore (define_individual_scheme dep KernelSilent None ind) + +(* Induction/recursion schemes *) + +let kinds_from_prop = + [InType,rect_scheme_kind_from_prop; + InProp,ind_scheme_kind_from_prop; + InSet,rec_scheme_kind_from_prop] + +let kinds_from_type = + [InType,rect_dep_scheme_kind_from_type; + InProp,ind_dep_scheme_kind_from_type; + InSet,rec_dep_scheme_kind_from_type] + + (* TODO: maybe switch to kernel verbose *) +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 kelim = elim_sorts (mib,mip) in + let elims = + list_map_filter (fun (sort,kind) -> + if 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 KernelSilent None ind)) + elims + +let declare_induction_schemes kn = + let mib = Global.lookup_mind kn in + if mib.mind_finite then begin + for i = 0 to Array.length mib.mind_packets - 1 do + declare_one_induction_scheme (kn,i); + done; + end + +(* Decidable equality *) + +let declare_eq_decidability_gen internal names kn = + let mib = Global.lookup_mind kn in + if mib.mind_finite then + ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn) + +let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) + str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind) + +let declare_eq_decidability_scheme_with l kn = + try_declare_scheme (eq_dec_scheme_msg (kn,0)) + declare_eq_decidability_gen UserVerbose l kn + +(* TODO: maybe switch to kernel verbose *) +let try_declare_eq_decidability kn = + try_declare_scheme (eq_dec_scheme_msg (kn,0)) + declare_eq_decidability_gen KernelSilent [] kn + +let declare_eq_decidability = declare_eq_decidability_scheme_with [] + +let ignore_error f x = try ignore (f x) with _ -> () + +let declare_rewriting_schemes ind = + if Hipattern.is_inductive_equality ind then begin + ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind); + ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind); + ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind + KernelSilent None ind); + (* These ones expect the equality to be symmetric; the first one also *) + (* needs eq *) + ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind; + ignore_error + (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind; + ignore_error + (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind + end + +(* TODO: maybe switch to kernel verbose *) +let declare_congr_scheme ind = + if Hipattern.is_equality_type (mkInd ind) then begin + if + try Coqlib.check_required_library Coqlib.logic_module_name; true + with _ -> false + then + ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind) + else + warning "Cannot build congruence scheme because eq is not found" + end + +(* TODO: maybe switch to kernel verbose *) +let declare_sym_scheme ind = + if Hipattern.is_inductive_equality ind then + (* Expect the equality to be symmetric *) + ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind + +(* Scheme command *) + +let rec split_scheme l = + let env = Global.env() in + match l with + | [] -> [],[] + | (Some id,t)::q -> let l1,l2 = split_scheme q in + ( match t with + | InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2 + | EqualityScheme x -> l1,((Some id,smart_global_inductive x)::l2) + ) +(* + if no name has been provided, we build one from the types of the ind +requested +*) + | (None,t)::q -> + let l1,l2 = split_scheme q in + ( match t with + | InductionScheme (x,y,z) -> + let ind = smart_global_inductive y in + let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in + let z' = family_of_sort (interp_sort z) in + let suffix = ( + match sort_of_ind with + | InProp -> + if x then (match z' with + | InProp -> "_ind_nodep" + | InSet -> "_rec_nodep" + | InType -> "_rect_nodep") + else ( match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + | _ -> + if x then (match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + else (match z' with + | InProp -> "_ind_dep" + | InSet -> "_rec_dep" + | InType -> "_rect_dep") + ) in + let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newref = (dummy_loc,newid) in + ((newref,x,ind,z)::l1),l2 + | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2) + ) + +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 + 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 + ConstRef cst :: lrecref + in + let _ = List.fold_right2 declare listdecl lrecnames [] in + fixpoint_message None lrecnames + +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 + | (_,ind')::_ -> + raise (RecursionSchemeError (NotMutualInScheme (ind,ind'))) + | [] -> + if not (list_distinct (List.map snd (List.map snd all))) then + error "A type occurs twice"; + mind, + 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 <> []) + then + error "Do not declare equality and induction scheme at the same time." + else ( + if ischeme <> [] then do_mutual_induction_scheme ischeme + else + let mind,l = get_common_underlying_mutual_inductive escheme in + declare_beq_scheme_with l mind; + declare_eq_decidability_scheme_with l mind + ) + +(**********************************************************************) +(* Combined scheme *) +(* Matthieu Sozeau, Dec 2006 *) + +let list_split_rev_at index l = + let rec aux i acc = function + hd :: tl when i = index -> acc, tl + | hd :: tl -> aux (succ i) (hd :: acc) tl + | [] -> failwith "list_split_when: Invalid argument" + in aux 0 [] l + +let fold_left' f = function + [] -> raise (Invalid_argument "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 nschemes = List.length schemes in *) + let find_inductive ty = + let (ctx, arity) = decompose_prod ty in + let (_, last) = List.hd ctx in + match kind_of_term last with + | App (ind, args) -> + let ind = destInd ind in + let (_,spec) = Inductive.lookup_mind_specif env ind in + ctx, ind, spec.mind_nrealargs + | _ -> ctx, destInd last, 0 + in + let (c, t) = List.hd defs in + let ctx, ind, nargs = find_inductive t in + (* Number of clauses, including the predicates quantification *) + let prods = nb_prod t - (nargs + 1) in + 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), + snd (decompose_prod_n prods t)) defs in + let concl_bod, concl_typ = + fold_left' + (fun (accb, acct) (cst, x) -> + mkApp (coqconj, [| x; acct; cst; accb |]), + mkApp (coqand, [| x; acct |])) concls + in + let ctx, _ = + list_split_rev_at prods + (List.rev_map (fun (x, y) -> x, None, y) ctx) in + let typ = it_mkProd_wo_LetIn concl_typ ctx in + let body = it_mkLambda_or_LetIn concl_bod ctx in + (body, typ) + +let do_combined_scheme name schemes = + let csts = + List.map (fun x -> + let refe = Ident x in + let qualid = qualid_of_reference refe in + try Nametab.locate_constant (snd qualid) + with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")) + schemes + in + let body,typ = build_combined_scheme (Global.env ()) csts in + ignore (define (snd name) UserVerbose body (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; + 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; + if !rewriting_flag then map_inductive_block declare_congr_scheme kn n; + if !rewriting_flag then map_inductive_block declare_sym_scheme kn n; + if !rewriting_flag then map_inductive_block declare_rewriting_schemes kn n |