aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh6
-rw-r--r--engine/evd.ml4
-rw-r--r--engine/uState.ml2
-rw-r--r--engine/universes.ml34
-rw-r--r--engine/universes.mli9
-rw-r--r--plugins/ltac/tactic_matching.ml2
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/constr_matching.mli2
8 files changed, 29 insertions, 34 deletions
diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
new file mode 100644
index 0000000000..517088a247
--- /dev/null
+++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then
+
+ ltac2_CI_BRANCH=fast-constr-match-no-context
+ ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi
diff --git a/engine/evd.ml b/engine/evd.ml
index af22de5cd4..20a7c80ea0 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -842,12 +842,12 @@ let universe_rigidity evd l =
else UnivRigid
let normalize_universe evd =
- let vars = ref (UState.subst evd.universes) in
+ let vars = UState.subst evd.universes in
let normalize = Universes.normalize_universe_opt_subst vars in
normalize
let normalize_universe_instance evd l =
- let vars = ref (UState.subst evd.universes) in
+ let vars = UState.subst evd.universes in
let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
Univ.Instance.subst_fn normalize l
diff --git a/engine/uState.ml b/engine/uState.ml
index 6c8dbe3f44..df50bae86e 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -156,7 +156,7 @@ let process_universe_constraints ctx cstrs =
let univs = ctx.uctx_universes in
let vars = ref ctx.uctx_univ_variables in
let weak = ref ctx.uctx_weak_constraints in
- let normalize = normalize_univ_variable_opt_subst vars in
+ let normalize u = normalize_univ_variable_opt_subst !vars u in
let nf_constraint = function
| ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
| UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v)
diff --git a/engine/universes.ml b/engine/universes.ml
index 938f5ad9cb..a13663cbad 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -605,31 +605,25 @@ let fresh_universe_context_set_instance ctx =
let cst' = subst_univs_level_constraints subst cst in
subst, (univs', cst')
-let normalize_univ_variable ~find ~update =
+let normalize_univ_variable ~find =
let rec aux cur =
let b = find cur in
let b' = subst_univs_universe aux b in
if Universe.equal b' b then b
- else update cur b'
+ else b'
in aux
let normalize_univ_variable_opt_subst ectx =
let find l =
- match Univ.LMap.find l !ectx with
+ match Univ.LMap.find l ectx with
| Some b -> b
| None -> raise Not_found
in
- let update l b =
- assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
- try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false
- in normalize_univ_variable ~find ~update
+ normalize_univ_variable ~find
let normalize_univ_variable_subst subst =
- let find l = Univ.LMap.find l !subst in
- let update l b =
- assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
- try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in
- normalize_univ_variable ~find ~update
+ let find l = Univ.LMap.find l subst in
+ normalize_univ_variable ~find
let normalize_universe_opt_subst subst =
let normlevel = normalize_univ_variable_opt_subst subst in
@@ -640,13 +634,10 @@ let normalize_universe_subst subst =
subst_univs_universe normlevel
let normalize_opt_subst ctx =
- let ectx = ref ctx in
- let normalize = normalize_univ_variable_opt_subst ectx in
- let () =
- Univ.LMap.iter (fun u v ->
- if Option.is_empty v then ()
- else try ignore(normalize u) with Not_found -> assert(false)) ctx
- in !ectx
+ let normalize = normalize_universe_opt_subst ctx in
+ Univ.LMap.mapi (fun u -> function
+ | None -> None
+ | Some v -> Some (normalize v)) ctx
type universe_opt_subst = Universe.t option universe_map
@@ -655,7 +646,7 @@ let subst_univs_fn_puniverses f (c, u as cu) =
if u' == u then cu else (c, u')
let nf_evars_and_universes_opt_subst f subst =
- let subst = normalize_univ_variable_opt_subst (ref subst) in
+ let subst = normalize_univ_variable_opt_subst subst in
let lsubst = level_subst_of subst in
let rec aux c =
match kind c with
@@ -975,7 +966,7 @@ let normalize_context_set g ctx us algs weak =
(* Process weak constraints: when one side is flexible and the 2
universes are unrelated unify them. *)
let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
- let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in
+ let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
let u = norm u and v = norm v in
let set_to a b =
(LSet.remove a ctx,
@@ -994,7 +985,6 @@ let normalize_context_set g ctx us algs weak =
(* Noneqs is now in canonical form w.r.t. equality constraints,
and contains only inequality constraints. *)
let noneqs =
- let us = ref us in
let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
Constraint.fold (fun (u,d,v) noneqs ->
let u = norm u and v = norm v in
diff --git a/engine/universes.mli b/engine/universes.mli
index e6bee42bb3..df2e961d60 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -184,19 +184,18 @@ val normalize_univ_variables : universe_opt_subst ->
val normalize_univ_variable :
find:(Level.t -> Universe.t) ->
- update:(Level.t -> Universe.t -> Universe.t) ->
Level.t -> Universe.t
-val normalize_univ_variable_opt_subst : universe_opt_subst ref ->
+val normalize_univ_variable_opt_subst : universe_opt_subst ->
(Level.t -> Universe.t)
-val normalize_univ_variable_subst : universe_subst ref ->
+val normalize_univ_variable_subst : universe_subst ->
(Level.t -> Universe.t)
-val normalize_universe_opt_subst : universe_opt_subst ref ->
+val normalize_universe_opt_subst : universe_opt_subst ->
(Universe.t -> Universe.t)
-val normalize_universe_subst : universe_subst ref ->
+val normalize_universe_subst : universe_subst ->
(Universe.t -> Universe.t)
(** Create a fresh global in the global environment, without side effects.
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index b6462c8106..c949589e22 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map ->
(** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *)
let id_map_try_add id x m =
match id with
- | Some id -> Id.Map.add id x m
+ | Some id -> Id.Map.add id (Lazy.force x) m
| None -> m
(** Adds a binding to a {!Id.Map.t} if the name is [Name id] *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 89d490a410..b4e1a1b102 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -427,7 +427,7 @@ let special_meta = (-1)
type matching_result =
{ m_sub : bound_ident_map * patvar_map;
- m_ctx : constr; }
+ m_ctx : constr Lazy.t; }
let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
@@ -451,7 +451,7 @@ let authorized_occ env sigma closed pat c mk_ctx =
let subst = matches_core_closed env sigma pat c in
if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
then (fun next -> next ())
- else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
+ else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next)
with PatternMatchingFailure -> (fun next -> next ())
let subargs env v = Array.map_to_list (fun c -> (env, c)) v
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 3c2c73915f..d19789ef42 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -61,7 +61,7 @@ val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool
(whose hole is denoted here with [special_meta]) *)
type matching_result =
{ m_sub : bound_ident_map * patvar_map;
- m_ctx : EConstr.t }
+ m_ctx : EConstr.t Lazy.t }
(** [match_subterm pat c] returns the substitution and the context
corresponding to each **closed** subterm of [c] matching [pat],
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:58:27 +0000