aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/evarutil.ml7
-rw-r--r--pretyping/evarutil.mli3
-rw-r--r--pretyping/typeclasses.ml87
-rw-r--r--pretyping/typeclasses.mli17
-rw-r--r--pretyping/unification.ml47
6 files changed, 112 insertions, 51 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 586ad716d..2f5099c1a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -79,7 +79,7 @@ module Default = struct
| [] -> { uj_val = applist (j_val funj,argl);
uj_type = typ }
| h::restl ->
- (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
+ (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
| Prod (_,c1,c2) ->
(* Typage garanti par l'appel à app_coercion*)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8d19feea4..0fe691358 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1231,8 +1231,11 @@ let check_evars env initial_sigma evd c =
assert (Evd.mem sigma evk);
if not (Evd.mem initial_sigma evk) then
let (loc,k) = evar_source evk evd in
- let evi = nf_evar_info sigma (Evd.find sigma evk) in
- error_unsolvable_implicit loc env sigma evi k None
+ (match k with
+ | ImplicitArg (gr, (i, id), false) -> ()
+ | _ ->
+ let evi = nf_evar_info sigma (Evd.find sigma evk) in
+ error_unsolvable_implicit loc env sigma evi k None)
| _ -> iter_constr proc_rec c
in proc_rec c
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index dc212c9ca..883a64b9a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -191,3 +191,6 @@ exception ClearDependencyError of identifier * clear_dependency_error
val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
identifier list -> named_context_val * types
+
+val push_rel_context_to_named_context : Environ.env -> types ->
+ named_context_val * types * constr list
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ceaf25be0..38fca2f19 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -24,6 +24,17 @@ open Typeclasses_errors
open Libobject
(*i*)
+
+let add_instance_hint_ref = ref (fun id pri -> assert false)
+let register_add_instance_hint =
+ (:=) add_instance_hint_ref
+let add_instance_hint id = !add_instance_hint_ref id
+
+let set_typeclass_transparency_ref = ref (fun id pri -> assert false)
+let register_set_typeclass_transparency =
+ (:=) set_typeclass_transparency_ref
+let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c
+
let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -54,10 +65,10 @@ type instance = {
-1 for discard, 0 for none, mutable to avoid redeclarations
when multiple rebuild_object happen. *)
is_global: int;
- is_impl: constant;
+ is_impl: global_reference;
}
-type instances = (global_reference, instance Cmap.t) Gmap.t
+type instances = (global_reference, (global_reference, instance) Gmap.t) Gmap.t
let instance_impl is = is.is_impl
@@ -95,11 +106,6 @@ let _ =
Summary.unfreeze_function = unfreeze;
Summary.init_function = init }
-let add_instance_hint_ref = ref (fun id pri -> assert false)
-let register_add_instance_hint =
- (:=) add_instance_hint_ref
-let add_instance_hint id = !add_instance_hint_ref id
-
(*
* classes persistent object
*)
@@ -177,11 +183,11 @@ let add_class cl =
* instances persistent object
*)
-let load_instance (_,inst) =
- let insts =
- try Gmap.find inst.is_class !instances
- with Not_found -> Cmap.empty in
- let insts = Cmap.add inst.is_impl inst insts in
+let load_instance (_,inst) =
+ let insts =
+ try Gmap.find inst.is_class !instances
+ with Not_found -> Gmap.empty in
+ let insts = Gmap.add inst.is_impl inst insts in
instances := Gmap.add inst.is_class insts !instances
let cache_instance = load_instance
@@ -189,7 +195,7 @@ let cache_instance = load_instance
let subst_instance (subst,inst) =
{ inst with
is_class = fst (subst_global subst inst.is_class);
- is_impl = fst (Mod_subst.subst_con subst inst.is_impl) }
+ is_impl = fst (subst_global subst inst.is_impl) }
let discharge_instance (_,inst) =
if inst.is_global <= 0 then None
@@ -197,7 +203,7 @@ let discharge_instance (_,inst) =
{ inst with
is_global = pred inst.is_global;
is_class = Lib.discharge_global inst.is_class;
- is_impl = Lib.discharge_con inst.is_impl }
+ is_impl = Lib.discharge_global inst.is_impl }
let rebuild_instance inst =
add_instance_hint inst.is_impl inst.is_pri;
@@ -222,6 +228,36 @@ let add_instance i =
Lib.add_anonymous_leaf (instance_input i);
add_instance_hint i.is_impl i.is_pri
+open Declarations
+
+let add_constant_class cst =
+ let ty = Typeops.type_of_constant (Global.env ()) cst in
+ let ctx, arity = decompose_prod_assum ty in
+ let tc =
+ { cl_impl = ConstRef cst;
+ cl_context = ([], ctx);
+ cl_props = [(Anonymous, None, arity)];
+ cl_projs = []
+ }
+ in add_class tc;
+ set_typeclass_transparency (EvalConstRef cst) false
+
+let add_inductive_class ind =
+ let mind, oneind = Global.lookup_inductive ind in
+ let k =
+ let ty = Inductive.type_of_inductive_knowing_parameters
+ (push_rel_context oneind.mind_arity_ctxt (Global.env ()))
+ oneind (Termops.rel_vect 1 (List.length oneind.mind_arity_ctxt))
+ in
+ { cl_impl = IndRef ind;
+ cl_context = [], oneind.mind_arity_ctxt;
+ cl_props = [Anonymous, None, ty];
+ cl_projs = [] }
+ in add_class k;
+ Array.iteri (fun i _ ->
+ add_instance (new_instance k None true (ConstructRef (ind, succ i))))
+ oneind.mind_consnames
+
(*
* interface functions
*)
@@ -243,25 +279,24 @@ let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
let cmapl_add x y m =
try
let l = Gmap.find x m in
- Gmap.add x (Cmap.add y.is_impl y l) m
+ Gmap.add x (Gmap.add y.is_impl y l) m
with Not_found ->
- Gmap.add x (Cmap.add y.is_impl y Cmap.empty) m
+ Gmap.add x (Gmap.add y.is_impl y Gmap.empty) m
-let cmap_elements c = Cmap.fold (fun k v acc -> v :: acc) c []
+let cmap_elements c = Gmap.fold (fun k v acc -> v :: acc) c []
let instances_of c =
try cmap_elements (Gmap.find c.cl_impl !instances) with Not_found -> []
-let all_instances () =
- Gmap.fold (fun k v acc ->
- Cmap.fold (fun k v acc -> v :: acc) v acc)
+let all_instances () =
+ Gmap.fold (fun k v acc ->
+ Gmap.fold (fun k v acc -> v :: acc) v acc)
!instances []
-let instances r =
- let cl = class_info r in instances_of cl
-
-
-let is_class gr =
+let instances r =
+ let cl = class_info r in instances_of cl
+
+let is_class gr =
Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false
let is_instance = function
@@ -273,6 +308,8 @@ let is_instance = function
(match Decls.variable_kind v with
| IsDefinition Instance -> true
| _ -> false)
+ | ConstructRef (ind,_) ->
+ is_class (IndRef ind)
| _ -> false
let is_implicit_arg k =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c9ee9adf0..19ec47cf4 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -49,7 +49,11 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> int option -> bool -> constant -> instance
+val add_constant_class : constant -> unit
+
+val add_inductive_class : inductive -> unit
+
+val new_instance : typeclass -> int option -> bool -> global_reference -> instance
val add_instance : instance -> unit
val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
@@ -60,8 +64,8 @@ val dest_class_app : env -> constr -> typeclass * constr list
(* Just return None if not a class *)
val class_of_constr : constr -> typeclass option
-
-val instance_impl : instance -> constant
+
+val instance_impl : instance -> global_reference
val is_class : global_reference -> bool
val is_instance : global_reference -> bool
@@ -86,8 +90,11 @@ val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
env -> evar_defs -> evar_defs
val resolve_one_typeclass : env -> evar_map -> types -> open_constr
-val register_add_instance_hint : (constant -> int option -> unit) -> unit
-val add_instance_hint : constant -> int option -> unit
+val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
+val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
+
+val register_add_instance_hint : (global_reference -> int option -> unit) -> unit
+val add_instance_hint : global_reference -> int option -> unit
val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8d95a798..a3e63541f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -27,6 +27,18 @@ open Retyping
open Coercion.Default
open Recordops
+let occur_meta_or_undefined_evar evd c =
+ let rec occrec c = match kind_of_term c with
+ | Meta _ -> raise Occur
+ | Evar (ev,args) ->
+ (match evar_body (Evd.find evd ev) with
+ | Evar_defined c ->
+ occrec c; Array.iter occrec args
+ | Evar_empty -> raise Occur)
+ | Sort s when is_sort_variable evd s -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur | Not_found -> true
+
(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
@@ -192,15 +204,16 @@ let oracle_order env cf1 cf2 =
let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
let trivial_unify curenv pb (sigma,metasubst,_) m n =
let subst = if flags.use_metas_eagerly then metasubst else ms in
- match subst_defined_metas subst m with
- | Some m1 ->
- if (match flags.modulo_conv_on_closed_terms with
- Some flags ->
+ match subst_defined_metas subst m, subst_defined_metas subst n with
+ | Some m1, Some n1 ->
+ let evd = (create_evar_defs sigma) in
+ if (occur_meta_or_undefined_evar evd m1 || occur_meta_or_undefined_evar evd n1)
+ then false
+ else if (match flags.modulo_conv_on_closed_terms with
+ | Some flags ->
is_trans_fconv (conv_pb_of pb) flags env sigma m1 n
- | None -> false) then true else
- if (not (is_ground_term (create_evar_defs sigma) m1))
- || occur_meta_or_existential n then false else
- error_cannot_unify curenv sigma (m, n)
+ | None -> false) then true
+ else error_cannot_unify curenv sigma (m, n)
| _ -> false in
let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
let cM = Evarutil.whd_castappevar sigma curm
@@ -370,22 +383,20 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
in
- if (if occur_meta m then false else
- if (match flags.modulo_conv_on_closed_terms with
- Some flags ->
- is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
- | None -> constr_cmp (conv_pb_of cv_pb) m n) then true else
- if (not (is_ground_term (create_evar_defs sigma) m))
- || occur_meta_or_existential n then false else
- if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+ let evd = create_evar_defs sigma in
+ if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n then false
+ else if (match flags.modulo_conv_on_closed_terms with
+ | Some flags ->
+ is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
+ | None -> constr_cmp (conv_pb_of cv_pb) m n) then true
+ else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
| Some (cv_id, cv_k), (dl_id, dl_k) ->
Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
| None,(dl_id, dl_k) ->
Idpred.is_empty dl_id && Cpred.is_empty dl_k)
then error_cannot_unify env sigma (m, n) else false)
then subst
- else
- unirec_rec (env,0) cv_pb conv_at_top subst m n
+ else unirec_rec (env,0) cv_pb conv_at_top subst m n
let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:49:12 +0000