diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 73 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 6 |
3 files changed, 53 insertions, 33 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e30f553fe..399264859 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -362,7 +362,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual + doesn't seem worth the effort (except for huge mutual fixpoints ?) *) let possible_indexes = Array.to_list (Array.mapi (fun i (n,_) -> match n with @@ -668,8 +668,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env evdref lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !evdref in let evd = nf_evar_defs evd in - let c' = nf_evar (evars_of evd) c' in - let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in let c' = nf_evar (evars_of evd) c' in evdref := evd; c' @@ -684,7 +683,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j = pretype empty_tycon env evdref ([],[]) c in let evd,_ = consider_remaining_unif_problems env !evdref in let j = j_nf_evar (evars_of evd) j in - let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:true env (evars_of evd) evd in let j = j_nf_evar (evars_of evd) j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index f9ab283ad..7a95f9c35 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -216,7 +216,7 @@ let instances r = with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id) let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) -let solve_instanciations_problem = ref (fun _ _ -> assert false) +let solve_instanciations_problem = ref (fun _ _ _ _ -> assert false) let resolve_typeclass env ev evi (evd, defined as acc) = try @@ -278,34 +278,43 @@ let destClassApp c = | _ when isInd c -> Some (destInd c, [||]) | _ -> None -let resolve_typeclasses ?(check=true) env sigma evd = +let is_independent evm ev = + Evd.fold (fun ev' evi indep -> indep && + (ev = ev' || + evi.evar_body <> Evar_empty || + not (Termops.occur_evar ev evi.evar_concl))) + evm true + + (* try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *) (* with _ -> *) - let evm = Evd.evars_of evd in - let tc_evars = - let f ev evi acc = - let (l, k) = Evd.evar_source ev evd in - if not check || is_implicit_arg k then - match destClassApp evi.evar_concl with - | Some (i, args) when is_class i -> - Evd.add acc ev evi - | _ -> acc - else acc - in Evd.fold f evm Evd.empty - in - let rec sat evars = - let (evars', progress) = - Evd.fold - (fun ev evi acc -> - if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then - resolve_typeclass env ev evi acc - else acc) - (Evd.evars_of evars) (evars, false) - in - if not progress then evars' - else - sat (Evarutil.nf_evar_defs evars') - in sat (Evarutil.nf_evar_defs evd) +(* let evm = Evd.evars_of evd in *) +(* let tc_evars = *) +(* let f ev evi acc = *) +(* let (l, k) = Evd.evar_source ev evd in *) +(* if not check || is_implicit_arg k then *) +(* match destClassApp evi.evar_concl with *) +(* | Some (i, args) when is_class i -> *) +(* Evd.add acc ev evi *) +(* | _ -> acc *) +(* else acc *) +(* in Evd.fold f evm Evd.empty *) +(* in *) +(* let rec sat evars = *) +(* let evm = Evd.evars_of evars in *) +(* let (evars', progress) = *) +(* Evd.fold *) +(* (fun ev evi acc -> *) +(* if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) *) +(* && evi.evar_body = Evar_empty then *) +(* resolve_typeclass env ev evi acc *) +(* else acc) *) +(* evm (evars, false) *) +(* in *) +(* if not progress then evars' *) +(* else *) +(* sat (Evarutil.nf_evar_defs evars') *) +(* in sat (Evarutil.nf_evar_defs evd) *) let class_of_constr c = let extract_ind c = @@ -317,6 +326,16 @@ let class_of_constr c = App (c, _) -> extract_ind c | _ -> extract_ind c +let has_typeclasses evd = + Evd.fold (fun ev evi has -> has || + (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None)) + evd false + +let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd = + if not (has_typeclasses sigma) then evd + else + !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs all + type substitution = (identifier * constr) list let substitution_of_named_context isevars env id n subst l = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index db408c889..f231c7406 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -61,10 +61,10 @@ val is_class : inductive -> bool val class_of_constr : constr -> typeclass option val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool -val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs +val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref -val solve_instanciations_problem : (env -> evar_defs -> evar_defs) ref +val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> evar_defs) ref type substitution = (identifier * constr) list @@ -73,3 +73,5 @@ val substitution_of_named_context : substitution -> named_context -> substitution val nf_substitution : evar_map -> substitution -> substitution + +val is_implicit_arg : hole_kind -> bool |