aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include2
-rw-r--r--interp/constrextern.ml38
-rw-r--r--interp/constrintern.ml32
-rw-r--r--kernel/mod_subst.ml5
-rw-r--r--kernel/mod_subst.mli3
-rw-r--r--library/globnames.ml4
-rw-r--r--library/globnames.mli1
-rw-r--r--plugins/extraction/extraction.ml7
-rw-r--r--plugins/ssrmatching/ssrmatching.ml20
-rw-r--r--pretyping/evarconv.ml51
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/pretyping.ml5
-rw-r--r--pretyping/pretyping.mllib2
-rw-r--r--pretyping/recordops.mli101
-rw-r--r--pretyping/structures.ml (renamed from pretyping/recordops.ml)309
-rw-r--r--pretyping/structures.mli163
-rw-r--r--pretyping/unification.ml13
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/tactics.ml4
-rw-r--r--vernac/canonical.ml16
-rw-r--r--vernac/comCoercion.ml8
-rw-r--r--vernac/comSearch.ml4
-rw-r--r--vernac/declareInd.ml2
-rw-r--r--vernac/prettyp.ml19
-rw-r--r--vernac/record.ml57
-rw-r--r--vernac/record.mli5
26 files changed, 503 insertions, 372 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/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/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/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/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..285fea183b 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
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/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..a1cc38e8e0
--- /dev/null
+++ b/pretyping/structures.mli
@@ -0,0 +1,163 @@
+(************************************************************************)
+(* * 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/unification.ml b/pretyping/unification.ml
index df0f49a033..18db75eed5 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 ->
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..decf19588f 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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:10:36 +0000