Skip to content

Commit

Permalink
Avoid retypechecking repeated subterms in typeops
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Jun 20, 2024
1 parent bbcefd9 commit 31e590b
Show file tree
Hide file tree
Showing 5 changed files with 526 additions and 61 deletions.
6 changes: 4 additions & 2 deletions kernel/constr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1147,8 +1147,8 @@ let invert_eqeq iv1 iv2 =
let hasheq_ctx (nas1, c1) (nas2, c2) =
array_eqeq nas1 nas2 && c1 == c2

let hasheq t1 t2 =
match kind t1, kind t2 with
let hasheq_kind t1 t2 =
match t1, t2 with
| Rel n1, Rel n2 -> n1 == n2
| Meta m1, Meta m2 -> m1 == m2
| Var id1, Var id2 -> id1 == id2
Expand Down Expand Up @@ -1189,6 +1189,8 @@ let hasheq t1 t2 =
| App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
| Fix _ | CoFix _ | Int _ | Float _ | String _ | Array _), _ -> false

let hasheq t1 t2 = hasheq_kind (kind t1) (kind t2)

(** Note that the following Make has the side effect of creating
once and for all the table we'll use for hash-consing all constr *)

Expand Down
9 changes: 9 additions & 0 deletions kernel/constr.mli
Original file line number Diff line number Diff line change
Expand Up @@ -630,6 +630,9 @@ val case_info_hash : case_info -> int

val hcons : constr -> constr

val hasheq_kind : (_ kind_of_term as 'k) -> 'k -> bool
(** Checks physical equality of every immediate element (goes inside tuples and arrays) *)

val debug_print : constr -> Pp.t
val debug_print_fix : ('a -> Pp.t) -> ('a, 'a, 'r) pfixpoint -> Pp.t

Expand All @@ -641,3 +644,9 @@ val mkInd : inductive -> constr

val mkConstruct : constructor -> constr
[@@deprecated "Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct]"]

val hcons_annot : Name.t binder_annot -> Name.t binder_annot

val hcons_caseinfo : case_info -> case_info

val hash_cast_kind : cast_kind -> int
Loading

0 comments on commit 31e590b

Please sign in to comment.