diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 17 | ||||
| -rw-r--r-- | interp/constrintern.ml | 14 | ||||
| -rw-r--r-- | interp/declare.ml | 61 | ||||
| -rw-r--r-- | interp/declare.mli | 15 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 3 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 6 |
6 files changed, 67 insertions, 49 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fe50bd4b08..701c07dc8d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -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 1dd68f2abf..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) diff --git a/interp/declare.ml b/interp/declare.ml index cc6f29f756..17de06ed57 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -39,10 +39,10 @@ type constant_obj = { cst_decl : Cooking.recipe option; (** Non-empty only when rebuilding a constant after a section *) cst_kind : logical_kind; - cst_locl : bool; + cst_locl : import_status; } -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind +type constant_declaration = Evd.side_effects constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -63,8 +63,9 @@ let cooking_info segment = (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn), obj) = (* Never open a local definition *) - if obj.cst_locl then () - else + match obj.cst_locl with + | ImportNeedQualified -> () + | ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Exactly i) sp (ConstRef con) @@ -137,14 +138,14 @@ let register_constant kn kind local = update_tables kn let register_side_effect (c, role) = - let () = register_constant c (IsProof Theorem) false in + let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in match role with - | Subproof -> () - | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] + | None -> () + | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -153,7 +154,14 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let define_constant ?role ?(export_seff=false) id cd = +let get_roles export eff = + let map c = + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in + (c, role) + in + List.map map export + +let define_constant ~side_effect ?(export_seff=false) id cd = (* Logically define the constant and its subproofs, no libobject tampering *) let is_poly de = match de.const_entry_universes with | Monomorphic_entry _ -> false @@ -167,30 +175,43 @@ 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 body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in + let body, eff = Future.force de.const_entry_body in + let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in + let export = get_roles export eff in let de = { de with const_entry_body = Future.from_val (body, ()) } in export, ConstantEntry (PureEntry, DefinitionEntry de) - | _ -> [], ConstantEntry (EffectEntry, cd) + | DefinitionEntry de -> + let map (body, eff) = body, eff.Evd.seff_private in + let body = Future.chain de.const_entry_body map in + let de = { de with const_entry_body = body } in + [], ConstantEntry (EffectEntry, DefinitionEntry de) + | ParameterEntry _ | PrimitiveEntry _ as cd -> + [], ConstantEntry (PureEntry, cd) in - let kn, eff = Global.add_constant ?role ~in_section id decl in + let kn, eff = Global.add_constant ~side_effect ~in_section id decl in kn, eff, export -let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) = let () = check_exists id in - let kn, _eff, export = define_constant ~export_seff id cd in + let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in (* Register the libobjects attached to the constants and its subproofs *) let () = List.iter register_side_effect export in let () = register_constant kn kind local in kn -let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = false) id (cd, kind) = - let kn, eff, export = define_constant ~role id cd in +let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = + let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in let () = assert (List.is_empty export) in let () = register_constant kn kind local in + let seff_roles = match role with + | None -> Cmap.empty + | Some r -> Cmap.singleton kn r + in + let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff let declare_definition ?(internal=UserIndividualRequest) - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) + ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) id ?types (body,univs) = let cb = definition_entry ?types ~univs ~opaque body @@ -200,7 +221,7 @@ let declare_definition ?(internal=UserIndividualRequest) (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry + | SectionLocalDef of Evd.side_effects definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -221,7 +242,9 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> (* 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), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in + let (body, eff) = Future.force de.const_entry_body in + let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in + let eff = get_roles export eff in let () = List.iter register_side_effect eff in let poly, univs = match de.const_entry_universes with | Monomorphic_entry uctx -> false, uctx diff --git a/interp/declare.mli b/interp/declare.mli index 795d9a767d..e2485d7cf0 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -23,7 +23,7 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry + | SectionLocalDef of Evd.side_effects definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -33,7 +33,7 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind +type constant_declaration = Evd.side_effects constant_entry * logical_kind type internal_flag = | UserAutomaticRequest @@ -44,7 +44,7 @@ type internal_flag = val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -53,14 +53,14 @@ val definition_entry : ?fix_exn:Future.fix_exn -> internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) val declare_constant : - ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t + ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t val declare_private_constant : - role:side_effect_role -> ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants + ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> Id.t -> ?types:constr -> + ?local:import_status -> Id.t -> ?types:constr -> constr Entries.in_universes_entry -> Constant.t (** Since transparent constants' side effects are globally declared, we @@ -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/dumpglob.ml b/interp/dumpglob.ml index a537b4848c..274f9b851a 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -91,7 +91,8 @@ let type_of_logical_kind = function (match a with | Definitional -> "defax" | Logical -> "prfax" - | Conjectural -> "prfax") + | Conjectural -> "prfax" + | Context -> "prfax") | IsProof th -> (match th with | Theorem 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 |