aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/constr_matching.ml2
-rw-r--r--pretyping/detyping.ml116
-rw-r--r--pretyping/detyping.mli7
-rw-r--r--pretyping/evarconv.ml85
-rw-r--r--pretyping/evardefine.ml6
-rw-r--r--pretyping/evarsolve.ml152
-rw-r--r--pretyping/evarsolve.mli4
-rw-r--r--pretyping/glob_ops.ml18
-rw-r--r--pretyping/glob_ops.mli2
-rw-r--r--pretyping/nativenorm.ml65
-rw-r--r--pretyping/nativenorm.mli10
-rw-r--r--pretyping/pattern.ml2
-rw-r--r--pretyping/patternops.ml6
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/reductionops.ml74
-rw-r--r--pretyping/tacred.ml6
-rw-r--r--pretyping/unification.ml53
-rw-r--r--pretyping/vnorm.ml3
19 files changed, 306 insertions, 319 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index f816599a17..b39ec37cd1 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -446,7 +446,7 @@ let rec norm_head info env t stack =
Some c -> norm_head info env c stack
| None ->
let e, xs = ev in
- let xs' = Array.map (apply_env env) xs in
+ let xs' = List.map (apply_env env) xs in
(VAL(0, mkEvar (e,xs')), stack))
(* non-neutral cases *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index f85635528d..25aa8915ba 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -404,7 +404,7 @@ let matches_core env sigma allow_bound_rels
Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
| PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
- Array.fold_left2 (sorec ctx env) subst args1 args2
+ List.fold_left2 (sorec ctx env) subst args1 args2
| PInt i1, Int i2 when Uint63.equal i1 i2 -> subst
| PFloat f1, Float f2 when Float64.equal f1 f2 -> subst
| (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 73be36d031..ff278baf9f 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) ->
@@ -812,7 +790,7 @@ and detype_r d flags avoid env sigma t =
id,l
with Not_found ->
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
- (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
+ (List.map (fun c -> (Id.of_string "__",c)) cl)
in
GEvar (id,
List.map (on_snd (detype d flags avoid env sigma)) l)
@@ -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..f1506f5f59 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 *)
@@ -199,7 +195,7 @@ let occur_rigidly flags env evd (evk,_) t =
| Evar (evk',l as ev) ->
if Evar.equal evk evk' then Rigid true
else if is_frozen flags ev then
- Rigid (Array.exists (fun x -> rigid_normal_occ (aux x)) l)
+ Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
else Reducible
| Cast (p, _, _) -> aux p
| Lambda (na, t, b) -> aux b
@@ -355,6 +351,14 @@ let ise_array2 evd f v1 v2 =
if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1)
else UnifFailure (evd,NotSameArgSize)
+let rec ise_inst2 evd f l1 l2 = match l1, l2 with
+| [], [] -> Success evd
+| [], (_ :: _) | (_ :: _), [] -> assert false
+| c1 :: l1, c2 :: l2 ->
+ match ise_inst2 evd f l1 l2 with
+ | Success evd' -> f evd' c1 c2
+ | UnifFailure _ as x -> x
+
(* Applicative node of stack are read from the outermost to the innermost
but are unified the other way. *)
let rec ise_app_stack2 env f evd sk1 sk2 =
@@ -767,7 +771,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,
@@ -1023,7 +1027,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
if Evar.equal sp1 sp2 then
match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with
|None, Success i' ->
- ise_array2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2
+ ise_inst2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2
|_, (UnifFailure _ as x) -> x
|Some _, _ -> UnifFailure (evd,NotSameArgSize)
else UnifFailure (evd,NotSameHead)
@@ -1224,16 +1228,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))
@@ -1245,6 +1249,7 @@ let filter_possible_projections evd c ty ctxt args =
(* Since args in the types will be replaced by holes, we count the
fv of args to have a well-typed filter; don't know how necessary
it is however to have a well-typed filter here *)
+ let args = Array.of_list args in
let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in
let fv2 = collect_vars evd (mkApp (c,args)) in
let len = Array.length args in
@@ -1313,8 +1318,8 @@ let thin_evars env sigma sign c =
match kind !sigma t with
| Evar (ev, args) ->
let evi = Evd.find_undefined !sigma ev in
- let filter = Array.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in
- let filter = Filter.make (Array.to_list filter) in
+ let filter = List.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in
+ let filter = Filter.make filter in
let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in
let evd, ev = restrict_evar !sigma ev filter candidates in
sigma := evd; whd_evar !sigma t
@@ -1337,12 +1342,12 @@ 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
+ let args = List.map (nf_evar evd) args in
let vars = List.map NamedDecl.get_id ctxt in
- let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in
+ let argsubst = List.map2 (fun id c -> (id, c)) vars args in
let instance = List.map mkVar vars in
let rhs = nf_evar evd rhs in
if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd);
@@ -1374,7 +1379,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 +1387,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 +1398,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,21 +1418,21 @@ 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
set_holes env_rhs' evd rhs' subst
| [] -> evd, rhs in
- let subst = make_subst (ctxt,Array.to_list args,argoccs) in
+ let subst = make_subst (ctxt,args,argoccs) in
let evd, rhs' = set_holes env_rhs evd rhs subst in
let rhs' = nf_evar evd rhs' in
(* 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 +1442,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 +1450,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 +1481,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 +1496,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 +1509,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'
@@ -1537,7 +1542,7 @@ let default_evar_selection flags evd (ev,args) =
in spec :: aux args abs
| l, [] -> List.map (fun _ -> default_occurrence_selection) l
| [], _ :: _ -> assert false
- in aux (Array.to_list args) evi.evar_abstract_arguments
+ in aux args evi.evar_abstract_arguments
let second_order_matching_with_args flags env evd with_ho pbty ev l t =
if with_ho then
@@ -1564,7 +1569,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/evardefine.ml b/pretyping/evardefine.ml
index 50187d82cc..71edcaa231 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -113,7 +113,7 @@ let define_evar_as_product env evd (evk,args) =
(* Quick way to compute the instantiation of evk with args *)
let na,dom,rng = destProd evd prod in
let evdom = mkEvar (fst (destEvar evd dom), args) in
- let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+ let evrngargs = mkRel 1 :: List.map (lift 1) args in
let evrng = mkEvar (fst (destEvar evd rng), evrngargs) in
evd, mkProd (na, evdom, evrng)
@@ -152,7 +152,7 @@ let define_evar_as_lambda env evd (evk,args) =
let evd,lam = define_pure_evar_as_lambda env evd evk in
(* Quick way to compute the instantiation of evk with args *)
let na,dom,body = destLambda evd lam in
- let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+ let evbodyargs = mkRel 1 :: List.map (lift 1) args in
let evbody = mkEvar (fst (destEvar evd body), evbodyargs) in
evd, mkLambda (na, dom, evbody)
@@ -163,7 +163,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function
let evd,lam = define_pure_evar_as_lambda env evd evk in
let _,_,body = destLambda evd lam in
let evk = fst (destEvar evd body) in
- evar_absorb_arguments env evd (evk, Array.cons a args) l
+ evar_absorb_arguments env evd (evk, a :: args) l
(* Refining an evar to a sort *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4eae0cf86c..34684e4a34 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -217,7 +217,7 @@ type 'a update =
| NoUpdate
open Context.Named.Declaration
-let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign
+let inst_of_vars sign = List.map (get_id %> mkVar) sign
let restrict_evar_key evd evk filter candidates =
match filter, candidates with
@@ -247,7 +247,7 @@ let restrict_applied_evar evd (evk,argsv) filter candidates =
| Some filter ->
let evi = Evd.find evd evk in
let subfilter = Filter.compose (evar_filter evi) filter in
- Filter.filter_array subfilter argsv in
+ Filter.filter_list subfilter argsv in
evd,(newevk,newargsv)
(* Restrict an evar in the current evar_map *)
@@ -258,7 +258,7 @@ let restrict_evar evd evk filter candidates =
let restrict_instance evd evk filter argsv =
match filter with None -> argsv | Some filter ->
let evi = Evd.find evd evk in
- Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
+ Filter.filter_list (Filter.compose (evar_filter evi) filter) argsv
open Context.Rel.Declaration
let noccur_evar env evd evk c =
@@ -269,7 +269,7 @@ let noccur_evar env evd evk c =
if Evar.equal evk evk' then raise Occur
else (if check_types then
occur_rec false acc (existential_type evd ev');
- Array.iter (occur_rec check_types acc) args')
+ List.iter (occur_rec check_types acc) args')
| Rel i when i > k ->
if not (Int.Set.mem (i-k) !cache) then
let decl = Environ.lookup_rel i env in
@@ -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
@@ -561,17 +552,13 @@ let get_actual_deps env evd aliases l t =
open Context.Named.Declaration
let remove_instance_local_defs evd evk args =
let evi = Evd.find evd evk in
- let len = Array.length args in
- let rec aux sign i = match sign with
- | [] ->
- let () = assert (i = len) in []
- | LocalAssum _ :: sign ->
- let () = assert (i < len) in
- (Array.unsafe_get args i) :: aux sign (succ i)
- | LocalDef _ :: sign ->
- aux sign (succ i)
+ let rec aux sign args = match sign, args with
+ | [], [] -> []
+ | LocalAssum _ :: sign, c :: args -> c :: aux sign args
+ | LocalDef _ :: sign, _ :: args -> aux sign args
+ | _ -> assert false
in
- aux (evar_filtered_context evi) 0
+ aux (evar_filtered_context evi) args
(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
@@ -678,7 +665,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,16 +675,16 @@ 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
+ sign (List.rev args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in
(full_subst,cstr_subst)
(*------------------------------------*
@@ -774,7 +761,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
(mkRel 1)::(List.map (lift 1) inst_in_sign),
push_rel d env,evd,Id.Set.add id.binder_name avoid))
rel_sign
- (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid)
+ (sign1,filter1,args1,inst_in_sign,env1,evd,avoid)
in
let evd,ev2ty_in_sign =
let s = Retyping.get_sort_of env evd ty_in_env in
@@ -784,11 +771,12 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
ty_t_in_sign sign2 filter2 inst2_in_env in
let (evd, ev2_in_sign) =
new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
- let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in
+ let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in
(evd, ev2_in_sign, ev2_in_env)
let restrict_upon_filter evd evk p args =
let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
+ let args = Array.of_list args in
let len = Array.length args in
Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i))
@@ -862,47 +850,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 +902,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 +970,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 +998,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 +1007,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 *)
@@ -1043,7 +1031,7 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
let p = invert_arg fullenv evd aliases k evk subst arg in
extract_unique_projection p
in
- Array.map invert args'
+ List.map invert args'
(* Redefines an evar with a smaller context (i.e. it may depend on less
* variables) such that c becomes closed.
@@ -1399,9 +1387,9 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 =
try evdref := Evd.add_universe_constraints !evdref cstr; true
with UniversesDiffer -> false
in
- if Array.equal eq_constr argsv1 argsv2 then !evdref else
+ if List.equal eq_constr argsv1 argsv2 then !evdref else
(* Filter and restrict if needed *)
- let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
+ let args = List.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
let untypedfilter =
restrict_upon_filter evd evk
(fun (a1,a2) -> unify flags TermUnification env evd Reduction.CONV a1 a2) args in
@@ -1461,7 +1449,7 @@ let occur_evar_upto_types sigma n c =
| Evar (sp,_) when Evar.equal sp n -> raise Occur
| Evar (sp,args as e) ->
if Evar.Set.mem sp !seen then
- Array.iter occur_rec args
+ List.iter occur_rec args
else (
seen := Evar.Set.add sp !seen;
Option.iter occur_rec (existential_opt_value0 sigma e);
@@ -1518,7 +1506,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)
@@ -1579,7 +1567,7 @@ let rec invert_definition unify flags choose imitate_defs
(* Evar/Evar problem (but left evar is virtual) *)
let aliases = lift_aliases k aliases in
(try
- let ev = (evk,Array.map (lift k) argsv) in
+ let ev = (evk,List.map (lift k) argsv) in
let evd,body = project_evar_on_evar false unify flags env' !evdref aliases k None ev' ev in
evdref := evd;
body
@@ -1657,7 +1645,7 @@ let rec invert_definition unify flags choose imitate_defs
| [], [] -> true
| _ -> false
in
- is_id_subst filter_ctxt (Array.to_list argsv) &&
+ is_id_subst filter_ctxt argsv &&
closed0 evd rhs &&
Id.Set.subset (collect_vars evd rhs) !names
in
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 0a1b731e6b..3fb80432ad 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -99,7 +99,7 @@ val refresh_universes :
env -> evar_map -> types -> evar_map * types
val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env -> evar_map ->
- bool option -> Evar.t -> constr array -> constr array -> evar_map
+ bool option -> Evar.t -> constr list -> constr list -> evar_map
val solve_evar_evar : ?force:bool ->
(env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
@@ -128,7 +128,7 @@ val check_evar_instance : unifier -> unify_flags ->
env -> evar_map -> Evar.t -> constr -> evar_map
val remove_instance_local_defs :
- evar_map -> Evar.t -> 'a array -> 'a list
+ evar_map -> Evar.t -> 'a list -> 'a list
val get_type_of_refresh :
?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
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 f989dae4c9..d672ddc906 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
@@ -428,8 +423,8 @@ and nf_evar env sigma evk args =
let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
let ty = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
if List.is_empty hyps then begin
- assert (Int.equal (Array.length args) 0);
- mkEvar (evk, [||]), ty
+ assert (Array.is_empty args);
+ mkEvar (evk, []), ty
end
else
(* Let-bound arguments are present in the evar arguments but not
@@ -441,7 +436,7 @@ and nf_evar env sigma evk args =
(* nf_args takes arguments in the reverse order but produces them
in the correct one, so we have to reverse them again for the
evar node *)
- mkEvar (evk, Array.rev_of_list args), ty
+ mkEvar (evk, List.rev args), ty
let evars_of_evar_map sigma =
{ Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
@@ -503,25 +498,29 @@ let native_norm env sigma c ty =
Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
*)
- let ml_filename, prefix = Nativelib.get_ml_filename () in
- let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
let profile = get_profiling_enabled () in
let print_timing = get_timing_enabled () in
- let tc0 = Sys.time () in
+ let ml_filename, prefix = Nativelib.get_ml_filename () in
+ let tnc0 = Unix.gettimeofday () in
+ let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
+ let tnc1 = Unix.gettimeofday () in
+ let time_info = Format.sprintf "native_compute: Conversion to native code done in %.5f" (tnc1 -. tnc0) in
+ if print_timing then Feedback.msg_info (Pp.str time_info);
+ let tc0 = Unix.gettimeofday () in
let fn = Nativelib.compile ml_filename code ~profile:profile in
- let tc1 = Sys.time () in
- let time_info = Format.sprintf "native_compute: Compilation done in %.5f@." (tc1 -. tc0) in
+ let tc1 = Unix.gettimeofday () in
+ let time_info = Format.sprintf "native_compute: Compilation done in %.5f" (tc1 -. tc0) in
if print_timing then Feedback.msg_info (Pp.str time_info);
let profiler_pid = if profile then start_profiler () else None in
- let t0 = Sys.time () in
+ let t0 = Unix.gettimeofday () in
Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd);
- let t1 = Sys.time () in
+ let t1 = Unix.gettimeofday () in
if profile then stop_profiler profiler_pid;
- let time_info = Format.sprintf "native_compute: Evaluation done in %.5f@." (t1 -. t0) in
+ let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in
if print_timing then Feedback.msg_info (Pp.str time_info);
let res = nf_val env sigma !Nativelib.rt1 ty in
- let t2 = Sys.time () in
- let time_info = Format.sprintf "native_compute: Reification done in %.5f@." (t2 -. t1) in
+ let t2 = Unix.gettimeofday () in
+ let time_info = Format.sprintf "native_compute: Reification done in %.5f" (t2 -. t1) in
if print_timing then Feedback.msg_info (Pp.str time_info);
EConstr.of_constr res
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/pattern.ml b/pretyping/pattern.ml
index 3f2e690da5..1dfb8b2cd1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -24,7 +24,7 @@ type case_info_pattern =
type constr_pattern =
| PRef of GlobRef.t
| PVar of Id.t
- | PEvar of Evar.t * constr_pattern array
+ | PEvar of constr_pattern Constr.pexistential
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b8635d03b7..6d30e0338e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -31,7 +31,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
| PRef r1, PRef r2 -> GlobRef.equal r1 r2
| PVar v1, PVar v2 -> Id.equal v1 v2
| PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
- Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
+ Evar.equal ev1 ev2 && List.equal constr_pattern_eq ctx1 ctx2
| PRel i1, PRel i2 ->
Int.equal i1 i2
| PApp (t1, arg1), PApp (t2, arg2) ->
@@ -115,7 +115,7 @@ let rec occurn_pattern n = function
(occurn_pattern n c) ||
(List.exists (fun (_,_,p) -> occurn_pattern n p) br)
| PMeta _ | PSoApp _ -> true
- | PEvar (_,args) -> Array.exists (occurn_pattern n) args
+ | PEvar (_,args) -> List.exists (occurn_pattern n) args
| PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false
| PFix (_,(_,tl,bl)) ->
Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
@@ -190,7 +190,7 @@ let pattern_of_constr env sigma t =
(* These are the two evar kinds used for existing goals *)
(* see Proofview.mark_in_evm *)
if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev)
- else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+ else PEvar (evk,List.map (pattern_of_constr env) ctxt)
| Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
PMeta None)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 015c26531a..f7e3d651ff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -438,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
@@ -599,7 +607,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
((id,c)::subst, update, sigma) in
let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in
check_instance loc subst inst;
- sigma, Array.map_of_list snd subst
+ sigma, List.map snd subst
module Default =
struct
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8bb268a92e..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
@@ -966,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
@@ -983,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
@@ -994,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
@@ -1746,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 =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 70605d58ab..2c717b8774 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -86,7 +86,7 @@ let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
| EvalVar id1, EvalVar id2 -> Id.equal id1 id2
| EvalRel i1, EvalRel i2 -> Int.equal i1 i2
| EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
- Evar.equal e1 e2 && Array.equal (EConstr.eq_constr sigma) ctx1 ctx2
+ Evar.equal e1 e2 && List.equal (EConstr.eq_constr sigma) ctx1 ctx2
| _ -> false
let mkEvalRef ref u =
@@ -408,7 +408,7 @@ let substl_with_function subst sigma constr =
let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in
evd := sigma;
minargs := Evar.Map.add evk min !minargs;
- Vars.lift k (mkEvar (evk, [|fx;ref|]))
+ Vars.lift k (mkEvar (evk, [fx; ref]))
| (fx, None) -> Vars.lift k fx
else mkRel (i - Array.length v)
| _ ->
@@ -455,7 +455,7 @@ let substl_checking_arity env subst sigma c =
(* we propagate the constraints: solved problems are substituted;
the other ones are replaced by the function symbol *)
let rec nf_fix c = match EConstr.kind sigma c with
- | Evar (i,[|fx;f|]) when Evar.Map.mem i minargs ->
+ | Evar (i,[fx;f]) when Evar.Map.mem i minargs ->
(* FIXME: find a less hackish way of doing this *)
begin match EConstr.kind sigma' c with
| Evar _ -> f
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 90dde01915..f5aaac315a 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. *)
@@ -82,7 +76,7 @@ let occur_meta_or_undefined_evar evd c =
| Evar (ev,args) ->
(match evar_body (Evd.find evd ev) with
| Evar_defined c ->
- occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args
+ occrec (EConstr.Unsafe.to_constr c); List.iter occrec args
| Evar_empty -> raise Occur)
| _ -> Constr.iter occrec c
in try occrec c; false with Occur | Not_found -> true
@@ -144,9 +138,9 @@ let abstract_list_all env evd typ c l =
error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
evd,(p,typp)
-let set_occurrences_of_last_arg args =
+let set_occurrences_of_last_arg n =
Evarconv.AtOccurrences AllOccurrences ::
- List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args)
+ List.tl (List.init n (fun _ -> Evarconv.Unspecified Abstraction.Abstract))
let occurrence_test _ _ _ env sigma _ c1 c2 =
match EConstr.eq_constr_universes env sigma c1 c2 with
@@ -159,7 +153,8 @@ let abstract_list_all_with_dependencies env evd typ c l =
let (evd, ev) = new_evar env evd typ in
let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in
let n = List.length l in
- let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
+ let () = assert (n <= List.length (snd ev')) in
+ let argoccs = set_occurrences_of_last_arg n in
let evd,b =
Evarconv.second_order_matching
(Evarconv.default_flags_of TransparentState.empty)
@@ -629,7 +624,7 @@ let subst_defined_metas_evars sigma (bl,el) c =
substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl)))
| Evar (evk,args) ->
let eq c1 c2 = Constr.equal c1 (EConstr.Unsafe.to_constr c2) in
- let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.for_all2 eq args args' in
+ let select (_,(evk',args'),_) = Evar.equal evk evk' && List.for_all2 eq args args' in
(try substrec (EConstr.Unsafe.to_constr (pi3 (List.find select el)))
with Not_found -> Constr.map substrec c)
| _ -> Constr.map substrec c
@@ -702,7 +697,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)
@@ -1127,7 +1122,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 =
@@ -1152,11 +1147,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
@@ -1745,7 +1740,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
@@ -1767,7 +1762,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
@@ -1913,7 +1908,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 d4da93cc5b..37c34d55cf 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -205,7 +205,7 @@ and nf_evar env sigma evk stk =
let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
if List.is_empty hyps then
- nf_stk env sigma (mkEvar (evk, [||])) concl stk
+ nf_stk env sigma (mkEvar (evk, [])) concl stk
else match stk with
| Zapp args :: stk ->
(* We assume that there is no consecutive Zapp nodes in a VM stack. Is that
@@ -217,6 +217,7 @@ and nf_evar env sigma evk stk =
let t = List.fold_left fold concl hyps in
let t, args = nf_args env sigma args t in
let inst, args = Array.chop (List.length hyps) args in
+ let inst = Array.to_list inst in
let c = mkApp (mkEvar (evk, inst), args) in
nf_stk env sigma c t stk
| _ ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 00:03:01 +0000