diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 66 | ||||
-rw-r--r-- | pretyping/cases.mli | 8 | ||||
-rw-r--r-- | pretyping/coercion.ml | 65 | ||||
-rw-r--r-- | pretyping/coercion.mli | 14 | ||||
-rw-r--r-- | pretyping/detyping.ml | 2 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
-rw-r--r-- | pretyping/glob_ops.ml | 2 | ||||
-rw-r--r-- | pretyping/glob_ops.mli | 2 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 44 | ||||
-rw-r--r-- | pretyping/pretyping.mli | 2 | ||||
-rw-r--r-- | pretyping/typing.ml | 6 | ||||
-rw-r--r-- | pretyping/typing.mli | 2 | ||||
-rw-r--r-- | pretyping/unification.ml | 4 |
13 files changed, 110 insertions, 111 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 347c49f44..f5e2e52a1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -122,7 +122,7 @@ type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : Name.t list; - eqn_loc : Loc.t; + eqn_loc : Loc.t option; used : bool ref } type 'a matrix = 'a equation list @@ -251,7 +251,7 @@ type 'a pattern_matching_problem = tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : Loc.t; + caseloc : Loc.t option; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } @@ -281,8 +281,8 @@ let inductive_template evdref env tmloc ind = let arsign = inductive_alldecls_env env indu in let indu = on_snd EInstance.make indu in let hole_source i = match tmloc with - | Some loc -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) - | None -> (Loc.ghost, Evar_kinds.TomatchTypeParameter (ind,i)) in + | Some loc -> Loc.tag ~loc @@ Evar_kinds.TomatchTypeParameter (ind,i) + | None -> Loc.tag @@ Evar_kinds.TomatchTypeParameter (ind,i) in let (_,evarl,_) = List.fold_right (fun decl (subst,evarl,n) -> @@ -351,7 +351,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env (Some loc) indopt in let j = typing_fun tycon env evdref tomatch in - let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in + let evd, j = Coercion.inh_coerce_to_base ~loc:(loc_of_glob_constr tomatch) env !evdref j in evdref := evd; let typ = nf_evar !evdref j.uj_type in let t = @@ -370,7 +370,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl = (************************************************************************) (* Utils *) -let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref = +let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e let evd_comb2 f evdref x y = @@ -402,7 +402,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let _ = e_cumul pb.env pb.evdref indt typ in current else - (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env) + (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) pb.evdref (make_judge current typ) indt).uj_val in let sigma = !(pb.evdref) in (current,try_find_ind pb.env sigma indt names)) @@ -469,11 +469,11 @@ let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } exception NotAdjustable -let rec adjust_local_defs loc = function +let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> - pat :: adjust_local_defs loc (pats,decls) + pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - (Loc.tag ~loc @@ PatVar Anonymous) :: adjust_local_defs loc (pats,decls) + (Loc.tag ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable @@ -489,14 +489,14 @@ let check_and_adjust_constructor env ind cstrs = function if Int.equal (List.length args) nb_args_constr then pat else try - let args' = adjust_local_defs loc (args, List.rev ci.cs_args) + let args' = adjust_local_defs ~loc (args, List.rev ci.cs_args) in Loc.tag ~loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> error_wrong_numarg_constructor ~loc env cstr nb_args_constr else (* Try to insert a coercion *) try - Coercion.inh_pattern_coerce_to loc env pat ind' ind + Coercion.inh_pattern_coerce_to ~loc env pat ind' ind with Not_found -> error_bad_constructor ~loc env cstr ind @@ -510,7 +510,7 @@ let check_all_variables env sigma typ mat = let check_unused_pattern env eqn = if not !(eqn.used) then - raise_pattern_matching_error ~loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns) + raise_pattern_matching_error ?loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns) let set_used_pattern eqn = eqn.used := true @@ -978,7 +978,7 @@ let add_assert_false_case pb tomatch = avoid_ids = []; it = None }; alias_stack = Anonymous::aliasnames; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false } ] let adjust_impossible_cases pb pred tomatch submat = @@ -1545,7 +1545,7 @@ let matx_of_eqns env eqns = it = Some initial_rhs } in { patterns = initial_lpat; alias_stack = []; - eqn_loc = loc; + eqn_loc = Some loc; used = ref false; rhs = rhs } in List.map build_eqn eqns @@ -1629,11 +1629,11 @@ let rec list_assoc_in_triple x = function * similarly for each ti. *) -let abstract_tycon loc env evdref subst tycon extenv t = +let abstract_tycon ?loc env evdref subst tycon extenv t = let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with - | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk) - | _ -> (loc,Evar_kinds.CasesType true) in + | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) + | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in (* We traverse the type T of the original problem Xi looking for subterms that match the non-constructor part of the constraints (this part @@ -1687,7 +1687,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = in aux (0,extenv,subst0) t0 -let build_tycon loc env tycon_env s subst tycon extenv evdref t = +let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let t,tt = match t with | None -> (* This is the situation we are building a return predicate and @@ -1695,10 +1695,10 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in + e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in (lift (n'-n) impossible_case_type, mkSort u) | Some t -> - let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in + let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in @@ -1786,7 +1786,7 @@ let build_inversion_problem loc env sigma tms t = let main_eqn = { patterns = patl; alias_stack = []; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; (* we assume all vars are used; in practice we discard dependent @@ -1806,7 +1806,7 @@ let build_inversion_problem loc env sigma tms t = else [ { patterns = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) patl; alias_stack = []; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; rhs_vars = []; @@ -1827,7 +1827,7 @@ let build_inversion_problem loc env sigma tms t = mat = main_eqn :: catch_all_eqn; caseloc = loc; casestyle = RegularStyle; - typing_function = build_tycon loc env pb_env s subst} in + typing_function = build_tycon ?loc env pb_env s subst} in let pred = (compile pb).uj_val in (!evdref,pred) @@ -1880,10 +1880,10 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | _ -> assert false in List.rev (buildrec 0 (tomatchl,tmsign)) -let inh_conv_coerce_to_tycon loc env evdref j tycon = +let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in + let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in evdref := evd'; j | None -> j @@ -1966,7 +1966,7 @@ let noccur_with_meta sigma n m term = in try (occur_rec n term; true) with LocalOccur -> false -let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = +let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = let refresh_tycon sigma t = (** If we put the typing constraint in the term, it has to be refreshed to preserve the invariant that no algebraic universe @@ -1997,7 +1997,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = | None -> let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((t, _), sigma, _) = - new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in + new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in let sigma = Sigma.to_evar_map sigma in sigma, t in @@ -2438,7 +2438,7 @@ let context_of_arsign l = l ([], 0) in x -let compile_program_cases loc style (typing_function, evdref) tycon env +let compile_program_cases ?loc style (typing_function, evdref) tycon env (predopt, tomatchl, eqns) = let typing_fun tycon env = function | Some t -> typing_function tycon env evdref t @@ -2545,9 +2545,9 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (**************************************************************************) (* Main entry of the matching compilation *) -let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = +let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then - compile_program_cases loc style (typing_fun, evdref) + compile_program_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) else @@ -2564,7 +2564,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e with the type of arguments to match; if none is provided, we build alternative possible predicates *) let arsign = extract_arity_signature env tomatchs tomatchl in - let preds = prepare_predicate loc typing_fun env !evdref tomatchs arsign tycon predopt in + let preds = prepare_predicate ?loc typing_fun env !evdref tomatchs arsign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = (* We push the initial terms to match and push their alias to rhs' envs *) @@ -2614,7 +2614,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e let j = compile pb in (* We coerce to the tycon (if an elim predicate was provided) *) - let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in + let j = inh_conv_coerce_to_tycon ?loc env myevdref j tycon in evdref := !myevdref; j in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 6c2b5bf68..b16342db4 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -38,7 +38,7 @@ val irrefutable : env -> cases_pattern -> bool (** {6 Compilation primitive. } *) val compile_cases : - Loc.t -> case_style -> + ?loc:Loc.t -> case_style -> (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> env -> glob_constr option * tomatch_tuples * cases_clauses -> @@ -65,7 +65,7 @@ type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : Name.t list; - eqn_loc : Loc.t; + eqn_loc : Loc.t option; used : bool ref } type 'a matrix = 'a equation list @@ -106,14 +106,14 @@ type 'a pattern_matching_problem = tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : Loc.t; + caseloc : Loc.t option; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } val compile : 'a pattern_matching_problem -> unsafe_judgment -val prepare_predicate : Loc.t -> +val prepare_predicate : ?loc:Loc.t -> (Evarutil.type_constraint -> Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) -> Environ.env -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index b2c1d0116..acccfc125 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -75,25 +75,25 @@ let apply_coercion_args env evd check isproj argl funj = !evdref, res (* appliquer le chemin de coercions de patterns p *) -let apply_pattern_coercion loc pat p = +let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> let f i = - if i<n then (Loc.tag ~loc @@ Glob_term.PatVar Anonymous) else pat in - Loc.tag ~loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) + if i<n then (Loc.tag ?loc @@ Glob_term.PatVar Anonymous) else pat in + Loc.tag ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) pat p (* raise Not_found if no coercion found *) -let inh_pattern_coerce_to loc env pat ind1 ind2 = +let inh_pattern_coerce_to ?loc env pat ind1 ind2 = let p = lookup_pattern_path_between env (ind1,ind2) in - apply_pattern_coercion loc pat p + apply_pattern_coercion ?loc pat p (* Program coercions *) open Program -let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c = - let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in +let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) env evdref c = + let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = @@ -142,7 +142,7 @@ let mu env evdref t = | None -> (None, v) in aux t -and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) +and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) : (EConstr.constr -> EConstr.constr) option = let open Context.Rel.Declaration in @@ -183,7 +183,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential loc env evdref eq in + let evar = make_existential ?loc env evdref eq in let eq_app x = papp evdref coq_eq_rect [| eqT; hdx; pred; x; hdy; evar|] in @@ -326,7 +326,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) Some (fun x -> let cx = app_opt env evdref c x in - let evar = make_existential loc env evdref (mkApp (p, [| cx |])) + let evar = make_existential ?loc env evdref (mkApp (p, [| cx |])) in (papp evdref sig_intro [| u; p; cx; evar |])) | None -> @@ -340,9 +340,9 @@ let app_coercion env evdref coercion v = let v' = Typing.e_solve_evars env evdref (f v) in whd_betaiota !evdref v' -let coerce_itf loc env evd v t c1 = +let coerce_itf ?loc env evd v t c1 = let evdref = ref evd in - let coercion = coerce loc env evdref t c1 in + let coercion = coerce ?loc env evdref t c1 in let t = Option.map (app_coercion env evdref coercion) v in !evdref, t @@ -410,16 +410,16 @@ let type_judgment env sigma j = | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | _ -> error_not_a_type env sigma j -let inh_tosort_force loc env evd j = +let inh_tosort_force ?loc env evd j = try let t,p = lookup_path_to_sort_from env evd j.uj_type in let evd,j1 = apply_coercion env evd p j t in let j2 = on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env evd j2) with Not_found | NoCoercion -> - error_not_a_type ~loc env evd j + error_not_a_type ?loc env evd j -let inh_coerce_to_sort loc env evd j = +let inh_coerce_to_sort ?loc env evd j = let typ = whd_all env evd j.uj_type in match EConstr.kind evd typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s }) @@ -427,9 +427,9 @@ let inh_coerce_to_sort loc env evd j = let (evd',s) = Evardefine.define_evar_as_sort env evd ev in (evd',{ utj_val = j.uj_val; utj_type = s }) | _ -> - inh_tosort_force loc env evd j + inh_tosort_force ?loc env evd j -let inh_coerce_to_base loc env evd j = +let inh_coerce_to_base ?loc env evd j = if Flags.is_program_mode () then let evdref = ref evd in let ct, typ' = mu env evdref j.uj_type in @@ -439,7 +439,7 @@ let inh_coerce_to_base loc env evd j = in !evdref, res else (evd, j) -let inh_coerce_to_prod loc env evd t = +let inh_coerce_to_prod ?loc env evd t = if Flags.is_program_mode () then let evdref = ref evd in let _, typ' = mu env evdref t in @@ -466,7 +466,7 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = try (the_conv_x_leq env t' c1 evd, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = +let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail env evd rigidonly v t c1 @@ -488,49 +488,50 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = let open Context.Rel.Declaration in let env1 = push_rel (LocalAssum (name,u1)) env in let (evd', v1) = - inh_conv_coerce_to_fail loc env1 evd rigidonly + inh_conv_coerce_to_fail ?loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in let v1 = Option.get v1 in let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in let t2 = match v2 with | None -> subst_term evd' v1 t2 | Some v2 -> Retyping.get_type_of env1 evd' v2 in - let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in + let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = +let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t = let (evd', val') = try - inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (best_failed_evd,e) -> try if Flags.is_program_mode () then - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> - error_actual_type ~loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in try if evd' == evd then - error_actual_type ~loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e else - inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type ~loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) -let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false -let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true +let inh_conv_coerce_to ?loc resolve_tc = inh_conv_coerce_to_gen ?loc resolve_tc false -let inh_conv_coerces_to loc env evd t t' = +let inh_conv_coerce_rigid_to ?loc resolve_tc = inh_conv_coerce_to_gen resolve_tc ?loc true + +let inh_conv_coerces_to ?loc env evd t t' = try - fst (inh_conv_coerce_to_fail loc env evd true None t t') + fst (inh_conv_coerce_to_fail ?loc env evd true None t t') with NoCoercion -> evd (* Maybe not enough information to unify *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index bc63d092d..25ee82bbf 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -26,17 +26,17 @@ val inh_app_fun : bool -> (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a sort; it fails if no coercion is applicable *) -val inh_coerce_to_sort : Loc.t -> +val inh_coerce_to_sort : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type its base type (the notion depends on the coercion system) *) -val inh_coerce_to_base : Loc.t -> +val inh_coerce_to_base : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) -val inh_coerce_to_prod : Loc.t -> +val inh_coerce_to_prod : ?loc:Loc.t -> env -> evar_map -> types -> evar_map * types (** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an @@ -44,20 +44,20 @@ val inh_coerce_to_prod : Loc.t -> a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) -val inh_conv_coerce_to : bool -> Loc.t -> +val inh_conv_coerce_to : ?loc:Loc.t -> bool -> env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment -val inh_conv_coerce_rigid_to : bool -> Loc.t -> +val inh_conv_coerce_rigid_to : ?loc:Loc.t -> bool -> env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) -val inh_conv_coerces_to : Loc.t -> +val inh_conv_coerces_to : ?loc:Loc.t -> env -> evar_map -> types -> types -> evar_map (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; raises [Not_found] if no coercion found *) val inh_pattern_coerce_to : - Loc.t -> env -> cases_pattern -> inductive -> inductive -> cases_pattern + ?loc:Loc.t -> env -> cases_pattern -> inductive -> inductive -> cases_pattern diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 05d6a1ad4..3079d1052 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -29,8 +29,6 @@ open Misctypes open Decl_kinds open Context.Named.Declaration -let dl = Loc.ghost - (** Should we keep details of universes during detyping ? *) let print_universes = Flags.univ_print diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4bb66b8e9..95680e18a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -888,7 +888,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else - let dloc = (Loc.ghost,Evar_kinds.InternalHole) in + let dloc = Loc.tag Evar_kinds.InternalHole in let i = Sigma.Unsafe.of_evar_map i in let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in let i' = Sigma.to_evar_map i' in @@ -1214,7 +1214,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let error_cannot_unify env evd pb ?reason t1 t2 = Pretype_errors.error_cannot_unify - ~loc:(loc_of_conv_pb evd pb) env + ?loc:(loc_of_conv_pb evd pb) env evd ?reason (t1, t2) let check_problems_are_solved env evd = diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 25ece5b8e..cba1780ba 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -22,7 +22,7 @@ let cases_predicate_names tml = | (tm,(na,None)) -> [na] | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) -let mkGApp loc p t = Loc.tag ~loc @@ +let mkGApp ?loc p t = Loc.tag ?loc @@ match snd p with | GApp (f,l) -> GApp (f,l@[t]) | _ -> GApp (p,[t]) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533..ac2118ba7 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -25,7 +25,7 @@ val cases_pattern_loc : cases_pattern -> Loc.t val cases_predicate_names : tomatch_tuples -> Name.t list (** Apply one argument to a glob_constr *) -val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr +val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5f9f4bb08..fe15cb490 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -133,7 +133,7 @@ let nf_fix sigma (nas, cs, ts) = let inj c = EConstr.to_constr sigma c in (nas, Array.map inj cs, Array.map inj ts) -let search_guard loc env possible_indexes fixdefs = +let search_guard ?loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in @@ -143,7 +143,7 @@ let search_guard loc env possible_indexes fixdefs = (try check_fix env fix with reraise -> let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in + let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in iraise (e, info)); indexes else @@ -166,7 +166,7 @@ let search_guard loc env possible_indexes fixdefs = with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in - user_err ~loc ~hdr:"search_guard" (Pp.str errmsg) + user_err ?loc ~hdr:"search_guard" (Pp.str errmsg) with Found indexes -> indexes) (* To force universe name declaration before use *) @@ -384,10 +384,10 @@ let process_inference_flags flags env initial_sigma (sigma,c) = let allow_anonymous_refs = ref false (* coerce to tycon if any *) -let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function +let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () @@ -568,18 +568,18 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* the type constraint tycon *) let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) (loc, t) = - let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in + let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in match t with | GRef (ref,u) -> - inh_conv_coerce_to_tycon loc env evdref + inh_conv_coerce_to_tycon ~loc env evdref (pretype_ref loc evdref env ref u) tycon | GVar id -> - inh_conv_coerce_to_tycon loc env evdref + inh_conv_coerce_to_tycon ~loc env evdref (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id) tycon @@ -594,7 +594,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in - inh_conv_coerce_to_tycon loc env evdref j tycon + inh_conv_coerce_to_tycon ~loc env evdref j tycon | GPatVar (someta,n) -> let env = ltac_interp_name_env k0 lvar env !evdref in @@ -674,7 +674,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; + Typing.check_type_fixpoint ~loc env.ExtraEnv.env evdref names ftys vdefj; let nf c = nf_evar !evdref c in let ftys = Array.map nf ftys in (** FIXME *) let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in @@ -696,7 +696,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) + ~loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> @@ -709,11 +709,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon loc env evdref fixj tycon + inh_conv_coerce_to_tycon ~loc env evdref fixj tycon | GSort s -> let j = pretype_sort loc evdref s in - inh_conv_coerce_to_tycon loc env evdref j tycon + inh_conv_coerce_to_tycon ~loc env evdref j tycon | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in @@ -792,7 +792,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else resj | _ -> resj in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ~loc env evdref resj tycon | GLambda(name,bk,c1,c2) -> let tycon' = evd_comb1 @@ -800,7 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod ~loc env.ExtraEnv.env evd ty in evd, Some ty') evdref tycon in @@ -814,7 +814,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ~loc env evdref resj tycon | GProd(name,bk,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in @@ -838,7 +838,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (e, info) = CErrors.push e in let info = Loc.add_loc info loc in iraise (e, info) in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ~loc env evdref resj tycon | GLetIn(name,c1,t,c2) -> let tycon1 = @@ -1020,10 +1020,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in - inh_conv_coerce_to_tycon loc env evdref cj tycon + inh_conv_coerce_to_tycon ~loc env evdref cj tycon | GCases (sty,po,tml,eqns) -> - Cases.compile_cases loc sty + Cases.compile_cases ~loc sty ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref) tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) @@ -1032,7 +1032,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match k with | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj + evd_comb1 (Coercion.inh_coerce_to_base ~loc env.ExtraEnv.env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in @@ -1067,7 +1067,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } - in inh_conv_coerce_to_tycon loc env evdref cj tycon + in inh_conv_coerce_to_tycon ~loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = @@ -1128,7 +1128,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | c -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort ~loc env.ExtraEnv.env) evdref j in match valcon with | None -> tj | Some v -> diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f13c10b05..79fafcf1a 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -24,7 +24,7 @@ open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - Loc.t -> env -> int list list -> rec_declaration -> int array + ?loc:Loc.t -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c2a030bcd..41d994553 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -152,13 +152,13 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } -let check_type_fixpoint loc env evdref lna lar vdefj = +let check_type_fixpoint ?loc env evdref lna lar vdefj = let lt = Array.length vdefj in if Int.equal (Array.length lar) lt then for i = 0 to lt-1 do if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body ~loc env !evdref + error_ill_typed_rec_body ?loc env !evdref i lna vdefj lar done @@ -361,7 +361,7 @@ and execute_recdef env evdref (names,lar,vdef) = let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in - let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in + let _ = check_type_fixpoint env1 evdref names lara vdefj in (names,lara,vdefv) and execute_array env evdref = Array.map (execute env evdref) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 91134b499..1f3ba34e5 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -44,7 +44,7 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> (** Raise an error message if bodies have types not unifiable with the expected ones *) -val check_type_fixpoint : Loc.t -> env -> evar_map ref -> +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref -> Names.Name.t array -> types array -> unsafe_judgment array -> unit val judge_of_prop : unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 532cc8baa..9678e3a42 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1250,7 +1250,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = let sigma = Sigma.to_evar_map evd in match EConstr.kind sigma (whd_all env sigma cty) with | Prod (_,c1,c2) -> - let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in + let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' | _ -> error "Apply_Head_Then" in @@ -1265,7 +1265,7 @@ let is_mimick_head sigma ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in + let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in (evd',j'.uj_val) |