diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 28 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 11 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
3 files changed, 30 insertions, 15 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ded159e484..015c26531a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -189,8 +189,10 @@ let interp_sort_info ?loc evd l = type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option +type use_typeclasses = NoUseTC | UseTCForConv | UseTC + type inference_flags = { - use_typeclasses : bool; + use_typeclasses : use_typeclasses; solve_unification_constraints : bool; fail_evar : bool; expand_evars : bool; @@ -231,7 +233,7 @@ let frozen_and_pending_holes (sigma, sigma') = end in FrozenProgress data -let apply_typeclasses ~program_mode env sigma frozen fail_evar = +let apply_typeclasses ~program_mode ~fail_evar env sigma frozen = let filter_frozen = match frozen with | FrozenId map -> fun evk -> Evar.Map.mem evk map | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen @@ -270,7 +272,7 @@ let apply_heuristics env sigma fail_evar = let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen = (* Naive way, call resolution again with failure flag *) - apply_typeclasses ~program_mode env current_sigma frozen true + apply_typeclasses ~program_mode ~fail_evar:true env current_sigma frozen let check_extra_evars_are_solved env current_sigma frozen = match frozen with | FrozenId _ -> () @@ -312,9 +314,9 @@ let solve_remaining_evars ?hook flags env ?initial sigma = let program_mode = flags.program_mode in let frozen = frozen_and_pending_holes (initial, sigma) in let sigma = - if flags.use_typeclasses - then apply_typeclasses ~program_mode env sigma frozen false - else sigma + match flags.use_typeclasses with + | UseTC -> apply_typeclasses ~program_mode ~fail_evar:false env sigma frozen + | NoUseTC | UseTCForConv -> sigma in let sigma = match hook with | None -> sigma @@ -1287,21 +1289,25 @@ let ise_pretype_gen flags env sigma lvar kind c = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let env = GlobEnv.make ~hypnaming env sigma lvar in + let use_tc = match flags.use_typeclasses with + | NoUseTC -> false + | UseTC | UseTCForConv -> true + in let sigma', c', c'_ty = match kind with | WithoutTypeConstraint | UnknownIfTermOrType -> - let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in + let sigma, j = pretype ~program_mode ~poly use_tc empty_tycon env sigma c in sigma, j.uj_val, j.uj_type | OfType exptyp -> - let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses (mk_tycon exptyp) env sigma c in + let sigma, j = pretype ~program_mode ~poly use_tc (mk_tycon exptyp) env sigma c in sigma, j.uj_val, j.uj_type | IsType -> - let sigma, tj = pretype_type ~program_mode ~poly flags.use_typeclasses empty_valcon env sigma c in + let sigma, tj = pretype_type ~program_mode ~poly use_tc empty_valcon env sigma c in sigma, tj.utj_val, mkSort tj.utj_type in process_inference_flags flags !!env sigma (sigma',c',c'_ty) let default_inference_flags fail = { - use_typeclasses = true; + use_typeclasses = UseTC; solve_unification_constraints = true; fail_evar = fail; expand_evars = true; @@ -1310,7 +1316,7 @@ let default_inference_flags fail = { } let no_classes_no_fail_inference_flags = { - use_typeclasses = false; + use_typeclasses = NoUseTC; solve_unification_constraints = true; fail_evar = false; expand_evars = true; diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index abbb745161..8be7b1477b 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -44,8 +44,17 @@ type typing_constraint = | OfType of types (** A term of the expected type *) | WithoutTypeConstraint (** A term of unknown expected type *) +type use_typeclasses = NoUseTC | UseTCForConv | UseTC +(** Typeclasses are used in 2 ways: + +- through the "Typeclass Resolution For Conversion" option, if a + conversion problem fails we try again after resolving typeclasses + (UseTCForConv and UseTC) +- after pretyping we resolve typeclasses (UseTC) (in [solve_remaining_evars]) +*) + type inference_flags = { - use_typeclasses : bool; + use_typeclasses : use_typeclasses; solve_unification_constraints : bool; fail_evar : bool; expand_evars : bool; diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8822cc2338..8bb268a92e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -715,7 +715,7 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with f x := t. End M. Definition f := u. and say goodbye to any hope of refolding M.f this way ... *) -let magicaly_constant_of_fixbody env sigma reference bd = function +let magically_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> let open UnivProblem in @@ -757,7 +757,7 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in + | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -799,7 +799,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in + | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) |