diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-17 17:43:37 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-17 17:43:37 +0200 |
commit | b0cf6c4042ed8e91c6f7081a6f0c4b83ec9407c2 (patch) | |
tree | 7f0cd1ed2217f826c0d64f6a0fa700f506dd8e86 /pretyping | |
parent | 78c8d75e38844cb88c551881112e10728962dc2d (diff) | |
parent | 9f175bbeb19175a1e422225986f139e8f1a1b56c (diff) |
Merge PR #7359: Reduce usage of evar_map references
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 57 | ||||
-rw-r--r-- | pretyping/coercion.ml | 44 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 23 | ||||
-rw-r--r-- | pretyping/evarconv.mli | 8 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 27 | ||||
-rw-r--r-- | pretyping/program.ml | 4 | ||||
-rw-r--r-- | pretyping/typing.ml | 397 | ||||
-rw-r--r-- | pretyping/typing.mli | 11 | ||||
-rw-r--r-- | pretyping/unification.ml | 4 |
9 files changed, 318 insertions, 257 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4c87b4e7e..ee7c39982 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -295,8 +295,11 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = e_new_evar env evdref ~src:(hole_source n) ty' in - (e::subst,e::evarl,n+1) + let e = evd_comb1 + (Evarutil.new_evar env ~src:(hole_source n)) + evdref ty' + in + (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in (substl subst b::subst,evarl,n+1)) @@ -314,13 +317,15 @@ let try_find_ind env sigma typ realnames = IsInd (typ,ind,names) let inh_coerce_to_ind evdref env loc ty tyi = - let sigma = !evdref in + let orig = !evdref in let expected_typ = inductive_template evdref env loc tyi in (* Try to refine the type with inductive information coming from the constructor and renounce if not able to give more information *) (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) - if not (e_cumul env evdref expected_typ ty) then evdref := sigma + match cumul env !evdref expected_typ ty with + | Some sigma -> evdref := sigma + | None -> evdref := orig let binding_vars_of_inductive sigma = function | NotInd _ -> [] @@ -372,8 +377,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref !lvar tomatch in - let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in - evdref := evd; + let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in let typ = nf_evar !evdref j.uj_type in lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = @@ -396,12 +400,8 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = (* Utils *) 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 = - let (evd',y) = f !evdref x y in - evdref := evd'; - y + let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in + e let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the @@ -424,7 +424,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let current = if List.is_empty deps && isEvar !(pb.evdref) typ then (* Don't insert coercions if dependent; only solve evars *) - let _ = e_cumul pb.env pb.evdref indt typ in + let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in current else (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) @@ -1014,8 +1014,8 @@ let adjust_impossible_cases pb pred tomatch submat = begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin - let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk default.uj_type evd + let default = evd_comb0 use_unit_judge pb.evdref in + pb.evdref := Evd.define evk default.uj_type !(pb.evdref) end; add_assert_false_case pb tomatch | _ -> @@ -1681,7 +1681,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev' = e_new_evar env evdref ~src ty in + let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1712,7 +1712,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in + let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in lift k ev in aux (0,extenv,subst0) t0 @@ -1724,17 +1724,20 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = we are in an impossible branch *) 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.tag ?loc Evar_kinds.ImpossibleCase) in - (lift (n'-n) impossible_case_type, mkSort u) + let impossible_case_type, u = + evd_comb1 + (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)) + evdref univ_flexible_alg + 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 evd,tt = Typing.type_of extenv !evdref t in - evdref := evd; + let tt = evd_comb1 (Typing.type_of extenv) evdref t in (t,tt) in - let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type."); - { uj_val = t; uj_type = tt } + match cumul env !evdref tt (mkSort s) with + | None -> anomaly (Pp.str "Build_tycon: should be a type."); + | Some sigma -> evdref := sigma; + { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return @@ -1923,9 +1926,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in - evdref := evd'; - j + evd_comb2 (Coercion.inh_conv_coerce_to ?loc true env) evdref j p | None -> j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6dc3687a0..c9c2445a7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -48,31 +48,35 @@ exception NoCoercion exception NoCoercionNoUnifier of evar_map * unification_error (* Here, funj is a coercion therefore already typed in global context *) -let apply_coercion_args env evd check isproj argl funj = - let evdref = ref evd in - let rec apply_rec acc typ = function +let apply_coercion_args env sigma check isproj argl funj = + let rec apply_rec sigma acc typ = function | [] -> if isproj then - let cst = fst (destConst !evdref (j_val funj)) in + let cst = fst (destConst sigma (j_val funj)) in let p = Projection.make cst false in let pb = lookup_projection p env in let args = List.skipn pb.Declarations.proj_npars argl in let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in - { uj_val = applist (mkProj (p, hd), tl); - uj_type = typ } + sigma, { uj_val = applist (mkProj (p, hd), tl); + uj_type = typ } else - { uj_val = applist (j_val funj,argl); - uj_type = typ } + sigma, { uj_val = applist (j_val funj,argl); + uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) - match EConstr.kind !evdref (whd_all env !evdref typ) with + match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> - if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then - raise NoCoercion; - apply_rec (h::acc) (subst1 h c2) restl + let sigma = + if check then + begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with + | None -> raise NoCoercion + | Some sigma -> sigma + end + else sigma + in + apply_rec sigma (h::acc) (subst1 h c2) restl | _ -> anomaly (Pp.str "apply_coercion_args.") in - let res = apply_rec [] funj.uj_type argl in - !evdref, res + apply_rec sigma [] funj.uj_type argl (* appliquer le chemin de coercions de patterns p *) let apply_pattern_coercion ?loc pat p = @@ -94,7 +98,9 @@ open Program let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in - Evarutil.e_new_evar env evdref ~src c + let evd, v = Evarutil.new_evar env !evdref ~src c in + evdref := evd; + v let app_opt env evdref f t = whd_betaiota !evdref (app_opt f t) @@ -191,7 +197,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - Typing.e_solve_evars env evdref term) + let sigma, term = Typing.solve_evars env !evdref term in + evdref := sigma; term) in if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) @@ -337,8 +344,9 @@ let app_coercion env evdref coercion v = match coercion with | None -> v | Some f -> - let v' = Typing.e_solve_evars env evdref (f v) in - whd_betaiota !evdref v' + let sigma, v' = Typing.solve_evars env !evdref (f v) in + evdref := sigma; + whd_betaiota !evdref v' let coerce_itf ?loc env evd v t c1 = let evdref = ref evd in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 144166a34..49c429458 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1159,17 +1159,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let subst = make_subst (ctxt,Array.to_list args,argoccs) in - let evdref = ref evd in - let rhs = set_holes evdref rhs subst in - let evd = !evdref in + let evd, rhs = + let evdref = ref evd in + let rhs = set_holes evdref rhs subst in + !evdref, rhs + in (* We instantiate the evars of which the value is forced by typing *) let evd,rhs = - let evdref = ref evd in - try let c = !solve_evars env_evar evdref rhs in !evdref,c + try !solve_evars env_evar evd rhs with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise (TypingFailed !evdref) in + raise (TypingFailed evd) in let rec abstract_free_holes evd = function | (id,idty,c,_,evsref,_,_)::l -> @@ -1394,6 +1395,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) +let make_opt = function + | Success evd -> Some evd + | UnifFailure _ -> None + +let conv env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CONV t1 t2) + +let cumul env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CUMUL t1 t2) + let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CONV t1 t2 with | Success evd' -> evdref := evd'; true diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9270d6e3a..cdf5dd0e5 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -28,7 +28,13 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma (** The same function resolving evars by side-effect and catching the exception *) val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.conv]"] + val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.cumul]"] + +val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option (** {6 Unification heuristics. } *) @@ -63,7 +69,7 @@ val second_order_matching : transparent_state -> env -> evar_map -> (** Declare function to enforce evars resolution by using typing constraints *) -val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit +val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e68a25a87..35cc5702a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -674,14 +674,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in let nbfix = Array.length lar in let names = Array.map (fun id -> Name id) names in - let _ = + let () = match tycon with | Some t -> let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env.ExtraEnv.env evdref ftys.(fixi) t - | None -> true + in + begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with + | None -> () + | Some sigma -> evdref := sigma + end + | None -> () in (* Note: bodies are not used by push_rec_types, so [||] is safe *) let newenv = push_rec_types !evdref (names,ftys,[||]) env in @@ -698,7 +702,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; + evdref := 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 @@ -793,9 +797,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env.ExtraEnv.env evdref (j_val hj) arg then - args, nf_evar !evdref (j_val hj) - else [], j_val hj + begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with + | Some sigma -> evdref := sigma; + args, nf_evar !evdref (j_val hj) + | None -> + [], j_val hj + end in let ujval = adjust_evar_source evdref na ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in @@ -1166,10 +1173,12 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj - else + begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with + | Some sigma -> evdref := sigma; tj + | None -> error_unexpected_type ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + end let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in diff --git a/pretyping/program.ml b/pretyping/program.ml index 52d940d8e..8cfb7966c 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -16,7 +16,9 @@ let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = let open EConstr in let gr = delayed_force r in - mkApp (Evarutil.e_new_global evdref gr, args) + let evd, hd = Evarutil.new_global !evdref gr in + evdref := evd; + mkApp (hd, args) let sig_typ = init_reference ["Init"; "Specif"] "sig" let sig_intro = init_reference ["Init"; "Specif"] "exist" diff --git a/pretyping/typing.ml b/pretyping/typing.ml index aaec73f04..6bd75c93d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -37,104 +37,115 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl = let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp -let e_type_judgment env evdref j = - match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s } +let type_judgment env sigma j = + match EConstr.kind sigma (whd_all env sigma j.uj_type) with + | Sort s -> sigma, {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | Evar ev -> - let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in - evdref := evd; { utj_val = j.uj_val; utj_type = s } - | _ -> error_not_a_type env !evdref j - -let e_assumption_of_judgment env evdref j = - try (e_type_judgment env evdref j).utj_val + let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in + sigma, { utj_val = j.uj_val; utj_type = s } + | _ -> error_not_a_type env sigma j + +let assumption_of_judgment env sigma j = + try + let sigma, j = type_judgment env sigma j in + sigma, j.utj_val with Type_errors.TypeError _ | PretypeError _ -> - error_assumption env !evdref j + error_assumption env sigma j -let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv = - let rec apply_rec n typ = function +let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = + let rec apply_rec sigma n typ = function | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = - let ar = inductive_type_knowing_parameters env !evdref ind argjv in - hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) } + sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = + let ar = inductive_type_knowing_parameters env sigma ind argjv in + hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) } | hj::restjl -> - let (c1,c2) = - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> (c1,c2) + let sigma, (c1,c2) = + match EConstr.kind sigma (whd_all env sigma typ) with + | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,c1,c2) = destProd evd' t in - (c1,c2) + let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (_,c1,c2) = destProd sigma t in + sigma, (c1,c2) | _ -> - error_cant_apply_not_functional env !evdref funj argjv + error_cant_apply_not_functional env sigma funj argjv in - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + begin match Evarconv.cumul env sigma hj.uj_type c1 with + | Some sigma -> + apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl + | None -> + error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv + end in - apply_rec 1 funj.uj_type (Array.to_list argjv) + apply_rec sigma 1 funj.uj_type (Array.to_list argjv) -let e_judge_of_apply env evdref funj argjv = - let rec apply_rec n typ = function +let judge_of_apply env sigma funj argjv = + let rec apply_rec sigma n typ = function | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } + sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = typ } | hj::restjl -> - let (c1,c2) = - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> (c1,c2) + let sigma, (c1,c2) = + match EConstr.kind sigma (whd_all env sigma typ) with + | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,c1,c2) = destProd evd' t in - (c1,c2) + let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (_,c1,c2) = destProd sigma t in + sigma, (c1,c2) | _ -> - error_cant_apply_not_functional env !evdref funj argjv + error_cant_apply_not_functional env sigma funj argjv in - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + begin match Evarconv.cumul env sigma hj.uj_type c1 with + | Some sigma -> + apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl + | None -> + error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv + end in - apply_rec 1 funj.uj_type (Array.to_list argjv) + apply_rec sigma 1 funj.uj_type (Array.to_list argjv) -let e_check_branch_types env evdref (ind,u) cj (lfj,explft) = +let check_branch_types env sigma (ind,u) cj (lfj,explft) = if not (Int.equal (Array.length lfj) (Array.length explft)) then - error_number_branches env !evdref cj (Array.length explft); - for i = 0 to Array.length explft - 1 do - if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then - error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) - done + error_number_branches env sigma cj (Array.length explft); + Array.fold_left2_i (fun i sigma lfj explft -> + match Evarconv.cumul env sigma lfj.uj_type explft with + | Some sigma -> sigma + | None -> + error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft) + sigma lfj explft let max_sort l = if Sorts.List.mem InType l then InType else if Sorts.List.mem InSet l then InSet else InProp -let e_is_correct_arity env evdref c pj ind specif params = - let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in +let is_correct_arity env sigma c pj ind specif params = + let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in - let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in - let rec srec env pt ar = - let pt' = whd_all env !evdref pt in - match EConstr.kind !evdref pt', ar with + let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in + let rec srec env sigma pt ar = + let pt' = whd_all env sigma pt in + match EConstr.kind sigma pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - if not (Evarconv.e_cumul env evdref a1 a1') then error (); - srec (push_rel (LocalAssum (na1,a1)) env) t ar' + begin match Evarconv.cumul env sigma a1 a1' with + | None -> error () + | Some sigma -> + srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar' + end | Sort s, [] -> - let s = ESorts.kind !evdref s in + let s = ESorts.kind sigma s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () + else sigma | Evar (ev,_), [] -> - let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in - evdref := Evd.define ev (mkSort s) evd + let sigma, s = Evd.fresh_sort_in_family env sigma (max_sort allowed_sorts) in + let sigma = Evd.define ev (mkSort s) sigma in + sigma | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' + srec (push_rel d env) sigma (lift 1 pt') ar' | _ -> error () in - srec env pj.uj_type (List.rev arsign) + srec env sigma pj.uj_type (List.rev arsign) let lambda_applist_assum sigma n c l = let rec app n subst t l = @@ -147,39 +158,41 @@ let lambda_applist_assum sigma n c l = | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l -let e_type_case_branches env evdref (ind,largs) pj c = +let type_case_branches env sigma (ind,largs) pj c = let specif = lookup_mind_specif env (fst ind) in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let params = List.map EConstr.Unsafe.to_constr params in - let () = e_is_correct_arity env evdref c pj ind specif params in - let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in + let sigma = is_correct_arity env sigma c pj ind specif params in + let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in - let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in - (lc, ty) + let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in + sigma, (lc, ty) -let e_judge_of_case env evdref ci pj cj lfj = +let judge_of_case env sigma ci pj cj lfj = let ((ind, u), spec) = - try find_mrectype env !evdref cj.uj_type - with Not_found -> error_case_not_inductive env !evdref cj in - let indspec = ((ind, EInstance.kind !evdref u), spec) in + try find_mrectype env sigma cj.uj_type + with Not_found -> error_case_not_inductive env sigma cj in + let indspec = ((ind, EInstance.kind sigma u), spec) in let _ = check_case_info env (fst indspec) ci in - let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in - e_check_branch_types env evdref (fst indspec) cj (lfj,bty); - { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); - uj_type = rslty } + let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in + let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in + sigma, { 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 sigma 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 - i lna vdefj lar - done + assert (Int.equal (Array.length lar) lt); + Array.fold_left2_i (fun i sigma defj ar -> + match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with + | Some sigma -> sigma + | None -> + error_ill_typed_rec_body ?loc env sigma + i lna vdefj lar) + sigma vdefj lar + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = @@ -192,17 +205,19 @@ let check_allowed_sort env sigma ind c p = error_elim_arity env sigma ind sorts c pj (Some(ksort,s,Type_errors.error_elim_explain ksort s)) -let e_judge_of_cast env evdref cj k tj = +let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then - error_actual_type_core env !evdref cj expected_type; - { uj_val = mkCast (cj.uj_val, k, expected_type); - uj_type = expected_type } - -let enrich_env env evdref = + match Evarconv.cumul env sigma cj.uj_type expected_type with + | None -> + error_actual_type_core env sigma cj expected_type; + | Some sigma -> + sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } + +let enrich_env env sigma = let penv = Environ.pre_env env in let penv' = Pre_env.({ penv with env_stratification = - { penv.env_stratification with env_universes = Evd.universes !evdref } }) in + { penv.env_stratification with env_universes = Evd.universes sigma } }) in Environ.env_of_pre_env penv' let check_fix env sigma pfix = @@ -267,165 +282,167 @@ let judge_of_letin env name defj typj j = (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) -let rec execute env evdref cstr = - let cstr = whd_evar !evdref cstr in - match EConstr.kind !evdref cstr with +let rec execute env sigma cstr = + let cstr = whd_evar sigma cstr in + match EConstr.kind sigma cstr with | Meta n -> - { uj_val = cstr; uj_type = meta_type !evdref n } + sigma, { uj_val = cstr; uj_type = meta_type sigma n } | Evar ev -> - let ty = EConstr.existential_type !evdref ev in - let jty = execute env evdref ty in - let jty = e_assumption_of_judgment env evdref jty in - { uj_val = cstr; uj_type = jty } + let ty = EConstr.existential_type sigma ev in + let sigma, jty = execute env sigma ty in + let sigma, jty = assumption_of_judgment env sigma jty in + sigma, { uj_val = cstr; uj_type = jty } | Rel n -> - judge_of_relative env n + sigma, judge_of_relative env n | Var id -> - judge_of_variable env id + sigma, judge_of_variable env id | Const (c, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) | Ind (ind, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) | Construct (cstruct, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) | Case (ci,p,c,lf) -> - let cj = execute env evdref c in - let pj = execute env evdref p in - let lfj = execute_array env evdref lf in - e_judge_of_case env evdref ci pj cj lfj + let sigma, cj = execute env sigma c in + let sigma, pj = execute env sigma p in + let sigma, lfj = execute_array env sigma lf in + judge_of_case env sigma ci pj cj lfj | Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evdref recdef in + let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in let fix = (vni,recdef') in - check_fix env !evdref fix; - make_judge (mkFix fix) tys.(i) + check_fix env sigma fix; + sigma, make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evdref recdef in + let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in let cofix = (i,recdef') in - check_cofix env !evdref cofix; - make_judge (mkCoFix cofix) tys.(i) + check_cofix env sigma cofix; + sigma, make_judge (mkCoFix cofix) tys.(i) | Sort s -> - begin match ESorts.kind !evdref s with + begin match ESorts.kind sigma s with | Prop c -> - judge_of_prop_contents c + sigma, judge_of_prop_contents c | Type u -> - judge_of_type u + sigma, judge_of_type u end | Proj (p, c) -> - let cj = execute env evdref c in - judge_of_projection env !evdref p cj + let sigma, cj = execute env sigma c in + sigma, judge_of_projection env sigma p cj | App (f,args) -> - let jl = execute_array env evdref args in - (match EConstr.kind !evdref f with + let sigma, jl = execute_array env sigma args in + (match EConstr.kind sigma f with | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> - let fj = execute env evdref f in - e_judge_of_applied_inductive_knowing_parameters env evdref fj (ind, u) jl + let sigma, fj = execute env sigma f in + judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl | _ -> (* No template polymorphism *) - let fj = execute env evdref f in - e_judge_of_apply env evdref fj jl) + let sigma, fj = execute env sigma f in + judge_of_apply env sigma fj jl) | Lambda (name,c1,c2) -> - let j = execute env evdref c1 in - let var = e_type_judgment env evdref j in + let sigma, j = execute env sigma c1 in + let sigma, var = type_judgment env sigma j in let env1 = push_rel (LocalAssum (name, var.utj_val)) env in - let j' = execute env1 evdref c2 in - judge_of_abstraction env1 name var j' + let sigma, j' = execute env1 sigma c2 in + sigma, judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> - let j = execute env evdref c1 in - let varj = e_type_judgment env evdref j in + let sigma, j = execute env sigma c1 in + let sigma, varj = type_judgment env sigma j in let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in - let j' = execute env1 evdref c2 in - let varj' = e_type_judgment env1 evdref j' in - judge_of_product env name varj varj' + let sigma, j' = execute env1 sigma c2 in + let sigma, varj' = type_judgment env1 sigma j' in + sigma, judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> - let j1 = execute env evdref c1 in - let j2 = execute env evdref c2 in - let j2 = e_type_judgment env evdref j2 in - let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in + let sigma, j1 = execute env sigma c1 in + let sigma, j2 = execute env sigma c2 in + let sigma, j2 = type_judgment env sigma j2 in + let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in - let j3 = execute env1 evdref c3 in - judge_of_letin env name j1 j2 j3 + let sigma, j3 = execute env1 sigma c3 in + sigma, judge_of_letin env name j1 j2 j3 | Cast (c,k,t) -> - let cj = execute env evdref c in - let tj = execute env evdref t in - let tj = e_type_judgment env evdref tj in - e_judge_of_cast env evdref cj k tj - -and execute_recdef env evdref (names,lar,vdef) = - let larj = execute_array env evdref lar in - let lara = Array.map (e_assumption_of_judgment env evdref) larj in + let sigma, cj = execute env sigma c in + let sigma, tj = execute env sigma t in + let sigma, tj = type_judgment env sigma tj in + judge_of_cast env sigma cj k tj + +and execute_recdef env sigma (names,lar,vdef) = + let sigma, larj = execute_array env sigma lar in + let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 evdref vdef in + let sigma, vdefj = execute_array env1 sigma vdef in let vdefv = Array.map j_val vdefj in - let _ = check_type_fixpoint env1 evdref names lara vdefj in - (names,lara,vdefv) + let sigma = check_type_fixpoint env1 sigma names lara vdefj in + sigma, (names,lara,vdefv) -and execute_array env evdref = Array.map (execute env evdref) +and execute_array env = Array.fold_left_map (execute env) + +let check env sigma c t = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + match Evarconv.cumul env sigma j.uj_type t with + | None -> + error_actual_type_core env sigma j t + | Some sigma -> sigma let e_check env evdref c t = - let env = enrich_env env evdref in - let j = execute env evdref c in - if not (Evarconv.e_cumul env evdref j.uj_type t) then - error_actual_type_core env !evdref j t + evdref := check env !evdref c t (* Type of a constr *) -let unsafe_type_of env evd c = - let evdref = ref evd in - let env = enrich_env env evdref in - let j = execute env evdref c in - j.uj_type +let unsafe_type_of env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + j.uj_type (* Sort of a type *) +let sort_of env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + let sigma, a = type_judgment env sigma j in + sigma, a.utj_type + let e_sort_of env evdref c = - let env = enrich_env env evdref in - let j = execute env evdref c in - let a = e_type_judgment env evdref j in - a.utj_type + Evarutil.evd_comb1 (sort_of env) evdref c (* Try to solve the existential variables by typing *) -let type_of ?(refresh=false) env evd c = - let evdref = ref evd in - let env = enrich_env env evdref in - let j = execute env evdref c in +let type_of ?(refresh=false) env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type - else !evdref, j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type + else sigma, j.uj_type + +let e_type_of ?refresh env evdref c = + Evarutil.evd_comb1 (type_of ?refresh env) evdref c -let e_type_of ?(refresh=false) env evdref c = - let env = enrich_env env evdref in - let j = execute env evdref c in +let solve_evars env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in (* side-effect on evdref *) - if refresh then - let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in - let () = evdref := evd in - c - else j.uj_type + sigma, nf_evar sigma j.uj_val let e_solve_evars env evdref c = - let env = enrich_env env evdref in - let c = (execute env evdref c).uj_val in - (* side-effect on evdref *) - nf_evar !evdref c + Evarutil.evd_comb1 (solve_evars env) evdref c -let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c) +let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 4905adf1f..3cf43ace0 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -26,18 +26,25 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Variant of [type_of] using references instead of state-passing. *) val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types +[@@ocaml.deprecated "Use [Typing.type_of]"] (** Typecheck a type and return its sort *) +val sort_of : env -> evar_map -> types -> evar_map * Sorts.t val e_sort_of : env -> evar_map ref -> types -> Sorts.t +[@@ocaml.deprecated "Use [Typing.sort_of]"] (** Typecheck a term has a given type (assuming the type is OK) *) +val check : env -> evar_map -> constr -> types -> evar_map val e_check : env -> evar_map ref -> constr -> types -> unit +[@@ocaml.deprecated "Use [Typing.check]"] (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) +val solve_evars : env -> evar_map -> constr -> evar_map * constr val e_solve_evars : env -> evar_map ref -> constr -> constr +[@@ocaml.deprecated "Use [Typing.solve_evars]"] (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) @@ -46,8 +53,8 @@ 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:Loc.t -> env -> evar_map ref -> - Names.Name.t array -> types array -> unsafe_judgment array -> unit +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> + Names.Name.t array -> types array -> unsafe_judgment array -> evar_map val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d98ce9aba..1caa629ff 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -198,8 +198,8 @@ let pose_all_metas_as_evars env evd t = then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in - let ev = Evarutil.e_new_evar env evdref ~src ty in - evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; + let evd, ev = Evarutil.new_evar env !evdref ~src ty in + evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd; ev) | _ -> EConstr.map !evdref aux t in |