aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercionops.ml12
-rw-r--r--pretyping/detyping.ml114
-rw-r--r--pretyping/detyping.mli7
-rw-r--r--pretyping/evarconv.ml60
-rw-r--r--pretyping/evarsolve.ml109
-rw-r--r--pretyping/glob_ops.ml18
-rw-r--r--pretyping/glob_ops.mli2
-rw-r--r--pretyping/nativenorm.ml39
-rw-r--r--pretyping/nativenorm.mli10
-rw-r--r--pretyping/pretyping.ml38
-rw-r--r--pretyping/pretyping.mli11
-rw-r--r--pretyping/reductionops.ml154
-rw-r--r--pretyping/reductionops.mli15
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--pretyping/unification.ml48
-rw-r--r--pretyping/vnorm.ml2
16 files changed, 286 insertions, 363 deletions
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index d6458e1409..49401a9937 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -67,8 +67,6 @@ end
module ClTypMap = Map.Make(ClTyp)
-module IntMap = Map.Make(Int)
-
let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
type inheritance_path = coe_info_typ list
@@ -97,13 +95,13 @@ struct
module Index = struct include Int let print = Pp.int end
- type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t }
- let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty }
+ type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
+ let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
let mem y b = ClTypMap.mem y b.inv
- let map x b = IntMap.find x b.v
- let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v))
+ let map x b = Int.Map.find x b.v
+ let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
let add x y b =
- { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
+ { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
end
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 73be36d031..857918c928 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -221,53 +221,35 @@ module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet)
(* Flags.for printing or not wildcard and synthetisable types *)
-open Goptions
-
-let wildcard_value = ref true
-let force_wildcard () = !wildcard_value
-
-let () = declare_bool_option
- { optdepr = false;
- optkey = ["Printing";"Wildcard"];
- optread = force_wildcard;
- optwrite = (:=) wildcard_value }
-
-let fast_name_generation = ref false
-
-let () = declare_bool_option {
- optdepr = false;
- optkey = ["Fast";"Name";"Printing"];
- optread = (fun () -> !fast_name_generation);
- optwrite = (:=) fast_name_generation;
-}
-
-let synth_type_value = ref true
-let synthetize_type () = !synth_type_value
-
-let () = declare_bool_option
- { optdepr = false;
- optkey = ["Printing";"Synth"];
- optread = synthetize_type;
- optwrite = (:=) synth_type_value }
-
-let reverse_matching_value = ref true
-let reverse_matching () = !reverse_matching_value
-
-let () = declare_bool_option
- { optdepr = false;
- optkey = ["Printing";"Matching"];
- optread = reverse_matching;
- optwrite = (:=) reverse_matching_value }
-
-let print_primproj_params_value = ref false
-let print_primproj_params () = !print_primproj_params_value
-
-let () = declare_bool_option
- { optdepr = false;
- optkey = ["Printing";"Primitive";"Projection";"Parameters"];
- optread = print_primproj_params;
- optwrite = (:=) print_primproj_params_value }
-
+let force_wildcard =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Wildcard"]
+ ~value:true
+
+let fast_name_generation =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Fast";"Name";"Printing"]
+ ~value:false
+
+let synthetize_type =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Synth"]
+ ~value:true
+
+let reverse_matching =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Matching"]
+ ~value:true
+
+let print_primproj_params =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Primitive";"Projection";"Parameters"]
+ ~value:false
(* Auxiliary function for MutCase printing *)
(* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -338,27 +320,23 @@ let lookup_index_as_renamed env sigma t n =
(**********************************************************************)
(* Factorization of match patterns *)
-let print_factorize_match_patterns = ref true
-
-let () =
- declare_bool_option
- { optdepr = false;
- 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 print_factorize_match_patterns =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Factorizable";"Match";"Patterns"]
+ ~value:true
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Printing";"Allow";"Match";"Default";"Clause"];
- optread = (fun () -> !print_allow_match_default_clause);
- optwrite = (fun b -> print_allow_match_default_clause := b) }
+let print_allow_match_default_opt_name =
+ ["Printing";"Allow";"Match";"Default";"Clause"]
+let print_allow_match_default_clause =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:print_allow_match_default_opt_name
+ ~value:true
let rec join_eqns (ids,rhs as x) patll = function
| ({CAst.loc; v=(ids',patl',rhs')} as eqn')::rest ->
- if not !Flags.raw_print && !print_factorize_match_patterns &&
+ 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
@@ -404,7 +382,7 @@ let factorize_eqns eqns =
let eqns = aux [] (List.rev eqns) in
let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in
let open CAst in
- if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then
+ 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 {loc=gloc;v=([],patl::_::_,rhs)}, (_::_ as eqns) ->
@@ -925,16 +903,16 @@ let detype_rel_context d flags where avoid env sigma sign =
let detype_names isgoal avoid nenv env sigma t =
let flags = { flg_isgoal = isgoal; flg_lax = false } in
- let avoid = Avoid.make ~fast:!fast_name_generation avoid in
+ let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in
detype Now flags avoid (nenv,env) sigma t
let detype d ?(lax=false) isgoal avoid env sigma t =
let flags = { flg_isgoal = isgoal; flg_lax = lax } in
- let avoid = Avoid.make ~fast:!fast_name_generation avoid in
+ let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in
detype d flags avoid (names_of_rel_context env, env) sigma t
let detype_rel_context d ?(lax = false) where avoid env sigma sign =
let flags = { flg_isgoal = false; flg_lax = lax } in
- let avoid = Avoid.make ~fast:!fast_name_generation avoid in
+ let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in
detype_rel_context d flags where avoid env sigma sign
let detype_closed_glob ?lax isgoal avoid env sigma t =
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5723b47715..254f772ff8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -29,11 +29,12 @@ 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
+val print_factorize_match_patterns : unit -> bool
-(** If true and the last non unique clause of a "match" is a
+(** If this flag is 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 print_allow_match_default_clause : unit -> bool
+val print_allow_match_default_opt_name : string list
val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 26bf02aa25..3d887e1a95 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -47,21 +47,17 @@ let default_flags env =
let ts = default_transparent_state env in
default_flags_of ts
-let debug_unification = ref (false)
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Debug";"Unification"];
- optread = (fun () -> !debug_unification);
- optwrite = (fun a -> debug_unification:=a);
-})
-
-let debug_ho_unification = ref (false)
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Debug";"HO";"Unification"];
- optread = (fun () -> !debug_ho_unification);
- optwrite = (fun a -> debug_ho_unification:=a);
-})
+let debug_unification =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Debug";"Unification"]
+ ~value:false
+
+let debug_ho_unification =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Debug";"HO";"Unification"]
+ ~value:false
(*******************************************)
(* Functions to deal with impossible cases *)
@@ -767,7 +763,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
in
let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
(* Evar must be undefined since we have flushed evars *)
- let () = if !debug_unification then
+ let () = if debug_unification () then
let open Pp in
Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
match (flex_kind_of_term flags env evd term1 sk1,
@@ -1224,16 +1220,16 @@ let apply_on_subterm env evd fixedref f test c t =
(fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t
else
- (if !debug_ho_unification then
+ (if debug_ho_unification () then
Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t);
let b, evd =
try test env !evdref k c t
with e when CErrors.noncritical e -> assert false in
- if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded");
+ if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded");
let evd', t' = f !evdref k t in
evdref := evd'; t')
else (
- if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed");
+ if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
map_constr_with_binders_left_to_right !evdref
(fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t))
@@ -1337,7 +1333,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
let env_evar = evar_filtered_env env_rhs evi in
let sign = named_context_val env_evar in
let ctxt = evar_filtered_context evi in
- if !debug_ho_unification then
+ if debug_ho_unification () then
(Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
let args = Array.map (nf_evar evd) args in
@@ -1374,7 +1370,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
let rec set_holes env_rhs evd rhs = function
| (id,idty,c,cty,evsref,filter,occs)::subst ->
let c = nf_evar evd c in
- if !debug_ho_unification then
+ if debug_ho_unification () then
Feedback.msg_debug Pp.(str"set holes for: " ++
prc env_rhs evd (mkVar id.binder_name) ++ spc () ++
prc env_rhs evd c ++ str" in " ++
@@ -1382,7 +1378,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
let occ = ref 1 in
let set_var evd k inst =
let oc = !occ in
- if !debug_ho_unification then
+ if debug_ho_unification () then
(Feedback.msg_debug Pp.(str"Found one occurrence");
Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c));
incr occ;
@@ -1393,7 +1389,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
| Unspecified prefer_abstraction ->
let evd, evty = set_holes env_rhs evd cty subst in
let evty = nf_evar evd evty in
- if !debug_ho_unification then
+ if debug_ho_unification () then
Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
str" of type: " ++ prc env_evar evd evty ++
str " for " ++ prc env_rhs evd c);
@@ -1413,7 +1409,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
evd, ev
in
let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
- if !debug_ho_unification then
+ if debug_ho_unification () then
Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs');
let () = check_selected_occs env_rhs evd c !occ occs in
let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
@@ -1427,7 +1423,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
(* Thin evars making the term typable in env_evar *)
let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
(* We instantiate the evars of which the value is forced by typing *)
- if !debug_ho_unification then
+ if debug_ho_unification () then
(Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs');
Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
let evd,rhs' =
@@ -1437,7 +1433,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
raise (TypingFailed evd) in
let rhs' = nf_evar evd rhs' in
(* We instantiate the evars of which the value is forced by typing *)
- if !debug_ho_unification then
+ if debug_ho_unification () then
(Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs');
Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
@@ -1445,7 +1441,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
| (id,idty,c,cty,evsref,_,_)::l ->
let id = id.binder_name in
let c = nf_evar evd c in
- if !debug_ho_unification then
+ if debug_ho_unification () then
Feedback.msg_debug Pp.(str"abstracting: " ++
prc env_rhs evd (mkVar id) ++ spc () ++
prc env_rhs evd c);
@@ -1476,7 +1472,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
| _ -> evd)
with e -> user_err (Pp.str "Cannot find an instance")
else
- ((if !debug_ho_unification then
+ ((if debug_ho_unification () then
let evi = Evd.find evd evk in
let env = Evd.evar_env env_rhs evi in
Feedback.msg_debug Pp.(str"evar is defined: " ++
@@ -1491,7 +1487,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
if Evd.is_defined evd evk then
(* Can happen due to dependencies: instantiating evars in the arguments of evk might
instantiate evk itself. *)
- (if !debug_ho_unification then
+ (if debug_ho_unification () then
begin
let evi = Evd.find evd evk in
let evenv = evar_env env_rhs evi in
@@ -1504,13 +1500,13 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
let evi = Evd.find_undefined evd evk in
let evenv = evar_env env_rhs evi in
let rhs' = nf_evar evd rhs' in
- if !debug_ho_unification then
+ if debug_ho_unification () then
Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
prc evenv evd rhs');
(* solve_evars is not commuting with nf_evar, because restricting
an evar might provide a more specific type. *)
let evd, _ = !solve_evars evenv evd rhs' in
- if !debug_ho_unification then
+ if debug_ho_unification () then
Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'));
let flags = default_flags_of TransparentState.full in
Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs'
@@ -1564,7 +1560,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in
let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
- let () = if !debug_unification then
+ let () = if debug_unification () then
let open Pp in
Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
Termops.Internal.print_constr_env env evd t1 ++ cut () ++
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4eae0cf86c..e475e4c52b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -416,19 +416,10 @@ let get_alias_chain_of sigma aliases x = match x with
| RelAlias n -> (try Int.Map.find n aliases.rel_aliases with Not_found -> empty_aliasing)
| VarAlias id -> (try cast_aliasing (Id.Map.find id aliases.var_aliases) with Not_found -> empty_aliasing)
-let normalize_alias_opt_alias sigma aliases x =
- match get_alias_chain_of sigma aliases x with
- | _, [] -> None
- | _, a :: _ -> Some a
-
-let normalize_alias_opt sigma aliases x = match to_alias sigma x with
-| None -> None
-| Some a -> normalize_alias_opt_alias sigma aliases a
-
let normalize_alias sigma aliases x =
- match normalize_alias_opt_alias sigma aliases x with
- | Some a -> a
- | None -> x
+ match get_alias_chain_of sigma aliases x with
+ | _, [] -> x
+ | _, a :: _ -> a
let normalize_alias_var sigma var_aliases id =
let aliases = { var_aliases; rel_aliases = Int.Map.empty } in
@@ -678,7 +669,7 @@ let make_projectable_subst aliases sigma evi args =
let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in
Constrmap.add (fst cstr) ((args,id)::l) cstrs
| _ -> cstrs in
- let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in
+ let all = Int.Map.add i [a, id] all in
(rest,all,cstrs,revmap)
| LocalDef ({binder_name=id},c,_), a::rest ->
let revmap = Id.Map.add id i revmap in
@@ -688,13 +679,13 @@ let make_projectable_subst aliases sigma evi args =
let ic, sub =
try let ic = Id.Map.find idc revmap in ic, Int.Map.find ic all
with Not_found -> i, [] (* e.g. [idc] is a filtered variable: treat [id] as an assumption *) in
- if List.exists (fun (c,_,_) -> EConstr.eq_constr sigma a c) sub then
+ if List.exists (fun (c, _) -> EConstr.eq_constr sigma a c) sub then
(rest,all,cstrs,revmap)
else
- let all = Int.Map.add ic ((a,normalize_alias_opt sigma aliases a,id)::sub) all in
+ let all = Int.Map.add ic ((a, id)::sub) all in
(rest,all,cstrs,revmap)
| _ ->
- let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in
+ let all = Int.Map.add i [a, id] all in
(rest,all,cstrs,revmap))
| _ -> anomaly (Pp.str "Instance does not match its signature.")) 0
sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in
@@ -862,47 +853,47 @@ type evar_projection =
exception NotUnique
exception NotUniqueInType of (Id.t * evar_projection) list
-let rec assoc_up_to_alias sigma aliases y yc = function
+let rec assoc_up_to_alias sigma aliases y = function
| [] -> raise Not_found
- | (c,cc,id)::l ->
- if is_alias sigma c y then id
+ | (c, id)::l ->
+ match to_alias sigma c with
+ | None -> assoc_up_to_alias sigma aliases y l
+ | Some c ->
+ if eq_alias c y then id
else
match l with
- | _ :: _ -> assoc_up_to_alias sigma aliases y yc l
+ | _ :: _ -> assoc_up_to_alias sigma aliases y l
| [] ->
(* Last chance, we reason up to alias conversion *)
- match (normalize_alias_opt sigma aliases c) with
- | Some cc when eq_alias yc cc -> id
- | _ -> if is_alias sigma c yc then id else raise Not_found
+ let cc = normalize_alias sigma aliases c in
+ let yc = normalize_alias sigma aliases y in
+ if eq_alias cc yc then id else raise Not_found
-let rec find_projectable_vars with_evars aliases sigma y subst =
- let yc = normalize_alias sigma aliases y in
- let is_projectable idc idcl (subst1,subst2 as subst') =
+let rec find_projectable_vars aliases sigma y subst =
+ let is_projectable _ idcl (subst1,subst2 as subst') =
(* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
try
- let id = assoc_up_to_alias sigma aliases y yc idcl in
+ let id = assoc_up_to_alias sigma aliases y idcl in
(id,ProjectVar)::subst1,subst2
with Not_found ->
(* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
(* projectable on [y] *)
- if with_evars then
- let f (c,_,id) = isEvar sigma c in
- let idcl' = List.filter f idcl in
- match idcl' with
- | [c,_,id] ->
- begin
- let (evk,argsv as t) = destEvar sigma c in
- let evi = Evd.find sigma evk in
- let subst,_ = make_projectable_subst aliases sigma evi argsv in
- let l = find_projectable_vars with_evars aliases sigma y subst in
- match l with
- | [id',p] -> (subst1,(id,ProjectEvar (t,evi,id',p))::subst2)
- | _ -> subst'
- end
- | [] -> subst'
- | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.")
- else
- subst' in
+ let f (c, id) = isEvar sigma c in
+ let idcl' = List.filter f idcl in
+ match idcl' with
+ | [c, id] ->
+ begin
+ let (evk,argsv as t) = destEvar sigma c in
+ let evi = Evd.find sigma evk in
+ let subst,_ = make_projectable_subst aliases sigma evi argsv in
+ let l = find_projectable_vars aliases sigma y subst in
+ match l with
+ | [id',p] -> (subst1,(id,ProjectEvar (t,evi,id',p))::subst2)
+ | _ -> subst'
+ end
+ | [] -> subst'
+ | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.")
+ in
let subst1,subst2 = Int.Map.fold is_projectable subst ([],[]) in
(* We return the substitution with ProjectVar first (from most
recent to oldest var), followed by ProjectEvar (from most recent
@@ -914,14 +905,15 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
let filter_solution = function
| [] -> raise Not_found
- | (id,p)::_::_ -> raise NotUnique
- | [id,p] -> (mkVar id, p)
+ | _ :: _ :: _ -> raise NotUnique
+ | [id] -> mkVar id
-let project_with_effects aliases sigma effects t subst =
- let c, p =
- filter_solution (find_projectable_vars false aliases sigma t subst) in
- effects := p :: !effects;
- c
+let project_with_effects aliases sigma t subst =
+ let is_projectable _ idcl accu =
+ try assoc_up_to_alias sigma aliases t idcl :: accu
+ with Not_found -> accu
+ in
+ filter_solution (Int.Map.fold is_projectable subst [])
open Context.Named.Declaration
let rec find_solution_type evarenv = function
@@ -981,28 +973,27 @@ let rec do_projection_effects unify flags define_fun env ty evd = function
type projectibility_kind =
| NoUniqueProjection
- | UniqueProjection of EConstr.constr * evar_projection list
+ | UniqueProjection of EConstr.constr
type projectibility_status =
| CannotInvert
| Invertible of projectibility_kind
let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
- let effects = ref [] in
let rec aux k t =
match EConstr.kind evd t with
| Rel i when i>k0+k -> aux' k (RelAlias (i-k))
| Var id -> aux' k (VarAlias id)
| _ -> map_with_binders evd succ aux k t
and aux' k t =
- try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
+ try project_with_effects aliases evd t subst_in_env_extended_with_k_binders
with Not_found ->
match expand_alias_once evd aliases t with
| None -> raise Not_found
| Some c -> aux k (Alias.eval (Alias.lift k c)) in
try
let c = aux 0 c_in_env_extended_with_k_binders in
- Invertible (UniqueProjection (c,!effects))
+ Invertible (UniqueProjection c)
with
| Not_found -> CannotInvert
| NotUnique -> Invertible NoUniqueProjection
@@ -1010,7 +1001,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
match res with
- | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
+ | Invertible (UniqueProjection c) when not (noccur_evar fullenv evd evk c)
->
CannotInvert
| _ ->
@@ -1019,7 +1010,7 @@ let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_
exception NotEnoughInformationToInvert
let extract_unique_projection = function
-| Invertible (UniqueProjection (c,_)) -> c
+| Invertible (UniqueProjection c) -> c
| _ ->
(* For instance, there are evars with non-invertible arguments and *)
(* we cannot arbitrarily restrict these evars before knowing if there *)
@@ -1518,7 +1509,7 @@ let rec invert_definition unify flags choose imitate_defs
let project_variable t =
(* Evar/Var problem: unifiable iff variable projectable from ev subst *)
try
- let sols = find_projectable_vars true aliases !evdref t subst in
+ let sols = find_projectable_vars aliases !evdref t subst in
let c, p = match sols with
| [] -> raise Not_found
| [id,p] -> (mkVar id, p)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a006c82993..cb868e0480 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -60,12 +60,20 @@ let glob_sort_family = let open Sorts in function
| UNamed [GSet,0] -> InSet
| _ -> raise ComplexSort
-let glob_sort_eq u1 u2 = match u1, u2 with
+let glob_sort_expr_eq f u1 u2 =
+ match u1, u2 with
| UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
- | UNamed l1, UNamed l2 ->
- List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n) l1 l2
+ | UNamed l1, UNamed l2 -> f l1 l2
| (UNamed _ | UAnonymous _), _ -> false
+let glob_sort_eq u1 u2 =
+ glob_sort_expr_eq
+ (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n))
+ u1 u2
+
+let glob_level_eq u1 u2 =
+ glob_sort_expr_eq glob_sort_name_eq u1 u2
+
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Explicit, Explicit -> true
| NonMaxImplicit, NonMaxImplicit -> true
@@ -123,7 +131,9 @@ let instance_eq f (x1,c1) (x2,c2) =
Id.equal x1 x2 && f c1 c2
let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
- | GRef (gr1, _), GRef (gr2, _) -> GlobRef.equal gr1 gr2
+ | GRef (gr1, u1), GRef (gr2, u2) ->
+ GlobRef.equal gr1 gr2 &&
+ Option.equal (List.equal glob_level_eq) u1 u2
| GVar id1, GVar id2 -> Id.equal id1 id2
| GEvar (id1, arg1), GEvar (id2, arg2) ->
Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 14bf2f6764..6da8173dce 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -15,6 +15,8 @@ open Glob_term
val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
+val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
+
val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
(** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 7be34d4cf1..c1ca40329a 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -28,16 +28,22 @@ exception Find_at of int
(* timing *)
-let timing_enabled = ref false
+let get_timing_enabled =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["NativeCompute"; "Timing"]
+ ~value:false
(* profiling *)
-let profiling_enabled = ref false
+let get_profiling_enabled =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["NativeCompute"; "Profiling"]
+ ~value:false
(* for supported platforms, filename for profiler results *)
-let profile_filename = ref "native_compute_profile.data"
-
let profiler_platform () =
match [@warning "-8"] Sys.os_type with
| "Unix" ->
@@ -48,10 +54,11 @@ let profiler_platform () =
| "Win32" -> "Windows (Win32)"
| "Cygwin" -> "Windows (Cygwin)"
-let get_profile_filename () = !profile_filename
-
-let set_profile_filename fn =
- profile_filename := fn
+let get_profile_filename =
+ Goptions.declare_string_option_and_ref
+ ~depr:false
+ ~key:["NativeCompute"; "Profile"; "Filename"]
+ ~value:"native_compute_profile.data"
(* find unused profile filename *)
let get_available_profile_filename () =
@@ -77,18 +84,6 @@ let get_available_profile_filename () =
let _ = Feedback.msg_info (Pp.str msg) in
assert false
-let get_profiling_enabled () =
- !profiling_enabled
-
-let set_profiling_enabled b =
- profiling_enabled := b
-
-let get_timing_enabled () =
- !timing_enabled
-
-let set_timing_enabled b =
- timing_enabled := b
-
let invert_tag cst tag reloc_tbl =
try
for j = 0 to Array.length reloc_tbl - 1 do
@@ -496,8 +491,8 @@ let stop_profiler 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 not Coq_config.native_compiler then
- user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
+ if not (Flags.get_native_compiler ()) then
+ user_err Pp.(str "Native_compute reduction has been disabled.")
else
(*
Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 4f18174261..73a8add6ec 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -14,16 +14,6 @@ open Evd
(** This module implements normalization by evaluation to OCaml code *)
-val get_profile_filename : unit -> string
-val set_profile_filename : string -> unit
-
-val get_profiling_enabled : unit -> bool
-val set_profiling_enabled : bool -> unit
-
-val get_timing_enabled : unit -> bool
-val set_timing_enabled : bool -> unit
-
-
val native_norm : env -> evar_map -> constr -> types -> constr
(** Conversion with inference of universe constraints *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ded159e484..940150b15a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -189,8 +189,10 @@ let interp_sort_info ?loc evd l =
type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
+type use_typeclasses = NoUseTC | UseTCForConv | UseTC
+
type inference_flags = {
- use_typeclasses : bool;
+ use_typeclasses : use_typeclasses;
solve_unification_constraints : bool;
fail_evar : bool;
expand_evars : bool;
@@ -231,7 +233,7 @@ let frozen_and_pending_holes (sigma, sigma') =
end in
FrozenProgress data
-let apply_typeclasses ~program_mode env sigma frozen fail_evar =
+let apply_typeclasses ~program_mode ~fail_evar env sigma frozen =
let filter_frozen = match frozen with
| FrozenId map -> fun evk -> Evar.Map.mem evk map
| FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
@@ -270,7 +272,7 @@ let apply_heuristics env sigma fail_evar =
let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen =
(* Naive way, call resolution again with failure flag *)
- apply_typeclasses ~program_mode env current_sigma frozen true
+ apply_typeclasses ~program_mode ~fail_evar:true env current_sigma frozen
let check_extra_evars_are_solved env current_sigma frozen = match frozen with
| FrozenId _ -> ()
@@ -312,9 +314,9 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
let program_mode = flags.program_mode in
let frozen = frozen_and_pending_holes (initial, sigma) in
let sigma =
- if flags.use_typeclasses
- then apply_typeclasses ~program_mode env sigma frozen false
- else sigma
+ match flags.use_typeclasses with
+ | UseTC -> apply_typeclasses ~program_mode ~fail_evar:false env sigma frozen
+ | NoUseTC | UseTCForConv -> sigma
in
let sigma = match hook with
| None -> sigma
@@ -436,7 +438,15 @@ let pretype_ref ?loc sigma env ref us =
match ref with
| GlobRef.VarRef id ->
(* Section variable *)
- (try sigma, make_judge (mkVar id) (NamedDecl.get_type (lookup_named id !!env))
+ (try
+ let ty = NamedDecl.get_type (lookup_named id !!env) in
+ (match us with
+ | None | Some [] -> ()
+ | Some (_ :: _) ->
+ CErrors.user_err ?loc
+ Pp.(str "Section variables are not polymorphic:" ++ spc ()
+ ++ str "universe instance should have length 0."));
+ sigma, make_judge (mkVar id) ty
with Not_found ->
(* This may happen if env is a goal env and section variables have
been cleared - section variables should be different from goal
@@ -1287,21 +1297,25 @@ let ise_pretype_gen flags env sigma lvar kind c =
if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
in
let env = GlobEnv.make ~hypnaming env sigma lvar in
+ let use_tc = match flags.use_typeclasses with
+ | NoUseTC -> false
+ | UseTC | UseTCForConv -> true
+ in
let sigma', c', c'_ty = match kind with
| WithoutTypeConstraint | UnknownIfTermOrType ->
- let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode ~poly use_tc empty_tycon env sigma c in
sigma, j.uj_val, j.uj_type
| OfType exptyp ->
- let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+ let sigma, j = pretype ~program_mode ~poly use_tc (mk_tycon exptyp) env sigma c in
sigma, j.uj_val, j.uj_type
| IsType ->
- let sigma, tj = pretype_type ~program_mode ~poly flags.use_typeclasses empty_valcon env sigma c in
+ let sigma, tj = pretype_type ~program_mode ~poly use_tc empty_valcon env sigma c in
sigma, tj.utj_val, mkSort tj.utj_type
in
process_inference_flags flags !!env sigma (sigma',c',c'_ty)
let default_inference_flags fail = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = fail;
expand_evars = true;
@@ -1310,7 +1324,7 @@ let default_inference_flags fail = {
}
let no_classes_no_fail_inference_flags = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index abbb745161..8be7b1477b 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -44,8 +44,17 @@ type typing_constraint =
| OfType of types (** A term of the expected type *)
| WithoutTypeConstraint (** A term of unknown expected type *)
+type use_typeclasses = NoUseTC | UseTCForConv | UseTC
+(** Typeclasses are used in 2 ways:
+
+- through the "Typeclass Resolution For Conversion" option, if a
+ conversion problem fails we try again after resolving typeclasses
+ (UseTCForConv and UseTC)
+- after pretyping we resolve typeclasses (UseTC) (in [solve_remaining_evars])
+*)
+
type inference_flags = {
- use_typeclasses : bool;
+ use_typeclasses : use_typeclasses;
solve_unification_constraints : bool;
fail_evar : bool;
expand_evars : bool;
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1e4b537117..f7456ef35e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -30,14 +30,6 @@ exception Elimconst
their parameters in its stack.
*)
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Cumulativity";"Weak";"Constraints"];
- optread = (fun () -> not !UState.drop_weak_constraints);
- optwrite = (fun a -> UState.drop_weak_constraints:=not a);
-})
-
-
(** Support for reduction effects *)
open Mod_subst
@@ -622,9 +614,8 @@ type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
evar_map -> constr -> constr * constr list
-type contextual_state_reduction_function =
+type state_reduction_function =
env -> evar_map -> state -> state
-type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
let pr_state env sigma (tm,sk) =
@@ -716,7 +707,7 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
f x := t. End M. Definition f := u. and say goodbye to any hope
of refolding M.f this way ...
*)
-let magicaly_constant_of_fixbody env sigma reference bd = function
+let magically_constant_of_fixbody env sigma reference bd = function
| Name.Anonymous -> bd
| Name.Name id ->
let open UnivProblem in
@@ -758,7 +749,7 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo
| Some e ->
match reference with
| None -> bd
- | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+ | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -800,7 +791,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
| Some e ->
match reference with
| None -> bd
- | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+ | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -967,13 +958,11 @@ module CredNative = RedNative(CNativeEntries)
contract_* in any case .
*)
-let debug_RAKAM = ref (false)
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Debug";"RAKAM"];
- optread = (fun () -> !debug_RAKAM);
- optwrite = (fun a -> debug_RAKAM:=a);
-})
+let debug_RAKAM =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Debug";"RAKAM"]
+ ~value:false
let equal_stacks sigma (x, l) (y, l') =
let f_equal x y = eq_constr sigma x y in
@@ -984,7 +973,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let open Context.Named.Declaration in
let open ReductionBehaviour in
let rec whrec cst_l (x, stack) =
- let () = if !debug_RAKAM then
+ let () = if debug_RAKAM () then
let open Pp in
let pr c = Termops.Internal.print_constr_env env sigma c in
Feedback.msg_debug
@@ -995,7 +984,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
in
let c0 = EConstr.kind sigma x in
let fold () =
- let () = if !debug_RAKAM then
+ let () = if debug_RAKAM () then
let open Pp in Feedback.msg_debug (str "<><><><><>") in
((EConstr.of_kind c0, stack),cst_l)
in
@@ -1571,10 +1560,6 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
(* Special-Purpose Reduction *)
(********************************************************************)
-let whd_meta sigma c = match EConstr.kind sigma c with
- | Meta p -> (try meta_value sigma p with Not_found -> c)
- | _ -> c
-
let default_plain_instance_ident = Id.of_string "H"
(* Try to replace all metas. Does not replace metas in the metas' values
@@ -1751,26 +1736,46 @@ let is_sort env sigma t =
let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
let refold = false in
let tactic_mode = false in
- let rec whrec csts s =
- let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in
+ let all' = CClosure.RedFlags.red_add_transparent CClosure.all ts in
+ (* Unset the sharing flag to get a call-by-name reduction. This matters for
+ the shape of the generated term. *)
+ let env' = Environ.set_typing_flags { (Environ.typing_flags env) with Declarations.share_reduction = false } env in
+ let whd_opt c =
+ let open CClosure in
+ let evars ev = safe_evar_value sigma ev in
+ let infos = create_clos_infos ~evars all' env' in
+ let tab = create_tab () in
+ let c = inject (EConstr.Unsafe.to_constr (Stack.zip sigma c)) in
+ let (c, stk) = whd_stack infos tab c [] in
+ match fterm_of c with
+ | (FConstruct _ | FCoFix _) ->
+ (* Non-neutral normal, can trigger reduction below *)
+ let c = EConstr.of_constr (term_of_process c stk) in
+ Some (decompose_app_vect sigma c)
+ | _ -> None
+ in
+ let rec whrec s =
+ let (t, stack as s), _ = whd_state_gen ~refold ~tactic_mode CClosure.betaiota env sigma s in
match Stack.strip_app stack with
|args, (Stack.Case _ :: _ as stack') ->
- let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
- (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
- if reducible_mind_case sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+ begin match whd_opt (t, args) with
+ | Some (t_o, args) when reducible_mind_case sigma t_o -> whrec (t_o, Stack.append_app args stack')
+ | (Some _ | None) -> s
+ end
|args, (Stack.Fix _ :: _ as stack') ->
- let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
- (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
- if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+ begin match whd_opt (t, args) with
+ | Some (t_o, args) when isConstruct sigma t_o -> whrec (t_o, Stack.append_app args stack')
+ | (Some _ | None) -> s
+ end
|args, (Stack.Proj (p,_) :: stack'') ->
- let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
- (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
- if isConstruct sigma t_o then
- whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
- else s,csts'
- |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s,csts'
+ begin match whd_opt (t, args) with
+ | Some (t_o, args) when isConstruct sigma t_o ->
+ whrec (args.(Projection.npars p + Projection.arg p), stack'')
+ | (Some _ | None) -> s
+ end
+ |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s
in
- fst (whrec Cst_stack.empty s)
+ whrec s
let find_conclusion env sigma =
let rec decrec env c =
@@ -1810,70 +1815,3 @@ let meta_instance sigma b =
let nf_meta sigma c =
let cl = mk_freelisted c in
meta_instance sigma { cl with rebus = cl.rebus }
-
-(* Instantiate metas that create beta/iota redexes *)
-
-let meta_reducible_instance evd b =
- let fm = b.freemetas in
- let fold mv accu =
- let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in
- match fvalue with
- | None -> accu
- | Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu
- in
- let metas = Metaset.fold fold fm Metamap.empty in
- let rec irec u =
- let u = whd_betaiota Evd.empty u (* FIXME *) in
- match EConstr.kind evd u with
- | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
- let m = destMeta evd (strip_outer_cast evd c) in
- (match
- try
- let g, s = Metamap.find m metas in
- let is_coerce = match s with CoerceToType -> true | _ -> false in
- if isConstruct evd g || not is_coerce then Some g else None
- with Not_found -> None
- with
- | Some g -> irec (mkCase (ci,p,g,bl))
- | None -> mkCase (ci,irec p,c,Array.map irec bl))
- | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
- let m = destMeta evd (strip_outer_cast evd f) in
- (match
- try
- let g, s = Metamap.find m metas in
- let is_coerce = match s with CoerceToType -> true | _ -> false in
- if isLambda evd g || not is_coerce then Some g else None
- with Not_found -> None
- with
- | Some g -> irec (mkApp (g,l))
- | None -> mkApp (f,Array.map irec l))
- | Meta m ->
- (try let g, s = Metamap.find m metas in
- 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)) (* 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
- let is_coerce = match s with CoerceToType -> true | _ -> false in
- if isConstruct evd g || not is_coerce then Some g else None
- with Not_found -> None
- with
- | Some g -> irec (mkProj (p,g))
- | None -> mkProj (p,c))
- | _ -> EConstr.map evd irec u
- in
- if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
- else irec b.rebus
-
-let betazetaevar_applist sigma n c l =
- let rec stacklam n env t stack =
- if Int.equal n 0 then applist (substl env t, stack) else
- match EConstr.kind sigma t, stack with
- | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
- | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
- | Evar _, _ -> applist (substl env t, stack)
- | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
- stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5202380a13..243a2745f0 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -139,9 +139,8 @@ type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
evar_map -> constr -> constr * constr list
-type contextual_state_reduction_function =
+type state_reduction_function =
env -> evar_map -> state -> state
-type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
val pr_state : env -> evar_map -> state -> Pp.t
@@ -203,8 +202,8 @@ val whd_nored_state : local_state_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
val whd_betaiotazeta_state : local_state_reduction_function
-val whd_all_state : contextual_state_reduction_function
-val whd_allnolet_state : contextual_state_reduction_function
+val whd_all_state : state_reduction_function
+val whd_allnolet_state : state_reduction_function
val whd_betalet_state : local_state_reduction_function
(** {6 Head normal forms } *)
@@ -309,13 +308,6 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env ->
evar_map -> constr -> constr -> evar_map option
-(** {6 Special-Purpose Reduction Functions } *)
-
-val whd_meta : local_reduction_function
-val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
-val instance : evar_map -> constr Metamap.t -> constr -> constr
-val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
-
(** {6 Heuristic for Conversion with Evar } *)
val whd_betaiota_deltazeta_for_iota_state :
@@ -324,4 +316,3 @@ val whd_betaiota_deltazeta_for_iota_state :
(** {6 Meta-related reduction functions } *)
val meta_instance : evar_map -> constr freelisted -> constr
val nf_meta : evar_map -> constr -> constr
-val meta_reducible_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 821c57d033..1f091c3df8 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -97,6 +97,16 @@ let decomp_sort env sigma t =
let destSort sigma s = ESorts.kind sigma (destSort sigma s)
+let betazetaevar_applist sigma n c l =
+ let rec stacklam n env t stack =
+ if Int.equal n 0 then applist (substl env t, stack) else
+ match EConstr.kind sigma t, stack with
+ | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+ | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
+ | Evar _, _ -> applist (substl env t, stack)
+ | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
+ stacklam n [] c l
+
let retype ?(polyprop=true) sigma =
let rec type_of env cstr =
match EConstr.kind sigma cstr with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ec3fb0758e..e168f6d1b6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,23 +43,17 @@ type subst0 =
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-let keyed_unification = ref (false)
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Keyed";"Unification"];
- optread = (fun () -> !keyed_unification);
- optwrite = (fun a -> keyed_unification:=a);
-})
-
-let is_keyed_unification () = !keyed_unification
-
-let debug_unification = ref (false)
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Debug";"Tactic";"Unification"];
- optread = (fun () -> !debug_unification);
- optwrite = (fun a -> debug_unification:=a);
-})
+let is_keyed_unification =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Keyed";"Unification"]
+ ~value:false
+
+let debug_unification =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Debug";"Tactic";"Unification"]
+ ~value:false
(** Making this unification algorithm correct w.r.t. the evar-map abstraction
breaks too much stuff. So we redefine incorrect functions here. *)
@@ -87,6 +81,12 @@ let occur_meta_or_undefined_evar evd c =
| _ -> Constr.iter occrec c
in try occrec c; false with Occur | Not_found -> true
+let whd_meta sigma c = match EConstr.kind sigma c with
+ | Meta p ->
+ (try Evd.meta_value sigma p with Not_found -> c)
+ (* Not recursive, for some reason *)
+ | _ -> c
+
let occur_meta_evd sigma mv c =
let rec occrec c =
(* Note: evars are not instantiated by terms with metas *)
@@ -696,7 +696,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let cM = Evarutil.whd_head_evar sigma curm
and cN = Evarutil.whd_head_evar sigma curn in
let () =
- if !debug_unification then
+ if debug_unification () then
Feedback.msg_debug (
Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
Termops.Internal.print_constr_env curenv sigma cN)
@@ -1121,7 +1121,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- if !debug_unification then Feedback.msg_debug (str "Starting unification");
+ if debug_unification () then Feedback.msg_debug (str "Starting unification");
let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
try
let res =
@@ -1146,11 +1146,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let a = match res with
| Some sigma -> sigma, ms, es
| None -> unirec_rec (env,0) cv_pb opt subst m n in
- if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
+ if debug_unification () then Feedback.msg_debug (str "Leaving unification with success");
a
with e ->
let e = Exninfo.capture e in
- if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
+ if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure");
Exninfo.iraise e
let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
@@ -1739,7 +1739,7 @@ let make_abstraction env evd ccl abs =
env evd c ty occs check_occs ccl
let keyed_unify env evd kop =
- if not !keyed_unification then fun cl -> true
+ if not (is_keyed_unification ()) then fun cl -> true
else
match kop with
| None -> fun _ -> true
@@ -1761,7 +1761,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
(try
if closed0 evd cl && not (isEvar evd cl) && keyed_unify env evd kop cl then
(try
- if !keyed_unification then
+ if is_keyed_unification () then
let f1, l1 = decompose_app_vect evd op in
let f2, l2 = decompose_app_vect evd cl in
w_typed_unify_array env evd flags f1 l1 f2 l2,cl
@@ -1907,7 +1907,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
else
let allow_K = flags.allow_K_in_toplevel_higher_order_unification in
let flags =
- if unsafe_occur_meta_or_existential op || !keyed_unification then
+ if unsafe_occur_meta_or_existential op || is_keyed_unification () then
(* This is up to delta for subterms w/o metas ... *)
flags
else
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 64068724af..d4da93cc5b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -73,7 +73,7 @@ let type_constructor mind mib u (ctx, typ) params =
if Int.equal ndecls 0 then ctyp
else
let _,ctyp = decompose_prod_n_assum ndecls ctyp in
- substl (List.rev (adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params)))
+ substl (subst_of_rel_context_instance mib.mind_params_ctxt (Array.to_list params))
ctyp
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:05:45 +0000