diff options
Diffstat (limited to 'pretyping')
42 files changed, 984 insertions, 433 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 84295959fb..9d4badc60a 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 65e3c3be56..6a776dc961 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 4c87b4e7ed..ee7c39982b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -295,8 +295,11 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = e_new_evar env evdref ~src:(hole_source n) ty' in - (e::subst,e::evarl,n+1) + let e = evd_comb1 + (Evarutil.new_evar env ~src:(hole_source n)) + evdref ty' + in + (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in (substl subst b::subst,evarl,n+1)) @@ -314,13 +317,15 @@ let try_find_ind env sigma typ realnames = IsInd (typ,ind,names) let inh_coerce_to_ind evdref env loc ty tyi = - let sigma = !evdref in + let orig = !evdref in let expected_typ = inductive_template evdref env loc tyi in (* Try to refine the type with inductive information coming from the constructor and renounce if not able to give more information *) (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) - if not (e_cumul env evdref expected_typ ty) then evdref := sigma + match cumul env !evdref expected_typ ty with + | Some sigma -> evdref := sigma + | None -> evdref := orig let binding_vars_of_inductive sigma = function | NotInd _ -> [] @@ -372,8 +377,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref !lvar tomatch in - let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in - evdref := evd; + let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in let typ = nf_evar !evdref j.uj_type in lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = @@ -396,12 +400,8 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e - -let evd_comb2 f evdref x y = - let (evd',y) = f !evdref x y in - evdref := evd'; - y + let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in + e let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the @@ -424,7 +424,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let current = if List.is_empty deps && isEvar !(pb.evdref) typ then (* Don't insert coercions if dependent; only solve evars *) - let _ = e_cumul pb.env pb.evdref indt typ in + let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in current else (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) @@ -1014,8 +1014,8 @@ let adjust_impossible_cases pb pred tomatch submat = begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin - let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk default.uj_type evd + let default = evd_comb0 use_unit_judge pb.evdref in + pb.evdref := Evd.define evk default.uj_type !(pb.evdref) end; add_assert_false_case pb tomatch | _ -> @@ -1681,7 +1681,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev' = e_new_evar env evdref ~src ty in + let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1712,7 +1712,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in + let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in lift k ev in aux (0,extenv,subst0) t0 @@ -1724,17 +1724,20 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = we are in an impossible branch *) let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in - let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in - (lift (n'-n) impossible_case_type, mkSort u) + let impossible_case_type, u = + evd_comb1 + (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)) + evdref univ_flexible_alg + in + (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.type_of extenv !evdref t in - evdref := evd; + let tt = evd_comb1 (Typing.type_of extenv) evdref t in (t,tt) in - let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type."); - { uj_val = t; uj_type = tt } + match cumul env !evdref tt (mkSort s) with + | None -> anomaly (Pp.str "Build_tycon: should be a type."); + | Some sigma -> evdref := sigma; + { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return @@ -1923,9 +1926,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in - evdref := evd'; - j + evd_comb2 (Coercion.inh_conv_coerce_to ?loc true env) evdref j p | None -> j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index a0804b72b2..7dbef01c22 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 f8600bbe02..35691ea37a 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 6dc3687a0a..c9c2445a73 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -48,31 +48,35 @@ exception NoCoercion exception NoCoercionNoUnifier of evar_map * unification_error (* Here, funj is a coercion therefore already typed in global context *) -let apply_coercion_args env evd check isproj argl funj = - let evdref = ref evd in - let rec apply_rec acc typ = function +let apply_coercion_args env sigma check isproj argl funj = + let rec apply_rec sigma acc typ = function | [] -> if isproj then - let cst = fst (destConst !evdref (j_val funj)) in + let cst = fst (destConst sigma (j_val funj)) in let p = Projection.make cst false in let pb = lookup_projection p env in let args = List.skipn pb.Declarations.proj_npars argl in let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in - { uj_val = applist (mkProj (p, hd), tl); - uj_type = typ } + sigma, { uj_val = applist (mkProj (p, hd), tl); + uj_type = typ } else - { uj_val = applist (j_val funj,argl); - uj_type = typ } + sigma, { uj_val = applist (j_val funj,argl); + uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) - match EConstr.kind !evdref (whd_all env !evdref typ) with + match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> - if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then - raise NoCoercion; - apply_rec (h::acc) (subst1 h c2) restl + let sigma = + if check then + begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with + | None -> raise NoCoercion + | Some sigma -> sigma + end + else sigma + in + apply_rec sigma (h::acc) (subst1 h c2) restl | _ -> anomaly (Pp.str "apply_coercion_args.") in - let res = apply_rec [] funj.uj_type argl in - !evdref, res + apply_rec sigma [] funj.uj_type argl (* appliquer le chemin de coercions de patterns p *) let apply_pattern_coercion ?loc pat p = @@ -94,7 +98,9 @@ open Program let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in - Evarutil.e_new_evar env evdref ~src c + let evd, v = Evarutil.new_evar env !evdref ~src c in + evdref := evd; + v let app_opt env evdref f t = whd_betaiota !evdref (app_opt f t) @@ -191,7 +197,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - Typing.e_solve_evars env evdref term) + let sigma, term = Typing.solve_evars env !evdref term in + evdref := sigma; term) in if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) @@ -337,8 +344,9 @@ let app_coercion env evdref coercion v = match coercion with | None -> v | Some f -> - let v' = Typing.e_solve_evars env evdref (f v) in - whd_betaiota !evdref v' + let sigma, v' = Typing.solve_evars env !evdref (f v) in + evdref := sigma; + whd_betaiota !evdref v' let coerce_itf ?loc env evd v t c1 = let evdref = ref evd in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 89d490a410..0ff6a330f6 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -20,7 +20,6 @@ open EConstr open Vars open Pattern open Patternops -open Misctypes open Context.Rel.Declaration open Ltac_pretype (*i*) @@ -277,6 +276,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 @@ -427,7 +427,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) ) @@ -451,7 +451,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 3c2c73915f..d19789ef42 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/constrexpr.ml b/pretyping/constrexpr.ml new file mode 100644 index 0000000000..1443dfb513 --- /dev/null +++ b/pretyping/constrexpr.ml @@ -0,0 +1,153 @@ +(************************************************************************) +(* * 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 +open Libnames +open Misctypes +open Decl_kinds + +(** {6 Concrete syntax for terms } *) + +(** [constr_expr] is the abstract syntax tree produced by the parser *) + +type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl + +type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option + +type notation = string + +type explicitation = + | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) + | ExplByName of Id.t + +type binder_kind = + | Default of binding_kind + | Generalized of binding_kind * binding_kind * bool + (** Inner binding, outer bindings, typeclass-specific flag + for implicit generalization of superclasses *) + +type abstraction_kind = AbsLambda | AbsPi + +type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) + +(** Representation of integer literals that appear in Coq scripts. + We now use raw strings of digits in base 10 (big-endian), and a separate + sign flag. Note that this representation is not unique, due to possible + multiple leading zeros, and -0 = +0 *) + +type sign = bool +type raw_natural_number = string + +type prim_token = + | Numeral of raw_natural_number * sign + | String of string + +type instance_expr = Glob_term.glob_level list + +type cases_pattern_expr_r = + | CPatAlias of cases_pattern_expr * lname + | CPatCstr of reference + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) + | CPatAtom of reference option + | CPatOr of cases_pattern_expr list + | CPatNotation of notation * cases_pattern_notation_substitution + * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents + (notation n applied with substitution l1) + applied to arguments l2 *) + | CPatPrim of prim_token + | CPatRecord of (reference * cases_pattern_expr) list + | CPatDelimiters of string * cases_pattern_expr + | CPatCast of cases_pattern_expr * constr_expr +and cases_pattern_expr = cases_pattern_expr_r CAst.t + +and cases_pattern_notation_substitution = + cases_pattern_expr list * (** for constr subterms *) + cases_pattern_expr list list (** for recursive notations *) + +and constr_expr_r = + | CRef of reference * instance_expr option + | CFix of lident * fix_expr list + | CCoFix of lident * cofix_expr list + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr + | CLetIn of lname * constr_expr * constr_expr option * constr_expr + | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list + | CApp of (proj_flag * constr_expr) * + (constr_expr * explicitation CAst.t option) list + | CRecord of (reference * constr_expr) list + + (* representation of the "let" and "match" constructs *) + | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) + * constr_expr option (* return-clause *) + * case_expr list + * branch_expr list (* branches *) + + | CLetTuple of lname list * (lname option * constr_expr option) * + constr_expr * constr_expr + | CIf of constr_expr * (lname option * constr_expr option) + * constr_expr * constr_expr + | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CPatVar of patvar + | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list + | CSort of Glob_term.glob_sort + | CCast of constr_expr * constr_expr cast_type + | CNotation of notation * constr_notation_substitution + | CGeneralization of binding_kind * abstraction_kind option * constr_expr + | CPrim of prim_token + | CDelimiters of string * constr_expr + | CProj of reference * constr_expr +and constr_expr = constr_expr_r CAst.t + +and case_expr = constr_expr (* expression that is being matched *) + * lname option (* as-clause *) + * cases_pattern_expr option (* in-clause *) + +and branch_expr = + (cases_pattern_expr list list * constr_expr) CAst.t + +and fix_expr = + lident * (lident option * recursion_order_expr) * + local_binder_expr list * constr_expr * constr_expr + +and cofix_expr = + lident * local_binder_expr list * constr_expr * constr_expr + +and recursion_order_expr = + | CStructRec + | CWfRec of constr_expr + | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) + +(* Anonymous defs allowed ?? *) +and local_binder_expr = + | CLocalAssum of lname list * binder_kind * constr_expr + | CLocalDef of lname * constr_expr * constr_expr option + | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t + +and constr_notation_substitution = + constr_expr list * (** for constr subterms *) + constr_expr list list * (** for recursive notations *) + cases_pattern_expr list * (** for binders *) + local_binder_expr list list (** for binder lists (recursive notations) *) + +type constr_pattern_expr = constr_expr + +(** Concrete syntax for modules and module types *) + +type with_declaration_ast = + | CWith_Module of Id.t list CAst.t * qualid CAst.t + | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr + +type module_ast_r = + | CMident of qualid + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast +and module_ast = module_ast_r CAst.t diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bb563220b6..7795084779 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -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 @@ -920,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) ) @@ -940,7 +940,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') @@ -957,25 +957,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'))) @@ -985,14 +985,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 @@ -1000,12 +1000,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 @@ -1018,7 +1018,7 @@ 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) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 817b8ba6e8..5310455fe6 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 diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 144166a343..062136ff52 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) @@ -210,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 @@ -1159,17 +1159,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let subst = make_subst (ctxt,Array.to_list args,argoccs) in - let evdref = ref evd in - let rhs = set_holes evdref rhs subst in - let evd = !evdref in + let evd, rhs = + let evdref = ref evd in + let rhs = set_holes evdref rhs subst in + !evdref, rhs + in (* We instantiate the evars of which the value is forced by typing *) let evd,rhs = - let evdref = ref evd in - try let c = !solve_evars env_evar evdref rhs in !evdref,c + try !solve_evars env_evar evd rhs with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise (TypingFailed !evdref) in + raise (TypingFailed evd) in let rec abstract_free_holes evd = function | (id,idty,c,_,evsref,_,_)::l -> @@ -1394,6 +1395,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) +let make_opt = function + | Success evd -> Some evd + | UnifFailure _ -> None + +let conv env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CONV t1 t2) + +let cumul env ?(ts=default_transparent_state env) evd t1 t2 = + make_opt(evar_conv_x ts env evd CUMUL t1 t2) + let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CONV t1 t2 with | Success evd' -> evdref := evd'; true diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9270d6e3aa..cdf5dd0e50 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -28,7 +28,13 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma (** The same function resolving evars by side-effect and catching the exception *) val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.conv]"] + val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.cumul]"] + +val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option (** {6 Unification heuristics. } *) @@ -63,7 +69,7 @@ val second_order_matching : transparent_state -> env -> evar_map -> (** Declare function to enforce evars resolution by using typing constraints *) -val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit +val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result diff --git a/pretyping/genredexpr.ml b/pretyping/genredexpr.ml new file mode 100644 index 0000000000..80697461a6 --- /dev/null +++ b/pretyping/genredexpr.ml @@ -0,0 +1,66 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** Reduction expressions *) + +(** The parsing produces initially a list of [red_atom] *) + +type 'a red_atom = + | FBeta + | FMatch + | FFix + | FCofix + | FZeta + | FConst of 'a list + | FDeltaBut of 'a list + +(** This list of atoms is immediately converted to a [glob_red_flag] *) + +type 'a glob_red_flag = { + rBeta : bool; + rMatch : bool; + rFix : bool; + rCofix : bool; + rZeta : bool; + rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) + rConst : 'a list +} + +(** Generic kinds of reductions *) + +type ('a,'b,'c) red_expr_gen = + | Red of bool + | Hnf + | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option + | Cbv of 'b glob_red_flag + | Cbn of 'b glob_red_flag + | Lazy of 'b glob_red_flag + | Unfold of 'b Locus.with_occurrences list + | Fold of 'a list + | Pattern of 'a Locus.with_occurrences list + | ExtraRedExpr of string + | CbvVm of ('b,'c) Util.union Locus.with_occurrences option + | CbvNative of ('b,'c) Util.union Locus.with_occurrences option + +type ('a,'b,'c) may_eval = + | ConstrTerm of 'a + | ConstrEval of ('a,'b,'c) red_expr_gen * 'a + | ConstrContext of Misctypes.lident * 'a + | ConstrTypeOf of 'a + +open Libnames +open Constrexpr +open Misctypes + +type r_trm = constr_expr +type r_pat = constr_pattern_expr +type r_cst = reference or_by_notation + +type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index e89bbf7c34..5056c0457e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -113,7 +113,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 @@ -331,19 +331,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 +355,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 +366,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 *) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml new file mode 100644 index 0000000000..6ecb479e6f --- /dev/null +++ b/pretyping/glob_term.ml @@ -0,0 +1,131 @@ +(************************************************************************) +(* * 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 +open Misctypes + +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 + +(** 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 * 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 3327c250d7..40f4d4ff89 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -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 119ff52223..d87a19d282 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/locus.ml b/pretyping/locus.ml new file mode 100644 index 0000000000..95a2e495be --- /dev/null +++ b/pretyping/locus.ml @@ -0,0 +1,96 @@ +(************************************************************************) +(* * 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 +open Misctypes + +(** Locus : positions in hypotheses and goals *) + +(** {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/miscops.ml b/pretyping/miscops.ml index 0f0af5409e..1b536bfda3 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -29,7 +29,7 @@ let smartmap_cast_type f c = (** Equalities on [glob_sort] *) -let glob_sort_eq g1 g2 = match g1, g2 with +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 -> diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index abe817fe53..1d45045414 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -18,7 +18,7 @@ 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 +val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool (** Equalities on [intro_pattern_naming] *) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml new file mode 100644 index 0000000000..996a2dc36a --- /dev/null +++ b/pretyping/pattern.ml @@ -0,0 +1,42 @@ +(************************************************************************) +(* * 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 +open Misctypes + +(** {5 Patterns} *) + +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 existential_key * 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 27e457e3b3..375ed10d0d 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -30,7 +30,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 @@ -293,11 +293,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) -> @@ -312,7 +312,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') @@ -326,7 +326,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 @@ -334,18 +334,18 @@ 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 (lni,(lna,tl,bl)) -> - let tl' = Array.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + 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.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + 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')) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 9f0878578a..dfbfb147f2 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -8,12 +8,12 @@ (* * (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 +32,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/pretyping.ml b/pretyping/pretyping.ml index 947469ca0e..de72f94272 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 415c4e1722..73f5b77e0e 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 ae4ad0be7d..c48decdb08 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,5 +1,5 @@ Geninterp -Ltac_pretype +Locus Locusops Pretype_errors Reductionops @@ -16,9 +16,14 @@ Evarsolve Recordops Evarconv Typing +Constrexpr +Genredexpr Miscops +Glob_term +Ltac_pretype Glob_ops Redops +Pattern Patternops Constr_matching Tacred diff --git a/pretyping/program.ml b/pretyping/program.ml index 52d940d8eb..8cfb7966cb 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 df0848ba16..a8f5115788 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 d070edead1..9eb410f06a 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 diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 1f7b23c0c0..748f053b2f 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/reductionops.ml b/pretyping/reductionops.ml index 244b8e60b1..6fde868370 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 @@ -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) -> @@ -1404,7 +1404,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 +1413,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')) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b8ac085a7a..ad280d9f37 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 -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 696001ab77..5a47acd22e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -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 aa7604f53d..e6065dda87 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 30ddeffa69..12a944d322 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_expr = Constrexpr.constr_pattern_expr 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_expr) 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_expr; (* 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 = @@ -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 b80c287117..2a8e0b8748 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_expr = Constrexpr.constr_pattern_expr 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_expr) 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_expr -> 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_expr -> 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_expr -> 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_expr 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_expr -> + (GlobRef.t list * hint_info_expr * constr) list diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index e10c81c24a..89c5d7e7b4 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,17 +9,17 @@ (************************************************************************) (*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 *) + | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *) | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index d98295658f..4aabc0aee1 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,23 +8,23 @@ (* * (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 *) + | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *) | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) exception TypeClassError of env * typeclass_error val not_a_class : env -> constr -> 'a -val unbound_method : env -> global_reference -> Misctypes.lident -> 'a +val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/pretyping/typing.ml b/pretyping/typing.ml index aaec73f045..6bd75c93d5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -37,104 +37,115 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl = let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp -let e_type_judgment env evdref j = - match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s } +let type_judgment env sigma j = + match EConstr.kind sigma (whd_all env sigma j.uj_type) with + | Sort s -> sigma, {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | Evar ev -> - let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in - evdref := evd; { utj_val = j.uj_val; utj_type = s } - | _ -> error_not_a_type env !evdref j - -let e_assumption_of_judgment env evdref j = - try (e_type_judgment env evdref j).utj_val + let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in + sigma, { utj_val = j.uj_val; utj_type = s } + | _ -> error_not_a_type env sigma j + +let assumption_of_judgment env sigma j = + try + let sigma, j = type_judgment env sigma j in + sigma, j.utj_val with Type_errors.TypeError _ | PretypeError _ -> - error_assumption env !evdref j + error_assumption env sigma j -let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv = - let rec apply_rec n typ = function +let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = + let rec apply_rec sigma n typ = function | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = - let ar = inductive_type_knowing_parameters env !evdref ind argjv in - hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) } + sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = + let ar = inductive_type_knowing_parameters env sigma ind argjv in + hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) } | hj::restjl -> - let (c1,c2) = - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> (c1,c2) + let sigma, (c1,c2) = + match EConstr.kind sigma (whd_all env sigma typ) with + | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,c1,c2) = destProd evd' t in - (c1,c2) + let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (_,c1,c2) = destProd sigma t in + sigma, (c1,c2) | _ -> - error_cant_apply_not_functional env !evdref funj argjv + error_cant_apply_not_functional env sigma funj argjv in - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + begin match Evarconv.cumul env sigma hj.uj_type c1 with + | Some sigma -> + apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl + | None -> + error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv + end in - apply_rec 1 funj.uj_type (Array.to_list argjv) + apply_rec sigma 1 funj.uj_type (Array.to_list argjv) -let e_judge_of_apply env evdref funj argjv = - let rec apply_rec n typ = function +let judge_of_apply env sigma funj argjv = + let rec apply_rec sigma n typ = function | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } + sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = typ } | hj::restjl -> - let (c1,c2) = - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> (c1,c2) + let sigma, (c1,c2) = + match EConstr.kind sigma (whd_all env sigma typ) with + | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,c1,c2) = destProd evd' t in - (c1,c2) + let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (_,c1,c2) = destProd sigma t in + sigma, (c1,c2) | _ -> - error_cant_apply_not_functional env !evdref funj argjv + error_cant_apply_not_functional env sigma funj argjv in - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + begin match Evarconv.cumul env sigma hj.uj_type c1 with + | Some sigma -> + apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl + | None -> + error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv + end in - apply_rec 1 funj.uj_type (Array.to_list argjv) + apply_rec sigma 1 funj.uj_type (Array.to_list argjv) -let e_check_branch_types env evdref (ind,u) cj (lfj,explft) = +let check_branch_types env sigma (ind,u) cj (lfj,explft) = if not (Int.equal (Array.length lfj) (Array.length explft)) then - error_number_branches env !evdref cj (Array.length explft); - for i = 0 to Array.length explft - 1 do - if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then - error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) - done + error_number_branches env sigma cj (Array.length explft); + Array.fold_left2_i (fun i sigma lfj explft -> + match Evarconv.cumul env sigma lfj.uj_type explft with + | Some sigma -> sigma + | None -> + error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft) + sigma lfj explft let max_sort l = if Sorts.List.mem InType l then InType else if Sorts.List.mem InSet l then InSet else InProp -let e_is_correct_arity env evdref c pj ind specif params = - let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in +let is_correct_arity env sigma c pj ind specif params = + let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in - let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in - let rec srec env pt ar = - let pt' = whd_all env !evdref pt in - match EConstr.kind !evdref pt', ar with + let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in + let rec srec env sigma pt ar = + let pt' = whd_all env sigma pt in + match EConstr.kind sigma pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - if not (Evarconv.e_cumul env evdref a1 a1') then error (); - srec (push_rel (LocalAssum (na1,a1)) env) t ar' + begin match Evarconv.cumul env sigma a1 a1' with + | None -> error () + | Some sigma -> + srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar' + end | Sort s, [] -> - let s = ESorts.kind !evdref s in + let s = ESorts.kind sigma s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () + else sigma | Evar (ev,_), [] -> - let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in - evdref := Evd.define ev (mkSort s) evd + let sigma, s = Evd.fresh_sort_in_family env sigma (max_sort allowed_sorts) in + let sigma = Evd.define ev (mkSort s) sigma in + sigma | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' + srec (push_rel d env) sigma (lift 1 pt') ar' | _ -> error () in - srec env pj.uj_type (List.rev arsign) + srec env sigma pj.uj_type (List.rev arsign) let lambda_applist_assum sigma n c l = let rec app n subst t l = @@ -147,39 +158,41 @@ let lambda_applist_assum sigma n c l = | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l -let e_type_case_branches env evdref (ind,largs) pj c = +let type_case_branches env sigma (ind,largs) pj c = let specif = lookup_mind_specif env (fst ind) in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let params = List.map EConstr.Unsafe.to_constr params in - let () = e_is_correct_arity env evdref c pj ind specif params in - let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in + let sigma = is_correct_arity env sigma c pj ind specif params in + let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in - let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in - (lc, ty) + let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in + sigma, (lc, ty) -let e_judge_of_case env evdref ci pj cj lfj = +let judge_of_case env sigma ci pj cj lfj = let ((ind, u), spec) = - try find_mrectype env !evdref cj.uj_type - with Not_found -> error_case_not_inductive env !evdref cj in - let indspec = ((ind, EInstance.kind !evdref u), spec) in + try find_mrectype env sigma cj.uj_type + with Not_found -> error_case_not_inductive env sigma cj in + let indspec = ((ind, EInstance.kind sigma u), spec) in let _ = check_case_info env (fst indspec) ci in - let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in - e_check_branch_types env evdref (fst indspec) cj (lfj,bty); - { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); - uj_type = rslty } + let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in + let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in + sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); + uj_type = rslty } -let check_type_fixpoint ?loc env evdref lna lar vdefj = +let check_type_fixpoint ?loc env sigma lna lar vdefj = let lt = Array.length vdefj in - if Int.equal (Array.length lar) lt then - for i = 0 to lt-1 do - if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body ?loc env !evdref - i lna vdefj lar - done + assert (Int.equal (Array.length lar) lt); + Array.fold_left2_i (fun i sigma defj ar -> + match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with + | Some sigma -> sigma + | None -> + error_ill_typed_rec_body ?loc env sigma + i lna vdefj lar) + sigma vdefj lar + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = @@ -192,17 +205,19 @@ let check_allowed_sort env sigma ind c p = error_elim_arity env sigma ind sorts c pj (Some(ksort,s,Type_errors.error_elim_explain ksort s)) -let e_judge_of_cast env evdref cj k tj = +let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then - error_actual_type_core env !evdref cj expected_type; - { uj_val = mkCast (cj.uj_val, k, expected_type); - uj_type = expected_type } - -let enrich_env env evdref = + match Evarconv.cumul env sigma cj.uj_type expected_type with + | None -> + error_actual_type_core env sigma cj expected_type; + | Some sigma -> + sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } + +let enrich_env env sigma = let penv = Environ.pre_env env in let penv' = Pre_env.({ penv with env_stratification = - { penv.env_stratification with env_universes = Evd.universes !evdref } }) in + { penv.env_stratification with env_universes = Evd.universes sigma } }) in Environ.env_of_pre_env penv' let check_fix env sigma pfix = @@ -267,165 +282,167 @@ let judge_of_letin env name defj typj j = (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) -let rec execute env evdref cstr = - let cstr = whd_evar !evdref cstr in - match EConstr.kind !evdref cstr with +let rec execute env sigma cstr = + let cstr = whd_evar sigma cstr in + match EConstr.kind sigma cstr with | Meta n -> - { uj_val = cstr; uj_type = meta_type !evdref n } + sigma, { uj_val = cstr; uj_type = meta_type sigma n } | Evar ev -> - let ty = EConstr.existential_type !evdref ev in - let jty = execute env evdref ty in - let jty = e_assumption_of_judgment env evdref jty in - { uj_val = cstr; uj_type = jty } + let ty = EConstr.existential_type sigma ev in + let sigma, jty = execute env sigma ty in + let sigma, jty = assumption_of_judgment env sigma jty in + sigma, { uj_val = cstr; uj_type = jty } | Rel n -> - judge_of_relative env n + sigma, judge_of_relative env n | Var id -> - judge_of_variable env id + sigma, judge_of_variable env id | Const (c, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) | Ind (ind, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) | Construct (cstruct, u) -> - let u = EInstance.kind !evdref u in - make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) + let u = EInstance.kind sigma u in + sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) | Case (ci,p,c,lf) -> - let cj = execute env evdref c in - let pj = execute env evdref p in - let lfj = execute_array env evdref lf in - e_judge_of_case env evdref ci pj cj lfj + let sigma, cj = execute env sigma c in + let sigma, pj = execute env sigma p in + let sigma, lfj = execute_array env sigma lf in + judge_of_case env sigma ci pj cj lfj | Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evdref recdef in + let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in let fix = (vni,recdef') in - check_fix env !evdref fix; - make_judge (mkFix fix) tys.(i) + check_fix env sigma fix; + sigma, make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evdref recdef in + let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in let cofix = (i,recdef') in - check_cofix env !evdref cofix; - make_judge (mkCoFix cofix) tys.(i) + check_cofix env sigma cofix; + sigma, make_judge (mkCoFix cofix) tys.(i) | Sort s -> - begin match ESorts.kind !evdref s with + begin match ESorts.kind sigma s with | Prop c -> - judge_of_prop_contents c + sigma, judge_of_prop_contents c | Type u -> - judge_of_type u + sigma, judge_of_type u end | Proj (p, c) -> - let cj = execute env evdref c in - judge_of_projection env !evdref p cj + let sigma, cj = execute env sigma c in + sigma, judge_of_projection env sigma p cj | App (f,args) -> - let jl = execute_array env evdref args in - (match EConstr.kind !evdref f with + let sigma, jl = execute_array env sigma args in + (match EConstr.kind sigma f with | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> - let fj = execute env evdref f in - e_judge_of_applied_inductive_knowing_parameters env evdref fj (ind, u) jl + let sigma, fj = execute env sigma f in + judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl | _ -> (* No template polymorphism *) - let fj = execute env evdref f in - e_judge_of_apply env evdref fj jl) + let sigma, fj = execute env sigma f in + judge_of_apply env sigma fj jl) | Lambda (name,c1,c2) -> - let j = execute env evdref c1 in - let var = e_type_judgment env evdref j in + let sigma, j = execute env sigma c1 in + let sigma, var = type_judgment env sigma j in let env1 = push_rel (LocalAssum (name, var.utj_val)) env in - let j' = execute env1 evdref c2 in - judge_of_abstraction env1 name var j' + let sigma, j' = execute env1 sigma c2 in + sigma, judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> - let j = execute env evdref c1 in - let varj = e_type_judgment env evdref j in + let sigma, j = execute env sigma c1 in + let sigma, varj = type_judgment env sigma j in let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in - let j' = execute env1 evdref c2 in - let varj' = e_type_judgment env1 evdref j' in - judge_of_product env name varj varj' + let sigma, j' = execute env1 sigma c2 in + let sigma, varj' = type_judgment env1 sigma j' in + sigma, judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> - let j1 = execute env evdref c1 in - let j2 = execute env evdref c2 in - let j2 = e_type_judgment env evdref j2 in - let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in + let sigma, j1 = execute env sigma c1 in + let sigma, j2 = execute env sigma c2 in + let sigma, j2 = type_judgment env sigma j2 in + let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in - let j3 = execute env1 evdref c3 in - judge_of_letin env name j1 j2 j3 + let sigma, j3 = execute env1 sigma c3 in + sigma, judge_of_letin env name j1 j2 j3 | Cast (c,k,t) -> - let cj = execute env evdref c in - let tj = execute env evdref t in - let tj = e_type_judgment env evdref tj in - e_judge_of_cast env evdref cj k tj - -and execute_recdef env evdref (names,lar,vdef) = - let larj = execute_array env evdref lar in - let lara = Array.map (e_assumption_of_judgment env evdref) larj in + let sigma, cj = execute env sigma c in + let sigma, tj = execute env sigma t in + let sigma, tj = type_judgment env sigma tj in + judge_of_cast env sigma cj k tj + +and execute_recdef env sigma (names,lar,vdef) = + let sigma, larj = execute_array env sigma lar in + let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 evdref vdef in + let sigma, vdefj = execute_array env1 sigma vdef in let vdefv = Array.map j_val vdefj in - let _ = check_type_fixpoint env1 evdref names lara vdefj in - (names,lara,vdefv) + let sigma = check_type_fixpoint env1 sigma names lara vdefj in + sigma, (names,lara,vdefv) -and execute_array env evdref = Array.map (execute env evdref) +and execute_array env = Array.fold_left_map (execute env) + +let check env sigma c t = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + match Evarconv.cumul env sigma j.uj_type t with + | None -> + error_actual_type_core env sigma j t + | Some sigma -> sigma let e_check env evdref c t = - let env = enrich_env env evdref in - let j = execute env evdref c in - if not (Evarconv.e_cumul env evdref j.uj_type t) then - error_actual_type_core env !evdref j t + evdref := check env !evdref c t (* Type of a constr *) -let unsafe_type_of env evd c = - let evdref = ref evd in - let env = enrich_env env evdref in - let j = execute env evdref c in - j.uj_type +let unsafe_type_of env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + j.uj_type (* Sort of a type *) +let sort_of env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in + let sigma, a = type_judgment env sigma j in + sigma, a.utj_type + let e_sort_of env evdref c = - let env = enrich_env env evdref in - let j = execute env evdref c in - let a = e_type_judgment env evdref j in - a.utj_type + Evarutil.evd_comb1 (sort_of env) evdref c (* Try to solve the existential variables by typing *) -let type_of ?(refresh=false) env evd c = - let evdref = ref evd in - let env = enrich_env env evdref in - let j = execute env evdref c in +let type_of ?(refresh=false) env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type - else !evdref, j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type + else sigma, j.uj_type + +let e_type_of ?refresh env evdref c = + Evarutil.evd_comb1 (type_of ?refresh env) evdref c -let e_type_of ?(refresh=false) env evdref c = - let env = enrich_env env evdref in - let j = execute env evdref c in +let solve_evars env sigma c = + let env = enrich_env env sigma in + let sigma, j = execute env sigma c in (* side-effect on evdref *) - if refresh then - let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in - let () = evdref := evd in - c - else j.uj_type + sigma, nf_evar sigma j.uj_val let e_solve_evars env evdref c = - let env = enrich_env env evdref in - let c = (execute env evdref c).uj_val in - (* side-effect on evdref *) - nf_evar !evdref c + Evarutil.evd_comb1 (solve_evars env) evdref c -let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c) +let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 4905adf1f3..3cf43ace01 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -26,18 +26,25 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Variant of [type_of] using references instead of state-passing. *) val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types +[@@ocaml.deprecated "Use [Typing.type_of]"] (** Typecheck a type and return its sort *) +val sort_of : env -> evar_map -> types -> evar_map * Sorts.t val e_sort_of : env -> evar_map ref -> types -> Sorts.t +[@@ocaml.deprecated "Use [Typing.sort_of]"] (** Typecheck a term has a given type (assuming the type is OK) *) +val check : env -> evar_map -> constr -> types -> evar_map val e_check : env -> evar_map ref -> constr -> types -> unit +[@@ocaml.deprecated "Use [Typing.check]"] (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) +val solve_evars : env -> evar_map -> constr -> evar_map * constr val e_solve_evars : env -> evar_map ref -> constr -> constr +[@@ocaml.deprecated "Use [Typing.solve_evars]"] (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) @@ -46,8 +53,8 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> (** Raise an error message if bodies have types not unifiable with the expected ones *) -val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref -> - Names.Name.t array -> types array -> unsafe_judgment array -> unit +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> + Names.Name.t array -> types array -> unsafe_judgment array -> evar_map val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d98ce9abab..62bee5a362 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -198,8 +198,8 @@ let pose_all_metas_as_evars env evd t = then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in - let ev = Evarutil.e_new_evar env evdref ~src ty in - evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; + let evd, ev = Evarutil.new_evar env !evdref ~src ty in + evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd; ev) | _ -> EConstr.map !evdref aux t in @@ -561,16 +561,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 = @@ -1504,8 +1504,7 @@ let indirectly_dependent sigma 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 { @@ -1593,9 +1592,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 = |