diff options
74 files changed, 879 insertions, 654 deletions
diff --git a/dev/base_include b/dev/base_include index 061bf1f3e1..b761924b46 100644 --- a/dev/base_include +++ b/dev/base_include @@ -68,7 +68,7 @@ open Constr_matching open Glob_term open Glob_ops open Coercion -open Recordops +open Structures open Detyping open Reductionops open Evarconv diff --git a/dev/ci/user-overlays/13958-gares-recordops-api.sh b/dev/ci/user-overlays/13958-gares-recordops-api.sh new file mode 100644 index 0000000000..0ec50a1dda --- /dev/null +++ b/dev/ci/user-overlays/13958-gares-recordops-api.sh @@ -0,0 +1,6 @@ +overlay metacoq https://github.com/gares/metacoq recordops-api 13958 +overlay mtac2 https://github.com/gares/Mtac2 recordops-api 13958 +overlay elpi https://github.com/gares/coq-elpi recordops-api 13958 +overlay unicoq https://github.com/gares/unicoq recordops-api 13958 +overlay equations https://github.com/gares/Coq-Equations recordops-api 13958 +overlay hierarchy_builder https://github.com/gares/hierarchy-builder coq-master 13958 diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 4452baf513..5c8b8944a7 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -344,6 +344,16 @@ Conversion machines noticeable if activated by chance, since it usually breaks control-flow integrity + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: arbitrary code execution on irreducible PArray.set + introduced: 8.13 + impacted released versions: 8.13.0, 8.13.1 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 8.13.2 + found by: Melquiond + GH issue number: #13998 + risk: none, unless using primitive array operations; systematic otherwise + Side-effects component: side-effects diff --git a/doc/changelog/01-kernel/14004-vm-array-set.rst b/doc/changelog/01-kernel/14004-vm-array-set.rst new file mode 100644 index 0000000000..f90d611f84 --- /dev/null +++ b/doc/changelog/01-kernel/14004-vm-array-set.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Crash when using :tacn:`vm_compute` on an irreducible ``PArray.set`` + (`#14005 <https://github.com/coq/coq/pull/14005>`_, + fixes `#13998 <https://github.com/coq/coq/issues/13998>`_, + by Guillaume Melquiond). diff --git a/doc/changelog/04-tactics/14012-ltac2-array-init.rst b/doc/changelog/04-tactics/14012-ltac2-array-init.rst new file mode 100644 index 0000000000..c79fc7e29a --- /dev/null +++ b/doc/changelog/04-tactics/14012-ltac2-array-init.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Ltac2 ``Array.init`` no longer incurs exponential overhead when used + recursively (`#14012 <https://github.com/coq/coq/pull/14012>`_, fixes `#14011 + <https://github.com/coq/coq/issues/14011>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/14033-fix-14009.rst b/doc/changelog/04-tactics/14033-fix-14009.rst new file mode 100644 index 0000000000..3b58e193cb --- /dev/null +++ b/doc/changelog/04-tactics/14033-fix-14009.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Properly expand projection parameters in hint discrimination + nets. (`#14033 <https://github.com/coq/coq/pull/14033>`_, + fixes `#9000 <https://github.com/coq/coq/issues/9000>`_, + `#14009 <https://github.com/coq/coq/issues/14009>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst new file mode 100644 index 0000000000..b5b63455c9 --- /dev/null +++ b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst @@ -0,0 +1,5 @@ +- **Added:** + Added a FFI to convert between Ltac1 and Ltac2 identifiers + (`#13997 <https://github.com/coq/coq/pull/13997>`_, + fixes `#13996 <https://github.com/coq/coq/issues/13996>`_, + by Pierre-Marie Pédrot). diff --git a/engine/uState.ml b/engine/uState.ml index 20ea24dd87..81559778f2 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -296,9 +296,6 @@ let add_constraints uctx cstrs = universes = UGraph.merge_constraints cstrs' uctx.universes; weak_constraints = weak; } -(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) - let add_universe_constraints uctx cstrs = let univs, local = uctx.local in let vars, weak, local' = process_universe_constraints uctx cstrs in diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 4ed6e97526..86bf2c9298 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -406,6 +406,3 @@ let normalize_context_set ~lbound g ctx us algs weak = in let us = normalize_opt_subst us in (us, algs), (ctx', Constraint.union noneqs eqs) - -(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 330ed5d0ad..c76a4cd751 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -83,12 +83,6 @@ let subst_univs_constr subst c = let f = Univ.make_subst subst in subst_univs_fn_constr f c -let subst_univs_constr = - if Flags.profile then - let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in - CProfile.profile2 subst_univs_constr_key subst_univs_constr - else subst_univs_constr - let normalize_univ_variable ~find = let rec aux cur = let b = find cur in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3cabf52197..f687c4a640 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -27,6 +27,7 @@ open Glob_term open Glob_ops open Pattern open Detyping +open Structures module NamedDecl = Context.Named.Declaration (*i*) @@ -232,7 +233,7 @@ let get_record_print = let is_record indsp = try - let _ = Recordops.lookup_structure indsp in + let _ = Structure.find indsp in true with Not_found -> false @@ -407,7 +408,7 @@ let pattern_printable_in_both_syntax (ind,_ as c) = let extern_record_pattern cstrsp args = try if !Flags.raw_print then raise Exit; - let projs = Recordops.lookup_projections (fst cstrsp) in + let projs = Structure.find_projections (fst cstrsp) in if PrintingRecord.active (fst cstrsp) then () else if PrintingConstructor.active (fst cstrsp) then @@ -614,9 +615,12 @@ let is_gvar id c = match DAst.get c with let is_projection nargs r = if not !Flags.in_debugger && not !Flags.raw_print && !print_projections then try - let n = Recordops.find_projection_nparams r + 1 in - if n <= nargs then Some n - else None + match r with + | GlobRef.ConstRef c -> + let n = Structure.projection_nparams c + 1 in + if n <= nargs then Some n + else None + | _ -> None with Not_found -> None else None @@ -689,33 +693,29 @@ let extern_record ref args = try if !Flags.raw_print then raise Exit; let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in - let struc = Recordops.lookup_structure (fst cstrsp) in + let struc = Structure.find (fst cstrsp) in if PrintingRecord.active (fst cstrsp) then () else if PrintingConstructor.active (fst cstrsp) then raise Exit else if not (get_record_print ()) then raise Exit; - let projs = struc.Recordops.s_PROJ in - let locals = struc.Recordops.s_PROJKIND in + let projs = struc.Structure.projections in let rec cut args n = if Int.equal n 0 then args else match args with | [] -> raise No_match | _ :: t -> cut t (n - 1) in - let args = cut args struc.Recordops.s_EXPECTEDPARAM in - let rec ip projs locs args acc = + let args = cut args struc.Structure.nparams in + let rec ip projs args acc = match projs with | [] -> acc - | None :: q -> raise No_match - | Some c :: q -> - match locs with - | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") - | { Recordops.pk_true_proj = false } :: locs' -> + | { Structure.proj_body = None } :: _ -> raise No_match + | { Structure.proj_body = Some c; proj_true = false } :: q -> (* we don't want to print locals *) - ip q locs' args acc - | { Recordops.pk_true_proj = true } :: locs' -> + ip q args acc + | { Structure.proj_body = Some c; proj_true = true } :: q -> match args with | [] -> raise No_match (* we give up since the constructor is not complete *) @@ -723,9 +723,9 @@ let extern_record ref args = let arg = Lazy.force arg in let loc = arg.CAst.loc in let ref = extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c) in - ip q locs' tail ((ref, arg) :: acc) + ip q tail ((ref, arg) :: acc) in - Some (List.rev (ip projs locals args [])) + Some (List.rev (ip projs args [])) with | Not_found | No_match | Exit -> None diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7c63ebda3a..958e1408f8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -24,6 +24,7 @@ open Glob_term open Glob_ops open Patternops open Pretyping +open Structures open Cases open Constrexpr open Constrexpr_ops @@ -34,6 +35,7 @@ open Inductiveops open Context.Rel.Declaration open NumTok + (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments - it replaces notations by their value (scopes stuff are here) @@ -100,7 +102,7 @@ type internalization_error = | NonLinearPattern of Id.t | BadPatternsNumber of int * int | NotAProjection of qualid - | ProjectionsOfDifferentRecords of Recordops.struc_typ * Recordops.struc_typ + | ProjectionsOfDifferentRecords of Structure.t * Structure.t exception InternalizationError of internalization_error @@ -126,8 +128,8 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 -let inductive_of_record record = - let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in +let inductive_of_record s = + let inductive = GlobRef.IndRef (s.Structure.name) in Nametab.shortest_qualid_of_global Id.Set.empty inductive let explain_field_not_a_projection field_id = @@ -1130,8 +1132,10 @@ let intern_reference qid = let intern_projection qid = try - let gr = Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) in - (gr, Recordops.find_projection gr) + match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with + | GlobRef.ConstRef c as gr -> + (gr, Structure.find_from_projection c) + | _ -> raise Not_found with Not_found -> Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) @@ -1296,8 +1300,8 @@ let check_applied_projection isproj realref qid = let is_prim = match realref with | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false | Some (ConstRef c) -> - if Recordops.is_primitive_projection c then true - else if Recordops.is_projection c then false + if PrimitiveProjections.mem c then true + else if Structure.is_projection c then false else error_nonprojection_syntax ?loc:qid.loc qid (* TODO check projargs, note we will need implicit argument info *) in @@ -1498,18 +1502,18 @@ let sort_fields ~complete loc fields completer = | (first_field_ref, _):: _ -> let (first_field_glob_ref, record) = intern_projection first_field_ref in (* the number of parameters *) - let nparams = record.Recordops.s_EXPECTEDPARAM in + let nparams = record.Structure.nparams in (* the reference constructor of the record *) - let base_constructor = GlobRef.ConstructRef record.Recordops.s_CONST in + let base_constructor = GlobRef.ConstructRef (record.Structure.name,1) in let () = check_duplicate ?loc fields in - let build_proj idx proj kind = - if proj = None && complete then + let build_proj idx proj = + if proj.Structure.proj_body = None && complete then (* we don't want anonymous fields *) user_err ?loc (str "This record contains anonymous fields.") else - (idx, proj, kind.Recordops.pk_true_proj) in + (idx, proj.Structure.proj_body, proj.Structure.proj_true) in let proj_list = - List.map2_i build_proj 1 record.Recordops.s_PROJ record.Recordops.s_PROJKIND in + List.map_i build_proj 1 record.Structure.projections in (* now we want to have all fields assignments indexed by their place in the constructor *) let rec index_fields fields remaining_projs acc = @@ -1538,7 +1542,7 @@ let sort_fields ~complete loc fields completer = (* For terms, we keep only regular fields *) None else - Some (idx, completer idx field_ref record.Recordops.s_CONST) in + Some (idx, completer idx field_ref (record.Structure.name,1)) in List.map_filter complete_field remaining_projs in List.rev_append remaining_fields acc in diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 6ef0e9fa15..9e0f574fa3 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -295,38 +295,57 @@ let types = PITT_param 1)) in function - | Int63head0 | Int63tail0 -> [int_ty; int_ty] + | Int63head0 | Int63tail0 -> + [int_ty], int_ty | Int63add | Int63sub | Int63mul | Int63div | Int63mod | Int63divs | Int63mods | Int63lsr | Int63lsl | Int63asr - | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] + | Int63land | Int63lor | Int63lxor -> + [int_ty; int_ty], int_ty | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> - [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)] + [int_ty; int_ty], PITT_ind (PIT_carry, int_ty) | Int63mulc | Int63diveucl -> - [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] - | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] - | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] + [int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty)) + | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> + [int_ty; int_ty], PITT_ind (PIT_bool, ()) + | Int63compare | Int63compares -> + [int_ty; int_ty], PITT_ind (PIT_cmp, ()) | Int63div21 -> - [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] - | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] + [int_ty; int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty)) + | Int63addMulDiv -> + [int_ty; int_ty; int_ty], int_ty | Float64opp | Float64abs | Float64sqrt - | Float64next_up | Float64next_down -> [float_ty; float_ty] - | Float64ofInt63 -> [int_ty; float_ty] - | Float64normfr_mantissa -> [float_ty; int_ty] - | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))] - | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())] - | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())] - | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())] - | Float64add | Float64sub | Float64mul - | Float64div -> [float_ty; float_ty; float_ty] - | Float64ldshiftexp -> [float_ty; int_ty; float_ty] - | Arraymake -> [int_ty; PITT_param 1; array_ty] - | Arrayget -> [array_ty; int_ty; PITT_param 1] - | Arraydefault -> [array_ty; PITT_param 1] - | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty] - | Arraycopy -> [array_ty; array_ty] - | Arraylength -> [array_ty; int_ty] + | Float64next_up | Float64next_down -> + [float_ty], float_ty + | Float64ofInt63 -> + [int_ty], float_ty + | Float64normfr_mantissa -> + [float_ty], int_ty + | Float64frshiftexp -> + [float_ty], PITT_ind (PIT_pair, (float_ty, int_ty)) + | Float64eq | Float64lt | Float64le -> + [float_ty; float_ty], PITT_ind (PIT_bool, ()) + | Float64compare -> + [float_ty; float_ty], PITT_ind (PIT_f_cmp, ()) + | Float64classify -> + [float_ty], PITT_ind (PIT_f_class, ()) + | Float64add | Float64sub | Float64mul | Float64div -> + [float_ty; float_ty], float_ty + | Float64ldshiftexp -> + [float_ty; int_ty], float_ty + | Arraymake -> + [int_ty; PITT_param 1], array_ty + | Arrayget -> + [array_ty; int_ty], PITT_param 1 + | Arraydefault -> + [array_ty], PITT_param 1 + | Arrayset -> + [array_ty; int_ty; PITT_param 1], array_ty + | Arraycopy -> + [array_ty], array_ty + | Arraylength -> + [array_ty], int_ty let one_param = (* currently if there's a parameter it's always this *) @@ -460,14 +479,17 @@ type args_red = arg_kind list (* Invariant only argument of type int63, float or an inductive can have kind Kwhnf *) -let arity t = let sign = types t in nparams t + List.length sign - 1 +let arity t = + nparams t + List.length (fst (types t)) let kind t = let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in - params (nparams t) @ List.map args (CList.drop_last (types t)) + params (nparams t) @ List.map args (fst (types t)) -let types t = params t, types t +let types t = + let args_ty, ret_ty = types t in + params t, args_ty, ret_ty (** Special Entries for Register **) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index de90179726..6661851d53 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -140,8 +140,8 @@ val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type val univs : t -> Univ.AUContext.t -val types : t -> Constr.rel_context * ind_or_type list -(** Parameters * Reduction relevant arguments and output type +val types : t -> Constr.rel_context * ind_or_type list * ind_or_type +(** Parameters * Reduction relevant arguments * output type XXX we could reify universes in ind_or_type (currently polymorphic types like array are assumed to use universe 0). *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f82b754c59..87b1a71c9d 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -252,9 +252,6 @@ let cook_constant { from = cb; info } = cook_context = Some const_hyps; } -(* let cook_constant_key = CProfile.declare_profile "cook_constant" *) -(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) - (********************************) (* Discharging mutual inductive *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index eb18d4b90e..6cb61174d3 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1334,11 +1334,6 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = else () -(* -let cfkey = CProfile.declare_profile "check_fix";; -let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; -*) - (************************************************************************) (* Co-fixpoints. *) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index c5ac57a2cd..d2fb773dc4 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -291,6 +291,11 @@ let subst_ind sub (ind,i as indi) = let ind' = subst_mind sub ind in if ind' == ind then indi else ind',i +let subst_constructor subst (ind,j as ref) = + let ind' = subst_ind subst ind in + if ind==ind' then ref + else (ind',j) + let subst_pind sub (ind,u) = (subst_ind sub ind, u) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 9cf270cff7..e7bfceb4de 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -127,6 +127,9 @@ val subst_mind : val subst_ind : substitution -> inductive -> inductive +val subst_constructor : + substitution -> constructor -> constructor + val subst_pind : substitution -> pinductive -> pinductive val subst_kn : diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9ce388929c..22bbcb8a65 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -994,9 +994,8 @@ let extract_prim ml_of l = let decl = ref [] in let cond = ref [] in let type_args p = - let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in - let params, sign = CPrimitives.types p in - List.length params, Array.of_list (aux sign) in + let params, args_ty, _ = CPrimitives.types p in + List.length params, Array.of_list args_ty in let rec aux l = match l with | Lprim(prefix,kn,p,args) -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1e39756d47..18c3a3ec9c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -964,7 +964,8 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = compare_instances = infer_convert_instances; compare_cumul_instances = infer_inductive_instances; } -let gen_conv cv_pb l2r reds env evars univs t1 t2 = +let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _ -> None)) t1 t2 = + let univs = Environ.universes env in let b = if cv_pb = CUMUL then leq_constr_univs univs t1 t2 else eq_constr_univs univs t1 t2 @@ -974,16 +975,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in () -(* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) = - let univs = Environ.universes env in - if Flags.profile then - let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in - CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs - else gen_conv cv_pb l2r reds env evars univs - let conv = gen_conv CONV - let conv_leq = gen_conv CUMUL let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = @@ -992,7 +984,7 @@ let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2 in s -let infer_conv_universes cv_pb l2r evars reds env t1 t2 = +let infer_conv_universes cv_pb ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env t1 t2 = let univs = Environ.universes env in let b, cstrs = if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 @@ -1001,37 +993,16 @@ let infer_conv_universes cv_pb l2r evars reds env t1 t2 = if b then cstrs else let state = ((univs, Univ.Constraint.empty), inferred_universes) in - let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in + let ((_,cstrs), _) = clos_gen_conv ts cv_pb l2r evars env univs state t1 t2 in cstrs -(* Profiling *) -let infer_conv_universes = - if Flags.profile then - let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in - CProfile.profile7 infer_conv_universes_key infer_conv_universes - else infer_conv_universes - -let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) - env t1 t2 = - infer_conv_universes CONV l2r evars ts env t1 t2 - -let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) - env t1 t2 = - infer_conv_universes CUMUL l2r evars ts env t1 t2 +let infer_conv = infer_conv_universes CONV +let infer_conv_leq = infer_conv_universes CUMUL let default_conv cv_pb ?l2r:_ env t1 t2 = gen_conv cv_pb env t1 t2 let default_conv_leq = default_conv CUMUL -(* -let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";; -let conv_leq env t1 t2 = - CProfile.profile4 convleqkey conv_leq env t1 t2;; - -let convkey = CProfile.declare_profile "Kernel_reduction.conv";; -let conv env t1 t2 = - CProfile.profile4 convleqkey conv env t1 t2;; -*) (* Application with on-the-fly reduction *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 741491c917..3a946fc03a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -644,12 +644,6 @@ let infer env constr = let constr, t = execute env constr in make_judge constr t -let infer = - if Flags.profile then - let infer_key = CProfile.declare_profile "Fast_infer" in - CProfile.profile2 infer_key (fun b c -> infer b c) - else (fun b c -> infer b c) - let assumption_of_judgment env {uj_val=c; uj_type=t} = infer_assumption env c t @@ -785,15 +779,16 @@ let type_of_prim env u t = | PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t | PITT_param i -> Constr.mkRel (n+i) in - let rec nary_op n = function - | [] -> assert false - | [ret_ty] -> tr_type n ret_ty + let rec nary_op n ret_ty = function + | [] -> tr_type n ret_ty | arg_ty :: r -> - Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r) + Constr.mkProd (Context.nameR (Id.of_string "x"), + tr_type n arg_ty, nary_op (n + 1) ret_ty r) in - let params, sign = types t in + let params, args_ty, ret_ty = types t in assert (AUContext.size (univs t) = Instance.length u); - Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params) + Vars.subst_instance_constr u + (Term.it_mkProd_or_LetIn (nary_op 0 ret_ty args_ty) params) let type_of_prim_or_type env u = let open CPrimitives in function diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index b988ec40a7..6db54a3bb6 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -251,28 +251,3 @@ type node = G.node = let repr g = G.repr g.graph let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g - -(** Profiling *) - -let merge_constraints = - if Flags.profile then - let key = CProfile.declare_profile "merge_constraints" in - CProfile.profile2 key merge_constraints - else merge_constraints -let check_constraints = - if Flags.profile then - let key = CProfile.declare_profile "check_constraints" in - CProfile.profile2 key check_constraints - else check_constraints - -let check_eq = - if Flags.profile then - let check_eq_key = CProfile.declare_profile "check_eq" in - CProfile.profile3 check_eq_key check_eq - else check_eq - -let check_leq = - if Flags.profile then - let check_leq_key = CProfile.declare_profile "check_leq" in - CProfile.profile3 check_leq_key check_leq - else check_leq diff --git a/kernel/vars.ml b/kernel/vars.ml index b09577d4db..b9991391c2 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -123,11 +123,6 @@ let substn_many lamv n c = | _ -> Constr.map_with_binders succ substrec depth c in substrec n c -(* -let substkey = CProfile.declare_profile "substn_many";; -let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;; -*) - let make_subst = function | [] -> [||] | hd :: tl -> @@ -343,9 +338,6 @@ let univ_instantiate_constr u c = assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder)); subst_instance_constr u c.univ_abstracted_value -(* let substkey = CProfile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *) - let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index c2b087f061..b5604d0593 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -35,6 +35,7 @@ type instruction = | Kpush | Kpop of int | Kpush_retaddr of Label.t + | Kshort_apply of int | Kapply of int | Kappterm of int * int | Kreturn of int @@ -93,6 +94,7 @@ let rec pp_instr i = | Kpush -> str "push" | Kpop n -> str "pop " ++ int n | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl + | Kshort_apply n -> str "short_apply " ++ int n | Kapply n -> str "apply " ++ int n | Kappterm(n, m) -> str "appterm " ++ int n ++ str ", " ++ int m @@ -146,8 +148,8 @@ let rec pp_instr i = (Constant.print (fst id)) | Kcamlprim (op, lbl) -> - str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ - pp_lbl lbl + str "camlcall " ++ str (CPrimitives.to_string op) ++ str ", branch " ++ + pp_lbl lbl ++ str " on accu" and pp_bytecodes c = match c with diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli index eeca0d2ad1..d9e2d91177 100644 --- a/kernel/vmbytecodes.mli +++ b/kernel/vmbytecodes.mli @@ -30,6 +30,7 @@ type instruction = | Kpush (** sp = accu :: sp *) | Kpop of int (** sp = skipn n sp *) | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *) + | Kshort_apply of int (** number of arguments (arguments on top of stack) *) | Kapply of int (** number of arguments (arguments on top of stack) *) | Kappterm of int * int (** number of arguments, slot size *) | Kreturn of int (** slot size *) diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 7d3b3469b0..b4d97228bf 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -461,7 +461,7 @@ let comp_app comp_fun comp_arg cenv f args sz cont = | None -> if nargs <= 4 then comp_args comp_arg cenv args sz - (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) + (Kpush :: (comp_fun cenv f (sz+nargs) (Kshort_apply nargs :: cont))) else let lbl,cont1 = label_code cont in Kpush_retaddr lbl :: @@ -757,26 +757,25 @@ let rec compile_lam env cenv lam sz cont = let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in comp_args (compile_lam env) cenv args sz cont - | Lprim ((kn,u), op, args) when is_caml_prim op -> + | Lprim (kn, op, args) when is_caml_prim op -> let arity = CPrimitives.arity op in let nparams = CPrimitives.nparams op in let nargs = arity - nparams in - assert (arity = Array.length args && arity <= 4); + assert (arity = Array.length args && arity <= 4 && nargs >= 1); let (jump, cont) = make_branch cont in let lbl_default = Label.create () in let default = - let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in + let cont = [Kshort_apply arity; jump] in + let cont = Kpush :: compile_get_global cenv kn (sz + arity) cont in let cont = - if Univ.Instance.is_empty u then cont - else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) - in - Klabel lbl_default :: - Kpush :: - if Int.equal nparams 0 then cont - else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) - in + if Int.equal nparams 0 then cont + else + let params = Array.sub args 0 nparams in + Kpush :: comp_args (compile_lam env) cenv params (sz + nargs) cont in + Klabel lbl_default :: cont in fun_code := Ksequence default :: !fun_code; - comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) + let cont = Kcamlprim (op, lbl_default) :: cont in + comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz cont | Lprim (kn, op, args) -> comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index caa263432e..44e933ef26 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -300,8 +300,11 @@ let emit_instr env = function out env opPOP; out_int env n | Kpush_retaddr lbl -> out env opPUSH_RETADDR; out_label env lbl + | Kshort_apply n -> + assert (1 <= n && n <= 4); + out env(opAPPLY1 + n - 1) | Kapply n -> - if n <= 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n) + out env opAPPLY; out_int env n | Kappterm(n, sz) -> if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz) else (out env opAPPTERM; out_int env n; out_int env sz) diff --git a/lib/cProfile.ml b/lib/cProfile.ml index b68d35d2d4..7245b35d59 100644 --- a/lib/cProfile.ml +++ b/lib/cProfile.ml @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +let enable_profile = false + let word_length = Sys.word_size / 8 let float_of_time t = float_of_int t /. 100. @@ -87,9 +89,9 @@ let init_alloc = ref 0.0 let reset_profile () = List.iter reset_record !prof_table let init_profile () = - (* We test Flags.profile as a way to support declaring profiled + (* We test enable_profile as a way to support declaring profiled functions in plugins *) - if !prof_table <> [] || Flags.profile then begin + if !prof_table <> [] || enable_profile then begin let outside = create_record () in stack := [outside]; last_alloc := get_alloc (); diff --git a/lib/flags.ml b/lib/flags.ml index 57e879add7..c87a375356 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -51,8 +51,6 @@ let xml_debug = ref false let in_debugger = ref false let in_toplevel = ref false -let profile = false - let raw_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index e10e2c8cb8..2f59a0cc18 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -44,8 +44,6 @@ val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref -val profile : bool - (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref diff --git a/library/globnames.ml b/library/globnames.ml index 654349dea0..491c89e68e 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -31,10 +31,6 @@ let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" -let subst_constructor subst (ind,j as ref) = - let ind' = subst_ind subst ind in - if ind==ind' then ref - else (ind',j) let subst_global_reference subst ref = match ref with | VarRef var -> ref diff --git a/library/globnames.mli b/library/globnames.mli index 8acea5ef28..58e0efbc7a 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -34,7 +34,6 @@ val destConstructRef : GlobRef.t -> constructor val is_global : GlobRef.t -> constr -> bool [@@ocaml.deprecated "Use [Constr.isRefX] instead."] -val subst_constructor : substitution -> constructor -> constructor val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0cad192332..ca4f5429a2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -22,7 +22,6 @@ open Reductionops open Inductive open Termops open Inductiveops -open Recordops open Namegen open Miniml open Table @@ -531,7 +530,7 @@ and extract_really_ind env kn mib = let n = nb_default_params env sg (EConstr.of_constr ty) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in - List.iter (Option.iter check_proj) (lookup_projections ip) + List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip) with Not_found -> () end; Record field_glob @@ -1129,7 +1128,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_typ (get_body c) | Some p -> let body = fake_match_projection env p in @@ -1142,7 +1141,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_def (get_body c) | Some p -> let body = fake_match_projection env p in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c7bda43465..1640bff43b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -373,11 +373,6 @@ end) = struct end -(* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) -(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) - - let type_app_poly env env evd f args = let evars, c = app_poly_nocheck env evd f args in let evd', t = Typing.type_of env (goalevars evars) c in @@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) - (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 5e88bf7c79..f2f5fc16a6 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -91,6 +91,13 @@ let to_int v = Some (out_gen (topwit wit_int) v) else None +let of_ident id = in_gen (topwit wit_ident) id + +let to_ident v = + if has_type v (topwit wit_ident) then + Some (out_gen (topwit wit_ident) v) + else None + let to_list v = prj Val.typ_list v let to_option v = prj Val.typ_opt v diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 8ca2510459..c748fb3d1a 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -39,6 +39,8 @@ sig val to_uconstr : t -> Ltac_pretype.closed_glob_constr option val of_int : int -> t val to_int : t -> int option + val of_ident : Id.t -> t + val to_ident : t -> Id.t option val to_list : t -> t list option val to_option : t -> t option option val to_pair : t -> (t * t) option diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 935cef58b9..ad85f68b03 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -46,6 +46,7 @@ open Ssrtacticals open Ssrbwd open Ssrequality open Ssripats +open Libobject (** Ssreflect load check. *) @@ -79,8 +80,39 @@ let ssrtac_entry name = { mltac_index = 0; } -let register_ssrtac name f = - Tacenv.register_ml_tactic (ssrtac_name name) [|f|] +let cache_tactic_notation (_, (key, body, parule)) = + Tacenv.register_alias key body; + Pptactic.declare_notation_tactic_pprule key parule + +type tactic_grammar_obj = KerName.t * Tacenv.alias_tactic * Pptactic.pp_tactic + +let inSsrGrammar : tactic_grammar_obj -> obj = + declare_object {(default_object "SsrGrammar") with + load_function = (fun _ -> cache_tactic_notation); + cache_function = cache_tactic_notation; + classify_function = (fun x -> Keep x)} + +let path = MPfile (DirPath.make @@ List.map Id.of_string ["ssreflect"; "ssr"; "Coq"]) + +let register_ssrtac name f prods = + let open Pptactic in + Tacenv.register_ml_tactic (ssrtac_name name) [|f|]; + let map id = Reference (Locus.ArgVar (CAst.make id)) in + let get_id = function + | TacTerm s -> None + | TacNonTerm (_, (_, ido)) -> ido in + let ids = List.map_filter get_id prods in + let tac = TacML (CAst.make (ssrtac_entry name, List.map map ids)) in + let key = KerName.make path (Label.make ("ssrparser_" ^ name)) in + let body = Tacenv.{ alias_args = ids; alias_body = tac; alias_deprecation = None } in + let parule = { + pptac_level = 0; + pptac_prods = prods + } in + let obj () = + Lib.add_anonymous_leaf (inSsrGrammar (key, body, parule)) in + Mltop.declare_cache_obj obj __coq_plugin_name; + key let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v @@ -933,7 +965,7 @@ END { let pr_intros sep intrs = - if intrs = [] then mt() else sep () ++ str "=>" ++ pr_ipats intrs + if intrs = [] then mt() else sep () ++ str "=>" ++ sep () ++ pr_ipats intrs let pr_ssrintros _ _ _ = pr_intros mt } @@ -963,15 +995,6 @@ END { -let () = register_ssrtac "tclintros" begin fun args ist -> match args with -| [arg] -> - let arg = cast_arg wit_ssrintrosarg arg in - let tac, intros = arg in - ssrevaltac ist tac <*> tclIPATssr intros -| _ -> assert false -end - - (** Defined identifier *) let pr_ssrfwdid id = pr_spc () ++ pr_id id @@ -1672,20 +1695,28 @@ let _ = add_internal_name (is_tagged perm_tag) { -type ssrargfmt = ArgSsr of string | ArgSep of string + let ssrtac_expr ?loc key args = + TacAlias (CAst.make ?loc (key, (List.map (fun x -> Tacexpr.TacGeneric (None, x)) args))) -let set_pr_ssrtac name prec afmt = (* FIXME *) () (* - let fmt = List.map (function - | ArgSep s -> Egramml.GramTerminal s - | ArgSsr s -> Egramml.GramTerminal s - | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in - let tacname = ssrtac_name name in () *) +let mk_non_term wit id = + let open Pptactic in + TacNonTerm (None, (Extend.Uentry (Genarg.ArgT.Any (Genarg.get_arg_tag wit)), Some id)) -let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) +let tclintroskey = + let prods = + [ mk_non_term wit_ssrintrosarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [arg] -> + let arg = cast_arg wit_ssrintrosarg arg in + let tac, intros = arg in + ssrevaltac ist tac <*> tclIPATssr intros + | _ -> assert false + end in + register_ssrtac "tclintros" tac prods let tclintros_expr ?loc tac ipats = - let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in - ssrtac_expr ?loc "tclintros" args + let args = [in_gen (rawwit wit_ssrintrosarg) (tac, ipats)] in + ssrtac_expr ?loc tclintroskey args } @@ -1768,18 +1799,20 @@ END { -let () = register_ssrtac "tcldo" begin fun args ist -> match args with -| [arg] -> - let arg = cast_arg wit_ssrdoarg arg in - ssrdotac ist arg -| _ -> assert false -end - -let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] +let tcldokey = + let open Pptactic in + let prods = [ TacTerm "do"; mk_non_term wit_ssrdoarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [arg] -> + let arg = cast_arg wit_ssrdoarg arg in + ssrdotac ist arg + | _ -> assert false + end in + register_ssrtac "tcldo" tac prods let ssrdotac_expr ?loc n m tac clauses = let arg = ((n, m), tac), clauses in - ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)] + ssrtac_expr ?loc tcldokey [in_gen (rawwit wit_ssrdoarg) arg] } @@ -1815,22 +1848,26 @@ END { -let () = register_ssrtac "tclseq" begin fun args ist -> match args with -| [tac; dir; arg] -> - let tac = cast_arg wit_ssrtclarg tac in - let dir = cast_arg wit_ssrseqdir dir in - let arg = cast_arg wit_ssrseqarg arg in - tclSEQAT ist tac dir arg -| _ -> assert false -end - -let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] +let tclseqkey = + let prods = + [ mk_non_term wit_ssrtclarg (Names.Id.of_string "tac") + ; mk_non_term wit_ssrseqdir (Names.Id.of_string "dir") + ; mk_non_term wit_ssrseqarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [tac; dir; arg] -> + let tac = cast_arg wit_ssrtclarg tac in + let dir = cast_arg wit_ssrseqdir dir in + let arg = cast_arg wit_ssrseqarg arg in + tclSEQAT ist tac dir arg + | _ -> assert false + end in + register_ssrtac "tclseq" tac prods let tclseq_expr ?loc tac dir arg = let arg1 = in_gen (rawwit wit_ssrtclarg) tac in let arg2 = in_gen (rawwit wit_ssrseqdir) dir in let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in - ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3]) + ssrtac_expr ?loc tclseqkey [arg1; arg2; arg3] } @@ -2453,8 +2490,9 @@ GRAMMAR EXTEND Gram GLOBAL: ltac_expr; ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> - { ssrtac_expr ~loc "abstract" - [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; + { TacML (CAst.make ~loc ( + ssrtac_entry "abstract", [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)])) + } ]]; END TACTIC EXTEND ssrabstract | [ "abstract" ssrdgens(gens) ] -> { diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 7774258fca..805be1fc87 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -22,7 +22,6 @@ open Vars open Libnames open Tactics open Termops -open Recordops open Tacmach open Glob_term open Util @@ -333,7 +332,8 @@ type tpattern = { let all_ok _ _ = true let proj_nparams c = - try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0 + try 1 + Structures.Structure.projection_nparams c + with Not_found -> 0 let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true @@ -429,9 +429,13 @@ let ungen_upat lhs (sigma, uc, t) u = | _ -> KpatRigid in sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t} -let nb_cs_proj_args pc f u = +let nb_cs_proj_args ise pc f u = + let open Structures in + let open ValuePattern in let na k = - List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in + let open CanonicalSolution in + let _, { cvalue_arguments } = find (Global.env()) ise (GlobRef.ConstRef pc, k) in + List.length cvalue_arguments in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be @@ -441,7 +445,7 @@ let nb_cs_proj_args pc f u = | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f - | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.CanOrd.equal (Names.Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 @@ -467,7 +471,7 @@ let splay_app ise = | Cast _ | Evar _ -> loop c [| |] | _ -> c, [| |] -let filter_upat i0 f n u fpats = +let filter_upat ise i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with @@ -479,7 +483,7 @@ let filter_upat i0 f n u fpats = | KpatRigid when isRigid f -> na | KpatFlex -> na | KpatProj pc -> - let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np + let np = na + nb_cs_proj_args ise pc f u in if n < np then -1 else np | _ -> -1 in if np < na then fpats else let () = if !i0 < np then i0 := n in (u, np) :: fpats @@ -568,7 +572,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = let f, a = splay_app ise c in let i0 = ref (-1) in - let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in + let fpats = List.fold_right (filter_upat ise i0 f (Array.length a)) upats [] in while !i0 >= 0 do let i = !i0 in i0 := -1; let one_match (u, np) = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e1d6fff3e4..5eb8a88698 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -19,7 +19,7 @@ open Context open Vars open Reduction open Reductionops -open Recordops +open Structures open Evarutil open Evardefine open Evarsolve @@ -230,33 +230,30 @@ let occur_rigidly flags env evd (evk,_) t = projection would have been reduced) *) let check_conv_record env sigma (t1,sk1) (t2,sk2) = + let open ValuePattern in let (proji, u), arg = Termops.global_app_of_constr sigma t1 in - let canon_s,sk2_effective = + let (sigma, solution), sk2_effective = try match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then - lookup_canonical_conversion env (proji, Prod_cs), + CanonicalSolution.find env sigma (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> let s = ESorts.kind sigma s in - lookup_canonical_conversion env + CanonicalSolution.find env sigma (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> - lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2 + CanonicalSolution.find env sigma(proji, Proj_cs (Names.Projection.repr p)), Stack.append_app [|c|] sk2 | _ -> let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in - lookup_canonical_conversion env (proji, Const_cs c2),sk2 + CanonicalSolution.find env sigma (proji, Const_cs c2),sk2 with Not_found -> - let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in - (c,cs),[] + CanonicalSolution.find env sigma (proji,Default_cs), [] in - let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; - o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in - let us = List.map EConstr.of_constr us in - let params = List.map EConstr.of_constr params in + let open CanonicalSolution in let params1, c1, extra_args1 = match arg with | Some c -> (* A primitive projection applied to c *) @@ -267,28 +264,19 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 | None -> - match Stack.strip_n_app nparams sk1 with + match Stack.strip_n_app solution.nparams sk1 with | Some (params1, c1, extra_args1) -> params1, c1, extra_args1 | _ -> raise Not_found in let us2,extra_args2 = - let l_us = List.length us in + let l_us = List.length solution.cvalue_arguments in if Int.equal l_us 0 then Stack.empty,sk2_effective else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let u, ctx' = UnivGen.fresh_instance_from ctx None in - let subst = Univ.make_inverse_instance_subst u in - let c = EConstr.of_constr c in - let c' = subst_univs_level_constr subst c in - let t' = EConstr.of_constr t' in - let t' = subst_univs_level_constr subst t' in - let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in - let params = List.map (fun c -> subst_univs_level_constr subst c) params in - let us = List.map (fun c -> subst_univs_level_constr subst c) us in - let h, _ = decompose_app_vect sigma t' in - ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), - (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, - (n, Stack.zip sigma (t2,sk2)) + let h, _ = decompose_app_vect sigma solution.body in + sigma,(h, t2),solution.constant,solution.abstractions_ty,(Stack.append_app_list solution.params Stack.empty,params1), + (Stack.append_app_list solution.cvalue_arguments Stack.empty,us2),(extra_args1,extra_args2),c1, + (solution.cvalue_abstraction, Stack.zip sigma (t2,sk2)) (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) @@ -926,7 +914,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty and f2 i = (try if not flags.with_cs then raise Not_found - else conv_record flags env i + else conv_record flags env (try check_conv_record env i appr1 appr2 with Not_found -> check_conv_record env i appr2 appr1) with Not_found -> UnifFailure (i,NoCanonicalStructure)) @@ -989,7 +977,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let f3 i = (try if not flags.with_cs then raise Not_found - else conv_record flags env i (check_conv_record env i appr1 appr2) + else conv_record flags env (check_conv_record env i appr1 appr2) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = evar_eqappr_x flags env i pbty @@ -1003,7 +991,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let f3 i = (try if not flags.with_cs then raise Not_found - else conv_record flags env i (check_conv_record env i appr2 appr1) + else conv_record flags env (check_conv_record env i appr2 appr1) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = evar_eqappr_x flags env i pbty appr1 @@ -1113,7 +1101,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | LetIn _, _ -> assert false end -and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = +and conv_record flags env (evd,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = (* Tries to unify the states (proji params1 c1 | sk1) = (proji params2 (c (?xs:bs)) | sk2) @@ -1137,7 +1125,6 @@ and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk had to be initially resolved *) - let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in if Reductionops.Stack.compare_shape sk1 sk2 then let (evd',ks,_,test) = List.fold_left @@ -1195,13 +1182,6 @@ let evar_conv_x flags = evar_conv_x flags let evar_unify = conv_fun evar_conv_x -(* Profiling *) -let evar_conv_x = - if Flags.profile then - let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in - CProfile.profile6 evar_conv_xkey evar_conv_x - else evar_conv_x - let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () let evar_conv_x flags = Hook.get evar_conv_hook_get flags diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index be03ced7eb..965cd7de67 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -78,7 +78,7 @@ val check_problems_are_solved : env -> evar_map -> unit val check_conv_record : env -> evar_map -> state -> state -> - Univ.ContextSet.t * (constr * constr) + evar_map * (constr * constr) * constr * constr list * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * constr * diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index de1af62043..21b2137f09 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -35,6 +35,7 @@ open Environ open EConstr open Vars open Reductionops +open Structures open Type_errors open Typing open Evarutil @@ -801,8 +802,8 @@ struct in let app_f = match EConstr.kind sigma fj.uj_val with - | Const (p, u) when Recordops.is_primitive_projection p -> - let p = Option.get @@ Recordops.find_primitive_projection p in + | Const (p, u) when PrimitiveProjections.mem p -> + let p = Option.get @@ PrimitiveProjections.find_opt p in let p = Projection.make p false in let npars = Projection.npars p in fun n -> diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index c31ecc135c..980575abac 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -12,7 +12,7 @@ Cbv Find_subterm Evardefine Evarsolve -Recordops +Structures Heads Evarconv Typing diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli deleted file mode 100644 index 83927085e9..0000000000 --- a/pretyping/recordops.mli +++ /dev/null @@ -1,101 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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 Names -open Constr - -(** Operations concerning records and canonical structures *) - -(** {6 Records } *) -(** A structure S is a non recursive inductive type with a single - constructor (the name of which defaults to Build_S) *) - -type proj_kind = { - pk_name: Name.t; - pk_true_proj: bool; - pk_canonical: bool; -} - -type struc_typ = { - s_CONST : constructor; - s_EXPECTEDPARAM : int; - s_PROJKIND : proj_kind list; - s_PROJ : Constant.t option list; -} - -val register_structure : struc_typ -> unit -val subst_structure : Mod_subst.substitution -> struc_typ -> struc_typ -val rebuild_structure : Environ.env -> struc_typ -> struc_typ - -(** [lookup_structure isp] returns the struc_typ associated to the - inductive path [isp] if it corresponds to a structure, otherwise - it fails with [Not_found] *) -val lookup_structure : inductive -> struc_typ - -(** [lookup_projections isp] returns the projections associated to the - inductive path [isp] if it corresponds to a structure, otherwise - it fails with [Not_found] *) -val lookup_projections : inductive -> Constant.t option list - -(** raise [Not_found] if not a projection *) -val find_projection_nparams : GlobRef.t -> int - -(** raise [Not_found] if not a projection *) -val find_projection : GlobRef.t -> struc_typ - -val is_projection : Constant.t -> bool - -(** Sets up the mapping from constants to primitive projections *) -val register_primitive_projection : Projection.Repr.t -> Constant.t -> unit - -val is_primitive_projection : Constant.t -> bool - -val find_primitive_projection : Constant.t -> Projection.Repr.t option - -(** {6 Canonical structures } *) -(** A canonical structure declares "canonical" conversion hints between - the effective components of a structure and the projections of the - structure *) - -(** A cs_pattern characterizes the form of a component of canonical structure *) -type cs_pattern = - Const_cs of GlobRef.t - | Proj_cs of Projection.Repr.t - | Prod_cs - | Sort_cs of Sorts.family - | Default_cs - -type obj_typ = { - o_ORIGIN : GlobRef.t; - o_DEF : constr; - o_CTX : Univ.AUContext.t; - o_INJ : int option; (** position of trivial argument *) - o_TABS : constr list; (** ordered *) - o_TPARAMS : constr list; (** ordered *) - o_NPARAMS : int; - o_TCOMPS : constr list } (** ordered *) - -(** Return the form of the component of a canonical structure *) -val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list - -val pr_cs_pattern : cs_pattern -> Pp.t - -type cs = GlobRef.t * inductive - -val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ -val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> - cs -> unit -val subst_canonical_structure : Mod_subst.substitution -> cs -> cs -val is_open_canonical_projection : - Environ.env -> Evd.evar_map -> EConstr.t -> bool -val canonical_projections : unit -> - ((GlobRef.t * cs_pattern) * obj_typ) list - -val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4083d3bc23..cb576a379a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1038,13 +1038,6 @@ let nf_all env sigma = (********************************************************************) (* Conversion *) (********************************************************************) -(* -let fkey = CProfile.declare_profile "fhnf";; -let fhnf info v = CProfile.profile2 fkey fhnf info v;; - -let fakey = CProfile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; -*) let is_transparent e k = match Conv_oracle.get_strategy (Environ.oracle e) k with diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 064990f6bf..cdb86afa1a 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -249,17 +249,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) | _ -> assert false -(* Profiling *) -(* let get_type_of polyprop lax env sigma c = *) -(* let f,_,_,_ = retype ~polyprop sigma in *) -(* if lax then f env c else anomaly_on_error (f env) c *) - -(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) -(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) - -(* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) -(* get_type_of polyprop lax env sigma c *) - let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c diff --git a/pretyping/recordops.ml b/pretyping/structures.ml index aa862a912e..3ef6e98373 100644 --- a/pretyping/recordops.ml +++ b/pretyping/structures.ml @@ -37,71 +37,67 @@ open Reductionops * the constant realizing this projection (if any). *) -type proj_kind = { - pk_name: Name.t; - pk_true_proj: bool; - pk_canonical: bool; +module Structure = struct + +type projection = { + proj_name : Names.Name.t; + proj_true : bool; + proj_canonical : bool; + proj_body : Names.Constant.t option; +} + +type t = { + name : Names.inductive; + projections : projection list; + nparams : int; } -type struc_typ = { - s_CONST : constructor; - s_EXPECTEDPARAM : int; - s_PROJKIND : proj_kind list; - s_PROJ : Constant.t option list } +let make env name projections = + let nparams = Inductiveops.inductive_nparams env name in + { name; projections; nparams } let structure_table = - Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs" + Summary.ref (Indmap.empty : t Indmap.t) ~name:"record-structs" let projection_table = - Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs" + Summary.ref (Cmap.empty : t Cmap.t) ~name:"record-projs" -let register_structure ({ s_CONST = (ind,_); s_PROJ = projs; } as struc) = - structure_table := Indmap.add ind struc !structure_table; +let register ({ name; projections; nparams } as s) = + structure_table := Indmap.add name s !structure_table; projection_table := - List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc)) - projs !projection_table - -let subst_structure subst struc = - let projs' = - (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) - (* the first component of subst_con. *) - List.Smart.map - (Option.Smart.map (subst_constant subst)) - struc.s_PROJ - in - let id' = Globnames.subst_constructor subst struc.s_CONST in - if projs' == struc.s_PROJ && id' == struc.s_CONST - then struc - else { struc with s_CONST = id'; s_PROJ = projs' } + List.fold_right (fun { proj_body } m -> + Option.fold_right (fun proj -> Cmap.add proj s) proj_body m) + projections !projection_table -let rebuild_structure env struc = - let mib = Environ.lookup_mind (fst (fst struc.s_CONST)) env in - let npars = mib.Declarations.mind_nparams in - { struc with s_EXPECTEDPARAM = npars } +let subst subst ({ name; projections; nparams } as s) = + let subst_projection subst ({ proj_body } as p) = + let proj_body = Option.Smart.map (subst_constant subst) proj_body in + if proj_body == p.proj_body then p else + { p with proj_body } in + let projections = List.Smart.map (subst_projection subst) projections in + let name = Mod_subst.subst_ind subst name in + if projections == s.projections && + name == s.name + then s + else { name; projections; nparams } -let lookup_structure indsp = Indmap.find indsp !structure_table +let rebuild env s = + let mib = Environ.lookup_mind (fst s.name) env in + let nparams = mib.Declarations.mind_nparams in + { s with nparams } -let lookup_projections indsp = (lookup_structure indsp).s_PROJ +let find indsp = Indmap.find indsp !structure_table -let find_projection_nparams = function - | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM - | _ -> raise Not_found +let find_projections indsp = + (find indsp).projections |> + List.map (fun { proj_body } -> proj_body) -let find_projection = function - | GlobRef.ConstRef cst -> Cmap.find cst !projection_table - | _ -> raise Not_found +let find_from_projection cst = Cmap.find cst !projection_table -let is_projection cst = Cmap.mem cst !projection_table +let projection_nparams cst = (Cmap.find cst !projection_table).nparams -let prim_table = - Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" - -let register_primitive_projection p c = - prim_table := Cmap_env.add c p !prim_table - -let is_primitive_projection c = Cmap_env.mem c !prim_table +let is_projection cst = Cmap.mem cst !projection_table -let find_primitive_projection c = - try Some (Cmap_env.find c !prim_table) with Not_found -> None +end (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) @@ -142,49 +138,55 @@ type obj_typ = { o_NPARAMS : int; o_TCOMPS : constr list } (* ordered *) -type cs_pattern = +module ValuePattern = struct + +type t = Const_cs of GlobRef.t - | Proj_cs of Projection.Repr.t + | Proj_cs of Names.Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs -let eq_cs_pattern env p1 p2 = match p1, p2 with -| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2 -| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2 -| Prod_cs, Prod_cs -> true -| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 -| Default_cs, Default_cs -> true -| _ -> false - -let rec assoc_pat env a = function - | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs - | [] -> raise Not_found - - -let object_table = - Summary.ref (GlobRef.Map.empty : ((cs_pattern * constr) * obj_typ) list GlobRef.Map.t) - ~name:"record-canonical-structs" - -let canonical_projections () = - GlobRef.Map.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc)) - !object_table [] - -let keep_true_projections projs kinds = - let filter (p, { pk_true_proj ; pk_canonical }) = if pk_true_proj then Some (p, pk_canonical) else None in - List.map_filter filter (List.combine projs kinds) +let equal env p1 p2 = match p1, p2 with + | Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2 + | Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2 + | Prod_cs, Prod_cs -> true + | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 + | Default_cs, Default_cs -> true + | _ -> false -let rec cs_pattern_of_constr env t = +let rec of_constr env t = match kind t with | App (f,vargs) -> - let patt, n, args = cs_pattern_of_constr env f in + let patt, n, args = of_constr env f in patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c] + | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (fst @@ destRef t) , None, [] +let print = function + Const_cs c -> Nametab.pr_global_env Id.Set.empty c + | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Names.Projection.Repr.constant p)) + | Prod_cs -> str "_ -> _" + | Default_cs -> str "_" + | Sort_cs s -> Sorts.pr_sort_family s + +end + +let rec assoc_pat env a = function + | ((pat, t), e) :: xs -> if ValuePattern.equal env pat a then (t, e) else assoc_pat env a xs + | [] -> raise Not_found + +let object_table = + Summary.ref (GlobRef.Map.empty : ((ValuePattern.t * constr) * obj_typ) list GlobRef.Map.t) + ~name:"record-canonical-structs" + +let keep_true_projections projs = + let filter { Structure.proj_true ; proj_canonical; proj_body } = if proj_true then Some (proj_body, proj_canonical) else None in + List.map_filter filter projs + let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (sign,env,t,ref,proji_sp) -> @@ -213,17 +215,17 @@ let compute_canonical_projections env ~warn (gref,ind) = let t = EConstr.Unsafe.to_constr t in let o_TABS = List.rev_map snd sign in let args = snd (decompose_app t) in - let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = - lookup_structure ind in + let { Structure.nparams = p; projections = lpj } = + Structure.find ind in let o_TPARAMS, projs = List.chop p args in let o_NPARAMS = List.length o_TPARAMS in - let lpj = keep_true_projections lpj kl in + let lpj = keep_true_projections lpj in let nenv = Termops.push_rels_assum sign env in List.fold_left2 (fun acc (spopt, canonical) t -> if canonical then Option.cata (fun proji_sp -> - match cs_pattern_of_constr nenv t with + match ValuePattern.of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) @@ -235,13 +237,6 @@ let compute_canonical_projections env ~warn (gref,ind) = else acc ) [] lpj projs -let pr_cs_pattern = function - Const_cs c -> Nametab.pr_global_env Id.Set.empty c - | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p)) - | Prod_cs -> str "_ -> _" - | Default_cs -> str "_" - | Sort_cs s -> Sorts.pr_sort_family s - let warn_redundant_canonical_projection = CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker" (fun (hd_val,prj,new_can_s,old_can_s) -> @@ -249,26 +244,13 @@ let warn_redundant_canonical_projection = ++ strbrk " by " ++ prj ++ strbrk " in " ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) -let register_canonical_structure ~warn env sigma o = - compute_canonical_projections env ~warn o |> - List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> - let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in - match assoc_pat env cs_pat l with - | exception Not_found -> - object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table - | _, cs -> - if warn - then - let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in - let new_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF) in - let prj = Nametab.pr_global_env Id.Set.empty proj in - let hd_val = pr_cs_pattern cs_pat in - warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) - ) +module Instance = struct -type cs = GlobRef.t * inductive +type t = GlobRef.t * inductive -let subst_canonical_structure subst (gref,ind as obj) = +let repr = fst + +let subst subst (gref,ind as obj) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) match gref with @@ -286,7 +268,7 @@ let error_not_structure ref description = (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ description)) -let check_and_decompose_canonical_structure env sigma ref = +let make env sigma ref = let vc = match ref with | GlobRef.ConstRef sp -> @@ -311,17 +293,71 @@ let check_and_decompose_canonical_structure env sigma ref = | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let s = - try lookup_structure indsp + try Structure.find indsp with Not_found -> error_not_structure ref (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in - let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in - if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then + let ntrue_projs = List.count (fun { Structure.proj_true = x } -> x) s.Structure.projections in + if s.Structure.nparams + ntrue_projs > Array.length args then error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (ref,indsp) -let lookup_canonical_conversion env (proj,pat) = - assoc_pat env pat (GlobRef.Map.find proj !object_table) +let register ~warn env sigma o = + compute_canonical_projections env ~warn o |> + List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> + let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in + match assoc_pat env cs_pat l with + | exception Not_found -> + object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table + | _, cs -> + if warn + then + let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in + let new_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF) in + let prj = Nametab.pr_global_env Id.Set.empty proj in + let hd_val = ValuePattern.print cs_pat in + warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) + ) + +end + +(** The canonical solution of a problem (proj,val) is a global + [constant = fun abs : abstractions_ty => body] and + [ body = RecodConstructor params canon_values ] and the canonical value + corresponding to val is [val cvalue_arguments]. + It is possible that val is one of the [abs] abstractions, eg [Default_cs], + and in that case [cvalue_abstraction = Some i] *) + +module CanonicalSolution = struct +type t = { + constant : EConstr.t; + + abstractions_ty : EConstr.t list; + body : EConstr.t; + + nparams : int; + params : EConstr.t list; + cvalue_abstraction : int option; + cvalue_arguments : EConstr.t list; +} + +let find env sigma (proj,pat) = + let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; + o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = assoc_pat env pat (GlobRef.Map.find proj !object_table) in + let us = List.map EConstr.of_constr us in + let params = List.map EConstr.of_constr params in + let u, ctx' = UnivGen.fresh_instance_from ctx None in + let subst = Univ.make_inverse_instance_subst u in + let c = EConstr.of_constr c in + let c' = EConstr.Vars.subst_univs_level_constr subst c in + let t' = EConstr.of_constr t' in + let t' = EConstr.Vars.subst_univs_level_constr subst t' in + let bs' = List.map (EConstr.of_constr %> EConstr.Vars.subst_univs_level_constr subst) bs in + let params = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) params in + let us = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) us in + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in + sigma, { body = t'; constant = c'; abstractions_ty = bs'; nparams; params; cvalue_arguments = us; cvalue_abstraction = n } + let rec get_nth n = function | [] -> raise Not_found @@ -336,12 +372,12 @@ let rec decompose_projection sigma c args = | Cast (c, _, _) -> decompose_projection sigma c args | App (c, arg) -> decompose_projection sigma c (arg :: args) | Const (c, u) -> - let n = find_projection_nparams (GlobRef.ConstRef c) in + let n = Structure.projection_nparams c in (* Check if there is some canonical projection attached to this structure *) let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in get_nth n args | Proj (p, c) -> - let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in + let _ = GlobRef.Map.find (GlobRef.ConstRef (Names.Projection.constant p)) !object_table in c | _ -> raise Not_found @@ -355,3 +391,44 @@ let is_open_canonical_projection env sigma c = not (isConstruct sigma hd) with Failure _ -> false with Not_found -> false + +end + +module CSTable = struct + +type entry = { + projection : Names.GlobRef.t; + value : ValuePattern.t; + solution : Names.GlobRef.t; +} + +let canonical_entry_of_object projection ((value,_), { o_ORIGIN = solution }) = + { projection; value; solution } + +let entries () = + GlobRef.Map.fold (fun p ol acc -> + List.fold_right (fun o acc -> canonical_entry_of_object p o :: acc) ol acc) + !object_table [] + +let entries_for ~projection:p = + try + GlobRef.Map.find p !object_table |> + List.map (canonical_entry_of_object p) + with Not_found -> [] + +end + +module PrimitiveProjections = struct + +let prim_table = + Summary.ref (Cmap_env.empty : Names.Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" + +let register p c = + prim_table := Cmap_env.add c p !prim_table + +let mem c = Cmap_env.mem c !prim_table + +let find_opt c = + try Some (Cmap_env.find c !prim_table) with Not_found -> None + +end diff --git a/pretyping/structures.mli b/pretyping/structures.mli new file mode 100644 index 0000000000..05b21b1033 --- /dev/null +++ b/pretyping/structures.mli @@ -0,0 +1,162 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + + +(** A structure S is a non recursive inductive type with a single + constructor *) +module Structure : sig + +(** A projection to a structure field *) +type projection = { + proj_name : Names.Name.t; (** field name *) + proj_true : bool; (** false for primitive records *) + proj_canonical : bool; (** false = not to be used for CS inference *) + proj_body : Names.Constant.t option; (** the projection function *) +} + +type t = { + name : Names.inductive; + projections : projection list; + nparams : int; +} + +val make : Environ.env -> Names.inductive -> projection list -> t + +val register : t -> unit +val subst : Mod_subst.substitution -> t -> t + +(** refreshes nparams, e.g. after section discharging *) +val rebuild : Environ.env -> t -> t + +(** [find isp] returns the Structure.t associated to the + inductive path [isp] if it corresponds to a structure, otherwise + it fails with [Not_found] *) +val find : Names.inductive -> t + +(** raise [Not_found] if not a structure projection *) +val find_from_projection : Names.Constant.t -> t + +(** [lookup_projections isp] returns the projections associated to the + inductive path [isp] if it corresponds to a structure, otherwise + it fails with [Not_found] *) +val find_projections : Names.inductive -> Names.Constant.t option list + +(** raise [Not_found] if not a projection *) +val projection_nparams : Names.Constant.t -> int + +val is_projection : Names.Constant.t -> bool + +end + +(** A canonical instance declares "canonical" conversion hints between + the effective components of a structure and the projections of the + structure *) +module Instance : sig + +type t + +(** Process a record instance, checkig it can be registered as canonical. + The record type must be declared as a canonical Structure.t beforehand. *) +val make : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t + +(** Register an instance as canonical *) +val register : warn:bool -> Environ.env -> Evd.evar_map -> t -> unit + +val subst : Mod_subst.substitution -> t -> t +val repr : t -> Names.GlobRef.t + +end + + +(** A ValuePattern.t characterizes the form of a component of canonical + instance and is used to query the data base of canonical instances *) +module ValuePattern : sig + +type t = + | Const_cs of Names.GlobRef.t + | Proj_cs of Names.Projection.Repr.t + | Prod_cs + | Sort_cs of Sorts.family + | Default_cs + +val equal : Environ.env -> t -> t -> bool +val print : t -> Pp.t + +(** Return the form of the component of a canonical structure *) +val of_constr : Environ.env -> Constr.t -> t * int option * Constr.t list + +end + + +(** The canonical solution of a problem (proj,val) is a global + [constant = fun abs : abstractions_ty => body] and + [body = RecodConstructor params canon_values] and the canonical value + corresponding to val is [val cvalue_arguments]. + It is possible that val is one of the [abs] abstractions, eg [Default_cs], + and in that case [cvalue_abstraction = Some i] *) +module CanonicalSolution : sig + +type t = { + constant : EConstr.t; + + abstractions_ty : EConstr.t list; + body : EConstr.t; + + nparams : int; + params : EConstr.t list; + cvalue_abstraction : int option; + cvalue_arguments : EConstr.t list; +} + +(** [find (p,v)] returns a s such that p s = v. + The solution s gets a fresh universe instance and is decomposed into + bits for consumption by evarconv. Can raise [Not_found] on failure *) +val find : + Environ.env -> Evd.evar_map -> (Names.GlobRef.t * ValuePattern.t) -> + Evd.evar_map * t + +(** [is_open_canonical_projection env sigma t] is true if t is a FieldName + applied to term which is not a constructor. Used by evarconv not to + unfold too much and lose a projection too early *) +val is_open_canonical_projection : + Environ.env -> Evd.evar_map -> EConstr.t -> bool + +end + +(** Low level access to the Canonical Structure database *) +module CSTable : sig + +type entry = { + projection : Names.GlobRef.t; + value : ValuePattern.t; + solution : Names.GlobRef.t; +} + +(** [all] returns the list of tuples { p ; v ; s } + Note: p s = v *) +val entries : unit -> entry list + +(** [entries_for p] returns the list of canonical entries that have + p as their FieldName *) +val entries_for : projection:Names.GlobRef.t -> entry list + +end + +(** Some extra info for structures which are primitive records *) +module PrimitiveProjections : sig + +(** Sets up the mapping from constants to primitive projections *) +val register : Names.Projection.Repr.t -> Names.Constant.t -> unit + +val mem : Names.Constant.t -> bool + +val find_opt : Names.Constant.t -> Names.Projection.Repr.t option + +end diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 4e89018656..b59d4b5655 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1015,12 +1015,6 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = in app_stack (redrec (c, empty_stack)) *) -let whd_simpl_stack = - if Flags.profile then - let key = CProfile.declare_profile "whd_simpl_stack" in - CProfile.profile3 key whd_simpl_stack - else whd_simpl_stack - (* Same as [whd_simpl] but also reduces constants that do not hide a reducible fix, but does this reduction of constants only until it immediately hides a non reducible fix or a cofix *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 51b228a640..dd1d27e4c5 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -242,10 +242,6 @@ let get_solve_all_instances, solve_all_instances_hook = Hook.make () let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail -(** Profiling resolution of typeclasses *) -(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) -(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) - let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = if not (has_typeclasses filter evd) then evd diff --git a/pretyping/unification.ml b/pretyping/unification.ml index df0f49a033..43d562f77d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -22,13 +22,13 @@ open Namegen open Evd open Reduction open Reductionops +open Structures open Evarutil open Evardefine open Evarsolve open Pretype_errors open Retyping open Coercion -open Recordops open Locus open Locusops open Find_subterm @@ -509,13 +509,13 @@ let key_of env sigma b flags f = match EConstr.kind sigma f with | Const (cst, u) when is_transparent env (ConstKey cst) && (TransparentState.is_transparent_constant flags.modulo_delta cst - || Recordops.is_primitive_projection cst) -> + || PrimitiveProjections.mem cst) -> let u = EInstance.kind sigma u in Some (IsKey (ConstKey (cst, u))) | Var id when is_transparent env (VarKey id) && TransparentState.is_transparent_variable flags.modulo_delta id -> Some (IsKey (VarKey id)) - | Proj (p, c) when Projection.unfolded p + | Proj (p, c) when Names.Projection.unfolded p || (is_transparent env (ConstKey (Projection.constant p)) && (TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) -> Some (IsProj (p, c)) @@ -1077,7 +1077,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = if isApp_or_Proj sigma cM then - if is_open_canonical_projection curenv sigma cM then + if CanonicalSolution.is_open_canonical_projection curenv sigma cM then solve_canonical_projection curenvnb pb opt cM cN substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1091,7 +1091,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else try f1 () with e when precatchable_exception e -> if isApp_or_Proj sigma cN then - if is_open_canonical_projection curenv sigma cN then + if CanonicalSolution.is_open_canonical_projection curenv sigma cN then solve_canonical_projection curenvnb pb opt cN cM substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1099,12 +1099,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) = let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in - let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = + let (sigma,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2 with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN) in if Reductionops.Stack.compare_shape ts ts1 then - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in let (evd,ks,_) = List.fold_left (fun (evd,ks,m) b -> @@ -2070,11 +2069,5 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = let w_unify env evd cv_pb flags ty1 ty2 = w_unify env evd cv_pb ~flags:flags ty1 ty2 -let w_unify = - if Flags.profile then - let wunifkey = CProfile.declare_profile "w_unify" in - CProfile.profile6 wunifkey w_unify - else w_unify - let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = w_unify env evd cv_pb flags ty1 ty2 diff --git a/tactics/auto.ml b/tactics/auto.ml index 353e138599..0189e3ab04 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -500,12 +500,6 @@ let delta_auto debug mod_delta n lems dbnames = (search d n mod_delta db_list hints) end -let delta_auto = - if Flags.profile then - let key = CProfile.declare_profile "delta_auto" in - CProfile.profile5 key delta_auto - else delta_auto - let auto ?(debug=Off) n = delta_auto debug false n let new_auto ?(debug=Off) n = delta_auto debug true n diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index af0ca22868..794d2bb94f 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -32,18 +32,25 @@ let compare_term_label t1 t2 = match t1, t2 with type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything -let decomp_pat = +let decomp_pat p = let rec decrec acc = function | PApp (f,args) -> decrec (Array.to_list args @ acc) f - | PProj (p, c) -> (PRef (GlobRef.ConstRef (Projection.constant p)), c :: acc) + | PProj (p, c) -> + let hole = PMeta None in + let params = List.make (Projection.npars p) hole in + (PRef (GlobRef.ConstRef (Projection.constant p)), params @ c :: acc) | c -> (c,acc) in - decrec [] + decrec [] p let decomp sigma t = let rec decrec acc c = match EConstr.kind sigma c with | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc) + | Proj (p, c) -> + (* Hack: fake evar to generate [Everything] in the functions below *) + let hole = mkEvar (Evar.unsafe_of_int (-1), []) in + let params = List.make (Projection.npars p) hole in + (mkConst (Projection.constant p), params @ c :: acc) | Cast (c1,_,_) -> decrec acc c1 | _ -> (c,acc) in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 20c557b282..5df9fab236 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -359,9 +359,6 @@ let e_search_auto debug (in_depth,p) lems db_list = tclIDTAC gl end -(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) -(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) - let eauto_with_bases ?(debug=Off) np lems db_list = Hints.wrap_hint_warning (e_search_auto debug np lems db_list) diff --git a/tactics/hints.ml b/tactics/hints.ml index 5e9c3baeb1..31b276bb3e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -320,7 +320,7 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (cst,_) -> - (match Recordops.find_primitive_projection cst with + (match Structures.PrimitiveProjections.find_opt cst with | Some p -> let p = Projection.make p false in let npars = Projection.npars p in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67bf8d0d29..c24520b371 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1555,7 +1555,7 @@ let make_projection env sigma params cstr sign elim i n c u = | Some proj -> let args = Context.Rel.to_extended_vect mkRel 0 sign in let proj = - match Recordops.find_primitive_projection proj with + match Structures.PrimitiveProjections.find_opt proj with | Some proj -> mkProj (Projection.make proj false, mkApp (c, args)) | None -> @@ -1585,7 +1585,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let params = List.map EConstr.of_constr params in let cstr = (get_constructors env indf).(0) in let elim = - try DefinedRecord (Recordops.lookup_projections ind) + try DefinedRecord (Structures.Structure.find_projections ind) with Not_found -> let u = EInstance.kind sigma u in let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in @@ -1886,12 +1886,6 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) -(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) - -(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) -(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) - let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) diff --git a/test-suite/bugs/closed/bug_14009.v b/test-suite/bugs/closed/bug_14009.v new file mode 100644 index 0000000000..bf86f5117e --- /dev/null +++ b/test-suite/bugs/closed/bug_14009.v @@ -0,0 +1,16 @@ +Class Bin {P:Type} (A B : P) := {}. + +Set Primitive Projections. + +Record test (n : nat) := { proj : Prop }. +Axiom Bin_test : forall {t1 t2 : test O}, Bin (proj _ t1) (proj _ t2). + +Create HintDb db discriminated. +#[local] Hint Resolve Bin_test : db. +#[local] Hint Opaque proj : db. + +Goal forall t1 t2 : test O, Bin (proj O t1) (proj O t2). +Proof. +intros. +solve [typeclasses eauto with db]. +Qed. diff --git a/test-suite/bugs/closed/bug_14011.v b/test-suite/bugs/closed/bug_14011.v new file mode 100644 index 0000000000..ccbeca792d --- /dev/null +++ b/test-suite/bugs/closed/bug_14011.v @@ -0,0 +1,32 @@ +(** Test that Ltac2 Array.init doesn't compute the first argument twice, and has the correct asymptotics when nested *) +Require Import Ltac2.Ltac2. + +(** Non-performance-based test *) +Ltac2 foo () := + let x := { contents := 0 } in + let _ := Array.init 1 (fun _ => x.(contents) := Int.add 1 (x.(contents))) in + Control.assert_true (Int.equal 1 (x.(contents))). + +Ltac2 Eval foo (). + +Ltac2 Type rec singleton := [ Single (int) | Arr (singleton array) ]. +Ltac2 rec init_rec (n : int) := + match Int.equal n 0 with + | true => Single 0 + | false => Arr (Array.init 1 (fun _ => init_rec (Int.sub n 1))) + end. +Ltac2 rec timing (n : int) := + (match Int.equal n 0 with + | true => () + | false => timing (Int.sub n 1) + end; + Message.print (Message.concat (Message.of_int n) (Message.of_string ": ")); + let _ := Control.time None (fun _ => init_rec n) in + ()). +(** Should take less than 0.1 seconds if the asymptotics are correct. +Previous behavior was to take an expected 1 million times the age of +the universe. Capping the time at 100 seconds seems like a reasonable +middle ground between these times, as I expect that compilation of Coq +itself will not finish in reasonable time if the computer is running +1000x slower than modern machines. *) +Timeout 100 Ltac2 Eval timing 100. diff --git a/test-suite/bugs/closed/bug_9000.v b/test-suite/bugs/closed/bug_9000.v new file mode 100644 index 0000000000..e239c8b1fe --- /dev/null +++ b/test-suite/bugs/closed/bug_9000.v @@ -0,0 +1,17 @@ +Set Primitive Projections. +Class type (t : Type) : Type := + { bar : t -> Prop }. + +Instance type_nat : type nat := + { bar := fun _ => True }. + +Definition foo_bar {n : nat} : bar n := I. + +#[local] Hint Resolve (@foo_bar) : typeclass_instances. +#[local] Hint Resolve I : typeclass_instances. +Check ltac:(typeclasses eauto with nocore typeclass_instances) : True. +Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _. +Existing Class bar. +Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _. +#[local] Hint Resolve (@foo_bar) : foo. +Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _. diff --git a/test-suite/output/bug_13240.out b/test-suite/output/bug_13240.out new file mode 100644 index 0000000000..5fccef5cfe --- /dev/null +++ b/test-suite/output/bug_13240.out @@ -0,0 +1,3 @@ +Ltac t1 a b := a ; last b +Ltac t2 := do !idtac +Ltac t3 := idtac => True diff --git a/test-suite/output/bug_13240.v b/test-suite/output/bug_13240.v new file mode 100644 index 0000000000..a999450cd2 --- /dev/null +++ b/test-suite/output/bug_13240.v @@ -0,0 +1,10 @@ +Require Import ssreflect. + +Ltac t1 a b := a; last b. +Print t1. + +Ltac t2 := do !idtac. +Print t2. + +Ltac t3 := idtac => True. +Print t3. diff --git a/test-suite/primitive/arrays/set.v b/test-suite/primitive/arrays/set.v index f265c37ea8..787d2867dd 100644 --- a/test-suite/primitive/arrays/set.v +++ b/test-suite/primitive/arrays/set.v @@ -20,3 +20,50 @@ Definition x3 := Eval compute in t.[1]. Definition foo9 := (eq_refl : x3 = 3). Definition x4 := Eval cbn in t.[1]. Definition foo10 := (eq_refl : x4 = 3). + +Ltac check_const_eq name constr := + let v := (eval cbv delta [name] in name) in + tryif constr_eq v constr + then idtac + else fail 0 "Not syntactically equal:" name ":=" v "<>" constr. + +Notation check_const_eq name constr := (ltac:(check_const_eq name constr; exact constr)) (only parsing). + +(* Stuck primitive *) +Definition lazy_stuck_set := Eval lazy in (fun A (t : array A) v => t.[1 <- v]). +Definition vm_stuck_set := Eval vm_compute in (fun A (t : array A) v => t.[1 <- v]). +Definition native_stuck_set := Eval native_compute in (fun A (t : array A) v => t.[1 <- v]). +Definition compute_stuck_set := Eval compute in (fun A (t : array A) v => t.[1 <- v]). +Definition cbn_stuck_set := Eval cbn in (fun A (t : array A) v => t.[1 <- v]). + +Check check_const_eq lazy_stuck_set (fun A (t : array A) v => t.[1 <- v]). +Check check_const_eq vm_stuck_set (fun A (t : array A) v => t.[1 <- v]). +Check check_const_eq native_stuck_set (fun A (t : array A) v => t.[1 <- v]). +Check check_const_eq compute_stuck_set (fun A (t : array A) v => t.[1 <- v]). +Check check_const_eq cbn_stuck_set (fun A (t : array A) v => t.[1 <- v]). + +(* Not stuck primitive, but with an accumulator as last argument *) +Definition lazy_accu_set := Eval lazy in (fun v => t.[1 <- v]). +Definition vm_accu_set := Eval vm_compute in (fun v => t.[1 <- v]). +Definition native_accu_set := Eval native_compute in (fun v => t.[1 <- v]). +Definition compute_accu_set := Eval compute in (fun v => t.[1 <- v]). +Definition cbn_accu_set := Eval cbn in (fun v => t.[1 <- v]). + +Check check_const_eq lazy_accu_set (fun v => [| 1; v; 2 | 4 |]). +Check check_const_eq vm_accu_set (fun v => [| 1; v; 2 | 4 |]). +Check check_const_eq native_accu_set (fun v => [| 1; v; 2 | 4 |]). +Check check_const_eq compute_accu_set (fun v => [| 1; v; 2 | 4 |]). +Check check_const_eq cbn_accu_set (fun v => [| 1; v; 2 | 4 |]). + +(* Under-application *) +Definition lazy_set := Eval lazy in @PArray.set. +Definition vm_set := Eval vm_compute in @PArray.set. +Definition native_set := Eval native_compute in @PArray.set. +Definition compute_set := Eval compute in @PArray.set. +Definition cbn_set := Eval cbn in @PArray.set. + +Check check_const_eq lazy_set (@PArray.set). +Check check_const_eq vm_set (fun A (t : array A) i v => t.[i <- v]). +Check check_const_eq native_set (fun A (t : array A) i v => t.[i <- v]). +Check check_const_eq compute_set (@PArray.set). +Check check_const_eq cbn_set (@PArray.set). diff --git a/theories/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v index 29bd732c78..b4aed4c3f7 100644 --- a/theories/extraction/ExtrOcamlBigIntConv.v +++ b/theories/extraction/ExtrOcamlBigIntConv.v @@ -8,12 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Extraction to Ocaml: conversion from/to [big_int] *) +(** Extraction to OCaml: conversion from/to [Z.t] *) -(** NB: The extracted code should be linked with [nums.cm(x)a] - from ocaml's stdlib and with the wrapper [big.ml] that - simplifies the use of [Big_int] (it can be found in the sources - of Coq). *) +(** NB: The extracted code should be linked with [zarith.cm(x)a] and with + the [big.ml] wrapper. The latter can be found in the sources of Coq. *) Require Coq.extraction.Extraction. diff --git a/theories/extraction/ExtrOcamlNatBigInt.v b/theories/extraction/ExtrOcamlNatBigInt.v index 8a7ba92a94..c854f8fd5d 100644 --- a/theories/extraction/ExtrOcamlNatBigInt.v +++ b/theories/extraction/ExtrOcamlNatBigInt.v @@ -8,17 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Extraction of [nat] into Ocaml's [big_int] *) +(** Extraction of [nat] into Zarith's [Z.t] *) Require Coq.extraction.Extraction. Require Import Arith Even Div2 EqNat Euclid. Require Import ExtrOcamlBasic. -(** NB: The extracted code should be linked with [nums.cm(x)a] - from ocaml's stdlib and with the wrapper [big.ml] that - simplifies the use of [Big_int] (it can be found in the sources - of Coq). *) +(** NB: The extracted code should be linked with [zarith.cm(x)a] and with + the [big.ml] wrapper. The latter can be found in the sources of Coq. *) (** Disclaimer: trying to obtain efficient certified programs by extracting [nat] into [big_int] isn't necessarily a good idea. diff --git a/theories/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v index 40a47b36fa..df9153a46d 100644 --- a/theories/extraction/ExtrOcamlZBigInt.v +++ b/theories/extraction/ExtrOcamlZBigInt.v @@ -8,17 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *) +(** Extraction of [positive], [N], and [Z], into Zarith's [Z.t] *) Require Coq.extraction.Extraction. Require Import ZArith NArith. Require Import ExtrOcamlBasic. -(** NB: The extracted code should be linked with [nums.cm(x)a] - from ocaml's stdlib and with the wrapper [big.ml] that - simplifies the use of [Big_int] (it can be found in the sources - of Coq). *) +(** NB: The extracted code should be linked with [zarith.cm(x)a] and with + the [big.ml] wrapper. The latter can be found in the sources of Coq. *) (** Disclaimer: trying to obtain efficient certified programs by extracting [Z] into [big_int] isn't necessarily a good idea. diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v index 5adba829c5..b5e7f37c9f 100644 --- a/user-contrib/Ltac2/Array.v +++ b/user-contrib/Ltac2/Array.v @@ -70,7 +70,7 @@ Ltac2 init (l : int) (f : int->'a) := | true => empty () | false => let arr:=make l (f 0) in - init_aux arr 0 (length arr) f; + init_aux arr 1 (Int.sub l 1) f; arr end. diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v index fd1555c2fb..0f7167939b 100644 --- a/user-contrib/Ltac2/Ltac1.v +++ b/user-contrib/Ltac2/Ltac1.v @@ -40,5 +40,8 @@ Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_ap Ltac2 @ external of_constr : constr -> t := "ltac2" "ltac1_of_constr". Ltac2 @ external to_constr : t -> constr option := "ltac2" "ltac1_to_constr". +Ltac2 @ external of_ident : ident -> t := "ltac2" "ltac1_of_ident". +Ltac2 @ external to_ident : t -> ident option := "ltac2" "ltac1_to_ident". + Ltac2 @ external of_list : t list -> t := "ltac2" "ltac1_of_list". Ltac2 @ external to_list : t -> t list option := "ltac2" "ltac1_to_list". diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index fa7df5dfeb..457b8e1acf 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1186,6 +1186,16 @@ let () = define1 "ltac1_to_constr" ltac1 begin fun v -> return (Value.of_option Value.of_constr (Tacinterp.Value.to_constr v)) end +let () = define1 "ltac1_of_ident" ident begin fun c -> + let open Ltac_plugin in + return (Value.of_ext val_ltac1 (Taccoerce.Value.of_ident c)) +end + +let () = define1 "ltac1_to_ident" ltac1 begin fun v -> + let open Ltac_plugin in + return (Value.of_option Value.of_ident (Taccoerce.Value.to_ident v)) +end + let () = define1 "ltac1_of_list" (list ltac1) begin fun l -> let open Geninterp.Val in return (Value.of_ext val_ltac1 (inject (Base typ_list) l)) diff --git a/vernac/canonical.ml b/vernac/canonical.ml index eaa6c84791..2c04032ca0 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -7,30 +7,30 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names open Libobject -open Recordops +open Structures let open_canonical_structure i (_, (o,_)) = let env = Global.env () in let sigma = Evd.from_env env in - if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o + if Int.equal i 1 then Instance.register env sigma ~warn:false o let cache_canonical_structure (_, (o,_)) = let env = Global.env () in let sigma = Evd.from_env env in - register_canonical_structure ~warn:true env sigma o + Instance.register ~warn:true env sigma o -let discharge_canonical_structure (_,((gref, _ as x), local)) = +let discharge_canonical_structure (_,(x, local)) = + let gref = Instance.repr x in if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None else Some (x, local) -let inCanonStruc : (GlobRef.t * inductive) * bool -> obj = +let inCanonStruc : Instance.t * bool -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = simple_open open_canonical_structure; cache_function = cache_canonical_structure; - subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local); + subst_function = (fun (subst,(c,local)) -> Instance.subst subst c, local); classify_function = (fun x -> Substitute x); discharge_function = discharge_canonical_structure } @@ -39,4 +39,4 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let declare_canonical_structure ?(local=false) ref = let env = Global.env () in let sigma = Evd.from_env env in - add_canonical_structure (check_and_decompose_canonical_structure env sigma ref, local) + add_canonical_structure (Instance.make env sigma ref, local) diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 86b15739f9..26d696ff8e 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -90,7 +90,7 @@ let uniform_cond sigma ctx lt = let class_of_global = function | GlobRef.ConstRef sp -> - (match Recordops.find_primitive_projection sp with + (match Structures.PrimitiveProjections.find_opt sp with | Some p -> CL_PROJ p | None -> CL_CONST sp) | GlobRef.IndRef sp -> CL_IND sp | GlobRef.VarRef id -> CL_SECVAR id @@ -141,8 +141,8 @@ let get_target env t ind = CL_FUN else match pi1 (find_class_type env Evd.empty (EConstr.of_constr t)) with - | CL_CONST p when Recordops.is_primitive_projection p -> - CL_PROJ (Option.get @@ Recordops.find_primitive_projection p) + | CL_CONST p when Structures.PrimitiveProjections.mem p -> + CL_PROJ (Option.get @@ Structures.PrimitiveProjections.find_opt p) | x -> x let strength_of_cl = function @@ -265,7 +265,7 @@ let inCoercion : coe_info_typ -> obj = let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = let isproj = match coef with - | GlobRef.ConstRef c -> Recordops.find_primitive_projection c + | GlobRef.ConstRef c -> Structures.PrimitiveProjections.find_opt c | _ -> None in let c = { diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index 1b811f3db7..39520a68ec 100644 --- a/vernac/comSearch.ml +++ b/vernac/comSearch.ml @@ -41,8 +41,8 @@ let kind_searcher = Decls.(function Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr && (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions) | IsDefinition CanonicalStructure -> - let canonproj = Recordops.canonical_projections () in - Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj) + let canonproj = Structures.CSTable.entries () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Structures.CSTable.solution gr) canonproj) | IsDefinition Scheme -> let schemes = DeclareScheme.all_schemes () in Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes) diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index 7050ddc042..2ab6e3bb15 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -76,7 +76,7 @@ let objInductive : inductive_obj Libobject.Dyn.tag = let inInductive v = Libobject.Dyn.Easy.inj v objInductive -let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c +let cache_prim (_,(p,c)) = Structures.PrimitiveProjections.register p c let load_prim _ p = cache_prim p diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index ec6e3b44ba..a3cd7a8edc 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -24,7 +24,6 @@ open Impargs open Libobject open Libnames open Globnames -open Recordops open Printer open Printmod open Context.Rel.Declaration @@ -1005,22 +1004,24 @@ let print_path_between cls clt = print_path ((cls, clt), p) let print_canonical_projections env sigma grefs = - let match_proj_gref ((x,y),c) gr = - GlobRef.equal x gr || - begin match y with - | Const_cs y -> GlobRef.equal y gr + let open Structures in + let match_proj_gref { CSTable.projection; value; solution } gr = + GlobRef.equal projection gr || + begin match value with + | ValuePattern.Const_cs y -> GlobRef.equal y gr | _ -> false end || - GlobRef.equal c.o_ORIGIN gr + GlobRef.equal solution gr in let projs = List.filter (fun p -> List.for_all (match_proj_gref p) grefs) - (canonical_projections ()) + (CSTable.entries ()) in prlist_with_sep fnl - (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ + (fun { CSTable.projection; value; solution } -> + ValuePattern.print value ++ str " <- " ++ - pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )") + pr_global projection ++ str " ( " ++ pr_global solution ++ str " )") projs (*************************************************************************) diff --git a/vernac/record.ml b/vernac/record.ml index ff6bdc5199..fccc3e4fbd 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -22,6 +22,7 @@ open Type_errors open Constrexpr open Constrexpr_ops open Context.Rel.Declaration +open Structures module RelDecl = Context.Rel.Declaration @@ -348,7 +349,7 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = this could be refactored as noted above by moving to the higher-level declare constant API *) let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls - paramargs decl impls fid subst sp_projs nfi ti i indsp mib lifted_fields x rp = + paramargs decl impls fid subst nfi ti i indsp mib lifted_fields x rp = let ccl = subst_projection fid subst ti in let body, p_opt = match decl with | LocalDef (_,ci,_) -> subst_projection fid subst ci, None @@ -396,32 +397,33 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl end; let i = if is_local_assum decl then i+1 else i in - (Some kn::sp_projs, i, Projection term::subst) + (Some kn, i, Projection term::subst) (** [build_proj] will build a projection for each field, or skip if the field is anonymous, i.e. [_ : t] *) let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs - (nfi,i,kinds,sp_projs,subst) flags decl impls = + (nfi,i,kinds,subst) flags decl impls = let fi = RelDecl.get_name decl in let ti = RelDecl.get_type decl in - let (sp_projs,i,subst) = + let (sp_proj,i,subst) = match fi with | Anonymous -> - (None::sp_projs,i,NoProjection fi::subst) + (None,i,NoProjection fi::subst) | Name fid -> try build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid - subst sp_projs nfi ti i indsp mib lifted_fields x rp + subst nfi ti i indsp mib lifted_fields x rp with NotDefinable why as exn -> let _, info = Exninfo.capture exn in warning_or_error ~info flags.pf_subclass indsp why; - (None::sp_projs,i,NoProjection fi::subst) + (None,i,NoProjection fi::subst) in (nfi - 1, i, - { Recordops.pk_name = fi - ; pk_true_proj = is_local_assum decl - ; pk_canonical = flags.pf_canonical } :: kinds - , sp_projs, subst) + { Structure.proj_name = fi + ; proj_true = is_local_assum decl + ; proj_canonical = flags.pf_canonical + ; proj_body = sp_proj } :: kinds + , subst) (** [declare_projections] prepares the common context for all record projections and then calls [build_proj] for each one. *) @@ -445,11 +447,12 @@ let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name | PrimRecord _ -> true | FakeRecord | NotRecord -> false in - let (_,_,kinds,sp_projs,_) = + let (_,_,canonical_projections,_) = List.fold_left3 (build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs) - (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls) - in (kinds,sp_projs) + (List.length fields,0,[],[]) flags (List.rev fields) (List.rev fieldimpls) + in + List.rev canonical_projections open Typeclasses @@ -485,20 +488,17 @@ let check_template ~template ~poly ~univs ~params { Data.id; rdata = { DataR.min (* auto detect template *) ComInductive.should_auto_template id (template && template_candidate ()) -let load_structure i (_, structure) = - Recordops.register_structure structure +let load_structure i (_, structure) = Structure.register structure -let cache_structure o = - load_structure 1 o +let cache_structure o = load_structure 1 o -let subst_structure (subst, obj) = - Recordops.subst_structure subst obj +let subst_structure (subst, obj) = Structure.subst subst obj let discharge_structure (_, x) = Some x -let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s +let rebuild_structure s = Structure.rebuild (Global.env()) s -let inStruc : Recordops.struc_typ -> Libobject.obj = +let inStruc : Structure.t -> Libobject.obj = let open Libobject in declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; @@ -601,17 +601,10 @@ let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls par let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in + let projections = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in let build = GlobRef.ConstructRef cstr in let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in - let npars = Inductiveops.inductive_nparams (Global.env()) rsp in - let struc = { - Recordops.s_CONST = cstr; - s_PROJ = List.rev sp_projs; - s_PROJKIND = List.rev kinds; - s_EXPECTEDPARAM = npars; - } - in + let struc = Structure.make (Global.env ()) rsp projections in let () = declare_structure_entry struc in rsp in @@ -674,7 +667,7 @@ let build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template meth_info = b; meth_const = y; } in - let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in + let l = List.map3 map (List.rev fields) coers (Structure.find_projections ind) in GlobRef.IndRef ind, l in List.map map inds diff --git a/vernac/record.mli b/vernac/record.mli index 7a40af048c..feb257da3c 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -11,6 +11,7 @@ open Names open Vernacexpr open Constrexpr +open Structures module Ast : sig type t = @@ -51,8 +52,8 @@ module Internal : sig -> projection_flags list -> Impargs.manual_implicits list -> Constr.rel_context - -> Recordops.proj_kind list * Names.Constant.t option list + -> Structure.projection list - val declare_structure_entry : Recordops.struc_typ -> unit + val declare_structure_entry : Structure.t -> unit end |