From 34ece1ae3e6696bdc9556e5019c3b8ec3fd23f8a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 18 Mar 2021 19:15:39 +0100 Subject: [recordops] complete API rewrite; the module is now called [structures] --- pretyping/evarconv.ml | 51 ++---- pretyping/evarconv.mli | 2 +- pretyping/pretyping.ml | 5 +- pretyping/pretyping.mllib | 2 +- pretyping/recordops.ml | 357 -------------------------------------- pretyping/recordops.mli | 101 ----------- pretyping/structures.ml | 434 ++++++++++++++++++++++++++++++++++++++++++++++ pretyping/structures.mli | 163 +++++++++++++++++ pretyping/unification.ml | 13 +- 9 files changed, 627 insertions(+), 501 deletions(-) delete mode 100644 pretyping/recordops.ml delete mode 100644 pretyping/recordops.mli create mode 100644 pretyping/structures.ml create mode 100644 pretyping/structures.mli (limited to 'pretyping') 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.ml b/pretyping/recordops.ml deleted file mode 100644 index aa862a912e..0000000000 --- a/pretyping/recordops.ml +++ /dev/null @@ -1,357 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* 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' } - -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 lookup_structure indsp = Indmap.find indsp !structure_table - -let lookup_projections indsp = (lookup_structure indsp).s_PROJ - -let find_projection_nparams = function - | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM - | _ -> raise Not_found - -let find_projection = function - | GlobRef.ConstRef cst -> Cmap.find cst !projection_table - | _ -> raise Not_found - -let is_projection cst = Cmap.mem cst !projection_table - -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 find_primitive_projection c = - try Some (Cmap_env.find c !prim_table) with Not_found -> None - -(************************************************************************) -(*s A canonical structure declares "canonical" conversion hints between *) -(* the effective components of a structure and the projections of the *) -(* structure *) - -(* Table of "object" definitions: for each object c, - - c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) - - If ti has the form (ci ui1...uir) where ci is a global reference (or - a sort, or a product or a reference to a parameter) and if the - corresponding projection Li of the structure R is defined, one - declares a "conversion" between ci and Li. - - x1:B1..xk:Bk |- (Li a1..am (c x1..xk)) =_conv (ci ui1...uir) - - that maps the pair (Li,ci) to the following data - - o_ORIGIN = c (the constant name which this conversion rule is - synthesized from) - o_DEF = c - o_TABS = B1...Bk - o_INJ = Some n (when ci is a reference to the parameter xi) - o_TPARAMS = a1...am - o_NPARAMS = m - o_TCOMP = ui1...uir - -*) - -type obj_typ = { - o_ORIGIN : GlobRef.t; - o_DEF : constr; - o_CTX : Univ.AUContext.t; - o_INJ : int option; (* position of trivial argument if any *) - o_TABS : constr list; (* ordered *) - o_TPARAMS : constr list; (* ordered *) - o_NPARAMS : int; - o_TCOMPS : constr list } (* ordered *) - -type cs_pattern = - Const_cs of GlobRef.t - | Proj_cs of 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 rec cs_pattern_of_constr env t = - match kind t with - | App (f,vargs) -> - let patt, n, args = cs_pattern_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] - | Sort s -> Sort_cs (Sorts.family s), None, [] - | _ -> Const_cs (fst @@ destRef t) , None, [] - -let warn_projection_no_head_constant = - CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (sign,env,t,ref,proji_sp) -> - let env = Termops.push_rels_assum sign env in - let con_pp = Nametab.pr_global_env Id.Set.empty ref in - let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in - let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in - strbrk "Projection value has no head constant: " - ++ term_pp ++ strbrk " in canonical instance " - ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") - -(* Intended to always succeed *) -let compute_canonical_projections env ~warn (gref,ind) = - let o_CTX = Environ.universes_of_global env gref in - let o_DEF, c = - match gref with - | GlobRef.ConstRef con -> - let u = Univ.make_abstract_instance o_CTX in - mkConstU (con, u), Environ.constant_value_in env (con,u) - | GlobRef.VarRef id -> - mkVar id, Option.get (Environ.named_body id env) - | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false - in - let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in - let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in - 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 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 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 - | 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 }) - :: acc - | exception DestKO -> - if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); - acc - ) acc spopt - 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) -> - strbrk "Ignoring canonical projection to " ++ hd_val - ++ 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) - ) - -type cs = GlobRef.t * inductive - -let subst_canonical_structure subst (gref,ind as obj) = - (* invariant: cst is an evaluable reference. Thus we can take *) - (* the first component of subst_con. *) - match gref with - | GlobRef.ConstRef cst -> - let cst' = subst_constant subst cst in - let ind' = subst_ind subst ind in - if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind') - | _ -> assert false - -(*s High-level declaration of a canonical structure *) - -let error_not_structure ref description = - user_err ~hdr:"object_declare" - (str"Could not declare a canonical structure " ++ - (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ - description)) - -let check_and_decompose_canonical_structure env sigma ref = - let vc = - match ref with - | GlobRef.ConstRef sp -> - let u = Univ.make_abstract_instance (Environ.constant_context env sp) in - begin match Environ.constant_opt_value_in env (sp, u) with - | Some vc -> vc - | None -> error_not_structure ref (str "Could not find its value in the global environment.") end - | GlobRef.VarRef id -> - begin match Environ.named_body id env with - | Some b -> b - | None -> error_not_structure ref (str "Could not find its value in the global environment.") end - | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> - error_not_structure ref (str "Expected an instance of a record or structure.") - in - let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in - let body = EConstr.Unsafe.to_constr body in - let f,args = match kind body with - | App (f,args) -> f,args - | _ -> - error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in - let indsp = match kind f with - | 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 - 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 - 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 rec get_nth n = function -| [] -> raise Not_found -| arg :: args -> - let len = Array.length arg in - if n < len then arg.(n) - else get_nth (n - len) args - -let rec decompose_projection sigma c args = - match EConstr.kind sigma c with - | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) 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 - (* 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 - c - | _ -> raise Not_found - -let is_open_canonical_projection env sigma c = - let open EConstr in - try - let arg = decompose_projection sigma c [] in - try - let arg = whd_all env sigma arg in - let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in - not (isConstruct sigma hd) - with Failure _ -> false - with Not_found -> false 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 *) -(* 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/structures.ml b/pretyping/structures.ml new file mode 100644 index 0000000000..3ef6e98373 --- /dev/null +++ b/pretyping/structures.ml @@ -0,0 +1,434 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + Option.fold_right (fun proj -> Cmap.add proj s) proj_body m) + projections !projection_table + +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 rebuild env s = + let mib = Environ.lookup_mind (fst s.name) env in + let nparams = mib.Declarations.mind_nparams in + { s with nparams } + +let find indsp = Indmap.find indsp !structure_table + +let find_projections indsp = + (find indsp).projections |> + List.map (fun { proj_body } -> proj_body) + +let find_from_projection cst = Cmap.find cst !projection_table + +let projection_nparams cst = (Cmap.find cst !projection_table).nparams + +let is_projection cst = Cmap.mem cst !projection_table + +end + +(************************************************************************) +(*s A canonical structure declares "canonical" conversion hints between *) +(* the effective components of a structure and the projections of the *) +(* structure *) + +(* Table of "object" definitions: for each object c, + + c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) + + If ti has the form (ci ui1...uir) where ci is a global reference (or + a sort, or a product or a reference to a parameter) and if the + corresponding projection Li of the structure R is defined, one + declares a "conversion" between ci and Li. + + x1:B1..xk:Bk |- (Li a1..am (c x1..xk)) =_conv (ci ui1...uir) + + that maps the pair (Li,ci) to the following data + + o_ORIGIN = c (the constant name which this conversion rule is + synthesized from) + o_DEF = c + o_TABS = B1...Bk + o_INJ = Some n (when ci is a reference to the parameter xi) + o_TPARAMS = a1...am + o_NPARAMS = m + o_TCOMP = ui1...uir + +*) + +type obj_typ = { + o_ORIGIN : GlobRef.t; + o_DEF : constr; + o_CTX : Univ.AUContext.t; + o_INJ : int option; (* position of trivial argument if any *) + o_TABS : constr list; (* ordered *) + o_TPARAMS : constr list; (* ordered *) + o_NPARAMS : int; + o_TCOMPS : constr list } (* ordered *) + +module ValuePattern = struct + +type t = + Const_cs of GlobRef.t + | Proj_cs of Names.Projection.Repr.t + | Prod_cs + | Sort_cs of Sorts.family + | Default_cs + +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 of_constr env t = + match kind t with + | App (f,vargs) -> + 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 (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) -> + let env = Termops.push_rels_assum sign env in + let con_pp = Nametab.pr_global_env Id.Set.empty ref in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in + let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in + strbrk "Projection value has no head constant: " + ++ term_pp ++ strbrk " in canonical instance " + ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") + +(* Intended to always succeed *) +let compute_canonical_projections env ~warn (gref,ind) = + let o_CTX = Environ.universes_of_global env gref in + let o_DEF, c = + match gref with + | GlobRef.ConstRef con -> + let u = Univ.make_abstract_instance o_CTX in + mkConstU (con, u), Environ.constant_value_in env (con,u) + | GlobRef.VarRef id -> + mkVar id, Option.get (Environ.named_body id env) + | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false + in + let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in + 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 { 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 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 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 }) + :: acc + | exception DestKO -> + if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); + acc + ) acc spopt + else acc + ) [] lpj projs + +let warn_redundant_canonical_projection = + CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker" + (fun (hd_val,prj,new_can_s,old_can_s) -> + strbrk "Ignoring canonical projection to " ++ hd_val + ++ strbrk " by " ++ prj ++ strbrk " in " + ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) + +module Instance = struct + +type t = GlobRef.t * inductive + +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 + | GlobRef.ConstRef cst -> + let cst' = subst_constant subst cst in + let ind' = subst_ind subst ind in + if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind') + | _ -> assert false + +(*s High-level declaration of a canonical structure *) + +let error_not_structure ref description = + user_err ~hdr:"object_declare" + (str"Could not declare a canonical structure " ++ + (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ + description)) + +let make env sigma ref = + let vc = + match ref with + | GlobRef.ConstRef sp -> + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in + begin match Environ.constant_opt_value_in env (sp, u) with + | Some vc -> vc + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.VarRef id -> + begin match Environ.named_body id env with + | Some b -> b + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> + error_not_structure ref (str "Expected an instance of a record or structure.") + in + let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in + let body = EConstr.Unsafe.to_constr body in + let f,args = match kind body with + | App (f,args) -> f,args + | _ -> + error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in + let indsp = match kind f with + | Construct ((indsp,1),u) -> indsp + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in + let s = + 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 { 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 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 +| arg :: args -> + let len = Array.length arg in + if n < len then arg.(n) + else get_nth (n - len) args + +let rec decompose_projection sigma c args = + match EConstr.kind sigma c with + | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args + | Cast (c, _, _) -> decompose_projection sigma c args + | App (c, arg) -> decompose_projection sigma c (arg :: args) + | Const (c, u) -> + 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 (Names.Projection.constant p)) !object_table in + c + | _ -> raise Not_found + +let is_open_canonical_projection env sigma c = + let open EConstr in + try + let arg = decompose_projection sigma c [] in + try + let arg = whd_all env sigma arg in + let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in + 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 *) +(* 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 -> -- cgit v1.2.3