diff options
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r-- | pretyping/pretyping.ml | 112 |
1 files changed, 56 insertions, 56 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index fe15cb490..a256eaa5d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -216,8 +216,8 @@ let interp_universe_level_name evd (loc,s) = evd, snd (Idmap.find id names) with Not_found -> if not (is_strict_universe_declarations ()) then - new_univ_level_variable ~loc ~name:s univ_rigid evd - else user_err ~loc ~hdr:"interp_universe_level_name" + new_univ_level_variable ?loc ~name:s univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function @@ -229,8 +229,8 @@ let interp_universe ?loc evd = function (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l -let interp_level_info loc evd : Misctypes.level_info -> _ = function - | None -> new_univ_level_variable ~loc univ_rigid evd +let interp_level_info ?loc evd : Misctypes.level_info -> _ = function + | None -> new_univ_level_variable ?loc univ_rigid evd | Some (loc,s) -> interp_universe_level_name evd (loc,s) let interp_sort ?loc evd = function @@ -337,7 +337,7 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> - error_unsolvable_implicit ~loc env current_sigma evk None) pending + error_unsolvable_implicit ?loc env current_sigma evk None) pending (* [check_evars] fails if some unresolved evar remains *) @@ -349,7 +349,7 @@ let check_evars env initial_sigma sigma c = let (loc,k) = evar_source evk sigma in begin match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None + | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None end | _ -> EConstr.iter sigma proc_rec c in proc_rec c @@ -393,9 +393,9 @@ let check_instance loc subst = function | [] -> () | (id,_) :: _ -> if List.mem_assoc id subst then - user_err ~loc (pr_id id ++ str "appears more than once.") + user_err ?loc (pr_id id ++ str "appears more than once.") else - user_err ~loc (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") + user_err ?loc (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -475,7 +475,7 @@ let pretype_id pretype k0 loc env evdref lvar id = (* and build a nice error message *) if Id.Map.mem id lvar.ltac_genargs then begin let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in - user_err ~loc + user_err ?loc (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ bound to a " ++ Geninterp.Val.pr typ ++ str ".") end; @@ -484,47 +484,47 @@ let pretype_id pretype k0 loc env evdref lvar id = { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) - error_var_not_found ~loc id + error_var_not_found ?loc id (*************************************************************************) (* Main pretyping function *) -let interp_glob_level loc evd : Misctypes.glob_level -> _ = function +let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set - | GType s -> interp_level_info loc evd s + | GType s -> interp_level_info ?loc evd s -let interp_instance loc evd ~len l = +let interp_instance ?loc evd ~len l = if len != List.length l then - user_err ~loc ~hdr:"pretype" + user_err ?loc ~hdr:"pretype" (str "Universe instance should have length " ++ int len) else let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_glob_level loc evd l in + let evd, l = interp_glob_level ?loc evd l in (evd, l :: univs)) (evd, []) l in if List.exists (fun l -> Univ.Level.is_prop l) l' then - user_err ~loc ~hdr:"pretype" + user_err ?loc ~hdr:"pretype" (str "Universe instances cannot contain Prop, polymorphic" ++ str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) -let pretype_global loc rigid env evd gr us = +let pretype_global ?loc rigid env evd gr us = let evd, instance = match us with | None -> evd, None | Some l -> let _, ctx = Universes.unsafe_constr_of_global gr in let len = Univ.UContext.size ctx in - interp_instance loc evd ~len l + interp_instance ?loc evd ~len l in - let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in + let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in (sigma, EConstr.of_constr c) -let pretype_ref loc evdref env ref us = +let pretype_ref ?loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) @@ -533,15 +533,15 @@ let pretype_ref loc evdref env ref us = (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal variables *) - Pretype_errors.error_var_not_found ~loc id) + Pretype_errors.error_var_not_found ?loc id) | ref -> - let evd, c = pretype_global loc univ_flexible env !evdref ref us in + let evd, c = pretype_global ?loc univ_flexible env !evdref ref us in let () = evdref := evd in let ty = unsafe_type_of env.ExtraEnv.env evd c in make_judge c ty let judge_of_Type loc evd s = - let evd, s = interp_universe ~loc evd s in + let evd, s = interp_universe ?loc evd s in let judge = { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } in @@ -574,12 +574,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let open Context.Rel.Declaration in match t with | GRef (ref,u) -> - inh_conv_coerce_to_tycon ~loc env evdref - (pretype_ref loc evdref env ref u) + 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 @@ -589,12 +589,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let evk = try Evd.evar_key id !evdref with Not_found -> - user_err ~loc (str "Unknown existential variable.") in + user_err ?loc (str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in 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 -> @@ -705,15 +705,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls) with reraise -> let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in + let info = Option.cata (Loc.add_loc info) info loc in 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 @@ -775,7 +775,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional - ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref + ?loc:(Loc.merge_opt floc argloc) env.ExtraEnv.env !evdref resj [|hj|] in let resj = apply_rec env 1 fj candargs args 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,11 +800,11 @@ 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 - let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon ?loc env.ExtraEnv.env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So @@ -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 @@ -836,9 +836,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre judge_of_product env.ExtraEnv.env name j j' with TypeError _ as e -> let (e, info) = CErrors.push e in - let info = Loc.add_loc info loc in + let info = Option.cata (Loc.add_loc info) 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 = @@ -867,15 +867,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj + error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then - user_err ~loc (str "Destructing let is only for inductive types" ++ + user_err ?loc (str "Destructing let is only for inductive types" ++ str " with one constructor."); let cs = cstrs.(0) in if not (Int.equal (List.length nal) cs.cs_nargs) then - user_err ~loc:loc (str "Destructing let on this type expects " ++ + user_err ?loc:loc (str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in @@ -944,7 +944,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type ~loc env.ExtraEnv.env !evdref + error_cant_find_case_type ?loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in @@ -960,10 +960,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in + error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then - user_err ~loc + user_err ?loc (str "If is only for inductive types with two constructors."); let arsgn = @@ -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 @@ -1048,9 +1048,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval + error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) - else user_err ~loc (str "Cannot check cast with vm: " ++ + else user_err ?loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in @@ -1059,7 +1059,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval + error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> @@ -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) = @@ -1087,7 +1087,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let t' = env |> lookup_named id |> NamedDecl.get_type in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> - user_err ~loc (str "Cannot interpret " ++ + user_err ?loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ str " in current context: no binding for " ++ pr_id id ++ str ".") in ((id,c)::subst, update) in @@ -1128,14 +1128,14 @@ 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 -> if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type - ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in |