diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 19 | ||||
| -rw-r--r-- | interp/constrintern.ml | 34 | ||||
| -rw-r--r-- | interp/declare.ml | 27 | ||||
| -rw-r--r-- | interp/declare.mli | 5 | ||||
| -rw-r--r-- | interp/discharge.ml | 118 | ||||
| -rw-r--r-- | interp/discharge.mli | 16 | ||||
| -rw-r--r-- | interp/impargs.ml | 4 | ||||
| -rw-r--r-- | interp/impargs.mli | 6 | ||||
| -rw-r--r-- | interp/interp.mllib | 1 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 6 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 |
11 files changed, 49 insertions, 189 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb66658a37..701c07dc8d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -107,7 +107,7 @@ let _show_inactive_notations () = let deactivate_notation nr = match nr with | SynDefRule kn -> - (* shouldn't we check wether it is well defined? *) + (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> match availability_of_notation (scopt, ntn) (scopt, []) with @@ -757,11 +757,10 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo (* mapping glob_constr to constr_expr *) let extern_glob_sort = function - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType _ as s when !print_universes -> s - | GType _ -> GType [] + (* In case we print a glob_constr w/o having passed through detyping *) + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed _ when not !print_universes -> UAnonymous {rigid=true} + | UNamed _ | UAnonymous _ as u -> u let extern_universes = function | Some _ as l when !print_universes -> l @@ -1312,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) - | PSort Sorts.InSProp -> GSort GSProp - | PSort Sorts.InProp -> GSort GProp - | PSort Sorts.InSet -> GSort GSet - | PSort Sorts.InType -> GSort (GType []) + | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0]) + | PSort Sorts.InProp -> GSort (UNamed [GProp,0]) + | PSort Sorts.InSet -> GSort (UNamed [GSet,0]) + | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i let extern_constr_pattern env sigma pat = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 753065b7dd..1a81dc41a1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -998,18 +998,10 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option = - match info with - | UAnonymous -> None - | UUnknown -> None - | UNamed id -> Some (id, 0) - let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType info -> GType [sort_info_of_level_info info] + | UAnonymous {rigid} -> UAnonymous {rigid} + | UNamed id -> UNamed [id,0] (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = @@ -1045,7 +1037,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (UAnonymous {rigid=true}) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) @@ -1229,7 +1221,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); - (* Two possibilities: either the args are given with explict + (* Two possibilities: either the args are given with explicit variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be added later on; or the args are not enough to have all arguments, @@ -1467,7 +1459,7 @@ let alias_of als = match als.alias_ids with @returns a raw_case_pattern_expr : - no notations and syntactic definition - - global reference and identifeir instead of reference + - global reference and identifier instead of reference *) @@ -1642,15 +1634,13 @@ let drop_notations_pattern looked_for genv = | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supportted only in local binders and only at top - level. In fact, they are currently eliminated by the - parser. The only reason why they are in the - [cases_pattern_expr] type is that the parser needs to factor - the "(c : t)" notation with user defined notations (such as - the pair). In the long term, we will try to support such - casts everywhere, and use them to print the domains of - lambdas in the encoding of match in constr. This check is - here and not in the parser because it would require + are supported only in local binders and only at top level. + The only reason they are in the [cases_pattern_expr] type + is that the parser needs to factor the "c : t" notation + with user defined notations. In the long term, we will try to + support such casts everywhere, and perhaps use them to print + the domains of lambdas in the encoding of match in constr. + This check is here and not in the parser because it would require duplicating the levels of the [pattern] rule. *) CErrors.user_err ?loc ~hdr:"drop_notations_pattern" (Pp.strbrk "Casts are not supported in this pattern.") diff --git a/interp/declare.ml b/interp/declare.ml index 7ee7ecb5e8..cc6f29f756 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -53,6 +53,13 @@ let load_constant i ((sp,kn), obj) = Nametab.push (Nametab.Until i) sp (ConstRef con); add_constant_kind con obj.cst_kind +let cooking_info segment = + let modlist = replacement_context () in + let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in + let named_ctx = List.map fst hyps in + let abstract = (named_ctx, subst, uctx) in + { Opaqueproof.modlist; abstract } + (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn), obj) = (* Never open a local definition *) @@ -89,13 +96,10 @@ let cache_constant ((sp,kn), obj) = let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in - let modlist = replacement_context () in - let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - let abstract = (named_of_variable_context hyps, subst, uctx) in - let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in + let info = cooking_info (section_segment_of_constant con) in (* This is a hack: when leaving a section, we lose the constant definition, so we have to store it in the libobject to be able to retrieve it after. *) - Some { obj with cst_decl = Some new_decl; } + Some { obj with cst_decl = Some { from; info } } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { @@ -163,7 +167,8 @@ let define_constant ?role ?(export_seff=false) id cd = not de.const_entry_opaque || is_poly de -> (* This globally defines the side-effects in the environment. *) - let de, export = Global.export_private_constants ~in_section de in + let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in + let de = { de with const_entry_body = Future.from_val (body, ()) } in export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) in @@ -214,11 +219,10 @@ let cache_variable ((sp,_),o) = let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let (de, eff) = Global.export_private_constants ~in_section:true de in - let () = List.iter register_side_effect eff in (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, uctx), () = Future.force de.const_entry_body in + let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in + let () = List.iter register_side_effect eff in let poly, univs = match de.const_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx @@ -312,9 +316,8 @@ let cache_inductive ((sp,kn),mie) = let discharge_inductive ((sp,kn),mie) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in - let repl = replacement_context () in - let info = section_segment_of_mutual_inductive mind in - Some (Discharge.process_inductive info repl mie) + let info = cooking_info (section_segment_of_mutual_inductive mind) in + Some (Cooking.cook_inductive info mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; diff --git a/interp/declare.mli b/interp/declare.mli index 2ffde31fc0..0b1a396a34 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -40,7 +40,7 @@ type internal_flag = | InternalTacticRequest | UserIndividualRequest -(* Defaut definition entries, transparent with no secctx or proj information *) +(* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> @@ -90,5 +90,4 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> lident list -> unit -val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> - unit +val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit diff --git a/interp/discharge.ml b/interp/discharge.ml deleted file mode 100644 index 1efd13adb1..0000000000 --- a/interp/discharge.ml +++ /dev/null @@ -1,118 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Term -open Constr -open Vars -open Declarations -open Cooking -open Entries - -(********************************) -(* Discharging mutual inductive *) - -(* Replace - - Var(y1)..Var(yq):C1..Cq |- Ij:Bj - Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti - - by - - |- Ij: (y1..yq:C1..Cq)Bj - I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] -*) - -let abstract_inductive decls nparamdecls inds = - let ntyp = List.length inds in - let ndecls = Context.Named.length decls in - let args = Context.Named.to_instance mkVar (List.rev decls) in - let args = Array.of_list args in - let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in - let inds' = - List.map - (function (tname,arity,template,cnames,lc) -> - let lc' = List.map (substl subs) lc in - let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in - let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in - (tname,arity',template,cnames,lc'')) - inds in - let nparamdecls' = nparamdecls + Array.length args in -(* To be sure to be the same as before, should probably be moved to process_inductive *) - let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparamdecls' arity in - params - in - let ind'' = - List.map - (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparamdecls' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in - { mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_template = template; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' - in (params',ind'') - -let refresh_polymorphic_type_of_inductive (_,mip) = - match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, false - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true - -let process_inductive info modlist mib = - let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in - let nparamdecls = Context.Rel.length mib.mind_params_ctxt in - let subst, ind_univs = - match mib.mind_universes with - | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx - | Polymorphic auctx -> - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_entry (nas, auctx) - in - let variance = match mib.mind_variance with - | None -> None - | Some _ -> Some (InferCumulativity.dummy_variance ind_univs) - in - let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in - let inds = - Array.map_to_list - (fun mip -> - let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in - let arity = discharge ty in - let lc = Array.map discharge mip.mind_user_lc in - (mip.mind_typename, - arity, template, - Array.to_list mip.mind_consnames, - Array.to_list lc)) - mib.mind_packets in - let section_decls' = Context.Named.map discharge section_decls in - let (params',inds') = abstract_inductive section_decls' nparamdecls inds in - let record = match mib.mind_record with - | PrimRecord info -> - Some (Some (Array.map (fun (x,_,_,_) -> x) info)) - | FakeRecord -> Some None - | NotRecord -> None - in - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_private = mib.mind_private; - mind_entry_variance = variance; - mind_entry_universes = ind_univs - } - diff --git a/interp/discharge.mli b/interp/discharge.mli deleted file mode 100644 index f7408937cf..0000000000 --- a/interp/discharge.mli +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Declarations -open Entries -open Opaqueproof - -val process_inductive : - Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/interp/impargs.ml b/interp/impargs.ml index 806fe93297..f3cdd64633 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -96,11 +96,11 @@ let set_maximality imps b = this kind if there is enough arguments to infer them) - [DepFlex] means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) - [DepFlexAndRigid] means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) diff --git a/interp/impargs.mli b/interp/impargs.mli index ccdd448460..1099074c63 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments - of a reference can be automatically infered *) + of a reference can be automatically inferred *) type argument_position = @@ -50,11 +50,11 @@ type implicit_explanation = this kind if there is enough arguments to infer them) *) | DepFlex of argument_position (** means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position (** means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) *) diff --git a/interp/interp.mllib b/interp/interp.mllib index 1262dbb181..b65a171ef9 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -16,5 +16,4 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Discharge Declare diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7f084fffdd..08619d912e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 = Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 - | GSort (GType _), NSort (GType _) when not u -> sigma + + (* Next pair of lines useful only if not coming from detyping *) + | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match + | GSort _, NSort (UAnonymous _) when not u -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 49273c4146..a7e1de736c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = match onlyparse with | None -> (* Redeclare it to be used as (short) name in case an other (distfix) - notation was declared inbetween *) + notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat | _ -> () end |