diff options
Diffstat (limited to 'pretyping')
60 files changed, 1357 insertions, 1083 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 84295959f..9d4badc60 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -26,7 +26,7 @@ let name_table = type req = | ReqLocal - | ReqGlobal of global_reference * Name.t list + | ReqGlobal of GlobRef.t * Name.t list let load_rename_args _ (_, (_, (r, names))) = name_table := Refmap.add r names !name_table diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 65e3c3be5..6a776dc96 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -9,14 +9,13 @@ (************************************************************************) open Names -open Globnames open Environ open Constr -val rename_arguments : bool -> global_reference -> Name.t list -> unit +val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit (** [Not_found] is raised if no names are defined for [r] *) -val arguments_names : global_reference -> Name.t list +val arguments_names : GlobRef.t -> Name.t list val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a48889c6c..6e1d3e551 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) @@ -574,7 +574,7 @@ let dependent_decl sigma a = let rec dep_in_tomatch sigma n = function | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l - | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l + | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l | [] -> false let dependencies_in_rhs sigma nargs current tms eqns = @@ -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 (EConstr.Unsafe.to_constr 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 | _ -> @@ -1663,7 +1663,7 @@ let rec list_assoc_in_triple x = function let abstract_tycon ?loc env evdref subst tycon extenv t = let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with - | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) + | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,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 @@ -1682,7 +1682,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 @@ -1705,15 +1705,17 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = List.map_i (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 (rel_context extenv) in - let rel_filter = - List.map (fun a -> not (isRel !evdref a) || dependent !evdref a u - || Int.Set.mem (destRel !evdref a) depvl) inst in + let map a = match EConstr.kind !evdref a with + | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl + | _ -> true + in + let rel_filter = List.map map inst in let named_filter = List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u) (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 @@ -1725,17 +1727,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 @@ -1846,7 +1851,7 @@ let build_inversion_problem loc env sigma tms t = (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) let s' = Retyping.get_sort_of env sigma t in - let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in + let sigma, s = Evd.new_sort_variable univ_flexible sigma in let sigma = Evd.set_leq_sort env sigma s' s in let evdref = ref sigma in let pb = @@ -1924,9 +1929,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. *) @@ -1937,8 +1940,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in match EConstr.kind sigma tm with - | Rel n when dependent sigma tm c - && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> + | Rel n when Int.equal signlen 1 && not (noccurn sigma n c) + (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> @@ -1949,13 +1952,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_left (fun (subst, len) arg -> match EConstr.kind sigma arg with - | Rel n when dependent sigma arg c -> + | Rel n when not (noccurn sigma n c) -> ((n, len) :: subst, pred len) | _ -> (subst, pred len)) (subst, len) realargs in let subst = - if dependent sigma tm c && List.for_all (isRel sigma) realargs + if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs then (n, len) :: subst else subst in (subst, pred len)) | _ -> (subst, len - signlen)) @@ -2101,7 +2104,7 @@ let mk_JMeq_refl evdref typ x = let hole na = DAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), - Misctypes.IntroAnonymous, None) + IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = @@ -2582,7 +2585,8 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); } + (* XXX: is this normalization needed? *) + uj_type = Evarutil.nf_evar !evdref tycon; } in j (**************************************************************************) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index a2155697e..cb0fc3257 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -71,7 +71,7 @@ and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of projection * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack (* les vars pourraient etre des constr, cela permet de retarder les lift: utile ?? *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 2ac59911c..cdaa39c53 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -41,7 +41,7 @@ and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of projection * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack val shift_value : int -> cbv_value -> cbv_value diff --git a/pretyping/classops.ml b/pretyping/classops.ml index a0804b72b..7dbef01c2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -37,7 +37,7 @@ type cl_info_typ = { cl_param : int } -type coe_typ = global_reference +type coe_typ = GlobRef.t module CoeTypMap = Refmap_env @@ -316,7 +316,7 @@ let lookup_pattern_path_between env (s,t) = let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; coe_is_identity = b; coe_is_projection = b' } = - let subst, ctx = Universes.fresh_universe_context_set_instance ctx in + let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c and t' = Vars.subst_univs_level_constr subst t in (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx @@ -440,7 +440,7 @@ let cache_coercion env sigma (_, c) = let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = diff --git a/pretyping/classops.mli b/pretyping/classops.mli index f8600bbe0..35691ea37 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -36,7 +36,7 @@ type cl_info_typ = { cl_param : int } (** This is the type of coercion kinds *) -type coe_typ = Globnames.global_reference +type coe_typ = GlobRef.t (** This is the type of infos for declared coercions *) type coe_info_typ diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 04cb6a59f..bf9e37aa7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -20,6 +20,7 @@ open CErrors open Util open Names open Term +open Constr open Environ open EConstr open Vars @@ -48,31 +49,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 +99,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 +198,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. *) @@ -251,7 +259,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let (n, dom, rng) = destLambda !evdref t in if isEvar !evdref dom then let (domk, args) = destEvar !evdref dom in - evdref := define domk (EConstr.Unsafe.to_constr a) !evdref; + evdref := define domk a !evdref; else (); t, rng | _ -> raise NoSubtacCoercion @@ -337,8 +345,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/constr_matching.ml b/pretyping/constr_matching.ml index 888c76e3d..2bc603a90 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -13,6 +13,7 @@ open Pp open CErrors open Util open Names +open Constr open Globnames open Termops open Term @@ -20,7 +21,6 @@ open EConstr open Vars open Pattern open Patternops -open Misctypes open Context.Rel.Declaration open Ltac_pretype (*i*) @@ -59,7 +59,7 @@ let warn_meta_collision = strbrk " and a metavariable of same name.") -let constrain sigma n (ids, m) (names, terms as subst) = +let constrain sigma n (ids, m) ((names,seen as names_seen), terms as subst) = let open EConstr in try let (ids', m') = Id.Map.find n terms in @@ -67,19 +67,21 @@ let constrain sigma n (ids, m) (names, terms as subst) = else raise PatternMatchingFailure with Not_found -> let () = if Id.Map.mem n names then warn_meta_collision n in - (names, Id.Map.add n (ids, m) terms) + (names_seen, Id.Map.add n (ids, m) terms) -let add_binders na1 na2 binding_vars (names, terms as subst) = +let add_binders na1 na2 binding_vars ((names,seen), terms as subst) = match na1, na2 with | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> if Id.Map.mem id1 names then let () = Glob_ops.warn_variable_collision id1 in - (names, terms) + subst else + let id2 = Namegen.next_ident_away id2 seen in let names = Id.Map.add id1 id2 names in + let seen = Id.Set.add id2 seen in let () = if Id.Map.mem id1 terms then warn_meta_collision id1 in - (names, terms) + ((names,seen), terms) | _ -> subst let rec build_lambda sigma vars ctx m = match vars with @@ -183,9 +185,36 @@ let push_binder na1 na2 t ctx = Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in (na1, id2, t) :: ctx -let to_fix (idx, (nas, cs, ts)) = - let inj = EConstr.of_constr in - (idx, (nas, Array.map inj cs, Array.map inj ts)) +(* This is an optimization of the main pattern-matching which shares + the longest common prefix of the body and type of a fixpoint. The + only practical effect at the time of writing is in binding variable + names: these variable names must be bound only once since the user + view at a fix displays only a (maximal) shared common prefix *) + +let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 = + match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with + | PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') -> + let ctx = push_binder na1 na2 c2 ctx in + let ctx' = push_binder na1 na2' c2' ctx' in + let env = EConstr.push_rel (LocalAssum (na2,c2)) env in + let subst = sorec ctx env subst c1 c2 in + let subst = sorec ctx env subst c1' c2' in + let subst = add_binders na1 na2 binding_vars subst in + match_under_common_fix_binders sorec sigma binding_vars + ctx ctx' env env' subst t1' t2' b1' b2' + | PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) -> + let ctx = push_binder na1 na2 u2 ctx in + let ctx' = push_binder na1 na2' u2' ctx' in + let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in + let subst = sorec ctx env subst c1 c2 in + let subst = sorec ctx env subst c1' c2' in + let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in + let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in + let subst = add_binders na1 na2 binding_vars subst in + match_under_common_fix_binders sorec sigma binding_vars + ctx ctx' env env' subst t1 t2 b1 b2 + | _ -> + sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2 let merge_binding sigma allow_bound_rels ctx n cT subst = let c = match ctx with @@ -250,6 +279,7 @@ let matches_core env sigma allow_bound_rels | PSort ps, Sort s -> + let open Glob_term in begin match ps, ESorts.kind sigma s with | GProp, Prop Null -> subst | GSet, Prop Pos -> subst @@ -364,8 +394,20 @@ let matches_core env sigma allow_bound_rels let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in List.fold_left chk_branch chk_head br1 - | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst - | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst + | PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2)) + when Array.equal Int.equal ln1 ln2 && i1 = i2 -> + let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in + let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in + let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in + Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2 + + | PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2)) + when i1 = i2 -> + let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in + let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in + let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in + Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2 + | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> Array.fold_left2 (sorec ctx env) subst args1 args2 | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ @@ -373,13 +415,15 @@ let matches_core env sigma allow_bound_rels | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure in - sorec [] env (Id.Map.empty, Id.Map.empty) pat c + sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c let matches_core_closed env sigma pat c = let names, subst = matches_core env sigma false pat c in - (names, Id.Map.map snd subst) + (fst names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma true +let extended_matches env sigma pat c = + let (names,_), subst = matches_core env sigma true pat c in + names, subst let matches env sigma pat c = snd (matches_core_closed env sigma (Id.Set.empty,pat) c) @@ -388,7 +432,7 @@ let special_meta = (-1) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : constr; } + m_ctx : constr Lazy.t; } let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) @@ -412,7 +456,7 @@ let authorized_occ env sigma closed pat c mk_ctx = let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) - else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) + else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next) with PatternMatchingFailure -> (fun next -> next ()) let subargs env v = Array.map_to_list (fun c -> (env, c)) v diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 3c2c73915..d19789ef4 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,7 +61,7 @@ val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : EConstr.t } + m_ctx : EConstr.t Lazy.t } (** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 587892141..df89d9eac 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -14,6 +14,7 @@ open Pp open CErrors open Util open Names +open Constr open Term open EConstr open Vars @@ -26,7 +27,6 @@ open Libnames open Globnames open Nametab open Mod_subst -open Misctypes open Decl_kinds open Context.Named.Declaration open Ltac_pretype @@ -36,7 +36,7 @@ type _ delay = | Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) -let print_universes = Flags.univ_print +let print_universes = ref false (** If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false @@ -501,6 +501,97 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let rec share_names detype n l avoid env sigma c t = + match EConstr.kind sigma c, EConstr.kind sigma t with + (* factorize even when not necessary to have better presentation *) + | Lambda (na,t,c), Prod (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in + share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + (* May occur for fix built interactively *) + | LetIn (na,b,t',c), _ when n > 0 -> + let t'' = detype avoid env sigma t' in + let b' = detype avoid env sigma b in + let id = next_name_away na avoid in + let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in + share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) + (* Only if built with the f/n notation or w/o let-expansion in types *) + | _, LetIn (_,b,_,t) when n > 0 -> + share_names detype n l avoid env sigma c (subst1 b t) + (* If it is an open proof: we cheat and eta-expand *) + | _, Prod (na',t',c') when n > 0 -> + let t'' = detype avoid env sigma t' in + let id = next_name_away na' avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in + let appc = mkApp (lift 1 c,[|mkRel 1|]) in + share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' + (* If built with the f/n notation: we renounce to share names *) + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let rec share_pattern_names detype n l avoid env sigma c t = + let open Pattern in + if n = 0 then + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + else match c, t with + | PLambda (na,t,c), PProd (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid in + let env = Name id :: env in + share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let n = Array.length tys in + let v = Array.map3 + (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t)) + bodies tys vn in + GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + +let detype_cofix detype avoid env sigma n (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let ntys = Array.length tys in + let v = Array.map2 + (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t)) + bodies tys in + GRec(GCoFix n,Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + let detype_universe sigma u = let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in Univ.Universe.map fn u @@ -655,76 +746,8 @@ and detype_r d flags avoid env sigma t = (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) p c bl - | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef - | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef - -and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let n = Array.length tys in - let v = Array.map3 - (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t)) - bodies tys vn in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and detype_cofix d flags avoid env sigma n (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let ntys = Array.length tys in - let v = Array.map2 - (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t)) - bodies tys in - GRec(GCoFix n,Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and share_names d flags n l avoid env sigma c t = - match EConstr.kind sigma c, EConstr.kind sigma t with - (* factorize even when not necessary to have better presentation *) - | Lambda (na,t,c), Prod (na',t',c') -> - let na = match (na,na') with - Name _, _ -> na - | _, Name _ -> na' - | _ -> na in - let t' = detype d flags avoid env sigma t in - let id = next_name_away na avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in - share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' - (* May occur for fix built interactively *) - | LetIn (na,b,t',c), _ when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let b' = detype d flags avoid env sigma b in - let id = next_name_away na avoid in - let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in - share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) - (* Only if built with the f/n notation or w/o let-expansion in types *) - | _, LetIn (_,b,_,t) when n > 0 -> - share_names d flags n l avoid env sigma c (subst1 b t) - (* If it is an open proof: we cheat and eta-expand *) - | _, Prod (na',t',c') when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let id = next_name_away na' avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in - let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' - (* If built with the f/n notation: we renounce to share names *) - | _ -> - if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype d flags avoid env sigma c in - let t = detype d flags avoid env sigma t in - (List.rev l,c,t) + | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try @@ -897,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -906,9 +929,11 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make () let rec subst_glob_constr subst = DAst.map (function | GRef (ref,u) as raw -> - let ref',t = subst_global subst ref in - if ref' == ref then raw else - DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t)) + let ref',t = subst_global subst ref in + if ref' == ref then raw else + let env = Global.env () in + let evd = Evd.from_env env in + DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)) | GSort _ | GVar _ @@ -917,7 +942,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -934,25 +959,25 @@ let rec subst_glob_constr subst = DAst.map (function | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in - let t' = Option.smartmap (subst_glob_constr subst) t in + let t' = Option.Smart.map (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in - let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + let rtno' = Option.Smart.map (subst_glob_constr subst) rtno + and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in - let topt' = Option.smartmap + let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -962,14 +987,14 @@ let rec subst_glob_constr subst = DAst.map (function GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 and c' = subst_glob_constr subst c in @@ -977,12 +1002,12 @@ let rec subst_glob_constr subst = DAst.map (function GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> - let ra1' = Array.smartmap (subst_glob_constr subst) ra1 - and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in - let bl' = Array.smartmap - (List.smartmap (fun (na,k,obd,ty as dcl) -> + let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 + and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in + let bl' = Array.Smart.map + (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in - let obd' = Option.smartmap (subst_glob_constr subst) obd in + let obd' = Option.Smart.map (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else @@ -995,13 +1020,13 @@ let rec subst_glob_constr subst = DAst.map (function if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in + let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in - let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in + let k' = smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') | GProj (p,c) as raw -> diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 32b94e1b0..5310455fe 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -14,7 +14,6 @@ open EConstr open Glob_term open Termops open Mod_subst -open Misctypes open Evd open Ltac_pretype @@ -56,6 +55,13 @@ val detype_sort : evar_map -> Sorts.t -> glob_sort val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> evar_map -> rel_context -> 'a glob_decl_g list +val share_pattern_names : + (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int -> + (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list -> + Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> + Pattern.constr_pattern -> + (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a + val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr (** look for the index of a named var or a nondep var as it is renamed *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d37090a65..6d08f66c1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -49,7 +49,7 @@ let _ = Goptions.declare_bool_option { (* XXX: we would like to search for this with late binding "data.id.type" etc... *) let impossible_default_case () = - let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in let (_, u) = Constr.destConst c in Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) @@ -114,9 +114,6 @@ let flex_kind_of_term ts env evd c sk = | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false -let add_conv_pb (pb, env, x, y) sigma = - Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma - let apprec_nohdbeta ts env evd c = let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in if Stack.not_purely_applicative sk @@ -213,7 +210,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let u, ctx' = Universes.fresh_instance_from ctx None in + let u, ctx' = UnivGen.fresh_instance_from ctx None in let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in @@ -369,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( let e = - try - let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd term1 term2 - in - if b then Success evd - else UnifFailure (evd, ConversionFailed (env,term1,term2)) - with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) + match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with + | Some evd -> Success evd + | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)) + | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with | UnifFailure (evd, e) when not (is_ground_env evd env) -> None @@ -1045,7 +1039,7 @@ let choose_less_dependent_instance evk evd term args = let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in match subst' with | [] -> None - | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd) + | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) let apply_on_subterm env evdref f c t = let rec applyrec (env,(k,c) as acc) t = @@ -1085,7 +1079,7 @@ let filter_possible_projections evd c ty ctxt args = let a = Array.unsafe_get args i in (match decl with | NamedDecl.LocalAssum _ -> false - | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) || + | NamedDecl.LocalDef (_,c,_) -> not (isRel evd c || isVar evd c)) || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) @@ -1135,7 +1129,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = end | decl'::ctxt', c::l, occs::occsl -> let id = NamedDecl.get_id decl' in - let t = EConstr.of_constr (NamedDecl.get_type decl') in + let t = NamedDecl.get_type decl' in let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections evd c ty ctxt args in @@ -1162,17 +1156,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 -> @@ -1183,7 +1178,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* We force abstraction over this unconstrained occurrence *) (* and we use typing to propagate this instantiation *) (* This is an arbitrary choice *) - let evd = Evd.define evk (Constr.mkVar id) evd in + let evd = Evd.define evk (mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> @@ -1205,14 +1200,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (evar_conv_x full_transparent_state) with IllTypedInstance _ -> raise (TypingFailed evd) in - Evd.define evk (EConstr.Unsafe.to_constr rhs) evd + Evd.define evk rhs evd in abstract_free_holes evd subst, true with TypingFailed evd -> evd, false -let to_pb (pb, env, t1, t2) = - (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2) - let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in @@ -1222,7 +1214,7 @@ let second_order_matching_with_args ts env evd pbty ev l t = else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else *) - let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = @@ -1245,7 +1237,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> @@ -1255,7 +1247,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd @@ -1295,10 +1287,10 @@ let error_cannot_unify env evd pb ?reason t1 t2 = let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2) + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () -exception MaxUndefined of (Evar.t * evar_info * Constr.t list) +exception MaxUndefined of (Evar.t * evar_info * EConstr.t list) let max_undefined_with_candidates evd = let fold evk evi () = match evi.evar_candidates with @@ -1326,7 +1318,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | a::l -> try let conv_algo = evar_conv_x ts in - let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in + let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in match reconsider_unif_constraints conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd @@ -1348,7 +1340,7 @@ let solve_unconstrained_impossible_cases env evd = let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in let evd' = check_evar_instance evd' evk ty conv_algo in - Evd.define evk (EConstr.Unsafe.to_constr ty) evd' + Evd.define evk ty evd' | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env @@ -1357,8 +1349,6 @@ let solve_unif_constraints_with_heuristics env let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with | Success evd' -> let (evd', rest) = extract_all_conv_pbs evd' in @@ -1375,9 +1365,7 @@ let solve_unif_constraints_with_heuristics env match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in - (* There remains stuck problems *) + (* There remains stuck problems *) error_cannot_unify env evd pb t1 t2 in let (evd,pbs) = extract_all_conv_pbs evd in @@ -1404,6 +1392,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 627430708..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. } *) @@ -38,7 +44,7 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map -(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) +[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"] (** Check all pending unification problems are solved and raise an error otherwise *) @@ -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/evardefine.ml b/pretyping/evardefine.ml index 03f40ad92..b452755b1 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -19,6 +19,7 @@ open Vars open Namegen open Evd open Evarutil +open Evar_kinds open Pretype_errors module RelDecl = Context.Rel.Declaration @@ -76,14 +77,16 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in - let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in + let concl = Reductionops.whd_all evenv evd evi.evar_concl in let s = destSort evd concl in + let evksrc = evar_source evk evd in + let src = subterm_source evk ~where:Domain evksrc in let evd1,(dom,u1) = - new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) + new_type_evar evenv evd univ_flexible_alg ~src ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (LocalAssum (id, dom)) evenv in - let src = evar_source evk evd1 in + let src = subterm_source evk ~where:Codomain evksrc in let filter = Filter.extend 1 (evar_filter evi) in if Sorts.is_prop (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) @@ -98,7 +101,7 @@ let define_pure_evar_as_product evd evk = evd3, rng in let prod = mkProd (Name id, dom, subst_var id rng) in - let evd3 = Evd.define evk (EConstr.Unsafe.to_constr prod) evd2 in + let evd3 = Evd.define evk prod evd2 in evd3,prod (* Refine an applied evar to a product and returns its instantiation *) @@ -125,7 +128,7 @@ let define_pure_evar_as_lambda env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi)) in + let typ = Reductionops.whd_all evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match EConstr.kind evd typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ @@ -135,10 +138,10 @@ let define_pure_evar_as_lambda env evd evk = next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in - let src = evar_source evk evd1 in + let src = subterm_source evk ~where:Body (evar_source evk evd1) in let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in let lam = mkLambda (Name id, dom, subst_var id body) in - Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam + Evd.define evk lam evd2, lam let define_evar_as_lambda env evd (evk,args) = let evd,lam = define_pure_evar_as_lambda env evd evk in @@ -163,9 +166,9 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in - let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in + let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in let sort = destSort evd concl in - let evd' = Evd.define ev (Constr.mkSort s) evd in + let evd' = Evd.define ev (mkSort s) evd in Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s (* Propagation of constraints through application and abstraction: diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 96d80741a..8afb9b942 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -89,9 +89,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh ~onlyalg univ_flexible ~direction:true (EConstr.of_constr evi.evar_concl) in + let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in if !modified then - evdref := Evd.add !evdref ev {evi with evar_concl = EConstr.Unsafe.to_constr ty'} + evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () | _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t and refresh_polymorphic_positions args pos = @@ -137,8 +137,6 @@ let test_success conv_algo env evd c c' rhs = is_success (conv_algo env evd c c' rhs) let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = - let t1 = EConstr.Unsafe.to_constr t1 in - let t2 = EConstr.Unsafe.to_constr t2 in match pbty with | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd @@ -197,7 +195,7 @@ let restrict_evar_key evd evk filter candidates = | None -> evar_filter evi | Some filter -> filter in let candidates = match candidates with - | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates + | NoUpdate -> evi.evar_candidates | UpdateWith c -> Some c in restrict_evar evd evk filter candidates end @@ -527,7 +525,7 @@ let is_unification_pattern_meta env evd nb m l t = match Option.List.map map l with | Some l -> begin match find_unification_pattern_args env evd l t with - | Some _ as x when not (dependent evd (mkMeta m) t) -> x + | Some _ as x when not (occur_metavariable evd m t) -> x | _ -> None end | None -> @@ -600,7 +598,6 @@ let solve_pattern_eqn env sigma l c = let make_projectable_subst aliases sigma evi args = let sign = evar_filtered_context evi in - let sign = List.map (fun d -> map_named_decl EConstr.of_constr d) sign in let evar_aliases = compute_var_aliases sign sigma in let (_,full_subst,cstr_subst) = List.fold_right @@ -877,7 +874,7 @@ let choose_projection evi sols = let rec do_projection_effects define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = Evd.define evk (Constr.mkVar id) evd in + let evd = Evd.define evk (mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in let ty = whd_all env evd (Lazy.force ty) in @@ -887,7 +884,7 @@ let rec do_projection_effects define_fun env ty evd = function one (however, regarding coercions, because t is obtained by unif, we know that no coercion can be inserted) *) let subst = make_pure_subst evi argsv in - let ty' = replace_vars subst (EConstr.of_constr evi.evar_concl) in + let ty' = replace_vars subst evi.evar_concl in if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd else evd @@ -932,7 +929,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ with Not_found -> match expand_alias_once evd aliases t with | None -> raise Not_found - | Some c -> aux k c in + | Some c -> aux k (lift k c) in try let c = aux 0 c_in_env_extended_with_k_binders in Invertible (UniqueProjection (c,!effects)) @@ -1004,7 +1001,7 @@ let filter_effective_candidates evd evi filter candidates = let filter_candidates evd evk filter candidates_update = let evi = Evd.find_undefined evd evk in let candidates = match candidates_update with - | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates + | NoUpdate -> evi.evar_candidates | UpdateWith c -> Some c in match candidates with @@ -1023,13 +1020,12 @@ let closure_of_filter evd evk = function | None -> None | Some filter -> let evi = Evd.find_undefined evd evk in - let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in + let vars = collect_vars evd (evar_concl evi) in let test b decl = b || Id.Set.mem (get_id decl) vars || match decl with | LocalAssum _ -> false | LocalDef (_,c,_) -> - let c = EConstr.of_constr c in not (isRel evd c || isVar evd c) in let newfilter = Filter.map_along test filter (evar_context evi) in @@ -1062,7 +1058,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = match candidates,filter with | UpdateWith [], _ -> user_err Pp.(str "Not solvable.") | UpdateWith [nc],_ -> - let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in + let evd = Evd.define evk nc evd in raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) | NoUpdate, None -> evd,ev | _ -> restrict_applied_evar evd ev filter candidates @@ -1072,8 +1068,14 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = let rhs = expand_vars_in_term env evd rhs in - let filter = - restrict_upon_filter evd evk + let filter a = match EConstr.kind evd a with + | Rel n -> not (noccurn evd n rhs) + | Var id -> + local_occur_var evd id rhs + || List.exists (fun (id', _) -> Id.equal id id') sols + | _ -> true + in + let filter = restrict_upon_filter evd evk filter argsv in (* Keep only variables that occur in rhs *) (* This is not safe: is the variable is a local def, its body *) (* may contain references to variables that are removed, leading to *) @@ -1081,9 +1083,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = (* that says that the body is hidden. Note that expand_vars_in_term *) (* expands only rels and vars aliases, not rels or vars bound to an *) (* arbitrary complex term *) - (fun a -> not (isRel evd a || isVar evd a) - || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols) - argsv in let filter = closure_of_filter evd evk filter in let candidates = extract_candidates sols in match candidates with @@ -1113,9 +1112,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) -let instantiate_evar_array evi c args = - EConstr.of_constr (instantiate_evar_array evi (EConstr.Unsafe.to_constr c) (Array.map EConstr.Unsafe.to_constr args)) - let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in match conv_algo env evd Reduction.CONV rhs c' with @@ -1135,8 +1131,6 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = | _, None -> filter_candidates evd evk1 filter1 NoUpdate | None, Some _ -> raise DoesNotPreserveCandidateRestriction | Some l1, Some l2 -> - let l1 = List.map EConstr.of_constr l1 in - let l2 = List.map EConstr.of_constr l2 in let l1 = filter_effective_candidates evd evi1 filter1 l1 in let l1' = List.filter (fun c1 -> let c1' = instantiate_evar_array evi1 c1 argsv1 in @@ -1242,9 +1236,9 @@ let check_evar_instance evd evk1 body conv_algo = try Retyping.get_type_of ~lax:true evenv evd body with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") in - match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with + match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd - | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,EConstr.of_constr evi.evar_concl)) + | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) let update_evar_source ev1 ev2 evd = let loc, evs2 = evar_source ev2 evd in @@ -1257,7 +1251,7 @@ let update_evar_source ev1 ev2 evd = let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in - let evd' = Evd.define evk2 (EConstr.Unsafe.to_constr body) evd in + let evd' = Evd.define evk2 body evd in let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> @@ -1292,17 +1286,19 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let pbty = if force then None else pbty in let evi = Evd.find evd evk1 in - let downcast evk t evd = downcast evk (EConstr.Unsafe.to_constr t) evd in + let downcast evk t evd = downcast evk t evd in let evd = try (* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j. The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *) let evienv = Evd.evar_env evi in - let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in + let concl1 = EConstr.Unsafe.to_constr evi.evar_concl in + let ctx1, i = Reduction.dest_arity evienv concl1 in let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in let evi2 = Evd.find evd evk2 in let evi2env = Evd.evar_env evi2 in - let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in + let concl2 = EConstr.Unsafe.to_constr evi2.evar_concl in + let ctx2, j = Reduction.dest_arity evi2env concl2 in let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in let ui, uj = univ_of_sort i, univ_of_sort j in if i == j || Evd.check_eq evd ui uj @@ -1375,14 +1371,14 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = | Some l -> let l' = List.map_filter - (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs (EConstr.of_constr c)) l in + (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs c) l in match l' with | [] -> raise IncompatibleCandidates | [c,evd] -> (* solve_candidates might have been called recursively in the mean *) (* time and the evar been solved by the filtering process *) if Evd.is_undefined evd evk then - let evd' = Evd.define evk (EConstr.Unsafe.to_constr c) evd in + let evd' = Evd.define evk c evd in check_evar_instance evd' evk c conv_algo else evd | l when List.length l < List.length l' -> @@ -1401,8 +1397,8 @@ let occur_evar_upto_types sigma n c = Array.iter occur_rec args else ( seen := Evar.Set.add sp !seen; - Option.iter occur_rec (existential_opt_value sigma e); - occur_rec (Evd.existential_type sigma e)) + Option.iter occur_rec (existential_opt_value0 sigma e); + occur_rec (Evd.existential_type0 sigma e)) | _ -> Constr.iter occur_rec c in try occur_rec c; false with Occur -> true @@ -1529,7 +1525,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* Try to project (a restriction of) the left evar ... *) try let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in - let evd = Evd.define evk' (EConstr.Unsafe.to_constr body) evd in + let evd = Evd.define evk' body evd in check_evar_instance evd evk' body conv_algo with | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *) @@ -1592,14 +1588,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = Id.Set.subset (collect_vars evd rhs) !names in let body = - if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *) + if fast rhs then nf_evar evd rhs (** FIXME? *) else let t' = imitate (env,0) rhs in if !progress then (recheck_applications conv_algo (evar_env evi) evdref t'; t') else t' in (!evdref,body) - + (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, * [define] tries to find an instance lhs such that @@ -1644,7 +1640,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = print_constr body); raise e in*) let evd' = check_evar_instance evd' evk body conv_algo in - Evd.define evk (EConstr.Unsafe.to_constr body) evd' + Evd.define evk body evd' with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs @@ -1691,8 +1687,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = *) let status_changed evd lev (pbty,_,t1,t2) = - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false) @@ -1702,7 +1696,7 @@ let reconsider_unif_constraints conv_algo evd = (fun p (pbty,env,t1,t2 as x) -> match p with | Success evd -> - (match conv_algo env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with + (match conv_algo env evd pbty t1 t2 with | Success _ as x -> x | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e))) | UnifFailure _ as x -> x) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 9b21599b6..3f05c58c4 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -63,7 +63,7 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result -(** @deprecated Alias for [reconsider_unif_constraints] *) +[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"] val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 74f2cefab..8ecec30cf 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -13,7 +13,6 @@ open CAst open Names open Nameops open Globnames -open Misctypes open Glob_term open Evar_kinds open Ltac_pretype @@ -47,12 +46,20 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = let comp2 = f ty in (na,k,comp1,comp2) + +let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with +| GProp, GProp -> true +| GSet, GSet -> true +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 +| _ -> false + let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Decl_kinds.Explicit, Decl_kinds.Explicit -> true | Decl_kinds.Implicit, Decl_kinds.Implicit -> true | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false -let case_style_eq s1 s2 = match s1, s2 with +let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true | IfStyle, IfStyle -> true | LetPatternStyle, LetPatternStyle -> true @@ -113,7 +120,7 @@ let instance_eq f (x1,c1) (x2,c2) = Id.equal x1 x2 && f c1 c2 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with - | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 + | GRef (gr1, _), GRef (gr2, _) -> GlobRef.equal gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 @@ -136,14 +143,14 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> f m1 m2 && Name.equal pat1 pat2 && Option.equal f p1 p2 && f c1 c2 && f t1 t2 - | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) -> fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 - | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 + | GSort s1, GSort s2 -> glob_sort_eq s1 s2 | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> Option.equal (==) gn1 gn2 (** Only thing sensible *) && - Miscops.intro_pattern_naming_eq nam1 nam2 + Namegen.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 | GProj (p1, t1), GProj (p2, t2) -> @@ -153,6 +160,21 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c +(** Mapping [cast_type] *) + +let map_cast_type f = function + | CastConv a -> CastConv (f a) + | CastVM a -> CastVM (f a) + | CastCoerce -> CastCoerce + | CastNative a -> CastNative (f a) + +let smartmap_cast_type f c = + match c with + | CastConv a -> let a' = f a in if a' == a then c else CastConv a' + | CastVM a -> let a' = f a in if a' == a then c else CastVM a' + | CastCoerce -> CastCoerce + | CastNative a -> let a' = f a in if a' == a then c else CastNative a' + let map_glob_constr_left_to_right f = DAst.map (function | GApp (g,args) -> let comp1 = f g in @@ -193,7 +215,7 @@ let map_glob_constr_left_to_right f = DAst.map (function GRec (fk,idl,comp1,comp2,comp3) | GCast (c,k) -> let comp1 = f c in - let comp2 = Miscops.map_cast_type f k in + let comp2 = map_cast_type f k in GCast (comp1,comp2) | GProj (p,c) -> GProj (p, f c) @@ -247,8 +269,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function | GCases (_,rtntypopt,tml,pl) -> let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in let fold_tomatch (v',acc) (tm,(na,onal)) = - (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'') - (Name.fold_right g na v') onal, + ((if rtntypopt = None then v' else + Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'') + (Name.fold_right g na v') onal), f v acc tm) in let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in let acc = Option.fold_left (f v') acc rtntypopt in @@ -259,6 +282,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function | GIf (c,rtntyp,b1,b2) -> f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2 | GRec (_,idl,bll,tyl,bv) -> + let v' = Array.fold_right g idl v in let f' i acc fid = let v,acc = List.fold_left @@ -266,7 +290,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty)) (v,acc) bll.(i) in - f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in + f v' (f v acc tyl.(i)) (bv.(i)) in Array.fold_left_i f' acc idl | GCast (c,k) -> let acc = match k with @@ -331,19 +355,19 @@ let bound_glob_vars = (** Mapping of names in binders *) -(* spiwack: I used a smartmap-style kind of mapping here, because the +(* spiwack: I used a smart-style kind of mapping here, because the operation will be the identity almost all of the time (with any term outside of Ltac to begin with). But to be honest, there would probably be no significant penalty in doing reallocation as pattern-matching expressions are usually rather small. *) let map_inpattern_binders f ({loc;v=(id,nal)} as x) = - let r = CList.smartmap f nal in + let r = CList.Smart.map f nal in if r == nal then x else CAst.make ?loc (id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = - let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in + let r = Option.Smart.map (fun p -> map_inpattern_binders f p) inp in if r == inp then x else c,(f na, r) @@ -355,7 +379,7 @@ let rec map_case_pattern_binders f = DAst.map (function | PatCstr (c,ps,na) as x -> let rna = f na in let rps = - CList.smartmap (fun p -> map_case_pattern_binders f p) ps + CList.Smart.map (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x else PatCstr(c,rps,rna) @@ -366,13 +390,13 @@ let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause = It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) - let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in + let r = List.Smart.map (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x else CAst.make ?loc (il,r,rhs) let map_pattern_binders f tomatch branches = - CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, - CList.smartmap (fun br -> map_cases_branch_binders f br) branches + CList.Smart.map (fun tm -> map_tomatch_binders f tm) tomatch, + CList.Smart.map (fun br -> map_cases_branch_binders f br) branches (** /mapping of names in binders *) @@ -538,7 +562,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo | PatVar (Name id) when not isclosed -> GVar id | PatVar Anonymous when not isclosed -> - GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None) + GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None) | _ -> raise Not_found ) x diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 124440f5d..c967f4e88 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,8 @@ open Glob_term (** Equalities *) +val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool + val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val alias_of_pat : 'a cases_pattern_g -> Name.t @@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g val cast_type_eq : ('a -> 'a -> bool) -> - 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool + 'a cast_type -> 'a cast_type -> bool val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool +(** Mapping [cast_type] *) + +val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type +val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type + (** Operations on [glob_constr] *) val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml new file mode 100644 index 000000000..54fa5328f --- /dev/null +++ b/pretyping/glob_term.ml @@ -0,0 +1,138 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Untyped intermediate terms *) + +(** [glob_constr] comes after [constr_expr] and before [constr]. + + Resolution of names, insertion of implicit arguments placeholder, + and notations are done, but coercions, inference of implicit + arguments and pattern-matching compilation are not. *) + +open Names +open Decl_kinds + +type existential_name = Id.t + +(** Sorts *) + +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) + +type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + +type level_info = Libnames.reference universe_kind +type glob_level = level_info glob_sort_gen +type glob_constraint = glob_level * Univ.constraint_type * glob_level + +type sort_info = (Libnames.reference * int) option list +type glob_sort = sort_info glob_sort_gen + +(** Casts *) + +type 'a cast_type = + | CastConv of 'a + | CastVM of 'a + | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) + | CastNative of 'a + +(** The kind of patterns that occurs in "match ... with ... end" + + locs here refers to the ident's location, not whole pat *) +type 'a cases_pattern_r = + | PatVar of Name.t + | PatCstr of constructor * 'a cases_pattern_g list * Name.t + (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) +and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t + +type cases_pattern = [ `any ] cases_pattern_g + +(** Representation of an internalized (or in other words globalized) term. *) +type 'a glob_constr_r = + | GRef of GlobRef.t * glob_level list option + (** An identifier that represents a reference to an object defined + either in the (global) environment or in the (local) context. *) + | GVar of Id.t + (** An identifier that cannot be regarded as "GRef". + Bound variables are typically represented this way. *) + | GEvar of existential_name * (Id.t * 'a glob_constr_g) list + | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *) + | GApp of 'a glob_constr_g * 'a glob_constr_g list + | GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GProd of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GLetIn of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g + | GCases of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g + (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) + | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * + 'a glob_constr_g array * 'a glob_constr_g array + | GSort of glob_sort + | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option + | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type + | GProj of Projection.t * 'a glob_constr_g +and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t + +and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g + +and 'a fix_recursion_order_g = + | GStructRec + | GWfRec of 'a glob_constr_g + | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option + +and 'a fix_kind_g = + | GFix of ((int option * 'a fix_recursion_order_g) array * int) + | GCoFix of int + +and 'a predicate_pattern_g = + Name.t * (inductive * Name.t list) CAst.t option + (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) + +and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) + +and 'a tomatch_tuples_g = 'a tomatch_tuple_g list + +and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t +(** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables + of [t] are members of [il]. *) +and 'a cases_clauses_g = 'a cases_clause_g list + +type glob_constr = [ `any ] glob_constr_g +type tomatch_tuple = [ `any ] tomatch_tuple_g +type tomatch_tuples = [ `any ] tomatch_tuples_g +type cases_clause = [ `any ] cases_clause_g +type cases_clauses = [ `any ] cases_clauses_g +type glob_decl = [ `any ] glob_decl_g +type fix_kind = [ `any ] fix_kind_g +type predicate_pattern = [ `any ] predicate_pattern_g +type fix_recursion_order = [ `any ] fix_recursion_order_g + +type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr + +type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.t +type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list +type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list + +type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g +type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g +type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g + +type 'a extended_glob_local_binder_r = + | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g + | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option + | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g +and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t + +type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 3327c250d..27b029aad 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -42,7 +42,7 @@ type recursion_scheme_error = exception RecursionSchemeError of recursion_scheme_error -let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na +let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na let name_assumption env = function | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) @@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = if not (Sorts.List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind))) + (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind))) in let ndepar = mip.mind_nrealdecls + 1 in @@ -550,7 +550,7 @@ let check_arities env listdepkind = let kelim = elim_sorts (mibi,mipi) in if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env + (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env kind),(mind,u)))) else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 119ff5222..d87a19d28 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -61,7 +61,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> (** Recursor names utilities *) -val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference +val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t val elimination_suffix : Sorts.family -> string val make_elimination_ident : Id.t -> Sorts.family -> Id.t diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 8e3c33ff7..b1ab2d2b7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -629,6 +629,10 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = env evdref scl ar.template_level (ctx,ar.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) +let type_of_projection_constant env (p,u) = + let pb = lookup_projection p env in + Vars.subst_instance_constr u pb.proj_type + let type_of_projection_knowing_arg env sigma p c ty = let c = EConstr.Unsafe.to_constr c in let IndType(pars,realargs) = @@ -637,7 +641,7 @@ let type_of_projection_knowing_arg env sigma p c ty = raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type") in let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u)) + substl (c :: List.rev pars) (type_of_projection_constant env (p,u)) (***********************************************) (* Guard condition *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 296f25d3f..b0d714b03 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -129,8 +129,8 @@ val allowed_sorts : env -> inductive -> Sorts.family list val has_dependent_elim : mutual_inductive_body -> bool (** Primitive projections *) -val projection_nparams : projection -> int -val projection_nparams_env : env -> projection -> int +val projection_nparams : Projection.t -> int +val projection_nparams_env : env -> Projection.t -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> EConstr.t -> EConstr.types -> types diff --git a/pretyping/locus.ml b/pretyping/locus.ml new file mode 100644 index 000000000..37dd120c1 --- /dev/null +++ b/pretyping/locus.ml @@ -0,0 +1,99 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** Locus : positions in hypotheses and goals *) + +type 'a or_var = + | ArgArg of 'a + | ArgVar of lident + +(** {6 Occurrences} *) + +type 'a occurrences_gen = + | AllOccurrences + | AllOccurrencesBut of 'a list (** non-empty *) + | NoOccurrences + | OnlyOccurrences of 'a list (** non-empty *) + +type occurrences_expr = (int or_var) occurrences_gen +type 'a with_occurrences = occurrences_expr * 'a + +type occurrences = int occurrences_gen + + +(** {6 Locations} + + Selecting the occurrences in body (if any), in type, or in both *) + +type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly + + +(** {6 Abstract clauses expressions} + + A [clause_expr] (and its instance [clause]) denotes occurrences and + hypotheses in a goal in an abstract way; in particular, it can refer + to the set of all hypotheses independently of the effective contents + of the current goal + + Concerning the field [onhyps]: + - [None] means *on every hypothesis* + - [Some l] means on hypothesis belonging to l *) + +type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag + +type 'id clause_expr = + { onhyps : 'id hyp_location_expr list option; + concl_occs : occurrences_expr } + +type clause = Id.t clause_expr + + +(** {6 Concrete view of occurrence clauses} *) + +(** [clause_atom] refers either to an hypothesis location (i.e. an + hypothesis with occurrences and a position, in body if any, in type + or in both) or to some occurrences of the conclusion *) + +type clause_atom = + | OnHyp of Id.t * occurrences_expr * hyp_location_flag + | OnConcl of occurrences_expr + +(** A [concrete_clause] is an effective collection of occurrences + in the hypotheses and the conclusion *) + +type concrete_clause = clause_atom list + + +(** {6 A weaker form of clause with no mention of occurrences} *) + +(** A [hyp_location] is an hypothesis together with a location *) + +type hyp_location = Id.t * hyp_location_flag + +(** A [goal_location] is either an hypothesis (together with a location) + or the conclusion (represented by None) *) + +type goal_location = hyp_location option + + +(** {6 Simple clauses, without occurrences nor location} *) + +(** A [simple_clause] is a set of hypotheses, possibly extended with + the conclusion (conclusion is represented by None) *) + +type simple_clause = Id.t option list + +(** {6 A notion of occurrences allowing to express "all occurrences + convertible to the first which matches"} *) + +type 'a or_like_first = AtOccs of 'a | LikeFirst + diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 1664e68f2..6b6a3f8a9 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") - | Misctypes.ArgArg x -> x + | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") + | ArgArg x -> x let occurrences_of_hyp id cls = let rec hyp_occ = function diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml deleted file mode 100644 index 0f0af5409..000000000 --- a/pretyping/miscops.ml +++ /dev/null @@ -1,76 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Misctypes -open Genredexpr - -(** Mapping [cast_type] *) - -let map_cast_type f = function - | CastConv a -> CastConv (f a) - | CastVM a -> CastVM (f a) - | CastCoerce -> CastCoerce - | CastNative a -> CastNative (f a) - -let smartmap_cast_type f c = - match c with - | CastConv a -> let a' = f a in if a' == a then c else CastConv a' - | CastVM a -> let a' = f a in if a' == a then c else CastVM a' - | CastCoerce -> CastCoerce - | CastNative a -> let a' = f a in if a' == a then c else CastNative a' - -(** Equalities on [glob_sort] *) - -let glob_sort_eq g1 g2 = match g1, g2 with -| GProp, GProp -> true -| GSet, GSet -> true -| GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 -| _ -> false - -let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with -| IntroAnonymous, IntroAnonymous -> true -| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2 -| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 -| _ -> false - -(** Mapping [red_expr_gen] *) - -let map_flags f flags = - { flags with rConst = List.map f flags.rConst } - -let map_occs f (occ,e) = (occ,f e) - -let map_red_expr_gen f g h = function - | Fold l -> Fold (List.map f l) - | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) - | Simpl (flags,occs_o) -> - Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o) - | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) - | Cbv flags -> Cbv (map_flags g flags) - | Lazy flags -> Lazy (map_flags g flags) - | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o) - | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o) - | Cbn flags -> Cbn (map_flags g flags) - | ExtraRedExpr _ | Red _ | Hnf as x -> x - -(** Mapping bindings *) - -let map_explicit_bindings f l = - let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in - List.map map l - -let map_bindings f = function -| ImplicitBindings l -> ImplicitBindings (List.map f l) -| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl) -| NoBindings -> NoBindings - -let map_with_bindings f (x, bl) = (f x, map_bindings f bl) diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli deleted file mode 100644 index abe817fe5..000000000 --- a/pretyping/miscops.mli +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Misctypes -open Genredexpr - -(** Mapping [cast_type] *) - -val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type -val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type - -(** Equalities on [glob_sort] *) - -val glob_sort_eq : glob_sort -> glob_sort -> bool - -(** Equalities on [intro_pattern_naming] *) - -val intro_pattern_naming_eq : - intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool - -(** Mapping [red_expr_gen] *) - -val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) -> - ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen - -(** Mapping bindings *) - -val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings -val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index fcbf50fea..4b8e0e096 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -188,6 +188,14 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch +let get_proj env ((mind, _n), i) = + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | None | Some None -> + CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") + | Some (Some (_, projs, _)) -> + Projection.make projs.(i) true + let rec nf_val env sigma v typ = match kind_of_value v with | Vaccu accu -> nf_accu env sigma accu @@ -279,9 +287,10 @@ and nf_atom env sigma atom = let codom = nf_type env sigma (codom vn) in mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv - | Aproj(p,c) -> + | Aproj (p, c) -> let c = nf_accu env sigma c in - mkProj(Projection.make p true,c) + let p = get_proj env p in + mkProj(p, c) | _ -> fst (nf_atom_type env sigma atom) and nf_atom_type env sigma atom = @@ -303,10 +312,10 @@ and nf_atom_type env sigma atom = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env + hnf_prod_applist_assum env nparamdecls (Inductiveops.type_of_inductive env ind) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma ind mip params p pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in @@ -357,25 +366,30 @@ and nf_atom_type env sigma atom = | Aproj(p,c) -> let c,tc = nf_accu_type env sigma c in let cj = make_judge c tc in - let uj = Typeops.judge_of_projection env (Projection.make p true) cj in + let p = get_proj env p in + let uj = Typeops.judge_of_projection env p cj in uj.uj_val, uj.uj_type and nf_predicate env sigma ind mip params v pT = - match kind_of_value v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in - let name,dom,codom = - try decompose_prod env pT with - DestKO -> - CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") - in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> false, nf_type env sigma v + end + | _ -> + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in let name = Name (Id.of_string "c") in @@ -385,7 +399,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_type env sigma v + | _ -> false, nf_type env sigma v and nf_evar env sigma evk ty args = let evi = try Evd.find sigma evk with Not_found -> assert false in @@ -401,9 +415,9 @@ and nf_evar env sigma evk ty args = mkEvar (evk, Array.of_list args), ty let evars_of_evar_map sigma = - { Nativelambda.evars_val = Evd.existential_opt_value sigma; - Nativelambda.evars_typ = Evd.existential_type sigma; - Nativelambda.evars_metas = Evd.meta_type sigma } + { Nativelambda.evars_val = Evd.existential_opt_value0 sigma; + Nativelambda.evars_typ = Evd.existential_type0 sigma; + Nativelambda.evars_metas = Evd.meta_type0 sigma } (* fork perf process, return profiler's process id *) let start_profiler_linux profile_fn = @@ -457,13 +471,12 @@ let native_norm env sigma c ty = if not Coq_config.native_compiler then user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else - let penv = Environ.pre_env env in (* Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); *) let ml_filename, prefix = Nativelib.get_ml_filename () in - let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in + let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in let profile = get_profiling_enabled () in match Nativelib.compile ml_filename code ~profile:profile with | true, fn -> diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 67b7a2a40..4997d0bf0 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml new file mode 100644 index 000000000..be7ebe49c --- /dev/null +++ b/pretyping/pattern.ml @@ -0,0 +1,44 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** {5 Patterns} *) + +(** Cases pattern variables *) +type patvar = Id.t + +type case_info_pattern = + { cip_style : Constr.case_style; + cip_ind : inductive option; + cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) + cip_extensible : bool (** does this match end with _ => _ ? *) } + +type constr_pattern = + | PRef of GlobRef.t + | PVar of Id.t + | PEvar of Evar.t * constr_pattern array + | PRel of int + | PApp of constr_pattern * constr_pattern array + | PSoApp of patvar * constr_pattern list + | PProj of Projection.t * constr_pattern + | PLambda of Name.t * constr_pattern * constr_pattern + | PProd of Name.t * constr_pattern * constr_pattern + | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern + | PSort of Glob_term.glob_sort + | PMeta of patvar option + | PIf of constr_pattern * constr_pattern * constr_pattern + | PCase of case_info_pattern * constr_pattern * constr_pattern * + (int * bool list * constr_pattern) list (** index of constructor, nb of args *) + | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) + | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) + +(** Nota : in a [PCase], the array of branches might be shorter than + expected, denoting the use of a final "_ => _" branch *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index dcb93bfb6..622a8e982 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -15,11 +15,9 @@ open Globnames open Nameops open Term open Constr -open Vars open Glob_term open Pp open Mod_subst -open Misctypes open Decl_kinds open Pattern open Environ @@ -31,7 +29,7 @@ let case_info_pattern_eq i1 i2 = i1.cip_extensible == i2.cip_extensible let rec constr_pattern_eq p1 p2 = match p1, p2 with -| PRef r1, PRef r2 -> eq_gr r1 r2 +| PRef r1, PRef r2 -> GlobRef.equal r1 r2 | PVar v1, PVar v2 -> Id.equal v1 v2 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) -> Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2 @@ -48,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) -> Name.equal v1 v2 && constr_pattern_eq b1 b2 && Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2 -| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2 +| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2 @@ -57,10 +55,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with constr_pattern_eq p1 p2 && constr_pattern_eq r1 r2 && List.equal pattern_eq l1 l2 -| PFix f1, PFix f2 -> - fixpoint_eq f1 f2 -| PCoFix f1, PCoFix f2 -> - cofixpoint_eq f1 f2 +| PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) -> + Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq f1 f2 +| PCoFix (i1,f1), PCoFix (i2,f2) -> + Int.equal i1 i2 && rec_declaration_eq f1 f2 | PProj (p1, t1), PProj (p2, t2) -> Projection.equal p1 p2 && constr_pattern_eq t1 t2 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ @@ -71,19 +69,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with and pattern_eq (i1, j1, p1) (i2, j2, p2) = Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2 -and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) = - Int.equal i1 i2 && - Array.equal Int.equal arg1 arg2 && - rec_declaration_eq r1 r2 - -and cofixpoint_eq (i1, r1) (i2, r2) = - Int.equal i1 i2 && - rec_declaration_eq r1 r2 - and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && - Array.equal Constr.equal c1 c2 && - Array.equal Constr.equal r1 r2 + Array.equal constr_pattern_eq c1 c2 && + Array.equal constr_pattern_eq r1 r2 let rec occur_meta_pattern = function | PApp (f,args) -> @@ -123,8 +112,10 @@ let rec occurn_pattern n = function | PMeta _ | PSoApp _ -> true | PEvar (_,args) -> Array.exists (occurn_pattern n) args | PVar _ | PRef _ | PSort _ -> false - | PFix fix -> not (noccurn n (mkFix fix)) - | PCoFix cofix -> not (noccurn n (mkCoFix cofix)) + | PFix (_,(_,tl,bl)) -> + Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl + | PCoFix (_,(_,tl,bl)) -> + Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl let noccurn_pattern n c = not (occurn_pattern n c) @@ -192,7 +183,7 @@ let pattern_of_constr env sigma t = | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) - if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) + if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev) else PEvar (evk,Array.map (pattern_of_constr env) ctxt) | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> @@ -209,8 +200,16 @@ let pattern_of_constr env sigma t = in PCase (cip, pattern_of_constr env p, pattern_of_constr env a, Array.to_list (Array.mapi branch_of_constr br)) - | Fix f -> PFix f - | CoFix f -> PCoFix f in + | Fix (lni,(lna,tl,bl)) -> + let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in + let env' = Array.fold_left2 push env lna tl in + PFix (lni,(lna,Array.map (pattern_of_constr env) tl, + Array.map (pattern_of_constr env') bl)) + | CoFix (ln,(lna,tl,bl)) -> + let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in + let env' = Array.fold_left2 push env lna tl in + PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl, + Array.map (pattern_of_constr env') bl)) in pattern_of_constr env t (* To process patterns, we need a translation without typing at all. *) @@ -225,10 +224,14 @@ let map_pattern_with_binders g f l = function | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) | PProj (p,pc) -> PProj (p, f l pc) + | PFix (lni,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | PCoFix (ln,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* Non recursive *) - | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ - (* Bound to terms *) - | PFix _ | PCoFix _ as x) -> x + | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x let error_instantiate_pattern id l = let is = match l with @@ -262,15 +265,12 @@ let instantiate_pattern env sigma lvar c = error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) - | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.") | c -> map_pattern_with_binders (fun id vars -> id::vars) aux vars c in aux [] c let rec liftn_pattern k n = function | PRel i as x -> if i >= n then PRel (i+k) else x - | PFix x -> PFix (destFix (liftn k n (mkFix x))) - | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x))) | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c let lift_pattern k = liftn_pattern k 1 @@ -278,9 +278,11 @@ let lift_pattern k = liftn_pattern k 1 let rec subst_pattern subst pat = match pat with | PRef ref -> - let ref',t = subst_global subst ref in - if ref' == ref then pat else - pattern_of_constr (Global.env()) Evd.empty t + let ref',t = subst_global subst ref in + if ref' == ref then pat else + let env = Global.env () in + let evd = Evd.from_env env in + pattern_of_constr env evd t | PVar _ | PEvar _ | PRel _ -> pat @@ -292,11 +294,11 @@ let rec subst_pattern subst pat = PProj(p',c') | PApp (f,args) -> let f' = subst_pattern subst f in - let args' = Array.smartmap (subst_pattern subst) args in + let args' = Array.Smart.map (subst_pattern subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.smartmap (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> @@ -311,7 +313,7 @@ let rec subst_pattern subst pat = PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in - let t' = Option.smartmap (subst_pattern subst) t in + let t' = Option.Smart.map (subst_pattern subst) t in let c2' = subst_pattern subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') @@ -325,7 +327,7 @@ let rec subst_pattern subst pat = PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in - let ind' = Option.smartmap (subst_ind subst) ind in + let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in @@ -333,23 +335,39 @@ let rec subst_pattern subst pat = let c' = subst_pattern subst c in if c' == c then br else (i,n,c') in - let branches' = List.smartmap subst_branch branches in + let branches' = List.Smart.map subst_branch branches in if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') - | PFix fixpoint -> - let cstr = mkFix fixpoint in - let fixpoint' = destFix (subst_mps subst cstr) in - if fixpoint' == fixpoint then pat else - PFix fixpoint' - | PCoFix cofixpoint -> - let cstr = mkCoFix cofixpoint in - let cofixpoint' = destCoFix (subst_mps subst cstr) in - if cofixpoint' == cofixpoint then pat else - PCoFix cofixpoint' - -let mkPLambda na b = PLambda(na,PMeta None,b) -let rev_it_mkPLambda = List.fold_right mkPLambda + | PFix (lni,(lna,tl,bl)) -> + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in + if bl' == bl && tl' == tl then pat + else PFix (lni,(lna,tl',bl')) + | PCoFix (ln,(lna,tl,bl)) -> + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in + if bl' == bl && tl' == tl then pat + else PCoFix (ln,(lna,tl',bl')) + +let mkPLetIn na b t c = PLetIn(na,b,t,c) +let mkPProd na t u = PProd(na,t,u) +let mkPLambda na t b = PLambda(na,t,b) +let mkPLambdaUntyped na b = PLambda(na,PMeta None,b) +let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped + +let mkPProd_or_LetIn (na,_,bo,t) c = + match bo with + | None -> mkPProd na t c + | Some b -> mkPLetIn na b (Some t) c + +let mkPLambda_or_LetIn (na,_,bo,t) c = + match bo with + | None -> mkPLambda na t c + | Some b -> mkPLetIn na b (Some t) c + +let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c) +let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c) let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp @@ -399,7 +417,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> let mkGLambda na c = DAst.make ?loc @@ - GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; @@ -428,7 +446,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function let pred = match p,indnames with | Some p, Some {CAst.v=(_,nal)} -> let nvars = na :: List.rev nal @ vars in - rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) + rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p)) | None, _ -> PMeta None | Some p, None -> match DAst.get p with @@ -450,9 +468,40 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | GProj(p,c) -> PProj(p, pat_of_raw metas vars c) - | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> + | GRec (GFix (ln,n), ids, decls, tl, cl) -> + if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then + err ?loc (Pp.str "\"struct\" annotation is expected.") + else + let ln = Array.map (fst %> Option.get) ln in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PFix ((ln,n), (names, tl, cl)) + + | GRec (GCoFix n, ids, decls, tl, cl) -> + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PCoFix (n, (names, tl, cl)) + + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ -> err ?loc (Pp.str "Non supported pattern.")) +and pat_of_glob_in_context metas vars decls c = + let rec aux acc vars = function + | (na,bk,b,t) :: decls -> + let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in + aux (decl::acc) (na::vars) decls + | [] -> + acc, pat_of_raw metas vars c + in aux [] vars decls + and pats_of_glob_branches loc metas vars ind brs = let get_arg p = match DAst.get p with | PatVar na -> @@ -477,7 +526,7 @@ and pats_of_glob_branches loc metas vars ind brs = (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in let vars' = List.rev lna @ vars in - let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in + let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 9f0878578..36317b3ac 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -8,12 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open EConstr -open Globnames -open Glob_term +open Names open Mod_subst -open Misctypes +open Glob_term open Pattern +open EConstr open Ltac_pretype (** {5 Functions on patterns} *) @@ -32,12 +31,12 @@ exception BoundPattern type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly if [t] is an abstraction *) -val head_pattern_bound : constr_pattern -> global_reference +val head_pattern_bound : constr_pattern -> GlobRef.t (** [head_of_constr_reference c] assumes [r] denotes a reference and returns its label; raises an anomaly otherwise *) -val head_of_constr_reference : Evd.evar_map -> constr -> global_reference +val head_of_constr_reference : Evd.evar_map -> constr -> GlobRef.t (** [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 278a4761d..856894d9a 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -165,7 +165,7 @@ let error_not_product ?loc env sigma c = (*s Error in conversion from AST to glob_constr *) let error_var_not_found ?loc s = - raise_pretype_error ?loc (empty_env, Evd.empty, VarNotFound s) + raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s) (*s Typeclass errors *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4962b89a0..9e024b1c2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,6 +28,7 @@ open CErrors open Util open Names open Evd +open Constr open Term open Termops open Environ @@ -44,7 +45,6 @@ open Pretype_errors open Glob_term open Glob_ops open Evarconv -open Misctypes open Ltac_pretype module NamedDecl = Context.Named.Declaration @@ -117,7 +117,7 @@ open ExtraEnv exception Found of int array let nf_fix sigma (nas, cs, ts) = - let inj c = EConstr.to_constr sigma c in + let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in (nas, Array.map inj cs, Array.map inj ts) let search_guard ?loc env possible_indexes fixdefs = @@ -169,14 +169,6 @@ let _ = optread = is_strict_universe_declarations; optwrite = (:=) strict_universe_declarations }) -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = Universes.is_set_minimization; - optwrite = (:=) Universes.set_minimization }) - (** Miscellaneous interpretation functions *) let interp_known_universe_level evd r = @@ -245,7 +237,7 @@ let interp_known_level_info ?loc evd = function with Not_found -> user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) -let interp_level_info ?loc evd : Misctypes.level_info -> _ = function +let interp_level_info ?loc evd : level_info -> _ = function | UUnknown -> new_univ_level_variable ?loc univ_rigid evd | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s @@ -315,7 +307,7 @@ let apply_inference_hook hook evdref frozen = match frozen with then try let sigma, c = hook sigma evk in - Evd.define evk (EConstr.Unsafe.to_constr c) sigma + Evd.define evk c sigma with Exit -> sigma else @@ -429,7 +421,7 @@ let ltac_interp_name_env k0 lvar env sigma = let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let open Context.Rel.Declaration in - let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env else push_rel_context sigma ctxt' (pop_rel_context n env sigma) @@ -499,7 +491,7 @@ let interp_known_glob_level ?loc evd = function | GSet -> Univ.Level.set | GType s -> interp_known_level_info ?loc evd s -let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function +let interp_glob_level ?loc evd : glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set | GType s -> interp_level_info ?loc evd s @@ -532,7 +524,7 @@ let pretype_global ?loc rigid env evd gr us = interp_instance ?loc evd ~len l in let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in - (sigma, EConstr.of_constr c) + (sigma, c) let pretype_ref ?loc evdref env ref us = match ref with @@ -674,14 +666,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 +694,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 +789,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 @@ -1082,9 +1081,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential !evdref cty || occur_existential !evdref tval) then - let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> 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: " ++ @@ -1093,9 +1092,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end @@ -1109,7 +1108,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = let id = NamedDecl.get_id decl in - let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in + let t = replace_vars subst (NamedDecl.get_type decl) in let c, update = try let c = List.assoc id update in @@ -1118,7 +1117,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in @@ -1150,7 +1149,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D (* Correction of bug #5315 : we need to define an evar for *all* holes *) let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in let ev,_ = destEvar !evdref evkt in - evdref := Evd.define ev (to_constr !evdref v) !evdref; + evdref := Evd.define ev (nf_evar !evdref v) !evdref; (* End of correction of bug #5315 *) { utj_val = v; utj_type = s } @@ -1166,10 +1165,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/pretyping.mli b/pretyping/pretyping.mli index 415c4e172..73f5b77e0 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -22,7 +22,7 @@ open Ltac_pretype open Evardefine val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> - Misctypes.glob_level -> Univ.Level.t + glob_level -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index ae4ad0be7..3d9b5d3cf 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,5 +1,5 @@ Geninterp -Ltac_pretype +Locus Locusops Pretype_errors Reductionops @@ -17,8 +17,10 @@ Recordops Evarconv Typing Miscops +Glob_term +Ltac_pretype Glob_ops -Redops +Pattern Patternops Constr_matching Tacred @@ -32,4 +34,3 @@ Indrec Cases Pretyping Unification -Univdecls 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/program.mli b/pretyping/program.mli index df0848ba1..a8f511578 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -8,37 +8,37 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open EConstr -open Globnames (** A bunch of Coq constants used by Progam *) -val sig_typ : unit -> global_reference -val sig_intro : unit -> global_reference -val sig_proj1 : unit -> global_reference -val sigT_typ : unit -> global_reference -val sigT_intro : unit -> global_reference -val sigT_proj1 : unit -> global_reference -val sigT_proj2 : unit -> global_reference +val sig_typ : unit -> GlobRef.t +val sig_intro : unit -> GlobRef.t +val sig_proj1 : unit -> GlobRef.t +val sigT_typ : unit -> GlobRef.t +val sigT_intro : unit -> GlobRef.t +val sigT_proj1 : unit -> GlobRef.t +val sigT_proj2 : unit -> GlobRef.t -val prod_typ : unit -> global_reference -val prod_intro : unit -> global_reference -val prod_proj1 : unit -> global_reference -val prod_proj2 : unit -> global_reference +val prod_typ : unit -> GlobRef.t +val prod_intro : unit -> GlobRef.t +val prod_proj1 : unit -> GlobRef.t +val prod_proj2 : unit -> GlobRef.t -val coq_eq_ind : unit -> global_reference -val coq_eq_refl : unit -> global_reference -val coq_eq_refl_ref : unit -> global_reference -val coq_eq_rect : unit -> global_reference +val coq_eq_ind : unit -> GlobRef.t +val coq_eq_refl : unit -> GlobRef.t +val coq_eq_refl_ref : unit -> GlobRef.t +val coq_eq_rect : unit -> GlobRef.t -val coq_JMeq_ind : unit -> global_reference -val coq_JMeq_refl : unit -> global_reference +val coq_JMeq_ind : unit -> GlobRef.t +val coq_JMeq_refl : unit -> GlobRef.t val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) -val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr +val papp : Evd.evar_map ref -> (unit -> GlobRef.t) -> constr array -> constr val get_proofs_transparency : unit -> bool val is_program_cases : unit -> bool diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index d070edead..56a883099 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -69,8 +69,8 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - List.smartmap - (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) + List.Smart.map + (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn))) projs in let id' = fst (subst_constructor subst id) in @@ -144,13 +144,13 @@ type obj_typ = { o_TCOMPS : constr list } (* ordered *) type cs_pattern = - Const_cs of global_reference + Const_cs of GlobRef.t | Prod_cs | Sort_cs of Sorts.family | Default_cs let eq_cs_pattern p1 p2 = match p1, p2 with -| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2 +| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2 | Prod_cs, Prod_cs -> true | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 | Default_cs, Default_cs -> true @@ -199,7 +199,7 @@ let warn_projection_no_head_constant = let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in + let term_pp = Termops.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") @@ -211,7 +211,7 @@ let compute_canonical_projections warn (con,ind) = let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in let c = Environ.constant_value_in env (con,u) in - let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in let lt = List.rev_map snd sign in @@ -317,7 +317,9 @@ let check_and_decompose_canonical_structure ref = let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref "Could not find its value in the global environment." in - let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in + let env = Global.env () in + let evd = Evd.from_env env in + let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 1f7b23c0c..748f053b2 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -10,7 +10,6 @@ open Names open Constr -open Globnames (** Operations concerning records and canonical structures *) @@ -40,10 +39,10 @@ val lookup_structure : inductive -> struc_typ val lookup_projections : inductive -> Constant.t option list (** raise [Not_found] if not a projection *) -val find_projection_nparams : global_reference -> int +val find_projection_nparams : GlobRef.t -> int (** raise [Not_found] if not a projection *) -val find_projection : global_reference -> struc_typ +val find_projection : GlobRef.t -> struc_typ (** {6 Canonical structures } *) (** A canonical structure declares "canonical" conversion hints between @@ -52,7 +51,7 @@ val find_projection : global_reference -> struc_typ (** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = - Const_cs of global_reference + Const_cs of GlobRef.t | Prod_cs | Sort_cs of Sorts.family | Default_cs @@ -71,9 +70,9 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t -val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ -val declare_canonical_structure : global_reference -> unit +val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ +val declare_canonical_structure : GlobRef.t -> unit val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> - ((global_reference * cs_pattern) * obj_typ) list + ((GlobRef.t * cs_pattern) * obj_typ) list diff --git a/pretyping/redops.ml b/pretyping/redops.ml deleted file mode 100644 index 90c3bdfae..000000000 --- a/pretyping/redops.ml +++ /dev/null @@ -1,44 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Genredexpr - -let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *) - -let make_red_flag l = - let rec add_flag red = function - | [] -> red - | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FMatch :: lf -> add_flag { red with rMatch = true } lf - | FFix :: lf -> add_flag { red with rFix = true } lf - | FCofix :: lf -> add_flag { red with rCofix = true } lf - | FZeta :: lf -> add_flag { red with rZeta = true } lf - | FConst l :: lf -> - if red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); - add_flag { red with rConst = union_consts red.rConst l } lf - | FDeltaBut l :: lf -> - if red.rConst <> [] && not red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); - add_flag - { red with rConst = union_consts red.rConst l; rDelta = true } - lf - in - add_flag - {rBeta = false; rMatch = false; rFix = false; rCofix = false; - rZeta = false; rDelta = false; rConst = []} - l - - -let all_flags = - {rBeta = true; rMatch = true; rFix = true; rCofix = true; - rZeta = true; rDelta = true; rConst = []} diff --git a/pretyping/redops.mli b/pretyping/redops.mli deleted file mode 100644 index 285931ecd..000000000 --- a/pretyping/redops.mli +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Genredexpr - -val make_red_flag : 'a red_atom list -> 'a glob_red_flag - -val all_flags : 'a glob_red_flag diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9e3e68f05..7fb1a0a57 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -83,7 +83,7 @@ let declare_reduction_effect funkey f = (** A function to set the value of the print function *) let set_reduction_effect x funkey = - let termkey = Universes.constr_of_global x in + let termkey = UnivGen.constr_of_global x in Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey)) @@ -104,7 +104,7 @@ module ReductionBehaviour = struct type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] type req = | ReqLocal - | ReqGlobal of global_reference * (int list * int * flag list) + | ReqGlobal of GlobRef.t * (int list * int * flag list) let load _ (_,(_,(r, b))) = table := Refmap.add r b !table @@ -275,12 +275,12 @@ sig type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list @@ -332,12 +332,12 @@ struct type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list @@ -701,18 +701,18 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> - let open Universes in + let open UnivProblem in try let (cst_mod,cst_sect,_) = Constant.repr3 reference in let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in - let (cst, u), ctx = fresh_constant_instance env cst in + let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in begin match csts with | Some csts -> - let subst = Constraints.fold (fun cst acc -> + let subst = Set.fold (fun cst acc -> let l, r = match cst with | ULub (u, v) | UWeak (u, v) -> u, v | UEq (u, v) | ULe (u, v) -> @@ -871,7 +871,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Evar ev -> fold () | Meta ev -> (match safe_meta_value sigma ev with - | Some body -> whrec cst_l (EConstr.of_constr body, stack) + | Some body -> whrec cst_l (body, stack) | None -> fold ()) | Const (c,u as const) -> reduction_effect_hook env sigma (EConstr.to_constr sigma x) @@ -1106,7 +1106,7 @@ let local_whd_state_gen flags sigma = | Evar ev -> s | Meta ev -> (match safe_meta_value sigma ev with - Some c -> whrec (EConstr.of_constr c,stack) + Some c -> whrec (c,stack) | None -> s) | Construct ((ind,c),u) -> @@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) try - let b, sigma = - let ans = - if pb == Reduction.CUMUL then + let ans = match pb with + | Reduction.CUMUL -> EConstr.leq_constr_universes env sigma x y - else + | Reduction.CONV -> EConstr.eq_constr_universes env sigma x y in let ans = match ans with @@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with - | None -> false, sigma - | Some sigma -> true, sigma - in - if b then sigma, true - else + | Some sigma -> ans + | None -> let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in - sigma', true + Some sigma' with - | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ when catch_incon -> sigma, false + | Reduction.NotConvertible -> None + | Univ.UniverseInconsistency _ when catch_incon -> None | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> @@ -1392,7 +1388,7 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = (********************************************************************) let whd_meta sigma c = match EConstr.kind sigma c with - | Meta p -> (try EConstr.of_constr (meta_value sigma p) with Not_found -> c) + | Meta p -> (try meta_value sigma p with Not_found -> c) | _ -> c let default_plain_instance_ident = Id.of_string "H" @@ -1404,7 +1400,7 @@ let plain_instance sigma s c = | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in - let l' = CArray.Fun1.smartmap irec n l in + let l' = Array.Fun1.Smart.map irec n l in (match EConstr.kind sigma f with | Meta p -> (* Don't flatten application nodes: this is used to extract a @@ -1413,7 +1409,7 @@ let plain_instance sigma s c = (try let g = Metamap.find p s in match EConstr.kind sigma g with | App _ -> - let l' = CArray.Fun1.smartmap lift 1 l' in + let l' = Array.Fun1.Smart.map lift 1 l' in mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) @@ -1612,7 +1608,7 @@ let meta_value evd mv = match meta_opt_fvalue evd mv with | Some (b,_) -> let metas = Metamap.bind valrec b.freemetas in - instance evd metas (EConstr.of_constr b.rebus) + instance evd metas b.rebus | None -> mkMeta mv in valrec mv @@ -1625,9 +1621,8 @@ let meta_instance sigma b = instance sigma c_sigma b.rebus let nf_meta sigma c = - let c = EConstr.Unsafe.to_constr c in let cl = mk_freelisted c in - meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus } + meta_instance sigma { cl with rebus = cl.rebus } (* Instantiate metas that create beta/iota redexes *) @@ -1648,7 +1643,6 @@ let meta_reducible_instance evd b = (match try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None @@ -1660,7 +1654,6 @@ let meta_reducible_instance evd b = (match try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if isLambda evd g || not is_coerce then Some g else None with Not_found -> None @@ -1669,7 +1662,6 @@ let meta_reducible_instance evd b = | None -> mkApp (f,Array.map irec l)) | Meta m -> (try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if not is_coerce then irec g else u with Not_found -> u) @@ -1678,7 +1670,6 @@ let meta_reducible_instance evd b = (match try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 29dc3ed0f..9256fa7ce 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -25,10 +25,10 @@ module ReductionBehaviour : sig (** [set is_local ref (recargs, nargs, flags)] *) val set : - bool -> Globnames.global_reference -> (int list * int * flag list) -> unit + bool -> GlobRef.t -> (int list * int * flag list) -> unit val get : - Globnames.global_reference -> (int list * int * flag list) option - val print : Globnames.global_reference -> Pp.t + GlobRef.t -> (int list * int * flag list) option + val print : GlobRef.t -> Pp.t end (** {6 Support for reduction effects } *) @@ -41,7 +41,7 @@ val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit (* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *) -val set_reduction_effect : Globnames.global_reference -> effect_name -> unit +val set_reduction_effect : GlobRef.t -> effect_name -> unit (* [effect_hook env sigma key term] apply effect associated to [key] on [term] *) val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr -> @@ -70,12 +70,12 @@ module Stack : sig type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t @@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> constr -> constr -> evar_map * bool + env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool) -> unit + evar_map option) -> unit val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a @@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> constr -> constr -> evar_map * bool + evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3582b6447..746a68b21 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -57,8 +57,8 @@ let get_type_from_constraints env sigma t = if isEvar sigma (fst (decompose_app_vect sigma t)) then match List.map_filter (fun (pbty,env,t1,t2) -> - if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2 - else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1 + if is_fconv Reduction.CONV env sigma t t1 then Some t2 + else if is_fconv Reduction.CONV env sigma t t2 then Some t1 else None) (snd (Evd.extract_all_conv_pbs sigma)) with @@ -99,7 +99,7 @@ let retype ?(polyprop=true) sigma = let rec type_of env cstr = match EConstr.kind sigma cstr with | Meta n -> - (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) + (try strip_outer_cast sigma (Evd.meta_ftype sigma n).Evd.rebus with Not_found -> retype_error (BadMeta n)) | Rel n -> let ty = RelDecl.get_type (lookup_rel n env) in @@ -115,7 +115,7 @@ let retype ?(polyprop=true) sigma = try Inductiveops.find_rectype env sigma t with Not_found -> try - let t = EConstr.of_constr (get_type_from_constraints env sigma t) in + let t = get_type_from_constraints env sigma t in Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in @@ -170,7 +170,7 @@ let retype ?(polyprop=true) sigma = and type_of_global_reference_knowing_parameters env c args = let argtyps = - Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in + Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in match EConstr.kind sigma c with | Ind (ind, u) -> let u = EInstance.kind sigma u in diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 40424ead4..2aff0c777 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -50,6 +50,6 @@ val type_of_global_reference_knowing_conclusion : val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list -val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr +val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr val print_retype_error : retype_error -> Pp.t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 518d2f604..40c4cfaa4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Libnames open Globnames open Termops @@ -416,7 +416,7 @@ exception Partial reduction is solved by the expanded fix term. *) let solve_arity_problem env sigma fxminargs c = let evm = ref sigma in - let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in + let set_fix i = evm := Evd.define i (mkVar vfx) !evm in let rec check strict c = let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app_vect sigma c' in @@ -558,7 +558,7 @@ let match_eval_ref_value env sigma constr stack = else None | Proj (p, c) when not (Projection.unfolded p) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr) (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef (Projection.constant p)) then Some (mkProj (Projection.unfold p, c)) @@ -641,7 +641,7 @@ let whd_nothing_for_iota env sigma s = | _ -> s) | Evar ev -> s | Meta ev -> - (try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack) + (try whrec (Evd.meta_value sigma ev, stack) with Not_found -> s) | Const (const, u) when is_transparent_constant full_transparent_state const -> let u = EInstance.kind sigma u in @@ -1279,7 +1279,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = error_cannot_recognize ref | _ -> try - if eq_gr (fst (global_of_constr sigma c)) ref + if GlobRef.equal (fst (global_of_constr sigma c)) ref then it_mkProd_or_LetIn t l else raise Not_found with Not_found -> diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index aa7604f53..e6065dda8 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -14,7 +14,6 @@ open Evd open EConstr open Reductionops open Pattern -open Globnames open Locus open Univ open Ltac_pretype @@ -30,13 +29,13 @@ exception ReductionTacticError of reduction_tactic_error val is_evaluable : Environ.env -> evaluable_global_reference -> bool -val error_not_evaluable : Globnames.global_reference -> 'a +val error_not_evaluable : GlobRef.t -> 'a val evaluable_of_global_reference : - Environ.env -> Globnames.global_reference -> evaluable_global_reference + Environ.env -> GlobRef.t -> evaluable_global_reference val global_of_evaluable_reference : - evaluable_global_reference -> Globnames.global_reference + evaluable_global_reference -> GlobRef.t exception Redelimination @@ -88,10 +87,10 @@ val reduce_to_quantified_ind : env -> evar_map -> types -> (inductive * EInstan (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *) val reduce_to_quantified_ref : - env -> evar_map -> global_reference -> types -> types + env -> evar_map -> GlobRef.t -> types -> types val reduce_to_atomic_ref : - env -> evar_map -> global_reference -> types -> types + env -> evar_map -> GlobRef.t -> types -> types val find_hnf_rectype : env -> evar_map -> types -> (inductive * EInstance.t) * constr list diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 08051fd3a..d3aa7ac64 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -25,6 +25,13 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (*i*) +(* Core typeclasses hints *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen + let typeclasses_unique_solutions = ref false let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions @@ -64,16 +71,16 @@ type typeclass = { cl_univs : Univ.AUContext.t; (* The class implementation *) - cl_impl : global_reference; + cl_impl : GlobRef.t; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : global_reference option list * Context.Rel.t; + cl_context : GlobRef.t option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; (* The method implementaions as projections. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; cl_strict : bool; @@ -84,19 +91,19 @@ type typeclass = { type typeclasses = typeclass Refmap.t type instance = { - is_class: global_reference; - is_info: Vernacexpr.hint_info_expr; + is_class: GlobRef.t; + is_info: hint_info; (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_impl: global_reference; + is_impl: GlobRef.t; } type instances = (instance Refmap.t) Refmap.t let instance_impl is = is.is_impl -let hint_priority is = is.is_info.Vernacexpr.hint_priority +let hint_priority is = is.is_info.hint_priority let new_instance cl info glob impl = let global = @@ -158,7 +165,7 @@ let rec is_class_type evd c = | _ -> is_class_constr evd c let is_class_evar evd evi = - is_class_type evd (EConstr.of_constr evi.Evd.evar_concl) + is_class_type evd evi.Evd.evar_concl (* * classes persistent object @@ -173,12 +180,12 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.Smart.map do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.smartmap (fun (x, y, z) -> - (x, y, Option.smartmap do_subst_con z)) projs in + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> + (x, y, Option.Smart.map do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; @@ -216,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.Smart.map Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -227,12 +234,12 @@ let discharge_class (_,cl) = let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in - let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in + let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in { cl_univs = cl_univs'; cl_impl = cl_impl'; cl_context = context; cl_props = props; - cl_projs = List.smartmap discharge_proj cl.cl_projs; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } @@ -266,8 +273,6 @@ let check_instance env sigma c = not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false -open Vernacexpr - let build_subclasses ~check env sigma glob { hint_priority = pri } = let _id = Nametab.basename_of_global glob in let _next_id = @@ -276,7 +281,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in - let inst, ctx = Universes.fresh_instance_from ctx None in + let inst, ctx = UnivGen.fresh_instance_from ctx None in let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in @@ -316,7 +321,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob, inst) in + let term = UnivGen.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] @@ -475,7 +480,7 @@ let instances r = let cl = class_info r in instances_of cl let is_class gr = - Refmap.exists (fun _ v -> eq_gr v.cl_impl gr) !classes + Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes let is_instance = function | ConstRef c -> diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b80c28711..e4a56960c 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -16,6 +16,13 @@ open Environ type direction = Forward | Backward +(* Core typeclasses hints *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen + (** This module defines type-classes *) type typeclass = { (** The toplevel universe quantification in which the typeclass lives. In @@ -24,11 +31,11 @@ type typeclass = { (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) - cl_impl : global_reference; + cl_impl : GlobRef.t; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : global_reference option list * Context.Rel.t; + cl_context : GlobRef.t option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -37,7 +44,7 @@ type typeclass = { Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list; + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -49,18 +56,17 @@ type typeclass = { type instance -val instances : global_reference -> instance list +val instances : GlobRef.t -> instance list val typeclasses : unit -> typeclass list val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> - global_reference -> instance +val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance val add_instance : instance -> unit val remove_instance : instance -> unit -val class_info : global_reference -> typeclass (** raises a UserError if not a class *) +val class_info : GlobRef.t -> typeclass (** raises a UserError if not a class *) (** These raise a UserError if not a class. @@ -74,12 +80,12 @@ val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option -val instance_impl : instance -> global_reference +val instance_impl : instance -> GlobRef.t val hint_priority : instance -> int option -val is_class : global_reference -> bool -val is_instance : global_reference -> bool +val is_class : GlobRef.t -> bool +val is_instance : GlobRef.t -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) @@ -121,24 +127,24 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u val classes_transparent_state_hook : (unit -> transparent_state) Hook.t val classes_transparent_state : unit -> transparent_state -val add_instance_hint_hook : - (global_reference_or_constr -> global_reference list -> - bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t -val remove_instance_hint_hook : (global_reference -> unit) Hook.t -val add_instance_hint : global_reference_or_constr -> global_reference list -> - bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit -val remove_instance_hint : global_reference -> unit +val add_instance_hint_hook : + (global_reference_or_constr -> GlobRef.t list -> + bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t +val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t +val add_instance_hint : global_reference_or_constr -> GlobRef.t list -> + bool -> hint_info -> Decl_kinds.polymorphic -> unit +val remove_instance_hint : GlobRef.t -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit +val declare_instance : hint_info option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. check tells if we should check for existence of the subinstances and add only the missing ones. *) -val build_subclasses : check:bool -> env -> evar_map -> global_reference -> - Vernacexpr.hint_info_expr -> - (global_reference list * Vernacexpr.hint_info_expr * constr) list +val build_subclasses : check:bool -> env -> evar_map -> GlobRef.t -> + hint_info -> + (GlobRef.t list * hint_info * constr) list diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index e10c81c24..2720a3e4d 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,18 +9,16 @@ (************************************************************************) (*i*) +open Names open EConstr open Environ -open Constrexpr -open Globnames (*i*) type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * Misctypes.lident (* Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) + | UnboundMethod of GlobRef.t * lident (* Class name, method *) exception TypeClassError of env * typeclass_error @@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err)) let not_a_class env c = typeclass_error env (NotAClass c) let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) - -let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index d98295658..9831627a9 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,23 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open EConstr open Environ -open Constrexpr -open Globnames type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * Misctypes.lident (** Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) + | UnboundMethod of GlobRef.t * lident (** Class name, method *) exception TypeClassError of env * typeclass_error val not_a_class : env -> constr -> 'a -val unbound_method : env -> global_reference -> Misctypes.lident -> 'a - -val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a +val unbound_method : env -> GlobRef.t -> lident -> 'a diff --git a/pretyping/typing.ml b/pretyping/typing.ml index df189735b..cf34ac016 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -14,6 +14,7 @@ open Pp open CErrors open Util open Term +open Constr open Environ open EConstr open Vars @@ -29,113 +30,123 @@ let meta_type evd mv = let ty = try Evd.meta_ftype evd mv with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in - let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in + 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 (Constr.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 = @@ -148,39 +159,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 !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 = @@ -196,21 +209,20 @@ 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 } + 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 evdref = - 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 - Environ.env_of_pre_env penv' +let enrich_env env sigma = + set_universes env @@ Evd.universes sigma let check_fix env sigma pfix = - let inj c = EConstr.to_constr sigma c in + let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in let (idx, (ids, cs, ts)) = pfix in check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts)) @@ -271,165 +283,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 fe83a2cc8..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 @@ -55,4 +62,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment -val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f2f922fd5..5cf6e4b26 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -84,7 +84,7 @@ let occur_meta_or_undefined_evar evd c = | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with | Evar_defined c -> - occrec c; Array.iter occrec args + occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args | Evar_empty -> raise Occur) | _ -> Constr.iter occrec c in try occrec c; false with Occur | Not_found -> true @@ -189,18 +189,17 @@ let pose_all_metas_as_evars env evd t = let rec aux t = match EConstr.kind !evdref t with | Meta mv -> (match Evd.meta_opt_fvalue !evdref mv with - | Some ({rebus=c},_) -> EConstr.of_constr c + | Some ({rebus=c},_) -> c | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in - let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in let ty = if Flags.version_strictly_greater Flags.V8_6 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 (EConstr.Unsafe.to_constr 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 @@ -399,8 +398,13 @@ let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with modulo_betaiota = false; } -let default_no_delta_unify_flags () = - let flags = default_no_delta_core_unify_flags () in { +let default_no_delta_unify_flags ts = + let flags = default_no_delta_core_unify_flags () in + let flags = { flags with + modulo_conv_on_closed_terms = Some ts; + modulo_delta_types = ts + } in + { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = flags; @@ -466,7 +470,7 @@ let use_metas_pattern_unification sigma flags nb l = type key = | IsKey of CClosure.table_key - | IsProj of projection * EConstr.constr + | IsProj of Projection.t * EConstr.constr let expand_table_key env = function | ConstKey cst -> constant_opt_value_in env cst @@ -562,16 +566,16 @@ let is_rigid_head sigma flags t = | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = - let open Universes in - Constraints.fold + let open UnivProblem in + Set.fold (fun c acc -> let c' = match c with (* Should we be forcing weak constraints? *) | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r) | ULe _ | UEq _ -> c in - Constraints.add c' acc) - c Constraints.empty + Set.add c' acc) + c Set.empty let constr_cmp pb env sigma flags t u = let cstrs = @@ -580,16 +584,16 @@ let constr_cmp pb env sigma flags t u = in match cstrs with | Some cstrs -> - begin try Evd.add_universe_constraints sigma cstrs, true - with Univ.UniverseInconsistency _ -> sigma, false + begin try Some (Evd.add_universe_constraints sigma cstrs) + with Univ.UniverseInconsistency _ -> None | Evd.UniversesDiffer -> if is_rigid_head sigma flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), true - with Univ.UniverseInconsistency _ -> sigma, false - else sigma, false + try Some (Evd.add_universe_constraints sigma (force_eqs cstrs)) + with Univ.UniverseInconsistency _ -> None + else None end | None -> - sigma, false + None let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state @@ -624,9 +628,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM | None -> sigma | Some n -> if is_ground_term sigma m && is_ground_term sigma n then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in - if b then sigma - else error_cannot_unify env sigma (m,n) + match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with + | Some sigma -> sigma + | None -> error_cannot_unify env sigma (m,n) else sigma @@ -699,7 +703,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst else sigma,(k2,cM,stM)::metasubst,evarsubst | Meta k, _ - when not (dependent sigma cM cN) (* helps early trying alternatives *) -> + when not (occur_metavariable sigma k cN) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -719,7 +723,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k - when not (dependent sigma cN cM) (* helps early trying alternatives *) -> + when not (occur_metavariable sigma k cM) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -741,11 +745,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb env sigma flags cM cN in - if b then - sigma',metasubst,evarsubst - else + begin match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> + sigma, metasubst, evarsubst + | None -> sigma,metasubst,((curenv,ev,cN)::evarsubst) + end | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) && not (occur_evar sigma evk cN) -> @@ -838,6 +843,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e with ex when precatchable_exception ex -> reduce curenvnb pb opt substn cM cN) + | Fix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(_,tl2,bl2)) when + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + + | CoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(_,tl2,bl2)) when + Int.equal i1 i2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + | App (f1,l1), _ when (isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1 || use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) -> @@ -923,9 +948,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb env sigma flags cM cN in - if b then (sigma', metas, evars) - else + match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> (sigma, metas, evars) + | None -> try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = @@ -982,12 +1007,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (* Renounce, maybe metas/evars prevents typing *) sigma else sigma in - let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in - if b then Some (sigma, metasubst, evarsubst) - else - if is_ground_term sigma m1 && is_ground_term sigma n1 then - error_cannot_unify curenv sigma (cM,cN) - else None + match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with + | Some sigma -> + Some (sigma, metasubst, evarsubst) + | None -> + if is_ground_term sigma m1 && is_ground_term sigma n1 then + error_cannot_unify curenv sigma (cM,cN) + else None in match res with | Some substn -> substn @@ -1060,7 +1086,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (evd,t2::ks, m-1) else let mv = new_meta () in - let evd' = meta_declare mv (EConstr.Unsafe.to_constr (substl ks b)) evd in + let evd' = meta_declare mv (substl ks b) evd in (evd', mkMeta mv :: ks, m - 1)) (sigma,[],List.length bs) bs in @@ -1090,11 +1116,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e then None else - let sigma, b = match flags.modulo_conv_on_closed_terms with + let ans = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in - if b then Some sigma - else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with + match ans with + | Some sigma -> ans + | None -> + if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k | None,(dl_id, dl_k) -> @@ -1247,7 +1275,7 @@ 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 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 + let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in (evd',j'.uj_val) let w_coerce_to_type env evd c cty mvty = @@ -1359,11 +1387,11 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = if meta_defined evd mv then let {rebus=c'},(status',_) = meta_fvalue evd mv in let (take_left,st,(evd,metas',evars')) = - merge_instances env evd flags status' status (EConstr.of_constr c') c + merge_instances env evd flags status' status c' c in let evd' = if take_left then evd - else meta_reassign mv (EConstr.Unsafe.to_constr c,(st,TypeProcessed)) evd + else meta_reassign mv (c,(st,TypeProcessed)) evd in w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns else @@ -1372,7 +1400,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = if isMetaOf evd mv (whd_all env evd c) then evd else error_cannot_unify env evd (mkMeta mv,c) else - meta_assign mv (EConstr.Unsafe.to_constr c,(status,TypeProcessed)) evd in + meta_assign mv (c,(status,TypeProcessed)) evd in w_merge_rec evd' (metas''@metas) evars'' eqns | [] -> (* Process type eqns *) @@ -1392,21 +1420,21 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = and mimick_undefined_evar evd flags hdc nargs sp = let ev = Evd.find_undefined evd sp in - let sp_env = Global.env_of_context ev.evar_hyps in + let sp_env = Global.env_of_context (evar_filtered_hyps ev) in let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags - (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in + (get_type_of sp_env evd' c) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' - then Evd.define sp (EConstr.Unsafe.to_constr c) evd''' - else Evd.define sp (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in + then Evd.define sp c evd''' + else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in let check_types evd = let metas = Evd.meta_list evd in let eqns = List.fold_left (fun acc (mv, b) -> match b with - | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, EConstr.of_constr t.rebus) :: acc + | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc | _ -> acc) [] metas in w_merge_rec evd [] [] eqns in @@ -1417,11 +1445,6 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = in if with_types then check_types res else res -let retract_coercible_metas evd = - let (metas, evd) = retract_coercible_metas evd in - let map (mv, c, st) = (mv, EConstr.of_constr c, st) in - (List.map map metas, evd) - let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = let metas,evd = retract_coercible_metas evd in w_merge env true flags.merge_unify_flags (evd,metas,[]) @@ -1506,12 +1529,12 @@ let indirectly_dependent sigma c d decls = it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious way to see that the second hypothesis depends indirectly over 2 *) - List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls + let open Context.Named.Declaration in + List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in - let sigma, subst = nf_univ_variables sigma in - (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) + (sigma, nf_evar sigma c) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1589,8 +1612,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> - let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in - if b then Some (evd, c1, x) else raise (NotUnifiable None) + begin match infer_conv ~pb:CONV env evd c1 c2 with + | Some evd -> Some (evd, c1, x) + | None -> raise (NotUnifiable None) + end | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in @@ -1599,9 +1624,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = (fun test -> match test.testing_state with | None -> None | Some (sigma,_,l) -> - let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in - let univs, subst = nf_univ_variables sigma in - Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) + let c = applist (local_strong whd_meta sigma c, l) in + Some (sigma, c)) let make_eq_test env evd c = let out cstr = @@ -1908,10 +1932,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in - let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in - if not b then + match infer_conv ~pb:CUMUL env evd' predtyp typp with + | None -> error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; + | Some evd' -> w_merge env false flags.merge_unify_flags (evd',[p,pred,(Conv,TypeProcessed)],[]) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 16ce5c93d..e2e261ae7 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Constr open EConstr open Environ @@ -40,7 +41,7 @@ val default_core_unify_flags : unit -> core_unify_flags val default_no_delta_core_unify_flags : unit -> core_unify_flags val default_unify_flags : unit -> unify_flags -val default_no_delta_unify_flags : unit -> unify_flags +val default_no_delta_unify_flags : transparent_state -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml deleted file mode 100644 index 8864be576..000000000 --- a/pretyping/univdecls.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open CErrors - -(** Local universes and constraints declarations *) -type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl - -let default_univ_decl = - let open Misctypes in - { univdecl_instance = []; - univdecl_extensible_instance = true; - univdecl_constraints = Univ.Constraint.empty; - univdecl_extensible_constraints = true } - -let interp_univ_constraints env evd cstrs = - let interp (evd,cstrs) (u, d, u') = - let ul = Pretyping.interp_known_glob_level evd u in - let u'l = Pretyping.interp_known_glob_level evd u' in - let cstr = (ul,d,u'l) in - let cstrs' = Univ.Constraint.add cstr cstrs in - try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in - evd, cstrs' - with Univ.UniverseInconsistency e -> - user_err ~hdr:"interp_constraint" - (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) - in - List.fold_left interp (evd,Univ.Constraint.empty) cstrs - -let interp_univ_decl env decl = - let open Misctypes in - let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in - let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in - let decl = { univdecl_instance = pl; - univdecl_extensible_instance = decl.univdecl_extensible_instance; - univdecl_constraints = cstrs; - univdecl_extensible_constraints = decl.univdecl_extensible_constraints } - in evd, decl - -let interp_univ_decl_opt env l = - match l with - | None -> Evd.from_env env, default_univ_decl - | Some decl -> interp_univ_decl env decl diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli deleted file mode 100644 index 305d045b1..000000000 --- a/pretyping/univdecls.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Local universe and constraint declarations. *) -type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl - -val default_univ_decl : universe_decl - -val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr -> - Evd.evar_map * universe_decl - -val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> - Evd.evar_map * universe_decl diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 3c9b8bc33..14c9f49b1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -205,7 +205,7 @@ and nf_univ_args ~nb_univs mk env sigma stk = and nf_evar env sigma evk stk = let evi = try Evd.find sigma evk with Not_found -> assert false in let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in - let concl = Evd.evar_concl evi in + let concl = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in if List.is_empty hyps then nf_stk env sigma (mkEvar (evk, [||])) concl stk else match stk with @@ -266,7 +266,6 @@ and nf_stk ?from:(from=0) env sigma c t stk = let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma ind mib mip u params dep p in @@ -288,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> assert false + end + | _ -> + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in let name = Name (Id.of_string "c") in @@ -306,7 +314,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_val env sigma v crazy_type + | _ -> false, nf_val env sigma v crazy_type and nf_args env sigma vargs ?from:(f=0) t = let t = ref t in @@ -381,9 +389,9 @@ let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); (** This evar-normalizes terms beforehand *) - let c = EConstr.to_constr sigma c in - let t = EConstr.to_constr sigma t in - let v = Vconv.val_of_constr env c in + let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in + let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in + let v = Csymtable.val_of_constr env c in EConstr.of_constr (nf_val env sigma v t) let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = |