Permalink
Browse files

Adapt Y. Bertot's path on private inductives (now the keyword is "Pri…

…vate").

A quick and dirty approach to private inductive types
Types for which computable functions are provided, but pattern-matching is disallowed.
This kind of type can be used to simulate simple forms of higher inductive types, with
convertibility for applications of the inductive principle to 0-constructors

Conflicts:
	intf/vernacexpr.mli
	kernel/declarations.ml
	kernel/declarations.mli
	kernel/entries.mli
	kernel/indtypes.ml
	library/declare.ml
	parsing/g_vernac.ml4
	plugins/funind/glob_term_to_relation.ml
	pretyping/indrec.ml
	pretyping/tacred.mli
	printing/ppvernac.ml
	toplevel/vernacentries.ml

Conflicts:
	kernel/declarations.mli
	kernel/declareops.ml
	kernel/indtypes.ml
	kernel/modops.ml
  • Loading branch information...
1 parent 29794b8 commit 8a905458039b631165d068bbf62f88e11eb36eb1 Yves Bertot committed with mattam82 Mar 2, 2013
View
@@ -14,6 +14,8 @@ type binding_kind = Explicit | Implicit
type polymorphic = bool
+type private_flag = bool
+
type theorem_kind =
| Theorem
| Lemma
View
@@ -296,7 +296,7 @@ type vernac_expr =
| VernacExactProof of constr_expr
| VernacAssumption of (locality option * assumption_object_kind) *
inline * simple_binder with_coercion list
- | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of private_flag * inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of
locality option * (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of
View
@@ -172,7 +172,9 @@ type mutual_inductive_body = {
mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
- }
+ mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
+
+}
(** {6 Module declarations } *)
View
@@ -227,7 +227,8 @@ let subst_mind_body sub mib =
Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_polymorphic = mib.mind_polymorphic;
- mind_universes = mib.mind_universes }
+ mind_universes = mib.mind_universes;
+ mind_private = mib.mind_private }
(** {6 Hash-consing of inductive declarations } *)
View
@@ -46,7 +46,8 @@ type mutual_inductive_entry = {
mind_entry_params : (Id.t * local_entry) list;
mind_entry_inds : one_inductive_entry list;
mind_entry_polymorphic : bool;
- mind_entry_universes : Univ.universe_context }
+ mind_entry_universes : Univ.universe_context;
+ mind_entry_private : bool option }
(** {6 Constants (Definition/Axiom) } *)
type proof_output = constr * Declareops.side_effects
View
@@ -628,6 +628,7 @@ let used_section_variables env inds =
(fun l c -> Id.Set.union (Environ.global_vars_set env c) l)
Id.Set.empty inds in
keep_hyps env ids
+
let lift_decl n d =
map_rel_declaration (lift n) d
@@ -660,7 +661,7 @@ let compute_expansion ((kn, _ as ind), u) params ctx =
(Array.map (fun p -> mkProj (p, mkRel 1)) projarr))
in exp, projarr
-let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recargs =
+let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let hyps = used_section_variables env inds in
@@ -743,6 +744,7 @@ let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recarg
mind_packets = packets;
mind_polymorphic = p;
mind_universes = ctx;
+ mind_private = prv;
}
(************************************************************************)
@@ -757,7 +759,7 @@ let check_inductive env kn mie =
(* Then check positivity conditions *)
let (nmr,recargs) = check_positivity kn env_ar params inds in
(* Build the inductive packets *)
- build_inductive env mie.mind_entry_polymorphic
+ build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
mie.mind_entry_universes
env_ar params kn mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs
View
@@ -308,6 +308,11 @@ let rec add_structure mp sign resolver linkinfo env =
Environ.add_constant_key c cb linkinfo env
|SFBmind mib ->
let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
+ let mib =
+ if mib.mind_private != None then
+ { mib with mind_private = Some true }
+ else mib
+ in
Environ.add_mind_key mind (mib,linkinfo) env
|SFBmodule mb -> add_module mb linkinfo env (* adds components as well *)
|SFBmodtype mtb -> Environ.add_modtype mtb env
View
@@ -358,7 +358,8 @@ let dummy_inductive_entry (_,m) = ([],{
mind_entry_finite = true;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
mind_entry_polymorphic = false;
- mind_entry_universes = Univ.UContext.empty })
+ mind_entry_universes = Univ.UContext.empty;
+ mind_entry_private = None })
type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
View
@@ -190,11 +190,11 @@ GEXTEND Gram
| IDENT "Let"; id = identref; b = def_body ->
VernacDefinition ((Some Discharge, Definition), id, b)
(* Gallina inductive declarations *)
- | f = finite_token;
+ | priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
let (k,f) = f in
let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
- VernacInductive (f,false,indl)
+ VernacInductive (priv,f,false,indl)
| "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
VernacFixpoint (None, recs)
| IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -212,13 +212,14 @@ GEXTEND Gram
;
gallina_ext:
- [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
+ [ [ priv = private_token;
+ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
ps = binders;
s = OPT [ ":"; s = lconstr -> s ];
cfs = [ ":="; l = constructor_list_or_record_decl -> l
| -> RecordDecl (None, []) ] ->
let (recf,indf) = b in
- VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),[]])
+ VernacInductive (priv,indf,infer,[((oc,name),ps,s,recf,cfs),[]])
] ]
;
thm_token:
@@ -260,6 +261,9 @@ GEXTEND Gram
infer_token:
[ [ IDENT "Infer" -> true | -> false ] ]
;
+ private_token:
+ [ [ IDENT "Private" -> true | -> false ] ]
+ ;
record_token:
[ [ IDENT "Record" -> (Record,BiFinite)
| IDENT "Structure" -> (Structure,BiFinite)
@@ -1405,7 +1405,7 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true
+ with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) true
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
@@ -1416,7 +1416,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
++ fnl () ++
msg
in
@@ -1431,7 +1431,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
++ fnl () ++
Errors.print reraise
in
View
@@ -884,7 +884,8 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in
+ let mie,impls = Command.interp_mutual_inductive indl []
+ false (*FIXMEnon-poly *) false (* means not private *) true (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
View
@@ -1298,6 +1298,7 @@ and match_current pb (initial,tomatch) =
compile_all_variables initial tomatch pb
| IsInd (_,(IndType(indf,realargs) as indt),names) ->
let mind,_ = dest_ind_family indf in
+ let mind = Tacred.check_privacy pb.env mind in
let cstrs = get_constructors pb.env indf in
let arsign, _ = get_arity pb.env indf in
let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
View
@@ -45,6 +45,15 @@ let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
(* Building curryfied elimination *)
(*******************************************)
+let is_private mib =
+ match mib.mind_private with
+ | Some true -> true
+ | _ -> false
+
+let check_privacy_block mib =
+ if is_private mib then
+ errorlabstrm ""(str"case analysis on a private inductive type")
+
(**********************************************************************)
(* Building case analysis schemes *)
(* Christine Paulin, 1996 *)
@@ -54,12 +63,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
let lnamespar = Vars.subst_univs_context usubst
mib.mind_params_ctxt
in
-
- if not (Sorts.List.mem kind (elim_sorts specif)) then
- raise
- (RecursionSchemeError
- (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)));
-
+ let () = check_privacy_block mib in
+ let () =
+ if not (Sorts.List.mem kind (elim_sorts specif)) then
+ raise
+ (RecursionSchemeError
+ (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)))
+ in
let ndepar = mip.mind_nrealargs_ctxt + 1 in
(* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
View
@@ -1093,14 +1093,18 @@ let pattern_occs loccs_trm env sigma c =
(* Used in several tactics. *)
+let check_privacy env ind =
+ if (fst (Inductive.lookup_mind_specif env (fst ind))).Declarations.mind_private = Some true then
+ errorlabstrm "" (str "case analysis on a private type")
+ else ind
(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
return name, B and t' *)
let reduce_to_ind_gen allow_product env sigma t =
let rec elimrec env t l =
let t = hnf_constr env sigma t in
match kind_of_term (fst (decompose_app t)) with
- | Ind ind-> (ind, it_mkProd_or_LetIn t l)
+ | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
| Prod (n,ty,t') ->
if allow_product then
elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l)
@@ -1111,7 +1115,7 @@ let reduce_to_ind_gen allow_product env sigma t =
was partially the case between V5.10 and V8.1 *)
let t' = whd_betadeltaiota env sigma t in
match kind_of_term (fst (decompose_app t')) with
- | Ind ind-> (ind, it_mkProd_or_LetIn t' l)
+ | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
| _ -> errorlabstrm "" (str"Not an inductive product.")
in
elimrec env t []
View
@@ -14,6 +14,7 @@ open Reductionops
open Pattern
open Globnames
open Locus
+open Univ
type reduction_tactic_error =
InvalidAbstraction of env * constr * (env * Type_errors.type_error)
@@ -106,3 +107,7 @@ val contextually : bool -> occurrences * constr_pattern ->
val e_contextually : bool -> occurrences * constr_pattern ->
(patvar_map -> e_reduction_function) -> e_reduction_function
+
+(** Returns the same inductive if it is allowed for pattern-matching
+ raises an error otherwise. **)
+val check_privacy : env -> inductive puniverses -> inductive puniverses
View
@@ -627,7 +627,7 @@ let rec pr_vernac = function
hov 2
(pr_assumption_token (n > 1) stre ++ spc() ++
pr_ne_params_list pr_lconstr_expr l)
- | VernacInductive (f,i,l) ->
+ | VernacInductive (p,f,i,l) ->
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
View
@@ -126,7 +126,7 @@ let rec classify_vernac e =
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
VtSideff ids, VtLater
| VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
- | VernacInductive (_,_,l) ->
+ | VernacInductive (_,_,_,l) ->
let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
View
@@ -755,7 +755,8 @@ let descend_then sigma env head dirn =
try find_rectype env sigma (get_type_of env sigma head)
with Not_found ->
error "Cannot project on an inductive type derived from a dependency." in
- let (ind,_),_ = dest_ind_family indf in
+ let indp,_ = (dest_ind_family indf) in
+ let ind, _ = check_privacy env indp in
let (mib,mip) = lookup_mind_specif env ind in
let cstr = get_constructors env indf in
let dirn_nlams = cstr.(dirn-1).cs_nargs in
@@ -804,7 +805,8 @@ let construct_discriminator sigma env dirn c sort =
errorlabstrm "Equality.construct_discriminator"
(str "Cannot discriminate on inductive constructors with \
dependent types.") in
- let ((ind,_),_) = dest_ind_family indf in
+ let (indp,_) = dest_ind_family indf in
+ let ind, _ = check_privacy env indp in
let (mib,mip) = lookup_mind_specif env ind in
let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
let deparsign = make_arity_signature env true indf in
View
@@ -412,7 +412,7 @@ let inductive_levels env evdref arities inds =
!evdref (Array.to_list levels') destarities sizes
in evdref := evd; arities
-let interp_mutual_inductive (paramsl,indl) notations poly finite =
+let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
check_all_names_different indl;
let env0 = Global.env() in
let evdref = ref Evd.(from_env env0) in
@@ -487,6 +487,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly finite =
mind_entry_finite = finite;
mind_entry_inds = entries;
mind_entry_polymorphic = poly;
+ mind_entry_private = if prv then Some false else None;
mind_entry_universes = Evd.universe_context evd },
impls
@@ -535,7 +536,7 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
constrimpls)
impls;
if_verbose msg_info (minductive_message names);
- declare_default_schemes mind;
+ if mie.mind_entry_private == None then declare_default_schemes mind;
mind
type one_inductive_impls =
@@ -545,10 +546,10 @@ type one_inductive_impls =
type one_inductive_expr =
lident * local_binder list * constr_expr option * constructor_expr list
-let do_mutual_inductive indl poly finite =
+let do_mutual_inductive indl poly prv finite =
let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
- let mie,impls = interp_mutual_inductive indl ntns poly finite in
+ let mie,impls = interp_mutual_inductive indl ntns poly prv finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
(* Declare the possible notations of inductive types *)
View
@@ -86,7 +86,8 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> polymorphic -> bool(*finite*) ->
+ structured_inductive_expr -> decl_notation list -> polymorphic ->
+ private_flag -> bool(*finite*) ->
mutual_inductive_entry * one_inductive_impls list
(** Registering a mutual inductive definition together with its
@@ -99,7 +100,8 @@ val declare_mutual_inductive_with_eliminations :
(** Entry points for the vernacular commands Inductive and CoInductive *)
val do_mutual_inductive :
- (one_inductive_expr * decl_notation list) list -> polymorphic -> bool -> unit
+ (one_inductive_expr * decl_notation list) list -> polymorphic ->
+ private_flag -> bool -> unit
(** {6 Fixpoints and cofixpoints} *)
View
@@ -102,5 +102,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
mind_entry_params = params';
mind_entry_inds = inds';
mind_entry_polymorphic = mib.mind_polymorphic;
+ mind_entry_private = mib.mind_private;
mind_entry_universes = univs
}
View
@@ -340,6 +340,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f
mind_entry_finite = finite != CoFinite;
mind_entry_inds = [mie_ind];
mind_entry_polymorphic = poly;
+ mind_entry_private = None;
mind_entry_universes = ctx } in
let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
Oops, something went wrong.

0 comments on commit 8a90545

Please sign in to comment.