diff options
Diffstat (limited to 'pretyping')
50 files changed, 776 insertions, 545 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ea33f1c0d..d59102b6c 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -10,6 +10,7 @@ open Names open Globnames open Term +open Constr open Environ open Util open Libobject @@ -103,7 +104,7 @@ let rename_type_of_constructor env cstruct = let rename_typing env c = let j = Typeops.infer env c in let j' = - match kind_of_term c with + match kind c with | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) } | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) } | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) } diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 804e38216..b499da3ab 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -9,7 +9,7 @@ open Names open Globnames open Environ -open Term +open Constr val rename_arguments : bool -> global_reference -> Name.t list -> unit diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aefa09dbe..1207c967b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -13,7 +13,7 @@ open CErrors open Util open Names open Nameops -open Term +open Constr open Termops open Environ open EConstr @@ -1014,7 +1014,7 @@ let adjust_impossible_cases pb pred tomatch submat = this means that the Evd.define below may redefine an already defined evar. See e.g. first definition of test for bug #3388. *) let pred = EConstr.Unsafe.to_constr pred in - begin match kind_of_term pred with + 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 @@ -1566,11 +1566,9 @@ substituer après par les initiaux *) (* builds the matrix of equations testing that each eqn has n patterns * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) + * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,(ids,lpat,rhs)) = - let initial_lpat,initial_rhs = lpat,rhs in - let initial_rhs = rhs in + let build_eqn (loc,(ids,initial_lpat,initial_rhs)) = let avoid = ids_of_named_context_val (named_context_val env) in let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index cbf5788e4..43dbc3105 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -7,14 +7,14 @@ (************************************************************************) open Names -open Term +open Constr open Evd open Environ open EConstr open Inductiveops open Glob_term -open Evarutil open Ltac_pretype +open Evardefine (** {5 Compilation of pattern-matching } *) @@ -116,7 +116,7 @@ type 'a pattern_matching_problem = val compile : 'a pattern_matching_problem -> unsafe_judgment val prepare_predicate : ?loc:Loc.t -> - (Evarutil.type_constraint -> + (type_constraint -> Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> @@ -124,7 +124,7 @@ val prepare_predicate : ?loc:Loc.t -> (types * tomatch_type) list -> (rel_context * rel_context) list -> constr option -> - glob_constr option -> (Evd.evar_map * Names.name list * constr) list + glob_constr option -> (Evd.evar_map * Name.t list * constr) list -val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name -> +val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t -> Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 19d61a64d..192eca63b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -8,7 +8,7 @@ open Util open Names -open Term +open Constr open Vars open CClosure open Esubst @@ -45,7 +45,7 @@ type cbv_value = | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array - | CONSTR of constructor puniverses * cbv_value array + | CONSTR of constructor Univ.puniverses * cbv_value array (* type of terms with a hole. This hole can appear only under App or Case. * TOP means the term is considered without context @@ -208,25 +208,32 @@ and reify_value = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (reify_stack (reify_value v) stk) | CBN(t,env) -> - t - (* map_constr_with_binders subs_lift (cbv_norm_term) env t *) - | LAM (n,ctxt,b,env) -> - List.fold_left (fun c (n,t) -> Term.mkLambda (n, t, c)) b ctxt + apply_env env t + | LAM (k,ctxt,b,env) -> + apply_env env @@ + List.fold_left (fun c (n,t) -> + mkLambda (n, t, c)) b ctxt | FIXP ((lij,(names,lty,bds)),env,args) -> - mkApp - (mkFix (lij, - (names, - lty, - bds)), - Array.map reify_value args) + let fix = mkFix (lij, (names, lty, bds)) in + mkApp (apply_env env fix, Array.map reify_value args) | COFIXP ((j,(names,lty,bds)),env,args) -> - mkApp - (mkCoFix (j, - (names,lty,bds)), - Array.map reify_value args) + let cofix = mkCoFix (j, (names,lty,bds)) in + mkApp (apply_env env cofix, Array.map reify_value args) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map reify_value args) +and apply_env env t = + match kind t with + | Rel i -> + begin match expand_rel i env with + | Inl (k, v) -> + reify_value (shift_value k v) + | Inr (k,_) -> + mkRel k + end + | _ -> + map_with_binders subs_lift apply_env env t + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -240,7 +247,7 @@ and reify_value = function (* reduction under binders *) let rec norm_head info env t stack = (* no reduction under binders *) - match kind_of_term t with + match kind t with (* stack grows (remove casts) *) | App (head,args) -> (* Applied terms are normalized immediately; they could be computed when getting out of the stack *) @@ -290,11 +297,14 @@ let rec norm_head info env t stack = | Evar ev -> (match evar_value info.infos.i_cache ev with Some c -> norm_head info env c stack - | None -> (VAL(0, t), stack)) + | None -> + let e, xs = ev in + let xs' = Array.map (apply_env env) xs in + (VAL(0, mkEvar (e,xs')), stack)) (* non-neutral cases *) | Lambda _ -> - let ctxt,b = decompose_lam t in + let ctxt,b = Term.decompose_lam t in (LAM(List.length ctxt, List.rev ctxt,b,env), stack) | Fix fix -> (FIXP(fix,env,[||]), stack) | CoFix cofix -> (COFIXP(cofix,env,[||]), stack) @@ -411,12 +421,12 @@ and cbv_norm_value info = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (apply_stack info (cbv_norm_value info v) stk) | CBN(t,env) -> - map_constr_with_binders subs_lift (cbv_norm_term info) env t + Constr.map_with_binders subs_lift (cbv_norm_term info) env t | LAM (n,ctxt,b,env) -> let nctxt = List.map_i (fun i (x,ty) -> (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in - compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) + Term.compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) | FIXP ((lij,(names,lty,bds)),env,args) -> mkApp (mkFix (lij, diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 3ee7bebf0..1d4c88ea2 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -24,7 +24,7 @@ val cbv_norm : cbv_infos -> constr -> constr (*********************************************************************** i This is for cbv debug *) -open Term +open Constr type cbv_value = | VAL of int * constr @@ -33,7 +33,7 @@ type cbv_value = | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array - | CONSTR of constructor puniverses * cbv_value array + | CONSTR of constructor Univ.puniverses * cbv_value array and cbv_stack = | TOP diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 260cd0444..6d5ee504e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -10,12 +10,12 @@ open CErrors open Util open Pp open Names +open Constr open Libnames open Globnames open Nametab open Environ open Libobject -open Term open Mod_subst (* usage qque peu general: utilise aussi dans record *) @@ -27,9 +27,9 @@ type cl_typ = | CL_SORT | CL_FUN | CL_SECVAR of variable - | CL_CONST of constant + | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of constant + | CL_PROJ of Constant.t type cl_info_typ = { cl_param : int @@ -43,7 +43,7 @@ type coe_info_typ = { coe_value : constr; coe_type : types; coe_local : bool; - coe_context : Univ.universe_context_set; + coe_context : Univ.ContextSet.t; coe_is_identity : bool; coe_is_projection : bool; coe_param : int } @@ -59,8 +59,8 @@ let coe_info_typ_equal c1 c2 = let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 - | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2 + | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2 | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 | _ -> Pervasives.compare t1 t2 (** OK *) @@ -322,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) +let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ _ _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path x = !path_printer x +let print_path env sigma x = !path_printer env sigma x -let message_ambig l = - (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path ijp) l) +let message_ambig env sigma l = + str"Ambiguous paths:" ++ spc () ++ + prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -344,8 +344,8 @@ let different_class_params i = | CL_IND i -> Global.is_polymorphic (IndRef i) | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false - -let add_coercion_in_graph (ic,source,target) = + +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig !ambig_paths) + Feedback.msg_info (message_ambig env sigma !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -433,13 +433,13 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_, c) = +let cache_coercion env sigma (_, c) = let () = add_class c.coercion_source in 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 (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let value, ctx = Universes.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 = { coe_value = value; @@ -450,15 +450,15 @@ let cache_coercion (_, c) = coe_is_projection = c.coercion_is_proj; coe_param = c.coercion_params } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) + add_coercion_in_graph env sigma (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let open_coercion i o = if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -497,7 +497,9 @@ let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; - cache_function = cache_coercion; + cache_function = (fun objn -> + let env = Global.env () in cache_coercion env Evd.empty objn + ); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 8707078b5..47b41f17b 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -17,9 +17,9 @@ type cl_typ = | CL_SORT | CL_FUN | CL_SECVAR of variable - | CL_CONST of constant + | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of constant + | CL_PROJ of Constant.t (** Equality over [cl_typ] *) val cl_typ_eq : cl_typ -> cl_typ -> bool @@ -96,7 +96,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ddef1cee9..ec7c3077f 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -12,9 +12,7 @@ open CErrors open Util open Names open Globnames -open Nameops open Termops -open Reductionops open Term open EConstr open Vars @@ -55,7 +53,7 @@ exception PatternMatchingFailure let warn_meta_collision = CWarnings.create ~name:"meta-collision" ~category:"ltac" (fun name -> - strbrk "Collision between bound variable " ++ pr_id name ++ + strbrk "Collision between bound variable " ++ Id.print name ++ strbrk " and a metavariable of same name.") @@ -208,20 +206,16 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = match ref, EConstr.kind sigma c with | VarRef id, Var id' -> Names.Id.equal id id' - | ConstRef c, Const (c',_) -> Names.eq_constant c c' + | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -266,7 +260,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PApp (PApp (h, a1), a2), _ -> sorec ctx env subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) -> (let diff = Array.length args2 - Array.length args1 in if diff >= 0 then let args21, args22 = Array.chop diff args2 in @@ -286,7 +280,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PApp (c1,arg1), App (c2,arg2) -> (match c1, EConstr.kind sigma c2 with - | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) + | PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> @@ -303,7 +297,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels with Invalid_argument _ -> raise PatternMatchingFailure) | PApp (PRef (ConstRef c1), _), Proj (pr, c2) - when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> + when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> @@ -372,19 +366,21 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> Array.fold_left2 (sorec ctx env) subst args1 args2 - | _ -> raise PatternMatchingFailure + | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ + | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _ + | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +let matches_core_closed env sigma pat c = + let names, subst = matches_core env sigma false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma (Id.Set.empty,pat) c) let special_meta = (-1) @@ -409,9 +405,9 @@ let matches_head env sigma pat c = matches env sigma pat head (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx = +let authorized_occ env sigma closed pat c mk_ctx = try - let subst = matches_core_closed env sigma false partial_app pat c in + 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) @@ -420,10 +416,10 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx = let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) -let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = +let sub_match ?(closed=true) env sigma pat c = let open EConstr in let rec aux env c mk_ctx next = - let here = authorized_occ env sigma partial_app closed pat c mk_ctx in + let here = authorized_occ env sigma closed pat c mk_ctx in let next () = match EConstr.kind sigma c with | Cast (c1,k,c2) -> let next_mk_ctx = function @@ -453,34 +449,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> - let topdown = true in - if partial_app then - if topdown then - let lc1 = Array.sub lc 0 (Array.length lc - 1) in - let app = mkApp (c1,lc1) in - let mk_ctx = function - | [app';c] -> mk_ctx (mkApp (app',[|c|])) - | _ -> assert false in - try_aux [(env, app); (env, Array.last lc)] mk_ctx next - else - let rec aux2 app args next = - match args with - | [] -> - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next - | arg :: args -> - let app = mkApp (app,[|arg|]) in - let next () = aux2 app args next in - let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in - aux env app mk_ctx next in - aux2 c1 (Array.to_list lc) next - else - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [(env, app); (env, Array.last lc)] mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) @@ -503,14 +477,11 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let sub = subargs env types @ subargs env bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> - let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - if partial_app then - try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> next () - else - try_aux [env, c'] next_mk_ctx next + begin try + let term = Retyping.expand_projection env sigma p c' [] in + aux env term mk_ctx next + with Retyping.RetypeError _ -> next () + end | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> next () in @@ -531,13 +502,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let result () = aux env c (fun x -> x) lempty in IStream.thunk result -let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c - -let match_appsubterm env sigma pat c = - sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c - -let match_subterm_gen env sigma app pat c = - sub_match ~partial_app:app env sigma pat c +let match_subterm env sigma pat c = sub_match env sigma pat c let is_matching env sigma pat c = try let _ = matches env sigma pat c in true @@ -549,12 +514,5 @@ let is_matching_head env sigma pat c = let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in - let results = sub_match ~partial_app:true ~closed env sigma pat c in + let results = sub_match ~closed env sigma pat c in not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 34c62043e..e4d9ff9e1 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -9,7 +9,7 @@ (** This module implements pattern-matching on terms *) open Names -open Term +open Constr open EConstr open Environ open Pattern @@ -55,38 +55,19 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; m_ctx : EConstr.t } -(** [match_subterm n pat c] returns the substitution and the context - corresponding to each **closed** subterm of [c] matching [pat]. *) -val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_appsubterm pat c] returns the substitution and the context +(** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], considering application contexts as well. *) -val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : env -> Evd.evar_map -> - bool (** true = with app context *) -> +val match_subterm : env -> Evd.evar_map -> binding_bound_vars * constr_pattern -> constr -> matching_result IStream.t (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c02fc5aaf..23993243f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -252,6 +252,89 @@ let lookup_index_as_renamed env sigma t n = in lookup n 1 t (**********************************************************************) +(* Factorization of match patterns *) + +let print_factorize_match_patterns = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "factorization of \"match\" patterns in printing"; + optkey = ["Printing";"Factorizable";"Match";"Patterns"]; + optread = (fun () -> !print_factorize_match_patterns); + optwrite = (fun b -> print_factorize_match_patterns := b) } + +let print_allow_match_default_clause = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "possible use of \"match\" default pattern in printing"; + optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; + optread = (fun () -> !print_allow_match_default_clause); + optwrite = (fun b -> print_allow_match_default_clause := b) } + +let rec join_eqns (ids,rhs as x) patll = function + | (loc,(ids',patl',rhs') as eqn')::rest -> + if not !Flags.raw_print && !print_factorize_match_patterns && + List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' + then + join_eqns x (patl'::patll) rest + else + let eqn,rest = join_eqns x patll rest in + eqn, eqn'::rest + | [] -> + patll, [] + +let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll + +let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = [] + +let rec move_more_factorized_default_candidate_to_end eqn n = function + | eqn' :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn' && set (number_of_patterns eqn') >= n then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn' (get ()) eqns in + if isbest then false, dft, eqns else false, dft, eqn' :: eqns + else + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn n eqns in + isbest, dft, eqn' :: eqns + | [] -> true, Some eqn, [] + +let rec select_default_clause = function + | eqn :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn && set (number_of_patterns eqn) > 1 then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn (get ()) eqns in + if isbest then dft, eqns else dft, eqn :: eqns + else + let dft, eqns = select_default_clause eqns in dft, eqn :: eqns + | [] -> None, [] + +let factorize_eqns eqns = + let rec aux found = function + | (loc,(ids,patl,rhs))::rest -> + let patll,rest = join_eqns (ids,rhs) [patl] rest in + aux ((loc,(ids,patll,rhs))::found) rest + | [] -> + found in + let eqns = aux [] (List.rev eqns) in + let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in + if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then + match select_default_clause eqns with + (* At least two clauses and the last one is disjunctive with no variables *) + | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)] + (* Only one clause which is disjunctive with no variables: we keep at least one constructor *) + (* so that it is not interpreted as a dummy "match" *) + | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)] + | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false + | None, eqns -> eqns + else + eqns + +(**********************************************************************) (* Fragile algorithm to reverse pattern-matching compilation *) let update_name sigma na ((_,(e,_)),c) = @@ -284,13 +367,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = let rec build_tree na isgoal e sigma ci cl = let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in let cnl = ci.ci_pp_info.cstr_tags in - let cna = ci.ci_cstr_nargs in List.flatten (List.init (Array.length cl) - (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i)))) + (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i)))) and align_tree nal isgoal (e,c as rhs) sigma = match nal with - | [] -> [[],rhs] + | [] -> [Id.Set.empty,[],rhs] | na::nal -> match EConstr.kind sigma c with | Case (ci,p,c,cl) when @@ -300,19 +382,20 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e sigma ci cl in List.flatten - (List.map (fun (pat,rhs) -> + (List.map (fun (ids,pat,rhs) -> let lines = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) lines) + List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines) clauses) | _ -> - let pat = DAst.make @@ PatVar(update_name sigma na rhs) in - let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) mat + let na = update_name sigma na rhs in + let pat = DAst.make @@ PatVar na in + let mat = align_tree nal isgoal rhs sigma in + List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat -and contract_branch isgoal e sigma (cdn,can,mkpat,b) = - let nal,rhs = decomp_branch cdn [] isgoal e sigma b in +and contract_branch isgoal e sigma (cdn,mkpat,rhs) = + let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat + List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat (**********************************************************************) (* Transform internal representation of pattern-matching into list of *) @@ -414,15 +497,17 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let detype_universe sigma u = + let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in + Univ.Universe.map fn u + let detype_sort sigma = function | Prop Null -> GProp | Prop Pos -> GSet | Type u -> GType (if !print_universes - then - let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in - [Loc.tag @@ Name.mk_name (Id.of_string_soft u)] + then detype_universe sigma u else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,8 +519,8 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in - GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l))) + let l = Termops.reference_of_level sigma l in + GType (UNamed l) let detype_instance sigma l = let l = EInstance.kind sigma l in @@ -554,7 +639,7 @@ and detype_r d flags avoid env sigma t = let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in id,l with Not_found -> - Id.of_string ("X" ^ string_of_int (Evar.repr evk)), + Id.of_string ("X" ^ string_of_int (Evar.repr evk)), (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in GEvar (id, @@ -646,7 +731,7 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in - List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c)) + List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index f03bde68e..f150cb195 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ open EConstr open Glob_term @@ -27,10 +26,20 @@ val print_universes : bool ref (** If true, prints full local context of evars *) val print_evar_arguments : bool ref +(** If true, contract branches with same r.h.s. and same matching + variables in a disjunctive pattern *) +val print_factorize_match_patterns : bool ref + +(** If true and the last non unique clause of a "match" is a + variable-free disjunctive pattern, turn it into a catch-call case *) +val print_allow_match_default_clause : bool ref + val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern val subst_glob_constr : substitution -> glob_constr -> glob_constr +val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g + (** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr de Bruijn indexes are turned to bound names, avoiding names in [avoid] [isgoal] tells if naming must avoid global-level synonyms as intro does @@ -40,7 +49,7 @@ val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> const val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g -val detype_sort : evar_map -> sorts -> glob_sort +val detype_sort : evar_map -> Sorts.t -> glob_sort val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> evar_map -> rel_context -> 'a glob_decl_g list diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0f1a508c8..cb8844623 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -9,7 +9,7 @@ open CErrors open Util open Names -open Term +open Constr open Termops open Environ open EConstr @@ -48,8 +48,8 @@ let _ = Goptions.declare_bool_option { "data.id.type" etc... *) let impossible_default_case () = let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in - let (_, u) = Term.destConst c in - Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx) + let (_, u) = Constr.destConst c in + Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) let coq_unit_judge = let open Environ in @@ -175,7 +175,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Sort s -> let s = ESorts.kind sigma s in lookup_canonical_conversion - (proji, Sort_cs (family_of_sort s)),[] + (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> let c2 = Globnames.ConstRef (Projection.constant p) in let c = Retyping.expand_projection env sigma p c [] in @@ -297,7 +297,7 @@ let ise_stack2 no_app env evd f sk1 sk2 = | UnifFailure _ as x -> fail x) | UnifFailure _ as x -> fail x) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, @@ -310,8 +310,6 @@ let ise_stack2 no_app env evd f sk1 sk2 = | Success i' -> ise_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin match ise_app_stack2 env f i sk1 sk2 with @@ -341,11 +339,9 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> begin match ise_app_stack2 env f i sk1 sk2 with |_,(UnifFailure _ as x) -> x @@ -457,7 +453,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), + (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 @@ -771,7 +767,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] (* Catch the p.c ~= p c' cases *) - | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> + | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' -> let res = try Some (destApp evd (Retyping.expand_projection env evd p c [])) with Retyping.RetypeError _ -> None @@ -782,7 +778,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (appr2,csts2) | None -> UnifFailure (evd,NotSameHead)) - | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> + | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') -> let res = try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) with Retyping.RetypeError _ -> None @@ -1067,8 +1063,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index c30d1d26b..d793b06d3 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -47,7 +47,7 @@ val check_problems_are_solved : env -> evar_map -> unit val check_conv_record : env -> evar_map -> state -> state -> - Univ.universe_context_set * (constr * constr) + Univ.ContextSet.t * (constr * constr) * constr * constr list * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * constr * diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 5f12f360b..b646a37f8 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Sorts open Util open Pp open Names -open Term +open Constr open Termops open EConstr open Vars @@ -82,7 +83,7 @@ let define_pure_evar_as_product evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in - if is_prop_sort (ESorts.kind evd1 s) then + if Sorts.is_prop (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 5477c5c99..869e3adbf 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Evd open Environ @@ -39,7 +38,7 @@ val lift_tycon : int -> type_constraint -> type_constraint val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types -val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts +val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t (** {6 debug pretty-printer:} *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b906c3b59..e6d1e59b3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Sorts open Util open CErrors open Names -open Term +open Constr open Environ open Termops open Evd @@ -1391,7 +1392,7 @@ let occur_evar_upto_types sigma n c = let c = EConstr.Unsafe.to_constr c in let seen = ref Evar.Set.empty in (** FIXME: Is that supposed to be evar-insensitive? *) - let rec occur_rec c = match kind_of_term c with + let rec occur_rec c = match Constr.kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> if Evar.Set.mem sp !seen then diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 811b4dc18..703c4616c 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr open Evd open Environ @@ -49,7 +48,7 @@ val refresh_universes : env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> - bool option -> existential_key -> constr array -> constr array -> evar_map + bool option -> Evar.t -> constr array -> constr array -> evar_map val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> @@ -78,10 +77,10 @@ exception IllTypedInstance of env * types * types (* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : - evar_map -> existential_key -> constr -> conv_fun -> evar_map + evar_map -> Evar.t -> constr -> conv_fun -> evar_map val remove_instance_local_defs : - evar_map -> existential_key -> 'a array -> 'a list + evar_map -> Evar.t -> 'a array -> 'a list val get_type_of_refresh : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 9e7652da6..fd6bfe0a2 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -12,7 +12,6 @@ open CErrors open Names open Locus open EConstr -open Nameops open Termops open Pretype_errors @@ -30,7 +29,7 @@ let explain_invalid_occurrence l = ++ prlist_with_sep spc int l ++ str "." let explain_incorrect_in_value_occurrence id = - pr_id id ++ str " has no value." + Id.print id ++ str " has no value." let explain_occurrence_error = function | InvalidOccurrence l -> explain_invalid_occurrence l diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml new file mode 100644 index 000000000..768ef3cfd --- /dev/null +++ b/pretyping/geninterp.ml @@ -0,0 +1,100 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Genarg + +module TacStore = Store.Make () + +(** Dynamic toplevel values *) + +module ValT = Dyn.Make () + +module Val = +struct + + type 'a typ = 'a ValT.tag + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + let eq = ValT.eq + let repr = ValT.repr + let create = ValT.create + + let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t) + + let typ_list = ValT.create "list" + let typ_opt = ValT.create "option" + let typ_pair = ValT.create "pair" + + let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with + | Base t -> Dyn (t, x) + | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x) + | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x) + | Pair (tag1, tag2) -> + Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x))) + +end + +module ValTMap = ValT.Map + +module ValReprObj = +struct + type ('raw, 'glb, 'top) obj = 'top Val.tag + let name = "valrepr" + let default _ = None +end + +module ValRepr = Register(ValReprObj) + +let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function +| ListArg t -> Val.List (val_tag t) +| OptArg t -> Val.Opt (val_tag t) +| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) +| ExtraArg s -> ValRepr.obj (ExtraArg s) + +let val_tag = function Topwit t -> val_tag t + +let register_val0 wit tag = + let tag = match tag with + | None -> + let name = match wit with + | ExtraArg s -> ArgT.repr s + | _ -> assert false + in + Val.Base (Val.create name) + | Some tag -> tag + in + ValRepr.register0 wit tag + +(** Interpretation functions *) + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +module InterpObj = +struct + type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun + let name = "interp" + let default _ = None +end + +module Interp = Register(InterpObj) + +let interp = Interp.obj + +let register_interp0 = Interp.register0 diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli new file mode 100644 index 000000000..ae0b26e59 --- /dev/null +++ b/pretyping/geninterp.mli @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Interpretation functions for generic arguments and interpreted Ltac + values. *) + +open Names +open Genarg + +(** {6 Dynamic toplevel values} *) + +module Val : +sig + type 'a typ + + val create : string -> 'a typ + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option + val repr : 'a typ -> string + val pr : 'a typ -> Pp.t + + val typ_list : t list typ + val typ_opt : t option typ + val typ_pair : (t * t) typ + + val inject : 'a tag -> 'a -> t + +end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + +(** Dynamic types for toplevel values. While the generic types permit to relate + objects at various levels of interpretation, toplevel values are wearing + their own type regardless of where they came from. This allows to use the + same runtime representation for several generic types. *) + +val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag +(** Retrieve the dynamic type associated to a toplevel genarg. *) + +val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit +(** Register the representation of a generic argument. If no tag is given as + argument, a new fresh tag with the same name as the argument is associated + to the generic type. *) + +(** {6 Interpretation functions} *) + +module TacStore : Store.S + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun + +val register_interp0 : + ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 055fd68f6..093f1f0b6 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -290,7 +290,7 @@ let warn_variable_collision = let open Pp in CWarnings.create ~name:"variable-collision" ~category:"ltac" (fun name -> - strbrk "Collision between bound variables of name " ++ pr_id name) + strbrk "Collision between bound variables of name " ++ Id.print name) let add_and_check_ident id set = if Id.Set.mem id set then warn_variable_collision id; @@ -524,7 +524,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function try Name (Id.Map.find id ltac_idents) with Not_found -> if Id.Map.mem id ltac_genargs then - user_err (str"Ltac variable"++spc()++ pr_id id ++ + user_err (str"Ltac variable"++spc()++ Id.print id ++ spc()++str"is not bound to an identifier."++spc()++ str"It cannot be used in a binder.") else n diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index f27928662..9dd7068cb 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -64,7 +64,7 @@ val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_ here by its relevant components [m] and [c]. It is used to interpret Ltac-bound names both in pretyping and printing of terms. *) -val map_pattern_binders : (name -> name) -> +val map_pattern_binders : (Name.t -> Name.t) -> tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses) (** [map_pattern f m c] applies [f] to the return predicate and the @@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name +val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index aced42f83..b7b5b1662 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -18,6 +18,7 @@ open Libnames open Globnames open Nameops open Term +open Constr open Vars open Namegen open Declarations @@ -33,7 +34,7 @@ type dep_flag = bool (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive @@ -168,7 +169,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in - match kind_of_term p' with + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) @@ -186,13 +187,13 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | _ -> let t' = whd_all env sigma (EConstr.of_constr p) in let t' = EConstr.Unsafe.to_constr t' in - if Term.eq_constr p' t' then assert false + if Constr.equal p' t' then assert false else prec env i sign t' in prec env 0 [] in let rec process_constr env i c recargs nhyps li = - if nhyps > 0 then match kind_of_term c with + if nhyps > 0 then match kind c with | Prod (n,t,c_0) -> let (optionpos,rest) = match recargs with @@ -247,7 +248,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in - match kind_of_term p' with + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) @@ -261,7 +262,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = | _ -> let t' = whd_all env sigma (EConstr.of_constr p) in let t' = EConstr.Unsafe.to_constr t' in - if Term.eq_constr t' p' then assert false + if Constr.equal t' p' then assert false else prec env i hyps t' in prec env 0 [] @@ -505,7 +506,7 @@ let build_case_analysis_scheme_default env sigma pity kind = [rec] by [s] *) let change_sort_arity sort = - let rec drec a = match kind_of_term a with + let rec drec a = match kind a with | Cast (c,_,_) -> drec c | Prod (n,t,c) -> let s, c' = drec c in s, mkProd (n, t, c') | LetIn (n,b,t,c) -> let s, c' = drec c in s, mkLetIn (n,b,t,c') @@ -519,7 +520,7 @@ let change_sort_arity sort = let weaken_sort_scheme env evd set sort npars term ty = let evdref = ref evd in let rec drec np elim = - match kind_of_term elim with + match kind elim with | Prod (n,t,c) -> if Int.equal np 0 then let osort, t' = change_sort_arity sort t in @@ -566,7 +567,7 @@ let build_mutual_induction_scheme env sigma = function (List.map (function ((mind',u'),dep',s') -> let (sp',_) = mind' in - if eq_mind sp sp' then + if MutInd.equal sp sp' then let (mibi',mipi') = lookup_mind_specif env mind' in ((mind',u'),mibi',mipi',dep',s') else @@ -605,7 +606,7 @@ let lookup_eliminator ind_sp s = (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) try - let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in + let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in let _ = Global.lookup_constant cst in ConstRef cst with Not_found -> @@ -615,7 +616,7 @@ let lookup_eliminator ind_sp s = with Not_found -> user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ - pr_id id ++ strbrk ", the elimination of the inductive definition " ++ + Id.print id ++ strbrk ", the elimination of the inductive definition " ++ pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 2825c4d83..a9838cffe 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -7,14 +7,14 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Evd (** Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive @@ -27,25 +27,25 @@ type dep_flag = bool (** Build a case analysis elimination scheme in some sort family *) val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * Constr.t + dep_flag -> Sorts.family -> evar_map * Constr.t (** Build a dependent case elimination predicate unless type is in Prop or is a recursive record with primitive projections. *) val build_case_analysis_scheme_default : env -> evar_map -> pinductive -> - sorts_family -> evar_map * Constr.t + Sorts.family -> evar_map * Constr.t (** Builds a recursive induction scheme (Peano-induction style) in the same sort family as the inductive family; it is dependent if not in Prop or a recursive record with primitive projections. *) val build_induction_scheme : env -> evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * constr + dep_flag -> Sorts.family -> evar_map * constr (** Builds mutual (recursive) induction schemes *) val build_mutual_induction_scheme : - env -> evar_map -> (pinductive * dep_flag * sorts_family) list -> evar_map * constr list + env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list (** Scheme combinators *) @@ -54,13 +54,13 @@ val build_mutual_induction_scheme : scheme quantified on sort [s]. [set] asks for [s] be declared equal to [i], otherwise just less or equal to [i]. *) -val weaken_sort_scheme : env -> evar_map -> bool -> sorts -> int -> constr -> types -> +val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> types -> evar_map * types * constr (** Recursor names utilities *) -val lookup_eliminator : inductive -> sorts_family -> Globnames.global_reference -val elimination_suffix : sorts_family -> string -val make_elimination_ident : Id.t -> sorts_family -> Id.t +val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference +val elimination_suffix : Sorts.family -> string +val make_elimination_ident : Id.t -> Sorts.family -> Id.t val case_suffix : string diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b31ee03d8..34df7d3d7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -11,6 +11,7 @@ open Util open Names open Univ open Term +open Constr open Vars open Termops open Declarations @@ -643,7 +644,7 @@ let type_of_projection_knowing_arg env sigma p c ty = syntactic conditions *) let control_only_guard env c = - let check_fix_cofix e c = match kind_of_term c with + let check_fix_cofix e c = match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> @@ -659,7 +660,7 @@ let control_only_guard env c = (* inference of subtyping condition for inductive types *) let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = + (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) = let numchecked = ref 0 in let numparams = Context.Rel.nhyps params in let update_contexts (env, evd, csts) csts' = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index aa38d3b47..58b1ce6c3 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Declarations open Environ open Evd @@ -28,8 +28,8 @@ val arities_of_constructors : env -> pinductive -> types array reasoning either with only recursively uniform parameters or with all parameters including the recursively non-uniform ones *) type inductive_family -val make_ind_family : inductive puniverses * constr list -> inductive_family -val dest_ind_family : inductive_family -> inductive puniverses * constr list +val make_ind_family : inductive Univ.puniverses * constr list -> inductive_family +val dest_ind_family : inductive_family -> inductive Univ.puniverses * constr list val map_ind_family : (constr -> constr) -> inductive_family -> inductive_family val liftn_inductive_family : int -> int -> inductive_family -> inductive_family val lift_inductive_family : int -> inductive_family -> inductive_family @@ -120,7 +120,7 @@ val constructor_nrealdecls_env : env -> constructor -> int val constructor_has_local_defs : constructor -> bool val inductive_has_local_defs : inductive -> bool -val allowed_sorts : env -> inductive -> sorts_family list +val allowed_sorts : env -> inductive -> Sorts.family list (** (Co)Inductive records with primitive projections do not have eta-conversion, hence no dependent elimination. *) @@ -147,17 +147,17 @@ val get_constructor : pinductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary val get_constructors : env -> inductive_family -> constructor_summary array -val get_projections : env -> inductive_family -> constant array option +val get_projections : env -> inductive_family -> Constant.t array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family +val get_arity : env -> inductive_family -> Context.Rel.t * Sorts.family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context -val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types +val make_arity : env -> evar_map -> bool -> inductive_family -> Sorts.t -> EConstr.types val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) @@ -172,7 +172,7 @@ val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr. (** Builds the case predicate arity (dependent or not) *) val arity_of_case_predicate : - env -> inductive_family -> bool -> sorts -> types + env -> inductive_family -> bool -> Sorts.t -> types val type_case_branches_with_names : env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types @@ -195,7 +195,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * EConstr.types + env -> evar_map -> Inductive.mind_specif Univ.puniverses -> EConstr.types -> evar_map * EConstr.types (********************) val control_only_guard : env -> types -> unit @@ -203,8 +203,8 @@ val control_only_guard : env -> types -> unit (* inference of subtyping condition for inductive types *) (* for debugging purposes only to be removed *) val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> -(Term.constr -> Term.constr) -> -Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t +(constr -> constr) -> +types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entry diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index bc563b46d..f0cb8fd1f 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,8 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index fe134f512..79e0afa72 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -7,6 +7,7 @@ (************************************************************************) open CErrors open Term +open Constr open Vars open Environ open Reduction @@ -98,7 +99,7 @@ let app_type env c = let find_rectype_a env c = let (t, l) = app_type env c in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -131,7 +132,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = let construct_of_constr const env tag typ = let t, l = app_type env typ in - match kind_of_term t with + match kind t with | Ind (ind,u) -> construct_of_constr_notnative const env tag ind u l | _ -> assert false @@ -360,7 +361,7 @@ and nf_atom_type env sigma atom = and nf_predicate env sigma ind mip params v pT = - match kind_of_value v, kind_of_term pT with + match kind_of_value v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in let vb = f (mk_rel_accu k) in @@ -435,11 +436,11 @@ let stop_profiler m_pid = match profiler_platform() with "Unix (Linux)" -> stop_profiler_linux m_pid | _ -> () - + let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in - if Coq_config.no_native_compiler then + if not Coq_config.native_compiler then user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else let penv = Environ.pre_env env in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index aaa946706..41e09004c 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -12,6 +12,7 @@ open Names open Globnames open Nameops open Term +open Constr open Vars open Glob_term open Pp @@ -58,7 +59,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with fixpoint_eq f1 f2 | PCoFix f1, PCoFix f2 -> cofixpoint_eq f1 f2 -| _ -> false +| PProj (p1, t1), PProj (p2, t2) -> + Projection.equal p1 p2 && constr_pattern_eq t1 t2 +| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ + | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _ + | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _), _ -> false (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq (i1, j1, p1) (i2, j2, p2) = @@ -75,8 +80,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) = and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && - Array.equal Term.eq_constr c1 c2 && - Array.equal Term.eq_constr r1 r2 + Array.equal Constr.equal c1 c2 && + Array.equal Constr.equal r1 r2 let rec occur_meta_pattern = function | PApp (f,args) -> @@ -149,7 +154,7 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with let pattern_of_constr env sigma t = let rec pattern_of_constr env t = let open Context.Rel.Declaration in - match kind_of_term t with + match kind t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id @@ -165,7 +170,7 @@ let pattern_of_constr env sigma t = pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match - match kind_of_term f with + match kind f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id @@ -174,7 +179,7 @@ let pattern_of_constr env sigma t = with | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) - | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) + | Const (sp,u) -> PRef (ConstRef (Constant.make1 (Constant.canonical sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> @@ -229,8 +234,8 @@ let error_instantiate_pattern id l = | [_] -> "is" | _ -> "are" in - user_err (str "Cannot substitute the term bound to " ++ pr_id id - ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l + user_err (str "Cannot substitute the term bound to " ++ Id.print id + ++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") let instantiate_pattern env sigma lvar c = @@ -441,8 +446,8 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) - | r -> err ?loc (Pp.str "Non supported pattern.") - ) + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> + err ?loc (Pp.str "Non supported pattern.")) and pats_of_glob_branches loc metas vars ind brs = let get_arg p = match DAst.get p with diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 54b477bed..7149d62a1 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -7,20 +7,19 @@ (************************************************************************) open Names -open Term open Environ open EConstr open Type_errors type unification_error = - | OccurCheck of existential_key * constr + | OccurCheck of Evar.t * constr | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr (* Non convertible closed terms *) - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | MetaOccurInBody of Evar.t + | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities @@ -39,8 +38,8 @@ type pretype_error = (* Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (* Tactic unification *) - | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option + | UnifOccurCheck of Evar.t * constr + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -57,7 +56,7 @@ type pretype_error = | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of - (existential_key * Evar_kinds.t) option * Evar.Set.t option + (Evar.t * Evar_kinds.t) option * Evar.Set.t option exception PretypeError of env * Evd.evar_map * pretype_error diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 124fa6e06..430755ea0 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open EConstr open Type_errors @@ -15,14 +15,14 @@ open Type_errors (** {6 The type of errors raised by the pretyper } *) type unification_error = - | OccurCheck of existential_key * constr + | OccurCheck of Evar.t * constr | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | MetaOccurInBody of Evar.t + | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities @@ -41,8 +41,8 @@ type pretype_error = (** Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) - | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option + | UnifOccurCheck of Evar.t * constr + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -59,7 +59,7 @@ type pretype_error = | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of - (existential_key * Evar_kinds.t) option * Evar.Set.t option + (Evar.t * Evar_kinds.t) option * Evar.Set.t option (** unresolvable evar, connex component *) exception PretypeError of env * Evd.evar_map * pretype_error @@ -99,8 +99,8 @@ val error_ill_typed_rec_body : val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> - pinductive -> sorts_family list -> constr -> - unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b + pinductive -> Sorts.family list -> constr -> + unsafe_judgment -> (Sorts.family * Sorts.family * arity_error) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b @@ -112,10 +112,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b (** {6 Implicit arguments synthesis errors } *) -val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b +val error_occur_check : env -> Evd.evar_map -> Evar.t -> constr -> 'b val error_unsolvable_implicit : - ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> + ?loc:Loc.t -> env -> Evd.evar_map -> Evar.t -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> @@ -154,7 +154,7 @@ val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b (** {6 Typeclass errors } *) -val unsatisfiable_constraints : env -> Evd.evar_map -> Evd.evar option -> +val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option -> Evar.Set.t option -> 'a val unsatisfiable_exception : exn -> bool diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a69caecab..b930c5db8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -177,53 +177,79 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) -let interp_universe_level_name ~anon_rigidity evd (loc, s) = - match s with - | Anonymous -> - new_univ_level_variable ?loc anon_rigidity evd - | Name s -> - let s = Id.to_string s in - let names, _ = Global.global_universe_names () in - if CString.string_contains ~where:s ~what:"." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try - let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Id.Map.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:s univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) + +let interp_known_universe_level evd r = + let loc, qid = Libnames.qualid_of_reference r in + try + match r with + | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id + | Libnames.Qualid _ -> raise Not_found + with Not_found -> + let univ, k = Nametab.locate_universe qid in + Univ.Level.make univ k + +let interp_universe_level_name ~anon_rigidity evd r = + try evd, interp_known_universe_level evd r + with Not_found -> + match r with (* Qualified generated name *) + | Libnames.Qualid (loc, qid) -> + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) + in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + | Libnames.Ident (loc, id) -> (* Undeclared *) + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> - List.fold_left (fun (evd, u) l -> - (* [univ_flexible_alg] can produce algebraic universes in terms *) - let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in - (evd', Univ.sup u (Univ.Universe.make l))) + List.fold_left (fun (evd, u) l -> + let evd', u' = + match l with + | Some (l,n) -> + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let anon_rigidity = univ_flexible in + let evd', l = interp_universe_level_name ~anon_rigidity evd l in + let u' = Univ.Universe.make l in + (match n with + | 0 -> evd', u' + | 1 -> evd', Univ.Universe.super u' + | _ -> + user_err ?loc ~hdr:"interp_universe" + (Pp.(str "Cannot interpret universe increment +" ++ int n))) + | None -> + let evd, l = new_univ_level_variable ?loc univ_flexible evd in + evd, Univ.Universe.make l + in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l +let interp_known_level_info ?loc evd = function + | UUnknown | UAnonymous -> + user_err ?loc ~hdr:"interp_known_level_info" + (str "Anonymous universes not allowed here.") + | UNamed ref -> + try interp_known_universe_level evd ref + 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 - | None -> new_univ_level_variable ?loc univ_rigid evd - | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) + | 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 -type inference_hook = env -> evar_map -> evar -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; @@ -382,9 +408,9 @@ let check_instance loc subst = function | [] -> () | (id,_) :: _ -> if List.mem_assoc id subst then - user_err ?loc (pr_id id ++ str "appears more than once.") + user_err ?loc (Id.print id ++ str "appears more than once.") else - user_err ?loc (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") + user_err ?loc (str "No such variable in the signature of the existential variable: " ++ Id.print id ++ str ".") (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -410,8 +436,8 @@ let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in try mkRel (pi1 (lookup_rel_id id' (rel_context env))) with Not_found -> - user_err (str "Ltac variable " ++ pr_id id0 ++ - str " depends on pattern variable name " ++ pr_id id ++ + user_err (str "Ltac variable " ++ Id.print id0 ++ + str " depends on pattern variable name " ++ Id.print id ++ str " which is not bound in current context.") let protected_get_type_of env sigma c = @@ -454,7 +480,7 @@ let pretype_id pretype k0 loc env evdref lvar id = if Id.Map.mem id lvar.ltac_genargs then begin let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in user_err ?loc - (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ + (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \ bound to a " ++ Geninterp.Val.pr typ ++ str ".") end; (* Check if [id] is a section or goal variable *) @@ -467,6 +493,11 @@ let pretype_id pretype k0 loc env evdref lvar id = (*************************************************************************) (* Main pretyping function *) +let interp_known_glob_level ?loc evd = function + | GProp -> Univ.Level.prop + | GSet -> Univ.Level.set + | GType s -> interp_known_level_info ?loc evd s + let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set @@ -888,6 +919,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in + let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) fsign + else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in @@ -997,6 +1031,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in + let cs_args = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) cs_args + else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = List.map (set_name Anonymous) cs_args in @@ -1082,7 +1120,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> user_err ?loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ - str " in current context: no binding for " ++ pr_id id ++ str ".") in + str " in current context: no binding for " ++ Id.print id ++ str ".") in ((id,c)::subst, update) in let subst,inst = List.fold_right f hyps ([],update) in check_instance loc subst inst; diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 6537d1ecf..fe10be9e7 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -12,13 +12,16 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) -open Term +open Constr open Environ open Evd open EConstr open Glob_term -open Evarutil open Ltac_pretype +open Evardefine + +val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> + Misctypes.glob_level -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) @@ -27,7 +30,7 @@ val search_guard : type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type inference_hook = env -> evar_map -> evar -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 9904b7354..1da5b4567 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,3 +1,4 @@ +Geninterp Ltac_pretype Locusops Pretype_errors diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e970a1db9..9ff9a75b3 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,7 +19,7 @@ open Pp open Names open Globnames open Nametab -open Term +open Constr open Libobject open Mod_subst open Reductionops @@ -37,7 +37,7 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } let structure_table = Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs" @@ -48,7 +48,7 @@ let projection_table = is the inductive always (fst constructor) ? It seems so... *) type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * Constant.t option list let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in @@ -144,7 +144,7 @@ type obj_typ = { type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs let eq_cs_pattern p1 p2 = match p1, p2 with @@ -172,7 +172,7 @@ let keep_true_projections projs kinds = List.map_filter filter (List.combine projs kinds) let cs_pattern_of_constr env t = - match kind_of_term t with + match kind t with App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs @@ -184,7 +184,7 @@ let cs_pattern_of_constr env t = let { Environ.uj_type = ty } = Typeops.infer env c in let _, params = Inductive.find_rectype env ty in Const_cs (ConstRef (Projection.constant p)), None, params @ [c] - | Sort s -> Sort_cs (family_of_sort s), None, [] + | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> begin try Const_cs (global_of_constr t) , None, [] @@ -286,7 +286,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) = let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) -let inCanonStruc : constant * inductive -> obj = +let inCanonStruc : Constant.t * inductive -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; @@ -300,7 +300,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref = user_err ~hdr:"object_declare" - (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.") + (Id.print (basename_of_global ref) ++ str" is not a structure object.") let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in @@ -311,10 +311,10 @@ let check_and_decompose_canonical_structure ref = | None -> error_not_structure ref in let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in let body = EConstr.Unsafe.to_constr body in - let f,args = match kind_of_term body with + let f,args = match kind body with | App (f,args) -> f,args | _ -> error_not_structure ref in - let indsp = match kind_of_term f with + let indsp = match kind f with | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 8e2333b34..f15418577 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Globnames (** Operations concerning records and canonical structures *) @@ -20,10 +20,10 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * Constant.t option list val declare_structure : struc_tuple -> unit @@ -35,7 +35,7 @@ val lookup_structure : inductive -> struc_typ (** [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise it fails with [Not_found] *) -val lookup_projections : inductive -> constant option list +val lookup_projections : inductive -> Constant.t option list (** raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int @@ -52,7 +52,7 @@ val find_projection : global_reference -> struc_typ type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs type obj_typ = { diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2aa2f9013..ac8846854 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -9,7 +9,7 @@ open CErrors open Util open Names -open Term +open Constr open Termops open Univ open Evd @@ -284,8 +284,6 @@ sig | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list exception IncompatibleFold2 @@ -296,12 +294,12 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) - val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool) - -> 'a t -> 'a t -> (int * int) option + val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool) + -> 'a t -> 'a t -> bool val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a val append_app_list : 'a list -> 'a t -> 'a t val strip_app : 'a t -> 'a t * 'a t val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -339,12 +337,10 @@ struct type 'a member = | App of 'a app_node - | Case of Term.case_info * 'a * 'a array * Cst_stack.t + | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list let rec pr_member pr_c member = @@ -358,7 +354,7 @@ struct ++ str ")" | Proj (n,m,p,cst) -> str "ZProj(" ++ int n ++ pr_comma () ++ int m ++ - pr_comma () ++ pr_con (Projection.constant p) ++ str ")" + pr_comma () ++ Constant.print (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -367,8 +363,6 @@ struct ++ pr_comma () ++ prlist_with_sep pr_semicolon int remains ++ pr_comma () ++ pr pr_c params ++ str ")" - | Shift i -> str "ZShift(" ++ int i ++ str ")" - | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l @@ -403,54 +397,42 @@ struct else (l.(j), sk) let equal f f_fix sk1 sk2 = - let equal_cst_member x lft1 y lft2 = + let equal_cst_member x y = match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> - Constant.equal c1 c2 && Univ.Instance.equal u1 u2 + Constant.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + Constant.equal (Projection.constant p1) (Projection.constant p2) | _, _ -> false in - let rec equal_rec sk1 lft1 sk2 lft2 = + let rec equal_rec sk1 sk2 = match sk1,sk2 with - | [],[] -> Some (lft1,lft2) - | (Update _ :: _, _ | _, Update _ :: _) -> assert false - | Shift k :: s1, _ -> equal_rec s1 (lft1+k) sk2 lft2 - | _, Shift k :: s2 -> equal_rec sk1 lft1 s2 (lft2+k) + | [],[] -> true | App a1 :: s1, App a2 :: s2 -> - let t1,s1' = decomp_node_last a1 s1 in - let t2,s2' = decomp_node_last a2 s2 in - if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None + let t1,s1' = decomp_node_last a1 s1 in + let t2,s2' = decomp_node_last a2 s2 in + (f t1 t2) && (equal_rec s1' s2') | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> - if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2 - then equal_rec s1 lft1 s2 lft2 - else None + f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> - if Int.equal n1 n2 && Int.equal m1 m2 - && Constant.equal (Projection.constant p) (Projection.constant p2) - then equal_rec s1 lft1 s2 lft2 - else None + Int.equal n1 n2 && Int.equal m1 m2 + && Constant.equal (Projection.constant p) (Projection.constant p2) + && equal_rec s1 s2 | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> - if f_fix (f1,lft1) (f2,lft2) then - match equal_rec (List.rev s1) lft1 (List.rev s2) lft2 with - | None -> None - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - else None + f_fix f1 f2 + && equal_rec (List.rev s1) (List.rev s2) + && equal_rec s1' s2' | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' -> - if equal_cst_member c1 lft1 c2 lft2 then - match equal_rec (List.rev params1) lft1 (List.rev params2) lft2 with - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - | None -> None - else None - | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> None - in equal_rec (List.rev sk1) 0 (List.rev sk2) 0 + equal_cst_member c1 c2 + && equal_rec (List.rev params1) (List.rev params2) + && equal_rec s1' s2' + | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false + in equal_rec (List.rev sk1) (List.rev sk2) let compare_shape stk1 stk2 = let rec compare_rec bal stk1 stk2 = match (stk1,stk2) with ([],[]) -> Int.equal bal 0 - | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2 - | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> @@ -466,40 +448,29 @@ struct exception IncompatibleFold2 let fold2 f o sk1 sk2 = - let rec aux o lft1 sk1 lft2 sk2 = - let fold_array = - Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y)) - in + let rec aux o sk1 sk2 = match sk1,sk2 with - | [], [] -> o,lft1,lft2 - | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2 - | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2 + | [], [] -> o | App n1 :: q1, App n2 :: q2 -> - let t1,l1 = decomp_node_last n1 q1 in - let t2,l2 = decomp_node_last n2 q2 in - aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - lft1 l1 lft2 l2 + let t1,l1 = decomp_node_last n1 q1 in + let t2,l2 = decomp_node_last n2 q2 in + aux (f o t1 t2) l1 l2 | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 -> - aux (fold_array - (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - a1 a2) lft1 q1 lft2 q2 + aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> - aux o lft1 q1 lft2 q2 + aux o q1 q2 | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> - let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2) - lft1 (List.rev s1) lft2 (List.rev s2) in - aux o' lft1' q1 lft2' q2 + let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in + aux o' q1 q2 | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 -> - let (o',lft1',lft2') = - aux o lft1 (List.rev params1) lft2 (List.rev params2) - in aux o' lft1' q1 lft2' q2 - | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> - raise IncompatibleFold2 - in aux o 0 (List.rev sk1) 0 (List.rev sk2) + let o' = aux o (List.rev params1) (List.rev params2) in + aux o' q1 q2 + | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + raise IncompatibleFold2 + in aux o (List.rev sk1) (List.rev sk2) let rec map f x = List.map (function - | Update _ -> assert false - | (Proj (_,_,_,_) | Shift _) as e -> e + | (Proj (_,_,_,_)) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) @@ -516,18 +487,15 @@ struct let rec args_size = function | App (i,_,j)::s -> j + 1 - i + args_size s - | Shift(_)::s -> args_size s - | Update(_)::s -> args_size s | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0 let strip_app s = let rec aux out = function - | ( App _ | Shift _ as e) :: s -> aux (e :: out) s + | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s let strip_n_app n s = let rec aux n out = function - | Shift k as e :: s -> aux n (e :: out) s | App (i,a,j) as e :: s -> let nb = j - i + 1 in if n >= nb then @@ -552,14 +520,12 @@ struct let list_of_app_stack s = let rec aux = function | App (i,a,j) :: s -> - let (k,(args',s')) = aux s in - let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in - k,(Array.fold_right (fun x y -> x::y) a' args', s') - | Shift n :: s -> - let (k,(args',s')) = aux s in (k+n,(args', s')) - | s -> (0,([],s)) in - let (lft,(out,s')) = aux s in - let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in + let (args',s') = aux s in + let a' = Array.sub a i (j - i + 1) in + (Array.fold_right (fun x y -> x::y) a' args', s') + | s -> ([],s) in + let (out,s') = aux s in + let init = match s' with [] -> true | _ -> false in Option.init init out let assign s p c = @@ -568,20 +534,18 @@ struct | None -> assert false let tail n0 s0 = - let rec aux lft n s = - let out s = if Int.equal lft 0 then s else Shift lft :: s in - if Int.equal n 0 then out s else + let rec aux n s = + if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> let nb = j - i + 1 in if n >= nb then - aux lft (n - nb) s + aux (n - nb) s else let p = i+n in if j >= p then App(p,a,j)::s else s - | Shift k :: s' -> aux (lft+k) n s' | _ -> raise (Invalid_argument "Reductionops.Stack.tail") - in aux 0 n0 s0 + in aux n0 s0 let nth s p = match strip_n_app p s with @@ -627,11 +591,9 @@ struct zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Shift n::s) -> zip (lift n f, s) | f, (Proj (n,m,p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) - | _, (Update _::_) -> assert false in zip s @@ -868,11 +830,9 @@ let _ = Goptions.declare_bool_option { } let equal_stacks sigma (x, l) (y, l') = - let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in - let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in - match Stack.equal f_equal eq_fix l l' with - | None -> false - | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) + let f_equal x y = eq_constr sigma x y in + let eq_fix a b = f_equal (mkFix a) (mkFix b) in + Stack.equal f_equal eq_fix l l' && f_equal x y let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in @@ -1074,7 +1034,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (arg, Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end - |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false + |_, (Stack.App _)::_ -> assert false |_, _ -> fold () else fold () @@ -1155,7 +1115,7 @@ let local_whd_state_gen flags sigma = |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip sigma (x,args) in whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) - |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false + |_, (Stack.App _|Stack.Cst _)::_ -> assert false |_, _ -> s else s @@ -1167,7 +1127,8 @@ let local_whd_state_gen flags sigma = |_ -> s else s - | x -> s + | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ -> s + in whrec @@ -1291,11 +1252,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = @@ -1305,7 +1266,7 @@ let is_transparent e k = (* Conversion utility functions *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t let pb_is_equal pb = pb == Reduction.CONV @@ -1314,7 +1275,9 @@ let pb_equal = function | Reduction.CONV -> Reduction.CONV let report_anomaly e = - let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in + let msg = Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) in + let e = UserError (None,msg) in let e = CErrors.push e in iraise e @@ -1682,7 +1645,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = if isConstruct sigma t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' - |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' + |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' in whrec csts s let find_conclusion env sigma = @@ -1769,8 +1732,8 @@ let meta_reducible_instance evd b = let is_coerce = match s with CoerceToType -> true | _ -> false in if not is_coerce then irec g else u with Not_found -> u) - | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) -> - let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in + | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) -> + let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in (match try let g, s = Metamap.find m metas in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1828196fe..a277864c9 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open EConstr open Univ open Evd @@ -82,8 +82,6 @@ module Stack : sig | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list val pr : ('a -> Pp.t) -> 'a t -> Pp.t @@ -102,12 +100,12 @@ module Stack : sig @return the result and the lifts to apply on the terms @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *) val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t val append_app_list : 'a list -> 'a t -> 'a t (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App or Shift *) + start by App *) val strip_app : 'a t -> 'a t * 'a t (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -258,11 +256,11 @@ val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixp val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) -val is_transparent : Environ.env -> constant tableKey -> bool +val is_transparent : Environ.env -> Constant.t tableKey -> bool (** {6 Conversion Functions (uses closures, lazy strategy) } *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 56f8b33e0..00b175c48 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -10,6 +10,7 @@ open Pp open CErrors open Util open Term +open Constr open Inductive open Inductiveops open Names @@ -146,7 +147,7 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> type1_sort + | Prop _ -> Sorts.type1 | Type u -> Type (Univ.super u) end | Prod (name,t,c2) -> @@ -165,23 +166,6 @@ let retype ?(polyprop=true) sigma = | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> decomp_sort env sigma (type_of env t) - and sort_family_of env t = - match EConstr.kind sigma t with - | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s) - | Sort _ -> InType - | Prod (name,t,c2) -> - let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in - if not (is_impredicative_set env) && - s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma f -> - let t = type_of_global_reference_knowing_parameters env f args in - family_of_sort (sort_of_atomic_type env sigma t args) - | App(f,args) -> - family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) - | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | _ -> - family_of_sort (decomp_sort env sigma (type_of env t)) - and type_of_global_reference_knowing_parameters env c args = let argtyps = Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in @@ -197,15 +181,34 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (type_of_constructor env (cstr, u)) | _ -> assert false - in type_of, sort_of, sort_family_of, - type_of_global_reference_knowing_parameters + in type_of, sort_of, type_of_global_reference_knowing_parameters + +let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = + let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in + let rec sort_family_of env t = + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) + | Sort _ -> InType + | Prod (name,t,c2) -> + let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in + if not (is_impredicative_set env) && + s2 == InSet && sort_family_of env t == InType then InType else s2 + | App(f,args) when is_template_polymorphic env sigma f -> + if truncation_style then InType else + let t = type_of_global_reference_knowing_parameters env f args in + Sorts.family (sort_of_atomic_type env sigma t args) + | App(f,args) -> + Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) + | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType + | _ -> + Sorts.family (decomp_sort env sigma (type_of env t)) + in sort_family_of env t let get_sort_of ?(polyprop=true) env sigma t = - let _,f,_,_ = retype ~polyprop sigma in anomaly_on_error (f env) t -let get_sort_family_of ?(polyprop=true) env sigma c = - let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c + let _,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) t let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in anomaly_on_error (f env c) args + let _,_,f = retype sigma in anomaly_on_error (f env c) args let type_of_global_reference_knowing_conclusion env sigma c conclty = match EConstr.kind sigma c with @@ -224,14 +227,14 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = - let f,_,_,_ = retype ~polyprop sigma in + let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c (* Makes an unsafe judgment from a constr *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index ed3a9d0f9..6fdde9046 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Evd open Environ open EConstr @@ -30,10 +29,13 @@ val get_type_of : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types val get_sort_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts + ?polyprop:bool -> env -> evar_map -> types -> Sorts.t +(* When [truncation_style] is [true], tells if the type has been explicitly + truncated to Prop or (impredicative) Set; in particular, singleton type and + small inductive types, which have all eliminations to Type, are in Type *) val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts_family + ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment @@ -44,7 +46,7 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> val type_of_global_reference_knowing_conclusion : env -> evar_map -> constr -> types -> evar_map * types -val sorts_of_context : env -> evar_map -> rel_context -> sorts list +val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9451b0f86..5a522e06a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -75,13 +75,13 @@ let global_of_evaluable_reference = function | EvalVarRef id -> VarRef id type evaluable_reference = - | EvalConst of constant + | EvalConst of Constant.t | EvalVar of Id.t | EvalRel of int | EvalEvar of EConstr.existential let evaluable_reference_eq sigma r1 r2 = match r1, r2 with -| EvalConst c1, EvalConst c2 -> eq_constant c1 c2 +| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) -> @@ -240,7 +240,7 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - Some (EvalConst (con_with_label kn (Label.of_id id))) in + Some (EvalConst (Constant.change_label kn (Label.of_id id))) in match refi with | None -> None | Some ref -> @@ -521,7 +521,7 @@ let reduce_mind_case_use_function func env sigma mia = the block was indeed initially built as a global definition *) let (kn, u) = destConst sigma func in - let kn = con_with_label kn (Label.of_id id) in + let kn = Constant.change_label kn (Label.of_id id) in let cst = (kn, EInstance.kind sigma u) in try match constant_opt_value_in env cst with | None -> None @@ -927,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a @@ -944,7 +944,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = | CoFix _ | Fix _ -> s' | Proj (p,t) when (match EConstr.kind sigma constr with - | Const (c', _) -> eq_constant (Projection.constant p) c' + | Const (c', _) -> Constant.equal (Projection.constant p) c' | _ -> false) -> let pb = Environ.lookup_projection p env in if List.length stack <= pb.Declarations.proj_npars then @@ -1050,7 +1050,7 @@ let contextually byhead occs f env sigma t = let match_constr_evaluable_ref sigma c evref = match EConstr.kind sigma c, evref with - | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u + | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 375a8a983..b49da57a4 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -11,6 +11,7 @@ open Names open Globnames open Decl_kinds open Term +open Constr open Vars open Evd open Util @@ -71,7 +72,7 @@ type typeclass = { (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option - * constant option) list; + * Constant.t option) list; cl_strict : bool; @@ -520,7 +521,7 @@ let mark_unresolvable evi = mark_resolvability false evi let mark_resolvable evi = mark_resolvability true evi open Evar_kinds -type evar_filter = existential_key -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t -> bool let all_evars _ _ = true let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false @@ -551,8 +552,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 99cdbd3a3..618826f3d 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -8,7 +8,7 @@ open Names open Globnames -open Term +open Constr open Evd open Environ @@ -36,7 +36,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 option) list; + cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -68,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) -val typeclass_univ_instance : typeclass puniverses -> typeclass +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 @@ -83,11 +83,11 @@ val is_instance : global_reference -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) -val instance_constructor : typeclass puniverses -> constr list -> +val instance_constructor : typeclass Univ.puniverses -> constr list -> constr option * types (** Filter which evars to consider for resolution. *) -type evar_filter = existential_key -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t -> bool val all_evars : evar_filter val all_goals : evar_filter val no_goals : evar_filter diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1f35fa19a..43066c809 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -160,7 +160,7 @@ let check_type_fixpoint ?loc env evdref lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in - let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in + let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in if not (List.exists ((==) ksort) sorts) then @@ -195,11 +195,11 @@ let check_cofix env sigma pcofix = let judge_of_prop = { uj_val = EConstr.mkProp; - uj_type = EConstr.mkSort type1_sort } + uj_type = EConstr.mkSort Sorts.type1 } let judge_of_set = { uj_val = EConstr.mkSet; - uj_type = EConstr.mkSort type1_sort } + uj_type = EConstr.mkSort Sorts.type1 } let judge_of_prop_contents = function | Null -> judge_of_prop diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1e2078826..9f084ae8d 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open EConstr open Evd @@ -26,7 +26,7 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) -val e_sort_of : env -> evar_map ref -> types -> sorts +val e_sort_of : env -> evar_map ref -> types -> Sorts.t (** Typecheck a term has a given type (assuming the type is OK) *) val e_check : env -> evar_map ref -> constr -> types -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e8f7e2bba..30674fee2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -12,7 +12,7 @@ open CErrors open Pp open Util open Names -open Term +open Constr open Termops open Environ open EConstr @@ -68,10 +68,10 @@ let _ = Goptions.declare_bool_option { let unsafe_occur_meta_or_existential c = let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Evar _ -> raise Occur | Meta _ -> raise Occur - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Occur -> true @@ -79,7 +79,7 @@ let occur_meta_or_undefined_evar evd c = (** This is performance-critical. Using the evar-insensitive API changes the resulting heuristic. *) let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Meta _ -> raise Occur | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with @@ -194,6 +194,10 @@ let pose_all_metas_as_evars env evd t = let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in + let ty = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) + else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in let ev = Evarutil.e_new_evar env evdref ~src ty in evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref; @@ -554,10 +558,10 @@ let oracle_order env cf1 cf2 = | Some k2 -> match k1, k2 with | IsProj (p, _), IsKey (ConstKey (p',_)) - when eq_constant (Projection.constant p) p' -> + when Constant.equal (Projection.constant p) p' -> Some (not (Projection.unfolded p)) | IsKey (ConstKey (p,_)), IsProj (p', _) - when eq_constant p (Projection.constant p') -> + when Constant.equal p (Projection.constant p') -> Some (Projection.unfolded p') | _ -> Some (Conv_oracle.oracle_order (fun x -> x) @@ -569,7 +573,9 @@ let is_rigid_head sigma flags t = | Ind (i,u) -> true | Construct _ -> true | Fix _ | CoFix _ -> true - | _ -> false + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _) + | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _) + | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = Universes.Constraints.fold @@ -609,7 +615,7 @@ let subst_defined_metas_evars sigma (bl,el) c = (** This seems to be performance-critical, and using the evar-insensitive primitives blow up the time passed in this function. *) let c = EConstr.Unsafe.to_constr c in - let rec substrec c = match kind_of_term c with + let rec substrec c = match Constr.kind c with | Meta i -> let select (j,_,_) = Int.equal i j in substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl))) @@ -650,7 +656,10 @@ let rec is_neutral env sigma ts t = | Evar _ | Meta _ -> true | Case (_, p, c, cl) -> is_neutral env sigma ts c | Proj (p, c) -> is_neutral env sigma ts c - | _ -> false + | Lambda _ | LetIn _ | Construct _ | CoFix _ -> false + | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *) + | Fix _ -> false (* This is an approximation *) + | App _ -> assert false let is_eta_constructor_app env sigma ts f l1 term = match EConstr.kind sigma f with @@ -784,7 +793,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (** Fast path for projections. *) - | Proj (p1,c1), Proj (p2,c2) when eq_constant + | Proj (p1,c1), Proj (p2,c2) when Constant.equal (Projection.constant p1) (Projection.constant p2) -> (try unify_same_proj curenvnb cv_pb {opt with at_top = true} substn c1 c2 @@ -1068,13 +1077,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e in try let opt' = {opt with with_types = false} in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) (evd,ms,es) us2 us in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) substn params1 params in - let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in + let substn = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in let app = mkApp (c, Array.rev_of_list ks) in (* let substn = unirec_rec curenvnb pb b false substn t cN in *) unirec_rec curenvnb pb opt' substn c1 app @@ -1624,7 +1633,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context_val x (named_context_val env) then user_err ~hdr:"Unification.make_abstraction_core" - (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") + (str "The variable " ++ Id.print x ++ str " is already declared.") else x in @@ -1784,7 +1793,9 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = with ex when precatchable_exception ex -> matchrec c) - | _ -> user_err Pp.(str "Match_subterm"))) + | Cast (_, _, _) (* Is this expected? *) + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ + | Construct _ -> user_err Pp.(str "Match_subterm"))) in try matchrec cl with ex when precatchable_exception ex -> @@ -1850,7 +1861,11 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = | Lambda (_,t,c) -> bind (matchrec t) (matchrec c) - | _ -> fail "Match_subterm")) + | Cast (_, _, _) -> fail "Match_subterm" (* Is this expected? *) + + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ + | Construct _ -> fail "Match_subterm")) + in let res = matchrec cl [] in match res with @@ -2000,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 = let w_unify = if Flags.profile then - let wunifkey = Profile.declare_profile "w_unify" in - Profile.profile6 wunifkey w_unify + let wunifkey = CProfile.declare_profile "w_unify" in + CProfile.profile6 wunifkey w_unify else w_unify let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index fce17d564..085e8c5b8 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr open Environ open Evd diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index d7c42d03a..3cf32d7ff 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -7,9 +7,7 @@ (************************************************************************) open Names -open Nameops open CErrors -open Pp (** Local universes and constraints declarations *) type universe_decl = @@ -23,27 +21,16 @@ let default_univ_decl = univdecl_extensible_constraints = true } let interp_univ_constraints env evd cstrs = - let open Misctypes in - let u_of_id x = - match x with - | Misctypes.GProp -> Loc.tag Univ.Level.prop - | GSet -> Loc.tag Univ.Level.set - | GType None | GType (Some (_, Anonymous)) -> - user_err ~hdr:"interp_constraint" - (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, Name id)) -> - try loc, Evd.universe_of_name evd (Id.to_string id) - with Not_found -> - user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ pr_id id) - in let interp (evd,cstrs) (u, d, u') = - let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in + let ul = Pretyping.interp_known_glob_level evd u in + let u'l = Pretyping.interp_known_glob_level evd u' in let cstr = (ul,d,u'l) in let cstrs' = Univ.Constraint.add cstr cstrs in try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in evd, cstrs' with Univ.UniverseInconsistency e -> - user_err ~hdr:"interp_constraint" (str "Universe inconsistency" (* TODO *)) + user_err ~hdr:"interp_constraint" + (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) in List.fold_left interp (evd,Univ.Constraint.empty) cstrs diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 66cc42cb6..e395bdbc6 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -10,6 +10,7 @@ open Util open Names open Declarations open Term +open Constr open Vars open Environ open Inductive @@ -51,7 +52,7 @@ let invert_tag cst tag reloc_tbl = let find_rectype_a env c = let (t, l) = decompose_appvect (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> assert false @@ -262,7 +263,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind_of_term pT with + match whd_val v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in let vb = body_of_vfun k f in @@ -364,4 +365,4 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb) ~catch_incon:true ~pb env sigma t1 t2 -let _ = Reductionops.set_vm_infer_conv vm_infer_conv +let _ = if Coq_config.bytecode_compiler then Reductionops.set_vm_infer_conv vm_infer_conv |